From e8ec0dd4698e2914db834e153333b711dadbcf01 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Jul 2026 11:13:55 +0100 Subject: [PATCH 1/4] refactor: add new `syntax` but FAILS --- src/Algebra/Properties/KleeneAlgebra.agda | 7 +++++++ src/Relation/Binary/Reasoning/PartialOrder.agda | 9 +++++++++ 2 files changed, 16 insertions(+) diff --git a/src/Algebra/Properties/KleeneAlgebra.agda b/src/Algebra/Properties/KleeneAlgebra.agda index 9acf3c26ce..eddbe0ef77 100644 --- a/src/Algebra/Properties/KleeneAlgebra.agda +++ b/src/Algebra/Properties/KleeneAlgebra.agda @@ -252,6 +252,13 @@ x⋆≈1+x⋆x x = ≤-antisym (⋆-elimʳ (x≤x+y _ _) $ begin x ⋆ * x ≤⟨ y≤x+y _ _ ⟩ 1# + x ⋆ * x ∎) $ starExpansiveˡ _ +{- FAILS: parser falls over + begin-equality + x ⋆ ≈⟨ {!!} ⟨⟩ ? ⟩ + {!!} ≈⟨ {!!} ⟩ + 1# + x ⋆ * x ∎ +-} + -- special cases for 0# and 1# 0⋆≤1 : 0# ⋆ ≤ 1# diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda index 6b79f09b23..4bda4cc031 100644 --- a/src/Relation/Binary/Reasoning/PartialOrder.agda +++ b/src/Relation/Binary/Reasoning/PartialOrder.agda @@ -61,3 +61,12 @@ open import Relation.Binary.Reasoning.Base.Triple (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈) (Strict.≤-<-trans trans antisym ≤-respˡ-≈) public + +antisym-step-≈-⟩ : ∀ x {y z} → y IsRelatedTo z → y ≤ x → x ≤ y → x IsRelatedTo z +antisym-step-≈-⟩ x yRz y≤x x≤y = step-≈-⟩ x yRz (antisym x≤y y≤x) + +antisym-step-≈-⟨ : ∀ x {y z} → y IsRelatedTo z → x ≤ y → y ≤ x → x IsRelatedTo z +antisym-step-≈-⟨ x yRz x≤y y≤x = step-≈-⟩ x yRz (antisym x≤y y≤x) + +syntax antisym-step-≈-⟩ x yRz y≤x x≤y = x ≈⟨ y≤x ⟨⟩ x≤y ⟩ yRz +syntax antisym-step-≈-⟨ x yRz y≤x x≤y = x ≈⟨ x≤y ⟩⟨ y≤x ⟩ yRz From 14b9bdb7f53e38d5eb9e2cc4c0794157b9cbe401 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Jul 2026 09:12:47 +0100 Subject: [PATCH 2/4] [ add ] `syntax` for `antisym` equality reasoning in `Relation.Binary.Reasoning.PartialOrder` --- CHANGELOG.md | 6 ++++++ src/Algebra/Properties/KleeneAlgebra.agda | 20 +++++++++---------- .../Binary/Reasoning/PartialOrder.agda | 13 ++++-------- 3 files changed, 19 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 03df3230cc..f14f96d60a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -443,3 +443,9 @@ Additions to existing modules StarRightDestructive : ∀ (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _ StarDestructive : ∀ (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _ ``` + +* In `Relation.Binary.Reasoning.PartialOrder`: + ```agda + antisym-syntax = antisym + syntax antisym-syntax x≤y y≤x = x≤y ⟨⟩ y≤x + ``` diff --git a/src/Algebra/Properties/KleeneAlgebra.agda b/src/Algebra/Properties/KleeneAlgebra.agda index eddbe0ef77..9628c32cef 100644 --- a/src/Algebra/Properties/KleeneAlgebra.agda +++ b/src/Algebra/Properties/KleeneAlgebra.agda @@ -246,18 +246,16 @@ x⋆≈1+xx⋆ x = ≤-antisym (⋆-elimˡ (x≤x+y _ _) $ begin 1# + x * x ⋆ ∎) $ starExpansiveʳ _ x⋆≈1+x⋆x : ∀ x → x ⋆ ≈ 1# + x ⋆ * x -x⋆≈1+x⋆x x = ≤-antisym (⋆-elimʳ (x≤x+y _ _) $ begin - (1# + x ⋆ * x) * x ≤⟨ *-monoʳ _ $ +-monoˡ _ $ x⋆x≤x⋆ _ ⟩ - (1# + x ⋆) * x ≈⟨ *-congʳ (1+x⋆≈x⋆ _) ⟩ - x ⋆ * x ≤⟨ y≤x+y _ _ ⟩ - 1# + x ⋆ * x ∎) $ starExpansiveˡ _ - -{- FAILS: parser falls over - begin-equality - x ⋆ ≈⟨ {!!} ⟨⟩ ? ⟩ - {!!} ≈⟨ {!!} ⟩ +x⋆≈1+x⋆x x = begin-equality + x ⋆ ≈⟨ ⋆-elimʳ (x≤x+y _ _) lemma ⟨⟩ starExpansiveˡ _ ⟩ 1# + x ⋆ * x ∎ --} + where + lemma : (1# + x ⋆ * x) * x ≤ 1# + x ⋆ * x + lemma = begin + (1# + x ⋆ * x) * x ≤⟨ *-monoʳ _ $ +-monoˡ _ $ x⋆x≤x⋆ _ ⟩ + (1# + x ⋆) * x ≈⟨ *-congʳ (1+x⋆≈x⋆ _) ⟩ + x ⋆ * x ≤⟨ y≤x+y _ _ ⟩ + 1# + x ⋆ * x ∎ -- special cases for 0# and 1# diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda index 4bda4cc031..5b491f4dd5 100644 --- a/src/Relation/Binary/Reasoning/PartialOrder.agda +++ b/src/Relation/Binary/Reasoning/PartialOrder.agda @@ -40,6 +40,7 @@ {-# OPTIONS --without-K --safe #-} open import Relation.Binary.Bundles using (Poset) +--open import Relation.Binary.Structures using (IsPartialOrder) module Relation.Binary.Reasoning.PartialOrder {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where @@ -49,6 +50,9 @@ open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as Strict using (_<_) +antisym-syntax = antisym +syntax antisym-syntax x≤y y≤x = x≤y ⟨⟩ y≤x + ------------------------------------------------------------------------ -- Re-export contents of base module @@ -61,12 +65,3 @@ open import Relation.Binary.Reasoning.Base.Triple (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈) (Strict.≤-<-trans trans antisym ≤-respˡ-≈) public - -antisym-step-≈-⟩ : ∀ x {y z} → y IsRelatedTo z → y ≤ x → x ≤ y → x IsRelatedTo z -antisym-step-≈-⟩ x yRz y≤x x≤y = step-≈-⟩ x yRz (antisym x≤y y≤x) - -antisym-step-≈-⟨ : ∀ x {y z} → y IsRelatedTo z → x ≤ y → y ≤ x → x IsRelatedTo z -antisym-step-≈-⟨ x yRz x≤y y≤x = step-≈-⟩ x yRz (antisym x≤y y≤x) - -syntax antisym-step-≈-⟩ x yRz y≤x x≤y = x ≈⟨ y≤x ⟨⟩ x≤y ⟩ yRz -syntax antisym-step-≈-⟨ x yRz y≤x x≤y = x ≈⟨ x≤y ⟩⟨ y≤x ⟩ yRz From b2f5c90b6c5b86b108faaf57a57497589ad2366c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Jul 2026 11:29:56 +0100 Subject: [PATCH 3/4] refactor: use new syntax, for illustrative comparison --- src/Algebra/Properties/KleeneAlgebra.agda | 36 +++++++++++++---------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/src/Algebra/Properties/KleeneAlgebra.agda b/src/Algebra/Properties/KleeneAlgebra.agda index 9628c32cef..fec009908b 100644 --- a/src/Algebra/Properties/KleeneAlgebra.agda +++ b/src/Algebra/Properties/KleeneAlgebra.agda @@ -236,24 +236,29 @@ x≤x⋆ x = begin ⋆-*-elimʳ = starDestructiveʳ _ _ _ ∘ x≤z∧y≤z⇒[x+y]≤z ≤-refl 1+x⋆≈x⋆ : ∀ x → 1# + x ⋆ ≈ x ⋆ -1+x⋆≈x⋆ x = ≤-antisym (x≤z∧y≤z⇒[x+y]≤z 1≤[ _ ]⋆ ≤-refl) (y≤x+y _ _) +1+x⋆≈x⋆ x = x≤z∧y≤z⇒[x+y]≤z 1≤[ _ ]⋆ ≤-refl ⟨⟩ y≤x+y _ _ x⋆≈1+xx⋆ : ∀ x → x ⋆ ≈ 1# + x * x ⋆ -x⋆≈1+xx⋆ x = ≤-antisym (⋆-elimˡ (x≤x+y _ _) $ begin - x * (1# + x * x ⋆) ≤⟨ *-monoˡ _ $ +-monoˡ _ $ xx⋆≤x⋆ _ ⟩ - x * (1# + x ⋆) ≈⟨ *-congˡ (1+x⋆≈x⋆ _) ⟩ - x * x ⋆ ≤⟨ y≤x+y _ _ ⟩ - 1# + x * x ⋆ ∎) $ starExpansiveʳ _ +x⋆≈1+xx⋆ x = begin-equality + x ⋆ ≈⟨ ⋆-elimˡ (x≤x+y _ _) lemma ⟨⟩ starExpansiveʳ _ ⟩ + 1# + x * x ⋆ ∎ + where + lemma : x * (1# + x * x ⋆) ≤ 1# + x * x ⋆ + lemma = begin + x * (1# + x * x ⋆) ≤⟨ *-monoˡ _ $ +-monoˡ _ $ xx⋆≤x⋆ _ ⟩ + x * (1# + x ⋆) ≈⟨ *-congˡ (1+x⋆≈x⋆ _) ⟩ + x * x ⋆ ≤⟨ y≤x+y _ _ ⟩ + 1# + x * x ⋆ ∎ x⋆≈1+x⋆x : ∀ x → x ⋆ ≈ 1# + x ⋆ * x -x⋆≈1+x⋆x x = begin-equality - x ⋆ ≈⟨ ⋆-elimʳ (x≤x+y _ _) lemma ⟨⟩ starExpansiveˡ _ ⟩ +x⋆≈1+x⋆x x = begin-equality + x ⋆ ≈⟨ ⋆-elimʳ (x≤x+y _ _) lemma ⟨⟩ starExpansiveˡ _ ⟩ 1# + x ⋆ * x ∎ where lemma : (1# + x ⋆ * x) * x ≤ 1# + x ⋆ * x lemma = begin (1# + x ⋆ * x) * x ≤⟨ *-monoʳ _ $ +-monoˡ _ $ x⋆x≤x⋆ _ ⟩ - (1# + x ⋆) * x ≈⟨ *-congʳ (1+x⋆≈x⋆ _) ⟩ + (1# + x ⋆) * x ≈⟨ *-congʳ $ 1+x⋆≈x⋆ _ ⟩ x ⋆ * x ≤⟨ y≤x+y _ _ ⟩ 1# + x ⋆ * x ∎ @@ -266,13 +271,13 @@ x⋆≈1+x⋆x x = begin-equality 1# ∎ 0⋆≈1 : 0# ⋆ ≈ 1# -0⋆≈1 = ≤-antisym 0⋆≤1 1≤[ _ ]⋆ +0⋆≈1 = 0⋆≤1 ⟨⟩ 1≤[ _ ]⋆ 1⋆≤1 : 1# ⋆ ≤ 1# 1⋆≤1 = ⋆-elimˡ ≤-refl $ ≤-reflexive $ *-identityˡ _ 1⋆≈1 : 1# ⋆ ≈ 1# -1⋆≈1 = ≤-antisym 1⋆≤1 1≤[ _ ]⋆ +1⋆≈1 = 1⋆≤1 ⟨⟩ 1≤[ _ ]⋆ -- _⋆ is monotonic, and hence congruent for _≈_ @@ -294,7 +299,7 @@ x⋆≤x⋆⋆ : ∀ x → x ⋆ ≤ (x ⋆) ⋆ x⋆≤x⋆⋆ = ⋆-mono ∘ x≤x⋆ x⋆⋆≈x⋆ : ∀ x → (x ⋆) ⋆ ≈ x ⋆ -x⋆⋆≈x⋆ x = ≤-antisym (x⋆⋆≤x⋆ x) (x⋆≤x⋆⋆ x) +x⋆⋆≈x⋆ x = x⋆⋆≤x⋆ x ⟨⟩ x⋆≤x⋆⋆ x -- distributive laws @@ -317,9 +322,10 @@ yx≤zy⇒yx⋆≤z⋆y {y = y}{x = x} {z = z} yx≤zy = starDestructiveʳ _ _ _ z ⋆ * y ∎ xy≈yz⇒x⋆y≈yz⋆ : x * y ≈ y * z → x ⋆ * y ≈ y * z ⋆ -xy≈yz⇒x⋆y≈yz⋆ {x = x} {y = y} {z = z} xy≈yz = ≤-antisym - (xy≤yz⇒x⋆y≤yz⋆ (≤-reflexive xy≈yz)) - (yx≤zy⇒yx⋆≤z⋆y (≤-reflexive (sym xy≈yz))) +xy≈yz⇒x⋆y≈yz⋆ {x = x} {y = y} {z = z} xy≈yz = + xy≤yz⇒x⋆y≤yz⋆ (begin x * y ≈⟨ xy≈yz ⟩ y * z ∎) + ⟨⟩ + yx≤zy⇒yx⋆≤z⋆y (begin y * z ≈⟨ xy≈yz ⟨ x * y ∎) -- a useful absorption property From 5d108844f397941b8d6b0756c66206848a11c93d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Jul 2026 11:31:46 +0100 Subject: [PATCH 4/4] cleanup: remove spurious `import` --- src/Relation/Binary/Reasoning/PartialOrder.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda index 5b491f4dd5..72993aa500 100644 --- a/src/Relation/Binary/Reasoning/PartialOrder.agda +++ b/src/Relation/Binary/Reasoning/PartialOrder.agda @@ -40,7 +40,6 @@ {-# OPTIONS --without-K --safe #-} open import Relation.Binary.Bundles using (Poset) ---open import Relation.Binary.Structures using (IsPartialOrder) module Relation.Binary.Reasoning.PartialOrder {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where