text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}

-- This module provides some scaffolding to define the handlers for our fake/simple "implementation"
-- and connect them to the interface of the SystemModel.

open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Util

open import LibraBFT.Impl.Properties.Aux  -- TODO-1: maybe Aux properties should be in this file?
open import LibraBFT.Concrete.System impl-sps-avp
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK
open        Structural impl-sps-avp

module LibraBFT.Impl.Handle.Properties
  (hash    : BitString → Hash)
  (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)
  where
  open import LibraBFT.Impl.Consensus.ChainedBFT.EventProcessor hash hash-cr
  open import LibraBFT.Impl.Handle hash hash-cr

  ----- Properties that bridge the system model gap to the handler -----
  msgsToSendWereSent1 : ∀ {pid ts pm vm} {st : EventProcessor}
                      → send (V vm) ∈ proj₂ (peerStep pid (P pm) ts st)
                      → ∃[ αs ] (SendVote vm αs ∈ LBFT-outs (handle pid (P pm) ts) st)
  msgsToSendWereSent1 {pid} {ts} {pm} {vm} {st} send∈acts
     with send∈acts
     -- The fake handler sends only to node 0 (fakeAuthor), so this doesn't
     -- need to be very general yet.
     -- TODO-1: generalize this proof so it will work when the set of recipients is
     -- not hard coded.

     -- The system model allows any message sent to be received by any peer (so the list of
     -- recipients it essentially ignored), meaning that our safety proofs will be for a slightly
     -- stronger model.  Progress proofs will require knowledge of recipients, though, so we will
     -- keep the implementation model faithful to the implementation.
  ...| here refl = fakeAuthor ∷ [] , here refl

  msgsToSendWereSent : ∀ {pid ts nm m} {st : EventProcessor}
                     → m ∈ proj₂ (peerStepWrapper pid nm st)
                     → ∃[ vm ] (m ≡ V vm × send (V vm) ∈ proj₂ (peerStep pid nm ts st))
  msgsToSendWereSent {pid} {nm = nm} {m} {st} m∈outs
    with nm
  ...| C _ = ⊥-elim (¬Any[] m∈outs)
  ...| V _ = ⊥-elim (¬Any[] m∈outs)
  ...| P pm
     with m∈outs
  ...| here v∈outs
       with m
  ...| P _ = ⊥-elim (P≢V v∈outs)
  ...| C _ = ⊥-elim (C≢V v∈outs)
  ...| V vm rewrite sym v∈outs = vm , refl , here refl

  ----- Properties that relate handler to system state -----

  postulate -- TODO-2: this will be proved for the implementation, confirming that honest
            -- participants only store QCs comprising votes that have actually been sent.
   -- Votes stored in highesQuorumCert and highestCommitCert were sent before.
   -- Note that some implementations might not ensure this, but LibraBFT does
   -- because even the leader of the next round sends its own vote to itself,
   -- as opposed to using it to construct a QC using its own unsent vote.
   qcVotesSentB4 : ∀{e pid ps vs pk q vm}{st : SystemState e}
                 → ReachableSystemState st
                 → initialised st pid ≡ initd
                 → ps ≡ peerStates st pid
                 → q QC∈VoteMsg vm
                 → vm ^∙ vmSyncInfo ≡ mkSyncInfo (ps ^∙ epHighestQC) (ps ^∙ epHighestCommitQC)
                 → vs ∈ qcVotes q
                 → MsgWithSig∈ pk (proj₂ vs) (msgPool st)

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module utm where

open import turing
open import Data.Product
-- open import Data.Bool
open import Data.List
open import Data.Nat
open import logic

data utmStates : Set where
     reads : utmStates
     read0 : utmStates
     read1 : utmStates
     read2 : utmStates
     read3 : utmStates
     read4 : utmStates
     read5 : utmStates
     read6 : utmStates

     loc0 : utmStates
     loc1 : utmStates
     loc2 : utmStates
     loc3 : utmStates
     loc4 : utmStates
     loc5 : utmStates
     loc6 : utmStates

     fetch0 : utmStates
     fetch1 : utmStates
     fetch2 : utmStates
     fetch3 : utmStates
     fetch4 : utmStates
     fetch5 : utmStates
     fetch6 : utmStates
     fetch7 : utmStates

     print0 : utmStates
     print1 : utmStates
     print2 : utmStates
     print3 : utmStates
     print4 : utmStates
     print5 : utmStates
     print6 : utmStates
     print7 : utmStates

     mov0 : utmStates
     mov1 : utmStates
     mov2 : utmStates
     mov3 : utmStates
     mov4 : utmStates
     mov5 : utmStates
     mov6 : utmStates

     tidy0 : utmStates
     tidy1 : utmStates
     halt : utmStates

data utmΣ : Set where
    ０ : utmΣ
    １ : utmΣ
    B : utmΣ
    * : utmΣ
    $ : utmΣ
    ^ : utmΣ
    X : utmΣ
    Y : utmΣ
    Z : utmΣ
    ＠ : utmΣ
    b : utmΣ

utmδ :  utmStates →  utmΣ  → utmStates × (Write utmΣ) × Move
utmδ reads  x = read0 , wnone , mnone
utmδ read0  * = read1 , write * , left
utmδ read0  x = read0 , write x , right
utmδ read1  x = read2 , write ＠ , right
utmδ read2  ^ = read3 , write ^ , right
utmδ read2  x = read2 , write x , right
utmδ read3  ０ = read4 , write ０ , left
utmδ read3  １ = read5 , write １ , left
utmδ read3  b = read6 , write b , left
utmδ read4  ＠ = loc0 , write ０ , right
utmδ read4  x = read4 , write x , left
utmδ read5  ＠ = loc0 , write １ , right
utmδ read5  x = read5 , write x , left
utmδ read6  ＠ = loc0 , write B , right
utmδ read6  x = read6 , write x , left
utmδ loc0  ０ = loc0 , write X , left
utmδ loc0  １ = loc0 , write Y , left
utmδ loc0  B = loc0 , write Z , left
utmδ loc0  $ = loc1 , write $ , right
utmδ loc0  x = loc0 , write x , left
utmδ loc1  X = loc2 , write ０ , right
utmδ loc1  Y = loc3 , write １ , right
utmδ loc1  Z = loc4 , write B , right
utmδ loc1  * = fetch0 , write * , right
utmδ loc1  x = loc1 , write x , right
utmδ loc2  ０ = loc5 , write X , right
utmδ loc2  １ = loc6 , write Y , right
utmδ loc2  B = loc6 , write Z , right
utmδ loc2  x = loc2 , write x , right
utmδ loc3  １ = loc5 , write Y , right
utmδ loc3  ０ = loc6 , write X , right
utmδ loc3  B = loc6 , write Z , right
utmδ loc3  x = loc3 , write x , right
utmδ loc4  B = loc5 , write Z , right
utmδ loc4  ０ = loc6 , write X , right
utmδ loc4  １ = loc6 , write Y , right
utmδ loc4  x = loc4 , write x , right
utmδ loc5  $ = loc1 , write $ , right
utmδ loc5  x = loc5 , write x , left
utmδ loc6  $ = halt , write $ , right
utmδ loc6  * = loc0 , write * , left
utmδ loc6  x = loc6 , write x , right
utmδ fetch0  ０ = fetch1 , write X , left
utmδ fetch0  １ = fetch2 , write Y , left
utmδ fetch0  B = fetch3 , write Z , left
utmδ fetch0  x = fetch0 , write x , right
utmδ fetch1  $ = fetch4 , write $ , right
utmδ fetch1  x = fetch1 , write x , left
utmδ fetch2  $ = fetch5 , write $ , right
utmδ fetch2  x = fetch2 , write x , left
utmδ fetch3  $ = fetch6 , write $ , right
utmδ fetch3  x = fetch3 , write x , left
utmδ fetch4  ０ = fetch7 , write X , right
utmδ fetch4  １ = fetch7 , write X , right
utmδ fetch4  B = fetch7 , write X , right
utmδ fetch4  * = print0 , write * , left
utmδ fetch4  x = fetch4 , write x , right
utmδ fetch5  ０ = fetch7 , write Y , right
utmδ fetch5  １ = fetch7 , write Y , right
utmδ fetch5  B = fetch7 , write Y , right
utmδ fetch5  * = print0 , write * , left
utmδ fetch5  x = fetch5 , write x , right
utmδ fetch6  ０ = fetch7 , write Z , right
utmδ fetch6  １ = fetch7 , write Z , right
utmδ fetch6  B = fetch7 , write Z , right
utmδ fetch6  * = print0 , write * , left
utmδ fetch6  x = fetch6 , write x , right
utmδ fetch7  * = fetch0 , write * , right
utmδ fetch7  x = fetch7 , write x , right
utmδ print0  X = print1 , write X , right
utmδ print0  Y = print2 , write Y , right
utmδ print0  Z = print3 , write Z , right
utmδ print1  ^ = print4 , write ^ , right
utmδ print1  x = print1 , write x , right
utmδ print2  ^ = print5 , write ^ , right
utmδ print2  x = print2 , write x , right
utmδ print3  ^ = print6 , write ^ , right
utmδ print3  x = print3 , write x , right
utmδ print4  x = print7 , write ０ , left
utmδ print5  x = print7 , write １ , left
utmδ print6  x = print7 , write B , left
utmδ print7  X = mov0 , write X , right
utmδ print7  Y = mov1 , write Y , right
utmδ print7  x = print7 , write x , left
utmδ mov0  ^ = mov2 , write ^ , left
utmδ mov0  x = mov0 , write x , right
utmδ mov1  ^ = mov3 , write ^ , right
utmδ mov1  x = mov1 , write x , right
utmδ mov2  ０ = mov4 , write ^ , right
utmδ mov2  １ = mov5 , write ^ , right
utmδ mov2  B = mov6 , write ^ , right
utmδ mov3  ０ = mov4 , write ^ , left
utmδ mov3  １ = mov5 , write ^ , left
utmδ mov3  B = mov6 , write ^ , left
utmδ mov4  ^ = tidy0 , write ０ , left
utmδ mov5  ^ = tidy0 , write １ , left
utmδ mov6  ^ = tidy0 , write B , left
utmδ tidy0  $ = tidy1 , write $ , left
utmδ tidy0  x = tidy0 , write x , left
utmδ tidy1  X = tidy1 , write ０ , left
utmδ tidy1  Y = tidy1 , write １ , left
utmδ tidy1  Z = tidy1 , write B , left
utmδ tidy1  $ = reads , write $ , right
utmδ tidy1  x = tidy1 , write x , left
utmδ _  x = halt , write x , mnone

