Software Fundations を Lean4 で書き直す

[Seasawher]

@aconite-ac @haruhisa-enomoto

https://softwarefoundations.cis.upenn.edu/

Software Foundations というのは Coq で書かれた教科書です．これの Lean 版はないようですが，Coq と Lean は似ているので書き直すことが比較的容易にできるのではないかと思います．

全巻を書き直すとなると大変ですし，おそらく頓挫しますが，Volume 3 の挿入ソートの話だけ，とかそういう風に部分的に翻案するのでもおもしろいと思います．

[s-taiga]

こちらの書籍ですが、以下に日本語訳がありますので、こちらを利用されると作業進めやすいかもしれないです。
http://proofcafe.org/sf/toc.html
ただ、確か少し古いバージョンに対する訳で一部内容が違った記憶があります。

[Seasawher]

ありがとうございます
日本語訳があったんですね
困った時に助かりそうです

software fundations に関しては、英語でleanに翻訳したものも存在しないと思うので、本気でleanに翻訳するならまずは英語で作るべきという気もちょっとしています。
Zulip で相談してみます。

[Seasawher]

とりあえず insertion sort の性質の証明をやってみたいです！

冒頭の，配列がソート済みであることの定義を書き直してみました

• https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.html

import Mathlib.Tactic

/-- 
the formal definition of what "array is sorted" means.
-/
def Sorted : List Nat → Prop
| [] => true
| [_] => true
| x :: y :: as => x ≤ y ∧ Sorted (y :: as) 

-- check the above definition by proving trivial results!
example : Sorted [1, 2] := by
  rw [Sorted]
  constructor
  · norm_num
  · rfl

-- [2, 1] is not sorted!
example : ¬ Sorted [2, 1] := by
  dsimp [Sorted]
  push_neg
  intro h
  contradiction