The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

>>>>> "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    |