Mercurial > cpdt > repo
changeset 125:8a548a6c7074
Add ext_eq axiom and DepList notations
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 20 Oct 2008 10:44:20 -0400 |
| parents | 57eaceb085f6 |
| children | d7aec67f808b |
| files | Makefile src/Axioms.v src/DepList.v |
| diffstat | 3 files changed, 34 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/Makefile Mon Oct 20 09:11:54 2008 -0400 +++ b/Makefile Mon Oct 20 10:44:20 2008 -0400 @@ -1,4 +1,4 @@ -MODULES_NODOC := Tactics MoreSpecif DepList +MODULES_NODOC := Axioms Tactics MoreSpecif DepList MODULES_PROSE := Intro MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \ MoreDep DataStruct Equality
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Axioms.v Mon Oct 20 10:44:20 2008 -0400 @@ -0,0 +1,17 @@ +(* Copyright (c) 2008, Adam Chlipala + * + * This work is licensed under a + * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 + * Unported License. + * The license text is available at: + * http://creativecommons.org/licenses/by-nc-nd/3.0/ + *) + +(* Additional axioms not in the Coq standard library *) + +Axiom ext_eq : forall (A : Type) (B : A -> Type) + (f g : forall x, B x), + (forall x, f x = g x) + -> f = g. + +Ltac ext_eq := apply ext_eq; intro.
--- a/src/DepList.v Mon Oct 20 09:11:54 2008 -0400 +++ b/src/DepList.v Mon Oct 20 10:44:20 2008 -0400 @@ -52,6 +52,10 @@ | x :: ls' => B x * hlist ls' end%type. + Definition hnil : hlist nil := tt. + Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) := + (v, hls). + Variable elm : A. Fixpoint member (ls : list A) : Type := @@ -71,6 +75,18 @@ | inr idx' => hget ls' (snd mls) idx' end end. + + Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) := + match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with + | nil => fun _ hls2 => hls2 + | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2) + end. End hlist. +Implicit Arguments hnil [A B]. +Implicit Arguments hcons [A B x ls]. Implicit Arguments hget [A B elm ls]. +Implicit Arguments happ [A B ls1 ls2]. + +Infix ":::" := hcons (right associativity, at level 60). +Infix "+++" := happ (right associativity, at level 60).