text:
{-# OPTIONS --rewriting #-}
module DualLMRefined where

open import Data.Bool
open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Fin hiding (_+_)
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Extensionality
open import Direction

-- variables

variable
  n m : ℕ

----------------------------------------------------------------------
-- auxiliaries for automatic rewriting

n+1=suc-n : n + 1 ≡ suc n
n+1=suc-n {zero} = refl
n+1=suc-n {suc n} = cong suc (n+1=suc-n {n})

{-# REWRITE n+1=suc-n #-}

n+0=n : n + 0 ≡ n
n+0=n {zero} = refl
n+0=n {suc n} = cong suc (n+0=n {n})

{-# REWRITE n+0=n #-}

inject+0-x=x : {x : Fin m} → inject+ 0 x ≡ x
inject+0-x=x {x = zero} = refl
inject+0-x=x {x = suc x} = cong suc inject+0-x=x

{-# REWRITE inject+0-x=x #-}

n+sucm : n + suc m ≡ suc (n + m)
n+sucm {0} = refl
n+sucm {suc n} = cong suc (n+sucm{n})

{-# REWRITE n+sucm #-}

n=fromℕtoℕn : (toℕ (fromℕ n)) ≡ n
n=fromℕtoℕn {zero}  = refl
n=fromℕtoℕn {suc n} = cong suc (n=fromℕtoℕn {n})

{-# REWRITE n=fromℕtoℕn #-}

sucn∸suctoℕx≡n∸toℕx : {n : ℕ} {x : Fin n} → suc (n ∸ suc (toℕ x)) ≡ n ∸ (toℕ x)
sucn∸suctoℕx≡n∸toℕx {suc n} {zero} = refl
sucn∸suctoℕx≡n∸toℕx {suc n} {suc x} = sucn∸suctoℕx≡n∸toℕx{n}{x}

sym-sucn∸suctoℕx≡n∸toℕx : {n : ℕ} {x : Fin n} → n ∸ (toℕ x) ≡ suc (n ∸ suc (toℕ x))
sym-sucn∸suctoℕx≡n∸toℕx {n} {x} = sym (sucn∸suctoℕx≡n∸toℕx{n}{x})

{-# REWRITE sym-sucn∸suctoℕx≡n∸toℕx #-}

n∸n≡0F : n ∸ n ≡ 0
n∸n≡0F {0} = refl
n∸n≡0F {suc n} = n∸n≡0F{n}

{-# REWRITE n∸n≡0F #-}

{-# REWRITE m+n∸n≡m #-}

----------------------------------------------------------------------
-- some more required properties on natural numbers and fin

toℕx≤n : {n : ℕ} {x : Fin n} → Data.Nat._≤_ (toℕ x) n
toℕx≤n {suc n} {zero} = z≤n
toℕx≤n {suc n} {suc x} = s≤s toℕx≤n

toℕx≤n' : {n : ℕ} {x : Fin (suc n)} → Data.Nat._≤_ (toℕ x) n
toℕx≤n' {0} {zero} = z≤n
toℕx≤n' {suc n} {zero} = z≤n
toℕx≤n' {suc n} {suc x} = s≤s (toℕx≤n'{n}{x})

n∸x+x≡n : {n x : ℕ} → Data.Nat._≤_ x n  → n ∸ x + x ≡ n
n∸x+x≡n {0} {zero} le = refl
n∸x+x≡n {0} {suc x} ()
n∸x+x≡n {suc n} {zero} le = refl
n∸x+x≡n {suc n} {suc x} (s≤s le) = cong suc (n∸x+x≡n le)

toℕx<n : {n : ℕ} {x : Fin n} → Data.Nat._<_ (toℕ x) n
toℕx<n {suc n} {zero} = s≤s z≤n
toℕx<n {suc n} {suc x} = s≤s toℕx<n

n∸x≡suc[n∸sucx] : {n x : ℕ} → Data.Nat._<_ x n → n ∸ x ≡ suc (n ∸ (suc x))
n∸x≡suc[n∸sucx] {suc n} {0} le = refl
n∸x≡suc[n∸sucx] {suc n} {suc x} (s≤s le) = n∸x≡suc[n∸sucx] le

suc[n+x]≡n+sucx : {n x : ℕ} → suc (n + x) ≡ (n + suc x)
suc[n+x]≡n+sucx {0} {x} = refl
suc[n+x]≡n+sucx {suc n} {x} = refl

suc[n∸sucx+x]≡n : {n x : ℕ} → Data.Nat._<_ x n → suc (n ∸ (suc x) + x) ≡ n
suc[n∸sucx+x]≡n {suc n} {0} le = refl
suc[n∸sucx+x]≡n {suc n} {suc x} (s≤s le) = cong suc (suc[n∸sucx+x]≡n {n} {x} le)

suc[n∸suc[toℕi]+toℕi]≡n : {n : ℕ} {i : Fin n} → suc (n ∸ (suc (toℕ i)) + toℕ i) ≡ n
suc[n∸suc[toℕi]+toℕi]≡n {n} {i} = suc[n∸sucx+x]≡n{n}{toℕ i} toℕx<n

{-# REWRITE suc[n∸suc[toℕi]+toℕi]≡n #-}

m∸toℕ+toℕ≡m : {n : ℕ} {i : Fin (suc n)} → n ∸ (toℕ i) + (toℕ i) ≡ n
m∸toℕ+toℕ≡m {n} {i} = m∸n+n≡m{n}{toℕ i} toℕx≤n'

{-# REWRITE m∸toℕ+toℕ≡m #-}

<suc : {n x : ℕ} → Data.Nat._<_ x n → Data.Nat._<_ x (suc n)
<suc {suc n} {0} le = s≤s z≤n
<suc {suc n} {suc x} (s≤s le) = s≤s (<suc {n} {x} le)

≤suc : {n x : ℕ} → Data.Nat._≤_ x n → Data.Nat._≤_ x (suc n)
≤suc {n} {0} le = z≤n
≤suc {suc n} {suc x} (s≤s le) = s≤s (≤suc {n} {x} le)

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

module IND where

  mutual
    data Type (n : ℕ) : Set where
      TUnit TInt : Type n
      TPair : Type n → Type n → Type n
      TChan : SType n → Type n

    data SType (n : ℕ) : Set where
      gdd : (gst : GType n) → SType n
      rec : (gst : GType (suc n)) → SType n
      var : (x : Fin n) → SType n

    data GType (n : ℕ) : Set where
      transmit : (d : Dir) (t : Type n) (s : SType n) → GType n
      choice : (d : Dir) (m : ℕ) (alt : Fin m → SType n) → GType n
      end : GType n

    data MClType (n : ℕ) : Set where
      MClTUnit MClTInt : MClType n
      MClTPair : MClType n → MClType n → MClType n
      MClTChan : SType 0 → MClType n

    data MClSType (n : ℕ) : Set where
      tgdd : (tgst : MClGType n) → MClSType n
      trec : (tgst : MClGType (suc n)) → MClSType n
      tvar : (x : Fin n) → MClSType n

    data MClGType (n : ℕ) : Set where
      ttransmit : (d : Dir) (t : MClType n) (s : MClSType n) → MClGType n
      tchoice : (d : Dir) (m : ℕ) (alt : Fin m → MClSType n) → MClGType n
      end : MClGType n

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

  weaken1'N : Fin (suc n) → Fin n → Fin (suc n)
  weaken1'N zero x = suc x
  weaken1'N (suc i) zero = zero
  weaken1'N (suc i) (suc x) = suc (weaken1'N i x)

  weaken1'S : Fin (suc n) → SType n → SType (suc n)
  weaken1'G : Fin (suc n) → GType n → GType (suc n)
  weaken1'T : Fin (suc n) → Type n → Type (suc n)

  weaken1'S i (gdd gst) = gdd (weaken1'G i gst)
  weaken1'S i (rec gst) = rec (weaken1'G (suc i) gst)
  weaken1'S i (var x) = var (weaken1'N i x)

  weaken1'G i (transmit d t s) = transmit d (weaken1'T i t) (weaken1'S i s)
  weaken1'G i (choice d m alt) = choice d m (weaken1'S i ∘ alt)
  weaken1'G i end = end

  weaken1'T i TUnit = TUnit
  weaken1'T i TInt = TInt
  weaken1'T i (TPair t₁ t₂) = TPair (weaken1'T i t₁) (weaken1'T i t₂)
  weaken1'T i (TChan x) = TChan (weaken1'S i x)

  weaken1S : SType n → SType (suc n)
  weaken1G : GType n → GType (suc n)
  weaken1T : Type n → Type (suc n)

  weaken1S = weaken1'S zero
  weaken1G = weaken1'G zero
  weaken1T = weaken1'T zero

  weakenS : (n : ℕ) → SType m → SType (m + n)
  weakenG : (n : ℕ) → GType m → GType (m + n)
  weakenT : (n : ℕ) → Type m → Type (m + n)

  weakenS n (gdd gst) = gdd (weakenG n gst)
  weakenS n (rec gst) = rec (weakenG n gst)
  weakenS n (var x) = var (inject+ n x)

  weakenG n (transmit d t s) = transmit d (weakenT n t) (weakenS n s)
  weakenG n (choice d m alt) = choice d m (λ i → weakenS n (alt i))
  weakenG n end = end

  weakenT n TUnit = TUnit
  weakenT n TInt = TInt
  weakenT n (TPair ty ty₁) = TPair (weakenT n ty) (weakenT n ty₁)
  weakenT n (TChan x) = TChan (weakenS n x)

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

  -- Single substitution with SType 0

  st-substS : SType (suc n) → Fin (suc n) → SType 0 → SType n
  st-substG : GType (suc n) → Fin (suc n) → SType 0 → GType n
  st-substT : Type (suc n) → Fin (suc n) → SType 0 → Type n

  st-substS (gdd gst) i st0 = gdd (st-substG gst i st0)
  st-substS (rec gst) i st0 = rec (st-substG gst (suc i) st0)
  st-substS {n} (var zero) zero st0 = weakenS n st0
  st-substS {suc n} (var zero) (suc i) st0 = var zero
  st-substS {suc n} (var (suc x)) zero st0 = var x
  st-substS {suc n} (var (suc x)) (suc i) st0 = weaken1S (st-substS (var x) i st0)

  st-substG (transmit d t s) i st0 = transmit d (st-substT t i st0) (st-substS s i st0)
  st-substG (choice d m alt) i st0 = choice d m (λ j → st-substS (alt j) i st0)
  st-substG end i st0 = end

  st-substT TUnit i st0 = TUnit
  st-substT TInt i st0 = TInt
  st-substT (TPair ty ty₁) i st0 = TPair (st-substT ty i st0) (st-substT ty₁ i st0)
  st-substT (TChan st) i st0 = TChan (st-substS st i st0)

  -- Single substitution with SType n

  st-substS' : Fin (suc n) → SType n → SType (suc n) → SType n
  st-substG' : Fin (suc n) → SType n → GType (suc n) → GType n
  st-substT' : Fin (suc n) → SType n → Type (suc n) → Type n

  st-substS' i st (gdd gst) = gdd (st-substG' i st gst)
  st-substS' i st (rec gst) = rec (st-substG' (suc i) (weaken1S st) gst)
  st-substS' i st (var x)
    with compare x i
  st-substS' i st (var .(inject least)) | less .i least = var (inject! least)
  st-substS' .x st (var x) | equal .x = st
  st-substS' .(inject least) st (var (suc x)) | greater .(suc x) least = var x

  st-substG' i st (transmit d t s) = transmit d (st-substT' i st t) (st-substS' i st s)
  st-substG' i st (choice d m alt) = choice d m (λ j → st-substS' i st (alt j))
  st-substG' i st end = end

  st-substT' i st TUnit = TUnit
  st-substT' i st TInt  = TInt
  st-substT' i st (TPair ty ty₁) = TPair (st-substT' i st ty) (st-substT' i st ty₁)
  st-substT' i st (TChan s) = TChan (st-substS' i st s)

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

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

