## 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)

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