Cleanup names, remove unusued strictness assumption.

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. -/

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

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$,
   %

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,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.14.0-rc3