Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 465:4320c1a967c2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spell check
author Adam Chlipala <adam@chlipala.net>
date Wed, 29 Aug 2012 18:26:26 -0400
parents e3fa35c750ac
children b36876d4611e
comparison
equal deleted inserted replaced
464:e53d051681b0 465:4320c1a967c2
242 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) -> 242 (forall (y : A) (p : R y x), f y p = g y p) -> F x f = F x g) ->
243 forall x : A, 243 forall x : A,
244 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y) 244 Fix Rwf P F x = F x (fun (y : A) (_ : R y x) => Fix Rwf P F y)
245 ]] 245 ]]
246 246
247 Most such obligations are dischargable with straightforward proof automation, and this example is no exception. *) 247 Most such obligations are dischargeable with straightforward proof automation, and this example is no exception. *)
248 248
249 match goal with 249 match goal with
250 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E 250 | [ |- context[match ?E with left _ => _ | right _ => _ end] ] => destruct E
251 end; simpl; f_equal; auto. 251 end; simpl; f_equal; auto.
252 Qed. 252 Qed.
746 repeat (apply eval_frob; simpl; constructor). 746 repeat (apply eval_frob; simpl; constructor).
747 Qed. 747 Qed.
748 748
749 (** We need to apply constructors of [eval] explicitly, but the process is easy to automate completely for concrete input programs. 749 (** We need to apply constructors of [eval] explicitly, but the process is easy to automate completely for concrete input programs.
750 750
751 Now consider another very similar definition, this time of a Fibonacci number funtion. *) 751 Now consider another very similar definition, this time of a Fibonacci number function. *)
752 752
753 Notation "x <- m1 ; m2" := 753 Notation "x <- m1 ; m2" :=
754 (TBind m1 (fun x => m2)) (right associativity, at level 70). 754 (TBind m1 (fun x => m2)) (right associativity, at level 70).
755 755
756 (* begin hide *) 756 (* begin hide *)
910 910
911 Another useful property is that a function and its termination argument may be developed separately. We may even want to define functions that fail to terminate on some or all inputs. The well-founded recursion technique does not have this property, but the other three do. 911 Another useful property is that a function and its termination argument may be developed separately. We may even want to define functions that fail to terminate on some or all inputs. The well-founded recursion technique does not have this property, but the other three do.
912 912
913 One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators. This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader. 913 One minor plus is the ability to write recursive definitions in natural syntax, rather than with calls to higher-order combinators. This downside of the first two techniques is actually rather easy to get around using Coq's notation mechanism, though we leave the details as an exercise for the reader.
914 914
915 The first two techniques impose proof obligations that are more basic than terminaton arguments, where well-founded recursion requires a proof of extensionality and domain-theoretic recursion requires a proof of continuity. A function may not be defined, and thus may not be computed with, until these obligations are proved. The co-inductive techniques avoid this problem, as recursive definitions may be made without any proof obligations. 915 The first two techniques impose proof obligations that are more basic than termination arguments, where well-founded recursion requires a proof of extensionality and domain-theoretic recursion requires a proof of continuity. A function may not be defined, and thus may not be computed with, until these obligations are proved. The co-inductive techniques avoid this problem, as recursive definitions may be made without any proof obligations.
916 916
917 We can also consider support for common idioms in functional programming. For instance, the [thunk] monad effectively only supports recursion that is tail recursion, while the others allow arbitrary recursion schemes. 917 We can also consider support for common idioms in functional programming. For instance, the [thunk] monad effectively only supports recursion that is tail recursion, while the others allow arbitrary recursion schemes.
918 918
919 On the other hand, the [comp] monad does not support the effective mixing of higher-order functions and general recursion, while all the other techniques do. For instance, we can finish the failed [curriedAdd] example in the domain-theoretic monad. *) 919 On the other hand, the [comp] monad does not support the effective mixing of higher-order functions and general recursion, while all the other techniques do. For instance, we can finish the failed [curriedAdd] example in the domain-theoretic monad. *)
920 920