The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/04/2015 03:09 PM, Jonathan Leivent wrote:
> On 11/04/2015 02:47 PM, Michael Shulman wrote:
> > On Wed, Nov 4, 2015 at 8:35 AM, Jonathan Leivent 
> > <jonikelee AT gmail.com> wrote:
> > > I have been developing a set of tactics that does something like this -
> > > it rewrites ring equality hyps so that they have a single variable on
> > > their lhs, and then rewrites them over the goal, which produces a more
> > > general rewriting.
> > Nice!  Is anything available yet?
>
> I have a working version embedded into other things - I will dis-embed 
> it shortly and pass it along...

Here it is (attached).

-- Jonathan

Require Import ZArith.
Open Scope Z_scope.

Lemma lhsify_rw : forall (x y : Z), x = y <-> x - y = 0.
Proof. intros; omega. Qed.

Lemma deadd1 : forall x y z, x + y = z <-> x = z - y.
Proof. intros; omega. Qed.

Lemma deadd2 : forall x y z, x + y = z <-> y = z - x.
Proof. intros; omega. Qed.

Lemma desub1 : forall x y z, x - y = z <-> x = z + y.
Proof. intros; omega. Qed.

Lemma desub2 : forall x y z, x - y = z <-> y = x - z.
Proof. intros; omega. Qed.

Lemma deopp : forall x y, -x = y <-> x = -y.
Proof. intros; omega. Qed.


Ltac z_subst H :=
  lazymatch type of H with
  | ?X + ?Y = _ => 
    (*use backtrackable choice to search for a monomial var*)
    (rewrite (deadd1 X Y) in H + rewrite (deadd2 X Y) in H);
    z_subst H
  | ?X - ?Y = _ => 
    (rewrite (desub1 X Y) in H + rewrite (desub2 X Y) in H);
    z_subst H
  | - ?X = _ => 
    rewrite (deopp X) in H;
    z_subst H
  | ?V = _ =>
    is_var V; (*found a monomial var*)
    (*don't rewrite and clear unless the rewrite does something*)
    rewrite !H in *;
    clear V H
  end.

Ltac z_hyp H :=
  rewrite lhsify_rw in H; z_subst H.

Goal forall x y z, x*y = z + 2 -> z = y*x - 2.
intros x y z H.
Fail omega.
Fail ring.
z_hyp H.
ring.
Qed.