text:
------------------------------------------------------------------------
-- A variant of weak bisimilarity that can be used to relate the
-- number of steps in two computations
------------------------------------------------------------------------

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

open import Prelude hiding (_+_; _*_)

module Delay-monad.Quantitative-weak-bisimilarity {a} {A : Type a} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Conat equality-with-J as Conat
  using (Conat; zero; suc; force; ⌜_⌝; _+_; _*_;
         [_]_≤_; step-≤; step-∼≤; _∎≤; step-∼; _∎∼)
open import Function-universe equality-with-J as F hiding (id; _∘_)

open import Delay-monad
open import Delay-monad.Bisimilarity as B
  using (now; later; laterˡ; laterʳ; force)

------------------------------------------------------------------------
-- The relation

mutual

  -- Quantitative weak bisimilarity. [ ∞ ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y
  -- is a variant of x B.≈ y for which the number of later
  -- constructors in x is bounded by nˡ plus 1 + mˡ times the number
  -- of later constructors in y, and the number of later constructors
  -- in y is bounded by nʳ plus 1 + mʳ times the number of later
  -- constructors in x (see ≈⇔≈×steps≤steps² below).

  infix 4 [_∣_∣_∣_∣_]_≈_ [_∣_∣_∣_∣_]_≈′_

  data [_∣_∣_∣_∣_]_≈_
         (i : Size) (mˡ mʳ : Conat ∞) :
         Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a where
    now    : ∀ {x nˡ nʳ} → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] now x ≈ now x
    later  : ∀ {x y nˡ nʳ} →
             [ i ∣ mˡ ∣ mʳ ∣ nˡ + mˡ ∣ nʳ + mʳ ] x .force ≈′ y .force →
             [ i ∣ mˡ ∣ mʳ ∣ nˡ      ∣ nʳ      ] later x  ≈  later y
    laterˡ : ∀ {x y nˡ nʳ} →
             [ i ∣ mˡ ∣ mʳ ∣ nˡ .force ∣ nʳ ] x .force ≈ y →
             [ i ∣ mˡ ∣ mʳ ∣ suc nˡ    ∣ nʳ ] later x  ≈ y
    laterʳ : ∀ {x y nˡ nʳ} →
             [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ .force ] x ≈ y .force →
             [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ suc nʳ    ] x ≈ later y

  record [_∣_∣_∣_∣_]_≈′_
           (i : Size) (mˡ mʳ nˡ nʳ : Conat ∞)
           (x y : Delay A ∞) : Type a where
    coinductive
    field
      force : {j : Size< i} → [ j ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y

open [_∣_∣_∣_∣_]_≈′_ public

-- Specialised variants of [_∣_∣_∣_∣_]_≈_ and [_∣_∣_∣_∣_]_≈′_.

infix 4 [_∣_∣_]_≈_ [_∣_∣_]_≈′_

[_∣_∣_]_≈_ : Size → Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ mˡ ∣ mʳ ] x ≈ y = [ i ∣ mˡ ∣ mʳ ∣ zero ∣ zero ] x ≈ y

[_∣_∣_]_≈′_ : Size → Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ mˡ ∣ mʳ ] x ≈′ y = [ i ∣ mˡ ∣ mʳ ∣ zero ∣ zero ] x ≈′ y

-- Quantitative expansion.

infix 4 [_∣_∣_]_≳_ [_∣_∣_]_≳′_ [_∣_]_≳_ [_∣_]_≳′_

[_∣_∣_]_≳_ : Size → Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ∣ n ] x ≳ y = [ i ∣ m ∣ zero ∣ n ∣ zero ] x ≈ y

[_∣_∣_]_≳′_ : Size → Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ∣ n ] x ≳′ y = [ i ∣ m ∣ zero ∣ n ∣ zero ] x ≈′ y

[_∣_]_≳_ : Size → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ] x ≳ y = [ i ∣ m ∣ zero ] x ≳ y

[_∣_]_≳′_ : Size → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ] x ≳′ y = [ i ∣ m ∣ zero ] x ≳′ y

-- The converse of quantitative expansion.

infix 4 [_∣_∣_]_≲_ [_∣_∣_]_≲′_ [_∣_]_≲_ [_∣_]_≲′_

[_∣_∣_]_≲_ : Size → Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ∣ n ] x ≲ y = [ i ∣ m ∣ n ] y ≳ x

[_∣_∣_]_≲′_ : Size → Conat ∞ → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ∣ n ] x ≲′ y = [ i ∣ m ∣ n ] y ≳′ x

[_∣_]_≲_ : Size → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ] x ≲ y = [ i ∣ m ] y ≳ x

[_∣_]_≲′_ : Size → Conat ∞ → Delay A ∞ → Delay A ∞ → Type a
[ i ∣ m ] x ≲′ y = [ i ∣ m ] y ≳′ x

------------------------------------------------------------------------
-- Conversions

-- Weakening.

weaken :
  ∀ {i mˡ mˡ′ mʳ mʳ′ nˡ nˡ′ nʳ nʳ′ x y} →
  [ ∞ ] mˡ ≤ mˡ′ → [ ∞ ] mʳ ≤ mʳ′ →
  [ ∞ ] nˡ ≤ nˡ′ → [ ∞ ] nʳ ≤ nʳ′ →
  [ i ∣ mˡ  ∣ mʳ  ∣ nˡ  ∣ nʳ  ] x ≈ y →
  [ i ∣ mˡ′ ∣ mʳ′ ∣ nˡ′ ∣ nʳ′ ] x ≈ y
weaken pˡ pʳ = λ where
  qˡ       qʳ       now        → now
  (suc qˡ) qʳ       (laterˡ r) → laterˡ (weaken pˡ pʳ (qˡ .force) qʳ r)
  qˡ       (suc qʳ) (laterʳ r) → laterʳ (weaken pˡ pʳ qˡ (qʳ .force) r)
  qˡ       qʳ       (later r)  → later λ { .force →
                                   weaken pˡ pʳ
                                     (qˡ Conat.+-mono pˡ)
                                     (qʳ Conat.+-mono pʳ)
                                     (r .force) }

weakenˡʳ :
  ∀ {i mˡ mʳ nˡ nˡ′ nʳ nʳ′ x y} →
  [ ∞ ] nˡ ≤ nˡ′ → [ ∞ ] nʳ ≤ nʳ′ →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ  ∣ nʳ  ] x ≈ y →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ′ ∣ nʳ′ ] x ≈ y
weakenˡʳ = weaken (_ ∎≤) (_ ∎≤)

weakenˡ :
  ∀ {i mˡ mʳ nˡ nˡ′ nʳ x y} →
  [ ∞ ] nˡ ≤ nˡ′ →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ  ∣ nʳ ] x ≈ y →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ′ ∣ nʳ ] x ≈ y
weakenˡ p = weakenˡʳ p (_ ∎≤)

weakenʳ :
  ∀ {i mˡ mʳ nˡ nʳ nʳ′ x y} →
  [ ∞ ] nʳ ≤ nʳ′ →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ  ] x ≈ y →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ′ ] x ≈ y
weakenʳ p = weakenˡʳ (_ ∎≤) p

-- Strong bisimilarity is contained in quantitative weak bisimilarity.

∼→≈ : ∀ {i mˡ mʳ nˡ nʳ x y} →
      B.[ i ] x ∼ y → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y
∼→≈ now       = now
∼→≈ (later p) = later λ { .force → ∼→≈ (p .force) }

-- Quantitative expansion is contained in expansion.

≳→≳ : ∀ {i m n x y} →
      [ i ∣ m ∣ n ] x ≳ y → B.[ i ] x ≳ y
≳→≳ now        = now
≳→≳ (later p)  = later λ { .force → ≳→≳ (p .force) }
≳→≳ (laterˡ p) = laterˡ (≳→≳ p)

-- Quantitative weak bisimilarity is contained in weak bisimilarity.

≈→≈ : ∀ {i mˡ mʳ nˡ nʳ x y} →
      [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y → B.[ i ] x ≈ y
≈→≈ now        = now
≈→≈ (later p)  = later λ { .force → ≈→≈ (p .force) }
≈→≈ (laterˡ p) = laterˡ (≈→≈ p)
≈→≈ (laterʳ p) = laterʳ (≈→≈ p)

-- In some cases expansion is contained in quantitative expansion.

≳→≳-steps :
  ∀ {m x y i} → B.[ i ] x ≳ y → [ i ∣ m ∣ steps x ] x ≳ y
≳→≳-steps     now               = now
≳→≳-steps     (laterˡ p)        = laterˡ (≳→≳-steps p)
≳→≳-steps {m} (later {x = x} p) = later λ { .force →
  weakenˡ lemma (≳→≳-steps (p .force)) }
  where
  lemma =
    steps (x .force)     ≤⟨ Conat.≤suc ⟩
    steps (later x)      ≤⟨ Conat.m≤m+n ⟩
    steps (later x) + m  ∎≤

-- In some cases weak bisimilarity is contained in quantitative weak
-- bisimilarity.

≈→≈-steps :
  ∀ {mˡ mʳ x y i} →
  B.[ i ] x ≈ y → [ i ∣ mˡ ∣ mʳ ∣ steps x ∣ steps y ] x ≈ y
≈→≈-steps           now                       = now
≈→≈-steps           (laterˡ p)                = laterˡ (≈→≈-steps p)
≈→≈-steps           (laterʳ p)                = laterʳ (≈→≈-steps p)
≈→≈-steps {mˡ} {mʳ} (later {x = x} {y = y} p) = later λ { .force →
  weakenˡʳ x-lemma y-lemma (≈→≈-steps (p .force)) }
  where
  x-lemma =
    steps (x .force)      ≤⟨ Conat.≤suc ⟩
    steps (later x)       ≤⟨ Conat.m≤m+n ⟩
    steps (later x) + mˡ  ∎≤

  y-lemma =
    steps (y .force)      ≤⟨ Conat.≤suc ⟩
    steps (later y)       ≤⟨ Conat.m≤m+n ⟩
    steps (later y) + mʳ  ∎≤

-- In some cases quantitative weak bisimilarity is contained in strong
-- bisimilarity.

never≈→∼ :
  ∀ {i mˡ mʳ nˡ nʳ x} →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] never ≈ x → B.[ i ] never ∼ x
never≈→∼ (later  p) = later λ { .force → never≈→∼ (p .force) }
never≈→∼ (laterˡ p) = never≈→∼ p
never≈→∼ (laterʳ p) = later λ { .force → never≈→∼ p }

≈never→∼ :
  ∀ {i mˡ mʳ nˡ nʳ x} →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ never → B.[ i ] x ∼ never
≈never→∼ (later  p) = later λ { .force → ≈never→∼ (p .force) }
≈never→∼ (laterˡ p) = later λ { .force → ≈never→∼ p }
≈never→∼ (laterʳ p) = ≈never→∼ p

≈→∼ : ∀ {i x y} → [ i ∣ zero ∣ zero ] x ≈ y → B.[ i ] x ∼ y
≈→∼ now       = now
≈→∼ (later p) = later λ { .force → ≈→∼ (p .force) }

------------------------------------------------------------------------
-- Reflexivity, symmetry/antisymmetry, transitivity

-- Quantitative weak bisimilarity is reflexive.

reflexive-≈ : ∀ {i mˡ mʳ nˡ nʳ} x → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ x
reflexive-≈ (now _)   = now
reflexive-≈ (later x) = later λ { .force → reflexive-≈ (x .force) }

-- Quantitative weak bisimilarity is symmetric (in a certain sense).

symmetric-≈ :
  ∀ {i mˡ mʳ nˡ nʳ x y} →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y →
  [ i ∣ mʳ ∣ mˡ ∣ nʳ ∣ nˡ ] y ≈ x
symmetric-≈ now        = now
symmetric-≈ (later p)  = later λ { .force → symmetric-≈ (p .force) }
symmetric-≈ (laterˡ p) = laterʳ (symmetric-≈ p)
symmetric-≈ (laterʳ p) = laterˡ (symmetric-≈ p)

-- Four variants of transitivity.

transitive-≳∼ :
  ∀ {i m n x y z} →
  [ i ∣ m ∣ n ] x ≳ y → B.[ i ] y ∼ z → [ i ∣ m ∣ n ] x ≳ z
transitive-≳∼ = λ where
  now        now       → now
  (laterˡ p) q         → laterˡ (transitive-≳∼ p q)
  (later  p) (later q) → later λ { .force →
                           transitive-≳∼ (p .force) (q .force) }

transitive-∼≲ :
  ∀ {i m n x y z} →
  B.[ i ] x ∼ y → [ i ∣ m ∣ n ] y ≲ z → [ i ∣ m ∣ n ] x ≲ z
transitive-∼≲ p q = transitive-≳∼ q (B.symmetric p)

transitive-≈∼ :
  ∀ {i mˡ mʳ nˡ nʳ x y z} →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y → y B.∼ z →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ z
transitive-≈∼ = λ where
  now        now       → now
  (later  p) (later q) → later λ { .force →
                           transitive-≈∼ (p .force) (q .force) }
  (laterˡ p) q         → laterˡ (transitive-≈∼ p q)
  (laterʳ p) (later q) → laterʳ (transitive-≈∼ p (q .force))

transitive-∼≈ :
  ∀ {i mˡ mʳ nˡ nʳ x y z} →
  x B.∼ y → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] y ≈ z →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ z
transitive-∼≈ = λ where
  now       now        → now
  (later p) (later q)  → later λ { .force →
                           transitive-∼≈ (p .force) (q .force) }
  (later p) (laterˡ q) → laterˡ (transitive-∼≈ (p .force) q)
  p         (laterʳ q) → laterʳ (transitive-∼≈ p q)

-- Equational reasoning combinators.

infix  -1 _∎ˢ
infixr -2 step-∼≈ˢ step-≳∼ˢ step-≈∼ˢ _≳⟨⟩ˢ_ step-≡≈ˢ _∼⟨⟩ˢ_

_∎ˢ : ∀ {i mˡ mʳ nˡ nʳ} x → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ x
_∎ˢ = reflexive-≈

