The Coq mailing list

[Dachuan Yu <dachuan.yu AT yale.edu>]

Hi,

We met with a problem when encoding something using Coq 7.3. Here is a simplified version.

First, we define a "Type" T which depends on a "nat" n as follows:

Fixpoint T[n:nat] : Type :=
 Cases n of
 | O => (nat -> Prop)
 | (S n') => (T n')
 end.

Then, we define a relation R as follows:

Inductive R : (n:nat)(T n) -> nat -> Prop :=
  | RO : (Psi:(T O); l:nat)
          (Psi l) -> (R O Psi l)
  | RS : (n:nat; Psi:(T (S n)); l:nat)
          (R n Psi l) -> (R (S n) Psi l).

Next, we define two objects of type (T O).

Definition Psi00 : (nat -> Prop) := [n:nat] False.
Definition Psi0 : (T O) := Psi00.

So far everything is ok. Now we want to prove the following lemma:

Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l).

This lemma is true because the premise is false. It seems easily provable by doing inversion on (R O Psi0 l). However, when I did that , I got an error:

    Anomaly: Failure "try_find". Please report.

Is there a way that I can perform this inversion? I also tried Case, Elim, NewInduction , NewDestruct, etc. But after using either one of them, the Psi0 in the premise was changed to an arbitrary variable so I could not proceed.

Thanks for any help,

Dachuan