The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 20 Mar 2012 11:53:16 +0100,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 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? :-)
> 
> 
2 other solutions than the ones provided by those who replied your mail:

- The first one is essentially the one they refered to, with a clean
  separation of the two parts
  (which allows "Definition beq_list_a2 := beq_list_a beq_a.")
- The other is a redefinition of the type a, so that "b" and "list_b"
  are really mutually recursive.

The pros and cons:

First solution allows you to directly use the "List" module.

Second solution makes it easier to perform induction.
In particular, if you want to do some proofs with your type, you may
require to define your own induction principle, whereas you don't have
to do it in the 2nd solution.

(*************************************)

Require Import List.
Require Import Bool.

Fixpoint beq_nat (m n : nat) :=
  match m, n with
    | O, O     => true
    | S m, S n => beq_nat m n
    | _, _     => false
  end.

(**************************************)

Inductive a : Type :=
  | A : nat -> list a -> a.

Definition beq_list_a (beq_a : a -> a -> bool) : list a -> list a ->
bool := fix 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.

Fixpoint beq_a (x y:a) {struct x} : bool :=
 match x, y with
   | A n lz, A n' lz' => (beq_nat n n') &&  (beq_list_a beq_a lz lz')
 end.

(****************************************)
(* The type has been renamed to avoid conflicts with the previous one*)
Inductive b : Type :=
  | B : nat -> list_b -> b
with list_b : Type :=
  | Nil_b : list_b
  | Cons_b : b -> list_b -> list_b.

(* Don't bother with Notations if you don't like them… *)
Notation "'ε'" := (Nil_b).
Notation "p ∷ q" := (Cons_b p q) (at level 60, right associativity).

Fixpoint beq_b (x y:b) {struct x} : bool :=
 match x, y with
   | B n lz, B n' lz' => (beq_nat n n') &&  (beq_list_b lz lz')
 end
with beq_list_b (l l': list_b) {struct l}: bool :=
  match l, l' with
    | ε, ε           => true
    | e ∷ r, e' ∷ r' => (beq_b e e') && (beq_list_b r r')
    | _, _           => false
  end.