Quotients & synthesizing

Stream: maths

[Ryan Lahfa]

Hello, I'm trying to do some quotients stuff, namely to build the completion of a metric space.
So here's a minimal example:

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

section test
open metric_space
variables {X: Type*} [metric_space X]

def cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)
def cauchy_seqs := { f : ℕ → X // cauchy f }


def cauchy.setoid : setoid cauchy_seqs :=
{
  r := sorry,
  iseqv := sorry
}

def completion_of_metric_space: Type* := quotient cauchy.setoid
-- instance completion.metric_space: espace_metrique cauchy.setoid
end test

So here's my first attempt, cauchy.setoid fails with:

don't know how to synthesize placeholder
context:
⊢ Type ?

So what I have done is to add types everywhere and had this new minimal example, but now I have this "too many arguments" issues:

import data.set
import data.real.basic


-- Une structure d'espace métrique sur un type X --
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

namespace test
open metric_space
variables {X: Type*} [metric_space X]

def cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)

end test

section test2
def cauchy_seqs (X: Type*) [metric_space X] := { f : ℕ → X // test.cauchy f }
def cauchy.setoid (X: Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := sorry,
  iseqv := sorry
}

-- en termes d'univers, quotient retourne un type d'univers u + 1 en partant de T : Type u.
def completion_of_metric_space (X: Type*) [metric_space X]: Type* := quotient (cauchy.setoid X)

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion_of_metric_space X)
{
  d := sorry,
}
end test2

Precisely:

function expected at
  metric_space (completion_of_metric_space X)
term has type
  Type ?
Additional information:
/home/raito/dev/projects/projet-maths-lean/src/espaces-metriques/test.lean:34:62: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

I have found this topic: https://leanprover-community.github.io/archive/stream/113488-general/topic/has_coe_to_fun.20with.20implicit.20arguments.html which seems to have this error, but I don't understand how to port the idea to my problem.

Also, I guess it might have to do with some universes stuff as I'm trying to cheat and let Lean compute the correct universes, but it might be possible that I need to be explicit and specify that a completion lives in Type (u + 1) ?

[Kevin Buzzard]

Not at lean right now so treat with a pinch of salt. Lean can't figure out X in the first example. Make it explicit and call it cauchy_seqs X

[Kevin Buzzard]

Oh you got that far

[Ryan Lahfa]

Kevin Buzzard said:

Oh you got that far

Indeed, but that means that I have to do it the 2nd way at least :)

[Kevin Buzzard]

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }


def cauchy.setoid (X : Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := sorry,
  iseqv := sorry
}

def completion (X : Type*) [metric_space X] : Type* := quotient (cauchy.setoid X)

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := sorry,
  d_pos := sorry,
  -- etc
}

end test

[Kevin Buzzard]

PS d_pos follows from the other axioms :P (use the triangle equality) and presep should just be forall x, d x x = 0

[Ryan Lahfa]

Wow, I don't see very well what's the difference, @Kevin Buzzard

[Ryan Lahfa]

(@Kevin Buzzard I agree, you've already told me this :D! But I'm not allowed to change those :D)

[Kevin Buzzard]

I guess you just made some syntax error in the second example -- no :=?

[Ryan Lahfa]

… indeed.

[Ryan Lahfa]

The error is a bit cryptic though

[Kevin Buzzard]

There used to be a comment on the official Lean github repo saying something like "we will close issues complaining that error messages are confusing"

[Ryan Lahfa]

While I'm on the subject of quotients, is there a way to transfer a map f : (a_1 a_2 … a_n: cauchy_seqs X) → Y into a f' : (a_1 … a_n: completion X) → Y?

[Reid Barton]

quotient.lift?

[Ryan Lahfa]

it sounded like quotient.lift takes a f : α → β,

[Reid Barton]

Oh I see.

[Reid Barton]

Well you can't have …, but I think there is a version for 2 arguments at least and you can look at how that works.

[Ryan Lahfa]

I tried lift_2, and it's complaining about synthesizing:

failed to synthesize type class instance for
T : Type,
_inst_1 : metric_space T,
x y : completion T
⊢ setoid (cauchy_seqs T)

For full example:

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }


