The Coq mailing list

[David Nowak <david.nowak AT aist.go.jp>]

Hi Eelis,

You can prove Abis below which is a bit more general than A and then 
apply it.  eq_rect is used to convince Coq that, because 0=n, C0 in also 
of type P n.

  Require Export Eqdep_dec.

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

  Lemma Abis : forall n (x : P n) (p : 0 = n), x = eq_rect 0 P C0 n p.
  Proof.
  intros n x.
  case x.
   intro.
     pattern p in |- *.
     apply K_dec_set.
    decide equality.
    reflexivity.
   intro.
     absurd (0 = 1).
    discriminate.
    assumption.
  Qed.

  Theorem A: forall (x: P 0), x = C0.
  Proof.
  intro.
  apply (Abis 0 x (refl_equal 0)).
  Qed.



Eelis van der Weegen a écrit :
> 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.

David

--
David Nowak
http://staff.aist.go.jp/david.nowak/