Planar geometry with Cartesian coordinates

Stream: Is there code for X?

[Dustin Mixon]

I would like an implementation of ℝ^2 with the following properties:

(1) the implementation is already in mathlib,

(2) it is possible to specify explicit coordinates of certain members of ℝ^2 (e.g., using numbers from the rationals adjoin sqrt(2) and sqrt(3)), and

(3) there is an implementation of the euclidian norm for ℝ^2 such that

(3a) the obvious lemmas like triangle inequality are already in mathlib,

(3b) it is possible to interact with the square of the norm as a polynomial of the vector coordinates, and

(3c) it is possible to evaluate the norm given explicit coordinates of a member of ℝ^2.

I initially thought that I should use euclidean_space ℝ (fin 2), but I don’t know how to do (2), (3b), or (3c). As an aside, while attempting to resolve (3b) for this implementation of ℝ^2, I quickly got stuck at the goal

(finset.univ.sum (λ (i : fin 2), |x i| ^ 2) ^ (1 / 2)) ^ 2 = x 0 ^ 2 + x 1 ^ 2

I would assume that data.real.sqrt is relevant, but apparently a ^ (1 / 2) is not the same thing as real.sqrt a.

While at LftCM, I noticed folks were using the notation ![2,3] for the vector in ℝ^2 with coordinates 2 and 3, which I suspect will eventually satisfy (2) for me. I #check'd, and ![2,3] is a member of fin 1.succ → ℕ, so maybe there's some coercion in my future. I tried putting fractions in for coordinates, but it also thinks that 1/2 is in ℕ. (?!)

Any help would be greatly appreciated!

[Eric Wieser]

