From 8018e923c75eb5504310864f821972f794b7d554 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Wed, 13 Feb 2019 20:40:51 -0500 Subject: New upstream version 8.8.0+1.gbp069dc3b --- Tutorial.v | 399 ------------------------------------------------------------- 1 file changed, 399 deletions(-) delete mode 100644 Tutorial.v (limited to 'Tutorial.v') diff --git a/Tutorial.v b/Tutorial.v deleted file mode 100644 index 76006ca..0000000 --- a/Tutorial.v +++ /dev/null @@ -1,399 +0,0 @@ -(***************************************************************************) -(* 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. *) - -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. - *) - -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. - 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, *) - 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. - 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. - - - - -(** ** Examples from the web page *) -Section Examples. - - Import Instances.Z. - Require Import ZArith. - Open Scope Z_scope. - - (** *** 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. - - - (** *** 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. - - -- cgit v1.2.3