leanprover · WegmannDavid · May 20, 2026
@@ -89,6 +89,7 @@ public import Cslib.Foundations.Semantics.LTS.Union
 public import Cslib.Foundations.Syntax.Congruence
 public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasParallelSubstitution
 public import Cslib.Foundations.Syntax.HasSubstitution
 public import Cslib.Foundations.Syntax.HasWellFormed
 public import Cslib.Init
@@ -122,9 +123,10 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.ParallelSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.SubstEnv
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.HML.LogicalEquivalence

@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2026 David Wegmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Claude Opus 4.7 (via Claude Code), David Wegmann
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Parallel (simultaneous) substitution
+
+A typeclass for *parallel* substitution: replacing every variable of a term
+simultaneously, according to an assignment `σ : Var → T`, in a single pass.
+
+This is the operation needed by first-order unification — where a unifier is a
+simultaneous assignment and most-general-unifier reasoning relies on substitution
+composition — and it subsumes the finite multi-substitution used elsewhere (e.g.
+the strong-normalization proof), which is recovered by turning a finite
+`Context` into a total assignment.
+
+Unlike `Cslib.HasSubstitution` (single-variable replacement `t[x := t']`),
+parallel substitution is *not* derivable from iterated single substitutions:
+applying bindings one at a time is sequential, whereas here all variables are
+replaced at once.
+
+## Operation vs. laws
+
+Following the `Monad` / `LawfulMonad` pattern (and mirroring `Cslib.HasSubstitution`,
+which is a pure notation typeclass), the operation and its laws are split:
+
+* `HasParallelSubstitution` carries only `var` and `psubst`, plus notation.
+* `LawfulHasParallelSubstitution` carries the laws.
+
+A syntax with variables that satisfies the laws is exactly a (relative) monad:
+`var` is the unit (`return`) and `psubst` is the Kleisli extension (`bind`, with
+arguments flipped). In particular `psubst_comp` is associativity, which gives
+substitution *composition* `t⟦τ⟧ₚ⟦σ⟧ₚ = t⟦σ ∘ₚ τ⟧ₚ` — the algebra the MGU proof
+rests on. The laws hold unconditionally for capture-free representations
+(first-order terms, locally-nameless λ-terms); named representations, whose
+substitution is only well-behaved up to α-equivalence, are deliberately not
+expected to be lawful instances.
+-/
+
+public section
+
+namespace Cslib
+
+universe u v
+
+/-- Types `T` whose values are syntax over variables of type `Var`, equipped with
+*parallel* (simultaneous) substitution.
+
+`var` embeds a variable as a value; `psubst σ t` replaces every variable `x`
+occurring in `t` by `σ x`, all at once. This is a pure notation/operation class;
+the substitution laws live in `LawfulHasParallelSubstitution`. -/
+class HasParallelSubstitution (T : Type u) (Var : outParam (Type v)) where
+  /-- Embed a variable as a value. -/
+  var : Var → T
+  /-- Simultaneously replace every variable `x` in `t` by `σ x`. -/
+  psubst : (Var → T) → T → T
+
+namespace HasParallelSubstitution
+
+/-- Notation for parallel substitution, `t⟦σ⟧ₚ`: apply assignment `σ` to `t`. -/
+scoped notation:max t "⟦" σ "⟧ₚ" => HasParallelSubstitution.psubst σ t
+
+variable {T : Type u} {Var : Type v} [HasParallelSubstitution T Var]
+
+/-- Kleisli composition of assignments: `(σ ∘ₚ τ) x = (τ x)⟦σ⟧ₚ`, i.e. apply `τ`
+first, then `σ`. -/
+def comp (σ τ : Var → T) : Var → T := fun x => psubst σ (τ x)
+
+@[inherit_doc]
+scoped infixr:90 " ∘ₚ " => comp
+
+/-- `σ` is at least as general as `τ` (written `σ ≤ₚ τ`) when `τ` factors through
+`σ`: there is an assignment `ρ` with `τ = ρ ∘ₚ σ`, i.e. `τ x = (σ x)⟦ρ⟧ₚ` for
+every variable `x`. Equivalently, in the "apply to every term" formulation (see
+`moreGeneral_iff`), applying `τ` to any term equals applying `σ` and then `ρ`.
+
+This is the standard "more general than" relation underlying most-general
+unifiers. In the usual textbook notation, where the composite `στ` applies `σ`
+first and then `τ`, it reads `σ ≤ₚ τ ↔ ∃ ρ, τ = σρ`; we write the same thing
+with the (right-to-left) Kleisli composite `ρ ∘ₚ σ`. The relation is taken over
+total assignments — there is deliberately no restriction to a finite domain.
+
+This needs only the operation to *state*; that it is a preorder needs the laws. -/
+def MoreGeneral (σ τ : Var → T) : Prop := ∃ ρ : Var → T, τ = ρ ∘ₚ σ
+
+@[inherit_doc]
+scoped infix:50 " ≤ₚ " => MoreGeneral
+
+end HasParallelSubstitution
+
+open HasParallelSubstitution in
+/-- The laws of parallel substitution: a lawful instance is exactly a (relative)
+monad with `var` as unit and `psubst` as Kleisli extension. Stated as a `Prop`
+class over an existing `HasParallelSubstitution`, mirroring `LawfulMonad`. -/
+class LawfulHasParallelSubstitution (T : Type u) (Var : outParam (Type v))
+    [HasParallelSubstitution T Var] : Prop where
+  /-- Substituting into a single variable looks it up in the assignment.
+  (Monad left identity: `bind (pure x) σ = σ x`.) -/
+  psubst_var : ∀ (σ : Var → T) (x : Var), psubst σ (var x) = σ x
+  /-- The identity assignment `var` acts as the identity substitution.
+  (Monad right identity: `bind t pure = t`.) -/
+  psubst_id : ∀ (t : T), psubst var t = t
+  /-- Substitutions compose into a single pass.
+  (Monad associativity.) -/
+  psubst_comp : ∀ (σ τ : Var → T) (t : T),
+    psubst σ (psubst τ t) = psubst (fun x => psubst σ (τ x)) t
+
+namespace HasParallelSubstitution
+
+variable {T : Type u} {Var : Type v}
+  [HasParallelSubstitution T Var] [LawfulHasParallelSubstitution T Var]
+
+export LawfulHasParallelSubstitution (psubst_var psubst_id psubst_comp)
+
+/-- Substitution composition, stated via `comp`: substituting by `τ` and then `σ`
+is one substitution by `σ ∘ₚ τ`. -/
+theorem psubst_psubst (σ τ : Var → T) (t : T) :
+    psubst σ (psubst τ t) = psubst (σ ∘ₚ τ) t :=
+  psubst_comp σ τ t
+
+/-- Term-level characterization of generality, matching the "apply to every term"
+formulation used for unifiers: `σ ≤ₚ τ` iff there is `ρ` with
+`t⟦τ⟧ₚ = (t⟦σ⟧ₚ)⟦ρ⟧ₚ` for all terms `t`. The forward direction is `psubst_comp`;
+the backward direction instantiates at `t = var x` and uses `psubst_var`. -/
+theorem moreGeneral_iff {σ τ : Var → T} :
+    σ ≤ₚ τ ↔ ∃ ρ : Var → T, ∀ t : T, psubst τ t = psubst ρ (psubst σ t) := by
+  constructor
+  · rintro ⟨ρ, rfl⟩
+    exact ⟨ρ, fun t => (psubst_comp ρ σ t).symm⟩
+  · rintro ⟨ρ, h⟩
+    refine ⟨ρ, ?_⟩
+    funext x
+    simpa [comp, psubst_var] using h (var x)
+
+/-- Generality is reflexive: the identity assignment `var` witnesses `σ ≤ₚ σ`. -/
+@[refl]
+theorem MoreGeneral.refl (σ : Var → T) : σ ≤ₚ σ :=
+  ⟨var, by funext x; simp [comp, psubst_id]⟩
+
+/-- Generality is transitive: compose the two witnessing assignments. -/
+theorem MoreGeneral.trans {σ τ υ : Var → T} (h₁ : σ ≤ₚ τ) (h₂ : τ ≤ₚ υ) : σ ≤ₚ υ := by
+  obtain ⟨ρ₁, rfl⟩ := h₁
+  obtain ⟨ρ₂, rfl⟩ := h₂
+  refine ⟨ρ₂ ∘ₚ ρ₁, ?_⟩
+  funext x
+  simp only [comp]
+  exact psubst_comp ρ₂ ρ₁ (σ x)
+
+end HasParallelSubstitution
+
+end Cslib
@@ -12,7 +12,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.SubstEnv
 
 /-! Strong normalization (termination) for full beta-reduction of simply typed lambda calculus. -/
 
