text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about integers
------------------------------------------------------------------------

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

module Data.Integer.Properties where

open import Algebra
import Algebra.Morphism as Morphism
import Algebra.Properties.AbelianGroup
open import Data.Integer.Base renaming (suc to sucℤ)
open import Data.Nat as ℕ
  using (ℕ; suc; zero; _∸_; s≤s; z≤n)
  hiding (module ℕ)
import Data.Nat.Properties as ℕₚ
open import Data.Nat.Solver
open import Data.Product using (proj₁; proj₂; _,_)
open import Data.Sum as Sum using (inj₁; inj₂)
open import Data.Sign as Sign using () renaming (_*_ to _𝕊*_)
import Data.Sign.Properties as 𝕊ₚ
open import Function using (_∘_; _$_)
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
import Relation.Binary.Reasoning.PartialOrder as POR
import Relation.Binary.Reasoning.Preorder as PreR
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
import Relation.Nullary.Decidable as Dec

open import Algebra.FunctionProperties {A = ℤ} _≡_
open import Algebra.FunctionProperties.Consequences.Propositional
open import Algebra.Structures {A = ℤ} _≡_
module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_
module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_
open +-*-Solver

------------------------------------------------------------------------
-- Equality

+-injective : ∀ {m n} → + m ≡ + n → m ≡ n
+-injective refl = refl

-[1+-injective : ∀ {m n} → -[1+ m ] ≡ -[1+ n ] → m ≡ n
-[1+-injective refl = refl

infix 4 _≟_
_≟_ : Decidable {A = ℤ} _≡_
+ m      ≟ + n      = Dec.map′ (cong (+_)) +-injective (m ℕ.≟ n)
+ m      ≟ -[1+ n ] = no λ()
-[1+ m ] ≟ + n      = no λ()
-[1+ m ] ≟ -[1+ n ] = Dec.map′ (cong -[1+_]) -[1+-injective (m ℕ.≟ n)

≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid _≟_

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

neg-involutive : ∀ n → - - n ≡ n
neg-involutive (+ zero)   = refl
neg-involutive (+ suc n)  = refl
neg-involutive (-[1+ n ]) = refl

neg-injective : ∀ {m n} → - m ≡ - n → m ≡ n
neg-injective {m} {n} -m≡-n = begin
  m     ≡⟨ sym (neg-involutive m) ⟩
  - - m ≡⟨ cong -_ -m≡-n ⟩
  - - n ≡⟨ neg-involutive n ⟩
  n ∎ where open ≡-Reasoning

neg-suc : ∀ m → - + suc m ≡ pred (- + m)
neg-suc zero    = refl
neg-suc (suc m) = refl

------------------------------------------------------------------------
-- Properties of ∣_∣

∣n∣≡0⇒n≡0 : ∀ {n} → ∣ n ∣ ≡ 0 → n ≡ + 0
∣n∣≡0⇒n≡0 {+ .zero}   refl = refl
∣n∣≡0⇒n≡0 { -[1+ n ]} ()

∣-n∣≡∣n∣ : ∀ n → ∣ - n ∣ ≡ ∣ n ∣
∣-n∣≡∣n∣ (+ zero)   = refl
∣-n∣≡∣n∣ (+ suc n)  = refl
∣-n∣≡∣n∣ (-[1+ n ]) = refl

0≤n⇒+∣n∣≡n : ∀ {n} → + 0 ≤ n → + ∣ n ∣ ≡ n
0≤n⇒+∣n∣≡n (+≤+ 0≤n) = refl

+∣n∣≡n⇒0≤n : ∀ {n} → + ∣ n ∣ ≡ n → + 0 ≤ n
+∣n∣≡n⇒0≤n {+ n} _ = +≤+ z≤n
+∣n∣≡n⇒0≤n { -[1+ n ]} ()

------------------------------------------------------------------------
-- Properties of sign and _◃_

◃-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
◃-inverse -[1+ n ]  = refl
◃-inverse (+ zero)  = refl
◃-inverse (+ suc n) = refl

◃-cong : ∀ {i j} → sign i ≡ sign j → ∣ i ∣ ≡ ∣ j ∣ → i ≡ j
◃-cong {i} {j} sign-≡ abs-≡ = begin
  i               ≡⟨ sym $ ◃-inverse i ⟩
  sign i ◃ ∣ i ∣  ≡⟨ cong₂ _◃_ sign-≡ abs-≡ ⟩
  sign j ◃ ∣ j ∣  ≡⟨ ◃-inverse j ⟩
  j               ∎ where open ≡-Reasoning

+◃n≡+n : ∀ n → Sign.+ ◃ n ≡ + n
+◃n≡+n zero    = refl
+◃n≡+n (suc _) = refl

-◃n≡-n : ∀ n → Sign.- ◃ n ≡ - + n
-◃n≡-n zero    = refl
-◃n≡-n (suc _) = refl

sign-◃ : ∀ s n → sign (s ◃ suc n) ≡ s
sign-◃ Sign.- _ = refl
sign-◃ Sign.+ _ = refl

abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
abs-◃ _      zero    = refl
abs-◃ Sign.- (suc n) = refl
abs-◃ Sign.+ (suc n) = refl

signₙ◃∣n∣≡n : ∀ n → sign n ◃ ∣ n ∣ ≡ n
signₙ◃∣n∣≡n (+ n)      = +◃n≡+n n
signₙ◃∣n∣≡n (-[1+ n ]) = refl

sign-cong : ∀ {s₁ s₂ n₁ n₂} →
            s₁ ◃ suc n₁ ≡ s₂ ◃ suc n₂ → s₁ ≡ s₂
sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  s₁                  ≡⟨ sym $ sign-◃ s₁ n₁ ⟩
  sign (s₁ ◃ suc n₁)  ≡⟨ cong sign eq ⟩
  sign (s₂ ◃ suc n₂)  ≡⟨ sign-◃ s₂ n₂ ⟩
  s₂                  ∎ where open ≡-Reasoning

abs-cong : ∀ {s₁ s₂ n₁ n₂} → s₁ ◃ n₁ ≡ s₂ ◃ n₂ → n₁ ≡ n₂
abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  n₁           ≡⟨ sym $ abs-◃ s₁ n₁ ⟩
  ∣ s₁ ◃ n₁ ∣  ≡⟨ cong ∣_∣ eq ⟩
  ∣ s₂ ◃ n₂ ∣  ≡⟨ abs-◃ s₂ n₂ ⟩
  n₂           ∎ where open ≡-Reasoning

∣s◃m∣*∣t◃n∣≡m*n : ∀ s t m n → ∣ s ◃ m ∣ ℕ.* ∣ t ◃ n ∣ ≡ m ℕ.* n
∣s◃m∣*∣t◃n∣≡m*n s t m n = cong₂ ℕ._*_ (abs-◃ s m) (abs-◃ t n)

◃-≡ : ∀ {m n} → sign m ≡ sign n → ∣ m ∣ ≡ ∣ n ∣ → m ≡ n
◃-≡ {+ m}       {+ n }      ≡-sign ≡-abs = cong ℤ.pos ≡-abs
◃-≡ { -[1+ m ]} { -[1+ n ]} ≡-sign ≡-abs = cong -[1+_] (ℕₚ.suc-injective ≡-abs)
◃-≡ {+ m}       { -[1+ n ]} ()     ≡-abs
◃-≡ { -[1+ m ]} {+ n }      ()     ≡-abs

------------------------------------------------------------------------
-- Properties of _⊖_

n⊖n≡0 : ∀ n → n ⊖ n ≡ + 0
n⊖n≡0 zero    = refl
n⊖n≡0 (suc n) = n⊖n≡0 n

⊖-swap : ∀ a b → a ⊖ b ≡ - (b ⊖ a)
⊖-swap zero    zero    = refl
⊖-swap (suc _) zero    = refl
⊖-swap zero    (suc _) = refl
⊖-swap (suc a) (suc b) = ⊖-swap a b

⊖-≥ : ∀ {m n} → m ℕ.≥ n → m ⊖ n ≡ + (m ∸ n)
⊖-≥ z≤n         = refl
⊖-≥ (ℕ.s≤s n≤m) = ⊖-≥ n≤m

⊖-< : ∀ {m n} → m ℕ.< n → m ⊖ n ≡ - + (n ∸ m)
⊖-< {zero}  (ℕ.s≤s z≤n) = refl
⊖-< {suc m} (ℕ.s≤s m<n) = ⊖-< m<n

⊖-≰ : ∀ {m n} → n ℕ.≰ m → m ⊖ n ≡ - + (n ∸ m)
⊖-≰ = ⊖-< ∘ ℕₚ.≰⇒>

∣⊖∣-< : ∀ {m n} → m ℕ.< n → ∣ m ⊖ n ∣ ≡ n ∸ m
∣⊖∣-< {zero}  (ℕ.s≤s z≤n) = refl
∣⊖∣-< {suc n} (ℕ.s≤s m<n) = ∣⊖∣-< m<n

∣⊖∣-≰ : ∀ {m n} → n ℕ.≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m
∣⊖∣-≰ = ∣⊖∣-< ∘ ℕₚ.≰⇒>

sign-⊖-< : ∀ {m n} → m ℕ.< n → sign (m ⊖ n) ≡ Sign.-
sign-⊖-< {zero}  (ℕ.s≤s z≤n) = refl
sign-⊖-< {suc n} (ℕ.s≤s m<n) = sign-⊖-< m<n

sign-⊖-≰ : ∀ {m n} → n ℕ.≰ m → sign (m ⊖ n) ≡ Sign.-
sign-⊖-≰ = sign-⊖-< ∘ ℕₚ.≰⇒>

-[n⊖m]≡-m+n : ∀ m n → - (m ⊖ n) ≡ (- (+ m)) + (+ n)
-[n⊖m]≡-m+n zero    zero    = refl
-[n⊖m]≡-m+n zero    (suc n) = refl
-[n⊖m]≡-m+n (suc m) zero    = refl
-[n⊖m]≡-m+n (suc m) (suc n) = sym (⊖-swap n m)

∣m⊖n∣≡∣n⊖m∣ : ∀ x y → ∣ x ⊖ y ∣ ≡ ∣ y ⊖ x ∣
∣m⊖n∣≡∣n⊖m∣ zero    zero    = refl
∣m⊖n∣≡∣n⊖m∣ zero    (suc _) = refl
∣m⊖n∣≡∣n⊖m∣ (suc _) zero    = refl
∣m⊖n∣≡∣n⊖m∣ (suc x) (suc y) = ∣m⊖n∣≡∣n⊖m∣ x y

+-cancelˡ-⊖ : ∀ a b c → (a ℕ.+ b) ⊖ (a ℕ.+ c) ≡ b ⊖ c
+-cancelˡ-⊖ zero    b c = refl
+-cancelˡ-⊖ (suc a) b c = +-cancelˡ-⊖ a b c

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

+-comm : Commutative _+_
+-comm -[1+ a ] -[1+ b ] = cong (-[1+_] ∘ suc) (ℕₚ.+-comm a b)
+-comm (+   a ) (+   b ) = cong +_ (ℕₚ.+-comm a b)
+-comm -[1+ _ ] (+   _ ) = refl
+-comm (+   _ ) -[1+ _ ] = refl

+-identityˡ : LeftIdentity (+ 0) _+_
+-identityˡ -[1+ _ ] = refl
+-identityˡ (+   _ ) = refl

+-identityʳ : RightIdentity (+ 0) _+_
+-identityʳ = comm+idˡ⇒idʳ +-comm +-identityˡ

+-identity : Identity (+ 0) _+_
+-identity = +-identityˡ , +-identityʳ

distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ.+ a ⊖ c
distribˡ-⊖-+-pos _ zero    zero    = refl
distribˡ-⊖-+-pos _ zero    (suc _) = refl
distribˡ-⊖-+-pos _ (suc _) zero    = refl
distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c

distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ.+ a)
distribˡ-⊖-+-neg _ zero    zero    = refl
distribˡ-⊖-+-neg _ zero    (suc _) = refl
distribˡ-⊖-+-neg _ (suc _) zero    = refl
distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c

distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ.+ b ⊖ c
distribʳ-⊖-+-pos a b c = begin
  + a + (b ⊖ c) ≡⟨ +-comm (+ a) (b ⊖ c) ⟩
  (b ⊖ c) + + a ≡⟨ distribˡ-⊖-+-pos a b c ⟩
  b ℕ.+ a ⊖ c   ≡⟨ cong (_⊖ c) (ℕₚ.+-comm b a) ⟩
  a ℕ.+ b ⊖ c   ∎ where open ≡-Reasoning

distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ.+ c)
distribʳ-⊖-+-neg a b c = begin
  -[1+ a ] + (b ⊖ c) ≡⟨ +-comm -[1+ a ] (b ⊖ c) ⟩
  (b ⊖ c) + -[1+ a ] ≡⟨ distribˡ-⊖-+-neg a b c ⟩
  b ⊖ suc (c ℕ.+ a)  ≡⟨ cong (λ x → b ⊖ suc x) (ℕₚ.+-comm c a) ⟩
  b ⊖ suc (a ℕ.+ c)  ∎ where open ≡-Reasoning

suc-+ : ∀ m n → + suc m + n ≡ sucℤ (+ m + n)
suc-+ m (+ n)      = refl
suc-+ m (-[1+ n ]) = sym (distribʳ-⊖-+-pos 1 m (suc n))

pos-+-commute : ℕtoℤ.Homomorphic₂ +_ ℕ._+_ _+_
pos-+-commute zero    n = refl
pos-+-commute (suc m) n = cong sucℤ (pos-+-commute m n)

+-assoc : Associative _+_
+-assoc (+ zero) y z rewrite +-identityˡ      y  | +-identityˡ (y + z) = refl
+-assoc x (+ zero) z rewrite +-identityʳ  x      | +-identityˡ      z  = refl
+-assoc x y (+ zero) rewrite +-identityʳ (x + y) | +-identityʳ  y      = refl
+-assoc -[1+ a ]  -[1+ b ]  (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
+-assoc -[1+ a ]  (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
+-assoc (+ suc a) -[1+ b ]  -[1+ c ]  = distribˡ-⊖-+-neg c a b
+-assoc (+ suc a) -[1+ b ] (+ suc c)
  rewrite distribˡ-⊖-+-pos (suc c) a b
        | distribʳ-⊖-+-pos (suc a) c b
        | sym (ℕₚ.+-assoc a 1 c)
        | ℕₚ.+-comm a 1
        = refl
+-assoc (+ suc a) (+ suc b) -[1+ c ]
  rewrite distribʳ-⊖-+-pos (suc a) b c
        | sym (ℕₚ.+-assoc a 1 b)
        | ℕₚ.+-comm a 1
        = refl
+-assoc -[1+ a ] -[1+ b ] -[1+ c ]
  rewrite sym (ℕₚ.+-assoc a 1 (b ℕ.+ c))
        | ℕₚ.+-comm a 1
        | ℕₚ.+-assoc a b c
        = refl
+-assoc -[1+ a ] (+ suc b) -[1+ c ]
  rewrite distribʳ-⊖-+-neg a b c
        | distribˡ-⊖-+-neg c b a
        = refl
+-assoc (+ suc a) (+ suc b) (+ suc c)
  rewrite ℕₚ.+-assoc (suc a) (suc b) (suc c)
        = refl

suc-pred : ∀ m → sucℤ (pred m) ≡ m
suc-pred m = begin
  sucℤ (pred m) ≡⟨ sym (+-assoc (+ 1) (- + 1) m) ⟩
  + 0 + m       ≡⟨ +-identityˡ m ⟩
  m ∎ where open ≡-Reasoning

pred-suc : ∀ m → pred (sucℤ m) ≡ m
pred-suc m = begin
  pred (sucℤ m) ≡⟨ sym (+-assoc (- + 1) (+ 1) m) ⟩
  + 0 + m       ≡⟨ +-identityˡ m ⟩
  m ∎ where open ≡-Reasoning

+-pred : ∀ m n → m + pred n ≡ pred (m + n)
+-pred m n = begin
  m + (-[1+ 0 ] + n) ≡⟨ sym (+-assoc m -[1+ 0 ] n) ⟩
  m + -[1+ 0 ] + n   ≡⟨ cong (_+ n) (+-comm m -[1+ 0 ]) ⟩
  -[1+ 0 ] + m + n   ≡⟨ +-assoc -[1+ 0 ] m n ⟩
  -[1+ 0 ] + (m + n) ∎ where open ≡-Reasoning

pred-+ : ∀ m n → pred m + n ≡ pred (m + n)
pred-+ m n = begin
  pred m + n   ≡⟨ +-comm (pred m) n ⟩
  n + pred m   ≡⟨ +-pred n m ⟩
  pred (n + m) ≡⟨ cong pred (+-comm n m) ⟩
  pred (m + n) ∎ where open ≡-Reasoning

+-inverseˡ : LeftInverse (+ 0) -_ _+_
+-inverseˡ -[1+ n ]  = n⊖n≡0 n
+-inverseˡ (+ zero)  = refl
+-inverseˡ (+ suc n) = n⊖n≡0 n

+-inverseʳ : RightInverse (+ 0) -_ _+_
+-inverseʳ = comm+invˡ⇒invʳ +-comm +-inverseˡ

+-inverse : Inverse (+ 0) -_ _+_
+-inverse = +-inverseˡ , +-inverseʳ

+-isMagma : IsMagma _+_
+-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _+_
  }

+-magma : Magma 0ℓ 0ℓ
+-magma = record
  { isMagma = +-isMagma
  }

+-isSemigroup : IsSemigroup _+_
+-isSemigroup = record
  { isMagma = +-isMagma
  ; assoc   = +-assoc
  }

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

+-0-isMonoid : IsMonoid _+_ (+ 0)
+-0-isMonoid = record
  { isSemigroup = +-isSemigroup
  ; identity    = +-identity
  }

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

+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ (+ 0)
+-0-isCommutativeMonoid = record
  { isSemigroup = +-isSemigroup
  ; identityˡ   = +-identityˡ
  ; comm        = +-comm
  }

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

+-0-isGroup : IsGroup _+_ (+ 0) (-_)
+-0-isGroup = record
  { isMonoid = +-0-isMonoid
  ; inverse  = +-inverse
  ; ⁻¹-cong  = cong (-_)
  }

+-isAbelianGroup : IsAbelianGroup _+_ (+ 0) (-_)
+-isAbelianGroup = record
  { isGroup = +-0-isGroup
  ; comm    = +-comm
  }

+-0-abelianGroup : AbelianGroup _ _
+-0-abelianGroup = record
  { isAbelianGroup = +-isAbelianGroup
  }

-- Other properties of _+_

n≢1+n : ∀ {n} → n ≢ sucℤ n
n≢1+n {+ _}           ()
n≢1+n { -[1+ 0 ]}     ()
n≢1+n { -[1+ suc n ]} ()

1-[1+n]≡-n : ∀ n → sucℤ -[1+ n ] ≡ - (+ n)
1-[1+n]≡-n zero    = refl
1-[1+n]≡-n (suc n) = refl

neg-distrib-+ : ∀ m n → - (m + n) ≡ (- m) + (- n)
neg-distrib-+ (+ zero)  (+ zero)  = refl
neg-distrib-+ (+ zero)  (+ suc n) = refl
neg-distrib-+ (+ suc m) (+ zero)  = cong -[1+_] (ℕₚ.+-identityʳ m)
neg-distrib-+ (+ suc m) (+ suc n) = cong -[1+_] (ℕₚ.+-suc m n)
neg-distrib-+ -[1+ m ]  -[1+ n ]  = cong (λ v → + suc v) (sym (ℕₚ.+-suc m n))
neg-distrib-+ (+   m)   -[1+ n ]  = -[n⊖m]≡-m+n m (suc n)
neg-distrib-+ -[1+ m ]  (+   n)   =
  trans (-[n⊖m]≡-m+n n (suc m)) (+-comm (- + n) (+ suc m))

◃-distrib-+ : ∀ s m n → s ◃ (m ℕ.+ n) ≡ (s ◃ m) + (s ◃ n)
◃-distrib-+ Sign.- m n = begin
  Sign.- ◃ (m ℕ.+ n)          ≡⟨ -◃n≡-n (m ℕ.+ n) ⟩
  - (+ (m ℕ.+ n))             ≡⟨⟩
  - ((+ m) + (+ n))           ≡⟨ neg-distrib-+ (+ m) (+ n) ⟩
  (- (+ m)) + (- (+ n))       ≡⟨ sym (cong₂ _+_ (-◃n≡-n m) (-◃n≡-n n)) ⟩
  (Sign.- ◃ m) + (Sign.- ◃ n) ∎ where open ≡-Reasoning
◃-distrib-+ Sign.+ m n = begin
  Sign.+ ◃ (m ℕ.+ n)          ≡⟨ +◃n≡+n (m ℕ.+ n) ⟩
  + (m ℕ.+ n)                 ≡⟨⟩
  (+ m) + (+ n)               ≡⟨ sym (cong₂ _+_ (+◃n≡+n m) (+◃n≡+n n)) ⟩
  (Sign.+ ◃ m) + (Sign.+ ◃ n) ∎ where open ≡-Reasoning

+-minus-telescope : ∀ x y z → (x - y) + (y - z) ≡ x - z
+-minus-telescope x y z = begin
  (x - y) + (y - z)   ≡⟨ +-assoc x (- y) (y - z) ⟩
  x + (- y + (y - z)) ≡⟨ cong (λ v → x + v) (sym (+-assoc (- y) y _)) ⟩
  x + ((- y + y) - z) ≡⟨ sym (+-assoc x (- y + y) (- z)) ⟩
  x + (- y + y) - z   ≡⟨ cong (λ a → x + a - z) (+-inverseˡ y) ⟩
  x + (+ 0) - z       ≡⟨ cong (_- z) (+-identityʳ x) ⟩
  x - z               ∎ where open ≡-Reasoning

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

neg-minus-pos : ∀ x y → -[1+ x ] - (+ y) ≡ -[1+ (y ℕ.+ x) ]
neg-minus-pos x       zero    = refl
neg-minus-pos zero    (suc y) = cong (-[1+_] ∘ suc) (sym (ℕₚ.+-identityʳ y))
neg-minus-pos (suc x) (suc y) = cong (-[1+_] ∘ suc) (ℕₚ.+-comm (suc x) y)

[+m]-[+n]≡m⊖n : ∀ x y → (+ x) - (+ y) ≡ x ⊖ y
[+m]-[+n]≡m⊖n zero    zero    = refl
[+m]-[+n]≡m⊖n zero    (suc y) = refl
[+m]-[+n]≡m⊖n (suc x) zero    = cong (+_ ∘ suc) (ℕₚ.+-identityʳ x)
[+m]-[+n]≡m⊖n (suc x) (suc y) = refl

∣m-n∣≡∣n-m∣ : (x y : ℤ) → ∣ x - y ∣ ≡ ∣ y - x ∣
∣m-n∣≡∣n-m∣ -[1+ x ] -[1+ y ] = ∣m⊖n∣≡∣n⊖m∣ y x
∣m-n∣≡∣n-m∣ -[1+ x ] (+ y)    = begin
  ∣ -[1+ x ] - (+ y) ∣   ≡⟨ cong ∣_∣ (neg-minus-pos x y) ⟩
  suc (y ℕ.+ x)          ≡⟨ sym (ℕₚ.+-suc y x) ⟩
  y ℕ.+ suc x            ∎ where open ≡-Reasoning
∣m-n∣≡∣n-m∣ (+ x)    -[1+ y ] = begin
  x ℕ.+ suc y            ≡⟨ ℕₚ.+-suc x y ⟩
  suc (x ℕ.+ y)          ≡⟨ cong ∣_∣ (sym (neg-minus-pos y x)) ⟩
  ∣ -[1+ y ] + - (+ x) ∣ ∎ where open ≡-Reasoning
∣m-n∣≡∣n-m∣ (+ x)     (+ y) = begin
  ∣ (+ x) - (+ y) ∣ ≡⟨ cong ∣_∣ ([+m]-[+n]≡m⊖n x y) ⟩
  ∣ x ⊖ y ∣         ≡⟨ ∣m⊖n∣≡∣n⊖m∣ x y ⟩
  ∣ y ⊖ x ∣         ≡⟨ cong ∣_∣ (sym ([+m]-[+n]≡m⊖n y x)) ⟩
  ∣ (+ y) - (+ x) ∣ ∎ where open ≡-Reasoning

minus-suc : ∀ m n → m - + suc n ≡ pred (m - + n)
minus-suc m n = begin
  m + - + suc n      ≡⟨ cong (_+_ m) (neg-suc n) ⟩
  m + pred (- (+ n)) ≡⟨ +-pred m (- + n) ⟩
  pred (m - + n)     ∎ where open ≡-Reasoning

m≡n⇒m-n≡0 : ∀ m n → m ≡ n → m - n ≡ + 0
m≡n⇒m-n≡0 m m refl = +-inverseʳ m

m-n≡0⇒m≡n : ∀ m n → m - n ≡ + 0 → m ≡ n
m-n≡0⇒m≡n m n m-n≡0 = begin
  m             ≡⟨ sym (+-identityʳ m) ⟩
  m + + 0       ≡⟨ cong (_+_ m) (sym (+-inverseˡ n)) ⟩
  m + (- n + n) ≡⟨ sym (+-assoc m (- n) n) ⟩
  (m - n) + n   ≡⟨ cong (_+ n) m-n≡0 ⟩
  + 0 + n       ≡⟨ +-identityˡ n ⟩
  n ∎ where open ≡-Reasoning

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

*-comm : Commutative _*_
*-comm -[1+ a ] -[1+ b ] rewrite ℕₚ.*-comm (suc a) (suc b) = refl
*-comm -[1+ a ] (+   b ) rewrite ℕₚ.*-comm (suc a) b       = refl
*-comm (+   a ) -[1+ b ] rewrite ℕₚ.*-comm a       (suc b) = refl
*-comm (+   a ) (+   b ) rewrite ℕₚ.*-comm a       b       = refl

*-identityˡ : LeftIdentity (+ 1) _*_
*-identityˡ (+ zero ) = refl
*-identityˡ -[1+  n ] rewrite ℕₚ.+-identityʳ n = refl
*-identityˡ (+ suc n) rewrite ℕₚ.+-identityʳ n = refl

*-identityʳ : RightIdentity (+ 1) _*_
*-identityʳ = comm+idˡ⇒idʳ *-comm *-identityˡ

*-identity : Identity (+ 1) _*_
*-identity = *-identityˡ , *-identityʳ

*-zeroˡ : LeftZero (+ 0) _*_
*-zeroˡ n = refl

*-zeroʳ : RightZero (+ 0) _*_
*-zeroʳ = comm+zeˡ⇒zeʳ *-comm *-zeroˡ

*-zero : Zero (+ 0) _*_
*-zero = *-zeroˡ , *-zeroʳ

private
  lemma : ∀ a b c → c ℕ.+ (b ℕ.+ a ℕ.* suc b) ℕ.* suc c
                  ≡ c ℕ.+ b ℕ.* suc c ℕ.+ a ℕ.* suc (c ℕ.+ b ℕ.* suc c)
  lemma =
    solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c)
                    := c :+ b :* (con 1 :+ c) :+
                       a :* (con 1 :+ (c :+ b :* (con 1 :+ c))))
            refl

