Skip to content

feat(confluence): add relation-level reduction inclusions #719

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
JJYYY-JJY wants to merge 2 commits into
base: main
Choose a base branch
from
+31 −30
Open

feat(confluence): add relation-level reduction inclusions #719

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8917f04
feat(confluence): add relation-level reduction inclusions
JJYYY-JJY Jul 14, 2026
b5f19b0
refactor(confluence): namespace relation inclusions
JJYYY-JJY Jul 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 20 additions & 22 deletions Cslib/Languages/CombinatoryLogic/Confluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,45 +59,43 @@ inductive ParallelReduction : SKI → SKI → Prop
| par ⦃a a' b b' : SKI⦄ :
ParallelReduction a a' → ParallelReduction b b' → ParallelReduction (a ⬝ b) (a' ⬝ b')

/-- The inclusion `⭢ₚ ⊆ ↠` -/
theorem mRed_of_parallelReduction {a a' : SKI} (h : a ⭢ₚ a') : a ↠ a' := by
/-- The inclusion `(· ⭢ₚ ·) ≤ (· ↠ ·)`. -/
theorem ParallelReduction.le_reflTransGen_red :
(· ⭢ₚ ·) ≤ (· ↠ ·) := by
Comment thread
JJYYY-JJY marked this conversation as resolved.
intro a a' h
cases h
case refl => exact Relation.ReflTransGen.refl
case par a a' b b' ha hb =>
apply parallel_mRed
· exact mRed_of_parallelReduction ha
· exact mRed_of_parallelReduction hb
case red_I => exact Relation.ReflTransGen.single (red_I a')
case red_K b => exact Relation.ReflTransGen.single (red_K a' b)
case red_S a b c => exact Relation.ReflTransGen.single (red_S a b c)

/-- The inclusion `⭢ ⊆ ⭢ₚ` -/
theorem parallelReduction_of_red {a a' : SKI} (h : a ⭢ a') : a ⭢ₚ a' := by
· exact ha.le_reflTransGen_red
· exact hb.le_reflTransGen_red
case red_I => exact Relation.ReflTransGen.single (Red.red_I a')
case red_K b => exact Relation.ReflTransGen.single (Red.red_K a' b)
case red_S a b c => exact Relation.ReflTransGen.single (Red.red_S a b c)

/-- The inclusion `(· ⭢ ·) ≤ (· ⭢ₚ ·)`. -/
theorem Red.le_parallelReduction :
(· ⭢ ·) ≤ (· ⭢ₚ ·) := by
intro a a' h
cases h
case red_S => apply ParallelReduction.red_S
case red_K => apply ParallelReduction.red_K
case red_I => apply ParallelReduction.red_I
case red_head a a' b h =>
apply ParallelReduction.par
· exact parallelReduction_of_red h
· exact h.le_parallelReduction
· exact ParallelReduction.refl b
case red_tail a b b' h =>
apply ParallelReduction.par
· exact ParallelReduction.refl a
· exact parallelReduction_of_red h
· exact h.le_parallelReduction

/-- The inclusions of `mRed_of_parallelReduction` and
`parallelReduction_of_red` imply that `⭢` and `⭢ₚ` have the same reflexive-transitive
closure. -/
/-- The relations `⭢` and `⭢ₚ` have the same reflexive-transitive closure. -/
theorem reflTransGen_parallelReduction_mRed :
ReflTransGen ParallelReduction = ReflTransGen Red := by
ext a b
constructor
· apply reflTransGen_le_of_le
-- TODO: restate `parallelReduction_of_red` and others using `≤`?
exact @mRed_of_parallelReduction
· apply Relation.reflTransGen_le_of_le
exact fun a a' h => Relation.ReflTransGen.single (parallelReduction_of_red h)
apply le_antisymm
· exact reflTransGen_le_of_le ParallelReduction.le_reflTransGen_red
· exact ReflTransGen.mono Red.le_parallelReduction

/-!
Irreducibility for the (partially applied) primitive combinators.
Expand Down
19 changes: 11 additions & 8 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,8 +73,10 @@ lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
all_goals grind

omit [HasFresh Var] [DecidableEq Var] in
/-- A single β-reduction implies a single parallel reduction. -/
lemma step_to_para (step : M ⭢βᶠ N) : M ⭢ₚ N := by
/-- The inclusion `(· ⭢βᶠ ·) ≤ (· ⭢ₚ ·)`. -/
lemma FullBeta.le_parallel :
((· ⭢βᶠ ·) : Term Var → Term Var → Prop) ≤ (· ⭢ₚ ·) := by
Comment thread
JJYYY-JJY marked this conversation as resolved.
intro M N step
induction step with
| base h =>
cases h with | beta abs_lc _ =>
Expand All @@ -84,8 +86,10 @@ lemma step_to_para (step : M ⭢βᶠ N) : M ⭢ₚ N := by
| _ => grind

open FullBeta in
/-- A single parallel reduction implies a multiple β-reduction. -/
lemma para_to_redex (para : M ⭢ₚ N) : M ↠βᶠ N := by
/-- The inclusion `(· ⭢ₚ ·) ≤ (· ↠βᶠ ·)`. -/
lemma Parallel.le_reflTransGen_fullBeta :
((· ⭢ₚ ·) : Term Var → Term Var → Prop) ≤ (· ↠βᶠ ·) := by
intro M N para
induction para
case fvar => constructor
case app L L' R R' l_para m_para redex_l redex_m =>
Expand All @@ -106,10 +110,9 @@ lemma para_to_redex (para : M ⭢ₚ N) : M ↠βᶠ N := by
_ ⭢βᶠ m' ^ n' := by grind

/-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
theorem parachain_iff_redex : M ↠ₚ N ↔ M ↠βᶠ N := by
refine Iff.intro ?chain_redex ?redex_chain <;> intros h <;> induction h <;> try rfl
case redex_chain redex chain => exact ReflTransGen.tail chain (step_to_para redex)
case chain_redex para redex => exact ReflTransGen.trans redex (para_to_redex para)
theorem parachain_iff_redex : M ↠ₚ N ↔ M ↠βᶠ N :=

@chenson2018 chenson2018 Jul 16, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe for consistency this should now be stated as (· ↠ₚ ·) = (· ↠βᶠ ·) and given a better consistent name.

⟨reflTransGen_le_of_le Parallel.le_reflTransGen_fullBeta M N,
ReflTransGen.mono FullBeta.le_parallel M N⟩

/-- Parallel reduction respects substitution. -/
@[scoped grind .]
Expand Down
Loading