-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathFSetNotin.v
172 lines (139 loc) · 4.25 KB
/
FSetNotin.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
(** Lemmas and tactics for working with and solving goals related to
non-membership in finite sets. The main tactic of interest here
is [notin_solve].
Authors: Arthur Charguéraud and Brian Aydemir. *)
Set Implicit Arguments.
Require Import FSetInterface.
(* *********************************************************************** *)
(** * Implementation *)
Module Notin (X : FSetInterface.S).
Import X.
(* *********************************************************************** *)
(** ** Facts about set (non-)membership *)
Lemma in_singleton : forall x,
In x (singleton x).
Proof.
intros x.
apply singleton_2.
apply E.eq_refl.
Qed.
Lemma notin_empty : forall x,
~ In x empty.
Proof.
auto using empty_1.
Qed.
Lemma notin_union : forall x E F,
~ In x E -> ~ In x F -> ~ In x (union E F).
Proof.
intros x E F H J K.
destruct (union_1 K); intuition.
Qed.
Lemma elim_notin_union : forall x E F,
~ In x (union E F) -> (~ In x E) /\ (~ In x F).
Proof.
intros x E F H. split; intros J; contradiction H.
auto using union_2.
auto using union_3.
Qed.
Lemma notin_singleton : forall x y,
~ E.eq x y -> ~ In x (singleton y).
Proof.
intros x y H J. assert (K := singleton_1 J). intuition.
Qed.
Lemma elim_notin_singleton : forall x y,
~ In x (singleton y) -> ~ E.eq x y.
Proof.
intros x y H J.
contradiction H.
apply singleton_2, E.eq_sym, J.
Qed.
Lemma elim_notin_singleton' : forall x y,
~ In x (singleton y) -> x <> y.
Proof.
intros. assert (~ E.eq x y). auto using singleton_2.
intros J. subst. intuition.
intros x_eq_y.
apply H0.
rewrite x_eq_y.
apply E.eq_refl.
Qed.
Lemma notin_singleton_swap : forall x y,
~ In x (singleton y) -> ~ In y (singleton x).
Proof.
intros.
assert (Q := elim_notin_singleton H).
auto using singleton_1.
Qed.
(* *********************************************************************** *)
(** ** Rewriting non-membership facts *)
Lemma notin_singleton_rw : forall x y,
~ In x (singleton y) <-> ~ E.eq x y.
Proof.
intros. split.
auto using elim_notin_singleton.
auto using notin_singleton.
Qed.
(* *********************************************************************** *)
(** ** Tactics *)
(** The tactic [notin_simpl_hyps] destructs all hypotheses of the form
[(~ In x E)], where [E] is built using only [empty], [union], and
[singleton]. *)
Ltac notin_simpl_hyps :=
try match goal with
| H: In ?x ?E -> False |- _ =>
change (~ In x E) in H;
notin_simpl_hyps
| H: ~ In _ empty |- _ =>
clear H;
notin_simpl_hyps
| 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;
notin_simpl_hyps
| H: ~ In ?x (union ?E ?F) |- _ =>
destruct (@elim_notin_union x E F H);
clear H;
notin_simpl_hyps
end.
(** The tactic [notin_solve] solves goals of them form [(x <> y)] and
[(~ In x E)] that are provable from hypotheses of the form
destructed by [notin_simpl_hyps]. *)
Ltac notin_solve :=
repeat notin_simpl_hyps;
repeat (progress ( apply notin_empty
|| apply notin_union
|| apply notin_singleton ));
solve [ trivial | congruence | intuition ].
(* *********************************************************************** *)
(** ** Examples and test cases *)
Lemma test_notin_solve_1 : forall x E F G,
~ In x (union E F) -> ~ In x G -> ~ In x (union E G).
Proof.
intros. notin_solve.
Qed.
Lemma test_notin_solve_2 : forall x y E F G,
~ In x (union E (union (singleton y) F)) -> ~ In x G ->
~ In x (singleton y) /\ ~ In y (singleton x).
Proof.
intros. split. notin_solve. notin_solve.
Qed.
Lemma test_notin_solve_3 : forall x y,
~ E.eq x y -> ~ In x (singleton y) /\ ~ In y (singleton x).
Proof.
intros. split. notin_solve. notin_solve.
Qed.
Lemma test_notin_solve_4 : forall x y E F G,
~ In x (union E (union (singleton x) F)) -> ~ In y G.
Proof.
intros. notin_solve.
Qed.
Lemma test_notin_solve_5 : forall x y E F,
~ In x (union E (union (singleton y) F)) -> ~ In y E ->
~ E.eq y x /\ ~ E.eq x y.
Proof.
intros. split. notin_solve. notin_solve.
Qed.
End Notin.