Lean4 学習6
パターンマッチを書いている時、
match xs with | [] => [] | y::ys => _
としたときに二番目にマッチしたケースでは 0 < xs.length が成り立っていて欲しいけどそれはダメみたい？そう言う場合はどうすればいいか？素直に if h : 0 < xs.length then ... else ... で書くか？こうすれば補題 h を後続で使用できるらしい。しかしその場合 y::ys が使えないので要素にアクセスできない。let で書いてしまえばいいか？if 内で let で分解した場合、補題 h も 0 < (y::ys).length に分解されるようだ。
List をインデックス付きの List にする zipIndices 関数を書いてみた
def zipIndices {α : Type} (xs : List α) : List ((Fin xs.length) × α) :=
let rec f (ys : List α) (hx : 0 < xs.length) : List ((Fin xs.length) × α) :=
if hy : 0 < ys.length then
let y::ys := ys
({ val := xs.length - (y::ys).length, isLt := (Nat.sub_lt hx hy) }, y)::(f ys hx)
else []
if h : 0 < xs.length then f xs h
else []
なんか条件分岐が多くて醜い。再帰のローカル関数必要だろうか？ h : 0 < xs.length を与えてあげれば単純な再帰で直せるか？しかしインデックスを計算するためには大元の xs にアクセスする必要があるのでそれは難しいかもしれない。zip 関数を定義して、0 ~ n までのリストを返す seq n みたいな関数を定義してやるのが本来なのかもしれない。
本来やりたかったことは以下の定理を示すことだった。時系列の状態をもったデータが並んでいる時に状態が遷移したことの証明として、状態 A の最小値と状態 B の最大値が発生時刻を前後して現れていればいい、と言うもの。(なんかこれ自明じゃない？とか示せると嬉しいの？みたいな疑問が湧いているけど)
theorem exists_iff_min_lt_max (xs : List Status) (s1 : Status) (s2 : Status) : min xs s1 < max xs s2 ↔ ∃ i j : Fin xs.length, i < j ∧ xs.get i = s1 ∧ xs.get j = s2 := sorry
そのために条件を満たす最小/最大のインデックスを返す min/max を定義したいが、その前に色々必要で zipIndices を定義することにした。