*-assoc : Associative _*_
*-assoc (+ zero) _ _ = refl
*-assoc x (+ zero) z rewrite ℕₚ.*-zeroʳ ∣ x ∣ = refl
*-assoc x y (+ zero) rewrite
    ℕₚ.*-zeroʳ ∣ y ∣
  | ℕₚ.*-zeroʳ ∣ x ∣
  | ℕₚ.*-zeroʳ ∣ sign x 𝕊* sign y ◃ ∣ x ∣ ℕ.* ∣ y ∣ ∣
  = refl
*-assoc -[1+ a  ] -[1+ b  ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
*-assoc -[1+ a  ] (+ suc b) -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
*-assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
*-assoc (+ suc a) -[1+ b  ] -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
*-assoc -[1+ a  ] -[1+ b  ] -[1+ c  ] = cong -[1+_]     (lemma a b c)
*-assoc -[1+ a  ] (+ suc b) (+ suc c) = cong -[1+_]     (lemma a b c)
*-assoc (+ suc a) -[1+ b  ] (+ suc c) = cong -[1+_]     (lemma a b c)
*-assoc (+ suc a) (+ suc b) -[1+ c  ] = cong -[1+_]     (lemma a b c)

private

  -- lemma used to prove distributivity.
  distrib-lemma :
    ∀ a b c → (c ⊖ b) * -[1+ a ] ≡ a ℕ.+ b ℕ.* suc a ⊖ (a ℕ.+ c ℕ.* suc a)
  distrib-lemma a b c
    rewrite +-cancelˡ-⊖ a (b ℕ.* suc a) (c ℕ.* suc a)
          | ⊖-swap (b ℕ.* suc a) (c ℕ.* suc a)
    with b ℕ.≤? c
  ... | yes b≤c
    rewrite ⊖-≥ b≤c
          | ⊖-≥ (ℕₚ.*-mono-≤ b≤c (ℕₚ.≤-refl {x = suc a}))
          | -◃n≡-n ((c ∸ b) ℕ.* suc a)
          | ℕₚ.*-distribʳ-∸ (suc a) c b
          = refl
  ... | no b≰c
    rewrite sign-⊖-≰ b≰c
          | ∣⊖∣-≰ b≰c
          | +◃n≡+n ((b ∸ c) ℕ.* suc a)
          | ⊖-≰ (b≰c ∘ ℕₚ.*-cancelʳ-≤ b c a)
          | neg-involutive (+ (b ℕ.* suc a ∸ c ℕ.* suc a))
          | ℕₚ.*-distribʳ-∸ (suc a) b c
          = refl

*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ (+ zero) y z
  rewrite ℕₚ.*-zeroʳ ∣ y ∣
        | ℕₚ.*-zeroʳ ∣ z ∣
        | ℕₚ.*-zeroʳ ∣ y + z ∣
        = refl
*-distribʳ-+ x (+ zero) z
  rewrite +-identityˡ z
        | +-identityˡ (sign z 𝕊* sign x ◃ ∣ z ∣ ℕ.* ∣ x ∣)
        = refl
*-distribʳ-+ x y (+ zero)
  rewrite +-identityʳ y
        | +-identityʳ (sign y 𝕊* sign x ◃ ∣ y ∣ ℕ.* ∣ x ∣)
        = refl
*-distribʳ-+ -[1+ a ] -[1+ b ] -[1+ c ] = cong (+_) $
  solve 3 (λ a b c → (con 2 :+ b :+ c) :* (con 1 :+ a)
                  := (con 1 :+ b) :* (con 1 :+ a) :+
                     (con 1 :+ c) :* (con 1 :+ a))
          refl a b c
*-distribʳ-+ (+ suc a) (+ suc b) (+ suc c) = cong (+_) $
  solve 3 (λ a b c → (con 1 :+ b :+ (con 1 :+ c)) :* (con 1 :+ a)
                  := (con 1 :+ b) :* (con 1 :+ a) :+
                     (con 1 :+ c) :* (con 1 :+ a))
        refl a b c
*-distribʳ-+ -[1+ a ] (+ suc b) (+ suc c) = cong -[1+_] $
  solve 3 (λ a b c → a :+ (b :+ (con 1 :+ c)) :* (con 1 :+ a)
                   := (con 1 :+ b) :* (con 1 :+ a) :+
                      (a :+ c :* (con 1 :+ a)))
         refl a b c
*-distribʳ-+ (+ suc a) -[1+ b ] -[1+ c ] = cong -[1+_] $
  solve 3 (λ a b c → a :+ (con 1 :+ a :+ (b :+ c) :* (con 1 :+ a))
                  := (con 1 :+ b) :* (con 1 :+ a) :+
                     (a :+ c :* (con 1 :+ a)))
         refl a b c
*-distribʳ-+ -[1+ a ] -[1+ b ] (+ suc c) = distrib-lemma a b c
*-distribʳ-+ -[1+ a ] (+ suc b) -[1+ c ] = distrib-lemma a c b
*-distribʳ-+ (+ suc a) -[1+ b ] (+ suc c) with b ℕ.≤? c
... | yes b≤c
  rewrite +-cancelˡ-⊖ a (c ℕ.* suc a) (b ℕ.* suc a)
        | ⊖-≥ b≤c
        | +-comm (- (+ (a ℕ.+ b ℕ.* suc a))) (+ (a ℕ.+ c ℕ.* suc a))
        | ⊖-≥ (ℕₚ.*-mono-≤ b≤c (ℕₚ.≤-refl {x = suc a}))
        | ℕₚ.*-distribʳ-∸ (suc a) c b
        | +◃n≡+n (c ℕ.* suc a ∸ b ℕ.* suc a)
        = refl
... | no b≰c
  rewrite +-cancelˡ-⊖ a (c ℕ.* suc a) (b ℕ.* suc a)
        | sign-⊖-≰ b≰c
        | ∣⊖∣-≰ b≰c
        | -◃n≡-n ((b ∸ c) ℕ.* suc a)
        | ⊖-≰ (b≰c ∘ ℕₚ.*-cancelʳ-≤ b c a)
        | ℕₚ.*-distribʳ-∸ (suc a) b c
        = refl
*-distribʳ-+ (+ suc c) (+ suc a) -[1+ b ] with b ℕ.≤? a
... | yes b≤a
  rewrite +-cancelˡ-⊖ c (a ℕ.* suc c) (b ℕ.* suc c)
        | ⊖-≥ b≤a
        | ⊖-≥ (ℕₚ.*-mono-≤ b≤a (ℕₚ.≤-refl {x = suc c}))
        | +◃n≡+n ((a ∸ b) ℕ.* suc c)
        | ℕₚ.*-distribʳ-∸ (suc c) a b
        = refl
... | no b≰a
  rewrite +-cancelˡ-⊖ c (a ℕ.* suc c) (b ℕ.* suc c)
        | sign-⊖-≰ b≰a
        | ∣⊖∣-≰ b≰a
        | ⊖-≰ (b≰a ∘ ℕₚ.*-cancelʳ-≤ b a c)
        | -◃n≡-n ((b ∸ a) ℕ.* suc c)
        | ℕₚ.*-distribʳ-∸ (suc c) b a
        = refl

*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-+

[1+m]*n≡n+m*n : ∀ m n → sucℤ m * n ≡ n + m * n
[1+m]*n≡n+m*n m n = begin
  sucℤ m * n      ≡⟨ *-distribʳ-+ n (+ 1) m ⟩
  + 1 * n + m * n ≡⟨ cong (_+ m * n) (*-identityˡ n) ⟩
  n + m * n       ∎ where open ≡-Reasoning

*-isMagma : IsMagma _*_
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _*_
  }

