text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic properties of ℕᵇ
------------------------------------------------------------------------

{-# OPTIONS --without-K --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
open import Data.Nat.Binary.Base
open import Data.Nat as ℕ using (ℕ; z≤n; s≤s)
import Data.Nat.Properties as ℕₚ
open import Data.Nat.Solver
open import Data.Product using (_,_; proj₁; proj₂; ∃)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function using (_∘_; _$_; id)
open import Function.Definitions using (Injective)
open import Function.Definitions.Core2 using (Surjective)
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Morphism
import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism
open import Relation.Binary.PropositionalEquality
import Relation.Binary.Reasoning.Base.Triple as InequalityReasoning
open import Relation.Nullary using (¬_; yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation using (contradiction)

open import Algebra.Definitions {A = ℕᵇ} _≡_
open import Algebra.Structures {A = ℕᵇ} _≡_
import Algebra.Properties.CommutativeSemigroup ℕₚ.+-commutativeSemigroup
  as ℕ-+-semigroupProperties
import Relation.Binary.Construct.StrictToNonStrict _≡_ _<_
  as StrictToNonStrict
open +-*-Solver

------------------------------------------------------------------------
-- Properties of _≡_
------------------------------------------------------------------------

2[1+x]≢0 : ∀ {x} → 2[1+ x ] ≢ 0ᵇ
2[1+x]≢0 ()

1+[2x]≢0 : ∀ {x} → 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

_≟_ : Decidable {A = ℕᵇ} _≡_
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 _≟_

------------------------------------------------------------------------
-- Properties of toℕ & fromℕ
------------------------------------------------------------------------

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

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 _} 1 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ˡ-≡ 1 2xN≡2yN
  x≡y     = toℕ-injective xN≡yN

toℕ-surjective : Surjective _≡_ toℕ
toℕ-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ℕ

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ℕ x))  ≡⟨ cong fromℕ (sym (toℕ-pred x)) ⟩
  fromℕ (toℕ (pred x))    ≡⟨ fromℕ-toℕ (pred x) ⟩
  pred x                  ≡⟨ refl ⟩
  pred (fromℕ n)          ∎
  where open ≡-Reasoning;  x = fromℕ n

x≡0⇒toℕ[x]≡0 : ∀ {x} → x ≡ zero → toℕ x ≡ 0
x≡0⇒toℕ[x]≡0 {zero} _ = refl

toℕ[x]≡0⇒x≡0 : ∀ {x} → toℕ x ≡ 0 → x ≡ zero
toℕ[x]≡0⇒x≡0 {zero} _ = refl

------------------------------------------------------------------------
-- Properties of _<_
------------------------------------------------------------------------
-- Basic properties

x≮0 : ∀ {x} → x ≮ zero
x≮0 ()

x≢0⇒x>0 : ∀ {x} → 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₁

------------------------------------------------------------------------------
-- Properties of _<_ and toℕ & fromℕ.

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)            ≤⟨ ℕₚ.≤-step ℕₚ.≤-refl ⟩
  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 (ℕₚ.≤-step ℕₚ.≤-refl) ⟩
  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ʳ-< 1 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-< (ℕ.≤-pred (ℕₚ.*-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 _)) (ℕₚ.≤-pred 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ˡ-≤ 1 (ℕₚ.+-cancelˡ-≤ 2 x<y)) x≢y)))
toℕ-cancel-< {1+[2 x ]} {1+[2 y ]} x<y =
  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 (ℕ.≤-pred 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-<
  }

------------------------------------------------------------------------------
-- Relational properties of _<_

<-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)

-- Should not be implemented via the morphism `toℕ` in order to
-- preserve O(log n) time requirement.
<-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

------------------------------------------------------------------------------
-- Structures for _<_

<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
  { isEquivalence = isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans
  ; <-resp-≈      = resp₂ _<_
  }

<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
  { isEquivalence = isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

------------------------------------------------------------------------------
-- Bundles for _<_

<-strictPartialOrder : StrictPartialOrder _ _ _
<-strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder
  }

<-strictTotalOrder : StrictTotalOrder _ _ _
<-strictTotalOrder = record
  { isStrictTotalOrder =  <-isStrictTotalOrder
  }

------------------------------------------------------------------------------
-- Other properties of _<_

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)

------------------------------------------------------------------------------
-- Properties of _≤_
------------------------------------------------------------------------------
-- Basic properties

<⇒≱ : _<_ ⇒ _≱_
<⇒≱ 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} → x ≤ zero → x ≡ zero
x≤0⇒x≡0 (inj₂ x≡0) = x≡0

------------------------------------------------------------------------------
-- Properties of _<_ and toℕ & fromℕ.

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-≤
  }

------------------------------------------------------------------------------
-- Relational properties of _≤_

≤-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)

-- Should not be implemented via the morphism `toℕ` in order to
-- preserve O(log n) time requirement.
_≤?_ : 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)

------------------------------------------------------------------------------
-- Structures

≤-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
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

------------------------------------------------------------------------------
-- Bundles

≤-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
  }

------------------------------------------------------------------------------
-- Equational reasoning for _≤_ and _<_

module ≤-Reasoning = InequalityReasoning
  ≤-isPreorder
  <-trans
  (resp₂ _<_) <⇒≤
  <-≤-trans ≤-<-trans
  hiding (step-≈; step-≈˘)

------------------------------------------------------------------------------
-- Properties of _<ℕ_
------------------------------------------------------------------------------

<⇒<ℕ : ∀ {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

------------------------------------------------------------------------
-- Properties of _+_
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Raw bundles for _+_

+-rawMagma : RawMagma 0ℓ 0ℓ
+-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  }

+-0-rawMonoid : RawMonoid 0ℓ 0ℓ
+-0-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _+_
  ; ε   = 0ᵇ
  }

------------------------------------------------------------------------
-- toℕ/fromℕ are homomorphisms for _+_

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

------------------------------------------------------------------------
-- Algebraic properties of _+_

-- Mostly proved by using the isomorphism between `ℕ` and `ℕᵇ` provided
-- by `toℕ`/`fromℕ`.

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ʳ-≡

------------------------------------------------------------------------
-- Structures for _+_

+-isMagma : IsMagma _+_
+-isMagma = isMagma _+_

+-isSemigroup : IsSemigroup _+_
+-isSemigroup = +-Monomorphism.isSemigroup ℕₚ.+-isSemigroup

+-0-isMonoid : IsMonoid _+_ 0ᵇ
+-0-isMonoid = +-Monomorphism.isMonoid ℕₚ.+-0-isMonoid

+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0ᵇ
+-0-isCommutativeMonoid = +-Monomorphism.isCommutativeMonoid ℕₚ.+-0-isCommutativeMonoid

------------------------------------------------------------------------
-- Bundles for _+_

+-magma : Magma 0ℓ 0ℓ
+-magma = magma _+_

+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
  { isSemigroup = +-isSemigroup
  }

+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
  { ε        = zero
  ; isMonoid = +-0-isMonoid
  }

+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
  { isCommutativeMonoid = +-0-isCommutativeMonoid
  }

------------------------------------------------------------------------------
-- Properties of _+_ and _≤_

+-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} → x < 1ᵇ → x ≡ zero
x<1⇒x≡0 0<odd = refl

------------------------------------------------------------------------
-- Other properties

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

------------------------------------------------------------------------
-- Properties of _*_
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Raw bundles for _*_

*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  }

*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
*-1-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  ; ε   = 1ᵇ
  }

------------------------------------------------------------------------
-- toℕ/fromℕ are homomorphisms for _*_

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-*

------------------------------------------------------------------------
-- Algebraic properties of _*_

-- Mostly proved by using the isomorphism between `ℕ` and `ℕᵇ` provided
-- by `toℕ`/`fromℕ`.

*-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ʳ-+

------------------------------------------------------------------------
-- Structures

*-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
  ; *-isMonoid            = *-1-isMonoid
  ; distrib               = *-distrib-+
  }

*-+-isSemiring : IsSemiring _+_ _*_ zero 1ᵇ
*-+-isSemiring = record
  { isSemiringWithoutAnnihilatingZero = *-+-isSemiringWithoutAnnihilatingZero
  ; zero                              = *-zero
  }

*-+-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ zero 1ᵇ
*-+-isCommutativeSemiring = record
  { isSemiring = *-+-isSemiring
  ; *-comm = *-comm
  }

------------------------------------------------------------------------
-- Bundles

*-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
  }

------------------------------------------------------------------------
-- Properties of _*_ and _≤_ & _<_

*-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

------------------------------------------------------------------------
-- Other properties of _*_

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

------------------------------------------------------------------------
-- Properties of double
------------------------------------------------------------------------

double[x]≡0⇒x≡0 : ∀ {x} → double x ≡ zero → x ≡ zero
double[x]≡0⇒x≡0 {zero} _ = refl

x≢0⇒double[x]≢0 : ∀ {x} → x ≢ zero → double x ≢ zero
x≢0⇒double[x]≢0 x≢0 = x≢0 ∘ double[x]≡0⇒x≡0

double≢1 : ∀ {x} → 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

------------------------------------------------------------------------
-- Properties of suc
------------------------------------------------------------------------

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

suc≢0 : ∀ {x} → suc x ≢ zero
suc≢0 {zero}     ()
suc≢0 {2[1+ _ ]} ()
suc≢0 {1+[2 _ ]} ()

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

------------------------------------------------------------------------
-- Properties of pred
------------------------------------------------------------------------

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} → 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} → 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

------------------------------------------------------------------------
-- Properties of size
------------------------------------------------------------------------

