is restate_axiom needed?

Stream: mathlib4

[Edward Ayers]

With respect to getting started with porting I was looking at restate_axiom because it seemed the simplest. But the demonstrative breaking example given in that file doesn't seem to break in Lean 4:

structure A :=
(x : Nat)
(a' : x = 1 := by trivial)

def asdf (z : A) : z.x = 1 := by rw [A.a']

I guess the defeq algorithm has changed slightly in Lean 4?
So maybe restate_axiom isn't needed? Are there any examples in the mathlib3port which would break without restate_axiom?

[Johan Commelin]

cc @Scott Morrison (I think you wrote this, right?)

[Mario Carneiro]

I think it is still useful, because referencing these expressions leads to messy types:

structure A :=
  x : Nat
  a' : x = 1 := by trivial

example (z : A) : z.x = 1 := by
  have := z.a'
  -- z : A
  -- this : autoParam (A.x z = 1) _auto✝
  -- ⊢ A.x z = 1
  exact this

[Edward Ayers]

Ok nice I'll have a go at porting. This might be too radical but maybe lean core could be edited so that structure projection erases autoParam and optParam?

[Leonardo de Moura]

@Edward Ayers Sebastian and I are discussing how to filter this kind of auxiliary annotation. It is not just the projection, there are other places they leak into the local context.

[Edward Ayers]

I've made restate_axiom. Should I delete the corresponding syntax in Mathlib/Mathport/syntax.lean or make my command use that?

[Arthur Paulino]

The former

[Edward Ayers]

https://github.com/leanprover-community/mathlib4/pull/228