type class instance synthesis

Stream: maths

[Joseph Corneli]

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]

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]

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

[Johan Commelin]

If you tell it to view 1 and/or x as a real number, then you might have more luck.

[Johan Commelin]

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

[Johan Commelin]

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

[Joseph Corneli]

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

[Joseph Corneli]

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]

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

[Johan Commelin]

I'd expect something like continuous.comp continuous_inv continuous_subtype_val

[Joseph Corneli]

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]

@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]

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]

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

[Joseph Corneli]

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

[Johan Commelin]

It also knows exactly where your x lives, but it lives in a space on which division has not been defined.

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Joseph Corneli]

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]

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