|x|≡0⇒x≡0 : ∀ {x} → size x ≡ 0 → x ≡ 0ᵇ
|x|≡0⇒x≡0 {zero} refl =  refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lemmas for use in proving the polynomial homomorphism.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Data.Bool                                  using (Bool;true;false)
open import Data.Nat.Base as ℕ                              using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
open import Data.Nat.Properties as ℕₚ                  using (≤′-trans)
open import Data.Vec.Base as Vec                            using (Vec; _∷_)
open import Data.Fin                                   using (Fin; zero; suc)
open import Data.List                                  using (_∷_; [])
open import Data.Unit using (tt)
open import Data.List.Kleene
open import Data.Product                               using (_,_; proj₁; proj₂; map₁; _×_)
open import Data.Empty                                 using (⊥-elim)
open import Data.Maybe                                 using (nothing; just)
open import Function
open import Level                                      using (lift)
open import Relation.Nullary                           using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open Homomorphism homo hiding (_^_)
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Semantics homo

open import Algebra.Operations.Ring rawRing

------------------------------------------------------------------------
-- Power lemmas
--
-- We prove some things about our odd exponentiation operator (described
-- in Algebra.Operations.Ring.Compact) here.

-- First, that the optimised operator is the same as normal
-- exponentiation.
pow-opt : ∀ x ρ i → x *⟨ ρ ⟩^ i ≈ ρ ^ i * x
pow-opt x ρ ℕ.zero = sym (*-identityˡ x)
pow-opt x ρ (suc i) = refl

-- Some normal identities on exponentiation.
--  xⁿxᵐ = xⁿ⁺ᵐ
pow-add′ : ∀ x i j → (x ^ i +1) * (x ^ j +1) ≈ x ^ (j ℕ.+ suc i) +1
pow-add′ x i ℕ.zero = refl
pow-add′ x i (suc j) =
  begin
    x ^ i +1 * (x ^ j +1 * x)
  ≈⟨ sym (*-assoc _ _ _) ⟩
    x ^ i +1 * x ^ j +1 * x
  ≈⟨ ≪* pow-add′ x i j ⟩
    x ^ (j ℕ.+ suc i) +1 * x
  ∎

pow-add : ∀ x y i j → y ^ j +1 * x *⟨ y ⟩^ i  ≈ x *⟨ y ⟩^ (i ℕ.+ suc j)
pow-add x y ℕ.zero j = refl
pow-add x y (suc i) j = go x y i j
  where
  go : ∀ x y i j → y ^ j +1 * ((y ^ i +1) * x) ≈ y ^ (i ℕ.+ suc j) +1 * x
  go x y ℕ.zero j =  sym (*-assoc _ _ _)
  go x y (suc i) j =
    begin
      y ^ j +1 * (y ^ i +1 * y * x)
    ≈⟨ *≫ *-assoc _ y x ⟩
      y ^ j +1 * (y ^ i +1 * (y * x))
    ≈⟨ go (y * x) y i j ⟩
      y ^ (i ℕ.+ suc j) +1 * (y * x)
    ≈⟨ sym (*-assoc _ y x) ⟩
      y ^ suc (i ℕ.+ suc j) +1 * x
    ∎

-- Here we show a homomorphism on exponentiation, i.e. that using the
-- exponentiation function on polynomials and then evaluating is the same
-- as evaluating and then exponentiating.
pow-hom : ∀ {n} i
        → (xs : Coeff n +)
        → ∀ ρ ρs
        → ⅀⟦ xs ⟧ (ρ , ρs) *⟨ ρ ⟩^ i ≈ ⅀⟦ xs ⍓+ i ⟧ (ρ , ρs)
pow-hom ℕ.zero (x Δ j & xs) ρ ρs rewrite ℕₚ.+-identityʳ j = refl
pow-hom (suc i) (x ≠0 Δ j & xs) ρ ρs =
  begin
    ρ ^ i +1 * (((x , xs) ⟦∷⟧ (ρ , ρs)) *⟨ ρ ⟩^ j)
  ≈⟨ pow-add _ ρ j i ⟩
    (((x , xs) ⟦∷⟧ (ρ , ρs)) *⟨ ρ ⟩^ (j ℕ.+ suc i))
  ∎

-- Proving a congruence (we don't get this for free because we're using
-- setoids).
pow-mul-cong : ∀ {x y} → x ≈ y → ∀ ρ i → x *⟨ ρ ⟩^ i ≈ y *⟨ ρ ⟩^ i
pow-mul-cong x≈y ρ ℕ.zero = x≈y
pow-mul-cong x≈y ρ (suc i₁) = *≫ x≈y

-- The identity:
--  (xy)ⁿ = xⁿyⁿ
pow-distrib-+1 : ∀ x y i → (x * y) ^ i +1 ≈ x ^ i +1 * y ^ i +1
pow-distrib-+1 x y ℕ.zero = refl
pow-distrib-+1 x y (suc i) =
  begin
    (x * y) ^ i +1 * (x * y)
  ≈⟨ ≪* pow-distrib-+1 x y i ⟩
    (x ^ i +1 * y ^ i +1) * (x * y)
  ≈⟨ *-assoc _ _ _ ⟨ trans ⟩ (*≫ (sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* *-comm _ _))) ⟩
    x ^ i +1 * (x * y ^ i +1 * y)
  ≈⟨ (*≫ *-assoc _ _ _) ⟨ trans ⟩ sym (*-assoc _ _ _) ⟩
    (x ^ i +1 * x) * (y ^ i +1 * y)
  ∎

pow-distrib : ∀ x y i → (x * y) ^ i ≈ x ^ i * y ^ i
pow-distrib x y ℕ.zero = sym (*-identityˡ _)
pow-distrib x y (suc i) = pow-distrib-+1 x y i

-- This proves the identity:
--   (xⁿ)ᵐ = xⁿᵐ
-- The reason it looks different is because we're using the special exponentiation
-- operator.
pow-mult-+1 : ∀ x i j → (x ^ i +1) ^ j +1 ≈ x ^ (i ℕ.+ j ℕ.* suc i) +1
pow-mult-+1 x i ℕ.zero rewrite ℕₚ.+-identityʳ i = refl
pow-mult-+1 x i (suc j) =
  begin
    (x ^ i +1) ^ j +1 * (x ^ i +1)
  ≈⟨ ≪* pow-mult-+1 x i j ⟩
    (x ^ (i ℕ.+ j ℕ.* suc i) +1) * (x ^ i +1)
  ≈⟨ pow-add′ x _ i ⟩
    x ^ (i ℕ.+ suc (i ℕ.+ j ℕ.* suc i)) +1
  ∎

pow-cong-+1 : ∀ {x y} i → x ≈ y → x ^ i +1 ≈ y ^ i +1
pow-cong-+1 ℕ.zero x≈y = x≈y
pow-cong-+1 (suc i) x≈y = pow-cong-+1 i x≈y ⟨ *-cong ⟩ x≈y

pow-cong : ∀ {x y} i → x ≈ y → x ^ i ≈ y ^ i
pow-cong ℕ.zero x≈y = refl
pow-cong (suc i) x≈y = pow-cong-+1 i x≈y

-- Demonstrating that the proof of zeroness is correct.
zero-hom : ∀ {n} (p : Poly n) → Zero p → (ρs : Vec Carrier n) → 0# ≈ ⟦ p ⟧ ρs
zero-hom (Κ x  ⊐ i≤n) p≡0 ρs = Zero-C⟶Zero-R x p≡0

--   x¹⁺ⁿ = xxⁿ
pow-suc : ∀ x i → x ^ suc i ≈ x * x ^ i
pow-suc x ℕ.zero  = sym (*-identityʳ _)
pow-suc x (suc i) = *-comm _ _

--   x¹⁺ⁿ = xⁿx
pow-sucʳ : ∀ x i → x ^ suc i ≈ x ^ i * x
pow-sucʳ x ℕ.zero  = sym (*-identityˡ _)
pow-sucʳ x (suc i) = refl

-- In the proper evaluation function, we avoid ever inserting an unnecessary 0#
-- like we do here. However, it is easier to prove with the form that does insert
-- 0#. So we write one here, and then prove that it's equivalent to the one that
-- adds a 0#.
⅀?⟦_⟧ : ∀ {n} (xs : Coeff n *) → Carrier × Vec Carrier n → Carrier
⅀?⟦ []  ⟧ _ = 0#
⅀?⟦ ∹ x ⟧   = ⅀⟦ x ⟧

_⟦∷⟧?_ : ∀ {n} (x : Poly n × Coeff n *) → Carrier × Vec Carrier n → Carrier
(x , xs) ⟦∷⟧? (ρ , ρs) = ρ * ⅀?⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs

⅀?-hom : ∀ {n} (xs : Coeff n +) → ∀ ρ → ⅀?⟦ ∹ xs ⟧ ρ ≈ ⅀⟦ xs ⟧ ρ
⅀?-hom _ _ = refl

⟦∷⟧?-hom : ∀ {n} (x : Poly n) → ∀ xs ρ ρs → (x , xs) ⟦∷⟧? (ρ , ρs) ≈ (x , xs) ⟦∷⟧ (ρ , ρs)
⟦∷⟧?-hom x (∹ xs ) ρ ρs = refl
⟦∷⟧?-hom x [] ρ ρs =  (≪+ zeroʳ _) ⟨ trans ⟩ +-identityˡ _

