don't know how to

Stream: new members

[Etienne Laurin]

Hi! I'm a C++ developer in Dublin. I'm trying to learn Lean by doing some exercises.

variables {T : Type} {A B : T → Prop}
lemma t₁ : (∃ x, A x) → ∃ x, (A x ∨ B x) := λ ⟨x, p⟩, ⟨x, or.inl p⟩
lemma t₂ : (∃ x, A x) ∨ (∃ x, B x) → ∃ x, (A x ∨ B x) :=
    λ h, h.cases_on (λ ⟨x, p⟩, ⟨x, or.inl p⟩) (λ ⟨x, p⟩, ⟨x, or.inr p⟩)

t₁ works but t₂ fails with "don't know how to synthesize placeholder". How can I get Lean to tell me what/where this placeholder is? Is there something better than or.cases_on that I could be using?

[Mario Carneiro]

There is a known issue with using projection notation in conjunction with @[elab_as_eliminator] definitions like or.cases_on. You can fix the proof by either not using projection notation, i.e. or.cases_on h instead of h.cases_on, or by using h.elim instead (which is basically the same as or.cases_on without the weird elaborator marking)

[Etienne Laurin]

Thanks!

[Kevin Buzzard]

How can you tell or.cases_on is tagged @[elab_as_eliminator]? #print or.cases_on only tells me it's @[reducible]

[Mario Carneiro]

Hm, that's interesting. T.rec, T.rec_on, and T.cases_on are automatically generated for every inductive type and are always treated as if they have elab_as_eliminator enabled, although you are right that there is no explicit indication of such. You can test it by making a copy of or.cases_on with exactly the definition #print says, and the lemma will typecheck; then if you add elab_as_eliminator you get exactly the same errors

[Kevin Buzzard]

example : @or.cases_on = @or.elim := rfl, and they're both there, so they must be different somehow ;-) It's how the elaborator elaborates them.

[Mario Carneiro]

you should be aware that that's not the best way to check that two definitions are the same according to lean, that is only up to defeq which ignores annotations and bindings, as well as unifying universes

[Mario Carneiro]

Also, strange as it may sound I'm pretty sure there are duplicate definitions (completely identical) in lean. Often this has to do with renaming

[Edward Ayers]

I got this to work with
λ h, or.cases_on h (λ ⟨x, p⟩, ⟨x, or.inl p⟩) (λ ⟨x, p⟩, ⟨x, or.inr p⟩)

[Edward Ayers]

Can someone explain what the "synthesize placeholder" error actually means? It is by far the most common error I get and I currently get rid of it by making random transformations to the source until it goes away

[Mario Carneiro]

it means the proof is unfinished

[Edward Ayers]

proof that the term typechecks?

[Mario Carneiro]

lean is saying "there is a missing part of the proof and I don't know how to fill it in"

[Mario Carneiro]

No, the term itself is the proof

[Edward Ayers]

I often get it where the goal that it is trying to prove is Type ?. What should I do then?

[Mario Carneiro]

That means there is a missing type somewhere

[Mario Carneiro]

for example, looking at the term you just gave without any other context, I can't figure out the type of h

[Mario Carneiro]

I know it is an or of something but I don't know what

[Mario Carneiro]

so if I were lean I would say "couldn't synth placeholder |- Type ?"

[Edward Ayers]

Ok let me paste some code where I can't figure out what it wants
I put this file in mathlib/category_theory/scratch.lean

import .category
import .functor
universes u1 u2 v1 v2

namespace category_theory
    section
        variables
            {C : Type u1} [𝒞 : category.{u1 v1} C]
            {D : Type u2} [𝒟 : category.{u2 v2} D]
        include 𝒞 𝒟
        def t : Π (a b c : D) (p : a = b) (x : a ⟶ c), b ⟶ c := λ a b c p x, eq.rec x p
        def t2 (F G : C ↝ D) (ob_eq : ∀ (Z : C), F Z = G Z)  (X Y : C) (f : X ⟶ Y) : (G X ⟶ F Y)
            := t (F X) (G X) (F Y) (ob_eq X) (F.map f)
    end
end category_theory

And I get a synth Type ? error for t in t2 but I can't figure out which type I am missing

[Reid Barton]

