text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Number.Instances.Int where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

open import Number.Instances.Nat using (lemma10''; lemma12'')
open import Number.Prelude.Nat

import Agda.Builtin.Int as Builtin
import Data.Integer.Base as BuiltinBase
import Data.Integer.Properties as BuiltinProps

open import Cubical.Data.Int renaming
  ( Int to ℤ
  ; isSetInt to isSetℤ
  ; _-_ to infix 7 _-_
  ; _+_ to infix 5 _+_
  )

import Cubical.HITs.Ints.QuoInt as QuoInt

-- Cubical.Data.Int is isomorphic to Agda.Builtin.Int
Int≅Builtin : Iso ℤ Builtin.Int
Int≅Builtin .Iso.fun      (        pos    n) = Builtin.pos n
Int≅Builtin .Iso.fun      (        negsuc n) = Builtin.negsuc n
Int≅Builtin .Iso.inv      (Builtin.pos    n) = pos n
Int≅Builtin .Iso.inv      (Builtin.negsuc n) = negsuc n
Int≅Builtin .Iso.rightInv (Builtin.pos    n) = refl
Int≅Builtin .Iso.rightInv (Builtin.negsuc n) = refl
Int≅Builtin .Iso.leftInv  (        pos    n) = refl
Int≅Builtin .Iso.leftInv  (        negsuc n) = refl

Int≡Builtin : ℤ ≡ Builtin.Int
Int≡Builtin = isoToPath Int≅Builtin

Sign : Type₀
Sign = Bool

pattern spos = Bool.false
pattern sneg = Bool.true

_·ˢ_ : Sign → Sign → Sign
_·ˢ_ = Bool._⊕_

sign : ℤ → Sign
sign (pos n)    = spos
sign (negsuc n) = sneg

signed : Sign → ℕ → ℤ
signed spos      x  = pos x
signed sneg  zero   = 0
signed sneg (suc x) = neg (suc x)

-_ : ℤ → ℤ
- pos zero = pos zero
- pos (suc n) = negsuc n
- negsuc n = pos (suc n)

-involutive : ∀ a → - - a ≡ a
-involutive (pos zero) = refl
-involutive (pos (suc n)) = refl
-involutive (negsuc n) = refl

infix 8 -_
infix 7 _·_
infix 7 _·'_
infix 7 _·''_
infixl 4 _<_

-- multiplication on integers
-- NOTE: this definition leads to a lot cases and a lot of calculations
--       the general advice would be to have as few cases as possible
--       because then at a call site we also need not many cases
-- NOTE: the way that QuoInt._+_ is defined works that it reduces the first argument, e.g. it reduces `a` in `a + b`
--       therefore we also need to split (only) on the first argument `a`
--         _+_ : ℤ → ℤ → ℤ
--         (signed _ zero) + n = n
--         (posneg _)      + n = n
--         (pos (suc m))   + n = sucℤ  (pos m + n)
--         (neg (suc m))   + n = predℤ (neg m + n)
--       we might apply something similar for _·_
--       although that is not done for QuoInt._*_
--         _*_ : ℤ → ℤ → ℤ
--         m * n = signed (sign m *S sign n) (abs m ℕ.* abs n)
--       but it is done for ℕ._*_
--         _*_ : Nat → Nat → Nat
--         zero  * m = zero
--         suc n * m = m + n * m
_·_ : ℤ → ℤ → ℤ
pos      a  · pos      b  = pos (a ·ⁿ b)
pos  zero   · negsuc   b  = pos 0
pos (suc a) · negsuc   b  = negsuc (a ·ⁿ b +ⁿ (a +ⁿ b)) -- maybe `(a +ⁿ b) +ⁿ a ·ⁿ b` would be a better choice ?
negsuc   a  · pos  zero   = pos 0
negsuc   a  · pos (suc b) = negsuc (a ·ⁿ b +ⁿ (a +ⁿ b))
negsuc   a  · negsuc   b  = pos (suc a ·ⁿ suc b)

-- an equivalent multiplication on integers
-- NOTE: this is the way it's defined in the noncubical standard library
--       I used it to proof associativity, which seemed incredibly hard for the previous definition
_·'_ : ℤ → ℤ → ℤ
x ·' y  = signed (sign x ·ˢ sign y) (abs x ·ⁿ abs y)

mksigned : Sign → ℕ → ℤ
mksigned s zero = pos 0
mksigned s (suc n) = signed s (suc n)

-- a third multiplication on the integers
-- NOTE: with the use of `mksigned` we need not case-split on the sign, if the absolute value is zero
_·''_ : ℤ → ℤ → ℤ
x ·'' y = mksigned (sign x ·ˢ sign y) (abs x ·ⁿ abs y)

abstract
  ·''-nullifiesʳ : ∀ x → x ·'' 0 ≡ 0
  ·''-nullifiesʳ (pos    n) i = mksigned spos (·ⁿ-nullifiesʳ n i)
  ·''-nullifiesʳ (negsuc n) i = mksigned sneg (·ⁿ-nullifiesʳ n i)

-- hProp-valued _<_
_<_ : ∀(x y : ℤ) → hProp ℓ-zero
pos    x < pos    y = x <ⁿ y
pos    x < negsuc y = ⊥
negsuc x < pos    y = ⊤
negsuc x < negsuc y = y <ⁿ x

min : ℤ → ℤ → ℤ
min (pos    x) (pos    y) = pos (minⁿ x y)
min (pos    x) (negsuc y) = negsuc y
min (negsuc x) (pos    y) = negsuc x
min (negsuc x) (negsuc y) = negsuc (maxⁿ x y)

max : ℤ → ℤ → ℤ
max (pos    x) (pos    y) = pos (maxⁿ x y)
max (pos    x) (negsuc y) = pos x
max (negsuc x) (pos    y) = pos y
max (negsuc x) (negsuc y) = negsuc (minⁿ x y)

-- some calculations that arose in the proofs
private
  abstract
    lemma1 : ∀ a b → a ·ⁿ b +ⁿ (a +ⁿ b) ≡ b +ⁿ a ·ⁿ suc b
    lemma1 a b = a ·ⁿ b +ⁿ (a +ⁿ b)  ≡⟨ (λ i → +ⁿ-assoc (a ·ⁿ b) a b i) ⟩
                (a ·ⁿ b +ⁿ a) +ⁿ b  ≡⟨ (λ i → +ⁿ-comm (a ·ⁿ b) a i +ⁿ b) ⟩
                (a +ⁿ a ·ⁿ b) +ⁿ b  ≡⟨ (λ i → +ⁿ-comm (a +ⁿ a ·ⁿ b) b i) ⟩
                b +ⁿ (a +ⁿ a ·ⁿ b)  ≡⟨ (λ i → b +ⁿ ·ⁿ-suc a b (~ i)) ⟩
                b +ⁿ a ·ⁿ suc b     ∎

    lemma2 : ∀ a b c →  c +ⁿ (b +ⁿ a ·ⁿ suc b) ·ⁿ suc c
                     ≡ (c +ⁿ b ·ⁿ suc c) +ⁿ a ·ⁿ suc (c +ⁿ b ·ⁿ suc c)
    lemma2 a b c =
      c +ⁿ (b +ⁿ a ·ⁿ suc b) ·ⁿ suc c                 ≡⟨ (λ i → c +ⁿ ·ⁿ-distribʳ b (a ·ⁿ suc b) (suc c) (~ i)) ⟩
      c +ⁿ (b ·ⁿ suc c +ⁿ (a ·ⁿ suc b) ·ⁿ suc c)      ≡⟨ +ⁿ-assoc c _ _ ⟩
      (c +ⁿ b ·ⁿ suc c) +ⁿ (a ·ⁿ suc b) ·ⁿ suc c      ≡⟨ (λ i → (c +ⁿ b ·ⁿ suc c) +ⁿ ·ⁿ-assoc a (suc b) (suc c) (~ i)) ⟩
      (c +ⁿ b ·ⁿ suc c) +ⁿ a ·ⁿ (suc b ·ⁿ suc c)      ≡⟨ refl ⟩
      (c +ⁿ b ·ⁿ suc c) +ⁿ a ·ⁿ suc (c +ⁿ b ·ⁿ suc c) ∎

    lemma3 : ∀ y z → y ·ⁿ z +ⁿ (y +ⁿ z) ≡ y ·ⁿ suc z +ⁿ z
    lemma3 y z =     y ·ⁿ z +ⁿ (y +ⁿ z) ≡⟨ +ⁿ-assoc (y ·ⁿ z) y z ⟩
                   (y ·ⁿ z +ⁿ y) +ⁿ z  ≡⟨ (λ i → +ⁿ-comm (y ·ⁿ z) y i +ⁿ z) ⟩
                   (y +ⁿ y ·ⁿ z) +ⁿ z  ≡⟨ (λ i → ·ⁿ-suc y z (~ i) +ⁿ z) ⟩
                    y ·ⁿ suc z +ⁿ z    ∎

    lemma4 = λ(a b : ℕ) →
      a ·ⁿ suc b +ⁿ (a +ⁿ suc b)    ≡⟨ (λ i → ·ⁿ-suc a b i +ⁿ (a +ⁿ suc b)) ⟩
      (a +ⁿ a ·ⁿ b) +ⁿ (a +ⁿ suc b) ≡⟨ sym $ +ⁿ-assoc a (a ·ⁿ b) (a +ⁿ suc b) ⟩
      a +ⁿ (a ·ⁿ b +ⁿ (a +ⁿ suc b)) ≡⟨ (λ i → a +ⁿ +ⁿ-assoc (a ·ⁿ b) a (suc b) i) ⟩
      a +ⁿ ((a ·ⁿ b +ⁿ a) +ⁿ suc b) ≡⟨ (λ i → a +ⁿ +ⁿ-suc (a ·ⁿ b +ⁿ a) b i) ⟩
      a +ⁿ suc ((a ·ⁿ b +ⁿ a) +ⁿ b) ≡⟨ (λ i → a +ⁿ suc (+ⁿ-assoc (a ·ⁿ b) a b (~ i))) ⟩
      a +ⁿ suc (a ·ⁿ b +ⁿ (a +ⁿ b)) ∎

    lemma5 = λ(a b : ℕ) →
              a +ⁿ (b +ⁿ a ·ⁿ suc b) ≡⟨ +ⁿ-assoc a b (a ·ⁿ suc b) ⟩
              (a +ⁿ b) +ⁿ a ·ⁿ suc b ≡⟨ (λ i → +ⁿ-comm a b i +ⁿ a ·ⁿ suc b) ⟩
              (b +ⁿ a) +ⁿ a ·ⁿ suc b ≡⟨ sym $ +ⁿ-assoc b a (a ·ⁿ suc b) ⟩
              b +ⁿ (a +ⁿ a ·ⁿ suc b) ≡⟨ (λ i → b +ⁿ ·ⁿ-suc a (suc b) (~ i)) ⟩
              b +ⁿ a ·ⁿ suc (suc b)  ∎

    lemma6 : ∀ m n → suc (m +ⁿ n ·ⁿ suc (suc (suc m))) ≡ suc n +ⁿ (m +ⁿ n ·ⁿ suc (suc m))
    lemma6 m n = suc (m +ⁿ n ·ⁿ suc (suc (suc m)))  ≡⟨ (λ i → suc $ m +ⁿ ·ⁿ-suc n (suc (suc m)) i) ⟩
              suc (m +ⁿ (n +ⁿ n ·ⁿ suc (suc m))) ≡⟨ (λ i → suc $ +ⁿ-assoc m n (n ·ⁿ (suc (suc m))) i) ⟩
              suc ((m +ⁿ n) +ⁿ n ·ⁿ suc (suc m)) ≡⟨ (λ i → suc $ +ⁿ-comm m n i +ⁿ n ·ⁿ suc (suc m)) ⟩
              suc ((n +ⁿ m) +ⁿ n ·ⁿ suc (suc m)) ≡⟨ (λ i → suc $ +ⁿ-assoc n m (n ·ⁿ (suc (suc m))) (~ i)) ⟩
              suc (n +ⁿ (m +ⁿ n ·ⁿ suc (suc m))) ≡⟨ refl ⟩
              suc n +ⁿ (m +ⁿ n ·ⁿ suc (suc m))   ∎

    lemma7 : ∀ a b → b +ⁿ a ·ⁿ suc b ≡ a +ⁿ b ·ⁿ suc a
    lemma7 a b =
      b +ⁿ a ·ⁿ suc b    ≡⟨ (λ i → b +ⁿ ·ⁿ-suc a b i) ⟩
      b +ⁿ (a +ⁿ a ·ⁿ b) ≡⟨ (λ i → +ⁿ-assoc b a (a ·ⁿ b) i) ⟩
      (b +ⁿ a) +ⁿ a ·ⁿ b ≡⟨ (λ i → +ⁿ-comm b a i +ⁿ a ·ⁿ b) ⟩
      (a +ⁿ b) +ⁿ a ·ⁿ b ≡⟨ (λ i → +ⁿ-assoc a b (a ·ⁿ b) (~ i)) ⟩
      a +ⁿ (b +ⁿ a ·ⁿ b) ≡⟨ (λ i → a +ⁿ (b +ⁿ ·ⁿ-comm a b i)) ⟩
      a +ⁿ (b +ⁿ b ·ⁿ a) ≡⟨ (λ i → a +ⁿ ·ⁿ-suc b a (~ i)) ⟩
      a +ⁿ b ·ⁿ suc a    ∎

abstract
  <-irrefl : (a : ℤ) → [ ¬ (a < a) ]
  <-irrefl (pos  zero  ) = <ⁿ-irrefl 0
  <-irrefl (pos (suc n)) = <ⁿ-irrefl (suc n)
  <-irrefl (negsuc   n ) = <ⁿ-irrefl n

  <-trans : (a b c : ℤ) → [ a < b ] → [ b < c ] → [ a < c ]
  <-trans (pos    a) (pos    b) (pos    c) a<b b<c = <ⁿ-trans a<b b<c
  <-trans (negsuc a) (pos    b) (pos    c) a<b b<c = tt
  <-trans (negsuc a) (negsuc b) (pos    c) a<b b<c = tt
  <-trans (negsuc a) (negsuc b) (negsuc c) a<b b<c = <ⁿ-trans b<c a<b

  <-asym : (a b : ℤ) → [ a < b ] → [ ¬(b < a) ]
  <-asym = irrefl+trans⇒asym _<_ <-irrefl <-trans

  <-cotrans : (a b : ℤ) → [ a < b ] → (x : ℤ) → [ (a < x) ⊔ (x < b) ]
  <-cotrans (pos    a) (pos    b) a<b (pos    x) = <ⁿ-cotrans _ _ a<b x
  <-cotrans (pos    a) (pos    b) a<b (negsuc x) = inrᵖ tt
  <-cotrans (negsuc a) (pos    b) a<b (pos    x) = inlᵖ tt
  <-cotrans (negsuc a) (pos    b) a<b (negsuc x) = inrᵖ tt
  <-cotrans (negsuc a) (negsuc b) a<b (pos    x) = inlᵖ tt
  <-cotrans (negsuc a) (negsuc b) a<b (negsuc x) = pathTo⇒ (⊔-comm (b <ⁿ x) (x <ⁿ a)) (<ⁿ-cotrans _ _ a<b x)