open IND

data Stack : ℕ → Set where
  ε : Stack 0
  ⟪_,_⟫ : Stack n → IND.GType (suc n) → Stack (suc n)

data StackS : ℕ → Set where
  ε : StackS 0
  ⟪_,_⟫ : StackS n → IND.SType n → StackS (suc n)

data StackS0 : ℕ → Set where
  ε : StackS0 0
  ⟪_,_⟫ : StackS0 n → IND.SType 0 → StackS0 (suc n)

data StackMCl : ℕ → Set where
  ε : StackMCl 0
  ⟪_,_⟫ : StackMCl n → IND.MClGType (suc n) → StackMCl (suc n)

-- Stack of length m starting at arbitrary type size n
data Stack' : ℕ → ℕ → Set where
  ε : Stack' n 0
  ⟪_,_⟫ : Stack' n m → IND.GType (suc (n + m)) → Stack' n (suc m)

data Stack'S : ℕ → ℕ → Set where
  ε : Stack'S n 0
  ⟪_,_⟫ : Stack'S n m → IND.SType (n + m) → Stack'S n (suc m)

data Stack'Sn : ℕ → ℕ → Set where
  ε : Stack'Sn n 0
  ⟪_,_⟫ : Stack'Sn n m → IND.SType n → Stack'Sn n (suc m)

get : {n : ℕ} → (i : Fin n) → Stack n → Stack (n ∸ (suc (toℕ i))) × IND.GType (n ∸ (toℕ i))
get {suc n} zero ⟪ σ , x ⟫ = σ , x
get {suc n} (suc i) ⟪ σ , x ⟫ = get i σ

getS : {n : ℕ} → (i : Fin n) → StackS n → StackS (n ∸ (suc (toℕ i))) × IND.SType (n ∸ (suc (toℕ i)))
getS {suc n} zero ⟪ σ , x ⟫ = σ , x
getS {suc n} (suc i) ⟪ σ , x ⟫ = getS i σ

getS0 : {n : ℕ} → (i : Fin n) → StackS0 n → StackS0 (n ∸ (suc (toℕ i))) × IND.SType 0
getS0 {suc n} zero ⟪ σ , x ⟫ = σ , x
getS0 {suc n} (suc i) ⟪ σ , x ⟫ = getS0 i σ

getMCl : {n : ℕ} → (i : Fin n) → StackMCl n → StackMCl (n ∸ (suc (toℕ i))) × IND.MClGType (n ∸ (toℕ i))
getMCl {suc n} zero ⟪ σ , x ⟫ = σ , x
getMCl {suc n} (suc i) ⟪ σ , x ⟫ = getMCl i σ

get' : {n m : ℕ} → (i : Fin m) → Stack' n m → Stack' n (m ∸ (suc (toℕ i))) × IND.GType (n + (m ∸ (toℕ i)))
get' {n} {suc m} zero ⟪ σ , x ⟫ = σ , x
get' {n} {suc m} (suc i) ⟪ σ , x ⟫ = get' i σ

get'S : {n m : ℕ} → (i : Fin m) → Stack'S n m → Stack'S n (m ∸ (suc (toℕ i))) × IND.SType (n + (m ∸ (suc (toℕ i))))
get'S {n} {suc m} zero ⟪ σ , x ⟫ = σ , x
get'S {n} {suc m} (suc i) ⟪ σ , x ⟫ = get'S i σ

get'Sn : {n m : ℕ} → (i : Fin m) → Stack'Sn n m → Stack'Sn n (m ∸ (suc (toℕ i))) × IND.SType n
get'Sn {n} {suc m} zero ⟪ σ , x ⟫ = σ , x
get'Sn {n} {suc m} (suc i) ⟪ σ , x ⟫ = get'Sn i σ

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

stack-split : (i : Fin (suc n)) → Stack n → Stack (n ∸ toℕ i) × Stack' (n ∸ toℕ i) (toℕ i)
stack-split zero σ = σ , ε
stack-split{n} (suc i) ⟪ σ , x ⟫
  with stack-split i σ
... | σ' , σ'' = σ' , ⟪ σ'' , x ⟫

-- couldn't achieve this by rewriting alone
suc[n+[m∸sucx]+x]≡n+m : {n m x : ℕ} → Data.Nat._<_ x m → suc (n + (m ∸ suc x) + x) ≡ n + m
suc[n+[m∸sucx]+x]≡n+m {0} {m} {x} le = suc[n∸sucx+x]≡n{m}{x} le
suc[n+[m∸sucx]+x]≡n+m {suc n} {suc m} {0} le = refl
suc[n+[m∸sucx]+x]≡n+m {suc n} {suc m} {suc x} (s≤s le) = cong suc (cong suc (suc[n+[m∸sucx]+x]≡n+m le))

-- i from the top of the stack
stack'-m-i : {n m : ℕ} → (i : Fin m) → Stack' n m → Stack' (n + (m ∸ (toℕ i))) (toℕ i)
stack'-m-i {n} {m} zero σ = ε
stack'-m-i {n} {suc m} (suc i) ⟪ σ , x ⟫ rewrite (sym (suc[n+[m∸sucx]+x]≡n+m{n}{m}{toℕ i} toℕx<n)) = ⟪ (stack'-m-i i σ) , x ⟫

weaken1-Stack' : (i : Fin (suc n)) → Stack' n m → Stack' (suc n) m
weaken1-Stack' i ε = ε
weaken1-Stack'{n}{m} i ⟪ σ , x ⟫ = ⟪ (weaken1-Stack' i σ) , (weaken1'G (inject+ m i) x) ⟫

weaken1-Stack'Sn : (i : Fin (suc n)) → Stack'Sn n m → Stack'Sn (suc n) m
weaken1-Stack'Sn i ε = ε
weaken1-Stack'Sn{n}{m} i ⟪ σ , x ⟫ = ⟪ (weaken1-Stack'Sn i σ) , (weaken1'S i x) ⟫

-- substitute after index i, required for rec case
stack-sim-substS-i> : (i : Fin n) → StackS0 (n ∸ (toℕ (suc i))) → SType n → SType (toℕ (suc i))
stack-sim-substG-i> : (i : Fin n) → StackS0 (n ∸ (toℕ (suc i))) → GType n → GType (toℕ (suc i))
stack-sim-substT-i> : (i : Fin n) → StackS0 (n ∸ (toℕ (suc i))) → Type n → Type (toℕ (suc i))

stack-sim-substS-i> i σ (gdd gst) = gdd (stack-sim-substG-i> i σ gst)
stack-sim-substS-i> i σ (rec gst) = rec (stack-sim-substG-i> (suc i) σ gst)
stack-sim-substS-i>{suc n} zero σ (var zero) = var zero
stack-sim-substS-i> zero σ (var (suc x))
  with getS0 x σ
... | σ' , s = weaken1S s
stack-sim-substS-i> (suc i) σ (var zero) = var zero
stack-sim-substS-i> (suc i) σ (var (suc x)) = weaken1S (stack-sim-substS-i> i σ (var x))

stack-sim-substG-i> i σ (transmit d t s) = transmit d (stack-sim-substT-i> i σ t) (stack-sim-substS-i> i σ s)
stack-sim-substG-i> i σ (choice d m alt) = choice d m (λ x → stack-sim-substS-i> i σ (alt x))
stack-sim-substG-i> i σ end = end

stack-sim-substT-i> i σ TUnit = TUnit
stack-sim-substT-i> i σ TInt = TInt
stack-sim-substT-i> i σ (TPair t t₁) = TPair (stack-sim-substT-i> i σ t) (stack-sim-substT-i> i σ t₁)
stack-sim-substT-i> i σ (TChan x) = TChan (stack-sim-substS-i> i σ x)

-- substitute stack
stack-sim-substS : StackS0 n → SType n → SType 0
stack-sim-substG : StackS0 n → GType n → GType 0
stack-sim-substT : StackS0 n → Type n → Type 0

stack-sim-substS σ (gdd gst) = gdd (stack-sim-substG σ gst)
stack-sim-substS σ (rec gst) = rec (stack-sim-substG-i> zero σ gst) -- Apply stack substitution to variables 1, ..., suc n; keep 0F; can't extend StackS0 since only SType 0F allowed
stack-sim-substS σ (var x)
  with getS0 x σ
... | σ' , s = s

stack-sim-substG σ (transmit d t s) = transmit d (stack-sim-substT σ t) (stack-sim-substS σ s)
stack-sim-substG σ (choice d m alt) = choice d m (λ x → stack-sim-substS σ (alt x))
stack-sim-substG σ end = end

stack-sim-substT σ TUnit = TUnit
stack-sim-substT σ TInt = TInt
stack-sim-substT σ (TPair t t₁) = TPair (stack-sim-substT σ t) (stack-sim-substT σ t₁)
stack-sim-substT σ (TChan x) = TChan (stack-sim-substS σ x)

stack-sim-substS'-i≥ : (i : Fin (suc m)) → Stack'Sn n (m ∸ toℕ i) → SType m → SType (n + toℕ i)
stack-sim-substG'-i≥ : (i : Fin (suc m)) → Stack'Sn n (m ∸ toℕ i) → GType m → GType (n + toℕ i)
stack-sim-substT'-i≥ : (i : Fin (suc m)) → Stack'Sn n (m ∸ toℕ i) → Type m → Type (n + toℕ i)

stack-sim-substS'-i≥ i σ (gdd gst) = gdd (stack-sim-substG'-i≥ i σ gst)
stack-sim-substS'-i≥ i σ (rec gst) = rec (stack-sim-substG'-i≥ (suc i) σ gst)
stack-sim-substS'-i≥ zero σ (var x)
  with get'Sn x σ
