let overload

Stream: lean4

[Chris B]

There's something about this combination of let-shadowing and typeclass resolution that Lean seems to be rejecting, though it's very close (nightly 7-14). Some other testing confirms that this sort of shadowing works with almost any other combination of elements. If the element being returned by if/else doesn't reference p, this works fine. Is this a bridge too far? For clarity, the expectation is that p := Point 1 0 in the if-then-else.

structure Point where
x : Nat
y : Nat

def Point.compute (p : Point) : Point :=
  let p := { p with x := 1 }
  let p := { p with y := 0 }
  if (p.x - p.y) > p.x then p else p

/-
(kernel) declaration has metavariables 'Point.compute'

synthesized type class instance type is not definitionally equal to expected type, synthesized
  Nat.decLt p.x (p.x - p.y)
has type
  Decidable (p.x < p.x - p.y)
expected
  let p : ?m.1960 p✝¹ := ?m.1988 p✝¹;
  let p : Point := ?m.1990 p✝¹ p;
  Decidable (p.x - p.y > p.x)
-/

[Chris B]

Maybe this variation is more interesting since it's even closer:

def Point.compute (p : Point) : Point :=
  let p := { p with x := 1 }
  let p := { p with y := 0 }
  if (p.x - p.y) <= p.x then p else p

/-
synthesized type class instance type is not definitionally equal to expected type, synthesized
  Nat.decLe (p.x - p.y) p.x
has type
  Decidable (p.x - p.y ≤ p.x)
expected
  let p : ?m.1955 p✝¹ := ?m.1983 p✝¹;
  let p : Point := ?m.1985 p✝¹ p;
  Decidable (p.x - p.y ≤ p.x)
-/

[David Renshaw]

This works:

def Point.compute (p : Point) : Point :=
  let p := { p with x := 1 }
  let p : Point := { p with y := 0 }
  if (p.x - p.y) ≤ p.x then p else p

[Kevin Buzzard]

Is all this fixed if you don't over-use p? It's hard to have sympathy with someone who uses p to mean three different things and then something with p in doesn't work

[Gabriel Ebner]

The shadowing is a red herring, this fails as well:

structure Point where
  x : Nat
  y : Nat

def Point.compute (p : Point) : Point :=
  let q := { p with x := 1 }
  let r := { q with y := 0 }
  if (r.x - r.y) > r.x then r else r

[Kevin Buzzard]

Oh ok!

[Chris B]

Those are both interesting examples, thanks. I guess anything that doesn't make the Point constructor explicit at least once doesn't given enough information about the metavariables.

-- fails
def Point.compute (p : Point) : Point :=
  let q := { p with x := 1 }
  let r := ⟨q.x, 0⟩
  if (r.x - r.y) > r.x then r else r

-- succeeds
def Point.compute (p : Point) : Point :=
  let q := { p with x := 1 }
  let r := Point.mk q.x 0
  if (r.x - r.y) > r.x then r else r

-- succeeds
def Point.compute (p : Point) : Point :=
  let q := Point.mk 1 p.y
  let r := { q with x := 0 }
  if (r.x - r.y) > r.x then r else r

[Mario Carneiro]

doesn't { p with x := 1 } get the type Point because p : Point?

[Chris B]

One would have thought. It's also interesting that the error text suggests that Lean wasn't able to figure out the metavariables, but hovering over each let binding says q and r are unambiguously of type Point.

[Kyle Miller]

@Mario Carneiro Interesting, looks like no:

structure Point2D where
  (x y : Nat)
structure Point3D where
  (x y z : Nat)

def p : Point2D := ⟨1, 2⟩
def q : Point3D := {p with z := 3}

[Chris B]

Whoah how does that work

[Mario Carneiro]

Same as in lean 3 I would guess

[Mario Carneiro]

still, it should use the original type as a hint if it doesn't have more explicit typing like this

[Kyle Miller]

I'm on an old version of Lean 4, but this is what #print q shows for me:

def q : Point3D :=
let src : Point2D := p;
{ x := src.x, y := src.y, z := 3 }

[Mario Carneiro]

it uses the names of the fields to line things up

[Mario Carneiro]

in mathlib we do this a lot to transfer things between old structures

[Kyle Miller]

Does with subsume the ... syntax?

[Mario Carneiro]

no, it's the other way around

[Mario Carneiro]

..s can have multiple, s with can't

[Kyle Miller]

