text:
module Numeral.Natural.Oper.Proofs where

import Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Induction
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
import      Structure.Operator.Names as Names
open import Structure.Relator.Properties
open import Syntax.Transitivity

-- TODO: For old code
open import Numeral.Natural.Proofs public
open import Numeral.Natural.Oper.Proofs.Rewrite public

instance
  [+]-identityₗ : Identityₗ(_+_)(0)
  Identityₗ.proof([+]-identityₗ) = [+]-baseₗ

instance
  [+]-identityᵣ : Identityᵣ(_+_)(0)
  Identityᵣ.proof([+]-identityᵣ) {x} = ℕ-elim [≡]-intro (x ↦ [≡]-with(𝐒) {x + 𝟎}{x}) x

instance
  [+]-identity : Identity (_+_) (0)
  [+]-identity = intro

instance
  [+]-associativity : Associativity(_+_)
  Associativity.proof([+]-associativity) {x}{y}{z} = ℕ-elim [≡]-intro (i ↦ [≡]-with(𝐒) {(x + y) + i} {x + (y + i)}) z

instance
  [+]-commutativity : Commutativity (_+_)
  Commutativity.proof([+]-commutativity) {x}{y} = ℕ-elim base next y where
    base = identityᵣ(_+_)(𝟎) 🝖 symmetry(_≡_) (identityₗ(_+_)(𝟎))
    next = \i eq → ([≡]-with(𝐒) {x + i}{i + x} eq) 🝖 symmetry(_≡_) ([+]-stepₗ {i}{x})

[+1]-and-[𝐒] : ∀{x : ℕ} → (x + 1 ≡ 𝐒(x))
[+1]-and-[𝐒] {x} = [≡]-intro

[1+]-and-[𝐒] : ∀{x : ℕ} → (1 + x ≡ 𝐒(x))
[1+]-and-[𝐒] {x} = [+1]-and-[𝐒] {x} 🝖 commutativity(_+_) {x}{1}

