From e52d359181a521f1f57323a74cd1fde1098f8ca0 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 14:14:50 -0800 Subject: [PATCH 01/16] feat: add contents on step counting --- .../Semantics/ReductionSystem/Basic.lean | 212 ++++++++++++++++++ 1 file changed, 212 insertions(+) diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 5aad8a38..b1b8127c 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/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,213 @@ 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 _ => simp only [Nat.zero_add]; exact h₂ + | cons t t' t'' k h_red _ ih => + simp only [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 h; subst h; 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_one : reducesToInSteps rs t' b 1 := cons t' b b 0 h_red (refl b) + have := trans h_steps h_one + simp only [Nat.add_one] at this + exact this + +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: From 1d56bb29d581469a8df22de4566a93fe090838c2 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 14:43:18 -0800 Subject: [PATCH 02/16] clean up --- .../Semantics/ReductionSystem/Basic.lean | 30 ++++++++++--------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index b1b8127c..0aecd37b 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -67,9 +67,11 @@ lemma ReductionSystem.reducesToInSteps.trans {rs : ReductionSystem Term} {a b c (h₁ : reducesToInSteps rs a b n) (h₂ : reducesToInSteps rs b c m) : reducesToInSteps rs a c (n + m) := by induction h₁ with - | refl _ => simp only [Nat.zero_add]; exact h₂ + | refl _ => + rw [Nat.zero_add] + exact h₂ | cons t t' t'' k h_red _ ih => - simp only [Nat.add_right_comm] + 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} @@ -83,8 +85,8 @@ lemma ReductionSystem.reducesToInSteps.zero_iff {rs : ReductionSystem Term} {a b reducesToInSteps rs a b 0 ↔ a = b := by constructor · exact reducesToInSteps.zero - · intro h; subst h; exact reducesToInSteps.refl a - + · intro rfl + exact reducesToInSteps.refl a lemma ReductionSystem.reducesToInSteps.succ {rs : ReductionSystem Term} {a b : Term} {n : ℕ} (h : reducesToInSteps rs a b (n + 1)) : @@ -92,14 +94,16 @@ lemma ReductionSystem.reducesToInSteps.succ {rs : ReductionSystem Term} {a b : T 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 : ℕ} : +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 : ℕ} +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 @@ -113,19 +117,17 @@ lemma ReductionSystem.reducesToInSteps.succ' {rs : ReductionSystem Term} {a b : 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 : ℕ} : +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_one : reducesToInSteps rs t' b 1 := cons t' b b 0 h_red (refl b) - have := trans h_steps h_one - simp only [Nat.add_one] at this - exact this + 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 → ℕ) +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) : From 5ed7c3ca2639dbc6d4eae808467eaea7a57274bb Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Wed, 21 Jan 2026 17:05:09 -0800 Subject: [PATCH 03/16] rewrite and move to relation file --- Cslib/Foundations/Data/Relation.lean | 209 +++++++++++++++++- .../Semantics/ReductionSystem/Basic.lean | 197 ----------------- 2 files changed, 207 insertions(+), 199 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index c6193e0b..d4e1373a 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Fabrizio Montesi and Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi, Thomas Waring, Chris Henson +Author: Fabrizio Montesi, Thomas Waring, Chris Henson -/ module @@ -27,7 +27,7 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou ## References -* [*Term Rewriting and All That*][Baader1998] +* [*α Rewriting and All That*][Baader1998] -/ @@ -307,4 +307,209 @@ theorem reflTransGen_mono_closed (h₁ : Subrelation r₁ r₂) (h₂ : Subrelat ext exact ⟨ReflTransGen.mono @h₁, reflTransGen_closed @h₂⟩ +section Steps + +/-- +A relation `r` relates two elements of `α` in `n` steps +if there is a chain of `n` pairs `(t_i, t_{i+1})` such that `r t_i t_{i+1}` for each `i`, +starting from the first element and ending at the second. +-/ +inductive relatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop + | refl (t : α) : relatesInSteps r t t 0 + | cons (t t' t'' : α) (n : ℕ) (h₁ : r t t') (h₂ : relatesInSteps r t' t'' n) : + relatesInSteps r t t'' (n + 1) + +lemma relatesInSteps.trans {a b c : α} {n m : ℕ} + (h₁ : relatesInSteps r a b n) (h₂ : relatesInSteps r b c m) : + relatesInSteps r 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 relatesInSteps.cons t t' c (k + m) h_red (ih h₂) + +lemma relatesInSteps.zero {a b : α} + (h : relatesInSteps r a b 0) : + a = b := by + cases h + rfl + +@[simp] +lemma relatesInSteps.zero_iff {a b : α} : + relatesInSteps r a b 0 ↔ a = b := by + constructor + · exact relatesInSteps.zero + · intro rfl + exact relatesInSteps.refl a + +lemma relatesInSteps.succ {a b : α} {n : ℕ} + (h : relatesInSteps r a b (n + 1)) : + ∃ t', r a t' ∧ relatesInSteps r t' b n := by + cases h with + | cons _ t' _ _ h_red h_steps => exact ⟨t', h_red, h_steps⟩ + +lemma relatesInSteps.succ_iff + {a b : α} {n : ℕ} : + relatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ relatesInSteps r t' b n := by + constructor + · exact relatesInSteps.succ + · rintro ⟨t', h_red, h_steps⟩ + exact relatesInSteps.cons a t' b n h_red h_steps + +lemma relatesInSteps.succ' + {a b : α} {n : ℕ} + (h : relatesInSteps r a b (n + 1)) : + ∃ t', relatesInSteps r a t' n ∧ r 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, relatesInSteps.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'', relatesInSteps.cons a t' t'' k h_red h_steps', h_red'⟩ + +lemma relatesInSteps.succ'_iff + {a b : α} {n : ℕ} : + relatesInSteps r a b (n + 1) ↔ ∃ t', relatesInSteps r a t' n ∧ r 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 + +/-- +If `h : α → ℕ` increases by at most 1 on each step of `r`, +then the value of `h` at the output is at most `h` at the input plus the number of steps. +-/ +lemma relatesInSteps.apply_le_apply_add + {a b : α} (h : α → ℕ) + (h_step : ∀ a b, r a b → h b ≤ h a + 1) + (m : ℕ) + (hevals : relatesInSteps r 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 `r` to `r'` (i.e., it preserves the reduction relation), +then `relatesInSteps` is preserved under `g`. +-/ +lemma relatesInSteps.map {α α' : Type*} + {r : α → α → Prop} {r' : α' → α' → Prop} + (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) + {a b : α} {n : ℕ} + (h : relatesInSteps r a b n) : + relatesInSteps r' (g a) (g b) n := by + induction h with + | refl t => exact relatesInSteps.refl (g t) + | cons t t' t'' m h_red h_steps ih => + exact relatesInSteps.cons (g t) (g t') (g t'') m (hg t t' h_red) ih + +/-- +`relatesWithinSteps` is a variant of `relatesInSteps` that allows for a loose bound. +It states that `a` relates to `b` in *at most* `n` steps. +-/ +def relatesWithinSteps (r : α → α → Prop) + (a b : α) (n : ℕ) : Prop := + ∃ m ≤ n, relatesInSteps r a b m + +/-- Reflexivity of `relatesWithinSteps` in 0 steps. -/ +lemma relatesWithinSteps.refl (a : α) : + relatesWithinSteps r a a 0 := by + use 0 + exact ⟨Nat.le_refl 0, relatesInSteps.refl a⟩ + +/-- Transitivity of `relatesWithinSteps` in the sum of the step bounds. -/ +@[trans] +lemma relatesWithinSteps.trans + {a b c : α} {n₁ n₂ : ℕ} + (h₁ : relatesWithinSteps r a b n₁) (h₂ : relatesWithinSteps r b c n₂) : + relatesWithinSteps r a c (n₁ + n₂) := by + obtain ⟨m₁, hm₁, hevals₁⟩ := h₁ + obtain ⟨m₂, hm₂, hevals₂⟩ := h₂ + use m₁ + m₂ + constructor + · omega + · exact relatesInSteps.trans hevals₁ hevals₂ + +/-- Monotonicity of `relatesWithinSteps` in the step bound. -/ +lemma relatesWithinSteps.mono_steps + {a b : α} {n₁ n₂ : ℕ} + (h : relatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : + relatesWithinSteps r a b n₂ := by + obtain ⟨m, hm, hevals⟩ := h + use m + constructor + · omega + · exact hevals + +/-- If `h : α → ℕ` increases by at most 1 on each step of `r`, +then the value of `h` at the output is at most `h` at the input plus the step bound. -/ +lemma relatesWithinSteps.apply_le_apply_add + {a b : α} (h : α → ℕ) + (h_step : ∀ a b, r a b → h b ≤ h a + 1) + (n : ℕ) + (hevals : relatesWithinSteps r a b n) : + h b ≤ h a + n := by + obtain ⟨m, hm, hevals_m⟩ := hevals + have := relatesInSteps.apply_le_apply_add h h_step m hevals_m + omega + +/-- +If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), +then `relatesWithinSteps` is preserved under `g`. +-/ +lemma relatesWithinSteps.map {α α' : Type*} + {r : α → α → Prop} {r' : α' → α' → Prop} + (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) + {a b : α} {n : ℕ} + (h : relatesWithinSteps r a b n) : + relatesWithinSteps r' (g a) (g b) n := by + obtain ⟨m, hm, hevals⟩ := h + exact ⟨m, hm, relatesInSteps.map g hg hevals⟩ + +/-- A single reduction step gives `relatesWithinSteps` with bound 1. -/ +lemma relatesWithinSteps.single + {a b : α} (h : r a b) : + relatesWithinSteps r a b 1 := by + use 1 + constructor + · exact Nat.le_refl 1 + · exact relatesInSteps.cons a b b 0 h (relatesInSteps.refl b) + +/-- `relatesInSteps` implies `relatesWithinSteps` with the same bound. -/ +lemma relatesWithinSteps.of_relatesInSteps + {a b : α} {n : ℕ} + (h : relatesInSteps r a b n) : + relatesWithinSteps r a b n := + ⟨n, Nat.le_refl n, h⟩ + +/-- Zero steps means the `α`s are equal. -/ +lemma relatesWithinSteps.zero {a b : α} + (h : relatesWithinSteps r a b 0) : + a = b := by + obtain ⟨m, hm, hevals⟩ := h + have : m = 0 := Nat.le_zero.mp hm + subst this + exact relatesInSteps.zero hevals + +@[simp] +lemma relatesWithinSteps.zero_iff {a b : α} : + relatesWithinSteps r a b 0 ↔ a = b := by + constructor + · exact relatesWithinSteps.zero + · intro h + subst h + exact relatesWithinSteps.refl a + +end Steps + end Relation diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 0aecd37b..0f236af0 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -55,203 +55,6 @@ 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, From 83450fb7ac069e8e0070d934d4d03822d4dd77a0 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Wed, 21 Jan 2026 17:07:13 -0800 Subject: [PATCH 04/16] revert other file --- .../Semantics/ReductionSystem/Basic.lean | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 0f236af0..5aad8a38 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -29,11 +29,6 @@ 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 @@ -55,18 +50,6 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b) end MultiStep -/-- -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: From ce88a580f6fa82533a218d8536dab7135dc94cbc Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Wed, 21 Jan 2026 17:34:09 -0800 Subject: [PATCH 05/16] revert mistaken changes --- Cslib/Foundations/Data/Relation.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index d4e1373a..4301eaca 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Fabrizio Montesi and Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Fabrizio Montesi, Thomas Waring, Chris Henson +Authors: Fabrizio Montesi, Thomas Waring, Chris Henson -/ module @@ -27,7 +27,7 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou ## References -* [*α Rewriting and All That*][Baader1998] +* [*Term Rewriting and All That*][Baader1998] -/ From 32558eee3a61cef9b6bf4259432d1fa7d65ae804 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Wed, 21 Jan 2026 17:42:25 -0800 Subject: [PATCH 06/16] remove unneeded newlines in args --- Cslib/Foundations/Data/Relation.lean | 67 +++++++++------------------- 1 file changed, 21 insertions(+), 46 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 4301eaca..ea992e0f 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -330,37 +330,30 @@ lemma relatesInSteps.trans {a b c : α} {n m : ℕ} rw [Nat.add_right_comm] exact relatesInSteps.cons t t' c (k + m) h_red (ih h₂) -lemma relatesInSteps.zero {a b : α} - (h : relatesInSteps r a b 0) : - a = b := by +lemma relatesInSteps.zero {a b : α} (h : relatesInSteps r a b 0) : a = b := by cases h rfl @[simp] -lemma relatesInSteps.zero_iff {a b : α} : - relatesInSteps r a b 0 ↔ a = b := by +lemma relatesInSteps.zero_iff {a b : α} : relatesInSteps r a b 0 ↔ a = b := by constructor · exact relatesInSteps.zero · intro rfl exact relatesInSteps.refl a -lemma relatesInSteps.succ {a b : α} {n : ℕ} - (h : relatesInSteps r a b (n + 1)) : +lemma relatesInSteps.succ {a b : α} {n : ℕ} (h : relatesInSteps r a b (n + 1)) : ∃ t', r a t' ∧ relatesInSteps r t' b n := by cases h with | cons _ t' _ _ h_red h_steps => exact ⟨t', h_red, h_steps⟩ -lemma relatesInSteps.succ_iff - {a b : α} {n : ℕ} : +lemma relatesInSteps.succ_iff {a b : α} {n : ℕ} : relatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ relatesInSteps r t' b n := by constructor · exact relatesInSteps.succ · rintro ⟨t', h_red, h_steps⟩ exact relatesInSteps.cons a t' b n h_red h_steps -lemma relatesInSteps.succ' - {a b : α} {n : ℕ} - (h : relatesInSteps r a b (n + 1)) : +lemma relatesInSteps.succ' {a b : α} {n : ℕ} (h : relatesInSteps r a b (n + 1)) : ∃ t', relatesInSteps r a t' n ∧ r t' b := by induction n generalizing a b with | zero => @@ -373,8 +366,7 @@ lemma relatesInSteps.succ' obtain ⟨t'', h_steps', h_red'⟩ := ih h_steps exact ⟨t'', relatesInSteps.cons a t' t'' k h_red h_steps', h_red'⟩ -lemma relatesInSteps.succ'_iff - {a b : α} {n : ℕ} : +lemma relatesInSteps.succ'_iff {a b : α} {n : ℕ} : relatesInSteps r a b (n + 1) ↔ ∃ t', relatesInSteps r a t' n ∧ r t' b := by constructor · exact succ' @@ -386,11 +378,9 @@ lemma relatesInSteps.succ'_iff If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the number of steps. -/ -lemma relatesInSteps.apply_le_apply_add - {a b : α} (h : α → ℕ) +lemma relatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (m : ℕ) - (hevals : relatesInSteps r a b m) : + (m : ℕ) (hevals : relatesInSteps r a b m) : h b ≤ h a + m := by induction hevals with | refl _ => simp @@ -405,8 +395,7 @@ then `relatesInSteps` is preserved under `g`. lemma relatesInSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) - {a b : α} {n : ℕ} - (h : relatesInSteps r a b n) : + {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : relatesInSteps r' (g a) (g b) n := by induction h with | refl t => exact relatesInSteps.refl (g t) @@ -417,20 +406,17 @@ lemma relatesInSteps.map {α α' : Type*} `relatesWithinSteps` is a variant of `relatesInSteps` that allows for a loose bound. It states that `a` relates to `b` in *at most* `n` steps. -/ -def relatesWithinSteps (r : α → α → Prop) - (a b : α) (n : ℕ) : Prop := +def relatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := ∃ m ≤ n, relatesInSteps r a b m /-- Reflexivity of `relatesWithinSteps` in 0 steps. -/ -lemma relatesWithinSteps.refl (a : α) : - relatesWithinSteps r a a 0 := by +lemma relatesWithinSteps.refl (a : α) : relatesWithinSteps r a a 0 := by use 0 exact ⟨Nat.le_refl 0, relatesInSteps.refl a⟩ /-- Transitivity of `relatesWithinSteps` in the sum of the step bounds. -/ @[trans] -lemma relatesWithinSteps.trans - {a b c : α} {n₁ n₂ : ℕ} +lemma relatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} (h₁ : relatesWithinSteps r a b n₁) (h₂ : relatesWithinSteps r b c n₂) : relatesWithinSteps r a c (n₁ + n₂) := by obtain ⟨m₁, hm₁, hevals₁⟩ := h₁ @@ -441,8 +427,7 @@ lemma relatesWithinSteps.trans · exact relatesInSteps.trans hevals₁ hevals₂ /-- Monotonicity of `relatesWithinSteps` in the step bound. -/ -lemma relatesWithinSteps.mono_steps - {a b : α} {n₁ n₂ : ℕ} +lemma relatesWithinSteps.mono_steps {a b : α} {n₁ n₂ : ℕ} (h : relatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : relatesWithinSteps r a b n₂ := by obtain ⟨m, hm, hevals⟩ := h @@ -453,11 +438,9 @@ lemma relatesWithinSteps.mono_steps /-- If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the step bound. -/ -lemma relatesWithinSteps.apply_le_apply_add - {a b : α} (h : α → ℕ) +lemma relatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (n : ℕ) - (hevals : relatesWithinSteps r a b n) : + (n : ℕ) (hevals : relatesWithinSteps r a b n) : h b ≤ h a + n := by obtain ⟨m, hm, hevals_m⟩ := hevals have := relatesInSteps.apply_le_apply_add h h_step m hevals_m @@ -467,18 +450,15 @@ lemma relatesWithinSteps.apply_le_apply_add If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), then `relatesWithinSteps` is preserved under `g`. -/ -lemma relatesWithinSteps.map {α α' : Type*} - {r : α → α → Prop} {r' : α' → α' → Prop} +lemma relatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) - {a b : α} {n : ℕ} - (h : relatesWithinSteps r a b n) : + {a b : α} {n : ℕ} (h : relatesWithinSteps r a b n) : relatesWithinSteps r' (g a) (g b) n := by obtain ⟨m, hm, hevals⟩ := h exact ⟨m, hm, relatesInSteps.map g hg hevals⟩ /-- A single reduction step gives `relatesWithinSteps` with bound 1. -/ -lemma relatesWithinSteps.single - {a b : α} (h : r a b) : +lemma relatesWithinSteps.single {a b : α} (h : r a b) : relatesWithinSteps r a b 1 := by use 1 constructor @@ -486,24 +466,19 @@ lemma relatesWithinSteps.single · exact relatesInSteps.cons a b b 0 h (relatesInSteps.refl b) /-- `relatesInSteps` implies `relatesWithinSteps` with the same bound. -/ -lemma relatesWithinSteps.of_relatesInSteps - {a b : α} {n : ℕ} - (h : relatesInSteps r a b n) : +lemma relatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : relatesWithinSteps r a b n := ⟨n, Nat.le_refl n, h⟩ /-- Zero steps means the `α`s are equal. -/ -lemma relatesWithinSteps.zero {a b : α} - (h : relatesWithinSteps r a b 0) : - a = b := by +lemma relatesWithinSteps.zero {a b : α} (h : relatesWithinSteps r a b 0) : a = b := by obtain ⟨m, hm, hevals⟩ := h have : m = 0 := Nat.le_zero.mp hm subst this exact relatesInSteps.zero hevals @[simp] -lemma relatesWithinSteps.zero_iff {a b : α} : - relatesWithinSteps r a b 0 ↔ a = b := by +lemma relatesWithinSteps.zero_iff {a b : α} : relatesWithinSteps r a b 0 ↔ a = b := by constructor · exact relatesWithinSteps.zero · intro h From a3675bf0d5cd3a5823f9f156d4c66e5edd0a91d6 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Wed, 21 Jan 2026 19:15:25 -0800 Subject: [PATCH 07/16] better name choice --- Cslib/Foundations/Data/Relation.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index ea992e0f..6120d6aa 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -426,8 +426,7 @@ lemma relatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} · omega · exact relatesInSteps.trans hevals₁ hevals₂ -/-- Monotonicity of `relatesWithinSteps` in the step bound. -/ -lemma relatesWithinSteps.mono_steps {a b : α} {n₁ n₂ : ℕ} +lemma relatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} (h : relatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : relatesWithinSteps r a b n₂ := by obtain ⟨m, hm, hevals⟩ := h From 32a6b0c9df3b1ceb64b1c56edad2dd56077d8c42 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Wed, 21 Jan 2026 19:24:13 -0800 Subject: [PATCH 08/16] improve names and order --- Cslib/Foundations/Data/Relation.lean | 85 +++++++++++++--------------- 1 file changed, 39 insertions(+), 46 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 6120d6aa..05a4ce60 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -319,16 +319,9 @@ inductive relatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop | cons (t t' t'' : α) (n : ℕ) (h₁ : r t t') (h₂ : relatesInSteps r t' t'' n) : relatesInSteps r t t'' (n + 1) -lemma relatesInSteps.trans {a b c : α} {n m : ℕ} - (h₁ : relatesInSteps r a b n) (h₂ : relatesInSteps r b c m) : - relatesInSteps r 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 relatesInSteps.cons t t' c (k + m) h_red (ih h₂) +lemma relatesInSteps.single {a b : α} (h : r a b) : + relatesInSteps r a b 1 := by + exact relatesInSteps.cons a b b 0 h (relatesInSteps.refl b) lemma relatesInSteps.zero {a b : α} (h : relatesInSteps r a b 0) : a = b := by cases h @@ -341,6 +334,17 @@ lemma relatesInSteps.zero_iff {a b : α} : relatesInSteps r a b 0 ↔ a = b := b · intro rfl exact relatesInSteps.refl a +lemma relatesInSteps.trans {a b c : α} {n m : ℕ} + (h₁ : relatesInSteps r a b n) (h₂ : relatesInSteps r b c m) : + relatesInSteps r 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 relatesInSteps.cons t t' c (k + m) h_red (ih h₂) + lemma relatesInSteps.succ {a b : α} {n : ℕ} (h : relatesInSteps r a b (n + 1)) : ∃ t', r a t' ∧ relatesInSteps r t' b n := by cases h with @@ -409,10 +413,30 @@ It states that `a` relates to `b` in *at most* `n` steps. def relatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := ∃ m ≤ n, relatesInSteps r a b m -/-- Reflexivity of `relatesWithinSteps` in 0 steps. -/ -lemma relatesWithinSteps.refl (a : α) : relatesWithinSteps r a a 0 := by - use 0 - exact ⟨Nat.le_refl 0, relatesInSteps.refl a⟩ +/-- `relatesInSteps` implies `relatesWithinSteps` with the same bound. -/ +lemma relatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : + relatesWithinSteps r a b n := + ⟨n, Nat.le_refl n, h⟩ + +lemma relatesWithinSteps.refl (a : α) : relatesWithinSteps r a a 0 := + relatesWithinSteps.of_relatesInSteps (relatesInSteps.refl a) + +lemma relatesWithinSteps.single {a b : α} (h : r a b) : relatesWithinSteps r a b 1 := + relatesWithinSteps.of_relatesInSteps (relatesInSteps.single h) + +lemma relatesWithinSteps.zero {a b : α} (h : relatesWithinSteps r a b 0) : a = b := by + obtain ⟨m, hm, hevals⟩ := h + have : m = 0 := Nat.le_zero.mp hm + subst this + exact relatesInSteps.zero hevals + +@[simp] +lemma relatesWithinSteps.zero_iff {a b : α} : relatesWithinSteps r a b 0 ↔ a = b := by + constructor + · exact relatesWithinSteps.zero + · intro h + subst h + exact relatesWithinSteps.refl a /-- Transitivity of `relatesWithinSteps` in the sum of the step bounds. -/ @[trans] @@ -430,10 +454,7 @@ lemma relatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} (h : relatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : relatesWithinSteps r a b n₂ := by obtain ⟨m, hm, hevals⟩ := h - use m - constructor - · omega - · exact hevals + exact ⟨m, Nat.le_trans hm hn, hevals⟩ /-- If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the step bound. -/ @@ -456,34 +477,6 @@ lemma relatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' obtain ⟨m, hm, hevals⟩ := h exact ⟨m, hm, relatesInSteps.map g hg hevals⟩ -/-- A single reduction step gives `relatesWithinSteps` with bound 1. -/ -lemma relatesWithinSteps.single {a b : α} (h : r a b) : - relatesWithinSteps r a b 1 := by - use 1 - constructor - · exact Nat.le_refl 1 - · exact relatesInSteps.cons a b b 0 h (relatesInSteps.refl b) - -/-- `relatesInSteps` implies `relatesWithinSteps` with the same bound. -/ -lemma relatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : - relatesWithinSteps r a b n := - ⟨n, Nat.le_refl n, h⟩ - -/-- Zero steps means the `α`s are equal. -/ -lemma relatesWithinSteps.zero {a b : α} (h : relatesWithinSteps r a b 0) : a = b := by - obtain ⟨m, hm, hevals⟩ := h - have : m = 0 := Nat.le_zero.mp hm - subst this - exact relatesInSteps.zero hevals - -@[simp] -lemma relatesWithinSteps.zero_iff {a b : α} : relatesWithinSteps r a b 0 ↔ a = b := by - constructor - · exact relatesWithinSteps.zero - · intro h - subst h - exact relatesWithinSteps.refl a - end Steps end Relation From ec41f75d9f084cdee67e4889506b8f96f5ba5d62 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 17:39:27 -0800 Subject: [PATCH 09/16] rewrite in tail form --- Cslib/Foundations/Data/Relation.lean | 104 +++++++++++++++++---------- 1 file changed, 68 insertions(+), 36 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index f5d23ed9..a839ec61 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -341,19 +341,54 @@ theorem reflTransGen_compRel : ReflTransGen (CompRel r) = EqvGen r := by section Steps +variable {a b c : α} + /-- A relation `r` relates two elements of `α` in `n` steps if there is a chain of `n` pairs `(t_i, t_{i+1})` such that `r t_i t_{i+1}` for each `i`, starting from the first element and ending at the second. -/ inductive relatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop - | refl (t : α) : relatesInSteps r t t 0 - | cons (t t' t'' : α) (n : ℕ) (h₁ : r t t') (h₂ : relatesInSteps r t' t'' n) : + | refl (a : α) : relatesInSteps r a a 0 + | tail (t t' t'' : α) (n : ℕ) (h₁ : relatesInSteps r t t' n) (h₂ : r t' t'') : relatesInSteps r t t'' (n + 1) +theorem relatesInSteps.reflTransGen (h : relatesInSteps r a b n) : ReflTransGen r a b := by + induction h with + | refl => rfl + | tail _ _ _ _ h ih => exact .tail ih h + +theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, relatesInSteps r a b n := by + induction h with + | refl => exact ⟨0, .refl a⟩ + | tail _ _ ih => + obtain ⟨n, _⟩ := ih + exact ⟨n + 1, by grind [relatesInSteps]⟩ + lemma relatesInSteps.single {a b : α} (h : r a b) : relatesInSteps r a b 1 := by - exact relatesInSteps.cons a b b 0 h (relatesInSteps.refl b) + exact tail a a b 0 (refl a) h + +theorem relatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') + (h₂ : relatesInSteps r t' t'' n) : relatesInSteps r t t'' (n+1) := by + induction h₂ with + | refl => + exact single h₁ + | tail _ _ n _ hcd hac => + exact tail _ _ _ (n + 1) hac hcd + +@[elab_as_elim] +theorem relatesInSteps.head_induction_on {motive : ∀ (a : α) (n : ℕ), relatesInSteps r a b n → Prop} + {a : α} {n : ℕ} (h : relatesInSteps r a b n) (hrefl : motive b 0 (.refl b)) + (hhead : ∀ {a c n} (h' : r a c) (h : relatesInSteps r c b n), + motive c n h → motive a (n + 1) (h.head a c b n h')) : + motive a n h := by + induction h with + | refl => exact hrefl + | tail t' b' m hstep hrt'b' hstep_ih => + apply hstep_ih + · exact hhead hrt'b' _ hrefl + · exact fun h1 h2 ↦ hhead h1 (.tail _ t' b' _ h2 hrt'b') lemma relatesInSteps.zero {a b : α} (h : relatesInSteps r a b 0) : a = b := by cases h @@ -369,46 +404,43 @@ lemma relatesInSteps.zero_iff {a b : α} : relatesInSteps r a b 0 ↔ a = b := b lemma relatesInSteps.trans {a b c : α} {n m : ℕ} (h₁ : relatesInSteps r a b n) (h₂ : relatesInSteps r b c m) : relatesInSteps r 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 relatesInSteps.cons t t' c (k + m) h_red (ih h₂) + induction h₂ generalizing a n with + | refl => simp [h₁] + | tail t' t'' k hsteps hstep ih => + rw [← Nat.add_assoc] + exact .tail _ t' t'' (n + k) (ih h₁) hstep lemma relatesInSteps.succ {a b : α} {n : ℕ} (h : relatesInSteps r a b (n + 1)) : - ∃ t', r a t' ∧ relatesInSteps r t' b n := by + ∃ t', relatesInSteps r a t' n ∧ r t' b := by cases h with - | cons _ t' _ _ h_red h_steps => exact ⟨t', h_red, h_steps⟩ + | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩ lemma relatesInSteps.succ_iff {a b : α} {n : ℕ} : - relatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ relatesInSteps r t' b n := by + relatesInSteps r a b (n + 1) ↔ ∃ t', relatesInSteps r a t' n ∧ r t' b := by constructor · exact relatesInSteps.succ - · rintro ⟨t', h_red, h_steps⟩ - exact relatesInSteps.cons a t' b n h_red h_steps + · rintro ⟨t', h_steps, h_red⟩ + exact .tail _ t' b n h_steps h_red -lemma relatesInSteps.succ' {a b : α} {n : ℕ} (h : relatesInSteps r a b (n + 1)) : - ∃ t', relatesInSteps r a t' n ∧ r t' b := by - induction n generalizing a b with +lemma relatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, relatesInSteps r a b (n + 1) → + ∃ t', r a t' ∧ relatesInSteps r t' b n := by + intro n h + obtain ⟨t', hsteps, hstep⟩ := succ h + cases n with | zero => - obtain ⟨t', h_red, h_steps⟩ := succ h - rw [zero_iff] at h_steps - subst h_steps - exact ⟨a, relatesInSteps.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'', relatesInSteps.cons a t' t'' k h_red h_steps', h_red'⟩ + rw [zero_iff] at hsteps + subst hsteps + exact ⟨b, hstep, .refl _⟩ + | succ k' => + obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps + exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩ lemma relatesInSteps.succ'_iff {a b : α} {n : ℕ} : - relatesInSteps r a b (n + 1) ↔ ∃ t', relatesInSteps r a t' n ∧ r t' b := by + relatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ relatesInSteps r t' b n := 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 + · rintro ⟨t', h_red, h_steps⟩ + exact h_steps.head a t' b n h_red /-- If `h : α → ℕ` increases by at most 1 on each step of `r`, @@ -419,9 +451,9 @@ lemma relatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) (m : ℕ) (hevals : relatesInSteps r 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 + | refl => simp + | tail t' t'' k _ hstep ih => + have h_step' := h_step t' t'' hstep omega /-- @@ -434,9 +466,9 @@ lemma relatesInSteps.map {α α' : Type*} {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : relatesInSteps r' (g a) (g b) n := by induction h with - | refl t => exact relatesInSteps.refl (g t) - | cons t t' t'' m h_red h_steps ih => - exact relatesInSteps.cons (g t) (g t') (g t'') m (hg t t' h_red) ih + | refl => exact relatesInSteps.refl (g _) + | tail t' t'' m _ hstep ih => + exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep) /-- `relatesWithinSteps` is a variant of `relatesInSteps` that allows for a loose bound. From 500bf6d40980605bccb59c1700085342c593168f Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 17:40:17 -0800 Subject: [PATCH 10/16] capitalize --- Cslib/Foundations/Data/Relation.lean | 94 ++++++++++++++-------------- 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index a839ec61..6396da69 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -348,29 +348,29 @@ A relation `r` relates two elements of `α` in `n` steps if there is a chain of `n` pairs `(t_i, t_{i+1})` such that `r t_i t_{i+1}` for each `i`, starting from the first element and ending at the second. -/ -inductive relatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop - | refl (a : α) : relatesInSteps r a a 0 - | tail (t t' t'' : α) (n : ℕ) (h₁ : relatesInSteps r t t' n) (h₂ : r t' t'') : - relatesInSteps r t t'' (n + 1) +inductive RelatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop + | refl (a : α) : RelatesInSteps r a a 0 + | tail (t t' t'' : α) (n : ℕ) (h₁ : RelatesInSteps r t t' n) (h₂ : r t' t'') : + RelatesInSteps r t t'' (n + 1) -theorem relatesInSteps.reflTransGen (h : relatesInSteps r a b n) : ReflTransGen r a b := by +theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen r a b := by induction h with | refl => rfl | tail _ _ _ _ h ih => exact .tail ih h -theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, relatesInSteps r a b n := by +theorem ReflTransGen.RelatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by induction h with | refl => exact ⟨0, .refl a⟩ | tail _ _ ih => obtain ⟨n, _⟩ := ih - exact ⟨n + 1, by grind [relatesInSteps]⟩ + exact ⟨n + 1, by grind [RelatesInSteps]⟩ -lemma relatesInSteps.single {a b : α} (h : r a b) : - relatesInSteps r a b 1 := by +lemma RelatesInSteps.single {a b : α} (h : r a b) : + RelatesInSteps r a b 1 := by exact tail a a b 0 (refl a) h -theorem relatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') - (h₂ : relatesInSteps r t' t'' n) : relatesInSteps r t t'' (n+1) := by +theorem RelatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') + (h₂ : RelatesInSteps r t' t'' n) : RelatesInSteps r t t'' (n+1) := by induction h₂ with | refl => exact single h₁ @@ -378,9 +378,9 @@ theorem relatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') exact tail _ _ _ (n + 1) hac hcd @[elab_as_elim] -theorem relatesInSteps.head_induction_on {motive : ∀ (a : α) (n : ℕ), relatesInSteps r a b n → Prop} - {a : α} {n : ℕ} (h : relatesInSteps r a b n) (hrefl : motive b 0 (.refl b)) - (hhead : ∀ {a c n} (h' : r a c) (h : relatesInSteps r c b n), +theorem RelatesInSteps.head_induction_on {motive : ∀ (a : α) (n : ℕ), RelatesInSteps r a b n → Prop} + {a : α} {n : ℕ} (h : RelatesInSteps r a b n) (hrefl : motive b 0 (.refl b)) + (hhead : ∀ {a c n} (h' : r a c) (h : RelatesInSteps r c b n), motive c n h → motive a (n + 1) (h.head a c b n h')) : motive a n h := by induction h with @@ -390,40 +390,40 @@ theorem relatesInSteps.head_induction_on {motive : ∀ (a : α) (n : ℕ), relat · exact hhead hrt'b' _ hrefl · exact fun h1 h2 ↦ hhead h1 (.tail _ t' b' _ h2 hrt'b') -lemma relatesInSteps.zero {a b : α} (h : relatesInSteps r a b 0) : a = b := by +lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by cases h rfl @[simp] -lemma relatesInSteps.zero_iff {a b : α} : relatesInSteps r a b 0 ↔ a = b := by +lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by constructor - · exact relatesInSteps.zero + · exact RelatesInSteps.zero · intro rfl - exact relatesInSteps.refl a + exact RelatesInSteps.refl a -lemma relatesInSteps.trans {a b c : α} {n m : ℕ} - (h₁ : relatesInSteps r a b n) (h₂ : relatesInSteps r b c m) : - relatesInSteps r a c (n + m) := by +lemma RelatesInSteps.trans {a b c : α} {n m : ℕ} + (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) : + RelatesInSteps r a c (n + m) := by induction h₂ generalizing a n with | refl => simp [h₁] | tail t' t'' k hsteps hstep ih => rw [← Nat.add_assoc] exact .tail _ t' t'' (n + k) (ih h₁) hstep -lemma relatesInSteps.succ {a b : α} {n : ℕ} (h : relatesInSteps r a b (n + 1)) : - ∃ t', relatesInSteps r a t' n ∧ r t' b := by +lemma RelatesInSteps.succ {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) : + ∃ t', RelatesInSteps r a t' n ∧ r t' b := by cases h with | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩ -lemma relatesInSteps.succ_iff {a b : α} {n : ℕ} : - relatesInSteps r a b (n + 1) ↔ ∃ t', relatesInSteps r a t' n ∧ r t' b := by +lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} : + RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by constructor - · exact relatesInSteps.succ + · exact RelatesInSteps.succ · rintro ⟨t', h_steps, h_red⟩ exact .tail _ t' b n h_steps h_red -lemma relatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, relatesInSteps r a b (n + 1) → - ∃ t', r a t' ∧ relatesInSteps r t' b n := by +lemma RelatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, RelatesInSteps r a b (n + 1) → + ∃ t', r a t' ∧ RelatesInSteps r t' b n := by intro n h obtain ⟨t', hsteps, hstep⟩ := succ h cases n with @@ -435,8 +435,8 @@ lemma relatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, relatesInSteps r a b (n + obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩ -lemma relatesInSteps.succ'_iff {a b : α} {n : ℕ} : - relatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ relatesInSteps r t' b n := by +lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} : + RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by constructor · exact succ' · rintro ⟨t', h_red, h_steps⟩ @@ -446,9 +446,9 @@ lemma relatesInSteps.succ'_iff {a b : α} {n : ℕ} : If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the number of steps. -/ -lemma relatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) +lemma RelatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (m : ℕ) (hevals : relatesInSteps r a b m) : + (m : ℕ) (hevals : RelatesInSteps r a b m) : h b ≤ h a + m := by induction hevals with | refl => simp @@ -458,41 +458,41 @@ lemma relatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) /-- If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), -then `relatesInSteps` is preserved under `g`. +then `RelatesInSteps` is preserved under `g`. -/ -lemma relatesInSteps.map {α α' : Type*} +lemma RelatesInSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) - {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : - relatesInSteps r' (g a) (g b) n := by + {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : + RelatesInSteps r' (g a) (g b) n := by induction h with - | refl => exact relatesInSteps.refl (g _) + | refl => exact RelatesInSteps.refl (g _) | tail t' t'' m _ hstep ih => exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep) /-- -`relatesWithinSteps` is a variant of `relatesInSteps` that allows for a loose bound. +`relatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound. It states that `a` relates to `b` in *at most* `n` steps. -/ def relatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := - ∃ m ≤ n, relatesInSteps r a b m + ∃ m ≤ n, RelatesInSteps r a b m -/-- `relatesInSteps` implies `relatesWithinSteps` with the same bound. -/ -lemma relatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : relatesInSteps r a b n) : +/-- `RelatesInSteps` implies `relatesWithinSteps` with the same bound. -/ +lemma relatesWithinSteps.of_RelatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : relatesWithinSteps r a b n := ⟨n, Nat.le_refl n, h⟩ lemma relatesWithinSteps.refl (a : α) : relatesWithinSteps r a a 0 := - relatesWithinSteps.of_relatesInSteps (relatesInSteps.refl a) + relatesWithinSteps.of_RelatesInSteps (RelatesInSteps.refl a) lemma relatesWithinSteps.single {a b : α} (h : r a b) : relatesWithinSteps r a b 1 := - relatesWithinSteps.of_relatesInSteps (relatesInSteps.single h) + relatesWithinSteps.of_RelatesInSteps (RelatesInSteps.single h) lemma relatesWithinSteps.zero {a b : α} (h : relatesWithinSteps r a b 0) : a = b := by obtain ⟨m, hm, hevals⟩ := h have : m = 0 := Nat.le_zero.mp hm subst this - exact relatesInSteps.zero hevals + exact RelatesInSteps.zero hevals @[simp] lemma relatesWithinSteps.zero_iff {a b : α} : relatesWithinSteps r a b 0 ↔ a = b := by @@ -512,7 +512,7 @@ lemma relatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} use m₁ + m₂ constructor · omega - · exact relatesInSteps.trans hevals₁ hevals₂ + · exact RelatesInSteps.trans hevals₁ hevals₂ lemma relatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} (h : relatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : @@ -527,7 +527,7 @@ lemma relatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) (n : ℕ) (hevals : relatesWithinSteps r a b n) : h b ≤ h a + n := by obtain ⟨m, hm, hevals_m⟩ := hevals - have := relatesInSteps.apply_le_apply_add h h_step m hevals_m + have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m omega /-- @@ -539,7 +539,7 @@ lemma relatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' {a b : α} {n : ℕ} (h : relatesWithinSteps r a b n) : relatesWithinSteps r' (g a) (g b) n := by obtain ⟨m, hm, hevals⟩ := h - exact ⟨m, hm, relatesInSteps.map g hg hevals⟩ + exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩ end Steps From 547af2a65719dfb581ec734822194150ebde37a6 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 17:41:45 -0800 Subject: [PATCH 11/16] further capitalization fix, and line sizing --- Cslib/Foundations/Data/Relation.lean | 57 ++++++++++++++-------------- 1 file changed, 28 insertions(+), 29 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 6396da69..39835a7a 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -365,9 +365,8 @@ theorem ReflTransGen.RelatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInS obtain ⟨n, _⟩ := ih exact ⟨n + 1, by grind [RelatesInSteps]⟩ -lemma RelatesInSteps.single {a b : α} (h : r a b) : - RelatesInSteps r a b 1 := by - exact tail a a b 0 (refl a) h +lemma RelatesInSteps.single {a b : α} (h : r a b) : RelatesInSteps r a b 1 := + tail a a b 0 (refl a) h theorem RelatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') (h₂ : RelatesInSteps r t' t'' n) : RelatesInSteps r t t'' (n+1) := by @@ -471,42 +470,42 @@ lemma RelatesInSteps.map {α α' : Type*} exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep) /-- -`relatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound. +`RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound. It states that `a` relates to `b` in *at most* `n` steps. -/ -def relatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := +def RelatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := ∃ m ≤ n, RelatesInSteps r a b m -/-- `RelatesInSteps` implies `relatesWithinSteps` with the same bound. -/ -lemma relatesWithinSteps.of_RelatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : - relatesWithinSteps r a b n := +/-- `RelatesInSteps` implies `RelatesWithinSteps` with the same bound. -/ +lemma RelatesWithinSteps.of_RelatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : + RelatesWithinSteps r a b n := ⟨n, Nat.le_refl n, h⟩ -lemma relatesWithinSteps.refl (a : α) : relatesWithinSteps r a a 0 := - relatesWithinSteps.of_RelatesInSteps (RelatesInSteps.refl a) +lemma RelatesWithinSteps.refl (a : α) : RelatesWithinSteps r a a 0 := + RelatesWithinSteps.of_RelatesInSteps (RelatesInSteps.refl a) -lemma relatesWithinSteps.single {a b : α} (h : r a b) : relatesWithinSteps r a b 1 := - relatesWithinSteps.of_RelatesInSteps (RelatesInSteps.single h) +lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a b 1 := + RelatesWithinSteps.of_RelatesInSteps (RelatesInSteps.single h) -lemma relatesWithinSteps.zero {a b : α} (h : relatesWithinSteps r a b 0) : a = b := by +lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by obtain ⟨m, hm, hevals⟩ := h have : m = 0 := Nat.le_zero.mp hm subst this exact RelatesInSteps.zero hevals @[simp] -lemma relatesWithinSteps.zero_iff {a b : α} : relatesWithinSteps r a b 0 ↔ a = b := by +lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by constructor - · exact relatesWithinSteps.zero + · exact RelatesWithinSteps.zero · intro h subst h - exact relatesWithinSteps.refl a + exact RelatesWithinSteps.refl a -/-- Transitivity of `relatesWithinSteps` in the sum of the step bounds. -/ +/-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/ @[trans] -lemma relatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} - (h₁ : relatesWithinSteps r a b n₁) (h₂ : relatesWithinSteps r b c n₂) : - relatesWithinSteps r a c (n₁ + n₂) := by +lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} + (h₁ : RelatesWithinSteps r a b n₁) (h₂ : RelatesWithinSteps r b c n₂) : + RelatesWithinSteps r a c (n₁ + n₂) := by obtain ⟨m₁, hm₁, hevals₁⟩ := h₁ obtain ⟨m₂, hm₂, hevals₂⟩ := h₂ use m₁ + m₂ @@ -514,17 +513,17 @@ lemma relatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} · omega · exact RelatesInSteps.trans hevals₁ hevals₂ -lemma relatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} - (h : relatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : - relatesWithinSteps r a b n₂ := by +lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} + (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : + RelatesWithinSteps r a b n₂ := by obtain ⟨m, hm, hevals⟩ := h exact ⟨m, Nat.le_trans hm hn, hevals⟩ /-- If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the step bound. -/ -lemma relatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) +lemma RelatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (n : ℕ) (hevals : relatesWithinSteps r a b n) : + (n : ℕ) (hevals : RelatesWithinSteps r a b n) : h b ≤ h a + n := by obtain ⟨m, hm, hevals_m⟩ := hevals have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m @@ -532,12 +531,12 @@ lemma relatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) /-- If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), -then `relatesWithinSteps` is preserved under `g`. +then `RelatesWithinSteps` is preserved under `g`. -/ -lemma relatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} +lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) - {a b : α} {n : ℕ} (h : relatesWithinSteps r a b n) : - relatesWithinSteps r' (g a) (g b) n := by + {a b : α} {n : ℕ} (h : RelatesWithinSteps r a b n) : + RelatesWithinSteps r' (g a) (g b) n := by obtain ⟨m, hm, hevals⟩ := h exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩ From e38abd27b80d0fae105cda9ff462c86395b595fc Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 17:42:38 -0800 Subject: [PATCH 12/16] omega -> lia --- Cslib/Foundations/Data/Relation.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 39835a7a..3b82d707 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -453,7 +453,7 @@ lemma RelatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) | refl => simp | tail t' t'' k _ hstep ih => have h_step' := h_step t' t'' hstep - omega + lia /-- If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), @@ -510,7 +510,7 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} obtain ⟨m₂, hm₂, hevals₂⟩ := h₂ use m₁ + m₂ constructor - · omega + · lia · exact RelatesInSteps.trans hevals₁ hevals₂ lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} @@ -527,7 +527,7 @@ lemma RelatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) h b ≤ h a + n := by obtain ⟨m, hm, hevals_m⟩ := hevals have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m - omega + lia /-- If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), From ad7204422d51036bfd6b20b347e46cdb49c59f23 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 17:46:57 -0800 Subject: [PATCH 13/16] I think its lower camel snake case after the namespace. --- Cslib/Foundations/Data/Relation.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 3b82d707..4f65711b 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -477,15 +477,15 @@ def RelatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := ∃ m ≤ n, RelatesInSteps r a b m /-- `RelatesInSteps` implies `RelatesWithinSteps` with the same bound. -/ -lemma RelatesWithinSteps.of_RelatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : +lemma RelatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : RelatesWithinSteps r a b n := ⟨n, Nat.le_refl n, h⟩ lemma RelatesWithinSteps.refl (a : α) : RelatesWithinSteps r a a 0 := - RelatesWithinSteps.of_RelatesInSteps (RelatesInSteps.refl a) + RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.refl a) lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a b 1 := - RelatesWithinSteps.of_RelatesInSteps (RelatesInSteps.single h) + RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.single h) lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by obtain ⟨m, hm, hevals⟩ := h From ad997daba2a84975a733fd7ef2399a54f2876f05 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 17:53:39 -0800 Subject: [PATCH 14/16] fix other casing --- Cslib/Foundations/Data/Relation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 4f65711b..959c0712 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -358,7 +358,7 @@ theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen | refl => rfl | tail _ _ _ _ h ih => exact .tail ih h -theorem ReflTransGen.RelatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by +theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by induction h with | refl => exact ⟨0, .refl a⟩ | tail _ _ ih => From 3d0ba3365b75fb62b7fc5d76b01b60cfab9dd7b9 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 18:08:48 -0800 Subject: [PATCH 15/16] move to new file --- Cslib/Foundations/Data/RelatesInSteps.lean | 222 +++++++++++++++++++++ Cslib/Foundations/Data/Relation.lean | 203 ------------------- 2 files changed, 222 insertions(+), 203 deletions(-) create mode 100644 Cslib/Foundations/Data/RelatesInSteps.lean diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean new file mode 100644 index 00000000..07c66d0f --- /dev/null +++ b/Cslib/Foundations/Data/RelatesInSteps.lean @@ -0,0 +1,222 @@ +/- +Copyright (c) 2025 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ + +module + +public import Cslib.Init +public import Mathlib.Logic.Relation + +@[expose] public section + +variable {α : Type*} {r : α → α → Prop} {a b c : α} + +/-! # Relations Across Steps + +This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`). +These are inductively defines propositions that communicate whether a relation forms a +chain of length `n` (or at most `n`) between two elements. +-/ + +namespace Relation + +/-- +A relation `r` relates two elements of `α` in `n` steps +if there is a chain of `n` pairs `(t_i, t_{i+1})` such that `r t_i t_{i+1}` for each `i`, +starting from the first element and ending at the second. +-/ +inductive RelatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop + | refl (a : α) : RelatesInSteps r a a 0 + | tail (t t' t'' : α) (n : ℕ) (h₁ : RelatesInSteps r t t' n) (h₂ : r t' t'') : + RelatesInSteps r t t'' (n + 1) + +theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen r a b := by + induction h with + | refl => rfl + | tail _ _ _ _ h ih => exact .tail ih h + +theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by + induction h with + | refl => exact ⟨0, .refl a⟩ + | tail _ _ ih => + obtain ⟨n, _⟩ := ih + exact ⟨n + 1, by grind [RelatesInSteps]⟩ + +lemma RelatesInSteps.single {a b : α} (h : r a b) : RelatesInSteps r a b 1 := + tail a a b 0 (refl a) h + +theorem RelatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') + (h₂ : RelatesInSteps r t' t'' n) : RelatesInSteps r t t'' (n+1) := by + induction h₂ with + | refl => + exact single h₁ + | tail _ _ n _ hcd hac => + exact tail _ _ _ (n + 1) hac hcd + +@[elab_as_elim] +theorem RelatesInSteps.head_induction_on {motive : ∀ (a : α) (n : ℕ), RelatesInSteps r a b n → Prop} + {a : α} {n : ℕ} (h : RelatesInSteps r a b n) (hrefl : motive b 0 (.refl b)) + (hhead : ∀ {a c n} (h' : r a c) (h : RelatesInSteps r c b n), + motive c n h → motive a (n + 1) (h.head a c b n h')) : + motive a n h := by + induction h with + | refl => exact hrefl + | tail t' b' m hstep hrt'b' hstep_ih => + apply hstep_ih + · exact hhead hrt'b' _ hrefl + · exact fun h1 h2 ↦ hhead h1 (.tail _ t' b' _ h2 hrt'b') + +lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by + cases h + rfl + +@[simp] +lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by + constructor + · exact RelatesInSteps.zero + · intro rfl + exact RelatesInSteps.refl a + +lemma RelatesInSteps.trans {a b c : α} {n m : ℕ} + (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) : + RelatesInSteps r a c (n + m) := by + induction h₂ generalizing a n with + | refl => simp [h₁] + | tail t' t'' k hsteps hstep ih => + rw [← Nat.add_assoc] + exact .tail _ t' t'' (n + k) (ih h₁) hstep + +lemma RelatesInSteps.succ {n : ℕ} (h : RelatesInSteps r a b (n + 1)) : + ∃ t', RelatesInSteps r a t' n ∧ r t' b := by + cases h with + | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩ + +lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} : + RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by + constructor + · exact RelatesInSteps.succ + · rintro ⟨t', h_steps, h_red⟩ + exact .tail _ t' b n h_steps h_red + +lemma RelatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, RelatesInSteps r a b (n + 1) → + ∃ t', r a t' ∧ RelatesInSteps r t' b n := by + intro n h + obtain ⟨t', hsteps, hstep⟩ := succ h + cases n with + | zero => + rw [zero_iff] at hsteps + subst hsteps + exact ⟨b, hstep, .refl _⟩ + | succ k' => + obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps + exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩ + +lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} : + RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by + constructor + · exact succ' + · rintro ⟨t', h_red, h_steps⟩ + exact h_steps.head a t' b n h_red + +/-- +If `h : α → ℕ` increases by at most 1 on each step of `r`, +then the value of `h` at the output is at most `h` at the input plus the number of steps. +-/ +lemma RelatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) + (h_step : ∀ a b, r a b → h b ≤ h a + 1) + (m : ℕ) (hevals : RelatesInSteps r a b m) : + h b ≤ h a + m := by + induction hevals with + | refl => simp + | tail t' t'' k _ hstep ih => + have h_step' := h_step t' t'' hstep + lia + +/-- +If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), +then `RelatesInSteps` is preserved under `g`. +-/ +lemma RelatesInSteps.map {α α' : Type*} + {r : α → α → Prop} {r' : α' → α' → Prop} + (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) + {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : + RelatesInSteps r' (g a) (g b) n := by + induction h with + | refl => exact RelatesInSteps.refl (g _) + | tail t' t'' m _ hstep ih => + exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep) + +/-- +`RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound. +It states that `a` relates to `b` in *at most* `n` steps. +-/ +def RelatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := + ∃ m ≤ n, RelatesInSteps r a b m + +/-- `RelatesInSteps` implies `RelatesWithinSteps` with the same bound. -/ +lemma RelatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : + RelatesWithinSteps r a b n := + ⟨n, Nat.le_refl n, h⟩ + +lemma RelatesWithinSteps.refl (a : α) : RelatesWithinSteps r a a 0 := + RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.refl a) + +lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a b 1 := + RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.single h) + +lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by + obtain ⟨m, hm, hevals⟩ := h + have : m = 0 := Nat.le_zero.mp hm + subst this + exact RelatesInSteps.zero hevals + +@[simp] +lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by + constructor + · exact RelatesWithinSteps.zero + · intro h + subst h + exact RelatesWithinSteps.refl a + +/-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/ +@[trans] +lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} + (h₁ : RelatesWithinSteps r a b n₁) (h₂ : RelatesWithinSteps r b c n₂) : + RelatesWithinSteps r a c (n₁ + n₂) := by + obtain ⟨m₁, hm₁, hevals₁⟩ := h₁ + obtain ⟨m₂, hm₂, hevals₂⟩ := h₂ + use m₁ + m₂ + constructor + · lia + · exact RelatesInSteps.trans hevals₁ hevals₂ + +lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} + (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : + RelatesWithinSteps r a b n₂ := by + obtain ⟨m, hm, hevals⟩ := h + exact ⟨m, Nat.le_trans hm hn, hevals⟩ + +/-- If `h : α → ℕ` increases by at most 1 on each step of `r`, +then the value of `h` at the output is at most `h` at the input plus the step bound. -/ +lemma RelatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) + (h_step : ∀ a b, r a b → h b ≤ h a + 1) + (n : ℕ) (hevals : RelatesWithinSteps r a b n) : + h b ≤ h a + n := by + obtain ⟨m, hm, hevals_m⟩ := hevals + have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m + lia + +/-- +If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), +then `RelatesWithinSteps` is preserved under `g`. +-/ +lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} + (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) + {a b : α} {n : ℕ} (h : RelatesWithinSteps r a b n) : + RelatesWithinSteps r' (g a) (g b) n := by + obtain ⟨m, hm, hevals⟩ := h + exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩ + +end Relation diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 959c0712..2084c729 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -339,207 +339,4 @@ theorem reflTransGen_compRel : ReflTransGen (CompRel r) = EqvGen r := by exact reflTransGen_swap.mp ih | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ -section Steps - -variable {a b c : α} - -/-- -A relation `r` relates two elements of `α` in `n` steps -if there is a chain of `n` pairs `(t_i, t_{i+1})` such that `r t_i t_{i+1}` for each `i`, -starting from the first element and ending at the second. --/ -inductive RelatesInSteps (r : α → α → Prop) : α → α → ℕ → Prop - | refl (a : α) : RelatesInSteps r a a 0 - | tail (t t' t'' : α) (n : ℕ) (h₁ : RelatesInSteps r t t' n) (h₂ : r t' t'') : - RelatesInSteps r t t'' (n + 1) - -theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen r a b := by - induction h with - | refl => rfl - | tail _ _ _ _ h ih => exact .tail ih h - -theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by - induction h with - | refl => exact ⟨0, .refl a⟩ - | tail _ _ ih => - obtain ⟨n, _⟩ := ih - exact ⟨n + 1, by grind [RelatesInSteps]⟩ - -lemma RelatesInSteps.single {a b : α} (h : r a b) : RelatesInSteps r a b 1 := - tail a a b 0 (refl a) h - -theorem RelatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') - (h₂ : RelatesInSteps r t' t'' n) : RelatesInSteps r t t'' (n+1) := by - induction h₂ with - | refl => - exact single h₁ - | tail _ _ n _ hcd hac => - exact tail _ _ _ (n + 1) hac hcd - -@[elab_as_elim] -theorem RelatesInSteps.head_induction_on {motive : ∀ (a : α) (n : ℕ), RelatesInSteps r a b n → Prop} - {a : α} {n : ℕ} (h : RelatesInSteps r a b n) (hrefl : motive b 0 (.refl b)) - (hhead : ∀ {a c n} (h' : r a c) (h : RelatesInSteps r c b n), - motive c n h → motive a (n + 1) (h.head a c b n h')) : - motive a n h := by - induction h with - | refl => exact hrefl - | tail t' b' m hstep hrt'b' hstep_ih => - apply hstep_ih - · exact hhead hrt'b' _ hrefl - · exact fun h1 h2 ↦ hhead h1 (.tail _ t' b' _ h2 hrt'b') - -lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by - cases h - rfl - -@[simp] -lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by - constructor - · exact RelatesInSteps.zero - · intro rfl - exact RelatesInSteps.refl a - -lemma RelatesInSteps.trans {a b c : α} {n m : ℕ} - (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) : - RelatesInSteps r a c (n + m) := by - induction h₂ generalizing a n with - | refl => simp [h₁] - | tail t' t'' k hsteps hstep ih => - rw [← Nat.add_assoc] - exact .tail _ t' t'' (n + k) (ih h₁) hstep - -lemma RelatesInSteps.succ {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) : - ∃ t', RelatesInSteps r a t' n ∧ r t' b := by - cases h with - | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩ - -lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} : - RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by - constructor - · exact RelatesInSteps.succ - · rintro ⟨t', h_steps, h_red⟩ - exact .tail _ t' b n h_steps h_red - -lemma RelatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, RelatesInSteps r a b (n + 1) → - ∃ t', r a t' ∧ RelatesInSteps r t' b n := by - intro n h - obtain ⟨t', hsteps, hstep⟩ := succ h - cases n with - | zero => - rw [zero_iff] at hsteps - subst hsteps - exact ⟨b, hstep, .refl _⟩ - | succ k' => - obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps - exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩ - -lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} : - RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by - constructor - · exact succ' - · rintro ⟨t', h_red, h_steps⟩ - exact h_steps.head a t' b n h_red - -/-- -If `h : α → ℕ` increases by at most 1 on each step of `r`, -then the value of `h` at the output is at most `h` at the input plus the number of steps. --/ -lemma RelatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) - (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (m : ℕ) (hevals : RelatesInSteps r a b m) : - h b ≤ h a + m := by - induction hevals with - | refl => simp - | tail t' t'' k _ hstep ih => - have h_step' := h_step t' t'' hstep - lia - -/-- -If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), -then `RelatesInSteps` is preserved under `g`. --/ -lemma RelatesInSteps.map {α α' : Type*} - {r : α → α → Prop} {r' : α' → α' → Prop} - (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) - {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : - RelatesInSteps r' (g a) (g b) n := by - induction h with - | refl => exact RelatesInSteps.refl (g _) - | tail t' t'' m _ hstep ih => - exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep) - -/-- -`RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound. -It states that `a` relates to `b` in *at most* `n` steps. --/ -def RelatesWithinSteps (r : α → α → Prop) (a b : α) (n : ℕ) : Prop := - ∃ m ≤ n, RelatesInSteps r a b m - -/-- `RelatesInSteps` implies `RelatesWithinSteps` with the same bound. -/ -lemma RelatesWithinSteps.of_relatesInSteps {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : - RelatesWithinSteps r a b n := - ⟨n, Nat.le_refl n, h⟩ - -lemma RelatesWithinSteps.refl (a : α) : RelatesWithinSteps r a a 0 := - RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.refl a) - -lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a b 1 := - RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.single h) - -lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by - obtain ⟨m, hm, hevals⟩ := h - have : m = 0 := Nat.le_zero.mp hm - subst this - exact RelatesInSteps.zero hevals - -@[simp] -lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by - constructor - · exact RelatesWithinSteps.zero - · intro h - subst h - exact RelatesWithinSteps.refl a - -/-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/ -@[trans] -lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ} - (h₁ : RelatesWithinSteps r a b n₁) (h₂ : RelatesWithinSteps r b c n₂) : - RelatesWithinSteps r a c (n₁ + n₂) := by - obtain ⟨m₁, hm₁, hevals₁⟩ := h₁ - obtain ⟨m₂, hm₂, hevals₂⟩ := h₂ - use m₁ + m₂ - constructor - · lia - · exact RelatesInSteps.trans hevals₁ hevals₂ - -lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} - (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : - RelatesWithinSteps r a b n₂ := by - obtain ⟨m, hm, hevals⟩ := h - exact ⟨m, Nat.le_trans hm hn, hevals⟩ - -/-- If `h : α → ℕ` increases by at most 1 on each step of `r`, -then the value of `h` at the output is at most `h` at the input plus the step bound. -/ -lemma RelatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) - (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (n : ℕ) (hevals : RelatesWithinSteps r a b n) : - h b ≤ h a + n := by - obtain ⟨m, hm, hevals_m⟩ := hevals - have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m - lia - -/-- -If `g` is a homomorphism from `r` to `r'` (i.e., it preserves the reduction relation), -then `RelatesWithinSteps` is preserved under `g`. --/ -lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α' → α' → Prop} - (g : α → α') (hg : ∀ a b, r a b → r' (g a) (g b)) - {a b : α} {n : ℕ} (h : RelatesWithinSteps r a b n) : - RelatesWithinSteps r' (g a) (g b) n := by - obtain ⟨m, hm, hevals⟩ := h - exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩ - -end Steps - end Relation From 5704312ec95b569fa6d7af6b8be84c6b66bc4562 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Thu, 22 Jan 2026 18:20:52 -0800 Subject: [PATCH 16/16] lake exe mk_all --module --- Cslib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib.lean b/Cslib.lean index 8c6984eb..2be39bd8 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -36,6 +36,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten public import Cslib.Foundations.Data.OmegaSequence.InfOcc public import Cslib.Foundations.Data.OmegaSequence.Init public import Cslib.Foundations.Data.OmegaSequence.Temporal +public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Relation public import Cslib.Foundations.Lint.Basic public import Cslib.Foundations.Semantics.FLTS.Basic