text:
------------------------------------------------------------------------
-- Unambiguity
------------------------------------------------------------------------

module TotalParserCombinators.Unambiguity where

open import Data.Product
open import Function using (_$_)
open import Function.Equivalence
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as H
  renaming (_≅_ to _≅′_)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

-- A parser is unambiguous if every string can be parsed in at most
-- one way.

Unambiguous : ∀ {Tok R xs} → Parser Tok R xs → Set₁
Unambiguous p =
  ∀ {x₁ x₂ s} (x₁∈p : x₁ ∈ p · s) (x₂∈p : x₂ ∈ p · s) →
  x₁ ≡ x₂ × x₁∈p ≅′ x₂∈p

-- Language and parser equivalence coincide for unambiguous parsers.

≈⇒≅ : ∀ {Tok R xs₁ xs₂}
        {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
      Unambiguous p₁ → Unambiguous p₂ → p₁ ≈ p₂ → p₁ ≅ p₂
≈⇒≅ u₁ u₂ p₁≈p₂ = record
  { to         = Equivalence.to   p₁≈p₂
  ; from       = Equivalence.from p₁≈p₂
  ; inverse-of = record
    { left-inverse-of  = λ x∈p₁ → H.≅-to-≡ $ proj₂ $ u₁ _ x∈p₁
    ; right-inverse-of = λ x∈p₂ → H.≅-to-≡ $ proj₂ $ u₂ _ x∈p₂
    }
  }

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Data.Num.Standard where
-- Standard positional notations

open import Data.Nat
open ≤-Reasoning
    renaming (begin_ to start_; _∎ to _□)
 -- using (≰⇒>; +-∸-assoc; ∸-mono)
open import Data.Nat.Properties
open import Data.Fin using (Fin)
    renaming (zero to Fzero; suc to Fsuc; toℕ to F→N; fromℕ≤ to N→F)
open import Data.Fin.Properties using (bounded)
open import Function
open import Relation.Nullary
-- open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse; fromWitness; fromWitnessFalse)

open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; sym; trans; inspect)
open PropEq.≡-Reasoning
open import Relation.Binary

ℕ-isDecTotalOrder   = DecTotalOrder.isDecTotalOrder decTotalOrder
ℕ-isTotalOrder      = IsDecTotalOrder.isTotalOrder ℕ-isDecTotalOrder
ℕ-isPartialOrder    = IsTotalOrder.isPartialOrder ℕ-isTotalOrder
ℕ-isPreorder        = IsPartialOrder.isPreorder ℕ-isPartialOrder
≤-refl      = IsPreorder.reflexive ℕ-isPreorder
≤-antisym   = IsPartialOrder.antisym ℕ-isPartialOrder
≤-total     = IsTotalOrder.total ℕ-isTotalOrder

data Digit : (base : ℕ) → Set where
    D : ∀ {base} → Fin base → Digit base

infixl 6 _D+_

_D+_ : ∀ {b} → Digit b → Digit b → Digit b
D x D+ D {b} y with b ≤? (F→N x + F→N y)
D x D+ D {b} y | yes p = D $ N→F {F→N x + F→N y ∸ b} $
    start
        suc (F→N x + F→N y ∸ b)
    ≤⟨ ≤-refl (sym (+-∸-assoc 1 p)) ⟩
        (suc (F→N x) + F→N y) ∸ b
    ≤⟨ ∸-mono {suc (F→N x) + F→N y} {b + b} {b} {b} (bounded x +-mono (
            start
                F→N y
            ≤⟨ n≤1+n (F→N y) ⟩
                suc (F→N y)
            ≤⟨ bounded y ⟩
                b
            □
        )) (≤-refl refl) ⟩
        b + b ∸ b
    ≤⟨ ≤-refl (m+n∸n≡m b b) ⟩
        b
    □
D x D+ D {b} y | no ¬p = D $ N→F (≰⇒> ¬p)

-- start
--     {!   !}
-- ≤⟨ {!    !} ⟩
--     {!    !}
-- ≤⟨ {!    !} ⟩
--     {!   !}
-- ≤⟨ {!    !} ⟩
--     {!   !}
-- ≤⟨ {!    !} ⟩
--     {!   !}
-- □

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

ext: agda

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts
open import lemmas-disjointness

