1
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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.
$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you. Step indexing ElProp helped me finish the proof. $\endgroup$ – Gowtham Kaki May 22 '14 at 18:50

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.