module EnumMap
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]
  [@java:visibility:package]

  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.util.Queue as Q
  use mach.java.util.UnmodifiableList as UL
  use ref.Ref

  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.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse

  type t = {
    bds : Q.queue VoeuClasse.t;
    bhs : Q.queue VoeuClasse.t;
    nbds : Q.queue VoeuClasse.t;
    nbhs : Q.queue VoeuClasse.t;
  } invariant { [@expl:map size is integer]
    0 <= Seq.length bds + Seq.length bhs + Seq.length nbds + Seq.length nbhs <= max_integer
  } invariant { [@expl: bds sorted]
    seq_rangs_sorted bds
  } invariant { [@expl: bds well-typed]
    boursiers_du_secteur_seulement bds
  } invariant { [@expl: nbds sorted]
    seq_rangs_sorted nbds
  } invariant { [@expl: nbds well-typed]
    non_boursiers_du_secteur_seulement nbds
  } invariant { [@expl: bhs sorted]
    seq_rangs_sorted bhs
  } invariant { [@expl: bhs well-typed]
    boursiers_hors_secteur_seulement bhs
  } invariant { [@expl: nbhs sorted]
    seq_rangs_sorted nbhs
  } invariant { [@expl: nbhs well-typed ]
    non_boursiers_hors_secteur_seulement nbhs
  } by {
    bds = Q.empty (); bhs = Q.empty (); nbds = Q.empty (); nbhs = Q.empty ();
  }

  let ghost function get_queue (self : t) (x: type_candidat) : (res : seq_voeu)
    ensures { seulement_type res x }
    ensures { seq_rangs_sorted res }
    ensures { match x with
    | BOURSIER_DU_SECTEUR -> res = Q.content self.bds
    | BOURSIER_HORS_SECTEUR -> res = Q.content self.bhs
    | NON_BOURSIER_DU_SECTEUR -> res = Q.content self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> res = Q.content self.nbhs
    end }
  =
    match x with
    | BOURSIER_DU_SECTEUR -> Q.content self.bds
    | BOURSIER_HORS_SECTEUR -> Q.content self.bhs
    | NON_BOURSIER_DU_SECTEUR -> Q.content self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> Q.content self.nbhs
    end

  let ghost function get_queue_of (self : t) (x : VoeuClasse.t) : (q : seq_voeu)
    ensures { forall v. seq_contains v q -> get_type_candidat v = get_type_candidat x }
  =
    let q = get_queue self (get_type_candidat x) in
    assert { seulement_type q (get_type_candidat x) };
    q

  predicate enummap_contains (self : t) (v : VoeuClasse.t) =
    match v.type_candidat with
    | BOURSIER_DU_SECTEUR -> seq_contains v self.bds
    | BOURSIER_HORS_SECTEUR -> seq_contains v self.bhs
    | NON_BOURSIER_DU_SECTEUR -> seq_contains v self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> seq_contains v self.nbhs
    end

  predicate enummap_not_contains (self : t) (v : VoeuClasse.t) =
    match v.type_candidat with
    | BOURSIER_DU_SECTEUR -> not seq_contains v self.bds
    | BOURSIER_HORS_SECTEUR -> not seq_contains v self.bhs
    | NON_BOURSIER_DU_SECTEUR -> not seq_contains v self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> not seq_contains v self.nbhs
    end

  let lemma enummap_not_contains_equiv (self : t) (v : VoeuClasse.t)
    ensures { enummap_not_contains self v <-> not enummap_contains self v }
  = ()

  predicate enummap_is_empty (self : t) =
    self.bds = Seq.empty /\ self.bhs = Seq.empty /\ self.nbds = Seq.empty /\ self.nbhs = Seq.empty

  predicate enummap_queue_is_empty (self : t) (x : type_candidat) =
    match x with
    | BOURSIER_DU_SECTEUR -> self.bds = Seq.empty
    | BOURSIER_HORS_SECTEUR -> self.bhs = Seq.empty
    | NON_BOURSIER_DU_SECTEUR -> self.nbds = Seq.empty
    | NON_BOURSIER_HORS_SECTEUR -> self.nbhs = Seq.empty
    end

  predicate enummap_is_peeked (self : t) (x : type_candidat) (v: VoeuClasse.t) =
    (not enummap_queue_is_empty self x) /\ (v = Seq.get (get_queue self x) 0)

  predicate enummap_v_is_head (self : t) (v : voeu) =
    enummap_is_peeked self (get_type_candidat v) v

  predicate enummap_equals_for_type (m1 m2 : t) (x : type_candidat) =
    match x with
    | BOURSIER_DU_SECTEUR -> m1.bds = m2.bds
    | BOURSIER_HORS_SECTEUR -> m1.bhs = m2.bhs
    | NON_BOURSIER_DU_SECTEUR -> m1.nbds = m2.nbds
    | NON_BOURSIER_HORS_SECTEUR -> m1.nbhs = m2.nbhs
    end

  predicate enummap_equals_except_for_type (m1 m2 : t) (x : type_candidat) =
    match x with
    | BOURSIER_DU_SECTEUR       -> m1.bhs = m2.bhs /\ m1.nbds = m2.nbds /\ m1.nbhs = m2.nbhs
    | BOURSIER_HORS_SECTEUR     -> m1.bds = m2.bds /\ m1.nbds = m2.nbds /\ m1.nbhs = m2.nbhs
    | NON_BOURSIER_DU_SECTEUR   -> m1.bds = m2.bds /\ m1.bhs = m2.bhs /\ m1.nbhs = m2.nbhs
    | NON_BOURSIER_HORS_SECTEUR -> m1.bds = m2.bds /\ m1.bhs = m2.bhs /\ m1.nbds = m2.nbds
    end

  predicate enummap_pop_v (om m : t) (v : VoeuClasse.t) =
    (enummap_equals_except_for_type om m (get_type_candidat v)) &&
    get_queue om (get_type_candidat v) == cons v (get_queue m (get_type_candidat v))

  let enummap [@java:constructor] () : t
    ensures { enummap_is_empty result }
  =
    { bds = Q.empty (); bhs = Q.empty (); nbds = Q.empty (); nbhs = Q.empty (); }

  let function get_nb_voeux_classes (self : t) : integer
    ensures { result = Seq.length self.bds + Seq.length self.bhs + Seq.length self.nbds + Seq.length self.nbhs }
  =
    Q.size self.bds + Q.size self.bhs + Q.size self.nbds + Q.size self.nbhs

  let function get_nb_boursiers (self : t) : integer
    ensures { result = Seq.length (self.bds) + Seq.length (self.bhs) }
  =
    Q.size self.bds + Q.size self.bhs

  let function get_nb_du_secteur (self : t) : integer
    ensures { result = Seq.length (self.bds) + Seq.length (self.nbds) }
  =
    Q.size self.bds + Q.size self.nbds

  let function queue_is_empty (self : t) (x : type_candidat) : bool
    ensures { result = enummap_queue_is_empty self x }
  =
    match x with
    | BOURSIER_DU_SECTEUR -> Q.is_empty self.bds
    | BOURSIER_HORS_SECTEUR -> Q.is_empty self.bhs
    | NON_BOURSIER_DU_SECTEUR -> Q.is_empty self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> Q.is_empty self.nbhs
    end

  let function peek (self : t) (x : type_candidat) : VoeuClasse.t
    requires { [@expl:pre peek / queue no empty] not (queue_is_empty self x) }
    ensures { result = Seq.get (get_queue self x) 0 }
  =
    match x with
    | BOURSIER_DU_SECTEUR -> Q.peek self.bds
    | BOURSIER_HORS_SECTEUR -> Q.peek self.bhs
    | NON_BOURSIER_DU_SECTEUR -> Q.peek self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> Q.peek self.nbhs
    end

  let put (self : t) (v : VoeuClasse.t) : unit
    requires { get_nb_voeux_classes self < max_integer }
    requires { [@expl:pre - v not in map m] not enummap_contains self v }
    requires { [@expl:pre - v is greater its destination queue]
      	       v_is_greater_than_seq (get_queue_of self v) v }
    ensures { get_queue self v.type_candidat == snoc (get_queue (old self) v.type_candidat) v }
    ensures { length (get_queue_of self v) = old (length (get_queue_of self v)) + 1 }
    ensures { forall y. y <> (get_type_candidat v) <-> enummap_equals_for_type self (old self) y }
    ensures { ((get_type_candidat v) <> BOURSIER_HORS_SECTEUR) <->
              enummap_equals_for_type self (old self) BOURSIER_HORS_SECTEUR }
    ensures { ((get_type_candidat v) <> BOURSIER_DU_SECTEUR) <->
       	      enummap_equals_for_type self (old self) BOURSIER_DU_SECTEUR }
    ensures { ((get_type_candidat v) <> NON_BOURSIER_HORS_SECTEUR) <->
       	      enummap_equals_for_type self (old self) NON_BOURSIER_HORS_SECTEUR }
    ensures { ((get_type_candidat v) <> NON_BOURSIER_DU_SECTEUR) <->
              enummap_equals_for_type self (old self) NON_BOURSIER_DU_SECTEUR }
    ensures { enummap_contains self v }
    ensures { seq_contains v (get_queue_of self v) }
    ensures { forall x. x <> v -> (enummap_contains (old self) x <-> enummap_contains self x) }
  =
    match get_type_candidat v with
    | BOURSIER_DU_SECTEUR -> Q.add self.bds v
    | BOURSIER_HORS_SECTEUR -> Q.add self.bhs v
    | NON_BOURSIER_DU_SECTEUR -> Q.add self.nbds v
    | NON_BOURSIER_HORS_SECTEUR -> Q.add self.nbhs v
    end

  let lemma enummap_same_types_in_queues (m : t)
    ensures { forall v. seq_contains v m.bds -> get_type_candidat v = BOURSIER_DU_SECTEUR }
    ensures { forall v. seq_contains v m.bhs -> get_type_candidat v = BOURSIER_HORS_SECTEUR }
    ensures { forall v. seq_contains v m.nbds -> get_type_candidat v = NON_BOURSIER_DU_SECTEUR }
    ensures { forall v. seq_contains v m.nbhs -> get_type_candidat v = NON_BOURSIER_HORS_SECTEUR }
    ensures { forall t: type_candidat. let q = get_queue m t in
                forall v vp. seq_contains v q -> seq_contains vp q -> get_type_candidat v = get_type_candidat vp }
  = ()

  let pop (self : t) (x: type_candidat) : (res : VoeuClasse.t)
    requires { [@expl:pre pop / queue not empty] not (queue_is_empty self x) }
    ensures { (get_queue self x) == (get_queue (old self) x)[1..] }
    ensures { res = (get_queue (old self) x)[0] }
    ensures { res = peek (old self) x }
    ensures { enummap_not_contains self res }
    ensures { forall v. v <> res -> (enummap_contains (old self) v -> enummap_contains self v) }
    ensures { voeu_lt_than_queue res (get_queue self x) }
    ensures { forall v. v <> res -> enummap_contains self v -> enummap_contains (old self) v }
    ensures { forall t. t <> get_type_candidat res -> enummap_equals_for_type self (old self) t }
    ensures { enummap_pop_v (old self) self res }
  =
    enummap_same_types_in_queues self;
    let res = match x with
    | BOURSIER_DU_SECTEUR -> Q.poll self.bds
    | BOURSIER_HORS_SECTEUR -> Q.poll self.bhs
    | NON_BOURSIER_DU_SECTEUR -> Q.poll self.nbds
    | NON_BOURSIER_HORS_SECTEUR -> Q.poll self.nbhs
    end in
    assert { type_candidat res = x };
    assert { (get_queue_of (old self) res) == cons res (get_queue_of self res) };
    assert { forall v. type_candidat v <> type_candidat res -> get_queue_of (old self) v == get_queue_of self v };
    assert { forall v. type_candidat v = type_candidat res -> v <> res ->
               seq_contains v (get_queue_of self res) -> seq_contains v (get_queue_of (old self) res) };
    res

  let lemma enummap_contains_lemma_1 (m : t) (v vv : VoeuClasse.t)
    requires { seq_contains vv (get_queue_of m v) }
    ensures { enummap_contains m vv }
  =
    assert { get_type_candidat v = get_type_candidat vv };
    match get_type_candidat v with
    | BOURSIER_DU_SECTEUR -> assert { seq_contains vv m.bds }
    | BOURSIER_HORS_SECTEUR -> assert { seq_contains vv m.bhs }
    | NON_BOURSIER_DU_SECTEUR -> assert { seq_contains vv m.nbds }
    | NON_BOURSIER_HORS_SECTEUR -> assert { seq_contains vv m.nbhs }
    end

  predicate enummap_in_grp (m : t) (grp : seq_voeu) =
    forall v. enummap_contains m v -> seq_contains v grp

  predicate grp_in_enummap (grp : seq_voeu) (m : t) =
    forall v. seq_contains v grp -> enummap_contains m v

  predicate enummap_eq_grp (m : t) (grp : seq_voeu) =
    forall v. enummap_contains m v <-> seq_contains v grp

  predicate enummap_all_distincts (m : t) =
     forall x y. enummap_contains m x -> enummap_contains m y -> x <> y -> voeu_distinct x y

  let lemma enummap_eq_grp_lemma (g : seq_voeu) (m : t)
    requires { seq_rangs_sorted g }
    requires { forall v. enummap_contains m v -> seq_contains v g }
    requires { forall v. seq_contains v g -> enummap_contains m v }
    ensures { enummap_all_distincts m }
  =
    let lemma aux (x y : VoeuClasse.t)
      requires { enummap_contains m x }
      requires { enummap_contains m y }
      requires { x <> y }
      ensures { voeu_distinct x y }
    =
      if get_rang x = get_rang y then
      begin
        assert { all_distincts g };
        absurd;
      end
    in
      ()

  let from_groupe (grp : UL.ulist VoeuClasse.t) : t
    requires { [@expl:g is ok] seq_groupe_ok grp }
    requires { [@expl:g is sorted] seq_rangs_sorted grp }
    requires { [@expl:g size is integer] 0 <= Seq.length grp <= Integer.max_integer }

    ensures { get_nb_voeux_classes result = Seq.length grp }
    ensures { get_nb_boursiers result = nb_boursiers grp }
    ensures { get_nb_du_secteur result = nb_du_secteur grp }
    ensures { forall v. enummap_contains result v -> seq_contains v grp }
    ensures { forall v. seq_contains v grp -> enummap_contains result v }
    ensures { enummap_eq_grp result grp }
    ensures { enummap_all_distincts result }
    ensures { [@expl:IQ0-1/3] seq_contains_seq grp Seq.empty }
    ensures { [@expl:IQ0-2/3] enummap_in_grp result grp }
    ensures { [@expl:IQ0-3/3] forall i. 0 <= i < length grp -> seq_contains grp[i] Seq.empty \/ enummap_contains result grp[i] }
  =
    let ghost nb_b : ref integer = ref 0 in
    let ghost nb_r : ref integer = ref 0 in

    let res = enummap () in
    let nb_v = UL.size grp in
    for i = 0 to nb_v -1 do
      invariant { get_nb_voeux_classes res = i }
      invariant { [@expl:#R.grp] nb_du_secteur_r grp 0 i = !nb_r }
      invariant { [@expl:#B.grp] nb_boursiers_r grp 0 i = !nb_b }
      invariant { [@expl:#B.res] get_nb_boursiers res = nb_boursiers_r grp 0 i  }
      invariant { [@expl:#R.res] get_nb_du_secteur res = nb_du_secteur_r grp 0 i }
      invariant { [@expl:res in grp] forall v. enummap_contains res v -> seq_contains v grp[..i] }
      invariant { [@expl:grp in res] forall j. 0 <= j < i -> enummap_contains res grp[j] }

      assert { [@expl:v > q] forall j. i <= j < nb_v -> forall v. enummap_contains res v ->  voeu_lt v grp[j] };
      try
        let v = UL.get grp i in
        ghost begin
          if est_boursier v then begin
            nb_b := !nb_b + 1;
          end;
          if est_du_secteur v then
            nb_r := !nb_r + 1;
        end;

        label H in
        assert { forall vv. enummap_contains res vv -> seq_contains vv grp[..i] };
        assert { forall vv. enummap_contains res vv -> voeu_lt vv v };
        assert { forall vv. seq_contains vv (get_queue_of res v) -> enummap_contains res vv };

        put res v;

        assert { grp[..i+1] == snoc grp[..i] v };
  (*
        assert { forall x. enummap_contains res x -> x = v -> seq_contains x grp[..i+1] };
        assert { forall x. x <> v -> (enummap_contains (res at H) x -> enummap_contains res x) };
        assert { forall vp. vp <> v -> enummap_contains res vp -> enummap_contains (res at H) vp ->
                  seq_contains vp grp[..i+1] }
  *)
      with
        IndexOutOfBoundsException.E _ -> absurd
      end
    done;
    res
end

module EnumMap_Props
  use int.Int
  use seq.Seq
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use EnumMap

  predicate enummap_est_boursier (m : EnumMap.t) (v : VoeuClasse.t) =
     enummap_contains m v && est_boursier v

  predicate enummap_est_du_secteur (m : EnumMap.t) (v : VoeuClasse.t) =
     enummap_contains m v && est_du_secteur v

  predicate enummap_remains_boursiers (m : EnumMap.t) =
    EnumMap.get_nb_boursiers m > 0

  predicate enummap_remains_du_secteur (m : EnumMap.t) =
    EnumMap.get_nb_du_secteur m > 0

  let lemma enummap_remains_boursiers_equiv (m : EnumMap.t)
    ensures { enummap_remains_boursiers m <->  (not (m.bds == empty)  || (not m.bhs == empty)) }
  =
    ()

  let lemma enummap_remains_du_secteur_equiv (m : EnumMap.t)
    ensures { enummap_remains_du_secteur m <-> (m.bds <> empty  || m.nbds <> empty) }
  =
    ()
end

module EnumMap_Lemmas
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use EnumMap
  use EnumMap_Props
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  let lemma enummap_equals_for_type_imply_queue_eq (m1 m2 : EnumMap.t) (x : type_candidat)
    requires { enummap_equals_for_type m1 m2 x }
    ensures { (get_queue m1 x) = (get_queue m2 x) }
  =
    ()

  let lemma enummap_non_empty (m : EnumMap.t)
    requires { EnumMap.get_nb_voeux_classes m > 0 }
    ensures { exists v. enummap_contains m v }
  = assert { m.bds <> empty || m.bhs <> empty || m.nbds <> empty || m.nbhs <> empty };
    assert { m.bds <> empty -> exists v. seq_contains v m.bds };
    assert { m.bhs <> empty -> exists v. seq_contains v m.bhs };
    assert { m.nbds <> empty -> exists v. seq_contains v m.nbds };
    assert { m.nbhs <> empty -> exists v. seq_contains v m.nbhs }

  let lemma enummap_pop_imply_size_decrease (om m : EnumMap.t) (v : VoeuClasse.t)
    requires { enummap_pop_v om m v }
    ensures { EnumMap.get_nb_voeux_classes om = EnumMap.get_nb_voeux_classes m + 1 }
  = ()

  let lemma enummap_pop_imply_included (om m : EnumMap.t)
    requires { exists v : VoeuClasse.t. enummap_pop_v om m v }
    ensures { forall v. enummap_contains m v -> enummap_contains om v }
  =
    let lemma enummap_pop_imply_included_aux (v : VoeuClasse.t) (vv :VoeuClasse.t)
      requires { enummap_pop_v om m v }
      requires { enummap_contains m vv }
      ensures { enummap_contains om vv }
    = let q = get_queue om (get_type_candidat v) in
      assert { q == cons v q[1..] };
      assert { get_type_candidat v = get_type_candidat vv -> v <> vv -> seq_contains vv q[1..] };
      assert { get_type_candidat v = get_type_candidat vv -> v <> vv -> seq_contains vv q } in
    ()

  let lemma enummap_pop_v_imply_not_in_m (om m : EnumMap.t) (v : VoeuClasse.t)
    requires { enummap_pop_v om m v }
    ensures { enummap_contains om v }
    ensures { not enummap_contains m v }
  = ()

  let lemma enummap_pop_v_all_eq_except_v (om m : EnumMap.t) (v vv : VoeuClasse.t)
      requires { enummap_pop_v om m v }
      requires { enummap_contains om vv }
      requires { v <> vv }
      ensures { enummap_contains m vv }
    =
      assert { get_type_candidat v = get_type_candidat vv -> v <> vv ->
                seq_contains vv (get_queue m (get_type_candidat v)) }

  let lemma enummap_in_grp_included (m1 m2 : EnumMap.t) (grp : seq_voeu)
     requires { forall v. enummap_contains m1 v -> enummap_contains m2 v }
     requires { enummap_in_grp m2 grp}
     ensures { enummap_in_grp m1 grp}
  =  ()

  let lemma enummap_contains_equiv_seq_contains_q (m : EnumMap.t) (v : VoeuClasse.t)
    ensures { enummap_contains m v -> seq_contains v (get_queue_of m v) }
    ensures { seq_contains v (get_queue_of m v) -> enummap_contains m v }
  = ()

  let lemma enummap_non_empty_imply_exists_head (m : EnumMap.t) : (v : VoeuClasse.t)
    requires { not enummap_is_empty m }
    ensures { enummap_v_is_head m v }
  =
    let t = any type_candidat ensures { get_queue m result <> empty } in
    (get_queue m t)[0]

  let lemma enummap_non_empty_du_secteur (m : EnumMap.t) : (v : VoeuClasse.t)
    requires { enummap_remains_du_secteur m }
    ensures { enummap_v_is_head m v }
    ensures { est_du_secteur v }
  =
    let t = any (t : type_candidat) ensures { type_est_du_secteur t /\ get_queue m t <> empty } in
    (get_queue m t)[0]

  let lemma enummap_non_empty_boursier (m : EnumMap.t) : (v : VoeuClasse.t)
    requires { enummap_remains_boursiers m }
    ensures { enummap_v_is_head m v }
    ensures { est_boursier v }
  =
    let t = any (t : type_candidat) ensures { type_est_boursier t /\ get_queue m t <> empty } in
    (get_queue m t)[0]

  let lemma enummap_head_is_lt_its_queue (m : EnumMap.t) (v h : VoeuClasse.t)
    requires { enummap_v_is_head m h }
    requires { seq_contains v (get_queue m (type_candidat h)) }
    ensures {  v <> h -> voeu_lt h v }
  =
    ()

  let lemma enummap_poped_head_saved (om m : EnumMap.t) (x v h : VoeuClasse.t)
    requires { enummap_pop_v om m x }
    requires { get_type_candidat x <> get_type_candidat v }
    requires { get_type_candidat h = get_type_candidat v }
    requires { enummap_v_is_head om h }
    ensures { enummap_v_is_head m h }
    ensures { seq_contains v (EnumMap.get_queue om (get_type_candidat v)) -> seq_contains v (EnumMap.get_queue m (get_type_candidat h)) }
  =
    ()

end

module AllDistincts
  use int.Int
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use EnumMap

  predicate enummap_all_distincts (m : EnumMap.t) =
     forall x y. enummap_contains m x -> enummap_contains m y -> x <> y ->
       voeu_distinct x y

  predicate enummap_seq_distincts (m : EnumMap.t) (s : seq_voeu) =
    forall x, y. enummap_contains m x -> seq_contains y s -> voeu_distinct x y

  predicate enummap_seq_all_distincts (s : seq_voeu) (m : EnumMap.t) =
      all_distincts s && enummap_all_distincts m && enummap_seq_distincts m s

end

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