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