Skip to Content.
Sympa Menu

coq-club - [Coq-Club] programing dependent types without program

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] programing dependent types without program


chronological Thread 
  • From: David Singh <david.singh45 AT googlemail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] programing dependent types without program
  • Date: Wed, 20 Jan 2010 17:07:17 +0000
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=YmtGTIwDcy0YrlwP9Pf5mcnsER2PhDlABgX1LP3JPvL7Z6CXAtntD2vekNc5TMlqMf 1wrqHw5MP9TQu5Aeu2NhJl0Utc2mUaOFz7Mp3MwA52lvs7mE7cetuxWRYJqo+sSFDnbD VatrMI72AB3VhcixPIbyWoDvRfTIwdZE5i8i8=

 Dear Coq Club,

  I will be very greatful if someone can assist me with the following.

  Suppose I have the following Inductive types declared:

    Inductive PT : nat ->  Set :=
   | P1 : forall n,  PT n
   | P2 : forall n ,  PT n -> PT n -> PT n
   | P3 : forall n, PT (S n).


   Inductive T (F : nat -> Type) : nat -> Type :=
   | e : T F 0
   | cn : forall n, F n -> T F n -> T F (S n).

   
   Inductive EPT : forall n, PT n -> T PT n ->  Type :=
   | p1 : forall n (t : T PT n), EPT (P1 _) t
   | p3  : forall n (t : PT n) (ts : T PT n), EPT t ts -> EPT (P3 _ ) (cn t  ts)
   | p2 : forall n (l r : PT n) (t : T PT n), EPT l t -> EPT r t -> EPT (P2 l r) t.


 I would now like to show that the type EPT (P3 _ ) (cn a b) has only one inhabitant
  and that inhabitant is built from a and b. One way is to declare the 
  type

  Inductive PPT n I (t : T PT n) : EPT (P3 n) (cn I t) -> Type :=
   | pp3 : forall (x : EPT I t), PPT (p3 x).

  and define the function
 
  Definition pPT n I (t : T PT n) (x : EPT (P3 n) (cn I t)) : PPT x.

  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?

  Regards,

  DS.


Archive powered by MhonArc 2.6.16.

Top of Page