Parcoursup / Calcul de l'ordre d'appel des candidats index
module Q4_2 use int.Int use seq.Seq use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use fr.parcoursup.whyml.ordreappel.algo.taux.Taux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
Q4.2 * * a) Un candidat non-resident boursier qui a le rang r dans le classement * pedagogique ne peut être double que par des residents, boursiers ou non,
predicate q4_2a_loc (oa: seq_voeu) (k : int) = est_boursier_hors_secteur oa[k] -> forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> est_du_secteur oa[i] predicate q4_2a (oa: seq_voeu) = forall k. 0 <= k < length oa -> q4_2a_loc oa k predicate q4_2a_aux_loc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (k : int) = est_boursier_hors_secteur oa[k] -> forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> (est_du_secteur oa[i] && in_Zr nb_ds tx_ds oa i) predicate q4_2a_aux (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q4_2a_aux_loc nb_ds tx_ds oa k predicate q4_2b_loc (tx_ds : Taux.t) (oa : seq_voeu) (k : int) = est_boursier_hors_secteur oa[k] -> 0 <= (100 - tx_ds) * k <= 100 * (get_rang oa[k])
* b) et a un rang dans l'ordre d'appel k inférieur ou egal à * 1 + floor((1 + tx_ds/(1-tx_ds))*r)
predicate q4_2b (tx_ds : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q4_2b_loc tx_ds oa k predicate q4_2b_aux_loc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (k : int) = est_boursier_hors_secteur oa[k] -> let nbCb = nb_contraintes_taux_ds nb_ds tx_ds oa[..k] in k <= (get_rang oa[k]) - 1 + nbCb predicate q4_2b_aux (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q4_2b_aux_loc nb_ds tx_ds oa k predicate q4_2 (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) = q4_2a_aux nb_ds tx_ds oa && q4_2a oa && q4_2b_aux nb_ds tx_ds oa && q4_2b tx_ds oa let lemma q4_2a_aux_imp_q4_2a (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) requires { q4_2a_aux nb_ds tx_ds oa } ensures { q4_2a oa } = assert { forall k. 0 <= k < length oa -> q4_2a_aux_loc nb_ds tx_ds oa k -> q4_2a_loc oa k } end module Q4_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 proofs.ordre_appel.invariants.iq4_1.IQ4_1 use export Q4_2 let lemma q4_2_up_to_rang_appel_oa (nb_ds : int) (tx_ds : Taux.t) (oa1 oa2 : seq_voeu) requires { q4_2 nb_ds tx_ds oa1 } requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 } ensures { q4_2 nb_ds tx_ds oa2 } = for i = 0 to length oa2 - 1 do invariant { [@expl:q4_2a_aux_loc] forall k. 0 <= k < i -> q4_2a_aux_loc nb_ds tx_ds oa2 k } invariant { [@expl:q4_2a_loc] forall k. 0 <= k < i -> q4_2a_loc oa2 k } invariant { [@expl:q4_2b_aux_loc] forall k. 0 <= k < i -> q4_2b_aux_loc nb_ds tx_ds oa2 k } invariant { [@expl:q4_2b_loc] forall k. 0 <= k < i -> q4_2b_loc tx_ds oa2 k } if not est_boursier_hors_secteur oa2[i] then continue; assert { q4_2a_aux_loc nb_ds tx_ds oa1 i }; assert { q4_2a_loc oa1 i }; assert { q4_2b_aux_loc nb_ds tx_ds oa1 i }; assert { q4_2b_loc tx_ds oa1 i }; assert { est_boursier_hors_secteur 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 -> voeu_lt oa2[i] oa2[k] -> in_Zr nb_ds tx_ds oa2 k }; assert { nb_contraintes_taux_ds nb_ds tx_ds oa1[..i] = nb_contraintes_taux_ds nb_ds tx_ds oa2[..i] } done end module Q4_2a_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 Q4_2 use fr.parcoursup.whyml.ordreappel.algo.taux.Taux 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 q4_2a_snoc1 (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (x : voeu) requires { q4_2a_aux nb_ds tx_ds oa } requires { est_boursier_hors_secteur x -> (forall i. 0 <= i < length oa -> voeu_lt x oa[i] -> in_Zr nb_ds tx_ds oa i) } ensures { q4_2a_aux nb_ds 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 -> q4_2a_aux_loc nb_ds tx_ds s i } if k < length s - 1 then begin assert { q4_2a_aux_loc nb_ds tx_ds oa k }; assert { q4_2a_aux_loc nb_ds tx_ds s k } end done let lemma q4_2a_snoc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { iq4_1 nb_ds tx_ds (snoc oa x) m } requires { q4_2a_aux nb_ds tx_ds oa } ensures { q4_2a_aux nb_ds 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 -> q4_2a_aux_loc nb_ds tx_ds s i } if k < length s - 1 then begin assert { q4_2a_aux_loc nb_ds tx_ds oa k }; assert { forall i. 0 <= i < k -> s[i] = oa[i] }; assert { s[..k] = oa[..k] }; assert { q4_2a_aux_loc nb_ds tx_ds s k } end else if est_boursier_hors_secteur x then begin assert { forall i. 0 <= i < k -> s[i+1..] == snoc oa[i+1..] x }; assert { est_boursier_hors_secteur s[k] }; assert { iq4_1b_loc nb_ds tx_ds s m k }; assert { forall i. 0 <= i < k -> not in_Zr nb_ds tx_ds s i -> seq_contains s[k] s[i+1..] -> est_boursier s[k] -> 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_Zr nb_ds tx_ds s i -> s[i] <> s[k] -> voeu_lt s[i] s[k] }; assert { forall i. 0 <= i < k -> voeu_lt s[k] s[i] -> in_Zr nb_ds tx_ds s i }; assert { q4_2a_aux_loc nb_ds tx_ds s k } end done end module Q4_2b_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 Q4_2 use fr.parcoursup.whyml.ordreappel.algo.taux.Taux 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 q4_2b_aux_snoc (nb_ds : int) (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_1 nb_ds tx_ds (snoc oa x) m } requires { q4_2a_aux nb_ds tx_ds (snoc oa x) } requires { q4_2b_aux nb_ds tx_ds oa } ensures { q4_2b_aux nb_ds 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 -> q4_2b_aux_loc nb_ds tx_ds s i } if not est_boursier_hors_secteur s[k] then continue; let nbCr_k = nb_contraintes_taux_ds nb_ds tx_ds s[..k] in if k < length s -1 then begin assert { q4_2b_aux_loc nb_ds tx_ds oa k }; assert { q4_2b_aux_loc nb_ds tx_ds s k }; end else begin let lt = ref Seq.empty in let gt = ref Seq.empty in assert { q4_2a_aux_loc nb_ds 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 !gt <= nb_contraintes_taux_ds nb_ds tx_ds s[..i] <= nbCr_k } invariant { length !lt + length !gt = 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 -> 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 { q4_2a_aux_loc nb_ds tx_ds s k }; assert { in_Zr nb_ds tx_ds s i }; seq_prefix_snoc s i; gt := snoc !gt s[i]; end; done; assert { k = length !lt + length !gt <= s[k].rang - 1 + nbCr_k }; end; done let lemma q4_2b_snoc (nb_ds : int) (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_1 nb_ds tx_ds (snoc oa x) m } requires { q4_2a_aux nb_ds tx_ds (snoc oa x) } requires { q4_2b_aux nb_ds tx_ds oa } ensures { q4_2b tx_ds (snoc oa x) } = let s = snoc oa x in let taux_r = tx_ds in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q4_2b_loc taux_r s i } assert { iq4_1a_loc nb_ds tx_ds s k }; if est_boursier_hors_secteur s[k] then begin let nbCb = nb_contraintes_taux_ds nb_ds taux_r s[..k] in q4_2b_aux_snoc nb_ds tx_ds oa m x ; assert { 100 * nbCb <= taux_r * k + 100 }; assert { q4_2b_aux_loc nb_ds tx_ds s k }; assert { k <= s[k].rang - 1 + nbCb }; assert { 100*(k + 1 - nbCb) <= 100 * s[k].rang }; assert { 0 <= (100 - taux_r) * k <= 100 * s[k].rang }; end done end module Q4_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.SeqVoeuxDistincts use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use Q4_2a_Lemmas use Q4_2b_Lemmas use export Q4_2 let lemma q4_2_snoc (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { [@expl:pre q4_2 / rangs >= 1] 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang } requires { [@expl:pre q4_2 / alld(oa.x)] all_distincts (snoc oa x) } requires { [@expl:pre q4_2 / iq4_2 (oa.x)] iq4_1 nb_ds tx_ds (snoc oa x) m } requires { [@expl:pre q4_2 / q4_1 oa] q4_2 nb_ds tx_ds oa } ensures { q4_2 nb_ds tx_ds (snoc oa x) } = q4_2a_snoc nb_ds tx_ds oa m x; q4_2b_snoc nb_ds tx_ds oa m x let lemma q4_2_empty (nb_ds : int) (tx_ds : Taux.t) (oa : seq_voeu) requires { oa = Seq.empty } ensures { q4_2 nb_ds tx_ds oa } = () end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git