Library AAC_tactics.Caveats
From Coq Require NArith PeanoNat.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.
Limitations
Dependent parameters
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.
Hypothesis Hf: ∀ n x, f n x + x == x.
Hypothesis Hf': ∀ n, Proper (R ==> R) (f n).
Goal ∀ a b k, a + f k (b+a) + b == a+b.
intros.
Fail aac_rewrite Hf.
Hypothesis Hf': ∀ n, Proper (R ==> R) (f n).
Goal ∀ a b k, a + f k (b+a) + b == a+b.
intros.
Fail aac_rewrite Hf.
aac_rewrite does not instantiate n automatically
of course, this argument can be given explicitly
aac_reflexivity.
Qed.
Qed.
for the same reason, we cannot handle higher-order parameters (here, g)
Hypothesis H : ∀ g x y, g x + g y == g (x + y).
Variable g : X → X.
Hypothesis Hg : Proper (R ==> R) g.
Goal ∀ 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.
Variable g : X → X.
Hypothesis Hg : Proper (R ==> R) g.
Goal ∀ 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.
Exogeneous morphisms
Typically, although N_of_nat is a proper morphism from
@eq nat to @eq N, we cannot rewrite under N_of_nat
Goal ∀ a b: nat, N_of_nat (a+b-(b+a)) = 0%N.
intros.
Fail aac_rewrite Nat.sub_diag.
Abort.
Context {P} {HP : Proper (@eq nat ==> iff) P}.
Hypothesis H : P 0.
Goal ∀ a b, P (a + b - (b + a)).
intros a b.
Fail aac_rewrite Nat.sub_diag.
intros.
Fail aac_rewrite Nat.sub_diag.
Abort.
Context {P} {HP : Proper (@eq nat ==> iff) P}.
Hypothesis H : P 0.
Goal ∀ a b, P (a + b - (b + a)).
intros a b.
Fail aac_rewrite Nat.sub_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 Nat.sub_diag.
reflexivity.
exact H.
Qed.
Goal ∀ a b, a+b-(b+a) = 0 ∧ b-b = 0.
intros.
aac_rewrite Nat.sub_diag.
reflexivity.
exact H.
Qed.
Goal ∀ 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
Treatment of variance with inequations
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: ∀ x, x+x ≤ x.
Goal ∀ a b c, c + - (a + a) + b + b ≤ c.
intros.
this fails because the first solution is not valid (Zopp is not increasing),
on the contrary, the second solution is valid:
Currently, we cannot filter out such invalid solutions in an easy way;
this should be fixed in the future
Caveats
Special treatment for units
ok (no multiplication around), x is instantiated with O
ok (no multiplication around), x is instantiated with 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
More generally, similar counter-intuitive behaviours can appear
when declaring an applied morphism as an unit.
Existential variables
Section evars.
Import ZArith.
Import Instances.Z.
Variable P: Prop.
Hypothesis H: ∀ x y, x+y+x = x → P.
Hypothesis idem: ∀ 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.
symmetry. aac_reflexivity.
this does work but there are remaining evars in the end
this fails since we do not instantiate evars
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 : ∀ 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 : ∀ x, x×f x == x.
Goal f 1 == 1.
Fail aac_rewrite dot_inv_right.
aacu_rewrite dot_inv_right. reflexivity.
Qed.
End U.
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.
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: ∀ 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.
Section W.
Import Instances.Peano.
Variables a b c: nat.
Hypothesis H: 0 = c.
Goal b*(a+a) ≤ b*(c+a+a+1).
Import Instances.Peano.
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)
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.
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: ∀ x, 0 = x - x.
Hypothesis H1: ∀ 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
Abort.
Another example of the former case
Here, only one solution if we use the aac_instance tactic
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.
The 7 last solutions are the same as if we were matching 1
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