{-# OPTIONS --cubical-compatible --safe #-}
module Data.Nat.Binary.Properties where
open import Algebra.Bundles
open import Algebra.Morphism.Structures
import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism
open import Algebra.Consequences.Propositional using (comm∧distrˡ⇒distrʳ)
open import Data.Bool.Base using (if_then_else_; Bool; true; false)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Nat.Binary.Base
open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; s<s⁻¹)
open import Data.Nat.DivMod using (_%_; _/_; m/n≤m; +-distrib-/-∣ˡ)
open import Data.Nat.Divisibility using (∣-refl)
import Data.Nat.Properties as ℕ
open import Data.Nat.Solver using (module +-*-Solver)
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_∘_; _$_; id)
open import Function.Definitions using (Injective; Surjective;
Inverseˡ; Inverseʳ; Inverseᵇ)
open import Function.Consequences.Propositional
using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ;
strictlyInverseʳ⇒inverseʳ)
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.Consequences using (trans∧irr⇒asym; tri⇒dec<)
open import Relation.Binary.Morphism
using (IsRelHomomorphism; IsOrderHomomorphism; IsOrderMonomorphism)
import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism
open import Relation.Binary.PropositionalEquality.Algebra
using (magma; isMagma)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≢_; refl; cong; cong₂; sym; _≗_; trans; ≢-sym; subst₂;
subst; resp₂)
open import Relation.Binary.PropositionalEquality.Properties
using (isDecEquivalence; setoid; decSetoid; module ≡-Reasoning;
isEquivalence)
open import Relation.Nullary using (¬_; yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation.Core using (contradiction)
open import Algebra.Definitions {A = ℕᵇ} _≡_
open import Algebra.Structures {A = ℕᵇ} _≡_
import Algebra.Properties.CommutativeSemigroup as CommSemigProp
import Algebra.Properties.CommutativeSemigroup ℕ.+-commutativeSemigroup
as ℕ-+-semigroupProperties
import Relation.Binary.Construct.StrictToNonStrict _≡_ _<_
as StrictToNonStrict
open +-*-Solver
private
variable
x : ℕᵇ
infix 4 _<?_ _≟_ _≤?_
2[1+x]≢0 : 2[1+ x ] ≢ 0ᵇ
2[1+x]≢0 ()
1+[2x]≢0 : 1+[2 x ] ≢ 0ᵇ
1+[2x]≢0 ()
2[1+_]-injective : Injective _≡_ _≡_ 2[1+_]
2[1+_]-injective refl = refl
1+[2_]-injective : Injective _≡_ _≡_ 1+[2_]
1+[2_]-injective refl = refl
_≟_ : DecidableEquality ℕᵇ
zero ≟ zero = yes refl
zero ≟ 2[1+ _ ] = no λ()
zero ≟ 1+[2 _ ] = no λ()
2[1+ _ ] ≟ zero = no λ()
2[1+ x ] ≟ 2[1+ y ] = Dec.map′ (cong 2[1+_]) 2[1+_]-injective (x ≟ y)
2[1+ _ ] ≟ 1+[2 _ ] = no λ()
1+[2 _ ] ≟ zero = no λ()
1+[2 _ ] ≟ 2[1+ _ ] = no λ()
1+[2 x ] ≟ 1+[2 y ] = Dec.map′ (cong 1+[2_]) 1+[2_]-injective (x ≟ y)
≡-isDecEquivalence : IsDecEquivalence {A = ℕᵇ} _≡_
≡-isDecEquivalence = isDecEquivalence _≟_
≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid ℕᵇ
≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_
toℕ-double : ∀ x → toℕ (double x) ≡ 2 ℕ.* (toℕ x)
toℕ-double zero = refl
toℕ-double 1+[2 x ] = cong ((2 ℕ.*_) ∘ ℕ.suc) (toℕ-double x)
toℕ-double 2[1+ x ] = cong (2 ℕ.*_) (sym (ℕ.*-distribˡ-+ 2 1 (toℕ x)))
toℕ-suc : ∀ x → toℕ (suc x) ≡ ℕ.suc (toℕ x)
toℕ-suc zero = refl
toℕ-suc 2[1+ x ] = cong (ℕ.suc ∘ (2 ℕ.*_)) (toℕ-suc x)
toℕ-suc 1+[2 x ] = ℕ.*-distribˡ-+ 2 1 (toℕ x)
toℕ-pred : ∀ x → toℕ (pred x) ≡ ℕ.pred (toℕ x)
toℕ-pred zero = refl
toℕ-pred 2[1+ x ] = cong ℕ.pred $ sym $ ℕ.*-distribˡ-+ 2 1 (toℕ x)
toℕ-pred 1+[2 x ] = toℕ-double x
toℕ-fromℕ' : toℕ ∘ fromℕ' ≗ id
toℕ-fromℕ' 0 = refl
toℕ-fromℕ' (ℕ.suc n) = begin
toℕ (fromℕ' (ℕ.suc n)) ≡⟨⟩
toℕ (suc (fromℕ' n)) ≡⟨ toℕ-suc (fromℕ' n) ⟩
ℕ.suc (toℕ (fromℕ' n)) ≡⟨ cong ℕ.suc (toℕ-fromℕ' n) ⟩
ℕ.suc n ∎
where open ≡-Reasoning
fromℕ≡fromℕ' : fromℕ ≗ fromℕ'
fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕ.≤-refl
where
split : ℕᵇ → Maybe Bool × ℕᵇ
split zero = nothing , zero
split 2[1+ n ] = just false , n
split 1+[2 n ] = just true , n
head = proj₁ ∘ split
tail = proj₂ ∘ split
split-injective : Injective _≡_ _≡_ split
split-injective {zero} {zero} refl = refl
split-injective {2[1+ _ ]} {2[1+ _ ]} refl = refl
split-injective {1+[2 _ ]} {1+[2 _ ]} refl = refl
split-if : ∀ x xs → split (if x then 1+[2 xs ] else 2[1+ xs ]) ≡ (just x , xs)
split-if false xs = refl
split-if true xs = refl
head-suc : ∀ n → head (suc (suc (suc n))) ≡ head (suc n)
head-suc zero = refl
head-suc 2[1+ n ] = refl
head-suc 1+[2 n ] = refl
tail-suc : ∀ n → suc (tail (suc n)) ≡ tail (suc (suc (suc n)))
tail-suc zero = refl
tail-suc 2[1+ n ] = refl
tail-suc 1+[2 n ] = refl
head-homo : ∀ n → head (suc (fromℕ' n)) ≡ just (n % 2 ℕ.≡ᵇ 0)
head-homo ℕ.zero = refl
head-homo (ℕ.suc ℕ.zero) = refl
head-homo (ℕ.suc (ℕ.suc n)) = trans (head-suc (fromℕ' n)) (head-homo n)
open ≡-Reasoning
tail-homo : ∀ n → tail (suc (fromℕ' n)) ≡ fromℕ' (n / 2)
tail-homo ℕ.zero = refl
tail-homo (ℕ.suc ℕ.zero) = refl
tail-homo (ℕ.suc (ℕ.suc n)) = begin
tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡⟨ tail-suc (fromℕ' n) ⟨
suc (tail (suc (fromℕ' n))) ≡⟨ cong suc (tail-homo n) ⟩
fromℕ' (ℕ.suc (n / 2)) ≡⟨ cong fromℕ' (+-distrib-/-∣ˡ {2} n ∣-refl) ⟨
fromℕ' (ℕ.suc (ℕ.suc n) / 2) ∎
fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ.helper n n w ≡ fromℕ' n
fromℕ-helper≡fromℕ' ℕ.zero w p = refl
fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) =
split-injective (begin
split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩
just (n % 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n / 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩
just (n % 2 ℕ.≡ᵇ 0) , fromℕ' (n / 2) ≡⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟨
head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩
split (fromℕ' (ℕ.suc n)) ∎)
where rec-n/2 = fromℕ-helper≡fromℕ' (n / 2) w (ℕ.≤-trans (m/n≤m n 2) n≤w)
toℕ-fromℕ : toℕ ∘ fromℕ ≗ id
toℕ-fromℕ n rewrite fromℕ≡fromℕ' n = toℕ-fromℕ' n
toℕ-injective : Injective _≡_ _≡_ toℕ
toℕ-injective {zero} {zero} _ = refl
toℕ-injective {2[1+ x ]} {2[1+ y ]} 2[1+xN]≡2[1+yN] = cong 2[1+_] x≡y
where
1+xN≡1+yN = ℕ.*-cancelˡ-≡ (ℕ.suc _) (ℕ.suc _) 2 2[1+xN]≡2[1+yN]
xN≡yN = cong ℕ.pred 1+xN≡1+yN
x≡y = toℕ-injective xN≡yN
toℕ-injective {2[1+ x ]} {1+[2 y ]} 2[1+xN]≡1+2yN =
contradiction 2[1+xN]≡1+2yN (ℕ.even≢odd (ℕ.suc (toℕ x)) (toℕ y))
toℕ-injective {1+[2 x ]} {2[1+ y ]} 1+2xN≡2[1+yN] =
contradiction (sym 1+2xN≡2[1+yN]) (ℕ.even≢odd (ℕ.suc (toℕ y)) (toℕ x))
toℕ-injective {1+[2 x ]} {1+[2 y ]} 1+2xN≡1+2yN = cong 1+[2_] x≡y
where
2xN≡2yN = cong ℕ.pred 1+2xN≡1+2yN
xN≡yN = ℕ.*-cancelˡ-≡ _ _ 2 2xN≡2yN
x≡y = toℕ-injective xN≡yN
toℕ-surjective : Surjective _≡_ _≡_ toℕ
toℕ-surjective = strictlySurjective⇒surjective (λ n → fromℕ n , toℕ-fromℕ n)
toℕ-isRelHomomorphism : IsRelHomomorphism _≡_ _≡_ toℕ
toℕ-isRelHomomorphism = record
{ cong = cong toℕ
}
fromℕ-injective : Injective _≡_ _≡_ fromℕ
fromℕ-injective {x} {y} f[x]≡f[y] = begin
x ≡⟨ sym (toℕ-fromℕ x) ⟩
toℕ (fromℕ x) ≡⟨ cong toℕ f[x]≡f[y] ⟩
toℕ (fromℕ y) ≡⟨ toℕ-fromℕ y ⟩
y ∎
where open ≡-Reasoning
fromℕ-toℕ : fromℕ ∘ toℕ ≗ id
fromℕ-toℕ = toℕ-injective ∘ toℕ-fromℕ ∘ toℕ
toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ
toℕ-inverseˡ = strictlyInverseˡ⇒inverseˡ {f⁻¹ = fromℕ} toℕ toℕ-fromℕ
toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ
toℕ-inverseʳ = strictlyInverseʳ⇒inverseʳ toℕ fromℕ-toℕ
toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ
toℕ-inverseᵇ = toℕ-inverseˡ , toℕ-inverseʳ
fromℕ-pred : ∀ n → fromℕ (ℕ.pred n) ≡ pred (fromℕ n)
fromℕ-pred n = begin
fromℕ (ℕ.pred n) ≡⟨ cong (fromℕ ∘ ℕ.pred) (sym (toℕ-fromℕ n)) ⟩
fromℕ (ℕ.pred (toℕ y)) ≡⟨ cong fromℕ (sym (toℕ-pred y)) ⟩
fromℕ (toℕ (pred y)) ≡⟨ fromℕ-toℕ (pred y) ⟩
pred y ≡⟨ refl ⟩
pred (fromℕ n) ∎
where open ≡-Reasoning; y = fromℕ n
x≡0⇒toℕ[x]≡0 : x ≡ zero → toℕ x ≡ 0
x≡0⇒toℕ[x]≡0 {zero} _ = refl
toℕ[x]≡0⇒x≡0 : toℕ x ≡ 0 → x ≡ zero
toℕ[x]≡0⇒x≡0 {zero} _ = refl
x≮0 : x ≮ zero
x≮0 ()
x≢0⇒x>0 : x ≢ zero → x > zero
x≢0⇒x>0 {zero} 0≢0 = contradiction refl 0≢0
x≢0⇒x>0 {2[1+ _ ]} _ = 0<even
x≢0⇒x>0 {1+[2 _ ]} _ = 0<odd
1+[2x]<2[1+x] : ∀ x → 1+[2 x ] < 2[1+ x ]
1+[2x]<2[1+x] x = odd<even (inj₂ refl)
<⇒≢ : _<_ ⇒ _≢_
<⇒≢ (even<even x<x) refl = <⇒≢ x<x refl
<⇒≢ (odd<odd x<x) refl = <⇒≢ x<x refl
>⇒≢ : _>_ ⇒ _≢_
>⇒≢ y<x = ≢-sym (<⇒≢ y<x)
≡⇒≮ : _≡_ ⇒ _≮_
≡⇒≮ x≡y x<y = <⇒≢ x<y x≡y
≡⇒≯ : _≡_ ⇒ _≯_
≡⇒≯ x≡y x>y = >⇒≢ x>y x≡y
<⇒≯ : _<_ ⇒ _≯_
<⇒≯ (even<even x<y) (even<even y<x) = <⇒≯ x<y y<x
<⇒≯ (even<odd x<y) (odd<even (inj₁ y<x)) = <⇒≯ x<y y<x
<⇒≯ (even<odd x<y) (odd<even (inj₂ refl)) = <⇒≢ x<y refl
<⇒≯ (odd<even (inj₁ x<y)) (even<odd y<x) = <⇒≯ x<y y<x
<⇒≯ (odd<even (inj₂ refl)) (even<odd y<x) = <⇒≢ y<x refl
<⇒≯ (odd<odd x<y) (odd<odd y<x) = <⇒≯ x<y y<x
>⇒≮ : _>_ ⇒ _≮_
>⇒≮ y<x = <⇒≯ y<x
<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = inj₁
toℕ-mono-< : toℕ Preserves _<_ ⟶ ℕ._<_
toℕ-mono-< {zero} {2[1+ _ ]} _ = ℕ.0<1+n
toℕ-mono-< {zero} {1+[2 _ ]} _ = ℕ.0<1+n
toℕ-mono-< {2[1+ x ]} {2[1+ y ]} (even<even x<y) = begin
ℕ.suc (2 ℕ.* (ℕ.suc xN)) ≤⟨ ℕ.+-monoʳ-≤ 1 (ℕ.*-monoʳ-≤ 2 xN<yN) ⟩
ℕ.suc (2 ℕ.* yN) ≤⟨ ℕ.n≤1+n _ ⟩
2 ℕ.+ (2 ℕ.* yN) ≡⟨ sym (ℕ.*-distribˡ-+ 2 1 yN) ⟩
2 ℕ.* (ℕ.suc yN) ∎
where open ℕ.≤-Reasoning; xN = toℕ x; yN = toℕ y; xN<yN = toℕ-mono-< x<y
toℕ-mono-< {2[1+ x ]} {1+[2 y ]} (even<odd x<y) =
ℕ.+-monoʳ-≤ 1 (ℕ.*-monoʳ-≤ 2 (toℕ-mono-< x<y))
toℕ-mono-< {1+[2 x ]} {2[1+ y ]} (odd<even (inj₁ x<y)) = begin
ℕ.suc (ℕ.suc (2 ℕ.* xN)) ≡⟨⟩
2 ℕ.+ (2 ℕ.* xN) ≡⟨ sym (ℕ.*-distribˡ-+ 2 1 xN) ⟩
2 ℕ.* (ℕ.suc xN) ≤⟨ ℕ.*-monoʳ-≤ 2 xN<yN ⟩
2 ℕ.* yN ≤⟨ ℕ.*-monoʳ-≤ 2 (ℕ.n≤1+n _) ⟩
2 ℕ.* (ℕ.suc yN) ∎
where open ℕ.≤-Reasoning; xN = toℕ x; yN = toℕ y; xN<yN = toℕ-mono-< x<y
toℕ-mono-< {1+[2 x ]} {2[1+ .x ]} (odd<even (inj₂ refl)) =
ℕ.≤-reflexive (sym (ℕ.*-distribˡ-+ 2 1 (toℕ x)))
toℕ-mono-< {1+[2 x ]} {1+[2 y ]} (odd<odd x<y) = ℕ.+-monoʳ-< 1 (ℕ.*-monoʳ-< 2 xN<yN)
where xN = toℕ x; yN = toℕ y; xN<yN = toℕ-mono-< x<y
toℕ-cancel-< : ∀ {x y} → toℕ x ℕ.< toℕ y → x < y
toℕ-cancel-< {zero} {2[1+ y ]} x<y = 0<even
toℕ-cancel-< {zero} {1+[2 y ]} x<y = 0<odd
toℕ-cancel-< {2[1+ x ]} {2[1+ y ]} x<y =
even<even (toℕ-cancel-< (s<s⁻¹ (ℕ.*-cancelˡ-< 2 _ _ x<y)))
toℕ-cancel-< {2[1+ x ]} {1+[2 y ]} x<y
rewrite ℕ.*-distribˡ-+ 2 1 (toℕ x) =
even<odd (toℕ-cancel-< (ℕ.*-cancelˡ-< 2 _ _ (ℕ.≤-trans (s≤s (ℕ.n≤1+n _)) (s<s⁻¹ x<y))))
toℕ-cancel-< {1+[2 x ]} {2[1+ y ]} x<y with toℕ x ℕ.≟ toℕ y
... | yes x≡y = odd<even (inj₂ (toℕ-injective x≡y))
... | no x≢y
rewrite ℕ.+-suc (toℕ y) (toℕ y ℕ.+ 0) =
odd<even (inj₁ (toℕ-cancel-< (ℕ.≤∧≢⇒< (ℕ.*-cancelˡ-≤ 2 (ℕ.+-cancelˡ-≤ 2 _ _ x<y)) x≢y)))
toℕ-cancel-< {1+[2 x ]} {1+[2 y ]} x<y =
odd<odd (toℕ-cancel-< (ℕ.*-cancelˡ-< 2 _ _ (s<s⁻¹ x<y)))
fromℕ-cancel-< : ∀ {x y} → fromℕ x < fromℕ y → x ℕ.< y
fromℕ-cancel-< = subst₂ ℕ._<_ (toℕ-fromℕ _) (toℕ-fromℕ _) ∘ toℕ-mono-<
fromℕ-mono-< : fromℕ Preserves ℕ._<_ ⟶ _<_
fromℕ-mono-< = toℕ-cancel-< ∘ subst₂ ℕ._<_ (sym (toℕ-fromℕ _)) (sym (toℕ-fromℕ _))
toℕ-isHomomorphism-< : IsOrderHomomorphism _≡_ _≡_ _<_ ℕ._<_ toℕ
toℕ-isHomomorphism-< = record
{ cong = cong toℕ
; mono = toℕ-mono-<
}
toℕ-isMonomorphism-< : IsOrderMonomorphism _≡_ _≡_ _<_ ℕ._<_ toℕ
toℕ-isMonomorphism-< = record
{ isOrderHomomorphism = toℕ-isHomomorphism-<
; injective = toℕ-injective
; cancel = toℕ-cancel-<
}
<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (even<even x<x) = <-irrefl refl x<x
<-irrefl refl (odd<odd x<x) = <-irrefl refl x<x
<-trans : Transitive _<_
<-trans {zero} {_} {2[1+ _ ]} _ _ = 0<even
<-trans {zero} {_} {1+[2 _ ]} _ _ = 0<odd
<-trans (even<even x<y) (even<even y<z) = even<even (<-trans x<y y<z)
<-trans (even<even x<y) (even<odd y<z) = even<odd (<-trans x<y y<z)
<-trans (even<odd x<y) (odd<even (inj₁ y<z)) = even<even (<-trans x<y y<z)
<-trans (even<odd x<y) (odd<even (inj₂ refl)) = even<even x<y
<-trans (even<odd x<y) (odd<odd y<z) = even<odd (<-trans x<y y<z)
<-trans (odd<even (inj₁ x<y)) (even<even y<z) = odd<even (inj₁ (<-trans x<y y<z))
<-trans (odd<even (inj₂ refl)) (even<even x<z) = odd<even (inj₁ x<z)
<-trans (odd<even (inj₁ x<y)) (even<odd y<z) = odd<odd (<-trans x<y y<z)
<-trans (odd<even (inj₂ refl)) (even<odd x<z) = odd<odd x<z
<-trans (odd<odd x<y) (odd<even (inj₁ y<z)) = odd<even (inj₁ (<-trans x<y y<z))
<-trans (odd<odd x<y) (odd<even (inj₂ refl)) = odd<even (inj₁ x<y)
<-trans (odd<odd x<y) (odd<odd y<z) = odd<odd (<-trans x<y y<z)
<-asym : Asymmetric _<_
<-asym {x} {y} = trans∧irr⇒asym refl <-trans <-irrefl {x} {y}
<-cmp : Trichotomous _≡_ _<_
<-cmp zero zero = tri≈ x≮0 refl x≮0
<-cmp zero 2[1+ _ ] = tri< 0<even (λ()) x≮0
<-cmp zero 1+[2 _ ] = tri< 0<odd (λ()) x≮0
<-cmp 2[1+ _ ] zero = tri> (λ()) (λ()) 0<even
<-cmp 2[1+ x ] 2[1+ y ] with <-cmp x y
... | tri< x<y _ _ = tri< lt (<⇒≢ lt) (<⇒≯ lt) where lt = even<even x<y
... | tri≈ _ refl _ = tri≈ (<-irrefl refl) refl (<-irrefl refl)
... | tri> _ _ x>y = tri> (>⇒≮ gt) (>⇒≢ gt) gt where gt = even<even x>y
<-cmp 2[1+ x ] 1+[2 y ] with <-cmp x y
... | tri< x<y _ _ = tri< lt (<⇒≢ lt) (<⇒≯ lt) where lt = even<odd x<y
... | tri≈ _ refl _ = tri> (>⇒≮ gt) (>⇒≢ gt) gt
where
gt = subst (_< 2[1+ x ]) refl (1+[2x]<2[1+x] x)
... | tri> _ _ y<x = tri> (>⇒≮ gt) (>⇒≢ gt) gt where gt = odd<even (inj₁ y<x)
<-cmp 1+[2 _ ] zero = tri> (>⇒≮ gt) (>⇒≢ gt) gt where gt = 0<odd
<-cmp 1+[2 x ] 2[1+ y ] with <-cmp x y
... | tri< x<y _ _ = tri< lt (<⇒≢ lt) (<⇒≯ lt) where lt = odd<even (inj₁ x<y)
... | tri≈ _ x≡y _ = tri< lt (<⇒≢ lt) (<⇒≯ lt) where lt = odd<even (inj₂ x≡y)
... | tri> _ _ x>y = tri> (>⇒≮ gt) (>⇒≢ gt) gt where gt = even<odd x>y
<-cmp 1+[2 x ] 1+[2 y ] with <-cmp x y
... | tri< x<y _ _ = tri< lt (<⇒≢ lt) (<⇒≯ lt) where lt = odd<odd x<y
... | tri≈ _ refl _ = tri≈ (≡⇒≮ refl) refl (≡⇒≯ refl)
... | tri> _ _ x>y = tri> (>⇒≮ gt) (>⇒≢ gt) gt where gt = odd<odd x>y
_<?_ : Decidable _<_
_<?_ = tri⇒dec< <-cmp
<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
{ isEquivalence = isEquivalence
; irrefl = <-irrefl
; trans = <-trans
; <-resp-≈ = resp₂ _<_
}
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
; compare = <-cmp
}
<-strictPartialOrder : StrictPartialOrder _ _ _
<-strictPartialOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
}
<-strictTotalOrder : StrictTotalOrder _ _ _
<-strictTotalOrder = record
{ isStrictTotalOrder = <-isStrictTotalOrder
}
x<2[1+x] : ∀ x → x < 2[1+ x ]
x<1+[2x] : ∀ x → x < 1+[2 x ]
x<2[1+x] zero = 0<even
x<2[1+x] 2[1+ x ] = even<even (x<2[1+x] x)
x<2[1+x] 1+[2 x ] = odd<even (inj₁ (x<1+[2x] x))
x<1+[2x] zero = 0<odd
x<1+[2x] 2[1+ x ] = even<odd (x<2[1+x] x)
x<1+[2x] 1+[2 x ] = odd<odd (x<1+[2x] x)
<⇒≱ : _<_ ⇒ _≱_
<⇒≱ x<y (inj₁ y<x) = contradiction y<x (<⇒≯ x<y)
<⇒≱ x<y (inj₂ y≡x) = contradiction (sym y≡x) (<⇒≢ x<y)
≤⇒≯ : _≤_ ⇒ _≯_
≤⇒≯ x≤y x>y = <⇒≱ x>y x≤y
≮⇒≥ : _≮_ ⇒ _≥_
≮⇒≥ {x} {y} x≮y with <-cmp x y
... | tri< lt _ _ = contradiction lt x≮y
... | tri≈ _ eq _ = inj₂ (sym eq)
... | tri> _ _ y<x = <⇒≤ y<x
≰⇒> : _≰_ ⇒ _>_
≰⇒> {x} {y} x≰y with <-cmp x y
... | tri< lt _ _ = contradiction (<⇒≤ lt) x≰y
... | tri≈ _ eq _ = contradiction (inj₂ eq) x≰y
... | tri> _ _ x>y = x>y
≤∧≢⇒< : ∀ {x y} → x ≤ y → x ≢ y → x < y
≤∧≢⇒< (inj₁ x<y) _ = x<y
≤∧≢⇒< (inj₂ x≡y) x≢y = contradiction x≡y x≢y
0≤x : ∀ x → zero ≤ x
0≤x zero = inj₂ refl
0≤x 2[1+ _ ] = inj₁ 0<even
0≤x 1+[2 x ] = inj₁ 0<odd
x≤0⇒x≡0 : x ≤ zero → x ≡ zero
x≤0⇒x≡0 (inj₂ x≡0) = x≡0
fromℕ-mono-≤ : fromℕ Preserves ℕ._≤_ ⟶ _≤_
fromℕ-mono-≤ m≤n with ℕ.m≤n⇒m<n∨m≡n m≤n
... | inj₁ m<n = inj₁ (fromℕ-mono-< m<n)
... | inj₂ m≡n = inj₂ (cong fromℕ m≡n)
toℕ-mono-≤ : toℕ Preserves _≤_ ⟶ ℕ._≤_
toℕ-mono-≤ (inj₁ x<y) = ℕ.<⇒≤ (toℕ-mono-< x<y)
toℕ-mono-≤ (inj₂ refl) = ℕ.≤-reflexive refl
toℕ-cancel-≤ : ∀ {x y} → toℕ x ℕ.≤ toℕ y → x ≤ y
toℕ-cancel-≤ = subst₂ _≤_ (fromℕ-toℕ _) (fromℕ-toℕ _) ∘ fromℕ-mono-≤
fromℕ-cancel-≤ : ∀ {x y} → fromℕ x ≤ fromℕ y → x ℕ.≤ y
fromℕ-cancel-≤ = subst₂ ℕ._≤_ (toℕ-fromℕ _) (toℕ-fromℕ _) ∘ toℕ-mono-≤
toℕ-isHomomorphism-≤ : IsOrderHomomorphism _≡_ _≡_ _≤_ ℕ._≤_ toℕ
toℕ-isHomomorphism-≤ = record
{ cong = cong toℕ
; mono = toℕ-mono-≤
}
toℕ-isMonomorphism-≤ : IsOrderMonomorphism _≡_ _≡_ _≤_ ℕ._≤_ toℕ
toℕ-isMonomorphism-≤ = record
{ isOrderHomomorphism = toℕ-isHomomorphism-≤
; injective = toℕ-injective
; cancel = toℕ-cancel-≤
}
≤-refl : Reflexive _≤_
≤-refl = inj₂ refl
≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive {x} {_} refl = ≤-refl {x}
≤-trans : Transitive _≤_
≤-trans = StrictToNonStrict.trans isEquivalence (resp₂ _<_) <-trans
<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z
<-≤-trans x<y (inj₁ y<z) = <-trans x<y y<z
<-≤-trans x<y (inj₂ refl) = x<y
≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z
≤-<-trans (inj₁ x<y) y<z = <-trans x<y y<z
≤-<-trans (inj₂ refl) y<z = y<z
≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym = StrictToNonStrict.antisym isEquivalence <-trans <-irrefl
≤-total : Total _≤_
≤-total x y with <-cmp x y
... | tri< x<y _ _ = inj₁ (<⇒≤ x<y)
... | tri≈ _ x≡y _ = inj₁ (≤-reflexive x≡y)
... | tri> _ _ y<x = inj₂ (<⇒≤ y<x)
_≤?_ : Decidable _≤_
x ≤? y with <-cmp x y
... | tri< x<y _ _ = yes (<⇒≤ x<y)
... | tri≈ _ x≡y _ = yes (≤-reflexive x≡y)
... | tri> _ _ y<x = no (<⇒≱ y<x)
≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = ≤-reflexive
; trans = ≤-trans
}
≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
{ isPreorder = ≤-isPreorder
; antisym = ≤-antisym
}
≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
{ isPartialOrder = ≤-isPartialOrder
; total = ≤-total
}
≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
{ isTotalOrder = ≤-isTotalOrder
; _≟_ = _≟_
; _≤?_ = _≤?_
}
≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
{ isPreorder = ≤-isPreorder
}
≤-partialOrder : Poset 0ℓ 0ℓ 0ℓ
≤-partialOrder = record
{ isPartialOrder = ≤-isPartialOrder
}
≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
{ isTotalOrder = ≤-isTotalOrder
}
≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
{ isDecTotalOrder = ≤-isDecTotalOrder
}
module ≤-Reasoning where
open import Relation.Binary.Reasoning.Base.Triple
≤-isPreorder
<-asym
<-trans
(resp₂ _<_)
<⇒≤
<-≤-trans
≤-<-trans
public
hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
<⇒<ℕ : ∀ {x y} → x < y → x <ℕ y
<⇒<ℕ x<y = toℕ-mono-< x<y
<ℕ⇒< : ∀ {x y} → x <ℕ y → x < y
<ℕ⇒< {x} {y} t[x]<t[y] = begin-strict
x ≡⟨ sym (fromℕ-toℕ x) ⟩
fromℕ (toℕ x) <⟨ fromℕ-mono-< t[x]<t[y] ⟩
fromℕ (toℕ y) ≡⟨ fromℕ-toℕ y ⟩
y ∎
where open ≤-Reasoning
toℕ-homo-+ : ∀ x y → toℕ (x + y) ≡ toℕ x ℕ.+ toℕ y
toℕ-homo-+ zero _ = refl
toℕ-homo-+ 2[1+ x ] zero = cong ℕ.suc (sym (ℕ.+-identityʳ _))
toℕ-homo-+ 1+[2 x ] zero = cong ℕ.suc (sym (ℕ.+-identityʳ _))
toℕ-homo-+ 2[1+ x ] 2[1+ y ] = begin
toℕ (2[1+ x ] + 2[1+ y ]) ≡⟨⟩
toℕ 2[1+ (suc (x + y)) ] ≡⟨⟩
2 ℕ.* (1 ℕ.+ (toℕ (suc (x + y)))) ≡⟨ cong ((2 ℕ.*_) ∘ ℕ.suc) (toℕ-suc (x + y)) ⟩
2 ℕ.* (2 ℕ.+ toℕ (x + y)) ≡⟨ cong ((2 ℕ.*_) ∘ (2 ℕ.+_)) (toℕ-homo-+ x y) ⟩
2 ℕ.* (2 ℕ.+ (toℕ x ℕ.+ toℕ y)) ≡⟨ solve 2 (λ m n → con 2 :* (con 2 :+ (m :+ n)) :=
con 2 :* (con 1 :+ m) :+ con 2 :* (con 1 :+ n))
refl (toℕ x) (toℕ y) ⟩
toℕ 2[1+ x ] ℕ.+ toℕ 2[1+ y ] ∎
where open ≡-Reasoning
toℕ-homo-+ 2[1+ x ] 1+[2 y ] = begin
toℕ (2[1+ x ] + 1+[2 y ]) ≡⟨⟩
toℕ (suc 2[1+ (x + y) ]) ≡⟨ toℕ-suc 2[1+ (x + y) ] ⟩
ℕ.suc (toℕ 2[1+ (x + y) ]) ≡⟨⟩
ℕ.suc (2 ℕ.* (ℕ.suc (toℕ (x + y)))) ≡⟨ cong (λ v → ℕ.suc (2 ℕ.* ℕ.suc v)) (toℕ-homo-+ x y) ⟩
ℕ.suc (2 ℕ.* (ℕ.suc (m ℕ.+ n))) ≡⟨ solve 2 (λ m n → con 1 :+ (con 2 :* (con 1 :+ (m :+ n))) :=
con 2 :* (con 1 :+ m) :+ (con 1 :+ (con 2 :* n)))
refl m n ⟩
(2 ℕ.* ℕ.suc m) ℕ.+ (ℕ.suc (2 ℕ.* n)) ≡⟨⟩
toℕ 2[1+ x ] ℕ.+ toℕ 1+[2 y ] ∎
where open ≡-Reasoning; m = toℕ x; n = toℕ y
toℕ-homo-+ 1+[2 x ] 2[1+ y ] = begin
toℕ (1+[2 x ] + 2[1+ y ]) ≡⟨⟩
toℕ (suc 2[1+ (x + y) ]) ≡⟨ toℕ-suc 2[1+ (x + y) ] ⟩
ℕ.suc (toℕ 2[1+ (x + y) ]) ≡⟨⟩
ℕ.suc (2 ℕ.* (ℕ.suc (toℕ (x + y)))) ≡⟨ cong (ℕ.suc ∘ (2 ℕ.*_) ∘ ℕ.suc) (toℕ-homo-+ x y) ⟩
ℕ.suc (2 ℕ.* (ℕ.suc (m ℕ.+ n))) ≡⟨ solve 2 (λ m n → con 1 :+ (con 2 :* (con 1 :+ (m :+ n))) :=
(con 1 :+ (con 2 :* m)) :+ (con 2 :* (con 1 :+ n)))
refl m n ⟩
(ℕ.suc (2 ℕ.* m)) ℕ.+ (2 ℕ.* (ℕ.suc n)) ≡⟨⟩
toℕ 1+[2 x ] ℕ.+ toℕ 2[1+ y ] ∎
where open ≡-Reasoning; m = toℕ x; n = toℕ y
toℕ-homo-+ 1+[2 x ] 1+[2 y ] = begin
toℕ (1+[2 x ] + 1+[2 y ]) ≡⟨⟩
toℕ (suc 1+[2 (x + y) ]) ≡⟨ toℕ-suc 1+[2 (x + y) ] ⟩
ℕ.suc (toℕ 1+[2 (x + y) ]) ≡⟨⟩
ℕ.suc (ℕ.suc (2 ℕ.* (toℕ (x + y)))) ≡⟨ cong (ℕ.suc ∘ ℕ.suc ∘ (2 ℕ.*_)) (toℕ-homo-+ x y) ⟩
ℕ.suc (ℕ.suc (2 ℕ.* (m ℕ.+ n))) ≡⟨ solve 2 (λ m n → con 1 :+ (con 1 :+ (con 2 :* (m :+ n))) :=
(con 1 :+ (con 2 :* m)) :+ (con 1 :+ (con 2 :* n)))
refl m n ⟩
(ℕ.suc (2 ℕ.* m)) ℕ.+ (ℕ.suc (2 ℕ.* n)) ≡⟨⟩
toℕ 1+[2 x ] ℕ.+ toℕ 1+[2 y ] ∎
where open ≡-Reasoning; m = toℕ x; n = toℕ y
toℕ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℕ.+-rawMagma toℕ
toℕ-isMagmaHomomorphism-+ = record
{ isRelHomomorphism = toℕ-isRelHomomorphism
; homo = toℕ-homo-+
}
toℕ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-0-rawMonoid ℕ.+-0-rawMonoid toℕ
toℕ-isMonoidHomomorphism-+ = record
{ isMagmaHomomorphism = toℕ-isMagmaHomomorphism-+
; ε-homo = refl
}
toℕ-isMonoidMonomorphism-+ : IsMonoidMonomorphism +-0-rawMonoid ℕ.+-0-rawMonoid toℕ
toℕ-isMonoidMonomorphism-+ = record
{ isMonoidHomomorphism = toℕ-isMonoidHomomorphism-+
; injective = toℕ-injective
}
suc≗1+ : suc ≗ 1ᵇ +_
suc≗1+ zero = refl
suc≗1+ 2[1+ _ ] = refl
suc≗1+ 1+[2 _ ] = refl
suc-+ : ∀ x y → suc x + y ≡ suc (x + y)
suc-+ zero y = sym (suc≗1+ y)
suc-+ 2[1+ x ] zero = refl
suc-+ 1+[2 x ] zero = refl
suc-+ 2[1+ x ] 2[1+ y ] = cong (suc ∘ 2[1+_]) (suc-+ x y)
suc-+ 2[1+ x ] 1+[2 y ] = cong (suc ∘ 1+[2_]) (suc-+ x y)
suc-+ 1+[2 x ] 2[1+ y ] = refl
suc-+ 1+[2 x ] 1+[2 y ] = refl
1+≗suc : (1ᵇ +_) ≗ suc
1+≗suc = suc-+ zero
fromℕ'-homo-+ : ∀ m n → fromℕ' (m ℕ.+ n) ≡ fromℕ' m + fromℕ' n
fromℕ'-homo-+ 0 _ = refl
fromℕ'-homo-+ (ℕ.suc m) n = begin
fromℕ' ((ℕ.suc m) ℕ.+ n) ≡⟨⟩
suc (fromℕ' (m ℕ.+ n)) ≡⟨ cong suc (fromℕ'-homo-+ m n) ⟩
suc (a + b) ≡⟨ sym (suc-+ a b) ⟩
(suc a) + b ≡⟨⟩
(fromℕ' (ℕ.suc m)) + (fromℕ' n) ∎
where open ≡-Reasoning; a = fromℕ' m; b = fromℕ' n
fromℕ-homo-+ : ∀ m n → fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n
fromℕ-homo-+ m n rewrite fromℕ≡fromℕ' (m ℕ.+ n) | fromℕ≡fromℕ' m | fromℕ≡fromℕ' n =
fromℕ'-homo-+ m n
private
module +-Monomorphism = MonoidMonomorphism toℕ-isMonoidMonomorphism-+
+-assoc : Associative _+_
+-assoc = +-Monomorphism.assoc ℕ.+-isMagma ℕ.+-assoc
+-comm : Commutative _+_
+-comm = +-Monomorphism.comm ℕ.+-isMagma ℕ.+-comm
+-identityˡ : LeftIdentity zero _+_
+-identityˡ _ = refl
+-identityʳ : RightIdentity zero _+_
+-identityʳ = +-Monomorphism.identityʳ ℕ.+-isMagma ℕ.+-identityʳ
+-identity : Identity zero _+_
+-identity = +-identityˡ , +-identityʳ
+-cancelˡ-≡ : LeftCancellative _+_
+-cancelˡ-≡ = +-Monomorphism.cancelˡ ℕ.+-isMagma ℕ.+-cancelˡ-≡
+-cancelʳ-≡ : RightCancellative _+_
+-cancelʳ-≡ = +-Monomorphism.cancelʳ ℕ.+-isMagma ℕ.+-cancelʳ-≡
+-isMagma : IsMagma _+_
+-isMagma = isMagma _+_
+-isSemigroup : IsSemigroup _+_
+-isSemigroup = +-Monomorphism.isSemigroup ℕ.+-isSemigroup
+-isCommutativeSemigroup : IsCommutativeSemigroup _+_
+-isCommutativeSemigroup = record
{ isSemigroup = +-isSemigroup
; comm = +-comm
}
+-0-isMonoid : IsMonoid _+_ 0ᵇ
+-0-isMonoid = +-Monomorphism.isMonoid ℕ.+-0-isMonoid
+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0ᵇ
+-0-isCommutativeMonoid = +-Monomorphism.isCommutativeMonoid ℕ.+-0-isCommutativeMonoid
+-magma : Magma 0ℓ 0ℓ
+-magma = magma _+_
+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
{ isSemigroup = +-isSemigroup
}
+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
{ isCommutativeSemigroup = +-isCommutativeSemigroup
}
+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
{ ε = zero
; isMonoid = +-0-isMonoid
}
+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
{ isCommutativeMonoid = +-0-isCommutativeMonoid
}
module Bin+CSemigroup = CommSemigProp +-commutativeSemigroup
+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+-mono-≤ {x} {x′} {y} {y′} x≤x′ y≤y′ = begin
x + y ≡⟨ sym $ cong₂ _+_ (fromℕ-toℕ x) (fromℕ-toℕ y) ⟩
fromℕ m + fromℕ n ≡⟨ sym (fromℕ-homo-+ m n) ⟩
fromℕ (m ℕ.+ n) ≤⟨ fromℕ-mono-≤ (ℕ.+-mono-≤ m≤m′ n≤n′) ⟩
fromℕ (m′ ℕ.+ n′) ≡⟨ fromℕ-homo-+ m′ n′ ⟩
fromℕ m′ + fromℕ n′ ≡⟨ cong₂ _+_ (fromℕ-toℕ x′) (fromℕ-toℕ y′) ⟩
x′ + y′ ∎
where
open ≤-Reasoning
m = toℕ x; m′ = toℕ x′
n = toℕ y; n′ = toℕ y′
m≤m′ = toℕ-mono-≤ x≤x′; n≤n′ = toℕ-mono-≤ y≤y′
+-monoˡ-≤ : ∀ x → (_+ x) Preserves _≤_ ⟶ _≤_
+-monoˡ-≤ x y≤z = +-mono-≤ y≤z (≤-refl {x})
+-monoʳ-≤ : ∀ x → (x +_) Preserves _≤_ ⟶ _≤_
+-monoʳ-≤ x y≤z = +-mono-≤ (≤-refl {x}) y≤z
+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
+-mono-<-≤ {x} {x′} {y} {y′} x<x′ y≤y′ = begin-strict
x + y ≡⟨ sym $ cong₂ _+_ (fromℕ-toℕ x) (fromℕ-toℕ y) ⟩
fromℕ m + fromℕ n ≡⟨ sym (fromℕ-homo-+ m n) ⟩
fromℕ (m ℕ.+ n) <⟨ fromℕ-mono-< (ℕ.+-mono-<-≤ m<m′ n≤n′) ⟩
fromℕ (m′ ℕ.+ n′) ≡⟨ fromℕ-homo-+ m′ n′ ⟩
fromℕ m′ + fromℕ n′ ≡⟨ cong₂ _+_ (fromℕ-toℕ x′) (fromℕ-toℕ y′) ⟩
x′ + y′ ∎
where
open ≤-Reasoning
m = toℕ x; n = toℕ y
m′ = toℕ x′; n′ = toℕ y′
m<m′ = toℕ-mono-< x<x′; n≤n′ = toℕ-mono-≤ y≤y′
+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
+-mono-≤-< {x} {x′} {y} {y′} x≤x′ y<y′ = subst₂ _<_ (+-comm y x) (+-comm y′ x′) y+x<y′+x′
where
y+x<y′+x′ = +-mono-<-≤ y<y′ x≤x′
+-monoˡ-< : ∀ x → (_+ x) Preserves _<_ ⟶ _<_
+-monoˡ-< x y<z = +-mono-<-≤ y<z (≤-refl {x})
+-monoʳ-< : ∀ x → (x +_) Preserves _<_ ⟶ _<_
+-monoʳ-< x y<z = +-mono-≤-< (≤-refl {x}) y<z
x≤y+x : ∀ x y → x ≤ y + x
x≤y+x x y = begin
x ≡⟨ sym (+-identityˡ x) ⟩
0ᵇ + x ≤⟨ +-monoˡ-≤ x (0≤x y) ⟩
y + x ∎
where open ≤-Reasoning
x≤x+y : ∀ x y → x ≤ x + y
x≤x+y x y = begin
x ≤⟨ x≤y+x x y ⟩
y + x ≡⟨ +-comm y x ⟩
x + y ∎
where open ≤-Reasoning
x<x+y : ∀ x {y} → y > 0ᵇ → x < x + y
x<x+y x {y} y>0 = begin-strict
x ≡⟨ sym (fromℕ-toℕ x) ⟩
fromℕ (toℕ x) <⟨ fromℕ-mono-< (ℕ.m<m+n (toℕ x) (toℕ-mono-< y>0)) ⟩
fromℕ (toℕ x ℕ.+ toℕ y) ≡⟨ fromℕ-homo-+ (toℕ x) (toℕ y) ⟩
fromℕ (toℕ x) + fromℕ (toℕ y) ≡⟨ cong₂ _+_ (fromℕ-toℕ x) (fromℕ-toℕ y) ⟩
x + y ∎
where open ≤-Reasoning
x<x+1 : ∀ x → x < x + 1ᵇ
x<x+1 x = x<x+y x 0<odd
x<1+x : ∀ x → x < 1ᵇ + x
x<1+x x rewrite +-comm 1ᵇ x = x<x+1 x
x<1⇒x≡0 : x < 1ᵇ → x ≡ zero
x<1⇒x≡0 0<odd = refl
x≢0⇒x+y≢0 : ∀ {x} (y : ℕᵇ) → x ≢ zero → x + y ≢ zero
x≢0⇒x+y≢0 {2[1+ _ ]} zero _ = λ()
x≢0⇒x+y≢0 {zero} _ 0≢0 = contradiction refl 0≢0
private 2*ₙ2*ₙ = (2 ℕ.*_) ∘ (2 ℕ.*_)
toℕ-homo-* : ∀ x y → toℕ (x * y) ≡ toℕ x ℕ.* toℕ y
toℕ-homo-* x y = aux x y (size x ℕ.+ size y) ℕ.≤-refl
where
aux : (x y : ℕᵇ) → (cnt : ℕ) → (size x ℕ.+ size y ℕ.≤ cnt) → toℕ (x * y) ≡ toℕ x ℕ.* toℕ y
aux zero _ _ _ = refl
aux 2[1+ x ] zero _ _ = sym (ℕ.*-zeroʳ (toℕ x ℕ.+ (ℕ.suc (toℕ x ℕ.+ 0))))
aux 1+[2 x ] zero _ _ = sym (ℕ.*-zeroʳ (toℕ x ℕ.+ (toℕ x ℕ.+ 0)))
aux 2[1+ x ] 2[1+ y ] (ℕ.suc cnt) (s≤s |x|+1+|y|≤cnt) = begin
toℕ (2[1+ x ] * 2[1+ y ]) ≡⟨⟩
toℕ (double 2[1+ (x + (y + xy)) ]) ≡⟨ toℕ-double 2[1+ (x + (y + xy)) ] ⟩
2 ℕ.* (toℕ 2[1+ (x + (y + xy)) ]) ≡⟨⟩
2*ₙ2*ₙ (ℕ.suc (toℕ (x + (y + xy)))) ≡⟨ cong (2*ₙ2*ₙ ∘ ℕ.suc) (toℕ-homo-+ x (y + xy)) ⟩
2*ₙ2*ₙ (ℕ.suc (m ℕ.+ (toℕ (y + xy)))) ≡⟨ cong (2*ₙ2*ₙ ∘ ℕ.suc ∘ (m ℕ.+_)) (toℕ-homo-+ y xy) ⟩
2*ₙ2*ₙ (ℕ.suc (m ℕ.+ (n ℕ.+ toℕ xy))) ≡⟨ cong (2*ₙ2*ₙ ∘ ℕ.suc ∘ (m ℕ.+_) ∘ (n ℕ.+_))
(aux x y cnt |x|+|y|≤cnt) ⟩
2*ₙ2*ₙ (ℕ.suc (m ℕ.+ (n ℕ.+ (m ℕ.* n)))) ≡⟨ solve 2 (λ m n → con 2 :* (con 2 :* (con 1 :+ (m :+ (n :+ m :* n)))) :=
(con 2 :* (con 1 :+ m)) :* (con 2 :* (con 1 :+ n)))
refl m n ⟩
(2 ℕ.* (1 ℕ.+ m)) ℕ.* (2 ℕ.* (1 ℕ.+ n)) ≡⟨⟩
toℕ 2[1+ x ] ℕ.* toℕ 2[1+ y ] ∎
where
open ≡-Reasoning; m = toℕ x; n = toℕ y; xy = x * y
|x|+|y|≤cnt = ℕ.≤-trans (ℕ.+-monoʳ-≤ (size x) (ℕ.n≤1+n (size y))) |x|+1+|y|≤cnt
aux 2[1+ x ] 1+[2 y ] (ℕ.suc cnt) (s≤s |x|+1+|y|≤cnt) = begin
toℕ (2[1+ x ] * 1+[2 y ]) ≡⟨⟩
toℕ (2[1+ (x + y * 2[1+ x ]) ]) ≡⟨⟩
2 ℕ.* (ℕ.suc (toℕ (x + y * 2[1+ x ]))) ≡⟨ cong ((2 ℕ.*_) ∘ ℕ.suc) (toℕ-homo-+ x _) ⟩
2 ℕ.* (ℕ.suc (m ℕ.+ (toℕ (y * 2[1+ x ])))) ≡⟨ cong ((2 ℕ.*_) ∘ ℕ.suc ∘ (m ℕ.+_))
(aux y 2[1+ x ] cnt |y|+1+|x|≤cnt) ⟩
2 ℕ.* (1+m ℕ.+ (n ℕ.* (toℕ 2[1+ x ]))) ≡⟨⟩
2 ℕ.* (1+m ℕ.+ (n ℕ.* 2[1+m])) ≡⟨ solve 2 (λ m n →
con 2 :* ((con 1 :+ m) :+ (n :* (con 2 :* (con 1 :+ m)))) :=
(con 2 :* (con 1 :+ m)) :* (con 1 :+ con 2 :* n))
refl m n ⟩
2[1+m] ℕ.* (ℕ.suc (2 ℕ.* n)) ≡⟨⟩
toℕ 2[1+ x ] ℕ.* toℕ 1+[2 y ] ∎
where
open ≡-Reasoning; m = toℕ x; n = toℕ y; 1+m = ℕ.suc m; 2[1+m] = 2 ℕ.* (ℕ.suc m)
eq : size x ℕ.+ (ℕ.suc (size y)) ≡ size y ℕ.+ (ℕ.suc (size x))
eq = ℕ-+-semigroupProperties.x∙yz≈z∙yx (size x) 1 _
|y|+1+|x|≤cnt = subst (ℕ._≤ cnt) eq |x|+1+|y|≤cnt
aux 1+[2 x ] 2[1+ y ] (ℕ.suc cnt) (s≤s |x|+1+|y|≤cnt) = begin
toℕ (1+[2 x ] * 2[1+ y ]) ≡⟨⟩
toℕ 2[1+ (y + x * 2[1+ y ]) ] ≡⟨⟩
2 ℕ.* (ℕ.suc (toℕ (y + x * 2[1+ y ]))) ≡⟨ cong ((2 ℕ.*_) ∘ ℕ.suc)
(toℕ-homo-+ y (x * 2[1+ y ])) ⟩
2 ℕ.* (ℕ.suc (n ℕ.+ (toℕ (x * 2[1+ y ])))) ≡⟨ cong ((2 ℕ.*_) ∘ ℕ.suc ∘ (n ℕ.+_))
(aux x 2[1+ y ] cnt |x|+1+|y|≤cnt) ⟩
2 ℕ.* (1+n ℕ.+ (m ℕ.* toℕ 2[1+ y ])) ≡⟨⟩
2 ℕ.* (1+n ℕ.+ (m ℕ.* 2[1+n])) ≡⟨ solve 2 (λ m n →
con 2 :* ((con 1 :+ n) :+ (m :* (con 2 :* (con 1 :+ n)))) :=
(con 1 :+ (con 2 :* m)) :* (con 2 :* (con 1 :+ n)))
refl m n ⟩
(ℕ.suc 2m) ℕ.* 2[1+n] ≡⟨⟩
toℕ 1+[2 x ] ℕ.* toℕ 2[1+ y ] ∎
where
open ≡-Reasoning
m = toℕ x; n = toℕ y; 1+n = ℕ.suc n
2m = 2 ℕ.* m; 2[1+n] = 2 ℕ.* (ℕ.suc n)
aux 1+[2 x ] 1+[2 y ] (ℕ.suc cnt) (s≤s |x|+1+|y|≤cnt) = begin
toℕ (1+[2 x ] * 1+[2 y ]) ≡⟨⟩
toℕ 1+[2 (x + y * 1+2x) ] ≡⟨⟩
ℕ.suc (2 ℕ.* (toℕ (x + y * 1+2x))) ≡⟨ cong (ℕ.suc ∘ (2 ℕ.*_)) (toℕ-homo-+ x (y * 1+2x)) ⟩
ℕ.suc (2 ℕ.* (m ℕ.+ (toℕ (y * 1+2x)))) ≡⟨ cong (ℕ.suc ∘ (2 ℕ.*_) ∘ (m ℕ.+_))
(aux y 1+2x cnt |y|+1+|x|≤cnt) ⟩
ℕ.suc (2 ℕ.* (m ℕ.+ (n ℕ.* [1+2x]′))) ≡⟨ cong ℕ.suc $ ℕ.*-distribˡ-+ 2 m (n ℕ.* [1+2x]′) ⟩
ℕ.suc (2m ℕ.+ (2 ℕ.* (n ℕ.* [1+2x]′))) ≡⟨ cong (ℕ.suc ∘ (2m ℕ.+_)) (sym (ℕ.*-assoc 2 n _)) ⟩
(ℕ.suc 2m) ℕ.+ 2n ℕ.* [1+2x]′ ≡⟨⟩
[1+2x]′ ℕ.+ 2n ℕ.* [1+2x]′ ≡⟨ cong (ℕ._+ (2n ℕ.* [1+2x]′)) $
sym (ℕ.*-identityˡ [1+2x]′) ⟩
1 ℕ.* [1+2x]′ ℕ.+ 2n ℕ.* [1+2x]′ ≡⟨ sym (ℕ.*-distribʳ-+ [1+2x]′ 1 2n) ⟩
(ℕ.suc 2n) ℕ.* [1+2x]′ ≡⟨ ℕ.*-comm (ℕ.suc 2n) [1+2x]′ ⟩
toℕ 1+[2 x ] ℕ.* toℕ 1+[2 y ] ∎
where
open ≡-Reasoning
m = toℕ x; n = toℕ y; 2m = 2 ℕ.* m; 2n = 2 ℕ.* n
1+2x = 1+[2 x ]; [1+2x]′ = toℕ 1+2x
eq : size x ℕ.+ (ℕ.suc (size y)) ≡ size y ℕ.+ (ℕ.suc (size x))
eq = ℕ-+-semigroupProperties.x∙yz≈z∙yx (size x) 1 _
|y|+1+|x|≤cnt = subst (ℕ._≤ cnt) eq |x|+1+|y|≤cnt
toℕ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℕ.*-rawMagma toℕ
toℕ-isMagmaHomomorphism-* = record
{ isRelHomomorphism = toℕ-isRelHomomorphism
; homo = toℕ-homo-*
}
toℕ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℕ.*-1-rawMonoid toℕ
toℕ-isMonoidHomomorphism-* = record
{ isMagmaHomomorphism = toℕ-isMagmaHomomorphism-*
; ε-homo = refl
}
toℕ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-1-rawMonoid ℕ.*-1-rawMonoid toℕ
toℕ-isMonoidMonomorphism-* = record
{ isMonoidHomomorphism = toℕ-isMonoidHomomorphism-*
; injective = toℕ-injective
}
fromℕ-homo-* : ∀ m n → fromℕ (m ℕ.* n) ≡ fromℕ m * fromℕ n
fromℕ-homo-* m n = begin
fromℕ (m ℕ.* n) ≡⟨ cong fromℕ (cong₂ ℕ._*_ m≡aN n≡bN) ⟩
fromℕ (toℕ a ℕ.* toℕ b) ≡⟨ cong fromℕ (sym (toℕ-homo-* a b)) ⟩
fromℕ (toℕ (a * b)) ≡⟨ fromℕ-toℕ (a * b) ⟩
a * b ∎
where
open ≡-Reasoning
a = fromℕ m; b = fromℕ n
m≡aN = sym (toℕ-fromℕ m); n≡bN = sym (toℕ-fromℕ n)
private
module *-Monomorphism = MonoidMonomorphism toℕ-isMonoidMonomorphism-*
*-assoc : Associative _*_
*-assoc = *-Monomorphism.assoc ℕ.*-isMagma ℕ.*-assoc
*-comm : Commutative _*_
*-comm = *-Monomorphism.comm ℕ.*-isMagma ℕ.*-comm
*-identityˡ : LeftIdentity 1ᵇ _*_
*-identityˡ = *-Monomorphism.identityˡ ℕ.*-isMagma ℕ.*-identityˡ
*-identityʳ : RightIdentity 1ᵇ _*_
*-identityʳ x = trans (*-comm x 1ᵇ) (*-identityˡ x)
*-identity : Identity 1ᵇ _*_
*-identity = (*-identityˡ , *-identityʳ)
*-zeroˡ : LeftZero zero _*_
*-zeroˡ _ = refl
*-zeroʳ : RightZero zero _*_
*-zeroʳ zero = refl
*-zeroʳ 2[1+ _ ] = refl
*-zeroʳ 1+[2 _ ] = refl
*-zero : Zero zero _*_
*-zero = *-zeroˡ , *-zeroʳ
*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ a b c = begin
a * (b + c) ≡⟨ sym (fromℕ-toℕ (a * (b + c))) ⟩
fromℕ (toℕ (a * (b + c))) ≡⟨ cong fromℕ (toℕ-homo-* a (b + c)) ⟩
fromℕ (k ℕ.* (toℕ (b + c))) ≡⟨ cong (fromℕ ∘ (k ℕ.*_)) (toℕ-homo-+ b c) ⟩
fromℕ (k ℕ.* (m ℕ.+ n)) ≡⟨ cong fromℕ (ℕ.*-distribˡ-+ k m n) ⟩
fromℕ (k ℕ.* m ℕ.+ k ℕ.* n) ≡⟨ cong fromℕ $ sym $
cong₂ ℕ._+_ (toℕ-homo-* a b) (toℕ-homo-* a c) ⟩
fromℕ (toℕ (a * b) ℕ.+ toℕ (a * c)) ≡⟨ cong fromℕ (sym (toℕ-homo-+ (a * b) (a * c))) ⟩
fromℕ (toℕ (a * b + a * c)) ≡⟨ fromℕ-toℕ (a * b + a * c) ⟩
a * b + a * c ∎
where open ≡-Reasoning; k = toℕ a; m = toℕ b; n = toℕ c
*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ = comm∧distrˡ⇒distrʳ *-comm *-distribˡ-+
*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+
*-isMagma : IsMagma _*_
*-isMagma = isMagma _*_
*-isSemigroup : IsSemigroup _*_
*-isSemigroup = *-Monomorphism.isSemigroup ℕ.*-isSemigroup
*-1-isMonoid : IsMonoid _*_ 1ᵇ
*-1-isMonoid = *-Monomorphism.isMonoid ℕ.*-1-isMonoid
*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1ᵇ
*-1-isCommutativeMonoid = *-Monomorphism.isCommutativeMonoid ℕ.*-1-isCommutativeMonoid
+-*-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _*_ zero 1ᵇ
+-*-isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-0-isCommutativeMonoid
; *-cong = cong₂ _*_
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
}
+-*-isSemiring : IsSemiring _+_ _*_ zero 1ᵇ
+-*-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = +-*-isSemiringWithoutAnnihilatingZero
; zero = *-zero
}
+-*-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ zero 1ᵇ
+-*-isCommutativeSemiring = record
{ isSemiring = +-*-isSemiring
; *-comm = *-comm
}
*-magma : Magma 0ℓ 0ℓ
*-magma = record
{ isMagma = *-isMagma
}
*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
{ isSemigroup = *-isSemigroup
}
*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
{ isMonoid = *-1-isMonoid
}
*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
{ isCommutativeMonoid = *-1-isCommutativeMonoid
}
+-*-semiring : Semiring 0ℓ 0ℓ
+-*-semiring = record
{ isSemiring = +-*-isSemiring
}
+-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
+-*-commutativeSemiring = record
{ isCommutativeSemiring = +-*-isCommutativeSemiring
}
*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
*-mono-≤ {x} {u} {y} {v} x≤u y≤v = toℕ-cancel-≤ (begin
toℕ (x * y) ≡⟨ toℕ-homo-* x y ⟩
toℕ x ℕ.* toℕ y ≤⟨ ℕ.*-mono-≤ (toℕ-mono-≤ x≤u) (toℕ-mono-≤ y≤v) ⟩
toℕ u ℕ.* toℕ v ≡⟨ sym (toℕ-homo-* u v) ⟩
toℕ (u * v) ∎)
where open ℕ.≤-Reasoning
*-monoʳ-≤ : ∀ x → (x *_) Preserves _≤_ ⟶ _≤_
*-monoʳ-≤ x y≤y′ = *-mono-≤ (≤-refl {x}) y≤y′
*-monoˡ-≤ : ∀ x → (_* x) Preserves _≤_ ⟶ _≤_
*-monoˡ-≤ x y≤y′ = *-mono-≤ y≤y′ (≤-refl {x})
*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
*-mono-< {x} {u} {y} {v} x<u y<v = toℕ-cancel-< (begin-strict
toℕ (x * y) ≡⟨ toℕ-homo-* x y ⟩
toℕ x ℕ.* toℕ y <⟨ ℕ.*-mono-< (toℕ-mono-< x<u) (toℕ-mono-< y<v) ⟩
toℕ u ℕ.* toℕ v ≡⟨ sym (toℕ-homo-* u v) ⟩
toℕ (u * v) ∎)
where open ℕ.≤-Reasoning
*-monoʳ-< : ∀ x → ((1ᵇ + x) *_) Preserves _<_ ⟶ _<_
*-monoʳ-< x {y} {z} y<z = begin-strict
(1ᵇ + x) * y ≡⟨ *-distribʳ-+ y 1ᵇ x ⟩
1ᵇ * y + x * y ≡⟨ cong (_+ x * y) (*-identityˡ y) ⟩
y + x * y <⟨ +-mono-<-≤ y<z (*-monoʳ-≤ x (<⇒≤ y<z)) ⟩
z + x * z ≡⟨ cong (_+ x * z) (sym (*-identityˡ z)) ⟩
1ᵇ * z + x * z ≡⟨ sym (*-distribʳ-+ z 1ᵇ x) ⟩
(1ᵇ + x) * z ∎
where open ≤-Reasoning
*-monoˡ-< : ∀ x → (_* (1ᵇ + x)) Preserves _<_ ⟶ _<_
*-monoˡ-< x {y} {z} y<z = begin-strict
y * (1ᵇ + x) ≡⟨ *-comm y (1ᵇ + x) ⟩
(1ᵇ + x) * y <⟨ *-monoʳ-< x y<z ⟩
(1ᵇ + x) * z ≡⟨ *-comm (1ᵇ + x) z ⟩
z * (1ᵇ + x) ∎
where open ≤-Reasoning
x*y≡0⇒x≡0∨y≡0 : ∀ x {y} → x * y ≡ zero → x ≡ zero ⊎ y ≡ zero
x*y≡0⇒x≡0∨y≡0 zero {_} _ = inj₁ refl
x*y≡0⇒x≡0∨y≡0 _ {zero} _ = inj₂ refl
x≢0∧y≢0⇒x*y≢0 : ∀ {x y} → x ≢ zero → y ≢ zero → x * y ≢ zero
x≢0∧y≢0⇒x*y≢0 {x} {_} x≢0 y≢0 xy≡0 with x*y≡0⇒x≡0∨y≡0 x xy≡0
... | inj₁ x≡0 = x≢0 x≡0
... | inj₂ y≡0 = y≢0 y≡0
2*x≡x+x : ∀ x → 2ᵇ * x ≡ x + x
2*x≡x+x x = begin
2ᵇ * x ≡⟨⟩
(1ᵇ + 1ᵇ) * x ≡⟨ *-distribʳ-+ x 1ᵇ 1ᵇ ⟩
1ᵇ * x + 1ᵇ * x ≡⟨ cong₂ _+_ (*-identityˡ x) (*-identityˡ x) ⟩
x + x ∎
where open ≡-Reasoning
1+-* : ∀ x y → (1ᵇ + x) * y ≡ y + x * y
1+-* x y = begin
(1ᵇ + x) * y ≡⟨ *-distribʳ-+ y 1ᵇ x ⟩
1ᵇ * y + x * y ≡⟨ cong (_+ x * y) (*-identityˡ y) ⟩
y + x * y ∎
where open ≡-Reasoning
*-1+ : ∀ x y → y * (1ᵇ + x) ≡ y + y * x
*-1+ x y = begin
y * (1ᵇ + x) ≡⟨ *-distribˡ-+ y 1ᵇ x ⟩
y * 1ᵇ + y * x ≡⟨ cong (_+ y * x) (*-identityʳ y) ⟩
y + y * x ∎
where open ≡-Reasoning
double[x]≡0⇒x≡0 : double x ≡ zero → x ≡ zero
double[x]≡0⇒x≡0 {zero} _ = refl
x≡0⇒double[x]≡0 : x ≡ 0ᵇ → double x ≡ 0ᵇ
x≡0⇒double[x]≡0 = cong double
x≢0⇒double[x]≢0 : x ≢ zero → double x ≢ zero
x≢0⇒double[x]≢0 x≢0 = x≢0 ∘ double[x]≡0⇒x≡0
double≢1 : double x ≢ 1ᵇ
double≢1 {zero} ()
double≗2* : double ≗ 2ᵇ *_
double≗2* x = toℕ-injective $ begin
toℕ (double x) ≡⟨ toℕ-double x ⟩
2 ℕ.* (toℕ x) ≡⟨ sym (toℕ-homo-* 2ᵇ x) ⟩
toℕ (2ᵇ * x) ∎
where open ≡-Reasoning
double-*-assoc : ∀ x y → (double x) * y ≡ double (x * y)
double-*-assoc x y = begin
(double x) * y ≡⟨ cong (_* y) (double≗2* x) ⟩
(2ᵇ * x) * y ≡⟨ *-assoc 2ᵇ x y ⟩
2ᵇ * (x * y) ≡⟨ sym (double≗2* (x * y)) ⟩
double (x * y) ∎
where open ≡-Reasoning
double[x]≡x+x : ∀ x → double x ≡ x + x
double[x]≡x+x x = trans (double≗2* x) (2*x≡x+x x)
double-distrib-+ : ∀ x y → double (x + y) ≡ double x + double y
double-distrib-+ x y = begin
double (x + y) ≡⟨ double≗2* (x + y) ⟩
2ᵇ * (x + y) ≡⟨ *-distribˡ-+ 2ᵇ x y ⟩
(2ᵇ * x) + (2ᵇ * y) ≡⟨ sym (cong₂ _+_ (double≗2* x) (double≗2* y)) ⟩
double x + double y ∎
where open ≡-Reasoning
double-mono-≤ : double Preserves _≤_ ⟶ _≤_
double-mono-≤ {x} {y} x≤y = begin
double x ≡⟨ double≗2* x ⟩
2ᵇ * x ≤⟨ *-monoʳ-≤ 2ᵇ x≤y ⟩
2ᵇ * y ≡⟨ sym (double≗2* y) ⟩
double y ∎
where open ≤-Reasoning
double-mono-< : double Preserves _<_ ⟶ _<_
double-mono-< {x} {y} x<y = begin-strict
double x ≡⟨ double≗2* x ⟩
2ᵇ * x <⟨ *-monoʳ-< 1ᵇ x<y ⟩
2ᵇ * y ≡⟨ sym (double≗2* y) ⟩
double y ∎
where open ≤-Reasoning
double-cancel-≤ : ∀ {x y} → double x ≤ double y → x ≤ y
double-cancel-≤ {x} {y} 2x≤2y with <-cmp x y
... | tri< x<y _ _ = <⇒≤ x<y
... | tri≈ _ x≡y _ = ≤-reflexive x≡y
... | tri> _ _ x>y = contradiction 2x≤2y (<⇒≱ (double-mono-< x>y))
double-cancel-< : ∀ {x y} → double x < double y → x < y
double-cancel-< {x} {y} 2x<2y with <-cmp x y
... | tri< x<y _ _ = x<y
... | tri≈ _ refl _ = contradiction 2x<2y (<-irrefl refl)
... | tri> _ _ x>y = contradiction (double-mono-< x>y) (<⇒≯ 2x<2y)
x<double[x] : ∀ x → x ≢ zero → x < double x
x<double[x] x x≢0 = begin-strict
x <⟨ x<x+y x (x≢0⇒x>0 x≢0) ⟩
x + x ≡⟨ sym (double[x]≡x+x x) ⟩
double x ∎
where open ≤-Reasoning
x≤double[x] : ∀ x → x ≤ double x
x≤double[x] x = begin
x ≤⟨ x≤x+y x x ⟩
x + x ≡⟨ sym (double[x]≡x+x x) ⟩
double x ∎
where open ≤-Reasoning
double-suc : ∀ x → double (suc x) ≡ 2ᵇ + double x
double-suc x = begin
double (suc x) ≡⟨ cong double (suc≗1+ x) ⟩
double (1ᵇ + x) ≡⟨ double-distrib-+ 1ᵇ x ⟩
2ᵇ + double x ∎
where open ≡-Reasoning
suc≢0 : suc x ≢ zero
suc≢0 {zero} ()
suc≢0 {2[1+ _ ]} ()
suc≢0 {1+[2 _ ]} ()
suc-injective : Injective _≡_ _≡_ suc
suc-injective {zero} {zero} p = refl
suc-injective {zero} {2[1+ y ]} p = contradiction 1+[2 p ]-injective (suc≢0 ∘ sym)
suc-injective {2[1+ x ]} {zero} p = contradiction 1+[2 p ]-injective suc≢0
suc-injective {2[1+ x ]} {2[1+ y ]} p = cong 2[1+_] (suc-injective 1+[2 p ]-injective)
suc-injective {1+[2 x ]} {1+[2 y ]} refl = refl
2[1+_]-double-suc : 2[1+_] ≗ double ∘ suc
2[1+_]-double-suc zero = refl
2[1+_]-double-suc 2[1+ x ] = cong 2[1+_] (2[1+_]-double-suc x)
2[1+_]-double-suc 1+[2 x ] = refl
1+[2_]-suc-double : 1+[2_] ≗ suc ∘ double
1+[2_]-suc-double zero = refl
1+[2_]-suc-double 2[1+ x ] = refl
1+[2_]-suc-double 1+[2 x ] = begin
1+[2 1+[2 x ] ] ≡⟨ cong 1+[2_] (1+[2_]-suc-double x) ⟩
1+[2 (suc 2x) ] ≡⟨⟩
suc 2[1+ 2x ] ≡⟨ cong suc (2[1+_]-double-suc 2x) ⟩
suc (double (suc 2x)) ≡⟨ cong (suc ∘ double) (sym (1+[2_]-suc-double x)) ⟩
suc (double 1+[2 x ]) ∎
where open ≡-Reasoning; 2x = double x
x+suc[y]≡suc[x]+y : ∀ x y → x + suc y ≡ suc x + y
x+suc[y]≡suc[x]+y x y = begin
x + suc y ≡⟨ +-comm x _ ⟩
suc y + x ≡⟨ suc-+ y x ⟩
suc (y + x) ≡⟨ cong suc (+-comm y x) ⟩
suc (x + y) ≡⟨ sym (suc-+ x y) ⟩
suc x + y ∎
where open ≡-Reasoning
0<suc : ∀ x → zero < suc x
0<suc x = x≢0⇒x>0 (suc≢0 {x})
x<suc[x] : ∀ x → x < suc x
x<suc[x] x = begin-strict
x <⟨ x<1+x x ⟩
1ᵇ + x ≡⟨ sym (suc≗1+ x) ⟩
suc x ∎
where open ≤-Reasoning
x≤suc[x] : ∀ x → x ≤ suc x
x≤suc[x] x = <⇒≤ (x<suc[x] x)
x≢suc[x] : ∀ x → x ≢ suc x
x≢suc[x] x = <⇒≢ (x<suc[x] x)
suc-mono-≤ : suc Preserves _≤_ ⟶ _≤_
suc-mono-≤ {x} {y} x≤y = begin
suc x ≡⟨ suc≗1+ x ⟩
1ᵇ + x ≤⟨ +-monoʳ-≤ 1ᵇ x≤y ⟩
1ᵇ + y ≡⟨ sym (suc≗1+ y) ⟩
suc y ∎
where open ≤-Reasoning
suc[x]≤y⇒x<y : ∀ {x y} → suc x ≤ y → x < y
suc[x]≤y⇒x<y {x} (inj₁ sx<y) = <-trans (x<suc[x] x) sx<y
suc[x]≤y⇒x<y {x} (inj₂ refl) = x<suc[x] x
x<y⇒suc[x]≤y : ∀ {x y} → x < y → suc x ≤ y
x<y⇒suc[x]≤y {x} {y} x<y = begin
suc x ≡⟨ sym (fromℕ-toℕ (suc x)) ⟩
fromℕ (toℕ (suc x)) ≡⟨ cong fromℕ (toℕ-suc x) ⟩
fromℕ (ℕ.suc (toℕ x)) ≤⟨ fromℕ-mono-≤ (toℕ-mono-< x<y) ⟩
fromℕ (toℕ y) ≡⟨ fromℕ-toℕ y ⟩
y ∎
where open ≤-Reasoning
suc-* : ∀ x y → suc x * y ≡ y + x * y
suc-* x y = begin
suc x * y ≡⟨ cong (_* y) (suc≗1+ x) ⟩
(1ᵇ + x) * y ≡⟨ 1+-* x y ⟩
y + x * y ∎
where open ≡-Reasoning
*-suc : ∀ x y → x * suc y ≡ x + x * y
*-suc x y = begin
x * suc y ≡⟨ cong (x *_) (suc≗1+ y) ⟩
x * (1ᵇ + y) ≡⟨ *-1+ y x ⟩
x + x * y ∎
where open ≡-Reasoning
x≤suc[y]*x : ∀ x y → x ≤ (suc y) * x
x≤suc[y]*x x y = begin
x ≤⟨ x≤x+y x (y * x) ⟩
x + y * x ≡⟨ sym (suc-* y x) ⟩
(suc y) * x ∎
where open ≤-Reasoning
suc[x]≤double[x] : ∀ x → x ≢ zero → suc x ≤ double x
suc[x]≤double[x] x = x<y⇒suc[x]≤y {x} {double x} ∘ x<double[x] x
suc[x]<2[1+x] : ∀ x → suc x < 2[1+ x ]
suc[x]<2[1+x] x = begin-strict
suc x <⟨ x<double[x] (suc x) suc≢0 ⟩
double (suc x) ≡⟨ sym (2[1+_]-double-suc x) ⟩
2[1+ x ] ∎
where open ≤-Reasoning
double[x]<1+[2x] : ∀ x → double x < 1+[2 x ]
double[x]<1+[2x] x = begin-strict
double x <⟨ x<suc[x] (double x) ⟩
suc (double x) ≡⟨ sym (1+[2_]-suc-double x) ⟩
1+[2 x ] ∎
where open ≤-Reasoning
pred-suc : pred ∘ suc ≗ id
pred-suc zero = refl
pred-suc 2[1+ x ] = sym (2[1+_]-double-suc x)
pred-suc 1+[2 x ] = refl
suc-pred : x ≢ zero → suc (pred x) ≡ x
suc-pred {zero} 0≢0 = contradiction refl 0≢0
suc-pred {2[1+ _ ]} _ = refl
suc-pred {1+[2 x ]} _ = sym (1+[2_]-suc-double x)
pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_
pred-mono-≤ {x} {y} x≤y = begin
pred x ≡⟨ cong pred (sym (fromℕ-toℕ x)) ⟩
pred (fromℕ m) ≡⟨ sym (fromℕ-pred m) ⟩
fromℕ (ℕ.pred m) ≤⟨ fromℕ-mono-≤ (ℕ.pred-mono-≤ (toℕ-mono-≤ x≤y)) ⟩
fromℕ (ℕ.pred n) ≡⟨ fromℕ-pred n ⟩
pred (fromℕ n) ≡⟨ cong pred (fromℕ-toℕ y) ⟩
pred y ∎
where
open ≤-Reasoning; m = toℕ x; n = toℕ y
pred[x]<x : x ≢ zero → pred x < x
pred[x]<x {x} x≢0 = begin-strict
pred x <⟨ x<suc[x] (pred x) ⟩
suc (pred x) ≡⟨ suc-pred x≢0 ⟩
x ∎
where open ≤-Reasoning
pred[x]+y≡x+pred[y] : ∀ {x y} → x ≢ 0ᵇ → y ≢ 0ᵇ → (pred x) + y ≡ x + pred y
pred[x]+y≡x+pred[y] {x} {y} x≢0 y≢0 = begin
px + y ≡⟨ cong (px +_) (sym (suc-pred y≢0)) ⟩
px + suc py ≡⟨ cong (px +_) (suc≗1+ py) ⟩
px + (1ᵇ + py) ≡⟨ Bin+CSemigroup.x∙yz≈yx∙z px 1ᵇ py ⟩
(1ᵇ + px) + py ≡⟨ cong (_+ py) (sym (suc≗1+ px)) ⟩
(suc px) + py ≡⟨ cong (_+ py) (suc-pred x≢0) ⟩
x + py ∎
where open ≡-Reasoning; px = pred x; py = pred y
|x|≡0⇒x≡0 : size x ≡ 0 → x ≡ 0ᵇ
|x|≡0⇒x≡0 {zero} refl = refl
*-+-isSemiringWithoutAnnihilatingZero = +-*-isSemiringWithoutAnnihilatingZero
{-# WARNING_ON_USAGE *-+-isSemiringWithoutAnnihilatingZero
"Warning: *-+-isSemiringWithoutAnnihilatingZero was deprecated in v1.4.
Please use +-*-isSemiringWithoutAnnihilatingZero instead."
#-}
*-+-isSemiring = +-*-isSemiring
{-# WARNING_ON_USAGE *-+-isSemiring
"Warning: *-+-isSemiring was deprecated in v1.4.
Please use +-*-isSemiring instead."
#-}
*-+-isCommutativeSemiring = +-*-isCommutativeSemiring
{-# WARNING_ON_USAGE *-+-isCommutativeSemiring
"Warning: *-+-isCommutativeSemiring was deprecated in v1.4.
Please use +-*-isCommutativeSemiring instead."
#-}
*-+-semiring = +-*-semiring
{-# WARNING_ON_USAGE *-+-semiring
"Warning: *-+-semiring was deprecated in v1.4.
Please use +-*-semiring instead."
#-}
*-+-commutativeSemiring = +-*-commutativeSemiring
{-# WARNING_ON_USAGE *-+-commutativeSemiring
"Warning: *-+-commutativeSemiring was deprecated in v1.4.
Please use +-*-commutativeSemiring instead."
#-}
open Data.Nat.Binary.Base public
using (+-rawMagma; +-0-rawMonoid; *-rawMagma; *-1-rawMonoid)