shadok Lean

Stream: general

[Patrick Massot]

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]

I think this is a job for @Gabriel Ebner

[Gabriel Ebner]

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

[Patrick Massot]

It changes nothing

[Gabriel Ebner]

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

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

[Gabriel Ebner]

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]

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

[Patrick Massot]

Being applied to what?

[Gabriel Ebner]

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]

But what is it applied to?

[Patrick Massot]

A meta-variable?

[Gabriel Ebner]

Right!

[Patrick Massot]

This is crazy.

[Gabriel Ebner]

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]

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

[Patrick Massot]

Let me now try on my real problem.

[Gabriel Ebner]

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]

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

[Patrick Massot]

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