pow′-hom : ∀ {n} i (xs : Coeff n *) → ∀ ρ ρs → ((⅀?⟦ xs ⟧ (ρ , ρs)) *⟨ ρ ⟩^ i) ≈ (⅀?⟦ xs ⍓* i ⟧ (ρ , ρs))
pow′-hom i (∹ xs ) ρ ρs = pow-hom i xs ρ ρs
pow′-hom zero [] ρ ρs = refl
pow′-hom (suc i) [] ρ ρs = zeroʳ _

-- Here, we show that the normalising cons is correct.
-- This lets us prove with respect to the non-normalising form, especially
-- when we're using the folds.
∷↓-hom-0 : ∀ {n} (x : Poly n) → ∀ xs ρ ρs → ⅀?⟦ x Δ 0 ∷↓ xs ⟧ (ρ , ρs) ≈ (x , xs) ⟦∷⟧ (ρ , ρs)
∷↓-hom-0 x xs      ρ ρs with zero? x
∷↓-hom-0 x xs      ρ ρs | no ¬p = refl
∷↓-hom-0 x []      ρ ρs | yes p = zero-hom x p ρs
∷↓-hom-0 x (∹ xs ) ρ ρs | yes p =
  begin
    ⅀⟦ xs ⍓+ 1 ⟧ (ρ , ρs)
  ≈⟨ sym (pow-hom 1 xs ρ ρs) ⟩
    ρ * ⅀⟦ xs ⟧ (ρ , ρs)
  ≈⟨ sym (+-identityʳ _) ⟨ trans ⟩ (+≫ zero-hom x p ρs) ⟩
    ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
  ∎

∷↓-hom-s : ∀ {n} (x : Poly n) → ∀ i xs ρ ρs → ⅀?⟦ x Δ suc i ∷↓ xs ⟧ (ρ , ρs) ≈ (ρ ^ i +1) * (x , xs) ⟦∷⟧ (ρ , ρs)
∷↓-hom-s x i xs ρ ρs with zero? x
∷↓-hom-s x i xs ρ ρs | no ¬p = refl
∷↓-hom-s x i [] ρ ρs | yes p = sym ((*≫ sym (zero-hom x p ρs)) ⟨ trans ⟩ zeroʳ _)
∷↓-hom-s x i (∹ xs ) ρ ρs | yes p =
  begin
    ⅀⟦ xs ⍓+ (suc (suc i)) ⟧ (ρ , ρs)
  ≈⟨ sym (pow-hom (suc (suc i)) xs ρ ρs) ⟩
    (ρ ^ suc i +1) * ⅀⟦ xs ⟧ (ρ , ρs)
  ≈⟨ *-assoc _ _ _ ⟩
    (ρ ^ i +1) * (ρ * ⅀⟦ xs ⟧ (ρ , ρs))
  ≈⟨ *≫ (sym (+-identityʳ _) ⟨ trans ⟩ (+≫ zero-hom x p ρs)) ⟩
    ρ ^ i +1 * (ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs)
  ∎

∷↓-hom : ∀ {n}
       → (x : Poly n)
       → ∀ i xs ρ ρs
       → ⅀?⟦ x Δ i ∷↓ xs ⟧ (ρ , ρs) ≈ ρ ^ i * ((x , xs) ⟦∷⟧ (ρ , ρs))
∷↓-hom x ℕ.zero  xs ρ ρs = ∷↓-hom-0 x xs ρ ρs ⟨ trans ⟩ sym (*-identityˡ _)
∷↓-hom x (suc i) xs ρ ρs = ∷↓-hom-s x i xs ρ ρs

⟦∷⟧-hom : ∀ {n}
       → (x : Poly n)
       → (xs : Coeff n *)
       → ∀ ρ ρs → (x , xs) ⟦∷⟧ (ρ , ρs) ≈ ρ * ⅀?⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
⟦∷⟧-hom x []     ρ ρs = sym ((≪+ zeroʳ _) ⟨ trans ⟩ +-identityˡ _)
⟦∷⟧-hom x (∹ xs) ρ ρs = refl

-- This proves that injecting a polynomial into more variables is correct.
-- Basically, we show that if a polynomial doesn't care about the first few
-- variables, we can drop them from the input vector.
⅀-⊐↑-hom : ∀ {i n m}
         → (xs : Coeff i +)
         → (si≤n : suc i ≤′ n)
         → (sn≤m : suc n ≤′ m)
         → ∀ ρ
         → ⅀⟦ xs ⟧ (drop-1 (≤′-step si≤n ⟨ ≤′-trans ⟩ sn≤m) ρ)
         ≈ ⅀⟦ xs ⟧ (drop-1 si≤n (proj₂ (drop-1 sn≤m ρ)))
⅀-⊐↑-hom xs si≤n ≤′-refl        (_ ∷ _) = refl
⅀-⊐↑-hom xs si≤n (≤′-step sn≤m) (_ ∷ ρ) = ⅀-⊐↑-hom xs si≤n sn≤m ρ

⊐↑-hom : ∀ {n m}
       → (x : Poly n)
       → (sn≤m : suc n ≤′ m)
       → ∀ ρ
       → ⟦ x ⊐↑ sn≤m ⟧ ρ ≈ ⟦ x ⟧ (proj₂ (drop-1 sn≤m ρ))
⊐↑-hom (Κ x  ⊐ i≤sn) _ _ = refl
⊐↑-hom (⅀ xs ⊐ i≤sn) = ⅀-⊐↑-hom xs i≤sn

trans-join-coeffs-hom : ∀ {i j-1 n}
                      → (i≤j-1 : suc i ≤′ j-1)
                      → (j≤n   : suc j-1 ≤′ n)
                      → (xs : Coeff i +)
                      → ∀ ρ
                      → ⅀⟦ xs ⟧ (drop-1 i≤j-1 (proj₂ (drop-1 j≤n ρ))) ≈ ⅀⟦ xs ⟧ (drop-1 (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) ρ)
trans-join-coeffs-hom i<j-1 ≤′-refl       xs (_ ∷ _) = refl
trans-join-coeffs-hom i<j-1 (≤′-step j<n) xs (_ ∷ ρ) = trans-join-coeffs-hom i<j-1 j<n xs ρ

trans-join-hom : ∀ {i j-1 n}
      → (i≤j-1 : i ≤′ j-1)
      → (j≤n   : suc j-1 ≤′ n)
      → (x : FlatPoly i)
      → ∀ ρ
      → ⟦ x ⊐ i≤j-1 ⟧ (proj₂ (drop-1 j≤n ρ)) ≈ ⟦ x ⊐ (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) ⟧ ρ
trans-join-hom i≤j-1 j≤n (Κ x) _ = refl
trans-join-hom i≤j-1 j≤n (⅀ x) = trans-join-coeffs-hom i≤j-1 j≤n x

⊐↓-hom : ∀ {n m}
       → (xs : Coeff n *)
       → (sn≤m : suc n ≤′ m)
       → ∀ ρ
       → ⟦ xs ⊐↓ sn≤m ⟧ ρ ≈ ⅀?⟦ xs ⟧ (drop-1 sn≤m ρ)
⊐↓-hom []                       sn≤m _ = 0-homo
⊐↓-hom (∹ x₁   Δ zero  & ∹ xs) sn≤m _ = refl
⊐↓-hom (∹ x    Δ suc j & xs )      sn≤m _ = refl
⊐↓-hom (∹ _≠0 x {x≠0} Δ zero  & []) sn≤m ρs =
  let (ρ , ρs′) = drop-1 sn≤m ρs
  in
  begin
    ⟦ x ⊐↑ sn≤m ⟧ ρs
  ≈⟨ ⊐↑-hom x sn≤m ρs ⟩
    ⟦ x ⟧ ρs′
  ∎

drop-1⇒lookup : ∀ {n} (i : Fin n) (ρs : Vec Carrier n) →
                proj₁ (drop-1 (space≤′n i) ρs) ≡ Vec.lookup ρs i
drop-1⇒lookup zero    (ρ ∷ ρs) = ≡.refl
drop-1⇒lookup (suc i) (ρ ∷ ρs) = drop-1⇒lookup i ρs

