default / inhabited for ℚ, ℝ, ℂ

Stream: new members

[Bryan Gin-ge Chen]

I'm going through TPIL's chapter on typeclasses and while messing around tried the following:

import data.complex.basic
#reduce default ℚ -- no type class instance of inhabited ℚ
#reduce default ℝ -- timeout
#reduce default ℂ -- timeout

#check succeeds on the last two.

Questions: Is the lack of something like

instance : inhabited ℚ := ⟨0⟩

in data.rat just an oversight or was this intentional? Why do the other two lines time out?

Meta-question: am I right that this doesn't really matter; i.e. default is unlikely to be used in an "actual" proof?

[Kevin Buzzard]

I suspect that #reduce fails on the last two because the reals and complexes are in general a pain to compute with -- they don't have decidable equality and they might well not even have an algorithm for printing out a real number. What would you expect sqrt(2) to look like in Lean? Is it supposed to print out all the digits? :-)

I would imagine that Q not being inhabited, if true, is an oversight.

[Chris Hughes]

They time out because a real number is built from a Cauchy sequence, and making a Cauchy sequence requires a proof that the sequence is Cauchy. When you #reduce a real, it will try to unfold this proof to axioms, and this will be huge.

[Bryan Gin-ge Chen]

Thanks, that makes sense! Out of curiosity, what would be the right way to get Lean to spit out the default elements for ℝ and ℂ then?

[Chris Hughes]

The best way to check what they are is to look at the definition of the inhabited instance. Reals don't have decidable equality, so given a real, lean cannot tell if it equals zero or not.

[Kevin Buzzard]

import data.real.basic

definition d : inhabited ℝ := by apply_instance

#print d

/-

def d : inhabited ℝ :=
real.inhabited

-/

#check real.inhabited -- inhabited ℝ

-- Now right-click on real.inhabited and select "peek definition"

[Kevin Buzzard]

I only mention this because I know of no other way of figuring out the real number which was used other than by looking at the source. I don't know how to look at the definition of d directly, as it were.

[Bryan Gin-ge Chen]

Ah, OK, so in general, instance : typeclass something can be accessed with something.typeclass. I must have read this somewhere...

Knowing that I can just #print real.inhabited and read off {default := 0}.

As an aside, it seems that rat is missing a bunch of other stuff too, like rat.ring, rat.add_group, rat.field, etc. although they're all an easy by apply_instance away.

[Kevin Buzzard]

waitwaitwait. If by apply_instance works, it's there.

[Kevin Buzzard]

A lot of these instances might be being inferred automatically. For example, Lean knows that any field is automatically a comm_ring, a ring, an add_monoid etc etc.

[Bryan Gin-ge Chen]

waitwaitwait. If by apply_instance works, it's there.

Maybe I used the wrong words, but I was referring to the following behavior:

#check rat.comm_ring -- unknown identifier
instance : comm_ring rat := by apply_instance
#check rat.comm_ring -- Lean is happy

[Chris Hughes]

Another way of discovering the name is
```lean
def foo : inhabited real := by apply_instance
#print foo

[Patrick Massot]

Bryan, this is not a bug, this is what the type class system is about

[Patrick Massot]

You get cascading for free

[Bryan Gin-ge Chen]

Bryan, this is not a bug, this is what the type class system is about

Right, I didn't intend to imply that there were any bugs other than in my understanding.

[Kevin Buzzard]

https://github.com/leanprover/mathlib/pull/254

[Kevin Buzzard]

import data.rat

definition x : comm_ring ℚ := by apply_instance

#print x

/-

def x : comm_ring ℚ :=
field.to_comm_ring ℚ

-/

Lean knows that the rationals are a commutative ring, but the instance is not called rat.comm_ring, it's called something else.

If X is an inductive type and there's something called X.foo, and if a has type X, then you can sometimes talk about a.foo on a good day. But that's not what's happening here. It's not rat that has type comm_ring, it's some other thing which has type comm_ring rat.

[Chris Hughes]

Lean knows that the rationals are a commutative ring, but the instance is not called rat.comm_ring, it's called something else.

I don't think it has a name, it's just inferred from rat.discrete_linear_ordered_field or something.

[Kevin Buzzard]

I guess the term is field.to_comm_ring ℚ and there's no name for this term. On the other hand when instance : foo bar := blah is run, Lean has a go at naming the instance itself using some vaguely sane algorithm.

[Bryan Gin-ge Chen]

It looks like field.to_comm_ring itself is created automatically from extends comm_ring in the class field declaration.

[Kevin Buzzard]

Yeah, that's a cool part of type class inference. The projectors get constructed automatically.

[Kevin Buzzard]

import data.rat

definition d : comm_monoid ℚ := by apply_instance

set_option pp.all true
#print d

/-

def d : comm_monoid.{0} rat :=
@linear_ordered_comm_ring.to_comm_monoid.{0} rat
  (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} rat
     (@discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring.{0} rat rat.discrete_linear_ordered_field))

-/

Type class inference is quite clever.

[Bryan Gin-ge Chen]

It looks much more persistent than clever when I put on set_option trace.class_instances true :wink: