Mercurial > cpdt > repo

annotate src/DepList.v @ 563:af97676583f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Jan 2018 11:53:31 -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].