-- The fold: this function saves us hundreds of lines of proofs in the rest of the
-- homomorphism proof.
-- Many of the functions on polynomials are defined using para: this function allows
-- us to prove properties of those functions (in a foldr-fusion style) *ignoring*
-- optimisations we have made to the polynomial structure.
poly-foldR : ∀ {n} ρ ρs
        → ([f] : Fold n)
        → (f : Carrier → Carrier)
        → (∀ {x y} → x ≈ y → f x ≈ f y)
        → (∀ x y → x * f y ≈ f (x * y))
        → (∀ y {ys} zs → ⅀?⟦ ys ⟧ (ρ , ρs) ≈ f (⅀?⟦ zs ⟧ (ρ , ρs)) → [f] (y , ys) ⟦∷⟧? (ρ , ρs) ≈ f ((y , zs) ⟦∷⟧? (ρ , ρs)) )
        → (f 0# ≈ 0#)
        → ∀ xs
        → ⅀?⟦ para [f] xs ⟧ (ρ , ρs) ≈ f (⅀⟦ xs ⟧ (ρ , ρs))
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ suc i & []) =
  let y,ys = f (x , [])
      y = proj₁ y,ys
      ys = proj₂ y,ys
  in
  begin
    ⅀?⟦ y Δ suc i ∷↓ ys ⟧ (ρ , ρs)
  ≈⟨ ∷↓-hom-s y i ys ρ ρs ⟩
    (ρ ^ i +1) * ((y , ys) ⟦∷⟧ (ρ , ρs))
  ≈˘⟨ *≫ ⟦∷⟧?-hom y ys ρ ρs ⟩
    (ρ ^ i +1) * ((y , ys) ⟦∷⟧? (ρ , ρs))
  ≈⟨ *≫ step x [] (sym base) ⟩
    (ρ ^ i +1) * e ((x , []) ⟦∷⟧? (ρ , ρs))
  ≈⟨ *≫ cng (⟦∷⟧?-hom x [] ρ ρs) ⟩
    (ρ ^ i +1) * e ((x , []) ⟦∷⟧ (ρ , ρs))
  ≈⟨ dist _ _   ⟩
    e (ρ ^ i +1 * ((x , []) ⟦∷⟧ (ρ , ρs)))
  ∎
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ suc i & ∹ xs) =
  let ys = para f xs
      y,zs = f (x , ys)
      y = proj₁ y,zs
      zs = proj₂ y,zs
  in
  begin
    ⅀?⟦ y Δ suc i ∷↓ zs ⟧ (ρ , ρs)
  ≈⟨ ∷↓-hom-s y i zs ρ ρs ⟩
    (ρ ^ i +1) * ((y , zs) ⟦∷⟧ (ρ , ρs))
  ≈˘⟨ *≫ ⟦∷⟧?-hom y zs ρ ρs ⟩
    (ρ ^ i +1) * ((y , zs) ⟦∷⟧? (ρ , ρs))
  ≈⟨ *≫ step x (∹ xs) (poly-foldR ρ ρs f e cng dist step base xs) ⟩
    (ρ ^ i +1) * e ((x , (∹ xs )) ⟦∷⟧? (ρ , ρs))
  ≈⟨ *≫ cng (⟦∷⟧?-hom x (∹ xs ) ρ ρs) ⟩
    (ρ ^ i +1) * e ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs))
  ≈⟨ dist _ _   ⟩
    e (ρ ^ i +1 * ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs)))
  ∎
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ ℕ.zero & []) =
  let y,zs = f (x , [])
      y = proj₁ y,zs
      zs = proj₂ y,zs
  in
  begin
    ⅀?⟦ y Δ ℕ.zero ∷↓ zs ⟧ (ρ , ρs)
  ≈⟨ ∷↓-hom-0 y zs ρ ρs ⟩
    ((y , zs) ⟦∷⟧ (ρ , ρs))
  ≈˘⟨ ⟦∷⟧?-hom y zs ρ ρs ⟩
    ((y , zs) ⟦∷⟧? (ρ , ρs))
  ≈⟨ step x [] (sym base) ⟩
    e ((x , []) ⟦∷⟧? (ρ , ρs))
  ≈⟨ cng (⟦∷⟧?-hom x [] ρ ρs) ⟩
    e ((x , []) ⟦∷⟧ (ρ , ρs))
  ∎
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ ℕ.zero & (∹ xs )) =
  let ys = para f xs
      y,zs = f (x , ys)
      y = proj₁ y,zs
      zs = proj₂ y,zs
  in
  begin
    ⅀?⟦ y Δ ℕ.zero ∷↓ zs ⟧ (ρ , ρs)
  ≈⟨ ∷↓-hom-0 y zs ρ ρs ⟩
    ((y , zs) ⟦∷⟧ (ρ , ρs))
  ≈˘⟨ ⟦∷⟧?-hom y zs ρ ρs ⟩
    ((y , zs) ⟦∷⟧? (ρ , ρs))
  ≈⟨ step x (∹ xs ) (poly-foldR ρ ρs f e cng dist step base xs) ⟩
    e ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs))
  ≈⟨ cng (⟦∷⟧?-hom x (∹ xs ) ρ ρs) ⟩
    e ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs))
  ∎

poly-mapR : ∀ {n} ρ ρs
          → ([f] : Poly n → Poly n)
          → (f : Carrier → Carrier)
          → (∀ {x y} → x ≈ y → f x ≈ f y)
          → (∀ x y → x * f y ≈ f (x * y))
          → (∀ x y → f (x + y) ≈ f x + f y)
          → (∀ y → ⟦ [f] y ⟧ ρs ≈ f (⟦ y ⟧ ρs) )
          → (f 0# ≈ 0#)
          → ∀ xs
          → ⅀?⟦ poly-map [f] xs ⟧ (ρ , ρs) ≈ f (⅀⟦ xs ⟧ (ρ , ρs))
poly-mapR ρ ρs [f] f cng *-dist +-dist step′ base xs = poly-foldR ρ ρs (map₁ [f]) f cng *-dist step base xs
  where
  step : ∀ y {ys} zs → ⅀?⟦ ys ⟧ (ρ , ρs) ≈ f (⅀?⟦ zs ⟧ (ρ , ρs)) →(map₁ [f] (y , ys) ⟦∷⟧? (ρ , ρs)) ≈ f ((y , zs) ⟦∷⟧? (ρ , ρs))
  step y {ys} zs ys≋zs =
    begin
      map₁ [f] (y , ys) ⟦∷⟧? (ρ , ρs)
    ≡⟨⟩
      ρ * ⅀?⟦ ys ⟧ (ρ , ρs) + ⟦ [f] y ⟧ ρs
    ≈⟨ ((*≫ ys≋zs) ⟨ trans ⟩ *-dist ρ _) ⟨ +-cong ⟩ step′ y ⟩
      f (ρ * ⅀?⟦ zs ⟧ (ρ , ρs)) + f (⟦ y ⟧ ρs)
    ≈⟨ sym (+-dist _ _) ⟩
      f ((y , zs) ⟦∷⟧? (ρ , ρs))
    ∎

ext: agda


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Functor.Duality where

open import Level
open import Data.Product using (Σ; _,_)

open import Categories.Category
open import Categories.Category.Construction.Cones as Con
open import Categories.Category.Construction.Cocones as Coc
open import Categories.Functor
open import Categories.Functor.Limits
open import Categories.Object.Initial
open import Categories.Object.Terminal
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Colimit as Col
open import Categories.Diagram.Duality
open import Categories.Morphism.Duality as MorD

private
  variable
    o ℓ e : Level
    C D E J : Category o ℓ e

module _ (G : Functor C D) {J : Category o ℓ e} where
  private
    module C = Category C
    module D = Category D
    module G = Functor G
    module J = Category J

  coPreservesLimit⇒PreservesCoLimit : ∀ {F : Functor J C} (L : Limit (Functor.op F)) →
                                          PreservesLimit G.op L →
                                          PreservesColimit G (coLimit⇒Colimit C L)
  coPreservesLimit⇒PreservesCoLimit L is⊤ = record
    { !        = λ {K} → coCone⇒⇒Cocone⇒ _ (! {Cocone⇒coCone _ K})
    ; !-unique = λ f → !-unique (Cocone⇒⇒coCone⇒ _ f)
    }
    where open IsTerminal is⊤

  PreservesColimit⇒coPreservesLimit : ∀ {F : Functor J C} (L : Colimit F) →
                                        PreservesColimit G L →
                                        PreservesLimit G.op (Colimit⇒coLimit C L)
  PreservesColimit⇒coPreservesLimit L is⊥ = record
    { !        = λ {K} → Cocone⇒⇒coCone⇒ _ (! {coCone⇒Cocone _ K})
    ; !-unique = λ f → !-unique (coCone⇒⇒Cocone⇒ _ f)
    }
    where open IsInitial is⊥

module _ {o ℓ e} (G : Functor C D) where
  private
    module G = Functor G

  coContinuous⇒Cocontinuous : Continuous o ℓ e G.op → Cocontinuous o ℓ e G
  coContinuous⇒Cocontinuous Con L =
    coPreservesLimit⇒PreservesCoLimit G (Colimit⇒coLimit C L) (Con (Colimit⇒coLimit C L))

  Cocontinuous⇒coContinuous : Cocontinuous o ℓ e G → Continuous o ℓ e G.op
  Cocontinuous⇒coContinuous Coc L =
    PreservesColimit⇒coPreservesLimit G (coLimit⇒Colimit C L) (Coc (coLimit⇒Colimit C L))

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sum combinators for setoid equality preserving functions
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Sum.Function.Setoid where

open import Data.Sum
open import Data.Sum.Relation.Binary.Pointwise
open import Relation.Binary
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; _↣_; module Injection)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)

------------------------------------------------------------------------
-- Combinators for equality preserving functions

module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where

  _⊎-⟶_ : (A ⟶ B) → (C ⟶ D) → (A ⊎ₛ C) ⟶ (B ⊎ₛ D)
  _⊎-⟶_ f g = record
    { _⟨$⟩_ = fg
    ; cong  = fg-cong
    }
    where
    open Setoid (A ⊎ₛ C) using () renaming (_≈_ to _≈AC_)
    open Setoid (B ⊎ₛ D) using () renaming (_≈_ to _≈BD_)

    fg = map (_⟨$⟩_ f) (_⟨$⟩_ g)

    fg-cong : _≈AC_ =[ fg ]⇒ _≈BD_
    fg-cong (inj₁ x∼₁y) = inj₁ (F.cong f x∼₁y)
    fg-cong (inj₂ x∼₂y) = inj₂ (F.cong g x∼₂y)

module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} where

  inj₁ₛ : A ⟶ (A ⊎ₛ B)
  inj₁ₛ = record { _⟨$⟩_ = inj₁ ; cong = inj₁ }

  inj₂ₛ : B ⟶ (A ⊎ₛ B)
  inj₂ₛ = record { _⟨$⟩_ = inj₂ ; cong = inj₂ }

  [_,_]ₛ : ∀ {c₁ c₂} {C : Setoid c₁ c₂} →
           (A ⟶ C) → (B ⟶ C) → (A ⊎ₛ B) ⟶ C
  [ f , g ]ₛ = record
    { _⟨$⟩_ = [ f ⟨$⟩_ , g ⟨$⟩_ ]
    ; cong = λ where
      (inj₁ x∼₁y) → F.cong f x∼₁y
      (inj₂ x∼₂y) → F.cong g x∼₂y
    }

