### changeset 282:caa69851c78d

Subset suggestions from PC; improvements to build process for coqdoc fontification
author Adam Chlipala Fri, 05 Nov 2010 10:35:56 -0400 4146889930c5 756ce68e42fb Makefile src/Intro.v src/Subset.v 3 files changed, 119 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/Makefile	Fri Oct 15 09:50:34 2010 -0400
+++ b/Makefile	Fri Nov 05 10:35:56 2010 -0400
@@ -37,9 +37,9 @@
-o ../latex/cpdt.tex

latex/%.tex: src/%.v
-	coqdoc --interpolate --latex -s \
+	cd src ; coqdoc --interpolate --latex -s \
-p "\usepackage{url,amsmath,amssymb}" \
-		$< -o$@
+		$*.v -o ../latex/$*.tex

latex/%.dvi: latex/%.tex
cd latex ; latex $* ; latex$*
--- a/src/Intro.v	Fri Oct 15 09:50:34 2010 -0400
+++ b/src/Intro.v	Fri Nov 05 10:35:56 2010 -0400
@@ -21,7 +21,7 @@

(**

Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
--- a/src/Subset.v	Fri Oct 15 09:50:34 2010 -0400
+++ b/src/Subset.v	Fri Nov 05 10:35:56 2010 -0400
@@ -1,4 +1,4 @@
*
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -71,7 +71,20 @@

(** We expand the type of [pred] to include a %\textit{%#<i>#proof#</i>#%}% that its argument [n] is greater than 0.  When [n] is 0, we use the proof to derive a contradiction, which we can use to build a value of any type via a vacuous pattern match.  When [n] is a successor, we have no need for the proof and just return the answer.  The proof argument can be said to have a %\textit{%#<i>#dependent#</i>#%}% type, because its type depends on the %\textit{%#<i>#value#</i>#%}% of the argument [n].

-One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
+   Coq's [Eval] command can execute particular invocations of [pred_strong1] just as easily as it can execute more traditional functional programs.  Note that Coq has decided that argument [n] of [pred_strong1] can be made %\textit{%#<i>#implicit#</i>#%}%, since it can be deduced from the type of the second argument, so we need not write [n] in function calls. *)
+
+Theorem two_gt0 : 2 > 0.
+  crush.
+Qed.
+
+Eval compute in pred_strong1 two_gt0.
+(** %\vspace{-.15in}% [[
+     = 1
+     : nat
+
+ ]]
+
+ One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.

[[
Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
@@ -145,6 +158,15 @@
| exist (S n') _ => n'
end.

+(** To build a value of a subset type, we use the [exist] constructor, and the details of how to do that follow from the output of our earlier [Print sig] command. *)
+
+Eval compute in pred_strong2 (exist _ 2 two_gt0).
+(** %\vspace{-.15in}% [[
+     = 1
+     : nat
+
+     ]] *)
+
Extraction pred_strong2.

(** %\begin{verbatim}
@@ -173,7 +195,14 @@
| exist (S n') pf => exist _ n' (refl_equal _)
end.

-(** The function [proj1_sig] extracts the base value from a subset type.  Besides the use of that function, the only other new thing is the use of the [exist] constructor to build a new [sig] value, and the details of how to do that follow from the output of our earlier [Print] command.  It also 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.
+Eval compute in pred_strong3 (exist _ 2 two_gt0).
+(** %\vspace{-.15in}% [[
+     = 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.

By now, the reader is probably ready to believe that the new [pred_strong] leads to the same OCaml code as we have seen several times so far, and Coq does not disappoint. *)

@@ -253,9 +282,16 @@

]]

-We see the code we entered, with some proofs filled in.  The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand.  The second proof obligation is a simple reflexivity proof.
+We see the code we entered, with some proofs filled in.  The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand.  The second proof obligation is a simple reflexivity proof. *)

-We are almost done with the ideal implementation of dependent predecessor.  We can use Coq's syntax extension facility to arrive at code with almost no complexity beyond a Haskell or ML program with a complete specification in a comment. *)
+Eval compute in pred_strong4 two_gt0.
+(** %\vspace{-.15in}% [[
+     = exist (fun m : nat => 2 = S m) 1 (refl_equal 2)
+     : {m : nat | 2 = S m}
+
+     ]]
+
+     We are almost done with the ideal implementation of dependent predecessor.  We can use Coq's syntax extension facility to arrive at code with almost no complexity beyond a Haskell or ML program with a complete specification in a comment. *)

Notation "!" := (False_rec _ _).
Notation "[ e ]" := (exist _ e _).
@@ -268,7 +304,16 @@
end); crush.
Defined.

-(** One other alternative is worth demonstrating.  Recent Coq versions include a facility called [Program] that streamlines this style of definition.  Here is a complete implementation using [Program]. *)
+(** By default, notations are also used in pretty-printing terms, including results of evaluation. *)
+
+Eval compute in pred_strong5 two_gt0.
+(** %\vspace{-.15in}% [[
+     = [1]
+     : {m : nat | 2 = S m}
+
+     ]]
+
+  One other alternative is worth demonstrating.  Recent Coq versions include a facility called [Program] that streamlines this style of definition.  Here is a complete implementation using [Program]. *)

Obligation Tactic := crush.

@@ -280,6 +325,13 @@

(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives you more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem-proving. *)

+Eval compute in pred_strong6 two_gt0.
+(** %\vspace{-.15in}% [[
+     = [1]
+     : {m : nat | 2 = S m}
+
+     ]] *)
+

(** * Decidable Proposition Types *)

@@ -313,6 +365,20 @@
end); congruence.
Defined.

+Eval compute in eq_nat_dec 2 2.
+(** %\vspace{-.15in}% [[
+     = 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. *)

Extraction eq_nat_dec.
@@ -401,9 +467,23 @@
| nil => No
| x' :: ls' => A_eq_dec x x' || f x ls'
end); crush.
-  Qed.
+  Defined.
End In_dec.

+Eval compute in In_dec eq_nat_dec 2 (1 :: 2 :: nil).
+(** %\vspace{-.15in}% [[
+     = 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. *)

Extraction In_dec.
@@ -456,7 +536,21 @@
end); trivial.
Defined.

-(** Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case.  We can strengthen the type to rule out such vacuous implementations, and the type family [sumor] from the standard library provides the easiest starting point.  For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *)
+Eval compute in pred_strong7 2.
+(** %\vspace{-.15in}% [[
+     = [[1]]
+     : {{m | 2 = S m}}
+
+     ]] *)
+
+Eval compute in pred_strong7 0.
+(** %\vspace{-.15in}% [[
+     = ??
+     : {{m | 0 = S m}}
+
+     ]]
+
+     Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case.  We can strengthen the type to rule out such vacuous implementations, and the type family [sumor] from the standard library provides the easiest starting point.  For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *)

Print sumor.
(** %\vspace{-.15in}% [[
@@ -481,6 +575,20 @@
end); trivial.
Defined.

+Eval compute in pred_strong8 2.
+(** %\vspace{-.15in}% [[
+     = [[[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 *)