coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Problem defining a function using lexicographic combinations and then wf-annotation
chronological Thread
- From: Arthur Chargu�raud <arthur AT chargueraud.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Problem defining a function using lexicographic combinations and then wf-annotation
- Date: Fri, 16 Mar 2012 10:07:04 +0100
Hi Harley, If you are happy to use non-constructive definitions, you may use the "Optimal Fixed Point Combinator" for your definitions. For the ackermann function, you can construct the fix point and then prove a fixed point equation that allows unfolding the body of the function when needed. My Coq script is as follows. Definition Ack ack m n := If m = 0 then n+1 else If n = 0 then ack (m-1) 1 else ack (m-1) (ack m (n-1)). Definition ack := FixFun2 Ack. Ltac emaths := eauto with maths. Lemma fix_ack : forall m n, ack m n = Ack ack m n. Proof. applys~ (FixFun2_fix (lexico2 (@lt nat _) (@lt nat _))). introv IH. unfolds. case_if~. case_if~. apply IH. emaths. rewrite IH. fequals~. emaths. emaths. Qed.You can find more details from: http://arthur.chargueraud.org/projects/fix/ Arthur PS: If you need to remain constructive, you will probably need to use "Program Fixpoint" and give you definition a dependent type that captures enough of the specification of the function for you to be able to justify termination. I am not aware of any recursive functions for which the dependent-type approach is impossible to use. Hello. |
- [Coq-Club] Problem defining a function using lexicographic combinations and then wf-annotation, Harley D. Eades III
- Re: [Coq-Club] Problem defining a function using lexicographic combinations and then wf-annotation, Arthur Charguéraud
- Re: [Coq-Club] Problem defining a function using lexicographic combinations and then wf-annotation, AUGER Cédric
Archive powered by MhonArc 2.6.16.