diff options
Diffstat (limited to 'theories/Caveats.v')
| -rw-r--r-- | theories/Caveats.v | 376 |
1 files changed, 376 insertions, 0 deletions
diff --git a/theories/Caveats.v b/theories/Caveats.v new file mode 100644 index 0000000..d7824cd --- /dev/null +++ b/theories/Caveats.v @@ -0,0 +1,376 @@ +(***************************************************************************) +(* 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. *) +(***************************************************************************) + +(** * Currently known caveats and limitations of the [aac_tactics] library. + + Depending on your installation, either uncomment the following two + lines, or add them to your .coqrc files, replacing "." + with the path to the [aac_tactics] library +*) + +Require NArith Minus. + +From AAC_tactics +Require Import AAC. +From AAC_tactics +Require Instances. + +(** ** Limitations *) + +(** *** 1. Dependent parameters + The type of the rewriting hypothesis must be of the form + + [forall (x_1: T_1) ... (x_n: T_n), R l r], + + where [R] is a relation over some type [T] and such that for all + variable [x_i] appearing in the left-hand side ([l]), we actually + have [T_i]=[T]. The goal should be of the form [S g d], where [S] + is a relation on [T]. + + In other words, we cannot instantiate arguments of an exogeneous + type. *) + +Section parameters. + + Context {X} {R} {E: @Equivalence X R} + {plus} {plus_A: Associative R plus} {plus_C: Commutative R plus} + {plus_Proper: Proper (R ==> R ==> R) plus} + {zero} {Zero: Unit R plus zero}. + + Notation "x == y" := (R x y) (at level 70). + Notation "x + y" := (plus x y) (at level 50, left associativity). + Notation "0" := (zero). + + Variable f: nat -> X -> X. + + (** in [Hf], the parameter [n] has type [nat], it cannot be instantiated automatically *) + Hypothesis Hf: forall n x, f n x + x == x. + Hypothesis Hf': forall n, Proper (R ==> R) (f n). + + Goal forall a b k, a + f k (b+a) + b == a+b. + intros. + Fail aac_rewrite Hf. (** [aac_rewrite] does not instantiate [n] automatically *) + aac_rewrite (Hf k). (** of course, this argument can be given explicitly *) + aac_reflexivity. + Qed. + + (** for the same reason, we cannot handle higher-order parameters (here, [g])*) + Hypothesis H : forall g x y, g x + g y == g (x + y). + Variable g : X -> X. + Hypothesis Hg : Proper (R ==> R) g. + Goal forall a b c, g a + g b + g c == g (a + b + c). + intros. + Fail aac_rewrite H. + do 2 aac_rewrite (H g). aac_reflexivity. + Qed. + +End parameters. + + +(** *** 2. Exogeneous morphisms + + We do not handle `exogeneous' morphisms: morphisms that move from + type [T] to some other type [T']. *) + +Section morphism. + Import NArith Minus. + Open Scope nat_scope. + + (** Typically, although [N_of_nat] is a proper morphism from + [@eq nat] to [@eq N], we cannot rewrite under [N_of_nat] *) + Goal forall a b: nat, N_of_nat (a+b-(b+a)) = 0%N. + intros. + Fail aac_rewrite minus_diag. + Abort. + + + (* More generally, this prevents us from rewriting under + propositional contexts *) + Context {P} {HP : Proper (@eq nat ==> iff) P}. + Hypothesis H : P 0. + + Goal forall a b, P (a + b - (b + a)). + intros a b. + Fail aac_rewrite minus_diag. + (** a solution is to introduce an evar to replace the part to be + rewritten. This tiresome process should be improved in the + future. Here, it can be done using eapply and the morphism. *) + eapply HP. + aac_rewrite minus_diag. + reflexivity. + exact H. + Qed. + + Goal forall a b, a+b-(b+a) = 0 /\ b-b = 0. + intros. + (** similarly, we need to bring equations to the toplevel before + being able to rewrite *) + Fail aac_rewrite minus_diag. + split; aac_rewrite minus_diag; reflexivity. + Qed. + +End morphism. + + +(** *** 3. Treatment of variance with inequations. + + We do not take variance into account when we compute the set of + solutions to a matching problem modulo AC. As a consequence, + [aac_instances] may propose solutions for which [aac_rewrite] will + fail, due to the lack of adequate morphisms *) + +Section ineq. + + Import ZArith. + Import Instances.Z. + Open Scope Z_scope. + + Instance Zplus_incr: Proper (Z.le ==> Z.le ==> Z.le) Zplus. + Proof. intros ? ? H ? ? H'. apply Zplus_le_compat; assumption. Qed. + + Hypothesis H: forall x, x+x <= x. + Goal forall a b c, c + - (a + a) + b + b <= c. + intros. + (** this fails because the first solution is not valid ([Zopp] is not increasing), *) + Fail aac_rewrite H. + aac_instances H. + (** on the contrary, the second solution is valid: *) + aac_rewrite H at 1. + (** Currently, we cannot filter out such invalid solutions in an easy way; + this should be fixed in the future *) + Abort. + +End ineq. + + + +(** ** Caveats *) + +(** *** 1. Special treatment for units. + [S O] is considered as a unit for multiplication whenever a [Peano.mult] + appears in the goal. The downside is that [S x] does not match [1], + and [1] does not match [S(0+0)] whenever [Peano.mult] appears in + the goal. *) + +Section Peano. + Import Instances.Peano. + + Hypothesis H : forall x, x + S x = S (x+x). + + Goal 1 = 1. + (** ok (no multiplication around), [x] is instantiated with [O] *) + aacu_rewrite H. + Abort. + + Goal 1*1 = 1. + (** fails since 1 is seen as a unit, not the application of the + morphism [S] to the constant [O] *) + Fail aacu_rewrite H. + Abort. + + Hypothesis H': forall x, x+1 = 1+x. + + Goal forall a, a+S(0+0) = 1+a. + (** ok (no multiplication around), [x] is instantiated with [a]*) + intro. aac_rewrite H'. + Abort. + + Goal forall a, a*a+S(0+0) = 1+a*a. + (** fails: although [S(0+0)] is understood as the application of + the morphism [S] to the constant [O], it is not recognised + as the unit [S O] of multiplication *) + intro. Fail aac_rewrite H'. + Abort. + + (** More generally, similar counter-intuitive behaviours can appear + when declaring an applied morphism as an unit. *) + +End Peano. + + + +(** *** 2. Existential variables. +We implemented an algorithm for _matching_ modulo AC, not for +_unifying_ modulo AC. As a consequence, existential variables +appearing in a goal are considered as constants, they will not be +instantiated. *) + +Section evars. + Import ZArith. + Import Instances.Z. + + Variable P: Prop. + Hypothesis H: forall x y, x+y+x = x -> P. + Hypothesis idem: forall x, x+x = x. + Goal P. + eapply H. + aac_rewrite idem. (** this works: [x] is instantiated with an evar *) + instantiate (2 := 0). + symmetry. aac_reflexivity. (** this does work but there are remaining evars in the end *) + Abort. + + Hypothesis H': forall x, 3+x = x -> P. + Goal P. + eapply H'. + Fail aac_rewrite idem. (** this fails since we do not instantiate evars *) + Abort. +End evars. + + +(** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *) + +Section U. + Context {X} {R} {E: @Equivalence X R} + {dot} {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot} + {one} {One: Unit R dot one}. + + Infix "==" := R (at level 70). + Infix "*" := dot. + Notation "1" := one. + + (** In some situations, the [aac_rewrite] tactic allows + instantiations of a variable with a unit, when the variable occurs + directly under a function symbol: *) + + Variable f : X -> X. + Hypothesis Hf : Proper (R ==> R) f. + Hypothesis dot_inv_left : forall x, f x*x == x. + Goal f 1 == 1. + aac_rewrite dot_inv_left. reflexivity. + Qed. + + (** This behaviour seems desirable in most situations: these + solutions with units are less peculiar than the other ones, since + the unit comes from the goal. However, this policy is not properly + enforced for now (hard to do with the current algorithm): *) + + Hypothesis dot_inv_right : forall x, x*f x == x. + Goal f 1 == 1. + Fail aac_rewrite dot_inv_right. + aacu_rewrite dot_inv_right. reflexivity. + Qed. + +End U. + +(** *** 4. Rewriting units *) +Section V. + Context {X} {R} {E: @Equivalence X R} + {dot} {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot} + {one} {One: Unit R dot one}. + + Infix "==" := R (at level 70). + Infix "*" := dot. + Notation "1" := one. + + (** [aac_rewrite] uses the symbols appearing in the goal and the + hypothesis to infer the AC and A operations. In the following + example, [dot] appears neither in the left-hand-side of the goal, + nor in the right-hand side of the hypothesis. Hence, 1 is not + recognised as a unit. To circumvent this problem, we can force + [aac_rewrite] to take into account a given operation, by giving + it an extra argument. This extra argument seems useful only in + this peculiar case. *) + + Lemma inv_unique: forall x y y', x*y == 1 -> y'*x == 1 -> y==y'. + Proof. + intros x y y' Hxy Hy'x. + aac_instances <- Hy'x [dot]. + aac_rewrite <- Hy'x at 1 [dot]. + aac_rewrite Hxy. aac_reflexivity. + Qed. +End V. + +(** *** 5. Rewriting too much things. *) +Section W. + Variables a b c: nat. + Hypothesis H: 0 = c. + + Goal b*(a+a) <= b*(c+a+a+1). + + (** [aac_rewrite] finds a pattern modulo AC that matches a given + hypothesis, and then makes a call to [setoid_rewrite]. This + [setoid_rewrite] can unfortunately make several rewrites (in a + non-intuitive way: below, the [1] in the right-hand side is + rewritten into [S c]) *) + aac_rewrite H. + + (** To this end, we provide a companion tactic to [aac_rewrite] + and [aacu_rewrite], that makes the transitivity step, but not the + setoid_rewrite: + + This allows the user to select the relevant occurrences in which + to rewrite. *) + aac_pattern H at 2. setoid_rewrite H at 1. + Abort. + +End W. + +(** *** 6. Rewriting nullifiable patterns. *) +Section Z. + +(** If the pattern of the rewritten hypothesis does not contain "hard" +symbols (like constants, function symbols, AC or A symbols without +units), there can be infinitely many subterms such that the pattern +matches: it is possible to build "subterms" modulo ACU that make the +size of the term increase (by making neutral elements appear in a +layered fashion). Hence, we settled with heuristics to propose only +"some" of these solutions. In such cases, the tactic displays a +(conservative) warning. *) + +Variables a b c: nat. +Variable f: nat -> nat. +Hypothesis H0: forall x, 0 = x - x. +Hypothesis H1: forall x, 1 = x * x. + +Goal a+b*c = c. + aac_instances H0. + (** In this case, only three solutions are proposed, while there are + infinitely many solutions. E.g. + - a+b*c*(1+[]) + - a+b*c*(1+0*(1+ [])) + - ... + *) +Abort. + +(** **** If the pattern is a unit or can be instantiated to be equal + to a unit: + + The heuristic is to make the unit appear at each possible position + in the term, e.g. transforming [a] into [1*a] and [a*1], but this + process is not recursive (we will not transform [1*a]) into + [(1+0*1)*a] *) + +Goal a+b+c = c. + + aac_instances H0 [mult]. + (** 1 solution, we miss solutions like [(a+b+c*(1+0*(1+[])))] and so on *) + + aac_instances H1 [mult]. + (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*) +Abort. + +(** *** Another example of the former case is the following, where the hypothesis can be instantiated to be equal to [1] *) +Hypothesis H : forall x y, (x+y)*x = x*x + y *x. +Goal a*a+b*a + c = c. + (** Here, only one solution if we use the aac_instance tactic *) + aac_instances <- H. + + (** There are 8 solutions using aacu_instances (but, here, + there are infinitely many different solutions). We miss e.g. [a*a +b*a + + (x*x + y*x)*c], which seems to be more peculiar. *) + aacu_instances <- H. + + (** The 7 last solutions are the same as if we were matching [1] *) + aacu_instances H1. Abort. + +(** The behavior of the tactic is not satisfying in this case. It is +still unclear how to handle properly this kind of situation : we plan +to investigate on this in the future *) + +End Z. + |