How to actually compute midpoint

Stream: maths

[Dmitry Polyakov]

According to MIL and its source file midpoint is noncomputable. But manual claims More interestingly, we can compute the midpoint of two points on the simplex.

import MIL.Common
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Data.Real.Basic
open BigOperators

structure StandardSimplex (n : ℕ) where
  V : Fin n → ℝ
  NonNeg : ∀ i : Fin n, 0 ≤ V i
  sum_eq_one : (∑ i, V i) = 1

namespace StandardSimplex

def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
    where
  V i := (a.V i + b.V i) / 2
  NonNeg := by
    intro i
    apply div_nonneg
    · linarith [a.NonNeg i, b.NonNeg i]
    norm_num
  sum_eq_one := by
    simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
      a.sum_eq_one, b.sum_eq_one]
    field_simp

I can apply midpoint to Simpex:

variable (xx : StandardSimplex 3)
variable (yy : Fin 3)
#check (midpoint 3 xx xx)

But can not get actually value of midpint.
May be it is due V : Fin n → ℝ.

My question is "How to actually compute midpoint?". Or what MIL mean by we can compute?

My specific question is how to get midpoint of two points: 1 0 0 and 0 1 0, and get midpoints x, y and z values.

[Patrick Massot]

MIL means computing in the sense of defining here. We should probably change that wording. Nothing involving real numbers will be computable in the sense of software engineering.

[Dmitry Polyakov]

Patrick Massot said:

MIL means computing in the sense of defining here. We should probably change that wording. Nothing involving real numbers will be computable in the sense of software engineering.

According to advice, I changed V : Fin n → ℝ to V : Fin n → ℚ, and expression #check V (midpoint 3 xx xx) yy has type ℚ.

Sorry for straight question, but what I should read to get midpoint of two points: 1 0 0 and 0 1 0, and get midpoints x, y and z values?

[Jireh Loreaux]

Use #eval to see the results of computations, not #check, which just tells you the type.

[Dmitry Polyakov]

Jireh Loreaux said:

Use #eval to see the results of computations, not #check, which just tells you the type.

variable (xx : StandardSimplex 3)
variable (yy : Fin 3)

#eval V (midpoint 3 xx xx) yy

gives me (kernel) declaration has free variables '_eval'

[Kevin Buzzard]

That means "this isn't a concrete number so how can I eval it?"

[Scott Morrison]

@Dmitry Polyakov, could you sketch what sort of answer you are hoping to see?

[Scott Morrison]

