wlog and structure variables

Stream: mathlib4

[Filippo A. E. Nuccio]

I am stumbling upon something that looks crazy to me:

import Mathlib.Tactic

variable (A B C D X : Type*) [AddGroup A] [BooleanAlgebra B] [CommRing C] [DivisionRing D]

structure MyStructure (α : Type*) (a b : α) : Prop where
  ne : a ≠ b

def foo (x y : X) (h : x ≠ y): MyStructure X x y := by
  wlog _ : x ≠ y
  · exact ⟨h⟩
  · exact ⟨h⟩

def bar (x y : X) (h : x ≠ y): MyStructure X x y := ⟨h⟩

#check foo -- depends on A, B, C, D, their class instances; and on X, x, y and h
#check bar -- depends on X, x, y and h

Why does the wlog change the variables that bar and foo depend upon?

[Aaron Liu]

It's because you've made them a def

[Aaron Liu]

If you make them a theorem then the proof can't affect the statement

[Aaron Liu]

you can also use wlog _ : _ generalizing var1 var2 var3 (the default is generalize everything)

[Filippo A. E. Nuccio]

This does really answer my question, it's more of a way out... Ah so it has generalised also `A, B, C, D ``, etc...

[Aaron Liu]

so when wlog generalizes over a hypothesis, it adds a dependency

[Aaron Liu]

and this is a way you can restrict it

[Filippo A. E. Nuccio]

Oh great, I see.

[Aaron Liu]

and def brings everything into scope but if something isn't used in the body it's removed from the type of the theorem

[Riccardo Brasca]

This is why you should not use tactics in def.

[Riccardo Brasca]

I mean, because sometimes they do strange things and in defs you really care on what is after the :=

[Aaron Liu]

but with theorem it brings everything into scope when checking the type of the statement, and removes the unused stuff before elaborating the body, so the body can't affect the statement

[Filippo A. E. Nuccio]

Riccardo Brasca said:

This is why you should not use tactics in def.

My point was more to understand what was peculiar about wlog (this does not happen with other tactics), and I really believe that the point is @Aaron Liu 's comment.

[Riccardo Brasca]

Maybe then this is just another reason to hate wlog :sweat_smile:

[Kenny Lau]

More specifically, when Lean is elaborating a def/theorem, it initially assumes that all defined variables are used, and then at the end it automatically kicks out unused variables.

For defs, this happens at the end, and for theorems, this happens after the statement. (I think)

[Filippo A. E. Nuccio]

Oh, nice!

[Filippo A. E. Nuccio]

But at any rate, this behaviour of wlog was unexpected.

[Jireh Loreaux]

I'm actually not sure why this doesn't happen with induction or cases, because it definitely used to be a problem. During porting, before we had the new variable behavior for theorem, this was a continual problem where the types of theorems would be affected by these tactics because they would pull in new variables, and then Lean would decide they were used in the proof and therefore belonged in the statement.