The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Jul 13, 2012 at 6:34 AM, Rémi Nollet 
<remi.nollet AT ens-lyon.fr>
 wrote:
> Hello.
>
> I am looking for a tactic to solve a particular problem :
>
> I have a type for some trees, which is :
>
> Inductive t : Set :=
>   | Zero : t
>   | Gen : A -> t
>   | Opp : t -> t
>   | Add : t -> t -> t
>
> and I want to prove something like :
>
> Goal forall x y, x <> Add (Opp (Opp x)) y

My solution would be to use the well-foundedness of subterm relations
on inductive types.

(* First, some generic set-up: *)

Inductive TC {X:Type} (R:X->X->Prop) : X -> X -> Prop :=
| TC_base : forall x y:X, R x y -> TC R x y
| TC_step : forall x y z:X, TC R x y -> R y z -> TC R x z.

Lemma TC_wf : forall (X:Type) (R:X->X->Prop),
  well_founded R -> well_founded (TC R).
Proof.
intros.
intro x.
induction (H x).
constructor; intros.
destruct H2.
  eauto.

  apply (H1 _ H3); trivial.
Qed.

Lemma Acc_irrefl : forall (X:Type) (R:X->X->Prop) (x:X),
  Acc R x -> ~ R x x.
Proof.
intros.
induction H.
intro.
exact (H0 x H1 H1).
Qed.

Corollary wf_rel_impl_neq : forall (X:Type) (R:X->X->Prop)
  (x y:X), well_founded R -> R x y -> x <> y.
Proof.
intros; red; destruct 1.
exact (Acc_irrefl _ _ _ (H x) H0).
Qed.

Corollary wf_TC_rel_impl_neq : forall (X:Type) (R:X->X->Prop)
  (x y:X), well_founded R -> TC R x y -> x <> y.
Proof.
eauto using wf_rel_impl_neq, TC_wf.
Qed.

(* And then the arguments specific to your example: *)

Parameter A : Set.

Inductive t : Set :=
  | Zero : t
  | Gen : A -> t
  | Opp : t -> t
  | Add : t -> t -> t.

Inductive t_subterm : t -> t -> Prop :=
| Opp_subterm : forall x:t, t_subterm x (Opp x)
| Add_subterm_l : forall x y:t, t_subterm x (Add x y)
| Add_subterm_r : forall x y:t, t_subterm y (Add x y).

Lemma t_subterm_wf : well_founded t_subterm.
Proof.
intro x; induction x; constructor; inversion 1; trivial.
Qed.

Goal forall x y, x <> Add (Opp (Opp x)) y.
Proof.
eauto using wf_TC_rel_impl_neq, t_subterm_wf, @TC, t_subterm.
Qed.

Essentially, Adam's solution was proving the well-foundedness of (TC
t_subterm) using the size function and the well-foundedness of lt on
nat.  (And in fact, the latter well-foundedness can be seen as a
special case of this argument, since lt is exactly the transitive
closure of the "subterm" relation on nat.)
-- 
Daniel Schepler