# Zulip Chat Archive

## Stream: new members

### Topic: refl on different instances

#### Horatiu Cheval (Feb 27 2021 at 09:31):

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 (Feb 27 2021 at 10:03):

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 (Feb 27 2021 at 10:06):

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 (Feb 27 2021 at 10:07):

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 (Feb 27 2021 at 15:03):

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!

Last updated: May 16 2021 at 21:11 UTC