Propriété 5

Si l’on munit l’ensemble des sélections ordonnées de candidats de l’ordre lexicographique induit par les classements, alors l’ordre d’appel est le maximum parmi toutes les sélections qui garantissent la première propriété.

module P5
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.lib.permutation.Permutation
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use proofs.ordre_appel.properties.q1.Q1

  (*
   * Ordre lexicographique sur les sequences de voeux
   *)
  predicate lexico_less_ind (s1 s2 : seq_voeu) (i : int)  =
  (
    (0<= i <= length s1 /\ 0<= i <= length s2)
    /\ (forall ip. 0 <= ip < i -> get_rang s1[ip] = get_rang s2[ip])
    /\ (i < length s1 -> (i < length s2 /\ voeu_lt s1[i] s2[i]))
  )

  predicate lexico_less_or_equal (s1 s2 : seq_voeu)  =
    (s1 == s2) || (exists i. lexico_less_ind s1 s2 i)

  (*
   * propriete 5 : minimalite pour l'ordre lexicographique parmi les
   * permutations de voeux ayant la propriete 1.
   *)
  predicate p5 (taux_b taux_r : Taux.t) (s : seq_voeu) =
    taux_r = 0->
      forall p : permutation. p.n = length s ->
         let sp = permut s p in  q1 taux_b sp -> lexico_less_or_equal s sp

end

