reducible defeq and rewrites

Stream: lean4

[Jireh Loreaux]

I just found out that my mental model of how rw works with definitional equality is broken. I expected the following to fail because X is not reducibly defeq to Nat, and so I thought Nat.mul_comm wouldn't fire with rw. But it does!

def X := Nat

instance : Mul X := inferInstanceAs (Mul Nat)

example (x y : X) : x * y = y * x := by rw [Nat.mul_comm] -- works! why?

Can someone explain what I'm missing here?

[Adam Topaz]

I assume it's because x * y is notation for Nat.mul x y.

[Jireh Loreaux]

I don't follow.

[Adam Topaz]

ok, I don't know the details of how rw actually works, but my guess is that in this case it works because the match of the lhs of the goal with Nat.mul ? ? succeeds

[Adam Topaz]

again, just a guess

[Damiano Testa]

You could try with X := ℝ . :shrug:

[Adam Topaz]

Still works for what I assume are similar reasons:

import Mathlib.Tactic

def X := ℝ

instance : Mul X := inferInstanceAs (Mul ℝ)


lemma Real.mul_comm (x y : ℝ) : x * y = y * x := by ring

example (x y : X) : x * y = y * x := by rw [Real.mul_comm]

[Jireh Loreaux]

This also works:

import Mathlib

def X := ℝ

instance : Mul X := inferInstanceAs (Mul ℝ)

example (x y : X) : x * y = y * x := by rw [mul_comm (G := ℝ)] -- works! why?

[Matthew Ballard]

I thought rw operated at default

[Adam Topaz]

yeah that's right.

[Jireh Loreaux]

Surely this wasn't the case in Lean 3, though?

[Matthew Ballard]

I thought everything was at default/semireducible there (says the person who used it very little)

[Kevin Buzzard]

Yeah I am also surprised by this. I thought that the whole point of def was not to let this stuff leak through so how can it leak through?

[Jireh Loreaux]

I mean, it makes sense if rw works at default transparency, I just didn't think that was the case. I'm fairly confident it didn't in Lean 3, but perhaps that changed.

[Kyle Miller]

Implicit arguments switch to a higher transparency setting, but I don't remember the exact details

[Jireh Loreaux]

@Kyle Miller the first example works even if you write by rw [Nat.mul_comm x y]

[Kyle Miller]

Sure, but that makes sense if implicit arguments use a higher transparency setting:

[Kyle Miller]

example (x y : X) : type_of% (Nat.mul_comm x y) = (x * y = y * x) := by with_reducible rfl

[Eric Wieser]

What breaks if this behavior is disabled?

[Eric Wieser]

If a heuristic of some kind is still needed, perhaps adapting the rule to not change reducibility of Sorts would work?

[Jovan Gerbscheid]

The reducibility can be controlled using Rewrite.Config:

structure Config where
  transparency : TransparencyMode := TransparencyMode.reducible
  offsetCnstrs : Bool := true
  occs : Occurrences := Occurrences.all

Setting it can be done with this syntax: rw (config := {transparency := .all}). As you can see the default setting is reducible.

[Eric Wieser]

Jovan, as alluded to above, the default is using a more lenient interpretation of reducIbility than reducible is supposed to mean.

[Eric Wieser]

Which is to say; I think that setting is only partially respected

[Jovan Gerbscheid]

Eric Wieser said:

If a heuristic of some kind is still needed, perhaps adapting the rule to not change reducibility of Sorts would work?

Looking at it from a DiscrTree perspective, I think you want unification with the lookup results to work in the reducible transparency. DiscrTree does not index instance arguments, and does not index implicit arguments if they do not satisfy isType. For the not indexed terms I think you do want to change the transparency. But not changing the transparency in the case of implicit type arguments seems alright.

[Eric Wieser]

Does rw not currently use discrtrees?

[Jovan Gerbscheid]

No, I thought you were suggesting to change the behaviour of isDefEq. And isDefEq is used in combination with DiscrTree for example in simp.

[Jovan Gerbscheid]

Because in the above example isDefEq is what changes the transparency setting for implicit arguments.

[Jovan Gerbscheid]

rw?? also uses discrimination trees, but in that case it is my RefinedDiscrTree instead of lean's DiscrTree.

rw uses a more light weight form of "indexing" (in the function kabstract): it uses Expr.toHeadIndex and Expr.headNumArgs to find the head and number of arguments of each subexpression. And only if those match, will it try the more expensive isDefEq check.