text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties about natural number operations
------------------------------------------------------------------------

-- See README.Data.Nat for some examples showing how this module can be
-- used.

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

module Data.Nat.Properties where

open import Axiom.UniquenessOfIdentityProofs
open import Algebra.Bundles
open import Algebra.Morphism
open import Algebra.Consequences.Propositional
open import Data.Bool.Base using (Bool; false; true; T)
open import Data.Bool.Properties using (T?)
open import Data.Empty
open import Data.Nat.Base
open import Data.Product
open import Data.Sum.Base as Sum
open import Data.Unit using (tt)
open import Function.Base
open import Function.Injection using (_↣_)
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.Consequences using (flip-Connex)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Decidable using (True; via-injection; map′)
open import Relation.Nullary.Negation using (contradiction)

open import Algebra.Definitions {A = ℕ} _≡_
  hiding (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.Definitions
  using (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.Structures {A = ℕ} _≡_

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

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

≡ᵇ⇒≡ : ∀ m n → T (m ≡ᵇ n) → m ≡ n
≡ᵇ⇒≡ zero    zero    _  = refl
≡ᵇ⇒≡ (suc m) (suc n) eq = cong suc (≡ᵇ⇒≡ m n eq)

≡⇒≡ᵇ : ∀ m n → m ≡ n → T (m ≡ᵇ n)
≡⇒≡ᵇ zero    zero    eq = _
≡⇒≡ᵇ (suc m) (suc n) eq = ≡⇒≡ᵇ m n (suc-injective eq)

-- NB: we use the builtin function `_≡ᵇ_` here so that the function
-- quickly decides whether to return `yes` or `no`. It still takes
-- a linear amount of time to generate the proof if it is inspected.
-- We expect the main benefit to be visible in compiled code as the
-- backend erases proofs.

infix 4 _≟_
_≟_ : Decidable {A = ℕ} _≡_
m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))

≡-irrelevant : Irrelevant {A = ℕ} _≡_
≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_

≟-diag : ∀ {m n} (eq : m ≡ n) → (m ≟ n) ≡ yes eq
≟-diag = ≡-≟-identity _≟_

≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
≡-isDecEquivalence = record
  { isEquivalence = isEquivalence
  ; _≟_           = _≟_
  }

≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = record
  { Carrier          = ℕ
  ; _≈_              = _≡_
  ; isDecEquivalence = ≡-isDecEquivalence
  }

0≢1+n : ∀ {n} → 0 ≢ suc n
0≢1+n ()

1+n≢0 : ∀ {n} → suc n ≢ 0
1+n≢0 ()

1+n≢n : ∀ {n} → suc n ≢ n
1+n≢n {suc n} = 1+n≢n ∘ suc-injective

------------------------------------------------------------------------
-- Properties of _<ᵇ_
------------------------------------------------------------------------

<ᵇ⇒< : ∀ m n → T (m <ᵇ n) → m < n
<ᵇ⇒< zero    (suc n) m<n = s≤s z≤n
<ᵇ⇒< (suc m) (suc n) m<n = s≤s (<ᵇ⇒< m n m<n)

<⇒<ᵇ : ∀ {m n} → m < n → T (m <ᵇ n)
<⇒<ᵇ (s≤s z≤n)       = tt
<⇒<ᵇ (s≤s (s≤s m<n)) = <⇒<ᵇ (s≤s m<n)

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

≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-pred (s≤s m≤n) = m≤n

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

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive {zero}  refl = z≤n
≤-reflexive {suc m} refl = s≤s (≤-reflexive refl)

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

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym z≤n       z≤n       = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

≤-trans : Transitive _≤_
≤-trans z≤n       _         = z≤n
≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

≤-total : Total _≤_
≤-total zero    _       = inj₁ z≤n
≤-total _       zero    = inj₂ z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n≤m = inj₂ (s≤s n≤m)

≤-irrelevant : Irrelevant _≤_
≤-irrelevant z≤n        z≤n        = refl
≤-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) = cong s≤s (≤-irrelevant m≤n₁ m≤n₂)

-- NB: we use the builtin function `_<ᵇ_` here so that the function
-- quickly decides whether to return `yes` or `no`. It still takes
-- a linear amount of time to generate the proof if it is inspected.
-- We expect the main benefit to be visible in compiled code as the
-- backend erases proofs.

infix 4 _≤?_ _≥?_

_≤?_ : Decidable _≤_
zero  ≤? _ = yes z≤n
suc m ≤? n = map′ (<ᵇ⇒< m n) <⇒<ᵇ (T? (m <ᵇ n))

_≥?_ : Decidable _≥_
_≥?_ = flip _≤?_

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

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

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

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

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

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

≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
  { isPreorder = ≤-isPreorder
  }

≤-poset : Poset 0ℓ 0ℓ 0ℓ
≤-poset = record
  { isPartialOrder = ≤-isPartialOrder
  }

≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  }

≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
  { isDecTotalOrder = ≤-isDecTotalOrder
  }

------------------------------------------------------------------------
-- Other properties of _≤_

s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
s≤s-injective refl = refl

≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
≤-step z≤n       = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)

n≤1+n : ∀ n → n ≤ 1 + n
n≤1+n _ = ≤-step ≤-refl

1+n≰n : ∀ {n} → 1 + n ≰ n
1+n≰n (s≤s le) = 1+n≰n le

n≤0⇒n≡0 : ∀ {n} → n ≤ 0 → n ≡ 0
n≤0⇒n≡0 z≤n = refl

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

-- Relationships between the various relations

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ (s≤s m≤n) = ≤-trans m≤n (≤-step ≤-refl)

<⇒≢ : _<_ ⇒ _≢_
<⇒≢ m<n refl = 1+n≰n m<n

≤⇒≯ : _≤_ ⇒ _≯_
≤⇒≯ (s≤s m≤n) (s≤s n≤m) = ≤⇒≯ m≤n n≤m

<⇒≱ : _<_ ⇒ _≱_
<⇒≱ (s≤s m+1≤n) (s≤s n≤m) = <⇒≱ m+1≤n n≤m

<⇒≯ : _<_ ⇒ _≯_
<⇒≯ (s≤s m<n) (s≤s n<m) = <⇒≯ m<n n<m

≰⇒≮ : _≰_ ⇒ _≮_
≰⇒≮ m≰n 1+m≤n = m≰n (<⇒≤ 1+m≤n)

≰⇒> : _≰_ ⇒ _>_
≰⇒> {zero}          z≰n = contradiction z≤n z≰n
≰⇒> {suc m} {zero}  _   = s≤s z≤n
≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n ∘ s≤s))

≰⇒≥ : _≰_ ⇒ _≥_
≰⇒≥ = <⇒≤ ∘ ≰⇒>

≮⇒≥ : _≮_ ⇒ _≥_
≮⇒≥ {_}     {zero}  _       = z≤n
≮⇒≥ {zero}  {suc j} 1≮j+1   = contradiction (s≤s z≤n) 1≮j+1
≮⇒≥ {suc i} {suc j} i+1≮j+1 = s≤s (≮⇒≥ (i+1≮j+1 ∘ s≤s))

≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤∧≢⇒< {_} {zero}  z≤n       m≢n     = contradiction refl m≢n
≤∧≢⇒< {_} {suc n} z≤n       m≢n     = s≤s z≤n
≤∧≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
  s≤s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))

≤-<-connex : Connex _≤_ _<_
≤-<-connex m n with m ≤? n
... | yes m≤n = inj₁ m≤n
... | no ¬m≤n = inj₂ (≰⇒> ¬m≤n)

≥->-connex : Connex _≥_ _>_
≥->-connex = flip ≤-<-connex

<-≤-connex : Connex _<_ _≤_
<-≤-connex = flip-Connex ≤-<-connex

>-≥-connex : Connex _>_ _≥_
>-≥-connex = flip-Connex ≥->-connex

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

<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (s≤s n<n) = <-irrefl refl n<n

<-asym : Asymmetric _<_
<-asym (s≤s n<m) (s≤s m<n) = <-asym n<m m<n

<-trans : Transitive _<_
<-trans (s≤s i≤j) (s≤s j<k) = s≤s (≤-trans i≤j (≤-trans (n≤1+n _) j<k))

<-transʳ : Trans _≤_ _<_ _<_
<-transʳ m≤n (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

<-transˡ : Trans _<_ _≤_ _<_
<-transˡ (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

-- NB: we use the builtin function `_<ᵇ_` here so that the function
-- quickly decides which constructor to return. It still takes a
-- linear amount of time to generate the proof if it is inspected.
-- We expect the main benefit to be visible in compiled code as the
-- backend erases proofs.

<-cmp : Trichotomous _≡_ _<_
<-cmp m n with m ≟ n | T? (m <ᵇ n)
... | yes m≡n | _       = tri≈ (<-irrefl m≡n) m≡n (<-irrefl (sym m≡n))
... | no  m≢n | yes m<n = tri< (<ᵇ⇒< m n m<n) m≢n (<⇒≯ (<ᵇ⇒< m n m<n))
... | no  m≢n | no  m≮n = tri> (m≮n ∘ <⇒<ᵇ)   m≢n (≤∧≢⇒< (≮⇒≥ (m≮n ∘ <⇒<ᵇ)) (m≢n ∘ sym))

infix 4 _<?_ _>?_

_<?_ : Decidable _<_
m <? n = suc m ≤? n

_>?_ : Decidable _>_
_>?_ = flip _<?_

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

<-resp₂-≡ : _<_ Respects₂ _≡_
<-resp₂-≡ = subst (_ <_) , subst (_< _)

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

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

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

<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
<-strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder
  }

<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder
  }

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

n≮n : ∀ n → n ≮ n
n≮n n = <-irrefl (refl {x = n})

0<1+n : ∀ {n} → 0 < suc n
0<1+n = s≤s z≤n

n<1+n : ∀ n → n < suc n
n<1+n n = ≤-refl

n≢0⇒n>0 : ∀ {n} → n ≢ 0 → n > 0
n≢0⇒n>0 {zero}  0≢0 =  contradiction refl 0≢0
n≢0⇒n>0 {suc n} _   =  0<1+n

m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
m<n⇒n≢0 (s≤s m≤n) ()

m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
m<n⇒m≤1+n (s≤s z≤n)       = z≤n
m<n⇒m≤1+n (s≤s (s≤s m<n)) = s≤s (m<n⇒m≤1+n (s≤s m<n))

∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
∀[m≤n⇒m≢o]⇒n<o _       zero    m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)
∀[m≤n⇒m≢o]⇒n<o zero    (suc o) _       = 0<1+n
∀[m≤n⇒m≢o]⇒n<o (suc n) (suc o) m≤n⇒n≢o = s≤s (∀[m≤n⇒m≢o]⇒n<o n o rec)
  where
  rec : ∀ {m} → m ≤ n → m ≢ o
  rec m≤n refl = m≤n⇒n≢o (s≤s m≤n) refl

∀[m<n⇒m≢o]⇒n≤o : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
∀[m<n⇒m≢o]⇒n≤o zero    n       _       = z≤n
∀[m<n⇒m≢o]⇒n≤o (suc n) zero    m<n⇒m≢0 = contradiction refl (m<n⇒m≢0 0<1+n)
∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
  where
  rec : ∀ {m} → m < n → m ≢ o
  rec x<m refl = m<n⇒m≢o (s≤s x<m) refl

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

module ≤-Reasoning where
  open import Relation.Binary.Reasoning.Base.Triple
    ≤-isPreorder
    <-trans
    (resp₂ _<_)
    <⇒≤
    <-transˡ
    <-transʳ
    public
    hiding (step-≈; step-≈˘)

open ≤-Reasoning

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

pred-mono : pred Preserves _≤_ ⟶ _≤_
pred-mono z≤n      = z≤n
pred-mono (s≤s le) = le

≤pred⇒≤ : ∀ {m n} → m ≤ pred n → m ≤ n
≤pred⇒≤ {m} {zero}  le = le
≤pred⇒≤ {m} {suc n} le = ≤-step le

≤⇒pred≤ : ∀ {m n} → m ≤ n → pred m ≤ n
≤⇒pred≤ {zero}  le = le
≤⇒pred≤ {suc m} le = ≤-trans (n≤1+n m) le

<⇒≤pred : ∀ {m n} → m < n → m ≤ pred n
<⇒≤pred (s≤s le) = le

suc[pred[n]]≡n : ∀ {n} → n ≢ 0 → suc (pred n) ≡ n
suc[pred[n]]≡n {zero}  n≢0 = contradiction refl n≢0
suc[pred[n]]≡n {suc n} n≢0 = refl

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

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

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

+-assoc : Associative _+_
+-assoc zero    _ _ = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

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

+-identityʳ : RightIdentity 0 _+_
+-identityʳ zero    = refl
+-identityʳ (suc n) = cong suc (+-identityʳ n)

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

+-comm : Commutative _+_
+-comm zero    n = sym (+-identityʳ n)
+-comm (suc m) n = begin-equality
  suc m + n   ≡⟨⟩
  suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
  suc (n + m) ≡⟨ sym (+-suc n m) ⟩
  n + suc m   ∎

+-cancelˡ-≡ : LeftCancellative _≡_ _+_
+-cancelˡ-≡ zero    eq = eq
+-cancelˡ-≡ (suc m) eq = +-cancelˡ-≡ m (cong pred eq)

+-cancelʳ-≡ : RightCancellative _≡_ _+_
+-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡

+-cancel-≡ : Cancellative _≡_ _+_
+-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡

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

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

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

+-isCommutativeSemigroup : IsCommutativeSemigroup _+_
+-isCommutativeSemigroup = record
  { isSemigroup = +-isSemigroup
  ; comm        = +-comm
  }

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

+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0
+-0-isCommutativeMonoid = record
  { isMonoid = +-0-isMonoid
  ; comm     = +-comm
  }

------------------------------------------------------------------------
-- Raw bundles

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

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

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

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

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

+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
  { isCommutativeSemigroup = +-isCommutativeSemigroup
  }

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

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

------------------------------------------------------------------------
-- Other properties of _+_ and _≡_

m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)

m≢1+n+m : ∀ m {n} → m ≢ suc (n + m)
m≢1+n+m m m≡1+n+m = m≢1+m+n m (trans m≡1+n+m (cong suc (+-comm _ m)))

m+1+n≢m : ∀ m {n} → m + suc n ≢ m
m+1+n≢m (suc m) = (m+1+n≢m m) ∘ suc-injective

m+1+n≢0 : ∀ m {n} → m + suc n ≢ 0
m+1+n≢0 m {n} rewrite +-suc m n = λ()

m+n≡0⇒m≡0 : ∀ m {n} → m + n ≡ 0 → m ≡ 0
m+n≡0⇒m≡0 zero eq = refl

m+n≡0⇒n≡0 : ∀ m {n} → m + n ≡ 0 → n ≡ 0
m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))

------------------------------------------------------------------------
-- Properties of _+_ and _≤_/_<_

+-cancelˡ-≤ : LeftCancellative _≤_ _+_
+-cancelˡ-≤ zero    le       = le
+-cancelˡ-≤ (suc m) (s≤s le) = +-cancelˡ-≤ m le

+-cancelʳ-≤ : RightCancellative _≤_ _+_
+-cancelʳ-≤ {m} n o le =
  +-cancelˡ-≤ m (subst₂ _≤_ (+-comm n m) (+-comm o m) le)

+-cancel-≤ : Cancellative _≤_ _+_
+-cancel-≤ = +-cancelˡ-≤ , +-cancelʳ-≤

+-cancelˡ-< : LeftCancellative _<_ _+_
+-cancelˡ-< m {n} {o} = +-cancelˡ-≤ m ∘ subst (_≤ m + o) (sym (+-suc m n))

+-cancelʳ-< : RightCancellative _<_ _+_
+-cancelʳ-< n o n+m<o+m = +-cancelʳ-≤ (suc n) o n+m<o+m

+-cancel-< : Cancellative _<_ _+_
+-cancel-< = +-cancelˡ-< , +-cancelʳ-<

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

≤-stepsʳ : ∀ {m n} o → m ≤ n → m ≤ n + o
≤-stepsʳ {m} o m≤n = subst (m ≤_) (+-comm o _) (≤-stepsˡ o m≤n)

m≤m+n : ∀ m n → m ≤ m + n
m≤m+n zero    n = z≤n
m≤m+n (suc m) n = s≤s (m≤m+n m n)

m≤n+m : ∀ m n → m ≤ n + m
m≤n+m m n = subst (m ≤_) (+-comm m n) (m≤m+n m n)

m≤n⇒m<n∨m≡n :  ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
m≤n⇒m<n∨m≡n {0}     {0}     _          =  inj₂ refl
m≤n⇒m<n∨m≡n {0}     {suc n} _          =  inj₁ 0<1+n
m≤n⇒m<n∨m≡n {suc m} {suc n} (s≤s m≤n)  with m≤n⇒m<n∨m≡n m≤n
... | inj₂ m≡n = inj₂ (cong suc m≡n)
... | inj₁ m<n = inj₁ (s≤s m<n)

