The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>]

I once wrote the following tactic. It applies on a goal of the form
(f x y ...) = (f x' y' ...), and try to solve it by proving x=x',
y=y'.... Of course if f is not a constructor this generally won't
work.

By the way if someone knows how to make it more general and cleaner in
Ltac... The basic problem is that I have to consider each arity
separately.


Tactic Definition Decompeq :=
Match Context With
 [|-(?1 ?2)=(?1 ?3)]
 -> 
  Try (Replace ?3 with ?2;Auto)
 | [|-(?1 ?2 ?4)=(?1 ?3 ?5)]
 -> 
  Try (Replace ?3 with ?2;Auto);
  Try (Replace ?5 with ?4;Auto)
 | [|-(?1 ?2 ?4 ?6)=(?1 ?3 ?5 ?7)]
 -> 
  Try (Replace ?3 with ?2;Auto);
  Try (Replace ?5 with ?4;Auto);
  Try (Replace ?7 with ?6;Auto)
 | [|-(?1 ?2 ?4 ?6 ?8)=(?1 ?3 ?5 ?7 ?9)]
 -> 
  Try (Replace ?3 with ?2;Auto);
  Try (Replace ?5 with ?4;Auto);
  Try (Replace ?7 with ?6;Auto);
  Try (Replace ?9 with ?8;Auto)
 | [|-(?1 ?2 ?4 ?6 ?8 ?10)=(?1 ?3 ?5 ?7 ?9 ?11)]
 -> 
  Try (Replace ?3 with ?2;Auto);
  Try (Replace ?5 with ?4;Auto);
  Try (Replace ?7 with ?6;Auto);
  Try (Replace ?9 with ?8;Auto);
  Try (Replace ?11 with ?10;Auto)
 | [|-(?1 ?2 ?4 ?6 ?8 ?10 ?12)=(?1 ?3 ?5 ?7 ?9 ?11 ?13)]
 -> 
  Try (Replace ?3 with ?2;Auto);
  Try (Replace ?5 with ?4;Auto);
  Try (Replace ?7 with ?6;Auto);
  Try (Replace ?9 with ?8;Auto);
  Try (Replace ?11 with ?10;Auto);
  Try (Replace ?13 with ?12;Auto).






Benjamin GREGOIRE 
<Benjamin.Gregoire AT inria.fr>
 wrote:
> Romain Janvier wrote:
> 
> > Is there a tactic that can automaticly transforme a goal the same way
> > that "inversion" does with the hypothesys as (Pair A x)=(Pair A B)
> > giving x=B.