text:
------------------------------------------------------------------------
-- Alternative functional semantics for an untyped λ-calculus with
-- constants
------------------------------------------------------------------------

-- I noted that the compiler correctness proof in
-- Lambda.Closure.Functional might be easier if the semantics was
-- defined using continuation-passing style, so I decided to try this
-- out. The proof at the end of this module /is/ slightly shorter, but
-- the continuation-passing definition of the semantics is quite
-- awkward (due to the limitations imposed by Agda). Furthermore it
-- seemed to me as if the soundness proofs in
-- Lambda.Closure.Equivalence would be harder to prove using this
-- formulation of the semantics.

module Lambda.Closure.Functional.Alternative where

open import Category.Monad
open import Category.Monad.Partiality as Partiality
  using (_⊥; never; Kind; OtherKind)
open import Codata.Musical.Notation
open import Data.List hiding (lookup)
open import Data.Maybe
import Data.Maybe.Categorical as Maybe
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Function
open import Level
open import Relation.Binary using (module Preorder)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Partiality._⊥
open Partiality.Kind
private
  open module E {A : Set} = Partiality.Equality (_≡_ {A = A})
  open module R {A : Set} =
    Partiality.Reasoning (P.isEquivalence {A = A})

open import Lambda.Syntax
open Closure Tm
open import Lambda.VirtualMachine
open Functional
private
  module VM = Closure Code

------------------------------------------------------------------------
-- A monad with partiality and failure

PF : RawMonad {f = zero} (_⊥ ∘ Maybe)
PF = Maybe.monadT Partiality.monad

module PF where
  open RawMonad PF public

  fail : {A : Set} → Maybe A ⊥
  fail = now nothing

open PF

------------------------------------------------------------------------
-- Semantics

module Workaround₁ where

  -- This module provides a workaround for the limitations of
  -- guardedness.

  mutual

    data Maybe_⊥P (A : Set) : Set where
      ⌈_⌉   : (x : Maybe A ⊥) → Maybe A ⊥P
      later : (x : ∞ (Maybe A ⊥P)) → Maybe A ⊥P
      ⟦_⟧P  : ∀ {n} (t : Tm n) (ρ : Env n) (k : Value → Maybe A ⊥W) →
              Maybe A ⊥P

    data Maybe_⊥W (A : Set) : Set where
      ⌈_⌉   : (x : Maybe A ⊥) → Maybe A ⊥W
      later : (x : Maybe A ⊥P) → Maybe A ⊥W

  mutual

    -- The semantics, in slightly scrambled form.

    infix 5 _∙W_

    ⟦_⟧W : ∀ {A n} → Tm n → Env n → (Value → Maybe A ⊥W) → Maybe A ⊥W
    ⟦ con i ⟧W   ρ k = k (con i)
    ⟦ var x ⟧W   ρ k = k (lookup ρ x)
    ⟦ ƛ t ⟧W     ρ k = k (ƛ t ρ)
    ⟦ t₁ · t₂ ⟧W ρ k = ⟦ t₁ ⟧W ρ (λ v₁ →
                       ⟦ t₂ ⟧W ρ (λ v₂ →
                       (v₁ ∙W v₂) k))

    _∙W_ : ∀ {A} → Value → Value → (Value → Maybe A ⊥W) → Maybe A ⊥W
    (con i  ∙W v₂) k = ⌈ fail ⌉
    (ƛ t₁ ρ ∙W v₂) k = later (⟦ t₁ ⟧P (v₂ ∷ ρ) k)

  -- Interpretation of the definitions above.

  whnf : ∀ {A} → Maybe A ⊥P → Maybe A ⊥W
  whnf ⌈ x ⌉        = ⌈ x ⌉
  whnf (later x)    = later (♭ x)
  whnf (⟦ t ⟧P ρ k) = ⟦ t ⟧W ρ k

  mutual

    ⟪_⟫W : ∀ {A} → Maybe A ⊥W → Maybe A ⊥
    ⟪ ⌈ x ⌉    ⟫W = x
    ⟪ later  x ⟫W = later (♯ ⟪ x ⟫P)

    ⟪_⟫P : ∀ {A} → Maybe A ⊥P → Maybe A ⊥
    ⟪ x ⟫P = ⟪ whnf x ⟫W

-- The actual semantics. Note that this definition gives us
-- determinism "for free".

infix 5 _∙_

⟦_⟧ : ∀ {A n} → Tm n → Env n → (Value → Maybe A ⊥) → Maybe A ⊥
⟦ t ⟧ ρ k = ⟪ ⟦ t ⟧P ρ (λ v → ⌈ k v ⌉) ⟫P
  where open Workaround₁

_∙_ : ∀ {A} → Value → Value → (Value → Maybe A ⊥) → Maybe A ⊥
(v₁ ∙ v₂) k = ⟪ (v₁ ∙W v₂) (λ v → ⌈ k v ⌉) ⟫W
  where open Workaround₁

-- ⟦_⟧ and _∙_ preserve equality of their continuations.

module Workaround₂ {k : Kind} where

  open Workaround₁

  mutual

    infix 4 _≈P_ _≈W_

    data _≈P_ {A : Set} : Maybe A ⊥ → Maybe A ⊥ → Set where
      ⌈_⌉        : ∀ {x y} (x≈y : Rel k x y) → x ≈P y
      later      : ∀ {x y} (x≈y : ∞ (♭ x ≈P ♭ y)) → later x ≈P later y
      ⟦_⟧W-congP : ∀ {n} t (ρ : Env n) {k₁ k₂ : Value → Maybe A ⊥W}
                   (k₁≈k₂ : ∀ v → ⟪ k₁ v ⟫W ≈W ⟪ k₂ v ⟫W) →
                   ⟪ ⟦ t ⟧W ρ k₁ ⟫W ≈P ⟪ ⟦ t ⟧W ρ k₂ ⟫W

    data _≈W_ {A : Set} : Maybe A ⊥ → Maybe A ⊥ → Set where
      ⌈_⌉   : ∀ {x y} (x≈y : Rel k x y) → x ≈W y
      later : ∀ {x y} (x≈y : ♭ x ≈P ♭ y) → later x ≈W later y

  mutual

    ⟦_⟧W-congW : ∀ {A n} t (ρ : Env n) {k₁ k₂ : Value → Maybe A ⊥W} →
                 (∀ v → ⟪ k₁ v ⟫W ≈W ⟪ k₂ v ⟫W) →
                 ⟪ ⟦ t ⟧W ρ k₁ ⟫W ≈W ⟪ ⟦ t ⟧W ρ k₂ ⟫W
    ⟦ con i   ⟧W-congW ρ k₁≈k₂ = k₁≈k₂ (con i)
    ⟦ var x   ⟧W-congW ρ k₁≈k₂ = k₁≈k₂ (lookup ρ x)
    ⟦ ƛ t     ⟧W-congW ρ k₁≈k₂ = k₁≈k₂ (ƛ t ρ)
    ⟦ t₁ · t₂ ⟧W-congW ρ k₁≈k₂ = ⟦ t₁ ⟧W-congW ρ (λ v₁ →
                                 ⟦ t₂ ⟧W-congW ρ (λ v₂ →
                                 (v₁ ∙W v₂ -congW) k₁≈k₂))

    _∙W_-congW : ∀ {A} v₁ v₂ {k₁ k₂ : Value → Maybe A ⊥W} →
                 (∀ v → ⟪ k₁ v ⟫W ≈W ⟪ k₂ v ⟫W) →
                 ⟪ (v₁ ∙W v₂) k₁ ⟫W ≈W ⟪ (v₁ ∙W v₂) k₂ ⟫W
    (con i  ∙W v₂ -congW) k₁≈k₂ = ⌈ fail ∎ ⌉
    (ƛ t₁ ρ ∙W v₂ -congW) k₁≈k₂ = later (⟦ t₁ ⟧W-congP (v₂ ∷ ρ) k₁≈k₂)

  whnf≈ : ∀ {A} {x y : Maybe A ⊥} → x ≈P y → x ≈W y
  whnf≈ ⌈ x≈y ⌉                = ⌈ x≈y ⌉
  whnf≈ (later x≈y)            = later (♭ x≈y)
  whnf≈ (⟦ t ⟧W-congP ρ k₁≈k₂) = ⟦ t ⟧W-congW ρ k₁≈k₂

  mutual

    soundW : ∀ {A} {x y : Maybe A ⊥} → x ≈W y → Rel k x y
    soundW ⌈ x≈y ⌉     = x≈y
    soundW (later x≈y) = later (♯ soundP x≈y)

    soundP : ∀ {A} {x y : Maybe A ⊥} → x ≈P y → Rel k x y
    soundP x≈y = soundW (whnf≈ x≈y)

⟦_⟧-cong : ∀ {k A n} t (ρ : Env n) {k₁ k₂ : Value → Maybe A ⊥} →
           (∀ v → Rel k (k₁ v) (k₂ v)) →
           Rel k (⟦ t ⟧ ρ k₁) (⟦ t ⟧ ρ k₂)
⟦ t ⟧-cong ρ k₁≈k₂ = soundW (⟦ t ⟧W-congW ρ (λ v → ⌈ k₁≈k₂ v ⌉))
  where open Workaround₂

_∙_-cong : ∀ {k A} v₁ v₂ {k₁ k₂ : Value → Maybe A ⊥} →
           (∀ v → Rel k (k₁ v) (k₂ v)) →
           Rel k ((v₁ ∙ v₂) k₁) ((v₁ ∙ v₂) k₂)
(v₁ ∙ v₂ -cong) k₁≈k₂ = soundW ((v₁ ∙W v₂ -congW) (λ v → ⌈ k₁≈k₂ v ⌉))
  where open Workaround₂

-- ⟦_⟧ and _∙_ satisfy their intended defining equations.

sem-con : ∀ {A n} i {ρ : Env n} {k : Value → Maybe A ⊥} →
          ⟦ con i ⟧ ρ k ≅ k (con i)
sem-con i {k = k} = k (con i) ∎

sem-var : ∀ {A n} x {ρ : Env n} {k : Value → Maybe A ⊥} →
          ⟦ var x ⟧ ρ k ≅ k (lookup ρ x)
sem-var x {ρ} {k} = k (lookup ρ x) ∎

sem-ƛ : ∀ {A n} t {ρ : Env n} {k : Value → Maybe A ⊥} →
        ⟦ ƛ t ⟧ ρ k ≅ k (ƛ t ρ)
sem-ƛ t {ρ} {k} = k (ƛ t ρ) ∎

sem-· : ∀ {A n} t₁ t₂ {ρ : Env n} {k : Value → Maybe A ⊥} →
        ⟦ t₁ · t₂ ⟧ ρ k ≅ (⟦ t₁ ⟧ ρ λ v₁ → ⟦ t₂ ⟧ ρ λ v₂ → (v₁ ∙ v₂) k)
sem-· t₁ t₂ {ρ} {k} = soundW $
  ⟦ t₁ ⟧W-congW ρ λ v₁ →
  ⟦ t₂ ⟧W-congW ρ λ v₂ →
  ⌈ (v₁ ∙ v₂) k ∎ ⌉
  where open Workaround₂

app-con : ∀ {A} i v₂ {k : Value → Maybe A ⊥} →
          (con i ∙ v₂) k ≅ fail
app-con i v₂ = fail ∎

app-ƛ : ∀ {A n} t₁ (ρ : Env n) v₂ {k : Value → Maybe A ⊥} →
        (ƛ t₁ ρ ∙ v₂) k ≅ later (♯ ⟦ t₁ ⟧ (v₂ ∷ ρ) k)
app-ƛ t₁ ρ v₂ {k} = later (♯ (⟦ t₁ ⟧ (v₂ ∷ ρ) k ∎))

-- ⟦_⟧ and _∙_ are the unique solutions to the system of equations
-- which is intended to define them. I have stated this result using
-- strong equality, which is (more or less) the kind of equality you
-- get from a definition. I tried using weak equality instead, but
-- this turned out to make the proof tricky (due to the lack of
-- transitivity).