m+n≤o⇒m≤o : ∀ m {n o} → m + n ≤ o → m ≤ o
m+n≤o⇒m≤o zero    m+n≤o       = z≤n
m+n≤o⇒m≤o (suc m) (s≤s m+n≤o) = s≤s (m+n≤o⇒m≤o m m+n≤o)

m+n≤o⇒n≤o : ∀ m {n o} → m + n ≤ o → n ≤ o
m+n≤o⇒n≤o zero    n≤o   = n≤o
m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)

+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+-mono-≤ {_} {m} z≤n       o≤p = ≤-trans o≤p (m≤n+m _ m)
+-mono-≤ {_} {_} (s≤s m≤n) o≤p = s≤s (+-mono-≤ m≤n o≤p)

+-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
+-monoˡ-≤ n m≤o = +-mono-≤ m≤o (≤-refl {n})

+-monoʳ-≤ : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_
+-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o

+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
+-mono-<-≤ {_} {suc n} (s≤s z≤n)       o≤p = s≤s (≤-stepsˡ n o≤p)
+-mono-<-≤ {_} {_}     (s≤s (s≤s m<n)) o≤p = s≤s (+-mono-<-≤ (s≤s m<n) o≤p)

+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
+-mono-≤-< {_} {n} z≤n       o<p = ≤-trans o<p (m≤n+m _ n)
+-mono-≤-< {_} {_} (s≤s m≤n) o<p = s≤s (+-mono-≤-< m≤n o<p)

+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+-mono-< m≤n = +-mono-≤-< (<⇒≤ m≤n)

+-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
+-monoˡ-< n = +-monoˡ-≤ n

+-monoʳ-< : ∀ n → (n +_) Preserves _<_ ⟶ _<_
+-monoʳ-< zero    m≤o = m≤o
+-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)

m+1+n≰m : ∀ m {n} → m + suc n ≰ m
m+1+n≰m (suc m) le = m+1+n≰m m (≤-pred le)

m<m+n : ∀ m {n} → n > 0 → m < m + n
m<m+n zero    n>0 = n>0
m<m+n (suc m) n>0 = s≤s (m<m+n m n>0)

m<n+m : ∀ m {n} → n > 0 → m < n + m
m<n+m m {n} n>0 rewrite +-comm n m = m<m+n m n>0

m+n≮n : ∀ m n → m + n ≮ n
m+n≮n zero    n                   = n≮n n
m+n≮n (suc m) (suc n) (s≤s m+n<n) = m+n≮n m (suc n) (≤-step m+n<n)

m+n≮m : ∀ m n → m + n ≮ m
m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)

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

*-suc : ∀ m n → m * suc n ≡ m + m * n
*-suc zero    n = refl
*-suc (suc m) n = begin-equality
  suc m * suc n         ≡⟨⟩
  suc n + m * suc n     ≡⟨ cong (suc n +_) (*-suc m n) ⟩
  suc n + (m + m * n)   ≡⟨⟩
  suc (n + (m + m * n)) ≡⟨ cong suc (sym (+-assoc n m (m * n))) ⟩
  suc (n + m + m * n)   ≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
  suc (m + n + m * n)   ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
  suc (m + (n + m * n)) ≡⟨⟩
  suc m + suc m * n     ∎

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

*-identityˡ : LeftIdentity 1 _*_
*-identityˡ n = +-identityʳ n

*-identityʳ : RightIdentity 1 _*_
*-identityʳ zero    = refl
*-identityʳ (suc n) = cong suc (*-identityʳ n)

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

*-zeroˡ : LeftZero 0 _*_
*-zeroˡ _ = refl

*-zeroʳ : RightZero 0 _*_
*-zeroʳ zero    = refl
*-zeroʳ (suc n) = *-zeroʳ n

*-zero : Zero 0 _*_
*-zero = *-zeroˡ , *-zeroʳ

*-comm : Commutative _*_
*-comm zero    n = sym (*-zeroʳ n)
*-comm (suc m) n = begin-equality
  suc m * n  ≡⟨⟩
  n + m * n  ≡⟨ cong (n +_) (*-comm m n) ⟩
  n + n * m  ≡⟨ sym (*-suc n m) ⟩
  n * suc m  ∎

*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ m zero    o = refl
*-distribʳ-+ m (suc n) o = begin-equality
  (suc n + o) * m     ≡⟨⟩
  m + (n + o) * m     ≡⟨ cong (m +_) (*-distribʳ-+ m n o) ⟩
  m + (n * m + o * m) ≡⟨ sym (+-assoc m (n * m) (o * m)) ⟩
  m + n * m + o * m   ≡⟨⟩
  suc n * m + o * m   ∎

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

*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

*-assoc : Associative _*_
*-assoc zero    n o = refl
*-assoc (suc m) n o = begin-equality
  (suc m * n) * o     ≡⟨⟩
  (n + m * n) * o     ≡⟨ *-distribʳ-+ o n (m * n) ⟩
  n * o + (m * n) * o ≡⟨ cong (n * o +_) (*-assoc m n o) ⟩
  n * o + m * (n * o) ≡⟨⟩
  suc m * (n * o)     ∎

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

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

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

*-isCommutativeSemigroup : IsCommutativeSemigroup _*_
*-isCommutativeSemigroup = record
  { isSemigroup = *-isSemigroup
  ; comm        = *-comm
  }

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

*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1
*-1-isCommutativeMonoid = record
  { isMonoid = *-1-isMonoid
  ; comm     = *-comm
  }

*-+-isSemiring : IsSemiring _+_ _*_ 0 1
*-+-isSemiring = record
  { isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-0-isCommutativeMonoid
    ; *-isMonoid            = *-1-isMonoid
    ; distrib               = *-distrib-+
    }
  ; zero = *-zero
  }

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

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

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

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

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

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

*-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
*-commutativeSemigroup = record
  { isCommutativeSemigroup = *-isCommutativeSemigroup
  }

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

*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
  { isCommutativeMonoid = *-1-isCommutativeMonoid
  }

*-+-semiring : Semiring 0ℓ 0ℓ
*-+-semiring = record
  { isSemiring = *-+-isSemiring
  }

*-+-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
*-+-commutativeSemiring = record
  { isCommutativeSemiring = *-+-isCommutativeSemiring
  }

------------------------------------------------------------------------
-- Other properties of _*_ and _≡_

*-cancelʳ-≡ : ∀ m n {o} → m * suc o ≡ n * suc o → m ≡ n
*-cancelʳ-≡ zero    zero        eq = refl
*-cancelʳ-≡ (suc m) (suc n) {o} eq =
  cong suc (*-cancelʳ-≡ m n (+-cancelˡ-≡ (suc o) eq))

*-cancelˡ-≡ : ∀ {m n} o → suc o * m ≡ suc o * n → m ≡ n
*-cancelˡ-≡ {m} {n} o eq = *-cancelʳ-≡ m n
  (subst₂ _≡_ (*-comm (suc o) m) (*-comm (suc o) n) eq)

m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
m*n≡0⇒m≡0∨n≡0 zero    {n}     eq = inj₁ refl
m*n≡0⇒m≡0∨n≡0 (suc m) {zero}  eq = inj₂ refl

m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1
m*n≡1⇒m≡1 (suc zero)    n             _  = refl
m*n≡1⇒m≡1 (suc (suc m)) (suc zero)    ()
m*n≡1⇒m≡1 (suc (suc m)) zero          eq =
  contradiction (trans (sym $ *-zeroʳ m) eq) λ()

m*n≡1⇒n≡1 : ∀ m n → m * n ≡ 1 → n ≡ 1
m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)

------------------------------------------------------------------------
-- Other properties of _*_ and _≤_/_<_

*-cancelʳ-≤ : ∀ m n o → m * suc o ≤ n * suc o → m ≤ n
*-cancelʳ-≤ zero    _       _ _  = z≤n
*-cancelʳ-≤ (suc m) (suc n) o le =
  s≤s (*-cancelʳ-≤ m n o (+-cancelˡ-≤ (suc o) le))

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

*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
*-mono-≤ z≤n       _   = z≤n
*-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)

*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n})

*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o

*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
*-mono-< (s≤s z≤n)       (s≤s u≤v) = s≤s z≤n
*-mono-< (s≤s (s≤s m≤n)) (s≤s u≤v) =
  +-mono-< (s≤s u≤v) (*-mono-< (s≤s m≤n) (s≤s u≤v))

*-monoˡ-< : ∀ n → (_* suc n) Preserves _<_ ⟶ _<_
*-monoˡ-< n (s≤s z≤n)       = s≤s z≤n
*-monoˡ-< n (s≤s (s≤s m≤o)) =
  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< n (s≤s m≤o))

*-monoʳ-< : ∀ n → (suc n *_) Preserves _<_ ⟶ _<_
*-monoʳ-< zero    (s≤s m≤o) = +-mono-≤ (s≤s m≤o) z≤n
*-monoʳ-< (suc n) (s≤s m≤o) =
  +-mono-≤ (s≤s m≤o) (<⇒≤ (*-monoʳ-< n (s≤s m≤o)))

m≤m*n : ∀ m {n} → 0 < n → m ≤ m * n
m≤m*n m {n} 0<n = begin
  m     ≡⟨ sym (*-identityʳ m) ⟩
  m * 1 ≤⟨ *-monoʳ-≤ m 0<n ⟩
  m * n ∎

m<m*n :  ∀ {m n} → 0 < m → 1 < n → m < m * n
m<m*n {m@(suc m-1)} {n@(suc (suc n-2))} (s≤s _) (s≤s (s≤s _)) = begin-strict
  m           <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
  n + m-1     ≤⟨ +-monoʳ-≤ n (m≤m*n m-1 0<1+n) ⟩
  n + m-1 * n ≡⟨⟩
  m * n       ∎

*-cancelʳ-< : RightCancellative _<_ _*_
*-cancelʳ-< {zero}  zero    (suc o) _     = 0<1+n
*-cancelʳ-< {suc m} zero    (suc o) _     = 0<1+n
*-cancelʳ-< {m}     (suc n) (suc o) nm<om =
  s≤s (*-cancelʳ-< n o (+-cancelˡ-< m nm<om))

-- Redo in terms of `comm+cancelʳ⇒cancelˡ` when generalised
*-cancelˡ-< : LeftCancellative _<_ _*_
*-cancelˡ-< x {y} {z} rewrite *-comm x y | *-comm x z = *-cancelʳ-< y z

*-cancel-< : Cancellative _<_ _*_
*-cancel-< = *-cancelˡ-< , *-cancelʳ-<

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

^-identityʳ : RightIdentity 1 _^_
^-identityʳ zero    = refl
^-identityʳ (suc n) = cong suc (^-identityʳ n)

^-zeroˡ : LeftZero 1 _^_
^-zeroˡ zero    = refl
^-zeroˡ (suc n) = begin-equality
  1 ^ suc n   ≡⟨⟩
  1 * (1 ^ n) ≡⟨ *-identityˡ (1 ^ n) ⟩
  1 ^ n       ≡⟨ ^-zeroˡ n ⟩
  1           ∎

^-distribˡ-+-* : ∀ m n o → m ^ (n + o) ≡ m ^ n * m ^ o
^-distribˡ-+-* m zero    o = sym (+-identityʳ (m ^ o))
^-distribˡ-+-* m (suc n) o = begin-equality
  m * (m ^ (n + o))       ≡⟨ cong (m *_) (^-distribˡ-+-* m n o) ⟩
  m * ((m ^ n) * (m ^ o)) ≡⟨ sym (*-assoc m _ _) ⟩
  (m * (m ^ n)) * (m ^ o) ∎

^-semigroup-morphism : ∀ {n} → (n ^_) Is +-semigroup -Semigroup⟶ *-semigroup
^-semigroup-morphism = record
  { ⟦⟧-cong = cong (_ ^_)
  ; ∙-homo  = ^-distribˡ-+-* _
  }

^-monoid-morphism : ∀ {n} → (n ^_) Is +-0-monoid -Monoid⟶ *-1-monoid
^-monoid-morphism = record
  { sm-homo = ^-semigroup-morphism
  ; ε-homo  = refl
  }

^-*-assoc : ∀ m n o → (m ^ n) ^ o ≡ m ^ (n * o)
^-*-assoc m n zero    = cong (m ^_) (sym $ *-zeroʳ n)
^-*-assoc m n (suc o) = begin-equality
  (m ^ n) * ((m ^ n) ^ o) ≡⟨ cong ((m ^ n) *_) (^-*-assoc m n o) ⟩
  (m ^ n) * (m ^ (n * o)) ≡⟨ sym (^-distribˡ-+-* m n (n * o)) ⟩
  m ^ (n + n * o)         ≡⟨ cong (m ^_) (sym (*-suc n o)) ⟩
  m ^ (n * (suc o)) ∎

m^n≡0⇒m≡0 : ∀ m n → m ^ n ≡ 0 → m ≡ 0
m^n≡0⇒m≡0 m (suc n) eq = [ id , m^n≡0⇒m≡0 m n ]′ (m*n≡0⇒m≡0∨n≡0 m eq)

m^n≡1⇒n≡0∨m≡1 : ∀ m n → m ^ n ≡ 1 → n ≡ 0 ⊎ m ≡ 1
m^n≡1⇒n≡0∨m≡1 m zero    _  = inj₁ refl
m^n≡1⇒n≡0∨m≡1 m (suc n) eq = inj₂ (m*n≡1⇒m≡1 m (m ^ n) eq)

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

------------------------------------------------------------------------
-- Algebraic properties

⊔-assoc : Associative _⊔_
⊔-assoc zero    _       _       = refl
⊔-assoc (suc m) zero    o       = refl
⊔-assoc (suc m) (suc n) zero    = refl
⊔-assoc (suc m) (suc n) (suc o) = cong suc $ ⊔-assoc m n o

⊔-identityˡ : LeftIdentity 0 _⊔_
⊔-identityˡ _ = refl

⊔-identityʳ : RightIdentity 0 _⊔_
⊔-identityʳ zero    = refl
⊔-identityʳ (suc n) = refl

⊔-identity : Identity 0 _⊔_
⊔-identity = ⊔-identityˡ , ⊔-identityʳ

⊔-comm : Commutative _⊔_
⊔-comm zero    n       = sym $ ⊔-identityʳ n
⊔-comm (suc m) zero    = refl
⊔-comm (suc m) (suc n) = cong suc (⊔-comm m n)

⊔-sel : Selective _⊔_
⊔-sel zero    _    = inj₂ refl
⊔-sel (suc m) zero = inj₁ refl
⊔-sel (suc m) (suc n) with ⊔-sel m n
... | inj₁ m⊔n≡m = inj₁ (cong suc m⊔n≡m)
... | inj₂ m⊔n≡n = inj₂ (cong suc m⊔n≡n)

⊔-idem : Idempotent _⊔_
⊔-idem = sel⇒idem ⊔-sel

⊔-least : ∀ {m n o} → m ≤ o → n ≤ o → m ⊔ n ≤ o
⊔-least {m} {n} m≤o n≤o with ⊔-sel m n
... | inj₁ m⊔n≡m rewrite m⊔n≡m = m≤o
... | inj₂ m⊔n≡n rewrite m⊔n≡n = n≤o

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

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

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

⊔-isBand : IsBand _⊔_
⊔-isBand = record
  { isSemigroup = ⊔-isSemigroup
  ; idem        = ⊔-idem
  }

⊔-isSemilattice : IsSemilattice _⊔_
⊔-isSemilattice = record
  { isBand = ⊔-isBand
  ; comm   = ⊔-comm
  }

⊔-0-isMonoid : IsMonoid _⊔_ 0
⊔-0-isMonoid = record
  { isSemigroup = ⊔-isSemigroup
  ; identity = ⊔-identity
  }

⊔-0-isCommutativeMonoid : IsCommutativeMonoid _⊔_ 0
⊔-0-isCommutativeMonoid = record
  { isMonoid = ⊔-0-isMonoid
  ; comm = ⊔-comm
  }

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

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

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

⊔-band : Band 0ℓ 0ℓ
⊔-band = record
  { isBand = ⊔-isBand
  }

⊔-semilattice : Semilattice 0ℓ 0ℓ
⊔-semilattice = record
  { isSemilattice = ⊔-isSemilattice
  }

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

------------------------------------------------------------------------
-- Other properties of _⊔_ and _≡_

⊔-triangulate : ∀ m n o → m ⊔ n ⊔ o ≡ (m ⊔ n) ⊔ (n ⊔ o)
⊔-triangulate m n o = begin-equality
  m ⊔ n ⊔ o           ≡⟨ cong (λ v → m ⊔ v ⊔ o) (sym (⊔-idem n)) ⟩
  m ⊔ (n ⊔ n) ⊔ o     ≡⟨ ⊔-assoc m _ _ ⟩
  m ⊔ ((n ⊔ n) ⊔ o)   ≡⟨ cong (m ⊔_) (⊔-assoc n _ _) ⟩
  m ⊔ (n ⊔ (n ⊔ o))   ≡⟨ sym (⊔-assoc m _ _) ⟩
  (m ⊔ n) ⊔ (n ⊔ o)   ∎

