text:
--{-# OPTIONS --allow-unsolved-metas #-}

module StateSizedIO.GUI.WxGraphicsLibLevel3 where

open import StateSizedIO.GUI.Prelude

data GuiLev1Command  : Set where
  putStrLn     : String  →  GuiLev1Command
  createFrame  : GuiLev1Command
  addButton    : Frame → Button → GuiLev1Command

  createTextCtrl     : Frame   → String → GuiLev1Command
  fireCustomEvent    : Frame   → GuiLev1Command
  setAttribButton    : Button  → WxColor → GuiLev1Command
  setAttribTextCtrl  : TextCtrl  → WxColor → GuiLev1Command
  setChildredLayout  : Frame   → ℕ → ℕ → ℕ → ℕ → GuiLev1Command
  createButton       : Frame   → String → GuiLev1Command
  deleteButton       : Button  → GuiLev1Command
  deleteTextCtrl     : TextCtrl → GuiLev1Command
  drawBitmap         : DC      → Bitmap → Point → Bool → GuiLev1Command
  repaint            : Frame   → GuiLev1Command
  bitmapGetWidth     : Bitmap  → GuiLev1Command

GuiLev1Response : GuiLev1Command → Set
GuiLev1Response  createFrame         = Frame
GuiLev1Response  (createButton _ _)    = Button
GuiLev1Response  (bitmapGetWidth _)  = ℤ
GuiLev1Response  (createTextCtrl _ _)    = TextCtrl
GuiLev1Response _                    =  Unit

GuiLev1Interface  :  IOInterface
GuiLev1Interface  .Command   =  GuiLev1Command
GuiLev1Interface  .Response  =  GuiLev1Response

GuiLev2State : Set₁
GuiLev2State = VarList

data GuiLev2Command (s :  GuiLev2State) : Set₁ where
  level1C        : GuiLev1Command → GuiLev2Command s
  createVar      : {A : Set} → A → GuiLev2Command s
  setButtonHandler :
    Button
    → List (prod s → IO GuiLev1Interface ∞ (prod s))
    → GuiLev2Command s
  setTimer          : Frame → ℤ → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → GuiLev2Command s
  setKeyHandler     : Button
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → GuiLev2Command s
  setOnPaint        : Frame
                     → List (prod s → DC → Rect → IO GuiLev1Interface ∞ (prod s))
                     → GuiLev2Command s

GuiLev2Response : (s : GuiLev2State)
                  → GuiLev2Command s → Set
GuiLev2Response _ (level1C c) = GuiLev1Response c
GuiLev2Response _ (createVar {A} a) = Var A
GuiLev2Response _ (setTimer fra x p) = Timer
GuiLev2Response _ _ = Unit

GuiLev2Next : (s : GuiLev2State) (c : GuiLev2Command s)
              → GuiLev2Response s c
              → GuiLev2State
GuiLev2Next s (createVar {A} a) var = addVar A var s
GuiLev2Next s _  _                  = s

GuiLev2Interface : IOInterfaceˢ
Stateˢ     GuiLev2Interface = GuiLev2State
Commandˢ   GuiLev2Interface = GuiLev2Command
Responseˢ  GuiLev2Interface = GuiLev2Response
nextˢ      GuiLev2Interface = GuiLev2Next

translateLev1Local :  (c : GuiLev1Command)
                      → NativeIO (GuiLev1Response c)
translateLev1Local createFrame            = nativeCreateFrame

translateLev1Local (setChildredLayout win a b c d) = nativeSetChildredLayout win a b c d
translateLev1Local (createButton fra str)   = nativeMakeButton fra str
translateLev1Local (deleteButton bt)      = nativeDeleteButton bt
translateLev1Local (deleteTextCtrl txt)   = nativeDeleteTextCtrl txt
translateLev1Local (addButton fra bt)     = nativeAddButton fra bt
translateLev1Local (setAttribButton bt col) = nativeSetColorButton bt col

translateLev1Local (setAttribTextCtrl txt col) = nativeSetColorTextCtrl txt col
translateLev1Local (drawBitmap dc bm p b) = nativeDrawBitmap dc bm p b
translateLev1Local (repaint fra)          = nativeRepaint fra
translateLev1Local (bitmapGetWidth b)     = nativeBitmapGetWidth b
translateLev1Local (putStrLn s)           = nativePutStrLn s
translateLev1Local (fireCustomEvent fr)   = nativeFireCustomEvent fr
translateLev1Local (createTextCtrl f str) = nativeMakeTextCtrl f str

translateLev1 : {A : Set} → IO GuiLev1Interface ∞ A → NativeIO A
translateLev1 = translateIO translateLev1Local

translateLev1List : {A : Set} → List (IO GuiLev1Interface ∞ A) → List (NativeIO A)
translateLev1List l = map translateLev1 l

translateLev2Local : (s : GuiLev2State)
                          → (c : GuiLev2Command s)
                          → NativeIO (GuiLev2Response s c)
translateLev2Local s (level1C c) = translateLev1Local c

translateLev2Local s (createVar {A} a)   = nativeNewVar {A} a
translateLev2Local s (setButtonHandler bt proglist)
    = nativeSetButtonHandler bt
            (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglist))

translateLev2Local s (setTimer fra interv proglist)
    = nativeSetTimer fra interv (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglist))

translateLev2Local s (setKeyHandler bt proglistRight proglistLeft proglistUp proglistDown)
    =  nativeSetKeyHandler bt
           (λ key -> case (showKey key) of λ
                 { "Right" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistRight))
                 ; "Left" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistLeft))
                 ; "Up" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistUp))
                 ; "Down" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistDown))
                 ; _  → nativeReturn unit
                 } )

translateLev2Local s (setOnPaint fra proglist)
    = nativeSetOnPaint fra (λ dc rect → (dispatchList s
         (map (λ prog aa → translateLev1 (prog aa dc rect)) proglist)))

translateLev2 : {s : GuiLev2State} → {A : Set}
                     → IOˢ GuiLev2Interface ∞ (λ _ → A) s → NativeIO A
translateLev2 = translateIOˢ {I = GuiLev2Interface} translateLev2Local

data GuiLev3Command (s :  GuiLev2State) : Set₂ where
  level2C : GuiLev2Command s → GuiLev3Command s
  setCustomEvent :
    Frame
    →  List
       ((x : prod s) → IOˢ GuiLev2Interface ∞ (λ _ → prod s) s)
    →  GuiLev3Command s

  setRightClick     : Frame → List ( (x : prod s) → IOˢ GuiLev2Interface ∞ (λ _ → prod s) s)
                     → GuiLev3Command s

GuiLev3Response : (s : GuiLev2State) → GuiLev3Command s → Set
GuiLev3Response s (level2C c)         = GuiLev2Response s c
GuiLev3Response _ _                   = Unit

GuiLev3Next : (s : GuiLev2State) → (c : GuiLev3Command s)
              → GuiLev3Response s c
              → GuiLev2State
GuiLev3Next s (level2C c) r = GuiLev2Next s c r
GuiLev3Next s (setRightClick _ _) _ = s
GuiLev3Next s (setCustomEvent _ _) _ = s

GuiLev3Interface : IOInterfaceˢ
GuiLev3Interface .Stateˢ = GuiLev2State
GuiLev3Interface .Commandˢ = GuiLev3Command
GuiLev3Interface .Responseˢ = GuiLev3Response
GuiLev3Interface .nextˢ = GuiLev3Next

translateLev3Local : (s : GuiLev2State)
                          → (c : GuiLev3Command s)
                          → NativeIO (GuiLev3Response s c)
translateLev3Local s (level2C c) = translateLev2Local s c
translateLev3Local s (setRightClick f proglist) =
    nativeSetClickRight f
           (dispatchList s (map (λ prog → translateLev2{s} ∘ prog ) proglist))

translateLev3Local s (setCustomEvent f proglist) =

    nativeRegisterCustomEvent f
           (dispatchList s (map (λ prog → translateLev2{s} ∘ prog ) proglist))

translateLev3 : {s : GuiLev2State} → {A : Set}
                     → IOˢ GuiLev3Interface ∞ (λ _ → A) s → NativeIO A
translateLev3 = translateIOˢ {I = GuiLev3Interface} translateLev3Local