@@ -74,10 +74,12 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) :=
 /-- The `entails_context` predicate ensures that each variable in the context
     is mapped to a term in the corresponding semantic map. -/
 abbrev entails_context (E : Term.Env Var) (Γ : Context Var (Ty Base)) :=
-  ∀ {x τ}, ⟨x, τ⟩ ∈ Γ → (multiSubst E (fvar x)) ∈ semanticMap τ
+  ∀ {x τ}, ⟨x, τ⟩ ∈ Γ → (E.toAssignment x) ∈ semanticMap τ
 
 /-- The empty context is entailed by any environment. -/
-lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context [] Γ := by
+lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context Env.empty Γ := by
+  intro x τ _
+  rw [Env.empty_toAssignment]
   have := semanticMap_saturated (Var := Var) (Base := Base)
   grind
 
@@ -90,36 +92,45 @@ lemma entails_context_cons (E : Term.Env Var) (Γ : Context Var (Ty Base))
     (x : Var) (τ : Ty Base) (sub : Term Var)
     (h_fresh : x ∉ E.dom ∪ E.fv ∪ Γ.dom)
     (h_mem : sub ∈ semanticMap τ) :
-    entails_context E Γ → entails_context (⟨ x, sub ⟩ :: E) (⟨ x, τ ⟩ :: Γ) := by
-  grind [multiSubst_fvar_fresh, subst_fresh, multiSubst_preserves_not_fvar]
+    entails_context E Γ → entails_context (E.update x sub) (⟨ x, τ ⟩ :: Γ) := by
+  intro hE x' τ' hmem
+  rcases List.mem_cons.mp hmem with h | h
+  · simp only [Sigma.mk.injEq, heq_eq_eq] at h
+    obtain ⟨rfl, rfl⟩ := h
+    rw [Env.update_toAssignment, Function.update_self]
+    exact h_mem
+  · have hx' : x' ≠ x := by grind
+    rw [Env.update_toAssignment, Function.update_of_ne hx']
+    exact hE h
 
 /-- The `entails` predicate states that a term `t` is
     semantically valid with respect to a context `Γ` and a type `τ` -/
 abbrev entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
-    ∀ E, env_LC E → (entails_context E Γ) → (multiSubst E t) ∈ semanticMap τ
+    ∀ E, env_LC E → (entails_context E Γ) → (psubst E.toAssignment t) ∈ semanticMap τ
 
 /-- The `soundness` lemma states that if a term `t` has type `τ` in context `Γ`,
     then `t` is semantically valid with respect to `Γ` and `τ` -/
 lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) : entails Γ t τ := by
   induction derivation_t with
