Simple geom: perpendicular drop & cosine adjacent hypotenuse

Stream: new members

[MohanadAhmed]

While doing some simple geometry proofs I needed to drop a perpendicular from a point to line. Then take the cosine of the angle from by this perpendicular from the point it was droped from. Thus a I need a definition/lemma/something that says that in a right angle triangle the cosine is the adjacent over the hypotenuse.

DropPerpendicular.drawio.png

I looked a through the euclidean_geometry in mathlib but couldn't find either points. I guess it is either somewhere else or not implemented yet.

First Question

So my first question is there somewhere I am missing where basic right angle triangle definitions are?

Second Question

I tried my hand both and would welcome any critique.

1. For example would the way I defined the perpendicular drop be Ok or do you think there is a more useful way.
2. To require a right angle better use pi/2 or use an inner product definition?
3. What is the difference between having this on the lemma
   {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
   or having variables at the beginning of my file

{V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
    [normed_add_torsor V P]
include V

4. There is definitely a better way to do this. What I did seems very verbose, any thoughts?

Third Question

when doing proofs with euclidean_geometry is there a normed_add_torsor V P goal that appears when I use the lemmas dist_eq_norm_vsub that I can clear at the end by assumption, but I have on idea what it is.

Thanks for any comments or help.

Perpendicular Drop Code

lemma perpendicular_drop
    (p1 p2 p3 : P)
    (ha: p2 ≠ p1) (hb: p3 ≠ p2) (hc: p1 ≠ p3)
    :
    (
      ∃ (pa : P) (α :ℝ ), pa = (line_map p1 p2 (α:ℝ)) ∧
      (α = ⟪ p3 -ᵥ p1, p2 -ᵥ p1 ⟫ / (∥ p2 -ᵥ p1 ∥ * ∥ p2 -ᵥ p1 ∥)) ∧
      angle p1 pa p3 = π /2 ∧
      angle p3 pa p2 = π/2
    ) :=
begin

  let β := ⟪ p3 -ᵥ p1, p2 -ᵥ p1 ⟫ / (∥ p2 -ᵥ p1 ∥ * ∥ p2 -ᵥ p1 ∥),
  use (line_map p1 p2 β),
  use β,
  have hα : β = ⟪ p3 -ᵥ p1, p2 -ᵥ p1 ⟫ / (∥ p2 -ᵥ p1 ∥ * ∥ p2 -ᵥ p1 ∥), {
    tauto,
  },

  have xz : ∥p2 -ᵥ p1∥ ≠ 0, {
    by_contradiction,
    simp at h, tauto,
  },

  have rza: ∥p2 -ᵥ p1∥^2 * (∥p2 -ᵥ p1∥^2)⁻¹ = 1, by {
    ring_nf,
    rw inv_mul_cancel, by_contradiction,
    rw sq_eq_zero_iff at h, tauto,
  },

  refine ⟨_, _, _ , _⟩, tauto, tauto,

  rw line_map_apply,
  rw euclidean_geometry.angle,
  rw inner_product_geometry.angle,
  simp,
  left,
  rw vsub_vadd_eq_vsub_sub,
  rw vsub_vadd_eq_vsub_sub,

  simp,
  rw [inner_sub_right],
  rw real_inner_smul_right,
  rw real_inner_smul_left, rw real_inner_smul_left,
  rw real_inner_comm (p3 -ᵥ p1) (p2 -ᵥ p1),

  rw real_inner_self_eq_norm_sq,
  rw hα,
  ring_nf, rw ← pow_two,
  rw rza, linarith,

  rw line_map_apply,
  rwa euclidean_geometry.angle,
  rw inner_product_geometry.angle,
  simp,
  left,
  rw vsub_vadd_eq_vsub_sub,
  rw vsub_vadd_eq_vsub_sub,

  rw [inner_sub_left, inner_sub_right, inner_sub_right],
  rw real_inner_smul_right,
  rw real_inner_smul_right, rw real_inner_smul_left,

  rw real_inner_self_eq_norm_sq,
  rw hα,
  ring_nf, rw ← pow_two,
  rw rza, linarith,

end

Cosine is Equal Adjacent over Hypotenuse

lemma cos_adjacent_div_hypotenuse
  {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
  [normed_add_torsor V P]
  (p1 p2 p3 : P)
  (ha: p2 ≠ p1) (hb: p3 ≠ p2) (hc: p1 ≠ p3)
  (hpi_div_2: angle p2 p1 p3 = π / 2) :
  (real.cos(angle p1 p2 p3) = dist p1 p2 / dist p2 p3) :=
begin

  have abs_p321:
    |inner (p1 -ᵥ p2) (p3 -ᵥ p2) / (∥p1 -ᵥ p2∥ * ∥p3 -ᵥ p2∥)| ≤ 1,
      by apply abs_real_inner_div_norm_mul_norm_le_one,

  rw abs_le at abs_p321,
  cases abs_p321 with h_leq_one h_geq_one,

  have p321: p3 -ᵥ p2 = (p3 -ᵥ p1 + (p1 -ᵥ p2)), by simp,

  have mixz: ⟪(p1 -ᵥ p2), (p3 -ᵥ p1)⟫ = 0, by
     rwa [← neg_eq_zero,
     ← inner_neg_left,
     neg_vsub_eq_vsub_rev,
     inner_eq_zero_iff_angle_eq_pi_div_two],

  rw euclidean_geometry.angle,
  rw inner_product_geometry.angle,
  rw real.cos_arccos h_leq_one h_geq_one,

  -- inner (p1 -ᵥ p2) (p3 -ᵥ p2) / (∥p1 -ᵥ p2∥ * ∥p3 -ᵥ p2∥) = dist p1 p2 / dist p2 p3
  rw p321,
  rw inner_add_right,
  rw mixz,
  rw real_inner_self_eq_norm_sq,
  rw ← p321,
  rw dist_eq_norm_vsub V, rw dist_comm,
  rw dist_eq_norm_vsub V,
  simp,

  -- ∥p1 -ᵥ p2∥ ^ 2 / (∥p1 -ᵥ p2∥ * ∥p3 -ᵥ p2∥) = ∥p1 -ᵥ p2∥ / ∥p3 -ᵥ p2∥
  have nz_p12: ∥p1 -ᵥ p2∥ ≠ 0, {rw ← norm_neg, simp, rwa push_neg.not_eq, },
  have nz_p23: ∥p3 -ᵥ p2∥ ≠ 0, {simp, rwa push_neg.not_eq,},

  rw div_mul_eq_div_div_swap,
  rw div_right_comm,
  rw div_eq_iff nz_p23,
  rw div_mul_cancel,

  -- ∥p1 -ᵥ p2∥ ^ 2 / ∥p1 -ᵥ p2∥ = ∥p1 -ᵥ p2∥
  rw div_eq_iff nz_p12, ring, exact nz_p23,

  -- clear normed_add_torsor V P that showed up: I have no idea why!!
  assumption,

end

[Joseph Myers]

Geometry in mathlib defines and proves things in ways that make sense in more than two dimensions, where possible. There are at least two different ways of defining a perpendicular (from a point to an affine subspace that may not necessarily be a line). You can use affine_subspace.mk' p s.directionᗮ, which is the affine subspace through the point p in the direction orthogonal to the subspace s (which is not a line in general, depending on the dimensions involved); that's how altitude is defined for a general simplex, for example. Or you can take the affine_span of the point and its orthogonal_projection onto the subspace (required to have its direction a complete_space, which is automatically the case by type class inference when it's finite_dimensional); this is just a point, not a line, when the point lies in the subspace. Which one of those you want depends on what you want the resulting subspace to be in more than two dimensions, as well as what you want when the point lies in the subspace. Or if what you want is just the foot of the perpendicular rather than the line itself, just use orthogonal_projection, which there are lots of lemmas about.

I'd say that if you're talking about a right angle between two vectors, either the inner product or the angle is appropriate (we have Pythagoras in both forms), but if you're talking about it between three points, using the angle is appropriate rather than the inner product.

We have the law of cosines, in one form only for each of angles between vectors and angles between points (both of those include degenerate cases, not just the cases of an actual triangle). It would seem reasonable to add various rearranged forms of that result, such as one that gives an expression for the cosine of the angle in terms of the vector norms or distances (again, including degenerate cases, not restricted to a triangle; the way angles are defined means they end up as pi/2 if a zero vector is involved, so everything should work out in the degenerate cases). Once you have such rearranged forms, deducing results specific to the right-angled case should be straightforward. (Splitting out small lemmas that are independently meaningful - and, when you do so, thinking about what the appropriately general form of such a lemma is, which may not be the exact form you're using in your larger proof - is generally a good way to simplify proofs.)

It may sometimes help to pass at least one point explicitly to dist_eq_norm_vsub even if rw can work out the point for itself; I think the issue you're having is about order of elaboration, where Lean needs to know the type P early enough to know what type class instance it should look for involving P.