------------------------------------------------------------------------
-- Other properties of _⊔_ and _≤_/_<_

m≤m⊔n : ∀ m n → m ≤ m ⊔ n
m≤m⊔n zero    _       = z≤n
m≤m⊔n (suc m) zero    = ≤-refl
m≤m⊔n (suc m) (suc n) = s≤s $ m≤m⊔n m n

n≤m⊔n : ∀ m n → n ≤ m ⊔ n
n≤m⊔n m n = subst (n ≤_) (⊔-comm n m) (m≤m⊔n n m)

m≤n⇒n⊔m≡n : ∀ {m n} → m ≤ n → n ⊔ m ≡ n
m≤n⇒n⊔m≡n z≤n       = ⊔-identityʳ _
m≤n⇒n⊔m≡n (s≤s m≤n) = cong suc (m≤n⇒n⊔m≡n m≤n)

m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n
m≤n⇒m⊔n≡n {m} m≤n = trans (⊔-comm m _) (m≤n⇒n⊔m≡n m≤n)

n⊔m≡m⇒n≤m : ∀ {m n} → n ⊔ m ≡ m → n ≤ m
n⊔m≡m⇒n≤m n⊔m≡m = subst (_ ≤_) n⊔m≡m (m≤m⊔n _ _)

n⊔m≡n⇒m≤n : ∀ {m n} → n ⊔ m ≡ n → m ≤ n
n⊔m≡n⇒m≤n n⊔m≡n = subst (_ ≤_) n⊔m≡n (n≤m⊔n _ _)

m≤n⇒m≤n⊔o : ∀ {m n} o → m ≤ n → m ≤ n ⊔ o
m≤n⇒m≤n⊔o o m≤n = ≤-trans m≤n (m≤m⊔n _ o)

m≤n⇒m≤o⊔n : ∀ {m n} o → m ≤ n → m ≤ o ⊔ n
m≤n⇒m≤o⊔n n m≤n = ≤-trans m≤n (n≤m⊔n n _)

m⊔n≤o⇒m≤o : ∀ m n {o} → m ⊔ n ≤ o → m ≤ o
m⊔n≤o⇒m≤o m n m⊔n≤o = ≤-trans (m≤m⊔n m n) m⊔n≤o

m⊔n≤o⇒n≤o : ∀ m n {o} → m ⊔ n ≤ o → n ≤ o
m⊔n≤o⇒n≤o m n m⊔n≤o = ≤-trans (n≤m⊔n m n) m⊔n≤o

m<n⇒m<n⊔o : ∀ {m n} o → m < n → m < n ⊔ o
m<n⇒m<n⊔o = m≤n⇒m≤n⊔o

m<n⇒m<o⊔n : ∀ {m n} o → m < n → m < o ⊔ n
m<n⇒m<o⊔n = m≤n⇒m≤o⊔n

m⊔n<o⇒m<o : ∀ m n {o} → m ⊔ n < o → m < o
m⊔n<o⇒m<o m n m⊔n<o = <-transʳ (m≤m⊔n m n) m⊔n<o

m⊔n<o⇒n<o : ∀ m n {o} → m ⊔ n < o → n < o
m⊔n<o⇒n<o m n m⊔n<o = <-transʳ (n≤m⊔n m n) m⊔n<o

⊔-mono-≤ : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
⊔-mono-≤ {m} {n} {u} {v} m≤n u≤v with ⊔-sel m u
... | inj₁ m⊔u≡m rewrite m⊔u≡m = ≤-trans m≤n (m≤m⊔n n v)
... | inj₂ m⊔u≡u rewrite m⊔u≡u = ≤-trans u≤v (n≤m⊔n n v)

⊔-monoˡ-≤ : ∀ n → (_⊔ n) Preserves _≤_ ⟶ _≤_
⊔-monoˡ-≤ n m≤o = ⊔-mono-≤ m≤o (≤-refl {n})

⊔-monoʳ-≤ : ∀ n → (n ⊔_) Preserves _≤_ ⟶ _≤_
⊔-monoʳ-≤ n m≤o = ⊔-mono-≤ (≤-refl {n}) m≤o

⊔-mono-< : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊔-mono-< = ⊔-mono-≤

⊔-pres-≤m : ∀ {m n o} → n ≤ m → o ≤ m → n ⊔ o ≤ m
⊔-pres-≤m {m} n≤m o≤m = subst (_ ≤_) (⊔-idem m) (⊔-mono-≤ n≤m o≤m)

⊔-pres-<m : ∀ {m n o} → n < m → o < m → n ⊔ o < m
⊔-pres-<m {m} n<m o<m = subst (_ <_) (⊔-idem m) (⊔-mono-< n<m o<m)

------------------------------------------------------------------------
-- Other properties of _⊔_ and _+_

+-distribˡ-⊔ : _+_ DistributesOverˡ _⊔_
+-distribˡ-⊔ zero    n o = refl
+-distribˡ-⊔ (suc m) n o = cong suc (+-distribˡ-⊔ m n o)

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

+-distrib-⊔ : _+_ DistributesOver _⊔_
+-distrib-⊔ = +-distribˡ-⊔ , +-distribʳ-⊔

m⊔n≤m+n : ∀ m n → m ⊔ n ≤ m + n
m⊔n≤m+n m n with ⊔-sel m n
... | inj₁ m⊔n≡m rewrite m⊔n≡m = m≤m+n m n
... | inj₂ m⊔n≡n rewrite m⊔n≡n = m≤n+m n m

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

------------------------------------------------------------------------
-- Algebraic properties

⊓-assoc : Associative _⊓_
⊓-assoc zero    _       _       = refl
⊓-assoc (suc m) zero    o       = refl
⊓-assoc (suc m) (suc n) zero    = refl
⊓-assoc (suc m) (suc n) (suc o) = cong suc $ ⊓-assoc m n o

⊓-zeroˡ : LeftZero 0 _⊓_
⊓-zeroˡ _ = refl

⊓-zeroʳ : RightZero 0 _⊓_
⊓-zeroʳ zero    = refl
⊓-zeroʳ (suc n) = refl

⊓-zero : Zero 0 _⊓_
⊓-zero = ⊓-zeroˡ , ⊓-zeroʳ

⊓-comm : Commutative _⊓_
⊓-comm zero    n       = sym $ ⊓-zeroʳ n
⊓-comm (suc m) zero    = refl
⊓-comm (suc m) (suc n) = cong suc (⊓-comm m n)

⊓-sel : Selective _⊓_
⊓-sel zero    _    = inj₁ refl
⊓-sel (suc m) zero = inj₂ refl
⊓-sel (suc m) (suc n) with ⊓-sel m n
... | inj₁ m⊓n≡m = inj₁ (cong suc m⊓n≡m)
... | inj₂ m⊓n≡n = inj₂ (cong suc m⊓n≡n)

⊓-idem : Idempotent _⊓_
⊓-idem = sel⇒idem ⊓-sel

⊓-greatest : ∀ {m n o} → m ≥ o → n ≥ o → m ⊓ n ≥ o
⊓-greatest {m} {n} m≥o n≥o with ⊓-sel m n
... | inj₁ m⊓n≡m rewrite m⊓n≡m = m≥o
... | inj₂ m⊓n≡n rewrite m⊓n≡n = n≥o

⊓-distribʳ-⊔ : _⊓_ DistributesOverʳ _⊔_
⊓-distribʳ-⊔ (suc m) (suc n) (suc o) = cong suc $ ⊓-distribʳ-⊔ m n o
⊓-distribʳ-⊔ (suc m) (suc n) zero    = cong suc $ refl
⊓-distribʳ-⊔ (suc m) zero    o       = refl
⊓-distribʳ-⊔ zero    n       o       = begin-equality
  (n ⊔ o) ⊓ 0    ≡⟨ ⊓-comm (n ⊔ o) 0 ⟩
  0 ⊓ (n ⊔ o)    ≡⟨⟩
  0 ⊓ n ⊔ 0 ⊓ o  ≡⟨ ⊓-comm 0 n ⟨ cong₂ _⊔_ ⟩ ⊓-comm 0 o ⟩
  n ⊓ 0 ⊔ o ⊓ 0  ∎

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

⊓-distrib-⊔ : _⊓_ DistributesOver _⊔_
⊓-distrib-⊔ = ⊓-distribˡ-⊔ , ⊓-distribʳ-⊔

⊔-abs-⊓ : _⊔_ Absorbs _⊓_
⊔-abs-⊓ zero    n       = refl
⊔-abs-⊓ (suc m) zero    = refl
⊔-abs-⊓ (suc m) (suc n) = cong suc $ ⊔-abs-⊓ m n

⊓-abs-⊔ : _⊓_ Absorbs _⊔_
⊓-abs-⊔ zero    n       = refl
⊓-abs-⊔ (suc m) (suc n) = cong suc $ ⊓-abs-⊔ m n
⊓-abs-⊔ (suc m) zero    = cong suc $ begin-equality
  m ⊓ m       ≡⟨ cong (m ⊓_) $ sym $ ⊔-identityʳ m ⟩
  m ⊓ (m ⊔ 0) ≡⟨ ⊓-abs-⊔ m zero ⟩
  m           ∎

⊓-⊔-absorptive : Absorptive _⊓_ _⊔_
⊓-⊔-absorptive = ⊓-abs-⊔ , ⊔-abs-⊓

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

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

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

⊓-isBand : IsBand _⊓_
⊓-isBand = record
  { isSemigroup = ⊓-isSemigroup
  ; idem        = ⊓-idem
  }

⊓-isSemilattice : IsSemilattice _⊓_
⊓-isSemilattice = record
  { isBand = ⊓-isBand
  ; comm   = ⊓-comm
  }

⊔-⊓-isSemiringWithoutOne : IsSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isSemiringWithoutOne = record
  { +-isCommutativeMonoid = ⊔-0-isCommutativeMonoid
  ; *-isSemigroup         = ⊓-isSemigroup
  ; distrib               = ⊓-distrib-⊔
  ; zero                  = ⊓-zero
  }

⊔-⊓-isCommutativeSemiringWithoutOne
  : IsCommutativeSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isCommutativeSemiringWithoutOne = record
  { isSemiringWithoutOne = ⊔-⊓-isSemiringWithoutOne
  ; *-comm               = ⊓-comm
  }

⊓-⊔-isLattice : IsLattice _⊓_ _⊔_
⊓-⊔-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ⊓-comm
  ; ∨-assoc       = ⊓-assoc
  ; ∨-cong        = cong₂ _⊓_
  ; ∧-comm        = ⊔-comm
  ; ∧-assoc       = ⊔-assoc
  ; ∧-cong        = cong₂ _⊔_
  ; absorptive    = ⊓-⊔-absorptive
  }

⊓-⊔-isDistributiveLattice : IsDistributiveLattice _⊓_ _⊔_
⊓-⊔-isDistributiveLattice = record
  { isLattice    = ⊓-⊔-isLattice
  ; ∨-distribʳ-∧ = ⊓-distribʳ-⊔
  }

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

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

⊓-semigroup : Semigroup 0ℓ 0ℓ
⊓-semigroup = record
  { isSemigroup = ⊔-isSemigroup
  }

⊓-band : Band 0ℓ 0ℓ
⊓-band = record
  { isBand = ⊓-isBand
  }

⊓-semilattice : Semilattice 0ℓ 0ℓ
⊓-semilattice = record
  { isSemilattice = ⊓-isSemilattice
  }

⊔-⊓-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne 0ℓ 0ℓ
⊔-⊓-commutativeSemiringWithoutOne = record
  { isCommutativeSemiringWithoutOne =
      ⊔-⊓-isCommutativeSemiringWithoutOne
  }

⊓-⊔-lattice : Lattice 0ℓ 0ℓ
⊓-⊔-lattice = record
  { isLattice = ⊓-⊔-isLattice
  }

⊓-⊔-distributiveLattice : DistributiveLattice 0ℓ 0ℓ
⊓-⊔-distributiveLattice = record
  { isDistributiveLattice = ⊓-⊔-isDistributiveLattice
  }

------------------------------------------------------------------------
-- Other properties of _⊓_ and _≡_

⊓-triangulate : ∀ m n o → m ⊓ n ⊓ o ≡ (m ⊓ n) ⊓ (n ⊓ o)
⊓-triangulate m n o = begin-equality
  m ⊓ n ⊓ o           ≡⟨ sym (cong (λ v → m ⊓ v ⊓ o) (⊓-idem n)) ⟩
  m ⊓ (n ⊓ n) ⊓ o     ≡⟨ ⊓-assoc m _ _ ⟩
  m ⊓ ((n ⊓ n) ⊓ o)   ≡⟨ cong (m ⊓_) (⊓-assoc n _ _) ⟩
  m ⊓ (n ⊓ (n ⊓ o))   ≡⟨ sym (⊓-assoc m _ _) ⟩
  (m ⊓ n) ⊓ (n ⊓ o)   ∎

------------------------------------------------------------------------
-- Other properties of _⊓_ and _≤_/_<_

m⊓n≤m : ∀ m n → m ⊓ n ≤ m
m⊓n≤m zero    _       = z≤n
m⊓n≤m (suc m) zero    = z≤n
m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n

m⊓n≤n : ∀ m n → m ⊓ n ≤ n
m⊓n≤n m n = subst (_≤ n) (⊓-comm n m) (m⊓n≤m n m)

m≤n⇒m⊓n≡m : ∀ {m n} → m ≤ n → m ⊓ n ≡ m
m≤n⇒m⊓n≡m z≤n       = refl
m≤n⇒m⊓n≡m (s≤s m≤n) = cong suc (m≤n⇒m⊓n≡m m≤n)

m≤n⇒n⊓m≡m : ∀ {m n} → m ≤ n → n ⊓ m ≡ m
m≤n⇒n⊓m≡m {m} m≤n = trans (⊓-comm _ m) (m≤n⇒m⊓n≡m m≤n)

m⊓n≡m⇒m≤n : ∀ {m n} → m ⊓ n ≡ m → m ≤ n
m⊓n≡m⇒m≤n m⊓n≡m = subst (_≤ _) m⊓n≡m (m⊓n≤n _ _)

m⊓n≡n⇒n≤m : ∀ {m n} → m ⊓ n ≡ n → n ≤ m
m⊓n≡n⇒n≤m m⊓n≡n = subst (_≤ _) m⊓n≡n (m⊓n≤m _ _)

m≤n⇒m⊓o≤n : ∀ {m n} o → m ≤ n → m ⊓ o ≤ n
m≤n⇒m⊓o≤n o m≤n = ≤-trans (m⊓n≤m _ o) m≤n

m≤n⇒o⊓m≤n : ∀ {m n} o → m ≤ n → o ⊓ m ≤ n
m≤n⇒o⊓m≤n n m≤n = ≤-trans (m⊓n≤n n _) m≤n

m≤n⊓o⇒m≤n : ∀ {m} n o → m ≤ n ⊓ o → m ≤ n
m≤n⊓o⇒m≤n n o m≤n⊓o = ≤-trans m≤n⊓o (m⊓n≤m n o)

m≤n⊓o⇒m≤o : ∀ {m} n o → m ≤ n ⊓ o → m ≤ o
m≤n⊓o⇒m≤o n o m≤n⊓o = ≤-trans m≤n⊓o (m⊓n≤n n o)

m<n⇒m⊓o<n : ∀ {m n} o → m < n → m ⊓ o < n
m<n⇒m⊓o<n o m<n = <-transʳ (m⊓n≤m _ o) m<n

m<n⇒o⊓m<n : ∀ {m n} o → m < n → o ⊓ m < n
m<n⇒o⊓m<n o m<n = <-transʳ (m⊓n≤n o _) m<n

m<n⊓o⇒m<n : ∀ {m} n o → m < n ⊓ o → m < n
m<n⊓o⇒m<n = m≤n⊓o⇒m≤n

m<n⊓o⇒m<o : ∀ {m} n o → m < n ⊓ o → m < o
m<n⊓o⇒m<o = m≤n⊓o⇒m≤o

⊓-mono-≤ : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
⊓-mono-≤ {m} {n} {u} {v} m≤n u≤v with ⊓-sel n v
... | inj₁ n⊓v≡n rewrite n⊓v≡n = ≤-trans (m⊓n≤m m u) m≤n
... | inj₂ n⊓v≡v rewrite n⊓v≡v = ≤-trans (m⊓n≤n m u) u≤v

⊓-monoˡ-≤ : ∀ n → (_⊓ n) Preserves _≤_ ⟶ _≤_
⊓-monoˡ-≤ n m≤o = ⊓-mono-≤ m≤o (≤-refl {n})