module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} where

  swapₛ : (A ⊎ₛ B) ⟶ (B ⊎ₛ A)
  swapₛ = [ inj₂ₛ , inj₁ₛ ]ₛ

------------------------------------------------------------------------
-- Combinators for more complex function types

module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where

  _⊎-equivalence_ : Equivalence A B → Equivalence C D →
                    Equivalence (A ⊎ₛ C) (B ⊎ₛ D)
  A⇔B ⊎-equivalence C⇔D = record
    { to   = to   A⇔B ⊎-⟶ to   C⇔D
    ; from = from A⇔B ⊎-⟶ from C⇔D
    } where open Equivalence

  _⊎-injection_ : Injection A B → Injection C D →
                  Injection (A ⊎ₛ C) (B ⊎ₛ D)
  _⊎-injection_ A↣B C↣D = record
    { to        = to A↣B ⊎-⟶ to C↣D
    ; injective = inj _ _
    }
    where
    open Injection
    open Setoid (A ⊎ₛ C) using () renaming (_≈_ to _≈AC_)
    open Setoid (B ⊎ₛ D) using () renaming (_≈_ to _≈BD_)

    inj : ∀ x y →
          (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ x ≈BD (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ y →
          x ≈AC y
    inj (inj₁ x) (inj₁ y) (inj₁ x∼₁y) = inj₁ (injective A↣B x∼₁y)
    inj (inj₂ x) (inj₂ y) (inj₂ x∼₂y) = inj₂ (injective C↣D x∼₂y)
    -- Can be removed in Agda 2.6.0?
    inj (inj₁ x) (inj₂ y) ()
    inj (inj₂ x) (inj₁ y) ()

  _⊎-left-inverse_ : LeftInverse A B → LeftInverse C D →
                     LeftInverse (A ⊎ₛ C) (B ⊎ₛ D)
  A↞B ⊎-left-inverse C↞D = record
    { to              = Equivalence.to   eq
    ; from            = Equivalence.from eq
    ; left-inverse-of = [ (λ x → inj₁ (left-inverse-of A↞B x))
                        , (λ x → inj₂ (left-inverse-of C↞D x)) ]
    }
    where
    open LeftInverse
    eq = LeftInverse.equivalence A↞B ⊎-equivalence
         LeftInverse.equivalence C↞D

module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
         {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
         {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
         where

  _⊎-surjection_ : Surjection A B → Surjection C D →
                   Surjection (A ⊎ₛ C) (B ⊎ₛ D)
  A↠B ⊎-surjection C↠D = record
    { to         = LeftInverse.from inv
    ; surjective = record
      { from             = LeftInverse.to inv
      ; right-inverse-of = LeftInverse.left-inverse-of inv
      }
    }
    where
    open Surjection
    inv = right-inverse A↠B ⊎-left-inverse right-inverse C↠D

  _⊎-inverse_ : Inverse A B → Inverse C D →
                Inverse (A ⊎ₛ C) (B ⊎ₛ D)
  A↔B ⊎-inverse C↔D = record
    { to         = Surjection.to   surj
    ; from       = Surjection.from surj
    ; inverse-of = record
      { left-inverse-of  = LeftInverse.left-inverse-of inv
      ; right-inverse-of = Surjection.right-inverse-of surj
      }
    }
    where
    open Inverse
    surj = Inverse.surjection   A↔B ⊎-surjection
           Inverse.surjection   C↔D
    inv  = Inverse.left-inverse A↔B ⊎-left-inverse
           Inverse.left-inverse C↔D


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

open import Data.Unit
open import Data.Int as ℤ using (ℤ)
open import Data.List
open import Data.List.Relation.Unary.All as List

module MyTestModule where

emptyList : List ℤ
emptyList = []

empty : List.All (λ (x : ℤ) → ⊤) emptyList
empty = checkProperty record
  { databasePath = DATABASE_PATH
  ; propertyUUID = ????
  }

max_stars_repo_name: Yiergot/vehicle

max_issues_repo_name: Yiergot/vehicle

max_forks_repo_name: Yiergot/vehicle


text:
------------------------------------------------------------------------
-- An investigation of various ways to define the semantics of an
-- untyped λ-calculus and a virtual machine, and a discussion of
-- type soundness and compiler correctness
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module Lambda where

-- Syntax and type system for an untyped λ-calculus.

import Lambda.Syntax

------------------------------------------------------------------------
-- Semantics based on substitutions

-- Substitutions.

import Lambda.Substitution

-- A big-step semantics for the language. Conditional coinduction is
-- used to avoid duplication of rules.
--
-- Cousot and Cousot give a similar definition in "Bi-inductive
-- structural semantics", and their definition inspired this one.
-- Their definition has almost the same rules, but these rules are
-- interpreted in the framework of bi-induction rather than the
-- framework of mixed induction and (conditional) coinduction.

import Lambda.Substitution.OneSemantics

-- Two separate semantics for the language, one for converging terms
-- and the other for diverging terms, as given by Leroy and Grall in
-- "Coinductive big-step operational semantics".
--
-- Leroy and Grall attempted to unify their two semantics into a
-- single one, using only coinduction, but failed to find a definition
-- which was equivalent to the two that they started with. However,
-- they aimed for a definition which did not have more rules than the
-- definition for converging terms; the definition in OneSemantics
-- does not satisfy this criterion.

import Lambda.Substitution.TwoSemantics

-- The two definitions are equivalent.

import Lambda.Substitution.Equivalence

-- A functional semantics, along with a type soundness proof.

import Lambda.Substitution.Functional

------------------------------------------------------------------------
-- Virtual machine

-- A virtual machine with two semantics (one relational and one
-- functional), a compiler from the λ-calculus defined above into the
-- language of the virtual machine, and a proof showing that the two
-- semantics are equivalent.

import Lambda.VirtualMachine

------------------------------------------------------------------------
-- Semantics based on closures

-- A semantics for the untyped λ-calculus, based on closures and
-- environments, as given by Leroy and Grall in "Coinductive big-step
-- operational semantics" (more or less).
--
-- The module also contains a proof which shows that the compiler in
-- Lambda.VirtualMachine preserves the semantics (assuming that the
-- virtual machine is deterministic). Leroy and Grall prove almost the
-- same thing. In their proof they use a relation indexed by a natural
-- number to work around limitations in Coq's productivity checker.
-- Agda has similar limitations, but I work around them using mixed
-- induction/coinduction, which in my opinion is more elegant. I am
-- not sure if my workaround would work in Coq, though.

import Lambda.Closure.Relational

-- A semantics for the untyped λ-calculus which uses the partiality
-- monad, along with another compiler correctness proof. An advantage
-- of formulating the semantics in this way is that it is very easy to
-- state compiler correctness.

import Lambda.Closure.Functional

-- The module above uses some workarounds in order to convince Agda
-- that the code is productive. The following module contains (more or
-- less) the same code without the workarounds, but is checked with
-- the termination checker turned off.

import Lambda.Closure.Functional.No-workarounds

-- The relational and functional semantics are equivalent.

import Lambda.Closure.Equivalence

-- An alternative definition of the functional semantics. This
-- definition uses continuation-passing style instead of bind.

import Lambda.Closure.Functional.Alternative

-- A definition of a type system (with recursive types) for the
-- λ-calculus given above, and a proof of type soundness for the
-- functional semantics.

import Lambda.Closure.Functional.Type-soundness

-- A very brief treatment of different kinds of term equivalences,
-- including contextual equivalence and applicative bisimilarity.

import Lambda.Closure.Equivalences

-- A functional semantics, a compiler and a compiler correctness
-- proof, and a type soundness proof for a non-deterministic untyped
-- λ-calculus with constants.

import Lambda.Closure.Functional.Non-deterministic

-- A variant of the code above without the workarounds used to
-- convince Agda that the code is productive.

import Lambda.Closure.Functional.Non-deterministic.No-workarounds

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Show using (show)
open import Function using (_$!_)
open import IO using (run; putStrLn)

sum : ℕ
sum = f 1000000000 0
  where
  f : ℕ → ℕ → ℕ
  f zero    acc = acc
  f (suc n) acc = f n $! suc n + acc

main = run (putStrLn (show sum))


text:
{-# OPTIONS --without-K --rewriting #-}

module HoTT where

open import lib.Basics public

open import lib.Equivalence2 public
open import lib.NConnected public
open import lib.NType2 public
open import lib.Relation2 public
open import lib.Function2 public

open import lib.cubical.Cubical public
open import lib.types.Types public
open import lib.groups.Groups public
open import lib.groupoids.Groupoids public
open import lib.modalities.Modalities public

{-
To use coinduction in the form of [∞], [♭] and [♯] you can do:

open import HoTT
open Coinduction

You can also use coinductive records and copatterns instead, that’s prettier
(see experimental/GlobularTypes.agda for an example)
-}
module Coinduction where
  open import lib.Coinduction public

-- deprecated operators
module _ where
  infix 15 _∎
  _∎ = _=∎
  conn-elim = conn-extend
  conn-elim-β = conn-extend-β
  conn-elim-general = conn-extend-general
  conn-intro = conn-in

  if_then_else_ : ∀ {i} {A : Type i}
    → Bool → A → A → A
  if true then t else e = t
  if false then t else e = e

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module StreamPredicates where

open import PropsAsTypes
open import Stream

module Modalities (A : Set) where

  private
    Aω : Set
    Aω = Stream A

  record Always (P : Pred Aω) (s : Stream A) : Prop where
    coinductive
    field
      valid : P s
      step : Always P (tl s)
  open Always public

  data Eventually (P : Pred Aω) (s : Stream A) : Prop where
    now : P s → Eventually P s
    later : Eventually P (tl s) → Eventually P s

  GE : Pred Aω → Pred Aω
  GE P = Always (Eventually P)

  EG : Pred Aω → Pred Aω
  EG P = Eventually (Always P)

  Always⇒GE : ∀{P : Pred Aω} → Always P ⊆ GE P
  Always⇒GE s p .valid = now (p .valid)
  Always⇒GE s p .step  = Always⇒GE (s .tl) (p .step)

  EG⇒Eventually : ∀{P : Pred Aω} → EG P ⊆ Eventually P
  EG⇒Eventually s (now p)      = now (p .valid)
  EG⇒Eventually s (later Evs') = later (EG⇒Eventually (s .tl) Evs')

  EG⇒GE : ∀{P : Pred Aω} → EG P ⊆ GE P
  EG⇒GE s p         .valid = EG⇒Eventually s p
  EG⇒GE s (now p)   .step  = Always⇒GE (tl s) (p .step)
  EG⇒GE s (later p) .step  = EG⇒GE (tl s) p

module ModalitiesExamples where
  open import Data.Nat
  open import Relation.Binary.PropositionalEquality as PE

  exP : Pred (Stream ℕ)
  exP s = s .hd ≡ 0

  alt : Stream ℕ
  alt .hd     = 0
  alt .tl .hd = 1
  alt .tl .tl = alt

  open Modalities ℕ

  exP-holds-on-alt-GE : GE exP alt
  exP-holds-on-alt-GE .valid       = now refl
  exP-holds-on-alt-GE .step .valid = later (now refl)
  exP-holds-on-alt-GE .step .step  = exP-holds-on-alt-GE

  exP-holds-not-on-alt-EG : ¬ (EG exP alt)
  exP-holds-not-on-alt-EG (now p)         = zero-not-suc 0 (p .step .valid)
  exP-holds-not-on-alt-EG (later (now p)) = zero-not-suc 0 (p .valid)
  exP-holds-not-on-alt-EG (later (later EGalt'')) =
    exP-holds-not-on-alt-EG EGalt''

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{-# OPTIONS --universe-polymorphism #-}
-- in a lot of cases we have a relation that is already reflexive and symmetric
-- and we want to make it symmetric
module Categories.Support.ZigZag where

open import Level
open import Relation.Binary
open import Relation.Binary.Construct.On using () renaming (isEquivalence to on-preserves-equivalence)

open import Categories.Support.Equivalence using () renaming (Setoid to ISetoid; module Setoid to ISetoid)

data Direction : Set where
  ↘ ↗ : Direction

rotate : Direction → Direction
rotate ↘ = ↗
rotate ↗ = ↘

data ZigZag′ {c ℓ₂} {Carrier : Set c} (_∼_ : Carrier -> Carrier -> Set ℓ₂) : (x y : Carrier) (begin end : Direction) → Set (c ⊔ ℓ₂) where
  zig : ∀ {x y z e} (first : x ∼ y) (rest : ZigZag′ _∼_ y z ↗ e) → ZigZag′ _∼_ x z ↘ e
  zag : ∀ {x y z e} (first : y ∼ x) (rest : ZigZag′ _∼_ y z ↘ e) → ZigZag′ _∼_ x z ↗ e
  slish : ∀ {x y} (last : x ∼ y) → ZigZag′ _∼_ x y ↘ ↘
  slash : ∀ {x y} (last : y ∼ x) → ZigZag′ _∼_ x y ↗ ↗

ZigZag : ∀ {c ℓ₁ ℓ₂} (Base : Preorder c ℓ₁ ℓ₂) → (x y : Preorder.Carrier Base) (begin end : Direction) → Set (c ⊔ ℓ₂)
ZigZag Base = ZigZag′ (Preorder._∼_ Base)

zz-sym′ : ∀ {c ℓ₁ ℓ₂} {Base : Preorder c ℓ₁ ℓ₂} {x y z begin middle end} → ZigZag Base y z middle end → ZigZag Base y x middle begin → ZigZag Base z x (rotate end) begin
zz-sym′ {Base = Base} (zig first rest) accum = zz-sym′ {Base = Base} rest (zag first accum)
zz-sym′ {Base = Base} (zag first rest) accum = zz-sym′ {Base = Base} rest (zig first accum)
zz-sym′ (slish last) accum = zag last accum
zz-sym′ (slash last) accum = zig last accum

zz-sym : ∀ {c ℓ₁ ℓ₂} {Base : Preorder c ℓ₁ ℓ₂} {x y begin end} → ZigZag Base x y begin end → ZigZag Base y x (rotate end) (rotate begin)
zz-sym {Base = Base} (zig first rest) = zz-sym′ {Base = Base} rest (slash first)
zz-sym {Base = Base} (zag first rest) = zz-sym′ {Base = Base} rest (slish first)
zz-sym (slish last) = slash last
zz-sym (slash last) = slish last

zz-trans : ∀ {c ℓ₁ ℓ₂} {Base : Preorder c ℓ₁ ℓ₂} {x y z begin end begin′ end′} → ZigZag Base x y begin end → ZigZag Base y z begin′ end′ → ZigZag Base x z begin end′
zz-trans {Base = Base} (zig first rest) yz = zig first (zz-trans {Base = Base} rest yz)
zz-trans {Base = Base} (zag first rest) yz = zag first (zz-trans {Base = Base} rest yz)
zz-trans {Base = Base} (slish last) (zig first rest) = zig (Preorder.trans Base last first) rest
zz-trans (slish last) (zag first rest) = zig last (zag first rest)
zz-trans {Base = Base} (slish last) (slish only) = slish (Preorder.trans Base last only)
zz-trans (slish last) (slash only) = zig last (slash only)
zz-trans (slash last) (zig first rest) = zag last (zig first rest)
zz-trans {Base = Base} (slash last) (zag first rest) = zag (Preorder.trans Base first last) rest
zz-trans (slash last) (slish only) = zag last (slish only)
zz-trans {Base = Base} (slash last) (slash only) = slash (Preorder.trans Base only last)

data Alternating′ {c ℓ₂} {Carrier : Set c} (_∼_ : Carrier -> Carrier -> Set ℓ₂) (x y : Carrier) : Set (c ⊔ ℓ₂) where
  disorient : ∀ {begin end} (zz : ZigZag′ _∼_ x y begin end) → Alternating′ _∼_ x y

Alternating : ∀ {c ℓ₁ ℓ₂} (Base : Preorder c ℓ₁ ℓ₂) → (x y : Preorder.Carrier Base) → Set (c ⊔ ℓ₂)
Alternating Base = Alternating′ (Preorder._∼_ Base)

is-equivalence : ∀ {c ℓ₁ ℓ₂} (Base : Preorder c ℓ₁ ℓ₂) → IsEquivalence (Alternating Base)
is-equivalence Base = record
  { refl = disorient (slash (Base.refl))
  ; sym = my-sym
  ; trans = my-trans
  }
  where
  module Base = Preorder Base
  my-sym : ∀ {i j} → Alternating Base i j → Alternating Base j i
  my-sym (disorient zz) = disorient (zz-sym {Base = Base} zz)
  my-trans : ∀ {i j k} → Alternating Base i j → Alternating Base j k → Alternating Base i k
  my-trans (disorient ij) (disorient jk) = disorient (zz-trans {Base = Base} ij jk)

setoid : ∀ {c ℓ₁ ℓ₂} (Base : Preorder c ℓ₁ ℓ₂) → Setoid c (c ⊔ ℓ₂)
setoid Base = record
  { Carrier = Preorder.Carrier Base
  ; _≈_ = Alternating Base
  ; isEquivalence = is-equivalence Base }

isetoid : ∀ {c ℓ₁ ℓ₂} (Base : Preorder c ℓ₁ ℓ₂) → ISetoid c (c ⊔ ℓ₂)
isetoid Base = record
  { Carrier = Preorder.Carrier Base
  ; _≈_ = Alternating Base
  ; isEquivalence = is-equivalence Base }

-- the main eliminators for Alternating -- they prove that any equivalence that
-- respects the base preorder also respects its Alternating completion.

locally-minimal : ∀ {c ℓ₁ ℓ₂ ℓ′} (Base : Preorder c ℓ₁ ℓ₂) {_≈_ : Rel (Preorder.Carrier Base) ℓ′} (≈-isEquivalence : IsEquivalence _≈_) → (Preorder._∼_ Base ⇒ _≈_) → (Alternating Base ⇒ _≈_)
locally-minimal Base {_≋_} isEq inj (disorient zz) = impl zz
  where
  open IsEquivalence isEq renaming (trans to _>trans>_)

  impl : ∀ {i j b e} → ZigZag Base i j b e → i ≋ j
  impl (zig first rest) = inj first >trans> impl rest
  impl (zag first rest) = sym (inj first) >trans> impl rest
  impl (slish last) = inj last
  impl (slash last) = sym (inj last)

minimal : ∀ {c ℓ₁ ℓ₂ c′ ℓ′} (Base : Preorder c ℓ₁ ℓ₂) (Dest : Setoid c′ ℓ′) (f : Preorder.Carrier Base → Setoid.Carrier Dest) → (Preorder._∼_ Base =[ f ]⇒ Setoid._≈_ Dest) → (Alternating Base =[ f ]⇒ Setoid._≈_ Dest)
minimal Base Dest f inj = locally-minimal Base (on-preserves-equivalence f (Setoid.isEquivalence Dest)) inj

.iminimal : ∀ {c ℓ₁ ℓ₂ c′ ℓ′} (Base : Preorder c ℓ₁ ℓ₂) (Dest : ISetoid c′ ℓ′) (f : Preorder.Carrier Base → ISetoid.Carrier Dest) → (Preorder._∼_ Base =[ f ]⇒ ISetoid._≈_ Dest) → (Alternating Base =[ f ]⇒ ISetoid._≈_ Dest)
iminimal Base Dest f inj = locally-minimal Base (on-preserves-equivalence f (ISetoid.isEquivalence Dest)) inj

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Category.Groupoid where

open import Algebra.Category.Category
open import Core

-- A groupoid is a category where all morphisms are isomorphisms.

record Groupoid {c h r} : Set (lsuc (c ⊔ h ⊔ r)) where
  field category : Category {c} {h} {r}
  open Category category public

  field iso : ∀ {A B} (f : Hom A B) → Iso f
  open module MyIso {A B} (f : Hom A B) = Iso (iso f) public
       using (inv; left-inv; right-inv; inv-unique)

  field
    inv-cong : ∀ {A B} {f g : Hom A B} → f ≈ g → inv f ≈ inv g

  -- The inverse function is an involution.
  inv-invol : ∀ {A B} {f : Hom A B} → inv (inv f) ≈ f
  inv-invol {f = f} =
    begin
      inv (inv f)               ≈[ sym (right-id _) ]
      inv (inv f) ∘ id          ≈[ ∘-cong refl (sym (left-inv _)) ]
      inv (inv f) ∘ (inv f ∘ f) ≈[ sym (assoc _ _ _) ]
      (inv (inv f) ∘ inv f) ∘ f ≈[ ∘-cong (left-inv _) refl ]
      id ∘ f                    ≈[ left-id _ ]
      f
    qed

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module Data.Num.Pred where

open import Data.Num.Core
open import Data.Num
open import Data.Num.Properties
open import Data.Num.Continuous
-- open import Data.Num.Bijection

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra
open import Data.Fin using (Fin; suc; zero; #_)
open import Data.Vec
open import Data.Product hiding (map)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable using (True; fromWitness; toWitness)

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

-- infixl 6 _∔_
infixl 6 _∔_

data Term : ℕ → Set where
    var : ∀ {n} → Fin n → Term n
    _∔_ : ∀ {n} → Term n → Term n → Term n

data Predicate : ℕ → Set where
    -- equality
    _≋P_ : ∀ {n} → (t₁ : Term n) → (t₂ : Term n) → Predicate n
    -- implication
    _→P_ : ∀ {n} → (p₁ : Predicate n) → (p₂ : Predicate n) → Predicate n
    -- ∀, introduces new variable
    ∀P : ∀ {n} → (p : Predicate (suc n)) → Predicate n

record Signature : Set₁ where
    constructor sig
    field
        carrier : Set
        _⊕_ : carrier → carrier → carrier
        _≈_ : carrier → carrier → Set

open Signature

ℕ-sig : Signature
ℕ-sig = sig ℕ _+_ _≡_

Numeral-sig : (b d : ℕ) → True (Continuous? b d 0) → Signature
Numeral-sig b d cont = sig (Numeral b d 0) (_⊹_ {cont = cont}) _≋_

-- BijN-sig : ℕ → Signature
-- BijN-sig b = sig (BijN b) (_⊹_ {surj = fromWitness (BijN⇒Surjective b)}) _≡_
--

Env : Set → ℕ → Set
Env = Vec

-- the decoder
⟦_⟧T : ∀ {n}
    → Term n
    → (sig : Signature)
    → Vec (carrier sig) n
    → carrier sig
⟦ var i         ⟧T _                env = lookup i env
⟦ term₁ ∔ term₂ ⟧T (sig A _⊕_ _≈_) env = ⟦ term₁ ⟧T (sig A _⊕_ _≈_) env ⊕ ⟦ term₂ ⟧T (sig A _⊕_ _≈_) env

⟦_⟧P : ∀ {n}
    → Predicate n
    → (sig : Signature)
    → Env (carrier sig) n
    → Set
⟦ t₁ ≋P t₂ ⟧P (sig carrier _⊕_ _≈_) env
    = ⟦ t₁ ⟧T (sig carrier _⊕_ _≈_) env ≈ ⟦ t₂ ⟧T (sig carrier _⊕_ _≈_) env
⟦ p →P q   ⟧P signature env = ⟦ p ⟧P signature env → ⟦ q ⟧P signature env
⟦ ∀P pred  ⟧P signature env = ∀ x → ⟦ pred ⟧P signature (x ∷ env)

module Example-1 where
    ≋-trans : Predicate zero
    ≋-trans = let   x = var (# 0)
                    y = var (# 1)
                    z = var (# 2)
        in ∀P (∀P (∀P (((x ≋P y) →P (y ≋P z)) →P (x ≋P z))))

    ≋-trans-ℕ : Set
    ≋-trans-ℕ = ⟦ ≋-trans ⟧P ℕ-sig []

    ≋-trans-Numeral : (b d : ℕ) → True (Continuous? b d 0) → Set
    ≋-trans-Numeral b d prop = ⟦ ≋-trans ⟧P (Numeral-sig b d prop) []

-- lemma for env
lookup-map : ∀ {i j} → {A : Set i} {B : Set j}
           → (f : A → B) →
           ∀ {n} → (xs : Vec A n) (i : Fin n)
           → lookup i (map f xs) ≡ f (lookup i xs)
lookup-map f []       ()
lookup-map f (x ∷ xs) zero    = refl
lookup-map f (x ∷ xs) (suc i) = lookup-map f xs i

-- ------------------------------------------------------------------------
-- -- toℕ : preserving structures of terms and predicates
-- ------------------------------------------------------------------------

toℕ-term-homo : ∀ {b d n}
    → (cont : True (Continuous? b d 0))
    → (t : Term n)
    → (env : Vec (Numeral b d 0) n)
    → ⟦ t ⟧T ℕ-sig (map ⟦_⟧ env) ≡ ⟦ ⟦ t ⟧T (Numeral-sig b d cont) env ⟧
toℕ-term-homo     cont (var i)   env = lookup-map ⟦_⟧ env i
toℕ-term-homo {b} {d} cont (t₁ ∔ t₂) env
    rewrite toℕ-term-homo cont t₁ env | toℕ-term-homo cont t₂ env
    = sym (toℕ-⊹-homo cont (⟦ t₁ ⟧T (Numeral-sig b d cont) env) (⟦ t₂ ⟧T (Numeral-sig b d cont) env))

mutual
    toℕ-pred-ℕ⇒Numeral : ∀ {b d n}
        → (cont : True (Continuous? b (suc d) 0))
        → (pred : Predicate n)
        → (env : Vec (Numeral b (suc d) 0) n)
        → ⟦ pred ⟧P ℕ-sig (map ⟦_⟧ env)
        → ⟦ pred ⟧P (Numeral-sig b (suc d) cont) env
    toℕ-pred-ℕ⇒Numeral {b} {d} cont (t₁ ≋P t₂) env sem-ℕ =
        begin
            ⟦ ⟦ t₁ ⟧T (Numeral-sig b (suc d) cont) env ⟧
        ≡⟨ sym (toℕ-term-homo cont t₁ env) ⟩
            ⟦ t₁ ⟧T ℕ-sig (map ⟦_⟧ env)
        ≡⟨ sem-ℕ ⟩
            ⟦ t₂ ⟧T ℕ-sig (map ⟦_⟧ env)
        ≡⟨ toℕ-term-homo cont t₂ env ⟩
            ⟦ ⟦ t₂ ⟧T (Numeral-sig b (suc d) cont) env ⟧
        ∎
    toℕ-pred-ℕ⇒Numeral cont (p →P q) env sem-ℕ ⟦p⟧P-Numeral =
        toℕ-pred-ℕ⇒Numeral cont q env
            (sem-ℕ (toℕ-pred-Numeral⇒ℕ cont p env ⟦p⟧P-Numeral))
    toℕ-pred-ℕ⇒Numeral cont (∀P pred) env sem-ℕ x =
        toℕ-pred-ℕ⇒Numeral cont pred (x ∷ env) (sem-ℕ ⟦ x ⟧)

    toℕ-pred-Numeral⇒ℕ : ∀ {b d n}
        → (cont : True (Continuous? b (suc d) 0))
        → (pred : Predicate n)
        → (env : Vec (Numeral b (suc d) 0) n)
        → ⟦ pred ⟧P (Numeral-sig b (suc d) cont) env
        → ⟦ pred ⟧P ℕ-sig (map ⟦_⟧ env)
    toℕ-pred-Numeral⇒ℕ {b} {d} cont (t₁ ≋P t₂) env sem-Num =
        begin
            ⟦ t₁ ⟧T ℕ-sig (map ⟦_⟧ env)
        ≡⟨ toℕ-term-homo cont t₁ env ⟩
            ⟦ ⟦ t₁ ⟧T (Numeral-sig b (suc d) cont) env ⟧
        ≡⟨ sem-Num ⟩
            ⟦ ⟦ t₂ ⟧T (Numeral-sig b (suc d) cont) env ⟧
        ≡⟨ sym (toℕ-term-homo cont t₂ env) ⟩
            ⟦ t₂ ⟧T ℕ-sig (map ⟦_⟧ env)
        ∎
    toℕ-pred-Numeral⇒ℕ cont (p →P q) env sem-Num ⟦p⟧P
        = toℕ-pred-Numeral⇒ℕ cont q env
            (sem-Num
                (toℕ-pred-ℕ⇒Numeral cont p env ⟦p⟧P))
    toℕ-pred-Numeral⇒ℕ {b} {d} cont (∀P pred) env sem-Num n with n ≟ ⟦ fromℕ {cont = cont} n z≤n ⟧
    toℕ-pred-Numeral⇒ℕ {b} {d} cont (∀P pred) env sem-Num n | yes eq
        rewrite eq
        = toℕ-pred-Numeral⇒ℕ cont pred (fromℕ {cont = cont} n _ ∷ env) (sem-Num (fromℕ {cont = cont} n _))
    toℕ-pred-Numeral⇒ℕ {b} {d} cont (∀P pred) env sem-Num n | no ¬eq
        = contradiction (sym (fromℕ-toℕ cont n _)) ¬eq

module Example-2 where

    +-comm-Predicate : Predicate 0
    +-comm-Predicate = ∀P (∀P ((var (# 1) ∔ var (# 0)) ≋P (var (# 0) ∔ var (# 1))))

    +-comm-ℕ : ∀ a b → a + b ≡ b + a
    +-comm-ℕ = +-comm

    +-comm-Num : ∀ {b d}
        → {cont : True (Continuous? b (suc d) 0)}
        → (xs ys : Numeral b (suc d) 0)
        → (_⊹_ {cont = cont} xs ys) ≋ (_⊹_ {cont = cont} ys xs)
    +-comm-Num {cont = cont} = toℕ-pred-ℕ⇒Numeral cont +-comm-Predicate [] +-comm-ℕ
--
-- mutual
--     toℕ-pred-ℕ⇒Bij : ∀ {b n}
--                 → (pred : Predicate n)
--                 → (env  : Vec (Bij (suc b)) n)
--                 → ⟦ pred ⟧ ℕ-sig            (map toℕ env)
--                 → ⟦ pred ⟧ (BijN-sig (suc b)) env
--     toℕ-pred-ℕ⇒Bij {b} (t₁ ≋ t₂) env ⟦t₁≈t₂⟧ℕ
--         rewrite toℕ-term-homo t₁ env | toℕ-term-homo t₂ env -- ⟦ t₁ ⟧T ℕ-sig (map toℕ env) ≡ toℕ (⟦ t₁ ⟧T (Bij-sig (suc b)) env)
--         = toℕ-injective (⟦ t₁ ⟧T (BijN-sig (suc b)) env) (⟦ t₂ ⟧T (BijN-sig (suc b)) env) ⟦t₁≈t₂⟧ℕ
--     toℕ-pred-ℕ⇒Bij (p ⇒ q)   env ⟦p→q⟧ℕ ⟦p⟧B = toℕ-pred-ℕ⇒Bij q env (⟦p→q⟧ℕ (toℕ-pred-Bij⇒ℕ p env ⟦p⟧B))
--     toℕ-pred-ℕ⇒Bij (All p)   env ⟦λx→p⟧ℕ x = toℕ-pred-ℕ⇒Bij p (x ∷ env) (⟦λx→p⟧ℕ (toℕ x))
--
--     toℕ-pred-Bij⇒ℕ : ∀ {b n}
--                 → (pred : Predicate n)
--                 → (env  : Vec (Bij (suc b)) n)
--                 → ⟦ pred ⟧ (BijN-sig (suc b)) env
--                 → ⟦ pred ⟧ ℕ-sig             (map toℕ env)
--     toℕ-pred-Bij⇒ℕ (t₁ ≋ t₂) env ⟦t₁≈t₂⟧B
--         rewrite toℕ-term-homo t₁ env | toℕ-term-homo t₂ env
--         = cong toℕ ⟦t₁≈t₂⟧B
--     toℕ-pred-Bij⇒ℕ (p ⇒ q) env ⟦p→q⟧B ⟦p⟧ℕ = toℕ-pred-Bij⇒ℕ q env (⟦p→q⟧B (toℕ-pred-ℕ⇒Bij p env ⟦p⟧ℕ))
--     toℕ-pred-Bij⇒ℕ {b} (All p) env ⟦λx→p⟧B x
--         rewrite (sym (toℕ-fromℕ b x)) -- rewritting "x" to "toℕ (fromℕ x)"
--         = toℕ-pred-Bij⇒ℕ p (fromℕ x ∷ env) (⟦λx→p⟧B (fromℕ x))

-- fromℕ-term-homo : ∀ {b n}
--     → (term : Term n)
--     → (env : Vec ℕ n)
--     → ⟦ term ⟧T (Bij-sig (suc b)) (map fromℕ env) ≡ fromℕ (⟦ term ⟧T ℕ-sig env)
-- fromℕ-term-homo         (var i)   env = lookup-map fromℕ env i
-- fromℕ-term-homo {b} {n} (t₁ ∔ t₂) env
--     rewrite fromℕ-term-homo {b} {n} t₁ env | fromℕ-term-homo {b} {n} t₂ env
--     = sym (fromℕ-⊹-homo (⟦ t₁ ⟧T (sig ℕ _+_ _≡_) env) (⟦ t₂ ⟧T (sig ℕ _+_ _≡_) env))
--
--
-- ------------------------------------------------------------------------
--
-- open import Data.Nat.Properties.Simple
--
--
-- testExtract : {pred : Predicate 0}
--         → ⟦ pred ⟧ ℕ-sig []
--         → Predicate 0
-- testExtract {pred} ⟦pred⟧ℕ = pred
--
-- ∔-comm : Predicate 0
-- ∔-comm = testExtract {All (All (var (suc zero) ∔ var zero ≋ var zero ∔ var (suc zero)))} +-comm
--
-- ∔-assoc : Predicate 0
-- ∔-assoc = testExtract {All (All (All (var (suc (suc zero)) ∔ var (suc zero) ∔ var zero ≋ var (suc (suc zero)) ∔ (var (suc zero) ∔ var zero))))} +-assoc
-- ∔-assoc = testExtract {All (All (All (var (suc (suc zero)) ∔ var (suc zero) ∔ var zero ≋ var (suc (suc zero)) ∔ (var (suc zero) ∔ var zero))))} +-assoc

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --cubical #-}
module Multidimensional.Data.DirNum.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Nat

open import Multidimensional.Data.Dir

-- Dependent "directional numerals":
-- for natural n, obtain 2ⁿ "numerals".
-- This is basically a little-endian binary notation.
-- NOTE: Would an implementation of DirNum with dependent vectors be preferable
--       over using products?
DirNum : ℕ → Type₀
DirNum zero = Unit
DirNum (suc n) = Dir × (DirNum n)

DirNum→ℕ : ∀ {n} → DirNum n → ℕ
DirNum→ℕ {zero} tt = zero
DirNum→ℕ {suc n} (↓ , d) = doublesℕ (suc zero) (DirNum→ℕ d)
DirNum→ℕ {suc n} (↑ , d) = suc (doublesℕ (suc zero) (DirNum→ℕ d))

-- give the next numeral, cycling back to 0
-- in case of 2ⁿ - 1
next : ∀ {n} → DirNum n → DirNum n
next {zero} tt = tt
next {suc n} (↓ , ds) = (↑ , ds)
next {suc n} (↑ , ds) = (↓ , next ds)

prev : ∀ {n} → DirNum n → DirNum n
prev {zero} tt = tt
prev {suc n} (↓ , ds) = (↓ , prev ds)
prev {suc n} (↑ , ds) = (↓ , ds)

zero-n : (n : ℕ) → DirNum n
zero-n zero = tt
zero-n (suc n) = (↓ , zero-n n)

one-n : (n : ℕ) → DirNum n
one-n zero = tt
one-n (suc n) = (↑ , zero-n n)

-- numeral for 2ⁿ - 1
max-n : (n : ℕ) → DirNum n
max-n zero = tt
max-n (suc n) = (↑ , max-n n)

-- -- TODO: rename
-- embed-next : (r : ℕ) → DirNum r → DirNum (suc r)
-- embed-next zero tt = (↓ , tt)
-- embed-next (suc r) (d , ds) with zero-n? ds
-- ... | no _ = (d , embed-next r ds)
-- ... | yes _ = (d , zero-n (suc r))

sucDoubleDirNum+ : (r : ℕ) → DirNum r → DirNum (suc r)
sucDoubleDirNum+ r x = (↑ , x)

-- bad name, since this is doubling "to" suc r
doubleDirNum+ : (r : ℕ) → DirNum r → DirNum (suc r)
doubleDirNum+ r x = (↓ , x)

dropLeast : {r : ℕ} → DirNum (suc r) → DirNum r
dropLeast {zero} d = tt
dropLeast {suc r} (x , x₁) = x₁

dropMost : {r : ℕ} → DirNum (suc r) → DirNum r
dropMost {zero} d = tt
dropMost {suc zero} (x , (x₁ , x₂)) = (x₁ , x₂)
dropMost {suc (suc r)} (x , x₁) = (x , dropMost x₁)

-- need to prove property about doubleable
--doubleDirNum : (r : ℕ) (d : DirNum r) → doubleable-n? {r} d ≡ true → DirNum r
-- bad? is not correct when not "doubleable"
-- possibly should view as operations in residue classes?
doubleDirNum : (r : ℕ) (d : DirNum r) → DirNum r
doubleDirNum zero d  = tt
doubleDirNum (suc r) d  = doubleDirNum+ r (dropMost {r} d)
-- doubleDirNum zero d doubleable = ⊥-elim (false≢true doubleable)
-- doubleDirNum (suc r) d doubleable = doubleDirNum+ r (dropMost {r} d)

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional