Stream: Coq users

Topic: Rewrite with equal parameters of phantom type

William Spencer (Mar 02 2024 at 18:03):

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.

1. Is there such a tactic already? I couldn't find one, but also have no idea what search terms would work.
2. In trying to write an Ltac to do this, I found myself wanting to generate patterns in an Ltac. Is this possible, and how?
3. 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!

Meven Lennon-Bertrand (Mar 04 2024 at 16:14):

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

Li-yao (Mar 05 2024 at 18:09):

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: Oct 13 2024 at 01:02 UTC