Parcoursup / Calcul de l'ordre d'appel des candidats index
module Q4_1 use int.Int use seq.Seq use proofs.ordre_appel.invariants.iq4_2.IQ4_2 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.1 * * a) Un candidat resident non-boursier qui a le rang r dans le classement * pedagogique ne peut être double que par des boursiers, residents ou non,
predicate q4_1a_loc (oa: seq_voeu) (k : int) = est_non_boursier_du_secteur oa[k] -> forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> est_boursier oa[i] predicate q4_1a (oa: seq_voeu) = forall k. 0 <= k < Seq.length oa -> q4_1a_loc oa k predicate q4_1a_aux_loc (nb_b : int) (tx_b : Taux.t) (oa: seq_voeu) (k : int) = est_non_boursier_du_secteur oa[k] -> forall i. 0 <= i < k -> voeu_lt oa[k] oa[i] -> (est_boursier oa[i] && in_Zb nb_b tx_b oa i) predicate q4_1a_aux (nb_b : int) (tx_b : Taux.t) (oa: seq_voeu) = forall k. 0 <= k < length oa -> q4_1a_aux_loc nb_b tx_b oa k
* b) et a un rang dans l'ordre d'appel k inférieur ou egal à * 1 + floor((1 + tx_b/(1-tx_b))*r)
predicate q4_1b_loc (taux_b : Taux.t) (oa: seq_voeu) (k : int) = est_non_boursier_du_secteur oa[k] -> 0 <= (100 - taux_b) * k <= 100 * (get_rang oa[k]) predicate q4_1b (tx_b : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < length oa -> q4_1b_loc tx_b oa k predicate q4_1b_aux_loc (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (k : int) = est_non_boursier_du_secteur oa[k] -> let nbCb = nb_contraintes_taux_b nb_b tx_b oa[..k] in k <= (get_rang oa[k]) - 1 + nbCb predicate q4_1b_aux (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) = forall k. 0 <= k < Seq.length oa -> q4_1b_aux_loc nb_b tx_b oa k predicate q4_1 (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) = q4_1a_aux nb_b tx_b oa && q4_1a oa && q4_1b_aux nb_b tx_b oa && q4_1b tx_b oa let lemma q4_1a_aux_imp_q4_1a (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) requires { q4_1a_aux nb_b tx_b oa } ensures { q4_1a oa } = assert { forall k. 0 <= k < length oa -> q4_1a_aux_loc nb_b tx_b oa k -> q4_1a_loc oa k } end module Q4_1_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_2.IQ4_2 use export Q4_1 let lemma q4_1_up_to_rang_appel_oa (nb_b : int) (tx_b : Taux.t) (oa1 oa2 : seq_voeu) requires { q4_1 nb_b tx_b oa1 } requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 } ensures { q4_1 nb_b tx_b oa2 } = for i = 0 to length oa2 - 1 do invariant { [@expl:q4_1a_aux_loc] forall k. 0 <= k < i -> q4_1a_aux_loc nb_b tx_b oa2 k } invariant { [@expl:q4_1a_loc] forall k. 0 <= k < i -> q4_1a_loc oa2 k } invariant { [@expl:q4_1b_aux_loc] forall k. 0 <= k < i -> q4_1b_aux_loc nb_b tx_b oa2 k } invariant { [@expl:q4_1b_loc] forall k. 0 <= k < i -> q4_1b_loc tx_b oa2 k } if not est_non_boursier_du_secteur oa2[i] then continue; assert { q4_1a_aux_loc nb_b tx_b oa1 i }; assert { q4_1a_loc oa1 i }; assert { q4_1b_aux_loc nb_b tx_b oa1 i }; assert { q4_1b_loc tx_b oa1 i }; assert { est_non_boursier_du_secteur oa1[i] }; 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 }; assert { nb_contraintes_taux_b nb_b tx_b oa1[..i] = nb_contraintes_taux_b nb_b tx_b oa2[..i] } done end module Q4_1a_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_2.IQ4_2 use Q4_1 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_1a_snoc1 (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (x : voeu) requires { q4_1a_aux nb_b tx_b oa } requires { est_non_boursier_du_secteur x -> forall i. 0 <= i < length oa -> voeu_lt x oa[i] -> in_Zb nb_b tx_b oa i } ensures { q4_1a_aux nb_b tx_b (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q4_1a_aux_loc nb_b tx_b s i } if k < length s - 1 then begin assert { q4_1a_aux_loc nb_b tx_b oa k }; assert { q4_1a_aux_loc nb_b tx_b s k } end done let lemma q4_1a_snoc (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { iq4_2 nb_b tx_b (snoc oa x) m } requires { q4_1a_aux nb_b tx_b oa } ensures { q4_1a_aux nb_b tx_b (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q4_1a_aux_loc nb_b tx_b s i } if k < length s - 1 then begin assert { q4_1a_aux_loc nb_b tx_b oa k }; assert { forall i. 0 <= i < k -> s[i] = oa[i] }; assert { s[..k] == oa[..k] }; assert { q4_1a_aux_loc nb_b tx_b s k } end else if est_non_boursier_du_secteur x then begin assert { forall i. 0 <= i < k -> s[i+1..] == snoc oa[i+1..] x }; assert { est_non_boursier_du_secteur s[k] }; assert { iq4_2b_loc nb_b tx_b s m k }; assert { forall i. 0 <= i < k -> not in_Zb nb_b tx_b s i -> seq_contains s[k] s[i+1..] -> est_du_secteur 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_Zb nb_b tx_b 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_Zb nb_b tx_b s i }; assert { q4_1a_aux_loc nb_b tx_b s k } end done end module Q4_1b_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_2.IQ4_2 use Q4_1 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_1b_aux_snoc (nb_b : int) (tx_b : 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_2 nb_b tx_b (snoc oa x) m } requires { q4_1a_aux nb_b tx_b (snoc oa x) } requires { q4_1b_aux nb_b tx_b oa } ensures { q4_1b_aux nb_b tx_b (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q4_1b_aux_loc nb_b tx_b s i } if not est_non_boursier_du_secteur s[k] then continue; let nbCb_k = nb_contraintes_taux_b nb_b tx_b s[..k] in if k < length s -1 then begin assert { q4_1b_aux_loc nb_b tx_b oa k }; assert { q4_1b_aux_loc nb_b tx_b s k }; end else begin let lt = ref Seq.empty in let gt = ref Seq.empty in assert { q4_1a_aux_loc nb_b tx_b 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_b nb_b tx_b s[..i] <= nbCb_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 i j. 0 <= i < j < length !lt -> voeu_distinct !lt[i] !lt[j] };*) 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 (get_rang s[k] - 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_1a_aux_loc nb_b tx_b s k }; assert { in_Zb nb_b tx_b s i }; seq_prefix_snoc s i; gt := snoc !gt s[i]; end; done; assert { k = length !lt + length !gt <= s[k].rang - 1 + nbCb_k }; end; done let lemma q4_1b_snoc (nb_b : int) (tx_b : 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_2 nb_b tx_b (snoc oa x) m } requires { q4_1a_aux nb_b tx_b (snoc oa x) } requires { q4_1b_aux nb_b tx_b oa } ensures { q4_1b tx_b (snoc oa x) } = let s = snoc oa x in for k = 0 to length s - 1 do invariant { forall i. 0 <= i < k -> q4_1b_loc tx_b s i } assert { iq4_2a_loc nb_b tx_b s k }; if est_non_boursier_du_secteur s[k] then begin let nbCb = nb_contraintes_taux_b nb_b tx_b s[..k] in q4_1b_aux_snoc nb_b tx_b oa m x ; assert { 100 * nbCb <= tx_b * k + 100 }; assert { q4_1b_aux_loc nb_b tx_b s k }; assert { k <= s[k].rang - 1 + nbCb }; assert { 100*(k + 1 - nbCb) <= 100 * s[k].rang }; assert { 0 <= (100 - tx_b) * k <= 100 * s[k].rang }; end done end module Q4_1_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_2.IQ4_2 use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use Q4_1a_Lemmas use Q4_1b_Lemmas use export Q4_1 let lemma q4_1_snoc (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (x :voeu) requires { [@expl:pre q4_1 / rangs >= 1] 1 <= x.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang } requires { [@expl:pre q4_1 / alld(oa.x)] all_distincts (snoc oa x) } requires { [@expl:pre q4_1 / iq4_2 (oa.x)] iq4_2 nb_b tx_b (snoc oa x) m } requires { [@expl:pre q4_1 / q4_1 oa] q4_1 nb_b tx_b oa } ensures { [@expl:q4_1(oa.x)] q4_1 nb_b tx_b (snoc oa x) } = q4_1a_snoc nb_b tx_b oa m x; q4_1a_aux_imp_q4_1a nb_b tx_b (snoc oa x); q4_1b_aux_snoc nb_b tx_b oa m x; q4_1b_snoc nb_b tx_b oa m x let lemma q4_1_empty (nb_b : int) (tx_b : Taux.t) (oa : seq_voeu) requires { oa = Seq.empty } ensures { q4_1 nb_b tx_b oa } = () end (* generated on Thu Nov 21 02:04:27 UTC 2024 from rev: *)
Generated by why3doc 1.7.2+git