# Zulip Chat Archive

## 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 ?
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 (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 `:=`

?

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

… 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 : α → β`

,

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

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 `{…}`

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

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`

?

#### Kenny Lau (May 10 2020 at 16:45):

#### 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 `change`

ing the whole type.

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

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):

- use
`premetric_space.d x y`

instead of`cauchy.dist T x y`

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

- 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?

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

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`

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

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):

#### 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