module SeqVoeux
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  type voeu = VoeuClasse.t
  type seq_voeu = seq voeu

  function nb_boursiers (s : seq_voeu) : int = seq_numof est_boursier s

  function nb_boursiers_r (s : seq_voeu) (a b : int): int = seq_numof_r est_boursier s a b

  lemma nb_boursiers_positive:
    forall s. nb_boursiers s >= 0

  let lemma nb_boursiers_next (s : seq_voeu) (a b : int)
    requires { 0 <= a <= b < length s }
    requires { est_boursier s[b] }
    ensures { nb_boursiers_r s a (b+1) = (nb_boursiers_r s a b) + 1 }
  = ()

  function nb_residents (s : seq_voeu) : int = seq_numof est_du_secteur s

  function nb_du_secteur (s : seq_voeu) : int = seq_numof est_du_secteur s

  function nb_du_secteur_r (s : seq_voeu) (a b : int): int = seq_numof_r est_du_secteur s a b

  lemma nb_du_secteur_positive:
    forall s. nb_du_secteur s >= 0

  let lemma nb_du_secteur_next (s: seq_voeu) (a b : int)
    requires { 0 <= a <=  b < length s }
    requires { est_du_secteur s[b] }
    ensures { nb_du_secteur_r s a (b + 1) = (nb_du_secteur_r s a b) + 1 }
  =
    ()

  predicate est_boursier_du_secteur (v : voeu) =
    v.type_candidat = BOURSIER_DU_SECTEUR

  function nb_bour_res (s: seq_voeu) : int = seq_numof est_boursier_du_secteur s

  function contient (v : voeu) (s: seq_voeu) : bool = seq_contains v s

  predicate boursiers_du_secteur_seulement (s : seq_voeu) =
    seq_forall est_boursier_du_secteur s

  predicate est_boursier_hors_secteur (v : voeu) =
    v.type_candidat = BOURSIER_HORS_SECTEUR

  predicate boursiers_hors_secteur_seulement (s : seq_voeu) =
    seq_forall est_boursier_hors_secteur s

  predicate est_non_boursier_du_secteur (v : voeu) =
    v.type_candidat = NON_BOURSIER_DU_SECTEUR

  predicate non_boursiers_du_secteur_seulement (s : seq_voeu) =
    seq_forall est_non_boursier_du_secteur s

  predicate est_non_boursier_hors_secteur (v : voeu) =
    v.type_candidat = NON_BOURSIER_HORS_SECTEUR

  predicate non_boursiers_hors_secteur_seulement (s : seq_voeu) =
    seq_forall est_non_boursier_hors_secteur s

  predicate du_secteur_seulement (s : seq_voeu) =
    seq_forall est_du_secteur s

  predicate est_hors_secteur (v : voeu) =
    not est_du_secteur v

  predicate hors_secteur_seulement (s : seq_voeu) =
    seq_forall est_hors_secteur s

  let lemma hors_secteur_seulement_snoc (s : seq_voeu) (v: voeu)
    requires { hors_secteur_seulement s }
    requires { est_hors_secteur v }
    ensures { hors_secteur_seulement (snoc s v) }
  = ()

  predicate boursiers_seulement (s : seq_voeu) =
    seq_forall est_boursier s

  predicate est_non_boursier (v : voeu) =
    not (est_boursier v)

  predicate non_boursiers_seulement (s : seq_voeu) =
    seq_forall est_non_boursier s

  let rec lemma carac_non_bour_seulement (s : seq_voeu)
      ensures { non_boursiers_seulement s -> nb_boursiers s = 0 }
      ensures { nb_boursiers s = 0 -> non_boursiers_seulement s }
      variant { length s }
  = if length s > 0 then
    begin
      carac_non_bour_seulement s[1..];
      assert { non_boursiers_seulement s -> est_non_boursier s[0] };
      assert { nb_boursiers s = 0 -> est_non_boursier s[0] };
    end

  let lemma non_boursiers_seulement_snoc (s : seq_voeu) (x : voeu)
    requires { non_boursiers_seulement s }
    requires { not est_boursier x }
    ensures { non_boursiers_seulement (snoc s x) }
  = ()

  let lemma  non_boursiers_seulement_after_i_snoc (s : seq_voeu) (v : voeu) (i : int)
    requires { 0 <= i <= length s }
    requires {  non_boursiers_seulement s[i..] }
    requires { est_non_boursier v }
    ensures { non_boursiers_seulement (snoc s v)[i..] }
  = ()

  let lemma non_boursiers_seulement_after_i (s : seq_voeu) (i k : int)
    requires { 0 <= i <= k < length s }
    requires { non_boursiers_seulement s[i..] }
    ensures { est_non_boursier s[k] }
  =
    assert { s[k] = s[i..][k-i] }

  let lemma non_boursiers_seulement_suffix_i (s : seq_voeu) (i : int)
    requires { 0 <= i <= length s }
    requires { non_boursiers_seulement s[i..] }
    ensures { forall k. i <= k <= length s -> non_boursiers_seulement s[k..] }
  =
    ()

  predicate seulement_type (s : seq_voeu) (t : type_candidat) =
    match t with
    | BOURSIER_DU_SECTEUR -> boursiers_du_secteur_seulement s
    | BOURSIER_HORS_SECTEUR -> boursiers_hors_secteur_seulement s
    | NON_BOURSIER_DU_SECTEUR -> non_boursiers_du_secteur_seulement s
    | NON_BOURSIER_HORS_SECTEUR -> non_boursiers_hors_secteur_seulement s
    end

  let lemma seulement_type_equiv_type (s : seq_voeu) (t : type_candidat)
    ensures { seulement_type s t <-> forall v. seq_contains v s -> get_type_candidat v = t }
  = ()

  let rec lemma seulement_type_snoc (s : seq_voeu) (v : voeu)
    requires { seulement_type s (get_type_candidat v)}
    ensures { seulement_type (snoc s v) (get_type_candidat v) }
    variant { length s }
  =
    if length s = 0 then
      assert { seulement_type (cons v Seq.empty) (get_type_candidat v) }
    else begin
      assert { seulement_type s (get_type_candidat v) };
      seulement_type_snoc s[1..] v
    end

  predicate remains_boursiers (s : seq_voeu) (total_b : int) =
    0 <= nb_boursiers s < total_b

  let lemma remains_boursiers_snoc (s : seq_voeu) (v: voeu) (total_b : int)
    requires { remains_boursiers (snoc s v) total_b }
    ensures { remains_boursiers s total_b }
  = ()

  let lemma remains_boursiers_prefix (s : seq_voeu) (total_b : int)
    requires { remains_boursiers s total_b }
    ensures { forall k. 0 <= k <= length s -> remains_boursiers s[..k] total_b }
  = ()

  let lemma not_remains_boursiers_snoc (s : seq_voeu) (v: voeu) (total_b : int)
    requires { not remains_boursiers s total_b }
    ensures { not remains_boursiers (snoc s v) total_b }
  = ()

  predicate remains_du_secteur (s : seq_voeu) (total_ds : int) =
    0 <= nb_du_secteur s < total_ds

  let lemma remains_du_secteur_prefix (s : seq_voeu) (total_ds : int)
    requires { remains_du_secteur s total_ds }
    ensures { forall k. 0 <= k <= length s ->
    	      remains_du_secteur s[..k] total_ds }
  = ()

  let lemma nb_du_secteur_app (s1 s2 s3 : seq_voeu)
    requires { s1 == s2 ++ s3 }
    ensures { nb_du_secteur (s1) = nb_du_secteur s2 + nb_du_secteur s3 }
  = ()

  let lemma remains_du_secteur_prefix_loc (s : seq_voeu) (total_ds : int)
      	    			      (i : int)
    requires { 0 <= i <= length s }
    requires { remains_du_secteur s[..i] total_ds }
    ensures { forall k. 0 <= k <= i ->
    	      remains_du_secteur s[..k] total_ds }
  = for k = 0 to i do
      invariant { forall j. 0 <= j < k -> remains_du_secteur s[..j] total_ds }
      nb_du_secteur_app s[..i] s[..k] s[k..i] ;
      assert { nb_du_secteur s[..k] <= nb_du_secteur s[..i] }
    done

  predicate voeu_lt_than_queue (v : voeu) (q : seq_voeu) =
    forall k. 0 <= k < length q -> voeu_lt v q[k]

  predicate voeu_lt_than_typed_in_queue (v : voeu) (s : seq_voeu)
  	    				(t : type_candidat) =
    forall j. 0 <= j < length s -> s[j].type_candidat = t -> voeu_lt v s[j]

  predicate v_is_greater_than_seq (s : seq_voeu) (v : voeu) =
    forall i. 0 <= i < length s -> voeu_lt s[i] v

  let lemma voeu_lt_than_queue_trans (v v': voeu) (q : seq_voeu)
    requires { voeu_lt_than_queue v q }
    requires { voeu_lt v' v }
    ensures { voeu_lt_than_queue v' q }
  = ()

  let lemma voeu_lt_than_queue_cons (v v': voeu) (q : seq_voeu)
    requires { voeu_lt_than_queue v' q }
    requires { voeu_lt v v' }
    ensures { voeu_lt_than_queue v (cons v' q) }
  = ()

  let lemma voeu_lt_than_last_typed_in_queue (s : seq_voeu) (t : type_candidat)
    requires { length s > 0 }
    requires { forall i. 0 <= i < length s - 1 ->
               voeu_lt_than_typed_in_queue s[i] s[i+1..] t }
    ensures { s[length s -1].type_candidat = t ->
  	      forall i. 0 <= i < length s - 1 -> voeu_lt s[i] s[length s -1] }
  =
    let k = length s - 1 in
    let x = s[k] in

    if voeu_has_type x t then
    begin
      for i = 0 to k - 1 do
        invariant { forall j. 0 <= j < i -> voeu_lt s[j] x }
	      assert { s[i+1..][k - i - 1] = x };
      done
    end

  let lemma voeu_lt_than_queue_suffix (s : seq_voeu) (z : VoeuClasse.t)
    requires { voeu_lt_than_queue z s }
    requires { length s > 0 }
    ensures { voeu_lt_than_queue z s[1..] }
  = ()
end

module SeqVoeuxTaux
  use int.Int
  use seq.Seq
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use SeqVoeux

  type taux = Taux.t

  (*
   * Le predicat 'taux_ok' exprime le fait que le nombre de candidats 'nb'
   * d'un type considéré sur le nombre 'total' de candidats est supérieur au
   * 'taux' spécifié. Donc lorsque 'taux' est ok si 'nb' / 'total' >= 'taux'.
   * Le taux étant exprimé par un entier de [0, 100] l'inéquation devient
   * 'nb' / 'total' >= 'taux / 100 c'est-à-dire:
   *)
  predicate taux_ok (taux : taux) (nb: int) (total: int)
    = 100 * nb >= taux * total

  (*
   * Si 'taux_x' est la taux minimum de candidats de type 'x' souhaité. 's' est
   * une liste de candidats, 'count' une fonction de comptage du nombre de 'x'
   * dans 's' et 'total_x' le nombre maximum de candidats existants. 'total_x'
   * n'est pas nécessairement la longueur de 's'.
   *
   * 'taux_x_contraignant' exprime le fait que si on ajoute un nouveau candidat
   * qui n'est pas de type 'x' à 's' (alors qu'il reste des candidats 'x')
   * alors 'taux_x' n'est pas respecté.
   *)
  predicate taux_x_contraignant (taux_x : taux) (s : seq_voeu) (count : seq_voeu -> int) (total_x : int) =
   let nb_x = count s in
     nb_x < total_x && 100 * nb_x < taux_x * (1 + length s)

  (* Spécialisation du taux contraignant pour les boursiers *)
  predicate taux_b_contraignant (taux_b : taux) (s : seq_voeu) (total_b : int) =
    taux_x_contraignant taux_b s nb_boursiers total_b

  (* Spécialisation du taux contraignant pour les residents *)
  predicate taux_ds_contraignant (taux_ds : taux) (s : seq_voeu) (total_ds : int) =
    taux_x_contraignant taux_ds s nb_du_secteur total_ds

  (*
   * Le taux de boursiers et de residents sont en conflit si ils sont tous
   * les deux contraignants.
   *)
  predicate conflit_taux (s : seq_voeu) (taux_b : taux) (total_b : int) (taux_ds : taux) (total_ds : int) =
    taux_b_contraignant taux_b s total_b &&
    taux_ds_contraignant taux_ds s total_ds

  predicate seq_respecte_taux (tx : taux) (s : seq_voeu) (count : seq_voeu -> int) =
    taux_ok tx (count s) (length s)

  predicate seq_respecte_taux_b (tb : taux) (s : seq_voeu) =
    taux_ok tb (nb_boursiers s) (length s)

  predicate seq_respecte_taux_ds (tds : taux) (s : seq_voeu) =
    taux_ok tds (nb_du_secteur s) (length s)

  let lemma seq_respecte_taux_snoc (tx : taux) (s : seq_voeu) (count : seq_voeu -> int) (v : voeu) (k : int)
    requires { 0 <= k <= length s }
    requires { seq_respecte_taux tx (snoc s v)[..k] count }
    ensures { seq_respecte_taux tx s[..k] count }
  = ()

  let lemma seq_respecte_taux_app (s1 s2 : seq_voeu) (taux : taux)
    ensures { (seq_respecte_taux_b taux s1 && seq_respecte_taux_b taux s2) -> seq_respecte_taux_b taux (s1 ++ s2) }
    ensures { (seq_respecte_taux_ds taux s1 && seq_respecte_taux_ds taux s2) -> seq_respecte_taux_ds taux (s1 ++ s2) }
  = ()
end

module SeqVoeuxTauxMinore
  use int.Int
  use seq.Seq
  use seq.FreeMonoid
  use SeqVoeux
  use SeqVoeuxTaux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  (*
   * Le taux minoré est le plus petit des taux taux_r et 1-taux_b' où
   * taux_b' = 1/(1+(1-taux_b)).
   * Il est respecté si au moins un des deux est respecté. Pour taux_b',
   * on utilise l'inégalité:
   * (200 - taux_b)*(nb_ds) >= (100 - tau_b) * total_ds
   *)
  predicate taux_ds_minore_ok (taux_b taux_ds : taux) (nb_ds total : int) =
    taux_ok taux_ds nb_ds total \/
    (200 - taux_b)*(nb_ds) >= (100 - taux_b) * total

  predicate seq_respecte_taux_ds_minore (taux_b taux_ds : taux) (s : seq_voeu) =
    taux_ds_minore_ok taux_b taux_ds (nb_du_secteur s) (length s)

  let lemma seq_respecte_taux_ds_minore_snoc (taux_b taux_ds : taux)
      	    				     (s : seq_voeu) (x : voeu)
    requires { seq_respecte_taux_ds_minore taux_b taux_ds s }
    requires { est_du_secteur x }
    ensures { seq_respecte_taux_ds_minore taux_b taux_ds (snoc s x) }
  = ()

  let lemma seq_respecte_taux_ds_minore_p1 (s : seq_voeu)
      	    				   (taux_b taux_ds : taux)
    requires { seq_respecte_taux_ds_minore taux_b taux_ds s }
    requires { not taux_ok taux_ds (nb_du_secteur s) (length s) }
    ensures { (200 - taux_b)*((nb_du_secteur s)) >= (100 - taux_b) * (length s) }
  = ()

  let lemma seq_respecte_taux_ds_minore_app (s1 s2 : seq_voeu)
      	    				    (taux_b taux_ds : taux)
    ensures { (seq_respecte_taux_ds_minore taux_b taux_ds s1 &&
    	       seq_respecte_taux_ds_minore taux_b taux_ds s2) ->
    	       seq_respecte_taux_ds_minore taux_b taux_ds (s1 ++ s2) }
  = ()

end

module SeqVoeuxDistincts
  use int.Int
  use seq.Seq
  use SeqVoeux
  use mach.java.lang.Integer
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  clone export proofs.lib.distincts.Distincts
  	with type t=voeu, predicate distinct=VoeuClasse_Props.voeu_distinct

  let lemma alld_imp_distinct_ranks (s : seq_voeu)
    requires { all_distincts s }
    ensures { forall i j. 0 <= i < length s -> 0 <= j < length s -> i <> j ->
	             get_rang s[i] <> get_rang s[j] }
  =
    for i = 0 to length s -1 do
      invariant { forall j. 0 <= j < i -> forall k. 0 <= k < i -> k <> j -> get_rang s[k] <> get_rang s[j] }
      for j = 0 to length s - 1 do
        invariant { forall k. 0 <= k < j -> k <> i -> get_rang s[k] <> get_rang s[i] }
        if i <> j then begin
          alld_inst s i j;
          assert { get_rang s[i] <> get_rang s[j] } ;
        end
      done
    done;
    assert { forall i j. 0 <= i < length s -> 0 <= j < length s -> i <> j ->
	           voeu_distinct s[i] s[j] };
    ()
end

module SortedSeqVoeux
  use SeqVoeux
  use seq.Seq
  use proofs.lib.seq.Seq
  use int.Int
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  predicate sorted (s : seq_voeu) =
    seq_forall_two voeu_lt s

  predicate seq_all_lt (s1 s2 : seq_voeu) =
    forall i j: int. 0 <= i < length s1 /\ 0 <= j < length s2
    	   -> voeu_lt s1[i] s2[j]

  let lemma sorted_cons (v : voeu) (s : seq_voeu)
   ensures { (seq_forall (voeu_lt v) s /\ sorted s) <-> sorted (cons v s) }
  = ()

  let lemma sorted_append (s1 s2: seq_voeu)
    ensures { (sorted s1 /\ sorted s2 /\ seq_all_lt s1 s2) <-> sorted (s1 ++ s2) }
  = ()

  let lemma sorted_snoc (v : voeu) (s : seq_voeu)
    ensures { (seq_forall (fun v' -> voeu_lt v' v) s /\ sorted s) <-> sorted (snoc s v) }
  = ()

  let lemma sorted_pop (v : voeu) (s : seq_voeu)
    requires { sorted (cons v s) }
    ensures { not seq_contains v s }
  = ()

end

module NbBoursiers
  use int.Int
  use seq.Seq
  use int.NumOf
  use proofs.lib.seq.Seq
  use SeqVoeux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  function nombre_non_boursiers (s: seq_voeu) : int = seq_numof est_non_boursier s

  let lemma nb_snoc (p : voeu -> bool) (d : seq_voeu) (k : int)
    requires { 0 < k <= length d }
    ensures { seq_numof p d[k-1..k] = if p d[k-1] then 1 else 0 }
    ensures { seq_numof p d[..k] = seq_numof p d[..k-1] +  seq_numof p d[k-1..k] }
    ensures { p d[k-1] -> seq_numof p d[..k] = seq_numof p d[..k-1] +  1 }
    ensures { not (p d[k-1]) -> seq_numof p d[..k] = seq_numof p d[..k-1]  }
  =
    assert { d[..k] == d[..k-1] ++ d[k-1..k] }

  let lemma nb_snoc2 (p : voeu -> bool) (s s' : seq_voeu) (l: int)
    requires { 0 < l <= length s = length s' }
    requires { seq_numof p s[..l-1] = seq_numof p s'[..l-1] }
    requires { p s[l-1] <-> p s'[l-1] }
    ensures { seq_numof p s[..l] = seq_numof p s'[..l] }
  = ()

  let lemma nb_boursiers_snoc (d : seq_voeu) (k : int)
    requires { 0 < k <= length d }
    ensures { nb_boursiers d[k-1..k] = if est_boursier d[k-1] then 1 else 0 }
    ensures { nb_boursiers d[..k]
              = nb_boursiers d[..k-1] +  nb_boursiers d[k-1..k] }
    ensures { est_boursier d[k-1]
              -> nb_boursiers d[..k] = nb_boursiers d[..k-1] +  1 }
    ensures { est_non_boursier d[k-1]
              -> nb_boursiers d[..k] = nb_boursiers d[..k-1]  }
  = nb_snoc est_boursier d k

  let lemma nb_boursiers_eq_snoc (s s' : seq_voeu) (l: int)
    requires { 0 < l <= length s = length s' }
    requires { nb_boursiers s[..l-1] = nb_boursiers s'[..l-1] }
    requires { est_boursier s[l-1] <-> est_boursier s'[l-1] }
    ensures { nb_boursiers s[..l] = nb_boursiers s'[..l] }
  = nb_snoc2 est_boursier s s' l

  (* Invariant 2: si deux candidats sont de même type alors ils sont dans le 
     même ordre dans l'ordre d'appel *)

  let lemma nb_boursiers_pos_implique_existe (s : seq_voeu)
    requires { nb_boursiers s > 0 }
    ensures { exists k. (0 <= k < length s /\ est_boursier s[k]) }
  = ()

  let lemma nb_non_boursiers_snoc (d : seq_voeu) (k : int)
    requires { 0 < k <= length d }
    ensures { nombre_non_boursiers d[k-1..k] =
    	      if est_non_boursier d[k-1] then 1 else 0 }
    ensures { nombre_non_boursiers d[..k] =
              nombre_non_boursiers d[..k-1] + nombre_non_boursiers d[k-1..k] }
    ensures { est_non_boursier d[k-1] ->
              nombre_non_boursiers d[..k] = nombre_non_boursiers d[..k-1] + 1 }
    ensures { est_boursier d[k-1] ->
              nombre_non_boursiers d[..k] = nombre_non_boursiers d[..k-1]  }
  = nb_snoc est_non_boursier d k

  let lemma nombre_non_boursiers_snoc2 (s s' : seq_voeu) (l: int)
    requires { 0 < l <= length s = length s' }
    requires { nombre_non_boursiers s[..l-1] = nombre_non_boursiers s'[..l-1] }
    requires { est_non_boursier s[l-1] <-> est_non_boursier s'[l-1] }
    ensures { nombre_non_boursiers s[..l] = nombre_non_boursiers s'[..l] }
  = nb_snoc2 est_non_boursier s s' l

  let rec lemma nb_boursiers_part (s : seq_voeu) (i : int)
    requires { 0 < i <= length s }
    ensures { i = nb_boursiers s[..i] + nombre_non_boursiers s[..i] }
    variant { i }
  =
    if i > 1 then
      nb_boursiers_part s[..i-1] (i-1)

end

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

  clone export proofs.lib.inversions.Inversions with type t = VoeuClasse.t, predicate lt = voeu_lt
end

module SeqVoeuxGroupe
  use int.Int
  use seq.Seq
  use seq.Distinct
  use seq.Permut
  use mach.java.lang.Integer
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use proofs.lib.seq.Seq
  use SeqVoeux

  predicate seq_field_uniques_loc (s : seq_voeu) (field : VoeuClasse.t -> integer) (k : int) =
    forall i j. 0 <= i < k -> 0 <= j < k -> i <> j -> field s[i] <> field s[j]

  predicate seq_field_ge_x_loc (s : seq_voeu) (field : VoeuClasse.t -> integer) (x : int) (k : int) =
    forall i. 0 <= i < k -> field s[i] >= x

  predicate seq_field_sorted_loc (s : seq_voeu) (field : VoeuClasse.t -> integer) (k : int) =
    forall i j. 0 <= i < j < k -> field s[i] < field s[j]

  predicate seq_rangs_uniques_loc (s : seq_voeu) (k : int) =
    seq_field_uniques_loc s get_rang k

  predicate seq_rangs_ge_1_loc (s : seq_voeu) (k : int) =
    seq_field_ge_x_loc s get_rang 1 k

  predicate seq_rangs_sorted_loc (s : seq_voeu) (k : int) =
    seq_field_sorted_loc s get_rang k

  predicate seq_rangs_appel_uniques_loc (s : seq_voeu) (k : int) =
    seq_field_uniques_loc s get_rang_appel k

  let lemma seq_rangs_appel_uniques_loc_equiv (s : seq_voeu) (k : int)
    requires { seq_rangs_appel_uniques_loc s k }
    ensures { forall i j. 0 <= i < k -> 0 <= j < k -> i <> j -> s[i].rang_appel <> s[j].rang_appel }
  =
    ()

  predicate seq_rangs_appel_ge_1_loc (s : seq_voeu) (k : int) =
    seq_field_ge_x_loc s get_rang_appel 1 k

  predicate seq_rangs_appel_sorted_loc (s : seq_voeu) (k : int) =
    seq_field_sorted_loc s get_rang_appel k

  predicate seq_g_cn_cod_uniques_loc (s : seq_voeu) (k : int) =
    seq_field_uniques_loc s get_g_cn_cod k

  predicate seq_g_cn_cod_ge_0_loc (s : seq_voeu) (k : int) =
    seq_field_ge_x_loc s get_g_cn_cod 0 k

  predicate seq_field_uniques (s : seq_voeu) (field : VoeuClasse.t -> integer) =
    seq_field_uniques_loc s field (length s)

  predicate seq_field_sorted (s : seq_voeu) (field : VoeuClasse.t -> integer) =
    seq_field_sorted_loc s field (length s)

  predicate seq_rangs_uniques (s : seq_voeu) =
    seq_rangs_uniques_loc s (length s)

  predicate seq_rangs_ge_1 (s : seq_voeu) =
    seq_rangs_ge_1_loc s (length s)

  predicate seq_rangs_sorted (s : seq_voeu) =
    seq_rangs_sorted_loc s (length s)

  predicate seq_rangs_appel_uniques (s : seq_voeu) =
    seq_rangs_appel_uniques_loc s (length s)

  predicate seq_rangs_appel_ge_1 (s : seq_voeu) =
    seq_rangs_appel_ge_1_loc s (length s)

  predicate seq_rangs_appel_contiguous (s : seq_voeu) =
    forall i. 0 <= i < length s -> get_rang_appel s[i] = i + 1

  predicate seq_rangs_appel_sorted (s : seq_voeu) =
    seq_rangs_appel_sorted_loc s (length s)

  predicate seq_g_cn_cod_uniques (s : seq_voeu) =
    seq_g_cn_cod_uniques_loc s (length s)

  predicate seq_g_cn_cod_ge_0 (s : seq_voeu) =
    seq_g_cn_cod_ge_0_loc s (length s)

  predicate seq_groupe_ok (g : seq_voeu) =
       distinct g
    /\ Seq.length g < Integer.max_integer
    /\ seq_rangs_uniques g
    /\ seq_rangs_ge_1 g
    /\ seq_rangs_appel_uniques g
    /\ seq_rangs_appel_ge_1 g
    /\ seq_g_cn_cod_ge_0 g
    /\ seq_g_cn_cod_uniques g

  let lemma seq_field_sorted_cons (v : VoeuClasse.t) (s : seq_voeu) (field : VoeuClasse.t -> integer)
    requires { seq_field_sorted s field }
    requires { forall x. seq_contains x s -> field v < field x }
    ensures { seq_field_sorted (cons v s) field }
  =
    ()

  let lemma seq_field_sorted_append (s1 s2: seq_voeu) (field : VoeuClasse.t -> integer)
    requires { seq_field_sorted s1 field }
    requires { seq_field_sorted s2 field }
    requires { forall v1 v2. seq_contains v1 s1 -> seq_contains v2 s2 -> field v1 < field v2 }
    ensures { seq_field_sorted (s1 ++ s2) field }
  =
    ()

  let lemma seq_field_sorted_snoc (v : voeu) (s : seq_voeu) (field : VoeuClasse.t -> integer)
    requires { seq_field_sorted s field }
    requires { forall x. seq_contains x s -> field x < field v }
    ensures { seq_field_sorted (snoc s v) field }
  =
    ()

  let lemma seq_rangs_sorted_snoc (v : voeu) (s : seq_voeu)
    requires { seq_rangs_sorted s }
    requires { v_is_greater_than_seq s v  }
    ensures { seq_rangs_sorted (snoc s v) }
  =
    assert { forall x. seq_contains x s -> get_rang x < get_rang v }

  let lemma seq_field_sorted_pop (v : voeu) (s : seq_voeu) (field : VoeuClasse.t -> integer)
    requires { seq_field_sorted (cons v s) field }
    ensures { not seq_contains v s }
  =
    assert { forall x. seq_contains x s -> field v < field x }

  let lemma seq_rangs_sorted_pop (v : voeu) (s : seq_voeu)
    requires { seq_rangs_sorted (cons v s) }
    ensures { not seq_contains v s }
    ensures { voeu_lt_than_queue v s }
  =
    ()

  let lemma seq_rangs_sorted_suffix_prefix (s: seq_voeu) (i : int)
    requires { 0 <= i < length s }
    requires { seq_rangs_sorted s }
    ensures { seq_rangs_sorted s[..i] }
    ensures { seq_rangs_sorted s[i..] }
  =
    ()

  let lemma seq_rangs_sorted_shift (s: seq_voeu) (i j : int)
    requires { 0 <= i <= j < length s }
    requires { seq_rangs_sorted s }
    ensures { forall v. seq_contains v s[..i] -> get_rang v < get_rang s[j] }
  =
    ()

  let lemma seq_field_uniques_imp_distinct (s : seq_voeu) (field : VoeuClasse.t -> integer)
    requires { seq_field_uniques_loc s field (length s) }
    ensures { seq_distinct s }
  =
    for i = 0 to length s -1 do
      invariant { forall j k. 0 <= j < i -> 0 <= k < i -> k <> j -> s[j] <> s[k] }
      for j = 0 to length s - 1 do
        invariant { forall k. 0 <= k < j -> k <> i -> s[k] <> s[i] }
        if j = i then continue;
        assert { s[j] = s[i] -> field s[j] = field s[i] };
      done
    done

  let lemma seq_rangs_sorted_imp_distinct (s : seq_voeu)
    requires { seq_rangs_sorted s }
    ensures { seq_distinct s }
  =
    assert { seq_rangs_uniques s }

  let lemma seq_rangs_appel_sorted_imp_distinct (s : seq_voeu)
    requires { seq_rangs_appel_sorted s }
    ensures { seq_distinct s }
  =
    assert { seq_rangs_appel_uniques s }

  let rec lemma seq_rangs_appel_sorted_permut (s1 s2 : seq_voeu)
    requires { seq_rangs_appel_sorted s1 }
    requires { permut_all s1 s2 }
    requires { seq_rangs_appel_sorted s2 }
    ensures { s1 == s2 }
    variant { length s1 }
  =
    if length s1 = 0 then return;
    let j = any (j : int) ensures { 0 <= j < length s2 && s2[j] = s1[0] } in
    if j <> 0 then
    begin
      let i = any (i : int) ensures { 0 <= i < j < length s1 && s1[i] = s2[0] } in
      assert { get_rang_appel s1[i] = get_rang_appel s2[0] < get_rang_appel s2[j] = get_rang_appel s1[0] };
      absurd;
    end;
    seq_rangs_appel_sorted_permut s1[1..] s2[1..]

  let lemma seq_field_uniques_permut (s1 s2 : seq_voeu) (field : VoeuClasse.t -> integer)
    requires { permut_all s1 s2 }
    requires { seq_field_uniques s1 field }
    ensures { seq_field_uniques s2 field }
  =
    ()

  let lemma list_voeu_classe_groupe_ok (g1 g2 : seq_voeu)
    requires { seq_groupe_ok g1 }
    requires { permut_all g1 g2 }
    ensures { seq_groupe_ok g2 }
  =
    assert { seq_rangs_uniques g2 };
    assert { seq_rangs_ge_1 g2 };
    assert { seq_g_cn_cod_ge_0 g2 };
    assert { seq_g_cn_cod_uniques g2 };

  use SeqVoeuxDistincts

  let lemma seq_rangs_uniques_imp_distinct (s : seq_voeu)
    requires { seq_rangs_uniques s }
    ensures { all_distincts s }
  =
    ()
end

module SeqVoeuxEqUpToRangAppel
  use int.Int
  use seq.Seq
  use seq.Distinct
  use seq.Permut
  use proofs.lib.seq.Seq
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use SeqVoeuxGroupe
  use SeqVoeuxTaux
  use SeqVoeux

  predicate seq_voeu_eq_up_to_rang_appel (s1 s2 : seq_voeu) =
    length s1 = length s2 &&
    forall i. 0 <= i < length s1 -> voeux_classes_eq_up_to_rang_appel s1[i] s2[i]

  let lemma seq_voeu_eq_up_to_rang_appel_groupe_ok (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    requires { seq_groupe_ok s1 }
    requires { seq_rangs_appel_uniques s2 }
    requires { seq_rangs_appel_ge_1 s2 }
    ensures { seq_groupe_ok s2 }
  =
    assert { seq_rangs_uniques s2 };
    assert { seq_rangs_ge_1 s2 };
    assert { seq_g_cn_cod_ge_0 s2 };
    assert { seq_g_cn_cod_uniques s2 }

  let lemma seq_voeu_eq_up_to_rang_appel_props1 (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { forall k. 0 <= k <= length s1 -> nb_boursiers s1[..k] = nb_boursiers s2[..k] }
    ensures { nb_boursiers s1 = nb_boursiers s2 }
  =
    seq_numof_eq_prefix s1 s2 est_boursier;
    seq_numof_equiv s1 s2 est_boursier

  let lemma seq_voeu_eq_up_to_rang_appel_props2 (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { forall k. 0 <= k <= length s1 -> nb_du_secteur s1[..k] = nb_du_secteur s2[..k] }
    ensures { nb_du_secteur s1 = nb_du_secteur s2 }
  =
    seq_numof_eq_prefix s1 s2 est_du_secteur;
    seq_numof_equiv s1 s2 est_du_secteur

  let lemma seq_voeu_eq_up_to_rang_appel_props3 (tx : Taux.t) (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { forall k. 0 <= k <= length s1 -> seq_respecte_taux_b tx s1[..k] = seq_respecte_taux_b tx s2[..k] }
  =
    seq_voeu_eq_up_to_rang_appel_props1 s1 s2;
    assert { forall k. 0 <= k <= length s1 -> nb_boursiers s1[..k] = nb_boursiers s2[..k] };
    assert { forall k. 0 <= k <= length s1 -> taux_ok tx (nb_boursiers s1[..k]) k = taux_ok tx (nb_boursiers s2[..k]) k }

 let lemma seq_voeu_eq_up_to_rang_appel_props4 (tx : Taux.t) (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { forall k. 0 <= k <= length s1 -> seq_respecte_taux_ds tx s1[..k] = seq_respecte_taux_ds tx s2[..k] }
  =
    seq_voeu_eq_up_to_rang_appel_props2 s1 s2

 let lemma seq_voeu_eq_up_to_rang_appel_props5  (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { forall k. 0 <= k < length s1 -> non_boursiers_seulement s1[k..] = non_boursiers_seulement s2[k..] }
  =
    seq_forall_eq_suffix s1 s2 est_non_boursier

 let lemma seq_voeu_eq_up_to_rang_appel_props6 (s1 s2 : seq_voeu)
    requires { seq_voeu_eq_up_to_rang_appel s1 s2 }
    ensures { forall k. 0 <= k < length s1 -> hors_secteur_seulement s1[k..] = hors_secteur_seulement s2[k..] }
  =
    seq_forall_eq_suffix s1 s2 est_hors_secteur

  predicate seq_voeu_permut_up_to_rang_appel (s1 s2 : seq_voeu) =
    exists s1p. permut_all s1 s1p && seq_voeu_eq_up_to_rang_appel s1p s2

  let lemma seq_voeu_rangs_sorted_eq_up_to_rang_appel (op1 oa op2 : seq_voeu)
    requires { [@expl:op1 sorted] seq_rangs_sorted op1 }
    requires { [@expl:op1 = oa (mod ra)] seq_voeu_permut_up_to_rang_appel op1 oa }
    requires { [@expl:oa permut op2] permut_all oa op2 }
    requires { [@expl:op1 sorted] seq_rangs_sorted op2 }
    ensures { [@expl:op1 = op2 (mod ra)] seq_voeu_eq_up_to_rang_appel op1 op2 }
  =
    let lemma aux1 (i : int) : (k : int)
      requires { 0 <= i < length op2 }
      ensures { 0 <= k < length op1 }
      ensures { voeux_classes_eq_up_to_rang_appel op1[k] op2[i] }
    =
      let j = any (j : int) ensures { 0 <= j < length oa && oa[j] = op2[i] } in
      let op1p = any (op1p : seq_voeu) ensures { permut_all op1 op1p && seq_voeu_eq_up_to_rang_appel op1p oa } in
      let k = any (k : int) ensures { 0 <= k < length op1 && op1[k] = op1p[j] } in
      k
    in
    let lemma aux2 (k : int) : (i : int)
      requires { 0 <= k < length op1 }
      ensures { 0 <= i < length op2 }
      ensures { voeux_classes_eq_up_to_rang_appel op1[k] op2[i] }
    =
      let op1p = any (op1p : seq_voeu) ensures { permut_all op1 op1p && seq_voeu_eq_up_to_rang_appel op1p oa } in
      let j = any (j : int) ensures { 0 <= j < length op1 && op1[k] = op1p[j] } in
      let i = any (i : int) ensures { 0 <= i < length oa && oa[j] = op2[i] } in
      i
    in
    for i = 0 to length op1 - 1 do
      invariant { forall k. 0 <= k < i -> voeux_classes_eq_up_to_rang_appel op1[k] op2[k] }
      let k = aux1 i in
      assert { voeux_classes_eq_up_to_rang_appel op1[k] op2[i] };

      if k = i then
        continue;

      if k < i then
        assert { voeux_classes_eq_up_to_rang_appel op1[k] op2[k] }
      else if i < k then begin
        let j = aux2 i in
        assert { j = i };
      end;
      absurd
    done

end

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