diff options
Diffstat (limited to 'Tutorial.v')
| -rw-r--r-- | Tutorial.v | 126 |
1 files changed, 63 insertions, 63 deletions
@@ -6,7 +6,7 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) -(** * Tutorial for using the [aac_tactics] library. +(** * 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 @@ -17,7 +17,7 @@ Add ML Path ".". Require Import AAC. Require Instances. -(** ** Introductory example +(** ** Introductory example Here is a first example with relative numbers ([Z]): one can rewrite an universally quantified hypothesis modulo the @@ -39,37 +39,37 @@ Section introduction. reflexivity. Qed. - (** Notes: + (** 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. +End introduction. -(** ** Usage +(** ** 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} + Context {X} {R} {E: Equivalence R} + {plus} + {dot} {zero} {one} - {dot_A: @Associative X R dot } + {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). @@ -83,7 +83,7 @@ Section base. 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. @@ -97,7 +97,7 @@ Section base. 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 @@ -108,7 +108,7 @@ Section base. 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). @@ -117,7 +117,7 @@ Section base. Qed. End morphisms. - (** *** Selecting what and where to rewrite + (** *** 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 @@ -127,7 +127,7 @@ Section base. Variable f : X -> X. Variable a : X. Hypothesis Hf : Proper (R ==> R) f. - Hypothesis H : forall x, x + x == x. + 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 @@ -137,29 +137,29 @@ Section base. (** 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 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 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 @@ -169,7 +169,7 @@ Section base. 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. @@ -179,10 +179,10 @@ Section base. aac_rewrite H at 0 subst 1 in_right. aac_reflexivity. Qed. - + End both. - (** *** Distinction between [aac_rewrite] and [aacu_rewrite]: + (** *** 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 @@ -192,31 +192,31 @@ Section base. 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_*] + (** 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. *) + try aac_instances H. + (** while we get solutions with the [aacu_*] tactics. *) aacu_instances H. aacu_rewrite H. reflexivity. - Qed. - + 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_instances H'. aac_rewrite H' at 0. (** more than 52 with units. *) aacu_instances H'. Abort. - End dealing_with_units. + End dealing_with_units. End base. -(** *** Declaring instances +(** *** Declaring instances To use one's own operations: it suffices to declare them as instances of our classes. (Note that the following instances are @@ -224,15 +224,15 @@ End base. 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 := + + 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 @@ -241,26 +241,26 @@ Section Peano. 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. + 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. + + 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. + 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] @@ -272,28 +272,28 @@ Section Peano. (** One can rewrite equations in the left member of inequations, *) Goal (forall x, x + x = x) -> a + b + b + a <= a + b. - intro Hx. + 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. + 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. + intro Hx. aac_rewrite Hx. reflexivity. - Qed. + Qed. (** possibly in the right-hand side. *) Goal (forall x, x <= x + x) -> a + b <= a + b + b + a. - intro Hx. + intro Hx. aac_rewrite <- Hx in_right. reflexivity. Qed. @@ -319,7 +319,7 @@ Section Peano. End Peano. -(** *** Normalising goals +(** *** Normalising goals We also provide a tactic to normalise terms modulo AC. This normalisation is the one we use internally. *) @@ -329,7 +329,7 @@ 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. @@ -349,16 +349,16 @@ Section Examples. (** *** Reverse triangle inequality *) - Lemma Zabs_triangle : forall x y, Zabs (x + y) <= Zabs x + Zabs y . - Proof Zabs_triangle. + 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. + 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. @@ -367,8 +367,8 @@ Section Examples. aac_instances <- (Zminus_diag b). aac_rewrite <- (Zminus_diag b) at 3. unfold Zminus. - aac_rewrite Zabs_triangle. - aac_rewrite Zplus_opp_r. + aac_rewrite Zabs_triangle. + aac_rewrite Zplus_opp_r. aac_reflexivity. Qed. @@ -380,8 +380,8 @@ Section Examples. 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. - + 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. |