(* *********************************************************************** *)
(*  This is part of aac_tactics, it is distributed under the terms of the  *)
(*         GNU Lesser General Public License version 3                     *)
(*              (see file LICENSE for more details)                        *)
(*                                                                         *)
(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
(* *********************************************************************** *)

Tutorial for using AAC Tactics


From Coq Require PeanoNat ZArith List Permutation Lia.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.

Introductory example

Here is a first example with relative numbers (Z): one can rewrite an universally quantified hypothesis modulo the associativity and commutativity of Z.add.

Section introduction.
  Import ZArith.
  Import Instances.Z.

  Variables a b c : Z.
  Hypothesis H: forall x, x + Z.opp x = 0.

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

  Goal a + c + Z.opp (b + a + Z.opp b) = c.
    do 2 aac_rewrite H.
    reflexivity.
  Qed.

Note:
  • the tactic handles arbitrary function symbols like Z.opp (as long as they are proper morphisms w.r.t. the considered equivalence relation)
  • here, the ring tactic would have done the job
Several associative/commutative operations can be used at the same time, here, Z.mul and Z.add, which are both associative and commutative (AC)
  Goal (b + c) * (c + b) + a + Z.opp ((c + b) * (b + c)) = a.
    aac_rewrite H.
    aac_reflexivity.
  Qed.

Some commutative operations can be declared as idempotent, here Z.max which is taken into account by the aac_normalise and aac_reflexivity tactics; however, aac_rewrite does not match modulo idempotency
  Goal Z.max (b + c) (c + b) + a + Z.opp (c + b) = a.
    aac_normalise.
    aac_rewrite H.
    aac_reflexivity.
  Qed.

  Goal Z.max c (Z.max b c) + a + Z.opp (Z.max c b) = a.
    aac_normalise.
    aac_rewrite H.
    aac_reflexivity.
  Qed.

End introduction.

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.)

Section base.
  Context {X} {R} {E: Equivalence R}
  {plus} {dot} {zero} {one}
  {dot_A: @Associative X R dot }
  {plus_A: @Associative X R plus }
  {plus_C: @Commutative X R plus }
  {dot_Proper :Proper (R ==> R ==> R) dot}
  {plus_Proper :Proper (R ==> R ==> R) plus}
  {Zero : Unit R plus zero}
  {One : Unit R dot one}.

  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.

The tactic starts by normalising 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.

The tactic can deal with "proper" morphisms of arbitrary arity (here f and g, or Z.opp earlier): it rewrites under such morphisms (g), and, more importantly, it is able to reorder terms modulo AC under these morphisms (f)
  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 solutions to the matching problem. 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 the *coq* buffer): *)
      aac_instances H.
      (* the default choice is the occurrence with the smallest
        possible context (number 0), but one can choose the desired one *)
      aac_rewrite H at 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 occurrence, but several substitutions: *)
      aac_instances H.
      (* one 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 the keywords at and subst together to select the occurrence and the substitution. Note that by default, the rewrite is done in the left-hand side of the equation. We provide the keyword in_right to specify that the rewrite should instead be done in the right-hand side. The keyword in_right can then be combined with at and subst.
  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 at 1 subst 1.
      aac_instances H.
      aac_rewrite H.
      aac_rewrite H'.
      aac_rewrite H at 0 subst 1 in_right.
      aac_reflexivity.
    Qed.

  End both.

Distinction between aac_rewrite and aacu_rewrite

aac_rewrite rejects solutions in which variables are instantiated by units, while 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, so that the aac_*
        tactics give no solutions: *)
      try aac_instances H.
      (* while we get solutions with the aacu_* tactics: *)
      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'.
      aac_rewrite H' at 0.
      (* more than 52 with units *)
      aacu_instances H'.
    Abort.

  End dealing_with_units.
End base.

Declaring instances

To use one's own operations: it suffices to declare them as instances of our classes. (Note that the following instances are already declared in the Instances module.)

Section Peano.
  Import PeanoNat.

  #[local] Instance aac_Nat_add_Assoc : Associative eq Nat.add := Nat.add_assoc.
  #[local] Instance aac_Nat_add_Comm : Commutative eq Nat.add := Nat.add_comm.

  #[local] Instance aac_Nat_mul_Comm : Commutative eq Nat.mul := Nat.mul_comm.
  #[local] Instance aac_Nat_mul_Assoc : Associative eq Nat.mul := Nat.mul_assoc.

  #[local] Instance aac_Nat_mul_1_Unit : Unit eq Nat.mul 1 :=
    Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r.
  #[local] Instance aac_Nat_add_0_Unit : Unit eq Nat.add 0 :=
    Build_Unit eq Nat.add (O) Nat.add_0_l Nat.add_0_r.

Two (or more) operations may share the same units: in the following example, 0 is understood as the unit of Nat.max as well as the unit of Nat.add.

  #[local] Instance aac_Nat_max_Comm : Commutative eq Nat.max := Nat.max_comm.
  #[local] Instance aac_Nat_max_Assoc : Associative eq Nat.max := Nat.max_assoc.

Commutative operations may additionally be declared as idempotent. This does not change the behaviour of aac_rewrite, but this enables more simplifications in aac_normalise and aac_reflexivity.

  #[local] Instance aac_Nat_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.

  #[local] Instance aac_Nat_max_0_Unit : Unit eq Nat.max 0 :=
    Build_Unit eq Nat.max 0 Nat.max_0_l Nat.max_0_r.

  Variable a b c : nat.

  Goal Nat.max (a + 0) 0 = a.
    aac_reflexivity.
  Qed.

Here, we use idempotency:
  Goal Nat.max (a + 0) a = a.
    aac_reflexivity.
  Qed.

