I'm a Coq newbie and I'd like to prove that the inclusion relation is antisymmetric, that is: $\forall x\forall y(x\subseteq y\land y\subseteq x\rightarrow x=y)$.
I wrote the following thing:
Section Test.
Variable set : Type.
Variable element : set -> set -> Prop.
Definition subset (x:set) (y:set) := forall z:set, element z x -> element z y.
Axiom equality : forall x y:set, x = y <-> forall z:set, element z x <-> element z y.
Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.
Proof.
intros a b.
unfold subset.
intro H.
destruct H as [H0 H1].
At this point I get the following output:
1 subgoal
set : Type
element : set -> set -> Prop
a : set
b : set
H0 : forall z : set, element z a -> element z b
H1 : forall z : set, element z b -> element z a
______________________________________(1/1)
a = b
I'm stuck now because I don't know how to:
- change the goal from $a=b$ to $\forall z(z\in a\leftrightarrow z\in b)$ and then to $c\in a\leftrightarrow c\in b$
- change
H0
from $\forall z(z\in a\rightarrow z\in b)$ to $c\in a\rightarrow c\in b$ - change
H1
from $\forall z(z\in b\rightarrow z\in c)$ to $c\in b\rightarrow c\in a$
That is, I know how to prove this theorem on paper but not with Coq.
rewrite equality
should get you one step further, after addingRequire Import Setoid
to the top of your script. $\endgroup$