module P5_UpToRangAppel
  use int.Int
  use seq.Seq
  use proofs.lib.permutation.Permutation
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use proofs.ordre_appel.properties.q1.Q1_UpToRangAppel

  use export P5

  let lemma permut_up_to_rang_appel (s1 s1p s2 s2p : seq_voeu) (p : permutation)
    requires { length s1 = p.n }
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    requires { s1p == permut s1 p }
    requires { s2p == permut s2 p }
    ensures {  seq_voeu_eq_up_to_rang_appel s1p s2p }
  = ()

  let lemma p5_up_to_rang_appel_oa (tx_b tx_r : Taux.t) (oa1 oa2 : seq_voeu)
    requires { [@expl:all(oa1)] all_distincts oa1 }
    requires { [@expl:p5(oa1)] p5 tx_b tx_r oa1 }
    requires { [@expl:oa1 = oa2 (mod ra)] seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { p5 tx_b tx_r oa2 }
  =
   if Taux.to_int tx_r > 0 then return;
   let lemma aux (p : permutation) (oa2p : seq_voeu)
     requires { p.n = length oa2 }
     requires { oa2p = permut oa2 p }
     requires { q1 tx_b oa2p }
     ensures { lexico_less_or_equal oa2 oa2p }
   =
     let oa1p = permut oa1 p in
     assert { seq_voeu_eq_up_to_rang_appel oa1p oa2p };
     q1_up_to_rang_appel_oa tx_b oa2p oa1p;
     assert { q1 tx_b oa1p };
     assert { lexico_less_or_equal oa1 oa1p };
     if oa1 == oa1p then
       assert { oa2 == oa2p }
     else let i = any (i : int ) ensures { lexico_less_ind oa1 oa1p i } in
      assert { lexico_less_ind oa2 oa2p i}
   in
    ()
end

module P5_Lemmas
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq as CS
  use proofs.lib.permutation.Permutation
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.NbBoursiers
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1 as IQ4_1
  use proofs.ordre_appel.invariants.iq4_2.IQ4_2 as IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3 as IQ4_3
  use proofs.ordre_appel.properties.q1.Q1

  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use P5

  predicate type_ordonne(s : seq_voeu) (t : type_candidat)=
    forall i. 0 <= i < length s -> voeu_lt_than_typed_in_queue s[i] s[i+1..] t

  predicate non_boursiers_ordonnes(s : seq_voeu) =
    forall i j. 0 <= i < j < length s -> est_non_boursier s[i] -> est_non_boursier s[j] -> voeu_lt s[i] s[j]

  predicate boursiers_ordonnes(s : seq_voeu) =
    forall i j. 0 <= i < j < length s -> est_boursier s[i] -> est_boursier s[j] -> voeu_lt s[i] s[j]

  predicate tension_taux_boursier (taux_b : taux) (oa : seq_voeu) (k : int)   =
    (0 <= k <= length oa ) /\
    not (taux_ok taux_b (nb_boursiers oa[..k]) (k+1) )

  let lemma p5_empty (tx_b tx_ds : Taux.t)
    ensures { p5 tx_b tx_ds empty }
  =
    ()

  predicate iq4_1b_loc_nomap (nb_ds : int) (tx_ds : Taux.t) (s : seq_voeu) (i : int) =
     not (IQ4_1.in_Zr nb_ds tx_ds s i) ->
       (forall v. (Seq.seq_contains v s[i+1..]) -> est_boursier v -> voeu_lt s[i] v)

  predicate iq4_1b_nomap (nb_ds : int) (tx_ds : Taux.t) (s : seq_voeu) =
    forall i. 0 <= i < length s -> iq4_1b_loc_nomap nb_ds tx_ds s i

  predicate iq3_0_loc_nomap (oak : seq_voeu) (i : int) =
    voeu_lt_than_typed_in_queue oak[i] oak[i+1..] (get_type_candidat oak[i])

  predicate iq3_0_nomap (oak : seq_voeu) =
    forall i. 0 <= i < length oak -> iq3_0_loc_nomap oak i

  predicate iq3_2_loc_nomap (oak : seq_voeu) (i : int) =
    not est_boursier oak[i] ->
    voeu_lt_than_typed_in_queue oak[i] oak[i+1..] NON_BOURSIER_DU_SECTEUR

  predicate iq3_2_nomap (oak : seq_voeu) =
    forall i. 0 <= i < length oak -> iq3_2_loc_nomap oak i

  predicate iq4_3b_loc_nomap (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (i : int) =
     not (IQ4_3.in_some_Z nb_b nb_ds tx_b tx_ds s i) ->
       (forall v. (Seq.seq_contains v s[i+1..]) -> voeu_lt s[i] v)

  predicate iq4_3b_nomap (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) =
    forall i. 0 <= i < length s -> iq4_3b_loc_nomap nb_b nb_ds tx_b tx_ds s i

  let lemma all_resident_implies_Zr_empty (nb_ds : int) (tx_ds : Taux.t) (s : seq_voeu)
    requires { tx_ds = 0 }
    ensures { forall i. 0 <= i < length s -> not IQ4_1.in_Zr nb_ds tx_ds s i }
  =
    ()

  let lemma iq3_implies_non_boursiers_ordonnes (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (d : seq_voeu)
    requires { tx_ds = 0 }
    requires { iq3_0_nomap d }
    requires { iq3_2_nomap d }
    requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds d }
    ensures { non_boursiers_ordonnes d }
  =
    (
      all_resident_implies_Zr_empty nb_ds tx_ds d;
      let n = length d in
      for i = 0 to n-1 do
        invariant { forall ip j.
            0 <= ip < i
            -> ip < j < n
            -> est_non_boursier d[ip]
            -> est_non_boursier d[j]
            -> voeu_lt d[ip] d[j] }
        if est_non_boursier d[i] then
          for j = i+1 to n-1 do
          invariant { forall j'.
              i < j' < j
              -> est_non_boursier d[j']
              -> voeu_lt d[i] d[j']
          }
          if est_non_boursier d[j] then
            begin

            assert { d[j] = d[i+1..][j-i-1] };
            assert { Seq.seq_contains d[j] d[i+1..] };
            assert { iq3_0_loc_nomap d i };
            assert { iq3_2_loc_nomap d i };
            assert { iq4_3b_loc_nomap nb_b nb_ds tx_b tx_ds d i };
            assert { not (IQ4_1.in_Zr nb_ds tx_ds d i) };
            assert { not (IQ4_2.in_Zb nb_b tx_b d i) };
            assert { voeu_lt d[i] d[j] }
            end
          done
      done
    )

  let lemma iq41b_implies_boursiers_ordonnes (nb_ds : int) (tx_ds : Taux.t) (d : seq_voeu)
    requires { tx_ds = 0 }
    requires { iq4_1b_nomap nb_ds tx_ds d }
    ensures { boursiers_ordonnes d }
  =
    (
      all_resident_implies_Zr_empty nb_ds tx_ds d;
      let n = length d in
      for i = 0 to n-1 do
        invariant { forall ip j.
            0 <= ip < i
            -> ip < j < n
            -> est_boursier d[ip]
            -> est_boursier d[j]
            -> voeu_lt d[ip] d[j] }
        if est_boursier d[i] then
          for j = i+1 to n-1 do
          invariant { forall j'.
              i < j' < j
              -> est_boursier d[j']
              -> voeu_lt d[i] d[j']
          }
          if est_boursier d[j] then
            begin

            assert { d[j] = d[i+1..][j-i-1] };
            assert { Seq.seq_contains d[j] d[i+1..] };
            assert { iq4_1b_loc_nomap nb_ds tx_ds d i };
            assert { not (IQ4_1.in_Zr nb_ds tx_ds d i) };
            assert { voeu_lt d[i] d[j] }
            end
          done
      done
    )

  let lemma oav_sat_p5_rec (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (ordre_appel s : seq_voeu) (p : permutation)
    requires { tx_ds = 0 }
    requires { boursiers_ordonnes ordre_appel }
    requires { non_boursiers_ordonnes ordre_appel }
    requires { all_distincts ordre_appel }
    requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds ordre_appel }
    requires { q1 tx_b ordre_appel }
    requires { length ordre_appel = p.n = length s }
    requires { forall k. 0 <= k < length s -> voeu_eq s[k] ordre_appel[p k] }
    requires { q1 tx_b s }
    ensures  { lexico_less_or_equal ordre_appel s }
  =

    let cl = ordre_appel in
    let  i = first_not_id p in
    assert { forall j. 0<= j < i ->
    	     s[..i][j] = s[j] = cl[p j] = cl[j] = cl[..i][j]};
    assert { forall j. 0<= j < i ->
    	     est_boursier s[..i][j] <-> est_boursier cl[..i][p j] <-> est_boursier cl[..i][j]};
    CS.seq_numof_equiv cl[..i] s[..i] est_boursier;
    assert { nb_boursiers cl[..i] = nb_boursiers s[..i]  };

    if i = p.n then
    begin
      assert { forall j. 0<= j < p.n -> rang s[j] = rang cl[p j] = rang cl[j]};
      assert { lexico_less_ind cl s p.n };
      return
    end;

    let c = cl[i] in
    let bp = nb_boursiers cl[..i] in
    let bs = nb_boursiers cl[i..] in
    assert { nb_boursiers cl = bp + bs };

    let k = (p.map i) in

    (* begin preuve  de i < k *)
    if i >= k then
    begin
      assert { k = p k && p.inv k = k && k = i};
      absurd
    end;
    assert { i < k < length cl };
    (* fin preuve  de i <k *)

    (* preuve rang cl[i] <> rang cl[k] *)
    assert { s[i] = cl[p i] = cl[k] };
    assert { rang cl[i] <> rang cl[k] };
    (* fin preuve rang cl[i] <> rang cl[k] *)

    (* on montre que rang cl[i] < rang s[i]
       cas 1: le taux est contraignant
         1.1 : cl[i..] contient au moins un boursier
         1.2 : cl[i..] ne contient pas de boursier
       cas 2: le taux est non contraignant
     *)

    (* taux contraignant (donc il reste des boursiers dans cl) *)
    if tension_taux_boursier tx_b cl i &&
       not non_boursiers_seulement cl[i..] then
    begin

      if not est_boursier c then
      begin
        assert { not seq_respecte_taux_b tx_b cl[..i+1] };
        assert { q1_loc tx_b cl (i+1) };
        assert { nb_boursiers cl[i..] = nb_boursiers cl[i+1..]};
        carac_non_bour_seulement cl[i+1..];
        assert { not non_boursiers_seulement cl[i+1..] };
        assert { seq_respecte_taux_b tx_b cl[..i+1] };
        absurd;
      end;

      assert { est_boursier c };

      if est_boursier s[i] then
      begin

        assert { est_boursier cl[k] };

        assert { voeu_lt cl[i] cl[k] };
        assert { voeu_lt cl[i] s[i]}
      end else begin
        assert { 0 <= p.inv i < length s };
        assert { s[p.inv i] = cl[ p (p.inv i )] = cl[i] };
        assert { est_boursier s[p.inv i] };
        assert { p.inv i >= i };
        assert { (p.inv i = i) -> (s[i] = s[p (p.inv i)] = cl[i] ) &&
	         est_boursier s[i] };
        assert { p.inv i > i };
        assert { s[p.inv i] = s[i+1..][p.inv i - i - 1] };
        assert { est_boursier s[i+1..][p.inv i - i - 1] };
        assert { not non_boursiers_seulement s[i+1..] };
        assert { not (taux_ok tx_b (nb_boursiers s[..i]) (i+1)) };
        assert { not (taux_ok tx_b (nb_boursiers s[..i+1]) (i+1)) };
        assert { not q1_loc tx_b s (i+1) };
        absurd;
      end;
      assert {voeu_lt cl[i] s[i]}
    end
    else if non_boursiers_seulement cl[i..] then
    begin
      assert { cl[i] = cl[i..][0] };
      assert { est_non_boursier cl[i] };
      assert { cl[k] = cl[i..][k-i] };
      assert { est_non_boursier cl[k] };
      assert { voeu_lt cl[i] cl[k]};
      assert { s[i] = cl[k]};
      assert { voeu_lt cl[i] s[i]}
    end
    else
    (* taux non contraignant donc on a choisit le meilleur candidat point 
     barre***)
    begin
      assert { not tension_taux_boursier tx_b cl i};
      assert { not IQ4_2.in_Zb nb_b tx_b cl i };
      all_resident_implies_Zr_empty nb_ds tx_ds s;
      assert { not IQ4_1.in_Zr nb_ds tx_ds cl i };
      assert { not IQ4_3.in_some_Z nb_b nb_ds tx_b tx_ds cl i };
      assert { i < k < length cl };
      assert { cl[k] = cl[i+1..][k - i - 1] };
      assert { Seq.seq_contains cl[k] cl[i+1..] };
      assert { iq4_3b_loc_nomap nb_b nb_ds tx_b tx_ds cl i };

      assert { voeu_lt cl[i] cl[k]};
      assert { voeu_lt cl[i] s[i]}
    end;

    assert { forall j. 0 <= j < i -> rang s[j] = rang cl[p j] = rang cl[j] };
    assert { lexico_less_ind cl s i }

  (*
   * Un ordre d'appel valide satisfait P5
   *)
  let lemma oav_sat_p5 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (ordre_appel : seq_voeu)
    requires { tx_ds = 0 }
    requires { boursiers_ordonnes ordre_appel }
    requires { non_boursiers_ordonnes ordre_appel }
    requires { all_distincts ordre_appel }
    requires { iq4_3b_nomap nb_b nb_ds tx_b tx_ds ordre_appel }
    requires { q1 tx_b ordre_appel }
    ensures  { p5 tx_b tx_ds ordre_appel }
  =
    let p = any permutation in
    if p.n = (length ordre_appel) then
    begin
      let sp = permut ordre_appel p in
      if (q1 tx_b sp) then
        oav_sat_p5_rec nb_b nb_ds tx_b tx_ds ordre_appel sp p;
    end

  use proofs.ordre_appel.invariants.iq3_0.IQ3_0 as IQ3_0
  use proofs.ordre_appel.invariants.iq3_2.IQ3_2 as IQ3_2
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap

  let lemma iq_nomap_transfers (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (m : EnumMap.t)
    requires {[@expl: p4precond_iq3_0] IQ3_0.iq3_0 s m }
    requires {[@expl: p4precond_iq3_2] IQ3_2.iq3_2 s m }
    requires {[@expl: p4precond_iq4_1b] IQ4_1.iq4_1b nb_ds tx_ds s m }
    requires {[@expl: p4precond_iq4_3b] IQ4_3.iq4_3b nb_b nb_ds tx_b tx_ds s m }
    ensures {[@expl: p4precond_iq3_0] iq3_0_nomap s }
    ensures {[@expl: p4precond_iq3_2] iq3_2_nomap s }
    ensures {[@expl: p4precond_iq4_1b] iq4_1b_nomap nb_ds tx_ds s }
    ensures {[@expl: p4precond_iq4_3b] iq4_3b_nomap nb_b nb_ds tx_b tx_ds s }
  = (
    assert { forall i. 0 <= i < length s -> IQ3_0.iq3_0_loc s m i -> iq3_0_loc_nomap s i };
    assert { iq3_0_nomap s };
    assert { forall i. 0 <= i < length s -> IQ3_2.iq3_2_loc s m i -> iq3_2_loc_nomap s i };
    assert { iq3_2_nomap s };
    assert { forall i. 0 <= i < length s -> IQ4_1.iq4_1b_loc nb_ds tx_ds s m i -> iq4_1b_loc_nomap nb_ds tx_ds s i };
    assert { iq4_1b_nomap nb_ds tx_ds s };
    assert { forall i. 0 <= i < length s -> IQ4_3.iq4_3b_loc nb_b nb_ds tx_b tx_ds s m i -> iq4_3b_loc_nomap nb_b nb_ds tx_b tx_ds s i };
    assert { iq4_3b_nomap nb_b nb_ds tx_b tx_ds s };
    )
end

module P5_Snoc
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.invariants.iq3_0.IQ3_0
  use proofs.ordre_appel.invariants.iq3_2.IQ3_2
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use proofs.ordre_appel.properties.q1.Q1

  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  use P5_Lemmas
  use export P5

  let lemma p5_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oak s : seq_voeu) (m : EnumMap.t) (v : voeu)
    requires {[@expl:pre p5 / s = oak.v] s == snoc oak v }
    requires {[@expl:pre p5 / all_distincts] all_distincts s }
    requires {[@expl:pre p5 / q1] q1 tx_b s }
    requires {[@expl:pre p5 / iq3_0] iq3_0 s m }
    requires {[@expl:pre p5 / iq3_2] iq3_2 s m }
    requires {[@expl:pre p5 / iq4_1b] iq4_1b nb_ds tx_ds s m }
    requires {[@expl:pre p5 / iq4_3b] iq4_3b nb_b nb_ds tx_b tx_ds s m }
    requires {[@expl:pre p5 / p5] p5 tx_b tx_ds  oak }
    ensures { p5 tx_b tx_ds  s }
  =
    iq_nomap_transfers nb_b nb_ds tx_b tx_ds s m;
    if tx_ds.tx = (0:integer) then
      begin
        iq41b_implies_boursiers_ordonnes nb_ds tx_ds s;
        assert { boursiers_ordonnes s };
        iq3_implies_non_boursiers_ordonnes nb_b nb_ds tx_b tx_ds s;
        assert { non_boursiers_ordonnes s };
        oav_sat_p5 nb_b nb_ds tx_b tx_ds s
      end

  let lemma p5_empty (tx_b tx_ds : Taux.t) (oak : seq_voeu)
      requires { oak = empty }
      ensures { p5 tx_b tx_ds oak }
    =
      ()

end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)