⊓-monoʳ-≤ : ∀ n → (n ⊓_) Preserves _≤_ ⟶ _≤_
⊓-monoʳ-≤ n m≤o = ⊓-mono-≤ (≤-refl {n}) m≤o

⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊓-mono-< = ⊓-mono-≤

m⊓n≤m⊔n : ∀ m n → m ⊓ n ≤ m ⊔ n
m⊓n≤m⊔n zero    n       = z≤n
m⊓n≤m⊔n (suc m) zero    = z≤n
m⊓n≤m⊔n (suc m) (suc n) = s≤s (m⊓n≤m⊔n m n)

⊓-pres-m≤ : ∀ {m n o} → m ≤ n → m ≤ o → m ≤ n ⊓ o
⊓-pres-m≤ {m} m≤n m≤o = subst (_≤ _) (⊓-idem m) (⊓-mono-≤ m≤n m≤o)

⊓-pres-m< : ∀ {m n o} → m < n → m < o → m < n ⊓ o
⊓-pres-m< {m} m<n m<o = subst (_< _) (⊓-idem m) (⊓-mono-< m<n m<o)

------------------------------------------------------------------------
-- Other properties of _⊓_ and _+_

+-distribˡ-⊓ : _+_ DistributesOverˡ _⊓_
+-distribˡ-⊓ zero    n o = refl
+-distribˡ-⊓ (suc m) n o = cong suc (+-distribˡ-⊓ m n o)

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

+-distrib-⊓ : _+_ DistributesOver _⊓_
+-distrib-⊓ = +-distribˡ-⊓ , +-distribʳ-⊓

m⊓n≤m+n : ∀ m n → m ⊓ n ≤ m + n
m⊓n≤m+n m n with ⊓-sel m n
... | inj₁ m⊓n≡m rewrite m⊓n≡m = m≤m+n m n
... | inj₂ m⊓n≡n rewrite m⊓n≡n = m≤n+m n m

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

0∸n≡0 : LeftZero zero _∸_
0∸n≡0 zero    = refl
0∸n≡0 (suc _) = refl

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

------------------------------------------------------------------------
-- Properties of _∸_ and _≤_/_<_

m∸n≤m : ∀ m n → m ∸ n ≤ m
m∸n≤m n       zero    = ≤-refl
m∸n≤m zero    (suc n) = ≤-refl
m∸n≤m (suc m) (suc n) = ≤-trans (m∸n≤m m n) (n≤1+n m)

m≮m∸n : ∀ m n → m ≮ m ∸ n
m≮m∸n m       zero    = n≮n m
m≮m∸n (suc m) (suc n) = m≮m∸n m n ∘ ≤-trans (n≤1+n (suc m))

1+m≢m∸n : ∀ {m} n → suc m ≢ m ∸ n
1+m≢m∸n {m} n eq = m≮m∸n m n (≤-reflexive eq)

∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
∸-mono z≤n         (s≤s n₁≥n₂)    = z≤n
∸-mono (s≤s m₁≤m₂) (s≤s n₁≥n₂)    = ∸-mono m₁≤m₂ n₁≥n₂
∸-mono m₁≤m₂       (z≤n {n = n₁}) = ≤-trans (m∸n≤m _ n₁) m₁≤m₂

∸-monoˡ-≤ : ∀ {m n} o → m ≤ n → m ∸ o ≤ n ∸ o
∸-monoˡ-≤ o m≤n = ∸-mono {u = o} m≤n ≤-refl

∸-monoʳ-≤ : ∀ {m n} o → m ≤ n → o ∸ m ≥ o ∸ n
∸-monoʳ-≤ _ m≤n = ∸-mono ≤-refl m≤n

∸-monoʳ-< : ∀ {m n o} → o < n → n ≤ m → m ∸ n < m ∸ o
∸-monoʳ-< {n = suc n} {zero}  (s≤s o<n) (s≤s n<m) = s≤s (m∸n≤m _ n)
∸-monoʳ-< {n = suc n} {suc o} (s≤s o<n) (s≤s n<m) = ∸-monoʳ-< o<n n<m

∸-cancelʳ-≤ : ∀ {m n o} → m ≤ o → o ∸ n ≤ o ∸ m → m ≤ n
∸-cancelʳ-≤ {_}     {_}     z≤n       _       = z≤n
∸-cancelʳ-≤ {suc m} {zero}  (s≤s _)   o<o∸m   = contradiction o<o∸m (m≮m∸n _ m)
∸-cancelʳ-≤ {suc m} {suc n} (s≤s m≤o) o∸n<o∸m = s≤s (∸-cancelʳ-≤ m≤o o∸n<o∸m)

∸-cancelʳ-< : ∀ {m n o} → o ∸ m < o ∸ n → n < m
∸-cancelʳ-< {zero}  {n}     {o}     o<o∸n   = contradiction o<o∸n (m≮m∸n o n)
∸-cancelʳ-< {suc m} {zero}  {_}     o∸n<o∸m = 0<1+n
∸-cancelʳ-< {suc m} {suc n} {suc o} o∸n<o∸m = s≤s (∸-cancelʳ-< o∸n<o∸m)

∸-cancelˡ-≡ :  ∀ {m n o} → n ≤ m → o ≤ m → m ∸ n ≡ m ∸ o → n ≡ o
∸-cancelˡ-≡ {_}         z≤n       z≤n       _  = refl
∸-cancelˡ-≡ {o = suc o} z≤n       (s≤s _)   eq = contradiction eq (1+m≢m∸n o)
∸-cancelˡ-≡ {n = suc n} (s≤s _)   z≤n       eq = contradiction (sym eq) (1+m≢m∸n n)
∸-cancelˡ-≡ {_}         (s≤s n≤m) (s≤s o≤m) eq = cong suc (∸-cancelˡ-≡ n≤m o≤m eq)

∸-cancelʳ-≡ :  ∀ {m n o} → o ≤ m → o ≤ n → m ∸ o ≡ n ∸ o → m ≡ n
∸-cancelʳ-≡  z≤n       z≤n      eq = eq
∸-cancelʳ-≡ (s≤s o≤m) (s≤s o≤n) eq = cong suc (∸-cancelʳ-≡ o≤m o≤n eq)

m∸n≡0⇒m≤n : ∀ {m n} → m ∸ n ≡ 0 → m ≤ n
m∸n≡0⇒m≤n {zero}  {_}    _   = z≤n
m∸n≡0⇒m≤n {suc m} {suc n} eq = s≤s (m∸n≡0⇒m≤n eq)

m≤n⇒m∸n≡0 : ∀ {m n} → m ≤ n → m ∸ n ≡ 0
m≤n⇒m∸n≡0 {n = n} z≤n      = 0∸n≡0 n
m≤n⇒m∸n≡0 {_}    (s≤s m≤n) = m≤n⇒m∸n≡0 m≤n

m<n⇒0<n∸m : ∀ {m n} → m < n → 0 < n ∸ m
m<n⇒0<n∸m {zero}  {suc n} _         = 0<1+n
m<n⇒0<n∸m {suc m} {suc n} (s≤s m<n) = m<n⇒0<n∸m m<n

m∸n≢0⇒n<m : ∀ {m n} → m ∸ n ≢ 0 → n < m
m∸n≢0⇒n<m {m} {n} m∸n≢0 with n <? m
... | yes n<m = n<m
... | no  n≮m = contradiction (m≤n⇒m∸n≡0 (≮⇒≥ n≮m)) m∸n≢0

m>n⇒m∸n≢0 : ∀ {m n} → m > n → m ∸ n ≢ 0
m>n⇒m∸n≢0 {n = suc n} (s≤s m>n) = m>n⇒m∸n≢0 m>n

---------------------------------------------------------------
-- Properties of _∸_ and _+_

+-∸-comm : ∀ {m} n {o} → o ≤ m → (m + n) ∸ o ≡ (m ∸ o) + n
+-∸-comm {zero}  _ {zero}  _         = refl
+-∸-comm {suc m} _ {zero}  _         = refl
+-∸-comm {suc m} n {suc o} (s≤s o≤m) = +-∸-comm n o≤m

∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
∸-+-assoc zero zero o = refl
∸-+-assoc zero (suc n) o = 0∸n≡0 o
∸-+-assoc (suc m) zero o = refl
∸-+-assoc (suc m) (suc n) o = ∸-+-assoc m n o

