Mercurial > cpdt > repo
changeset 302:7b38729be069
Tweak mark-up to support coqdoc 8.3
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 17 Jan 2011 15:12:30 -0500 |
| parents | f4768d5a75eb |
| children | 921d6936c11d |
| files | .hgignore Makefile src/Coinductive.v src/DataStruct.v src/DeBruijn.v src/Equality.v src/Extensional.v src/Generic.v src/Hoas.v src/InductiveTypes.v src/Intensional.v src/Interps.v src/Large.v src/Match.v src/MoreDep.v src/Predicates.v src/Reflection.v src/StackMachine.v src/Subset.v src/Universes.v |
| diffstat | 20 files changed, 341 insertions(+), 170 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgignore Mon Jan 17 11:42:09 2011 -0500 +++ b/.hgignore Mon Jan 17 15:12:30 2011 -0500 @@ -25,3 +25,5 @@ *.aux *.dvi *.log +*.tex +*.toc
--- a/Makefile Mon Jan 17 11:42:09 2011 -0500 +++ b/Makefile Mon Jan 17 15:12:30 2011 -0500 @@ -37,7 +37,7 @@ -o ../latex/cpdt.tex latex/%.tex: src/%.v src/%.glob - cd src ; coqdoc --interpolate --latex -s \ + cd src ; coqdoc --interpolate --latex \ -p "\usepackage{url,amsmath,amssymb}" \ $*.v -o ../latex/$*.tex
--- a/src/Coinductive.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Coinductive.v Mon Jan 17 15:12:30 2011 -0500 @@ -77,7 +77,8 @@ (** %\vspace{-.15in}% [[ = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil : list nat - ]] *) + ]] + *) Eval simpl in approx trues 10. (** %\vspace{-.15in}% [[ @@ -324,7 +325,8 @@ (** [[ Guarded. - ]] *) + ]] + *) Abort. (* end thide *)
--- a/src/DataStruct.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/DataStruct.v Mon Jan 17 15:12:30 2011 -0500 @@ -136,26 +136,30 @@ (** %\vspace{-.15in}% [[ Cons 0 (Cons 1 (Cons 2 Nil)) : ilist nat 3 -]] *) +]] +*) (* begin thide *) Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First. (** %\vspace{-.15in}% [[ = 0 : nat -]] *) +]] +*) Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First). (** %\vspace{-.15in}% [[ = 1 : nat -]] *) +]] +*) Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)). (** %\vspace{-.15in}% [[ = 2 : nat -]] *) +]] +*) (* end thide *) (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *) @@ -258,13 +262,15 @@ (** %\vspace{-.15in}% [[ = 5 : (fun T : Set => T) nat -]] *) +]] +*) Eval simpl in hget someValues (MNext MFirst). (** %\vspace{-.15in}% [[ = true : (fun T : Set => T) bool -]] *) +]] +*) (** We can also build indexed lists of pairs in this way. *) @@ -324,32 +330,37 @@ (** %\vspace{-.15in}% [[ = tt : typeDenote Unit -]] *) +]] +*) Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil. (** %\vspace{-.15in}% [[ = fun x : unit => x : typeDenote (Arrow Unit Unit) -]] *) +]] +*) Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var (MNext MFirst)))) MNil. (** %\vspace{-.15in}% [[ = fun x _ : unit => x : typeDenote (Arrow Unit (Arrow Unit Unit)) -]] *) +]] +*) Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil. (** %\vspace{-.15in}% [[ = fun _ x0 : unit => x0 : typeDenote (Arrow Unit (Arrow Unit Unit)) -]] *) +]] +*) Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil. (** %\vspace{-.15in}% [[ = tt : typeDenote Unit -]] *) +]] +*) (* end thide *)
--- a/src/DeBruijn.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/DeBruijn.v Mon Jan 17 15:12:30 2011 -0500 @@ -318,7 +318,8 @@ [[ end; simp); eauto. - ]] *) + ]] + *) (** * Theorems *)
--- a/src/Equality.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Equality.v Mon Jan 17 15:12:30 2011 -0500 @@ -87,7 +87,8 @@ ============================ 0 = 0 - ]] *) + ]] + *) reflexivity. Qed. @@ -217,7 +218,8 @@ [[ reflexivity. - ]] *) + ]] + *) Qed. (* end thide *) @@ -268,7 +270,8 @@ User error: Cannot solve a second-order unification problem - ]] *) + ]] + *) Abort. (** Nonetheless, we can adapt the last manual proof to handle this theorem. *) @@ -291,7 +294,8 @@ simple destruct pf. User error: Cannot solve a second-order unification problem - ]] *) + ]] + *) Abort. @@ -429,7 +433,8 @@ fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 - ]] *) + ]] + *) reflexivity. @@ -716,7 +721,8 @@ ============================ x = y - ]] *) + ]] + *) destruct H. (** [[ @@ -727,7 +733,8 @@ ============================ x = y - ]] *) + ]] + *) rewrite H. (** [[ @@ -737,7 +744,8 @@ | refl_equal => y end = y - ]] *) + ]] + *) rewrite (UIP_refl _ _ x0); reflexivity. Qed. @@ -801,7 +809,8 @@ | 0 => True | S _ => True end = True - ]] *) + ]] + *) reflexivity.
--- a/src/Extensional.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Extensional.v Mon Jan 17 15:12:30 2011 -0500 @@ -343,19 +343,22 @@ (** %\vspace{-.15in}% [[ = fun var : type -> Type => x <- ^0; Halt x : Prog - ]] *) + ]] + *) Eval compute in CpsExp one. (** %\vspace{-.15in}% [[ = fun var : type -> Type => x <- ^1; Halt x : Prog - ]] *) + ]] + *) Eval compute in CpsExp zpo. (** %\vspace{-.15in}% [[ = fun var : type -> Type => x <- ^0; x0 <- ^1; x1 <- (x +^ x0); Halt x1 : Prog - ]] *) + ]] + *) Eval compute in CpsExp app_ident. (** %\vspace{-.15in}% [[ @@ -364,7 +367,8 @@ x <- ^0; x0 <- ^1; x1 <- (x +^ x0); kf <- (\ r, Halt r); p <- [x1, kf]; f @@ p : Prog - ]] *) + ]] + *) Eval compute in CpsExp app_ident'. (** %\vspace{-.15in}% [[ @@ -386,37 +390,43 @@ x1 <- (x +^ x0); kf <- (\ r0, Halt r0); p <- [x1, kf]; r @@ p); p <- [f0, kf]; f @@ p : Prog - ]] *) + ]] + *) Eval compute in ProgDenote (CpsExp zero). (** %\vspace{-.15in}% [[ = 0 : nat - ]] *) + ]] + *) Eval compute in ProgDenote (CpsExp one). (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in ProgDenote (CpsExp zpo). (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in ProgDenote (CpsExp app_ident). (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in ProgDenote (CpsExp app_ident'). (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) (** Our main inductive lemma about [cpsExp] needs a notion of compatibility between source-level and CPS-level values. We express compatibility with a %\textit{%#<i>#logical relation#</i>#%}%; that is, we define a binary relation by recursion on type structure, and the function case of the relation considers functions related if they map related arguments to related results. In detail, the function case is slightly more complicated, since it must deal with our continuation-based calling convention. *)
--- a/src/Generic.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Generic.v Mon Jan 17 15:12:30 2011 -0500 @@ -172,7 +172,8 @@ (** %\vspace{-.15in}% [[ = fun b : bool => if b then 1 else 1 : bool -> nat -]] *) +]] +*) Definition nat_fix : fixDenote nat nat_dt := fun R cases => fix F (n : nat) : R := @@ -190,7 +191,8 @@ | S n' => F n' + 1 end : nat -> nat -]] *) +]] +*) Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) := fun R cases => fix F (ls : list A) : R := @@ -207,7 +209,8 @@ | _ :: ls' => F ls' + 1 end : forall A : Type, list A -> nat -]] *) +]] +*) Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) := fun R cases => fix F (t : tree A) : R := @@ -224,7 +227,8 @@ | Node t1 t2 => F t1 + (F t2 + 1) end : forall A : Type, tree A -> n -]] *) +]] +*) (* end thide *) @@ -260,7 +264,8 @@ : forall (A : Type) (B1 B2 : A -> Type), (forall x : A, B1 x -> B2 x) -> forall ls : list A, hlist B1 ls -> hlist B2 ls -]] *) +]] +*) Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string := fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string) @@ -275,13 +280,15 @@ = fun emp : Empty_set => match emp return string with end : Empty_set -> string - ]] *) + ]] + *) Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix. (** %\vspace{-.15in}% [[ = fun _ : unit => "tt()" : unit -> string - ]] *) + ]] + *) Eval compute in print (^ "true" (fun _ => "") ::: ^ "false" (fun _ => "") @@ -289,7 +296,8 @@ (** %\vspace{-.15in}% [[ = fun b : bool => if b then "true()" else "false()" : bool -> s - ]] *) + ]] + *) Definition print_nat := print (^ "O" (fun _ => "") ::: ^ "S" (fun _ => "") @@ -302,25 +310,29 @@ | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")" end : nat -> string - ]] *) + ]] + *) Eval simpl in print_nat 0. (** %\vspace{-.15in}% [[ = "O()" : string - ]] *) + ]] + *) Eval simpl in print_nat 1. (** %\vspace{-.15in}% [[ = "S(, O())" : string - ]] *) + ]] + *) Eval simpl in print_nat 2. (** %\vspace{-.15in}% [[ = "S(, S(, O()))" : string - ]] *) + ]] + *) Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => print (^ "nil" (fun _ => "") @@ -334,7 +346,8 @@ | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")" end : forall A : Type, (A -> string) -> list A -> string - ]] *) + ]] + *) Eval cbv beta iota delta -[append] in fun A (pr : A -> string) => print (^ "Leaf" pr @@ -349,7 +362,8 @@ "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")" end : forall A : Type, (A -> string) -> tree A -> string - ]] *) + ]] + *) (** ** Mapping *) @@ -371,19 +385,22 @@ match emp return Empty_set with end : (Empty_set -> Empty_set) -> Empty_set -> Empty_set - ]] *) + ]] + *) Eval compute in map unit_den unit_fix. (** %\vspace{-.15in}% [[ = fun (f : unit -> unit) (_ : unit) => f tt : (unit -> unit) -> unit -> unit - ]] *) + ]] + *) Eval compute in map bool_den bool_fix. (** %\vspace{-.15in}% [[ = fun (f : bool -> bool) (b : bool) => if b then f true else f false : (bool -> bool) -> bool -> bool - ]] *) + ]] + *) Eval compute in map nat_den nat_fix. (** %\vspace{-.15in}% [[ @@ -394,7 +411,8 @@ | S n' => f (S (F n')) end : (nat -> nat) -> nat -> nat - ]] *) + ]] + *) Eval compute in fun A => map (list_den A) (@list_fix A). (** %\vspace{-.15in}% [[ @@ -405,7 +423,8 @@ | x :: ls' => f (x :: F ls') end : forall A : Type, (list A -> list A) -> list A -> list A - ]] *) + ]] + *) Eval compute in fun A => map (tree_den A) (@tree_fix A). (** %\vspace{-.15in}% [[ @@ -416,26 +435,30 @@ | Node t1 t2 => f (Node (F t1) (F t2)) end : forall A : Type, (tree A -> tree A) -> tree A -> tree A - ]] *) + ]] + *) Definition map_nat := map nat_den nat_fix. Eval simpl in map_nat S 0. (** %\vspace{-.15in}% [[ = 1%nat : nat - ]] *) + ]] + *) Eval simpl in map_nat S 1. (** %\vspace{-.15in}% [[ = 3%nat : nat - ]] *) + ]] + *) Eval simpl in map_nat S 2. (** %\vspace{-.15in}% [[ = 5%nat : nat - ]] *) + ]] + *) (** * Proving Theorems about Recursive Definitions *) @@ -523,7 +546,8 @@ (fun (x : constructor) (_ : nonrecursive x) (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v - ]] *) + ]] + *) apply dok; crush. (** [[
--- a/src/Hoas.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Hoas.v Mon Jan 17 15:12:30 2011 -0500 @@ -234,43 +234,50 @@ (** %\vspace{-.15in}% [[ = 0 : nat - ]] *) + ]] + *) Eval compute in CountVars one. (** %\vspace{-.15in}% [[ = 0 : nat - ]] *) + ]] + *) Eval compute in CountVars one_again. (** %\vspace{-.15in}% [[ = 0 : nat - ]] *) + ]] + *) Eval compute in CountVars ident. (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in CountVars app_ident. (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in CountVars app. (** %\vspace{-.15in}% [[ = 2 : nat - ]] *) + ]] + *) Eval compute in CountVars app_ident'. (** %\vspace{-.15in}% [[ = 3 : nat - ]] *) + ]] + *) (* EX: Define a function to count the number of occurrences of a single distinguished variable. *) @@ -306,25 +313,29 @@ (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in CountOne add_self. (** %\vspace{-.15in}% [[ = 2 : nat - ]] *) + ]] + *) Eval compute in CountOne app_zero. (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) Eval compute in CountOne app_ident1. (** %\vspace{-.15in}% [[ = 1 : nat - ]] *) + ]] + *) (* EX: Define a function to pretty-print [Exp]s as strings. *) @@ -368,43 +379,50 @@ (** %\vspace{-.15in}% [[ = "O"%string : string - ]] *) + ]] + *) Eval compute in ToString one. (** %\vspace{-.15in}% [[ = "S(O)"%string : string - ]] *) + ]] + *) Eval compute in ToString one_again. (** %\vspace{-.15in}% [[ = "(O) + (S(O))"%string : string - ]] *) + ]] + *) Eval compute in ToString ident. (** %\vspace{-.15in}% [[ = "(\x, x)"%string : string - ]] *) + ]] + *) Eval compute in ToString app_ident. (** %\vspace{-.15in}% [[ = "((\x, x)) ((O) + (S(O)))"%string : string - ]] *) + ]] + *) Eval compute in ToString app. (** %\vspace{-.15in}% [[ = "(\x, (\x', (x) (x')))"%string : string - ]] *) + ]] + *) Eval compute in ToString app_ident'. (** %\vspace{-.15in}% [[ = "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string : string - ]] *) + ]] + *) (* EX: Define a substitution function. *) @@ -435,27 +453,31 @@ (** %\vspace{-.15in}% [[ = fun var : type -> Type => Const' 1 : Exp Nat - ]] *) + ]] + *) Eval compute in Subst one add_self. (** %\vspace{-.15in}% [[ = fun var : type -> Type => Plus' (Const' 1) (Const' 1) : Exp Nat - ]] *) + ]] + *) Eval compute in Subst ident app_zero. (** %\vspace{-.15in}% [[ = fun var : type -> Type => App' (Abs' (fun X : var Nat => Var X)) (Const' 0) : Exp Nat - ]] *) + ]] + *) Eval compute in Subst one app_ident1. (** %\vspace{-.15in}% [[ = fun var : type -> Type => App' (Abs' (fun x : var Nat => Var x)) (Const' 1) : Exp Nat - ]] *) + ]] + *) (** * A Type Soundness Proof *)
--- a/src/InductiveTypes.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/InductiveTypes.v Mon Jan 17 15:12:30 2011 -0500 @@ -52,7 +52,8 @@ (** The goal changes to: [[ tt = tt -]] *) +]] +*) (** ...which we can discharge trivially. *) @@ -370,7 +371,8 @@ (forall n : nat_btree, P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) -> forall n : nat_btree, P n -]] *) +]] +*) (** * Parameterized Types *) @@ -895,7 +897,8 @@ Notation Scope "A /\ B" := and A B : type_scope (default interpretation) -]] *) +]] +*) Print and. (** %\vspace{-.15in}% [[ @@ -1102,7 +1105,8 @@ ============================ True -]] *) +]] +*) trivial. Qed.
--- a/src/Intensional.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Intensional.v Mon Jan 17 15:12:30 2011 -0500 @@ -189,7 +189,8 @@ fun (t : type) (E : Exp t) => forall var1 var2 : type -> Type, exp_equiv nil (E var1) (E var2) : forall t : type, Exp t -> Prop - ]] *) + ]] + *) Section vars. Variables var1 var2 : type -> Type.
--- a/src/Interps.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Interps.v Mon Jan 17 15:12:30 2011 -0500 @@ -116,43 +116,50 @@ (** %\vspace{-.15in}% [[ = 0 : typeDenote Nat - ]] *) + ]] + *) Eval compute in ExpDenote one. (** %\vspace{-.15in}% [[ = 1 : typeDenote Nat - ]] *) + ]] + *) Eval compute in ExpDenote zpo. (** %\vspace{-.15in}% [[ = 1 : typeDenote Nat - ]] *) + ]] + *) Eval compute in ExpDenote ident. (** %\vspace{-.15in}% [[ = fun x : nat => x : typeDenote (Nat --> Nat) - ]] *) + ]] + *) Eval compute in ExpDenote app_ident. (** %\vspace{-.15in}% [[ = 1 : typeDenote Nat - ]] *) + ]] + *) Eval compute in ExpDenote app. (** %\vspace{-.15in}% [[ = fun (x : nat -> nat) (x0 : nat) => x x0 : typeDenote ((Nat --> Nat) --> Nat --> Nat) - ]] *) + ]] + *) Eval compute in ExpDenote app_ident'. (** %\vspace{-.15in}% [[ = 1 : typeDenote Nat - ]] *) + ]] + *) (* EX: Define a constant-folding function for [Exp]s. *) @@ -347,19 +354,22 @@ (** %\vspace{-.15in}% [[ = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0) : typeDenote (Nat ** Nat --> Nat ** Nat) - ]] *) + ]] + *) Eval compute in ExpDenote zo. (** %\vspace{-.15in}% [[ = (0, 1) : typeDenote (Nat ** Nat) - ]] *) + ]] + *) Eval compute in ExpDenote swap_zo. (** %\vspace{-.15in}% [[ = (1, 0) : typeDenote (Nat ** Nat) - ]] *) + ]] + *) Eval cbv beta iota delta -[plus] in ExpDenote natOut. (** %\vspace{-.15in}% [[ @@ -368,31 +378,36 @@ | inr v => v + v end : typeDenote (Nat ++ Nat --> Nat) - ]] *) + ]] + *) Eval compute in ExpDenote ns1. (** %\vspace{-.15in}% [[ = inl nat 3 : typeDenote (Nat ++ Nat) - ]] *) + ]] + *) Eval compute in ExpDenote ns2. (** %\vspace{-.15in}% [[ = inr nat 5 : typeDenote (Nat ++ Nat) - ]] *) + ]] + *) Eval compute in ExpDenote natOut_ns1. (** %\vspace{-.15in}% [[ = 3 : typeDenote Nat - ]] *) + ]] + *) Eval compute in ExpDenote natOut_ns2. (** %\vspace{-.15in}% [[ = 10 : typeDenote Nat - ]] *) + ]] + *) (** We adapt the [cfold] function using the same basic dependent-types trick that we applied in an earlier chapter to a very similar function for a language without variables. *)
--- a/src/Large.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Large.v Mon Jan 17 15:12:30 2011 -0500 @@ -123,7 +123,8 @@ Error: The reference IHe1 was not found in the current environment. - ]] *) + ]] + *) Abort. @@ -184,7 +185,8 @@ Error: Expects a disjunctive pattern with 3 branches. - ]] *) + ]] + *) Abort. @@ -540,7 +542,8 @@ Time eauto 6. (** [[ Finished transaction in 0. secs (0.068004u,0.s) -]] *) +]] +*) Qed. @@ -722,7 +725,8 @@ (** %\vspace{-.15in}% [[ IntTheorems.unique_ident : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e - ]] *) + ]] + *) Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. exact IntTheorems.unique_ident.
--- a/src/Match.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Match.v Mon Jan 17 15:12:30 2011 -0500 @@ -129,7 +129,8 @@ (** [[ ============================ g (g (g x)) = g x - ]] *) + ]] + *) Abort. @@ -158,7 +159,8 @@ P (f x) subgoal 4 is: P (f x) - ]] *) + ]] + *) Abort. @@ -414,7 +416,8 @@ H4 : S x ============================ S x - ]] *) + ]] + *) assumption. Qed. @@ -479,7 +482,8 @@ end. User error: No matching clauses for match goal - ]] *) + ]] + *) Abort. (* end thide *) @@ -569,7 +573,8 @@ n := 3 : nat ============================ False - ]] *) + ]] + *) Abort. (* end thide *) @@ -601,7 +606,8 @@ l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat) ============================ False - ]] *) + ]] + *) Abort. (* end thide *) @@ -850,7 +856,8 @@ (Match (P:=P x) (imp_True (P:=True)))))))) : forall (P : nat -> Prop) (Q : Prop), (exists x : nat, P x /\ Q) --> Q /\ (exists x : nat, P x) -]] *) +]] +*) (** * Creating Unification Variables *)
--- a/src/MoreDep.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/MoreDep.v Mon Jan 17 15:12:30 2011 -0500 @@ -152,7 +152,8 @@ | S _ => A end - ]] *) + ]] + *) Definition hd n (ls : ilist (S n)) : A := hd' ls. (* end thide *) @@ -420,7 +421,8 @@ min_dec : forall n m : nat, {min n m = n} + {min n m = m} - ]] *) + ]] + *) Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n. induction t; crush; @@ -512,13 +514,15 @@ (** [[ Notation Scope "{ x : A & P }" := sigT (fun x : A => P) -]] *) +]] +*) Print sigT. (** [[ Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> sigT P -]] *) +]] +*) (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
--- a/src/Predicates.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Predicates.v Mon Jan 17 15:12:30 2011 -0500 @@ -23,12 +23,14 @@ Print unit. (** %\vspace{-.15in}% [[ Inductive unit : Set := tt : unit -]] *) +]] +*) Print True. (** %\vspace{-.15in}% [[ Inductive True : Prop := I : True -]] *) +]] +*) (** Recall that [unit] is the type with only one value, and [True] is the proposition that always holds. Despite this superficial difference between the two concepts, in both cases we can use the same inductive definition mechanism. The connection goes further than this. We see that we arrive at the definition of [True] by replacing [unit] by [True], [tt] by [I], and [Set] by [Prop]. The first two of these differences are superficial changes of names, while the third difference is the crucial one for separating programs from proofs. A term [T] of type [Set] is a type of programs, and a term of type [T] is a program. A term [T] of type [Prop] is a logical proposition, and its proofs are of type [T]. @@ -120,7 +122,8 @@ (** [[ ============================ 2 + 2 = 5 -> False - ]] *) + ]] + *) crush. (* end thide *) @@ -214,7 +217,8 @@ H : Q ============================ Q \/ P - ]] *) + ]] + *) left; assumption. (* end thide *) @@ -366,7 +370,8 @@ [[ ============================ 1 + 1 = 2 - ]] *) + ]] + *) reflexivity. (* end thide *) @@ -641,7 +646,8 @@ (** [[ ============================ even (S (S (n0 + m))) - ]] *) + ]] + *) constructor. (** [[ @@ -754,7 +760,8 @@ SearchRewrite (_ + S _). (** %\vspace{-.15in}% [[ plus_n_Sm : forall n m : nat, S (n + m) = n + S m - ]] *) + ]] + *) rewrite <- plus_n_Sm in H0. @@ -919,7 +926,8 @@ match goal with | [ |- context[eq_nat_dec ?X ?Y] ] => destruct (eq_nat_dec X Y) end -]] #</li># +]] + #</li># %\item%#<li># You probably do not want to use an inductive definition for compatibility of variable assignments and typings.#</li># %\item%#<li># The [Tactics] module from this book contains a variant [crush'] of [crush]. [crush'] takes two arguments. The first argument is a list of lemmas and other functions to be tried automatically in %``%#"#forward reasoning#"#%''% style, where we add new facts without being sure yet that they link into a proof of the conclusion. The second argument is a list of predicates on which inversion should be attempted automatically. For instance, running [crush' (lemma1, lemma2) pred] will search for chances to apply [lemma1] and [lemma2] to hypotheses that are already available, adding the new concluded fact if suitable hypotheses can be found. Inversion will be attempted on any hypothesis using [pred], but only those inversions that narrow the field of possibilities to one possible rule will be kept. The format of the list arguments to [crush'] is that you can pass an empty list as [tt], a singleton list as the unadorned single element, and a multiple-element list as a tuple of the elements.#</li># %\item%#<li># If you want [crush'] to apply polymorphic lemmas, you may have to do a little extra work, if the type parameter is not a free variable of your proof context (so that [crush'] does not know to try it). For instance, if you define a polymorphic map insert function [assign] of some type [forall T : Set, ...], and you want particular applications of [assign] added automatically with type parameter [U], you would need to include [assign] in the lemma list as [assign U] (if you have implicit arguments off) or [assign (T := U)] or [@assign U] (if you have implicit arguments on).#</li>#
--- a/src/Reflection.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Reflection.v Mon Jan 17 15:12:30 2011 -0500 @@ -593,7 +593,8 @@ (And Truth (And Truth (And Truth (And Truth Falsehood)))))) Falsehood)) : True /\ True /\ True /\ True /\ True /\ True /\ False --> False - ]] *) + ]] + *) Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False. tauto. @@ -616,7 +617,8 @@ and_ind (fun (_ : True) (H11 : False) => False_ind False H11) H9) H7) H5) H3) H1) H : True /\ True /\ True /\ True /\ True /\ True /\ False -> False - ]] *) + ]] + *) (** * Exercises *)
--- a/src/StackMachine.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/StackMachine.v Mon Jan 17 15:12:30 2011 -0500 @@ -311,9 +311,11 @@ progDenote ((IConst n :: nil) ++ p) s = progDenote p (expDenote (Const n) :: s) -]] *) +]] +*) unfold expDenote. + (** [[ n : nat s : stack @@ -529,7 +531,8 @@ (** [[ app_nil_end : forall (A : Type) (l : list A), l = l ++ nil -]] *) +]] +*) rewrite (app_nil_end (compile e)). @@ -827,7 +830,8 @@ (TCons (TIBinop ts b) (TNil (res :: ts)))) end : forall t : type, texp t -> forall ts : tstack, tprog ts (t :: ts) -]] *) +]] +*) (** We can check that the compiler generates programs that behave appropriately on our sample programs from above: *)
--- a/src/Subset.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Subset.v Mon Jan 17 15:12:30 2011 -0500 @@ -150,7 +150,8 @@ "{ x : A | P }" := sig (fun x : A => P) : type_scope (default interpretation) - ]] *) + ]] + *) Definition pred_strong2 (s : {n : nat | n > 0}) : nat := match s with @@ -165,7 +166,8 @@ = 1 : nat - ]] *) + ]] + *) Extraction pred_strong2. @@ -200,7 +202,8 @@ = exist (fun m : nat => 2 = S m) 1 (refl_equal 2) : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m} - ]] *) + ]] + *) (** The function [proj1_sig] extracts the base value from a subset type. It turns out that we need to include an explicit [return] clause here, since Coq's heuristics are not smart enough to propagate the result type that we wrote earlier. @@ -330,7 +333,8 @@ = [1] : {m : nat | 2 = S m} - ]] *) + ]] + *) (** * Decidable Proposition Types *) @@ -370,14 +374,16 @@ = Yes : {2 = 2} + {2 <> 2} - ]] *) + ]] + *) Eval compute in eq_nat_dec 2 3. (** %\vspace{-.15in}% [[ = No : {2 = 2} + {2 <> 2} - ]] *) + ]] + *) (** Our definition extracts to reasonable OCaml code. *) @@ -475,14 +481,16 @@ = Yes : {In 2 (1 :: 2 :: nil)} + {~ In 2 (1 :: 2 :: nil)} - ]] *) + ]] + *) Eval compute in In_dec eq_nat_dec 3 (1 :: 2 :: nil). (** %\vspace{-.15in}% [[ = No : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)} - ]] *) + ]] + *) (** [In_dec] has a reasonable extraction to OCaml. *) @@ -541,7 +549,8 @@ = [[1]] : {{m | 2 = S m}} - ]] *) + ]] + *) Eval compute in pred_strong7 0. (** %\vspace{-.15in}% [[ @@ -558,7 +567,8 @@ inleft : A -> A + {B} | inright : B -> A + {B} For inleft: Argument A is implicit For inright: Argument B is implicit -]] *) +]] +*) (** We add notations for easy use of the [sumor] constructors. The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *) @@ -580,14 +590,16 @@ = [[[1]]] : {m : nat | 2 = S m} + {2 = 0} - ]] *) + ]] + *) Eval compute in pred_strong8 0. (** %\vspace{-.15in}% [[ = !! : {m : nat | 0 = S m} + {0 = 0} - ]] *) + ]] + *) (** * Monadic Notations *) @@ -706,19 +718,22 @@ (** %\vspace{-.15in}% [[ = [[TNat]] : {{t | hasType (Nat 0) t}} - ]] *) + ]] + *) Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)). (** %\vspace{-.15in}% [[ = [[TNat]] : {{t | hasType (Plus (Nat 1) (Nat 2)) t}} - ]] *) + ]] + *) Eval simpl in typeCheck (Plus (Nat 1) (Bool false)). (** %\vspace{-.15in}% [[ = ?? : {{t | hasType (Plus (Nat 1) (Bool false)) t}} - ]] *) + ]] + *) (** The type-checker also extracts to some reasonable OCaml code. *) @@ -856,21 +871,24 @@ = [[[TNat]]] : {t : type | hasType (Nat 0) t} + {(forall t : type, ~ hasType (Nat 0) t)} - ]] *) + ]] + *) Eval simpl in typeCheck' (Plus (Nat 1) (Nat 2)). (** %\vspace{-.15in}% [[ = [[[TNat]]] : {t : type | hasType (Plus (Nat 1) (Nat 2)) t} + {(forall t : type, ~ hasType (Plus (Nat 1) (Nat 2)) t)} - ]] *) + ]] + *) Eval simpl in typeCheck' (Plus (Nat 1) (Bool false)). (** %\vspace{-.15in}% [[ = !! : {t : type | hasType (Plus (Nat 1) (Bool false)) t} + {(forall t : type, ~ hasType (Plus (Nat 1) (Bool false)) t)} - ]] *) + ]] + *) (** * Exercises *)
--- a/src/Universes.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Universes.v Mon Jan 17 15:12:30 2011 -0500 @@ -69,7 +69,8 @@ (** %\vspace{-.15in}% [[ nat : Set - ]] *) + ]] + *) (** printing $ %({}*% #(<a/>*# *) (** printing ^ %*{})% #*<a/>)# *) @@ -79,7 +80,8 @@ Set : Type $ (0)+1 ^ - ]] *) + ]] + *) Check Type. (** %\vspace{-.15in}% [[ @@ -100,13 +102,15 @@ (** %\vspace{-.15in}% [[ forall T : nat, fin T : Set - ]] *) + ]] + *) Check forall T : Set, T. (** %\vspace{-.15in}% [[ forall T : Set, T : Type $ max(0, (0)+1) ^ - ]] *) + ]] + *) Check forall T : Type, T. (** %\vspace{-.15in}% [[ @@ -142,19 +146,22 @@ (** %\vspace{-.15in}% [[ id 0 : nat - ]] *) + ]] + *) Check id Set. (** %\vspace{-.15in}% [[ id Set : Type $ Top.17 ^ - ]] *) + ]] + *) Check id Type. (** %\vspace{-.15in}% [[ id Type $ Top.18 ^ : Type $ Top.19 ^ - ]] *) + ]] + *) (** So far so good. As we apply [id] to different [T] values, the inferred index for [T]'s [Type] occurrence automatically moves higher up the type hierarchy. @@ -197,13 +204,15 @@ (** %\vspace{-.15in}% [[ Const 0 : exp nat - ]] *) + ]] + *) Check Pair (Const 0) (Const tt). (** %\vspace{-.15in}% [[ Pair (Const 0) (Const tt) : exp (nat * unit) - ]] *) + ]] + *) Check Eq (Const Set) (Const Type). (** %\vspace{-.15in}% [[ @@ -306,13 +315,15 @@ (** %\vspace{-.15in}% [[ foo nat : Set - ]] *) + ]] + *) Check foo Set. (** %\vspace{-.15in}% [[ foo Set : Type - ]] *) + ]] + *) Check foo True. (** %\vspace{-.15in}% [[ @@ -347,7 +358,8 @@ (** %\vspace{-.15in}% [[ Inductive sig (A : Type) (P : A -> Prop) : Type := exist : forall x : A, P x -> sig P - ]] *) + ]] + *) Print ex. (** %\vspace{-.15in}% [[ @@ -412,7 +424,7 @@ let sym_ex = __ >> -In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the (Coq-specific) type %\texttt{%#<tt>#__#</tt>#%}%, whose single constructor is %\texttt{%#<tt>#__#</tt>#%}%. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here. +In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the (Coq-specific) type %\texttt{\_\_}%#<tt>__</tt>#, whose single constructor is %\texttt{\_\_}%#<tt>__</tt>#. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here. Extraction is very helpful as an optimization over programs that contain proofs. In languages like Haskell, advanced features make it possible to program with proofs, as a way of convincing the type checker to accept particular definitions. Unfortunately, when proofs are encoded as values in GADTs, these proofs exist at runtime and consume resources. In contrast, with Coq, as long as you keep all of your proofs within [Prop], extraction is guaranteed to erase them. @@ -442,19 +454,22 @@ (** %\vspace{-.15in}% [[ ConstP 0 : expP nat - ]] *) + ]] + *) Check PairP (ConstP 0) (ConstP tt). (** %\vspace{-.15in}% [[ PairP (ConstP 0) (ConstP tt) : expP (nat * unit) - ]] *) + ]] + *) Check EqP (ConstP Set) (ConstP Type). (** %\vspace{-.15in}% [[ EqP (ConstP Set) (ConstP Type) : expP bool - ]] *) + ]] + *) Check ConstP (ConstP O). (** %\vspace{-.15in}% [[ @@ -475,19 +490,22 @@ (** %\vspace{-.15in}% [[ Base 0 : eqPlus 0 0 - ]] *) + ]] + *) Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)). (** %\vspace{-.15in}% [[ Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n) : eqPlus (fun n : nat => n) (fun n : nat => 0 + n) - ]] *) + ]] + *) Check (Base (Base 1)). (** %\vspace{-.15in}% [[ Base (Base 1) : eqPlus (Base 1) (Base 1) - ]] *) + ]] + *) (** * Axioms *) @@ -548,7 +566,8 @@ Print Assumptions t1. (** %\vspace{-.15in}% [[ Closed under the global context -]] *) +]] +*) Theorem t2 : forall P : Prop, ~ ~ P -> P. (** [[ @@ -556,7 +575,8 @@ Error: tauto failed. -]] *) +]] +*) intro P; destruct (classic P); tauto. Qed. @@ -696,7 +716,8 @@ forall P : A -> Prop, (forall x : A, {P x} + {~ P x}) -> (exists! x : A, P x) -> {x : A | P x} - ]] *) + ]] + *) Print Assumptions constructive_definite_description. (** %\vspace{-.15in}% [[ @@ -764,7 +785,8 @@ (** [[ = 13 : nat - ]] *) + ]] + *) (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *) @@ -817,4 +839,5 @@ (** %\vspace{-.15in}% [[ = First : fin (13 + 1) - ]] *) + ]] + *)