U-TM : Turing utmStates utmΣ
U-TM = record {
        tδ = utmδ
     ;  tstart = read0
     ;  tend = tend
     ;  tnone =  b
  } where
      tend : utmStates →  Bool
      tend halt = true
      tend _ = false

-- Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move
-- Copyδ s1 0  = H    , wnone       , mnone
-- Copyδ s1 1  = s2   , write 0 , right
-- Copyδ s2 0  = s3   , write 0 , right
-- Copyδ s2 1  = s2   , write 1 , right
-- Copyδ s3 0  = s4   , write 1 , left
-- Copyδ s3 1  = s3   , write 1 , right
-- Copyδ s4 0  = s5   , write 0 , left
-- Copyδ s4 1  = s4   , write 1 , left
-- Copyδ s5 0  = s1   , write 1 , right
-- Copyδ s5 1  = s5   , write 1 , left
-- Copyδ H  _  = H    , wnone   , mnone
-- Copyδ _  (suc (suc _))      = H    , wnone       , mnone

Copyδ-encode : List utmΣ
Copyδ-encode =
       ０  ∷ ０  ∷ １  ∷ ０  ∷  １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷   -- s1 0  = H    , wnone       , mnone
  *  ∷ ０  ∷ ０  ∷ １  ∷ １  ∷  ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷   -- s1 1  = s2   , write 0 , right
  *  ∷ ０  ∷ １  ∷ ０  ∷ ０  ∷  ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷   -- s2 0  = s3   , write 0 , right
  *  ∷ ０  ∷ １  ∷ ０  ∷ １  ∷  ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷   -- s2 1  = s2   , write 1 , right
  *  ∷ ０  ∷ １  ∷ １  ∷ ０  ∷  １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷   -- s3 0  = s4   , write 1 , left
  *  ∷ ０  ∷ １  ∷ １  ∷ １  ∷  ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷   -- s3 1  = s3   , write 1 , right
  *  ∷ １  ∷ ０  ∷ ０  ∷ ０  ∷  １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷   -- s4 0  = s5   , write 0 , left
  *  ∷ １  ∷ ０  ∷ ０  ∷ １  ∷  １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷   -- s4 1  = s4   , write 1 , left
  *  ∷ １  ∷ ０  ∷ １  ∷ ０  ∷  ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷   -- s5 0  = s1   , write 1 , right
  *  ∷ １  ∷ ０  ∷ １  ∷ １  ∷  １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷   -- s5 1  = s5   , write 1 , left
  []

input-encode : List utmΣ
input-encode =  １  ∷ １  ∷ ０  ∷ ０  ∷  ０ ∷ []

input+Copyδ : List utmΣ
input+Copyδ = ( $  ∷ ０  ∷ ０  ∷  ０ ∷  ０ ∷  * ∷  [] ) -- start state
        ++   Copyδ-encode
        ++ ( $ ∷ ^ ∷ input-encode )

short-input : List utmΣ
short-input = $  ∷ ０  ∷ ０  ∷  ０ ∷  * ∷
    ０  ∷ ０  ∷  ０ ∷  １  ∷ ０  ∷ １ ∷ １  ∷  * ∷
    ０  ∷ ０  ∷  １ ∷  ０  ∷ １  ∷ １ ∷ １  ∷  * ∷
    ０  ∷ １  ∷  B  ∷  １ ∷  ０  ∷ １ ∷ ０  ∷  * ∷
    １  ∷ ０  ∷  ０ ∷  ０ ∷  １  ∷ １ ∷ １  ∷  $ ∷
    ^   ∷ ０  ∷  ０ ∷  １  ∷ １ ∷ []

utm-test1 : List  utmΣ → utmStates × ( List  utmΣ ) × ( List  utmΣ )
utm-test1 inp = Turing.taccept U-TM  inp

{-# TERMINATING #-}
utm-test2 : ℕ  → List  utmΣ  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
utm-test2 n inp  = loop n (Turing.tstart U-TM) inp []
  where
        loop :  ℕ → utmStates → ( List  utmΣ ) → ( List  utmΣ ) → utmStates × ( List  utmΣ ) × ( List  utmΣ )
        loop zero q L R = ( q , L , R )
        loop (suc n) q L R with  move {utmStates} {utmΣ} {０} {utmδ} q L R | q
        ... | nq , nL , nR | reads = loop n nq nL nR
        ... | nq , nL , nR | _ = loop (suc n) nq nL nR

t1 = utm-test2 20 short-input

t : (n : ℕ)  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
-- t n = utm-test2 n input+Copyδ
t n = utm-test2 n short-input

ext: agda

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.TypeQuotients where

open import Cubical.HITs.TypeQuotients.Base public
open import Cubical.HITs.TypeQuotients.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

data _≤_ : ℕ → ℕ → Set where
  zero : ∀ {n}                → zero  ≤ n
  suc  : ∀ {m n} (le : m ≤ n) → suc m ≤ suc n

_<_ : ℕ → ℕ → Set
m < n = suc m ≤ n

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero    = zero
toℕ (suc i) = suc (toℕ i)

fromℕ≤ : ∀ {m n} → m < n → Fin n
fromℕ≤ (suc zero)       = zero
fromℕ≤ (suc (suc m≤n)) = suc (fromℕ≤ (suc m≤n))

-- If we treat constructors as inert this fails to solve. Not entirely sure why.
fromℕ≤-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i < m) → fromℕ≤ i<m ≡ i
fromℕ≤-toℕ zero    (suc zero)       = refl
fromℕ≤-toℕ (suc i) (suc (suc m≤n)) = cong suc (fromℕ≤-toℕ i (suc m≤n))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --no-positivity-check #-}
module IIRDg where

import LF
import DefinitionalEquality
import IIRD

open LF
open DefinitionalEquality
open IIRD

mutual

  data Ug {I : Set}{D : I -> Set1}(γ : OPg I D) : I -> Set where
    introg : (a : Gu γ (Ug γ) (Tg γ)) -> Ug γ (Gi γ (Ug γ) (Tg γ) a)

  Tg : {I : Set}{D : I -> Set1}(γ : OPg I D)(i : I) -> Ug γ i -> D i
  Tg γ .(Gi γ (Ug γ) (Tg γ) a) (introg a) = Gt γ (Ug γ) (Tg γ) a

Arg : {I : Set}{D : I -> Set1}(γ : OPg I D) -> Set
Arg γ = Gu γ (Ug γ) (Tg γ)

index : {I : Set}{D : I -> Set1}(γ : OPg I D) -> Arg γ -> I
index γ a = Gi γ (Ug γ) (Tg γ) a

IH : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1) -> Arg γ -> Set1
IH γ = KIH γ (Ug γ) (Tg γ)

-- Elimination rule
Rg : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1) ->
     (h : (a : Arg γ) -> IH γ F a -> F (index γ a) (introg a)) ->
     (i : I)(u : Ug γ i) -> F i u
Rg γ F h .(index γ a) (introg a) = h a (Kmap γ (Ug γ) (Tg γ) F (Rg γ F h) a)

{-
-- We don't have general IIRDs so we have to postulate Ug/Tg

postulate
  Ug : {I : Set}{D : I -> Set1} -> OPg I D -> I -> Set
  Tg : {I : Set}{D : I -> Set1}(γ : OPg I D)(i : I) -> Ug γ i -> D i

  introg : {I : Set}{D : I -> Set1}(γ : OPg I D)(a : Gu γ (Ug γ) (Tg γ)) ->
           Ug γ (Gi γ (Ug γ) (Tg γ) a)

  Tg-equality : {I : Set}{D : I -> Set1}(γ : OPg I D)(a : Gu γ (Ug γ) (Tg γ)) ->
                Tg γ (Gi γ (Ug γ) (Tg γ) a) (introg γ a) ≡₁ Gt γ (Ug γ) (Tg γ) a

  Rg : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1)
       (h : (a : Gu γ (Ug γ) (Tg γ)) -> KIH γ (Ug γ) (Tg γ) F a -> F (Gi γ (Ug γ) (Tg γ) a) (introg γ a))
       (i : I)(u : Ug γ i) -> F i u

  Rg-equality : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1)
                (h : (a : Gu γ (Ug γ) (Tg γ)) -> KIH γ (Ug γ) (Tg γ) F a -> F (Gi γ (Ug γ) (Tg γ) a) (introg γ a))
                (a : Gu γ (Ug γ) (Tg γ)) ->
                Rg γ F h (Gi γ (Ug γ) (Tg γ) a) (introg γ a)
                ≡₁ h a (Kmap γ (Ug γ) (Tg γ) F (Rg γ F h) a)