-  | var Γ xσ_mem_Γ => grind
+  | var Γ xσ_mem_Γ => grind [psubst_fvar]
   | @abs σ Γ t τ L HL IH =>
     intro E _ _ s
     have sat_semMap_σ := semanticMap_saturated (Var := Var) σ
     have sat_semMap_τ := semanticMap_saturated (Var := Var) τ
-    have := sat_semMap_τ.multiApp (multiSubst E t) s []
-    let := multiSubst E t
+    have := sat_semMap_τ.multiApp (psubst E.toAssignment t) s []
+    let := psubst E.toAssignment t
     have ⟨x, _⟩ := fresh_exists <| E.dom ∪ free_union [fv, Context.dom, Env.fv] Var
-    have := IH (x := x) (E := ⟨x,s⟩ :: E)
-    grind [multiSubst_abs, entails_context_cons, multiSubst_open_var]
-  | app => grind [multiSubst_app]
+    have := IH (x := x) (E := E.update x s)
+    grind [psubst_update, entails_context_cons, psubst_open_var, psubst_abs, env_LC_update]
+  | app => grind [psubst_app]
 
 /-- Using soundness and the fact that the empty context
     is entailed by any environment, we can conclude that
     a well-typed term is strongly normalizing. -/
 theorem strong_norm {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN FullBeta t := by
   apply (semanticMap_saturated τ).sn
-  apply (soundness der [] (by grind) entails_context_empty)
+  have h := soundness der Env.empty env_LC_empty entails_context_empty
+  rwa [Env.empty_toAssignment, psubst_fvar_id] at h
 
 end LambdaCalculus.LocallyNameless.Stlc