Oh, I meant "does with replace .. in Lean 4" (even if it doesn't do exactly the same thing)

[Mario Carneiro]

I'm not really sure why the devs didn't go for it but I'm going to have to write it myself in mathlib4 if not

[Mario Carneiro]

Note that lean 3 structinst has both s with and ..s

[Mario Carneiro]

but mathlib style uses only ..s

[Mario Carneiro]

the ..s was a late lean 3 addition

[Chris B]

That's pretty neat, I didn't know you could do that transfer thing. What do you mean by '.. can have multiple'?

[Mario Carneiro]

def foo (a : A) (b : B) (c : C) : D := { a with d := 1, ..b, ..c }

[Chris B]

Oh I see, thanks.

[Mario Carneiro]

here D has fields a,b,c,d and A,B,C have one field each

[Mario Carneiro]

In lean 3 the ..s have to go at the end, although I'm not really sure why that syntactic restriction exists

[Mario Carneiro]

I think it has something to do with the order in which fields are replaced

[Mario Carneiro]

lean 4 finishes parsing before starting elaboration so I think that wouldn't be an issue

[Mario Carneiro]

Personally, I think that a with should be restricted to non-type-changing struct update and leave that for the splay args

[Mario Carneiro]

the restriction to only one with argument makes more sense in that context

[Kyle Miller]

There's other syntax available for specifying the type of a "structure instance":

structure Point where
x : Nat
y : Nat

def Point.compute (p : Point) : Point :=
  let p := { p with x := 1 : Point }
  let p := { p with y := 0 : Point }
  if (p.x - p.y) > p.x then p else p

Found this by reading through https://github.com/leanprover/lean4/blob/7dc3e72bcb079f552fdce5aa5657ace9857283e2/stage0/src/Lean/Elab/StructInst.lean

[Kyle Miller]

I also found that you can put .. in a structure instance:{ p with y := 0 .. } or { p with y := 0 .. : Point }. I wasn't able to figure out whether .. did anything, though.

[Kyle Miller]

Oh, .. is supposed to indicate that the remaining fields of the struct are implicit -- the "invalid structure instance with and .. cannot be used together" error message suggests these shouldn't be allowed.

[Mario Carneiro]

The .. argument in structinst means the same in lean 4 as it does in lean 3 (yes, you can do { a := 1, .. })

[Mario Carneiro]

it puts := _ on all remaining unfilled fields

[Mario Carneiro]

which is usually an error, but is especially useful in tactic proofs with refine

[Mario Carneiro]

Kyle Miller said:

the "invalid structure instance with and .. cannot be used together" error message suggests these shouldn't be allowed.

This error message also makes me think that the devs are only considering the same-type use case for s with, because that error message doesn't make sense if you have { (s:Point2D) with .. : Point3D }

[Sebastian Ullrich]

Yes, the Lean 4 structure notation is simpler than the Lean 3 one, which frankly was too complicated to really make robust and maintainable (guess who wrote it :grimacing: ). And it does use the "source" type when the expected type is unavailable, which its simpler, non-nominal semantics allow it to do: https://github.com/leanprover/lean4/blob/7dc3e72bcb079f552fdce5aa5657ace9857283e2/stage0/src/Lean/Elab/StructInst.lean#L169-L170

[Mario Carneiro]

Do you know why it isn't working here then?

[Sebastian Ullrich]

I think it is also a better fit for the "new-style structures" (the only kind of structures in Lean 4): you can set entire subobjects with { z := ..., toPoint2D := ... }. Having said that, if someone wrote an extended structure command to simulate diamond inheritance, it might also make sense to write an extended structure instance notation that allows multiple, overlapping sources like in Lean 3.

[Mario Carneiro]

I've opened an issue for this at dselsam/mathport#9 . That's going to be a requirement for the port

[Mario Carneiro]

That said, it's not clear to me to what extent it's possible to actually override all this structure stuff in userland

[Mario Carneiro]

I also opened a bunch of issues at https://github.com/dselsam/mathport/issues to track features of lean 3 that have no obvious analogues in lean 4, which are starting to become more immediate issues as the porting tool matures. Some of this stuff can be implemented in userland (and I encourage anyone who wants to take a shot at them to do so in mathlib4)

[Sebastian Ullrich]

Mario Carneiro said:

Do you know why it isn't working here then?

It's a more general elaboration order issue I believe. The structure notations are visited first, but are then postponed because the expected type is not available yet. This is correct even if the source type is available since, as @Kyle Miller showed, the two do not have to be equal. So in order to be deterministic, we should always inspect the expected type first.
This postponing creates synthetic metavariables, which typeclass inference later chokes on as shown in the error message. Now the actual issue, I believe, is that this error is considered fatal instead of postponing typeclass inference as well until those metavariables are solved. Thus elaboration fails.

[Mario Carneiro]

Do you have any opinion on removing the type changing / nominal typing behavior of s with? As you point out, lean 4's structures are trying to stick to compositional inheritance, which means that you should be able to use { toPoint2D := p, z := ... } when extending a structure and reject Kyle's example (where Point2D is not a parent of Point3D)

[Sebastian Ullrich]

Mmh, I would be open to it at least. What would be the advantage, purely to simplify elaboration ordering?

[Mario Carneiro]

I don't like that it's currently half-assed nominal typing. It should either allow multiple with args or not do the splay thing

[Mario Carneiro]

I think, if you take that part out, structure inheritance shouldn't be anything more than composition, except for the fact that you can use field := ... instead of toParent.field := ... in structure instances (and even this seems a little borderline from a rust perspective)

[Mario Carneiro]

maybe I'm just arguing against extends altogether :upside_down:

[Mario Carneiro]

well, I'm no stakeholder here since I fully intend to replace it with a full nominal typing structure extension in mathlib, so limitations of lean 4 core structures aren't likely to be an issue for me

[Kyle Miller]

How complicated would it be to change structure instances so that there are splays? Sorry if this has been discussed before -- I'm just curious about the difficulties.

"{" >> optional (atomic (termParser >> " with "))
          >> manyIndent (group ((structInstFieldAbbrev <|> structInstField <|> structInstSplay) >> optional ", "))
          >> optEllipsis
          >> optional (" : " >> termParser)
          >> " }"

def structInstSplay := ".." >> termParser

Then {s with foo} could mean "update s, don't change the type" and {..s} could effectively be the nominally typed version.

Also optEllipsis could probably be rolled into structInstSplay, and an empty splay would mean "insert holes for the remaining fields".

[Gabriel Ebner]

https://github.com/leanprover-community/mathlib4/blob/1fd1cdc64b9a968e302ebd34af228b40cc05eb04/Mathlib/Tactic/Spread.lean

[Gabriel Ebner]

This adds support for structure instance spread syntax.

instance : Foo α where
  __ := instSomething -- include fields from `instSomething`

example : Foo α := {
  __ := instSomething -- include fields from `instSomething`
}

[Mac]

(deleted -- wrong thread)