module IQ6
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  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 fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  predicate iq6_loc (s : seq_voeu) (m : EnumMap.t) (k : int) =
    forall i. 0 <= i < k ->
      forall v. (enummap_contains m v ->  voeu_lt s[i] v) && (seq_contains v s[i+1..] -> voeu_lt s[i] v)

  predicate iq6 (tx_b tx_ds : Taux.t) (s : seq_voeu) (m : EnumMap.t) =
    tx_b = 0 -> tx_ds = 0 -> iq6_loc s m (length s)
end

module IQ6_Lemmas
  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.seq_voeux.SortedSeqVoeux
  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 fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use IQ6

  let lemma taux_zeros_imp_taux_non_contraignants (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu)
    requires { tx_b = 0 && tx_ds = 0 }
    ensures { not taux_b_contraignant tx_b s nb_b }
    ensures { not taux_ds_contraignant tx_ds s nb_ds }
  = ()

  let lemma iq6_loc_ex (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (s : seq_voeu) (m : EnumMap.t) (k : int)
    requires { tx_b = 0 && tx_ds = 0 }
    requires { forall i. 0 <= i <= k -> not in_some_Z nb_b nb_ds tx_b tx_ds 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_ds tx_b tx_ds s i
                -> forall v. seq_contains v s[i+1..] -> voeu_lt s[i] v }
    ensures { iq6_loc s m k }
  =
    assert { forall i. 0 <= i <= k -> not in_Zb nb_b tx_b s i };
    assert { forall i. 0 <= i <= k -> not in_Zr nb_ds tx_ds s i }

  let lemma iq6_imp_sorted (tx_b tx_ds : Taux.t) (s : seq_voeu) (m : EnumMap.t)
    requires { iq6 tx_b tx_ds s m }
    requires { tx_b = 0 && tx_ds = 0 }
    ensures { sorted s }
  =
    for i = 0 to length s - 1 do
      invariant { forall j. 0 <= j < i -> forall k. j < k < length s -> voeu_lt s[j] s[k] }
      assert { iq6_loc s m i };
      assert { forall v. seq_contains v s[i+1..] -> voeu_lt s[i] v };
      assert { forall k. i < k < length s -> s[k] = s[i+1..][k-i-1] };
    done
end

module IQ6_Snoc
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux

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

  use IQ6_Lemmas
  use export IQ6

  let lemma iq6_snoc (cB cR : bool) (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (oak : seq_voeu) (om m : EnumMap.t) (x : voeu)
   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_ds oak nb_ds }
   requires {[@expl:pre iq6] iq6 tx_b tx_ds oak om }
   requires {[@expl:pre iq4_3] iq4_3 nb_b nb_ds tx_b tx_ds (snoc oak x) m }

   ensures  { iq6 tx_b tx_ds (snoc oak x) m }
  =
    if not (tx_b.tx = (0:integer) && tx_ds.tx = (0:integer)) then
      return;
    assert { not cB && not cR };
    let s = snoc oak x in
    for k = 0 to length s - 1 do
      invariant { forall j. 0 <= j <= k -> iq6_loc s m j }
      assert { forall i. 0 <= i <= k -> not in_some_Z nb_b nb_ds tx_b tx_ds s i };
      assert { iq4_3b_loc  nb_b nb_ds tx_b tx_ds s m k };
      iq6_loc_ex nb_b nb_ds tx_b tx_ds s m k;
    done;
    assert { iq6_loc s m (length s) }

(*
  let lemma iq6_empty (g :GroupeClassementValide.t) (oak : seq_voeu) (m : EnumMap.t)
    requires { oak = empty }
    ensures { iq6 g oak m }
  =
    ()
*)
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)