Easy lemma on collinear points and determinants

Stream: new members

[Nicolau Oliver]

I have been attempting to formalize this useful collinearity test determinant, commonly used in computational geometry. I hope this can be the first building block of a small project.

It currently compiles, and I am more or less satisfied with the proof, but had many more problems than I initially expected. Maybe the approach to the proof is not the best, but I was not able to use the rank/finrank lemmas to get a proof, and ended up with this case analysis on vertical lines and some other trivial cases.

Also, I am very new to formatting my proofs, and don't know what is the best practice on using tactics like simp. The linter gave me a warning and I followed the suggestions.

Here is the current code I have. Any questions, suggestions, improvements and criticisms are very welcome.

import Mathlib.Data.Finset.Basic
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Sphere.Basic
import Mathlib.LinearAlgebra.Matrix.Defs
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

open Finset Matrix BigOperators

noncomputable section
namespace FormalButterfly

/-- A point in the Euclidean plane (ℝ²). -/
abbrev Point := EuclideanSpace ℝ (Fin 2)

/-- A finite set of points in the Euclidean plane. -/
abbrev PointSet := Finset Point

/-- A set of points is in *general position* if it contains
    no collinear triples and no concyclic quadruples. -/
def GeneralPosition (S : PointSet) : Prop :=
  (∀ p ∈ S, ∀ q ∈ S, ∀ r ∈ S,
      p ≠ q → q ≠ r → p ≠ r →
      ¬ Collinear ℝ {p, q, r}) ∧
  (∀ p ∈ S, ∀ q ∈ S, ∀ r ∈ S, ∀ s ∈ S,
      p ≠ q → p ≠ r → p ≠ s →
      q ≠ r → q ≠ s → r ≠ s →
      ¬ EuclideanGeometry.Concyclic {p, q, r, s})

/-- Determinant criterion for collinearity of three points in ℝ². -/
def collinearDet (p q r : Point) : ℝ :=
  let m : Matrix (Fin 3) (Fin 3) ℝ :=
    ![
      ![p 0, p 1, 1],
      ![q 0, q 1, 1],
      ![r 0, r 1, 1]
    ]
  m.det

/-- Three points are collinear iff the determinant of their collinearDet is zero. -/
lemma collinear_iff_det_zero (p q r : Point) :
  Collinear ℝ ({p, q, r} : Set Point) ↔ collinearDet p q r = 0 := by
  constructor <;> intro h
  · unfold FormalButterfly.collinearDet
    rw [collinear_iff_exists_forall_eq_smul_vadd] at h
    simp_all [Matrix.det_fin_three]
    rcases h with ⟨ base_pt, dir_vec, ⟨ t_p, rfl ⟩, ⟨ t_q, rfl ⟩, ⟨ t_r, rfl ⟩ ⟩
    norm_num
    ring
  · rw [collinear_iff_exists_forall_eq_smul_vadd]
    use p
    unfold FormalButterfly.collinearDet at h
    simp only [Matrix.det_fin_three] at h
    simp only [Fin.isValue, cons_val', cons_val_zero, cons_val_fin_one, cons_val_one,
      Matrix.cons_val, mul_one, one_mul] at h
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff, vadd_eq_add, forall_eq_or_imp,
      right_eq_add, smul_eq_zero, exists_or_eq_left, forall_eq, true_and]
    by_cases h_qx_eq_px : q 0 = p 0
    · by_cases h_qy_eq_py : q 1 = p 1
      · have h_p_eq_q : p = q := by ext i; fin_cases i <;> simp [h_qx_eq_px, h_qy_eq_py]
        subst h_p_eq_q
        use r - p
        constructor <;> [use 0; use 1]
        · simp only [zero_smul, zero_add]
        · simp only [one_smul, sub_add_cancel]
      · use !₂[0, 1]
        constructor
        · use q 1 - p 1
          ext i; fin_cases i <;> simp [h_qx_eq_px]
        · use r 1 - p 1
          ext i; fin_cases i
          · have h_det_factorized : (p 0 - r 0) * (q 1 - p 1) = 0 := by
              rw [h_qx_eq_px] at h; rw [← h]; ring
            rcases eq_zero_or_eq_zero_of_mul_eq_zero h_det_factorized
              with h_rx_eq_px | h_qy_eq_py_contradiction
            · rw [sub_eq_zero] at h_rx_eq_px; simp [h_rx_eq_px]
            · rw [sub_eq_zero] at h_qy_eq_py_contradiction; contradiction
          · simp
    · use q - p
      constructor
      · use 1; simp
      · use (r 0 - p 0) / (q 0 - p 0)
        ext i; fin_cases i
        · simp only [Fin.zero_eta, Fin.isValue,
            PiLp.add_apply, PiLp.smul_apply, PiLp.sub_apply, smul_eq_mul]
          rw [div_mul_cancel₀]
          · ring
          · exact sub_ne_zero.mpr h_qx_eq_px
        · simp; field_simp [sub_ne_zero.mpr h_qx_eq_px]; nlinarith [h]

end FormalButterfly

#lint

