The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Rémi Nollet wrote:
> 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
>
> I hoped [discriminate] would solve it, but it does not; and I have not 
> found anything which could help, me in the documentation.

I'm not aware of some hidden feature of Coq that would solve your 
problem directly, but here is an instance of a general recipe you can 
use for deriving such contradictions:

Fixpoint size (x : t) : nat :=
  match x with
    | Zero => O
    | Gen _ => O
    | Opp y => S (size y)
    | Add y z => size y + size z
  end.

Lemma size_argument : forall x y : t,
  size x <> size y
  -> x <> y.
  congruence.
Qed.

Require Import Omega.

Goal forall x y, x <> Add (Opp (Opp x)) y.
  intros; apply size_argument; simpl; omega.
Qed.