Parcoursup / Calcul de l'ordre d'appel des candidats index


module IQ4_2
  use int.Int
  use seq.Seq
  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.SeqVoeuxEqUpToRangAppel
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props

  clone proofs.ordre_appel.invariants.iq4_xa.IQ4_xa as IQ4_2a with function est_x = est_boursier

  function in_Zb (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (i : int) : bool =
     IQ4_2a.in_Z oa tx_b nb_b i

  function nb_contraintes_taux_b (nb_b: int) (tx_b : Taux.t) (oa : seq_voeu) : int =
     IQ4_2a.nb_contraintes_taux_x oa tx_b nb_b

  let lemma in_Zb_eq_up_to_rang_appel (s1 s2 : seq_voeu) (nb_b : int) (tx_b : Taux.t) (i : int)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    requires { 0 <= i < length s1 }
    ensures { in_Zb nb_b tx_b s1 i = in_Zb nb_b tx_b s2 i }
  =
    ()

  let lemma nb_contraintes_taux_b_up_to_rang_appel (s1 s2 : seq_voeu) (tx_b : taux) (nb_b : int) (i : int)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    requires { 0 <= i < length s1 }
    ensures { nb_contraintes_taux_b nb_b tx_b s1[..i] = nb_contraintes_taux_b nb_b tx_b s2[..i] }
  =
    ()

  let lemma not_in_Zb (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) (i : int)
    requires { not in_Zb nb_b tx_b s i }
    ensures { not est_boursier s[i] \/ not taux_b_contraignant tx_b s[..i] nb_b }
  = ()

  let lemma taux_b_0_imp_not_in_Zb (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) (i : int)
     requires { tx_b = 0 }
     ensures { not in_Zb nb_b tx_b s i }
  = ()

  predicate iq4_2a_loc (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) (k : int) =
    (* IQ4_2a.iq4_xa_loc s taux_b total_b k *)
    forall i. 0 <= i <= k ->
      let taux_b = tx_b in
      let nbCb = nb_contraintes_taux_b nb_b taux_b s[..i] in
          100 * nbCb <= taux_b * i + 100

  let lemma iq4_2a_loc_equiv (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) (k : int)
     ensures { iq4_2a_loc nb_b tx_b s k <-> IQ4_2a.iq4_xa_loc s tx_b nb_b k }
  = ()

  predicate iq4_2a (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) =
    (* IQ4_2a.iq4_xa s taux_b total_b  *)
    forall k. 0 <= k <= length s -> iq4_2a_loc nb_b tx_b s k

  let lemma iq4_2a_equiv (nb_b: int) (tx_b : Taux.t) (s : seq_voeu)
     ensures { iq4_2a nb_b tx_b s <-> IQ4_2a.iq4_xa s tx_b nb_b }
  = ()

  predicate iq4_2b_loc (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) (m : EnumMap.t) (k : int) =
    forall i. 0 <= i <= k ->
    (not in_Zb nb_b tx_b s i) ->
      ((forall v. enummap_est_du_secteur m v -> voeu_lt s[i] v) &&
       (forall v. seq_contains v s[i+1..] -> est_du_secteur v -> voeu_lt s[i] v))

  predicate iq4_2b  (nb_b: int) (tx_b : Taux.t) (s : seq_voeu) (m : EnumMap.t) =
    forall k. 0 <= k < length s -> iq4_2b_loc nb_b tx_b s m k

  predicate iq4_2 (nb_b: int) (tx_b : Taux.t) (oak : seq_voeu) (m : EnumMap.t) =
    iq4_2a nb_b tx_b oak && iq4_2b nb_b tx_b oak m

end

module IQ4_2_UpToRangAppel
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use export IQ4_2

  let lemma iq4_2a_up_to_rang_appel_oa (nb_b : int) (tx_b : Taux.t) (oa1 oa2 : seq_voeu)
    requires { iq4_2a nb_b tx_b oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { iq4_2a nb_b tx_b oa2 }
  =
    for i = 0 to length oa2 do
      invariant { [@expl:iq4_2a_loc] forall k. 0 <= k < i -> iq4_2a_loc nb_b tx_b oa2 k }
      IQ4_2a.nb_contraintes_taux_x_up_to_rang_appel oa1 oa2 tx_b nb_b i;
      assert { iq4_2a_loc nb_b tx_b oa1 i };
      let nbCb1 = nb_contraintes_taux_b nb_b tx_b oa1[..i] in
      let nbCb2 = nb_contraintes_taux_b nb_b tx_b oa2[..i] in
      assert { nbCb1 = nbCb2};
      assert { 100 * nbCb1 <= tx_b * i + 100 };
      assert { 100 * nbCb2 <= tx_b * i + 100 };
    done
end

module IQ4_2_Lemmas
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.eligibles.Eligibles
  use proofs.ordre_appel.eligibles.ValidEligibles
  use proofs.ordre_appel.invariants.iq3_2.IQ3_2

  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Lemmas
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts

  use IQ4_2

  let lemma iq4_2b_loc_ex (nb_b : int) (tx_b : Taux.t) (s : seq_voeu) (m : EnumMap.t) (k : int)
    requires {
      (forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b s i) ->
        ((forall v. enummap_est_du_secteur m v -> voeu_lt s[i] v) &&
          (forall v. seq_contains v s[i+1..] -> est_du_secteur v -> voeu_lt s[i] v))) }
    ensures { iq4_2b_loc nb_b tx_b s m k }
  = ()

  let lemma aux1 (cB cR : bool) (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) (om m : EnumMap.t)
                 (eligibles: PQueue.t) (x : voeu)
    requires {[@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
    requires {[@expl:alld m] enummap_all_distincts om }
    requires {[@expl:x selected] enummap_pop_v om m x }
    requires {[@expl:iq3_2 oak+x] iq3_2 (snoc oak x) m }
    requires { not Fset.is_empty eligibles }
    requires { not taux_b_contraignant tx_b oak nb_b && not cB }
    ensures { forall v. enummap_est_du_secteur m v -> voeu_lt x v }
  =
    assert {[@expl:A 0] eligibles_contains_eligible_heads cB cR om eligibles };
    let lemma aux11 (v h : VoeuClasse.t)

      requires { enummap_est_du_secteur m v }
      requires { get_type_candidat x <> get_type_candidat v }
      requires { h = Seq.get (EnumMap.get_queue om (get_type_candidat v)) 0 }

      ensures { h = Seq.get (EnumMap.get_queue m (get_type_candidat v)) 0 }
      ensures { est_du_secteur h }
      ensures { seq_contains v (EnumMap.get_queue m (get_type_candidat v)) }
      ensures { est_eligible_p cB cR h }
      ensures { Fset.mem h eligibles }
      ensures { h <> x }
      ensures { voeu_lt x h }
      ensures { v <> h -> voeu_lt h v }
    =
      assert { seq_contains v (get_queue om (get_type_candidat v)) };
      assert { get_type_candidat v = get_type_candidat h };
      assert { enummap_v_is_head om h };

      enummap_poped_head_saved om m x v h;
      enummap_head_is_lt_its_queue m v h in

    assert { forall v. enummap_contains m v -> est_du_secteur v -> x <> v };

    assert { forall v. enummap_contains m v -> est_du_secteur v ->
     	        (get_type_candidat x) <> (get_type_candidat v) ->
	              let q = EnumMap.get_queue m (get_type_candidat v) in
	                voeu_lt x q[0] };

    assert { forall v. enummap_contains m v -> est_du_secteur v ->
     	         (get_type_candidat x) <> (get_type_candidat v) ->
	                let q = EnumMap.get_queue m (get_type_candidat v) in
   	                (v <> q[0] -> voeu_lt x v) };

    assert { forall v. enummap_contains m v -> est_du_secteur v ->
     	        (get_type_candidat x) <> (get_type_candidat v) ->
	                voeu_lt x v };

    assert { forall v. enummap_contains m v -> est_du_secteur v ->
     	         (get_type_candidat x) = (get_type_candidat v) ->
	                EnumMap.get_queue m (get_type_candidat v)  = EnumMap.get_queue m (get_type_candidat x) };

    assert { forall v. enummap_contains m v -> est_du_secteur v ->
     	         (get_type_candidat x) = (get_type_candidat v) ->
	                let q = EnumMap.get_queue m (get_type_candidat v) in
      	            voeu_lt_than_queue x q  };

    assert { forall v. enummap_contains m v -> est_du_secteur v ->
     	         (get_type_candidat x) = (get_type_candidat v) ->
	                let q = EnumMap.get_queue m (get_type_candidat v) in
      	            voeu_lt_than_queue x q so voeu_lt x v };

    assert { forall v. enummap_contains m v -> est_du_secteur v -> voeu_lt x v }

  let lemma iq4_2b_snoc_aux (cB cR : bool) (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) (om m : EnumMap.t)
                            (eligibles: PQueue.t) (x : voeu)
    requires {[@expl:pre iq4_2b] iq4_2b nb_b tx_b oak om }
    requires {[@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
    requires {[@expl:alld m] enummap_all_distincts om }
    requires {[@expl:x selected] enummap_pop_v om m x }
    requires {[@expl:iq3_2 oak+x] iq3_2 (snoc oak x) m }
    requires {[@expl:cR equiv tx_ds contraignant] cB = taux_b_contraignant tx_b oak nb_b }
    requires { not in_Zb nb_b tx_b (snoc oak x) (length oak) }
    ensures  { iq4_2b_loc nb_b tx_b (snoc oak x) m (length oak) }
  =
    let s = snoc oak x in
    let k = length s - 1 in
    assert { iq4_2b_loc nb_b tx_b oak om (k-1) };
    assert { forall i. 0 <= i <= k-1 -> (not in_Zb nb_b tx_b oak i) ->
                forall v. enummap_est_du_secteur om v -> voeu_lt oak[i] v };

    assert { forall i. 0 <= i <= k-1 -> (not in_Zb nb_b tx_b oak i) ->
               forall v. seq_contains v oak[i+1..] -> est_du_secteur v -> voeu_lt oak[i] v };

    assert { forall i. 0 <= i <= k-1 -> not in_Zb nb_b tx_b s i -> not in_Zb nb_b tx_b oak i };
    assert { enummap_contains om x };
    assert { est_du_secteur x -> enummap_est_du_secteur om x };
    assert { forall i. 0 <= i <= k-1 -> not in_Zb nb_b tx_b oak i -> est_du_secteur x -> voeu_lt oak[i] x };

    seq_suffix_snoc s oak x;

    assert { forall i. 0 <= i <= (k-1) -> not in_Zb nb_b tx_b oak i ->
               forall v. seq_contains v oak[i+1..] -> est_du_secteur v -> voeu_lt oak[i] v };

    assert { forall i. 0 <= i <= k-1 ->
               forall v. seq_contains v s[i+1..] -> seq_contains v (snoc oak [i+1..] x) };

    assert { forall i. 0 <= i <= k-1 -> (not in_Zb nb_b tx_b s i) ->
              forall v. seq_contains v s[i+1..] -> est_du_secteur v -> x = v -> voeu_lt oak[i] x };

    assert { forall i. 0 <= i <= k-1 -> (not in_Zb nb_b tx_b s i) ->
              forall v. seq_contains v s[i+1..] -> est_du_secteur v -> x <> v -> voeu_lt s[i] v };

    assert { forall i. 0 <= i <= k-1 -> (not in_Zb nb_b tx_b s i) ->
              forall v. enummap_est_du_secteur m v -> voeu_lt s[i] v };

    assert { forall i. 0 <= i <= k-1 -> (not in_Zb nb_b tx_b s i) ->
              ((forall v. enummap_est_du_secteur m v -> voeu_lt s[i] v) &&
                (forall v. seq_contains v s[i+1..] -> est_du_secteur v -> voeu_lt s[i] v)) };
    iq4_2b_loc_ex nb_b tx_b s m (k-1);
    assert { iq4_2b_loc nb_b tx_b s m (k-1) };

    if not taux_b_contraignant tx_b oak nb_b then
    begin
     if not PQueue.is_empty eligibles then begin
       aux1 cB cR nb_b tx_b oak om m eligibles x;
       iq4_2b_loc_ex nb_b tx_b s m k;
       assert { iq4_2b_loc nb_b tx_b s m k };
     end else
       absurd;
    end else begin
     assert { not est_boursier x };
     assert { est_eligible_p cB cR x };

     absurd;
    end

  let lemma iq4_2a_snoc (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) (x : voeu)
    requires { iq4_2a nb_b tx_b oak }
    ensures { iq4_2a nb_b tx_b (snoc oak x) }
  = ()

 let lemma iq4_2b_snoc (cB cR : bool) (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) (om m : EnumMap.t)
                       (eligibles: PQueue.t) (x : voeu)
   requires { [@expl:pre iq4_2b] iq4_2b nb_b tx_b oak om }
   requires { [@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
   requires { [@expl:alld m] enummap_all_distincts om }
   requires { [@expl:x selected] enummap_pop_v om m x }
   requires { [@expl:iq3_2 oak+x] iq3_2 (snoc oak x) m }
   requires { [@expl:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b }
   ensures { iq4_2b nb_b tx_b (snoc oak x) m }
 =
   let s = snoc oak x in
   assert { enummap_contains om x };
   assert { est_du_secteur x -> enummap_est_du_secteur om x };

   for k = 0 to length s - 1 do
     invariant { forall j. 0 <= j < k -> iq4_2b_loc nb_b tx_b s m j }
     assert { forall i. 0 <= i < k -> s[i] = oak[i] };
     assert { forall i. 0 <= i <= k -> s[..i] == oak[..i] };
     if k < length s - 1 then
     begin
       assert { forall i. 0 <= i <= k -> s[i+1..] == snoc oak[i+1..] x };
       assert { iq4_2b_loc nb_b tx_b oak om k };
       assert { forall i. 0 <= i < k -> s[i] = oak[i] };
       assert {  forall v. enummap_est_du_secteur m v -> enummap_est_du_secteur om v };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b s i) -> (not in_Zb nb_b tx_b oak i) };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b oak i) -> forall v. enummap_est_du_secteur om v -> voeu_lt oak[i] v };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b s i) -> forall v. enummap_est_du_secteur m v -> voeu_lt s[i] v };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b oak i) -> forall v. seq_contains v oak[i+1..] -> est_du_secteur v -> voeu_lt oak[i] v };
       seq_suffix_snoc s oak x;
       assert { forall i. 0 <= i <= k -> forall v. seq_contains v s[i+1..] -> est_du_secteur v -> seq_contains v (snoc oak[i+1..] x) };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b s i) -> forall v. seq_contains v s[i+1..] -> est_du_secteur v -> voeu_lt s[i] v };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b s i) -> forall v. enummap_est_du_secteur m v -> voeu_lt s[i] v };
       assert { forall i. 0 <= i <= k -> (not in_Zb nb_b tx_b s i) -> forall v. seq_contains v s[i+1..] -> est_du_secteur v -> voeu_lt s[i] v };
       iq4_2b_loc_ex nb_b tx_b s m k;
       assert { iq4_2b_loc nb_b tx_b s m k };
     end
     else
     begin
       assert { forall i. 0 <= i < k -> s[i+1..] == snoc oak[i+1..] x };
       assert { iq4_2b_loc nb_b tx_b oak om (k-1) };
       assert { forall i. 0 <= i < k -> s[i] = oak[i] };
       assert {  forall v. enummap_est_du_secteur m v
       	       	 -> enummap_est_du_secteur om v };
       assert { forall i. 0 <= i < length s - 1 ->
    	 	 (not in_Zb nb_b tx_b oak i) ->
     		 forall v. enummap_est_du_secteur om v ->
		 voeu_lt oak[i] v };

       assert { forall i. 0 <= i < length s - 1 ->
    	 	 (not in_Zb nb_b tx_b s i) ->
     		 forall v. enummap_est_du_secteur m v ->
		 voeu_lt s[i] v };

       assert { forall i. 0 <= i < k ->
    	 	 (not in_Zb nb_b tx_b oak i) ->
     		 forall v. seq_contains v oak[i+1..] -> est_du_secteur v ->
		 voeu_lt oak[i] v };
       assert { forall i. 0 <= i < k ->
     		  forall v. seq_contains v s[i+1..] ->
		  est_du_secteur v ->
		  (seq_contains v (snoc oak[i+1..] x) ) };

       assert { forall i. 0 <= i < length s - 1 ->
    	 	 (not in_Zb nb_b tx_b s i) ->
     		 forall v. seq_contains v s[i+1..] -> est_du_secteur v ->
		 voeu_lt s[i] v };
       iq4_2b_loc_ex nb_b tx_b s m (k-1);
       assert { iq4_2b_loc nb_b tx_b oak m (k-1) };
       if in_Zb nb_b tx_b s (length s -1) then begin
       iq4_2b_loc_ex nb_b tx_b s m k;
         assert { iq4_2b_loc nb_b tx_b s m k }
       end else
      	 iq4_2b_snoc_aux cB cR nb_b tx_b oak om m eligibles x;
     end
   done