-- some properties about `pos`, `negsuc`, `+pos` and `+negsuc`
abstract
  +-identityʳ : ∀ x → x + 0 ≡ x
  +-identityʳ x = refl

  +-identityˡ : ∀ x → 0 + x ≡ x
  +-identityˡ x = +-comm 0 x ∙ +-identityʳ x

  -- usage count: 3
  -1·≡- : ∀ a → negsuc 0 · a ≡ - a
  -1·≡- (pos zero) = refl
  -1·≡- (pos (suc n)) = refl
  -1·≡- (negsuc n) = λ i → pos $ suc $ +ⁿ-comm n 0 i

  -- usage count: 0
  negsuc≡-pos : ∀ a → negsuc a ≡ - pos (suc a)
  negsuc≡-pos a = refl

  -- usage count: 2
  negsuc-reflects-≡ : ∀ x y → negsuc x ≡ negsuc y → x ≡ y
  negsuc-reflects-≡ x y p i = predⁿ (abs (p i))

  -- usage count: 2
  pos-reflects-≡ : ∀ x y → pos x ≡ pos y → x ≡ y
  pos-reflects-≡ x y p i = abs (p i)

  -- usage count: 1 - 2
  possuc+negsuc≡0 : ∀ n → (pos (suc n) +negsuc n) ≡ pos 0
  possuc+negsuc≡0 zero = refl
  possuc+negsuc≡0 (suc n) = let r = possuc+negsuc≡0 n in sym ind ∙ r where
    ind =           pos      (suc n)   +negsuc n  ≡⟨ refl ⟩
           predInt (pos (suc (suc n))) +negsuc n  ≡⟨ sym $ predInt+negsuc n (pos (suc (suc n))) ⟩
           predInt (pos (suc (suc n))  +negsuc n) ∎

  -- usage count: 0 - 1
  sucInt[negsuc+pos]≡0 : ∀ n → sucInt (negsuc n +pos n) ≡ pos 0
  sucInt[negsuc+pos]≡0 zero = refl
  sucInt[negsuc+pos]≡0 (suc n) = let r = sucInt[negsuc+pos]≡0 n in sym ind ∙ r where
    ind = sucInt (        negsuc n        +pos n ) ≡⟨ refl ⟩
          sucInt (sucInt (negsuc (suc n)) +pos n ) ≡⟨ (λ i → sucInt $ sucInt+pos n (negsuc (suc n)) (~ i)) ⟩
          sucInt (sucInt (negsuc (suc n)  +pos n)) ∎

  +-inverseʳ : ∀ a → a + (- a) ≡ 0
  +-inverseʳ (pos  zero  ) = refl
  +-inverseʳ (pos (suc n)) = possuc+negsuc≡0 n
  +-inverseʳ (negsuc   n ) = sucInt[negsuc+pos]≡0 n

  +-inverseˡ : ∀ a → (- a) + a ≡ 0
  +-inverseˡ a = +-comm (- a) a ∙ +-inverseʳ a

  +-inverse : (x : ℤ) → (x + (- x) ≡ pos 0) × ((- x) + x ≡ pos 0)
  +-inverse x .fst = +-inverseʳ x
  +-inverse x .snd = +-inverseˡ x

  -- usage count: 11 - 14
  pos+pos≡+ⁿ : ∀ a x → (pos a +pos x) ≡ pos (a +ⁿ x)
  pos+pos≡+ⁿ a zero = λ i → pos $ +ⁿ-comm 0 a i
  pos+pos≡+ⁿ a (suc x) = let r = pos+pos≡+ⁿ a x in
    sucInt (pos a +pos x) ≡⟨ (λ i → sucInt $ r i) ⟩
    sucInt (pos (a +ⁿ x)) ≡⟨ refl ⟩
    pos (suc (a +ⁿ x))    ≡⟨ (λ i → pos $ +ⁿ-suc a x (~ i)) ⟩
    pos (a +ⁿ suc x)      ∎

  -- usage count: 7 - 8
  negsuc+negsuc≡+ⁿ : ∀ a x → (negsuc a +negsuc x) ≡ negsuc (suc (a +ⁿ x))
  negsuc+negsuc≡+ⁿ a zero = λ i → negsuc $ suc $ +ⁿ-comm 0 a i
  negsuc+negsuc≡+ⁿ a (suc x) = let r = negsuc+negsuc≡+ⁿ a x in
    predInt (negsuc a +negsuc x)    ≡⟨ (λ i → predInt (r i)) ⟩
    predInt (negsuc (suc (a +ⁿ x))) ≡⟨ refl ⟩
    negsuc (suc (suc (a +ⁿ x)))     ≡⟨ (λ i → negsuc $ suc $ +ⁿ-suc a x (~ i)) ⟩
    negsuc (suc (a +ⁿ suc x))       ∎

  -- usage count: 6 - 7
  +negsuc-identityˡ : ∀ x → 0 +negsuc x ≡ negsuc x
  +negsuc-identityˡ zero = refl
  +negsuc-identityˡ (suc x) = λ i → predInt $ +negsuc-identityˡ x i

  -- usage count: 0
  pos+negsuc≡⊎ : ∀ a b → (Σ[ y ∈ ℕ ] pos a +negsuc b ≡ pos y) ⊎ (Σ[ y ∈ ℕ ] pos a +negsuc b ≡ negsuc y)
  pos+negsuc≡⊎ zero zero = inr (0 , refl)
  pos+negsuc≡⊎ (suc a) zero = inl (a , refl)
  pos+negsuc≡⊎ zero (suc b) = inr (suc b , λ i → predInt $ +negsuc-identityˡ b i)
  pos+negsuc≡⊎ (suc a) (suc b) with pos+negsuc≡⊎ a b
  ... | inl (y , p) = inl (y , predInt+negsuc b (pos (suc a)) ∙ p)
  ... | inr (y , p) = inr (y , predInt+negsuc b (pos (suc a)) ∙ p)

  -- usage count: 0
  negsuc+pos≡⊎ : ∀ a b → (Σ[ y ∈ ℕ ] negsuc a +pos b ≡ pos y) ⊎ (Σ[ y ∈ ℕ ] negsuc a +pos b ≡ negsuc y)
  negsuc+pos≡⊎ zero zero = inr (0 , refl)
  negsuc+pos≡⊎ (suc a) zero = inr (suc a , refl)
  negsuc+pos≡⊎ zero (suc b) = inl (b , sucInt+pos b (negsuc 0) ∙ +-identityˡ (pos b))
  negsuc+pos≡⊎ (suc a) (suc b) with negsuc+pos≡⊎ a b
  ... | inl (y , p) = inl (y , sucInt+pos b (negsuc (suc a)) ∙ p)
  ... | inr (y , p) = inr (y , sucInt+pos b (negsuc (suc a)) ∙ p)

  -- usage count: 4 - 6
  pos+negsuc≡negsuc+pos : ∀ a b → pos a +negsuc b ≡ negsuc b +pos a
  pos+negsuc≡negsuc+pos a zero = (λ i → predInt $ pos+pos≡+ⁿ 0 a (~ i)) ∙ predInt+pos a 0
  pos+negsuc≡negsuc+pos a (suc b) = (λ i → predInt $ pos+negsuc≡negsuc+pos a b i) ∙ predInt+ (negsuc b) (pos a)

  -- usage count: 0 - 1
  predInt- : ∀ a → predInt (- a) ≡ - (sucInt a)
  predInt- (pos zero) = refl
  predInt- (pos (suc n)) = refl
  predInt- (negsuc zero) = refl
  predInt- (negsuc (suc n)) = refl

  -- usage count: 2 - 3
  pos+negsuc-swap : ∀ a b → pos (suc a) +negsuc b ≡ -(pos (suc b) + negsuc a)
  pos+negsuc-swap zero zero = refl
  pos+negsuc-swap (suc a) zero = λ i → - (predInt+negsuc a 1 ∙ +negsuc-identityˡ a) (~ i)
  pos+negsuc-swap a (suc b) =
    predInt (pos (suc a) +negsuc b)     ≡⟨ (λ i → predInt $ pos+negsuc-swap a b i) ⟩
    predInt (- (pos (suc b) +negsuc a)) ≡⟨ predInt- (pos (suc b) +negsuc a) ⟩
    - sucInt (pos (suc b) +negsuc a)    ≡⟨ (λ i → - sucInt+negsuc a (pos (suc b)) i) ⟩
    - (pos (suc (suc b)) +negsuc a)     ∎

  -- usage count: 2
  negsuc+pos-swap : ∀ a b → negsuc a +pos (suc b) ≡ -(negsuc b + pos (suc a))
  negsuc+pos-swap a b = sym (pos+negsuc≡negsuc+pos (suc b) a) ∙ pos+negsuc-swap b a ∙ (λ i → - pos+negsuc≡negsuc+pos (suc a) b i)

  -- usage count: 1
  +negsuc-assoc : ∀ a b c → a +negsuc (b +ⁿ suc c) ≡ (a +negsuc b) +negsuc c
  +negsuc-assoc a b c = (λ i → a + (negsuc+negsuc≡+ⁿ b c ∙ (λ j → negsuc (+ⁿ-suc b c (~ j)))) (~ i)) ∙ +-assoc a (negsuc b) (negsuc c)

  -- usage count: 1
  sucInt[negsuc+pos]≡pos : ∀ a → sucInt (negsuc 0 +pos a) ≡ pos a
  sucInt[negsuc+pos]≡pos a = sucInt+pos a (negsuc 0) ∙ pos+pos≡+ⁿ 0 a

  -- usage count: 1
  +pos-inverse : ∀ a → negsuc a +pos a ≡ negsuc 0
  +pos-inverse zero = refl
  +pos-inverse (suc a) = sucInt+pos a (negsuc (suc a)) ∙ +pos-inverse a

  -- usage count: 1
  +pos-assoc : ∀ a b c → (a +pos b) +pos c ≡ a +pos (b +ⁿ c)
  +pos-assoc a b c = sym (+-assoc a (pos b) (pos c)) ∙ (λ i → a + pos+pos≡+ⁿ b c i)

data Trichotomy (m n : ℤ) : Type₀ where
  lt : [ m < n ] → Trichotomy m n
  eq :   m ≡ n   → Trichotomy m n
  gt : [ n < m ] → Trichotomy m n

_≟_ : ∀ m n → Trichotomy m n
pos    a ≟ pos    b with a ≟ⁿ b
... | ltⁿ p = lt p
... | eqⁿ p = eq λ i → pos (p i)
... | gtⁿ p = gt p
pos    a ≟ negsuc b = gt tt
negsuc a ≟ pos    b = lt tt
negsuc a ≟ negsuc b with a ≟ⁿ b
... | ltⁿ p = gt p
... | eqⁿ p = eq λ i → negsuc (p i)
... | gtⁿ p = lt p

data MinTrichtotomy (x y : ℤ) : Type where
  min-lt : min x y ≡ x → [ x < y ]   → MinTrichtotomy x y
  min-gt : min x y ≡ y → [ y < x ]   → MinTrichtotomy x y
  min-eq : min x y ≡ x → min x y ≡ y → MinTrichtotomy x y

data MaxTrichtotomy (x y : ℤ) : Type where
  max-lt : max x y ≡ y → [ x < y ]   → MaxTrichtotomy x y
  max-gt : max x y ≡ x → [ y < x ]   → MaxTrichtotomy x y
  max-eq : max x y ≡ x → max x y ≡ y → MaxTrichtotomy x y

min-trichotomy : ∀ x y → MinTrichtotomy x y
min-trichotomy (pos    x) (pos    y) with (pos x) ≟ (pos y)
... | lt p = min-lt (λ i → pos $ minⁿ-tightˡ x y p i) p
... | eq p = let minxy≡x = (λ i → minⁿ x (pos-reflects-≡ x y p (~ i))) ∙ minⁿ-identity x
             in min-eq (λ j → pos $ minxy≡x j) ((λ i → pos $ minxy≡x i) ∙ p)
... | gt p = min-gt (λ i → pos $ minⁿ-tightʳ x y p i) p
min-trichotomy (pos    x) (negsuc y) = min-gt refl tt
min-trichotomy (negsuc x) (pos    y) = min-lt refl tt
min-trichotomy (negsuc x) (negsuc y) with (negsuc x) ≟ (negsuc y)
... | lt p = min-lt (λ i → negsuc $ maxⁿ-tightˡ x y p i) p
... | eq p = let maxxy≡x = (λ i → maxⁿ x (negsuc-reflects-≡ x y p (~ i))) ∙ maxⁿ-identity x
             in min-eq (λ j → negsuc $ maxxy≡x j) ((λ i → negsuc $ maxxy≡x i) ∙ p)
... | gt p = min-gt (λ i → negsuc $ maxⁿ-tightʳ x y p i) p

max-trichotomy : ∀ x y → MaxTrichtotomy x y
max-trichotomy (pos    x) (pos    y) with (pos x) ≟ (pos y)
... | lt p = max-lt ((λ i → pos $ maxⁿ-tightʳ x y p i)) p
... | eq p = let maxxy≡x = (λ i → maxⁿ x (pos-reflects-≡ x y p (~ i))) ∙ maxⁿ-identity x
             in max-eq (λ j → pos $ maxxy≡x j) ((λ i → pos $ maxxy≡x i) ∙ p)
... | gt p = max-gt (λ i → pos $ maxⁿ-tightˡ x y p i) p
max-trichotomy (pos    x) (negsuc y) = max-gt refl tt
max-trichotomy (negsuc x) (pos    y) = max-lt refl tt
max-trichotomy (negsuc x) (negsuc y) with (negsuc x) ≟ (negsuc y)
... | lt p = max-lt (λ i → negsuc $ minⁿ-tightʳ x y p i) p
... | eq p = let minxy≡x = (λ i → minⁿ x (negsuc-reflects-≡ x y p (~ i))) ∙ minⁿ-identity x
             in max-eq (λ j → negsuc $ minxy≡x j) ((λ i → negsuc $ minxy≡x i) ∙ p)
... | gt p = max-gt (λ i → negsuc $ minⁿ-tightˡ x y p i) p

abstract
  -- NOTE: same proof as in `Number.Instances.Nat`
  is-min : (x y z : ℤ) → [ ¬ᵖ (min x y < z) ⇔ ¬ᵖ (x < z) ⊓ ¬ᵖ (y < z) ]
  is-min x y z .fst z≤minxy with min-trichotomy x y
  ... | min-lt p x<y = (λ x<z → z≤minxy $ pathTo⇐ (λ i → p i < z) x<z)
                     , (λ y<z → z≤minxy $ pathTo⇐ (λ i → p i < z) $ <-trans x y z x<y y<z)
  ... | min-gt p y<x = (λ x<z → z≤minxy $ pathTo⇐ (λ i → p i < z) $ <-trans y x z y<x x<z)
                     , (λ y<z → z≤minxy $ pathTo⇐ (λ i → p i < z) y<z)
  ... | min-eq p q   = (λ x<z → z≤minxy $ pathTo⇐ (λ i → p i < z) x<z)
                     , (λ y<z → z≤minxy $ pathTo⇐ (λ i → q i < z) y<z)
  is-min x y z .snd (z≤x , z≤y) minxy<z with min-trichotomy x y
  ... | min-lt p _   = z≤x $ pathTo⇒ (λ i → p i < z) minxy<z
  ... | min-gt p _   = z≤y $ pathTo⇒ (λ i → p i < z) minxy<z
  ... | min-eq p q   = z≤x $ pathTo⇒ (λ i → p i < z) minxy<z

  -- NOTE: same proof as in `Number.Instances.Nat`
  is-max : (x y z : ℤ) → [ ¬ᵖ (z < max x y) ⇔ ¬ᵖ (z < x) ⊓ ¬ᵖ (z < y) ]
  is-max x y z .fst maxxy≤z with max-trichotomy x y
  ... | max-gt p y<x = (λ z<x → maxxy≤z $ pathTo⇐ (λ i → z < p i) z<x )
                     , (λ z<y → maxxy≤z $ pathTo⇐ (λ i → z < p i) $ <-trans z y x z<y y<x )
  ... | max-lt p x<y = (λ z<x → maxxy≤z $ pathTo⇐ (λ i → z < p i) $ <-trans z x y z<x x<y )
                     , (λ z<y → maxxy≤z $ pathTo⇐ (λ i → z < p i) z<y )
  ... | max-eq p q   = (λ z<x → maxxy≤z $ pathTo⇐ (λ i → z < p i) z<x )
                     , (λ z<y → maxxy≤z $ pathTo⇐ (λ i → z < q i) z<y )
  is-max x y z .snd (z≤x , z≤y) maxxy<z with max-trichotomy x y
  ... | max-gt p _   = z≤x $ pathTo⇒ (λ i → z < p i) maxxy<z
  ... | max-lt p _   = z≤y $ pathTo⇒ (λ i → z < p i) maxxy<z
  ... | max-eq p q   = z≤x $ pathTo⇒ (λ i → z < p i) maxxy<z

abstract
  sucInt-reflects-< : ∀ x y → [ sucInt x < sucInt y ] → [ x < y ]
  sucInt-reflects-< (pos         x ) (pos         y ) p = sucⁿ-creates-<ⁿ x y .snd p
  sucInt-reflects-< (pos         x ) (negsuc  zero  ) p = ¬-<ⁿ-zero p
  sucInt-reflects-< (negsuc      x ) (pos         y ) p = tt
  sucInt-reflects-< (negsuc  zero  ) (negsuc  zero  ) p = p
  sucInt-reflects-< (negsuc (suc x)) (negsuc  zero  ) p = 0<ⁿsuc x
  sucInt-reflects-< (negsuc (suc x)) (negsuc (suc y)) p = sucⁿ-creates-<ⁿ y x .fst p

  predInt-reflects-< : ∀ x y → [ predInt x < predInt y ] → [ x < y ]
  predInt-reflects-< (pos  zero  ) (pos  zero  ) p = p
  predInt-reflects-< (pos  zero  ) (pos (suc y)) p = 0<ⁿsuc y
  predInt-reflects-< (pos (suc x)) (pos (suc y)) p = sucⁿ-creates-<ⁿ x y .fst p
  predInt-reflects-< (pos  zero  ) (negsuc   y ) p = ¬-<ⁿ-zero p
  predInt-reflects-< (negsuc   x ) (pos      y ) p = tt
  predInt-reflects-< (negsuc   x ) (negsuc   y ) p = sucⁿ-creates-<ⁿ y x .snd p

  sucInt-preserves-< : ∀ x y → [ x < y ] → [ sucInt x < sucInt y ]
  sucInt-preserves-< (pos         x ) (pos         y ) p = sucⁿ-creates-<ⁿ x y .fst p
  sucInt-preserves-< (negsuc  zero  ) (pos         y ) p = 0<ⁿsuc y
  sucInt-preserves-< (negsuc (suc x)) (pos         y ) p = tt
  sucInt-preserves-< (negsuc  zero  ) (negsuc  zero  ) p = p
  sucInt-preserves-< (negsuc  zero  ) (negsuc (suc y)) p = ¬-<ⁿ-zero p
  sucInt-preserves-< (negsuc (suc x)) (negsuc  zero  ) p = tt
  sucInt-preserves-< (negsuc (suc x)) (negsuc (suc y)) p = sucⁿ-creates-<ⁿ y x .snd p

  predInt-preserves-< : ∀ x y → [ x < y ] → [ predInt x < predInt y ]
  predInt-preserves-< (pos  zero  ) (pos  zero  ) p = p
  predInt-preserves-< (pos  zero  ) (pos (suc y)) p = tt
  predInt-preserves-< (pos (suc x)) (pos  zero  ) p = ¬-<ⁿ-zero p
  predInt-preserves-< (pos (suc x)) (pos (suc y)) p = sucⁿ-creates-<ⁿ x y .snd p
  predInt-preserves-< (negsuc   x ) (pos  zero  ) p = 0<ⁿsuc x
  predInt-preserves-< (negsuc   x ) (pos (suc y)) p = tt
  predInt-preserves-< (negsuc   x ) (negsuc   y ) p = sucⁿ-creates-<ⁿ y x .fst p

abstract
  +-preserves-< : ∀ a b x → [ a < b ] → [ (a + x) < (b + x) ]
  +-preserves-< a b (pos zero) a<b = a<b
  +-preserves-< a b (pos (suc n)) a<b = let r = +-preserves-< a b (pos n) a<b
                                        in sucInt-preserves-< (a +pos n) (b +pos n) r
  +-preserves-< a b (negsuc zero) a<b = predInt-preserves-< a b a<b
  +-preserves-< a b (negsuc (suc n)) a<b = let r = +-preserves-< a b (negsuc n) a<b
                                           in predInt-preserves-< (a +negsuc n) (b +negsuc n) r

  +-reflects-< : ∀ a b x → [ (a + x) < (b + x) ] → [ a < b ]
  +-reflects-< a b x = snd (
    (a + x) < (b + x) ⇒ᵖ⟨ +-preserves-< (a + x) (b + x) (- x) ⟩
    ((a + x) + (- x)) < ((b + x) + (- x)) ⇒ᵖ⟨ (pathTo⇐ λ i → +-assoc a x (- x) i < +-assoc b x (- x) i) ⟩
    (a + (x + (- x))) < (b + (x + (- x))) ⇒ᵖ⟨ (pathTo⇒ λ i → (a + +-inverseʳ x i) < (b + +-inverseʳ x i)) ⟩
    (a + 0) < (b + 0)                     ⇒ᵖ⟨ (λ x → x) ⟩
    a < b             ◼ᵖ)

  +-reflects-<ˡ : ∀ a b x → [ (x + a) < (x + b) ] → [ a < b ]
  +-reflects-<ˡ a b x p = +-reflects-< a b x (transport (λ i → [ +-comm x a i < +-comm x b i ]) p)

abstract
  -- + is <-extentional
  +-<-ext : (w x y z : ℤ) → [ (w + x) < (y + z) ] → [ (w < y) ⊔ (x < z) ]
  +-<-ext w x y z r with w ≟ y | x ≟ z
  ... | lt w<y | q = inlᵖ w<y
  ... | eq w≡y | q = inrᵖ (+-reflects-<ˡ x z y (transport (λ i → [ (w≡y i + x) < (y + z) ]) r))
  ... | gt y<w | q = inrᵖ $ case (<-cotrans (w + x) (y + z) r (y + x)) as ((w + x) < (y + x)) ⊔ ((y + x) < (y + z)) ⇒ x < z of λ
    { (inl p) → ⊥-elim {A = λ _ → [ x < z ]} (<-asym y w y<w (+-reflects-< w y x p))
    ; (inr p) → +-reflects-<ˡ x z y p
    }

-- properties about multiplication
abstract
  -- equality of _·_ and _·'_
  ·≡·' : ∀ x y → x · y ≡ x ·' y
  ·≡·' (pos a) (pos b) = refl
  ·≡·' (pos zero) (negsuc b) = refl
  ·≡·' (pos (suc a)) (negsuc b) =
    negsuc   (a ·ⁿ b +ⁿ (a +ⁿ b))  ≡⟨ (λ i → negsuc $ lemma1 a b i) ⟩
    negsuc   (b +ⁿ a ·ⁿ suc b)     ≡⟨ refl ⟩
    neg (suc (b +ⁿ a ·ⁿ suc b))    ∎
  ·≡·' (negsuc a) (pos zero) = λ i → signed sneg $ ·ⁿ-nullifiesʳ a (~ i)
  ·≡·' (negsuc a) (pos (suc b)) = λ i → negsuc $ lemma1 a b i
  ·≡·' (negsuc a) (negsuc b) = refl

  ·'-nullifiesʳ : ∀ x → x ·' 0 ≡ 0
  ·'-nullifiesʳ (pos    n) i = signed spos (·ⁿ-nullifiesʳ n i)
  ·'-nullifiesʳ (negsuc n) i = signed sneg (·ⁿ-nullifiesʳ n i)

  ·'-nullifiesˡ : ∀ x → 0 ·' x ≡ 0
  ·'-nullifiesˡ (pos    n) i = pos (·ⁿ-nullifiesˡ n i)
  ·'-nullifiesˡ (negsuc n)   = refl

