SKIコンビネータを実装する例

えびさんによる例:

/-!
  # LeanでSKIコンビネータを定義して遊ぶ

  ## モチベーション
  - SKIコンビネータをLean上で定義したい
  - `S K x` と `I` が同じであることを示したい
  - 正規形の一意性を証明したい
  - 評価関数を定義して遊べるようにしたい

-/

/--
  (Wikipediaより) SKIコンビネータ論理の項は次の規則により帰納的に定義される：
  1. 定数記号（ここではS、K、I）及び変数記号は項である。この形の項を原子（atom）という。
  2. M と N が項ならば, (MN)は項である。この形の項を適用（application）という。
  3. 以上より項とわかるもののみを項という。
-/
inductive Term where
  | S | K | I | Var (name : String)
  | App (M : Term) (N : Term)
deriving Repr, DecidableEq, Inhabited

open Term

#check (S.App K).App K -- SKK を表現した式

-- 毎回 `.App` とか書くのが面倒なので、マクロを定義する
declare_syntax_cat ski
syntax "S" : ski
syntax "K" : ski
syntax "I" : ski
syntax:10 ski:10 ski:11 : ski -- 10や11は適用が左結合と解釈されるようにするための優先度指定
syntax ident : ski  -- M N R などの項の中に登場する変数がLeanの環境上の項を参照している場合
syntax name : ski -- 項の中に登場する変数をatomとして扱う場合。バッククォートをつけて書く
syntax "(" ski ")" : ski  -- 括弧で囲む表記
syntax hole : ski -- 滅多に使わないので消しても良いかも

syntax "[|" ski "]" : term
open Lean Macro in macro_rules
  | `([| S ]) => `(Term.S)
  | `([| K ]) => `(Term.K)
  | `([| I ]) => `(Term.I)
  | `([| $m:ski $n:ski ]) => `(Term.App [| $m ] [| $n ])
  | `([| $i:ident ]) => `($i)
  | `([| $n:name ]) => do
    -- `hoge などのNameリテラルを "hoge" のようにStringリテラルに変換する
    let name := n.getName |> toString |> Syntax.mkStrLit
    `(Term.Var $name)
  | `([| ( $t:ski )]) => `([| $t ])
  | `([| _ ]) => `(_)

section
  /-- info: (S.App K).App K : Term -/
  #guard_msgs in #check [| S K K ]  -- 項が書きやすくなった

  -- 原子(atom)としての変数項
  /-- info: ((S.App (Var "M")).App (Var "N")).App (Var "R") : Term -/
  #guard_msgs in #check [| S `M `N `R ]
  /-- info: ((Var "M").App (Var "R")).App ((Var "N").App (Var "R")) : Term -/
  #guard_msgs in #check [| `M `R (`N `R) ]

  -- M N R という変数名で Term 型の値が存在していた場合
  /-- info: fun M N R => ((S.App M).App N).App R : Term → Term → Term → Term -/
  #guard_msgs in #check fun M N R => [| S M N R ]
end

/--
  (Wikipediaより) 変数記号を含まない項を閉項といい、SKIのみから構成される項を結合子（コンビネータ）という。適用は左結合であるものとし、括弧を省略するのが普通である。SKIコンビネータ計算は次の簡約規則
  - S M N R ⟶ M R (N R)
  - K M N   ⟶ M
  - I M     ⟶ M
  からなる項書換え系である。
-/
inductive Eval1 : Term → Term → Prop where
  | E_S (M N R : Term) : Eval1 [| S M N R ] [| M R (N R) ]
  | E_K (M N : Term) : Eval1 [| K M N ] [| M ]
  | E_I (M : Term) : Eval1 [| I M ] [| M ]
  -- Wikipediaには載ってないけどこの2つの規則がないと複雑な項は簡約が止まってしまうので入れておく
  | E_AppLeft {M N M' : Term} (M_M' : Eval1 M M') : Eval1 [| M N ] [| M' N ]
  | E_AppRight {M N N' : Term} (N_N' : Eval1 N N') : Eval1 [| M N ] [| M N' ]

