Skip to content

Instantly share code, notes, and snippets.

@righ1113

righ1113/CosineFormula.idr

Last active July 5, 2023 19:59
Show Gist options
  • Save righ1113/1ebefceaec024a95ba31959141f8ce05 to your computer and use it in GitHub Desktop.
Save righ1113/1ebefceaec024a95ba31959141f8ce05 to your computer and use it in GitHub Desktop.
Download ZIP
ベクトルを用いた余弦定理の証明 in Idris, Lean
Raw
CosineFormula.idr
module CosineFormula
-- > idris -p base
import Syntax.PreorderReasoning
%default total
%hide Language.Reflection.P
%hide cos
-- ・pointの定義
data Point = P Double Double
-- ・vectorの定義
data Vector = Vec Point Point
-- ・normの定義
postulate norm : Vector -> Double
syntax "||" [x] "||" = norm x
-- ・cosの定義
postulate cos : Point -> Double
-- ・ベクトルの引き算の定義
postulate minus : Vector -> Vector -> Vector
syntax [x] "<->" [y] = minus x y
postulate minusV : {A, B, C : Point}
-> Vec B C = ((Vec A C) <-> (Vec A B))
-- ・内積の定義
postulate innerP : Vector -> Vector -> Double
syntax [x] "<*>" [y] = innerP x y
postulate difInnerP1 : {A, B, C : Point}
-> ((Vec A C) <*> (Vec A B)) = || (Vec A C) || * || (Vec A B) || * cos A
postulate difInnerP2 : {A, B : Point}
-> ((Vec A B) <*> (Vec A B)) = || (Vec A B) || * || (Vec A B) ||
-- ・内積の交換法則
postulate commOfInnerP : (x, y : Vector)
-> (x <*> y) = (y <*> x)
-- ・内積の分配法則
postulate distOfInnerP1 : (x, y, z : Vector)
-> ((x <-> y) <*> z) = (x <*> z) - (y <*> z)
postulate distOfInnerP2 : (x, y, z : Vector)
-> (z <*> (x <-> y)) = (z <*> x) - (z <*> y)
-- ・三角形の辺からベクトル
namespace tri
postulate a : Double
postulate b : Double
postulate c : Double
postulate A : Point
postulate B : Point
postulate C : Point
cong2 : {f : t -> u -> v} -> (e = g) -> (h = i) -> f e h = f g i
cong2 Refl Refl = Refl
postulate lemma_a : tri.a = || (Vec B C) ||
postulate lemma_b : tri.b = || (Vec A C) ||
postulate lemma_c : tri.c = || (Vec A B) ||
-- ・Doubleの定理（仮定）
postulate dMinus1 : (x, y, z : Double) -> z - (x - y) = z - x + y
postulate dMinus2 : (x, y, z : Double) -> x - y - y + z = x - 2 * y + z
postulate dMulti1 : (x, y1, y2, y3, z : Double) -> x - 2 * (y1*y2*y3) + z = x - 2 * y1*y2*y3 + z
postulate dComm1 : (x, y, z : Double) -> x - y + z = x + z - y
-- ・余弦定理
cosineFormula :
tri.a * tri.a = (tri.b * tri.b + tri.c * tri.c - 2 * tri.b * tri.c * cos A)
cosineFormula =
(a * a) ={ cong2 {f=(*)} lemma_a lemma_a }=
((norm (Vec B C)) * (norm (Vec B C))) ={ sym difInnerP2 }=
((Vec B C) <*> (Vec B C)) ={ cong2 {f=innerP} minusV minusV }=
(((Vec A C) <-> (Vec A B))
<*> ((Vec A C) <-> (Vec A B))) ={ distOfInnerP2 (Vec A C) (Vec A B) ((Vec A C) <-> (Vec A B)) }=
((((Vec A C) <-> (Vec A B)) <*> (Vec A C))
- (((Vec A C) <-> (Vec A B)) <*> (Vec A B))) ={ cong {f=(\t=>(t-(((Vec A C) <-> (Vec A B)) <*> (Vec A B))))} (distOfInnerP1 (Vec A C) (Vec A B) (Vec A C)) }=
(((Vec A C) <*> (Vec A C)) - ((Vec A B) <*> (Vec A C))
- (((Vec A C) <-> (Vec A B)) <*> (Vec A B))) ={ cong (distOfInnerP1 (Vec A C) (Vec A B) (Vec A B)) }=
(((Vec A C) <*> (Vec A C)) - ((Vec A B) <*> (Vec A C))
- (((Vec A C) <*> (Vec A B)) - ((Vec A B) <*> (Vec A B)))) ={ dMinus1 ((Vec A C) <*> (Vec A B)) ((Vec A B) <*> (Vec A B)) (((Vec A C) <*> (Vec A C)) - ((Vec A B) <*> (Vec A C))) }=
(((Vec A C) <*> (Vec A C)) - ((Vec A B) <*> (Vec A C))
- ((Vec A C) <*> (Vec A B)) + ((Vec A B) <*> (Vec A B))) ={ cong {f=(\t=>(((Vec A C) <*> (Vec A C)) - t - ((Vec A C) <*> (Vec A B)) + ((Vec A B) <*> (Vec A B))))} (commOfInnerP (Vec A B) (Vec A C)) }=
(((Vec A C) <*> (Vec A C)) - ((Vec A C) <*> (Vec A B))
- ((Vec A C) <*> (Vec A B)) + ((Vec A B) <*> (Vec A B))) ={ dMinus2 ((Vec A C) <*> (Vec A C)) ((Vec A C) <*> (Vec A B)) ((Vec A B) <*> (Vec A B)) }=
(((Vec A C) <*> (Vec A C)) - 2 * ((Vec A C) <*> (Vec A B))
+ ((Vec A B) <*> (Vec A B))) ={ cong {f=(\t=>(t - 2 * ((Vec A C) <*> (Vec A B)) + ((Vec A B) <*> (Vec A B))))} (difInnerP2 {A=A} {B=C}) }=
(norm (Vec A C) * norm (Vec A C)
- 2 * ((Vec A C) <*> (Vec A B))
+ ((Vec A B) <*> (Vec A B))) ={ cong {f=(\t=>(norm (Vec A C) * norm (Vec A C) - 2 * ((Vec A C) <*> (Vec A B)) + t))} (difInnerP2 {A=A} {B=B}) }=
(norm (Vec A C) * norm (Vec A C)
- 2 * ((Vec A C) <*> (Vec A B))
+ norm (Vec A B) * norm (Vec A B)) ={ cong {f=(\t=>(norm (Vec A C) * norm (Vec A C) - 2 * t + norm (Vec A B) * norm (Vec A B)))} (difInnerP1 {A=A} {B=B} {C=C}) }=
(norm (Vec A C) * norm (Vec A C)
- 2 * (norm (Vec A C) * norm (Vec A B) * cos A)
+ norm (Vec A B) * norm (Vec A B)) ={ dMulti1 (norm (Vec A C) * norm (Vec A C)) (norm (Vec A C)) (norm (Vec A B)) (cos A) (norm (Vec A B) * norm (Vec A B)) }=
(norm (Vec A C) * norm (Vec A C)
- 2 * norm (Vec A C) * norm (Vec A B) * cos A
+ norm (Vec A B) * norm (Vec A B)) ={ cong {f=(\t=>(t * norm (Vec A C) - 2 * norm (Vec A C) * norm (Vec A B) * cos A + norm (Vec A B) * norm (Vec A B)))} (sym lemma_b) }=
(b * norm (Vec A C)
- 2 * norm (Vec A C) * norm (Vec A B) * cos A
+ norm (Vec A B) * norm (Vec A B)) ={ cong {f=(\t=>(b * t - 2 * norm (Vec A C) * norm (Vec A B) * cos A + norm (Vec A B) * norm (Vec A B)))} (sym lemma_b) }=
(b * b
- 2 * norm (Vec A C) * norm (Vec A B) * cos A
+ norm (Vec A B) * norm (Vec A B)) ={ cong {f=(\t=>(b * b - 2 * t * norm (Vec A B) * cos A + norm (Vec A B) * norm (Vec A B)))} (sym lemma_b) }=
(b * b
- 2 * b * norm (Vec A B) * cos A
+ norm (Vec A B) * norm (Vec A B)) ={ cong {f=(\t=>(b * b - 2 * b * t * cos A + norm (Vec A B) * norm (Vec A B)))} (sym lemma_c) }=
(b * b
- 2 * b * c * cos A
+ norm (Vec A B) * norm (Vec A B)) ={ cong {f=(\t=>(b * b - 2 * b * c * cos A + t * norm (Vec A B)))} (sym lemma_c) }=
(b * b
- 2 * b * c * cos A
+ c * norm (Vec A B)) ={ cong {f=(\t=>(b * b - 2 * b * c * cos A + c * t))} (sym lemma_c) }=
(b * b - 2 * b * c * cos A + c * c) ={ dComm1 (b * b) (2 * b * c * cos A) (c * c) }=
(b * b + c * c - 2 * b * c * cos A) QED
Raw
cosineFormula.lean
-- ・pointの定義
inductive Point
| mk : ℕ → ℕ → Point
#check Point.mk 10 20
-- ・Vectorの定義
inductive Vec
| mk : Point → Point → Vec
-- ・normの定義
axiom norm : Vec → ℕ
notation `||` x `||` := norm x
-- ・cosの定義
axiom cos : Point → ℕ
-- ・ベクトルの引き算の定義
axiom minus : Vec → Vec → Vec
local infixr `<->`:50 := minus
axiom minusV {A B C : Point} : (Vec.mk A C <-> Vec.mk A B) = Vec.mk B C
-- ・内積の定義
axiom innerP : Vec → Vec → ℕ
local infixr `<*>`:50 := innerP
axiom difInnerP1 {A B C : Point}
: (Vec.mk A C <*> Vec.mk A B)
= norm (Vec.mk A C) * norm (Vec.mk A B) * cos A
axiom difInnerP2 {A B : Point}
: (Vec.mk A B <*> Vec.mk A B)
= norm (Vec.mk A B) * norm (Vec.mk A B)
-- ・内積の交換法則
axiom commOfInnerP : ∀ (x y : Vec), (x <*> y) = (y <*> x)
-- ・内積の分配法則
axiom distOfInnerP1 {x y z : Vec} : ((x <-> y) <*> z) = (x <*> z) - (y <*> z)
axiom distOfInnerP2 {x y z : Vec} : (z <*> (x <-> y)) = (z <*> x) - (z <*> y)
-- ・三角形の辺からベクトル
#check 3.14
#reduce 157.0/50.0
variables a b c : ℕ
variables A B C : Point
axiom lemma_a : a = norm (Vec.mk B C)
axiom lemma_b : b = norm (Vec.mk A C)
axiom lemma_c : c = norm (Vec.mk A B)
-- ・自然数の定理（仮定）
axiom ℕminus1 : ∀ (x y z : ℕ), z - (x - y) = z - x + y
axiom ℕminus2 : ∀ (x y : ℕ), x - y - y = x - 2 * y
axiom ℕmulti1 : ∀ (x y z w : ℕ), x - 2 * (y * z * w) = x - 2 * y * z * w
axiom ℕcomm1 : ∀ (x y z : ℕ), x - y + z = x + z - y
-- ・余弦定理
theorem cosineFormula
: a * a = b * b + c * c - 2 * b * c * cos A
:= calc
a * a
= norm (Vec.mk B C) * norm (Vec.mk B C) : by rw lemma_a a
... = (Vec.mk B C <*> Vec.mk B C) : by rw difInnerP2
... = ((Vec.mk A C <-> Vec.mk A B)
<*> (Vec.mk A C <-> Vec.mk A B)) : by rw minusV
... = ((Vec.mk A C <-> Vec.mk A B) <*> Vec.mk A C)
- ((Vec.mk A C <-> Vec.mk A B) <*> Vec.mk A B) : by rw distOfInnerP2
... = (Vec.mk A C <*> Vec.mk A C) - (Vec.mk A B <*> Vec.mk A C)
- ((Vec.mk A C <-> Vec.mk A B) <*> Vec.mk A B) : by rw distOfInnerP1
... = (Vec.mk A C <*> Vec.mk A C) - (Vec.mk A B <*> Vec.mk A C)
- ((Vec.mk A C <*> Vec.mk A B) - (Vec.mk A B <*> Vec.mk A B)) : by rw distOfInnerP1
... = (Vec.mk A C <*> Vec.mk A C) - (Vec.mk A B <*> Vec.mk A C)
- (Vec.mk A C <*> Vec.mk A B) + (Vec.mk A B <*> Vec.mk A B) : by rw ℕminus1
... = (Vec.mk A C <*> Vec.mk A C) - (Vec.mk A C <*> Vec.mk A B)
- (Vec.mk A C <*> Vec.mk A B) + (Vec.mk A B <*> Vec.mk A B) : by rw commOfInnerP (Vec.mk A C) (Vec.mk A B)
... = (Vec.mk A C <*> Vec.mk A C) - 2 * (Vec.mk A C <*> Vec.mk A B)
+ (Vec.mk A B <*> Vec.mk A B) : by rw ℕminus2
... = norm (Vec.mk A C) * norm (Vec.mk A C)
- 2 * (Vec.mk A C <*> Vec.mk A B)
+ (Vec.mk A B <*> Vec.mk A B) : by rw difInnerP2
... = norm (Vec.mk A C) * norm (Vec.mk A C)
- 2 * (Vec.mk A C <*> Vec.mk A B)
+ norm (Vec.mk A B) * norm (Vec.mk A B) : by rw difInnerP2
... = norm (Vec.mk A C) * norm (Vec.mk A C)
- 2 * (norm (Vec.mk A C) * norm (Vec.mk A B) * cos A)
+ norm (Vec.mk A B) * norm (Vec.mk A B) : by rw difInnerP1
... = norm (Vec.mk A C) * norm (Vec.mk A C)
- 2 * norm (Vec.mk A C) * norm (Vec.mk A B) * cos A
+ norm (Vec.mk A B) * norm (Vec.mk A B) : by rw ℕmulti1
... = b * b
- 2 * b * norm (Vec.mk A B) * cos A
+ norm (Vec.mk A B) * norm (Vec.mk A B) : by rw lemma_b b
... = b * b - 2 * b * c * cos A + c * c : by rw lemma_c c
... = b * b + c * c - 2 * b * c * cos A : by rw ℕcomm1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment