Certified Programming with Dependent Types: src/GeneralRec.v comparison

comparison src/GeneralRec.v @ 357:b01c7b3122cc

New release

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 28 Oct 2011 18:26:16 -0400
parents	50e1d338728c
children	d1276004eec9

comparison

equal deleted inserted replaced

-:50e1d338728c
+:b01c7b3122cc
 (** %\vspace{-.15in}% [[
 Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
 Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
 ]]
-In prose, an element [x] is accessible for a relation [R] if every element %``%#"#less than#"#%''% [x] according to [R] is also accessible.  Since [Acc] is defined inductively, we know that any accessibility proof involves a finite chain of invocations, in a certain sense which we can make formal.  Building on Chapter 5's examples, let us define a co-inductive relation that is closer to the usual informal notion of %``%#"#absence of infinite decreasing chains.#"#%''% *)
+In prose, an element [x] is accessible for a relation [R] if every element %``%#"#less than#"#%''% [x] according to [R] is also accessible.  Since [Acc] is defined inductively, we know that any accessibility proof involves a finite chain of invocations, in a certain sense that we can make formal.  Building on Chapter 5's examples, let us define a co-inductive relation that is closer to the usual informal notion of %``%#"#absence of infinite decreasing chains.#"#%''% *)
 CoInductive isChain A (R : A -> A -> Prop) : stream A -> Prop :=
 | ChainCons : forall x y s, isChain R (Cons y s)
 -> R y x
 -> isChain R (Cons x (Cons y s)).
 (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
 forall x : A, P x
 ]]
 A call to %\index{Gallina terms!Fix}%[Fix] must present a relation [R] and a proof of its well-foundedness.  The next argument, [P], is the possibly dependent range type of the function we build; the domain [A] of [R] is the function's domain.  The following argument has this type:
 [[
 forall x : A, (forall y : A, R y x -> P y) -> P x
 ]]
 This is an encoding of the function body.  The input [x] stands for the function argument, and the next input stands for the function we are defining.  Recursive calls are encoded as calls to the second argument, whose type tells us it expects a value [y] and a proof that [y] is %``%#"#less than#"#%''% [x], according to [R].  In this way, we enforce the well-foundedness restriction on recursive calls.
 Some more recent Coq features provide more convenient syntax for defining recursive functions.  Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *)
 (** * A Non-Termination Monad Inspired by Domain Theory *)
