text:
------------------------------------------------------------------------
-- Asymmetric choice
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module TotalParserCombinators.AsymmetricChoice where

open import Data.Empty
open import Data.List
open import Data.List.Any using (here)
open import Data.List.Any.Membership.Propositional
  using (_∈_) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Product
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (module Equivalence)
open import Function.Inverse as Inv using (_↔_)
open import Function.Related as Related
open import Function.Related.TypeIsomorphisms
import Relation.Binary.PropositionalEquality as P
import Relation.Binary.Sigma.Pointwise as Σ

open import TotalParserCombinators.Congruence using (_∼[_]P_; _≅P_)
open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Parser
import TotalParserCombinators.Pointwise as Pointwise
open import TotalParserCombinators.Semantics using (_∈_·_)

------------------------------------------------------------------------
-- An initial bag operator

-- first-nonempty returns the left-most non-empty initial bag, if any.

first-nonempty : {R : Set} → List R → List R → List R
first-nonempty [] ys = ys
first-nonempty xs ys = xs

-- first-nonempty preserves equality.

first-nonempty-cong :
  ∀ {k R} {xs₁ xs₁′ xs₂ xs₂′ : List R} →
  xs₁ List-∼[ ⌊ k ⌋⇔ ] xs₁′ → xs₂ List-∼[ ⌊ k ⌋⇔ ] xs₂′ →
  first-nonempty xs₁ xs₂ List-∼[ ⌊ k ⌋⇔ ] first-nonempty xs₁′ xs₂′
first-nonempty-cong {xs₁ = []}    {[]}    eq₁ eq₂ = eq₂
first-nonempty-cong {xs₁ = _ ∷ _} {_ ∷ _} eq₁ eq₂ = eq₁
first-nonempty-cong {xs₁ = []} {_ ∷ _} eq₁ eq₂
  with Equivalence.from (⇒⇔ eq₁) ⟨$⟩ here P.refl
... | ()
first-nonempty-cong {xs₁ = _ ∷ _} {[]} eq₁ eq₂
  with Equivalence.to (⇒⇔ eq₁) ⟨$⟩ here P.refl
... | ()

-- first-nonempty is correct.

first-nonempty-left :
  ∀ {k R} {xs₁ xs₂ : List R} →
  (∃ λ y → y ∈ xs₁) → first-nonempty xs₁ xs₂ List-∼[ k ] xs₁
first-nonempty-left {xs₁ = []}    (_ , ())
first-nonempty-left {xs₁ = _ ∷ _} _        = _ ∎
  where open Related.EquationalReasoning

first-nonempty-right :
  ∀ {k R} {xs₁ xs₂ : List R} →
  (∄ λ y → y ∈ xs₁) → first-nonempty xs₁ xs₂ List-∼[ k ] xs₂
first-nonempty-right {xs₁ = x ∷ _} ∉x∷ = ⊥-elim $ ∉x∷ (x , here P.refl)
first-nonempty-right {xs₁ = []}    _   = _ ∎
  where open Related.EquationalReasoning

------------------------------------------------------------------------
-- Asymmetric choice

-- _◃_ is defined as a pointwise lifting of first-nonempty. Note that
-- _◃_ preserves parser and language equality, but not the
-- sub-/superparser and sub-/superlanguage relations.

private
  module AC {R} = Pointwise R R ⌊_⌋⇔ first-nonempty first-nonempty-cong

-- p₁ ◃ p₂ returns a result if either p₁ or p₂ does. For a given
-- string results are returned either from p₁ or from p₂, not both.

infixl 5 _◃_ _◃-cong_

_◃_ : ∀ {Tok R xs₁ xs₂} →
      Parser Tok R xs₁ → Parser Tok R xs₂ →
      Parser Tok R (first-nonempty xs₁ xs₂)
_◃_ = AC.lift

-- D distributes over _◃_.