abstract
  -distrˡ : ∀ a b → -(a · b) ≡ (- a) · b
  -distrˡ (pos   zero ) (pos  zero  ) = refl
  -distrˡ (pos   zero ) (pos (suc b)) = refl
  -distrˡ (pos (suc a)) (pos  zero  ) = λ i → - pos (·ⁿ-nullifiesʳ a i)
  -distrˡ (pos (suc a)) (pos (suc b)) = λ i → negsuc $ lemma1 a b (~ i)
  -distrˡ (pos  zero  ) (negsuc   b ) = refl
  -distrˡ (pos (suc a)) (negsuc   b ) = λ i → pos $ suc $ lemma1 a b i
  -distrˡ (negsuc   a ) (pos  zero  ) = λ i → pos (·ⁿ-nullifiesʳ a (~ i))
  -distrˡ (negsuc   a ) (pos (suc b)) = λ i → pos $ suc $ lemma1 a b i
  -distrˡ (negsuc   a ) (negsuc   b ) = λ i → negsuc $ lemma1 a b (~ i)

abstract
  ·-comm : ∀ a b → a · b ≡ b · a
  ·-comm (pos      a ) (pos      b ) = λ i → pos $ ·ⁿ-comm a b i
  ·-comm (pos  zero  ) (negsuc   b ) = refl
  ·-comm (pos (suc a)) (negsuc   b ) = λ i → negsuc $ ·ⁿ-comm a b i +ⁿ +ⁿ-comm a b i
  ·-comm (negsuc   a ) (pos  zero  ) = refl
  ·-comm (negsuc   a ) (pos (suc b)) = λ i → negsuc $ ·ⁿ-comm a b i +ⁿ +ⁿ-comm a b i
  ·-comm (negsuc   a ) (negsuc   b ) i = pos (suc (lemma7 a b i))

  -distrʳ : ∀ a b → -(a · b) ≡ a · (- b)
  -distrʳ a b = (λ i → - ·-comm a b i) ∙ -distrˡ b a ∙ ·-comm (- b) a

