Parcoursup / Calcul de l'ordre d'appel des candidats index


Propriété 4

Comparé au classement pédagogique, l'ordre d'appel minimise le nombre d'inversions (distance de Kendall-tau), parmi ceux qui garantissent la première propriété.

module P4
  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.SeqVoeuxInversions
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.properties.q1.Q1

  predicate p4 (tx_b tx_r : Taux.t) (s : seq_voeu) =
    tx_r = 0 ->
      forall p : permutation.
        length s = p.n ->
          let sp = permut s p in
            q1 tx_b sp -> nb_inversions s <= nb_inversions sp
end

Minimalité du nombre d'inversions parmi les permutations de voeux ayant la propriété 1.

module P4_UpToRangAppel
  use int.Int
  use seq.Seq
  use proofs.lib.pair.Pair
  use proofs.lib.permutation.Permutation
  use proofs.lib.sum2d.Sum2d
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxInversions
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  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
  use proofs.ordre_appel.properties.q1.Q1_UpToRangAppel
  use proofs.ordre_appel.properties.p5.P5_UpToRangAppel

  use export P4

  let rec lemma nb_inversions_up_to_rang_appel (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { nb_inversions s1 = nb_inversions s2 }
    variant { length s1 }
  =
    let n = length s1 in
    if n <= 1 then return;
    assert { forall p. inversions_count s1 p = inversions_count s2 p };
    assert { sum2d (inversions_count s1) n n = sum2d (inversions_count s2) n n }

  let lemma p4_up_to_rang_appel_oa (tx_b tx_r : Taux.t) (oa1 oa2 : seq_voeu)
    requires { p4 tx_b tx_r oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { p4 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 { nb_inversions oa2 <= nb_inversions 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 };
      ()
    in
    ()

end

module P4_Lemmas
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.lib.permutation.Permutation
  use proofs.lib.permutation.Swap
  use proofs.lib.sum2d.SumBasics
  use proofs.lib.pair.Pair
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.seq_voeux.SeqVoeuxInversions
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.seq_voeux.NbBoursiers
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use proofs.ordre_appel.properties.q1.Q1
  use proofs.ordre_appel.properties.p5.P5_Lemmas

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

  use P4

Preuve de la propriété 4

  (*
   * Le nombre d'inversion est positif.
   *)
  let lemma nb_inv_pos (d : seq_voeu)
    ensures { nb_inversions d >= 0 }
  =
    ()

  (*
   * Pas d'inversion pour un sequence vide ou un singleton.
   *)
  let lemma nb_inv_small (d : seq_voeu)
    requires { length d <= 1 }
    ensures { nb_inversions d = 0 }
  =
  ()

  (*
   * Le swap d'une inversion diminue le nombre total d'inversions.
   * Prouvé dans le module Inversions.
   * Egalement prouvé en Coq.
   *)
  let lemma p4_dec_inv (s : seq_voeu) (i j : int)
    requires { 0 <= i < j < length s }
    requires { voeu_lt s[j] s[i] }
    ensures { nb_inversions (swap s (mkp i j)) < nb_inversions s }
  =
    inversions_dec s (mkp i j)

  (*
   * Effet de 'swap' sur le nombre de boursiers dans un préfixe de longueur 'k'.
   *)
  let lemma swap_nb_boursiers (d : seq_voeu) (i j k : int)
    requires { 0 <= i < j < length d }
    requires { 0 <= k <= length d }
    ensures {
      let d' = (swap d (mkp i j)) in
      if i < k <= j then
        let x = (if est_boursier d[i] then 1 else 0) in
        let y = (if est_boursier d[j] then 1 else 0) in
         nb_boursiers d[..k] = nb_boursiers d'[..k] + x - y
      else
         nb_boursiers d[..k] = nb_boursiers d'[..k]
    }
  =
    let d' = (swap d (mkp i j)) in
    let x = (nb_boursiers d[i..i+1]) in
    let y = (nb_boursiers d[j..j+1]) in
    for l = 0 to k-1 do
      invariant { forall k'. 0 <= k' <= l ->
        if i < k' <= j then
          nb_boursiers d[..k'] = nb_boursiers d'[..k'] + x - y
        else
          nb_boursiers d[..k'] = nb_boursiers d'[..k']
      }
      begin
       let dk = nb_boursiers d[..l] - nb_boursiers d'[..l] in
       let dk1 = nb_boursiers d[..l+1] - nb_boursiers d'[..l+1] in
       let xk = nb_boursiers d[l..l+1] in
       let yk = nb_boursiers d'[l..l+1] in
         assert { dk1 = dk + xk - yk };
         assert { l <> i /\ l <> j -> xk = yk };
         assert { l <> i /\ l <> j -> dk1 = dk };
         assert { l = i -> (dk = 0) /\ dk1 = x - y};
         assert { l = j -> (dk = (x - y)) /\ dk1 = (x - y) + (y - x) = 0 };
      end
    done

  let lemma nbs_helper (s : seq_voeu) (k  :int)
    requires { 0 <= k < length s }
    requires { non_boursiers_seulement s[k..] }
    ensures { est_non_boursier s[k] }
    ensures { non_boursiers_seulement s[k+1..] }
    =(
    assert { s[k] = s[k..][0]  }
    )

  let lemma nbs_helper2 (s : seq_voeu) (k  :int)
    requires { 0 <= k < length s }
    requires { est_non_boursier s[k] }
    requires { non_boursiers_seulement s[k+1..] }
    ensures { non_boursiers_seulement s[k..] }
    =(
    )

  (*
   * 'swap' préserve le nombre de non-boursiers sur un suffixe ne contenant
   * que des non boursiers.
   *)
  let rec lemma swap_preserve_non_boursiers  (s : seq_voeu) (i j k : int)
    requires { 0 <= i < j < length s }
    requires { est_boursier s[i] -> est_boursier s[j] }
    requires { 0 <= k < length s }
    requires { non_boursiers_seulement s[k..] }
    ensures { non_boursiers_seulement (swap s (mkp i j))[k..] }
    variant { length s - k }
  =
    let sp = (swap s (mkp i j)) in
    if k < length s - 1 then
      swap_preserve_non_boursiers s i j (k+1);
    (* induction hypothesis *)
    assert { non_boursiers_seulement sp[k+1..] };
    nbs_helper s k;
    assert { non_boursiers_seulement s[k+1..] };
    (* induction step *)
    if k <> i && k <> j then
    begin
      assert { sp[k] = s[k] };
      nbs_helper s k;
      assert { est_non_boursier s[k] };
    end
    else if k = i then
    begin
      assert { sp[k] = s[k..][j-k] };
      assert { est_non_boursier s[k..][j-k] };
    end
    else (* k = j *)
    begin
      assert { sp[k] = s[i] };
      assert { est_non_boursier sp[k] };
    end;
    assert { est_non_boursier sp[k] };
    nbs_helper2 sp k

  (*
   * 'swap' préserve Q1
   *)
  let function taux_ok (taux_p: int) (nb_p: int) (nb_total: int)
    = 100 * nb_p >= taux_p * nb_total

  let lemma swap_preserve_q1  (tx_b: Taux.t) (s : seq_voeu) (i j k: int)
    requires { 0 <= i < j < length s }
    requires { 0 <= k < length s }
    requires { q1_loc tx_b s k }
    requires { est_boursier s[i] -> est_boursier s[j]}
    ensures { q1_loc tx_b (swap s (mkp i j)) k }
  =
    let sp = (swap s (mkp i j)) in
    if non_boursiers_seulement s[k..] then
    begin
      swap_preserve_non_boursiers s i j k;
      assert { non_boursiers_seulement sp[k..] };
    end
    else
      swap_nb_boursiers s i j k

  (*
   * Si les types de voeux correspondent deux à deux dans d et d'
   * alors 'non_boursiers_seulement' a la même valeur pour les deux séquences.
   *)
  let rec lemma meme_non_boursiers_seulement (d d' : seq_voeu) (l : int)
    requires { 0 <= l <= length d = length d'}
    requires { forall k. l <= k < length d -> est_boursier d[k] <-> est_boursier d'[k] }
    ensures { non_boursiers_seulement d[l..] = non_boursiers_seulement d'[l..] }
    variant { length d - l }
  =
    if l < length d then
    begin
      meme_non_boursiers_seulement d d' (l+1);
      assert { est_non_boursier d[l] <-> est_non_boursier d'[l] }
    end

  (*
   * Si deux séquences sont égales elles respectent toutes les deux Q1.
   *)
  let lemma meme_q1 (tx_b : Taux.t) (d d' : seq_voeu)
    requires { length d = length d'}
    requires { forall k. 0 <= k < length d -> d[k] = d'[k] }
    ensures { q1 tx_b d = q1 tx_b d'}
  = assert { d == d' }

  (*
   * Si deux séquences sont égales elles ont le même nombre d'inversions.
   *)
  let lemma meme_nb_inversions (d d' : seq_voeu)
    requires { length d = length d'}
    requires { d == d' }
    ensures { nb_inversions d = nb_inversions d' }
  = ()

  (*
   * 'swap' et 'transposition' ont le même effet.
   *)
  let lemma swap_carac  (s : seq_voeu) (i j : int)
    requires { 0 <= i < j < length s }
    ensures {
      let n = length s in
      let t = transposition n i j in
      let d' = permut s t in
      let dij = (swap s (mkp i j)) in
        d' == dij
    }
  =
    (
      let n = length s in
      let t = transposition n i j in
      let d' = permut s t in
      let dij = (swap s (mkp i j)) in
      for k = 0 to n-1 do
      invariant { forall k'. 0<= k' < k -> d'[k'] = dij[k'] }
      ()

      done
    )

    let lemma swap_carac2  (s : seq_voeu) (p : permutation) (i j : int)
    requires { 0 <= i < j < p.n }
    requires { p.n = length s }
    ensures {
      let p' = compose (transposition p.n i j) p in
      let d' = permut s p' in
      let dij = (swap (permut s p) (mkp i j)) in
        d' == dij
    }
  = (swap_carac (permut s p) i j)

  (*
   * Si on application 'p' à l'ordre d'appel alors Q1 est maintenue.
   *)
  predicate satisfait_q1 (tx_b : Taux.t) (ordre_appel: seq_voeu) (p : permutation) =
    let d = (permut ordre_appel p) in
      p.n = length ordre_appel /\ q1 tx_b d

  (*
   * La séquence 'd' est équitable pour les voeux 'i' et 'j'
   *)
  predicate is_fair_loc_seq (d: seq_voeu) (i j: int) =
    (i < j && voeu_lt d[j] d[i]) -> (est_boursier d[i] && est_non_boursier d[j])

  (*
   * La permutation 'p' de l'ordre d'appel 'oa' est équitable pour 'i' et 'j'
   *)
  predicate is_fair_loc (d: seq_voeu) (p: permutation) (i j: int) =
    let d' = (permut d p) in is_fair_loc_seq d' i j

  predicate is_fair (d : seq_voeu) =
    forall i j. 0 <= i < j < length d -> is_fair_loc_seq d i j

  predicate satq1_and_is_fair (tx_b : Taux.t) (d : seq_voeu) (p: permutation) =
    satisfait_q1 tx_b d p
    /\ let d' = (permut d p) in is_fair d'

  (*
   * Si 'p' est une permutation de l'ordre d'appel qui satisfait Q1 mais qui
   * n'est pas équitable pour les candidats 'i' et 'j' alors
   * il existe une autre permutation de l'ordre d'appel qui satisfait Q1
   * mais qui contient moins d'inversions que 'p'. Il suffit de composer 'p'
   * la permutation qui échange 'i' et 'j'.
   *)
  let lemma loc_improve (tx_b : Taux.t) (ordre_appel : seq_voeu) (p : permutation) (i j : int) : permutation
    requires { 0 <= i < j < p.n }
    requires { p.n = length ordre_appel }
    requires { satisfait_q1 tx_b ordre_appel p }
    requires { not is_fair_loc ordre_appel p i j }
    ensures { satisfait_q1 tx_b ordre_appel result }
    ensures { nb_inversions (permut ordre_appel result) < nb_inversions (permut ordre_appel p)}
  =
    let ooa = ordre_appel in
    let d = (permut ooa p) in
    let dij = (swap d (mkp i j)) in
    let result = compose (transposition p.n i j) p in

    (* preuve de satisfait_q1 oa result *)
    for k = 0 to length d - 1 do
      invariant { forall k'. 0<= k' <= k -> q1_loc tx_b dij k' }
      swap_preserve_q1 tx_b d i j k
    done;
    assert { q1 tx_b dij };
    swap_carac2 ooa p i j;

    let d' = permut ooa result in
    assert { dij == d'};
    assert { satisfait_q1 tx_b ooa result };
    (* le nombre d'inversion diminue *)
    assert { voeu_lt d[j] d[i] };
    p4_dec_inv d i j;
    swap_carac2 ooa p i j;
    assert { nb_inversions (permut ooa result) = nb_inversions dij < nb_inversions d  = nb_inversions d };
    result

  let rec lemma q1_ordering_rec (tx_b : Taux.t) (oa: seq_voeu) (p : permutation) (i j : int) : permutation
    requires { satisfait_q1 tx_b oa p }
    requires { 0 <= i < j < p.n }
    requires {
      forall i' j'.
         0 <= i' < j' < p.n
        -> ((i' < i) \/ (i' = i /\ j' < j))
        -> is_fair_loc oa p i' j'
    }
    ensures { satq1_and_is_fair tx_b oa result }
    ensures { nb_inversions (permut oa result) <= nb_inversions (permut oa p) }
    variant { nb_inversions (permut oa p), p.n - i, p.n - j }
  =
    if not is_fair_loc oa p i j  then
      let p' = loc_improve tx_b oa p i j in
        q1_ordering_rec tx_b oa p' 0 1
    else if j < (p.n - 1) then
      q1_ordering_rec tx_b oa p i (j + 1)
    else if i < (p.n - 2) then
      q1_ordering_rec tx_b oa p (i + 1) (i + 2)
    else
      p

(* 
   * Etant donnée une permutation 'p' de l'ordre d'appel qui satisfait Q1
   * il existe une permutation satisfaisant Q1, avec moins d'inversions et 
   * qui satisfait la condition d'équité boursier/non-boursier.
   *)
  predicate q1_ordering_p (tx_b : Taux.t) (oa: seq_voeu) (p pr: permutation) =
    satq1_and_is_fair tx_b oa pr &&
    nb_inversions (permut oa pr) <= nb_inversions (permut oa p)

  let lemma q1_ordering (tx_b : Taux.t) (oa: seq_voeu) (p : permutation) : permutation
    requires { satisfait_q1 tx_b oa p }
    requires { p.n > 1 }
    ensures { satq1_and_is_fair tx_b oa result }
    ensures { nb_inversions (permut oa result) <= nb_inversions (permut oa p) }
    ensures { q1_ordering_p tx_b oa p result }
  =
    q1_ordering_rec tx_b oa p 0 1

  let lemma meme_nombre_boursier_avant_id (d : seq_voeu) (p : permutation)
      (k : int)
     requires { 0 <= k  < length d}
     requires { p.n = length d }
     requires { k = first_not_id p }
     ensures { let d' = permut d p in nb_boursiers d[..k] = nb_boursiers d'[..k] }
  =
    let d' = permut d p in
    for l = 0 to k -1 do
       invariant { nb_boursiers d[..l] = nb_boursiers d'[..l] }

       assert { d[l] = d[p l] = d'[l] };
       assert { est_boursier d[l] <-> est_boursier d'[l] };
       assert { nb_boursiers d[l..l+1]
                = (if est_boursier d[l] then 1 else 0)
		            = (if est_boursier d'[l] then 1 else 0)
		            = nb_boursiers d'[l..l+1] };
       nb_boursiers_eq_snoc d d' (l+1);
       assert { nb_boursiers d[..l+1] = nb_boursiers d'[..l+1] }
    done;
    assert { nb_boursiers d[..k] = nb_boursiers d'[..k] }

  let lemma perm_preserves_all_distincts (d : seq_voeu) (p: permutation)
     requires { all_distincts d }
     requires { length d  = p.n }
     ensures { let d'= permut d p in all_distincts d' }
  =(
  let n = length d in
  let d'= permut d p in
  assert { forall i j.
        0 <= i < n
        -> 0 <= j < n
        -> i <> j
        ->
        ((p i) <> (p j)
        && (voeu_distinct d[p i] d[p j])
        && (voeu_distinct d'[i] d'[j ]))}
    )

  let lemma inZb_implies_tension (nb_b : int) (tx_b : Taux.t) (d : seq_voeu) (k : int)
    requires { 0 <= k < length d }
    requires { IQ4_2.in_Zb nb_b tx_b d k }
    ensures  { tension_taux_boursier tx_b d k  }
   = ()

  let lemma q1_loc_permut (d : seq_voeu) (tx_b : taux) (p: permutation)
   requires { length d = p.n }
   requires { q1_loc tx_b d p.n }
   ensures  { q1_loc tx_b (permut d p) p.n}
   =()

  let lemma equiv_seq (d : seq_voeu)
   ensures  { d == d[..length d] }
   = ()

  (*
   * Preuve de minimalité de l'ordre d'appel par rapport aux permutations 
   * satisfaisant Q1
   *)

  let lemma p4_rec_case_0 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa: seq_voeu) (p0: permutation)
    requires { tx_ds = 0 }
    requires { all_distincts oa }
    requires { non_boursiers_ordonnes oa }
    requires { q1 tx_b oa }
    requires { iq4_3b_nomap nb_b  nb_ds tx_b tx_ds oa }
    requires { is_fair oa }
    requires { satisfait_q1 tx_b oa p0 }
    requires { length oa <= 1 }
    ensures  { nb_inversions oa <= nb_inversions (permut oa p0) }
  =
    nb_inv_small oa;
    nb_inv_pos (permut oa p0)

  let lemma p4_rec_case_1 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (d d': seq_voeu) (p0 p: permutation)
    requires { tx_ds = 0 }
    requires { all_distincts d }
    requires { non_boursiers_ordonnes d }
    requires { q1 tx_b d }
    requires { iq4_3b_nomap nb_b  nb_ds tx_b tx_ds d }
    requires { is_fair d }
    requires { satisfait_q1 tx_b d p0 }
    requires { length d > 1 }
    requires { q1_ordering_p tx_b d p0 p }
    requires { d' = permut d p }
    requires { length d = first_not_id p }
    ensures  { nb_inversions d <= nb_inversions (permut d p0) }
  =
    meme_nb_inversions d d'

  let lemma p4_rec_case_2_1_n_2_2 (nb_b nb_ds nb k : int) (tx_b tx_ds : Taux.t) (d d': seq_voeu) (p0 p: permutation)
    requires { tx_ds = 0 }
    requires { all_distincts d }
    requires { non_boursiers_ordonnes d }
    requires { q1 tx_b d }
    requires { iq4_3b_nomap nb_b  nb_ds tx_b tx_ds d }
    requires { is_fair d }
    requires { satisfait_q1 tx_b d p0 }
    requires { nb = length d > 1 }
    requires { q1_ordering_p tx_b d p0 p }
    requires { d' = permut d p }
    requires { k = first_not_id p }
    requires { k <> nb }
    ensures { not same_type d[k] d'[k] }
    ensures { not est_boursier d[k] }
  =
    let c = d[k] in
    let c' = d'[k] in
    let k0' = (p.inv k) in
    let k0 = (p.map k) in

    assert { (k < k0' < nb) /\ (c = d[k] = d[p k0'] = d'[k0']) };
    assert { is_fair_loc_seq d' k k0' };

    assert { (k < k0 < nb) /\ (c' = d'[k] = d'[p.inv k0] = d[k0]) };
    assert { is_fair_loc_seq d k k0 };

    if same_type c c' then
      begin
        (* puisque d et d' sont équitables *)
        assert { voeu_lt c c' /\ voeu_lt c' c };
        absurd
      end;

    (* Cas 2.2: si c est boursier, il y a contradiction de Q1 par d' *)
    if est_boursier c then
      begin
        (* la condition d'équité sur d' implique (car c' non boursier) *)
        assert { rang c' < rang c };

        (* le boursier c est plus loin que c' dans d' *)
        assert { est_boursier d'[k+1..][k0' - (k + 1)] };
        assert { not non_boursiers_seulement d'[k+1..] };

        (* d'après Q1 sur d' le taux est ok *)
        assert { [@expl:accel] satisfait_q1 tx_b d p };
        assert { q1_loc tx_b d' (k+1) };
        assert { nb_boursiers d'[..k+1] = nb_boursiers d'[..k] };
        assert { taux_ok tx_b (nb_boursiers d'[..k]) (k+1) };

        (* c a doublé c' donc d'après prop 1 sur d tension sur le taux *)
        assert { iq4_3b_loc_nomap nb_b nb_ds tx_b tx_ds d k };
        assert { c' = d[k0] = d[k+1..][k0 - k - 1] };
        assert { Seq.seq_contains c' d[k+1..] };
        assert { voeu_lt c' d[k]  };
        assert { IQ4_3.in_some_Z nb_b nb_ds tx_b tx_ds d k };
        all_resident_implies_Zr_empty nb_ds tx_ds d;
        assert { not IQ4_1.in_Zr nb_ds tx_ds d k };
        assert { IQ4_2.in_Zb nb_b tx_b d k };
        inZb_implies_tension nb_b tx_b d k;
        assert { tension_taux_boursier tx_b d k  };
        assert { not taux_ok tx_b (nb_boursiers d[..k]) (k+1) };
        assert { nb_boursiers d[..k] = nb_boursiers d'[..k] };
        assert { not taux_ok tx_b (nb_boursiers d'[..k]) (k+1) };
        absurd
      end

  let lemma p4_rec_case_2_3_a (nb_b nb_ds nb k k0 k0' : int) (tx_b tx_ds : Taux.t) (d d' d'': seq_voeu) (p0 p: permutation)
    requires { tx_ds = 0 }
    requires { all_distincts d }
    requires { non_boursiers_ordonnes d }
    requires { q1 tx_b d }
    requires { iq4_3b_nomap nb_b  nb_ds tx_b tx_ds d }
    requires { is_fair d }
    requires { satisfait_q1 tx_b d p0 }
    requires { nb = length d > 1 }
    requires { q1_ordering_p tx_b d p0 p }
    requires { d' = permut d p }
    requires { k = first_not_id p }
    requires { k <> nb }
    requires { not same_type d[k] d'[k] }
    requires { not est_boursier d[k] }
    requires { d'' = (swap d' (mkp k k0')) }
    requires { k0' = (p.inv k) }
    requires { k0 = (p.map k) }
    ensures { nb_boursiers d[..k] = nb_boursiers d''[..k] = nb_boursiers d'[..k] }
    ensures {forall l. 0 <= l < k -> q1_loc tx_b d'' l }
  =
     let c = d[k] in
     let c' = d'[k] in
     assert { (k < k0' < nb) /\ (c = d[k] = d[p k0'] = d'[k0']) };
     assert { is_fair_loc_seq d' k k0' };

     assert { (k < k0 < nb) /\ (c' = d'[k] = d'[p.inv k0] = d[k0]) };
     assert { is_fair_loc_seq d k k0 };

     for l = 0 to k-1 do
          invariant { forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' }
          invariant { nb_boursiers d[..l]
                      = nb_boursiers d''[..l]
                      = nb_boursiers d'[..l] }
        assert { est_boursier d'[l..][k-l] };
        assert { c' = d'[l..][k - l] };
        assert { not est_non_boursier d'[l..][k - l] };
        assert { not non_boursiers_seulement d'[l..] };

Q1 pour d' **

        assert { satisfait_q1 tx_b d p };
        assert { q1_loc tx_b d' l };
        assert { taux_ok tx_b (nb_boursiers d'[..l]) l };
        assert { taux_ok tx_b (nb_boursiers d''[..l]) l };
        assert { q1_loc tx_b d'' l };
        assert { d[l] = d[p l] = d'[l] = (swap d' (mkp k k0'))[l] = d''[l] };
        assert { same_type d'[l]  d''[l] };
        nb_boursiers_eq_snoc d' d'' (l+1);
        nb_boursiers_eq_snoc d d' (l+1);
        assert { nb_boursiers d[..l+1] = nb_boursiers d'[..l+1]
                 = nb_boursiers d''[..l+1] };
     done

  let rec lemma p4_rec (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa: seq_voeu) (p0: permutation)
    requires { tx_ds = 0 }
    requires { all_distincts oa }
    requires { non_boursiers_ordonnes oa }
    requires { q1 tx_b oa }
    requires { iq4_3b_nomap nb_b  nb_ds tx_b tx_ds oa }
    requires { is_fair oa }
    requires { satisfait_q1 tx_b oa p0 }
    ensures  { nb_inversions oa <= nb_inversions (permut oa p0) }
    variant { nb_inversions (permut oa p0) }
  =
    let tx_b = tx_b in
    let nb = length oa in
    let d = oa in

    (* Cas 0: pas de voeux ou 1 seul *)
    if nb <= 1 then
      return;

    let p = q1_ordering tx_b oa p0 in
    let d'= permut d p in
    let k = first_not_id p in

    (* Cas 1: p est la permutation identité *)
    if k = nb  then
      return;

    (* Cas 2: p n'est pas l'identité
       k est l'indice du premier swap dans p. On compare les candidats/voeux, 
       c et c', en k dans d et d'. Trois cas à étudier:
       1) si les candidats sont de même type, il y a contradiction de la 
          condition d'équité
       2) si c est boursier (et c' non boursier) alors il y a contradiction de Q1 
          dans d'
       3) c est non boursier (et c' boursier) alors on pourrait faire un swap
     *)
    let c = d[k] in
    let c' = d'[k] in
    let k0' = (p.inv k) in
    let k0 = (p.map k) in

    assert { (k < k0' < nb) /\ (c = d[k] = d[p k0'] = d'[k0']) };
    assert { is_fair_loc_seq d' k k0' };

    assert { (k < k0 < nb) /\ (c' = d'[k] = d'[p.inv k0] = d[k0]) };
    assert { is_fair_loc_seq d k k0 };

    (* Cas 2.1: les deux voeux sont de même type. *)
    (* Cas 2.2: si c est boursier, il y a contradiction de Q1 par d' *)
    if same_type c c' || est_boursier c then
      absurd;

    (* Cas 2.3: d' a réduit son nombre d'inversions en faisant remonter
                prématurément un boursier.
       mais alors on pourrait échanger c et c' dans d' et faire moins
       d'inversions en contredisant la minimalité de d' tout en conservant la
       propriete 1 au niveau du nombre de boursiers.

       sur 0..k    d'' a comme d
       en k+1..k0' d'' au taquet
       en k0'+1..n d'' a comme d'
     *)
    assert {[@expl:comment] est_non_boursier c /\ est_boursier c' };

todo assert {[@expl:oav inv] non_boursier_mieux_classe_que_suivants d k k0 };**

    assert { rang c < rang c' };
    let d'' = (swap d' (mkp k k0')) in

    (* d'' satisfait Q1 sur [0,k[ *)
    for l = 0 to k-1 do
         invariant { forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' }
         invariant { nb_boursiers d[..l]
                     = nb_boursiers d''[..l]
                     = nb_boursiers d'[..l] }
       assert { est_boursier d'[l..][k-l] };
       assert { c' = d'[l..][k - l] };
       assert { not est_non_boursier d'[l..][k - l] };
       assert { not non_boursiers_seulement d'[l..] };

Q1 pour d' **

       assert { satisfait_q1 tx_b oa p };
       assert { q1_loc tx_b d' l };
       assert { taux_ok tx_b (nb_boursiers d'[..l]) l };
       assert { taux_ok tx_b (nb_boursiers d''[..l]) l };
       assert { q1_loc tx_b d'' l };
       assert { d[l] = d[p l] = d'[l] = (swap d' (mkp k k0'))[l] = d''[l] };
       assert { same_type d'[l]  d''[l] };
       nb_boursiers_eq_snoc d' d'' (l+1);
       nb_boursiers_eq_snoc d d' (l+1);
       assert { nb_boursiers d[..l+1] = nb_boursiers d'[..l+1]
                = nb_boursiers d''[..l+1] };
    done;
    (* fin preuve d'' satisfies Q1 on [0, k[ *)
    assert { nb_boursiers d[..k] = nb_boursiers d''[..k]
     	     = nb_boursiers d'[..k] };
    assert { forall l. 0 <= l < k -> q1_loc tx_b d'' l };

    (* d'' satisfies Q1 on [k, k0'[ *)
    assert { nb_boursiers d''[..k+1] = nb_boursiers d[..k+1] };

    assert { q1_loc tx_b d (k+1) };
    assert { est_boursier d[k0] };
    assert { d[k0] = d[k+1..][k0 - (k+1)] };
    assert { not est_non_boursier d[k+1..][k0 - (k+1)] };
    assert { not non_boursiers_seulement d[k+1..] };
    assert { seq_respecte_taux_b tx_b d[..k+1] };
    assert { taux_ok tx_b (nb_boursiers d[..k+1]) (k+1) };
    assert { taux_ok tx_b (nb_boursiers d''[..k+1]) (k+1) };
    assert { seq_respecte_taux_b tx_b d''[..k] };
    assert { q1_loc tx_b d'' k };
    for l = k + 1 to k0' -1 do
      invariant { nb_boursiers d''[..l] = nb_boursiers d[..k] + (l - k - 1) }
      invariant { forall l'. k+1 <= l' < l -> taux_ok tx_b (nb_boursiers d''[..l']) l' }
      invariant { forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' }
      if est_non_boursier d'[l] then
      begin
        assert {[@expl: post_cond_of_q1_ordering] let oa' = (permut oa p) in is_fair oa' };
    	    assert { is_fair_loc oa p l k0' };
    	    assert { is_fair_loc_seq d' l k0' };
    	    assert { not voeu_lt d'[k0'] d'[l] };
        	perm_preserves_all_distincts d p;
        	assert { voeu_lt d'[l] d'[k0'] };
    	    assert { d'[l] = d[p l] by d'= permut d p };
    	    assert { d'[k0'] = d[k] };
    	    assert { voeu_lt d[p l] d[k] };

Q1 pour d **

    	    assert { forall i. 0 <= i < k -> p i = i };
    	    let l' = (p.map l) in
    	    assert { 0 <= l < p.n };
    	    assert { in_range p.n p.map };
    	    assert { l' < p.n };
        	assert { est_non_boursier d[k]};
    	    assert { d[l'] = d[p l] = d'[l] };
    	    assert { est_non_boursier d[l'] };
        	assert { k < l' };
        assert { non_boursiers_ordonnes d };
    	    assert { p.n = length d };
    	    assert { 0 <= k < l' < p.n = length d };
    	    assert {voeu_lt d[k] d[l'] };
    	    absurd;
      end;
      assert { est_boursier d'[l] };
      assert { est_boursier d''[l] };
      assert {
      	  nb_boursiers d''[..l+1]
          = nb_boursiers d''[..l] + nb_boursiers d''[l..l+1]
          = nb_boursiers d''[..l] + 1
      };
     assert {
         100 * (nb_boursiers d''[..l+1])
	      = 100 * nb_boursiers d''[..l] + 100
	      >= tx_b + tx_b * l = tx_b * (l+1) };
	   assert { seq_respecte_taux_b tx_b d''[..l]};
     assert { q1_loc tx_b d'' l };
    done;
   (* fin preuve d'' satisfies Q1 on [k, k0'[ *)

   (* d'' satisfait Q1 sur [k0',length d[ *)
   assert { [@expl: init inv1]
          forall l'. 0 <= l' < k0' -> q1_loc tx_b d'' l' };
   assert { [@expl: init inv1]
          seq_respecte_taux_b tx_b d''[..k0'] };
   assert { [@expl: init inv1]
          q1_loc tx_b d'' k0' };
   for l = k0' + 1 to nb - 1  do
     invariant { [@expl: inv1 q1 sur [k0',l[] forall l'. 0 <= l' < l -> q1_loc tx_b d'' l' }
     invariant { nb_boursiers d'[..l] = nb_boursiers d''[..l] }
     assert {  l<>k && l <> k0' };
     assert { d''[l] = (swap d' (mkp k k0'))[l] = d'[l] };
     assert { d'[l] = d''[l] };
     if non_boursiers_seulement d'[l..] then
     begin
       assert { [@precond2 meme_non_boursiers_seulement]
            forall l'. l <= l' < length d
            -> (l'<>k && l' <> k0') && (d'[l'] = d''[l'])};
       meme_non_boursiers_seulement d' d'' l;
       assert { non_boursiers_seulement d''[l..] };
       assert { q1_loc tx_b d'' l };
     end else begin
       assert { q1 tx_b d'};
       assert { q1_loc tx_b d' l };
       assert { seq_respecte_taux_b tx_b d'[..l] };
       assert { taux_ok tx_b (nb_boursiers d'[..l]) l };
       swap_nb_boursiers d' k k0' l;
       assert { nb_boursiers d'[l..l+1] = nb_boursiers d''[l..l+1]};
       assert { nb_boursiers d'[..l+1]
       	      = nb_boursiers d'[..l]  + nb_boursiers d'[l..l+1]
              = nb_boursiers d''[..l]  + nb_boursiers d''[l..l+1]
              = nb_boursiers d''[..l+1] };
       assert { taux_ok tx_b (nb_boursiers d''[..l]) l };
       assert { q1_loc tx_b d'' l };
     end;
     assert { q1_loc tx_b d'' l };
   done;
   (* fin preuve d'' satisfait Q1 dur [k0',length d[ *)

   assert { forall l. 0 <= l < length d''  -> q1_loc tx_b d'' l };
   assert { length d = length d' = length d'' = nb };
   assert { q1_loc tx_b d nb };
   q1_loc_permut d tx_b p;
   assert { q1_loc tx_b d' nb };
   let t = (transposition nb k k0' ) in
   let d''' = permut d' t in
   swap_carac d' k k0';
   assert { d'' == d'''};
   q1_loc_permut d' tx_b t ;
   assert { q1 tx_b d''' };
   assert { q1 tx_b d'' };

   (*equiv_seq d';
   equiv_seq d''; *)
   assert { nb_boursiers d'[..nb] = nb_boursiers d' = nb_boursiers d'' = nb_boursiers d''[..nb] };
   (*assert { seq_respecte_taux_b tx_b d''[..nb] };*)
   assert { q1_loc tx_b d'' nb };
   assert { q1 tx_b d'' };
   assert { nb_inversions d'' < nb_inversions d' } ;

   let p'' = (compose (transposition nb k k0') p) in
   swap_carac2 oa p k k0';
   assert { nb_inversions (permut oa p'') = nb_inversions d'' };
   meme_q1 tx_b d'' (permut d p'');
   assert { satisfait_q1 tx_b oa p''};
   p4_rec nb_b nb_ds tx_b tx_ds oa p''

  let lemma iq4_1b_implies_fair (nb_ds : int) (tx_ds : Taux.t) (d: seq_voeu)
    requires { tx_ds = 0 }
    requires { non_boursiers_ordonnes d }
    requires { iq4_1b_nomap nb_ds tx_ds d }
    ensures { is_fair d }
    =
    (
      P5_Lemmas.all_resident_implies_Zr_empty nb_ds tx_ds d;
      let n = length d in
      for i = 0 to n-1 do
        invariant { forall i' j.
            0 <= i' < i
            -> i' < j < n
            -> is_fair_loc_seq d i' j }
        for j = i+1 to n-1 do
        invariant { forall j'. i < j' < j -> is_fair_loc_seq d i j' }
        begin
          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
         else if est_non_boursier d[i] then

            assert { voeu_lt d[i] d[j] }
         end
        done
      done
    )

  (*
   * Un ordre d'appel valide satisfait P4
   *)
  let lemma oa_sat_p4 (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oa: seq_voeu)
    requires { tx_ds = 0 }
    requires { all_distincts oa }
    requires { non_boursiers_ordonnes oa }
    requires { q1 tx_b oa }
    requires { iq4_1b_nomap nb_ds tx_ds oa}
    requires { iq4_3b_nomap nb_b  nb_ds tx_b tx_ds oa }
    ensures { forall p : permutation. satisfait_q1 tx_b oa p -> nb_inversions oa <= nb_inversions (permut oa p) }
  =
    iq4_1b_implies_fair nb_ds tx_ds oa;
    let p = any permutation in
    if satisfait_q1 tx_b oa p then
       p4_rec nb_b nb_ds tx_b tx_ds oa p

end

module P4_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_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use proofs.ordre_appel.properties.q1.Q1
  use proofs.ordre_appel.properties.p5.P5_Lemmas

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

  use P4_Lemmas
  use export P4

  let lemma p4_snoc (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oak s : seq_voeu) (m :EnumMap.t) (v : voeu)
    requires {[@expl:pre p4 / s = oak.v] s == snoc oak v }
    requires {[@expl:pre p4 / all_distincts s] all_distincts s }
    requires {[@expl:pre p4 / q1] q1 tx_b s }
    requires {[@expl:pre p4 / iq3_0] iq3_0 s m }
    requires {[@expl:pre p4 / iq3_2] iq3_2 s m }
    requires {[@expl:pre p4 / iq4_1b] iq4_1b nb_ds tx_ds s m }
    requires {[@expl:pre p4 / iq4_3b] iq4_3b nb_b nb_ds tx_b tx_ds s m }
    requires {[@expl:pre p4 / p4] p4 tx_b tx_ds oak }
    ensures { p4 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 };
        oa_sat_p4 nb_b nb_ds tx_b tx_ds s
      end

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

end

(* generated on Thu Jan 30 02:06:23 UTC 2025 from rev:  *)

Generated by why3doc 1.7.2+git