def cauchy.setoid (X : Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := sorry,
  iseqv := sorry
}
-- Définit la distance entre 2 suites de Cauchy par lim d(x_n, y_n).
def cauchy.dist (T: Type*) [metric_space T] (x y: cauchy_seqs T): ℝ
  := sorry -- some cauchy limit stuff.

def completion (X : Type*) [metric_space X] : Type* := quotient (cauchy.setoid X)
def completion.dist (T: Type*) [metric_space T] (x y: completion T): ℝ :=
  quotient.lift₂ (cauchy.dist T) x y

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := sorry,
  d_pos := sorry,
  -- etc
}

end test

completion.dist has errors

[Reid Barton]

Okay, because your completion is not an instance. To be honest, this whole type class design with quotient is pretty dubious.
Is there a lift\2' that uses a {} argument for the setoid?

[Ryan Lahfa]

Reid Barton said:

Okay, because your completion is not an instance. To be honest, this whole type class design with quotient is pretty dubious.
Is there a lift\2' that uses a {} argument for the setoid?

I can turn it into an instance, but I heard/read here that most of the time quotients need not to be instances, I don't really understand why (but I guess there must be a good reason)

[Ryan Lahfa]

As far as I see it, in quot.lean, there's no {…}

[Ryan Lahfa]

for setoids.

[Patrick Massot]

There is nothing specific about quotient, the question is: do you want multiple instances on the same type?

[Patrick Massot]

If yes then there will be trouble.

[Patrick Massot]

The link with quotients is that this issue comes up for instance with setoid on Z (you want several quotients of Z)

[Reid Barton]

Since you defined your own cauchy_seqs type and the setoid only depends on other stuff available through instances, it would be fine (and easiest) to make it an instance in this case.

[Ryan Lahfa]

I don't think I'm going to have an instance of something else than a metric space for the Cauchy sequences quotient by $\lim_n d(x_n, y_n)$ AFAIK.

[Ryan Lahfa]

Alright, will do :)

[Kenny Lau]

I think the last time I asked, Mario told me that arbitrary lifting is independent of Lean

[Kenny Lau]

at least the computable one

[Kenny Lau]

but finite lifting should be doable by induction

[Ryan Lahfa]

Also, when I have x ~ y, how can I get the underlying property?
Like I have x ~ y <=> dist x y = 0, how can I derive dist x y = 0 in this situation?

[Kevin Buzzard]

Is it rfl?

[Kenny Lau]

#mwe

[Ryan Lahfa]

@Kenny Lau :P
I'll provide a MWE

[Ryan Lahfa]

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }


instance cauchy.setoid (X : Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := sorry,
  iseqv := sorry
}
local attribute [instance] cauchy.setoid
def cauchy.dist (T: Type*) [metric_space T] (x y: cauchy_seqs T): ℝ
  := sorry -- some cauchy limit stuff.

def completion (X : Type*) [metric_space X] : Type* := quotient (cauchy.setoid X)

def completion.dist_soundness (T: Type*) [metric_space T]:
  ∀ x₁ x₂: cauchy_seqs T, ∀ y₁ y₂: cauchy_seqs T, (x₁ ≈ y₁) → (x₂ ≈ y₂) → (cauchy.dist T x₁ x₂ = cauchy.dist T y₁ y₂) := begin
  intros x y z t Hxz Hyt,
  -- what to do with Hxz, Hyt? I want cauchy.dist x z = 0 to rewrite them and conclude by refl.
end
def completion.dist (T: Type*) [metric_space T] (x y: completion T): ℝ :=
  quotient.lift₂ (cauchy.dist T) (completion.dist_soundness T) x y

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := completion.dist X,
  d_pos := sorry,
  -- etc
}

end test

[Ryan Lahfa]

@Kenny Lau @Kevin Buzzard Here's a MWE, I'm not sure how to use rfl to be able to rewrite the goal using Hxz, Hyz?

[Kevin Buzzard]

Wait -- you cannot do anything at all with x₁ ≈ y₁ because this means r x₁ y₁ and your definition of r is sorry.

[Ryan Lahfa]

ah, let me edit it

[Kevin Buzzard]

I think that x₁ ≈ y₁ is definitionally equal to r x₁ y₁ and hence to whatever you define it to be.

