# Zulip Chat Archive

## Stream: maths

### Topic: type class instance synthesis

#### Joseph Corneli (Apr 04 2019 at 11:23):

Can anyone comment on what's reasonable to expect from type class instance synthesis? This question might be to broad for a definitive answer, but here are some illustrative examples, for which I can be more specific.

1. Lean can infer that a subinterval of the reals is a topological space

2. ... but it can't infer that 1/x is defined for x in a given subset of the reals

(1) Why and (2) why not?

import analysis.exponential data.set.intervals analysis.exponential open real set def two_interval_set := (Icc (0:ℝ) 2) -- we get topological_space for free theorem continuous_id_on_tworeal' : continuous (λ (x : ↥two_interval_set), x) := begin exact continuous_id, end -- but we don't get has_div or has_one theorem continuous_1_over_x : continuous (λ (x : {r : ℝ | r ≠ 0} ), 1/x) := begin refine continuous_subtype_mk _ _, refine continuous_mul _ _, apply continuous_const, refine real.continuous_inv _ _, exact subtype.property, apply continuous_subtype_val, end

#### Joseph Corneli (Apr 04 2019 at 11:24):

Error for the second theorem:

failed to synthesize type class instance for x : ↥{r : ℝ | r ≠ 0} ⊢ has_div ↥{r : ℝ | r ≠ 0} failed to synthesize type class instance for x : ↥{r : ℝ | r ≠ 0} ⊢ has_one ↥{r : ℝ | r ≠ 0}

#### Johan Commelin (Apr 04 2019 at 11:26):

The problem is that Lean doesn't know what to do with the `1/x`

.

#### Johan Commelin (Apr 04 2019 at 11:26):

If you tell it to view `1`

and/or `x`

as a real number, then you might have more luck.

#### Johan Commelin (Apr 04 2019 at 11:27):

In particular, it doesn't know how to figure out the codomain of your function (let alone a topology on the codomain).

#### Johan Commelin (Apr 04 2019 at 11:27):

Try writing `(1 : ℝ)`

or `(x : ℝ)`

.

#### Joseph Corneli (Apr 04 2019 at 11:27):

OK, interesting... that got past the initial error.

#### Joseph Corneli (Apr 04 2019 at 11:29):

Viz., this proof works.

theorem continuous_1_over_x' : continuous (λ (x : {r : ℝ | r ≠ 0} ), (1:ℝ)/x) := begin refine continuous_mul _ _, apply continuous_const, refine real.continuous_inv _ _, exact subtype.property, apply continuous_subtype_val, end

#### Johan Commelin (Apr 04 2019 at 11:30):

That surpises me. I didn't expect the `mul const _`

#### Johan Commelin (Apr 04 2019 at 11:30):

I'd expect something like `continuous.comp continuous_inv continuous_subtype_val`

#### Joseph Corneli (Apr 04 2019 at 11:37):

Maybe this is more natural.

theorem continuous_1_over_x'' : continuous (λ (x : {r : ℝ | r ≠ 0} ), (1:ℝ)/x) := begin simp only [one_div_eq_inv], refine real.continuous_inv _ _, exact subtype.property, apply continuous_subtype_val, end

#### Johan Commelin (Apr 04 2019 at 11:39):

@Joseph Corneli I guess you know about the version in the library?

lemma real.continuous_inv' : continuous (λa:{r:ℝ // r ≠ 0}, a.val⁻¹) := continuous_iff_continuous_at.mpr $ assume ⟨r, hr⟩, (continuous_iff_continuous_at.mp continuous_subtype_val _).comp (real.tendsto_inv hr)

#### Joseph Corneli (Apr 04 2019 at 11:41):

I suspect I did see it at one point, yes! It's interesting that writing `a.val⁻¹`

escapes the problem of defining the codomain.

#### Johan Commelin (Apr 04 2019 at 11:42):

That is because Lean knows exactly where `a.val`

lives.

#### Joseph Corneli (Apr 04 2019 at 11:42):

But why doesn't it know where `x`

lives, in my example?

#### Johan Commelin (Apr 04 2019 at 11:42):

It also knows exactly where your `x`

lives, but it lives in a space on which division has not been defined.

#### Johan Commelin (Apr 04 2019 at 11:43):

Writing `(x : ℝ)`

means that Lean will silently turn your `x`

into `x.val`

.

#### Johan Commelin (Apr 04 2019 at 11:44):

Similarly, `1`

can live in any type with a `has_one`

instance. But if you write `(1 : ℝ)`

it figures out which Type you want `1`

to live in.

#### Johan Commelin (Apr 04 2019 at 11:44):

You could of course define a topology on `units ℝ`

, and prove that inversion is continuous there.

#### Johan Commelin (Apr 04 2019 at 11:45):

That's a different theorem from the one you just proved.

#### Joseph Corneli (Apr 04 2019 at 11:47):

OK, I think the key take-away for me is that `x`

and `x.val`

are different, which I *might* have picked up on from some of the other examples I was looking at, but didn't. Thanks!

#### Johan Commelin (Apr 04 2019 at 11:48):

One lives in the subtype, the other in the ambient type.

Last updated: May 19 2021 at 02:10 UTC