abstract
  -- this proof of associativity is ported from `Data.Integer.Properties` which works on
  --   _·_ : ℤ → ℤ → ℤ
  --   i · j = sign i S· sign j ◃ ∣ i ∣ ℕ· ∣ j ∣

  ·'-assoc : ∀ x y z → (x ·' y) ·' z ≡ x ·' (y ·' z)
  ·'-assoc (pos 0) y z = (λ i → ·'-nullifiesˡ y i ·' z) ∙ ·'-nullifiesˡ z ∙ sym (·'-nullifiesˡ (y ·' z))
  ·'-assoc x (pos 0) z = (λ i → ·'-nullifiesʳ x i ·' z) ∙ ·'-nullifiesˡ z ∙ sym (·'-nullifiesʳ x)  ∙ (λ i → x ·' ·'-nullifiesˡ z (~ i))
  ·'-assoc x y (pos 0) = ·'-nullifiesʳ (x ·' y) ∙ sym (·'-nullifiesʳ x) ∙ (λ i → x ·' ·'-nullifiesʳ y (~ i))
  ·'-assoc (negsuc   a ) (negsuc   b ) (pos (suc c)) = λ i → (pos (suc (lemma2 a b c i)))
  ·'-assoc (negsuc   a ) (pos (suc b)) (negsuc   c ) = λ i → (pos (suc (lemma2 a b c i)))
  ·'-assoc (pos (suc a)) (pos (suc b)) (pos (suc c)) = λ i → (pos (suc (lemma2 a b c i)))
  ·'-assoc (pos (suc a)) (negsuc   b ) (negsuc   c ) = λ i → (pos (suc (lemma2 a b c i)))
  ·'-assoc (negsuc   a ) (negsuc   b ) (negsuc   c ) = λ i → (negsuc   (lemma2 a b c i) )
  ·'-assoc (negsuc   a ) (pos (suc b)) (pos (suc c)) = λ i → (negsuc   (lemma2 a b c i) )
  ·'-assoc (pos (suc a)) (negsuc   b ) (pos (suc c)) = λ i → (negsuc   (lemma2 a b c i) )
  ·'-assoc (pos (suc a)) (pos (suc b)) (negsuc   c ) = λ i → (negsuc   (lemma2 a b c i) )

abstract
  -- equality of associativity on _·_ and _·'_
  ·'-assoc≡ : ∀ x y z
            → ((x ·  y) ·  z ≡ x ·  (y ·  z))
            ≡ ((x ·' y) ·' z ≡ x ·' (y ·' z))
  ·'-assoc≡ x y z i = ·≡·' (·≡·' x y i) z i ≡ ·≡·' x (·≡·' y z i) i

  -- associativity of _·_ from associativiy of _·'_
  ·-assoc : ∀ x y z → (x · y) · z ≡ x · (y · z)
  ·-assoc x y z = transport (sym (·'-assoc≡ x y z)) (·'-assoc x y z)

abstract
  ·-nullifiesˡ : ∀ x → 0 · x ≡ 0
  ·-nullifiesˡ (pos n) = refl
  ·-nullifiesˡ (negsuc n) = refl

  ·-nullifiesʳ : ∀ x → x · 0 ≡ 0
  ·-nullifiesʳ x = ·-comm x 0 ∙ ·-nullifiesˡ x

  ·-identityˡ : ∀ x → 1 · x ≡ x
  ·-identityˡ (pos n) = λ i → pos $ +ⁿ-comm n 0 i
  ·-identityˡ (negsuc n) = refl

  ·-identityʳ : ∀ x → x · 1 ≡ x
  ·-identityʳ x = ·-comm x 1 ∙ ·-identityˡ x

abstract
  ·-preserves-< : (x y z : ℤ) → [ 0 < z ] → [ x < y ] → [ (x · z) < (y · z) ]
  ·-preserves-< (pos    x) (pos    y) (pos      z ) p q = ·ⁿ-preserves-<ⁿ x y z p q
  ·-preserves-< (negsuc x) (pos    y) (pos  zero  ) p q = subst (λ p → [ 0 <ⁿ p ]) (sym $ ·ⁿ-nullifiesʳ y) p
  ·-preserves-< (negsuc x) (pos    y) (pos (suc z)) p q = tt
  ·-preserves-< (negsuc x) (negsuc y) (pos  zero  ) p q = p
  ·-preserves-< (negsuc x) (negsuc y) (pos (suc z)) p q = (
       y                   <ⁿ  x                   ⇒ᵖ⟨ ·ⁿ-preserves-<ⁿ y x (suc z) (0<ⁿsuc z) ⟩
      (y ·ⁿ suc z        ) <ⁿ (x ·ⁿ suc z        ) ⇒ᵖ⟨ +ⁿ-createsʳ-<ⁿ (y ·ⁿ suc z) (x ·ⁿ suc z) z .fst ⟩
      (y ·ⁿ suc z +ⁿ z   ) <ⁿ (x ·ⁿ suc z +ⁿ z   ) ⇒ᵖ⟨ pathTo⇐ (λ i → lemma3 y z i <ⁿ lemma3 x z i) ⟩
      (y ·ⁿ z +ⁿ (y +ⁿ z)) <ⁿ (x ·ⁿ z +ⁿ (x +ⁿ z)) ◼ᵖ) .snd q

  ·-reflects-< : (x y z : ℤ) → [ 0 < z ] → [ (x · z) < (y · z) ] → [ x < y ]
  ·-reflects-< (pos    x) (pos    y) (pos      z ) p q = ·ⁿ-reflects-<ⁿ x y z p q
  ·-reflects-< (pos    x) (negsuc y) (pos  zero  ) p q = <ⁿ-irrefl 0 p
  ·-reflects-< (negsuc x) (pos    y) (pos  zero  ) p q = tt
  ·-reflects-< (negsuc x) (pos    y) (pos (suc z)) p q = tt
  ·-reflects-< (negsuc x) (negsuc y) (pos  zero  ) p (k , q) = ⊥-elim {A = λ _ → [ y <ⁿ x ]} $ snotzⁿ (sym (+ⁿ-suc k 0) ∙ q)
  ·-reflects-< (negsuc x) (negsuc y) (pos (suc z)) p q = (
    (y ·ⁿ z +ⁿ (y +ⁿ z)) <ⁿ (x ·ⁿ z +ⁿ (x +ⁿ z)) ⇒ᵖ⟨ pathTo⇒ (λ i → +ⁿ-assoc (y ·ⁿ z) y z i <ⁿ +ⁿ-assoc (x ·ⁿ z) x z i) ⟩
    ((y ·ⁿ z +ⁿ y) +ⁿ z) <ⁿ ((x ·ⁿ z +ⁿ x) +ⁿ z) ⇒ᵖ⟨ +ⁿ-createsʳ-<ⁿ (y ·ⁿ z +ⁿ y) (x ·ⁿ z +ⁿ x) z .snd ⟩
    (y ·ⁿ z +ⁿ y       ) <ⁿ (x ·ⁿ z +ⁿ x       ) ⇒ᵖ⟨ pathTo⇒ (λ i → γ y i <ⁿ γ x i) ⟩
    (y ·ⁿ suc z        ) <ⁿ (x ·ⁿ suc z        ) ⇒ᵖ⟨ ·ⁿ-reflects-<ⁿ y x (suc z) (0<ⁿsuc z) ⟩
     y                   <ⁿ  x                   ◼ᵖ) .snd q where
     γ : ∀ x → x ·ⁿ z +ⁿ x ≡ x ·ⁿ suc z
     γ x = sym $ ·ⁿ-comm x (suc z) ∙ +ⁿ-comm x (z ·ⁿ x) ∙ (λ i → ·ⁿ-comm z x i +ⁿ x)

abstract
  ·-sucInt : ∀ m n → (m · sucInt n) ≡ (m + (m · n))
  ·-sucInt (pos      a ) (pos      b ) = (λ i → pos (·ⁿ-suc a b i)) ∙ sym (pos+pos≡+ⁿ a (a ·ⁿ b))
  ·-sucInt (pos  zero  ) (negsuc   b ) = ·-nullifiesˡ _
  ·-sucInt (pos (suc a)) (negsuc zero) =
    pos (a ·ⁿ zero)                                  ≡⟨ (λ i → pos $ ·ⁿ-nullifiesʳ a i) ⟩
    pos 0                                            ≡⟨ sym $ +-inverse (pos (suc a)) .fst ⟩
    (pos (suc a) +negsuc                a          ) ≡⟨ refl ⟩
    (pos (suc a) +negsuc (     zero +ⁿ  a         )) ≡⟨ (λ i → pos (suc a) +negsuc (sym (·ⁿ-nullifiesʳ a) i +ⁿ +ⁿ-comm 0 a i)) ⟩
    (pos (suc a) +negsuc (a ·ⁿ zero +ⁿ (a +ⁿ zero))) ∎
  ·-sucInt (pos (suc a)) (negsuc (suc b)) =
    negsuc (a ·ⁿ b +ⁿ (a +ⁿ b))                          ≡⟨ sym $ +negsuc-identityˡ (a ·ⁿ b +ⁿ (a +ⁿ b)) ⟩
    0 +negsuc (a ·ⁿ b +ⁿ (a +ⁿ b))                       ≡⟨ (λ i → possuc+negsuc≡0 a (~ i) +negsuc (a ·ⁿ b +ⁿ (a +ⁿ b))) ⟩
    (pos (suc a) +negsuc a) +negsuc (a ·ⁿ b +ⁿ (a +ⁿ b)) ≡⟨ sym $ +negsuc-assoc (pos (suc a)) a (a ·ⁿ b +ⁿ (a +ⁿ b)) ⟩
    pos (suc a) +negsuc (a +ⁿ suc (a ·ⁿ b +ⁿ (a +ⁿ b)))  ≡⟨ (λ i → pos (suc a) +negsuc (lemma4 a b (~ i))) ⟩
    pos (suc a) +negsuc (a ·ⁿ suc b +ⁿ (a +ⁿ suc b))     ∎
  ·-sucInt (negsuc   a ) (pos  zero  ) = λ i → negsuc $ ·ⁿ-nullifiesʳ a i +ⁿ +ⁿ-comm a 0 i
  ·-sucInt (negsuc   a ) (pos (suc b)) =
    negsuc (a ·ⁿ suc b +ⁿ (a +ⁿ suc b))    ≡⟨ (λ i → negsuc $ lemma4 a b i) ⟩
    negsuc (a +ⁿ suc (a ·ⁿ b +ⁿ (a +ⁿ b))) ≡⟨ (λ i → negsuc $ +ⁿ-suc a (a ·ⁿ b +ⁿ (a +ⁿ b)) i) ∙ sym (negsuc+negsuc≡+ⁿ a (a ·ⁿ b +ⁿ (a +ⁿ b))) ⟩
    negsuc a +negsuc (a ·ⁿ b +ⁿ (a +ⁿ b))  ∎
  ·-sucInt (negsuc a) (negsuc zero) = sym (+-inverse (pos (suc a)) .snd) ∙ (λ i → sucInt (negsuc a +pos (·ⁿ-identityʳ a (~ i))))
  ·-sucInt (negsuc a) (negsuc (suc b)) =
    pos (suc (b +ⁿ a ·ⁿ suc b))                                ≡⟨ refl ⟩
    sucInt (pos (b +ⁿ a ·ⁿ suc b))                             ≡⟨ (λ i → sucInt $ sucInt[negsuc+pos]≡pos (b +ⁿ a ·ⁿ suc b) (~ i)) ⟩
    sucInt (sucInt (negsuc 0 +pos (b +ⁿ a ·ⁿ suc b)))          ≡⟨ (λ i → sucInt (sucInt (+pos-inverse a (~ i) +pos (b +ⁿ a ·ⁿ suc b)))) ⟩
    sucInt (sucInt ((negsuc a +pos a) +pos (b +ⁿ a ·ⁿ suc b))) ≡⟨ (λ i → sucInt $ sucInt $ +pos-assoc (negsuc a) a (b +ⁿ a ·ⁿ suc b) i) ⟩
    sucInt (sucInt (negsuc a +pos (a +ⁿ (b +ⁿ a ·ⁿ suc b))))   ≡⟨ (λ i → sucInt (sucInt (negsuc a +pos lemma5 a b i))) ⟩
    sucInt (sucInt (negsuc a +pos (b +ⁿ a ·ⁿ suc (suc b))))    ∎

abstract
  ·-sucIntˡ : ∀ m n → (sucInt m · n) ≡ (n + (m · n))
  ·-sucIntˡ m n = ·-comm (sucInt m) n ∙ ·-sucInt n m ∙ λ i → n + ·-comm n m i

  ·-predInt : ∀ m n → (m · predInt n) ≡ ((- m) + (m · n))
  ·-predInt m (pos zero) = ·-comm m (negsuc 0) ∙ -1·≡- m ∙ λ i → (- m) + ·-nullifiesʳ m (~ i)
  ·-predInt m (pos (suc n)) =
    m · pos n                 ≡⟨ +-comm (m · pos n) 0 ⟩
    0 + m · pos n             ≡⟨ (λ i → +-inverseˡ m (~ i) + (m · pos n)) ⟩
    ((- m) + m) + (m · pos n) ≡⟨ sym $ +-assoc (- m) m (m · pos n) ⟩
    (- m) + (m + (m · pos n)) ≡⟨ (λ i → (- m) + ·-sucInt m (pos n) (~ i)) ⟩
    (- m) + (m · pos (suc n)) ∎
  ·-predInt (pos zero) (negsuc zero) = refl
  ·-predInt (pos (suc n)) (negsuc zero) = (λ i → negsuc $ ·ⁿ-identityʳ n i +ⁿ +ⁿ-comm n 1 i) ∙ (λ i → negsuc $ +ⁿ-comm n (suc n) i) ∙ sym (negsuc+negsuc≡+ⁿ n n) ∙ (λ i → negsuc n +negsuc (·ⁿ-nullifiesʳ n (~ i) +ⁿ +ⁿ-comm 0 n i))
  ·-predInt (pos zero) (negsuc (suc m)) = refl
  ·-predInt (pos (suc n)) (negsuc (suc m)) =
    negsuc (n ·ⁿ suc (suc m) +ⁿ (n +ⁿ suc (suc m)))  ≡⟨ (λ i → negsuc $ ·ⁿ-suc n (suc m) i +ⁿ +ⁿ-suc n (suc m) i) ⟩
    negsuc ((n +ⁿ n ·ⁿ suc m) +ⁿ suc (n +ⁿ suc m))   ≡⟨ (λ i → negsuc $ +ⁿ-assoc n (n ·ⁿ suc m) (suc n +ⁿ suc m) (~ i)) ⟩
    negsuc (n +ⁿ (n ·ⁿ suc m +ⁿ suc (n +ⁿ suc m)))   ≡⟨ (λ i → negsuc $ n +ⁿ +ⁿ-suc (n ·ⁿ suc m) (n +ⁿ suc m) i) ⟩
    negsuc (n +ⁿ suc (n ·ⁿ suc m +ⁿ (n +ⁿ suc m)))   ≡⟨ (λ i → negsuc $ +ⁿ-suc n (n ·ⁿ suc m +ⁿ (n +ⁿ suc m)) i) ⟩
    negsuc (suc (n +ⁿ (n ·ⁿ suc m +ⁿ (n +ⁿ suc m)))) ≡⟨ sym $ negsuc+negsuc≡+ⁿ n (n ·ⁿ suc m +ⁿ (n +ⁿ suc m)) ⟩
    (negsuc n +negsuc (n ·ⁿ suc m +ⁿ (n +ⁿ suc m)))  ∎
  ·-predInt (negsuc n) (negsuc zero) = cong sucInt ((λ i → pos $ suc $ ·ⁿ-suc n 1 i) ∙ sym (pos+pos≡+ⁿ (suc n) (n ·ⁿ 1)))
  ·-predInt (negsuc n) (negsuc (suc m)) =
    pos (suc (suc (suc (m +ⁿ n ·ⁿ suc (suc (suc m))))))        ≡⟨ refl ⟩
    sucInt (sucInt (pos (suc (m +ⁿ n ·ⁿ suc (suc (suc m))))))  ≡⟨ (λ i → sucInt $ sucInt $ pos $ lemma6 m n i) ⟩
    sucInt (sucInt (pos (suc n +ⁿ (m +ⁿ n ·ⁿ suc (suc m)))))   ≡⟨ (λ i → sucInt $ sucInt $ pos+pos≡+ⁿ (suc n) (m +ⁿ n ·ⁿ suc (suc m)) (~ i)) ⟩
    sucInt (sucInt (pos (suc n) +pos (m +ⁿ n ·ⁿ suc (suc m)))) ∎

abstract
  ·-predIntˡ : ∀ m n → (predInt m · n) ≡ ((- n) + (m · n))
  ·-predIntˡ m n = ·-comm (predInt m) n ∙ ·-predInt n m ∙ λ i → (- n) + (·-comm n m i)

  -distrib : ∀ m n → -(m + n) ≡ (- m) + (- n)
  -distrib (pos zero) (pos zero) = refl
  -distrib (pos (suc n)) (pos zero) = refl
  -distrib (pos zero) (pos (suc m)) =
    - sucInt (pos zero +pos m) ≡⟨ (λ i → - sucInt (pos+pos≡+ⁿ 0 m i)) ⟩
    negsuc m                   ≡⟨ sym $ +negsuc-identityˡ m ⟩
    (pos zero +negsuc m)       ∎
  -distrib (pos (suc n)) (pos (suc m)) = (λ i → - sucInt (pos+pos≡+ⁿ (suc n) m i)) ∙ sym (negsuc+negsuc≡+ⁿ n m)
  -distrib (pos zero) (negsuc m) = (λ i → - +negsuc-identityˡ m i) ∙ sym (pos+pos≡+ⁿ 0 (suc m))
  -distrib (pos (suc n)) (negsuc m) = sym (pos+negsuc-swap m n) ∙ pos+negsuc≡negsuc+pos (suc m) n
  -distrib (negsuc n) (pos zero) = refl
  -distrib (negsuc n) (pos (suc m)) = (λ i → - pos+negsuc≡negsuc+pos (suc m) n (~ i)) ∙ sym (pos+negsuc-swap n m)
  -distrib (negsuc n) (negsuc m) = (λ i → - negsuc+negsuc≡+ⁿ n m i) ∙ (λ i → sucInt $ pos+pos≡+ⁿ (suc n) m (~ i))

abstract
  ·-distribˡ : ∀ o m n → (o · m) + (o · n) ≡ o · (m + n)
  ·-distribˡ (pos zero) m n = (λ i → ·-nullifiesˡ m i + ·-nullifiesˡ n i) ∙ (sym $ ·-nullifiesˡ (m + n))
  ·-distribˡ (pos (suc o)) m n = let
    ind = ·-distribˡ (pos o) m n
    lhs = (pos (suc o) · m) + (pos (suc o) · n)  ≡⟨ (λ i → ·-sucIntˡ (pos o) m i + ·-sucIntˡ (pos o) n i) ⟩
          (m + (pos o · m)) + (n + (pos o · n))  ≡⟨ sym $ +-assoc m (pos o · m) (n + (pos o · n)) ⟩
           m + ((pos o · m) + (n + (pos o · n))) ≡⟨ (λ i → m + +-comm (pos o · m) (n + (pos o · n)) i) ⟩
           m + ((n + (pos o · n)) + (pos o · m)) ≡⟨ (λ i → m + +-assoc n (pos o · n) (pos o · m) (~ i)) ⟩
           m + (n + ((pos o · n) + (pos o · m))) ≡⟨ (λ i → +-assoc m n (+-comm (pos o · n) (pos o · m) i) i) ⟩
          (m + n) + ((pos o · m) + (pos o · n))  ≡⟨ (λ i → (m + n) + ind i) ⟩
          (m + n) + (pos o · (m + n))            ∎
    rhs = (pos (suc o) · (m + n))       ≡⟨ refl ⟩
          (sucInt (pos o) · (m + n))    ≡⟨ ·-sucIntˡ (pos o) (m + n) ⟩
          ((m + n) + (pos o · (m + n))) ∎
    in lhs ∙ sym rhs
  ·-distribˡ (negsuc zero) (pos zero) (pos zero) = refl
  ·-distribˡ (negsuc zero) (pos zero) (pos (suc n)) = +negsuc-identityˡ n ∙ λ i → negsuc 0 · sucInt (pos+pos≡+ⁿ 0 n (~ i))
  ·-distribˡ (negsuc zero) (pos (suc m)) (pos zero) = refl
  ·-distribˡ (negsuc zero) (pos (suc m)) (pos (suc n)) = negsuc+negsuc≡+ⁿ m n ∙ λ i → negsuc 0 · sucInt (pos+pos≡+ⁿ (suc m) n (~ i))
  ·-distribˡ (negsuc zero) (pos zero) (negsuc n) = (λ i → sucInt $ pos+pos≡+ⁿ 0 (n +ⁿ 0) i) ∙ (λ i → negsuc 0 · +negsuc-identityˡ n (~ i))
  ·-distribˡ (negsuc zero) (pos (suc m)) (negsuc n) =
    sucInt (negsuc m +pos (n +ⁿ zero))           ≡⟨ (λ i → sucInt $ negsuc m +pos +ⁿ-comm n 0 i) ⟩
    sucInt (negsuc m +pos n)                     ≡⟨ refl ⟩
    negsuc m +pos (suc n)                        ≡⟨ negsuc+pos-swap m n ⟩
    - (negsuc n +pos (suc m))                    ≡⟨ (λ i → - pos+negsuc≡negsuc+pos (suc m) n (~ i)) ⟩
    - (pos (suc m) +negsuc n)                    ≡⟨ sym $ -1·≡- (pos (suc m) +negsuc n) ⟩
    negsuc zero · (pos (suc m) +negsuc n)        ∎
  ·-distribˡ (negsuc zero) (negsuc m) (pos zero) = refl
  ·-distribˡ (negsuc zero) (negsuc m) (pos (suc n)) =
    pos (suc (m +ⁿ zero)) +negsuc n        ≡⟨ (λ i → pos (suc (+ⁿ-comm m 0 i)) +negsuc n) ⟩
    pos (suc m) +negsuc n                  ≡⟨ pos+negsuc≡negsuc+pos (suc m) n ⟩
    sucInt (negsuc n +pos m)               ≡⟨ negsuc+pos-swap n m ⟩
    - negsuc m +pos (suc n)                ≡⟨ refl ⟩
    - sucInt (negsuc m +pos n)             ≡⟨ sym $ -1·≡- (sucInt (negsuc m +pos n)) ⟩
    negsuc zero · sucInt (negsuc m +pos n) ∎
  ·-distribˡ (negsuc zero) (negsuc m) (negsuc n) =
    sucInt (pos (suc (m +ⁿ zero)) +pos (n +ⁿ zero)) ≡⟨ (λ i → sucInt (pos (suc (+ⁿ-comm m 0 i)) +pos (+ⁿ-comm n 0 i))) ⟩
    sucInt (pos (suc m) +pos (n))                   ≡⟨ (λ i → sucInt $ pos+pos≡+ⁿ (suc m) n i) ⟩
    sucInt (pos (suc m +ⁿ n))                       ≡⟨ refl ⟩
    pos (suc (suc (m +ⁿ n)))                        ≡⟨ (λ i → pos $ suc $ suc $ +ⁿ-comm 0 (m +ⁿ n) i) ⟩
    negsuc zero · (negsuc (suc (m +ⁿ n)))           ≡⟨ (λ i → negsuc zero · negsuc+negsuc≡+ⁿ m n (~ i)) ⟩
    negsuc zero · (negsuc m +negsuc n)              ∎
  ·-distribˡ (negsuc (suc o)) m n = let
    r = ·-distribˡ (negsuc o) m n
    lhs = (negsuc (suc o) · m) + (negsuc (suc o) · n)          ≡⟨ (λ i → ·-predIntˡ (negsuc o) m i + ·-predIntˡ (negsuc o) n i) ⟩
          ((- m) + (negsuc o · m)) + ((- n) + (negsuc o · n))  ≡⟨ sym $ +-assoc (- m)  (negsuc o · m) ((- n) + (negsuc o · n)) ⟩
           (- m) + ((negsuc o · m) + ((- n) + (negsuc o · n))) ≡⟨ (λ i → (- m) + +-comm (negsuc o · m) ((- n) + (negsuc o · n)) i) ⟩
           (- m) + (((- n) + (negsuc o · n)) + (negsuc o · m)) ≡⟨ (λ i → (- m) + +-assoc (- n) (negsuc o · n) (negsuc o · m) (~ i)) ⟩
           (- m) + ((- n) + ((negsuc o · n) + (negsuc o · m))) ≡⟨ (λ i → +-assoc (- m) (- n) (+-comm (negsuc o · n) (negsuc o · m) i) i) ⟩
          ((- m) + (- n)) + ((negsuc o · m) + (negsuc o · n))  ≡⟨ (λ i → ((- m) + (- n)) + r i) ⟩
          ((- m) + (- n)) + (negsuc o · (m + n))            ∎
    rhs = negsuc (suc o) · (m + n)               ≡⟨ ·-predIntˡ (negsuc o) (m + n) ⟩
          (- (m + n)) + negsuc (o) · (m + n)     ≡⟨ (λ i → -distrib m n i + negsuc (o) · (m + n)) ⟩
          ((- m) + (- n)) + (negsuc (o) · (m + n)) ∎
    in lhs ∙ sym rhs

abstract
  ·-distribʳ : ∀ m n o → (m · o) + (n · o) ≡ (m + n) · o
  ·-distribʳ m n o = transport (sym λ i → ·-comm m o i + ·-comm n o i ≡ ·-comm (m + n) o i) $ ·-distribˡ o m n

+-Semigroup : [ isSemigroup _+_ ]
+-Semigroup .IsSemigroup.is-set   = isSetℤ
+-Semigroup .IsSemigroup.is-assoc = +-assoc

·-Semigroup : [ isSemigroup _·_ ]
·-Semigroup .IsSemigroup.is-set   = isSetℤ
·-Semigroup .IsSemigroup.is-assoc x y z = sym (·-assoc x y z)

+-Monoid : [ isMonoid 0 _+_ ]
+-Monoid .IsMonoid.is-Semigroup = +-Semigroup
+-Monoid .IsMonoid.is-identity x = +-identityʳ x , +-identityˡ x

·-Monoid : [ isMonoid 1 _·_ ]
·-Monoid .IsMonoid.is-Semigroup = ·-Semigroup
·-Monoid .IsMonoid.is-identity x = ·-identityʳ x , ·-identityˡ x

is-Semiring : [ isSemiring 0 1 _+_ _·_ ]
is-Semiring .IsSemiring.+-Monoid = +-Monoid
is-Semiring .IsSemiring.·-Monoid = ·-Monoid
is-Semiring .IsSemiring.+-comm   = +-comm
is-Semiring .IsSemiring.is-dist x y z = sym (·-distribˡ x y z) , sym (·-distribʳ x y z)

is-CommSemiring : [ isCommSemiring 0 1 _+_ _·_ ]
is-CommSemiring .IsCommSemiring.is-Semiring = is-Semiring
is-CommSemiring .IsCommSemiring.·-comm      = ·-comm

<-StrictLinearOrder : [ isStrictLinearOrder _<_ ]
<-StrictLinearOrder .IsStrictLinearOrder.is-irrefl = <-irrefl
<-StrictLinearOrder .IsStrictLinearOrder.is-trans  a b c = <-trans a b c
<-StrictLinearOrder .IsStrictLinearOrder.is-tricho a b with a ≟ b
... | lt a<b = inl (inl a<b)
... | eq a≡b = inr ∣ a≡b ∣
... | gt b<a = inl (inr b<a)

≤-Lattice : [ isLattice (λ x y → ¬ᵖ (y < x)) min max ]
≤-Lattice .IsLattice.≤-PartialOrder = linearorder⇒partialorder _ (≤'-isLinearOrder <-StrictLinearOrder)
≤-Lattice .IsLattice.is-min         = is-min
≤-Lattice .IsLattice.is-max         = is-max

is-LinearlyOrderedCommSemiring : [ isLinearlyOrderedCommSemiring 0 1 _+_ _·_ _<_ min max ]
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.is-CommSemiring     = is-CommSemiring
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.<-StrictLinearOrder = <-StrictLinearOrder
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.≤-Lattice           = ≤-Lattice
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.+-<-ext             = +-<-ext
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.·-preserves-<       = ·-preserves-<

is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0 1 _+_ _·_ -_ _<_ min max ]
is-LinearlyOrderedCommRing .IsLinearlyOrderedCommRing.is-LinearlyOrderedCommSemiring = is-LinearlyOrderedCommSemiring
is-LinearlyOrderedCommRing .IsLinearlyOrderedCommRing.+-inverse                      = +-inverse

ℤbundle : LinearlyOrderedCommRing {ℓ-zero} {ℓ-zero}
ℤbundle .LinearlyOrderedCommRing.Carrier                    = ℤ
ℤbundle .LinearlyOrderedCommRing.0f                         = 0
ℤbundle .LinearlyOrderedCommRing.1f                         = 1
ℤbundle .LinearlyOrderedCommRing._+_                        = _+_
ℤbundle .LinearlyOrderedCommRing._·_                        = _·_
ℤbundle .LinearlyOrderedCommRing.-_                         = -_
ℤbundle .LinearlyOrderedCommRing.min                        = min
ℤbundle .LinearlyOrderedCommRing.max                        = max
ℤbundle .LinearlyOrderedCommRing._<_                        = _<_
ℤbundle .LinearlyOrderedCommRing.is-LinearlyOrderedCommRing = is-LinearlyOrderedCommRing

-- ·-reflects-≡ˡ : ∀ a b x → (pos (suc x)) ·' a ≡ (pos (suc x)) ·' b → a ≡ b
-- ·-reflects-≡ˡ a b x p = {!   !}

-- private
--   ¬0≡suc
--   ¬0≡possuc
--   ¬0≡negsuc
--   ¬pos≡negsuc
--
-- ·-reflects-≡ʳ : ∀ a b x → a · (pos (suc x)) ≡ b · (pos (suc x)) → a ≡ b
-- ·-reflects-≡ʳ (pos      0 ) (pos      0 ) x q = refl
-- ·-reflects-≡ʳ (pos      0 ) (pos (suc b)) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (pos (suc a)) (pos      0 ) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (pos (suc a)) (pos (suc b)) x q i = sucInt $ ·-reflects-≡ʳ (pos a) (pos b) x {!   !} i
-- ·-reflects-≡ʳ (pos      0 ) (negsuc   b ) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (pos (suc a)) (negsuc   b ) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (negsuc   a ) (pos      0 ) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (negsuc   a ) (pos (suc b)) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (negsuc zero) (negsuc zero) x q = refl
-- ·-reflects-≡ʳ (negsuc zero) (negsuc (suc b)) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (negsuc (suc a)) (negsuc zero) x q = {! ⊥  !}
-- ·-reflects-≡ʳ (negsuc (suc a)) (negsuc (suc b)) x q i = predInt $ ·-reflects-≡ʳ (negsuc a) (negsuc b) x {!   !} i

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --without-K #-}
module higher.circle where

open import higher.circle.core public
open import higher.circle.properties public

ext: agda

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Instances.Unit where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure

open import Cubical.Data.Unit
open import Cubical.Data.Sigma.Properties using (Σ≡Prop)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommRing.Instances.Unit
open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom)
open import Cubical.Algebra.CommRingSolver.Reflection

private
  variable
    ℓ ℓ' : Level

module _ (R : CommRing ℓ) where
  UnitCommAlgebra : CommAlgebra R ℓ'
  UnitCommAlgebra =
    commAlgebraFromCommRing
      UnitCommRing
      (λ _ _ → tt*) (λ _ _ _ → refl) (λ _ _ _ → refl)
      (λ _ _ _ → refl) (λ _ → refl) (λ _ _ _ → refl)

  module _ (A : CommAlgebra R ℓ) where
    terminalMap : CommAlgebraHom A (UnitCommAlgebra {ℓ' = ℓ})
    terminalMap = (λ _ → tt*) , isHom
      where open IsAlgebraHom
            isHom : IsCommAlgebraHom (snd A) _ (snd UnitCommAlgebra)
            pres0 isHom = isPropUnit* _ _
            pres1 isHom = isPropUnit* _ _
            pres+ isHom = λ _ _ → isPropUnit* _ _
            pres· isHom = λ _ _ → isPropUnit* _ _
            pres- isHom = λ _ → isPropUnit* _ _
            pres⋆ isHom = λ _ _ → isPropUnit* _ _

    terminalityContr : isContr (CommAlgebraHom A UnitCommAlgebra)
    terminalityContr = terminalMap , path
      where path : (ϕ : CommAlgebraHom A UnitCommAlgebra) → terminalMap ≡ ϕ
            path ϕ = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = UnitCommAlgebra})
                            λ i _ → isPropUnit* _ _ i

    open CommAlgebraStr (snd A)
    module _ (1≡0 : 1a ≡ 0a) where

      1≡0→isContr : isContr ⟨ A ⟩
      1≡0→isContr = 0a , λ a →
        0a      ≡⟨ step1 a ⟩
        a · 0a  ≡⟨ cong (λ b → a · b) (sym 1≡0) ⟩
        a · 1a  ≡⟨ step2 a ⟩
        a       ∎
          where S = CommAlgebra→CommRing A
                open CommRingStr (snd S) renaming (_·_ to _·s_)
                step1 : (x : ⟨ A ⟩) → 0r ≡ x ·s 0r
                step1 = solve S
                step2 : (x : ⟨ A ⟩) → x ·s 1r ≡ x
                step2 = solve S

      equivFrom1≡0 : CommAlgebraEquiv A UnitCommAlgebra
      equivFrom1≡0 = isContr→Equiv 1≡0→isContr isContrUnit*  ,
                     snd terminalMap

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Qualified mixfix operators
module Issue597 where

open import Common.Prelude as Prel hiding (if_then_else_)
open import Common.Level using (lzero)

lz = lzero Common.Level.⊔ lzero

module A where

  data _×_ (A B : Set) : Set where
    _,_ : A → B → A × B

  if_then_else_ : ∀ {A : Set} → Bool → A → A → A
  if true  then x else y = x
  if false then x else y = y

  pattern _+2 n = suc (suc n)

  module B where

    _₁ : ∀ {A B} → A × B → A
    (x , y)₁ = x

    _₂ : ∀ {A B} → A × B → B
    (x , y)₂ = y

    syntax Exist (λ x → p) = ∃ x ∶ p
    data Exist {A : Set}(P : A → Set) : Set where
      _,_ : (x : A) → P x → Exist P

pp : Nat → Nat
pp 0 = 0
pp 1 = 0
pp (n A.+2) = n

infix 5 add_
add_ : Nat A.× Nat → Nat
add_ p = p A.B.₁ Prel.+ p A.B.₂

six : Nat
six = add 1 A., 5

two : Nat
two = A.if true then 2 else 4

data Even : Nat → Set where
  ez  : Even 0
  ess : ∀ n → Even n → Even (suc (suc n))

pair : A.B.∃ n ∶ Even n
pair = 2 A.B., ess zero ez

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Group.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Structures.Monoid hiding (⟨_⟩)

private
  variable
    ℓ : Level

record IsGroup {G : Type ℓ}
               (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where

  constructor isgroup

  field
    isMonoid  : IsMonoid 0g _+_
    inverse   : (x : G) → (x + (- x) ≡ 0g) × ((- x) + x ≡ 0g)

  open IsMonoid isMonoid public

  infixl 6 _-_

  _-_ : G → G → G
  x - y = x + (- y)

  invl : (x : G) → (- x) + x ≡ 0g
  invl x = inverse x .snd

  invr : (x : G) → x + (- x) ≡ 0g
  invr x = inverse x .fst

record Group : Type (ℓ-suc ℓ) where

  constructor group

  field
    Carrier : Type ℓ
    0g      : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    isGroup : IsGroup 0g _+_ -_

  infix  8 -_
  infixr 7 _+_

  open IsGroup isGroup public

-- Extractor for the carrier type
⟨_⟩ : Group → Type ℓ
⟨_⟩ = Group.Carrier

makeIsGroup : {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
              (is-setG : isSet G)
              (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
              (rid : (x : G) → x + 0g ≡ x)
              (lid : (x : G) → 0g + x ≡ x)
              (rinv : (x : G) → x + (- x) ≡ 0g)
              (linv : (x : G) → (- x) + x ≡ 0g)
            → IsGroup 0g _+_ -_
makeIsGroup is-setG assoc rid lid rinv linv =
   isgroup (makeIsMonoid is-setG assoc rid lid) λ x → rinv x , linv x

makeGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
            (is-setG : isSet G)
            (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
            (rid : (x : G) → x + 0g ≡ x)
            (lid : (x : G) → 0g + x ≡ x)
            (rinv : (x : G) → x + (- x) ≡ 0g)
            (linv : (x : G) → (- x) + x ≡ 0g)
          → Group
makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv =
  group _ 0g _+_ -_ (makeIsGroup is-setG assoc rid lid rinv linv)

makeGroup-right : ∀ {ℓ} {A : Type ℓ}
  → (id : A)
  → (comp : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → comp a (comp b c) ≡ comp (comp a b) c)
  → (rUnit : ∀ a → comp a id ≡ a)
  → (rCancel : ∀ a → comp a (inv a) ≡ id)
  → Group
makeGroup-right {A = A} id comp inv set assoc rUnit rCancel =
  makeGroup id comp inv set assoc rUnit lUnit rCancel lCancel
  where
    _⨀_ = comp
    abstract
      lCancel : ∀ a → comp (inv a) a ≡ id
      lCancel a =
        inv a ⨀ a
          ≡⟨ sym (rUnit (comp (inv a) a))  ⟩
        (inv a ⨀ a) ⨀ id
          ≡⟨ cong (comp (comp (inv a) a)) (sym (rCancel (inv a))) ⟩
        (inv a ⨀ a) ⨀ (inv a ⨀ (inv (inv a)))
          ≡⟨ assoc _ _ _ ⟩
        ((inv a ⨀ a) ⨀ (inv a)) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → □ ⨀ _) (sym (assoc _ _ _)) ⟩
        (inv a ⨀ (a ⨀ inv a)) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → (inv a ⨀ □) ⨀ (inv (inv a))) (rCancel a) ⟩
        (inv a ⨀ id) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → □ ⨀ (inv (inv a))) (rUnit (inv a)) ⟩
        inv a ⨀ (inv (inv a))
          ≡⟨ rCancel (inv a) ⟩
        id
          ∎

      lUnit : ∀ a → comp id a ≡ a
      lUnit a =
        id ⨀ a
          ≡⟨ cong (λ b → comp b a) (sym (rCancel a)) ⟩
        (a ⨀ inv a) ⨀ a
          ≡⟨ sym (assoc _ _ _) ⟩
        a ⨀ (inv a ⨀ a)
          ≡⟨ cong (comp a) (lCancel a) ⟩
        a ⨀ id
          ≡⟨ rUnit a ⟩
        a
          ∎

makeGroup-left : ∀ {ℓ} {A : Type ℓ}
  → (id : A)
  → (comp : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → comp a (comp b c) ≡ comp (comp a b) c)
  → (lUnit : ∀ a → comp id a ≡ a)
  → (lCancel : ∀ a → comp (inv a) a ≡ id)
  → Group
makeGroup-left {A = A} id comp inv set assoc lUnit lCancel =
  makeGroup id comp inv set assoc rUnit lUnit rCancel lCancel
  where
    abstract
      rCancel : ∀ a → comp a (inv a) ≡ id
      rCancel a =
        comp a (inv a)
          ≡⟨ sym (lUnit (comp a (inv a)))  ⟩
        comp id (comp a (inv a))
          ≡⟨ cong (λ b → comp b (comp a (inv a))) (sym (lCancel (inv a))) ⟩
        comp (comp (inv (inv a)) (inv a)) (comp a (inv a))
          ≡⟨ sym (assoc (inv (inv a)) (inv a) (comp a (inv a))) ⟩
        comp (inv (inv a)) (comp (inv a) (comp a (inv a)))
          ≡⟨ cong (comp (inv (inv a))) (assoc (inv a) a (inv a)) ⟩
        comp (inv (inv a)) (comp (comp (inv a) a) (inv a))
          ≡⟨ cong (λ b → comp (inv (inv a)) (comp b (inv a))) (lCancel a) ⟩
        comp (inv (inv a)) (comp id (inv a))
          ≡⟨ cong (comp (inv (inv a))) (lUnit (inv a)) ⟩
        comp (inv (inv a)) (inv a)
          ≡⟨ lCancel (inv a) ⟩
        id
          ∎

      rUnit : ∀ a → comp a id ≡ a
      rUnit a =
        comp a id
          ≡⟨ cong (comp a) (sym (lCancel a)) ⟩
        comp a (comp (inv a) a)
          ≡⟨ assoc a (inv a) a ⟩
        comp (comp a (inv a)) a
          ≡⟨ cong (λ b → comp b a) (rCancel a) ⟩
        comp id a
          ≡⟨ lUnit a ⟩
        a
          ∎

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Data.Maybe where

data Maybe (a : Set) : Set where
  nothing : Maybe a
  just    : a -> Maybe a

fmap : {A B : Set} -> (A -> B) -> Maybe A -> Maybe B
fmap f nothing  = nothing
fmap f (just a) = just (f a )

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module imper-repeat where

open import lib
open import eq-reasoning

data Singleton {a} {A : Set a} (x : A) : Set a where
  _with≡_ : (y : A) → x ≡ y → Singleton x

inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
inspect x = x with≡ refl

-- Unicode notes. I use:
--   \Mix, \Mie, \MiF etc for meta-variables 𝑥, 𝑒, 𝐹 etc.
--   \mapsto for variable frame bindings and update.
--   \| for the frame update operation.
--   \|- turnstile ⊢ is used for the semantics relations.
--   (\|-n for its negation ⊬)
--   \d= for code literal values e.g. ⇓ 42 and ⇓true
--   The down arrow is also used for the eval relation.
--   \u= for code variable lookups like ⇑ "x" and ⇑ "y"
--   superscripts of items with \^e as ᵉ, \c^c as ᶜ
--   ↩ for sequencing. This is \lefthookarrow.
--   ∷= which is \:: followed by =

--
-- variable identifiers
--
Id : Set
Id = string

_=Id_ : Id → Id → 𝔹
_=Id_ = _=string_

--
-- values (just natural numbers here)
--
Val : Set
Val = ℕ

--
-- value and variable expressions
--
data Expn : Set where
  ⇓_ : Val → Expn
  ⇑_ : Id → Expn
  _+ᵉ_ : Expn → Expn → Expn
  _-ᵉ_ : Expn → Expn → Expn
  _*ᵉ⇓_ : Expn → Val → Expn

--
-- conditions on values and variables
--
data Cond : Set where
  ⇓true : Cond
  ⇓false : Cond
  _∧ᶜ_ : Cond → Cond → Cond
  _∨ᶜ_ : Cond → Cond → Cond
  ¬ᶜ_ : Cond → Cond
  [_<ᶜ_] : Expn → Expn → Cond
  [_=ᶜ_] : Expn → Expn → Cond

--
-- stack frames containing variable bindings
--
Frm : Set
Frm = 𝕃 (Id × Val)

[_↦_] : Id → Val → Frm
[ 𝑥 ↦ 𝑣 ] = [(𝑥 , 𝑣)]

[-↦0] : Frm
[-↦0] = []

--
-- program statements that transform a frame
--
data Stmt : Set where
  skip : Stmt
  _∷=_ : Id → Expn → Stmt
  _↩_ : Stmt → Stmt → Stmt
  if_then_else_end : Cond → Stmt → Stmt → Stmt
  by_repeat_end : Id → Stmt → Stmt
  returns_ : Expn → Stmt

infix 10 ⇑_ ⇓_
infix 9 _*ᵉ⇓_
infixl 8 _+ᵉ_ _-ᵉ_
infix 7 ¬ᶜ_
infixl 6 _∨ᶜ_
infixl 5 _∧ᶜ_
infix 4 _∷=_
infix 3 returns_
infixl 2 _↩_

--
-- functional SEMANTICS of frames
--

_∥_ : Frm → Id → Val
[] ∥ 𝑥 = 0
((𝑦 , 𝑤) :: 𝐹) ∥ 𝑥  = if (𝑥 =Id 𝑦) then 𝑤 else (𝐹 ∥ 𝑥)

_∣_↦_ : Frm → Id → Val → Frm
[] ∣ 𝑥 ↦ 𝑣 = [ 𝑥 ↦ 𝑣 ]
((𝑦 , 𝑤) :: 𝐹) ∣ 𝑥 ↦ 𝑣
          = if (𝑥 =Id 𝑦)
              then (𝑦 , 𝑣) :: 𝐹
              else (𝑦 , 𝑤) :: (𝐹 ∣ 𝑥 ↦ 𝑣)

--
-- functional SEMANTICS of expressions
--
⟦_⟧ᵉ_ : Expn → Frm → Val
⟦ ⇓ 𝑣 ⟧ᵉ _ = 𝑣
⟦ ⇑ 𝑥 ⟧ᵉ 𝐹 = 𝐹 ∥ 𝑥
⟦ 𝑒₁ +ᵉ 𝑒₂ ⟧ᵉ 𝐹 = (⟦ 𝑒₁ ⟧ᵉ 𝐹) + (⟦ 𝑒₂ ⟧ᵉ 𝐹)
⟦ 𝑒₁ -ᵉ 𝑒₂ ⟧ᵉ 𝐹 = (⟦ 𝑒₁ ⟧ᵉ 𝐹) ∸ (⟦ 𝑒₂ ⟧ᵉ 𝐹)
⟦ 𝑒₁ *ᵉ⇓ 𝑣₂ ⟧ᵉ 𝐹 = (⟦ 𝑒₁ ⟧ᵉ 𝐹) * 𝑣₂

--
-- functional SEMANTICS of conditions
--
⟦_⟧ᶜ_ : Cond → Frm → 𝔹
⟦ ⇓true ⟧ᶜ _ = tt
⟦ ⇓false ⟧ᶜ _ = ff
⟦ 𝒸₁ ∧ᶜ 𝒸₂ ⟧ᶜ 𝐹 = (⟦ 𝒸₁ ⟧ᶜ 𝐹) && (⟦ 𝒸₂ ⟧ᶜ 𝐹)
⟦ 𝒸₁ ∨ᶜ 𝒸₂ ⟧ᶜ 𝐹 = (⟦ 𝒸₁ ⟧ᶜ 𝐹) || (⟦ 𝒸₂ ⟧ᶜ 𝐹)
⟦ ¬ᶜ 𝒸 ⟧ᶜ 𝐹 = ~ (⟦ 𝒸 ⟧ᶜ 𝐹)
⟦ [ 𝑒₁ <ᶜ 𝑒₂ ] ⟧ᶜ 𝐹 = (⟦ 𝑒₁ ⟧ᵉ 𝐹) < (⟦ 𝑒₂ ⟧ᵉ 𝐹)
⟦ [ 𝑒₁ =ᶜ 𝑒₂ ] ⟧ᶜ 𝐹 = (⟦ 𝑒₁ ⟧ᵉ 𝐹) =ℕ (⟦ 𝑒₂ ⟧ᵉ 𝐹)

--
-- functional SEMANTICS of program execution
--
⟦_∣_∷=_…0⟧ˢ_ : Stmt → Id → ℕ → Frm → Frm
⟦_⟧ˢ_ : Stmt → Frm → Frm
⟦ 𝑠 ∣ 𝑥 ∷= 0 …0⟧ˢ 𝐹 = 𝐹
⟦ 𝑠 ∣ 𝑥 ∷= (suc 𝑛) …0⟧ˢ 𝐹
                  = ⟦ 𝑠 ∣ 𝑥 ∷= 𝑛 …0⟧ˢ ((⟦ 𝑠 ⟧ˢ 𝐹) ∣ 𝑥 ↦ 𝑛)
⟦ skip ⟧ˢ 𝐹 = 𝐹
⟦ 𝑥 ∷= 𝑒 ⟧ˢ 𝐹 = (𝐹 ∣ 𝑥 ↦ (⟦ 𝑒 ⟧ᵉ 𝐹))
⟦ 𝑠₁ ↩ 𝑠₂ ⟧ˢ 𝐹 = (⟦ 𝑠₂ ⟧ˢ (⟦ 𝑠₁ ⟧ˢ 𝐹))
⟦ if 𝒸 then 𝑠₁ else 𝑠₂ end ⟧ˢ 𝐹 = if (⟦ 𝒸 ⟧ᶜ 𝐹) then (⟦ 𝑠₁ ⟧ˢ 𝐹) else (⟦ 𝑠₂ ⟧ˢ 𝐹)
⟦ by 𝑥 repeat 𝑠 end ⟧ˢ 𝐹 = ⟦ 𝑠 ∣ 𝑥 ∷= (⟦ ⇑ 𝑥 ⟧ᵉ 𝐹) …0⟧ˢ 𝐹
⟦ returns 𝑒 ⟧ˢ 𝐹 = 𝐹 ∣ "retval" ↦ (⟦ 𝑒 ⟧ᵉ 𝐹)

--
-- SEMANTICS of stack bindings as a relation
--
infixl 7 _⊢ᶠ_↦_
infixl 5 _∣_↦_
infixl 4 _⊢ᵉ_⇓_
infixl 3 _⊢ᶜ_ _⊬ᶜ_ -- _↦_

data _⊢ᶠ_↦_ : Frm → Id → Val → Set where

  var-undef : ∀ {𝑥 : Id}
              ----------------
              → [] ⊢ᶠ 𝑥 ↦ 0

  var-match : ∀ {𝑥 𝑦 : Id} {𝐹 : Frm} {𝑤 : Val}
              → (𝑥 =string 𝑦) ≡ tt
              ---------------------------
              → ((𝑦 , 𝑤) :: 𝐹) ⊢ᶠ 𝑥 ↦ 𝑤

  var-mismatch : ∀ {𝑥 𝑦 : Id} {𝐹 : Frm} {𝑣 𝑤 : Val}
                 → (𝑥 =string 𝑦) ≡ ff
                 → 𝐹 ⊢ᶠ 𝑥 ↦ 𝑣
                 -------------------------
                 → ((𝑦 , 𝑤) :: 𝐹) ⊢ᶠ 𝑥 ↦ 𝑣

if-tt-then : ∀{A : Set} {b : 𝔹} {a1 a2 : A}
    → b ≡ tt → if b then a1 else a2 ≡ a1
if-tt-then{A}{b}{a1}{a2} b≡tt =
  begin
    if b then a1 else a2
  ≡⟨ cong3 if_then_else_ b≡tt refl refl ⟩
    if tt then a1 else a2
  ≡⟨ refl ⟩
    a1
  ∎

postulate
  if-ff-then : ∀{A : Set}{b : 𝔹}{a1 a2 : A}
    → b ≡ ff → if b then a1 else a2 ≡ a2

var-thm-fwd : ∀{x : Id}{F : Frm}{v : Val}
  → F ⊢ᶠ x ↦ v → F ∥ x ≡ v
var-thm-fwd{x}{[]}{0} var-undef =
  begin
    [] ∥ x
  ≡⟨ refl ⟩
    0
  ∎
var-thm-fwd (var-match{x}{y}{F}{w} x≡y) =
  begin
    ((y , w) :: F) ∥ x
  ≡⟨ refl ⟩
    if (x =Id y) then w else (F ∥ x)
  ≡⟨ if-tt-then x≡y ⟩
    w
  ∎
var-thm-fwd (var-mismatch{x}{y}{F}{v}{w} x≢y x↦v) =
  let
    F∥x≡v : F ∥ x ≡ v
    F∥x≡v = var-thm-fwd x↦v
  in begin
    ((y , w) :: F) ∥ x
  ≡⟨ refl ⟩
    if (x =Id y) then w else (F ∥ x)
  ≡⟨ if-ff-then x≢y ⟩
    F ∥ x
  ≡⟨ F∥x≡v ⟩
    v
  ∎

var-thm-rev : ∀{x : Id}{F : Frm}{v : Val}
  → F ∥ x ≡ v → F ⊢ᶠ x ↦ v
var-thm-rev{x}{[]}{v} []∥x≡v =
  let v≡0 : v ≡ 0
      v≡0 = begin
             v
            ≡⟨ sym []∥x≡v ⟩
             [] ∥ x
            ≡⟨ refl ⟩
             0
            ∎
   in cong-pred (λ xxx → [] ⊢ᶠ x ↦ xxx) (sym v≡0) var-undef
var-thm-rev{x}{(y , w) :: F}{v} y,w::F∥x≡v
 with inspect (x =string y)
... | tt with≡ same =
          let v≡w : v ≡ w
              v≡w = begin
                      v
                    ≡⟨ sym y,w::F∥x≡v ⟩
                      ((y , w) :: F) ∥ x
                    ≡⟨ refl ⟩
                      if x =string y then w else F ∥ x
                    ≡⟨ cong3 if_then_else_ same refl refl ⟩
                      if tt then w else F ∥ x
                    ≡⟨ refl ⟩
                      w
                    ∎
           in cong-pred (λ xxx → ((y , w) :: F) ⊢ᶠ x ↦ xxx) (sym v≡w) (var-match same)
... | ff with≡ diff =
          let v≡F∥x : v ≡ F ∥ x
              v≡F∥x = begin
                      v
                    ≡⟨ sym y,w::F∥x≡v ⟩
                      ((y , w) :: F) ∥ x
                    ≡⟨ refl ⟩
                      if x =string y then w else F ∥ x
                    ≡⟨ cong3 if_then_else_ diff refl refl ⟩
                      if ff then w else F ∥ x
                    ≡⟨ refl ⟩
                      F ∥ x
                    ∎
           in (var-mismatch diff (var-thm-rev (sym v≡F∥x)))

--
-- SEMANTICS of expression evaluation as a relation
--

data _⊢ᵉ_⇓_ : Frm → Expn → Val → Set where

  e-val : ∀ {𝑣 : Val} {𝐹 : Frm}
            ----------------
            → 𝐹 ⊢ᵉ (⇓ 𝑣) ⇓ 𝑣

  e-var : ∀ {𝑥 : Id} {𝐹 : Frm} {𝑣 : Val}
          → 𝐹 ⊢ᶠ 𝑥 ↦ 𝑣
          ---------------
          → 𝐹 ⊢ᵉ (⇑ 𝑥) ⇓ 𝑣

  e-add : ∀ {𝑒₁ 𝑒₂ : Expn} {𝐹 : Frm} {𝑣₁ 𝑣₂ : Val}
          → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
          → 𝐹 ⊢ᵉ 𝑒₂ ⇓ 𝑣₂
          ---------------------------
          → 𝐹 ⊢ᵉ (𝑒₁ +ᵉ 𝑒₂) ⇓ (𝑣₁ + 𝑣₂)

  e-sub : ∀ {𝑒₁ 𝑒₂ : Expn} {𝐹 : Frm} {𝑣₁ 𝑣₂ : Val}
          → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
          → 𝐹 ⊢ᵉ 𝑒₂ ⇓ 𝑣₂
          ---------------------------
          → 𝐹 ⊢ᵉ (𝑒₁ -ᵉ 𝑒₂) ⇓ (𝑣₁ ∸ 𝑣₂)

  e-scale : ∀ {𝑒₁ : Expn} {𝑣₁ 𝑣₂ : Val} {𝐹 : Frm}
            → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
            ---------------------------
            → 𝐹 ⊢ᵉ ( 𝑒₁ *ᵉ⇓ 𝑣₂) ⇓ (𝑣₁ * 𝑣₂)

e-thm-fwd : ∀{𝑒 : Expn}{𝐹 : Frm}{𝑣 : Val}
            → (𝐹 ⊢ᵉ 𝑒 ⇓ 𝑣) → ((⟦ 𝑒 ⟧ᵉ 𝐹) ≡ 𝑣)
e-thm-fwd (e-val{v}{F}) =
  begin
    ⟦ ⇓ v ⟧ᵉ F
  ≡⟨ refl ⟩
    v
  ∎
e-thm-fwd (e-var{x}{F}{v} x↦v) =
  begin
    ⟦ ⇑ x ⟧ᵉ F
  ≡⟨ var-thm-fwd x↦v ⟩
    v
  ∎
e-thm-fwd (e-add{e1}{e2}{F}{v1}{v2} e1⇓v1 e2⇓v2) =
  let
    ⟦e1⟧≡v1 = e-thm-fwd e1⇓v1
    ⟦e2⟧≡v2 = e-thm-fwd e2⇓v2
  in begin
    ⟦ e1 +ᵉ e2 ⟧ᵉ F
  ≡⟨ refl ⟩
    ⟦ e1 ⟧ᵉ F + ⟦ e2 ⟧ᵉ F
  ≡⟨ cong2 _+_ ⟦e1⟧≡v1 ⟦e2⟧≡v2 ⟩
    v1 + v2
  ∎
e-thm-fwd (e-sub{e1}{e2}{F}{v1}{v2} e1⇓v1 e2⇓v2) =
  let
    ⟦e1⟧≡v1 = e-thm-fwd e1⇓v1
    ⟦e2⟧≡v2 = e-thm-fwd e2⇓v2
  in begin
    ⟦ e1 -ᵉ e2 ⟧ᵉ F
  ≡⟨ refl ⟩
    ⟦ e1 ⟧ᵉ F ∸ ⟦ e2 ⟧ᵉ F
  ≡⟨ cong2 _∸_ ⟦e1⟧≡v1 ⟦e2⟧≡v2 ⟩
    v1 ∸ v2
  ∎
e-thm-fwd (e-scale{e1}{v1}{v2}{F} e1⇓v1) =
  let
    ⟦e1⟧≡v1 = e-thm-fwd e1⇓v1
  in begin
    ⟦ e1 *ᵉ⇓ v2 ⟧ᵉ F
  ≡⟨ refl ⟩
    ⟦ e1 ⟧ᵉ F * v2
  ≡⟨ cong2 _*_ ⟦e1⟧≡v1 refl ⟩
    v1 * v2
  ∎

e-thm-rev : ∀{𝑒 : Expn}{𝐹 : Frm}{𝑣 : Val}
  → ((⟦ 𝑒 ⟧ᵉ 𝐹) ≡ 𝑣) → (𝐹 ⊢ᵉ 𝑒 ⇓ 𝑣)
e-thm-rev{e}{F}{v} ⟦e⟧F≡v
    with e
...    | ⇓ w = cong-pred (λ xxx → F ⊢ᵉ (⇓ w) ⇓ xxx) ⟦e⟧F≡v e-val
...    | ⇑ x = let v≡F∥x : v ≡ F ∥ x
                   v≡F∥x = begin
                             v
                           ≡⟨ sym ⟦e⟧F≡v ⟩
                             ⟦ ⇑ x ⟧ᵉ F
                           ≡⟨ refl ⟩
                             F ∥ x
                           ∎
                in  e-var (var-thm-rev (sym v≡F∥x))
...    | e1 +ᵉ e2 = {!!}
...    | e1 -ᵉ e2 = {!!}
...    | e1 *ᵉ⇓ v2 = {!!}

--
-- SEMANTICS of conditions as a decidable relation
--

data _⊢ᶜ_ : Frm → Cond → Set
data _⊬ᶜ_ : Frm → Cond → Set

data _⊢ᶜ_ where

  c-tt :  ∀ {𝐹 : Frm}
          -----------
          → 𝐹 ⊢ᶜ ⇓true

  c-and : ∀ {𝒸₁ 𝒸₂ : Cond} {𝐹 : Frm}
          → 𝐹 ⊢ᶜ 𝒸₁
          → 𝐹 ⊢ᶜ 𝒸₂
          -----------------
          → 𝐹 ⊢ᶜ (𝒸₁ ∧ᶜ 𝒸₂)

  c-or₁ : ∀ {𝒸₁ 𝒸₂ : Cond} {𝐹 : Frm}
          → 𝐹 ⊢ᶜ 𝒸₁
          ---------------
          → 𝐹 ⊢ᶜ (𝒸₁ ∨ᶜ 𝒸₂)

  c-or₂ : ∀ {𝒸₁ 𝒸₂ : Cond} {𝐹 : Frm}
          → 𝐹 ⊢ᶜ 𝒸₂
          ----------------
          → 𝐹 ⊢ᶜ (𝒸₁ ∨ᶜ 𝒸₂)

  c-less : ∀ {𝑒₁ 𝑒₂ : Expn} {𝐹 : Frm} {𝑣₁ 𝑣₂ : Val}
           → 𝑣₁ < 𝑣₂ ≡ tt
           → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
           → 𝐹 ⊢ᵉ 𝑒₂ ⇓ 𝑣₂
           -------------------
           → 𝐹 ⊢ᶜ [ 𝑒₁ <ᶜ 𝑒₂ ]

  c-eq : ∀ {𝑒₁ 𝑒₂ : Expn} {𝐹 : Frm} {𝑣₁ 𝑣₂ : Val}
           → 𝑣₁ =ℕ 𝑣₂ ≡ tt
           → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
           → 𝐹 ⊢ᵉ 𝑒₂ ⇓ 𝑣₂
           -------------------
           → 𝐹 ⊢ᶜ [ 𝑒₁ =ᶜ 𝑒₂ ]

  c-not : ∀ {𝒸 : Cond} {𝐹 : Frm}
          → 𝐹 ⊬ᶜ 𝒸
          -------------
          → 𝐹 ⊢ᶜ (¬ᶜ 𝒸)

data _⊬ᶜ_ where

  ~c-ff :  ∀ {𝐹 : Frm}
           --------------
           → 𝐹 ⊬ᶜ ⇓false

  ~c-or : ∀ {𝒸₁ 𝒸₂ : Cond} {𝐹 : Frm}
          → 𝐹 ⊬ᶜ 𝒸₁
          → 𝐹 ⊬ᶜ 𝒸₂
          ----------------
          → 𝐹 ⊬ᶜ (𝒸₁ ∨ᶜ 𝒸₂)

  ~c-and₁ : ∀ {𝒸₁ 𝒸₂ : Cond} {𝐹 : Frm}
            → 𝐹 ⊬ᶜ 𝒸₁
            -----------------
            → 𝐹 ⊬ᶜ (𝒸₁ ∧ᶜ 𝒸₂)

  ~c-and₂ : ∀ {𝒸₁ 𝒸₂ : Cond} {𝐹 : Frm}
            → 𝐹 ⊬ᶜ 𝒸₂
            -----------------
            → 𝐹 ⊬ᶜ (𝒸₁ ∧ᶜ 𝒸₂)

  ~c-eq : ∀ {𝑒₁ 𝑒₂ : Expn} {𝐹 : Frm} {𝑣₁ 𝑣₂ : Val}
            → 𝑣₁ =ℕ 𝑣₂ ≡ ff
            → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
            → 𝐹 ⊢ᵉ 𝑒₂ ⇓ 𝑣₂
            -------------------
            → 𝐹 ⊬ᶜ [ 𝑒₁ =ᶜ 𝑒₂ ]

  ~c-less : ∀ {𝑒₁ 𝑒₂ : Expn} {𝐹 : Frm} {𝑣₁ 𝑣₂ : Val}
            → 𝑣₁ < 𝑣₂ ≡ ff
            → 𝐹 ⊢ᵉ 𝑒₁ ⇓ 𝑣₁
            → 𝐹 ⊢ᵉ 𝑒₂ ⇓ 𝑣₂
            -------------------
            → 𝐹 ⊬ᶜ [ 𝑒₁ <ᶜ 𝑒₂ ]

  ~c-not : ∀ {𝒸 : Cond} {𝐹 : Frm}
           → 𝐹 ⊢ᶜ 𝒸
           -------------
           → 𝐹 ⊬ᶜ (¬ᶜ 𝒸)

test3 : [] ⊢ᶜ (⇓true ∧ᶜ (¬ᶜ ⇓false))
test3 = c-and c-tt (c-not ~c-ff)

c-thm-fwd : ∀{𝒸 : Cond}{𝐹 : Frm} → 𝐹 ⊢ᶜ 𝒸 → (⟦ 𝒸 ⟧ᶜ 𝐹 ≡ tt)
~c-thm-fwd : ∀{𝒸 : Cond}{𝐹 : Frm} → 𝐹 ⊬ᶜ 𝒸 → (⟦ 𝒸 ⟧ᶜ 𝐹 ≡ ff)
c-thm-fwd (c-tt{F}) =
  begin
    ⟦ ⇓true ⟧ᶜ F
  ≡⟨ refl ⟩
    tt
  ∎
c-thm-fwd (c-and{c1}{c2}{F} dat1 dat2) =
  let
    ⟦c1⟧F≡tt : ⟦ c1 ⟧ᶜ F ≡ tt
    ⟦c1⟧F≡tt = c-thm-fwd dat1
    ⟦c2⟧F≡tt : ⟦ c2 ⟧ᶜ F ≡ tt
    ⟦c2⟧F≡tt = c-thm-fwd dat2
  in begin
    ⟦ c1 ∧ᶜ c2 ⟧ᶜ F
  ≡⟨ refl ⟩
    (⟦ c1 ⟧ᶜ F) && (⟦ c2 ⟧ᶜ F)
  ≡⟨ cong2 _&&_ ⟦c1⟧F≡tt ⟦c2⟧F≡tt ⟩
    tt && tt
  ≡⟨ refl ⟩
    tt
  ∎
c-thm-fwd (c-or₁{c1}{c2}{F} dat1) =
  let
    ⟦c1⟧F≡tt : ⟦ c1 ⟧ᶜ F ≡ tt
    ⟦c1⟧F≡tt = c-thm-fwd dat1
  in begin
    ⟦ c1 ∨ᶜ c2 ⟧ᶜ F
  ≡⟨ refl ⟩
    (⟦ c1 ⟧ᶜ F) || (⟦ c2 ⟧ᶜ F)
  ≡⟨ cong2 _||_ ⟦c1⟧F≡tt refl ⟩
    tt || (⟦ c2 ⟧ᶜ F)
  ≡⟨ refl ⟩
    tt
  ∎
c-thm-fwd (c-or₂{c1}{c2}{F} dat2) =
  let
    ⟦c2⟧F≡tt : ⟦ c2 ⟧ᶜ F ≡ tt
    ⟦c2⟧F≡tt = c-thm-fwd dat2
  in begin
    ⟦ c1 ∨ᶜ c2 ⟧ᶜ F
  ≡⟨ refl ⟩
    (⟦ c1 ⟧ᶜ F) || (⟦ c2 ⟧ᶜ F)
  ≡⟨ cong2 _||_ refl ⟦c2⟧F≡tt ⟩
    (⟦ c1 ⟧ᶜ F) || tt
  ≡⟨ ||-tt (⟦ c1 ⟧ᶜ F) ⟩
    tt
  ∎
c-thm-fwd (c-less{e1}{e2}{F}{v1}{v2} v1<v2 e1⇓v1 e2⇓v2) =
  let
    ⟦e1⟧F≡v1 : ⟦ e1 ⟧ᵉ F ≡ v1
    ⟦e1⟧F≡v1 = e-thm-fwd e1⇓v1
    ⟦e2⟧F≡v2 : ⟦ e2 ⟧ᵉ F ≡ v2
    ⟦e2⟧F≡v2 = e-thm-fwd e2⇓v2
  in
    begin
      ⟦ [ e1 <ᶜ e2 ] ⟧ᶜ F
    ≡⟨ refl ⟩
      ⟦ e1 ⟧ᵉ F < ⟦ e2 ⟧ᵉ F
    ≡⟨ cong2 _<_ ⟦e1⟧F≡v1 ⟦e2⟧F≡v2 ⟩
      v1 < v2
    ≡⟨ v1<v2 ⟩
     tt
   ∎
c-thm-fwd (c-eq{e1}{e2}{F}{v1}{v2} v1≡v2 e1⇓v1 e2⇓v2) =
  let
    ⟦e1⟧F≡v1 : ⟦ e1 ⟧ᵉ F ≡ v1
    ⟦e1⟧F≡v1 = e-thm-fwd e1⇓v1
    ⟦e2⟧F≡v2 : ⟦ e2 ⟧ᵉ F ≡ v2
    ⟦e2⟧F≡v2 = e-thm-fwd e2⇓v2
  in begin
    ⟦ [ e1 =ᶜ e2 ] ⟧ᶜ F
  ≡⟨ refl ⟩
    ⟦ e1 ⟧ᵉ F =ℕ ⟦ e2 ⟧ᵉ F
  ≡⟨ cong2 _=ℕ_ ⟦e1⟧F≡v1 ⟦e2⟧F≡v2 ⟩
    v1 =ℕ v2
  ≡⟨ v1≡v2 ⟩
   tt
  ∎
c-thm-fwd (c-not{c}{F} dat) =
  let
    ⟦c⟧F≡ff : ⟦ c ⟧ᶜ F ≡ ff
    ⟦c⟧F≡ff = ~c-thm-fwd dat
  in begin
  begin
    ⟦ ¬ᶜ c ⟧ᶜ F
  ≡⟨ refl ⟩
    ~ ⟦ c ⟧ᶜ F
  ≡⟨ cong ~_ ⟦c⟧F≡ff ⟩
    ~ ff
  ≡⟨ refl ⟩
    tt
  ∎
~c-thm-fwd (~c-ff{F}) =
  begin
    ⟦ ⇓false ⟧ᶜ F
  ≡⟨ refl ⟩
    ff
  ∎
~c-thm-fwd (~c-or{c1}{c2}{F} dat1 dat2) =
  let
    ⟦c1⟧F≡ff : ⟦ c1 ⟧ᶜ F ≡ ff
    ⟦c1⟧F≡ff = ~c-thm-fwd dat1
    ⟦c2⟧F≡ff : ⟦ c2 ⟧ᶜ F ≡ ff
    ⟦c2⟧F≡ff = ~c-thm-fwd dat2
  in begin
    ⟦ c1 ∨ᶜ c2 ⟧ᶜ F
  ≡⟨ refl ⟩
    (⟦ c1 ⟧ᶜ F) || (⟦ c2 ⟧ᶜ F)
  ≡⟨ cong2 _||_ ⟦c1⟧F≡ff ⟦c2⟧F≡ff ⟩
    ff || ff
  ≡⟨ refl ⟩
    ff
  ∎
~c-thm-fwd (~c-and₁{c1}{c2}{F} dat1) =
  let
    ⟦c1⟧F≡ff : ⟦ c1 ⟧ᶜ F ≡ ff
    ⟦c1⟧F≡ff = ~c-thm-fwd dat1
  in begin
    ⟦ c1 ∧ᶜ c2 ⟧ᶜ F
  ≡⟨ refl ⟩
    (⟦ c1 ⟧ᶜ F) && (⟦ c2 ⟧ᶜ F)
  ≡⟨ cong2 _&&_ ⟦c1⟧F≡ff refl ⟩
    ff && (⟦ c2 ⟧ᶜ F)
  ≡⟨ refl ⟩
    ff
  ∎
~c-thm-fwd (~c-and₂{c1}{c2}{F} dat2) =
  let
    ⟦c2⟧F≡ff : ⟦ c2 ⟧ᶜ F ≡ ff
    ⟦c2⟧F≡ff = ~c-thm-fwd dat2
  in begin
  begin
    ⟦ c1 ∧ᶜ c2 ⟧ᶜ F
  ≡⟨ refl ⟩
    (⟦ c1 ⟧ᶜ F) && (⟦ c2 ⟧ᶜ F)
  ≡⟨ cong2 _&&_ refl ⟦c2⟧F≡ff ⟩
    (⟦ c1 ⟧ᶜ F) && ff
  ≡⟨ &&-ff (⟦ c1 ⟧ᶜ F) ⟩
    ff
  ∎
~c-thm-fwd (~c-less{e1}{e2}{F}{v1}{v2} v1≮v2 e1⇓v1 e2⇓v2) =
  let
    ⟦e1⟧F≡v1 : ⟦ e1 ⟧ᵉ F ≡ v1
    ⟦e1⟧F≡v1 = e-thm-fwd e1⇓v1
    ⟦e2⟧F≡v2 : ⟦ e2 ⟧ᵉ F ≡ v2
    ⟦e2⟧F≡v2 = e-thm-fwd e2⇓v2
  in
    begin
      ⟦ [ e1 <ᶜ e2 ] ⟧ᶜ F
    ≡⟨ refl ⟩
      ⟦ e1 ⟧ᵉ F < ⟦ e2 ⟧ᵉ F
    ≡⟨ cong2 _<_ ⟦e1⟧F≡v1 ⟦e2⟧F≡v2 ⟩
      v1 < v2
    ≡⟨ v1≮v2 ⟩
     ff
   ∎
~c-thm-fwd (~c-eq{e1}{e2}{F}{v1}{v2} v1≢v2 e1⇓v1 e2⇓v2) =
  let
    ⟦e1⟧F≡v1 : ⟦ e1 ⟧ᵉ F ≡ v1
    ⟦e1⟧F≡v1 = e-thm-fwd e1⇓v1
    ⟦e2⟧F≡v2 : ⟦ e2 ⟧ᵉ F ≡ v2
    ⟦e2⟧F≡v2 = e-thm-fwd e2⇓v2
  in begin
    ⟦ [ e1 =ᶜ e2 ] ⟧ᶜ F
  ≡⟨ refl ⟩
    ⟦ e1 ⟧ᵉ F =ℕ ⟦ e2 ⟧ᵉ F
  ≡⟨ cong2 _=ℕ_ ⟦e1⟧F≡v1 ⟦e2⟧F≡v2 ⟩
    v1 =ℕ v2
  ≡⟨ v1≢v2 ⟩
   ff
  ∎
~c-thm-fwd (~c-not{c}{F} ⊢c) =
  begin
    ⟦ ¬ᶜ c ⟧ᶜ F
  ≡⟨ refl ⟩
    ~ ⟦ c ⟧ᶜ F
  ≡⟨ cong ~_ (c-thm-fwd ⊢c) ⟩
    ~ tt
  ≡⟨ refl ⟩
    ff
  ∎

-- These can probably be shown just by using
-- the contrapositives of c-thm-fwd and ~c-thm-fwd
postulate
  c-thm-rev : ∀{𝒸 : Cond}{𝐹 : Frm} → (⟦ 𝒸 ⟧ᶜ 𝐹 ≡ tt) → 𝐹 ⊢ᶜ 𝒸
  ~c-thm-rev : ∀{𝒸 : Cond}{𝐹 : Frm} → (⟦ 𝒸 ⟧ᶜ 𝐹 ≡ ff) → 𝐹 ⊬ᶜ 𝒸

--
-- SEMANTICS of program statements
-- as a state transformation relation
--

data _=[_]⇒_ : Frm → Stmt → Frm → Set where

  s-skip : ∀ {𝐹 : Frm}
    --------------
    → 𝐹 =[ skip ]⇒ 𝐹

  s-assign : ∀ {𝑥 : Id} {𝑒 : Expn} {𝐹 : Frm}  {𝑣 : Val}
    → 𝐹 ⊢ᵉ 𝑒 ⇓ 𝑣
    ---------------------------
    → 𝐹 =[ 𝑥 ∷= 𝑒 ]⇒ (𝐹 ∣ 𝑥 ↦ 𝑣)

  s-seq : ∀ {𝑠₁ 𝑠₂ : Stmt} {𝐹₀ 𝐹₁ 𝐹₂ : Frm}
    → 𝐹₀ =[ 𝑠₁ ]⇒ 𝐹₁
    → 𝐹₁ =[ 𝑠₂ ]⇒ 𝐹₂
    -------------------
    → 𝐹₀ =[ 𝑠₁ ↩ 𝑠₂ ]⇒ 𝐹₂

  s-if-then : ∀ {𝒸 : Cond} {𝑠₁ 𝑠₂ : Stmt} {𝐹 𝐹' : Frm}
    → 𝐹 ⊢ᶜ 𝒸
    → 𝐹 =[ 𝑠₁ ]⇒ 𝐹'
    → 𝐹 =[ 𝑠₂ ]⇒ 𝐹'
    ------------------------------------
    → 𝐹 =[ if 𝒸 then 𝑠₁ else 𝑠₂ end ]⇒ 𝐹'

  s-if-else : ∀ {𝒸 : Cond} {𝑠₁ 𝑠₂ : Stmt} {𝐹 𝐹' : Frm}
    → 𝐹 ⊬ᶜ 𝒸
    → 𝐹 =[ 𝑠₂ ]⇒ 𝐹'
    ------------------------------------
    → 𝐹 =[ if 𝒸 then 𝑠₁ else 𝑠₂ end ]⇒ 𝐹'

  s-repeat-0 : ∀ {𝑠 : Stmt} {𝑥 : Id} {𝐹 : Frm}
     → 𝐹 ⊢ᶠ 𝑥 ↦ 0
     -----------------------------
     → 𝐹 =[ by 𝑥 repeat 𝑠 end ]⇒ 𝐹

  s-repeat-suc : ∀ {𝑛 : ℕ} {𝑠 : Stmt} {𝑥 : Id} {𝐹 𝐹' : Frm}
    → 𝐹 ⊢ᶠ 𝑥 ↦ suc 𝑛
    → 𝐹 =[ 𝑠 ↩ 𝑥 ∷= (⇓ 𝑛) ↩ by 𝑥 repeat 𝑠 end ]⇒ 𝐹'
    ----------------------------------------------
    → 𝐹 =[ by 𝑥 repeat 𝑠 end ]⇒ 𝐹'

  --
  -- A lil cheat: "returns" is just assign; doesn't exit

  s-return : ∀ {𝑒 : Expn} {𝐹 : Frm}  {𝑣 : Val}
    → 𝐹 ⊢ᵉ 𝑒 ⇓ 𝑣
    -------------------------------------
    → 𝐹 =[ returns 𝑒 ]⇒ (𝐹 ∣ "retval" ↦ 𝑣)

arg1 : Id
arg1 = "arg1"

arg2 : Id
arg2 = "arg2"

retval : Id
retval = "retval"

W : Id
W = "w"

X : Id
X = "x"

Y : Id
Y = "y"

Z : Id
Z = "z"

pgm0 : Stmt
pgm0 = X ∷= ⇓ 3 ↩
       Y ∷= ⇓ 1 ↩
       Y ∷= ⇑ Y *ᵉ⇓ 2

pgm1 : Stmt
pgm1 = X ∷= ⇓ 3 ↩
       Y ∷= ⇓ 1 ↩
       by X repeat
         Y ∷= ⇑ Y *ᵉ⇓ 2
       end

Z∷=X*Y = W ∷= ⇑ X ↩
         Z ∷= ⇓ 0 ↩
         by W repeat
           Z ∷= ⇑ Z +ᵉ ⇑ Y
         end

pgm2 = X ∷= ⇓ 3 ↩
       Y ∷= ⇓ 1 ↩
       by X repeat
         Z∷=X*Y ↩
         Y ∷= ⇑ Z
       end

fact-pgm : Stmt
fact-pgm =
  X ∷= ⇑ arg1 ↩
  Y ∷= ⇓ 1 ↩
  by X repeat
    Z∷=X*Y ↩
    Y ∷= ⇑ Z
  end ↩
  returns ⇑ Y

min-pgm : Stmt
min-pgm = if [ ⇑ arg2 <ᶜ ⇑ arg1 ] then
            X ∷= ⇑ arg1 ↩
            arg1 ∷= ⇑ arg2 ↩
            arg2 ∷= ⇑ X
          else
            skip
          end

result1 = ⟦ pgm1 ⟧ˢ [-↦0]
result2 = ⟦ pgm2 ⟧ˢ [-↦0]

[➊↦_] : Val → Frm
[➊↦ 𝑣 ] = [-↦0] ∣ arg1 ↦ 𝑣

[➊↦_,➋↦_] : Val →  Val → Frm
[➊↦ 𝑣₁ ,➋↦ 𝑣₂ ] = (([-↦0] ∣ arg1 ↦ 𝑣₁) ∣ arg2 ↦ 𝑣₂ )

frame6 = ((((( [➊↦ 3 ] ∣ X ↦ 0) ∣ Y ↦ 6) ∣ W ↦ 0) ∣ Z ↦ 6) ∣ retval ↦ 6)
postulate
  test6 : [➊↦ 3 ] =[ fact-pgm ]⇒ frame6

exec : Stmt → Frm
exec 𝑠 = ⟦ 𝑠 ⟧ˢ [-↦0]

exec1 : Stmt → Val → Frm
exec1 𝑠 𝑣₁ = ⟦ 𝑠 ⟧ˢ [➊↦ 𝑣₁ ]

exec2 : Stmt → Val → Val → Frm
exec2 𝑠 𝑣₁ 𝑣₂ = ⟦ 𝑠 ⟧ˢ [➊↦ 𝑣₁ ,➋↦ 𝑣₂ ]

test7 = exec2 min-pgm 7 5

test7a : (test7 ∥ arg1) ≡ 5
test7a = refl

test7b : (test7 ∥ arg2) ≡ 7
test7b = refl

postulate
  s-thm : ∀ {𝑠 : Stmt } {𝐹 : Frm} → 𝐹 =[ 𝑠 ]⇒ (⟦ 𝑠 ⟧ˢ 𝐹)

postulate
  fact-thm : ∀ {n : ℕ} {𝐹 : Frm} → [➊↦ n ] =[ fact-pgm ]⇒ 𝐹 → 𝐹 ⊢ᶠ retval ↦ (factorial n)

max_stars_repo_name: JimFixGroupResearch/imper-ial

max_issues_repo_name: JimFixGroupResearch/imper-ial

max_forks_repo_name: JimFixGroupResearch/imper-ial


text:
{- Name: Bowornmet (Ben) Hudson

--Progress and Preservation in Godel's T--

Progress: if e:τ, then either e val or ∃e' such that e=>e'.
Preservation: if e:τ and e=>e', then e':τ.

-}

open import Preliminaries

module Godel where

  -- nat and =>
  data Typ : Set where
    nat : Typ
    _⇒_ : Typ → Typ → Typ

------------------------------------------

  -- represent a context as a list of types
  Ctx = List Typ

  -- de Bruijn indices (for free variables)
  data _∈_ : Typ → Ctx → Set where
    i0 : ∀ {Γ τ}
       → τ ∈ (τ :: Γ)
    iS : ∀ {Γ τ τ1}
       → τ ∈ Γ
       → τ ∈ (τ1 :: Γ)

------------------------------------------

  -- static semantics
  data _|-_ : Ctx → Typ → Set where
    var : ∀ {Γ τ}
        → (x : τ ∈ Γ) → Γ |- τ
    z : ∀ {Γ}
      → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ τ}
        → (e : Γ |- nat)
        → (e0 : Γ |- τ)
        → (e1 : (nat :: (τ :: Γ)) |- τ)
        → Γ |- τ
    lam : ∀ {Γ τ ρ}
        → (x : (ρ :: Γ) |- τ)
        → Γ |- (ρ ⇒ τ)
    app : ∀ {Γ τ1 τ2}
       → (e1 : Γ |- (τ2 ⇒ τ1)) → (e2 : Γ |- τ2)
       → Γ |- τ1

------------------------------------------

  -- renaming function
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  -- re: transferring variables in contexts
  lem1 : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  lem1 d i0 = i0
  lem1 d (iS x) = iS (d x)

  -- renaming lemma
  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren (var x) d = var (d x)
  ren z d = z
  ren (suc e) d = suc (ren e d)
  ren (rec e e0 e1) d = rec (ren e d) (ren e0 d) (ren e1 (lem1(lem1 d)))
  ren (lam e) d = lam (ren e (lem1 d))
  ren (app e1 e2) d = app (ren e1 d) (ren e2 d)

------------------------------------------

  -- substitution
  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  -- weakening a context
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  -- weakening also works with substitution
  wkn-s : ∀ {Γ τ1 Γ'} → sctx Γ Γ' → sctx (τ1 :: Γ) Γ'
  wkn-s d = λ f → wkn (d f)

  wkn-r : ∀ {Γ τ1 Γ'} → rctx Γ Γ' → rctx (τ1 :: Γ) Γ'
  wkn-r d = λ x → iS (d x)

  -- lem2 (need a lemma for subst like we did for renaming)
  lem2 : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  lem2 d i0 = var i0
  lem2 d (iS i) = wkn (d i)

  -- another substitution lemma
  lem3 : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  lem3 e i0 = e
  lem3 e (iS i) = var i

  -- one final lemma needed for the last stepping rule. Thank you Professor Licata!
  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 e1 e2 i0 = e1
  lem4 e1 e2 (iS i0) = e2
  lem4 e1 e2 (iS (iS i)) = var i

  -- the 'real' substitution lemma (if (x : τ') :: Γ |- (e : τ) and Γ |- (e : τ') , then Γ |- e[x -> e'] : τ)
  subst : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ' |- τ → Γ |- τ
  subst d (var x) = d x
  subst d z = z
  subst d (suc e) = suc (subst d e)
  subst d (rec e e0 e1) = rec (subst d e) (subst d e0) (subst (lem2 (lem2 d)) e1)
  subst d (lam e) = lam (subst (lem2 d) e)
  subst d (app e1 e2) = app (subst d e1) (subst d e2)

------------------------------------------

  -- closed values of L{nat,⇒} (when something is a value)
  -- recall that we use empty contexts when we work with dynamic semantics
  data val : ∀ {τ} → [] |- τ → Set where
    z-isval : val z
    suc-isval : (e : [] |- nat) → (val e)
              → val (suc e)
    lam-isval : ∀ {ρ τ} (e : (ρ :: []) |- τ)
              → val (lam e)

------------------------------------------

  -- stepping rules (preservation is folded into this)
  -- Preservation: if e:τ and e=>e', then e':τ
  data _>>_ : ∀ {τ} → [] |- τ → [] |- τ → Set where
     suc-steps : (e e' : [] |- nat)
               → e >> e'
               → (suc e) >> (suc e')
     app-steps : ∀ {τ1 τ2}
              → (e1 e1' : [] |- (τ2 ⇒ τ1)) → (e2 : [] |- τ2)
              → e1 >> e1'
              → (app e1 e2) >> (app e1' e2)
     app-steps-2 : ∀ {τ1 τ2}
                → (e1 : [] |- (τ2 ⇒ τ1)) → (e2 e2' : [] |- τ2)
                → val e1 → e2 >> e2'
                → (app e1 e2) >> (app e1 e2')
     app-steps-3 : ∀ {τ1 τ2}
                → (e1 : (τ1 :: []) |- τ2)
                → (e2 : [] |- τ1)
                → (app (lam e1) e2) >> subst (lem3 e2) e1
     rec-steps : ∀ {τ}
               → (e e' : [] |- nat)
               → (e0 : [] |- τ)
               → (e1 : (nat :: (τ :: [])) |- τ)
               → e >> e'
               → (rec e e0 e1) >> (rec e' e0 e1)
     rec-steps-z : ∀ {τ}
                 → (e : val z)
                 → (e0 : [] |- τ)
                 → (e1 : (nat :: (τ :: [])) |- τ)
                 → (rec z e0 e1) >> e0
     rec-steps-suc : ∀ {τ}
                   → (e : [] |- nat)
                   → (e0 : [] |- τ)
                   → (e1 : (nat :: (τ :: [])) |- τ)
                   → val e
                   → (rec (suc e) e0 e1) >> subst (lem4 e (rec e e0 e1)) e1

------------------------------------------

  -- Proof of progress!
  -- Progress: if e:τ, then either e val or ∃e' such that e=>e'
  progress : ∀ {τ} (e : [] |- τ) → Either (val e) (Σ (λ e' → (e >> e')))
  progress (var ())
  progress z = Inl z-isval
  progress (suc e) with progress e
  progress (suc e) | Inl d = Inl (suc-isval e d)
  progress (suc e) | Inr (e' , d) = Inr (suc e' , suc-steps e e' d)
  progress (rec e e1 e2) with progress e
  progress (rec .z e1 e2) | Inl z-isval = Inr (e1 , rec-steps-z z-isval e1 e2)
  progress (rec .(suc e) e1 e2) | Inl (suc-isval e d) = Inr (subst (lem4 e (rec e e1 e2)) e2 , rec-steps-suc e e1 e2 d)
  progress (rec e e1 e2) | Inr (e' , d) = Inr (rec e' e1 e2 , rec-steps e e' e1 e2 d)
  progress (lam e) = Inl (lam-isval e)
  progress (app e1 e2) with progress e1
  progress (app .(lam e) e2) | Inl (lam-isval e) = Inr (subst (lem3 e2) e , app-steps-3 e e2)
  progress (app e1 e2) | Inr (e1' , d) = Inr (app e1' e2 , app-steps e1 e1' e2 d)

------------------------------------------

  -- Denotational semantics

  -- interpreting a T type in Agda
  interp : Typ → Set
  interp nat = Nat
  interp (A ⇒ B) = interp A → interp B

  -- interpreting contexts
  interpC : Ctx → Set
  interpC [] = Unit
  interpC (A :: Γ) = interpC Γ × interp A

  -- helper function to look a variable up in an interpC gamma
  lookupC : ∀{Γ A} → (x : A ∈ Γ) → interpC Γ → interp A
  lookupC i0 (recur , return) = return
  lookupC (iS i) (recur , return) = lookupC i recur

  -- primitive recursion function corresponding to rec
  natrec : ∀{C : Set} → C → (Nat → C → C) → Nat → C
  natrec base step Z = base
  natrec base step (S n) = step n (natrec base step n)

  -- interpreting expressions in Godel's T as a function from the interpretation of the context to the interpretation of its corresponding type
  interpE : ∀{Γ τ} → Γ |- τ → (interpC Γ → interp τ)
  interpE (var x) d = lookupC x d
  interpE z d = Z
  interpE (suc e) d = S (interpE e d)
  interpE (rec e e0 e1) d = natrec (interpE e0 d)  (λ n k → interpE e1 ((d , k) , n)) (interpE e d)
  interpE (lam e) d = λ x → interpE e (d , x)
  interpE (app e1 e2) d = interpE e1 d (interpE e2 d)

  helper : ∀ {Γ Γ' τ} → sctx Γ (τ :: Γ') → sctx Γ Γ'
  helper d = λ x → d (iS x)

  helper-r : ∀ {Γ Γ' τ} → rctx Γ (τ :: Γ') → rctx Γ Γ'
  helper-r d = λ x → d (iS x)

  -- compositionality of functions
  interpS : ∀ {Γ Γ'} → sctx Γ Γ' → interpC Γ → interpC Γ'
  interpS {Γ} {[]} a b = <>
  interpS {Γ} {A :: Γ'} a b = interpS (helper a) b , interpE (a i0) b

  interpR : ∀ {Γ Γ'} → rctx Γ Γ' → interpC Γ → interpC Γ'
  interpR {Γ} {[]} a b = <>
  interpR {Γ} {A :: Γ'} a b = interpR (helper-r a) b , lookupC (a i0) b

  --lemmas for lambda case of interpR-lemma
  interpR-lemma-lemma-lemma : ∀ {Γ Γ' τ} → (x : interp τ) → (Θ : rctx Γ Γ') → (Θ' : interpC Γ) → (interpR Θ Θ') == interpR (wkn-r Θ) (Θ' , x)
  interpR-lemma-lemma-lemma {Γ} {[]} x Θ Θ' = Refl
  interpR-lemma-lemma-lemma {Γ} {A :: Γ'} x Θ Θ' = ap (λ h → h , lookupC (Θ i0) Θ') (interpR-lemma-lemma-lemma x (helper-r Θ) Θ')

  interpR-lemma-lemma : ∀ {Γ Γ' τ} → (x : interp τ) → (Θ : rctx Γ Γ') → (Θ' : interpC Γ) → (interpR Θ Θ' , x) == (interpR (lem1 Θ) (Θ' , x))
  interpR-lemma-lemma {Γ} {[]} x Θ Θ' = Refl
  interpR-lemma-lemma {Γ} {A :: Γ'} x Θ Θ' = ap (λ h → h , x) (interpR-lemma-lemma-lemma x Θ Θ')

  interpR-lemma-lemma-rec : ∀ {Γ Γ' τ} → (x : interp nat) → (y : interp τ) → (Θ : rctx Γ Γ') → (Θ' : interpC Γ)
                                         → ((interpR Θ Θ' , y) , x) == interpR (lem1 (lem1 Θ)) ((Θ' , y) , x)
  interpR-lemma-lemma-rec x y Θ Θ' = interpR-lemma-lemma x (lem1 Θ) (Θ' , y) ∘ ap (λ h → h , x) (interpR-lemma-lemma y Θ Θ')

  interpR-lemma : ∀ {Γ Γ' τ} (e : Γ' |- τ) → (Θ : rctx Γ Γ') → (Θ' : interpC Γ) → (interpE e) (interpR Θ Θ') == (interpE (ren e Θ)) Θ'
  interpR-lemma (var i0) Θ Θ' = Refl
  interpR-lemma (var (iS x)) Θ Θ' = interpR-lemma (var x) (helper-r Θ) Θ'
  interpR-lemma z Θ Θ' = Refl
  interpR-lemma (suc e) Θ Θ' = ap S (interpR-lemma e Θ Θ')
  interpR-lemma {Γ} {Γ'} {τ} (rec e e1 e2) Θ Θ' = natrec (interpE e1 (interpR Θ Θ'))
                                                    (λ n k → interpE e2 ((interpR Θ Θ' , k) , n))
                                                      (interpE e (interpR Θ Θ'))                       =⟨ ap
                                                                                (λ h →
                                                                                natrec h (λ n k → interpE e2 ((interpR Θ Θ' , k) , n))
                                                                                (interpE e (interpR Θ Θ')))
                                                                                (interpR-lemma e1 Θ Θ') ⟩
                                                  natrec (interpE (ren e1 Θ) Θ')
                                                    (λ n k → interpE e2 ((interpR Θ Θ' , k) , n))
                                                      (interpE e (interpR Θ Θ'))                       =⟨ ap
                                                                                (λ h →
                                                                                natrec (interpE (ren e1 Θ) Θ')
                                                                                (λ n k → interpE e2 ((interpR Θ Θ' , k) , n)) h)
                                                                                (interpR-lemma e Θ Θ') ⟩
                                                  natrec (interpE (ren e1 Θ) Θ')
                                                    (λ n k → interpE e2 ((interpR Θ Θ' , k) , n))
                                                      (interpE (ren e Θ) Θ')                           =⟨ ap
                                                                                (λ h →
                                                                                natrec (interpE (ren e1 Θ) Θ') h (interpE (ren e Θ) Θ'))
                                                                                (λ=
                                                                                (λ x →
                                                                                λ=
                                                                                (λ y →
                                                                                ap (λ h → interpE e2 h) (interpR-lemma-lemma-rec x y Θ Θ')))) ⟩
                                                  natrec (interpE (ren e1 Θ) Θ')
                                                    (λ n k → interpE e2 (interpR (lem1 (lem1 Θ)) ((Θ' , k) , n)))
                                                      (interpE (ren e Θ) Θ')                           =⟨ ap
                                                                                (λ h →
                                                                                natrec (interpE (ren e1 Θ) Θ') h (interpE (ren e Θ) Θ'))
                                                                                (λ=
                                                                                (λ x →
                                                                                λ=
                                                                                (λ y →
                                                                                interpR-lemma {nat :: τ :: Γ} {nat :: τ :: Γ'} e2 (lem1 (lem1 Θ))
                                                                                ((Θ' , y) , x)))) ⟩
                                                  natrec (interpE (ren e1 Θ) Θ')
                                                    (λ n k → interpE (ren e2 (lem1 (lem1 Θ))) ((Θ' , k) , n))
                                                       (interpE (ren e Θ) Θ')                          ∎

  interpR-lemma {Γ} {Γ'} {ρ ⇒ τ} (lam e) Θ Θ' = interpE (lam e) (interpR Θ Θ') =⟨ Refl ⟩
                              (λ x → interpE e (interpR Θ Θ' , x)) =⟨ λ= (λ x → ap (λ h → interpE e h) (interpR-lemma-lemma x Θ Θ')) ⟩
                              (λ x → interpE e (interpR (lem1 Θ) (Θ' , x))) =⟨ λ= (λ x → interpR-lemma {ρ :: Γ} {ρ :: Γ'} e (lem1 Θ) (Θ' , x)) ⟩
                              ((λ x → interpE (ren e (lem1 Θ)) (Θ' , x)) ∎)

  interpR-lemma (app e1 e2) Θ Θ' = interpE (app e1 e2) (interpR Θ Θ')                     =⟨ Refl ⟩
                                   interpE e1 (interpR Θ Θ') (interpE e2 (interpR Θ Θ'))  =⟨ ap (λ x → x (interpE e2 (interpR Θ Θ'))) (interpR-lemma e1 Θ Θ') ⟩
                                   interpE (ren e1 Θ) Θ' (interpE e2 (interpR Θ Θ'))      =⟨ ap (λ x → interpE (ren e1 Θ) Θ' x) (interpR-lemma e2 Θ Θ')  ⟩
                                   interpE (ren e1 Θ) Θ' (interpE (ren e2 Θ) Θ')          ∎

  -- no proof is possible without the genius of Dan Licata
  mutual
    wkn-lemma : ∀ {Γ τ} (a : interp τ) → (Θ' : interpC Γ) →  Θ' == interpR iS (Θ' , a)
    wkn-lemma a Θ' = interpR-lemma-lemma-lemma a (λ x → x) Θ' ∘ ! (mutual-lemma Θ')

    mutual-lemma : ∀ {Γ} (Θ' : interpC Γ) → interpR (λ x → x) Θ' == Θ'
    mutual-lemma {[]} Θ' = Refl
    mutual-lemma {A :: Γ} (Θ' , a) = ! (ap (λ h → h , a) (wkn-lemma a Θ'))

  interp-lemma2 : ∀ {Γ τ' Θ' τ} (a : interp τ) → (e : Γ |- τ') → interpE e Θ' == interpE (wkn e) (Θ' , a)
  interp-lemma2 {Γ} {τ'} {Θ'} a e = interpE e Θ'                      =⟨ ap (λ x → interpE e x) (wkn-lemma a Θ') ⟩
                                    interpE e (interpR iS (Θ' , a))   =⟨ interpR-lemma e iS (Θ' , a) ⟩
                                    interpE (ren e iS) (Θ' , a)       ∎

  interp-lemma : ∀ {Γ Γ' Θ' τ} (a : interp τ) → (Θ : sctx Γ Γ') → interpS Θ Θ' == interpS (wkn-s Θ) (Θ' , a)
  interp-lemma {Γ} {[]} a Θ = Refl
  interp-lemma {Γ} {A :: Γ'} a Θ = ap2 (λ x y → x , y) (interp-lemma a (helper Θ)) (interp-lemma2 a (Θ i0))

  lemma : ∀ {Γ Γ' Θ' τ} (x : interp τ) → (Θ : sctx Γ Γ') → ((interpS Θ Θ') , x) == (interpS (lem2 Θ) (Θ' , x))
  lemma x Θ = ap (λ y → y , x) (interp-lemma x Θ)

  lemma-c-lemma-lemma : ∀ {Γ Γ' τ} → (x : interp τ) → (Θ : sctx Γ Γ') → (Θ' : interpC Γ) → (interpS Θ Θ') == (interpS (wkn-s Θ) (Θ' , x))
  lemma-c-lemma-lemma {Γ} {[]} x Θ Θ' = Refl
  lemma-c-lemma-lemma {Γ} {A :: Γ'} x Θ Θ' = ap2 (λ x₁ y → x₁ , y) (lemma-c-lemma-lemma x (helper Θ) Θ') (interp-lemma2 x (Θ i0))

  lemma-c-lemma : ∀ {Γ Γ' τ} → (x : interp τ) → (Θ : sctx Γ Γ') → (Θ' : interpC Γ) → (interpS Θ Θ' , x) == (interpS (lem2 Θ) (Θ' , x))
  lemma-c-lemma {Γ} {[]} x Θ Θ' = Refl
  lemma-c-lemma {Γ} {A :: Γ'} x Θ Θ' = ap (λ h → h , x) (lemma-c-lemma-lemma x Θ Θ')

  lemma-c-lemma-rec : ∀ {Γ Γ' τ} → (x : interp nat) → (y : interp τ) → (Θ : sctx Γ Γ') → (Θ' : interpC Γ)
                                         → ((interpS Θ Θ' , y) , x) == interpS (lem2 (lem2 Θ)) ((Θ' , y) , x)
  lemma-c-lemma-rec {Γ} {[]} x y Θ Θ' = Refl
  lemma-c-lemma-rec {Γ} {A :: Γ'} x y Θ Θ' = lemma-c-lemma x (lem2 Θ) (Θ' , y) ∘ ap (λ h → h , x) (lemma-c-lemma y Θ Θ')

  lemma-c : ∀ {Γ Γ' τ} (e : Γ' |- τ) → (Θ : sctx Γ Γ') → (Θ' : interpC Γ) → (interpE e) (interpS Θ Θ') == (interpE (subst Θ e)) Θ'
  lemma-c (var i0) b c = Refl
  lemma-c (var (iS x)) b c = lemma-c (var x) (helper b) c
  lemma-c z b c = Refl
  lemma-c (suc e) b c = ap S (lemma-c e b c)
  lemma-c {Γ} {Γ'} {τ} (rec e e0 e1) b c = natrec (interpE e0 (interpS b c))
                                (λ n k → interpE e1 ((interpS b c , k) , n))
                                (interpE e (interpS b c))
                                                      =⟨ ap
                                                        (λ h →
                                                          natrec h (λ n k → interpE e1 ((interpS b c , k) , n))
                                                            (interpE e (interpS b c)))
                                                              (lemma-c e0 b c) ⟩
                              natrec (interpE (subst b e0) c)
                                (λ n k → interpE e1 ((interpS b c , k) , n))
                                (interpE e (interpS b c))
                                                      =⟨ ap
                                                           (λ h →
                                                              natrec (interpE (subst b e0) c)
                                                              (λ n k → interpE e1 ((interpS b c , k) , n)) h)
                                                           (lemma-c e b c) ⟩
                              natrec (interpE (subst b e0) c)
                                (λ n k → interpE e1 ((interpS b c , k) , n))
                                (interpE (subst b e) c) =⟨ ap
                                                             (λ h → natrec (interpE (subst b e0) c) h (interpE (subst b e) c))
                                                               (λ= (λ x →
                                                                 λ= (λ y →
                                                                   ap (λ h → interpE e1 h) (lemma-c-lemma-rec x y b c)))) ⟩
                              natrec (interpE (subst b e0) c)
                                (λ n k → interpE e1 (interpS (lem2 (lem2 b)) ((c , k) , n)))
                                (interpE (subst b e) c) =⟨ ap
                                        (λ h → natrec (interpE (subst b e0) c) h (interpE (subst b e) c))
                                          (λ= (λ x →
                                            λ= (λ y → lemma-c {nat :: τ :: Γ} {nat :: τ :: Γ'} e1 (lem2 (lem2 b)) ((c , y) , x)))) ⟩
                             natrec (interpE (subst b e0) c)
                                 (λ n k → interpE (subst (lem2 (lem2 b)) e1) ((c , k) , n))
                                 (interpE (subst b e) c)
                                                 ∎

  lemma-c {Γ} {Γ'} {ρ ⇒ τ} (lam e) b c = interpE (lam e) (interpS b c) =⟨ Refl ⟩
                        (λ x → interpE e (interpS b c , x)) =⟨ λ= (λ x → ap (λ h → interpE e h) (lemma-c-lemma x b c)) ⟩
                        (λ x → interpE e (interpS (lem2 b) (c , x))) =⟨ λ= (λ x → lemma-c {ρ :: Γ} {ρ :: Γ'} e (lem2 b) (c , x)) ⟩
                        (λ x → interpE (subst (lem2 b) e) (c , x)) ∎
  lemma-c (app e1 e2) b c = interpE (app e1 e2) (interpS b c)                     =⟨ Refl ⟩
                            interpE e1 (interpS b c) (interpE e2 (interpS b c))   =⟨ ap (λ f → f (interpE e2 (interpS b c))) (lemma-c e1 b c) ⟩
                            interpE (subst b e1) c (interpE e2 (interpS b c))     =⟨ ap (λ f → interpE (subst b e1) c f) (lemma-c e2 b c) ⟩
                            interpE (subst b e1) c (interpE (subst b e2) c)       ∎

  -- Soundness: if e >> e' then interp e == interp e'
  sound : ∀ {τ} (e e' : [] |- τ) → e >> e' → (interpE e <>) == (interpE e' <>)
  sound (var x) d ()
  sound z d ()
  sound (suc e) .(suc e') (suc-steps .e e' p) = ap S (sound e e' p)
  sound (rec e e0 e1) .(rec e' e0 e1) (rec-steps .e e' .e0 .e1 p) = ap (natrec (interpE e0 <>) (λ n k → interpE e1 ((<> , k) , n))) (sound e e' p)
  sound (rec .z .d e1) d (rec-steps-z e .d .e1) = Refl
  sound (rec .(suc e) e0 e1) .(subst (lem4 e (rec e e0 e1)) e1) (rec-steps-suc e .e0 .e1 x) = lemma-c e1 (lem4 e (rec e e0 e1)) <>
  sound (lam x) d ()
  sound (app e1 e2) .(app e1' e2) (app-steps .e1 e1' .e2 p) = ap (λ d → d (interpE e2 <>)) (sound e1 e1' p)
  sound (app e1 e2) .(app e1 e2') (app-steps-2 .e1 .e2 e2' x p) = ap (λ d → interpE e1 <> d) (sound e2 e2' p)
  sound (app .(lam e1) e2) .(subst (lem3 e2) e1) (app-steps-3 e1 .e2) = lemma-c e1 (lem3 e2) <>

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import Generics.Prelude hiding (lookup)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc
import Generics.Helpers as Helpers

module Generics.Constructions.Recursion
  {P I ℓ} {A : Indexed P I ℓ}
  (H : HasDesc A) (open HasDesc H)
  {p c} (Pr : Pred′ I (λ i → A′ (p , i) → Set c))
  where

private
  variable
    V : ExTele P
    i : ⟦ I ⟧tel p
    v : ⟦ V ⟧tel p

Pr′ : A′ (p , i) → Set c
Pr′ {i} = unpred′ I _ Pr i

Below : (x : A′ (p , i)) → Acc x → Setω

BelowIndArg : (C : ConDesc P V I)
              (x : ⟦ C ⟧IndArg A′ (p , v))
            → AllIndArgω Acc C x
            → Setω
BelowIndArg (var _) x = Below x
BelowIndArg (π ai S C) x a = ∀ s → BelowIndArg C (app< ai > x s) (a s)
BelowIndArg (A ⊗ B) (x , y) (ax , ay)
  = BelowIndArg A x ax ×ω BelowIndArg B y ay

BelowCon : (C : ConDesc P V I)
           (x : ⟦ C ⟧Con A′ (p , v , i))
         → AllConω Acc C x
         → Setω
BelowCon (var _) x _ = ⊤ω
BelowCon (π ai S C) (s , x) = BelowCon C x
BelowCon (A ⊗ B) (f , x) (af , ax)
  =  BelowIndArg A f af
  ×ω BelowCon B x ax

Below x (acc a) with split x
... | (k , x) = BelowCon _ x a

module _ (f : ∀ {i} (x : A′ (p , i)) (a : Acc x) → Below x a → Pr′ x) where

  below : (x : A′ (p , i)) (a : Acc x) → Below x a
  below x (acc a) with split x
  ... | (k , x) = belowCon _ x a
    where
      belowIndArg : (C : ConDesc P V I)
                    (x : ⟦ C ⟧IndArg A′ (p , v))
                    (a : AllIndArgω Acc C x)
                  → BelowIndArg C x a
      belowIndArg (var _) x a = below x a
      belowIndArg (π ai _ C) x a s =
        belowIndArg C (app< ai > x s) (a s)
      belowIndArg (A ⊗ B) (x , y) (ax , ay)
        = belowIndArg A x ax
        , belowIndArg B y ay

      belowCon : (C : ConDesc P V I)
                 (x : ⟦ C ⟧Con A′ (p , v , i))
                 (a : AllConω Acc C x)
               → BelowCon C x a
      belowCon (var _) _ _ = tt
      belowCon (π _ _ C) (_ , x) a = belowCon C x a
      belowCon (A ⊗ B) (f , x) (af , ax)
        = belowIndArg A f af
        , belowCon B x ax

  rec : (x : A′ (p , i)) → Pr′ x
  rec x = f x (wf x) (below x (wf x))

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
module Type.WellOrdering where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Type
open import Type.Dependent

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level

-- Types with terms that are well-founded trees.
-- Constructs types that are similar to some kind of tree.
-- The first parameter is the index for a constructor.
-- The second parameter is the arity for each constructor.
--
-- A type able to describe all non-dependent inductively defined data types assuming there are some previously defined types.
-- When described like this, the parameters should be interpreted as the following:
-- • The first parameter `A` indicates the "number" of branches based on another type's "cardinality" and should also contain the data for every branch.
-- • The second parameter `B` is used when the type to be defined refers to itself.
-- Examples:
--   open import Data
--   open import Data.Boolean
--
--   module _ (L R : Type{Lvl.𝟎}) where
--     E : Type{Lvl.𝟎}
--     E = W{A = Σ(Bool)(if_then R else L)}(const Empty) -- Either type using W.
--     l : L → E                                         -- Left branch introduction.
--     l x = sup (intro 𝐹 x) empty
--     r : R → E                                         -- Rght branch introduction.
--     r x = sup (intro 𝑇 x) empty
--
--   N = W{A = Bool}(if_then Unit{Lvl.𝟎} else Empty{Lvl.𝟎}) -- Natural numbers using W.
--   z : N                                                  -- Zero branch introduction.
--   z = sup 𝐹 empty
--   z' : _ → N                                             -- Zero branch introduction (defined like this because empty functions are not unique (from no function extensionality) resulting in more than one zero for this definition of the natural numbers).
--   z' empty = sup 𝐹 empty
--   s : N → N                                              -- Successor branch introduction.
--   s n = sup 𝑇 (\{<> → n})
--   e : ∀{P : N → Type{Lvl.𝟎}} → (∀{empty} → P(z empty)) → (∀{n} → P(n) → P(s n)) → (∀{n} → P(n)) -- TODO: Is this a correct eliminator? Note: It does not pass the termination checker
--   e pz ps {sup 𝐹 b} = pz
--   e pz ps {sup 𝑇 b} = ps (e pz (\{n} → ps{n}) {b <>})
record W {A : Type{ℓ₁}} (B : A → Type{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂} where
  inductive
  eta-equality
  constructor sup
  field
    a : A
    b : B(a) → W(B)

-- TODO: Is the type of this eliminator correct?
-- W-elim : ∀{A : Type{ℓ₁}}{B : A → Type{ℓ₂}}{P : W(B) → Type{ℓ}} → (∀{a : A}{b : B(a) → W(B)} → (∀{ba : B(a)} → P(b(ba))) → P(sup a b)) → (∀{w : W(B)} → P(w))

-- TODO: Note that this is essentially Sets.IterativeSet
V : ∀{ℓ₁} → Type{Lvl.𝐒(ℓ₁)}
V {ℓ₁} = W {A = Type{ℓ₁}} id

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:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category using (Category)

-- Defines the following properties of a Category:
-- Cartesian -- a Cartesian category is a category with all products

--  (for the induced Monoidal structure, see Cartesian.Monoidal)

module Categories.Category.Cartesian {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level using (levelOfTerm)
open import Data.Nat using (ℕ; zero; suc)

open Category 𝒞
open HomReasoning

open import Categories.Category.BinaryProducts 𝒞 using (BinaryProducts; module BinaryProducts)
open import Categories.Object.Terminal 𝒞 using (Terminal)

private
  variable
    A B C D W X Y Z : Obj
    f f′ g g′ h i : A ⇒ B

-- Cartesian monoidal category
record Cartesian : Set (levelOfTerm 𝒞) where
  field
    terminal : Terminal
    products : BinaryProducts
  open BinaryProducts products using (_×_)

  power : Obj → ℕ → Obj
  power A 0 = Terminal.⊤ terminal
  power A 1 = A
  power A (suc (suc n)) = A × power A (suc n)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2014-11-25, variant of Issue 1366

{-# OPTIONS --copatterns #-}

open import Common.Prelude using (Nat; zero; suc; Unit; unit)

data Vec (A : Set) : Nat → Set where
   []  : Vec A zero
   _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

-- Singleton type

data Sg {A : Set} (x : A) : Set where
  sg : Sg x

-- Generalizing Unit → Nat

record DNat : Set₁ where
  field
    D     : Set
    force : D → Nat
open DNat

nonNil : ∀ {n} → Vec Unit n → Nat
nonNil []       = zero
nonNil (i ∷ is) = suc (force f i) where
  f : DNat
  D     f      = Unit
  force f unit = zero

g : ∀ {n} {v : Vec Unit n} → Sg (nonNil v) → Sg v
g sg = sg

one : Sg (suc zero)
one = sg

test : Sg (unit ∷ [])
test = g one


text:
module Ints where

open import Nats public
  using (ℕ; zero; _∸_)
  renaming (suc to nsuc; _+_ to _:+:_; _*_ to _:*:_)
open import Agda.Builtin.Int public
  renaming (Int to ℤ; negsuc to -[1+_]; pos to +_)

infix  8 -_
-- infixl 7 _*_ _⊓_
infixl 6 _+_ _-_ _⊖_

∣_∣ : ℤ → ℕ
∣ + n      ∣ = n
∣ -[1+ n ] ∣ = nsuc n

-_ : ℤ → ℤ
- (+ nsuc n) = -[1+ n ]
- (+ zero)   = + zero
- -[1+ n ]   = + nsuc n

_⊖_ : ℕ → ℕ → ℤ
m      ⊖ zero   = + m
zero   ⊖ nsuc n = -[1+ n ]
nsuc m ⊖ nsuc n = m ⊖ n

_+_ : ℤ → ℤ → ℤ
-[1+ m ] + -[1+ n ] = -[1+ nsuc (m :+: n) ]
-[1+ m ] + +    n   = n ⊖ nsuc m
+    m   + -[1+ n ] = m ⊖ nsuc n
+    m   + +    n   = + (m :+: n)

_-_ : ℤ → ℤ → ℤ
i - j = i + - j

suc : ℤ → ℤ
suc i = + 1 + i