[ add ] syntax for antisym equality reasoning in Relation.Binary.Reasoning.PartialOrder #3047

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
+  ```

src/Algebra/Properties/KleeneAlgebra.agda

@@ -246,11 +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ˡ _
+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#
 

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