dependent rewrite tactic

Stream: metaprogramming / tactics

[Aaron Liu]

I wrote a dependent rewrite tactic. This is the first time I've written a tactic, so I'd like some feedback.
DepRewrite.lean, last updated 2025-02-22T23:32:40-05:00

[Kyle Miller]

Could you say a bit about what it does and what sorts of examples it can handle?

[Aaron Liu]

I built this by modifying the rw tactic, so it should be able to do anything that rw can do. I tried it with

example {α : Sort u} {β : α → Sort v} {a a' : α} (h : a = a') (b : β a)
    {γ : (a : α) → β a → Sort w} (r : (a : α) → β a → β a) (c : γ a (r a b)) :
    Eq.rec (motive := fun x h ↦ γ x (h ▸ r a b)) c h =
    Eq.rec
      (motive := fun x (h' : a' = x) ↦ γ a' (h' ▸ r x ((h'.symm ▸ h) ▸ b)))
      (Eq.rec (motive := fun x h ↦ γ x (r x (h ▸ b))) c h) h.symm := by
  -- rw! [h] works

  -- conv => also works
  --   congr
  --   · rw! [h]
  --   · rw! [h]

[Aaron Liu]

The tactic is meant to do the same as rw, but insert casts so that the motive does not become type incorrect.

[Aaron Liu]

The version of my tactic that I posted here leaks free variables when operating on let expressions. I have updated it to not do that. If anyone wants the updated version then feel free to ping me.

[Kyle Miller]

I had a vague idea of a project in this area that you might be interested in looking into.

Unconstrained rewrites are not great to work with, which is a reason that rw and simp don't insert casts just to make a rewrite go through (that's to say, it can lead you deeper into "DTT hell"). However, sometimes there is a "good" cast function available. There might be a way where we can synthesize a good cast with these. For example, docs#Fin.cast could be used when the discrepancy appears inside the Nat argument to Fin inside the type of the term that needs rewriting.

Unconstrained casts are always there as a fallback, but we could have an option that enables the fallback. We can also allow unconstrained casts in certain situations indiscriminately, for example if the value is a proof. That's what simp does already. There are other strategies too to consider.

[Kyle Miller]

Independently of this, you might also look into modifying your rw! to make use of simp's congruence lemma system when rewriting applications. There is not much example code, but the conv-mode arg tactic uses it in a custom way. The idea being that you can ask for a lemma with CongrArgKind.cast arguments, and the generator will handle building up a relatively efficient congruence lemma for you for the entire application, rather than just rewriting individual Expr.app nodes.

It might not be necessary to do, but it would be a reasonable thing to look into to learn this part of metaprogramming.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kyle Miller said:

I had a vague idea of a project in this area that you might be interested in looking into.

Unconstrained rewrites are not great to work with, which is a reason that rw and simp don't insert casts just to make a rewrite go through (that's to say, it can lead you deeper into "DTT hell"). However, sometimes there is a "good" cast function available. There might be a way where we can synthesize a good cast with these. For example, docs#Fin.cast could be used when the discrepancy appears inside the Nat argument to Fin inside the type of the term that needs rewriting.

Unconstrained casts are always there as a fallback, but we could have an option that enables the fallback. We can also allow unconstrained casts in certain situations indiscriminately, for example if the value is a proof. That's what simp does already. There are other strategies too to consider.

I am wondering what exactly you mean by a "good" cast". My working characterization atm is that these are casts along an equality of indices of a type family, where the indices are not themselves types. So e.g. cast (h : n = m) (motive := Fin) (v : Fin n) is good, but cast (h : Nat = Nat') (motive := λ(α: Type) => α) (n : Nat) (rewriting along an equality of types) is bad, and cast (h : Nat = Nat') (motive := λα. List α) (l : List Nat) is also bad. Mathlib tends to introduce definitions for the "good" casts, though one could as well just use Eq.rec with a "good" motive.

[Kyle Miller]

By "good" cast, I was meaning some registered casting function, but I think you're right about this characterization. The difference though between a registered casting function and Eq.rec with a "good" motive is that the registered casting function will have a library around it with algebraic rules , where Eq.rec tends to be less amenable to rw-based reasoning.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

We can also allow unconstrained casts in certain situations indiscriminately, for example if the value is a proof. That's what simp does already.

Why is my question here not a counterexample to this? The thing you need to do is exactly to rewrite in a proof's type, but simp doesn't seem to be doing this.

[Kyle Miller]

simp can't rewrite in that position.

The signature of homMk is

homMk {X : C} (U V : Over X) (f : Hom U.left V.left) (w : _root_.comp f V.hom = U.hom) : OverHom U V

and the rewrite you want to do involves needing to rewrite U. However, f depends on U, so it's fixed. It also appears in the resulting type OverHom U V, so it's fixed for that reason as well (simp can't rewrite something to have a different type).

[Joachim Breitner]

And you are saying it would be in principle possible to do the rewriting of the U argument by putting casts around the next argument and the results, but that it would lead to basically impossible to work with terms, with casts all over the place. It would also possibly start to loop, since U is mentioned in the type of the casts, if one isn't careful, I assume.

[Kyle Miller]

Yeah, that looping issue is a problem too.

I forgot to mention that sometimes the "good" casts are good not just because they're canonical. They have good defeq properties:

example (n m : Nat) (h : n = m) (a : Fin n) : a.1 = (h ▸ a : Fin m).1 := rfl -- fails
example (n m : Nat) (h : n = m) (a : Fin n) : a.1 = (Fin.cast h a).1 := rfl -- succeeds

The custom cast is able to drop the rewrite down inside the proof field of Fin.

[Jovan Gerbscheid]

Here is a minimized example of what problem I ran into in lean4#7181:

import Mathlib

axiom foo (a : Nat) : Subring Int

class IsFunnyRing (α : Type) : Prop where
instance (n : Nat) : IsFunnyRing (foo n) where

-- Adding this instance makes the rewrite break:
-- instance : IsFunnyRing (foo 3) where

axiom bar (α : Type) [Ring α] [IsFunnyRing α] : String

example : bar (foo 3) = "hello" := by
  rw [show 3 = 2+1 from rfl]

If this dependent rewrite tactic can solve this problem then that would be amazing. It only needs to insert a cast around a proof.

See also the conversation here

[Jovan Gerbscheid]

It seems that it can :tada:
It replaces the instance with the somewhat scary looking

(fun {α} a motive refl => refl) 3 (fun x h => IsFunnyRing ↥(foo x))
  ((fun {α} a motive refl => refl) (2 + 1) (fun x' h' => IsFunnyRing ↥(foo 3))
    instIsFunnyRingSubtypeIntMemSubringFooOfNatNat)

[Joachim Breitner]

I agree that better rewriting tactics are a worthwhile direction to explore

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I certainly agree! I took Aaron's code posted above, added a couple of features, and deployed it in a project I am working on: commit. While it doesn't solve all my DTT problems, it helps with many of them; in the commit, results that could only be established via careful generalize sequences are now just rw!. See also tests for what the tactic can do. I am wondering if there is interest in including this in mathlib.

it would be in principle possible to do the rewriting of the U argument by putting casts around the next argument and the results, but that it would lead to basically impossible to work with terms, with casts all over the place

This is not really true. The point is that in some cases (including the Over example) you only have to cast proofs. Casting these causes no increase in complexity because we don't care about proof terms anyway. As one addition to Aaron's code, I added a configuration option for what kinds of casts can be inserted. The default mode only casts proof terms.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kyle Miller said:

simp can't rewrite in that position.

The signature of homMk is

homMk {X : C} (U V : Over X) (f : Hom U.left V.left) (w : _root_.comp f V.hom = U.hom) : OverHom U V

and the rewrite you want to do involves needing to rewrite U. However, f depends on U, so it's fixed. It also appears in the resulting type OverHom U V, so it's fixed for that reason as well (simp can't rewrite something to have a different type).

Right, so it depends on how you interpret 'allow unconstrained casts if the value is a proof'; in my interpretation (allow it even if this changes the proof's type), there are examples that rw! can handle but simp and rw cannot.

[Aaron Liu]

(deleted)