simplifying Pairwise

Stream: new members

[ZhiKai Pong]

I'm trying to prove three vectors in EuclideanSpace ℝ (Fin 3) are docs#Orthonormal.

import Mathlib

example (u v w : EuclideanSpace ℝ (Fin 3)) (huv : inner ℝ u v = 0) (hvw : inner ℝ v w = 0) (huw : inner ℝ u w = 0):
    Orthonormal ℝ ![u, v, w] := by
  rw [Orthonormal]
  constructor
  · sorry
  · rw [Pairwise]
    intro i j h
    fin_cases i <;>
    fin_cases j
    · contradiction
    · sorry -- i j = 0 1
    · sorry -- i j = 0 2
    · sorry -- i j = 1 0
    · contradiction
    · sorry -- i j = 1 2
    · sorry -- i j = 2 0
    · sorry -- i j = 2 1
    · contradiction

The first sorry is fine (showing norm of each = 1). I'm wondering is there a simpler way of unfolding Pairwise using the condition i ≠ j, and without loss of generality only proving it three times instead of having to do all 6 cases where there are 3 symmetric pairs.

[Matt Diamond]

this is a bit silly, but if all else fails you could throw a tactic combinator at it:

import Mathlib

example (u v w : EuclideanSpace ℝ (Fin 3)) (huv : inner ℝ u v = 0) (hvw : inner ℝ v w = 0) (huw : inner ℝ u w = 0):
    Orthonormal ℝ ![u, v, w] := by
  rw [Orthonormal]
  constructor
  · sorry
  · rw [Pairwise]
    intro i j h
    fin_cases i <;>
    fin_cases j <;>
    (first | contradiction | assumption | simp [mul_comm] at *; assumption)

[Matt Diamond]

a bit inelegant, though (and probably slower than necessary)

[Eric Wieser]

@loogle Pairwise, Matrix.vecCons

[loogle]

:shrug: nothing found

[Eric Wieser]

I think the missing result is something like Pairwise R ↔(∀ x. R 0 (succ x)) ∧ (∀ x. R (succ x) 0) ∧ Pairwise (fun x y => R (succ x) (succ y))

[Terence Tao]

Here is one option that I just learned from @Aaron Liu :

import Mathlib

theorem Fin.forall_fin_three {p : Fin 3 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 ∧ p 2 :=
  Fin.forall_fin_succ.trans <| and_congr_right fun _ => Fin.forall_fin_two

example (u v w : EuclideanSpace ℝ (Fin 3)) (huv : inner ℝ u v = 0) (hvw : inner ℝ v w = 0) (huw : inner ℝ u w = 0):
    Orthonormal ℝ ![u, v, w] := by
  rw [Orthonormal]
  let R3 := EuclideanSpace ℝ (Fin 3)
  constructor
  · sorry
  · let r : R3 → R3 → Prop := fun u v ↦ (inner ℝ u v = 0)
    change Pairwise (Function.onFun r ![u,v,w])
    have hr : Symmetric r := fun _ _ ↦ inner_eq_zero_symm.mp
    simp_rw [Symmetric.pairwise_on hr, Fin.forall_fin_three, r]
    simp [huv, hvw, huw]

[Eric Wieser]

#25205 should make this less painful, after which you need

  simp [orthonormal_vecCons_iff, Fin.forall_fin_succ, -PiLp.inner_apply]

[ZhiKai Pong]

thanks to all!