search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
47 stars 7 forks source link

`rify` タクティクを紹介する #806

Open Seasawher opened 1 month ago

Seasawher commented 1 month ago

レイリーの定理の証明で以下のように役に立つ場面があった。

      /-
      x : ℕ
      r : ℝ
      xpos : x > 0
      rpos : r > 0
      nmem : x ∉ Beatty r
      M : ℕ := ⌊↑x / r⌋₊
      lem : 0 ≤ ↑x / r
      le : ↑M * r ≤ ↑x
      hx : ↑M * r = ↑x
      ⊢ M > 0
      -/

      -- これは `x > 0` より従う。
      rify at xpos ⊢
      nlinarith
Seasawher commented 1 month ago

何気に nlinarith が健闘している場面でもある。

Seasawher commented 1 month ago

これは型キャスト系のタクティクである。こういう、タクティクの系統についての情報をタグなどで管理できると良いのだけど…