module lemmas-freshness where
  -- if x is fresh in an hexp, it's fresh in its expansion
  mutual
    fresh-elab-synth1 : ∀{x e τ d Γ Δ} →
                         x # Γ →
                         freshh x e →
                         Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                         fresh x d
    fresh-elab-synth1 apt FHNum ESNum = FNum
    fresh-elab-synth1 apt (FRHPlus x x₄) (ESPlus gapt x₁ x₂ x₃) =
                          FPlus (FCast (fresh-elab-ana1 apt x x₂))
                                (FCast (fresh-elab-ana1 apt x₄ x₃))
    fresh-elab-synth1 apt (FRHAsc frsh) (ESAsc x₁) = FCast (fresh-elab-ana1 apt frsh x₁)
    fresh-elab-synth1 _ (FRHVar x₂) (ESVar x₃) = FVar x₂
    fresh-elab-synth1 {Γ = Γ} apt (FRHLam2 x₂ frsh) (ESLam x₃ exp) = FLam x₂ (fresh-elab-synth1 (apart-extend1 Γ x₂ apt) frsh exp)
    fresh-elab-synth1 apt (FRHAp frsh frsh₁) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) = FAp (FCast (fresh-elab-ana1 apt frsh x₅)) (FCast (fresh-elab-ana1 apt frsh₁ x₆))
    fresh-elab-synth1 apt (FRHPair frsh frsh₁) (ESPair x x₁ x₂ x₃) = FPair (fresh-elab-synth1 apt frsh x₂) (fresh-elab-synth1 apt frsh₁ x₃)
    fresh-elab-synth1 apt (FRHFst frsh) (ESFst x x₁ x₂) = FFst (FCast (fresh-elab-ana1 apt frsh x₂))
    fresh-elab-synth1 apt (FRHSnd frsh) (ESSnd x x₁ x₂) = FSnd (FCast (fresh-elab-ana1 apt frsh x₂))
    fresh-elab-synth1 apt FRHEHole ESEHole = FHole (EFId apt)
    fresh-elab-synth1 apt (FRHNEHole frsh) (ESNEHole x₁ exp) = FNEHole (EFId apt) (fresh-elab-synth1 apt frsh exp)

    fresh-elab-ana1 : ∀{x e τ d τ' Γ Δ} →
                      x # Γ →
                      freshh x e →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      fresh x d
    fresh-elab-ana1 {Γ = Γ}  apt (FRHLam1 x₁ frsh) (EALam x₂ x₃ exp) = FLam x₁ (fresh-elab-ana1 (apart-extend1 Γ x₁ apt) frsh exp )
    fresh-elab-ana1 apt frsh (EASubsume x₁ x₂ x₃ x₄) = fresh-elab-synth1 apt frsh x₃
    fresh-elab-ana1 apt (FRHInl frsh) (EAInl x x₁) = FInl (fresh-elab-ana1 apt frsh x₁)
    fresh-elab-ana1 apt (FRHInr frsh) (EAInr x x₁) = FInr (fresh-elab-ana1 apt frsh x₁)
    fresh-elab-ana1 {Γ = Γ} apt (FRHCase frsh x₁ frsh₁ x₂ frsh₂) (EACase x x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃) = FCase (FCast (fresh-elab-synth1 apt frsh x₁₀)) x₁ (FCast (fresh-elab-ana1 (apart-extend1 Γ x₁ apt) frsh₁ x₁₂)) x₂ (FCast (fresh-elab-ana1 (apart-extend1 Γ x₂ apt) frsh₂ x₁₃))
    fresh-elab-ana1 apt FRHEHole EAEHole = FHole (EFId apt)
    fresh-elab-ana1 apt (FRHNEHole frsh) (EANEHole x₁ x₂) = FNEHole (EFId apt) (fresh-elab-synth1 apt frsh x₂)

  -- if x is fresh in the expansion of an hexp, it's fresh in that hexp
  mutual
    fresh-elab-synth2 : ∀{x e τ d Γ Δ} →
                         fresh x d →
                         Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                         freshh x e
    fresh-elab-synth2 FNum ESNum = FRHNum
    fresh-elab-synth2 (FPlus (FCast x) (FCast x₄)) (ESPlus apt x₁ x₂ x₃) =
      FRHPlus (fresh-elab-ana2 x x₂) (fresh-elab-ana2 x₄ x₃)
    fresh-elab-synth2 (FVar x₂) (ESVar x₃) = FRHVar x₂
    fresh-elab-synth2 (FLam x₂ frsh) (ESLam x₃ exp) = FRHLam2 x₂ (fresh-elab-synth2 frsh exp)
    fresh-elab-synth2 (FAp (FCast frsh) (FCast frsh₁)) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) = FRHAp (fresh-elab-ana2 frsh x₅) (fresh-elab-ana2 frsh₁ x₆)
    fresh-elab-synth2 (FPair frsh frsh₁) (ESPair x x₁ x₂ x₃) = FRHPair (fresh-elab-synth2 frsh x₂) (fresh-elab-synth2 frsh₁ x₃)
    fresh-elab-synth2 (FFst (FCast frsh)) (ESFst x x₁ x₂) = FRHFst (fresh-elab-ana2 frsh x₂)
    fresh-elab-synth2 (FSnd (FCast frsh)) (ESSnd x x₁ x₂) = FRHSnd (fresh-elab-ana2 frsh x₂)
    fresh-elab-synth2 (FHole x₁) ESEHole = FRHEHole
    fresh-elab-synth2 (FNEHole x₁ frsh) (ESNEHole x₂ exp) = FRHNEHole (fresh-elab-synth2 frsh exp)
    fresh-elab-synth2 (FCast frsh) (ESAsc x₁) = FRHAsc (fresh-elab-ana2 frsh x₁)

    fresh-elab-ana2 : ∀{ x e τ d τ' Γ Δ} →
                      fresh x d →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      freshh x e
    fresh-elab-ana2 (FLam x₁ frsh) (EALam x₂ x₃ exp) = FRHLam1 x₁ (fresh-elab-ana2 frsh exp)
    fresh-elab-ana2 frsh (EASubsume x₁ x₂ x₃ x₄) = fresh-elab-synth2 frsh x₃
    fresh-elab-ana2 (FHole x₁) EAEHole = FRHEHole
    fresh-elab-ana2 (FNEHole x₁ frsh) (EANEHole x₂ x₃) = FRHNEHole (fresh-elab-synth2 frsh x₃)
    fresh-elab-ana2 (FInl frsh) (EAInl x x₁) = FRHInl (fresh-elab-ana2 frsh x₁)
    fresh-elab-ana2 (FInr frsh) (EAInr x x₁) = FRHInr (fresh-elab-ana2 frsh x₁)
    fresh-elab-ana2 (FCase (FCast frsh) x (FCast frsh₁) x₁ (FCast frsh₂)) (EACase x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃) = FRHCase (fresh-elab-synth2 frsh x₁₀) x (fresh-elab-ana2 frsh₁ x₁₂) x₁ (fresh-elab-ana2 frsh₂ x₁₃)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module SN where

open import Relation.Unary using (_∈_; _⊆_)
open import Library
open import Terms
open import Substitution
open import TermShape public

-- Inductive definition of strong normalization.

infix 7 _⟨_⟩⇒_ _⇒ˢ_

mutual

  -- Strongly normalizing evaluation contexts

  SNhole : ∀ {i : Size} {Γ : Cxt} {a b : Ty} → Tm Γ b → ECxt Γ a b → Tm Γ a → Set
  SNhole {i} = PCxt (SN {i})

  -- Strongly neutral terms.

  SNe : ∀ {i : Size} {Γ} {b} → Tm Γ b → Set
  SNe {i} = PNe (SN {i})

  -- Strongly normalizing terms.

  data SN {i : Size}{Γ} : ∀ {a} → Tm Γ a → Set where

    ne   : ∀ {j : Size< i} {a t}
           → (𝒏 : SNe {j} t)
           → SN {a = a} t

    abs  : ∀ {j : Size< i} {a b}{t : Tm (a ∷ Γ) b}
           → (𝒕 : SN {j} t)
           → SN (abs t)

    exp  : ∀ {j₁ j₂ : Size< i} {a t t′}
           → (t⇒ :  t ⟨ j₁ ⟩⇒ t′) (𝒕′ : SN {j₂} t′)
           → SN {a = a} t

  _⟨_⟩⇒_ : ∀ {Γ a} → Tm Γ a → Size → Tm Γ a → Set
  t ⟨ i ⟩⇒ t′ = SN {i} / t ⇒ t′

  -- Strong head reduction

  _⇒ˢ_ : ∀ {i : Size} {Γ} {a} → Tm Γ a → Tm Γ a → Set
  _⇒ˢ_ {i} t t' = (SN {i}) / t ⇒ t'

-- -- Inductive definition of strong normalization.

-- mutual

--   -- Strongly normalizing evaluation contexts

--   data SNhole {i : Size} (n : ℕ) {Γ : Cxt} : {a b : Ty} → Tm Γ b → ECxt Γ a b → Tm Γ a → Set where

--     appl  : ∀ {a b t u}
--             → (𝒖 : SN {i} n u)
--             → SNhole n (app t u) (appl u) (t ∶ (a →̂ b))

--   -- Strongly neutral terms.

--   data SNe {i : Size} (n : ℕ) {Γ} {b} : Tm Γ b → Set where

--     var  : ∀ x                              → SNe n (var x)

--     elim : ∀ {a} {t : Tm Γ a} {E Et}
--            → (𝒏 : SNe {i} n t) (𝑬𝒕 : SNhole {i} n Et E t) → SNe n Et
--     -- elim : ∀ {j₁ j₂ : Size< i}{a} {t : Tm Γ a} {E Et}
--     --        → (𝒏 : SNe {j₁} n t) (𝑬𝒕 : SNhole {j₂} n Et E t) → SNe n Et

--   -- Strongly normalizing terms.

--   data SN {i : Size}{Γ} : ℕ → ∀ {a} → Tm Γ a → Set where

--     ne   : ∀ {j : Size< i} {a n t}
--            → (𝒏 : SNe {j} n t)
--            → SN n {a} t

--     abs  : ∀ {j : Size< i} {a b n}{t : Tm (a ∷ Γ) b}
--            → (𝒕 : SN {j} n t)
--            → SN n (abs t)

--     exp  : ∀ {j₁ j₂ : Size< i} {a n t t′}
--            → (t⇒ : j₁ size t ⟨ n ⟩⇒ t′) (𝒕′ : SN {j₂} n t′)
--            → SN n {a} t

--   _size_⟨_⟩⇒_ : ∀ (i : Size) {Γ}{a} → Tm Γ a → ℕ → Tm Γ a → Set
--   i size t ⟨ n ⟩⇒ t′ = _⟨_⟩⇒_ {i} t n t′

--   -- Strong head reduction

--   data _⟨_⟩⇒_ {i : Size} {Γ} : ∀ {a} → Tm Γ a → ℕ → Tm Γ a → Set where

--     β     : ∀  {a b}{t : Tm (a ∷ Γ) b}{u}
--             → (𝒖 : SN {i} n u)
--             → (app (abs t) u) ⟨ n ⟩⇒ subst0 u t

--     cong  : ∀  {a b t t' Et Et'}{E : ECxt Γ a b}
--             → (𝑬𝒕 : Ehole Et E t)
--             → (𝑬𝒕' : Ehole Et' E t')
--             → (t⇒ : i size t ⟨ n ⟩⇒ t')
--             → Et ⟨ n ⟩⇒ Et'

    -- β     : ∀ {j : Size< i} {a b}{t : Tm (a ∷ Γ) b}{u}
    --         → (𝒖 : SN {j} n u)
    --         → (app (abs t) u) ⟨ n ⟩⇒ subst0 u t

    -- cong  : ∀ {j : Size< i} {a b t t' Et Et'}{E : ECxt Γ a b}
    --         → (𝑬𝒕 : Ehole Et E t)
    --         → (𝑬𝒕' : Ehole Et' E t')
    --         → (t⇒ : j size t ⟨ n ⟩⇒ t')
    --         → Et ⟨ n ⟩⇒ Et'

-- Strong head reduction is deterministic.

det⇒ : ∀ {a Γ} {t t₁ t₂ : Tm Γ a}
       → (t⇒₁ : t ⟨ _ ⟩⇒ t₁) (t⇒₂ : t ⟨ _ ⟩⇒ t₂) → t₁ ≡ t₂
det⇒ (β _) (β _)                                              = ≡.refl
det⇒ (β _) (cong (appl u) (appl .u) (cong () _ _))
det⇒ (cong (appl u) (appl .u) (cong () _ _)) (β _)
det⇒ (cong (appl u) (appl .u) x) (cong (appl .u) (appl .u) y) = ≡.cong (λ t → app t u) (det⇒ x y)

-- Strongly neutrals are closed under application.

sneApp : ∀{Γ a b}{t : Tm Γ (a →̂ b)}{u : Tm Γ a} →
  SNe t → SN u → SNe (app t u)
sneApp 𝒏 𝒖 = elim 𝒏 (appl 𝒖)

-- Substituting strongly neutral terms

record RenSubSNe {i} (vt : VarTm i) (Γ Δ : Cxt) : Set where
  constructor _,_
  field theSubst : RenSub vt Γ Δ
        isSNe    : ∀ {a} (x : Var Γ a) → SNe (vt2tm _ (theSubst x))
open RenSubSNe

RenSN    = RenSubSNe `Var
SubstSNe = RenSubSNe `Tm

-- The singleton SNe substitution.
-- Replaces the first variable by another variable.

sgs-varSNe : ∀ {Γ a} → Var Γ a → SubstSNe (a ∷ Γ) Γ
theSubst (sgs-varSNe x)         = sgs (var x)
isSNe    (sgs-varSNe x) (zero)  = (var x)
isSNe    (sgs-varSNe x) (suc y) = var y

-- The SN-notions are closed under SNe substitution.

mutual
  substSNh : ∀ {i vt Γ Δ a b} → (σ : RenSubSNe {i} vt Γ Δ) → ∀ {E : ECxt Γ a b}{Et t} → (SNh : SNhole Et E t)
                                → SNhole (subst (theSubst σ) Et) (substEC (theSubst σ) E) (subst (theSubst σ) t)
  substSNh σ (appl u) = appl (substSN σ u)

  subst⇒ : ∀ {i vt Γ Δ a} (σ : RenSubSNe {i} vt Γ Δ) {t t' : Tm Γ a} → t ⟨ _ ⟩⇒ t' → subst (theSubst σ) t ⟨ _ ⟩⇒ subst (theSubst σ) t'
  subst⇒ (σ , σ∈Ne) (β {t = t} {u = u} x) = ≡.subst (λ t' → app (abs (subst (lifts σ) t)) (subst σ u) ⟨ _ ⟩⇒ t')
                                                   (sgs-lifts-term {σ = σ} {u} {t})
                                                   (β {t = subst (lifts σ) t} (substSN (σ , σ∈Ne) x))

  subst⇒ σ (cong Eh Eh' t→t')    = cong (substEh (theSubst σ) Eh) (substEh (theSubst σ) Eh') (subst⇒ σ t→t')

  -- Lifting a SNe substitution.

  liftsSNe : ∀ {i vt Γ Δ a} → RenSubSNe {i} vt Γ Δ → RenSubSNe {i} vt (a ∷ Γ) (a ∷ Δ)
  theSubst (liftsSNe σ)                   = lifts (theSubst σ)
  isSNe    (liftsSNe {vt = `Var} (σ , σ∈SNe)) (zero)    = var (zero)
  isSNe    (liftsSNe {vt = `Var} (σ , σ∈SNe)) (suc y) = var (suc (σ y))
  isSNe    (liftsSNe {vt = `Tm } (σ , σ∈SNe)) (zero)    = var (zero)
  isSNe    (liftsSNe {vt = `Tm } (σ , σ∈SNe)) (suc y) = substSNe {vt = `Var} (suc , (λ x → var (suc x))) (σ∈SNe y)

  substSNe : ∀ {i vt Γ Δ τ} → (σ : RenSubSNe {i} vt Γ Δ) → ∀ {t : Tm Γ τ} → SNe t → SNe (subst (theSubst σ) t)
  substSNe σ (var x)            = isSNe σ x
  substSNe σ (elim t∈SNe E∈SNh) = elim (substSNe σ t∈SNe) (substSNh σ E∈SNh)

  substSN : ∀ {i vt Γ Δ τ} → (σ : RenSubSNe {i} vt Γ Δ) → ∀ {t : Tm Γ τ} → SN t → SN (subst (theSubst σ) t)
  substSN σ (ne t∈SNe)         = ne (substSNe σ t∈SNe)
  substSN σ (abs t∈SN)         = abs (substSN (liftsSNe σ) t∈SN)
  substSN σ (exp t→t' t'∈SN)   = exp (subst⇒ σ t→t') (substSN σ t'∈SN)

-- SN is closed under renaming.

renSN :  ∀{Γ Δ} (ρ : Γ ≤ Δ) → RenSN Δ Γ
renSN ρ = (ρ , λ x → var (ρ x))

renameSNe : ∀{a Γ Δ} (ρ : Γ ≤ Δ) {t : Tm Δ a} →
  SNe t → SNe (rename ρ t)
renameSNe ρ = substSNe (renSN ρ)

renameSN : ∀{a Γ Δ} (ρ : Γ ≤ Δ) {t : Tm Δ a} →
  SN t → SN (rename ρ t)
renameSN ρ = substSN (renSN ρ)

-- Variables are SN.

varSN : ∀{Γ a x} → var x ∈ SN {Γ = Γ} {a}
varSN = ne (var _)

-- SN is closed under application to variables.

appVarSN : ∀{Γ a b}{t : Tm Γ (a →̂ b)}{x} → t ∈ SN → app t (var x) ∈ SN
appVarSN (ne t∈SNe)       = ne (elim t∈SNe (appl varSN))
appVarSN (abs t∈SN)       = exp (β varSN) (substSN (sgs-varSNe _) t∈SN)
appVarSN (exp t→t' t'∈SN) = exp (cong (appl (var _)) (appl (var _)) t→t') (appVarSN t'∈SN)

-- Subterm properties of SN

-- If app t u ∈ SN then u ∈ SN.

apprSN : ∀{i a b Γ}{t : Tm Γ (a →̂ b)}{u : Tm Γ a} → SN {i} (app t u) → SN {i} u
apprSN (ne (elim 𝒏 (appl 𝒖)))               = 𝒖
apprSN (exp (β 𝒖) 𝒕)                        = 𝒖
apprSN (exp (cong (appl u) (appl .u) t⇒) 𝒕) = apprSN 𝒕

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
-- This module is used to illustrate how to import a parameterised module.
module examples.syntax.ModuleB
	(A : Set)
	((==) : A -> A -> Prop)
	(refl : (x : A) -> x == x)
    where

  infix 5 /\

  module SubModule where
    postulate dummy : A

  data True : Prop where
    tt : True

  data False : Prop where

  data (/\) (P, Q : Prop) : Prop where
    andI : P -> Q -> P /\ Q

  data List : Set where
    nil	  : List
    cons  : A -> List -> List

  eqList : List -> List -> Prop
  eqList nil         nil	  =  True
  eqList (cons x xs) nil          =  False
  eqList nil         (cons y ys)  =  False
  eqList (cons x xs) (cons y ys)  =  x == y /\ eqList xs ys

  reflEqList : (xs : List) -> eqList xs xs
  reflEqList nil	  = tt
  reflEqList (cons x xs)  = andI (refl x) (reflEqList xs)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NatEquality where

open import Definitions

_≟_ : (m n : ℕ) → Equal? m n
_≟_ = {!!}

equality-disjoint : (m n : ℕ) → m ≡ n → m ≢ n → ⊥
equality-disjoint = {!!}

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
------------------------------------------------------------------------
-- This module proves that the parser combinators correspond exactly
-- to functions of type List Tok → List R (if bag equality is used for
-- the lists of results)
------------------------------------------------------------------------

module TotalParserCombinators.ExpressiveStrength where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.List as List
open import Data.List.Membership.Propositional
import Data.List.Properties as ListProp
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.List.Relation.Unary.Any
open import Data.List.Reverse
open import Data.Product
open import Function.Base
open import Function.Inverse using (_↔_)
import Function.Related as Related
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality
  using (_≅_; _≇_; refl)
open import Relation.Nullary

open Related using (SK-sym)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S
  hiding (_≅_; _∼[_]_; token)
open import TotalParserCombinators.Lib
private
  open module Tok = Token Bool _≟_ using (tok)
open import TotalParserCombinators.BreadthFirst as Backend
  using (parse)

------------------------------------------------------------------------
-- Expressive strength

-- One direction of the correspondence has already been established:
-- For every parser there is an equivalent function.

parser⇒fun : ∀ {R xs} (p : Parser Bool R xs) {x s} →
             x ∈ p · s ↔ x ∈ parse p s
parser⇒fun p = Backend.parse-correct

-- For every function there is a corresponding parser.

module Monadic where

  -- The parser.

  grammar : ∀ {Tok R} (f : List Tok → List R) → Parser Tok R (f [])
  grammar f = token >>= (λ t → ♯ grammar (f ∘ _∷_ t))
            ∣ return⋆ (f [])

  -- Correctness proof.

  grammar-correct : ∀ {Tok R} (f : List Tok → List R) {x s} →
                    x ∈ grammar f · s ↔ x ∈ f s
  grammar-correct f {s = s} = record
    { to         = P.→-to-⟶ (sound f)
    ; from       = P.→-to-⟶ (complete f s)
    ; inverse-of = record
      { left-inverse-of  = complete∘sound f
      ; right-inverse-of = sound∘complete f s
      }
    }
    where
    sound : ∀ {Tok R x s} (f : List Tok → List R) →
            x ∈ grammar f · s → x ∈ f s
    sound f (∣-right ._ x∈) with Return⋆.sound (f []) x∈
    ... | (refl , x∈′) = x∈′
    sound f (∣-left (S.token {t} >>= x∈)) = sound (f ∘ _∷_ t) x∈

    complete : ∀ {Tok R x} (f : List Tok → List R) s →
               x ∈ f s → x ∈ grammar f · s
    complete f []      x∈ = ∣-right [] (Return⋆.complete x∈)
    complete f (t ∷ s) x∈ =
      ∣-left ([ ○ - ◌ ] S.token >>= complete (f ∘ _∷_ t) s x∈)

    complete∘sound : ∀ {Tok R x s} (f : List Tok → List R)
                     (x∈pf : x ∈ grammar f · s) →
                     complete f s (sound f x∈pf) ≡ x∈pf
    complete∘sound f (∣-left (S.token {t} >>= x∈))
      rewrite complete∘sound (f ∘ _∷_ t) x∈ = refl
    complete∘sound f (∣-right .[] x∈)
      with Return⋆.sound (f []) x∈ | Return⋆.complete∘sound (f []) x∈
    complete∘sound f (∣-right .[] .(Return⋆.complete x∈f[]))
      | (refl , x∈f[]) | refl = refl

    sound∘complete : ∀ {Tok R x} (f : List Tok → List R) s
                     (x∈fs : x ∈ f s) →
                     sound f (complete f s x∈fs) ≡ x∈fs
    sound∘complete       f (t ∷ s) x∈ = sound∘complete (f ∘ _∷_ t) s x∈
    sound∘complete {Tok} f []      x∈
      with Return⋆.sound {Tok = Tok} (f []) (Return⋆.complete x∈)
         | Return⋆.sound∘complete {Tok = Tok} x∈
    ... | (refl , .x∈) | refl = refl

  -- A corollary.

  maximally-expressive :
    ∀ {Tok R} (f : List Tok → List R) {s} →
    parse (grammar f) s ∼[ bag ] f s
  maximally-expressive f {s} {x} =
    (x ∈ parse (grammar f) s)  ↔⟨ SK-sym Backend.parse-correct ⟩
    x ∈ grammar f · s          ↔⟨ grammar-correct f ⟩
    x ∈ f s                    ∎
    where open Related.EquationalReasoning

-- If the token type is finite (in this case Bool), then the result
-- above can be established without the use of bind (_>>=_). (The
-- definition of tok uses bind, but if bind were removed it would be
-- reasonable to either add tok as a primitive combinator, or make it
-- possible to define tok using other combinators.)

module Applicative where

  -- A helper function.

  specialise : {A B : Set} → (List A → B) → A → (List A → B)
  specialise f x = λ xs → f (xs ∷ʳ x)

  -- The parser.

  grammar : ∀ {R} (f : List Bool → List R) → Parser Bool R (f [])
  grammar f =
      ♯ (const <$> grammar (specialise f true )) ⊛ tok true
    ∣ ♯ (const <$> grammar (specialise f false)) ⊛ tok false
    ∣ return⋆ (f [])

  -- Correctness proof.

  grammar-correct : ∀ {R} (f : List Bool → List R) {x s} →
                    x ∈ grammar f · s ↔ x ∈ f s
  grammar-correct {R} f {s = s} = record
    { to         = P.→-to-⟶ (sound f)
    ; from       = P.→-to-⟶ (complete f (reverseView s))
    ; inverse-of = record
      { right-inverse-of = sound∘complete f (reverseView s)
      ; left-inverse-of  = λ x∈ →
          complete∘sound f (reverseView s) _ x∈ refl refl
      }
    }
    where
    sound : ∀ {x : R} {s} f → x ∈ grammar f · s → x ∈ f s
    sound f (∣-right ._ x∈) with Return⋆.sound (f []) x∈
    ... | (refl , x∈′) = x∈′
    sound f (∣-left (∣-left (<$> x∈ ⊛ t∈))) with Tok.sound true t∈
    ... | (refl , refl) = sound (specialise f true ) x∈
    sound f (∣-left (∣-right ._ (<$> x∈ ⊛ t∈))) with Tok.sound false t∈
    ... | (refl , refl) = sound (specialise f false) x∈

    complete : ∀ {x : R} {s} f → Reverse s →
               x ∈ f s → x ∈ grammar f · s
    complete f []                 x∈ = ∣-right [] (Return⋆.complete x∈)
    complete f (bs ∶ rs ∶ʳ true ) x∈ =
      ∣-left {xs₁ = []} (∣-left (
        [ ◌ - ○ ] <$> complete (specialise f true ) rs x∈ ⊛ Tok.complete))
    complete f (bs ∶ rs ∶ʳ false) x∈ =
      ∣-left (∣-right [] (
        [ ◌ - ○ ] <$> complete (specialise f false) rs x∈ ⊛ Tok.complete))

    sound∘complete : ∀ {x : R} {s} f (rs : Reverse s) (x∈fs : x ∈ f s) →
                     sound f (complete f rs x∈fs) ≡ x∈fs
    sound∘complete f [] x∈
      rewrite Return⋆.sound∘complete {Tok = Bool} x∈ = refl
    sound∘complete f (bs ∶ rs ∶ʳ true) x∈ =
      sound∘complete (specialise f true) rs x∈
    sound∘complete f (bs ∶ rs ∶ʳ false) x∈ =
      sound∘complete (specialise f false) rs x∈

    complete∘sound : ∀ {x : R} {s s′ : List Bool}
                     f (rs : Reverse s) (rs′ : Reverse s′)
                     (x∈pf : x ∈ grammar f · s) → s ≡ s′ → rs ≅ rs′ →
                     complete f rs (sound f x∈pf) ≡ x∈pf

    complete∘sound f rs rs′ (∣-right ._ x∈) s≡ rs≅
      with Return⋆.sound (f []) x∈
         | Return⋆.complete∘sound (f []) x∈
    complete∘sound f ._ []                 (∣-right ._ .(Return⋆.complete x∈′)) refl refl | (refl , x∈′) | refl = refl
    complete∘sound f _  ([]      ∶ _ ∶ʳ _) (∣-right ._ .(Return⋆.complete x∈′)) ()   _    | (refl , x∈′) | refl
    complete∘sound f _  ((_ ∷ _) ∶ _ ∶ʳ _) (∣-right ._ .(Return⋆.complete x∈′)) ()   _    | (refl , x∈′) | refl

    complete∘sound f rs rs′ (∣-left (∣-left (<$> x∈ ⊛ t∈))) s≡ rs≅ with Tok.sound true t∈
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ true)  (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₁ $ ListProp.∷ʳ-injective bs bs′ s≡
    complete∘sound f rs (.bs ∶ rs′ ∶ʳ true)  (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl with s≡ | rs≅
    complete∘sound f ._ (.bs ∶ rs′ ∶ʳ true)  (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl | refl | refl
      rewrite complete∘sound (specialise f true) rs′ rs′ x∈ refl refl
            | Tok.η t∈ = refl
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ false) (∣-left (∣-left (_⊛_ {s₁ = bs}    (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₂ $ ListProp.∷ʳ-injective bs bs′ s≡
    ... | ()
    complete∘sound f rs []                   (∣-left (∣-left (_⊛_ {s₁ = []}    (<$> x∈) t∈))) () _   | (refl , refl)
    complete∘sound f rs []                   (∣-left (∣-left (_⊛_ {s₁ = _ ∷ _} (<$> x∈) t∈))) () _   | (refl , refl)

    complete∘sound f rs rs′ (∣-left (∣-right ._ (<$> x∈ ⊛ t∈))) s≡ rs≅ with Tok.sound false t∈
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ false) (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₁ $ ListProp.∷ʳ-injective bs bs′ s≡
    complete∘sound f rs (.bs ∶ rs′ ∶ʳ false) (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl with s≡ | rs≅
    complete∘sound f ._ (.bs ∶ rs′ ∶ʳ false) (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl) | refl | refl | refl
      rewrite complete∘sound (specialise f false) rs′ rs′ x∈ refl refl
            | Tok.η t∈ = refl
    complete∘sound f rs (bs′ ∶ rs′ ∶ʳ true)  (∣-left (∣-right ._ (_⊛_ {s₁ = bs} (<$> x∈) t∈))) s≡ rs≅ | (refl , refl)
      with proj₂ $ ListProp.∷ʳ-injective bs bs′ s≡
    ... | ()
    complete∘sound f rs []                   (∣-left (∣-right ._ (_⊛_ {s₁ = []} (<$> x∈) t∈))) () _   | (refl , refl)
    complete∘sound f rs []                (∣-left (∣-right ._ (_⊛_ {s₁ = _ ∷ _} (<$> x∈) t∈))) () _   | (refl , refl)

  -- A corollary.

  maximally-expressive :
    ∀ {R} (f : List Bool → List R) {s} →
    parse (grammar f) s ∼[ bag ] f s
  maximally-expressive f {s} {x} =
    (x ∈ parse (grammar f) s)  ↔⟨ SK-sym Backend.parse-correct ⟩
    x ∈ grammar f · s          ↔⟨ grammar-correct f ⟩
    x ∈ f s                    ∎
    where open Related.EquationalReasoning

max_stars_repo_name: nad/parser-combinators


text:
module Everything where

import Records
import Basics
import Modules
import With
import Families
import Datatypes
import Bool
import Naturals

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Definitional interpreters can model systems with bounded space
------------------------------------------------------------------------

-- In "Reasoning on Divergent Computations with Coaxioms" Ancona,
-- Dagnino and Zucca write the following:
--
--   "To assess the applicability and generality of our approach much
--   work is still needed. We are currently considering to apply
--   coaxioms to other kinds of semantics; in particular, trace
--   semantics seems particularly interesting for investigating
--   whether our approach is suitable for formalizing and proving
--   important safety properties of non terminating programs, as
--   ensuring that a server will never try to use infinite resources.
--   Other approaches based on definitional interpreters [Danielsson
--   2012], and the adoption of step counters [Amin and Rompf 2017;
--   Ancona 2014; Ernst et al. 2006; Owens et al. 2016] seem to be
--   appealing for proving type soundness properties with big-step
--   semantics, and other results concerning program equivalence;
--   however, it is not clear whether these solutions work well for
--   other kinds of properties. For instance, if a program consists of
--   an infinite loop that allocates new heap space at each step
--   without releasing it, one would like to conclude that it will
--   eventually crash even though a definitional interpreter returns
--   timeout for all possible values of the step counter."
--
-- This is an attempt to show that definitional interpreters can
-- handle this situation.

module Bounded-space where

open import Equality.Propositional
open import Prelude
open import Tactic.By.Propositional
open import Prelude.Size

open import Colist equality-with-J
open import Nat equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity as B
  hiding (reflexive; symmetric)

open import Only-allocation

------------------------------------------------------------------------
-- Heaps

-- Bounded heaps. (Only a size, plus a proof showing that the size is
-- bounded.)

record Heap (limit : ℕ) : Type where
  field
    size  : ℕ
    bound : size ≤ limit

open Heap public

-- An empty heap.

empty : ∀ {l} → Heap l
empty = record { size = zero; bound = zero≤ _ }

-- A full heap.

full : ∀ l → Heap l
full l = record { size = l; bound = ≤-refl }

-- Reduces the heap's size by one. If the heap is empty, then it is
-- returned unchanged.

shrink : ∀ {l} → Heap l → Heap l
shrink {l} h = record
  { size  = pred (h .size)
  ; bound = pred (h .size)  ≤⟨ pred≤ _ ⟩
            h .size         ≤⟨ h .bound ⟩∎
            l               ∎≤
  }

-- Increases the heap's size by one. If the heap already has the
-- maximum size, then nothing is returned.

grow : ∀ {l} → Heap l → Maybe (Heap l)
grow {l} h with l ≤⊎> h .size
... | inj₁ _   = nothing
... | inj₂ h<l = just (record { size  = suc (h .size)
                              ; bound = h<l
                              })

-- Lemmas related to grow.

grow-full :
  ∀ {l} (h : Heap l) → h .size ≡ l → grow h ≡ nothing
grow-full {l} h h≡l with l ≤⊎> h .size
... | inj₁ _   = refl
... | inj₂ h<l =
  ⊥-elim (+≮ 0 (
    1 + h .size  ≤⟨ h<l ⟩
    l            ≡⟨ sym h≡l ⟩≤
    h .size      ∎≤))

grow-not-full :
  ∀ {l} (h : Heap l) →
  h .size < l → ∃ λ h′ → grow h ≡ just h′ × h′ .size ≡ 1 + h .size
grow-not-full {l} h h<l with l ≤⊎> h .size
... | inj₂ _   = _ , refl , refl
... | inj₁ l≤h =
  ⊥-elim (+≮ 0 (
    1 + h .size  ≤⟨ h<l ⟩
    l            ≤⟨ l≤h ⟩∎
    h .size      ∎≤))

------------------------------------------------------------------------
-- Definitional interpreter

-- One step of computation.

step : ∀ {l} → Stmt → Heap l → Maybe (Heap l)
step dealloc heap = just (shrink heap)
step alloc   heap = grow heap

-- A crashing computation.

crash : ∀ {i l} → Delay (Maybe (Heap l)) i
crash = now nothing

-- A definitional interpreter.

⟦_⟧ : ∀ {i l} → Program i → Heap l → Delay (Maybe (Heap l)) i
⟦ []    ⟧ heap = now (just heap)
⟦ s ∷ p ⟧ heap with step s heap
... | nothing       = crash
... | just new-heap = later λ { .force → ⟦ p .force ⟧ new-heap }

------------------------------------------------------------------------
-- A program equivalence

-- An equivalence relation that identifies programs that, given a
-- sufficient amount of memory, behave identically (up to weak
-- bisimilarity).

infix 4 [_]_≃_ [_]_≃′_

[_]_≃_ : Size → Program ∞ → Program ∞ → Type
[ i ] p ≃ q =
  ∃ λ c →
  ∀ l (h : Heap l) →
  c + h .size ≤ l →
  [ i ] ⟦ p ⟧ h ≈ ⟦ q ⟧ h

[_]_≃′_ : Size → Program ∞ → Program ∞ → Type
[ i ] p ≃′ q =
  ∃ λ c →
  ∀ l (h : Heap l) →
  c + h .size ≤ l →
  [ i ] ⟦ p ⟧ h ≈′ ⟦ q ⟧ h

-- The relation is an equivalence relation.

reflexive : ∀ {i} p → [ i ] p ≃ p
reflexive _ = 0 , λ _ _ _ → B.reflexive _

symmetric : ∀ {i p q} → [ i ] p ≃ q → [ i ] q ≃ p
symmetric = Σ-map id λ hyp l h c → B.symmetric (hyp l h c)

transitive : ∀ {i p q r} → [ ∞ ] p ≃ q → [ ∞ ] q ≃ r → [ i ] p ≃ r
transitive {p = p} {q} {r} (c₁ , p₁) (c₂ , p₂) =
  max c₁ c₂ , λ l h c →
    ⟦ p ⟧ h  ≈⟨ p₁ l h (lemma₁ l h c) ⟩
    ⟦ q ⟧ h  ≈⟨ p₂ l h (lemma₂ l h c) ⟩∎
    ⟦ r ⟧ h  ∎
  where
  lemma₁ = λ l h c →
    c₁ + h .size         ≤⟨ ˡ≤max c₁ _ +-mono ≤-refl ⟩
    max c₁ c₂ + h .size  ≤⟨ c ⟩∎
    l                   ∎≤

  lemma₂ = λ l h c →
    c₂ + h .size         ≤⟨ ʳ≤max c₁ _ +-mono ≤-refl ⟩
    max c₁ c₂ + h .size  ≤⟨ c ⟩∎
    l                   ∎≤

-- The relation is compatible with respect to the program formers.

[]-cong : ∀ {i} → [ i ] [] ≃ []
[]-cong = reflexive []

∷-cong : ∀ {s p q i} → [ i ] p .force ≃′ q .force → [ i ] s ∷ p ≃ s ∷ q
∷-cong {dealloc} (c , p≈q) =
  c , λ l h c≤ → later λ { .force → p≈q l (shrink h) (
        c + shrink h .size  ≤⟨ ≤-refl {n = c} +-mono pred≤ _ ⟩
        c + h .size         ≤⟨ c≤ ⟩
        l                   ∎≤) .force }
∷-cong {alloc} {p} {q} {i} (c , p≈q) = 1 + c , lemma
  where
  lemma : ∀ l (h : Heap l) → 1 + c + h .size ≤ l →
          [ i ] ⟦ alloc ∷ p ⟧ h ≈ ⟦ alloc ∷ q ⟧ h
  lemma l h 1+c≤ with l ≤⊎> h .size
  ... | inj₁ _   = now
  ... | inj₂ h<l = later λ { .force → p≈q l _ (
                     c + (1 + h .size)  ≡⟨ +-assoc c ⟩≤
                     c + 1 + h .size    ≡⟨ by (+-comm c) ⟩≤
                     1 + c + h .size    ≤⟨ 1+c≤ ⟩∎
                     l                  ∎≤) .force }

------------------------------------------------------------------------
-- Some examples

-- The program bounded crashes when the heap is full.

bounded-crash :
  ∀ {i l} (h : Heap l) →
  h .size ≡ l →
  [ i ] ⟦ bounded ⟧ h ≈ crash
bounded-crash h h≡l
  rewrite grow-full h h≡l =
  now

-- However, for smaller heaps the program loops.

bounded-loop :
  ∀ {i l} (h : Heap l) →
  h .size < l →
  [ i ] ⟦ bounded ⟧ h ≈ never
bounded-loop {l = l} h <l
  with grow h | grow-not-full h <l
... | .(just h′) | h′ , refl , refl =
  later λ { .force →
  later λ { .force →
  bounded-loop _ <l }}

-- The program bounded₂ loops when there are at least two empty slots
-- in the heap.

bounded₂-loop :
  ∀ {i l} (h : Heap l) →
  2 + h .size ≤ l →
  [ i ] ⟦ bounded₂ ⟧ h ≈ never
bounded₂-loop {i} {l} h 2+h≤l
  with grow h | grow-not-full h (<→≤ 2+h≤l)
... | .(just h′) | h′ , refl , refl = later λ { .force → lemma }
  where
  lemma : [ i ] ⟦ force (tail bounded₂) ⟧ h′ ≈ never
  lemma with grow h′ | grow-not-full h′ 2+h≤l
  lemma | .(just h″) | h″ , refl , refl =
    later λ { .force →
    later λ { .force →
    later λ { .force →
    bounded₂-loop _ 2+h≤l }}}

-- The program unbounded crashes for all heaps.

unbounded-crash :
  ∀ {i l} (h : Heap l) → [ i ] ⟦ unbounded ⟧ h ≈ crash
unbounded-crash {l = l} h = helper h (≤→≤↑ (h .bound))
  where
  helper :
    ∀ {i} (h′ : Heap l) → size h′ ≤↑ l →
    [ i ] ⟦ unbounded ⟧ h′ ≈ crash
  helper h′ (≤↑-refl h′≡l)
    rewrite grow-full h′ h′≡l =
    now
  helper h′ (≤↑-step 1+h′≤l)
    with grow h′ | grow-not-full h′ (≤↑→≤ 1+h′≤l)
  ... | .(just h″) | h″ , refl , refl =
    laterˡ (helper h″ 1+h′≤l)

-- The programs bounded and bounded₂ are ≃-equivalent.

bounded≃bounded₂ : [ ∞ ] bounded ≃ bounded₂
bounded≃bounded₂ =
  2 , λ l h 2+h≤l →
    ⟦ bounded ⟧ h   ≈⟨ bounded-loop _ (<→≤ 2+h≤l) ⟩
    never           ≈⟨ B.symmetric (bounded₂-loop _ 2+h≤l) ⟩∎
    ⟦ bounded₂ ⟧ h  ∎

-- The programs bounded and unbounded are not ≃-equivalent.

¬bounded≃unbounded :
  ¬ [ ∞ ] bounded ≃ unbounded
¬bounded≃unbounded (c , c≈u) = now≉never (
  crash            ≈⟨ B.symmetric (unbounded-crash h) ⟩
  ⟦ unbounded ⟧ h  ≈⟨ B.symmetric (c≈u _ h (≤-refl +-mono zero≤ _)) ⟩
  ⟦ bounded ⟧ h    ≈⟨ bounded-loop h (m≤n+m _ _) ⟩∎
  never            ∎)
  where
  h : Heap (c + 1)
  h = record
    { size  = 0
    ; bound = zero≤ _
    }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
open import Coinduction using ( ♯_ ; ♭ )
open import Data.Strict using ( Strict ; ! )
open import Data.Natural using ( Natural ; # ; _+_ )
open import Data.Bool using ( Bool ; true ; false )
open import System.IO.Transducers.Session using ( I ; Σ ; ⟨_⟩ ; * ; _&*_ ; ¿ )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done )
open import System.IO.Transducers.Strict using ( _⇛_ )

module System.IO.Transducers.List where

-- Length of a list

length' : ∀ {T S} → (Strict Natural) → (T &* S) ⇛ ⟨ Natural ⟩
length' {I}     {S} (! n) true  = inp (♯ length' {S} {S} (! (n + # 1)))
length' {I}     {S} (! n) false = out n done
length' {Σ V G} {S} (! n) b     = inp (♯ length' {♭ G b} {S} (! n))

length : ∀ {S} → (* S) ⇛ ⟨ Natural ⟩
length {S} = length' {I} {S} (! (# 0))

-- Flatten a list of lists

mutual

  concat' : ∀ {T S} → ((T &* S) &* * S) ⇛ (T &* S)
  concat' {I}     {S} true  = out true (inp (♯ concat' {S} {S}))
  concat' {I}     {S} false = inp (♯ concat {S})
  concat' {Σ W G} {S} a     = out a (inp (♯ concat' {♭ G a} {S}))

  concat : ∀ {S} → (* (* S)) ⇛ (* S)
  concat {S} true  = inp (♯ concat' {I} {S})
  concat {S} false = out false done

-- Some inclusions, which coerce traces from one session to another.

-- TODO: Add more inclusions.
-- TODO: Prove that these are monomorphisms.
-- TODO: It would be nice if inclusions like this could be handled by subtyping.

S⊆S&*T : ∀ {S T} → S ⇒ S &* T
S⊆S&*T {I}     = out false done
S⊆S&*T {Σ V F} = inp (♯ λ a → out a S⊆S&*T)

S⊆*S : ∀ {S} → S ⇒ * S
S⊆*S = out true S⊆S&*T

¿S⊆*S : ∀ {S} → ¿ S ⇛ * S
¿S⊆*S {S} true  = out true (S⊆S&*T {S} {S})
¿S⊆*S {S} false = out false done

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

open import Categories.Category using (Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Category.Monoidal.Reasoning {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Data.Product using (_,_)

open import Categories.Functor renaming (id to idF)

private
  module C = Category C

open C hiding (id; identityˡ; identityʳ; assoc)

private
  variable
    X Y : Obj
    f g h i : X ⇒ Y

open Monoidal M using (_⊗₁_; ⊗)
open Functor ⊗ using (F-resp-≈; homomorphism)
open HomReasoning public

infixr 6 _⟩⊗⟨_ refl⟩⊗⟨_
infixl 7 _⟩⊗⟨refl

⊗-resp-≈ : f ≈ h → g ≈ i → (f ⊗₁ g) ≈ (h ⊗₁ i)
⊗-resp-≈ p q = F-resp-≈ (p , q)

⊗-resp-≈ˡ : f ≈ h → (f ⊗₁ g) ≈ (h ⊗₁ g)
⊗-resp-≈ˡ p = ⊗-resp-≈ p Equiv.refl

⊗-resp-≈ʳ : g ≈ i → (f ⊗₁ g) ≈ (f ⊗₁ i)
⊗-resp-≈ʳ p = ⊗-resp-≈ Equiv.refl p

_⟩⊗⟨_ : f ≈ h → g ≈ i → (f ⊗₁ g) ≈ (h ⊗₁ i)
_⟩⊗⟨_ = ⊗-resp-≈

refl⟩⊗⟨_ : g ≈ i → (f ⊗₁ g) ≈ (f ⊗₁ i)
refl⟩⊗⟨_ = ⊗-resp-≈ʳ

_⟩⊗⟨refl : f ≈ h → (f ⊗₁ g) ≈ (h ⊗₁ g)
_⟩⊗⟨refl = ⊗-resp-≈ˡ

-- removing the {_} makes the whole thing not type check anymore for some reason
-- an issue was raised on the main agda GitHub repository about this
-- (https://github.com/agda/agda/issues/4140)
-- if this is fixed feel free to remove the {_}
⊗-distrib-over-∘ : ((f ∘ h) ⊗₁ (g ∘ i)) ≈ ((f ⊗₁ g) ∘ (h ⊗₁ i))
⊗-distrib-over-∘ {_} = homomorphism
  -- This also corresponds with the graphical coherence property of diagrams modelling monoidal categories:
--   |        |         |   |
--  [h]      [i]       [h] [i]
--   |        |    ≈    |   |
--  [f]      [g]        |   |
--   |        |         |   |
--                     [f] [g]
--                      |   |

-- Parallel-to-serial conversions
--
--   |   |        |   |       |   |
--   |   |        |  [g]     [f]  |
--  [f] [g]   =   |   |   =   |   |
--   |   |       [f]  |       |  [g]
--   |   |        |   |       |   |

serialize₁₂ : ∀ {X₁ Y₁ X₂ Y₂} {f : X₁ ⇒ Y₁} {g : X₂ ⇒ Y₂} →
              f ⊗₁ g ≈ f ⊗₁ C.id ∘ C.id ⊗₁ g
serialize₁₂ {f = f} {g} = begin
  f ⊗₁ g                     ≈˘⟨ C.identityʳ ⟩⊗⟨ C.identityˡ ⟩
  (f ∘ C.id) ⊗₁ (C.id ∘ g)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ C.id ∘ C.id ⊗₁ g      ∎

serialize₂₁ : ∀ {X₁ Y₁ X₂ Y₂} {f : X₁ ⇒ Y₁} {g : X₂ ⇒ Y₂} →
              f ⊗₁ g ≈ C.id ⊗₁ g ∘ f ⊗₁ C.id
serialize₂₁ {f = f} {g} = begin
  f ⊗₁ g                     ≈˘⟨ C.identityˡ ⟩⊗⟨ C.identityʳ ⟩
  (C.id ∘ f) ⊗₁ (g ∘ C.id)   ≈⟨ ⊗-distrib-over-∘ ⟩
  C.id ⊗₁ g ∘ f ⊗₁ C.id      ∎

-- Split a composite in the first component
--
--   |   |        |   |       |   |
--  [g]  |       [g]  |      [g] [h]
--   |  [h]   =   |   |   =   |   |
--  [f]  |       [f] [h]     [f]  |
--   |   |        |   |       |   |

split₁ʳ : ∀ {X₁ Y₁ Z₁ X₂ Y₂} {f : Y₁ ⇒ Z₁} {g : X₁ ⇒ Y₁} {h : X₂ ⇒ Y₂} →
          (f ∘ g) ⊗₁ h ≈ f ⊗₁ h ∘ g ⊗₁ C.id
split₁ʳ {f = f} {g} {h} = begin
  (f ∘ g) ⊗₁ h            ≈˘⟨ refl⟩⊗⟨ C.identityʳ ⟩
  (f ∘ g) ⊗₁ (h ∘ C.id)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ h ∘ g ⊗₁ C.id      ∎

split₁ˡ : ∀ {X₁ Y₁ Z₁ X₂ Y₂} {f : Y₁ ⇒ Z₁} {g : X₁ ⇒ Y₁} {h : X₂ ⇒ Y₂} →
          (f ∘ g) ⊗₁ h ≈ f ⊗₁ C.id ∘ g ⊗₁ h
split₁ˡ {f = f} {g} {h} = begin
  (f ∘ g) ⊗₁ h            ≈˘⟨ refl⟩⊗⟨ C.identityˡ ⟩
  (f ∘ g) ⊗₁ (C.id ∘ h)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ C.id ∘ g ⊗₁ h      ∎

-- Split a composite in the second component
--
--   |   |        |   |       |   |
--   |  [h]       |  [h]     [f] [h]
--  [f]  |    =   |   |   =   |   |
--   |  [g]      [f] [g]      |  [g]
--   |   |        |   |       |   |

split₂ʳ : ∀ {X₁ Y₁ X₂ Y₂ Z₂} {f : X₁ ⇒ Y₁} {g : Y₂ ⇒ Z₂} {h : X₂ ⇒ Y₂} →
          f ⊗₁ (g ∘ h) ≈ f ⊗₁ g ∘ C.id ⊗₁ h
split₂ʳ {f = f} {g} {h} = begin
  f ⊗₁ (g ∘ h)            ≈˘⟨ C.identityʳ ⟩⊗⟨refl ⟩
  (f ∘ C.id) ⊗₁ (g ∘ h)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ g ∘ C.id ⊗₁ h      ∎

split₂ˡ : ∀ {X₁ Y₁ X₂ Y₂ Z₂} {f : X₁ ⇒ Y₁} {g : Y₂ ⇒ Z₂} {h : X₂ ⇒ Y₂} →
          f ⊗₁ (g ∘ h) ≈ C.id ⊗₁ g ∘ f ⊗₁ h
split₂ˡ {f = f} {g} {h} = begin
  f ⊗₁ (g ∘ h)            ≈˘⟨ C.identityˡ ⟩⊗⟨refl ⟩
  (C.id ∘ f) ⊗₁ (g ∘ h)   ≈⟨ ⊗-distrib-over-∘ ⟩
  C.id ⊗₁ g ∘ f ⊗₁ h      ∎

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- Export only the experiments that are expected to compile (without
-- any holes)
{-# OPTIONS --cubical #-}
module Cubical.Experiments.Everything where

open import Cubical.Experiments.Brunerie public
open import Cubical.Experiments.Generic public
open import Cubical.Experiments.Problem
open import Cubical.Experiments.FunExtFromUA public

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
-- Andreas, 2017-09-16, issue #2759
-- Allow empty declaration blocks in the parser.

open import Agda.Builtin.Nat

x0 = zero
mutual
x1 = suc x0
abstract
x2 = suc x1
private
x3 = suc x2
instance
x4 = suc x3
macro
x5 = suc x4
postulate
x6 = suc x5

-- Expected: 6 warnings about empty blocks

mutual
  postulate

-- Empty postulate block.

abstract private instance macro

-- Empty macro block.

-- Empty blocks are also tolerated in lets and lambdas.

_ = λ (let abstract ) → let abstract  in Set
_ = λ (let field    ) → let field     in Set
_ = λ (let instance ) → let instance  in Set
_ = λ (let macro    ) → let macro     in Set
_ = λ (let mutual   ) → let mutual    in Set
_ = λ (let postulate) → let postulate in Set
_ = λ (let private  ) → let private   in Set


text:
module plfa-code.Reasoning-legacy where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans)

infixr 2 _≡⟨_⟩_
infix  3 _∎

_≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A}
  → x ≡ y
  → y ≡ z
    -------
  → x ≡ z
x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

_∎ : ∀ {A : Set} (x : A)
    ------
  → x ≡ x
x ∎  = refl

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
module Oscar.Property.Symmetry where

open import Oscar.Level

record Symmetry {𝔬} {⋆ : Set 𝔬} {𝔮} (_≒_ : ⋆ → ⋆ → Set 𝔮) : Set (𝔬 ⊔ 𝔮) where
  field
    symmetry : ∀ {x y} → x ≒ y → y ≒ x

open Symmetry ⦃ … ⦄ public


text:
-- Reported by Christian Sattler on 2019-12-7

postulate
  A B : Set

barb : Set
barb = (A → (_ : B) → _) _

-- WAS: unsolved constraints.
-- SHOULD: throw an error that A → ... is not a function.


text:
{-# OPTIONS --type-in-type #-}

data IBool : Set where
  itrue ifalse : IBool

Bool : Set; Bool
 = (B : Set) → B → B → B

toIBool : Bool → IBool
toIBool b = b _ itrue ifalse

true : Bool; true
 = λ B t f → t

and : Bool → Bool → Bool; and
 = λ a b B t f → a B (b B t f) f

Nat : Set; Nat
 = (n : Set) → (n → n) → n → n

add : Nat → Nat → Nat; add
 = λ a b n s z → a n s (b n s z)

mul : Nat → Nat → Nat; mul
 = λ a b n s → a n (b n s)

suc : Nat → Nat; suc
 = λ a n s z → s (a n s z)

Eq : {A : Set} → A → A → Set
Eq {A} x y = (P : A → Set) → P x → P y

refl : {A : Set}{x : A} → Eq {A} x x; refl
 = λ P px → px

n2  : Nat; n2 = λ N s z → s (s z)
n3  : Nat; n3 = λ N s z → s (s (s z))
n4  : Nat; n4 = λ N s z → s (s (s (s z)))
n5  : Nat; n5 = λ N s z → s (s (s (s (s z))))
n10    = mul n2 n5
n10b   = mul n5 n2
n15    = add n10  n5
n15b   = add n10b n5
n18    = add n15  n3
n18b   = add n15b n3
n19    = add n15  n4
n19b   = add n15b n4
n20    = mul n2 n10
n20b   = mul n2 n10b
n21    = suc n20
n21b   = suc n20b
n22    = suc n21
n22b   = suc n21b
n23    = suc n22
n23b   = suc n22b
n100   = mul n10   n10
n100b  = mul n10b  n10b
n10k   = mul n100  n100
n10kb  = mul n100b n100b
n100k  = mul n10k  n10
n100kb = mul n10kb n10b
n1M    = mul n10k  n100
n1Mb   = mul n10kb n100b
n5M    = mul n1M   n5
n5Mb   = mul n1Mb  n5
n10M   = mul n5M   n2
n10Mb  = mul n5Mb  n2

Tree : Set; Tree = (T : Set) → (T → T → T) → T → T
leaf : Tree; leaf = λ T n l → l
node : Tree → Tree → Tree; node = λ t1 t2 T n l → n (t1 T n l) (t2 T n l)

fullTree : Nat → Tree; fullTree
 = λ n → n Tree (λ t → node t t) leaf

-- full tree with given trees at bottom level
fullTreeWithLeaf : Tree → Nat → Tree; fullTreeWithLeaf
 = λ bottom n → n Tree (λ t → node t t) bottom

forceTree : Tree → Bool; forceTree
 = λ t → t Bool and true

t15  = fullTree n15
t15b = fullTree n15b
t18  = fullTree n18
t18b = fullTree n18b
t19  = fullTree n19
t19b = fullTree n19b
t20  = fullTree n20
t20b = fullTree n20b
t21  = fullTree n21
t21b = fullTree n21b
t22  = fullTree n22
t22b = fullTree n22b
t23  = fullTree n23
t23b = fullTree n23b

-- Nat conversion
--------------------------------------------------------------------------------

-- convn1M : Eq n1M n1Mb; convn1M = refl
-- convn5M : Eq n5M n5Mb; convn5M = refl
-- convn10M : Eq n10M n10Mb; convn10M = refl

-- Full tree conversion
--------------------------------------------------------------------------------

-- convt15  : Eq t15  t15b; convt15  = refl -- 16 ms
-- convt18  : Eq t18  t18b; convt18  = refl -- 20 ms
-- convt19  : Eq t19  t19b; convt19  = refl -- 30 ms
-- convt20  : Eq t20  t20b; convt20  = refl -- 1.7 s
-- convt21  : Eq t21  t21b; convt21  = refl -- 3.4 s
-- convt22  : Eq t22  t22b; convt22  = refl -- 6.6 s
-- convt23  : Eq t23  t23b; convt23  = refl -- 13.1 s

-- Full meta-containing tree conversion
--------------------------------------------------------------------------------

-- convmt15 : Eq t15b  (fullTreeWithLeaf _ n15 ); convmt15 = refl --
-- convmt18 : Eq t18b  (fullTreeWithLeaf _ n18 ); convmt18 = refl --
-- convmt19 : Eq t19b  (fullTreeWithLeaf _ n19 ); convmt19 = refl --
-- convmt20 : Eq t20b  (fullTreeWithLeaf _ n20 ); convmt20 = refl --
-- convmt21 : Eq t21b  (fullTreeWithLeaf _ n21 ); convmt21 = refl
-- convmt22 : Eq t22b  (fullTreeWithLeaf _ n22 ); convmt22 = refl
-- convmt23 : Eq t23b  (fullTreeWithLeaf _ n23 ); convmt23 = refl

-- Full tree forcing
--------------------------------------------------------------------------------

-- forcet15 : Eq (toIBool (forceTree t15)) itrue; forcet15 = refl -- 50 ms
-- forcet18 : Eq (toIBool (forceTree t18)) itrue; forcet18 = refl -- 450 ms
-- forcet19 : Eq (toIBool (forceTree t19)) itrue; forcet19 = refl -- 900 ms
-- forcet20 : Eq (toIBool (forceTree t20)) itrue; forcet20 = refl -- 1.75 s
-- forcet21 : Eq (toIBool (forceTree t21)) itrue; forcet21 = refl -- 3.5 s
-- forcet22 : Eq (toIBool (forceTree t22)) itrue; forcet22 = refl -- 7.5 s
-- forcet23 : Eq (toIBool (forceTree t23)) itrue; forcet23 = refl -- 15 s

max_stars_repo_name: int-index/smalltt

max_issues_repo_name: int-index/smalltt

max_forks_repo_name: int-index/smalltt


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

module Data.Binary.Proofs where

open import Data.Binary.Proofs.Multiplication using (*-homo)
open import Data.Binary.Proofs.Addition       using (+-homo)
open import Data.Binary.Proofs.Unary          using (inc-homo)
open import Data.Binary.Proofs.Bijection      using (𝔹↔ℕ)

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Sets.FinSet
open import Groups.Groups
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Setoids.Functions.Extension
open import Groups.SymmetricGroups.Definition

module Groups.SymmetricGroups.Finite.Definition where

snSet : (n : ℕ) → Set
snSet n = SymmetryGroupElements (reflSetoid (FinSet n))

snSetoid : (n : ℕ) → Setoid (snSet n)
snSetoid n = symmetricSetoid (reflSetoid (FinSet n))

SymmetricGroupN : (n : ℕ) → Group (snSetoid n) (symmetricGroupOp)
SymmetricGroupN n = symmetricGroup (reflSetoid (FinSet n))

record Cycles {n : ℕ} (s : snSet n) : Set where
  field

cycles : {n : ℕ} → (s : snSet n) → Cycles s
cycles s = {!!}


text:
open import SOAS.Common
import SOAS.Families.Core

-- Families with syntactic structure
module SOAS.Metatheory.MetaAlgebra {T : Set}
  (open SOAS.Families.Core {T})
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ)
  (𝔛 : Familyₛ) where

open import SOAS.Context {T}
open import SOAS.Variable {T}
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted

open import SOAS.Metatheory.Algebra ⅀F

private
  variable
    Γ Δ Π : Ctx
    α : T

-- A family with support for variables, metavariables, and ⅀-algebra structure
record MetaAlg (𝒜 : Familyₛ) : Set where

  field
    𝑎𝑙𝑔  : ⅀ 𝒜 ⇾̣ 𝒜
    𝑣𝑎𝑟  :   ℐ ⇾̣ 𝒜
    𝑚𝑣𝑎𝑟 :   𝔛 ⇾̣ 〖 𝒜 , 𝒜 〗

  -- Congruence in metavariable arguments
  𝑚≈₁ : {𝔪₁ 𝔪₂ : 𝔛 α Π}{σ : Π ~[ 𝒜 ]↝ Γ}
      → 𝔪₁ ≡ 𝔪₂
      → 𝑚𝑣𝑎𝑟 𝔪₁ σ ≡ 𝑚𝑣𝑎𝑟 𝔪₂ σ
  𝑚≈₁ refl = refl

  𝑚≈₂ : {𝔪 : 𝔛 α Π}{σ ς : Π ~[ 𝒜 ]↝ Γ}
      → ({τ : T}(v : ℐ τ Π) → σ v ≡ ς v)
      → 𝑚𝑣𝑎𝑟 𝔪 σ ≡ 𝑚𝑣𝑎𝑟 𝔪 ς
  𝑚≈₂ {𝔪 = 𝔪} p = cong (𝑚𝑣𝑎𝑟 𝔪) (dext p)

-- Meta-algebra homomorphism
record MetaAlg⇒ {𝒜 ℬ : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜)(ℬᵃ : MetaAlg ℬ)
                (f : 𝒜 ⇾̣ ℬ) : Set where
  private module 𝒜 = MetaAlg 𝒜ᵃ
  private module ℬ = MetaAlg ℬᵃ

  field
    ⟨𝑎𝑙𝑔⟩  : {t : ⅀ 𝒜 α Γ} → f (𝒜.𝑎𝑙𝑔 t) ≡ ℬ.𝑎𝑙𝑔 (⅀₁ f t)
    ⟨𝑣𝑎𝑟⟩  : {v : ℐ α Γ} → f (𝒜.𝑣𝑎𝑟 v) ≡ ℬ.𝑣𝑎𝑟 v
    ⟨𝑚𝑣𝑎𝑟⟩ : {𝔪 : 𝔛 α Π}{ε : Π ~[ 𝒜 ]↝ Γ} → f (𝒜.𝑚𝑣𝑎𝑟 𝔪 ε) ≡ ℬ.𝑚𝑣𝑎𝑟 𝔪 (f ∘ ε)

-- Category of meta-algebras
module MetaAlgebraStructure = Structure 𝔽amiliesₛ MetaAlg

MetaAlgebraCatProps : MetaAlgebraStructure.CategoryProps
MetaAlgebraCatProps = record
  { IsHomomorphism = MetaAlg⇒
  ; id-hom = λ {𝒜}{𝒜ᵃ} → record
    { ⟨𝑎𝑙𝑔⟩ = cong (𝑎𝑙𝑔 𝒜ᵃ) (sym ⅀.identity)
    ; ⟨𝑣𝑎𝑟⟩ = refl
    ; ⟨𝑚𝑣𝑎𝑟⟩ = refl }
  ; comp-hom = λ{ {𝐶ˢ = 𝒜ᵃ}{ℬᵃ}{𝒞ᵃ} g f gᵃ⇒ fᵃ⇒ → record
    { ⟨𝑎𝑙𝑔⟩ = trans (cong g (⟨𝑎𝑙𝑔⟩ fᵃ⇒))
            (trans (⟨𝑎𝑙𝑔⟩  gᵃ⇒)
                    (cong (𝑎𝑙𝑔 𝒞ᵃ) (sym ⅀.homomorphism)))
    ; ⟨𝑣𝑎𝑟⟩ = trans (cong g (⟨𝑣𝑎𝑟⟩ fᵃ⇒)) (⟨𝑣𝑎𝑟⟩ gᵃ⇒)
    ; ⟨𝑚𝑣𝑎𝑟⟩ = trans (cong g (⟨𝑚𝑣𝑎𝑟⟩ fᵃ⇒)) (⟨𝑚𝑣𝑎𝑟⟩ gᵃ⇒) }
  }} where open MetaAlg ; open MetaAlg⇒

module MetaAlgProps = MetaAlgebraStructure.CategoryProps MetaAlgebraCatProps

𝕄etaAlgebras : Category 1ℓ 0ℓ 0ℓ
𝕄etaAlgebras = MetaAlgebraStructure.StructCat MetaAlgebraCatProps

module 𝕄etaAlg = Category 𝕄etaAlgebras

MetaAlgebra : Set₁
MetaAlgebra = 𝕄etaAlg.Obj

MetaAlgebra⇒ : MetaAlgebra → MetaAlgebra → Set
MetaAlgebra⇒ = 𝕄etaAlg._⇒_

-- Identity is a meta-algebra homomorphism
idᵃ : {𝒜 : Familyₛ} → (𝒜ᵃ : MetaAlg 𝒜) → MetaAlg⇒ 𝒜ᵃ 𝒜ᵃ id
idᵃ 𝒜ᵃ = record { ⟨𝑎𝑙𝑔⟩ = cong (MetaAlg.𝑎𝑙𝑔 𝒜ᵃ) (sym ⅀.identity)
                ; ⟨𝑣𝑎𝑟⟩ = refl ; ⟨𝑚𝑣𝑎𝑟⟩ = refl }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

module Definition.Typed.Weakening where

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed

import Tools.PropositionalEquality as PE

-- Weakening type

data _∷_⊆_ : Wk → Con Term → Con Term → Set where
  id   : ∀ {Γ}       → id ∷ Γ ⊆ Γ
  step : ∀ {Γ Δ A ρ} → ρ  ∷ Δ ⊆ Γ → step ρ ∷ Δ ∙ A        ⊆ Γ
  lift : ∀ {Γ Δ A ρ} → ρ  ∷ Δ ⊆ Γ → lift ρ ∷ Δ ∙ U.wk ρ A ⊆ Γ ∙ A

-- -- Weakening composition

_•ₜ_ : ∀ {ρ ρ′ Γ Δ Δ′} → ρ ∷ Γ ⊆ Δ → ρ′ ∷ Δ ⊆ Δ′ → ρ • ρ′ ∷ Γ ⊆ Δ′
id     •ₜ η′ = η′
step η •ₜ η′ = step (η •ₜ η′)
lift η •ₜ id = lift η
lift η •ₜ step η′ = step (η •ₜ η′)
_•ₜ_ {lift ρ} {lift ρ′} {Δ′ = Δ′ ∙ A} (lift η) (lift η′) =
  PE.subst (λ x → lift (ρ • ρ′) ∷ x ⊆ Δ′ ∙ A)
           (PE.cong₂ _∙_ PE.refl (PE.sym (wk-comp ρ ρ′ A)))
           (lift (η •ₜ η′))

-- Weakening of judgements

wkIndex : ∀ {Γ Δ n A ρ} → ρ ∷ Δ ⊆ Γ →
        let ρA = U.wk ρ A
            ρn = wkVar ρ n
        in  ⊢ Δ → n ∷ A ∈ Γ → ρn ∷ ρA ∈ Δ
wkIndex id ⊢Δ i = PE.subst (λ x → _ ∷ x ∈ _) (PE.sym (wk-id _)) i
wkIndex (step ρ) (⊢Δ ∙ A) i = PE.subst (λ x → _ ∷ x ∈ _)
                                       (wk1-wk _ _)
                                       (there (wkIndex ρ ⊢Δ i))
wkIndex (lift ρ) (⊢Δ ∙ A) (there i) = PE.subst (λ x → _ ∷ x ∈ _)
                                               (wk1-wk≡lift-wk1 _ _)
                                               (there (wkIndex ρ ⊢Δ i))
wkIndex (lift ρ) ⊢Δ here =
  let G = _
      n = _
  in  PE.subst (λ x → n ∷ x ∈ G)
               (wk1-wk≡lift-wk1 _ _)
               here

mutual
  wk : ∀ {Γ Δ A ρ} → ρ ∷ Δ ⊆ Γ →
     let ρA = U.wk ρ A
     in  ⊢ Δ → Γ ⊢ A → Δ ⊢ ρA
  wk ρ ⊢Δ (ℕⱼ ⊢Γ) = ℕⱼ ⊢Δ
  wk ρ ⊢Δ (Uⱼ ⊢Γ) = Uⱼ ⊢Δ
  wk ρ ⊢Δ (Πⱼ F ▹ G) = let ρF = wk ρ ⊢Δ F
                       in  Πⱼ ρF ▹ (wk (lift ρ) (⊢Δ ∙ ρF) G)
  wk ρ ⊢Δ (univ A) = univ (wkTerm ρ ⊢Δ A)

  wkTerm : ∀ {Γ Δ A t ρ} → ρ ∷ Δ ⊆ Γ →
         let ρA = U.wk ρ A
             ρt = U.wk ρ t
         in ⊢ Δ → Γ ⊢ t ∷ A → Δ ⊢ ρt ∷ ρA
  wkTerm ρ ⊢Δ (ℕⱼ ⊢Γ) = ℕⱼ ⊢Δ
  wkTerm ρ ⊢Δ (Πⱼ F ▹ G) = let ρF = wkTerm ρ ⊢Δ F
                          in  Πⱼ ρF ▹ (wkTerm (lift ρ) (⊢Δ ∙ univ ρF) G)
  wkTerm ρ ⊢Δ (var ⊢Γ x) = var ⊢Δ (wkIndex ρ ⊢Δ x)
  wkTerm ρ ⊢Δ (lamⱼ F t) = let ρF = wk ρ ⊢Δ F
                          in lamⱼ ρF (wkTerm (lift ρ) (⊢Δ ∙ ρF) t)
  wkTerm ρ ⊢Δ (_∘ⱼ_ {G = G} g a) = PE.subst (λ x → _ ⊢ _ ∷ x)
                                           (PE.sym (wk-β G))
                                           (wkTerm ρ ⊢Δ g ∘ⱼ wkTerm ρ ⊢Δ a)
  wkTerm ρ ⊢Δ (zeroⱼ ⊢Γ) = zeroⱼ ⊢Δ
  wkTerm ρ ⊢Δ (sucⱼ n) = sucⱼ (wkTerm ρ ⊢Δ n)
  wkTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrecⱼ {G = G} {s = s} ⊢G ⊢z ⊢s ⊢n) =
    PE.subst (λ x → _ ⊢ natrec _ _ _ _ ∷ x) (PE.sym (wk-β G))
             (natrecⱼ (wk (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) ⊢G)
                      (PE.subst (λ x → _ ⊢ _ ∷ x) (wk-β G) (wkTerm [ρ] ⊢Δ ⊢z))
                      (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x)
                                (wk-β-natrec ρ G)
                                (wkTerm [ρ] ⊢Δ ⊢s))
                      (wkTerm [ρ] ⊢Δ ⊢n))
  wkTerm ρ ⊢Δ (conv t A≡B) = conv (wkTerm ρ ⊢Δ t) (wkEq ρ ⊢Δ A≡B)

  wkEq : ∀ {Γ Δ A B ρ} → ρ ∷ Δ ⊆ Γ →
       let ρA = U.wk ρ A
           ρB = U.wk ρ B
       in ⊢ Δ → Γ ⊢ A ≡ B → Δ ⊢ ρA ≡ ρB
  wkEq ρ ⊢Δ (univ A≡B) = univ (wkEqTerm ρ ⊢Δ A≡B)
  wkEq ρ ⊢Δ (refl A) = refl (wk ρ ⊢Δ A)
  wkEq ρ ⊢Δ (sym A≡B) = sym (wkEq ρ ⊢Δ A≡B)
  wkEq ρ ⊢Δ (trans A≡B B≡C) = trans (wkEq ρ ⊢Δ A≡B) (wkEq ρ ⊢Δ B≡C)
  wkEq ρ ⊢Δ (Π-cong F F≡H G≡E) = let ρF = wk ρ ⊢Δ F
                                 in  Π-cong ρF (wkEq ρ ⊢Δ F≡H)
                                               (wkEq (lift ρ) (⊢Δ ∙ ρF) G≡E)

  wkEqTerm : ∀ {Γ Δ A t u ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρt = U.wk ρ t
               ρu = U.wk ρ u
           in ⊢ Δ → Γ ⊢ t ≡ u ∷ A → Δ ⊢ ρt ≡ ρu ∷ ρA
  wkEqTerm ρ ⊢Δ (refl t) = refl (wkTerm ρ ⊢Δ t)
  wkEqTerm ρ ⊢Δ (sym t≡u) = sym (wkEqTerm ρ ⊢Δ t≡u)
  wkEqTerm ρ ⊢Δ (trans t≡u u≡r) = trans (wkEqTerm ρ ⊢Δ t≡u) (wkEqTerm ρ ⊢Δ u≡r)
  wkEqTerm ρ ⊢Δ (conv t≡u A≡B) = conv (wkEqTerm ρ ⊢Δ t≡u) (wkEq ρ ⊢Δ A≡B)
  wkEqTerm ρ ⊢Δ (Π-cong F F≡H G≡E) =
    let ρF = wk ρ ⊢Δ F
    in  Π-cong ρF (wkEqTerm ρ ⊢Δ F≡H)
                  (wkEqTerm (lift ρ) (⊢Δ ∙ ρF) G≡E)
  wkEqTerm ρ ⊢Δ (app-cong {G = G} f≡g a≡b) =
    PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x)
             (PE.sym (wk-β G))
             (app-cong (wkEqTerm ρ ⊢Δ f≡g) (wkEqTerm ρ ⊢Δ a≡b))
  wkEqTerm ρ ⊢Δ (β-red {a = a} {t = t} {G = G} F ⊢t ⊢a) =
    let ρF = wk ρ ⊢Δ F
    in  PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x)
                 (PE.sym (wk-β G))
                 (PE.subst (λ x → _ ⊢ U.wk _ ((lam t) ∘ a) ≡ x ∷ _)
                           (PE.sym (wk-β t))
                           (β-red ρF (wkTerm (lift ρ) (⊢Δ ∙ ρF) ⊢t)
                                     (wkTerm ρ ⊢Δ ⊢a)))
  wkEqTerm ρ ⊢Δ (η-eq F f g f0≡g0) =
    let ρF = wk ρ ⊢Δ F
    in  η-eq ρF (wkTerm ρ ⊢Δ f)
                (wkTerm ρ ⊢Δ g)
                (PE.subst (λ t → _ ⊢ t ∘ _ ≡ _ ∷ _)
                          (PE.sym (wk1-wk≡lift-wk1 _ _))
                          (PE.subst (λ t → _ ⊢ _ ≡ t ∘ _ ∷ _)
                                    (PE.sym (wk1-wk≡lift-wk1 _ _))
                                    (wkEqTerm (lift ρ) (⊢Δ ∙ ρF) f0≡g0)))
  wkEqTerm ρ ⊢Δ (suc-cong m≡n) = suc-cong (wkEqTerm ρ ⊢Δ m≡n)
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-cong {s = s} {s′ = s′} {F = F}
                                     F≡F′ z≡z′ s≡s′ n≡n′) =
    PE.subst (λ x → Δ ⊢ natrec _ _ _ _ ≡ _ ∷ x) (PE.sym (wk-β F))
             (natrec-cong (wkEq (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) F≡F′)
                          (PE.subst (λ x → Δ ⊢ _ ≡ _ ∷ x) (wk-β F)
                                    (wkEqTerm [ρ] ⊢Δ z≡z′))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ s
                                             ≡ U.wk ρ s′ ∷ x)
                                    (wk-β-natrec _ F)
                                    (wkEqTerm [ρ] ⊢Δ s≡s′))
                          (wkEqTerm [ρ] ⊢Δ n≡n′))
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-zero {z} {s} {F} ⊢F ⊢z ⊢s) =
    PE.subst (λ x → Δ ⊢ natrec (U.wk (lift _) F) _ _ _ ≡ _ ∷ x)
             (PE.sym (wk-β F))
             (natrec-zero (wk (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) ⊢F)
                          (PE.subst (λ x → Δ ⊢ U.wk ρ z ∷ x)
                                    (wk-β F)
                                    (wkTerm [ρ] ⊢Δ ⊢z))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x)
                                    (wk-β-natrec _ F)
                                    (wkTerm [ρ] ⊢Δ ⊢s)))
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-suc {n} {z} {s} {F} ⊢n ⊢F ⊢z ⊢s) =
    PE.subst (λ x → Δ ⊢ natrec (U.wk (lift _) F) _ _ _
                      ≡ _ ∘ (natrec _ _ _ _) ∷ x)
             (PE.sym (wk-β F))
             (natrec-suc (wkTerm [ρ] ⊢Δ ⊢n)
                         (wk (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) ⊢F)
                         (PE.subst (λ x → Δ ⊢ U.wk ρ z ∷ x)
                                   (wk-β F)
                                   (wkTerm [ρ] ⊢Δ ⊢z))
                         (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x)
                                   (wk-β-natrec _ F)
                                   (wkTerm [ρ] ⊢Δ ⊢s)))

mutual
  wkRed : ∀ {Γ Δ A B ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρB = U.wk ρ B
           in ⊢ Δ → Γ ⊢ A ⇒ B → Δ ⊢ ρA ⇒ ρB
  wkRed ρ ⊢Δ (univ A⇒B) = univ (wkRedTerm ρ ⊢Δ A⇒B)

  wkRedTerm : ∀ {Γ Δ A t u ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρt = U.wk ρ t
               ρu = U.wk ρ u
           in ⊢ Δ → Γ ⊢ t ⇒ u ∷ A → Δ ⊢ ρt ⇒ ρu ∷ ρA
  wkRedTerm ρ ⊢Δ (conv t⇒u A≡B) = conv (wkRedTerm ρ ⊢Δ t⇒u) (wkEq ρ ⊢Δ A≡B)
  wkRedTerm ρ ⊢Δ (app-subst {B = B} t⇒u a) =
    PE.subst (λ x → _ ⊢ _ ⇒ _ ∷ x) (PE.sym (wk-β B))
             (app-subst (wkRedTerm ρ ⊢Δ t⇒u) (wkTerm ρ ⊢Δ a))
  wkRedTerm ρ ⊢Δ (β-red {A} {B} {a} {t} ⊢A ⊢t ⊢a) =
    let ⊢ρA = wk ρ ⊢Δ ⊢A
    in  PE.subst (λ x → _ ⊢ _ ⇒ _ ∷ x) (PE.sym (wk-β B))
                 (PE.subst (λ x → _ ⊢ U.wk _ ((lam t) ∘ a) ⇒ x ∷ _)
                           (PE.sym (wk-β t))
                           (β-red ⊢ρA (wkTerm (lift ρ) (⊢Δ ∙ ⊢ρA) ⊢t)
                                      (wkTerm ρ ⊢Δ ⊢a)))
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-subst {s = s} {F = F} ⊢F ⊢z ⊢s n⇒n′) =
    PE.subst (λ x → _ ⊢ natrec _ _ _ _ ⇒ _ ∷ x) (PE.sym (wk-β F))
             (natrec-subst (wk (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) ⊢F)
                           (PE.subst (λ x → _ ⊢ _ ∷ x) (wk-β F)
                                     (wkTerm [ρ] ⊢Δ ⊢z))
                           (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x)
                                     (wk-β-natrec _ F)
                                     (wkTerm [ρ] ⊢Δ ⊢s))
                           (wkRedTerm [ρ] ⊢Δ n⇒n′))
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-zero {s = s} {F = F} ⊢F ⊢z ⊢s) =
    PE.subst (λ x → _ ⊢ natrec (U.wk (lift ρ) F) _ _ _ ⇒ _ ∷ x)
             (PE.sym (wk-β F))
             (natrec-zero (wk (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) ⊢F)
                          (PE.subst (λ x → _ ⊢ _ ∷ x)
                                    (wk-β F)
                                    (wkTerm [ρ] ⊢Δ ⊢z))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x)
                                    (wk-β-natrec ρ F)
                                    (wkTerm [ρ] ⊢Δ ⊢s)))
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-suc {s = s} {F = F} ⊢n ⊢F ⊢z ⊢s) =
    PE.subst (λ x → _ ⊢ natrec _ _ _ _ ⇒ _ ∘ natrec _ _ _ _ ∷ x)
             (PE.sym (wk-β F))
             (natrec-suc (wkTerm [ρ] ⊢Δ ⊢n)
                         (wk (lift [ρ]) (⊢Δ ∙ ℕⱼ ⊢Δ) ⊢F)
                         (PE.subst (λ x → _ ⊢ _ ∷ x)
                                   (wk-β F)
                                   (wkTerm [ρ] ⊢Δ ⊢z))
                         (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x)
                                   (wk-β-natrec ρ F)
                                   (wkTerm [ρ] ⊢Δ ⊢s)))

wkRed* : ∀ {Γ Δ A B ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρB = U.wk ρ B
           in ⊢ Δ → Γ ⊢ A ⇒* B → Δ ⊢ ρA ⇒* ρB
wkRed* ρ ⊢Δ (id A) = id (wk ρ ⊢Δ A)
wkRed* ρ ⊢Δ (A⇒A′ ⇨ A′⇒*B) = wkRed ρ ⊢Δ A⇒A′ ⇨ wkRed* ρ ⊢Δ A′⇒*B

wkRed*Term : ∀ {Γ Δ A t u ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρt = U.wk ρ t
               ρu = U.wk ρ u
           in ⊢ Δ → Γ ⊢ t ⇒* u ∷ A → Δ ⊢ ρt ⇒* ρu ∷ ρA
wkRed*Term ρ ⊢Δ (id t) = id (wkTerm ρ ⊢Δ t)
wkRed*Term ρ ⊢Δ (t⇒t′ ⇨ t′⇒*u) = wkRedTerm ρ ⊢Δ t⇒t′ ⇨ wkRed*Term ρ ⊢Δ t′⇒*u

wkRed:*: : ∀ {Γ Δ A B ρ} → ρ ∷ Δ ⊆ Γ →
         let ρA = U.wk ρ A
             ρB = U.wk ρ B
         in ⊢ Δ → Γ ⊢ A :⇒*: B → Δ ⊢ ρA :⇒*: ρB
wkRed:*: ρ ⊢Δ [ ⊢A , ⊢B , D ] = [ wk ρ ⊢Δ ⊢A , wk ρ ⊢Δ ⊢B , wkRed* ρ ⊢Δ D ]

wkRed:*:Term : ∀ {Γ Δ A t u ρ} → ρ ∷ Δ ⊆ Γ →
             let ρA = U.wk ρ A
                 ρt = U.wk ρ t
                 ρu = U.wk ρ u
             in ⊢ Δ → Γ ⊢ t :⇒*: u ∷ A → Δ ⊢ ρt :⇒*: ρu ∷ ρA
wkRed:*:Term ρ ⊢Δ [ ⊢t , ⊢u , d ] =
  [ wkTerm ρ ⊢Δ ⊢t , wkTerm ρ ⊢Δ ⊢u , wkRed*Term ρ ⊢Δ d ]

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Pi-.Examples where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L
open import Function using (_∘_)
open import Pi-.Syntax
open import Pi-.Opsem
open import Pi-.Eval

-----------------------------------------------------------------------------
-- Patterns and data definitions

pattern 𝔹 = 𝟙 +ᵤ 𝟙
pattern 𝔽 = inj₁ tt
pattern 𝕋 = inj₂ tt

𝔹+ : ℕ → 𝕌
𝔹+ 0 = 𝟘
𝔹+ 1 = 𝔹
𝔹+ (suc (suc n)) = 𝔹 +ᵤ (𝔹+ (suc n))

𝔹^ : ℕ → 𝕌
𝔹^ 0 = 𝟙
𝔹^ 1 = 𝔹
𝔹^ (suc (suc n)) = 𝔹 ×ᵤ 𝔹^ (suc n)

𝔹* : ℕ → 𝕌
𝔹* n = 𝔹^ (1 + n)

𝔽^ : (n : ℕ) → ⟦ 𝔹^ n ⟧
𝔽^ 0 = tt
𝔽^ 1 = 𝔽
𝔽^ (suc (suc n)) = 𝔽 , 𝔽^ (suc n)

-----------------------------------------------------------------------------
-- Adaptors

[A+B]+C=[C+B]+A : ∀ {A B C} → (A +ᵤ B) +ᵤ C ↔ (C +ᵤ B) +ᵤ A
[A+B]+C=[C+B]+A = assocr₊ ⨾ (id↔ ⊕ swap₊) ⨾ swap₊

[A+B]+C=[A+C]+B : ∀ {A B C} → (A +ᵤ B) +ᵤ C ↔ (A +ᵤ C) +ᵤ B
[A+B]+C=[A+C]+B = assocr₊ ⨾ (id↔ ⊕ swap₊) ⨾ assocl₊

[A+B]+[C+D]=[A+C]+[B+D] : {A B C D : 𝕌} → (A +ᵤ B) +ᵤ (C +ᵤ D) ↔ (A +ᵤ C) +ᵤ (B +ᵤ D)
[A+B]+[C+D]=[A+C]+[B+D] = assocl₊ ⨾ (assocr₊ ⊕ id↔) ⨾ ((id↔ ⊕ swap₊) ⊕ id↔) ⨾ (assocl₊ ⊕ id↔) ⨾ assocr₊

A+[B+C]=B+[A+C] : ∀ {A B C} → A +ᵤ (B +ᵤ C) ↔ B +ᵤ (A +ᵤ C)
A+[B+C]=B+[A+C] = assocl₊ ⨾ swap₊ ⊕ id↔ ⨾ assocr₊

Ax[BxC]=Bx[AxC] : {A B C : 𝕌} → A ×ᵤ (B ×ᵤ C) ↔ B ×ᵤ (A ×ᵤ C)
Ax[BxC]=Bx[AxC] = assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾  assocr⋆

[AxB]×C=[A×C]xB : ∀ {A B C} → (A ×ᵤ B) ×ᵤ C ↔ (A ×ᵤ C) ×ᵤ B
[AxB]×C=[A×C]xB = assocr⋆ ⨾ (id↔ ⊗ swap⋆) ⨾ assocl⋆

[A×B]×[C×D]=[A×C]×[B×D] : {A B C D : 𝕌} → (A ×ᵤ B) ×ᵤ (C ×ᵤ D) ↔ (A ×ᵤ C) ×ᵤ (B ×ᵤ D)
[A×B]×[C×D]=[A×C]×[B×D] = assocl⋆ ⨾ (assocr⋆ ⊗ id↔) ⨾ ((id↔ ⊗ swap⋆) ⊗ id↔) ⨾ (assocl⋆ ⊗ id↔) ⨾ assocr⋆

-- FST2LAST(b₁,b₂,…,bₙ) = (b₂,…,bₙ,b₁)
FST2LAST : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
FST2LAST {0} = id↔
FST2LAST {1} = id↔
FST2LAST {2} = swap⋆
FST2LAST {suc (suc (suc n))} = Ax[BxC]=Bx[AxC] ⨾ (id↔ ⊗ FST2LAST)

FST2LAST⁻¹ : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
FST2LAST⁻¹ = ! FST2LAST

-----------------------------------------------------------------------------
-- Reversible Conditionals

-- NOT(b) = ¬b
NOT : 𝔹 ↔ 𝔹
NOT = swap₊

-- CNOT(b₁,b₂) = (b₁,b₁ xor b₂)
CNOT : 𝔹 ×ᵤ 𝔹 ↔ 𝔹 ×ᵤ 𝔹
CNOT = dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor

-- CIF(c₁,c₂)(𝔽,a) = (𝔽,c₁ a)
-- CIF(c₁,c₂)(𝕋,a) = (𝕋,c₂ a)
CIF : {A : 𝕌} → (c₁ c₂ : A ↔ A) → 𝔹 ×ᵤ A ↔ 𝔹 ×ᵤ A
CIF c₁ c₂ = dist ⨾ ((id↔ ⊗ c₁) ⊕ (id↔ ⊗ c₂)) ⨾ factor

CIF₁ CIF₂ : {A : 𝕌} → (c : A ↔ A) → 𝔹 ×ᵤ A ↔ 𝔹 ×ᵤ A
CIF₁ c = CIF c id↔
CIF₂ c = CIF id↔ c

-- TOFFOLI(b₁,…,bₙ,b) = (b₁,…,bₙ,b xor (b₁ ∧ … ∧ bₙ))
TOFFOLI : {n : ℕ} → 𝔹^ n ↔ 𝔹^ n
TOFFOLI {0} = id↔
TOFFOLI {1} = swap₊
TOFFOLI {suc (suc n)} = CIF₂ TOFFOLI

-- TOFFOLI(b₁,…,bₙ,b) = (b₁,…,bₙ,b xor (¬b₁ ∧ … ∧ ¬bₙ))
TOFFOLI' : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
TOFFOLI' {0} = id↔
TOFFOLI' {1} = swap₊
TOFFOLI' {suc (suc n)} = CIF₁ TOFFOLI'

-- RESET(b₁,…,bₙ) = (b₁ xor (b₁ ∨ … ∨ bₙ),…,bₙ)
RESET : ∀ {n} → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
RESET {0} = id↔
RESET {1} = swap⋆ ⨾ CNOT ⨾ swap⋆
RESET {suc (suc n)} = Ax[BxC]=Bx[AxC] ⨾ CIF RESET (swap₊ ⊗ id↔) ⨾ Ax[BxC]=Bx[AxC]

-----------------------------------------------------------------------------
-- Reversible Copy
-- copy(𝔽,b₁,…,bₙ) = (b₁,b₁,…,bₙ)
COPY : ∀ {n} → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
COPY {0} = id↔
COPY {1} = swap⋆ ⨾ CNOT ⨾ swap⋆
COPY {suc (suc n)} = assocl⋆ ⨾ (COPY {1} ⊗ id↔) ⨾ assocr⋆

-----------------------------------------------------------------------------
-- Arithmetic
-- INCR(b̅) = INCR(b̅ + 1)
INCR : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
INCR {0} = id↔
INCR {1} = swap₊
INCR {suc (suc n)} = (id↔ ⊗ INCR) ⨾ FST2LAST ⨾ TOFFOLI' ⨾ FST2LAST⁻¹

-----------------------------------------------------------------------------
-- Control flow
zigzag : 𝔹 ↔ 𝔹
zigzag = uniti₊l ⨾ (η₊ ⊕ id↔) ⨾ [A+B]+C=[C+B]+A ⨾ (ε₊ ⊕ id↔) ⨾ unite₊l
zigzagₜᵣ = evalₜᵣ zigzag 𝔽

-----------------------------------------------------------------------------
-- Iteration

trace₊ : ∀ {A B C} → A +ᵤ C ↔ B +ᵤ C → A ↔ B
trace₊ f = uniti₊r ⨾ (id↔ ⊕ η₊) ⨾ assocl₊ ⨾ (f ⊕ id↔) ⨾ assocr₊ ⨾ (id↔ ⊕ ε₊) ⨾ unite₊r

-- Given reversible F : 𝔹^n ↔ 𝔹^n, generate a circuit to find x̅ such that F(x̅) = (𝔽,…)
-- via running (LOOP F)(𝔽,𝔽̅).
-- (id↔ ⊗ F)((LOOP F)(𝔽,𝔽̅)) = (𝔽,𝔽,…)
LOOP : ∀ {n} → 𝔹^ n ↔ 𝔹^ n → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
LOOP {0} F = id↔
LOOP {1} F = id↔ ⊗ F
LOOP {suc (suc n)} F = trace₊ ((dist ⊕ id↔) ⨾ [A+B]+C=[A+C]+B ⨾ (factor ⊕ id↔) ⨾
                               ((RESET ⨾ (id↔ ⊗ F) ⨾ COPY ⨾ (id↔ ⊗ ! F)) ⊕ id↔) ⨾
                               (dist ⊕ id↔) ⨾ [A+B]+C=[A+C]+B ⨾ (factor ⊕ (id↔ ⊗ INCR)))

module loop_test where
  -- Examples
  -- AND(𝔽,a,b) = AND(a∧b,a,b)
  AND : 𝔹^ 3 ↔ 𝔹^ 3
  AND = FST2LAST ⨾ (dist ⨾ (id↔ ⊕ (id↔ ⊗ (dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor))) ⨾ factor) ⨾ FST2LAST⁻¹

  NAND : 𝔹^ 3 ↔ 𝔹^ 3
  NAND = AND ⨾ (NOT ⊗ id↔)

  -- OR(𝔽,a,b) = OR(a∨b,a,b)
  OR : 𝔹^ 3 ↔ 𝔹^ 3
  OR = FST2LAST ⨾ (dist ⨾ ((id↔ ⊗ (dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor)) ⊕ (id↔ ⊗ (id↔ ⊗ swap₊))) ⨾ factor) ⨾ FST2LAST⁻¹

  NOR : 𝔹^ 3 ↔ 𝔹^ 3
  NOR = OR ⨾ (NOT ⊗ id↔)

  -- XOR(a,b) = XOR(a xor b,b)
  XOR : 𝔹^ 2 ↔ 𝔹^ 2
  XOR = distl ⨾ (id↔ ⊕ (swap₊ ⊗ id↔)) ⨾ factorl

  tests : List (∃[ n ] (𝔹^ n ↔ 𝔹^ n))
  tests = (_ , LOOP AND) ∷ (_ , LOOP NAND) ∷ (_ , LOOP OR) ∷ (_ , LOOP NOR) ∷ (_ , LOOP XOR) ∷ []

  results : List (Σ[ t ∈ 𝕌 ] ⟦ t ⟧)
  results = L.map (λ {(_ , c) → proj₁ (eval' c (𝔽^ _))}) tests
  -- (_ , 𝔽 , 𝔽 , 𝔽 , 𝔽) ∷
  -- (_ , 𝔽 , 𝔽 , 𝕋 , 𝕋) ∷
  -- (_ , 𝔽 , 𝔽 , 𝔽 , 𝔽) ∷
  -- (_ , 𝔽 , 𝔽 , 𝔽 , 𝕋) ∷
  -- (_ , 𝔽 , 𝔽 , 𝔽) ∷ []

-----------------------------------------------------------------------------
-- Data Structures Conversions
𝟙+ : ℕ → 𝕌
𝟙+ 0 = 𝟘
𝟙+ 1 = 𝟙
𝟙+ (suc (suc n)) = 𝟙 +ᵤ (𝟙+ (suc n))

convert : ∀ {n} → 𝟙+ (2 ^ n) ↔ 𝔹^ n
convert {0} = id↔
convert {1} = id↔
convert {suc (suc n)} =
  split ⨾
  (convert {suc n} ⊕ (coe {n} ⨾ convert {suc n})) ⨾
  (uniti⋆l ⊕ uniti⋆l) ⨾
  factor

  where
    coe : ∀ {n} → 𝟙+ ((2 ^ n) + ((2 ^ n) + 0) + 0) ↔ 𝟙+ (2 ^ (1 + n))
    coe {n} rewrite +-identityʳ ((2 ^ n) + ((2 ^ n) + 0)) = id↔

    split : ∀ {n m} → 𝟙+ (n + m) ↔ (𝟙+ n +ᵤ 𝟙+ m)
    split {0} {m} = uniti₊l
    split {1} {0} = uniti₊r
    split {1} {1} = id↔
    split {1} {suc (suc m)} = id↔
    split {suc (suc n)} {m} = (id↔ ⊕ split) ⨾ assocl₊

2047→2¹¹-1 : 𝟙+ 2047 ↔ (- 𝟙 +ᵤ 𝔹^ 11)
2047→2¹¹-1 = uniti₊l ⨾
             ((η₊ ⨾ swap₊) ⊕ id↔) ⨾
             assocr₊ ⨾
             (id↔ ⊕ convert {11})

incr+ : ∀ {n} → 𝟙+ n ↔ 𝟙+ n
incr+ {0} = id↔
incr+ {1} = id↔
incr+ {2} = swap₊
incr+ {suc (suc (suc n))} = (id↔ ⊕ incr+) ⨾ A+[B+C]=B+[A+C]

incr+' : 𝟙+ 2047 ↔ 𝟙+ 2047
incr+' = 2047→2¹¹-1 ⨾ (id↔ ⊕ INCR) ⨾ ! 2047→2¹¹-1

v : (n : ℕ) → ¬ n ≡ 0 → ⟦ 𝟙+ n ⟧
v 0 0≠0 = 0≠0 refl
v 1 _ = tt
v (suc (suc n)) _ = inj₂ (v (suc n) (λ ()))

len1 = proj₂ (eval' (incr+ {2047}) (v 2047 (λ ())))     -- 32721
len2 = proj₂ (eval' incr+' (v 2047 (λ ())))             -- 20143
len3 = proj₂ (eval' 2047→2¹¹-1 (v 2047 (λ ())))         -- 12433
v' = (proj₂ ∘ proj₁) (eval' 2047→2¹¹-1 (v 2047 (λ ())))
len4 = proj₂ (eval' (id↔ ⊕ INCR) v')                    -- 3453
v'' = (proj₂ ∘ proj₁) (eval' (id↔ ⊕ INCR) v')
len5 = proj₂ (eval' (! 2047→2¹¹-1) v'')                 -- 249

-----------------------------------------------------------------------------
-- Higher-Order Combinators
hof- : {A B : 𝕌} → (A ↔ B) → (𝟘 ↔ - A +ᵤ B)
hof- c = η₊ ⨾ (c ⊕ id↔) ⨾ swap₊

comp- : {A B C : 𝕌} → (- A +ᵤ B) +ᵤ (- B +ᵤ C) ↔ (- A +ᵤ C)
comp- = assocl₊ ⨾ (assocr₊ ⊕ id↔) ⨾ ((id↔ ⊕ ε₊) ⊕ id↔) ⨾ (unite₊r ⊕ id↔)

app- : {A B : 𝕌} → (- A +ᵤ B) +ᵤ A ↔ B
app- = swap₊ ⨾ assocl₊ ⨾ (ε₊ ⊕ id↔) ⨾ unite₊l

-----------------------------------------------------------------------------
-- Algebraic Identities

inv- : {A : 𝕌} → A ↔ - (- A)
inv- = uniti₊r ⨾ (id↔ ⊕ η₊) ⨾ assocl₊ ⨾ (ε₊ ⊕ id↔) ⨾ unite₊l

dist- : {A B : 𝕌} → - (A +ᵤ B) ↔ - A +ᵤ - B
dist- = uniti₊l ⨾ (η₊ ⊕ id↔) ⨾ uniti₊l ⨾ (η₊ ⊕ id↔) ⨾ assocl₊ ⨾
        ([A+B]+[C+D]=[A+C]+[B+D] ⊕ id↔) ⨾
        (swap₊ ⊕ id↔) ⨾ assocr₊ ⨾ (id↔ ⊕ ε₊) ⨾ unite₊r

neg- : {A B : 𝕌} → (A ↔ B) →  (- A ↔ - B)
neg- c = uniti₊r ⨾ (id↔ ⊕ η₊) ⨾
         (id↔ ⊕ ! c ⊕ id↔) ⨾ assocl₊ ⨾
         ((swap₊ ⨾ ε₊) ⊕ id↔) ⨾ unite₊l


text:
-- Agda program using the Iowa Agda library

open import bool

module PROOF-appendAddLengths
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

++ : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
++ [] x = x
++ (y :: z) u = y :: (++ z u)

append : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
append x y = ++ x y

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

appendAddLengths : {a : Set} → (x : 𝕃 a) → (y : 𝕃 a)
                 → ((length x) + (length y)) ≡ (length (append x y))
appendAddLengths [] y = refl
appendAddLengths (x :: xs) y rewrite appendAddLengths xs y = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


text:
{-# OPTIONS --without-K  #-}
module algebra.group.core where

open import level
open import algebra.monoid.core
open import equality.core
open import function.isomorphism
open import sum

record IsGroup {i} (G : Set i) : Set i where
  field instance mon : IsMonoid G
  open IsMonoid mon public

  field
    inv : G → G
    linv : (x : G) → inv x * x ≡ e
    rinv : (x : G) → x * inv x ≡ e

Group : ∀ i → Set (lsuc i)
Group i = Σ (Set i) IsGroup

module _ {i} {G : Set i} ⦃ grp : IsGroup G ⦄ where
  open IsGroup ⦃ ... ⦄

  left-translation-iso : (g : G) → G ≅ G
  left-translation-iso g = record
    { to = λ x → g * x
    ; from = λ x → inv g * x
    ; iso₁ = λ x → sym (assoc _ _ _)
           · ap (λ u → u * x) (linv g)
           · lunit x
    ; iso₂ = λ x → sym (assoc _ _ _)
           · ap (λ u → u * x) (rinv g)
           · lunit x }

  right-translation-iso : (g : G) → G ≅ G
  right-translation-iso g = record
    { to = λ x → x * g
    ; from = λ x → x * inv g
    ; iso₁ = λ x → assoc _ _ _
           · ap (λ u → x * u) (rinv g)
           · runit x
    ; iso₂ = λ x → assoc _ _ _
           · ap (λ u → x * u) (linv g)
           · runit x }

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Andreas, 2015-09-18, issue reported by Guillaume Brunerie

{-# OPTIONS --rewriting #-}

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a
{-# BUILTIN REWRITE _==_ #-}

postulate
  A : Set
  a b : A

r : a == b
{-# REWRITE r #-}
r = idp

-- Should not work, as this behavior is confusing the users.
-- Instead, should give an error that rewrite rule
-- can only be added after function body.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A delimited continuation monad
------------------------------------------------------------------------

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

module Category.Monad.Continuation where

open import Category.Applicative
open import Category.Applicative.Indexed
open import Category.Monad
open import Function.Identity.Categorical as Id using (Identity)
open import Category.Monad.Indexed
open import Function
open import Level

------------------------------------------------------------------------
-- Delimited continuation monads

DContT : ∀ {i f} {I : Set i} → (I → Set f) → (Set f → Set f) → IFun I f
DContT K M r₂ r₁ a = (a → M (K r₁)) → M (K r₂)

DCont : ∀ {i f} {I : Set i} → (I → Set f) → IFun I f
DCont K = DContT K Identity

DContTIMonad : ∀ {i f} {I : Set i} (K : I → Set f) {M} →
               RawMonad M → RawIMonad (DContT K M)
DContTIMonad K Mon = record
  { return = λ a k → k a
  ; _>>=_  = λ c f k → c (flip f k)
  }
  where open RawMonad Mon

DContIMonad : ∀ {i f} {I : Set i} (K : I → Set f) → RawIMonad (DCont K)
DContIMonad K = DContTIMonad K Id.monad

------------------------------------------------------------------------
-- Delimited continuation operations

record RawIMonadDCont {i f} {I : Set i} (K : I → Set f)
                      (M : IFun I f) : Set (i ⊔ suc f) where
  field
    monad : RawIMonad M
    reset : ∀ {r₁ r₂ r₃} → M r₁ r₂ (K r₂) → M r₃ r₃ (K r₁)
    shift : ∀ {a r₁ r₂ r₃ r₄} →
            ((a → M r₁ r₁ (K r₂)) → M r₃ r₄ (K r₄)) → M r₃ r₂ a

  open RawIMonad monad public

DContTIMonadDCont : ∀ {i f} {I : Set i} (K : I → Set f) {M} →
                    RawMonad M → RawIMonadDCont K (DContT K M)
DContTIMonadDCont K Mon = record
  { monad = DContTIMonad K Mon
  ; reset = λ e k → e return >>= k
  ; shift = λ e k → e (λ a k' → (k a) >>= k') return
  }
  where
  open RawIMonad Mon

DContIMonadDCont : ∀ {i f} {I : Set i}
                   (K : I → Set f) → RawIMonadDCont K (DCont K)
DContIMonadDCont K = DContTIMonadDCont K Id.monad


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Reflection.StrictEquiv

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Record

open Iso

private
  variable
    ℓ : Level

-- Semigroups as a record, inspired by the Agda standard library:
--
--  https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Bundles.agda#L48
--  https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L50
--
-- Note that as we are using Path for all equations the IsMagma record
-- would only contain isSet A if we had it.
record IsSemigroup {A : Type ℓ} (_·_ : A → A → A) : Type ℓ where

  constructor issemigroup

  field
    is-set : isSet A
    assoc  : (x y z : A) → x · (y · z) ≡ (x · y) · z

record SemigroupStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor semigroupstr

  field
    _·_         : A → A → A
    isSemigroup : IsSemigroup _·_

  infixl 7 _·_

  open IsSemigroup isSemigroup public

Semigroup : Type (ℓ-suc ℓ)
Semigroup = TypeWithStr _ SemigroupStr

semigroup : (A : Type ℓ) (_·_ : A → A → A) (h : IsSemigroup _·_) → Semigroup
semigroup A _·_ h = A , semigroupstr _·_ h

record SemigroupEquiv (M N : Semigroup {ℓ}) (e : ⟨ M ⟩ ≃ ⟨ N ⟩) : Type ℓ where

  constructor semigroupequiv

  -- Shorter qualified names
  private
    module M = SemigroupStr (snd M)
    module N = SemigroupStr (snd N)

  field
    isHom : (x y : ⟨ M ⟩) → equivFun e (x M.· y) ≡ equivFun e x N.· equivFun e y

open SemigroupStr
open IsSemigroup
open SemigroupEquiv

-- Develop some theory about Semigroups using various general results
-- that are stated using Σ-types. For this we define Semigroup as a
-- nested Σ-type, prove that it's equivalent to the above record
-- definition and then transport results along this equivalence.
module SemigroupΣTheory {ℓ} where

  RawSemigroupStructure : Type ℓ → Type ℓ
  RawSemigroupStructure X = X → X → X

  RawSemigroupEquivStr = AutoEquivStr RawSemigroupStructure

  rawSemigroupUnivalentStr : UnivalentStr _ RawSemigroupEquivStr
  rawSemigroupUnivalentStr = autoUnivalentStr RawSemigroupStructure

  SemigroupAxioms : (A : Type ℓ) → RawSemigroupStructure A → Type ℓ
  SemigroupAxioms A _·_ = isSet A
                        × ((x y z : A) → x · (y · z) ≡ (x · y) · z)

  SemigroupStructure : Type ℓ → Type ℓ
  SemigroupStructure = AxiomsStructure RawSemigroupStructure SemigroupAxioms

  SemigroupΣ : Type (ℓ-suc ℓ)
  SemigroupΣ = TypeWithStr ℓ SemigroupStructure

  isPropSemigroupAxioms : (A : Type ℓ) (_·_ : RawSemigroupStructure A)
                        → isProp (SemigroupAxioms A _·_)
  isPropSemigroupAxioms _ _ = isPropΣ isPropIsSet λ isSetA → isPropΠ3 λ _ _ _ → isSetA _ _

  SemigroupEquivStr : StrEquiv SemigroupStructure ℓ
  SemigroupEquivStr = AxiomsEquivStr RawSemigroupEquivStr SemigroupAxioms

  SemigroupAxiomsIsoIsSemigroup : {A : Type ℓ} (_·_ : RawSemigroupStructure A)
                                → Iso (SemigroupAxioms A _·_) (IsSemigroup _·_)
  fun (SemigroupAxiomsIsoIsSemigroup s) (x , y)           = issemigroup x y
  inv (SemigroupAxiomsIsoIsSemigroup s) M                 = is-set M , assoc M
  rightInv (SemigroupAxiomsIsoIsSemigroup s) _            = refl
  leftInv (SemigroupAxiomsIsoIsSemigroup s) _             = refl

  SemigroupAxioms≡IsSemigroup : {A : Type ℓ} (_·_ : RawSemigroupStructure A)
                              → SemigroupAxioms _ _·_ ≡ IsSemigroup _·_
  SemigroupAxioms≡IsSemigroup s = isoToPath (SemigroupAxiomsIsoIsSemigroup s)

  Semigroup→SemigroupΣ : Semigroup → SemigroupΣ
  Semigroup→SemigroupΣ (A , semigroupstr _·_ isSemigroup) =
    A , _·_ , SemigroupAxiomsIsoIsSemigroup _ .inv isSemigroup

  SemigroupΣ→Semigroup : SemigroupΣ → Semigroup
  SemigroupΣ→Semigroup (A , _·_ , isSemigroupΣ) =
    semigroup A _·_ (SemigroupAxiomsIsoIsSemigroup _ .fun isSemigroupΣ)

  SemigroupIsoSemigroupΣ : Iso Semigroup SemigroupΣ
  SemigroupIsoSemigroupΣ =
    iso Semigroup→SemigroupΣ SemigroupΣ→Semigroup (λ _ → refl) (λ _ → refl)

  semigroupUnivalentStr : UnivalentStr SemigroupStructure SemigroupEquivStr
  semigroupUnivalentStr = axiomsUnivalentStr _ isPropSemigroupAxioms rawSemigroupUnivalentStr

  SemigroupΣPath : (M N : SemigroupΣ) → (M ≃[ SemigroupEquivStr ] N) ≃ (M ≡ N)
  SemigroupΣPath = SIP semigroupUnivalentStr

  SemigroupEquivΣ : (M N : Semigroup) → Type ℓ
  SemigroupEquivΣ M N = Semigroup→SemigroupΣ M ≃[ SemigroupEquivStr ] Semigroup→SemigroupΣ N

  SemigroupIsoΣPath : {M N : Semigroup} → Iso (Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] SemigroupEquiv M N e) (SemigroupEquivΣ M N)
  fun SemigroupIsoΣPath (e , x) = e , isHom x
  inv SemigroupIsoΣPath (e , h) = e , semigroupequiv h
  rightInv SemigroupIsoΣPath _  = refl
  leftInv SemigroupIsoΣPath _   = refl

  SemigroupPath : (M N : Semigroup) → (Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] SemigroupEquiv M N e) ≃ (M ≡ N)
  SemigroupPath M N =
    Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] SemigroupEquiv M N e ≃⟨ strictIsoToEquiv SemigroupIsoΣPath ⟩
    SemigroupEquivΣ M N ≃⟨ SemigroupΣPath _ _ ⟩
    Semigroup→SemigroupΣ M ≡ Semigroup→SemigroupΣ N ≃⟨ isoToEquiv (invIso (congIso SemigroupIsoSemigroupΣ)) ⟩
    M ≡ N ■

-- We now extract the important results from the above module

isPropIsSemigroup : {A : Type ℓ} (_·_ : A → A → A) → isProp (IsSemigroup _·_)
isPropIsSemigroup _·_ =
  subst isProp (SemigroupΣTheory.SemigroupAxioms≡IsSemigroup _·_)
        (SemigroupΣTheory.isPropSemigroupAxioms _ _·_)

SemigroupPath : (M N : Semigroup {ℓ}) → (Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] SemigroupEquiv M N e) ≃ (M ≡ N)
SemigroupPath {ℓ = ℓ} =
  SIP
    (autoUnivalentRecord
      (autoRecordSpec (SemigroupStr {ℓ}) SemigroupEquiv
        (fields:
          data[ _·_ ∣ isHom ]
          prop[ isSemigroup ∣ (λ _ → isPropIsSemigroup _) ]))
      _ _)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module STLC1.Kovacs.Convertibility where

open import STLC1.Kovacs.Substitution public

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

-- Convertibility (_~_ ; ~refl ; _~⁻¹ ; lam ; app ; β ; η)
infix 3 _∼_
data _∼_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set
  where
    refl∼ : ∀ {Γ A} → {M : Γ ⊢ A}
                    → M ∼ M

    _⁻¹∼  : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
                    → (p : M₁ ∼ M₂)
                    → M₂ ∼ M₁

    _⦙∼_  : ∀ {Γ A} → {M₁ M₂ M₃ : Γ ⊢ A}
                    → (p : M₁ ∼ M₂) (q : M₂ ∼ M₃)
                    → M₁ ∼ M₃

    ƛ∼    : ∀ {Γ A B} → {M₁ M₂ : Γ , A ⊢ B}
                      → (p : M₁ ∼ M₂)
                      → ƛ M₁ ∼ ƛ M₂

    _∙∼_  : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⇒ B} {N₁ N₂ : Γ ⊢ A}
                      → (p : M₁ ∼ M₂) (q : N₁ ∼ N₂)
                      → M₁ ∙ N₁ ∼ M₂ ∙ N₂

    _,∼_  : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A} {N₁ N₂ : Γ ⊢ B}
                      → (p : M₁ ∼ M₂) (q : N₁ ∼ N₂)
                      → M₁ , N₁ ∼ M₂ , N₂

    π₁∼   : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⩕ B}
                      → (p : M₁ ∼ M₂)
                      → π₁ M₁ ∼ π₁ M₂

    π₂∼   : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⩕ B}
                      → (p : M₁ ∼ M₂)
                      → π₂ M₁ ∼ π₂ M₂

    red⇒ : ∀ {Γ A B} → (M : Γ , A ⊢ B) (N : Γ ⊢ A)
                      → (ƛ M) ∙ N ∼ cut N M

    red⩕₁ : ∀ {Γ A B} → (M : Γ ⊢ A) (N : Γ ⊢ B)
                      → π₁ (M , N) ∼ M

    red⩕₂ : ∀ {Γ A B} → (M : Γ ⊢ A) (N : Γ ⊢ B)
                      → π₂ (M , N) ∼ N

    exp⇒ : ∀ {Γ A B} → (M : Γ ⊢ A ⇒ B)
                      → M ∼ ƛ (wk M ∙ 0)

    exp⩕  : ∀ {Γ A B} → (M : Γ ⊢ A ⩕ B)
                      → M ∼ π₁ M , π₂ M

    exp⫪ : ∀ {Γ} → (M : Γ ⊢ ⫪)
                  → M ∼ τ

≡→∼ : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
               → M₁ ≡ M₂
               → M₁ ∼ M₂
≡→∼ refl = refl∼

instance
  per∼ : ∀ {Γ A} → PER (Γ ⊢ A) _∼_
  per∼ =
    record
      { _⁻¹ = _⁻¹∼
      ; _⦙_ = _⦙∼_
      }

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

renwk : ∀ {Γ Γ′ A B} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ A)
                     → (wk {B} ∘ ren η) M ≡
                        (ren (liftₑ η) ∘ wk) M
renwk η M = ren○ (wkₑ idₑ) η M ⁻¹
          ⦙ (λ η′ → ren (wkₑ η′) M) & ( rid○ η
                                       ⦙ lid○ η ⁻¹
                                       )
          ⦙ ren○ (liftₑ η) (wkₑ idₑ) M

rencut : ∀ {Γ Γ′ A B} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ A) (N : Γ , A ⊢ B)
                      → (cut (ren η M) ∘ ren (liftₑ η)) N ≡
                         (ren η ∘ cut M) N
rencut η M N = sub◑ (idₛ , ren η M) (liftₑ η) N ⁻¹
             ⦙ (λ σ → sub (σ , ren η M) N) & ( rid◑ η
                                              ⦙ lid◐ η ⁻¹
                                              )
             ⦙ sub◐ η (idₛ , M) N

-- (~ₑ)
ren∼ : ∀ {Γ Γ′ A} → {M₁ M₂ : Γ ⊢ A}
                  → (η : Γ′ ⊇ Γ) → M₁ ∼ M₂
                  → ren η M₁ ∼ ren η M₂
ren∼ η refl∼       = refl∼
ren∼ η (p ⁻¹∼)     = ren∼ η p ⁻¹
ren∼ η (p ⦙∼ q)    = ren∼ η p ⦙ ren∼ η q
ren∼ η (ƛ∼ p)      = ƛ∼ (ren∼ (liftₑ η) p)
ren∼ η (p ∙∼ q)    = ren∼ η p ∙∼ ren∼ η q
ren∼ η (p ,∼ q)    = ren∼ η p ,∼ ren∼ η q
ren∼ η (π₁∼ p)     = π₁∼ (ren∼ η p)
ren∼ η (π₂∼ p)     = π₂∼ (ren∼ η p)
ren∼ η (red⇒ M N) = coe (((ƛ (ren (liftₑ η) M) ∙ ren η N) ∼_)
                          & rencut η N M)
                         (red⇒ (ren (liftₑ η) M) (ren η N))
ren∼ η (red⩕₁ M N) = red⩕₁ (ren η M) (ren η N)
ren∼ η (red⩕₂ M N) = red⩕₂ (ren η M) (ren η N)
ren∼ η (exp⇒ M)   = coe ((λ M′ → ren η M ∼ ƛ (M′ ∙ 0))
                          & renwk η M)
                         (exp⇒ (ren η M))
ren∼ η (exp⩕ M)    = exp⩕ (ren η M)
ren∼ η (exp⫪ M)   = exp⫪ (ren η M)

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
module Perm where

open import Basics
open import All
open import Splitting

data _~_ {X : Set} : List X -> List X -> Set where
  [] : [] ~ []
  _,-_ : forall {x xs ys zs} -> (x ,- []) <[ ys ]> zs -> xs ~ zs -> (x ,- xs) ~ ys

permute : {X : Set}{xs ys : List X} -> xs ~ ys ->
          {P : X -> Set} -> All P xs -> All P ys
permute []        <> = <>
permute (i ,- is) (p , ps) = riffle i (p , <>) (permute is ps)

reflP : {X : Set}(xs : List X) -> xs ~ xs
reflP [] = []
reflP (x ,- xs) = sl (srs xs) ,- reflP xs

insP : forall {X : Set}{x : X}{xs xs' ys ys'} -> (x ,- []) <[ xs' ]> xs -> (x ,- []) <[ ys' ]> ys
         -> xs ~ ys -> xs' ~ ys'
insP (sl i) j p with isSRS i
insP (sl .(srs _)) j p | mkSRS = j ,- p
insP (sr i) j (k ,- p) =
  let  _ , k' , j' = llswap (_ , j , k)
  in   k' ,- insP i j' p

l2r : forall {X : Set}{x : X}{xs xs' ys'}(i : (x ,- []) <[ xs' ]> xs)(p' : xs' ~ ys') ->
  Sg (List X) \ ys -> Sg ((x ,- []) <[ ys' ]> ys) \ j -> xs ~ ys
l2r (sl i) (j ,- p) with isSRS i
l2r (sl .(srs _)) (j ,- p) | mkSRS = _ , j , p
l2r (sr i) (k' ,- p') with l2r i p'
... | _ , j' , p with llswap (_ , k' , j')
... | _ , j , k = _ , j , (k ,- p)

transP : {X : Set}{xs ys zs : List X} -> xs ~ ys -> ys ~ zs -> xs ~ zs
transP [] [] = []
transP (i ,- p) q' with l2r i q'
... | _ , j , q = j ,- transP p q

symP : {X : Set}{xs ys : List X} -> xs ~ ys -> ys ~ xs
symP [] = []
symP (i ,- p) = insP i (sl (srs _)) (symP p)

swapP : {X : Set}(xs ys : List X) -> (xs +L ys) ~ (ys +L xs)
swapP [] ys rewrite ys +L[] = reflP ys
swapP (x ,- xs) ys = insS ys x xs ,- swapP xs ys

catP : forall {X : Set}{as bs cs ds : List X} -> as ~ cs -> bs ~ ds -> (as +L bs) ~ (cs +L ds)
catP [] q = q
catP (x ,- p) q = catS x (srs _) ,- catP p q

permap : forall {X Y}(f : X -> Y){xs xs' : List X} -> xs ~ xs' -> list f xs ~ list f xs'
permap f [] = []
permap f (x ,- p) = splimap f x ,- permap f p

cartNil : forall {I}(is : List I){J} -> cart {J = J} is [] == []
cartNil [] = refl []
cartNil (i ,- is) = cartNil is

cartCons : forall {I J}(is : List I)(j : J)(js : List J) ->
  cart is (j ,- js) ~ (list (_, j) is +L cart is js)
cartCons [] j js = []
cartCons (i ,- is) j js with catP (swapP (list (i ,_) js) (list (_, j) is)) (reflP (cart is js))
... | z rewrite assoc+L (list (i ,_) js) (list (_, j) is) (cart is js)
              | assoc+L (list (_, j) is) (list (i ,_) js) (cart is js)
  =
  (sl (srs (list (_, j) is +L cart (i ,- is) js))) ,-
  transP (catP (reflP (list (i ,_) js)) (cartCons is j js))
    z

cartLemma : forall {I J}(is : List I)(js : List J) ->
  cart is js ~ list swap (cart js is)
cartLemma {I}{J} [] js rewrite cartNil js {I} = []
cartLemma {I}{J} (i ,- is) js with catP (reflP (list (i ,_) js)) (cartLemma is js)
... | z rewrite sym (listlist swap (_, i) (i ,_) (\ j ->  refl (i , j)) js)
              | catNatural swap (list (_, i) js) (cart js is)
  = transP
  z
  (symP (permap (\ ji -> snd ji , fst ji) (cartCons js i is)))

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
-- Andreas, 2012-09-19 propagate irrelevance info to dot patterns
{-# OPTIONS --experimental-irrelevance #-}
-- {-# OPTIONS -v tc.lhs:20 #-}
module ShapeIrrelevantIndex where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

data Good : ..(_ : Nat) → Set where
  goo  : .(n : Nat) → Good (S n)

good : .(n : Nat) → Good n → Nat
good .(S n) (goo n) = Z


text:
module Pi.Examples where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Vec as V hiding (map)
open import Pi.Syntax
open import Pi.Opsem
open import Pi.Eval

pattern 𝔹 = 𝟙 +ᵤ 𝟙
pattern 𝔽 = inj₁ tt
pattern 𝕋 = inj₂ tt

𝔹^ : ℕ → 𝕌
𝔹^ 0 = 𝟙
𝔹^ 1 = 𝔹
𝔹^ (suc (suc n)) = 𝔹 ×ᵤ 𝔹^ (suc n)

-----------------------------------------------------------------------------
-- Adaptors

[A+B]+C=[C+B]+A : ∀ {A B C} → (A +ᵤ B) +ᵤ C ↔ (C +ᵤ B) +ᵤ A
[A+B]+C=[C+B]+A = assocr₊ ⨾ (id↔ ⊕ swap₊) ⨾ swap₊

[A+B]+C=[A+C]+B : ∀ {A B C} → (A +ᵤ B) +ᵤ C ↔ (A +ᵤ C) +ᵤ B
[A+B]+C=[A+C]+B = assocr₊ ⨾ (id↔ ⊕ swap₊) ⨾ assocl₊

[A+B]+[C+D]=[A+C]+[B+D] : {A B C D : 𝕌} → (A +ᵤ B) +ᵤ (C +ᵤ D) ↔ (A +ᵤ C) +ᵤ (B +ᵤ D)
[A+B]+[C+D]=[A+C]+[B+D] =  assocl₊ ⨾ (assocr₊ ⊕ id↔) ⨾ ((id↔ ⊕ swap₊) ⊕ id↔) ⨾ (assocl₊ ⊕ id↔) ⨾ assocr₊

Ax[BxC]=Bx[AxC] : {A B C : 𝕌} → A ×ᵤ (B ×ᵤ C) ↔ B ×ᵤ (A ×ᵤ C)
Ax[BxC]=Bx[AxC] = assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾  assocr⋆

[AxB]×C=[A×C]xB : ∀ {A B C} → (A ×ᵤ B) ×ᵤ C ↔ (A ×ᵤ C) ×ᵤ B
[AxB]×C=[A×C]xB = assocr⋆ ⨾ (id↔ ⊗ swap⋆) ⨾ assocl⋆

[A×B]×[C×D]=[A×C]×[B×D] : {A B C D : 𝕌} → (A ×ᵤ B) ×ᵤ (C ×ᵤ D) ↔ (A ×ᵤ C) ×ᵤ (B ×ᵤ D)
[A×B]×[C×D]=[A×C]×[B×D] = assocl⋆ ⨾ (assocr⋆ ⊗ id↔) ⨾ ((id↔ ⊗ swap⋆) ⊗ id↔) ⨾ (assocl⋆ ⊗ id↔) ⨾ assocr⋆

-- FST2LAST(b₁,b₂,…,bₙ) = (b₂,…,bₙ,b₁)
FST2LAST : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
FST2LAST {0} = id↔
FST2LAST {1} = id↔
FST2LAST {2} = swap⋆
FST2LAST {suc (suc (suc n))} = Ax[BxC]=Bx[AxC] ⨾ (id↔ ⊗ FST2LAST)

FST2LAST⁻¹ : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
FST2LAST⁻¹ = ! FST2LAST

-- NOT(b) = ¬b
NOT : 𝔹 ↔ 𝔹
NOT = swap₊

-- CNOT(b₁,b₂) = (b₁,b₁ xor b₂)
CNOT : 𝔹 ×ᵤ 𝔹 ↔ 𝔹 ×ᵤ 𝔹
CNOT = dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor

-- CIF(c₁,c₂)(𝔽,a) = (𝔽,c₁ a)
-- CIF(c₁,c₂)(𝕋,a) = (𝕋,c₂ a)
CIF : {A : 𝕌} → (c₁ c₂ : A ↔ A) → 𝔹 ×ᵤ A ↔ 𝔹 ×ᵤ A
CIF c₁ c₂ = dist ⨾ ((id↔ ⊗ c₁) ⊕ (id↔ ⊗ c₂)) ⨾ factor

CIF₁ CIF₂ : {A : 𝕌} → (c : A ↔ A) → 𝔹 ×ᵤ A ↔ 𝔹 ×ᵤ A
CIF₁ c = CIF c id↔
CIF₂ c = CIF id↔ c

-- TOFFOLI(b₁,…,bₙ,b) = (b₁,…,bₙ,b xor (b₁ ∧ … ∧ bₙ))
TOFFOLI : {n : ℕ} → 𝔹^ n ↔ 𝔹^ n
TOFFOLI {0} = id↔
TOFFOLI {1} = swap₊
TOFFOLI {suc (suc n)} = CIF₂ TOFFOLI

-- TOFFOLI(b₁,…,bₙ,b) = (b₁,…,bₙ,b xor (¬b₁ ∧ … ∧ ¬bₙ))
TOFFOLI' : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
TOFFOLI' {0} = id↔
TOFFOLI' {1} = swap₊
TOFFOLI' {suc (suc n)} = CIF₁ TOFFOLI'

-- RESET(b₁,…,bₙ) = (b₁ xor (b₁ ∨ … ∨ bₙ),…,bₙ)
RESET : ∀ {n} → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
RESET {0} = id↔
RESET {1} = swap⋆ ⨾ CNOT ⨾ swap⋆
RESET {suc (suc n)} = Ax[BxC]=Bx[AxC] ⨾ CIF RESET (swap₊ ⊗ id↔) ⨾ Ax[BxC]=Bx[AxC]

-----------------------------------------------------------------------------
-- Reversible Copy
-- copy(𝔽,b₁,…,bₙ) = (b₁,b₁,…,bₙ)
COPY : ∀ {n} → 𝔹 ×ᵤ 𝔹^ n ↔ 𝔹 ×ᵤ 𝔹^ n
COPY {0} = id↔
COPY {1} = swap⋆ ⨾ CNOT ⨾ swap⋆
COPY {suc (suc n)} = assocl⋆ ⨾ (COPY {1} ⊗ id↔) ⨾ assocr⋆

-----------------------------------------------------------------------------
-- Arithmetic
-- INCR(b̅) = INCR(b̅ + 1)
INCR : ∀ {n} → 𝔹^ n ↔ 𝔹^ n
INCR {0} = id↔
INCR {1} = swap₊
INCR {suc (suc n)} = (id↔ ⊗ INCR) ⨾ FST2LAST ⨾ TOFFOLI' ⨾ FST2LAST⁻¹

iterate : (n : ℕ) → (𝔹^ n ↔ 𝔹^ n) → Vec ⟦ 𝔹^ n ⟧ (2 ^ n)
iterate n f = go initial
  where
    initial : ∀ {m} → ⟦ 𝔹^ m ⟧
    initial {zero} = tt
    initial {suc zero} = 𝔽
    initial {suc (suc m)} = 𝔽 , initial

    go : ∀ {m} → ⟦ 𝔹^ n ⟧ → Vec ⟦ 𝔹^ n ⟧ m
    go {0} v = []
    go {suc m} v = let v' = eval f v
                   in  v ∷ go v'

INCRₜₑₛₜ = iterate 4 INCR