overwriting fields

Stream: mathlib4

[Matthew Ballard]

In the example

structure A where
  x : Nat
  y : Nat

structure B extends A where
  z : Nat

def a : A := {x := 0, y := 0}

def b : B := {a with x :=0, z := 0}

Lean builds b as B.mk (A.mk 0 a.y) 0 which is less efficient than B.mk a 0 and forces unification to open up A.mk for defeq checks in cases where it could have figured out a is defeq to the RHS and not unfolded.

[Matthew Ballard]

I built a list of all files where such collisions occur #6965. Not all are as useless at x := 0 above.

[Matthew Ballard]

The end goal here is to try to stamp out the useless ones.

But right now the branch is only useful for the list itself unless you are on Apple Silicon since that is the only architecture the toolchain is built for.

[Matthew Ballard]

The toolchain just writes to stdout the list of fields specified and the module we are in at that moment.

[Matthew Ballard]

Unsurprisingly Lean CI does not like this so I only built the minimal amount I needed to. I can try to build some more if anyone wants to directly use the toolchain.

[Matthew Ballard]

Please feel encouraged to tell me I am doing it wrong (it only took ~10 lines this way) and to suggest things.

[Matthew Ballard]

Here is the generated list if you just want to look at that. Each line is a single instance with collisions.

[Matthew Ballard]

One disadvantage of my hacky method was that I didn’t know how to find the declaration name to which the term syntax I was elaborating belonged to

[Thomas Murrills]

Interesting! Am I right in thinking that the list linked above shows all potential field collisions, not just collisions where the overwriting field is actually defeq to the overwritten one (e.g. it would also flag { a with x := 1, z := 0 })? (I looked for an isDefEq check in the lean4 commits but couldn’t find one; did I miss it?)

[Matthew Ballard]

Checking isDefEq would probably cut it down more. But I would guess not much. Some times they are defeq but syntactically distinct. Feel free to prove me wrong!

[Thomas Murrills]

Gotcha! and just to be clear, you’re not saying that anything’s inefficient in how the case

def a : A := {x := 0, y := 0}

def b : B := {a with x := 1, z := 0}

is handled, right? This is only about the case where b.toA is actually the same as a up to unfolding?

[Matthew Ballard]

I just took a very coarse criteria because it was simplest to implement.