-- (書籍「型システム入門」にならって、) t を1ステップ評価すると t' になるという命題を `t ⟶ t'` と表す
@[inherit_doc] infix:60 " ⟶ " => Eval1

example : [| S M N R ] ⟶ [| M R (N R) ] := by apply Eval1.E_S

/-- t を1ステップ評価する先が存在しないとき、 `t は正規形である` という -/
def Term.isNormalForm (t : Term) : Prop := ¬ ∃ t', t ⟶ t'

-- 1ステップ評価の一意性が成り立っていない
def Eval1.Determination : Prop := ∀ t t' t'', t ⟶ t' → t ⟶ t'' → t' = t''
theorem Eval1.not_uniq : ¬ Eval1.Determination := by
  simp [Determination]
  let t := [| K I (I K) ]
  let t' := [| I ]
  let t'' := [| K I K ]
  have t_t' : t ⟶ t' := by apply Eval1.E_K
  have t_t'' : t ⟶ t'' := by apply Eval1.E_AppRight; apply Eval1.E_I
  exists t; exists t'; simp [t_t']; exists t''
  done

/-- t が0回以上の評価で t' になることを多ステップ評価と呼び、 `t ⟶* t'` と表す -/
inductive EvalMulti : Term → Term → Prop where
  | E_Self (t : Term) : EvalMulti t t
  | E_Step {t t' t''} (t_t': t ⟶ t') (t'__t'': EvalMulti t' t'') : EvalMulti t t''
@[inherit_doc] infix:60 " ⟶* " => EvalMulti

/-- 多ステップ評価関係は推移的 -/
theorem EvalMulti.trans {t t' t'' : Term} (t__t' : t ⟶* t') (t'__t'' : t' ⟶* t'') : t ⟶* t'' := by
  induction t__t'
  case E_Self => assumption
  case E_Step u u' u'' u_u' _u__u'' ind_h =>
    have u'__t'' := ind_h t'__t''
    exact EvalMulti.E_Step u_u' u'__t''
  done

/-- 正規形を多ステップ評価しても変化しない -/
theorem EvalMulti.nf_eq {nf x : Term} (nf__x : nf ⟶* x) (nf_h : nf.isNormalForm)
  : x = nf := by
  cases nf__x
  . rfl
  . rename_i h _; exact nf_h ⟨_, h⟩ |>.elim

-- calcを使えるようにしておく
instance : Trans (· ⟶ ·) (· ⟶* ·) (· ⟶* ·) := ⟨EvalMulti.E_Step⟩
instance : Trans (· ⟶* ·) (· ⟶* ·) (· ⟶* ·) := ⟨EvalMulti.trans⟩
instance : Trans (· ⟶ ·) (· ⟶ ·) (· ⟶* ·) where
  trans a_b b_c := EvalMulti.E_Step a_b (EvalMulti.E_Step b_c (EvalMulti.E_Self _))
instance : Trans (· ⟶* ·) (· ⟶ ·) (· ⟶* ·) where
  trans a__b b_c := EvalMulti.trans a__b (EvalMulti.E_Step b_c (EvalMulti.E_Self _))

-- `S K x M` と `I M` が共に `M` に多ステップ評価できることが示せる
theorem I_identity : ∀ M, [| I M ] ⟶* [| M ] := by
  intro M
  calc
    [| I M ] ⟶ [| M ] := Eval1.E_I ..
    [| M ] ⟶* [| M ] := EvalMulti.E_Self ..

theorem SKx_identity (x : Term) : ∀ M, [| (S K x) M ] ⟶* [| M ] := by
  intro M
  calc
    [| (S K x) M ] ⟶ [| K M (x M) ] := Eval1.E_S ..
    [| K M (x M) ] ⟶ [| M ] := Eval1.E_K ..

/-- EvalMEq は2つの項が多ステップ評価すると同じになるという関係を表す -/
def EvalMEq : Term → Term → Prop := fun t1 t2 => ∃ t', t1 ⟶* t' ∧ t2 ⟶* t'

example : EvalMEq [| S K x M ] [| I M ] := by
  exists M
  simp [I_identity, SKx_identity]

-- `EvalMEq`が同値関係である(反射率、対称率、推移率が成り立つ)ことは後で証明する

-- Wikipediaに載っていた「式の逆転」の例
example (α β : Term) : [| S (K (S I)) K α β ] ⟶* [| β α ] := calc
  _ ⟶ [| (K (S I) α) (K α) β ] := Eval1.E_AppLeft (Eval1.E_S ..)
  _ ⟶ [| S I (K α) β ] := Eval1.E_AppLeft (Eval1.E_AppLeft (Eval1.E_K ..))
  _ ⟶ [| (I β) (K α β) ] := Eval1.E_S ..
  _ ⟶ [| (I β) α ] := Eval1.E_AppRight (Eval1.E_K ..)
  _ ⟶ [| β α ] := Eval1.E_AppLeft (Eval1.E_I ..)

-- メモ: ↑の証明を自動化するタクティクが作れたら便利そう

-- SKIコンビネータには停止しない項が存在する
example : [| (S I I) (S I I) ] ⟶* [| (S I I) (S I I) ] := calc
  _ ⟶ [| I (S I I) (I (S I I)) ] := Eval1.E_S ..
  _ ⟶ [| (I (S I I)) (S I I) ] := Eval1.E_AppRight (Eval1.E_I ..)
  _ ⟶ [| (S I I) (S I I) ] := Eval1.E_AppLeft (Eval1.E_I ..)

-- TODO: この項が停止しない(正規形を持たない)ことの証明をちゃんとしたいが、なんかむずかった
def Term.hasNF (t : Term) : Prop := ∃ n, t ⟶* n ∧ n.isNormalForm

example : ∃ t : Term, ¬ t.hasNF := by
  simp only [hasNF, not_exists, not_and]
  let t := [| (S I I) (S I I) ]
  exists t
  sorry

/-
  ## 合流性を証明したいよね？

  SKIコンビネータは項によっては簡約候補が複数ある
  次の簡約先の選び方次第で、簡約が停止したりしなかったりする場合もある

  そこで次の問いが生まれる
  1. 停止する可能性がある項の簡約先を恣意的に選んだ結果、停止する可能性を失うことは有り得るか？
  2. 簡約先の選び方によって正規形が複数存在することは有り得るか？

  どちらもNOであってほしい。つまり、
  1. 任意の項 t について、 t ⟶* nf (nf は正規形) の時、任意の項 t' (t ⟶* t') において t' ⟶* nf が成り立つ
  2. t ⟶* nf (nf は正規形) かつ t ⟶* nf' (nf' は正規形) の時、 nf = nf'
  が成り立つかを調べたい

  実はSKIコンビネータが [合流性](https://ja.wikipedia.org/wiki/%E5%90%88%E6%B5%81%E6%80%A7) と呼ばれる性質を持つならこの2つも成り立つことを示せる
  合流性の証明は [Fabian Kunze, Confluence in SK using parallel reduction, 2015](https://www.ps.uni-saarland.de/~kunze/intern_download/SK-Confluence.pdf) を参考にした
-/

-- 合流性の定義
def Confluence := ∀ {a b c}, a ⟶* b → a ⟶* c → ∃ d, b ⟶* d ∧ c ⟶* d

/--
  SKIコンビネータは1ステップ評価の決定性がないので、Eval1が扱いづらくなっている

  例えば項`S M N R`を考えると、`R ⟶ R'`の時に
  E_AppRightからE_Sだと2回で `M R' (N R')`となるが、
  E_Sを先にやると E_S -> E_AppLeft -> E_AppRight と3回必要になる

  これが合流性の証明を面倒にするので、Eval1とEvalMultiの中間であるParallel Reductionを導入する
-/
inductive ParEval : Term → Term → Prop where
  | E_Self (t : Term) : ParEval t t
  | E_S (M N R : Term) : ParEval [| S M N R ] [| M R (N R) ]
  | E_K (M N : Term) : ParEval [| K M N ] [| M ]
  | E_I (M : Term) : ParEval [| I M ] [| M ]
  | E_App (M_M' : ParEval M M') (N_N' : ParEval N N') : ParEval [| M N ] [| M' N' ]
@[inherit_doc] infix:60 " ⇒ " => ParEval

-- 使いそうな補題を適当に用意しておく
section
  @[simp] def Eval1.left {l r : Term} (_h : l ⟶ r) := l
  @[simp] def Eval1.right {l r : Term} (_h : l ⟶ r) := r
  @[simp] def ParEval.left {l r : Term} (_h : l ⇒ r) := l
  @[simp] def ParEval.right {l r : Term} (_h : l ⇒ r) := r
  @[simp] def EvalMulti.left {l r : Term} (_h : l ⟶* r) := l
  @[simp] def EvalMulti.right {l r : Term} (_h : l ⟶* r) := r

  @[simp] theorem Eval1.E_S' {M N R} : [| S M N R ] ⟶ [| M R (N R) ] := Eval1.E_S ..
  @[simp] theorem Eval1.E_K' {M N} : [| K M N ] ⟶ [| M ] := Eval1.E_K ..
  @[simp] theorem Eval1.E_I' {M} : [| I M ] ⟶ [| M ] := Eval1.E_I ..

  @[simp] theorem ParEval.refl (t : Term) : t ⇒ t := ParEval.E_Self ..
  @[simp] theorem ParEval.E_S' {M N R} : [| S M N R ] ⇒ [| M R (N R) ] :=
    ParEval.E_S ..
  @[simp] theorem ParEval.E_K' {M N} : [| K M N ] ⇒ [| M ] := ParEval.E_K ..
  @[simp] theorem ParEval.E_I' {M} : [| I M ] ⇒ [| M ] := ParEval.E_I ..

  @[simp] theorem EvalMulti.refl (t : Term) : t ⟶* t := EvalMulti.E_Self ..
  @[simp] theorem EvalMulti.E_S' {M N R} : [| S M N R ] ⟶* [| M R (N R) ] := by
    apply EvalMulti.E_Step; apply Eval1.E_S ..; simp
  @[simp] theorem EvalMulti.E_K' {M N} : [| K M N ] ⟶* [| M ] := by
    apply EvalMulti.E_Step; apply Eval1.E_K ..; simp
  @[simp] theorem EvalMulti.E_I' {M} : [| I M ] ⟶* [| M ] := by
    apply EvalMulti.E_Step; apply Eval1.E_I ..; simp

  theorem EvalMulti.E_AppLeft {M N M'} (M__M' : M ⟶* M') : [| M N ] ⟶* [| M' N ] := by
    induction M__M' with
    | E_Self _ => simp
    | E_Step M_m _m__M' ih =>
      apply EvalMulti.E_Step (by apply Eval1.E_AppLeft; assumption)
      assumption

  theorem EvalMulti.E_AppRight {M N N'} (N__N' : N ⟶* N') : [| M N ] ⟶* [| M N' ] := by
    induction N__N' with
    | E_Self _ => simp
    | E_Step N_n _n__N' ih =>
      apply EvalMulti.E_Step (by apply Eval1.E_AppRight; assumption)
      assumption
end

theorem ParEval.ofEval1 {t t' : Term} : t ⟶ t' → t ⇒ t'
  | .E_S _ _ _ => by apply ParEval.E_S
  | .E_K _ _ => by apply ParEval.E_K
  | .E_I _ => by apply ParEval.E_I
  | .E_AppLeft h => by apply ParEval.E_App (ParEval.ofEval1 h) (ParEval.E_Self _)
  | .E_AppRight h => by apply ParEval.E_App (ParEval.E_Self _) (ParEval.ofEval1 h)

theorem ParEval.toMulti {t t'} (h : t ⇒ t') : t ⟶* t' := by
  cases h <;> try simp
  . rename_i M_M' N_N'
    cases M_M'
    . apply EvalMulti.E_AppRight; apply ParEval.toMulti; assumption
    . apply EvalMulti.trans
      . apply EvalMulti.E_AppLeft; apply EvalMulti.E_S'
      . apply EvalMulti.E_AppRight; apply ParEval.toMulti; assumption
    . apply EvalMulti.trans
      . apply EvalMulti.E_AppLeft; apply EvalMulti.E_K'
      . apply EvalMulti.E_AppRight; apply ParEval.toMulti; assumption
    . apply EvalMulti.trans
      . apply EvalMulti.E_AppLeft; apply EvalMulti.E_I'
      . apply EvalMulti.E_AppRight; apply ParEval.toMulti; assumption
    . apply EvalMulti.trans
      . apply EvalMulti.E_AppRight; apply ParEval.toMulti; assumption
      . apply EvalMulti.trans <;> apply EvalMulti.E_AppLeft
        . apply EvalMulti.E_AppLeft; apply ParEval.toMulti; assumption
        . apply EvalMulti.E_AppRight; apply ParEval.toMulti; assumption

theorem ParEval.diamond (a_b : a ⇒ b) (a_c : a ⇒ c) : ∃ d, b ⇒ d ∧ c ⇒ d := by
  match a_b, a_c with
  | .E_Self _, _ => exists c; simpa | _, .E_Self _ => exists b; simpa
  | .E_S M N R, .E_S _ _ _ => exists [| M R (N R) ]; simp
  | .E_K M N, .E_K _ _ => exists [| M ]; simp
  | .E_I M, .E_I _ => exists M; simp
  | .E_S _ _ _, .E_App L_L' R_R' | .E_App L_L' R_R', .E_S _ _ _ =>
    try
      guard_target =~ ∃ d, [| _ _ _ ] ⇒ d ∧ _
      rename_i M N R _ R'
    try
      guard_target =~ ∃ d, _ ∧ [| _ _ _ ] ⇒ d
      rename_i M N _ R R'
    cases L_L'
    . exists [| M R' (N R') ]; simp only [E_S', and_true, true_and]
      apply ParEval.E_App <;> apply ParEval.E_App <;> simp_all
    . rename_i N' L_L' N_N'; cases L_L'
      . exists [| M R' (N' R') ]; simp only [E_S', and_true, true_and]
        apply ParEval.E_App <;> apply ParEval.E_App <;> simp_all
      . rename_i S' M' S_S' M_M'; cases S_S'; exists [| M' R' (N' R') ]; simp only [E_S', and_true, true_and]
        apply ParEval.E_App <;> apply ParEval.E_App <;> simp_all
  | .E_K _ _, .E_App L_L' N_N' | .E_App L_L' N_N', .E_K _ _ =>
    cases L_L'
    . try { exists b; simp }; try { exists c; simp }
    . rename_i M' L_L' M_M'; cases L_L'; exists M'; simp_all
  | .E_I _, .E_App L_L' R_R' | .E_App L_L' R_R', .E_I _ =>
    cases L_L'; exists R_R'.right; simp_all
  | .E_App L_L'1 R_R'1, .E_App L_L'2 R_R'2 =>
    have ⟨M', M'_h⟩ := diamond L_L'1 L_L'2
    have ⟨N', N'_h⟩ := diamond R_R'1 R_R'2
    exists [| M' N' ]; constructor <;> apply ParEval.E_App <;> simp_all
  done

theorem interleaved_diamond (a_b : a ⇒ b) (a__c : a ⟶* c) : ∃ d, b ⟶* d ∧ c ⇒ d := by
  induction a__c generalizing b; { exists b; simpa }; case E_Step a_a' _a'__c ih =>
  clear a c; rename_i a a' c
  have ⟨b', a'_b', b_b'⟩ := ParEval.diamond (ParEval.ofEval1 a_a') a_b
  obtain ⟨d, b'__d, c_d⟩ := ih a'_b'
  have b__d : b ⟶* d := EvalMulti.trans b_b'.toMulti b'__d
  exists d

theorem semi_confluence (a_b : a ⟶ b) (a__c : a ⟶* c) : ∃ d, b ⟶* d ∧ c ⟶* d := by
  have ⟨d, b__d, c_d⟩ := interleaved_diamond (ParEval.ofEval1 a_b) a__c
  have c__d : c ⟶* d := c_d.toMulti
  exists d

/-- 合流性の証明 -/
theorem confluence : Confluence := by
  intro a b c a__b a__c
  induction a__b generalizing c; { exists c; simpa }; case E_Step a_a' _a'__b ih =>
  rename_i a a' b
  obtain ⟨d', a'__d', c__d'⟩ := semi_confluence a_a' a__c
  obtain ⟨d, b__d, d'__d⟩ := ih a'__d'
  have c__d : c ⟶* d := EvalMulti.trans c__d' d'__d
  exists d

/-
  証明したかったことのおさらい

  以下の疑問があった
  1. 停止する可能性がある項の簡約先を恣意的に選んだ結果、停止する可能性を失うことは有り得るか？
  2. 簡約先の選び方によって正規形が複数存在することは有り得るか？

  これを否定するために次の2つを証明する
  1. 任意の項 t について、 t ⟶* nf (nf は正規形) の時、任意の項 t' (t ⟶* t') において t' ⟶* nf が成り立つ
  2. t ⟶* nf (nf は正規形) かつ t ⟶* nf' (nf' は正規形) の時、 nf = nf'
-/

/--
  任意の項 t について、 t ⟶* nf (nf は正規形) の時、任意の項 t' (t ⟶* t') において t' ⟶* nf が成り立つ
  言い換えると、 t の簡約先をどう選んだとしてもその簡約先から nf に簡約できる
