diff --git a/PartialCombinatoryAlgebras/Basic.lean b/PartialCombinatoryAlgebras/Basic.lean index a70f503..56ca211 100644 --- a/PartialCombinatoryAlgebras/Basic.lean +++ b/PartialCombinatoryAlgebras/Basic.lean @@ -7,14 +7,16 @@ import Mathlib.Data.Finset.Basic 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 defined the class `PartialApplication` which equips a given set `A` with +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` -which is strict: if an application is defined then so are its arguments. In other -words, we *always* work with partial elements, and separately state that they are +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, @@ -25,7 +27,7 @@ with a separate claim that they are total. /-- A notation for definedness of a partial element (we find writing `x.Dom` a bit silly). -/ notation:50 u:max " ⇓ " => Part.Dom u -/-- A generic notation for a left-associative binary operation -/ +/-- A generic notation for a left-associative binary operation. -/ class HasDot (A : Type*) where /-- (possibly partial) binary application -/ dot : A → A → A @@ -37,10 +39,6 @@ infixl:70 " ⬝ " => HasDot.dot class PartialApplication (A : Type*) where /-- Partial application -/ app : Part A → Part A → Part A - /-- Partial application is strict in the left argument -/ - strict_left : ∀ {u v : Part A}, (app u v) ⇓ → u ⇓ - /-- Partial application is strict in the right argument -/ - strict_right : ∀ {u v : Part A}, (app u v) ⇓ → v ⇓ instance PartialApplication.hasDot {A : Type*} [PartialApplication A] : HasDot (Part A) where dot := app @@ -49,25 +47,25 @@ instance PartialApplication.hasDot {A : Type*} [PartialApplication A] : HasDot ( class PCA (A : Type*) extends PartialApplication A where K : Part A S : Part A - defined_K₀ : K ⇓ - defined_K₁ : ∀ {u : Part A}, u ⇓ → (K ⬝ u) ⇓ - defined_S₀ : S ⇓ - defined_S₁ : ∀ {u : Part A}, u ⇓ → (S ⬝ u) ⇓ - defined_S₂ : ∀ {u v : Part A}, u ⇓ → v ⇓ → (S ⬝ u ⬝ v) ⇓ + 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.defined_K₀ -attribute [simp] PCA.defined_K₁ +attribute [simp] PCA.df_K₀ +attribute [simp] PCA.df_K₁ attribute [simp] PCA.eq_K -attribute [simp] PCA.defined_S₀ -attribute [simp] PCA.defined_S₁ -attribute [simp] PCA.defined_S₂ +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 defined_K₀ + default := K.get df_K₀ /-! `Expr Γ A` is the type of expressions built inductively from constants `K` and `S`, variables in `Γ` (the variable context), @@ -77,6 +75,7 @@ instance PCA.inhabited {A : Type*} [PCA A] : Inhabited A where 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`. -/ @@ -92,6 +91,7 @@ inductive Expr (Γ A : Type*) where /-- 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 @@ -100,27 +100,6 @@ namespace Expr variable {Γ : Type u} [DecidableEq Γ] variable {A : Type v} [PCA A] - /-- Does a variable occur in an expression? -/ - @[reducible] - def occurs (x : Γ) : Expr Γ A → Prop - | K => False - | S => False - | elm _ => False - | var y => y = x - | app e₁ e₂ => occurs x e₁ ∨ occurs x e₂ - - /-- Occurrence of a variable is decidable -/ - instance decide_occurs {x : Γ} (e : Expr Γ A) : Decidable (occurs x e) := - match e with - | K => .isFalse not_false - | S => .isFalse not_false - | elm _ => .isFalse not_false - | var y => decEq y x - | app e₁ e₂ => - let _ := @decide_occurs x e₁ - let _ := @decide_occurs x e₂ - inferInstance - /-- A valuation `η : Γ → A` assigning elements to variables, with the value of `x` overridden to be `a`. -/ @[reducible] @@ -158,7 +137,7 @@ namespace Expr | app e₁ e₂ => S ⬝ (abstr x e₁) ⬝ (abstr x e₂) /-- An abstraction is defined. -/ - lemma defined_abstr (x : Γ) (e : Expr Γ A) : defined (abstr x e) := by + lemma df_abstr (x : Γ) (e : Expr Γ A) : defined (abstr x e) := by intro η induction e case K => simp [eval] @@ -172,7 +151,7 @@ namespace Expr /-- `abstr e` behaves like abstraction in the extra variable. This is known as *combinatory completeness*. -/ - lemma eq_abstr (x : Γ) (e : Expr Γ A) (a : A) (η : Γ → A): + 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] @@ -185,13 +164,14 @@ namespace Expr case app e₁ e₂ ih₁ ih₂ => simp [abstr, eval] at ih₁ simp [abstr, eval] at ih₂ - simp [abstr, eval, defined_abstr x _ η, ih₁, 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 eq_abstr + _ = eval (override x (u.get hu) η) e := by apply eval_abstr /-- Compile an expression to a partial element, substituting the default value for any variables occurring in e. -/ diff --git a/PartialCombinatoryAlgebras/Programming.lean b/PartialCombinatoryAlgebras/Programming.lean index bc44cbf..acac552 100644 --- a/PartialCombinatoryAlgebras/Programming.lean +++ b/PartialCombinatoryAlgebras/Programming.lean @@ -9,26 +9,26 @@ namespace PCA def I : Part A := S ⬝ K ⬝ K @[simp] - theorem equal_I {u : Part A} : u ⇓ → I ⬝ u = u := by + theorem eq_I {u : Part A} : u ⇓ → I ⬝ u = u := by intro hu ; simp [I, hu] @[simp] - theorem defined_I (u : Part A) : u ⇓ → (I ⬝ u) ⇓ := by + theorem df_I (u : Part A) : u ⇓ → (I ⬝ u) ⇓ := by intro hu - rw [equal_I] <;> assumption + rw [eq_I] <;> assumption def pair : Part A := compile (abstr "x" (abstr "y" (abstr "z" (var "z" ⬝ var "x" ⬝ var "y")))) @[simp] - theorem defined_pair (u v : Part A): + theorem df_pair (u v : Part A): u ⇓ → v ⇓ → (pair ⬝ u ⬝ v) ⇓ := by intro hu hv simp [pair] rw [eval_abstr_app, eval_abstr_app] <;> try assumption - apply defined_abstr + apply df_abstr - theorem equal_pair (u v w : Part A) : + theorem eq_pair (u v w : Part A) : u ⇓ → v ⇓ → w ⇓ → pair ⬝ u ⬝ v ⬝ w = w ⬝ u ⬝ v := by intros hu hv hw simp [pair] @@ -39,7 +39,7 @@ namespace PCA def fst : Part A := compile (abstr "x" (var "x" ⬝ .K)) - theorem equal_fst (u : Part A): + theorem eq_fst (u : Part A): u ⇓ → fst ⬝ u = u ⬝ K := by intro hu simp [fst] @@ -51,7 +51,7 @@ namespace PCA def snd : Part A := compile ((abstr "x" (var "x" ⬝ (.K ⬝ (.S ⬝ .K ⬝ .K))))) - theorem equal_snd (u : Part A): + theorem eq_snd (u : Part A): u ⇓ → snd ⬝ u = u ⬝ (K ⬝ (S ⬝ K ⬝ K)) := by intro hu simp [snd] @@ -61,39 +61,39 @@ namespace PCA assumption @[simp] - def equal_fst_pair (u v : Part A) : u ⇓ → v ⇓ → fst ⬝ (pair ⬝ u ⬝ v) = u := by + def eq_fst_pair (u v : Part A) : u ⇓ → v ⇓ → fst ⬝ (pair ⬝ u ⬝ v) = u := by intro hu hv calc - _ = pair ⬝ u ⬝ v ⬝ K := by apply equal_fst ; apply defined_pair <;> assumption - _ = K ⬝ u ⬝ v := by apply equal_pair <;> simp [hu, hv] + _ = pair ⬝ u ⬝ v ⬝ K := by apply eq_fst ; apply df_pair <;> assumption + _ = K ⬝ u ⬝ v := by apply eq_pair <;> simp [hu, hv] _ = u := by apply eq_K <;> assumption @[simp] - def equal_snd_pair (u v : Part A) : u ⇓ → v ⇓ → snd ⬝ (pair ⬝ u ⬝ v) = v := by + def eq_snd_pair (u v : Part A) : u ⇓ → v ⇓ → snd ⬝ (pair ⬝ u ⬝ v) = v := by intro hu hv calc - _ = pair ⬝ u ⬝ v ⬝ (K ⬝ (S ⬝ K ⬝ K)) := by apply equal_snd ; apply defined_pair <;> assumption - _ = (K ⬝ (S ⬝ K ⬝ K)) ⬝ u ⬝ v := by apply equal_pair <;> simp [hu, hv] + _ = pair ⬝ u ⬝ v ⬝ (K ⬝ (S ⬝ K ⬝ K)) := by apply eq_snd ; apply df_pair <;> assumption + _ = (K ⬝ (S ⬝ K ⬝ K)) ⬝ u ⬝ v := by apply eq_pair <;> simp [hu, hv] _ = v := by rw [eq_K, eq_S, eq_K] <;> simp [hu, hv] def ite : Part A := sorry def fal : Part A := sorry def tru : Part A := sorry - theorem equal_ite_fal (u v : Part A) : u ⇓ → v ⇓ → ite ⬝ fal ⬝ u ⬝ v = v := by + theorem eq_ite_fal (u v : Part A) : u ⇓ → v ⇓ → ite ⬝ fal ⬝ u ⬝ v = v := by sorry - theorem equal_ite_tru (u v : Part A) : u ⇓ → v ⇓ → ite ⬝ tru ⬝ u ⬝ v = u := by + theorem eq_ite_tru (u v : Part A) : u ⇓ → v ⇓ → ite ⬝ tru ⬝ u ⬝ v = u := by sorry def numeral (n : ℕ) : Part A := sorry def succ : Part A := sorry def primrec : Part A := sorry - theorem equal_primrec_zero (n : ℕ) (u f : Part A) : u ⇓ → f ⇓ → primrec ⬝ u ⬝ f ⬝ numeral 0 = u := by + theorem eq_primrec_zero (n : ℕ) (u f : Part A) : u ⇓ → f ⇓ → primrec ⬝ u ⬝ f ⬝ numeral 0 = u := by sorry - theorem equal_primrec_succ (n : ℕ) (u f : Part A) : u ⇓ → f ⇓ → + theorem eq_primrec_succ (n : ℕ) (u f : Part A) : u ⇓ → f ⇓ → primrec ⬝ u ⬝ f ⬝ numeral n.succ = f ⬝ numeral n ⬝ (primrec ⬝ u ⬝ f ⬝ numeral n) := by sorry diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index a4c0aa8..9572a81 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -150,7 +150,7 @@ \section{Combinatory completeness} % \leanok \lean{Expr.abstr} - \uses{def:expression, def:extension} + \uses{def:expression, def:extension, def:PCA} % The \emph{abstraction} of an expression $e \in \Expr \Gamma A$ with respect to a variable $x \in \Gamma$ @@ -169,7 +169,7 @@ \section{Combinatory completeness} \label{prop:abstraction-defined} % \leanok - \lean{Expr.defined_abstr} + \lean{Expr.df_abstr} \uses{def:expression-defined, def:abstraction} % An abstraction $\abstr{x} e$ is defined. @@ -184,7 +184,7 @@ \section{Combinatory completeness} \label{prop:abstraction-equal} % \leanok - \lean{Expr.eq_abstr} + \lean{Expr.eval_abstr} \uses{def:expression, def:evaluation, def:abstraction} % Let $x \in \Gamma$ and $e \in \Expr {(\Gamma \cup \{x\})} A$. @@ -208,17 +208,17 @@ \section{Programming with PCAs} \begin{definition}[Identity] \label{def:combinator-I} - \lean{PCA.I, PCA.equal_I} + \lean{PCA.I, PCA.eq_I} \leanok - \uses{def:pca} + \uses{def:PCA} % There is the \emph{identity combinator} $\comb{I} \in A$ such that $I \, a = a$ for all $a \in A$. \end{definition} \begin{definition}[Pairing] \label{def:combinator-pairing} - \uses{def:pca} - \lean{PCA.pair, PCA.fst, PCA.snd, PCA.equal_fst_pair, PCA.equal_snd_pair} + \uses{def:PCA} + \lean{PCA.pair, PCA.fst, PCA.snd, PCA.eq_fst_pair, PCA.eq_snd_pair} \leanok % There are combinators $\comb{pair}, \comb{fst}, \comb{snd} \in A$ such that, for all $a, b \in A$, @@ -232,8 +232,8 @@ \section{Programming with PCAs} \begin{definition}[Booleans] \label{def:combinator-bool} - \lean{PCA.ite, PCA.fal, PCA.tru, PCA.equal_ite_fal, PCA.equal_ite_tru} - \uses{def:pca} + \lean{PCA.ite, PCA.fal, PCA.tru, PCA.eq_ite_fal, PCA.eq_ite_tru} + \uses{def:PCA} % There are combinators $\comb{ite} , \comb{fal}, \comb{tru} \in A$ such that, for all $a, b \in a$, % @@ -247,7 +247,7 @@ \section{Programming with PCAs} \begin{definition}[Numerals] \label{def:combinator-nat} \lean{PCA.numeral, PCA.succ, PCA.primrec} - \uses{def:pca} + \uses{def:PCA} % For each $n \in \NN$ there is $\overline{n} \in A$, as well as combinators $\comb{succ}, \comb{primrec} \in A$ such that, for all $n \in \NN$ and $a, f \in A$, @@ -264,7 +264,7 @@ \section{Programming with PCAs} \begin{definition}[General recursion] % \label{def:combinator-fix} - \uses{def:pca} + \uses{def:PCA} % There is a combinator $\comb{Y} \in A$ such that, for all $f, a \in A$, % diff --git a/lake-manifest.json b/lake-manifest.json index 95218ff..54e4324 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "44e2d2e643fd2618b01f9a0592d7dcbd3ffa22de", + "rev": "c933dd9b00271d869e22b802a015092d1e8e454a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7113817ab894ff56fb3a99f2efdff55f8da6df16", + "rev": "ab780650a6c8db2942d137b91ede7c94c47a4950", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 57a4710..6d9e70f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0-rc3