[⋅]-absorberₗ-raw : Names.Absorberₗ(_⋅_)(0)
[⋅]-absorberₗ-raw {x} = ℕ-elim [≡]-intro (\i → [≡]-with(0 +_) {0 ⋅ i}{0}) x
{-# REWRITE [⋅]-absorberₗ-raw #-}
instance
  [⋅]-absorberₗ : Absorberₗ(_⋅_)(0)
  Absorberₗ.proof([⋅]-absorberₗ) {x} = [⋅]-absorberₗ-raw {x}

instance
  [⋅]-absorberᵣ : Absorberᵣ(_⋅_)(0)
  Absorberᵣ.proof([⋅]-absorberᵣ) {x} = [≡]-intro

instance
  [⋅]-absorber : Absorber(_⋅_)(0)
  [⋅]-absorber = intro

[⋅]-identityₗ-raw : Names.Identityₗ(_⋅_)(1)
[⋅]-identityₗ-raw {x} = ℕ-elim [≡]-intro (\i eq → (commutativity(_+_) {1} {1 ⋅ i}) 🝖 ([≡]-with(𝐒) {_}{i} eq)) x
{-# REWRITE [⋅]-identityₗ-raw #-}
instance
  [⋅]-identityₗ : Identityₗ(_⋅_)(1)
  Identityₗ.proof([⋅]-identityₗ) {x} = [⋅]-identityₗ-raw {x}

instance
  [⋅]-identityᵣ : Identityᵣ(_⋅_)(1)
  Identityᵣ.proof([⋅]-identityᵣ) = [≡]-intro

instance
  [⋅]-identity : Identity(_⋅_)(1)
  [⋅]-identity = intro

instance
  [⋅][+]-distributivityᵣ : Distributivityᵣ(_⋅_)(_+_)
  Distributivityᵣ.proof([⋅][+]-distributivityᵣ) {x}{y}{z} = ℕ-elim [≡]-intro next z where
    next : ∀(z : ℕ) → ((x + y) ⋅ z) ≡ ((x ⋅ z) + (y ⋅ z)) → ((x + y) ⋅ 𝐒(z)) ≡ ((x ⋅ 𝐒(z)) + (y ⋅ 𝐒(z)))
    next z proof = ([≡]-with((x + y) +_) proof) 🝖 (One.associate-commute4 {a = x}{y}{x ⋅ z}{y ⋅ z} (commutativity(_+_){x = y}))

[⋅]-with-[𝐒]ₗ : ∀{x y} → (𝐒(x) ⋅ y ≡ (x ⋅ y) + y)
[⋅]-with-[𝐒]ₗ {x}{y} = (distributivityᵣ(_⋅_)(_+_) {x}{1}{y}) 🝖 ([≡]-with(expr ↦ (x ⋅ y) + expr) ([⋅]-identityₗ-raw {y}))

[⋅]-with-[𝐒]ᵣ : ∀{x y} → (x ⋅ 𝐒(y) ≡ x + (x ⋅ y))
[⋅]-with-[𝐒]ᵣ = [≡]-intro

instance
  [⋅][+]-distributivityₗ : Distributivityₗ(_⋅_)(_+_)
  Distributivityₗ.proof([⋅][+]-distributivityₗ) {x}{y}{z} = p{x}{y}{z} where
    p : Names.Distributivityₗ(_⋅_)(_+_)
    p {𝟎}   {y}   {z}   = [≡]-intro
    p {𝐒 x} {𝟎}   {z}   = [≡]-intro
    p {𝐒 x} {𝐒 y} {𝟎}   = [≡]-intro
    p {𝐒 x} {𝐒 y} {𝐒 z} = [≡]-with(𝐒 ∘ 𝐒) $
      x + (x + (𝐒 x ⋅ (y + z)))         🝖[ _≡_ ]-[ [≡]-with((x +_) ∘ (x +_)) (p {𝐒 x} {y} {z}) ]
      x + (x + ((𝐒 x ⋅ y) + (𝐒 x ⋅ z))) 🝖[ _≡_ ]-[ [≡]-with(x +_) (One.commuteₗ-assocᵣ ⦃ comm = intro(\{x y} → commutativity(_+_) {x}{y}) ⦄ {a = x}{b = 𝐒 x ⋅ y}{c = 𝐒 x ⋅ z}) ]
      x + ((𝐒 x ⋅ y) + (x + (𝐒 x ⋅ z))) 🝖[ _≡_ ]-[ associativity(_+_) {x = x}{y = 𝐒 x ⋅ y} ]-sym
      (x + (𝐒 x ⋅ y)) + (x + (𝐒 x ⋅ z)) 🝖-end

instance
  [⋅]-associativity : Associativity (_⋅_)
  Associativity.proof([⋅]-associativity) {x}{y}{z} = p{x}{y}{z} where
    p : Names.Associativity(_⋅_)
    p {𝟎}   {𝟎}   {𝟎}   = [≡]-intro
    p {𝟎}   {𝟎}   {𝐒 z} = [≡]-intro
    p {𝟎}   {𝐒 y} {𝟎}   = [≡]-intro
    p {𝟎}   {𝐒 y} {𝐒 z} = [≡]-intro
    p {𝐒 x} {𝟎}   {𝟎}   = [≡]-intro
    p {𝐒 x} {𝟎}   {𝐒 z} = [≡]-intro
    p {𝐒 x} {𝐒 y} {𝟎}   = [≡]-intro
    p {𝐒 x} {𝐒 y} {𝐒 z} = [≡]-with(𝐒) $
      (x + (𝐒 x ⋅ y)) + (𝐒(x + 𝐒 x ⋅ y) ⋅ z)  🝖[ _≡_ ]-[ associativity(_+_) {x = x}{y = 𝐒 x ⋅ y} ]
      x + ((𝐒 x ⋅ y) + (𝐒(x + 𝐒 x ⋅ y) ⋅ z))  🝖[ _≡_ ]-[]
      x + ((𝐒 x ⋅ y) + ((𝐒 x + 𝐒 x ⋅ y) ⋅ z)) 🝖[ _≡_ ]-[]
      x + ((𝐒 x ⋅ y) + ((𝐒 x ⋅ 𝐒 y) ⋅ z))     🝖[ _≡_ ]-[ [≡]-with(expr ↦ x + ((𝐒 x ⋅ y) + expr)) (p{𝐒 x}{𝐒 y}{z}) ]
      x + ((𝐒 x ⋅ y) + (𝐒 x ⋅ (𝐒 y ⋅ z)))     🝖[ _≡_ ]-[ [≡]-with(x +_) (distributivityₗ(_⋅_)(_+_) {x = 𝐒 x}{y = y}{z = 𝐒 y ⋅ z}) ]-sym
      x + (𝐒 x ⋅ (y + (𝐒 y ⋅ z)))             🝖-end

instance
  [⋅]-commutativity : Commutativity (_⋅_)
  Commutativity.proof([⋅]-commutativity) {x}{y} = p {x}{y} where
    p : Names.Commutativity(_⋅_)
    p {𝟎} {𝟎} = [≡]-intro
    p {𝟎} {𝐒 y} = [≡]-intro
    p {𝐒 x} {𝟎} = [≡]-intro
    p {𝐒 x} {𝐒 y} = [≡]-with(𝐒) $
      x + (𝐒 x ⋅ y)     🝖-[ [≡]-with(x +_) ([⋅]-with-[𝐒]ₗ {x}{y}) ]
      x + ((x ⋅ y) + y) 🝖-[ [≡]-with(x +_) (commutativity(_+_) {x ⋅ y}{y}) ]
      x + (y + (x ⋅ y)) 🝖-[ One.commuteₗ-assocᵣ ⦃ comm = intro(\{x y} → commutativity(_+_) {x}{y}) ⦄ {a = x}{b = y}{c = x ⋅ y} ]
      y + (x + (x ⋅ y)) 🝖-[ [≡]-with(expr ↦ y + (x + expr)) (p {x} {y}) ]
      y + (x + (y ⋅ x)) 🝖-[ [≡]-with(y +_) (commutativity(_+_) {x}{y ⋅ x}) ]
      y + ((y ⋅ x) + x) 🝖-[ [≡]-with(y +_) ([⋅]-with-[𝐒]ₗ {y}{x}) ]-sym
      y + (𝐒 y ⋅ x)     🝖-end

[𝐏][𝐒]-inverses : ∀{n} → (𝐏(𝐒(n)) ≡ n)
[𝐏][𝐒]-inverses = [≡]-intro

[+]-sum-is-0 : ∀{a b} → (a + b ≡ 0) → (a ≡ 0)∧(b ≡ 0)
[+]-sum-is-0 {a}{b} proof = [∧]-intro (l{a}{b} proof) r where
  l = \{a b} → ℕ-elim{T = \b → (a + b ≡ 0) → (a ≡ 0)} id (\_ p → p ∘ [≡]-with(𝐏)) b
  r = l{b}{a} (commutativity(_+_) {b}{a} 🝖 proof)

[⋅]-product-is-1ₗ : ∀{a b} → (a ⋅ b ≡ 1) → (a ≡ 1)
[⋅]-product-is-1ₗ {𝟎}   {_}   p = p
[⋅]-product-is-1ₗ {𝐒 a} {𝟎}   ()
[⋅]-product-is-1ₗ {𝐒 a} {𝐒 b} p = [≡]-with(𝐒) ([∧]-elimₗ ([+]-sum-is-0 (injective(𝐒) p)))

[⋅]-product-is-1ᵣ : ∀{a b} → (a ⋅ b ≡ 1) → (b ≡ 1)
[⋅]-product-is-1ᵣ {a}{b} = [⋅]-product-is-1ₗ {b}{a} ∘ (commutativity(_⋅_) {b}{a} 🝖_)

[⋅]-product-is-0 : ∀{a b} → (a ⋅ b ≡ 0) → ((a ≡ 0)∨(b ≡ 0))
[⋅]-product-is-0 {_}   {0}    _   = [∨]-introᵣ [≡]-intro
[⋅]-product-is-0 {0}   {𝐒(_)} _   = [∨]-introₗ [≡]-intro
[⋅]-product-is-0 {𝐒(a)}{𝐒(b)} ab0 with () ← [𝐒]-not-0 {(𝐒(a) ⋅ b) + a} (commutativity(_+_) {𝐒(a) ⋅ b}{𝐒(a)} 🝖 ab0)

[⋅]-product-is-positive : ∀{a b n} → (a ⋅ b ≡ 𝐒(n)) → (∃(n₁ ↦ a ≡ 𝐒(n₁)) ∧ ∃(n₂ ↦ b ≡ 𝐒(n₂)))
[⋅]-product-is-positive {_}   {0}    p with () ← [𝐒]-not-0 (symmetry(_≡_) p)
[⋅]-product-is-positive {0}   {𝐒(_)} p with () ← [𝐒]-not-0 (symmetry(_≡_) p)
[⋅]-product-is-positive {𝐒(a)}{𝐒(b)} p = [∧]-intro ([∃]-intro a) ([∃]-intro b)

instance
  [+]-cancellationᵣ : Cancellationᵣ(_+_)
  Cancellationᵣ.proof([+]-cancellationᵣ) {a}{x}{y} = ℕ-elim{T = \a → (x + a ≡ y + a) → (x ≡ y)} id (\_ → _∘ injective(𝐒)) a

instance
  [+]-cancellationₗ : Cancellationₗ(_+_)
  Cancellationₗ.proof([+]-cancellationₗ) {a}{x}{y} = cancellationᵣ(_+_) ∘ One.commuteBothTemp {a₁ = a}{x}{a}{y}

[^]-of-𝟎ₗ : ∀{x} → (𝟎 ^ 𝐒(x) ≡ 𝟎)
[^]-of-𝟎ₗ = [≡]-intro

[^]-of-𝟏ₗ : ∀{x} → (𝟏 ^ x ≡ 𝟏)
[^]-of-𝟏ₗ {𝟎}   = [≡]-intro
[^]-of-𝟏ₗ {𝐒 x} = [^]-of-𝟏ₗ {x}

[−₀]-absorberₗ-raw : ∀{x} → ((𝟎 −₀ x) ≡ 𝟎)
[−₀]-absorberₗ-raw {n} = ℕ-elim{T = \n → ((𝟎 −₀ n) ≡ 𝟎)} [≡]-intro (\_ _ → [≡]-intro) n
{-# REWRITE [−₀]-absorberₗ-raw #-}
instance
  [−₀]-absorberₗ : Absorberₗ (_−₀_) (𝟎)
  Absorberₗ.proof([−₀]-absorberₗ) {x} = [−₀]-absorberₗ-raw {x}

instance
  [−₀]-identityᵣ : Identityᵣ (_−₀_) (𝟎)
  Identityᵣ.proof([−₀]-identityᵣ) {x} = [≡]-intro

[−₀]-self : ∀{x} → ((x −₀ x) ≡ 𝟎)
[−₀]-self {n} = ℕ-elim{T = \n → ((n −₀ n) ≡ 𝟎)} [≡]-intro (\_ p → p) n
{-# REWRITE [−₀]-self #-}

[−₀]-with-[𝐒]ᵣ : ∀{x y} → ((x −₀ 𝐒(y)) ≡ 𝐏(x −₀ y))
[−₀]-with-[𝐒]ᵣ {𝟎} {𝟎}     = [≡]-intro
[−₀]-with-[𝐒]ᵣ {𝟎} {𝐒 y}   = [≡]-intro
[−₀]-with-[𝐒]ᵣ {𝐒 x} {𝟎}   = [≡]-intro
[−₀]-with-[𝐒]ᵣ {𝐒 x} {𝐒 y} = [−₀]-with-[𝐒]ᵣ {x} {y}

[−₀][−₀]-to-[−₀][+] : ∀{x y z} → ((x −₀ y) −₀ z ≡ x −₀ (y + z))
[−₀][−₀]-to-[−₀][+] {x}{y}{𝟎} = [≡]-intro
[−₀][−₀]-to-[−₀][+] {x}{y}{𝐒 z} =
  (x −₀ y) −₀ 𝐒(z) 🝖[ _≡_ ]-[ [−₀]-with-[𝐒]ᵣ {x −₀ y}{z} ]
  𝐏((x −₀ y) −₀ z) 🝖[ _≡_ ]-[ congruence₁(𝐏) ([−₀][−₀]-to-[−₀][+] {x}{y}{z}) ]
  𝐏(x −₀ (y + z))  🝖[ _≡_ ]-[ [−₀]-with-[𝐒]ᵣ {x}{y + z} ]-sym
  x −₀ 𝐒(y + z)    🝖[ _≡_ ]-[]
  x −₀ (y + 𝐒(z))  🝖-end

[−₀]ₗ[+]ᵣ-nullify : ∀{x y} → ((x + y) −₀ y ≡ x)
[−₀]ₗ[+]ᵣ-nullify{𝟎}   {𝟎}    = [≡]-intro
[−₀]ₗ[+]ᵣ-nullify{𝟎}   {𝐒(y)} = [≡]-intro
[−₀]ₗ[+]ᵣ-nullify{𝐒(x)}{𝐒(y)} = [≡]-intro 🝖 ([−₀]ₗ[+]ᵣ-nullify{𝐒(x)}{y})
[−₀]ₗ[+]ᵣ-nullify{𝐒(x)}{𝟎}    = [≡]-intro
instance
  [+][−₀]-inverseOperatorᵣ : InverseOperatorᵣ(_+_)(_−₀_)
  InverseOperatorᵣ.proof [+][−₀]-inverseOperatorᵣ {x} {y} = [−₀]ₗ[+]ᵣ-nullify {x}{y}

[−₀]ₗ[+]ₗ-nullify : ∀{x y} → ((x + y) −₀ x ≡ y)
[−₀]ₗ[+]ₗ-nullify {x}{y} = [≡]-substitutionᵣ (commutativity(_+_) {y}{x}) {expr ↦ (expr −₀ x ≡ y)} ([−₀]ₗ[+]ᵣ-nullify {y}{x})

[−₀][+]ᵣ-nullify : ∀{x₁ x₂ y} → ((x₁ + y) −₀ (x₂ + y) ≡ x₁ −₀ x₂)
[−₀][+]ᵣ-nullify {_} {_} {𝟎}    = [≡]-intro
[−₀][+]ᵣ-nullify {x₁}{x₂}{𝐒(y)} = [−₀][+]ᵣ-nullify {x₁}{x₂}{y}

[−₀][+]ₗ-nullify : ∀{x y₁ y₂} → ((x + y₁) −₀ (x + y₂) ≡ y₁ −₀ y₂)
[−₀][+]ₗ-nullify {x}{y₁}{y₂} =
  [≡]-with-op(_−₀_) (commutativity(_+_) {x}{y₁}) (commutativity(_+_) {x}{y₂})
  🝖 [−₀][+]ᵣ-nullify{y₁}{y₂}{x}

[−₀]-cases : ∀{x y} → ((x −₀ y) + y ≡ x) ∨ (x −₀ y ≡ 𝟎)
[−₀]-cases {𝟎}   {𝟎}    = [∨]-introᵣ [≡]-intro
[−₀]-cases {𝟎}   {𝐒(_)} = [∨]-introᵣ [≡]-intro
[−₀]-cases {𝐒(_)}{𝟎}    = [∨]-introₗ [≡]-intro
[−₀]-cases {𝐒(x)}{𝐒(y)} with [−₀]-cases {x}{y}
... | [∨]-introₗ proof = [∨]-introₗ ([≡]-with(𝐒) (proof))
... | [∨]-introᵣ proof = [∨]-introᵣ proof

[−₀]-cases-commuted : ∀{x y} → (y + (x −₀ y) ≡ x) ∨ (x −₀ y ≡ 𝟎)
[−₀]-cases-commuted {x}{y} with [−₀]-cases{x}{y}
... | [∨]-introₗ proof = [∨]-introₗ (commutativity(_+_) {y}{x −₀ y} 🝖 proof)
... | [∨]-introᵣ proof = [∨]-introᵣ proof

[𝄩]-𝐒-cases : ∀{x y} → (𝐒(x 𝄩 y) ≡ 𝐒(x) 𝄩 y) ∨ (𝐒(x 𝄩 y) ≡ x 𝄩 𝐒(y))
[𝄩]-𝐒-cases {𝟎}   {𝟎}   = [∨]-introₗ [≡]-intro
[𝄩]-𝐒-cases {𝟎}   {𝐒 y} = [∨]-introᵣ [≡]-intro
[𝄩]-𝐒-cases {𝐒 x} {𝟎}   = [∨]-introₗ [≡]-intro
[𝄩]-𝐒-cases {𝐒 x} {𝐒 y} = [𝄩]-𝐒-cases {x}{y}

[𝄩]-identityₗ-raw : Names.Identityₗ(_𝄩_)(0)
[𝄩]-identityₗ-raw {𝟎}    = [≡]-intro
[𝄩]-identityₗ-raw {𝐒(_)} = [≡]-intro
{-# REWRITE [𝄩]-identityₗ-raw #-}
instance
  [𝄩]-identityₗ : Identityₗ(_𝄩_)(𝟎)
  Identityₗ.proof([𝄩]-identityₗ) {x} = [𝄩]-identityₗ-raw {x}

[𝄩]-identityᵣ-raw : Names.Identityᵣ (_𝄩_) (0)
[𝄩]-identityᵣ-raw {𝟎}    = [≡]-intro
[𝄩]-identityᵣ-raw {𝐒(_)} = [≡]-intro
{-# REWRITE [𝄩]-identityᵣ-raw #-}
instance
  [𝄩]-identityᵣ : Identityᵣ(_𝄩_)(𝟎)
  Identityᵣ.proof([𝄩]-identityᵣ) {x} = [𝄩]-identityᵣ-raw {x}

instance
  [𝄩]-identity : Identity(_𝄩_)(𝟎)
  [𝄩]-identity = intro

[𝄩]-self : ∀{x} → (x 𝄩 x ≡ 𝟎)
[𝄩]-self {𝟎}    = [≡]-intro
[𝄩]-self {𝐒(x)} = [𝄩]-self {x}
{-# REWRITE [𝄩]-self #-}

instance
  [𝄩]-inverseFunctionₗ : InverseFunctionₗ(_𝄩_) ⦃ [∃]-intro 𝟎 ⦄ (id)
  [𝄩]-inverseFunctionₗ = intro \{x} → [𝄩]-self {x}

instance
  [𝄩]-inverseFunctionᵣ : InverseFunctionᵣ(_𝄩_) ⦃ [∃]-intro 𝟎 ⦄ (id)
  [𝄩]-inverseFunctionᵣ = intro \{x} → [𝄩]-self {x}

instance
  [𝄩]-commutativity : Commutativity(_𝄩_)
  Commutativity.proof([𝄩]-commutativity) {x}{y} = p{x}{y} where
    p : Names.Commutativity (_𝄩_)
    p{𝟎}   {𝟎}    = [≡]-intro
    p{𝟎}   {𝐒(y)} = [≡]-intro
    p{𝐒(x)}{𝟎}    = [≡]-intro
    p{𝐒(x)}{𝐒(y)} = p{x}{y}

instance
  [+][𝄩]-inverseOperatorᵣ : InverseOperatorᵣ(_+_)(_𝄩_)
  InverseOperatorᵣ.proof [+][𝄩]-inverseOperatorᵣ {x}{y} = p{x}{y} where
    p : ∀{x y} → ((x + y) 𝄩 y ≡ x)
    p{𝟎}   {𝟎}    = [≡]-intro
    p{𝟎}   {𝐒(y)} = [≡]-intro
    p{𝐒(x)}{𝐒(y)} = [≡]-intro 🝖 (p{𝐒(x)}{y})
    p{𝐒(x)}{𝟎}    = [≡]-intro

instance
  [swap+][𝄩]-inverseOperatorᵣ : InverseOperatorᵣ(swap(_+_))(_𝄩_)
  InverseOperatorᵣ.proof [swap+][𝄩]-inverseOperatorᵣ {x}{y} = congruence₂ₗ(_𝄩_)(y) (commutativity(_+_) {y}{x}) 🝖 inverseOperᵣ(_+_)(_𝄩_) {x}{y}

instance
  [swap+][𝄩]-inverseOperatorₗ : InverseOperatorₗ(swap(_+_))(_𝄩_)
  InverseOperatorₗ.proof [swap+][𝄩]-inverseOperatorₗ {x}{y} = commutativity(_𝄩_) {x}{y + x} 🝖 inverseOperᵣ(_+_)(_𝄩_) {y}{x}

instance
  [+][𝄩]-inverseOperatorₗ : InverseOperatorₗ(_+_)(_𝄩_)
  InverseOperatorₗ.proof [+][𝄩]-inverseOperatorₗ {x}{y} = commutativity(_𝄩_) {x}{x + y} 🝖 inverseOperᵣ(swap(_+_))(_𝄩_) {y}{x}

[𝄩]-with-[+]ᵣ : ∀{x y z} → ((x + z) 𝄩 (y + z) ≡ x 𝄩 y)
[𝄩]-with-[+]ᵣ {𝟎}   {𝟎}   {𝟎}    = [≡]-intro
[𝄩]-with-[+]ᵣ {𝟎}   {𝐒(y)}{𝟎}    = [≡]-intro
[𝄩]-with-[+]ᵣ {𝟎}   {𝟎}   {𝐒(z)} = [≡]-intro
[𝄩]-with-[+]ᵣ {𝟎}   {𝐒(y)}{𝐒(z)} = inverseOperₗ(swap(_+_))(_𝄩_) {z}{_}
[𝄩]-with-[+]ᵣ {𝐒(x)}{𝟎}   {𝟎}    = [≡]-intro
[𝄩]-with-[+]ᵣ {𝐒(x)}{𝐒(y)}{𝟎}    = [≡]-intro
[𝄩]-with-[+]ᵣ {𝐒(x)}{𝟎}   {𝐒(z)} = inverseOperᵣ(_+_)(_𝄩_) {𝐒(x)}{z}
[𝄩]-with-[+]ᵣ {𝐒(x)}{𝐒(y)}{𝐒(z)} = [𝄩]-with-[+]ᵣ {𝐒(x)}{𝐒(y)}{z}

[𝄩]-with-[+]ₗ : ∀{x y z} → ((z + x) 𝄩 (z + y) ≡ x 𝄩 y)
[𝄩]-with-[+]ₗ {𝟎}   {𝟎}   {𝟎}    = [≡]-intro
[𝄩]-with-[+]ₗ {𝟎}   {𝐒(y)}{𝟎}    = [≡]-intro
[𝄩]-with-[+]ₗ {𝟎}   {𝟎}   {𝐒(z)} = [≡]-intro
[𝄩]-with-[+]ₗ {𝟎}   {𝐒(y)}{𝐒(z)} = inverseOperₗ(_+_)(_𝄩_) {z}{𝐒(y)}
[𝄩]-with-[+]ₗ {𝐒(x)}{𝟎}   {𝟎}    = [≡]-intro
[𝄩]-with-[+]ₗ {𝐒(x)}{𝐒(y)}{𝟎}    = [≡]-intro
[𝄩]-with-[+]ₗ {𝐒(x)}{𝟎}   {𝐒(z)} = inverseOperᵣ(swap(_+_))(_𝄩_) {𝐒(x)}{z}
[𝄩]-with-[+]ₗ {𝐒(x)}{𝐒(y)}{𝐒(z)} = [𝄩]-with-[+]ₗ {𝐒(x)}{𝐒(y)}{z}

[𝄩]-equality : ∀{x y} → (x 𝄩 y ≡ 𝟎) → (x ≡ y)
[𝄩]-equality {𝟎}   {𝟎}    [≡]-intro = [≡]-intro
[𝄩]-equality {𝟎}   {𝐒(y)} ()
[𝄩]-equality {𝐒(x)}{𝟎}    ()
[𝄩]-equality {𝐒(x)}{𝐒(y)} proof     = [≡]-with(𝐒) ([𝄩]-equality {x}{y} proof)

instance
  [⋅][𝄩]-distributivityᵣ : Distributivityᵣ(_⋅_)(_𝄩_)
  Distributivityᵣ.proof [⋅][𝄩]-distributivityᵣ {x}{y}{z} = p{x}{y}{z} where
    p : Names.Distributivityᵣ(_⋅_)(_𝄩_)
    p {𝟎} {𝟎} {z} = [≡]-intro
    p {𝟎} {𝐒 y} {z} = [≡]-intro
    p {𝐒 x} {𝟎} {z} = [≡]-intro
    p {𝐒 x} {𝐒 y} {z} =
      (𝐒(x) 𝄩 𝐒(y)) ⋅ z             🝖[ _≡_ ]-[]
      (x 𝄩 y) ⋅ z                   🝖[ _≡_ ]-[ p{x}{y}{z} ]
      (x ⋅ z) 𝄩 (y ⋅ z)             🝖[ _≡_ ]-[ [𝄩]-with-[+]ᵣ {x ⋅ z}{y ⋅ z}{z} ]-sym
      ((x ⋅ z) + z) 𝄩 ((y ⋅ z) + z) 🝖[ _≡_ ]-[ congruence₂(_𝄩_) ([⋅]-with-[𝐒]ₗ {x}{z}) ([⋅]-with-[𝐒]ₗ {y}{z}) ]-sym
      (𝐒(x) ⋅ z) 𝄩 (𝐒(y) ⋅ z)       🝖-end

instance
  [⋅][𝄩]-distributivityₗ : Distributivityₗ(_⋅_)(_𝄩_)
  Distributivityₗ.proof [⋅][𝄩]-distributivityₗ {x}{y}{z} =
    x ⋅ (y 𝄩 z)       🝖[ _≡_ ]-[ commutativity(_⋅_) {x}{y 𝄩 z} ]
    (y 𝄩 z) ⋅ x       🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_𝄩_) {y}{z}{x} ]
    (y ⋅ x) 𝄩 (z ⋅ x) 🝖[ _≡_ ]-[ congruence₂(_𝄩_) (commutativity(_⋅_) {y}{x}) (commutativity(_⋅_) {z}{x}) ]
    (x ⋅ y) 𝄩 (x ⋅ z) 🝖-end

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a single relation
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Reasoning.Base.Single
  {a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
  (refl : Reflexive _∼_) (trans : Transitive _∼_)
  where

open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

infix  4 _IsRelatedTo_
infix  3 _∎
infixr 2 _∼⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix  1 begin_

-- This seemingly unnecessary type is used to make it possible to
-- infer arguments even if the underlying equality evaluates.

data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ) where
  relTo : (x∼y : x ∼ y) → x IsRelatedTo y

begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
begin relTo x∼y = x∼y

_∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_ ≡⟨ P.refl ⟩ x∼z = x∼z

_≡˘⟨_⟩_ : ∀ x {y z} → y ≡ x → y IsRelatedTo z → x IsRelatedTo z
_ ≡˘⟨ P.refl ⟩ x∼z = x∼z

_≡⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x∼y = _ ≡⟨ P.refl ⟩ x∼y

_∎ : ∀ x → x IsRelatedTo x
_∎ _ = relTo refl

ext: agda


text:
module PatternSynonymUnderapplied where

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

pattern suc' x = suc x

f : Nat -> Nat
f zero = zero
f suc' = zero

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

-- Normalization by Evaluation for Graded Call-By-Push-Value.

module GradedCBPV where

-- Imports from the Agda standard library.

open import Library hiding (_×̇_)
pattern here! = here refl

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

open import ProMonoid as _

-- We postulate an effect algebra, a pre-ordered monoid

postulate
  effAlg : ProMonoid lzero lzero lzero

open ProMonoid effAlg public
  renaming
    ( Carrier to Eff
    ; _∙_     to infixl 6 _+_
    ; ε       to ∅
    ; _≼_     to _≤_
    ; _≈_     to _=E_
    )

-- postulate
--   +-unitˡ : ∅ + e ≡ e
--   +-unitʳ : e + ∅ ≡ e
--   +-assoc : (e₁ + e₂) + e₃ ≡ e₁ + (e₂ + e₃)
--   +-supʳ  : sup es + e ≡ sup λ i → es i + e
--   sup-k   : sup {I = I} (λ _ → e) ≡ e

-- {-# REWRITE +-unitˡ +-unitʳ +-assoc +-supʳ sup-k #-}

-- We postulate a set of generic value types.
-- There are no operations defined on these types, thus,
-- they play the type of (universal) type variables.

postulate
  Base : Set

variable
  o : Base

-- Variants (Σ) (and records (Π), resp.) can in principle have any number of
-- constructors (fields, resp.), including infinitely one.
-- In general, the constructor (field, resp.) names are given by a set I.
-- However, I : Set would make syntax already a big type, living in Set₁.
-- To keep it in Set₀, we only consider variants (records) with finitely
-- many constructors (fields), thus, I : ℕ.
-- Branching over I is then realized as functions out of El I, where
-- El I = { i | i < I} = Fin I.

set = ℕ
El  = Fin

-- Let I range over arities (constructor/field sets) and i over
-- constructor/field names.

variable
  I : set
  i : El I

variable
  e e' e₁ e₂ e₃ : Eff
  es : El I → Eff

-- The types of CBPV are classified into value types P : Ty⁺ which we
-- refer to as positive types, and computation types N : Ty⁻ which we
-- refer to as negative types.

mutual

  -- Value types

  data Ty⁺ : Set where
    base  : (o : Base) → Ty⁺                   -- Base type.
    _×̇_   : (P₁ P₂ : Ty⁺) → Ty⁺                -- Finite product (tensor).
    Σ̇     : (I : set) (Ps : El I → Ty⁺) → Ty⁺  -- Variant (sum).
    [_]   : (e : Eff) (N : Ty⁻) → Ty⁺          -- Thunk (U).
                                               -- Remembers effects.

  -- Computation types

  data Ty⁻ : Set where
    ◇̇    : (P : Ty⁺) → Ty⁻                     -- Comp (F).
    Π̇    : (I : set) (Ns : El I → Ty⁻) → Ty⁻   -- Record (lazy product).
    _⇒̇_  : (P : Ty⁺) (N : Ty⁻) → Ty⁻           -- Function type.

-- In CBPV, a variable stands for a value.
-- Thus, environments only contain values,
-- and typing contexts only value types.

-- We use introduce syntax in an intrinsically well-typed way
-- with variables being de Bruijn indices into the typing context.
-- Thus, contexts are just lists of types.

Cxt = List Ty⁺

variable
  Γ Δ Φ            : Cxt
  J                : Cxt → Set
  P P₁ P₂ P' P′ Q  : Ty⁺
  N N₁ N₂ N' N′    : Ty⁻
  Ps               : El I → Ty⁺
  Ns               : El I → Ty⁻

-- Generic values

module _ (Var : Ty⁺ → Cxt → Set) (Comp : Eff → Ty⁻ → Cxt → Set) where

  -- Right non-invertible

  data Val' : (P : Ty⁺) (Γ : Cxt) → Set where
    var    : (x : Var P Γ)                      → Val' P Γ
    pair   : (v₁ : Val' P₁ Γ) (v₂ : Val' P₂ Γ)  → Val' (P₁ ×̇ P₂) Γ
    inj    : (i : _) (v : Val' (Ps i) Γ)        → Val' (Σ̇ I Ps) Γ
    thunk  : (t : Comp e N Γ)                   → Val' ([ e ] N) Γ

-- Terms

mutual

  Val = Val' _∈_ Comp

  data Comp (e : Eff) : (N : Ty⁻) (Γ : Cxt) → Set where
    -- introductions
    ret    : (∅≤ : ∅ ≤ e)
             (v : Val P Γ)                → Comp e (◇̇ P)    Γ
    rec    : (t : ∀ i → Comp e (Ns i) Γ)  → Comp e (Π̇ I Ns) Γ
    abs    : (t : Comp e N (P ∷ Γ))       → Comp e (P ⇒̇ N)  Γ
    -- positive eliminations
    split  : (v : Val (P₁ ×̇ P₂) Γ)  (t : Comp e N (P₂ ∷ P₁ ∷ Γ))      → Comp e N Γ
    case   : (v : Val (Σ̇ I Ps) Γ)   (t : ∀ i → Comp e N (Ps i ∷ Γ))   → Comp e N Γ
    bind   : (+≤ : e₁ + e₂ ≤ e)
             (u : Comp e₁ (◇̇ P) Γ)  (t : Comp e₂ N (P ∷ Γ))           → Comp e N Γ
    -- cut
    letv   : (v : Val P Γ)          (t : Comp e N (P ∷ Γ))            → Comp e N Γ
    -- negative eliminations
    force  : (v : Val  ([ e ] N)  Γ)                  → Comp e N      Γ
    prj    : (i : _) (t : Comp e (Π̇ I Ns) Γ)          → Comp e (Ns i) Γ
    app    : (t : Comp e (P ⇒̇ N)  Γ)   (v : Val P Γ)  → Comp e N      Γ

-- Normal forms
------------------------------------------------------------------------

-- Normal values only reference variables of base type

NVar : (P : Ty⁺) (Γ : Cxt) → Set
NVar (base o) Γ = base o ∈ Γ
NVar _ _ = ⊥

-- Negative neutrals

module _ (Val : Ty⁺ → Cxt → Set) where

  -- Right non-invertible
  -- Propagates the effect from the head variable, a thunk.

  data Ne' (e : Eff) : (N : Ty⁻) (Γ : Cxt) → Set where
    force  : (x : [ e ] N ∈ Γ)                    → Ne' e N Γ
    prj    : (i : El I) (t : Ne' e (Π̇ I Ns) Γ)    → Ne' e (Ns i) Γ
    app    : (t : Ne' e (P ⇒̇ N) Γ) (v : Val P Γ)  → Ne' e N Γ

mutual

  NVal = Val' NVar Nf
  Ne   = Ne' NVal

  -- Cover monad (generalized case tree).
  -- Collects effects from all bind nodes.

  data ⟨_⟩ (e : Eff) (J : Cxt → Set) (Γ : Cxt) : Set where
    return  : (∅≤ : ∅ ≤ e)         (j : J Γ)                          → ⟨ e ⟩ J Γ
    bind    : (+≤ : e₁ + e₂ ≤ e)
              (u : Ne e₁ (◇̇ P) Γ)  (t :      ⟨ e₂ ⟩ J       (P ∷ Γ))  → ⟨ e ⟩ J Γ
    case    : (x : Σ̇ I Ps ∈ Γ)     (t : ∀ i → ⟨ e ⟩ J    (Ps i ∷ Γ))  → ⟨ e ⟩ J Γ
    split   : (x : (P₁ ×̇ P₂) ∈ Γ)  (t :       ⟨ e ⟩ J (P₂ ∷ P₁ ∷ Γ))  → ⟨ e ⟩ J Γ

  ◇ : ∀ J e Γ → Set
  ◇ J e = ⟨ e ⟩ J

  -- syntax ◇ J e = ⟨ e ⟩ J

  -- Right invertible.

  data Nf (e : Eff) : (N : Ty⁻) (Γ : Cxt) → Set where
    -- ne only needed for negative base types
    -- ne    : let N = ◇̇ (base o) in (n : ⟨ e ⟩ (Ne e N) Γ)  → Nf e N       Γ
    -- ne    : let N = ◇̇ (base o) in
    --         (+≤ : e₁ + e₂ ≤ e) (n : ⟨ e₂ ⟩ (Ne e₁ N) Γ)  → Nf e N Γ
    ret   : (v : ⟨ e ⟩ (NVal P) Γ)                        → Nf e (◇̇ P)   Γ   -- Invoke RFoc
    rec   : (ts : ∀ i → Nf e (Ns i) Γ)                    → Nf e (Π̇ I Ns) Γ
    abs   : (t : Nf e N (P ∷ Γ))                          → Nf e (P ⇒̇ N)  Γ

-- Context-indexed sets
------------------------------------------------------------------------

PSet = (Γ : Cxt) → Set
NSet = (e : Eff) (Γ : Cxt) → Set

variable
  C A A' A₁ A₂ : PSet
  B B' B₁ B₂ : NSet
  F G As : (i : El I) → PSet
  Bs Bs' Bs₁ Bs₂ : (i : El I) → NSet

-- Constructions on PSet

1̂ : PSet
1̂ Γ = ⊤

_×̂_ : (A₁ A₂ : PSet) → PSet
(A₁ ×̂ A₂) Γ = A₁ Γ × A₂ Γ

Σ̂ : (I : set) (As : El I → PSet) → PSet
(Σ̂ I F) Γ = ∃ λ i → F i Γ

_⇒̂_ : (A₁ A₂ : PSet) → PSet
(A₁ ⇒̂ A₂) Γ = A₁ Γ → A₂ Γ

Π̂ : (I : set) (As : El I → PSet) → PSet
(Π̂ I As) Γ = ∀ i → As i Γ

⟪_⟫ : (P : Ty⁺) (A : PSet) → PSet
⟪ P ⟫ A Γ = A (P ∷ Γ)

-- Constructions on NSet

_⇒ⁿ_ : (A : PSet) (B : NSet) → NSet
(A ⇒ⁿ B) e Γ = A Γ → B e Γ

Πⁿ : (I : set) (Bs : El I → NSet) → NSet
(Πⁿ I Bs) e Γ = ∀ i → Bs i e Γ

-- Morphisms between ISets

_→̇_ : (A₁ A₂ : PSet) → Set
A₁ →̇ A₂ = ∀{Γ} → A₁ Γ → A₂ Γ

_→̈_ : (B₁ B₂ : NSet) → Set
B₁ →̈ B₂ = ∀{e Γ} → B₁ e Γ → B₂ e Γ

⟨_⊙_⟩→̇_ : (P Q R : PSet) → Set
⟨ P ⊙ Q ⟩→̇ R = ∀{Γ} → P Γ → Q Γ → R Γ

⟨_⊙_⊙_⟩→̇_ : (P Q R S : PSet) → Set
⟨ P ⊙ Q ⊙ R ⟩→̇ S = ∀{Γ} → P Γ → Q Γ → R Γ → S Γ

Map : (F : (PSet) → PSet) → Set₁
Map F = ∀{A B : PSet} (f : A →̇ B) → F A →̇ F B

Π-map : (∀ i {e} → Bs i e →̇ Bs' i e) → ∀{e} → Πⁿ I Bs e →̇ Πⁿ I Bs' e
Π-map f r i = f i (r i)

-- -- Introductions and eliminations for ×̂

-- p̂air : ⟨ A ⊙ B ⟩→̇ (A ×̂ B)
-- p̂air a b = λ

-- Monotonicity
------------------------------------------------------------------------

-- Monotonization □ is a monoidal comonad

□ : (A : PSet) → PSet
□ A Γ = ∀{Δ} (τ : Γ ⊆ Δ) → A Δ

extract : □ A →̇ A
extract a = a ⊆-refl

duplicate : □ A →̇ □ (□ A)
duplicate a τ τ′ = a (⊆-trans τ τ′)

□-map : Map □
□-map f a τ = f (a τ)

extend : (□ A →̇ C) → □ A →̇ □ C
extend f = □-map f ∘ duplicate

□-weak : □ A →̇ ⟪ P ⟫ (□ A)
□-weak a τ = a (⊆-trans (_ ∷ʳ ⊆-refl) τ)

□-weak' : □ A →̇ □ (⟪ P ⟫ A)
□-weak' a τ = a (_ ∷ʳ τ)

□-sum : Σ̂ I (□ ∘ F) →̇ □ (Σ̂ I F)
□-sum (i , a) τ = i , a τ

-- Monoidality:

□-unit : 1̂ →̇ □ 1̂
□-unit = _

□-pair : ⟨ □ A₁ ⊙ □ A₂ ⟩→̇ □ (A₁ ×̂ A₂)
□-pair a b τ = (a τ , b τ)

-- -- Strong functoriality

Map! : (F : PSet → PSet) → Set₁
Map! F = ∀{A C} → ⟨ □ (λ Γ → A Γ → C Γ) ⊙ F A ⟩→̇ F C

-- Monotonicity

Mon : (A : PSet) → Set
Mon A = A →̇ □ A

monVar : Mon (P ∈_)
monVar x τ = ⊆-lookup τ x

-- Positive ISets are monotone

□-mon : Mon (□ A)
□-mon = duplicate

1-mon : Mon 1̂
1-mon = □-unit

×-mon : Mon A₁ → Mon A₂ → Mon (A₁ ×̂ A₂)
×-mon mA mB (a , b) = □-pair (mA a) (mB b)

Σ-mon : ((i : El I) → Mon (F i)) → Mon (Σ̂ I F)
Σ-mon m (i , a) = □-sum (i , m i a)

□-intro : Mon A → (A →̇ C) → (A →̇ □ C)
□-intro mA f = □-map f ∘ mA

-- Cover monad: a strong graded monad
------------------------------------------------------------------------

join : ⟨ e₁ ⟩ (⟨ e₂ ⟩ A) →̇ ⟨ e₁ + e₂ ⟩ A
join (return ∅≤e c)  = {!c !}
join (bind ≤e u c)  = {!bind u (join c) !}
join (case x t)  = case x (join ∘ t)
join (split x c) = split x (join c)

{-
◇-map : Map ⟨ e ⟩
◇-map f (return  j) = return  (f j)
◇-map f (bind  u a) = bind  u (◇-map f a)
◇-map f (case  x t) = case  x (λ i → ◇-map f (t i))
◇-map f (split x a) = split x (◇-map f a)

◇-map! : Map! ⟨ e ⟩
◇-map! f (return  j) = return  (extract f j)
◇-map! f (bind  u a) = bind  u (◇-map! (□-weak f) a)
◇-map! f (case  x t) = case  x (λ i → ◇-map! (□-weak f) (t i))
◇-map! f (split x a) = split x (◇-map! (□-weak (□-weak f)) a)

◇-bind : A →̇ ⟨ e₂ ⟩ C → ⟨ e₁ ⟩ A →̇ ⟨ e₁ + e₂ ⟩ C
◇-bind f = join ∘ ◇-map f

◇-record : (⟨ e ⟩ ∘ Πⁿ I Bs) →̈ Πⁿ I (λ i → ⟨ e ⟩ ∘ Bs i)
◇-record c i = ◇-map (_$ i) c

◇-fun : Mon A → (⟨ e ⟩ ∘ A ⇒ⁿ B) →̈ (A ⇒ⁿ (⟨ e ⟩ ∘ B))
◇-fun mA c a = ◇-map! (λ τ f → f (mA a τ)) c

-- Monoidal functoriality

◇-pair : ⟨ □ (⟨ e₁ ⟩ A₁) ⊙ ⟨ e₂ ⟩ (□ A₂) ⟩→̇ ⟨ e₂ + e₁ ⟩ (A₁ ×̂ A₂)
◇-pair ca = join ∘ ◇-map! λ τ b → ◇-map! (λ τ′ a → a , b τ′) (ca τ)

_⋉_ = ◇-pair

□◇-pair' : ⟨ □ (⟨ e₁ ⟩ A₁) ⊙ □ (⟨ e₂ ⟩ (□ A₂)) ⟩→̇ □ (⟨ e₂ + e₁ ⟩ (A₁ ×̂ A₂))
□◇-pair' ca cb τ = ◇-pair (□-mon ca τ) (cb τ)

□◇-pair : Mon A₂ → ⟨ □ (⟨ e₁ ⟩ A₁) ⊙ □ (⟨ e₂ ⟩ A₂) ⟩→̇ □ (⟨ e₂ + e₁ ⟩ (A₁ ×̂ A₂))
□◇-pair mB ca cb τ = join $
  ◇-map! (λ τ₁ b → ◇-map! (λ τ₂ a → a , mB b τ₂) (ca (⊆-trans τ τ₁))) (cb τ)

◇□-pair' : ⟨ ⟨ e₁ ⟩ (□ A₁) ⊙ □ (⟨ e₂ ⟩ (□ A₂)) ⟩→̇ ⟨ e₁ + e₂ ⟩ (□ (A₁ ×̂ A₂))
◇□-pair' ca cb = join (◇-map! (λ τ a → ◇-map! (λ τ₁ b {_} τ₂ → a (⊆-trans τ₁ τ₂) , b τ₂) (cb τ)) ca)
  -- Without the abstraction over {_}, there is an incomprehensible error.

◇□-pair : ⟨ □ (⟨ e₁ ⟩ (□ A₁)) ⊙ ⟨ e₂ ⟩ (□ A₂) ⟩→̇ ⟨ e₂ + e₁ ⟩ (□ (A₁ ×̂ A₂))
◇□-pair ca cb = join (◇-map! (λ τ b → ◇-map! (λ τ₁ a {_} τ₂ → a τ₂ , b (⊆-trans τ₁ τ₂)) (ca τ)) cb)
  -- Without the abstraction over {_}, there is an incomprehensible error.

-- Runnability

Run : (B : NSet) → Set
Run B = ∀{e₁ e₂} → ⟨ e₁ ⟩ (B e₂) →̇ B (e₁ + e₂)

-- Negative ISets are runnable

◇-run : Run (◇ A)
◇-run = join

Π-run : (∀ i → Run (Bs i)) → Run (Πⁿ I Bs)
Π-run f c i = f i (◇-map (_$ i) c)
-- Π-run f x i = Π-map {!λ j → f j!} {!!} {!!}
-- Π-run f = {!Π-map f!} ∘ ◇-record

⇒-run : Mon A → Run B → Run (A ⇒ⁿ B)
⇒-run {B = B} mA rB f = rB ∘ ◇-fun {B = B} mA f

-- Bind for the ◇ monad

◇-elim : Run B → (A →̇ B e₂) → ⟨ e₁ ⟩ A →̇ B (e₁ + e₂)
◇-elim rB f = rB ∘ ◇-map f

◇-elim! : Run B → ⟨ □ (A ⇒̂ B e₂) ⊙ ⟨ e₁ ⟩ A ⟩→̇ B (e₁ + e₂)
◇-elim! rB f = rB ∘ ◇-map! f

◇-elim-□ : Run B → ⟨ □ (A ⇒̂ B e₂) ⊙ □ (⟨ e₁ ⟩ A) ⟩→̇ □ (B (e₁ + e₂))
◇-elim-□ {B = B} rB f c = □-map (uncurry (◇-elim! {B = B} rB)) (□-pair (□-mon f) c)

◇-elim-□-alt : Run B → ⟨ □ (A ⇒̂ B e₂) ⊙ □ (⟨ e₁ ⟩ A) ⟩→̇ □ (B (e₁ + e₂))
◇-elim-□-alt {B = B} rB f c τ = ◇-elim! {B = B} rB (□-mon f τ) (c τ)

bind! : Mon C → Run B → (C →̇ ⟨ e₁ ⟩ A) → (C →̇ (A ⇒̂ B e₂)) → C →̇ B (e₁ + e₂)
bind! {B = B} mC rB f k γ = ◇-elim! {B = B} rB (λ τ a → k (mC γ τ) a) (f γ)

-- Type interpretation
------------------------------------------------------------------------

mutual
  ⟦_⟧⁺ : Ty⁺ → PSet
  ⟦ base o  ⟧⁺ = base o ∈_
  ⟦ P₁ ×̇ P₂ ⟧⁺ = ⟦ P₁ ⟧⁺ ×̂ ⟦ P₂ ⟧⁺
  ⟦ Σ̇ I P   ⟧⁺ = Σ̂ I λ i → ⟦ P i ⟧⁺
  ⟦ [ e ] N ⟧⁺ = □ (⟦ N ⟧⁻ e)

  ⟦_⟧⁻ : Ty⁻ → NSet
  ⟦ ◇̇ P   ⟧⁻ = ◇ ⟦ P ⟧⁺
  ⟦ Π̇ I N ⟧⁻ = Πⁿ I λ i → ⟦ N i ⟧⁻
  ⟦ P ⇒̇ N ⟧⁻ = ⟦ P ⟧⁺ ⇒ⁿ ⟦ N ⟧⁻

⟦_⟧ᶜ : Cxt → PSet
⟦_⟧ᶜ Γ Δ = All (λ P → ⟦ P ⟧⁺ Δ) Γ

-- ⟦ []    ⟧ᶜ = 1̂
-- ⟦ P ∷ Γ ⟧ᶜ = ⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺

-- Positive types are monotone.

mon⁺ : (P : Ty⁺) → Mon ⟦ P ⟧⁺
mon⁺ (base o)  = monVar
mon⁺ (P₁ ×̇ P₂) = ×-mon (mon⁺ P₁) (mon⁺ P₂)
mon⁺ (Σ̇ I P)   = Σ-mon (mon⁺ ∘ P)
mon⁺ ([ e ] N) = □-mon

monᶜ : (Γ : Cxt) → Mon ⟦ Γ ⟧ᶜ
monᶜ Γ γ τ = All.map (λ {P} v → mon⁺ P v τ) γ

-- Negative types are runnable.

run⁻ : (N : Ty⁻) → Run ⟦ N ⟧⁻
run⁻ (◇̇ P)   = ◇-run
run⁻ (Π̇ I N) = Π-run (run⁻ ∘ N)
run⁻ (P ⇒̇ N) = ⇒-run {B = ⟦ N ⟧⁻} (mon⁺ P) (run⁻ N)

-- monᶜ []      = 1-mon
-- monᶜ (P ∷ Γ) = ×-mon (monᶜ Γ) (mon⁺ P)

-- Interpretation
------------------------------------------------------------------------

mutual

  ⦅_⦆⁺ : Val P Γ → ⟦ Γ ⟧ᶜ →̇ ⟦ P ⟧⁺
  ⦅ var x ⦆⁺      = λ γ → All.lookup γ x
  ⦅ pair v₁ v₂ ⦆⁺ = < ⦅ v₁ ⦆⁺ , ⦅ v₂ ⦆⁺ >
  ⦅ inj i v ⦆⁺    = (i ,_) ∘ ⦅ v ⦆⁺
  ⦅ thunk t ⦆⁺    = □-intro (monᶜ _) ⦅ t ⦆⁻

  λ⦅_⦆⁻ : Comp e N (P ∷ Γ) → ⟦ Γ ⟧ᶜ →̇ ⟦ P ⇒̇ N ⟧⁻ e
  λ⦅ t ⦆⁻ γ a = ⦅ t ⦆⁻ (a ∷ γ)

  ⦅_⦆⁻ : Comp e N Γ → ⟦ Γ ⟧ᶜ →̇ ⟦ N ⟧⁻ e
  ⦅ ret v ⦆⁻ = return ∘ ⦅ v ⦆⁺
  ⦅ rec t ⦆⁻ = flip λ i → {! ⦅ t i ⦆⁻ !}  -- need effect subsumption es i ≤ sup es
  ⦅ abs t ⦆⁻ = λ⦅ t ⦆⁻
  ⦅ split v t ⦆⁻ γ = let (a₁ , a₂) = ⦅ v ⦆⁺ γ in ⦅ t ⦆⁻ (a₂ ∷ (a₁ ∷ γ))
  ⦅ case v t ⦆⁻  γ = let (i , a) = ⦅ v ⦆⁺ γ in  {! ⦅ t i ⦆⁻ (a ∷ γ) !}  -- eff sub
  ⦅ bind {Γ = Γ} {N = N} t t₁ ⦆⁻ = bind! {B = ⟦ N ⟧⁻} (monᶜ Γ) (run⁻ N) ⦅ t ⦆⁻ λ⦅ t₁ ⦆⁻
  ⦅ force v ⦆⁻  = extract ∘ ⦅ v ⦆⁺
  ⦅ prj i t ⦆⁻  = (_$ i) ∘ ⦅ t ⦆⁻
  ⦅ app t v ⦆⁻  = ⦅ t ⦆⁻  ˢ ⦅ v ⦆⁺
  ⦅ letv v t ⦆⁻ = λ⦅ t ⦆⁻ ˢ ⦅ v ⦆⁺

-- Reflection and reification

mutual

  fresh□◇□ : ∀ P {Γ} → ⟪ P ⟫ (□ (⟨ ∅ ⟩ (□ ⟦ P ⟧⁺))) Γ
  fresh□◇□ P = reflect⁺□ P ∘ monVar here!

  fresh□ : ∀ P {Γ} → ⟪ P ⟫ (□ (⟨ ∅ ⟩ ⟦ P ⟧⁺)) Γ
  fresh□ P = ◇-map extract ∘ reflect⁺□ P ∘ monVar here!
  fresh□ P = reflect⁺ P ∘ monVar here!

  fresh : ∀ {P Γ} → ⟪ P ⟫ (⟨ ∅ ⟩ ⟦ P ⟧⁺) Γ
  fresh {P} = ◇-map extract (reflect⁺□ P here!)
  fresh {P} = reflect⁺ P here!

  fresh◇ : ∀ {P Γ} → ⟪ P ⟫ (⟨ ∅ ⟩ (□ ⟦ P ⟧⁺)) Γ
  fresh◇ {P} = reflect⁺□ P here!
  fresh◇ {P} = ◇-map (mon⁺ P) fresh

  -- saves us use of Mon P in freshᶜ
  reflect⁺□ : (P : Ty⁺) → (P ∈_) →̇ (⟨ ∅ ⟩ (□ ⟦ P ⟧⁺))
  reflect⁺□ (base o)  x = return (monVar x)
  reflect⁺□ (P₁ ×̇ P₂) x = split x (◇□-pair (reflect⁺□ P₁ ∘ monVar (there here!)) fresh◇)
  reflect⁺□ (Σ̇ I Ps)  x = case x λ i → ◇-map (□-map (i ,_)) fresh◇
  reflect⁺□ ([ e ] N) x = return (□-mon (reflect⁻ N ∘ force ∘ monVar x))

  reflect⁺ : (P : Ty⁺) → (P ∈_) →̇ (⟨ ∅ ⟩ ⟦ P ⟧⁺)
  reflect⁺ (base o)  x = return x
  reflect⁺ (P₁ ×̇ P₂) x = split x (□-weak (fresh□ P₁) ⋉ fresh◇)
  reflect⁺ (Σ̇ I Ps)  x = case x λ i → ◇-map (i ,_) fresh
  reflect⁺ ([ e ] N) x = return λ τ → reflect⁻ N (force (monVar x τ))

  reflect⁻ : (N : Ty⁻) → Ne e N →̇ ⟦ N ⟧⁻ e
  reflect⁻ (◇̇ P)    u = bind u fresh
  reflect⁻ (Π̇ I Ns) u = λ i → reflect⁻ (Ns i) (prj i u)
  reflect⁻ (P ⇒̇ N)  u = λ a → reflect⁻ N (app u (reify⁺ P a))

  reify⁺ : (P : Ty⁺) → ⟦ P ⟧⁺ →̇ NVal P
  reify⁺ (base o) = var
  reify⁺ (P₁ ×̇ P₂) (a₁ , a₂) = pair (reify⁺ P₁ a₁) (reify⁺ P₂ a₂)
  reify⁺ (Σ̇ I Ps)  (i  , a ) = inj i (reify⁺ (Ps i) a)
  reify⁺ ([ e ] N) a = thunk (reify⁻ N a)

  reify⁻ : (N : Ty⁻) → □ (⟦ N ⟧⁻ e) →̇ Nf e N
  reify⁻         (◇̇ P)    f = ret (◇-map (reify⁺ P) (extract f))
  reify⁻ {e = e} (Π̇ I Ns) f = rec {es = λ i → e} λ i → reify⁻ (Ns i) (□-map (_$ i) f)
  reify⁻         (P ⇒̇ N)  f = abs $ reify⁻ N $ ◇-elim-□ {B = ⟦ N ⟧⁻} (run⁻ N) (□-weak f) $ fresh□ P

ext : (⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺) →̇ ⟦ P ∷ Γ ⟧ᶜ
ext (γ , a) = a ∷ γ

◇-ext : ⟨ e ⟩ (⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺) →̇ ⟨ e ⟩ ⟦ P ∷ Γ ⟧ᶜ
◇-ext = ◇-map ext

-- Without the use of ◇-mon!

freshᶜ : (Γ : Cxt) → □ (⟨ ∅ ⟩ ⟦ Γ ⟧ᶜ) Γ
freshᶜ []      = λ τ → return []
freshᶜ (P ∷ Γ) = ◇-ext ∘ □◇-pair' (□-weak (freshᶜ Γ)) (fresh□◇□ P)
freshᶜ (P ∷ Γ) = ◇-ext ∘ □◇-pair (mon⁺ P) (□-weak (freshᶜ Γ)) (fresh□ P)
freshᶜ (P ∷ Γ) = ◇-ext ∘ □◇-pair' (□-weak (freshᶜ Γ)) (◇-map (mon⁺ P) ∘ (fresh□ P))
freshᶜ (P ∷ Γ) = ◇-ext ∘ λ τ →
  (□-weak (□-mon (freshᶜ Γ)) τ)
  ⋉ ◇-map (mon⁺ P) (fresh□ P τ)

norm : Comp e N →̇ Nf e N
norm {N = N} {Γ = Γ} t = reify⁻ N $ □-map (run⁻ N ∘ ◇-map ⦅ t ⦆⁻) $ freshᶜ Γ
norm {N = N} {Γ = Γ} t = reify⁻ N $ run⁻ N ∘ ◇-map ⦅ t ⦆⁻ ∘ freshᶜ Γ

-- -}
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


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

module Lecture8 where

import Lecture7
open Lecture7 public

-- Section 8.1 Propositions

is-prop : {i : Level} (A : UU i) → UU i
is-prop A = (x y : A) → is-contr (Id x y)

is-prop-empty : is-prop empty
is-prop-empty ()

is-prop-unit : is-prop unit
is-prop-unit = is-prop-is-contr is-contr-unit

is-prop' : {i : Level} (A : UU i) → UU i
is-prop' A = (x y : A) → Id x y

is-prop-is-prop' : {i : Level} {A : UU i} → is-prop' A → is-prop A
is-prop-is-prop' {i} {A} H x y =
  dpair
    (concat _ (inv (H x x)) (H x y))
    (ind-Id
      (λ z p → Id (concat _ (inv (H x x)) (H x z)) p)
      (left-inv (H x x)) y)

is-prop'-is-prop : {i : Level} {A : UU i} → is-prop A → is-prop' A
is-prop'-is-prop H x y = pr1 (H x y)

is-contr-is-prop-inh : {i : Level} {A : UU i} → is-prop A → A → is-contr A
is-contr-is-prop-inh H a = dpair a (is-prop'-is-prop H a)

is-subtype : {i j : Level} {A : UU i} (B : A → UU j) → UU (i ⊔ j)
is-subtype B = (x : _) → is-prop (B x)

-- Section 8.2 Sets

is-set : {i : Level} → UU i → UU i
is-set A = (x y : A) → is-prop (Id x y)

axiom-K : {i : Level} → UU i → UU i
axiom-K A = (x : A) (p : Id x x) → Id refl p

is-set-axiom-K : {i : Level} (A : UU i) → axiom-K A → is-set A
is-set-axiom-K A H x y =
  is-prop-is-prop' (ind-Id (λ z p → (q : Id x z) → Id p q) (H x) y)

axiom-K-is-set : {i : Level} (A : UU i) → is-set A → axiom-K A
axiom-K-is-set A H x p =
  concat
    (center (is-contr-is-prop-inh (H x x) refl))
      (inv (contraction (is-contr-is-prop-inh (H x x) refl) refl))
      (contraction (is-contr-is-prop-inh (H x x) refl) p)

is-equiv-prop-in-id : {i j : Level} {A : UU i}
  (R : A → A → UU j)
  (p : (x y : A) → is-prop (R x y))
  (ρ : (x : A) → R x x)
  (i : (x y : A) → R x y → Id x y)
  → (x y : A) → is-equiv (i x y)
is-equiv-prop-in-id R p ρ i x =
  id-fundamental-retr x (i x)
    (λ y → dpair
      (ind-Id (λ z p → R x z) (ρ x) y)
      ((λ r → is-prop'-is-prop (p x y) _ r)))

is-prop-is-equiv : {i j : Level} {A : UU i} (B : UU j)
  (f : A → B) (E : is-equiv f) → is-prop B → is-prop A
is-prop-is-equiv B f E H x y =
  is-contr-is-equiv (ap f {x} {y}) (is-emb-is-equiv f E x y) (H (f x) (f y))

is-prop-is-equiv' : {i j : Level} (A : UU i) {B : UU j}
  (f : A → B) (E : is-equiv f) → is-prop A → is-prop B
is-prop-is-equiv' A f E H =
  is-prop-is-equiv _ (inv-is-equiv E) (is-equiv-inv-is-equiv E) H

is-set-prop-in-id : {i j : Level} {A : UU i}
  (R : A → A → UU j)
  (p : (x y : A) → is-prop (R x y))
  (ρ : (x : A) → R x x)
  (i : (x y : A) → R x y → Id x y)
  → is-set A
is-set-prop-in-id R p ρ i x y = is-prop-is-equiv' (R x y) (i x y) (is-equiv-prop-in-id R p ρ i x y) (p x y)

is-prop-EqN : (n m : ℕ) → is-prop (EqN n m)
is-prop-EqN Nzero Nzero = is-prop-unit
is-prop-EqN Nzero (Nsucc m) = is-prop-empty
is-prop-EqN (Nsucc n) Nzero = is-prop-empty
is-prop-EqN (Nsucc n) (Nsucc m) = is-prop-EqN n m

is-set-nat : is-set ℕ
is-set-nat =
  is-set-prop-in-id
    EqN
    is-prop-EqN
    reflexive-EqN
    (least-reflexive-EqN (λ n → refl))


text:
module MLib.Fin.Parts.Nat where

open import MLib.Prelude
open import MLib.Fin.Parts.Core

open Nat using (_*_; _+_; _<_)
open Fin using (fromℕ≤)
open Table

module Impl where
  tryLookup : ∀ {n} {a} {A : Set a} → A → Table A n → ℕ → A
  tryLookup {n = zero} z t _ = z
  tryLookup {n = suc n} z t zero = lookup t zero
  tryLookup {n = suc n} z t (suc i) = tryLookup z (tail t) i

  tryLookup-prop : ∀ {n} {a} {A : Set a} {z : A} (t : Table A n) {i : Fin n} → lookup t i ≡ tryLookup z t (Fin.toℕ i)
  tryLookup-prop _ {i = zero} = ≡.refl
  tryLookup-prop t {i = suc i} = tryLookup-prop (tail t)

  data Ordering′ : ℕ → ℕ → Set where
    less : ∀ m k → Ordering′ m (suc (m + k))
    gte : ∀ m k → Ordering′ (m + k) m

  compare′ : ∀ m n → Ordering′ m n
  compare′ zero zero = gte zero zero
  compare′ zero (suc n) = less zero n
  compare′ (suc m) zero = gte zero (suc m)
  compare′ (suc m) (suc n) with compare′ m n
  compare′ (suc m) (suc .(suc (m + k))) | less .m k = less (suc m) k
  compare′ (suc .(n + k)) (suc n) | gte .n k = gte (suc n) k

  -- Core lemmas

  lz-lem : ∀ a b c → a + b < a + c → b < c
  lz-lem zero b c p = p
  lz-lem (suc a) b c p = lz-lem a b c (Nat.+-cancelˡ-≤ 1 p)

  lz-lem₂ : ∀ a b → a < a + b → 0 < b
  lz-lem₂ zero b p = p
  lz-lem₂ (suc a) b p = lz-lem₂ a b (Nat.+-cancelˡ-≤ 1 p)

  fromℕ≤-cong′ : ∀ {a b m n} {p : a < m} {q : b < n} → m ≡ n → a ≡ b → fromℕ≤ {a} p ≅ fromℕ≤ {b} q
  fromℕ≤-cong′ {p = Nat.s≤s Nat.z≤n} {Nat.s≤s Nat.z≤n} ≡.refl ≡.refl = ≅.refl
  fromℕ≤-cong′ {p = Nat.s≤s (Nat.s≤s p)} {Nat.s≤s (Nat.s≤s q)} ≡.refl ≡.refl = ≅.cong suc (fromℕ≤-cong′ {p = Nat.s≤s p} {q = Nat.s≤s q} ≡.refl ≡.refl)

  fromℕ≤-cong : ∀ {a b n} {p : a < n} {q : b < n} → a ≡ b → fromℕ≤ {a} p ≡ fromℕ≤ {b} q
  fromℕ≤-cong = ≅.≅-to-≡ ∘ fromℕ≤-cong′ ≡.refl

  -- Core functions

  fromParts : {numParts : ℕ} (parts : Table ℕ numParts) → ℕ × ℕ → ℕ
  fromParts parts (zero , j) = j
  fromParts {zero} parts (suc i , j) = 0
  fromParts {suc numParts} parts (suc i , j) = lookup parts zero + fromParts (tail parts) (i , j)

  toParts : {numParts : ℕ} (parts : Table ℕ numParts) (k : ℕ) → ℕ × ℕ
  toParts {zero} parts k = 0 , 0
  toParts {suc n} parts k with lookup parts zero | compare′ k (lookup parts zero)
  toParts {suc n} parts k | .(suc (k + k₁)) | less .k k₁ = 0 , k
  toParts {suc n} parts .(lz + k) | lz | gte .lz k =
    let i , j = toParts (tail parts) k
    in (suc i , j)

  -- Property lemmas

  +-<-lem : ∀ {a b c} → b < c → a + b < a + c
  +-<-lem {zero} p = p
  +-<-lem {suc a} p = Nat.s≤s (+-<-lem p)

  fromℕ-suc-lem : ∀ {m n} (p : m < n) → suc (fromℕ≤ p) ≡ fromℕ≤ (Nat.s≤s p)
  fromℕ-suc-lem (Nat.s≤s p) = ≡.refl

  -- Properties

  fromParts-prop : ∀ {numParts} (parts : Table ℕ numParts) {i j} → i < numParts → j < tryLookup 0 parts i → fromParts parts (i , j) < sum parts
  fromParts-prop {suc numParts} _ {zero} (Nat.s≤s p) q = Nat.≤-trans q (Nat.m≤m+n _ _)
  fromParts-prop {suc numParts} parts {suc i} (Nat.s≤s p) q = +-<-lem (fromParts-prop (tail parts) p q)

  toParts-prop : ∀ {numParts : ℕ} (parts : Table ℕ numParts) {k} → k < sum parts →
    let i , j = toParts parts k
    in Σ (i < numParts) (λ q → j < lookup parts (fromℕ≤ {i} q))
  toParts-prop {zero} parts {k} ()
  toParts-prop {suc numParts} parts {k} p with lookup parts zero | compare′ k (lookup parts zero) | ≡.inspect (lookup parts) zero
  toParts-prop {suc numParts} parts {k} p | .(suc (k + k₁)) | less .k k₁ | ≡.[ eq ] =
    Nat.s≤s Nat.z≤n ,
    Nat.≤-trans (Nat.s≤s (Nat.m≤m+n _ _)) (Nat.≤-reflexive (≡.sym eq))
  toParts-prop {suc numParts} parts {.(lz + k)} p | lz | gte .lz k | insp =
    let q , r = toParts-prop (tail parts) {k} (lz-lem _ _ _ p)
    in Nat.s≤s q , Nat.≤-trans r (Nat.≤-reflexive (≡.cong (lookup parts) (fromℕ-suc-lem _)))

  toParts-fromParts :
    {numParts : ℕ} (parts : Table ℕ numParts) (i j : ℕ) (p : j < tryLookup 0 parts i) →
    toParts parts (fromParts parts (i , j)) ≡ (i , j)
  toParts-fromParts {zero} _ i j ()
  toParts-fromParts {suc numParts} parts i j p
    with lookup parts zero
       | fromParts parts (i , j)
       | compare′ (fromParts parts (i , j)) (lookup parts zero)
       | ≡.inspect (lookup parts) zero
       | ≡.inspect (fromParts parts) (i , j)
  toParts-fromParts {suc numParts} parts zero .ipi p
    | .(suc (ipi + k)) | ipi | less .ipi k | insp₁ | ≡.[ ≡.refl ]
    = ≡.refl
  toParts-fromParts {suc numParts} parts zero .(lookup parts zero + k) p
    | .(lookup parts zero) | .(lookup parts zero + k) | gte .(lookup parts zero) k | ≡.[ ≡.refl ] | ≡.[ ≡.refl ]
    = ⊥-elim (Nat.n≮n _ (Nat.≤-trans p (Nat.m≤m+n _ k)))
  toParts-fromParts {suc numParts} parts (suc i) j p
    | .(suc (ipi + k)) | ipi | less .ipi k | ≡.[ eq ] | ≡.[ eq₁ ]
    = let y = lookup parts zero
          z = fromParts _ (i , j)
      in ⊥-elim (Nat.m≢1+m+n y {z + k} (
         begin
           y                   ≡⟨ eq ⟩
           suc (ipi + k)       ≡⟨ ≡.cong (λ h → suc (h + k)) (≡.sym eq₁) ⟩
           suc ((y + z) + k)   ≡⟨ ≡.cong suc (Nat.+-assoc y z k) ⟩
           suc (y + (z + k))   ∎))
    where open ≡.Reasoning
  toParts-fromParts {suc numParts} parts (suc i) j p
    | .(lookup parts zero) | .(lookup parts zero + k) | gte .(lookup parts zero) k | ≡.[ ≡.refl ] | ≡.[ eq₁ ]
    with Nat.+-cancelˡ-≡ (lookup parts zero) eq₁
  toParts-fromParts {suc numParts} parts (suc i) j p
    | .(lookup parts zero) | .(lookup parts zero + k) | gte .(lookup parts zero) k | ≡.[ ≡.refl ] | ≡.[ eq₁ ]
    | eq₂ rewrite ≡.sym eq₂
    = let q , r = Σ.≡⇒Pointwise-≡ (toParts-fromParts (tail parts) i j p)
      in Σ.Pointwise-≡⇒≡ (≡.cong suc q , r)

  fromParts-toParts : {numParts : ℕ} (parts : Table ℕ numParts) (k : ℕ) (p : k < sum parts) → fromParts parts (toParts parts k) ≡ k
  fromParts-toParts {zero} parts k ()
  fromParts-toParts {suc numParts} parts k p
    with lookup parts zero
       | compare′ k (lookup parts zero)
       | ≡.inspect (lookup parts) zero
  fromParts-toParts {suc numParts} parts k p | .(suc (k + k₁)) | less .k k₁ | insp = ≡.refl
  fromParts-toParts {suc numParts} parts .(lookup parts zero + k) p | .(lookup parts zero) | gte .(lookup parts zero) k | ≡.[ ≡.refl ]
    = ≡.cong₂ Nat._+_
      ≡.refl
      (fromParts-toParts (tail parts) k
        (Nat.+-cancelˡ-≤ (lookup parts zero) (Nat.≤-trans (Nat.≤-reflexive (Nat.+-suc _ k)) p)))

module Partsℕ {a} {A : Set a} {size : A → ℕ} (P : Parts A size) where
  open Parts P public

  fromParts : ℕ × ℕ → ℕ
  fromParts = Impl.fromParts partsizes

  toParts : ℕ → ℕ × ℕ
  toParts = Impl.toParts partsizes

  private
    tryLookup-lem : ∀ {i j} (p : i < numParts) → j < sizeAt (Fin.fromℕ≤ p) → j < Impl.tryLookup 0 partsizes i
    tryLookup-lem p q = Nat.≤-trans q (Nat.≤-reflexive (≡.trans (Impl.tryLookup-prop {z = 0} partsizes) (≡.cong (Impl.tryLookup 0 partsizes) (Fin.toℕ-fromℕ≤ _))))

  fromParts-prop : ∀ {i j} (p : i < numParts) → j < sizeAt (Fin.fromℕ≤ p) → fromParts (i , j) < totalSize
  fromParts-prop p = Impl.fromParts-prop _ p ∘ tryLookup-lem p

  toParts-prop : ∀ {k} → k < totalSize →
    let i , j = toParts k
    in Σ (i < numParts) (λ q → j < lookup partsizes (fromℕ≤ q))
  toParts-prop = Impl.toParts-prop _

  abstract
    toParts-fromParts : ∀ {i j} (p : i < numParts) (q : j < sizeAt (Fin.fromℕ≤ p)) → toParts (fromParts (i , j)) ≡ (i , j)
    toParts-fromParts p = Impl.toParts-fromParts partsizes _ _ ∘ tryLookup-lem p

    fromParts-toParts : ∀ k (p : k < totalSize) → fromParts (toParts k) ≡ k
    fromParts-toParts = Impl.fromParts-toParts partsizes


text:
Type-of : {A : Set} → A → Set
Type-of {A = A} _ = A

module _ (A : Set) where

  Foo : A → Set
  Foo a with Type-of a
  ... | B = B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module RecordPatternMatching where

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

data Unit : Set where
  unit : Unit

foo : Unit × Unit → Unit
foo (x , y) = {!!}

record Box (A : Set) : Set where
  constructor [_]
  field
    proj : A

bar : Box Unit → Unit
bar [ x ] = {!!}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unary relations
------------------------------------------------------------------------

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

module Relation.Unary where

open import Data.Empty
open import Data.Unit.Base using (⊤)
open import Data.Product
open import Data.Sum.Base using (_⊎_; [_,_])
open import Function.Base
open import Level
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Decidable.Core using (True)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

private
  variable
    a b c ℓ ℓ₁ ℓ₂ : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Definition

-- Unary relations are known as predicates and `Pred A ℓ` can be viewed
-- as some property that elements of type A might satisfy.

-- Consequently `P : Pred A ℓ` can also be seen as a subset of A
-- containing all the elements of A that satisfy property P. This view
-- informs much of the notation used below.

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Pred A ℓ = A → Set ℓ

------------------------------------------------------------------------
-- Special sets

-- The empty set.

∅ : Pred A 0ℓ
∅ = λ _ → ⊥

-- The singleton set.

｛_｝ : A → Pred A _
｛ x ｝ = x ≡_

-- The universal set.

U : Pred A 0ℓ
U = λ _ → ⊤

------------------------------------------------------------------------
-- Membership

infix 4 _∈_ _∉_

_∈_ : A → Pred A ℓ → Set _
x ∈ P = P x

_∉_ : A → Pred A ℓ → Set _
x ∉ P = ¬ x ∈ P

------------------------------------------------------------------------
-- Subset relations

infix 4 _⊆_ _⊇_ _⊈_ _⊉_ _⊂_ _⊃_ _⊄_ _⊅_

_⊆_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

_⊇_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊇ Q = Q ⊆ P

_⊈_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊈ Q = ¬ (P ⊆ Q)

_⊉_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊉ Q = ¬ (P ⊇ Q)

_⊂_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊂ Q = P ⊆ Q × Q ⊈ P

_⊃_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊃ Q = Q ⊂ P

_⊄_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊄ Q = ¬ (P ⊂ Q)

_⊅_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊅ Q = ¬ (P ⊃ Q)

-- The following primed variants of _⊆_ can be used when 'x' can't
-- be inferred from 'x ∈ P'.

infix 4 _⊆′_ _⊇′_ _⊈′_ _⊉′_ _⊂′_ _⊃′_ _⊄′_ _⊅′_

_⊆′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q

_⊇′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
Q ⊇′ P = P ⊆′ Q

_⊈′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊈′ Q = ¬ (P ⊆′ Q)

_⊉′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊉′ Q = ¬ (P ⊇′ Q)

_⊂′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊂′ Q = P ⊆′ Q × Q ⊈′ P

_⊃′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊃′ Q = Q ⊂′ P

_⊄′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊄′ Q = ¬ (P ⊂′ Q)

_⊅′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊅′ Q = ¬ (P ⊃′ Q)

------------------------------------------------------------------------
-- Properties of sets

infix 10 Satisfiable Universal IUniversal

-- Emptiness - no element satisfies P.

Empty : Pred A ℓ → Set _
Empty P = ∀ x → x ∉ P

-- Satisfiable - at least one element satisfies P.

Satisfiable : Pred A ℓ → Set _
Satisfiable P = ∃ λ x → x ∈ P

syntax Satisfiable P = ∃⟨ P ⟩

-- Universality - all elements satisfy P.

Universal : Pred A ℓ → Set _
Universal P = ∀ x → x ∈ P

syntax Universal  P = Π[ P ]

-- Implicit universality - all elements satisfy P.

IUniversal : Pred A ℓ → Set _
IUniversal P = ∀ {x} → x ∈ P

syntax IUniversal P = ∀[ P ]

-- Decidability - it is possible to determine if an arbitrary element
-- satisfies P.

Decidable : Pred A ℓ → Set _
Decidable P = ∀ x → Dec (P x)

-- Erasure: A decidable predicate gives rise to another one, more
-- amenable to η-expansion

⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
⌊ P? ⌋ a = Lift _ (True (P? a))

-- Irrelevance - any two proofs that an element satifies P are
-- indistinguishable.

Irrelevant : Pred A ℓ → Set _
Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b

-- Recomputability - we can rebuild a relevant proof given an
-- irrelevant one.

Recomputable : Pred A ℓ → Set _
Recomputable P = ∀ {x} → .(P x) → P x

------------------------------------------------------------------------
-- Operations on sets

infix 10 ⋃ ⋂
infixr 9 _⊢_
infixr 8 _⇒_
infixr 7 _∩_
infixr 6 _∪_
infix 4 _≬_

-- Complement.

∁ : Pred A ℓ → Pred A ℓ
∁ P = λ x → x ∉ P

-- Implication.

_⇒_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ⇒ Q = λ x → x ∈ P → x ∈ Q

-- Union.

_∪_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q

-- Intersection.

_∩_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ∩ Q = λ x → x ∈ P × x ∈ Q

-- Infinitary union.

⋃ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
⋃ I P = λ x → Σ[ i ∈ I ] P i x

syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P

-- Infinitary intersection.

⋂ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
⋂ I P = λ x → (i : I) → P i x

syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P

-- Positive version of non-disjointness, dual to inclusion.

_≬_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q

-- Update.

_⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
f ⊢ P = λ x → P (f x)

------------------------------------------------------------------------
-- Predicate combinators

-- These differ from the set operations above, as the carrier set of the
-- resulting predicates are not the same as the carrier set of the
-- component predicates.

infixr  2 _⟨×⟩_
infixr  2 _⟨⊙⟩_
infixr  1 _⟨⊎⟩_
infixr  0 _⟨→⟩_
infixl  9 _⟨·⟩_
infix  10 _~
infixr  9 _⟨∘⟩_
infixr  2 _//_ _\\_

-- Product.

_⟨×⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q

-- Sum over one element.

_⟨⊎⟩_ : Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
P ⟨⊎⟩ Q = [ P , Q ]

-- Sum over two elements.

_⟨⊙⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q

-- Implication.

_⟨→⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
(P ⟨→⟩ Q) f = P ⊆ Q ∘ f

-- Product.

_⟨·⟩_ : (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
(P ⟨·⟩ Q) (p , f) = f p

-- Converse.

_~ : Pred (A × B) ℓ → Pred (B × A) ℓ
P ~ = P ∘ swap

-- Composition.

_⟨∘⟩_ : Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
(P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q

-- Post-division.

_//_ : Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
(P // Q) (x , y) = Q ∘ (y ,_) ⊆ P ∘ (x ,_)

-- Pre-division.

_\\_ : Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
P \\ Q = (P ~ // Q ~) ~


text:
-- Andreas, 2016-06-20, issue #1891

-- Computation of which variables are splittable was wrong
-- in the presence of a where-module.

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

data D : Set where
  c : D

test : (x : D) → D
test x = {!x!}  -- C-c C-c
  where
   y = c

-- WAS:
-- Splitting on x reports:
-- Not a (splittable) variable: x
-- when checking that the expression ? has type D

-- Should work now.

-- Further tests:

record R (A : Set) : Set where
  testR : (x : D) → D
  testR x = {!x!}
    where B = A

module M (A : Set) where
  testM : (x : D) → D
  testM x = {!x!}
    where open R {A = A}


text:
open import Data.Nat    using (ℕ; _+_) renaming (_≤?_ to _≤?ₙ_)
open import Data.Bool   using (Bool; true; false; not; _∧_)
open import Data.String using (String; _≟_)
open import Data.Sum    using (_⊎_; [_,_]′; inj₁; inj₂)
open import Data.Product               using (_×_; _,_)
open import Relation.Nullary           using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.Product using (_×_; _,_; -,_; _-,-_; ∃; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Level using (Level; suc; _⊔_)

open import IMP
open import Hoare

data True {l} : Set l where
  ⊤ : True

data acom {l} : Set (suc l) where
  SKIP  : acom
  _::=_ : String → aexp → acom
  _::_  : acom {l} → acom {l} → acom
  IF_THEN_ELSE_ : bexp → acom {l} → acom {l} → acom
  WHILE[_]_DO_ : assn {l} → bexp → acom {l} → acom

strip : ∀{l} → acom {l} → com
strip SKIP = SKIP
strip (x ::= a) = x ::= a
strip (c₁ :: c₂) = strip c₁ :: strip c₂
strip (IF b THEN c₁ ELSE c₂) = IF b THEN strip c₁ ELSE strip c₂
strip (WHILE[ I ] b DO c) = WHILE b DO strip c

pre : ∀{l} → acom {l} → assn → assn
pre SKIP Q = Q
pre (x ::= a) Q s = Q (s [ x ::= aval a s ])
pre (c₁ :: c₂) Q = pre c₁ (pre c₂ Q)
pre (IF b THEN c₁ ELSE c₂) Q s with bval b s
... | true = pre c₁ Q s
... | false = pre c₂ Q s
pre (WHILE[ I ] b DO c) Q = I

vc : ∀{l} → acom {l} → assn → Set l
vc SKIP Q = True
vc (x ::= x₁) Q = True
vc (c₁ :: c₂) Q = vc c₁ (pre c₂ Q) × vc c₂ Q
vc (IF b THEN c₁ ELSE c₂) Q = vc c₁ Q × vc c₂ Q
vc (WHILE[ I ] b DO c) Q =
     (∀ s → I s × bval b s ≡ true  → pre c I s)
   × (∀ s → I s × bval b s ≡ false → Q s)
   × vc c I

extract-if-pre₁ : ∀{l} {Q : assn {l}} {c₁ c₂ s} b
  → pre (IF b THEN c₁ ELSE c₂) Q s
  × bval b s ≡ true
  → pre c₁ Q s
extract-if-pre₁ b (x , y) rewrite y = x

extract-if-pre₂ : ∀{l} {Q : assn {l}} {c₁ c₂ s} b
  → pre (IF b THEN c₁ ELSE c₂) Q s
  × bval b s ≡ false
  → pre c₂ Q s
extract-if-pre₂ b (x , y) rewrite y = x

vc-correctness : ∀{l} {P Q : assn} c
  → vc {l} c Q
  → (∀ s → P s → pre c Q s)
  → ⊢[ P ] strip c [ Q ]
vc-correctness SKIP v i = Conseq i Skip (λ s z → z)
vc-correctness (x ::= a) v i = Conseq i Loc (λ r k → k)
vc-correctness (c₁ :: c₂) v i = Comp (vc-correctness c₁ (Data.Product.proj₁ v) i)
                                     (vc-correctness c₂ (Data.Product.proj₂ v) (λ s z → z))
vc-correctness {l}{P}{Q} (IF b THEN c₁ ELSE c₂) (fst , snd) i =
     Conseq i (If (vc-correctness c₁ fst (λ s p → extract-if-pre₁ b p))
                  (vc-correctness c₂ snd (λ s p → extract-if-pre₂ b p)))
              (λ s z → z)
vc-correctness (WHILE[ I ] b DO c) (fst , fst₁ , snd) i =
    Conseq i (While (vc-correctness c snd fst)) fst₁

pre-mono : ∀{l} {P P′ : assn {l}} {s′} c
  → (∀ s → P s → P′ s)
  → pre c P s′ → pre c P′ s′
pre-mono {s′ = s′} SKIP x x₁ = x s′ x₁
pre-mono (x₂ ::= x₃) x x₁ = x _ x₁
pre-mono (c :: c₁) x x₁ = pre-mono c (λ s → pre-mono c₁ x) x₁
pre-mono {s′ = s′} (IF x₂ THEN c₁ ELSE c₂) x x₁ with bval x₂ s′
... | true  = pre-mono c₁ x x₁
... | false = pre-mono c₂ x x₁
pre-mono (WHILE[ x₂ ] x₃ DO c) x x₁ = x₁

vc-mono : ∀{l} {P P′ : assn {l}} c
  → (∀ s → P s → P′ s)
  → vc c P → vc c P′
vc-mono SKIP _ _ = ⊤
vc-mono (x ::= a) _ _ = ⊤
vc-mono (c₁ :: c₂) pp′ (vcpre , vc2) = vc-mono c₁ (λ _ → pre-mono c₂ pp′) vcpre , vc-mono c₂ pp′ vc2
vc-mono (IF b THEN c₁ ELSE c₂) pp′ (vc₁ , vc₂) = vc-mono c₁ pp′ vc₁ , vc-mono c₂ pp′ vc₂
vc-mono (WHILE[ I ] b DO c) pp′ (I₁ , I₂ , vcc) = I₁ , (λ s z → pp′ s (I₂ s z)) , vcc

either : ∀ c → c ≡ true ⊎ c ≡ false
either true  = inj₁ refl
either false = inj₂ refl

construct-if-pre : ∀{l} {P Q : assn {l}} {ac₁ ac₂} b s
   → (bval b s ≡ true  → pre ac₁ Q s)
   → (bval b s ≡ false → pre ac₂ Q s)
   → pre (IF b THEN ac₁ ELSE ac₂) Q s
construct-if-pre b s f g with bval b s
... | true = f refl
... | false = g refl

vc-completeness : ∀{l} {P Q : assn {l}} c
  → ⊢[ P ] c [ Q ]
  → ∃[ c̃ ] ( c ≡ strip c̃
           × vc c̃ Q
           × (∀ s → P s → pre c̃ Q s))
vc-completeness c Skip = SKIP , refl , ⊤ , (λ x c → c)
vc-completeness c Loc = _ , refl , ⊤ ,  (λ x c → c)
vc-completeness (c₁ :: c₂) (Comp x y) with vc-completeness c₁ x
... | ac₁ , b , c , d                 with vc-completeness c₂ y
... | ac₂ , f , g , h rewrite b | f
                      = (ac₁ :: ac₂) , refl
                      , (vc-mono ac₁ h c , g)
                      , (λ s ps → pre-mono ac₁ h (d s ps))
vc-completeness {P = P} (IF b THEN c₁ ELSE c₂) (If d₁ d₂) with vc-completeness c₁ d₁
... | ac₁ , f , g , h                                     with vc-completeness c₂ d₂
... | ac₂ , j , k , m rewrite f | j
                      = (IF b THEN ac₁ ELSE ac₂) , refl
                      , (g , k)
                      , (λ s ps → construct-if-pre {P = P} b s (λ t → h s (ps , t)) (λ f → m s (ps , f)))
vc-completeness (WHILE b DO c) (While r) with vc-completeness c r
... | ac , f , g , h rewrite f = (WHILE[ _ ] b DO ac) , refl
                               , (h , (λ s z → z) , g)
                               , λ s z → z
vc-completeness c (Conseq x₁ r x₂) with vc-completeness c r
... | ac , f , g , h rewrite f
                     = ac , refl
                     , vc-mono ac x₂ g
                     , (λ s ps → pre-mono ac x₂ (h s (x₁ s ps)))

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
module Category.Monoidal where

open import Category.NatIsomorphism

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
module Data.QuadTree.FoldableProofs.FoldableProof where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Logic
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.SafeFunctions
open import Data.QuadTree.Implementation.PropDepthRelation
open import Data.QuadTree.Implementation.Foldable

-- All proofs for Foldables

-- foldr f z t = appEndo (foldMap (Endo . f) t ) z
-- foldl f z t = appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z
-- fold = foldMap id
-- length = getSum . foldMap (Sum . const 1)
-- I didn't change the default implementations of foldl/foldr/fold/length, so these laws should all hold

-- However, I will proof that the length of the quadtree is equal to width * height.
-- lengthₑ quadtreeFoldable vqt ≡ size vqt

size : {t : Set} {{eqT : Eq t}} {dep : Nat} -> (vqt : VQuadTree t {dep}) -> Nat
size (CVQuadTree (Wrapper (w , h) x₁)) = w * h

lengthₙ : {t : Set → Set} ⦃ r : Foldable t ⦄ {a : Set} → t a → Nat
lengthₙ {{r}} = foldMap {{r}} {{ MonoidSum }} (const 1)

length-replicateₙ : {t : Set} (n : Nat) (v : t) -> lengthₙ (replicateₙ n v) ≡ n
length-replicateₙ {t} Z v = refl
length-replicateₙ {t} (S n) v =
    begin
        lengthₙ (replicateₙ (S n) v)
    =⟨⟩
        S (lengthₙ (replicateₙ n v))
    =⟨ cong S (length-replicateₙ n v ) ⟩
        S n
    end

length-concat-sub : {t : Set} -> (list : List t) (lists : List (List t)) -> lengthₙ (list ++ concat lists) ≡ lengthₙ list + lengthₙ (concat lists)
length-concat-sub {t} [] lists = refl
length-concat-sub {t} (x ∷ xs) lists =
    begin
        lengthₙ ((x ∷ xs) ++ concat lists)
    =⟨⟩
        S (lengthₙ (xs ++ concat lists))
    =⟨ cong S (length-concat-sub xs lists) ⟩
        lengthₙ (x ∷ xs) + lengthₙ (concat lists)
    end

length-concat : {t : Set} -> (lists : List (List t)) -> lengthₙ (concat lists) ≡ sum (map lengthₙ lists)
length-concat {t} [] = refl
length-concat {t} (list ∷ lists) =
    begin
        lengthₙ (concat (list ∷ lists))
    =⟨⟩
        lengthₙ (list ++ concat lists)
    =⟨ length-concat-sub list lists ⟩
        lengthₙ list + lengthₙ (concat lists)
    =⟨ cong (λ q -> lengthₙ list + q) (length-concat lists) ⟩
        lengthₙ list + sum (map lengthₙ lists)
    =⟨⟩
        sum (map lengthₙ (list ∷ lists))
    end

concat-nothing : {t : Set} -> (list : List t) -> list ++ [] ≡ list
concat-nothing [] = refl
concat-nothing (x ∷ list) = cong (λ z → x ∷ z) (concat-nothing list)

diff-n-zero : (n : Nat) -> diff n Z ≡ n
diff-n-zero Z = refl
diff-n-zero (S n) = refl

map-concat : {s t : Set} -> (a b : List s)
    -> (f : s -> t)
    -> map f (a ++ b) ≡ map f a ++ map f b
map-concat [] b f = refl
map-concat (a ∷ as) b f = cong (λ z → f a ∷ z) (map-concat as b f)

map-concat4 : {s t : Set} -> (a b c d : List s)
    -> (f : s -> t)
    -> map f (a ++ b ++ c ++ d) ≡ map f a ++ map f b ++ map f c ++ map f d
map-concat4 a b c d f =
    begin
        map f (a ++ b ++ c ++ d)
    =⟨ map-concat a (b ++ c ++ d) f ⟩
        map f a ++ map f (b ++ c ++ d)
    =⟨ cong (λ q -> map f a ++ q) (map-concat b (c ++ d) f) ⟩
        map f a ++ map f b ++ map f (c ++ d)
    =⟨ cong (λ q -> map f a ++ map f b ++ q) (map-concat c d f) ⟩
        map f a ++ map f b ++ map f c ++ map f d
    end

sum-concat : (a b : List Nat) -> sum (a ++ b) ≡ sum a + sum b
sum-concat [] b = refl
sum-concat (a ∷ as) b =
    begin
        a + sum (as ++ b)
    =⟨ cong (λ q -> a + q) (sum-concat as b) ⟩
        a + (sum as + sum b)
    =⟨ sym $ add-assoc a (sum as) (sum b) ⟩
        sum (a ∷ as) + sum b
    end

sum-concat4 : (a b c d : List Nat) -> sum (a ++ b ++ c ++ d) ≡ sum a + sum b + sum c + sum d
sum-concat4 a b c d =
    begin
        sum (a ++ b ++ c ++ d)
    =⟨ sum-concat a (b ++ c ++ d) ⟩
        sum a + sum (b ++ c ++ d)
    =⟨ cong (λ q -> sum a + q) (sum-concat b (c ++ d)) ⟩
        sum a + (sum b + sum (c ++ d))
    =⟨ cong (λ q -> sum a + (sum b + q)) (sum-concat c d) ⟩
        sum a + (sum b + (sum c + sum d))
    =⟨ sym $ add-assoc (sum a) (sum b) (sum c + sum d) ⟩
        (sum a + sum b) + (sum c + sum d)
    =⟨ sym $ add-assoc (sum a + sum b) (sum c) (sum d) ⟩
        sum a + sum b + sum c + sum d
    end

nat-distributive : (a b c : Nat) -> (a * c) + (b * c) ≡ (a + b) * c
nat-distributive Z b c = refl
nat-distributive (S a) b c =
    begin
        (S a * c) + (b * c)
    =⟨ add-assoc c (a * c) (b * c) ⟩
        c + ((a * c) + b * c)
    =⟨ cong (_+_ c) (nat-distributive a b c) ⟩
        c + ((a + b) * c)
    =⟨⟩
        (S a + b) * c
    end

add-diff : (a b : Nat) -> IsTrue (a <= b) -> a + diff b a ≡ b
add-diff Z Z ab = refl
add-diff Z (S b) ab = refl
add-diff (S a) (S b) ab = cong S (add-diff a b ab)

line-split-left : (x1 xm x2 y : Nat) -> IsTrue (x1 <= xm) -> IsTrue (xm <= x2) -> IsTrue (x1 <= x2)
    -> diff xm x1 * y + diff x2 xm * y ≡ diff x2 x1 * y
line-split-left Z Z Z y x1m xm2 x12 = refl
line-split-left Z Z (S x2) y x1m xm2 x12 = refl
line-split-left Z (S xm) (S x2) y x1m xm2 x12 =
    begin
        (S xm) * y + diff (S x2) (S xm) * y
    =⟨ nat-distributive (S xm) (diff (S x2) (S xm)) y ⟩
        ((S xm) + diff (S x2) (S xm)) * y
    =⟨ cong (λ z → y + (z * y)) (add-diff xm x2 xm2) ⟩
        (S x2) * y
    end
line-split-left (S x1) (S xm) (S x2) y x1m xm2 x12 = line-split-left x1 xm x2 y x1m xm2 x12

line-split-right : (x1 xm x2 y : Nat) -> IsTrue (x1 <= xm) -> IsTrue (xm <= x2) -> IsTrue (x1 <= x2)
    -> y * diff xm x1 + y * diff x2 xm ≡ y * diff x2 x1
line-split-right x1 xm x2 y x1m xm2 x12 =
    begin
        y * diff xm x1 + y * diff x2 xm
    =⟨ cong2 _+_ (mul-comm y (diff xm x1)) (mul-comm y (diff x2 xm)) ⟩
        diff xm x1 * y + diff x2 xm * y
    =⟨ line-split-left x1 xm x2 y x1m xm2 x12 ⟩
        diff x2 x1 * y
    =⟨ mul-comm (diff x2 x1) y ⟩
        y * diff x2 x1
    end

square-split : (x1 y1 xm ym x2 y2 : Nat) -> IsTrue (x1 <= xm) -> IsTrue (xm <= x2) -> IsTrue (y1 <= ym) -> IsTrue (ym <= y2)
    -> diff xm x1 * diff ym y1 + diff x2 xm * diff ym y1 + diff xm x1 * diff y2 ym + diff x2 xm * diff y2 ym ≡ diff x2 x1 * diff y2 y1
square-split x1 y1 xm ym x2 y2 x1m xm2 y1m ym2 =
    begin
        diff xm x1 * diff ym y1 + diff x2 xm * diff ym y1 + diff xm x1 * diff y2 ym + diff x2 xm * diff y2 ym
    =⟨ add-assoc ((diff xm x1 * diff ym y1) + (diff x2 xm * diff ym y1)) (diff xm x1 * diff y2 ym) (diff x2 xm * diff y2 ym) ⟩
        (diff xm x1 * diff ym y1 + diff x2 xm * diff ym y1) + (diff xm x1 * diff y2 ym + diff x2 xm * diff y2 ym)
    =⟨ cong2 _+_
        (line-split-left x1 xm x2 (diff ym y1) x1m xm2 (lteTransitive x1 xm x2 x1m xm2))
        (line-split-left x1 xm x2 (diff y2 ym) x1m xm2 (lteTransitive x1 xm x2 x1m xm2)) ⟩
        (diff x2 x1 * diff ym y1) + (diff x2 x1 * diff y2 ym)
    =⟨ line-split-right y1 ym y2 (diff x2 x1) y1m ym2 (lteTransitive y1 ym y2 y1m ym2) ⟩
        diff x2 x1 * diff y2 y1
    end

min-comb : (a b c : Nat) -> IsTrue (a <= b) -> IsTrue (a <= c) -> IsTrue (a <= min b c)
min-comb a b c ab ac = useEq (sym $
    begin
        a <= min b c
    =⟨ sym $ propFnIf {c = c < b} (_<=_ a) ⟩
        (if _ then a <= c else a <= b)
    =⟨ cong2 (if_then_else_ _) (isTrueToEquiv ac) (isTrueToEquiv ab)  ⟩
        (if _ then true else true)
    =⟨ propIfBranchesSame true ⟩
        true
    end) IsTrue.itsTrue

min-rel-1 : (x1 mid x2 : Nat) -> IsTrue (x1 <= x2) -> IsTrue (x1 <= min x2 (mid + x1))
min-rel-1 x1 mid x2 x12 = min-comb x1 x2 (mid + x1) x12 (lteSumOne x1 x1 mid (lteSelf x1))

min-rel-2 : (a b : Nat) -> IsTrue (min a b <= a)
min-rel-2 a b = useEq (sym $
    begin
        min a b <= a
    =⟨ sym (propFnIf (λ z → (z <= a))) ⟩
        (if b < a then b <= a else a <= a)
    =⟨ ifTrueMap {c = b < a} (λ c -> isTrueToEquiv (orFst c)) ⟩
        (if b < a then true else a <= a)
    =⟨ cong (if_then_else_ (b < a) true) (isTrueToEquiv (lteSelf a)) ⟩
        (if b < a then true else true)
    =⟨ propIfBranchesSame true ⟩
        true
    end) IsTrue.itsTrue

length-tilesQd : {t : Set} {{eqT : Eq t}} {dep : Nat} -> (vqd : VQuadrant t {dep})
    -> (x1 y1 x2 y2 : Nat) -> IsTrue (x1 <= x2) -> IsTrue (y1 <= y2)
    -> sum (map lengthₙ (map expand (tilesQd dep vqd (RegionC (x1 , y1) (x2 , y2))))) ≡ diff x2 x1 * diff y2 y1
length-tilesQd {t} {dep = dep} (CVQuadrant (Leaf v) {p}) x1 y1 x2 y2 _ _ =
    begin
        sum (map lengthₙ (map expand (tilesQd dep (CVQuadrant (Leaf v) {p}) (RegionC (x1 , y1) (x2 , y2)))))
    =⟨⟩
        lengthₙ (replicateₙ (diff x2 x1 * diff y2 y1) v) + 0
    =⟨ add-comm _ 0 ⟩
        lengthₙ (replicateₙ (diff x2 x1 * diff y2 y1) v)
    =⟨ length-replicateₙ (diff x2 x1 * diff y2 y1) v ⟩
        diff x2 x1 * diff y2 y1
    end
length-tilesQd {dep = S dep} (CVQuadrant (Node a b c d) {p}) x1 y1 x2 y2 xp yp =
    begin
        sum (map lengthₙ (map expand (tilesQd (S dep) (CVQuadrant (Node a b c d) {p}) (RegionC (x1 , y1) (x2 , y2)))))
    =⟨⟩
        sum (map lengthₙ (map expand (ca ++ cb ++ cc ++ cd)))
    =⟨ cong (λ q -> sum (map lengthₙ q)) (map-concat4 ca cb cc cd expand) ⟩
        sum (map lengthₙ (map expand ca  ++ map expand cb ++ map expand cc ++ map expand cd))
    =⟨ cong sum (map-concat4 (map expand ca) (map expand cb) (map expand cc) (map expand cd) lengthₙ) ⟩
        sum (map lengthₙ (map expand ca) ++ map lengthₙ (map expand cb) ++ map lengthₙ (map expand cc) ++ map lengthₙ (map expand cd))
    =⟨ sum-concat4 (map lengthₙ (map expand ca)) (map lengthₙ (map expand cb)) (map lengthₙ (map expand cc)) (map lengthₙ (map expand cd)) ⟩
        sum (map lengthₙ (map expand ca)) + sum (map lengthₙ (map expand cb)) + sum (map lengthₙ (map expand cc)) + sum (map lengthₙ (map expand cd))
    =⟨ cong4 (λ a b c d -> a + b + c + d)
        (length-tilesQd (CVQuadrant a) x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) (min-rel-1 x1 mid x2 xp) (min-rel-1 y1 mid y2 yp))
        (length-tilesQd (CVQuadrant b) (min x2 (mid + x1)) y1 x2 (min y2 (mid + y1)) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp))
        (length-tilesQd (CVQuadrant c) x1 (min y2 (mid + y1)) (min x2 (mid + x1)) y2 (min-rel-1 x1 mid x2 xp) (min-rel-2 y2 (mid + y1)))
        (length-tilesQd (CVQuadrant d) (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2 (min-rel-2 x2 (mid + x1)) (min-rel-2 y2 (mid + y1))) ⟩
          diff (min x2 (mid + x1)) x1 * diff (min y2 (mid + y1)) y1
        + diff x2 (min x2 (mid + x1)) * diff (min y2 (mid + y1)) y1
        + diff (min x2 (mid + x1)) x1 * diff y2 (min y2 (mid + y1))
        + diff x2 (min x2 (mid + x1)) * diff y2 (min y2 (mid + y1))
    =⟨ square-split x1 y1 (min x2 (mid + x1)) (min y2 (mid + y1)) x2 y2 (min-rel-1 x1 mid x2 xp) (min-rel-2 x2 (mid + x1)) (min-rel-1 y1 mid y2 yp) (min-rel-2 y2 (mid + y1)) ⟩
        diff x2 x1 * diff y2 y1
    end where
        mid = pow 2 dep
        ca = tilesQd dep (CVQuadrant a) (RegionC (x1 , y1) (min x2 (mid + x1) , min y2 (mid + y1)) )
        cb = tilesQd dep (CVQuadrant b) (RegionC (min x2 (mid + x1) , y1) (x2 , min y2 (mid + y1)) )
        cc = tilesQd dep (CVQuadrant c) (RegionC (x1 , min y2 (mid + y1)) (min x2 (mid + x1) , y2) )
        cd = tilesQd dep (CVQuadrant d) (RegionC (min x2 (mid + x1) , min y2 (mid + y1)) (x2 , y2) )

proof-length : {t : Set} {{eqT : Eq t}} {dep : Nat} -> (vqt : VQuadTree t {dep}) -> lengthₑ (quadtreeFoldable dep) vqt ≡ size vqt
proof-length {t} ⦃ eqT ⦄ {dep} vqt@(CVQuadTree (Wrapper (w , h) qd) {p1} {p2}) =
    begin
        lengthₑ (quadtreeFoldable dep) vqt
    =⟨⟩
        lengthₙ (concat (map expand (tilesQd dep (CVQuadrant qd {p1}) (RegionC (0 , 0) (w , h)))))
    =⟨ length-concat (map expand (tilesQd dep (CVQuadrant qd {p1}) (RegionC (0 , 0) (w , h)))) ⟩
        sum (map lengthₙ (map expand (tilesQd dep (CVQuadrant qd {p1}) (RegionC (0 , 0) (w , h)))))
    =⟨ length-tilesQd {dep = dep} (CVQuadrant qd {p1}) 0 0 w h (zeroLteAny w) (zeroLteAny h) ⟩
        w * h
    end

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

-- This file is a glorious testament to all of agda's greatest strengths -
-- a beautiful work that will shine brightly throughout the ages and instill
-- hope for the future in many generations to come. May I never use any other
-- proof assistant.
module decidability where
  mutual
    -- We define context decidability in contexts.agda,
    -- because it's an important metatheorem. However, it accepts a
    -- decidability theorem for its value type, and for environments that
    -- value type is result, so the termination checker complains. To fix
    -- this, we redefine type-specific versions of this theorem here.
    -- Note that we really should not be destructing contexts via `_::_` -
    -- here we only do that because we copied this code from the contexts file.

    ctx<result>-==-dec : (Γ1 Γ2 : result ctx) →
                          Γ1 == Γ2 ∨ Γ1 ≠ Γ2
    ctx<result>-==-dec [] []       = Inl refl
    ctx<result>-==-dec [] (_ :: _) = Inr (λ ())
    ctx<result>-==-dec (_ :: _) [] = Inr (λ ())
    ctx<result>-==-dec ((hx1 , hr1) :: t1) ((hx2 , hr2) :: t2)
      with natEQ hx1 hx2 | result-==-dec hr1 hr2 | ctx<result>-==-dec t1 t2
    ... | Inl refl | Inl refl | Inl refl = Inl refl
    ... | Inl refl | Inl refl | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl | Inr ne   | _        = Inr λ where refl → ne refl
    ... | Inr ne   | _        | _        = Inr λ where refl → ne refl

    ctx<rule>-==-dec : (rules1 rules2 : rule ctx) →
                        rules1 == rules2 ∨ rules1 ≠ rules2
    ctx<rule>-==-dec [] [] = Inl refl
    ctx<rule>-==-dec [] (_ :: _) = Inr (λ ())
    ctx<rule>-==-dec (_ :: _) [] = Inr (λ ())
    ctx<rule>-==-dec ((hx1 , hrule1) :: t1) ((hx2 , hrule2) :: t2)
      with natEQ hx1 hx2 | rule-==-dec hrule1 hrule2 | ctx<rule>-==-dec t1 t2
    ... | Inl refl | Inl refl | Inl refl = Inl refl
    ... | Inl refl | Inl refl | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl | Inr ne   | _        = Inr λ where refl → ne refl
    ... | Inr ne   | _        | _        = Inr λ where refl → ne refl

    rule-==-dec : (rule1 rule2 : rule) →
                   rule1 == rule2 ∨ rule1 ≠ rule2
    rule-==-dec (|C parm1 => branch1) (|C parm2 => branch2)
      with natEQ parm1 parm2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with exp-==-dec branch1 branch2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl

    ex-==-dec : (ex1 ex2 : ex) →
                 ex1 == ex2 ∨ ex1 ≠ ex2
    ex-==-dec ⟨⟩ ⟨⟩ = Inl refl
    ex-==-dec ⟨⟩ ⟨ ex2 , ex3 ⟩ = Inr (λ ())
    ex-==-dec ⟨⟩ (C[ x ] ex2) = Inr (λ ())
    ex-==-dec ⟨⟩ ¿¿ = Inr (λ ())
    ex-==-dec ⟨⟩ (x ↦ ex2) = Inr (λ ())
    ex-==-dec ⟨ ex1a , ex1b ⟩ ⟨ ex2a , ex2b ⟩
      with ex-==-dec ex1a ex2a
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with ex-==-dec ex1b ex2b
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    ex-==-dec ⟨ ex1 , ex2 ⟩ ⟨⟩ = Inr (λ ())
    ex-==-dec ⟨ _ , _ ⟩ (C[ _ ] _) = Inr (λ ())
    ex-==-dec ⟨ ex1 , ex2 ⟩ ¿¿ = Inr (λ ())
    ex-==-dec ⟨ ex1 , ex2 ⟩ (x ↦ ex3) = Inr (λ ())
    ex-==-dec (C[ c1 ] ex1) (C[ c2 ] ex2)
      with natEQ c1 c2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with ex-==-dec ex1 ex2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    ex-==-dec (C[ x ] ex1) ⟨⟩ = Inr (λ ())
    ex-==-dec (C[ _ ] _) ⟨ _ , _ ⟩ = Inr (λ ())
    ex-==-dec (C[ x ] ex1) ¿¿ = Inr (λ ())
    ex-==-dec (C[ x ] ex1) (x₁ ↦ ex2) = Inr (λ ())
    ex-==-dec ¿¿ ¿¿ = Inl refl
    ex-==-dec ¿¿ ⟨⟩ = Inr (λ ())
    ex-==-dec ¿¿ ⟨ ex2 , ex3 ⟩ = Inr (λ ())
    ex-==-dec ¿¿ (C[ x ] ex2) = Inr (λ ())
    ex-==-dec ¿¿ (x ↦ ex2) = Inr (λ ())
    ex-==-dec (v1 ↦ ex1) (v2 ↦ ex2)
      with result-==-dec v1 v2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with ex-==-dec ex1 ex2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    ex-==-dec (x ↦ ex1) ⟨⟩ = Inr (λ ())
    ex-==-dec (x ↦ ex1) ⟨ ex2 , ex3 ⟩ = Inr (λ ())
    ex-==-dec (x ↦ ex1) (C[ x₁ ] ex2) = Inr (λ ())
    ex-==-dec (x ↦ ex1) ¿¿ = Inr (λ ())

    exp-==-dec : (e1 e2 : exp) → e1 == e2 ∨ e1 ≠ e2
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ fix f2 ⦇·λ x2 => e2 ·⦈
      with natEQ f1 f2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with natEQ x1 x2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with exp-==-dec e1 e2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ X[ x ] = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ (e2 ∘ e3) = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ ⟨⟩ = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ (fst _) = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ (snd _) = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ (C[ x ] e2) = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ ??[ x ] = Inr (λ ())
    exp-==-dec fix f1 ⦇·λ x1 => e1 ·⦈ (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec X[ x1 ] X[ x2 ]
      with natEQ x1 x2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec X[ x1 ] fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec X[ x1 ] (e2 ∘ e3) = Inr (λ ())
    exp-==-dec X[ x1 ] ⟨⟩ = Inr (λ ())
    exp-==-dec X[ x1 ] ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec X[ x1 ] (fst _) = Inr (λ ())
    exp-==-dec X[ x1 ] (snd _) = Inr (λ ())
    exp-==-dec X[ x1 ] (C[ x ] e2) = Inr (λ ())
    exp-==-dec X[ x1 ] case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec X[ x1 ] ??[ x ] = Inr (λ ())
    exp-==-dec X[ x1 ] (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) (ef2 ∘ earg2)
      with exp-==-dec ef1 ef2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with exp-==-dec earg1 earg2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec (ef1 ∘ earg1) fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) X[ x ] = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) ⟨⟩ = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) (fst _) = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) (snd _) = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) (C[ x ] e2) = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) ??[ x ] = Inr (λ ())
    exp-==-dec (ef1 ∘ earg1) (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec ⟨⟩ ⟨⟩ = Inl refl
    exp-==-dec ⟨⟩ fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec ⟨⟩ X[ x ] = Inr (λ ())
    exp-==-dec ⟨⟩ (e2 ∘ e3) = Inr (λ ())
    exp-==-dec ⟨⟩ ⟨ e2 , e3 ⟩ = Inr (λ ())
    exp-==-dec ⟨⟩ (fst e2) = Inr (λ ())
    exp-==-dec ⟨⟩ (snd e2) = Inr (λ ())
    exp-==-dec ⟨⟩ (C[ x ] e2) = Inr (λ ())
    exp-==-dec ⟨⟩ case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec ⟨⟩ ??[ x ] = Inr (λ ())
    exp-==-dec ⟨⟩ (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec ⟨ es1a , es1b ⟩ ⟨ es2a , es2b ⟩
      with exp-==-dec es1a es2a
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with exp-==-dec es1b es2b
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec ⟨ _ , _ ⟩ fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ X[ x ] = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ (e2 ∘ e3) = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ ⟨⟩ = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ (fst _) = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ (snd _) = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ (C[ x ] e2) = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ ??[ x ] = Inr (λ ())
    exp-==-dec ⟨ _ , _ ⟩ (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec (fst e1) (fst e2)
      with exp-==-dec e1 e2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec (fst e1) fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec (fst e1) X[ x ] = Inr (λ ())
    exp-==-dec (fst e1) (e2 ∘ e3) = Inr (λ ())
    exp-==-dec (fst e1) ⟨⟩ = Inr (λ ())
    exp-==-dec (fst e1) ⟨ e2 , e3 ⟩ = Inr (λ ())
    exp-==-dec (fst e1) (snd e2) = Inr (λ ())
    exp-==-dec (fst e1) (C[ x ] e2) = Inr (λ ())
    exp-==-dec (fst e1) case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec (fst e1) ??[ x ] = Inr (λ ())
    exp-==-dec (fst e1) (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec (snd e1) (snd e2)
      with exp-==-dec e1 e2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec (snd e1) fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec (snd e1) X[ x ] = Inr (λ ())
    exp-==-dec (snd e1) (e2 ∘ e3) = Inr (λ ())
    exp-==-dec (snd e1) ⟨⟩ = Inr (λ ())
    exp-==-dec (snd e1) ⟨ e2 , e3 ⟩ = Inr (λ ())
    exp-==-dec (snd e1) (fst e2) = Inr (λ ())
    exp-==-dec (snd e1) (C[ x ] e2) = Inr (λ ())
    exp-==-dec (snd e1) case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec (snd e1) ??[ x ] = Inr (λ ())
    exp-==-dec (snd e1) (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) (C[ c2 ] e2)
      with natEQ c1 c2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with exp-==-dec e1 e2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec (C[ c1 ] e1) fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) X[ x ] = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) (e2 ∘ e3) = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) ⟨⟩ = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) (fst _) = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) (snd _) = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) ??[ x ] = Inr (λ ())
    exp-==-dec (C[ c1 ] e1) (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ case e2 of⦃· rules2 ·⦄
      with exp-==-dec e1 e2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with ctx<rule>-==-dec rules1 rules2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec case e1 of⦃· rules1 ·⦄ fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ X[ x ] = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ (e2 ∘ e3) = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ ⟨⟩ = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ (fst _) = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ (snd _) = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ (C[ x ] e2) = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ ??[ x ] = Inr (λ ())
    exp-==-dec case e1 of⦃· rules1 ·⦄ (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec ??[ u1 ] ??[ u2 ]
      with natEQ u1 u2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec ??[ u1 ] fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec ??[ u1 ] X[ x ] = Inr (λ ())
    exp-==-dec ??[ u1 ] (e2 ∘ e3) = Inr (λ ())
    exp-==-dec ??[ u1 ] ⟨⟩ = Inr (λ ())
    exp-==-dec ??[ u1 ] ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec ??[ u1 ] (fst _) = Inr (λ ())
    exp-==-dec ??[ u1 ] (snd _) = Inr (λ ())
    exp-==-dec ??[ u1 ] (C[ x ] e2) = Inr (λ ())
    exp-==-dec ??[ u1 ] case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec ??[ u1 ] (PBE:assert e2 e3) = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) (PBE:assert e2a e2b)
      with exp-==-dec e1a e2a
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl
      with exp-==-dec e1b e2b
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    exp-==-dec (PBE:assert e1a e1b) fix x ⦇·λ x₁ => e2 ·⦈ = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) X[ x ] = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) (e2 ∘ e3) = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) ⟨⟩ = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) ⟨ _ , _ ⟩ = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) (fst _) = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) (snd _) = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) (C[ x ] e2) = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) case e2 of⦃· x ·⦄ = Inr (λ ())
    exp-==-dec (PBE:assert e1a e1b) ??[ x ] = Inr (λ ())

    result-==-dec : (r1 r2 : result) → r1 == r2 ∨ r1 ≠ r2
    result-==-dec [ E1 ]fix f1 ⦇·λ x1 => e1 ·⦈ [ E2 ]fix f2 ⦇·λ x2 => e2 ·⦈
      with ctx<result>-==-dec E1 E2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with natEQ f1 f2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with natEQ x1 x2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with exp-==-dec e1 e2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ ⟨⟩ = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ ⟨ _ , _ ⟩ = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ (C[ _ ] _) = Inr (λ ())
    result-==-dec [ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ (C⁻[ x₄ ] r2) = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ [ _ ]??[ _ ] = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ (_ ∘ _) = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ (fst _) = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ (snd _) = Inr (λ ())
    result-==-dec [ E ]fix f ⦇·λ x => e ·⦈ [ _ ]case _ of⦃· _ ·⦄ = Inr (λ ())
    result-==-dec ⟨⟩ ⟨⟩ = Inl refl
    result-==-dec ⟨⟩ [ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ = Inr (λ ())
    result-==-dec ⟨⟩ ⟨ r2 , r3 ⟩ = Inr (λ ())
    result-==-dec ⟨⟩ (C[ x ] r2) = Inr (λ ())
    result-==-dec ⟨⟩ (C⁻[ x ] r2) = Inr (λ ())
    result-==-dec ⟨⟩ [ x ]??[ x₁ ] = Inr (λ ())
    result-==-dec ⟨⟩ (r2 ∘ r3) = Inr (λ ())
    result-==-dec ⟨⟩ (fst r2) = Inr (λ ())
    result-==-dec ⟨⟩ (snd r2) = Inr (λ ())
    result-==-dec ⟨⟩ [ x ]case r2 of⦃· x₁ ·⦄ = Inr (λ ())
    result-==-dec ⟨ rs1a , rs1b ⟩ ⟨ rs2a , rs2b ⟩
      with result-==-dec rs1a rs2a
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with result-==-dec rs1b rs2b
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec ⟨ _ , _ ⟩ [ _ ]fix _ ⦇·λ _ => _ ·⦈ = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ ⟨⟩ = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ (C[ _ ] _) = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ (C⁻[ x ] r3) = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ [ _ ]??[ _ ] = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ (_ ∘ _) = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ (snd _) = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ (fst _) = Inr (λ ())
    result-==-dec ⟨ _ , _ ⟩ [ _ ]case _ of⦃· _ ·⦄ = Inr (λ ())
    result-==-dec (C[ c1 ] r1) (C[ c2 ] r2)
      with natEQ c1 c2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with result-==-dec r1 r2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec (C[ c ] r) [ _ ]fix _ ⦇·λ _ => _ ·⦈ = Inr (λ ())
    result-==-dec (C[ c ] r) ⟨⟩ = Inr (λ ())
    result-==-dec (C[ c ] r) ⟨ _ , _ ⟩ = Inr (λ ())
    result-==-dec (C[ x ] r1) (C⁻[ x₁ ] r2) = Inr (λ ())
    result-==-dec (C[ c ] r) [ _ ]??[ _ ] = Inr (λ ())
    result-==-dec (C[ c ] r) (_ ∘ _) = Inr (λ ())
    result-==-dec (C[ c ] r) (fst _) = Inr (λ ())
    result-==-dec (C[ c ] r) (snd _) = Inr (λ ())
    result-==-dec (C[ c ] r) [ _ ]case _ of⦃· _ ·⦄ = Inr (λ ())
    result-==-dec (C⁻[ c1 ] r1) (C⁻[ c2 ] r2)
      with natEQ c1 c2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with result-==-dec r1 r2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec (C⁻[ x ] r1) [ x₁ ]fix x₂ ⦇·λ x₃ => x₄ ·⦈ = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) ⟨⟩ = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) ⟨ r2 , r3 ⟩ = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) (C[ x₁ ] r2) = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) [ x₁ ]??[ x₂ ] = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) (r2 ∘ r3) = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) (fst r2) = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) (snd r2) = Inr (λ ())
    result-==-dec (C⁻[ x ] r1) [ x₁ ]case r2 of⦃· x₂ ·⦄ = Inr (λ ())
    result-==-dec [ E1 ]??[ u1 ] [ E2 ]??[ u2 ]
      with ctx<result>-==-dec E1 E2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with natEQ u1 u2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec [ E ]??[ u1 ] [ _ ]fix _ ⦇·λ _ => _ ·⦈ = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] ⟨⟩ = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] ⟨ _ , _ ⟩ = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] (C[ _ ] _) = Inr (λ ())
    result-==-dec [ x ]??[ x₁ ] (C⁻[ x₂ ] r2) = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] (_ ∘ _) = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] (fst _) = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] (snd _) = Inr (λ ())
    result-==-dec [ E ]??[ u1 ] [ _ ]case _ of⦃· _ ·⦄ = Inr (λ ())
    result-==-dec (rf1 ∘ rarg1) (rf2 ∘ rarg2)
      with result-==-dec rf1 rf2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with result-==-dec rarg1 rarg2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec (rf ∘ rarg) [ _ ]fix _ ⦇·λ _ => _ ·⦈ = Inr (λ ())
    result-==-dec (rf ∘ rarg) ⟨⟩ = Inr (λ ())
    result-==-dec (rf ∘ rarg) ⟨ _ , _ ⟩ = Inr (λ ())
    result-==-dec (rf ∘ rarg) (C[ _ ] _) = Inr (λ ())
    result-==-dec (r1 ∘ r2) (C⁻[ x ] r3) = Inr (λ ())
    result-==-dec (rf ∘ rarg) [ _ ]??[ _ ] = Inr (λ ())
    result-==-dec (rf ∘ rarg) (fst _) = Inr (λ ())
    result-==-dec (rf ∘ rarg) (snd _) = Inr (λ ())
    result-==-dec (rf ∘ rarg) [ _ ]case _ of⦃· _ ·⦄ = Inr (λ ())
    result-==-dec (fst r1) (fst r2)
      with result-==-dec r1 r2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    result-==-dec (fst r1) [ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ = Inr (λ ())
    result-==-dec (fst r1) ⟨⟩ = Inr (λ ())
    result-==-dec (fst r1) ⟨ r2 , r3 ⟩ = Inr (λ ())
    result-==-dec (fst r1) (C[ x ] r2) = Inr (λ ())
    result-==-dec (fst r1) (C⁻[ x ] r2) = Inr (λ ())
    result-==-dec (fst r1) [ x ]??[ x₁ ] = Inr (λ ())
    result-==-dec (fst r1) (r2 ∘ r3) = Inr (λ ())
    result-==-dec (fst r1) (snd r2) = Inr (λ ())
    result-==-dec (fst r1) [ x ]case r2 of⦃· x₁ ·⦄ = Inr (λ ())
    result-==-dec (snd r1) (snd r2)
      with result-==-dec r1 r2
    ... | Inr ne   = Inr (λ where refl → ne refl)
    ... | Inl refl = Inl refl
    result-==-dec (snd r1) [ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ = Inr (λ ())
    result-==-dec (snd r1) ⟨⟩ = Inr (λ ())
    result-==-dec (snd r1) ⟨ r2 , r3 ⟩ = Inr (λ ())
    result-==-dec (snd r1) (C[ x ] r2) = Inr (λ ())
    result-==-dec (snd r1) (C⁻[ x ] r2) = Inr (λ ())
    result-==-dec (snd r1) [ x ]??[ x₁ ] = Inr (λ ())
    result-==-dec (snd r1) (r2 ∘ r3) = Inr (λ ())
    result-==-dec (snd r1) (fst r2) = Inr (λ ())
    result-==-dec (snd r1) [ x ]case r2 of⦃· x₁ ·⦄ = Inr (λ ())
    result-==-dec [ E1 ]case r1 of⦃· rules1 ·⦄ [ E2 ]case r2 of⦃· rules2 ·⦄
      with ctx<result>-==-dec E1 E2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with result-==-dec r1 r2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl
      with ctx<rule>-==-dec rules1 rules2
    ... | Inr ne   = Inr λ where refl → ne refl
    ... | Inl refl = Inl refl
    result-==-dec [ E ]case r of⦃· rules ·⦄ [ _ ]fix _ ⦇·λ _ => _ ·⦈ = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ ⟨⟩ = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ ⟨ _ , _ ⟩ = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ (C[ _ ] _) = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ [ _ ]??[ _ ] = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ (_ ∘ _) = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ (fst _) = Inr (λ ())
    result-==-dec [ E ]case r of⦃· rules ·⦄ (snd _) = Inr (λ ())
    result-==-dec [ x ]case r1 of⦃· x₁ ·⦄ (C⁻[ x₂ ] r2) = Inr (λ ())

  typ-==-dec : (τ1 τ2 : typ) → τ1 == τ2 ∨ τ1 ≠ τ2
  typ-==-dec (τ1i ==> τ1o) (τ2i ==> τ2o)
    with typ-==-dec τ1i τ2i
  ... | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl
    with typ-==-dec τ1o τ2o
  ... | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl = Inl refl
  typ-==-dec (τ1i ==> τ1o) ⟨⟩ = Inr (λ ())
  typ-==-dec (τ1i ==> τ1o) ⟨ _ × _ ⟩ = Inr (λ ())
  typ-==-dec (τ1i ==> τ1o) D[ _ ] = Inr (λ ())
  typ-==-dec ⟨⟩ ⟨⟩ = Inl refl
  typ-==-dec ⟨⟩ ⟨ τ2 × τ3 ⟩ = Inr (λ ())
  typ-==-dec ⟨⟩ (_ ==> _) = Inr (λ ())
  typ-==-dec ⟨⟩ D[ _ ] = Inr (λ ())
  typ-==-dec ⟨ τ1a × τ1b ⟩ ⟨ τ2a × τ2b ⟩
    with typ-==-dec τ1a τ2a
  ... | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl
    with typ-==-dec τ1b τ2b
  ... | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl = Inl refl
  typ-==-dec ⟨ τ1 × τ2 ⟩ ⟨⟩ = Inr (λ ())
  typ-==-dec ⟨ _ × _ ⟩ (_ ==> _) = Inr (λ ())
  typ-==-dec ⟨ _ × _ ⟩ D[ _ ] = Inr (λ ())
  typ-==-dec D[ d1 ] D[ d2 ]
    with natEQ d1 d2
  ... | Inr ne   = Inr λ where refl → ne refl
  ... | Inl refl = Inl refl
  typ-==-dec D[ _ ] (_ ==> _) = Inr (λ ())
  typ-==-dec D[ _ ] ⟨⟩ = Inr (λ ())
  typ-==-dec D[ _ ] ⟨ _ × _ ⟩ = Inr (λ ())

  final-dec : ∀{r} → r final ∨ (r final → ⊥)

  env-final-dec : ∀{E} → E env-final ∨ (E env-final → ⊥)

  final-dec {[ E ]fix x₁ ⦇·λ x₂ => e ·⦈}
    with env-final-dec {E}
  ... | Inr nf  = Inr (λ {(FFix f) → nf f})
  ... | Inl E-f = Inl (FFix E-f)
  final-dec {⟨⟩} = Inl FUnit
  final-dec {⟨ r1 , r2 ⟩}
    with final-dec {r1}
  ... | Inr nf   = Inr λ {(FPair h1 h2) → nf h1}
  ... | Inl r1-f
    with final-dec {r2}
  ... | Inr nf   = Inr λ {(FPair h1 h2) → nf h2}
  ... | Inl r2-f = Inl (FPair r1-f r2-f)
  final-dec {C[ x ] r}
    with final-dec {r}
  ... | Inr nf  = Inr λ {(FCon h1) → nf h1}
  ... | Inl r-f = Inl (FCon r-f)
  final-dec {C⁻[ x ] r} = Inr (λ ())
  final-dec {[ E ]??[ x₁ ]}
    with env-final-dec {E}
  ... | Inr nf  = Inr λ {(FHole h1) → nf h1}
  ... | Inl E-f = Inl (FHole E-f)
  final-dec {r1 ∘ r2}
    with final-dec {r1}
  ... | Inr nf   = Inr λ {(FAp h _ _) → nf h}
  ... | Inl r1-f
    with final-dec {r2}
  ... | Inr nf   = Inr λ {(FAp _ h _) → nf h}
  final-dec {[ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈ ∘ r2} | Inl r1-f | Inl r2-f
    = Inr λ {(FAp _ _ h) → abort (h refl)}
  final-dec {⟨⟩ ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {⟨ r1 , r3 ⟩ ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {(C[ x ] r1) ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {[ x ]??[ x₁ ] ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f  (λ {E} {f} {x} {e} ()))
  final-dec {(r1 ∘ r3) ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {fst r1 ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {snd r1 ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {[ x ]case r1 of⦃· x₁ ·⦄ ∘ r2} | Inl r1-f | Inl r2-f = Inl (FAp r1-f r2-f (λ {E} {f} {x} {e} ()))
  final-dec {fst r}
    with final-dec {r}
  ... | Inr nf  = Inr λ {(FFst h _) → nf h}
  final-dec {fst ⟨ r , r₁ ⟩} | Inl r-f
    = Inr λ {(FFst _ h) → abort (h refl)}
  final-dec {fst [ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst ⟨⟩} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst (C[ x ] r)} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst [ x ]??[ x₁ ]} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst (r ∘ r₁)} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst (fst r)} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst (snd r)} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {fst [ x ]case r of⦃· x₁ ·⦄} | Inl r-f = Inl (FFst r-f (λ {r1} {r2} ()))
  final-dec {snd r}
    with final-dec {r}
  ... | Inr nf  = Inr λ {(FSnd h _) → nf h}
  final-dec {snd ⟨ r , r₁ ⟩} | Inl r-f
    = Inr λ {(FSnd _ h) → abort (h refl)}
  final-dec {snd [ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd ⟨⟩} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd (C[ x ] r)} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd [ x ]??[ x₁ ]} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd (r ∘ r₁)} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd (fst r)} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd (snd r)} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {snd [ x ]case r of⦃· x₁ ·⦄} | Inl r-f = Inl (FSnd r-f (λ {r1} {r2} ()))
  final-dec {[ E ]case r of⦃· x₁ ·⦄}
    with final-dec {r}
  ... | Inr nf  = Inr λ {(FCase h _ _) → nf h}
  ... | Inl r-f
    with env-final-dec {E}
  ... | Inr nf  = Inr λ {(FCase _ _ h) → nf h}
  final-dec {[ E ]case C[ x ] r of⦃· x₁ ·⦄} | Inl r-f | Inl E-f
    = Inr λ {(FCase _ h _) → abort (h refl)}
  final-dec {[ E ]case [ x ]fix x₂ ⦇·λ x₃ => x₄ ·⦈ of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case ⟨⟩ of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case ⟨ r , r₁ ⟩ of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case [ x ]??[ x₂ ] of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case r ∘ r₁ of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case fst r of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case snd r of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)
  final-dec {[ E ]case [ x ]case r of⦃· x₂ ·⦄ of⦃· x₁ ·⦄} | Inl r-f | Inl E-f = Inl (FCase r-f (λ {c} {r'} ()) E-f)

  env-final-dec {[]} = Inl (EF (λ ()))
  env-final-dec {(_ , r) :: E}
    with final-dec {r}
  ... | Inr nf       = Inr (λ {(EF h) → nf (h InH)})
  ... | Inl r-f
    with env-final-dec {E}
  ... | Inr nf       = Inr (λ {(EF h) → nf (EF (λ z → h (InT z)))})
  ... | Inl (EF E-f) = Inl (EF λ {InH → r-f ; (InT h) → E-f h})

  Coerce-dec : ∀{r} → Σ[ ex ∈ ex ] (Coerce r := ex) ∨ (Σ[ ex ∈ ex ] (Coerce r := ex) → ⊥)
  Coerce-dec {[ x ]fix x₁ ⦇·λ x₂ => x₃ ·⦈} = Inr (λ where (_ , ()))
  Coerce-dec {⟨⟩} = Inl (⟨⟩ , CoerceUnit)
  Coerce-dec {⟨ r1 , r2 ⟩}
    with Coerce-dec {r1}
  ...  | Inr nc          = Inr λ {(_ , CoercePair c-r1 _) → nc (_ , c-r1)}
  ...  | Inl (_ , c-r1)
    with Coerce-dec {r2}
  ...  | Inr nc          = Inr λ {(_ , CoercePair _ c-r2) → nc (_ , c-r2)}
  ...  | Inl (_ , c-r2)  = Inl (_ , CoercePair c-r1 c-r2)
  Coerce-dec {C[ c ] r}
    with Coerce-dec {r}
  ...  | Inr nc         = Inr λ {(_ , CoerceCtor c-r) → nc (_ , c-r)}
  ...  | Inl (_ , c-r)  = Inl (_ , CoerceCtor c-r)
  Coerce-dec {C⁻[ x ] r} = Inr (λ where (_ , ()))
  Coerce-dec {[ x ]??[ x₁ ]} = Inr (λ where (_ , ()))
  Coerce-dec {r ∘ r₁} = Inr (λ where (_ , ()))
  Coerce-dec {fst r} = Inr (λ where (_ , ()))
  Coerce-dec {snd r} = Inr (λ where (_ , ()))
  Coerce-dec {[ x ]case r of⦃· x₁ ·⦄} = Inr (λ where (_ , ()))

  value-dec : ∀{r} → r value ∨ (r value → ⊥)
  value-dec {[ E ]fix x₁ ⦇·λ x₂ => x₃ ·⦈}
    with env-final-dec {E}
  ... | Inr nf  = Inr (λ {(VFix E-f) → nf E-f})
  ... | Inl E-f = Inl (VFix E-f)
  value-dec {⟨⟩} = Inl VUnit
  value-dec {⟨ r1 , r2 ⟩}
    with value-dec {r1}
  ... | Inr nv  = Inr λ {(VPair h _) → nv h}
  ... | Inl r1v
    with value-dec {r2}
  ... | Inr nv  = Inr λ {(VPair _ h) → nv h}
  ... | Inl r2v = Inl (VPair r1v r2v)
  value-dec {C[ x ] r}
    with value-dec {r}
  ... | Inl rv = Inl (VCon rv)
  ... | Inr nv = Inr (λ {(VCon rv) → nv rv})
  value-dec {C⁻[ x ] r} = Inr (λ ())
  value-dec {[ x ]??[ x₁ ]} = Inr (λ ())
  value-dec {r ∘ r₁} = Inr (λ ())
  value-dec {fst r} = Inr (λ ())
  value-dec {snd r} = Inr (λ ())
  value-dec {[ x ]case r of⦃· x₁ ·⦄} = Inr (λ ())

  ex-¿¿-dec : ∀{ex} → ex == ¿¿ ∨ ex ≠ ¿¿
  ex-¿¿-dec {⟨⟩} = Inr (λ ())
  ex-¿¿-dec {⟨ ex₁ , ex₂ ⟩} = Inr (λ ())
  ex-¿¿-dec {C[ x ] ex₁} = Inr (λ ())
  ex-¿¿-dec {¿¿} = Inl refl
  ex-¿¿-dec {x ↦ ex₁} = Inr (λ ())

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-