LEAN help?

Stream: general

[Aron]

I'm a green undergrad and I'm having trouble with the syntax and the import statements. I'm trying to write this problem up:
Given two Cauchy sequences c,c' on a metric space (X,d), the sequence x_n=d(c_n,c'_n) is Cauchy.
I've gotten to:

import topology.metric_space.basic.metric_space
theorem prb1 (X metric_space)(???)... :???:=

It doesn't seem to recognize metric_space as a type. I know I'll also need topology.uniformspace.cauchy_seq.
I'm not looking for a proof of this, I just need help formalizing the problem.

[Patrick Massot]

You probably need to read a bit more documentation before trying this, since your (X metric_space) is pretty far from the correct syntax. What did you read so far?

[Patrick Massot]

Maybe watch https://www.youtube.com/watch?v=xYenPIeX6MY&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N&index=8 and next few videos in this series if you prefer videos to reading.

[Aron]

I'm honestly having a pretty tough time parsing it. I'm not well-versed in dep type theory.
I've been looking over example LEAN files instead.
I noticed I've forgotten colons, now I'm at:

theorem prb1 (X : metric_space)(c c' : cauchy_seq X)... :???:=

[Patrick Massot]

(this is number 8 in a series, you should have a look at 8, 9, 10, 11, assuming you already know more basic things)

[Patrick Massot]

The first easy thing to fix is to write Lean instead of LEAN :wink:

[Heather Macbeth]

I actually think it's not so bad to just dive in, the way that Aron is doing. Here's a starting point:

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

def my_cauchy (c : ℕ → X) := sorry

example (c c' : ℕ → X) (hc : my_cauchy c) (hc' : my_cauchy c') : my_cauchy (λ n, dist (c n) (c' n)) := sorry

[Heather Macbeth]

Note that I am suggesting you make your own definition my_cauchy, because the existing definition docs#cauchy in mathlib is very general (for filters).

[Heather Macbeth]

But the videos Patrick linked are definitely also worth your time, especially as a complement to some fun hours of blind experimentation! :)

[Patrick Massot]

I wouldn't be too worried about the generality of Cauchy in mathlib. You can get rid of it using metric.cauchy_seq_iff or metric.cauchy_seq_iff'. So you can start with

import topology.metric_space.basic

