Lean shows me the wrong goal?

Stream: general

[Moritz R]

Why does Lean show me the goal bla = bla` and not what i think to have specified?

opaque Calculus : Type u

-- opaque P : Calculus -> Prop
def P (c : Calculus) : Prop := sorry


class BaseSpecification where
  param : Nat





class ExtendedSpecification extends BaseSpecification where
  extra : Nat


def ExtendedSpecification.toCalc (e : ExtendedSpecification) : Calculus := sorry

/-- A base spec is made a calculus by extending it with some arbitrary parameter
      and converting that. -/
def BaseSpecification.toExtendSpecification (e : BaseSpecification) : ExtendedSpecification where
  extra := 0



def BaseSpecification.toCalc (e : BaseSpecification) : Calculus := e.toExtendSpecification.toCalc


-- i originally wanted to use this as a simp lemma, but i think it doesn't prove what i think it does..
-- goal and theorem hover shows `⊢ P e.toCalc ↔ P e.toCalc`
theorem the_problem (e : ExtendedSpecification) :
    P (ExtendedSpecification.toCalc e)
    ↔ P (BaseSpecification.toCalc e.toBaseSpecification) := by
  rfl

If one makes P opaque, then the proof by rfl doesnt go through, but i still get the wrong goal and the wrong theorem.
I wanted to use this theorem for rewriting, but it gets simplified to bla = bla somehow

[Henrik Böving]

toCalc elaborates to your rhs under the hood, there is no difference between the two (when using projections of the parent of a structure that was defined with structure Foo extends Bar implicitly resolving to a chain of projections is the intended behavior). The infoview recovers the goals you can see by looking at elaborated low level expressions (after all not all expressions in a goal are created from syntax but usually directly through meta programs) and trying to guess a syntax that could've produced this low level expression. Because both terms elaborate to the exact same expression it guesses the same resulting expression.

[Henrik Böving]

I guess there is an argument to be made to change the parent projection elaborator to not do this but the goal its showing is at least faithful to what is actually happening^^

[Moritz R]

It is faithful in the sense of showing defeq things, but that really is not faithful

[Henrik Böving]

No this is not about definitional equality, they are syntactically equal at the Expr level

[Moritz R]

oh what

[Henrik Böving]

That's what I was trying to get at, the declaration ExtendedSpecification.toCalc syntactically elaborates to BaseSpecification.toCalc e.toBaseSpecification, there is no difference on the Expr level.

[Moritz R]

Sorry i don't get how lean does this.
If i instead inline the definition i get the goal that i expect

theorem the_problem (e : ExtendedSpecification) :
    P (ExtendedSpecification.toCalc e)
    ↔ P (e.toBaseSpecification.toExtendSpecification.toCalc) := by
  rfl

Why is the goal here different?

[Aaron Liu]

this sounds very suspicious

[Moritz R]

Maybe the difference has to do with parsing of dot notation? Maybe som fun is inserted which makes the terms not elab identically?

[Aaron Liu]

Henrik Böving said:

That's what I was trying to get at, the declaration ExtendedSpecification.toCalc syntactically elaborates to BaseSpecification.toCalc e.toBaseSpecification, there is no difference on the Expr level.

This is false, they are different terms but are pretty printing the same

[Henrik Böving]

Interesting, David recently told me about this behavior and added special support for it in doc-gen because he observed that behavior.

[Aaron Liu]

if you have a : A and a function B.foo and A extends B then B.foo a.toB will pretty print as a.foo

[Aaron Liu]

in this case A.foo also exists and A.foo a also pretty prints as a.foo

[Henrik Böving]

Ah, david told me about a feature very specifically related to projections where this happens

[Henrik Böving]

I had mistakenly assumed without reading enough that toCalc is a projection where this would indeed be true. But here the expression is actually different then. Regardless the root cause for why you see a funny goal remains the same, the delaborator guesses the same syntax.

[Henrik Böving]

structure A where
  x : Nat

structure B extends A where
  y : String


set_option pp.raw true
example (b : B) : b.x = b.toA.x := rfl

this is the specific situation I had in mind (and accidentally pattern matched on to*)

[Moritz R]

Henrik Böving schrieb:

structure A where
  x : Nat

structure B extends A where
  y : String


set_option pp.raw true
example (b : B) : b.x = b.toA.x := rfl

this is the specific situation I had in mind (and accidentally pattern matched on to*)

I think for this situation it makes a lot of sense

[Moritz R]

Aaron Liu schrieb:

if you have a : A and a function B.foo and A extends B then B.foo a.toB will pretty print as a.foo

But i think this is a bit dangerous

[Henrik Böving]

I agree, there is probably some heuristic in the delaborator for dot notation on structures that's messing up to differentiate these situations a bit better. Maybe @Kyle Miller has an idea for what to do here?

[Kyle Miller]

Henrik Böving said:

Interesting, David recently told me about this behavior and added special support for it in doc-gen because he observed that behavior.

Could you point me to this change?

[Henrik Böving]

That was a wrong asessment by me only related to this type of behavior:

structure A where
  x : Nat

structure B extends A where
  y : String


set_option pp.raw true
example (b : B) : b.x = b.toA.x := rfl

the to* functions above are not the ones auto derived for extends but manually written out so my comment doesn't apply.

[Kyle Miller]

What's the pretty printer getting wrong? Both of these are true:

example (e : ExtendedSpecification) : e.toCalc = ExtendedSpecification.toCalc e := rfl
example (e : ExtendedSpecification) : e.toCalc = BaseSpecification.toCalc e.toBaseSpecification := rfl

[Kyle Miller]

By the way, you can use set_option pp.fieldNotation false rather than pp.raw to debug dot notation issues. It's a lot easier to read!

[Kyle Miller]

Certainly for simp purposes it's inconvenient that the pretty printed form isn't reducibly defeq:

example (e : ExtendedSpecification) : e.toCalc = ExtendedSpecification.toCalc e := by
  with_reducible rfl -- succeeds
example (e : ExtendedSpecification) : e.toCalc = BaseSpecification.toCalc e.toBaseSpecification := by
  with_reducible rfl -- fails

[Henrik Böving]

theorem the_problem (e : ExtendedSpecification) :
    P (ExtendedSpecification.toCalc e)
    ↔ P (BaseSpecification.toCalc e.toBaseSpecification) := by
  sorry

in this statement the ExtendedSpecification.toCalc is not necessarily the same as the BaseSpecification.toCalc (they are two different functions that could have different bodies) but if you inspect the pretty printed goal you see P e.toCalc ↔ P e.toCalc. Consider this version where the theorem is not provable:

opaque Calculus : Type u

opaque P (c : Calculus) : Prop

axiom c1 : Calculus
axiom c2 : Calculus

class BaseSpecification where
  param : Nat

class ExtendedSpecification extends BaseSpecification where
  extra : Nat


noncomputable def ExtendedSpecification.toCalc (e : ExtendedSpecification) : Calculus := c1

def BaseSpecification.toExtendSpecification (e : BaseSpecification) : ExtendedSpecification where
  extra := 0

noncomputable def BaseSpecification.toCalc (e : BaseSpecification) : Calculus := c2

theorem the_problem (e : ExtendedSpecification) :
    P (ExtendedSpecification.toCalc e)
    ↔ P (BaseSpecification.toCalc e.toBaseSpecification) := by
  sorry

the goal still reads

e : ExtendedSpecification
⊢ P e.toCalc ↔ P e.toCalc