-/
example (t__nf : t ⟶* nf) (nf_h : nf.isNormalForm) (t__t' : t ⟶* t') : t' ⟶* nf := by
  obtain ⟨x, nf__x, t'__x⟩ := confluence t__nf t__t'
  have : x = nf := nf__x.nf_eq nf_h
  rw [this] at t'__x
  assumption

/-- 正規形の一意性 -/
theorem Term.nf_determination (t : Term) (t__nf : t ⟶* nf) (nf_h : nf.isNormalForm)
  (t__nf' : t ⟶* nf') (nf'_h : nf'.isNormalForm) : nf = nf' := by
  obtain ⟨nf'', nf__nf'', nf'__nf''⟩ := confluence t__nf t__nf'
  cases nf__nf''; case E_Step h _ => exfalso; apply nf_h; exists h.right
  cases nf'__nf''; case E_Step h _ => exfalso; apply nf'_h; exists h.right
  rfl

-- EvalMEqが同値関係になっていることも、合流性から示せる
instance : Setoid Term where
  r := EvalMEq
  iseqv := {
    refl := by intro x; exists x; simp [EvalMulti.E_Self]
    symm := by intro _ _ ⟨t', ⟨h1, h2⟩⟩; exists t'; done
    trans := by
      intro x y z ⟨xy, x__xy, y__xy⟩ ⟨yz, y__yz, z__yz⟩
      obtain ⟨xz, xy__xz, yz__xz⟩ := confluence y__xy y__yz
      have x__xz : x ⟶* xz := EvalMulti.trans x__xy xy__xz
      have z__xz : z ⟶* xz := EvalMulti.trans z__yz yz__xz
      exists xz
  }

