Mysterious arguments

Stream: new members

[Gareth Ma]

Hello. I have the following definition, which I defined to only take 3 arguments, nothing else. However, for some reason Lean requires me to supply additional arguments, more than what I defined. Can someone explain how this works? Can't seem to find documentation of it either.

import geometry.euclidean.angle.sphere
import linear_algebra.affine_space.finite_dimensional

open affine affine_map affine_subspace euclidean_geometry finite_dimensional set
open_locale affine big_operators classical euclidean_geometry real

namespace real_space

-- Specify on the real plane
noncomputable theory

variables (V : Type*) (Pt : Type*) [inner_product_space ℝ V] [metric_space Pt]
variables [normed_add_torsor V Pt] [normed_add_torsor ℝ Pt] [hd2 : fact (finrank ℝ V = 2)]
include hd2

-- Perpendicular distance from p3 to p1 p2, which doesn't seem to be defined in mathlib
def perpendicular_distance (p1 p2 p3 : Pt) := ‖p3 -ᵥ ↑(orthogonal_projection line[ℝ, p1, p2] p3)‖

-- The shortest distance from p3 to any point on p1 p2 is perpendicular distance
lemma lemma2 {p1 p2 p3 : Pt} :
⨅ x ∈ line[ℝ, p1, p2], ‖x -ᵥ p3‖ = perpendicular_distance V _ p1 p2 p3 :=
begin

end

If you look at perpendicular_distance, I defined it to take in 3 points. However, Lean forces me to also supply V and Pt when I use it in the statement of lemma2.

[Eric Wieser]

When you write variables (V : Type*) (Pt : Type*) you are saying "all functions which use V or Pt from this point on will take them as explicit arguments"

[Eric Wieser]

If you change those () (explicit) s to {} (implicit) then your problem might go away

[Gareth Ma]

Yea it does! But now it deduces the wrong argument :tear: It thinks it's ... \R Pt p1 p2 p3 instead of the correct ... V Pt p1 p2 p3.

[Eric Wieser]

I have no idea why it's doing that!

[Eric Wieser]

Oh I think normed_add_torsor ℝ Pt is the problem

[Eric Wieser]

Lean doesn't want you having more than vector space associated with your affine space

[Gareth Ma]

:thinking:

[Gareth Ma]

I will think through all the instances and assumptions then. I am just copying them here and there, mainly from the IMO 2019 Q2 geometry question formalisation, since it uses euclidean geometry lol

[Eric Wieser]

[normed_add_torsor ℝ Pt] means "you can subtract any two points and get a real number"

[Eric Wieser]

Which essentially makes your problem 1D, I think (and therefore trivial because your assumption is that it's 2D, so contradiction)

[Gareth Ma]

Oh hmm, so it's kind of saying Pt - Pt is the distance? Instead of say the vector

[Eric Wieser]

It's saying that it's the signed distance along 1D space

[Eric Wieser]

To get this to work it seems you need complete_space ↥((affine_span ℝ {p1, p2}).direction) and I'm not sure where that comes from

[Gareth Ma]

Maybe I should start from scratch. Like essentially all I want is 2d vectors over the reals.

[Gareth Ma]

Since the theorem I am trying to prove is specifically for 2d and over the reals, at least for now

[Eric Wieser]

Maybe @Joseph Myers can advise on why your version doesn't work out

[Gareth Ma]

Thanks in advance :pray: Or just point me to what I actually need I guess. I think the major reason why I am struggling is I don't know the broad theory that is implemented in Lean, i.e. all the torsor and things, and there hasn't been past samples on how to setup a specific instance (R^2) either.

[Eric Wieser]

This seems to work, but feels ugly:

import linear_algebra.affine_space.finite_dimensional

open affine affine_map affine_subspace euclidean_geometry finite_dimensional set
open_locale affine big_operators classical euclidean_geometry real

namespace real_space

-- Specify on the real plane
noncomputable theory

variables (V : Type*) {Pt : Type*} [inner_product_space ℝ V] [metric_space Pt]
variables [normed_add_torsor V Pt] [complete_space V] [hd2 : fact (finrank ℝ V = 2)]
include hd2

-- Perpendicular distance from p3 to p1 p2, which doesn't seem to be defined in mathlib
def perpendicular_distance (p1 p2 p3 : Pt) : ℝ :=
if h : complete_space (line[ℝ, p1, p2]).direction then
  by exactI ‖p3 -ᵥ ↑(euclidean_geometry.orthogonal_projection line[ℝ, p1, p2] p3)‖
else 0

[Sebastien Gouezel]

Why not use docs#metric.inf_dist?

[Gareth Ma]

That if seems weird lol

[Gareth Ma]

Sebastien Gouezel said:

Why not use docs#metric.inf_dist?

I will take a look, thanks! Looks good so far:

-- Perpendicular distance from p3 to p1 p2, which doesn't seem to be defined in mathlib
def perpendicular_distance (p1 p2 p3 : Pt) : ℝ := metric.inf_dist p3 line[ℝ, p1, p2]

-- (Practice lemmas)
-- The perpendicular distance from p1 to p1 p2 is 0
lemma lemma1 {p1 p2 : Pt} : perpendicular_distance V p1 p2 p1 = 0 :=
begin
  simp only [perpendicular_distance, coe_affine_span, inf_dist,
             inf_edist_zero_of_mem (mem_span_points ℝ p1 _ (mem_insert p1 _)), zero_to_real],
end

[Joseph Myers]

Eric Wieser said:

To get this to work it seems you need complete_space ↥((affine_span ℝ {p1, p2}).direction) and I'm not sure where that comes from

I think we need instances finite_dimensional_direction_affine_span_singleton and finite_dimensional_vector_span_singleton and finite_dimensional_direction_affine_span_insert_set to go along with the existing finite_dimensional_vector_span_insert_set, and then type class inference should be able to deduce complete_space ↥((affine_span ℝ s).direction) (via finite_dimensional) for any s that is syntactically of the form {p1, p2, p3, ...}.

[Eric Wieser]

Oh, does adding a finite_dimensional ℝ V instance argument make the first example work?

[Gareth Ma]

Okay so essentially I got a bit lost in everything, so I deleted everything and started again, but this time deriving the instances I need on my own lmao. Here is what I got: https://github.com/grhkm21/lean/blob/master/sketch/sylvester_gallai.lean#L61 I think it is working okay, just need to fix the remaining 50 bugs :D Thanks for the help

[Eric Wieser]

Eric Wieser said:

Oh, does adding a finite_dimensional ℝ V instance argument make the first example work?

Yes, this is the fix:

import geometry.euclidean.angle.sphere
import linear_algebra.affine_space.finite_dimensional

open affine affine_map affine_subspace euclidean_geometry finite_dimensional set
open_locale affine big_operators classical euclidean_geometry real

namespace real_space

-- Specify on the real plane
noncomputable theory

variables (V : Type*) {Pt : Type*} [inner_product_space ℝ V] [metric_space Pt]
variables [normed_add_torsor V Pt] [finite_dimensional ℝ V] [hd2 : fact (finrank ℝ V = 2)]
include hd2

-- Perpendicular distance from p3 to p1 p2, which doesn't seem to be defined in mathlib
def perpendicular_distance (p1 p2 p3 : Pt) : ℝ :=
‖p3 -ᵥ ↑(euclidean_geometry.orthogonal_projection line[ℝ, p1, p2] p3)‖

end real_space

metric.inf_dist is probably still a good choice