<pre><code>Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -&gt; x = y.
Proof.
  firstorder using equality.
Qed.
</code></pre>

CC BY-SA 3.0
2011-07-15T20:45:35.297Z
2011-07-15T20:45:35.297Z
Andrej Bauer
<p>An alternative answer, that only uses basic tactics:</p>

<p><code>
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.
</code></p>

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

CC BY-SA 3.0
2015-02-07T12:45:43.243Z
2015-02-07T12:45:43.243Z
Luke Mathieson
<p>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)$.</p>

<p>I wrote the following thing:</p>

<pre><code>Section Test.
Variable set : Type.
Variable element : set -&gt; set -&gt; Prop.
Definition subset (x:set) (y:set) := forall z:set, element z x -&gt; element z y.
Axiom equality : forall x y:set, x = y &lt;-&gt; forall z:set, element z x &lt;-&gt; element z y.
Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -&gt; x = y.
Proof.
intros a b.
unfold subset.
intro H.
destruct H as [H0 H1].
</code></pre>

<p>At this point I get the following output:</p>

<pre><code>1 subgoal
set : Type
element : set -&gt; set -&gt; Prop
a : set
b : set
H0 : forall z : set, element z a -&gt; element z b
H1 : forall z : set, element z b -&gt; element z a
______________________________________(1/1)
a = b
</code></pre>

<p>I'm stuck now because I don't know how to:</p>

<ul>
<li>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$</li>
<li>change <code>H0</code> from $\forall z(z\in a\rightarrow z\in b)$ to $c\in a\rightarrow c\in b$</li>
<li>change <code>H1</code> from $\forall z(z\in b\rightarrow z\in c)$ to $c\in b\rightarrow c\in a$</li>
</ul>

<p>That is, I know how to prove this theorem on paper but not with Coq.</p>

CC BY-SA 3.0
2011-07-12T11:56:24.453Z
I think `rewrite equality` should get you one step further, after adding `Require Import Setoid` to the top of your script.
Dave Clarke
CC BY-SA 3.0
2011-07-12T12:07:10.093Z
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".
gbo4
<coq><set-theory>
Proving that inclusion is antisymmetric in Coq
gbo4
# Proving that inclusion is antisymmetric in Coq

(Asked by: username_0 on 2011-07-12)

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.

**Tags:** coq, set-theory

> **Comments:**
> **username_1**: I think `rewrite equality` should get you one step further, after adding `Require Import Setoid` to the top of your script.  
> **username_0**: 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".  

---

## 2 answers

### Answer by username_2 on 2011-07-15. Score: 6

Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.
Proof.
  firstorder using equality.
Qed.


---

### Answer by username_3 on 2015-02-07. Score: 1

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).


---

