Library Tutorial


Examples about uses of the aac_rewrite library


Require Export AAC.
Require Instances.

Introductory examples


First, we settle in the context of Z, and show an usage of our tactics: we rewrite an universally quantified hypothesis modulo associativity and commutativity.

Section introduction.
  Import ZArith.
  Import Instances.Z.

  Variables a b c : Z.
  Hypothesis H: forall x, x + Zopp x = 0.
  Goal a + b + c + Zopp (c + a) = b.
    aac_rewrite H.
    aac_reflexivity.
  Qed.
  Goal a + c+ Zopp (b + a + Zopp b) = c.
    do 2 aac_rewrite H.
    reflexivity.
  Qed.

Notes:
  • the tactic handles arbitrary function symbols like Zopp (as long as they are proper morphisms);
  • here, ring would have done the job.

End introduction.

Second, we show how to exploit binomial identities to prove a goal about pythagorean triples, without breaking a sweat. By comparison, even if the goal and the hypothesis are both in normal form, making the rewrites using standard tools is difficult.

Section binomials.

  Import ZArith.
  Import Instances.Z.

  Notation "x ^2" := (x*x) (at level 40).
  Notation "2 ⋅ x" := (x+x) (at level 41).
  Lemma Hbin1: forall x y, (x+y)^2 = x^2 + y^2 + 2⋅x*y. Proof. intros; ring. Qed.
  Lemma Hbin2: forall x y, x^2 + y^2 = (x+y)^2 + -(2⋅x*y). Proof. intros; ring. Qed.
  Lemma Hopp : forall x, x + -x = 0. Proof Zplus_opp_r.

  Variables a b c : Z.
  Hypothesis H : c^2 + 2⋅(a+1)*b = (a+1+b)^2.
  Goal a^2 + b^2 + 2⋅a + 1 = c^2.
    aacu_rewrite <- Hbin1.
    aac_rewrite Hbin2.
    aac_rewrite <- H.
    aac_rewrite Hopp.
    aac_reflexivity.
  Qed.

Note: after the aac_rewrite <- H, one could use ring to close the proof.

End binomials.

Usage


One can also work in an abstract context, with arbitrary associative and commutative operators.

(Note that one can declare several operations of each kind; however, to be able to use this plugin, one currently needs at least one associative operator, and one associative-commutative operator.)

Section base.

  Context {X} {R} {E: Equivalence R}
  {plus} {zero}
  {dot} {one}
  {A: @Op_A X R dot one}
  {AC: Op_AC R plus zero}.

  Notation "x == y" := (R x y) (at level 70).
  Notation "x * y" := (dot x y) (at level 40, left associativity).
  Notation "1" := (one).
  Notation "x + y" := (plus x y) (at level 50, left associativity).
  Notation "0" := (zero).

In the very first example, ring would have solved the goal. Here, since dot does not necessarily distribute over plus, it is not possible to rely on it.

  Section reminder.
    Hypothesis H : forall x, x * x == x.
    Variables a b c : X.

    Goal (a+b+c)*(c+a+b) == a+b+c.
      aac_rewrite H.
      aac_reflexivity.
    Qed.

Note: the tactic starts by normalizing terms, so that trailing units are always eliminated.

    Goal ((a+b)+0+c)*((c+a)+b*1) == a+b+c.
      aac_rewrite H.
      aac_reflexivity.
    Qed.
  End reminder.

We can deal with "proper" morphisms of arbitrary arity (here f, or Zopp earlier), and rewrite under morphisms (here g).

  Section morphisms.
    Variable f : X -> X -> X.
    Hypothesis Hf : Proper (R ==> R ==> R) f.
    Variable g : X -> X.
    Hypothesis Hg : Proper (R ==> R) g.

    Variable a b: X.
    Hypothesis H : forall x y, x+f (b+y) x == y+x.
    Goal g ((f (a+b) a) + a) == g (a+a).
      aac_rewrite H.
      reflexivity.
    Qed.
  End morphisms.

Selecting what and where to rewrite


There are sometimes several possible rewriting. We now show how to interact with the tactic to select the desired one.

  Section occurrence.
    Variable f : X -> X .
    Variable a : X.
    Hypothesis Hf : Proper (R ==> R) f.
    Hypothesis H : forall x, x + x == x.

    Goal f(a+a)+f(a+a) == f a.
In case there are several possible solutions, one can print the different solutions using the aac_instances tactic (in proofgeneral, look at buffer *coq* ):
      aac_instances H.
the default choice is the smallest possible context (number 0), but one can choose the desired context;
      aac_rewrite H subterm 1.
