Mercurial > cpdt > repo

annotate src/Generic.v @ 216:d1464997078d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch DepList to inductive, not recursive, types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:28:47 -0500
parents f8bcd33bdd91
children dbac52f5bce1
rev   line source
adamc@216 1 (* Copyright (c) 2008-2009, Adam Chlipala
adamc@193 2 *
adamc@193 3 * This work is licensed under a
adamc@193 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@193 5 * Unported License.
adamc@193 6 * The license text is available at:
adamc@193 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@193 8 *)
adamc@193 9
adamc@193 10 (* begin hide *)
adamc@195 11 Require Import String List.
adamc@193 12
adamc@193 13 Require Import Tactics DepList.
adamc@193 14
adamc@193 15 Set Implicit Arguments.
adamc@193 16 (* end hide *)
adamc@193 17
adamc@193 18
adamc@193 19 (** %\part{Chapters to be Moved Earlier}
adamc@193 20
adamc@193 21 \chapter{Generic Programming}% *)
adamc@193 22
adamc@193 23 (** TODO: Prose for this chapter *)
adamc@193 24
adamc@193 25
adamc@195 26 (** * Reflecting Datatype Definitions *)
adamc@193 27
adamc@198 28 (* EX: Define a reflected representation of simple algebraic datatypes. *)
adamc@198 29
adamc@198 30 (* begin thide *)
adamc@193 31 Record constructor : Type := Con {
adamc@193 32 nonrecursive : Type;
adamc@193 33 recursive : nat
adamc@193 34 }.
adamc@193 35
adamc@193 36 Definition datatype := list constructor.
adamc@193 37
adamc@193 38 Definition Empty_set_dt : datatype := nil.
adamc@193 39 Definition unit_dt : datatype := Con unit 0 :: nil.
adamc@193 40 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
adamc@193 41 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
adamc@193 42 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
adamc@198 43 (* end thide *)
adamc@193 44
adamc@193 45 Section tree.
adamc@193 46 Variable A : Type.
adamc@193 47
adamc@193 48 Inductive tree : Type :=
adamc@193 49 | Leaf : A -> tree
adamc@193 50 | Node : tree -> tree -> tree.
adamc@193 51 End tree.
adamc@193 52
adamc@198 53 (* begin thide *)
adamc@193 54 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
adamc@193 55
adamc@193 56 Section denote.
adamc@193 57 Variable T : Type.
adamc@193 58
adamc@193 59 Definition constructorDenote (c : constructor) :=
adamc@193 60 nonrecursive c -> ilist T (recursive c) -> T.
adamc@193 61
adamc@193 62 Definition datatypeDenote := hlist constructorDenote.
adamc@193 63 End denote.
adamc@198 64 (* end thide *)
adamc@193 65
adamc@193 66 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
adamc@193 67 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
adamc@193 68 Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
adamc@193 69 Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
adamc@193 70
adamc@198 71 (* begin thide *)
adamc@193 72 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
adamc@216 73 HNil.
adamc@193 74 Definition unit_den : datatypeDenote unit unit_dt :=
adamc@216 75 [!, ! ~> tt] ::: HNil.
adamc@193 76 Definition bool_den : datatypeDenote bool bool_dt :=
adamc@216 77 [!, ! ~> true] ::: [!, ! ~> false] ::: HNil.
adamc@193 78 Definition nat_den : datatypeDenote nat nat_dt :=
adamc@216 79 [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: HNil.
adamc@193 80 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
adamc@216 81 [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: HNil.
adamc@193 82 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
adamc@216 83 [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: HNil.
adamc@198 84 (* end thide *)
adamc@194 85
adamc@195 86
adamc@195 87 (** * Recursive Definitions *)
adamc@195 88
adamc@198 89 (* EX: Define a generic [size] function. *)
adamc@198 90
adamc@198 91 (* begin thide *)
adamc@194 92 Definition fixDenote (T : Type) (dt : datatype) :=
adamc@194 93 forall (R : Type), datatypeDenote R dt -> (T -> R).
adamc@194 94
adamc@194 95 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
adamc@194 96 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
adamc@194 97
adamc@194 98 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
adamc@194 99 fun R _ emp => match emp with end.
adamc@194 100 Eval compute in size Empty_set_fix.
adamc@194 101
adamc@194 102 Definition unit_fix : fixDenote unit unit_dt :=
adamc@216 103 fun R cases _ => (hhd cases) tt INil.
adamc@194 104 Eval compute in size unit_fix.
adamc@194 105
adamc@194 106 Definition bool_fix : fixDenote bool bool_dt :=
adamc@194 107 fun R cases b => if b
adamc@216 108 then (hhd cases) tt INil
adamc@216 109 else (hhd (htl cases)) tt INil.
adamc@194 110 Eval compute in size bool_fix.
adamc@194 111
adamc@194 112 Definition nat_fix : fixDenote nat nat_dt :=
adamc@194 113 fun R cases => fix F (n : nat) : R :=
adamc@194 114 match n with
adamc@216 115 | O => (hhd cases) tt INil
adamc@216 116 | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
adamc@194 117 end.
adamc@194 118 Eval cbv beta iota delta -[plus] in size nat_fix.
adamc@194 119
adamc@194 120 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
adamc@194 121 fun R cases => fix F (ls : list A) : R :=
adamc@194 122 match ls with
adamc@216 123 | nil => (hhd cases) tt INil
adamc@216 124 | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
adamc@194 125 end.
adamc@194 126 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@194 127
adamc@194 128 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
adamc@194 129 fun R cases => fix F (t : tree A) : R :=
adamc@194 130 match t with
adamc@216 131 | Leaf x => (hhd cases) x INil
adamc@216 132 | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
adamc@194 133 end.
adamc@194 134 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@198 135 (* end thide *)
adamc@195 136
adamc@195 137
adamc@195 138 (** ** Pretty-Printing *)
adamc@195 139
adamc@198 140 (* EX: Define a generic pretty-printing function. *)
adamc@198 141
adamc@198 142 (* begin thide *)
adamc@195 143 Record print_constructor (c : constructor) : Type := PI {
adamc@195 144 printName : string;
adamc@195 145 printNonrec : nonrecursive c -> string
adamc@195 146 }.
adamc@195 147
adamc@195 148 Notation "^" := (PI (Con _ _)).
adamc@195 149
adamc@195 150 Definition print_datatype := hlist print_constructor.
adamc@195 151
adamc@195 152 Open Local Scope string_scope.
adamc@195 153
adamc@195 154 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
adamc@195 155 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
adamc@195 156 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
adamc@195 157 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
adamc@198 158 (* end thide *)
adamc@195 159
adamc@216 160 Eval compute in print HNil Empty_set_fix.
adamc@216 161 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
adamc@195 162 Eval compute in print (^ "true" (fun _ => "")
adamc@195 163 ::: ^ "false" (fun _ => "")
adamc@216 164 ::: HNil) bool_fix.
adamc@195 165
adamc@195 166 Definition print_nat := print (^ "O" (fun _ => "")
adamc@195 167 ::: ^ "S" (fun _ => "")
adamc@216 168 ::: HNil) nat_fix.
adamc@195 169 Eval cbv beta iota delta -[append] in print_nat.
adamc@195 170 Eval simpl in print_nat 0.
adamc@195 171 Eval simpl in print_nat 1.
adamc@195 172 Eval simpl in print_nat 2.
adamc@195 173
adamc@195 174 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 175 print (^ "nil" (fun _ => "")
adamc@195 176 ::: ^ "cons" pr
adamc@216 177 ::: HNil) (@list_fix A).
adamc@195 178 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 179 print (^ "Leaf" pr
adamc@195 180 ::: ^ "Node" (fun _ => "")
adamc@216 181 ::: HNil) (@tree_fix A).
adamc@196 182
adamc@196 183
adamc@196 184 (** ** Mapping *)
adamc@196 185
adamc@198 186 (* EX: Define a generic [map] function. *)
adamc@198 187
adamc@198 188 (* begin thide *)
adamc@196 189 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T :=
adamc@196 190 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
adamc@196 191 (fun _ c x r => f (c x r)) dd).
adamc@198 192 (* end thide *)
adamc@196 193
adamc@196 194 Eval compute in map Empty_set_den Empty_set_fix.
adamc@196 195 Eval compute in map unit_den unit_fix.
adamc@196 196 Eval compute in map bool_den bool_fix.
adamc@196 197 Eval compute in map nat_den nat_fix.
adamc@196 198 Eval compute in fun A => map (list_den A) (@list_fix A).
adamc@196 199 Eval compute in fun A => map (tree_den A) (@tree_fix A).
adamc@196 200
adamc@196 201 Definition map_nat := map nat_den nat_fix.
adamc@196 202 Eval simpl in map_nat S 0.
adamc@196 203 Eval simpl in map_nat S 1.
adamc@196 204 Eval simpl in map_nat S 2.
adamc@196 205
adamc@196 206
adamc@196 207 (** * Proving Theorems about Recursive Definitions *)
adamc@196 208
adamc@198 209 (* begin thide *)
adamc@196 210 Section ok.
adamc@196 211 Variable T : Type.
adamc@196 212 Variable dt : datatype.
adamc@196 213
adamc@196 214 Variable dd : datatypeDenote T dt.
adamc@196 215 Variable fx : fixDenote T dt.
adamc@196 216
adamc@196 217 Definition datatypeDenoteOk :=
adamc@196 218 forall P : T -> Prop,
adamc@196 219 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@215 220 (forall i : fin (recursive c), P (get r i))
adamc@196 221 -> P ((hget dd m) x r))
adamc@196 222 -> forall v, P v.
adamc@196 223
adamc@196 224 Definition fixDenoteOk :=
adamc@196 225 forall (R : Type) (cases : datatypeDenote R dt)
adamc@196 226 c (m : member c dt)
adamc@196 227 (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@216 228 fx cases ((hget dd m) x r)
adamc@216 229 = (hget cases m) x (imap (fx cases) r).
adamc@196 230 End ok.
adamc@196 231
adamc@196 232 Implicit Arguments datatypeDenoteOk [T dt].
adamc@196 233
adamc@196 234 Lemma foldr_plus : forall n (ils : ilist nat n),
adamc@196 235 foldr plus 1 ils > 0.
adamc@216 236 induction ils; crush.
adamc@196 237 Qed.
adamc@198 238 (* end thide *)
adamc@196 239
adamc@197 240 Theorem size_positive : forall T dt
adamc@197 241 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 242 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@196 243 (v : T),
adamc@196 244 size fx v > 0.
adamc@198 245 (* begin thide *)
adamc@196 246 Hint Rewrite hget_hmake : cpdt.
adamc@196 247 Hint Resolve foldr_plus.
adamc@196 248
adamc@197 249 unfold size; intros; pattern v; apply dok; crush.
adamc@196 250 Qed.
adamc@198 251 (* end thide *)
adamc@197 252
adamc@197 253 Theorem map_id : forall T dt
adamc@197 254 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 255 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@197 256 (v : T),
adamc@197 257 map dd fx (fun x => x) v = v.
adamc@198 258 (* begin thide *)
adamc@197 259 Hint Rewrite hget_hmap : cpdt.
adamc@197 260
adamc@197 261 unfold map; intros; pattern v; apply dok; crush.
adamc@197 262 match goal with
adamc@197 263 | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2
adamc@197 264 end; crush.
adamc@197 265
adamc@197 266 induction (recursive c); crush.
adamc@216 267 dep_destruct r; reflexivity.
adamc@216 268 dep_destruct r; crush.
adamc@216 269 rewrite (H First).
adamc@197 270 f_equal.
adamc@197 271 apply IHn; crush.
adamc@216 272 apply (H (Next i)).
adamc@197 273 Qed.
adamc@198 274 (* end thide *)