coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Claude Marche <Claude.Marche AT lri.fr>
- To: mulhern <mulhern AT gmail.com>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Fwd: Question about Fixpoint
- Date: Fri, 4 Feb 2005 10:28:56 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
>>>>> "mulhern" == mulhern
>>>>>Â <mulhern AT gmail.com>
>>>>> writes:
mulhern> Hi!
mulhern> Thanks for your response, but it doesn't appear to solve the
problem.
mulhern> I have taken your example and changed it so that the local
methods is
mulhern> no longer local and it is still considered well-formed by Coq.
Here's
mulhern> the text.
You're right, my example is too simple. Here is a better one :
Require Import List.
Inductive tree : Set := Empty : tree | Node : nat -> list tree -> tree.
then
Fixpoint sumtree (t:tree) : nat:=
match t with
| Empty => 0
| Node n f => n + sumforest f
end
with sumforest (f:list tree) : nat :=
match f with
nil => 0
|cons t f' => sumtree t + sumforest f'
end.
does not work whereas
Fixpoint sumtree (t:tree) : nat:=
let sumforest := fix sumforest (f:list tree) : nat :=
match f with
nil => 0
|cons t f' => sumtree t + sumforest f'
end
in
match t with
| Empty => 0
| Node n f => n + sumforest f
end.
works.
mulhern> I've tried to construct the smallest possible example that I
believe
mulhern> captures the problem, and here it is.
mulhern> Require Import List.
mulhern> Definition R (p p': List.list nat * nat) := length (fst p) <
length (fst p').
mulhern> Fixpoint sum (p : List.list nat * nat) : nat := match p with
mulhern> (List.nil, O) => O
mulhern> | (List.nil, S x) => S (sum (List.nil, x))
mulhern> | (List.cons y ll, O) => S(sum(ll, O))
mulhern> | (List.cons y ll, S x) => S (sum (ll,x))
mulhern> end.
mulhern> My question is, why does the fourth match yield an error when the
mulhern> third match doesn't? It is clear by inspection that this
function must
mulhern> terminate.
This has nothing to do with previous example. And you misinterpret
Coq answer: no, both the second, third and fourth cases are ill-formed
(see note)
as you may see with
Fixpoint sum (p : List.list nat * nat) : nat := match p with
(List.nil, O) => O
| (List.nil, S x) => S (sum (List.nil, x))
| (List.cons y ll, O) => S(sum(ll, O))
| (List.cons y ll, S x) => O
end.
And Coq is right, none of those cases are recursive call on a subterm.
note : why do you think typechecking should go topdown ? indeed, this
is an extended matching which is internally transform into nested matches,
hence in an unspecified order see Chapter 15 of reference manual
--
| Claude Marché |
mailto:Claude.Marche AT lri.fr
|
| LRI - Bât. 490 | http://www.lri.fr/~marche/ |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85 |
| F-91405 ORSAY Cedex | faxto: +33 1 69 15 65 86 |
- [Coq-Club] Fwd: Question about Fixpoint, mulhern
- Re: [Coq-Club] Fwd: Question about Fixpoint,
Pierre Casteran
- Re: [Coq-Club] Fwd: Question about Fixpoint,
roconnor
- Re: [Coq-Club] Fwd: Question about Fixpoint, Pierre Casteran
- Re: [Coq-Club] Fwd: Question about Fixpoint,
roconnor
- Re: [Coq-Club] Fwd: Question about Fixpoint,
Claude Marche
- Message not available
- Re: [Coq-Club] Fwd: Question about Fixpoint, Claude Marche
- Message not available
- Re: [Coq-Club] Fwd: Question about Fixpoint,
Pierre Casteran
Archive powered by MhonArc 2.6.16.