The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi, Nuno.  You need to use a Fixpoint.  Your function is decreasing lexicographically.

Here is the easiest way to do it:

Inductive a : Type :=

  | A : nat -> list a -> a.

Fixpoint beq_a (x y:a) : bool := 

  match x, y with

    | A n lz, A n' lz' => 

      let aux := (fix beq_list_a (l l': list a) :=

        match l, l' with

          | nil, nil         => true

          | e :: r, e' :: r' => andb (beq_a e e') (beq_list_a r r')

          | _, _             => false

        end) in andb (beq_nat n n') (aux lz lz')

  end.

I hope this helps.

Harley

On Tue, Mar 20, 2012 at 5:53 AM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

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.