[ fix #392] Added cancellative and conical properties for _++_

CHANGELOG.md

@@ -483,6 +483,10 @@ Other minor additions
 
 * Added new types to `Algebra.FunctionProperties`:
   ```agda
+  LeftConical e _∙_  = ∀ x y → (x ∙ y) ≈ e → x ≈ e
+  RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
+  Conical e ∙        = LeftConical e ∙ × RightConical e ∙
+
   LeftCongruent  _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
   RightCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
   ```
@@ -773,15 +777,21 @@ Other minor additions
 
 * Added new proofs to `Data.List.Properties`:
   ```agda
-  ≡-dec : Decidable _≡_ → Decidable {A = List A} _≡_
+  ≡-dec       : Decidable _≡_ → Decidable {A = List A} _≡_
 
-  ++-isMagma : IsMagma _++_
+  ++-cancelˡ  : xs ++ ys ≡ xs ++ zs → ys ≡ zs
+  ++-cancelʳ  : ys ++ xs ≡ zs ++ xs → ys ≡ zs
+  ++-cancel   : Cancellative _++_
+  ++-conicalˡ : xs ++ ys ≡ [] → xs ≡ []
+  ++-conicalʳ : xs ++ ys ≡ [] → ys ≡ []
+  ++-conical  : Conical [] _++_
+  ++-isMagma  : IsMagma _++_
 
-  length-%=  : length (xs [ k ]%= f) ≡ length xs
-  length-∷=  : length (xs [ k ]∷= v) ≡ length xs
-  map-∷=     : map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
-  length-─   : length (xs ─ k) ≡ pred (length xs)
-  map-─      : map f (xs ─ k) ≡ map f xs ─ cast eq k
+  length-%=   : length (xs [ k ]%= f) ≡ length xs
+  length-∷=   : length (xs [ k ]∷= v) ≡ length xs
+  map-∷=      : map f (xs [ k ]∷= v) ≡ map f xs [ cast eq k ]∷= f v
+  length-─    : length (xs ─ k) ≡ pred (length xs)
+  map-─       : map f (xs ─ k) ≡ map f xs ─ cast eq k
 
   length-applyUpTo     : length (applyUpTo     f n) ≡ n
   length-applyDownFrom : length (applyDownFrom f n) ≡ n
@@ -893,6 +903,7 @@ Other minor additions
   m⊔n<o⇒n<o : ∀ m n {o} → m ⊔ n < o → n < o
 
   m≢0⇒suc[pred[m]]≡m : m ≢ 0 → suc (pred m) ≡ m
+  m≢1+n+m            : m ≢ suc (n + m)
 
   ≡ᵇ⇒≡         : T (m ≡ᵇ n) → m ≡ n
   ≡⇒≡ᵇ         : m ≡ n → T (m ≡ᵇ n)

src/Algebra/FunctionProperties.agda

@@ -38,7 +38,7 @@ RightIdentity : A → Op₂ A → Set _
 RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x
 
 Identity : A → Op₂ A → Set _
-Identity e ∙ = LeftIdentity e ∙ × RightIdentity e ∙
+Identity e ∙ = (LeftIdentity e ∙) × (RightIdentity e ∙)
 
 LeftZero : A → Op₂ A → Set _
 LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z
@@ -47,7 +47,7 @@ RightZero : A → Op₂ A → Set _
 RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
 
 Zero : A → Op₂ A → Set _
-Zero z ∙ = LeftZero z ∙ × RightZero z ∙
+Zero z ∙ = (LeftZero z ∙) × (RightZero z ∙)
 
 LeftInverse : A → Op₁ A → Op₂ A → Set _
 LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e
@@ -56,7 +56,16 @@ RightInverse : A → Op₁ A → Op₂ A → Set _
 RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e
 
 Inverse : A → Op₁ A → Op₂ A → Set _
-Inverse e ⁻¹ ∙ = LeftInverse e ⁻¹ ∙ × RightInverse e ⁻¹ ∙
+Inverse e ⁻¹ ∙ = (LeftInverse e ⁻¹) ∙ × (RightInverse e ⁻¹ ∙)
+
+LeftConical : A → Op₂ A → Set _
+LeftConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → x ≈ e
+
+RightConical : A → Op₂ A → Set _
+RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
+
+Conical : A → Op₂ A → Set _
+Conical e ∙ = (LeftConical e ∙) × (RightConical e ∙)
 
 _DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
 _*_ DistributesOverˡ _+_ =
@@ -97,7 +106,7 @@ RightCancellative : Op₂ A → Set _
 RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
 
 Cancellative : Op₂ A → Set _
-Cancellative _•_ = LeftCancellative _•_ × RightCancellative _•_
+Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
 Congruent₁ : Op₁ A → Set _
 Congruent₁ f = f Preserves _≈_ ⟶ _≈_

src/Data/List/Properties.agda

@@ -13,7 +13,7 @@ module Data.List.Properties where
 
 open import Algebra
 import Algebra.Structures as Structures
-open import Algebra.FunctionProperties
+import Algebra.FunctionProperties as FunctionProperties
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
 open import Data.Fin using (Fin; zero; suc; cast; toℕ)
 open import Data.List as List
@@ -132,18 +132,24 @@ module _ {a b} {A : Set a} {B : Set b} (f : A → Maybe B) where
 
 module _ {a} {A : Set a} where
 
-  ++-assoc : Associative {A = List A} _≡_ _++_
+  length-++ : ∀ (xs : List A) {ys} → length (xs ++ ys) ≡ length xs + length ys
+  length-++ []       = refl
+  length-++ (x ∷ xs) = P.cong suc (length-++ xs)
+
+  open FunctionProperties {A = List A} _≡_
+
+  ++-assoc : Associative _++_
   ++-assoc []       ys zs = refl
   ++-assoc (x ∷ xs) ys zs = P.cong (x ∷_) (++-assoc xs ys zs)
 
-  ++-identityˡ : LeftIdentity {A = List A} _≡_ [] _++_
+  ++-identityˡ : LeftIdentity [] _++_
   ++-identityˡ xs = refl
 
-  ++-identityʳ : RightIdentity {A = List A} _≡_ [] _++_
+  ++-identityʳ : RightIdentity [] _++_
   ++-identityʳ []       = refl
   ++-identityʳ (x ∷ xs) = P.cong (x ∷_) (++-identityʳ xs)
 
-  ++-identity : Identity {A = List A} _≡_ [] _++_
+  ++-identity : Identity [] _++_
   ++-identity = ++-identityˡ , ++-identityʳ
 
   ++-identityʳ-unique : ∀ (xs : List A) {ys} → xs ≡ xs ++ ys → ys ≡ []
@@ -163,9 +169,32 @@ module _ {a} {A : Set a} where
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()
 
-  length-++ : ∀ (xs : List A) {ys} → length (xs ++ ys) ≡ length xs + length ys
-  length-++ []       = refl
-  length-++ (x ∷ xs) = P.cong suc (length-++ xs)
+  ++-cancelˡ : ∀ xs {ys zs : List A} → xs ++ ys ≡ xs ++ zs → ys ≡ zs
+  ++-cancelˡ []       ys≡zs             = ys≡zs
+  ++-cancelˡ (x ∷ xs) x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)
+
+  ++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≡ zs ++ xs → ys ≡ zs
+  ++-cancelʳ []       []       _             = refl
+  ++-cancelʳ {xs} []           (z ∷ zs) eq =
+    contradiction (P.trans (cong length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
+  ++-cancelʳ {xs} (y ∷ ys) []       eq =
+    contradiction (P.trans (P.sym (length-++ (y ∷ ys))) (cong length eq)) (m≢1+n+m (length xs) ∘ sym)
+  ++-cancelʳ (y ∷ ys) (z ∷ zs) eq =
+    P.cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ ys zs (∷-injectiveʳ eq))
+
+  ++-cancel : Cancellative _++_
+  ++-cancel = ++-cancelˡ , ++-cancelʳ
+
+  ++-conicalˡ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → xs ≡ []
+  ++-conicalˡ []       _ refl = refl
+  ++-conicalˡ (x ∷ xs) _ ()
+
+  ++-conicalʳ : ∀ (xs ys : List A) → xs ++ ys ≡ [] → ys ≡ []
+  ++-conicalʳ []       _ refl = refl
+  ++-conicalʳ (x ∷ xs) _ ()
+
+  ++-conical : Conical [] _++_
+  ++-conical = ++-conicalˡ , ++-conicalʳ
 
 module _ {a} {A : Set a} where
 
@@ -764,6 +793,8 @@ module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where
 
 module _ {a} {A : Set a} where
 
+  open FunctionProperties {A = List A} _≡_
+
   unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
   unfold-reverse x xs = helper [ x ] xs
     where
@@ -787,7 +818,7 @@ module _ {a} {A : Set a} where
     reverse ys ++ reverse (x ∷ xs)       ∎
     where open P.≡-Reasoning
 
-  reverse-involutive : Involutive {A = List A} _≡_ reverse
+  reverse-involutive : Involutive reverse
   reverse-involutive [] = refl
   reverse-involutive (x ∷ xs) = begin
     reverse (reverse (x ∷ xs))   ≡⟨ P.cong reverse $ unfold-reverse x xs ⟩

src/Data/Nat/Properties.agda

@@ -461,6 +461,9 @@ m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
 m≢1+m+n zero    ()
 m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)
 
+m≢1+n+m : ∀ m {n} → m ≢ suc (n + m)
+m≢1+n+m m m≡1+n+m = m≢1+m+n m (trans m≡1+n+m (cong suc (+-comm _ m)))
+
 i+1+j≢i : ∀ i {j} → i + suc j ≢ i
 i+1+j≢i zero    ()
 i+1+j≢i (suc i) = (i+1+j≢i i) ∘ suc-injective