Just looking at this (haven't built recent mathlib yet), I think the problem is that t "depends on" C, because of include 𝒞, but there's nothing in the type of t which can ever determine what C has to be.

[Edward Ayers]

Ah, so if you are in a section and write variables, then all definitions in that section implicitly depend on these variables, even if they are not used in the definition?

[Reid Barton]

And so there's no reason that t's C in the use of t in t2needs to be the same as the C in t2, so Lean can't figure out how to assign it.

[Reid Barton]

Not in general, but using include forces the variable to be included as a parameter to every subsequent definition.

[Edward Ayers]

Where can I find some docs on include? I find it cryptic

[Reid Barton]

So if you show the full inferred type of t, it should begin t : \Pi {C : Type u1} [𝒞 : category.{u1 v1} C] ...

[Reid Barton]

𝒞was included because of the include, and C was included because 𝒞 depends on it

[Edward Ayers]

If I comment out include, then the \hom arrows become errors. How would I get rid of those errors without using include?

[Edward Ayers]

It can't find evidence for category D.

[Reid Barton]

https://leanprover.github.io/theorem_proving_in_lean/tactics.html mentions include/omit in the first section. I don't remember whether it is also explained elsewhere in TPIL

[Reid Barton]

In this case, you could put include 𝒟 between the definitions of t and t2

[Edward Ayers]

Fixed code:

import .category
import .functor
universes u1 u2 v1 v2

namespace category_theory
    section
        variables
            {C : Type u1} [𝒞 : category.{u1 v1} C]
            {D : Type u2} [𝒟 : category.{u2 v2} D]
        include 𝒟
        def t : Π (a b c : D) (p : a = b) (x : a ⟶ c), b ⟶ c := λ a b c p x, eq.rec x p
        include 𝒞
        def t2 (F G : C ↝ D) (ob_eq : ∀ (Z : C), F Z = G Z)  (X Y : C) (f : X ⟶ Y) : (G X ⟶ F Y)
            := t (F X) (G X) (F Y) (ob_eq X) (F.map f)
    end
end category_theory

[Reid Barton]

Normally you could just omit the names 𝒞 : and 𝒟 : and the include statements and Lean would figure out where it needs the instance variables. The fact that that doesn't work here is some combination of there being extra universe parameters involved and a bug in Lean, I think.

[Edward Ayers]

Ok but this then errors for me:

import .category
import .functor
universes u1 u2 v1 v2

namespace category_theory
    section
        variables
            {C : Type u1} [category.{u1 v1} C]
            {D : Type u2} [category.{u2 v2} D]
        --include 𝒟
        def t : Π (a b c : D) (p : a = b) (x : a ⟶ c), b ⟶ c := λ a b c p x, eq.rec x p
        --include 𝒞
        def t2 (F G : C ↝ D) (ob_eq : ∀ (Z : C), F Z = G Z)  (X Y : C) (f : X ⟶ Y) : (G X ⟶ F Y)
            := t (F X) (G X) (F Y) (ob_eq X) (F.map f)
    end
end category_theory

[Edward Ayers]

kernel failed to type check declaration 't' this is usually due to a buggy tactic or a bug in the builtin elaborator

[Edward Ayers]

cool

[Edward Ayers]

which must be why it had 𝒞 : in to start with, to avoid the lean bug

[Reid Barton]

Yes. The reason is either that Lean doesn't know what universe parameters to specialize ⟶ to, or that there's a bug where including the instance variable doesn't cause C to also get included. I don't remember the exact details any more.
When you get that "kernel failed to type check declaration" error, it means it failed to include C, I think.

[Reid Barton]

Right, the workaround is that when you manually tell it to include the category instance, then it can correctly infer that it needs C too. The downside is that now you are responsible for making sure the right variables are included--if you have too many then you end up with your original issue.

[Edward Ayers]

thanks so much for your help

[Reid Barton]

In general, this class of error can be tough to figure out. I don't know of a better way than thinking really hard about what Lean is trying to do and figuring out where it might be getting stuck.

[Reid Barton]

No problem

[Edward Ayers]

It seems like solving these errors requires intimately knowing what the elaborator is doing. And from what I know, the elaborator is very elaborate

[Patrick Massot]

Normally you could just omit the names 𝒞 : and 𝒟 : and the include statements and Lean would figure out where it needs the instance variables.

I think this is not true. To me it seems Lean will always include these statements. That explains why we sometimes see unneeded or duplicate instance arguments, even in mathlib

[Patrick Massot]

It seems like solving these errors requires intimately knowing what the elaborator is doing. And from what I know, the elaborator is very elaborate

Unfortunately and fortunately, this is all very true.

[Edward Ayers]

It would be great if when there was an elaborator error, a textbox appeared that you could enter the missing type or proof into.

[Mario Carneiro]

Lean will include an unnamed typeclass variable when all of its dependencies are included (usually because they are mentioned directly in the statement or are dependencies of something mentioned). Like so:

variables (A : Type) [group A]
example (x : A) : true := ... -- group A is included
example : true := ... -- group A is not included

[Patrick Massot]

yes, this matches what I saw

[Reid Barton]

Yes, good point @Patrick Massot.

[Mario Carneiro]

Lean will never include a named typeclass variable unless it is mentioned:

variables (A : Type) [G : group A]
example (x : A) : true := ... -- group A is not included
example : x + x = x := ... -- group A is included

And an included typeclass variable is always included:

variables (A : Type) [G : group A]
include G
example (x : A) : true := ... -- group A is included
example : true := ... -- group A is included

[Scott Morrison]

I will add some documentation about include right in the category_theory files, specialised to the use case there.

Unfortunately category C has an unbound universe level, because we need to know the universe level of the morphisms, and this is not determined by the universe level of C itself. (This design decision is constrained by the desire to be able to write uniform code for small categories and large categories.)

When we write variable [category.{u v} C], Lean is reasonably rather hesistant to use this variable, unless it is sure that v is the actually intended universe level. To avoid having to explicitly write this universe variable in every definition that you're hoping will make use of this [category C] variable, we give it a name as in [𝒞 : category.{u v} C] and explicitly include it in every following declaration, via include 𝒞.

This then adds a danger: if you write another declaration that doesn't actually care about this category (e.g. one declaration refers to four different categories, but a subsequent one only mentions two), this typeclass variable will still be included as an argument, mucking everything up. Hence include 𝒞 statements need to be carefully scoped with section .... end commands.