Parcoursup / Calcul de l'ordre d'appel des candidats index
module Properties use seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.properties.q1.Q1 use proofs.ordre_appel.properties.q2.Q2 use proofs.ordre_appel.properties.q3.Q3 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.properties.q4_1.Q4_1 use proofs.ordre_appel.properties.q4_2.Q4_2 use proofs.ordre_appel.properties.q5.Q5 use proofs.ordre_appel.properties.q6.Q6 use proofs.ordre_appel.properties.p4.P4 use proofs.ordre_appel.properties.p5.P5 use fr.parcoursup.whyml.ordreappel.algo.taux.Taux use fr.parcoursup.whyml.ordreappel.algo.ordre_appel.OrdreAppel predicate ordre_appel_properties (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) = q1 tx_b oa /\ q2 tx_b tx_ds oa /\ q3 oa /\ iq4_2a nb_b tx_b oa /\ q4_1 nb_b tx_b oa /\ q4_2 nb_ds tx_ds oa /\ q5 nb_b nb_ds tx_b tx_ds oa /\ q6 tx_b tx_ds op oa /\ p4 tx_b tx_ds oa /\ p5 tx_b tx_ds oa end module Properties_Snoc use Properties use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.invariants.iq0.IQ0 use export proofs.ordre_appel.properties.q1.Q1_Snoc use export proofs.ordre_appel.properties.q2.Q2_Snoc use export proofs.ordre_appel.properties.q3.Q3_Snoc use export proofs.ordre_appel.invariants.iq4_2.IQ4_2_Snoc use export proofs.ordre_appel.properties.q4_1.Q4_1_Snoc use export proofs.ordre_appel.properties.q4_2.Q4_2_Snoc use export proofs.ordre_appel.properties.q5.Q5_Snoc use export proofs.ordre_appel.properties.q6.Q6_Snoc use export proofs.ordre_appel.properties.p4.P4_Snoc use export proofs.ordre_appel.properties.p5.P5_Snoc let lemma properties_empty (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) (m : EnumMap.t) requires { oa = Seq.empty} requires { iq0 op oa m } requires { nb_b = nb_boursiers op } requires { nb_ds = nb_du_secteur op } ensures { ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa } = assert { q6 tx_b tx_ds op oa }; iq4_2_empty nb_b tx_b op oa m end module Properties_UpToRangAppel use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts 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.properties.q1.Q1_UpToRangAppel use proofs.ordre_appel.properties.q2.Q2_UpToRangAppel use proofs.ordre_appel.properties.q3.Q3_UpToRangAppel use proofs.ordre_appel.invariants.iq4_2.IQ4_2_UpToRangAppel use proofs.ordre_appel.properties.q4_1.Q4_1_UpToRangAppel use proofs.ordre_appel.properties.q4_2.Q4_2_UpToRangAppel use proofs.ordre_appel.properties.q5.Q5_UpToRangAppel use proofs.ordre_appel.properties.q6.Q6_UpToRangAppel use proofs.ordre_appel.properties.p4.P4_UpToRangAppel use proofs.ordre_appel.properties.p5.P5_UpToRangAppel use Properties let lemma properties_up_to_rang_appel_oa (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa1 oa2 : seq_voeu) requires { [@expl:alld(oa1)] all_distincts oa1 } requires { ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa1 } requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 } ensures { ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa2 } = q1_up_to_rang_appel_oa tx_b oa1 oa2; q2_up_to_rang_appel_oa tx_b tx_ds oa1 oa2; q3_up_to_rang_appel_oa oa1 oa2; iq4_2a_up_to_rang_appel_oa nb_b tx_b oa1 oa2; q4_1_up_to_rang_appel_oa nb_b tx_b oa1 oa2; q4_2_up_to_rang_appel_oa nb_ds tx_ds oa1 oa2; q5_up_to_rang_appel_oa nb_b nb_ds tx_b tx_ds oa1 oa2; q6_up_to_rang_appel_oa tx_b tx_ds op oa1 oa2; p4_up_to_rang_appel_oa tx_b tx_ds oa1 oa2; p5_up_to_rang_appel_oa tx_b tx_ds oa1 oa2 let lemma properties_up_to_rang_appel_op (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op1 op2 oa : seq_voeu) requires { ordre_appel_properties nb_b nb_ds tx_b tx_ds op1 oa } requires { seq_voeu_eq_up_to_rang_appel op1 op2 } ensures { ordre_appel_properties nb_b nb_ds tx_b tx_ds op2 oa } = q6_up_to_rang_appel_op tx_b tx_ds op1 op2 oa end module Invariants use proofs.ordre_appel.seq_voeux.SeqVoeux use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use proofs.ordre_appel.invariants.iqx.IQX use proofs.ordre_appel.invariants.iq0.IQ0 use proofs.ordre_appel.invariants.iq1.IQ1 use proofs.ordre_appel.invariants.iq2.IQ2 use proofs.ordre_appel.invariants.iq3_0.IQ3_0 use proofs.ordre_appel.invariants.iq3_1.IQ3_1 use proofs.ordre_appel.invariants.iq3_2.IQ3_2 use proofs.ordre_appel.invariants.iq3_3.IQ3_3 use proofs.ordre_appel.invariants.iq3_4.IQ3_4 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.invariants.iq6.IQ6 use Properties predicate invariants_algo (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa :seq_voeu) (filesAttente : EnumMap.t) = let nb_v = Seq.length op in nb_b = nb_boursiers op && nb_ds = nb_du_secteur op && iq0 op oa filesAttente && iqx_0 nb_v nb_b nb_ds oa filesAttente && iqx_2 nb_b tx_b oa && iqx_3 nb_b nb_ds oa && iqx_4 oa filesAttente && iqx_5 oa filesAttente && iq1 nb_b tx_b oa && iq2 nb_b nb_ds tx_b tx_ds oa && iq3_0 oa filesAttente && iq3_1 oa filesAttente && iq3_2 oa filesAttente && iq3_3 oa filesAttente && iq3_4 oa filesAttente && iq4_1 nb_ds tx_ds oa filesAttente && iq4_2 nb_b tx_b oa filesAttente && iq4_3 nb_b nb_ds tx_b tx_ds oa filesAttente && iq6 tx_b tx_ds oa filesAttente && ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa end module Invariants_Snoc use int.Int use seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use proofs.ordre_appel.eligibles.ValidEligibles use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Lemmas use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.PQueueVoeuxClasses as PQueue use proofs.ordre_appel.invariants.iqx.IQX_Snoc use proofs.ordre_appel.invariants.iq0.IQ0_Snoc use proofs.ordre_appel.invariants.iq1.IQ1_Snoc use proofs.ordre_appel.invariants.iq2.IQ2_Snoc use proofs.ordre_appel.invariants.iq3_0.IQ3_0_Snoc use proofs.ordre_appel.invariants.iq3_1.IQ3_1_Snoc use proofs.ordre_appel.invariants.iq3_2.IQ3_2_Snoc use proofs.ordre_appel.invariants.iq3_3.IQ3_3_Snoc use proofs.ordre_appel.invariants.iq3_4.IQ3_4_Snoc use proofs.ordre_appel.invariants.iq4_1.IQ4_1_Snoc use proofs.ordre_appel.invariants.iq4_2.IQ4_2_Snoc use proofs.ordre_appel.invariants.iq4_3.IQ4_3_Snoc use proofs.ordre_appel.invariants.iq6.IQ6_Snoc use Properties_Snoc use export Invariants (* unfold invariants_algo *) (* unfold ordre_appel_properties_for_oa *) (* unfold ordre_appel_seq_properties *) (* split_all_full *) let lemma invariants_algo_snoc (cB cR : bool) (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) (om m : EnumMap.t) (eligibles: PQueue.t) (v : VoeuClasse.t) requires { [@expl:pre/g ok] seq_groupe_ok op } requires { [@expl:pre/g sorted] seq_rangs_sorted op } (*requires { [@expl:pre/rangs >= 1] 1 <= v.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang }*) requires { [@expl:pre/valid eligibles] meilleur_eligible cB cR om eligibles v } requires { [@expl:pre/alld m] enummap_all_distincts om } requires { [@expl:pre/x selected] enummap_pop_v om m v } requires { [@expl:pre/cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oa nb_b } requires { [@expl:pre/cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_ds oa nb_ds } requires { [@expl:pre/inv algo om] invariants_algo nb_b nb_ds tx_b tx_ds op oa om } ensures { invariants_algo nb_b nb_ds tx_b tx_ds op (snoc oa v) m } = let nb_v = Seq.length op in let s = snoc oa v in iq0_snoc op oa om m v; iqx_0_snoc nb_v nb_b nb_ds oa om m v; iqx_2_snoc cB cR nb_b tx_b oa om eligibles v; iqx_3_snoc nb_v nb_b nb_ds oa om m v; iqx_4_snoc oa om m v; iqx_5_snoc oa om m v; iq1_snoc nb_b tx_b oa v; q1_snoc nb_b tx_b oa v; iq2_snoc cB cR nb_b nb_ds tx_b tx_ds oa om m eligibles v; q2_snoc nb_b nb_ds tx_b tx_ds oa v; iq3_0_snoc cB cR eligibles oa om m v; iq3_1_snoc cB cR eligibles oa om m v; q3_snoc oa m v; iq3_2_snoc cB cR eligibles oa om m v; iq3_3_snoc cB cR eligibles oa om m v; iq3_4_snoc cB cR eligibles oa om m v; iq4_1_snoc cB cR nb_ds tx_ds oa om m eligibles v; iq4_2_snoc cB cR nb_b tx_b oa om m eligibles v; iq4_3_snoc cB cR nb_b nb_ds tx_b tx_ds oa om m eligibles v; iq6_snoc cB cR nb_b nb_ds tx_b tx_ds oa om m v; q4_1_snoc nb_b tx_b oa m v; q4_2_snoc nb_ds tx_ds oa m v; q5_snoc nb_b nb_ds tx_b tx_ds oa m v; q6_snoc nb_b nb_ds tx_b tx_ds op oa m v; p4_snoc nb_b nb_ds tx_b tx_ds oa s m v; p5_snoc nb_b nb_ds tx_b tx_ds oa s m v; () let lemma invariants_algo_init (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) (m : EnumMap.t) requires { length op = EnumMap.get_nb_voeux_classes m } requires { nb_b = nb_boursiers op = EnumMap.get_nb_boursiers m } requires { nb_ds = nb_du_secteur op = EnumMap.get_nb_du_secteur m } requires { seq_groupe_ok op } requires { seq_rangs_sorted op } requires { oa = Seq.empty } requires { enummap_eq_grp m op } ensures { invariants_algo nb_b nb_ds tx_b tx_ds op oa m } = iq0_empty op m; iqx_0_empty op oa m; iq4_1_empty nb_ds tx_ds op oa m; iq4_2_empty nb_b tx_b op oa m; iqx_4_empty op oa m; (* iqx_4_empty g oa m; iqx_5_empty g oa m; iq4_2_empty g oa m; iq4_3_empty g oa m; iq6_empty g oa m; properties_empty g oa m *) () end module GroupeClassementValideProperties use int.Int use seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel use Properties use Properties_UpToRangAppel use fr.parcoursup.whyml.ordreappel.algo.taux.Taux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide predicate ordre_appel_properties_oa (g : GroupeClassementValide.t) (oa : seq_voeu) = let nb_b, tx_b = nb_boursiers g, get_taux_min_boursiers g in let nb_ds, tx_ds = nb_du_secteur g, get_taux_min_du_secteur g in let op = get_ordre_pedagogique g in Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa predicate ordre_appel_properties (g : GroupeClassementValide.t) = let oa = get_ordre_appel_list g in ordre_appel_properties_oa g oa predicate ordre_appel_contiguous (g : GroupeClassementValide.t) = let oa = get_ordre_appel_list g in seq_rangs_appel_contiguous oa let lemma oap_up_to_rang_appel (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op1 oa1 op2 oa2 : seq_voeu) requires { all_distincts oa1 } requires { Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op1 oa1 } requires { seq_voeu_eq_up_to_rang_appel op1 op2 } requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 } ensures { Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op2 oa2 } = properties_up_to_rang_appel_oa nb_b nb_ds tx_b tx_ds op1 oa1 oa2; assert { Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op1 oa2 } let lemma oap_up_to_rang_appel_groupe (g1 : GroupeClassementValide.t) (oa : seq_voeu) (g2 : GroupeClassementValide.t) requires { [@expl:pre/alld(oa)] all_distincts oa } requires { [@expl:pre/#b g1 = #b g2] nb_boursiers g1 = nb_boursiers g2 } requires { [@expl:pre/#ds g1 = #ds g2] nb_du_secteur g1 = nb_du_secteur g2 } requires { [@expl:pre/%b g1 = %b g2] get_taux_min_boursiers g1 = get_taux_min_boursiers g2 } requires { [@expl:pre/%ds g1 = %ds g2] get_taux_min_du_secteur g1 = get_taux_min_du_secteur g2 } requires { [@expl:pre/specs g1 oa] ordre_appel_properties_oa g1 oa } requires { [@expl:pre/op g1 = op g2 (mod ra)] seq_voeu_eq_up_to_rang_appel (get_ordre_pedagogique g1) (get_ordre_pedagogique g2) } requires { [@expl:pre/oa g1 = oa g2 (mod ra)] seq_voeu_eq_up_to_rang_appel oa (get_ordre_appel_list g2) } ensures { [@expl:specs g2] ordre_appel_properties g2 } = () end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git