coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Function problem when executing Defined
- Date: Mon, 18 Jul 2016 08:32:48 +0200
Dear Sorin,
In my opinion, the bug is that this is reported as an anomaly. I participated in the design of the Function command a while ago, and at the time, it was clear that nested recursion could not be handled, given the technology that was employed. You code is designed in a way that it looks like nested recursion.
the expression 'match f tr with ...' appears in one of the branches of the expression 'match f tl'. In reality you don't use nested recursion, because the pattern on 'f tl' in this case is not used (it is an anonymous pattern '_'), but this is too hard to guess for our crude code analyzer.
Your code could be rewritten to make it obvious that the recursive call are direct calls to sub-terms that are already visible even without the first call. One problem with this is that the code you obtain is functionally equivalent, but risks having a different complexity behavior when the executed with an 'Ocaml-like' evaluation strategy. For proof purposes, functional equivalence is enough. To fix the complexity behavior, it depends on the technology you use to obtain the final executable code. For instance, if you use extraction, I believe you should be able to request that the "combine_results" function be inlined.
Here is my replacement for your code.
On 07/17/2016 01:38 PM, sorin stratulat wrote:
Dear Coq-club,
I have encountered a problem when defining a recursive function on binary trees. A simplified version of the problem is given below:
-----------
Require Import Recdef.
Require Import Program.
Require Import List.
Inductive Btree : Set :=
| Epsilon : Btree
| Node : Btree -> nat -> Btree -> Btree.
Fixpoint nr_nodes (t: Btree) : nat :=
match t with
| Epsilon => 0
| Node tl n tr => S ((nr_nodes tl) + (nr_nodes tr))
end.
Require Import Omega.
Function f (t: Btree){wf (fun t1 t2: Btree => (nr_nodes t1) < ( nr_nodes t2)) t}: Btree :=
match t with
| Epsilon => Epsilon
| Node tl _ tr =>
match f tl with
| Epsilon => Epsilon
| _ =>
match f tr with
| Epsilon => Epsilon
| _ => Epsilon
end
end
end.
Proof.
intros. simpl. omega.
intros. simpl. omega.
apply (well_founded_lt_compat Btree nr_nodes).
intros. trivial.
Defined.
--------
When Defined is executed (the last line), Coq yields "Anomaly: Cannot create equation Lemma. Please report.". This is exactly what I am doing, i.e. reporting this problem.
Is there any way to avoid this problem or should I wait for the next release (I am using 8.5pl2 new version) ?
Thanks for any help,
Sorin
- [Coq-Club] Function problem when executing Defined, sorin stratulat, 07/17/2016
- Re: [Coq-Club] Function problem when executing Defined, Yves Bertot, 07/18/2016
- Re: [Coq-Club] Function problem when executing Defined, Yves Bertot, 07/18/2016
- Re: [Coq-Club] Function problem when executing Defined, sorin stratulat, 07/18/2016
- Re: [Coq-Club] Function problem when executing Defined, Yves Bertot, 07/18/2016
- Re: [Coq-Club] Function problem when executing Defined, Yves Bertot, 07/18/2016
Archive powered by MHonArc 2.6.18.