diff options
Diffstat (limited to 'Caveats.v')
| -rw-r--r-- | Caveats.v | 64 |
1 files changed, 32 insertions, 32 deletions
@@ -35,8 +35,8 @@ Require Instances. Section parameters. - Context {X} {R} {E: @Equivalence X R} - {plus} {plus_A: Associative R plus} {plus_C: Commutative R plus} + 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}. @@ -55,9 +55,9 @@ Section parameters. 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. + Qed. - (** for the same reason, we cannot handle higher-order parameters (here, [g])*) + (** 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. @@ -70,16 +70,16 @@ Section parameters. End parameters. -(** *** 2. Exogeneous morphisms +(** *** 2. Exogeneous morphisms We do not handle `exogeneous' morphisms: morphisms that move from type [T] to some other type [T']. *) Section morphism. - Require Import NArith Minus. + Require Import NArith Minus. Open Scope nat_scope. - (** Typically, although [N_of_nat] is a proper morphism from + (** 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. @@ -111,39 +111,39 @@ Section morphism. 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, + 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. +Section ineq. Require Import ZArith. Import Instances.Z. Open Scope Z_scope. Instance Zplus_incr: Proper (Zle ==> Zle ==> Zle) Zplus. - Proof. intros ? ? H ? ? H'. apply Zplus_le_compat; assumption. Qed. + 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. + 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. +End ineq. @@ -166,23 +166,23 @@ Section Peano. Abort. Goal 1*1 = 1. - (** fails since 1 is seen as a unit, not the application of the + (** fails since 1 is seen as a unit, not the application of the morphism [S] to the constant [O] *) - Fail aacu_rewrite H. + 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'. + 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 + the morphism [S] to the constant [O], it is not recognised as the unit [S O] of multiplication *) - intro. Fail aac_rewrite H'. + intro. Fail aac_rewrite H'. Abort. (** More generally, similar counter-intuitive behaviours can appear @@ -223,7 +223,7 @@ End evars. (** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *) Section U. - Context {X} {R} {E: @Equivalence X R} + 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}. @@ -257,14 +257,14 @@ End U. (** *** 4. Rewriting units *) Section V. - Context {X} {R} {E: @Equivalence X R} + 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, @@ -289,7 +289,7 @@ Section W. 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 @@ -299,8 +299,8 @@ Section W. (** To this end, we provide a companion tactic to [aac_rewrite] and [aacu_rewrite], that makes the transitivity step, but not the - setoid_rewrite: - + 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. @@ -336,18 +336,18 @@ Goal a+b*c = c. Abort. (** **** If the pattern is 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]. + + aac_instances H0 [mult]. (** 1 solution, we miss solutions like [(a+b+c*(1+0*(1+[])))] and so on *) - - aac_instances H1 [mult]. + + aac_instances H1 [mult]. (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*) Abort. @@ -365,7 +365,7 @@ Goal a*a+b*a + c = c. (** There are three 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. + aacu_instances <- H. Abort. |