0
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ I think rewrite equality should get you one step further, after adding Require Import Setoid to the top of your script. $\endgroup$ – Dave Clarke Jul 12 '11 at 11:56
  • $\begingroup$ Thank you. I managed to finish the proof by adding: rewrite equality. intro c. split. apply H0. apply H1. Still, I'd like to know if there is any other way of doing this, for example without having to import "Setoid". $\endgroup$ – gbo4 Jul 12 '11 at 12:07
6
$\begingroup$
Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.
Proof.
  firstorder using equality.
Qed.
$\endgroup$
1
$\begingroup$

An alternative answer, that only uses basic tactics:

Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y. Proof. intros x y H. inversion H. apply equality. split. apply H0. apply H1. Qed.

For those that don't want to run it through Coq, the proof is fairly obvious, the equality axiom is literally the antecedent subset x y /\ subset y x with a little bit of obfuscation (the quantification is in sort of the wrong spot, and we can effectively move it with the split).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.