D-◃ : ∀ {Tok R xs₁ xs₂ t}
      (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
      D t (p₁ ◃ p₂) ≅P D t p₁ ◃ D t p₂
D-◃ = AC.D-lift

-- _◃_ preserves equality.

_◃-cong_ : ∀ {k Tok R xs₁ xs₁′ xs₂ xs₂′}
             {p₁  : Parser Tok R xs₁} {p₁′ : Parser Tok R xs₁′}
             {p₂  : Parser Tok R xs₂} {p₂′ : Parser Tok R xs₂′} →
           p₁ ∼[ ⌊ k ⌋⇔ ]P p₁′ → p₂ ∼[ ⌊ k ⌋⇔ ]P p₂′ →
           p₁ ◃ p₂ ∼[ ⌊ k ⌋⇔ ]P p₁′ ◃ p₂′
_◃-cong_ = AC.lift-cong

-- If p₁ accepts s, then p₁ ◃ p₂ behaves as p₁ when applied to s.

left : ∀ {Tok R xs₁ xs₂ x s}
       (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
       (∃ λ y → y ∈ p₁ · s) → x ∈ p₁ ◃ p₂ · s ↔ x ∈ p₁ · s
left {x = x} =
  AC.lift-property
    (λ F _ H → ∃ F → H x ↔ F x)
    (λ F↔F′ _ H↔H′ →
       Σ.cong Inv.id (λ {x} → ↔⇒ (F↔F′ x))
         →-cong-⇔
       Related-cong (H↔H′ x) (F↔F′ x))
    (λ ∈xs₁ → first-nonempty-left ∈xs₁)

-- If p₁ does not accept s, then p₁ ◃ p₂ behaves as p₂ when applied to
-- s.

right : ∀ {Tok R xs₁ xs₂ x s}
        (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
        (∄ λ y → y ∈ p₁ · s) → x ∈ p₁ ◃ p₂ · s ↔ x ∈ p₂ · s
right {x = x} =
  AC.lift-property
    (λ F G H → ∄ F → H x ↔ G x)
    (λ F↔F′ G↔G′ H↔H′ →
       ¬-cong-⇔ (Σ.cong Inv.id λ {x} → ↔⇒ (F↔F′ x))
         →-cong-⇔
       Related-cong (H↔H′ x) (G↔G′ x))
    (λ ∉xs₁ → first-nonempty-right ∉xs₁)

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: yurrriq/parser-combinators

max_forks_repo_name: yurrriq/parser-combinators


text:
{-

        Agda Implementors' Meeting VI

                  Göteborg
             May 24 - 30, 2007

                Hello Agda!

                Ulf Norell

-}

{-

   Getting your hands on Agda

   http://www.cs.chalmers.se/~ulfn/Agda

   darcs get --partial http://www.cs.chalmers.se/~ulfn/darcs/Agda2

-}

-- Each Agda file contains a top-level module, whose
-- name corresponds to the file name.

module Basics where

{-

  Expressions (types and terms)

-}

-- The expression language of Agda is your favorite dependently
-- typed λ-calculus.

-- For instance:
id₁ : (A : Set) -> A -> A
id₁ = \ A x -> x

id₂ : (A : Set) -> A -> A
id₂ = \ A x -> id₁ A (id₁ A x)

-- Note: Agda likes white space. This is not correct:
--   id:(A:Set)->A->A
-- Why not? In Agda the following strings are valid identifiers:
--   id:
--   A:Set
--   ->A->A

-- Another useful function, featuring telescopes
-- and typed λs.
compose : (A B C : Set)(f : B -> C)(g : A -> B) -> A -> C
compose = \(A B C : Set) -> \ f g x -> f (g x)

{-

  Implicit arguments

-}

-- Writing down type arguments explicitly soon gets old.
-- Enter implicit arguments.

-- Note the curlies in the telescope. And A mysteriously disappeared
-- in the definition.
id₃ : {A : Set} -> A -> A
id₃ = \ x -> x

-- And it's not there when applying the function.
id₄ : {A : Set} -> A -> A
id₄ = \ x -> (id₃ (id₃ x))

-- You can give implicit arguments explicitly.
id₅ : {A : Set} -> A -> A
id₅ {A} x = id₄ {A} x

-- If you want to give a particular implicit argument, you can refer
-- to it by name.
const : {A B : Set} -> A -> B -> A
const = \ x y -> x

const' : (A : Set) -> A -> A -> A
const' = \ A -> const {B = A}

-- It also works the other way around. If you think the type checker
-- should figure out the value of something explicit, you write _.
id₆ : {A : Set} -> A -> A
id₆ x = id₁ _ x

-- Interesting though it is, eventually you'll get bored
-- with the λ-calculus...

-- Move on to: Datatypes.agda

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

postulate
  F : Set → Set

module M₀ where
  macro
    go-tactic₀ : Term → TC ⊤
    go-tactic₀ hole = unify hole (def (quote F) [])

  test₀ : Set
  test₀ = go-tactic₀ ⊤

module M₁ (A : Set) where
  macro
    go-tactic₁ : Term → TC ⊤
    go-tactic₁ hole = unify hole (def (quote F) [])

  test-inside-M₁ : Set
  test-inside-M₁ = go-tactic₁ ⊤

test-outside-M₁ : Set
test-outside-M₁ = M₁.go-tactic₁ ⊤ ⊤


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

module Relation.Binary where

open import Level

open import Function using (_∘_; flip; id)
open import Inspect  using (inspect;〖_〗)

open import HLevels   using (isSet)
open import Path as ≡ hiding (sym; refl)

open import Data.Bool            using (Bool; true; false; bool)
open import Data.Bool.Properties using (false≢true)
open import Data.Empty           using (⊥; ⊥-elim; ¬_)
open import Data.Sum             using (either; inl; inr; _⊎_; is-l)

open import Relation.Nullary.Decidable            using (Dec; yes; no; does)
open import Relation.Nullary.Decidable.Properties using (Dec→Stable)
open import Relation.Nullary.Discrete             using (Discrete)
open import Relation.Nullary.Discrete.Properties  using (Discrete→isSet)
open import Relation.Nullary.Stable               using (Stable)

module _ (_~_ : A → A → Type b) where
  Reflexive : Type _
  Reflexive = ∀ {x} → x ~ x

  Transitive : Type _
  Transitive = ∀ {x y z} → x ~ y → y ~ z → x ~ z

  Symmetric : Type _
  Symmetric = ∀ {x y} → x ~ y → y ~ x

  Decidable : Type _
  Decidable = ∀ x y → Dec (x ~ y)

  Antisymmetric : Type _
  Antisymmetric = ∀ {x y} → x ~ y → y ~ x → x ≡ y

  Connected : Type _
  Connected = ∀ {x y} → ¬ (x ~ y) → ¬ (y ~ x) → x ≡ y

  Asymmetric : Type _
  Asymmetric = ∀ {x y} → x ~ y → ¬ (y ~ x)

  Irreflexive : Type _
  Irreflexive = ∀ {x} → ¬ (x ~ x)

  Total : Type _
  Total = ∀ x y → (x ~ y) ⊎ (y ~ x)

record Preorder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _≤_
  field
    _≤_ : 𝑆 → 𝑆 → Type ℓ₂
    refl : Reflexive _≤_
    trans : Transitive _≤_

  infix 4 _≰_ _≥_ _≱_
  _≰_ _≥_ _≱_ : 𝑆 → 𝑆 → Type ℓ₂
  x ≰ y = ¬ (x ≤ y)
  x ≥ y = y ≤ x
  x ≱ y = ¬ (y ≤ x)

record StrictPreorder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _<_
  field
    _<_ : 𝑆 → 𝑆 → Type ℓ₂
    trans : Transitive _<_
    irrefl : Irreflexive _<_

  asym : Asymmetric _<_
  asym x<y y<x = irrefl (trans x<y y<x)

  infix 4 _≮_ _>_ _≯_
  _≮_ _>_ _≯_ : 𝑆 → 𝑆 → Type ℓ₂
  x ≮ y = ¬ (x < y)
  x > y = y < x
  x ≯ y = ¬ (y < x)

record StrictPartialOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  field strictPreorder : StrictPreorder 𝑆 ℓ₂
  open StrictPreorder strictPreorder public
  field conn : Connected _<_

record PartialOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  field preorder : Preorder 𝑆 ℓ₂
  open Preorder preorder public
  field antisym : Antisymmetric _≤_

data Tri (A : Type a) (B : Type b) (C : Type c) : Type (a ℓ⊔ b ℓ⊔ c) where
  lt : (x<y : A) → Tri A B C
  eq : (x≡y : B) → Tri A B C
  gt : (x>y : C) → Tri A B C

record TotalOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ ℓ₃ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂ ℓ⊔ ℓsuc ℓ₃) where
  field
    strictPartialOrder : StrictPartialOrder 𝑆 ℓ₂
    partialOrder : PartialOrder 𝑆 ℓ₃
  open PartialOrder partialOrder renaming (trans to ≤-trans) public
  open StrictPartialOrder strictPartialOrder renaming (trans to <-trans) public

  infix 4 _<?_
  field
    _<?_ : Decidable _<_

    ≰⇒> : ∀ {x y} → x ≰ y → x > y
    ≮⇒≥ : ∀ {x y} → x ≮ y → x ≥ y

  <⇒≤ : ∀ {x y} → x < y → x ≤ y
  <⇒≤ = ≮⇒≥ ∘ asym

  _<ᵇ_ : 𝑆 → 𝑆 → Bool
  x <ᵇ y = does (x <? y)

  <⇒≱ : ∀ {x y} → x < y → x ≱ y
  <⇒≱ {x} {y} x<y x≥y = irrefl (subst (_< _) (antisym (<⇒≤ x<y) x≥y) x<y)

  ≤⇒≯ : ∀ {x y} → x ≤ y → x ≯ y
  ≤⇒≯ {x} {y} x≤y x>y = irrefl (subst (_< _) (antisym (≮⇒≥ (asym x>y)) x≤y) x>y)

  infix 4 _≤ᵇ_ _≤?_ _≤|≥_ _≟_

  _≤?_ : Decidable _≤_
  x ≤? y with y <? x
  ... | yes y<x = no  (<⇒≱ y<x)
  ... | no  y≮x = yes (≮⇒≥ y≮x)

  _≤ᵇ_ : 𝑆 → 𝑆 → Bool
  x ≤ᵇ y = does (x ≤? y)

  _≤|≥_ : Total _≤_
  x ≤|≥ y with x <? y
  ... | yes x<y = inl (<⇒≤ x<y)
  ... | no  x≮y = inr (≮⇒≥ x≮y)

  _≟_ : Discrete 𝑆
  x ≟ y with x <? y | y <? x
  ... | yes x<y | _ = no (λ x≡y → irrefl (subst (_< _) x≡y x<y))
  ... | _ | yes y<x = no (λ x≡y → irrefl (subst (_ <_) x≡y y<x))
  ... | no x≮y | no y≮x = yes (conn x≮y y≮x)

  Ordering : (x y : 𝑆) → Type (ℓ₁ ℓ⊔  ℓ₂)
  Ordering x y = Tri (x < y) (x ≡ y) (x > y)

  compare : ∀ x y → Ordering x y
  compare x y with x <? y | y <? x
  ... | yes x<y | _ = lt x<y
  ... | no  x≮y | yes y<x = gt y<x
  ... | no  x≮y | no  y≮x = eq (conn x≮y y≮x)

  total⇒isSet : isSet 𝑆
  total⇒isSet = Discrete→isSet _≟_

module FromPartialOrder {ℓ₁} {𝑆 : Type ℓ₁} {ℓ₂} (po : PartialOrder 𝑆 ℓ₂) (_≤|≥_ : Total (PartialOrder._≤_ po)) where
  open PartialOrder po

  partialOrder = po

  ≤-side : 𝑆 → 𝑆 → Bool
  ≤-side x y = is-l (x ≤|≥ y)

  ≤-dec : Decidable _≤_
  ≤-dec x y with x ≤|≥ y | y ≤|≥ x | inspect (≤-side x) y | inspect (≤-side y) x
  ≤-dec x y | inl x≤y | _       | _ | _ = yes x≤y
  ≤-dec x y | inr x≥y | inr y≥x | _ | _ = yes y≥x
  ≤-dec x y | inr x≥y | inl y≤x | 〖 x≥yᵇ 〗 | 〖 y≤xᵇ 〗 = no (x≢y ∘ flip antisym x≥y)
    where
    x≢y : x ≢ y
    x≢y x≡y = false≢true (≡.sym x≥yᵇ ; cong₂ ≤-side x≡y (≡.sym x≡y) ; y≤xᵇ)

  ≮⇒≥ : ∀ {x y} → Stable (x ≤ y)
  ≮⇒≥ {x} {y} = Dec→Stable _ (≤-dec x y)

  strictPartialOrder : StrictPartialOrder 𝑆 ℓ₂
  strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder._<_ x y = ¬ (y ≤ x)
  strictPartialOrder .StrictPartialOrder.conn x<y y<x = antisym (≮⇒≥ y<x) (≮⇒≥ x<y)
  strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder.irrefl y≰x = y≰x refl
  strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder.trans {x} {y} {z} y≰x z≰y z≤x with ≤-dec y z
  ... | yes y≤z = y≰x (trans y≤z z≤x)
  ... | no  y≰z = either z≰y y≰z (z ≤|≥ y)

  ≰⇒> = id

  _<?_ : Decidable _≱_
  _<?_ x y with ≤-dec y x
  ... | yes y≤x = no λ y≰x → y≰x y≤x
  ... | no  y≰x = yes y≰x

fromPartialOrder : (po : PartialOrder A b) (_≤|≥_ : Total (PartialOrder._≤_ po)) → TotalOrder _ _ _
fromPartialOrder po tot = record { FromPartialOrder po tot }

module FromStrictPartialOrder {ℓ₁} {𝑆 : Type ℓ₁} {ℓ₂} (spo : StrictPartialOrder 𝑆 ℓ₂) (<-dec : Decidable (StrictPartialOrder._<_ spo)) where
  open StrictPartialOrder spo
  strictPartialOrder = spo
  _<?_ = <-dec

  partialOrder : PartialOrder _ _
  partialOrder .PartialOrder.preorder .Preorder._≤_ x y = ¬ (y < x)
  partialOrder .PartialOrder.preorder .Preorder.refl x<x = asym x<x x<x
  partialOrder .PartialOrder.preorder .Preorder.trans {x} {y} {z} y≮x z≮y z<x with x <? y
  ... | yes x<y = z≮y (trans z<x x<y)
  ... | no  x≮y = z≮y (subst (z <_) (conn x≮y y≮x) z<x)
  partialOrder .PartialOrder.antisym = flip conn

  ≰⇒> : ∀ {x y} → Stable (x < y)
  ≰⇒> {x} {y} = Dec→Stable (x < y) (x <? y)

  ≮⇒≥ = id

fromStrictPartialOrder : (spo : StrictPartialOrder A b) (_<?_ : Decidable (StrictPartialOrder._<_ spo)) → TotalOrder _ _ _
fromStrictPartialOrder spo _<?_ = record { FromStrictPartialOrder spo _<?_ }

record Equivalence {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _≋_
  field
    _≋_ : 𝑆 → 𝑆 → Type ℓ₂
    sym   : ∀ {x y} → x ≋ y → y ≋ x
    refl  : ∀ {x} → x ≋ x
    trans : ∀ {x y z} → x ≋ y → y ≋ z → x ≋ z

≡-equivalence : ∀ {a} {A : Set a} → Equivalence A a
≡-equivalence = record
  { _≋_ = _≡_
  ; sym = ≡.sym
  ; refl = ≡.refl
  ; trans = _;_
  }

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

data ⊥ : Set where

private

  {-# TERMINATING #-}
  f : ⊥
  f = f

mutual

  {-# TERMINATING #-}
  g : ⊥
  g = f

abstract

  {-# TERMINATING #-}
  h : ⊥
  h = f

record I : Set where
  {-# TERMINATING #-}
  i : ⊥
  i = f

instance

  {-# TERMINATING #-}
  j : I
  j = j


text:
module Duploid where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning

open import Level

open import Preduploid

private
  variable p q r s : Polarity

record Duploid o ℓ : Set (suc (o ⊔ ℓ)) where
  field
    𝒟 : Preduploid o ℓ

  open Preduploid.Preduploid 𝒟 public

  field
    ⇓ : Ob ⊝ -> Ob +
    ⇑ : Ob + -> Ob ⊝

    delay : forall {P : Ob +} -> P ⇒ ⇑ P
    force : forall {P : Ob +} -> ⇑ P ⇒ P

    wrap : forall {N : Ob ⊝} -> N ⇒ ⇓ N
    unwrap : forall {N : Ob ⊝} -> ⇓ N ⇒ N

    force∘delay∙ : forall {A : Ob p} {P : Ob +} {f : A ⇒ P} -> force ∘ (delay ∙ f) ≡ f
    ∘unwrap∙wrap : forall {N : Ob ⊝} {A : Ob p} {f : N ⇒ A} -> (f ∘ unwrap) ∙ wrap ≡ f
    delay∙force : forall {P : Ob +} -> delay ∙ force ≡ id {A = ⇑ P}
    wrap∘unwrap : forall {N : Ob ⊝} -> wrap ∘ unwrap ≡ id {A = ⇓ N}

  ∙force∘delay : forall {P : Ob +} {A : Ob p} {g : P ⇒ A} -> (g ∙ force) ∘ delay ≡ g
  ∙force∘delay {g = g} =
    begin
      (g ∙ force) ∘ delay
    ≡⟨ assoc∙∘ ⟩
      g ∙ (force ∘ delay)
    ≡˘⟨ cong (g ∙_) (cong (force ∘_) identity∙ʳ) ⟩
      g ∙ (force ∘ (delay ∙ id))
    ≡⟨ cong (g ∙_) force∘delay∙ ⟩
      g ∙ id
    ≡⟨ identity∙ʳ ⟩
     g
    ∎

  unwrap∙wrap∘ : forall {A : Ob p} {N : Ob ⊝} {g : A ⇒ N} -> unwrap ∙ (wrap ∘ g) ≡ g
  unwrap∙wrap∘ {g = g} =
    begin
      unwrap ∙ (wrap ∘ g)
    ≡˘⟨ assoc∙∘ ⟩
      (unwrap ∙ wrap) ∘ g
    ≡˘⟨ cong (_∘ g) (cong (_∙ wrap) identity∘ˡ) ⟩
      ((id ∘ unwrap) ∙ wrap) ∘ g
    ≡⟨ cong (_∘ g) ∘unwrap∙wrap ⟩
      id ∘ g
    ≡⟨ identity∘ˡ ⟩
      g
    ∎

  wrap-Thunkable : forall {N : Ob ⊝} -> Thunkable (wrap {N = N})
  wrap-Thunkable {r = +} = sym assoc∙∙
  wrap-Thunkable {r = ⊝} {g = g} {h = h} =
    begin
      h ∘ (g ∙ wrap)
    ≡˘⟨ ∘unwrap∙wrap ⟩
      ((h ∘ (g ∙ wrap)) ∘ unwrap) ∙ wrap
    ≡⟨ cong (_∙ wrap) assoc∘∘ ⟩
      (h ∘ ((g ∙ wrap) ∘ unwrap)) ∙ wrap
    ≡⟨ cong (_∙ wrap) (cong (h ∘_) assoc∙∘) ⟩
      (h ∘ (g ∙ (wrap ∘ unwrap))) ∙ wrap
    ≡⟨ cong (_∙ wrap) (cong (h ∘_) (cong (g ∙_) wrap∘unwrap)) ⟩
      (h ∘ (g ∙ id)) ∙ wrap
    ≡⟨ cong (_∙ wrap) (cong (h ∘_) identity∙ʳ) ⟩
      (h ∘ g) ∙ wrap
    ∎

  force-Linear : forall {P : Ob +} -> Linear (force {P = P})
  force-Linear {q = +} {g = g} {h = h} = sym (
    begin
      (force ∘ g) ∙ h
    ≡˘⟨ force∘delay∙ ⟩
      force ∘ (delay ∙ ((force ∘ g) ∙ h))
    ≡˘⟨ cong (force ∘_) assoc∙∙ ⟩
      force ∘ ((delay ∙ (force ∘ g)) ∙ h)
    ≡˘⟨ cong (force ∘_) (cong (_∙ h) assoc∙∘) ⟩
      force ∘ (((delay ∙ force) ∘ g) ∙ h)
    ≡⟨ cong (force ∘_) (cong (_∙ h) (cong (_∘ g) delay∙force)) ⟩
      force ∘ ((id ∘ g) ∙ h)
    ≡⟨ cong (force ∘_) (cong (_∙ h) identity∘ˡ) ⟩
      force ∘ (g ∙ h)
    ∎)
  force-Linear {q = ⊝} = sym assoc∘∘

  helper1 : forall {A : Ob p} {P : Ob +} {f : A ⇒ P}
    -> (wrap ∘ delay) ∙ f ≡ wrap ∘ (delay ∙ f)
    -> forall {B : Ob q} {h : ⇑ P ⇒ B} -> (h ∘ delay) ∙ f ≡ h ∘ (delay ∙ f)
  helper1 {f = f} e {h = h} =
    begin
      (h ∘ delay) ∙ f
    ≡˘⟨ cong (_∙ f) (cong (_∘ delay) ∘unwrap∙wrap) ⟩
      (((h ∘ unwrap) ∙ wrap) ∘ delay) ∙ f
    ≡⟨ cong (_∙ f) assoc∙∘ ⟩
      ((h ∘ unwrap) ∙ (wrap ∘ delay)) ∙ f
    ≡⟨ assoc∙∙ ⟩
      (h ∘ unwrap) ∙ ((wrap ∘ delay) ∙ f)
    ≡⟨ cong ((h ∘ unwrap) ∙_) e ⟩
      (h ∘ unwrap) ∙ (wrap ∘ (delay ∙ f))
    ≡˘⟨ assoc∙∘ ⟩
      ((h ∘ unwrap) ∙ wrap) ∘ (delay ∙ f)
    ≡⟨ cong (_∘ _) ∘unwrap∙wrap ⟩
      h ∘ (delay ∙ f)
    ∎

  assoc-wrap∘delay∙→Thunkable : forall {A : Ob p} {P : Ob +} {f : A ⇒ P}
    -> (wrap ∘ delay) ∙ f ≡ wrap ∘ (delay ∙ f)
    -> Thunkable f
  assoc-wrap∘delay∙→Thunkable e {r = +} = sym assoc∙∙
  assoc-wrap∘delay∙→Thunkable {f = f} e {r = ⊝} {g = g} {h = h} =
    begin
      h ∘ (g ∙ f)
    ≡˘⟨ cong (h ∘_) (cong (_∙ f) ∙force∘delay) ⟩
      h ∘ (((g ∙ force) ∘ delay) ∙ f)
    ≡⟨ cong (h ∘_) (helper1 e) ⟩
      h ∘ ((g ∙ force) ∘ (delay ∙ f))
    ≡˘⟨ assoc∘∘ ⟩
      (h ∘ (g ∙ force)) ∘ (delay ∙ f)
    ≡˘⟨ helper1 e ⟩
      ((h ∘ (g ∙ force)) ∘ delay) ∙ f
    ≡⟨ cong (_∙ f) assoc∘∘ ⟩
      (h ∘ ((g ∙ force) ∘ delay)) ∙ f
    ≡⟨ cong (_∙ f) (cong (h ∘_) ∙force∘delay) ⟩
      (h ∘ g) ∙ f
    ∎

  helper2 : forall {N : Ob ⊝} {A : Ob p} {f : N ⇒ A}
    -> f ∘ (unwrap ∙ force) ≡ (f ∘ unwrap) ∙ force
    -> forall {B : Ob q} {h : B ⇒ ⇓ N} -> f ∘ (unwrap ∙ h) ≡ (f ∘ unwrap) ∙ h
  helper2 {f = f} e {h = h} =
    begin
      f ∘ (unwrap ∙ h)
    ≡˘⟨ cong (f ∘_) (cong (unwrap ∙_) force∘delay∙) ⟩
      f ∘ (unwrap ∙ (force ∘ (delay ∙ h)))
    ≡˘⟨ cong (f ∘_) assoc∙∘ ⟩
      f ∘ ((unwrap ∙ force) ∘ (delay ∙ h))
    ≡˘⟨ assoc∘∘ ⟩
      (f ∘ (unwrap ∙ force)) ∘ (delay ∙ h)
    ≡⟨ cong (_∘ (delay ∙ h)) e ⟩
      ((f ∘ unwrap) ∙ force) ∘ (delay ∙ h)
    ≡⟨ assoc∙∘ ⟩
      (f ∘ unwrap) ∙ (force ∘ (delay ∙ h))
    ≡⟨ cong ((f ∘ unwrap) ∙_) force∘delay∙ ⟩
      (f ∘ unwrap) ∙ h
    ∎

  assoc-∘unwrap∙force→Linear : forall {N : Ob ⊝} {A : Ob p} {f : N ⇒ A}
    -> f ∘ (unwrap ∙ force) ≡ (f ∘ unwrap) ∙ force
    -> Linear f
  assoc-∘unwrap∙force→Linear {f = f} e {q = +} {g = g} {h = h} =
    begin
      f ∘ (g ∙ h)
    ≡˘⟨ cong (f ∘_) (cong (_∙ h) unwrap∙wrap∘) ⟩
      f ∘ ((unwrap ∙ (wrap ∘ g)) ∙ h)
    ≡⟨ cong (f ∘_) assoc∙∙ ⟩
      f ∘ (unwrap ∙ ((wrap ∘ g) ∙ h))
    ≡⟨ helper2 e ⟩
      (f ∘ unwrap) ∙ ((wrap ∘ g) ∙ h)
    ≡˘⟨ assoc∙∙ ⟩
      ((f ∘ unwrap) ∙ (wrap ∘ g)) ∙ h
    ≡˘⟨ cong (_∙ h) assoc∙∘ ⟩
      (((f ∘ unwrap) ∙ wrap) ∘ g) ∙ h
    ≡⟨ cong (_∙ h) (cong (_∘ g) ∘unwrap∙wrap) ⟩
      (f ∘ g) ∙ h
    ∎
  assoc-∘unwrap∙force→Linear e {q = ⊝} = sym assoc∘∘

max_stars_repo_name: elpinal/duploids

max_issues_repo_name: elpinal/duploids

max_forks_repo_name: elpinal/duploids


text:
{- Kleisli category for a monad. -}
module CategoryTheory.Instances.Kleisli where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad

open Category

-- Kleisli category from a category ℂ and a monad on ℂ
Kleisli : ∀{n} -> (ℂ : Category n) -> Monad ℂ -> Category n
Kleisli ℂ M = record
    { obj = ℂ.obj
    ; _~>_ = λ A B → A ℂ.~> T B
    ; id = λ {A} → η.at A
    ; _∘_ = λ {A}{B}{C} g f → (μ.at C ℂ.∘ fmap g) ℂ.∘ f
    ; _≈_ = ℂ._≈_
    ; id-left = λ {A} {B} {f} → ℂ.≈-cong-left (η-unit2 {B}) ℂ.≈> ℂ.id-left
    ; id-right = id-right-K
    ; ∘-assoc = ∘-assoc-K
    ; ≈-equiv = ℂ.≈-equiv
    ; ≈-cong = λ p1 p2 → ℂ.≈-cong-right p1 ℂ.≈> ℂ.≈-cong-left (ℂ.≈-cong-right (fmap-cong p2))
    }
    where
    private module ℂ = Category ℂ
    open Monad M renaming (T to F)
    open Functor F renaming (omap to T)

    id-right-K : {A B : ℂ.obj} {f : A ℂ.~> T B} → (μ.at B ℂ.∘ fmap f) ℂ.∘ η.at A ℂ.≈ f
    id-right-K {A}{B}{f}=
        ℂ.begin
            (μ.at B ℂ.∘ fmap f) ℂ.∘ η.at A
        ℂ.≈⟨ ℂ.∘-assoc ⟩
            μ.at B ℂ.∘ (fmap f ℂ.∘ η.at A)
        ℂ.≈⟨ ℂ.≈-cong-right η.nat-cond ℂ.≈> ℂ.∘-assoc ℂ.[sym] ⟩
            (μ.at B ℂ.∘ η.at (T B)) ℂ.∘ f
        ℂ.≈⟨ ℂ.≈-cong-left (η-unit1) ℂ.≈> ℂ.id-left ⟩
            f
        ℂ.∎
    ∘-assoc-K : {A B C D : ℂ.obj} {f : C ℂ.~> T D} {g : B ℂ.~> T C} {h : A ℂ.~> T B} →
          (μ.at D ℂ.∘ fmap ((μ.at D ℂ.∘ fmap f) ℂ.∘ g)) ℂ.∘ h ℂ.≈
          (μ.at D ℂ.∘ fmap f) ℂ.∘ ((μ.at C ℂ.∘ fmap g) ℂ.∘ h)
    ∘-assoc-K {A}{B}{C}{D}{f}{g}{h} =
        ℂ.begin
            (μ.at D ℂ.∘ fmap ((μ.at D ℂ.∘ fmap f) ℂ.∘ g)) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.≈-cong-right fmap-∘) ⟩
            (μ.at D ℂ.∘ (fmap (μ.at D ℂ.∘ fmap f) ℂ.∘ fmap g)) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.≈-cong-right (ℂ.≈-cong-left fmap-∘)) ⟩
            (μ.at D ℂ.∘ ((fmap (μ.at D) ℂ.∘ fmap (fmap f)) ℂ.∘ fmap g)) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.∘-assoc ℂ.[sym]) ℂ.≈> ℂ.≈-cong-left (ℂ.≈-cong-left (ℂ.∘-assoc ℂ.[sym])) ⟩
            (((μ.at D ℂ.∘ fmap (μ.at D)) ℂ.∘ fmap (fmap f)) ℂ.∘ fmap g) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.≈-cong-left (ℂ.≈-cong-left (μ-assoc ℂ.[sym]))) ⟩
            (((μ.at D ℂ.∘ μ.at (T D)) ℂ.∘ fmap (fmap f)) ℂ.∘ fmap g) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.≈-cong-left (ℂ.∘-assoc)) ⟩
            ((μ.at D ℂ.∘ (μ.at (T D) ℂ.∘ fmap (fmap f))) ℂ.∘ fmap g) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.≈-cong-left (ℂ.≈-cong-right (μ.nat-cond ℂ.[sym]))) ⟩
            ((μ.at D ℂ.∘ (fmap f ℂ.∘ μ.at C)) ℂ.∘ fmap g) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.≈-cong-left (ℂ.∘-assoc ℂ.[sym])) ⟩
            (((μ.at D ℂ.∘ fmap f) ℂ.∘ μ.at C) ℂ.∘ fmap g) ℂ.∘ h
        ℂ.≈⟨ ℂ.≈-cong-left (ℂ.∘-assoc) ℂ.≈> ℂ.∘-assoc ⟩
            (μ.at D ℂ.∘ fmap f) ℂ.∘ ((μ.at C ℂ.∘ fmap g) ℂ.∘ h)
        ℂ.∎

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Argument visibility used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Argument.Visibility where

open import Data.String as String using (String)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Re-exporting the builtins publically

open import Agda.Builtin.Reflection public using (Visibility)
open Visibility public

------------------------------------------------------------------------
-- Decidable equality

_≟_ : DecidableEquality Visibility
visible   ≟ visible   = yes refl
hidden    ≟ hidden    = yes refl
instance′ ≟ instance′ = yes refl
visible   ≟ hidden    = no λ()
visible   ≟ instance′ = no λ()
hidden    ≟ visible   = no λ()
hidden    ≟ instance′ = no λ()
instance′ ≟ visible   = no λ()
instance′ ≟ hidden    = no λ()


text:
module NotNot where

data ⊥ : Set where

Not : Set → Set
Not A = ⊥

Whoa : ∀ {A : Set} → Not (Not A) → A
Whoa ()

postulate
  -- Law of excluded middle.
  LEM : ∀ {A : Set} → Not (Not A) → A

Alright : ∀ {A : Set} → Not (Not A) → A
Alright p = LEM p

-- Constructive LEM requires hProp, hSet, Discrete, etc.

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.AbGroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.NAryOp
open import Cubical.Structures.Group hiding (⟨_⟩)

private
  variable
    ℓ : Level

abelian-group-axioms : (X : Type ℓ) → raw-group-structure X → Type ℓ
abelian-group-axioms X _·_ = group-axioms X _·_ ×
                             ((x y : X) → x · y ≡ y · x)

abelian-group-structure : Type ℓ → Type ℓ
abelian-group-structure = add-to-structure raw-group-structure abelian-group-axioms

AbGroup : Type (ℓ-suc ℓ)
AbGroup {ℓ} = TypeWithStr ℓ abelian-group-structure

abelian-group-iso : StrIso abelian-group-structure ℓ
abelian-group-iso = add-to-iso (nAryFunIso 2) abelian-group-axioms

abelian-group-axioms-isProp : (X : Type ℓ)
                           → (s : raw-group-structure X)
                           → isProp (abelian-group-axioms X s)
abelian-group-axioms-isProp X _·_ = isPropΣ (group-axioms-isProp X _·_)
                                    λ { ((isSetX , _) , _) → isPropΠ2 λ _ _ → isSetX _ _}

abelian-group-is-SNS : SNS {ℓ} abelian-group-structure abelian-group-iso
abelian-group-is-SNS = add-axioms-SNS _ abelian-group-axioms-isProp raw-group-is-SNS

AbGroupPath : (M N : AbGroup {ℓ}) → (M ≃[ abelian-group-iso ] N) ≃ (M ≡ N)
AbGroupPath = SIP abelian-group-is-SNS

-- Abelian group is group

AbGroup→Group : AbGroup {ℓ} → Group
AbGroup→Group (G , _·_ , isGroup , ·comm) = G , _·_ , isGroup

-- Abelian group extractors

⟨_⟩ : AbGroup {ℓ} → Type ℓ
⟨ G , _ ⟩ = G

module _ (G : AbGroup {ℓ}) where

  abgroup-operation = group-operation (AbGroup→Group G)

  abgroup-is-set = group-is-set (AbGroup→Group G)

  abgroup-assoc = group-assoc (AbGroup→Group G)

  abgroup-id = group-id (AbGroup→Group G)

  abgroup-rid = group-rid (AbGroup→Group G)

  abgroup-lid = group-lid (AbGroup→Group G)

  abgroup-inv = group-inv (AbGroup→Group G)

  abgroup-rinv = group-rinv (AbGroup→Group G)

  abgroup-linv = group-linv (AbGroup→Group G)

module abgroup-operation-syntax where

  abgroup-operation-syntax : (G : AbGroup {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
  abgroup-operation-syntax G = abgroup-operation G
  infixr 20 abgroup-operation-syntax
  syntax abgroup-operation-syntax G x y = x ·⟨ G ⟩ y

open abgroup-operation-syntax

abgroup-comm : (G : AbGroup {ℓ}) (x y : ⟨ G ⟩) → x ·⟨ G ⟩ y ≡ y ·⟨ G ⟩ x
abgroup-comm (_ , _ , _ , P) = P

-- AbGroup ·syntax

module abgroup-·syntax (G : AbGroup {ℓ}) where
  open group-·syntax (AbGroup→Group G) public


text:
-- Andreas, 2015-11-18, issue 1692 reported by m0davis

-- {-# OPTIONS -v tc.with.top:20 #-}

open import Common.Level
open import Common.Equality
open import Common.Product

postulate
  Key   : Set
  Value : Key → Set
  anyOf : ∀{A : Set} → A → A → A

data Tree : Set where
  node : (k : Key) (v : Value k) → Tree

data _∼_∈_ ( k : Key ) ( v : Value k ) : Tree → Set where
  here :  k ∼ v ∈ node k v

postulate
  k₁≡k₂ : ∀ ( k₁ k₂ : Key ) → k₁ ≡ k₂
  ∈→v₁≡v₂ : ∀ { k } { v₁ v₂ : Value k } → k ∼ v₁ ∈ node k v₂ → v₁ ≡ v₂

lem : ( t₁ t₂ : Tree )
      ( t₁→t₂ : ∀ {k} {v : Value k} → k ∼ v ∈ t₁ → k ∼ v ∈ t₂ )
      ( t₂→t₁ : ∀ {k} {v : Value k} → k ∼ v ∈ t₂ → k ∼ v ∈ t₁ ) →
      ∃ λ t → ∀ {k} {v : Value k} → k ∼ v ∈ t → k ∼ v ∈ t
lem (node k₁ v₁) (node k₂ v₂) t₁→t₂ t₂→t₁ rewrite k₁≡k₂ k₁ k₂
     | ∈→v₁≡v₂ (t₁→t₂ here) -- equivalent to v₂ ≡ v₁
     = _ , anyOf t₁→t₂ t₂→t₁

-- PROBLEM WAS:

-- When the second rewrite expression is commented-out, then we get the following types:
   {-
     t₂→t₁    : {k : Key} {v : Value k} →
                k ∼ v ∈ node k₂ v₂ → k ∼ v ∈ node k₂ v₁
     t₁→t₂    : {k : Key} {v : Value k} →
                k ∼ v ∈ node k₂ v₁ → k ∼ v ∈ node k₂ v₂
   -}
-- With both rewrite expressions, we get:
   {-
     t₂→t₁    : {k : Key} {v : Value k} →
                k ∼ v ∈ node k₂ v₂ → k ∼ v ∈ node k₂ v₂
     t₁→t₂    : {k : Key} {v : Value k} →
                k ∼ v ∈ node k₂ v₁ → k ∼ v ∈ node k₂ v₂
   -}
-- The unexpected behavior here is that v₁ has been rewritten to v₂ in t₂→t₁ but not in t₁→t₂.

-- Should be symmetric now, test case passes.

-- Dual case:

lem′ : ( t₁ t₂ : Tree )
      ( t₁→t₂ : ∀ {k} {v : Value k} → k ∼ v ∈ t₁ → k ∼ v ∈ t₂ )
      ( t₂→t₁ : ∀ {k} {v : Value k} → k ∼ v ∈ t₂ → k ∼ v ∈ t₁ ) →
      ∃ λ t → ∀ {k} {v : Value k} → k ∼ v ∈ t → k ∼ v ∈ t
lem′ (node k₁ v₁) (node k₂ v₂) t₁→t₂ t₂→t₁ rewrite k₁≡k₂ k₁ k₂
     | ∈→v₁≡v₂ (t₂→t₁ here) -- equivalent to v₁ ≡ v₂
     = _ , anyOf t₁→t₂ t₂→t₁


text:
------------------------------------------------------------------------
-- The rec construction can be encoded using λ-terms
------------------------------------------------------------------------

module Recursion-without-rec where

open import Equality.Propositional.Cubical
open import Prelude hiding (id; swap)

import Finite-subset.Listed equality-with-paths as S

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Alpha-equivalence χ-ℕ-atoms
open import Chi               χ-ℕ-atoms
open import Compatibility     χ-ℕ-atoms
open import Constants         χ-ℕ-atoms
open import Free-variables    χ-ℕ-atoms
open import Reasoning         χ-ℕ-atoms
open import Substitution      χ-ℕ-atoms
open import Values            χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

open import Combinators using (id; id-closed)

private
  variable
    A           : Type
    R           : A → A → Type
    x y z z₁ z₂ : Var
    e e′ v      : Exp

------------------------------------------------------------------------
-- "Plain" lambda terms

-- A predicate that holds for plain lambda terms, i.e. terms that are
-- built up using only var, lambda and apply.

Plain : Exp → Type
Plain (var _)       = ⊤
Plain (lambda _ e)  = Plain e
Plain (apply e₁ e₂) = Plain e₁ × Plain e₂
Plain (case _ _)    = ⊥
Plain (rec _ _)     = ⊥
Plain (const _ _)   = ⊥

-- Plain is preserved by substitutions.

plain-subst : ∀ e → Plain e → Plain e′ → Plain (e [ x ← e′ ])
plain-subst (apply e₁ e₂) (e₁-ok , e₂-ok) e′-ok =
  plain-subst e₁ e₁-ok e′-ok , plain-subst e₂ e₂-ok e′-ok
plain-subst {x = x} (lambda y e) e-ok e′-ok with x V.≟ y
… | yes _ = e-ok
… | no _  = plain-subst e e-ok e′-ok
plain-subst {x = x} (var y) _ e′-ok with x V.≟ y
… | yes _ = e′-ok
… | no _  = _

------------------------------------------------------------------------
-- A variant of a fixpoint combinator

-- A variant of the call-by-value fixpoint combinator Θᵥ that (at the
-- time of writing) is presented on the Wikipedia page about
-- fixed-point combinators
-- (https://en.wikipedia.org/wiki/Fixed-point_combinator). There Θᵥ is
-- defined to be the application of λxy.y(λz.xxyz) to itself. I have
-- dropped the final z, and made the choice of variable name for z
-- customisable.

mutual

  F : Var → Exp
  F z = apply (f z) (f z)

  f : Var → Exp
  f z =
    lambda v-x (lambda v-y (
      apply (var v-y) (
        lambda z (
          apply (apply (var v-x) (var v-x)) (var v-y)))))

-- The expressions f z, F z and id are closed.

f-closed : Closed (f z)
f-closed =
  Closed′-closed-under-lambda $
  Closed′-closed-under-lambda $
  Closed′-closed-under-apply
    (from-⊎ (closed′? (var v-y) (v-y ∷ v-x ∷ [])))
    (Closed′-closed-under-lambda $
     Closed′-closed-under-apply
       (Closed′-closed-under-apply
          (Closed′-closed-under-var (inj₂ (inj₂ (inj₁ refl))))
          (Closed′-closed-under-var (inj₂ (inj₂ (inj₁ refl)))))
       (Closed′-closed-under-var (inj₂ (inj₁ refl))))

F-closed : Closed (F z)
F-closed = Closed′-closed-under-apply f-closed f-closed

-- F z₁ and f z₁ are α-equivalent to F z₂ and f z₂, respectively,
-- assuming that z₁ and z₂ are distinct from v-x and v-y.

f≈αf :
  z₁ ≢ v-x → z₁ ≢ v-y → z₂ ≢ v-x → z₂ ≢ v-y →
  Alpha R (f z₁) (f z₂)
f≈αf {z₁ = z₁} {z₂ = z₂} {R = R} z₁≢x z₁≢y z₂≢x z₂≢y =
  lambda (
  lambda (
  apply (var y∼y₁) (
  lambda (
  apply (
  apply (var x∼x) (var x∼x)) (
  var y∼y₂)))))
  where
  x∼x : (R [ v-x ∼ v-x ] [ v-y ∼ v-y ] [ z₁ ∼ z₂ ]) v-x v-x
  x∼x = inj₂ (z₁≢x , z₂≢x , inj₂ ((λ ()) , (λ ()) , inj₁ (refl , refl)))

  y∼y₁ : (R [ v-x ∼ v-x ] [ v-y ∼ v-y ]) v-y v-y
  y∼y₁ = inj₁ (refl , refl)

  y∼y₂ : (R [ v-x ∼ v-x ] [ v-y ∼ v-y ] [ z₁ ∼ z₂ ]) v-y v-y
  y∼y₂ = inj₂ (z₁≢y , z₂≢y , y∼y₁)

F≈αF :
  z₁ ≢ v-x → z₁ ≢ v-y → z₂ ≢ v-x → z₂ ≢ v-y →
  Alpha R (F z₁) (F z₂)
F≈αF z₁≢x z₁≢y z₂≢x z₂≢y =
  apply (f≈αf z₁≢x z₁≢y z₂≢x z₂≢y) (f≈αf z₁≢x z₁≢y z₂≢x z₂≢y)

------------------------------------------------------------------------
-- A plain alternative to rec

-- An expression former that has the same semantics as rec, but that
-- takes plain expressions to plain expressions.
--
-- Note that substitution does not necessarily behave in the same way
-- for plain-rec as for rec (see below).

plain-rec : Var → Exp → Exp
plain-rec x e =
  let z , _ = fresh′ (S.from-List (v-x ∷ v-y ∷ [])) e in
  apply (lambda z (apply (F z) (lambda x (e [ x ← apply (var x) id ]))))
    id

-- If e is a plain lambda term, then plain-rec x e is a plain
-- lambda term.

plain-rec-plain : ∀ e → Plain e → Plain (plain-rec x e)
plain-rec-plain e ok = (_ , plain-subst e ok _) , _

-- The semantic rule given for rec is admissible for plain-rec.

plain-rec-⇓ :
  ∀ e → e [ x ← plain-rec x e ] ⇓ v → plain-rec x e ⇓ v
plain-rec-⇓ {x = x} {v = v} e ⇓v =
  plain-rec x e                                                         ⟶⟨⟩

  apply (lambda z′
           (apply (F z′) (lambda x (e [ x ← apply (var x) id ]))))
    id                                                                  ⟶⟨ apply lambda lambda ⟩

  apply (F z′) (lambda x (e [ x ← apply (var x) id ])) [ z′ ← id ]      ≡⟨ subst-∉ z′ _ z∉apply ⟩⟶

  apply (F z′) (lambda x (e [ x ← apply (var x) id ]))                  ⟶⟨ []⇓ (apply← ∙) F⇓ ⟩

  apply (lambda v-y
           (apply (var v-y) (lambda z′ (apply (F z′) (var v-y)))))
    (lambda x (e [ x ← apply (var x) id ]))                             ⟶⟨ apply lambda lambda ⟩

  apply (var v-y) (lambda z′ (apply (F z′) (var v-y)))
    [ v-y ← lambda x (e [ x ← apply (var x) id ]) ]                     ≡⟨ cong (apply _) (lambda-step-≢ y≢z) ⟩⟶

  apply (lambda x (e [ x ← apply (var x) id ]))
    (lambda z′ (apply (F z′) (lambda x (e [ x ← apply (var x) id ]))))  ⟶⟨ apply lambda lambda ⟩

  e [ x ← apply (var x) id ]
    [ x ← lambda z′
            (apply (F z′) (lambda x (e [ x ← apply (var x) id ]))) ]    ≡⟨ fusion e ⟩⟶

  e [ x ← apply (var x) id
            [ x ← lambda z′
                    (apply (F z′)
                       (lambda x (e [ x ← apply (var x) id ]))) ] ]     ≡⟨ cong₂ (λ e₁ e₂ → e [ x ← apply e₁ e₂ ])
                                                                             (var-step-≡ (refl {x = x}))
                                                                             (subst-closed x _ id-closed) ⟩⟶

  e [ x ← plain-rec x e ]                                               ⇓⟨ ⇓v ⟩■

  v
  where
  z,f = fresh′ (S.from-List (v-x ∷ v-y ∷ [])) e

  z′ : Var
  z′ = proj₁ z,f

  z∉e : ¬ z′ ∈FV e
  z∉e = proj₁ (proj₂ z,f)

  x≢z : v-x ≢ z′
  x≢z x≡z = proj₂ (proj₂ z,f) (S.≡→∈∷ (sym x≡z))

  y≢z : v-y ≢ z′
  y≢z y≡z = proj₂ (proj₂ z,f) (S.∈→∈∷ (S.≡→∈∷ (sym y≡z)))

  F⇓ :
    F z′ ⇓
    lambda v-y (apply (var v-y) (lambda z′ (apply (F z′) (var v-y))))
  F⇓ =
    apply lambda lambda
      (lambda v-y
         (apply (var v-y)
            (lambda z′ (apply (apply (var v-x) (var v-x)) (var v-y))))
         [ v-x ← f z′ ]                                                   ⟶⟨⟩

       lambda v-y
         (apply (var v-y)
            (lambda z′ (apply (apply (var v-x) (var v-x)) (var v-y))
               [ v-x ← f z′ ]))                                           ≡⟨ cong (lambda _) $ cong (apply _) $
                                                                             lambda-step-≢ x≢z ⟩⟶

       lambda v-y (apply (var v-y) (lambda z′ (apply (F z′) (var v-y))))  ■⟨ lambda _ _ ⟩)

  z∉apply :
    ¬ z′ ∈FV apply (F z′) (lambda x (e [ x ← apply (var x) id ]))
  z∉apply (apply-left z∈Fz) =
    F-closed z′ (λ ()) z∈Fz
  z∉apply (apply-right (lambda z≢x z∈)) with subst-∈FV x e z∈
  … | inj₁ (z∈e , _)              = z∉e z∈e
  … | inj₂ (apply-left (var z≡x)) = z≢x z≡x
  … | inj₂ (apply-right z∈id)     = id-closed z′ (λ ()) z∈id

-- Substitution of closed expressions is not in general defined in the
-- same way for plain-rec as for rec.

¬-plain-rec-subst :
  ¬ (∀ y e x e′ →
     Closed e′ →
     plain-rec y e [ x ← e′ ] ≡
     plain-rec y (if x V.≟ y then e else e [ x ← e′ ]))
¬-plain-rec-subst plain-rec-subst =
  not-equal (plain-rec-subst y′ e₁ x′ e₂ id-closed)
  where
  y′ = v-y
  x′ = v-z
  e₂ = id
  e₁ = var x′

  not-equal :
    plain-rec y′ e₁ [ x′ ← e₂ ] ≢
    plain-rec y′ (if x′ V.≟ y′ then e₁ else e₁ [ x′ ← e₂ ])
  not-equal ()

-- However, it is defined in the same way /up to α-equivalence/.

plain-rec-subst :
  ∀ x →
  Closed e′ →
  plain-rec y e [ x ← e′ ] ≈α
  plain-rec y (if x V.≟ y then e else e [ x ← e′ ])
plain-rec-subst {e′ = e′} {y = y} {e = e} x cl-e′ =
  apply (lambda z¹
           (apply (F z¹) (lambda y (e [ y ← apply (var y) id ]))))
    id [ x ← e′ ]                                                   ≡⟨ cong (apply _) $
                                                                       subst-closed x _ id-closed ⟩α
  apply (lambda z¹
           (apply (F z¹) (lambda y (e [ y ← apply (var y) id ])))
           [ x ← e′ ])
    id                                                              ≡⟨ cong (λ e → apply (lambda z¹ e) id) $
                                                                       lemma₁ (x V.≟ z¹) (x V.≟ y) ⟩α
  apply (lambda z¹
           (apply (F z¹)
              (lambda y ((if x V.≟ y then e else e [ x ← e′ ])
                           [ y ← apply (var y) id ]))))
    id                                                              ≈⟨ apply (lambda (apply (F≈αF z¹≢x z¹≢y z²≢x z²≢y)
                                                                                (refl-Alpha _ lemma₂)))
                                                                         refl-α ⟩α∎
  apply (lambda z²
           (apply (F z²)
              (lambda y ((if x V.≟ y then e else e [ x ← e′ ])
                           [ y ← apply (var y) id ]))))
    id                                                              ∎
  where
  z¹,f₁ = fresh′ (S.from-List (v-x ∷ v-y ∷ [])) e

  z¹ : Var
  z¹ = proj₁ z¹,f₁

  z¹∉e : ¬ z¹ ∈FV e
  z¹∉e = proj₁ (proj₂ z¹,f₁)

  z¹≢x : z¹ ≢ v-x
  z¹≢x z¹≡x = proj₂ (proj₂ z¹,f₁) (S.≡→∈∷ z¹≡x)

  z¹≢y : z¹ ≢ v-y
  z¹≢y z¹≡y = proj₂ (proj₂ z¹,f₁) (S.∈→∈∷ (S.≡→∈∷ z¹≡y))

  z²,f₂ =
    fresh′ (S.from-List (v-x ∷ v-y ∷ []))
      (if x V.≟ y then e else e [ x ← e′ ])

  z² : Var
  z² = proj₁ z²,f₂

  z²∉ : ¬ z² ∈FV if x V.≟ y then e else e [ x ← e′ ]
  z²∉ = proj₁ (proj₂ z²,f₂)

  z²≢x : z² ≢ v-x
  z²≢x z²≡x = proj₂ (proj₂ z²,f₂) (S.≡→∈∷ z²≡x)

  z²≢y : z² ≢ v-y
  z²≢y z²≡y = proj₂ (proj₂ z²,f₂) (S.∈→∈∷ (S.≡→∈∷ z²≡y))

  x∉y-id : x ≢ y → ¬ x ∈FV apply (var y) id
  x∉y-id x≢y (apply-left (var x≡y)) = x≢y x≡y
  x∉y-id _   (apply-right x∈id)     = id-closed x (λ ()) x∈id

  lemma₁ :
    (x≟z¹ : Dec (x ≡ z¹)) (x≟y : Dec (x ≡ y)) →
    if x≟z¹
    then apply (F z¹) (lambda y (e [ y ← apply (var y) id ]))
    else apply (F z¹) (lambda y (e [ y ← apply (var y) id ]))
           [ x ← e′ ] ≡
    apply (F z¹)
      (lambda y ((if x≟y then e else e [ x ← e′ ])
                   [ y ← apply (var y) id ]))
  lemma₁ (yes _) (yes _) = refl

  lemma₁ (yes x≡z¹) (no _) =
    apply (F z¹) (lambda y (e [ y ← apply (var y) id ]))             ≡⟨ cong (apply _) $ cong (lambda _) $ cong (_[ _ ← _ ]) $ sym $
                                                                        subst-∉ x e (z¹∉e ∘ subst (_∈FV _) x≡z¹) ⟩∎
    apply (F z¹) (lambda y (e [ x ← e′ ] [ y ← apply (var y) id ]))  ∎

  lemma₁ (no _) (yes x≡y) =
    apply (F z¹ [ x ← e′ ])
      (lambda y (e [ y ← apply (var y) id ]) [ x ← e′ ])             ≡⟨ cong (λ e″ → apply e″ (lambda y (e [ y ← apply (var y) id ])
                                                                                [ x ← e′ ])) $
                                                                        subst-closed x e′ F-closed ⟩

    apply (F z¹) (lambda y (e [ y ← apply (var y) id ]) [ x ← e′ ])  ≡⟨ cong (apply (F z¹)) $
                                                                        lambda-step-≡ x≡y ⟩∎
    apply (F z¹) (lambda y (e [ y ← apply (var y) id ]))             ∎

  lemma₁ (no _) (no x≢y) =
    apply (F z¹ [ x ← e′ ])
      (lambda y (e [ y ← apply (var y) id ]) [ x ← e′ ])             ≡⟨ cong (λ e″ → apply e″ (lambda y (e [ y ← apply (var y) id ])
                                                                                [ x ← e′ ])) $
                                                                        subst-closed x e′ F-closed ⟩

    apply (F z¹) (lambda y (e [ y ← apply (var y) id ]) [ x ← e′ ])  ≡⟨ cong (apply (F z¹)) $
                                                                        lambda-step-≢ x≢y ⟩

    apply (F z¹) (lambda y (e [ y ← apply (var y) id ] [ x ← e′ ]))  ≡⟨ cong (apply _) $ cong (lambda _) $ sym $
                                                                        swap x≢y (x∉y-id x≢y) (cl-e′ _ (λ ())) e ⟩∎
    apply (F z¹) (lambda y (e [ x ← e′ ] [ y ← apply (var y) id ]))  ∎

  lemma₂ :
    ∀ z →
    z ∈FV lambda y ((if x V.≟ y then e else e [ x ← e′ ])
                      [ y ← apply (var y) id ]) →
    (_≡_ [ z¹ ∼ z² ]) z z
  lemma₂ z (lambda z≢y z∈) =
    case subst-∈FV y _ z∈ of λ where
      (inj₁ (z∈ , _)) →
        inj₂ ( z¹≢ (x V.≟ y) z∈
             , z²∉ ∘ flip (subst (_∈FV _)) z∈ ∘ sym
             , refl
             )

      (inj₂ (apply-left (var z≡y))) →
        ⊥-elim $ z≢y z≡y

      (inj₂ (apply-right ∈id)) →
        ⊥-elim $ id-closed _ (λ ()) ∈id
    where
    z¹≢ :
      ∀ x≟y →
      z ∈FV if x≟y then e else e [ x ← e′ ] →
      z¹ ≢ z
    z¹≢ (yes _) z∈ = z¹∉e ∘ flip (subst (_∈FV _)) z∈ ∘ sym
    z¹≢ (no _)  z∈ = case subst-∈FV x e z∈ of λ where
      (inj₁ (z∈ , _)) →
        z¹∉e ∘ flip (subst (_∈FV _)) z∈ ∘ sym
      (inj₂ z∈e′) →
        ⊥-elim $ cl-e′ _ (λ ()) z∈e′

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
-- TODO
-- Basic Tarski-style semantics, for soundness only.

module BasicT.Semantics.BasicTarski where

open import BasicT.Syntax.Common public

-- Tarski models.

record Model : Set₁ where
  infix 3 ⊩ᵅ_
  field
    -- Forcing for atomic propositions.
    ⊩ᵅ_ : Atom → Set

open Model {{…}} public

-- Forcing in a particular model.

module _ {{_ : Model}} where
  infix 3 ⊩_
  ⊩_ : Ty → Set
  ⊩ α P   = ⊩ᵅ P
  ⊩ A ▻ B = ⊩ A → ⊩ B
  ⊩ A ∧ B = ⊩ A × ⊩ B
  ⊩ ⊤    = 𝟙
  ⊩ BOOL  = 𝔹
  ⊩ NAT   = ℕ

  infix 3 ⊩⋆_
  ⊩⋆_ : Cx Ty → Set
  ⊩⋆ ∅     = 𝟙
  ⊩⋆ Ξ , A = ⊩⋆ Ξ × ⊩ A

-- Entailment, or forcing in all models.

infix 3 ⊨_
⊨_ : Ty → Set₁
⊨ A = ∀ {{_ : Model}} → ⊩ A

-- Forcing in a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 ⊩_⇒_
  ⊩_⇒_ : Cx Ty → Ty → Set
  ⊩ Γ ⇒ A = ⊩⋆ Γ → ⊩ A

  infix 3 ⊩_⇒⋆_
  ⊩_⇒⋆_ : Cx Ty → Cx Ty → Set
  ⊩ Γ ⇒⋆ Ξ = ⊩⋆ Γ → ⊩⋆ Ξ

-- Entailment, or forcing in all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} → ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} → ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ} → A ∈ Γ → ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

  ⟦λ⟧ : ∀ {A B Γ} → ⊩ Γ , A ⇒ B → ⊩ Γ ⇒ A ▻ B
  ⟦λ⟧ f γ = λ a → f (γ , a)

  _⟦$⟧_ : ∀ {A B Γ} → ⊩ Γ ⇒ A ▻ B → ⊩ Γ ⇒ A → ⊩ Γ ⇒ B
  (f ⟦$⟧ g) γ = f γ $ g γ

  ⟦S⟧ : ∀ {A B C Γ} → ⊩ Γ ⇒ A ▻ B ▻ C → ⊩ Γ ⇒ A ▻ B → ⊩ Γ ⇒ A → ⊩ Γ ⇒ C
  ⟦S⟧ f g a γ = S (f γ) (g γ) (a γ)

  _⟦,⟧_ : ∀ {A B Γ} → ⊩ Γ ⇒ A → ⊩ Γ ⇒ B → ⊩ Γ ⇒ A ∧ B
  (a ⟦,⟧ b) γ = a γ , b γ

  ⟦π₁⟧ : ∀ {A B Γ} → ⊩ Γ ⇒ A ∧ B → ⊩ Γ ⇒ A
  ⟦π₁⟧ s γ = π₁ (s γ)

  ⟦π₂⟧ : ∀ {A B Γ} → ⊩ Γ ⇒ A ∧ B → ⊩ Γ ⇒ B
  ⟦π₂⟧ s γ = π₂ (s γ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
open import Agda.Primitive

record Setoid (a : Level) : Set₁ where
  constructor mk
  field
    carrier : Set

record HeytingAlgebra {a} (setoid : Setoid a) (A : Set) : Set a where
  constructor laws
  open Setoid setoid
  field ∧-cong : carrier

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Bottom where

open import Common.FOL.FOL-Eq

postulate bot : ⊥

postulate
  zero : D
  succ : D → D

postulate false : zero ≡ succ zero
{-# ATP prove false bot #-}

-- $ apia -isrc -inotes/papers/FoSSaCS-2012/  notes/papers/FoSSaCS-2012/Bottom.agda
-- Proving the conjecture in /tmp/Bottom/16-false.tptp ...
-- Vampire 0.6 (revision 903) proved the conjecture in /tmp/Bottom/16-false.tptp

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Unit tests for Tactic.By.Parametrised
------------------------------------------------------------------------

-- Nothing is exported from this module.

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

open import Equality

module Tactic.By.Parametrised.Tests
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Maybe eq
open import Monad eq
open import TC-monad eq hiding (Type)

open import Tactic.By.Parametrised eq

------------------------------------------------------------------------
-- Some unit tests

private

  module Tests
    (assumption : 48 ≡ 42)
    (lemma      : ∀ n → n + 8 ≡ n + 2)
    (f          : ℕ → ℕ → ℕ → ℕ)
    where

    g : ℕ → ℕ → ℕ → ℕ
    g zero    _ _ = 12
    g (suc _) _ _ = 12

    fst : ∀ {a b} {A : Type a} {B : A → Type b} →
          Σ A B → A
    fst = proj₁

    {-# NOINLINE fst #-}

    record R (F : Type → Type) : Type₁ where
      field
        p : {A : Type} {x : F A} → x ≡ x

    open R ⦃ … ⦄ public

    test₁ : ⟨ 40 + 2 ⟩ ≡ 42
    test₁ = ⟨by⟩ refl

    test₂ : 48 ≡ 42 → ⟨ 42 ⟩ ≡ 48
    test₂ eq = ⟨by⟩ eq

    test₃ : (f : ℕ → ℕ) → f ⟨ 42 ⟩ ≡ f 48
    test₃ f = ⟨by⟩ assumption

    test₄ : (f : ℕ → ℕ) → f ⟨ 48 ⟩ ≡ f 42
    test₄ f = ⟨by⟩ assumption

    test₅ : (f : ℕ → ℕ → ℕ) → f ⟨ 42 ⟩ ⟨ 42 ⟩ ≡ f 48 48
    test₅ f = ⟨by⟩ assumption

    test₆ : (f : ℕ → ℕ → ℕ → ℕ) → f ⟨ 48 ⟩ 45 ⟨ 48 ⟩ ≡ f 42 45 42
    test₆ f = ⟨by⟩ assumption

    test₇ : f ⟨ 48 ⟩ (f ⟨ 48 ⟩ 45 ⟨ 48 ⟩) ⟨ 48 ⟩ ≡ f 42 (f 42 45 42) 42
    test₇ = ⟨by⟩ assumption

    test₈ : ∀ n → g n (g n 45 ⟨ 48 ⟩) ⟨ 48 ⟩ ≡ g n (g n 45 42) 42
    test₈ n = ⟨by⟩ assumption

    test₉ : (f : ℕ → ℕ) → f ⟨ 42 ⟩ ≡ f 48
    test₉ f = ⟨by⟩ (lemma 40)

    test₁₀ : (f : ℕ → ℕ) → f ⟨ 42 ⟩ ≡ f 48
    test₁₀ f = ⟨by⟩ (λ (_ : ⊤) → assumption)

    test₁₁ : (f : ℕ × ℕ → ℕ × ℕ) → (∀ x → ⟨ _≡_ ⟩ (f x) x) →
             fst ⟨ f (12 , 73) ⟩ ≡ fst {B = λ _ → ℕ} (12 , 73)
    test₁₁ _ hyp = ⟨by⟩ hyp

    test₁₂ : (h : ℕ → Maybe ℕ) →
             ((xs : ℕ) → h xs ≡ just xs) →
             (xs : ℕ) → suc ⟨$⟩ h xs ≡ suc ⟨$⟩ return xs
    test₁₂ h hyp xs =
      suc ⟨$⟩ ⟨ h xs ⟩   ≡⟨ ⟨by⟩ (hyp xs) ⟩∎
      suc ⟨$⟩ return xs  ∎

    test₁₃ : (h : List ⊤ → Maybe (List ⊤)) →
             ((xs : List ⊤) → h xs ≡ just xs) →
             (x : ⊤) (xs : List ⊤) → _
    test₁₃ h hyp x xs =
      _∷_ ⟨$⟩ return x ⊛ ⟨ h xs ⟩   ≡⟨ ⟨by⟩ (hyp xs) ⟩∎
      _∷_ ⟨$⟩ return x ⊛ return xs  ∎

    test₁₄ : (h : List ℕ → Maybe (List ℕ)) →
             ((xs : List ℕ) → h xs ≡ just xs) →
             (x : ℕ) (xs : List ℕ) → _
    test₁₄ h hyp x xs =
      _∷_ ⟨$⟩ ⟨ h xs ⟩   ≡⟨ ⟨by⟩ (hyp xs) ⟩∎
      _∷_ ⟨$⟩ return xs  ∎

    test₁₅ :
      (F : Type → Type → Type)
      (G : Bool → Type → Type) →
      ((A : Type) → F (G false A) A ≡ G false (F A A)) →
      (A : Type) →
      G false (F (G false A) A) ≡
      G false (G false (F A A))
    test₁₅ F G hyp A =
      G false ⟨ F (G false A) A ⟩  ≡⟨ ⟨by⟩ hyp ⟩∎
      G false (G false (F A A))    ∎

    test₁₆ : 48 ≡ 42 →
             _≡_ {A = ℕ → ℕ} (λ x → x + ⟨ 42 ⟩) (λ x → x + 48)
    test₁₆ hyp = ⟨by⟩ hyp

    test₁₇ :
      (P : ℕ → Type)
      (f : ∀ {n} → P n → P n)
      (p : P 0) →
      f ⟨ subst P (refl _) p ⟩ ≡ f p
    test₁₇ _ _ _ = ⟨by⟩ subst-refl

    test₁₈ :
      (subst′ :
         ∀ {a p} {A : Type a} {x y : A}
         (P : A → Type p) → x ≡ y → P x → P y) →
      (∀ {a p} {A : Type a} {x : A} (P : A → Type p) (p : P x) →
       subst′ P (refl x) p ≡ p) →
      (P : ℕ → Type)
      (f : ∀ {n} → P n → P n)
      (p : P 0) →
      f ⟨ subst′ P (refl 0) p ⟩ ≡ f p
    test₁₈ _ subst′-refl _ _ _ = ⟨by⟩ subst′-refl

    -- test₁₉ :
    --   {F : Type → Type} ⦃ r : R F ⦄ {A : Type} {x₁ x₂ : F A}
    --   (p₁ p₂ : x₁ ≡ x₂) (assumption : p₁ ≡ p₂) →
    --   trans p p₁ ≡ trans p p₂
    -- test₁₉ p₁ p₂ assumption =
    --   trans p p₁      ≡⟨⟩
    --   trans p ⟨ p₁ ⟩  ≡⟨ ⟨by⟩ assumption ⟩∎
    --   trans p p₂      ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- A parametrised coinductive definition that can be used to define
-- strong and weak bisimilarity as well as expansion
------------------------------------------------------------------------

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

open import Prelude

open import Labelled-transition-system

module Bisimilarity.General
         {ℓ}
         (lts : LTS ℓ)
         (open LTS lts)
         (_[_]↝₁_ _[_]↝₂_ : Proc → Label → Proc → Type ℓ)
         (⟶→↝₁ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝₁ q)
         (⟶→↝₂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝₂ q)
         where

open import Equality.Propositional as Eq hiding (Extensionality)
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Bijection equality-with-J as Bijection using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Bisimilarity.Step lts _[_]↝₁_ _[_]↝₂_ as Step public
  using (StepC)
open import Indexed-container hiding (⟨_⟩; Bisimilarity)
open import Indexed-container.Combinators hiding (id; _∘_)
open import Relation
import Similarity.Step lts _[_]↝₁_ as Step₁
import Similarity.Step lts _[_]↝₂_ as Step₂

open Indexed-container public using (force)

------------------------------------------------------------------------
-- Bisimilarity

-- Bisimilarity. Note that this definition is small.

infix 4 _∼_ _∼′_ [_]_∼_ [_]_∼′_

Bisimilarity : Size → Rel₂ ℓ Proc
Bisimilarity = ν StepC

Bisimilarity′ : Size → Rel₂ ℓ Proc
Bisimilarity′ = ν′ StepC

[_]_∼_ : Size → Proc → Proc → Type ℓ
[_]_∼_ i = curry (Bisimilarity i)

[_]_∼′_ : Size → Proc → Proc → Type ℓ
[_]_∼′_ i = curry (Bisimilarity′ i)

_∼_ : Proc → Proc → Type ℓ
_∼_ = [ ∞ ]_∼_

_∼′_ : Proc → Proc → Type ℓ
_∼′_ = [ ∞ ]_∼′_

-- Bisimilarity is reflexive.

mutual

  reflexive-∼ : ∀ {p i} → [ i ] p ∼ p
  reflexive-∼ =
    StepC.⟨ (λ p⟶p′ → _ , ⟶→↝₁ p⟶p′ , reflexive-∼′)
          , (λ q⟶q′ → _ , ⟶→↝₂ q⟶q′ , reflexive-∼′)
          ⟩

  reflexive-∼′ : ∀ {p i} → [ i ] p ∼′ p
  force reflexive-∼′ = reflexive-∼

≡⇒∼ : ∀ {p q} → p ≡ q → p ∼ q
≡⇒∼ refl = reflexive-∼

-- Functions that can be used to aid the instance resolution
-- mechanism.

infix -2 ∼:_ ∼′:_

∼:_ : ∀ {i p q} → [ i ] p ∼ q → [ i ] p ∼ q
∼:_ = id

∼′:_ : ∀ {i p q} → [ i ] p ∼′ q → [ i ] p ∼′ q
∼′:_ = id

------------------------------------------------------------------------
-- Bisimilarity for bisimilarity

-- Bisimilarity of bisimilarity proofs.

infix 4 [_]_≡_ [_]_≡′_

[_]_≡_ : ∀ {p q} → Size → (_ _ : ν StepC ∞ (p , q)) → Type ℓ
[_]_≡_ i = curry (ν-bisimilar i)

[_]_≡′_ : ∀ {p q} → Size → (_ _ : ν′ StepC ∞ (p , q)) → Type ℓ
[_]_≡′_ i = curry (ν′-bisimilar i)

-- An alternative characterisation of bisimilarity of bisimilarity
-- proofs.

[]≡↔ :
  Eq.Extensionality ℓ ℓ →
  ∀ {p q} {i : Size} (p∼q₁ p∼q₂ : ν StepC ∞ (p , q)) →

  [ i ] p∼q₁ ≡ p∼q₂

    ↔

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
   let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
   in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)

[]≡↔ ext {p} {q} {i} p∼q₁@(s₁ , f₁) p∼q₂@(s₂ , f₂) =

  [ i ] p∼q₁ ≡ p∼q₂                                                    ↝⟨ ν-bisimilar↔ ext p∼q₁ p∼q₂ ⟩

  ⟦ StepC₁ ⟷ StepC₂ ⟧₂ (ν′-bisimilar i) (p∼q₁ , p∼q₂)                  ↝⟨ ⟦⟷⟧₂↔ ext StepC₁ StepC₂ (ν′-bisimilar i) p∼q₁ p∼q₂ ⟩

  ⟦ StepC₁ ⟧₂ (ν′-bisimilar i)
    ((proj₁ s₁ , f₁ ∘ inj₁) , (proj₁ s₂ , f₂ ∘ inj₁))
    ×
  ⟦ StepC₂ ⟧₂ (ν′-bisimilar i)
    ( (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p)))
    , (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p)))
    )                                                                  ↝⟨ Step₁.⟦StepC⟧₂↔ ext (ν′-bisimilar i) (proj₁ s₁ , f₁ ∘ inj₁)
                                                                                (proj₁ s₂ , f₂ ∘ inj₁)
                                                                            ×-cong
                                                                          Step₂.⟦StepC⟧₂↔ ext (ν′-bisimilar i)
                                                                            (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p)))
                                                                            (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p))) ⟩
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′∼q′₁ =
         Step₁.StepC.challenge (proj₁ s₁ , f₁ ∘ inj₁) p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ =
         Step₁.StepC.challenge (proj₁ s₂ , f₂ ∘ inj₁) p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  ((∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
   let p′₁ , p⟶p′₁ , p′∼q′₁ =
          Step₂.StepC.challenge
             (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p))) q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ =
          Step₂.StepC.challenge
             (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p))) q⟶q′
   in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂))  ↔⟨⟩

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
   let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
   in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)   □

  where
  open Container

  StepC₁ = Step₁.StepC
  StepC₂ = Step₂.StepC

