# Zulip Chat Archive

## Stream: lean4

### Topic: apply and term mode unfolding

#### Yakov Pechersky (Mar 24 2021 at 14:54):

In the following (somewhat minimal) mwe, the last two `example`

s 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 (Mar 24 2021 at 16:05):

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 (Mar 24 2021 at 16:06):

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

#### Kevin Buzzard (Mar 25 2021 at 21:02):

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 ≤ x`

to `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 (Mar 25 2021 at 21:07):

This is what `{{a : A}}`

binders are for

#### Yakov Pechersky (Mar 25 2021 at 21:09):

Yes, but are those a thing in lean4?

#### Mario Carneiro (Mar 25 2021 at 21:10):

Just checked: no

#### Kevin Buzzard (Mar 25 2021 at 21:13):

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 (Mar 25 2021 at 21:34):

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 (Mar 25 2021 at 21:46):

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 (Mar 25 2021 at 21:47):

in particular, the fact that `apply @infLeRight`

doesn't work seems like the latest iteration of the apply bug

#### Leonardo de Moura (Mar 26 2021 at 01:34):

@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 (Mar 26 2021 at 01:35):

Thank you for the fixes!

Last updated: May 18 2021 at 23:14 UTC