now the goal is f a + f a == f a, there is only one solution.
      aac_rewrite H.
      reflexivity.
    Qed.

  End occurrence.

  Section subst.
    Variables a b c d : X.
    Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b.
    Hypothesis H': forall x, x + x == x.

    Goal a*c*d*c*d*b == a*c*d*b.
Here, there is only one possible context, but several substitutions;
      aac_instances H.
we can select them with the proper keyword.
      aac_rewrite H subst 1.
      aac_rewrite H'.
      aac_reflexivity.
    Qed.
  End subst.

As expected, one can use both keyword together to select the correct subterm and the correct substitution.

  Section both.
    Variables a b c d : X.
    Hypothesis H: forall x y, a*x*y*b == a*(x+y)*b.
    Hypothesis H': forall x, x + x == x.

    Goal a*c*d*c*d*b*b == a*(c*d+b)*b.
      aac_instances H.
      aac_rewrite H subterm 1 subst 1.
      aac_rewrite H.
      aac_rewrite H'.
      aac_reflexivity.
    Qed.

  End both.

We now turn on explaining the distinction between aac_rewrite and aacu_rewrite: aac_rewrite rejects solutions in which variables are instantiated by units, the companion tactic, aacu_rewrite allows such solutions.

  Section dealing_with_units.
    Variables a b c: X.
    Hypothesis H: forall x, a*x*a == x.
    Goal a*a == 1.
Here, x must be instantiated with 1, hence no solutions;
      aac_instances H.
while we get solutions with the "aacu" tactic.
      aacu_instances H.
      aacu_rewrite H.
      reflexivity.
    Qed.

We introduced this distinction because it allows us to rule out dummy cases in common situations:

    Hypothesis H': forall x y z, x*y + x*z == x*(y+z).
    Goal a*b*c + a*c+ a*b == a*(c+b*(1+c)).
6 solutions without units,
      aac_instances H'.
more than 52 with units.
      aacu_instances H'.
    Abort.

  End dealing_with_units.
End base.

Declaring instances


One can use one's own operations: it suffices to declare them as instances of our classes. (Note that these instances are already declared in file Instances.v.)

Section Peano.
  Require Import Arith.

  Program Instance nat_plus : Op_AC eq plus O.
  Solve All Obligations using firstorder.

  Program Instance nat_dot : Op_AC eq mult 1.
  Solve All Obligations using firstorder.

Caveat: we need at least an instance of an operator that is AC and one that is A for a given relation. However, one can reuse an AC operator as an A operator.

  Definition default_a := AC_A nat_dot. Existing Instance default_a.
End Peano.

Caveats


Section Peano'.
  Import Instances.Peano.

1. We have a special treatment for units, thus, S x + x does not match S 0, which is considered as a unit (one) of the mult operation.

  Section caveat_one.
    Definition double_plus_one x := 2*x + 1.
    Hypothesis H : forall x, S x + x = double_plus_one x.
    Goal S O = double_plus_one O.
      try aac_rewrite H.
0 solutions (normal since it would use 0 to instantiate x)
      try aacu_rewrite H.
0 solutions (abnormal)
    Abort.
  End caveat_one.

2. We cannot at the moment have two classes with the same units: in the following example, 0 is understood as the unit of max rather than as the unit of plus.

  Section max.
    Program Instance aac_max : Op_AC eq Max.max O := Build_Op_AC _ _ _ Max.max_assoc Max.max_comm.
    Variable a : nat.
    Goal 0 + a = a.
      try aac_reflexivity.
    Abort.
  End max.
End Peano'.

3. If some computations are possible in the goal or in the hypothesis, the inference mechanism we use will make the conversion. However, it seems that in most cases, these conversions can be done by hand using simpl rather than rewrite.

Section Z.

  Import ZArith.
  Open Scope Z_scope.
  Opaque Zmult.

  Hypothesis dot_ann_left :forall x, x * 0 = 0.
  Hypothesis dot_ann_right :forall x, 0 * x = 0.

  Goal forall a, a*0 = 0.
    intros. aacu_rewrite dot_ann_left. reflexivity.
  Qed.

Here the tactic fails, since the 0*a is converted to 0, and no rewrite can occur (even though Zmult is opaque).
  Goal forall a, 0*a = 0.
    intros. try aacu_rewrite dot_ann_left.
  Abort.

Here the tactic fails, since the 0*x is converted to 0 in the hypothesis.
  Goal forall a, a*0 = 0.
    intros. try aacu_rewrite dot_ann_right.
  Abort.


End Z.