<p>I think you need induction here to help you show that there is no term like <code>C2 (C1 (C2 (C1 ...</code>. I also think you need to strengthen your induction hypothesis, because you don't just need to know that <code>ElProp C1</code> is uninhabited, but that <code>ElProp C2</code> is as well.</p>

<p>I proved this using an auxiliary lemma</p>

<p><code>Theorem excircular_help : forall y, forall x:(ElProp y), y = R3.</code></p>

<p>Try this and let me know if you get stuck.</p>

CC BY-SA 3.0
2014-05-22T18:50:58.270Z
Thank you. Step indexing ElProp helped me finish the proof.
Gowtham Kaki
CC BY-SA 3.0
2014-05-20T15:01:11.137Z
2014-05-20T15:01:11.137Z
jbapple
<p>You should use <code>False</code> instead of <code>1&gt;2</code> in the conclusion of the theorem. Using indirect ways of denoting an impossible proposition is an unnecessary complication. <code>False</code> is the impossible proposition used in the standard library.</p>

<p>In order to prove that <code>ElProp R1</code> is uninhabited, you need to prove that <code>ElProp R2</code> is uninhabited, and vice versa. You need induction over <code>ElProp</code>. The inductive property is that there is inhabitant of <code>ElProp R1</code> or <code>ElProp R2</code>. (You can also work on proving that there is no way to construct an object with <code>C1</code> or <code>C2</code>, but this is harder because they have different types.)</p>

<pre><code>~(ElProp R1 \/ ElProp R2)
</code></pre>

<p>In order to perform induction over <code>ElProp</code>, you need to work in a generic inhabitant of <code>ElProp</code>. It has the type <code>ElProp R</code> for some <code>R : El</code>. What we want to prove is that for such an inhabitant, <code>R</code> cannot be <code>R1</code> or <code>R2</code>. Here's a way to state this:</p>

<pre><code>Lemma excircular : forall R, (R = R1 \/ R = R2) -&gt; ~ElProp R.
</code></pre>

<p>Now let's prove the lemma. First, expand the <code>~</code> abbreviation for <code>fun A =&gt; A -&gt; False</code>.</p>

<pre><code>unfold not; intros.
</code></pre>

<p>We have a hypothesis of type <code>ElProp R</code>, perfect for induction.</p>

<pre><code>induction H0.
</code></pre>

<p>First the <code>C1</code> case; it's an inductive case: the property we're working on works for an <code>ElProp R1</code> because it works for the parameter (which is of type <code>ElProp R2</code>), putting it all together with some straightforward first-order logic. We have a hypothesis of type <code>R2 = R1 \/ R2 = R2</code>; once we've applied <code>IHElProp</code>, the goal becomes <code>R1 = R1 \/ R1 = R2</code>. I'll leave doing that manually as an exercise. The built-in tactic <code>tauto</code> makes short work of this case, as well as the symmetric case for <code>C2</code>.</p>

<pre><code>tauto.
tauto.
</code></pre>

<p>For the <code>C3</code> case, we need to show that the hypotheses are contradictory. We have a single hypothesis <code>R3 = R1 \/ R3 = R2</code>. Each branch of the disjunction is an impossible equality because the constructors <code>R1</code>, <code>R2</code> and <code>R3</code> are distinct.</p>

<pre><code>destruct H. discriminate. discriminate.
Qed.
</code></pre>

<p>Here's a shorter way of proving this lemma. All the intelligence we really need to provide is to use induction on the proper hypothesis, Coq can figure out the rest with some general hints.</p>

<pre><code>Lemma excircular : forall R, (R = R1 \/ R = R2) -&gt; ~ElProp R.
Proof.
  unfold not; intros.
  induction H0; firstorder discriminate.
Qed.
</code></pre>

<p>Now we can prove the desired goal. Expand out the <code>~</code> abbreviation, apply <code>excircular</code> and let Coq fill in the details.</p>

<pre><code>Theorem excircular1 : ~ElProp R1.
Proof.
  intro. eapply excircular; eauto.
Qed.
</code></pre>

CC BY-SA 3.0
2014-05-20T19:00:51.323Z
2014-10-01T19:59:51.360Z
2014-10-01T19:59:51.360Z
Gilles 'SO- stop being evil'
<p>Consider the following inductive definition of "ElProp" in coq:</p>

<pre><code>Inductive El : Set :=
  | R1 : El
  | R2 : El
  | R3 : El.

Inductive ElProp : El -&gt; Prop :=
  | C1 : ElProp R1 -&gt; ElProp R2
  | C2 : ElProp R2 -&gt; ElProp R1
  | C3 : ElProp R3.
</code></pre>

<p>Observing that "(ElProp R1)" is uninhabited, I state the following theorem:</p>

<pre><code>Theorem excircular : ElProp R1 -&gt; 1&gt;2.
</code></pre>

<p>I expect the theorem to be valid, much like the following theorem:</p>

<pre><code>Theorem exfalso : False -&gt; 1&gt;2.
</code></pre>

<p>Since there are no inhabitants in "False", inverting "False" is enough to prove "exfalso". But how do I prove "excircular"? In general, how can we prove that circular propositions are uninhabited?</p>

<coq><calculus-of-constructions>
How to prove that a circular prop is uninhabited?
Gowtham Kaki
# How to prove that a circular prop is uninhabited?

(Asked by: username_0 on 2014-05-20)

Consider the following inductive definition of "ElProp" in coq:
Inductive El : Set :=
  | R1 : El
  | R2 : El
  | R3 : El.

Inductive ElProp : El -> Prop :=
  | C1 : ElProp R1 -> ElProp R2
  | C2 : ElProp R2 -> ElProp R1
  | C3 : ElProp R3.

Observing that "(ElProp R1)" is uninhabited, I state the following theorem:
Theorem excircular : ElProp R1 -> 1>2.

I expect the theorem to be valid, much like the following theorem:
Theorem exfalso : False -> 1>2.

Since there are no inhabitants in "False", inverting "False" is enough to prove "exfalso". But how do I prove "excircular"? In general, how can we prove that circular propositions are uninhabited?

**Tags:** coq, calculus-of-constructions

---

## 2 answers

### Answer by username_2 on 2014-05-20. Score: 5 | Accepted answer

You should use False instead of 1>2 in the conclusion of the theorem. Using indirect ways of denoting an impossible proposition is an unnecessary complication. False is the impossible proposition used in the standard library.
In order to prove that ElProp R1 is uninhabited, you need to prove that ElProp R2 is uninhabited, and vice versa. You need induction over ElProp. The inductive property is that there is inhabitant of ElProp R1 or ElProp R2. (You can also work on proving that there is no way to construct an object with C1 or C2, but this is harder because they have different types.)
~(ElProp R1 \/ ElProp R2)

In order to perform induction over ElProp, you need to work in a generic inhabitant of ElProp. It has the type ElProp R for some R : El. What we want to prove is that for such an inhabitant, R cannot be R1 or R2. Here's a way to state this:
Lemma excircular : forall R, (R = R1 \/ R = R2) -> ~ElProp R.

Now let's prove the lemma. First, expand the ~ abbreviation for fun A => A -> False.
unfold not; intros.

We have a hypothesis of type ElProp R, perfect for induction.
induction H0.

First the C1 case; it's an inductive case: the property we're working on works for an ElProp R1 because it works for the parameter (which is of type ElProp R2), putting it all together with some straightforward first-order logic. We have a hypothesis of type R2 = R1 \/ R2 = R2; once we've applied IHElProp, the goal becomes R1 = R1 \/ R1 = R2. I'll leave doing that manually as an exercise. The built-in tactic tauto makes short work of this case, as well as the symmetric case for C2.
tauto.
tauto.

For the C3 case, we need to show that the hypotheses are contradictory. We have a single hypothesis R3 = R1 \/ R3 = R2. Each branch of the disjunction is an impossible equality because the constructors R1, R2 and R3 are distinct.
destruct H. discriminate. discriminate.
Qed.

Here's a shorter way of proving this lemma. All the intelligence we really need to provide is to use induction on the proper hypothesis, Coq can figure out the rest with some general hints.
Lemma excircular : forall R, (R = R1 \/ R = R2) -> ~ElProp R.
Proof.
  unfold not; intros.
  induction H0; firstorder discriminate.
Qed.

Now we can prove the desired goal. Expand out the ~ abbreviation, apply excircular and let Coq fill in the details.
Theorem excircular1 : ~ElProp R1.
Proof.
  intro. eapply excircular; eauto.
Qed.


---

### Answer by username_1 on 2014-05-20. Score: 4

I think you need induction here to help you show that there is no term like `C2 (C1 (C2 (C1 ...`. I also think you need to strengthen your induction hypothesis, because you don't just need to know that `ElProp C1` is uninhabited, but that `ElProp C2` is as well.

I proved this using an auxiliary lemma

`Theorem excircular_help : forall y, forall x:(ElProp y), y = R3.`

Try this and let me know if you get stuck.

> **Comments:**
> **username_0**: Thank you. Step indexing ElProp helped me finish the proof.  

---

