Library FSetWeakNotin


Lemmas and tactics for working with and solving goals related to non-membership in finite sets. The main tactic of interest here is solve_notin.

Implicit arguments are declared by default in this library.

Require Import FSetInterface.

Implementation


Module Notin
  (E : DecidableType) (Import X : FSetInterface.WS with Module E := E).

Facts about set non-membership


Lemma notin_empty : ∀ x,
  ~ In x empty.

Lemma notin_union : ∀ x E F,
  ~ In x E → ~ In x F → ~ In x (union E F).

Lemma elim_notin_union : ∀ x E F,
  ~ In x (union E F) → (~ In x E) ∧ (~ In x F).


Lemma notin_singleton : ∀ x y,
  ~ E.eq x y → ~ In x (singleton y).


Lemma elim_notin_singleton : ∀ x y,
  ~ In x (singleton y) → ~ E.eq x y.


Lemma elim_notin_singleton' : ∀ x y,
  ~ In x (singleton y) → xy.



Lemma notin_add : ∀ x y F,
  ~ E.eq y x → ~ In x F → ~ In x (add y F).


Lemma elim_notin_add : ∀ x y F,
  ~ In x (add y F) → ~ E.eq y x ∧ ~ In x F.


Lemma elim_notin_add' : ∀ x y F,
  ~ In x (add y F) → yx ∧ ~ In x F.



Lemma notin_remove_1 : ∀ x y E,
  ~ In x E → ~ In x (remove y E).

Lemma notin_remove_2 : ∀ x y E,
  E.eq x y → ~ In x (remove y E).

Lemma notin_remove_3 : ∀ x y E,
  x = y → ~ In x (remove y E).


Lemma elim_notin_remove : ∀ x y E,
  ~ In x (remove y E) → E.eq y x ∨ ~ In x E.


Tactics


The tactic destruct_notin destructs hypotheses of the form (~ In x E).

Ltac destruct_notin :=
  match goal with
    | H: In ?x ?E → False |- _
      change (~ In x E) in H;
      destruct_notin
    | H: ~ In _ empty |- _
      clear H;
      destruct_notin
    | H: ~ In ?x (union ?E ?F) |- _
      destruct (@elim_notin_union x E F H);
      clear H;
      destruct_notin
    | H: ~ In ?x (singleton ?y) |- _
      let F1 := fresh in
      let F2 := fresh in
      assert (F1 := @elim_notin_singleton x y H);
      assert (F2 := @elim_notin_singleton' x y H);
      clear H;
      destruct_notin
    | H: ~ In ?x (add ?y ?F) |- _
      destruct (@elim_notin_add x y F H);
      destruct (@elim_notin_add' x y F H);
      clear H;
      destruct_notin
    | H: ~ In ?x (remove ?y ?E) |- _
      destruct (@elim_notin_remove x y E);
      clear H;
      destruct_notin
    | _
      idtac
  end.

The tactic solve_notin solves goals of them form (xy) and (~ In x E) that are provable from hypotheses of the form destructed by destruct_notin.

Ltac solve_notin :=
  destruct_notin;
  repeat (progress ( apply notin_add
                   || apply notin_empty
                   || apply notin_remove_1
                   || apply notin_remove_2
                   || apply notin_remove_3
                   || apply notin_singleton
                   || apply notin_union ));
  solve [ trivial | congruence | intuition auto ].

Examples and test cases


These examples and test cases are not meant to be exhaustive.

Lemma test_solve_notin_1 : ∀ x E F G,
  ~ In x (union E F) → ~ In x G → ~ In x (union E G).


Lemma test_solve_notin_2 : ∀ x y E F G,
  ~ In x (union E (union (singleton y) F)) → ~ In x G
  ~ In x (singleton y) ∧ ~ In y (singleton x).


Lemma test_solve_notin_3 : ∀ x y,
  ~ E.eq x y → ~ In x (singleton y) ∧ ~ In y (singleton x).


Lemma test_solve_notin_4 : ∀ x y E F G,
  ~ In x (union E (union (singleton x) F)) → ~ In y G.


Lemma test_solve_notin_5 : ∀ x y E F,
  ~ In x (union E (union (singleton y) F)) → ~ In y E
  ~ E.eq y x ∧ ~ E.eq x y.


Lemma test_solve_notin_6 : ∀ x y E,
  ~ In x (add y E) → ~ E.eq x y ∧ ~ In x E.


End Notin.

This page has been generated by coqdoc