🍃 _Set.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Map.

(* @TODO: move these proofs to [Map.v] *)
Section With_Set.
  Context {t : Set}
    (Ord : Compare.COMPARABLE (t := t))
    (S := _Set.Make Ord)
    (compare := Ord.(Compare.COMPARABLE.compare))
    (eqb := (Compare.Make Ord).(Compare.S.op_eq))
    (lt := fun x1 x2 ⇒ (Compare.Make Ord).(Compare.S.op_lt) x1 x2 = true)
    (strictly_sorted_list := Sorting.Sorted.Sorted lt).

  Axiom mem_fold_right_add_eq : ∀ v l,
    strictly_sorted_list l →
    S.(_Set.S.mem) v (List.fold_right S.(_Set.S.add) l S.(_Set.S.empty)) =
    List.mem eqb v l.

  Axiom elements_fold_right_add_eq : ∀ l,
    strictly_sorted_list l →
    S.(_Set.S.elements) (List.fold_right S.(_Set.S.add) l S.(_Set.S.empty)) =
    l.
End With_Set.