Library mcertikos.clib.ZSet

Require Import Coqlib.

Require Import MSets.
Require Import MSetList.

Module Z_OWL <: OrderedTypeWithLeibniz.
  Definition t := Z.
  Definition eq := @eq t.

  Instance eq_equiv : Equivalence (@eq) := eq_equivalence.
  Definition lt := Z.lt.
  Instance lt_strorder : StrictOrder Z.lt := Z.lt_strorder.
  Instance lt_compat : Proper (eq ==> eq ==> iff) lt := Z.lt_wd.

  Definition compare := Zcompare.
  Definition compare_spec := Zcompare_spec.
  Definition eq_dec := zeq.
  Definition eq_leibniz a b (H:eq a b) := H.
End Z_OWL.
Module ZSet := MakeWithLeibniz Z_OWL.

Lemma not_eq_true : ∀ b,
   b = false ↔ ¬ b = true.
Proof.
  destruct b; split; auto; try tauto; inversion 1.
Qed.

Lemma ZSet_mem_empty: ∀ i, ZSet.mem i ZSet.empty = false.
Proof.
  intros i.
  rewrite not_eq_true.
  rewrite ZSet.mem_spec.
  apply ZSet.empty_spec.
Qed.

Lemma ZSet_mem_spec_false : ∀ x s, ZSet.mem x s = false ↔ ¬ZSet.In x s.
Proof.
  intros.
  rewrite <- ZSet.mem_spec.
  destruct (ZSet.mem x s); split; intros; congruence.
Qed.

Lemma ZSet_mem_remove : ∀ x s, (ZSet.mem x (ZSet.remove x s)) = false.
  intros.
  assert (¬ ZSet.mem x (ZSet.remove x s) = true).
  {
    rewrite ZSet.mem_spec.
    rewrite ZSet.remove_spec.
    tauto.
  }
  destruct (ZSet.mem x (ZSet.remove x s)); tauto.
Qed.

Lemma ZSet_add_commute : ∀ x y s,
    ZSet.add x (ZSet.add y s) = ZSet.add y (ZSet.add x s).
Proof.
  intros.
  apply ZSet.eq_leibniz.
  unfold ZSet.eq.
  unfold ZSet.Equal.
  intros z.
  repeat rewrite ZSet.add_spec.
  tauto.
Qed.

Lemma ZSet_gss : ∀ x s, (ZSet.mem x (ZSet.add x s)) = true.
  intros.
  rewrite ZSet.mem_spec.
  rewrite ZSet.add_spec.
  tauto.
Qed.

Lemma ZSet_gso : ∀ x y s, x≠y → (ZSet.mem x (ZSet.add y s)) = (ZSet.mem x s).
  intros.
  cut (ZSet.mem x (ZSet.add y s) = true ↔ ZSet.mem x s = true).
  {
    destruct (ZSet.mem x (ZSet.add y s)); destruct (ZSet.mem x s); intuition.
  }

  rewrite ZSet.mem_spec.
  rewrite ZSet.add_spec.
  rewrite ZSet.mem_spec.
  intuition.
Qed.

Lemma ZSet_remove_add_empty
  : ∀ x, (ZSet.remove x (ZSet.add x ZSet.empty)) = ZSet.empty.
Proof.
  intros.
  apply ZSet.eq_leibniz.
  unfold ZSet.eq.
  unfold ZSet.Equal.
  intros y.
  rewrite ZSet.remove_spec.
  rewrite ZSet.add_spec.
  intuition.
    apply ZSet.empty_spec in H. auto.
Qed.

Lemma ZSet_remove_gso : ∀ i j s,
  i ≠ j →
  ZSet.mem i (ZSet.remove j s) = ZSet.mem i s.
Proof.
  intros i j s Hij.
  destruct (ZSet.mem i s) eqn:H.
  × rewrite ZSet.mem_spec in ×.
     rewrite ZSet.remove_spec in ×.
     auto.
  × rewrite not_eq_true in ×.
    rewrite ZSet.mem_spec in ×.
    rewrite ZSet.remove_spec.
    tauto.
Qed.

Lemma ZSet_remove_preserves_not_in : ∀ i j s,
  ZSet.mem i s = false →
  ZSet.mem i (ZSet.remove j s) = false.
Proof.
  intros.
  rewrite not_eq_true in ×.
  rewrite ZSet.mem_spec in ×.
  rewrite ZSet.remove_spec in ×.
  tauto.
Qed.

Lemma ZSet_remove_preserves_not_in_contra : ∀ i j s,
    ZSet.mem i (ZSet.remove j s) = true →
    ZSet.mem i s = true.
Proof.
  intros.
  rewrite ZSet.mem_spec in ×.
  rewrite ZSet.remove_spec in ×.
  tauto.
Qed.

Lemma ZSet_add_preserves_in : ∀ i j s,
    ZSet.mem i s = true →
    ZSet.mem i (ZSet.add j s) = true.
Proof.
  intros.
  rewrite ZSet.mem_spec in ×.
  rewrite ZSet.add_spec.
  auto.
Qed.