Lean4 学習8

Lean4 で証明とプログラムをうまく組み合わせたものが書けないか色々試している。証明を書いて、その具体的な値を使って何かするといったことがなかなかうまく出来ず、何となくこれでいいんじゃないかな、という方法が少しわかったのでメモしておく。単体を定義して具体的な点を取得してみた。本当は Vector で書きたかったが、sum メソッドがないということなので一旦 List で書いた。by simp の部分は脳死で書いている。

import Mathlib

def pos := { x : List Nat // (∀ i : Fin 3, x[i]! ≥ 0) ∧ x.sum = 1 }

theorem h : ∀ i: Fin 3, [1, 0, 0][i]! ≥ 0 := fun i =>
  let l := [1, 0, 0]
  match i with
  | 0 => calc l[0] = 1 := by simp
                 _ ≥ 0 := by simp
  | 1 => calc l[1] = 0 := by simp
                 _ ≥ 0 := by simp
  | 2 => calc l[2] = 0 := by simp
                 _ ≥ 0 := by simp
theorem g : [1, 0, 0].sum = 1 := by simp

def l : pos := ⟨[1, 0, 0], ⟨h, g⟩⟩ 
def ll : pos := ⟨[1, 0, 0], And.intro h g⟩ 
def lll : pos := Subtype.mk [1, 0, 0] (And.intro h g)
-- def llll : pos := ⟨[1, 0, 0], h ∧ g⟩ -- error (なんか間違っている？)

#eval l
#eval ll

感想

最初、具体的な def l : List Nat := [1, 0, 0] が l ∈ pos であることを示そうと思ったが、pos は型なのでうまくいかず、かといってキャストなどができるかと言えば情報が見つからず悩んでいた。しかし、証明付きで Subtype のコンストラクタに渡せばいいということがわかり、これを使えば具体的な値に関して話を進められるかもしれない。