Zulip Chat Archive

Stream: new members

Topic: refl on different instances


view this post on Zulip Horatiu Cheval (Feb 27 2021 at 09:31):

Hello, I defined a typeclass stating that a real number is in [0,1][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

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

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

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

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