Parcoursup / Calcul de l'ordre d'appel des candidats index
module Q5 use seq.Seq use int.Int use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.invariants.iq4_3.IQ4_3 use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse predicate q5a_loc (oa: seq_voeu) (k : int) = est_non_boursier_hors_secteur oa[k] -> forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> est_boursier oa[i] \/ est_du_secteur oa[i]
Q5 * * a) Un candidat non-boursier non-resident boursier qui a le rang r dans * le classement pedagogique ne double jamais personne
predicate q5a (oa: seq_voeu) = forall k. 0 <= k < length oa -> q5a_loc oa k predicate q5a_aux_loc (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (k : int) = est_non_boursier_hors_secteur oa[k] -> forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> (in_Zb nb_b tx_b oa i \/ in_Zr nb_r tx_r oa i) predicate q5a_aux (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q5a_aux_loc nb_b nb_r tx_b tx_r oa k
* * b) et a un rang dans l'ordre d'appel k inférieur ou egal à * 1 + ceiling((1 + (tx_b+tx_ds)/(1-(tx_b+tx_ds)))*(r+1))
predicate q5b_loc (taux_b taux_ds : Taux.t) (oa : seq_voeu) (k : int) = taux_b + taux_ds < 100 -> est_non_boursier_hors_secteur oa[k] -> 0 <= (100 - (taux_b + taux_ds)) * k <= 100 * (get_rang oa[k]) + 100 predicate q5b (tx_b tx_r : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q5b_loc tx_b tx_r oa k predicate q5b_aux_loc (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (k : int) = est_non_boursier_hors_secteur oa[k] -> let nbCb = nb_contraintes_taux_b nb_b tx_b oa[..k] in let nbCds = nb_contraintes_taux_ds nb_r tx_r oa[..k] in k <= (get_rang oa[k]) - 1 + nbCb + nbCds predicate q5b_aux (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q5b_aux_loc nb_b nb_r tx_b tx_r oa k predicate q5 (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) = q5a_aux nb_b nb_r tx_b tx_r oa && q5a oa && q5b_aux nb_b nb_r tx_b tx_r oa && q5b tx_b tx_r oa let lemma q5a_aux_imp_q5a (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) requires { q5a_aux nb_b nb_r tx_b tx_r oa } ensures { q5a oa } = assert { forall k. 0 <= k < length oa -> q5a_aux_loc nb_b nb_r tx_b tx_r oa k -> q5a_loc oa k } end module Q5_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 proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.invariants.iq4_3.IQ4_3 use export Q5 let lemma q5_up_to_rang_appel_oa (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa1 oa2 : seq_voeu) requires { q5 nb_b nb_ds tx_b tx_ds oa1 } requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 } ensures { q5 nb_b nb_ds tx_b tx_ds oa2 } = for i = 0 to length oa2 - 1 do invariant { [@expl:q5a_aux_loc] forall k. 0 <= k < i -> q5a_aux_loc nb_b nb_ds tx_b tx_ds oa2 k } invariant { [@expl:q5a_loc] forall k. 0 <= k < i -> q5a_loc oa2 k } invariant { [@expl:q5b_aux_loc] forall k. 0 <= k < i -> q5b_aux_loc nb_b nb_ds tx_b tx_ds oa2 k } invariant { [@expl:q5b_loc] forall k. 0 <= k < i -> q5b_loc tx_b tx_ds oa2 k } if not est_non_boursier_hors_secteur oa2[i] then continue; assert { est_non_boursier_hors_secteur oa1[i] }; assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds oa1 i }; assert { q5a_loc oa1 i }; assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds oa1 i }; assert { q5b_loc tx_b tx_ds oa1 i }; assert { forall k. 0 <= k < i -> in_Zr nb_ds tx_ds oa1 k = in_Zr nb_ds tx_ds oa2 k }; assert { forall k. 0 <= k < i -> in_Zb nb_b tx_b oa1 k = in_Zb nb_b tx_b oa2 k }; assert { forall k. 0 <= k < i -> voeu_lt oa2[i] oa2[k] -> (in_Zb nb_b tx_b oa2 k \/ in_Zr nb_ds tx_ds oa2 k) }; assert { nb_contraintes_taux_ds nb_b tx_b oa1[..i] = nb_contraintes_taux_ds nb_b tx_b oa2[..i] }; assert { nb_contraintes_taux_ds nb_ds tx_ds oa1[..i] = nb_contraintes_taux_ds nb_ds tx_ds oa2[..i] } done end module Q5a_Lemmas use int.Int use seq.Seq use proofs.lib.seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.invariants.iq4_3.IQ4_3 use Q5 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 let lemma q5a_snoc1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (x : voeu) requires { q5a_aux nb_b nb_ds tx_b tx_ds oa } requires { est_non_boursier_hors_secteur x -> forall i. 0 <= i < length oa -> voeu_lt x oa[i] -> in_some_Z nb_b nb_ds tx_b tx_ds oa i } ensures { q5a_aux nb_b nb_ds tx_b tx_ds (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q5a_aux_loc nb_b nb_ds tx_b tx_ds s i } if k < length s - 1 then begin assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds oa k }; assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k } end else begin if est_non_boursier_hors_secteur x then begin assert { forall i. 0 <= i < length s -> voeu_lt x s[i] -> in_some_Z nb_b nb_ds tx_b tx_ds s i }; assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k } end end done let lemma q5a_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m } requires { q5a_aux nb_b nb_ds tx_b tx_ds oa } ensures { q5a_aux nb_b nb_ds tx_b tx_ds (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q5a_aux_loc nb_b nb_ds tx_b tx_ds s i } if k < length s - 1 then begin assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds oa k }; assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k } end else if est_non_boursier_hors_secteur x then begin assert { forall i. 0 <= i < k -> s[i+1..] == snoc oa[i+1..] x }; assert { est_non_boursier_hors_secteur s[k] }; assert { iq4_3b_loc nb_b nb_ds tx_b tx_ds s m k }; assert { forall i. 0 <= i <= k -> not in_some_Z nb_b nb_ds tx_b tx_ds s i -> seq_contains s[k] s[i+1..] -> s[k] <> s[i] -> voeu_lt s[i] s[k] }; seq_contains_suffix_snoc s[k] oa s; assert { forall i. 0 <= i < k -> not in_some_Z nb_b nb_ds tx_b tx_ds oa i -> s[k] <> s[i] -> voeu_lt s[i] s[k] }; assert { forall i. 0 <= i < k -> voeu_lt s[k] s[i] -> in_some_Z nb_b nb_ds tx_b tx_ds oa i }; assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k } end done end module Q5b_Lemmas use int.Int use seq.Seq use mach.java.lang.Integer use proofs.lib.seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.invariants.iq4_3.IQ4_3 use Q5 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 ref.Ref use pigeon.Pigeonhole function pigeon_map (s : seq_voeu) (x : voeu) (i : int) : int = x.rang -1 - s[i].rang let lemma q5b_aux_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang } requires { all_distincts (snoc oa x) } requires { iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m } requires { q5a_aux nb_b nb_ds tx_b tx_ds (snoc oa x) } requires { q5b_aux nb_b nb_ds tx_b tx_ds oa } ensures { q5b_aux nb_b nb_ds tx_b tx_ds oa } ensures { q5b_aux nb_b nb_ds tx_b tx_ds (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q5b_aux_loc nb_b nb_ds tx_b tx_ds s i } if not est_non_boursier_hors_secteur s[k] then continue; let nbCb_k = nb_contraintes_taux_b nb_b tx_b s[..k] in let nbCds_k = nb_contraintes_taux_ds nb_ds tx_ds s[..k] in if k < length s -1 then begin assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds oa k }; assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds s k }; end else begin let lt = ref Seq.empty in let gtb = ref Seq.empty in let gtds = ref Seq.empty in assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s (k-1) }; for i = 0 to k - 1 do invariant { forall j. 0 <= j < length !lt -> 1 <= !lt[j].rang } invariant { forall j. 0 <= j < length !lt -> voeu_lt !lt[j] s[k] } invariant { length !lt <= s[k].rang - 1 } invariant { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i..] } invariant { forall j. 0 <= j < length !lt -> seq_contains !lt[j] s } invariant { all_distincts !lt } invariant { length !gtb <= nb_contraintes_taux_b nb_b tx_b s[..i] <= nbCb_k } invariant { length !gtds <= nb_contraintes_taux_ds nb_ds tx_ds s[..i] <= nbCds_k } invariant { length !lt + length !gtb + length !gtds = i } if voeu_lt s[i] s[k] then begin seq_suffix_cons s i; assert { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i+1..] }; assert { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i..] }; assert { forall j. 0 <= j < length !lt -> voeu_distinct !lt[j] s[i] } ; lt := snoc !lt s[i]; assert { forall j. 0 <= j < length !lt -> seq_forall (voeu_distinct !lt[j]) s[i+1..] }; assert { forall i j. 0 <= i < j < length !lt -> voeu_distinct !lt[i] !lt[j] }; assert { seq_forall_two voeu_distinct !lt }; assert { all_distincts !lt }; if length !lt > Integer.to_int(s[k].rang - 1) then begin let n = length !lt in let m = Integer.to_int (s[k].rang - 1) in assert { forall j. 0 <= j < length !lt -> 1 <= !lt[j].rang < s[k].rang }; assert { [@expl:pc pigeon hole] forall i. 0 <= i < n -> 0 <= s[k].rang -1 - !lt[i].rang < m }; pigeonhole n m (pigeon_map !lt s[k]); assert { exists i1, i2. 0 <= i1 < i2 < n && pigeon_map !lt s[k] i1 = pigeon_map !lt s[k] i2 so !lt[i1].rang = !lt[i2].rang so not voeu_distinct !lt[i1] !lt[i2] }; absurd; end; end else begin assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s k }; assert { in_Zb nb_b tx_b s i \/ in_Zr nb_ds tx_ds s i }; seq_prefix_snoc s i; if in_Zb nb_b tx_b s i then gtb := snoc !gtb s[i] else gtds := snoc !gtds s[i] end; done; assert { k = length !lt + length !gtb + length !gtds <= s[k].rang - 1 + nbCb_k + nbCds_k }; end; done let lemma q5b_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang } requires { tx_b+tx_ds < 100 } requires { all_distincts (snoc oa x) } requires { iq4_1 nb_ds tx_ds (snoc oa x) m } requires { iq4_2 nb_b tx_b (snoc oa x) m } requires { iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m } requires { q5a_aux nb_b nb_ds tx_b tx_ds (snoc oa x) } requires { q5b_aux nb_b nb_ds tx_b tx_ds oa } ensures { q5b tx_b tx_ds (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q5b_loc tx_b tx_ds s i } assert { iq4_1a_loc nb_ds tx_ds s k }; assert { iq4_2a_loc nb_b tx_b s k }; if est_non_boursier_hors_secteur s[k] then begin let nbCb = nb_contraintes_taux_b nb_b tx_b s[..k] in let nbCds = nb_contraintes_taux_ds nb_ds tx_ds s[..k] in q5b_aux_snoc nb_b nb_ds tx_b tx_ds oa m x; assert { 100 * nbCb <= tx_b * k + 100 }; assert { 100 * nbCds <= tx_ds * k + 100 }; assert { 100 * (nbCb + nbCds) <= tx_b * k + tx_ds * k + 200 }; assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds s k }; assert {[@expl:to prove] k <= s[k].rang - 1 + nbCb + nbCds }; assert { 100*(k + 1 - nbCb - nbCds) <= 100 * s[k].rang }; assert { 0 <= (100 - (tx_b + tx_ds)) * k <= 100 * s[k].rang + 100}; end; done end module Q5_Snoc use int.Int use seq.Seq use mach.java.lang.Integer use proofs.lib.seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.invariants.iq4_3.IQ4_3 use fr.parcoursup.whyml.ordreappel.algo.taux.Taux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use Q5a_Lemmas use Q5b_Lemmas use export Q5 let lemma q5_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { [@expl:pre q5 / rangs >= 1] 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang } requires { [@expl:pre q5 / alld(oa.x)] all_distincts (snoc oa x) } requires { [@expl:pre q5 / iq4_1 (oa.x)] iq4_1 nb_ds tx_ds (snoc oa x) m } requires { [@expl:pre q5 / iq4_2 (oa.x)] iq4_2 nb_b tx_b (snoc oa x) m } requires { [@expl:pre q5 / iq4_3 (oa.x)] iq4_3 nb_b nb_ds tx_b tx_ds (snoc oa x) m } requires { [@expl:pre q5 / q5 oa] q5 nb_b nb_ds tx_b tx_ds oa } ensures { [@expl:q5(oa.x)] q5 nb_b nb_ds tx_b tx_ds (snoc oa x) } = q5a_snoc nb_b nb_ds tx_b tx_ds oa m x; if tx_b.tx + tx_ds.tx < 100 then q5b_snoc nb_b nb_ds tx_b tx_ds oa m x let lemma q5_empty (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa : seq_voeu) requires { oa = Seq.empty } ensures { q5 nb_b nb_ds tx_b tx_ds oa } = () end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git