module IQ0
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  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.voeu_classe.VoeuClasse

  (*
   * L'ordre d'appel courant (oak) et les files d'attentes (m) contiennent
   * exactement les mêmes voeux que le groupe de classement (g)
   *)
  predicate iq0 (g : seq_voeu) (oak : seq_voeu) (m : EnumMap.t) =
    (* oak ++ m est inclus dans g *)
    seq_contains_seq g oak && enummap_in_grp m g &&
    (* g est inclus dans oak ++ m *)
    forall i. 0 <= i < length g -> seq_contains g[i] oak \/ enummap_contains m g[i]

end

module IQ0_Lemmas
  use int.Int
  use seq.Seq
  use seq.Occ
  use seq.Permut
  use mach.java.lang.Integer
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use IQ0

  let lemma iq0_m_empty (op oak : seq_voeu) (m : EnumMap.t)
    requires { length op = length oak }
    requires { seq_groupe_ok op }
    requires { all_distincts oak }
    requires { iq0 op oak m }
    requires { EnumMap.get_nb_voeux_classes m = 0 }
    ensures { permut_all op oak }
  =
    let nb_voeux = length op in
    assert { forall i. 0 <= i < nb_voeux -> occ_all oak[i] oak = 1 };
    assert { forall i. 0 <= i < nb_voeux -> occ_all op[i] op = 1 };
    assert { seq_contains_seq op oak };
    assert { seq_contains_seq oak op };
    assert { forall v. seq_contains v op -> seq_contains v oak };
    assert { forall v. not seq_contains v op -> not seq_contains v oak};
    assert { forall v. seq_contains v op ->  occ_all v op = 1 = occ_all v oak };
    assert { forall v. not seq_contains v op -> occ_all v op = 0 = occ_all v oak };

end

module IQ0_Snoc
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  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.enum_map.EnumMap_Lemmas
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use export IQ0

  let lemma iq0_snoc (op oak : seq_voeu) (om m : EnumMap.t) (x : VoeuClasse.t)
   requires {[@expl:x selected] enummap_pop_v om m x }
   requires {[@expl:iq0] iq0 op oak om }
   ensures { iq0 op (snoc oak x) m }
  =
    assert { enummap_contains om x };
    assert { seq_contains_seq op (snoc oak x) };
    enummap_pop_imply_included om m;
    enummap_in_grp_included m om op;

    let s = snoc oak x in
    let nb_c = length op in
    for i = 0 to nb_c - 1 do
      invariant { forall j : integer. 0 <= j < i -> (seq_contains op[j] s \/ enummap_contains m op[j]) }
      assert { seq_contains op[i] oak \/ enummap_contains om op[i] };
      if voeu_eq op[i] x then
        assert { seq_contains op[i] s }
      else if enummap_contains om op[i] then begin
        assert { enummap_contains m op[i] };
      end else
        assert { seq_contains op[i] s };
    done

  let lemma iq0_empty (op : seq_voeu) (m : EnumMap.t)
    requires { enummap_eq_grp m op }
    ensures { iq0 op Seq.empty m }
  = ()

end

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