The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Klaus,

This is becoming a classic. What you need is a good induction principle
for trees of arbitrary arity. This is one way to do it.

Dominique

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

Require Import Arith.
Require Import List.

Inductive id : Set := in_id : nat -> id.

Unset Elimination Schemes.

Inductive ty : Set :=
  | tvar : id -> ty
  | tpoly : id -> list ty -> ty.

Set Elimination Schemes.

Fixpoint occ {X} (x : X) l : Type :=
  match l with
    | nil  => False
    | y::l => ((x = y) + occ x l)%type
  end.

Section ty_rect.

  Variable P : ty -> Type.

  Hypothesis HP1 : forall i, P (tvar i).
  Hypothesis HP2 : forall i l, (forall t, occ t l -> P t) -> P (tpoly i l).

  Fixpoint ty_rect t : P t.
  Proof.
    refine (match t with
              | tvar i    => HP1 i
              | tpoly i l => HP2 _ _ _
            end).
    clear t.
    induction l as [ | x l IHl ]; intros t Ht; destruct Ht.
    subst; apply ty_rect.
    apply IHl; assumption.
  Qed.

End ty_rect.

Definition id_eq_dec (i1 i2 : id) : { i1 = i2 } + { i1 <> i2 }.
Proof.
  decide equality.
  apply eq_nat_dec.
Qed.

Definition list_eq_dec {X} l1 l2 :
     (forall x y : X, occ x l1 -> occ y l2 -> { x = y } + { x <> y })
  -> { l1 = l2 } + { l1 <> l2 }.
Proof.
  revert l2; induction l1 as [ | x l1 IH ]; intros [ | y l2 ] H.
  left; auto.
  right; discriminate.
  right; discriminate.
  destruct (H x y) as [ | C1 ]; try (left; auto; fail).
  subst.
  destruct (IH l2) as [ | C2 ].
  intros; apply H; right; auto.
  subst; left; auto.
  right; contradict C2; injection C2; auto.
  right; contradict C1; injection C1; auto.
Qed.

Definition ty_eq_dec (t1 t2 : ty) : { t1 = t2 } + { t1 <> t2 }.
Proof.
  revert t2; induction t1 as [ i1 | i1 l1 IHl ] using ty_rect; intros [
i2 | i2 l2 ].
  destruct (id_eq_dec i1 i2) as [ | C ]; [ left; subst | right;
contradict C; injection C ]; auto.
  right; discriminate.
  right; discriminate.
  destruct (id_eq_dec i1 i2) as [ | C ].
  2: right; contradict C; injection C; auto.
  subst i2.
  destruct (list_eq_dec l1 l2) as [ | C ].
  intros; auto.
  subst; left; auto.
  right; contradict C; injection C; auto.
Qed.