step-∼≈ˢ : ∀ {i mˡ mʳ nˡ nʳ} x {y z} →
           [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] y ≈ z → x B.∼ y →
           [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ z
step-∼≈ˢ _ y≈z x∼y = transitive-∼≈ x∼y y≈z

syntax step-∼≈ˢ x y≈z x∼y = x ∼⟨ x∼y ⟩ˢ y≈z

step-≳∼ˢ : ∀ {i m n} x {y z} →
           B.[ i ] y ∼ z → [ i ∣ m ∣ n ] x ≳ y →
           [ i ∣ m ∣ n ] x ≳ z
step-≳∼ˢ _ y∼z x≳y = transitive-≳∼ x≳y y∼z

syntax step-≳∼ˢ x y∼z x≳y = x ≳⟨ x≳y ⟩ˢ y∼z

step-≈∼ˢ : ∀ {i mˡ mʳ nˡ nʳ} x {y z} →
           y B.∼ z → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y →
           [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ z
step-≈∼ˢ _ y∼z x≈y = transitive-≈∼ x≈y y∼z

syntax step-≈∼ˢ x y∼z x≈y = x ≈⟨ x≈y ⟩ˢ y∼z

_≳⟨⟩ˢ_ : ∀ {i mˡ mʳ nˡ nʳ} x {y} →
         [ i ∣ mˡ ∣ mʳ ∣ nˡ         ∣ nʳ ] drop-later x ≈ y →
         [ i ∣ mˡ ∣ mʳ ∣ ⌜ 1 ⌝ + nˡ ∣ nʳ ] x ≈ y
now _   ≳⟨⟩ˢ p = weakenˡ Conat.≤suc p
later _ ≳⟨⟩ˢ p = laterˡ p

step-≡≈ˢ : ∀ {i mˡ mʳ nˡ nʳ} x {y z} →
           [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] y ≈ z → x ≡ y →
           [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ z
step-≡≈ˢ _ y≈z refl = y≈z

syntax step-≡≈ˢ x y≈z x≡y = x ≡⟨ x≡y ⟩ˢ y≈z

_∼⟨⟩ˢ_ : ∀ {i mˡ mʳ nˡ nʳ} x {y} →
         [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y →
         [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y
_ ∼⟨⟩ˢ x≈y = x≈y

------------------------------------------------------------------------
-- Some results related to the steps function

-- If y is a quantitative expansion of x, then it contains at least as
-- many later constructors as x.

steps-mono :
  ∀ {i m n x y} → [ i ∣ m ∣ n ] x ≲ y → [ i ] steps x ≤ steps y
steps-mono = B.steps-mono ∘ ≳→≳

-- If [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y holds, then the number of later
-- constructors in x is bounded by nˡ plus 1 + mˡ times the number of
-- later constructors in y.

steps-+-*ʳ :
  ∀ {mˡ mʳ nˡ nʳ i x y} →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y →
  [ i ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y
steps-+-*ʳ {mˡ} {mʳ} {nˡ} {nʳ} = λ where
  now → zero

  (later {x = x} {y = y} p) →
    steps (later x)                                                 ∼⟨ suc (λ { .force → _ ∎∼ }) ⟩≤
    suc (λ { .force → steps (x .force) })                           ≤⟨ suc (λ { .force → steps-+-*ʳ (p .force) }) ⟩
    suc (λ { .force → nˡ + mˡ + (⌜ 1 ⌝ + mˡ) * steps (y .force) })  ∼⟨ suc (λ { .force → Conat.symmetric-∼ (Conat.+-assoc nˡ) }) ⟩≤
    ⌜ 1 ⌝ + nˡ + (mˡ + (⌜ 1 ⌝ + mˡ) * steps (y .force))             ∼⟨ Conat.suc+∼+suc ⟩≤
    nˡ + ((⌜ 1 ⌝ + mˡ) + (⌜ 1 ⌝ + mˡ) * steps (y .force))           ∼⟨ (nˡ ∎∼) Conat.+-cong Conat.symmetric-∼ Conat.*suc∼+* ⟩≤
    nˡ + (⌜ 1 ⌝ + mˡ) * steps (later y)                             ∎≤

  (laterˡ {x = x} {y = y} {nˡ = nˡ} p) →
    steps (later x)                               ∼⟨ suc (λ { .force → _ ∎∼ }) ⟩≤
    ⌜ 1 ⌝ + steps (x .force)                      ≤⟨ (_ Conat.∎≤) Conat.+-mono steps-+-*ʳ p ⟩
    ⌜ 1 ⌝ + (nˡ .force + (⌜ 1 ⌝ + mˡ) * steps y)  ∼⟨ suc (λ { .force → _ ∎∼ }) ⟩≤
    suc nˡ + (⌜ 1 ⌝ + mˡ) * steps y               ∎≤

  (laterʳ {x = x} {y = y} {nʳ = nʳ} p) →
    steps x                                                ≤⟨ steps-+-*ʳ p ⟩
    nˡ + (⌜ 1 ⌝ + mˡ) * steps (y .force)                   ≤⟨ (nˡ ∎≤) Conat.+-mono Conat.m≤n+m ⟩
    nˡ + ((⌜ 1 ⌝ + mˡ) + (⌜ 1 ⌝ + mˡ) * steps (y .force))  ∼⟨ (nˡ ∎∼) Conat.+-cong Conat.symmetric-∼ Conat.*suc∼+* ⟩≤
    nˡ + (⌜ 1 ⌝ + mˡ) * steps (later y)                    ∎≤

-- If [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y holds, then the number of later
-- constructors in y is bounded by nʳ plus 1 + mʳ times the number of
-- later constructors in x.

steps-+-*ˡ :
  ∀ {mˡ mʳ nˡ nʳ i x y} →
  [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y →
  [ i ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x
steps-+-*ˡ = steps-+-*ʳ ∘ symmetric-≈

-- [ ∞ ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y holds iff x and y are weakly
-- bisimilar and the number of later constructors in x and y are
-- related in a certain way.

≈⇔≈×steps≤steps² :
  ∀ {mˡ mʳ nˡ nʳ x y} →
  [ ∞ ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y ⇔
  x B.≈ y ×
  [ ∞ ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y ×
  [ ∞ ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x
≈⇔≈×steps≤steps² {mˡ} {mʳ} {x = x} {y} = record
  { to   = λ p → ≈→≈ p , steps-+-*ʳ p , steps-+-*ˡ p
  ; from = λ { (p , q , r) → from p q r }
  }
  where
  from-lemma :
    ∀ {m n} {x y : Delay′ A ∞} {i} {j : Size< i} →
    [ i ] steps (later x) ≤ n + (⌜ 1 ⌝ + m) * steps (later y) →
    [ j ] steps (x .force) ≤ n + m + (⌜ 1 ⌝ + m) * steps (y .force)
  from-lemma {m} {n} {x} {y} hyp = Conat.cancel-suc-≤ lemma .force
    where
    lemma =
      ⌜ 1 ⌝ + steps (x .force)                            ∼⟨ suc (λ { .force → _ ∎∼ }) ⟩≤
      steps (later x)                                     ≤⟨ hyp ⟩
      n + (⌜ 1 ⌝ + m) * steps (later y)                   ∼⟨ (n ∎∼) Conat.+-cong Conat.*suc∼+* ⟩≤
      n + ((⌜ 1 ⌝ + m) + (⌜ 1 ⌝ + m) * steps (y .force))  ∼⟨ Conat.symmetric-∼ Conat.suc+∼+suc ⟩≤
      ⌜ 1 ⌝ + n + (m + (⌜ 1 ⌝ + m) * steps (y .force))    ∼⟨ suc (λ { .force → _ ∎∼ }) ⟩≤
      ⌜ 1 ⌝ + (n + (m + (⌜ 1 ⌝ + m) * steps (y .force)))  ∼⟨ suc (λ { .force → Conat.+-assoc n }) ⟩≤
      ⌜ 1 ⌝ + (n + m + (⌜ 1 ⌝ + m) * steps (y .force))    ∎≤

  from :
    ∀ {nˡ nʳ i x y} →
    B.[ i ] x ≈ y →
    [ ∞ ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y →
    [ ∞ ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x →
    [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y
  from now _ _ = now

  from (later p) q r = later λ { .force →
    from (p .force) (from-lemma q) (from-lemma r) }

  from (laterˡ {y = later _} p) q r = later λ { .force →
    from (B.laterʳ⁻¹ p) (from-lemma q) (from-lemma r) }

  from (laterʳ {x = later _} p) q r = later λ { .force →
    from (B.laterˡ⁻¹ p) (from-lemma q) (from-lemma r) }

  from {nˡ = zero}  (laterˡ {y = now _} p) ()
  from {nˡ = suc _} (laterˡ {y = now _} p) (suc q) _ =
    laterˡ (from p (q .force) zero)

  from {nʳ = zero}  (laterʳ {x = now _} p) _ ()
  from {nʳ = suc _} (laterʳ {x = now _} p) _ (suc r) =
    laterʳ (from p zero (r .force))

-- [ ∞ ∣ m ∣ n ] x ≳ y holds iff x is an expansion of y and the number
-- of later constructors in x and y are related in a certain way.

≳⇔≳×steps≤steps :
  ∀ {m n x y} →
  [ ∞ ∣ m ∣ n ] x ≳ y ⇔
  x B.≳ y × [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y
≳⇔≳×steps≤steps {m} {n} {x} {y} =
  [ ∞ ∣ m ∣ n ] x ≳ y                                  ↝⟨ ≈⇔≈×steps≤steps² ⟩

  x B.≈ y ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y ×
  [ ∞ ] steps y ≤ (⌜ 1 ⌝ + ⌜ 0 ⌝) * steps x            ↝⟨ F.id ×-cong F.id ×-cong (_ ∎∼) Conat.≤-cong-∼ lemma ⟩

  x B.≈ y ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y ×
  [ ∞ ] steps y ≤ steps x                              ↝⟨ record { to = B.symmetric; from = B.symmetric } ×-cong from-isomorphism ×-comm ⟩

  y B.≈ x ×
  [ ∞ ] steps y ≤ steps x ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y            ↔⟨ ×-assoc ⟩

  (y B.≈ x ×
   [ ∞ ] steps y ≤ steps x) ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y            ↝⟨ inverse B.≲⇔≈×steps≤steps ×-cong F.id ⟩□

  x B.≳ y × [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y  □
  where
  lemma =
    (⌜ 1 ⌝ + ⌜ 0 ⌝) * steps x  ∼⟨ suc (λ { .force → _ ∎∼ }) Conat.*-cong (_ ∎∼) ⟩
    ⌜ 1 ⌝ * steps x            ∼⟨ Conat.*-left-identity _ ⟩
    steps x                    ∎∼

-- [ ∞ ∣ m ∣ n ] x ≳ y holds iff x is weakly bisimilar to y and the
-- number of later constructors in x and y are related in a certain
-- way.

≳⇔≈×steps≤steps² :
  ∀ {m n x y} →
  [ ∞ ∣ m ∣ n ] x ≳ y ⇔
  x B.≈ y ×
  [ ∞ ] steps y ≤ steps x ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y
≳⇔≈×steps≤steps² {m} {n} {x} {y} =
  [ ∞ ∣ m ∣ n ] x ≳ y                        ↝⟨ ≳⇔≳×steps≤steps ⟩

  x B.≳ y ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y  ↝⟨ B.≲⇔≈×steps≤steps ×-cong F.id ⟩

  (y B.≈ x ×
   [ ∞ ] steps y ≤ steps x) ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y  ↔⟨ inverse ×-assoc ⟩

  y B.≈ x ×
  [ ∞ ] steps y ≤ steps x ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y  ↝⟨ record { to = B.symmetric; from = B.symmetric } ×-cong F.id ⟩□

  x B.≈ y ×
  [ ∞ ] steps y ≤ steps x ×
  [ ∞ ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y  □

-- The left-to-right direction of ≳⇔≳×steps≤steps can be made
-- size-preserving.

≳→≳×steps≤steps :
  ∀ {i m n x y} →
  [ i ∣ m ∣ n ] x ≳ y →
  B.[ i ] x ≳ y × [ i ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y
≳→≳×steps≤steps x≳y = ≳→≳ x≳y , steps-+-*ʳ x≳y

-- The right-to-left direction of ≳⇔≳×steps≤steps can be made
-- size-preserving iff A is uninhabited.

≳×steps≤steps→≳⇔uninhabited :
  (∀ {i m n x y} →
   B.[ i ] x ≳ y ×
   [ i ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y →
   [ i ∣ m ∣ n ] x ≳ y)
    ⇔
  ¬ A
≳×steps≤steps→≳⇔uninhabited = record
  { to   = flip to
  ; from =
    ¬ A                                           ↝⟨ (λ ¬A {_ _ _ _ _} → ∼→≈ (B.uninhabited→trivial ¬A _ _)) ⟩

    (∀ {i m n x y} → [ i ∣ m ∣ n ] x ≳ y)         ↝⟨ (λ hyp {_ _ _ _ _} _ → hyp {_}) ⟩□

    (∀ {i m n x y} →
     B.[ i ] x ≳ y ×
     [ i ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y →
     [ i ∣ m ∣ n ] x ≳ y)                         □
  }
  where
  strengthen-≳now :
    ∀ {i m n x y} →
    [ i ∣ m ∣ n ] x ≳ now y →
    [ ∞ ∣ m ∣ n ] x ≳ now y
  strengthen-≳now now        = now
  strengthen-≳now (laterˡ p) = laterˡ (strengthen-≳now p)

  to :
    A →
    ¬ (∀ {i m n x y} →
       B.[ i ] x ≳ y ×
       [ i ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y →
       [ i ∣ m ∣ n ] x ≳ y)
  to x =
    (∀ {i m n x y} →
     B.[ i ] x ≳ y ×
     [ i ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y →
     [ i ∣ m ∣ n ] x ≳ y)                                         ↝⟨ (λ hyp → curry hyp) ⟩

    (∀ {i m n} →
     B.[ i ] f m ≳ now x →
     [ i ] steps (f m) ≤ n + zero →
     [ i ∣ zero ∣ n ] f m ≳ now x)                                ↝⟨ (λ hyp {_ _ _} p → hyp (≳now _) (complicate p)) ⟩

    (∀ {i m n} → [ i ] ⌜ m ⌝ ≤ n → [ i ∣ zero ∣ n ] f m ≳ now x)  ↝⟨ strengthen-≳now ∘_ ⟩

    (∀ {i m n} → [ i ] ⌜ m ⌝ ≤ n → [ ∞ ∣ zero ∣ n ] f m ≳ now x)  ↝⟨ (λ hyp {_ _ _} p → steps-+-*ʳ (hyp p)) ⟩

    (∀ {i m n} → [ i ] ⌜ m ⌝ ≤ n → [ ∞ ] steps (f m) ≤ n + zero)  ↝⟨ (λ hyp {_ _ _} p → simplify (hyp p)) ⟩

    (∀ {i m n} → [ i ] ⌜ m ⌝ ≤ n → [ ∞ ] ⌜ m ⌝ ≤ n)               ↝⟨ (λ hyp → hyp) ⟩

    (∀ {i} → [ i ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝ → [ ∞ ] ⌜ 2 ⌝ ≤ ⌜ 1 ⌝)           ↝⟨ Conat.no-strengthening-≤-21 ⟩□

    ⊥                                                             □
    where
    f : ∀ {i} → ℕ → Delay A i
    f zero    = now x
    f (suc n) = later λ { .force → f n }

    ≳now : ∀ {i} n → B.[ i ] f n ≳ now x
    ≳now zero    = now
    ≳now (suc n) = laterˡ (≳now n)

    ∼steps : ∀ {i} n → Conat.[ i ] ⌜ n ⌝ ∼ steps (f n)
    ∼steps zero    = zero
    ∼steps (suc n) = suc λ { .force → ∼steps n }

    complicate :
      ∀ {m n i} → [ i ] ⌜ m ⌝ ≤ n → [ i ] steps (f m) ≤ n + zero
    complicate {m} {n} p =
      steps (f m) ∼⟨ Conat.symmetric-∼ (∼steps m) ⟩≤
      ⌜ m ⌝       ≤⟨ p ⟩
      n           ∼⟨ Conat.symmetric-∼ (Conat.+-right-identity _) ⟩≤
      n + zero    ∎≤

    simplify :
      ∀ {m n i} → [ i ] steps (f m) ≤ n + zero → [ i ] ⌜ m ⌝ ≤ n
    simplify {m} {n} p =
      ⌜ m ⌝        ∼⟨ ∼steps m ⟩≤
      steps (f m)  ≤⟨ p ⟩
      n + zero     ∼⟨ Conat.+-right-identity _ ⟩≤
      n            ∎≤

-- The left-to-right direction of ≈⇔≈×steps≤steps² can be made
-- size-preserving.

≈→≈×steps≤steps² :
  ∀ {i mˡ mʳ nˡ nʳ x y} →
  [ ∞ ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y →
  B.[ i ] x ≈ y ×
  [ i ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y ×
  [ i ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x
≈→≈×steps≤steps² x≈y = ≈→≈ x≈y , steps-+-*ʳ x≈y , steps-+-*ˡ x≈y

-- The right-to-left direction of ≈⇔≈×steps≤steps² can be made
-- size-preserving iff A is uninhabited.

≈×steps≤steps²→≈⇔uninhabited :
  (∀ {i mˡ mʳ nˡ nʳ x y} →
   B.[ i ] x ≈ y ×
   [ i ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y ×
   [ i ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x →
   [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y)
    ⇔
  ¬ A
≈×steps≤steps²→≈⇔uninhabited = record
  { to =
    (∀ {i mˡ mʳ nˡ nʳ x y} →
     B.[ i ] x ≈ y ×
     [ i ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y ×
     [ i ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x →
     [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y)               ↝⟨ (λ { hyp (p , q) → hyp (B.≳→ p , q , lemma (B.steps-mono p)) }) ⟩

    (∀ {i m n x y} →
     B.[ i ] x ≳ y ×
     [ i ] steps x ≤ n + (⌜ 1 ⌝ + m) * steps y →
     [ i ∣ m ∣ n ] x ≳ y)                           ↝⟨ _⇔_.to ≳×steps≤steps→≳⇔uninhabited ⟩□

    ¬ A                                             □
  ; from =
    ¬ A                                                        ↝⟨ (λ ¬A {_ _ _ _ _} → ∼→≈ (B.uninhabited→trivial ¬A _ _)) ⟩

    (∀ {i mˡ mʳ nˡ nʳ x y} → [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y)  ↝⟨ (λ hyp {_ _ _ _ _ _ _} _ → hyp {_}) ⟩□

    (∀ {i mˡ mʳ nˡ nʳ x y} →
     B.[ i ] x ≈ y ×
     [ i ] steps x ≤ nˡ + (⌜ 1 ⌝ + mˡ) * steps y ×
     [ i ] steps y ≤ nʳ + (⌜ 1 ⌝ + mʳ) * steps x →
     [ i ∣ mˡ ∣ mʳ ∣ nˡ ∣ nʳ ] x ≈ y)                          □
  }
  where
  lemma :
    ∀ {m n i} →
    [ i ] m ≤ n →
    [ i ] m ≤ (⌜ 1 ⌝ + ⌜ 0 ⌝) * n
  lemma {m} {n} p =
    m                    ≤⟨ p ⟩
    n                    ∼⟨ Conat.symmetric-∼ (Conat.*-left-identity _) ⟩≤
    ⌜ 1 ⌝ * n            ∼⟨ Conat.symmetric-∼ (Conat.+-right-identity _) Conat.*-cong (_ ∎∼) ⟩≤
    (⌜ 1 ⌝ + ⌜ 0 ⌝) * n  ∎≤

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
module trichotomy where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)

open import Relations using (_<_; z<s; s<s)

-- 三分法
data Trichotomy (m n : ℕ) : Set where
  m<n : m < n → Trichotomy m n
  m≡n : m ≡ n → Trichotomy m n
  n<m : n < m → Trichotomy m n

trichotomy : ∀ (m n : ℕ) → Trichotomy m n
trichotomy zero    zero                        = m≡n refl
trichotomy (suc m) zero                        = n<m z<s
trichotomy zero    (suc n)                     = m<n z<s
trichotomy (suc m) (suc n) with trichotomy m n
...                           | m<n m′<n′      = m<n (s<s m′<n′)
...                           | m≡n refl       = m≡n refl
...                           | n<m n′<m′      = n<m (s<s n′<m′)

ext: agda

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Terminal {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Relation.Binary using (IsEquivalence; Setoid)
open import Categories.Support.PropositionalEquality

open Category C

record Terminal : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊤ : Obj
    ! : ∀ {A} → (A ⇒ ⊤)
    .!-unique : ∀ {A} → (f : A ⇒ ⊤) → ! ≡ f

  .!-unique₂ : ∀ {A} → (f g : A ⇒ ⊤) → f ≡ g
  !-unique₂ f g =
    begin
      f
    ↑⟨ !-unique f ⟩
      !
    ↓⟨ !-unique g ⟩
      g
    ∎
    where open HomReasoning

  .⊤-id : (f : ⊤ ⇒ ⊤) → f ≡ id
  ⊤-id f = !-unique₂ f id

  open Heterogeneous C

  !-unique∼ : ∀ {A A′} → (f : A′ ⇒ ⊤) → (A ≣ A′) → ! {A} ∼ f
  !-unique∼ f ≣-refl = Heterogeneous.≡⇒∼ (!-unique f)

import Categories.Morphisms
open Categories.Morphisms C
open import Categories.Square
open GlueSquares C
open Terminal
open Heterogeneous C

!-is-propertylike : ∀ t₁ t₂ → ⊤ t₁ ≣ ⊤ t₂ → ∀ {A} → ! t₁ {A} ∼ ! t₂ {A}
!-is-propertylike t₁ t₂ eq = helper t₁ eq (! t₂)
  where
  helper : ∀ t {T} → (⊤ t ≣ T) → ∀ {A} (f : A ⇒ T) → ! t {A} ∼ f
  helper t ≣-refl f = ≡⇒∼ (!-unique t f)

up-to-iso : (t₁ t₂ : Terminal) → ⊤ t₁ ≅ ⊤ t₂
up-to-iso t₁ t₂ = record
  { f = ! t₂
  ; g = ! t₁
  ; iso = record { isoˡ = ⊤-id t₁ _; isoʳ = ⊤-id t₂ _ }
  }

up-to-iso-cong₂ : {t₁ t₁′ t₂ t₂′ : Terminal} → ⊤ t₁ ≣ ⊤ t₁′ → ⊤ t₂ ≣ ⊤ t₂′ → up-to-iso t₁ t₂ ∼ⁱ up-to-iso t₁′ t₂′
up-to-iso-cong₂ {t₁} {t₁′} {t₂} {t₂′} eq₁ eq₂ = heqⁱ (up-to-iso t₁ t₂) (up-to-iso t₁′ t₂′) (helper t₂ t₂′ eq₂ eq₁) (helper t₁ t₁′ eq₁ eq₂)
  where
  helper : ∀ t t′ → (⊤ t ≣ ⊤ t′) → ∀ {A A′} → A ≣ A′ → ! t {A} ∼ ! t′ {A′}
  helper t t′ eq-t ≣-refl = !-is-propertylike t t′ eq-t

transport-by-iso : (t : Terminal) → ∀ {X} → ⊤ t ≅ X → Terminal
transport-by-iso t {X} t≅X = record
  { ⊤ = X
  ; ! = f ∘ ! t
  ; !-unique = λ h → let open HomReasoning in
      begin
        f ∘ ! t
      ↓⟨ ∘-resp-≡ʳ (!-unique t (g ∘ h)) ⟩
        f ∘ (g ∘ h)
      ↓⟨ cancelLeft isoʳ ⟩
        h
      ∎
  }
  where open _≅_ t≅X

transport-by-iso-cong₂ : ∀ {t t′} → (⊤ t ≣ ⊤ t′) → ∀ {X} {i : ⊤ t ≅ X} {X′} {i′ : ⊤ t′ ≅ X′} → (i ∼ⁱ i′) → ⊤ (transport-by-iso t i) ≣ ⊤ (transport-by-iso t′ i′)
transport-by-iso-cong₂ eq-t eq-i = codomain-≣ⁱ eq-i

.up-to-iso-unique : ∀ t t′ → (i : ⊤ t ≅ ⊤ t′) → up-to-iso t t′ ≡ⁱ i
up-to-iso-unique t t′ i = record { f-≡ = !-unique t′ _; g-≡ = !-unique t _ }

.up-to-iso-invˡ : ∀ {t X} {i : ⊤ t ≅ X} → up-to-iso t (transport-by-iso t i) ≡ⁱ i
up-to-iso-invˡ {t} {i = i} = up-to-iso-unique t (transport-by-iso t i) i

up-to-iso-invʳ : ∀ {t t′} → ⊤ (transport-by-iso t (up-to-iso t t′)) ≣ ⊤ t′
up-to-iso-invʳ {t} {t′} = ≣-refl

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- Concrete syntax used by the mixfix operator parser
------------------------------------------------------------------------

module RecursiveDescent.Hybrid.Mixfix.Expr where

open import Data.Nat hiding (_≟_)
open import Data.Vec
open import Data.List using (List)
open import Data.Product
open import Data.Maybe
open import Data.String using (String)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import RecursiveDescent.Hybrid.Mixfix.Fixity

-- Name parts.

NamePart : Set
NamePart = String

-- Operators. arity is the internal arity of the operator, i.e. the
-- number of arguments taken between the first and last name parts.

data Operator (fix : Fixity) (arity : ℕ) : Set where
  operator : (nameParts : Vec NamePart (1 + arity)) ->
             Operator fix arity

-- Predicate filtering out operators of the given fixity and
-- associativity.

hasFixity : forall fix -> ∃₂ Operator -> Maybe (∃ (Operator fix))
hasFixity fix (fix' , op) with fix ≟ fix'
hasFixity fix (.fix , op) | yes refl = just op
hasFixity fix (fix' , op) | _        = nothing

-- Precedence graphs are represented by their unfoldings as forests
-- (one tree for every node in the graph). This does not take into
-- account the sharing of the precedence graphs, but this program is
-- not aimed at efficiency.

mutual

  PrecedenceGraph : Set
  PrecedenceGraph = List PrecedenceTree

  data PrecedenceTree : Set where
    precedence : (ops : (fix : Fixity) -> List (∃ (Operator fix)))
                 (successors : PrecedenceGraph) ->
                 PrecedenceTree

-- Concrete syntax. TODO: Ensure that expressions are precedence
-- correct by parameterising the expression type on a precedence graph
-- and indexing on precedences.

mutual

  infixl 4 _⟨_⟩_ _∙_
  infix  4 _⟨_⟫ ⟪_⟩_

  data Expr : Set where
    _⟨_⟩_ : forall {assoc}
            (l : Expr) (op : Internal (infx assoc)) (r : Expr) -> Expr
    _⟨_⟫  : (l : Expr) (op : Internal postfx)                  -> Expr
    ⟪_⟩_  :            (op : Internal prefx)        (r : Expr) -> Expr
    ⟪_⟫   :            (op : Internal closed)                  -> Expr

  -- Application of an operator to all its internal arguments.

  data Internal (fix : Fixity) : Set where
    _∙_ : forall {arity}
          (op : Operator fix arity) (args : Vec Expr arity) ->
          Internal fix

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --type-in-type #-}
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Product hiding ( curry ; uncurry )
open import Data.Nat
open import Data.String
open import Relation.Binary.PropositionalEquality using ( refl ; _≢_ ; _≡_ )
open import Function
module ClosedTheory where

noteq = _≢_

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

data Desc (I : Set) : Set₁ where
  End : (i : I) → Desc I
  Rec : (i : I) (D : Desc I) → Desc I
  Arg : (A : Set) (B : A → Desc I) → Desc I

ISet : Set → Set₁
ISet I = I → Set

El : {I : Set} (D : Desc I) → ISet I → ISet I
El (End j) X i = j ≡ i
El (Rec j D) X i = X j × El D X i
El (Arg A B) X i = Σ A (λ a → El (B a) X i)

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

UncurriedEl : {I : Set} (D : Desc I) (X : ISet I) → Set
UncurriedEl D X = ∀{i} → El D X i → X i

CurriedEl : {I : Set} (D : Desc I) (X : ISet I) → Set
CurriedEl (End i) X = X i
CurriedEl (Rec i D) X = (x : X i) → CurriedEl D X
CurriedEl (Arg A B) X = (a : A) → CurriedEl (B a) X

CurriedEl' : {I : Set} (D : Desc I) (X : ISet I) (i : I) → Set
CurriedEl' (End j) X i = j ≡ i → X i
CurriedEl' (Rec j D) X i = (x : X j) → CurriedEl' D X i
CurriedEl' (Arg A B) X i = (a : A) → CurriedEl' (B a) X i

curryEl : {I : Set} (D : Desc I) (X : ISet I)
  → UncurriedEl D X → CurriedEl D X
curryEl (End i) X cn = cn refl
curryEl (Rec i D) X cn = λ x → curryEl D X (λ xs → cn (x , xs))
curryEl (Arg A B) X cn = λ a → curryEl (B a) X (λ xs → cn (a , xs))

uncurryEl : {I : Set} (D : Desc I) (X : ISet I)
  → CurriedEl D X → UncurriedEl D X
uncurryEl (End i) X cn refl = cn
uncurryEl (Rec i D) X cn (x , xs) = uncurryEl D X (cn x) xs
uncurryEl (Arg A B) X cn (a , xs) = uncurryEl (B a) X (cn a) xs

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

data μ {I : Set} (D : Desc I) (i : I) : Set where
  init : El D (μ D) i → μ D i

Inj : {I : Set} (D : Desc I) → Set
Inj D = CurriedEl D (μ D)

inj : {I : Set} (D : Desc I) → Inj D
inj D = curryEl D (μ D) init

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

data VecT : Set where
  nilT consT : VecT

VecC : (A : Set) → VecT → Desc ℕ
VecC A nilT = End zero
VecC A consT = Arg ℕ (λ n → Arg A λ _ → Rec n (End (suc n)))

VecD : (A : Set) → Desc ℕ
VecD A = Arg VecT (VecC A)

Vec : (A : Set) → ℕ → Set
Vec A = μ (VecD A)

InjConsT : Set → ℕ → Set
InjConsT A m = El (VecC A consT) (Vec A) m → Vec A m

InjConsT' : Set → ℕ → Set
InjConsT' A m = Σ ℕ (λ n → A × Vec A n × suc n ≡ m) → Vec A m

test-InjConsT : (A : Set) (n : ℕ) → InjConsT A n ≡ InjConsT' A n
test-InjConsT A n = refl

nil : (A : Set) → Vec A zero
nil A = init (nilT , refl)

cons : (A : Set) (n : ℕ) (x : A) (xs : Vec A n) → Vec A (suc n)
cons A n x xs = init (consT , n , x , xs , refl)

nil2 : (A : Set) → Vec A zero
nil2 A = inj (VecD A) nilT

cons2 : (A : Set) (n : ℕ) (x : A) (xs : Vec A n) → Vec A (suc n)
cons2 A = inj (VecD A) consT

bit : Vec Bool (suc zero)
bit = cons Bool zero true (nil Bool)

bit2 : Vec Bool (suc zero)
bit2 = init (consT , zero , true , init (nilT , refl) , refl)

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

data TreeT : Set where
  leaf₁T leaf₂T branchT : TreeT

TreeC : (A B : Set) → TreeT → Desc (ℕ × ℕ)
TreeC A B leaf₁T = Arg A λ _ → End (suc zero , zero)
TreeC A B leaf₂T = Arg B λ _ → End (zero , suc zero)
TreeC A B branchT = Arg ℕ λ m → Arg ℕ λ n
                  → Arg ℕ λ x → Arg ℕ λ y
                  → Rec (m , n) $ Rec (x , y)
                  $ End (m + x , n + y)

TreeD : (A B : Set) → Desc (ℕ × ℕ)
TreeD A B = Arg TreeT (TreeC A B)

Tree : (A B : Set) (m n : ℕ) → Set
Tree A B m n = μ (TreeD A B) (m , n)

leaf₁ : (A B : Set) → A → Tree A B (suc zero) zero
leaf₁ A B a = init (leaf₁T , a , refl)

leaf₁2 : (A B : Set) → A → Tree A B (suc zero) zero
leaf₁2 A B = inj (TreeD A B) leaf₁T

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

max_stars_repo_name: larrytheliquid/generic-elim

max_issues_repo_name: larrytheliquid/generic-elim

max_forks_repo_name: larrytheliquid/generic-elim


text:
module VaryingClauseArity where

-- see also thread https://lists.chalmers.se/pipermail/agda-dev/2015-January/000041.html

open import Common.IO
open import Common.Unit
open import Common.Nat

Sum : Nat → Set
Sum 0       = Nat
Sum (suc n) = Nat → Sum n

sum : (acc : Nat) (n : Nat) → Sum n
sum acc 0         = acc
sum acc (suc n) 0 = sum acc n
sum acc (suc n) m = sum (m + acc) n

-- expected:
-- 10
-- 20
-- 33
main : IO Unit
main = printNat (sum 10 0) ,,
  putStr "\n" ,,
  printNat (sum 20 1 0) ,,
  putStr "\n" ,,
  printNat (sum 30 1 3)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors where all elements satisfy a given property
------------------------------------------------------------------------

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

module Data.Vec.Relation.Unary.All where

open import Data.Nat using (zero; suc)
open import Data.Fin using (Fin; zero; suc)
open import Data.Product as Prod using (_,_)
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Function using (_∘_)
open import Level using (_⊔_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary
open import Relation.Binary.PropositionalEquality as P using (subst)

------------------------------------------------------------------------
-- All P xs means that all elements in xs satisfy P.

infixr 5 _∷_

data All {a p} {A : Set a}
         (P : A → Set p) : ∀ {k} → Vec A k → Set (p ⊔ a) where
  []  : All P []
  _∷_ : ∀ {k x} {xs : Vec A k} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

------------------------------------------------------------------------
-- Operations on All

head : ∀ {a p} {A : Set a} {P : A → Set p} {k x} {xs : Vec A k} →
       All P (x ∷ xs) → P x
head (px ∷ pxs) = px

tail : ∀ {a p} {A : Set a} {P : A → Set p} {k x} {xs : Vec A k} →
       All P (x ∷ xs) → All P xs
tail (px ∷ pxs) = pxs

lookup : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} →
         (i : Fin k) → All P xs → P (Vec.lookup xs i)
lookup ()      []
lookup zero    (px ∷ pxs) = px
lookup (suc i) (px ∷ pxs) = lookup i pxs

tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {k xs} →
           (∀ i → P (Vec.lookup xs i)) → All P {k} xs
tabulate {xs = []}    pxs = []
tabulate {xs = _ ∷ _} pxs = pxs zero ∷ tabulate (pxs ∘ suc)

map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {k} →
      P ⊆ Q → All P {k} ⊆ All Q {k}
map g []         = []
map g (px ∷ pxs) = g px ∷ map g pxs

zipWith : ∀ {a b c p q r} {A : Set a} {B : Set b} {C : Set c} {_⊕_ : A → B → C}
          {P : A → Set p} {Q : B → Set q} {R : C → Set r} →
          (∀ {x y} → P x → Q y → R (x ⊕ y)) →
          ∀ {k xs ys} → All P {k} xs → All Q {k} ys →
          All R {k} (Vec.zipWith _⊕_ xs ys)
zipWith _⊕_ {xs = []}     {[]}     []         []         = []
zipWith _⊕_ {xs = x ∷ xs} {y ∷ ys} (px ∷ pxs) (qy ∷ qys) =
  px ⊕ qy ∷ zipWith _⊕_ pxs qys

zip : ∀ {a p q k} {A : Set a} {P : A → Set p} {Q : A → Set q} →
      All P ∩ All Q ⊆ All (P ∩ Q) {k}
zip ([] , [])             = []
zip (px ∷ pxs , qx ∷ qxs) = (px , qx) ∷ zip (pxs , qxs)

unzip : ∀ {a p q k} {A : Set a} {P : A → Set p} {Q : A → Set q} →
        All (P ∩ Q) {k} ⊆ All P ∩ All Q
unzip []           = [] , []
unzip (pqx ∷ pqxs) = Prod.zip _∷_ _∷_ pqx (unzip pqxs)

------------------------------------------------------------------------
-- Properties of predicates preserved by All

module _ {a p} {A : Set a} {P : A → Set p} where

  all : ∀ {k} → Decidable P → Decidable (All P {k})
  all P? []       = yes []
  all P? (x ∷ xs) with P? x
  ... | yes px = Dec.map′ (px ∷_) tail (all P? xs)
  ... | no ¬px = no (¬px ∘ head)

  universal : Universal P → ∀ {k} → Universal (All P {k})
  universal u []       = []
  universal u (x ∷ xs) = u x ∷ universal u xs

  irrelevant : Irrelevant P → ∀ {k} → Irrelevant (All P {k})
  irrelevant irr []           []           = P.refl
  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
    P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)

  satisfiable : Satisfiable P → ∀ {k} → Satisfiable (All P {k})
  satisfiable (x , p) {zero}  = [] , []
  satisfiable (x , p) {suc k} = Prod.map (x ∷_) (p ∷_) (satisfiable (x , p))


text:
{-# OPTIONS --without-K #-}
open import Type using (Type₀; Type₁; Type_)
open import Type.Identities
open import Function.NP using (Π; _∘_; const)
open import Function.Extensionality using (FunExt)
open import Data.Zero using (𝟘)
open import Data.One using (𝟙; 0₁)
open import Data.Two.Base using (𝟚; 0₂; 1₂)
open import Data.Product.NP using (Σ; _×_; _,_; fst; snd)
open import Data.Sum.NP using (_⊎_; inl; inr)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin using (Fin)
open import Relation.Nullary.NP using (Dec)
open import Relation.Binary.PropositionalEquality.NP using (_≡_; idp; ap; !_; _∙_; tr)
open import HoTT using (ua; UA; module Equivalences)
open        Equivalences using (_≃_; ≃-!; ≃-refl; _≃-∙_)

open import Explore.Core
open import Explore.Properties
open import Explore.Zero
open import Explore.One
open import Explore.Two
open import Explore.Product
open        Explore.Product.Operators
open import Explore.Sum
open import Explore.Explorable
open import Explore.Isomorphism
open import Explore.GuessingGameFlipping
import      Explore.Universe.Type
import      Explore.Universe.FromE

module Explore.Universe (X : Type₀) where

open Explore.Universe.Type {X}

module FromXᵉ = Explore.Universe.FromE X

open Adequacy _≡_
module FromKit
    {Xᵉ : ∀ {ℓ} → Explore ℓ X}
    (Xⁱ : ∀ {ℓ p} → ExploreInd p (Xᵉ {ℓ}))
    (let module Xᴱ = FromExploreInd Xⁱ)
    (Xˢ-ok : ∀{{_ : UA}}{{_ : FunExt}} → Adequate-sum Xᴱ.sum)
    (Xˡ : ∀ {ℓ} → Lookup {ℓ} Xᵉ)
    (Xᶠ : ∀ {ℓ} → Focus {ℓ} Xᵉ)
    (ΣᵉX-ok : ∀{{_ : UA}}{{_ : FunExt}}{ℓ} → Adequate-Σ {ℓ} (Σᵉ Xᵉ))
    (ΠᵉX-ok : ∀{{_ : UA}}{{_ : FunExt}}{ℓ} → Adequate-Π {ℓ} (Πᵉ Xᵉ))
    (⟦Xᵉ⟧≡ : ∀ {ℓ₀ ℓ₁} ℓᵣ → ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ _≡_ Xᵉ Xᵉ)
    (ΠX : (X → U) → U)
    (ΠX≃ : ∀{{_ : UA}}{{_ : FunExt}} v → El (ΠX v) ≃ Π X (El ∘ v))
    (u : U)
  where

  private
   module M where
    open FromXᵉ Xᵉ public
    open FromXⁱ Xⁱ public
    open FromXˡ Xˡ public
    open FromXᶠ Xᶠ public
    open FromΠX ΠX public

    module _ {{_ : FunExt}}{{_ : UA}} where
      open FromΣᵉX-ok ΣᵉX-ok public
      open FromΠᵉX-ok ΠᵉX-ok public
      open From⟦Xᵉ⟧≡  ⟦Xᵉ⟧≡  public
      open FromΠX≃   ΠX≃ public

  explore : ∀ {ℓ} → Explore ℓ (El u)
  explore = M.explore u

  explore-ind : ∀ {ℓ p} → ExploreInd {ℓ} p explore
  explore-ind = M.explore-ind u

  open FromExploreInd explore-ind public hiding (⟦explore⟧)
  -- TODO list what is exported here

  lookup : ∀ {ℓ} → Lookup {ℓ} explore
  lookup = M.lookup u

  open FromLookup {explore = explore} lookup public

  focus : ∀ {ℓ} → Focus {ℓ} explore
  focus = M.focus u

  Πᵁ : (v : El u → U) → U
  Πᵁ = M.Πᵁ u

  _→ᵁ_ : (v : U) → U
  _→ᵁ_ = M._→ᵁ_ u

  module _ {{_ : FunExt}}{{_ : UA}} where
    Σᵉ-ok : ∀ {ℓ} → Adequate-Σ {ℓ} (Σᵉ explore)
    Σᵉ-ok = M.Σᵉ-ok u

    Πᵉ-ok : ∀ {ℓ} → Adequate-Π {ℓ} (Πᵉ explore)
    Πᵉ-ok = M.Πᵉ-ok u

    ⟦explore⟧≡ : ∀ {ℓ₀ ℓ₁} ℓᵣ → ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ _≡_ explore explore
    ⟦explore⟧≡ ℓᵣ = M.⟦explore⟧≡ ℓᵣ u

    open From⟦Explore⟧ ⟦explore⟧≡ public
      using ( sum⇒Σᵉ
            ; product⇒Πᵉ
            ; ✓all-Πᵉ
            ; ✓any→Σᵉ
            ; module FromAdequate-Σᵉ
            ; module FromAdequate-Πᵉ
            )

    open FromAdequate-Σᵉ Σᵉ-ok public
      using ( sumStableUnder
            ; sumStableUnder′
            ; same-count→iso
            ; adequate-sum
            ; adequate-any
            )

    open FromAdequate-Πᵉ Πᵉ-ok public
      using ( adequate-product
            ; adequate-all
            ; check!
            )

    Dec-Σ : ∀ {p}{P : El u → Type p} → Π (El u) (Dec ∘ P) → Dec (Σ (El u) P)
    Dec-Σ = FromFocus.Dec-Σ focus

    Πᵁ-Π : ∀ v → El (Πᵁ v) ≡ Π (El u) (El ∘ v)
    Πᵁ-Π = M.Πᵁ-Π u

    →ᵁ-→ : ∀ v → El (_→ᵁ_ v) ≡ (El u → El v)
    →ᵁ-→ = M.→ᵁ-→ u

    Πᵁ→Π : ∀ v → El (Πᵁ v) → Π (El u) (El ∘ v)
    Πᵁ→Π = M.Πᵁ→Π u

    Π→Πᵁ : ∀ v → Π (El u) (El ∘ v) → El (Πᵁ v)
    Π→Πᵁ = M.Π→Πᵁ u

    →ᵁ→→ : ∀ v → El (_→ᵁ_ v) → (El u → El v)
    →ᵁ→→ = M.→ᵁ→→ u

    →→→ᵁ : ∀ v → (El u → El v) → El (_→ᵁ_ v)
    →→→ᵁ = M.→→→ᵁ u

    guessing-game-flipping = Explore.GuessingGameFlipping.thm (El u) sum sum-ind
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.Ledger2WaypointConverter as Ledger2WaypointConverter
open import LibraBFT.ImplShared.Consensus.Types
import      LibraBFT.ImplShared.Util.Crypto              as Crypto
open import Optics.All
open import Util.Hash
open import Util.Prelude

module LibraBFT.Impl.Types.Waypoint where

newAny : LedgerInfo → Waypoint
newAny ledgerInfo =
  let converter = Ledger2WaypointConverter.new ledgerInfo
   in Waypoint∙new (ledgerInfo ^∙ liVersion) (Crypto.hashL2WC converter)

newEpochBoundary : LedgerInfo → Either ErrLog Waypoint
newEpochBoundary ledgerInfo =
  if ledgerInfo ^∙ liEndsEpoch
  then pure (newAny ledgerInfo)
  else Left fakeErr -- ["newEpochBoundary", "no validator set"]

verify : Waypoint → LedgerInfo → Either ErrLog Unit
verify self ledgerInfo = do
  lcheck (self ^∙ wVersion == ledgerInfo ^∙ liVersion)
         ("Waypoint" ∷ "version mismatch" ∷ []) --show (self^.wVersion), show (ledgerInfo^.liVersion)]
  let converter = Ledger2WaypointConverter.new ledgerInfo
  lcheck (self ^∙ wValue == Crypto.hashL2WC converter)
         ("Waypoint" ∷ "value mismatch" ∷ []) --show (self^.wValue), show (Crypto.hashL2WC converter)]
  pure unit

epochChangeVerificationRequired : Waypoint → Epoch → Bool
epochChangeVerificationRequired _self _epoch = true

isLedgerInfoStale : Waypoint → LedgerInfo → Bool
isLedgerInfoStale self ledgerInfo = ⌊ (ledgerInfo ^∙ liVersion) <?-Version (self ^∙ wVersion) ⌋

verifierVerify : Waypoint → LedgerInfoWithSignatures → Either ErrLog Unit
verifierVerify self liws = verify self (liws ^∙ liwsLedgerInfo)


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.DinaturalTransformation where

open import Level
open import Data.Product

open import Categories.Category
import Categories.NaturalTransformation
private module NT = Categories.NaturalTransformation
open import Categories.Functor using (Functor) renaming (_∘_ to _∘F_)
open import Categories.Bifunctor using (Bifunctor; module Functor)
open import Categories.Product
open import Categories.Square

record DinaturalTransformation {o ℓ e o′ ℓ′ e′}
                               {C : Category o ℓ e}
                               {D : Category o′ ℓ′ e′}
                               (F G : Bifunctor (Category.op C) C D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module C = Category C
    module D = Category D
  open Functor F renaming (op to Fop)
  open Functor G renaming (F₀ to G₀; F₁ to G₁; op to Gop)
  open D hiding (op)
  field
    α : (c : C.Obj) → D [ F₀ (c , c) , G₀ (c , c) ]

    .commute : ∀ {c c′} (f : C [ c , c′ ]) → G₁ (f , C.id) ∘ α c′ ∘ F₁ ( C.id , f ) ≡ G₁ ( C.id , f ) ∘ α c ∘ F₁ ( f , C.id )

  op : DinaturalTransformation {C = C.op} {D = D.op} Gop Fop
  op = record { α = α; commute = λ f → D.Equiv.trans assoc (D.Equiv.trans (D.Equiv.sym (commute f)) (D.Equiv.sym assoc)) }

_<∘_ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G H : Bifunctor (Category.op C) C D}
      → NT.NaturalTransformation G H → DinaturalTransformation {C = C} F G → DinaturalTransformation {C = C} F H
_<∘_ {C = C} {D} {F} {G} {H} eta alpha = record { α = λ c → η (c , c) ∘ α c; commute = λ {c} {c′} f →
     begin
       H.F₁ (f , C.id) ∘ ((η (c′ , c′) ∘ α c′) ∘ F.F₁ (C.id , f))
     ↓⟨ ∘-resp-≡ʳ assoc ⟩
       H.F₁ (f , C.id) ∘ (η (c′ , c′) ∘ (α c′ ∘ F.F₁ (C.id , f)))
     ↑⟨ assoc ⟩
       (H.F₁ (f , C.id) ∘ η (c′ , c′)) ∘ (α c′ ∘ F.F₁ (C.id , f))
     ↑⟨ ∘-resp-≡ˡ (eta.commute (f , C.id)) ⟩
       (η (c , c′) ∘ G.F₁ (f , C.id)) ∘ (α c′ ∘ F.F₁ (C.id , f))
     ↓⟨ pullʳ (commute f) ⟩
       η (c , c′) ∘ G.F₁ (C.id , f) ∘ (α c ∘ F.F₁ (f , C.id))
     ↓⟨ pullˡ (eta.commute (C.id , f)) ⟩
       (H.F₁ (C.id , f) ∘ η (c , c)) ∘ (α c ∘ F.F₁ (f , C.id))
     ↓⟨ assoc ⟩
       H.F₁ (C.id , f) ∘ (η (c , c) ∘ (α c ∘ F.F₁ (f , C.id)))
     ↑⟨ ∘-resp-≡ʳ assoc ⟩
       H.F₁ (C.id , f) ∘ ((η (c , c) ∘ α c) ∘ F.F₁ (f , C.id))
     ∎
{-  This uses 'associative-unital reasoning, which is now broken.  Above uses
    direct reasoning, which is heavier, but works.  JC.
     begin
       H.F₁ (f , C.id) ∙ ((η (c′ , c′) ∙ α c′) ∙ F.F₁ (C.id , f))
     ↑⟨ refl ⟩
       (H.F₁ (f , C.id) ∙ η (c′ , c′)) ∙ (α c′ ∙ F.F₁ (C.id , f))
     ↑≡⟨ ∘-resp-≡ˡ (eta.commute (f , C.id)) ⟩
       (η (c , c′) ∙ G.F₁ (f , C.id)) ∙ (α c′ ∙ F.F₁ (C.id , f))
     ↓≡⟨ pullʳ (commute f) ⟩
       η (c , c′) ∙ G.F₁ (C.id , f) ∙ α c ∙ F.F₁ (f , C.id)
     ↓≡⟨ pullˡ (eta.commute (C.id , f)) ⟩
       (H.F₁ (C.id , f) ∙ η (c , c)) ∙ α c ∙ F.F₁ (f , C.id)
     ↓⟨ refl ⟩
       H.F₁ (C.id , f) ∙ (η (c , c) ∙ α c) ∙ F.F₁ (f , C.id)
     ∎ -} }
  where
    module C = Category C
    module D = Category D
    open D
    open D.Equiv
    module F = Functor F
    module G = Functor G
    module H = Functor H
    module eta = NT.NaturalTransformation eta
    open eta using (η)
    open DinaturalTransformation alpha
    -- open AUReasoning D
    open HomReasoning
    open GlueSquares D

_∘>_ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G H : Bifunctor (Category.op C) C D}
       → DinaturalTransformation {C = C} G H → NT.NaturalTransformation F G → DinaturalTransformation {C = C} F H
alpha ∘> eta = DinaturalTransformation.op (eta.op <∘ alpha.op)
  where
    module eta = NT.NaturalTransformation eta
    module alpha = DinaturalTransformation alpha

_∘ʳ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Bifunctor (Category.op C) C D}
     → (η : DinaturalTransformation {C = C} F G) → (K : Functor E C) → DinaturalTransformation {C = E} (F ∘F ((Functor.op K) ⁂ K)) (G ∘F ((Functor.op K) ⁂ K))
_∘ʳ_ {C = C} {D = D} {E} {F} {G} η K = record
  { α = λ c → DinaturalTransformation.α η (K.F₀ c)
  ; commute = λ {c} {c′} f → begin
      G.F₁ (K.F₁ f , K.F₁ E.id) D.∘ η.α (K.F₀ c′) D.∘ F.F₁ (K.F₁ E.id , K.F₁ f)
        ↓⟨ G.F-resp-≡ (C.Equiv.refl , K.identity) ⟩∘⟨ D.Equiv.refl ⟩∘⟨ F.F-resp-≡ (K.identity , C.Equiv.refl) ⟩
      G.F₁ (K.F₁ f , C.id) D.∘ η.α (K.F₀ c′) D.∘ F.F₁ (C.id , K.F₁ f)
        ↓⟨ DinaturalTransformation.commute η (K.F₁ f) ⟩
      G.F₁ (C.id , K.F₁ f) D.∘ η.α (K.F₀ c) D.∘ F.F₁ (K.F₁ f , C.id)
        ↑⟨ G.F-resp-≡ (K.identity , C.Equiv.refl) ⟩∘⟨ D.Equiv.refl ⟩∘⟨ F.F-resp-≡ (C.Equiv.refl , K.identity) ⟩
      G.F₁ (K.F₁ E.id , K.F₁ f) D.∘ η.α (K.F₀ c) D.∘ F.F₁ (K.F₁ f , K.F₁ E.id)
        ∎
  }
  where
    module K = Functor K
    module C = Category C
    module D = Category D
    module E = Category E
    module F = Functor F
    module G = Functor G
    module η = DinaturalTransformation η
    open D.HomReasoning

max_stars_repo_name: copumpkin/categories


text:
------------------------------------------------------------------------------
-- Proving that two group theory formalisations are equivalents
------------------------------------------------------------------------------

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

-- We prove that group theory axioms based on the signature (G, ·, ε,)
-- (see for example [p. 39, 1]), i.e.

-- ∀ a b c. abc = a(bc)

-- ∀ a. εa = aε = a

-- ∀ a. ∃ a'. a'a = aa' = ε

-- are equivalents to the axioms based on the signature (G, ·, _⁻¹, ε,)
-- (see for example [2,3]), i.e.

-- ∀ a b c. abc = a(bc)

-- ∀ a. εa = aε  = a

-- ∀ a. a⁻¹a = aa⁻¹ = ε

-- [1] C. C. Chang and H. J. Keisler. Model Theory, volume 73 of Studies
--  in Logic and the Foundations of Mathematics. North-Holland, 3rd
--  edition, 3rd impression 1992.

-- [2] Agda standard library_0.8.1 (see Algebra/Structures.agda)

-- [3] Coq implementation
--     (http://coq.inria.fr/pylons/contribs/files/GroupTheory/v8.3/GroupTheory.g1.html)

module FOT.GroupTheory.FormalisationsSL where

open import Data.Product
open import Relation.Binary.PropositionalEquality

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

-- NB. We only write the proof for the left-inverse property.

infixl 10 _·_ -- The symbol is '\cdot'.

postulate
  G   : Set        -- The universe
  ε   : G          -- The identity element.
  _·_ : G → G → G  -- The binary operation.

-- Left-inverse property based on the signature (G, ·, ε,).
leftInverse₁ : Set
leftInverse₁ = ∀ a → Σ G (λ a' → a' · a ≡ ε)

-- Left-inverse property based on the signature (G, ·, _⁻¹, ε,).
infix  11 _⁻¹

postulate  _⁻¹ : G → G -- The inverse function.

leftInverse₂ : Set
leftInverse₂ = ∀ a → a ⁻¹ · a ≡ ε

-- From the left-inverse property based on the signature (G, ·, _⁻¹, ε,)
-- to the one based on the signature (G, ·, ε,).
leftInverse₂₋₁ : leftInverse₂ → leftInverse₁
leftInverse₂₋₁ h a = (a ⁻¹) , (h a)

-- From the left-inverse property based on the signature (G, ·, ε,) to
-- the one based on the signature (G, ·, _⁻¹, ε,).
--
-- In this case we prove the existence of the inverse function.
leftInverse₁₋₂ : leftInverse₁ → Σ (G → G) (λ f → ∀ a → f a · a ≡ ε)
leftInverse₁₋₂ h = f , prf
  where
  f : G → G  --  The inverse function.
  f a = proj₁ (h a)

  prf : ∀ a → f a · a ≡ ε
  prf a = proj₂ (h a)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Record constructors are not allowed in patterns.

module RecordConstructorPatternMatching where

record R : Set₁ where
  constructor con
  field
    {A}         : Set
    f           : A → A
    {B C} D {E} : Set
    g           : B → C → E

id : R → R
id (con f D g) = con f D g


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

mutual

  data D : Set → Set₁ where
    c : (@0 A : Set) → _ → D _

  _ : (@0 A : Set) → A → D A
  _ = c


text:
{- Name: Bowornmet (Ben) Hudson

-- new source language module. trying stuff out

-}

open import Preliminaries
open import Preorder-withmax

module Source2 where

  data Tp : Set where
    unit : Tp
    nat : Tp
    susp : Tp → Tp
    _->s_ : Tp → Tp → Tp
    _×s_ : Tp → Tp → Tp
    list : Tp → Tp
    bool : Tp

  Ctx = List Tp

  -- de Bruijn indices
  data _∈_ : Tp → Ctx → Set where
    i0 : ∀ {Γ τ} → τ ∈ τ :: Γ
    iS : ∀ {Γ τ τ1} → τ ∈ Γ → τ ∈ τ1 :: Γ

  data _|-_ : Ctx → Tp → Set where
    unit : ∀ {Γ} → Γ |- unit
    var : ∀ {Γ τ}
        → τ ∈ Γ
        → Γ |- τ
    z : ∀ {Γ} → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ τ} → Γ |- nat → Γ |- τ → (nat :: (susp τ :: Γ)) |- τ
        → Γ |- τ
    lam : ∀ {Γ τ ρ} → (ρ :: Γ) |- τ
        → Γ |- (ρ ->s τ)
    app : ∀ {Γ τ1 τ2}
        → Γ |- (τ2 ->s τ1) → Γ |- τ2
        → Γ |- τ1
    prod : ∀ {Γ τ1 τ2}
         → Γ |- τ1 → Γ |- τ2
         → Γ |- (τ1 ×s τ2)
    delay : ∀ {Γ τ}
          → Γ |- τ
          → Γ |- susp τ
    force : ∀ {Γ τ}
          → Γ |- susp τ
          → Γ |- τ
    split : ∀ {Γ τ τ1 τ2}
          → Γ |- (τ1 ×s τ2) → (τ1 :: (τ2 :: Γ)) |- τ
          → Γ |- τ
    nil : ∀ {Γ τ} → Γ |- list τ
    _::s_ : ∀ {Γ τ} → Γ |- τ → Γ |- list τ → Γ |- list τ
    listrec : ∀ {Γ τ τ'} → Γ |- list τ → Γ |- τ' → (τ :: (list τ :: (susp τ' :: Γ))) |- τ' → Γ |- τ'
    true : ∀ {Γ} → Γ |- bool
    false : ∀ {Γ} → Γ |- bool

  module RenSubst where

      -- renaming = variable for variable substitution
      --functional view:
      --avoids induction,
      --some associativity/unit properties for free
    module Ren where

      -- read: you can rename Γ' as Γ
      rctx : Ctx → Ctx → Set
      rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

      rename-var : ∀ {Γ Γ' τ} → rctx Γ Γ' → τ ∈ Γ' → τ ∈ Γ
      rename-var ρ a = ρ a

      idr : ∀ {Γ} → rctx Γ Γ
      idr x = x

      -- weakening with renaming
      p∙ : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) Γ'
      p∙ ρ = λ x → iS (ρ x)

      p : ∀ {Γ τ} → rctx (τ :: Γ) Γ
      p = p∙ idr

      _∙rr_ : ∀ {A B C} → rctx A B → rctx B C → rctx A C
      ρ1 ∙rr ρ2 = ρ1 o ρ2

      -- free stuff
      rename-var-ident : ∀ {Γ τ} → (x : τ ∈ Γ) → rename-var idr x == x
      rename-var-ident _ = Refl

      rename-var-∙ : ∀ {A B C τ} → (r1 : rctx A B) (r2 : rctx B C) (x : τ ∈ C)
                  → rename-var r1 (rename-var r2 x) == rename-var (r1 ∙rr r2) x
      rename-var-∙ _ _ _ = Refl

      ∙rr-assoc : ∀ {A B C D} → (r1 : rctx A B) (r2 : rctx B C) (r3 : rctx C D) → _==_ {_} {rctx A D} (r1 ∙rr (r2 ∙rr r3)) ((r1 ∙rr r2) ∙rr r3)
      ∙rr-assoc r1 r2 r3 = Refl

      r-extend : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
      r-extend ρ i0 = i0
      r-extend ρ (iS x) = iS (ρ x)

      ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
      ren unit ρ = unit
      ren (var x) ρ = var (ρ x)
      ren z ρ = z
      ren (suc e) ρ = suc (ren e ρ)
      ren (rec e e₁ e₂) ρ = rec (ren e ρ) (ren e₁ ρ) (ren e₂ (r-extend (r-extend ρ)))
      ren (lam e) ρ = lam (ren e (r-extend ρ))
      ren (app e e₁) ρ = app (ren e ρ) (ren e₁ ρ)
      ren (prod e1 e2) ρ = prod (ren e1 ρ) (ren e2 ρ)
      ren (delay e) ρ = delay (ren e ρ)
      ren (force e) ρ = force (ren e ρ)
      ren (split e e₁) ρ = split (ren e ρ) (ren e₁ (r-extend (r-extend ρ)))
      -- list stuff
      ren nil ρ = nil
      ren (x ::s xs) ρ = ren x ρ ::s ren xs ρ
      ren true ρ = true
      ren false ρ = false
      ren (listrec e e₁ e₂) ρ = listrec (ren e ρ) (ren e₁ ρ) (ren e₂ (r-extend (r-extend (r-extend ρ))))

      extend-ren-comp-lemma : ∀ {Γ Γ' Γ'' τ τ'} → (x : τ ∈ τ' :: Γ'') (ρ1 : rctx Γ Γ') (ρ2 : rctx Γ' Γ'')
                            → Id {_} {_} ((r-extend ρ1 ∙rr r-extend ρ2) x) (r-extend (ρ1 ∙rr ρ2) x)
      extend-ren-comp-lemma i0 ρ1 ρ2 = Refl
      extend-ren-comp-lemma (iS x) ρ1 ρ2 = Refl

      extend-ren-comp : ∀ {Γ Γ' Γ'' τ} → (ρ1 : rctx Γ Γ') → (ρ2 : rctx Γ' Γ'')
                      → Id {_} {rctx (τ :: Γ) (τ :: Γ'')} (r-extend ρ1 ∙rr r-extend ρ2) (r-extend (ρ1 ∙rr ρ2))
      extend-ren-comp ρ1 ρ2 = λ=i (λ τ → λ= (λ x → extend-ren-comp-lemma x ρ1 ρ2))

      ren-comp : ∀ {Γ Γ' Γ'' τ} → (ρ1 : rctx Γ Γ') → (ρ2 : rctx Γ' Γ'') → (e : Γ'' |- τ)
               → (ren (ren e ρ2) ρ1) == (ren e (ρ1 ∙rr ρ2))
      ren-comp ρ1 ρ2 unit = Refl
      ren-comp ρ1 ρ2 (var x) = ap var (rename-var-∙ ρ1 ρ2 x)
      ren-comp ρ1 ρ2 z = Refl
      ren-comp ρ1 ρ2 (suc e) = ap suc (ren-comp ρ1 ρ2 e)
      ren-comp ρ1 ρ2 (rec e e₁ e₂) = ap3 rec (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
                                         (ap (ren e₂) (ap r-extend (extend-ren-comp ρ1 ρ2) ∘
                                           extend-ren-comp (r-extend ρ1) (r-extend ρ2)) ∘
                                           ren-comp (r-extend (r-extend ρ1)) (r-extend (r-extend ρ2)) e₂)
      ren-comp ρ1 ρ2 (lam e) = ap lam ((ap (ren e) (extend-ren-comp ρ1 ρ2)) ∘ ren-comp (r-extend ρ1) (r-extend ρ2) e)
      ren-comp ρ1 ρ2 (app e e₁) = ap2 app (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
      ren-comp ρ1 ρ2 (prod e e₁) = ap2 prod (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
      ren-comp ρ1 ρ2 (delay e) = ap delay (ren-comp ρ1 ρ2 e)
      ren-comp ρ1 ρ2 (force e) = ap force (ren-comp ρ1 ρ2 e)
      ren-comp ρ1 ρ2 (split e e₁) = ap2 split (ren-comp ρ1 ρ2 e)
                                        (ap (ren e₁) (ap r-extend (extend-ren-comp ρ1 ρ2) ∘
                                        extend-ren-comp (r-extend ρ1) (r-extend ρ2)) ∘
                                        ren-comp (r-extend (r-extend ρ1)) (r-extend (r-extend ρ2)) e₁)
      ren-comp ρ1 ρ2 nil = Refl
      ren-comp ρ1 ρ2 (e ::s e₁) = ap2 _::s_ (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
      ren-comp ρ1 ρ2 (listrec e e₁ e₂) = ap3 listrec (ren-comp ρ1 ρ2 e) (ren-comp ρ1 ρ2 e₁)
                                           (ap (ren e₂) (ap r-extend (ap r-extend (extend-ren-comp ρ1 ρ2)) ∘
                                           (ap r-extend (extend-ren-comp (r-extend ρ1) (r-extend ρ2)) ∘
                                           extend-ren-comp (r-extend (r-extend ρ1)) (r-extend (r-extend ρ2)))) ∘
                                           ren-comp (r-extend (r-extend (r-extend ρ1)))
                                                    (r-extend (r-extend (r-extend ρ2))) e₂)
      ren-comp ρ1 ρ2 true = Refl
      ren-comp ρ1 ρ2 false = Refl

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

    open Ren

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

    --lem2 (addvar)
    s-extend : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
    s-extend Θ i0 = var i0
    s-extend Θ (iS x) = wkn (Θ x)

    ids : ∀ {Γ} → sctx Γ Γ
    ids x = var x

      -- weakening with substitution
    q∙ : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) Γ'
    q∙ Θ = λ x → wkn (Θ x)

    lem3' : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ |- τ → sctx Γ (τ :: Γ')
    lem3' Θ e i0 = e
    lem3' Θ e (iS i) = Θ i

      --lem3
    q : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
    q e = lem3' ids e

    -- subst-var
    svar : ∀ {Γ1 Γ2 τ} → sctx Γ1 Γ2 → τ ∈ Γ2 → Γ1 |- τ
    svar Θ i = q (Θ i) i0

    lem4' : ∀ {Γ Γ' τ1 τ2} → sctx Γ Γ' → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ'))
    lem4' Θ a b = lem3' (lem3' Θ b) a

    lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
    lem4 e1 e2 = lem4' ids e1 e2

    subst : ∀ {Γ Γ' τ} → Γ' |- τ → sctx Γ Γ' → Γ |- τ
    subst unit Θ = unit
    subst (var x) Θ = Θ x
    subst z Θ = z
    subst (suc e) Θ = suc (subst e Θ)
    subst (rec e e₁ e₂) Θ = rec (subst e Θ) (subst e₁ Θ) (subst e₂ (s-extend (s-extend Θ)))
    subst (lam e) Θ = lam (subst e (s-extend Θ))
    subst (app e e₁) Θ = app (subst e Θ) (subst e₁ Θ)
    subst (prod e1 e2) Θ = prod (subst e1 Θ) (subst e2 Θ)
    subst (delay e) Θ = delay (subst e Θ)
    subst (force e) Θ = force (subst e Θ)
    subst (split e e₁) Θ = split (subst e Θ) (subst e₁ (s-extend (s-extend Θ)))
      -- list stuff
    subst nil Θ = nil
    subst (x ::s xs) Θ = subst x Θ ::s subst xs Θ
    subst true Θ = true
    subst false Θ = false
    subst (listrec e e₁ e₂) Θ = listrec (subst e Θ) (subst e₁ Θ) (subst e₂ (s-extend (s-extend (s-extend Θ))))

    subst1 : ∀ {Γ τ τ1} → Γ |- τ1 → (τ1 :: Γ) |- τ → Γ |- τ
    subst1 e e' = subst e' (q e)

    _rs_ : ∀ {A B C} → rctx A B → sctx B C → sctx A C
    _rs_ ρ Θ x = ren (subst (var x) Θ) ρ

    _ss_ : ∀ {A B C} → sctx A B → sctx B C → sctx A C
    _ss_ Θ1 Θ2 x = subst (subst (var x) Θ2) Θ1

    _sr_ : ∀ {A B C} → sctx A B → rctx B C → sctx A C
    _sr_ Θ ρ x = subst (ren (var x) ρ) Θ

    --free stuff
    svar-rs : ∀ {A B C τ} (ρ : rctx A B) (Θ : sctx B C) (x : τ ∈ C)
            → svar (ρ rs Θ) x == ren (svar Θ x) ρ
    svar-rs = λ ρ Θ x → Refl

    svar-ss : ∀ {A B C τ} (Θ1 : sctx A B) (Θ2 : sctx B C) (x : τ ∈ C)
            → svar (Θ1 ss Θ2) x == subst (svar Θ2 x) Θ1
    svar-ss = λ Θ1 Θ2 x → Refl

    svar-sr : ∀ {A B C τ} (Θ : sctx A B) (ρ : rctx B C) (x : τ ∈ C)
            → svar Θ (rename-var ρ x) == svar (Θ sr ρ) x
    svar-sr = λ Θ ρ x → Refl

    svar-id : ∀ {Γ τ} → (x : τ ∈ Γ) → var x == svar ids x
    svar-id = λ x → Refl

    rsr-assoc : ∀ {A B C D} → (ρ1 : rctx A B) (Θ : sctx B C) (ρ2 : rctx C D)
              → Id {_} {sctx A D} ((ρ1 rs Θ) sr ρ2) (ρ1 rs (Θ sr ρ2))
    rsr-assoc = λ ρ1 Θ ρ2 → Refl

    extend-id-once-lemma : ∀ {Γ τ τ'} → (x : τ ∈ τ' :: Γ) → _==_ {_} {τ' :: Γ |- τ}
                         (ids {τ' :: Γ} {τ} x) (s-extend {Γ} {Γ} {τ'} (ids {Γ}) {τ} x)
    extend-id-once-lemma i0 = Refl
    extend-id-once-lemma (iS x) = Refl

    extend-id-once : ∀ {Γ τ} → Id {_} {sctx (τ :: Γ) (τ :: Γ)} (ids {τ :: Γ}) (s-extend ids)
    extend-id-once = λ=i (λ τ → λ= (λ x → extend-id-once-lemma x))

    extend-id-twice : ∀ {Γ τ1 τ2} → Id {_} {sctx (τ1 :: τ2 :: Γ) (τ1 :: τ2 :: Γ)} (ids {τ1 :: τ2 :: Γ}) (s-extend (s-extend ids))
    extend-id-twice = ap s-extend extend-id-once ∘ extend-id-once

    subst-id : ∀ {Γ τ} (e : Γ |- τ) → e == subst e ids
    subst-id unit = Refl
    subst-id (var x) = svar-id x
    subst-id z = Refl
    subst-id (suc e) = ap suc (subst-id e)
    subst-id (rec e e₁ e₂) = ap3 rec (subst-id e) (subst-id e₁) (ap (subst e₂) extend-id-twice ∘ subst-id e₂)
    subst-id (lam e) = ap lam (ap (subst e) extend-id-once ∘ subst-id e)
    subst-id (app e e₁) = ap2 app (subst-id e) (subst-id e₁)
    subst-id (prod e e₁) = ap2 prod (subst-id e) (subst-id e₁)
    subst-id (delay e) = ap delay (subst-id e)
    subst-id (force e) = ap force (subst-id e)
    subst-id (split e e₁) = ap2 split (subst-id e) (ap (subst e₁) extend-id-twice ∘ subst-id e₁)
    subst-id nil = Refl
    subst-id (e ::s e₁) = ap2 _::s_ (subst-id e) (subst-id e₁)
    subst-id true = Refl
    subst-id false = Refl
    subst-id (listrec e e₁ e₂) = ap3 listrec (subst-id e) (subst-id e₁) (ap (subst e₂) (ap s-extend (ap s-extend extend-id-once) ∘ extend-id-twice) ∘ subst-id e₂)

    extend-rs-once-lemma : ∀ {A B C τ τ'} → (x : τ ∈ τ' :: B) (ρ : rctx C A) (Θ : sctx A B) → _==_ {_} {τ' :: C |- τ}
                         (_rs_ {τ' :: C} {τ' :: A} {τ' :: B} (r-extend {C} {A} {τ'} ρ)
                           (s-extend {A} {B} {τ'} Θ) {τ} x)
                           (s-extend {C} {B} {τ'} (_rs_ {C} {A} {B} ρ Θ) {τ} x)
    extend-rs-once-lemma i0 ρ Θ = Refl
    extend-rs-once-lemma (iS x) ρ Θ = ! (ren-comp iS ρ (Θ x)) ∘ ren-comp (r-extend ρ) iS (Θ x)

    extend-rs-once : ∀ {A B C τ} → (ρ : rctx C A) (Θ : sctx A B)
                   → Id {_} {sctx (τ :: C) (τ :: B)} (r-extend ρ rs s-extend Θ) (s-extend (ρ rs Θ))
    extend-rs-once ρ Θ = λ=i (λ τ → λ= (λ x → extend-rs-once-lemma x ρ Θ))

    extend-rs-twice : ∀ {A B C τ τ'} → (ρ : rctx C A) (Θ : sctx A B)
                    → Id {_} {sctx (τ :: τ' :: C) (τ :: τ' :: B)} ((r-extend (r-extend ρ)) rs (s-extend (s-extend Θ))) ((s-extend (s-extend (ρ rs Θ))))
    extend-rs-twice ρ Θ = ap s-extend (extend-rs-once ρ Θ) ∘ extend-rs-once (r-extend ρ) (s-extend Θ)

    subst-rs : ∀ {A B C τ} → (ρ : rctx C A) (Θ : sctx A B) (e : B |- τ)
             → ren (subst e Θ) ρ == subst e (ρ rs Θ)
    subst-rs ρ Θ unit = Refl
    subst-rs ρ Θ (var x) = svar-rs ρ Θ x
    subst-rs ρ Θ z = Refl
    subst-rs ρ Θ (suc e) = ap suc (subst-rs ρ Θ e)
    subst-rs ρ Θ (rec e e₁ e₂) = ap3 rec (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
                                   (ap (subst e₂) (extend-rs-twice ρ Θ) ∘
                                   subst-rs (r-extend (r-extend ρ)) (s-extend (s-extend Θ)) e₂)
    subst-rs ρ Θ (lam e) = ap lam (ap (subst e) (extend-rs-once ρ Θ) ∘ subst-rs (r-extend ρ) (s-extend Θ) e)
    subst-rs ρ Θ (app e e₁) = ap2 app (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
    subst-rs ρ Θ (prod e e₁) = ap2 prod (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
    subst-rs ρ Θ (delay e) = ap delay (subst-rs ρ Θ e)
    subst-rs ρ Θ (force e) = ap force (subst-rs ρ Θ e)
    subst-rs ρ Θ (split e e₁) = ap2 split (subst-rs ρ Θ e)
                                          (ap (subst e₁) (extend-rs-twice ρ Θ) ∘
                                          subst-rs (r-extend (r-extend ρ)) (s-extend (s-extend Θ)) e₁)
    subst-rs ρ Θ nil = Refl
    subst-rs ρ Θ (e ::s e₁) = ap2 _::s_ (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
    subst-rs ρ Θ true = Refl
    subst-rs ρ Θ false = Refl
    subst-rs ρ Θ (listrec e e₁ e₂) = ap3 listrec (subst-rs ρ Θ e) (subst-rs ρ Θ e₁)
                                         (ap (subst e₂) (ap s-extend (ap s-extend (extend-rs-once ρ Θ)) ∘
                                         extend-rs-twice (r-extend ρ) (s-extend Θ)) ∘
                                         subst-rs (r-extend (r-extend (r-extend ρ))) (s-extend (s-extend (s-extend Θ))) e₂)

    rs-comp : ∀ {Γ Γ' Γ'' τ} → (ρ : rctx Γ Γ') → (Θ : sctx Γ' Γ'') → (e : Γ'' |- τ)
            → (ren (subst e Θ) ρ) == subst e (ρ rs Θ)
    rs-comp ρ Θ unit = Refl
    rs-comp ρ Θ (var x) = svar-rs ρ Θ x
    rs-comp ρ Θ z = Refl
    rs-comp ρ Θ (suc e) = ap suc (rs-comp ρ Θ e)
    rs-comp ρ Θ (rec e e₁ e₂) = ap3 rec (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
                                (ap (subst e₂) (extend-rs-twice ρ Θ) ∘ rs-comp (r-extend (r-extend ρ)) (s-extend (s-extend Θ)) e₂)
    rs-comp ρ Θ (lam e) = ap lam (ap (subst e) (extend-rs-once ρ Θ) ∘ rs-comp (r-extend ρ) (s-extend Θ) e)
    rs-comp ρ Θ (app e e₁) = ap2 app (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
    rs-comp ρ Θ (prod e e₁) = ap2 prod (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
    rs-comp ρ Θ (delay e) = ap delay (rs-comp ρ Θ e)
    rs-comp ρ Θ (force e) = ap force (rs-comp ρ Θ e)
    rs-comp ρ Θ (split e e₁) = ap2 split (rs-comp ρ Θ e) (ap (subst e₁) (extend-rs-twice ρ Θ) ∘ rs-comp (r-extend (r-extend ρ)) (s-extend (s-extend Θ)) e₁)
    rs-comp ρ Θ nil = Refl
    rs-comp ρ Θ (e ::s e₁) = ap2 _::s_ (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
    rs-comp ρ Θ (listrec e e₁ e₂) = ap3 listrec (rs-comp ρ Θ e) (rs-comp ρ Θ e₁)
                                      (ap (subst e₂) (ap s-extend (ap s-extend (extend-rs-once ρ Θ)) ∘
                                      extend-rs-twice (r-extend ρ) (s-extend Θ)) ∘
                                      rs-comp (r-extend (r-extend (r-extend ρ)))
                                      (s-extend (s-extend (s-extend Θ))) e₂)
    rs-comp ρ Θ true = Refl
    rs-comp ρ Θ false = Refl

    extend-sr-once-lemma : ∀ {A B C τ τ'} → (Θ : sctx A B) (ρ : rctx B C) (x : τ ∈ τ' :: C)
                         → _==_ {_} {τ' :: A |- τ} (s-extend (_sr_ Θ ρ) x) (_sr_ (s-extend Θ) (r-extend ρ) x)
    extend-sr-once-lemma Θ ρ i0 = Refl
    extend-sr-once-lemma Θ ρ (iS x) = Refl

    extend-sr-once : ∀ {A B C τ} → (Θ : sctx A B) (ρ : rctx B C)
                   → Id {_} {sctx (τ :: A) (τ :: C)} (s-extend Θ sr r-extend ρ) (s-extend (Θ sr ρ))
    extend-sr-once Θ ρ = λ=i (λ τ → λ= (λ x → ! (extend-sr-once-lemma Θ ρ x)))

    extend-sr-twice : ∀ {A B C τ τ'} → (Θ : sctx A B) (ρ : rctx B C)
                   → Id {_} {sctx (τ' :: τ :: A) (τ' :: τ :: C)}
                     (s-extend (s-extend Θ) sr r-extend (r-extend ρ)) (s-extend (s-extend (Θ sr ρ)))
    extend-sr-twice Θ ρ = ap s-extend (extend-sr-once Θ ρ) ∘ extend-sr-once (s-extend Θ) (r-extend ρ)

    sr-comp : ∀ {Γ Γ' Γ'' τ} → (Θ : sctx Γ Γ') → (ρ : rctx Γ' Γ'') → (e : Γ'' |- τ)
            → (subst (ren e ρ) Θ) == subst e (Θ sr ρ)
    sr-comp Θ ρ unit = Refl
    sr-comp Θ ρ (var x) = svar-sr Θ ρ x
    sr-comp Θ ρ z = Refl
    sr-comp Θ ρ (suc e) = ap suc (sr-comp Θ ρ e)
    sr-comp Θ ρ (rec e e₁ e₂) = ap3 rec (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
                                        (ap (subst e₂) (ap s-extend (extend-sr-once Θ ρ) ∘
                                        extend-sr-once (s-extend Θ) (r-extend ρ)) ∘
                                        sr-comp (s-extend (s-extend Θ)) (r-extend (r-extend ρ)) e₂)
    sr-comp Θ ρ (lam e) = ap lam (ap (subst e) (extend-sr-once Θ ρ) ∘ sr-comp (s-extend Θ) (r-extend ρ) e)
    sr-comp Θ ρ (app e e₁) = ap2 app (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
    sr-comp Θ ρ (prod e e₁) = ap2 prod (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
    sr-comp Θ ρ (delay e) = ap delay (sr-comp Θ ρ e)
    sr-comp Θ ρ (force e) = ap force (sr-comp Θ ρ e)
    sr-comp Θ ρ (split e e₁) = ap2 split (sr-comp Θ ρ e) (ap (subst e₁) (ap s-extend (extend-sr-once Θ ρ) ∘
                                                         extend-sr-once (s-extend Θ) (r-extend ρ)) ∘
                                                         sr-comp (s-extend (s-extend Θ)) (r-extend (r-extend ρ)) e₁)
    sr-comp Θ ρ nil = Refl
    sr-comp Θ ρ (e ::s e₁) = ap2 _::s_ (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
    sr-comp Θ ρ (listrec e e₁ e₂) = ap3 listrec (sr-comp Θ ρ e) (sr-comp Θ ρ e₁)
                                                (ap (subst e₂) (ap s-extend (ap s-extend (extend-sr-once Θ ρ)) ∘
                                                extend-sr-twice (s-extend Θ) (r-extend ρ)) ∘
                                                   sr-comp (s-extend (s-extend (s-extend Θ)))
                                                   (r-extend (r-extend (r-extend ρ))) e₂)

    sr-comp Θ ρ true = Refl
    sr-comp Θ ρ false = Refl

    extend-ss-once-lemma : ∀ {A B C τ τ'} → (Θ1 : sctx A B) (Θ2 : sctx B C) (x : τ ∈ τ' :: C)
                         → _==_ {_} {τ' :: A |- τ} (s-extend (_ss_ Θ1 Θ2) x) (_ss_ (s-extend Θ1) (s-extend Θ2) x)
    extend-ss-once-lemma Θ1 Θ2 i0 = Refl
    extend-ss-once-lemma Θ1 Θ2 (iS x) = ! (sr-comp (s-extend Θ1) iS (Θ2 x)) ∘ rs-comp iS Θ1 (Θ2 x)

    extend-ss-once : ∀ {A B C τ} → (Θ1 : sctx A B) (Θ2 : sctx B C)
                → _==_ {_} {sctx (τ :: A) (τ :: C)} (s-extend (Θ1 ss Θ2))
                ((s-extend Θ1) ss
                (s-extend Θ2))
    extend-ss-once Θ1 Θ2 = λ=i (λ τ → λ= (λ x → extend-ss-once-lemma Θ1 Θ2 x))

    subst-ss : ∀ {A B C τ} → (Θ1 : sctx A B) (Θ2 : sctx B C) (e : C |- τ)
             → subst e (Θ1 ss Θ2) == subst (subst e Θ2) Θ1
    subst-ss Θ1 Θ2 unit = Refl
    subst-ss Θ1 Θ2 (var x) = svar-ss Θ1 Θ2 x
    subst-ss Θ1 Θ2 z = Refl
    subst-ss Θ1 Θ2 (suc e) = ap suc (subst-ss Θ1 Θ2 e)
    subst-ss Θ1 Θ2 (rec e e₁ e₂) = ap3 rec (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
                                   (subst-ss (s-extend (s-extend Θ1)) (s-extend (s-extend Θ2)) e₂ ∘
                                   ap (subst e₂) (extend-ss-once (s-extend Θ1) (s-extend Θ2) ∘
                                   ap s-extend (extend-ss-once Θ1 Θ2)))
    subst-ss Θ1 Θ2 (lam e) = ap lam (subst-ss (s-extend Θ1) (s-extend Θ2) e ∘ ap (subst e) (extend-ss-once Θ1 Θ2))
    subst-ss Θ1 Θ2 (app e e₁) = ap2 app (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
    subst-ss Θ1 Θ2 (prod e e₁) = ap2 prod (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
    subst-ss Θ1 Θ2 (delay e) = ap delay (subst-ss Θ1 Θ2 e)
    subst-ss Θ1 Θ2 (force e) = ap force (subst-ss Θ1 Θ2 e)
    subst-ss Θ1 Θ2 (split e e₁) = ap2 split (subst-ss Θ1 Θ2 e)
                                            (subst-ss (s-extend (s-extend Θ1)) (s-extend (s-extend Θ2)) e₁ ∘
                                            ap (subst e₁) (extend-ss-once (s-extend Θ1) (s-extend Θ2) ∘
                                            ap s-extend (extend-ss-once Θ1 Θ2)))
    subst-ss Θ1 Θ2 nil = Refl
    subst-ss Θ1 Θ2 (e ::s e₁) = ap2 _::s_ (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
    subst-ss Θ1 Θ2 true = Refl
    subst-ss Θ1 Θ2 false = Refl
    subst-ss Θ1 Θ2 (listrec e e₁ e₂) = ap3 listrec (subst-ss Θ1 Θ2 e) (subst-ss Θ1 Θ2 e₁)
                                       (subst-ss (s-extend (s-extend (s-extend Θ1))) (s-extend (s-extend (s-extend Θ2))) e₂ ∘
                                       ap (subst e₂) (extend-ss-once (s-extend (s-extend Θ1)) (s-extend (s-extend Θ2)) ∘
                                       ap s-extend (extend-ss-once (s-extend Θ1) (s-extend Θ2) ∘
                                       ap s-extend (extend-ss-once Θ1 Θ2))))

    throw : ∀ {Γ Γ' τ} → sctx Γ (τ :: Γ') → sctx Γ Γ'
    throw Θ x = Θ (iS x)

    fuse1 : ∀ {Γ Γ' τ τ'} (v : Γ |- τ') (Θ : sctx Γ Γ') (x : τ ∈ Γ') → (q v ss q∙ Θ) x == Θ x
    fuse1 v Θ x = subst (ren (Θ x) iS) (q v) =⟨ sr-comp (q v) iS (Θ x) ⟩
               subst (Θ x) (q v sr iS) =⟨ Refl ⟩
               subst (Θ x) ids =⟨ ! (subst-id (Θ x)) ⟩
               (Θ x ∎)

    subst-compose-lemma-lemma : ∀ {Γ Γ' τ τ'} (v : Γ |- τ') (Θ : sctx Γ Γ') (x : τ ∈ τ' :: Γ')
                              → _==_ {_} {Γ |- τ} (_ss_ (q v) (s-extend Θ) x) (lem3' Θ v x)
    subst-compose-lemma-lemma v Θ i0 = Refl
    subst-compose-lemma-lemma v Θ (iS x) = subst (wkn (subst (var x) Θ)) (lem3' ids v) =⟨ subst-ss (q v) (q∙ Θ) (var x) ⟩
                                           subst (var x) (q v ss q∙ Θ) =⟨ fuse1 v Θ x ⟩
                                           subst (var x) Θ =⟨ Refl ⟩
                                           Θ x ∎

    fuse2 : ∀ {Γ Γ' τ τ1 τ2} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (Θ : sctx Γ Γ') (x : τ ∈ τ2 :: Γ')
        → (lem4 v1 v2 ss throw (s-extend (s-extend Θ))) x == (lem3' Θ v2) x
    fuse2 v1 v2 Θ x = subst (ren (s-extend Θ x) iS) (lem4 v1 v2) =⟨ sr-comp (lem4 v1 v2) iS (s-extend Θ x) ⟩
                      subst (s-extend Θ x) (lem4 v1 v2 sr iS) =⟨ Refl ⟩
                      subst (s-extend Θ x) (lem3' ids v2) =⟨ subst-compose-lemma-lemma v2 Θ x ⟩
                      (lem3' Θ v2 x ∎)

    subst-compose-lemma : ∀ {Γ Γ' τ} (v : Γ |- τ) (Θ : sctx Γ Γ')
                        → _==_ {_} {sctx Γ (τ :: Γ')} ((q v) ss (s-extend Θ)) (lem3' Θ v)
    subst-compose-lemma v Θ = λ=i (λ τ → λ= (λ x → subst-compose-lemma-lemma v Θ x))

    subst-compose : ∀ {Γ Γ' τ τ1} (Θ : sctx Γ Γ') (v : Γ |- τ) (e : (τ :: Γ' |- τ1) )
                  → subst (subst e (s-extend Θ)) (q v) == subst e (lem3' Θ v)
    subst-compose Θ v e = ap (subst e) (subst-compose-lemma v Θ) ∘ (! (subst-ss (q v) (s-extend Θ) e))

    subst-compose2-lemma-lemma : ∀ {Γ Γ' τ τ1 τ2 τ'} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (e1 : τ1 :: τ2 :: Γ' |- τ) (Θ : sctx Γ Γ') (x : τ' ∈ τ1 :: τ2 :: Γ')
                               → _==_ {_} {_} ((lem4 v1 v2 ss s-extend (s-extend Θ)) x) (lem4' Θ v1 v2 x)
    subst-compose2-lemma-lemma v1 v2 e1 Θ i0 = Refl
    subst-compose2-lemma-lemma v1 v2 e1 Θ (iS x) = subst (wkn (s-extend Θ x)) (lem4 v1 v2) =⟨ Refl ⟩
                                                   subst (var x) (lem4 v1 v2 ss throw (s-extend (s-extend Θ))) =⟨ fuse2 v1 v2 Θ x ⟩
                                                   subst (var x) (lem3' Θ v2) =⟨ Refl ⟩
                                                   (lem3' Θ v2 x ∎)

    subst-compose2-lemma : ∀ {Γ Γ' τ τ1 τ2} (v1 : Γ |- τ1) (v2 : Γ |- τ2) (e1 : τ1 :: τ2 :: Γ' |- τ) (Θ : sctx Γ Γ')
                         → _==_ {_} {sctx Γ (τ1 :: τ2 :: Γ')} (lem4 v1 v2 ss s-extend (s-extend Θ)) (lem4' Θ v1 v2)
    subst-compose2-lemma v1 v2 e1 Θ = λ=i (λ τ → λ= (λ x → subst-compose2-lemma-lemma v1 v2 e1 Θ x))

    subst-compose2 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (n : Γ |- nat) (e1 : Γ' |- τ) (e2 : (nat :: (susp τ :: Γ')) |- τ)
                  →  subst (subst e2 (s-extend (s-extend Θ))) (lem4 n (delay (rec n (subst e1 Θ) (subst e2 (s-extend (s-extend Θ)))))) ==
                     subst e2 (lem4' Θ n (delay (rec n (subst e1 Θ) (subst e2 (s-extend (s-extend Θ))))))
    subst-compose2 Θ n e1 e2 = ap (subst e2) (subst-compose2-lemma n (delay (rec n (subst e1 Θ) (subst e2 (s-extend (s-extend Θ))))) e2 Θ) ∘
                               ! (subst-ss (lem4 n (delay (rec n (subst e1 Θ) (subst e2 (s-extend (s-extend Θ)))))) (s-extend (s-extend Θ)) e2)

    subst-compose3 : ∀ {Γ Γ' τ τ1 τ2} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ |- τ1) (v2 : Γ |- τ2)
                   → subst (subst e1 (s-extend (s-extend Θ))) (lem4 v1 v2) == subst e1 (lem4' Θ v1 v2)
    subst-compose3 Θ e1 v1 v2 = ap (subst e1) (subst-compose2-lemma v1 v2 e1 Θ) ∘
                                ! (subst-ss (lem4 v1 v2) (s-extend (s-extend Θ)) e1)

    subst-compose4 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (v' : Γ |- nat) (r : Γ |- susp τ) (e2 : (nat :: (susp τ :: Γ')) |- τ)
                   → subst (subst e2 (s-extend (s-extend Θ))) (lem4 v' r) == subst e2 (lem4' Θ v' r)
    subst-compose4 Θ v' r e2 = ap (subst e2) (subst-compose2-lemma v' r e2 Θ) ∘
                             ! (subst-ss (lem4 v' r) (s-extend (s-extend Θ)) e2)

  open RenSubst

  --closed values of the source language
  data val : ∀ {τ} → [] |- τ → Set where
    z-isval : val z
    suc-isval : (e : [] |- nat) → (val e)
              → val (suc e)
    pair-isval : ∀ {τ1 τ2} (e1 : [] |- τ1) → (e2 : [] |- τ2)
               → val e1 → val e2
               → val (prod e1 e2)
    lam-isval : ∀ {ρ τ} (e : (ρ :: []) |- τ)
              → val (lam e)
    unit-isval : val unit
    delay-isval : ∀ {τ} (e : [] |- τ) → val (delay e)
    nil-isval : ∀ {τ} → val (nil {_} {τ})
    cons-isval : ∀ {τ} (x : [] |- τ) → (xs : [] |- list τ)
               → val x → val xs
               → val (x ::s xs)
    true-isval : val true
    false-isval : val false

  data Cost : Set where
    0c : Cost
    1c : Cost
    _+c_ : Cost → Cost → Cost

  data Equals0c : Cost → Set where
    Eq0-0c : Equals0c 0c
    Eq0-+c : ∀ {c c'} → Equals0c c → Equals0c c' → Equals0c (c +c c')

  mutual
    -- define evals (e : source exp) (v : value) (c : nat)
    -- analogous to "e evaluates to v in c steps"
    -- figure 2 from ICFP paper
    data evals : {τ : Tp} → [] |- τ → [] |- τ → Cost → Set where
      pair-evals : ∀ {n1 n2}
                 → {τ1 τ2 : Tp} {e1 v1 : [] |- τ1} {e2 v2 : [] |- τ2}
                 → evals e1 v1 n1
                 → evals e2 v2 n2
                 → evals (prod e1 e2) (prod v1 v2) (n1 +c n2)
      lam-evals : ∀ {ρ τ} {e : (ρ :: []) |- τ}
                → evals (lam e) (lam e) 0c
      app-evals : ∀ {n0 n1 n}
               → {τ1 τ2 : Tp} {e0 : [] |- (τ1 ->s τ2)} {e0' : (τ1 :: []) |- τ2} {e1 v1 : [] |- τ1} {v : [] |- τ2}
               → evals e0 (lam e0') n0
               → evals e1 v1 n1
               → evals (subst e0' (q v1)) v n
               → evals (app e0 e1) v ((n0 +c n1) +c n)
      z-evals : evals z z 0c
      s-evals : ∀ {n}
              → {e v : [] |- nat}
              → evals e v n
              → evals (suc e) (suc v) n
      unit-evals : evals unit unit 0c
      rec-evals : ∀ {n1 n2}
                  → {τ : Tp} {e v : [] |- nat} {e0 v' : [] |- τ} {e1 : (nat :: (susp τ :: [])) |- τ}
                  → evals e v n1
                  → evals-rec-branch e0 e1 v v' n2
                  → evals (rec e e0 e1) v' (n1 +c (1c +c n2))
      delay-evals : {τ : Tp} {e : [] |- τ}
                  → evals (delay e) (delay e) 0c
      force-evals : ∀ {n1 n2}
                  → {τ : Tp} {e' v : [] |- τ} {e : [] |- susp τ}
                  → evals e (delay e') n1
                  → evals e' v n2
                  → evals (force e) v (n1 +c n2)
      split-evals : ∀ {n1 n2}
                  → {τ τ1 τ2 : Tp} {e0 : [] |- (τ1 ×s τ2)} {v1 : [] |- τ1} {v2 : [] |- τ2} {e1 : (τ1 :: (τ2 :: [])) |- τ} {v : [] |- τ}
                  → evals e0 (prod v1 v2) n1
                  → evals (subst e1 (lem4 v1 v2)) v n2
                  → evals (split e0 e1) v (n1 +c n2)
      nil-evals : ∀ {τ : Tp} → evals (nil {_} {τ}) (nil {_} {τ}) 0c
      cons-evals : ∀ {n1 n2}
                 → {τ : Tp} {x v : [] |- τ} {xs vs : [] |- list τ}
                 → evals x v n1
                 → evals xs vs n2
                 → evals (x ::s xs) (v ::s vs) (n1 +c n2)
      true-evals : evals true true 0c
      false-evals : evals false false 0c

    -- means evals (rec v e0 e1) v' n
    -- but helpful to have a separate type for this
    data evals-rec-branch {τ : Tp} (e0 : [] |- τ) (e1 : (nat :: (susp τ :: [])) |- τ) : (e : [] |- nat) (v : [] |- τ) → Cost → Set where
         evals-rec-z : ∀ {v n} → evals e0 v n → evals-rec-branch e0 e1 z v n
         evals-rec-s : ∀ {v v' n} → evals (subst e1 (lem4 v (delay (rec v e0 e1)))) v' n
                               → evals-rec-branch e0 e1 (suc v) v' n

  evals-val : {τ : Tp} {e : [] |- τ} {v : [] |- τ} {n : Cost} → evals e v n → val v
  evals-val (pair-evals D D₁) = pair-isval _ _ (evals-val D) (evals-val D₁)
  evals-val lam-evals = lam-isval _
  evals-val (app-evals D D₁ D₂) = evals-val D₂
  evals-val z-evals = z-isval
  evals-val (s-evals D) = suc-isval _ (evals-val D)
  evals-val unit-evals = unit-isval
  evals-val (rec-evals x (evals-rec-z D)) = evals-val D
  evals-val (rec-evals x (evals-rec-s D)) = evals-val D
  evals-val delay-evals = delay-isval _
  evals-val (force-evals D D₁) = evals-val D₁
  evals-val (split-evals D D₁) = evals-val D₁
  evals-val nil-evals = nil-isval
  evals-val (cons-evals D D₁) = cons-isval _ _ (evals-val D) (evals-val D₁)
  evals-val true-evals = true-isval
  evals-val false-evals = false-isval

  -- lemma 2 from ICFP paper
  val-evals-inversion : {τ : Tp} {v v' : [] |- τ} {n : Cost} → val v → evals v v' n → (v == v') × Equals0c n
  val-evals-inversion z-isval z-evals = Refl , Eq0-0c
  val-evals-inversion (suc-isval e ve) (s-evals D) = (ap suc (fst IH)) , snd IH where
    IH = val-evals-inversion ve D
  val-evals-inversion (pair-isval e1 e2 ve1 ve2) (pair-evals D D₁) = ap2 prod (fst IH1) (fst IH2) , Eq0-+c (snd IH1) (snd IH2) where
    IH1 = val-evals-inversion ve1 D
    IH2 = val-evals-inversion ve2 D₁
  val-evals-inversion (lam-isval e) lam-evals = Refl , Eq0-0c
  val-evals-inversion unit-isval unit-evals = Refl , Eq0-0c
  val-evals-inversion (delay-isval e) delay-evals = Refl , Eq0-0c
  val-evals-inversion nil-isval nil-evals = Refl , Eq0-0c
  val-evals-inversion (cons-isval x xs vx vxs) (cons-evals D D₁) = ap2 _::s_ (fst IH1) (fst IH2) , Eq0-+c (snd IH1) (snd IH2) where
    IH1 = val-evals-inversion vx D
    IH2 = val-evals-inversion vxs D₁
  val-evals-inversion true-isval true-evals = Refl , Eq0-0c
  val-evals-inversion false-isval false-evals = Refl , Eq0-0c

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
------------------------------------------------------------------------------
-- All parameters are required in an ATP definition
------------------------------------------------------------------------------

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

module Issue11 where

postulate
  D          : Set
  false true : D

data Bool : D → Set where
  btrue  : Bool true
  bfalse : Bool false

OkBit : D → Set
OkBit b = Bool b
{-# ATP definition OkBit #-}

postulate foo : ∀ b → OkBit b → OkBit b
{-# ATP prove foo #-}

WrongBit : D → Set
WrongBit = Bool
{-# ATP definition WrongBit #-}

postulate bar : ∀ b → WrongBit b → WrongBit b
{-# ATP prove bar #-}

-- $ apia --check Issue11.agda
-- apia: tptp4X found an error in the file /tmp/Issue11/29-bar.tptp

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- Parser monad
------------------------------------------------------------------------

-- This code may have bitrotted.

open import Relation.Binary
open import Relation.Binary.OrderMorphism
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)
import Relation.Binary.Props.StrictTotalOrder as STOProps
open import Data.Product

module StructurallyRecursiveDescentParsing.Memoised.Monad

  -- Input string positions.

  {Position : Set} {_<P_ : Rel Position}
  (posOrdered : IsStrictTotalOrder _≡_ _<P_)

  -- Input strings.

  (Input : Position → Set)

  -- In order to be able to store results in a memo table (and avoid
  -- having to lift the table code to Set1) the result types have to
  -- come from the following universe:

  {Result : Set} (⟦_⟧ : Result → Set)

  -- Memoisation keys. These keys must uniquely identify the
  -- computation that they are associated with, when paired up with
  -- the current input string position.

  {Key : let PosPoset = STOProps.poset
                          (record { carrier = _ ; _≈_ = _; _<_ = _
                                  ; isStrictTotalOrder = posOrdered })
             MonoFun = PosPoset ⇒-Poset PosPoset in
         MonoFun → Result → Set}
  {_≈_ _<_ : Rel (∃₂ Key)}
  (keyOrdered : IsStrictTotalOrder _≈_ _<_)

  -- Furthermore the underlying equality needs to be strong enough.

  (funsEqual    : _≈_ =[ proj₁ ]⇒ _≡_)
  (resultsEqual : _≈_ =[ (λ rfk → proj₁ (proj₂ rfk)) ]⇒ _≡_)

  where

open _⇒-Poset_
open STOProps (record { carrier = _ ; _≈_ = _; _<_ = _
                      ; isStrictTotalOrder = posOrdered })

import Data.AVL.IndexedMap as Map renaming (Map to MemoTable)
open import Category.Monad
open import Category.Monad.State
import Data.List as List; open List using (List)
open import Function using (_⟨_⟩_; _on_)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Unit using (⊤)
open import Relation.Binary.Product.StrictLex
open import Relation.Binary.Product.Pointwise
import Relation.Binary.On as On

------------------------------------------------------------------------
-- Monotone functions

MonoFun : Set
MonoFun = poset ⇒-Poset poset

------------------------------------------------------------------------
-- Memo table keys and values

-- Indices and keys used by the memo table.

Index : Set
Index = Position × MonoFun × Result

data MemoTableKey : Index → Set where
  key : ∀ {f r} (key : Key f r) pos → MemoTableKey (pos , f , r)

-- Input strings of a certain maximum length.

record Input≤ (bnd : Position) : Set where
  field
    position : Position
    bounded  : position ≤ bnd
    string   : Input position

open Input≤ public

_isBounded∶_ : ∀ {bnd pos} → Input pos → pos ≤ bnd → Input≤ bnd
xs isBounded∶ le = record { position = _; bounded = le; string = xs }

-- Memo table values.

Value : Index → Set
Value (pos , f , r) = List (⟦ r ⟧ × Input≤ (fun f pos))

------------------------------------------------------------------------
-- Parser monad

-- The parser monad is instantiated with the memo table at the end of
-- the file in order to reduce the time required to type check it.

private
 module Dummy
        (MemoTable : Set)
        (empty  : MemoTable)
        (insert : ∀ {i} → MemoTableKey i → Value i →
                                           MemoTable → MemoTable)
        (lookup : ∀ {i} → MemoTableKey i → MemoTable → Maybe (Value i))
        where

  -- The parser monad is built upon a list monad, for backtracking, and
  -- two state monads. One of the state monads stores a memo table, and
  -- is unaffected by backtracking. The other state monad, which /is/
  -- affected by backtracking, stores the remaining input string.

  -- The memo table state monad.

  module MemoState = RawMonadState (StateMonadState MemoTable)

  -- The list monad.

  module List = RawMonadPlus List.monadPlus

  -- The inner monad (memo table plus list).

  module IM where

    Inner : Set → Set
    Inner R = State MemoTable (List R)

    InnerMonadPlus : RawMonadPlus Inner
    InnerMonadPlus = record
      { monadZero = record
        { monad = record
          { return = λ x → return (List.return x)
          ; _>>=_  = λ m f → List.concat <$> (List.mapM monad f =<< m)
          }
        ; ∅ = return List.∅
        }
      ; _∣_ = λ m₁ m₂ → List._∣_ <$> m₁ ⊛ m₂
      }
      where open MemoState

    InnerMonadState : RawMonadState MemoTable Inner
    InnerMonadState = record
      { monad = RawMonadPlus.monad InnerMonadPlus
      ; get   = List.return <$> get
      ; put   = λ s → List.return <$> put s
      }
      where open MemoState

    open RawMonadPlus  InnerMonadPlus  public
    open RawMonadState InnerMonadState public
      using (get; put; modify)

  -- The complete parser monad.

  module PM where

    infixr 5 _∣_
    infixl 1 _>>=_ _>>_
    infixr 1 _=<<_

    -- Parameters:
    -- • bnd: Upper bound of the length of the input.
    -- • f:   The actual length of the output is bounded by
    --        f (actual length of the input).
    -- • A:   Result type.

    data P (bnd : Position) (f : MonoFun) (A : Set) : Set where
      pm : (im : (inp : Input≤ bnd) →
                 IM.Inner (A × Input≤ (fun f (position inp)))) →
           P bnd f A

    private

      unPM : ∀ {bnd f A} → P bnd f A → (inp : Input≤ bnd) →
             IM.Inner (A × Input≤ (fun f (position inp)))
      unPM (pm m) = m

    -- Memoises the computation, assuming that the key is sufficiently
    -- unique.

    memoise : ∀ {bnd f r} → Key f r → P bnd f ⟦ r ⟧ → P bnd f ⟦ r ⟧
    memoise {bnd} {f} {r} k (pm p) = pm helper₁
      where
      helper₁ : (inp : Input≤ bnd) →
                IM.Inner (⟦ r ⟧ × Input≤ (fun f (position inp)))
      helper₁ xs = let open IM in
                   helper₂ =<< lookup k′ <$> get
        where
        i = (position xs , f , r)

        k′ : MemoTableKey i
        k′ = key k (position xs)

        helper₂ : Maybe (Value i) → State MemoTable (Value i)
        helper₂ (just v) = return v  where open MemoState
        helper₂ nothing  = p xs                 >>= λ v →
                           modify (insert k′ v) >>
                           return v
          where open MemoState

    -- Other monadic operations.

    return : ∀ {bnd A} → A → P bnd id A
    return a =
      pm λ xs → IM.return (a , string xs isBounded∶ refl)

    _>>=_ : ∀ {bnd A B f g} →
            P bnd f A → (A → P (fun f bnd) g B) → P bnd (g ∘ f) B
    _>>=_ {f = f} {g} (pm m₁) m₂ = pm λ xs →
      m₁ xs ⟨ IM._>>=_ ⟩ λ ays →
      let a = proj₁ ays; ys = proj₂ ays in
      fix (bounded ys) ⟨ IM._<$>_ ⟩
        unPM (m₂ a) (string ys isBounded∶
                       lemma f (bounded xs) (bounded ys))
      where
      lemma : ∀ f {i j k} → j ≤ k → i ≤ fun f j → i ≤ fun f k
      lemma f j≤k i≤gj = trans i≤gj (monotone f j≤k)

      fix : ∀ {A i j} → i ≤ j →
            A × Input≤ (fun g i) →
            A × Input≤ (fun g j)
      fix le (a , xs) =
        (a , string xs isBounded∶ lemma g le (bounded xs))

    _>>_ : ∀ {bnd A B f g} →
           P bnd f A → P (fun f bnd) g B → P bnd (g ∘ f) B
    m₁ >> m₂ = m₁ >>= λ _ → m₂

    _=<<_ : ∀ {bnd A B f g} →
            (A → P (fun f bnd) g B) → P bnd f A → P bnd (g ∘ f) B
    m₂ =<< m₁ = m₁ >>= m₂

    ∅ : ∀ {bnd f A} → P bnd f A
    ∅ = pm (λ _ → IM.∅)

    _∣_ : ∀ {bnd f A} → P bnd f A → P bnd f A → P bnd f A
    pm m₁ ∣ pm m₂ = pm λ xs → IM._∣_ (m₁ xs) (m₂ xs)

    get : ∀ {bnd} → P bnd id (Input≤ bnd)
    get = pm λ xs → IM.return (xs , string xs isBounded∶ refl)

    put : ∀ {bnd bnd′} → Input≤ bnd′ → P bnd (const bnd′) ⊤
    put xs = pm λ _ → IM.return (_ , xs)

    -- A generalised variant of modify.

    gmodify : ∀ {bnd A} f →
              ((inp : Input≤ bnd) → A × Input≤ (fun f (position inp))) →
              P bnd f A
    gmodify f g = pm λ xs → IM.return (g xs)

    modify : ∀ {bnd} f →
             ((inp : Input≤ bnd) → Input≤ (fun f (position inp))) →
             P bnd f ⊤
    modify f g = gmodify f (λ xs → (_ , g xs))

    adjustBound : ∀ {bnd f g A} →
                  (∀ p → fun f p ≤ fun g p) → P bnd f A → P bnd g A
    adjustBound hyp (pm m) =
      pm λ xs →
        let le = λ (ys : _) → trans (bounded ys) (hyp (position xs)) in
        map (λ x → x) (λ ys → string ys isBounded∶ le ys)
          ⟨ IM._<$>_ ⟩
        m xs

    run : ∀ {A f pos} →
          Input pos → P pos f A → List (A × Input≤ (fun f pos))
    run xs (pm m) = proj₁ (m (xs isBounded∶ refl) empty)

------------------------------------------------------------------------
-- Memo tables

-- Shuffles the elements to simplify defining equality and order
-- relations for the keys.

shuffle : ∃ MemoTableKey → Position × ∃₂ Key
shuffle ((pos , f , r) , key k .pos) = (pos , f , r , k)

-- Equality and ordering.

Eq : Rel (∃ MemoTableKey)
Eq = _≡_ ×-Rel _≈_  on  shuffle

Lt : Rel (∃ MemoTableKey)
Lt = ×-Lex _≡_ _<P_ _<_  on  shuffle

isOrdered : IsStrictTotalOrder Eq Lt
isOrdered = On.isStrictTotalOrder shuffle
              (posOrdered ×-isStrictTotalOrder keyOrdered)

indicesEqual′ : Eq =[ proj₁ ]⇒ _≡_
indicesEqual′ {((_ , _ , _) , key _ ._)}
              {((_ , _ , _) , key _ ._)} (eq₁ , eq₂) =
  PropEq.cong₂ _,_ eq₁
    (PropEq.cong₂ _,_ (funsEqual eq₂) (resultsEqual eq₂))

open Map isOrdered (λ {k₁} {k₂} → indicesEqual′ {k₁} {k₂}) Value

-- Instantiation of the Dummy module above.

open Dummy MemoTable empty insert lookup public


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Empty.Base where

open import Cubical.Core.Everything

data ⊥ : Type₀ where

⊥-elim : ∀ {ℓ} {A : Type ℓ} → ⊥ → A
⊥-elim ()

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Luau.Addr.ToString where

open import Agda.Builtin.String using (String; primStringAppend)
open import Luau.Addr using (Addr)
open import Agda.Builtin.Int using (Int; primShowInteger; pos)

addrToString : Addr → String
addrToString a = primStringAppend "a" (primShowInteger (pos a))

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
open import Agda.Primitive

module ManySortedAlgebra where

  -- a many sorted signature
  record Signature {l : Level} : Set (lsuc l) where
    field
      sort : Set l -- sorts
      op : Set l -- operations
      arg : op → Set l
      op-sort : op → sort -- the sort of the operation
      arg-sort : ∀ {f} → arg f → sort -- the sorts of arguments

  open Signature

  -- we allow general contexts in which there are arbitrarily many variables,
  -- which makes things easier
  record Context {l : Level} (Σ : Signature {l}) : Set (lsuc l) where
    field
      var : Set l
      var-sort : var → sort Σ

  open Context

  -- terms over a signature in a context of a given sort
  data Term {l : Level} {Σ : Signature {l}} (Γ : Context Σ) : sort Σ → Set l  where
    tm-var : ∀ (x : var Γ) → Term Γ (var-sort Γ x)
    tm-op : ∀ (f : op Σ) → (∀ (i : arg Σ f) → Term Γ (arg-sort Σ i)) → Term Γ (op-sort Σ f)

  substitution : ∀ {l : Level} {Σ : Signature {l}} (Γ Δ : Context Σ) → Set l
  substitution Γ Δ = ∀ (x : var Γ) → Term Δ (var-sort Γ x)

  -- the action of a substitution on a term
  _·_ : ∀ {l : Level} {Σ : Signature {l}} {Γ Δ : Context Σ} → substitution Γ Δ → ∀ {A} → Term Γ A → Term Δ A
  σ · (tm-var x) = σ x
  σ · (tm-op f x) = tm-op f (λ i → σ · x i)

  infixr 6 _·_

  -- composition of substitutions
  _○_ : ∀ {l : Level} {Σ : Signature {l}} {Γ Δ Θ : Context Σ} → substitution Δ Θ → substitution Γ Δ → substitution Γ Θ
  (σ ○ τ) x = σ · τ x

  infixl 7 _○_

  -- an equational theory is a family of equations over a given sort
  record EquationalTheory {l : Level} (Σ : Signature {l}) : Set (lsuc l) where
    field
      eq : Set l
      eq-ctx : ∀ (ε : eq) → Context {l} Σ
      eq-sort : ∀ (ε : eq) → sort Σ
      eq-lhs : ∀ (ε : eq) → Term (eq-ctx ε) (eq-sort ε)
      eq-rhs : ∀ (ε : eq) → Term (eq-ctx ε) (eq-sort ε)

  open EquationalTheory

  infix 4 _≡_

  -- the remaining judgement form is equality
  data _≡_ {l : Level} {Σ : Signature {l}} {T : EquationalTheory {l} Σ } : {Γ : Context Σ} → {S : sort Σ} → Term Γ S → Term Γ S → Set (lsuc l) where
    -- general rules
    eq-refl : ∀ {Γ} {S : sort Σ} {t : Term Γ S} → t ≡ t
    eq-symm : ∀ {Γ} {S : sort Σ} {s t : Term {l} {Σ} Γ S} → _≡_ {T = T} s t → t ≡ s
    eq-tran : ∀ {Γ} {S : sort Σ} {s t u : Term Γ S} → _≡_ {T = T} s t → _≡_ {T = T} t u → s ≡ u
    -- congruence rule
    eq-congr : ∀ {Γ} {f : op Σ} (x y : ∀ (i : arg Σ f) → Term Γ (arg-sort Σ i)) →
               (∀ i → _≡_ {_} {_} {T} (x i) (y i)) → tm-op f x ≡ tm-op f y
    -- equational axiom
    eq-axiom : ∀ (ε : eq T) {Δ : Context Σ} (σ : substitution (eq-ctx T ε) Δ) →
               σ · eq-lhs T ε ≡ σ · eq-rhs T ε

  -- composition is functorial
  subst-○ : ∀ {l : Level} {Σ : Signature {l}} {T : EquationalTheory Σ} {Γ Δ Θ : Context Σ}
              (σ : substitution Δ Θ) (τ : substitution Γ Δ) →
              ∀ {A} (t : Term Γ A) → _≡_ {T = T} (σ · τ · t)  (σ ○ τ · t)
  subst-○ σ τ (tm-var x) = eq-refl
  subst-○ σ τ (tm-op f x) = eq-congr (λ i → σ · τ · x i) (λ i → σ ○ τ · x i) λ i → subst-○ σ τ (x i)

  -- substitution preserves equality
  eq-subst : ∀ {l : Level} {Σ : Signature {l}} {T : EquationalTheory Σ} {Γ Δ : Context Σ} {S : sort Σ} (σ : substitution Γ Δ)
               {s t : Term Γ S} → _≡_ {T = T} s t → _≡_ {T = T} (σ · s) (σ · t)
  eq-subst σ eq-refl = eq-refl
  eq-subst σ (eq-symm ξ) = eq-symm (eq-subst σ ξ)
  eq-subst σ (eq-tran ζ ξ) = eq-tran (eq-subst σ ζ) (eq-subst σ ξ)
  eq-subst σ (eq-congr x y ξ) = eq-congr (λ i → σ · x i) (λ i → σ · y i) λ i → eq-subst σ (ξ i)
  eq-subst {T = T} σ (eq-axiom ε τ) =
    eq-tran (subst-○ σ τ (eq-lhs T ε))
            (eq-tran (eq-axiom ε (σ ○ τ)) (eq-symm (subst-○ σ τ (eq-rhs T ε))))

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt