apply and term mode unfolding

Stream: lean4

[Yakov Pechersky]

In the following (somewhat minimal) mwe, the last two examples behave unexpectedly for me (at least, based on my lean3 understanding). Why would apply break but refine is fine? Why does the goal in the term mode example display the statement describing an unfolded set Le instead of a plain Le?

class HasMem (α : outParam $ Type u) (β : Type v) where
    mem : α → β → Prop

class PartialOrder (P : Type u) extends HasLessEq P where
  refl (s : P) : s ≤ s
  antisymm (s t : P) : s ≤ t → t ≤ s → s = t
  trans (s t u : P) : s ≤ t → t ≤ u → s ≤ u

theorem HasLessEq.LessEq.trans {P : Type _} [PartialOrder P] {x y z : P} : x ≤ y → y ≤ z → x ≤ z := PartialOrder.trans _ _ _

infix:50 " ∈ " => HasMem.mem

def Set (α : Type u) := α → Prop

namespace Set

instance : HasMem α (Set α) := ⟨λ a s => s a⟩

theorem ext {s t : Set α} (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t :=
  funext $ λ x => propext $ h x

instance : HasLessEq (Set α) := ⟨λ s t => ∀ {x : α}, x ∈ s → x ∈ t⟩

instance : PartialOrder (Set α) where
  refl := λ s x => id
  antisymm := λ s t hst hts => ext $ λ x => ⟨hst, hts⟩
  trans := λ s t u hst htu x hxs => htu $ hst hxs

variable (x y z : Set α) (hxy : x ≤ y) (hyz : y ≤ z)

example : x ≤ z := hxy.trans hyz

example : x ≤ z := by
  refine hxy.trans ?_
  exact hyz

example : x ≤ z := by
  apply hxy.trans -- failed to unify
  admit

example : x ≤ y → y ≤ z → x ≤ z := λ h h' => _ -- goal view has the unfolded `x✝ ∈ x → x✝ ∈ z` instead of `x ≤ y`

[Yakov Pechersky]

The unfolded situation at the bottom example improves when we instead say

instance : HasLessEq (Set α) := ⟨λ s t => ∀ (x : α), x ∈ s → x ∈ t⟩ -- notice the explicit arg

[Yakov Pechersky]

So it seems like it is eagerly expanding the lambda when the lambda has an implicit arg

[Kevin Buzzard]

I'm also seeing this. If instance : HasLessEq (Set α) := ⟨λ s t => ∀ {a : α}, a ∈ s → a ∈ t⟩ with implicit a then goals unfold from x ⊓ y ≤ xto x✝ ∈ x ⊓ y → x✝ ∈ x and then I can't directly apply a theorem saying x ⊓ y ≤ x because I get a typeclass instance problem is stuck error; I have to explicitly tell infLeLeft that I'm talking about Set α. Conversely if I define instance : HasLessEq (Set α) := ⟨λ s t => ∀ (a : α), a ∈ s → a ∈ t⟩ with explicit a then I get extra _s everywhere (but it stops x ⊓ y ≤ x from unfolding).

[Mario Carneiro]

This is what {{a : A}} binders are for

[Yakov Pechersky]

Yes, but are those a thing in lean4?

[Mario Carneiro]

Just checked: no

[Kevin Buzzard]

Yakov just pointed out this from the manual:

Implicit lambdas
In Lean 3 stdlib, we find many instances of the dreadful @+_ idiom. It is often used when we the expected type is a function type with implicit arguments, and we have a constant (reader_t.pure in the example) which also takes implicit arguments. In Lean 4, the elaborator automatically introduces lambdas for consuming implicit arguments. We are still exploring this feature and analyzing its impact, but the experience so far has been very positive. As an example, here is the example in the link above using Lean 4 implicit lambdas.

[Kevin Buzzard]

OK so it's not hard to work around:

def Set α := α → Prop

class HasMem (α : outParam $ Type u) (β : Type v) where
    mem : α → β → Prop

infix:50 " ∈ " => HasMem.mem

instance : HasMem α (Set α) := ⟨λ a s => s a⟩

instance : HasLessEq (Set α) := ⟨λ s t => ∀ {x : α}, x ∈ s → x ∈ t⟩ -- implicit seems best

class HasInf (P : Type u) where
  inf : P → P → P

infix:70 " ⊓ " => HasInf.inf

instance : HasInf (Set α) := ⟨λ s t x => x ∈ s ∧ x ∈ t⟩

theorem infLeLeft {s t : Set α} : s ⊓ t ≤ s := And.left -- introducing implicits works great here
theorem infLeRight {s t : Set α} : s ⊓ t ≤ t := And.right -- introducing implicits works great here

theorem inter_mem_sets_iff (f : Set (Set α)) (hf : ∀ {s t}, s ∈ f → s ≤ t → t ∈ f) :
  x ⊓ y ∈ f → x ∈ f ∧ y ∈ f := by
  refine λ h => ⟨hf h (infLeLeft), -- introducing implicits work great if you finish the job
                 hf h ?h2⟩; -- but here I don't finish the job
  /-
    goal now not x ⊓ y ≤ y, but
    x✝ : α
    ⊢ x✝ ∈ x ⊓ y → x✝ ∈ y
    This surprised me, but now I see it's in the manual.
  -/
  -- apply infLeRight; -- fails to unify
  intro thing; -- to make apply work
  apply infLeRight thing;

[Mario Carneiro]

You can use @ to prevent auto-lambda on goals starting with implicits, but I don't see an easy way to make it work with apply

theorem inter_mem_sets_iff (f : Set (Set α)) (hf : ∀ {s t}, s ∈ f → s ≤ t → t ∈ f) :
  x ⊓ y ∈ f → x ∈ f ∧ y ∈ f := by
  refine λ h => ⟨hf h (infLeLeft), hf h @?h2⟩
  -- goal now x ⊓ y ≤ y
  -- apply infLeRight -- fails to unify
  -- apply @infLeRight -- fails to unify
  refine @infLeRight _ _ _

[Mario Carneiro]

in particular, the fact that apply @infLeRight doesn't work seems like the latest iteration of the apply bug

[Leonardo de Moura]

@Yakov Pechersky @Kevin Buzzard I fixed the two problems that were creating the weird behavior. I was a bug in the apply tactic and the new implicit lambda feature. The examples above are working now.

[Yakov Pechersky]

Thank you for the fixes!