-- `Setoid Term` を実装したので同値であることを表す記号が使えるようになった
example : [| S K x M ] ≈ [| I M ] := by
  exists M; simp [SKx_identity, I_identity]

/-
  ## 評価関数を定義してみる
  定義した関数と`Eval1`の関係についても調べたい
-/

/-- 項を1ステップ評価する。項が正規形なら `eval1 t = t` となる -/
def eval1 : Term → Term
  | [| S M N R ]  => [| M R (N R) ]
  | [| K M _N ]   => [| M ]
  | [| I M ]      => [| M ]
  | [| M N ]      =>
    let M' := eval1 M
    if M ≠ M' then [| M' N ]
    else
      let N' := eval1 N
      if N ≠ N' then [| M N' ]
      else [| M N ]
  | t             => t

/-
  `eval1`関数が定義できたので、この関数と評価関係との間に整合性があることを証明したい
  (例えば `(eval1 t = t' ∧ t ≠ t') ↔ t ⟶ t'` のような命題)

  ちなみに↑の例は証明できない
  1ステップ評価の一意性がないので `t ⟶ t'` であっても `eval1 t = t'` とは限らないため
  左から右は示せるが、右から左は主張を弱めないと成り立たない
-/

theorem Eval1.not_eq {t t' : Term} (h : t ⟶ t') : t ≠ t' := by
  intro eq_h
  rw [eq_h] at h
  cases h
  . rename_i M_M'; nomatch Eval1.not_eq M_M'
  . rename_i N_N'; nomatch Eval1.not_eq N_N'

