The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

You are basically trying to use an higher-order function (makeAll)
applied to a  function nat_tree_ind''  inside the recursive definition
of nat_tree_ind'' itself. Unfortunately, there is no way to ensure
that the function defined in this fashion is going to terminate...
Consider the following snippet, which boils down to the same
situation.

Section t.
   Variable bad_apply : (list nat -> bool) -> nat -> list nat -> bool.
   Fixpoint bad_fixpoint (l : list nat) : bool :=
   match l with
     | nil => false
     | cons t q => bad_apply bad_fixpoint t q
   end. (*fails *)
End t.

Definition bad_apply (f : list nat -> bool) (t : nat) (q : list nat)
:= f (cons t q).
Definition absurd := bad_fixpoint bad_apply.

If the definition of bad_fixpoint was accepted, I would have built a
non-terminating function inside coq...

From an higher-level point of view, this is why one is so often
compelled into using nested recursion, in this kind of cases, and I
agree that this is painful... (Not to mention the subtle differences
between nested recursion and mutually recursive definitions).

With best regards,
Thomas

PS: note that in the above snippet, the use of the section variable is
required to make the definition of bad_apply opaque inside the
definition of bad_fixpoint.




On Wed, Apr 18, 2012 at 12:39 AM,  
<apk32 AT cam.ac.uk>
 wrote:
>
> Require Import List.
> Set Implicit Arguments.
>
> Inductive nat_tree : Set :=
> | NLeaf : nat_tree
> | NNode : nat -> list nat_tree -> nat_tree.
>
> Section All.
>  Variable T : Set.
>  Variable P : T -> Prop.
>
>  Fixpoint All (ls : list T) : Prop :=
>    match ls with
>      | nil => True
>      | cons h t => P h /\ All t
>    end.
>
>  Lemma makeAll (f : forall t:T, P t) (ls : list T) : All ls.
>  Proof.
>    induction ls; simpl; auto.
>  Qed.
> End All.
>
> Section nat_tree_ind'.
>  Variable P : nat_tree -> Prop.
>
>  Hypothesis NLeaf_case : P NLeaf.
>  Hypothesis NNode_case : forall (n : nat) (ls : list nat_tree),
>    All P ls -> P (NNode n ls).
>
>  Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
>    match tr with
>      | NLeaf => NLeaf_case
>      | NNode n ls => NNode_case n ls
>        ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
>          match ls  with
>            | nil => I
>            | cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind 
> rest)
>          end) ls)
>    end.
>
>  Fixpoint nat_tree_ind'' (tr : nat_tree) : P tr :=
>    match tr with
>      | NLeaf => NLeaf_case
>      | NNode n ls => NNode_case n ls (makeAll P nat_tree_ind'' ls)
>    end.
>
> End nat_tree_ind'.