Mercurial > cpdt > repo

annotate src/DepList.v @ 287:be571572c088

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC-inspired Universes tweaks
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 14:05:00 -0500
parents d1464997078d
children d5787b70cf48
rev   line source
adamc@216 1 (* Copyright (c) 2008-2009, 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@216 20 Inductive ilist : nat -> Type :=
adamc@216 21 | INil : ilist O
adamc@216 22 | ICons : forall n, A -> ilist n -> ilist (S n).
adamc@114 23
adamc@216 24 Definition hd n (ls : ilist (S n)) :=
adamc@216 25 match ls in ilist n' return match n' with
adamc@216 26 | O => unit
adamc@216 27 | S _ => A
adamc@216 28 end with
adamc@216 29 | INil => tt
adamc@216 30 | ICons _ x _ => x
adamc@216 31 end.
adamc@216 32 Definition tl n (ls : ilist (S n)) :=
adamc@216 33 match ls in ilist n' return match n' with
adamc@216 34 | O => unit
adamc@216 35 | S n => ilist n
adamc@216 36 end with
adamc@216 37 | INil => tt
adamc@216 38 | ICons _ _ ls' => ls'
adamc@114 39 end.
adamc@114 40
adamc@216 41 Inductive fin : nat -> Set :=
adamc@216 42 | First : forall n, fin (S n)
adamc@216 43 | Next : forall n, fin n -> fin (S n).
adamc@216 44
adamc@216 45 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@216 46 match ls with
adamc@216 47 | INil => fun idx =>
adamc@216 48 match idx in fin n' return (match n' with
adamc@216 49 | O => A
adamc@216 50 | S _ => unit
adamc@216 51 end) with
adamc@216 52 | First _ => tt
adamc@216 53 | Next _ _ => tt
adamc@114 54 end
adamc@216 55 | ICons _ x ls' => fun idx =>
adamc@216 56 match idx in fin n' return (fin (pred n') -> A) -> A with
adamc@216 57 | First _ => fun _ => x
adamc@216 58 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@216 59 end (get ls')
adamc@114 60 end.
adamc@149 61
adamc@149 62 Section everywhere.
adamc@149 63 Variable x : A.
adamc@149 64
adamc@149 65 Fixpoint everywhere (n : nat) : ilist n :=
adamc@216 66 match n with
adamc@216 67 | O => INil
adamc@216 68 | S n' => ICons x (everywhere n')
adamc@149 69 end.
adamc@149 70 End everywhere.
adamc@149 71
adamc@149 72 Section singleton.
adamc@149 73 Variables x default : A.
adamc@149 74
adamc@216 75 Fixpoint singleton (n m : nat) : ilist n :=
adamc@216 76 match n with
adamc@216 77 | O => INil
adamc@149 78 | S n' =>
adamc@149 79 match m with
adamc@216 80 | O => ICons x (everywhere default n')
adamc@216 81 | S m' => ICons default (singleton n' m')
adamc@149 82 end
adamc@149 83 end.
adamc@149 84 End singleton.
adamc@149 85
adamc@149 86 Section map2.
adamc@149 87 Variable f : A -> A -> A.
adamc@149 88
adamc@216 89 Fixpoint map2 n (il1 : ilist n) : ilist n -> ilist n :=
adamc@216 90 match il1 in ilist n return ilist n -> ilist n with
adamc@216 91 | INil => fun _ => INil
adamc@216 92 | ICons _ x il1' => fun il2 => ICons (f x (hd il2)) (map2 il1' (tl il2))
adamc@149 93 end.
adamc@149 94 End map2.
adamc@194 95
adamc@194 96 Section fold.
adamc@194 97 Variable B : Type.
adamc@194 98 Variable f : A -> B -> B.
adamc@194 99 Variable i : B.
adamc@194 100
adamc@216 101 Fixpoint foldr n (il : ilist n) : B :=
adamc@216 102 match il with
adamc@216 103 | INil => i
adamc@216 104 | ICons _ x il' => f x (foldr il')
adamc@194 105 end.
adamc@194 106 End fold.
adamc@114 107 End ilist.
adamc@114 108
adamc@216 109 Implicit Arguments INil [A].
adamc@216 110 Implicit Arguments First [n].
adamc@114 111
adamc@196 112 Section imap.
adamc@196 113 Variables A B : Type.
adamc@196 114 Variable f : A -> B.
adamc@196 115
adamc@216 116 Fixpoint imap n (il : ilist A n) : ilist B n :=
adamc@216 117 match il with
adamc@216 118 | INil => INil
adamc@216 119 | ICons _ x il' => ICons (f x) (imap il')
adamc@196 120 end.
adamc@196 121 End imap.
adamc@196 122
adamc@114 123 Section hlist.
adamc@114 124 Variable A : Type.
adamc@114 125 Variable B : A -> Type.
adamc@114 126
adamc@216 127 Inductive hlist : list A -> Type :=
adamc@216 128 | HNil : hlist nil
adamc@216 129 | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@114 130
adamc@216 131 Definition hhd ls (hl : hlist ls) :=
adamc@216 132 match hl in hlist ls return match ls with
adamc@216 133 | nil => unit
adamc@216 134 | x :: _ => B x
adamc@216 135 end with
adamc@216 136 | HNil => tt
adamc@216 137 | HCons _ _ v _ => v
adamc@216 138 end.
adamc@216 139
adamc@216 140 Definition htl ls (hl : hlist ls) :=
adamc@216 141 match hl in hlist ls return match ls with
adamc@216 142 | nil => unit
adamc@216 143 | _ :: ls' => hlist ls'
adamc@216 144 end with
adamc@216 145 | HNil => tt
adamc@216 146 | HCons _ _ _ hl' => hl'
adamc@216 147 end.
adamc@125 148
adamc@114 149 Variable elm : A.
adamc@114 150
adamc@216 151 Inductive member : list A -> Type :=
adamc@216 152 | HFirst : forall ls, member (elm :: ls)
adamc@216 153 | HNext : forall x ls, member ls -> member (x :: ls).
adamc@114 154
adamc@216 155 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
adamc@216 156 match mls with
adamc@216 157 | HNil => fun mem =>
adamc@216 158 match mem in member ls' return (match ls' with
adamc@216 159 | nil => B elm
adamc@216 160 | _ :: _ => unit
adamc@216 161 end) with
adamc@216 162 | HFirst _ => tt
adamc@216 163 | HNext _ _ _ => tt
adamc@114 164 end
adamc@216 165 | HCons _ _ x mls' => fun mem =>
adamc@216 166 match mem in member ls' return (match ls' with
adamc@216 167 | nil => Empty_set
adamc@216 168 | x' :: ls'' =>
adamc@216 169 B x' -> (member ls'' -> B elm) -> B elm
adamc@216 170 end) with
adamc@216 171 | HFirst _ => fun x _ => x
adamc@216 172 | HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@216 173 end x (hget mls')
adamc@114 174 end.
adamc@125 175
adamc@216 176 Fixpoint happ (ls1 : list A) (hl1 : hlist ls1) : forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) :=
adamc@216 177 match hl1 in hlist ls1 return forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) with
adamc@216 178 | HNil => fun _ hl2 => hl2
adamc@216 179 | HCons _ _ x hl1' => fun _ hl2 => HCons x (happ hl1' hl2)
adamc@125 180 end.
adamc@194 181
adamc@194 182 Variable f : forall x, B x.
adamc@194 183
adamc@194 184 Fixpoint hmake (ls : list A) : hlist ls :=
adamc@216 185 match ls with
adamc@216 186 | nil => HNil
adamc@216 187 | x :: ls' => HCons (f x) (hmake ls')
adamc@194 188 end.
adamc@196 189
adamc@196 190 Theorem hget_hmake : forall ls (m : member ls),
adamc@196 191 hget (hmake ls) m = f elm.
adamc@216 192 induction ls; crush;
adamc@216 193 match goal with
adamc@216 194 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
adamc@216 195 end; crush.
adamc@196 196 Qed.
adamc@114 197 End hlist.
adamc@114 198
adamc@216 199 Implicit Arguments HNil [A B].
adamc@216 200 Implicit Arguments HCons [A B x ls].
adamc@194 201 Implicit Arguments hmake [A B].
adamc@125 202
adamc@216 203 Implicit Arguments HFirst [A elm ls].
adamc@216 204 Implicit Arguments HNext [A elm x ls].
adamc@126 205
adamc@216 206 Infix ":::" := HCons (right associativity, at level 60).
adamc@125 207 Infix "+++" := happ (right associativity, at level 60).
adamc@163 208
adamc@163 209 Section hmap.
adamc@163 210 Variable A : Type.
adamc@163 211 Variables B1 B2 : A -> Type.
adamc@163 212
adamc@163 213 Variable f : forall x, B1 x -> B2 x.
adamc@163 214
adamc@216 215 Fixpoint hmap (ls : list A) (hl : hlist B1 ls) : hlist B2 ls :=
adamc@216 216 match hl with
adamc@216 217 | HNil => HNil
adamc@216 218 | HCons _ _ x hl' => f x ::: hmap hl'
adamc@163 219 end.
adamc@179 220
adamc@179 221 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
adamc@179 222 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
adamc@216 223 induction h1; crush.
adamc@179 224 Qed.
adamc@197 225
adamc@197 226 Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls),
adamc@197 227 hget (hmap hls) m = f (hget hls m).
adamc@216 228 induction hls; crush;
adamc@216 229 match goal with
adamc@216 230 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
adamc@216 231 end; crush.
adamc@197 232 Qed.
adamc@163 233 End hmap.
adamc@163 234
adamc@163 235 Implicit Arguments hmap [A B1 B2 ls].