[ re #392 ] Proved results and added definitions for cancellative operators

CHANGELOG.md

@@ -8,6 +8,12 @@ Important changes since 0.16:
 Non-backwards compatible changes
 --------------------------------
 
+#### New results regarding cancellative operators
+
+* `Algebra.FunctionProperties.Consequences` now contains a proof of the
+  equi-provability of left and right cancellation for a binary operator,
+  provided we have access to an injective function that is contravariant on the operation.
+
 #### New codata library
 
 * A new `Codata` library using copatterns and sized types rather

src/Algebra/FunctionProperties.agda

@@ -70,6 +70,12 @@ _DistributesOver_ : Op₂ A → Op₂ A → Set _
 _IdempotentOn_ : Op₂ A → A → Set _
 _∙_ IdempotentOn x = (x ∙ x) ≈ x
 
+_ContravariantOn_ : Op₁ A → Op₂ A → Set _
+f ContravariantOn _∙_ = ∀ x y → f (x ∙ y) ≈ (f y ∙ f x)
+
+_NecessarilyIdempotentFor_ : A → Op₂ A → Set _
+z NecessarilyIdempotentFor _∙_ = ∀ x y → (x ∙ y) ≈ z → (x ≈ z) × (y ≈ z)
+
 Idempotent : Op₂ A → Set _
 Idempotent ∙ = ∀ x → ∙ IdempotentOn x
 

src/Algebra/FunctionProperties/Consequences.agda

@@ -15,6 +15,7 @@ open import Algebra.FunctionProperties _≈_
 open import Relation.Binary.EqReasoning S
 open import Data.Sum using (inj₁; inj₂)
 open import Data.Product using (proj₁; proj₂)
+open import Function.Injection using (Injection)
 
 ------------------------------------------------------------------------
 -- Existence of identity elements
@@ -164,6 +165,25 @@ comm+cancelʳ⇒cancelˡ {_•_} comm cancelʳ x {y} {z} eq = cancelʳ y z (begi
   x • z ≈⟨ comm x z ⟩
   z • x ∎)
 
+module InjectiveContravariantOperator {_•_ : Op₂ Carrier} (dual : Injection S S)
+         (let open Injection dual renaming (_⟨$⟩_ to _˘))
+         (contravariant : _˘ ContravariantOn _•_)
+  where
+
+    cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
+    cancelʳ⇒cancelˡ cancelʳ x {y} {z} xy≈xz = injective (cancelʳ _ _ (begin
+      (y ˘) • (x ˘) ≈⟨ sym (contravariant _ _) ⟩
+      (x • y) ˘     ≈⟨ cong xy≈xz              ⟩
+      (x • z) ˘     ≈⟨ contravariant _ _       ⟩
+      (z ˘) • (x ˘) ∎))
+
+    cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
+    cancelˡ⇒cancelʳ cancelˡ {x} y z yx≈zx = injective (cancelˡ _ ( begin
+      (x ˘) • (y ˘) ≈⟨ sym (contravariant _ _) ⟩
+      (y • x) ˘     ≈⟨ cong yx≈zx              ⟩
+      (z • x) ˘     ≈⟨ contravariant _ _       ⟩
+      (x ˘) • (z ˘) ∎ ) )
+
 ------------------------------------------------------------------------
 -- Selectivity implies idempotence