module Unique
  {A : Set}
  (⟪_⟫ : ∀ {n} t (ρ : Env n) (k : Value → Maybe A ⊥) → Maybe A ⊥)
  (_○_ : Value → Value → (Value → Maybe A ⊥) → Maybe A ⊥)

  (⟪con⟫ : ∀ {n} i {ρ : Env n} {k : Value → Maybe A ⊥} →
   ⟪ con i ⟫ ρ k ≅ k (con i))
  (⟪var⟫ : ∀ {n} x {ρ : Env n} {k : Value → Maybe A ⊥} →
   ⟪ var x ⟫ ρ k ≅ k (lookup ρ x))
  (⟪ƛ⟫ : ∀ {n} t {ρ : Env n} {k : Value → Maybe A ⊥} →
   ⟪ ƛ t ⟫ ρ k ≅ k (ƛ t ρ))
  (⟪·⟫ : ∀ {n} t₁ t₂ {ρ : Env n} {k : Value → Maybe A ⊥} →
   ⟪ t₁ · t₂ ⟫ ρ k ≅ (⟪ t₁ ⟫ ρ λ v₁ → ⟪ t₂ ⟫ ρ λ v₂ → (v₁ ○ v₂) k))

  (con○ : ∀ i v₂ {k : Value → Maybe A ⊥} →
   (con i ○ v₂) k ≅ fail)
  (ƛ○ : ∀ {n} t₁ (ρ : Env n) v₂ {k : Value → Maybe A ⊥} →
   (ƛ t₁ ρ ○ v₂) k ≅ later (♯ ⟪ t₁ ⟫ (v₂ ∷ ρ) k))
  where

  infix  4 _≅P_ _≅W_
  infixr 2 _≅⟨_⟩P_ _≅⟨_⟩W_ _≅⟪_⟫P_ _≅⟪_⟫W_

  mutual

    data _≅P_ : Maybe A ⊥ → Maybe A ⊥ → Set where
      _≅⟨_⟩P_ : ∀ x {y z} (x≅y : x ≅  y) (y≅z : y ≅P z) → x ≅P z
      _≅⟪_⟫P_ : ∀ x {y z} (x≅y : x ≅P y) (y≅z : y ≅  z) → x ≅P z
      semP    : ∀ {n} t {ρ : Env n} {k₁ k₂ : Value → Maybe A ⊥} →
                (k₁≅k₂ : ∀ v → k₁ v ≅W k₂ v) →
                ⟪ t ⟫ ρ k₁ ≅P ⟦ t ⟧ ρ k₂

    data _≅W_ : Maybe A ⊥ → Maybe A ⊥ → Set where
      ⌈_⌉    : ∀ {x y} (x≅y :   x ≅    y) →       x ≅W       y
      later  : ∀ {x y} (x≅y : ♭ x ≅P ♭ y) → later x ≅W later y

  _≅⟨_⟩W_ : ∀ x {y z} → x ≅ y → y ≅W z → x ≅W z
  _  ≅⟨ x≅y       ⟩W ⌈ y≅z ⌉    = ⌈ _ ≅⟨ x≅y ⟩ y≅z ⌉
  ._ ≅⟨ later x≅y ⟩W later  y≅z = later (_ ≅⟨ ♭ x≅y ⟩P y≅z)

  _≅⟪_⟫W_ : ∀ x {y z} → x ≅W y → y ≅ z → x ≅W z
  _  ≅⟪ ⌈ x≅y ⌉   ⟫W       y≅z = ⌈ _ ≅⟨ x≅y ⟩ y≅z ⌉
  ._ ≅⟪ later x≅y ⟫W later y≅z = later (_ ≅⟪ x≅y ⟫P ♭ y≅z)

  mutual

    semW : ∀ {n} t {ρ : Env n} {k₁ k₂ : Value → Maybe A ⊥} →
           (∀ v → k₁ v ≅W k₂ v) → ⟪ t ⟫ ρ k₁ ≅W ⟦ t ⟧ ρ k₂
    semW (con i) {ρ} {k₁} {k₂} k₁≅k₂ =
      ⟪ con i ⟫ ρ k₁  ≅⟨ ⟪con⟫ i ⟩W
      k₁ (con i)      ≅⟪ k₁≅k₂ _ ⟫W
      k₂ (con i)      ∎
    semW (var x) {ρ} {k₁} {k₂} k₁≅k₂ =
      ⟪ var x ⟫ ρ k₁   ≅⟨ ⟪var⟫ x ⟩W
      k₁ (lookup ρ x)  ≅⟪ k₁≅k₂ _ ⟫W
      k₂ (lookup ρ x)  ∎
    semW (ƛ t) {ρ} {k₁} {k₂} k₁≅k₂ =
      ⟪ ƛ t ⟫ ρ k₁  ≅⟨ ⟪ƛ⟫ t ⟩W
      k₁ (ƛ t ρ)    ≅⟪ k₁≅k₂ _ ⟫W
      k₂ (ƛ t ρ)    ∎
    semW (t₁ · t₂) {ρ} {k₁} {k₂} k₁≅k₂ =
      ⟪ t₁ · t₂ ⟫ ρ k₁                                ≅⟨ ⟪·⟫ t₁ t₂ ⟩W
      (⟪ t₁ ⟫ ρ λ v₁ → ⟪ t₂ ⟫ ρ λ v₂ → (v₁ ○ v₂) k₁)  ≅⟪ semW t₁ (λ v₁ → semW t₂ (λ v₂ → appW v₁ v₂ k₁≅k₂)) ⟫W
      (⟦ t₁ ⟧ ρ λ v₁ → ⟦ t₂ ⟧ ρ λ v₂ → (v₁ ∙ v₂) k₂)  ≅⟨ sym $ sem-· t₁ t₂ ⟩
      ⟦ t₁ · t₂ ⟧ ρ k₂                                ∎

    appW : ∀ v₁ v₂ {k₁ k₂ : Value → Maybe A ⊥} →
           (∀ v → k₁ v ≅W k₂ v) → (v₁ ○ v₂) k₁ ≅W (v₁ ∙ v₂) k₂
    appW (con i) v₂ {k₁} {k₂} k₁≅k₂ =
      ⌈ (con i ○ v₂) k₁  ≅⟨ con○ i v₂ ⟩
        fail             ∎ ⌉
    appW (ƛ t₁ ρ) v₂ {k₁} {k₂} k₁≅k₂ =
      (ƛ t₁ ρ ○ v₂) k₁  ≅⟨ ƛ○ t₁ ρ v₂ ⟩W
      later _           ≅⟪ later (semP t₁ k₁≅k₂) ⟫W
      (ƛ t₁ ρ ∙ v₂) k₂  ∎

  whnf : ∀ {x y} → x ≅P y → x ≅W y
  whnf (x ≅⟨ x≅y ⟩P y≅z) = x ≅⟨      x≅y ⟩W whnf y≅z
  whnf (x ≅⟪ x≅y ⟫P y≅z) = x ≅⟪ whnf x≅y ⟫W      y≅z
  whnf (semP t k₁≅k₂)    = semW t k₁≅k₂

  mutual

    soundW : ∀ {x y} → x ≅W y → x ≅ y
    soundW ⌈ x≅y ⌉     = x≅y
    soundW (later x≅y) = later (♯ soundP x≅y)

    soundP : ∀ {x y} → x ≅P y → x ≅ y
    soundP x≅y = soundW (whnf x≅y)

  sem : ∀ {n} t {ρ : Env n} {k : Value → Maybe A ⊥} →
        ⟪ t ⟫ ρ k ≅ ⟦ t ⟧ ρ k
  sem t {k = k} = soundW (semW t (λ v → ⌈ k v ∎ ⌉))

  dot : ∀ v₁ v₂ {k : Value → Maybe A ⊥} →
        (v₁ ○ v₂) k ≅ (v₁ ∙ v₂) k
  dot v₁ v₂ {k} = soundW (appW v₁ v₂ (λ v → ⌈ k v ∎ ⌉))

------------------------------------------------------------------------
-- Example

Ω-loops : ⟦ Ω ⟧ [] return ≈ never
Ω-loops = later (♯ Ω-loops)

------------------------------------------------------------------------
-- Compiler correctness

