Error in lean3

Stream: general

[Adalynn]

I know that you're typically not supposed to be have prelude at the top of files, but it's for a personal (read: a crank) project to see how close I can get Lean 3 notation to standard mathematics. So, now to the actual question: when trying to define has_zero and has_one to get natural numbers to work, it seems to give me an error about how it can't force them to be nats. I can't seem to find the error message anywhere in the C++ code for one, so I'm just... wondering what's going on?

[Alex J. Best]

Can you make a #mwe?

[Adalynn]

Will do, just in the middle of class right now so I don't have the MWE on hand.

[Adalynn]

prelude
universe u
class has_zero(α: Type u) := (zero: α)

constant T: Type
constant t: T
noncomputable instance: has_zero T := has_zero.mk t

#check 0

and the error is "invalid numeral, failed to force numeral to be a nat"

[Adalynn]

It still breaks even if I try something like 0 + t when I add in notation-stuff for + as well

[Johan Commelin]

The default type for numerals in Lean 3 is ℕ aka nat. But I don't know how this plays with prelude.

[Johan Commelin]

Is nat defined after prelude? Do you need to provide an instance of has_zero nat?

[Adalynn]

prelude-mode doesn't have nat, I've checked. So the default is the unicode symbol? I'll have to try that later, along with a has_zero nat.

[Johan Commelin]

@Adalynn No, you don't need the unicode symbol. Maybe just assert the existence of nat, via

constant nat
axiom nat.has_zero : has_zero nat

[Johan Commelin]

Or define the actual inductive type, etc...

[Adalynn]

Yeah, that also doesn't work... Need to actually have an instance, which causes it to work. Thanks for the advice!

[Notification Bot]

Adalynn has marked this topic as resolved.

[Alex J. Best]

I'm still a bit confused by your question, the following works fine for me

prelude
universe u
class has_zero(α: Type u) := (zero: α)

class has_add (α: Type u) := (add: α → α → α)
notation a ` + ` b := has_add.add a b
constant T: Type
constant t: T
noncomputable instance: has_zero T := has_zero.mk t

noncomputable instance: has_add T := sorry

#check 0 + t
#check (0 : T)

[Johan Commelin]

@Alex J. Best But does #check 0 (without a type) also work for you?

[Alex J. Best]

No, but I wouldn't expect it to

[Alex J. Best]

Maybe I just don't understand what the goal is enough but "It still breaks even if I try something like 0 + t when I add in notation-stuff for + as well" was unclear to me, so I'm just showing that if you set things up right that works fine. and 0 is interpreted as something of type T

[Adalynn]

OH right, It's because I had in my file, add was defined via class has_add(α: Type u)(β: Type v)(γ: out_param(Type w)) := (add: α → β → γ) to allow for coset notation

[Alex J. Best]

Right if you have a heterogeneous addition operation you would need to specify the type of 0as (0 : T) if you wanted it to be in T otherwise lean would assume its a nat indeed (even if nat isn't defined)

[Adalynn]

Yeah, I thought initially it wasn't the homogeneity of the has_add but the homogeneity of the arguments (i.e. I thought it would work if I had an instance as has_add T T T) which was why I was so confused, thanks.

[Notification Bot]

Adalynn has marked this topic as unresolved.

[Adalynn]

prelude
...
instance Class_subset_Class: has_subset Class Class :=
    ⟨λC: Class, λD: Class, ∀(x: Set)[x∈C ⇒ x∈D]⟩
  noncomputable instance Class_subset_Set: has_subset Class Set :=
    ⟨λC: Class, λS: Set, ∀(x: Set)[x∈C ⇒ x∈S]⟩
  noncomputable instance Set_subset_Class: has_subset Set Class :=
    ⟨λS: Set, λC: Class, ∀(x: Set)[x∈S ⇒ x∈C]⟩
  noncomputable instance Set_subset_Set: has_subset Set Set :=
    ⟨λS: Set, λT: Set, ∀(x: Set)[x∈S ⇒ x∈T]⟩

constants A B: Class
constants S T: Set
#check A ⊆ B

For some reason this also breaks, with a heterogeneous $\subseteq$ defined in a different file...

this is probably why people don't use prelude often

[Adalynn]

the same thing happened when I tried overloading the heterogenous equals with Set = Class and Class = Set, it for some reason clashed with the homogenous equals instance in a different file

What's going on? Does the lean 3 compiler just like to force homogeneity?

[Kyle Miller]

For what it's worth, here's where the nat error in the C++ is reported https://github.com/leanprover-community/lean/blob/f2b2beefe2e9ab200d23e1c99dc20879eb32e9fa/src/frontends/lean/elaborator.cpp#L3618

[Adalynn]

I fixed the nat error already, by using a workaround... but I'm now stuck on a similar error with typeclasses

[Adalynn]

Oh, I fixed it, I had needless out_params everywhere