[Snir Broshi]

Nice!
FWIW I think you should try to use grind more, here's the same proof but more than 50% shorter:

lemma collinear_iff_det_zero (p q r : Point) :
    Collinear ℝ ({p, q, r} : Set Point) ↔ collinearDet p q r = 0 := by
  refine collinear_iff_exists_forall_eq_smul_vadd _ |>.trans ⟨fun h ↦ ?_, fun h ↦ ⟨p, ?_⟩⟩
  · simp only [Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
    rcases h with ⟨base_pt, dir_vec, ⟨t_p, rfl⟩, ⟨t_q, rfl⟩, ⟨t_r, rfl⟩⟩
    simp only [FormalButterfly.collinearDet, det_fin_three, Matrix.cons_val]
    norm_num
    ring
  · simp only [FormalButterfly.collinearDet, Matrix.det_fin_three, Matrix.cons_val] at h
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff, vadd_eq_add, forall_eq_or_imp,
      right_eq_add, smul_eq_zero, exists_or_eq_left, forall_eq, true_and]
    by_cases h_qx_eq_px : q 0 = p 0
    · by_cases h_qy_eq_py : q 1 = p 1
      · have h_p_eq_q : p = q := by ext i; fin_cases i <;> simp [h_qx_eq_px, h_qy_eq_py]
        exact ⟨r - p, ⟨0, by simp [h_p_eq_q]⟩, ⟨1, by simp⟩⟩
      · refine ⟨!₂[0, 1], ⟨q 1 - p 1, ?_⟩, ⟨r 1 - p 1, ?_⟩⟩
        · ext i
          fin_cases i <;> simp [h_qx_eq_px]
        · ext i; fin_cases i <;> simp; grind
    · refine ⟨q - p, ⟨1, by simp⟩, (r 0 - p 0) / (q 0 - p 0), ?_⟩
      ext i; fin_cases i <;> simp <;> grind

Though the last grind specifically seems a bit slow, so maybe I'd stick to the nlinarith version

[Snir Broshi]

Nicolau Oliver said:

The linter gave me a warning and I followed the suggestions.

You're probably referring to the flexible linter. The issue it's linting against is assuming what the specific value of something is after you've just applied some general "hammer" that tries to do all sorts of stuff and you can't predict what'll happen, e.g. simp. Since the final result after simp might change if some parts of the library change slightly, you shouldn't follow it with something like use since maybe it might not even be an existential statement after simp is done with it. OTOH, grind after simp is fine, since grind acts similarly to simp where it tries a bunch of stuff without assuming that the goal has a specific structure.
simp only sort of fixes the issue because you're restricting the lemmas you're using, and also stating them explicitly so if someone changes one of them they can find your proof and fix it.

[Nicolau Oliver]

Wow! That is just so much shorter. Thank you so much for spending the time to understand my code and improve it! I would really like to open the repository so that you may even make a commit with your new proof. I am not very familiar with tactics I find complex like refine. Your example is very clear and helpful!

In general I am trying to avoid too heavy automatization while I am trying to grasp the basics. So I would like to avoid big hammers in my proof. Swaped back the last grind for the previous field_simp and nlinarith.

I have another lemma similar to this one but with concyclic points (as you might have guessed from the general position definition). I would like to eventually upload my code for future projects in computational geometry. Do you have any ideas on what would be standard git ettiqute for this kind of small projects?

[Snir Broshi]

Nicolau Oliver said:

I would like to eventually upload my code for future projects in computational geometry. Do you have any ideas on what would be standard git ettiqute for this kind of small projects?

Are you planning to add this to Mathlib? If so, I'd start by making a pull-request to Mathlib with the short proof (and without GeneralPosition and Point), and if you have future plans to add more computational geometry to Mathlib maybe you can announce it on #mathlib4 and ask for others to join. I think a long TODO list for the theorems you plan to prove is a good way to get people to contribute.
If you don't know your way around git/GitHub yet, check out the Git Guide for Mathlib4 Contributors.

[Snir Broshi]

Also since you mentioned "computational geometry", if you're also planning to formalize the algorithms involved, note that Mathlib isn't really the place for algorithms but rather #CSLib. Also, CSLib isn't yet ready to accept algorithm contributions, so I'd recommend posting a thread there about your intentions and to avoid any algorithms for now.

[Joseph Myers]

For mathlib I think the collinearity condition should be given for Fin 2 → 𝕜 for any [Field 𝕜] (I expect the same proof should work over any field).

[Joseph Myers]

Then you have the issue that EuclideanSpace isn't actually of that form, it's defined in terms of PiLp; not sure what the most general thing is that covers all PiLp p (Fin 2 → 𝕜) or if you should just state the theorem for PiLp p (Fin 2 → 𝕜) as well.

[Eric Wieser]

I would guess you want it defined for an arbitrary module, perhaps in terms of a choice of basis

[Eric Wieser]

Can you get there from LinearMap.det instead?

[Eric Wieser]

I'll also point out #new members > matrix and LinearIndependent @ 💬 (which I sent via DM), which along with the chain of older threads it links seems related here.