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.
Implicit arguments are declared by default in this library.
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) → x ≠ y.
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) → y ≠ x ∧ ~ 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.
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 (x ≠ y) 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 ].
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