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