How implicit arguments are inferred

Stream: new members

[Alex Meiburg]

Can someone help me understand how implicit arguments are inferred? When I try to leave an argument implicit, even though I have the right type in context, it fails to fill it in:

don't know how to synthesize implicit argument
  @cotransitive_pos_of_neg_pos α R a b c ?m.20834 hab hac
context:
α: Type u_1
β: Type u_2
l: List α
R: α → α → Prop
inst✝¹: DecidableRel R
ab: α
R₂: β → β → Prop
inst✝: DecidableRel R₂
hr: Coequivalence R
hab: ¬R a b
c: α
cs: List α
ih: length (destutter' R a cs) = length (destutter' R b cs)
ht: Cotransitive R
hac: R a c
⊢ Cotransitive R

I have an instance of Cotransitive R right there, but it doesn't pull it in... I don't know why.

[Alex Meiburg]

More generally, any good guide to how to deal with explicit/implicit/strict-implicit/[...] binders? And when to use them? And how to best pass them? I couldn't find a guide _anywhere_

[Kyle Miller]

They're solved purely by unification. It won't do by assumption to try to fill them in.

[Kyle Miller]

(strict implicit vs implicit are the same in this way; they just have to do with how eager the arguments get filled in with a metavariable)

[Kyle Miller]

I've thought about how it would be nice to have a new binder type that like an implicit but solves for itself using by assumption. This would make it easy to pass around additional facts without needing to hook it into the typeclass system, which is what [...] binders are about

[Kyle Miller]

I can't seem to find all the binder types in the Lean 4 reference manual... The Lean 3 reference manual mentions them: https://lean-lang.org/reference/expressions.html#implicit-arguments They're basically the same, except now (x : α . t) is (x : α := by t)

[Kyle Miller]

Theorem Proving in Lean mentions implicit arguments: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html?highlight=implicit#implicit-arguments

[Kyle Miller]

So does Functional Programming in Lean: https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#implicit-arguments

[Kyle Miller]

Kyle Miller said:

They're solved purely by unification.

In particular, what this means is that they have to be solvable from the expected type and all the explicit arguments (and maybe in some cases from typeclass arguments too). It does not take the local context into account.

[Alex Meiburg]

Okay, but when I write

variable {α : Type*} [LinearOrderedSemiring α] (P : Polynomial α)

then it knows to build the Polynomial from the LinearOrderedSemiring structure that I have in context. I also know that I could pass the necessary [Semiring R] argument to @Polynomial if I wanted to. Why does that work?

[Kyle Miller]

In those references, try looking up things about typeclasses. Typeclass arguments are synthesized using the collection of global instances and local instances.

[Kyle Miller]

I see why you might think that it's like it's pulling an assumption from the context, but there's a whole graph-search-like algorithm going on with these.

[Notification Bot]

This topic was moved here from #general > How implicit arguments are inferred by Kyle Miller.

[Kyle Miller]

