Tutorial for using the aac_tactics library.
Depending on your installation, either modify the following two lines, or add them to your .coqrc files, replacing "." with the path to the aac_tactics library.
Add Rec LoadPath "." as AAC_tactics.
Add ML Path ".".
Require Import AAC.
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 Zplus.
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 w.r.t. the considered equivalence relation);
- here, ring would have done the job.
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.
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 : 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
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;
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.
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;
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: 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.
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
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 file Instances.v.)
Section Peano.
Require Import Arith.
Instance aac_plus_Assoc : Associative eq plus := plus_assoc.
Instance aac_plus_Comm : Commutative eq plus := plus_comm.
Instance aac_one : Unit eq mult 1 :=
Build_Unit eq mult 1 mult_1_l mult_1_r.
Instance aac_zero_plus : Unit eq plus O :=
Build_Unit eq plus (O) plus_0_l plus_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 Max.max := Max.max_comm.
Instance aac_max_Assoc : Associative eq Max.max := Max.max_assoc.
Instance aac_zero_max : Unit eq Max.max O :=
Build_Unit eq Max.max 0 Max.max_0_l Max.max_0_r.
Variable a b c : nat.
Goal Max.max (a + 0) 0 = a.
aac_reflexivity.
Qed.
Furthermore, several operators can be mixed:
Hypothesis H : forall x y z, Max.max (x + y) (x + z) = x+ Max.max y z.
Goal Max.max (a + b) (c + (a * 1)) = Max.max c b + a.
aac_instances H. aac_rewrite H. aac_reflexivity.
Qed.
Goal Max.max (a + b) (c + Max.max (a*1+0) 0) = a + Max.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,
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.
intro Hx.
aac_rewrite Hx in_right.
reflexivity.
Qed.
Similarly, one can rewrite inequations in inequations,
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.
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
(plus,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:
(This instance is automatically inferred because eq is always a
valid candidate, here for le.)
Normalising goals
We also provide a tactic to normalise terms modulo AC. This normalisation is the one we use internally.
Section AAC_normalise.
Import Instances.Z.
Require 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.
End AAC_normalise.
Lemma Zabs_triangle : forall x y, Zabs (x + y) <= Zabs x + Zabs y .
Proof Zabs_triangle.
Lemma Zplus_opp_r : forall x, x + -x = 0.
Proof Zplus_opp_r.
The following morphisms are required to perform the required rewrites
Instance Zminus_compat : Proper (Zge ==> Zle) Zopp.
Proof. intros x y. omega. Qed.
Instance Proper_Zplus : Proper (Zle ==> Zle ==> Zle) Zplus.
Proof. firstorder. Qed.
Goal forall a b, Zabs a - Zabs b <= Zabs (a - b).
intros. unfold Zminus.
aac_instances <- (Zminus_diag b).
aac_rewrite <- (Zminus_diag b) at 3.
unfold Zminus.
aac_rewrite Zabs_triangle.
aac_rewrite Zplus_opp_r.
aac_reflexivity.
Qed.
Proof. intros x y. omega. Qed.
Instance Proper_Zplus : Proper (Zle ==> Zle ==> Zle) Zplus.
Proof. firstorder. Qed.
Goal forall a b, Zabs a - Zabs b <= Zabs (a - b).
intros. unfold Zminus.
aac_instances <- (Zminus_diag b).
aac_rewrite <- (Zminus_diag b) at 3.
unfold Zminus.
aac_rewrite Zabs_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: 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.
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.
This page has been generated by coqdoc