From af4fffb0e8e06d309072bab993311d0969f22bdf Mon Sep 17 00:00:00 2001 From: Andrej Bauer Date: Wed, 11 Dec 2024 09:40:17 +0100 Subject: [PATCH] Move PCAs to separate file, define CAs. --- PartialCombinatoryAlgebras.lean | 2 + PartialCombinatoryAlgebras/Basic.lean | 199 ----------------- .../CombinatoryAlgebra.lean | 51 +++++ .../FreeCombinatoryAlgebra.lean | 7 +- .../PartialCombinatoryAlgebra.lean | 202 ++++++++++++++++++ PartialCombinatoryAlgebras/Programming.lean | 65 ++++-- 6 files changed, 303 insertions(+), 223 deletions(-) create mode 100644 PartialCombinatoryAlgebras/CombinatoryAlgebra.lean create mode 100644 PartialCombinatoryAlgebras/PartialCombinatoryAlgebra.lean diff --git a/PartialCombinatoryAlgebras.lean b/PartialCombinatoryAlgebras.lean index 00381d4..10f7c16 100644 --- a/PartialCombinatoryAlgebras.lean +++ b/PartialCombinatoryAlgebras.lean @@ -2,4 +2,6 @@ -- Import modules here that should be built as part of the library. import PartialCombinatoryAlgebras.Basic +import PartialCombinatoryAlgebras.PartialCombinatoryAlgebra import PartialCombinatoryAlgebras.Programming +import PartialCombinatoryAlgebras.CombinatoryAlgebra diff --git a/PartialCombinatoryAlgebras/Basic.lean b/PartialCombinatoryAlgebras/Basic.lean index 2b0063d..c9fac90 100644 --- a/PartialCombinatoryAlgebras/Basic.lean +++ b/PartialCombinatoryAlgebras/Basic.lean @@ -1,28 +1,4 @@ import Mathlib.Data.Part -import Mathlib.Data.Finset.Basic - -/-! -# Partial combinatory algebras - -A partial combinatory algebra is a set equipped with a partial binary operation, -which has the so-called combinators `K` and `S`. We formalize it in two stages. - -We first define the class `PartialApplication` which equips a given set `A` with -a partial binary operation. One might expect such an operation to have type -`A → A → Part A`, but this leads to complications because it is not composable. -So instead we specify that a partial operation is a map of type `Part A → Part A → Part A`. -In other words, we *always* work with partial elements, and separately state that they are -total as necessary. - -(It would be natural to require that the applications be strict, i.e., if the result is defined -so are its arguments. An early version did so, but the assumption of strictness was never used.) - -We then define the class `PCA` (partial combinatory algebra) to be an extension of -`PartialApplication`. It prescribed combinators `K` and `S` satisfying the usual properties. -Following our strategy, `K` and `S` are again partial elements on the carrier set, -with a separate claim that they are total. - --/ /-- A notation for totality of a partial element (we find writing `x.Dom` a bit silly). -/ notation:50 u:max " ⇓ " => Part.Dom u @@ -42,178 +18,3 @@ class PartialApplication (A : Type*) where instance PartialApplication.hasDot {A : Type*} [PartialApplication A] : HasDot (Part A) where dot := app - -/-- The partial combinatory structure on a set `A`. -/ -class PCA (A : Type*) extends PartialApplication A where - K : Part A - S : Part A - df_K₀ : K ⇓ - df_K₁ : ∀ {u : Part A}, u ⇓ → (K ⬝ u) ⇓ - df_S₀ : S ⇓ - df_S₁ : ∀ {u : Part A}, u ⇓ → (S ⬝ u) ⇓ - df_S₂ : ∀ {u v : Part A}, u ⇓ → v ⇓ → (S ⬝ u ⬝ v) ⇓ - eq_K : ∀ (u v : Part A), u ⇓ → v ⇓ → (K ⬝ u ⬝ v) = u - eq_S : ∀ (u v w : Part A), u ⇓ → v ⇓ → w ⇓ → S ⬝ u ⬝ v ⬝ w = (u ⬝ w) ⬝ (v ⬝ w) - -attribute [simp] PCA.df_K₀ -attribute [simp] PCA.df_K₁ -attribute [simp] PCA.eq_K -attribute [simp] PCA.df_S₀ -attribute [simp] PCA.df_S₁ -attribute [simp] PCA.df_S₂ -attribute [simp] PCA.eq_S - -/-- Every PCA is inhabited. We pick K as its default element. -/ -instance PCA.inhabited {A : Type*} [PCA A] : Inhabited A where - default := K.get df_K₀ - -/-! `Expr Γ A` is the type of expressions built inductively from - constants `K` and `S`, variables in `Γ` (the variable context), - the elements of a carrier set `A`, and formal binary application. - - The usual accounts of PCAs typically do not introduce `K` and `S` - as separate constants, because a PCA `A` already contains such combinators. - However, as we defined the combinators to be partial elements, it is more - convenient to have separate primitive constants denoting them. - Also, this way `A` need not be an applicative structure. --/ - -/-- Expressions with variables from context `Γ` and elements from `A`. -/ -inductive Expr (Γ A : Type*) where - /-- Formal expression denoting the K combinator -/ -| K : Expr Γ A - /-- Formal expression denoting the S combinator -/ -| S : Expr Γ A - /-- An element as a formal expression -/ -| elm : A → Expr Γ A - /-- A variable as a formal expression -/ -| var : Γ → Expr Γ A - /-- Formal expression application -/ -| app : Expr Γ A → Expr Γ A → Expr Γ A - -/-- Formal application as a binary operation `·` -/ -instance Expr.hasDot {Γ A : Type*} : HasDot (Expr Γ A) where - dot := Expr.app - -namespace Expr - universe u v - variable {Γ : Type u} [DecidableEq Γ] - variable {A : Type v} [PCA A] - - /-- A valuation `η : Γ → A` assigning elements to variables, - with the value of `x` overridden to be `a`. -/ - @[reducible] - def override (x : Γ) (a : A) (η : Γ → A) (y : Γ) : A := - if y = x then a else η y - - /-- Evaluate an expression with respect to a given valuation `η`. -/ - def eval (η : Γ → A): Expr Γ A → Part A - | .K => PCA.K - | .S => PCA.S - | .elm a => .some a - | .var x => .some (η x) - | .app e₁ e₂ => (eval η e₁) ⬝ (eval η e₂) - - /-- An expression is said to be defined when it is defined at every valuation. -/ - def defined (e : Expr Γ A) := ∀ (η : Γ → A), (eval η e) ⇓ - - /-- The substitution of an element for the extra variable. -/ - def subst (x : Γ) (a : A) : Expr Γ A → Expr Γ A - | K => K - | S => S - | elm b => elm b - | var y => if y = x then elm a else var y - | app e₁ e₂ => (subst x a e₁) ⬝ (subst x a e₂) - - /-- `abstr e` is an expression with one fewer variables than - the expression `e`, which works similarly to function - abastraction in the λ-calculus. It is at the heart of - combinatory completeness. -/ - def abstr (x : Γ): Expr Γ A → Expr Γ A - | K => K ⬝ K - | S => K ⬝ S - | elm a => K ⬝ elm a - | var y => if y = x then S ⬝ K ⬝ K else K ⬝ var y - | app e₁ e₂ => S ⬝ (abstr x e₁) ⬝ (abstr x e₂) - - /-- An abstraction is defined. -/ - @[simp] - lemma df_abstr (x : Γ) (e : Expr Γ A) : defined (abstr x e) := by - intro η - induction e - case K => simp [eval] - case S => simp [eval] - case elm => simp [eval] - case var y => - cases (decEq y x) - case isFalse h => simp [abstr, eval, h] - case isTrue h => simp [abstr, eval, h] - case app e₁ e₂ ih₁ ih₂ => simp [eval, ih₁, ih₂] - - /-- `eval_abstr e` behaves like abstraction in the extra variable. - This is known as *combinatory completeness*. -/ - lemma eval_abstr (x : Γ) (e : Expr Γ A) (a : A) (η : Γ → A): - eval η (abstr x e ⬝ elm a) = eval (override x a η) e := by - induction e - case K => simp [eval] - case S => simp [eval] - case elm => simp [eval] - case var y => - cases (decEq y x) - case isFalse h => simp [eval, abstr, override, h] - case isTrue h => simp [eval, abstr, override, h] - case app e₁ e₂ ih₁ ih₂ => - simp [abstr, eval] at ih₁ - simp [abstr, eval] at ih₂ - simp [abstr, eval, df_abstr x _ η, ih₁, ih₂] - - /-- Like `eval_abstr` but with the application on the outside of `eval`. -/ - lemma eval_abstr_app (η : Γ → A) (x : Γ) (e : Expr Γ A) (u : Part A) (hu : u ⇓) : - eval η (abstr x e) ⬝ u = eval (override x (u.get hu) η) e := by - calc - _ = eval η (abstr x e ⬝ elm (u.get hu)) := by simp [eval] - _ = eval (override x (u.get hu) η) e := by apply eval_abstr - - @[simp] - lemma eval_override (η : Γ → A) (x : Γ) (a : A) (e : Expr Γ A) : - eval (override x a η) e = eval η (subst x a e) := by - induction e - case K => simp [eval] - case S => simp [eval] - case elm => simp [eval] - case var y => - cases (decEq y x) - case isFalse p => simp [eval, subst, p] - case isTrue p => simp [eval, subst, p] - case app e₁ e₂ ih₁ ih₂ => simp [eval, ih₁, ih₂] - - /-- Compile an expression to a partial element, substituting - the default value for any variables occurring in e. -/ - @[simp] - def compile (e : Expr Γ A) : Part A := - eval (fun _ => default) e - - /-- Evaluate an expression under the assumption that it is closed. - Return `inl x` if variable `x` is encountered, otherwise `inr u` - where `u` is the partial element so obtained. -/ - def eval_closed : Expr Γ A → Sum Γ (Part A) - | K => return PCA.K - | S => return PCA.S - | elm a => return (some a) - | var x => .inl x - | app e₁ e₂ => - do - let a₁ ← eval_closed e₁ ; - let a₂ ← eval_closed e₂ ; - return (a₁ ⬝ a₂) - - syntax:20 "≪" term "≫" term:20 : term - - macro_rules - | `(≪ $x:term ≫ $a:term) => `(Expr.abstr $x $a) - - syntax "[pca: " term "]" : term - macro_rules - | `([pca: $e:term ]) => `(Expr.compile (Γ := Lean.Name) $e) - -end Expr diff --git a/PartialCombinatoryAlgebras/CombinatoryAlgebra.lean b/PartialCombinatoryAlgebras/CombinatoryAlgebra.lean new file mode 100644 index 0000000..501222f --- /dev/null +++ b/PartialCombinatoryAlgebras/CombinatoryAlgebra.lean @@ -0,0 +1,51 @@ +import Mathlib.Data.Part +import PartialCombinatoryAlgebras.Basic + +/-- A (total) combinatory structure on a set `A`. -/ +class CA (A : Type*) extends HasDot A where + K : A + S : A + eq_K : ∀ {a b : A}, K ⬝ a ⬝ b = a + eq_S : ∀ (a b c : A), S ⬝ a ⬝ b ⬝ c = (a ⬝ c) ⬝ (b ⬝ c) + +attribute [simp] PCA.eq_K +attribute [simp] PCA.eq_S + +/-- Missing from `Part` -/ +@[simps] +def Part.map₂ {α β γ : Type*} (f : α → β → γ) (u : Part α) (v : Part β) : Part γ := + ⟨u.Dom ∧ v.Dom, fun p => f (u.get (And.left p)) (v.get (And.right p))⟩ + +@[simp] +lemma Part.eq_map₂_some {α β γ : Type*} (f : α → β → γ) (a : α) (b : β) : + Part.map₂ f (.some a) (.some b) = .some (f a b) := by + ext c + simp [map₂] + constructor <;> apply Eq.symm + +namespace CA + + /-- A total application induces a partial application -/ + @[reducible] + instance partialApp {A : Type} [d : HasDot A] : PartialApplication A where + app := Part.map₂ d.dot + + lemma eq_app {A : Type} [HasDot A] {u v : Part A} (hu : u ⇓) (hv : v ⇓): + u ⬝ v = .some (u.get hu ⬝ v.get hv) := by + nth_rewrite 1 [←Part.some_get hu] + nth_rewrite 1 [←Part.some_get hv] + apply Part.eq_map₂_some + + /-- A combinatory algebra is a PCA -/ + instance isPCA {A : Type} [CA A] : PCA A where + K := .some K + S := .some S + df_K₀ := by trivial + df_K₁ := by intros ; trivial + eq_K := by intro _ _ hu hv ; simp [CA.eq_app, hu, hv, CA.eq_K] + df_S₀ := by trivial + df_S₁ := by intros ; trivial + df_S₂ := by intros ; trivial + eq_S := by intro _ _ _ hu hv hw ; simp [CA.eq_app, hu, hv, hw, CA.eq_S] + + end CA diff --git a/PartialCombinatoryAlgebras/FreeCombinatoryAlgebra.lean b/PartialCombinatoryAlgebras/FreeCombinatoryAlgebra.lean index fa24bda..7cd8c5b 100644 --- a/PartialCombinatoryAlgebras/FreeCombinatoryAlgebra.lean +++ b/PartialCombinatoryAlgebras/FreeCombinatoryAlgebra.lean @@ -1,4 +1,5 @@ import PartialCombinatoryAlgebras.Basic +import PartialCombinatoryAlgebras.PartialCombinatoryAlgebra /-! # Free (total) combinatory algebra -/ @@ -71,7 +72,7 @@ instance CAisApplicativeStructure : PartialApplication carrier where @[simp] theorem df_app (u v : Part carrier) : u ⇓ → v ⇓ → (u ⬝ v) ⇓ := by intros hu hv - unfold raise₂ + sorry instance CAisPCA : PCA carrier where K := mk .K @@ -83,8 +84,8 @@ instance CAisPCA : PCA carrier where df_S₁ hu := by simp [hu] df_S₂ hu hv := by simp [hu, hv] - eq_K u v hu hv := by + eq_K u v hu hv := by sorry - eq_S u v w _ _ _ := sorry + eq_S u v w _ _ _ := by sorry end FreeCombinatoryAlgebra diff --git a/PartialCombinatoryAlgebras/PartialCombinatoryAlgebra.lean b/PartialCombinatoryAlgebras/PartialCombinatoryAlgebra.lean new file mode 100644 index 0000000..6fbc780 --- /dev/null +++ b/PartialCombinatoryAlgebras/PartialCombinatoryAlgebra.lean @@ -0,0 +1,202 @@ +import Mathlib.Data.Finset.Basic +import PartialCombinatoryAlgebras.Basic + +/-! +# Partial combinatory algebras + +A partial combinatory algebra is a set equipped with a partial binary operation, +which has the so-called combinators `K` and `S`. We formalize it in two stages. + +We first define the class `PartialApplication` which equips a given set `A` with +a partial binary operation. One might expect such an operation to have type +`A → A → Part A`, but this leads to complications because it is not composable. +So instead we specify that a partial operation is a map of type `Part A → Part A → Part A`. +In other words, we *always* work with partial elements, and separately state that they are +total as necessary. + +(It would be natural to require that the applications be strict, i.e., if the result is defined +so are its arguments. An early version did so, but the assumption of strictness was never used.) + +We then define the class `PCA` (partial combinatory algebra) to be an extension of +`PartialApplication`. It prescribed combinators `K` and `S` satisfying the usual properties. +Following our strategy, `K` and `S` are again partial elements on the carrier set, +with a separate claim that they are total. + +-/ + +/-- The partial combinatory structure on a set `A`. -/ +class PCA (A : Type*) extends PartialApplication A where + K : Part A + S : Part A + df_K₀ : K ⇓ + df_K₁ : ∀ {u : Part A}, u ⇓ → (K ⬝ u) ⇓ + df_S₀ : S ⇓ + df_S₁ : ∀ {u : Part A}, u ⇓ → (S ⬝ u) ⇓ + df_S₂ : ∀ {u v : Part A}, u ⇓ → v ⇓ → (S ⬝ u ⬝ v) ⇓ + eq_K : ∀ (u v : Part A), u ⇓ → v ⇓ → (K ⬝ u ⬝ v) = u + eq_S : ∀ (u v w : Part A), u ⇓ → v ⇓ → w ⇓ → S ⬝ u ⬝ v ⬝ w = (u ⬝ w) ⬝ (v ⬝ w) + +attribute [simp] PCA.df_K₀ +attribute [simp] PCA.df_K₁ +-- attribute [simp] eq_K +attribute [simp] PCA.df_S₀ +attribute [simp] PCA.df_S₁ +attribute [simp] PCA.df_S₂ +-- attribute [simp] eq_S + +/-- Every PCA is inhabited. We pick K as its default element. -/ +instance PCA.inhabited {A : Type*} [PCA A] : Inhabited A where + default := K.get df_K₀ + +/-! `Expr Γ A` is the type of expressions built inductively from + constants `K` and `S`, variables in `Γ` (the variable context), + the elements of a carrier set `A`, and formal binary application. + + The usual accounts of PCAs typically do not introduce `K` and `S` + as separate constants, because a PCA `A` already contains such combinators. + However, as we defined the combinators to be partial elements, it is more + convenient to have separate primitive constants denoting them. + Also, this way `A` need not be an applicative structure. +-/ + +namespace PCA + +/-- Expressions with variables from context `Γ` and elements from `A`. -/ +inductive Expr (Γ A : Type*) where + /-- Formal expression denoting the K combinator -/ +| K : Expr Γ A + /-- Formal expression denoting the S combinator -/ +| S : Expr Γ A + /-- An element as a formal expression -/ +| elm : A → Expr Γ A + /-- A variable as a formal expression -/ +| var : Γ → Expr Γ A + /-- Formal expression application -/ +| app : Expr Γ A → Expr Γ A → Expr Γ A + +/-- Formal application as a binary operation `·` -/ +instance Expr.hasDot {Γ A : Type*} : HasDot (Expr Γ A) where + dot := Expr.app + +section + universe u v + variable {Γ : Type u} [DecidableEq Γ] + variable {A : Type v} [PCA A] + + /-- A valuation `η : Γ → A` assigning elements to variables, + with the value of `x` overridden to be `a`. -/ + @[reducible] + def override (x : Γ) (a : A) (η : Γ → A) (y : Γ) : A := + if y = x then a else η y + + /-- Evaluate an expression with respect to a given valuation `η`. -/ + def eval (η : Γ → A): Expr Γ A → Part A + | .K => PCA.K + | .S => PCA.S + | .elm a => .some a + | .var x => .some (η x) + | .app e₁ e₂ => (eval η e₁) ⬝ (eval η e₂) + + /-- An expression is said to be defined when it is defined at every valuation. -/ + def defined (e : Expr Γ A) := ∀ (η : Γ → A), (eval η e) ⇓ + + /-- The substitution of an element for the extra variable. -/ + def subst (x : Γ) (a : A) : Expr Γ A → Expr Γ A + | .K => .K + | .S => .S + | .elm b => .elm b + | .var y => if y = x then .elm a else .var y + | .app e₁ e₂ => (subst x a e₁) ⬝ (subst x a e₂) + + /-- `abstr e` is an expression with one fewer variables than + the expression `e`, which works similarly to function + abastraction in the λ-calculus. It is at the heart of + combinatory completeness. -/ + def abstr (x : Γ): Expr Γ A → Expr Γ A + | .K => .K ⬝ .K + | .S => .K ⬝ .S + | .elm a => .K ⬝ .elm a + | .var y => if y = x then .S ⬝ .K ⬝ .K else .K ⬝ .var y + | .app e₁ e₂ => .S ⬝ (abstr x e₁) ⬝ (abstr x e₂) + + /-- An abstraction is defined. -/ + @[simp] + lemma df_abstr (x : Γ) (e : Expr Γ A) : defined (abstr x e) := by + intro η + induction e + case K => simp [eval] + case S => simp [eval] + case elm => simp [eval] + case var y => + cases (decEq y x) + case isFalse h => simp [abstr, eval, h] + case isTrue h => simp [abstr, eval, h] + case app e₁ e₂ ih₁ ih₂ => simp [eval, ih₁, ih₂] + + /-- `eval_abstr e` behaves like abstraction in the extra variable. + This is known as *combinatory completeness*. -/ + lemma eval_abstr (x : Γ) (e : Expr Γ A) (a : A) (η : Γ → A): + eval η (abstr x e ⬝ .elm a) = eval (override x a η) e := by + induction e + case K => simp [eq_K, eval] + case S => simp [eq_S, eq_K, eval] + case elm => simp [eq_K, eq_S, eval] + case var y => + cases (decEq y x) + case isFalse h => simp [eq_K, eval, abstr, override, h] + case isTrue h => simp [eq_S, eq_K, eval, abstr, override, h] + case app e₁ e₂ ih₁ ih₂ => + simp [abstr, eval] at ih₁ + simp [abstr, eval] at ih₂ + simp [eq_S, abstr, eval, df_abstr x _ η, ih₁, ih₂] + + /-- Like `eval_abstr` but with the application on the outside of `eval`. -/ + lemma eval_abstr_app (η : Γ → A) (x : Γ) (e : Expr Γ A) (u : Part A) (hu : u ⇓) : + eval η (abstr x e) ⬝ u = eval (override x (u.get hu) η) e := by + calc + _ = eval η (abstr x e ⬝ .elm (u.get hu)) := by simp [eval] + _ = eval (override x (u.get hu) η) e := by apply eval_abstr + + @[simp] + lemma eval_override (η : Γ → A) (x : Γ) (a : A) (e : Expr Γ A) : + eval (override x a η) e = eval η (subst x a e) := by + induction e + case K => simp [eval] + case S => simp [eval] + case elm => simp [eval] + case var y => + cases (decEq y x) + case isFalse p => simp [eval, subst, p] + case isTrue p => simp [eval, subst, p] + case app e₁ e₂ ih₁ ih₂ => simp [eval, ih₁, ih₂] + + /-- Compile an expression to a partial element, substituting + the default value for any variables occurring in e. -/ + @[simp] + def compile (e : Expr Γ A) : Part A := + eval (fun _ => default) e + + /-- Evaluate an expression under the assumption that it is closed. + Return `inl x` if variable `x` is encountered, otherwise `inr u` + where `u` is the partial element so obtained. -/ + def eval_closed : Expr Γ A → Sum Γ (Part A) + | .K => return K + | .S => return S + | .elm a => return (some a) + | .var x => .inl x + | .app e₁ e₂ => + do + let a₁ ← eval_closed e₁ ; + let a₂ ← eval_closed e₂ ; + return (a₁ ⬝ a₂) + + syntax:20 "≪" term "≫" term:20 : term + + macro_rules + | `(≪ $x:term ≫ $a:term) => `(PCA.abstr $x $a) + + syntax "[pca: " term "]" : term + macro_rules + | `([pca: $e:term ]) => `(PCA.compile (Γ := Lean.Name) $e) + +end diff --git a/PartialCombinatoryAlgebras/Programming.lean b/PartialCombinatoryAlgebras/Programming.lean index 192813d..e1c2907 100644 --- a/PartialCombinatoryAlgebras/Programming.lean +++ b/PartialCombinatoryAlgebras/Programming.lean @@ -1,15 +1,34 @@ import PartialCombinatoryAlgebras.Basic +import PartialCombinatoryAlgebras.PartialCombinatoryAlgebra -namespace PCA +/-! ## Programming with PCAs + + A (non-trivial) PCA is Turing-complete in the sense that it implements + every partial computable function. We develop here basic programming + constructs that witness this fact: + + * the identity combinatory `I` + * ordered pairs `pair` with projections `fst` and `snd` + * booleans `true`, `false` and the conditional statement `ite` + * fixed-point combinators `Z` and `Y` + * Curry numerals `numeral n` with `zero`, successor `succ`, predecessor `pred` and primitive recursion `primrec` + * TODO: general recursion (but it should be easy given what we have) - open Expr + For any of the combinators so defined, say `C`, we also prove two lemmas: `df_C` characterizes totality of + expressions involving `C`, and `eq_C` gives the characteristic equation for `C`. These lemmas are automatically + used by `simp`. +-/ + +namespace PCA universe u variable {A : Type u} [PCA A] + /-- The identity combinator -/ def I : Part A := S ⬝ K ⬝ K - def I.elm {Γ} : Expr Γ A := .elm (I.get (PCA.df_S₂ PCA.df_K₀ PCA.df_K₀)) + /-- The expression denoting the identity combinator -/ + def Expr.I {Γ} : Expr Γ A := .S ⬝ .K ⬝ .K @[simp] theorem df_I : (I : Part A) ⇓ := by @@ -17,9 +36,11 @@ namespace PCA @[simp] theorem eq_I {u : Part A} : u ⇓ → I ⬝ u = u := by - intro hu ; simp [I, hu, eval] + intro hu ; simp [eq_S, eq_K, I, hu, eval] - def K' : Part A := K ⬝ (S ⬝ K ⬝ K) + def K' : Part A := K ⬝ I + + def Expr.K' {Γ} : Expr Γ A := .K ⬝ .I @[simp] theorem df_K' : (K' : Part A) ⇓ := by simp [K', eval] @@ -28,11 +49,11 @@ namespace PCA theorem eq_K' (u v : Part A) : u ⇓ → v ⇓ → K' ⬝ u ⬝ v = v := by intros hu hv - simp [K', eval, hu, hv] + simp [K', eq_S, eq_K, eval, hu, hv] /-! ### Pairing -/ - def pair : Part A := [pca: ≪`x≫ ≪`y≫ ≪`z≫ var `z ⬝ var `x ⬝ var `y] + def pair : Part A := [pca: ≪`x≫ ≪`y≫ ≪`z≫ .var `z ⬝ .var `x ⬝ .var `y] @[simp] theorem df_pair : (pair : Part A) ⇓ := by @@ -63,7 +84,7 @@ namespace PCA simp [eval] rw [Part.some_get, Part.some_get, Part.some_get] <;> assumption - def fst : Part A := [pca: ≪ `x ≫ var `x ⬝ Expr.K] + def fst : Part A := [pca: ≪ `x ≫ .var `x ⬝ .K] def fst.elm {Γ}: Expr Γ A := .elm (fst.get (df_abstr _ _ _)) @@ -77,7 +98,7 @@ namespace PCA rw [Part.some_get] assumption - def snd : Part A := [pca: ≪ `x ≫ var `x ⬝ (Expr.K ⬝ (Expr.S ⬝ Expr.K ⬝ Expr.K))] + def snd : Part A := [pca: ≪ `x ≫ .var `x ⬝ .K'] def snd.elm {Γ} : Expr Γ A := .elm (snd.get (df_abstr _ _ _)) @@ -88,7 +109,9 @@ namespace PCA simp [snd] rw [eval_abstr_app, eval_override] simp [eval] - rw [Part.some_get] <;> simp [hu, K'] + rw [Part.some_get] + rfl + assumption @[simp] def eq_fst_pair (u v : Part A) : u ⇓ → v ⇓ → fst ⬝ (pair ⬝ u ⬝ v) = u := by @@ -129,11 +152,11 @@ namespace PCA @[simp] theorem eq_ite_tru (u v : Part A) : u ⇓ → v ⇓ → ite ⬝ tru ⬝ u ⬝ v = u := by intros hu hv - simp [hu, hv, ite, tru] + simp [eq_K, hu, hv, ite, tru] /-! ### The fixed point combinator -/ - def X : Part A := [pca: ≪`x≫ ≪`y≫ ≪`z≫ var `y ⬝ (var `x ⬝ var `x ⬝ var `y) ⬝ var `z] + def X : Part A := [pca: ≪`x≫ ≪`y≫ ≪`z≫ .var `y ⬝ (.var `x ⬝ .var `x ⬝ .var `y) ⬝ .var `z] @[simp] theorem df_X : (X : Part A) ⇓ := by @@ -179,7 +202,7 @@ namespace PCA simp [Z, hu, hv] rw [eq_X] <;> simp [hu, hv] - def W : Part A := [pca: ≪`x≫ ≪`y≫ var `y ⬝ (var `x ⬝ var `x ⬝ var `y)] + def W : Part A := [pca: ≪`x≫ ≪`y≫ .var `y ⬝ (.var `x ⬝ .var `x ⬝ .var `y)] @[simp] def df_W : (W : Part A) ⇓ := by simp [W] ; apply df_abstr @@ -241,10 +264,10 @@ namespace PCA @[simp] theorem eq_iszero_succ (n : Nat): iszero ⬝ (numeral n.succ) = (fal : Part A) := by - simp [iszero, numeral] + simp [iszero, numeral, eq_K] /-- Predecessor of a Curry numeral -/ - def pred : Part A := [pca: ≪`x≫ (fst.elm ⬝ var `x) ⬝ I.elm ⬝ (snd.elm ⬝ var `x)] + def pred : Part A := [pca: ≪`x≫ (fst.elm ⬝ .var `x) ⬝ .I ⬝ (snd.elm ⬝ .var `x)] @[simp] def df_pred : (pred : Part A) ⇓ := by simp [pred] ; apply df_abstr @@ -257,18 +280,18 @@ namespace PCA intro hu simp [pred] rw [eval_abstr_app, eval_override] <;> try assumption - simp [eval] + simp [eval] ; rfl @[simp] theorem eq_pred_succ (u : Part A) : u ⇓ → pred ⬝ (succ ⬝ u) = u := by intro hu simp [pred] - rw [eval_abstr_app, eval_override] <;> simp [eval, succ, fal, hu] + rw [eval_abstr_app, eval_override] <;> simp [eq_K, eq_K', eval, succ, fal, hu] def primrec.R : Part A := [pca: ≪`r≫ ≪`x≫ ≪`f≫ ≪`m≫ - (fst.elm ⬝ var `m) ⬝ (Expr.K ⬝ var `x) ⬝ - (≪ `y ≫ var `f ⬝ (pred.elm ⬝ var `m) ⬝ (var `r ⬝ var `x ⬝ var `f ⬝ (pred.elm ⬝ var `m) ⬝ (Expr.S ⬝ Expr.K ⬝ Expr.K))) + (fst.elm ⬝ .var `m) ⬝ (.K ⬝ .var `x) ⬝ + (≪ `y ≫ .var `f ⬝ (pred.elm ⬝ .var `m) ⬝ (.var `r ⬝ .var `x ⬝ .var `f ⬝ (pred.elm ⬝ .var `m) ⬝ .I)) ] def primrec.eq_R (r u f m : Part A) (hr : r ⇓) (hu : u ⇓) (hf : f ⇓) (hm : m ⇓) : @@ -286,7 +309,7 @@ namespace PCA def primrec.R.elm {Γ} : Expr Γ A := .elm (R.get df_R) /-- Primitive recursion -/ - def primrec : Part A := [pca: ≪`x≫ ≪`f≫ ≪`m≫ (Z.elm ⬝ primrec.R.elm) ⬝ var `x ⬝ var `f ⬝ var `m ⬝ I.elm] + def primrec : Part A := [pca: ≪`x≫ ≪`f≫ ≪`m≫ (Z.elm ⬝ primrec.R.elm) ⬝ .var `x ⬝ .var `f ⬝ .var `m ⬝ .I] @[simp] theorem eq_primrec (u f m : Part A) : @@ -294,7 +317,7 @@ namespace PCA intros hu hf hm simp [primrec] rw [eval_abstr_app, eval_abstr_app, eval_abstr_app, eval_override, eval_override, eval_override] <;> try assumption - simp [eval] + simp [eval] ; rfl theorem eq_primrec_zero (u f : Part A) : u ⇓ → f ⇓ → primrec ⬝ u ⬝ f ⬝ numeral 0 = u := by intro hu hf