The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

Hi all

Each time I reach a goal like (f a b ... = f c d ...) and I know that the 
arguments can be proved pairwise equal, it always takes me some time to 
remember the proper use of the lemmas a la f_equal, with their implicits 
arguments. So last time I designed some ltac code to take care of these
situations. Maybe this can interest others ?

The first try:

Ltac equal :=
  match goal with
   | |- ?f  _ = ?f _ => apply f_equal with (f:=f)
   | |- ?f _ _ = ?f _ _=> apply f_equal2 with (f:=f)
   | |- ?f _ _ _ = ?f _ _ _ => apply f_equal3 with (f:=f)
   | |- ?f _ _ _ _ = ?f _ _ _ _=> apply f_equal4 with (f:=f)
   | |- ?f _ _ _ _ _ = ?f _ _ _ _ _ => apply f_equal5 with (f:=f)
   | _ => idtac
  end.

This simple code works ok for simple situations, more precisely when there 
is no dependency in the type of f. But the exact goal I was trying to 
solve was (a,b)=(c,d), that is (pair A B a b)=(pair A B c d). Here is a 
(ugly) version that can handle that, based on the proofs of f_equal* :

Ltac equal :=
  let des := destruct 1 || intro in
  let r := try reflexivity in
  match goal with
   | |- ?f ?a = ?f' ?a' => cut (a=a'); des; r
   | |- ?f ?a ?b = ?f' ?a' ?b' =>
      cut (b=b');[cut (a=a');[do 2 des; r|r]|r]
   | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=>
      cut (c=c');[cut (b=b');[cut (a=a');[do 3 des; r|r]|r]|r]
   | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=>
      cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[do 4 des; r|r]|r]|r]|r]
  | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=>
      cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[do 5 des; 
r|r]|r]|r]|r]|r]
   | _ => idtac
  end.

One example:

Require Import ArithRing.
Lemma demo_equal : forall x y, (x*2,y*2)=(x+x,y+y).
intros.
equal.
ring.
ring.
Qed.