end

module IQ4_2_Snoc
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.eligibles.Eligibles
  use proofs.ordre_appel.eligibles.ValidEligibles
  use proofs.ordre_appel.invariants.iq3_2.IQ3_2

  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Lemmas
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts

  use IQ4_2_Lemmas

  use export IQ4_2

  let lemma iq4_2_snoc (cB cR : bool) (nb_b : int) (tx_b : Taux.t) (oak : seq_voeu) (om m : EnumMap.t)
                     (eligibles: PQueue.t) (x : voeu)
    requires {[@expl:valid eligibles] meilleur_eligible cB cR om eligibles x }
    requires {[@expl:alld m] enummap_all_distincts om }
    requires {[@expl:x selected] enummap_pop_v om m x }
    requires {[@expl:iq3_2 oak+x] iq3_2 (snoc oak x) m }
    requires {[@expl:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b }
    requires {[@expl:pre iq4_2] iq4_2 nb_b tx_b oak om }
    ensures  {[@expl:iq4_2(oak.x)] iq4_2 nb_b tx_b (snoc oak x) m }
  =
    ()

  use proofs.ordre_appel.invariants.iq0.IQ0
  let lemma iq4_2_empty (nb_b : int) (tx_b : Taux.t) (op oak : seq_voeu) (m : EnumMap.t)
    requires { oak = Seq.empty }
    requires { nb_b = nb_boursiers op }
    requires { iq0 op oak m }
    ensures { iq4_2 nb_b tx_b empty m }
  =
    ()

end

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

Generated by why3doc 1.7.2+git