The Coq mailing list

[Laurent Thery <Laurent.Thery AT sophia.inria.fr>]

Hi,

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

Regards,


-- 
Laurent Thery     Phone (33) 4 92 38 78 16 e-mail 
Laurent.Thery AT inria.fr
Action Lemme INRIA - Sophia Antipolis,
2004, route des Lucioles - B.P. 93 
06902 Sophia Antipolis Cedex France