[Kevin Buzzard]

You should just be able to use the change tactic to change something to anything definitionally equivalent to it.

[Ryan Lahfa]

Alright, will give it a try

[Ryan Lahfa]

Hmm, not sure how to use it here:

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

instance real.metric_space: metric_space ℝ :=
 { d := sorry, d_pos := sorry, presep := sorry, sep := sorry,
sym := sorry, triangle := sorry }
open_locale classical
noncomputable theory
section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)
def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)
def complete (T: Type) [metric_space T] := ∀ x : ℕ → T, is_cauchy x → ∃ l : T, converge x l

lemma R_is_complete: complete ℝ := sorry

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }
def cauchy.diff (x : ℕ → X) (y : ℕ → X) : ℕ → ℝ  :=
 λ n : ℕ, d (x n) (y n)
def cauchy.cauchy_of_diff (x y : ℕ →  X) (h1 : is_cauchy x) (h2 : is_cauchy y):
  is_cauchy (cauchy.diff x y) := sorry

def cauchy.limit (x: ℕ → ℝ) (H: is_cauchy x): ℝ := classical.some (R_is_complete x H)
def cauchy.dist (T: Type*) [metric_space T] (x y: cauchy_seqs T): ℝ
  := cauchy.limit (cauchy.diff x.val y.val) (cauchy.cauchy_of_diff x.val y.val x.property y.property)

instance cauchy.setoid (X : Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := sorry,
  iseqv := sorry
}
local attribute [instance] cauchy.setoid

def completion (X : Type*) [metric_space X] : Type* := quotient (cauchy.setoid X)

def completion.dist_soundness (T: Type*) [metric_space T]:
  ∀ x₁ x₂: cauchy_seqs T, ∀ y₁ y₂: cauchy_seqs T, (x₁ ≈ y₁) → (x₂ ≈ y₂) → (cauchy.dist T x₁ x₂ = cauchy.dist T y₁ y₂) := begin
  intros x y z t Hxz Hyt,
  change (x ≈ z) with (cauchy.dist T x z = 0) at Hxz,
  -- what to do with Hxz, Hyt?
end
def completion.dist (T: Type*) [metric_space T] (x y: completion T): ℝ :=
  quotient.lift₂ (cauchy.dist T) (completion.dist_soundness T) x y

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := completion.dist X,
  d_pos := sorry,
  -- etc
}

end test

[Patrick Massot]

@Ryan Lahfa nothing can help you if you keep sorried data and hope Lean will see it's defeq to what you wish

[Ryan Lahfa]

Patrick Massot said:

Ryan Lahfa nothing can help you if you keep sorried data and hope Lean will see it's defeq to what you wish

I have it fully, but it's quite long :/

[Patrick Massot]

here the relation in cauchy.setoid is sorried

[Ryan Lahfa]

Oops, you're right

[Ryan Lahfa]

It works \o/ thanks a lot @Patrick Massot @Kevin Buzzard !

[Ryan Lahfa]

But… I have still a little issue with change, it appears like my second change has no effect and no errors:

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

instance real.metric_space: metric_space ℝ :=
 { d := sorry, d_pos := sorry, presep := sorry, sep := sorry,
sym := sorry, triangle := sorry }
open_locale classical
noncomputable theory
section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)
def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)
def complete (T: Type) [metric_space T] := ∀ x : ℕ → T, is_cauchy x → ∃ l : T, converge x l

lemma R_is_complete: complete ℝ := sorry

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }
def cauchy.diff (x : ℕ → X) (y : ℕ → X) : ℕ → ℝ  :=
 λ n : ℕ, d (x n) (y n)
def cauchy.cauchy_of_diff (x y : ℕ →  X) (h1 : is_cauchy x) (h2 : is_cauchy y):
  is_cauchy (cauchy.diff x y) := sorry

def cauchy.limit (x: ℕ → ℝ) (H: is_cauchy x): ℝ := classical.some (R_is_complete x H)
def cauchy.dist (T: Type*) [metric_space T] (x y: cauchy_seqs T): ℝ
  := cauchy.limit (cauchy.diff x.val y.val) (cauchy.cauchy_of_diff x.val y.val x.property y.property)