*-magma : Magma 0ℓ 0ℓ
*-magma = record
  { isMagma = *-isMagma
  }

*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc   = *-assoc
  }

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

*-1-isMonoid : IsMonoid _*_ (+ 1)
*-1-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity    = *-identity
  }

*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
  { isMonoid = *-1-isMonoid
  }

*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ (+ 1)
*-1-isCommutativeMonoid = record
  { isSemigroup = *-isSemigroup
  ; identityˡ   = *-identityˡ
  ; comm        = *-comm
  }

*-1-commutativeMonoid : CommutativeMonoid _ _
*-1-commutativeMonoid = record
  { isCommutativeMonoid = *-1-isCommutativeMonoid
  }

+-*-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ (+ 0) (+ 1)
+-*-isCommutativeSemiring = record
  { +-isCommutativeMonoid = +-0-isCommutativeMonoid
  ; *-isCommutativeMonoid = *-1-isCommutativeMonoid
  ; distribʳ              = *-distribʳ-+
  ; zeroˡ                 = *-zeroˡ
  }

+-*-isRing : IsRing _+_ _*_ -_ (+ 0) (+ 1)
+-*-isRing = record
  { +-isAbelianGroup = +-isAbelianGroup
  ; *-isMonoid       = *-1-isMonoid
  ; distrib          = IsCommutativeSemiring.distrib
                         +-*-isCommutativeSemiring
  }

+-*-ring : Ring _ _
+-*-ring = record { isRing = +-*-isRing }

+-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ (+ 0) (+ 1)
+-*-isCommutativeRing = record
  { isRing = +-*-isRing
  ; *-comm = *-comm
  }

+-*-commutativeRing : CommutativeRing _ _
+-*-commutativeRing = record
  { Carrier           = ℤ
  ; _≈_               = _≡_
  ; _+_               = _+_
  ; _*_               = _*_
  ; -_                = -_
  ; 0#                = + 0
  ; 1#                = + 1
  ; isCommutativeRing = +-*-isCommutativeRing
  }

-- Other properties of _*_

abs-*-commute : ℤtoℕ.Homomorphic₂ ∣_∣ _*_ ℕ._*_
abs-*-commute i j = abs-◃ _ _

pos-distrib-* : ∀ x y → (+ x) * (+ y) ≡ + (x ℕ.* y)
pos-distrib-* zero    y       = refl
pos-distrib-* (suc x) zero    = pos-distrib-* x zero
pos-distrib-* (suc x) (suc y) = refl

◃-distrib-* :  ∀ s t m n → (s 𝕊* t) ◃ (m ℕ.* n) ≡ (s ◃ m) * (t ◃ n)
◃-distrib-* s t zero    zero    = refl
◃-distrib-* s t zero    (suc n) = refl
◃-distrib-* s t (suc m) zero    =
  trans
    (cong₂ _◃_ (𝕊ₚ.*-comm s t) (ℕₚ.*-comm m 0))
    (*-comm (t ◃ zero) (s ◃ suc m))
◃-distrib-* s t (suc m) (suc n) =
  sym (cong₂ _◃_
    (cong₂ _𝕊*_ (sign-◃ s m) (sign-◃ t n))
    (∣s◃m∣*∣t◃n∣≡m*n s t (suc m) (suc n)))

*-cancelʳ-≡ : ∀ i j k → k ≢ + 0 → i * k ≡ j * k → i ≡ j
*-cancelʳ-≡ i j k            ≢0 eq with signAbs k
*-cancelʳ-≡ i j .(+ 0)       ≢0 eq | s ◂ zero  = contradiction refl ≢0
*-cancelʳ-≡ i j .(s ◃ suc n) ≢0 eq | s ◂ suc n
  with ∣ s ◃ suc n ∣ | abs-◃ s (suc n) | sign (s ◃ suc n) | sign-◃ s n
...  | .(suc n)      | refl            | .s               | refl =
  ◃-cong (sign-i≡sign-j i j eq) $
         ℕₚ.*-cancelʳ-≡ ∣ i ∣ ∣ j ∣ $ abs-cong eq
  where
  sign-i≡sign-j : ∀ i j →
                  (sign i 𝕊* s) ◃ (∣ i ∣ ℕ.* suc n) ≡
                  (sign j 𝕊* s) ◃ (∣ j ∣ ℕ.* suc n) →
                  sign i ≡ sign j
  sign-i≡sign-j i              j              eq with signAbs i | signAbs j
  sign-i≡sign-j .(+ 0)         .(+ 0)         eq | s₁ ◂ zero   | s₂ ◂ zero   = refl
  sign-i≡sign-j .(+ 0)         .(s₂ ◃ suc n₂) eq | s₁ ◂ zero   | s₂ ◂ suc n₂
    with ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
  ... | .(suc n₂) | refl
    with abs-cong {s₁} {sign (s₂ ◃ suc n₂) 𝕊* s} {0} {suc n₂ ℕ.* suc n} eq
  ...   | ()
  sign-i≡sign-j .(s₁ ◃ suc n₁) .(+ 0)         eq | s₁ ◂ suc n₁ | s₂ ◂ zero
    with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
  ... | .(suc n₁) | refl
    with abs-cong {sign (s₁ ◃ suc n₁) 𝕊* s} {s₁} {suc n₁ ℕ.* suc n} {0} eq
  ...   | ()
  sign-i≡sign-j .(s₁ ◃ suc n₁) .(s₂ ◃ suc n₂) eq | s₁ ◂ suc n₁ | s₂ ◂ suc n₂
    with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
       | sign (s₁ ◃ suc n₁) | sign-◃ s₁ n₁
       | ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
       | sign (s₂ ◃ suc n₂) | sign-◃ s₂ n₂
  ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl =
    𝕊ₚ.*-cancelʳ-≡ s₁ s₂ (sign-cong eq)

*-cancelˡ-≡ : ∀ i j k → i ≢ + 0 → i * j ≡ i * k → j ≡ k
*-cancelˡ-≡ i j k
  rewrite *-comm i j
        | *-comm i k
        = *-cancelʳ-≡ j k i

*-cancelʳ-≤-pos : ∀ m n o → m * + suc o ≤ n * + suc o → m ≤ n
*-cancelʳ-≤-pos (-[1+ m ]) (-[1+ n ]) o (-≤- n≤m) =
  -≤- (ℕₚ.≤-pred (ℕₚ.*-cancelʳ-≤ (suc n) (suc m) o (s≤s n≤m)))
*-cancelʳ-≤-pos -[1+ _ ]   (+ _)      _ _         = -≤+
*-cancelʳ-≤-pos (+ 0)      -[1+ _ ]   _ ()
*-cancelʳ-≤-pos (+ suc _)  -[1+ _ ]   _ ()
*-cancelʳ-≤-pos (+ 0)      (+ 0)      _ _         = +≤+ z≤n
*-cancelʳ-≤-pos (+ 0)      (+ suc _)  _ _         = +≤+ z≤n
*-cancelʳ-≤-pos (+ suc _)  (+ 0)      _ (+≤+ ())
*-cancelʳ-≤-pos (+ suc m)  (+ suc n)  o (+≤+ m≤n) =
  +≤+ (ℕₚ.*-cancelʳ-≤ (suc m) (suc n) o m≤n)

*-cancelˡ-≤-pos : ∀ m n o → + suc m * n ≤ + suc m * o → n ≤ o
*-cancelˡ-≤-pos m n o
  rewrite *-comm (+ suc m) n
        | *-comm (+ suc m) o
        = *-cancelʳ-≤-pos n o m

*-monoʳ-≤-pos : ∀ n → (_* + suc n) Preserves _≤_ ⟶ _≤_
*-monoʳ-≤-pos _ (-≤+             {n = 0})         = -≤+
*-monoʳ-≤-pos _ (-≤+             {n = suc _})     = -≤+
*-monoʳ-≤-pos x (-≤-                         n≤m) =
  -≤- (ℕₚ.≤-pred (ℕₚ.*-mono-≤ (s≤s n≤m) (ℕₚ.≤-refl {x = suc x})))
*-monoʳ-≤-pos _ (+≤+ {m = 0}     {n = 0}     m≤n) = +≤+ m≤n
*-monoʳ-≤-pos _ (+≤+ {m = 0}     {n = suc _} m≤n) = +≤+ z≤n
*-monoʳ-≤-pos _ (+≤+ {m = suc _} {n = 0}     ())
*-monoʳ-≤-pos x (+≤+ {m = suc _} {n = suc _} m≤n) =
  +≤+ ((ℕₚ.*-mono-≤ m≤n (ℕₚ.≤-refl {x = suc x})))

*-monoʳ-≤-non-neg : ∀ n → (_* + n) Preserves _≤_ ⟶ _≤_
*-monoʳ-≤-non-neg (suc n) = *-monoʳ-≤-pos n
*-monoʳ-≤-non-neg zero {i} {j} i≤j
  rewrite *-zeroʳ i
        | *-zeroʳ j
        = +≤+ z≤n

*-monoˡ-≤-non-neg : ∀ n → (+ n *_) Preserves _≤_ ⟶ _≤_
*-monoˡ-≤-non-neg n {i} {j} i≤j
  rewrite *-comm (+ n) i
        | *-comm (+ n) j
        = *-monoʳ-≤-non-neg n i≤j

*-monoˡ-≤-pos : ∀ n → (+ suc n *_) Preserves _≤_ ⟶ _≤_
*-monoˡ-≤-pos n = *-monoˡ-≤-non-neg (suc n)

-1*n≡-n : ∀ n → -[1+ 0 ] * n ≡ - n
-1*n≡-n (+ zero)  = refl
-1*n≡-n (+ suc n) = cong -[1+_] (ℕₚ.+-identityʳ n)
-1*n≡-n -[1+ n ]  = cong (λ v → + suc v) (ℕₚ.+-identityʳ n)

neg-distribˡ-* : ∀ x y → - (x * y) ≡ (- x) * y
neg-distribˡ-* x y = begin
  - (x * y)          ≡⟨ sym (-1*n≡-n (x * y)) ⟩
  -[1+ 0 ] * (x * y) ≡⟨ sym (*-assoc -[1+ 0 ] x y) ⟩
  -[1+ 0 ] * x * y   ≡⟨ cong (_* y) (-1*n≡-n x) ⟩
  - x * y ∎ where open ≡-Reasoning

neg-distribʳ-* : ∀ x y → - (x * y) ≡ x * (- y)
neg-distribʳ-* x y = begin
  - (x * y) ≡⟨ cong -_ (*-comm x y) ⟩
  - (y * x) ≡⟨ neg-distribˡ-* y x ⟩
  - y * x   ≡⟨ *-comm (- y) x ⟩
  x * (- y) ∎ where open ≡-Reasoning

------------------------------------------------------------------------
-- Properties _⊓_

⊓-comm : Commutative _⊓_
⊓-comm -[1+ m ] -[1+ n ] = cong -[1+_] (ℕₚ.⊔-comm m n)
⊓-comm -[1+ m ] (+ n)    = refl
⊓-comm (+ m)    -[1+ n ] = refl
⊓-comm (+ m)    (+ n)    = cong +_ (ℕₚ.⊓-comm m n)

⊓-assoc : Associative _⊓_
⊓-assoc -[1+ m ] -[1+ n ] -[1+ p ] = cong -[1+_] (ℕₚ.⊔-assoc m n p)
⊓-assoc -[1+ m ] -[1+ n ] (+ p)    = refl
⊓-assoc -[1+ m ] (+ n)    -[1+ p ] = refl
⊓-assoc -[1+ m ] (+ n)    (+ p)    = refl
⊓-assoc (+ m)    -[1+ n ] -[1+ p ] = refl
⊓-assoc (+ m)    -[1+ n ] (+ p)    = refl
⊓-assoc (+ m)    (+ n)    -[1+ p ] = refl
⊓-assoc (+ m)    (+ n)    (+ p)    = cong +_ (ℕₚ.⊓-assoc m n p)

⊓-idem : Idempotent _⊓_
⊓-idem (+ m)    = cong +_ (ℕₚ.⊓-idem m)
⊓-idem -[1+ m ] = cong -[1+_] (ℕₚ.⊔-idem m)