I'm not sure it's an agreed upon spelling, but you can use (pi_Lp.equiv 2 (λ _, ℝ)).symm ![x, y] to get a term of the right type (docs#pi_Lp.equiv)

[Eric Wieser]

docs#euclidean_space.norm_eq should help with 3b

[Ruben Van de Velde]

A #mwe would be useful if you want help with the goal you mentioned, but docs#real.sqrt_eq_rpow might help

[Ruben Van de Velde]

And docs#real.rpow_nat_inv_pow_nat

[Dustin Mixon]

I'm at the point where I'm fighting with an implementation of sum:

import analysis.inner_product_space.pi_L2

notation `ℝ^2` := euclidean_space ℝ (fin 2)

lemma pythagoras (x : ℝ^2) : ∥ x ∥^2 = (x 0)^2 + (x 1)^2 :=
begin
  unfold norm,
  rw ← real.sqrt_eq_rpow,
  rw real.sq_sqrt,
  nth_rewrite 0 ← sq_abs,
  nth_rewrite 1 ← sq_abs,
  sorry,
end

Ideas?

[Eric Wieser]

unfold is usually a wrong turn

[Eric Wieser]

The lemma I suggest above should be better

[Yaël Dillies]

Use docs#fin.sum_univ_succ and docs#fin.sum_univ_zero

[Eric Wieser]

docs#fin.sum_fin_two is better than Yaël's suggestion; assuming it exists

[Yaël Dillies]

docs#fin.sum_univ_two

[Dustin Mixon]

Ah, very nice - thanks!

[Dustin Mixon]

Eric Wieser said:

I'm not sure it's an agreed upon spelling, but you can use (pi_Lp.equiv 2 (λ _, ℝ)).symm ![x, y] to get a term of the right type (docs#pi_Lp.equiv)

I tried this:

import analysis.normed_space.pi_Lp
#check (pi_Lp.equiv 2 (λ _, ℝ)).symm ![2, 3]

and got this error:

type mismatch at application
  ⇑((pi_Lp.equiv 2 (λ (_x : ?m_1), ℝ)).symm) ![2, 3]
term
  ![2, 3]
has type
  fin 1.succ → ?m_1 : Type ?
but is expected to have type
  Π (i : ?m_1), (λ (_x : ?m_1), ℝ) i : Type ?

Reading the documentation, I think pi_Lp.equiv is supposed to map members of fin(2) → ℝ to members of ℝ × ℝ, but I can't say for sure. And I'm still not sure how to force ![2,3] to treat 2 and 3 as real numbers. I looked, and I can't find the obvious coercion map.

[Eric Wieser]

Does

import analysis.normed_space.pi_Lp
#check (pi_Lp.equiv 2 (λ _ : fin 2, ℝ)).symm ![2, 3]

Work?

[Dustin Mixon]

No, I get this:

type mismatch at application
  ⇑((pi_Lp.equiv 2 (λ (_x : fin 2), ℝ)).symm) ![2, 3]
term
  ![2, 3]
has type
  fin 1.succ → ?m_1 : Type ?
but is expected to have type
  Π (i : fin 2), (λ (_x : fin 2), ℝ) i : Type

[Eric Wieser]

And I'm still not sure how to force ![2,3] to treat 2 and 3 as real numbers.

No coercion needed; just give lean a hint that's the type you want, with ![(1 : ℝ), 2] or (![1, 2] : fin 2 → ℝ)

[Eric Wieser]

Ouch, that's an annoying error. I think if you combine my previous message with that suggestion then the problem goes away, but that's certainly not ideal

[Dustin Mixon]

Ah - yes, (pi_Lp.equiv 2 (λ _ : fin 2, ℝ)).symm ![(2:ℝ),(3:ℝ)] does not return an error.

[Dustin Mixon]

But when I #check, I don't understand what I see:

⇑((pi_Lp.equiv 2 (λ (_x : fin 2), ℝ)).symm) ![2, 3] : pi_Lp 2 (λ (_x : fin 2), ℝ)

I think I'm hoping for a member of euclidean_space ℝ (fin 2).

[Eric Wieser]

One is an alias of the other

[Eric Wieser]

src#euclidean_space

[Eric Wieser]

Because it's reducible, lean will treat those two things as the same

[Eric Wieser]

This is absolutely a pain point though

[Dustin Mixon]

Ah, so maybe the point is encoded as ⇑((pi_Lp.equiv 2 (λ (_x : fin 2), ℝ)).symm) ![2, 3] and it resides in the type pi_Lp 2 (λ (_x : fin 2), ℝ, which is regarded as the same thing as euclidean_space ℝ (fin 2)?

[Dustin Mixon]

(I'm just trying to understand.)

[Dustin Mixon]

I was hoping that would do the trick, but then I tried this:

import analysis.normed_space.pi_Lp
notation `v1` := (pi_Lp.equiv 2 (λ _ : fin 2, ℝ)).symm ![(2:ℝ),(3:ℝ)]
notation `v2` := (pi_Lp.equiv 2 (λ _ : fin 2, ℝ)).symm ![(1/2:ℝ),(3:ℝ)]
#eval ∥ v1 - v2 ∥

and got this:

code generation failed, VM does not have code for 'classical.choice'

[Eric Wieser]

Unfortunately there are multiple notions of "the same thing" here

[Eric Wieser]

But your summary is largely accurate

[Eric Wieser]

Yes, your problem is that docs#real.normed_group is noncomputable, because it requires determining whether a real number is positive or negative

[Dustin Mixon]

So is it not possible to evaluate the norm given explicit coordinates of a member of ℝ^2? Or do I need to pass to another encoding for that?

[Dustin Mixon]

Also, your link to real.has_norm breaks for me.

[Eric Wieser]

What does it mean to evaluate a real? Do you mean compute a decimal expansion?

[Eric Wieser]

Note that even this doesn't do anything useful:

import data.real.basic

#eval (3 - 2 : ℝ)

[Dustin Mixon]

I would like to compute norms of vectors with entries in the rationals adjoint sqrt(2) and sqrt(3), say.

[Dustin Mixon]

Do I need to restrict to the smaller field somehow?

[Dustin Mixon]

Haha, I just tried your example. That internal representation is nuts.

[Eric Wieser]

Here's a way to see the representation more clearly:

import data.real.basic
import data.fin.vec_notation

#eval (2 + 3 : ℝ).cauchy.unquot.1 ∘ (coe : fin 10 → ℕ)

[Eric Wieser]

Dustin Mixon said:

I would like to compute norms of vectors with entries in the rationals adjoint sqrt(2) and sqrt(3), say.

That sounds like it should be computable, but you're still stuck with the problem that docs#has_norm.norm produces a real

[Dustin Mixon]

So is the verdict that there is no implementation of ℝ^2 that satisfies the properties I initially outlined?

[Dustin Mixon]

It seems that (3c) is the stickler for euclidean_space ℝ (fin 2)

[Eric Wieser]

Well you first need an implementation of ℝ that satisfies those properties. There are models for computable reals, but computation is something mathlib doesn't care about

[Eric Wieser]

Are you sure you need "computation" in the sense of #eval?

[Dustin Mixon]

I'm interested in formalizing the proof that the chromatic number of the plane is at least 5. This requires me to compute thousands of norms of the sort I describe.

[Eric Wieser]

Computation via #eval plays no part in proofs in Lean

[Dustin Mixon]

In particular, I need to be able to convince Lean that certain pairs of points in ℝ^2 are unit distance apart.

[Eric Wieser]

#eval runs code in an unverified VM

[Yaël Dillies]

This sounds like a tactic's job.

[Eric Wieser]

Here's another sort of "computation":

import data.real.basic
import data.fin.vec_notation

import analysis.inner_product_space.pi_L2
notation `v1` := (pi_Lp.equiv 2 (λ _ : fin 2, ℝ)).symm ![(2:ℝ),(3:ℝ)]
notation `v2` := (pi_Lp.equiv 2 (λ _ : fin 2, ℝ)).symm ![(1/2:ℝ),(3:ℝ)]

-- real.sqrt ((2 - 2⁻¹) ^ 2)
#simp [euclidean_space.norm_eq] ∥ v1 - v2 ∥

[Eric Wieser]

Or here's a proof that it "computes" to what you'd expect:

example : ∥ v1 - v2 ∥ = 3/2 :=
begin
  simp [euclidean_space.norm_eq],
  rw real.sqrt_sq,
  { field_simp,
    ring },
  { field_simp,
    linarith },
end

[Dustin Mixon]

Ah, very nice! I think I can run with this. Thanks!

[Reid Barton]

I suggest you first try to prove the chromatic number is at least 4 or even 3

[Eric Wieser]

You could almost "compute" with the rationals adjoined with your two square roots by using mv_polynomial (fin 2) ℚ ⧸ ideal.span {(X 0)^2-2, (X 1)^2-3, X 0*X 1 - 6}, but it turns out for less mathematical reasons polynomials are also noncomputable

[Dustin Mixon]

Reid Barton said:

I suggest you first try to prove the chromatic number is at least 4 or even 3

Yeah, I'm working on showing not 2-colorable right now. :)

[Dustin Mixon]

Eric Wieser said:

You could almost "compute" with the rationals adjoined with your two square roots by using mv_polynomial (fin 2) ℚ ⧸ ideal.span {(X 0)^2-2, (X 1)^2-3, X 0*X 1 - 6}, but it turns out for less mathematical reasons polynomials are also noncomputable

I wonder if polyrith might be useful here.

[Eric Wieser]

Eric Wieser said:

Here's a way to see the representation more clearly:

import data.real.basic
import data.fin.vec_notation

#eval (2 + 3 : ℝ).cauchy.unquot.1 ∘ (coe : fin 10 → ℕ)

I've PR'd something like this as #15575, so that #eval does something sensible when it's possible to

[Reid Barton]

There's no reason this should actually be correct, since you might well have a Cauchy sequence like 0, 0, 0, 0, 0, 0, 5, 5, 5, 5, ... that represents 5 not 0

[Eric Wieser]

Whoops, I guess I totally misread how cauchy sequences were defined. Thanks for the sanity check, I guess I'll just have it emit the sequence always

[Eric Wieser]

Fixed, it now spits out

#eval (37 : ℝ)
-- real.of_cauchy (sorry /- 37, 37, 37, 37, 37, 37, 37, 37, 37, 37, ... -/)

which is still a lot better than the megabyte of output it used to produce

[Violeta Hernández]

Nice!

[Violeta Hernández]

Does it work for irrationals too? Surely there's some irrational in mathlib with a computable Cauchy sequence...