VSnoc

Fin.snocの件がようやく落ち着いてきた

とりあえずFin.snocの件はこれでほとんど問題ないはず。

import Mathlib.Data.Set.Basic
import Mathlib.Data.Fin.Tuple.Basic

universe u

namespace VSnoc

variable {V: Type u}

/-- Fin.snoc for the type V-/
def VSnoc {n : ℕ} (xs : Fin n → V) (b : V):= (fun (k : Fin (n + 1)) => if h : k.val < n then xs (Fin.castLT k h) else b)

/-- Fin.snoc = VSnoc when applied to V-/
theorem VSnoc_lemma {n : ℕ} {xs : Fin n → V} {b : V} : Fin.snoc xs b = VSnoc xs b:= by
  exact rfl

/-- VSnoc xs a n = a when xs : Fin n → V -/
@[simp]
theorem VSnoc_last {n : ℕ} (xs : Fin n → V) (a : V) : (VSnoc xs a) (Fin.last n) = a := by
  rw [← VSnoc_lemma]
  simp

/-- VSnoc xs a k.castSucc = xs k when xs : Fin n → V and k : Fin n-/
@[simp]
theorem VSnoc_init {V : Type u} {n : ℕ} {xs : Fin n → V} {a : V} {k : Fin n} : VSnoc xs a k.castSucc = xs k := by
  rw [← VSnoc_lemma]
  simp

end VSnoc

VSnocはまあ見たまんまかな。Fin.castLT k hは{n m : \N}が暗黙的に与えられているときにk : Fin mとh : k.val<nからk : Fin nとキャストされたものを作る。なお、Fin.snocはなんかわかりづらいので一応自分で書いた。 VSnoc_lemmaはFin.snocからVSnocへの書き換え。そのまんま。 VSnoc_lastはVSnoc xs aの最後の元に関するもの。xs : Fin n→Vなら (VSnoc xs a) : Fin (n+1)→Vなので、Fin.last n、すなわち(n : Fin (n+1))を代入したらaが出てくるというもの。simpで証明できてしまう。 VSnoc_initはVSnoc xs aのそれ以外の元に関するもの。xs : Fin n→Vかつk : Fin nのときはVSnoc xs aのk番目の元はxs kになる。k.castSuccで(k : Fin(n+1))と一つ上のFinにキャストしたものを得られる。

xs : Fin n→Vのときに、例えばVSnoc (VSnoc (VSnoc xs a) b) cを考えると

• VSnoc (VSnoc (VSnoc xs a) b) c n = a
• VSnoc (VSnoc (VSnoc xs a) b) c (n +1) = b
• VSnoc (VSnoc (VSnoc xs a) b) c (n + 2) = c

となる。これが直接自動的に出てくれば文句はないのだけれども、キャスティングの関係で出てこないので、これを下記のように書き直してやると、simp [VSnoc_init, VSnoc_last]で等式が証明できる。

• VSnoc (VSnoc (VSnoc xs a) b) c (Fin.last n).castSucc.castSucc = a
• VSnoc (VSnoc (VSnoc xs a) b) c (Fin.last (n +1)).castSucc = b
• VSnoc (VSnoc (VSnoc xs a) b) c (Fin.last (n + 2)) = c

例えば３行目の証明はこれ。

example {n : ℕ} {xs : Fin n → V} {a b c: V} : VSnoc (VSnoc (VSnoc xs a) b) c (n + 2) = c := by
  have h : (n+2 : Fin (n+3)) = Fin.last (n+2) := by
    -- apply Fin.eq_last_of_not_lt
    apply Fin.eq_of_val_eq
    simp [Fin.val_add]
  simp [h, VSnoc_last]

Fin.eq_of_va_eqは(k1 k2 : Fin n)に対して、k1.val=k2.valならばk1=k2というもの。valというのはFin n型のオブジェクトの値を得るもの。k : Fin nは、k.val : ℕとk.isLT : k.val < nから成り立っていて、その前者。これは自明っぽいのだけれども、(n+2 : Fin (n+3))は( (n : Fin (n+3)) + (2 : Fin (n+3)) )と解釈されるので、これの値がn+2になるのはそんなに自明じゃなくて、そこの橋渡しをするのがFin.val_add。正確には

theorem Fin.val_add{n : Nat} (a b : Fin n) : ↑(a + b) = (↑a + ↑b) % n

あ、%nはLeanではnで割った余りのこと。(a +b).val<nが成り立っていないといけないのだけれども、それをnで割ったあまりをとることで回避している。 simp に[]で囲んで定理などをいれると、それらを使ったうえで簡略化してくれる。simp [h, VSnoc_last]でhを使って(n+2)をFin.last (n+2)にしてからVSnoc_lastを適用する。

1行目は

example {n : ℕ} {xs : Fin n → V} {a b c: V} : VSnoc (VSnoc (VSnoc xs a) b) c n = a := by
  have h : (n : Fin (n+3))= (Fin.last n).castSucc.castSucc := by
    apply Fin.eq_of_val_eq
    simp
    omega
  simp [h, VSnoc_init, VSnoc_last]

でいける。

面倒ではあるんだけど、Fin.snocの扱いで毎日何時間も溶かしていたのでとりあえず証明できる筋道ができたのは本当に良かった。自動化はチャレンジしたいけどひとまずこれで行く。

次回予告

論理式による関係の記述とそれを内側と外側で解釈する方法、そしてそれが関数かどうかの判定について書く予定。