The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

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.