Zulip Chat Archive

Stream: general

Topic: shadok Lean


Patrick Massot (Apr 10 2020 at 20:20):

Is it me or Lean being weird?

def ga :=  {u :   }, true

lemma bu : true  ga := λ _ _, trivial

lemma zo : ga  true := λ _, trivial

#check @bu     -- true → ga
#check trivial    -- true
#check bu trivial  -- true  ?!?

lemma meu : true :=
begin
  apply zo,
  -- exact bu trivial, -- invalid type ascription, term has type true but is expected to have type ga
  apply bu,
  exact trivial,
end

Note that switching from implicit argument to explicit in the first definition makes everything work as (I) expected.

Patrick Massot (Apr 10 2020 at 20:21):

I think this is a job for @Gabriel Ebner

Gabriel Ebner (Apr 10 2020 at 20:22):

Is this a reducibility problem? What happens if you put an @[reducible] on ga?

Patrick Massot (Apr 10 2020 at 20:22):

It changes nothing

Gabriel Ebner (Apr 10 2020 at 20:25):

Ah, then it is the typical "stuff is different when there is an expected type":

#check (bu trivial : ga)  -- invalid type ascription

Gabriel Ebner (Apr 10 2020 at 20:29):

Actually I'm not really sure what you expected. The implicit argument in ga is being applied, this is the purpose of implicit arguments. If you don't want this, use ⦃⦄.

Patrick Massot (Apr 10 2020 at 20:29):

Isn't this Lean program meant to follow somehow the typing rules lambda calculus?

Patrick Massot (Apr 10 2020 at 20:30):

Being applied to what?

Gabriel Ebner (Apr 10 2020 at 20:30):

This is the magic of implicit arguments. The function bu has one explicit argument and one implicit argument, so when you write bu trivial, the implicit argument is added implicitly.

Patrick Massot (Apr 10 2020 at 20:31):

But what is it applied to?

Patrick Massot (Apr 10 2020 at 20:31):

A meta-variable?

Gabriel Ebner (Apr 10 2020 at 20:31):

Right!

Patrick Massot (Apr 10 2020 at 20:32):

This is crazy.

Gabriel Ebner (Apr 10 2020 at 20:32):

Regarding ⦃⦄: if you look at the definitions of transitive, reflexive, etc., you will see that they also use the strict implicit binders for exactly the reason that you've just noticed.

Patrick Massot (Apr 10 2020 at 20:32):

I never really managed to remember what those {{ and }} are meant for.

Patrick Massot (Apr 10 2020 at 20:34):

Let me now try on my real problem.

Gabriel Ebner (Apr 10 2020 at 20:35):

If you have f : ∀ α {β} γ ⦃δ⦄ ε, ρ, then:

f          becomes    @f
f a        becomes    @f a _
f a g      becomes    @f a _ g
f a g e    becomes    @f a _ g _ e

Gabriel Ebner (Apr 10 2020 at 20:36):

The difference is whether Lean will eagerly add underscores or not.

Patrick Massot (Apr 10 2020 at 20:37):

Thanks Gabriel! It even work in my real use case!


Last updated: Dec 20 2023 at 11:08 UTC