Propriété Q2: le taux de résidents est satisfait par l'ordre d'appel

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

module Q2
  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.taux.Taux

  predicate q2_k_prime_p (k kp : int) (tx_b : taux) =
    (100 - tx_b) * k -100 <= (100 - tx_b) * kp &&
    (forall kp'. (100 - tx_b) * k -100 <= (100 - tx_b) * kp' -> kp <= kp')

  let ghost function q2_k_prime (k : int ) (tx_b : taux) : int
     requires { 0 <= (100 - tx_b) * k -100 }
     requires { 0 <= k }
     ensures { q2_k_prime_p k result tx_b }
     ensures { result <= k }
  = let rec ghost function aux (kp: int) : int
      requires { (100 - tx_b) * k -100 <= (100 - tx_b) * kp }
      ensures { q2_k_prime_p k result tx_b }
      ensures { result <= k }
      variant { kp }
    = if (100 - (to_int tx_b)) * k -100 <= (100 - (to_int tx_b)) * (kp-1) then
        aux (kp-1)
      else
        kp
     in aux k

  predicate q2_loc (tx_b tx_ds : Taux.t) (s: seq_voeu) (k : int) =
    0 <= (100-tx_b) * k - 100 ->
    let kp = q2_k_prime k tx_b in
      ((kp*tx_ds <= 100 * nb_du_secteur s[..k] \/
        kp*(100-tx_b) <= (200 - tx_b) * nb_du_secteur s[..k])
	\/ hors_secteur_seulement s[k..])

  predicate q2 (tx_b tx_r : Taux.t) (oa : seq_voeu) =
      forall k. 0 <= k <= length oa -> q2_loc tx_b tx_r oa k

end

module Q2_UpToRangAppel
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use export Q2

  let lemma q2_up_to_rang_appel_oa (tx_b tx_r : Taux.t) (oa1 oa2 : seq_voeu)
    requires { q2 tx_b tx_r oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { q2 tx_b tx_r oa2 }
  =
    for i = 0 to length oa2 do
      invariant { forall k. 0 <= k < i -> q2_loc tx_b tx_r oa2 k }
      assert { q2_loc tx_b tx_r oa1 i }
    done
end

module Q2_Lemmas
  use int.Int
  use seq.Seq
  use seq.FreeMonoid
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTauxMinore

  use proofs.ordre_appel.invariants.iqx.IQX
  use proofs.ordre_appel.invariants.iq2.IQ2_Lemmas
  use proofs.ordre_appel.invariants.iq2.IQ2_Snoc

  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux

  use Q2

  let lemma q2_snoc_aux (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s oak : seq_voeu) (v : voeu) (k : int)
    requires { s == snoc oak v }
    requires { q2 tx_b tx_ds oak }
    requires { iqx_2 nb_b tx_b (snoc oak v) }
    requires { iqx_3ds nb_ds (snoc oak v) }
    requires { iq2 nb_b nb_ds tx_b tx_ds (snoc oak v) }
    requires { conflit_taux s[..k-1] tx_b nb_b tx_ds nb_ds }
    requires { remains_du_secteur s[..k] nb_ds }
    requires { (100 - tx_b) * k >= 100 }
    requires { 0 <= k < length s }
    ensures { q2_loc tx_b tx_ds s k }
  =
    assert { taux_b_contraignant tx_b s[..k-1] nb_b };
    let x = iq2_case_2_2_x nb_b nb_ds tx_b tx_ds s[..k-1] (k-1) in
    (* L5 est applicable grace à iqX_2 *)
    iq2_l5 nb_b tx_b s[..k-1] x ;
    assert { length s[x..k-1] * (100 - tx_b) <= tx_b };
    assert { (k-1-x) * (100 - tx_b) <= tx_b };
    assert { (100-tx_b) * k -100 <=  (100-tx_b)*x };

    assert { [@expl: iq2 s(..x)] iq2_loc nb_b nb_ds tx_b tx_ds s (x-1) };
    assert { [@expl: s(..x) respected ds_min] seq_respecte_taux_ds_minore tx_b tx_ds s[..x] };

    cat_dec s[..k] x;
    assert { s[..k] == s[..x] ++ s[x..k] };
    let nb_ds_x = nb_du_secteur s[..x] in
    let nb_ds_k = nb_du_secteur s[..k] in
    nb_du_secteur_app s[..k] s[..x] s[x..k];
    assert { nb_ds_k >= nb_ds_x };
    assert { taux_ds_minore_ok tx_b tx_ds nb_ds_x x };
    assert { 100 * nb_ds_x >= tx_ds * x \/ (200 - tx_b)*(nb_ds_x) >= (100 - tx_b) * x };

    assert { taux_ds_minore_ok tx_b tx_ds (nb_du_secteur s[..k]) x };
    assert { tx_ds * x <= 100 * nb_ds_k \/ (100 - tx_b) * x <= (200 - tx_b)*(nb_ds_k) };
    let kp = q2_k_prime k tx_b in
    assert { kp <= x };
    assert { tx_ds * kp <= 100 * nb_ds_k \/ (100 - tx_b) * kp <= (200 - tx_b) * (nb_ds_k) };
    assert { q2_loc tx_b tx_ds s k }
end

module Q2_Snoc
  use int.Int
  use seq.Seq
  use seq.FreeMonoid
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTauxMinore

  use proofs.ordre_appel.invariants.iqx.IQX
  use proofs.ordre_appel.invariants.iq2.IQ2_Lemmas
  use proofs.ordre_appel.invariants.iq2.IQ2_Snoc

  use Q2_Lemmas
  use export Q2

  let lemma q2_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oak : seq_voeu) (v : voeu)
     requires { [@expl:pre q2 / iqx_2] iqx_2 nb_b tx_b (snoc oak v) }
     requires { [@expl:pre q2 / iqx_3ds] iqx_3ds nb_ds (snoc oak v) }
     requires { [@expl:pre q2 / iq2] iq2 nb_b nb_ds tx_b tx_ds (snoc oak v) }
     requires { [@expl:pre q2 / q2] q2 tx_b tx_ds oak }
     ensures { q2 tx_b tx_ds (snoc oak v) }
  =
    let s = snoc oak v in

    for k = 0 to length s - 1 do
      invariant { forall i. 0 <= i < k -> q2_loc tx_b tx_ds s i }

      if (100 - (Taux.to_int tx_b)) * k < 100 then
      begin
	      assert { [@expl:q2 s[..k] q2_loc tx_b tx_ds s k };
        continue;
      end;

      if not remains_du_secteur s[..k] nb_ds then
      begin (* thanks to iqX_3ds *)
        assert { [@expl:seulement hs s(k..)] hors_secteur_seulement s[k..] };
	      assert { [@expl:q2 s[..k] q2_loc tx_b tx_ds  s k };
        continue;
      end;

      if not conflit_taux s[..k-1] tx_b nb_b tx_ds nb_ds then
      begin
        assert { [@expl:iq2 s(..k-1)] iq2_loc nb_b nb_ds tx_b tx_ds s (k-1) };
	      assert { [@expl:iq2 s(..k+1) respected ds_min] seq_respecte_taux_ds_minore tx_b tx_ds s[..k] };

        let kp = q2_k_prime k tx_b in
      	let nb_ds = nb_du_secteur s[..k] in

	      if taux_ok tx_ds nb_ds k then
	      begin
	        assert { tx_ds * k <= 100 * nb_ds };
	        assert { kp * tx_ds <= k * tx_ds };
    	    assert { kp * tx_ds  <= 100 * nb_ds };
          assert { [@expl:q2 s[..k] q2_loc tx_b tx_ds  s k };
	      end else begin
	        assert { kp <= k };
          assert { 0 <= (100 - tx_b) * k -100 <= (100 - tx_b) * kp };
	        seq_respecte_taux_ds_minore_p1 s[..k] tx_b tx_ds;
 	        assert { (100 - tx_b) * k <= (200 - tx_b) * nb_ds };
  	      assert { (100 - tx_b) * kp <= (200 - tx_b) * nb_ds };
          assert { [@expl:q2 s[..k] q2_loc tx_b tx_ds s k };
	      end;
        continue;
      end;
      q2_snoc_aux nb_b nb_ds tx_b tx_ds s oak v k;
      assert { [@expl:q2 s[..k] q2_loc tx_b tx_ds  s k };
    done

  let lemma q2_empty (tx_b tx_ds : Taux.t) (oak : seq_voeu)
    requires { oak = Seq.empty }
    ensures { q2 tx_b tx_ds oak }
  =
    ()

end

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