Furthermore, several operators can be mixed:
  Hypothesis H : forall x y z, Nat.max (x + y) (x + z) = x + Nat.max y z.

  Goal Nat.max (a + b) (c + (a * 1)) = Nat.max c b + a.
    aac_instances H. aac_rewrite H. aac_reflexivity.
  Qed.

  Goal Nat.max (a + b) (c + Nat.max (a*1+0) 0) = a + Nat.max b c.
    aac_instances H. aac_rewrite H. aac_reflexivity.
  Qed.

Working with inequations

To be able to use the tactics, the goal must be a relation R applied to two arguments, and the rewritten hypothesis must end with a relation Q applied to two arguments. These relations are not necessarily equivalences, but they should be related according to the occurrence where the rewrite takes place; we leave this check to the underlying call to setoid_rewrite.
One can rewrite equations in the left member of inequations:
  Goal (forall x, x + x = x) -> a + b + b + a <= a + b.
    intro Hx.
    aac_rewrite Hx.
    reflexivity.
  Qed.

Or in the right member of inequations, using the in_right keyword:
  Goal (forall x, x + x = x) -> a + b <= a + b + b + a.
    intro Hx.
    aac_rewrite Hx in_right.
    reflexivity.
  Qed.

Similarly, one can rewrite inequations in inequations:
  Goal (forall x, x + x <= x) -> a + b + b + a <= a + b.
    intro Hx.
    aac_rewrite Hx.
    reflexivity.
  Qed.

Possibly in the right-hand side:
  Goal (forall x, x <= x + x) -> a + b <= a + b + b + a.
    intro Hx.
    aac_rewrite <- Hx in_right.
    reflexivity.
  Qed.

aac_reflexivity deals with "trivial" inequations too:
  Goal Nat.max (a + b) (c + a) <= Nat.max (b + a) (c + 1*a).
    aac_reflexivity.
  Qed.

In the last three examples, there were no equivalence relations involved in the goal. However, we actually had to guess the equivalence relation with respect to which the operators (add,max,0) were AC. In this case, it was Leibniz equality eq so that it was automatically inferred; more generally, one can specify which equivalence relation to use by declaring instances of the AAC_lift type class:
  #[local] Instance aac_le_eq_lift : AAC_lift le eq := {}.
(This instance is automatically inferred because eq is always a valid candidate, here for le.)

End Peano.

Normalising goals

We also provide the tactics aac_normalise and aac_normalise_all to normalise terms modulo AC. This normalisation is the one we use internally.

Section AAC_normalise.
  Import Instances.Z.
  Import ZArith Lia.
  Open Scope Z_scope.

  Variable a b c d : Z.
  Goal a + (b + c*c*d) + a + 0 + d*1 = a.
    aac_normalise.
  Abort.

  Goal b + 0 + a = c*1 -> a+b = c.
    intro H.
    aac_normalise in H.
    assumption.
  Qed.

  Goal b + 0 + a = c*1+d -> a+b = d*(1+0)+c.
    intro.
    aac_normalise in *.
    assumption.
  Qed.

  Goal Z.max (a+b) (b+a) = a+b.
    aac_reflexivity.
  Abort.

Example by Abhishek Anand extracted from verification of a C++ gcd function
  Goal forall a b a' b' : Z,
    0 < b' -> Z.gcd a' b' = Z.gcd a b -> Z.gcd b' (a' mod b') = Z.gcd a b.
  Proof.
    intros.
    aac_rewrite Z.gcd_mod; try lia.
    aac_normalise_all.
    lia.
  Qed.
End AAC_normalise.

Examples from previous website


Section Examples.

  Import Instances.Z.
  Import ZArith Lia.
  Open Scope Z_scope.

Reverse triangle inequality


  Lemma Z_abs_triangle : forall x y, Z.abs (x + y) <= Z.abs x + Z.abs y.
  Proof Z.abs_triangle.

  Lemma Z_add_opp_diag_r : forall x, x + -x = 0.
  Proof Z.add_opp_diag_r.

The following morphisms are required to perform the required rewrites:
  #[local] Instance Z_opp_ge_le_compat : Proper (Z.ge ==> Z.le) Z.opp.
  Proof. intros x y. lia. Qed.

  #[local] Instance Z_add_le_compat : Proper (Z.le ==> Z.le ==> Z.le) Z.add.
  Proof. intros ? ? ? ? ? ?; lia. Qed.

  Goal forall a b, Z.abs a - Z.abs b <= Z.abs (a - b).
    intros. unfold Z.sub.
    aac_instances <- (Z.sub_diag b).
    aac_rewrite <- (Z.sub_diag b) at 3.
    unfold Z.sub.
    aac_rewrite Z_abs_triangle.
    aac_rewrite Z_add_opp_diag_r.
    aac_reflexivity.
  Qed.

Pythagorean triples


  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. apply Zplus_opp_r. Qed.

  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.
    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 Examples.

List examples


Section Lists.
  Import List Permutation.
  Import Instances.Lists.

  Variables (X : Type) (l1 l2 l3 : list X).

  Goal l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
    aac_reflexivity.
  Qed.

  Goal Permutation (l1 ++ l2) (l2 ++ l1).
    aac_reflexivity.
  Qed.

  Hypothesis H : Permutation l1 l2.

  Goal Permutation (l1 ++ l3) (l3 ++ l2).
    aac_rewrite H.
    aac_reflexivity.
  Qed.
End Lists.

Prop examples


Section Props.
  Import Instances.Prop_ops.

  Variables (P Q : Prop).

  Goal (Q /\ P) <-> (P /\ (Q /\ True)).
    aac_reflexivity.
  Qed.

  Goal (Q \/ P) <-> (P \/ (Q \/ False)).
    aac_reflexivity.
  Qed.
End Props.