diff options
Diffstat (limited to 'Tutorial.v')
| -rw-r--r-- | Tutorial.v | 416 |
1 files changed, 247 insertions, 169 deletions
@@ -6,97 +6,70 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) -(** * Examples about uses of the aac_rewrite library *) +(** * Tutorial for using the [aac_tactics] library. -(* - Depending on your installation, either uncomment the following two - lines, or add them to your .coqrc files, replacing path_to_aac_tactics - with the correct path for your installation: + 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 "path_to_aac_tactics". - Add ML Path "path_to_aac_tactics". -*) -Require Export AAC. +Add Rec LoadPath "." as AAC_tactics. +Add ML Path ".". +Require Import AAC. Require Instances. -(** ** Introductory examples *) +(** ** Introductory example -(** First, we settle in the context of Z, and show an usage of our -tactics: we rewrite an universally quantified hypothesis modulo -associativity and commutativity. *) + 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. + Goal a + c + Zopp (b + a + Zopp b) = c. do 2 aac_rewrite H. reflexivity. Qed. - (** Notes: + (** Notes: - the tactic handles arbitrary function symbols like [Zopp] (as - long as they are proper morphisms); + long as they are proper morphisms w.r.t. the considered + equivalence relation); - here, ring would have done the job. *) -End introduction. - -(** Second, we show how to exploit binomial identities to prove a goal -about pythagorean triples, without breaking a sweat. By comparison, -even if the goal and the hypothesis are both in normal form, making -the rewrites using standard tools is difficult. -*) - -Section binomials. - - Import ZArith. - Import Instances.Z. - - 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. - aac_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 binomials. +End introduction. -(** ** Usage *) -(** One can also work in an abstract context, with arbitrary - associative and commutative operators. +(** ** Usage - (Note that one can declare several operations of each kind; - however, to be able to use this plugin, one currently needs at least - one associative operator, and one associative-commutative - operator.) *) + 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} {zero} - {dot} {one} - {A: @Op_A X R dot one} - {AC: Op_AC R plus zero}. - + 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). @@ -110,30 +83,32 @@ 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. Qed. - (** Note: the tactic starts by normalizing terms, so that trailing - units are always eliminated. *) + (** 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. - - (** We can deal with "proper" morphisms of arbitrary arity (here [f], - or [Zopp] earlier), and rewrite under morphisms (here [g]). *) + + (** 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). @@ -142,180 +117,283 @@ Section base. Qed. End morphisms. - (** ** Selecting what and where to rewrite *) + (** *** Selecting what and where to rewrite - (** There are sometimes several possible rewriting. We now show how - to interact with the tactic to select the desired one. *) + 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 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 the different solutions using the [aac_instances] tactic (in - proofgeneral, look at buffer *coq* ): *) + proof-general, look at buffer *coq* ): *) aac_instances H. - (** the default choice is the smallest possible context (number - 0), but one can choose the desired context; *) - aac_rewrite H subterm 1. - (** now the goal is [f a + f a == f a], there is only one solution. *) + (** 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 context, but several substitutions; *) + (** Here, there is only one possible occurrence, but several substitutions; *) aac_instances H. - (** we can select them with the proper keyword. *) - aac_rewrite H subst 1. + (** 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 keyword together to select the - correct subterm and the correct substitution. *) + + (** 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. + + 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 subterm 1 subst 1. aac_rewrite H. aac_rewrite H'. + aac_rewrite H at 0 subst 1 in_right. aac_reflexivity. Qed. - + End both. - (** We now turn on explaining the distinction between [aac_rewrite] - and [aacu_rewrite]: [aac_rewrite] rejects solutions in which - variables are instantiated by units, the companion tactic, - [aacu_rewrite] allows such solutions. *) + (** *** 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, hence no solutions; *) - aac_instances H. - (** while we get solutions with the "aacu" tactic. *) + (** 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)). + 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. + Abort. + + End dealing_with_units. End base. -(** ** Declaring instances *) +(** *** Declaring instances -(** One can use one's own operations: it suffices to declare them as - instances of our classes. (Note that these instances are already - declared in file [Instances.v].) *) + 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. - - Program Instance nat_plus : Op_AC eq plus O. - Solve All Obligations using firstorder. + + 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. - Program Instance nat_dot : Op_AC eq mult 1. - Solve All Obligations using firstorder. - + 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].) *) - (** Caveat: we need at least an instance of an operator that is AC - and one that is A for a given relation. However, one can reuse an - AC operator as an A operator. *) - Definition default_a := AC_A nat_dot. Existing Instance default_a. End Peano. -(** ** Caveats *) -Section Peano'. - Import Instances.Peano. +(** *** Normalising goals - (** 1. We have a special treatment for units, thus, [S x + x] does not - match [S 0], which is considered as a unit (one) of the mult - operation. *) + We also provide a tactic to normalise terms modulo AC. This + normalisation is the one we use internally. *) - Section caveat_one. - Definition double_plus_one x := 2*x + 1. - Hypothesis H : forall x, S x + x = double_plus_one x. - Goal S O = double_plus_one O. - try aac_rewrite H. (** 0 solutions (normal since it would use 0 to instantiate x) *) - try aacu_rewrite H. (** 0 solutions (abnormal) *) - Abort. - End caveat_one. +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. - (** 2. We cannot at the moment have two classes with the same - units: in the following example, [0] is understood as the unit of - [max] rather than as the unit of [plus]. *) +End AAC_normalise. - Section max. - Program Instance aac_max : Op_AC eq Max.max O := Build_Op_AC _ _ _ Max.max_assoc Max.max_comm. - Variable a : nat. - Goal 0 + a = a. - try aac_reflexivity. - Abort. - End max. -End Peano'. -(** 3. If some computations are possible in the goal or in the -hypothesis, the inference mechanism we use will make the -conversion. However, it seems that in most cases, these conversions -can be done by hand using simpl rather than rewrite. *) -Section Z. - (* The order of the following lines is important in order to get the right scope afterwards. *) - Import ZArith. +(** ** Examples from the web page *) +Section Examples. + + Import Instances.Z. + Require Import ZArith. Open Scope Z_scope. - Opaque Zmult. - - Hypothesis dot_ann_left :forall x, x * 0 = 0. - Hypothesis dot_ann_right :forall x, 0 * x = 0. - Goal forall a, a*0 = 0. - intros. aacu_rewrite dot_ann_left. reflexivity. + (** *** Reverse triangle inequality *) + + 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. - (** Here the tactic fails, since the 0*a is converted to 0, and no - rewrite can occur (even though Zmult is opaque). *) - Goal forall a, 0*a = 0. - intros. try aacu_rewrite dot_ann_left. - Abort. - - (** Here the tactic fails, since the 0*x is converted to 0 in the hypothesis. *) - Goal forall a, a*0 = 0. - intros. try aacu_rewrite dot_ann_right. - Abort. - + + (** *** 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. -End Z. + 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. + |