def cauchy.cong (T: Type*) [metric_space T] (x y: cauchy_seqs T): Prop := cauchy.dist T x y = 0
instance cauchy.setoid (X : Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := cauchy.cong X,
  iseqv := sorry
}
local attribute [instance] cauchy.setoid

def completion (X : Type*) [metric_space X] : Type* := quotient (cauchy.setoid X)

def completion.dist_soundness (T: Type*) [metric_space T]:
  ∀ x₁ x₂: cauchy_seqs T, ∀ y₁ y₂: cauchy_seqs T, (x₁ ≈ y₁) → (x₂ ≈ y₂) → (cauchy.dist T x₁ x₂ = cauchy.dist T y₁ y₂) := begin
  intros x y z t Hxz Hyt,
  change (x ≈ z) with (cauchy.dist T x z = 0) at Hxz,
  change (y ≈ t) with (cauchy.dist T y t = 0) at Hyt,
  apply le_antisymm,
  calc
    cauchy.dist T x y ≤ cauchy.dist T x z + cauchy.dist T z t + cauchy.dist T t y : sorry
    ... = cauchy.dist T z t + cauchy.dist T t y : by rw Hxz
    ... = cauchy.dist T z t + cauchy.dist T y t : sorry -- symmetry
    ... = cauchy.dist T z t : sorry,
  calc
    cauchy.dist T z t ≤ cauchy.dist T z x + cauchy.dist T x y + cauchy.dist T y t : sorry
    ... = cauchy.dist T x z + cauchy.dist T x y : sorry
    ... = cauchy.dist T x y : sorry,
end
def completion.dist (T: Type*) [metric_space T] (x y: completion T): ℝ :=
  quotient.lift₂ (cauchy.dist T) (completion.dist_soundness T) x y

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := completion.dist X,
  d_pos := sorry,
  -- etc
}

end test

[Ryan Lahfa]

Hyt stays the same

[Ryan Lahfa]

I triple-checked and I don't think I'm doing something stupid

[Reid Barton]

I don't know specifically why it doesn't work, but just use change cauchy.dist T y t = 0 at Hyt since you are changeing the whole type.

[Ryan Lahfa]

Alright!

[Ryan Lahfa]

It works fine, this way @Reid Barton thanks!

[Reid Barton]

I actually only learned about change ... with a couple weeks ago, I think.

[Kevin Buzzard]

related: change' ... with

[Ryan Lahfa]

And here I come back with a complex issue because I cannot reproduce it as a MWE:

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)
class premetric_space (X : Type*) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

instance real.metric_space: metric_space ℝ :=
 { d := sorry, d_pos := sorry, presep := sorry, sep := sorry,
sym := sorry, triangle := sorry }
open_locale classical
noncomputable theory
section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)
def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)
def complete (T: Type) [metric_space T] := ∀ x : ℕ → T, is_cauchy x → ∃ l : T, converge x l

lemma R_is_complete: complete ℝ := sorry

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }
def cauchy.diff (x : ℕ → X) (y : ℕ → X) : ℕ → ℝ  :=
 λ n : ℕ, d (x n) (y n)
def cauchy.cauchy_of_diff (x y : ℕ →  X) (h1 : is_cauchy x) (h2 : is_cauchy y):
  is_cauchy (cauchy.diff x y) := sorry

def cauchy.limit (x: ℕ → ℝ) (H: is_cauchy x): ℝ := classical.some (R_is_complete x H)
def cauchy.dist (T: Type*) [metric_space T] (x y: cauchy_seqs T): ℝ
  := cauchy.limit (cauchy.diff x.val y.val) (cauchy.cauchy_of_diff x.val y.val x.property y.property)


instance pre_ecart.premetrique (X: Type*) [metric_space X]: premetric_space (cauchy_seqs X) :=
{ d := cauchy.dist X,
  d_pos := sorry,
  presep := sorry,
  sym := sorry,
  triangle := sorry }

def cauchy.cong (T: Type*) [metric_space T] (x y: cauchy_seqs T): Prop := cauchy.dist T x y = 0
instance cauchy.setoid (X : Type*) [metric_space X] : setoid (cauchy_seqs X) :=
{
  r := cauchy.cong X,
  iseqv := sorry
}
local attribute [instance] cauchy.setoid

