Zulip Chat Archive

Stream: maths

Topic: type class instance synthesis


view this post on Zulip 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

view this post on Zulip 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}

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:26):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:27):

Try writing (1 : ℝ) or (x : ℝ).

view this post on Zulip Joseph Corneli (Apr 04 2019 at 11:27):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:30):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:30):

I'd expect something like continuous.comp continuous_inv continuous_subtype_val

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:42):

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

view this post on Zulip Joseph Corneli (Apr 04 2019 at 11:42):

But why doesn't it know where x lives, in my example?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:43):

Writing (x : ℝ) means that Lean will silently turn your x into x.val.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:44):

You could of course define a topology on units ℝ, and prove that inversion is continuous there.

view this post on Zulip Johan Commelin (Apr 04 2019 at 11:45):

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

view this post on Zulip 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!

view this post on Zulip 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