Mercurial > cpdt > repo

annotate src/DepList.v @ 562:36b1f893c1e0

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