## Stream: maths

### Topic: Quotients & synthesizing

#### Ryan Lahfa (May 10 2020 at 14:18):

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 ?
/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 (May 10 2020 at 14:24):

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 (May 10 2020 at 14:26):

Oh you got that far

#### Ryan Lahfa (May 10 2020 at 14:27):

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 (May 10 2020 at 14:33):

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 (May 10 2020 at 14:38):

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 (May 10 2020 at 14:38):

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

#### Ryan Lahfa (May 10 2020 at 14:38):

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

#### Kevin Buzzard (May 10 2020 at 14:39):

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

… indeed.

#### Ryan Lahfa (May 10 2020 at 14:41):

The error is a bit cryptic though

#### Kevin Buzzard (May 10 2020 at 14:44):

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 (May 10 2020 at 15:04):

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 (May 10 2020 at 15:07):

quotient.lift?

#### Ryan Lahfa (May 10 2020 at 15:10):

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

Oh I see.

#### Reid Barton (May 10 2020 at 15:11):

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 (May 10 2020 at 15:14):

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 (May 10 2020 at 15:16):

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 (May 10 2020 at 15:17):

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 (May 10 2020 at 15:18):

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

for setoids.

#### Patrick Massot (May 10 2020 at 15:18):

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

#### Patrick Massot (May 10 2020 at 15:18):

If yes then there will be trouble.

#### Patrick Massot (May 10 2020 at 15:19):

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

#### Reid Barton (May 10 2020 at 15:20):

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 (May 10 2020 at 15:20):

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 (May 10 2020 at 15:20):

Alright, will do :)

#### Kenny Lau (May 10 2020 at 15:21):

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

#### Kenny Lau (May 10 2020 at 15:21):

at least the computable one

#### Kenny Lau (May 10 2020 at 15:21):

but finite lifting should be doable by induction

#### Ryan Lahfa (May 10 2020 at 16:38):

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 (May 10 2020 at 16:38):

Is it rfl?

#mwe

#### Ryan Lahfa (May 10 2020 at 16:47):

@Kenny Lau :P
I'll provide a MWE

#### Ryan Lahfa (May 10 2020 at 16:57):

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 (May 10 2020 at 16:57):

@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 (May 10 2020 at 17:15):

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 (May 10 2020 at 17:15):

ah, let me edit it

#### Kevin Buzzard (May 10 2020 at 17:16):

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

#### Kevin Buzzard (May 10 2020 at 17:17):

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

#### Ryan Lahfa (May 10 2020 at 17:22):

Alright, will give it a try

#### Ryan Lahfa (May 10 2020 at 17:28):

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 (May 10 2020 at 17:38):

@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 (May 10 2020 at 17:39):

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 (May 10 2020 at 17:39):

here the relation in cauchy.setoid is sorried

#### Ryan Lahfa (May 10 2020 at 17:39):

Oops, you're right

#### Ryan Lahfa (May 10 2020 at 17:40):

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

#### Ryan Lahfa (May 10 2020 at 17:50):

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 (May 10 2020 at 17:50):

Hyt stays the same

#### Ryan Lahfa (May 10 2020 at 17:51):

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

#### Reid Barton (May 10 2020 at 18:16):

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.

Alright!

#### Ryan Lahfa (May 10 2020 at 18:19):

It works fine, this way @Reid Barton thanks!

#### Reid Barton (May 10 2020 at 18:20):

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

#### Kevin Buzzard (May 10 2020 at 18:26):

related: change' ... with

#### Ryan Lahfa (May 10 2020 at 21:58):

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 (May 10 2020 at 21:59):

0/10 this is real not complex

#### Kenny Lau (May 10 2020 at 22:04):

aha, this is an API issue

#### Ryan Lahfa (May 10 2020 at 22:06):

Kenny Lau said:

aha, this is an API issue

What do you mean?

#### Ryan Lahfa (May 10 2020 at 22:06):

Kenny Lau said:

0/10 this is real not complex

:-D

#### Kenny Lau (May 10 2020 at 22:08):

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 (May 10 2020 at 22:08):

so there are two solutions

#### Ryan Lahfa (May 10 2020 at 22:09):

I listen carefully

#### Kenny Lau (May 10 2020 at 22:09):

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

#### Kenny Lau (May 10 2020 at 22:10):

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

#### Kenny Lau (May 10 2020 at 22:10):

(the proof is just premetric_space.sym this time)

#### Ryan Lahfa (May 10 2020 at 22:10):

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

#### Kenny Lau (May 10 2020 at 22:10):

Lean will infer it

#### Ryan Lahfa (May 10 2020 at 22:12):

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 (May 10 2020 at 22:12):

@Mario Carneiro is 1 or 2 better?

1 worked fine

#### Kenny Lau (May 10 2020 at 22:15):

doesn't mean it's better

#### Kenny Lau (May 10 2020 at 22:15):

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 (May 10 2020 at 22:15):

use induction_on instead of exists_rep

Thanks a lot

#### Mario Carneiro (May 10 2020 at 22:16):

Doesn't mathlib use dist for this?

#### Mario Carneiro (May 10 2020 at 22:17):

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 (May 10 2020 at 22:17):

aha, the third solution

#### Ryan Lahfa (May 10 2020 at 22:17):

@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 (May 10 2020 at 22:18):

That's fine, then just rebuild dist too

#### Ryan Lahfa (May 10 2020 at 22:18):

Is there some file or pointer where to look?

#### Mario Carneiro (May 10 2020 at 22:19):

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

#### Mario Carneiro (May 10 2020 at 22:20):

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

#### Mario Carneiro (May 10 2020 at 22:20):

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

#### Ryan Lahfa (May 10 2020 at 22:21):

Okay, so has_XXX technique, thanks

#### Ryan Lahfa (May 10 2020 at 22:22):

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

#### Ryan Lahfa (May 10 2020 at 22:23):

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 (May 10 2020 at 22:23):

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

#### Kenny Lau (May 10 2020 at 22:26):

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

#### Kenny Lau (May 10 2020 at 22:26):

because of definitional equalities involving quotient.lift

#### Ryan Lahfa (May 10 2020 at 22:27):

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 (May 10 2020 at 22:27):

quotient.sound

#### Ryan Lahfa (May 10 2020 at 22:27):

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

#### Ryan Lahfa (May 10 2020 at 22:28):

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

#### Ryan Lahfa (May 10 2020 at 22:32):

@Kenny Lau is there a induction_on3 ? :D

#### Ryan Lahfa (May 10 2020 at 22:32):

Oh there is !

Last updated: May 12 2021 at 07:17 UTC