Parcoursup / Calcul de l'ordre d'appel des candidats index
module IQ4_1 use int.Int use seq.Seq 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.SeqVoeuxEqUpToRangAppel 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 fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props clone proofs.ordre_appel.invariants.iq4_xa.IQ4_xa as IQ4_1a with function est_x = est_du_secteur function in_Zr (nb_r : int) (tx_r : Taux.t) (oa : seq_voeu) (i : int) : bool = IQ4_1a.in_Z oa tx_r nb_r i function nb_contraintes_taux_ds (nb_r : int) (tx_r : Taux.t) (oa : seq_voeu) : int = IQ4_1a.nb_contraintes_taux_x oa tx_r nb_r let lemma in_Zds_eq_up_to_rang_appel (s1 s2 : seq_voeu) (nb_r : int) (tx_r : Taux.t) (i : int) requires { seq_voeu_eq_up_to_rang_appel s1 s2 } requires { 0 <= i < length s1 } ensures { in_Zr nb_r tx_r s1 i = in_Zr nb_r tx_r s2 i } = () let lemma nb_contraintes_taux_r_up_to_rang_appel (s1 s2 : seq_voeu) (tx_r : taux) (nb_r : int) (i : int) requires { seq_voeu_eq_up_to_rang_appel s1 s2 } requires { 0 <= i < length s1 } ensures { nb_contraintes_taux_ds nb_r tx_r s1[..i] = nb_contraintes_taux_ds nb_r tx_r s2[..i] } = () let lemma not_in_Zr (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (i : int) requires { not in_Zr nb_r tx_r s i } ensures { not est_du_secteur s[i] \/ not taux_ds_contraignant tx_r s[..i] nb_r } = () let lemma taux_nul_pas_de_contrainte (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (i : int) requires { 0 <= i < length s } requires { tx_r = 0 } ensures { not in_Zr nb_r tx_r s i } = IQ4_1a.taux_nul_pas_de_contrainte s tx_r nb_r i predicate iq4_1a_loc (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (k : int) = (* IQ4_1a.iq4_xa_loc s tx_r nb_r k *) forall i. 0 <= i <= k -> let nbCb = nb_contraintes_taux_ds nb_r tx_r s[..i] in 100 * nbCb <= tx_r * i + 100 let lemma iq4_1a_loc_equiv (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (k : int) ensures { iq4_1a_loc nb_r tx_r s k <-> IQ4_1a.iq4_xa_loc s tx_r nb_r k } = () predicate iq4_1a (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) = (* IQ4_1a.iq4_xa s tx_r nb_r *) forall k. 0 <= k <= length s -> iq4_1a_loc nb_r tx_r s k let lemma iq4_1a_equiv (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) ensures { iq4_1a nb_r tx_r s <-> IQ4_1a.iq4_xa s tx_r nb_r } = () predicate iq4_1b_loc (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (m : EnumMap.t) (k : int) = forall i. 0 <= i <= k -> (*(not in_Zr (nb_boursiers g) nb_r (get_taux_min_boursiers g) tx_r s i) ->*) (not in_Zr nb_r tx_r s i) -> ((forall v. enummap_est_boursier m v -> voeu_lt s[i] v) && (forall v. seq_contains v s[i+1..] -> est_boursier v -> voeu_lt s[i] v)) predicate iq4_1b (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (m : EnumMap.t) = forall k. 0 <= k < length s -> iq4_1b_loc nb_r tx_r s m k predicate iq4_1 (nb_r : int) (tx_r : Taux.t) (oak : seq_voeu) (m : EnumMap.t) = iq4_1a nb_r tx_r oak && iq4_1b nb_r tx_r oak m end module IQ4_1_Lemmas use int.Int use seq.Seq use proofs.lib.seq.Seq use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux use proofs.ordre_appel.eligibles.Eligibles use proofs.ordre_appel.eligibles.ValidEligibles 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 fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Lemmas use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts use IQ4_1 let lemma iq4_1b_loc_ex (nb_r : int) (tx_r : Taux.t) (s : seq_voeu) (m : EnumMap.t) (k : int) requires { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r s i) -> ((forall v. enummap_est_boursier m v -> voeu_lt s[i] v) && (forall v. seq_contains v s[i+1..] -> est_boursier v -> voeu_lt s[i] v)) } ensures { iq4_1b_loc nb_r tx_r s m k } = () let lemma aux1 (cB cR : bool) (nb_r : int) (tx_r : 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 { not Fset.is_empty eligibles } requires { not taux_ds_contraignant tx_r oak nb_r && not cR } ensures { forall v. enummap_est_boursier m v -> voeu_lt x v } = assert { [@expl:A 0] eligibles_contains_eligible_heads cB cR om eligibles }; let lemma aux11 (v h : VoeuClasse.t) requires { enummap_est_boursier m v } requires { get_type_candidat x <> get_type_candidat v } requires { h = Seq.get (EnumMap.get_queue om (get_type_candidat v)) 0 } ensures { h = Seq.get (EnumMap.get_queue m (get_type_candidat v)) 0 } ensures { est_boursier h } ensures { seq_contains v (EnumMap.get_queue m (get_type_candidat v)) } ensures { est_eligible_p cB cR h } ensures { enummap_v_is_head om h } ensures { Fset.mem h eligibles } ensures { h <> x } ensures { voeu_lt x h } ensures { v <> h -> voeu_lt h v } = assert { get_type_candidat v = get_type_candidat h }; enummap_poped_head_saved om m x v h; enummap_head_is_lt_its_queue m v h in assert { [@expl:A 5] forall v. enummap_est_boursier m v -> (get_type_candidat x) <> (get_type_candidat v) -> let q = EnumMap.get_queue m (get_type_candidat v) in voeu_lt x q[0] }; assert { [@expl:A 6] forall v. enummap_est_boursier m v -> (get_type_candidat x) <> (get_type_candidat v) -> let q = EnumMap.get_queue_of m v in (v <> q[0] -> voeu_lt q[0] v) }; assert { forall v. enummap_est_boursier m v -> (get_type_candidat x) <> (get_type_candidat v) -> let q = EnumMap.get_queue_of m v in (v <> q[0] -> (voeu_lt x q[0] /\ voeu_lt q[0] v)) }; assert { forall v. enummap_est_boursier m v -> (get_type_candidat x) <> (get_type_candidat v) -> voeu_lt x v }; assert { [@expl:A 7] forall v. enummap_est_boursier m v -> (get_type_candidat x) = (get_type_candidat v) -> let q = EnumMap.get_queue_of m v in voeu_lt_than_queue x q }; assert { [@expl:A 8] forall v. enummap_est_boursier m v -> (get_type_candidat x) = (get_type_candidat v) -> EnumMap.get_queue_of m v = EnumMap.get_queue_of m x }; assert { [@expl:A 9] forall v. enummap_est_boursier m v -> (get_type_candidat x) = (get_type_candidat v) -> voeu_lt x v }; assert { forall v. enummap_est_boursier m v -> x <> v -> voeu_lt x v } let lemma iq4_1b_snoc_aux (cB cR : bool) (nb_r : int) (tx_r : Taux.t) (oak : seq_voeu) (om m : EnumMap.t) (eligibles: PQueue.t) (x : voeu) requires {[@expl:pre iq4_1b] iq4_1b nb_r tx_r oak om } 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:cR equiv tx_r contraignant] cR = taux_ds_contraignant tx_r oak nb_r} requires { not in_Zr nb_r tx_r (snoc oak x) (length oak) } ensures { iq4_1b_loc nb_r tx_r (snoc oak x) m (length oak) } = let s = snoc oak x in let k = length s - 1 in assert { iq4_1b_loc nb_r tx_r oak om (k-1) }; assert { forall i. 0 <= i <= k-1 -> not in_Zr nb_r tx_r s i -> not in_Zr nb_r tx_r oak i }; assert { forall i. 0 <= i <= (k-1) -> not in_Zr nb_r tx_r oak i -> forall v. enummap_est_boursier om v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k-1 -> not in_Zr nb_r tx_r s i -> forall v. enummap_est_boursier m v -> voeu_lt s[i] v }; assert { enummap_contains om x }; assert { est_boursier x -> enummap_est_boursier om x }; assert { forall i. 0 <= i <= k-1 -> not in_Zr nb_r tx_r oak i -> est_boursier x -> voeu_lt oak[i] x }; seq_suffix_snoc s oak x; assert { forall i. 0 <= i <= (k-1) -> not in_Zr nb_r tx_r oak i -> forall v. seq_contains v oak[i+1..] -> est_boursier v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k-1 -> forall v. seq_contains v s[i+1..] -> seq_contains v (snoc oak[i+1..] x) }; assert { forall i. 0 <= i <= k-1 -> not in_Zr nb_r tx_r s i -> forall v. seq_contains v s[i+1..] -> est_boursier v -> voeu_lt s[i] v }; iq4_1b_loc_ex nb_r tx_r s m (k-1); assert { iq4_1b_loc nb_r tx_r s m (k-1) }; if not taux_ds_contraignant tx_r oak nb_r then begin if not PQueue.is_empty eligibles then begin aux1 cB cR nb_r tx_r oak om m eligibles x; iq4_1b_loc_ex nb_r tx_r s m k; assert { iq4_1b_loc nb_r tx_r s m k }; end else begin absurd; end; end else begin assert { x = s[length oak] }; assert { s[..length oak] == oak }; assert { not est_du_secteur x }; if est_eligible_p cB cR x then begin absurd; end else begin assert { est_boursier_hors_secteur x }; assert { enummap_v_is_head om x }; assert { m.bds = empty }; assert { forall v. enummap_contains m v -> enummap_contains om v }; assert { forall v. enummap_est_boursier om v -> est_boursier_hors_secteur v }; assert { forall v. enummap_est_boursier om v -> v <> x -> voeu_lt x v }; assert { forall v. enummap_est_boursier m v -> v <> x -> voeu_lt x v }; iq4_1b_loc_ex nb_r tx_r s m k; assert { iq4_1b_loc nb_r tx_r s m k }; end end let lemma iq4_1a_snoc (nb_r : int) (tx_r : Taux.t) (oak : seq_voeu) (x : voeu) requires { iq4_1a nb_r tx_r oak } ensures { iq4_1a nb_r tx_r (snoc oak x) } = IQ4_1a.iq4_xa_snoc oak tx_r nb_r x let lemma iq4_1b_snoc (cB cR : bool) (nb_r : int) (tx_r : Taux.t) (oak : seq_voeu) (om m : EnumMap.t) (eligibles: PQueue.t) (x : voeu) requires { [@expl:pre iq4_1b] iq4_1b nb_r tx_r oak om } 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:cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_r oak nb_r } ensures { iq4_1b nb_r tx_r (snoc oak x) m } = let s = snoc oak x in assert { enummap_contains om x }; assert { est_boursier x -> enummap_est_boursier om x }; for k = 0 to length s - 1 do invariant { forall j. 0 <= j < k -> iq4_1b_loc nb_r tx_r s m j } assert { forall i. 0 <= i < k -> s[i] = oak[i] }; assert { forall i. 0 <= i <= k -> s[..i] == oak[..i] }; if k < length s - 1 then begin assert { forall i. 0 <= i <= k -> s[i+1..] == snoc oak[i+1..] x }; assert { iq4_1b_loc nb_r tx_r oak om k }; assert { forall i. 0 <= i < k -> s[i] = oak[i] }; assert { forall v. enummap_est_boursier m v -> enummap_est_boursier om v }; assert { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r s i) -> (not in_Zr nb_r tx_r oak i) }; assert { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r oak i) -> forall v. enummap_est_boursier om v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r s i) -> forall v. enummap_est_boursier m v -> voeu_lt s[i] v }; assert { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r oak i) -> forall v. seq_contains v oak[i+1..] -> est_boursier v -> voeu_lt oak[i] v }; seq_suffix_snoc s oak x; assert { forall i. 0 <= i <= k -> forall v. seq_contains v s[i+1..] -> est_boursier v -> (seq_contains v (snoc oak[i+1..] x) ) }; assert { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r s i) -> forall v. seq_contains v s[i+1..] -> est_boursier v -> voeu_lt s[i] v }; assert { forall i. 0 <= i <= k -> (not in_Zr nb_r tx_r s i) -> ((forall v. enummap_est_boursier m v -> voeu_lt s[i] v) && (forall v. seq_contains v s[i+1..] -> est_boursier v -> voeu_lt s[i] v)) }; iq4_1b_loc_ex nb_r tx_r s m k; assert { iq4_1b_loc nb_r tx_r s m k }; end else begin assert { forall i. 0 <= i < k -> s[i+1..] == snoc oak[i+1..] x }; assert { iq4_1b_loc nb_r tx_r oak om (k-1) }; assert { forall i. 0 <= i < k -> s[i] = oak[i] }; assert { forall v. enummap_est_boursier m v -> enummap_est_boursier om v }; assert { forall i. 0 <= i < k -> (not in_Zr nb_r tx_r oak i) -> (forall v. enummap_est_boursier om v -> voeu_lt oak[i] v ) }; assert { forall i. 0 <= i < length s - 1 -> (not in_Zr nb_r tx_r s i) -> forall v. enummap_est_boursier m v -> voeu_lt s[i] v }; assert { forall i. 0 <= i < k -> (not in_Zr nb_r tx_r oak i) -> forall v. seq_contains v oak[i+1..] -> est_boursier v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i < k -> forall v. seq_contains v s[i+1..] -> est_boursier v -> (seq_contains v (snoc oak[i+1..] x)) }; assert { forall i. 0 <= i < length s - 1 -> (not in_Zr nb_r tx_r s i) -> forall v. seq_contains v s[i+1..] -> est_boursier v -> voeu_lt s[i] v }; assert { iq4_1b_loc nb_r tx_r oak m (k-1) }; if in_Zr nb_r tx_r s (length s -1) then begin iq4_1b_loc_ex nb_r tx_r s m k; assert { iq4_1b_loc nb_r tx_r s m k } end else iq4_1b_snoc_aux cB cR nb_r tx_r oak om m eligibles x; end done end module IQ4_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.SeqVoeuxTaux use proofs.ordre_appel.eligibles.Eligibles use proofs.ordre_appel.eligibles.ValidEligibles 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 fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.PQueueVoeuxClasses as PQueue use IQ4_1_Lemmas use export IQ4_1 let lemma iq4_1_snoc (cB cR : bool) (nb_r : int) (tx_r : 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:cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_r oak nb_r } requires {[@expl:pre iq4_1] iq4_1 nb_r tx_r oak om } ensures {[@expl:iq4_1(oak.x)] iq4_1 nb_r tx_r (snoc oak x) m } = () use proofs.ordre_appel.invariants.iq0.IQ0 let lemma iq4_1_empty (nb_r : int) (tx_r : Taux.t) (op oak : seq_voeu) (m : EnumMap.t) requires { oak = Seq.empty } requires { nb_r = nb_du_secteur op } requires { iq0 op oak m } ensures { iq4_1 nb_r tx_r empty m } = () end (* generated on Thu Nov 21 02:04:27 UTC 2024 from rev: *)
Generated by why3doc 1.7.2+git