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