-(** The key insights of %\index{domain theory}%domain theory%~\cite{WinskelDomains}% inspire the next approach to modeling non-termination.  Domain theory is based on %\emph{%#<i>#information orders#</i>#%}% that relate values representing computatiion results, according to how much information these values convey.  For instance, a simple domain might include values %``%#"#the program does not terminate#"#%''% and %``%#"#the program terminates with the answer 5.#"#%''%  The former is considered to be an %\emph{%#<i>#approximation#</i>#%}% of the latter, while the latter is %\emph{%#<i>#not#</i>#%}% an approximation of %``%#"#the program terminates with the answer 6.#"#%''%  The details of domain theory will not be important in what follows; we merely borrow the notion of an approximation ordering on computation results.
+(** The key insights of %\index{domain theory}%domain theory%~\cite{WinskelDomains}% inspire the next approach to modeling non-termination.  Domain theory is based on %\emph{%#<i>#information orders#</i>#%}% that relate values representing computation results, according to how much information these values convey.  For instance, a simple domain might include values %``%#"#the program does not terminate#"#%''% and %``%#"#the program terminates with the answer 5.#"#%''%  The former is considered to be an %\emph{%#<i>#approximation#</i>#%}% of the latter, while the latter is %\emph{%#<i>#not#</i>#%}% an approximation of %``%#"#the program terminates with the answer 6.#"#%''%  The details of domain theory will not be important in what follows; we merely borrow the notion of an approximation ordering on computation results.
 Consider this definition of a type of computations. *)
 Section computation.
 Variable A : Type.
 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
 end.
 (* end hide *)
 (** remove printing exists *)
-(** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop.  For any approximation level, it fails to terminate (returns [None]).  Note the use of [abstract] to create a new opaque lemma for the proof found by the [run] tactic.  In contrast to the previous section, opauqe proofs are fine here, since the proof components of computations do not influence evaluation behavior. *)
+(** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop.  For any approximation level, it fails to terminate (returns [None]).  Note the use of [abstract] to create a new opaque lemma for the proof found by the [run] tactic.  In contrast to the previous section, opaque proofs are fine here, since the proof components of computations do not influence evaluation behavior. *)
 Section Bottom.
 Variable A : Type.
 Definition Bottom : computation A.
 Variable m1 : computation A.
 Variable m2 : A -> computation B.
 Definition Bind : computation B.
 exists (fun n =>
-let (f1, Hf1) := m1 in
+let (f1, _) := m1 in
 match f1 n with
 	| None => None
 	| Some v =>
-	  let (f2, Hf2) := m2 v in
+	  let (f2, _) := m2 v in
 	    f2 n
 end); abstract run.
 Defined.
 Theorem run_Bind : forall (v1 : A) (v2 : B),
 Theorem right_identity : forall A (m : computation A),
 meq (Bind m (@Return _)) m.
 run.
 Qed.
-Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C),
+Theorem associativity : forall A B C (m : computation A)
+(f : A -> computation B) (g : B -> computation C),
 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
 run.
 Qed.
 (** Now we come to the piece most directly inspired by domain theory.  We want to support general recursive function definitions, but domain theory tells us that not all definitions are reasonable; some fail to be %\emph{%#<i>#continuous#</i>#%}% and thus represent unrealizable computations.  To formalize an analogous notion of continuity for our non-termination monad, we write down the approximation relation on computation results that we have had in mind all along. *)
 repeat (apply eval_frob; simpl; constructor).
 Qed.
 (** We need to apply constructors of [eval] explicitly, but the process is easy to automate completely for concrete input programs.
-Now consider another very similar definition, this time of a Fibonacci number funtion.
+Now consider another very similar definition, this time of a Fibonacci number funtion. *)
-[[
+Notation "x <- m1 ; m2" :=
+(TBind m1 (fun x => m2)) (right associativity, at level 70).
+(** %\vspace{-.15in}%[[
 CoFixpoint fib (n : nat) : thunk nat :=
 match n with
 | 0 => Answer 1
 | 1 => Answer 1
-| _ => TBind (fib (pred n)) (fun n1 =>
+| _ => n1 <- fib (pred n);
-TBind (fib (pred (pred n))) (fun n2 =>
+n2 <- fib (pred (pred n));
-Answer (n1 + n2)))
+Answer (n1 + n2)
 end.
 ]]
 Coq complains that the guardedness condition is violated.  The two recursive calls are immediate arguments to [TBind], but [TBind] is not a constructor of [thunk].  Rather, it is a defined function.  This example shows a very serious limitation of [thunk] for traditional functional programming: it is not, in general, possible to make recursive calls and then make further recursive calls, depending on the first call's result.  The [fact] example succeeded because it was already tail recursive, meaning no further computation is needed after a recursive call.
 >>
 The problem has to do with rules for inductive definitions that we still study in more detail in Chapter 12.  Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B].  To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat].  However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined.  Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *)
-(** * Comparing the Options *)
+(** * Comparing the Alternatives *)
 (** We have seen four different approaches to encoding general recursive definitions in Coq.  Among them there is no clear champion that dominates the others in every important way.  Instead, we close the chapter by comparing the techniques along a number of dimensions.  Every technique allows recursive definitions with terminaton arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences.
 One useful property is automatic integration with normal Coq programming.  That is, we would like the type of a function to be the same, whether or not that function is defined using an interesting recursion pattern.  Only the first of the four techniques, well-founded recursion, meets this criterion.  It is also the only one of the four to meet the related criterion that evaluation of function calls can take place entirely inside Coq's built-in computation machinery.  The monad inspired by domain theory occupies some middle ground in this dimension, since generally standard computation is enough to evaluate a term once a high enough approximation level is provided.
 Definition curriedAdd' (n : nat) := Return (fun m : nat => Return (n + m)).
 Definition testCurriedAdd := Bind (curriedAdd' 2) (fun f => f 3).
-(** The same techniques also apply to more interesting higher-order functions like list map, and, as in all four techniques, we can mix regular and general recursion, preferring the former when possible to avoid proof obligations. *)
+(** The same techniques also apply to more interesting higher-order functions like list map, and, as in all four techniques, we can mix primitive and general recursion, preferring the former when possible to avoid proof obligations. *)
 Fixpoint map A B (f : A -> computation B) (ls : list A) : computation (list B) :=
 match ls with
 | nil => Return nil
 | x :: ls' => Bind (f x) (fun x' =>
 exists 1; reflexivity.
 Qed.
 (** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an %\emph{axiom}%, a logical complication that we discuss at more length in Chapter 12.  The other three techniques allow proof of all the important theorems within the normal logic of Coq.
-Perhaps one theme of our comparison is that one must trade off between on one hand, functional programming expressiveness and compatibility with normal Coq types and computation; and, on the other hand, the level of proof obligations one is willing to handle at function definition time. *)
+Perhaps one theme of our comparison is that one must trade off between, on one hand, functional programming expressiveness and compatibility with normal Coq types and computation; and, on the other hand, the level of proof obligations one is willing to handle at function definition time. *)

Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 357:b01c7b3122cc