diff options
Diffstat (limited to 'Tutorial.v')
| -rw-r--r-- | Tutorial.v | 321 |
1 files changed, 321 insertions, 0 deletions
diff --git a/Tutorial.v b/Tutorial.v new file mode 100644 index 0000000..84d40fc --- /dev/null +++ b/Tutorial.v @@ -0,0 +1,321 @@ +(***************************************************************************) +(* 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. *) +(***************************************************************************) + +(** * Examples about uses of the aac_rewrite 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: + + Add Rec LoadPath "path_to_aac_tactics". + Add ML Path "path_to_aac_tactics". +*) +Require Export AAC. +Require Instances. + +(** ** Introductory examples *) + +(** 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. *) + +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); + - 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. + +(** ** 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; + however, to be able to use this plugin, one currently needs at least + one associative operator, and one associative-commutative + operator.) *) + +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}. + + 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. + + (** Note: the tactic starts by normalizing 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]). *) + + 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 possible rewriting. 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 + proofgeneral, 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. *) + 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; *) + aac_instances H. + (** we 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. *) + + 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 subterm 1 subst 1. + aac_rewrite H. + aac_rewrite H'. + 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. *) + + 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. *) + 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'. + (** more than 52 with units. *) + aacu_instances H'. + Abort. + + End dealing_with_units. +End base. + +(** ** 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].) *) + +Section Peano. + Require Import Arith. + + Program Instance nat_plus : Op_AC eq plus O. + Solve All Obligations using firstorder. + + Program Instance nat_dot : Op_AC eq mult 1. + Solve All Obligations using firstorder. + + + (** 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. + + (** 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. *) + + 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. + + (** 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]. *) + + 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. + 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. + 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. + + +End Z. + |