-- Helpers

ι★g : {I : Set}(i : I) -> OPg I (\_ -> One')
ι★g i = ι < i | ★' >'

-- Examples

module Martin-Löf-Identity where

  IdOP : {A : Set} -> OPg (A * A) (\_ -> One')
  IdOP {A} = σ A \a -> ι★g < a | a >

  _==_ : {A : Set}(x y : A) -> Set
  x == y = Ug IdOP < x | y >

  refl : {A : Set}(x : A) -> x == x
  refl x = introg IdOP < x | ★ >

  -- We have to work slightly harder than desired since we don't have η for × and One.
  private
    -- F C is just uncurry C but dependent and at high universes.
    F : {A : Set}(C : (x y : A) -> x == y -> Set1)(i : A * A) -> Ug IdOP i -> Set1
    F C < x | y > p = C x y p

    h' : {A : Set}(C : (x y : A) -> x == y -> Set1)
         (h : (x : A) -> C x x (refl x))
         (a : Gu IdOP (Ug IdOP) (Tg IdOP)) -> KIH IdOP (Ug IdOP) (Tg IdOP) (F C) a ->
         F C (Gi IdOP (Ug IdOP) (Tg IdOP) a) (introg IdOP a)
    h' C h < x | ★ > _ = h x

  J : {A : Set}(C : (x y : A) -> x == y -> Set1)
      (h : (x : A) -> C x x (refl x))
      (x y : A)(p : x == y) -> C x y p
  J {A} C h x y p = Rg IdOP (F C) (h' C h) < x | y > p

  J-equality : {A : Set}(C : (x y : A) -> x == y -> Set1)
               (h : (x : A) -> C x x (refl x))(x : A) ->
               J C h x x (refl x) ≡₁ h x
  J-equality {A} C h x = Rg-equality IdOP (F C) (h' C h) < x | ★ >

module Christine-Identity where

  IdOP : {A : Set}(a : A) -> OPg A (\_ -> One')
  IdOP {A} a = ι★g a

  _==_ : {A : Set}(x y : A) -> Set
  x == y = Ug (IdOP x) y

  refl : {A : Set}(x : A) -> x == x
  refl x = introg (IdOP x) ★

  private
    h' : {A : Set}(x : A)(C : (y : A) -> x == y -> Set1)
         (h : C x (refl x))(a : Gu (IdOP x) (Ug (IdOP x)) (Tg (IdOP x))) ->
         KIH (IdOP x) (Ug (IdOP x)) (Tg (IdOP x)) C a ->
         C (Gi (IdOP x) (Ug (IdOP x)) (Tg (IdOP x)) a) (introg (IdOP x) a)
    h' x C h ★ _ = h

  H : {A : Set}(x : A)(C : (y : A) -> x == y -> Set1)
      (h : C x (refl x))
      (y : A)(p : x == y) -> C y p
  H x C h y p = Rg (IdOP x) C (h' x C h) y p

  H-equality : {A : Set}(x : A)(C : (y : A) -> x == y -> Set1)
               (h : C x (refl x)) ->
               H x C h x (refl x) ≡₁ h
  H-equality x C h = Rg-equality (IdOP x) C (h' x C h) ★

open Christine-Identity
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Oscar.Category.Setoid where

open import Oscar.Builtin.Objectevel
open import Oscar.Property

record IsSetoid {𝔬} {𝔒 : Ø 𝔬} {𝔮} (_≋_ : 𝑴 1 𝔒 𝔮) : Ø 𝔬 ∙̂ 𝔮 where
  field
    reflexivity : ∀ x → x ≋ x
    symmetry : ∀ {x y} → x ≋ y → y ≋ x
    transitivity : ∀ {x y} → x ≋ y → ∀ {z} → y ≋ z → x ≋ z

open IsSetoid ⦃ … ⦄ public

record Setoid 𝔬 𝔮 : Ø ↑̂ (𝔬 ∙̂ 𝔮) where
  constructor ↑_
  infix 4 _≋_
  field
    {⋆} : Set 𝔬
    _≋_ : ⋆ → ⋆ → Set 𝔮
    ⦃ isSetoid ⦄ : IsSetoid _≋_
  open IsSetoid isSetoid public


text:
module _ where

data Flat (A : Set) : Set where
  flat : @♭ A → Flat A

-- the lambda cohesion annotation must match the domain.
into : {A : Set} → A → Flat A
into = λ (@♭ a) → flat a


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

module Data.String where

open import Agda.Builtin.String using (String) public
open import Agda.Builtin.String
open import Agda.Builtin.String.Properties
open import Agda.Builtin.Char using (Char) public
open import Agda.Builtin.Char
open import Agda.Builtin.Char.Properties
open import Relation.Binary
open import Relation.Binary.Construct.On
import Data.Nat.Order as ℕ
open import Function.Injective
open import Function
open import Path
open import Data.List
open import Data.List.Relation.Binary.Lexicographic

unpack : String → List Char
unpack = primStringToList

pack : List Char → String
pack = primStringFromList

charOrd : TotalOrder Char _ _
charOrd = on-ord primCharToNat lemma ℕ.totalOrder
  where
  lemma : Injective primCharToNat
  lemma x y p = builtin-eq-to-path (primCharToNatInjective x y (path-to-builtin-eq p ))

listCharOrd : TotalOrder (List Char) _ _
listCharOrd = listOrd charOrd

stringOrd : TotalOrder String _ _
stringOrd = on-ord primStringToList lemma listCharOrd
  where
  lemma : Injective primStringToList
  lemma x y p = builtin-eq-to-path (primStringToListInjective x y (path-to-builtin-eq p))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Example usage of solver

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

open import Categories.Category

module Experiment.Categories.Solver.Category.Example
  {o ℓ e} (𝒞 : Category o ℓ e) where

open import Experiment.Categories.Solver.Category 𝒞

open Category 𝒞
open HomReasoning

private
  variable
    A B C D E : Obj

module _ (f : D ⇒ E) (g : C ⇒ D) (h : B ⇒ C) (i : A ⇒ B) where
  _ : (f ∘ id ∘ g) ∘ id ∘ h ∘ i ≈ f ∘ (g ∘ h) ∘ i
  _ = solve ((∥-∥ :∘ :id :∘ ∥-∥) :∘ :id :∘ ∥-∥ :∘ ∥-∥)
            (∥-∥ :∘ (∥-∥ :∘ ∥-∥) :∘ ∥-∥)
            refl


text:
----------------------------------------------------------------
-- This file contains the definition of isomorphisms.         --
----------------------------------------------------------------
module Category.Iso where

open import Category.Category

record Iso {l : Level}{ℂ : Cat {l}}{A B : Obj ℂ} (f : el (Hom ℂ A B)) : Set l where
  field
    inv : el (Hom ℂ B A)

    left-inv-ax  : ⟨ Hom ℂ A A ⟩[ f ○[ comp ℂ ] inv ≡ id ℂ ]
    right-inv-ax : ⟨ Hom ℂ B B ⟩[ inv ○[ comp ℂ ] f ≡ id ℂ ]

open Iso public

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Cowriter type and some operations
------------------------------------------------------------------------

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

module Codata.Cowriter where

open import Size
import Level as L
open import Codata.Thunk using (Thunk; force)
open import Codata.Conat
open import Codata.Delay using (Delay; later; now)
open import Codata.Stream as Stream using (Stream; _∷_)

open import Data.Unit
open import Data.List using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
open import Data.Nat.Base as Nat using (ℕ; zero; suc)
open import Data.Product as Prod using (_×_; _,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec using (Vec; []; _∷_)
open import Data.BoundedVec as BVec using (BoundedVec)
open import Function

data Cowriter {w a} (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where
  [_] : A → Cowriter W A i
  _∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i

------------------------------------------------------------------------
-- Relationship to Delay.

module _ {a} {A : Set a} where

  fromDelay : ∀ {i} → Delay A i → Cowriter ⊤ A i
  fromDelay (now a)    = [ a ]
  fromDelay (later da) = _ ∷ λ where .force → fromDelay (da .force)

module _ {w a} {W : Set w} {A : Set a} where

  toDelay : ∀ {i} → Cowriter W A i → Delay A i
  toDelay [ a ]    = now a
  toDelay (_ ∷ ca) = later λ where .force → toDelay (ca .force)

------------------------------------------------------------------------
-- Basic functions.

  fromStream : ∀ {i} → Stream W i → Cowriter W A i
  fromStream (w ∷ ws) = w ∷ λ where .force → fromStream (ws .force)

  repeat : W → Cowriter W A ∞
  repeat = fromStream ∘′ Stream.repeat

  length : ∀ {i} → Cowriter W A i → Conat i
  length [ _ ]    = zero
  length (w ∷ cw) = suc λ where .force → length (cw .force)

  splitAt : ∀ (n : ℕ) → Cowriter W A ∞ → (Vec W n × Cowriter W A ∞) ⊎ (BoundedVec W n × A)
  splitAt zero    cw       = inj₁ ([] , cw)
  splitAt (suc n) [ a ]    = inj₂ (BVec.[] , a)
  splitAt (suc n) (w ∷ cw) = Sum.map (Prod.map₁ (w ∷_)) (Prod.map₁ (w BVec.∷_))
                           $ splitAt n (cw .force)

  take : ∀ (n : ℕ) → Cowriter W A ∞ → Vec W n ⊎ (BoundedVec W n × A)
  take n = Sum.map₁ Prod.proj₁ ∘′ splitAt n

  infixr 5 _++_ _⁺++_
  _++_ : ∀ {i} → List W → Cowriter W A i → Cowriter W A i
  []       ++ ca = ca
  (w ∷ ws) ++ ca = w ∷ λ where .force → ws ++ ca

  _⁺++_ : ∀ {i} → List⁺ W → Thunk (Cowriter W A) i → Cowriter W A i
  (w ∷ ws) ⁺++ ca = w ∷ λ where .force → ws ++ ca .force

  concat : ∀ {i} → Cowriter (List⁺ W) A i → Cowriter W A i
  concat [ a ]    = [ a ]
  concat (w ∷ ca) = w ⁺++ λ where .force → concat (ca .force)

module _ {w x a b} {W : Set w} {X : Set x} {A : Set a} {B : Set b} where

------------------------------------------------------------------------
-- Functor, Applicative and Monad

  map : ∀ {i} → (W → X) → (A → B) → Cowriter W A i → Cowriter X B i
  map f g [ a ]    = [ g a ]
  map f g (w ∷ cw) = f w ∷ λ where .force → map f g (cw .force)

module _ {w a r} {W : Set w} {A : Set a} {R : Set r} where

  map₁ : ∀ {i} → (W → R) → Cowriter W A i → Cowriter R A i
  map₁ f = map f id

  map₂ : ∀ {i} → (A → R) → Cowriter W A i → Cowriter W R i
  map₂ = map id

  ap : ∀ {i} → Cowriter W (A → R) i → Cowriter W A i → Cowriter W R i
  ap [ f ]    ca = map₂ f ca
  ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca

  _>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W R i) → Cowriter W R i
  [ a ]    >>= f = f a
  (w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f

------------------------------------------------------------------------
-- Construction.

module _ {w s a} {W : Set w} {S : Set s} {A : Set a} where

  unfold : ∀ {i} → (S → (W × S) ⊎ A) → S → Cowriter W A i
  unfold next seed with next seed
  ... | inj₁ (w , seed') = w ∷ λ where .force → unfold next seed'
  ... | inj₂ a           = [ a ]


text:
module Dave.Algebra.Naturals.Bin where
  open import Dave.Algebra.Naturals.Definition
  open import Dave.Algebra.Naturals.Addition
  open import Dave.Algebra.Naturals.Multiplication
  open import Dave.Embedding

  data Bin : Set where
    ⟨⟩ : Bin
    _t : Bin → Bin
    _f : Bin → Bin

  inc : Bin → Bin
  inc ⟨⟩ = ⟨⟩ t
  inc (b t) = (inc b) f
  inc (b f) = b t

  to : ℕ → Bin
  to zero = ⟨⟩ f
  to (suc n) = inc (to n)

  from : Bin → ℕ
  from ⟨⟩ = zero
  from (b t) = 1 + 2  * (from b)
  from (b f) = 2 * (from b)

  from6 = from (⟨⟩ t t f)
  from23 = from (⟨⟩ t f t t t)
  from23WithZeros = from (⟨⟩ f f f t f t t t)

  Bin-ℕ-Suc-Homomorph : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
  Bin-ℕ-Suc-Homomorph ⟨⟩ = refl
  Bin-ℕ-Suc-Homomorph (b t) = begin
    from (inc (b t)) ≡⟨⟩
    from ((inc b) f) ≡⟨⟩
    2 * (from (inc b)) ≡⟨ cong (λ a → 2 * a) (Bin-ℕ-Suc-Homomorph b) ⟩
    2 * suc (from b) ≡⟨⟩
    2 * (1 + (from b)) ≡⟨ *-distrib1ₗ-+ₗ 2 (from b) ⟩
    2 + 2 * (from b) ≡⟨⟩
    suc (1 + 2 * (from b)) ≡⟨⟩
    suc (from (b t)) ∎
  Bin-ℕ-Suc-Homomorph (b f) = begin
    from (inc (b f)) ≡⟨⟩
    from (b t) ≡⟨⟩
    1 + 2 * (from b) ≡⟨⟩
    suc (2 * from b) ≡⟨⟩
    suc (from (b f)) ∎

  to-inverse-from : ∀ (n : ℕ) → from (to n) ≡ n
  to-inverse-from zero = refl
  to-inverse-from (suc n) = begin
    from (to (suc n)) ≡⟨⟩
    from (inc (to n)) ≡⟨ Bin-ℕ-Suc-Homomorph (to n) ⟩
    suc (from (to n)) ≡⟨ cong (λ a → suc a) (to-inverse-from n) ⟩
    suc n ∎

  ℕ≲Bin : ℕ ≲ Bin
  ℕ≲Bin = record
    {
      to = to;
      from = from;
      from∘to = to-inverse-from
    }


text:
open import ExtractSac as ES using ()
open import Extract (ES.kompile-fun)

open import Data.Nat as N using (ℕ; zero; suc; _≤_; _≥_; _<_; _>_; s≤s; z≤n; _∸_)
import      Data.Nat.DivMod as N
open import Data.Nat.Properties as N
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
import      Data.Vec.Properties as V
open import Data.Fin as F using (Fin; zero; suc; #_)
import      Data.Fin.Properties as F
open import Data.Product as Prod using (Σ; _,_; curry; uncurry) renaming (_×_ to _×ₜ_)
open import Data.String

open import Relation.Binary.PropositionalEquality

open import Structures
open import Function

open import Array.Base
open import Array.Properties

open import APL2
open import Agda.Builtin.Float

open import Reflection
open import ReflHelper

pattern I0 = (zero ∷ [])
pattern I1 = (suc zero ∷ [])
pattern I2 = (suc (suc zero) ∷ [])
pattern I3 = (suc (suc (suc zero)) ∷ [])

-- backin←{(d w in)←⍵⋄⊃+/,w{(⍴in)↑(-⍵+⍴d)↑⍺×d}¨⍳⍴w}
backin : ∀ {n s s₁} → (inp : Ar Float n s)
                     → (w : Ar Float n s₁)
                     → {≥ : ▴ s ≥a ▴ s₁}
                     → (d : Ar Float n $ ▾ ((s - s₁){≥} + 1))
                     → Ar Float n s
backin {n}{s}{s₁} inp w d = let
      ixs = ι ρ w
      use-ixs i,pf = let
        i , pf = i,pf
        iv = a→ix i (ρ w) pf
        wᵢ = sel w (subst-ix (λ i → V.lookup∘tabulate _ i) iv)
        --x = pre-pad i 0.0 (d ×ᵣ wᵢ)
        x = (i + ρ d) -↑⟨ 0.0 ⟩ (d ×ᵣ wᵢ)
        y = (ρ inp) ↑⟨ 0.0 ⟩ x
        in y
      s = reduce-1d _+ᵣ_ (cst 0.0) (, use-ixs ̈ ixs)
  in subst-ar (λ i → V.lookup∘tabulate _ i) s

kbin = kompile backin (quote _≥a_ ∷ quote reduce-1d ∷ quote _↑⟨_⟩_ ∷ quote _-↑⟨_⟩_ ∷ quote a→ix ∷ []) []
rkbin = frefl backin (quote _≥a_ ∷ quote reduce-1d ∷ quote _↑⟨_⟩_ ∷ quote _-↑⟨_⟩_ ∷ quote a→ix ∷ [])

fin-id : ∀ {n} → Fin n → Fin n
fin-id x = x

s-w+1≤s : ∀ {s w} → s ≥ w → s > 0 → w > 0 → s N.∸ w N.+ 1 ≤ s
s-w+1≤s {suc s} {suc w} (s≤s s≥w) s>0 w>0 rewrite (+-comm (s ∸ w) 1) = s≤s (m∸n≤m s w)
helper : ∀ {n} {sI sw : Vec ℕ n}
       → s→a sI ≥a s→a sw
       → (cst 0) <a s→a sI
       → (cst 0) <a s→a sw
       → (iv : Ix 1 (n ∷ []))
       → V.lookup sI (ix-lookup iv zero) ≥
         V.lookup (V.tabulate (λ i → V.lookup sI i ∸ V.lookup sw i N.+ 1))
         (ix-lookup iv zero)
helper {sI = sI} {sw} sI≥sw sI>0 sw>0 (x ∷ [])
       rewrite (V.lookup∘tabulate (λ i → V.lookup sI i ∸ V.lookup sw i N.+ 1) x) =
       s-w+1≤s (sI≥sw (x ∷ [])) (sI>0 (x ∷ [])) (sw>0 (x ∷ []))

a≤b⇒b≡c⇒a≤c : ∀ {a b c} → a ≤ b → b ≡ c → a ≤ c
a≤b⇒b≡c⇒a≤c a≤b refl = a≤b
-- sI - (sI - sw + 1) + 1 = sw
shape-same : ∀ {n} {sI sw : Vec ℕ n}
           → s→a sI ≥a s→a sw
           → (cst 0) <a s→a sI
           → (cst 0) <a s→a sw
           → (i : Fin n)
           → V.lookup
             (V.tabulate
              (λ i₁ →
                 V.lookup sI i₁ ∸
                 V.lookup (V.tabulate (λ i₂ → V.lookup sI i₂ ∸ V.lookup sw i₂ N.+ 1)) i₁
                 N.+ 1))
             i
             ≡ V.lookup sw i
shape-same {suc n} {x ∷ sI} {y ∷ sw} I≥w I>0 w>0 zero =
  begin
    x ∸ (x ∸ y N.+ 1) N.+ 1 ≡⟨ sym $ +-∸-comm  {m = x} 1 {o = (x ∸ y N.+ 1)}  (s-w+1≤s (I≥w I0) (I>0 I0) (w>0 I0)) ⟩
    x N.+ 1 ∸ (x ∸ y N.+ 1) ≡⟨ cong (x N.+ 1 ∸_) (sym $ +-∸-comm {m = x} 1 {o = y} (I≥w I0)) ⟩
    x N.+ 1 ∸ (x N.+ 1 ∸ y) ≡⟨ m∸[m∸n]≡n {m = x N.+ 1} {n = y} (a≤b⇒b≡c⇒a≤c (≤-step $ I≥w I0) (+-comm 1 x)) ⟩
    y
  ∎
  where open ≡-Reasoning
shape-same {suc n} {x ∷ sI} {x₁ ∷ sw} I≥w I>0 w>0 (suc i) =
  shape-same {sI = sI} {sw = sw} (λ { (i ∷ []) → I≥w (suc i ∷ []) })
                                 (λ { (i ∷ []) → I>0 (suc i ∷ []) })
                                 (λ { (i ∷ []) → w>0 (suc i ∷ []) }) i

{-backmulticonv ← {
  (d_out weights in bias) ← ⍵
  d_in ← +⌿d_out {backin ⍺ ⍵ in} ⍤((⍴⍴in), (⍴⍴in)) ⊢ weights
  d_w ← {⍵ conv in} ⍤(⍴⍴in) ⊢ d_out
  d_bias ← backbias ⍤(⍴⍴in) ⊢ d_out
  d_in d_w d_bias
}-}
backmulticonv : ∀ {n m}{sI sw so}
              → (W : Ar (Ar Float n sw) m so)
              → (I : Ar Float n sI)
              → (B : Ar Float m so)
                -- We can get rid of these two expressions if we rewrite
                -- the convolution to accept s+1 ≥ w, and not s ≥ w.
              → {>I : (cst 0) <a s→a sI}
              → {>w : (cst 0) <a s→a sw}
              → {≥ : s→a sI ≥a s→a sw}
              → (δo : Ar (Ar Float n (a→s $ (s→a sI - s→a sw) {≥} + 1)) m so)
              → {- (typeOf W) ×ₜ-}  (typeOf I) --×ₜ (typeOf B)
backmulticonv {n} {sI = sI} {sw} {so} W I B {sI>0} {sw>0} {sI≥sw} δo = let
    δI = reduce-1d _+ᵣ_ (cst 0.0) (, (W ̈⟨ (λ x y → backin I x {sI≥sw} y) ⟩ δo))
    {-
    δW = (λ x → (x conv I) {≥ = λ { iv@(i ∷ []) → subst₂ _≤_ (sym $ V.lookup∘tabulate _ i) refl
                                                  $ s-w+1≤s (sI≥sw iv) (sI>0 iv) (sw>0 iv) } }) ̈ δo
    δB = backbias ̈ δo
    -}
  in --(imap (λ iv → subst-ar (shape-same {sI = sI} {sw = sw} sI≥sw sI>0 sw>0) (sel δW iv)) ,
     δI {-,
     imap (λ iv → ▾ (sel δB iv))) -}
  where open import Example-04
        open import Example-03

kbckmconv = kompile backmulticonv (quote _≥a_ ∷ quote _<a_ ∷ quote reduce-1d ∷ quote _↑⟨_⟩_ ∷ quote _-↑⟨_⟩_ ∷ quote a→ix ∷ quote _conv_ ∷ []) []
  where open import Example-04

conv-fns : List (String ×ₜ Name)
conv-fns = ("blog" , quote blog)
         ∷ ("backbias" , quote backbias)
         ∷ ("logistic" , quote logistic)
         ∷ ("meansqerr" , quote meansqerr)
         ∷ ("backavgpool" , quote backavgpool)
         ∷ ("avgpool" , quote avgpool)
         ∷ ("conv" , quote _conv_)
         ∷ ("multiconv" , quote multiconv)
         ∷ ("backin", quote backin)
         ∷ ("backmulticonv" , quote backmulticonv)
         ∷ []
  where open import Example-03
        open import Example-04

--   * test-zhang
--   * train-zhang

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
module Properties.Base where

open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All
open import Data.Product
open import Data.Sum

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Global
open import Values
open import Session
open import Schedule

one-step : ∀ {G} → (∃ λ G' → ThreadPool (G' ++ G)) → Event × (∃ λ G → ThreadPool G)
one-step{G} (G1 , tp)
  with ssplit-refl-left-inactive (G1 ++ G)
... | G' , ina-G' , ss-GG'
  with Alternative.step ss-GG' tp (tnil ina-G')
... | ev , tp' = ev , ( _ , tp')

restart : ∀ {G} → Command G → Command G
restart (Ready ss v κ) = apply-cont ss κ v
restart cmd = cmd

-- auxiliary lemmas

lift-unrestricted :
  ∀ {t G} (unrt : Unr t) (v : Val G t)
  → unrestricted-val unrt (lift-val v) ≡ ::-inactive (unrestricted-val unrt v)
lift-unrestricted-venv :
  ∀ {Φ G} (unrt : All Unr Φ) (ϱ : VEnv G Φ)
  → unrestricted-venv unrt (lift-venv ϱ) ≡ ::-inactive (unrestricted-venv unrt ϱ)

lift-unrestricted UUnit (VUnit inaG) = refl
lift-unrestricted UInt (VInt i inaG) = refl
lift-unrestricted (UPair unrt unrt₁) (VPair ss-GG₁G₂ v v₁)
  rewrite lift-unrestricted unrt v | lift-unrestricted unrt₁ v₁
  = refl
lift-unrestricted UFun (VFun (inj₁ ()) ϱ e)
lift-unrestricted UFun (VFun (inj₂ y) ϱ e) = lift-unrestricted-venv y ϱ

lift-unrestricted-venv [] (vnil ina) = refl
lift-unrestricted-venv (px ∷ unrt) (vcons ssp v ϱ)
  rewrite lift-unrestricted px v | lift-unrestricted-venv unrt ϱ
  = refl

unrestricted-empty : ∀ {t} → (unrt : Unr t) (v : Val [] t) → unrestricted-val unrt v ≡ []-inactive
unrestricted-empty-venv : ∀ {t} → (unrt : All Unr t) (v : VEnv [] t) → unrestricted-venv unrt v ≡ []-inactive

unrestricted-empty UUnit (VUnit []-inactive) = refl
unrestricted-empty UInt (VInt i []-inactive) = refl
unrestricted-empty (UPair unrt unrt₁) (VPair ss-[] v v₁)
  rewrite unrestricted-empty unrt v | unrestricted-empty unrt₁ v₁
  = refl
unrestricted-empty UFun (VFun (inj₁ ()) ϱ e)
unrestricted-empty UFun (VFun (inj₂ y) ϱ e) = unrestricted-empty-venv y ϱ

unrestricted-empty-venv [] (vnil []-inactive) = refl
unrestricted-empty-venv (px ∷ unrt) (vcons ss-[] v v₁)
  rewrite unrestricted-empty px v | unrestricted-empty-venv unrt v₁
  = refl

split-env-lemma :
  ∀ { Φ Φ₁ Φ₂ }
  (sp : Split Φ Φ₁ Φ₂)
  (ϱ : VEnv [] Φ)
  → ∃ λ ϱ₁ → ∃ λ ϱ₂ →
             split-env sp (lift-venv ϱ) ≡
             (((nothing ∷ []) , (nothing ∷ [])) , (ss-both ss-[]) , lift-venv ϱ₁ , lift-venv ϱ₂)

split-env-lemma [] (vnil []-inactive) =
  (vnil []-inactive) , ((vnil []-inactive) , refl)
split-env-lemma (dupl unrt sp) (vcons ss-[] v ϱ)
  with split-env-lemma sp ϱ | unrestricted-val unrt v
... | ϱ₁ , ϱ₂ , spe==  | unr-v
  rewrite inactive-left-ssplit ss-[] unr-v | lift-unrestricted unrt v | unrestricted-empty unrt v | spe==
  with ssplit-compose3 (ss-both ss-[]) (ss-both ss-[])
... | ssc3
  = (vcons ss-[] v ϱ₁)
  , (vcons ss-[] v ϱ₂)
  , refl
split-env-lemma (Split.drop unrt sp) (vcons ss-[] v ϱ)
  with split-env-lemma sp ϱ | unrestricted-val unrt v
... | ϱ₁ , ϱ₂ , spe== | unr-v
  rewrite lift-unrestricted unrt v | unrestricted-empty unrt v
  = ϱ₁ , ϱ₂ , spe==
split-env-lemma (left sp) (vcons ss-[] v ϱ)
  with split-env-lemma sp ϱ
... | ϱ₁ , ϱ₂ , spe==
  rewrite spe==
  with ssplit-compose3 (ss-both ss-[]) (ss-both ss-[])
... | ssc3
  = (vcons ss-[] v ϱ₁) , (ϱ₂ , refl)
split-env-lemma (rght sp) (vcons ss-[] v ϱ)
  with split-env-lemma sp ϱ
... | ϱ₁ , ϱ₂ , spe==
  rewrite spe==
  with ssplit-compose4 (ss-both ss-[]) (ss-both ss-[])
... | ssc4
  = ϱ₁ , (vcons ss-[] v ϱ₂) , refl

split-env-right-lemma :
  ∀ {Φ} (ϱ : VEnv [] Φ) →
  split-env (split-all-right Φ) (lift-venv ϱ)
  ≡
  (((nothing ∷ []) , (nothing ∷ [])) , (ss-both ss-[]) , vnil (::-inactive []-inactive) , lift-venv ϱ)
split-env-right-lemma (vnil []-inactive) = refl
split-env-right-lemma (vcons ss-[] v ϱ)
  with split-env-right-lemma ϱ
... | sperl
  rewrite sperl
  with ssplit-compose4 (ss-both ss-[]) (ss-both ss-[])
... | ssc4
  = refl

split-env-right-lemma0 :
  ∀ {Φ} (ϱ : VEnv [] Φ) →
  split-env (split-all-right Φ) ϱ
  ≡
  (([] , []) , ss-[] , vnil []-inactive , ϱ)
split-env-right-lemma0 (vnil []-inactive) = refl
split-env-right-lemma0 (vcons ss-[] v ϱ)
  rewrite split-env-right-lemma0 ϱ
  = refl

split-env-left-lemma0 :
  ∀ {Φ} (ϱ : VEnv [] Φ) →
  split-env (split-all-left Φ) ϱ
  ≡
  (([] , []) , ss-[] , ϱ , vnil []-inactive)
split-env-left-lemma0 (vnil []-inactive) = refl
split-env-left-lemma0 (vcons ss-[] v ϱ)
  rewrite split-env-left-lemma0 ϱ
  = refl

split-env-lemma-2T : Set
split-env-lemma-2T =
  ∀ { Φ Φ₁ Φ₂ }
  (sp : Split Φ Φ₁ Φ₂)
  (ϱ : VEnv [] Φ)
  → ∃ λ ϱ₁ → ∃ λ ϱ₂ →
             split-env sp (lift-venv ϱ) ≡
             (_ , (ss-both ss-[]) , lift-venv ϱ₁ , lift-venv ϱ₂)
             ×
             split-env sp ϱ ≡
             (_ , ss-[] , ϱ₁ , ϱ₂)

split-env-lemma-2 : split-env-lemma-2T
split-env-lemma-2 [] (vnil []-inactive)
  = (vnil []-inactive) , ((vnil []-inactive) , (refl , refl))
split-env-lemma-2 (dupl unrt sp) (vcons ss-[] v ϱ)
  with split-env-lemma-2 sp ϱ
... | ϱ₁ , ϱ₂ , selift-ind , se-ind
  rewrite se-ind | lift-unrestricted unrt v
  with unrestricted-val unrt v
... | []-inactive
  rewrite selift-ind
  with ssplit-compose3 (ss-both ss-[]) (ss-both ss-[])
... | ssc3
  = (vcons ss-[] v ϱ₁) , (vcons ss-[] v ϱ₂) , refl , refl
split-env-lemma-2 (Split.drop unrt sp) (vcons ss-[] v ϱ)
  with split-env-lemma-2 sp ϱ
... | ϱ₁ , ϱ₂ , selift-ind , se-ind
  rewrite se-ind | lift-unrestricted unrt v
  with unrestricted-val unrt v
... | []-inactive
  = ϱ₁ , ϱ₂ , selift-ind , se-ind
split-env-lemma-2 (left sp) (vcons ss-[] v ϱ)
  with split-env-lemma-2 sp ϱ
... | ϱ₁ , ϱ₂ , selift-ind , se-ind
  rewrite se-ind | selift-ind
  with ssplit-compose3 (ss-both ss-[]) (ss-both ss-[])
... | ssc3
  = (vcons ss-[] v ϱ₁) , ϱ₂ , refl , refl
split-env-lemma-2 (rght sp) (vcons ss-[] v ϱ)
  with split-env-lemma-2 sp ϱ
... | ϱ₁ , ϱ₂ , selift-ind , se-ind
  rewrite se-ind | selift-ind
  with ssplit-compose4 (ss-both ss-[]) (ss-both ss-[])
... | ssc4
  = ϱ₁ , (vcons ss-[] v ϱ₂) , refl , refl

split-rotate-lemma : ∀ {Φ} →
  split-rotate (split-all-left Φ) (split-all-right Φ)
  ≡
  (Φ , split-all-right Φ , split-all-left Φ)

split-rotate-lemma {[]} = refl
split-rotate-lemma {x ∷ Φ}
  rewrite split-rotate-lemma {Φ}
  = refl

split-rotate-lemma' :  ∀ {Φ Φ₁ Φ₂}
  (sp : Split Φ Φ₁ Φ₂) →
  split-rotate (split-all-left Φ) sp
  ≡
  (Φ₂ , sp , split-all-left Φ₂)

split-rotate-lemma' {[]} [] = refl
split-rotate-lemma' {x ∷ Φ} (dupl un-x sp)
  rewrite split-rotate-lemma' {Φ} sp
  = refl
split-rotate-lemma' {x ∷ Φ} {Φ₁} {Φ₂} (Split.drop un-x sp)
  rewrite split-rotate-lemma' {Φ} sp
  = refl
split-rotate-lemma' {x ∷ Φ} (left sp)
  rewrite split-rotate-lemma' {Φ} sp
  = refl
split-rotate-lemma' {x ∷ Φ} (rght sp)
  rewrite split-rotate-lemma' {Φ} sp
  = refl

ssplit-compose-lemma : ∀ ss →
  ssplit-compose ss-[] ss ≡ ([] , ss-[] , ss-[])
ssplit-compose-lemma ss-[] = refl

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
open import Oscar.Prelude
open import Oscar.Class.IsFunctor
open import Oscar.Class.Reflexivity
open import Oscar.Class.Smap
open import Oscar.Class.Surjection
open import Oscar.Class.Transitivity

module Oscar.Class.Functor where

record Functor 𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂ : Ø ↑̂ (𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂) where
  constructor ∁
  field
    {𝔒₁} : Ø 𝔬₁
    _∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁
    _∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁
    ε₁ : Reflexivity.type _∼₁_
    _↦₁_ : Transitivity.type _∼₁_
    {𝔒₂} : Ø 𝔬₂
    _∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂
    _∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂
    ε₂ : Reflexivity.type _∼₂_
    _↦₂_ : Transitivity.type _∼₂_
    {μ} : Surjection.type 𝔒₁ 𝔒₂
    functor-smap : Smap.type _∼₁_ _∼₂_ μ μ -- FIXME cannot name this § or smap b/c of namespace conflict
    ⦃ `IsFunctor ⦄ : IsFunctor _∼₁_ _∼̇₁_ ε₁ _↦₁_ _∼₂_ _∼̇₂_ ε₂ _↦₂_ functor-smap


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Overloading ⟦_⟧ notation
--
-- This module defines a general mechanism for overloading the
-- ⟦_⟧ notation, using Agda’s instance arguments.
------------------------------------------------------------------------

module Base.Denotation.Notation where

open import Level

record Meaning (Syntax : Set) {ℓ : Level} : Set (suc ℓ) where
  constructor
    meaning
  field
    {Semantics} : Set ℓ
    ⟨_⟩⟦_⟧ : Syntax → Semantics

open Meaning {{...}} public
  renaming (⟨_⟩⟦_⟧ to ⟦_⟧)

open Meaning public
  using (⟨_⟩⟦_⟧)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
module IsLiteralProblem where

open import OscarPrelude
open import IsLiteralSequent
open import Problem

record IsLiteralProblem (𝔓 : Problem) : Set
 where
  constructor _¶_
  field
    {problem} : Problem
    isLiteralInferences : All IsLiteralSequent (inferences 𝔓)
    isLiteralInterest : IsLiteralSequent (interest 𝔓)

open IsLiteralProblem public

instance EqIsLiteralProblem : ∀ {𝔓} → Eq (IsLiteralProblem 𝔓)
EqIsLiteralProblem = {!!}


text:
module Pi-.Invariants where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Function using (_∘_)
open import Pi-.Syntax
open import Pi-.Opsem
open import Pi-.NoRepeat
open import Pi-.Dir

-- Direction of values
dir𝕍 : ∀ {t} → ⟦ t ⟧ → Dir
dir𝕍 {𝟘} ()
dir𝕍 {𝟙} v = ▷
dir𝕍 {_ +ᵤ _} (inj₁ x) = dir𝕍 x
dir𝕍 {_ +ᵤ _} (inj₂ y) = dir𝕍 y
dir𝕍 {_ ×ᵤ _} (x , y) = dir𝕍 x ×ᵈⁱʳ dir𝕍 y
dir𝕍 { - _} (- v) = -ᵈⁱʳ (dir𝕍 v)

-- Execution direction of states
dirState : State → Dir
dirState ⟨ _ ∣ _ ∣ _ ⟩▷ = ▷
dirState ［ _ ∣ _ ∣ _ ］▷ = ▷
dirState ⟨ _ ∣ _ ∣ _ ⟩◁ = ◁
dirState ［ _ ∣ _ ∣ _ ］◁ = ◁

dirCtx : ∀ {A B} → Context {A} {B} → Dir
dirCtx ☐ = ▷
dirCtx (☐⨾ c₂ • κ) = dirCtx κ
dirCtx (c₁ ⨾☐• κ) = dirCtx κ
dirCtx (☐⊕ c₂ • κ) = dirCtx κ
dirCtx (c₁ ⊕☐• κ) = dirCtx κ
dirCtx (☐⊗[ c₂ , x ]• κ) = dir𝕍 x ×ᵈⁱʳ dirCtx κ
dirCtx ([ c₁ , x ]⊗☐• κ) = dir𝕍 x ×ᵈⁱʳ dirCtx κ

dirState𝕍 : State → Dir
dirState𝕍 ⟨ _ ∣ v ∣ κ ⟩▷ = dir𝕍 v  ×ᵈⁱʳ dirCtx κ
dirState𝕍 ［ _ ∣ v ∣ κ ］▷ = dir𝕍 v  ×ᵈⁱʳ dirCtx κ
dirState𝕍 ⟨ _ ∣ v ∣ κ ⟩◁ = dir𝕍 v  ×ᵈⁱʳ dirCtx κ
dirState𝕍 ［ _ ∣ v ∣ κ ］◁ = dir𝕍 v  ×ᵈⁱʳ dirCtx κ

δdir : ∀ {A B} (c : A ↔ B) {b : base c} → (v : ⟦ A ⟧) → dir𝕍 v ≡ dir𝕍 (δ c {b} v)
δdir unite₊l (inj₂ v) = refl
δdir uniti₊l v = refl
δdir swap₊ (inj₁ x) = refl
δdir swap₊ (inj₂ y) = refl
δdir assocl₊ (inj₁ v) = refl
δdir assocl₊ (inj₂ (inj₁ v)) = refl
δdir assocl₊ (inj₂ (inj₂ v)) = refl
δdir assocr₊ (inj₁ (inj₁ v)) = refl
δdir assocr₊ (inj₁ (inj₂ v)) = refl
δdir assocr₊ (inj₂ v) = refl
δdir unite⋆l (tt , v) = identˡᵈⁱʳ (dir𝕍 v)
δdir uniti⋆l v = sym (identˡᵈⁱʳ (dir𝕍 v))
δdir swap⋆ (x , y) = commᵈⁱʳ _ _
δdir assocl⋆ (v₁ , (v₂ , v₃)) = assoclᵈⁱʳ _ _ _
δdir assocr⋆ ((v₁ , v₂) , v₃) = sym (assoclᵈⁱʳ _ _ _)
δdir dist (inj₁ v₁ , v₃) = refl
δdir dist (inj₂ v₂ , v₃) = refl
δdir factor (inj₁ (v₁ , v₃)) = refl
δdir factor (inj₂ (v₂ , v₃)) = refl

-- Invariant of directions
dirInvariant : ∀ {st st'} → st ↦ st' → dirState st ×ᵈⁱʳ dirState𝕍 st ≡ dirState st' ×ᵈⁱʳ dirState𝕍 st'
dirInvariant {⟨ c ∣ v ∣ κ ⟩▷} (↦⃗₁ {b = b}) rewrite δdir c {b} v = refl
dirInvariant ↦⃗₂ = refl
dirInvariant ↦⃗₃ = refl
dirInvariant ↦⃗₄ = refl
dirInvariant ↦⃗₅ = refl
dirInvariant {⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ⟩▷} ↦⃗₆ rewrite assoclᵈⁱʳ (dir𝕍 x) (dir𝕍 y) (dirCtx κ) = refl
dirInvariant ↦⃗₇ = refl
dirInvariant {［ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ］▷} ↦⃗₈ rewrite assoc-commᵈⁱʳ (dir𝕍 x) (dir𝕍 y) (dirCtx κ) = refl
dirInvariant {［ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ］▷} ↦⃗₉ rewrite assocl-commᵈⁱʳ (dir𝕍 y) (dir𝕍 x) (dirCtx κ) = refl
dirInvariant ↦⃗₁₀ = refl
dirInvariant ↦⃗₁₁ = refl
dirInvariant ↦⃗₁₂ = refl
dirInvariant {_} {⟨ c ∣ v ∣ κ ⟩◁} (↦⃖₁ {b = b}) rewrite δdir c {b} v = refl
dirInvariant ↦⃖₂ = refl
dirInvariant ↦⃖₃ = refl
dirInvariant ↦⃖₄ = refl
dirInvariant ↦⃖₅ = refl
dirInvariant {⟨ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ⟩◁} ↦⃖₆ rewrite assoclᵈⁱʳ (dir𝕍 x) (dir𝕍 y) (dirCtx κ) = refl
dirInvariant ↦⃖₇ = refl
dirInvariant {⟨ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ⟩◁} ↦⃖₈ rewrite assoc-commᵈⁱʳ (dir𝕍 y) (dir𝕍 x) (dirCtx κ) = refl
dirInvariant {［ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ］◁ } ↦⃖₉ rewrite assoclᵈⁱʳ (dir𝕍 y) (dir𝕍 x) (dirCtx κ) | commᵈⁱʳ (dir𝕍 y) (dir𝕍 x) = refl
dirInvariant ↦⃖₁₀ = refl
dirInvariant ↦⃖₁₁ = refl
dirInvariant ↦⃖₁₂ = refl
dirInvariant {［ η₊ ∣ inj₁ v ∣ κ ］◁} ↦η₁ with dir𝕍 v
... | ◁ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {［ η₊ ∣ inj₁ v ∣ κ ］◁} ↦η₁ | ▷ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {［ η₊ ∣ inj₂ (- v) ∣ κ ］◁} ↦η₂ with dir𝕍 v
... | ◁ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {［ η₊ ∣ inj₂ (- v) ∣ κ ］◁} ↦η₂ | ▷ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {⟨ ε₊ ∣ inj₁ v ∣ κ ⟩▷} ↦ε₁ with dir𝕍 v
... | ◁ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {⟨ ε₊ ∣ inj₁ v ∣ κ ⟩▷} ↦ε₁ | ▷ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {⟨ ε₊ ∣ inj₂ (- v) ∣ κ ⟩▷} ↦ε₂ with dir𝕍 v
... | ◁ with dirCtx κ
... | ◁ = refl
... | ▷ = refl
dirInvariant {⟨ ε₊ ∣ inj₂ (- v) ∣ κ ⟩▷} ↦ε₂ | ▷ with dirCtx κ
... | ◁ = refl
... | ▷ = refl

-- Reconstruct the whole combinator from context
getℂκ : ∀ {A B} → A ↔ B → Context {A} {B} → ∃[ C ] ∃[ D ] (C ↔ D)
getℂκ c ☐ = _ , _ , c
getℂκ c (☐⨾ c₂ • κ) = getℂκ (c ⨾ c₂) κ
getℂκ c (c₁ ⨾☐• κ) = getℂκ (c₁ ⨾ c) κ
getℂκ c (☐⊕ c₂ • κ) = getℂκ (c ⊕ c₂) κ
getℂκ c (c₁ ⊕☐• κ) = getℂκ (c₁ ⊕ c) κ
getℂκ c (☐⊗[ c₂ , x ]• κ) = getℂκ (c ⊗ c₂) κ
getℂκ c ([ c₁ , x ]⊗☐• κ) = getℂκ (c₁ ⊗ c) κ

getℂ : State → ∃[ A ] ∃[ B ] (A ↔ B)
getℂ ⟨ c ∣ _ ∣ κ ⟩▷ = getℂκ c κ
getℂ ［ c ∣ _ ∣ κ ］▷ = getℂκ c κ
getℂ ⟨ c ∣ _ ∣ κ ⟩◁ = getℂκ c κ
getℂ ［ c ∣ _ ∣ κ ］◁ = getℂκ c κ

-- The reconstructed combinator stays the same
ℂInvariant : ∀ {st st'} → st ↦ st' → getℂ st ≡  getℂ st'
ℂInvariant ↦⃗₁ = refl
ℂInvariant ↦⃗₂ = refl
ℂInvariant ↦⃗₃ = refl
ℂInvariant ↦⃗₄ = refl
ℂInvariant ↦⃗₅ = refl
ℂInvariant ↦⃗₆ = refl
ℂInvariant ↦⃗₇ = refl
ℂInvariant ↦⃗₈ = refl
ℂInvariant ↦⃗₉ = refl
ℂInvariant ↦⃗₁₀ = refl
ℂInvariant ↦⃗₁₁ = refl
ℂInvariant ↦⃗₁₂ = refl
ℂInvariant ↦⃖₁ = refl
ℂInvariant ↦⃖₂ = refl
ℂInvariant ↦⃖₃ = refl
ℂInvariant ↦⃖₄ = refl
ℂInvariant ↦⃖₅ = refl
ℂInvariant ↦⃖₆ = refl
ℂInvariant ↦⃖₇ = refl
ℂInvariant ↦⃖₈ = refl
ℂInvariant ↦⃖₉ = refl
ℂInvariant ↦⃖₁₀ = refl
ℂInvariant ↦⃖₁₁ = refl
ℂInvariant ↦⃖₁₂ = refl
ℂInvariant ↦η₁ = refl
ℂInvariant ↦η₂ = refl
ℂInvariant ↦ε₁ = refl
ℂInvariant ↦ε₂ = refl

ℂInvariant* : ∀ {st st'} → st ↦* st' → getℂ st ≡  getℂ st'
ℂInvariant* ◾ = refl
ℂInvariant* (r ∷ rs) = trans (ℂInvariant r) (ℂInvariant* rs)

-- Get the type of the deepest context
get𝕌 : ∀ {A B} → Context {A} {B} → 𝕌 × 𝕌
get𝕌 {A} {B} ☐ = A , B
get𝕌 (☐⨾ c₂ • κ) = get𝕌 κ
get𝕌 (c₁ ⨾☐• κ) = get𝕌 κ
get𝕌 (☐⊕ c₂ • κ) = get𝕌 κ
get𝕌 (c₁ ⊕☐• κ) = get𝕌 κ
get𝕌 (☐⊗[ c₂ , x ]• κ) = get𝕌 κ
get𝕌 ([ c₁ , x ]⊗☐• κ) = get𝕌 κ

get𝕌State : State → 𝕌 × 𝕌
get𝕌State ⟨ c ∣ v ∣ κ ⟩▷ = get𝕌 κ
get𝕌State ［ c ∣ v ∣ κ ］▷ = get𝕌 κ
get𝕌State ⟨ c ∣ v ∣ κ ⟩◁ = get𝕌 κ
get𝕌State ［ c ∣ v ∣ κ ］◁ = get𝕌 κ

-- Append a context to another context
appendκ : ∀ {A B} → (ctx : Context {A} {B}) → let (C , D) = get𝕌  ctx
                                              in  Context {C} {D} → Context {A} {B}
appendκ ☐ ctx = ctx
appendκ (☐⨾ c₂ • κ) ctx = ☐⨾ c₂ • appendκ κ ctx
appendκ (c₁ ⨾☐• κ) ctx = c₁ ⨾☐• appendκ κ ctx
appendκ (☐⊕ c₂ • κ) ctx = ☐⊕ c₂ • appendκ κ ctx
appendκ (c₁ ⊕☐• κ) ctx = c₁ ⊕☐• appendκ κ ctx
appendκ (☐⊗[ c₂ , x ]• κ) ctx = ☐⊗[ c₂ , x ]• appendκ κ ctx
appendκ ([ c₁ , x ]⊗☐• κ) ctx = [ c₁ , x ]⊗☐• appendκ κ ctx

appendκState : ∀ st → let (A , B) = get𝕌State st
                      in  Context {A} {B} → State
appendκState ⟨ c ∣ v ∣ κ ⟩▷ ctx = ⟨ c ∣ v ∣ appendκ κ ctx ⟩▷
appendκState ［ c ∣ v ∣ κ ］▷ ctx = ［ c ∣ v ∣ appendκ κ ctx ］▷
appendκState ⟨ c ∣ v ∣ κ ⟩◁ ctx = ⟨ c ∣ v ∣ appendκ κ ctx ⟩◁
appendκState ［ c ∣ v ∣ κ ］◁ ctx = ［ c ∣ v ∣ appendκ κ ctx ］◁

-- The type of context does not change during execution
𝕌Invariant : ∀ {st st'} → st ↦ st' → get𝕌State st ≡ get𝕌State st'
𝕌Invariant ↦⃗₁ = refl
𝕌Invariant ↦⃗₂ = refl
𝕌Invariant ↦⃗₃ = refl
𝕌Invariant ↦⃗₄ = refl
𝕌Invariant ↦⃗₅ = refl
𝕌Invariant ↦⃗₆ = refl
𝕌Invariant ↦⃗₇ = refl
𝕌Invariant ↦⃗₈ = refl
𝕌Invariant ↦⃗₉ = refl
𝕌Invariant ↦⃗₁₀ = refl
𝕌Invariant ↦⃗₁₁ = refl
𝕌Invariant ↦⃗₁₂ = refl
𝕌Invariant ↦⃖₁ = refl
𝕌Invariant ↦⃖₂ = refl
𝕌Invariant ↦⃖₃ = refl
𝕌Invariant ↦⃖₄ = refl
𝕌Invariant ↦⃖₅ = refl
𝕌Invariant ↦⃖₆ = refl
𝕌Invariant ↦⃖₇ = refl
𝕌Invariant ↦⃖₈ = refl
𝕌Invariant ↦⃖₉ = refl
𝕌Invariant ↦⃖₁₀ = refl
𝕌Invariant ↦⃖₁₁ = refl
𝕌Invariant ↦⃖₁₂ = refl
𝕌Invariant ↦η₁ = refl
𝕌Invariant ↦η₂ = refl
𝕌Invariant ↦ε₁ = refl
𝕌Invariant ↦ε₂ = refl

𝕌Invariant* : ∀ {st st'} → st ↦* st' → get𝕌State st ≡  get𝕌State st'
𝕌Invariant* ◾ = refl
𝕌Invariant* (r ∷ rs) = trans (𝕌Invariant r) (𝕌Invariant* rs)

-- Appending context does not affect reductions
appendκ↦ : ∀ {st st'} → (r : st ↦ st') (eq : get𝕌State st ≡  get𝕌State st')
         → (κ : Context {proj₁ (get𝕌State st)} {proj₂ (get𝕌State st)})
         → appendκState st κ ↦ appendκState st' (subst (λ {(A , B) → Context {A} {B}}) eq κ)
appendκ↦ ↦⃗₁ refl ctx = ↦⃗₁
appendκ↦ ↦⃗₂ refl ctx = ↦⃗₂
appendκ↦ ↦⃗₃ refl ctx = ↦⃗₃
appendκ↦ ↦⃗₄ refl ctx = ↦⃗₄
appendκ↦ ↦⃗₅ refl ctx = ↦⃗₅
appendκ↦ ↦⃗₆ refl ctx = ↦⃗₆
appendκ↦ ↦⃗₇ refl ctx = ↦⃗₇
appendκ↦ ↦⃗₈ refl ctx = ↦⃗₈
appendκ↦ ↦⃗₉ refl ctx = ↦⃗₉
appendκ↦ ↦⃗₁₀ refl ctx = ↦⃗₁₀
appendκ↦ ↦⃗₁₁ refl ctx = ↦⃗₁₁
appendκ↦ ↦⃗₁₂ refl ctx = ↦⃗₁₂
appendκ↦ ↦⃖₁ refl ctx = ↦⃖₁
appendκ↦ ↦⃖₂ refl ctx = ↦⃖₂
appendκ↦ ↦⃖₃ refl ctx = ↦⃖₃
appendκ↦ ↦⃖₄ refl ctx = ↦⃖₄
appendκ↦ ↦⃖₅ refl ctx = ↦⃖₅
appendκ↦ ↦⃖₆ refl ctx = ↦⃖₆
appendκ↦ ↦⃖₇ refl ctx = ↦⃖₇
appendκ↦ ↦⃖₈ refl ctx = ↦⃖₈
appendκ↦ ↦⃖₉ refl ctx = ↦⃖₉
appendκ↦ ↦⃖₁₀ refl ctx = ↦⃖₁₀
appendκ↦ ↦⃖₁₁ refl ctx = ↦⃖₁₁
appendκ↦ ↦⃖₁₂ refl ctx = ↦⃖₁₂
appendκ↦ ↦η₁ refl ctx = ↦η₁
appendκ↦ ↦η₂ refl ctx = ↦η₂
appendκ↦ ↦ε₁ refl ctx = ↦ε₁
appendκ↦ ↦ε₂ refl ctx = ↦ε₂

appendκ↦* : ∀ {st st'} → (r : st ↦* st') (eq : get𝕌State st ≡  get𝕌State st')
          → (κ : Context {proj₁ (get𝕌State st)} {proj₂ (get𝕌State st)})
          → appendκState st κ ↦* appendκState st' (subst (λ {(A , B) → Context {A} {B}}) eq κ)
appendκ↦* ◾ refl ctx = ◾
appendκ↦* (↦⃗₁ {b = b} {v} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₁ {b = b} {v} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₂ {v = v} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₂ {v = v} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₃ {v = v} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₃ {v = v} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₄ {x = x} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₄ {x = x} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₅ {y = y} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₅ {y = y} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₆ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₆ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₇ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₇ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₈ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₈ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₉ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₉ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₁₀ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₁₀ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₁₁ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₁₁ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃗₁₂ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃗₁₂ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₁ {b = b} {v} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₁ {b = b} {v} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₂ {v = v} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₂ {v = v} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₃ {v = v} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₃ {v = v} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₄ {x = x} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₄ {x = x} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₅ {y = y} {κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₅ {y = y} {κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₆ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₆ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₇ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₇ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₈ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₈ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₉ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₉ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₁₀ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₁₀ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₁₁ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₁₁ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦⃖₁₂ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦⃖₁₂ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦η₁ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦η₁ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦η₂ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦η₂ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦ε₁ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦ε₁ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦ε₂ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦ε₂ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx