The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi David,

Le 20 janv. 10 à 18:07, David Singh a écrit :

<snip/>
>   This can be defined as follows:
>
>    Require Import Program.Equality.
>
>     Definition pPT n I (t : T PT n) (x : EPT (P3 n) (cn I t)) : PPT x.
>     intros n I t x; dependent destruction x. exact (pp3 _ ).
>    Defined.
>
>   This is fine until one has to prove things involving pPT; the  
> function
>    reduces to a large, complicated expression. I was wondering if  
> there is a
>    better way to define pPT *without* the use of dependent  
> destruction, and which
>   would reduce as it should?

I think this example falls outside the capabilities of Coq's match  
without
K/JMeq, so something like [dependent destruction] is needed. I'm working
on a plugin that gives you the equations you expect (as rewrite rules,
not primitive reductions) and an elimination principle from dependent
pattern-matching definitions.
It's currently available only through git://github.com/mattam82/Coq- 
Equations.git

In your case the following definition works:

Require Import Equations.

Equations(nocomp) pPT n I (t : T PT n) (x : EPT (P3 n) (cn I t)) : PPT  
x :=
pPT _ _ _ (p3 e') := pp3 e'.

And you get
pPT_equation_1 :
forall (n : nat) (t : PT n) (ts : T PT n) (e : EPT t ts), pPT (p3 e) =  
pp3 e

and

pPT_elim :
forall
  P : forall (n : nat) (I : PT n) (t : T PT n) (x : EPT (P3 n) (cn I  
t)),
      PPT x -> Prop,
(forall (n : nat) (t : PT n) (ts : T PT n) (e : EPT t ts),
 P n t ts (p3 e) (pp3 e)) ->
forall (n : nat) (I : PT n) (t : T PT n) (x : EPT (P3 n) (cn I t)),
P n I t x (pPT x)

Hope this helps,
-- Matthieu