Propriété Q1: le taux de boursiers est satisfait par l'ordre d'appel

Si C = { d₁, ..., d_n} est l'ensemble des candidats et q_B le taux boursier alors:
Pour tout k = 1, ..., n:
- au moins ⌈q_B * k⌉ des candidats d₁, ..., d_k sont boursiers;
- ou sinon, aucun candidat parmi d_k+1, ..., d_n n’est boursier.

module Q1
  use int.Int
  use seq.Seq

  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.SeqVoeux

  (* Si 's' est l'ordre d'appel courant de longueur 'n', tous ses préfixes de 
   * longueur k satisfont Q1 exprimée de la manière suivante:
   * - le préfixe s[..k] = s[0], ..., s[k-1] satisfait le taux boursier 'tx' 
   *   (par rapport à sa longueur); 
   * - ou sinon, le suffixe s[k..] = s[k], ..., s[n-1] ne contient pas de 
   *   boursier.
   *)
  predicate q1_loc (tx_b : taux) (s : seq_voeu) (k : int) =
    (* Soit le taux est respecté s[0],..., s[k-1]. *)
    seq_respecte_taux_b tx_b s[..k]
    (* Soit il n'y a plus de boursiers après k. *)
    \/ non_boursiers_seulement s[k..]

  predicate q1 (tx_b : Taux.t) (oa : seq_voeu) =
    forall k. 0 <= k <= length oa -> q1_loc tx_b oa k
end

module Q1_UpToRangAppel
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use export Q1

  let lemma q1_up_to_rang_appel_oa (tx_b : Taux.t) (oa1 oa2 : seq_voeu)
    requires { q1 tx_b oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { q1 tx_b oa2 }
  =
   ()
end

module Q1_Snoc
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use proofs.ordre_appel.invariants.iq1.IQ1_Lemmas
  use proofs.ordre_appel.invariants.iq1.IQ1_Snoc
  use export Q1

  (*
   * Preuve que Q1 est maintenue lorsque l'on ajoute un nouveau candidat 'v'.
   * 
   * Ce dernier choisi par l'algorithme de telle manière que:
   * - si il est boursier alors il restait des boursiers au moment du choix de 
   * 'v' i.e. #boursiers(s) < #boursiers(g)
   * - si il n'est boursier alors il n'y avait pas de contrainte sur le taux 
   *   pour le choix de 'v'
   *)
  let lemma q1_snoc (nb_b : int) (tx_b : Taux.t) (s : seq_voeu) (v : VoeuClasse.t)
    requires { [@expl:pre/Q1(s)] q1 tx_b s }
    requires { [@expl:pre/IQ1(s.v)] iq1 nb_b tx_b (snoc s v) }
    requires { [@expl:pre/v boursier -> il reste des boursiers] est_boursier v -> remains_boursiers s nb_b }
    requires { [@expl:pre/v non boursier -> tx_b non contraignant] not est_boursier v -> not taux_b_contraignant tx_b s nb_b }

    ensures {[@expl:Q1(s.v)] q1 tx_b (snoc s v) }
  =
    let s' = snoc s v in
    for k = 0 to length s'-1 do
      invariant { forall i. 0 <= i < k -> q1_loc tx_b s' i }

     assert {[@expl:iq1 s(..k)] iq1_loc nb_b tx_b s' k };
      if k < length s' - 1 then begin
        assert { s'[k..] == snoc s[k..] v };
        assert { s'[..k] == s[..k] };
        assert { [@expl:q1 s(..k)] q1_loc tx_b s k };
        assert { [@expl:q1 s'(..k)] q1_loc tx_b s' k };
      end else if est_boursier v then begin
        iq1_l2a_b tx_b s v
      end else begin
	      iq1_l2b_b nb_b tx_b s v
      end
    done

  let lemma q1_empty (tx_b : Taux.t) (s : seq_voeu)
    requires { s = Seq.empty }
    ensures { q1 tx_b s }
  = ()

end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)