Parcoursup / Calcul de l'ordre d'appel des candidats index
module IQ4_3 use int.Int use seq.Seq use proofs.lib.seq.Seq use proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use proofs.ordre_appel.seq_voeux.SeqVoeux use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props use fr.parcoursup.whyml.ordreappel.algo.taux.Taux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse predicate in_some_Z (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (i : int) = (in_Zb nb_b tx_b oa i || in_Zr nb_r tx_r oa i) predicate iq4_3b_loc (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (m : EnumMap.t) (k : int) = forall i. 0 <= i <= k -> not (in_some_Z nb_b nb_r tx_b tx_r oa i) -> ((forall v. enummap_contains m v -> voeu_lt oa[i] v) && (forall v. (seq_contains v oa[i+1..]) -> voeu_lt oa[i] v)) predicate iq4_3b (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (m : EnumMap.t) = forall k. 0 <= k < length oa -> iq4_3b_loc nb_b nb_r tx_b tx_r oa m k predicate iq4_3 (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oa : seq_voeu) (m : EnumMap.t) = iq4_3b nb_b nb_r tx_b tx_r oa m end module IQ4_3_Aux 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 proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use IQ4_3 let lemma iq4_3b_loc_ex (nb_b nb_r : int) (tx_b tx_r : Taux.t) (s : seq_voeu) (m : EnumMap.t) (k : int) requires { forall i. 0 <= i <= k -> (not in_some_Z nb_b nb_r tx_b tx_r s i) -> forall v. enummap_contains m v -> voeu_lt s[i] v } requires { forall i. 0 <= i <= k -> (not in_some_Z nb_b nb_r tx_b tx_r s i) -> forall v. seq_contains v s[i+1..] -> voeu_lt s[i] v } ensures { iq4_3b_loc nb_b nb_r tx_b tx_r s m k } = () let lemma aux1 (cB cR : bool) (nb_b nb_r : int) (tx_b 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 } requires { not taux_b_contraignant tx_b oak nb_b && not cB } ensures { forall v. enummap_contains m v -> voeu_lt x v } = assert { eligibles_contains_eligible_heads cB cR om eligibles }; assert { forall v. enummap_contains om v -> let q = EnumMap.get_queue om (get_type_candidat v) in (enummap_v_is_head om q[0] && est_eligible_p cB cR q[0]) }; assert { forall v. enummap_contains 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 { forall v. enummap_contains 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 { forall v. enummap_contains m v -> (get_type_candidat x) <> (get_type_candidat v) -> let q = EnumMap.get_queue m (get_type_candidat v) in (v <> q[0] -> voeu_lt q[0] v) }; assert { forall v. enummap_contains m v -> (get_type_candidat x) <> (get_type_candidat v) -> let q = EnumMap.get_queue m (get_type_candidat v) in (v <> q[0] -> voeu_lt q[0] v /\ voeu_lt x q[0]) }; assert { forall v. enummap_contains m v -> (get_type_candidat x) <> (get_type_candidat v) -> let q = EnumMap.get_queue m (get_type_candidat v) in (voeu_lt q[0] v /\ voeu_lt x q[0]) -> voeu_lt x v }; assert { forall v. enummap_contains m v -> (get_type_candidat x) <> (get_type_candidat v) -> voeu_lt x v }; assert { forall v. enummap_contains m v -> (get_type_candidat x) = (get_type_candidat v) -> let q = EnumMap.get_queue m (get_type_candidat v) in voeu_lt_than_queue x q }; assert { forall v. enummap_contains m v -> (get_type_candidat x) = (get_type_candidat v) -> voeu_lt x v}; assert { forall v. enummap_contains m v -> x <> v -> voeu_lt x v } let lemma iq4_3b_snoc_aux (cB cR : bool) (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oak : seq_voeu) (om m : EnumMap.t) (eligibles: PQueue.t) (x : voeu) requires {[@expl:pre iq4_3b] iq4_3b nb_b nb_r tx_b 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 } requires {[@expl:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b } requires { not in_Zr nb_r tx_r (snoc oak x) (length oak) } requires { not in_Zb nb_b tx_b (snoc oak x) (length oak) } ensures { iq4_3b_loc nb_b nb_r tx_b tx_r (snoc oak x) m (length oak) } = let s = snoc oak x in let k = length s - 1 in assert { iq4_3b_loc nb_b nb_r tx_b tx_r oak om (k-1) }; assert { forall i. 0 <= i <= k-1 -> not (in_some_Z nb_b nb_r tx_b tx_r oak i) -> forall v. enummap_contains om v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k-1 -> not (in_some_Z nb_b nb_r tx_b tx_r oak i) -> forall v. (seq_contains v oak[i+1..]) -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k-1 ->not (in_some_Z nb_b nb_r tx_b tx_r oak i) -> forall v. enummap_contains om v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k-1 ->not (in_some_Z nb_b nb_r tx_b tx_r oak i) -> forall v. (seq_contains v oak[i+1..]) -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k-1 -> not in_some_Z nb_b nb_r tx_b tx_r s i -> not in_some_Z nb_b nb_r tx_b tx_r oak i }; seq_suffix_snoc s oak x; assert { forall i v. 0 <= i <= k-1 -> seq_contains v s[i+1..] -> seq_contains v (snoc oak [i+1..] x) }; assert { enummap_contains om x }; assert { forall i. 0 <= i <= k-1 -> not in_some_Z nb_b nb_r tx_b tx_r s i -> forall v. seq_contains v s[i+1..] -> x <> v -> voeu_lt s[i] v }; assert { forall i. 0 <= i <= k-1 -> not in_some_Z nb_b nb_r tx_b tx_r s i -> forall v. seq_contains v s[i+1..] -> voeu_lt s[i] v }; assert { forall i. 0 <= i <= k-1 -> not (in_some_Z nb_b nb_r tx_b tx_r s i) -> forall v. enummap_contains m v -> voeu_lt s[i] v }; assert { forall i. 0 <= i <= k-1 -> not (in_some_Z nb_b nb_r tx_b tx_r s i) -> forall v. (seq_contains v s[i+1..]) -> voeu_lt s[i] v }; if not taux_ds_contraignant tx_r oak nb_r && not taux_b_contraignant tx_b oak nb_b then begin if not PQueue.is_empty eligibles then begin aux1 cB cR nb_b nb_r tx_b tx_r oak om m eligibles x; iq4_3b_loc_ex nb_b nb_r tx_b tx_r s m k; assert { iq4_3b_loc nb_b nb_r tx_b tx_r s m k }; end else begin absurd; end; end else begin assert { not PQueue.is_empty eligibles }; assert { cB || cR }; assert { est_eligible_p cB cR x }; assert { est_du_secteur x \/ est_boursier x }; if est_du_secteur x then begin assert { not cB }; assert { taux_ds_contraignant tx_r s nb_r }; assert { oak == s[..length oak] }; assert { not in_Zr nb_r tx_r s (length oak) -> not taux_ds_contraignant tx_r s[..length oak] nb_r }; absurd; end else begin assert { taux_b_contraignant tx_b s nb_b }; absurd; end; end let lemma iq4_3b_snoc (cB cR : bool) (nb_b nb_r : int) (tx_b tx_r : Taux.t) (oak : seq_voeu) (om m : EnumMap.t) (eligibles: PQueue.t) (x : voeu) requires { [@expl:pre iq4_3b] iq4_3b nb_b nb_r tx_b 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:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b } requires { [@expl:cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_r oak nb_r } ensures { iq4_3b nb_b nb_r tx_b tx_r (snoc oak x) m } = let s = snoc oak x in for k = 0 to length s - 1 do invariant { forall j. 0 <= j < k -> iq4_3b_loc nb_b nb_r tx_b 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] }; assert { forall i. 0 <= i < k -> s[i+1..] == snoc oak[i+1..] x }; assert { forall i. 0 <= i < k -> (not in_some_Z nb_b nb_r tx_b tx_r s i) -> (not in_some_Z nb_b nb_r tx_b tx_r oak i) }; assert { forall v. enummap_contains m v -> enummap_contains om v }; if k < length s - 1 then begin assert { iq4_3b_loc nb_b nb_r tx_b tx_r oak om k }; assert { forall i. 0 <= i <= k -> (not in_some_Z nb_b nb_r tx_b tx_r oak i) -> forall v. enummap_contains om v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i <= k -> (not in_some_Z nb_b nb_r tx_b tx_r s i) -> forall v. enummap_contains m v -> voeu_lt s[i] v }; seq_suffix_snoc s oak x; assert { s[k+1..] == snoc oak[k+1..] x }; assert { forall i. 0 <= i <= k -> forall v. seq_contains v s[i+1..] -> (seq_contains v (snoc oak[i+1..] x)) }; assert { enummap_contains om x }; assert { forall i. 0 <= i <= k -> (not in_some_Z nb_b nb_r tx_b tx_r s i) -> forall v. seq_contains v s[i+1..] -> voeu_lt s[i] v }; iq4_3b_loc_ex nb_b nb_r tx_b tx_r s m k; end else begin assert { iq4_3b_loc nb_b nb_r tx_b tx_r oak om (k-1) }; assert { forall i. 0 <= i < length s - 1 -> not in_some_Z nb_b nb_r tx_b tx_r oak i -> forall v. enummap_contains om v -> voeu_lt oak[i] v }; assert { forall i. 0 <= i < k -> forall v. seq_contains v s[i+1..] -> seq_contains v (snoc oak[i+1..] x) }; assert { enummap_contains om x }; if in_Zr nb_r tx_r s (length s -1) then begin iq4_3b_loc_ex nb_b nb_r tx_b tx_r s m k; end else if in_Zb nb_b tx_b s (length s -1) then begin iq4_3b_loc_ex nb_b nb_r tx_b tx_r s m k; end else iq4_3b_snoc_aux cB cR nb_b nb_r tx_b tx_r oak om m eligibles x; end; assert { iq4_3b_loc nb_b nb_r tx_b tx_r s m k } done end module IQ4_3_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 proofs.ordre_appel.invariants.iq4_1.IQ4_1 use proofs.ordre_appel.invariants.iq4_2.IQ4_2 use IQ4_3_Aux 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 export IQ4_3 let lemma iq4_3_snoc (cB cR : bool) (nb_b nb_r : int) (tx_b 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:cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oak nb_b } requires { [@expl:cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_r oak nb_r } requires { [@expl:pre iq4_3] iq4_3 nb_b nb_r tx_b tx_r oak om } ensures { iq4_3 nb_b nb_r tx_b tx_r (snoc oak x) m } = iq4_3b_snoc cB cR nb_b nb_r tx_b tx_r oak om m eligibles x end (* generated on Mon Feb 3 02:06:12 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git