From b3c145aaef6a400e2fb8ad9bfce68e45b194f8b1 Mon Sep 17 00:00:00 2001 From: twwar Date: Thu, 19 Feb 2026 01:54:32 +0100 Subject: [PATCH 01/12] Deterministic relations --- Cslib/Foundations/Data/Relation.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index ea8b154f8..515da1475 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -417,6 +417,21 @@ theorem reflTransGen_compRel : ReflTransGen (SymmGen r) = EqvGen r := by exact reflTransGen_swap.mp ih | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ +/-- A relation is deterministic if any term on the left is related to at most one term on the +right. This is the same as Mathlib's `Relator.RightUnique`, which is not currently imported. -/ +abbrev Deterministic {α β : Type*} (r : α → β → Prop) : Prop := ∀ {x y y'}, r x y → r x y' → y = y' + +theorem Deterministic.toSemiConfluent (hr : Deterministic r) : SemiConfluent r := by + intro _ _ _ h' h + obtain (rfl | ⟨_, hxz, hzy'⟩) := h'.cases_head + · apply symmetric_join + exact join_of_single reflexive_reflTransGen (.single h) + · rw [← hr hxz h] + exact MJoin.single hzy' + +theorem Deterministic.toConfluent (hr : Deterministic r) : Confluent r := + SemiConfluent.toConfluent hr.toSemiConfluent + public meta section open Lean Elab Meta Command Term From 477246544cd168dc112ee1a2d522c755f153c884 Mon Sep 17 00:00:00 2001 From: twwar Date: Thu, 19 Feb 2026 02:04:01 +0100 Subject: [PATCH 02/12] use new API in URM, docs --- Cslib/Computability/URM/Execution.lean | 31 ++++---------------------- Cslib/Foundations/Data/Relation.lean | 8 +++---- 2 files changed, 8 insertions(+), 31 deletions(-) diff --git a/Cslib/Computability/URM/Execution.lean b/Cslib/Computability/URM/Execution.lean index 9aa62505e..858e26527 100644 --- a/Cslib/Computability/URM/Execution.lean +++ b/Cslib/Computability/URM/Execution.lean @@ -84,8 +84,7 @@ namespace Step variable {p : Program} /-- The step relation is deterministic: each state has at most one successor. -/ -theorem deterministic {s s' s'' : State} (h1 : Step p s s') (h2 : Step p s s'') : s' = s'' := by - grind +theorem deterministic : Relation.Deterministic (Step p) := by grind /-- A halted state has no successor in the step relation. -/ theorem no_step_of_halted {s s' : State} (hhalted : s.isHalted p) : ¬Step p s s' := by @@ -132,32 +131,10 @@ theorem isHalted_iff_normal {p : Program} {s : State} : · exact hnormal ⟨_, Step.jump_eq (hp ▸ hinstr) heq⟩ · exact hnormal ⟨_, Step.jump_ne (hp ▸ hinstr) heq⟩ -/-- The step relation is confluent. - -For a deterministic relation, any two execution paths from the same state must follow -the same sequence of steps, so if both reach some state, they reach the same state. -We prove this directly rather than via Diamond since Diamond requires the relation -to always have successors. -/ +/-- The step relation is confluent. -/ theorem step_confluent (p : Program) : Relation.Confluent (Step p) := by - intro init s₁ s₂ h1 h2 - -- Two multi-step reductions from init must follow the same path due to determinism - induction h1 using Relation.ReflTransGen.head_induction_on generalizing s₂ with - | refl => - -- s₁ = init, so s₂ is reachable from s₁ - exact ⟨s₂, h2, Relation.ReflTransGen.refl⟩ - | head hstep_a hrest_a ih => - -- init → a → ... → s₁ - cases h2 using Relation.ReflTransGen.head_induction_on with - | refl => - -- s₂ = init, so s₁ is reachable from s₂ - exact ⟨s₁, Relation.ReflTransGen.refl, Relation.ReflTransGen.head hstep_a hrest_a⟩ - | head hstep_b hrest_b => - -- init → b → ... → s₂ - -- By determinism, a = b - have heq := Step.deterministic hstep_a hstep_b - subst heq - -- Now both paths go through the same intermediate state - exact ih hrest_b + apply Relation.Deterministic.toConfluent + exact Step.deterministic namespace Steps diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 515da1475..8047c3746 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -422,11 +422,11 @@ right. This is the same as Mathlib's `Relator.RightUnique`, which is not current abbrev Deterministic {α β : Type*} (r : α → β → Prop) : Prop := ∀ {x y y'}, r x y → r x y' → y = y' theorem Deterministic.toSemiConfluent (hr : Deterministic r) : SemiConfluent r := by - intro _ _ _ h' h - obtain (rfl | ⟨_, hxz, hzy'⟩) := h'.cases_head + intro _ _ _ (h : ReflTransGen r _ _) (h' : r _ _) + obtain (rfl | ⟨_, hxz, hzy'⟩) := h.cases_head -- either h starts with a step or is refl · apply symmetric_join - exact join_of_single reflexive_reflTransGen (.single h) - · rw [← hr hxz h] + exact join_of_single reflexive_reflTransGen (.single h') + · rw [← hr hxz h'] -- in the second case the first step of h must be h' exact MJoin.single hzy' theorem Deterministic.toConfluent (hr : Deterministic r) : Confluent r := From aaeee961b85e3b1bce2e52970dcedbb79ac13f5e Mon Sep 17 00:00:00 2001 From: twwar Date: Thu, 19 Feb 2026 02:12:12 +0100 Subject: [PATCH 03/12] use `RightUnique` API --- Cslib/Foundations/Data/Relation.lean | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 8047c3746..3b9c55224 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -417,20 +417,14 @@ theorem reflTransGen_compRel : ReflTransGen (SymmGen r) = EqvGen r := by exact reflTransGen_swap.mp ih | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ -/-- A relation is deterministic if any term on the left is related to at most one term on the -right. This is the same as Mathlib's `Relator.RightUnique`, which is not currently imported. -/ -abbrev Deterministic {α β : Type*} (r : α → β → Prop) : Prop := ∀ {x y y'}, r x y → r x y' → y = y' - -theorem Deterministic.toSemiConfluent (hr : Deterministic r) : SemiConfluent r := by - intro _ _ _ (h : ReflTransGen r _ _) (h' : r _ _) - obtain (rfl | ⟨_, hxz, hzy'⟩) := h.cases_head -- either h starts with a step or is refl - · apply symmetric_join - exact join_of_single reflexive_reflTransGen (.single h') - · rw [← hr hxz h'] -- in the second case the first step of h must be h' - exact MJoin.single hzy' - -theorem Deterministic.toConfluent (hr : Deterministic r) : Confluent r := - SemiConfluent.toConfluent hr.toSemiConfluent +/-- `Relator.RightUnique` corresponds to deterministic reductions, which are confluent. -/ +theorem Relator.RightUnique.Confluent (hr : Relator.RightUnique r) : + Confluent r := by + intro a b c ab ac + obtain (h | h) := ReflTransGen.total_of_right_unique hr ab ac + · use c + · use b + public meta section From c4b2a8651728ae7e3e952decb2c47c1e2a3ad10f Mon Sep 17 00:00:00 2001 From: twwar Date: Thu, 19 Feb 2026 02:15:05 +0100 Subject: [PATCH 04/12] update URM --- Cslib/Computability/URM/Execution.lean | 4 ++-- Cslib/Foundations/Data/Relation.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Computability/URM/Execution.lean b/Cslib/Computability/URM/Execution.lean index 858e26527..d7ed02756 100644 --- a/Cslib/Computability/URM/Execution.lean +++ b/Cslib/Computability/URM/Execution.lean @@ -84,7 +84,7 @@ namespace Step variable {p : Program} /-- The step relation is deterministic: each state has at most one successor. -/ -theorem deterministic : Relation.Deterministic (Step p) := by grind +theorem deterministic : Relator.RightUnique (Step p) := by grind [Relator.RightUnique] /-- A halted state has no successor in the step relation. -/ theorem no_step_of_halted {s s' : State} (hhalted : s.isHalted p) : ¬Step p s s' := by @@ -133,7 +133,7 @@ theorem isHalted_iff_normal {p : Program} {s : State} : /-- The step relation is confluent. -/ theorem step_confluent (p : Program) : Relation.Confluent (Step p) := by - apply Relation.Deterministic.toConfluent + apply Relation.RightUnique.toConfluent exact Step.deterministic namespace Steps diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 3b9c55224..6b8a47d98 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -418,7 +418,7 @@ theorem reflTransGen_compRel : ReflTransGen (SymmGen r) = EqvGen r := by | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ /-- `Relator.RightUnique` corresponds to deterministic reductions, which are confluent. -/ -theorem Relator.RightUnique.Confluent (hr : Relator.RightUnique r) : +theorem RightUnique.toConfluent (hr : Relator.RightUnique r) : Confluent r := by intro a b c ab ac obtain (h | h) := ReflTransGen.total_of_right_unique hr ab ac From 9eb9b4ff610abb0561aaeafc1cc35525379afd4f Mon Sep 17 00:00:00 2001 From: twwar Date: Thu, 19 Feb 2026 02:16:27 +0100 Subject: [PATCH 05/12] docs --- Cslib/Foundations/Data/Relation.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 6b8a47d98..8ae25614d 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -417,7 +417,9 @@ theorem reflTransGen_compRel : ReflTransGen (SymmGen r) = EqvGen r := by exact reflTransGen_swap.mp ih | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ -/-- `Relator.RightUnique` corresponds to deterministic reductions, which are confluent. -/ +/-- `Relator.RightUnique` corresponds to deterministic reductions, which are confluent, as all +multi-reductions with a common origin start the same (this fact is +`Relation.ReflTransGen.total_of_right_unique`.) -/ theorem RightUnique.toConfluent (hr : Relator.RightUnique r) : Confluent r := by intro a b c ab ac @@ -425,7 +427,6 @@ theorem RightUnique.toConfluent (hr : Relator.RightUnique r) : · use c · use b - public meta section open Lean Elab Meta Command Term From 887786c904aab156d9f496691bb6adba821da0d0 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 18 Feb 2026 20:35:33 -0500 Subject: [PATCH 06/12] move signature to one line --- Cslib/Foundations/Data/Relation.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 8ae25614d..180f181ad 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -420,8 +420,7 @@ theorem reflTransGen_compRel : ReflTransGen (SymmGen r) = EqvGen r := by /-- `Relator.RightUnique` corresponds to deterministic reductions, which are confluent, as all multi-reductions with a common origin start the same (this fact is `Relation.ReflTransGen.total_of_right_unique`.) -/ -theorem RightUnique.toConfluent (hr : Relator.RightUnique r) : - Confluent r := by +theorem RightUnique.toConfluent (hr : Relator.RightUnique r) : Confluent r := by intro a b c ab ac obtain (h | h) := ReflTransGen.total_of_right_unique hr ab ac · use c From f8176c7d0c90564759b248af2a620283c95e6142 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 6 Mar 2026 17:15:03 +0100 Subject: [PATCH 07/12] encodings, recursion --- Cslib/Foundations/Semantics/Encoded.lean | 56 +++ Cslib/Languages/CombinatoryLogic/Basic.lean | 128 ------ Cslib/Languages/CombinatoryLogic/Encoded.lean | 232 +++++++++++ .../Languages/CombinatoryLogic/Recursion.lean | 375 ++++++++---------- 4 files changed, 452 insertions(+), 339 deletions(-) create mode 100644 Cslib/Foundations/Semantics/Encoded.lean create mode 100644 Cslib/Languages/CombinatoryLogic/Encoded.lean diff --git a/Cslib/Foundations/Semantics/Encoded.lean b/Cslib/Foundations/Semantics/Encoded.lean new file mode 100644 index 000000000..f7058fd28 --- /dev/null +++ b/Cslib/Foundations/Semantics/Encoded.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 + +/-- Types encoded some calculus. -/ +class Encoded (α β : Type*) where + /-- An element is represented by a term. -/ + IsEncoding : α → β → Prop + +def IsEncoding {α β : Type*} [Encoded α β] : α → β → Prop := Encoded.IsEncoding + +scoped notation x " ⊩ " a => IsEncoding a x + +/-- Types for which encodings are invariant by anti-reduction. -/ +class EncodedLift (α : Type*) {β : Type*} (r : β → β → Prop) extends Encoded α β where + /-- Representation lifts along reductions. -/ + isEncoding_left_of_red : {a : α} → {x y : β} → (y ⊩ a) → r x y → x ⊩ a + +/-- Types for which encodings are invariant by reduction. -/ +class EncodedDesc (α : Type*) {β : Type*} (r : β → β → Prop) extends Encoded α β where + /-- Representation descends along reductions. -/ + isEncoding_right_of_red : {a : α} → {x y : β} → (x ⊩ a) → r x y → y ⊩ a + +variable {α β : Type*} {r : β → β → Prop} + +lemma IsEncoding.left_of_red [EncodedLift α r] {a : α} {x y : β} (ha : y ⊩ a) (h : r x y) : + x ⊩ a := EncodedLift.isEncoding_left_of_red ha h + +lemma IsEncoding.left_of_mRed [EncodedLift α 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 IsEncoding.right_of_red [EncodedDesc α r] {a : α} {x y : β} (ha : x ⊩ a) (h : r x y) : + y ⊩ a := EncodedDesc.isEncoding_right_of_red ha h + +lemma IsEncoding.right_of_mRed [EncodedDesc α 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 diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index e8743062a..beaa86519 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -250,134 +250,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 diff --git a/Cslib/Languages/CombinatoryLogic/Encoded.lean b/Cslib/Languages/CombinatoryLogic/Encoded.lean new file mode 100644 index 000000000..e27d310fa --- /dev/null +++ b/Cslib/Languages/CombinatoryLogic/Encoded.lean @@ -0,0 +1,232 @@ +/- +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.Languages.CombinatoryLogic.Basic +public import Cslib.Foundations.Semantics.Encoded + +@[expose] public section + +namespace Cslib.SKI + +open Red MRed Relation Encoded IsEncoding + +/-- A term `xf` encodes a function `f : α → β` if for every `xa ⊩ a : α`, `xf ⬝ a ⊩ f a`. -/ +instance instEncodedPi (α β : Type*) [hα : Encoded α SKI] [hβ : Encoded β SKI] : + Encoded (α → β) SKI where + IsEncoding f z := ∀ {a : α} {x : SKI}, (x ⊩ a) → (z ⬝ x) ⊩ (f a) + +instance instEncodedLiftPi (α β : Type*) [hα : Encoded α SKI] [hβ : EncodedLift β Red] : + EncodedLift (α → β) Red where + isEncoding_left_of_red := by + intro f x y hy h a z hz + apply EncodedLift.isEncoding_left_of_red (hy hz) + exact red_head _ _ _ h + +instance instEncodedDescPi (α β : Type*) [hα : Encoded α SKI] [hβ : EncodedDesc β Red] : + EncodedDesc (α → β) Red where + isEncoding_right_of_red := by + intro f x y hy h a z hz + apply EncodedDesc.isEncoding_right_of_red (hy hz) + exact red_head _ _ _ h + +/-! +### Booleans + +`xu ⊩ u` if `xu` is βη-equivalent to the standard Church boolean. +-/ + +instance instEncodedLiftBool : EncodedLift Bool Red where + IsEncoding u z := ∀ x y : SKI, (z ⬝ x ⬝ y) ↠ (if u then x else y) + isEncoding_left_of_red := by + intro u x y hu h a b + trans y ⬝ a ⬝ b + · apply MRed.head; apply MRed.head; exact Relation.ReflTransGen.single h + · exact hu a b + + +/-- Standard true: TT := λ x y. x -/ +def TT : SKI := K + +@[scoped grind .] +theorem TT_correct : TT ⊩ true := fun x y ↦ MRed.K x y + +/-- Standard false: FF := λ x y. y -/ +def FF : SKI := K ⬝ I + +@[scoped grind .] +theorem FF_correct : FF ⊩ false := + 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 + +lemma cond_def {xu y z} {u : Bool} (hu : xu ⊩ u) : + (SKI.Cond ⬝ y ⬝ z ⬝ xu) ↠ if u then y else z := by + cases u + all_goals { + trans xu ⬝ y ⬝ z + · exact rotR_def .. + · exact hu .. + } + +lemma isEncoding_cond {α : Type*} [EncodedLift α Red] : + SKI.Cond ⊩ (fun (a b : α) (u : Bool) => if u then a else b) := by + intro a xa ha b xb hb u xu hu + cases u + case false => + exact hb.left_of_mRed <| cond_def hu + case true => + exact ha.left_of_mRed <| cond_def hu + +/-! +### Pairs + +`xp ⊩ ⟨a, b⟩` if `Fst ⬝ xp ⊩ a` and `Snd ⬝ xp ⊩ b`, where `Fst` and `Snd` are the canonical +projections. We note that this breaks the "Church encoding" pattern, which would define encodings +of a product by its recursor, ie `xp ⊩ ⟨a, b⟩` if for every `f`, `xp ⬝ f ↠ f ⬝ xa ⬝ xb` for some +`xa ⊩ a` and `xb ⊩ b`. +-/ + +/-- 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 := calc + _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _ + _ ↠ TT ⬝ a ⬝ b := rotR_def .. + _ ⭢ a := red_K .. + +@[scoped grind .] +theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by calc + _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _ + _ ↠ FF ⬝ a ⬝ b := rotR_def .. + _ ⭢ I ⬝ b := red_head _ _ b <| red_K .. + _ ⭢ b := red_I b + +instance instEncodedProd {α β : Type*} [Encoded α SKI] [Encoded β SKI] : Encoded (α × β) SKI where + IsEncoding p x := ((Fst ⬝ x) ⊩ p.1) ∧ (Snd ⬝ x) ⊩ p.2 + +instance instEncodedLiftProd {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : + EncodedLift (α × β) Red where + isEncoding_left_of_red := by + intro p x y ⟨hp₁, hp₂⟩ h + constructor + · apply hp₁.left_of_mRed + exact Relation.ReflTransGen.single <| red_tail Fst _ _ h + · apply hp₂.left_of_mRed + exact Relation.ReflTransGen.single <| red_tail Snd _ _ h + +instance instEncodedDescProd {α β : Type*} [EncodedDesc α Red] [EncodedDesc β Red] : + EncodedDesc (α × β) Red where + isEncoding_right_of_red := by + intro p x y ⟨hp₁, hp₂⟩ h + constructor + · apply hp₁.right_of_mRed + exact Relation.ReflTransGen.single <| red_tail Fst _ _ h + · apply hp₂.right_of_mRed + exact Relation.ReflTransGen.single <| red_tail Snd _ _ h + +/-- The pairing term `SKI.MkPair` indeed encodes `Prod.Mk`. -/ +lemma isEncoding_mkPair {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : + SKI.MkPair ⊩ (Prod.mk : α → β → α × β) := by + intro a xa ha b xb hb + constructor + · exact ha.left_of_mRed <| fst_correct .. + · exact hb.left_of_mRed <| snd_correct .. + +lemma isEncoding_fst {α β : Type*} [Encoded α SKI] [Encoded β SKI] : + SKI.Fst ⊩ (Prod.fst : α × β → α) := by + intro _ _ h + exact h.1 + +lemma isEncoding_snd {α β : Type*} [Encoded α SKI] [Encoded β SKI] : + SKI.Snd ⊩ (Prod.snd : α × β → β) := by + intro _ _ h + exact h.2 + +def prodRecPoly : SKI.Polynomial 2 := &0 ⬝' (Fst ⬝' &1) ⬝' (Snd ⬝' &1) +/-- The term which will encode `Prod.rec`. -/ +def prodRec := prodRecPoly.toSKI +lemma prodRec_def (xf xp : SKI) : (prodRec ⬝ xf ⬝ xp) ↠ xf ⬝ (Fst ⬝ xp) ⬝ (Snd ⬝ xp) := + prodRecPoly.toSKI_correct [xf, xp] (by simp) + +theorem isEncoding_prod_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] + [EncodedLift γ Red] : prodRec ⊩ (Prod.rec : (α → β → γ) → α × β → γ) := by + intro f xf hf p xp hp + exact (hf hp.1 hp.2).left_of_mRed <| prodRec_def .. + +/-! +### Sums + +`xab ⊩ s : α ⊕ β` if for every `f, g`, `xab ⬝ f ⬝ g` reduces to `f ⬝ xa`, for `s = .inl a` and +`xa ⊩ a`, or `g ⬝ xb`, for `s = .inr b` and `xb ⊩ b`. +-/ + +def isEncodingSum {α β : Type*} [Encoded α SKI] [Encoded β SKI] : α ⊕ β → SKI → Prop + | .inl a, x => ∀ f g : SKI, ∃ xa : SKI, (xa ⊩ a) ∧ (x ⬝ f ⬝ g) ↠ f ⬝ xa + | .inr b, x => ∀ f g : SKI, ∃ xb : SKI, (xb ⊩ b) ∧ (x ⬝ f ⬝ g) ↠ g ⬝ xb + +instance instEncodedSum {α β : Type*} [Encoded α SKI] [Encoded β SKI] : Encoded (α ⊕ β) SKI where + IsEncoding := isEncodingSum + +instance instEncodedLiftSum {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : + EncodedLift (α ⊕ β) Red where + isEncoding_left_of_red := by + intro ab x y hy h + cases ab + case inl a => + intro f g + obtain ⟨xa, ha, hred⟩ := hy f g + use xa, ha + exact Relation.ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred + case inr b => + intro f g + obtain ⟨xb, hb, hred⟩ := hy f g + use xb, hb + exact Relation.ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred + +def inlPoly : SKI.Polynomial 3 := &1 ⬝' &0 +protected def Inl : SKI := inlPoly.toSKI +lemma inl_def (a f g : SKI) : (SKI.Inl ⬝ a ⬝ f ⬝ g) ↠ f ⬝ a := + inlPoly.toSKI_correct [a, f, g] (by simp) + +lemma isEncoding_sum_inl {α β : Type*} [Encoded α SKI] [Encoded β SKI] : + SKI.Inl ⊩ (Sum.inl : α → α ⊕ β) := by + intro a xa ha f g + use xa, ha, inl_def .. + +def inrPoly : SKI.Polynomial 3 := &2 ⬝' &0 +protected def Inr : SKI := inrPoly.toSKI +lemma inr_def (a f g : SKI) : (SKI.Inr ⬝ a ⬝ f ⬝ g) ↠ g ⬝ a := + inrPoly.toSKI_correct [a, f, g] (by simp) + +lemma isEncoding_sum_inr {α β : Type*} [Encoded α SKI] [Encoded β SKI] : + SKI.Inr ⊩ (Sum.inr : β → α ⊕ β) := by + intro b xb hb f g + use xb, hb, inr_def .. + +def sumRec : SKI := RotR + +theorem isEncoding_sum_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] [EncodedLift γ Red] : + sumRec ⊩ (Sum.rec : (α → γ) → (β → γ) → α ⊕ β → γ) := by + intro f xf hf g xg hg ab xab hab + cases ab with + | inl a => + obtain ⟨xa, ha, hred⟩ := hab xf xg + exact (hf ha).left_of_mRed <| (rotR_def ..).trans hred + | inr b => + obtain ⟨xb, hb, hred⟩ := hab xf xg + exact (hg hb).left_of_mRed <| (rotR_def ..).trans hred + +end Cslib.SKI diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index b9128f09f..ea0a9a6b2 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -6,7 +6,7 @@ Authors: Thomas Waring module -public import Cslib.Languages.CombinatoryLogic.Basic +public import Cslib.Languages.CombinatoryLogic.Encoded @[expose] public section @@ -73,27 +73,21 @@ lemma church_red (n : Nat) (f f' x x' : SKI) (hf : f ↠ f') (hx : x ↠ x') : | zero => exact hx | succ n ih => exact parallel_mRed hf ih -/-- The term `a` is βη-equivalent to a standard church numeral. -/ -def IsChurch (n : Nat) (a : SKI) : Prop := - ∀ f x :SKI, (a ⬝ f ⬝ x) ↠ (Church n f x) - -/-- To show `IsChurch n a` it suffices to show the same for a reduct of `a`. -/ -theorem isChurch_trans (n : Nat) {a a' : SKI} (h : a ↠ a') : - IsChurch n a' → IsChurch n a := by - simp_rw [IsChurch] - intro ha' f x - calc - _ ↠ a' ⬝ f ⬝ x := by apply MRed.head; apply MRed.head; exact h - _ ↠ Church n f x := by apply ha' - +instance instEncodedLiftNat : EncodedLift Nat Red where + IsEncoding n a := ∀ f x : SKI, (a ⬝ f ⬝ x) ↠ (Church n f x) + isEncoding_left_of_red := by + intro n a a' ha' h f x + calc + (a ⬝ f ⬝ x) ⭢ a' ⬝ f ⬝ x := red_head _ _ x <| red_head _ _ f <| h + _ ↠ Church n f x := by apply ha' /-! ### Church numeral basics -/ /-- Church zero := λ f x. x -/ protected def Zero : SKI := K ⬝ I + @[scoped grind .] -theorem zero_correct : IsChurch 0 SKI.Zero := by - unfold IsChurch SKI.Zero Church +theorem isEncoding_zero : SKI.Zero ⊩ 0 := by intro f x calc _ ↠ I ⬝ x := by apply Relation.ReflTransGen.single; apply red_head; apply red_K @@ -101,22 +95,22 @@ theorem zero_correct : IsChurch 0 SKI.Zero := by /-- Church one := λ f x. f x -/ protected def One : SKI := I + @[scoped grind .] -theorem one_correct : IsChurch 1 SKI.One := by +theorem isEncoding_one : SKI.One ⊩ 1 := by intro f x apply head exact .single (red_I f) /-- Church succ := λ a f x. f (a f x) ~ λ a f. B f (a f) ~ λ a. S B a ~ S B -/ protected def Succ : SKI := S ⬝ B -@[scoped grind →] -theorem succ_correct (n : Nat) (a : SKI) (h : IsChurch n a) : - IsChurch (n+1) (SKI.Succ ⬝ a) := by - intro f x + +theorem isEncoding_succ : SKI.Succ ⊩ Nat.succ := by + intro n xn hn f x calc - _ ⭢ B ⬝ f ⬝ (a ⬝ f) ⬝ x := by apply red_head; apply red_S - _ ↠ f ⬝ (a ⬝ f ⬝ x) := by apply B_def - _ ↠ f ⬝ (Church n f x) := by apply MRed.tail; exact h f x + _ ⭢ B ⬝ f ⬝ (xn ⬝ f) ⬝ x := by apply red_head; apply red_S + _ ↠ f ⬝ (xn ⬝ f ⬝ x) := by apply B_def + _ ↠ f ⬝ (Church n f x) := by apply MRed.tail; exact hn f x /-- Build the canonical SKI Church numeral for `n`. -/ def toChurch : ℕ → SKI @@ -125,81 +119,94 @@ def toChurch : ℕ → SKI /-- `toChurch 0 = Zero`. -/ @[simp] lemma toChurch_zero : toChurch 0 = SKI.Zero := rfl + /-- `toChurch (n + 1) = Succ ⬝ toChurch n`. -/ @[simp] lemma toChurch_succ (n : ℕ) : toChurch (n + 1) = SKI.Succ ⬝ (toChurch n) := rfl /-- `toChurch n` correctly represents `n`. -/ @[scoped grind .] -theorem toChurch_correct (n : ℕ) : IsChurch n (toChurch n) := by +theorem toChurch_correct (n : ℕ) : (toChurch n) ⊩ n := by induction n with - | zero => exact zero_correct - | succ n ih => exact succ_correct n (toChurch n) ih + | zero => exact isEncoding_zero + | succ n ih => exact isEncoding_succ ih -/-- -To define the predecessor, iterate the function `PredAux` ⟨i, j⟩ ↦ ⟨j, j+1⟩ on ⟨0,0⟩, then take -the first component. --/ -def PredAuxPoly : SKI.Polynomial 1 := MkPair ⬝' (Snd ⬝' &0) ⬝' (SKI.Succ ⬝' (Snd ⬝' &0)) -/-- A term representing PredAux -/ -def PredAux : SKI := PredAuxPoly.toSKI -theorem predAux_def (p : SKI) : (PredAux ⬝ p) ↠ MkPair ⬝ (Snd ⬝ p) ⬝ (SKI.Succ ⬝ (Snd ⬝ p)) := - PredAuxPoly.toSKI_correct [p] (by simp) - -/-- Useful auxiliary definition expressing that `p` represents ns ∈ Nat × Nat. -/ -def IsChurchPair (ns : Nat × Nat) (x : SKI) : Prop := - IsChurch ns.1 (Fst ⬝ x) ∧ IsChurch ns.2 (Snd ⬝ x) - -theorem isChurchPair_trans (ns : Nat × Nat) (a a' : SKI) (h : a ↠ a') : - IsChurchPair ns a' → IsChurchPair ns a := by - simp_rw [IsChurchPair] - intro ⟨ha₁,ha₂⟩ - constructor - · apply isChurch_trans (a' := Fst ⬝ a') - · apply MRed.tail; exact h - · exact ha₁ - · apply isChurch_trans (a' := Snd ⬝ a') - · apply MRed.tail; exact h - · exact ha₂ - -theorem predAux_correct (p : SKI) (ns : Nat × Nat) (h : IsChurchPair ns p) : - IsChurchPair ⟨ns.2, ns.2+1⟩ (PredAux ⬝ p) := by - refine isChurchPair_trans _ _ (MkPair ⬝ (Snd ⬝ p) ⬝ (SKI.Succ ⬝ (Snd ⬝ p))) (predAux_def p) ?_ - constructor - · exact isChurch_trans ns.2 (fst_correct _ _) h.2 - · refine isChurch_trans (ns.2+1) (snd_correct _ _) ?_ - exact succ_correct ns.2 (Snd ⬝ p) h.2 - -/-- The stronger induction hypothesis necessary for the proof of `pred_correct`. -/ -theorem predAux_correct' (n : Nat) : - IsChurchPair (n.pred, n) <| Church n PredAux (MkPair ⬝ SKI.Zero ⬝ SKI.Zero) := by +variable {α : Type*} [EncodedLift α Red] + +def Iter := R + +lemma isEncoding_iter : Iter ⊩ (Nat.iterate (α := α)) := by + intro f xf hf n xn hn a xa ha + suffices IsEncoding (f^[n] a) (Church n xf xa) by + apply this.left_of_mRed + calc + _ ↠ xn ⬝ xf ⬝ xa := MRed.head _ <| R_def .. + _ ↠ Church n xf xa := hn .. + clear hn induction n with - | zero => - apply isChurchPair_trans ⟨0,0⟩ _ (MkPair ⬝ SKI.Zero ⬝ SKI.Zero) - (by rfl) - constructor <;> apply isChurch_trans 0 ?_ zero_correct - · exact fst_correct _ _ - · exact snd_correct _ _ - | succ n ih => - simp_rw [Church_succ] - apply predAux_correct (ns := ⟨n.pred, n⟩) (h := ih) - -/-- Predecessor := λ n. Fst ⬝ (n ⬝ PredAux ⬝ (MkPair ⬝ Zero ⬝ Zero)) -/ -def PredPoly : SKI.Polynomial 1 := Fst ⬝' (&0 ⬝' PredAux ⬝' (MkPair ⬝ SKI.Zero ⬝ SKI.Zero)) -/-- A term representing Pred -/ -def Pred : SKI := PredPoly.toSKI -theorem pred_def (a : SKI) : (Pred ⬝ a) ↠ Fst ⬝ (a ⬝ PredAux ⬝ (MkPair ⬝ SKI.Zero ⬝ SKI.Zero)) := - PredPoly.toSKI_correct [a] (by simp) - -theorem pred_correct (n : Nat) (a : SKI) (h : IsChurch n a) : IsChurch n.pred (Pred ⬝ a) := by - refine isChurch_trans n.pred - (pred_def a) ?_ - refine isChurch_trans _ (a' := Fst ⬝ (Church n PredAux (MkPair ⬝ SKI.Zero ⬝ SKI.Zero))) ?_ ?_ - · apply MRed.tail - exact h _ _ - · exact predAux_correct' n |>.1 - - -/-! ### Primitive recursion -/ + | zero => simpa + | succ n ih => + rw [Function.iterate_succ'] + exact hf ih + +def Nat.recPairStep (f : Nat → α → α) : α × Nat → α × Nat + | ⟨y, m⟩ => ⟨f m y, m + 1⟩ + +lemma Nat.recPairStep_correct {α' : Type*} (a : α') (f : Nat → α' → α') (n : Nat) : + (Nat.recPairStep f)^[n] ⟨a, 0⟩ = ⟨Nat.rec a f n, n⟩ := by + induction n with + | zero => simp + | succ n ih => + rw [Function.iterate_succ', Function.comp_apply, ih, recPairStep] + +/-- We encode primitive recursion on `Nat` by the usual Kleene dentist trick. -/ +def natRecAuxPoly : SKI.Polynomial 2 := + SKI.MkPair ⬝' (&0 ⬝' (Snd ⬝' &1) ⬝' (Fst ⬝' &1)) ⬝' (SKI.Succ ⬝' (Snd ⬝' &1)) +def natRecAux := natRecAuxPoly.toSKI +lemma natRecAux_def (f p : SKI) : + (natRecAux ⬝ f ⬝ p) ↠ SKI.MkPair ⬝ (f ⬝ (Snd ⬝ p) ⬝ (Fst ⬝ p)) ⬝ (SKI.Succ ⬝ (Snd ⬝ p)) := + natRecAuxPoly.toSKI_correct [f, p] (by simp) + +lemma natRecAux_correct {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) : + (natRecAux ⬝ xf) ⊩ (Nat.recPairStep f) := by + intro p xp hp + suffices IsEncoding (Nat.recPairStep f p) + (SKI.MkPair ⬝ (xf ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (SKI.Succ ⬝ (Snd ⬝ xp))) by + exact this.left_of_mRed <| natRecAux_def .. + apply isEncoding_mkPair + · exact hf hp.2 hp.1 + · exact SKI.isEncoding_succ hp.2 + +lemma isEncoded_recPairStep_iter {a : α} {xa : SKI} (ha : xa ⊩ a) + {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) {n : Nat} {xn : SKI} (hn : xn ⊩ n) : + (R ⬝ (natRecAux ⬝ xf) ⬝ xn ⬝ (MkPair ⬝ xa ⬝ SKI.Zero)) ⊩ (⟨Nat.rec a f n, n⟩ : α × Nat) := by + rw [←Nat.recPairStep_correct] + refine isEncoding_iter (natRecAux_correct hf) hn ?_ + apply isEncoding_mkPair + · exact ha + · exact isEncoding_zero + +def natRecPoly : SKI.Polynomial 3 := + Fst ⬝' (R ⬝' (natRecAux ⬝' &1) ⬝' &2 ⬝' (MkPair ⬝' &0 ⬝' SKI.Zero)) +def natRec := natRecPoly.toSKI +lemma natRec_def (xa xf xn : SKI) : + (natRec ⬝ xa ⬝ xf ⬝ xn) ↠ Fst ⬝ (R ⬝ (natRecAux ⬝ xf) ⬝ xn ⬝ (MkPair ⬝ xa ⬝ SKI.Zero)) := + natRecPoly.toSKI_correct [xa, xf, xn] (by simp) + +/-- Primitive recursion on `Nat`. -/ +theorem isEncoding_nat_rec : + natRec ⊩ (Nat.rec : α → (Nat → α → α) → Nat → α) := by + intro a xa ha f xf hf n xn hn + exact IsEncoding.left_of_mRed (isEncoded_recPairStep_iter ha hf hn).1 (natRec_def xa xf xn) + +def Pred : SKI := natRec ⬝ SKI.Zero ⬝ K + +theorem isEncoding_pred : Pred ⊩ Nat.pred := by + intro n xn hn + have : n.pred = n.rec 0 (fun a _ => a) := by induction n <;> simp + rw [this] + refine isEncoding_nat_rec isEncoding_zero ?_ hn + intro _ _ h _ _ _ + exact h.left_of_red <| red_K .. /-- IsZero := λ n. n (K FF) TT -/ def IsZeroPoly : SKI.Polynomial 1 := &0 ⬝' (K ⬝ FF) ⬝' TT @@ -207,65 +214,22 @@ def IsZeroPoly : SKI.Polynomial 1 := &0 ⬝' (K ⬝ FF) ⬝' TT def IsZero : SKI := IsZeroPoly.toSKI theorem isZero_def (a : SKI) : (IsZero ⬝ a) ↠ a ⬝ (K ⬝ FF) ⬝ TT := IsZeroPoly.toSKI_correct [a] (by simp) -theorem isZero_correct (n : Nat) (a : SKI) (h : IsChurch n a) : - IsBool (n = 0) (IsZero ⬝ a) := by - apply isBool_trans (a' := a ⬝ (K ⬝ FF) ⬝ TT) (h := isZero_def a) - by_cases n=0 + +theorem isEncoding_isZero : IsZero ⊩ (· == 0) := by + intro n xn hn + refine IsEncoding.left_of_mRed ?_ (isZero_def _) + by_cases n = 0 case pos h0 => - simp_rw [h0] - rw [h0] at h - apply isBool_trans (ha' := TT_correct) - exact h _ _ + simp_rw [h0] at hn ⊢ + exact TT_correct.left_of_mRed <| hn .. case neg h0 => - simp_rw [h0] - let ⟨k,hk⟩ := Nat.exists_eq_succ_of_ne_zero h0 - rw [hk] at h - apply isBool_trans (ha' := FF_correct) + simp_rw [beq_false_of_ne h0] + let ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero h0 + rw [hk] at hn + apply FF_correct.left_of_mRed calc - _ ↠ (K ⬝ FF) ⬝ Church k (K ⬝ FF) TT := h _ _ - _ ⭢ FF := red_K _ _ - - -/-- -To define `Rec x g n := if n==0 then x else (Rec x g (Pred n))`, we obtain a fixed point of -R ↦ λ x g n. Cond ⬝ (IsZero ⬝ n) ⬝ x ⬝ (g ⬝ a ⬝ (R ⬝ x ⬝ g ⬝ (Pred ⬝ n))) --/ -def RecAuxPoly : SKI.Polynomial 4 := - SKI.Cond ⬝' &1 ⬝' (&2 ⬝' &3 ⬝' (&0 ⬝' &1 ⬝' &2 ⬝' (Pred ⬝' &3))) ⬝' (IsZero ⬝' &3) -/-- A term representing RecAux -/ -def RecAux : SKI := RecAuxPoly.toSKI -theorem recAux_def (R₀ x g a : SKI) : - (RecAux ⬝ R₀ ⬝ x ⬝ g ⬝ a) ↠ - SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (R₀ ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := - RecAuxPoly.toSKI_correct [R₀, x, g, a] (by simp) - -/-- -We define Rec so that -`Rec ⬝ x ⬝ g ⬝ a ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a)` --/ -def Rec : SKI := fixedPoint RecAux -theorem rec_def (x g a : SKI) : - (Rec ⬝ x ⬝ g ⬝ a) ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := calc - _ ↠ RecAux ⬝ Rec ⬝ x ⬝ g ⬝ a := by - apply MRed.head; apply MRed.head; apply MRed.head - apply fixedPoint_correct - _ ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := recAux_def Rec x g a - -theorem rec_zero (x g a : SKI) (ha : IsChurch 0 a) : (Rec ⬝ x ⬝ g ⬝ a) ↠ x := by - calc - _ ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := rec_def _ _ _ - _ ↠ if (Nat.beq 0 0) then x else (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) := by - apply cond_correct - exact isZero_correct 0 a ha - -theorem rec_succ (n : Nat) (x g a : SKI) (ha : IsChurch (n + 1) a) : - (Rec ⬝ x ⬝ g ⬝ a) ↠ g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a)) := by - calc - _ ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := rec_def _ _ _ - _ ↠ if (Nat.beq (n+1) 0) then x else (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) := by - apply cond_correct - exact isZero_correct (n+1) a ha - + _ ↠ (K ⬝ FF) ⬝ Church k (K ⬝ FF) TT := hn .. + _ ⭢ FF := red_K .. /-! ### Root-finding (μ-recursion) -/ @@ -282,55 +246,47 @@ lemma rfindAboveAux_def (R₀ f a : SKI) : (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := RFindAboveAuxPoly.toSKI_correct [R₀, a, f] (by trivial) -theorem rfindAboveAux_base (R₀ f a : SKI) (hfa : IsChurch 0 (f ⬝ a)) : +theorem rfindAboveAux_base (R₀ f a : SKI) (hfa : (f ⬝ a) ⊩ 0) : (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ a := calc _ ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := rfindAboveAux_def _ _ _ _ ↠ if (Nat.beq 0 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by - apply cond_correct - apply isZero_correct _ _ hfa -theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : IsChurch (m + 1) (f ⬝ a)) : + exact cond_def <| isEncoding_isZero hfa + +theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : (f ⬝ a) ⊩ m + 1) : (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f := calc _ ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := rfindAboveAux_def _ _ _ - _ ↠ if (Nat.beq (m+1) 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by - apply cond_correct - apply isZero_correct _ _ hfa + _ ↠ if (Nat.beq (m + 1) 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by + exact cond_def <| isEncoding_isZero hfa /-- Find the minimal root of `fNat` above a number n -/ def RFindAbove : SKI := RFindAboveAux.fixedPoint -theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI) - (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y → IsChurch (fNat i) (f ⬝ y)) - (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) : - IsChurch (m+n) (RFindAbove ⬝ x ⬝ f) := by + +theorem RFindAbove_correct (f : Nat → Nat) (xf x : SKI) (hf : xf ⊩ f) (n m : Nat) (hx : x ⊩ m) + (hroot : f (m + n) = 0) (hpos : ∀ i < n, f (m + i) ≠ 0) : + (RFindAbove ⬝ x ⬝ xf) ⊩ (m + n) := by induction n generalizing m x - all_goals apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ f) - case zero.a => - apply isChurch_trans (a' := x) <;> - grind [rfindAboveAux_base] - case succ.a n ih => - apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f) - · let y := (fNat m).pred - have : IsChurch (y + 1) (f ⬝ x) := by - subst y - exact Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf m x hx - apply rfindAboveAux_step - assumption - · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx) + all_goals apply IsEncoding.left_of_mRed (y := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ xf) + case zero.ha => + apply hx.left_of_mRed + apply rfindAboveAux_base + exact hroot ▸ hf hx + case succ.ha n ih => + apply IsEncoding.left_of_mRed (y := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ xf) + · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (isEncoding_succ hx) grind + · have : (xf ⬝ x) ⊩ ((f m).pred + 1) := Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf hx + exact rfindAboveAux_step _ _ _ this -- close the `h` goals of the above `apply isChurch_trans` all_goals {apply MRed.head; apply MRed.head; exact fixedPoint_correct _} - /-- Ordinary root finding is root finding above zero -/ def RFind := RFindAbove ⬝ SKI.Zero -theorem RFind_correct (fNat : Nat → Nat) (f : SKI) - (hf : ∀ (i : Nat) (y : SKI), IsChurch i y → IsChurch (fNat i) (f ⬝ y)) - (n : Nat) (hroot : fNat n = 0) (hpos : ∀ i < n, fNat i ≠ 0) : IsChurch n (RFind ⬝ f) := by - have :_ := RFindAbove_correct (n := n) (fNat := fNat) (hf := hf) (hx := zero_correct) +theorem RFind_correct (f : Nat → Nat) (xf : SKI) (hf : xf ⊩ f) + (n : Nat) (hroot : f n = 0) (hpos : ∀ i < n, f i ≠ 0) : (RFind ⬝ xf) ⊩ n := by + have :_ := RFindAbove_correct (n := n) (f := f) (hf := hf) (hx := isEncoding_zero) simp_rw [Nat.zero_add] at this exact this hroot hpos - - /-! ### Further numeric operations -/ /-- Addition: λ n m. n Succ m -/ @@ -340,18 +296,17 @@ protected def Add : SKI := AddPoly.toSKI theorem add_def (a b : SKI) : (SKI.Add ⬝ a ⬝ b) ↠ a ⬝ SKI.Succ ⬝ b := AddPoly.toSKI_correct [a, b] (by simp) -theorem add_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : - IsChurch (n + m) (SKI.Add ⬝ a ⬝ b) := by - refine isChurch_trans (n + m) (a' := Church n SKI.Succ b) ?_ ?_ - · calc - _ ↠ a ⬝ SKI.Succ ⬝ b := add_def a b - _ ↠ Church n SKI.Succ b := ha SKI.Succ b - · clear ha +theorem isEncoding_add : SKI.Add ⊩ Nat.add:= by + intro n xn hn m xm hm + refine IsEncoding.left_of_mRed (y := Church n SKI.Succ xm) ?_ ?_ + · clear hn induction n with - | zero => simp_rw [Nat.zero_add, Church]; exact hb + | zero => simpa | succ n ih => - simp_rw [Nat.add_right_comm, Church] - exact succ_correct _ _ ih + simpa [Nat.add_right_comm] using isEncoding_succ ih + · calc + _ ↠ xn ⬝ SKI.Succ ⬝ xm := add_def .. + _ ↠ Church n SKI.Succ xm := hn .. /-- Multiplication: λ n m. n (Add m) Zero -/ def MulPoly : SKI.Polynomial 2 := &0 ⬝' (SKI.Add ⬝' &1) ⬝' SKI.Zero @@ -360,16 +315,15 @@ protected def Mul : SKI := MulPoly.toSKI theorem mul_def (a b : SKI) : (SKI.Mul ⬝ a ⬝ b) ↠ a ⬝ (SKI.Add ⬝ b) ⬝ SKI.Zero := MulPoly.toSKI_correct [a, b] (by simp) -theorem mul_correct {n m : Nat} {a b : SKI} (ha : IsChurch n a) (hb : IsChurch m b) : - IsChurch (n * m) (SKI.Mul ⬝ a ⬝ b) := by - refine isChurch_trans (n * m) (a' := Church n (SKI.Add ⬝ b) SKI.Zero) ?_ ?_ - · exact Trans.trans (mul_def a b) (ha (SKI.Add ⬝ b) SKI.Zero) - · clear ha +theorem mul_correct : SKI.Mul ⊩ Nat.mul := by + intro n xn hn m xm hm + refine IsEncoding.left_of_mRed (y := Church n (SKI.Add ⬝ xm) SKI.Zero) ?_ ?_ + · clear hn induction n with - | zero => simp_rw [Nat.zero_mul, Church]; exact zero_correct + | zero => simpa using isEncoding_zero | succ n ih => - simp_rw [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church] - exact add_correct m (n * m) b (Church n (SKI.Add ⬝ b) SKI.Zero) hb ih + simpa [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church] using isEncoding_add hm ih + · exact Trans.trans (mul_def xn xm) (hn (SKI.Add ⬝ xm) SKI.Zero) /-- Subtraction: λ n m. n Pred m -/ def SubPoly : SKI.Polynomial 2 := &1 ⬝' Pred ⬝' &0 @@ -378,18 +332,17 @@ protected def Sub : SKI := SubPoly.toSKI theorem sub_def (a b : SKI) : (SKI.Sub ⬝ a ⬝ b) ↠ b ⬝ Pred ⬝ a := SubPoly.toSKI_correct [a, b] (by simp) -theorem sub_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : - IsChurch (n - m) (SKI.Sub ⬝ a ⬝ b) := by - refine isChurch_trans (n - m) (a' := Church m Pred a) ?_ ?_ - · calc - _ ↠ b ⬝ Pred ⬝ a := sub_def a b - _ ↠ Church m Pred a := hb Pred a - · clear hb +theorem sub_correct : SKI.Sub ⊩ Nat.sub := by + intro n xn hn m xm hm + refine IsEncoding.left_of_mRed (y := Church m Pred xn) ?_ ?_ + · clear hm induction m with - | zero => simp_rw [Nat.sub_zero, Church]; exact ha + | zero => simpa using hn | succ m ih => - simp_rw [←Nat.sub_sub, Church] - exact pred_correct _ _ ih + simpa using isEncoding_pred ih + · calc + _ ↠ xm ⬝ Pred ⬝ xn := sub_def .. + _ ↠ Church m Pred xn := hm Pred xn /-- Comparison: (. ≤ .) := λ n m. IsZero ⬝ (Sub ⬝ n ⬝ m) -/ def LEPoly : SKI.Polynomial 2 := IsZero ⬝' (SKI.Sub ⬝' &0 ⬝' &1) @@ -398,11 +351,11 @@ protected def LE : SKI := LEPoly.toSKI theorem le_def (a b : SKI) : (SKI.LE ⬝ a ⬝ b) ↠ IsZero ⬝ (SKI.Sub ⬝ a ⬝ b) := LEPoly.toSKI_correct [a, b] (by simp) -theorem le_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) : - IsBool (n ≤ m) (SKI.LE ⬝ a ⬝ b) := by - simp only [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le] - apply isBool_trans (a' := IsZero ⬝ (SKI.Sub ⬝ a ⬝ b)) (h := le_def _ _) - apply isZero_correct +theorem le_correct : SKI.LE ⊩ (· ≤ · : Nat → Nat → Bool) := by + intro n xn hn m xm hm + simp_rw [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le] + apply IsEncoding.left_of_mRed (y := IsZero ⬝ (SKI.Sub ⬝ xn ⬝ xm)) (h := le_def _ _) + apply isEncoding_isZero apply sub_correct <;> assumption end SKI From 5ab0cc9b40413aa31a51593358976bcd4838f7b4 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 6 Mar 2026 21:15:23 +0100 Subject: [PATCH 08/12] lists --- Cslib/Languages/CombinatoryLogic/List.lean | 287 +++++++++------------ 1 file changed, 126 insertions(+), 161 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean index c71721da9..baf5fd056 100644 --- a/Cslib/Languages/CombinatoryLogic/List.lean +++ b/Cslib/Languages/CombinatoryLogic/List.lean @@ -23,41 +23,34 @@ namespace SKI open Red MRed +variable {α β : Type*} [Encoded α SKI] [Encoded β SKI] + /-! ### Church List Representation -/ -/-- A term correctly Church-encodes a list of natural numbers. -/ -def IsChurchList : List ℕ → SKI → Prop +/-- A term correctly Church-encodes a list. -/ +def IsEncodingList : List α → SKI → Prop | [], cns => ∀ c n : SKI, (cns ⬝ c ⬝ n) ↠ n - | x :: xs, cns => ∀ c n : SKI, - ∃ cx cxs : SKI, IsChurch x cx ∧ IsChurchList xs cxs ∧ + | a :: as, cns => ∀ c n : SKI, + ∃ cx cxs : SKI, IsEncoding a cx ∧ IsEncodingList as cxs ∧ (cns ⬝ c ⬝ n) ↠ c ⬝ cx ⬝ (cxs ⬝ c ⬝ n) -/-- `IsChurchList` is preserved under multi-step reduction of the term. -/ -theorem isChurchList_trans {ns : List ℕ} {cns cns' : SKI} (h : cns ↠ cns') - (hcns' : IsChurchList ns cns') : IsChurchList ns cns := by - match ns with - | [] => - intro c n - exact Trans.trans (parallel_mRed (MRed.head c h) .refl) (hcns' c n) - | x :: xs => - intro c n - obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns' c n - exact ⟨cx, cxs, hcx, hcxs, Trans.trans (parallel_mRed (MRed.head c h) .refl) hred⟩ - -/-- Both components of a pair are Church lists. -/ -structure IsChurchListPair (prev curr : List ℕ) (p : SKI) : Prop where - fst : IsChurchList prev (Fst ⬝ p) - snd : IsChurchList curr (Snd ⬝ p) - -/-- IsChurchListPair is preserved under reduction. -/ -@[scoped grind →] -theorem isChurchListPair_trans {prev curr : List ℕ} {p p' : SKI} (hp : p ↠ p') - (hp' : IsChurchListPair prev curr p') : IsChurchListPair prev curr p := by - constructor - · apply isChurchList_trans (MRed.tail Fst hp) - exact hp'.1 - · apply isChurchList_trans (MRed.tail Snd hp) - exact hp'.2 +instance instEncodedList : Encoded (List α) SKI where + IsEncoding := IsEncodingList + +instance instEncodedLiftList [EncodedLift α Red] : EncodedLift (List α) Red where + isEncoding_left_of_red := by + intro as cns cns' has h + induction as generalizing cns cns' with + | nil => + intro c n + refine Relation.ReflTransGen.head ?_ (has c n) + exact red_head _ _ _ <| red_head _ _ _ h + | cons a as ih => + intro c n + obtain ⟨cx', cxs', hcx, hcxs, hred⟩ := has c n + use cx', cxs', hcx, hcxs + refine Relation.ReflTransGen.head ?_ hred + exact red_head _ _ _ <| red_head _ _ _ h namespace List @@ -74,7 +67,7 @@ theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n := NilPoly.toSKI_correct [c, n] (by simp) /-- The empty list term correctly represents `[]`. -/ -theorem nil_correct : IsChurchList [] Nil := nil_def +theorem isEncoding_nil : Nil ⊩ ([] : List α) := nil_def /-! ### Cons: Consing an element onto a list -/ @@ -90,37 +83,86 @@ theorem cons_def (x xs c n : SKI) : ConsPoly.toSKI_correct [x, xs, c, n] (by simp) /-- Cons preserves Church list representation. -/ -theorem cons_correct {x : ℕ} {xs : List ℕ} {cx cxs : SKI} - (hcx : IsChurch x cx) (hcxs : IsChurchList xs cxs) : - IsChurchList (x :: xs) (Cons ⬝ cx ⬝ cxs) := by - intro c n - use cx, cxs, hcx, hcxs +theorem isEncoding_cons : Cons ⊩ (List.cons : α → List α → List α) := by + intro c cx hx xs cxs hxs c n + use cx, cxs, hx, hxs exact cons_def cx cxs c n /-- Singleton list correctness. -/ -theorem singleton_correct {x : ℕ} {cx : SKI} (hcx : IsChurch x cx) : - IsChurchList [x] (Cons ⬝ cx ⬝ Nil) := - cons_correct hcx nil_correct - -/-- The canonical SKI term for a Church-encoded list. -/ -def toChurch : List ℕ → SKI - | [] => Nil - | x :: xs => Cons ⬝ (SKI.toChurch x) ⬝ (toChurch xs) - -/-- `toChurch [] = Nil`. -/ -@[simp] -lemma toChurch_nil : toChurch [] = Nil := rfl - -/-- `toChurch (x :: xs) = Cons ⬝ SKI.toChurch x ⬝ toChurch xs`. -/ -@[simp] -lemma toChurch_cons (x : ℕ) (xs : List ℕ) : - toChurch (x :: xs) = Cons ⬝ (SKI.toChurch x) ⬝ (toChurch xs) := rfl - -/-- `toChurch ns` correctly represents `ns`. -/ -theorem toChurch_correct (ns : List ℕ) : IsChurchList ns (toChurch ns) := by - induction ns with - | nil => exact nil_correct - | cons x xs ih => exact cons_correct (SKI.toChurch_correct x) ih +theorem isEncoding_singleton {x : α} {cx : SKI} (hcx : cx ⊩ x) : + (Cons ⬝ cx ⬝ Nil) ⊩ [x] := + isEncoding_cons hcx isEncoding_nil + +def FoldR := RotR + +lemma isEncoding_list_foldr {α β : Type*} [Encoded α SKI] [EncodedLift β Red] : + FoldR ⊩ (List.foldr : (α → β → β) → β → List α → β) := by + intro f xf hf b xb hb l xl hl + suffices (xl ⬝ xf ⬝ xb) ⊩ (l.foldr f b) by apply this.left_of_mRed <| rotR_def .. + induction l generalizing xl with + | nil => exact hb.left_of_mRed <| hl .. + | cons a l ih => + obtain ⟨xa, xl', ha, hl', hred⟩ := hl xf xb + have : IsEncoding (f a (List.foldr f b l)) (xf ⬝ xa ⬝ (xl' ⬝ xf ⬝ xb)) := + hf ha (ih hl') + exact this.left_of_mRed hred + +def recPairStep (f : α → List α → β → β) : α → (β × List α) → (β × List α) + | a, ⟨y, as⟩ => ⟨f a as y, a :: as⟩ + +lemma recPairStep_foldr {α' β' : Type*} (b : β') (f : α' → List α' → β' → β') (as : List α') : + List.foldr (β := β' × List α') (List.recPairStep f) ⟨b, []⟩ as = ⟨List.rec b f as, as⟩ := by + induction as <;> simp_all [recPairStep] + +def listRecAuxPoly : SKI.Polynomial 3 := + SKI.MkPair ⬝' (&0 ⬝' &1 ⬝' (Snd ⬝' &2) ⬝' (Fst ⬝' &2)) ⬝' (Cons ⬝' &1 ⬝' (Snd ⬝' &2)) +def listRecAux : SKI := listRecAuxPoly.toSKI +lemma listRecAux_def (xf xa xp : SKI) : + (listRecAux ⬝ xf ⬝ xa ⬝ xp) ↠ + SKI.MkPair ⬝ (xf ⬝ xa ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (Cons ⬝ xa ⬝ (Snd ⬝ xp)) := + listRecAuxPoly.toSKI_correct [xf, xa, xp] (by simp) + +lemma listRecAux_correct {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] + {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) : + (listRecAux ⬝ xf) ⊩ (List.recPairStep f) := by + intro a xa ha p xp hp + refine IsEncoding.left_of_mRed (α := β × List α) ?_ (listRecAux_def xf xa xp) + apply isEncoding_mkPair + · exact hf ha hp.2 hp.1 + · exact isEncoding_cons ha hp.2 + +lemma isEncoding_recPairStep_foldr {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] + {b : β} {xb : SKI} (hb : xb ⊩ b) + {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) {as : List α} {xas : SKI} (has : xas ⊩ as) : + (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) ⊩ + (⟨List.rec b f as, as⟩ : β × List α) := by + rw [←List.recPairStep_foldr] + refine isEncoding_list_foldr (listRecAux_correct hf) ?_ has + exact isEncoding_mkPair hb isEncoding_nil + +def listRecPoly : SKI.Polynomial 3 := + Fst ⬝' (SKI.RotR ⬝' (listRecAux ⬝' &1) ⬝' (MkPair ⬝' &0 ⬝' Nil) ⬝' &2) +def listRec := listRecPoly.toSKI +lemma listRec_def (xb xf xas : SKI) : + (listRec ⬝ xb ⬝ xf ⬝ xas) ↠ Fst ⬝ (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) := + listRecPoly.toSKI_correct [xb, xf, xas] (by simp) + +theorem isEncoding_list_rec {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : + listRec ⊩ (List.rec : β → (α → List α → β → β) → List α → β) := by + intro b xb hb f xf hf as xas has + have := isEncoding_recPairStep_foldr hb hf has + exact this.1.left_of_mRed <| listRec_def .. + +def Tail := (listRec ⬝ Nil ⬝ (&1 : SKI.Polynomial 3).toSKI) + +lemma isEncoding_tail {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : + Tail ⊩ (List.tail : List α → List α) := by + intro as xas has + have : (as.tail = as.rec [] (fun _ t _ => t)) := by cases as <;> rfl + rw [this] + refine isEncoding_list_rec isEncoding_nil ?_ has + intro _ xs _ t xt ht _ xu _ + apply ht.left_of_mRed <| (&1 : SKI.Polynomial 3).toSKI_correct [xs, xt, xu] (by simp) /-! ### Head: Extract the head of a list -/ @@ -135,20 +177,21 @@ theorem headD_def (d xs : SKI) : (HeadD ⬝ d ⬝ xs) ↠ xs ⬝ K ⬝ d := HeadDPoly.toSKI_correct [d, xs] (by simp) /-- General head-with-default correctness. -/ -theorem headD_correct {d : ℕ} {cd : SKI} (hcd : IsChurch d cd) - {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) : - IsChurch (ns.headD d) (HeadD ⬝ cd ⬝ cns) := by - match ns with +theorem isEncoding_headD {α : Type*} [EncodedLift α Red] : + HeadD ⊩ (fun a (as : List α) => as.headD a) := by + intro a xa ha as xas has + match as with | [] => simp only [List.headD_nil] - apply isChurch_trans d (headD_def cd cns) - apply isChurch_trans d (hcns K cd) - exact hcd + refine IsEncoding.left_of_mRed ?_ (headD_def xa xas) + apply ha.left_of_mRed + exact has K xa | x :: xs => simp only [List.headD_cons] - apply isChurch_trans x (headD_def cd cns) - obtain ⟨cx, cxs, hcx, _, hred⟩ := hcns K cd - exact isChurch_trans x hred (isChurch_trans x (MRed.K cx _) hcx) + refine IsEncoding.left_of_mRed ?_ (headD_def xa xas) + obtain ⟨cx, cxs, hcx, _, hred⟩ := has K xa + apply hcx.left_of_mRed + exact hred.trans <| MRed.K .. /-- The SKI term for list head (default 0). -/ def Head : SKI := HeadD ⬝ SKI.Zero @@ -158,88 +201,9 @@ theorem head_def (xs : SKI) : (Head ⬝ xs) ↠ xs ⬝ K ⬝ SKI.Zero := headD_def SKI.Zero xs /-- Head correctness (default 0). -/ -theorem head_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : - IsChurch (ns.headD 0) (Head ⬝ cns) := - headD_correct zero_correct hcns - -/-! ### Tail: Extract the tail of a list -/ - -/-- Step function for tail: (prev, curr) → (curr, cons h curr) -/ -def TailStepPoly : SKI.Polynomial 2 := - MkPair ⬝' (Snd ⬝' &1) ⬝' (Cons ⬝' &0 ⬝' (Snd ⬝' &1)) - -/-- The step function for computing list tail. -/ -def TailStep : SKI := TailStepPoly.toSKI - -/-- Reduction of the tail step function. -/ -theorem tailStep_def (h p : SKI) : - (TailStep ⬝ h ⬝ p) ↠ MkPair ⬝ (Snd ⬝ p) ⬝ (Cons ⬝ h ⬝ (Snd ⬝ p)) := - TailStepPoly.toSKI_correct [h, p] (by simp) - -/-- tail xs = Fst (xs TailStep (MkPair Nil Nil)) -/ -def TailPoly : SKI.Polynomial 1 := - Fst ⬝' (&0 ⬝' TailStep ⬝' (MkPair ⬝ Nil ⬝ Nil)) - -/-- The tail of a Church-encoded list. -/ -def Tail : SKI := TailPoly.toSKI - -/-- Reduction: `Tail ⬝ xs ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil))`. -/ -theorem tail_def (xs : SKI) : - (Tail ⬝ xs) ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) := - TailPoly.toSKI_correct [xs] (by simp) - -/-- The initial pair (nil, nil) satisfies the invariant. -/ -@[simp] -theorem tail_init : IsChurchListPair [] [] (MkPair ⬝ Nil ⬝ Nil) := by - constructor - · apply isChurchList_trans (fst_correct _ _); exact nil_correct - · apply isChurchList_trans (snd_correct _ _); exact nil_correct - -/-- The step function preserves the tail-computing invariant. -/ -theorem tailStep_correct {x : ℕ} {xs : List ℕ} {cx p : SKI} - (hcx : IsChurch x cx) (hp : IsChurchListPair xs.tail xs p) : - IsChurchListPair xs (x :: xs) (TailStep ⬝ cx ⬝ p) := by - apply isChurchListPair_trans (tailStep_def cx p) - exact ⟨isChurchList_trans (fst_correct _ _) hp.2, - isChurchList_trans (snd_correct _ _) (cons_correct hcx hp.2)⟩ - -theorem tailFold_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : - ∃ p, (cns ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) ↠ p ∧ - IsChurchListPair ns.tail ns p := by - induction ns generalizing cns with - | nil => - -- For empty list, the fold returns the initial pair - use MkPair ⬝ Nil ⬝ Nil - constructor - · exact hcns TailStep (MkPair ⬝ Nil ⬝ Nil) - · exact tail_init - | cons x xs ih => - -- For x :: xs, first fold xs, then apply step - -- cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init) - -- Get the Church representations for x and xs - obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns TailStep (MkPair ⬝ Nil ⬝ Nil) - -- By IH, folding xs gives a pair representing (xs.tail, xs) - obtain ⟨p_xs, hp_xs_red, hp_xs_pair⟩ := ih cxs hcxs - -- After step, we get a pair representing (xs, x :: xs) - have hstep := tailStep_correct hcx hp_xs_pair - -- The full fold: cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init) - -- ↠ TailStep ⬝ cx ⬝ p_xs - use TailStep ⬝ cx ⬝ p_xs - constructor - · exact Trans.trans hred (MRed.tail _ hp_xs_red) - · exact hstep - -/-- Tail correctness. -/ -theorem tail_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : - IsChurchList ns.tail (Tail ⬝ cns) := by - -- Tail ⬝ cns ↠ Fst ⬝ (cns ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) - apply isChurchList_trans (tail_def cns) - -- Get the fold result - obtain ⟨p, hp_red, hp_pair⟩ := tailFold_correct ns cns hcns - -- Fst ⬝ (cns ⬝ TailStep ⬝ init) ↠ Fst ⬝ p - apply isChurchList_trans (MRed.tail Fst hp_red) - -- Fst ⬝ p represents ns.tail (from hp_pair) - exact hp_pair.1 +theorem isEncoding_head : Head ⊩ (fun (xs : List Nat) => xs.headD 0) := by + intro ns xns hns + exact isEncoding_headD isEncoding_zero hns /-! ### Prepending zero to a list (for Code.zero') -/ @@ -254,10 +218,10 @@ theorem prependZero_def (xs : SKI) : (PrependZero ⬝ xs) ↠ Cons ⬝ SKI.Zero PrependZeroPoly.toSKI_correct [xs] (by simp) /-- Prepending zero preserves Church list representation. -/ -theorem prependZero_correct {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) : - IsChurchList (0 :: ns) (PrependZero ⬝ cns) := by - apply isChurchList_trans (prependZero_def cns) - exact cons_correct zero_correct hcns +theorem isEncoding_prependZero : PrependZero ⊩ (fun ns => 0 :: ns) := by + intro ns cns hns + refine IsEncoding.left_of_mRed ?_ (prependZero_def cns) + exact isEncoding_cons isEncoding_zero hns /-! ### Successor on list head (for Code.succ) -/ @@ -265,12 +229,13 @@ theorem prependZero_correct {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns def SuccHead : SKI := B ⬝ (C ⬝ Cons ⬝ Nil) ⬝ (B ⬝ SKI.Succ ⬝ Head) /-- `SuccHead` correctly computes a singleton containing `succ(head ns)`. -/ -theorem succHead_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) : - IsChurchList [ns.headD 0 + 1] (SuccHead ⬝ cns) := by - have hhead := head_correct ns cns hcns - have hsucc := succ_correct (ns.headD 0) (Head ⬝ cns) hhead - apply isChurchList_trans (.trans (B_tail_mred _ _ _ _ (B_def .Succ Head cns)) (C_def Cons Nil _)) - exact cons_correct hsucc nil_correct +theorem isEncoding_prependSucc : SuccHead ⊩ (fun (ns : List Nat) => [ns.headD 0 + 1]) := by + intro ns cns hcns + have hhead := isEncoding_head hcns + have hsucc := isEncoding_succ hhead + refine IsEncoding.left_of_mRed ?_ + (.trans (B_tail_mred _ _ _ _ (B_def .Succ Head cns)) (C_def Cons Nil _)) + exact isEncoding_cons hsucc isEncoding_nil end List From 707e9570633192811b7afce6c5c4d51cc8dca908 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 6 Mar 2026 21:44:00 +0100 Subject: [PATCH 09/12] partial values, tidy names --- Cslib/Languages/CombinatoryLogic/Encoded.lean | 31 +++++++++++++++++++ Cslib/Languages/CombinatoryLogic/List.lean | 10 +++--- .../Languages/CombinatoryLogic/Recursion.lean | 23 ++++++++------ 3 files changed, 50 insertions(+), 14 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Encoded.lean b/Cslib/Languages/CombinatoryLogic/Encoded.lean index e27d310fa..6bacc449b 100644 --- a/Cslib/Languages/CombinatoryLogic/Encoded.lean +++ b/Cslib/Languages/CombinatoryLogic/Encoded.lean @@ -8,6 +8,7 @@ module public import Cslib.Languages.CombinatoryLogic.Basic public import Cslib.Foundations.Semantics.Encoded +public import Mathlib.Data.Part @[expose] public section @@ -229,4 +230,34 @@ theorem isEncoding_sum_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] obtain ⟨xb, hb, hred⟩ := hab xf xg exact (hg hb).left_of_mRed <| (rotR_def ..).trans hred +/-! +### Partial values + +A term `x` encodes a partial value `o` if `o = Part.none`, or `o = Part.some a` and `x ⊩ a`. +-/ + +instance instEncodedPart {α : Type*} [Encoded α SKI] : Encoded (Part α) SKI where + IsEncoding o x := (h : o.Dom) → x ⊩ (o.get h) + +lemma isEncoding_of_mem {α : Type*} [Encoded α SKI] {o : Part α} {x : SKI} (h : x ⊩ o) + {a : α} (ha : a ∈ o) : x ⊩ a := by + obtain ⟨hao, ha⟩ := ha + exact ha ▸ h hao + +lemma isEncoding_some_iff {α : Type*} [Encoded α SKI] {a : α} {x : SKI} : + (x ⊩ Part.some a) ↔ x ⊩ a := by + refine ⟨?_, ?_⟩ + · intro h; exact h (Part.some_dom a) + · intro h; exact fun _ => h + +instance instEncodedLiftPart {α : Type*} [EncodedLift α Red] : EncodedLift (Part α) Red where + isEncoding_left_of_red := by + intro o x y ho h hdom + exact (ho hdom).left_of_red h + +instance instEncodedDescPart {α : Type*} [EncodedDesc α Red] : EncodedDesc (Part α) Red where + isEncoding_right_of_red := by + intro o x y ho h hdom + exact (ho hdom).right_of_red h + end Cslib.SKI diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean index baf5fd056..ee01e3b03 100644 --- a/Cslib/Languages/CombinatoryLogic/List.lean +++ b/Cslib/Languages/CombinatoryLogic/List.lean @@ -13,8 +13,8 @@ public import Cslib.Languages.CombinatoryLogic.Recursion /-! # Church-Encoded Lists in SKI Combinatory Logic -Church-encoded lists for proving SKI ≃ TM equivalence. A list is encoded as -`λ c n. c a₀ (c a₁ (... (c aₖ n)...))` where each `aᵢ` is a Church numeral. +Church-encoded lists for proving SKI ≃ TM equivalence. A list `[a₀, ... aₖ]` is encoded as +`λ c n. c xa₀ (c xa₁ (... (c xaₖ n)...))` where each `xaᵢ` represents `aᵢ`. -/ namespace Cslib @@ -93,6 +93,8 @@ theorem isEncoding_singleton {x : α} {cx : SKI} (hcx : cx ⊩ x) : (Cons ⬝ cx ⬝ Nil) ⊩ [x] := isEncoding_cons hcx isEncoding_nil +/-! ### Basic recursion on lists -/ + def FoldR := RotR lemma isEncoding_list_foldr {α β : Type*} [Encoded α SKI] [EncodedLift β Red] : @@ -122,7 +124,7 @@ lemma listRecAux_def (xf xa xp : SKI) : SKI.MkPair ⬝ (xf ⬝ xa ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (Cons ⬝ xa ⬝ (Snd ⬝ xp)) := listRecAuxPoly.toSKI_correct [xf, xa, xp] (by simp) -lemma listRecAux_correct {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] +lemma isEncoding_listRecAux {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) : (listRecAux ⬝ xf) ⊩ (List.recPairStep f) := by intro a xa ha p xp hp @@ -137,7 +139,7 @@ lemma isEncoding_recPairStep_foldr {α β : Type*} [EncodedLift α Red] [Encoded (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) ⊩ (⟨List.rec b f as, as⟩ : β × List α) := by rw [←List.recPairStep_foldr] - refine isEncoding_list_foldr (listRecAux_correct hf) ?_ has + refine isEncoding_list_foldr (isEncoding_listRecAux hf) ?_ has exact isEncoding_mkPair hb isEncoding_nil def listRecPoly : SKI.Polynomial 3 := diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index ea0a9a6b2..83e5bb62d 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -81,7 +81,10 @@ instance instEncodedLiftNat : EncodedLift Nat Red where (a ⬝ f ⬝ x) ⭢ a' ⬝ f ⬝ x := red_head _ _ x <| red_head _ _ f <| h _ ↠ Church n f x := by apply ha' -/-! ### Church numeral basics -/ +/-! ### Church numeral basics + +Canonical constructors, iteration and primitive recursion. +-/ /-- Church zero := λ f x. x -/ protected def Zero : SKI := K ⬝ I @@ -125,7 +128,7 @@ def toChurch : ℕ → SKI /-- `toChurch n` correctly represents `n`. -/ @[scoped grind .] -theorem toChurch_correct (n : ℕ) : (toChurch n) ⊩ n := by +theorem isEncoding_toChurch (n : ℕ) : (toChurch n) ⊩ n := by induction n with | zero => exact isEncoding_zero | succ n ih => exact isEncoding_succ ih @@ -151,7 +154,7 @@ lemma isEncoding_iter : Iter ⊩ (Nat.iterate (α := α)) := by def Nat.recPairStep (f : Nat → α → α) : α × Nat → α × Nat | ⟨y, m⟩ => ⟨f m y, m + 1⟩ -lemma Nat.recPairStep_correct {α' : Type*} (a : α') (f : Nat → α' → α') (n : Nat) : +lemma Nat.isEncoding_recPairStep {α' : Type*} (a : α') (f : Nat → α' → α') (n : Nat) : (Nat.recPairStep f)^[n] ⟨a, 0⟩ = ⟨Nat.rec a f n, n⟩ := by induction n with | zero => simp @@ -176,10 +179,10 @@ lemma natRecAux_correct {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) : · exact hf hp.2 hp.1 · exact SKI.isEncoding_succ hp.2 -lemma isEncoded_recPairStep_iter {a : α} {xa : SKI} (ha : xa ⊩ a) +lemma isEncoding_recPairStep_iter {a : α} {xa : SKI} (ha : xa ⊩ a) {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) {n : Nat} {xn : SKI} (hn : xn ⊩ n) : (R ⬝ (natRecAux ⬝ xf) ⬝ xn ⬝ (MkPair ⬝ xa ⬝ SKI.Zero)) ⊩ (⟨Nat.rec a f n, n⟩ : α × Nat) := by - rw [←Nat.recPairStep_correct] + rw [←Nat.isEncoding_recPairStep] refine isEncoding_iter (natRecAux_correct hf) hn ?_ apply isEncoding_mkPair · exact ha @@ -196,7 +199,7 @@ lemma natRec_def (xa xf xn : SKI) : theorem isEncoding_nat_rec : natRec ⊩ (Nat.rec : α → (Nat → α → α) → Nat → α) := by intro a xa ha f xf hf n xn hn - exact IsEncoding.left_of_mRed (isEncoded_recPairStep_iter ha hf hn).1 (natRec_def xa xf xn) + exact IsEncoding.left_of_mRed (isEncoding_recPairStep_iter ha hf hn).1 (natRec_def xa xf xn) def Pred : SKI := natRec ⬝ SKI.Zero ⬝ K @@ -315,7 +318,7 @@ protected def Mul : SKI := MulPoly.toSKI theorem mul_def (a b : SKI) : (SKI.Mul ⬝ a ⬝ b) ↠ a ⬝ (SKI.Add ⬝ b) ⬝ SKI.Zero := MulPoly.toSKI_correct [a, b] (by simp) -theorem mul_correct : SKI.Mul ⊩ Nat.mul := by +theorem isEncoding_mul : SKI.Mul ⊩ Nat.mul := by intro n xn hn m xm hm refine IsEncoding.left_of_mRed (y := Church n (SKI.Add ⬝ xm) SKI.Zero) ?_ ?_ · clear hn @@ -332,7 +335,7 @@ protected def Sub : SKI := SubPoly.toSKI theorem sub_def (a b : SKI) : (SKI.Sub ⬝ a ⬝ b) ↠ b ⬝ Pred ⬝ a := SubPoly.toSKI_correct [a, b] (by simp) -theorem sub_correct : SKI.Sub ⊩ Nat.sub := by +theorem isEncoding_sub : SKI.Sub ⊩ Nat.sub := by intro n xn hn m xm hm refine IsEncoding.left_of_mRed (y := Church m Pred xn) ?_ ?_ · clear hm @@ -351,12 +354,12 @@ protected def LE : SKI := LEPoly.toSKI theorem le_def (a b : SKI) : (SKI.LE ⬝ a ⬝ b) ↠ IsZero ⬝ (SKI.Sub ⬝ a ⬝ b) := LEPoly.toSKI_correct [a, b] (by simp) -theorem le_correct : SKI.LE ⊩ (· ≤ · : Nat → Nat → Bool) := by +theorem isEncoding_le : SKI.LE ⊩ (· ≤ · : Nat → Nat → Bool) := by intro n xn hn m xm hm simp_rw [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le] apply IsEncoding.left_of_mRed (y := IsZero ⬝ (SKI.Sub ⬝ xn ⬝ xm)) (h := le_def _ _) apply isEncoding_isZero - apply sub_correct <;> assumption + apply isEncoding_sub <;> assumption end SKI From d333a5b8b2d7e8108bfa331c5da80ab05c846b3e Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 7 Mar 2026 12:47:09 +0100 Subject: [PATCH 10/12] rename --- Cslib/Foundations/Semantics/Encoded.lean | 56 --------- Cslib/Foundations/Semantics/Realizes.lean | 56 +++++++++ Cslib/Languages/CombinatoryLogic/List.lean | 78 ++++++------ .../{Encoded.lean => Realizes.lean} | 111 ++++++++++-------- .../Languages/CombinatoryLogic/Recursion.lean | 104 ++++++++-------- 5 files changed, 206 insertions(+), 199 deletions(-) delete mode 100644 Cslib/Foundations/Semantics/Encoded.lean create mode 100644 Cslib/Foundations/Semantics/Realizes.lean rename Cslib/Languages/CombinatoryLogic/{Encoded.lean => Realizes.lean} (60%) diff --git a/Cslib/Foundations/Semantics/Encoded.lean b/Cslib/Foundations/Semantics/Encoded.lean deleted file mode 100644 index f7058fd28..000000000 --- a/Cslib/Foundations/Semantics/Encoded.lean +++ /dev/null @@ -1,56 +0,0 @@ -/- -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 - -/-- Types encoded some calculus. -/ -class Encoded (α β : Type*) where - /-- An element is represented by a term. -/ - IsEncoding : α → β → Prop - -def IsEncoding {α β : Type*} [Encoded α β] : α → β → Prop := Encoded.IsEncoding - -scoped notation x " ⊩ " a => IsEncoding a x - -/-- Types for which encodings are invariant by anti-reduction. -/ -class EncodedLift (α : Type*) {β : Type*} (r : β → β → Prop) extends Encoded α β where - /-- Representation lifts along reductions. -/ - isEncoding_left_of_red : {a : α} → {x y : β} → (y ⊩ a) → r x y → x ⊩ a - -/-- Types for which encodings are invariant by reduction. -/ -class EncodedDesc (α : Type*) {β : Type*} (r : β → β → Prop) extends Encoded α β where - /-- Representation descends along reductions. -/ - isEncoding_right_of_red : {a : α} → {x y : β} → (x ⊩ a) → r x y → y ⊩ a - -variable {α β : Type*} {r : β → β → Prop} - -lemma IsEncoding.left_of_red [EncodedLift α r] {a : α} {x y : β} (ha : y ⊩ a) (h : r x y) : - x ⊩ a := EncodedLift.isEncoding_left_of_red ha h - -lemma IsEncoding.left_of_mRed [EncodedLift α 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 IsEncoding.right_of_red [EncodedDesc α r] {a : α} {x y : β} (ha : x ⊩ a) (h : r x y) : - y ⊩ a := EncodedDesc.isEncoding_right_of_red ha h - -lemma IsEncoding.right_of_mRed [EncodedDesc α 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 diff --git a/Cslib/Foundations/Semantics/Realizes.lean b/Cslib/Foundations/Semantics/Realizes.lean new file mode 100644 index 000000000..51335ccd5 --- /dev/null +++ b/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 diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean index ee01e3b03..c63c37dec 100644 --- a/Cslib/Languages/CombinatoryLogic/List.lean +++ b/Cslib/Languages/CombinatoryLogic/List.lean @@ -23,22 +23,22 @@ namespace SKI open Red MRed -variable {α β : Type*} [Encoded α SKI] [Encoded β SKI] +variable {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] /-! ### Church List Representation -/ /-- A term correctly Church-encodes a list. -/ -def IsEncodingList : List α → SKI → Prop - | [], cns => ∀ c n : SKI, (cns ⬝ c ⬝ n) ↠ n - | a :: as, cns => ∀ c n : SKI, - ∃ cx cxs : SKI, IsEncoding a cx ∧ IsEncodingList as cxs ∧ +def RealizesList (cns : SKI) : List α → Prop + | [] => ∀ c n : SKI, (cns ⬝ c ⬝ n) ↠ n + | a :: as => ∀ c n : SKI, + ∃ cx cxs : SKI, Realizes cx a ∧ RealizesList cxs as ∧ (cns ⬝ c ⬝ n) ↠ c ⬝ cx ⬝ (cxs ⬝ c ⬝ n) -instance instEncodedList : Encoded (List α) SKI where - IsEncoding := IsEncodingList +instance instEncodedList : HasRealizer (List α) SKI where + Realizes := RealizesList -instance instEncodedLiftList [EncodedLift α Red] : EncodedLift (List α) Red where - isEncoding_left_of_red := by +instance instHasRealizerLiftList [HasRealizerLift α Red] : HasRealizerLift (List α) Red where + realizes_left_of_red := by intro as cns cns' has h induction as generalizing cns cns' with | nil => @@ -67,7 +67,7 @@ theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n := NilPoly.toSKI_correct [c, n] (by simp) /-- The empty list term correctly represents `[]`. -/ -theorem isEncoding_nil : Nil ⊩ ([] : List α) := nil_def +theorem realizes_nil : Nil ⊩ ([] : List α) := nil_def /-! ### Cons: Consing an element onto a list -/ @@ -83,21 +83,21 @@ theorem cons_def (x xs c n : SKI) : ConsPoly.toSKI_correct [x, xs, c, n] (by simp) /-- Cons preserves Church list representation. -/ -theorem isEncoding_cons : Cons ⊩ (List.cons : α → List α → List α) := by +theorem realizes_cons : Cons ⊩ (List.cons : α → List α → List α) := by intro c cx hx xs cxs hxs c n use cx, cxs, hx, hxs exact cons_def cx cxs c n /-- Singleton list correctness. -/ -theorem isEncoding_singleton {x : α} {cx : SKI} (hcx : cx ⊩ x) : +theorem realizes_singleton {x : α} {cx : SKI} (hcx : cx ⊩ x) : (Cons ⬝ cx ⬝ Nil) ⊩ [x] := - isEncoding_cons hcx isEncoding_nil + realizes_cons hcx realizes_nil /-! ### Basic recursion on lists -/ def FoldR := RotR -lemma isEncoding_list_foldr {α β : Type*} [Encoded α SKI] [EncodedLift β Red] : +lemma realizes_list_foldr {α β : Type*} [HasRealizer α SKI] [HasRealizerLift β Red] : FoldR ⊩ (List.foldr : (α → β → β) → β → List α → β) := by intro f xf hf b xb hb l xl hl suffices (xl ⬝ xf ⬝ xb) ⊩ (l.foldr f b) by apply this.left_of_mRed <| rotR_def .. @@ -105,7 +105,7 @@ lemma isEncoding_list_foldr {α β : Type*} [Encoded α SKI] [EncodedLift β Red | nil => exact hb.left_of_mRed <| hl .. | cons a l ih => obtain ⟨xa, xl', ha, hl', hred⟩ := hl xf xb - have : IsEncoding (f a (List.foldr f b l)) (xf ⬝ xa ⬝ (xl' ⬝ xf ⬝ xb)) := + have : Realizes (xf ⬝ xa ⬝ (xl' ⬝ xf ⬝ xb)) (f a (List.foldr f b l)) := hf ha (ih hl') exact this.left_of_mRed hred @@ -124,23 +124,23 @@ lemma listRecAux_def (xf xa xp : SKI) : SKI.MkPair ⬝ (xf ⬝ xa ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (Cons ⬝ xa ⬝ (Snd ⬝ xp)) := listRecAuxPoly.toSKI_correct [xf, xa, xp] (by simp) -lemma isEncoding_listRecAux {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] +lemma realizes_listRecAux {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) : (listRecAux ⬝ xf) ⊩ (List.recPairStep f) := by intro a xa ha p xp hp - refine IsEncoding.left_of_mRed (α := β × List α) ?_ (listRecAux_def xf xa xp) - apply isEncoding_mkPair + refine Realizes.left_of_mRed (α := β × List α) ?_ (listRecAux_def xf xa xp) + apply realizes_mkPair · exact hf ha hp.2 hp.1 - · exact isEncoding_cons ha hp.2 + · exact realizes_cons ha hp.2 -lemma isEncoding_recPairStep_foldr {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] +lemma realizes_recPairStep_foldr {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] {b : β} {xb : SKI} (hb : xb ⊩ b) {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) {as : List α} {xas : SKI} (has : xas ⊩ as) : (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) ⊩ (⟨List.rec b f as, as⟩ : β × List α) := by rw [←List.recPairStep_foldr] - refine isEncoding_list_foldr (isEncoding_listRecAux hf) ?_ has - exact isEncoding_mkPair hb isEncoding_nil + refine realizes_list_foldr (realizes_listRecAux hf) ?_ has + exact realizes_mkPair hb realizes_nil def listRecPoly : SKI.Polynomial 3 := Fst ⬝' (SKI.RotR ⬝' (listRecAux ⬝' &1) ⬝' (MkPair ⬝' &0 ⬝' Nil) ⬝' &2) @@ -149,20 +149,20 @@ lemma listRec_def (xb xf xas : SKI) : (listRec ⬝ xb ⬝ xf ⬝ xas) ↠ Fst ⬝ (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) := listRecPoly.toSKI_correct [xb, xf, xas] (by simp) -theorem isEncoding_list_rec {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : +theorem realizes_list_rec {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] : listRec ⊩ (List.rec : β → (α → List α → β → β) → List α → β) := by intro b xb hb f xf hf as xas has - have := isEncoding_recPairStep_foldr hb hf has + have := realizes_recPairStep_foldr hb hf has exact this.1.left_of_mRed <| listRec_def .. def Tail := (listRec ⬝ Nil ⬝ (&1 : SKI.Polynomial 3).toSKI) -lemma isEncoding_tail {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : +lemma realizes_tail {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] : Tail ⊩ (List.tail : List α → List α) := by intro as xas has have : (as.tail = as.rec [] (fun _ t _ => t)) := by cases as <;> rfl rw [this] - refine isEncoding_list_rec isEncoding_nil ?_ has + refine realizes_list_rec realizes_nil ?_ has intro _ xs _ t xt ht _ xu _ apply ht.left_of_mRed <| (&1 : SKI.Polynomial 3).toSKI_correct [xs, xt, xu] (by simp) @@ -179,18 +179,18 @@ theorem headD_def (d xs : SKI) : (HeadD ⬝ d ⬝ xs) ↠ xs ⬝ K ⬝ d := HeadDPoly.toSKI_correct [d, xs] (by simp) /-- General head-with-default correctness. -/ -theorem isEncoding_headD {α : Type*} [EncodedLift α Red] : +theorem realizes_headD {α : Type*} [HasRealizerLift α Red] : HeadD ⊩ (fun a (as : List α) => as.headD a) := by intro a xa ha as xas has match as with | [] => simp only [List.headD_nil] - refine IsEncoding.left_of_mRed ?_ (headD_def xa xas) + refine Realizes.left_of_mRed ?_ (headD_def xa xas) apply ha.left_of_mRed exact has K xa | x :: xs => simp only [List.headD_cons] - refine IsEncoding.left_of_mRed ?_ (headD_def xa xas) + refine Realizes.left_of_mRed ?_ (headD_def xa xas) obtain ⟨cx, cxs, hcx, _, hred⟩ := has K xa apply hcx.left_of_mRed exact hred.trans <| MRed.K .. @@ -203,9 +203,9 @@ theorem head_def (xs : SKI) : (Head ⬝ xs) ↠ xs ⬝ K ⬝ SKI.Zero := headD_def SKI.Zero xs /-- Head correctness (default 0). -/ -theorem isEncoding_head : Head ⊩ (fun (xs : List Nat) => xs.headD 0) := by +theorem realizes_head : Head ⊩ (fun (xs : List Nat) => xs.headD 0) := by intro ns xns hns - exact isEncoding_headD isEncoding_zero hns + exact realizes_headD realizes_zero hns /-! ### Prepending zero to a list (for Code.zero') -/ @@ -220,10 +220,10 @@ theorem prependZero_def (xs : SKI) : (PrependZero ⬝ xs) ↠ Cons ⬝ SKI.Zero PrependZeroPoly.toSKI_correct [xs] (by simp) /-- Prepending zero preserves Church list representation. -/ -theorem isEncoding_prependZero : PrependZero ⊩ (fun ns => 0 :: ns) := by +theorem realizes_prependZero : PrependZero ⊩ (fun ns => 0 :: ns) := by intro ns cns hns - refine IsEncoding.left_of_mRed ?_ (prependZero_def cns) - exact isEncoding_cons isEncoding_zero hns + refine Realizes.left_of_mRed ?_ (prependZero_def cns) + exact realizes_cons realizes_zero hns /-! ### Successor on list head (for Code.succ) -/ @@ -231,13 +231,13 @@ theorem isEncoding_prependZero : PrependZero ⊩ (fun ns => 0 :: ns) := by def SuccHead : SKI := B ⬝ (C ⬝ Cons ⬝ Nil) ⬝ (B ⬝ SKI.Succ ⬝ Head) /-- `SuccHead` correctly computes a singleton containing `succ(head ns)`. -/ -theorem isEncoding_prependSucc : SuccHead ⊩ (fun (ns : List Nat) => [ns.headD 0 + 1]) := by +theorem realizes_prependSucc : SuccHead ⊩ (fun (ns : List Nat) => [ns.headD 0 + 1]) := by intro ns cns hcns - have hhead := isEncoding_head hcns - have hsucc := isEncoding_succ hhead - refine IsEncoding.left_of_mRed ?_ + have hhead := realizes_head hcns + have hsucc := realizes_succ hhead + refine Realizes.left_of_mRed ?_ (.trans (B_tail_mred _ _ _ _ (B_def .Succ Head cns)) (C_def Cons Nil _)) - exact isEncoding_cons hsucc isEncoding_nil + exact realizes_cons hsucc realizes_nil end List diff --git a/Cslib/Languages/CombinatoryLogic/Encoded.lean b/Cslib/Languages/CombinatoryLogic/Realizes.lean similarity index 60% rename from Cslib/Languages/CombinatoryLogic/Encoded.lean rename to Cslib/Languages/CombinatoryLogic/Realizes.lean index 6bacc449b..ca0faab32 100644 --- a/Cslib/Languages/CombinatoryLogic/Encoded.lean +++ b/Cslib/Languages/CombinatoryLogic/Realizes.lean @@ -7,32 +7,32 @@ Authors: Thomas Waring module public import Cslib.Languages.CombinatoryLogic.Basic -public import Cslib.Foundations.Semantics.Encoded +public import Cslib.Foundations.Semantics.Realizes public import Mathlib.Data.Part @[expose] public section namespace Cslib.SKI -open Red MRed Relation Encoded IsEncoding +open Red MRed Relation HasRealizer Realizes /-- A term `xf` encodes a function `f : α → β` if for every `xa ⊩ a : α`, `xf ⬝ a ⊩ f a`. -/ -instance instEncodedPi (α β : Type*) [hα : Encoded α SKI] [hβ : Encoded β SKI] : - Encoded (α → β) SKI where - IsEncoding f z := ∀ {a : α} {x : SKI}, (x ⊩ a) → (z ⬝ x) ⊩ (f a) +instance instHasRealizerPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizer β SKI] : + HasRealizer (α → β) SKI where + Realizes z f := ∀ {a : α} {x : SKI}, (x ⊩ a) → (z ⬝ x) ⊩ (f a) -instance instEncodedLiftPi (α β : Type*) [hα : Encoded α SKI] [hβ : EncodedLift β Red] : - EncodedLift (α → β) Red where - isEncoding_left_of_red := by +instance instHasRealizerLiftPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizerLift β Red] : + HasRealizerLift (α → β) Red where + realizes_left_of_red := by intro f x y hy h a z hz - apply EncodedLift.isEncoding_left_of_red (hy hz) + apply HasRealizerLift.realizes_left_of_red (hy hz) exact red_head _ _ _ h -instance instEncodedDescPi (α β : Type*) [hα : Encoded α SKI] [hβ : EncodedDesc β Red] : - EncodedDesc (α → β) Red where - isEncoding_right_of_red := by +instance instHasRealizerDescPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizerDesc β Red] : + HasRealizerDesc (α → β) Red where + realizes_right_of_red := by intro f x y hy h a z hz - apply EncodedDesc.isEncoding_right_of_red (hy hz) + apply HasRealizerDesc.realizes_right_of_red (hy hz) exact red_head _ _ _ h /-! @@ -41,9 +41,9 @@ instance instEncodedDescPi (α β : Type*) [hα : Encoded α SKI] [hβ : Encoded `xu ⊩ u` if `xu` is βη-equivalent to the standard Church boolean. -/ -instance instEncodedLiftBool : EncodedLift Bool Red where - IsEncoding u z := ∀ x y : SKI, (z ⬝ x ⬝ y) ↠ (if u then x else y) - isEncoding_left_of_red := by +instance instHasRealizerLiftBool : HasRealizerLift Bool Red where + Realizes z u := ∀ x y : SKI, (z ⬝ x ⬝ y) ↠ (if u then x else y) + realizes_left_of_red := by intro u x y hu h a b trans y ⬝ a ⬝ b · apply MRed.head; apply MRed.head; exact Relation.ReflTransGen.single h @@ -54,13 +54,13 @@ instance instEncodedLiftBool : EncodedLift Bool Red where def TT : SKI := K @[scoped grind .] -theorem TT_correct : TT ⊩ true := fun x y ↦ MRed.K x y +theorem realizes_true : TT ⊩ true := fun x y ↦ MRed.K x y /-- Standard false: FF := λ x y. y -/ def FF : SKI := K ⬝ I @[scoped grind .] -theorem FF_correct : FF ⊩ false := +theorem realizes_false : FF ⊩ false := 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 @@ -77,7 +77,7 @@ lemma cond_def {xu y z} {u : Bool} (hu : xu ⊩ u) : · exact hu .. } -lemma isEncoding_cond {α : Type*} [EncodedLift α Red] : +lemma realizes_cond {α : Type*} [HasRealizerLift α Red] : SKI.Cond ⊩ (fun (a b : α) (u : Bool) => if u then a else b) := by intro a xa ha b xb hb u xu hu cases u @@ -115,12 +115,13 @@ theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by cal _ ⭢ I ⬝ b := red_head _ _ b <| red_K .. _ ⭢ b := red_I b -instance instEncodedProd {α β : Type*} [Encoded α SKI] [Encoded β SKI] : Encoded (α × β) SKI where - IsEncoding p x := ((Fst ⬝ x) ⊩ p.1) ∧ (Snd ⬝ x) ⊩ p.2 +instance instHasRealizerProd {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] : + HasRealizer (α × β) SKI where + Realizes x p := ((Fst ⬝ x) ⊩ p.1) ∧ (Snd ⬝ x) ⊩ p.2 -instance instEncodedLiftProd {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : - EncodedLift (α × β) Red where - isEncoding_left_of_red := by +instance instHasRealizerLiftProd {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] : + HasRealizerLift (α × β) Red where + realizes_left_of_red := by intro p x y ⟨hp₁, hp₂⟩ h constructor · apply hp₁.left_of_mRed @@ -128,9 +129,9 @@ instance instEncodedLiftProd {α β : Type*} [EncodedLift α Red] [EncodedLift · apply hp₂.left_of_mRed exact Relation.ReflTransGen.single <| red_tail Snd _ _ h -instance instEncodedDescProd {α β : Type*} [EncodedDesc α Red] [EncodedDesc β Red] : - EncodedDesc (α × β) Red where - isEncoding_right_of_red := by +instance instHasRealizerDescProd {α β : Type*} [HasRealizerDesc α Red] [HasRealizerDesc β Red] : + HasRealizerDesc (α × β) Red where + realizes_right_of_red := by intro p x y ⟨hp₁, hp₂⟩ h constructor · apply hp₁.right_of_mRed @@ -139,19 +140,19 @@ instance instEncodedDescProd {α β : Type*} [EncodedDesc α Red] [EncodedDesc exact Relation.ReflTransGen.single <| red_tail Snd _ _ h /-- The pairing term `SKI.MkPair` indeed encodes `Prod.Mk`. -/ -lemma isEncoding_mkPair {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : +lemma realizes_mkPair {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] : SKI.MkPair ⊩ (Prod.mk : α → β → α × β) := by intro a xa ha b xb hb constructor · exact ha.left_of_mRed <| fst_correct .. · exact hb.left_of_mRed <| snd_correct .. -lemma isEncoding_fst {α β : Type*} [Encoded α SKI] [Encoded β SKI] : +lemma realizes_fst {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] : SKI.Fst ⊩ (Prod.fst : α × β → α) := by intro _ _ h exact h.1 -lemma isEncoding_snd {α β : Type*} [Encoded α SKI] [Encoded β SKI] : +lemma realizes_snd {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] : SKI.Snd ⊩ (Prod.snd : α × β → β) := by intro _ _ h exact h.2 @@ -162,8 +163,8 @@ def prodRec := prodRecPoly.toSKI lemma prodRec_def (xf xp : SKI) : (prodRec ⬝ xf ⬝ xp) ↠ xf ⬝ (Fst ⬝ xp) ⬝ (Snd ⬝ xp) := prodRecPoly.toSKI_correct [xf, xp] (by simp) -theorem isEncoding_prod_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] - [EncodedLift γ Red] : prodRec ⊩ (Prod.rec : (α → β → γ) → α × β → γ) := by +theorem realizes_prod_rec {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI] + [HasRealizerLift γ Red] : prodRec ⊩ (Prod.rec : (α → β → γ) → α × β → γ) := by intro f xf hf p xp hp exact (hf hp.1 hp.2).left_of_mRed <| prodRec_def .. @@ -174,16 +175,17 @@ theorem isEncoding_prod_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] `xa ⊩ a`, or `g ⬝ xb`, for `s = .inr b` and `xb ⊩ b`. -/ -def isEncodingSum {α β : Type*} [Encoded α SKI] [Encoded β SKI] : α ⊕ β → SKI → Prop - | .inl a, x => ∀ f g : SKI, ∃ xa : SKI, (xa ⊩ a) ∧ (x ⬝ f ⬝ g) ↠ f ⬝ xa - | .inr b, x => ∀ f g : SKI, ∃ xb : SKI, (xb ⊩ b) ∧ (x ⬝ f ⬝ g) ↠ g ⬝ xb +def realizesSum {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] (x : SKI) : α ⊕ β → Prop + | .inl a => ∀ f g : SKI, ∃ xa : SKI, (xa ⊩ a) ∧ (x ⬝ f ⬝ g) ↠ f ⬝ xa + | .inr b => ∀ f g : SKI, ∃ xb : SKI, (xb ⊩ b) ∧ (x ⬝ f ⬝ g) ↠ g ⬝ xb -instance instEncodedSum {α β : Type*} [Encoded α SKI] [Encoded β SKI] : Encoded (α ⊕ β) SKI where - IsEncoding := isEncodingSum +instance instHasRealizerSum {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] : + HasRealizer (α ⊕ β) SKI where + Realizes := realizesSum -instance instEncodedLiftSum {α β : Type*} [EncodedLift α Red] [EncodedLift β Red] : - EncodedLift (α ⊕ β) Red where - isEncoding_left_of_red := by +instance instHasRealizerLiftSum {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] : + HasRealizerLift (α ⊕ β) Red where + realizes_left_of_red := by intro ab x y hy h cases ab case inl a => @@ -202,7 +204,7 @@ protected def Inl : SKI := inlPoly.toSKI lemma inl_def (a f g : SKI) : (SKI.Inl ⬝ a ⬝ f ⬝ g) ↠ f ⬝ a := inlPoly.toSKI_correct [a, f, g] (by simp) -lemma isEncoding_sum_inl {α β : Type*} [Encoded α SKI] [Encoded β SKI] : +lemma realizes_sum_inl {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] : SKI.Inl ⊩ (Sum.inl : α → α ⊕ β) := by intro a xa ha f g use xa, ha, inl_def .. @@ -212,15 +214,15 @@ protected def Inr : SKI := inrPoly.toSKI lemma inr_def (a f g : SKI) : (SKI.Inr ⬝ a ⬝ f ⬝ g) ↠ g ⬝ a := inrPoly.toSKI_correct [a, f, g] (by simp) -lemma isEncoding_sum_inr {α β : Type*} [Encoded α SKI] [Encoded β SKI] : +lemma realizes_sum_inr {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] : SKI.Inr ⊩ (Sum.inr : β → α ⊕ β) := by intro b xb hb f g use xb, hb, inr_def .. def sumRec : SKI := RotR -theorem isEncoding_sum_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] [EncodedLift γ Red] : - sumRec ⊩ (Sum.rec : (α → γ) → (β → γ) → α ⊕ β → γ) := by +theorem realizes_sum_rec {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI] + [HasRealizerLift γ Red] : sumRec ⊩ (Sum.rec : (α → γ) → (β → γ) → α ⊕ β → γ) := by intro f xf hf g xg hg ab xab hab cases ab with | inl a => @@ -236,27 +238,32 @@ theorem isEncoding_sum_rec {α β γ : Type*} [Encoded α SKI] [Encoded β SKI] A term `x` encodes a partial value `o` if `o = Part.none`, or `o = Part.some a` and `x ⊩ a`. -/ -instance instEncodedPart {α : Type*} [Encoded α SKI] : Encoded (Part α) SKI where - IsEncoding o x := (h : o.Dom) → x ⊩ (o.get h) +instance instHasRealizerPart {α : Type*} [HasRealizer α SKI] : HasRealizer (Part α) SKI where + Realizes x o := (h : o.Dom) → x ⊩ (o.get h) -lemma isEncoding_of_mem {α : Type*} [Encoded α SKI] {o : Part α} {x : SKI} (h : x ⊩ o) +lemma realizes_of_mem {α : Type*} [HasRealizer α SKI] {o : Part α} {x : SKI} (h : x ⊩ o) {a : α} (ha : a ∈ o) : x ⊩ a := by obtain ⟨hao, ha⟩ := ha exact ha ▸ h hao -lemma isEncoding_some_iff {α : Type*} [Encoded α SKI] {a : α} {x : SKI} : +lemma realizes_some_iff {α : Type*} [HasRealizer α SKI] {a : α} {x : SKI} : (x ⊩ Part.some a) ↔ x ⊩ a := by refine ⟨?_, ?_⟩ · intro h; exact h (Part.some_dom a) · intro h; exact fun _ => h -instance instEncodedLiftPart {α : Type*} [EncodedLift α Red] : EncodedLift (Part α) Red where - isEncoding_left_of_red := by +lemma realizes_none {α : Type*} [HasRealizer α SKI] (x : SKI) : x ⊩ (Part.none : Part α) := + fun h => False.elim (Part.not_none_dom h) + +instance instHasRealizerLiftPart {α : Type*} [HasRealizerLift α Red] : + HasRealizerLift (Part α) Red where + realizes_left_of_red := by intro o x y ho h hdom exact (ho hdom).left_of_red h -instance instEncodedDescPart {α : Type*} [EncodedDesc α Red] : EncodedDesc (Part α) Red where - isEncoding_right_of_red := by +instance instHasRealizerDescPart {α : Type*} [HasRealizerDesc α Red] : + HasRealizerDesc (Part α) Red where + realizes_right_of_red := by intro o x y ho h hdom exact (ho hdom).right_of_red h diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index 83e5bb62d..3d39a3f73 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -6,7 +6,7 @@ Authors: Thomas Waring module -public import Cslib.Languages.CombinatoryLogic.Encoded +public import Cslib.Languages.CombinatoryLogic.Realizes @[expose] public section @@ -73,9 +73,9 @@ lemma church_red (n : Nat) (f f' x x' : SKI) (hf : f ↠ f') (hx : x ↠ x') : | zero => exact hx | succ n ih => exact parallel_mRed hf ih -instance instEncodedLiftNat : EncodedLift Nat Red where - IsEncoding n a := ∀ f x : SKI, (a ⬝ f ⬝ x) ↠ (Church n f x) - isEncoding_left_of_red := by +instance instHasRealizerLiftNat : HasRealizerLift Nat Red where + Realizes a n := ∀ f x : SKI, (a ⬝ f ⬝ x) ↠ (Church n f x) + realizes_left_of_red := by intro n a a' ha' h f x calc (a ⬝ f ⬝ x) ⭢ a' ⬝ f ⬝ x := red_head _ _ x <| red_head _ _ f <| h @@ -90,7 +90,7 @@ Canonical constructors, iteration and primitive recursion. protected def Zero : SKI := K ⬝ I @[scoped grind .] -theorem isEncoding_zero : SKI.Zero ⊩ 0 := by +theorem realizes_zero : SKI.Zero ⊩ 0 := by intro f x calc _ ↠ I ⬝ x := by apply Relation.ReflTransGen.single; apply red_head; apply red_K @@ -100,7 +100,7 @@ theorem isEncoding_zero : SKI.Zero ⊩ 0 := by protected def One : SKI := I @[scoped grind .] -theorem isEncoding_one : SKI.One ⊩ 1 := by +theorem realizes_one : SKI.One ⊩ 1 := by intro f x apply head exact .single (red_I f) @@ -108,7 +108,7 @@ theorem isEncoding_one : SKI.One ⊩ 1 := by /-- Church succ := λ a f x. f (a f x) ~ λ a f. B f (a f) ~ λ a. S B a ~ S B -/ protected def Succ : SKI := S ⬝ B -theorem isEncoding_succ : SKI.Succ ⊩ Nat.succ := by +theorem realizes_succ : SKI.Succ ⊩ Nat.succ := by intro n xn hn f x calc _ ⭢ B ⬝ f ⬝ (xn ⬝ f) ⬝ x := by apply red_head; apply red_S @@ -128,18 +128,18 @@ def toChurch : ℕ → SKI /-- `toChurch n` correctly represents `n`. -/ @[scoped grind .] -theorem isEncoding_toChurch (n : ℕ) : (toChurch n) ⊩ n := by +theorem realizes_toChurch (n : ℕ) : (toChurch n) ⊩ n := by induction n with - | zero => exact isEncoding_zero - | succ n ih => exact isEncoding_succ ih + | zero => exact realizes_zero + | succ n ih => exact realizes_succ ih -variable {α : Type*} [EncodedLift α Red] +variable {α : Type*} [HasRealizerLift α Red] def Iter := R -lemma isEncoding_iter : Iter ⊩ (Nat.iterate (α := α)) := by +lemma realizes_iter : Iter ⊩ (Nat.iterate (α := α)) := by intro f xf hf n xn hn a xa ha - suffices IsEncoding (f^[n] a) (Church n xf xa) by + suffices (Church n xf xa) ⊩ f^[n] a by apply this.left_of_mRed calc _ ↠ xn ⬝ xf ⬝ xa := MRed.head _ <| R_def .. @@ -154,7 +154,7 @@ lemma isEncoding_iter : Iter ⊩ (Nat.iterate (α := α)) := by def Nat.recPairStep (f : Nat → α → α) : α × Nat → α × Nat | ⟨y, m⟩ => ⟨f m y, m + 1⟩ -lemma Nat.isEncoding_recPairStep {α' : Type*} (a : α') (f : Nat → α' → α') (n : Nat) : +lemma Nat.realizes_recPairStep {α' : Type*} (a : α') (f : Nat → α' → α') (n : Nat) : (Nat.recPairStep f)^[n] ⟨a, 0⟩ = ⟨Nat.rec a f n, n⟩ := by induction n with | zero => simp @@ -169,24 +169,24 @@ lemma natRecAux_def (f p : SKI) : (natRecAux ⬝ f ⬝ p) ↠ SKI.MkPair ⬝ (f ⬝ (Snd ⬝ p) ⬝ (Fst ⬝ p)) ⬝ (SKI.Succ ⬝ (Snd ⬝ p)) := natRecAuxPoly.toSKI_correct [f, p] (by simp) -lemma natRecAux_correct {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) : +lemma natRecAux_realizes {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) : (natRecAux ⬝ xf) ⊩ (Nat.recPairStep f) := by intro p xp hp - suffices IsEncoding (Nat.recPairStep f p) - (SKI.MkPair ⬝ (xf ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (SKI.Succ ⬝ (Snd ⬝ xp))) by + suffices (SKI.MkPair ⬝ (xf ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (SKI.Succ ⬝ (Snd ⬝ xp))) ⊩ + (Nat.recPairStep f p) by exact this.left_of_mRed <| natRecAux_def .. - apply isEncoding_mkPair + apply realizes_mkPair · exact hf hp.2 hp.1 - · exact SKI.isEncoding_succ hp.2 + · exact SKI.realizes_succ hp.2 -lemma isEncoding_recPairStep_iter {a : α} {xa : SKI} (ha : xa ⊩ a) +lemma realizes_recPairStep_iter {a : α} {xa : SKI} (ha : xa ⊩ a) {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) {n : Nat} {xn : SKI} (hn : xn ⊩ n) : (R ⬝ (natRecAux ⬝ xf) ⬝ xn ⬝ (MkPair ⬝ xa ⬝ SKI.Zero)) ⊩ (⟨Nat.rec a f n, n⟩ : α × Nat) := by - rw [←Nat.isEncoding_recPairStep] - refine isEncoding_iter (natRecAux_correct hf) hn ?_ - apply isEncoding_mkPair + rw [←Nat.realizes_recPairStep] + refine realizes_iter (natRecAux_realizes hf) hn ?_ + apply realizes_mkPair · exact ha - · exact isEncoding_zero + · exact realizes_zero def natRecPoly : SKI.Polynomial 3 := Fst ⬝' (R ⬝' (natRecAux ⬝' &1) ⬝' &2 ⬝' (MkPair ⬝' &0 ⬝' SKI.Zero)) @@ -196,18 +196,18 @@ lemma natRec_def (xa xf xn : SKI) : natRecPoly.toSKI_correct [xa, xf, xn] (by simp) /-- Primitive recursion on `Nat`. -/ -theorem isEncoding_nat_rec : +theorem realizes_nat_rec : natRec ⊩ (Nat.rec : α → (Nat → α → α) → Nat → α) := by intro a xa ha f xf hf n xn hn - exact IsEncoding.left_of_mRed (isEncoding_recPairStep_iter ha hf hn).1 (natRec_def xa xf xn) + exact Realizes.left_of_mRed (realizes_recPairStep_iter ha hf hn).1 (natRec_def xa xf xn) def Pred : SKI := natRec ⬝ SKI.Zero ⬝ K -theorem isEncoding_pred : Pred ⊩ Nat.pred := by +theorem realizes_pred : Pred ⊩ Nat.pred := by intro n xn hn have : n.pred = n.rec 0 (fun a _ => a) := by induction n <;> simp rw [this] - refine isEncoding_nat_rec isEncoding_zero ?_ hn + refine realizes_nat_rec realizes_zero ?_ hn intro _ _ h _ _ _ exact h.left_of_red <| red_K .. @@ -218,18 +218,18 @@ def IsZero : SKI := IsZeroPoly.toSKI theorem isZero_def (a : SKI) : (IsZero ⬝ a) ↠ a ⬝ (K ⬝ FF) ⬝ TT := IsZeroPoly.toSKI_correct [a] (by simp) -theorem isEncoding_isZero : IsZero ⊩ (· == 0) := by +theorem realizes_isZero : IsZero ⊩ (· == 0) := by intro n xn hn - refine IsEncoding.left_of_mRed ?_ (isZero_def _) + refine Realizes.left_of_mRed ?_ (isZero_def _) by_cases n = 0 case pos h0 => simp_rw [h0] at hn ⊢ - exact TT_correct.left_of_mRed <| hn .. + exact realizes_true.left_of_mRed <| hn .. case neg h0 => simp_rw [beq_false_of_ne h0] let ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero h0 rw [hk] at hn - apply FF_correct.left_of_mRed + apply realizes_false.left_of_mRed calc _ ↠ (K ⬝ FF) ⬝ Church k (K ⬝ FF) TT := hn .. _ ⭢ FF := red_K .. @@ -253,13 +253,13 @@ theorem rfindAboveAux_base (R₀ f a : SKI) (hfa : (f ⬝ a) ⊩ 0) : (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ a := calc _ ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := rfindAboveAux_def _ _ _ _ ↠ if (Nat.beq 0 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by - exact cond_def <| isEncoding_isZero hfa + exact cond_def <| realizes_isZero hfa theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : (f ⬝ a) ⊩ m + 1) : (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f := calc _ ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := rfindAboveAux_def _ _ _ _ ↠ if (Nat.beq (m + 1) 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by - exact cond_def <| isEncoding_isZero hfa + exact cond_def <| realizes_isZero hfa /-- Find the minimal root of `fNat` above a number n -/ def RFindAbove : SKI := RFindAboveAux.fixedPoint @@ -268,14 +268,14 @@ theorem RFindAbove_correct (f : Nat → Nat) (xf x : SKI) (hf : xf ⊩ f) (n m : (hroot : f (m + n) = 0) (hpos : ∀ i < n, f (m + i) ≠ 0) : (RFindAbove ⬝ x ⬝ xf) ⊩ (m + n) := by induction n generalizing m x - all_goals apply IsEncoding.left_of_mRed (y := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ xf) + all_goals apply Realizes.left_of_mRed (y := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ xf) case zero.ha => apply hx.left_of_mRed apply rfindAboveAux_base exact hroot ▸ hf hx case succ.ha n ih => - apply IsEncoding.left_of_mRed (y := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ xf) - · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (isEncoding_succ hx) + apply Realizes.left_of_mRed (y := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ xf) + · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (realizes_succ hx) grind · have : (xf ⬝ x) ⊩ ((f m).pred + 1) := Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf hx exact rfindAboveAux_step _ _ _ this @@ -286,7 +286,7 @@ theorem RFindAbove_correct (f : Nat → Nat) (xf x : SKI) (hf : xf ⊩ f) (n m : def RFind := RFindAbove ⬝ SKI.Zero theorem RFind_correct (f : Nat → Nat) (xf : SKI) (hf : xf ⊩ f) (n : Nat) (hroot : f n = 0) (hpos : ∀ i < n, f i ≠ 0) : (RFind ⬝ xf) ⊩ n := by - have :_ := RFindAbove_correct (n := n) (f := f) (hf := hf) (hx := isEncoding_zero) + have :_ := RFindAbove_correct (n := n) (f := f) (hf := hf) (hx := realizes_zero) simp_rw [Nat.zero_add] at this exact this hroot hpos @@ -299,14 +299,14 @@ protected def Add : SKI := AddPoly.toSKI theorem add_def (a b : SKI) : (SKI.Add ⬝ a ⬝ b) ↠ a ⬝ SKI.Succ ⬝ b := AddPoly.toSKI_correct [a, b] (by simp) -theorem isEncoding_add : SKI.Add ⊩ Nat.add:= by +theorem realizes_add : SKI.Add ⊩ Nat.add:= by intro n xn hn m xm hm - refine IsEncoding.left_of_mRed (y := Church n SKI.Succ xm) ?_ ?_ + refine Realizes.left_of_mRed (y := Church n SKI.Succ xm) ?_ ?_ · clear hn induction n with | zero => simpa | succ n ih => - simpa [Nat.add_right_comm] using isEncoding_succ ih + simpa [Nat.add_right_comm] using realizes_succ ih · calc _ ↠ xn ⬝ SKI.Succ ⬝ xm := add_def .. _ ↠ Church n SKI.Succ xm := hn .. @@ -318,14 +318,14 @@ protected def Mul : SKI := MulPoly.toSKI theorem mul_def (a b : SKI) : (SKI.Mul ⬝ a ⬝ b) ↠ a ⬝ (SKI.Add ⬝ b) ⬝ SKI.Zero := MulPoly.toSKI_correct [a, b] (by simp) -theorem isEncoding_mul : SKI.Mul ⊩ Nat.mul := by +theorem realizes_mul : SKI.Mul ⊩ Nat.mul := by intro n xn hn m xm hm - refine IsEncoding.left_of_mRed (y := Church n (SKI.Add ⬝ xm) SKI.Zero) ?_ ?_ + refine Realizes.left_of_mRed (y := Church n (SKI.Add ⬝ xm) SKI.Zero) ?_ ?_ · clear hn induction n with - | zero => simpa using isEncoding_zero + | zero => simpa using realizes_zero | succ n ih => - simpa [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church] using isEncoding_add hm ih + simpa [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church] using realizes_add hm ih · exact Trans.trans (mul_def xn xm) (hn (SKI.Add ⬝ xm) SKI.Zero) /-- Subtraction: λ n m. n Pred m -/ @@ -335,14 +335,14 @@ protected def Sub : SKI := SubPoly.toSKI theorem sub_def (a b : SKI) : (SKI.Sub ⬝ a ⬝ b) ↠ b ⬝ Pred ⬝ a := SubPoly.toSKI_correct [a, b] (by simp) -theorem isEncoding_sub : SKI.Sub ⊩ Nat.sub := by +theorem realizes_sub : SKI.Sub ⊩ Nat.sub := by intro n xn hn m xm hm - refine IsEncoding.left_of_mRed (y := Church m Pred xn) ?_ ?_ + refine Realizes.left_of_mRed (y := Church m Pred xn) ?_ ?_ · clear hm induction m with | zero => simpa using hn | succ m ih => - simpa using isEncoding_pred ih + simpa using realizes_pred ih · calc _ ↠ xm ⬝ Pred ⬝ xn := sub_def .. _ ↠ Church m Pred xn := hm Pred xn @@ -354,12 +354,12 @@ protected def LE : SKI := LEPoly.toSKI theorem le_def (a b : SKI) : (SKI.LE ⬝ a ⬝ b) ↠ IsZero ⬝ (SKI.Sub ⬝ a ⬝ b) := LEPoly.toSKI_correct [a, b] (by simp) -theorem isEncoding_le : SKI.LE ⊩ (· ≤ · : Nat → Nat → Bool) := by +theorem realizes_le : SKI.LE ⊩ (· ≤ · : Nat → Nat → Bool) := by intro n xn hn m xm hm simp_rw [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le] - apply IsEncoding.left_of_mRed (y := IsZero ⬝ (SKI.Sub ⬝ xn ⬝ xm)) (h := le_def _ _) - apply isEncoding_isZero - apply isEncoding_sub <;> assumption + apply Realizes.left_of_mRed (y := IsZero ⬝ (SKI.Sub ⬝ xn ⬝ xm)) (h := le_def _ _) + apply realizes_isZero + apply realizes_sub <;> assumption end SKI From 7ce7cf120c6819b153e6cb568e59a5cb6aedc770 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 7 Mar 2026 12:49:34 +0100 Subject: [PATCH 11/12] tidy up evaluation --- Cslib/Languages/CombinatoryLogic/Evaluation.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Evaluation.lean b/Cslib/Languages/CombinatoryLogic/Evaluation.lean index 299c748d4..7647d1b80 100644 --- a/Cslib/Languages/CombinatoryLogic/Evaluation.lean +++ b/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,7 +284,7 @@ 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 => @@ -291,7 +292,7 @@ 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 ⬝ (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 From ede415261baeff4dbdd6d6ff7d99a1887a3a8372 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 20 Mar 2026 17:33:43 +0100 Subject: [PATCH 12/12] basic combinators --- Cslib/Languages/CombinatoryLogic/Basic.lean | 7 ++ .../Languages/CombinatoryLogic/Realizes.lean | 77 ++++++++++++++++--- 2 files changed, 73 insertions(+), 11 deletions(-) diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index beaa86519..df32b8676 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/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 -/ diff --git a/Cslib/Languages/CombinatoryLogic/Realizes.lean b/Cslib/Languages/CombinatoryLogic/Realizes.lean index ca0faab32..163cb2459 100644 --- a/Cslib/Languages/CombinatoryLogic/Realizes.lean +++ b/Cslib/Languages/CombinatoryLogic/Realizes.lean @@ -8,7 +8,7 @@ module public import Cslib.Languages.CombinatoryLogic.Basic public import Cslib.Foundations.Semantics.Realizes -public import Mathlib.Data.Part +public import Mathlib.Data.PFun @[expose] public section @@ -16,6 +16,13 @@ namespace Cslib.SKI open Red MRed Relation HasRealizer Realizes +/-! ### Function types + +Realizers for a function type `α → β` are defined by a logical relation: `xf ⊩ f` if for every +`xa ⊩ a`, `xf ⬝ xa ⊩ f a`. We provide realizer interpretations for the primitive combinators +`S`,`K` and `I` as well as those from the `BCKW` basis. +-/ + /-- A term `xf` encodes a function `f : α → β` if for every `xa ⊩ a : α`, `xf ⬝ a ⊩ f a`. -/ instance instHasRealizerPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizer β SKI] : HasRealizer (α → β) SKI where @@ -35,6 +42,28 @@ instance instHasRealizerDescPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : apply HasRealizerDesc.realizes_right_of_red (hy hz) exact red_head _ _ _ h +lemma realizes_id {α : Type*} [HasRealizerLift α Red] : I ⊩ (id : α → α) := + fun ha => ha.left_of_red <| red_I _ + +lemma realizes_const {α β : Type*} [HasRealizerLift α Red] [HasRealizer β SKI] : + K ⊩ (Function.const β : α → β → α) := fun ha _ _ _ => ha.left_of_red <| red_K .. + +lemma realizes_S {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI] + [HasRealizerLift γ Red] : S ⊩ (fun (f : α → β → γ) (g : α → β) (a : α) => f a (g a)) := + fun hf _ _ hg _ _ ha => (hf ha (hg ha)).left_of_red <| red_S .. + +lemma realizes_comp {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI] + [HasRealizerLift γ Red] : B ⊩ (Function.comp : (β → γ) → (α → β) → α → γ) := + fun hf _ _ hg _ _ ha => (hf <| hg ha).left_of_mRed <| B_def .. + +lemma realizes_swap {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI] + [HasRealizerLift γ Red] : C ⊩ (Function.swap : (α → β → γ) → β → α → γ) := + fun hf _ _ hb _ _ ha => (hf ha hb).left_of_mRed <| C_def .. + +lemma realizes_diagonal_app {α β : Type*} [HasRealizer α SKI] [HasRealizerLift β Red] : + W ⊩ (fun (f : α → α → β) (a : α) => f a a) := + fun hf _ _ ha => (hf ha ha).left_of_mRed <| W_def .. + /-! ### Booleans @@ -46,7 +75,7 @@ instance instHasRealizerLiftBool : HasRealizerLift Bool Red where realizes_left_of_red := by intro u x y hu h a b trans y ⬝ a ⬝ b - · apply MRed.head; apply MRed.head; exact Relation.ReflTransGen.single h + · apply MRed.head; apply MRed.head; exact ReflTransGen.single h · exact hu a b @@ -62,8 +91,8 @@ def FF : SKI := K ⬝ I @[scoped grind .] theorem realizes_false : FF ⊩ false := 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 + (FF ⬝ x ⬝ y) ↠ I ⬝ y := by apply 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 @@ -125,9 +154,9 @@ instance instHasRealizerLiftProd {α β : Type*} [HasRealizerLift α Red] [HasRe intro p x y ⟨hp₁, hp₂⟩ h constructor · apply hp₁.left_of_mRed - exact Relation.ReflTransGen.single <| red_tail Fst _ _ h + exact ReflTransGen.single <| red_tail Fst _ _ h · apply hp₂.left_of_mRed - exact Relation.ReflTransGen.single <| red_tail Snd _ _ h + exact ReflTransGen.single <| red_tail Snd _ _ h instance instHasRealizerDescProd {α β : Type*} [HasRealizerDesc α Red] [HasRealizerDesc β Red] : HasRealizerDesc (α × β) Red where @@ -135,9 +164,9 @@ instance instHasRealizerDescProd {α β : Type*} [HasRealizerDesc α Red] [HasRe intro p x y ⟨hp₁, hp₂⟩ h constructor · apply hp₁.right_of_mRed - exact Relation.ReflTransGen.single <| red_tail Fst _ _ h + exact ReflTransGen.single <| red_tail Fst _ _ h · apply hp₂.right_of_mRed - exact Relation.ReflTransGen.single <| red_tail Snd _ _ h + exact ReflTransGen.single <| red_tail Snd _ _ h /-- The pairing term `SKI.MkPair` indeed encodes `Prod.Mk`. -/ lemma realizes_mkPair {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] : @@ -192,12 +221,12 @@ instance instHasRealizerLiftSum {α β : Type*} [HasRealizerLift α Red] [HasRea intro f g obtain ⟨xa, ha, hred⟩ := hy f g use xa, ha - exact Relation.ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred + exact ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred case inr b => intro f g obtain ⟨xb, hb, hred⟩ := hy f g use xb, hb - exact Relation.ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred + exact ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred def inlPoly : SKI.Polynomial 3 := &1 ⬝' &0 protected def Inl : SKI := inlPoly.toSKI @@ -235,7 +264,8 @@ theorem realizes_sum_rec {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β /-! ### Partial values -A term `x` encodes a partial value `o` if `o = Part.none`, or `o = Part.some a` and `x ⊩ a`. +A term `x` encodes a partial value `o` if `o = Part.none`, or `o = Part.some a` and `x ⊩ a`. We +specialize the definition of realizers for function types to partial functions `a →. β`. -/ instance instHasRealizerPart {α : Type*} [HasRealizer α SKI] : HasRealizer (Part α) SKI where @@ -255,6 +285,11 @@ lemma realizes_some_iff {α : Type*} [HasRealizer α SKI] {a : α} {x : SKI} : lemma realizes_none {α : Type*} [HasRealizer α SKI] (x : SKI) : x ⊩ (Part.none : Part α) := fun h => False.elim (Part.not_none_dom h) +lemma realizes_some {α : Type*} [HasRealizerLift α Red] : I ⊩ (Part.some : α → Part α) := by + intro a xa ha + rw [realizes_some_iff] + exact ha.left_of_red (red_I xa) + instance instHasRealizerLiftPart {α : Type*} [HasRealizerLift α Red] : HasRealizerLift (Part α) Red where realizes_left_of_red := by @@ -267,4 +302,24 @@ instance instHasRealizerDescPart {α : Type*} [HasRealizerDesc α Red] : intro o x y ho h hdom exact (ho hdom).right_of_red h +instance instHasRealizerPFun (α β : Type*) [HasRealizer α SKI] [HasRealizer β SKI] : + HasRealizer (α →. β) SKI := inferInstanceAs <| HasRealizer (α → Part β) SKI + +instance instHasRealizerLiftPFun (α β : Type*) [hα : HasRealizer α SKI] + [hβ : HasRealizerLift β Red] : HasRealizerLift (α →. β) Red := + inferInstanceAs <| HasRealizerLift (α → Part β) Red + +instance instHasRealizerDescPFun (α β : Type*) [hα : HasRealizer α SKI] + [hβ : HasRealizerDesc β Red] : HasRealizerDesc (α →. β) Red := + inferInstanceAs <| HasRealizerDesc (α → Part β) Red + +lemma realizes_pfun_iff {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] (xf : SKI) + (f : α →. β) : + (xf ⊩ f) ↔ ∀ {a : α} (ha : a ∈ f.Dom) {xa : SKI}, (xa ⊩ a) → (xf ⬝ xa) ⊩ f.fn a ha := by + constructor + · intro h a ha xa hxa + exact h hxa ha + · intro h a xa ha hdom + exact h hdom ha + end Cslib.SKI