refl on different instances

Stream: new members

[Horatiu Cheval]

Hello, I defined a typeclass stating that a real number is in $[0, 1]$, and used it in the definition of some other class.
Now I can't prove the equality in the example below, because each term contains a different instance, as shown by set_option pp.all true.
Can I get around this?

import data.real.basic
import topology.metric_space.basic

--set_option pp.all true

noncomputable theory

class ℝ01 (x : ℝ) :=
(zero_le : 0 ≤ x)
(le_one : x ≤ 1)

class space (α : Type) extends metric_space α :=
(op : ∀ (θ : ℝ) [ℝ01 θ], α → α)

variables {α : Type} [space α]
open space

example (θ₁ θ₂ : ℝ) [ℝ01 θ₁] [ℝ01 θ₂] (h : θ₁ = θ₂) (x y : α) : op θ₁ x = op θ₂ x :=
begin
    -- rw h, /-fails, motive is not type correct-/
    tactic.unfreeze_local_instances,
    subst h,
    refl,
-- invalid apply tactic, failed to unify
--   op θ₁ x = op θ₁ x
-- with
--   ?m_2 = ?m_2
end

[Scott Morrison]

First, you probably don't want to use the typeclass system like this. It's not intended as a "prover", and often bundling the data in as fields of a structure (perhaps with a coercion back to the base type) works better (or just use subtype).

[Scott Morrison]

And then just

import data.real.basic
import topology.metric_space.basic

structure ℝ01 :=
(x : ℝ)
(zero_le : 0 ≤ x)
(le_one : x ≤ 1)

class space (α : Type) extends metric_space α :=
(op : ∀ (θ : ℝ01), α → α)

variables {α : Type} [space α]
open space

example (θ₁ θ₂ : ℝ01) (h : θ₁ = θ₂) (x y : α) : op θ₁ x = op θ₂ x :=
begin
    rw h,
end

[Scott Morrison]

And then the coercion

instance : has_coe ℝ01 ℝ :=
⟨λ x, x.x⟩

would let you treat terms of ℝ01 as if they were just in ℝ.

[Horatiu Cheval]

I see, I was hoping to avoid through typeclasses having to repetedly provide proofs for the fact that the interval is closed under some operations, but this seems to work better in the end. Thanks!