⊓-sel : Selective _⊓_
⊓-sel -[1+ m ] -[1+ n ] = Sum.map (cong -[1+_]) (cong -[1+_]) $ ℕₚ.⊔-sel m n
⊓-sel -[1+ m ] (+ n)    = inj₁ refl
⊓-sel (+ m)    -[1+ n ] = inj₂ refl
⊓-sel (+ m)    (+ n)    = Sum.map (cong ℤ.pos) (cong ℤ.pos) $ ℕₚ.⊓-sel m n

m≤n⇒m⊓n≡m : ∀ {m n} → m ≤ n → m ⊓ n ≡ m
m≤n⇒m⊓n≡m -≤+       = refl
m≤n⇒m⊓n≡m (-≤- n≤m) = cong -[1+_] (ℕₚ.m≤n⇒n⊔m≡n n≤m)
m≤n⇒m⊓n≡m (+≤+ m≤n) = cong +_ (ℕₚ.m≤n⇒m⊓n≡m m≤n)

m⊓n≡m⇒m≤n : ∀ {m n} → m ⊓ n ≡ m → m ≤ n
m⊓n≡m⇒m≤n { -[1+ m ]} { -[1+ n ]} eq = -≤- (ℕₚ.n⊔m≡n⇒m≤n (-[1+-injective eq))
m⊓n≡m⇒m≤n { -[1+ m ]} {+ n}       eq = -≤+
m⊓n≡m⇒m≤n {+ m}       { -[1+ n ]} ()
m⊓n≡m⇒m≤n {+ m}       {+ n}       eq = +≤+ (ℕₚ.m⊓n≡m⇒m≤n (+-injective eq))

m≥n⇒m⊓n≡n : ∀ {m n} → m ≥ n → m ⊓ n ≡ n
m≥n⇒m⊓n≡n {m} {n} pr rewrite ⊓-comm m n = m≤n⇒m⊓n≡m pr

m⊓n≡n⇒m≥n : ∀ {m n} → m ⊓ n ≡ n → m ≥ n
m⊓n≡n⇒m≥n {m} {n} eq rewrite ⊓-comm m n = m⊓n≡m⇒m≤n eq

m⊓n≤n : ∀ m n → m ⊓ n ≤ n
m⊓n≤n -[1+ m ] -[1+ n ] = -≤- (ℕₚ.n≤m⊔n m n)
m⊓n≤n -[1+ m ] (+ n)    = -≤+
m⊓n≤n (+ m)    -[1+ n ] = -≤- ℕₚ.≤-refl
m⊓n≤n (+ m)    (+ n)    = +≤+ (ℕₚ.m⊓n≤n m n)

m⊓n≤m : ∀ m n → m ⊓ n ≤ m
m⊓n≤m m n rewrite ⊓-comm m n = m⊓n≤n n m

------------------------------------------------------------------------
-- Properties _⊔_

⊔-comm : Commutative _⊔_
⊔-comm -[1+ m ] -[1+ n ] = cong -[1+_] (ℕₚ.⊓-comm m n)
⊔-comm -[1+ m ] (+ n)    = refl
⊔-comm (+ m)    -[1+ n ] = refl
⊔-comm (+ m)    (+ n)    = cong +_ (ℕₚ.⊔-comm m n)

⊔-assoc : Associative _⊔_
⊔-assoc -[1+ m ] -[1+ n ] -[1+ p ] = cong -[1+_] (ℕₚ.⊓-assoc m n p)
⊔-assoc -[1+ m ] -[1+ n ] (+ p)    = refl
⊔-assoc -[1+ m ] (+ n)    -[1+ p ] = refl
⊔-assoc -[1+ m ] (+ n)    (+ p)    = refl
⊔-assoc (+ m)    -[1+ n ] -[1+ p ] = refl
⊔-assoc (+ m)    -[1+ n ] (+ p)    = refl
⊔-assoc (+ m)    (+ n)    -[1+ p ] = refl
⊔-assoc (+ m)    (+ n)    (+ p)    = cong +_ (ℕₚ.⊔-assoc m n p)

⊔-idem : Idempotent _⊔_
⊔-idem (+ m)    = cong +_ (ℕₚ.⊔-idem m)
⊔-idem -[1+ m ] = cong -[1+_] (ℕₚ.⊓-idem m)

⊔-sel : Selective _⊔_
⊔-sel -[1+ m ] -[1+ n ] = Sum.map (cong -[1+_]) (cong -[1+_]) $ ℕₚ.⊓-sel m n
⊔-sel -[1+ m ] (+ n)    = inj₂ refl
⊔-sel (+ m)    -[1+ n ] = inj₁ refl
⊔-sel (+ m)    (+ n)    = Sum.map (cong ℤ.pos) (cong ℤ.pos) $ ℕₚ.⊔-sel m n

m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n
m≤n⇒m⊔n≡n -≤+       = refl
m≤n⇒m⊔n≡n (-≤- n≤m) = cong -[1+_] (ℕₚ.m≤n⇒n⊓m≡m n≤m)
m≤n⇒m⊔n≡n (+≤+ m≤n) = cong +_ (ℕₚ.m≤n⇒m⊔n≡n m≤n)

m⊔n≡n⇒m≤n : ∀ {m n} → m ⊔ n ≡ n → m ≤ n
m⊔n≡n⇒m≤n { -[1+ m ]} { -[1+ n ]} eq = -≤- (ℕₚ.m⊓n≡n⇒n≤m (-[1+-injective eq))
m⊔n≡n⇒m≤n { -[1+ m ]} {+ n}       eq = -≤+
m⊔n≡n⇒m≤n {+ m}       { -[1+ n ]} ()
m⊔n≡n⇒m≤n {+ m}       {+ n}       eq = +≤+ (ℕₚ.n⊔m≡m⇒n≤m (+-injective eq))

m≥n⇒m⊔n≡m : ∀ {m n} → m ≥ n → m ⊔ n ≡ m
m≥n⇒m⊔n≡m {m} {n} pr rewrite ⊔-comm m n = m≤n⇒m⊔n≡n pr

m⊔n≡m⇒m≥n : ∀ {m n} → m ⊔ n ≡ m → m ≥ n
m⊔n≡m⇒m≥n {m} {n} eq rewrite ⊔-comm m n = m⊔n≡n⇒m≤n eq

m≤m⊔n : ∀ m n → m ≤ m ⊔ n
m≤m⊔n -[1+ m ] -[1+ n ] = -≤- (ℕₚ.m⊓n≤m m n)
m≤m⊔n -[1+ m ] (+ n)    = -≤+
m≤m⊔n (+ m)    -[1+ n ] = +≤+ ℕₚ.≤-refl
m≤m⊔n (+ m)    (+ n)    = +≤+ (ℕₚ.m≤m⊔n m n)

n≤m⊔n : ∀ m n → n ≤ m ⊔ n
n≤m⊔n m n rewrite ⊔-comm m n = m≤m⊔n n m

neg-distrib-⊔-⊓ : ∀ m n → - (m ⊔ n) ≡ - m ⊓ - n
neg-distrib-⊔-⊓ -[1+ m ]  -[1+ n ]  = refl
neg-distrib-⊔-⊓ -[1+ m ]  (+ zero)  = refl
neg-distrib-⊔-⊓ -[1+ m ]  (+ suc n) = refl
neg-distrib-⊔-⊓ (+ zero)  -[1+ n ]  = refl
neg-distrib-⊔-⊓ (+ suc m) -[1+ n ]  = refl
neg-distrib-⊔-⊓ (+ zero)  (+ zero)  = refl
neg-distrib-⊔-⊓ (+ zero)  (+ suc n) = refl
neg-distrib-⊔-⊓ (+ suc m) (+ zero)  = refl
neg-distrib-⊔-⊓ (+ suc m) (+ suc n) = refl

neg-distrib-⊓-⊔ : ∀ m n → - (m ⊓ n) ≡ - m ⊔ - n
neg-distrib-⊓-⊔ -[1+ m ]  -[1+ n ]  = refl
neg-distrib-⊓-⊔ -[1+ m ]  (+ zero)  = refl
neg-distrib-⊓-⊔ -[1+ m ]  (+ suc n) = refl
neg-distrib-⊓-⊔ (+ zero)  -[1+ n ]  = refl
neg-distrib-⊓-⊔ (+ suc m) -[1+ n ]  = refl
neg-distrib-⊓-⊔ (+ zero)  (+ zero)  = refl
neg-distrib-⊓-⊔ (+ zero)  (+ suc n) = refl
neg-distrib-⊓-⊔ (+ suc m) (+ zero)  = refl
neg-distrib-⊓-⊔ (+ suc m) (+ suc n) = refl

------------------------------------------------------------------------
-- Properties _≤_

drop‿+≤+ : ∀ {m n} → + m ≤ + n → m ℕ.≤ n
drop‿+≤+ (+≤+ m≤n) = m≤n

drop‿-≤- : ∀ {m n} → -[1+ m ] ≤ -[1+ n ] → n ℕ.≤ m
drop‿-≤- (-≤- n≤m) = n≤m

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive { -[1+ n ]} refl = -≤- ℕₚ.≤-refl
≤-reflexive {+ n}       refl = +≤+ ℕₚ.≤-refl

≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl

≤-trans : Transitive _≤_
≤-trans -≤+       (+≤+ n≤m) = -≤+
≤-trans (-≤- n≤m) -≤+       = -≤+
≤-trans (-≤- n≤m) (-≤- k≤n) = -≤- (ℕₚ.≤-trans k≤n n≤m)
≤-trans (+≤+ m≤n) (+≤+ n≤k) = +≤+ (ℕₚ.≤-trans m≤n n≤k)

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym -≤+       ()
≤-antisym (-≤- n≤m) (-≤- m≤n) = cong -[1+_] $ ℕₚ.≤-antisym m≤n n≤m
≤-antisym (+≤+ m≤n) (+≤+ n≤m) = cong (+_)   $ ℕₚ.≤-antisym m≤n n≤m

≤-total : Total _≤_
≤-total (-[1+ m ]) (-[1+ n ]) with ℕₚ.≤-total m n
... | inj₁ m≤n = inj₂ (-≤- m≤n)
... | inj₂ n≤m = inj₁ (-≤- n≤m)
≤-total (-[1+ m ]) (+    n  ) = inj₁ -≤+
≤-total (+    m  ) (-[1+ n ]) = inj₂ -≤+
≤-total (+    m  ) (+    n  ) with ℕₚ.≤-total m n
... | inj₁ m≤n = inj₁ (+≤+ m≤n)
... | inj₂ n≤m = inj₂ (+≤+ n≤m)

infix  4 _≤?_
_≤?_ : Decidable _≤_
-[1+ m ] ≤? -[1+ n ] = Dec.map′ -≤- drop‿-≤- (ℕ._≤?_ n m)
-[1+ m ] ≤? +    n   = yes -≤+
+    m   ≤? -[1+ n ] = no λ ()
+    m   ≤? +    n   = Dec.map′ +≤+ drop‿+≤+ (ℕ._≤?_ m n)

≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-preorder : Preorder _ _ _
≤-preorder = record
  { isPreorder = ≤-isPreorder
  }

≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym  = ≤-antisym
  }

≤-poset : Poset _ _ _
≤-poset = record
  { Carrier = ℤ
  ; _≈_ = _≡_
  ; _≤_ = _≤_
  ; isPartialOrder = ≤-isPartialOrder
  }

≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

≤-decTotalOrder : DecTotalOrder _ _ _
≤-decTotalOrder = record
  { Carrier         = ℤ
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = ≤-isDecTotalOrder
  }

-- Other properties of _≤_

0⊖m≤+ : ∀ m {n} → 0 ⊖ m ≤ + n
0⊖m≤+ zero    = +≤+ z≤n
0⊖m≤+ (suc m) = -≤+

≤-step : ∀ {n m} → n ≤ m → n ≤ sucℤ m
≤-step -≤+             = -≤+
≤-step (+≤+ m≤n)       = +≤+ (ℕₚ.≤-step m≤n)
≤-step (-≤- z≤n)       = -≤+
≤-step (-≤- (ℕ.s≤s n≤m)) = -≤- (ℕₚ.≤-step n≤m)

≤-steps : ∀ {m n} p → m ≤ n → m ≤ + p + n
≤-steps {n = n} zero    m≤n rewrite +-identityˡ n = m≤n
≤-steps {n = n} (suc p) m≤n rewrite suc-+ p n     = ≤-step (≤-steps p m≤n)

≤-step-neg : ∀ {m n} → m ≤ n → pred m ≤ n
≤-step-neg -≤+             = -≤+
≤-step-neg (-≤- n≤m)       = -≤- (ℕₚ.≤-step n≤m)
≤-step-neg (+≤+ z≤n)       = -≤+
≤-step-neg (+≤+ (ℕ.s≤s m≤n)) = +≤+ (ℕₚ.≤-step m≤n)

≤-steps-neg : ∀ {m n} p → m ≤ n → m - + p ≤ n
≤-steps-neg {m} zero    m≤n rewrite +-identityʳ m = m≤n
≤-steps-neg {m} (suc p) m≤n rewrite minus-suc m p = ≤-step-neg (≤-steps-neg p m≤n)

⊖-monoʳ-≥-≤ : ∀ p → (p ⊖_) Preserves ℕ._≥_ ⟶ _≤_
⊖-monoʳ-≥-≤ zero    (z≤n {n})     = 0⊖m≤+ n
⊖-monoʳ-≥-≤ zero    (ℕ.s≤s m≤n)   = -≤- m≤n
⊖-monoʳ-≥-≤ (suc p) (z≤n {zero})  = ≤-refl
⊖-monoʳ-≥-≤ (suc p) (z≤n {suc n}) = ≤-step (⊖-monoʳ-≥-≤ p (z≤n {n}))
⊖-monoʳ-≥-≤ (suc p) (ℕ.s≤s m≤n)   = ⊖-monoʳ-≥-≤ p m≤n

⊖-monoˡ-≤ : ∀ p → (_⊖ p) Preserves ℕ._≤_ ⟶ _≤_
⊖-monoˡ-≤ zero    m≤n             = +≤+ m≤n
⊖-monoˡ-≤ (suc p) (z≤n {0})       = ≤-refl
⊖-monoˡ-≤ (suc p) (z≤n {(suc m)}) = ≤-trans (⊖-monoʳ-≥-≤ 0 (ℕₚ.n≤1+n p)) (⊖-monoˡ-≤ p z≤n)
⊖-monoˡ-≤ (suc p) (ℕ.s≤s m≤n)     = ⊖-monoˡ-≤ p m≤n

pred-mono : pred Preserves _≤_ ⟶ _≤_
pred-mono (-≤+ {n = 0})     = -≤- z≤n
pred-mono (-≤+ {n = suc n}) = -≤+
pred-mono (-≤- n≤m)         = -≤- (ℕ.s≤s n≤m)
pred-mono (+≤+ m≤n)         = ⊖-monoˡ-≤ 1 m≤n

suc-mono : sucℤ Preserves _≤_ ⟶ _≤_
suc-mono (-≤+ {m}) = 0⊖m≤+ m
suc-mono (-≤- n≤m) = ⊖-monoʳ-≥-≤ zero n≤m
suc-mono (+≤+ m≤n) = +≤+ (ℕ.s≤s m≤n)

+-pos-monoʳ-≤ : ∀ n → (_+_ (+ n)) Preserves _≤_ ⟶ _≤_
+-pos-monoʳ-≤ zero {i} {j} i≤j
  rewrite +-identityˡ i
        | +-identityˡ j
        = i≤j
+-pos-monoʳ-≤ (suc n) {i} {j} i≤j
  rewrite suc-+ n i
        | suc-+ n j
        = suc-mono (+-pos-monoʳ-≤ n i≤j)

+-neg-monoʳ-≤ : ∀ n → (_+_ -[1+ n ]) Preserves _≤_ ⟶ _≤_
+-neg-monoʳ-≤ zero i≤j = pred-mono i≤j
+-neg-monoʳ-≤ (suc n) {i} {j} i≤j
  rewrite pred-+ -[1+ n ] i
        | pred-+ -[1+ n ] j
        = pred-mono (+-neg-monoʳ-≤ n i≤j)

+-monoʳ-≤ : ∀ n → (_+_ n) Preserves _≤_ ⟶ _≤_
+-monoʳ-≤ (+ n)    = +-pos-monoʳ-≤ n
+-monoʳ-≤ -[1+ n ] = +-neg-monoʳ-≤ n

+-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
+-monoˡ-≤ n {i} {j} i≤j
  rewrite +-comm i n
        | +-comm j n
        = +-monoʳ-≤ n i≤j

+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+-mono-≤ {m} {n} {i} {j} m≤n i≤j = begin
  m + i ≤⟨ +-monoˡ-≤ i m≤n ⟩
  n + i ≤⟨ +-monoʳ-≤ n i≤j ⟩
  n + j ∎
  where open POR ≤-poset

neg-≤-pos : ∀ {m n} → - (+ m) ≤ + n
neg-≤-pos {zero}  = +≤+ z≤n
neg-≤-pos {suc m} = -≤+

neg-mono-≤-≥ : -_ Preserves _≤_ ⟶ _≥_
neg-mono-≤-≥ -≤+             = neg-≤-pos
neg-mono-≤-≥ (-≤- n≤m)       = +≤+ (s≤s n≤m)
neg-mono-≤-≥ (+≤+ z≤n)       = neg-≤-pos
neg-mono-≤-≥ (+≤+ (s≤s m≤n)) = -≤- m≤n

m≤m+n : ∀ {m} n → m ≤ m + + n
m≤m+n {m} n = begin
  m       ≡⟨ sym (+-identityʳ m) ⟩
  m + + 0 ≤⟨ +-monoʳ-≤ m (+≤+ z≤n) ⟩
  m + + n ∎
  where open POR ≤-poset

m-n≤m : ∀ m n → m - + n ≤ m
m-n≤m m n = ≤-steps-neg n ≤-refl

n≤m+n : ∀ m {n} → n ≤ + m + n
n≤m+n m {n} rewrite +-comm (+ m) n = m≤m+n m

m≤n⇒m-n≤0 : ∀ {m n} → m ≤ n → m - n ≤ + 0
m≤n⇒m-n≤0 (-≤+ {n = n})         = ≤-steps-neg n -≤+
m≤n⇒m-n≤0 (-≤- {n = n} n≤m)     = ≤-trans (⊖-monoʳ-≥-≤ n n≤m) (≤-reflexive (n⊖n≡0 n))
m≤n⇒m-n≤0 (+≤+ {n = 0} z≤n)     = +≤+ z≤n
m≤n⇒m-n≤0 (+≤+ {n = suc n} z≤n) = -≤+
m≤n⇒m-n≤0 (+≤+ (ℕ.s≤s {m} m≤n)) = ≤-trans (⊖-monoʳ-≥-≤ m m≤n) (≤-reflexive (n⊖n≡0 m))

m-n≤0⇒m≤n : ∀ {m n} → m - n ≤ + 0 → m ≤ n
m-n≤0⇒m≤n {m} {n} m-n≤0 = begin
  m             ≡⟨ sym (+-identityʳ m) ⟩
  m + + 0       ≡⟨ cong (_+_ m) (sym (+-inverseˡ n)) ⟩
  m + (- n + n) ≡⟨ sym (+-assoc m (- n) n) ⟩
  (m - n) + n   ≤⟨ +-monoˡ-≤ n m-n≤0 ⟩
  + 0 + n       ≡⟨ +-identityˡ n ⟩
  n             ∎
  where open POR ≤-poset

m≤n⇒0≤n-m : ∀ {m n} → m ≤ n → + 0 ≤ n - m
m≤n⇒0≤n-m {m} {n} m≤n = begin
  + 0   ≡⟨ sym (+-inverseʳ m) ⟩
  m - m ≤⟨ +-monoˡ-≤ (- m) m≤n ⟩
  n - m ∎
  where open POR ≤-poset

0≤n-m⇒m≤n : ∀ {m n} → + 0 ≤ n - m → m ≤ n
0≤n-m⇒m≤n {m} {n} 0≤n-m = begin
  m             ≡⟨ sym (+-identityˡ m) ⟩
  + 0 + m       ≤⟨ +-monoˡ-≤ m 0≤n-m ⟩
  n - m + m     ≡⟨ +-assoc n (- m) m ⟩
  n + (- m + m) ≡⟨ cong (_+_ n) (+-inverseˡ m) ⟩
  n + + 0       ≡⟨ +-identityʳ n ⟩
  n             ∎
  where open POR ≤-poset

n≤1+n : ∀ n → n ≤ (+ 1) + n
n≤1+n n = ≤-step ≤-refl

≤-irrelevant : Irrelevant _≤_
≤-irrelevant -≤+       -≤+         = refl
≤-irrelevant (-≤- n≤m₁) (-≤- n≤m₂) = cong -≤- (ℕₚ.≤-irrelevant n≤m₁ n≤m₂)
≤-irrelevant (+≤+ n≤m₁) (+≤+ n≤m₂) = cong +≤+ (ℕₚ.≤-irrelevant n≤m₁ n≤m₂)

------------------------------------------------------------------------
-- Properties _<_

-<+ : ∀ {m n} → -[1+ m ] < + n
-<+ {0}     = +≤+ z≤n
-<+ {suc _} = -≤+

<-irrefl : Irreflexive _≡_ _<_
<-irrefl { + n}          refl (+≤+ 1+n≤n) = ℕₚ.<-irrefl refl 1+n≤n
<-irrefl { -[1+ zero  ]} refl ()
<-irrefl { -[1+ suc n ]} refl (-≤- 1+n≤n) = ℕₚ.<-irrefl refl 1+n≤n

>-irrefl : Irreflexive _≡_ _>_
>-irrefl = <-irrefl ∘ sym

<-asym : Asymmetric _<_
<-asym {+ n}           {+ m}           (+≤+ n<m) (+≤+ m<n) =
  ℕₚ.<-asym n<m m<n
<-asym {+ n}           { -[1+ m ]}     ()        _
<-asym { -[1+ n ]}     {+_ n₁}         _         ()
<-asym { -[1+ 0 ]}     { -[1+_] _}     ()        _
<-asym { -[1+ _ ]}     { -[1+_] 0}     _         ()
<-asym { -[1+ suc n ]} { -[1+ suc m ]} (-≤- n<m) (-≤- m<n) =
  ℕₚ.<-asym n<m m<n

≤-<-trans : Trans _≤_ _<_ _<_
≤-<-trans { -[1+ m ]} {+ n} {+ p} -≤+ (+≤+ 1+n≤p) = -<+ {m} {p}
≤-<-trans {+ m} {+ n} {+ p} (+≤+ m≤n) (+≤+ 1+n≤p) = +≤+ (ℕₚ.≤-trans (ℕ.s≤s m≤n) 1+n≤p)
≤-<-trans { -[1+ m ]} { -[1+ n ]} (-≤- n≤m) n<p = ≤-trans (⊖-monoʳ-≥-≤ 0 n≤m) n<p

<-≤-trans : Trans _<_ _≤_ _<_
<-≤-trans = ≤-trans

<⇒≤ : ∀ {m n} → m < n → m ≤ n
<⇒≤ m<n =  ≤-trans (n≤1+n _) m<n

<-trans : Transitive _<_
<-trans {m} {n} {p} m<n n<p = ≤-<-trans {m} {n} {p} (<⇒≤ m<n) n<p

<-cmp : Trichotomous _≡_ _<_
<-cmp (+ m) (+ n) with ℕₚ.<-cmp m n
... | tri< m<n m≢n m≯n =
  tri< (+≤+ m<n)         (m≢n ∘ +-injective) (m≯n ∘ drop‿+≤+)
... | tri≈ m≮n m≡n m≯n =
  tri≈ (m≮n ∘ drop‿+≤+) (cong (+_) m≡n)     (m≯n ∘ drop‿+≤+)
... | tri> m≮n m≢n m>n =
  tri> (m≮n ∘ drop‿+≤+) (m≢n ∘ +-injective) (+≤+ m>n)
<-cmp (+_ m)       -[1+ 0 ]     = tri> (λ())     (λ()) (+≤+ z≤n)
<-cmp (+_ m)       -[1+ suc n ] = tri> (λ())     (λ()) -≤+
<-cmp -[1+ 0 ]     (+ n)        = tri< (+≤+ z≤n) (λ()) (λ())
<-cmp -[1+ suc m ] (+ n)        = tri< -≤+       (λ()) (λ())
<-cmp -[1+ 0 ]     -[1+ 0 ]     = tri≈ (λ())     refl  (λ())
<-cmp -[1+ 0 ]     -[1+ suc n ] = tri> (λ())     (λ()) (-≤- z≤n)
<-cmp -[1+ suc m ] -[1+ 0 ]     = tri< (-≤- z≤n) (λ()) (λ())
<-cmp -[1+ suc m ] -[1+ suc n ] with ℕₚ.<-cmp (suc m) (suc n)
... | tri< m<n m≢n m≯n =
  tri> (m≯n ∘ s≤s ∘ drop‿-≤-) (m≢n ∘ -[1+-injective) (-≤- (ℕₚ.≤-pred m<n))
... | tri≈ m≮n m≡n m≯n =
  tri≈ (m≯n ∘ ℕ.s≤s ∘ drop‿-≤-) (cong -[1+_] m≡n) (m≮n ∘ ℕ.s≤s ∘ drop‿-≤-)
... | tri> m≮n m≢n m>n =
  tri< (-≤- (ℕₚ.≤-pred m>n)) (m≢n ∘ -[1+-injective) (m≮n ∘ s≤s ∘ drop‿-≤-)

<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
  { isEquivalence = isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = λ {i} → <-trans {i}
  ; <-resp-≈      = (λ {x} → subst (x <_)) , subst (_< _)
  }

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

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

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

-- Other properties of _<_

n≮n : ∀ {n} → n ≮ n
n≮n {+ n}           (+≤+ n<n) =  contradiction n<n ℕₚ.1+n≰n
n≮n { -[1+ 0 ]}     ()
n≮n { -[1+ suc n ]} (-≤- n<n) =  contradiction n<n ℕₚ.1+n≰n

>⇒≰ : ∀ {x y} → x > y → x ≰ y
>⇒≰ {y = y} x>y x≤y = contradiction (<-≤-trans {i = y} x>y x≤y) n≮n

≰⇒> : ∀ {x y} → x ≰ y → x > y
≰⇒> {+ m}           {+ n}           m≰n =  +≤+ (ℕₚ.≰⇒> (m≰n ∘ +≤+))
≰⇒> {+ m}           { -[1+ n ]}     _   =  -<+ {n} {m}
≰⇒> { -[1+ m ]}     {+ _}           m≰n =  contradiction -≤+ m≰n
≰⇒> { -[1+ 0 ]}     { -[1+ 0 ]}     m≰n =  contradiction ≤-refl m≰n
≰⇒> { -[1+ suc _ ]} { -[1+ 0 ]}     m≰n =  contradiction (-≤- z≤n) m≰n
≰⇒> { -[1+ m ]}     { -[1+ suc n ]} m≰n with m ℕ.≤? n
... | yes m≤n  = -≤- m≤n
... | no  m≰n' = contradiction (-≤- (ℕₚ.≰⇒> m≰n')) m≰n

<-irrelevant : Irrelevant _<_
<-irrelevant = ≤-irrelevant

+-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
+-monoˡ-< n {i} {j} i<j
  rewrite sym (+-assoc (+ 1) i n)
          = +-monoˡ-≤ n i<j

+-monoʳ-< : ∀ n → (_+_ n) Preserves _<_ ⟶ _<_
+-monoʳ-< n {i} {j} i<j
  rewrite +-comm n i
        | +-comm n j
        = +-monoˡ-< n {i} {j} i<j

+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+-mono-< {m} {n} {i} {j} m<n i<j = begin
  sucℤ (m + i) ≤⟨ suc-mono {m + i} (<⇒≤ (+-monoˡ-< i {m} {n} m<n)) ⟩
  sucℤ (n + i) ≤⟨ +-monoʳ-< n i<j ⟩
  n + j        ∎
  where open POR ≤-poset

+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
+-mono-≤-< {m} {n} {i} {j} m≤n i<j = ≤-<-trans (+-monoˡ-≤ i m≤n) (+-monoʳ-< n i<j)

+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
+-mono-<-≤ {m} {n} {i} {j} m<n i≤j =
  <-≤-trans {m + i} {n + i} {n + j} (+-monoˡ-< i {m} {n} m<n) (+-monoʳ-≤ n i≤j)

------------------------------------------------------------------------
-- Extra properties

m≤pred[n]⇒m<n : ∀ {m n} → m ≤ pred n → m < n
m≤pred[n]⇒m<n {m} {n} m≤predn = begin
  sucℤ m               ≤⟨ +-monoʳ-≤ (+ 1) m≤predn ⟩
  + 1 + pred n         ≡⟨ sym (+-assoc (+ 1) -[1+ 0 ] n) ⟩
  (+ 1 + -[1+ 0 ]) + n ≡⟨ cong (_+ n) (+-inverseʳ (+ 1)) ⟩
  + 0 + n              ≡⟨ +-identityˡ n ⟩
  n                    ∎
  where open POR ≤-poset

m<n⇒m≤pred[n] : ∀ {m n} → m < n → m ≤ pred n
m<n⇒m≤pred[n] {m} {n} m<n = begin
  m             ≡⟨ sym (pred-suc m) ⟩
  pred (sucℤ m) ≤⟨ pred-mono m<n ⟩
  pred n        ∎
  where open POR ≤-poset

neg-mono-<-> : -_ Preserves _<_ ⟶ _>_
neg-mono-<-> {i} {j} i<j = begin
  + 1 - j       ≡⟨ cong (_- j) (neg-involutive (+ 1)) ⟩
  - - + 1 - j   ≡⟨ sym (neg-distrib-+ (- + 1) j) ⟩
  - (- + 1 + j) ≤⟨ neg-mono-≤-≥ (m<n⇒m≤pred[n] i<j) ⟩
  - i           ∎
  where open POR ≤-poset

------------------------------------------------------------------------
-- A specialised module for reasoning about the _≤_ and _<_ relations

module ≤-Reasoning where
  open import Relation.Binary.Reasoning.Base.Triple
    ≤-isPreorder
    (λ {i} → <-trans {i})
    (resp₂ _<_)
    <⇒≤
    (λ {i} → <-≤-trans {i})
    ≤-<-trans
    public hiding (_≈⟨_⟩_)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

inverseˡ = +-inverseˡ
{-# WARNING_ON_USAGE inverseˡ
"Warning: inverseˡ was deprecated in v0.15.
Please use +-inverseˡ instead."
#-}
inverseʳ = +-inverseʳ
{-# WARNING_ON_USAGE inverseʳ
"Warning: inverseʳ was deprecated in v0.15.
Please use +-inverseʳ instead."
#-}
distribʳ = *-distribʳ-+
{-# WARNING_ON_USAGE distribʳ
"Warning: distribʳ was deprecated in v0.15.
Please use *-distribʳ-+ instead."
#-}
isCommutativeSemiring = +-*-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring
"Warning: isCommutativeSemiring was deprecated in v0.15.
Please use +-*-isCommutativeSemiring instead."
#-}
commutativeRing = +-*-commutativeRing
{-# WARNING_ON_USAGE commutativeRing
"Warning: commutativeRing was deprecated in v0.15.
Please use +-*-commutativeRing instead."
#-}
*-+-right-mono = *-monoʳ-≤-pos
{-# WARNING_ON_USAGE *-+-right-mono
"Warning: *-+-right-mono was deprecated in v0.15.
Please use *-monoʳ-≤-pos instead."
#-}
cancel-*-+-right-≤ = *-cancelʳ-≤-pos
{-# WARNING_ON_USAGE cancel-*-+-right-≤
"Warning: cancel-*-+-right-≤ was deprecated in v0.15.
Please use *-cancelʳ-≤-pos instead."
#-}
cancel-*-right = *-cancelʳ-≡
{-# WARNING_ON_USAGE cancel-*-right
"Warning: cancel-*-right was deprecated in v0.15.
Please use *-cancelʳ-≡ instead."
#-}
doubleNeg = neg-involutive
{-# WARNING_ON_USAGE doubleNeg
"Warning: doubleNeg was deprecated in v0.15.
Please use neg-involutive instead."
#-}
-‿involutive = neg-involutive
{-# WARNING_ON_USAGE -‿involutive
"Warning: -‿involutive was deprecated in v0.15.
Please use neg-involutive instead."
#-}
+-⊖-left-cancel = +-cancelˡ-⊖
{-# WARNING_ON_USAGE +-⊖-left-cancel
"Warning: +-⊖-left-cancel was deprecated in v0.15.
Please use +-cancelˡ-⊖ instead."
#-}

-- Version 1.0

≰→> = ≰⇒>
{-# WARNING_ON_USAGE ≰→>
"Warning: ≰→> was deprecated in v1.0.
Please use ≰⇒> instead."
#-}
≤-irrelevance = ≤-irrelevant
{-# WARNING_ON_USAGE ≤-irrelevance
"Warning: ≤-irrelevance was deprecated in v1.0.
Please use ≤-irrelevant instead."
#-}
<-irrelevance = <-irrelevant
{-# WARNING_ON_USAGE <-irrelevance
"Warning: <-irrelevance was deprecated in v1.0.
Please use <-irrelevant instead."
#-}


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module LogicalFramework.AdequacyTheorems where

module Example5 where

  -- First-order logic with equality.
  open import Common.FOL.FOL-Eq public

  postulate
    A B C : Set
    f₁    : A → C
    f₂    : B → C

  g : (A → C) → (B → C) → A ∨ B → C
  g f₁ f₂ (inj₁ a) = f₁ a
  g f₁ f₂ (inj₂ b) = f₂ b

  g' : (A → C) → (B → C) → A ∨ B → C
  g' f₁ f₂ x = case f₁ f₂ x

module Example7 where

  -- First-order logic with equality.
  open import Common.FOL.FOL-Eq public

  postulate
    C  : D → D → Set
    d  : ∀ {a} → C a a

  g : ∀ {a b} → a ≡ b → C a b
  g refl = d

  g' : ∀ {a b} → a ≡ b → C a b
  g' {a} h = subst (C a) h d

module Example10 where

  -- First-order logic with equality.
  open import Common.FOL.FOL-Eq public

  postulate
    A B C : Set
    f₁ : A → C
    f₂ : B → C

  f : A ∨ B → C
  f (inj₁ a) = f₁ a
  f (inj₂ b) = f₂ b

  f' : A ∨ B → C
  f' = case f₁ f₂

module Example20 where

  -- First-order logic with equality.
  open import Common.FOL.FOL-Eq public

  f : {A : D → Set}{t t' : D} → t ≡ t' → A t → A t'
  f {A} {t} {.t} refl At = d At
    where
    postulate d : A t → A t

  f' : {A : D → Set}{t t' : D} → t ≡ t' → A t → A t'
  f' {A} h At = subst A h At

module Example30 where

  -- First-order logic with equality.
  open import Common.FOL.FOL-Eq public

  postulate
    A B C E : Set
    f₁ : A → E
    f₂ : B → E
    f₃ : C → E

  g : (A ∨ B) ∨ C → E
  g (inj₁ (inj₁ a)) = f₁ a
  g (inj₁ (inj₂ b)) = f₂ b
  g (inj₂ c)        = f₃ c

  g' : (A ∨ B) ∨ C → E
  g' = case (case f₁ f₂) f₃

module Example40 where

  infixl 9  _+_ _+'_
  infix  7  _≡_

  data ℕ : Set where
    zero :     ℕ
    succ : ℕ → ℕ

  ℕ-ind : (A : ℕ → Set) → A zero → (∀ n → A n → A (succ n)) → ∀ n → A n
  ℕ-ind A A0 h zero     = A0
  ℕ-ind A A0 h (succ n) = h n (ℕ-ind A A0 h n)

  data _≡_ (x : ℕ) : ℕ → Set where
    refl : x ≡ x

  subst : (A : ℕ → Set) → ∀ {x y} → x ≡ y → A x → A y
  subst A refl Ax = Ax

  _+_ : ℕ → ℕ → ℕ
  zero   + n = n
  succ m + n = succ (m + n)

  _+'_ : ℕ → ℕ → ℕ
  m +' n = ℕ-ind (λ _ → ℕ) n (λ x y → succ y) m

  -- Properties using pattern matching.
  succCong : ∀ {m n} → m ≡ n → succ m ≡ succ n
  succCong refl = refl

  +-rightIdentity : ∀ n → n + zero ≡ n
  +-rightIdentity zero     = refl
  +-rightIdentity (succ n) = succCong (+-rightIdentity n)

  -- Properties using the basic inductive constants.
  succCong' : ∀ {m n} → m ≡ n → succ m ≡ succ n
  succCong' {m} h = subst (λ x → succ m ≡ succ x) h refl

  +'-leftIdentity : ∀ n → zero +' n ≡ n
  +'-leftIdentity n = refl

  +'-rightIdentity : ∀ n → n +' zero ≡ n
  +'-rightIdentity = ℕ-ind A A0 is
    where
    A : ℕ → Set
    A n = n +' zero ≡ n

    A0 : A zero
    A0 = refl

    is : ∀ n → A n → A (succ n)
    is n ih = succCong' ih

module Example50 where

  infixl 10 _*_
  infixl 9  _+_
  infix  7  _≡_

  data ℕ : Set where
    zero :     ℕ
    succ : ℕ → ℕ

  ℕ-ind : (A : ℕ → Set) → A zero → (∀ n → A n → A (succ n)) → ∀ n → A n
  ℕ-ind A A0 h zero     = A0
  ℕ-ind A A0 h (succ n) = h n (ℕ-ind A A0 h n)

  data _≡_ (x : ℕ) : ℕ → Set where
    refl : x ≡ x

  ℕ-rec : {A : Set} → A → (ℕ → A → A) → ℕ → A
  ℕ-rec {A} = ℕ-ind (λ _ → A)

  _+_ : ℕ → ℕ → ℕ
  m + n = ℕ-rec n (λ _ x → succ x) m

  +-0x : ∀ n → zero + n ≡ n
  +-0x n = refl

  +-Sx : ∀ m n → succ m + n ≡ succ (m + n)
  +-Sx m n = refl

  _*_ : ℕ → ℕ → ℕ
  m * n = ℕ-rec zero (λ _ x → n + x) m

  *-0x : ∀ n → zero * n ≡ zero
  *-0x n = refl

  *-Sx : ∀ m n → succ m * n ≡ n + m * n
  *-Sx m n = refl

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of right-scaling
------------------------------------------------------------------------

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

open import Relation.Binary

-- The properties are parameterised by the two carriers and
-- the result equality.

module Algebra.Module.Definitions.Right
  {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
  where

open import Data.Product
open import Data.Sum

------------------------------------------------------------------------
-- Binary operations

open import Algebra.Core

------------------------------------------------------------------------
-- Properties of operations

RightIdentity : A → Opᵣ A B → Set _
RightIdentity a _∙ᴮ_ = ∀ m → (m ∙ᴮ a) ≈ m

Associative : Op₂ A → Opᵣ A B → Set _
Associative _∙ᴬ_ _∙ᴮ_ = ∀ m x y → ((m ∙ᴮ x) ∙ᴮ y) ≈ (m ∙ᴮ (x ∙ᴬ y))

_DistributesOverˡ_⟶_ : Opᵣ A B → Op₂ A → Op₂ B → Set _
_*_ DistributesOverˡ _+ᴬ_ ⟶ _+ᴮ_ =
  ∀ m x y → (m * (x +ᴬ y)) ≈ ((m * x) +ᴮ (m * y))

_DistributesOverʳ_ : Opᵣ A B → Op₂ B → Set _
_*_ DistributesOverʳ _+_ =
  ∀ x m n → ((m + n) * x) ≈ ((m * x) + (n * x))

LeftZero : B → Opᵣ A B → Set _
LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z

RightZero : A → B → Opᵣ A B → Set _
RightZero zᴬ zᴮ _∙_ = ∀ x → (x ∙ zᴬ) ≈ zᴮ

Commutative : Opᵣ A B → Set _
Commutative _∙_ = ∀ m x y → ((m ∙ x) ∙ y) ≈ ((m ∙ y) ∙ x)

LeftCongruent : ∀ {ℓa} → Rel A ℓa → Opᵣ A B → Set _
LeftCongruent ≈ᴬ _∙_ = ∀ {m} → (m ∙_) Preserves ≈ᴬ ⟶ _≈_

RightCongruent : Opᵣ A B → Set _
RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_

Congruent : ∀ {ℓa} → Rel A ℓa → Opᵣ A B → Set _
Congruent ≈ᴬ ∙ = ∙ Preserves₂ _≈_ ⟶ ≈ᴬ ⟶ _≈_


text:
module Lec1Done where

-- the -- mark introduces a "comment to end of line"

------------------------------------------------------------------------------
-- some basic "logical" types
------------------------------------------------------------------------------

data Zero : Set where
  -- to give a value in a data, choose one constructor
  -- there are no constructors
  -- so that's impossible

record One : Set where
  -- to give a value in a record type, fill all its fields
  -- there are no fields
  -- so that's trivial
  --   (can we have a constructor, for convenience?)
  constructor <>

{-# COMPILE GHC One = data () (()) #-}

data _+_ (S : Set)(T : Set) : Set where -- "where" wants an indented block
  -- to offer a choice of constructors, list them with their types
  inl : S -> S + T     -- constructors can pack up stuff
  inr : T -> S + T
  -- in Haskell, this was called "Either S T"

{-
record _*_ (S : Set)(T : Set) : Set where
  field -- introduces a bunch of fields, listed with their types
    fst : S
    snd : T
  -- in Haskell, this was called "(S, T)"
-}

-- _*_ IS GENERALIZED BY SIGMA

record Sg (S : Set)(T : S -> Set) : Set where  -- Sg is short for "Sigma"
  constructor _,_
  field -- introduces a bunch of fields, listed with their types
    fst : S
    snd : T fst
open Sg public -- brings fst and snd into scope hereafter unto all inheritors
-- make _*_ from Sg ?
_*_ : Set -> Set -> Set
S * T = Sg S \ _ -> T
infixr 4 _*_ _,_

------------------------------------------------------------------------------
-- some simple proofs
------------------------------------------------------------------------------

comm-* : {A : Set}{B : Set} -> A * B -> B * A
comm-* record { fst = a ; snd = b } = record { fst = b ; snd = a }

assocLR-+ : {A B C : Set} -> (A + B) + C -> A + (B + C)
assocLR-+ (inl (inl a)) = inl a
assocLR-+ (inl (inr b)) = inr (inl b)
assocLR-+ (inr c)       = inr (inr c)

_$*_ : {A A' B B' : Set} -> (A -> A') -> (B -> B') -> A * B -> A' * B'
(f $* g) record { fst = a ; snd = b } = record { fst = f a ; snd = g b }

-- record syntax is rather ugly for small stuff; can we have constructors?

_$+_ : {A A' B B' : Set} -> (A -> A') -> (B -> B') -> A + B -> A' + B'
(f $+ g) (inl a) = inl (f a)
(f $+ g) (inr b) = inr (g b)

combinatorK : {A E : Set} -> A -> E -> A
combinatorK = \ a _ -> a

combinatorS : {S T E : Set} -> (E -> S -> T) -> (E -> S) -> E -> T
combinatorS = \ f s e -> (f e) (s e)

id : {X : Set} -> X -> X
-- id x = x -- is the easy way; let's do it a funny way to make a point
id = combinatorS combinatorK (combinatorK {_} {Zero})
--                          no choice for -^   ^^^^- could be anything

naughtE : {X : Set} -> Zero -> X
naughtE ()

-- standard composition: f << g is "f after g"
_<<_ : {X Y Z : Set} -> (Y -> Z) -> (X -> Y) -> (X -> Z)
(f << g) x = f (g x)

-- diagrammatic composition: f >> g is "f then g"
_>>_ : {X Y Z : Set} -> (X -> Y) -> (Y -> Z) -> (X -> Z)
                     --       ^^^^^^^^          dominoes!
(f >> g) x = g (f x)

-- infix application
_$_ : {S : Set}{T : S -> Set}(f : (x : S) -> T x)(s : S) -> T s
f $ s = f s
infixl 2 _$_

------------------------------------------------------------------------------
-- from logic to data
------------------------------------------------------------------------------

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}
--  ^^^^^^^^^^^^^^^^^^^       this pragma lets us use decimal notation

_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)      -- there are other choices

four : Nat
four = 2 +N 2

------------------------------------------------------------------------------
-- and back to logic
------------------------------------------------------------------------------

data _==_ {X : Set} : X -> X -> Set where
  refl : (x : X) -> x == x           -- the relation that's "only reflexive"

{-# BUILTIN EQUALITY _==_ #-}  -- we'll see what that's for, later

_=$=_ : {X Y : Set}{f f' : X -> Y}{x x' : X} ->
        f == f' -> x == x' -> f x == f' x'
refl f =$= refl x = refl (f x)
infixl 2 _=$=_

zero-+N : (n : Nat) -> (zero +N n) == n
zero-+N n = refl n

+N-zero : (n : Nat) -> (n +N zero) == n
+N-zero zero     = refl zero
+N-zero (suc n)  = refl suc =$= +N-zero n

assocLR-+N : (x y z : Nat) -> ((x +N y) +N z) == (x +N (y +N z))
assocLR-+N zero    y z = refl (y +N z)
assocLR-+N (suc x) y z = refl suc =$= assocLR-+N x y z

------------------------------------------------------------------------------
-- computing types
------------------------------------------------------------------------------

_>=_ : Nat -> Nat -> Set
x     >= zero   = One
zero  >= suc y  = Zero
suc x >= suc y  = x >= y

refl->= : (n : Nat) -> n >= n
refl->= zero    = record {}
refl->= (suc n) = refl->= n

trans->= : (x y z : Nat) -> x >= y -> y >= z -> x >= z
trans->=      x       y  zero    x>=y y>=z = record {}
trans->=      x  zero    (suc z) x>=y ()
trans->= zero    (suc y) (suc z) ()   y>=z
trans->= (suc x) (suc y) (suc z) x>=y y>=z = trans->= x y z x>=y y>=z

------------------------------------------------------------------------------
-- construction by proof
------------------------------------------------------------------------------

{- -- MOVED UP TO REPLACE _*_
record Sg (S : Set)(T : S -> Set) : Set where  -- Sg is short for "Sigma"
  constructor _,_
  field -- introduces a bunch of fields, listed with their types
    fst : S
    snd : T fst
-- make _*_ from Sg ?
_*_ : Set -> Set -> Set
S * T = Sg S \ _ -> T
-}

difference : (m n : Nat) -> m >= n -> Sg Nat \ d -> m == (n +N d)
                                   --       (                    )
difference m       zero    m>=n = m , refl m
difference zero    (suc n) ()
difference (suc m) (suc n) m>=n with difference m n m>=n
difference (suc m) (suc n) m>=n | d , q = d , (refl suc =$= q)

tryMe      = difference 42 37 _
-- don'tTryMe = difference 37 42 {!!}

------------------------------------------------------------------------------
-- things to remember to say
------------------------------------------------------------------------------

-- why the single colon?

-- what's with all the spaces?

-- what's with identifiers mixing letters and symbols?

-- what's with all the braces?

-- what is Set?

-- are there any lowercase/uppercase conventions?

-- what's with all the underscores?
--   (i)   placeholders in mixfix operators
--   (ii)  don't care (on the left)
--   (iii) go figure (on the right)

-- why use arithmetic operators for types?

-- what's the difference between = and == ?

-- can't we leave out cases?

-- can't we loop?

-- the function type is both implication and universal quantification,
-- but why is it called Pi?

-- why is Sigma called Sigma?

-- B or nor B?

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym3 where

open import Symmetric
open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import FLutil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin
open import Data.Fin.Permutation hiding (_∘ₚ_)

infixr  200 _∘ₚ_
_∘ₚ_ = Data.Fin.Permutation._∘ₚ_

sym3solvable : solvable (Symmetric 3)
solvable.dervied-length sym3solvable = 2
solvable.end sym3solvable x d = solved1 x d where

   open import Data.List using ( List ; [] ; _∷_ )

   open Solvable (Symmetric 3)

   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
   p0id = pleq _ _ refl

   p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
   p1 =  FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0)))
   p2 =  FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0)))
   p3 =  FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
   p4 =  FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
   p5 =  FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0)))
   t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ []

   t1  =  plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷  plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷  plist [ p5 , p1 ] ∷
          plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷  plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷  plist [ p5 , p1 ] ∷
          plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷  plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷  plist [ p5 , p2 ] ∷
          plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷  plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷  plist [ p5 , p3 ] ∷
          plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷  plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p4 ] ∷
          plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷  plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p5 ] ∷
          []

   open _=p=_

   stage1 :  (x : Permutation 3 3) →  Set (Level.suc Level.zero)
   stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤)  x

   open import logic

   p33=4 : ( p3  ∘ₚ p3 ) =p= p4
   p33=4 = pleq _ _ refl

   p44=3 : ( p4  ∘ₚ p4 ) =p= p3
   p44=3 = pleq _ _ refl

   p34=0 : ( p3  ∘ₚ p4 ) =p= pid
   p34=0 = pleq _ _ refl

   p43=0 : ( p4  ∘ₚ p3 ) =p= pid
   p43=0 = pleq _ _ refl

   com33 : [ p3 , p3 ] =p= pid
   com33 = pleq _ _ refl

   com44 : [ p4 , p4 ] =p= pid
   com44 = pleq _ _ refl

   com34 : [ p3 , p4 ] =p= pid
   com34 = pleq _ _ refl

   com43 : [ p4 , p3 ] =p= pid
   com43 = pleq _ _ refl

   pFL : ( g : Permutation 3 3) → { x : FL 3 } →  perm→FL g ≡ x → g =p=  FL→perm x
   pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )

   open ≡-Reasoning

--   st01 : ( x y : Permutation 3 3) →   x =p= p3 →  y =p= p3 → x ∘ₚ  y =p= p4
--   st01 x y s t = record { peq = λ q → ( begin
--         (x ∘ₚ y) ⟨$⟩ʳ q
--       ≡⟨ peq ( presp s t ) q ⟩
--          ( p3  ∘ₚ p3 ) ⟨$⟩ʳ q
--       ≡⟨ peq  p33=4 q  ⟩
--         p4 ⟨$⟩ʳ q
--       ∎ ) }

   st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm  ((suc (suc zero)) :: (suc zero) :: (zero :: f0))  ]

   st02 :  ( g h : Permutation 3 3) →  ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
   st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
   ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
   ... | s | (zero :: (zero :: (zero :: f0))) | se |  record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
   ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (suc zero) :: (suc zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =
        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )

   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (suc (suc zero)) :: (zero :: (zero :: f0 ))| record { eq = ge } |  record { eq = he } =
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } |  record { eq = he } =
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
          case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
            case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } |  record { eq = he } =
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | ((suc zero) :: (zero :: (zero :: f0 ))) |  (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =
            case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } |  record { eq = he } =
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } |  record { eq = he } =
          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
          case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } |  record { eq = he } =
          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } |  record { eq = he } =
          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
          case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 )))  | record { eq = ge } |  record { eq = he } =
          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 ))  | record { eq = ge } |  record { eq = he } =
          case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))

   stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
   stage12 x (comm {g} {h} x1 y1 ) = st02 g h
   stage12 _ (ccong {y} x=y sx) with stage12 y sx
   ... | case1 id = case1 ( ptrans (psym x=y ) id )
   ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
   ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))

   solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
   solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d
   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
      cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
      cc q = begin
             x ⟨$⟩ʳ q
          ≡⟨ sym (f=g q) ⟩
             f ⟨$⟩ʳ q
          ≡⟨ f=e q ⟩
             q
          ∎
   solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
   ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
   ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
   ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
   ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com33 q) }
   ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com44 q) }
   ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com34 q) }
   ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com43 q) }

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
{-# OPTIONS --allow-unsolved-metas #-} -- FIXME

open import Everything

module Test.Test2 where

  failed-test test-functor-transextensionality test-the-test : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔯₁} {_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
    {ℓ₁} {_∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁}
    {ε₁ : Reflexivity.type _∼₁_}
    {_↦₁_ : Transitivity.type _∼₁_}
    {𝔬₂} {𝔒₂ : Ø 𝔬₂}
    {𝔯₂} {_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
    {ℓ₂} {_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂}
    {ε₂ : Reflexivity.type _∼₂_}
    {_↦₂_ : Transitivity.type _∼₂_}
    {surjection : Surjection.type 𝔒₁ 𝔒₂}
    {smap : Smap.type _∼₁_ _∼₂_ surjection surjection}
    ⦃ I : IsFunctor _∼₁_ _∼̇₁_ ε₁ _↦₁_ _∼₂_ _∼̇₂_ ε₂ _↦₂_ smap ⦄
    ⦃ J : IsFunctor _∼₁_ _∼̇₁_ ε₁ _↦₁_ _∼₂_ _∼̇₂_ ε₂ _↦₂_ smap ⦄
    → Transextensionality.type _∼₁_ _∼̇₁_ _↦₁_

  failed-test = transextensionality

  test-functor-transextensionality {_∼₁_ = _∼₁_} {_∼̇₁_ = _∼̇₁_} {_↦₁_ = _↦₁_} {{I}} = transextensionality {_∼_ = λ z z₁ → z ∼₁ z₁} {_∼̇_ = λ {x} {y} → _∼̇₁_ {x} {y}} {transitivity = λ {x y z} → _↦₁_ {x} {y} {z}} {{I .IsFunctor.`IsCategory₁ .IsCategory.`IsPrecategory .IsPrecategory.`𝓣ransextensionality}} -- FIXME can this be simplified?

  test-the-test {_∼₁_ = _∼₁_} {_∼̇₁_ = _∼̇₁_} {_↦₁_ = _↦₁_} = test-functor-transextensionality {_∼₁_ = _∼₁_} {_∼̇₁_ = _∼̇₁_} {_↦₁_ = _↦₁_}


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Definition of natural numbers and operations on them.            --
----------------------------------------------------------------------

module Basics.Nat where

open import Basics.Bool

-- Nat represents natural numbers (starting with 0)
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

-- We define a constant 1 as it will be useful later on
one : Nat
one = suc zero

-- Addition
_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)

infixl 6 _+_

-- Comparisons needed in our code
_<_ : Nat → Nat → Bool
n     < zero  = false
zero  < suc n = true
suc n < suc m = n < m

_≥_ : Nat → Nat → Bool
m     ≥ zero  = true
zero  ≥ suc n = false
suc m ≥ suc n = m ≥ n

infixl 4 _<_ _≥_

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
open import Common.Reflect
open import Common.Prelude
open import Common.Equality

data Maybe A : Set where
  nothing : Maybe A
  just : A → Maybe A

_<$>_ : ∀ {A B} → (A → B) → Maybe A → Maybe B
f <$> just x  = just (f x)
f <$> nothing = nothing

_==_ = primQNameEquality

-- This is awkward!
awkwardUnquoteNat : Term → Maybe Nat
awkwardUnquoteNat (con z []) =
  if z == quote Nat.zero
  then just 0
  else nothing
awkwardUnquoteNat (con s (arg _ n ∷ [])) =
  if s == quote Nat.suc
  then suc <$> awkwardUnquoteNat n
  else nothing
awkwardUnquoteNat v = nothing

testAwkward : just 10 ≡ awkwardUnquoteNat (quoteTerm 10)
testAwkward = refl

-- This is nicer!
pattern `zero  = con (quote Nat.zero) []
pattern `suc n = con (quote Nat.suc) (arg _ n ∷ [])

unquoteNat : Term → Maybe Nat
unquoteNat `zero    = just zero
unquoteNat (`suc n) = suc <$> unquoteNat n
unquoteNat _        = nothing

test : just 10 ≡ unquoteNat (quoteTerm 10)
test = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Testing where

data Nat : Set where
    zero : Nat
    suc : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

plus : Nat -> Nat -> Nat
plus zero n = n
plus (suc m) n = suc (plus m n)

times : Nat -> Nat -> Nat
times zero n = zero
times (suc m) n = plus n (times m n)

data List (A : Set) : Nat -> Set where
    nil : List A 0
    cons : {n : Nat} -> A -> List A n -> List A (suc n)

f : Nat -> (b : Nat) -> (a : Nat) -> Nat
f x = plus

-- Push argument doesn't work with implicit
-- Toggle implicit generates code that the tool can't handle
-- also, want to include {something = x} in language

map : {n : Nat} -> {A : Set} -> {B : Set} -> {renameMe0 : A -> B} -> List A n ->
    List B n
map {renameMe0 = f} nil = nil
map {renameMe0 = f} (cons x xs) = cons (f x) (map {_} {_} {_} {f} xs)

map2 : {n : Nat} -> {A : Set} -> {B : Set} -> (A -> B) -> List A n ->
    List B n
map2 f nil = nil
map2 f (cons x xs) = cons (f x) (map2 f xs)
{-
data Eq {A : Set} (x : A) : A -> Set where
  refl : Eq x x

subst : {A : Set} -> (P : A -> Set) ->
        {x : A} -> {y : A} -> Eq x y -> P x -> P y
subst P refl px = px

data Foo : Set where
  foo : Foo
  bar : Foo

-- Refactoring to introduce these!
{-# FOREIGN GHC data Foo = Foo | Bar #-}
{-# COMPILE GHC Foo = data Foo (Foo | Bar) #-}
-}


text:
-- Andreas, 2020-03-26, issue #4481, reported by gallais

-- #952 unintentionally added named lambdas, but without updating the type-checker.

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.term.expr.top:15 #-}
-- {-# OPTIONS -v tc.term.lambda:30 #-}

open import Agda.Primitive

-- In Agda 2.6.0 and 2.6.1, this is a fake inconsistency proof:

data ⊥ : Set where
record ⊤ : Set where

proj2 : ∀ a {A B : Set a} → Set a
proj2 = λ _ {B = B} → B

agdaIsInconsistent : proj2 lzero {⊤} {⊥}
agdaIsInconsistent = _  -- should be yellow in > 2.6.1

-- The following should complain about unexpected implicit argument:

_ : Set → {A B : Set} → Set
_ = λ _ {C = B} {A} → A  -- should fail

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- Andreas, 2014-03-02, issue and test case by Nisse

-- {-# OPTIONS --show-implicit -v tc.meta.assign:25 -v tc.meta.occurs:70 -v tc.meta.kill:30 #-}
-- {-# OPTIONS -v tc:10 #-}

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

postulate
  A : Set
  D : A → Set

data P : ∀ {xP} → D xP → Set where
  c : ∀ {xc} (dc : D xc) → P dc

module M (f : ∀ {x} → D x → Σ A D)
         (_ : ∀ {xM} (dM : D xM) → P (proj₂ (f dM)))
  where

  postulate
    p : ∀ {x} → D x → A
    q : ∀ {x} {d : D x} → D (p d)

p : ∀ {x} → D x → A
p = M.p (λ x → _ , x) c

q : ∀ {xq} {dq : D xq} → D (p dq)
q = M.q _ c

-- WAS: Unsound pruning of metas under projections
--
-- Cannot instantiate the metavariable _49 to solution d since it
-- contains the variable d which is not in scope of the metavariable
-- or irrelevant in the metavariable but relevant in the solution
-- when checking that the expression c has type ((d : D .x₁) → P _49)

-- NOW: type-checks fine

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --safe #-}

module NormalForm where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp; i0; i1)
open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Univalence  using (ua)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract; isoToEquiv)

open import Data.Bool       using (Bool; false; true; if_then_else_)
open import Data.Integer    using (ℤ; +_; -[1+_])
open import Data.Fin        using (Fin; toℕ; #_; _≟_) renaming (zero to fz; suc to fs)
open import Data.List       using (List; []; _∷_; foldr; length; map)
open import Data.Maybe      using (Maybe; just; nothing) renaming (map to mmap)
open import Data.Nat        using (ℕ; zero; suc; pred; _+_; _*_; _∸_; _≡ᵇ_; _>_; _<ᵇ_)
open import Data.Nat.DivMod using (_mod_; _div_)
open import Data.Product    using (_×_; _,_; proj₁)
open import Data.Vec        using (Vec; []; _∷_; lookup; replicate; _[_]%=_; toList) renaming (map to vmap)

open import Relation.Nullary using (yes; no)

open import BitVec          using (BitVec; insert; empty; show)
open import Util
open import Pitch
open import Interval

_≤[]_ : List ℕ → List ℕ → Bool
[]       ≤[] ys = true
(x ∷ xs) ≤[] [] = false
(x ∷ xs) ≤[] (y ∷ ys) =
  if x ≡ᵇ y
  then xs ≤[] ys
  else (if x <ᵇ y then true else false)

_≤[opci]_ : List PitchClass → List PitchClass → Bool
_≤[opci]_ xs ys =
  (map (toℕ ∘ unOrderedIntervalClass) (pcIntervals xs)) ≤[]
  (map (toℕ ∘ unOrderedIntervalClass) (pcIntervals ys))

bestPitchClassList : List PitchClass → List (List PitchClass) → List PitchClass
bestPitchClassList xs         []         = xs
bestPitchClassList []         (ys ∷ yss) = bestPitchClassList ys yss
bestPitchClassList xs@(_ ∷ _) (ys ∷ yss) =
  if xs ≤[opci] ys
  then bestPitchClassList xs yss
  else bestPitchClassList ys yss

normalForm : PitchClassSet → List PitchClass
normalForm pcs =
  let xs  = fromPitchClassSet pcs
  in bestPitchClassList [] (iter rotateLeft (pred (length xs)) xs)

bestNormalForm : PitchClassSet → List PitchClass
bestNormalForm pcs =
  let xs = normalForm pcs
      ys = normalForm (I pcs)
  in if xs ≤[opci] ys then xs else ys

primeForm : PitchClassSet → List PitchClass
primeForm pcs with bestNormalForm pcs
... | []                    = []
... | xs@(pitchClass p ∷ _) = map (Tp (toℕ (opposite p))) xs

-- Test

--ss = vmap pitchClass (# 4 ∷ # 7 ∷ # 9 ∷ [])
ss = vmap pitchClass (# 2 ∷ # 0 ∷ # 5 ∷ # 6 ∷ [])
--ss = vmap pitchClass (# 8 ∷ # 9 ∷ # 11 ∷ # 0 ∷ # 4 ∷ [])
--ss = vmap pitchClass (# 8 ∷ # 7 ∷ # 4 ∷ # 3 ∷ # 11 ∷ # 0 ∷ [])

aa = show (toPitchClassSet (toList ss))
bb = fromPitchClassSet (toPitchClassSet (toList ss))
cc = map (toℕ ∘ unPitchClass) (normalForm (toPitchClassSet (toList ss)))
dd = map (toℕ ∘ unPitchClass) (bestNormalForm (toPitchClassSet (toList ss)))
ee = map (toℕ ∘ unPitchClass) (primeForm (toPitchClassSet (toList ss)))
ff = icVector (primeForm (toPitchClassSet (toList ss)))
gg = map (toℕ ∘ unPitchClass) (fromPitchClassSet (T 8 (toPitchClassSet (toList ss))))

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Data.Bool using ( Bool )
open import Data.String using ( String )
open import Data.Word using ( Byte )
open import Data.Natural using ( Natural )

module Data.ByteString.Primitive where

postulate
  ByteStringLazy : Set
  ByteStringLazy² : Set
  emptyLazy : ByteStringLazy
  consLazy : Byte → ByteStringLazy → ByteStringLazy
  snocLazy : ByteStringLazy → Byte → ByteStringLazy
  appendLazy : ByteStringLazy → ByteStringLazy → ByteStringLazy
  lengthLazy : ByteStringLazy → Natural
  nullLazy : ByteStringLazy → Bool
  spanLazy : (Byte → Bool) → ByteStringLazy →  ByteStringLazy²
  breakLazy : (Byte → Bool) → ByteStringLazy →  ByteStringLazy²
  lazy₁ : ByteStringLazy² → ByteStringLazy
  lazy₂ : ByteStringLazy² → ByteStringLazy

{-# IMPORT Data.ByteString.Lazy #-}
{-# COMPILED_TYPE ByteStringLazy Data.ByteString.Lazy.ByteString #-}
{-# COMPILED_TYPE ByteStringLazy² (Data.ByteString.Lazy.ByteString,Data.ByteString.Lazy.ByteString) #-}
{-# COMPILED emptyLazy Data.ByteString.Lazy.empty #-}
{-# COMPILED consLazy Data.ByteString.Lazy.cons #-}
{-# COMPILED snocLazy Data.ByteString.Lazy.snoc #-}
{-# COMPILED appendLazy Data.ByteString.Lazy.append #-}
{-# COMPILED lengthLazy fromIntegral . Data.ByteString.Lazy.length #-}
{-# COMPILED nullLazy Data.ByteString.Lazy.null #-}
{-# COMPILED spanLazy Data.ByteString.Lazy.span #-}
{-# COMPILED breakLazy Data.ByteString.Lazy.break #-}
{-# COMPILED lazy₁ \ ( x , y ) -> x #-}
{-# COMPILED lazy₂ \ ( x , y ) -> y #-}

postulate
  ByteStringStrict : Set
  ByteStringStrict² : Set
  emptyStrict : ByteStringStrict
  consStrict : Byte → ByteStringStrict → ByteStringStrict
  snocStrict : ByteStringStrict → Byte → ByteStringStrict
  appendStrict : ByteStringStrict → ByteStringStrict → ByteStringStrict
  lengthStrict : ByteStringStrict → Natural
  nullStrict : ByteStringStrict → Bool
  spanStrict : (Byte → Bool) → ByteStringStrict →  ByteStringStrict²
  breakStrict : (Byte → Bool) → ByteStringStrict →  ByteStringStrict²
  strict₁ : ByteStringStrict² → ByteStringStrict
  strict₂ : ByteStringStrict² → ByteStringStrict

{-# IMPORT Data.ByteString #-}
{-# COMPILED_TYPE ByteStringStrict Data.ByteString.ByteString #-}
{-# COMPILED_TYPE ByteStringStrict² (Data.ByteString.ByteString,Data.ByteString.ByteString) #-}
{-# COMPILED emptyStrict Data.ByteString.empty #-}
{-# COMPILED consStrict Data.ByteString.cons #-}
{-# COMPILED snocStrict Data.ByteString.snoc #-}
{-# COMPILED appendStrict Data.ByteString.append #-}
{-# COMPILED lengthStrict fromIntegral . Data.ByteString.length #-}
{-# COMPILED nullStrict Data.ByteString.null #-}
{-# COMPILED spanStrict Data.ByteString.span #-}
{-# COMPILED breakStrict Data.ByteString.break #-}
{-# COMPILED strict₁ \ ( x , y ) -> x #-}
{-# COMPILED strict₂ \ ( x , y ) -> y #-}

postulate
  mkLazy : ByteStringStrict → ByteStringLazy
  mkStrict : ByteStringLazy → ByteStringStrict

{-# COMPILED mkStrict (Data.ByteString.concat . Data.ByteString.Lazy.toChunks) #-}
{-# COMPILED mkLazy (\ bs -> Data.ByteString.Lazy.fromChunks [ bs ]) #-}

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
open import Data.Empty
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.Unit

open import AEff
open import AwaitingComputations
open import EffectAnnotations
open import Preservation
open import Renamings
open import Substitutions
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation

module Progress where

-- WRAPPING PROMISES AROUND A CONTEXT

⟨⟨_⟩⟩ : Ctx → Ctx
⟨⟨ [] ⟩⟩ = []
⟨⟨ Γ ∷ X ⟩⟩ = ⟨⟨ Γ ⟩⟩ ∷ ⟨ X ⟩

-- RESULTS

data RunResult⟨_∣_⟩ (Γ : Ctx) : {C : CType} → ⟨⟨ Γ ⟩⟩ ⊢M⦂ C → Set where

  return   : {X : VType}
             {o : O}
             {i : I}
             (V : ⟨⟨ Γ ⟩⟩ ⊢V⦂ X) →
             ------------------------------------------
             RunResult⟨ Γ ∣ return {o = o} {i = i} V ⟩

  promise  : {X Y : VType}
             {o o' : O}
             {i i' : I}
             {op : Σₛ}
             {p : lkpᵢ op i ≡ just (o' , i')}
             {M : ⟨⟨ Γ ⟩⟩ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o' , i')}
             {N : ⟨⟨ Γ ⟩⟩ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i)} →
             RunResult⟨ Γ ∷ X ∣ N ⟩ →
             ----------------------------------------------------
             RunResult⟨ Γ ∣ promise op ∣ p ↦ M `in N ⟩

  awaiting : {C : CType}
             {Y : VType}
             {y : ⟨ Y ⟩ ∈ ⟨⟨ Γ ⟩⟩}
             {M : ⟨⟨ Γ ⟩⟩ ⊢M⦂ C} →
             y ⧗ M →
             ---------------------
             RunResult⟨ Γ ∣ M ⟩

data CompResult⟨_∣_⟩ (Γ : Ctx) : {C : CType} → ⟨⟨ Γ ⟩⟩ ⊢M⦂ C → Set where

  comp   : {C : CType}
           {M : ⟨⟨ Γ ⟩⟩ ⊢M⦂ C} →
           RunResult⟨ Γ ∣ M ⟩ →
           ---------------------
           CompResult⟨ Γ ∣ M ⟩

  signal : {X : VType}
           {o : O}
           {i : I}
           {op : Σₛ}
           {p : op ∈ₒ o}
           {V : ⟨⟨ Γ ⟩⟩ ⊢V⦂ ``(payload op)}
           {M : ⟨⟨ Γ ⟩⟩ ⊢M⦂ X ! (o , i)} →
           CompResult⟨ Γ ∣ M ⟩ →
           --------------------------------
           CompResult⟨ Γ ∣ ↑ op p V M ⟩

-- PROGRESS THEOREM FOR PROMISE-OPEN COMPUTATIONS

⇒-not-in-ctx : {Γ : Ctx} {X : VType} {C : CType} → X ⇒ C ∈ ⟨⟨ Γ ⟩⟩ → ⊥
⇒-not-in-ctx {Γ ∷ y} (Tl x) =
  ⇒-not-in-ctx x

{- THEOREM 3.3 -}

progress : {Γ : Ctx}
           {C : CType} →
           (M : ⟨⟨ Γ ⟩⟩ ⊢M⦂ C) →
           -------------------------------
           (Σ[ N ∈ ⟨⟨ Γ ⟩⟩ ⊢M⦂ C ] (M ↝ N)
            ⊎
            CompResult⟨ Γ ∣ M ⟩)

progress (return V) =
  inj₂ (comp (return V))
progress (let= M `in N) with progress M
... | inj₁ (M' , r) =
  inj₁ (_ , context (let= [-] `in N) r)
... | inj₂ (comp (return V)) =
  inj₁ (_ , let-return V N)
... | inj₂ (comp (promise {_} {_} {_} {_} {_} {_} {_} {p} {M'} {M''} R)) =
  inj₁ (_ , let-promise p M' M'' N)
... | inj₂ (comp (awaiting R)) =
  inj₂ (comp (awaiting (let-in R)))
... | inj₂ (signal {_} {_} {_} {_} {p} {V} {M'} R) =
  inj₁ (_ , let-↑ p V M' N)
progress (letrec M `in N) =
  inj₁ (_ , letrec-unfold M N)
progress ((` x) · W) with ⇒-not-in-ctx x
... | ()
progress (ƛ M · W) =
  inj₁ (_ , apply M W)
progress (↑ op p V M) with progress M
... | inj₁ (M' , r) =
  inj₁ (_ , context (↑ op p V [-]) r)
... | inj₂ R =
  inj₂ (signal R)
progress (↓ op V M) with progress M
... | inj₁ (M' , r) =
  inj₁ (_ , context (↓ op V [-]) r)
... | inj₂ (comp (return W)) =
  inj₁ (_ , (↓-return V W))
... | inj₂ (comp (awaiting R)) =
  inj₂ (comp (awaiting (interrupt R)))
... | inj₂ (signal {X} {o} {i} {op'} {p} {W} {M'} R) =
  inj₁ (_ , (↓-↑ p V W M'))
... | inj₂ (comp (promise {_} {_} {_} {_} {_} {_} {op'} {p} {M'} {M''} R)) with decₛ op op'
... | yes refl =
  inj₁ (_ , ↓-promise-op p V M' M'')
... | no ¬q =
  inj₁ (_ , ↓-promise-op' ¬q p V M' M'')
progress (promise op ∣ p ↦ M `in N) with progress N
... | inj₁ (M' , r) =
  inj₁ (_ , context (promise op ∣ p ↦ M `in [-]) r)
... | inj₂ (comp R) =
  inj₂ (comp (promise R))
... | inj₂ (signal {_} {_} {_} {_} {q} {V} {M'} R) =
  inj₁ (_ , promise-↑ p q V M M')
progress (await ` x until M) =
  inj₂ (comp (awaiting await))
progress (await ⟨ V ⟩ until M) =
  inj₁ (_ , await-promise V M)
progress (coerce p q M) with progress M
... | inj₁ (M' , r) =
  inj₁ (_ , context (coerce p q [-]) r)
... | inj₂ (comp (return V)) =
  inj₁ (_ , coerce-return V)
... | inj₂ (comp (promise {_} {_} {_} {_} {_} {_} {op'} {r} {M'} {M''} R)) =
  inj₁ (_ , coerce-promise r M' M'')
... | inj₂ (comp (awaiting R)) =
  inj₂ (comp (awaiting (coerce R)))
... | inj₂ (signal {_} {_} {_} {_} {r} {V} {M'} R) =
  inj₁ (_ , coerce-↑ r V M')

-- PROGRESS THEOREM FOR CLOSED COMPUTATIONS

{- COROLLARY 3.4 -}

closed-progress : {C : CType} →
                  (M : [] ⊢M⦂ C) →
                  --------------------------
                  (Σ[ N ∈ [] ⊢M⦂ C ] (M ↝ N)
                   ⊎
                   CompResult⟨ [] ∣ M ⟩)

closed-progress M =
  progress M

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


text:
{-# OPTIONS --without-K --exact-split #-}

module categories where

import 21-image
open 21-image public

{- We introduce precategories and categories. -}

Precat :
  (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Precat l1 l2 =
  Σ (UU l1) (λ Obj → Σ (Obj → Obj → hSet l2) (λ Hom →
    Σ ({X : Obj} → type-Set (Hom X X)) (λ i →
      Σ ( {X Y Z : Obj} →
          type-Set (Hom Y Z) → type-Set (Hom X Y) → type-Set (Hom X Z))
          ( λ comp →
            ( {X Y Z W : Obj} (f : type-Set (Hom X Y)) (g : type-Set (Hom Y Z))
              (h : type-Set (Hom Z W)) →
              Id (comp (comp h g) f) (comp h (comp g f))) ×
            ( ( {X Y : Obj} (f : type-Set (Hom X Y)) → Id (comp i f) f) ×
              ( {X Y : Obj} (f : type-Set (Hom X Y)) → Id (comp f i) f))))))

obj-Precat :
  {l1 l2 : Level} (C : Precat l1 l2) → UU l1
obj-Precat C = pr1 C

hom-Precat :
  {l1 l2 : Level} (C : Precat l1 l2) → obj-Precat C → obj-Precat C → hSet l2
hom-Precat C = pr1 (pr2 C)

id-Precat :
  {l1 l2 : Level} (C : Precat l1 l2)
  {X : obj-Precat C} → type-Set (hom-Precat C X X)
id-Precat C = pr1 (pr2 (pr2 C))

comp-Precat :
  {l1 l2 : Level} (C : Precat l1 l2)
  {X Y Z : obj-Precat C} → type-Set (hom-Precat C Y Z) →
  type-Set (hom-Precat C X Y) → type-Set (hom-Precat C X Z)
comp-Precat C = pr1 (pr2 (pr2 (pr2 C)))

assoc-Precat :
  {l1 l2 : Level} (C : Precat l1 l2)
  {X Y Z W : obj-Precat C} (f : type-Set (hom-Precat C X Y)) →
  ( g : type-Set (hom-Precat C Y Z)) ( h : type-Set (hom-Precat C Z W)) →
  Id (comp-Precat C (comp-Precat C h g) f) (comp-Precat C h (comp-Precat C g f))
assoc-Precat C = pr1 (pr2 (pr2 (pr2 (pr2 C))))

left-unit-Precat :
  {l1 l2 : Level} (C : Precat l1 l2)
  {X Y : obj-Precat C} (f : type-Set (hom-Precat C X Y)) →
  Id (comp-Precat C (id-Precat C) f) f
left-unit-Precat C = pr1 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))

right-unit-Precat :
  {l1 l2 : Level} (C : Precat l1 l2)
  {X Y : obj-Precat C} (f : type-Set (hom-Precat C X Y)) →
  Id (comp-Precat C f (id-Precat C)) f
right-unit-Precat C = pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))

{- We define the notion of isomorphism in a precategory. -}

is-iso-Precat :
  {l1 l2 : Level} (C : Precat l1 l2) {X Y : obj-Precat C} →
  (type-Set (hom-Precat C X Y)) → UU l2
is-iso-Precat C {X} {Y} f =
  Σ ( type-Set (hom-Precat C Y X)) (λ g →
    Id (comp-Precat C f g) (id-Precat C) ×
    Id (comp-Precat C g f) (id-Precat C))

iso-Precat :
  {l1 l2 : Level} (C : Precat l1 l2) →
  obj-Precat C → obj-Precat C → hSet l2
iso-Precat C X Y =
  {!!}

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro