Library AAC_tactics.Tutorial
From Coq Require PeanoNat ZArith List Permutation Lia.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.
Introductory example
Section introduction.
Import ZArith.
Import Instances.Z.
Variables a b c : Z.
Hypothesis H: ∀ 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.
Notes:
several associative/commutative operations can be used at the same time.
here, Zmult and Zplus, which are both associative and commutative (AC)
- the tactic handles arbitrary function symbols like Zopp (as long as they are proper morphisms w.r.t. the considered equivalence relation);
- here, ring would have done the job.
some commutative operations can be declared as idempotent, here Z.max
which is taken into account by the aac_normalise and aac_reflexivity tactics.
Note however that 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.
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
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 : ∀ 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.
The tactic can deal with "proper" morphisms of arbitrary arity
(here f and g, or Zopp 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 : ∀ 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
Section occurrence.
Variable f : X → X.
Variable a : X.
Hypothesis Hf : Proper (R ==> R) f.
Hypothesis H : ∀ 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
proof-general, look at buffer *coq* ):
the default choice is the occurrence with the smallest
possible context (number 0), but one can choose the desired
one;
aac_rewrite H.
reflexivity.
Qed.
End occurrence.
Section subst.
Variables a b c d : X.
Hypothesis H: ∀ x y, a×x×y×b == a*(x+y)*b.
Hypothesis H': ∀ x, x + x == x.
Goal a×c×d×c×d×b == a×c×d×b.
reflexivity.
Qed.
End occurrence.
Section subst.
Variables a b c d : X.
Hypothesis H: ∀ x y, a×x×y×b == a*(x+y)*b.
Hypothesis H': ∀ 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;
one can select them with the proper keyword.
As expected, one can use both keywords together to select the
occurrence and the substitution. We also provide a keyword to
specify that the rewrite should be done in the right-hand side of
the equation.
Section both.
Variables a b c d : X.
Hypothesis H: ∀ x y, a×x×y×b == a*(x+y)*b.
Hypothesis H': ∀ 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:
Here, x must be instantiated with 1, so that the aac_×
tactics give no solutions;
while we get solutions with the aacu_× tactics.
We introduced this distinction because it allows us to rule
out dummy cases in common situations:
6 solutions without units,
more than 52 with units.
Declaring instances
Section Peano.
Import PeanoNat.
Instance aac_add_Assoc : Associative eq Nat.add := Nat.add_assoc.
Instance aac_add_Comm : Commutative eq Nat.add := Nat.add_comm.
Instance aac_mul_Comm : Commutative eq Nat.mul := Nat.mul_comm.
Instance aac_mul_Assoc : Associative eq Nat.mul := Nat.mul_assoc.
Instance aac_one : Unit eq Nat.mul 1 :=
Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r.
Instance aac_zero_add : Unit eq Nat.add O :=
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 max as well as
the unit of plus.
Instance aac_max_Comm : Commutative eq Nat.max := Nat.max_comm.
Instance aac_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.
Instance aac_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.
Instance aac_zero_max : Unit eq Nat.max O :=
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.
Instance aac_zero_max : Unit eq Nat.max O :=
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.
Furthermore, several operators can be mixed:
Hypothesis H : ∀ 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.
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
or in the right member of inequations, using the in_right keyword
Similarly, one can rewrite inequations in inequations,
possibly in the right-hand side.
Goal (∀ x, x ≤ x + x) → a + b ≤ a + b + b + a.
intro Hx.
aac_rewrite <- Hx in_right.
reflexivity.
Qed.
intro Hx.
aac_rewrite <- Hx in_right.
reflexivity.
Qed.
aac_reflexivity deals with "trivial" inequations too
In the last three examples, there were no equivalence relation
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:
Normalising goals
Section AAC_normalise.
Import Instances.Z.
Import ZArith.
Open Scope Z_scope.
Variable a b c d : Z.
Goal a + (b + c×c×d) + a + 0 + d*1 = a.
aac_normalise.
Abort.
Print HintDb typeclass_instances.
Goal Z.max (a+b) (b+a) = a+b.
aac_reflexivity.
Show Proof.
Abort.
End AAC_normalise.
Lemma Zabs_triangle : ∀ x y, Z.abs (x + y) ≤ Z.abs x + Z.abs y .
Proof Z.abs_triangle.
Lemma Zplus_opp_r : ∀ x, x + -x = 0.
Proof Zplus_opp_r.
The following morphisms are required to perform the required rewrites
Instance Zminus_compat : Proper (Z.ge ==> Z.le) Z.opp.
Proof. intros x y. lia. Qed.
Instance Proper_Zplus : Proper (Z.le ==> Z.le ==> Z.le) Zplus.
Proof. intros ? ? ? ? ? ?; lia. Qed.
Goal ∀ a b, Z.abs a - Z.abs b ≤ Z.abs (a - b).
intros. unfold Zminus.
aac_instances <- (Zminus_diag b).
aac_rewrite <- (Zminus_diag b) at 3.
unfold Zminus.
aac_rewrite Z.abs_triangle.
aac_rewrite Zplus_opp_r.
aac_reflexivity.
Qed.
Proof. intros x y. lia. Qed.
Instance Proper_Zplus : Proper (Z.le ==> Z.le ==> Z.le) Zplus.
Proof. intros ? ? ? ? ? ?; lia. Qed.
Goal ∀ a b, Z.abs a - Z.abs b ≤ Z.abs (a - b).
intros. unfold Zminus.
aac_instances <- (Zminus_diag b).
aac_rewrite <- (Zminus_diag b) at 3.
unfold Zminus.
aac_rewrite Z.abs_triangle.
aac_rewrite Zplus_opp_r.
aac_reflexivity.
Qed.
Notation "x ^2" := (x×x) (at level 40).
Notation "2 ⋅ x" := (x+x) (at level 41).
Lemma Hbin1: ∀ x y, (x+y)^2 = x^2 + y^2 + 2⋅x×y. Proof. intros; ring. Qed.
Lemma Hbin2: ∀ x y, x^2 + y^2 = (x+y)^2 + -(2⋅x×y). Proof. intros; ring. Qed.
Lemma Hopp : ∀ 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.
rewrite Hbin2.
aac_rewrite <- H.
aac_rewrite Hopp.
aac_reflexivity.
Qed.
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.
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.