module Correctness {k : OtherKind} where

  infix  4 _≈P_ _≈W_
  infixr 2 _≡⟨_⟩W_ _≈⟨_⟩P_ _≈⟨_⟩W_

  mutual

    data _≈P_ : Maybe VM.Value ⊥ → Maybe VM.Value ⊥ → Set where
      _≈⟨_⟩P_ : ∀ x {y z} (x≈y : x ≈P y) (y≅z : y ≅ z) → x ≈P z
      correct :
        ∀ {n} t {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
        (hyp : ∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩
                       ≈W k v) →
        exec ⟨ comp t c , s , comp-env ρ ⟩ ≈P ⟦ t ⟧ ρ k

    data _≈W_ : Maybe VM.Value ⊥ → Maybe VM.Value ⊥ → Set where
      ⌈_⌉    : ∀ {x y} (x≈y : Rel (other k) x y) → x ≈W y
      later  : ∀ {x y} (x≈y : ♭ x ≈P ♭ y) → later x ≈W later y
      laterˡ : ∀ {x y} (x≈y : ♭ x ≈W   y) → later x ≈W       y

  _≡⟨_⟩W_ : ∀ x {y z} → x ≡ y → y ≈W z → x ≈W z
  _ ≡⟨ P.refl ⟩W y≈z = y≈z

  _≈⟨_⟩W_ : ∀ x {y z} → x ≈W y → y ≅ z → x ≈W z
  ._ ≈⟨ later  x≈y ⟩W later y≅z = later  (_ ≈⟨ x≈y ⟩P ♭ y≅z)
  ._ ≈⟨ laterˡ x≈y ⟩W       y≅z = laterˡ (_ ≈⟨ x≈y ⟩W   y≅z)
  _  ≈⟨ ⌈ x≈y ⌉    ⟩W       y≅z = ⌈ trans x≈y (Partiality.≅⇒ y≅z) ⌉
    where trans = Preorder.trans (Partiality.preorder P.isPreorder _)

  mutual

    correctW :
      ∀ {n} t {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈W k v) →
      exec ⟨ comp t c , s , comp-env ρ ⟩ ≈W ⟦ t ⟧ ρ k
    correctW (con i) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (Lambda.Syntax.Closure.con i) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (con i) ⟩W
      k (con i)                                                        ∎)
    correctW (var x) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (lookup (comp-env ρ) x) ∷ s , comp-env ρ ⟩  ≡⟨ P.cong (λ v → exec ⟨ c , val v ∷ s , comp-env ρ ⟩) $ lookup-hom x ρ ⟩W
      exec ⟨ c , val (comp-val (lookup ρ x)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (lookup ρ x) ⟩W
      k (lookup ρ x)                                             ∎)
    correctW (ƛ t) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (comp-val (ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (ƛ t ρ) ⟩W
      k (ƛ t ρ)                                             ∎)
    correctW (t₁ · t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩  ≈⟨ correctW t₁ (λ v₁ → correctW t₂ (λ v₂ → ∙-correctW v₁ v₂ hyp)) ⟩W
      (⟦ t₁ ⟧ ρ λ v₁ → ⟦ t₂ ⟧ ρ λ v₂ → (v₁ ∙ v₂) k)          ≅⟨ sym $ sem-· t₁ t₂ ⟩
      ⟦ t₁ · t₂ ⟧ ρ k                                        ∎

    ∙-correctW :
      ∀ {n} v₁ v₂ {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈W k v) →
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s , comp-env ρ ⟩ ≈W
      (v₁ ∙ v₂) k
    ∙-correctW (con i)   v₂                 _   = ⌈ fail ∎ ⌉
    ∙-correctW (ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val (ƛ t₁ ρ₁)) ∷ s , comp-env ρ ⟩  ≈⟨ later (

        exec ⟨ comp t₁ [ ret ] , ret c (comp-env ρ) ∷ s , comp-env (v₂ ∷ ρ₁) ⟩               ≈⟨ correct t₁ (λ v → laterˡ (hyp v)) ⟩P
        (⟦ t₁ ⟧ (v₂ ∷ ρ₁) k)                                                                 ∎) ⟩W

      (ƛ t₁ ρ₁ ∙ v₂) k                                                                  ∎

  whnf : ∀ {x y} → x ≈P y → x ≈W y
  whnf (x ≈⟨ x≈y ⟩P y≅z) = x ≈⟨ whnf x≈y ⟩W y≅z
  whnf (correct t hyp)   = correctW t hyp

  mutual

    soundW : ∀ {x y} → x ≈W y → Rel (other k) x y
    soundW ⌈ x≈y ⌉      = x≈y
    soundW (later  x≈y) = later (♯ soundP x≈y)
    soundW (laterˡ x≈y) = laterˡ (soundW x≈y)

    soundP : ∀ {x y} → x ≈P y → Rel (other k) x y
    soundP x≈y = soundW (whnf x≈y)

correct : ∀ t →
          exec ⟨ comp t [] , [] , [] ⟩ ≈
          ⟦ t ⟧ [] (λ v → return (comp-val v))
correct t =
  soundP $ Correctness.correct t (λ v → ⌈ return (comp-val v) ∎ ⌉)
  where open Correctness

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-
Reported by sattler.christian, Oct 10 (3 days ago)

This is a funny one. The below code snippet produces the following error under the current Agda development version:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Eliminators.hs:85

Note the spurious Tm datatype that isn't used anywhere? Remove it, move its declaration forward, or its definition backward, and the internal error vanishes, leaving a few yellow spots.

Now uncomment the two implicit arguments at the bottom of the code. All metavars are now resolved. Now put the Tm datatype back in - yellow spots reappear, but different from before!
-}

{-# OPTIONS --cubical-compatible #-}
module Issue918 where

record ⊤ : Set where
  constructor tt

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

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

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
g ∘ f = λ x → g (f x)

_+'_ : ℕ → ℕ → ℕ
i +' zero  = i
i +' suc j = suc i +' j

U : ℕ → Set
U zero    = ⊤
U (suc n) = Σ (U n) (λ _ → ⊤)

V : ℕ → Set
V zero    = ⊤
V (suc m) = Σ ⊤ (λ _ → V m)

combine : {i j : ℕ} → Σ (U i) (λ _ → V j) → U (i +' j)
combine {j = zero}  = λ {(A , _) → A}
combine {j = suc j} = combine {j = j} ∘ (λ {(Γ , (A , T)) → ((Γ , A) , T)})

data Tm : Set

ctx-hom : (m : ℕ) → U m → Set
ctx-hom zero    _       = ⊤
ctx-hom (suc m) (Δ , _) = Σ (ctx-hom m Δ) (λ _ → ⊤)

ctx-hom-split-iso : {m k : ℕ} {Δ : U m} {T : V k}
                  → ctx-hom (m +' k) (combine (Δ , T))
                  → Σ (ctx-hom m Δ) (λ _ → V k)
ctx-hom-split-iso {k = zero}  = λ Δ → (Δ , tt)
ctx-hom-split-iso {m} {k = suc k} {Δ} {(A , T)} =
    ((λ {((Γ , A) , T) → (Γ , (A , T))}))
  ∘ ctx-hom-split-iso {m = suc m} --{Δ = (Δ , A)}

data Tm where

{- Project Member #1 andreas.m.abel

That was quite a riddle to solve.

1. The internal error is actually triggered in the termination checking phase.
   I fixed this, will push soon.
   A workaround is --no-termination-check

2. The data-Tm-brace puts ctx-hom and ctx-hom-split-iso into a mutual block.
   This prevents ctx-hom to be unfolded during checking the -split-iso.
   You can achieve the same by explicitely putting the two defs into a mutual
   block.
   If the mutual block is removed, the yellow stuff appears.
   HO-unification is sensitive to reduction, at this moment I do not see an
   easy fix for this behavior.

3. "yellow spots reappear, but in different places"  I could not replay this.
   For me, the yellow only disappeared if I also gave {T = T}, but then
   it consistently disappears and reappears when putting in and out of a mutual
   block.

-}

ext: agda


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

module Luau.RuntimeError where

open import Agda.Builtin.Equality using (_≡_)
open import Luau.Heap using (Heap; _[_])
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String)
open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; string; binexp; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (RuntimeType; valueType; function; number; string)
open import Properties.Equality using (_≢_)

data BinOpError : BinaryOperator → RuntimeType → Set where
  + : ∀ {t} → (t ≢ number) → BinOpError + t
  - : ∀ {t} → (t ≢ number) → BinOpError - t
  * : ∀ {t} → (t ≢ number) → BinOpError * t
  / : ∀ {t} → (t ≢ number) → BinOpError / t
  < : ∀ {t} → (t ≢ number) → BinOpError < t
  > : ∀ {t} → (t ≢ number) → BinOpError > t
  <= : ∀ {t} → (t ≢ number) → BinOpError <= t
  >= : ∀ {t} → (t ≢ number) → BinOpError >= t
  ·· : ∀ {t} → (t ≢ string) → BinOpError ·· t

data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set

data RuntimeErrorᴱ H where
  FunctionMismatch : ∀ v w → (valueType v ≢ function) → RuntimeErrorᴱ H (val v $ val w)
  BinOpMismatch₁ : ∀ v w {op} → (BinOpError op (valueType v)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
  BinOpMismatch₂ : ∀ v w {op} → (BinOpError op (valueType w)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
  UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x)
  SEGV : ∀ {a} → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (val (addr a))
  app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
  app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
  block : ∀ {b B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
  bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
  bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)

data RuntimeErrorᴮ H where
  local : ∀ {x M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
  return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
module Numeral.Natural.Oper.Modulo.Proofs.DivisibilityWithRemainder where

open import Data
open import Functional
open import Numeral.Finite
import      Numeral.Finite.Proofs as 𝕟
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs.Algorithm
open import Numeral.Natural.Relation.DivisibilityWithRemainder hiding (base₀ ; base₊ ; step)
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator
open import Syntax.Transitivity

-- The remainder of the divisibility relation is given by the modulo operation.
[mod][∣ᵣₑₘ]-remainder-equality : ∀{x y r}{p : (𝐒(y) ∣ᵣₑₘ x)(r)} → ((x mod 𝐒(y)) ≡ 𝕟-to-ℕ ([∣ᵣₑₘ]-remainder p))
[mod][∣ᵣₑₘ]-remainder-equality {𝟎}             {_}   {𝟎}   {DivRem𝟎} = [≡]-intro
[mod][∣ᵣₑₘ]-remainder-equality {𝐒 .(𝕟-to-ℕ r)} {𝐒 y} {𝐒 r} {DivRem𝟎} = mod'-lesser-dividend {1}{𝐒(y)}{𝕟-to-ℕ r}{y} ([≤]-without-[𝐒] 𝕟.bounded)
[mod][∣ᵣₑₘ]-remainder-equality {𝐒 x}        {𝟎} {𝟎} {DivRem𝐒 p}      = mod'-zero-all-except-dividend {x}
{-# CATCHALL #-}
[mod][∣ᵣₑₘ]-remainder-equality {𝐒 .(x + y)} {y} {r} {DivRem𝐒 {x = x} p} =
  ([ 𝟎 , y ] 𝐒(x + y) mod' y)           🝖[ _≡_ ]-[]
  ([ 𝟎 , y ] (𝐒(x) + y) mod' y)         🝖[ _≡_ ]-[ mod'-sumᵣ-modulo {0}{y}{x}{y} ]
  ([ 𝟎 , y ] x mod' y)                  🝖[ _≡_ ]-[ [mod][∣ᵣₑₘ]-remainder-equality {p = p} ]
  𝕟-to-ℕ ([∣ᵣₑₘ]-remainder p)           🝖[ _≡_ ]-[]
  𝕟-to-ℕ ([∣ᵣₑₘ]-remainder (DivRem𝐒 p)) 🝖-end

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:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Definition
open import Rings.Definition
open import Setoids.Setoids

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Fields.Fields where

record Field {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) : Set (lsuc m ⊔ n) where
  open Ring R
  open Group additiveGroup
  open Setoid S
  field
    allInvertible : (a : A) → ((a ∼ Group.0G (Ring.additiveGroup R)) → False) → Sg A (λ t → t * a ∼ 1R)
    nontrivial : (0R ∼ 1R) → False
  0F : A
  0F = Ring.0R R

record Field' {m n : _} : Set (lsuc m ⊔ lsuc n) where
  field
    A : Set m
    S : Setoid {m} {n} A
    _+_ : A → A → A
    _*_ : A → A → A
    R : Ring S _+_ _*_
    isField : Field R

encapsulateField : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) → Field'
encapsulateField {A = A} {S = S} {_+_} {_*_} {R} F = record { A = A ; S = S ; _+_ = _+_ ; _*_ = _*_ ; R = R ; isField = F }

{-
record OrderedField {n} {A : Set n} {R : Ring A} (F : Field R) : Set (lsuc n) where
  open Field F
  field
    ord : TotalOrder A
  open TotalOrder ord
  open Ring R
  field
    productPos : {a b : A} → (0R < a) → (0R < b) → (0R < (a * b))
    orderRespectsAddition : {a b c : A} → (a < b) → (a + c) < (b + c)

-}


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

module PiEquiv where

open import Data.Empty
open import Data.Unit
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂)
open import Function using (_∘_; id)

open import Equiv
open import EquivEquiv
open _≋_
open import TypeEquiv as TE
open import TypeEquivEquiv
-- open import TypeEquivCat
open import PiU
open import PiLevel0
open import PiLevel1

open import Data.Sum.Properties2
open import Data.SumProd.Properties

------------------------------------------------------------------------------
-- A combinator t₁ ⟷ t₂ denotes an equivalence to types
-- note how we don't have to look at the types at all.

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

eval : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₁ ⟧ → ⟦ t₂ ⟧
eval unite₊l (inj₁ ())
eval unite₊l (inj₂ v) = v
eval uniti₊l v = inj₂ v
eval unite₊r (inj₁ x) = x
eval unite₊r (inj₂ ())
eval uniti₊r v = inj₁ v
eval swap₊ (inj₁ v) = inj₂ v
eval swap₊ (inj₂ v) = inj₁ v
eval assocl₊ (inj₁ v) = inj₁ (inj₁ v)
eval assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
eval assocl₊ (inj₂ (inj₂ v)) = inj₂ v
eval assocr₊ (inj₁ (inj₁ v)) = inj₁ v
eval assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
eval assocr₊ (inj₂ v) = inj₂ (inj₂ v)
eval unite⋆l (tt , v) = v
eval uniti⋆l v = (tt , v)
eval unite⋆r (v , tt) = v
eval uniti⋆r v = v , tt
eval swap⋆ (v₁ , v₂) = (v₂ , v₁)
eval assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
eval assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
eval absorbr (x , _) = x
eval absorbl (_ , y) = y
eval factorzl ()
eval factorzr ()
eval dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
eval dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
eval factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
eval factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
eval distl (v , inj₁ x) = inj₁ (v , x)
eval distl (v , inj₂ y) = inj₂ (v , y)
eval factorl (inj₁ (x , y)) = x , inj₁ y
eval factorl (inj₂ (x , y)) = x , inj₂ y
eval id⟷ v = v
eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₁ v) = inj₁ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₂ v) = inj₂ (eval c₂ v)
eval (c₁ ⊗ c₂) (v₁ , v₂) = (eval c₁ v₁ , eval c₂ v₂)

-- useful to have the backwards eval too

evalB : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₂ ⟧ → ⟦ t₁ ⟧
evalB unite₊l x = inj₂ x
evalB uniti₊l (inj₁ ())
evalB uniti₊l (inj₂ y) = y
evalB unite₊r v = inj₁ v
evalB uniti₊r (inj₁ x) = x
evalB uniti₊r (inj₂ ())
evalB swap₊ (inj₁ x) = inj₂ x
evalB swap₊ (inj₂ y) = inj₁ y
evalB assocl₊ (inj₁ (inj₁ x)) = inj₁ x
evalB assocl₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
evalB assocl₊ (inj₂ y) = inj₂ (inj₂ y)
evalB assocr₊ (inj₁ x) = inj₁ (inj₁ x)
evalB assocr₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
evalB assocr₊ (inj₂ (inj₂ y)) = inj₂ y
evalB unite⋆l x = tt , x
evalB uniti⋆l (tt , x) = x
evalB unite⋆r v = v , tt
evalB uniti⋆r (v , tt) = v
evalB swap⋆ (x , y) = y , x
evalB assocl⋆ ((x , y) , z) = x , y , z
evalB assocr⋆ (x , y , z) = (x , y) , z
evalB absorbr ()
evalB absorbl ()
evalB factorzr (_ , x) = x
evalB factorzl (x , _) = x
evalB dist (inj₁ (x , y)) = inj₁ x , y
evalB dist (inj₂ (x , y)) = inj₂ x , y
evalB factor (inj₁ x , z) = inj₁ (x , z)
evalB factor (inj₂ y , z) = inj₂ (y , z)
evalB distl (inj₁ (x , y)) = x , inj₁ y
evalB distl (inj₂ (x , y)) = x , inj₂ y
evalB factorl (v , inj₁ x) = inj₁ (v , x)
evalB factorl (v , inj₂ y) = inj₂ (v , y)
evalB id⟷ x = x
evalB (c₀ ◎ c₁) x = evalB c₀ (evalB c₁ x)
evalB (c₀ ⊕ c₁) (inj₁ x) = inj₁ (evalB c₀ x)
evalB (c₀ ⊕ c₁) (inj₂ y) = inj₂ (evalB c₁ y)
evalB (c₀ ⊗ c₁) (x , y) = evalB c₀ x , evalB c₁ y

-- should probably prove that these are inverses!
-- to a certain extent, no need, because here's
-- the right way to do it:

c2equiv : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → ⟦ t₁ ⟧ ≃ ⟦ t₂ ⟧
c2equiv unite₊l = TE.unite₊equiv
c2equiv uniti₊l = TE.uniti₊equiv
c2equiv unite₊r = TE.unite₊′equiv
c2equiv uniti₊r = TE.uniti₊′equiv
c2equiv swap₊ = TE.swap₊equiv
c2equiv assocl₊ = TE.assocl₊equiv
c2equiv assocr₊ = TE.assocr₊equiv
c2equiv unite⋆l = TE.unite⋆equiv
c2equiv uniti⋆l = TE.uniti⋆equiv
c2equiv unite⋆r = TE.unite⋆′equiv
c2equiv uniti⋆r = TE.uniti⋆′equiv
c2equiv swap⋆ = TE.swap⋆equiv
c2equiv assocl⋆ = TE.assocl⋆equiv
c2equiv assocr⋆ = TE.assocr⋆equiv
c2equiv absorbr = TE.distzequiv
c2equiv absorbl = TE.distzrequiv
c2equiv factorzr = TE.factorzrequiv
c2equiv factorzl = TE.factorzequiv
c2equiv dist = TE.distequiv
c2equiv factor = TE.factorequiv
c2equiv distl = TE.distlequiv
c2equiv factorl = TE.factorlequiv
c2equiv id⟷ = id≃
c2equiv (c ◎ c₁) = c2equiv c₁ ● c2equiv c
c2equiv (c ⊕ c₁) = (c2equiv c) ⊎≃ (c2equiv c₁)
c2equiv (c ⊗ c₁) = (c2equiv c) ×≃ (c2equiv c₁)

-- and these are 'coherent'
-- first with evaluation:

lemma0 : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → (v : ⟦ t₁ ⟧) →
  eval c v ≡ proj₁ (c2equiv c) v
lemma0 unite₊l (inj₁ ())
lemma0 unite₊l (inj₂ y) = refl
lemma0 uniti₊l v = refl
lemma0 unite₊r (inj₁ x) = refl
lemma0 unite₊r (inj₂ ())
lemma0 uniti₊r v = refl
lemma0 PiLevel0.swap₊ (inj₁ x) = refl
lemma0 PiLevel0.swap₊ (inj₂ y) = refl
lemma0 PiLevel0.assocl₊ (inj₁ x) = refl
lemma0 PiLevel0.assocl₊ (inj₂ (inj₁ x)) = refl
lemma0 PiLevel0.assocl₊ (inj₂ (inj₂ y)) = refl
lemma0 PiLevel0.assocr₊ (inj₁ (inj₁ x)) = refl
lemma0 PiLevel0.assocr₊ (inj₁ (inj₂ y)) = refl
lemma0 PiLevel0.assocr₊ (inj₂ y) = refl
lemma0 unite⋆l v = refl -- yay for η !
lemma0 uniti⋆l v = refl
lemma0 unite⋆r v = refl
lemma0 uniti⋆r v = refl
lemma0 PiLevel0.swap⋆ v = refl
lemma0 PiLevel0.assocl⋆ v = refl
lemma0 PiLevel0.assocr⋆ v = refl
lemma0 absorbr v = refl
lemma0 absorbl v = refl
lemma0 factorzr ()
lemma0 factorzl ()
lemma0 PiLevel0.dist (inj₁ x , proj₂) = refl
lemma0 PiLevel0.dist (inj₂ y , proj₂) = refl
lemma0 PiLevel0.factor (inj₁ x) = refl
lemma0 PiLevel0.factor (inj₂ y) = refl
lemma0 PiLevel0.distl (proj₁ , inj₁ x) = refl
lemma0 PiLevel0.distl (proj₁ , inj₂ y) = refl
lemma0 PiLevel0.factorl (inj₁ x) = refl
lemma0 PiLevel0.factorl (inj₂ y) = refl
lemma0 id⟷ v = refl
lemma0 (c ◎ c₁) v =
  trans (cong (eval c₁) (lemma0 c v)) (
  trans (lemma0 c₁ (proj₁ (c2equiv c) v))
        (sym (β₁ v)))
lemma0 (c ⊕ c₁) (inj₁ x) =
  trans (cong inj₁ (lemma0 c x)) (sym (β⊎₁ (inj₁ x)))
lemma0 (c ⊕ c₁) (inj₂ y) =
 trans (cong inj₂ (lemma0 c₁ y)) (sym (β⊎₁ (inj₂ y)))
lemma0 (c ⊗ c₁) (x , y) =
  trans (cong₂ _,_ (lemma0 c x) (lemma0 c₁ y)) (sym (β×₁ (x , y)))

lemma1 : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → (v : ⟦ t₂ ⟧) →
  evalB c v ≡ proj₁ (sym≃ (c2equiv c)) v
lemma1 PiLevel0.unite₊l v = refl
lemma1 PiLevel0.uniti₊l (inj₁ ())
lemma1 PiLevel0.uniti₊l (inj₂ y) = refl
lemma1 PiLevel0.unite₊r v = refl
lemma1 uniti₊r (inj₁ x) = refl
lemma1 uniti₊r (inj₂ ())
lemma1 PiLevel0.swap₊ (inj₁ x) = refl
lemma1 PiLevel0.swap₊ (inj₂ y) = refl
lemma1 PiLevel0.assocl₊ (inj₁ (inj₁ x)) = refl
lemma1 PiLevel0.assocl₊ (inj₁ (inj₂ y)) = refl
lemma1 PiLevel0.assocl₊ (inj₂ y) = refl
lemma1 PiLevel0.assocr₊ (inj₁ x) = refl
lemma1 PiLevel0.assocr₊ (inj₂ (inj₁ x)) = refl
lemma1 PiLevel0.assocr₊ (inj₂ (inj₂ y)) = refl
lemma1 PiLevel0.unite⋆l v = refl
lemma1 PiLevel0.uniti⋆l (tt , x) = refl
lemma1 PiLevel0.unite⋆r v = refl
lemma1 uniti⋆r (x , tt) = refl
lemma1 PiLevel0.swap⋆ (x , y) = refl
lemma1 PiLevel0.assocl⋆ ((x , y) , z) = refl
lemma1 PiLevel0.assocr⋆ (x , y , z) = refl
lemma1 absorbr ()
lemma1 absorbl ()
lemma1 PiLevel0.factorzr (_ , ())
lemma1 factorzl (() , v)
lemma1 PiLevel0.dist (inj₁ (proj₁ , proj₂)) = refl
lemma1 PiLevel0.dist (inj₂ (proj₁ , proj₂)) = refl
lemma1 PiLevel0.factor (inj₁ x , proj₂) = refl
lemma1 PiLevel0.factor (inj₂ y , proj₂) = refl
lemma1 PiLevel0.distl (inj₁ (proj₁ , proj₂)) = refl
lemma1 PiLevel0.distl (inj₂ (proj₁ , proj₂)) = refl
lemma1 PiLevel0.factorl (v , inj₁ x) = refl
lemma1 PiLevel0.factorl (v , inj₂ y) = refl
lemma1 id⟷ v = refl
lemma1 (c₀ ◎ c₁) v = trans (
  trans (cong (evalB c₀) (lemma1 c₁ v)) (lemma1 c₀ (gg (c2equiv c₁) v)) )
  (sym (β₂ v))
lemma1 (c₀ ⊕ c₁) (inj₁ x) = trans (cong inj₁ (lemma1 c₀ x)) (sym (β⊎₂ (inj₁ x))) -- cong inj₁ (lemma1 c₀ x)
lemma1 (c₀ ⊕ c₁) (inj₂ y) = trans (cong inj₂ (lemma1 c₁ y)) (sym (β⊎₂ (inj₂ y)))
lemma1 (c₀ ⊗ c₁) (x , y) = trans (cong₂ _,_ (lemma1 c₀ x) (lemma1 c₁ y)) (sym (β×₂ (x , y)))

-- and with reverse
!≡sym≃ : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) →
  c2equiv (! c) ≋ sym≃ (c2equiv c)
!≡sym≃ unite₊l = id≋
!≡sym≃ uniti₊l = id≋
!≡sym≃ unite₊r = id≋
!≡sym≃ uniti₊r = id≋
!≡sym≃ PiLevel0.swap₊ = id≋
!≡sym≃ PiLevel0.assocl₊ = id≋
!≡sym≃ PiLevel0.assocr₊ = id≋
!≡sym≃ unite⋆l = id≋
!≡sym≃ uniti⋆l = id≋
!≡sym≃ unite⋆r = id≋
!≡sym≃ uniti⋆r = id≋
!≡sym≃ PiLevel0.swap⋆ = id≋
!≡sym≃ PiLevel0.assocl⋆ = id≋
!≡sym≃ PiLevel0.assocr⋆ = id≋
!≡sym≃ absorbr = id≋
!≡sym≃ absorbl = id≋
!≡sym≃ PiLevel0.factorzr = id≋
!≡sym≃ factorzl = id≋
!≡sym≃ PiLevel0.dist = id≋
!≡sym≃ PiLevel0.factor = id≋
!≡sym≃ PiLevel0.distl = id≋
!≡sym≃ PiLevel0.factorl = id≋
!≡sym≃ id⟷ = id≋
!≡sym≃ (c ◎ c₁) = trans≋ (EquivEquiv._◎_ (!≡sym≃ c) (!≡sym≃ c₁)) (sym≋ sym≃●)
!≡sym≃ (c ⊕ c₁) = trans≋ ((!≡sym≃ c) ⊎≋ (!≡sym≃ c₁)) (sym≋ sym≃-distrib⊎)
!≡sym≃ (c ⊗ c₁) = trans≋ ((!≡sym≃ c) ×≋ (!≡sym≃ c₁)) (sym≋ sym≃-distrib×)

left-inv : {t₁ t₂ : U} (c : t₁ ⟷ t₂) →
  (c2equiv (! c) ● c2equiv c) ≋ id≃
left-inv c =
  let p = c2equiv c in
  trans≋ (!≡sym≃ c EquivEquiv.◎ id≋) (linv≋ p)

right-inv : {t₁ t₂ : U} (c : t₁ ⟷ t₂) →
  (c2equiv c ● c2equiv (! c)) ≋ id≃
right-inv c =
  let p = c2equiv c in
  trans≋ (id≋ EquivEquiv.◎ (!≡sym≃ c)) (rinv≋ p)

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

cc2equiv : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} (ce : c₁ ⇔ c₂) →
  c2equiv c₁ ≋ c2equiv c₂
cc2equiv assoc◎l = ●-assoc
cc2equiv assoc◎r = ●-assocl
cc2equiv assocl⊕l = assocl₊-nat
cc2equiv assocl⊕r = sym≋ assocl₊-nat
cc2equiv assocl⊗l = assocl⋆-nat
cc2equiv assocl⊗r = sym≋ assocl⋆-nat
cc2equiv assocr⊕r = assocr₊-nat
cc2equiv assocr⊗l = sym≋ assocr⋆-nat
cc2equiv assocr⊗r = assocr⋆-nat
cc2equiv assocr⊕l = sym≋ assocr₊-nat
cc2equiv dist⇔l = dist-nat
cc2equiv dist⇔r = sym≋ dist-nat
cc2equiv distl⇔l = distl-nat
cc2equiv distl⇔r = sym≋ distl-nat
cc2equiv factor⇔l = factor-nat
cc2equiv factor⇔r = sym≋ factor-nat
cc2equiv factorl⇔l = factorl-nat
cc2equiv factorl⇔r = sym≋ factorl-nat
cc2equiv idl◎l = rid≋
cc2equiv idl◎r = sym≋ rid≋
cc2equiv idr◎l = lid≋
cc2equiv idr◎r = sym≋ lid≋
cc2equiv (linv◎l {c = c}) = left-inv c
cc2equiv (linv◎r {c = c}) = sym≋ (left-inv c)
cc2equiv (rinv◎l {c = c}) = right-inv c
cc2equiv (rinv◎r {c = c}) = sym≋ (right-inv c)
cc2equiv (unite₊l⇔l {c₁ = c₁} {c₂}) = sym≋ (unite₊-nat {f = c2equiv c₂})
cc2equiv unite₊l⇔r = unite₊-nat
cc2equiv uniti₊l⇔l = sym≋ uniti₊-nat
cc2equiv uniti₊l⇔r = uniti₊-nat
cc2equiv unite₊r⇔l = sym≋ unite₊′-nat
cc2equiv unite₊r⇔r = unite₊′-nat
cc2equiv uniti₊r⇔l = sym≋ uniti₊′-nat
cc2equiv uniti₊r⇔r = uniti₊′-nat
cc2equiv swapl₊⇔ = sym≋ swap₊-nat
cc2equiv swapr₊⇔ = swap₊-nat
cc2equiv unitel⋆⇔l = sym≋ unite⋆-nat
cc2equiv uniter⋆⇔l = unite⋆-nat
cc2equiv unitil⋆⇔l = sym≋ uniti⋆-nat
cc2equiv unitir⋆⇔l = uniti⋆-nat
cc2equiv unitel⋆⇔r = sym≋ unite⋆′-nat
cc2equiv uniter⋆⇔r = unite⋆′-nat
cc2equiv unitil⋆⇔r = sym≋ uniti⋆′-nat
cc2equiv unitir⋆⇔r = uniti⋆′-nat
cc2equiv swapl⋆⇔ = sym≋ swap⋆-nat
cc2equiv swapr⋆⇔ = swap⋆-nat
cc2equiv id⇔ = id≋
cc2equiv (trans⇔ ce ce₁) = trans≋ (cc2equiv ce) (cc2equiv ce₁)
cc2equiv (ce ⊡ ce₁) = (cc2equiv ce₁) EquivEquiv.◎ (cc2equiv ce)
cc2equiv (resp⊕⇔ ce ce₁) = cc2equiv ce ⊎≋ cc2equiv ce₁
cc2equiv (resp⊗⇔ ce ce₁) = cc2equiv ce ×≋ cc2equiv ce₁
cc2equiv id⟷⊕id⟷⇔ = [id,id]≋id
cc2equiv split⊕-id⟷ = sym≋ [id,id]≋id
cc2equiv hom⊕◎⇔ = ⊎●≋●⊎
cc2equiv hom◎⊕⇔ = sym≋ ⊎●≋●⊎
cc2equiv id⟷⊗id⟷⇔ = id×id≋id
cc2equiv split⊗-id⟷ = sym≋ id×id≋id
cc2equiv hom⊗◎⇔ = ×●≋●×
cc2equiv hom◎⊗⇔ = sym≋ ×●≋●×
cc2equiv triangle⊕l = unite-assocr₊-coh
cc2equiv triangle⊕r = sym≋ unite-assocr₊-coh
cc2equiv triangle⊗l = unite-assocr⋆-coh
cc2equiv triangle⊗r = sym≋ unite-assocr⋆-coh
cc2equiv unite₊l-coh-l = unite₊l-coh
cc2equiv unite₊l-coh-r = sym≋ unite₊l-coh
cc2equiv unite⋆l-coh-l = unite⋆l-coh
cc2equiv unite⋆l-coh-r = sym≋ unite⋆l-coh
cc2equiv pentagon⊕l = assocr₊-coh
cc2equiv pentagon⊕r = sym≋ assocr₊-coh
cc2equiv pentagon⊗l = assocr⋆-coh
cc2equiv pentagon⊗r = sym≋ assocr⋆-coh
cc2equiv hexagonr⊕l = assocr₊-swap₊-coh
cc2equiv hexagonr⊕r = sym≋ assocr₊-swap₊-coh
cc2equiv hexagonl⊕l = assocl₊-swap₊-coh
cc2equiv hexagonl⊕r = sym≋ assocl₊-swap₊-coh
cc2equiv hexagonr⊗l = assocr⋆-swap⋆-coh
cc2equiv hexagonr⊗r = sym≋ assocr⋆-swap⋆-coh
cc2equiv hexagonl⊗l = assocl⋆-swap⋆-coh
cc2equiv hexagonl⊗r = sym≋ assocl⋆-swap⋆-coh
cc2equiv absorbl⇔l = distzr-nat
cc2equiv absorbl⇔r = sym≋ distzr-nat
cc2equiv absorbr⇔l = distz-nat
cc2equiv absorbr⇔r = sym≋ distz-nat
cc2equiv factorzl⇔l = factorz-nat
cc2equiv factorzl⇔r = sym≋ factorz-nat
cc2equiv factorzr⇔l = factorzr-nat
cc2equiv factorzr⇔r = sym≋ factorzr-nat
cc2equiv swap₊distl⇔l = A×[B⊎C]≃[A×C]⊎[A×B]
cc2equiv swap₊distl⇔r = sym≋ A×[B⊎C]≃[A×C]⊎[A×B]
cc2equiv dist-swap⋆⇔l = [A⊎B]×C≃[C×A]⊎[C×B]
cc2equiv dist-swap⋆⇔r = sym≋ [A⊎B]×C≃[C×A]⊎[C×B]
cc2equiv assocl₊-dist-dist⇔l = [A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D
cc2equiv assocl₊-dist-dist⇔r = sym≋ [A⊎B⊎C]×D≃[A×D⊎B×D]⊎C×D
cc2equiv assocl⋆-distl⇔l = A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D
cc2equiv assocl⋆-distl⇔r = sym≋ A×B×[C⊎D]≃[A×B]×C⊎[A×B]×D
cc2equiv absorbr0-absorbl0⇔ = 0×0≃0
cc2equiv absorbl0-absorbr0⇔ = sym≋ 0×0≃0
cc2equiv absorbr⇔distl-absorb-unite = 0×[A⊎B]≃0
cc2equiv distl-absorb-unite⇔absorbr = sym≋ 0×[A⊎B]≃0
cc2equiv unite⋆r0-absorbr1⇔ = 0×1≃0
cc2equiv absorbr1-unite⋆r-⇔ = sym≋ 0×1≃0
cc2equiv absorbl≡swap⋆◎absorbr = A×0≃0
cc2equiv swap⋆◎absorbr≡absorbl = sym≋ A×0≃0
cc2equiv absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr = 0×A×B≃0
cc2equiv [assocl⋆◎[absorbr⊗id⟷]]◎absorbr⇔absorbr = sym≋ 0×A×B≃0
cc2equiv [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr = A×0×B≃0
cc2equiv assocl⋆◎[absorbl⊗id⟷]◎absorbr⇔[id⟷⊗absorbr]◎absorbl = sym≋ A×0×B≃0
cc2equiv elim⊥-A[0⊕B]⇔l = A×[0+B]≃A×B
cc2equiv elim⊥-A[0⊕B]⇔r = sym≋ A×[0+B]≃A×B
cc2equiv elim⊥-1[A⊕B]⇔l = 1×[A⊎B]≃A⊎B
cc2equiv elim⊥-1[A⊕B]⇔r = sym≋ 1×[A⊎B]≃A⊎B
cc2equiv fully-distribute⇔l = [A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D
cc2equiv fully-distribute⇔r = sym≋ [A⊎B]×[C⊎D]≃[[A×C⊎B×C]⊎A×D]⊎B×D

--
-- These programs really are equivalent.  Here's two ways to see that:

-- 1. they give the same results as programs:

≋⇒≡ : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} (ce : c₁ ⇔ c₂) →
  eval c₁ ∼ eval c₂
≋⇒≡ {c₁ = c₁} {c₂} ce =
  trans∼ (lemma0 c₁) (
  trans∼ (_≋_.f≡ (cc2equiv ce))
         (sym∼ (lemma0 c₂)))

-- 2. in fact, you can run one forward, then the other
--    backward, and that's the identity

ping-pong : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} (ce : c₁ ⇔ c₂) →
  evalB c₂ ∘ eval c₁ ∼ id
ping-pong {c₁ = c₁} {c₂} ce =
  trans∼ (cong₂∘ (lemma1 c₂) (lemma0 c₁)) (
  trans∼ (cong∘r (proj₁ (c2equiv c₁)) (_≋_.f≡ (flip≋ (cc2equiv (2! ce))) )) (
  trans∼(sym∼ β₁)
         (_≋_.f≡ (linv≋ (c2equiv c₁)))))

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data ⊥ : Set where

T : Nat → Set
T zero    = ⊥
T (suc n) = Nat

module M (n : Nat) where

  foo : n ≡ 0 → T n → Nat
  foo refl t = 0
    module M' where
      bar : ⊥
      bar = t

  bad : ⊥
  bad = M'.bar

loop : ⊥
loop = M.bad 0

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module PigeonHole where

open import Prelude
open import Data.Nat hiding (_==_; _<_)
open import Data.Fin
open import Data.Vec as Vec
open import Logic.Base
open import Logic.Identity

open Vec.Elem

tooManyPigeons : {n : Nat}(xs : Vec (Fin (suc n)) n) -> ∃ \p -> p ∉ xs
tooManyPigeons {zero}  [] = ∃-I fzero nl
tooManyPigeons {suc n} zs = aux zs (find _==_ fzero zs)
  where

    -- We start by checking whether or not fzero is an element of the list
    aux : {n : Nat}(xs : Vec (Fin (suc (suc n))) (suc n)) ->
	  fzero ∈ xs \/ fzero ∉ xs -> ∃ \p -> p ∉ xs

    -- If it's not then we're done
    aux xs (\/-IR z∉xs) = ∃-I fzero z∉xs

    -- If it is we have to find another element
    aux xs (\/-IL z∈xs) = lem₂ ih
      where

	-- Let's remove the occurrence of fzero from the list and strip a fsuc
	-- from each of the other elements (i.e. map pred $ delete fzero xs)
	-- We can apply the induction hypothesis, giving us a p which is not in
	-- this list.
	ih : ∃ \p -> p ∉ map pred (delete fzero xs z∈xs)
	ih = tooManyPigeons (map pred $ delete _ xs z∈xs)

	-- First observe that if i ∉ map pred xs then fsuc i ∉ xs. Using this
	-- lemma we conclude that fsuc p ∉ delete fzero xs.
	lem₀ : {n m : Nat}(i : Fin (suc n))(xs : Vec (Fin (suc (suc n))) m) ->
	      i ∉ map pred xs -> fsuc i ∉ xs
	lem₀ i []	 nl	  = nl
	lem₀ i (x :: xs) (cns h t) = cns (rem₀ h) (lem₀ i xs t)
	  where
	    rem₀ : {n : Nat}{i : Fin (suc n)}{j : Fin (suc (suc n))} ->
		   i ≢ pred j -> fsuc i ≢ j
	    rem₀ i≠i refl = i≠i refl

	-- Furthermore, if i ∉ delete j xs and i ≠ j then i ∉ xs.
	lem₁ : {n m : Nat}{i : Fin (suc n)}{j : Fin n}
	       (xs : Vec (Fin (suc n)) (suc m))(p : i ∈ xs) ->
	       thin i j ∉ delete i xs p -> thin i j ∉ xs
	lem₁ (x :: xs)  hd    el = cns (thin-ij≠i _ _) el
	lem₁ {m = zero } (x :: xs) (tl ()) _
	lem₁ {m = suc _} (x :: xs) (tl p) (cns h t) = cns h (lem₁ xs p t)

	-- So we get fsuc p ∉ xs and we're done.
	lem₂ : (∃ \p -> p ∉ map pred (delete fzero xs z∈xs)) ->
	       (∃ \p -> p ∉ xs)
	lem₂ (∃-I p h) = ∃-I (fsuc p) (lem₁ xs z∈xs $ lem₀ _ _ h)

-- tooManyHoles : {n : Nat}(xs : Vec (Fin n) (suc n)) ->
-- 	       ∃ \p -> ∃ \i -> ∃ \j -> xs ! i ≡ p /\ xs ! thin i j ≡ p
-- tooManyHoles = ?

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Data.Vec.Extra where

open import Data.Product hiding (map; zip)
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Function

map-with-∈ : ∀ {a}{A : Set a}{b n}{B : Set b}
             (xs : Vec A n) → (∀ i {x} → lookup i xs ≡ x → B) → Vec B n
map-with-∈ []       f = []
map-with-∈ (x ∷ xs) f = f zero refl ∷ map-with-∈ xs (λ i x → f (suc i) refl)


text:
record R : Set₁ where
  field
    X : Set

data Δ (A : Set) : Set where
  _,_ : A → A → Δ A

foo : (A : Set) → R → Δ A → Set
foo A = λ { r (x , y) → let open R r in X }
  -- (y₁ : r) → Set !=< Set of type Set₁
  -- when checking that the expression .Foo.X has type Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2017-12-01, issue #2859 introduced by parameter-refinement

-- In Agda 2.5.2 any definition by pattern matching in a module
-- with a parameter that shadows a constructor will complain
-- about pattern variables with the same name as a constructor.

-- These are pattern variables added by the parameter-refinement
-- machinery, not user written ones.  Thus, no reason to complain here.

-- {-# OPTIONS -v scope.pat:60 #-}
-- {-# OPTIONS -v tc.lhs.shadow:30 #-}

data D : Set where
  c : D

module M (c : D) where

  data DD : Set where
    cc : DD

  should-work : DD → Set
  should-work cc = DD

  should-fail : D → D
  should-fail c = c

-- Expected error:
-- The pattern variable c has the same name as the constructor c
-- when checking the clause test c = c


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

-- | Functions for the composition of binary relations.
module Dodo.Binary.Composition where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Product using (_,_; _×_; ∃-syntax)
open import Function.Base using (flip)
open import Relation.Binary using (Rel; REL)
open import Relation.Binary using (Transitive; Symmetric)
-- Local imports
open import Dodo.Binary.Equality

-- # Definitions

infixl 10 _⨾_ ⨾:

-- | Composition of binary relations.
--
-- The composition of two relations P and Q, is mathematically denoted as `P⨾Q`. It is
-- inhabited as `(P⨾Q) x y`, iff `P x z` and `Q z y` are inhabited, for some `z`.
--
-- The notation used here is:
-- > Pxz ⨾[ z ]⨾ Qzy : (P ⨾ Q) x y
--
-- Where the corresponding types are:
-- > Pxz : P x z
-- > Qzy : Q z y
--
-- That notation is syntactic sugar for the constructor below:
-- > ⨾: z Pxz Qzy
--
--
-- # Design decision: Syntactic sugar with explicit `z`
--
-- The syntactic sugar /cannot/ be the actual constructor, as `Pxz` depends on `z`; Meaning
-- that Agda requires to know `z` before `Pxz`. Alternatively, `z` could be /implicit/
-- (as it is in the standard library). For instance:
-- > Pxz ⨾ Qzy : (P ⨾ Q) x y
--
-- The disadvantage of that approach is that `z` may not always be inferred from `Pxz` and `Qzy`.
-- After all, `Pxz` and `Qzy` may be beta-reduced, for which different types of `P`, `Q`, `x`, `y`,
-- and `z` hold; Which introduces ambiguity during type checking. This, in turn, requires making
-- the implicit argument /explicit/ in practice; namely:
-- > _⨾_  {z} Pxz Qzy
--
-- Which is syntactically even less desirable. Hence, in the definition below, `z` is represented
-- explicitly.
data _⨾_ {a b c ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {C : Set c} (L : REL A B ℓ₁) (R : REL B C ℓ₂)
    (i : A) (j : C) : Set (a ⊔ b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
  ⨾: : (k : B) → L i k → R k j → (L ⨾ R) i j

syntax ⨾: k Pik Qkj = Pik ⨾[ k ]⨾ Qkj

-- # Properties

module _ {a b c d ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
    {P : REL A B ℓ₁} {Q : REL B C ℓ₂} {R : REL C D ℓ₃} where

  -- | Composition of binary relations is associative.
  ⨾-assoc : (P ⨾ Q) ⨾ R ⇔₂ P ⨾ (Q ⨾ R)
  ⨾-assoc = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : (P ⨾ Q) ⨾ R ⊆₂' P ⨾ (Q ⨾ R)
    ⊆-proof _ _ ((Pxb ⨾[ b ]⨾ Qbc) ⨾[ c ]⨾ Rcy) = Pxb ⨾[ b ]⨾ (Qbc ⨾[ c ]⨾ Rcy)
    ⊇-proof : P ⨾ (Q ⨾ R) ⊆₂' (P ⨾ Q) ⨾ R
    ⊇-proof _ _ (Pxb ⨾[ b ]⨾ (Qbc ⨾[ c ]⨾ Rcy)) = (Pxb ⨾[ b ]⨾ Qbc) ⨾[ c ]⨾ Rcy

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  -- | The composition of a transitive relation with itself is a subset of itself.
  ⨾-trans-⊆₂ : Transitive R → (R ⨾ R) ⊆₂ R
  ⨾-trans-⊆₂ transR = ⊆: lemma
    where
    lemma : (R ⨾ R) ⊆₂' R
    lemma _ _ (Rxz ⨾[ z ]⨾ Rzy) = transR Rxz Rzy

-- # Operations

module _ {a b c ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL B C ℓ₃} where

  ⨾-substˡ-⊆₂ : P ⊆₂ Q → (P ⨾ R) ⊆₂ (Q ⨾ R)
  ⨾-substˡ-⊆₂ (⊆: P⊆Q) = ⊆: ⊆-proof
    where
    ⊆-proof : (P ⨾ R) ⊆₂' (Q ⨾ R)
    ⊆-proof x y (Pxz ⨾[ z ]⨾ Rzy) = P⊆Q x z Pxz ⨾[ z ]⨾ Rzy

module _ {a b c ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL B C ℓ₃} where

  ⨾-substˡ : P ⇔₂ Q → (P ⨾ R) ⇔₂ (Q ⨾ R)
  ⨾-substˡ = ⇔₂-compose ⨾-substˡ-⊆₂ ⨾-substˡ-⊆₂

module _ {a b c ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : REL B C ℓ₁} {Q : REL B C ℓ₂} {R : REL A B ℓ₃} where

  ⨾-substʳ-⊆₂ : P ⊆₂ Q → (R ⨾ P) ⊆₂ (R ⨾ Q)
  ⨾-substʳ-⊆₂ (⊆: P⊆Q) = ⊆: ⊆-proof
    where
    ⊆-proof : (R ⨾ P) ⊆₂' (R ⨾ Q)
    ⊆-proof x y (Rxz ⨾[ z ]⨾ Pzy) = Rxz ⨾[ z ]⨾ P⊆Q z y Pzy

module _ {a b c ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : REL B C ℓ₁} {Q : REL B C ℓ₂} {R : REL A B ℓ₃} where

  ⨾-substʳ : P ⇔₂ Q → (R ⨾ P) ⇔₂ (R ⨾ Q)
  ⨾-substʳ = ⇔₂-compose ⨾-substʳ-⊆₂ ⨾-substʳ-⊆₂

module _ {a b c ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {C : Set c}
    {P : REL A B ℓ₁} {Q : REL B C ℓ₂} where

  -- | Expanded definition of flipping the composition of two relations.
  ⨾-flip : flip (P ⨾ Q) ⇔₂ flip Q ⨾ flip P
  ⨾-flip = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : flip (P ⨾ Q) ⊆₂' flip Q ⨾ flip P
    ⊆-proof x y (Pyz ⨾[ z ]⨾ Qzx) = (Qzx ⨾[ z ]⨾ Pyz)
    ⊇-proof : flip Q ⨾ flip P ⊆₂' flip (P ⨾ Q)
    ⊇-proof x y (Qzy ⨾[ z ]⨾ Pxz) = (Pxz ⨾[ z ]⨾ Qzy)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

postulate
  A : Set
  u₁ u₂ : ⊤

mutual
  X : (⊤ → ⊤) → A
  X = _

  test : X (λ x → u₁) ≡ X (λ x → u₂)
  test = refl


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

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

-- RWS monad implementation, and functionality for proving properties about
-- programs written using this RWS monad.
-- It includes constructors for branching code, to aid in the verification.

module Haskell.Modules.RWS where

open import Haskell.Prelude
------------------------------------------------------------------------------
open import Data.Product using (_×_; _,_)

-- (free) RWS : the AST of computations with state `St` reading from an environment
-- `Ev` and producing a list of outputs of type `Wr`
data RWS (Ev Wr St : Set) : Set → Set₁ where
  -- Primitive combinators
  RWS-return : ∀ {A}   → A                                       → RWS Ev Wr St A
  RWS-bind   : ∀ {A B} → RWS Ev Wr St A → (A → RWS Ev Wr St B)   → RWS Ev Wr St B
  RWS-gets   : ∀ {A} → (St → A)                                  → RWS Ev Wr St A
  RWS-put    : St                                                → RWS Ev Wr St Unit
  RWS-ask    :                                                     RWS Ev Wr St Ev
  RWS-tell   : List Wr                                           → RWS Ev Wr St Unit
  -- Branching combinators (used for creating more convenient contracts)
  RWS-if     : ∀ {A} → Guards (RWS Ev Wr St A)                   → RWS Ev Wr St A
  RWS-either : ∀ {A B C}
             → (B → RWS Ev Wr St A) → (C → RWS Ev Wr St A)
             → Either B C                                        → RWS Ev Wr St A
  RWS-ebind  : ∀ {A B C}
             → RWS Ev Wr St (Either C A)
             → (A → RWS Ev Wr St (Either C B))                   → RWS Ev Wr St (Either C B)
  RWS-maybe  : ∀ {A B}
             → (RWS Ev Wr St A) → (B → RWS Ev Wr St A) → Maybe B → RWS Ev Wr St A

private
  variable
    Ev Wr St : Set
    A B C    : Set

-- From this instance declaration, we get _<$>_, pure, and _<*>_ also.
instance
  RWS-Monad : Monad (RWS Ev Wr St)
  Monad.return RWS-Monad = RWS-return
  Monad._>>=_  RWS-Monad = RWS-bind

gets : (St → A) → RWS Ev Wr St A
gets = RWS-gets

get : RWS Ev Wr St St
get = gets id

put : St → RWS Ev Wr St Unit
put = RWS-put

modify : (St → St) → RWS Ev Wr St Unit
modify f = do
  st ← get
  put (f st)

ask : RWS Ev Wr St Ev
ask = RWS-ask

tell : List Wr → RWS Ev Wr St Unit
tell = RWS-tell

void : RWS Ev Wr St A → RWS Ev Wr St Unit
void m = do
  _ ← m
  pure unit

-- To execute an RWS program, you provide an environment and prestate.
-- This produces a result value, poststate, and list of outputs.
RWS-run : RWS Ev Wr St A → Ev → St → A × St × List Wr
RWS-run (RWS-return x)               ev st = x , st , []
RWS-run (RWS-bind m f)               ev st
   with RWS-run m ev st
...| x₁ , st₁ , outs₁
   with RWS-run (f x₁) ev st₁
...| x₂ , st₂ , outs₂                      = x₂ , st₂ , outs₁ ++ outs₂
RWS-run (RWS-gets f)                 ev st = f st , st , []
RWS-run (RWS-put st)                 ev _  = unit , st , []
RWS-run RWS-ask                      ev st = ev , st , []
RWS-run (RWS-tell outs)              ev st = unit , st , outs
RWS-run (RWS-if (clause (b ≔ c) gs)) ev st =
  if toBool b then RWS-run c ev st else RWS-run (RWS-if gs) ev st
RWS-run (RWS-if (otherwise≔ c))      ev st = RWS-run c ev st
RWS-run (RWS-either f₁ f₂ (Left x) ) ev st = RWS-run (f₁ x) ev st
RWS-run (RWS-either f₁ f₂ (Right y)) ev st = RWS-run (f₂ y) ev st
RWS-run (RWS-ebind m f)              ev st
   with RWS-run m ev st
...| Left  c , st₁ , outs₁ = Left c , st₁ , outs₁
...| Right a , st₁ , outs₁
   with RWS-run (f a) ev st₁
...|       r , st₂ , outs₂                 = r , st₂ , outs₁ ++ outs₂
RWS-run (RWS-maybe f₁ f₂ nothing )   ev st = RWS-run f₁ ev st
RWS-run (RWS-maybe f₁ f₂ (just x))   ev st = RWS-run (f₂ x) ev st

-- Accessors for the result, poststate, and outputs.
RWS-result : RWS Ev Wr St A → Ev → St → A
RWS-result m ev st =      fst (RWS-run m ev st)

RWS-post   : RWS Ev Wr St A → Ev → St → St
RWS-post   m ev st = fst (snd (RWS-run m ev st))

RWS-outs   : RWS Ev Wr St A → Ev → St → List Wr
RWS-outs   m ev st = snd (snd (RWS-run m ev st))


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

open import LogicalFormulae
open import Functions.Definition

module Orders.Total.Definition {a : _} (carrier : Set a) where

open import Orders.Partial.Definition carrier

record TotalOrder {b : _} : Set (a ⊔ lsuc b) where
  field
    order : PartialOrder {b}
  _<_ : Rel carrier
  _<_ = PartialOrder._<_ order
  _≤_ : Rel carrier
  _≤_ a b = (a < b) || (a ≡ b)
  field
    totality : (a b : carrier) → ((a < b) || (b < a)) || (a ≡ b)

  min : carrier → carrier → carrier
  min a b with totality a b
  min a b | inl (inl a<b) = a
  min a b | inl (inr b<a) = b
  min a b | inr a=b = a
  max : carrier → carrier → carrier
  max a b with totality a b
  max a b | inl (inl a<b) = b
  max a b | inl (inr b<a) = a
  max a b | inr a=b = b

  irreflexive = PartialOrder.irreflexive order
  <Transitive = PartialOrder.<Transitive order
  <WellDefined = PartialOrder.<WellDefined order


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

open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Generics.HasDesc
open import Generics.All

module Generics.Constructions.Mu
  {P I ℓ} (A : Indexed P I ℓ) (H : HasDesc A)
  (open HasDesc H)
  {p} where

private
  variable
    V : ExTele P
    i : ⟦ I ⟧tel p
    v : ⟦ V ⟧tel p

open import Generics.Mu public

toData : (x : ⟦ D ⟧Data A′ (p , i)) → AllDataω Acc D x → μ D (p , i)

to-wf : (x : A′ (p , i)) → Acc x → μ D (p , i)
to-wf x (acc a) = toData (split x) a

toData (k , x) a = ⟨ k , toCon (lookupCon D k) x a ⟩
  where
    toIndArg : (C : ConDesc P V I)
               (x : ⟦ C ⟧IndArg A′ (p , v))
             → AllIndArgω Acc C x
             → ⟦ C ⟧IndArgω (μ D) (p , v)
    toIndArg (var _) x a = to-wf x a
    toIndArg (π ai _ C) x a s = toIndArg C (app< ai > x s) (a s)
    toIndArg (A ⊗ B) (xa , xb) (aa , ab)
      = toIndArg A xa aa , toIndArg B xb ab

    toCon : (C : ConDesc P V I)
            (x : ⟦ C ⟧Con A′ (p , v , i))
          → AllConω Acc C x
          → ⟦ C ⟧Conω (μ D) (p , v , i)
    toCon (var _) refl _ = liftω refl
    toCon (π _ _ C) (s , x) a = s , toCon C x a
    toCon (A ⊗ B) (xa , xb) (aa , ab)
      = toIndArg A xa aa , toCon B xb ab

to : A′ (p , i) → μ D (p , i)
to x = to-wf x (wf x)

from : μ D (p , i) → A′ (p , i)

fromIndArg : (C : ConDesc P V I)
           → ⟦ C ⟧IndArgω (μ D) (p , v)
           → ⟦ C ⟧IndArg A′ (p , v)
fromIndArg (var _) x = from x
fromIndArg (π ai S C) x = fun< ai > λ s → fromIndArg C (x s)
fromIndArg (A ⊗ B) (xa , xb) = fromIndArg A xa , fromIndArg B xb

fromCon : (C : ConDesc P V I)
        → ⟦ C ⟧Conω (μ D) (p , v , i)
        → ⟦ C ⟧Con A′ (p , v , i)
fromCon (var _) (liftω refl) = refl
fromCon (π _ S C) (s , x) = s , fromCon C x
fromCon (A ⊗ B) (xa , xb) = fromIndArg A xa , fromCon B xb

from ⟨ k , x ⟩ = constr (k , fromCon (lookupCon D k) x)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------------
-- A simple network using the Agda standard library
------------------------------------------------------------------------------

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

-- From (Sander, 1992, pp. 68-69).

module FOT.FOTC.Program.ABP.SimpleNetwork-SL where

open import Codata.Musical.Stream
open import Data.Bool.Base

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

postulate
  f₁ : {A : Set} → Stream A → Stream A → Stream A
  f₂ : {A : Set} → Stream A → Stream A

{-# TERMINATING #-}
trans : {A : Set} → Stream A → Stream A
trans {A} is = os
  where
  ys os : Stream A
  ys = f₁ os is
  os = f₂ ys

Ty : Set → Set
Ty A = (Stream A → Stream A → Stream A) → (Stream A → Stream A) →
       Stream A → Stream A

{-# TERMINATING #-}
trans' hys : {A : Set} → Ty A
trans' f₁ f₂ is = f₂ (hys f₁ f₂ is)
hys   f₁ f₂ is = f₁ (trans' f₁ f₂ is) is

------------------------------------------------------------------------------
-- References
--
-- Sander, Herbert P. (1992). A Logic of Functional Programs with an
-- Application to Concurrency. PhD thesis. Department of Computer
-- Sciences: Chalmers University of Technology and University of
-- Gothenburg.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
  postulate
    F  : Set₂ → Set₃
    #_ : Set₁ → Set₂
    !_ : Set₀ → Set₁

  infix 1 F
  infix 2 #_
  infix 3 !_

  syntax F x = ! x

  ok₁ : Set₁ → Set₃
  ok₁ X = ! # X

  ok₂ : Set₀ → Set₂
  ok₂ X = # ! X


text:
{- Category of sets -}
module CategoryTheory.Instances.Sets where

open import CategoryTheory.Categories
open import CategoryTheory.BCCCs

import Function as F using (_∘_)
open import Data.Unit using () renaming (⊤ to top) public
open import Data.Product public
open import Data.Empty using (⊥-elim) renaming (⊥ to bot) public
open import Data.Sum

-- Category of sets.
𝕊et : Category lzero
𝕊et = record
    { obj      = Set
    ; _~>_     = λ a b   -> (a -> b)
    ; id       = λ a     -> a
    ; _∘_      = λ g f a -> g (f a)
    ; _≈_      = λ f g   -> ∀ {a} -> f a ≡ g a
    ; id-left  = refl
    ; id-right = refl
    ; ∘-assoc  = refl
    ; ≈-equiv  = record { refl = refl
                        ; sym = λ p → sym p
                        ; trans = λ p q → trans p q }
    ; ≈-cong   = ≈-cong-𝕊
    }
    where
    ≈-cong-𝕊 : ∀{A B C : Set} {f f′ : A -> B} {g g′ : B -> C}
            -> (∀ {a} -> f a ≡ f′ a)
            -> (∀ {b} -> g b ≡ g′ b)
            -> (∀ {a} -> g (f a) ≡ g′ (f′ a))
    ≈-cong-𝕊 {f′ = f′} fe ge {a′} rewrite fe {a′} | ge {f′ a′} = refl

-- Bicartesian closed structure
𝕊et-BCCC : BicartesianClosed 𝕊et
𝕊et-BCCC = record
    { cart = record
        { term = record
            { ⊤ = top
            ; ! = λ {A} _ → top.tt
            ; !-unique = λ m → refl
            }
        ; prod = λ A B → record
            { A⊗B = A × B
            ; π₁ = proj₁
            ; π₂ = proj₂
            ; ⟨_,_⟩ = <_,_>
            ; π₁-comm = refl
            ; π₂-comm = refl
            ; ⊗-unique = λ pr1 pr2 → unique-cart (ext λ x → pr1 {x}) (ext λ x → pr2 {x})
            }
        }
    ; cocart = record
        { init = record
            { ⊥ = bot
            ; ¡ = ⊥-elim
            ; ¡-unique = λ {A} m → λ {}
            }
        ; sum = λ A B → record
            { A⊕B = A ⊎ B
            ; ι₁ = inj₁
            ; ι₂ = inj₂
            ; [_⁏_] = [_,_]
            ; ι₁-comm = λ {S} {i₁} {i₂} {a} → refl
            ; ι₂-comm = λ {S} {i₁} {i₂} {a} → refl
            ; ⊕-unique = λ {S} {i₁} {i₂} {m} pr1 pr2
                      -> unique-cocart {m = m} (ext λ x → pr1 {x}) (ext λ x → pr2 {x})
            }
        }
    ; closed = record
        { exp = λ A B → record
            { A⇒B = A -> B
            ; eval = λ fa → proj₁ fa (proj₂ fa)
            ; Λ = λ f a b → f (a , b)
            ; Λ-comm = refl
            ; Λ-unique = λ pr → λ {a} ->  unique-closed (ext λ x → pr {x})
            ; Λ-cong = λ pr → ext (λ _ → pr)
            }
        }
    }
    where
    unique-cart : ∀{A B P : Set}{a}
              -> {p₁ : P -> A} {p₂ : P -> B} {m : P -> A × B}
              -> proj₁ F.∘ m ≡ p₁ -> proj₂ F.∘ m ≡ p₂
              -> < p₁ , p₂ > a ≡ m a
    unique-cart refl refl = refl
    unique-cocart : ∀{A B S : Set}{a}
              -> {i₁ : A -> S} {i₂ : B -> S} {m : A ⊎ B -> S}
              -> m F.∘ inj₁ ≡ i₁ -> m F.∘ inj₂ ≡ i₂
              -> [ i₁ , i₂ ] a ≡ m a
    unique-cocart {a = inj₁ x} refl refl = refl
    unique-cocart {a = inj₂ y} refl refl = refl
    open Category 𝕊et
    unique-closed : ∀{A B E : Set}{a}
              -> {e : E × A -> B} {m : E -> (A -> B)}
              -> (λ fa → proj₁ fa (proj₂ fa)) ∘ < m ∘ proj₁ , proj₂ > ≡ e
              -> (λ b → e (a , b)) ≡ m a
    unique-closed refl = refl

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:
------------------------------------------------------------------------------
-- First-order Peano arithmetic
------------------------------------------------------------------------------

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

module PA.Axiomatic.Standard.README where

-- Formalization of first-order Peano arithmetic using Agda postulates
-- for the non-logical constants and the Peano's axioms, and using
-- axioms based on the propositional equality (see, for example,
-- (Machover 1996, p. 263), (Hájek and Pudlák 1998, p. 28).

------------------------------------------------------------------------------
-- The axioms
open import PA.Axiomatic.Standard.Base

-- Some properties
open import PA.Axiomatic.Standard.PropertiesATP
open import PA.Axiomatic.Standard.PropertiesI

------------------------------------------------------------------------------
-- References
--
-- Machover, Moshé (1996). Set theory, Logic and their
-- Limitations. Cambridge University Press.

-- Hájek, Petr and Pudlák, Pavel (1998). Metamathematics of
-- First-Order Arithmetic. 2nd printing. Springer.


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

module Parameters where

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

-- Error: The type of the constructor does not fit in the sort of the
-- datatype, since Set₁ is not less or equal than Set when checking
-- the constructor [] in the declaration of List₁
--
-- data List₁ : Set → Set where
--   []  : {A : Set} → List₁ A
--   _∷_ : {A : Set} → A → List₁ A → List₁ A

data List₁ : Set → Set₁ where
  []  : {A : Set} → List₁ A
  _∷_ : {A : Set} → A → List₁ A → List₁ A


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.String
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

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

macro
  give : Wrap Term → Term → TC ⊤
  give [ t ] hole = unify hole t

pattern vArg x = arg (arg-info visible relevant) x
pattern hArg x = arg (arg-info hidden  relevant) x

-- Naming the variable "_" doesn't affect the deBruijn indices for lambda and pi

`id : Term
`id = lam visible (abs "_" (var 0 []))

`IdType : Term
`IdType = pi (hArg (agda-sort (lit 0))) (abs "_" (pi (vArg (var 0 [])) (abs "_" (var 1 []))))

id : give [ `IdType ]
id = give [ `id ]

id-ok : (λ {A : Set} (x : A) → x) ≡ id
id-ok = refl

-- Underscores should behave the same for clauses as for lambda and pi

idClause : Clause
idClause = clause
             (("_" , vArg unknown) ∷ ("_" , hArg unknown) ∷ [])
             (hArg (var 1) ∷ vArg (var 0) ∷ [])
             (var 0 [])

infixr 4 _>>=_
_>>=_ = bindTC

unquoteDecl id₂ =
  declareDef (vArg id₂) `IdType >>= λ _ →
  defineFun id₂ (idClause ∷ [])

id₂-ok : (λ {A : Set} (x : A) → x) ≡ id₂
id₂-ok = refl

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.CommutativeMonoid {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where

open import Algebra.Operations.CommutativeMonoid M
open import Algebra.Solver.CommutativeMonoid M
open import Relation.Binary as B using (_Preserves_⟶_)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Data.Product
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc)
open import Data.List as List using ([]; _∷_)
import Data.Fin.Properties as FP
open import Data.Fin.Permutation as Perm using (Permutation; Permutation′; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
open import Data.Fin.Permutation.Components as PermC
open import Data.Table as Table
open import Data.Table.Relation.Binary.Equality as TE using (_≗_)
open import Data.Unit using (tt)
import Data.Table.Properties as TP
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Decidable using (⌊_⌋)

open CommutativeMonoid M
  renaming
  ( ε         to 0#
  ; _∙_       to _+_
  ; ∙-cong    to +-cong
  ; ∙-congˡ   to +-congˡ
  ; ∙-congʳ   to +-congʳ
  ; identityˡ to +-identityˡ
  ; identityʳ to +-identityʳ
  ; assoc     to +-assoc
  ; comm      to +-comm
  )
open import Algebra.FunctionProperties _≈_
open import Relation.Binary.Reasoning.Setoid setoid

module _ {n} where
  open B.Setoid (TE.setoid setoid n) public
    using ()
    renaming (_≈_ to _≋_)

-- When summing over a function from a finite set, we can pull out any value and move it to the front.

sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ lookup t i + sumₜ (remove i t)
sumₜ-remove {_}     {zero}   t = refl
sumₜ-remove {zero}  {suc ()} t
sumₜ-remove {suc n} {suc i}  t′ =
  begin
    t₀ + ∑t           ≈⟨ +-congˡ (sumₜ-remove t) ⟩
    t₀ + (tᵢ + ∑t′)   ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩
    tᵢ + (t₀ + ∑t′)   ∎
  where
  t = tail t′
  t₀ = head t′
  tᵢ = lookup t i
  ∑t = sumₜ t
  ∑t′ = sumₜ (remove i t)

-- '_≈_' is a congruence over 'sumTable n'.

sumₜ-cong-≈ : ∀ {n} → sumₜ {n} Preserves _≋_ ⟶ _≈_
sumₜ-cong-≈ {zero}  p = refl
sumₜ-cong-≈ {suc n} p = +-cong (p _) (sumₜ-cong-≈ (p ∘ suc))

-- '_≡_' is a congruence over 'sum n'.

sumₜ-cong-≡ : ∀ {n} → sumₜ {n} Preserves _≗_ ⟶ _≡_
sumₜ-cong-≡ {zero}  p = P.refl
sumₜ-cong-≡ {suc n} p = P.cong₂ _+_ (p _) (sumₜ-cong-≡ (p ∘ suc))

-- If addition is idempotent on a particular value 'x', then summing over a
-- nonzero number of copies of 'x' gives back 'x'.

sumₜ-idem-replicate : ∀ n {x} → _+_ IdempotentOn x → sumₜ (replicate {n = suc n} x) ≈ x
sumₜ-idem-replicate zero        idem = +-identityʳ _
sumₜ-idem-replicate (suc n) {x} idem = begin
  x + (x + sumₜ (replicate {n = n} x))  ≈⟨ sym (+-assoc _ _ _) ⟩
  (x + x) + sumₜ (replicate {n = n} x)  ≈⟨ +-congʳ idem ⟩
  x + sumₜ (replicate {n = n} x)        ≈⟨ sumₜ-idem-replicate n idem ⟩
  x                                 ∎

-- The sum over the constantly zero function is zero.

sumₜ-zero : ∀ n → sumₜ (replicate {n = n} 0#) ≈ 0#
sumₜ-zero n = begin
  sumₜ (replicate {n = n} 0#)      ≈⟨ sym (+-identityˡ _) ⟩
  0# + sumₜ (replicate {n = n} 0#) ≈⟨ sumₜ-idem-replicate n (+-identityˡ 0#) ⟩
  0#                               ∎

-- The '∑' operator distributes over addition.

∑-distrib-+ : ∀ n (f g : Fin n → Carrier) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
∑-distrib-+ zero    f g = sym (+-identityˡ _)
∑-distrib-+ (suc n) f g = begin
  f₀ + g₀ + ∑fg          ≈⟨ +-assoc _ _ _ ⟩
  f₀ + (g₀ + ∑fg)        ≈⟨ +-congˡ (+-congˡ (∑-distrib-+ n _ _)) ⟩
  f₀ + (g₀ + (∑f + ∑g))  ≈⟨ solve 4 (λ a b c d → a ⊕ (c ⊕ (b ⊕ d)) ⊜ (a ⊕ b) ⊕ (c ⊕ d)) refl f₀ ∑f g₀ ∑g ⟩
  (f₀ + ∑f) + (g₀ + ∑g)  ∎
  where
  f₀ = f zero
  g₀ = g zero
  ∑f  = ∑[ i < n ] f (suc i)
  ∑g  = ∑[ i < n ] g (suc i)
  ∑fg = ∑[ i < n ] (f (suc i) + g (suc i))

-- The '∑' operator commutes with itself.

∑-comm : ∀ n m (f : Fin n → Fin m → Carrier) → ∑[ i < n ] ∑[ j < m ] f i j ≈ ∑[ j < m ] ∑[ i < n ] f i j
∑-comm zero    m f = sym (sumₜ-zero m)
∑-comm (suc n) m f = begin
  ∑[ j < m ] f zero j + ∑[ i < n ] ∑[ j < m ] f (suc i) j  ≈⟨ +-congˡ (∑-comm n m _) ⟩
  ∑[ j < m ] f zero j + ∑[ j < m ] ∑[ i < n ] f (suc i) j  ≈⟨ sym (∑-distrib-+ m _ _) ⟩
  ∑[ j < m ] (f zero j + ∑[ i < n ] f (suc i) j)           ∎

-- Any permutation of a table has the same sum as the original.

sumₜ-permute : ∀ {m n} t (π : Permutation m n) → sumₜ t ≈ sumₜ (permute π t)
sumₜ-permute {zero}  {zero}  t π = refl
sumₜ-permute {zero}  {suc n} t π = contradiction π (Perm.refute λ())
sumₜ-permute {suc m} {zero}  t π = contradiction π (Perm.refute λ())
sumₜ-permute {suc m} {suc n} t π = begin
  sumₜ t                                                                            ≡⟨⟩
  lookup t 0i           + sumₜ (remove 0i t)                                        ≡⟨ P.cong₂ _+_ (P.cong (lookup t) (P.sym (Perm.inverseʳ π))) P.refl ⟩
  lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (remove 0i t)                                        ≈⟨ +-congˡ (sumₜ-permute (remove 0i t) (Perm.remove (π ⟨$⟩ˡ 0i) π)) ⟩
  lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (permute (Perm.remove (π ⟨$⟩ˡ 0i) π) (remove 0i t))  ≡⟨ P.cong₂ _+_ P.refl (sumₜ-cong-≡ (P.sym ∘ TP.remove-permute π 0i t)) ⟩
  lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (remove (π ⟨$⟩ˡ 0i) πt)                              ≈⟨ sym (sumₜ-remove (permute π t)) ⟩
  sumₜ πt                                                                           ∎
  where
  0i = zero
  πt = permute π t

∑-permute : ∀ {m n} f (π : Permutation m n) → ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i)
∑-permute = sumₜ-permute ∘ tabulate

-- If the function takes the same value at 'i' and 'j', then transposing 'i' and
-- 'j' then selecting 'j' is the same as selecting 'i'.

select-transpose : ∀ {n} t (i j : Fin n) → lookup t i ≈ lookup t j → ∀ k → (lookup (select 0# j t) ∘ PermC.transpose i j) k ≈ lookup (select 0# i t) k
select-transpose _ i j e k with k FP.≟ i
... | yes p rewrite P.≡-≟-identity FP._≟_ {j} P.refl = sym e
... | no ¬p with k FP.≟ j
...   | no ¬q rewrite proj₂ (P.≢-≟-identity FP._≟_ ¬q) = refl
...   | yes q rewrite proj₂ (P.≢-≟-identity FP._≟_
                               (¬p ∘ P.trans q ∘ P.sym)) = refl

-- Summing over a pulse gives you the single value picked out by the pulse.

sumₜ-select : ∀ {n i} (t : Table Carrier n) → sumₜ (select 0# i t) ≈ lookup t i
sumₜ-select {zero}  {()}
sumₜ-select {suc n} {i} t = begin
  sumₜ (select 0# i t)                                        ≈⟨ sumₜ-remove {i = i} (select 0# i t) ⟩
  lookup (select 0# i t) i + sumₜ (remove i (select 0# i t))  ≡⟨ P.cong₂ _+_ (TP.select-lookup t) (sumₜ-cong-≡ (TP.select-remove i t)) ⟩
  lookup t i + sumₜ (replicate {n = n} 0#)                    ≈⟨ +-congˡ (sumₜ-zero n) ⟩
  lookup t i + 0#                                             ≈⟨ +-identityʳ _ ⟩
  lookup t i                                                  ∎

-- Converting to a table then summing is the same as summing the original list

sumₜ-fromList : ∀ xs → sumₜ (fromList xs) ≡ sumₗ xs
sumₜ-fromList []       = P.refl
sumₜ-fromList (x ∷ xs) = P.cong (_ +_) (sumₜ-fromList xs)

-- Converting to a list then summing is the same as summing the original table

sumₜ-toList : ∀ {n} (t : Table Carrier n) → sumₜ t ≡ sumₗ (toList t)
sumₜ-toList {zero}  _ = P.refl
sumₜ-toList {suc n} _ = P.cong (_ +_) (sumₜ-toList {n} _)


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

module Cauchy where

-- Definitions for permutations in the Cauchy representation

open import Relation.Binary.PropositionalEquality using (subst)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+; +-*-suc)

open import Data.Bool using (Bool; false; true)
open import Data.Nat using (ℕ; suc; _+_; _*_)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ;
         raise; inject+; inject₁; inject≤; _≻toℕ_)
open import Data.Vec
  using (Vec; tabulate; []; _∷_; lookup; allFin)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Function using (id)

open import Proofs using (i*n+k≤m*n; trans≤; refl′; splitVOp+)

------------------------------------------------------------------------------
-- Semantic representations of permutations

-- One possibility of course is to represent them as functions but
-- this is a poor representation and eventually requires function
-- extensionality.

-- Representation III
-- This is the 2 line Cauchy representation. The first line is in
-- canonical order and implicit in the indices of the vector

Cauchy : ℕ → Set
Cauchy n = Vec (Fin n) n

------------------------------------------------------------------------------
-- Elementary permutations in the Cauchy representation

emptycauchy : Cauchy 0
emptycauchy = []

idcauchy : (n : ℕ) → Cauchy n
idcauchy = allFin

-- Sequential composition

scompcauchy : ∀ {n} → Cauchy n → Cauchy n → Cauchy n
scompcauchy {n} perm₁ perm₂ =
  tabulate (λ i → lookup (lookup i perm₁) perm₂)

-- swap the first m elements with the last n elements
-- [ v₀ , v₁   , v₂   , ... , vm-1 ,     vm , vm₊₁ , ... , vm+n-1 ]
-- ==>
-- [ vm , vm₊₁ , ... , vm+n-1 ,     v₀ , v₁   , v₂   , ... , vm-1 ]

id+ : ∀ {m n} → Fin (n + m) → Fin (m + n)
id+ {m} {n} x = subst Fin (+-comm n m) x

swap+cauchy : (m n : ℕ) → Cauchy (m + n)
swap+cauchy m n = splitVOp+ {m} {n} {f = id+ {m} {n}}

-- Parallel additive composition
-- append both permutations but adjust the indices in the second
-- permutation by the size of the first type so that it acts on the
-- second part of the vector

pcompcauchy : ∀ {m n} → Cauchy m → Cauchy n → Cauchy (m + n)
pcompcauchy {m} {n} α β = mapV (inject+ n) α ++V mapV (raise m) β

-- Tensor multiplicative composition
-- Transpositions in α correspond to swapping entire rows
-- Transpositions in β correspond to swapping entire columns

tcompcauchy : ∀ {m n} → Cauchy m → Cauchy n → Cauchy (m * n)
tcompcauchy {m} {n} α β =
  concatV
    (mapV
      (λ b →
         mapV (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d)) β)
      α)

-- swap⋆
--
-- This is essentially the classical problem of in-place matrix transpose:
-- "http://en.wikipedia.org/wiki/In-place_matrix_transposition"
-- Given m and n, the desired permutation in Cauchy representation is:
-- P(i) = m*n-1 if i=m*n-1
--      = m*i mod m*n-1 otherwise

transposeIndex : (m n : ℕ) →
       (b : Fin m) → (d : Fin n) → Fin (m * n)
transposeIndex m n b d =
  inject≤
    (fromℕ (toℕ d * m + toℕ b))
    (trans≤ (i*n+k≤m*n d b) (refl′ (*-comm n m)))

swap⋆cauchy : (m n : ℕ) → Cauchy (m * n)
swap⋆cauchy m n =
  concatV (mapV
            (λ b → mapV (λ d → transposeIndex m n b d) (allFin n))
            (allFin m))

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


text:
module Issue329c where

private
  infixl 0 D Undeclared
  data D : Set where

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Codata.Stream where

open import Prelude
open import Data.List using (List; _∷_; [])
open import Data.List.Kleene
import Data.List.Kleene.Membership as Kleene
open import Data.Fin

infixr 5 _◃_
record Stream (A : Type a) : Type a where
  constructor _◃_
  coinductive
  field
    head  : A
    tail  : Stream A
open Stream public

Stream′ : Type a → Type a
Stream′ A = ℕ → A

_!_ : Stream A → Stream′ A
xs ! zero  = xs .head
xs ! suc n = xs .tail ! n

tabulate : Stream′ A → Stream A
tabulate xs .head = xs zero
tabulate xs .tail = tabulate (xs ∘ suc)

linv : (xs : Stream A) → tabulate (xs !_) ≡ xs
linv xs i .head = xs .head
linv xs i .tail = linv (xs .tail) i

rinv : (xs : Stream′ A) → (tabulate xs !_) ≡ xs
rinv xs i zero    = xs zero
rinv xs i (suc n) = rinv (xs ∘ suc) i n

stream : Stream A ⇔ Stream′ A
stream .fun = _!_
stream .inv = tabulate
stream .rightInv = rinv
stream .leftInv = linv

-- infixr 5 _∈_
-- _∈_ : A → Stream A → Type _
-- x ∈ xs = fiber xs x

-- toList : ℕ → Stream A → List A
-- toList zero xs = []
-- toList (suc n) xs = xs zero ∷ toList n (xs ∘ suc)

-- mutual
--   concat⋆ : A ⋆ → Stream (A ⁺) → Stream A
--   concat⋆ []    xs = concat⁺ (xs zero) (xs ∘ suc)
--   concat⋆ (∹ x) xs = concat⁺ x xs

--   concat⁺ : A ⁺ → Stream (A ⁺) → Stream A
--   concat⁺ x xs zero    = x .head
--   concat⁺ x xs (suc n) = concat⋆ (x .tail) xs n

-- concat : Stream (A ⁺) → Stream A
-- concat xs = concat⁺ (xs zero) (xs ∘ suc)

-- infixr 5 _∈²_
-- _∈²_ : A → Stream (A ⁺) → Type _
-- x ∈² xs = ∃ n x Kleene.∈⁺ xs n

-- mutual
--   ◇++⋆ : ∀ (x : A) y ys → x Kleene.∈⋆ y → x ∈ concat⋆ y ys
--   ◇++⋆ x (∹ y) ys x∈y = ◇++⁺ x y ys x∈y

--   ◇++⁺ : ∀ (x : A) y ys → x Kleene.∈⁺ y → x ∈ concat⁺ y ys
--   ◇++⁺ x y ys (f0 , x∈y) = zero , x∈y
--   ◇++⁺ x y ys (fs n , x∈y) = let m , p = ◇++⋆ x (y .tail) ys (n , x∈y) in suc m , p

-- mutual
--   ++◇⋆ : ∀ (x : A) y ys → x ∈ concat ys → x ∈ concat⋆ y ys
--   ++◇⋆ x [] ys x∈ys = x∈ys
--   ++◇⋆ x (∹ y) ys x∈ys = ++◇⁺ x y ys x∈ys

--   ++◇⁺ : ∀ (x : A) y ys → x ∈ concat ys → x ∈ concat⁺ y ys
--   ++◇⁺ x y ys x∈ys = let n , p = ++◇⋆ x (y .tail) ys x∈ys in suc n , p

-- concat-∈ : ∀ (x : A) xs → x ∈² xs → x ∈ concat xs
-- concat-∈ x xs (zero  , x∈xs) = ◇++⁺ x (xs zero) (xs ∘ suc) x∈xs
-- concat-∈ x xs (suc n , x∈xs) = ++◇⁺ x (xs zero) (xs ∘ suc) (concat-∈ x (xs ∘ suc) (n , x∈xs))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- Axiomatic Peano arithmetic base
------------------------------------------------------------------------------

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

-- Mendelson's axioms for first-order Peano arithmetic [Mendelson,
-- 1977, p. 155].

-- Elliott Mendelson. Introduction to mathematical logic. Chapman &
-- Hall, 4th edition, 1997, p. 155.

-- NB. These axioms formalize the propositional equality.

module PA.Axiomatic.Mendelson.Base where

infixl 7 _*_
infixl 6 _+_
infix  4 _≈_ _≉_

------------------------------------------------------------------------------
-- First-order logic (without equality)
open import Common.FOL.FOL public renaming ( D to ℕ )

-- Non-logical constants
postulate
  zero    : ℕ
  succ    : ℕ → ℕ
  _+_ _*_ : ℕ → ℕ → ℕ

-- The PA equality.
--
-- N.B. We use the symbol _≈_ for avoiding to use the
-- --no-internal-equality Apia option.
postulate _≈_ : ℕ → ℕ → Set

-- Inequality.
_≉_ : ℕ → ℕ → Set
x ≉ y = ¬ x ≈ y
{-# ATP definition _≉_ #-}

-- Proper axioms

-- S₁. m = n → m = o → n = o
-- S₂. m = n → succ m = succ n
-- S₃. 0 ≠ succ n
-- S₄. succ m = succ n → m = n
-- S₅. 0 + n = n
-- S₆. succ m + n = succ (m + n)
-- S₇. 0 * n = 0
-- S₈. succ m * n = (m * n) + n
-- S₉. P(0) → (∀n.P(n) → P(succ n)) → ∀n.P(n), for any wff P(n) of PA.

postulate
  S₁ : ∀ {m n o} → m ≈ n → m ≈ o → n ≈ o
  S₂ : ∀ {m n} → m ≈ n → succ m ≈ succ n
  S₃ : ∀ {n} → zero ≉ succ n
  S₄ : ∀ {m n} → succ m ≈ succ n → m ≈ n
  S₅ : ∀ n → zero + n ≈ n
  S₆ : ∀ m n → succ m + n ≈ succ (m + n)
  S₇ : ∀ n → zero * n ≈ zero
  S₈ : ∀ m n → succ m * n ≈ n + m * n
{-# ATP axioms S₁ S₂ S₃ S₄ S₅ S₆ S₇ S₈ #-}

-- S₉ is an axiom schema, therefore we do not translate it to TPTP.
postulate S₉ : (A : ℕ → Set) → A zero → (∀ n → A n → A (succ n)) → ∀ n → A n


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

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty
open import Cubical.Data.Sum.Base
open import Cubical.Data.Unit.Base

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

-- Obtain the booleans
open import Agda.Builtin.Bool public

private
  variable
    ℓ : Level
    A : Type ℓ

infixr 6 _and_
infixr 5 _or_
infix  0 if_then_else_

not : Bool → Bool
not true = false
not false = true

_or_ : Bool → Bool → Bool
false or false = false
false or true  = true
true  or false = true
true  or true  = true

_and_ : Bool → Bool → Bool
false and false = false
false and true  = false
true  and false = false
true  and true  = true

-- xor / mod-2 addition
_⊕_ : Bool → Bool → Bool
false ⊕ x = x
true  ⊕ x = not x

if_then_else_ : Bool → A → A → A
if true  then x else y = x
if false then x else y = y

_≟_ : Discrete Bool
false ≟ false = yes refl
false ≟ true  = no λ p → subst (λ b → if b then ⊥ else Bool) p true
true  ≟ false = no λ p → subst (λ b → if b then Bool else ⊥) p true
true  ≟ true  = yes refl

Dec→Bool : Dec A → Bool
Dec→Bool (yes p) = true
Dec→Bool (no ¬p) = false

-- Helpers for automatic proof
Bool→Type : Bool → Type₀
Bool→Type true = Unit
Bool→Type false = ⊥

True : Dec A → Type₀
True Q = Bool→Type (Dec→Bool Q)

False : Dec A → Type₀
False Q = Bool→Type (not (Dec→Bool Q))

toWitness : {Q : Dec A} → True Q → A
toWitness {Q = yes p} _ = p

toWitnessFalse : {Q : Dec A} → False Q → ¬ A
toWitnessFalse {Q = no ¬p} _ = ¬p

dichotomyBool : (x : Bool) → (x ≡ true) ⊎ (x ≡ false)
dichotomyBool true  = inl refl
dichotomyBool false = inr refl

-- TODO: this should be uncommented and implemented using instance arguments
-- _==_ : {dA : Discrete A} → A → A → Bool
-- _==_ {dA = dA} x y = Dec→Bool (dA x y)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module #1 where

open import Relation.Binary.PropositionalEquality

{-
Exercise 2.1. Show that the three obvious proofs of Lemma 2.1.2 are pairwise equal.
-}

ind₌ : ∀{a b}{A : Set a} → (C : (x y : A) → (x ≡ y) → Set b) → ((x : A) → C x x refl) → {x y : A} → (p : x ≡ y) → C x y p
ind₌ C c {x}{y} p rewrite p = c y

composite : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite {i} {A} {_}{_}{z} p = ind₌ D d p where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y _ = y ≡ z → x ≡ z

  d : (x₁ : A) → D x₁ x₁ refl
  d _ = λ x → x

composite' : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite' {i} {A} {_}{_}{z} = ind₌ D d where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y _ = y ≡ z → x ≡ z

  d : (x : A) → D x x refl
  d x = ind₌ E e where
    E : (x z : A) → (q : x ≡ z) → Set i
    E x z _ = x ≡ z

    e : (x : A) → E x x refl
    e x = refl

composite'' : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite'' refl refl = refl

composite=composite' : ∀ {i} {A : Set i}{x y z : A} → (p : x ≡ y)(q : y ≡ z) → composite p q ≡ composite' p q
composite=composite' refl refl = refl

composite=composite'' : ∀ {i} {A : Set i}{x y z : A} → (p : x ≡ y)(q : y ≡ z) → composite p q ≡ composite'' p q
composite=composite'' refl refl = refl

composite'=composite'' : ∀ {i} {A : Set i}{x y z : A} → (p : x ≡ y)(q : y ≡ z) → composite' p q ≡ composite'' p q
composite'=composite'' refl refl = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Pi-2 where

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

open import Groupoid

infixr 10 _◎_
infixr 30 _⟷_

------------------------------------------------------------------------------
-- Level -2
-- Types are -2 groupoids or equivalently all types are contractible or
-- equivalently all types have exactly one point

-- There is no interesting path structure but we have the trivial paths
-- explicitly below.

-- Types and values are defined mutually without reference to programs Types
-- always include PATHs in addition to the usual types.

mutual

  data U : Set where
    ONE   : U
    TIMES : U → U → U
    PATH  : {t : U} → ⟦ t ⟧ → ⟦ t ⟧ → U

  ⟦_⟧ : U → Set
  ⟦ ONE ⟧         = ⊤
  ⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
  ⟦ PATH v₁ v₂ ⟧  = (v₁ ≡ v₂)

-- Proof that all types are contractible. Def. 3.11.1 in the HoTT book

isContr : (t : U) → Σ[ v ∈ ⟦ t ⟧ ] ((v' : ⟦ t ⟧) → (v ≡ v'))
isContr ONE = (tt , λ v → refl)
isContr (TIMES t₁ t₂) with isContr t₁ | isContr t₂
... | (v₁ , f₁) | (v₂ , f₂) = ((v₁ , v₂) , f)
  where f : (vv : ⟦ t₁ ⟧ × ⟦ t₂ ⟧) → (v₁ , v₂) ≡ vv
        f (v₁' , v₂') = cong₂ _,′_ (f₁ v₁') (f₂ v₂')
isContr (PATH {t} v₁ v₂) with isContr t
isContr (PATH {t} v₁ v₂) | (v' , f') = (p , λ q → proof-irrelevance p q)
  where p = trans (sym (f' v₁))  (f' v₂)

-- Proof that every type is a groupoid; this does not depend on the
-- definition of programs

isGroupoid : U → 1Groupoid
isGroupoid ONE              = discrete ⊤
isGroupoid (TIMES t₁ t₂)    = isGroupoid t₁ ×G isGroupoid t₂
isGroupoid (PATH {t} v₁ v₂) = discrete (v₁ ≡ v₂)

-- Programs
-- We use pointed types; programs map a pointed type to another
-- In other words, each program takes one particular value to another; if we
-- want to work on another value, we generally use another program

record U• : Set where
  constructor •[_,_]
  field
    ∣_∣ : U
    • : ⟦ ∣_∣ ⟧

open U•

Space : (t• : U•) → Set
Space •[ t , v ] = ⟦ t ⟧

point : (t• : U•) → Space t•
point •[ t , v ] = v

data _⟷_ : U• → U• → Set where
  id⟷    : {t : U•} → t ⟷ t
  sym⟷   : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
  _◎_     : {t₁ t₂ t₃ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  unite⋆  : {t : U•} → •[ TIMES ONE ∣ t ∣ , (tt , • t) ] ⟷ t
  uniti⋆  : {t : U•} → t ⟷ •[ TIMES ONE ∣ t ∣ , (tt , • t) ]
  swap⋆   : {t₁ t₂ : U•} → •[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂) ] ⟷
                           •[ TIMES ∣ t₂ ∣ ∣ t₁ ∣ , (• t₂ , • t₁) ]
  assocl⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ] ⟷
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ]
  assocr⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ] ⟷
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ]
  _⊗_     : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
            (•[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂ ) ] ⟷
             •[ TIMES ∣ t₃ ∣ ∣ t₄ ∣ , (• t₃ , • t₄ ) ])

-- Proof that the universe is itself a groupoid; this DOES depend on the
-- definition of programs; the morphisms between types ARE the programs; all
-- programs between the same types are forced to be the same using a
-- degenerate observational equivalence relation.

_obs≅_ : {t₁ t₂ : U•} → (c₁ c₂ : t₁ ⟷ t₂) → Set
c₁ obs≅ c₂ = ⊤

UG : 1Groupoid
UG = record
       { set = U•
       ; _↝_ = _⟷_
       ; _≈_ = _obs≅_
       ; id = id⟷
       ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
       ; _⁻¹ = sym⟷
       ; lneutr = λ _ →  tt
       ; rneutr = λ _ → tt
       ; assoc = λ _ _ _ → tt
       ; equiv = record { refl = tt
                        ; sym = λ _ → tt
                        ; trans = λ _ _ → tt
                        }
       ; linv = λ _ → tt
       ; rinv = λ _ → tt
       ; ∘-resp-≈ = λ _ _ → tt
       }

-- Examples

ONE• ONE×ONE• : U•
ONE•     = •[ ONE , tt ]
ONE×ONE• = •[ TIMES ONE ONE , (tt , tt) ]

PathSpace : {t : U•} → ⟦ ∣ t ∣ ⟧ → U•
PathSpace v = •[ PATH v v , refl ]

c₁ c₂ c₃ : ONE• ⟷ ONE•
c₁ = id⟷
c₂ = uniti⋆ ◎ swap⋆ ◎ unite⋆
c₃ = uniti⋆ ◎ uniti⋆ ◎ assocl⋆ ◎ (swap⋆ ⊗ (sym⟷ id⟷)) ◎
     assocr⋆ ◎ unite⋆ ◎ unite⋆

-- The evaluation of a program like c₁, c₂, c₃ above is not done in order to
-- figure out the output value. Both the input and output values are encoded
-- in the type of the program; what the evaluation does is follow the path to
-- constructively reach the ouput value from the input value. Even though the
-- programs are observationally equivalent, they follow different paths. The
-- next level will allow us to reason about which of these paths are
-- connected by 2paths etc. In general, one write programs at level i, and
-- reasons about their (observational) equivalence at levels i+1 and
-- higher. It is always possible to stop this game and use extensional
-- equality at some level, i.e., to equate all programs that connect the same
-- input and output values.

c₄ : ONE×ONE• ⟷ ONE•
c₄ = unite⋆

c₅ : PathSpace tt ⟷ PathSpace tt
c₅ = id⟷

c₁≅c₂ : c₁ obs≅ c₂
c₁≅c₂ = tt

-- the following does not typecheck
-- c₁≅c₄ : c₁ obs≅ c₄
-- it is not possible to equate programs that go between different types/values.

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


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Imports.Issue3730 where
X : _
X = _


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Weight biased leftist tree that proves both priority and rank    --
-- invariants. Uses a two-pass merging algorithm.                   --
----------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
module TwoPassMerge.CombinedProofs where

open import Basics
open import Sized
open import TwoPassMerge.RankProof using ( makeT-lemma; proof-1; proof-2 )

-- Now that we have separate proofs of priority and rank invariants we
-- can combine them into one proof. We index Heap with two indices:
-- one for Priority and one for Rank.
data Heap : {i : Size} → Priority → Rank → Set where
  empty : {i : Size} {b : Priority} → Heap {↑ i} b zero
  node  : {i : Size} {b : Priority} → (p : Priority) → p ≥ b → {l r : Rank} →
          l ≥ r → Heap {i} p l → Heap {i} p r → Heap {↑ i} b (suc (l + r))

-- Now we will combine functions that prove priority invariant and
-- functions that prove rank invariant into functions that prove both
-- invariants.

-- Let's begin with singleton. Note the type of created Heap. We set
-- first index to zero, because it proves the priority invariant and
-- second index to one because it proves rank invariant. The node now
-- needs two ge0 evidence.
singleton : Priority → Heap zero one
singleton p = node p ge0 ge0 empty empty

-- makeT function requires that we supply evidence that priority
-- invariant holds (value of type p ≥ b), guarantees that resulting
-- heap has correct size and maintains rank invariant by using Order
-- type to supply evidence of rank correctness to node constructor.
makeT : {b : Priority} {l r : Rank} → (p : Priority) → p ≥ b →
      Heap p l → Heap p r → Heap b (suc (l + r))
makeT {b} {l-rank} {r-rank} p p≥n l r with order l-rank r-rank
makeT {b} {l-rank} {r-rank} p p≥n l r | ge l≥r
  = node p p≥n l≥r l r
makeT {b} {l-rank} {r-rank} p p≥n l r | le r≥l
  = subst (Heap b) (makeT-lemma r-rank l-rank) (node p p≥n r≥l r l)

-- merge combines previous proofs:
--
--  1) it enforces priority invariant by comparing priorities using
--     order function. Recall that this function returns value of
--     Order datatype that not only gives a result of comparison but
--     also supplies evidence that result is true. That evidence is
--     given to makeT which uses it to construct a new node.
--
--  2) it proves size invariant of merge by reusing proofs from
--     TwoPassMerge.RankProof
--
--  3) it delegates the proof of rank invariant to makeT
merge : {i j : Size} {b : Priority} {l r : Rank} → Heap {i} b l → Heap {j} b r
      → Heap b (l + r)
merge empty h2 = h2 -- See [merge, proof 0a]
merge {_} .{_} {b} {suc l} {zero} h1 empty
  = subst (Heap b)
          (sym (+0 (suc l)))  -- See [merge, proof 0b]
          h1
merge .{↑ i} .{↑ j} .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  with order p1 p2
merge .{↑ i} .{↑ j} .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | le p1≤p2
  = subst (Heap b)
          (proof-1 l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 1]
          (makeT p1 p1≥b l1 (merge {i} {↑ j} r1 (node p2 p1≤p2 l2≥r2 l2 r2)))
merge .{↑ i} .{↑ j} .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | ge p1≥p2
  = subst (Heap b)
          (proof-2 l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 2]
          (makeT p2 p2≥b l2 (merge {j} {↑ i} r2 (node p1 p1≥p2 l1≥r1 l1 r1)))

-- Implementations of insert and findMin are the same as
-- previously. We only need to update the type signature accordingly.
insert : {b : Priority} {r : Rank} → Priority → Heap zero r → Heap zero (suc r)
insert p h = merge (singleton p) h

findMin : {b : Priority} {r : Rank} → Heap b (suc r) → Priority
findMin (node p _ _ _ _) = p

-- To define deleteMin we will need to update definition of
-- liftBound. We need to redefine ≥trans because Agda won't let us
-- import it from a module that has unfinished implementation (recall
-- that we left definitions of findMin and deleteMin incomplete in
-- TwoPassMerge.PriorityProof).
≥trans : {a b c : Nat} → a ≥ b → b ≥ c → a ≥ c
≥trans a≥b        ge0      = ge0
≥trans (geS a≥b) (geS b≥c) = geS (≥trans a≥b b≥c)

liftBound : {p b : Priority} → b ≥ p → {r : Rank} → Heap b r → Heap p r
liftBound b≥n empty                = empty
liftBound b≥n (node p p≥b l≥r l r) = node p (≥trans p≥b b≥n) l≥r l r

-- With the new definition of liftBound we can now define deleteMin.
-- Implementation is identical to the one in TwoPassMerge.RankProof -
-- we only had to update type signature.
deleteMin : {b : Priority} {r : Rank} → Heap b (suc r) → Heap b r
deleteMin (node _ p≥b _ l r) = merge (liftBound p≥b l) (liftBound p≥b r)

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
-- This was accepted, since we didn't fail on mismatched sorts when
-- comparing types.
module Issue485 where

ap : ((A : Set) → A → A) → Set → Set
ap f A = f _ A


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

module Data.Nat.Reasoning where

open import Data.Nat
import Data.Nat.Properties as ℕ-Prop
open import Relation.Binary.PropositionalEquality

infixr 3 _*≫_ _≪*_ _+≫_ _≪+_
_*≫_ : ∀ {x y} z → x ≡ y → z * x ≡ z * y
_*≫_ _ = cong _

_+≫_ : ∀ {x y} z → x ≡ y → z + x ≡ z + y
_+≫_ _ = cong _

_≪*_ : ∀ {x y} z → x ≡ y → x * z ≡ y * z
_≪*_ _ = cong _

_≪+_ : ∀ {x y} z → x ≡ y → x + z ≡ y + z
_≪+_ _ = cong _

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
------------------------------------------------------------------------
-- The state monad transformer
------------------------------------------------------------------------

-- The interface is based on that used by the "mtl" package on
-- Hackage.

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

open import Equality

module Monad.State
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude

open Derived-definitions-and-properties eq
open import Monad eq

-- The state monad transformer, defined using a wrapper type to make
-- instance resolution easier.

record StateT {s} (S : Type s)
              (M : Type s → Type s)
              (A : Type s) : Type s where
  constructor wrap
  field
    run : S → M (A × S)

open StateT public

instance

  -- StateT is a "raw monad" transformer.

  raw-monad-transformer :
    ∀ {s} {S : Type s} →
    Raw-monad-transformer (StateT S)
  run (Raw-monad.return (Raw-monad-transformer.transform
                           raw-monad-transformer) x) =
    λ s → return (x , s)
  run (Raw-monad._>>=_ (Raw-monad-transformer.transform
                          raw-monad-transformer) x f) =
    λ s → run x s >>= λ { (x , s) → run (f x) s }

  run (Raw-monad-transformer.liftʳ raw-monad-transformer m) =
    λ s → map (_, s) m

  transform : ∀ {s} {S : Type s} {M} ⦃ is-raw-monad : Raw-monad M ⦄ →
              Raw-monad (StateT S M)
  transform = Raw-monad-transformer.transform raw-monad-transformer

-- StateT is a monad transformer (assuming extensionality).

monad-transformer :
  ∀ {s} {S : Type s} →
  Extensionality s s →
  Monad-transformer (StateT S)
Monad.raw-monad (Monad-transformer.transform (monad-transformer _)) =
  Raw-monad-transformer.transform raw-monad-transformer

Monad.left-identity (Monad-transformer.transform
                       (monad-transformer ext)) x f =
  cong wrap (apply-ext ext λ s →
    (return (x , s) >>= λ { (x , s) → run (f x) s })  ≡⟨ left-identity _ _ ⟩∎
    run (f x) s                                       ∎)

Monad.right-identity (Monad-transformer.transform
                        (monad-transformer ext)) x =
  cong wrap (apply-ext ext λ s →
    run x s >>= (λ { (x , s) → return (x , s) })  ≡⟨ right-identity _ ⟩∎
    run x s                                       ∎)

Monad.associativity (Monad-transformer.transform
                       (monad-transformer ext)) x f g =
  cong wrap (apply-ext ext λ s →
    (run x s >>= λ { (x , s) →
     run (f x) s >>= λ { (x , s) →
     run (g x) s } })                                             ≡⟨ associativity _ _ _ ⟩∎

    ((run x s >>= λ { (x , s) → run (f x) s }) >>= λ { (x , s) →
     run (g x) s })                                               ∎)

Monad-transformer.liftᵐ (monad-transformer _) = liftʳ

Monad-transformer.lift-return (monad-transformer ext) x =
  cong wrap (apply-ext ext λ s →
    map (_, s) (return x)  ≡⟨ map-return _ _ ⟩∎
    return (x , s)         ∎)

Monad-transformer.lift->>= (monad-transformer ext) x f =
  cong wrap (apply-ext ext λ s →
    map (_, s) (x >>= f)                                 ≡⟨ map->>= _ _ _ ⟩
    (x >>= λ x → map (_, s) (f x))                       ≡⟨ sym $ >>=-map ext _ _ _ ⟩∎
    (map (_, s) x >>= λ { (x , s) → map (_, s) (f x) })  ∎)

-- Returns the state.

get : ∀ {s} {S : Type s} {M} ⦃ is-monad : Raw-monad M ⦄ →
      StateT S M S
run get = λ s → return (s , s)

-- Types the state.

set : ∀ {s} {S : Type s} {M} ⦃ is-monad : Raw-monad M ⦄ →
      S → StateT S M (↑ _ ⊤)
run (set s) = λ _ → return (_ , s)

-- Modifies the state.

modify :
  ∀ {s} {S : Type s} {M} ⦃ is-monad : Raw-monad M ⦄ →
  (S → S) → StateT S M (↑ _ ⊤)
modify f = get >>= set ∘ f

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Records where

variable
  a b : Set

-- parametrized record type exported as an Haskell record
record Pair (a b : Set) : Set where
  constructor MkPair
  field
    proj₁ : a
    proj₂ : b

open Pair public

{-# COMPILE AGDA2HS Pair #-}

-- no named constructor means we reuse the record name

record Wrap (a : Set) : Set where
  field
    unwrap : a

open Wrap public

{-# COMPILE AGDA2HS Wrap #-}

-- record type exported as an Haskell class definition
record MyMonoid (a : Set) : Set where
  field
    mempty  : a
    mappend : a → a → a

{-# COMPILE AGDA2HS MyMonoid class #-}

swap : Pair a b → Pair b a
swap (MkPair x y) = MkPair y x

swap₂ : Wrap (Pair a b) → Wrap (Pair b a)
swap₂ (record {unwrap = p}) = record {unwrap = record { proj₁ = proj₂ p; proj₂ = p .proj₁ } }

{-# COMPILE AGDA2HS swap #-}
{-# COMPILE AGDA2HS swap₂ #-}