theorem prb1 {X : Type*} [metric_space X] {c c' : ℕ → X} (hc : cauchy_seq c)
(hc' : cauchy_seq c') : cauchy_seq (λ n, dist (c n) (c' n)) :=
begin
  rw metric.cauchy_seq_iff at *,
  sorry
end

But I still think that trying this without knowing how to write "Let X be a metric space" in Lean will probably be very frustrating, so learning a bit first is wiser.

[Aron]

Thanks, both of those look good to me. I think dist is a little strange, I'm not sure why that wouldn't collide if one were to make two metspaces.

[Heather Macbeth]

Aron said:

I think dist is a little strange, I'm not sure why that wouldn't collide if one were to make two metspaces.

This is just part of the magic. Lean looks at the object you're trying to apply dist to, sees that it's of type X, and therefore applies the definition of dist coming from the metric space structure on X, rather than any of the other metric spaces that might be around.

[Aron]

Oh, that's pretty neat.

[Aron]

I noticed the definition for a Cauchy sequence is the open ball definition in my book, and now I'm trying to encode that.

def my_cauchy {X : Type*} (c : ℕ → X):=∀ (ε : ℝ), ε > 0 → (∃ (n : ℕ),∃ (x ∈ X),∀ (m : ℕ), m ≥ n → dist (c m) (x) < ε)

Where am I going wrong here?

[Heather Macbeth]

Can you describe the error you receive?

[Heather Macbeth]

And please make sure to include any necessary hypotheses, so that someone who wants to help can test the code. For example did you earlier define X to be a metric space?

[Aron]

import topology.metric_space.basic topology.uniform_space.basic

def my_cauchy {X : Type*} (c : ℕ → X):=∀ (ε : ℝ), ε > 0 → (∃ (n : ℕ),∃ (x ∈ X),∀ (m : ℕ), m ≥ n → dist (c m) (x) < ε)
theorem prb1 {X : Type*} {c c' : ℕ → X} (hX: metric_space X)(hc : cauchy_seq c) (hc' : cauchy_seq c') : cauchy_seq (λ n, dist (c n) (c' n)) :=
begin
  rw metric.cauchy_seq_iff at *,
  sorry
end

I intend on replacing cauchy_seq in the theorem preamble.

3:98: error:
failed to synthesize type class instance for
X : Type ?,
c : ℕ → X,
ε : ℝ,
a : ε > 0,
n : ℕ,
x : X,
H : x ∈ X,
m : ℕ,
a : m ≥ n
⊢ has_dist X
3:0: error:
failed to synthesize type class instance for
X : Type ?,
c : ℕ → X,
ε : ℝ,
a : ε > 0,
n : ℕ,
x : X
⊢ has_mem X (Type ?)

[Heather Macbeth]

Yep, so first problem is that you haven't told Lean that X is a metric space.

[Heather Macbeth]

That's why it can't find a has_dist on X. You seem to have taken Patrick's code but omitted the important hypothesis [metric_space X].

[Aron]

Put it in, now only the second error remains. Apparently has_mem isn't implied by X being a metspace?
def my_cauchy {X : Type*} [metric_space X] (c : ℕ → X):=∀ (ε : ℝ), ε > 0 → (∃ (n : ℕ),∃ (x ∈ X),∀ (m : ℕ), m ≥ n → dist (c m) (x) < ε)

[Heather Macbeth]

That's right, because X is a type, not a set. You should write, ∃ (x : X) rather than ∃ (x ∈ X).

[Heather Macbeth]

A couple of other points: you can say ∀ ε > 0, as an abbreviation for ∀ (ε : ℝ), ε > 0 →, likewise for ∀ (m : ℕ), m ≥ n → .

[Heather Macbeth]

And ... are you sure you have the right definition of Cauchy? :)

[Aron]

All works now.
I'm pretty sure I have the right def of Cauchy:
A sequence is Cauchy iff for all r>0, there is an x in the metspace such that the sequence is eventually in B(x,r). I expand a bit on the definitions to get that.

[Kevin Buzzard]

That's not the definition of Cauchy! Which book are you using?

[Kevin Buzzard]

Well, it's certainly not the standard definition of Cauchy...

[Heather Macbeth]

Sorry Aron, I guess it is equivalent to the standard definition. Just looks weird! I'm also curious about what book your professor is using!

[Kevin Buzzard]

It would be an interesting Lean exercise to prove that this definition of Cauchy was equivalent to the definition in Wikipedia, which is certainly the one I was taught as an undergraduate and the one we teach here

[Aron]

Not really a book, it's my prof's pdfs. I'm pretty sure he writes them on the fly.
The man loves his nets, so his definition of Cauchy is defined for nets too.
"A net x taking values in (X,d) is a Cauchy net iff for all r>0, there exists a point z in X such that x is evt.ly in B(z,r)"

[Aron]

I can kind of see how it's interchangeable with the lean def, if in the lean def m and n are too far apart, one must necessarily be outside the open ball.

[Heather Macbeth]

To be clear, here "Lean def" = "standard def for 99% of mathematicians" :)

[Kevin Buzzard]

Well you have a chance to prove that you can see how it's interchangeable because this is exactly a level of the lean puzzle game

[Aron]

Oh, cool.

[Kevin Buzzard]

Can you make the level?

[Aron]

You said this is one of the levels, I don't think I'm up to snuff to design the level.

[Heather Macbeth]

Your mission, if you choose to accept it :)

import topology.metric_space.basic

variables {X : Type*} [metric_space X]

def my_cauchy (c : ℕ → X) := ∀ ε > 0, ∃ n : ℕ, ∃ x : X, ∀ m ≥ n, dist (c m) x < ε

example (c : ℕ → X) :
  my_cauchy c ↔ ∀ ε > 0, ∃ n : ℕ, ∀ m₁ ≥ n, ∀ m₂ ≥ n, dist (c m₁) (c m₂) < ε :=
begin
  sorry
end

[Kevin Buzzard]

and if you can't do it, tell your Prof that you can't reconcile their notes with Wikipedia :-)

[Kevin Buzzard]

lol @Heather Macbeth I just checked to see if I could do the level and I was just about to finish with a goal of n ≥ n and I tried refl and it didn't work :D. I think ge_refl must have got removed!

[Kevin Buzzard]

OK I found another proof! @Aron I can confirm that Heather's level is solvable!

[Kevin Buzzard]

Feel free to ask questions. But most importantly, come up with a maths proof first.

[Kevin Buzzard]

This level is a good lean preparation for the question you originally mentioned

[Aron]

I was too busy solving the problem I mentioned. I didn't use Lean for it and I'm not very sure how to, but it's one big block of symbols so it's possible.

[Aron]

Screen-Shot-2020-10-10-at-8.33.26-PM.png

[Aron]

said block.