feat: add time bounds for ReductionSystems

Cslib/Foundations/Semantics/ReductionSystem/Basic.lean

@@ -29,6 +29,11 @@ structure ReductionSystem (Term : Type u) where
   /-- The reduction relation. -/
   Red : Term → Term → Prop
 
+structure TerminalReductionSystem (Term : Type u) extends ReductionSystem Term where
+  /-- The terminal terms. -/
+  Terminal : Term → Prop
+  /-- A terminal term cannot be further reduced. -/
+  terminal_not_reducible : ∀ t t', Terminal t → ¬ Red t t'
 
 section MultiStep
 
@@ -50,6 +55,215 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b)
 
 end MultiStep
 
+section Steps
+
+inductive ReductionSystem.reducesToInSteps
+    (rs : ReductionSystem Term) : Term → Term → ℕ → Prop
+  | refl (t : Term) : reducesToInSteps rs t t 0
+  | cons (t t' t'' : Term) (n : ℕ) (h₁ : rs.Red t t') (h₂ : reducesToInSteps rs t' t'' n) :
+      reducesToInSteps rs t t'' (n + 1)
+
+lemma ReductionSystem.reducesToInSteps.trans {rs : ReductionSystem Term} {a b c : Term} {n m : ℕ}
+    (h₁ : reducesToInSteps rs a b n) (h₂ : reducesToInSteps rs b c m) :
+    reducesToInSteps rs a c (n + m) := by
+  induction h₁ with
+  | refl _ =>
+    rw [Nat.zero_add]
+    exact h₂
+  | cons t t' t'' k h_red _ ih =>
+    rw [Nat.add_right_comm]
+    exact reducesToInSteps.cons t t' c (k + m) h_red (ih h₂)
+
+lemma ReductionSystem.reducesToInSteps.zero {rs : ReductionSystem Term} {a b : Term}
+    (h : reducesToInSteps rs a b 0) :
+    a = b := by
+  cases h
+  rfl
+
+@[simp]
+lemma ReductionSystem.reducesToInSteps.zero_iff {rs : ReductionSystem Term} {a b : Term} :
+    reducesToInSteps rs a b 0 ↔ a = b := by
+  constructor
+  · exact reducesToInSteps.zero
+  · intro rfl
+    exact reducesToInSteps.refl a
+
+lemma ReductionSystem.reducesToInSteps.succ {rs : ReductionSystem Term} {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b (n + 1)) :
+    ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by
+  cases h with
+  | cons _ t' _ _ h_red h_steps => exact ⟨t', h_red, h_steps⟩
+
+lemma ReductionSystem.reducesToInSteps.succ_iff {rs : ReductionSystem Term}
+    {a b : Term} {n : ℕ} :
+    reducesToInSteps rs a b (n + 1) ↔ ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by
+  constructor
+  · exact ReductionSystem.reducesToInSteps.succ
+  · rintro ⟨t', h_red, h_steps⟩
+    exact ReductionSystem.reducesToInSteps.cons a t' b n h_red h_steps
+
+lemma ReductionSystem.reducesToInSteps.succ' {rs : ReductionSystem Term}
+    {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b (n + 1)) :
+    ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by
+  induction n generalizing a b with
+  | zero =>
+    obtain ⟨t', h_red, h_steps⟩ := succ h
+    rw [zero_iff] at h_steps
+    subst h_steps
+    exact ⟨a, reducesToInSteps.refl a, h_red⟩
+  | succ k ih =>
+    obtain ⟨t', h_red, h_steps⟩ := succ h
+    obtain ⟨t'', h_steps', h_red'⟩ := ih h_steps
+    exact ⟨t'', reducesToInSteps.cons a t' t'' k h_red h_steps', h_red'⟩
+
+lemma ReductionSystem.reducesToInSteps.succ'_iff {rs : ReductionSystem Term}
+    {a b : Term} {n : ℕ} :
+    reducesToInSteps rs a b (n + 1) ↔ ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by
+  constructor
+  · exact succ'
+  · rintro ⟨t', h_steps, h_red⟩
+    have h_succ := trans h_steps (cons t' b b 0 h_red (refl b))
+    exact h_succ
+
+lemma ReductionSystem.reducesToInSteps.bounded_increase {rs : ReductionSystem Term}
+    {a b : Term} (h : Term → ℕ)
+    (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1)
+    (m : ℕ)
+    (hevals : rs.reducesToInSteps a b m) :
+    h b ≤ h a + m := by
+  induction hevals with
+  | refl _ => simp
+  | cons t t' t'' k h_red _ ih =>
+    have h_step' := h_step t t' h_red
+    omega
+
+/--
+If `g` is a homomorphism from `rs` to `rs'` (i.e., it preserves the reduction relation),
+then `reducesToInSteps` is preserved under `g`.
+-/
+lemma ReductionSystem.reducesToInSteps.map {Term Term' : Type*}
+    {rs : ReductionSystem Term} {rs' : ReductionSystem Term'}
+    (g : Term → Term') (hg : ∀ a b, rs.Red a b → rs'.Red (g a) (g b))
+    {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b n) :
+    reducesToInSteps rs' (g a) (g b) n := by
+  induction h with
+  | refl t => exact reducesToInSteps.refl (g t)
+  | cons t t' t'' m h_red h_steps ih =>
+    exact reducesToInSteps.cons (g t) (g t') (g t'') m (hg t t' h_red) ih
+
+/--
+`reducesToWithinSteps` is a variant of `reducesToInSteps` that allows for a loose bound.
+It states that a term `a` reduces to a term `b` in *at most* `n` steps.
+-/
+def ReductionSystem.reducesToWithinSteps (rs : ReductionSystem Term)
+    (a b : Term) (n : ℕ) : Prop :=
+  ∃ m ≤ n, reducesToInSteps rs a b m
+
+/-- Reflexivity of `reducesToWithinSteps` in 0 steps. -/
+lemma ReductionSystem.reducesToWithinSteps.refl {rs : ReductionSystem Term} (a : Term) :
+    reducesToWithinSteps rs a a 0 := by
+  use 0
+  exact ⟨Nat.le_refl 0, reducesToInSteps.refl a⟩
+
+/-- Transitivity of `reducesToWithinSteps` in the sum of the step bounds. -/
+@[trans]
+lemma ReductionSystem.reducesToWithinSteps.trans {rs : ReductionSystem Term}
+    {a b c : Term} {n₁ n₂ : ℕ}
+    (h₁ : reducesToWithinSteps rs a b n₁) (h₂ : reducesToWithinSteps rs b c n₂) :
+    reducesToWithinSteps rs a c (n₁ + n₂) := by
+  obtain ⟨m₁, hm₁, hevals₁⟩ := h₁
+  obtain ⟨m₂, hm₂, hevals₂⟩ := h₂
+  use m₁ + m₂
+  constructor
+  · omega
+  · exact reducesToInSteps.trans hevals₁ hevals₂
+
+/-- Monotonicity of `reducesToWithinSteps` in the step bound. -/
+lemma ReductionSystem.reducesToWithinSteps.mono_steps {rs : ReductionSystem Term}
+    {a b : Term} {n₁ n₂ : ℕ}
+    (h : reducesToWithinSteps rs a b n₁) (hn : n₁ ≤ n₂) :
+    reducesToWithinSteps rs a b n₂ := by
+  obtain ⟨m, hm, hevals⟩ := h
+  use m
+  constructor
+  · omega
+  · exact hevals
+
+/-- If `h : Term → ℕ` increases by at most 1 on each step of `rs`,
+then the value of `h` at the output is at most `h` at the input plus the step bound. -/
+lemma ReductionSystem.reducesToWithinSteps.bounded_increase {rs : ReductionSystem Term}
+    {a b : Term} (h : Term → ℕ)
+    (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1)
+    (n : ℕ)
+    (hevals : reducesToWithinSteps rs a b n) :
+    h b ≤ h a + n := by
+  obtain ⟨m, hm, hevals_m⟩ := hevals
+  have := reducesToInSteps.bounded_increase h h_step m hevals_m
+  omega
+
+/--
+If `g` is a homomorphism from `rs` to `rs'` (i.e., it preserves the reduction relation),
+then `reducesToWithinSteps` is preserved under `g`.
+-/
+lemma ReductionSystem.reducesToWithinSteps.map {Term Term' : Type*}
+    {rs : ReductionSystem Term} {rs' : ReductionSystem Term'}
+    (g : Term → Term') (hg : ∀ a b, rs.Red a b → rs'.Red (g a) (g b))
+    {a b : Term} {n : ℕ}
+    (h : reducesToWithinSteps rs a b n) :
+    reducesToWithinSteps rs' (g a) (g b) n := by
+  obtain ⟨m, hm, hevals⟩ := h
+  exact ⟨m, hm, reducesToInSteps.map g hg hevals⟩
+
+/-- A single reduction step gives `reducesToWithinSteps` with bound 1. -/
+lemma ReductionSystem.reducesToWithinSteps.single {rs : ReductionSystem Term}
+    {a b : Term} (h : rs.Red a b) :
+    reducesToWithinSteps rs a b 1 := by
+  use 1
+  constructor
+  · exact Nat.le_refl 1
+  · exact reducesToInSteps.cons a b b 0 h (reducesToInSteps.refl b)
+
+/-- `reducesToInSteps` implies `reducesToWithinSteps` with the same bound. -/
+lemma ReductionSystem.reducesToWithinSteps.of_reducesToInSteps {rs : ReductionSystem Term}
+    {a b : Term} {n : ℕ}
+    (h : reducesToInSteps rs a b n) :
+    reducesToWithinSteps rs a b n :=
+  ⟨n, Nat.le_refl n, h⟩
+
+/-- Zero steps means the terms are equal. -/
+lemma ReductionSystem.reducesToWithinSteps.zero {rs : ReductionSystem Term} {a b : Term}
+    (h : reducesToWithinSteps rs a b 0) :
+    a = b := by
+  obtain ⟨m, hm, hevals⟩ := h
+  have : m = 0 := Nat.le_zero.mp hm
+  subst this
+  exact reducesToInSteps.zero hevals
+
+@[simp]
+lemma ReductionSystem.reducesToWithinSteps.zero_iff {rs : ReductionSystem Term} {a b : Term} :
+    reducesToWithinSteps rs a b 0 ↔ a = b := by
+  constructor
+  · exact reducesToWithinSteps.zero
+  · intro h
+    subst h
+    exact reducesToWithinSteps.refl a
+
+end Steps
+
+/--
+Given a map σ → Option σ, we can construct a terminal reduction system on `σ` where:
+* a term is terminal if it maps to `none` under the given function,
+* and otherwise is reducible to its `some` value under the given function.
+-/
+def TerminalReductionSystem.Option {σ : Type*} (f : σ → Option σ) : TerminalReductionSystem σ where
+  Red := fun a b => f a = some b
+  Terminal := fun a => f a = none
+  terminal_not_reducible := by
+    intros t t' h_terminal h_red
+    simp [h_terminal] at h_red
+
 open Lean Elab Meta Command Term
 
 -- thank you to Kyle Miller for this: