Zulip Chat Archive

Stream: new members

Topic: Element in set is too restricted


Raphael Appenzeller (May 07 2022 at 21:38):

(mwe below). My goal state is:

a b :  
   (x : {x :  | a  x  x  b}), dist x x = 0 :=

and I try to change ... |x-x| = 0, but Lean is not comfortable subtracting x from x, as it is in a special set, which may not contain 0. How can I convince Lean that it should think of x as an element in ? The error I get is:

failed to synthesize type class instance for
a b : ,
x : {x :  | a  x  x  b}
 has_zero {x :  | a  x  x  b}
state:
a b : 
  (x : {x :  | a  x  x  b}), dist x x = 0

Minimal Working example:

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

namespace metric_space
variables {X : Type} [metric_space X]

noncomputable def interval (a b :  ) : metric_space {x :  | a  x  x  b }  :=
{
    dist := λ x y ,  |x-y|,
    dist_self :=
    begin
      change  (x : {x :  | a  x  x  b}), |x-x| = 0,
    end,
    dist_comm := sorry,
    dist_triangle := sorry,
    eq_of_dist_eq_zero := sorry,
}

Julian Berman (May 07 2022 at 21:44):

I think you put the coercion further inward. (I know nothing about the math you're doing, but...)

Julian Berman (May 07 2022 at 21:44):

change ∀ (x : {x : ℝ | a ≤ x ∧ x ≤ b}), |(x : ℝ)-x| = 0,

Julian Berman (May 07 2022 at 21:44):

seems to work.

Raphael Appenzeller (May 07 2022 at 22:00):

Thanks a lot! This worked.


Last updated: Dec 20 2023 at 11:08 UTC