The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,

In short, bad luck for you, you are the 134368th to face the situation  
where mutual fixpoints and inner fixpoints are not equivalent !

write

Fixpoint beq_a (x y:a) : bool :=
 match x, y with
   | A n lz, A n' lz' => (beq_nat n n') &&
((fix beq_list_a (l l': list a): bool :=
  match l, l' with
  | nil, nil         => true
  | cons e r, cons e' r' => (beq_a e e') && (beq_list_a r r')
  | _, _             => false
  end) lz lz')
 end.

and it's accepted.
Sorry for that

All the best.
Pierre

Le 20 mars 12 à 11:53, Nuno Gaspar a écrit :

> Hello.
>
> I want to define a boolean comparison function over the following  
> inductive definition.
>
> Inductive a : Type :=
>   | A : nat -> list a -> a.
>
> It's simple, two elements of type _a_ are equal if their projections  
> are. Now, it seemed to me that the following mutually recursive  
> function would do that...
>
> Function beq_a (x y:a) { ? } : bool :=
>  match x, y with
>    | A n lz, A n' lz' => (beq_nat n n') && (beq_list_a lz lz')
>  end
> with beq_list_a (l l': list a) {struct l}: bool :=
>   match l, l' with
>   | nil, nil         => true
>   | e :: r, e' :: r' => (beq_a e e') && (beq_list_a r r')
>   | _, _             => false
>   end.
>
> Coq requires the decreasing argument to be specified. However, in  
> this mutually recursive definition I do not know how to specify it  
> for [beq_a]. I guess this issue arises due to the fact that the  
> functions pattern-match on different types ..
>
> So, how can I convince Coq? :-)
>
>
> --
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made  
> $600 dollars last year.
> Marge: Bart! Don't make fun of grad students, they just made a  
> terrible life choice.