The Coq mailing list

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

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

I hoped [discriminate] would solve it, but it does not; and I have not 
found anything which could help, me in the documentation.

Actually, very simple cases such as [forall x, x <> Opp x] are easily 
proved by [induction] and [injection]/[inversion], but the first example 
I gave is not.

I still managed to solve it (by constructing a function f such that the 
call f x, morally, does not terminate, and therefore can be typed as 
False), but I have to rewrite this (not so short) proof entirely for 
each such case I encounter (and there are many of them). Neither have I 
succeeding in writing it with Ltac, because it would presuppose that I 
could pick a pattern into the context and use it to create a new pattern 
matching, which is, as far as I know, not allowed.

Does somebody already dealt with that ?

(Otherwise I guess I could write a tactic in OCaml for that, but it 
seems to be quite complicated... :p)

I hope this list to be the right place for this kind of questions...
Thank you all.

Rémi Nollet ~