mutual
  translateLev1toLev2∞ : ∀{s : GuiLev2State} → {A : Set}
                       → IO' GuiLev1Interface ∞ A → IOˢ' GuiLev2Interface ∞ (λ _ → A) s
  translateLev1toLev2∞ (do' c f) = doˢ' (level1C c) λ r → translateLev1toLev2 (f r)
  translateLev1toLev2∞ (return' a) = returnˢ' a

  translateLev1toLev2ₚ∞ : ∀{s : GuiLev2State} → {A : Set} → IO' GuiLev1Interface ∞ A
                                      → IOₚˢ' GuiLev2Interface ∞ A s s
  translateLev1toLev2ₚ∞ (do' c f) = doˢ' (level1C c) (λ r → translateLev1toLev2ₚ (f r))
  translateLev1toLev2ₚ∞ (return' a) = returnˢ' (refl , a)

  translateLev1toLev2 : ∀{s : GuiLev2State} → {A : Set}
                       → IO GuiLev1Interface ∞ A → IOˢ GuiLev2Interface ∞ (λ _ → A) s
  translateLev1toLev2 x .forceˢ = translateLev1toLev2∞ (x .force)

  translateLev1toLev2ₚ : ∀{s : GuiLev2State} → {A : Set}
                       → IO GuiLev1Interface ∞ A → IOₚˢ GuiLev2Interface ∞ A s s
  translateLev1toLev2ₚ x .forceˢ = translateLev1toLev2ₚ∞ (x .force)

mutual
  translateLev2toLev3∞ : ∀{α}{s : GuiLev2State} → {A : GuiLev2State → Set α}
                     → IOˢ' GuiLev2Interface ∞ A s → IOˢ' GuiLev3Interface ∞ A s
  translateLev2toLev3∞ (doˢ'{s} c f) = doˢ' (level2C c) λ r → translateLev2toLev3 (f r)
  translateLev2toLev3∞ (returnˢ' a) = returnˢ' a

  translateLev2toLev3 : ∀{α}{s : GuiLev2State} → {A : GuiLev2State → Set α}
                       → IOˢ GuiLev2Interface ∞ A s → IOˢ GuiLev3Interface ∞ A s
  translateLev2toLev3 x .forceˢ = translateLev2toLev3∞ (x .forceˢ)

--
-- Example
--
example : IO GuiLev1Interface ∞ Frame
example =
  do  createFrame                 λ frame  →
  do  (putStrLn "Frame created")  λ _      →
  return frame
private
 main : NativeIO Frame
 main = translateIO translateLev1Local example

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module Tactic.Monoid where

open import Prelude
open import Tactic.Reflection
open import Tactic.Reflection.Quote

open import Structure.Monoid.Laws

open import Tactic.Monoid.Exp
open import Tactic.Monoid.Reflect
open import Tactic.Monoid.Proofs

monoidTactic : ∀ {a} {A : Set a} {MonA : Monoid A} {{_ : MonoidLaws A {{MonA}}}} → Tactic
monoidTactic {A = A} {dict} {{laws}} hole = do
  goal   ← inferNormalisedType hole
  `A     ← quoteTC A
  unify goal (def (quote _≡_) (hArg unknown ∷ hArg `A ∷ vArg unknown ∷ vArg unknown ∷ []))
    <|> do typeError $ strErr "Goal is not an equality" ∷ termErr goal ∷ []
  goal   ← normalise goal
  ensureNoMetas goal
  match  ← monoidMatcher dict
  `dict  ← quoteTC dict
  `laws  ← quoteTC laws
  ensureNoMetas `dict
  debugPrint "tactic.monoid" 20 $ strErr "monoidTactic" ∷ termErr goal ∷ strErr "dict =" ∷ termErr `dict ∷ []
  (lhs , rhs) , env ← parseGoal match goal
  unify hole (def (quote proof) (iArg `dict ∷ iArg `laws ∷ vArg (` lhs) ∷ vArg (` rhs) ∷
                                 vArg (quoteEnv `dict env) ∷ vArg (con (quote refl) []) ∷ []))
    <|> do typeError $ strErr "Can't prove" ∷ termErr (` lhs) ∷ strErr "==" ∷ termErr (` rhs)
                     ∷ strErr "because" ∷ termErr (` (flatten lhs)) ∷ strErr "/=" ∷ termErr (` (flatten rhs))
                     ∷ []

macro
  auto-monoid : ∀ {a} {A : Set a} {Mon : Monoid A} {{Laws : MonoidLaws A {{Mon}}}} → Tactic
  auto-monoid {{Laws}} = monoidTactic {{Laws}}

ext: agda

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --guardedness #-}

module Cubical.Codata.Conat where

open import Cubical.Codata.Conat.Base public

open import Cubical.Codata.Conat.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Linear monoidal closed structure for families
module SOAS.Families.Linear {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Sorting {T}
open import SOAS.Families.Core {T}
open import SOAS.Families.Isomorphism {T}

open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Closed
open import Categories.Functor.Bifunctor

-- | Monoidal tensor and unit

-- Linear tensor product that combines two families with two disjoint contexts
data _⊗_ (X Y : Family) : Ctx → Set where
  merge : (Γ Δ : Ctx) → X Γ → Y Δ → (X ⊗ Y) (Δ ∔ Γ)
infixr 20 _⊗_

pattern _⊹_ {Γ}{Δ} t s = merge Γ Δ t s
infix 30 _⊹_

-- ⊗ is a bifunctor
⊗F : Bifunctor 𝔽amilies 𝔽amilies 𝔽amilies
⊗F = record
  { F₀ = λ (X , Y) → X ⊗ Y
  ; F₁ = λ{ {X , Y}{X′ , Y′} (f , g) (x ⊹ y) → (f x) ⊹ (g y)}
  ; identity = λ{ {X , Y}{Γ}{x ⊹ y} → refl }
  ; homomorphism = λ{ {X , Y}{X′ , Y′}{X″ , Y″}{f , g}{f′ , g′}{Γ}{x ⊹ y} → refl }
  ; F-resp-≈ = λ{ (p₁ , p₂) {.(Δ ∔ Γ)} {merge Γ Δ t s} → cong₂ (merge Γ Δ) p₁ p₂ }
  }

_⊗̣_ : Familyₛ → Familyₛ → Familyₛ
_⊗̣_ = sorted₂ _⊗_

𝒚 : Ctx → Family
𝒚 Γ Δ = Γ ≡ Δ

-- Family which is only inhabited at the empty context
E : Family
E = 𝒚 ∅

-- Sorted family which is only inhabited at a singleton context
N : Familyₛ
N α = 𝒚 ⌈ α ⌋

-- | Monoidal exponential

-- Linear exponential between families
_⊸_ : Family → Family → Family
(X ⊸ Y) Γ = {Δ : Ctx} → X Δ → Y (Δ ∔ Γ)
infixr 15 _⊸_

-- Linear exponential between sorted families
_⊸∙_ : Familyₛ → Familyₛ → Familyₛ
_⊸∙_ = sorted₂ _⊸_
infixr 15 _⊸∙_

-- ⊸ is a bifunctor
⊸F : Bifunctor 𝔽am.op 𝔽amilies 𝔽amilies
⊸F = record
  { F₀ = λ (X , Y) → X ⊸ Y
  ; F₁ = λ{ {X , Y}{X′ , Y′} (f , g) e x → g (e (f x))}
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = λ{ {X , Y}{X′ , Y′}{f , g} (p₁ , p₂) {Γ}{e} →
                      dext′ (trans (cong (g ∘ e) p₁) p₂) }
  }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import Nat
open import Prelude
open import contexts

module core where
  -- types
  data htyp : Set where
    b     : htyp
    ⦇-⦈    : htyp
    _==>_ : htyp → htyp → htyp

  -- arrow type constructors bind very tightly
  infixr 25  _==>_

  -- external expressions
  data hexp : Set where
    c       : hexp
    _·:_    : hexp → htyp → hexp
    X       : Nat → hexp
    ·λ      : Nat → hexp → hexp
    ·λ_[_]_ : Nat → htyp → hexp → hexp
    ⦇-⦈[_]   : Nat → hexp
    ⦇⌜_⌟⦈[_]  : hexp → Nat → hexp
    _∘_     : hexp → hexp → hexp

  -- the type of type contexts, i.e. Γs in the judegments below
  tctx : Set
  tctx = htyp ctx

  mutual
    -- identity substitution, substitition environments
    data env : Set where
      Id : (Γ : tctx) → env
      Subst : (d : ihexp) → (y : Nat) → env → env

    -- internal expressions
    data ihexp : Set where
      c         : ihexp
      X         : Nat → ihexp
      ·λ_[_]_   : Nat → htyp → ihexp → ihexp
      ⦇-⦈⟨_⟩     : (Nat × env) → ihexp
      ⦇⌜_⌟⦈⟨_⟩    : ihexp → (Nat × env) → ihexp
      _∘_       : ihexp → ihexp → ihexp
      _⟨_⇒_⟩    : ihexp → htyp → htyp → ihexp
      _⟨_⇒⦇-⦈⇏_⟩ : ihexp → htyp → htyp → ihexp

  -- convenient notation for chaining together two agreeable casts
  _⟨_⇒_⇒_⟩ : ihexp → htyp → htyp → htyp → ihexp
  d ⟨ t1 ⇒ t2 ⇒ t3 ⟩ = d ⟨ t1 ⇒ t2 ⟩ ⟨ t2 ⇒ t3 ⟩

  -- type consistency
  data _~_ : (t1 t2 : htyp) → Set where
    TCRefl  : {τ : htyp} → τ ~ τ
    TCHole1 : {τ : htyp} → τ ~ ⦇-⦈
    TCHole2 : {τ : htyp} → ⦇-⦈ ~ τ
    TCArr   : {τ1 τ2 τ1' τ2' : htyp} →
               τ1 ~ τ1' →
               τ2 ~ τ2' →
               τ1 ==> τ2 ~ τ1' ==> τ2'

  -- type inconsistency
  data _~̸_ : (τ1 τ2 : htyp) → Set where
    ICBaseArr1 : {τ1 τ2 : htyp} → b ~̸ τ1 ==> τ2
    ICBaseArr2 : {τ1 τ2 : htyp} → τ1 ==> τ2 ~̸ b
    ICArr1 : {τ1 τ2 τ3 τ4 : htyp} →
               τ1 ~̸ τ3 →
               τ1 ==> τ2 ~̸ τ3 ==> τ4
    ICArr2 : {τ1 τ2 τ3 τ4 : htyp} →
               τ2 ~̸ τ4 →
               τ1 ==> τ2 ~̸ τ3 ==> τ4

  --- matching for arrows
  data _▸arr_ : htyp → htyp → Set where
    MAHole : ⦇-⦈ ▸arr ⦇-⦈ ==> ⦇-⦈
    MAArr  : {τ1 τ2 : htyp} → τ1 ==> τ2 ▸arr τ1 ==> τ2

  -- the type of hole contexts, i.e. Δs in the judgements
  hctx : Set
  hctx = (htyp ctx × htyp) ctx

  -- notation for a triple to match the CMTT syntax
  _::_[_] : Nat → htyp → tctx → (Nat × (tctx × htyp))
  u :: τ [ Γ ] = u , (Γ , τ)

  -- the hole name u does not appear in the term e
  data hole-name-new : (e : hexp) (u : Nat) → Set where
    HNConst : ∀{u} → hole-name-new c u
    HNAsc : ∀{e τ u} →
            hole-name-new e u →
            hole-name-new (e ·: τ) u
    HNVar : ∀{x u} → hole-name-new (X x) u
    HNLam1 : ∀{x e u} →
             hole-name-new e u →
             hole-name-new (·λ x e) u
    HNLam2 : ∀{x e u τ} →
             hole-name-new e u →
             hole-name-new (·λ x [ τ ] e) u
    HNHole : ∀{u u'} →
             u' ≠ u →
             hole-name-new (⦇-⦈[ u' ]) u
    HNNEHole : ∀{u u' e} →
               u' ≠ u →
               hole-name-new e u →
               hole-name-new (⦇⌜ e ⌟⦈[ u' ]) u
    HNAp : ∀{ u e1 e2 } →
           hole-name-new e1 u →
           hole-name-new e2 u →
           hole-name-new (e1 ∘ e2) u

  -- two terms that do not share any hole names
  data holes-disjoint : (e1 : hexp) → (e2 : hexp) → Set where
    HDConst : ∀{e} → holes-disjoint c e
    HDAsc : ∀{e1 e2 τ} → holes-disjoint e1 e2 → holes-disjoint (e1 ·: τ) e2
    HDVar : ∀{x e} → holes-disjoint (X x) e
    HDLam1 : ∀{x e1 e2} → holes-disjoint e1 e2 → holes-disjoint (·λ x e1) e2
    HDLam2 : ∀{x e1 e2 τ} → holes-disjoint e1 e2 → holes-disjoint (·λ x [ τ ] e1) e2
    HDHole : ∀{u e2} → hole-name-new e2 u → holes-disjoint (⦇-⦈[ u ]) e2
    HDNEHole : ∀{u e1 e2} → hole-name-new e2 u → holes-disjoint e1 e2 → holes-disjoint (⦇⌜ e1 ⌟⦈[ u ]) e2
    HDAp :  ∀{e1 e2 e3} → holes-disjoint e1 e3 → holes-disjoint e2 e3 → holes-disjoint (e1 ∘ e2) e3

  -- bidirectional type checking judgements for hexp
  mutual
    -- synthesis
    data _⊢_=>_ : (Γ : tctx) (e : hexp) (τ : htyp) → Set where
      SConst  : {Γ : tctx} → Γ ⊢ c => b
      SAsc    : {Γ : tctx} {e : hexp} {τ : htyp} →
                 Γ ⊢ e <= τ →
                 Γ ⊢ (e ·: τ) => τ
      SVar    : {Γ : tctx} {τ : htyp} {x : Nat} →
                 (x , τ) ∈ Γ →
                 Γ ⊢ X x => τ
      SAp     : {Γ : tctx} {e1 e2 : hexp} {τ τ1 τ2 : htyp} →
                 holes-disjoint e1 e2 →
                 Γ ⊢ e1 => τ1 →
                 τ1 ▸arr τ2 ==> τ →
                 Γ ⊢ e2 <= τ2 →
                 Γ ⊢ (e1 ∘ e2) => τ
      SEHole  : {Γ : tctx} {u : Nat} → Γ ⊢ ⦇-⦈[ u ] => ⦇-⦈
      SNEHole : {Γ : tctx} {e : hexp} {τ : htyp} {u : Nat} →
                 hole-name-new e u →
                 Γ ⊢ e => τ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] => ⦇-⦈
      SLam    : {Γ : tctx} {e : hexp} {τ1 τ2 : htyp} {x : Nat} →
                 x # Γ →
                 (Γ ,, (x , τ1)) ⊢ e => τ2 →
                 Γ ⊢ ·λ x [ τ1 ] e => τ1 ==> τ2

    -- analysis
    data _⊢_<=_ : (Γ : htyp ctx) (e : hexp) (τ : htyp) → Set where
      ASubsume : {Γ : tctx} {e : hexp} {τ τ' : htyp} →
                 Γ ⊢ e => τ' →
                 τ ~ τ' →
                 Γ ⊢ e <= τ
      ALam : {Γ : tctx} {e : hexp} {τ τ1 τ2 : htyp} {x : Nat} →
                 x # Γ →
                 τ ▸arr τ1 ==> τ2 →
                 (Γ ,, (x , τ1)) ⊢ e <= τ2 →
                 Γ ⊢ (·λ x e) <= τ

  -- those types without holes
  data _tcomplete : htyp → Set where
    TCBase : b tcomplete
    TCArr : ∀{τ1 τ2} → τ1 tcomplete → τ2 tcomplete → (τ1 ==> τ2) tcomplete

  -- those external expressions without holes
  data _ecomplete : hexp → Set where
    ECConst : c ecomplete
    ECAsc : ∀{τ e} → τ tcomplete → e ecomplete → (e ·: τ) ecomplete
    ECVar : ∀{x} → (X x) ecomplete
    ECLam1 : ∀{x e} → e ecomplete → (·λ x e) ecomplete
    ECLam2 : ∀{x e τ} → e ecomplete → τ tcomplete → (·λ x [ τ ] e) ecomplete
    ECAp : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → (e1 ∘ e2) ecomplete

  -- those internal expressions without holes
  data _dcomplete : ihexp → Set where
    DCVar : ∀{x} → (X x) dcomplete
    DCConst : c dcomplete
    DCLam : ∀{x τ d} → d dcomplete → τ tcomplete → (·λ x [ τ ] d) dcomplete
    DCAp : ∀{d1 d2} → d1 dcomplete → d2 dcomplete → (d1 ∘ d2) dcomplete
    DCCast : ∀{d τ1 τ2} → d dcomplete → τ1 tcomplete → τ2 tcomplete → (d ⟨ τ1 ⇒ τ2 ⟩) dcomplete

  -- contexts that only produce complete types
  _gcomplete : tctx → Set
  Γ gcomplete = (x : Nat) (τ : htyp) → (x , τ) ∈ Γ → τ tcomplete

  -- those internal expressions where every cast is the identity cast and
  -- there are no failed casts
  data cast-id : ihexp → Set where
    CIConst  : cast-id c
    CIVar    : ∀{x} → cast-id (X x)
    CILam    : ∀{x τ d} → cast-id d → cast-id (·λ x [ τ ] d)
    CIHole   : ∀{u} → cast-id (⦇-⦈⟨ u ⟩)
    CINEHole : ∀{d u} → cast-id d → cast-id (⦇⌜ d ⌟⦈⟨ u ⟩)
    CIAp     : ∀{d1 d2} → cast-id d1 → cast-id d2 → cast-id (d1 ∘ d2)
    CICast   : ∀{d τ} → cast-id d → cast-id (d ⟨ τ ⇒ τ ⟩)

  -- expansion
  mutual
    -- synthesis
    data _⊢_⇒_~>_⊣_ : (Γ : tctx) (e : hexp) (τ : htyp) (d : ihexp) (Δ : hctx) → Set where
      ESConst : ∀{Γ} → Γ ⊢ c ⇒ b ~> c ⊣ ∅
      ESVar   : ∀{Γ x τ} → (x , τ) ∈ Γ →
                         Γ ⊢ X x ⇒ τ ~> X x ⊣ ∅
      ESLam   : ∀{Γ x τ1 τ2 e d Δ } →
                     (x # Γ) →
                     (Γ ,, (x , τ1)) ⊢ e ⇒ τ2 ~> d ⊣ Δ →
                      Γ ⊢ ·λ x [ τ1 ] e ⇒ (τ1 ==> τ2) ~> ·λ x [ τ1 ] d ⊣ Δ
      ESAp : ∀{Γ e1 τ τ1 τ1' τ2 τ2' d1 Δ1 e2 d2 Δ2 } →
              holes-disjoint e1 e2 →
              Δ1 ## Δ2 →
              Γ ⊢ e1 => τ1 →
              τ1 ▸arr τ2 ==> τ →
              Γ ⊢ e1 ⇐ (τ2 ==> τ) ~> d1 :: τ1' ⊣ Δ1 →
              Γ ⊢ e2 ⇐ τ2 ~> d2 :: τ2' ⊣ Δ2 →
              Γ ⊢ e1 ∘ e2 ⇒ τ ~> (d1 ⟨ τ1' ⇒ τ2 ==> τ ⟩) ∘ (d2 ⟨ τ2' ⇒ τ2 ⟩) ⊣ (Δ1 ∪ Δ2)
      ESEHole : ∀{ Γ u } →
                Γ ⊢ ⦇-⦈[ u ] ⇒ ⦇-⦈ ~> ⦇-⦈⟨ u , Id Γ ⟩ ⊣  ■ (u :: ⦇-⦈ [ Γ ])
      ESNEHole : ∀{ Γ e τ d u Δ } →
                 Δ ## (■ (u , Γ , ⦇-⦈)) →
                 Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] ⇒ ⦇-⦈ ~> ⦇⌜ d ⌟⦈⟨ u , Id Γ  ⟩ ⊣ (Δ ,, u :: ⦇-⦈ [ Γ ])
      ESAsc : ∀ {Γ e τ d τ' Δ} →
                 Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                 Γ ⊢ (e ·: τ) ⇒ τ ~> d ⟨ τ' ⇒ τ ⟩ ⊣ Δ

    -- analysis
    data _⊢_⇐_~>_::_⊣_ : (Γ : tctx) (e : hexp) (τ : htyp) (d : ihexp) (τ' : htyp) (Δ : hctx) → Set where
      EALam : ∀{Γ x τ τ1 τ2 e d τ2' Δ } →
              (x # Γ) →
              τ ▸arr τ1 ==> τ2 →
              (Γ ,, (x , τ1)) ⊢ e ⇐ τ2 ~> d :: τ2' ⊣ Δ →
              Γ ⊢ ·λ x e ⇐ τ ~> ·λ x [ τ1 ] d :: τ1 ==> τ2' ⊣ Δ
      EASubsume : ∀{e Γ τ' d Δ τ} →
                  ((u : Nat) → e ≠ ⦇-⦈[ u ]) →
                  ((e' : hexp) (u : Nat) → e ≠ ⦇⌜ e' ⌟⦈[ u ]) →
                  Γ ⊢ e ⇒ τ' ~> d ⊣ Δ →
                  τ ~ τ' →
                  Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ
      EAEHole : ∀{ Γ u τ  } →
                Γ ⊢ ⦇-⦈[ u ] ⇐ τ ~> ⦇-⦈⟨ u , Id Γ  ⟩ :: τ ⊣ ■ (u :: τ [ Γ ])
      EANEHole : ∀{ Γ e u τ d τ' Δ  } →
                 Δ ## (■ (u , Γ , τ)) →
                 Γ ⊢ e ⇒ τ' ~> d ⊣ Δ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] ⇐ τ ~> ⦇⌜ d ⌟⦈⟨ u , Id Γ  ⟩ :: τ ⊣ (Δ ,, u :: τ [ Γ ])

  -- ground types
  data _ground : (τ : htyp) → Set where
    GBase : b ground
    GHole : ⦇-⦈ ==> ⦇-⦈ ground

  mutual
    -- substitution typing
    data _,_⊢_:s:_ : hctx → tctx → env → tctx → Set where
      STAId : ∀{Γ Γ' Δ} →
                  ((x : Nat) (τ : htyp) → (x , τ) ∈ Γ' → (x , τ) ∈ Γ) →
                  Δ , Γ ⊢ Id Γ' :s: Γ'
      STASubst : ∀{Γ Δ σ y Γ' d τ } →
               Δ , Γ ,, (y , τ) ⊢ σ :s: Γ' →
               Δ , Γ ⊢ d :: τ →
               Δ , Γ ⊢ Subst d y σ :s: Γ'

    -- type assignment
    data _,_⊢_::_ : (Δ : hctx) (Γ : tctx) (d : ihexp) (τ : htyp) → Set where
      TAConst : ∀{Δ Γ} → Δ , Γ ⊢ c :: b
      TAVar : ∀{Δ Γ x τ} → (x , τ) ∈ Γ → Δ , Γ ⊢ X x :: τ
      TALam : ∀{ Δ Γ x τ1 d τ2} →
              x # Γ →
              Δ , (Γ ,, (x , τ1)) ⊢ d :: τ2 →
              Δ , Γ ⊢ ·λ x [ τ1 ] d :: (τ1 ==> τ2)
      TAAp : ∀{ Δ Γ d1 d2 τ1 τ} →
             Δ , Γ ⊢ d1 :: τ1 ==> τ →
             Δ , Γ ⊢ d2 :: τ1 →
             Δ , Γ ⊢ d1 ∘ d2 :: τ
      TAEHole : ∀{ Δ Γ σ u Γ' τ} →
                (u , (Γ' , τ)) ∈ Δ →
                Δ , Γ ⊢ σ :s: Γ' →
                Δ , Γ ⊢ ⦇-⦈⟨ u , σ ⟩ :: τ
      TANEHole : ∀ { Δ Γ d τ' Γ' u σ τ } →
                 (u , (Γ' , τ)) ∈ Δ →
                 Δ , Γ ⊢ d :: τ' →
                 Δ , Γ ⊢ σ :s: Γ' →
                 Δ , Γ ⊢ ⦇⌜ d ⌟⦈⟨ u , σ ⟩ :: τ
      TACast : ∀{ Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 →
             τ1 ~ τ2 →
             Δ , Γ ⊢ d ⟨ τ1 ⇒ τ2 ⟩ :: τ2
      TAFailedCast : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 →
             τ1 ground →
             τ2 ground →
             τ1 ≠ τ2 →
             Δ , Γ ⊢ d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩ :: τ2

  -- substitution
  [_/_]_ : ihexp → Nat → ihexp → ihexp
  [ d / y ] c = c
  [ d / y ] X x
    with natEQ x y
  [ d / y ] X .y | Inl refl = d
  [ d / y ] X x  | Inr neq = X x
  [ d / y ] (·λ x [ x₁ ] d')
    with natEQ x y
  [ d / y ] (·λ .y [ τ ] d') | Inl refl = ·λ y [ τ ] d'
  [ d / y ] (·λ x [ τ ] d')  | Inr x₁ = ·λ x [ τ ] ( [ d / y ] d')
  [ d / y ] ⦇-⦈⟨ u , σ ⟩ = ⦇-⦈⟨ u , Subst d y σ ⟩
  [ d / y ] ⦇⌜ d' ⌟⦈⟨ u , σ  ⟩ =  ⦇⌜ [ d / y ] d' ⌟⦈⟨ u , Subst d y σ ⟩
  [ d / y ] (d1 ∘ d2) = ([ d / y ] d1) ∘ ([ d / y ] d2)
  [ d / y ] (d' ⟨ τ1 ⇒ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒ τ2 ⟩
  [ d / y ] (d' ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩

  -- applying an environment to an expression
  apply-env : env → ihexp → ihexp
  apply-env (Id Γ) d = d
  apply-env (Subst d y σ) d' = [ d / y ] ( apply-env σ d')

  -- values
  data _val : (d : ihexp) → Set where
    VConst : c val
    VLam   : ∀{x τ d} → (·λ x [ τ ] d) val

  -- boxed values
  data _boxedval : (d : ihexp) → Set where
    BVVal : ∀{d} → d val → d boxedval
    BVArrCast : ∀{ d τ1 τ2 τ3 τ4 } →
                τ1 ==> τ2 ≠ τ3 ==> τ4 →
                d boxedval →
                d ⟨ (τ1 ==> τ2) ⇒ (τ3 ==> τ4) ⟩ boxedval
    BVHoleCast : ∀{ τ d } → τ ground → d boxedval → d ⟨ τ ⇒ ⦇-⦈ ⟩ boxedval

  mutual
    -- indeterminate forms
    data _indet : (d : ihexp) → Set where
      IEHole : ∀{u σ} → ⦇-⦈⟨ u , σ ⟩ indet
      INEHole : ∀{d u σ} → d final → ⦇⌜ d ⌟⦈⟨ u , σ ⟩ indet
      IAp : ∀{d1 d2} → ((τ1 τ2 τ3 τ4 : htyp) (d1' : ihexp) →
                       d1 ≠ (d1' ⟨(τ1 ==> τ2) ⇒ (τ3 ==> τ4)⟩)) →
                       d1 indet →
                       d2 final →
                       (d1 ∘ d2) indet
      ICastArr : ∀{d τ1 τ2 τ3 τ4} →
                 τ1 ==> τ2 ≠ τ3 ==> τ4 →
                 d indet →
                 d ⟨ (τ1 ==> τ2) ⇒ (τ3 ==> τ4) ⟩ indet
      ICastGroundHole : ∀{ τ d } →
                        τ ground →
                        d indet →
                        d ⟨ τ ⇒  ⦇-⦈ ⟩ indet
      ICastHoleGround : ∀ { d τ } →
                        ((d' : ihexp) (τ' : htyp) → d ≠ (d' ⟨ τ' ⇒ ⦇-⦈ ⟩)) →
                        d indet →
                        τ ground →
                        d ⟨ ⦇-⦈ ⇒ τ ⟩ indet
      IFailedCast : ∀{ d τ1 τ2 } →
                    d final →
                    τ1 ground →
                    τ2 ground →
                    τ1 ≠ τ2 →
                    d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩ indet

    -- final expressions
    data _final : (d : ihexp) → Set where
      FBoxedVal : ∀{d} → d boxedval → d final
      FIndet    : ∀{d} → d indet    → d final

  -- contextual dynamics

  -- evaluation contexts
  data ectx : Set where
    ⊙ : ectx
    _∘₁_ : ectx → ihexp → ectx
    _∘₂_ : ihexp → ectx → ectx
    ⦇⌜_⌟⦈⟨_⟩ : ectx → (Nat × env ) → ectx
    _⟨_⇒_⟩ : ectx → htyp → htyp → ectx
    _⟨_⇒⦇-⦈⇏_⟩ : ectx → htyp → htyp → ectx

  -- note: this judgement is redundant: in the absence of the premises in
  -- the red brackets, all syntactically well formed ectxs are valid. with
  -- finality premises, that's not true, and that would propagate through
  -- additions to the calculus. so we leave it here for clarity but note
  -- that, as written, in any use case its either trival to prove or
  -- provides no additional information

   --ε is an evaluation context
  data _evalctx : (ε : ectx) → Set where
    ECDot : ⊙ evalctx
    ECAp1 : ∀{d ε} →
            ε evalctx →
            (ε ∘₁ d) evalctx
    ECAp2 : ∀{d ε} →
            -- d final → -- red brackets
            ε evalctx →
            (d ∘₂ ε) evalctx
    ECNEHole : ∀{ε u σ} →
               ε evalctx →
               ⦇⌜ ε ⌟⦈⟨ u , σ ⟩ evalctx
    ECCast : ∀{ ε τ1 τ2} →
             ε evalctx →
             (ε ⟨ τ1 ⇒ τ2 ⟩) evalctx
    ECFailedCast : ∀{ ε τ1 τ2 } →
                   ε evalctx →
                   ε ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩ evalctx

  -- d is the result of filling the hole in ε with d'
  data _==_⟦_⟧ : (d : ihexp) (ε : ectx) (d' : ihexp) → Set where
    FHOuter : ∀{d} → d == ⊙ ⟦ d ⟧
    FHAp1 : ∀{d1 d1' d2 ε} →
           d1 == ε ⟦ d1' ⟧ →
           (d1 ∘ d2) == (ε ∘₁ d2) ⟦ d1' ⟧
    FHAp2 : ∀{d1 d2 d2' ε} →
           -- d1 final → -- red brackets
           d2 == ε ⟦ d2' ⟧ →
           (d1 ∘ d2) == (d1 ∘₂ ε) ⟦ d2' ⟧
    FHNEHole : ∀{ d d' ε u σ} →
              d == ε ⟦ d' ⟧ →
              ⦇⌜ d ⌟⦈⟨ (u , σ ) ⟩ ==  ⦇⌜ ε ⌟⦈⟨ (u , σ ) ⟩ ⟦ d' ⟧
    FHCast : ∀{ d d' ε τ1 τ2 } →
            d == ε ⟦ d' ⟧ →
            d ⟨ τ1 ⇒ τ2 ⟩ == ε ⟨ τ1 ⇒ τ2 ⟩ ⟦ d' ⟧
    FHFailedCast : ∀{ d d' ε τ1 τ2} →
            d == ε ⟦ d' ⟧ →
            (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) == (ε ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) ⟦ d' ⟧

  -- matched ground types
  data _▸gnd_ : htyp → htyp → Set where
    MGArr : ∀{τ1 τ2} →
            (τ1 ==> τ2) ≠ (⦇-⦈ ==> ⦇-⦈) →
            (τ1 ==> τ2) ▸gnd (⦇-⦈ ==> ⦇-⦈)

  -- instruction transition judgement
  data _→>_ : (d d' : ihexp) → Set where
    ITLam : ∀{ x τ d1 d2 } →
            -- d2 final → -- red brackets
            ((·λ x [ τ ] d1) ∘ d2) →> ([ d2 / x ] d1)
    ITCastID : ∀{d τ } →
               -- d final → -- red brackets
               (d ⟨ τ ⇒ τ ⟩) →> d
    ITCastSucceed : ∀{d τ } →
                    -- d final → -- red brackets
                    τ ground →
                    (d ⟨ τ ⇒ ⦇-⦈ ⇒ τ ⟩) →> d
    ITCastFail : ∀{ d τ1 τ2} →
                 -- d final → -- red brackets
                 τ1 ground →
                 τ2 ground →
                 τ1 ≠ τ2 →
                 (d ⟨ τ1 ⇒ ⦇-⦈ ⇒ τ2 ⟩) →> (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)
    ITApCast : ∀{d1 d2 τ1 τ2 τ1' τ2' } →
               -- d1 final → -- red brackets
               -- d2 final → -- red brackets
               ((d1 ⟨ (τ1 ==> τ2) ⇒ (τ1' ==> τ2')⟩) ∘ d2) →> ((d1 ∘ (d2 ⟨ τ1' ⇒ τ1 ⟩)) ⟨ τ2 ⇒ τ2' ⟩)
    ITGround : ∀{ d τ τ'} →
               -- d final → -- red brackets
               τ ▸gnd τ' →
               (d ⟨ τ ⇒ ⦇-⦈ ⟩) →> (d ⟨ τ ⇒ τ' ⇒ ⦇-⦈ ⟩)
    ITExpand : ∀{d τ τ' } →
               -- d final → -- red brackets
               τ ▸gnd τ' →
               (d ⟨ ⦇-⦈ ⇒ τ ⟩) →> (d ⟨ ⦇-⦈ ⇒ τ' ⇒ τ ⟩)

  -- single step (in contextual evaluation sense)
  data _↦_ : (d d' : ihexp) → Set where
    Step : ∀{ d d0 d' d0' ε} →
           d == ε ⟦ d0 ⟧ →
           d0 →> d0' →
           d' == ε ⟦ d0' ⟧ →
           d ↦ d'

  -- reflexive transitive closure of single steps into multi steps
  data _↦*_ : (d d' : ihexp) → Set where
    MSRefl : ∀{d} → d ↦* d
    MSStep : ∀{d d' d''} →
                 d ↦ d' →
                 d' ↦* d'' →
                 d  ↦* d''

  -- freshness
  mutual
    -- ... with respect to a hole context
    data envfresh : Nat → env → Set where
      EFId : ∀{x Γ} → x # Γ → envfresh x (Id Γ)
      EFSubst : ∀{x d σ y} → fresh x d
                           → envfresh x σ
                           → x ≠ y
                           → envfresh x (Subst d y σ)

    -- ... for inernal expressions
    data fresh : Nat → ihexp → Set where
      FConst : ∀{x} → fresh x c
      FVar   : ∀{x y} → x ≠ y → fresh x (X y)
      FLam   : ∀{x y τ d} → x ≠ y → fresh x d → fresh x (·λ y [ τ ] d)
      FHole  : ∀{x u σ} → envfresh x σ → fresh x (⦇-⦈⟨ u , σ ⟩)
      FNEHole : ∀{x d u σ} → envfresh x σ → fresh x d → fresh x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      FAp     : ∀{x d1 d2} → fresh x d1 → fresh x d2 → fresh x (d1 ∘ d2)
      FCast   : ∀{x d τ1 τ2} → fresh x d → fresh x (d ⟨ τ1 ⇒ τ2 ⟩)
      FFailedCast : ∀{x d τ1 τ2} → fresh x d → fresh x (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)

  -- ... for external expressions
  data freshh : Nat → hexp → Set where
    FRHConst : ∀{x} → freshh x c
    FRHAsc   : ∀{x e τ} → freshh x e → freshh x (e ·: τ)
    FRHVar   : ∀{x y} → x ≠ y → freshh x (X y)
    FRHLam1  : ∀{x y e} → x ≠ y → freshh x e → freshh x (·λ y e)
    FRHLam2  : ∀{x τ e y} → x ≠ y → freshh x e → freshh x (·λ y [ τ ] e)
    FRHEHole : ∀{x u} → freshh x (⦇-⦈[ u ])
    FRHNEHole : ∀{x u e} → freshh x e → freshh x (⦇⌜ e ⌟⦈[ u ])
    FRHAp : ∀{x e1 e2} → freshh x e1 → freshh x e2 → freshh x (e1 ∘ e2)

  -- x is not used in a binding site in d
  mutual
    data unbound-in-σ : Nat → env → Set where
      UBσId : ∀{x Γ} → unbound-in-σ x (Id Γ)
      UBσSubst : ∀{x d y σ} → unbound-in x d
                            → unbound-in-σ x σ
                            → x ≠ y
                            → unbound-in-σ x (Subst d y σ)

    data unbound-in : (x : Nat) (d : ihexp) → Set where
      UBConst : ∀{x} → unbound-in x c
      UBVar : ∀{x y} → unbound-in x (X y)
      UBLam2 : ∀{x d y τ} → x ≠ y
                           → unbound-in x d
                           → unbound-in x (·λ_[_]_ y τ d)
      UBHole : ∀{x u σ} → unbound-in-σ x σ
                         → unbound-in x (⦇-⦈⟨ u , σ ⟩)
      UBNEHole : ∀{x u σ d }
                  → unbound-in-σ x σ
                  → unbound-in x d
                  → unbound-in x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      UBAp : ∀{ x d1 d2 } →
            unbound-in x d1 →
            unbound-in x d2 →
            unbound-in x (d1 ∘ d2)
      UBCast : ∀{x d τ1 τ2} → unbound-in x d → unbound-in x (d ⟨ τ1 ⇒ τ2 ⟩)
      UBFailedCast : ∀{x d τ1 τ2} → unbound-in x d → unbound-in x (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)

  mutual
    data binders-disjoint-σ : env → ihexp → Set where
      BDσId : ∀{Γ d} → binders-disjoint-σ (Id Γ) d
      BDσSubst : ∀{d1 d2 y σ} → binders-disjoint d1 d2
                              → binders-disjoint-σ σ d2
                              → binders-disjoint-σ (Subst d1 y σ) d2

    -- two terms that do not share any binders
    data binders-disjoint : (d1 : ihexp) → (d2 : ihexp) → Set where
      BDConst : ∀{d} → binders-disjoint c d
      BDVar : ∀{x d} → binders-disjoint (X x) d
      BDLam : ∀{x τ d1 d2} → binders-disjoint d1 d2
                            → unbound-in x d2
                            → binders-disjoint (·λ_[_]_ x τ d1) d2
      BDHole : ∀{u σ d2} → binders-disjoint-σ σ d2
                         → binders-disjoint (⦇-⦈⟨ u , σ ⟩) d2
      BDNEHole : ∀{u σ d1 d2} → binders-disjoint-σ σ d2
                              → binders-disjoint d1 d2
                              → binders-disjoint (⦇⌜ d1 ⌟⦈⟨ u , σ ⟩) d2
      BDAp :  ∀{d1 d2 d3} → binders-disjoint d1 d3
                          → binders-disjoint d2 d3
                          → binders-disjoint (d1 ∘ d2) d3
      BDCast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint (d1 ⟨ τ1 ⇒ τ2 ⟩) d2
      BDFailedCast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint (d1 ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) d2

  mutual
  -- each term has to be binders unique, and they have to be pairwise
  -- disjoint with the collection of bound vars
    data binders-unique-σ : env → Set where
      BUσId : ∀{Γ} → binders-unique-σ (Id Γ)
      BUσSubst : ∀{d y σ} → binders-unique d
                          → binders-unique-σ σ
                          → binders-disjoint-σ σ d
                          → binders-unique-σ (Subst d y σ)

    -- all the variable names in the term are unique
    data binders-unique : ihexp → Set where
      BUHole : binders-unique c
      BUVar : ∀{x} → binders-unique (X x)
      BULam : {x : Nat} {τ : htyp} {d : ihexp} → binders-unique d
                                                → unbound-in x d
                                                → binders-unique (·λ_[_]_ x τ d)
      BUEHole : ∀{u σ} → binders-unique-σ σ
                        → binders-unique (⦇-⦈⟨ u , σ ⟩)
      BUNEHole : ∀{u σ d} → binders-unique d
                           → binders-unique-σ σ
                           → binders-unique (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      BUAp : ∀{d1 d2} → binders-unique d1
                       → binders-unique d2
                       → binders-disjoint d1 d2
                       → binders-unique (d1 ∘ d2)
      BUCast : ∀{d τ1 τ2} → binders-unique d
                           → binders-unique (d ⟨ τ1 ⇒ τ2 ⟩)
      BUFailedCast : ∀{d τ1 τ2} → binders-unique d
                                 → binders-unique (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

module Luau.TypeCheck where

open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (Maybe; just)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_; src; tgt)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import FFI.Data.Vector using (Vector)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Properties.Product using (_×_; _,_)

orUnknown : Maybe Type → Type
orUnknown nothing = unknown
orUnknown (just T) = T

srcBinOp : BinaryOperator → Type
srcBinOp + = number
srcBinOp - = number
srcBinOp * = number
srcBinOp / = number
srcBinOp < = number
srcBinOp > = number
srcBinOp == = unknown
srcBinOp ~= = unknown
srcBinOp <= = number
srcBinOp >= = number
srcBinOp ·· = string

tgtBinOp : BinaryOperator → Type
tgtBinOp + = number
tgtBinOp - = number
tgtBinOp * = number
tgtBinOp / = number
tgtBinOp < = boolean
tgtBinOp > = boolean
tgtBinOp == = boolean
tgtBinOp ~= = boolean
tgtBinOp <= = boolean
tgtBinOp >= = boolean
tgtBinOp ·· = string

data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set
data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set

data _⊢ᴮ_∈_ where

  done : ∀ {Γ} →

    ---------------
    Γ ⊢ᴮ done ∈ nil

  return : ∀ {M B T U Γ} →

    Γ ⊢ᴱ M ∈ T →
    Γ ⊢ᴮ B ∈ U →
    ---------------------
    Γ ⊢ᴮ return M ∙ B ∈ T

  local : ∀ {x M B T U V Γ} →

    Γ ⊢ᴱ M ∈ U →
    (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V →
    --------------------------------
    Γ ⊢ᴮ local var x ∈ T ← M ∙ B ∈ V

  function : ∀ {f x B C T U V W Γ} →

    (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V →
    (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W →
    -------------------------------------------------
    Γ ⊢ᴮ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W

data _⊢ᴱ_∈_ where

  nil : ∀ {Γ} →

    --------------------
    Γ ⊢ᴱ (val nil) ∈ nil

  var : ∀ {x T Γ} →

    T ≡ orUnknown(Γ [ x ]ⱽ) →
    ----------------
    Γ ⊢ᴱ (var x) ∈ T

  addr : ∀ {a Γ} T →

    -----------------
    Γ ⊢ᴱ val(addr a) ∈ T

  number : ∀ {n Γ} →

    ---------------------------
    Γ ⊢ᴱ val(number n) ∈ number

  bool : ∀ {b Γ} →

    --------------------------
    Γ ⊢ᴱ val(bool b) ∈ boolean

  string : ∀ {x Γ} →

    ---------------------------
    Γ ⊢ᴱ val(string x) ∈ string

  app : ∀ {M N T U Γ} →

    Γ ⊢ᴱ M ∈ T →
    Γ ⊢ᴱ N ∈ U →
    ----------------------
    Γ ⊢ᴱ (M $ N) ∈ (tgt T)

  function : ∀ {f x B T U V Γ} →

    (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V →
    -----------------------------------------------------
    Γ ⊢ᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U)

  block : ∀ {b B T U Γ} →

    Γ ⊢ᴮ B ∈ U →
    ------------------------------------
    Γ ⊢ᴱ (block var b ∈ T is B end) ∈ T

  binexp : ∀ {op Γ M N T U} →

    Γ ⊢ᴱ M ∈ T →
    Γ ⊢ᴱ N ∈ U →
    ----------------------------------
    Γ ⊢ᴱ (binexp M op N) ∈ tgtBinOp op

data ⊢ᴼ_ : Maybe(Object yes) → Set where

  nothing :

    ---------
    ⊢ᴼ nothing

  function : ∀ {f x T U V B} →

    (x ↦ T) ⊢ᴮ B ∈ V →
    ----------------------------------------------
    ⊢ᴼ (just function f ⟨ var x ∈ T ⟩∈ U is B end)

⊢ᴴ_ : Heap yes → Set
⊢ᴴ H = ∀ a {O} → (H [ a ]ᴴ ≡ O) → (⊢ᴼ O)

_⊢ᴴᴱ_▷_∈_ : VarCtxt → Heap yes → Expr yes → Type → Set
(Γ ⊢ᴴᴱ H ▷ M ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴱ M ∈ T)

_⊢ᴴᴮ_▷_∈_ : VarCtxt → Heap yes → Block yes → Type → Set
(Γ ⊢ᴴᴮ H ▷ B ∈ T) = (⊢ᴴ H) × (Γ ⊢ᴮ B ∈ T)

max_stars_repo_name: MeltzDev/luau

max_issues_repo_name: MeltzDev/luau

max_forks_repo_name: MeltzDev/luau


text:
module Pi.Syntax where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

infixr 12 _×ᵤ_
infixr 11 _+ᵤ_
infixr 50 _⨾_
infixr 10 _↔_
infix  99 !_

-- Types
data 𝕌 : Set where
  𝟘       : 𝕌
  𝟙       : 𝕌
  _+ᵤ_    : 𝕌 → 𝕌 → 𝕌
  _×ᵤ_    : 𝕌 → 𝕌 → 𝕌

⟦_⟧ : (A : 𝕌) → Set
⟦ 𝟘 ⟧ = ⊥
⟦ 𝟙 ⟧ = ⊤
⟦ t₁ +ᵤ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ t₁ ×ᵤ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

-- Combinators
data _↔_ : 𝕌 → 𝕌 → Set where
  unite₊l  : {t : 𝕌} → 𝟘 +ᵤ t ↔ t
  uniti₊l  : {t : 𝕌} → t ↔ 𝟘 +ᵤ t
  swap₊    : {t₁ t₂ : 𝕌} → t₁ +ᵤ t₂ ↔ t₂ +ᵤ t₁
  assocl₊  : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤ (t₂ +ᵤ t₃) ↔ (t₁ +ᵤ t₂) +ᵤ t₃
  assocr₊  : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) +ᵤ t₃ ↔ t₁ +ᵤ (t₂ +ᵤ t₃)
  unite⋆l  : {t : 𝕌} → 𝟙 ×ᵤ t ↔ t
  uniti⋆l  : {t : 𝕌} → t ↔ 𝟙 ×ᵤ t
  swap⋆    : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ↔ t₂ ×ᵤ t₁
  assocl⋆  : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ↔ (t₁ ×ᵤ t₂) ×ᵤ t₃
  assocr⋆  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ↔ t₁ ×ᵤ (t₂ ×ᵤ t₃)
  absorbr  : {t : 𝕌} → 𝟘 ×ᵤ t ↔ 𝟘
  factorzl : {t : 𝕌} → 𝟘 ↔ 𝟘 ×ᵤ t
  dist     : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) ×ᵤ t₃ ↔ (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃)
  factor   : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃) ↔ (t₁ +ᵤ t₂) ×ᵤ t₃
  id↔      : {t : 𝕌} → t ↔ t
  _⨾_      : {t₁ t₂ t₃ : 𝕌} → (t₁ ↔ t₂) → (t₂ ↔ t₃) → (t₁ ↔ t₃)
  _⊕_      : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ↔ t₃) → (t₂ ↔ t₄) → (t₁ +ᵤ t₂ ↔ t₃ +ᵤ t₄)
  _⊗_      : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ↔ t₃) → (t₂ ↔ t₄) → (t₁ ×ᵤ t₂ ↔ t₃ ×ᵤ t₄)

-- Some useful combinators
unite₊r  : {t : 𝕌} → t +ᵤ 𝟘 ↔ t
unite₊r  = swap₊ ⨾ unite₊l

uniti₊r  : {t : 𝕌} → t ↔ t +ᵤ 𝟘
uniti₊r  = uniti₊l ⨾ swap₊

unite⋆r  : {t : 𝕌} → t ×ᵤ 𝟙 ↔ t
unite⋆r  = swap⋆ ⨾ unite⋆l

uniti⋆r  : {t : 𝕌} → t ↔ t ×ᵤ 𝟙
uniti⋆r  = uniti⋆l ⨾ swap⋆

absorbl  : {t : 𝕌} → t ×ᵤ 𝟘 ↔ 𝟘
absorbl  = swap⋆ ⨾ absorbr

factorzr : {t : 𝕌} → 𝟘 ↔ t ×ᵤ 𝟘
factorzr = factorzl ⨾ swap⋆

distl    : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤ t₃) ↔ (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)
distl    = swap⋆ ⨾ dist ⨾ (swap⋆ ⊕ swap⋆)

factorl  : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃) ↔ t₁ ×ᵤ (t₂ +ᵤ t₃)
factorl  = (swap⋆ ⊕ swap⋆) ⨾ factor ⨾ swap⋆

-- Inverses of combinators
!_ : {A B : 𝕌} → A ↔ B → B ↔ A
! unite₊l = uniti₊l
! uniti₊l = unite₊l
! swap₊ = swap₊
! assocl₊ = assocr₊
! assocr₊ = assocl₊
! unite⋆l = uniti⋆l
! uniti⋆l = unite⋆l
! swap⋆ = swap⋆
! assocl⋆ = assocr⋆
! assocr⋆ = assocl⋆
! absorbr = factorzl
! factorzl = absorbr
! dist = factor
! factor = dist
! id↔ = id↔
! (c₁ ⨾ c₂) = ! c₂ ⨾ ! c₁
! (c₁ ⊕ c₂) = (! c₁) ⊕ (! c₂)
! (c₁ ⊗ c₂) = (! c₁) ⊗ (! c₂)


text:
module Automata.Nondeterministic where

-- Standard libraries imports ----------------------------------------
open import Level using ()
  renaming (zero to ℓ₀)

open import Data.Nat using (ℕ)
open import Data.Product using (_×_)
open import Data.Vec using (Vec ; [] ; _∷_)

open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality using (_≡_)
----------------------------------------------------------------------

-- Thesis imports ----------------------------------------------------
open import Utilities.ExistsSyntax using (∃-syntax)
----------------------------------------------------------------------

record NDA (Σ : Set) : Set₁ where
  constructor ⟨_,_,_,_⟩

  field
    Q : Set
    S : Pred Q ℓ₀
    F : Pred Q ℓ₀
    Δ : Q → Σ → Pred Q ℓ₀

  Δ* : Q → {n : ℕ} → Vec Σ n → Pred Q ℓ₀
  Δ* q [] = q ≡_
  Δ* q (x ∷ xs) q′ = ∃ q₀ ∶ Q • ((Δ q x q₀) × (Δ* q₀ xs q′))

  Accepts : {n : ℕ} → Pred (Vec Σ n) ℓ₀
  Accepts xs = ∃ q ∶ Q • (S q
                       × ∃ q′ ∶ Q • ((F q′)
                                  × (Δ* q xs q′)))

  -- :TODO: are these useful?
  _-Reachable : ℕ → Q → Pred Q ℓ₀
  _-Reachable n q q′ = ∃ xs ∶ Vec Σ n • (Δ* q xs q′)

  Reachable : Q → Pred Q ℓ₀
  Reachable q q′ = ∃ n ∶ ℕ • (n -Reachable) q q′

max_stars_repo_name: armkeh/agda-computability

max_issues_repo_name: armkeh/agda-computability

max_forks_repo_name: armkeh/agda-computability


text:
module ByteCount where

open import Agda.Builtin.Word

{-# FOREIGN GHC import Foreign.C.Types #-}

postulate
  CSize : Set
  mkCSize : Word64 → CSize

{-# COMPILE GHC CSize = type CSize #-}
{-# COMPILE GHC mkCSize = CSize #-}

ByteCount : Set
ByteCount = CSize

max_stars_repo_name: cruhland/agda-editor

max_issues_repo_name: cruhland/agda-editor

max_forks_repo_name: cruhland/agda-editor


text:
------------------------------------------------------------------------
-- Primitive IO: simple bindings to Haskell types and functions
------------------------------------------------------------------------

module IO.Primitive where

open import Data.String hiding (Costring)
open import Data.Char
open import Foreign.Haskell

------------------------------------------------------------------------
-- The IO monad

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}

infixl 1 _>>=_

postulate
  return : ∀ {A} → A → IO A
  _>>=_  : ∀ {A B} → IO A → (A → IO B) → IO B

{-# COMPILED return (\_ -> return :: a -> IO a) #-}
{-# COMPILED _>>=_  (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

------------------------------------------------------------------------
-- Simple lazy IO (UTF8-based)

private
  Costring = Colist Char

postulate
  getContents : IO Costring
  readFile    : String → IO Costring
  writeFile   : String → Costring → IO Unit
  putStr      : Costring → IO Unit
  putStrLn    : Costring → IO Unit

{-# IMPORT System.IO.UTF8 #-}
{-# COMPILED getContents System.IO.UTF8.getContents #-}
{-# COMPILED readFile    System.IO.UTF8.readFile    #-}
{-# COMPILED writeFile   System.IO.UTF8.writeFile   #-}
{-# COMPILED putStr      System.IO.UTF8.putStr      #-}
{-# COMPILED putStrLn    System.IO.UTF8.putStrLn    #-}

max_issues_repo_name: larrytheliquid/Lemmachine


text: {-# OPTIONS --cubical -van-extra-option-just-to-test-a-hack:0 #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Function using (_$_)

open import Relation.Nullary using (yes; no)
open import Relation.Binary using (Decidable; Irrelevant; Antisymmetric; Setoid)
open import AKS.Algebra.Bundles using (NonZeroCommutativeRing; Field)

module AKS.Algebra.Consequences {c ℓ} (R : NonZeroCommutativeRing c ℓ) where

open import AKS.Nat using (ℕ)

open import Algebra.Bundles using (CommutativeRing)

open NonZeroCommutativeRing R using (_+_; _*_; -_; _-_; 0#; 1#) renaming (Carrier to C)
open NonZeroCommutativeRing R using (_≈_; _≉_; setoid)
open Setoid setoid using (refl; sym)
open import Relation.Binary.Reasoning.Setoid setoid
open NonZeroCommutativeRing R using (isNonZeroCommutativeRing; commutativeRing)
open CommutativeRing commutativeRing using (+-identityʳ; +-assoc; +-comm; +-congʳ; +-congˡ; +-cong; -‿cong; -‿inverseʳ)
open CommutativeRing commutativeRing using (*-identityˡ; *-cong; *-congʳ; *-congˡ; *-assoc; *-comm; zeroʳ; zeroˡ; commutativeSemiring)
open import AKS.Algebra.Structures C _≈_ using (IsField; IsEuclideanDomain; module Modulus; module Divisibility; IsIntegralDomain; IsGCDDomain; IsUniqueFactorizationDomain)
open import AKS.Algebra.Divisibility commutativeSemiring using (module Euclidean)
open Modulus using (Remainder; 0≈)
open Divisibility _*_ using (_∣_; divides)

module Division⇒EuclideanDomain
  (_≈?_ : Decidable _≈_)
  (≈-irrelevant : Irrelevant _≈_)
  (≉-irrelevant : Irrelevant _≉_)
  (∣_∣ : ∀ n {n≉0 : n ≉ 0#} → ℕ)
  (_div_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  (_mod_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  (division : ∀ n m {m≉0 : m ≉ 0#} → n ≈ m * (n div m) {m≉0} + (n mod m) {m≉0})
  (modulus : ∀ n m {m≉0 : m ≉ 0#} → Remainder 0# ∣_∣ _mod_ n m {m≉0})
  (div-cong : ∀ {x₁ x₂} {y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → ∀ {y₁≉0 y₂≉0} → (x₁ div y₁) {y₁≉0} ≈ (x₂ div y₂) {y₂≉0})
  (mod-distribʳ-* : ∀ c a b {b≉0} {b*c≉0} → ((a * c) mod (b * c)) {b*c≉0} ≈ (a mod b) {b≉0} * c)
  (*-cancelˡ : ∀ x {y z} → x ≉ 0# → x * y ≈ x * z → y ≈ z)
  where

  private
    remainder : ∀ n m {m≉0 : m ≉ 0#} → (n mod m) {m≉0} ≈ n - m * (n div m) {m≉0}
    remainder n m {m≉0} = begin
      n mod m                               ≈⟨ sym (+-identityʳ (n mod m)) ⟩
      n mod m + 0#                          ≈⟨ +-congˡ (sym (-‿inverseʳ (m * n div m))) ⟩
      n mod m + (m * n div m - m * n div m) ≈⟨ sym (+-assoc (n mod m) (m * n div m) (- (m * n div m))) ⟩
      (n mod m + m * n div m) - m * n div m ≈⟨ +-congʳ (+-comm (n mod m) (m * n div m)) ⟩
      (m * n div m + n mod m) - m * n div m ≈⟨ +-congʳ (sym (division n m {m≉0})) ⟩
      n - m * n div m                       ∎

    mod-cong : ∀ {x₁ x₂} {y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → ∀ {y₁≉0 y₂≉0} → (x₁ mod y₁) {y₁≉0} ≈ (x₂ mod y₂) {y₂≉0}
    mod-cong {x₁} {x₂} {y₁} {y₂} x₁≈x₂ y₁≈y₂ {y₁≉0} {y₂≉0} = begin
      x₁ mod y₁           ≈⟨ remainder x₁ y₁ {y₁≉0} ⟩
      x₁ - y₁ * x₁ div y₁ ≈⟨ +-cong x₁≈x₂ (-‿cong (*-cong y₁≈y₂ (div-cong x₁≈x₂ y₁≈y₂))) ⟩
      x₂ - y₂ * x₂ div y₂ ≈⟨ sym (remainder x₂ y₂ {y₂≉0}) ⟩
      x₂ mod y₂           ∎

  open Euclidean ∣_∣ _div_ _mod_ _≈?_ ≈-irrelevant ≉-irrelevant division modulus mod-cong mod-distribʳ-* using (gcd; gcd-isGCD) public

  isIntegralDomain : IsIntegralDomain _+_ _*_ -_ 0# 1#
  isIntegralDomain = record { isNonZeroCommutativeRing = isNonZeroCommutativeRing; *-cancelˡ = *-cancelˡ }

  isGCDDomain : IsGCDDomain _+_ _*_ -_ 0# 1# gcd
  isGCDDomain = record { isIntegralDomain = isIntegralDomain; gcd-isGCD = gcd-isGCD }

  isUniqueFactorizationDomain : IsUniqueFactorizationDomain _+_ _*_ -_ 0# 1# gcd
  isUniqueFactorizationDomain = record { isGCDDomain = isGCDDomain }

  isEuclideanDomain : IsEuclideanDomain _+_ _*_ -_ 0# 1# ∣_∣ _div_ _mod_ gcd
  isEuclideanDomain = record
    { isUniqueFactorizationDomain = isUniqueFactorizationDomain
    ; division = division
    ; modulus = modulus
    ; div-cong = div-cong
    ; mod-cong = mod-cong
    }

module Inverse⇒Field
  (_≈?_ : Decidable _≈_)
  (≈-irrelevant : Irrelevant _≈_)
  (≉-irrelevant : Irrelevant _≉_)
  (_/_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  (inverse : ∀ (n m : C) {m≉0 : m ≉ 0#} → n ≈ m * (n / m) {m≉0})
  where

  private
    ∣_∣ : ∀ n {n≉0 : n ≉ 0#} → ℕ
    ∣ _ ∣ = 0

    _mod_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C
    _ mod _ = 0#

    division : ∀ n m {m≉0 : m ≉ 0#} → n ≈ m * (n / m) {m≉0} + (n mod m) {m≉0}
    division n m {m≉0} = begin
      n ≈⟨ inverse  n m {m≉0} ⟩
      m * (n / m) ≈⟨ sym (+-identityʳ (m * (n / m))) ⟩
      m * (n / m) {m≉0} + (n mod m) {m≉0} ∎

    modulus : ∀ n m {m≉0 : m ≉ 0#} → Remainder 0# ∣_∣ _mod_ n m {m≉0}
    modulus _ _ = 0≈ refl

    *-cancelˡ : ∀ x {y z} → x ≉ 0# → x * y ≈ x * z → y ≈ z
    *-cancelˡ x {y} {z} x≢0 x*y≡x*z = begin
      y                  ≈⟨ sym (*-identityˡ y) ⟩
      1# * y             ≈⟨ *-congʳ (inverse 1# x {x≢0}) ⟩
      (x * (1# / x)) * y ≈⟨ *-congʳ (*-comm x (1# / x)) ⟩
      ((1# / x) * x) * y ≈⟨ *-assoc _ _ _ ⟩
      (1# / x) * (x * y) ≈⟨ *-congˡ x*y≡x*z ⟩
      (1# / x) * (x * z) ≈⟨ sym (*-assoc _ _ _) ⟩
      ((1# / x) * x) * z ≈⟨ *-congʳ (*-comm (1# / x) x) ⟩
      (x * (1# / x)) * z ≈⟨ *-congʳ (sym (inverse 1# x {x≢0})) ⟩
      1# * z             ≈⟨ *-identityˡ z ⟩
      z ∎

    div-cong : ∀ {x₁ x₂} {y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → ∀ {y₁≉0 y₂≉0} → (x₁ / y₁) {y₁≉0} ≈ (x₂ / y₂) {y₂≉0}
    div-cong {x₁} {x₂} {y₁} {y₂} x₁≈x₂ y₁≈y₂ {y₁≉0} {y₂≉0} = *-cancelˡ y₁ y₁≉0 $ begin
      y₁ * (x₁ / y₁) ≈⟨ sym (inverse x₁ y₁) ⟩
      x₁             ≈⟨ x₁≈x₂ ⟩
      x₂             ≈⟨ inverse x₂ y₂ ⟩
      y₂ * (x₂ / y₂) ≈⟨ *-congʳ (sym y₁≈y₂) ⟩
      y₁ * (x₂ / y₂) ∎

    mod-distribʳ-* : ∀ c a b {b≉0} {b*c≉0} → ((a * c) mod (b * c)) {b*c≉0} ≈ (a mod b) {b≉0} * c
    mod-distribʳ-* c a b = sym (zeroˡ c)

  open Division⇒EuclideanDomain _≈?_ ≈-irrelevant ≉-irrelevant ∣_∣ _/_ _mod_ division modulus div-cong mod-distribʳ-* *-cancelˡ using (gcd; isEuclideanDomain) public

  isField : IsField _+_ _*_ -_ 0# 1# _/_ gcd
  isField = record { isEuclideanDomain = isEuclideanDomain }

  [field] : Field c ℓ
  [field] = record { isField = isField }

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
------------------------------------------------------------------------------
-- Natural numbers (PCF version)
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module LTC-PCF.Data.Nat where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Rec
open import LTC-PCF.Data.Nat.Type public

infixl 7 _*_
infixl 6 _+_ _∸_

------------------------------------------------------------------------------
-- Addition with recursion on the first argument.
_+_ : D → D → D
m + n = rec m n (lam (λ _ → lam succ₁))

-- Subtraction with recursion on the second argument.
_∸_ : D → D → D
m ∸ n = rec n m (lam (λ _ → lam pred₁))

-- Multiplication with recursion on the first argument.
_*_ : D → D → D
m * n = rec m zero (lam (λ _ → lam (λ x → n + x)))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module CombiningProofs.Erasing where

postulate
  D     : Set
  succ₁ : D → D

data N : D → Set where
  nsucc₁ : ∀ {n} → N n → N (succ₁ n)
  nsucc₂ : ∀ {n} → (Nn : N n) → N (succ₁ n)

-- The types of nsucc₁ and nsucc₂ are the same.

-- (18 April 2013)
-- $ dump-agdai Erasing

-- Qname: Erasing.N.nsucc₁
-- Type: El {getSort = Type (Max []), unEl = Pi []r{El {getSort = Type (Max []), unEl = Def Erasing.D []}} (Abs "n" El {getSort = Type (Max []), unEl = Pi []r(El {getSort = Type (Max []), unEl = Def Erasing.N [[]r(Var 0 [])]}) (NoAbs "_" El {getSort = Type (Max []), unEl = Def Erasing.N [[]r(Def Erasing.succ₁ [[]r(Var 0 [])])]})})}

-- Qname: Erasing.N.nsucc₂
-- Type: El {getSort = Type (Max []), unEl = Pi []r{El {getSort = Type (Max []), unEl = Def Erasing.D []}} (Abs "n" El {getSort = Type (Max []), unEl = Pi []r(El {getSort = Type (Max []), unEl = Def Erasing.N [[]r(Var 0 [])]}) (NoAbs "Nn" El {getSort = Type (Max []), unEl = Def Erasing.N [[]r(Def Erasing.succ₁ [[]r(Var 0 [])])]})})}


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Functions.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.WellFounded
open import Semirings.Definition
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Orders.WellFounded.Definition
open import Orders.WellFounded.Induction

module Sets.CantorBijection.Order where

order : Rel (ℕ && ℕ)
order (a ,, b) (c ,, d) = ((a +N b) <N (c +N d)) || (((a +N b) ≡ (c +N d)) && (b <N d))

totalOrder : TotalOrder (ℕ && ℕ)
PartialOrder._<_ (TotalOrder.order totalOrder) = order
PartialOrder.irreflexive (TotalOrder.order totalOrder) {fst ,, snd} (inl x) = exFalso (TotalOrder.irreflexive ℕTotalOrder x)
PartialOrder.irreflexive (TotalOrder.order totalOrder) {fst ,, snd} (inr (_ ,, p)) = exFalso (TotalOrder.irreflexive ℕTotalOrder p)
PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inl pr1) (inl pr2) = inl (TotalOrder.<Transitive ℕTotalOrder pr1 pr2)
PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inl pr1) (inr (f1 ,, f2)) = inl (identityOfIndiscernablesRight _<N_ pr1 f1)
PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inr (f1 ,, f2)) (inl x) = inl (identityOfIndiscernablesLeft _<N_ x (equalityCommutative f1))
PartialOrder.<Transitive (TotalOrder.order totalOrder) {x1 ,, x2} {y1 ,, y2} {z1 ,, z2} (inr (f1 ,, f2)) (inr (fst ,, snd)) = inr (transitivity f1 fst ,, TotalOrder.<Transitive ℕTotalOrder f2 snd)
TotalOrder.totality totalOrder (a ,, b) (c ,, d) with TotalOrder.totality ℕTotalOrder (a +N b) (c +N d)
TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inl (inl x) = inl (inl (inl x))
TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inl (inr x) = inl (inr (inl x))
TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inr eq with TotalOrder.totality ℕTotalOrder b d
TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inr eq | inl (inl x) = inl (inl (inr (eq ,, x)))
TotalOrder.totality totalOrder (a ,, b) (c ,, d) | inr eq | inl (inr x) = inl (inr (inr (equalityCommutative eq ,, x)))
TotalOrder.totality totalOrder (a ,, b) (c ,, .b) | inr eq | inr refl rewrite canSubtractFromEqualityRight {a} {b} {c} eq = inr refl

leastElement : {y : ℕ && ℕ} → order y (0 ,, 0) → False
leastElement {zero ,, b} (inl ())
leastElement {zero ,, b} (inr ())
leastElement {succ a ,, b} (inl ())
leastElement {succ a ,, b} (inr ())

mustDescend : (a b t : ℕ) → order (a ,, b) (t ,, zero) → a +N b <N t
mustDescend a b zero ord = exFalso (leastElement ord)
mustDescend a b (succ t) (inl x) rewrite Semiring.sumZeroRight ℕSemiring t = x

orderWellfounded : WellFounded order
orderWellfounded (a ,, b) = access (go b a)
  where
    g0 : (c : ℕ) (y : ℕ && ℕ) → order y (c ,, 0) → Accessible order y
    -- We want to induct on the second entry of x here, so we decompose so as to put that first.
    g : (x : ℕ) → ((y : ℕ) → y <N x → (b : ℕ) (z : ℕ && ℕ) → order z (b ,, y) → Accessible order z) → (c : ℕ) (y : ℕ && ℕ) → order y (c ,, x) → Accessible order y

    g0 = rec <NWellfounded (λ z → (x : ℕ && ℕ) (x₁ : order x (z ,, zero)) → Accessible order x) f
      where
        p : (a b : ℕ) → a ≡ b → (a ,, zero) ≡ (b ,, zero)
        p a .a refl = refl

        f : (x : ℕ) (x₁ : (x₂ : ℕ) (x₃ : x₂ <N x) (x₄ : ℕ && ℕ) (x₅ : order x₄ (x₂ ,, zero)) → Accessible order x₄) (x₂ : ℕ && ℕ) (x₃ : order x₂ (x ,, zero)) → Accessible order x₂
        f zero pr y ord = exFalso (leastElement ord)
        f (succ m) pr (fst ,, snd) (inl pr2) = h snd fst pr2
          where
            go : (x : ℕ) (x₁ : (x₂ : ℕ) (x₃ : x₂ <N x) (x₄ : ℕ) (x₅ : x₄ +N x₂ <N succ (m +N zero)) → Accessible order (x₄ ,, x₂)) (x₂ : ℕ) (x₃ : x₂ +N x <N succ (m +N zero)) → Accessible order (x₂ ,, x)
            go bound pr2 toProve bounded with TotalOrder.totality ℕTotalOrder (toProve +N bound) (m +N 0)
            ... | inl (inl bl) = pr m (le 0 refl) (toProve ,, bound) (inl bl)
            ... | inl (inr bl) = exFalso (noIntegersBetweenXAndSuccX (m +N 0) bl bounded)
            go zero pr2 toProve _ | inr bl rewrite Semiring.sumZeroRight ℕSemiring m | Semiring.sumZeroRight ℕSemiring toProve = access λ i i<z → pr m (le 0 refl) i (inl (mustDescend (_&&_.fst i) (_&&_.snd i) (m +N zero) (identityOfIndiscernablesLeft order (identityOfIndiscernablesRight order i<z (p toProve (m +N 0) (transitivity bl (equalityCommutative (Semiring.sumZeroRight ℕSemiring m))))) refl)))
            go (succ bound) pr2 toProve _ | inr bl = access desc
              where
                desc : (i : ℕ && ℕ) → (order i (toProve ,, succ bound)) → Accessible order i
                desc (i1 ,, i2) (inl ord) = pr m (le zero refl) (i1 ,, i2) (inl (identityOfIndiscernablesRight _<N_ ord bl))
                desc (i1 ,, i2) (inr (ord1 ,, ord2)) = pr2 i2 ord2 i1 (le 0 (applyEquality succ (transitivity ord1 bl)))

            h : (a : ℕ) (b : ℕ) (pr2 : b +N a <N succ m +N 0) → Accessible order (b ,, a)
            h = rec <NWellfounded (λ z → (x2 : ℕ) (x1 : x2 +N z <N succ (m +N zero)) → Accessible order (x2 ,, z)) go

    g zero _ = g0
    g (succ x) pr zero (y1 ,, y2) (inl pr1) with TotalOrder.totality ℕTotalOrder (y1 +N y2) x
    g (succ x) pr zero (y1 ,, y2) (inl pr1) | inl (inl y1+y2<x) = pr x (le 0 refl) zero (y1 ,, y2) (inl y1+y2<x)
    g (succ x) pr zero (y1 ,, y2) (inl pr1) | inl (inr x<y1+y2) = exFalso (noIntegersBetweenXAndSuccX x x<y1+y2 pr1)
    g (succ x) pr zero (y1 ,, y2) (inl pr1) | inr y1+y2=x = access (λ y y<zs → pr x (le 0 refl) zero y (ans y y<zs))
      where
        ans : (y : ℕ && ℕ) → order y (y1 ,, y2) → (_&&_.fst y +N _&&_.snd y <N x) || ((_&&_.fst y +N _&&_.snd y ≡ x) && (_&&_.snd y <N x))
        ans (fst ,, snd) (inl x) rewrite y1+y2=x = inl x
        ans (zero ,, snd) (inr (a1 ,, a2)) rewrite y1+y2=x | a1 = exFalso (bad x y1 y2 y1+y2=x a2)
          where
            bad : (x y1 y2 : ℕ) → y1 +N y2 ≡ x → x <N y2 → False
            bad x zero y2 y1+y2=x x<y2 = TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesRight _<N_ x<y2 y1+y2=x)
            bad x (succ y1) y2 y1+y2=x x<y2 rewrite equalityCommutative y1+y2=x = TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x<y2 (identityOfIndiscernablesRight _<N_ (addingIncreases y2 y1) (Semiring.commutative ℕSemiring y2 (succ y1))))
        ans (succ fst ,, snd) (inr (a1 ,, a2)) rewrite y1+y2=x = inr (a1 ,, le fst a1)
    g (succ x) pr zero (zero ,, y2) (inr (fst ,, snd)) = exFalso (TotalOrder.irreflexive ℕTotalOrder (identityOfIndiscernablesLeft _<N_ snd fst))
    g (succ x) pr zero (succ y1 ,, y2) (inr (fst ,, snd)) = pr y2 snd (succ (succ y1)) (succ y1 ,, y2) (inl (le 0 refl))
    g (succ x) pr (succ c) y (inl z) = pr x (le 0 refl) (succ (succ c)) y (inl (identityOfIndiscernablesRight _<N_ z (applyEquality succ (transitivity (Semiring.commutative ℕSemiring c (succ x)) (applyEquality succ (Semiring.commutative ℕSemiring x c))))))
    g (succ x) pr (succ c) y (inr (fst ,, snd)) with TotalOrder.totality ℕTotalOrder (_&&_.snd y) x
    ... | inl (inl bl) = pr x (le 0 refl) (succ (succ c)) y (inr (transitivity fst (applyEquality succ (transitivity (Semiring.commutative ℕSemiring c (succ x)) (applyEquality succ (Semiring.commutative ℕSemiring x c)))) ,, bl))
    ... | inl (inr bl) = exFalso (noIntegersBetweenXAndSuccX x bl snd)
    g (succ x) pr (succ c) (y1 ,, .x) (inr (fst ,, _)) | inr refl with canSubtractFromEqualityRight {y1} {x} {succ (succ c)} (transitivity fst (applyEquality succ (transitivity (Semiring.commutative ℕSemiring c (succ x)) (applyEquality succ (Semiring.commutative ℕSemiring x c)))))
    g (succ x) pr (succ c) (.(succ (succ c)) ,, .x) (inr (_ ,, _)) | inr refl | refl = pr x (le 0 refl) (succ (succ (succ c))) (succ (succ c) ,, x) (inl (le 0 refl))

    go : (a : ℕ) → (b : ℕ) → (y : ℕ && ℕ) → order y (b ,, a) → Accessible order y
    go = rec <NWellfounded (λ (a : ℕ) → (b : ℕ) → (y : ℕ && ℕ) → order y (b ,, a) → Accessible order y) g


text:
module Basic.Axiomatic.Partial where

open import Data.Bool hiding (not; if_then_else_; _∧_)
open import Data.Vec hiding ([_]; _++_; split)
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
import Level as L

open import Utils.Decidable
open import Basic.AST
open import Basic.BigStep

{-

Here we define a Hoare logic for partial correctness of While programs (chapter 6.2).

The most important point here is the choice of representation for predicates.

The book mention intensional and extensional approaches. In the intensional approach,
we define a separate assertion language. However, the assertion language has to be powerful
enough to be able to express useful properties of the program state, and it takes quite a bit
of work to define such a language. An advatange of the intensional approach is that we could reuse
the same assertion language to extend the object language in other ways.

The book uses the extensional approach, and so do we. We go a bit further than the book though:
the book has boolean predicates over the program state, while we have type theoretic
"(State n → Set)" predicates. This means that our predicates can be proof-relevant and contain data,
so they can express computations and transformations on states.

However, the higher-order nature of the "(State n → Set)" representation of predicates also makes
type inference quite hard. I attepmeted to do some correctness proofs with the Hoare logics, and
it's certainly feasible, but we would need a lot more machinery and lots of helper functions to
make it convenient enough.

It's interesting to note that manual proof-writing is generally easier with Hoare logics than with
raw semantics, but here in Agda it's the opposite: the proofs in raw semantics (see e. g. the
factorial proofs in Basic.SmallStep, Basic.BigStep and Extended.FunRetRec) are pretty neat convenient,
since Agda keeps track of the program state for us and hides lots of unnecessary details.

Side note: we could have made our definition universe polymorphic. It would be a trivial extension;
the reason we don't have it is that we don't need that much power of expression for any of our proofs.
Just using "Set" suffices.

-}

{-
Predicate combinators: these just lift conjunction and implication into the State environment.
-}
_∧_ :
  ∀ {α β γ}{A : Set α}
  → (A → Set β)
  → (A → Set γ)
  → (A → Set _)
_∧_ f g x = f x × g x

_==>_ :
  ∀ {α β γ}{A : Set α}
  → (A → Set β)
  → (A → Set γ)
  → Set _
_==>_ f g = ∀ {x} → f x → g x

infixr 4 _,_
data 〈_〉_〈_〉 {n} : (State n → Set) → St n → (State n → Set) → Set₁ where

  skip :
           ∀ {P}
    → -----------------
      〈 P 〉 skip 〈 P 〉

  ass :
                        ∀ {x a P}
    → ----------------------------------------------
      〈 (λ s → P (s [ x ]≔ ⟦ a ⟧ᵉ s)) 〉 x := a 〈 P 〉

  _,_ :
             ∀ {P Q R S₁ S₂} →
      〈 P 〉 S₁ 〈 Q 〉 → 〈 Q 〉 S₂ 〈 R 〉
    → --------------------------------
            〈 P 〉 S₁ , S₂ 〈 R 〉

  if :
                          ∀ {P Q b S₁ S₂} →
      〈 (T ∘ ⟦ b ⟧ᵉ) ∧ P 〉 S₁ 〈 Q 〉 → 〈 (F ∘ ⟦ b ⟧ᵉ) ∧ P 〉 S₂ 〈 Q 〉
    → --------------------------------------------------------------
                  〈 P 〉 if b then S₁ else S₂ 〈 Q 〉

  while :
                   ∀ {P b S} →
          〈 (T ∘ ⟦ b ⟧ᵉ) ∧ P 〉 S 〈 P 〉
    → ----------------------------------------
      〈 P 〉 while b do S 〈 (F ∘ ⟦ b ⟧ᵉ) ∧ P 〉

  cons :
                ∀ {P' Q' P Q S} →
      P ==> P' → 〈 P' 〉 S 〈 Q' 〉 → Q' ==> Q
    → -----------------------------------------
                 〈 P 〉 S 〈 Q 〉

{-
A part of exercise 6.13 (associativity of statement composition with respect to our logic).
-}

split :
  ∀ {n P R}{S₁ S₂ : St n}
  → 〈 P 〉 S₁ , S₂ 〈 R 〉
  → ∃ λ Q
  → (〈 P 〉 S₁ 〈 Q 〉) × (〈 Q 〉 S₂ 〈 R 〉)
split (p , p₁) = _ , (p , p₁)
split (cons x p y) with split p
... | Q , (p1 , p2)  = Q , (cons x p1 id , cons id p2 y)

ex-613a :
  ∀ {n P Q}{S₁ S₂ S₃ : St n}
  → 〈 P 〉 S₁ , (S₂ , S₃) 〈 Q 〉
  → 〈 P 〉 (S₁ , S₂) , S₃ 〈 Q 〉
ex-613a (p , p₁) with split p₁
... | _ , (p₁₁ , p₁₂) = (p , p₁₁) , p₁₂
ex-613a (cons x p x₁) = cons x (ex-613a p) x₁

ex-613b :
  ∀ {n P Q}{S₁ S₂ S₃ : St n}
  → 〈 P 〉 (S₁ , S₂) , S₃ 〈 Q 〉
  → 〈 P 〉 S₁ , (S₂ , S₃) 〈 Q 〉
ex-613b (p₁ , p₂) with split p₁
... | _ , (p₁₁ , p₁₂) = p₁₁ , (p₁₂ , p₂)
ex-613b (cons x p x₁) = cons x (ex-613b p) x₁

{-
Now we set out to prove soundess and completeness of our Hoare logic (see chapter 6.3).

Note that we express validity of a Hoare triple in terms of the weakest liberal precondition:

  ⊨ₚ { P } S { Q }  :=   (P ==> wlp S Q)

This is just a notational conveneince, but for some reason I also find it pleasing to the eye.

-}

-- Weakest liberal precondition
------------------------------------------------------------

wlp : ∀ {n} → St n → (State n → Set) → State n → Set
wlp S Q s = ∀ {s'} → ⟨ S , s ⟩⟱ s' → Q s'

-- Soundness
------------------------------------------------------------

{-
This proof is the same as in the book, because it's rather simple and there's not
much choice.
-}

sound : ∀ {n}{S : St n}{P Q} → 〈 P 〉 S 〈 Q 〉 → (P ==> wlp S Q)
sound skip ps skip                         = ps
sound ass ps ass                           = ps
sound (p , p₁) ps (run , run₁)             = sound p₁ (sound p ps run) run₁
sound (if p p₁) ps (if-true x run)         = sound p (x , ps) run
sound (if p p₁) ps (if-false x run)        = sound p₁ (x , ps) run
sound (while p) ps (while-true x run run₁) = sound (while p) (sound p (x , ps) run) run₁
sound (while p) ps (while-false x)         = x , ps
sound (cons x p x₁) ps run                 = x₁ (sound p (x ps) run)

-- Completeness
------------------------------------------------------------

{-
This one differs from the book proof.

The book proves the following:

  ∀ S Q → 〈 wlp S Q 〉 S 〈 Q 〉

then uses "cons" and the definition of "wlp" to infer 〈 P 〉 S 〈 Q 〉 from (P ==> wlp S Q).

We instead prove completeness directly. Our job here is essentially to recurse on sub-statements,
while making the postcondition of that statement equal to the weakest precondition of the following
statement.

As a result, the proofs for the "if_then_else_" , composition and "while" cases are all
a bit simpler than the book proofs.

In the case of "while", the book makes an unnecessary twist. It uses the law of excluded middle
on "〈 while b do S , s' 〉⟶ s''" derivations, but there's actually no need for that. It would be
indeed ugly in Agda, where we would have to assume classical logic and destroy constructivity
in order to be able to write that proof.

-}

complete : ∀ {n}(S : St n){P Q} → (P ==> wlp S Q) → 〈 P 〉 S 〈 Q 〉
complete (x := a) f = cons (λ z → f z ass) ass id
complete skip     f = cons (λ z → f z skip) skip id

complete (S , S₁){P}{Q} f =
    complete S {P} {wlp S₁ Q} (λ ps runS runS₁ → f ps (runS , runS₁))
  , complete S₁ id

complete (if b then S else S₁){P}{Q} f =
  if (complete S  {(T ∘ ⟦ b ⟧ᵉ) ∧ P} {Q} (λ {(pb , pP) → λ runS → f pP (if-true pb runS)}))
     (complete S₁ {(F ∘ ⟦ b ⟧ᵉ) ∧ P} {Q} (λ {(pb , pP) → λ runS₁ → f pP (if-false pb runS₁)}))

complete (while b do S){P}{Q} f =
  cons f
    (while
      (complete S {(T ∘ ⟦ b ⟧ᵉ) ∧ W} {W}
        (λ {(pb , pw) → λ runS runW → pw (while-true pb runS runW)})))
    (λ {(pb , pw) → pw (while-false pb)})
  where W = wlp (while b do S) Q

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.LT-Models where

-- Given a fixed Lawvere Theory LT and a fixed category C,
-- the Functors [LT , C] form a category.

-- The proof is basically the same as that of Functors.

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-CartesianCategory)
open import Categories.NaturalTransformation
  using (NaturalTransformation; _∘ᵥ_) renaming (id to idN)
open import Categories.NaturalTransformation.Equivalence using (_≃_; ≃-isEquivalence)
open import Categories.Theory.Lawvere using (LawvereTheory; ModelsOf_In_)

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

-- The reason the proofs below are so easy is that _∘ᵥ_ 'computes' all the way down into
-- expressions in C, from which the properties follow.
LT-Models : LawvereTheory ℓ e → CartesianCategory o′ ℓ′ e′ → Category (ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (ℓ ⊔ ℓ′ ⊔ e′) e′
LT-Models LT C = record
  { Obj       = ModelsOf LT In C
  ; _⇒_       = λ m₁ m₂ → NaturalTransformation (ModelsOf_In_.mod m₁) (ModelsOf_In_.mod m₂)
  ; _≈_       = _≃_
  ; id        = idN
  ; _∘_       = _∘ᵥ_
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = ≃-isEquivalence
  ; ∘-resp-≈  = λ eq eq′ → ∘-resp-≈ eq eq′
  }
  where
    module C = CartesianCategory C using (U)
    open Category C.U

LT-SetoidsModels : {ℓ′ e′ : Level} → LawvereTheory ℓ e → Category (ℓ ⊔ e ⊔ suc (ℓ′ ⊔ e′)) (ℓ ⊔ ℓ′ ⊔ e′) (ℓ′ ⊔ e′)
LT-SetoidsModels {ℓ′ = ℓ′} {e′} LT = LT-Models LT (Setoids-CartesianCategory ℓ′ e′)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Auto-Modules where

open import Auto.Prelude hiding (cong; trans)

module NonemptySet (X : Set) (x : X) where
 h0 : (P : X → Set) → (∀ x → P x) → Σ X P
 h0 = {!!}
-- h0 = λ P h → Σ-i x (h x)

module WithRAA (RAA : ∀ A → ¬ (¬ A) → A) where
 h1 : ∀ A → A ∨ ¬ A
 h1 = {!!}
 --h1 = λ A → RAA (A ∨ ((x : A) → ⊥)) (λ z → z (∨-i₂ (λ x → z (∨-i₁ x))))

 module B where
  h2 : ∀ A → A ∨ ¬ A
  h2 = {!!}

module A (X : Set) (x : X) where
 postulate AllSame : {x y : X} → x ≡ y

 n0 : (P : X → Set) → Σ X P → ∀ x → P x
-- n0 = {!subst AllSame!}  -- no solution found
 n0 = λ P h x → subst P (Σ.wit h) x AllSame (Σ.prf h)

module B (X : Set) (x y : X) (P : X → Set) where
 postulate p : P x

 h3 : P x
 h3 = {!p!}
-- h3 = p

module Setoid (X : Set)
              (Eq : X → X → Set)
              (refl : ∀ {x} → Eq x x)
              (symm : ∀ {x₁ x₂} → Eq x₁ x₂ → Eq x₂ x₁)
              (subst : ∀ {x₁ x₂} → (P : X → Set) → Eq x₁ x₂ → P x₁ → P x₂)
 where
 cong : ∀ {x₁ x₂} → (f : X → X) → Eq x₁ x₂ → Eq (f x₁) (f x₂)
 cong = {!!}  -- hole 4
-- cong = λ {x₁} {x₂} f z → subst (λ z₁ → Eq (f x₁) (f z₁)) z refl

 trans : ∀ {x₁ x₂ x₃} → Eq x₁ x₂ → Eq x₂ x₃ → Eq x₁ x₃
 trans = {!!}  -- hole 5
-- trans = λ {x₁} {x₂} {x₃} z z₁ → subst (Eq x₁) z₁ z

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Base where

data True : Set where
  T : True

data False : Set where

infix 20 _*_

data _*_ (A : Set)(B : A -> Set) : Set where
 <_,_> : (x : A) -> B x -> A * B

rel : Set -> Set1
rel A = A -> A -> Set

pred : Set -> Set1
pred A = A -> Set

Refl : {A : Set} -> rel A -> Set
Refl {A} R = {x : A} -> R x x

Sym : {A : Set} -> rel A -> Set
Sym {A} R = {x y : A} -> R x y -> R y x

Trans : {A : Set} -> rel A -> Set
Trans {A} R = {x y z : A} -> R x y -> R y z -> R x z

Map : {A : Set} -> rel A -> {B : Set} -> rel B -> pred (A -> B)
Map {A} _R_ _S_ f = {x y : A} -> x R y -> f x S f y

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Pointers to results from the paper
------------------------------------------------------------------------

-- Note that the code has evolved after the paper was published. For
-- code that is closer to the paper, see the version of the code that
-- is distributed with the paper.

{-# OPTIONS --sized-types #-}

module README.Pointers-to-results-from-the-paper where

import Bisimilarity
import Bisimilarity.CCS
import Bisimilarity.Classical
import Bisimilarity.Comparison
import Bisimilarity.Delay-monad
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.CCS.Examples
import Bisimilarity.CCS.Examples.Natural-numbers
import Bisimilarity.Step
import Bisimilarity.Up-to
import Bisimilarity.Up-to.CCS
import Bisimilarity.Up-to.Counterexamples
import Bisimilarity.Weak
import Bisimilarity.Weak.CCS
import Bisimilarity.Weak.Delay-monad
import Bisimilarity.Weak.Up-to
import Delay-monad
import Delay-monad.Bisimilarity
import Delay-monad.Bisimilarity.Alternative
import Delay-monad.Bisimilarity.Negative
import Expansion
import Expansion.CCS
import Expansion.Delay-monad
import Indexed-container
import Indexed-container.Delay-monad
import Labelled-transition-system
import Labelled-transition-system.CCS
import Labelled-transition-system.Delay-monad
import Relation
import Similarity
import Similarity.CCS
import Up-to
import Up-to.Closure

------------------------------------------------------------------------
-- Section 2

-- The Delay monad.
--
-- Note that, unlike the definition in the paper, this definition is
-- universe-polymorphic. Similar remarks apply to many definitions
-- below as well.

Delay  = Delay-monad.Delay
Delay′ = Delay-monad.Delay′

-- The non-terminating computation never.

never = Delay-monad.never

-- Strong bisimilarity for the delay monad.
--
-- Note that, unlike in the paper, strong bisimilarity, weak
-- bisimilarity and the expansion relation are defined as a single
-- family (with an extra index).

[_]_∼D_  = Delay-monad.Bisimilarity.[_]_∼_
[_]_∼′D_ = Delay-monad.Bisimilarity.[_]_∼′_

-- Strong bisimilarity is transitive.
--
-- (The proof is more general than the one in the paper.)

transitiveˢ = Delay-monad.Bisimilarity.transitive-∼ʳ

------------------------------------------------------------------------
-- Section 3

-- Indexed containers.
--
-- The paper defines indexed containers with one index type, but this
-- definition uses two.

Container = Indexed-container.Container
⟦_⟧       = Indexed-container.⟦_⟧
map       = Indexed-container.map

-- Index-preserving functions.

_⊆_ = Relation._⊆_

-- The greatest fixpoint.

ν      = Indexed-container.ν
ν′     = Indexed-container.ν′
ν-out  = Indexed-container.ν-out
ν-in   = Indexed-container.ν-in
unfold = Indexed-container.unfold

-- Relation containment (_⊆_) is not antisymmetric if the index type
-- is inhabited.

⊆-not-antisymmetric = Relation.⊆-not-antisymmetric

-- The shapes of a container are in pointwise bijective correspondence
-- with the interpretation of the container applied to the constant
-- function yielding the unit type.

Shape↔⟦⟧⊤ = Indexed-container.Shape↔⟦⟧⊤

-- A container corresponding to the Delay monad.

DelayC = Indexed-container.Delay-monad.DelayC

-- A (size-preserving) logical equivalence between the direct
-- definition of the delay monad and the indirect definition using ν
-- and the container DelayC.

Delay⇔νDelayC = Indexed-container.Delay-monad.Delay⇔νDelayC

-- Bisimilarity for ν.

ν-bisimilar = Indexed-container.ν-bisimilar

-- The two components of Delay⇔νDelayC {i = ∞} are inverses up to
-- (strong) bisimilarity.

Delay⇔νDelayC-inverses =
  Indexed-container.Delay-monad.Delay⇔νDelayC-inverses

------------------------------------------------------------------------
-- Section 4

-- Labelled transition systems.

LTS = Labelled-transition-system.LTS

-- The record type B.
--
-- The type is parametrised so that it can also be used to define weak
-- bisimilarity and expansion.

B = Bisimilarity.Step.Step

-- The container B^C, roughly as given in the paper.

B^C = Bisimilarity.Step.StepC′

-- The code mainly uses another definition of B^C, built up from
-- smaller building blocks, and employing a trick to make it easier
-- for Agda to infer implicit arguments.

B^C-code = Bisimilarity.Step.StepC

-- The two definitions of B^C have interpretations that are pointwise
-- logically equivalent, and in the presence of extensionality they
-- are pointwise isomorphic.

B^C-code↔B^C = Bisimilarity.Step.StepC↔StepC′

-- The interpretation of B^C is pointwise logically equivalent to B,
-- and in the presence of extensionality they are pointwise
-- isomorphic.

B↔B^C = Bisimilarity.Step.Step↔StepC′

-- The traditional definition of bisimilarity.

Bisimilar = Bisimilarity.Classical._∼_

-- The definition using ν.

[_]_∼_ = Bisimilarity.[_]_∼_

-- The two definitions are pointwise logically equivalent.

classical-and-ν-equivalent =
  Bisimilarity.Comparison.classical⇔coinductive

-- The definition using ν′.

[_]_∼′_ = Bisimilarity.[_]_∼′_

-- Derived transition relations.

_⇒_    = Labelled-transition-system.LTS._⇒_
_[_]⇒_ = Labelled-transition-system.LTS._[_]⇒_
_[_]⇒̂_ = Labelled-transition-system.LTS._[_]⇒̂_
_[_]→̂_ = Labelled-transition-system.LTS._[_]⟶̂_

-- Weak bisimilarity.

[_]_≈_ = Bisimilarity.Weak.[_]_≈_

-- Expansion.

[_]_≳_ = Expansion.[_]_≳_

-- A general definition that can be instantiated with different
-- transition relations to yield strong or weak bisimilarity or the
-- expansion relation.

import Bisimilarity.General

-- The labelled transition system for the delay monad.

delay-monad-lts = Labelled-transition-system.Delay-monad.delay-monad

-- The definition of bisimilarity obtained from this LTS is pointwise
-- logically equivalent to the direct definition of strong
-- bisimilarity for the delay monad.

delay-monad-direct⇔indirect = Bisimilarity.Delay-monad.direct⇔indirect

-- Symmetry of bisimilarity for an arbitrary LTS.
--
-- Note that, due to the use of a container in the definition of
-- strong bisimilarity, the proof uses a helper function instead of
-- the copatterns left-to-right and right-to-left. Furthermore the
-- function map₃ is not used, but rather a combination of other
-- functions. Similar remarks apply to several definitions below.

symmetric  = Bisimilarity.symmetric-∼
symmetric′ = Bisimilarity.symmetric-∼′

-- Transitivity of bisimilarity for an arbitrary LTS.

transitive = Bisimilarity.transitive-∼

------------------------------------------------------------------------
-- Section 5

-- CCS.

Name-with-kind = Labelled-transition-system.CCS.Name-with-kind
co             = Labelled-transition-system.CCS.co
Action         = Labelled-transition-system.CCS.Action
is-silent      = Labelled-transition-system.CCS.is-silent
Proc           = Labelled-transition-system.CCS.Proc
Proc′          = Labelled-transition-system.CCS.Proc′
_[_]→_         = Labelled-transition-system.CCS._[_]⟶_
_∉_            = Labelled-transition-system.CCS._∉_

-- The transition relation takes finite processes to finite processes.

finite→finite = Labelled-transition-system.CCS.finite→finite

-- Restricted and the corresponding lemma.

Restricted   = Bisimilarity.CCS.Examples.Restricted
Restricted∼∅ = Bisimilarity.CCS.Examples.Restricted∼∅

-- ∅ is a left identity for parallel composition.

∣-left-identity = Bisimilarity.CCS.∣-left-identity

-- Proofs showing that all the CCS process constructors preserve
-- strong bisimilarity. (For ∅ the proof is simply reflexivity of
-- strong bisimilarity.)
--
-- The proofs are written in such a way that the arguments can be
-- reused for similar proofs about strong similarity. (See below for
-- proofs that are closer to the proofs in the paper.)

module Strong-bisimilarity-congruence where

  _∣-cong_  = Bisimilarity.CCS._∣-cong_
  ·-cong    = Bisimilarity.CCS._·-cong_
  !-cong    = Bisimilarity.CCS.!-cong_
  _⊕-cong_  = Bisimilarity.CCS._⊕-cong_
  ⟨ν_⟩-cong = Bisimilarity.CCS.⟨ν_⟩-cong
  ∅-cong    = Bisimilarity.reflexive-∼

-- Some proofs have been repeated in order to provide code which is
-- closer to that presented in the paper.

module As-in-the-paper where

  _∣-cong_ = Bisimilarity.CCS._∣-congP_
  ·-cong   = Bisimilarity.CCS.·-congP
  !-cong   = Bisimilarity.CCS.!-congP

-- The code uses overloaded equational reasoning combinators.

import Equational-reasoning

-- The proof As-in-the-paper._∣-cong_ does not use symmetric′, but the
-- overloaded combinator symmetric. Agda resolves this use of
-- symmetric to an instance corresponding to symmetric′.

symmetric′-instance =
  Bisimilarity.Equational-reasoning-instances.symmetric∼′

-- Lemmas corresponding to ·-cong for expansion and weak bisimilarity.

module ·-cong where

  expansion         = Expansion.CCS._·-cong_
  weak-bisimilarity = Bisimilarity.Weak.CCS._·-cong_

-- The example with P and Q.

P   = Bisimilarity.CCS.Examples.Natural-numbers.P
Q   = Bisimilarity.CCS.Examples.Natural-numbers.Q
P∼Q = Bisimilarity.CCS.Examples.Natural-numbers.P∼Q

-- The processes in the family P are irregular.

P-irregular = Bisimilarity.CCS.Examples.Natural-numbers.P-irregular

-- The combinators _■ and _∼⟨_⟩_ presented in the paper correspond to
-- two instances.

_■     = Bisimilarity.Equational-reasoning-instances.reflexive∼
_∼⟨_⟩_ = Bisimilarity.Equational-reasoning-instances.trans∼∼

-- Equations of the form [ ∞ ] P ∼ (C [ P ]) have unique solutions up
-- to bisimilarity for contexts C where every hole is under a prefix.

existence  = Bisimilarity.CCS.solutions-exist
uniqueness = Bisimilarity.CCS.unique-solutions

------------------------------------------------------------------------
-- Section 6

-- Up-to techniques.

Up-to-technique = Up-to.Up-to-technique

-- Relation transformers.

Trans = Relation.Trans

-- Size-preserving transformers.

Size-preserving = Up-to.Size-preserving

-- Composition of binary relations.

_⊙_ = Relation._⊙_

-- Up to bisimilarity.

Up-to-bisimilarity =
  Bisimilarity.Up-to.Up-to-bisimilarity
up-to-bisimilarity-size-preserving =
  Bisimilarity.Up-to.up-to-bisimilarity-size-preserving

-- Up to context.

Up-to-context                 = Bisimilarity.Up-to.CCS.Up-to-context
up-to-context-size-preserving =
  Bisimilarity.Up-to.CCS.up-to-context-size-preserving

-- Up to the simple context consisting of replication applied to a
-- single hole.

Up-to-!                 = Bisimilarity.Up-to.CCS.Up-to-!
up-to-!-size-preserving = Bisimilarity.Up-to.CCS.up-to-!-size-preserving

-- If a transformer is size-preserving, then it satisfies a
-- corresponding property for ν′ (and vice versa).

size-preserving′ = Up-to.size-preserving⇔size-preserving′

-- Size-preserving transformers are up-to techniques.

size-preserving→up-to = Up-to.size-preserving→up-to

-- Monotonicity.

Monotone = Relation.Monotone

-- The definition of Size-preserving can be simplified for monotone
-- transformers.

simplification = Up-to.monotone→⇔

-- There are at least two size-preserving relation transformers that
-- are not monotone (or extensive).

not-monotone =
  Bisimilarity.Up-to.Counterexamples.∃-2-size-preserving×¬[monotone⊎extensive]

-- There is a container C such that there are at least two
-- transformers that, despite preserving every approximation of the
-- greatest fixpoint of C, are not up-to techniques with respect to C.

not-up-to =
  Bisimilarity.Up-to.Counterexamples.∃special-case-of-size-preserving×¬up-to

-- There are monotone (and extensive) up-to techniques G and H such
-- that G ∘ H is not an up-to-technique.

not-closed-under-composition =
  Bisimilarity.Up-to.Counterexamples.∃[monotone×extensive×up-to]²×¬∘-up-to

-- Size-preserving is closed under composition.

∘-closure = Up-to.∘-closure

-- It is not the case that every (monotone and extensive) up-to
-- technique is size-preserving.

¬up-to→size-preserving =
  Bisimilarity.Up-to.Counterexamples.¬monotone×extensive×up-to→size-preserving

-- There are at least two up-to techniques that are not
-- size-preserving (despite being monotone and extensive).

not-size-preserving =
  Bisimilarity.Up-to.Counterexamples.∃monotone×extensive×up-to×¬size-preserving

-- Monotone and compatible transformers are up-to techniques.

monotone→compatible→up-to = Up-to.monotone→compatible→up-to

-- If F is monotone and symmetric, and compatible for strong
-- similarity for some LTS, then F is compatible for strong
-- bisimilarity for this LTS.

compatible-for-similarity→compatible-for-bisimilarity =
  Up-to.Closure.compatible-for-similarity→compatible-for-bisimilarity

-- It is not in general the case that if F is monotone and symmetric,
-- and size-preserving for strong similarity for some LTS, then F is
-- size-preserving for strong bisimilarity for this LTS.

¬-compatible-for-similarity→compatible-for-bisimilarity =
  Up-to.Closure.¬-Size-preserving-⟷/⊗

------------------------------------------------------------------------
-- Section 7

-- The companion.

Companion = Up-to.Companion

-- Transformers below the companion.

Below-the-companion = Up-to.Below-the-companion

-- Transformers are below the companion if and only if they are
-- size-preserving.

below-the-companion⇔size-preserving =
  Up-to.below-the-companion⇔size-preserving

-- The companion is size-preserving.

companion-size-preserving = Up-to.companion-size-preserving

-- Compatibility.

Compatible = Up-to.Compatible

-- The large companion.

Companion₁ = Up-to.Companion₁

-- Monotone and compatible transformers are size-preserving.

compatible→size-preserving = Up-to.monotone→compatible→size-preserving

-- The large companion is below the small one.

companion₁⊆companion = Up-to.companion₁⊆companion

-- The small companion is monotone.

companion-monotone = Up-to.companion-monotone

-- The small companion is compatible if and only if it is below the
-- large one.

companion-compatible⇔companion⊆companion₁ =
  Up-to.companion-compatible⇔companion⊆companion₁

-- The small companion is compatible if certain assumptions (including
-- a strong version of excluded middle) are satisfied. However, at the
-- time of writing I don't know if these assumptions are consistent
-- with the variant of Agda that is used in this development.

companion-compatible = Up-to.companion-compatible

-- The identity function is below the companion.

id-below = Up-to.id-below

-- The interpretation ⟦ C ⟧ of a container C is below the
-- corresponding companion.

⟦⟧-below = Up-to.⟦⟧-below

-- The companion composed with itself is below the companion.

companion∘companion-below = Up-to.companion∘companion-below

-- An example: If F is below the companion, then ⟦ C ⟧ ∘ F is below
-- Companion ∘ Companion, which is below the companion.

below-the-companion-example = Up-to.below-the-companion-example

-- The greatest fixpoint is pointwise logically equivalent to the
-- companion applied to an empty relation.

ν⊆companion-⊥ = Up-to.ν⇔companion-⊥
companion-⊥⊆ν = Up-to.ν⇔companion-⊥

-- The companion is an up-to technique.

companion-up-to = Up-to.companion-up-to

------------------------------------------------------------------------
-- Section 8

-- Pous and Sangiorgi's lemma 6.1.3, part (2).

6-1-3-2 = Bisimilarity.CCS.6-1-3-2

-- Instances corresponding to some equational reasoning combinators
-- mentioned in the paper.

_∼′⟨_⟩′_ = Bisimilarity.Equational-reasoning-instances.trans∼′∼′
_∼⟨_⟩′_  = Bisimilarity.Equational-reasoning-instances.trans∼∼′
_■′      = Bisimilarity.Equational-reasoning-instances.reflexive∼′

-- The primed variant of _∣-cong_.

_∣-cong′_ = Bisimilarity.CCS._∣-cong′_

-- Replication preserves strong bisimilarity (already mentioned
-- above).

!-cong₂ = Bisimilarity.CCS.!-congP

-- Proofs showing that all the CCS process constructors preserve
-- strong bisimilarity (already mentioned above).

module Strong-bisimilarity-congruence₂ = Strong-bisimilarity-congruence

-- Proofs showing that all the CCS process constructors preserve
-- strong similarity. (For ∅ the proof is simply reflexivity.)

module Strong-similarity-congruence where

  _∣-cong_  = Similarity.CCS._∣-cong_
  ·-cong    = Similarity.CCS._·-cong_
  !-cong    = Similarity.CCS.!-cong_
  _⊕-cong_  = Similarity.CCS._⊕-cong_
  ⟨ν_⟩-cong = Similarity.CCS.⟨ν_⟩-cong
  ∅-cong    = Similarity.reflexive-≤

-- Proofs showing that all the CCS process constructors, except for
-- sum, preserve the expansion relation. (For ∅ the proof is simply
-- reflexivity.)

module Expansion-almost-congruence where

  _∣-cong_  = Expansion.CCS._∣-cong_
  ·-cong    = Expansion.CCS._·-cong_
  !-cong    = Expansion.CCS.!-cong_
  ⟨ν_⟩-cong = Expansion.CCS.⟨ν_⟩-cong
  ∅-cong    = Expansion.reflexive-≳

-- Proofs showing that all the CCS process constructors, except for
-- sum, preserve weak bisimilarity. (For ∅ the proof is simply
-- reflexivity.)

module Weak-bisimilarity-almost-congruence where

  _∣-cong_  = Bisimilarity.Weak.CCS._∣-cong_
  ·-cong    = Bisimilarity.Weak.CCS._·-cong_
  !-cong    = Bisimilarity.Weak.CCS.!-cong_
  ⟨ν_⟩-cong = Bisimilarity.Weak.CCS.⟨ν_⟩-cong
  ∅-cong    = Bisimilarity.Weak.reflexive-≈

------------------------------------------------------------------------
-- Section 9

-- Weak bisimilarity for the delay monad.
--
-- Note that, unlike in the paper, strong bisimilarity, weak
-- bisimilarity and the expansion relation are defined as a single
-- family (with an extra index).

[_]_≈D_  = Delay-monad.Bisimilarity.[_]_≈_
[_]_≈′D_ = Delay-monad.Bisimilarity.[_]_≈′_

-- This definition is pointwise logically equivalent, in a
-- size-preserving way, to the one obtained from the LTS for the delay
-- monad.

direct⇔indirect = Bisimilarity.Weak.Delay-monad.direct⇔indirect

-- Capretta's definition of weak bisimilarity, formulated using sized
-- types.

Capretta's-weak-bisimilarity =
  Delay-monad.Bisimilarity.Alternative.[_]_≈₃_

-- Capretta's definition is pointwise logically equivalent, in a
-- size-preserving way, to the one used in the paper.

direct⇔Capretta = Delay-monad.Bisimilarity.Alternative.≈⇔≈₃

------------------------------------------------------------------------
-- Section 9.1

-- Weak bisimilarity is transitive for every LTS.

transitiveʷ-lts = Bisimilarity.Weak.transitive-≈

-- The later constructors can be removed.
--
-- (Two of the proofs are more general than the corresponding proofs
-- in the paper.)

laterʳ⁻¹ = Delay-monad.Bisimilarity.laterʳ⁻¹
laterˡ⁻¹ = Delay-monad.Bisimilarity.laterˡ⁻¹
later⁻¹  = Delay-monad.Bisimilarity.later⁻¹

-- Weak bisimilarity for the delay monad is transitive.
--
-- (The proof is not quite identical to the one in the paper.)

transitiveʷ-now   = Delay-monad.Bisimilarity.transitive-≈-now
transitiveʷ-later = Delay-monad.Bisimilarity.transitive-≈-later
transitiveʷ       = Delay-monad.Bisimilarity.transitive-≈

------------------------------------------------------------------------
-- Section 9.2

-- If transitivity of weak bisimilarity for the delay monad is
-- size-preserving in both arguments, then weak bisimilarity is
-- trivial.

size-preserving→trivial =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈→trivial

-- Weak bisimilarity for the delay monad is reflexive.

_∎ʷ = Delay-monad.Bisimilarity.reflexive

-- The computation now x is not weakly bisimilar to never.
--
-- (The proof is more general than the one in the paper.)

now≉never = Delay-monad.Bisimilarity.now≉never

-- If transitivity of weak bisimilarity for the delay monad is
-- size-preserving in both arguments, then the carrier type is
-- uninhabited.

not-size-preservingʷ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈→uninhabited

-- If transitivity of weak bisimilarity is size-preserving in the
-- first argument, then weak bisimulations up to weak bisimilarity are
-- contained in weak bisimilarity.

size-preserving→weak-bisimulations-up-to-weak-bisimilarity-works =
  Bisimilarity.Weak.Up-to.size-preserving-transitivity→up-to-weak-bisimilarity-up-to

-- The Drop-later predicate.

Drop-later = Delay-monad.Bisimilarity.Negative.Laterˡ⁻¹-∼≈

-- Drop-later A implies that A is not inhabited, and vice versa.
--
-- The implementation of basic-counterexample in the paper is
-- different, because it does not include the "and vice versa" part.

basic-counterexample =
  Delay-monad.Bisimilarity.Negative.size-preserving-laterˡ⁻¹-∼≈⇔uninhabited

-- If there is a transitivity-like proof that takes a fully defined
-- weak bisimilarity proof and a strong bisimilarity proof of size i
-- to a weak bisimilarity proof of size i, then the carrier type is
-- uninhabited (and vice versa).
--
-- The implementation is superficially different from the one in the
-- paper (except for the "vice versa" part, which is not present in
-- the paper).

not-size-preservingʷˢ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈∼ʳ⇔uninhabited

-- A size-preserving translation from strong to weak bisimilarity for
-- the delay monad.
--
-- (The implementation is more general than the one in the paper.)

strong-to-weak = Delay-monad.Bisimilarity.∼→

-- Size-preserving translations from strong bisimilarity to expansion
-- and from expansion to weak bisimilarity for any LTS.

strong-to-expansion = Expansion.∼⇒≳
expansion-to-weak   = Bisimilarity.Weak.≳⇒≈

-- If there is a proof of transitivity that takes a fully defined weak
-- bisimilarity proof and a weak bisimilarity proof of size i to a
-- weak bisimilarity proof of size i, then the carrier type is
-- uninhabited (and vice versa).
--
-- The implementation is superficially different from the one in the
-- paper (except for the "vice versa" part, which is not present in
-- the paper).

not-size-preservingʷʳ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈ʳ⇔uninhabited

-- Size-preserving symmetry proofs for strong and weak bisimilarity.
--
-- (Actually a single proof that works for both relations.)

symmetryˢ = Delay-monad.Bisimilarity.symmetric
symmetryʷ = Delay-monad.Bisimilarity.symmetric

-- If there is a proof of transitivity that takes a strong (or
-- alternatively weak) bisimilarity proof of size i and a fully
-- defined weak bisimilarity proof to a weak bisimilarity proof of
-- size i, then the carrier type is uninhabited (and vice versa).

not-size-preservingˢʷ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-∼≈ˡ⇔uninhabited
not-size-preservingʷˡ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈ˡ⇔uninhabited

-- If the carrier type is not inhabited, then weak bisimilarity is
-- trivial.
--
-- (The proof is more general than the one in the paper.)

trivial = Delay-monad.Bisimilarity.uninhabited→trivial

-- If the type A is uninhabited, then Drop-later A is inhabited (and
-- vice versa).

basic-counterexample′ =
  Delay-monad.Bisimilarity.Negative.size-preserving-laterˡ⁻¹-∼≈⇔uninhabited

-- If the carrier type is uninhabited, then there is a fully
-- size-preserving transitivity proof for weak bisimilarity (and vice
-- versa).

size-preservingʷ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈⇔uninhabited

-- Size-preserving transitivity-like proofs involving strong and weak
-- bisimilarity.
--
-- (The type signatures of the proofs are more general than those
-- given in the paper.)

transitiveˢʷ = Delay-monad.Bisimilarity.transitive-∼ˡ
transitiveʷˢ = Delay-monad.Bisimilarity.transitive-∞∼ʳ

-- A direct definition of expansion for the delay monad.

[_]_≳D_ = Delay-monad.Bisimilarity.[_]_≳_

-- The direct definition of expansion for the delay monad is pointwise
-- logically equivalent, in a size-preserving way, to the one obtained
-- from the LTS for the delay monad.

direct⇔indirect-expansion = Expansion.Delay-monad.direct⇔indirect

-- Size-preserving transitivity-like proofs involving the direct
-- definitions of weak bisimilarity and expansion for the delay monad.
--
-- (The type signatures of the first three proofs are more general
-- than those given in the paper.)

transitiveᵉˢ = Delay-monad.Bisimilarity.transitive-∼ʳ
transitiveᵉ  = Delay-monad.Bisimilarity.transitive-≳ˡ
transitiveᵉʷ = Delay-monad.Bisimilarity.transitive-≳ˡ
transitiveʷᵉ = Delay-monad.Bisimilarity.transitive-≈≲

-- Size-preserving transitivity-like proofs involving weak
-- bisimilarity and expansion defined for an arbitrary LTS.

transitiveᵉˢ-lts = Expansion.transitive-≳∼
transitiveᵉ-lts  = Expansion.transitive-≳
transitiveᵉʷ-lts = Bisimilarity.Weak.transitive-≳≈
transitiveʷᵉ-lts = Bisimilarity.Weak.transitive-≈≲

-- Negative results related to expansion.

not-size-preservingˢᵉ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-∼≳ˡ⇔uninhabited
not-size-preservingᵉʷ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≳≈ˡ⇔uninhabited
not-size-preservingʷᵉ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈≳ˡ⇔uninhabited

-- The functions transitiveᵉ, transitiveᵉʷ and transitiveʷᵉ cannot in
-- general be made fully size-preserving.

not-fully-size-preservingᵉ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≳⇔uninhabited
not-fully-size-preservingᵉʷ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≳≈⇔uninhabited
not-fully-size-preservingʷᵉ =
  Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-≈≲⇔uninhabited

-- Up to expansion.

Up-to-expansion =
  Bisimilarity.Weak.Up-to.Up-to-expansion
up-to-expansion-size-preserving =
  Bisimilarity.Weak.Up-to.up-to-expansion-size-preserving

-- Relations that satisfy the diagrams of the variant of up to
-- expansion where two occurrences of the expansion relation have been
-- replaced by weak bisimilarity are contained in weak bisimilarity.

variant-of-up-to-expansion = Bisimilarity.Weak.Up-to.6-5-2-4

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to