... | σ' , y = y
stack-sim-substS'-i≥ (suc i) σ (var zero) = var zero
stack-sim-substS'-i≥ (suc i) σ (var (suc x)) = weaken1S (stack-sim-substS'-i≥ i σ (var x))

stack-sim-substG'-i≥ i σ (transmit d t s) = transmit d (stack-sim-substT'-i≥ i σ t) (stack-sim-substS'-i≥ i σ s)
stack-sim-substG'-i≥ i σ (choice d m alt) = choice d m (λ x → stack-sim-substS'-i≥ i σ (alt x))
stack-sim-substG'-i≥ i σ end = end

stack-sim-substT'-i≥ i σ TUnit = TUnit
stack-sim-substT'-i≥ i σ TInt = TInt
stack-sim-substT'-i≥ i σ (TPair t t₁) = TPair (stack-sim-substT'-i≥ i σ t) (stack-sim-substT'-i≥ i σ t₁)
stack-sim-substT'-i≥ i σ (TChan x) = TChan (stack-sim-substS'-i≥ i σ x)

-- substitute stack'
stack-sim-substS' : Stack'Sn n m → SType m → SType n
stack-sim-substG' : Stack'Sn n m → GType m → GType n
stack-sim-substT' : Stack'Sn n m → Type m → Type n

stack-sim-substS' σ (gdd gst) = gdd (stack-sim-substG' σ gst)
stack-sim-substS'{n}{m} σ (rec gst) = rec (stack-sim-substG'-i≥ (suc zero) σ gst)
stack-sim-substS' σ (var x)
  with get'Sn x σ
... | σ' , s = s

stack-sim-substG' σ (transmit d t s) = transmit d (stack-sim-substT' σ t) (stack-sim-substS' σ s)
stack-sim-substG' σ (choice d m alt) = choice d m (λ x → stack-sim-substS' σ (alt x))
stack-sim-substG' σ end = end

stack-sim-substT' σ TUnit = TUnit
stack-sim-substT' σ TInt = TInt
stack-sim-substT' σ (TPair t t₁) = TPair (stack-sim-substT' σ t) (stack-sim-substT' σ t₁)
stack-sim-substT' σ (TChan x) = TChan (stack-sim-substS' σ x)

{- required for alt. def. of rec case of stack-sim-substS'-top

stack-sim-substS'-top-i≥ : (i : Fin (suc m)) → Stack'Sn n (m ∸ toℕ i) → SType (n + m) → SType (n + toℕ i)
stack-sim-substG'-top-i≥ : (i : Fin (suc m)) → Stack'Sn n (m ∸ toℕ i) → GType (n + m) → GType (n + toℕ i)
stack-sim-substT'-top-i≥ : (i : Fin (suc m)) → Stack'Sn n (m ∸ toℕ i) → Type (n + m) → Type (n + toℕ i)

stack-sim-substS'-top-i≥ i σ (gdd gst) = {!!}
stack-sim-substS'-top-i≥ i σ (rec gst) = rec (stack-sim-substG'-top-i≥ (suc i) σ gst)
stack-sim-substS'-top-i≥ i σ (var x) = {!!}

stack-sim-substS'-top-i≥' : (i : Fin (suc m)) → Stack'Sn (n + toℕ i) (toℕ i) → SType (n + m) → SType (n + m ∸ toℕ i)
stack-sim-substG'-top-i≥' : (i : Fin (suc m)) → Stack'Sn (n + toℕ i) (toℕ i) → GType (n + m) → GType (n + m ∸ toℕ i)

stack-sim-substS'-top-i≥'{m = m}{n = suc n} i σ (rec gst) = rec (stack-sim-substG'-top-i≥' {!!} {!!} gst)
-}

-- substitute top variables from stack'
stack-sim-substS'-top : Stack'Sn n m → SType (n + m) → SType n
stack-sim-substG'-top : Stack'Sn n m → GType (n + m) → GType n
stack-sim-substT'-top : Stack'Sn n m → Type (n + m) → Type n

stack-sim-substS'-top σ (gdd gst) = gdd (stack-sim-substG'-top σ gst)
stack-sim-substS'-top{n}{m} σ (rec gst) = rec (stack-sim-substG'-top{m = m} (weaken1-Stack'Sn zero σ) gst) -- alternative: rec (stack-sim-substG'-top-i≥ 1 σ gst)
stack-sim-substS'-top{n}{m} σ (var x) = {!!} -- <= n => var n, > n => substitute

-- Transform Stack of STypes to Stack of closed STypes by substitution
-- ⟪ ε , SType 0 , SType 1               , SType 2                                            , ⋯ ⟫
-- ⟪ ε , SType 0 , SType 1 [0 ↦ SType 0], SType 2 [0 ↦ SType 0, 1 ↦ SType 1 [0 ↦ SType 0]], ⋯ ⟫
-- ⟪ ε , SType 0 , SType 0               , SType 0                                            , ⋯ ⟫
stack-transform : StackS n → StackS0 n
stack-transform ε = ε
stack-transform ⟪ σ , x ⟫
  with stack-transform σ
... | σ' = ⟪ σ' , (stack-sim-substS σ' x) ⟫

stack-transform' : Stack'S n m → Stack'Sn n m
stack-transform' ε = ε
stack-transform'{n} ⟪ σ , x ⟫
  with stack-transform' σ
... | σ' = ⟪ σ' , stack-sim-substS'-top σ' x  ⟫

stack-cat : Stack n → Stack' n m → Stack (n + m)
stack-cat σ ε = σ
stack-cat σ ⟪ σ' , x ⟫ = ⟪ (stack-cat σ σ') , x ⟫

stack-cat' : Stack' 0 n → Stack' n m → Stack' 0 (n + m)
stack-cat' σ ε = σ
stack-cat' σ ⟪ σ' , x ⟫ = ⟪ (stack-cat' σ σ') , x ⟫

stack-sim-substS-refl : (s : SType 0) → stack-sim-substS ε s ≡ s
stack-sim-substG-refl : (g : GType 0) → stack-sim-substG ε g ≡ g
stack-sim-substT-refl : (t : Type 0) → stack-sim-substT ε t ≡ t

stack-sim-substS-refl (gdd gst) = cong gdd (stack-sim-substG-refl gst)
stack-sim-substS-refl (rec gst) = {!!} -- requires stack-sim-substG-i>-refl

stack-sim-substG-refl (transmit d t s) = cong₂ (transmit d) (stack-sim-substT-refl t) (stack-sim-substS-refl s)
stack-sim-substG-refl (choice d m alt) = cong (choice d m) (ext (λ x → stack-sim-substS-refl (alt x)))
stack-sim-substG-refl end = refl

stack-sim-substT-refl TUnit = refl
stack-sim-substT-refl TInt = refl
stack-sim-substT-refl (TPair t t₁) = cong₂ TPair (stack-sim-substT-refl t) (stack-sim-substT-refl t₁)
stack-sim-substT-refl (TChan x) = cong TChan (stack-sim-substS-refl x)

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

-- Message closure
mclS : (σ : StackS n) → SType n → MClSType n
mclG : (σ : StackS n) → GType n → MClGType n
mclT : (σ : StackS n) → Type n → MClType n

mclS σ (gdd gst) = tgdd (mclG σ gst)
mclS σ (rec gst) = trec (mclG ⟪ σ , (rec gst) ⟫ gst)
mclS σ (var x) = tvar x

mclG σ (transmit d t s) = ttransmit d (mclT σ t) (mclS σ s)
mclG σ (choice d m alt) = tchoice d m (λ x → mclS σ (alt x))
mclG σ end = end

mclT σ TUnit = MClTUnit
mclT σ TInt = MClTInt
mclT σ (TPair t t₁) = MClTPair (mclT σ t) (mclT σ t₁)
mclT σ (TChan x) = MClTChan (stack-sim-substS (stack-transform σ) x)

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

-- Any mcl type is a normal type with weakening
mcl2indS : MClSType n → SType n
mcl2indG : MClGType n → GType n
mcl2indT : MClType n → Type n

mcl2indS (tgdd tgst) = gdd (mcl2indG tgst)
mcl2indS (trec tgst) = rec (mcl2indG tgst)
mcl2indS (tvar x) = var x

mcl2indG (ttransmit d t s) = transmit d (mcl2indT t) (mcl2indS s)
mcl2indG (tchoice d m alt) = choice d m (λ x → mcl2indS (alt x))
mcl2indG end = end

mcl2indT MClTUnit = TUnit
mcl2indT MClTInt = TInt
mcl2indT (MClTPair t t₁) = TPair (mcl2indT t) (mcl2indT t₁)
mcl2indT{n} (MClTChan x) = TChan (weakenS n x)

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

stack2StackS : Stack n → StackS n
stack2StackS ε = ε
stack2StackS ⟪ σ , x ⟫ = ⟪ (stack2StackS σ) , (rec x) ⟫

stackMCl2Stack : StackMCl n → Stack n
stackMCl2Stack ε = ε
stackMCl2Stack ⟪ σ , x ⟫ = ⟪ (stackMCl2Stack σ) , (mcl2indG x) ⟫

stackMCl2StackS : StackMCl n → StackS n
stackMCl2StackS ε = ε
stackMCl2StackS ⟪ σ , x ⟫ = ⟪ (stackMCl2StackS σ) , (rec (mcl2indG x)) ⟫