module Bisimilarity-of-∼
         (ext : Eq.Extensionality ℓ ℓ)
         {p q} {i : Size}
         (p∼q₁ p∼q₂ : ν StepC ∞ (p , q))
         where

  -- A "constructor".

  ⟨_,_,_,_,_⟩ :
    (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
     let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
         q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
     in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
          subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
            ×
          [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂) →
    (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
     let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
         p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
     in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
          subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
            ×
          [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂) →
    [ i ] p∼q₁ ≡ p∼q₂
  ⟨_,_,_,_,_⟩ = curry (_↔_.from ([]≡↔ ext p∼q₁ p∼q₂))

  -- Some "projections".

  left-to-right :
    [ i ] p∼q₁ ≡ p∼q₂ →
    ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
    let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
        q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
    in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
         subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
           ×
         [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂
  left-to-right = proj₁ ∘ _↔_.to ([]≡↔ ext p∼q₁ p∼q₂)

  right-to-left :
    [ i ] p∼q₁ ≡ p∼q₂ →
    ∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
    let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
        p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
    in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
         subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
           ×
         [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂
  right-to-left = proj₂ ∘ _↔_.to ([]≡↔ ext p∼q₁ p∼q₂)

-- A statement of extensionality for bisimilarity.

Extensionality : Type ℓ
Extensionality = ν′-extensionality StepC

-- This form of extensionality can be used to derive another form
-- (in the presence of extensionality for functions).

extensionality :
  Eq.Extensionality ℓ ℓ →
  Extensionality →
  ∀ {p q} {p∼q₁ p∼q₂ : ν StepC ∞ (p , q)} →
  [ ∞ ] p∼q₁ ≡ p∼q₂ → p∼q₁ ≡ p∼q₂
extensionality ext ν-ext = ν-extensionality ext ν-ext

open StepC public using (⟨_,_⟩; left-to-right; right-to-left)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
------------------------------------------------------------------------
-- Some theory of Erased, developed using Cubical Agda
------------------------------------------------------------------------

-- This module instantiates and reexports code from Erased.

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Erased.Cubical
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Bijection equality-with-J using (_↔_)
import Bijection P.equality-with-J as PB
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
import Equivalence P.equality-with-J as PEq
import Erased.Basics as EB
import Erased.Level-1 P.equality-with-J as EP
import Erased.Level-1 equality-with-J as E
open import Function-universe equality-with-J

private
  variable
    a p : Level
    A   : Type a
    x y : A

------------------------------------------------------------------------
-- []-cong

-- Given an erased path from x to y there is a path from [ x ] to
-- [ y ].

[]-cong-Path :
  {@0 A : Type a} {@0 x y : A} →
  EB.Erased (x P.≡ y) → EB.[ x ] P.≡ EB.[ y ]
[]-cong-Path EB.[ eq ] = λ i → EB.[ eq i ]

-- []-cong-Path is an equivalence.

[]-cong-Path-equivalence :
  {@0 A : Type a} {@0 x y : A} →
  PEq.Is-equivalence ([]-cong-Path {x = x} {y = y})
[]-cong-Path-equivalence =
  PEq._≃_.is-equivalence $ PEq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { from = λ eq → EB.[ P.cong EB.erased eq ]
        }
      ; right-inverse-of = λ _ → P.refl
      }
    ; left-inverse-of = λ _ → P.refl
    })

-- A rearrangement lemma for []-cong-Path (which holds by definition).

[]-cong-Path-[refl] :
  {@0 A : Type a} {@0 x : A} →
  []-cong-Path EB.[ P.refl {x = x} ] P.≡ P.refl {x = EB.[ x ]}
[]-cong-Path-[refl] = P.refl

-- The []-cong axioms can be instantiated.

instance-of-[]-cong-axiomatisation-for-Path : EP.[]-cong-axiomatisation a
instance-of-[]-cong-axiomatisation-for-Path = λ where
  .EP.[]-cong-axiomatisation.[]-cong             → []-cong-Path
  .EP.[]-cong-axiomatisation.[]-cong-equivalence → []-cong-Path-equivalence
  .EP.[]-cong-axiomatisation.[]-cong-[refl]      → []-cong-Path-[refl]

-- Given an erased proof of equality of x and y one can show that
-- EB.[ x ] is equal to EB.[ y ].

[]-cong : {@0 A : Type a} {@0 x y : A} →
          EB.Erased (x ≡ y) → EB.[ x ] ≡ EB.[ y ]
[]-cong {x = x} {y = y} =
  EB.Erased (x ≡ y)      ↝⟨ (λ (EB.[ eq ]) → EB.[ _↔_.to ≡↔≡ eq ]) ⟩
  EB.Erased (x P.≡ y)    ↝⟨ []-cong-Path ⟩
  EB.[ x ] P.≡ EB.[ y ]  ↔⟨ inverse ≡↔≡ ⟩□
  EB.[ x ] ≡ EB.[ y ]    □

-- []-cong is an equivalence.

[]-cong-equivalence :
  {@0 A : Type a} {@0 x y : A} →
  Is-equivalence ([]-cong {x = x} {y = y})
[]-cong-equivalence {x = x} {y = y} = _≃_.is-equivalence (
  EB.Erased (x ≡ y)      ↔⟨ _≃_.from ↔≃↔ $
                            EP.[]-cong.Erased-cong-↔
                              instance-of-[]-cong-axiomatisation-for-Path
                              (_≃_.to ↔≃↔ ≡↔≡) ⟩
  EB.Erased (x P.≡ y)    ↝⟨ _↔_.from ≃↔≃ PEq.⟨ _ , []-cong-Path-equivalence ⟩ ⟩
  EB.[ x ] P.≡ EB.[ y ]  ↔⟨ inverse ≡↔≡ ⟩□
  EB.[ x ] ≡ EB.[ y ]    □)

-- A rearrangement lemma for []-cong.

[]-cong-[refl] :
  {@0 A : Type a} {@0 x : A} →
  []-cong EB.[ refl x ] ≡ refl EB.[ x ]
[]-cong-[refl] {x = x} =
  sym $ _↔_.to (from≡↔≡to Eq.⟨ _ , []-cong-equivalence ⟩) (
    EB.[ _↔_.from ≡↔≡ (P.cong EB.erased (_↔_.to ≡↔≡ (refl EB.[ x ]))) ]  ≡⟨ []-cong EB.[ sym cong≡cong ] ⟩
    EB.[ cong EB.erased (_↔_.from ≡↔≡ (_↔_.to ≡↔≡ (refl EB.[ x ]))) ]    ≡⟨ []-cong EB.[ cong (cong EB.erased) (_↔_.left-inverse-of ≡↔≡ _) ] ⟩
    EB.[ cong EB.erased (refl EB.[ x ]) ]                                ≡⟨ []-cong EB.[ cong-refl _ ] ⟩∎
    EB.[ refl x ]                                                        ∎)

-- The []-cong axioms can be instantiated.

instance-of-[]-cong-axiomatisation : E.[]-cong-axiomatisation a
instance-of-[]-cong-axiomatisation = λ where
  .E.[]-cong-axiomatisation.[]-cong             → []-cong
  .E.[]-cong-axiomatisation.[]-cong-equivalence → []-cong-equivalence
  .E.[]-cong-axiomatisation.[]-cong-[refl]      → []-cong-[refl]

-- Some reexported definitions.

open import Erased equality-with-J instance-of-[]-cong-axiomatisation
  public
  hiding ([]-cong; []-cong-equivalence; []-cong-[refl];
          Π-Erased≃Π0[]; Π-Erased≃Π0)

------------------------------------------------------------------------
-- Variants of some of the reexported definitions

private

  -- The lemma push-subst-[], which is reexported above, can be proved
  -- very easily when path equality is used.

  push-subst-[]-Path :
    {@0 P : A → Type p} {@0 p : P x} {x≡y : x P.≡ y} →
    P.subst (λ x → Erased (P x)) x≡y [ p ] ≡ [ P.subst P x≡y p ]
  push-subst-[]-Path = refl _

  -- Above a lemma H-level-Erased is reexported. That lemma is proved
  -- in a certain way. The following two lemmas are included to
  -- illustrate a somewhat different proof technique that works for
  -- individual h-levels (given by closed natural numbers).

  -- Is-proposition is closed under Erased.

  Is-proposition-Erased :
    {@0 A : Type a} →
    @0 Is-proposition A → Is-proposition (Erased A)
  Is-proposition-Erased {A = A} prop =
    _↔_.from (H-level↔H-level 1)
      (Is-proposition-Erased′
         (_↔_.to (H-level↔H-level 1) prop))
    where
    Is-proposition-Erased′ :
      @0 P.Is-proposition A → P.Is-proposition (Erased A)
    Is-proposition-Erased′ prop x y = λ i →
      [ prop (erased x) (erased y) i ]

  -- Is-set is closed under Erased.

  Is-set-Erased :
    {@0 A : Type a} →
    @0 Is-set A → Is-set (Erased A)
  Is-set-Erased {A = A} set =
    _↔_.from (H-level↔H-level 2)
      (Is-set-Erased′
         (_↔_.to (H-level↔H-level 2) set))
    where
    Is-set-Erased′ : @0 P.Is-set A → P.Is-set (Erased A)
    Is-set-Erased′ set p q = λ i j →
      [ set (P.cong erased p) (P.cong erased q) i j ]

------------------------------------------------------------------------
-- Some isomorphisms/equivalences

-- The following four results are inspired by a result in
-- Mishra-Linger's PhD thesis (see Section 5.4.1).

-- There is a bijection (with paths for equality, not _≡_) between
-- (x : Erased A) → P x and (@0 x : A) → P [ x ].

Π-Erased↔Π0[] :
  {@0 A : Type a} {@0 P : Erased A → Type p} →
  ((x : Erased A) → P x) PB.↔ ((@0 x : A) → P [ x ])
Π-Erased↔Π0[] = record
  { surjection = record
    { logical-equivalence = Π-Erased⇔Π0
    ; right-inverse-of = λ f _ → f
    }
  ; left-inverse-of = λ f _ → f
  }

-- There is an equivalence (with paths for equality, not _≡_) between
-- (x : Erased A) → P x and (@0 x : A) → P [ x ].
--
-- This is not proved by converting Π-Erased↔Π0[] to an equivalence,
-- because the type arguments of the conversion function in
-- Equivalence are not erased, and P can only be used in erased
-- contexts.
--
-- This is a strengthening of E.Π-Erased≃Π0[].

Π-Erased≃Π0[] :
  {@0 A : Type a} {@0 P : Erased A → Type p} →
  ((x : Erased A) → P x) PEq.≃ ((@0 x : A) → P [ x ])
Π-Erased≃Π0[] = record
  { to             = λ f x → f [ x ]
  ; is-equivalence =
        (λ f ([ x ]) → f x)
      , (λ f _ → f)
      , (λ f _ → f)
      , (λ f _ _ x → f [ x ])
  }

-- There is a bijection (with paths for equality, not _≡_) between
-- (x : Erased A) → P (erased x) and (@0 x : A) → P x.

Π-Erased↔Π0 :
  {@0 A : Type a} {@0 P : A → Type p} →
  ((x : Erased A) → P (erased x)) PB.↔ ((@0 x : A) → P x)
Π-Erased↔Π0 = Π-Erased↔Π0[]

-- There is an equivalence (with paths for equality, not _≡_) between
-- (x : Erased A) → P (erased x) and (@0 x : A) → P x.
--
-- This is a strengthening of E.Π-Erased≃Π0.

Π-Erased≃Π0 :
  {@0 A : Type a} {@0 P : A → Type p} →
  ((x : Erased A) → P (erased x)) PEq.≃ ((@0 x : A) → P x)
Π-Erased≃Π0 = Π-Erased≃Π0[]


text:
-- Andreas, 2019-07-11, issue #3843, reported by shinji-kono
-- recordExpressionToCopattern translation invalidates projection-likeness.

-- {-# OPTIONS -v tc.proj.like:100 -v impossible:10 #-}

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

postulate
  ANY  : ∀{a} {A : Set a} → A
  Nat  : Set
  suc  : Nat → Nat
  diag : (x : Nat) → x ≡ x
  P    : Nat → Set
  Foo  : {x : Nat} (px : P x) → Set

record Pack (n : Nat) : Set where
  constructor pack
  field
    lv  : Nat
    ord : P lv
open Pack

-- Projection-like, because eta-contracted to  pidproj x = x
pidproj : ∀ {n} (x : Pack n) → Pack n
pidproj x = record { lv = lv x; ord = ord x }

-- Not considered projection-like, since
-- `pidpc (pack l o)` is stuck, but the `n` cannot be inferred.
pidpc : ∀ {n} (x : Pack n) → Pack n
pidpc x .lv = lv x
pidpc x .ord = ord x

-- Not considered projection-like, since
-- `pidcop (pack l o)` is stuck, but the `n` cannot be inferred.
pidcop : ∀ {n} (x : Pack n) → Pack n
pidcop (pack lx ox) .lv  = lx
pidcop (pack lx ox) .ord = ox

-- WAS: Projection-like function,
-- but since is translated to pidcop by recordExpressionsToCopatterns
-- projection-likeness is unsound here.
pid : ∀ {n} (x : Pack n) → Pack n
pid (pack lx ox) = record { lv = lx ; ord = ox }
-- pid record { lv = lx ; ord = ox } = record { lv = lx ; ord = ox }
-- pid (pack lx ox) = pack lx ox  -- no error
-- pid x = x  -- Error disappears with record pattern matching

test : ∀ {n} (x : Pack (suc n)) → x ≡ pid x
test {n} x@(pack lx ox) with diag (lv x)  -- The @-pattern is needed for 2.5.2 and 2.5.3
... | refl with Foo (ord x) -- with needed
... | _ = ANY

-- WAS: internal error

-- Should succeed.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Costrings
------------------------------------------------------------------------

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

module Codata.Musical.Costring where

open import Codata.Musical.Colist as Colist using (Colist)
open import Data.Char using (Char)
open import Data.String as String using (String)
open import Function using (_∘_)

-- Possibly infinite strings.

Costring : Set
Costring = Colist Char

-- Methods

toCostring : String → Costring
toCostring = Colist.fromList ∘ String.toList


text:
-- Andreas, AIM XXIII, 2016-04-25

-- Parameter arguments of overloaded projection applications
-- should not be skipped!

record R A : Set where
  field f : {x y : A} → A
open R

record S A : Set where
  field f : {x y : A} → A
open S

r : ∀{A} → R A
f r {x} = x

test : ∀{A B : Set} (a : A) (b : B) → A
test {A} a b = f (r {A}) {x = a} {y = b}


text:
module README where

------------------------------------------------------------------------
-- Core definitions
------------------------------------------------------------------------

import Generics.Prelude

-- Generics.Telescope introduces an encoding for telescopes,
-- along with functions to manipulate indexed functions and families.
import Generics.Telescope

-- Generics.Desc introduces the core universe of descriptions for datatypes.
import Generics.Desc

-- Generics.HasDesc defines the HasDesc record,
-- bridging the gap between descriptions of datatypes
-- and their concrete Agda counterpart.
import Generics.HasDesc

-- Generics.Reflection implements the deriveDesc macro
-- to automatically derive an instance of HasDesc for most datatypes.
import Generics.Reflection

------------------------------------------------------------------------
-- Generic constructions
------------------------------------------------------------------------

-- Generic show implemetation
import Generics.Constructions.Show

-- Datatype-generic case analysis principle
import Generics.Constructions.Case

-- Datatype-generic decidable equality
import Generics.Constructions.DecEq

-- Datatype-generic induction principle,
-- on described datatypes only
import Generics.Constructions.Induction

-- Datatype-generic elimination principle
import Generics.Constructions.Elim

-- WIP Datatype-generic injectivity of constructors
import Generics.Constructions.NoConfusion

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Classical.Semantics.Satisfaction (𝔏 : Signature) {ℓₘ} where
open Signature(𝔏)

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.ListSized
import      Data.ListSized.Functions as List
open import Formalization.PredicateLogic.Classical.Semantics(𝔏){ℓₘ}
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Functional using (_∘_ ; _∘₂_)
import      Logic.Propositional as Logic
import      Logic.Predicate     as Logic
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Natural
open import Relator.Equals
open import Sets.PredicateSet using (PredSet)
open        Sets.PredicateSet.BoundedQuantifiers
open import Syntax.Function
open import Type.Dependent renaming (intro to _,_)
open import Type.Properties.Decidable
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable P : Type{ℓₚ}
private variable args n vars : ℕ
private variable 𝔐 : Model

-- A `VarMapping(vars)(𝔐)` maps `vars` number of variables to objects in the domain of the model `𝔐`.
-- Also called: Variable assignment.
VarMapping : ℕ → Model → Type
VarMapping(vars)(𝔐) = 𝕟(vars) → Model.Domain(𝔐)
module VarMapping where
  -- Adds a mapping to an object in the domain of the model `𝔐`.
  add0 : VarMapping(vars)(𝔐) → Model.Domain(𝔐) → VarMapping(𝐒(vars))(𝔐)
  add0 𝔰 t 𝟎      = t
  add0 𝔰 t (𝐒(v)) = 𝔰(v)

private variable 𝔰 : VarMapping(vars)(𝔐)

module _ ((𝔐 , 𝔰) : Σ Model (VarMapping(vars))) where
  -- Maps terms to objects in the domain given a model and a variable mapping.
  val : Term(vars) → Model.Domain(𝔐)
  val₊ : List(Term(vars))(n) → List(Model.Domain(𝔐))(n)

  val(var v)    = 𝔰(v)
  val(func f x) = Model.function 𝔐 f (val₊ x)
  val₊ {0}       ∅       = ∅
  val₊ {𝐒(n)} (t ⊰ ts) = (val t ⊰ val₊ {n} ts)
  --val₊ = List.map val

-- Satisfication relation.
-- ((𝔐 , 𝔰) ⊧ φ) means that the formula φ is satisfied in the model 𝔐 with the variable mapping.
-- Or in other words: A formula is true in the model 𝔐.
_⊧_ : (Σ Model (VarMapping(vars))) → Formula(vars) → Type{ℓₘ}
(𝔐 , 𝔰) ⊧ (f $ x)  = Lvl.Up(IsTrue(Model.relation 𝔐 f (val₊(𝔐 , 𝔰) x)))  -- A model decides whether a relation is satisfied.
(𝔐 , 𝔰) ⊧ ⊤        = Unit                                                 -- All models satisfy top.
(𝔐 , 𝔰) ⊧ ⊥        = Empty                                                -- No model satisfies bottom.
(𝔐 , 𝔰) ⊧ (φ ∧ ψ)  = ((𝔐 , 𝔰) ⊧ φ) Logic.∧ ((𝔐 , 𝔰) ⊧ ψ)                  -- A model satisfies a conjunction when it satisfies both of the propositions.
(𝔐 , 𝔰) ⊧ (φ ∨ ψ)  = ((𝔐 , 𝔰) ⊧ φ) Logic.∨ ((𝔐 , 𝔰) ⊧ ψ)                  -- A model satisfies a disjunction when it satisfies any one of the propositions.
(𝔐 , 𝔰) ⊧ (φ ⟶ ψ)  = Logic.¬((𝔐 , 𝔰) ⊧ φ) Logic.∨ ((𝔐 , 𝔰) ⊧ ψ)
(𝔐 , 𝔰) ⊧ (Ɐ φ)    = Logic.∀ₗ(t ↦ (𝔐 , VarMapping.add0{𝔐 = 𝔐} 𝔰 t) ⊧ φ)
(𝔐 , 𝔰) ⊧ (∃ φ)    = Logic.∃(t ↦ (𝔐 , VarMapping.add0{𝔐 = 𝔐} 𝔰 t) ⊧ φ)

-- Satisfication of a set of formulas.
-- This means that a model satisfies all formulas at the same time.
_⊧₊_ : (Σ Model (VarMapping(vars))) → PredSet{ℓ}(Formula(vars)) → Type
𝔐 ⊧₊ Γ = ∀ₛ(Γ) (𝔐 ⊧_)

-- Validity of a formula.
-- A formula is valid when it is true independent of any model (is satisfied by all models).
-- Examples:
--   Valid(⊤)
--   Valid(⊥ ⟶ ⊥)
--   ¬ Valid(⊥)
--   ¬ Valid(P) where P : Prop(0)
Valid : Formula(vars) → Type
Valid(φ) = Logic.∀ₗ(_⊧ φ)

-- Satisfiability of sets of formulas.
-- A set of formulas is satisfiable when there is a model that satisfies all of them at the same time.
Satisfiable : PredSet{ℓ}(Formula(vars)) → Type
Satisfiable(Γ) = Logic.∃(_⊧₊ Γ)

-- Unsatisfiability of sets of formulas.
Unsatisfiable : PredSet{ℓ}(Formula(vars)) → Type
Unsatisfiable{ℓ} = Logic.¬_ ∘ Satisfiable{ℓ}

-- Semantic entailment of a formula.
-- A hypothetical statement. If a model would satisfy all formulas in Γ, then this same model satisifes the formula φ.
_⊨_ : PredSet{ℓ}(Formula(vars)) → Formula(vars) → Type
Γ ⊨ φ = ∀{𝔐} → (𝔐 ⊧₊ Γ) → (𝔐 ⊧ φ)

_⊭_ : PredSet{ℓ}(Formula(vars)) → Formula(vars) → Type
_⊭_ = (Logic.¬_) ∘₂ (_⊨_)

-- Axiomatization of a theory by a set of axioms.
-- A set of axioms is a set of formulas.
-- A theory is the closure of a set of axioms.
-- An axiomatization is a subset of formulas of the theory which entails all formulas in the axiomatized theory.
_axiomatizes_ : PredSet{ℓ₁}(Formula(vars)) → PredSet{ℓ₂}(Formula(vars)) → Type
Γ₁ axiomatizes Γ₂ = ∀{φ} → (Γ₁ ⊨ φ) → Γ₂(φ)

-- A set of formulas is closed when it includes all formulas that it entails.
Closed : PredSet{ℓ}(Formula(vars)) → Type
Closed(Γ) = Γ axiomatizes Γ

_⊨₊_ : PredSet{ℓ₁}(Formula(vars)) → PredSet{ℓ₂}(Formula(vars)) → Type
Γ₁ ⊨₊ Γ₂ = ∀{𝔐} → (𝔐 ⊧₊ Γ₁) → (𝔐 ⊧₊ Γ₂)

_⊭₊_ : PredSet{ℓ₁}(Formula(vars)) → PredSet{ℓ₂}(Formula(vars)) → Type
_⊭₊_ = (Logic.¬_) ∘₂ (_⊨₊_)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Andreas, 2017-10-04, issue #2765, reported by nad
-- Problem: inferred level expressions are often "reversed"

open import Agda.Primitive

postulate
  F : (ℓ : Level) → Set ℓ

G : (a b c : Level) → Set {!!}  -- C-c C-=
G a b c = F a → F b → F c

-- WAS:
-- ?0 := c ⊔ (b ⊔ a)

-- Expected: Inferred level should be
-- ?0 := a ⊔ (b ⊔ c)


text:
{-# OPTIONS --without-K --safe #-}
module Categories.GlobularSet where

-- Globular sets are defined in a Categorical context, but
-- should they be inside the Categories hierarchy?

open import Level
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category
open import Categories.Category.Instance.Globe
open import Categories.Category.Instance.Sets
open import Categories.Functor
open import Categories.Functor.Presheaf

private
  variable
    o ℓ e : Level

GlobularSet : (o : Level) → Set (suc o)
GlobularSet o = Presheaf Globe (Sets o)

-- TODO? make universe polymorphic with polymorphic ⊤
Trivial : GlobularSet zero
Trivial = record
  { F₀ = λ _ → ⊤
  ; F₁ = λ _ x → x
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = λ _ → refl
  }

GlobularObject : Category o ℓ e → Set _
GlobularObject C = Functor (Category.op Globe) C

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Data.QuadTree.InternalAgda where

open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.PublicFunctions
open import Data.QuadTree.Implementation.Functors
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.Foldable

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module _ where

module M where
  postulate A : Set

module N = M  -- This alias introduces a display form M.A --> N.A

open M

postulate
  a : A

{-# DISPLAY N.A = A #-} -- Makes Agda loop

test : Set
test = a


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory

module cw.cohomology.cochainequiv.DualizedHigherBoundary (OT : OrdinaryTheory lzero)
  {n} (⊙fin-skel : ⊙FinSkeleton (S (S n))) where

open OrdinaryTheory OT

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel

  fin-skel₋₁ = AttachedFinSkeleton.skel fin-skel
  I₋₁ = AttachedFinSkeleton.numCells fin-skel₋₁

abstract
  rephrase-dualized-higher-boundary-in-degree : ∀ g <I
    → GroupIso.g (FreeAbGroup-extend-iso (C2-abgroup 0))
        (GroupIso.f (FreeAbGroup-extend-iso (C2-abgroup 0)) g ∘ᴳ fboundary-last fin-skel) <I
    == Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁))
  rephrase-dualized-higher-boundary-in-degree g <I =
    FormalSum-extend (C2-abgroup 0) g (GroupHom.f (fboundary-last fin-skel) fs[ inl <I :: nil ])
      =⟨ ap (FormalSum-extend (C2-abgroup 0) g) $
          app= (is-equiv.g-f (FreeAbGroup-extend-is-equiv (FreeAbGroup (Fin I₋₁))) (fboundary'-last fin-skel)) <I ⟩
    FormalSum-extend (C2-abgroup 0) g
      (Group.sum (FreeAbGroup.grp (Fin I₋₁))
        (λ <I₋₁ → Group.exp (FreeAbGroup.grp (Fin I₋₁)) fs[ inl <I₋₁ :: nil ] (fdegree-last fin-skel <I <I₋₁)))
      =⟨ GroupHom.pres-sum (FreeAbGroup-extend (C2-abgroup 0) g)
          (λ <I₋₁ → Group.exp (FreeAbGroup.grp (Fin I₋₁)) fs[ inl <I₋₁ :: nil ] (fdegree-last fin-skel <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ →
        (FormalSum-extend (C2-abgroup 0) g
          (Group.exp (FreeAbGroup.grp (Fin I₋₁)) fs[ inl <I₋₁ :: nil ] (fdegree-last fin-skel <I <I₋₁))))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ →
            GroupHom.pres-exp (FreeAbGroup-extend (C2-abgroup 0) g)
              fs[ inl <I₋₁ :: nil ]
              (fdegree-last fin-skel <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ →
        (Group.exp (C2 0)
          (FormalSum-extend (C2-abgroup 0) g fs[ inl <I₋₁ :: nil ])
          (fdegree-last fin-skel <I <I₋₁)))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ → ap (λ g → Group.exp (C2 0) g (fdegree-last fin-skel <I <I₋₁)) $
            app= (is-equiv.g-f (FreeAbGroup-extend-is-equiv (C2-abgroup 0)) g) <I₋₁) ⟩
    Group.sum (C2 0) (λ <I₋₁ → (Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------------
-- A partial function: iter₀
------------------------------------------------------------------------------

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

module FOTC.Program.Iter0.Iter0 where

open import FOTC.Base
open import FOTC.Base.List

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

postulate
  iter₀    : D → D → D
  iter₀-eq : ∀ f n → iter₀ f n ≡
             (if (iszero₁ n) then [] else (n ∷ iter₀ f (f · n)))
{-# ATP axiom iter₀-eq #-}


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module BubbleSort.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import BubbleSort _≤_ tot≤
open import Data.Product
open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import Size
open import SList
open import SList.Properties A
open import SList.Concatenation A

lemma-swap*∼ : {ι : Size}(x : A) → (xs : SList A {ι}) → unsize A (x ∙ xs) ∼ unsize A (proj₂ (swap* x xs) ∙ proj₁ (swap* x xs))
lemma-swap*∼ x snil = ∼x /head /head ∼[]
lemma-swap*∼ x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y = ∼x /head (/tail /head) (lemma-swap*∼ y ys)
... | inj₂ y≤x = ∼x (/tail /head) (/tail /head) (lemma-swap*∼ x ys)

lemma-bubbleSort∼ : {ι : Size}(xs : SList A {ι}) → unsize A xs ∼ unsize A (bubbleSort xs)
lemma-bubbleSort∼ snil = ∼[]
lemma-bubbleSort∼ (x ∙ xs) = trans∼ (lemma-swap*∼ x xs) (trans∼ (lemma-⊕∼ y (lemma-bubbleSort∼ ys)) (lemma-size-unsize y (bubbleSort ys)))
                  where sxxs = swap* x xs
                        ys = proj₁ sxxs
                        y = proj₂ sxxs

theorem-bubbleSort∼ : (xs : List A) → xs ∼ unsize A (bubbleSort (size A xs))
theorem-bubbleSort∼ xs = trans∼ (lemma-unsize-size xs) (lemma-bubbleSort∼ (size A xs))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
---------------------------------------------------------------------------
-- The rec definition using the fixed-point combinator
---------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Rec where

open import LTC-PCF.Base

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

-- Let T = D → D → (D → D → D) → D be a type. Instead of defining
-- rec : T → T, we use the LTC-PCF λ-abstraction and application to
-- avoid use a polymorphic fixed-point operator.

rech : D → D
rech r = lam (λ n → lam (λ a → lam (λ f →
           if (iszero₁ n)
             then a
             else f · pred₁ n · (r · pred₁ n · a · f))))

rec : D → D → D → D
rec n a f = fix rech · n · a · f


text:
open import Prelude
open import Nat
open import Agda.Primitive using (Level; lzero; lsuc) renaming (_⊔_ to lmax)

module List where

  -- definitions

  data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

  _++_ : {A : Set} → List A → List A → List A
  [] ++ l₂ = l₂
  (h :: l₁) ++ l₂ = h :: (l₁ ++ l₂)

  infixl 50 _++_

  ∥_∥ : {A : Set} → List A → Nat
  ∥ [] ∥ = Z
  ∥ a :: as ∥ = 1+ ∥ as ∥

  _⟦_⟧ : {A : Set} → List A → Nat → Maybe A
  [] ⟦ i ⟧ = None
  (a :: as) ⟦ Z ⟧ = Some a
  (a :: as) ⟦ 1+ i ⟧ = as ⟦ i ⟧

  data _In_ : {A : Set} → A → List A → Set where
    LInH : ∀{A} {a : A} {l : List A} → a In (a :: l)
    LInT : ∀{A} {a a' : A} {l : List A} → a In l → a In (a' :: l)

  _⫇_ : {A : Set} → List A → List A → Set
  _⫇_ {A} l1 l2 = (i1 : Nat) (a : A) →
                  l1 ⟦ i1 ⟧ == Some a →
                  Σ[ i2 ∈ Nat ] (l2 ⟦ i2 ⟧ == Some a)

  _≈_ : {A : Set} → List A → List A → Set
  _≈_ {A} l1 l2 = l1 ⫇ l2 ∧ l2 ⫇ l1

  reverse : {A : Set} → List A → List A
  reverse [] = []
  reverse (a :: as) = reverse as ++ (a :: [])

  map : {A B : Set} → (A → B) → List A → List B
  map f [] = []
  map f (a :: as) = f a :: map f as

  foldl : {A B : Set} → (B → A → B) → B → List A → B
  foldl f b [] = b
  foldl f b (a :: as) = foldl f (f b a) as

  foldr : {A B : Set} → (B → A → B) → B → List A → B
  foldr f b = foldl f b ⊙ reverse

  concat : {A : Set} → List (List A) → List A
  concat [] = []
  concat (l1 :: rest) = l1 ++ (concat rest)

  -- if the lists aren't the same length,
  -- the extra elements of the longer list are ignored
  zip : {A B : Set} → List A → List B → List (A ∧ B)
  zip []        _         = []
  zip (a :: as) []        = []
  zip (a :: as) (b :: bs) = (a , b) :: zip as bs

  unzip : {A B : Set} → List (A ∧ B) → (List A ∧ List B)
  unzip [] = ([] , [])
  unzip ((a , b) :: rest)
    with unzip rest
  ... | (as , bs) = (a :: as , b :: bs)

  -- theorems

  list-==-dec :  {A : Set} →
                 (l1 l2 : List A) →
                 ((a1 a2 : A) → a1 == a2 ∨ a1 ≠ a2) →
                 l1 == l2 ∨ l1 ≠ l2
  list-==-dec [] [] A-==-dec       = Inl refl
  list-==-dec [] (_ :: _) A-==-dec = Inr (λ ())
  list-==-dec (_ :: _) [] A-==-dec = Inr (λ ())
  list-==-dec (h1 :: t1) (h2 :: t2) A-==-dec
    with A-==-dec h1 h2
  ... | Inr ne = Inr (λ where refl → ne refl)
  ... | Inl refl
    with list-==-dec t1 t2 A-==-dec
  ... | Inr ne = Inr (λ where refl → ne refl)
  ... | Inl refl = Inl refl

  -- if the items of two lists are equal, then the lists are equal
  ==-per-elem : {A : Set} → {l1 l2 : List A} →
                 ((i : Nat) → l1 ⟦ i ⟧ == l2 ⟦ i ⟧) →
                 l1 == l2
  ==-per-elem {l1 = []} {[]} items== = refl
  ==-per-elem {l1 = []} {h2 :: t2} items== = abort (somenotnone (! (items== Z)))
  ==-per-elem {l1 = h1 :: t1} {[]} items== = abort (somenotnone (items== Z))
  ==-per-elem {l1 = h1 :: t1} {h2 :: t2} items==
    rewrite someinj (items== Z) | ==-per-elem {l1 = t1} {t2} (λ i → items== (1+ i))
      = refl

  -- _++_ theorems
  ++assc : ∀{A a1 a2 a3} → (_++_ {A} a1 a2) ++ a3 == a1 ++ (a2 ++ a3)
  ++assc {A} {[]} {a2} {a3} = refl
  ++assc {A} {x :: a1} {a2} {a3} with a1 ++ a2 ++ a3 | ++assc {A} {a1} {a2} {a3}
  ++assc {A} {x :: a1} {a2} {a3} | _ | refl = refl

  l++[]==l : {A : Set} (l : List A) →
              l ++ [] == l
  l++[]==l [] = refl
  l++[]==l (a :: as)
    rewrite l++[]==l as
      = refl

  -- ∥_∥ theorem
  ∥-++-comm : ∀{A a1 a2} → ∥ a1 ∥ + (∥_∥ {A} a2) == ∥ a1 ++ a2 ∥
  ∥-++-comm {A} {[]} {a2} = refl
  ∥-++-comm {A} {a :: a1} {a2} = 1+ap (∥-++-comm {A} {a1})

  -- _⟦_⟧ and ++ theorem
  ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a : {A : Set} {l1 l2 : List A} {a : A} →
                             (l1 ++ (a :: []) ++ l2) ⟦ ∥ l1 ∥ ⟧ == Some a
  ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a {l1 = []} = refl
  ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a {l1 = a1 :: l1rest} {l2} {a} = ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a {l1 = l1rest} {l2}

  -- packaging of list indexing results
  list-index-dec : {A : Set} (l : List A) (i : Nat) →
                    l ⟦ i ⟧ == None ∨ Σ[ a ∈ A ] (l ⟦ i ⟧ == Some a)
  list-index-dec l i
    with l ⟦ i ⟧
  ... | None   = Inl refl
  ... | Some a = Inr (a , refl)

  -- theorems characterizing the partiality of list indexing
  list-index-some : {A : Set} {l : List A} {i : Nat} →
                     i < ∥ l ∥ →
                     Σ[ a ∈ A ] (l ⟦ i ⟧ == Some a)
  list-index-some {l = []}      {Z}    i<∥l∥ = abort (n≮0 i<∥l∥)
  list-index-some {l = a :: as} {Z}    i<∥l∥ = _ , refl
  list-index-some {l = a :: as} {1+ i} i<∥l∥ = list-index-some (1+n<1+m→n<m i<∥l∥)

  list-index-none : {A : Set} {l : List A} {i : Nat} →
                     ∥ l ∥ ≤ i →
                     l ⟦ i ⟧ == None
  list-index-none {l = []}             i≥∥l∥ = refl
  list-index-none {l = a :: as} {1+ i} i≥∥l∥ = list-index-none (1+n≤1+m→n≤m i≥∥l∥)

  list-index-some-conv : {A : Set} {l : List A} {i : Nat} {a : A} →
                          l ⟦ i ⟧ == Some a →
                          i < ∥ l ∥
  list-index-some-conv {l = l} {i} i≥∥l∥
    with <dec ∥ l ∥ i
  ... | Inr (Inr i<∥l∥) = i<∥l∥
  ... | Inr (Inl refl)
    rewrite list-index-none {l = l} {∥ l ∥} ≤refl
      = abort (somenotnone (! i≥∥l∥))
  ... | Inl ∥l∥<i
    rewrite list-index-none (n<m→n≤m ∥l∥<i)
      = abort (somenotnone (! i≥∥l∥))

  list-index-none-conv : {A : Set} {l : List A} {i : Nat} →
                          l ⟦ i ⟧ == None →
                          ∥ l ∥ ≤ i
  list-index-none-conv {l = l} {i} i≥∥l∥
    with <dec ∥ l ∥ i
  ... | Inl ∥l∥<i       = n<m→n≤m ∥l∥<i
  ... | Inr (Inl refl) = ≤refl
  ... | Inr (Inr i<∥l∥)
    with list-index-some i<∥l∥
  ... | _ , i≱∥l∥ rewrite i≥∥l∥ = abort (somenotnone (! i≱∥l∥))

  ∥l1∥==∥l2∥→l1[i]→l2[i] : {A B : Set} {la : List A} {lb : List B} {i : Nat} {a : A} →
                             ∥ la ∥ == ∥ lb ∥ →
                             la ⟦ i ⟧ == Some a →
                             Σ[ b ∈ B ] (lb ⟦ i ⟧ == Some b)
  ∥l1∥==∥l2∥→l1[i]→l2[i] {i = i} ∥la∥==∥lb∥ la[i]==a
    = list-index-some (tr (λ y → i < y) ∥la∥==∥lb∥ (list-index-some-conv la[i]==a))

  ∥l1∥==∥l2∥→¬l1[i]→¬l2[i] : {A B : Set} {la : List A} {lb : List B} {i : Nat} →
                                ∥ la ∥ == ∥ lb ∥ →
                                la ⟦ i ⟧ == None →
                                lb ⟦ i ⟧ == None
  ∥l1∥==∥l2∥→¬l1[i]→¬l2[i] {i = i} ∥la∥==∥lb∥ la[i]==None
    = list-index-none (tr (λ y → y ≤ i) ∥la∥==∥lb∥ (list-index-none-conv la[i]==None))

  -- more list indexing theorems
  i∈l2→|l1|+i∈l1++l2 : {A : Set} {l1 l2 : List A} {i : Nat} {a : A} →
                          l2 ⟦ i ⟧ == Some a →
                          (l1 ++ l2) ⟦ ∥ l1 ∥ + i ⟧ == Some a
  i∈l2→|l1|+i∈l1++l2 {l1 = []} i∈l2 = i∈l2
  i∈l2→|l1|+i∈l1++l2 {l1 = a1 :: l1} i∈l2 = i∈l2→|l1|+i∈l1++l2 {l1 = l1} i∈l2

  i∈l1→i∈l1++l2 : {A : Set} {l1 l2 : List A} {i : Nat} {a : A} →
                      l1 ⟦ i ⟧ == Some a →
                      (l1 ++ l2) ⟦ i ⟧ == Some a
  i∈l1→i∈l1++l2 {l1 = a1 :: l1} {i = Z} i∈l1 = i∈l1
  i∈l1→i∈l1++l2 {l1 = a1 :: l1} {i = 1+ i} i∈l1 = i∈l1→i∈l1++l2 {l1 = l1} i∈l1

  append-index-split : {A : Set} {l1 l2 : List A} {i : Nat} {a : A} →
                         (l1 ++ l2) ⟦ i ⟧ == Some a →
                         l1 ⟦ i ⟧ == Some a ∨ (Σ[ j ∈ Nat ] (∥ l1 ∥ + j == i ∧ l2 ⟦ j ⟧ == Some a))
  append-index-split {l1 = []} i∈l1==l2 = Inr (_ , refl , i∈l1==l2)
  append-index-split {l1 = a1 :: l1} {i = Z} i∈l1==l2 = Inl i∈l1==l2
  append-index-split {l1 = a1 :: l1} {i = 1+ i} i∈l1==l2
    with append-index-split {l1 = l1} i∈l1==l2
  ... | Inl i∈l1 = Inl i∈l1
  ... | Inr (j , |l1|+j=i , j∈l2) = Inr (_ , 1+ap |l1|+j=i , j∈l2)

  -- reverse theorems
  reverse-single : {A : Set} {a : A} → reverse (a :: []) == a :: []
  reverse-single = refl

  reverse-++ : {A : Set} {l1 l2 : List A} →
                reverse (l1 ++ l2) == reverse l2 ++ reverse l1
  reverse-++ {l1 = []} {l2}
    rewrite l++[]==l (reverse l2)
      = refl
  reverse-++ {l1 = a1 :: as1} {l2}
    rewrite reverse-++ {l1 = as1} {l2}
      = ++assc {a1 = reverse l2}

  reverse-inv : {A : Set} {l : List A} → reverse (reverse l) == l
  reverse-inv {l = []} = refl
  reverse-inv {l = a :: as}
    rewrite reverse-++ {l1 = reverse as} {a :: []} | reverse-inv {l = as}
      = refl

  -- map theorems
  map-ext : ∀{A B : Set} {f g : A → B} {l : List A} →
              ((a : A) → f a == g a) →
              map f l == map g l
  map-ext {l = []} ext = refl
  map-ext {l = a :: l} ext rewrite ext a | map-ext {l = l} ext = refl

  map-id : ∀{A : Set} {l : List A} → map (λ a → a) l == l
  map-id {l = []} = refl
  map-id {l = a :: l} rewrite map-id {l = l} = refl

  map-len : ∀{A B : Set} {f : A → B} {l : List A} → ∥ map f l ∥ == ∥ l ∥
  map-len {l = []} = refl
  map-len {l = _ :: l} = 1+ap map-len

  map-In : ∀{A B : Set} {f : A → B} {l : List A} {a : A} →
             a In l →
             f a In map f l
  map-In LInH = LInH
  map-In (LInT aInL) = LInT (map-In aInL)

  map-++-comm : ∀{A B f a b} → map f a ++ map f b == map {A} {B} f (a ++ b)
  map-++-comm {a = []} = refl
  map-++-comm {A} {B} {f} {h :: t} {b} with map f (t ++ b) | map-++-comm {A} {B} {f} {t} {b}
  map-++-comm {A} {B} {f} {h :: t} {b} | _ | refl = refl

  map^2 : ∀{A B C f g l} → map {B} {C} f (map {A} {B} g l) == map (f ⊙ g) l
  map^2 {l = []} = refl
  map^2 {f = f} {g} {h :: t} rewrite map^2 {f = f} {g} {t} = refl

  reverse-map : {A B : Set} {f : A → B} {l : List A} → reverse (map f l) == map f (reverse l)
  reverse-map {l = []} = refl
  reverse-map {f = f} {a' :: l}
    rewrite reverse-map {f = f} {l}
      = map-++-comm {a = reverse l}

  -- foldl theorem
  foldl-++ : {A B : Set} {l1 l2 : List A} {f : B → A → B} {b0 : B} →
              foldl f b0 (l1 ++ l2) == foldl f (foldl f b0 l1) l2
  foldl-++ {l1 = []} = refl
  foldl-++ {l1 = a1 :: l1rest} = foldl-++ {l1 = l1rest}

  -- fold+map theorem
  foldl-map : {A' A B : Set} {l : List A'} {f-fold : B → A → B} {f-map : A' → A} {b0 : B} →
               foldl f-fold b0 (map f-map l) == foldl (λ b a' → f-fold b (f-map a')) b0 l
  foldl-map {l = []} = refl
  foldl-map {l = a' :: l} {f-fold} {f-map} {b0} = foldl-map {l = l}

  foldr-map : {A' A B : Set} {l : List A'} {f-fold : B → A → B} {f-map : A' → A} {b0 : B} →
               foldr f-fold b0 (map f-map l) == foldr (λ b a' → f-fold b (f-map a')) b0 l
  foldr-map {l = l} {_} {f}
    rewrite reverse-map {f = f} {l}
      = foldl-map {l = reverse l}

  -- zip/unzip theorems
  unzip-inv : {A B : Set} {l : List (A ∧ B)} {la : List A} {lb : List B} →
               unzip l == (la , lb) →
               l == zip la lb
  unzip-inv {l = []} form
    with form
  ... | refl = refl
  unzip-inv {l = (a' , b') :: rest} {a :: as} {b :: bs} form
    with unzip rest  | unzip-inv {l = rest} refl | form
  ...  | (as' , bs') | refl                      | refl = refl

  zip-inv : {A B : Set} {la : List A} {lb : List B} →
             ∥ la ∥ == ∥ lb ∥ →
             unzip (zip la lb) == (la , lb)
  zip-inv {la = []}      {[]}      len-eq = refl
  zip-inv {la = a :: as} {b :: bs} len-eq
    with unzip (zip as bs) | zip-inv (1+inj len-eq)
  ...  | (as' , bs')       | refl                   = refl

  -- _≈_ theorems
  ≈-++-comm-lem' : (A : Set) (l1 l2 : List A) (i : Nat) (a : A) →
                   (l1 ++ l2) ⟦ i ⟧ == Some a →
                   Σ[ i' ∈ Nat ] ((l2 ++ l1) ⟦ i' ⟧ == Some a)
  ≈-++-comm-lem' A l1 l2 i a i∈l1++l2
    with append-index-split {l1 = l1} i∈l1++l2
  ... | Inl i∈l1 = _ , i∈l2→|l1|+i∈l1++l2 {l1 = l2} i∈l1
  ... | Inr (j , |l1|+j=i , j∈l2) = _ , i∈l1→i∈l1++l2 {l1 = l2} j∈l2

  ≈-++-comm : {A : Set} {l1 l2 : List A} → l1 ++ l2 ≈ l2 ++ l1
  ≈-++-comm {A} {l1} {l2} = ≈-++-comm-lem' A l1 l2 , ≈-++-comm-lem' A l2 l1

  ≈-++-dup : {A : Set} {l : List A} → l ++ l ≈ l
  ≈-++-dup {l = []} = (λ i a ()) , (λ i a ())
  ≈-++-dup {A} {a :: l}
    = ≈-++-dup'1 , ≈-++-dup'2
      where
      ≈-++-dup'1 : (i : Nat) (a' : A) →
                   (a :: (l ++ (a :: l))) ⟦ i ⟧ == Some a' →
                   Σ[ i' ∈ Nat ] ((a :: l) ⟦ i' ⟧ == Some a')
      ≈-++-dup'1 Z a' i∈alal = Z , i∈alal
      ≈-++-dup'1 (1+ i) a' i∈alal
        with append-index-split {l1 = l} i∈alal
      ... | Inl i∈l = (1+ i) , i∈l
      ... | Inr (j , |l1|+j=i , j∈al) = j , j∈al

      ≈-++-dup'2 : (i : Nat) (a' : A) →
                   (a :: l) ⟦ i ⟧ == Some a' →
                   Σ[ i' ∈ Nat ] ((a :: (l ++ (a :: l))) ⟦ i' ⟧ == Some a')
      ≈-++-dup'2 i a' i∈al = (1 + ∥ l ∥ + i) , i∈l2→|l1|+i∈l1++l2 {l1 = l} i∈al

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda