The Coq mailing list

[maggesi AT math.unice.fr (Marco.MAGGESI)]

Hi,

I wrote a tactic that I use a lot.  I called it "Congr" for lack of a
better name.  It has very little to with the new "Congruence" tactic
now available in Coq 8.0.

It works for goals that are equalities.  It compares the structure of
left and right terms and when both terms have the same head it try to
reduce the goal to the equality of their subterms.

This version of "Congr" is a "quick hack" but works pretty well in
practice.  It has several limitations that I would like to remove but
I do not know how do that in a simple way using the tactic language.
In particular, it works only for equations of the form

  f x_1 ... x_n = f y_1 ... y_n

where n <= 6.  The problem is that I cannot get around the fact that
match doesn't work with curried functions.

Any idea?


The listing of the file "Congr.v" with the source of the tactic is
at the end of this message.

The following script illustrate the effect of the tactic:


    Implicit Arguments On.
    
    Require Export List.
    
    Lemma app_nil_end : forall A (l:list A), l = l ++ nil.
    Proof. 
      induction l; simpl; auto.
      rewrite <- IHl.
      reflexivity.
    Qed.
    
    Require Export Congr.
    
    Lemma app_nil_end_NEW : forall A (l:list A), l = l ++ nil.
    Proof. 
      induction l; simpl; auto.
    Qed.


Try and enjoy,

  -- Marco




(* ------------------------------------------------------------ *)
(* File: Congr.v                                                *)
(* ------------------------------------------------------------ *)

Implicit Arguments On.

Ltac congr :=
  match goal with
  | |- ?f ?a = ?f ?b =>
      change ((fun u => f a = f u) b);
      replace b with a; trivial with *
  | |- ?f ?a ?a2= ?f ?b ?a2  =>
      change ((fun u => f a a2 = f u a2) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a= ?f ?b1 ?b =>
      change ((fun u => f a1 a = f b1 u) b);
      replace b with a; trivial with *
  | |- ?f ?a ?a2 ?a3 = ?f ?b ?a2 ?a3 =>
      change ((fun u => f a a2 a3 = f u a2 a3) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a ?a3 = ?f ?b1 ?b ?a3 =>
      change ((fun u => f a1 a a3 = f b1 u a3) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a = ?f ?b1 ?b2 ?b =>
      change ((fun u => f a1 a2 a = f b1 b2 u) b);
      replace b with a; trivial with *
  | |- ?f ?a ?a2 ?a3 ?a4 = ?f ?b ?a2 ?a3 ?a4 =>
      change ((fun u => f a a2 a3 a4 = f u a2 a3 a4) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a ?a3 ?a4 = ?f ?b1 ?b ?a3 ?a4 =>
      change ((fun u => f a1 a a3 a4 = f b1 u a3 a4) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a ?a4 = ?f ?b1 ?b2 ?b ?a4 =>
      change ((fun u => f a1 a2 a a4 = f b1 b2 u a4) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a3 ?a = ?f ?b1 ?b2 ?b3 ?b =>
      change ((fun u => f a1 a2 a3 a = f b1 b2 b3 u) b);
      replace b with a; trivial with *
  | |- ?f ?a ?a2 ?a3 ?a4 ?a5 = ?f ?b ?a2 ?a3 ?a4 ?a5 =>
      change ((fun u => f a a2 a3 a4 a5 = f u a2 a3 a4 a5) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a ?a3 ?a4 ?a5 = ?f ?a1 ?b ?a3 ?a4 ?a5 =>
      change ((fun u => f a1 a a3 a4 a5 = f a1 u a3 a4 a5) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a ?a4 ?a5 = ?f ?a1 ?a2 ?b ?a4 ?a5 =>
      change ((fun u => f a1 a2 a a4 a5 = f a1 a2 u a4 a5) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a3 ?a ?a5 = ?f ?a1 ?a2 ?a3 ?b ?a5 =>
      change ((fun u => f a1 a2 a3 a a5 = f a1 a2 a3 u a5) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a3 ?a4 ?a = ?f ?a1 ?a2 ?a3 ?a4 ?b =>
      change ((fun u => f a1 a2 a3 a4 a = f a1 a2 a3 a4 u) b);
      replace b with a; trivial with *
  | |- ?f ?a ?a2 ?a3 ?a4 ?a5 ?a6 = ?f ?b ?a2 ?a3 ?a4 ?a5 ?a6 =>
      change ((fun u => f a a2 a3 a4 a5 a6 = f u a2 a3 a4 a5 a6) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a ?a3 ?a4 ?a5 ?a6 = ?f ?a1 ?b ?a3 ?a4 ?a5 ?a6 =>
      change ((fun u => f a1 a a3 a4 a5 a6 = f a1 u a3 a4 a5 a6) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a ?a4 ?a5 ?a6 = ?f ?a1 ?a2 ?b ?a4 ?a5 ?a6 =>
      change ((fun u => f a1 a2 a a4 a5 a6 = f a1 a2 u a4 a5 a6) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a3 ?a ?a5 ?a6 = ?f ?a1 ?a2 ?a3 ?b ?a5 ?a6 =>
      change ((fun u => f a1 a2 a3 a a5 a6 = f a1 a2 a3 u a5 a6) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a3 ?a4 ?a ?a6 = ?f ?a1 ?a2 ?a3 ?a4 ?b ?a6 =>
      change ((fun u => f a1 a2 a3 a4 a a6 = f a1 a2 a3 a4 u a6) b);
      replace b with a; trivial with *
  | |- ?f ?a1 ?a2 ?a3 ?a4 ?a5 ?a = ?f ?a1 ?a2 ?a3 ?a4 ?a5 ?b =>
      change ((fun u => f a1 a2 a3 a4 a5 a = f a1 a2 a3 a4 a5 u) b);
      replace b with a; trivial with *
  end.


Hint Extern 1 (?x = ?y) => congr.