(@Alex Meiburg You're asking fine questions, and I moved this thread to where questions about Lean basics, like all the types of binders, normally would appear.)

[Alex Meiburg]

Oh, huh! Alright. I guess I would've thought that type classes are morally like hypotheses. Hmm

[Kyle Miller]

All the instances in Lean, std, and mathlib explain how to get a particular instance given 0 or more additional instances, and these are solved for recursively.

If you're familiar with Prolog, it's like that.

[Kyle Miller]

In particular, a local typeclass instance could be used as a hypothesis to one of these other instances

[Kyle Miller]

This is how a CommRing can be a Ring. There's an instance somewhere out there that helps make the inference.

[Patrick Massot]

Alex, beginners questions are welcome here, but it still feels like your life would be a lot easier if you read some documentation instead of trying to guess and then ask here.

[Matt Diamond]

(deleted)

[Kyle Miller]

(@Matt Diamond I read your deleted message -- there's still sort of a local instance cache, but Lean maintains it by itself. It's an optimization for answering the question "for each local variable, is it an instance, and if so which class is it for?")

[Matt Diamond]

Gotcha, makes sense.

[Alex Meiburg]

Okay, so I had read through https://leanprover-community.github.io/mathematics_in_lean/C06_Structures.html before asking this, but my confusion was (I guess) coming from seeing how Equivalence and related things are defined in lean/mathlib. Like, based on what you've said, and that documentation page, I would expect Equivalence to be a class. And then there would be an instance to show that it's also a Reflexive, Symmetric, and Transitive as well.

Instead, the definitions read like:

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  /-- An equivalence relation is reflexive: `x ~ x` -/
  refl  : ∀ x, r x x
  /-- An equivalence relation is symmetric: `x ~ y` implies `y ~ x` -/
  symm  : ∀ {x y}, r x y → r y x
  /-- An equivalence relation is transitive: `x ~ y` and `y ~ z` implies `x ~ z` -/
  trans : ∀ {x y z}, r x y → r y z → r x z

def Reflexive := ∀ x, x ≺ x

def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x

def Transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z

lemma Equivalence.reflexive {r : β → β → Prop} (h : Equivalence r) : Reflexive r := h.refl

lemma Equivalence.symmetric {r : β → β → Prop} (h : Equivalence r) : Symmetric r := λ _ _ => h.symm

lemma Equivalence.transitive {r : β → β → Prop} (h : Equivalence r) : Transitive r :=
  λ _ _ _ => h.trans

So maybe my confusion is that I was trying to go off of Equivalence as my reference, and maybe Equivalence is a weird one?

[Yaël Dillies]

Yeah, it is quite weird (and basically unused)

[Yaël Dillies]

Note however that we do have relation classes: docs#IsRefl, docs#IsTrans, docs#IsSymm ...

[Alex Meiburg]

Oh, I'd missed that! That's great, thanks. I'll probably use those instead, then.

[Alex Meiburg]

Regarding reading documentation first: I guess my two biggest questions where "is there a way to explicitly provide only some arguments" (that is, if I have a function with 6 implicit arguments, can I just provide one without stubbing out 5 underscores?) and "what is the ⦃⦄/{{ }} binder".

Of the pages given, none answer the first question. https://lean-lang.org/reference/expressions.html#implicit-arguments is the only one that mentions ⦃⦄, and it just says that it's "an implicit argument, weakly inserted". However, there's no information on what "weakly inserted" means, anywhere on that page or any other I could find. It does have one example (which uses pi-types, which don't exist in lean4, but I was able to find that I could change this to a ∀), but I wasn't able to divine what 'weakly inserted' means from that example.

Sorry if this comes across as a bit of a complaint. I realize this is a community project, and that there's a lot of changes from lean 3 to lean 4, and that a lot of lean documentation is written assuming some familiarity with other proof assistants or dependent type theory (which I lack). But it does make it pretty hard to navigate the documentation, and more often than not I'm not even sure if I'm (1) looking at the wrong documentation to try to answer my question, (2) looking at the right documentation and failing to understand the answer, or (3) not even asking a well-formed question.

[Yaël Dillies]

If h : ∀ ⦃a : α⦄, p a → q a (where α : Type*, p q : α → Prop), then h is defeq to ∀ a, p a → q a but h ha (where ha : p a) is defeq to q a.

[Yaël Dillies]

Namely, ⦃⦄ arguments act as implicit arguments iff a later argument has been provided. I use and abuse this feature.

[Yaël Dillies]

In contrast, if h : ∀ {a : α}, p a → q a, then h is defeq to p ?a → q ?a and h ha is defeq to q a, and if h : ∀ a, p a → q a, then h is defeq to ∀ a, p a → q a while h a is defeq to p a → q a

[Yaël Dillies]

To give an argument named arg to a function foo, you can do foo (arg := your_arg_here).

[Alex Meiburg]

Okay, thank you very much for that explanation! :) So in the first example, how would it look if I did want to pass a to h? Because if I pass one argument, it seems as though Lean always wants to assume that it's the p a second argument.

Is it only relevant if I was passing h to some other function, that wants an argument of type forall a, p a -> q a?

[Yaël Dillies]

Alex Meiburg said:

Is it only relevant if I was passing h to some other function, that wants an argument of type forall a, p a -> q a?

No, it's definitely relevant in that case, but the most important use case is for predicates like docs#ConvexOn

[Alex Meiburg]

Ahhh alright, I'll try better to understand what's going on there. Thanks a bunch! 🙏🏼

[Yaël Dillies]

For passing the first argument, you could @h a ha or h (a := a) ha

[Kevin Buzzard]

@Alex Meiburg all of this explicit/implicit stuff is explained in #tpil .