stack2StackMCl : Stack n → StackMCl n
stack2StackMCl ε = ε
stack2StackMCl ⟪ σ , x ⟫ = ⟪ (stack2StackMCl σ) , (mclG ⟪ stack2StackS σ , rec x ⟫ x) ⟫

stack2Stack' : Stack n → Stack' 0 n
stack2Stack' ε = ε
stack2Stack' ⟪ σ , x ⟫ = ⟪ stack2Stack' σ , x ⟫

stack'2Stack : Stack' 0 n → Stack n
stack'2Stack ε = ε
stack'2Stack ⟪ σ , x ⟫ = ⟪ stack'2Stack σ , x ⟫

stack'2Stack'S : Stack' n m → Stack'S n m
stack'2Stack'S ε = ε
stack'2Stack'S ⟪ σ , x ⟫ = ⟪ (stack'2Stack'S σ) , (rec x) ⟫

stack-stack'-refl : (σ : Stack n) → (stack'2Stack (stack2Stack' σ)) ≡ σ
stack-stack'-refl ε = refl
stack-stack'-refl ⟪ σ , x ⟫ rewrite (stack-stack'-refl σ) = refl

{-# REWRITE stack-stack'-refl #-}

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

naive-dualS : SType n → SType n
naive-dualG : GType n → GType n
naive-dualT : Type n → Type n

naive-dualS (gdd gst) = gdd (naive-dualG gst)
naive-dualS (rec gst) = rec (naive-dualG gst)
naive-dualS (var x) = var x

naive-dualG (transmit d t s) = transmit (dual-dir d) (naive-dualT t) (naive-dualS s)
naive-dualG (choice d m alt) = choice (dual-dir d) m (λ x → naive-dualS (alt x))
naive-dualG end = end

naive-dualT TUnit = TUnit
naive-dualT TInt = TInt
naive-dualT (TPair t t₁) = TPair (naive-dualT t) (naive-dualT t₁)
naive-dualT (TChan x) = TChan (naive-dualS x)

naive-dualSt : MClSType n → MClSType n
naive-dualGt : MClGType n → MClGType n
naive-dualTt : MClType n → MClType n

naive-dualSt (tgdd tgst) = tgdd (naive-dualGt tgst)
naive-dualSt (trec tgst) = trec (naive-dualGt tgst)
naive-dualSt (tvar x) = tvar x

naive-dualGt (ttransmit d t s) = ttransmit (dual-dir d) (naive-dualTt t) (naive-dualSt s)
naive-dualGt (tchoice d m alt) = tchoice (dual-dir d) m (λ x → naive-dualSt (alt x))
naive-dualGt end = end

naive-dualTt MClTUnit = MClTUnit
naive-dualTt MClTInt = MClTInt
naive-dualTt (MClTPair t t₁) = MClTPair (naive-dualTt t) (naive-dualTt t₁)
naive-dualTt (MClTChan x) = MClTChan (naive-dualS x)

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

dualS : (σ : StackS n) → SType n → MClSType n
dualG : (σ : StackS n) → GType n → MClGType n
dualT : (σ : StackS n) → Type n → MClType n

dualS σ (gdd gst) = tgdd (dualG σ gst)
dualS σ (rec gst) = trec (dualG ⟪ σ , (rec gst) ⟫ gst)
dualS σ (var x)   = (tvar x)

dualG{n} σ (transmit d t s) = ttransmit (dual-dir d) (dualT σ t) (dualS σ s)
dualG σ (choice d m alt) = tchoice (dual-dir d) m ((dualS σ) ∘ alt)
dualG σ end = end

dualT σ TUnit = MClTUnit
dualT σ TInt = MClTInt
dualT σ (TPair t t₁) = MClTPair (dualT σ t) (dualT σ t₁)
dualT σ (TChan x) = MClTChan (stack-sim-substS (stack-transform σ) x)

module sanity-check where
  -- μx.!x.x → μx.?(μx.!x.x).x
  S : SType 0
  S = rec (transmit SND (TChan (var zero)) (var zero))
  DS = rec (transmit RCV (weaken1T (TChan S)) (var zero))

  _ : mclS ε DS ≡ dualS ε S
  _ = refl

  -- μx.!x.!x.x → μx.?(μx.!x.!x.x).?(μx.!x.!x.x).x
  S' : SType 0
  S' = rec (transmit SND (TChan (var zero)) (gdd ((transmit SND (TChan (var zero)) (var zero)))))
  DS' =  rec (transmit RCV (weaken1T (TChan S')) (gdd ((transmit RCV (weaken1T (TChan S')) (var zero)))))

  _ : mclS ε DS' ≡ dualS ε S'
  _ = refl

  -- μx.!x.(μy.!y.y) → μx.?(μx.!x.(μy.!y.y)).(μy.?(μy.!y.y).y)
  S'' : SType 0
  S'' = rec (transmit SND (TChan (var zero)) (rec (transmit SND (TChan (var zero)) (var zero))))
  DS'' = rec (transmit RCV (weaken1T (TChan S'')) (weaken1S DS))

  _ : mclS ε DS'' ≡ dualS ε S''
  _ = refl

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

open import DualCoinductive hiding (n ; m)

_≈_ = COI._≈_
_≈'_ = COI._≈'_
_≈ᵗ_ = COI._≈ᵗ_

-- IND to Coinductive using two stacks
-- e.g. i = 0 => σ
--      i = 1 => σ , g         -- g = get σ' 0
--      i = 2F => σ , g' , g    -- g = get σ' 0; g' = get σ' 1
--      i = n  => σ'
ind2coiS' : (i : Fin (suc n)) → Stack (n ∸ toℕ i) → Stack' (n ∸ toℕ i) (toℕ i) → IND.SType n → COI.SType
ind2coiG' : (i : Fin (suc n)) → Stack (n ∸ toℕ i) → Stack' (n ∸ toℕ i) (toℕ i) → IND.GType n → COI.STypeF COI.SType
ind2coiT' : (i : Fin (suc n)) → Stack (n ∸ toℕ i) → Stack' (n ∸ toℕ i) (toℕ i) → IND.Type n → COI.Type

COI.SType.force (ind2coiS' i σ σ' (gdd gst)) = ind2coiG' i σ σ' gst
COI.SType.force (ind2coiS'{n} i σ σ' (rec gst)) = ind2coiG' (suc i) σ ⟪ σ' , gst ⟫ gst
COI.SType.force (ind2coiS' i σ σ' (var x)) = {!!}

-- IND to Coinductive
ind2coiS : Stack n → IND.SType n → COI.SType
ind2coiG : Stack n → IND.GType n → COI.STypeF COI.SType
ind2coiT : Stack n → IND.Type n → COI.Type

ind2coiT σ TUnit = COI.TUnit
ind2coiT σ TInt = COI.TInt
ind2coiT σ (TPair t t₁) = COI.TPair (ind2coiT σ t) (ind2coiT σ t₁)
ind2coiT σ (TChan x) = COI.TChan (ind2coiS σ x)

COI.SType.force (ind2coiS σ (gdd gst)) = ind2coiG σ gst
COI.SType.force (ind2coiS σ (rec gst)) = ind2coiG ⟪ σ , gst ⟫ gst
COI.SType.force (ind2coiS{n} σ (var x))
  with get x σ
... | σ' , gxs rewrite (n∸x≡suc[n∸sucx]{n}{toℕ x} toℕx<n) = ind2coiG ⟪ σ' , gxs ⟫ gxs

ind2coiG σ (transmit d t s) = COI.transmit d (ind2coiT σ t) (ind2coiS σ s)
ind2coiG σ (choice d m alt) = COI.choice d m (λ x → ind2coiS σ (alt x))
ind2coiG σ end = COI.end

-- IND to Coinductive using StackS0
ind2coiS'' : StackS0 n → IND.SType n → COI.SType
ind2coiG'' : StackS0 n → IND.GType n → COI.STypeF COI.SType

COI.SType.force (ind2coiS'' σ (gdd gst)) = ind2coiG'' σ gst
COI.SType.force (ind2coiS''{n} σ (rec gst)) = ind2coiG''{suc n} ⟪ σ , stack-sim-substS σ (rec gst) ⟫ gst
ind2coiS'' σ (var x)
  with getS0 x σ
... | σ' , gxs = ind2coiS'' ε gxs

-- Equivalence of IND to COI with one stack and IND to COI with two stacks
ind2coiS≈ind2coiS' : (σ : Stack' 0 n) (s : IND.SType n)
  → ind2coiS' (fromℕ n) ε σ s ≈ ind2coiS (stack'2Stack σ) s
ind2coiG≈ind2coiG' : (σ : Stack' 0 n) (g : IND.GType n)
  → ind2coiG' (fromℕ n) ε σ g ≈' ind2coiG (stack'2Stack σ) g

COI.Equiv.force (ind2coiS≈ind2coiS' σ (gdd gst)) = ind2coiG≈ind2coiG' σ gst
COI.Equiv.force (ind2coiS≈ind2coiS'{n} σ (rec gst)) = ind2coiG≈ind2coiG'{suc n} ⟪ σ , gst ⟫ gst
COI.Equiv.force (ind2coiS≈ind2coiS' σ (var x)) = {!!}

-- Message closure to Coinductive
mcl2coiT : StackMCl n → MClType n → COI.Type
mcl2coiS : StackMCl n → MClSType n → COI.SType
mcl2coiG : StackMCl n → MClGType n → COI.STypeF COI.SType

mcl2coiT σ MClTUnit = COI.TUnit
mcl2coiT σ MClTInt = COI.TInt
mcl2coiT σ (MClTPair t t₁) = COI.TPair (mcl2coiT σ t) (mcl2coiT σ t₁)
mcl2coiT σ (MClTChan s) = COI.TChan (ind2coiS ε s)

COI.SType.force (mcl2coiS σ (tgdd g)) = mcl2coiG σ g
COI.SType.force (mcl2coiS σ (trec g)) = mcl2coiG ⟪ σ , g ⟫ g
COI.SType.force (mcl2coiS{n} σ (tvar x))
  with getMCl x σ
... | σ' , gxs rewrite (n∸x≡suc[n∸sucx]{n}{toℕ x} toℕx<n) = mcl2coiG ⟪ σ' , gxs ⟫ gxs

mcl2coiG σ (ttransmit d t s) = COI.transmit d (mcl2coiT σ t) (mcl2coiS σ s)
mcl2coiG σ (tchoice d m alt) = COI.choice d m (mcl2coiS σ ∘ alt)
mcl2coiG σ end = COI.end

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

-- lemm 1
-- stack-sim-substS (stack-transform ⟪ stack2StackS σ , (rec x) ⟫) s ≡ stack-sim-substS (stack-transform (stack2StackS σ)) (st-substS' 0 (rec x) s)

-- lemm 2
-- ind2coiS ⟪ σ , x ⟫ s ≈ ind2coiS σ (st-substS' 0 (rec x) s)

-- unfolding vs single substitution
ind2coi-substS : (σ : Stack n) (g : GType (suc n)) (s : SType (suc n)) →
  ind2coiS ⟪ σ , g ⟫ s ≈ ind2coiS σ (st-substS' zero (rec g) s)
ind2coi-substG : (σ : Stack n) (g : GType (suc n)) (g' : GType (suc n)) →
  ind2coiG ⟪ σ , g ⟫ g' ≈' ind2coiG σ (st-substG' zero (rec g) g')

COI.Equiv.force (ind2coi-substS σ g (gdd gst)) = ind2coi-substG σ g gst
COI.Equiv.force (ind2coi-substS σ g (rec gst)) = {!!}
-- the following line for rec-case is a contradiction for gst = transmit d t (var 1)
-- COI.≈'-trans (COI.≈'-trans (ind2coi-substG ⟪ σ , g ⟫ gst gst) (ind2coi-substG σ g (st-substG' 0 (rec gst) gst))) (COI.≈'-trans {!!} (COI.≈'-symm (ind2coi-substG σ (st-substG' 1 (weaken1S (rec g)) gst) (st-substG' 1 (weaken1S (rec g)) gst))))
COI.Equiv.force (ind2coi-substS σ g (var zero)) = COI.≈'-refl
COI.Equiv.force (ind2coi-substS {n} σ g (var (suc x))) = {!!}

ind2coi-substG σ g (transmit d t s) = COI.eq-transmit d {!!} (ind2coi-substS σ g s)
ind2coi-substG σ g (choice d m alt) = COI.eq-choice d λ i → ind2coi-substS σ g (alt i)
ind2coi-substG σ g end = COI.eq-end

-- unfolding vs simultaneous substitution: special, needed case
st-unfold : {n : ℕ} (σ : Stack n) (s : IND.SType n) →
  ind2coiS ε (stack-sim-substS (stack-transform (stack2StackS σ)) s) ≈ ind2coiS σ s
st-unfold {0} ε s rewrite (stack-sim-substS-refl s) = COI.≈-refl
st-unfold {suc n} ⟪ σ , x ⟫ s = {!st-unfold σ (st-substS' 0 (rec x) s)!} -- provable if lemm 1 & lemm 2 hold

-- unfolding vs simultaneous substitution: general case
stack-unfoldS : (σ : Stack n) (σ' : Stack' n m) (s : IND.SType (n + m)) →
  ind2coiS σ (stack-sim-substS'-top (stack-transform' (stack'2Stack'S σ')) s) ≈ ind2coiS (stack-cat σ σ') s

COI.Equiv.force (stack-unfoldS {n} σ σ' (gdd gst)) = {!!}
COI.Equiv.force (stack-unfoldS σ σ' (rec gst)) = {!!}
COI.Equiv.force (stack-unfoldS {n} σ σ' (var x)) = {!!}

-- unfolding vs simultaneous substition: general case w/ alt. def. for ind2coiS
stack-unfoldS' : (i : Fin (suc n)) (σ : Stack (n ∸ toℕ i)) (σ' : Stack' (n ∸ toℕ i) (toℕ i)) (s : IND.SType n) →
  ind2coiS σ (stack-sim-substS'-top (stack-transform' (stack'2Stack'S σ')) s) ≈ ind2coiS' i σ σ' s

COI.Equiv.force (stack-unfoldS' i σ σ' (gdd gst)) = {!!}
COI.Equiv.force (stack-unfoldS' i σ σ' (rec gst)) = {!!} -- req. first lemma from graveyard of lemmas
COI.Equiv.force (stack-unfoldS' i σ σ' (var x)) = {!!}

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

-- proof idea for var case:
-- mcl2coiS (stack2StackMCl σ) (tvar x)
-------- getMCl x (stack2StackMCl σ) = σ' , g
-- => mcl2coiG ⟪ σ' , g ⟫ g
-------- getMCl x (stack2StackMCl σ) = (stack2StackMCl (get x σ).1 , mclG ⟪ stack2StackS (get x σ).1 , rec (get x σ).2 ⟫ (get x σ).2
-- => mcl2coiG ⟪ (stack2StackMCl (get x σ).1 , mclG ⟪ stack2StackS (get x σ).1 , rec (get x σ).2 ⟫ (get x σ).2 ⟫ (mclG ⟪ stack2StackS (get x σ).1 , rec (get x σ).2 ⟫ (get x σ).2)
------- which by definition of stack2StackMCl and stack2StackS is equivalent to
-- = mcl2coiG (stack2StackMCl ⟪ (get x σ).1 , (get x σ).2 ⟫) (mclG (stack2StackS ⟪ (get x σ).1 , (get x σ).2 ⟫) g)
------- which, by mcl-equiv-G
-- ≈' ind2coiG ⟪ (get x σ).1 , (get x σ).2 ⟫ (get x σ).2
-- = ind2coiG σ (var x)

getMCl-get : (x : Fin n) (σ : Stack n)
  → getMCl x (stack2StackMCl σ) ≡ (stack2StackMCl (proj₁ (get x σ)) , mclG ⟪ stack2StackS (proj₁ (get x σ)) , rec (proj₂ (get x σ)) ⟫  (proj₂ (get x σ)))
getMCl-get zero ⟪ σ , x ⟫ = refl
getMCl-get (suc x) ⟪ σ , x₁ ⟫ = getMCl-get x σ

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

mcl-equiv-S : (σ : Stack n) (s : IND.SType n) →
  mcl2coiS (stack2StackMCl σ) (mclS (stack2StackS σ) s) ≈ ind2coiS σ s
mcl-equiv-G : (σ : Stack n) (g : IND.GType n) →
  mcl2coiG (stack2StackMCl σ) (mclG (stack2StackS σ) g) ≈' ind2coiG σ g
mcl-equiv-T : (σ : Stack n) (t : IND.Type n) →
  mcl2coiT (stack2StackMCl σ) (mclT (stack2StackS σ) t) ≈ᵗ ind2coiT σ t

COI.Equiv.force (mcl-equiv-S σ (gdd gst)) = mcl-equiv-G σ gst
COI.Equiv.force (mcl-equiv-S σ (rec gst)) = mcl-equiv-G ⟪ σ , gst ⟫ gst
COI.Equiv.force (mcl-equiv-S{n} σ (var x))
  rewrite (getMCl-get x σ)
  with (proj₁ (get x σ)) | (proj₂ (get x σ))
... | σ' | g  rewrite (n∸x≡suc[n∸sucx]{n}{toℕ x} toℕx<n) = mcl-equiv-G ⟪ σ' , g ⟫ g

mcl-equiv-G σ (transmit d t s) = COI.eq-transmit d (mcl-equiv-T σ t) (mcl-equiv-S σ s)
mcl-equiv-G σ (choice d m alt) = COI.eq-choice d (λ i → mcl-equiv-S σ (alt i))
mcl-equiv-G σ end = COI.eq-end

mcl-equiv-T σ TUnit = COI.eq-unit
mcl-equiv-T σ TInt = COI.eq-int
mcl-equiv-T σ (TPair t t₁) = COI.eq-pair (mcl-equiv-T σ t) (mcl-equiv-T σ t₁)
mcl-equiv-T {n} σ (TChan x) = COI.eq-chan {!!}

σ : Stack 1
σ = ⟪ ε , end ⟫

g : GType 2
g = transmit SND TInt (var (suc zero))

s : COI.SType
s = ind2coiS σ (rec g)

s' : COI.SType
s' = ind2coiS ε (stack-sim-substS (stack-transform (stack2StackS σ)) (rec g))

s≈s' : s ≈ s'
COI.Equiv.force s≈s' = COI.eq-transmit SND COI.eq-int (record { force = COI.eq-end })

-- naive-mcl-dual : (σ : StackMCl n) (s : IND.SType n) →
--  mcl2coiS σ (naive-dualSt (mclS (stackTail2StackS σ) s)) ≈ mcl2coiS σ (dualS (stackTail2StackS σ) s)

{- graveyard of attempted lemmas

-- idea: "move" a substitution that is done at stack unfolding to a simultaneous subtitution before unfolding
-- problem: cannot formulate this for SType since Stack requires a GType

stack-unfold-lemmaG : {m n : ℕ} (σ : Stack n) (σ' : Stack' n m) (g : GType (suc (n + m))) →
  ind2coiG ⟪ σ , stack-sim-substG'-top (weaken1-Stack'Sn 0 (stack-transform' (stack'2Stack'S σ'))) g ⟫ (stack-sim-substG'-top (weaken1-Stack'Sn 0 (stack-transform' (stack'2Stack'S σ'))) g)
   ≈'
  ind2coiG σ (stack-sim-substG'-top (stack-transform' (stack'2Stack'S ⟪ σ' , g ⟫)) g)

stack-unfold-lemmaG {m} {n} σ σ' (transmit d t s) = {!!}
stack-unfold-lemmaG {m} {n} σ σ' (choice d m₁ alt) = {!!}
stack-unfold-lemmaG {m} {n} σ σ' end = {!!}

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

-- won't work for the same reason as below
stack-unfoldS-i : (i : Fin n) (σ : Stack n) (s : IND.SType (suc (n ∸ suc (toℕ i) + toℕ i)))
  → ind2coiS (proj₁ (stack-split i σ)) (stack-sim-substS'-top (stack-transform' (stack'2Stack'S (proj₂ (stack-split i σ)))) s) ≈ ind2coiS σ (rewrfixS{n}{i} s)
stack-unfoldG-i : (i : Fin n) (σ : Stack n) (g : IND.GType (suc (n ∸ suc (toℕ i) + toℕ i)))
  → ind2coiG (proj₁ (stack-split i σ)) (stack-sim-substG'-top (stack-transform' (stack'2Stack'S (proj₂ (stack-split i σ)))) g) ≈' ind2coiG σ (rewrfixG{n}{i} g)

COI.Equiv.force (stack-unfoldS-i i σ (gdd gst)) = {!!}
COI.Equiv.force (stack-unfoldS-i{n} i σ (rec gst)) = {!stack-unfoldG-i (suc i) ? gst!}
COI.Equiv.force (stack-unfoldS-i i σ (var x)) = {!!}

-- won't work. rec case adds something to σ on the left side, but something at the end of (stack-cat σ σ') on the right side.
stack-unfoldS' : (σ : Stack n) (σ' : Stack' n m) (s : IND.SType (n + m)) →
  ind2coiS σ (stack-sim-substS'-top (stack-transform' (stack'2Stack'S σ')) s) ≈ ind2coiS (stack-cat σ σ') s
stack-unfoldG' : (σ : Stack n) (σ' : Stack' n m) (g : IND.GType (n + m)) →
  ind2coiG σ (stack-sim-substG'-top (stack-transform' (stack'2Stack'S σ')) g) ≈' ind2coiG (stack-cat σ σ') g

COI.Equiv.force (stack-unfoldS' σ σ' (gdd gst)) = {!!}
COI.Equiv.force (stack-unfoldS'{n}{m} σ σ' (rec gst)) = {!!} -- {!stack-unfoldG'{suc n}{m} ⟪ σ , stack-sim-substG'-top-i≥ 1 (stack-transform' (stack'2Stack'S σ')) gst ⟫ (weaken1-Stack' 0 σ') gst!}
COI.Equiv.force (stack-unfoldS' σ σ' (var x)) = {!!}

-}

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.Solver where

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base
open import Cubical.Algebra.RingSolver.AlmostRing
open import Cubical.Algebra.RingSolver.RawRing renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.RingSolver.RingExpression
open import Cubical.Algebra.RingSolver.HornerForms
open import Cubical.Algebra.RingSolver.EvaluationHomomorphism

private
  variable
    ℓ : Level

module EqualityToNormalform (R : AlmostRing {ℓ}) where
  νR = AlmostRing→RawRing R
  open AlmostRing R
  open Theory R
  open Eval νR
  open IteratedHornerOperations νR
  open HomomorphismProperties R

  normalize : (n : ℕ) → Expr ⟨ R ⟩ n → IteratedHornerForms νR n
  normalize n (K r) = Constant n νR r
  normalize n (∣ k) = Variable n νR k
  normalize n (x ⊕ y) =
    (normalize n x) +ₕ (normalize n y)
  normalize n (x ⊗ y) =
    (normalize n x) ·ₕ (normalize n y)
  normalize n (⊝ x) =  -ₕ (normalize n x)

  isEqualToNormalform :
            (n : ℕ)
            (e : Expr ⟨ R ⟩ n) (xs : Vec ⟨ R ⟩ n)
          → eval n (normalize n e) xs ≡ ⟦ e ⟧ xs
  isEqualToNormalform ℕ.zero (K r) [] = refl
  isEqualToNormalform (ℕ.suc n) (K r) (x ∷ xs) =
     eval (ℕ.suc n) (Constant (ℕ.suc n) νR r) (x ∷ xs)           ≡⟨ refl ⟩
     eval (ℕ.suc n) (0ₕ ·X+ Constant n νR r) (x ∷ xs)             ≡⟨ refl ⟩
     eval (ℕ.suc n) 0ₕ (x ∷ xs) · x + eval n (Constant n νR r) xs
    ≡⟨ cong (λ u → u · x + eval n (Constant n νR r) xs) (eval0H _ (x ∷ xs)) ⟩
     0r · x + eval n (Constant n νR r) xs
    ≡⟨ cong (λ u → u + eval n (Constant n νR r) xs) (0LeftAnnihilates _) ⟩
     0r + eval n (Constant n νR r) xs                             ≡⟨ +Lid _ ⟩
     eval n (Constant n νR r) xs
    ≡⟨ isEqualToNormalform n (K r) xs ⟩
     r ∎

  isEqualToNormalform (ℕ.suc n) (∣ zero) (x ∷ xs) =
    eval (ℕ.suc n) (1ₕ ·X+ 0ₕ) (x ∷ xs)           ≡⟨ refl ⟩
    eval (ℕ.suc n) 1ₕ (x ∷ xs) · x + eval n 0ₕ xs ≡⟨ cong (λ u → u · x + eval n 0ₕ xs)
                                                          (eval1ₕ _ (x ∷ xs)) ⟩
    1r · x + eval n 0ₕ xs                         ≡⟨ cong (λ u → 1r · x + u ) (eval0H _ xs) ⟩
    1r · x + 0r                                   ≡⟨ +Rid _ ⟩
    1r · x                                        ≡⟨ ·Lid _ ⟩
    x ∎
  isEqualToNormalform (ℕ.suc n) (∣ (suc k)) (x ∷ xs) =
      eval (ℕ.suc n) (0ₕ ·X+ Variable n νR k) (x ∷ xs)             ≡⟨ refl ⟩
      eval (ℕ.suc n) 0ₕ (x ∷ xs) · x + eval n (Variable n νR k) xs
    ≡⟨ cong (λ u → u · x + eval n (Variable n νR k) xs) (eval0H _ (x ∷ xs)) ⟩
      0r · x + eval n (Variable n νR k) xs
    ≡⟨ cong (λ u → u + eval n (Variable n νR k) xs) (0LeftAnnihilates _) ⟩
      0r + eval n (Variable n νR k) xs                             ≡⟨ +Lid _ ⟩
      eval n (Variable n νR k) xs
    ≡⟨ isEqualToNormalform n (∣ k) xs ⟩
      ⟦ ∣ (suc k) ⟧ (x ∷ xs) ∎

  isEqualToNormalform ℕ.zero (⊝ e) [] =
    eval ℕ.zero (-ₕ (normalize ℕ.zero e)) [] ≡⟨ -evalDist ℕ.zero
                                                                  (normalize ℕ.zero e)
                                                                  [] ⟩
    - eval ℕ.zero (normalize ℕ.zero e) []    ≡⟨ cong -_
                                                          (isEqualToNormalform
                                                            ℕ.zero e [] ) ⟩
    - ⟦ e ⟧ [] ∎
  isEqualToNormalform (ℕ.suc n) (⊝ e) (x ∷ xs) =
    eval (ℕ.suc n) (-ₕ (normalize (ℕ.suc n) e)) (x ∷ xs) ≡⟨ -evalDist (ℕ.suc n)
                                                                  (normalize
                                                                    (ℕ.suc n) e)
                                                                  (x ∷ xs) ⟩
    - eval (ℕ.suc n) (normalize (ℕ.suc n) e) (x ∷ xs)    ≡⟨ cong -_
                                                          (isEqualToNormalform
                                                            (ℕ.suc n) e (x ∷ xs) ) ⟩
    - ⟦ e ⟧ (x ∷ xs) ∎

  isEqualToNormalform ℕ.zero (e ⊕ e₁) [] =
        eval ℕ.zero (normalize ℕ.zero e +ₕ normalize ℕ.zero e₁) []
      ≡⟨ +Homeval ℕ.zero (normalize ℕ.zero e) _ [] ⟩
        eval ℕ.zero (normalize ℕ.zero e) []
        + eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → u + eval ℕ.zero (normalize ℕ.zero e₁) [])
              (isEqualToNormalform ℕ.zero e []) ⟩
        ⟦ e ⟧ []
        + eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] + u) (isEqualToNormalform ℕ.zero e₁ []) ⟩
        ⟦ e ⟧ [] + ⟦ e₁ ⟧ [] ∎
  isEqualToNormalform (ℕ.suc n) (e ⊕ e₁) (x ∷ xs) =
        eval (ℕ.suc n) (normalize (ℕ.suc n) e
                         +ₕ normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ +Homeval (ℕ.suc n) (normalize (ℕ.suc n) e) _ (x ∷ xs) ⟩
        eval (ℕ.suc n) (normalize (ℕ.suc n) e) (x ∷ xs)
        + eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u + eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs))
              (isEqualToNormalform (ℕ.suc n) e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs)
        + eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) + u)
              (isEqualToNormalform (ℕ.suc n) e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) + ⟦ e₁ ⟧ (x ∷ xs) ∎

  isEqualToNormalform ℕ.zero (e ⊗ e₁) [] =
        eval ℕ.zero (normalize ℕ.zero e ·ₕ normalize ℕ.zero e₁) []
      ≡⟨ ·Homeval ℕ.zero (normalize ℕ.zero e) _ [] ⟩
        eval ℕ.zero (normalize ℕ.zero e) []
        · eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → u · eval ℕ.zero (normalize ℕ.zero e₁) [])
              (isEqualToNormalform ℕ.zero e []) ⟩
        ⟦ e ⟧ []
        · eval ℕ.zero (normalize ℕ.zero e₁) []
      ≡⟨ cong (λ u → ⟦ e ⟧ [] · u) (isEqualToNormalform ℕ.zero e₁ []) ⟩
        ⟦ e ⟧ [] · ⟦ e₁ ⟧ [] ∎

  isEqualToNormalform (ℕ.suc n) (e ⊗ e₁) (x ∷ xs) =
        eval (ℕ.suc n) (normalize (ℕ.suc n) e
                         ·ₕ normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ ·Homeval (ℕ.suc n) (normalize (ℕ.suc n) e) _ (x ∷ xs) ⟩
        eval (ℕ.suc n) (normalize (ℕ.suc n) e) (x ∷ xs)
        · eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → u · eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs))
              (isEqualToNormalform (ℕ.suc n) e (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs)
        · eval (ℕ.suc n) (normalize (ℕ.suc n) e₁) (x ∷ xs)
      ≡⟨ cong (λ u → ⟦ e ⟧ (x ∷ xs) · u)
              (isEqualToNormalform (ℕ.suc n) e₁ (x ∷ xs)) ⟩
        ⟦ e ⟧ (x ∷ xs) · ⟦ e₁ ⟧ (x ∷ xs) ∎

  solve :
    {n : ℕ} (e₁ e₂ : Expr ⟨ R ⟩ n) (xs : Vec ⟨ R ⟩ n)
    (p : eval n (normalize n e₁) xs ≡ eval n (normalize n e₂) xs)
    → ⟦ e₁ ⟧ xs ≡ ⟦ e₂ ⟧ xs
  solve e₁ e₂ xs p =
    ⟦ e₁ ⟧ xs                  ≡⟨ sym (isEqualToNormalform _ e₁ xs) ⟩
    eval _ (normalize _ e₁) xs ≡⟨ p ⟩
    eval _ (normalize _ e₂) xs ≡⟨ isEqualToNormalform _ e₂ xs ⟩
    ⟦ e₂ ⟧ xs ∎

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Number.Instances.Nat where

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

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

open import Cubical.HITs.PropositionalTruncation --.Properties

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

open import Cubical.Data.Nat as Nat renaming (_*_ to _·_)
open import Cubical.Data.Nat.Order renaming (_<_ to _<ᵗ_)
open import Cubical.Data.Nat.Properties using
  ( inj-*sm
  ; inj-sm*
  ) renaming
  ( *-distribʳ  to ·-distribʳ
  ; *-distribˡ  to ·-distribˡ
  ; *-assoc     to ·-assoc
  ; *-comm      to ·-comm
  ; *-identityʳ to ·-identityʳ
  ; *-identityˡ to ·-identityˡ
  )
-- open import Data.Nat.Properties using (+-assoc)
open import Data.Nat.Base using () renaming
  ( _⊔_ to max
  ; _⊓_ to min
  )

-- _<_ as an hProp-valued relation
_<_ : (x y : ℕ) → hProp ℓ-zero
(x < y) .fst = x <ᵗ y
(x < y) .snd (k₁ , k₁+sx≡y) (k₂ , k₂+sx≡y) = φ where
  abstract φ = Σ≡Prop (λ k → isSetℕ _ _) (inj-+m (k₁+sx≡y ∙ sym k₂+sx≡y))

0<suc : ∀ a → 0 <ᵗ suc a
0<suc a = a , +-comm a 1

·-nullifiesˡ : ∀ x → 0 · x ≡ 0
·-nullifiesˡ x = refl

·-nullifiesʳ : ∀ x → x · 0 ≡ 0
·-nullifiesʳ zero = refl
·-nullifiesʳ (suc x) = ·-nullifiesʳ x

abstract
  lemma10   : ∀ n → (n <ᵗ 0) ≡ [ ⊥ ]
  lemma10   n = isoToPath (iso (λ{ (k , p) → snotz (sym (+-suc k n) ∙ p) }) ⊥-elim (λ b → isProp⊥ _ _) (λ a → isProp[] (n < 0) _ _))

  lemma10'' : ∀ n → (n < 0) ≡ ⊥
  lemma10'' n = ⇔toPath (transport (lemma10 n)) (transport (sym (lemma10 n)))

  lemma12 : ∀ n → [ 0 < suc n ] ≡ [ ⊤ ]
  lemma12 n = isoToPath (iso (λ _ →  tt) (λ _ → n , +-suc n 0 ∙ (λ i → suc (+-zero n i))) (λ b → isProp⊤ _ _) (λ a → isProp[] (0 < suc n) _ _))

  lemma12'' : ∀ n → (0 < suc n) ≡ ⊤
  lemma12'' n = ⇔toPath (transport (lemma12 n)) (transport (sym (lemma12 n)))

abstract
  <-irrefl       : (a       : ℕ) → [ ¬ (a < a) ]
  <-irrefl zero q = transp (λ i → [ lemma10'' 0 i ]) i0 q
  <-irrefl (suc a) (k , p) =
    snotz (inj-m+ {a} (+-suc a k ∙ (λ i → suc (+-comm a k i)) ∙ sym (+-suc k a) ∙ inj-m+ {1} (sym (+-suc k (suc a)) ∙ p) ∙ sym (+-zero a)))

  suc-creates-< : ∀ a b → [ a < b ⇔ suc a < suc b ]
  suc-creates-< a b .fst (k , p) = k , (+-suc k (suc a)) ∙ (λ i → suc (p i))
  suc-creates-< a b .snd (k , p) = k , inj-m+ {1} (sym (+-suc k (suc a)) ∙ p)

  +-createsˡ-< : ∀ a b x → [ a < b ⇔ (x + a) < (x + b) ]
  +-createsˡ-< a b  zero   .fst a<b = a<b
  +-createsˡ-< a b (suc x) .fst a<b = suc-creates-< (x + a) (x + b) .fst $ +-createsˡ-< a b x .fst a<b
  +-createsˡ-< a b zero .snd a<b = a<b
  +-createsˡ-< a b (suc x) .snd p = +-createsˡ-< a b x .snd (suc-creates-< (x + a) (x + b) .snd p)

  +-createsʳ-< : ∀ a b x → [ a < b ⇔ (a + x) < (b + x) ]
  +-createsʳ-< a b x .fst p = transport (λ i → [ +-comm x a i < +-comm x b i ]) $ +-createsˡ-< a b x .fst p
  +-createsʳ-< a b x .snd p = +-createsˡ-< a b x .snd (transport (λ i → [ +-comm a x i < +-comm b x i ]) p)

  <-cotrans      : (a b     : ℕ) → [ a < b ] → (x : ℕ) → [ (a < x) ⊔ (x < b) ]
  <-cotrans  zero    zero        q      c  = ⊥-elim {A = λ _ → [ (zero < c) ⊔ (c < zero) ]}  (<-irrefl _ q)
  <-cotrans  zero   (suc b)      q  zero   = inrᵖ q
  <-cotrans  zero   (suc b)      q (suc c) = inlᵖ (c , +-comm c 1)
  <-cotrans (suc a)  zero   (k , p)     c  = ⊥-elim {A = λ _ → [ (suc a < c) ⊔ (c < zero) ]} (snotz (sym (+-suc k (suc a)) ∙ p))
  <-cotrans (suc a) (suc b)      q  zero   = inrᵖ (b , +-comm b 1)
  <-cotrans (suc a) (suc b)      q (suc c) = transport (λ i → [ r i ⊔ s i ]) (<-cotrans a b (suc-creates-< a b .snd q) c)
    where r : (a < c) ≡ (suc a < suc c)
          s : (c < b) ≡ (suc c < suc b)
          r = ⇔toPath (suc-creates-< a c .fst) (suc-creates-< a c .snd)
          s = ⇔toPath (suc-creates-< c b .fst) (suc-creates-< c b .snd)

·-reflects-≡ʳ : ∀ a b x → [ 0 < x ] → a · x ≡ b · x → a ≡ b
·-reflects-≡ʳ a b zero    p q = ⊥-elim {A = λ _ → a ≡ b} $ <-irrefl 0 p
·-reflects-≡ʳ a b (suc x) p q = inj-*sm {l = a} {m = x} {n = b} q

·-reflects-≡ˡ : ∀ a b x → [ 0 < x ] → x · a ≡ x · b → a ≡ b
·-reflects-≡ˡ a b zero    p q = ⊥-elim {A = λ _ → a ≡ b} $ <-irrefl 0 p
·-reflects-≡ˡ a b (suc x) p q = inj-sm* {m = x} {l = a} {n = b} q

¬suc<0 : ∀ x → [ ¬ (suc x < 0) ]
¬suc<0 x (k , p) = snotz $ sym (+-suc k (suc x)) ∙ p

·-reflects-< : ∀ a b x → [ 0 < x ] → [ (a · x) < (b · x) ] → [ a < b ]
·-reflects-< zero zero x p q = q
·-reflects-< zero (suc b) x p q = 0<suc b
·-reflects-< (suc a) zero x p q = ⊥-elim {A = λ _ → [ suc a < 0 ]} $ ¬-<-zero q
·-reflects-< (suc a) (suc b) x p q = suc-creates-< a b .fst $ ·-reflects-< a b x p (+-createsˡ-< (a · x) (b · x) x .snd q)

min-comm : ∀ x y → min x y ≡ min y x
min-comm zero zero = refl
min-comm zero (suc y) = refl
min-comm (suc x) zero = refl
min-comm (suc x) (suc y) i = suc $ min-comm x y i

min-tightˡ : ∀ x y → [ x < y ] → min x y ≡ x
min-tightˡ zero zero x<y = refl
min-tightˡ zero (suc y) x<y = refl
min-tightˡ (suc x) zero x<y = ⊥-elim {A = λ _ → zero ≡ suc x} (¬suc<0 x x<y)
min-tightˡ (suc x) (suc y) x<y i = suc $ min-tightˡ x y (suc-creates-< x y .snd x<y) i

min-tightʳ : ∀ x y → [ y < x ] → min x y ≡ y
min-tightʳ x y y<x = min-comm x y ∙ min-tightˡ y x y<x

min-identity : ∀ x → min x x ≡ x
min-identity zero = refl
min-identity (suc x) i = suc $ min-identity x i

max-comm : ∀ x y → max x y ≡ max y x
max-comm zero zero = refl
max-comm zero (suc y) = refl
max-comm (suc x) zero = refl
max-comm (suc x) (suc y) i = suc $ max-comm x y i

max-tightˡ : ∀ x y → [ y < x ] → max x y ≡ x
max-tightˡ zero zero y<x = refl
max-tightˡ zero (suc y) y<x = ⊥-elim {A = λ _ → suc y ≡ zero} (¬suc<0 y y<x)
max-tightˡ (suc x) zero y<x = refl
max-tightˡ (suc x) (suc y) y<x i = suc $ max-tightˡ x y (suc-creates-< y x .snd y<x) i

max-tightʳ : ∀ x y → [ x < y ] → max x y ≡ y
max-tightʳ x y x<y = max-comm x y ∙ max-tightˡ y x x<y

max-identity : ∀ x → max x x ≡ x
max-identity zero = refl
max-identity (suc x) i = suc $ max-identity x i

-- +-reflects-< : ∀ a b x → [ a + x < b + x ] → [ a < b ]
-- +-reflects-< a b x

-- suc-preserves-min : ∀ x y → suc (min x y) ≡ min (suc x) (suc y)
-- suc-preserves-min zero y = refl
-- suc-preserves-min (suc x) zero = refl
-- suc-preserves-min (suc x) (suc y) = refl
--
-- min-dichotomy : ∀ x y → (min x y ≡ x) ⊎ (min x y ≡ y)
-- min-dichotomy zero y = inl refl
-- min-dichotomy (suc x) zero = inr refl
-- min-dichotomy (suc x) (suc y) with min-dichotomy x y
-- ... | inl p = inl λ i → suc (p i)
-- ... | inr p = inr λ i → suc (p i)

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

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

abstract
  min-trichotomy : ∀ x y → MinTrichtotomy x y
  min-trichotomy zero zero = min-eq refl refl
  min-trichotomy zero (suc y) = min-lt refl (y , (+-comm y 1))
  min-trichotomy (suc x) zero = min-gt refl (x , (+-comm x 1))
  min-trichotomy (suc x) (suc y) with min-trichotomy x y
  ... | min-lt p (k , q) = min-lt (λ i → suc (p i)) (k , (+-assoc k 1 (suc x) ∙ (λ i → +-comm k 1 i + suc x) ∙ (λ i → 1 + q i)))
  ... | min-gt p (k , q) = min-gt (λ i → suc (p i)) (k , (+-assoc k 1 (suc y) ∙ (λ i → +-comm k 1 i + suc y) ∙ (λ i → 1 + q i)))
  ... | min-eq p q       = min-eq (λ i → suc (p i)) (λ i → suc (q i))

  max-trichotomy : ∀ x y → MaxTrichtotomy x y
  max-trichotomy zero zero = max-eq refl refl
  max-trichotomy zero (suc y) = max-lt refl (y , (+-comm y 1))
  max-trichotomy (suc x) zero = max-gt refl (x , (+-comm x 1))
  max-trichotomy (suc x) (suc y) with max-trichotomy x y
  ... | max-lt p (k , q) = max-lt (λ i → suc (p i)) (k , (+-assoc k 1 (suc x) ∙ (λ i → +-comm k 1 i + suc x) ∙ (λ i → 1 + q i)))
  ... | max-gt p (k , q) = max-gt (λ i → suc (p i)) (k , (+-assoc k 1 (suc y) ∙ (λ i → +-comm k 1 i + suc y) ∙ (λ i → 1 + q i)))
  ... | max-eq p q       = max-eq (λ i → suc (p i)) (λ i → suc (q i))

  is-min : (x y z : ℕ) → [ ¬ᵖ (min x y < z) ⇔ ¬ᵖ (x < z) ⊓ ¬ᵖ (y < z) ]
  is-min x y z .fst z≤minxy with min-trichotomy x y
  ... | min-lt p x<y = (λ x<z → z≤minxy $ pathTo⇐ (λ i → p i < z) x<z)
                     , (λ y<z → z≤minxy $ pathTo⇐ (λ i → p i < z) $ <-trans {x} {y} {z} x<y y<z)
  ... | min-gt p y<x = (λ x<z → z≤minxy $ pathTo⇐ (λ i → p i < z) $ <-trans {y} {x} {z} y<x x<z)
                     , (λ y<z → z≤minxy $ pathTo⇐ (λ i → p i < z) y<z)
  ... | min-eq p q   = (λ x<z → z≤minxy $ pathTo⇐ (λ i → p i < z) x<z)
                     , (λ y<z → z≤minxy $ pathTo⇐ (λ i → q i < z) y<z)
  is-min x y z .snd (z≤x , z≤y) minxy<z with min-trichotomy x y
  ... | min-lt p _   = z≤x $ pathTo⇒ (λ i → p i < z) minxy<z
  ... | min-gt p _   = z≤y $ pathTo⇒ (λ i → p i < z) minxy<z
  ... | min-eq p q   = z≤x $ pathTo⇒ (λ i → p i < z) minxy<z

  is-max : (x y z : ℕ) → [ ¬ᵖ (z < max x y) ⇔ ¬ᵖ (z < x) ⊓ ¬ᵖ (z < y) ]
  is-max x y z .fst maxxy≤z with max-trichotomy x y
  ... | max-gt p y<x = (λ z<x → maxxy≤z $ pathTo⇐ (λ i → z < p i) z<x )
                     , (λ z<y → maxxy≤z $ pathTo⇐ (λ i → z < p i) $ <-trans {z} {y} {x} z<y y<x )
  ... | max-lt p x<y = (λ z<x → maxxy≤z $ pathTo⇐ (λ i → z < p i) $ <-trans {z} {x} {y} z<x x<y )
                     , (λ z<y → maxxy≤z $ pathTo⇐ (λ i → z < p i) z<y )
  ... | max-eq p q   = (λ z<x → maxxy≤z $ pathTo⇐ (λ i → z < p i) z<x )
                     , (λ z<y → maxxy≤z $ pathTo⇐ (λ i → z < q i) z<y )
  is-max x y z .snd (z≤x , z≤y) maxxy<z with max-trichotomy x y
  ... | max-gt p _   = z≤x $ pathTo⇒ (λ i → z < p i) maxxy<z
  ... | max-lt p _   = z≤y $ pathTo⇒ (λ i → z < p i) maxxy<z
  ... | max-eq p q   = z≤x $ pathTo⇒ (λ i → z < p i) maxxy<z

abstract
  -- NOTE: maybe some clever use of cotrans makes this a bit shorter
  +-<-ext : (w x y z : ℕ) → [ (w + x) < (y + z) ] → [ (w < y) ⊔ (x < z) ]
  +-<-ext w x y z (k , k+suc[w+x]≡y+z) with w ≟ y | x ≟ z
  ... | lt w<y | q = ∣ inl w<y ∣
  ... | gt (l , l+suc[y]≡w) | q = inrᵖ (k + suc l , inj-m+ ((
    y + ((k + suc l) + suc x) ≡⟨ +-assoc y (k + suc l) (suc x) ⟩
    (y + (k + suc l)) + suc x ≡⟨ (λ i → +-assoc y k (suc l) i + suc x) ⟩
    ((y + k) + suc l) + suc x ≡⟨ (λ i → (+-comm y k i + suc l) + suc x) ⟩
    ((k + y) + suc l) + suc x ≡⟨ (λ i → +-assoc k y (suc l) (~ i) + suc x) ⟩
    (k + (y + suc l)) + suc x ≡⟨ sym $ +-assoc k (y + suc l) (suc x) ⟩
    k + ((y + suc l) + suc x) ≡⟨ (λ i → k + (+-suc y l i + suc x)) ⟩
    k + (suc (y + l) + suc x) ≡⟨ (λ i → k + (suc (+-comm y l i) + suc x)) ⟩
    k + (suc (l + y) + suc x) ≡⟨ (λ i → k + (+-suc l y (~ i) + suc x)) ⟩
    k + ((l + suc y) + suc x) ≡⟨ (λ i → k + +-suc (l + suc y) x i) ⟩
    k + suc ((l + suc y) + x) ≡⟨ (λ i → k + suc (l+suc[y]≡w i + x)) ⟩
    k + suc (w + x) ∎) ∙ k+suc[w+x]≡y+z))
  ... | eq w≡y | q = inrᵖ (k , inj-m+ ((
    y + (k + suc x) ≡⟨ +-assoc y k (suc x) ⟩
    (y + k) + suc x ≡⟨ (λ i → +-comm y k i + suc x) ⟩
    (k + y) + suc x ≡⟨ sym $ +-assoc k y (suc x) ⟩
    k + (y + suc x) ≡⟨ (λ i → k + +-suc y x i) ⟩
    k + suc (y + x) ≡⟨ (λ i → k + suc (w≡y (~ i) + x)) ⟩
    k + suc (w + x) ∎) ∙ k+suc[w+x]≡y+z))

  -- NOTE: instead of equational reasoning, this might follow more easily from induction on `z`?
  ·-preserves-< : (x y z : ℕ) → [ 0 < z ] → [ x < y ] → [ (x · z) < (y · z) ]
  ·-preserves-< x y z (k , k+1≡z) (l , l+suc[x]≡y) = l · z + k , (
    (l · z + k) + suc (x · z) ≡⟨ sym $ +-assoc (l · z) k (suc (x · z)) ⟩
    l · z + (k + suc (x · z)) ≡⟨ refl ⟩ -- 1 + x ≡ suc x holds definitionally
    l · z + (k + (1 + x · z)) ≡⟨ (λ i → l · z + +-assoc k 1 (x · z) i) ⟩
    l · z + ((k + 1) + x · z) ≡⟨ (λ i → l · z + (k+1≡z i + x · z)) ⟩
    l · z + (z + x · z)       ≡⟨ refl ⟩ -- suc x · z ≡ z + x · z holds definitionally
    l · z + (suc x) · z       ≡⟨ ·-distribʳ l (suc x) z ⟩
    (l + suc x) · z           ∎) ∙ (λ i → l+suc[x]≡y i · z) ∙ refl

  -- ·-reflects-< : (x y z : ℕ) → [ 0 < z ] → [ (x · z) < (y · z) ] → [ x < y ]
  -- ·-reflects-< x y zero (k , k+1≡z) _ = ⊥-elim {A = λ _ → [ x < y ]} $ snotz (sym (+-comm k 1) ∙ k+1≡z)
  -- ·-reflects-< x y (suc zero) _ (l , l+suc[xz]≡yz) = l , (λ i → l + suc (·-identityʳ x (~ i))) ∙ l+suc[xz]≡yz ∙ ·-identityʳ y
  -- ·-reflects-< x y (suc (suc z)) _ p@(l , l+suc[xz]≡yz) =
  --   let ind = {! ·-reflects-< x y (suc z) (0<suc z)   !}
  --     -- (x · suc (suc z)) < (y · suc (suc z))
  --     -- x + x · suc z < y + y · suc z
  --     -- (x + x · suc z) + < (y + y · suc z)
  --   in {! ·-suc x (suc z)  !}
  -- -- ·-reflects-< x y zero 0<z xz<yz = {!   !} -- ·-suc x z
  -- -- ·-reflects-< x y (suc z) 0<z xz<yz = {! ·-reflects-< x y z  !}
  -- --   (x · suc z) < (y · suc z)

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

·-Semigroup : [ isSemigroup _·_ ]
·-Semigroup .IsSemigroup.is-set   = isSetℕ
·-Semigroup .IsSemigroup.is-assoc = ·-assoc

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

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

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

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

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

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

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

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

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals