Mercurial > cpdt > repo

annotate src/DepList.v @ 206:3f4576f15130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Revising for 8.2 through first big example
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 16:44:06 -0500
parents f6293ba66559
children f8bcd33bdd91
rev   line source
adamc@114 1 (* Copyright (c) 2008, Adam Chlipala
adamc@114 2 *
adamc@114 3 * This work is licensed under a
adamc@114 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@114 5 * Unported License.
adamc@114 6 * The license text is available at:
adamc@114 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@114 8 *)
adamc@114 9
adamc@114 10 (* Dependent list types presented in Chapter 8 *)
adamc@114 11
adamc@179 12 Require Import Arith List Tactics.
adamc@114 13
adamc@114 14 Set Implicit Arguments.
adamc@114 15
adamc@114 16
adamc@114 17 Section ilist.
adamc@123 18 Variable A : Type.
adamc@114 19
adamc@123 20 Fixpoint ilist (n : nat) : Type :=
adamc@114 21 match n with
adamc@114 22 | O => unit
adamc@114 23 | S n' => A * ilist n'
adamc@114 24 end%type.
adamc@114 25
adamc@149 26 Definition inil : ilist O := tt.
adamc@149 27 Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls).
adamc@149 28
adamc@149 29 Definition hd n (ls : ilist (S n)) : A := fst ls.
adamc@149 30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls.
adamc@149 31
adamc@149 32 Implicit Arguments icons [n].
adamc@149 33
adamc@123 34 Fixpoint index (n : nat) : Type :=
adamc@114 35 match n with
adamc@114 36 | O => Empty_set
adamc@114 37 | S n' => option (index n')
adamc@114 38 end.
adamc@114 39
adamc@114 40 Fixpoint get (n : nat) : ilist n -> index n -> A :=
adamc@114 41 match n return ilist n -> index n -> A with
adamc@114 42 | O => fun _ idx => match idx with end
adamc@114 43 | S n' => fun ls idx =>
adamc@114 44 match idx with
adamc@114 45 | None => fst ls
adamc@114 46 | Some idx' => get n' (snd ls) idx'
adamc@114 47 end
adamc@114 48 end.
adamc@149 49
adamc@149 50 Section everywhere.
adamc@149 51 Variable x : A.
adamc@149 52
adamc@149 53 Fixpoint everywhere (n : nat) : ilist n :=
adamc@149 54 match n return ilist n with
adamc@149 55 | O => inil
adamc@149 56 | S n' => icons x (everywhere n')
adamc@149 57 end.
adamc@149 58 End everywhere.
adamc@149 59
adamc@149 60 Section singleton.
adamc@149 61 Variables x default : A.
adamc@149 62
adamc@149 63 Fixpoint singleton (n m : nat) {struct n} : ilist n :=
adamc@149 64 match n return ilist n with
adamc@149 65 | O => inil
adamc@149 66 | S n' =>
adamc@149 67 match m with
adamc@149 68 | O => icons x (everywhere default n')
adamc@149 69 | S m' => icons default (singleton n' m')
adamc@149 70 end
adamc@149 71 end.
adamc@149 72 End singleton.
adamc@149 73
adamc@149 74 Section map2.
adamc@149 75 Variable f : A -> A -> A.
adamc@149 76
adamc@149 77 Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n :=
adamc@149 78 match n return ilist n -> ilist n -> ilist n with
adamc@149 79 | O => fun _ _ => inil
adamc@149 80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
adamc@149 81 end.
adamc@149 82 End map2.
adamc@194 83
adamc@194 84 Section fold.
adamc@194 85 Variable B : Type.
adamc@194 86 Variable f : A -> B -> B.
adamc@194 87 Variable i : B.
adamc@194 88
adamc@194 89 Fixpoint foldr (n : nat) : ilist n -> B :=
adamc@194 90 match n return ilist n -> B with
adamc@194 91 | O => fun _ => i
adamc@194 92 | S n' => fun ils => f (hd ils) (foldr n' (tl ils))
adamc@194 93 end.
adamc@194 94 End fold.
adamc@114 95 End ilist.
adamc@114 96
adamc@194 97 Implicit Arguments inil [A].
adamc@194 98 Implicit Arguments icons [A n].
adamc@194 99
adamc@149 100 Implicit Arguments icons [A n].
adamc@114 101 Implicit Arguments get [A n].
adamc@149 102 Implicit Arguments map2 [A n].
adamc@194 103 Implicit Arguments foldr [A B n].
adamc@114 104
adamc@196 105 Section imap.
adamc@196 106 Variables A B : Type.
adamc@196 107 Variable f : A -> B.
adamc@196 108
adamc@196 109 Fixpoint imap (n : nat) : ilist A n -> ilist B n :=
adamc@196 110 match n return ilist A n -> ilist B n with
adamc@196 111 | O => fun _ => inil
adamc@196 112 | S n' => fun ls => icons (f (hd ls)) (imap _ (tl ls))
adamc@196 113 end.
adamc@196 114 End imap.
adamc@196 115
adamc@196 116 Implicit Arguments imap [A B n].
adamc@196 117
adamc@114 118 Section hlist.
adamc@114 119 Variable A : Type.
adamc@114 120 Variable B : A -> Type.
adamc@114 121
adamc@114 122 Fixpoint hlist (ls : list A) : Type :=
adamc@114 123 match ls with
adamc@114 124 | nil => unit
adamc@114 125 | x :: ls' => B x * hlist ls'
adamc@114 126 end%type.
adamc@114 127
adamc@125 128 Definition hnil : hlist nil := tt.
adamc@125 129 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
adamc@125 130 (v, hls).
adamc@125 131
adamc@114 132 Variable elm : A.
adamc@114 133
adamc@114 134 Fixpoint member (ls : list A) : Type :=
adamc@114 135 match ls with
adamc@114 136 | nil => Empty_set
adamc@114 137 | x :: ls' => (x = elm) + member ls'
adamc@114 138 end%type.
adamc@114 139
adamc@126 140 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
adamc@126 141 inl _ pf.
adamc@126 142 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
adamc@126 143 inr _ m.
adamc@126 144
adamc@114 145 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
adamc@114 146 match ls return hlist ls -> member ls -> B elm with
adamc@114 147 | nil => fun _ idx => match idx with end
adamc@114 148 | _ :: ls' => fun mls idx =>
adamc@114 149 match idx with
adamc@114 150 | inl pf => match pf with
adamc@114 151 | refl_equal => fst mls
adamc@114 152 end
adamc@114 153 | inr idx' => hget ls' (snd mls) idx'
adamc@114 154 end
adamc@114 155 end.
adamc@125 156
adamc@125 157 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
adamc@125 158 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
adamc@125 159 | nil => fun _ hls2 => hls2
adamc@125 160 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
adamc@125 161 end.
adamc@194 162
adamc@194 163 Variable f : forall x, B x.
adamc@194 164
adamc@194 165 Fixpoint hmake (ls : list A) : hlist ls :=
adamc@194 166 match ls return hlist ls with
adamc@194 167 | nil => hnil
adamc@194 168 | x :: ls' => hcons _ (f x) (hmake ls')
adamc@194 169 end.
adamc@196 170
adamc@196 171 Implicit Arguments hget [ls].
adamc@196 172
adamc@196 173 Theorem hget_hmake : forall ls (m : member ls),
adamc@196 174 hget (hmake ls) m = f elm.
adamc@196 175 induction ls; crush.
adamc@196 176 case a0; reflexivity.
adamc@196 177 Qed.
adamc@114 178 End hlist.
adamc@114 179
adamc@125 180 Implicit Arguments hnil [A B].
adamc@125 181 Implicit Arguments hcons [A B x ls].
adamc@114 182 Implicit Arguments hget [A B elm ls].
adamc@125 183 Implicit Arguments happ [A B ls1 ls2].
adamc@194 184 Implicit Arguments hmake [A B].
adamc@125 185
adamc@126 186 Implicit Arguments hfirst [A elm x ls].
adamc@126 187 Implicit Arguments hnext [A elm x ls].
adamc@126 188
adamc@125 189 Infix ":::" := hcons (right associativity, at level 60).
adamc@125 190 Infix "+++" := happ (right associativity, at level 60).
adamc@163 191
adamc@163 192 Section hmap.
adamc@163 193 Variable A : Type.
adamc@163 194 Variables B1 B2 : A -> Type.
adamc@163 195
adamc@163 196 Variable f : forall x, B1 x -> B2 x.
adamc@163 197
adamc@163 198 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
adamc@163 199 match ls return hlist B1 ls -> hlist B2 ls with
adamc@163 200 | nil => fun _ => hnil
adamc@163 201 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
adamc@163 202 end.
adamc@179 203
adamc@179 204 Implicit Arguments hmap [ls].
adamc@179 205
adamc@179 206 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
adamc@179 207 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
adamc@179 208 induction ls1; crush.
adamc@179 209 Qed.
adamc@197 210
adamc@197 211 Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls),
adamc@197 212 hget (hmap hls) m = f (hget hls m).
adamc@197 213 induction ls; crush.
adamc@197 214 case a1; crush.
adamc@197 215 Qed.
adamc@163 216 End hmap.
adamc@163 217
adamc@163 218 Implicit Arguments hmap [A B1 B2 ls].