Mercurial > cpdt > repo

annotate src/DepList.v @ 194:063b5741c248

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generic size examples
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 11:21:01 -0500
parents 8f3fc56b90d4
children b4ea71b6bf94
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@114 105 Section hlist.
adamc@114 106 Variable A : Type.
adamc@114 107 Variable B : A -> Type.
adamc@114 108
adamc@114 109 Fixpoint hlist (ls : list A) : Type :=
adamc@114 110 match ls with
adamc@114 111 | nil => unit
adamc@114 112 | x :: ls' => B x * hlist ls'
adamc@114 113 end%type.
adamc@114 114
adamc@125 115 Definition hnil : hlist nil := tt.
adamc@125 116 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
adamc@125 117 (v, hls).
adamc@125 118
adamc@114 119 Variable elm : A.
adamc@114 120
adamc@114 121 Fixpoint member (ls : list A) : Type :=
adamc@114 122 match ls with
adamc@114 123 | nil => Empty_set
adamc@114 124 | x :: ls' => (x = elm) + member ls'
adamc@114 125 end%type.
adamc@114 126
adamc@126 127 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
adamc@126 128 inl _ pf.
adamc@126 129 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
adamc@126 130 inr _ m.
adamc@126 131
adamc@114 132 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
adamc@114 133 match ls return hlist ls -> member ls -> B elm with
adamc@114 134 | nil => fun _ idx => match idx with end
adamc@114 135 | _ :: ls' => fun mls idx =>
adamc@114 136 match idx with
adamc@114 137 | inl pf => match pf with
adamc@114 138 | refl_equal => fst mls
adamc@114 139 end
adamc@114 140 | inr idx' => hget ls' (snd mls) idx'
adamc@114 141 end
adamc@114 142 end.
adamc@125 143
adamc@125 144 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
adamc@125 145 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
adamc@125 146 | nil => fun _ hls2 => hls2
adamc@125 147 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
adamc@125 148 end.
adamc@194 149
adamc@194 150 Variable f : forall x, B x.
adamc@194 151
adamc@194 152 Fixpoint hmake (ls : list A) : hlist ls :=
adamc@194 153 match ls return hlist ls with
adamc@194 154 | nil => hnil
adamc@194 155 | x :: ls' => hcons _ (f x) (hmake ls')
adamc@194 156 end.
adamc@114 157 End hlist.
adamc@114 158
adamc@125 159 Implicit Arguments hnil [A B].
adamc@125 160 Implicit Arguments hcons [A B x ls].
adamc@114 161 Implicit Arguments hget [A B elm ls].
adamc@125 162 Implicit Arguments happ [A B ls1 ls2].
adamc@194 163 Implicit Arguments hmake [A B].
adamc@125 164
adamc@126 165 Implicit Arguments hfirst [A elm x ls].
adamc@126 166 Implicit Arguments hnext [A elm x ls].
adamc@126 167
adamc@125 168 Infix ":::" := hcons (right associativity, at level 60).
adamc@125 169 Infix "+++" := happ (right associativity, at level 60).
adamc@163 170
adamc@163 171 Section hmap.
adamc@163 172 Variable A : Type.
adamc@163 173 Variables B1 B2 : A -> Type.
adamc@163 174
adamc@163 175 Variable f : forall x, B1 x -> B2 x.
adamc@163 176
adamc@163 177 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
adamc@163 178 match ls return hlist B1 ls -> hlist B2 ls with
adamc@163 179 | nil => fun _ => hnil
adamc@163 180 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
adamc@163 181 end.
adamc@179 182
adamc@179 183 Implicit Arguments hmap [ls].
adamc@179 184
adamc@179 185 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
adamc@179 186 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
adamc@179 187 induction ls1; crush.
adamc@179 188 Qed.
adamc@163 189 End hmap.
adamc@163 190
adamc@163 191 Implicit Arguments hmap [A B1 B2 ls].