Parcoursup / Calcul de l'ordre d'appel des candidats index
module Eligibles use int.Int use seq.Seq use proofs.ordre_appel.seq_voeux.SortedSeqVoeux use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props predicate est_eligible_p (cB : bool) (cR : bool) (v : VoeuClasse.t) = (est_boursier v || not cB) && (est_du_secteur v || not cR) predicate enummap_contains_eligible_p (cB : bool) (cR : bool) (m : EnumMap.t) (t : type_candidat) = match t with | BOURSIER_DU_SECTEUR -> m.bds <> Seq.empty && est_eligible_p cB cR m.bds[0] | BOURSIER_HORS_SECTEUR -> m.bhs <> Seq.empty && est_eligible_p cB cR m.bhs[0] | NON_BOURSIER_DU_SECTEUR -> m.nbds <> Seq.empty && est_eligible_p cB cR m.nbds[0] | NON_BOURSIER_HORS_SECTEUR -> m.nbhs <> Seq.empty && est_eligible_p cB cR m.nbhs[0] end let lemma eligibles_conditions (cB : bool) (cR : bool) (m : EnumMap.t) requires { [@expl: pre - m is not empty] not enummap_is_empty m } requires { [@expl: pre - cB impl remains boursiers] cB -> enummap_remains_boursiers m } requires { [@expl: pre - cR impl remains residents] cR -> enummap_remains_du_secteur m } ensures { (cB /\ cR /\ get_queue m BOURSIER_DU_SECTEUR = empty) <-> forall t. not enummap_contains_eligible_p cB cR m t } = assert { (cB /\ cR /\ get_queue m BOURSIER_DU_SECTEUR = empty) -> (forall t. t <> BOURSIER_DU_SECTEUR -> not enummap_contains_eligible_p cB cR m t) }; if not (EnumMap.queue_is_empty m BOURSIER_DU_SECTEUR) then assert { enummap_contains_eligible_p cB cR m BOURSIER_DU_SECTEUR } else if not cB && not cR then let t = any type_candidat ensures { get_queue m result <> empty } in assert { enummap_contains_eligible_p cB cR m t } else if cB && not cR then begin assert { m.bhs <> empty }; assert { enummap_contains_eligible_p cB cR m BOURSIER_HORS_SECTEUR } end else if not cB && cR then begin assert { m.nbds <> empty }; assert { enummap_contains_eligible_p cB cR m NON_BOURSIER_DU_SECTEUR }; end end module ValidEligibles use int.Int use seq.Seq use set.Fset use proofs.ordre_appel.seq_voeux.SeqVoeux use proofs.ordre_appel.seq_voeux.SortedSeqVoeux 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.voeu_classe.PQueueVoeuxClasses as PQueue use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap use fr.parcoursup.whyml.ordreappel.algo.enum_map.AllDistincts use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Props use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Lemmas use Eligibles predicate type_candidat_not_eligible (eligibles : PQueue.t) (t: type_candidat) = forall v. Fset.mem v eligibles -> (get_type_candidat v) <> t predicate eligibles_constraints_imp_remain (cB cR : bool) (m : EnumMap.t) = (cB -> enummap_remains_boursiers m) && (cR -> enummap_remains_du_secteur m) predicate eligibles_contains_eligible_heads (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) = forall v. (enummap_v_is_head m v /\ est_eligible_p cB cR v) <-> Fset.mem v eligibles predicate eligibles_empty_imp_conflict_non_empty_bhs (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) = not enummap_is_empty m -> eligibles = empty -> (cB && cR && m.bds = Seq.empty && m.bhs <> Seq.empty) predicate eligibles_lt_than_their_queue (m : EnumMap.t) (eligibles : PQueue.t) = forall v. Fset.mem v eligibles -> voeu_lt_than_queue v (get_queue m (get_type_candidat v))[1..] predicate eligibles_are_all_distincts (eligibles : PQueue.t) = forall v vp. Fset.mem v eligibles -> Fset.mem vp eligibles -> v <> vp -> voeu_distinct v vp predicate eligibles_contains_bds (m : EnumMap.t) (eligibles : PQueue.t) = m.bds <> Seq.empty -> Fset.mem m.bds[0] eligibles predicate eligibles_no_constraint_imp_all_heads_or_empty (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) = not (cB \/ cR) -> (forall t. type_candidat_not_eligible eligibles t -> EnumMap.queue_is_empty m t) predicate valid_eligibles (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) = eligibles_constraints_imp_remain cB cR m && eligibles_contains_eligible_heads cB cR m eligibles && eligibles_empty_imp_conflict_non_empty_bhs cB cR m eligibles && eligibles_lt_than_their_queue m eligibles && eligibles_contains_bds m eligibles && eligibles_no_constraint_imp_all_heads_or_empty cB cR m eligibles predicate meilleur_eligible (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) (v : voeu) = valid_eligibles cB cR m eligibles && if eligibles <> empty then (Fset.mem v eligibles /\ PQueue.minimal_elt v eligibles) else ((get_type_candidat v) = BOURSIER_HORS_SECTEUR /\ enummap_v_is_head m v) let lemma eligible_heads_imp_lt_than_their_queue (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) requires { eligibles_contains_eligible_heads cB cR m eligibles } ensures { eligibles_lt_than_their_queue m eligibles } = () let lemma eligible_heads_imp_eligibles_empty_imp_conflict_non_empty_bhs (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) requires { eligibles_constraints_imp_remain cB cR m } requires { eligibles_contains_eligible_heads cB cR m eligibles } ensures { eligibles_empty_imp_conflict_non_empty_bhs cB cR m eligibles } = if not enummap_is_empty m && PQueue.is_empty eligibles then begin assert { m.bds <> Seq.empty -> est_eligible_p cB cR m.bds[0] }; assert { forall v. enummap_v_is_head m v -> not est_eligible_p cB cR v }; end let lemma eligible_heads_imp_all_distincts (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) requires { eligibles_contains_eligible_heads cB cR m eligibles } requires { enummap_all_distincts m } ensures { eligibles_are_all_distincts eligibles } = () let lemma eligible_heads_imp_bds_eligibles (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) requires { eligibles_contains_eligible_heads cB cR m eligibles } ensures { eligibles_contains_bds m eligibles } = () let lemma eligible_heads_and_no_constraint_imp_all_heads_or_empty (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) requires { eligibles_contains_eligible_heads cB cR m eligibles } ensures { eligibles_no_constraint_imp_all_heads_or_empty cB cR m eligibles } = if not cR && not cB then assert { forall t. let q = EnumMap.get_queue m t in q <> Seq.empty -> Fset.mem q[0] eligibles } let lemma eligible_heads_implies_valid (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) requires { eligibles_constraints_imp_remain cB cR m } requires { eligibles_contains_eligible_heads cB cR m eligibles } ensures { valid_eligibles cB cR m eligibles } = () let lemma eligible_meilleur_lt_than_all_eligibles (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) (meilleur : voeu) requires { eligibles <> empty } requires { meilleur_eligible cB cR m eligibles meilleur } requires { enummap_all_distincts m } ensures { forall v. Fset.mem v eligibles -> v <> meilleur -> voeu_distinct meilleur v } ensures { forall v. Fset.mem v eligibles -> v <> meilleur -> voeu_lt meilleur v } ensures { forall v. Fset.mem v eligibles -> v <> meilleur -> let q = (EnumMap.get_queue m (get_type_candidat v)) in q <> Seq.empty -> (voeu_lt meilleur q[0] && voeu_lt_than_queue q[0] q[1..] && voeu_lt_than_queue meilleur q) } = assert { forall v. Fset.mem v eligibles -> v <> meilleur -> Fset.mem v eligibles -> enummap_v_is_head m v /\ est_eligible_p cB cR v } let lemma not_eligible_imp_empty_or_constraint (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) (t : type_candidat) requires { valid_eligibles cB cR m eligibles } requires { type_candidat_not_eligible eligibles t } ensures { EnumMap.get_queue m t = Seq.empty \/ (not type_est_boursier t && cB) \/ (not type_est_du_secteur t && cR) } = let q = EnumMap.get_queue m t in if not (q == Seq.empty) then begin let v = q[0] in assert { get_type_candidat v = t }; if est_eligible_p cB cR v then begin assert { enummap_v_is_head m v }; assert { Fset.mem v eligibles }; absurd; end; end let lemma eligibles_empty_imp_meilleur_lt_bds (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) (meilleur : voeu) requires { meilleur_eligible cB cR m eligibles meilleur } ensures { eligibles = empty -> voeu_lt_than_queue meilleur m.bds } = () let lemma meilleur_eligible_imp_pre_iq3 (cB cR : bool) (m : EnumMap.t) (eligibles : PQueue.t) (meilleur : voeu) requires { not (eligibles == Fset.empty) } requires { [@expl:meilleur eligibles] meilleur_eligible cB cR m eligibles meilleur } requires { [@expl:alld(m)] enummap_all_distincts m } ensures { not est_boursier_du_secteur meilleur -> m.bds <> Seq.empty -> (voeu_lt meilleur m.bds[0] && voeu_lt_than_queue m.bds[0] m.bds[1..] && voeu_lt_than_queue meilleur m.bds) } ensures { (get_type_candidat meilleur) = NON_BOURSIER_HORS_SECTEUR -> m.nbds <> Seq.empty -> (voeu_lt meilleur m.nbds[0] && voeu_lt_than_queue m.nbds[0] m.nbds[1..] && voeu_lt_than_queue meilleur m.nbds) } ensures { (get_type_candidat meilleur) = NON_BOURSIER_HORS_SECTEUR -> m.bhs <> Seq.empty -> (voeu_lt meilleur m.bhs[0] && voeu_lt_than_queue m.bhs[0] m.bhs[1..] && voeu_lt_than_queue meilleur m.bhs) } ensures { (get_type_candidat meilleur) = NON_BOURSIER_HORS_SECTEUR -> forall t. t<> NON_BOURSIER_HORS_SECTEUR -> let q = EnumMap.get_queue m t in q <> Seq.empty -> (voeu_lt meilleur q[0] && voeu_lt_than_queue q[0] q[1..] && voeu_lt_than_queue meilleur q) } = if not est_non_boursier_hors_secteur meilleur then return; assert { forall v. Fset.mem v eligibles -> v <> meilleur -> enummap_v_is_head m v -> voeu_lt meilleur v }; assert { not cB /\ not cR }; assert { not (Seq.(==) m.nbds Seq.empty) -> est_eligible_p cB cR m.nbds[0] }; assert { not (Seq.(==) m.nbds Seq.empty) -> voeu_lt meilleur m.nbds[0] }; assert { not (Seq.(==) m.bhs Seq.empty) -> voeu_lt meilleur m.bhs[0] } end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git