NatSet.v 3.65 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Require Import Coq.MSets.MSets Coq.Arith.PeanoNat.

(**
 Module for an ordered type with leibniz, based on code from coq-club mailing list
http://coq-club.inria.narkive.com/zptqoou2/how-to-use-msets
**)
Module OWL.
  Definition t := nat.
  Definition eq := @eq t.
  Definition eq_equiv :Equivalence eq := eq_equivalence.
  Definition lt := lt.
  Definition lt_strorder : StrictOrder lt := Nat.lt_strorder.
  Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
  Proof.
    now unfold eq; split; subst.
  Qed.
17
  Definition compare := Nat.compare.
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32

Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof.
  intros; case_eq (compare x y); constructor.
  now apply Compare_dec.nat_compare_eq.
  now apply Compare_dec.nat_compare_Lt_lt.
  now apply Compare_dec.nat_compare_Gt_gt.
Qed.

Definition eq_dec := Peano_dec.eq_nat_dec.
Definition eq_leibniz a b (H:eq a b) := H.
End OWL.

Module NatSet := MakeWithLeibniz OWL.

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
Module NatSetProps := WPropertiesOn OWL NatSet.

Notation "S1 ∪ S2" := (NatSet.union S1 S2) (at level 80, right associativity).

Notation "'{{' x '}}'" := (NatSet.singleton x) (at level 0, no associativity).

Notation "S1 -- S2" := (NatSet.diff S1 S2) (at level 80, right associativity).

Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity).

Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity).

Lemma not_in_not_mem:
  forall n S,
    NatSet.mem n S = false ->
    ~ NatSet.In n S.
Proof.
  intros * not_mem; hnf; intros not_in.
  rewrite <- NatSet.mem_spec in not_in;
    rewrite not_in in *;
    congruence.
Qed.

Lemma add_spec_strong:
  forall x y S,
    (x  (NatSet.add y S)) <-> x = y \/ ((~ (x = y)) /\ (x  S)).
Proof.
  split; intros x_in_add.
  - rewrite NatSet.add_spec in x_in_add.
    case_eq (Nat.eqb x y); intros x_eq_case.
    + left; apply Nat.eqb_eq; auto.
    + right; destruct x_in_add as [x_eq | x_in_S]; subst.
      * rewrite Nat.eqb_refl in x_eq_case; congruence.
      * split; try auto.
        hnf; intros; subst.
        rewrite Nat.eqb_refl in x_eq_case; congruence.
  - rewrite NatSet.add_spec.
    destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto.
Qed.
Heiko Becker's avatar
Heiko Becker committed
72

73
Ltac set_bool_to_prop :=
Heiko Becker's avatar
Heiko Becker committed
74 75 76
  match goal with
  | [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H
  | [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H
77 78 79 80 81 82 83 84 85 86 87
  | [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec
  end.

Ltac solve_simple_sets :=
  match goal with
  | [ H: NatSet.In ?x ?S1 |- NatSet.In ?x (NatSet.union ?S1 ?S2)]
    => rewrite NatSet.union_spec; auto
  end.

Ltac set_hnf_tac :=
  match goal with
Heiko Becker's avatar
Heiko Becker committed
88 89 90 91 92
  | [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H
  | [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H
  | [ H: NatSet.In ?x (NatSet.singleton ?y) |- _] => apply NatSetProps.Dec.F.singleton_1 in H
  | [ H: NatSet.In ?x NatSet.empty |- _ ] => inversion H
  | [ H: NatSet.In ?x (NatSet.union ?S1 ?S2) |- _ ] => rewrite NatSet.union_spec in H
93
  | [ H: NatSet.In ?x (NatSet.add ?y ?S) |- _ ] => rewrite add_spec_strong in H
Heiko Becker's avatar
Heiko Becker committed
94 95 96
  | [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec
  | [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec
  | [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec
97 98
  | [ |- context [NatSet.In ?x (NatSet.remove ?y ?S)]] => rewrite NatSet.remove_spec
  | [ |- context [NatSet.In ?x (NatSet.add ?y ?S)]] => rewrite NatSet.add_spec
Heiko Becker's avatar
Heiko Becker committed
99 100 101 102
  | [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros
  end.

Ltac set_tac :=
103 104 105 106 107 108
  repeat set_bool_to_prop;
  repeat solve_simple_sets;
  repeat set_hnf_tac;
  simpl in *;
  repeat solve_simple_sets;
  try auto.