The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Wed, Jun 07, 2006 at 02:09:52PM +0200, Fabrice Lemercier wrote:

> Thank you for the reply. 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?

I've a solution using Streicher's axiom K, which is a theorem on types
whose equality is decidable. I think it is morally the same as
Roland's, but then much more verbose and maybe more clumsy. I find it
easier to understand, though.

dec_eq_dadep is left as an exercise to the reader.

Inductive Trm : Set :=
  trm : nat->Trm.

Inductive Typ : Trm*nat->Set :=
  axiom : forall n, Typ (trm n, n).

Require Import Eqdep_dec.
Require Import Peano_dec.

Definition cast : forall (p p':Trm*nat), p=p' -> (Typ p) -> Typ p'.
intros p p' pp'.
rewrite pp'.
intros I; exact I.
Defined.


Lemma dec_eq_dadep:forall p p':Trm*nat, Decidable.decidable (p = p').
Admitted.

Lemma a: forall (p:Trm*nat)(x:Typ p)(p':Trm*nat)(y:Typ p')(pp':p=p'), (cast _ 
_ pp' x) = y.
intros p x.
dependent inversion x; subst.
intros p' y.
dependent inversion y; subst.
rename n0 into m.
intros pp'.
inversion pp'; subst.
eapply K_dec with (P:=fun pp' => cast _ _ pp' (axiom m) = axiom m).
apply dec_eq_dadep.
reflexivity.
Qed.

Goal forall t:Trm, forall n, forall x y:Typ (t,n), x=y.
intros.
apply a with (pp':=refl_equal (t,n)) (x:=x).
Qed.

-- 
Lionel