Parcoursup / Calcul de l'ordre d'appel des candidats index
module IQ2 use seq.Seq use int.Int use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use proofs.ordre_appel.seq_voeux.SeqVoeuxTauxMinore use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap predicate iq2_loc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) = remains_du_secteur s[..i] nb_ds -> not conflit_taux s[..i] tx_b nb_b tx_ds nb_ds -> seq_respecte_taux_ds_minore tx_b tx_ds s[..i+1] predicate iq2 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) = forall i. 0 <= i < length s -> iq2_loc nb_b nb_ds tx_b tx_ds s i end module IQ2_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 fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use proofs.ordre_appel.invariants.iqx.IQX use proofs.ordre_appel.invariants.iq1.IQ1_Lemmas use IQ2 let lemma iq2_l4 (s1 s2 : seq_voeu) (taux_b taux_ds : taux) ensures { (seq_respecte_taux_b taux_b s1 && seq_respecte_taux_b taux_b s2) -> seq_respecte_taux_b taux_b (s1 ++ s2) } ensures { (seq_respecte_taux_ds taux_ds s1 && seq_respecte_taux_ds taux_ds s2) -> seq_respecte_taux_ds taux_ds (s1 ++ s2) } ensures { (seq_respecte_taux_ds_minore taux_b taux_ds s1 && seq_respecte_taux_ds_minore taux_b taux_ds s2) -> seq_respecte_taux_ds_minore taux_b taux_ds (s1 ++ s2) } = () (* Lemme 5: le lemme original spécifie que la longueur du suffixe est * inférieure ou égale à 1/(1-taux_b). Il s'avère que cette longueur * peut (doit) être majorée par (taux_b / 1 - taux_b). *) let lemma iq2_l5 (nb_b : int) (tx_b : Taux.t) (s : seq_voeu) (i : int) requires { [@expl:iq2/l5 - tx_b contraignant s(..l) imp s(l) boursier] iqx_2 nb_b tx_b s } requires { [@expl:iq2/l5 - 0 <= i < |s|] 0 <= i <= length s } requires { [@expl:iq2/l5 - tx_b non contraignant s(..i)] i > 0 -> not taux_b_contraignant tx_b s[..i-1] nb_b } requires { [@expl:iq2/l5 - tx_b contraignant apres i] forall l. i <= l <= length s -> taux_b_contraignant tx_b s[..l] nb_b} ensures { (length s[i..]) * (100 - tx_b) <= tx_b } = if i = length s then return; if not remains_boursiers s[..i+1] nb_b then begin assert { forall l. i < l < length s -> (not remains_boursiers s[..l] nb_b /\ est_boursier s[l]) }; absurd; end else begin let s' = s[i..] in assert { forall l. i <= l < length s -> est_boursier s[l] }; assert { forall k. 0 <= k < length s' -> est_boursier s'[k] }; assert { nb_boursiers s[i..] = length s' = length s - i }; assert { length s[i..] = nb_boursiers s[i+1..] + 1 = length s - i }; assert { taux_b_contraignant tx_b s[..length s] nb_b }; assert { nb_boursiers s = nb_boursiers s[..i] + nb_boursiers s[i..] }; assert { nb_boursiers s = nb_boursiers s[..i] + length s[i..] }; assert { 100 * nb_boursiers s[..i] + 100 * length s[i..] < tx_b * (1+length s) }; if i = 0 then begin assert { est_boursier s[i] }; end else begin iq1_l2b_b nb_b tx_b s[..i-1] s[i-1] ; assert { seq_respecte_taux_b tx_b s[..i] \/ not remains_boursiers s[..i] nb_b }; end; assert { seq_respecte_taux_b tx_b s[..i] }; assert { tx_b * i <= 100 * nb_boursiers s[..i] }; assert { tx_b * i + 100 * length s[i..] < tx_b *(1+length s) }; assert { length s[i..] *(100 - tx_b) <= tx_b }; end (* |s| <= 1+ (1/(1-tx_b)) d'où * soit |s| <= (200 - tx_b)/(100 - tx_b) * d'où |s| * (100 - tx_b) <= 200 - tx_b *) let lemma iq2_l6 (s : seq_voeu) (taux_b taux_ds : taux) (i : int) requires {[@expl:nb du secteur s >= 1] (* exists i.*) 0 <= i < length s && est_du_secteur s[i] } requires {[@expl:length s <= 1+1/1-taux_b)] (length s) * (100 - taux_b) <= 200 - taux_b } ensures { seq_respecte_taux_ds_minore taux_b taux_ds s } = (*let i = any (i : int) ensures { 0 <= i < length s && est_du_secteur s[i] } in*) assert { s[i..] = cons s[i] s[i+1..] }; assert { nb_du_secteur s[i..] >= 1 }; assert { 1 <= nb_du_secteur s[..i]+ nb_du_secteur s[i..] } let lemma nb_s_pos_imp_witness (s : seq_voeu) requires { nb_du_secteur s >= 1 } ensures { exists i. 0 <= i < length s && est_du_secteur s[i] } = () let lemma iq2_snoc_aux_1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) requires { 0 <= i < length s } requires { remains_du_secteur s[..i] nb_ds } requires { not taux_ds_contraignant tx_ds s[..i] nb_ds } ensures { iq2_loc nb_b nb_ds tx_b tx_ds s i } = iq1_l2b_ds nb_ds tx_ds s[..i] s[i]; assert { seq_respecte_taux_ds tx_ds s[..i+1] } let lemma iq2_snoc_case_1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) requires { [@expl:1 - i = |s|-1] i = length s - 1 } requires { [@expl:1 - |s| > 0] length s >= 1 } requires { [@expl:1 - iq2 oak] forall j. 0 <= j < i -> iq2_loc nb_b nb_ds tx_b tx_ds s j } requires { [@expl:1 - remains ds s(..i)] remains_du_secteur s[..i] nb_ds } requires { [@expl:1 - not conflitct s(..i)] not conflit_taux s[..i] tx_b nb_b tx_ds nb_ds } requires { [@expl:1 - tx_ds non contraignant s(..i)] not taux_ds_contraignant tx_ds s[..i] nb_ds } ensures { iq2_loc nb_b nb_ds tx_b tx_ds s (length s - 1) } = iq2_snoc_aux_1 nb_b nb_ds tx_b tx_ds s i let lemma iq2_snoc_case_2_1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) requires { [@expl:2.1 - iqx_2 (oak.x)] iqx_2 nb_b tx_b s } requires { [@expl:2.1 -iq2 oak] forall j. 0 <= j < i -> iq2_loc nb_b nb_ds tx_b tx_ds s j } requires { i = length s - 1 && length s > 1 } requires { [@expl:2.1 - tx_b non contraignant] not taux_b_contraignant tx_b s[..i] nb_b } requires { [@expl:2.1 - x du secteur] est_du_secteur s[i] } requires { [@expl:2.1 - remains ds s(..i)] remains_du_secteur s[..i] nb_ds } requires { [@expl:2.1 - no conflict s(..i)] not conflit_taux s[..i] tx_b nb_b tx_ds nb_ds } requires { [@expl:2.1 - tx_ds contraignant s(..i)] taux_ds_contraignant tx_ds s[..i] nb_ds } requires { [@expl:2.1 - no conflict s(..i-1)] not conflit_taux s[..i-1] tx_b nb_b tx_ds nb_ds } ensures { iq2_loc nb_b nb_ds tx_b tx_ds s i } = begin remains_du_secteur_prefix_loc s[..i] nb_ds i; assert { [@expl:2.1 - remains ds s(..i-1)] remains_du_secteur s[..i-1] nb_ds }; assert { [@expl:2.1 - iq2(..i-1) expanded] remains_du_secteur s[..i-1] nb_ds -> not conflit_taux s[..i-1] tx_b nb_b tx_ds nb_ds -> seq_respecte_taux_ds_minore tx_b tx_ds s[..i] }; assert { [@expl:2.1 - iq2(..i-1) ACCEL] iq2_loc nb_b nb_ds tx_b tx_ds s[..i] (i-1) }; assert { [@expl:2.1 - tx ds minore respecte (..i)] seq_respecte_taux_ds_minore tx_b tx_ds s[..i] }; assert { [@expl:2.1 - iq2(i)] iq2_loc nb_b nb_ds tx_b tx_ds s i }; end let rec lemma iq2_case_2_2_x (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) requires { [@expl:2_2_x - i in (1,|s|)] 0 <= i <= length s } requires { [@expl:2_2_x - tx_b contraignant s(..i)] taux_b_contraignant tx_b s[..i] nb_b } ensures { 0 <= result <= i && (forall k. result <= k <= i -> taux_b_contraignant tx_b s[..k] nb_b) && (result = 0 \/ not taux_b_contraignant tx_b s[..result-1] nb_b) } variant { i } = if i > 0 && taux_b_contraignant tx_b s[..i-1] nb_b then iq2_case_2_2_x nb_b nb_ds tx_b tx_ds s (i-1) else i let lemma iq2_snoc_case_2_2 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) requires { [@expl:2.2 - iqx_2 (oak.x)] iqx_2 nb_b tx_b s } requires { [@expl:2.2 - iq2 oak] forall j. 0 <= j < i -> iq2_loc nb_b nb_ds tx_b tx_ds s j } requires { [@expl:2.2 - i = |s|-1 > 0] i = length s - 1 > 0 } requires { [@expl:2.2 - tx_b non contraignant s(..i)] not taux_b_contraignant tx_b s[..i] nb_b } requires { [@expl:2.2 - tx_ds contraignant s(..i)] taux_ds_contraignant tx_ds s[..i] nb_ds } requires { [@expl:2.2 - s(i) du secteur] est_du_secteur s[i] } requires { [@expl:2.2 - remains ds s(..i)] remains_du_secteur s[..i] nb_ds } requires { [@expl:2.2 - no conflict s(..i)] not conflit_taux s[..i] tx_b nb_b tx_ds nb_ds } requires { [@expl:2.2 - conflit s(..i-1)] conflit_taux s[..i-1] tx_b nb_b tx_ds nb_ds } ensures { iq2_loc nb_b nb_ds tx_b tx_ds s i } = let taux_b = tx_b in let taux_ds = tx_ds in begin assert { [@expl:2.2 - tx_b contraignant s(..i-1)] taux_b_contraignant tx_b s[..i-1] nb_b }; let x = iq2_case_2_2_x nb_b nb_ds tx_b tx_ds s (i-1) in if x < i-1 then iq2_l5 nb_b tx_b s[..i-1] x else assert { x = i -1 && length s[x..i-1] = 0 }; assert { [@expl:|s(x..i-1)| < 1/(1-taux_b)] (length s[x..i-1]) *(100 - taux_b) <= taux_b }; seq_cat_dec s x i (i+1); iq2_l6 s[x..i+1] taux_b taux_ds (i-x); assert { [@expl:s(x..i+1) respecte tx min] seq_respecte_taux_ds_minore taux_b taux_ds s[x..i+1] }; assert { [@expl:iq2 s(..x-1)] iq2_loc nb_b nb_ds tx_b tx_ds s (x-1) }; assert { [@expl:s(..x) respecte tx min] seq_respecte_taux_ds_minore taux_b taux_ds s[..x] }; iq2_l4 s[..x] s[x..i+1] taux_b taux_ds; assert { [@expl:s(..i+1) respecte tx min] seq_respecte_taux_ds_minore taux_b taux_ds s[..i+1] }; assert { [@expl:iq2 s(..i)] iq2_loc nb_b nb_ds tx_b tx_ds s i }; end let lemma iq2_snoc_case_2 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) requires { [@expl:iqx_2 (oak.x)] iqx_2 nb_b tx_b s } requires { [@expl:iq2 oak] forall j. 0 <= j < i -> iq2_loc nb_b nb_ds tx_b tx_ds s j } requires { [@expl: |s| > 1 && i = |s|] i = length s - 1 && length s > 1 } requires { [@expl:2 - tx_b non contraignant] not taux_b_contraignant tx_b s[..i] nb_b } requires { [@expl:2 - x du secteur] est_du_secteur s[i] } requires { remains_du_secteur s[..i] nb_ds } requires { not conflit_taux s[..i] tx_b nb_b tx_ds nb_ds } requires { taux_ds_contraignant tx_ds s[..i] nb_ds } ensures { iq2_loc nb_b nb_ds tx_b tx_ds s i } = begin if not conflit_taux s[..i-1] tx_b nb_b tx_ds nb_ds then iq2_snoc_case_2_1 nb_b nb_ds tx_b tx_ds s i else iq2_snoc_case_2_2 nb_b nb_ds tx_b tx_ds s i end use set.Fset use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.PQueueVoeuxClasses as PQueue use proofs.ordre_appel.eligibles.ValidEligibles use proofs.ordre_appel.eligibles.Eligibles use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap let lemma iq2_snoc_singleton (cB cR : bool) (nb_b nb_ds : int) (tx_b tx_ds : 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:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b } requires {[@expl:cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_ds oak nb_ds } requires {[@expl:iqx_2 (oak.x)] iqx_2 nb_b tx_b (snoc oak x) } requires {[@expl:iq2 oak] iq2 nb_b nb_ds tx_b tx_ds oak } requires { 0 <= nb_b && 0 <= nb_ds && length oak = 0 } ensures { iq2 nb_b nb_ds tx_b tx_ds (snoc oak x) } = let s = snoc oak x in if remains_du_secteur oak nb_ds && not conflit_taux oak tx_b nb_b tx_ds nb_ds then begin assert { 0 < nb_ds }; if taux_ds_contraignant tx_ds oak nb_ds then begin if not est_du_secteur x then begin assert { not Fset.is_empty eligibles }; assert { est_eligible_p cB cR x }; assert { est_du_secteur x }; absurd; end end else assert { tx_ds = 0 }; end; assert { iq2_loc nb_b nb_ds tx_b tx_ds s 0 } end module IQ2_Snoc use seq.Seq use int.Int use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts use proofs.lib.seq.Seq use proofs.ordre_appel.eligibles.ValidEligibles use proofs.ordre_appel.eligibles.Eligibles 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_Snoc use proofs.ordre_appel.invariants.iq1.IQ1_Lemmas use IQ2_Lemmas use export IQ2 let lemma iq2_snoc (cB cR : bool) (nb_b nb_ds : int) (tx_b tx_ds : 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:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b } requires {[@expl:cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_ds oak nb_ds } requires {[@expl:iqx_2 (oak.x)] iqx_2 nb_b tx_b (snoc oak x) } requires {[@expl:iq2 oak] iq2 nb_b nb_ds tx_b tx_ds oak } requires {[@expl:(nb_boursiers g) >=0] 0 <= nb_b } requires {[@expl:nb_ds >=0] 0 <= nb_ds } ensures { iq2 nb_b nb_ds tx_b tx_ds (snoc oak x) } = let s = snoc oak x in if length s = 1 then begin iq2_snoc_singleton cB cR nb_b nb_ds tx_b tx_ds oak om m eligibles x; return ; end; for i = 0 to length s - 1 do invariant { forall j. 0 <= j < i -> iq2_loc nb_b nb_ds tx_b tx_ds s j } if i < length s - 1 then begin assert { s[..i] == oak[..i] }; assert { iq2_loc nb_b nb_ds tx_b tx_ds oak i }; assert { iq2_loc nb_b nb_ds tx_b tx_ds s i }; continue; end; if not remains_du_secteur s[..i] nb_ds then continue; if conflit_taux s[..i] tx_b nb_b tx_ds nb_ds then continue; if not taux_ds_contraignant tx_ds s[..i] nb_ds then begin iq2_snoc_case_1 nb_b nb_ds tx_b tx_ds s i; end else begin assert { [@expl:2 - eligibles not empty] not PQueue.is_empty eligibles }; assert { [@expl:2 - tx_b non contraignant] not taux_b_contraignant tx_b s[..i] nb_b }; assert { [@expl:2 - x eligible] not cB /\ cR /\ est_eligible_p cB cR s[i] }; assert { [@expl:2 - so x du secteur] est_du_secteur s[i] }; iq2_snoc_case_2 nb_b nb_ds tx_b tx_ds s i; end done end (* generated on Thu Nov 21 02:04:27 UTC 2024 from rev: *)
Generated by why3doc 1.7.2+git