The Coq mailing list

[Hugo Herbelin <herbelin AT margaux.inria.fr>]

  Hi Laurent,

> I often need in my proofs to saturate my assumption lists to get
> new facts.
> 
> If I have the goal:
> 
> A: Set
> a0: A
> b0 : A
> c0: A
> Trans: (a,b,c: A) a = b -> b = c -> a = c
> Sym: (a,b) a = b -> b = a 
> Fact1: a0 = b0
> Fact2: b0 = c0
>   ============================
>     G
> 
> 
> I would like a tactic that adds the assumptions a0=c0 and c0=a0.
> 
> Has any Coq user developed such a tactic

  You could do this using AutoRewrite. The syntax is still more
sh-like than Coq-like but it works good ;)

Coq < Goal (a,b,c:nat)a=b-> c=b-> c=a.
Coq < Intros.AutoRewrite [[H LR] [H0 LR]] Step=[Trivial].
Subtree proved!

  To use commutativity, you could add "Sym" in the Step list as well.
There are a lot of customization available to circumvent circularity.

  Bon courage,
                                                  Hugo