adamc@216: (* Copyright (c) 2008-2009, Adam Chlipala
adamc@193:  * 
adamc@193:  * This work is licensed under a
adamc@193:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@193:  * Unported License.
adamc@193:  * The license text is available at:
adamc@193:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@193:  *)
adamc@193: 
adamc@193: (* begin hide *)
adamc@195: Require Import String List.
adamc@193: 
adamc@193: Require Import Tactics DepList.
adamc@193: 
adamc@193: Set Implicit Arguments.
adamc@193: (* end hide *)
adamc@193: 
adamc@193: 
adamc@193: (** %\part{Chapters to be Moved Earlier}
adamc@193: 
adamc@193: \chapter{Generic Programming}% *)
adamc@193: 
adamc@193: (** TODO: Prose for this chapter *)
adamc@193: 
adamc@193: 
adamc@195: (** * Reflecting Datatype Definitions *)
adamc@193: 
adamc@198: (* EX: Define a reflected representation of simple algebraic datatypes. *)
adamc@198: 
adamc@198: (* begin thide *)
adamc@193: Record constructor : Type := Con {
adamc@193:   nonrecursive : Type;
adamc@193:   recursive : nat
adamc@193: }.
adamc@193: 
adamc@193: Definition datatype := list constructor.
adamc@193: 
adamc@193: Definition Empty_set_dt : datatype := nil.
adamc@193: Definition unit_dt : datatype := Con unit 0 :: nil.
adamc@193: Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
adamc@193: Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
adamc@193: Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
adamc@198: (* end thide *)
adamc@193: 
adamc@193: Section tree.
adamc@193:   Variable A : Type.
adamc@193: 
adamc@193:   Inductive tree : Type :=
adamc@193:   | Leaf : A -> tree
adamc@193:   | Node : tree -> tree -> tree.
adamc@193: End tree.
adamc@193: 
adamc@198: (* begin thide *)
adamc@193: Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
adamc@193: 
adamc@193: Section denote.
adamc@193:   Variable T : Type.
adamc@193: 
adamc@193:   Definition constructorDenote (c : constructor) :=
adamc@193:     nonrecursive c -> ilist T (recursive c) -> T.
adamc@193: 
adamc@193:   Definition datatypeDenote := hlist constructorDenote.
adamc@193: End denote.
adamc@198: (* end thide *)
adamc@193: 
adamc@193: Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
adamc@193: Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
adamc@193: Notation "[ ! , r # n ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ n)).
adamc@193: Notation "[ v , r # n ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ n)).
adamc@193: 
adamc@198: (* begin thide *)
adamc@193: Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
adamc@216:   HNil.
adamc@193: Definition unit_den : datatypeDenote unit unit_dt :=
adamc@216:   [!, ! ~> tt] ::: HNil.
adamc@193: Definition bool_den : datatypeDenote bool bool_dt :=
adamc@216:   [!, ! ~> true] ::: [!, ! ~> false] ::: HNil.
adamc@193: Definition nat_den : datatypeDenote nat nat_dt :=
adamc@216:   [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: HNil.
adamc@193: Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
adamc@216:   [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: HNil.
adamc@193: Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
adamc@216:   [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: HNil.
adamc@198: (* end thide *)
adamc@194: 
adamc@195: 
adamc@195: (** * Recursive Definitions *)
adamc@195: 
adamc@198: (* EX: Define a generic [size] function. *)
adamc@198: 
adamc@198: (* begin thide *)
adamc@194: Definition fixDenote (T : Type) (dt : datatype) :=
adamc@194:   forall (R : Type), datatypeDenote R dt -> (T -> R).
adamc@194: 
adamc@194: Definition size T dt (fx : fixDenote T dt) : T -> nat :=
adamc@194:   fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
adamc@194: 
adamc@194: Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
adamc@194:   fun R _ emp => match emp with end.
adamc@194: Eval compute in size Empty_set_fix.
adamc@194: 
adamc@194: Definition unit_fix : fixDenote unit unit_dt :=
adamc@216:   fun R cases _ => (hhd cases) tt INil.
adamc@194: Eval compute in size unit_fix.
adamc@194: 
adamc@194: Definition bool_fix : fixDenote bool bool_dt :=
adamc@194:   fun R cases b => if b
adamc@216:     then (hhd cases) tt INil
adamc@216:     else (hhd (htl cases)) tt INil.
adamc@194: Eval compute in size bool_fix.
adamc@194: 
adamc@194: Definition nat_fix : fixDenote nat nat_dt :=
adamc@194:   fun R cases => fix F (n : nat) : R :=
adamc@194:     match n with
adamc@216:       | O => (hhd cases) tt INil
adamc@216:       | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
adamc@194:     end.
adamc@194: Eval cbv beta iota delta -[plus] in size nat_fix.
adamc@194: 
adamc@194: Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
adamc@194:   fun R cases => fix F (ls : list A) : R :=
adamc@194:     match ls with
adamc@216:       | nil => (hhd cases) tt INil
adamc@216:       | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
adamc@194:     end.
adamc@194: Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@194: 
adamc@194: Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
adamc@194:   fun R cases => fix F (t : tree A) : R :=
adamc@194:     match t with
adamc@216:       | Leaf x => (hhd cases) x INil
adamc@216:       | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
adamc@194:     end.
adamc@194: Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@198: (* end thide *)
adamc@195: 
adamc@195: 
adamc@195: (** ** Pretty-Printing *)
adamc@195: 
adamc@198: (* EX: Define a generic pretty-printing function. *)
adamc@198: 
adamc@198: (* begin thide *)
adamc@195: Record print_constructor (c : constructor) : Type := PI {
adamc@195:   printName : string;
adamc@195:   printNonrec : nonrecursive c -> string
adamc@195: }.
adamc@195: 
adamc@195: Notation "^" := (PI (Con _ _)).
adamc@195: 
adamc@195: Definition print_datatype := hlist print_constructor.
adamc@195: 
adamc@195: Open Local Scope string_scope.
adamc@195: 
adamc@195: Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
adamc@195:   fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
adamc@195:     (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
adamc@195:       ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
adamc@198: (* end thide *)
adamc@195: 
adamc@216: Eval compute in print HNil Empty_set_fix.
adamc@216: Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
adamc@195: Eval compute in print (^ "true" (fun _ => "")
adamc@195:   ::: ^ "false" (fun _ => "")
adamc@216:   ::: HNil) bool_fix.
adamc@195: 
adamc@195: Definition print_nat := print (^ "O" (fun _ => "")
adamc@195:   ::: ^ "S" (fun _ => "")
adamc@216:   ::: HNil) nat_fix.
adamc@195: Eval cbv beta iota delta -[append] in print_nat.
adamc@195: Eval simpl in print_nat 0.
adamc@195: Eval simpl in print_nat 1.
adamc@195: Eval simpl in print_nat 2.
adamc@195: 
adamc@195: Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195:   print (^ "nil" (fun _ => "")
adamc@195:   ::: ^ "cons" pr
adamc@216:   ::: HNil) (@list_fix A).
adamc@195: Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195:   print (^ "Leaf" pr
adamc@195:   ::: ^ "Node" (fun _ => "")
adamc@216:   ::: HNil) (@tree_fix A).
adamc@196: 
adamc@196: 
adamc@196: (** ** Mapping *)
adamc@196: 
adamc@198: (* EX: Define a generic [map] function. *)
adamc@198: 
adamc@198: (* begin thide *)
adamc@196: Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T) : T -> T :=
adamc@196:   fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
adamc@196:     (fun _ c x r => f (c x r)) dd).
adamc@198: (* end thide *)
adamc@196: 
adamc@196: Eval compute in map Empty_set_den Empty_set_fix.
adamc@196: Eval compute in map unit_den unit_fix.
adamc@196: Eval compute in map bool_den bool_fix.
adamc@196: Eval compute in map nat_den nat_fix.
adamc@196: Eval compute in fun A => map (list_den A) (@list_fix A).
adamc@196: Eval compute in fun A => map (tree_den A) (@tree_fix A).
adamc@196: 
adamc@196: Definition map_nat := map nat_den nat_fix.
adamc@196: Eval simpl in map_nat S 0.
adamc@196: Eval simpl in map_nat S 1.
adamc@196: Eval simpl in map_nat S 2.
adamc@196: 
adamc@196: 
adamc@196: (** * Proving Theorems about Recursive Definitions *)
adamc@196: 
adamc@198: (* begin thide *)
adamc@196: Section ok.
adamc@196:   Variable T : Type.
adamc@196:   Variable dt : datatype.
adamc@196: 
adamc@196:   Variable dd : datatypeDenote T dt.
adamc@196:   Variable fx : fixDenote T dt.
adamc@196: 
adamc@196:   Definition datatypeDenoteOk :=
adamc@196:     forall P : T -> Prop,
adamc@196:       (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@215:         (forall i : fin (recursive c), P (get r i))
adamc@196:         -> P ((hget dd m) x r))
adamc@196:       -> forall v, P v.
adamc@196: 
adamc@196:   Definition fixDenoteOk :=
adamc@196:     forall (R : Type) (cases : datatypeDenote R dt)
adamc@196:       c (m : member c dt)
adamc@196:       (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@216:       fx cases ((hget dd m) x r)
adamc@216:       = (hget cases m) x (imap (fx cases) r).
adamc@196: End ok.
adamc@196: 
adamc@196: Implicit Arguments datatypeDenoteOk [T dt].
adamc@196: 
adamc@196: Lemma foldr_plus : forall n (ils : ilist nat n),
adamc@196:   foldr plus 1 ils > 0.
adamc@216:   induction ils; crush.
adamc@196: Qed.
adamc@198: (* end thide *)
adamc@196: 
adamc@197: Theorem size_positive : forall T dt
adamc@197:   (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197:   (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@196:   (v : T),
adamc@196:   size fx v > 0.
adamc@198: (* begin thide *)
adamc@196:   Hint Rewrite hget_hmake : cpdt.
adamc@196:   Hint Resolve foldr_plus.
adamc@196:  
adamc@197:   unfold size; intros; pattern v; apply dok; crush.
adamc@196: Qed.
adamc@198: (* end thide *)
adamc@197: 
adamc@197: Theorem map_id : forall T dt
adamc@197:   (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197:   (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@197:   (v : T),
adamc@197:   map dd fx (fun x => x) v = v.
adamc@198: (* begin thide *)
adamc@197:   Hint Rewrite hget_hmap : cpdt.
adamc@197: 
adamc@197:   unfold map; intros; pattern v; apply dok; crush.
adamc@197:   match goal with
adamc@197:     | [ |- hget _ _ _ ?R1 = hget _ _ _ ?R2 ] => replace R1 with R2
adamc@197:   end; crush.
adamc@197: 
adamc@197:   induction (recursive c); crush.
adamc@216:   dep_destruct r; reflexivity.
adamc@216:   dep_destruct r; crush.
adamc@216:   rewrite (H First).
adamc@197:   f_equal.
adamc@197:   apply IHn; crush.
adamc@216:   apply (H (Next i)).
adamc@197: Qed.
adamc@198: (* end thide *)