def completion (X : Type*) [metric_space X] : Type* := quotient (cauchy.setoid X)

def completion.dist_soundness (T: Type*) [metric_space T]:
  ∀ x₁ x₂: cauchy_seqs T, ∀ y₁ y₂: cauchy_seqs T, (x₁ ≈ y₁) → (x₂ ≈ y₂) → (cauchy.dist T x₁ x₂ = cauchy.dist T y₁ y₂) := begin
  intros x y z t Hxz Hyt,
  change (cauchy.dist T x z = 0) at Hxz,
  change (cauchy.dist T y t = 0) at Hyt,
  apply le_antisymm,
  calc
    cauchy.dist T x y ≤ cauchy.dist T x z + cauchy.dist T z y : premetric_space.triangle x z y
    ... ≤ cauchy.dist T x z + (cauchy.dist T z t + cauchy.dist T t y) : add_le_add_left (premetric_space.triangle z t y) _ --
    ... = cauchy.dist T z t + cauchy.dist T y t : by rw [Hxz, zero_add, premetric_space.sym t y] -- the last rewrite don't work
    ... = cauchy.dist T z t : by rw Hyt,
  calc
    cauchy.dist T z t ≤ cauchy.dist T z x + cauchy.dist T x t : premetric_space.triangle z x t
    ... ≤ cauchy.dist T z x + (cauchy.dist T x y + cauchy.dist T y t) : add_le_add_left (premetric_space.triangle x y t) _
    ... = cauchy.dist T x z + cauchy.dist T x y : by rw [Hyt, add_zero, premetric_space.sym z x] -- the last rewrite don't work
    ... = cauchy.dist T x y : by rw Hxz,
end

def completion.dist (T: Type*) [metric_space T] (x y: completion T): ℝ :=
  quotient.lift₂ (cauchy.dist T) (completion.dist_soundness T) x y

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := completion.dist X,
  d_pos := sorry,
  -- etc
}

end test

Here's the expected MWE, it type check and work, but at the place where I've put comments, in my big code, it does not work, it complains about:

rewrite tactic failed, did not find instance of the pattern in the target expression
  premetric_space.d t y
state:
T : Type,
_inst_4 : metric_space T,
x y z t : cauchy_seqs T,
Hxz : cauchy.dist T x z = 0,
Hyt : cauchy.dist T y t = 0
⊢ cauchy.dist T z t + cauchy.dist T t y = cauchy.dist T z t + cauchy.dist T y t
state:
2 goals
T : Type,
_inst_4 : metric_space T,
x y z t : cauchy_seqs T,
Hxz : cauchy.dist T x z = 0,
Hyt : cauchy.dist T y t = 0
⊢ cauchy.dist T x y ≤ cauchy.dist T z t

T : Type,
_inst_4 : metric_space T,
x y z t : cauchy_seqs T,
Hxz : cauchy.dist T x z = 0,
Hyt : cauchy.dist T y t = 0
⊢ cauchy.dist T z t ≤ cauchy.dist T x y

I don't know if there's way to tell him: please use my instance on premetric spaces, which has the good definition of d (?)

[Kenny Lau]

0/10 this is real not complex

[Kenny Lau]

aha, this is an API issue

[Ryan Lahfa]

Kenny Lau said:

aha, this is an API issue

What do you mean?

[Ryan Lahfa]

Kenny Lau said:

0/10 this is real not complex

:-D

[Kenny Lau]

MWE:

import data.real.basic
class metric_space (X : Type*) :=
(d : X → X → ℝ)
class premetric_space (X : Type*) :=
(d : X → X → ℝ)
(sym : ∀ x y, d x y = d y x)

open_locale classical
noncomputable theory

section test
open metric_space
variables {X: Type*} [metric_space X]

def is_cauchy (x: ℕ → X) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, ((d (x p) (x q)) < ε)

