coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
- To: Randy Pollack <rpollack AT inf.ed.ac.uk>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Inductive definitions that go through lists
- Date: Tue, 05 Feb 2008 17:26:38 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Coq's inferred recursion principle for X is not the "reference". The mechanism at work inside
the verification of guards for recursive definition is the reference. The inferred recursion principle
that is given by Coq for an arbitrary inductive definition is a helper, but it does not capture the
whole expressive power.
This is why you can devise your own recursion principles that may turn out to be more powerful
than the ones provided by default by Coq.
Fixpoint map1 (A B:Type)(f:A->B) (l:list A) : list B :=
match l with nil => nil | a::tl => f a::map1 A B f tl end.
You don't get the same value as if you write
Section map_def.
Variables (A B:Type)(f:A->B).
Fixpoint map2 (l:list A) : list B :=
match l with nil => nil | a::tl => f a::map2 tl end.
End map_def.
The function map contains recursive calls where f occurs without being applied
to an argument, while map' contains no such recursive call. For this reason,
a recursive function on your type X based on map2 will pass the guard checking test,
while a recursive function on the same type based on map1 will not.
One more explanation: when performing guard-checking, the Coq system will unfold
functions as necessary to expose recursive calls and check that they are always applied,
and that they are always applied to structural sub-terms,
where structural sub-terms are defined through a recursive process:
- a variable obtained by pattern-matching from a structural sub-term is a structural sub-term,
- a variable obtained by pattern-matching from the initial structural argument is a structural sub-term,
- the structural variable of a fix expression, when this fix expression is applied to a structural sub-term,
is a structural subterm,
- a pattern-matching construct where all branches are structural subterm is a structural sub-term,
My explanation here may be slightly flawed, but I hope you get an idea. Note that your use of map
falls in 3rd point above, while well-founded recursion works mainly because of the 4th point.
In principle, this allows for "match (t:False) with end" to be accepted as a structural sub-term in any
function. I use this a lot.
I hope this helps,
Yves
- Re: [Coq-Club] Inductive definitions that go through lists, Randy Pollack
- Re: [Coq-Club] Inductive definitions that go through lists, Yves Bertot
Archive powered by MhonArc 2.6.16.