Zulip Chat Archive

Stream: maths

Topic: Quotients & synthesizing


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

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 14:26):

Oh you got that far

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

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

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:38):

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

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 14:39):

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:40):

… indeed.

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:41):

The error is a bit cryptic though

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

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

view this post on Zulip Reid Barton (May 10 2020 at 15:07):

quotient.lift?

view this post on Zulip Ryan Lahfa (May 10 2020 at 15:10):

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

view this post on Zulip Reid Barton (May 10 2020 at 15:11):

Oh I see.

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

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

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

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 15:18):

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 15:18):

for setoids.

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

view this post on Zulip Patrick Massot (May 10 2020 at 15:18):

If yes then there will be trouble.

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

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

view this post on Zulip 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 limnd(xn,yn)\lim_n d(x_n, y_n) AFAIK.

view this post on Zulip Ryan Lahfa (May 10 2020 at 15:20):

Alright, will do :)

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

view this post on Zulip Kenny Lau (May 10 2020 at 15:21):

at least the computable one

view this post on Zulip Kenny Lau (May 10 2020 at 15:21):

but finite lifting should be doable by induction

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 16:38):

Is it rfl?

view this post on Zulip Kenny Lau (May 10 2020 at 16:45):

#mwe

view this post on Zulip Ryan Lahfa (May 10 2020 at 16:47):

@Kenny Lau :P
I'll provide a MWE

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

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

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 17:15):

ah, let me edit it

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

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 17:22):

Alright, will give it a try

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

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

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

view this post on Zulip Patrick Massot (May 10 2020 at 17:39):

here the relation in cauchy.setoid is sorried

view this post on Zulip Ryan Lahfa (May 10 2020 at 17:39):

Oops, you're right

view this post on Zulip Ryan Lahfa (May 10 2020 at 17:40):

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

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 17:50):

Hyt stays the same

view this post on Zulip Ryan Lahfa (May 10 2020 at 17:51):

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

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 18:18):

Alright!

view this post on Zulip Ryan Lahfa (May 10 2020 at 18:19):

It works fine, this way @Reid Barton thanks!

view this post on Zulip Reid Barton (May 10 2020 at 18:20):

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 18:26):

related: change' ... with

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

view this post on Zulip Kenny Lau (May 10 2020 at 21:59):

0/10 this is real not complex

view this post on Zulip Kenny Lau (May 10 2020 at 22:04):

aha, this is an API issue

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:06):

Kenny Lau said:

aha, this is an API issue

What do you mean?

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:06):

Kenny Lau said:

0/10 this is real not complex

:-D

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:08):

so there are two solutions

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:09):

I listen carefully

view this post on Zulip Kenny Lau (May 10 2020 at 22:09):

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

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:10):

(the proof is just premetric_space.sym this time)

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:10):

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:10):

Lean will infer it

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:12):

@Mario Carneiro is 1 or 2 better?

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:14):

1 worked fine

view this post on Zulip Kenny Lau (May 10 2020 at 22:15):

doesn't mean it's better

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:15):

use induction_on instead of exists_rep

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:15):

Thanks a lot

view this post on Zulip Mario Carneiro (May 10 2020 at 22:16):

Doesn't mathlib use dist for this?

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:17):

aha, the third solution

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:18):

That's fine, then just rebuild dist too

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:18):

Is there some file or pointer where to look?

view this post on Zulip Mario Carneiro (May 10 2020 at 22:19):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:20):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:20):

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:21):

Okay, so has_XXX technique, thanks

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:22):

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

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

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:26):

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:26):

because of definitional equalities involving quotient.lift

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:27):

quotient.sound

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:27):

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:28):

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

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:32):

@Kenny Lau is there a induction_on3 ? :D

view this post on Zulip Ryan Lahfa (May 10 2020 at 22:32):

Oh there is !


Last updated: May 12 2021 at 07:17 UTC