+-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
+-∸-assoc m (z≤n {n = n})             = begin-equality m + n ∎
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin-equality
  (m + suc n) ∸ suc o  ≡⟨ cong (_∸ suc o) (+-suc m n) ⟩
  suc (m + n) ∸ suc o  ≡⟨⟩
  (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
  m + (n ∸ o)          ∎

m≤n+m∸n : ∀ m n → m ≤ n + (m ∸ n)
m≤n+m∸n zero    n       = z≤n
m≤n+m∸n (suc m) zero    = ≤-refl
m≤n+m∸n (suc m) (suc n) = s≤s (m≤n+m∸n m n)

m+n∸n≡m : ∀ m n → m + n ∸ n ≡ m
m+n∸n≡m m n = begin-equality
  (m + n) ∸ n  ≡⟨ +-∸-assoc m (≤-refl {x = n}) ⟩
  m + (n ∸ n)  ≡⟨ cong (m +_) (n∸n≡0 n) ⟩
  m + 0        ≡⟨ +-identityʳ m ⟩
  m            ∎

m+n∸m≡n : ∀ m n → m + n ∸ m ≡ n
m+n∸m≡n m n = trans (cong (_∸ m) (+-comm m n)) (m+n∸n≡m n m)

m+[n∸m]≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
m+[n∸m]≡n {m} {n} m≤n = begin-equality
  m + (n ∸ m)  ≡⟨ sym $ +-∸-assoc m m≤n ⟩
  (m + n) ∸ m  ≡⟨ cong (_∸ m) (+-comm m n) ⟩
  (n + m) ∸ m  ≡⟨ m+n∸n≡m n m ⟩
  n            ∎

m∸n+n≡m : ∀ {m n} → n ≤ m → (m ∸ n) + n ≡ m
m∸n+n≡m {m} {n} n≤m = begin-equality
  (m ∸ n) + n ≡⟨ sym (+-∸-comm n n≤m) ⟩
  (m + n) ∸ n ≡⟨ m+n∸n≡m m n ⟩
  m           ∎

m∸[m∸n]≡n : ∀ {m n} → n ≤ m → m ∸ (m ∸ n) ≡ n
m∸[m∸n]≡n {m}     {_}     z≤n       = n∸n≡0 m
m∸[m∸n]≡n {suc m} {suc n} (s≤s n≤m) = begin-equality
  suc m ∸ (m ∸ n)   ≡⟨ +-∸-assoc 1 (m∸n≤m m n) ⟩
  suc (m ∸ (m ∸ n)) ≡⟨ cong suc (m∸[m∸n]≡n n≤m) ⟩
  suc n             ∎

[m+n]∸[m+o]≡n∸o : ∀ m n o → (m + n) ∸ (m + o) ≡ n ∸ o
[m+n]∸[m+o]≡n∸o zero    n o = refl
[m+n]∸[m+o]≡n∸o (suc m) n o = [m+n]∸[m+o]≡n∸o m n o

------------------------------------------------------------------------
-- Properties of _∸_ and _*_

*-distribʳ-∸ : _*_ DistributesOverʳ _∸_
*-distribʳ-∸ m       zero    zero    = refl
*-distribʳ-∸ zero    zero    (suc o) = sym (0∸n≡0 (o * zero))
*-distribʳ-∸ (suc m) zero    (suc o) = refl
*-distribʳ-∸ m       (suc n) zero    = refl
*-distribʳ-∸ m       (suc n) (suc o) = begin-equality
  (n ∸ o) * m             ≡⟨ *-distribʳ-∸ m n o ⟩
  n * m ∸ o * m           ≡⟨ sym $ [m+n]∸[m+o]≡n∸o m _ _ ⟩
  m + n * m ∸ (m + o * m) ∎

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

*-distrib-∸ : _*_ DistributesOver _∸_
*-distrib-∸ = *-distribˡ-∸ , *-distribʳ-∸

even≢odd :  ∀ m n → 2 * m ≢ suc (2 * n)
even≢odd (suc m) zero    eq = contradiction (suc-injective eq) (m+1+n≢0 m)
even≢odd (suc m) (suc n) eq = even≢odd m n (suc-injective (begin-equality
  suc (2 * m)         ≡⟨ sym (+-suc m _) ⟩
  m + suc (m + 0)     ≡⟨ suc-injective eq ⟩
  suc n + suc (n + 0) ≡⟨ cong suc (+-suc n _) ⟩
  suc (suc (2 * n))   ∎))

------------------------------------------------------------------------
-- Properties of _∸_ and _⊓_ and _⊔_

m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
m⊓n+n∸m≡n zero    n       = refl
m⊓n+n∸m≡n (suc m) zero    = refl
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n

[m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
[m∸n]⊓[n∸m]≡0 zero zero       = refl
[m∸n]⊓[n∸m]≡0 zero (suc n)    = refl
[m∸n]⊓[n∸m]≡0 (suc m) zero    = refl
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n

∸-distribˡ-⊓-⊔ : ∀ m n o → m ∸ (n ⊓ o) ≡ (m ∸ n) ⊔ (m ∸ o)
∸-distribˡ-⊓-⊔ m       zero    zero    = sym (⊔-idem m)
∸-distribˡ-⊓-⊔ zero    zero    (suc o) = refl
∸-distribˡ-⊓-⊔ zero    (suc n) zero    = refl
∸-distribˡ-⊓-⊔ zero    (suc n) (suc o) = refl
∸-distribˡ-⊓-⊔ (suc m) (suc n) zero    = sym (m≤n⇒m⊔n≡n (≤-step (m∸n≤m m n)))
∸-distribˡ-⊓-⊔ (suc m) zero    (suc o) = sym (m≤n⇒n⊔m≡n (≤-step (m∸n≤m m o)))
∸-distribˡ-⊓-⊔ (suc m) (suc n) (suc o) = ∸-distribˡ-⊓-⊔ m n o

∸-distribʳ-⊓ : _∸_ DistributesOverʳ _⊓_
∸-distribʳ-⊓ zero    n       o       = refl
∸-distribʳ-⊓ (suc m) zero    o       = refl
∸-distribʳ-⊓ (suc m) (suc n) zero    = sym (⊓-zeroʳ (n ∸ m))
∸-distribʳ-⊓ (suc m) (suc n) (suc o) = ∸-distribʳ-⊓ m n o

∸-distribˡ-⊔-⊓ : ∀ m n o → m ∸ (n ⊔ o) ≡ (m ∸ n) ⊓ (m ∸ o)
∸-distribˡ-⊔-⊓ m       zero    zero    = sym (⊓-idem m)
∸-distribˡ-⊔-⊓ zero    zero    o       = 0∸n≡0 o
∸-distribˡ-⊔-⊓ zero    (suc n) o       = 0∸n≡0 (suc n ⊔ o)
∸-distribˡ-⊔-⊓ (suc m) (suc n) zero    = sym (m≤n⇒m⊓n≡m (≤-step (m∸n≤m m n)))
∸-distribˡ-⊔-⊓ (suc m) zero    (suc o) = sym (m≤n⇒n⊓m≡m (≤-step (m∸n≤m m o)))
∸-distribˡ-⊔-⊓ (suc m) (suc n) (suc o) = ∸-distribˡ-⊔-⊓ m n o

∸-distribʳ-⊔ : _∸_ DistributesOverʳ _⊔_
∸-distribʳ-⊔ zero    n       o       = refl
∸-distribʳ-⊔ (suc m) zero    o       = refl
∸-distribʳ-⊔ (suc m) (suc n) zero    = sym (⊔-identityʳ (n ∸ m))
∸-distribʳ-⊔ (suc m) (suc n) (suc o) = ∸-distribʳ-⊔ m n o

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

m≡n⇒∣m-n∣≡0 : ∀ {m n} → m ≡ n → ∣ m - n ∣ ≡ 0
m≡n⇒∣m-n∣≡0 {zero}  refl = refl
m≡n⇒∣m-n∣≡0 {suc m} refl = m≡n⇒∣m-n∣≡0 {m} refl

∣m-n∣≡0⇒m≡n : ∀ {m n} → ∣ m - n ∣ ≡ 0 → m ≡ n
∣m-n∣≡0⇒m≡n {zero}  {zero}  eq = refl
∣m-n∣≡0⇒m≡n {suc m} {suc n} eq = cong suc (∣m-n∣≡0⇒m≡n eq)

m≤n⇒∣n-m∣≡n∸m : ∀ {m n} → m ≤ n → ∣ n - m ∣ ≡ n ∸ m
m≤n⇒∣n-m∣≡n∸m {_} {zero}  z≤n       = refl
m≤n⇒∣n-m∣≡n∸m {_} {suc m} z≤n       = refl
m≤n⇒∣n-m∣≡n∸m {_} {_}     (s≤s m≤n) = m≤n⇒∣n-m∣≡n∸m m≤n

∣m-n∣≡m∸n⇒n≤m : ∀ {m n} → ∣ m - n ∣ ≡ m ∸ n → n ≤ m
∣m-n∣≡m∸n⇒n≤m {zero}  {zero}  eq = z≤n
∣m-n∣≡m∸n⇒n≤m {suc m} {zero}  eq = z≤n
∣m-n∣≡m∸n⇒n≤m {suc m} {suc n} eq = s≤s (∣m-n∣≡m∸n⇒n≤m eq)

∣n-n∣≡0 : ∀ n → ∣ n - n ∣ ≡ 0
∣n-n∣≡0 n = m≡n⇒∣m-n∣≡0 {n} refl

∣m-m+n∣≡n : ∀ m n → ∣ m - m + n ∣ ≡ n
∣m-m+n∣≡n zero    n = refl
∣m-m+n∣≡n (suc m) n = ∣m-m+n∣≡n m n

∣m+n-m+o∣≡∣n-o| : ∀ m n o → ∣ m + n - m + o ∣ ≡ ∣ n - o ∣
∣m+n-m+o∣≡∣n-o| zero    n o = refl
∣m+n-m+o∣≡∣n-o| (suc m) n o = ∣m+n-m+o∣≡∣n-o| m n o

m∸n≤∣m-n∣ : ∀ m n → m ∸ n ≤ ∣ m - n ∣
m∸n≤∣m-n∣ m n with ≤-total m n
... | inj₁ m≤n = subst (_≤ ∣ m - n ∣) (sym (m≤n⇒m∸n≡0 m≤n)) z≤n
... | inj₂ n≤m = subst (m ∸ n ≤_) (sym (m≤n⇒∣n-m∣≡n∸m n≤m)) ≤-refl

∣m-n∣≤m⊔n : ∀ m n → ∣ m - n ∣ ≤ m ⊔ n
∣m-n∣≤m⊔n zero    m       = ≤-refl
∣m-n∣≤m⊔n (suc m) zero    = ≤-refl
∣m-n∣≤m⊔n (suc m) (suc n) = ≤-step (∣m-n∣≤m⊔n m n)

∣-∣-identityˡ : LeftIdentity 0 ∣_-_∣
∣-∣-identityˡ x = refl

∣-∣-identityʳ : RightIdentity 0 ∣_-_∣
∣-∣-identityʳ zero    = refl
∣-∣-identityʳ (suc x) = refl

∣-∣-identity : Identity 0 ∣_-_∣
∣-∣-identity = ∣-∣-identityˡ , ∣-∣-identityʳ

∣-∣-comm : Commutative ∣_-_∣
∣-∣-comm zero    zero    = refl
∣-∣-comm zero    (suc n) = refl
∣-∣-comm (suc m) zero    = refl
∣-∣-comm (suc m) (suc n) = ∣-∣-comm m n

∣m-n∣≡[m∸n]∨[n∸m] : ∀ m n → (∣ m - n ∣ ≡ m ∸ n) ⊎ (∣ m - n ∣ ≡ n ∸ m)
∣m-n∣≡[m∸n]∨[n∸m] m n with ≤-total m n
... | inj₂ n≤m = inj₁ $ m≤n⇒∣n-m∣≡n∸m n≤m
... | inj₁ m≤n = inj₂ $ begin-equality
  ∣ m - n ∣ ≡⟨ ∣-∣-comm m n ⟩
  ∣ n - m ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m m≤n ⟩
  n ∸ m     ∎

private

  *-distribˡ-∣-∣-aux : ∀ a m n → m ≤ n → a * ∣ n - m ∣ ≡ ∣ a * n - a * m ∣
  *-distribˡ-∣-∣-aux a m n m≤n = begin-equality
    a * ∣ n - m ∣     ≡⟨ cong (a *_) (m≤n⇒∣n-m∣≡n∸m m≤n) ⟩
    a * (n ∸ m)       ≡⟨ *-distribˡ-∸ a n m ⟩
    a * n ∸ a * m     ≡⟨ sym $′ m≤n⇒∣n-m∣≡n∸m (*-monoʳ-≤ a m≤n) ⟩
    ∣ a * n - a * m ∣ ∎

*-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣
*-distribˡ-∣-∣ a m n with ≤-total m n
... | inj₁ m≤n = begin-equality
  a * ∣ m - n ∣     ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩
  a * ∣ n - m ∣     ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩
  ∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩
  ∣ a * m - a * n ∣ ∎
... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m

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

*-distrib-∣-∣ : _*_ DistributesOver ∣_-_∣
*-distrib-∣-∣ = *-distribˡ-∣-∣ , *-distribʳ-∣-∣

m≤n+∣n-m∣ : ∀ m n → m ≤ n + ∣ n - m ∣
m≤n+∣n-m∣ zero    n       = z≤n
m≤n+∣n-m∣ (suc m) zero    = ≤-refl
m≤n+∣n-m∣ (suc m) (suc n) = s≤s (m≤n+∣n-m∣ m n)

m≤n+∣m-n∣ : ∀ m n → m ≤ n + ∣ m - n ∣
m≤n+∣m-n∣ m n = subst (m ≤_) (cong (n +_) (∣-∣-comm n m)) (m≤n+∣n-m∣ m n)

m≤∣m-n∣+n : ∀ m n → m ≤ ∣ m - n ∣ + n
m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)

------------------------------------------------------------------------
-- Properties of ⌊_/2⌋ and ⌈_/2⌉
------------------------------------------------------------------------

⌊n/2⌋-mono : ⌊_/2⌋ Preserves _≤_ ⟶ _≤_
⌊n/2⌋-mono z≤n             = z≤n
⌊n/2⌋-mono (s≤s z≤n)       = z≤n
⌊n/2⌋-mono (s≤s (s≤s m≤n)) = s≤s (⌊n/2⌋-mono m≤n)

⌈n/2⌉-mono : ⌈_/2⌉ Preserves _≤_ ⟶ _≤_
⌈n/2⌉-mono m≤n = ⌊n/2⌋-mono (s≤s m≤n)

⌊n/2⌋≤⌈n/2⌉ : ∀ n → ⌊ n /2⌋ ≤ ⌈ n /2⌉
⌊n/2⌋≤⌈n/2⌉ zero          = z≤n
⌊n/2⌋≤⌈n/2⌉ (suc zero)    = z≤n
⌊n/2⌋≤⌈n/2⌉ (suc (suc n)) = s≤s (⌊n/2⌋≤⌈n/2⌉ n)

⌊n/2⌋+⌈n/2⌉≡n : ∀ n → ⌊ n /2⌋ + ⌈ n /2⌉ ≡ n
⌊n/2⌋+⌈n/2⌉≡n zero    = refl
⌊n/2⌋+⌈n/2⌉≡n (suc n) = begin-equality
  ⌊ suc n /2⌋ + suc ⌊ n /2⌋   ≡⟨ +-comm ⌊ suc n /2⌋ (suc ⌊ n /2⌋) ⟩
  suc ⌊ n /2⌋ + ⌊ suc n /2⌋   ≡⟨⟩
  suc (⌊ n /2⌋ + ⌊ suc n /2⌋) ≡⟨ cong suc (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
  suc n                       ∎

⌊n/2⌋≤n : ∀ n → ⌊ n /2⌋ ≤ n
⌊n/2⌋≤n zero          = z≤n
⌊n/2⌋≤n (suc zero)    = z≤n
⌊n/2⌋≤n (suc (suc n)) = s≤s (≤-step (⌊n/2⌋≤n n))

⌊n/2⌋<n : ∀ n → ⌊ suc n /2⌋ < suc n
⌊n/2⌋<n zero    = s≤s z≤n
⌊n/2⌋<n (suc n) = s≤s (s≤s (⌊n/2⌋≤n n))

⌈n/2⌉≤n : ∀ n → ⌈ n /2⌉ ≤ n
⌈n/2⌉≤n zero = z≤n
⌈n/2⌉≤n (suc n) = s≤s (⌊n/2⌋≤n n)

⌈n/2⌉<n : ∀ n → ⌈ suc (suc n) /2⌉ < suc (suc n)
⌈n/2⌉<n n = s≤s (⌊n/2⌋<n n)

------------------------------------------------------------------------
-- Properties of _≤′_ and _<′_
------------------------------------------------------------------------

≤′-trans : Transitive _≤′_
≤′-trans m≤n ≤′-refl       = m≤n
≤′-trans m≤n (≤′-step n≤o) = ≤′-step (≤′-trans m≤n n≤o)

z≤′n : ∀ {n} → zero ≤′ n
z≤′n {zero}  = ≤′-refl
z≤′n {suc n} = ≤′-step z≤′n

s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
s≤′s ≤′-refl        = ≤′-refl
s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)

≤′⇒≤ : _≤′_ ⇒ _≤_
≤′⇒≤ ≤′-refl        = ≤-refl
≤′⇒≤ (≤′-step m≤′n) = ≤-step (≤′⇒≤ m≤′n)

≤⇒≤′ : _≤_ ⇒ _≤′_
≤⇒≤′ z≤n       = z≤′n
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)

≤′-step-injective : ∀ {m n} {p q : m ≤′ n} → ≤′-step p ≡ ≤′-step q → p ≡ q
≤′-step-injective refl = refl

infix 4 _≤′?_ _<′?_ _≥′?_ _>′?_

_≤′?_ : Decidable _≤′_
m ≤′? n = map′ ≤⇒≤′ ≤′⇒≤ (m ≤? n)

_<′?_ : Decidable _<′_
m <′? n = suc m ≤′? n

_≥′?_ : Decidable _≥′_
_≥′?_ = flip _≤′?_

_>′?_ : Decidable _>′_
_>′?_ = flip _<′?_

m≤′m+n : ∀ m n → m ≤′ m + n
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)

n≤′m+n : ∀ m n → n ≤′ m + n
n≤′m+n zero    n = ≤′-refl
n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)

⌈n/2⌉≤′n : ∀ n → ⌈ n /2⌉ ≤′ n
⌈n/2⌉≤′n zero          = ≤′-refl
⌈n/2⌉≤′n (suc zero)    = ≤′-refl
⌈n/2⌉≤′n (suc (suc n)) = s≤′s (≤′-step (⌈n/2⌉≤′n n))

⌊n/2⌋≤′n : ∀ n → ⌊ n /2⌋ ≤′ n
⌊n/2⌋≤′n zero    = ≤′-refl
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)

------------------------------------------------------------------------
-- Properties of _≤″_ and _<″_
------------------------------------------------------------------------

m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)

m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)

<ᵇ⇒<″ : ∀ {m n} → T (m <ᵇ n) → m <″ n
<ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))

<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
<″⇒<ᵇ {m} (less-than-or-equal refl) = <⇒<ᵇ (m≤m+n (suc m) _)

-- equivalence to _≤_

≤″⇒≤ : _≤″_ ⇒ _≤_
≤″⇒≤ {zero}  (less-than-or-equal refl) = z≤n
≤″⇒≤ {suc m} (less-than-or-equal refl) =
  s≤s (≤″⇒≤ (less-than-or-equal refl))

≤⇒≤″ : _≤_ ⇒ _≤″_
≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n

-- NB: we use the builtin function `_<ᵇ_ : (m n : ℕ) → Bool` here so
-- that the function quickly decides whether to return `yes` or `no`.
-- It still takes a linear amount of time to generate the proof if it
-- is inspected. We expect the main benefit to be visible for compiled
-- code: the backend erases proofs.

infix 4 _<″?_ _≤″?_ _≥″?_ _>″?_

_<″?_ : Decidable _<″_
m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n))

_≤″?_ : Decidable _≤″_
zero  ≤″? n = yes (less-than-or-equal refl)
suc m ≤″? n = m <″? n

_≥″?_ : Decidable _≥″_
_≥″?_ = flip _≤″?_

_>″?_ : Decidable _>″_
_>″?_ = flip _<″?_

≤″-irrelevant : Irrelevant _≤″_
≤″-irrelevant {m} (less-than-or-equal eq₁)
                  (less-than-or-equal eq₂)
  with +-cancelˡ-≡ m (trans eq₁ (sym eq₂))
... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)

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

>″-irrelevant : Irrelevant _>″_
>″-irrelevant = ≤″-irrelevant

≥″-irrelevant : Irrelevant _≥″_
≥″-irrelevant = ≤″-irrelevant

------------------------------------------------------------------------
-- Properties of _≤‴_
------------------------------------------------------------------------

≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n
≤‴⇒≤″ {m = m} ≤‴-refl     = less-than-or-equal {k = 0} (+-identityʳ m)
≤‴⇒≤″ {m = m} (≤‴-step x) = less-than-or-equal (trans (+-suc m _) (_≤″_.proof ind)) where
  ind = ≤‴⇒≤″ x

m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n
m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m})
m≤‴m+k {m} {k = suc k} proof
  = ≤‴-step (m≤‴m+k {k = k} (trans (sym (+-suc m _)) proof))

≤″⇒≤‴ : ∀{m n} → m ≤″ n → m ≤‴ n
≤″⇒≤‴ (less-than-or-equal {k} proof) = m≤‴m+k proof

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

-- If there is an injection from a type to ℕ, then the type has
-- decidable equality.

eq? : ∀ {a} {A : Set a} → A ↣ ℕ → Decidable {A = A} _≡_
eq? inj = via-injection inj _≟_

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

-- Version 0.14

