diff options
Diffstat (limited to 'theories/Tutorial.v')
| -rw-r--r-- | theories/Tutorial.v | 401 |
1 files changed, 401 insertions, 0 deletions
diff --git a/theories/Tutorial.v b/theories/Tutorial.v new file mode 100644 index 0000000..e403d92 --- /dev/null +++ b/theories/Tutorial.v @@ -0,0 +1,401 @@ +(***************************************************************************) +(* 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 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. *) + +Require Arith ZArith. + +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 [Zplus]. *) + +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. + + (** 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. + *) + +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 [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* ): *) + 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 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. *) + + 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 file [Instances.v].) *) + +Section Peano. + 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, *) + 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 Max.max (a + b) (c + a) <= Max.max (b + a) (c + 1*a). + aac_reflexivity. + Qed. + + (** 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: *) + + Instance lift_le_eq : 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 a tactic to normalise terms modulo AC. This + normalisation is the one we use internally. *) + +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. + +End AAC_normalise. + + + + +(** ** Examples from the web page *) +Section Examples. + + Import Instances.Z. + Import ZArith. + Open Scope Z_scope. + + (** *** Reverse triangle inequality *) + + Lemma Zabs_triangle : forall x y, Z.abs (x + y) <= Z.abs x + Z.abs y . + Proof Z.abs_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 (Z.ge ==> Z.le) Z.opp. + Proof. intros x y. omega. Qed. + + Instance Proper_Zplus : Proper (Z.le ==> Z.le ==> Z.le) Zplus. + Proof. firstorder. Qed. + + Goal forall 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. + + + (** *** 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 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.*) + +End Examples. + + |