I'm working with a matrix (phantom) type

```
Definition Matrix (n m : nat) := nat -> nat -> C.
```

This makes it awkward to use a number of rewrite lemmas: often, the dimensions will not definitionally match, despite being equal (a * b vs b * a, say). As these are not true dependent types, this can be be resolved by replacing the appropriate dimensions, but it makes for unreadable (and fragile) proofs with lots of `replace (a*b) with (b*a) by lia`

or even worse `assert (H: a*b=b*a) by lia; rewrite H at 1 4 5; clear H`

to get Coq to unify the dimensions given in lemmas with the goal.

On a per-lemma basis, this is not so hard to resolve: you can write a tactic that matches the goal against a generic form of the statement of the lemma and assert each of the equalities. For example:

```
Lemma kron_comm_mul_inv_mat_equiv : forall p q : nat,
@mat_equiv (p*q) (p*q)
(@Mmult (p*q) (p*q) (p*q)
(kron_comm p q) (kron_comm q p)) (Matrix.I (p*q)).
(* Hard to use, often one of the `p*q`'s will be a `q*p`. This rewrites effectively: *)
Ltac rewrite_kron_comm_lem :=
match goal with
|- context[@Mmult ?n ?m ?o (kron_comm ?t' ?s') (kron_comm ?s'' ?t'')] =>
(* idtac n m o t' s' s'' t''; *)
replace s'' with s' by lia; replace t'' with t' by lia;
replace n with (t'*s')%nat by lia; replace m with (t'*s')%nat by lia;
replace o with (t'*s')%nat by lia;
replace (@Mmult n m o (kron_comm t' s') (kron_comm s' t'))
with (@Mmult (t'*s') (t'*s') (t'*s') (kron_comm t' s') (kron_comm s' t'))
by (f_equal;lia);
rewrite (kron_comm_mul_inv_mat_equiv t' s')
end.
```

(This has not been prepared to also work in hypotheses, nor have I checked it closely, but to illustrate the point.)

This is *a* solution, but not really effective. What I would like is some sort of "strong rewrite" tactic that performs some version of this on its own. I have not had success writing it, though. I am quite happy to use Ltac, and willing to learn another tool (Ltac2, ML, etc.) if that is necessary, but would appreciate some guidance on the issue.

- Is there such a tactic already? I couldn't find one, but also have no idea what search terms would work.
- In trying to write an Ltac to do this, I found myself wanting to generate patterns in an Ltac. Is this possible, and how?
- Is there another tool with capabilities that would enable me to do this without
*too*much work? (i.e. not reimplementing matching, for example) If so, what is a good resource to learn that tool?

Thanks for any advice - apologies for the rather open-ended question(s), and let me know if there's anything I can clarify!

Does the tactic applys_eq here do something like what you'd like?

Another idea is to reformulate the lemma with more variables, so that `rewrite`

is more likely to match in the first place, generating equality obligations instead:

```
forall p q pq1 pq2 pq3 pq4,
pq1 = p * q -> pq2 = p * q -> pq3 = p * q -> pq4 = p * q ->
@mat_equiv (p*q) (p*q)
(@Mmul pq1 pq2 pq3 (...) (...)) (Matrix.I pq4)
```

Last updated: Jun 23 2024 at 04:03 UTC