def cauchy_seqs (X : Type*) [metric_space X] := { f : ℕ → X // is_cauchy f }

def cauchy.dist (T: Type*) [metric_space T] (x y: cauchy_seqs T) : ℝ := sorry

instance pre_ecart.premetrique (X: Type*) [metric_space X]: premetric_space (cauchy_seqs X) :=
{ d := cauchy.dist X,
  sym := sorry }

example (T : Type*) [metric_space T] (x y : cauchy_seqs T) :
  cauchy.dist T x y = cauchy.dist T y x :=
by rw premetric_space.sym x y -- fails

end test

[Kenny Lau]

so there are two solutions

[Ryan Lahfa]

I listen carefully

[Kenny Lau]

1. use premetric_space.d x y instead of cauchy.dist T x y

[Kenny Lau]

2. prove cauchy.dist T x y = cauchy.dist T y x immediately after declaring the instance

[Kenny Lau]

(the proof is just premetric_space.sym this time)

[Ryan Lahfa]

can I even do that because premetric_space depends on some metricspace?

[Kenny Lau]

Lean will infer it

[Ryan Lahfa]

Okay, will try 1, then will fallback to 2, @Kenny Lau thanks a lot.
A more abstract question, if we take back my MWE:

def completion.dist (T: Type*) [metric_space T] (x y: completion T): ℝ :=
  quotient.lift₂ (cauchy.dist T) (completion.dist_soundness T) x y

Precisely this, when I have some assumption: completion.dist T x y = 0, how can I turn it into something more usable?
What I've done is turn back x y into [[X], [[Y]] (using exists_rep, sound) and then, can I somehow say that I have cauchy.dist T X Y = 0 ?

[Kenny Lau]

@Mario Carneiro is 1 or 2 better?

[Ryan Lahfa]

1 worked fine

[Kenny Lau]

doesn't mean it's better

[Kenny Lau]

instance completion.metric_space (X: Type*) [metric_space X]: metric_space (completion X) :=
{
  d := completion.dist X,
  d_pos := λ x y, quotient.induction_on₂ x y $ λ Y Z, show cauchy.dist X Y Z ≥ 0, from sorry,
  -- etc
}

[Kenny Lau]

use induction_on instead of exists_rep

[Ryan Lahfa]

Thanks a lot

[Mario Carneiro]

Doesn't mathlib use dist for this?

[Mario Carneiro]

There is a definition dist which just unwraps metric_space.dist, and rather than cauchy.dist or premetric_space.d you should be using dist

[Kenny Lau]

aha, the third solution

[Ryan Lahfa]

@Mario Carneiro I'm rebuilding this as an exercise, so I'm not sure what you're suggesting is not just reusing mathlib, which I cannot

[Mario Carneiro]

That's fine, then just rebuild dist too

[Ryan Lahfa]

Is there some file or pointer where to look?

[Mario Carneiro]

https://github.com/leanprover-community/mathlib/blob/master/src/topology/metric_space/premetric_space.lean

[Mario Carneiro]

It looks like has_dist has been broken off as its own typeclass

[Mario Carneiro]

https://github.com/leanprover-community/mathlib/blob/master/src/topology/metric_space/basic.lean#L46

[Ryan Lahfa]

Okay, so has_XXX technique, thanks

[Ryan Lahfa]

@Kenny Lau I just didn't understand something on induction_on2

[Ryan Lahfa]

When you pass the hypothesis: for all x, y: cauchy_seqs, I can prove cauchy.dist X Y Z ≥ 0, why does it "coerce" to completion.dist ?

[Ryan Lahfa]

i mean like, does cauchy.dist X Y Z ≥ 0 → completion.dist X [Y] [Z] ≥ 0 automatically?

[Kenny Lau]

completion.dist X [Y] [Z] is defeq to cauchy.dist X Y Z

[Kenny Lau]

because of definitional equalities involving quotient.lift

[Ryan Lahfa]

okay, nice it makes it super clear, last question, @Kenny Lau how can I prove X \~~ Y or [X] = [Y] knowing that I can prove that cauchy.dist X Y = 0 (which is exactly the def of the relation)?

[Kenny Lau]

quotient.sound

[Ryan Lahfa]

well
cauchy.dist X Y = 0 is defeq X ~~Y I guess

[Ryan Lahfa]

yes, I used quot.sound and some hypothesis and it just worked ™, thx a lot

[Ryan Lahfa]

@Kenny Lau is there a induction_on3 ? :D

[Ryan Lahfa]

Oh there is !