feat(CombinatoryLogic): SKI realizers of data

Cslib/Foundations/Semantics/Realizes.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Waring
+-/
+
+module
+
+public import Cslib.Foundations.Data.Relation
+
+@[expose] public section
+
+namespace Cslib
+
+open Relation
+
+/-- A type `α` has "realisers" in some calculus `β`. -/
+class HasRealizer (α β : Type*) where
+  /-- A term represents (realizes) a element. -/
+  Realizes : β → α → Prop
+
+def Realizes {α β : Type*} [HasRealizer α β] : β → α → Prop := HasRealizer.Realizes
+
+scoped notation x " ⊩ " a => Realizes x a
+
+/-- Types for which the realisability relation is invariant by anti-reduction. -/
+class HasRealizerLift (α : Type*) {β : Type*} (r : β → β → Prop) extends HasRealizer α β where
+  /-- Realisers lift along reductions. -/
+  realizes_left_of_red : {a : α} → {x y : β} → (y ⊩ a) → r x y → x ⊩ a
+
+/-- Types for which the realisability relation is invariant by reduction. -/
+class HasRealizerDesc (α : Type*) {β : Type*} (r : β → β → Prop) extends HasRealizer α β where
+  /-- Realisers descend along reductions. -/
+  realizes_right_of_red : {a : α} → {x y : β} → (x ⊩ a) → r x y → y ⊩ a
+
+variable {α β : Type*} {r : β → β → Prop}
+
+lemma Realizes.left_of_red [HasRealizerLift α r] {a : α} {x y : β} (ha : y ⊩ a) (h : r x y) :
+    x ⊩ a := HasRealizerLift.realizes_left_of_red ha h
+
+lemma Realizes.left_of_mRed [HasRealizerLift α r] {a : α} {x y : β} (ha : y ⊩ a)
+    (h : (ReflTransGen r) x y) : x ⊩ a := by
+  induction h with
+  | refl => assumption
+  | tail h h' ih => exact ih <| ha.left_of_red h'
+
+lemma Realizes.right_of_red [HasRealizerDesc α r] {a : α} {x y : β} (ha : x ⊩ a) (h : r x y) :
+    y ⊩ a := HasRealizerDesc.realizes_right_of_red ha h
+
+lemma Realizes.right_of_mRed [HasRealizerDesc α r] {a : α} {x y : β} (ha : x ⊩ a)
+    (h : (ReflTransGen r) x y) : y ⊩ a := by
+  induction h with
+  | refl => assumption
+  | tail h h' ih => exact ih.right_of_red h'
+
+end Cslib

Cslib/Languages/CombinatoryLogic/Basic.lean

@@ -187,6 +187,13 @@ theorem C_def (f x y : SKI) : (C ⬝ f ⬝ x ⬝ y) ↠ f ⬝ y ⬝ x :=
 lemma C_head_mred (f x y z : SKI) (h : (f ⬝ y) ↠ z) : (C ⬝ f ⬝ x ⬝ y) ↠ z ⬝ x :=
   Trans.trans (C_def f x y) (MRed.head x h)
 
+/-- W := λ f x. f x x -/
+def WPoly : SKI.Polynomial 2 := &0 ⬝' &1 ⬝' &1
+/-- A SKI term representing W -/
+def W : SKI := WPoly.toSKI
+theorem W_def (f x : SKI) : (W ⬝ f ⬝ x) ↠ f ⬝ x ⬝ x :=
+  WPoly.toSKI_correct [f, x] (by simp)
+
 /-- Rotate right: RotR := λ x y z. z x y -/
 def RotRPoly : SKI.Polynomial 3 := &2 ⬝' &0 ⬝' &1
 /-- A SKI term representing RotR -/
@@ -250,134 +257,6 @@ def Th : SKI := ThAux ⬝ ThAux
 /-- A SKI term representing Θ -/
 theorem Th_correct (f : SKI) : (Th ⬝ f) ↠ f ⬝ (Th ⬝ f) := ThAux_def ThAux f
 
