# Library AAC_tactics.Caveats

# Currently known limitations and caveats of AAC Tactics

From Stdlib Require NArith PeanoNat.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.

## Limitations

### Dependent parameters

The type of the rewriting hypothesis must be of the form
∀ (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, since the parameter n has type nat, it cannot be instantiated automatically
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.
aac_rewrite does not instantiate n automatically
Fail aac_rewrite Hf.
of course, this argument can be given explicitly
aac_rewrite (Hf k).
aac_reflexivity.
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.

### Exogeneous morphisms

We do not handle "exogeneous" morphisms: morphisms that move from type `T` to some other type `T'`.
Section morphism.
Import NArith PeanoNat.
Import Instances.N Instances.Peano.
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 ∀ a b: nat, N_of_nat (a+b-(b+a)) = 0%N.
intros.
Fail aac_rewrite Nat.sub_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 ∀ 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.
similarly, we need to bring equations to the toplevel before being able to rewrite
Fail aac_rewrite Nat.sub_diag.
split; aac_rewrite Nat.sub_diag; reflexivity.
Qed.
End morphism.

### 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.
#[local] Instance Z_add_incr: Proper (Z.le ==> Z.le ==> Z.le) Z.add.
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 (Z.opp 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

### Special treatment for units

S 0 is considered as a unit for multiplication whenever a Nat.mul appears in the goal. The downside is that S x does not match 1, and 1 does not match S (0 + 0) whenever Nat.mul appears in the goal.
Section Peano.
Import Instances.Peano.
Hypothesis H : ∀ 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': ∀ x, x + 1 = 1 + x.
Goal ∀ a, a + S (0+0) = 1 + a.
OK (no multiplication around), x is instantiated with a
intro. aac_rewrite H'.
Abort.
Goal ∀ 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 a unit
End Peano.

### 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 and will not be instantiated.
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.
this works: x is instantiated with an evar
aac_rewrite idem.
instantiate (2 := 0).
this does work but there are remaining evars in the end
symmetry. aac_reflexivity.
Abort.
Hypothesis H': ∀ x, 3+x = x → P.
Goal P.
eapply H'.
this fails since we do not instantiate evars
Fail aac_rewrite idem.
Abort.
End evars.

### 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 : ∀ 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.

### 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: ∀ 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.

### Rewriting too many things

Section W.
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)
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.

### Rewriting nullifiable patterns

Section Z.
Import Instances.Peano.
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, for example:

- 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

In the following, the hypothesis can be instantiated to be equal to 1.
Hypothesis H : ∀ 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 this in the future.
End Z.