Twitterで「ベクトルを使うと5秒位で余弦定理証明できるので良い」
とあったので、Idris, Leanでチャレンジしてみた。
参考記事：
ちなみに、余弦定理の証明に、
（成分表示で証明した）内積の分配法則を
使ってしまうと循環論法になるそうです。
自分は仮定のままにしてあります。
今回は、無条件の仮定である
postulate(axiom)をたくさん使っています。
Idris版
なかなかえぐい感じになった。
Lean版
Leanって、小数型ないのですかね。
LeanはReasoning内でrwを使えるので、
今回はLeanの方がIdrisよりやりやすかったです。
.
.
