Properties.agda

------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about signs
------------------------------------------------------------------------

module Data.Sign.Properties where

open import Data.Empty
open import Function
open import Data.Sign
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality
open import Algebra.FunctionProperties (_≡_ {A = Sign})

-- The opposite of a sign is not equal to the sign.

opposite-not-equal : ∀ s → s ≢ opposite s
opposite-not-equal - ()
opposite-not-equal + ()

opposite-cong : ∀ {s t} → opposite s ≡ opposite t → s ≡ t
opposite-cong { - } { - } refl = refl
opposite-cong { - } { + } ()
opposite-cong { + } { - } ()
opposite-cong { + } { + } refl = refl

------------------------------------------------------------------------
-- _*_

*-identityˡ : LeftIdentity + _*_
*-identityˡ _ = refl

*-identityʳ : RightIdentity + _*_
*-identityʳ - = refl
*-identityʳ + = refl

*-identity : Identity + _*_
*-identity = *-identityˡ  , *-identityʳ

cancel-*-right : RightCancellative _*_
cancel-*-right - - _  = refl
cancel-*-right - + eq = ⊥-elim (opposite-not-equal _ $ sym eq)
cancel-*-right + - eq = ⊥-elim (opposite-not-equal _ eq)
cancel-*-right + + _  = refl

cancel-*-left : LeftCancellative _*_
cancel-*-left - eq = opposite-cong eq
cancel-*-left + eq = eq

*-cancellative : Cancellative _*_
*-cancellative = cancel-*-left , cancel-*-right