The Coq mailing list

[Rémi Nollet <remi.nollet AT ens-lyon.fr>]

It works perfectly. :D Thank you very much !
Rémi ~

On 13/07/2012 15:39, Adam Chlipala wrote:
> 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.