(Don't worry about Lean syntax.)

[Kevin Buzzard]

Yes -- what do you want the answer to be? You do understand that lean is a theorem prover, not a computer algebra system?

[Eric Wieser]

Are you maybe looing for #simp [midpoint] (midpoint 3 xx xx).V?

[Dmitry Polyakov]

Kevin Buzzard said:

Yes -- what do you want the answer to be? You do understand that lean is a theorem prover, not a computer algebra system?

Lets p1 is a 3-dimension point with fields x=1, y=0, z=0.
Lets p2 is a 3-dimension point with fields x=0, y=1, z=0.

All what I want is to get object with fields x=0.5, y=0.5, z=0 somehow using general StandardSimplex (not special structure only for 3-dimension points) and midpoint function defined on it structure.

First of all, I don't understand how to define "points" i.e. can I create instance of StandardSimplex? I can do it with Point easily like this:

structure Point where
  x : ℚ
  y : ℚ
  z : ℚ

def p1 := Point.mk 1 0 0
def p2 := Point.mk 0 1 0

def midpoint1 (a b : Point) : Point
    where
  x := (a.x + b.x) / 2
  y := (a.y + b.y) / 2
  z := (a.z + b.z) / 2

#eval (midpoint1 p1 p2).x -- or get .y/.z

May be StandardSimplex is rather "theoretical" structure, and therefore I can not work with it like with any other computable structure?

[Eric Wieser]

First of all, I don't understand how to define "points" i.e. can I create instance of StandardSimplex? I can do it with Point easily like this:

You can use ![] notation, as

def myPointInSimplex : StandardSimplex 3 where
   V := ![1, 0, 0]
   NonNeg := sorry
   sum_eq_one := sorry

[Dmitry Polyakov]

Eric Wieser said:

First of all, I don't understand how to define "points" i.e. can I create instance of StandardSimplex? I can do it with Point easily like this:

You can use ![] notation, as

def myPointInSimplex : StandardSimplex 3 where
   V := ![1, 0, 0]
   NonNeg := sorry
   sum_eq_one := sorry

Thank you very much! As far as I understand, every time when I construct instance I must prove NonNeg and sum_eq_one constrains? It is tedious to do it every time.

[Eric Wieser]

You should be able to find a pretty short tactic you can just copy paste

[Eric Wieser]

You have to prove it every time, because the reason it is true changes every time depending on how you built it; especially if you start introducing other variables

[Patrick Massot]

If you use it a lot with numerical values then you can use norm_num as a discharger.

[Antoine Chambert-Loir]

To add a pinch of salt to what Eric and Patrick wrote: your type StandardSimplex 3 consists of 3 real numbers which are nonnegative and which add to 1; so it is natural that Lean expects you to provide 3 real numbers plus the proof that they are nonnegative and add to 1.
What Eric suggests is that most of the time, the proof would be similar, if not identical, if you use appropriate tactics.
Patrick suggests that the norm_num tactic (which is fairly efficient on such computations) will work most of the time.
To prove sum_eq_one, by norm_num should work; to prove NonNeg, intro n; by norm_num should work.
(I couldn't test because the notation ![…] does not seem to work on my playground.)

[Eric Wieser]

You need to import the file that defines docs#Matrix.vecNotation to make that notation work

[Antoine Chambert-Loir]

(my suggestion does not work; actually, I do not know how, given i : Fin n (for some explicit integer n), construct n distinct goals in each of which i has a given value).

[Eric Wieser]

fin_cases

[Damiano Testa]

You can use

  NonNeg : ∀ i : Fin n, 0 ≤ V i := by rintro ⟨_|_|_⟩ <;> norm_num

[Damiano Testa]

I was not able to get fin_cases to work as an auto-param, since auto-params apparently do not allow identifiers.

[Eric Wieser]

I think we're probably missing a lemma that says 0 ≤ cons x xs \iff 0 ≤ x \and 0 ≤ xs

[Eric Wieser]

(and for cons x xs ≤ cons y ys)

[Eric Wieser]

@Dmitry Polyakov, if you're interested in contributing to mathlib, that might be a straightforward first contribution!

[Dmitry Polyakov]

Eric Wieser said:

if you're interested in contributing to mathlib, that might be a straightforward first contribution!

I have tried to put:
theorem lemma1 : 0 ≤ cons x p ↔ 0 ≤ x ∧ 0 ≤ p := sorry

Somewhere after cons definition https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Tuple/Basic.lean#L68

But Lean told me:

failed to synthesize instance
  LE ((i : Fin (n + 1)) → α i)

[Kevin Buzzard]

That says "a certain space of functions doesn't have a <= defined on it so what do you mean by <=?"

[Kevin Buzzard]

If you adopt best practice here, by posting fully working lean code which others can run to see the same error (a #mwe), rather than just posting error messages, then it will be very easy for the community to give a much more helpful answer.

[Eric Wieser]

In this case building a mwe is slightly harder than the usual "this exercise didn't work" problem because the edit is happening within a mathlib file

[Dmitry Polyakov]

Kevin Buzzard said:

If you adopt best practice here, by posting fully working lean code which others can run to see the same error (a #mwe), rather than just posting error messages, then it will be very easy for the community to give a much more helpful answer.

Sorry, this is mwe

import Mathlib.Data.Fin.Basic
import Mathlib.Data.Pi.Lex
import Mathlib.Data.Set.Intervals.Basic

#align_import data.fin.tuple.basic from "leanprover-community/mathlib"@"ef997baa41b5c428be3fb50089a7139bf4ee886b"

universe u v

namespace Fin

variable {m n : ℕ}

section Tuple

variable {α : Fin (n + 1) → Type u} (x : α 0) (q : ∀ i, α i) (p : ∀ i : Fin n, α i.succ) (i : Fin n)
  (y : α i.succ) (z : α 0)

/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/
def cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j
#align fin.cons Fin.cons

theorem lemma1 : 0 ≤ cons x p ↔ 0 ≤ x ∧ 0 ≤ p := sorry

[Dmitry Polyakov]

Eric Wieser said:

I think we're probably missing a lemma that says 0 ≤ cons x xs \iff 0 ≤ x \and 0 ≤ xs

By cons x xs => 0 you mean length of vector (cons x xs) => 0?

[Eric Wieser]

No, I meant what I said :). You're missing a typeclass assumption; I think [∀ i, LE (α i)] might suffice

[Eric Wieser]

(in your original example you have this because α i = real)

[Eric Wieser]

(in your original example you have this because α i = real)

[Dmitry Polyakov]

Eric Wieser said:

No, I meant what I said :). You're missing a typeclass assumption; I think [∀ i, LE (α i)] might suffice

[∀ i, LE (α i)] works quite well with lemma2 (may be because of cons x₀ xs and cons y₀ ys are objects of the same type), but 0 is not instance of vector. To be honest I don't know how to apply [∀ i, LE (α i)] only for right side:

import Mathlib.Data.Fin.Basic

universe u
variable {n : ℕ}
variable {α : Fin (n + 1) → Type u}
variable (x₀ y₀ : α 0) (xs ys : ∀ i : Fin n, α i.succ)

def cons : ∀ i, α i := fun j ↦ Fin.cases x₀ xs j

theorem lemma1 [∀ i, LE (α i)] : 0 ≤ cons x₀ xs ↔ 0 ≤ x₀ ∧ 0 ≤ ys := by sorry

theorem lemma2 [∀ i, LE (α i)] : cons x₀ xs ≤ cons y₀ ys ↔ x₀ ≤ y₀ ∧ xs ≤ ys := by sorry

Thank you for patient.

[Eric Wieser]

Adding [∀ i, Zero (α i)] will help

[Kevin Buzzard]

You really want this for functions alpha to a general Type? Not the reals (which have got a huge amount of extra inbuilt structure)?

[Kevin Buzzard]

The issue with your code is that 0 ≤ cons x₀ xs is never going to work because in this generality Lean has no idea what 0 or ≤ mean. Note that even if you do write [∀ i, LE (α i)] then all this means is that "≤ means something" -- it doesn't mean that it obeys any axioms like $x\leq x$ or anything.

[Eric Wieser]

Kevin, this theorem doesn't need any axioms!

[Eric Wieser]

All it needs is that $x \le y$ means $\forall i, x_i \le y_i$ and $0_i = 0$, and [∀ i, LE (α i)] and [∀ i, Zero (α i)] make that true!

[Kevin Buzzard]

I was anticipating the next question.

[Dmitry Polyakov]

i promise i will prove it.