The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

On Jun 7, 2006, at 2:09 PM, Fabrice Lemercier wrote:
> Unfortunately my example was
> too simplified compare to the original type system I
> am dealing with. Here is a less simplified version.
> Can you prove the goal?
>
>   Inductive Trm : Set :=
>     trm : nat->Trm.
>
>   Inductive Typ : Trm*nat->Set :=
>     axiom : forall n, Typ (trm n, n).

You'll need to provide an elimination predicate. Think of "eq_rec" as  
a type cast here. To get rid of it one can use Streicher's axiom K,  
which happens to be verified by types with decidable equality.

>   Goal forall t:Trm, forall n, forall x y:Typ (t,n), x=y.
  intros; refine(
    match x as x0 in Typ tn0, y as y0 in Typ tn1 return forall  
(H:tn0=tn1), eq_rec _ Typ x0 _ H = y0 with
    | axiom _, axiom _ => fun H => _
    end (refl_equal _)).
  generalize H.
  inversion H.
  Require Import Eqdep_dec.
  intros; pattern H0; apply K_dec_set.
    repeat (decide equality).
    apply refl_equal.
  Qed.

However this is likely to become rather complicated when you try to  
prove more interesting things. If you tell us a little more about  
your type system, perhaps someone could suggest a different way to do  
describe it in Coq.

Best,

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/