Coq can't discriminate between constructors for dependently typed inductive proposition

Question

I created this example type to demonstrate the problem I'm having:

Inductive foo : nat -> Prop :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

Now clearly foo_1 0 <> foo_2 0, but I'm unable to prove this:

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H.

This returns the error

Not a discriminable equality.

inversion H doesn't change the context at all. Oddly, if I change foo from Prop to Type then the proof goes through, but I can't do this in my actual code because it causes problems elsewhere.

How can I get this proof to go through? And why is this problematic in the first place?

Answer 1

The logic underlying Coq is compatible with the axiom of "proof irrelevance" which states that any two proofs of a given Prop are equal. As a consequence it is impossible to prove the statement you have formulated.

If you want to be able to discriminate between the two constructors, you need to make foo an inductive Type rather than Prop. bar is then accepted as a valid proof.

Inductive foo : nat -> Type :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H. Qed.

Answer 2

Short answer: you can't.

Let's take a simpler example, where we also fail to prove a similar thing:

Inductive baz : Prop :=
| baz1 : baz
| baz2 : baz.

Goal baz1 <> baz2.
  intro H.
  Fail discriminate H.
Abort.

The above fails with the following error message:

Error: Not a discriminable equality.

Now, let's try and find out where exactly discriminate fails.

First of all, let's take a detour and prove a very simple statement:

Goal false <> true.
  intro prf; discriminate.
Qed.

We can also prove the above goal by providing its proof term directly, instead of building it using tactics:

Goal false <> true.
  exact (fun prf : false = true =>
    eq_ind false (fun e : bool => if e then False else True) I true prf).
Qed.

The above is a simplified version of what the discriminate tactic builds.

Let's replace false, true, and bool in the proof term with baz1, baz2, baz correspondingly and see what happens:

Goal baz1 <> baz2.
  Fail exact (fun prf : baz1 = baz2 =>
    eq_ind baz1 (fun e : baz => if e then False else True) I baz2 prf).
Abort.

The above fails with the following:

The command has indeed failed with message:
Incorrect elimination of e in the inductive type baz:
the return type has sort Type while it should be Prop.
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

The reason of the error is this abstraction:

Fail Check (fun e : baz => if e then False else True).

The above produces the same error message. And it's easy to see why. The abstraction's type is baz -> Prop and what's baz -> Prop's type?

Check baz -> Prop.   (* baz -> Prop : Type *)

Maps from proofs of propositions to propositions live in Type, not in Prop! Otherwise it would cause universe inconsistency.

Our conclusion is that there is no way to prove the inequality, since to there is no way to break through Prop to do that -- you can't just use rewriting (baz1 = baz2) to build a proof of False.

Another argument (I see it has been already proposed by @gallais): if it was possible to use some clever trick and do the proof staying within Prop, then the proof irrelevance axiom would be inconsistent with Coq's logic:

Variable contra : baz1 <> baz2.
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
Check contra (proof_irrelevance _ baz1 baz2).    (* False *)

But, it's known to be consistent, see Coq's FAQ.

You might want to look at the Universes chapter of CPDT, section "The Prop Universe" specifically.