-/-! ### Church Booleans -/
-
-/-- A term a represents the boolean value u if it is βη-equivalent to a standard Church boolean. -/
-def IsBool (u : Bool) (a : SKI) : Prop :=
-  ∀ x y : SKI, (a ⬝ x ⬝ y) ↠ (if u then x else y)
-
-theorem isBool_trans (u : Bool) (a a' : SKI) (h : a ↠ a') (ha' : IsBool u a') :
-    IsBool u a := by
-  intro x y
-  trans a' ⬝ x ⬝ y
-  · apply MRed.head
-    apply MRed.head
-    exact h
-  · exact ha' x y
-
-/-- Standard true: TT := λ x y. x -/
-def TT : SKI := K
-@[scoped grind .]
-theorem TT_correct : IsBool true TT := fun x y ↦ MRed.K x y
-
-/-- Standard false: FF := λ x y. y -/
-def FF : SKI := K ⬝ I
-@[scoped grind .]
-theorem FF_correct : IsBool false FF :=
-  fun x y ↦ calc
-    (FF ⬝ x ⬝ y) ↠ I ⬝ y := by apply Relation.ReflTransGen.single; apply red_head; exact red_K I x
-    _         ⭢ y := red_I y
-
-/-- Conditional: Cond x y b := if b then x else y -/
-protected def Cond : SKI := RotR
-theorem cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) :
-    (SKI.Cond ⬝ x ⬝ y ⬝ a) ↠ if u then x else y := by
-  trans a ⬝ x ⬝ y
-  · exact rotR_def x y a
-  · exact h x y
-
-/-- Neg := λ a. Cond FF TT a -/
-protected def Neg : SKI := SKI.Cond ⬝ FF ⬝ TT
-theorem neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (¬ ua) (SKI.Neg ⬝ a) := by
-  apply isBool_trans (a' := if ua then FF else TT)
-  · apply cond_correct (h := h)
-  · cases ua
-    · simp [TT_correct]
-    · simp [FF_correct]
-
-/-- And := λ a b. Cond (Cond TT FF b) FF a -/
-def AndPoly : SKI.Polynomial 2 := SKI.Cond ⬝' (SKI.Cond ⬝ TT ⬝ FF ⬝' &1) ⬝' FF ⬝' &0
-/-- A SKI term representing And -/
-protected def And : SKI := AndPoly.toSKI
-theorem and_def (a b : SKI) : (SKI.And ⬝ a ⬝ b) ↠ SKI.Cond ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ FF ⬝ a :=
-  AndPoly.toSKI_correct [a, b] (by simp)
-
-theorem and_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) :
-    IsBool (ua && ub) (SKI.And ⬝ a ⬝ b) := by
-  apply isBool_trans (a' := SKI.Cond ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ FF ⬝ a) (h := and_def _ _)
-  cases ua
-  · simp_rw [Bool.false_and] at ⊢
-    apply isBool_trans (a' := FF) (ha' := FF_correct) (h := cond_correct a _ _ false ha)
-  · simp_rw [Bool.true_and] at ⊢
-    apply isBool_trans (a' := SKI.Cond ⬝ TT ⬝ FF ⬝ b) (h := cond_correct a _ _ true ha)
-    apply isBool_trans (a' := if ub = true then TT else FF) (h := cond_correct b _ _ ub hb)
-    cases ub
-    · simp [FF_correct]
-    · simp [TT_correct]
-
-/-- Or := λ a b. Cond TT (Cond TT FF b) b -/
-def OrPoly : SKI.Polynomial 2 := SKI.Cond ⬝' TT ⬝' (SKI.Cond ⬝ TT ⬝ FF ⬝' &1) ⬝' &0
-/-- A SKI term representing Or -/
-protected def Or : SKI := OrPoly.toSKI
-theorem or_def (a b : SKI) : (SKI.Or ⬝ a ⬝ b) ↠ SKI.Cond ⬝ TT ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ a :=
-  OrPoly.toSKI_correct [a, b] (by simp)
-
-theorem or_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) :
-  IsBool (ua || ub) (SKI.Or ⬝ a ⬝ b) := by
-  apply isBool_trans (a' := SKI.Cond ⬝ TT ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ a) (h := or_def _ _)
-  cases ua
-  · simp_rw [Bool.false_or]
-    apply isBool_trans (a' := SKI.Cond ⬝ TT ⬝ FF ⬝ b) (h := cond_correct a _ _ false ha)
-    apply isBool_trans (a' := if ub = true then TT else FF) (h := cond_correct b _ _ ub hb)
-    cases ub
-    · simp [FF_correct]
-    · simp [TT_correct]
-  · apply isBool_trans (a' := TT) (h := cond_correct a _ _ true ha)
-    simp [TT_correct]
-
-/- TODO?: other boolean connectives -/
-
-/-! ### Pairs -/
-
-/-- MkPair := λ a b. ⟨a,b⟩ -/
-def MkPair : SKI := SKI.Cond
-/-- First projection -/
-def Fst : SKI := R ⬝ TT
-/-- Second projection -/
-def Snd : SKI := R ⬝ FF
-
-@[scoped grind .]
-theorem fst_correct (a b : SKI) : (Fst ⬝ (MkPair ⬝ a ⬝ b)) ↠ a := by calc
-  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _
-  _ ↠ a := cond_correct TT a b true TT_correct
-
-@[scoped grind .]
-theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by calc
-  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _
-  _ ↠ b := cond_correct FF a b false FF_correct
-
-/-- Unpaired f ⟨x, y⟩ := f x y, cf `Nat.unparied`. -/
-def UnpairedPoly : SKI.Polynomial 2 := &0 ⬝' (Fst ⬝' &1) ⬝' (Snd ⬝' &1)
-/-- A term representing Unpaired -/
-protected def Unpaired : SKI := UnpairedPoly.toSKI
-theorem unpaired_def (f p : SKI) : (SKI.Unpaired ⬝ f ⬝ p) ↠ f ⬝ (Fst ⬝ p) ⬝ (Snd ⬝ p) :=
-  UnpairedPoly.toSKI_correct [f, p] (by simp)
-
-theorem unpaired_correct (f x y : SKI) : (SKI.Unpaired ⬝ f ⬝ (MkPair ⬝ x ⬝ y)) ↠ f ⬝ x ⬝ y := by
-  trans f ⬝ (Fst ⬝ (MkPair ⬝ x ⬝ y)) ⬝ (Snd ⬝ (MkPair ⬝ x ⬝ y))
-  · exact unpaired_def f _
-  · apply parallel_mRed
-    · apply MRed.tail
-      exact fst_correct _ _
-    · exact snd_correct _ _
-
-/-- Pair f g x := ⟨f x, g x⟩, cf `Primrec.Pair`. -/
-def PairPoly : SKI.Polynomial 3 := MkPair ⬝' (&0 ⬝' &2) ⬝' (&1 ⬝' &2)
-/-- A SKI term representing Pair -/
-protected def Pair : SKI := PairPoly.toSKI
-theorem pair_def (f g x : SKI) : (SKI.Pair ⬝ f ⬝ g ⬝ x) ↠ MkPair ⬝ (f ⬝ x) ⬝ (g ⬝ x) :=
-  PairPoly.toSKI_correct [f, g, x] (by simp)
-
 end SKI
 
 end Cslib

Cslib/Languages/CombinatoryLogic/Evaluation.lean

@@ -209,7 +209,7 @@ lemma sk_nequiv : ¬ MJoin Red S K := by
   cases (redexFree_iff_mred_eq.1 hK _).1 hkz
 
 /-- Injectivity for booleans. -/
-theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool v y)
+theorem realizes_bool_injective (x y : SKI) (u v : Bool) (hx : x ⊩ u) (hy : y ⊩ v)
     (hxy : MJoin Red x y) : u = v := by
   have h : MJoin Red (if u then S else K) (if v then S else K) := by
     apply mJoin_red_equivalence.trans (y := x ⬝ S ⬝ K)
@@ -223,7 +223,8 @@ theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool
   grind [sk_nequiv, mJoin_red_equivalence.symm h]
 
 lemma TF_nequiv : ¬ MJoin Red TT FF := fun h =>
-  (Bool.eq_not_self true).mp <| isBool_injective TT FF true false TT_correct FF_correct h
+  (Bool.eq_not_self true).mp <|
+    realizes_bool_injective TT FF true false realizes_true realizes_false h
 
 /-- A specialisation of `Church : Nat → SKI`. -/
 def churchK : Nat → SKI
@@ -247,7 +248,7 @@ lemma churchK_injective : Function.Injective churchK :=
   fun n m h => by simpa using congrArg SKI.size h
 
 /-- Injectivity for Church numerals -/
-theorem isChurch_injective (x y : SKI) (n m : Nat) (hx : IsChurch n x) (hy : IsChurch m y)
+theorem realizes_nat_injective (x y : SKI) (n m : Nat) (hx : x ⊩ n) (hy : y ⊩ m)
     (hxy : MJoin Red x y) : n = m := by
   suffices MJoin Red (churchK n) (churchK m) by
     apply churchK_injective
@@ -283,15 +284,15 @@ theorem rice {P : SKI} (hP : ∀ x : SKI, ((P ⬝ x) ↠ TT) ∨ (P ⬝ x) ↠ F
       _ ↠ P ⬝ (Neg ⬝ Abs) := by apply MRed.tail; apply fixedPoint_correct
       _ ↠ P ⬝ (P ⬝ Abs ⬝ b ⬝ a) := by apply MRed.tail; apply Neg_app
       _ ↠ P ⬝ (TT ⬝ b ⬝ a) := by apply MRed.tail; apply MRed.head; apply MRed.head; exact h
-      _ ↠ P ⬝ b := by apply MRed.tail; apply TT_correct
+      _ ↠ P ⬝ b := by apply MRed.tail; apply realizes_true
       _ ↠ FF := hb
     exact TF_nequiv <| MRed.diamond h this
   case inr h =>
     have : (P ⬝ Abs) ↠ TT := calc
       _ ↠ P ⬝ (Neg ⬝ Abs) := by apply MRed.tail; apply fixedPoint_correct
       _ ↠ P ⬝ (P ⬝ Abs ⬝ b ⬝ a) := by apply MRed.tail; apply Neg_app
       _ ↠ P ⬝ (FF ⬝ b ⬝ a) := by apply MRed.tail; apply MRed.head; apply MRed.head; exact h
-      _ ↠ P ⬝ a := by apply MRed.tail; apply FF_correct
+      _ ↠ P ⬝ a := by apply MRed.tail; apply realizes_false
       _ ↠ TT := ha
     exact TF_nequiv <| MRed.diamond this h