theorem eval1_Eval1 {t t' : Term} (h : eval1 t = t') (not_eq : t ≠ t') : t ⟶ t' := by
  rw [← h]
  cases t; any_goals (simp [eval1]; contradiction)
  rename_i M N
  unfold eval1; split
  . rename_i heq; rw [heq]; apply Eval1.E_S
  . rename_i heq; rw [heq]; apply Eval1.E_K
  . rename_i heq; rw [heq]; apply Eval1.E_I
  . rename_i heq; injection heq
    rename_i eq1 eq2; simp [eq1, eq2] at *
    split
    . split
      . rename_i eq1 eq2; simp [eval1] at h
        split at h <;> contradiction
      . apply Eval1.E_AppRight; apply eval1_Eval1 <;> trivial
    . apply Eval1.E_AppLeft; apply eval1_Eval1 <;> trivial
  . simp_all [eval1]
  done

theorem Eval1_ex_eval1 {t t' : Term} (t_t' : t ⟶ t') : ∃ t'', eval1 t = t'' ∧ t ≠ t'' := by
  cases t_t' <;> simp [eval1] <;> intro h <;> try cases h
  . rename_i M_M'
    unfold eval1 at h; split at h <;> rename_i heq <;> rw [h] at heq <;> try cases heq
    . simp at heq h; rw [heq] at h; injection h with eq1 eq2; simp [eq1, eq2] at *
      have ⟨M'', ⟨_, _⟩⟩ := Eval1_ex_eval1 M_M'
      simp_all
    . apply heq _ _ h
  . rename_i N_N'
    unfold eval1 at h; split at h <;> rename_i heq <;> rw [h] at heq <;> try cases heq
    . simp at heq h; rw [heq] at h; injection h with eq1 eq2; simp [eq1, eq2] at *
      rename_i M _ _ _ _
      rcases Decidable.em (M = eval1 M) with h | h <;> try simp [← h] at *
      have ⟨N'', ⟨_, _⟩⟩ := Eval1_ex_eval1 N_N'
      simp_all
      simp_all
    . apply heq _ _ h
  done

theorem eq_eval1_nf {t : Term} (h : t = eval1 t) : t.isNormalForm := by
  intro ⟨t', t_t'⟩
  cases t_t'
  . nomatch h
  . nomatch h
  . nomatch h

  all_goals
    rename_i X_X'
    unfold eval1 at h; split at h <;> rename_i heq
    . rw [heq] at h; nomatch h
    . rw [heq] at h; nomatch h
    . rw [heq] at h; nomatch h
    rotate_left
    . apply heq _ _ h
    injection heq with eq1 eq2
    simp [eq1, eq2] at *
    have ⟨X'', h1, _⟩ := Eval1_ex_eval1 X_X'

  . simp_all
  . rename_i M _ _ _ _ _
    rcases Decidable.em (M = eval1 M) with h | h <;> try simp [← h] at *
    all_goals simp_all
  done

-- `eval1` のおかげで項が正規形かどうかが決定的に示せるようになった
instance {t : Term} : Decidable t.isNormalForm := by
  apply Decidable.byCases (p := t = eval1 t) <;> intro h
  . apply Decidable.isTrue; apply eq_eval1_nf; assumption
  . apply Decidable.isFalse
    have := eval1_Eval1 rfl h
    intro h; apply h; exists eval1 t

def not_nf_ex_Eval1 {t : Term} (h : ¬ t.isNormalForm) : { t' // t ⟶ t' } := by
  exists eval1 t
  have not_eq : t ≠ eval1 t := by intro h; have := eq_eval1_nf h; contradiction
  apply eval1_Eval1 rfl not_eq

-- TODO: t ⟶ t' の関係が成り立つかどうかを機械的に判定するアルゴリズム。うまく書けなかった
instance {t t' : Term} : Decidable (t ⟶ t') := sorry

-- 項が停止するとは限らないので、この関数の停止性は証明できない(partialをつけるしかない)
partial def evalM (t : Term) : Term :=
  if eval1 t = t then t
  else evalM (eval1 t)

#guard evalM [| S (K (S I)) K `α `β ] = [| `β `α ]

/-
  ## SKIコンビネータでFizzBuzz書ける？
  ラムダ計算の式からそれと等価なSKIコンビネータの式を導出するアルゴリズムがある
  SKIコンビネータで思い通りの関数を直接書き下すのは多分無理なので、ラムダ計算を経由しよう
  ということで、もしラムダ計算でFizzBuzzを書いたことがなければまずそっちをやった方が良いです

  僕もやろうとしたけど手作業での変換が面倒すぎて無理だったので、機械的な変換を実現できたら再チャレンジしたい

  以下はWikipediaに載っていた、SKIコンビネータで論理演算を実装する例
-/

def T := [| K ]
def F := [| S K ]
#guard evalM [| T `x `y ] = [| `x ]
#guard evalM [| F `x `y ] = [| `y ]

def NOT := [| S (S I (K F)) (K T) ]
#guard evalM [| NOT T ] = F
#guard evalM [| NOT F ] = T

def OR := [| S I (K T) ]
#guard evalM [| OR (NOT T) F ] = F
#guard evalM [| OR (NOT T) (NOT F) ] = T

def AND := [| S S (K (K F)) ]
#guard evalM [| AND T (NOT F) ] = T
#guard evalM [| AND T F ] = evalM [| NOT (OR (NOT T) (NOT F)) ]

No target file or test is named. Start by reading the Term, Eval1, EvalMulti, and ParEval definitions in the issue body, then identify where this example belongs in the repository. Done should include the stated SKI evaluation goals and resolve the unfinished sorry proof, with the intended scope clarified first.