coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] programing dependent types without program, David Singh
- Re: [Coq-Club] programing dependent types without program, Matthieu Sozeau
- Re: [Coq-Club] programing dependent types without program, Adam Chlipala
Archive powered by MhonArc 2.6.16.