_*-mono_ = *-mono-≤
{-# WARNING_ON_USAGE _*-mono_
"Warning: _*-mono_ was deprecated in v0.14.
Please use *-mono-≤ instead."
#-}
_+-mono_ = +-mono-≤
{-# WARNING_ON_USAGE _+-mono_
"Warning: _+-mono_ was deprecated in v0.14.
Please use +-mono-≤ instead."
#-}
+-right-identity = +-identityʳ
{-# WARNING_ON_USAGE +-right-identity
"Warning: +-right-identity was deprecated in v0.14.
Please use +-identityʳ instead."
#-}
*-right-zero     = *-zeroʳ
{-# WARNING_ON_USAGE *-right-zero
"Warning: *-right-zero was deprecated in v0.14.
Please use *-zeroʳ instead."
#-}
distribʳ-*-+     = *-distribʳ-+
{-# WARNING_ON_USAGE distribʳ-*-+
"Warning: distribʳ-*-+ was deprecated in v0.14.
Please use *-distribʳ-+ instead."
#-}
*-distrib-∸ʳ     = *-distribʳ-∸
{-# WARNING_ON_USAGE *-distrib-∸ʳ
"Warning: *-distrib-∸ʳ was deprecated in v0.14.
Please use *-distribʳ-∸ instead."
#-}
cancel-+-left    = +-cancelˡ-≡
{-# WARNING_ON_USAGE cancel-+-left
"Warning: cancel-+-left was deprecated in v0.14.
Please use +-cancelˡ-≡ instead."
#-}
cancel-+-left-≤  = +-cancelˡ-≤
{-# WARNING_ON_USAGE cancel-+-left-≤
"Warning: cancel-+-left-≤ was deprecated in v0.14.
Please use +-cancelˡ-≤ instead."
#-}
cancel-*-right   = *-cancelʳ-≡
{-# WARNING_ON_USAGE cancel-*-right
"Warning: cancel-*-right was deprecated in v0.14.
Please use *-cancelʳ-≡ instead."
#-}
cancel-*-right-≤ = *-cancelʳ-≤
{-# WARNING_ON_USAGE cancel-*-right-≤
"Warning: cancel-*-right-≤ was deprecated in v0.14.
Please use *-cancelʳ-≤ instead."
#-}
strictTotalOrder                      = <-strictTotalOrder
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v0.14.
Please use <-strictTotalOrder instead."
#-}
isCommutativeSemiring                 = *-+-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring
"Warning: isCommutativeSemiring was deprecated in v0.14.
Please use *-+-isCommutativeSemiring instead."
#-}
commutativeSemiring                   = *-+-commutativeSemiring
{-# WARNING_ON_USAGE commutativeSemiring
"Warning: commutativeSemiring was deprecated in v0.14.
Please use *-+-commutativeSemiring instead."
#-}
isDistributiveLattice                 = ⊓-⊔-isDistributiveLattice
{-# WARNING_ON_USAGE isDistributiveLattice
"Warning: isDistributiveLattice was deprecated in v0.14.
Please use ⊓-⊔-isDistributiveLattice instead."
#-}
distributiveLattice                   = ⊓-⊔-distributiveLattice
{-# WARNING_ON_USAGE distributiveLattice
"Warning: distributiveLattice was deprecated in v0.14.
Please use ⊓-⊔-distributiveLattice instead."
#-}
⊔-⊓-0-isSemiringWithoutOne            = ⊔-⊓-isSemiringWithoutOne
{-# WARNING_ON_USAGE ⊔-⊓-0-isSemiringWithoutOne
"Warning: ⊔-⊓-0-isSemiringWithoutOne was deprecated in v0.14.
Please use ⊔-⊓-isSemiringWithoutOne instead."
#-}
⊔-⊓-0-isCommutativeSemiringWithoutOne = ⊔-⊓-isCommutativeSemiringWithoutOne
{-# WARNING_ON_USAGE ⊔-⊓-0-isCommutativeSemiringWithoutOne
"Warning: ⊔-⊓-0-isCommutativeSemiringWithoutOne was deprecated in v0.14.
Please use ⊔-⊓-isCommutativeSemiringWithoutOne instead."
#-}
⊔-⊓-0-commutativeSemiringWithoutOne   = ⊔-⊓-commutativeSemiringWithoutOne
{-# WARNING_ON_USAGE ⊔-⊓-0-commutativeSemiringWithoutOne
"Warning: ⊔-⊓-0-commutativeSemiringWithoutOne was deprecated in v0.14.
Please use ⊔-⊓-commutativeSemiringWithoutOne instead."
#-}

-- Version 0.15

¬i+1+j≤i  = m+1+n≰m
{-# WARNING_ON_USAGE ¬i+1+j≤i
"Warning: ¬i+1+j≤i was deprecated in v0.15.
Please use m+1+n≰m instead."
#-}
≤-steps   = ≤-stepsˡ
{-# WARNING_ON_USAGE ≤-steps
"Warning: ≤-steps was deprecated in v0.15.
Please use ≤-stepsˡ instead."
#-}

-- Version 0.17

i∸k∸j+j∸k≡i+j∸k : ∀ i j k → i ∸ (k ∸ j) + (j ∸ k) ≡ i + j ∸ k
i∸k∸j+j∸k≡i+j∸k zero    j k    = cong (_+ (j ∸ k)) (0∸n≡0 (k ∸ j))
i∸k∸j+j∸k≡i+j∸k (suc i) j zero = cong (λ x → suc i ∸ x + j) (0∸n≡0 j)
i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin-equality
  i ∸ k + 0  ≡⟨ +-identityʳ _ ⟩
  i ∸ k      ≡⟨ cong (_∸ k) (sym (+-identityʳ _)) ⟩
  i + 0 ∸ k  ∎
i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin-equality
  suc i ∸ (k ∸ j) + (j ∸ k) ≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k ⟩
  suc i + j ∸ k             ≡⟨ cong (_∸ k) (sym (+-suc i j)) ⟩
  i + suc j ∸ k             ∎
{-# WARNING_ON_USAGE i∸k∸j+j∸k≡i+j∸k
"Warning: i∸k∸j+j∸k≡i+j∸k was deprecated in v0.17."
#-}
im≡jm+n⇒[i∸j]m≡n : ∀ i j m n → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
im≡jm+n⇒[i∸j]m≡n i j m n eq = begin-equality
  (i ∸ j) * m            ≡⟨ *-distribʳ-∸ m i j ⟩
  (i * m) ∸ (j * m)      ≡⟨ cong (_∸ j * m) eq ⟩
  (j * m + n) ∸ (j * m)  ≡⟨ cong (_∸ j * m) (+-comm (j * m) n) ⟩
  (n + j * m) ∸ (j * m)  ≡⟨ m+n∸n≡m n (j * m) ⟩
  n                      ∎
{-# WARNING_ON_USAGE im≡jm+n⇒[i∸j]m≡n
"Warning: im≡jm+n⇒[i∸j]m≡n was deprecated in v0.17."
#-}
≤+≢⇒< = ≤∧≢⇒<
{-# WARNING_ON_USAGE ≤+≢⇒<
"Warning: ≤+≢⇒< was deprecated in v0.17.
Please use ≤∧≢⇒< instead."
#-}

-- Version 1.0

≤-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."
#-}

-- Version 1.1

i+1+j≢i = m+1+n≢m
{-# WARNING_ON_USAGE i+1+j≢i
"Warning: i+1+j≢i was deprecated in v1.1.
Please use m+1+n≢m instead."
#-}
i+j≡0⇒i≡0 = m+n≡0⇒m≡0
{-# WARNING_ON_USAGE i+j≡0⇒i≡0
"Warning: i+j≡0⇒i≡0 was deprecated in v1.1.
Please use m+n≡0⇒m≡0 instead."
#-}
i+j≡0⇒j≡0 = m+n≡0⇒n≡0
{-# WARNING_ON_USAGE i+j≡0⇒j≡0
"Warning: i+j≡0⇒j≡0 was deprecated in v1.1.
Please use m+n≡0⇒n≡0 instead."
#-}
i+1+j≰i = m+1+n≰m
{-# WARNING_ON_USAGE i+1+j≰i
"Warning: i+1+j≰i was deprecated in v1.1.
Please use m+1+n≰m instead."
#-}
i*j≡0⇒i≡0∨j≡0 = m*n≡0⇒m≡0∨n≡0
{-# WARNING_ON_USAGE i*j≡0⇒i≡0∨j≡0
"Warning: i*j≡0⇒i≡0∨j≡0 was deprecated in v1.1.
Please use m*n≡0⇒m≡0∨n≡0 instead."
#-}
i*j≡1⇒i≡1 = m*n≡1⇒m≡1
{-# WARNING_ON_USAGE i*j≡1⇒i≡1
"Warning: i*j≡1⇒i≡1 was deprecated in v1.1.
Please use m*n≡1⇒m≡1 instead."
#-}
i*j≡1⇒j≡1 = m*n≡1⇒n≡1
{-# WARNING_ON_USAGE i*j≡1⇒j≡1
"Warning: i*j≡1⇒j≡1 was deprecated in v1.1.
Please use m*n≡1⇒n≡1 instead."
#-}
i^j≡0⇒i≡0 = m^n≡0⇒m≡0
{-# WARNING_ON_USAGE i^j≡0⇒i≡0
"Warning: i^j≡0⇒i≡0 was deprecated in v1.1.
Please use m^n≡0⇒m≡0 instead."
#-}
i^j≡1⇒j≡0∨i≡1 = m^n≡1⇒n≡0∨m≡1
{-# WARNING_ON_USAGE i^j≡1⇒j≡0∨i≡1
"Warning: i^j≡1⇒j≡0∨i≡1 was deprecated in v1.1.
Please use m^n≡1⇒n≡0∨m≡1 instead."
#-}
[i+j]∸[i+k]≡j∸k = [m+n]∸[m+o]≡n∸o
{-# WARNING_ON_USAGE [i+j]∸[i+k]≡j∸k
"Warning: [i+j]∸[i+k]≡j∸k was deprecated in v1.1.
Please use [m+n]∸[m+o]≡n∸o instead."
#-}
m≢0⇒suc[pred[m]]≡m = suc[pred[n]]≡n
{-# WARNING_ON_USAGE m≢0⇒suc[pred[m]]≡m
"Warning: m≢0⇒suc[pred[m]]≡m was deprecated in v1.1.
Please use suc[pred[n]]≡n instead."
#-}
n≡m⇒∣n-m∣≡0 = m≡n⇒∣m-n∣≡0
{-# WARNING_ON_USAGE n≡m⇒∣n-m∣≡0
"Warning: n≡m⇒∣n-m∣≡0 was deprecated in v1.1.
Please use m≡n⇒∣m-n∣≡0 instead."
#-}
∣n-m∣≡0⇒n≡m = ∣m-n∣≡0⇒m≡n
{-# WARNING_ON_USAGE ∣n-m∣≡0⇒n≡m
"Warning: ∣n-m∣≡0⇒n≡m was deprecated in v1.1.
Please use ∣m-n∣≡0⇒m≡n instead."
#-}
∣n-m∣≡n∸m⇒m≤n = ∣m-n∣≡m∸n⇒n≤m
{-# WARNING_ON_USAGE ∣n-m∣≡n∸m⇒m≤n
"Warning: ∣n-m∣≡n∸m⇒m≤n was deprecated in v1.1.
Please use ∣m-n∣≡m∸n⇒n≤m instead."
#-}
∣n-n+m∣≡m = ∣m-m+n∣≡n
{-# WARNING_ON_USAGE ∣n-n+m∣≡m
"Warning: ∣n-n+m∣≡m was deprecated in v1.1.
Please use ∣m-m+n∣≡n instead."
#-}
∣n+m-n+o∣≡∣m-o| = ∣m+n-m+o∣≡∣n-o|
{-# WARNING_ON_USAGE ∣n+m-n+o∣≡∣m-o|
"Warning: ∣n+m-n+o∣≡∣m-o| was deprecated in v1.1.
Please use ∣m+n-m+o∣≡∣n-o| instead."
#-}
n∸m≤∣n-m∣ = m∸n≤∣m-n∣
{-# WARNING_ON_USAGE n∸m≤∣n-m∣
"Warning: n∸m≤∣n-m∣ was deprecated in v1.1.
Please use m∸n≤∣m-n∣ instead."
#-}
∣n-m∣≤n⊔m = ∣m-n∣≤m⊔n
{-# WARNING_ON_USAGE ∣n-m∣≤n⊔m
"Warning: ∣n-m∣≤n⊔m was deprecated in v1.1.
Please use ∣m-n∣≤m⊔n instead."
#-}
n≤m+n : ∀ m n → n ≤ m + n
n≤m+n m n = subst (n ≤_) (+-comm n m) (m≤m+n n m)
{-# WARNING_ON_USAGE n≤m+n
"Warning: n≤m+n was deprecated in v1.1.
Please use m≤n+m instead (note, you will need to switch the argument order)."
#-}
n≤m+n∸m : ∀ m n → n ≤ m + (n ∸ m)
n≤m+n∸m m       zero    = z≤n
n≤m+n∸m zero    (suc n) = ≤-refl
n≤m+n∸m (suc m) (suc n) = s≤s (n≤m+n∸m m n)
{-# WARNING_ON_USAGE n≤m+n∸m
"Warning: n≤m+n∸m was deprecated in v1.1.
Please use m≤n+m∸n instead (note, you will need to switch the argument order)."
#-}
∣n-m∣≡[n∸m]∨[m∸n] : ∀ m n → (∣ n - m ∣ ≡ n ∸ m) ⊎ (∣ n - m ∣ ≡ m ∸ n)
∣n-m∣≡[n∸m]∨[m∸n] m n with ≤-total m n
... | inj₁ m≤n = inj₁ $ m≤n⇒∣n-m∣≡n∸m m≤n
... | inj₂ n≤m = inj₂ $ begin-equality
  ∣ n - m ∣ ≡⟨ ∣-∣-comm n m ⟩
  ∣ m - n ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m n≤m ⟩
  m ∸ n     ∎
{-# WARNING_ON_USAGE ∣n-m∣≡[n∸m]∨[m∸n]
"Warning: ∣n-m∣≡[n∸m]∨[m∸n] was deprecated in v1.1.
Please use ∣m-n∣≡[m∸n]∨[n∸m] instead (note, you will need to switch the argument order)."
#-}

-- Version 1.2

+-*-suc = *-suc
{-# WARNING_ON_USAGE +-*-suc
"Warning: +-*-suc was deprecated in v1.2.
Please use *-suc instead."
#-}

n∸m≤n : ∀ m n → n ∸ m ≤ n
n∸m≤n m n = m∸n≤m n m
{-# WARNING_ON_USAGE n∸m≤n
"Warning: n∸m≤n was deprecated in v1.2.
Please use m∸n≤m instead (note, you will need to switch the argument order)."
#-}

-- Version 1.3

∀[m≤n⇒m≢o]⇒o<n : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
∀[m≤n⇒m≢o]⇒o<n = ∀[m≤n⇒m≢o]⇒n<o
{-# WARNING_ON_USAGE n∸m≤∣n-m∣
"Warning: ∀[m≤n⇒m≢o]⇒o<n was deprecated in v1.3.
Please use ∀[m≤n⇒m≢o]⇒n<o instead."
#-}
∀[m<n⇒m≢o]⇒o≤n : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
∀[m<n⇒m≢o]⇒o≤n = ∀[m<n⇒m≢o]⇒n≤o
{-# WARNING_ON_USAGE n∸m≤∣n-m∣
"Warning: ∀[m<n⇒m≢o]⇒o≤n was deprecated in v1.3.
Please use ∀[m<n⇒m≢o]⇒n≤o instead."
#-}


text:
open import Nat
open import Prelude
open import core
open import checks
open import judgemental-erase

module structural where
  -- this module contains proofs that the judgements that mention contexts
  -- defined throughout the work enjoy the standard structural properties
  -- of contexts:
  --
  -- exchange
  --
  -- Γ, (x : t1), (y : t2) ⊢ A
  -- -------------------------
  -- Γ, (y : t2), (x : t1) ⊢ A
  --
  -- contraction
  --
  -- Γ, (x : t), (x : t) ⊢ A
  -- -----------------------
  --     Γ , (x : t) ⊢ A
  --
  -- weakening
  --
  --   Γ ⊢ A      x # Γ
  -- ----------------------
  --    Γ , (x : t) ⊢ A
  --
  -- proofs of the first two are generally easier: viewed as finite
  -- functions, the contexts on the top and bottom of both exchange answer
  -- every question the same, so an appeal to function extensionality is
  -- enough to treat them the same. weakening does not have this property,
  -- and there requires some induction to demonstrate.

  -- because of our choice to use barendrecht's convention, we need a quite
  -- strong form of freshness of a variable for weakening. specifically, we
  -- need to know not just that the variable we're using to extend the
  -- context doesn't appear in the context, as in a standard presentation,
  -- it can't appear anywhere in the term at all; it must be totally
  -- fresh. it's possible to drop this requirement with alpha-renaming to
  -- recover the standard description of these things, so we allow it here
  -- for convenience.
  fresh : Nat → ė → Set
  fresh x (e ·: t) = fresh x e
  fresh x (X y) = natEQp x y
  fresh x (·λ y e) = natEQp x y × fresh x e
  fresh x (N n) = ⊤
  fresh x (e1 ·+ e2) = fresh x e1 × fresh x e2
  fresh x ⦇-⦈ = ⊤
  fresh x ⦇⌜ e ⌟⦈ = fresh x e
  fresh x (e1 ∘ e2) = fresh x e1 × fresh x e2

  ---- lemmas

  -- freshness interacts with erasure as you'd expect. the proofs below mix
  -- and match between judgmental and functional erasure as usual, so this
  -- is needed enough times to pull it out.
  fresh-er-lem : ∀{ e e◆ x} → erase-e e e◆ → fresh x (e ◆e) → fresh x e◆
  fresh-er-lem er f = tr (λ q → fresh _ q) ( ! (erasee-det er (rel◆ _))) f

  --- a contracted context gives all the same responses as the
  --- non-contracted context
  lem-contract : (Γ : ·ctx) (x : Nat) (t : τ̇) (y : Nat) →
         ((Γ ,, (x , t)) ,, (x , t)) y == (Γ ,, (x , t)) y
  lem-contract Γ x t y with natEQ x y
  lem-contract Γ x t .x | Inl refl = refl
  ... | Inr qq with natEQ x y
  ... | Inl pp = abort (qq pp)
  ... | Inr pp = refl

  --- an exchanged context gives all the same responses as the
  --- non-exchanged context
  lem-swap : (Γ : ·ctx) (x y : Nat) (t1 t2 : τ̇) {x≠y : x == y → ⊥}  (z : Nat) →
         ((Γ ,, (x , t1)) ,, (y , t2)) z == ((Γ ,, (y , t2)) ,, (x , t1)) z
  lem-swap Γ x y t1 t2 z with natEQ x z | natEQ y z
  lem-swap Γ x y t1 t2 {x≠y} z | Inl p | Inl q = abort (x≠y (p · ! q))
  lem-swap Γ x y t1 t2 .x | Inl refl | Inr x₂ with natEQ x x
  lem-swap Γ x y t1 t2 .x | Inl refl | Inr x₂ | Inl refl = refl
  lem-swap Γ x y t1 t2 .x | Inl refl | Inr x₂ | Inr x₁ = abort (x₁ refl)
  lem-swap Γ x y t1 t2 .y | Inr x₁ | Inl refl with natEQ y y
  lem-swap Γ x₁ y t1 t2 .y | Inr x₂ | Inl refl | Inl refl = refl
  lem-swap Γ x₁ y t1 t2 .y | Inr x₂ | Inl refl | Inr x = abort (x refl)
  lem-swap Γ x y t1 t2 z | Inr x₁ | Inr x₂ with natEQ x z | natEQ y z
  lem-swap Γ x .x t1 t2 .x | Inr x₂ | Inr x₃ | Inl refl | Inl refl = abort (x₃ refl)
  lem-swap Γ x y t1 t2 .x | Inr x₂ | Inr x₃ | Inl refl | Inr x₁ = abort (x₂ refl)
  lem-swap Γ x y t1 t2 z | Inr x₃ | Inr x₄ | Inr x₁ | Inl x₂ = abort (x₄ x₂)
  lem-swap Γ x y t1 t2 z | Inr x₃ | Inr x₄ | Inr x₁ | Inr x₂ = refl

  -- extending a context with a new variable doesn't change anything under
  lem-extend : ∀{n x Γ t w} →
               (n == x → ⊥) → Γ n == w → (Γ ,, (x , t)) n == w
  lem-extend {n} {x} neq w with natEQ x n
  lem-extend neq w₁ | Inl refl = abort (neq refl)
  lem-extend neq w₁ | Inr x₁ = w₁

  ---- structural properties for the well-typedness jugements
  mutual
    wt-exchange-synth : {Γ : ·ctx} {x y : Nat} {t1 t2 t : τ̇} {e : ė} →
                        {x≠y : x == y → ⊥} →
                        ((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e => t →
                        ((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e => t
    wt-exchange-synth {Γ} {x} {y} {t1} {t2} {t} {e} {x≠y} d =
      tr (λ q → q ⊢ e => t) (funext (lem-swap Γ x y t1 t2 {x≠y = x≠y})) d

    wt-exchange-ana : {Γ : ·ctx} {x y : Nat} {t1 t2 t : τ̇} {e : ė} →
                        (x≠y : x == y → ⊥) →
                        ((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e <= t →
                        ((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e <= t
    wt-exchange-ana {Γ} {x} {y} {t1} {t2} {t} {e} x≠y d =
      tr (λ q → q ⊢ e <= t) (funext (lem-swap Γ x y t1 t2 {x≠y = x≠y})) d

  mutual
    wt-contract-synth : {Γ : ·ctx} {x : Nat} {t t' : τ̇} {e : ė} →
                    ((Γ ,, (x , t')) ,, (x , t')) ⊢ e => t →
                    (Γ ,, (x , t')) ⊢ e => t
    wt-contract-synth {Γ} {x} {t} {t'} {e}  wt =
         tr (λ q → q ⊢ e => t) (funext (lem-contract Γ x t')) wt

    wt-contract-ana : (Γ : ·ctx) (x : Nat) (t t' : τ̇) (e : ė) →
                    ((Γ ,, (x , t')) ,, (x , t')) ⊢ e <= t →
                    (Γ ,, (x , t')) ⊢ e <= t
    wt-contract-ana Γ x t t' e wt =
         tr (λ q → q ⊢ e <= t) (funext (lem-contract Γ x t')) wt

  mutual
    wt-weak-synth : {Γ : ·ctx} {x : Nat} {t t' : τ̇} {e : ė} →
                    x # Γ →
                    Γ ⊢ e => t →
                    fresh x e →
                    (Γ ,, (x , t')) ⊢ e => t
    wt-weak-synth apt (SAsc x₁) f = SAsc (wt-weak-ana apt x₁ f)
    wt-weak-synth {x = x} apt (SVar {n = n} x₁) f with natEQ n x
    wt-weak-synth apt (SVar x₂) f | Inl refl = abort (somenotnone (! x₂ · apt))
    wt-weak-synth apt (SVar x₂) f | Inr x₁ = SVar (lem-extend x₁ x₂)
    wt-weak-synth apt (SAp wt x₁ x₂) (f1 , f2) = SAp (wt-weak-synth apt wt f1) x₁ (wt-weak-ana apt x₂ f2)
    wt-weak-synth apt SNum f = SNum
    wt-weak-synth apt (SPlus x₁ x₂) (f1 , f2) = SPlus (wt-weak-ana apt x₁ f1) (wt-weak-ana apt x₂ f2)
    wt-weak-synth apt SEHole f = SEHole
    wt-weak-synth apt (SNEHole wt) f = SNEHole (wt-weak-synth apt wt f)

    wt-weak-ana : {Γ : ·ctx} {x : Nat} {t t' : τ̇} {e : ė} →
                    x # Γ →
                    Γ ⊢ e <= t →
                    fresh x e →
                    (Γ ,, (x , t')) ⊢ e <= t
    wt-weak-ana apt (ASubsume x₁ x₂) f = ASubsume (wt-weak-synth apt x₁ f) x₂
    wt-weak-ana {x = x} apt (ALam {x = x₁} x₂ x₃ wt) f with natEQ x x₁
    wt-weak-ana apt (ALam x₃ x₄ wt) (f1 , _) | Inl refl = abort f1
    wt-weak-ana apt (ALam x₃ m wt) (f1 , f2) | Inr x₂ = ALam (lem-extend (flip x₂) x₃) m (wt-exchange-ana (flip x₂) (wt-weak-ana (lem-extend x₂ apt) wt f2))

  ---- structural properties for the action jugements
  mutual
    act-exchange-synth : ∀{ Γ x y t1 t2 t t' e e' α } →
                         (x == y → ⊥) →
                         ((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e => t ~ α ~> e' => t' →
                         ((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e => t ~ α ~> e' => t'
    act-exchange-synth {Γ} {x} {y} {t1} {t2} {t} {t'} {e} {e'} {α} x≠y d = tr (λ q → q ⊢ e => t ~ α ~> e' => t') (funext (lem-swap Γ x y t1 t2 {x≠y})) d

    act-exchange-ana :  ∀{ Γ x y t1 t2 t e e' α } →
                         (x == y → ⊥) →
                         ((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e ~ α ~> e' ⇐ t →
                         ((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e ~ α ~> e' ⇐ t
    act-exchange-ana {Γ} {x} {y} {t1} {t2} {t} {e} {e'} {α} x≠y d = tr (λ q → q ⊢ e ~ α ~> e' ⇐ t) (funext (lem-swap Γ x y t1 t2 {x≠y})) d

  mutual
    act-contract-synth : ∀{ Γ x t t' t'' e e' α } →
                         ((Γ ,, (x , t'')) ,, (x , t'')) ⊢ e => t ~ α ~> e' => t' →
                         (Γ ,, (x , t'')) ⊢ e => t ~ α ~> e' => t'
    act-contract-synth {Γ} {x} {t} {t'} {t''} {e} {e'} {α} d = tr (λ q → q ⊢ e => t ~ α ~> e' => t') (funext (lem-contract Γ x t'')) d

    act-contract-ana : ∀{ Γ x t t' e e' α } →
                         ((Γ ,, (x , t')) ,, (x , t')) ⊢ e ~ α ~> e' ⇐ t →
                         (Γ ,, (x , t')) ⊢ e ~ α ~> e' ⇐ t
    act-contract-ana {Γ} {x} {t} {t'} {e} {e'} {α} d = tr (λ q → q ⊢ e ~ α ~> e' ⇐ t) (funext (lem-contract Γ x t')) d

  mutual
    act-weak-synth : ∀{ Γ x t t' t'' e e' α } →
                         x # Γ →
                         fresh x (e ◆e) →
                         fresh x (e' ◆e) →
                         (d : Γ ⊢ e => t ~ α ~> e' => t') →
                         (Γ ,, (x , t'')) ⊢ e => t ~ α ~> e' => t'
    act-weak-synth apt f f' (SAMove x₁) = SAMove x₁
    act-weak-synth apt f f' SADel = SADel
    act-weak-synth apt f f' SAConAsc = SAConAsc
    act-weak-synth {x = x} apt f f' (SAConVar {x = y} p) with natEQ x y
    act-weak-synth apt f f' (SAConVar p) | Inl refl = abort (somenotnone (! p · apt))
    act-weak-synth apt f f' (SAConVar p) | Inr x₂ = SAConVar (lem-extend (flip x₂) p)
    act-weak-synth {x = x} apt f f' (SAConLam {x = y} x₂) with natEQ x y
    act-weak-synth apt f f' (SAConLam x₃) | Inl refl = abort (π1 f')
    act-weak-synth apt f f' (SAConLam x₃) | Inr x₂ = SAConLam (lem-extend (flip x₂) x₃)
    act-weak-synth apt f f' (SAConApArr x₁) = SAConApArr x₁
    act-weak-synth apt f f' (SAConApOtw x₁) = SAConApOtw x₁
    act-weak-synth apt f f' SAConNumlit = SAConNumlit
    act-weak-synth apt f f' (SAConPlus1 x₁) = SAConPlus1 x₁
    act-weak-synth apt f f' (SAConPlus2 x₁) = SAConPlus2 x₁
    act-weak-synth apt f f' SAConNEHole = SAConNEHole
    act-weak-synth apt f f' (SAFinish x₁) = SAFinish (wt-weak-synth apt x₁ f')
    act-weak-synth apt f f' (SAZipAsc1 x₁) = SAZipAsc1 (act-weak-ana apt f f' x₁)
    act-weak-synth apt f f' (SAZipAsc2 x₁ x₂ x₃ x₄) = SAZipAsc2 x₁ x₂ x₃ (wt-weak-ana apt x₄ f')
    act-weak-synth apt f f' (SAZipApArr x₁ x₂ x₃ d x₄) = SAZipApArr x₁ x₂ (wt-weak-synth apt x₃ (fresh-er-lem x₂ (π1 f)))
                                                                          (act-weak-synth apt (π1 f) (π1 f') d)
                                                                          (wt-weak-ana apt x₄ (π2 f'))
    act-weak-synth apt f f' (SAZipApAna x₁ x₂ x₃) = SAZipApAna x₁ (wt-weak-synth apt x₂ (π1 f'))
                                                                  (act-weak-ana apt (π2 f) (π2 f') x₃)
    act-weak-synth apt f f' (SAZipPlus1 x₁) = SAZipPlus1 (act-weak-ana apt (π1 f) (π1 f') x₁)
    act-weak-synth apt f f' (SAZipPlus2 x₁) = SAZipPlus2 (act-weak-ana apt (π2 f) (π2 f') x₁)
    act-weak-synth apt f f' (SAZipHole x₁ x₂ d) = SAZipHole x₁ (wt-weak-synth apt x₂ (fresh-er-lem x₁ f))
                                                               (act-weak-synth apt f f' d)

    act-weak-ana : ∀{ Γ x t t' e e' α } →
                         x # Γ →
                         fresh x (e ◆e) →
                         fresh x (e' ◆e) →
                         (d : Γ ⊢ e ~ α ~> e' ⇐ t) →
                         (Γ ,, (x , t')) ⊢ e ~ α ~> e' ⇐ t
    act-weak-ana apt f f' (AASubsume x₁ x₂ x₃ x₄) = AASubsume x₁ (wt-weak-synth apt x₂ (fresh-er-lem x₁ f)) (act-weak-synth apt f f' x₃) x₄
    act-weak-ana apt f f' (AAMove x₁) = AAMove x₁
    act-weak-ana apt f f' AADel = AADel
    act-weak-ana apt f f' AAConAsc = AAConAsc
    act-weak-ana {x = x} apt f f' (AAConVar {x = y} x₂ p) with natEQ x y
    act-weak-ana apt f f' (AAConVar x₃ p) | Inl refl = abort (somenotnone (! p · apt))
    act-weak-ana apt f f' (AAConVar x₃ p) | Inr x₂ = AAConVar x₃ (lem-extend (flip x₂) p)
    act-weak-ana {x = x} apt f f' (AAConLam1 {x = y} x₂ x₃) with natEQ x y
    act-weak-ana apt f f' (AAConLam1 x₃ x₄) | Inl refl = abort (π1 f')
    act-weak-ana apt f f' (AAConLam1 x₃ x₄) | Inr x₂ = AAConLam1 (lem-extend (flip x₂) x₃) x₄
    act-weak-ana {x = x} apt f f' (AAConLam2 {x = y} x₂ x₃) with natEQ x y
    act-weak-ana apt f f' (AAConLam2 x₃ x₄) | Inl refl = abort (π1 f')
    act-weak-ana apt f f' (AAConLam2 x₃ x₄) | Inr x₂ = AAConLam2 (lem-extend (flip x₂) x₃) x₄
    act-weak-ana apt f f' (AAConNumlit x₁) = AAConNumlit x₁
    act-weak-ana apt f f' (AAFinish x₁) = AAFinish (wt-weak-ana apt x₁ f')
    act-weak-ana {x = x} apt f f' (AAZipLam {x = y} x₂ x₃ d) with natEQ x y
    act-weak-ana apt f f' (AAZipLam x₃ x₄ d) | Inl refl = abort (π1 f')
    act-weak-ana apt f f' (AAZipLam x₃ x₄ d) | Inr x₂ = AAZipLam (lem-extend (flip x₂) x₃) x₄ (act-exchange-ana (flip x₂) (act-weak-ana (lem-extend x₂ apt) (π2 f) (π2 f') d))

ext: agda


text:
module Sets.IterativeSet.Oper.Proofs where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using ()
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Equals using () renaming (_≡_ to Id ; [≡]-intro to intro)
open import Sets.IterativeSet.Oper
open import Sets.IterativeSet.Relator
open import Sets.IterativeSet.Relator.Proofs
open import Sets.IterativeSet
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Function
open import Syntax.Transitivity
open import Type.Dependent
open import Type.Properties.Decidable
open import Type.Properties.Decidable.Proofs

module _ where
  private variable {ℓ ℓ₁ ℓ₂} : Lvl.Level
  open Iset

  -- If there is an element in the empty set, then there exists an instance of the empty type by definition, and that is false by definition.
  ∅-membership : ∀{x : Iset{ℓ₁}} → (x ∉ ∅ {ℓ₂})
  ∅-membership ()

  -- There is a bijection between (A ‖ B) and ∃{Lvl.Up Bool}(\{(Lvl.up 𝐹) → A ; (Lvl.up 𝑇) → B}).
  pair-membership : ∀{a b x : Iset{ℓ}} → (x ∈ pair a b) ↔ (x ≡ a)∨(x ≡ b)
  Tuple.left (pair-membership {a = a} {x}) ([∨]-introₗ p) = [∃]-intro (Lvl.up 𝐹) ⦃ p ⦄
  Tuple.left (pair-membership {a = a} {x}) ([∨]-introᵣ p) = [∃]-intro (Lvl.up 𝑇) ⦃ p ⦄
  Tuple.right (pair-membership {a = a} {x}) ([∃]-intro (Lvl.up 𝐹) ⦃ eq ⦄) = [∨]-introₗ eq
  Tuple.right (pair-membership {a = a} {x}) ([∃]-intro (Lvl.up 𝑇) ⦃ eq ⦄) = [∨]-introᵣ eq

  -- There is a bijection between (A) and ∃{Unit}(\{<> → A}).
  singleton-membership : ∀{a x : Iset{ℓ}} → (x ∈ singleton(a)) ↔ (x ≡ a)
  Tuple.left (singleton-membership {a = a} {x}) xin = [∃]-intro <> ⦃ xin ⦄
  Tuple.right (singleton-membership {a = a} {x}) ([∃]-intro i ⦃ eq ⦄ ) = eq

  [∪]-membership : ∀{A B x : Iset{ℓ}} → (x ∈ (A ∪ B)) ↔ (x ∈ A)∨(x ∈ B)
  Tuple.left ([∪]-membership {A = A} {B} {x}) ([∨]-introₗ ([∃]-intro ia)) = [∃]-intro (Either.Left  ia)
  Tuple.left ([∪]-membership {A = A} {B} {x}) ([∨]-introᵣ ([∃]-intro ib)) = [∃]-intro (Either.Right ib)
  Tuple.right ([∪]-membership {A = A} {B} {x}) ([∃]-intro ([∨]-introₗ ia)) = [∨]-introₗ ([∃]-intro ia)
  Tuple.right ([∪]-membership {A = A} {B} {x}) ([∃]-intro ([∨]-introᵣ ib)) = [∨]-introᵣ ([∃]-intro ib)

  [⋃]-membership : ∀{A x : Iset{ℓ}} → (x ∈ (⋃ A)) ↔ ∃(a ↦ (a ∈ A) ∧ (x ∈ a))
  Σ.left  (∃.witness (Tuple.left ([⋃]-membership {A = A} {x}) ([∃]-intro a ⦃ [∧]-intro ([∃]-intro iA) _ ⦄))) = iA
  Σ.right (∃.witness (Tuple.left ([⋃]-membership {A = A} {x}) ([∃]-intro a ⦃ [∧]-intro ([∃]-intro iA ⦃ aA ⦄) ([∃]-intro ia) ⦄))) = _⊆_.map (Tuple.right aA) ia
  ∃.proof (Tuple.left ([⋃]-membership {A = A} {x}) ([∃]-intro a ⦃ [∧]-intro ([∃]-intro iA ⦃ aA ⦄) ([∃]-intro ia ⦃ xa ⦄) ⦄)) = [≡]-transitivity-raw xa ([⊆]-with-elem (sub₂(_≡_)(_⊆_) aA) {ia})
  ∃.witness (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄)) = elem(A)(iA)
  Tuple.left (∃.proof (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄))) = [∈]-of-elem {A = A}
  ∃.witness (Tuple.right (∃.proof (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄)))) = ia
  ∃.proof (Tuple.right (∃.proof (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄)))) = proof

  module _ {A : Iset{ℓ}} where
    open import Relator.Equals.Proofs.Equivalence using ([≡]-equiv)
    instance _ = [≡]-equiv {T = Index(A)}

    module _ {P : Index(A) → Stmt{ℓ}} where
      indexFilter-elem-membershipₗ : ∀{i : Index(A)} → (elem(A)(i) ∈ indexFilter A P) ← P(i)
      Σ.left (∃.witness ((indexFilter-elem-membershipₗ {i = i}) pi)) = i
      Σ.right(∃.witness ((indexFilter-elem-membershipₗ {i = i}) pi)) = pi
      Tuple.left  (∃.proof (indexFilter-elem-membershipₗ pi)) = intro id [≡]-reflexivity-raw
      Tuple.right (∃.proof (indexFilter-elem-membershipₗ pi)) = intro id [≡]-reflexivity-raw

    module _
      ⦃ _ : Injective(elem A) ⦄ -- TODO: Is this satisfiable?
      {P : Index(A) → Stmt{ℓ}}
      ⦃ unaryRelator-P : UnaryRelator(P) ⦄
      where

      indexFilter-elem-membership : ∀{i : Index(A)} → (elem(A)(i) ∈ indexFilter A P) ↔ P(i)
      Tuple.left   indexFilter-elem-membership = indexFilter-elem-membershipₗ
      Tuple.right (indexFilter-elem-membership {i = i}) ([∃]-intro (intro iA PiA) ⦃ pp ⦄) = substitute₁(P) (injective(elem A) (symmetry(_≡_) pp)) PiA

  filter-elem-membership : ∀{A : Iset{ℓ}}{P} ⦃ _ : UnaryRelator(P) ⦄ {i : Index(A)} → (elem(A)(i) ∈ filter A P) ↔ P(elem(A)(i))
  Tuple.left  (filter-elem-membership {A = A}{P = P}) = indexFilter-elem-membershipₗ {A = A}{P = P ∘ elem(A)}
  Tuple.right (filter-elem-membership {P = P}) ([∃]-intro (intro iA PiA) ⦃ pp ⦄) = substitute₁(P) (symmetry(_≡_) pp) PiA

  filter-membership : ∀{A : Iset{ℓ}}{P} ⦃ _ : UnaryRelator(P) ⦄ {x : Iset{ℓ}} → (x ∈ filter A P) ↔ ((x ∈ A) ∧ P(x))
  ∃.witness (Tuple.left(filter-membership {P = P}) ([∧]-intro ([∃]-intro i ⦃ p ⦄) pb)) = intro i (substitute₁(P) p pb)
  ∃.proof   (Tuple.left(filter-membership) ([∧]-intro ([∃]-intro i ⦃ p ⦄) pb)) = p
  ∃.witness (Tuple.left (Tuple.right(filter-membership) ([∃]-intro (intro iA PiA) ⦃ pp ⦄))) = iA
  ∃.proof (Tuple.left (Tuple.right(filter-membership) ([∃]-intro (intro iA PiA) ⦃ pp ⦄))) = pp
  Tuple.right (Tuple.right(filter-membership {P = P}) ([∃]-intro (intro iA PiA) ⦃ pp ⦄)) = substitute₁(P) (symmetry(_≡_) pp) PiA

  mapSet-membership : ∀{A : Iset{ℓ}}{f} ⦃ _ : Function(f) ⦄ {y : Iset{ℓ}} → (y ∈ mapSet f(A)) ↔ ∃(x ↦ (x ∈ A) ∧ (y ≡ f(x)))
  ∃.witness (Tuple.left  (mapSet-membership)                         ([∃]-intro x ⦃ [∧]-intro xA fxy ⦄)) = [∃]-witness xA
  ∃.proof   (Tuple.left  (mapSet-membership {A = A} {f = f} {y = y}) ([∃]-intro x ⦃ [∧]-intro xA fxy ⦄)) =
    y                                   🝖[ _≡_ ]-[ fxy ]
    f(x)                                🝖[ _≡_ ]-[ congruence₁(f) ([∃]-proof xA) ]
    f(elem(A) ([∃]-witness xA))         🝖[ _≡_ ]-[]
    elem (mapSet f(A)) ([∃]-witness xA) 🝖[ _≡_ ]-end
  ∃.witness (Tuple.right (mapSet-membership {A = A}) ([∃]-intro iA)) = elem(A) iA
  Tuple.left  (∃.proof (Tuple.right (mapSet-membership {A = A}) ([∃]-intro iA ⦃ p ⦄))) = [∈]-of-elem {A = A} {ia = iA}
  Tuple.right (∃.proof (Tuple.right  mapSet-membership          ([∃]-intro iA ⦃ p ⦄))) = p

  open import Logic.Classical
  module _ ⦃ classical : ∀{ℓ}{P} → Classical{ℓ}(P) ⦄ where
    instance _ = classical-to-decidable
    instance _ = classical-to-decider

    indexFilterBool-subset : ∀{A : Iset{ℓ}}{P} → (indexFilterBool A P ⊆ A)
    _⊇_.map indexFilterBool-subset (intro iA _) = iA
    _⊇_.proof (indexFilterBool-subset {ℓ = ℓ}{A = A}{P = P}) {intro iA (Lvl.up PiA)} =
      elem (indexFilterBool A P) (intro iA (Lvl.up PiA))                   🝖[ _≡_ ]-[]
      elem (indexFilter A (Lvl.Up ∘ IsTrue ∘ P)) (intro iA (Lvl.up PiA))   🝖[ _≡_ ]-[]
      elem A (Σ.left {B = Lvl.Up{ℓ} ∘ IsTrue ∘ P} (intro iA (Lvl.up PiA))) 🝖[ _≡_ ]-[]
      elem A iA                                                            🝖[ _≡_ ]-end

    ℘-membershipₗ : ∀{A : Iset{ℓ}}{B : Iset{ℓ}} → (B ∈ ℘(A)) ← (B ⊆ A)
    ∃.witness (℘-membershipₗ {A = A}{B = B} BA) iA = decide(0)(∃(iB ↦ Id(_⊆_.map BA iB) iA))
    _⊇_.map (Tuple.left (∃.proof (℘-membershipₗ {A = A} {B = B} _))) (intro iA (Lvl.up mapiBiA)) = [∃]-witness([↔]-to-[←] decider-true mapiBiA)
    _⊇_.proof (Tuple.left (∃.proof (℘-membershipₗ {ℓ = ℓ} {A = A} {B = B} BA))) {intro iA (Lvl.up mapiBiA)} =
      elem (elem (℘ A) f) (intro iA (Lvl.up mapiBiA))                          🝖[ _≡_ ]-[]
      elem (indexFilterBool A f) (intro iA (Lvl.up mapiBiA))                   🝖[ _≡_ ]-[]
      elem (indexFilter A (Lvl.Up ∘ IsTrue ∘ f)) (intro iA (Lvl.up mapiBiA))   🝖[ _≡_ ]-[]
      elem A (Σ.left {B = Lvl.Up{ℓ} ∘ IsTrue ∘ f} (intro iA (Lvl.up mapiBiA))) 🝖[ _≡_ ]-[]
      elem A iA                                                                🝖[ _≡_ ]-[ [≡]-to-equivalence(congruence₁(elem A) ([∃]-proof emapiBiA)) ]-sym
      elem A (_⊆_.map BA ([∃]-witness emapiBiA))                               🝖[ _≡_ ]-[ _⊆_.proof BA {[∃]-witness emapiBiA} ]-sym
      elem B ([∃]-witness emapiBiA)                                            🝖[ _≡_ ]-end
      where
        f = \iA → decide(0)(∃(iB ↦ Id(_⊆_.map BA iB) iA))
        emapiBiA = [↔]-to-[←] decider-true mapiBiA
        open import Relator.Equals.Proofs.Equiv using ([≡]-to-equivalence)
    _⊇_.map (Tuple.right (∃.proof (℘-membershipₗ {A = A} {B = B} BA))) iB = intro (_⊆_.map BA iB) (Lvl.up ([↔]-to-[→] decider-true ([∃]-intro iB ⦃ intro ⦄)))
    _⊇_.proof (Tuple.right (∃.proof (℘-membershipₗ {A = A} {B = B} BA))) = _⊆_.proof BA

    ℘-membershipᵣ : ∀{A : Iset{ℓ}}{B : Iset{ℓ}} → (B ∈ ℘(A)) → (B ⊆ A)
    ℘-membershipᵣ ([∃]-intro witness ⦃ b≡indexFilterBool ⦄) = substitute₂ₗ(_⊆_) (symmetry(_≡_) b≡indexFilterBool) indexFilterBool-subset

    ℘-membership : ∀{A : Iset{ℓ}}{x : Iset{ℓ}} → (x ∈ ℘(A)) ↔ (x ⊆ A)
    ℘-membership = [↔]-intro ℘-membershipₗ ℘-membershipᵣ

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Tensor where

open import Basics
open import Ix
open import All
open import Perm
open import Cutting
open import Recutter

open _|>_
open RECUTTER
open SUBCOLLECTLEMMA

_><_ : forall {I J} -> (I |> I) -> (J |> J) -> (I * J) |> (I * J)
Cuts   (C >< D) (i , j) = Cuts C i + Cuts D j
inners (C >< D) {i , j} (inl c) = list (_, j) (inners C c)
inners (C >< D) {i , j} (inr d) = list (i ,_) (inners D d)

module TENSORRECUT  {I J}(C : I |> I)(D : J |> J)(rec : Recutter C)(red : Recutter D) where

  cartLeftLemma : (is : List I)(j : J)(d : Cuts D j) -> subCollect (C >< D) (list (_, j) is)
                (allRe (_, j) is
                   (allPu (\ _ -> inr (inr d)) is)) == cart is (inners D d)
  cartLeftLemma [] j d = refl []
  cartLeftLemma (i ,- is) j d = refl (list (i ,_) (inners D d) +L_) =$= cartLeftLemma is j d

  cartRightLemma : (i : I)(c : Cuts C i)(js : List J) ->
     subCollect (C >< D) (list (i ,_) js)
                 (allRe (i ,_) js (allPu (\ _ -> inr (inl c)) js)) ==
                 list swap (cart js (inners C c))
  cartRightLemma i c [] = refl []
  cartRightLemma i c (j ,- js)
    rewrite sym (catNatural swap (list (j ,_) (inners C c)) (cart js (inners C c)))
                | listlist swap (j ,_) (_, j) (\ i -> refl (i , j)) (inners C c)
                = refl (list (_, j) (inners C c) +L_) =$= cartRightLemma i c js

  TensorRecut : Recutter (C >< D)

  -- both cuts in left dimension
  TensorRecut (i , j) (inl c) (inl c') with rec i c c'
  ... | x , y , m
      = allRe (_, j) (inners C c) (all (\ _ -> id +map inl) _ x)
      , allRe (_, j) (inners C c') (all (\ _ -> id +map inl) _ y)
      , lemma where
        lemma : subCollect (C >< D) (list (_, j) (inners C c))
                 (allRe (_, j) (inners C c) (all (\ _ -> id +map inl) (inners C c) x))
                ~
                subCollect (C >< D) (list (_, j) (inners C c'))
                 (allRe (_, j) (inners C c') (all (\ _ -> id +map inl) (inners C c') y))
        lemma rewrite subCollectLemma C (C >< D) (_, j) (\ _ -> inl) (\ i c -> refl _)
                        (inners C c) x
                    | subCollectLemma C (C >< D) (_, j) (\ _ -> inl) (\ i c -> refl _)
                        (inners C c') y
          = permap (_, j) m

  -- left to right
  fst (TensorRecut (i , j) (inl c) (inr d)) =
    allRe (_, j) (inners C c) (allPu (\ i -> inr (inr d)) (inners C c))
  fst (snd (TensorRecut (i , j) (inl c) (inr d))) =
    allRe (i ,_) (inners D d) (allPu (\ i -> inr (inl c)) (inners D d))
  snd (snd (TensorRecut (i , j) (inl c) (inr d)))
    rewrite cartLeftLemma (inners C c) j d
          | cartRightLemma i c (inners D d)
          = cartLemma (inners C c) (inners D d)

  -- right to left
  fst (TensorRecut (i , j) (inr d) (inl c)) =
    allRe (i ,_) (inners D d) (allPu (\ i -> inr (inl c)) (inners D d))
  fst (snd (TensorRecut (i , j) (inr d) (inl c))) =
    allRe (_, j) (inners C c) (allPu (\ i -> inr (inr d)) (inners C c))
  snd (snd (TensorRecut (i , j) (inr d) (inl c)))
    rewrite cartLeftLemma (inners C c) j d
          | cartRightLemma i c (inners D d)
          = symP (cartLemma (inners C c) (inners D d))

  -- both cuts in right dimension
  TensorRecut (i , j) (inr d) (inr d') with red j d d'
  ... | x , y , m
    = allRe (i ,_) (inners D d) (all (\ _ -> id +map inr) _ x)
    , allRe (i ,_) (inners D d') (all (\ _ -> id +map inr) _ y)
    , lemma where
        lemma : subCollect (C >< D) (list (i ,_) (inners D d))
                 (allRe (i ,_) (inners D d) (all (\ _ -> id +map inr) (inners D d) x))
                ~
                subCollect (C >< D) (list (i ,_) (inners D d'))
                 (allRe (i ,_) (inners D d') (all (\ _ -> id +map inr) (inners D d') y))
        lemma rewrite subCollectLemma D (C >< D) (i ,_) (\ _ -> inr) (\ i d -> refl _)
                        (inners D d) x
                    | subCollectLemma D (C >< D) (i ,_) (\ _ -> inr) (\ i d -> refl _)
                        (inners D d') y
                    = permap (i ,_) m

module RECTANGLE where

  RectCut = NatCut >< NatCut

  open NATRECUT
  open TENSORRECUT NatCut NatCut NatRecut NatRecut

  RectRecut = TensorRecut

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition for the permutation relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Inductive
  {a} {A : Set a} where

open import Data.List using (List; []; _∷_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.Reasoning.Setoid as EqReasoning

------------------------------------------------------------------------
-- An inductive definition of permutation

infix 3 _↭_

data _↭_ : Rel (List A) a where
  refl  : ∀ {xs}        → xs ↭ xs
  prep  : ∀ {xs ys} x   → xs ↭ ys → x ∷ xs ↭ x ∷ ys
  swap  : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
  trans : ∀ {xs ys zs}  → xs ↭ ys → ys ↭ zs → xs ↭ zs

------------------------------------------------------------------------
-- _↭_ is an equivalence

↭-reflexive : _≡_ ⇒ _↭_
↭-reflexive refl = refl

↭-refl : Reflexive _↭_
↭-refl = refl

↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
↭-sym refl                = refl
↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys)

↭-trans : Transitive _↭_
↭-trans = trans

↭-isEquivalence : IsEquivalence _↭_
↭-isEquivalence = record
  { refl  = refl
  ; sym   = ↭-sym
  ; trans = trans
  }

↭-setoid : Setoid _ _
↭-setoid = record
  { isEquivalence = ↭-isEquivalence
  }

------------------------------------------------------------------------
-- A reasoning API to chain permutation proofs and allow "zooming in"
-- to localised reasoning.

module PermutationReasoning where

  open EqReasoning ↭-setoid
    using (_IsRelatedTo_; relTo)

  open EqReasoning ↭-setoid public
    using (begin_ ; _∎ ; _≡⟨⟩_; _≡⟨_⟩_)
    renaming (_≈⟨_⟩_ to _↭⟨_⟩_; _≈˘⟨_⟩_ to _↭˘⟨_⟩_)

  infixr 2 _∷_<⟨_⟩_  _∷_∷_<<⟨_⟩_

  -- Skip reasoning on the first element
  _∷_<⟨_⟩_ : ∀ x xs {ys zs : List A} → xs ↭ ys →
               (x ∷ ys) IsRelatedTo zs → (x ∷ xs) IsRelatedTo zs
  x ∷ xs <⟨ xs↭ys ⟩ rel = relTo (trans (prep x xs↭ys) (begin rel))

  -- Skip reasoning about the first two elements
  _∷_∷_<<⟨_⟩_ : ∀ x y xs {ys zs : List A} → xs ↭ ys →
                  (y ∷ x ∷ ys) IsRelatedTo zs → (x ∷ y ∷ xs) IsRelatedTo zs
  x ∷ y ∷ xs <<⟨ xs↭ys ⟩ rel = relTo (trans (swap x y xs↭ys) (begin rel))


text:
-- Andreas, 2016-10-06 issue #2239

-- We need to subtract number of locals when computing
-- de Bruijn index of split variable!

-- {-# OPTIONS -v interaction.case:50 #-}

data Bool : Set where
  true false : Bool

test : (x y z : Bool) → Bool
test x y = λ z → {!y !}  -- splitting on y should succeed

fails : (x y z : Bool) → Bool
fails x y = λ z → {!z !}  -- splitting on z should fail

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda