The Coq mailing list

["Eelis van der Weegen" <eelis AT eelis.net>]

Greetings.

Is the following provable? If it is, how? If it isn't, why not? :

  Inductive P : nat -> Prop := C0 : P 0 | C1 : P 1.

  Theorem A: forall (x: P 0), x = C0.

As soon as I try to do case analysis or induction on x with the intention
to reveal that it can only be C0, I get "Cannot solve a second-order
unification problem". Coq Faq item 171 suggests helping Coq using the
"pattern" tactic, but I can't find a way to do that here. I've also tried
rephrasing the equality using Eqdep, but always seem to end up with the
same problem as above.

Had P been of type  nat -> Set  I could have used JMeq:

  Require Import JMeq.

  Inductive P : nat -> Set := C0 : P 0 | C1 : P 1.

  Lemma H: forall (n: nat) (x: P n), n = 0 -> JMeq x C0.
  Proof.
  induction x.
  reflexivity.
  intro.
    discriminate.
  Qed.

  Theorem B: forall (x: P 0), x = C0.
  Proof.
  intro.
  apply JMeq_eq.
  apply H.
  reflexivity.
  Qed.

However, JMeq doesn't seem to work for things in Prop.

As a side note, if there's a proof of B that does not rely on JMeq (and
its axiom) I'd also be very interested in that.

Any help is appreciated.

Thanks,

Eelis