text:
module Structure.Function.Domain.Proofs where

open import Data.Tuple as Tuple using (_⨯_ ; _,_)
import      Lvl
open import Functional
open import Function.Domains
open import Function.Equals
import      Function.Names as Names
open import Lang.Instance
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Setoid.Uniqueness
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Transitivity
open import Type
open import Type.Dependent

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₒ₁ ℓₒ₂ : Lvl.Level
private variable T A B C : Type{ℓ}

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₑ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ (f : A → B) where
  injective-to-unique : Injective(f) → ∀{y} → Unique(x ↦ f(x) ≡ y)
  injective-to-unique (intro(inj)) {y} {x₁}{x₂} fx₁y fx₂y =
    inj{x₁}{x₂} (fx₁y 🝖 symmetry(_≡_) fx₂y)

  instance
    bijective-to-injective : ⦃ bij : Bijective(f) ⦄ → Injective(f)
    Injective.proof(bijective-to-injective ⦃ intro(bij) ⦄) {x₁}{x₂} (fx₁fx₂) =
      ([∃!]-existence-eq (bij {f(x₂)}) {x₁} (fx₁fx₂))
      🝖 symmetry(_≡_) ([∃!]-existence-eq (bij {f(x₂)}) {x₂} (reflexivity(_≡_)))
    -- ∀{y : B} → ∃!(x ↦ f(x) ≡ y)
    -- ∃!(x ↦ f(x) ≡ f(x₂))
    -- ∀{x} → (f(x) ≡ f(x₂)) → (x ≡ [∃!]-witness e)
    -- (f(x₁) ≡ f(x₂)) → (x₁ ≡ [∃!]-witness e)
    --
    -- ∀{y : B} → ∃!(x ↦ f(x) ≡ y)
    -- ∃!(x ↦ f(x) ≡ f(x₂))
    -- ∀{x} → (f(x) ≡ f(x₂)) → (x ≡ [∃!]-witness e)
    -- (f(x₂) ≡ f(x₂)) → (x₂ ≡ [∃!]-witness e)

  instance
    bijective-to-surjective : ⦃ bij : Bijective(f) ⦄ → Surjective(f)
    Surjective.proof(bijective-to-surjective ⦃ intro(bij) ⦄) {y} =
      [∃!]-existence (bij {y})

  instance
    injective-surjective-to-bijective : ⦃ inj : Injective(f) ⦄ → ⦃ surj : Surjective(f) ⦄ → Bijective(f)
    Bijective.proof(injective-surjective-to-bijective ⦃ inj ⦄ ⦃ intro(surj) ⦄) {y} =
      [∃!]-intro surj (injective-to-unique inj)

  injective-surjective-bijective-equivalence : (Injective(f) ∧ Surjective(f)) ↔ Bijective(f)
  injective-surjective-bijective-equivalence =
    [↔]-intro
      (\bij → [∧]-intro (bijective-to-injective ⦃ bij = bij ⦄) (bijective-to-surjective ⦃ bij = bij ⦄))
      (\{([∧]-intro inj surj) → injective-surjective-to-bijective ⦃ inj = inj ⦄ ⦃ surj = surj ⦄})

module _ {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  instance
    injective-relator : UnaryRelator(Injective{A = A}{B = B})
    Injective.proof (UnaryRelator.substitution injective-relator {f₁}{f₂} (intro f₁f₂) (intro inj-f₁)) f₂xf₂y = inj-f₁ (f₁f₂ 🝖 f₂xf₂y 🝖 symmetry(_≡_) f₁f₂)

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  instance
    surjective-relator : UnaryRelator(Surjective{A = A}{B = B})
    Surjective.proof (UnaryRelator.substitution surjective-relator {f₁}{f₂} (intro f₁f₂) (intro surj-f₁)) {y} = [∃]-map-proof (\{x} f₁xf₁y → symmetry(_≡_) (f₁f₂{x}) 🝖 f₁xf₁y) (surj-f₁{y})

module _ {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  instance
    bijective-relator : UnaryRelator(Bijective{A = A}{B = B})
    UnaryRelator.substitution bijective-relator {f₁}{f₂} f₁f₂ bij-f₁ = injective-surjective-to-bijective(f₂) ⦃ substitute₁(Injective) f₁f₂ (bijective-to-injective(f₁)) ⦄ ⦃ substitute₁(Surjective) f₁f₂ (bijective-to-surjective(f₁)) ⦄ where
      instance _ = bij-f₁

module _
  {A : Type{ℓₒ₁}}
  {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  where

  invᵣ-surjective : (f : A → B) ⦃ surj : Surjective(f) ⦄ → (B → A)
  invᵣ-surjective _ ⦃ surj ⦄ (y) = [∃]-witness(Surjective.proof surj{y})

module _
  {A : Type{ℓₒ₁}}
  {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B}
  where

  surjective-to-inverseᵣ : ⦃ surj : Surjective(f) ⦄ → Inverseᵣ(f)(invᵣ-surjective f)
  surjective-to-inverseᵣ ⦃ intro surj ⦄ = intro([∃]-proof surj)

module _
  {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B} {f⁻¹ : B → A}
  where

  inverseᵣ-to-surjective : ⦃ inverᵣ : Inverseᵣ(f)(f⁻¹) ⦄ → Surjective(f)
  Surjective.proof inverseᵣ-to-surjective {y} = [∃]-intro (f⁻¹(y)) ⦃ inverseᵣ(f)(f⁻¹) ⦄

  Inverse-symmetry : Inverse(f)(f⁻¹) → Inverse(f⁻¹)(f)
  Inverse-symmetry ([∧]-intro (intro inverₗ) (intro inverᵣ)) = [∧]-intro (intro inverᵣ) (intro inverₗ)

module _
  {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B}
  where

  invertibleᵣ-to-surjective : ⦃ inverᵣ : Invertibleᵣ(f) ⦄ → Surjective(f)
  ∃.witness (Surjective.proof(invertibleᵣ-to-surjective ⦃ inverᵣ ⦄) {y}) = [∃]-witness inverᵣ(y)
  ∃.proof   (Surjective.proof(invertibleᵣ-to-surjective ⦃ inverᵣ ⦄) {y}) = inverseᵣ _ _ ⦃ [∧]-elimᵣ([∃]-proof inverᵣ) ⦄

  -- Every surjective function has a right inverse with respect to function composition.
  -- One of the right inverse functions of a surjective function f.
  -- Specifically the one that is used in the constructive proof of surjectivity for f.
  -- Without assuming that the value used in the proof of surjectivity constructs a function, this would be unprovable because it is not guaranteed in arbitrary setoids.
  -- Note: The usual formulation of this proposition (without assuming `inv-func`) is equivalent to the axiom of choice from set theory in classical logic.
  surjective-to-invertibleᵣ : ⦃ surj : Surjective(f) ⦄ ⦃ inv-func : Function(invᵣ-surjective f) ⦄ → Invertibleᵣ(f)
  ∃.witness (surjective-to-invertibleᵣ)                                                 = invᵣ-surjective f
  ∃.proof   (surjective-to-invertibleᵣ ⦃ surj = intro surj ⦄ ⦃ inv-func = inv-func ⦄)   = [∧]-intro inv-func (intro([∃]-proof surj))

  invertibleᵣ-when-surjective : Invertibleᵣ(f) ↔ Σ(Surjective(f)) (surj ↦ Function(invᵣ-surjective f ⦃ surj ⦄))
  invertibleᵣ-when-surjective =
    [↔]-intro
      (surj   ↦ surjective-to-invertibleᵣ ⦃ Σ.left surj ⦄ ⦃ Σ.right surj ⦄)
      (inverᵣ ↦ intro (invertibleᵣ-to-surjective ⦃ inverᵣ ⦄) ([∧]-elimₗ([∃]-proof inverᵣ)))

module _
  {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B} {f⁻¹ : B → A} ⦃ inverᵣ : Inverseᵣ(f)(f⁻¹) ⦄
  where

  -- Note: This states that a function which is injective and surjective (bijective) is a function, but another way of satisfying this proposition is from a variant of axiom of choice which directly state that the right inverse of a surjective function always exist.
  inverseᵣ-function : ⦃ inj : Injective(f) ⦄ → Function(f⁻¹)
  Function.congruence (inverseᵣ-function) {y₁}{y₂} y₁y₂ =
    injective(f) (
      f(f⁻¹(y₁)) 🝖-[ inverseᵣ(f)(f⁻¹) ]
      y₁         🝖-[ y₁y₂ ]
      y₂         🝖-[ inverseᵣ(f)(f⁻¹) ]-sym
      f(f⁻¹(y₂)) 🝖-end
    )

  -- The right inverse is injective when f is a surjective function.
  inverseᵣ-injective : ⦃ func : Function(f) ⦄ → Injective(f⁻¹)
  Injective.proof(inverseᵣ-injective) {x₁}{x₂} (invᵣfx₁≡invᵣfx₂) =
    x₁         🝖-[ inverseᵣ(f)(f⁻¹) ]-sym
    f(f⁻¹(x₁)) 🝖-[ congruence₁(f) {f⁻¹(x₁)} {f⁻¹(x₂)} (invᵣfx₁≡invᵣfx₂) ]
    f(f⁻¹(x₂)) 🝖-[ inverseᵣ(f)(f⁻¹) ]
    x₂         🝖-end

  -- The right inverse is surjective when the surjective f is injective.
  inverseᵣ-surjective : ⦃ inj : Injective(f) ⦄ → Surjective(f⁻¹)
  ∃.witness (Surjective.proof inverseᵣ-surjective {x}) = f(x)
  ∃.proof   (Surjective.proof inverseᵣ-surjective {x}) =
    injective(f) (
      f(f⁻¹(f(x))) 🝖-[ inverseᵣ(f)(f⁻¹) ]
      f(x)         🝖-end
    )

  -- The right inverse is a left inverse when the surjective f is injective.
  inverseᵣ-inverseₗ : ⦃ inj : Injective(f) ⦄ → Inverseₗ(f)(f⁻¹)
  inverseᵣ-inverseₗ = intro([∃]-proof(surjective(f⁻¹) ⦃ inverseᵣ-surjective ⦄))

  -- The right inverse is bijective when the surjective f is injective.
  inverseᵣ-bijective : ⦃ func : Function(f) ⦄ ⦃ inj : Injective(f) ⦄ → Bijective(f⁻¹)
  inverseᵣ-bijective = injective-surjective-to-bijective(f⁻¹) ⦃ inverseᵣ-injective ⦄ ⦃ inverseᵣ-surjective ⦄

  inverseᵣ-inverse : ⦃ inj : Injective(f) ⦄ → Inverse(f)(f⁻¹)
  inverseᵣ-inverse = [∧]-intro inverseᵣ-inverseₗ inverᵣ

  -- The right inverse is an unique right inverse when f is injective.
  inverseᵣ-unique-inverseᵣ : ⦃ inj : Injective(f) ⦄ → ∀{g} → (f ∘ g ⊜ id) → (g ⊜ f⁻¹)
  inverseᵣ-unique-inverseᵣ {g = g} (intro p) = intro $ \{x} →
    g(x)         🝖-[ inverseₗ(f)(f⁻¹) ⦃ inverseᵣ-inverseₗ ⦄ ]-sym
    f⁻¹(f(g(x))) 🝖-[ congruence₁(f⁻¹) ⦃ inverseᵣ-function ⦄ p ]
    f⁻¹(x)       🝖-end

  -- The right inverse is an unique left inverse function.
  inverseᵣ-unique-inverseₗ : ∀{g} ⦃ _ : Function(g) ⦄ → (g ∘ f ⊜ id) → (g ⊜ f⁻¹)
  inverseᵣ-unique-inverseₗ {g = g} (intro p) = intro $ \{x} →
    g(x)         🝖-[ congruence₁(g) (inverseᵣ(f)(f⁻¹)) ]-sym
    g(f(f⁻¹(x))) 🝖-[ p{f⁻¹(x)} ]
    f⁻¹(x)       🝖-end

  -- The right inverse is invertible.
  inverseᵣ-invertibleᵣ : ⦃ func : Function(f) ⦄ ⦃ inj : Injective(f) ⦄ → Invertibleᵣ(f⁻¹)
  ∃.witness inverseᵣ-invertibleᵣ                   = f
  ∃.proof   (inverseᵣ-invertibleᵣ ⦃ func = func ⦄) = [∧]-intro func inverseᵣ-inverseₗ

  -- TODO: invᵣ-unique-function : ∀{g} → (invᵣ(f) ∘ g ⊜ id) → (g ⊜ f)

module _
  {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B} {f⁻¹ : B → A} ⦃ inverₗ : Inverseₗ(f)(f⁻¹) ⦄
  where

  inverseₗ-surjective : Surjective(f⁻¹)
  inverseₗ-surjective = inverseᵣ-to-surjective

  inverseₗ-to-injective : ⦃ invₗ-func : Function(f⁻¹) ⦄ → Injective(f)
  inverseₗ-to-injective = inverseᵣ-injective

module _
  {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f   : A → B} ⦃ func     : Function(f)   ⦄
  {f⁻¹ : B → A} ⦃ inv-func : Function(f⁻¹) ⦄
  where

  inverseₗ-to-inverseᵣ : ⦃ surj : Surjective(f) ⦄ ⦃ inverₗ : Inverseₗ(f)(f⁻¹) ⦄ → Inverseᵣ(f)(f⁻¹)
  Inverseᵣ.proof inverseₗ-to-inverseᵣ {x} with [∃]-intro y ⦃ p ⦄ ← surjective f{x} =
    f(f⁻¹(x))    🝖-[ congruence₁(f) (congruence₁(f⁻¹) p) ]-sym
    f(f⁻¹(f(y))) 🝖-[ congruence₁(f) (inverseₗ(f)(f⁻¹)) ]
    f(y)         🝖-[ p ]
    x            🝖-end

  module _ ⦃ surj : Surjective(f) ⦄ ⦃ inverₗ : Inverseₗ(f)(f⁻¹) ⦄ where
    inverseₗ-injective : Injective(f⁻¹)
    Injective.proof inverseₗ-injective {x}{y} p =
      x         🝖-[ inverseᵣ(f)(f⁻¹) ⦃ inverseₗ-to-inverseᵣ ⦄ ]-sym
      f(f⁻¹(x)) 🝖-[ congruence₁(f) p ]
      f(f⁻¹(y)) 🝖-[ inverseᵣ(f)(f⁻¹) ⦃ inverseₗ-to-inverseᵣ ⦄ ]
      y         🝖-end

    inverseₗ-bijective : Bijective(f⁻¹)
    inverseₗ-bijective = injective-surjective-to-bijective(f⁻¹) ⦃ inverseₗ-injective ⦄ ⦃ inverseₗ-surjective ⦄

    inverseₗ-to-surjective : Surjective(f)
    inverseₗ-to-surjective = inverseᵣ-surjective ⦃ inj = inverseₗ-injective ⦄

    inverseₗ-to-bijective : Bijective(f)
    inverseₗ-to-bijective = injective-surjective-to-bijective(f) ⦃ inverseₗ-to-injective ⦄ ⦃ inverseₗ-to-surjective ⦄

module _
  {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B} {f⁻¹ : B → A} ⦃ inver : Inverse(f)(f⁻¹) ⦄
  where

  inverse-to-surjective : Surjective(f)
  inverse-to-surjective = inverseᵣ-to-surjective ⦃ inverᵣ = [∧]-elimᵣ inver ⦄

  module _ ⦃ inv-func : Function(f⁻¹) ⦄ where
    inverse-to-injective : Injective(f)
    inverse-to-injective = inverseₗ-to-injective ⦃ inverₗ = [∧]-elimₗ inver ⦄

    inverse-to-bijective : Bijective(f)
    inverse-to-bijective = injective-surjective-to-bijective(f) ⦃ inj = inverse-to-injective ⦄ ⦃ surj = inverse-to-surjective ⦄

  inverse-surjective : Surjective(f⁻¹)
  inverse-surjective = inverseₗ-surjective ⦃ inverₗ = [∧]-elimₗ inver ⦄

  module _ ⦃ func : Function(f) ⦄ where
    inverse-injective : Injective(f⁻¹)
    inverse-injective = inverseᵣ-injective ⦃ inverᵣ = [∧]-elimᵣ inver ⦄ ⦃ func = func ⦄

    inverse-bijective : Bijective(f⁻¹)
    inverse-bijective = injective-surjective-to-bijective(f⁻¹) ⦃ inj = inverse-injective ⦄ ⦃ surj = inverse-surjective ⦄

  inverse-function-when-injective : Function(f⁻¹) ↔ Injective(f)
  inverse-function-when-injective =
    [↔]-intro
      (inj ↦ inverseᵣ-function ⦃ inverᵣ = [∧]-elimᵣ inver ⦄ ⦃ inj = inj ⦄)
      (inv-func ↦ inverse-to-injective ⦃ inv-func = inv-func ⦄)

  function-when-inverse-injective : Function(f) ↔ Injective(f⁻¹)
  function-when-inverse-injective =
    [↔]-intro
      (inv-inj ↦ intro(\{x y} → xy ↦ injective(f⁻¹) ⦃ inv-inj ⦄ (
        f⁻¹(f(x)) 🝖-[ inverseₗ(f)(f⁻¹) ⦃ [∧]-elimₗ inver ⦄ ]
        x         🝖-[ xy ]
        y         🝖-[ inverseₗ(f)(f⁻¹) ⦃ [∧]-elimₗ inver ⦄ ]-sym
        f⁻¹(f(y)) 🝖-end
      )))
      (func ↦ inverse-injective ⦃ func = func ⦄)

  -- TODO: inverse-function-when-bijective : Function(f⁻¹) ↔ Bijective(f)
  -- Surjective(f) ↔ Injective(f⁻¹)
  -- Injective(f) ↔ Surjective(f⁻¹)

module _
  {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {f : A → B} ⦃ inver : Invertible(f) ⦄
  where

  invertible-elimₗ : Invertibleₗ(f)
  invertible-elimₗ = [∃]-map-proof (Tuple.mapRight [∧]-elimₗ) inver

  invertible-elimᵣ : Invertibleᵣ(f)
  invertible-elimᵣ = [∃]-map-proof (Tuple.mapRight [∧]-elimᵣ) inver

module _
  {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  where

  private variable f : A → B

  -- invertible-intro : ⦃ inverₗ : Invertibleₗ(f) ⦄ ⦃ inverᵣ : Invertibleᵣ(f) ⦄ → Invertible(f)
  -- invertible-intro = {!!}

  bijective-to-invertible : ⦃ bij : Bijective(f) ⦄ → Invertible(f)
  bijective-to-invertible {f = f} ⦃ bij = bij ⦄ = [∃]-intro f⁻¹ ⦃ [∧]-intro f⁻¹-function ([∧]-intro f⁻¹-inverseₗ f⁻¹-inverseᵣ) ⦄ where
    f⁻¹ : B → A
    f⁻¹ = invᵣ-surjective f ⦃ bijective-to-surjective(f) ⦄

    f⁻¹-inverseᵣ : Inverseᵣ(f)(f⁻¹)
    f⁻¹-inverseᵣ = surjective-to-inverseᵣ ⦃ surj = bijective-to-surjective(f) ⦄

    f⁻¹-inverseₗ : Inverseₗ(f)(f⁻¹)
    f⁻¹-inverseₗ = inverseᵣ-inverseₗ ⦃ inverᵣ = f⁻¹-inverseᵣ ⦄  ⦃ inj = bijective-to-injective(f) ⦄

    f⁻¹-function : Function(f⁻¹)
    f⁻¹-function = inverseᵣ-function ⦃ inverᵣ = f⁻¹-inverseᵣ ⦄ ⦃ inj = bijective-to-injective(f) ⦄

  invertible-to-bijective : ⦃ inver : Invertible(f) ⦄ → Bijective(f)
  invertible-to-bijective {f} ⦃ ([∃]-intro f⁻¹ ⦃ [∧]-intro func inver ⦄) ⦄ =
    injective-surjective-to-bijective(f)
      ⦃ inj  = inverse-to-injective  ⦃ inver = inver ⦄ ⦃ inv-func = func ⦄ ⦄
      ⦃ surj = inverse-to-surjective ⦃ inver = inver ⦄ ⦄

  invertible-when-bijective : Invertible(f) ↔ Bijective(f)
  invertible-when-bijective = [↔]-intro (bij ↦ bijective-to-invertible ⦃ bij ⦄) (inver ↦ invertible-to-bijective ⦃ inver ⦄)

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:
module Eval where

open import Coinduction
open import Data.Bool
open import Data.Fin     using (Fin)
import      Data.Fin     as F
open import Data.Product using (Σ; _,_)
import      Data.Product as P
open import Data.Stream  using (Stream; _∷_)
import      Data.Stream  as S
open import Data.Vec     using (Vec; []; _∷_)
import      Data.Vec     as V
open import Relation.Binary.PropositionalEquality

open import Types

⟦_⟧ᵗ : Type → Set
⟦ 𝔹     ⟧ᵗ = Bool
⟦ 𝔹⁺ n  ⟧ᵗ = Vec Bool n
⟦ ℂ τ   ⟧ᵗ = Stream ⟦ τ ⟧ᵗ
⟦ σ ⇒ τ ⟧ᵗ = ⟦ σ ⟧ᵗ → ⟦ τ ⟧ᵗ
⟦ σ × τ ⟧ᵗ = P._×_ ⟦ σ ⟧ᵗ ⟦ τ ⟧ᵗ

data Env : ∀ {n} → Ctx n → Set where
  [] : Env []
  _∷_ : ∀ {n} {Γ : Ctx n} {τ} → ⟦ τ ⟧ᵗ → Env Γ → Env (τ ∷ Γ)

lookupEnv : ∀ {n} {Γ : Ctx n} (i : Fin n) → Env Γ → ⟦ V.lookup i Γ ⟧ᵗ
lookupEnv F.zero (x ∷ env) = x
lookupEnv (F.suc i) (x ∷ env) = lookupEnv i env

private
  runReg : ∀ {σ τ} → (⟦ τ ⟧ᵗ → ⟦ τ ⟧ᵗ P.× ⟦ σ ⟧ᵗ) → ⟦ τ ⟧ᵗ → Stream ⟦ σ ⟧ᵗ
  runReg f s with f s
  runReg f s | s′ , x = x ∷ ♯ (runReg f s′)

_⟦_⟧ : ∀ {n} {Γ : Ctx n} {τ} → Env Γ → Term Γ τ → ⟦ τ ⟧ᵗ
env ⟦ bitI ⟧ = true
env ⟦ bitO ⟧ = false
env ⟦ [] ⟧ = []
env ⟦ x ∷ xs ⟧ = env ⟦ x ⟧ ∷ env ⟦ xs ⟧
env ⟦ x nand y ⟧ with env ⟦ x ⟧ | env ⟦ y ⟧
env ⟦ x nand y ⟧ |  true |  true = false
env ⟦ x nand y ⟧ |     _ |     _ =  true
env ⟦ reg xt ft ⟧ = runReg (env ⟦ ft ⟧) (env ⟦ xt ⟧)
env ⟦ pair xt yt ⟧ = (env ⟦ xt ⟧) , (env ⟦ yt ⟧)
env ⟦ latest t ⟧ = S.head (env ⟦ t ⟧)
env ⟦ head t ⟧ = V.head (env ⟦ t ⟧)
env ⟦ tail t ⟧ = V.tail (env ⟦ t ⟧)
env ⟦ var i refl ⟧ = lookupEnv i env
env ⟦ f ∙ x ⟧ = (env ⟦ f ⟧) (env ⟦ x ⟧)
env ⟦ lam t ⟧ = λ x → (x ∷ env) ⟦ t ⟧

ext: agda

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.Mul {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Plus struct
open import MLib.Algebra.Operations struct

open FunctionProperties
open Table using (head; tail; rearrange; fromList; toList; _≗_)

1● : ∀ {n} → Matrix S n n
1● i j with i Fin.≟ j
1● i j | yes _ = 1′
1● i j | no  _ = 0′

infixl 7 _⊗_

_⊗_ : ∀ {m n o} → Matrix S m n → Matrix S n o → Matrix S m o
_⊗_ {n = n} A B i k = ∑[ j < n ] (A i j *′ B j k)

⊗-cong : ∀ {m n o} {A A′ : Matrix S m n} {B B′ : Matrix S n o} → A ≈ A′ → B ≈ B′ → (A ⊗ B) ≈ (A′ ⊗ B′)
⊗-cong A≈A′ B≈B′ i k = sumₜ-cong (λ j → cong * (A≈A′ i j) (B≈B′ j k))

open _≃_

1●-cong-≃ : ∀ {m n} → m ≡ n → 1● {m} ≃ 1● {n}
1●-cong-≃ ≡.refl = ≃-refl

⊗-cong-≃ : ∀ {m n o m′ n′ o′} (A : Matrix S m n) (B : Matrix S n o) (A′ : Matrix S m′ n′) (B′ : Matrix S n′ o′) → A ≃ A′ → B ≃ B′ → (A ⊗ B) ≃ (A′ ⊗ B′)
⊗-cong-≃ A B A′ B′ p q .m≡p = p .m≡p
⊗-cong-≃ A B A′ B′ p q .n≡q = q .n≡q
⊗-cong-≃ {n = n} {n′ = n′} A B A′ B′ p q .equal {i} {i′} {k} {k′} i≅i′ k≅k′ =
  begin
    (A  ⊗ B ) i k                       ≡⟨⟩
    ∑[ j  < n  ] (A  i  j  *′ B  j  k)  ≈⟨ sumₜ-cong′ {n} {n′} (p .n≡q , λ _ _ j≅j′ → cong * (p .equal i≅i′ j≅j′) (q .equal j≅j′ k≅k′)) ⟩
    ∑[ j′ < n′ ] (A′ i′ j′ *′ B′ j′ k′) ≡⟨⟩
    (A′ ⊗ B′) i′ k′                     ∎
  where
    open EqReasoning S.setoid

⊗-assoc :
  ⦃ props : Has ( * ⟨ distributesOverˡ ⟩ₚ +
                ∷ * ⟨ distributesOverʳ ⟩ₚ +
                ∷ associative on *
                ∷ 0# is leftZero for *
                ∷ 0# is rightZero for *
                ∷ 0# is leftIdentity for +
                ∷ associative on +
                ∷ commutative on +
                ∷ []) ⦄
  → ∀ {m n p q} (A : Matrix S m n) (B : Matrix S n p) (C : Matrix S p q)
  → ((A ⊗ B) ⊗ C) ≈ (A ⊗ (B ⊗ C))
⊗-assoc ⦃ props ⦄ {m} {n} {p} {q} A B C i l =
  begin
    ((A ⊗ B) ⊗ C) i l                                    ≡⟨⟩
    ∑[ k < p ] (∑[ j < n ] (A i j *′ B j k) *′ C k l)     ≈⟨ sumₜ-cong {p} (λ k → sumDistribʳ ⦃ weaken props ⦄ {n} _ _) ⟩
    ∑[ k < p ] (∑[ j < n ] ((A i j *′ B j k) *′ C k l))   ≈⟨ sumₜ-cong {p} (λ k → sumₜ-cong {n} (λ j → from props (associative on *) _ _ _)) ⟩
    ∑[ k < p ] (∑[ j < n ] (A i j *′ (B j k *′ C k l)))   ≈⟨ ∑-comm ⦃ weaken props ⦄ p n _ ⟩
    ∑[ j < n ] (∑[ k < p ] (A i j *′ (B j k *′ C k l)))   ≈⟨ sumₜ-cong {n} (λ j → S.sym (sumDistribˡ ⦃ weaken props ⦄ {p} _ _)) ⟩
    ∑[ j < n ] (A i j *′ ∑[ k < p ] (B j k *′ C k l))     ≡⟨⟩
    (A ⊗ (B ⊗ C)) i l                                    ∎
  where open EqReasoning S.setoid

1-*-comm :
  ⦃ props : Has (1# is leftIdentity for * ∷ 1# is rightIdentity for * ∷ 0# is leftZero for * ∷ 0# is rightZero for * ∷ []) ⦄ →
  ∀ {n} (i j : Fin n) x → 1● i j *′ x ≈′ x *′ 1● i j
1-*-comm i j x with i Fin.≟ j
1-*-comm ⦃ props ⦄ i j x | yes p = S.trans (from props (1# is leftIdentity for *) _) (S.sym (from props (1# is rightIdentity for *) _))
1-*-comm ⦃ props ⦄ i j x | no ¬p = S.trans (from props (0# is leftZero for *) _) (S.sym (from props (0# is rightZero for *) _))

1-selectˡ :
  ⦃ props : Has (1# is leftIdentity for * ∷ 0# is leftZero for * ∷ []) ⦄ →
  ∀ {n} (i : Fin n) t j → (1● i j *′ lookup t j) ≈′ lookup (Table.select 0′ i t) j
1-selectˡ i t j with i Fin.≟ j | j Fin.≟ i
1-selectˡ ⦃ props ⦄ i t .i | yes ≡.refl | yes q = from props (1# is leftIdentity for *) _
1-selectˡ .j t j | yes ≡.refl | no ¬q = ⊥-elim (¬q ≡.refl)
1-selectˡ i t .i | no ¬p | yes ≡.refl = ⊥-elim (¬p ≡.refl)
1-selectˡ ⦃ props ⦄ i t j | no _ | no ¬p = from props (0# is leftZero for *) _

1-selectʳ :
  ⦃ props : Has (1# is rightIdentity for * ∷ 0# is rightZero for * ∷ []) ⦄ →
  ∀ {n} (i : Fin n) t j → (lookup t j *′ 1● j i) ≈′ lookup (Table.select 0′ i t) j
1-selectʳ i t j with i Fin.≟ j | j Fin.≟ i
1-selectʳ ⦃ props ⦄ i t .i | yes ≡.refl | yes q = from props (1# is rightIdentity for *) _
1-selectʳ .j t j | yes ≡.refl | no ¬q = ⊥-elim (¬q ≡.refl)
1-selectʳ i t .i | no ¬p | yes ≡.refl = ⊥-elim (¬p ≡.refl)
1-selectʳ ⦃ props ⦄ i t j | no _ | no ¬p = from props (0# is rightZero for *) _

1-sym : ∀ {n} (i j : Fin n) → 1● i j ≈′ 1● j i
1-sym i j with i Fin.≟ j | j Fin.≟ i
1-sym i j | yes _ | yes _ = S.refl
1-sym i j | no _  | no _ = S.refl
1-sym i .i | yes ≡.refl | no ¬q = ⊥-elim (¬q ≡.refl)
1-sym i .i | no ¬p | yes ≡.refl = ⊥-elim (¬p ≡.refl)

⊗-identityˡ :
  ⦃ props : Has ( 1# is leftIdentity for *
                ∷ 0# is leftZero for *
                ∷ 0# is leftIdentity for +
                ∷ 0# is rightIdentity for +
                ∷ associative on +
                ∷ commutative on +
                ∷ []) ⦄ →
  ∀ {m n} → ∀ (A : Matrix S m n) → (1● ⊗ A) ≈ A
⊗-identityˡ ⦃ props ⦄ {m} A i k =
  begin
    ∑[ j < m ] (1● i j *′ A j k)                        ≈⟨ sumₜ-cong (1-selectˡ ⦃ weaken props ⦄ i _) ⟩
    sumₜ (Table.select 0′ i (tabulate (λ x → A x k)))   ≈⟨ select-sum ⦃ weaken props ⦄ {m} _ ⟩
    A i k                                               ∎
  where open EqReasoning S.setoid

⊗-identityʳ :
  ⦃ props : Has ( 1# is rightIdentity for *
                ∷ 0# is rightZero for *
                ∷ 0# is leftIdentity for +
                ∷ 0# is rightIdentity for +
                ∷ associative on +
                ∷ commutative on +
                ∷ []) ⦄ →
  ∀ {m n} → ∀ (A : Matrix S m n) → (A ⊗ 1●) ≈ A
⊗-identityʳ ⦃ props ⦄ {n = n} A i k =
  begin
    ∑[ j < n ] (A i j *′ 1● j k)                ≈⟨ sumₜ-cong (1-selectʳ ⦃ weaken props ⦄ k _) ⟩
    sumₜ (Table.select 0′ k (tabulate (A i)))   ≈⟨ select-sum ⦃ weaken props ⦄ {n} _ ⟩
    A i k                                       ∎
  where open EqReasoning S.setoid

⊗-distributesOverˡ-⊕ :
  ⦃ props : Has (* ⟨ distributesOverˡ ⟩ₚ + ∷ 0# is leftIdentity for + ∷ associative on + ∷ commutative on + ∷ []) ⦄ →
  ∀ {m n o} (M : Matrix S m n) (A B : Matrix S n o) →
  M ⊗ (A ⊕ B) ≈ (M ⊗ A) ⊕ (M ⊗ B)
⊗-distributesOverˡ-⊕ ⦃ props ⦄ {n = n} M A B i k =
  begin
    ∑[ j < n ] (M i j *′ (A j k +′ B j k))                      ≈⟨ sumₜ-cong (λ j → from props (* ⟨ distributesOverˡ ⟩ₚ +) (M i j) (A j k) (B j k)) ⟩
    ∑[ j < n ] (M i j *′ A j k +′ M i j *′ B j k)               ≈⟨ S.sym (∑-+′-hom ⦃ weaken props ⦄ n (λ j → M i j *′ A j k) (λ j → M i j *′ B j k)) ⟩
    ∑[ j < n ] (M i j *′ A j k) +′ ∑[ j < n ] (M i j *′ B j k)  ∎
  where open EqReasoning S.setoid


text:
import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Syntax.MType as MType

module Parametric.Syntax.MTerm
    {Base : Type.Structure}
    (Const : Term.Structure Base)
  where

open Type.Structure Base
open MType.Structure Base
open Term.Structure Base Const

-- Our extension points are sets of primitives, indexed by the
-- types of their arguments and their return type.

-- We want different types of constants; some produce values, some produce
-- computations. In all cases, arguments are assumed to be values (though
-- individual primitives might require thunks).

ValConstStructure : Set₁
ValConstStructure = ValType → Set

CompConstStructure : Set₁
CompConstStructure = CompType → Set

CbnToCompConstStructure : CompConstStructure → Set
CbnToCompConstStructure CompConst = ∀ {τ} → Const τ → CompConst (cbnToCompType τ)

CbvToCompConstStructure : CompConstStructure → Set
CbvToCompConstStructure CompConst = ∀ {τ} → Const τ → CompConst (cbvToCompType τ)

module
  Structure
    (ValConst : ValConstStructure) (CompConst : CompConstStructure)
    (cbnToCompConst : CbnToCompConstStructure CompConst)
    (cbvToCompConst : CbvToCompConstStructure CompConst) where
  mutual
    -- Analogues of Terms
    Vals : ValContext → ValContext → Set
    Vals Γ = DependentList (Val Γ)

    Comps : ValContext → List CompType → Set
    Comps Γ = DependentList (Comp Γ)

    data Val Γ : (τ : ValType) → Set where
      vVar : ∀ {τ} (x : ValVar Γ τ) → Val Γ τ
      -- XXX Do we need thunks? The draft in the paper doesn't have them.
      -- However, they will start being useful if we deal with CBN source
      -- languages.
      vThunk : ∀ {τ} → Comp Γ τ → Val Γ (U τ)
      vConst : ∀ {τ} →
        (c : ValConst τ) →
        Val Γ τ

    data Comp Γ : (τ : CompType) → Set where
      cConst : ∀ {τ} →
        (c : CompConst τ) →
        Comp Γ τ

      cForce : ∀ {τ} → Val Γ (U τ) → Comp Γ τ
      cReturn : ∀ {τ} (v : Val Γ τ) → Comp Γ (F τ)
      {-
      -- Originally, M to x in N. But here we have no names!
      _into_ : ∀ {σ τ} →
        (e₁ : Comp Γ (F σ)) →
        (e₂ : Comp (σ •• Γ) τ) →
        Comp Γ τ
      -}
      -- The following constructor is the main difference between CBPV and this
      -- monadic calculus. This is better for the caching transformation.
      _into_ : ∀ {σ τ} →
        (e₁ : Comp Γ (F σ)) →
        (e₂ : Comp (σ •• Γ) (F τ)) →
        Comp Γ (F τ)
      cAbs : ∀ {σ τ} →
        (t : Comp (σ •• Γ) τ) →
        Comp Γ (σ ⇛ τ)
      cApp : ∀ {σ τ} →
        (s : Comp Γ (σ ⇛ τ)) →
        (t : Val Γ σ) →
        Comp Γ τ

  weaken-val : ∀ {Γ₁ Γ₂ τ} →
    (Γ₁≼Γ₂ : Γ₁ ≼≼ Γ₂) →
    Val Γ₁ τ →
    Val Γ₂ τ

  weaken-comp : ∀ {Γ₁ Γ₂ τ} →
    (Γ₁≼Γ₂ : Γ₁ ≼≼ Γ₂) →
    Comp Γ₁ τ →
    Comp Γ₂ τ

  weaken-val Γ₁≼Γ₂ (vVar x) = vVar (weaken-val-var Γ₁≼Γ₂ x)
  weaken-val Γ₁≼Γ₂ (vThunk x) = vThunk (weaken-comp Γ₁≼Γ₂ x)
  weaken-val Γ₁≼Γ₂ (vConst c) = vConst c
  weaken-comp Γ₁≼Γ₂ (cConst c) = cConst c
  weaken-comp Γ₁≼Γ₂ (cForce x) = cForce (weaken-val Γ₁≼Γ₂ x)
  weaken-comp Γ₁≼Γ₂ (cReturn v) = cReturn (weaken-val Γ₁≼Γ₂ v)
  weaken-comp Γ₁≼Γ₂ (_into_ {σ} c c₁) = (weaken-comp Γ₁≼Γ₂ c) into (weaken-comp (keep σ •• Γ₁≼Γ₂) c₁)
  weaken-comp Γ₁≼Γ₂ (cAbs {σ} c) = cAbs (weaken-comp (keep σ •• Γ₁≼Γ₂) c)
  weaken-comp Γ₁≼Γ₂ (cApp s t) = cApp (weaken-comp Γ₁≼Γ₂ s) (weaken-val Γ₁≼Γ₂ t)

  fromCBN : ∀ {Γ τ} (t : Term Γ τ) → Comp (fromCBNCtx Γ) (cbnToCompType τ)
  fromCBN (const c) = cConst (cbnToCompConst c)
  fromCBN (var x) = cForce (vVar (fromVar cbnToValType x))
  fromCBN (app s t) = cApp (fromCBN s) (vThunk (fromCBN t))
  fromCBN (abs t) = cAbs (fromCBN t)

  -- To satisfy termination checking, we'd need to inline fromCBV and weaken: fromCBV needs to produce a term in a bigger context.
  -- But let's ignore that.
  {-# TERMINATING #-}
  fromCBV : ∀ {Γ τ} (t : Term Γ τ) → Comp (fromCBVCtx Γ) (cbvToCompType τ)

  fromCBV (const c) = cConst (cbvToCompConst c)
  fromCBV (app s t) =
    (fromCBV s) into
      (fromCBV (weaken (drop _ • ≼-refl) t) into
        cApp (cForce (vVar (vThat vThis))) (vVar vThis))
  -- Values
  fromCBV (var x) = cReturn (vVar (fromVar cbvToValType x))
  fromCBV (abs t) = cReturn (vThunk (cAbs (fromCBV t)))

  -- This reflects the CBV conversion of values in TLCA '99, but we can't write
  -- this because it's partial on the Term type. Instead, we duplicate thunking
  -- at the call site.
  {-
  fromCBVToVal : ∀ {Γ τ} (t : Term Γ τ) → Val (fromCBVCtx Γ) (cbvToValType τ)
  fromCBVToVal (var x) = vVar (fromVar cbvToValType x)
  fromCBVToVal (abs t) = vThunk (cAbs (fromCBV t))

  fromCBVToVal (const c args) = {!!}
  fromCBVToVal (app t t₁) = {!!} -- Not a value
  -}

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

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

open import Algebra.Bundles

module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where

open Lattice L
open import Algebra.Structures _≈_
open import Algebra.Definitions _≈_
import Algebra.Properties.Semilattice as SemilatticeProperties
open import Relation.Binary
import Relation.Binary.Lattice as R
open import Relation.Binary.Reasoning.Setoid  setoid
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product using (_,_; swap)

------------------------------------------------------------------------
-- _∧_ is a semilattice

∧-idem : Idempotent _∧_
∧-idem x = begin
  x ∧ x            ≈⟨ ∧-congˡ (sym (∨-absorbs-∧ _ _)) ⟩
  x ∧ (x ∨ x ∧ x)  ≈⟨ ∧-absorbs-∨ _ _ ⟩
  x                ∎

∧-isMagma : IsMagma _∧_
∧-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = ∧-cong
  }

∧-isSemigroup : IsSemigroup _∧_
∧-isSemigroup = record
  { isMagma = ∧-isMagma
  ; assoc   = ∧-assoc
  }

∧-isBand : IsBand _∧_
∧-isBand = record
  { isSemigroup = ∧-isSemigroup
  ; idem        = ∧-idem
  }

∧-isSemilattice : IsSemilattice _∧_
∧-isSemilattice = record
  { isBand = ∧-isBand
  ; comm   = ∧-comm
  }

∧-semilattice : Semilattice l₁ l₂
∧-semilattice = record
  { isSemilattice = ∧-isSemilattice
  }

open SemilatticeProperties ∧-semilattice public
  using
  ( ∧-isOrderTheoreticMeetSemilattice
  ; ∧-isOrderTheoreticJoinSemilattice
  ; ∧-orderTheoreticMeetSemilattice
  ; ∧-orderTheoreticJoinSemilattice
  )

------------------------------------------------------------------------
-- _∨_ is a semilattice

∨-idem : Idempotent _∨_
∨-idem x = begin
  x ∨ x      ≈⟨ ∨-congˡ (sym (∧-idem _)) ⟩
  x ∨ x ∧ x  ≈⟨ ∨-absorbs-∧ _ _ ⟩
  x          ∎

∨-isMagma : IsMagma _∨_
∨-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = ∨-cong
  }

∨-isSemigroup : IsSemigroup _∨_
∨-isSemigroup = record
  { isMagma = ∨-isMagma
  ; assoc   = ∨-assoc
  }

∨-isBand : IsBand _∨_
∨-isBand = record
  { isSemigroup = ∨-isSemigroup
  ; idem        = ∨-idem
  }

∨-isSemilattice : IsSemilattice _∨_
∨-isSemilattice = record
  { isBand = ∨-isBand
  ; comm   = ∨-comm
  }

∨-semilattice : Semilattice l₁ l₂
∨-semilattice = record
  { isSemilattice = ∨-isSemilattice
  }

open SemilatticeProperties ∨-semilattice public
  using ()
  renaming
  ( ∧-isOrderTheoreticMeetSemilattice to ∨-isOrderTheoreticMeetSemilattice
  ; ∧-isOrderTheoreticJoinSemilattice to ∨-isOrderTheoreticJoinSemilattice
  ; ∧-orderTheoreticMeetSemilattice   to ∨-orderTheoreticMeetSemilattice
  ; ∧-orderTheoreticJoinSemilattice   to ∨-orderTheoreticJoinSemilattice
  )

------------------------------------------------------------------------
-- The dual construction is also a lattice.

∧-∨-isLattice : IsLattice _∧_ _∨_
∧-∨-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ∧-comm
  ; ∨-assoc       = ∧-assoc
  ; ∨-cong        = ∧-cong
  ; ∧-comm        = ∨-comm
  ; ∧-assoc       = ∨-assoc
  ; ∧-cong        = ∨-cong
  ; absorptive    = swap absorptive
  }

∧-∨-lattice : Lattice _ _
∧-∨-lattice = record
  { isLattice = ∧-∨-isLattice
  }

------------------------------------------------------------------------
-- Every algebraic lattice can be turned into an order-theoretic one.

open SemilatticeProperties ∧-semilattice public using (poset)
open Poset poset using (_≤_; isPartialOrder)

∨-∧-isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_
∨-∧-isOrderTheoreticLattice = record
  { isPartialOrder = isPartialOrder
  ; supremum       = supremum
  ; infimum        = infimum
  }
  where
  open R.MeetSemilattice ∧-orderTheoreticMeetSemilattice using (infimum)
  open R.JoinSemilattice ∨-orderTheoreticJoinSemilattice using (x≤x∨y; y≤x∨y; ∨-least)
    renaming (_≤_ to _≤′_)

  -- An alternative but equivalent interpretation of the order _≤_.

  sound : ∀ {x y} → x ≤′ y → x ≤ y
  sound {x} {y} y≈y∨x = sym $ begin
    x ∧ y        ≈⟨ ∧-congˡ y≈y∨x ⟩
    x ∧ (y ∨ x)  ≈⟨ ∧-congˡ (∨-comm y x) ⟩
    x ∧ (x ∨ y)  ≈⟨ ∧-absorbs-∨ x y ⟩
    x            ∎

  complete : ∀ {x y} → x ≤ y → x ≤′ y
  complete {x} {y} x≈x∧y = sym $ begin
    y ∨ x        ≈⟨ ∨-congˡ x≈x∧y ⟩
    y ∨ (x ∧ y)  ≈⟨ ∨-congˡ (∧-comm x y) ⟩
    y ∨ (y ∧ x)  ≈⟨ ∨-absorbs-∧ y x ⟩
    y            ∎

  supremum : R.Supremum _≤_ _∨_
  supremum x y =
     sound (x≤x∨y x y) ,
     sound (y≤x∨y x y) ,
     λ z x≤z y≤z → sound (∨-least (complete x≤z) (complete y≤z))

∨-∧-orderTheoreticLattice : R.Lattice _ _ _
∨-∧-orderTheoreticLattice = record
  { isLattice = ∨-∧-isOrderTheoreticLattice
  }

------------------------------------------------------------------------
-- One can replace the underlying equality with an equivalent one.

replace-equality : {_≈′_ : Rel Carrier l₂} →
                   (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → Lattice _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_       = _≈′_
  ; _∧_       = _∧_
  ; _∨_       = _∨_
  ; isLattice = record
    { isEquivalence = record
      { refl  = to ⟨$⟩ refl
      ; sym   = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
      ; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
      }
    ; ∨-comm     = λ x y → to ⟨$⟩ ∨-comm x y
    ; ∨-assoc    = λ x y z → to ⟨$⟩ ∨-assoc x y z
    ; ∨-cong     = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
    ; ∧-comm     = λ x y → to ⟨$⟩ ∧-comm x y
    ; ∧-assoc    = λ x y z → to ⟨$⟩ ∧-assoc x y z
    ; ∧-cong     = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
    ; absorptive = (λ x y → to ⟨$⟩ ∨-absorbs-∧ x y)
                 , (λ x y → to ⟨$⟩ ∧-absorbs-∨ x y)
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

∧-idempotent = ∧-idem
{-# WARNING_ON_USAGE ∧-idempotent
"Warning: ∧-idempotent was deprecated in v1.1.
Please use ∧-idem instead."
#-}
∨-idempotent = ∨-idem
{-# WARNING_ON_USAGE ∨-idempotent
"Warning: ∨-idempotent was deprecated in v1.1.
Please use ∨-idem instead."
#-}
isOrderTheoreticLattice = ∨-∧-isOrderTheoreticLattice
{-# WARNING_ON_USAGE isOrderTheoreticLattice
"Warning: isOrderTheoreticLattice was deprecated in v1.1.
Please use ∨-∧-isOrderTheoreticLattice instead."
#-}
orderTheoreticLattice = ∨-∧-orderTheoreticLattice
{-# WARNING_ON_USAGE orderTheoreticLattice
"Warning: orderTheoreticLattice was deprecated in v1.1.
Please use ∨-∧-orderTheoreticLattice instead."
#-}


text:
postulate
  A : Set

works : Set
works = let B : {X : Set} → Set
            B = let _ = Set in A
        in A

fails : Set
fails = let B : {X : Set} → Set
            B = A   -- Set !=< {X : Set} → Set
        in A

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.DiffInt where

open import Cubical.Data.Int.MoreInts.DiffInt.Base public
open import Cubical.Data.Int.MoreInts.DiffInt.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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 and uses single-pass merging algorithm.               --
----------------------------------------------------------------------

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

open import Basics
open import TwoPassMerge.RankProof
            using    ( makeT-lemma )
            renaming ( proof-1 to proof-1a; proof-2 to proof-2a )
open import SinglePassMerge.RankProof
            using    ( proof-1b; proof-2b )
open import Sized

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))

-- Here we combined previously conducted proofs of rank and priority
-- invariants in the same way we did it for two-pass merging algorithm
-- in TwoPassMerge.CombinedProofs. The most important thing here is
-- that we use order function both when comparing priorities and ranks
-- of new subtrees. This gives us evidence that required invariants
-- hold.
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
merge {_} .{_} {b} {suc l} {zero} h1 empty
          = subst (Heap b)
                  (sym (+0 (suc l)))
                  h1
merge .{_} .{_} .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {_} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {_}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  with order p1 p2
  | order l1-rank (r1-rank + suc (l2-rank + r2-rank))
  | order l2-rank (r2-rank + suc (l1-rank + r1-rank))
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
  | ge l1≥r1+h2
  | _
  = subst (Heap b)
          (proof-1a l1-rank r1-rank l2-rank r2-rank)
          (node p1 p1≥b l1≥r1+h2 l1 (merge 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)
  | le p1≤p2
  | le l1≤r1+h2
  | _
  = subst (Heap b)
          (proof-1b l1-rank r1-rank l2-rank r2-rank)
          (node p1 p1≥b l1≤r1+h2 (merge r1 (node p2 p1≤p2 l2≥r2 l2 r2)) l1)
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
  | _
  | ge l2≥r2+h1
  = subst (Heap b)
          (proof-2a l1-rank r1-rank l2-rank r2-rank)
          (node p2 p2≥b l2≥r2+h1 l2 (merge r2 (node p1 p1≥p2 l1≥r1 l1 r1)))
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
  | _
  | le l2≤r2+h1
  = subst (Heap b)
          (proof-2b l1-rank r1-rank l2-rank r2-rank)
          (node p2 p2≥b l2≤r2+h1 (merge r2 (node p1 p1≥p2 l1≥r1 l1 r1)) l2)

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:
module PiQ.Examples where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import PiQ.Syntax
open import PiQ.Opsem
open import PiQ.Eval
open import PiQ.Interp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-----------------------------------------------------------------------------
-- Ancilla Management

trace⋆ : ∀ {A B C} → (c : ⟦ C ⟧) → A ×ᵤ C ↔ B ×ᵤ C → A ↔ B
trace⋆ c f = uniti⋆r ⨾ (id↔ ⊗ ηₓ c) ⨾ assocl⋆ ⨾
             (f ⊗ id↔) ⨾
             assocr⋆ ⨾ (id↔ ⊗ εₓ _) ⨾ unite⋆r

-----------------------------------------------------------------------------
-- Higher-Order Combinators

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

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

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

curry- : {A B C : 𝕌} → (A +ᵤ B ↔ C) → (A ↔ - B +ᵤ C)
curry- c = uniti₊l ⨾ (η₊ ⊕ id↔) ⨾ swap₊ ⨾ assocl₊ ⨾ (c ⊕ id↔) ⨾ swap₊

hof/ : {A B : 𝕌} → (A ↔ B) → (v : ⟦ A ⟧) → (𝟙 ↔ 𝟙/ v ×ᵤ B)
hof/ c v = ηₓ v ⨾ (c ⊗ id↔) ⨾ swap⋆

comp/ : {A B C : 𝕌} {v : ⟦ A ⟧} → (w : ⟦ B ⟧) →
        (𝟙/ v ×ᵤ B) ×ᵤ (𝟙/ w ×ᵤ C) ↔ (𝟙/ v ×ᵤ C)
comp/ w = assocl⋆ ⨾ (assocr⋆ ⊗ id↔) ⨾ ((id↔ ⊗ εₓ w) ⊗ id↔) ⨾ (unite⋆r ⊗ id↔)

app/ : {A B : 𝕌} → (v : ⟦ A ⟧) → (𝟙/ v ×ᵤ B) ×ᵤ A ↔ B
app/ v = swap⋆ ⨾ assocl⋆ ⨾ (εₓ _ ⊗ id↔) ⨾ unite⋆l

curry/ : {A B C : 𝕌} → (A ×ᵤ B ↔ C) → (v : ⟦ B ⟧) → (A ↔ 𝟙/ v ×ᵤ C)
curry/ c v = uniti⋆l ⨾ (ηₓ v ⊗ id↔) ⨾ swap⋆ ⨾ assocl⋆ ⨾ (c ⊗ id↔) ⨾ swap⋆

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

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

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

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

inv/ : {A : 𝕌} {v : ⟦ A ⟧} → A ↔ (𝟙/_ {𝟙/ v} ↻)
inv/ = uniti⋆r ⨾ (id↔ ⊗ ηₓ _) ⨾ assocl⋆ ⨾ (εₓ _ ⊗ id↔) ⨾ unite⋆l

dist/ : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → 𝟙/ (a , b) ↔ 𝟙/ a ×ᵤ 𝟙/ b
dist/ {A} {B} {a} {b} =
  uniti⋆l ⨾ (ηₓ b ⊗ id↔) ⨾ uniti⋆l ⨾ (ηₓ a ⊗ id↔) ⨾ assocl⋆ ⨾
  ([A×B]×[C×D]=[A×C]×[B×D] ⊗ id↔) ⨾
  (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾ (id↔ ⊗ εₓ (a , b)) ⨾ unite⋆r

neg/ : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → (A ↔ B) → (𝟙/ a ↔ 𝟙/ b)
neg/ {A} {B} {a} {b} c =
  uniti⋆r ⨾ (id↔ ⊗ ηₓ _) ⨾
  (id↔ ⊗ ! c ⊗ id↔) ⨾ assocl⋆ ⨾
  ((swap⋆ ⨾ εₓ _) ⊗ id↔) ⨾ unite⋆l

dist×- : {A B : 𝕌} → (- A) ×ᵤ B ↔ - (A ×ᵤ B)
dist×- =
  uniti₊r ⨾ (id↔ ⊕ η₊) ⨾ assocl₊ ⨾
  ((factor ⨾ ((swap₊ ⨾ ε₊) ⊗ id↔) ⨾ absorbr) ⊕ id↔) ⨾
  unite₊l

neg× : {A B : 𝕌} → A ×ᵤ B ↔ (- A) ×ᵤ (- B)
neg× = inv- ⨾ neg- (! dist×- ⨾ swap⋆) ⨾ ! dist×- ⨾ swap⋆

fracDist : ∀ {A B} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → 𝟙/ a ×ᵤ 𝟙/ b ↔ 𝟙/ (a , b)
fracDist =
  uniti⋆l ⨾ ((ηₓ _ ⨾ swap⋆) ⊗ id↔) ⨾ assocr⋆ ⨾
  (id↔ ⊗ ([A×B]×[C×D]=[A×C]×[B×D] ⨾ (εₓ _ ⊗ εₓ _) ⨾ unite⋆l)) ⨾ unite⋆r

mulFrac : ∀ {A B C D} {b : ⟦ B ⟧} {d : ⟦ D ⟧}
        → (A ×ᵤ 𝟙/ b) ×ᵤ (C ×ᵤ 𝟙/ d) ↔ (A ×ᵤ C) ×ᵤ (𝟙/ (b , d))
mulFrac = [A×B]×[C×D]=[A×C]×[B×D] ⨾ (id↔ ⊗ fracDist)

addFracCom : ∀ {A B C} {v : ⟦ C ⟧}
        → (A ×ᵤ 𝟙/ v) +ᵤ (B ×ᵤ 𝟙/ v) ↔ (A +ᵤ B) ×ᵤ (𝟙/ v)
addFracCom = factor

addFrac : ∀ {A B C D} → (v : ⟦ C ⟧) → (w : ⟦ D ⟧)
        → (A ×ᵤ 𝟙/_ {C} v) +ᵤ (B ×ᵤ 𝟙/_ {D} w) ↔
         ((A ×ᵤ D) +ᵤ (C ×ᵤ B)) ×ᵤ (𝟙/_ {C ×ᵤ D} (v , w))
addFrac v w = ((uniti⋆r ⨾ (id↔ ⊗ ηₓ w)) ⊕ (uniti⋆l  ⨾ (ηₓ v ⊗ id↔))) ⨾
              [A×B]×[C×D]=[A×C]×[B×D] ⊕ [A×B]×[C×D]=[A×C]×[B×D] ⨾
              ((id↔ ⊗ fracDist) ⊕ (id↔ ⊗ fracDist)) ⨾ factor

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


text:
{-# OPTIONS -v treeless.opt:20 -v treeless.opt.unused:30 #-}

module _ where

open import Common.Prelude

-- First four arguments are unused.
maybe : ∀ {a b} {A : Set a} {B : Set b} → B → (A → B) → Maybe A → B
maybe z f nothing = z
maybe z f (just x) = f x

mapMaybe : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Maybe A → Maybe B
mapMaybe f x = maybe nothing (λ y → just (f y)) x

maybeToNat : Maybe Nat → Nat
maybeToNat m = maybe 0 (λ x → x) m

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr f z [] = z
foldr f z (x ∷ xs) = f x (foldr f z xs)

main : IO Unit
main = printNat (maybeToNat (just 42))
    ,, printNat (maybeToNat (mapMaybe (10 +_) (just 42)))
    ,, printNat (foldr _+_ 0 (1 ∷ 2 ∷ 3 ∷ 4 ∷ []))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Nat

data D : Nat → Set where
  c : (n : Nat) → D n

foo : (m : Nat) → D (suc m) → Nat
foo m (c (suc n)) = m + n


text:
open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Agda.Builtin.Equality

data ⊥ : Set where

infix 4 _≢_
_≢_ : {A : Set} → A → A → Set
x ≢ y = x ≡ y → ⊥

<?> = '\xFFFD'

infix 0 _∋_
_∋_ : (A : Set) → A → A
A ∋ x = x

_ = primNatToChar 0xD7FF ≢ <?> ∋ λ ()
_ = primNatToChar 0xD800 ≡ <?> ∋ refl
_ = primNatToChar 0xDFFF ≡ <?> ∋ refl
_ = primNatToChar 0xE000 ≢ <?> ∋ λ ()


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data Irr (A : Set) : Set where
  irr : .(x : A) → Irr A

data D {A : Set} : Irr A → Set where
  -- x is mistakenly marked as forced here!
  d : (x : A) → D (irr x)

unD : ∀ {A i} → D i → A
unD (d x) = x

dtrue=dfalse : d true ≡ d false
dtrue=dfalse = refl

_$≡_ : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
f $≡ refl = refl

true=false : true ≡ false
true=false = unD $≡ dtrue=dfalse

data ⊥ : Set where

loop : ⊥
loop with true=false
... | ()

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Numeral.Natural
open import Relator.Equals
open import Type.Properties.Decidable
open import Type

module Formalization.ClassicalPredicateLogic.Syntax.Substitution
  {ℓₚ ℓᵥ ℓₒ}
  (Prop : ℕ → Type{ℓₚ})
  (Var : Type{ℓᵥ}) ⦃ var-eq-dec : Decidable(2)(_≡_ {T = Var}) ⦄
  (Obj : ℕ → Type{ℓₒ})
  where

open import Data.Boolean
open import Data.ListSized
import      Data.ListSized.Functions as List
open import Formalization.ClassicalPredicateLogic.Syntax(Prop)(Var)(Obj)

private variable n : ℕ

substituteTerm : Var → Term → Term → Term
substituteTerm₊ : Var → Term → List(Term)(n) → List(Term)(n)
substituteTerm v t (var x)    = if(decide(2)(_≡_) v x) then t else (var x)
substituteTerm v t (func f x) = func f (substituteTerm₊ v t x)
substituteTerm₊ {0}    v t ∅        = ∅
substituteTerm₊ {𝐒(n)} v t (x ⊰ xs) = (substituteTerm v t x ⊰ substituteTerm₊ {n} v t xs)

substitute : Var → Term → Formula → Formula
substitute v t (f $ x)  = f $ List.map (substituteTerm v t) x
substitute v t ⊤        = ⊤
substitute v t ⊥        = ⊥
substitute v t (φ ∧ ψ)  = (substitute v t φ) ∧ (substitute v t ψ)
substitute v t (φ ∨ ψ)  = (substitute v t φ) ∨ (substitute v t ψ)
substitute v t (φ ⟶ ψ)  = (substitute v t φ) ⟶ (substitute v t ψ)
substitute v t (Ɐ(x) φ) = Ɐ(x) (if(decide(2)(_≡_) v x) then φ else (substitute v t φ))
substitute v t (∃(x) φ) = ∃(x) (if(decide(2)(_≡_) v x) then φ else (substitute v t φ))


text:
-- The (pre)category of (small) categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Instances.Categories where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Category.Precategory
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Functor.Properties
open import Cubical.Foundations.Prelude

module _ (ℓ ℓ' : Level) where
  open Precategory

  CatPrecategory : Precategory (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
  CatPrecategory .ob = Category ℓ ℓ'
  CatPrecategory .Hom[_,_] = Functor
  CatPrecategory .id = 𝟙⟨ _ ⟩
  CatPrecategory ._⋆_ G H = H ∘F G
  CatPrecategory .⋆IdL _ = F-lUnit
  CatPrecategory .⋆IdR _ = F-rUnit
  CatPrecategory .⋆Assoc _ _ _ = F-assoc

-- TODO: what is required for Functor C D to be a set?

max_stars_repo_name: FernandoLarrain/cubical


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

module Pi0Semiring where

import Level

open import PiU
open import PiLevel0

open import Algebra using (CommutativeSemiring)
open import Algebra.Structures
  using (IsSemigroup; IsCommutativeMonoid; IsCommutativeSemiring)

------------------------------------------------------------------------------
-- Commutative semiring structure of U

typesPlusIsSG : IsSemigroup _⟷_ PLUS
typesPlusIsSG = record {
  isEquivalence = record { refl = id⟷ ; sym = ! ; trans = _◎_ } ;
  assoc = λ t₁ t₂ t₃ → assocr₊ {t₁} {t₂} {t₃} ;
  ∙-cong = _⊕_
  }

typesTimesIsSG : IsSemigroup _⟷_ TIMES
typesTimesIsSG = record {
  isEquivalence = record { refl = id⟷ ; sym = ! ; trans = _◎_ } ;
  assoc = λ t₁ t₂ t₃ → assocr⋆ {t₁} {t₂} {t₃} ;
  ∙-cong = _⊗_
  }

typesPlusIsCM : IsCommutativeMonoid _⟷_ PLUS ZERO
typesPlusIsCM = record {
  isSemigroup = typesPlusIsSG ;
  identityˡ = λ t → unite₊l {t} ;
  comm = λ t₁ t₂ → swap₊ {t₁} {t₂}
  }

typesTimesIsCM : IsCommutativeMonoid _⟷_ TIMES ONE
typesTimesIsCM = record {
  isSemigroup = typesTimesIsSG ;
  identityˡ = λ t → unite⋆l {t} ;
  comm = λ t₁ t₂ → swap⋆ {t₁} {t₂}
  }

typesIsCSR : IsCommutativeSemiring _⟷_ PLUS TIMES ZERO ONE
typesIsCSR = record {
  +-isCommutativeMonoid = typesPlusIsCM ;
  *-isCommutativeMonoid = typesTimesIsCM ;
  distribʳ = λ t₁ t₂ t₃ → dist {t₂} {t₃} {t₁} ;
  zeroˡ = λ t → absorbr {t}
  }

typesCSR : CommutativeSemiring Level.zero Level.zero
typesCSR = record {
  Carrier = U ;
  _≈_ = _⟷_ ;
  _+_ = PLUS ;
  _*_ = TIMES ;
  0# = ZERO ;
  1# = ONE ;
  isCommutativeSemiring = typesIsCSR
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module NF.List {A : Set} where

open import NF
open import Data.List
open import Relation.Binary.PropositionalEquality

instance
  nf[] : NF {List A} []
  Sing.unpack (NF.!! nf[]) = []
  Sing.eq (NF.!! nf[]) = refl

  {-# INLINE nf[] #-}

  nf∷ : {x : A}{{nfx : NF x}}{t : List A}{{nft : NF t}} -> NF (x ∷ t)
  Sing.unpack (NF.!! (nf∷ {x} {t})) = nf x ∷ nf t
  Sing.eq (NF.!! (nf∷ {{nfx}} {{nft}})) rewrite nf≡ {{nfx}} | nf≡ {{nft}} = refl

  {-# INLINE nf∷ #-}

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
module Sessions.Semantics.Process where

open import Level
open import Size
open import Data.Nat
open import Data.Sum
open import Data.Product
open import Data.Unit
open import Data.Bool
open import Debug.Trace

open import Function
open import Relation.Unary hiding (Empty)
open import Relation.Unary.PredicateTransformer using (PT)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import Sessions.Syntax.Types
open import Sessions.Syntax.Values
open import Sessions.Syntax.Expr

open import Sessions.Semantics.Commands

open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Allstar
open import Relation.Ternary.Separation.Construct.Market
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Bigstar
open import Relation.Ternary.Separation.Monad.Free Cmd δ as Free hiding (step)
open import Relation.Ternary.Separation.Monad.State
open import Relation.Ternary.Separation.Monad.Error

open Monads using (Monad; str; typed-str)
open Monad {{...}}

data Exc : Set where
  outOfFuel : Exc
  delay     : Exc

open import Sessions.Semantics.Runtime delay
open import Sessions.Semantics.Communication delay

data Thread : Pred RCtx 0ℓ where
  forked :         ∀[ Comp unit ⇒ Thread ]
  main   : ∀ {a} → ∀[ Comp a ⇒ Thread ]

Pool : Pred RCtx 0ℓ
Pool = Bigstar Thread

St = Π₂ Pool ✴ Channels

open ExceptMonad {A = RCtx} Exc
open StateWithErr {C = RCtx} Exc

onPool : ∀ {P} → ∀[ (Pool ─✴ Except Exc (P ✴ Pool)) ⇒ State? St P ]
app (onPool f) (lift (snd pool ×⟨ σ , σ₁ ⟩ chs) k) (offerᵣ σ₂) with resplit σ₂ σ₁ k
... | _ , _ , τ₁ , τ₂ , τ₃ =
  case app f pool τ₁ of λ where
    (error e) → partial (inj₁ e)
    (✓ (p ×⟨ σ₃ ⟩ p')) →
      let _ , _ , τ₄ , τ₅ , τ₆ = resplit σ₃ τ₂ τ₃
      in return (inj p ×⟨ offerᵣ τ₄ ⟩ lift (snd p' ×⟨ σ , τ₅ ⟩ chs) τ₆)

onChannels : ∀ {P} → ∀[ State? Channels P ⇒ State? St P ]
app (onChannels f) μ (offerᵣ σ₃) with ○≺●ᵣ μ
... | inj pool ×⟨ offerᵣ σ₄ ⟩ chs with ⊎-assoc σ₃ (⊎-comm σ₄)
... | _ , τ₁ , τ₂ = do
  px ×⟨ σ₄ ⟩ ●chs ×⟨ σ₅ ⟩ inj pool ←
    mapM (app f chs (offerᵣ τ₁) &⟨ J Pool ∥ offerₗ τ₂ ⟩ inj pool) ✴-assocᵣ
  return (px ×⟨ σ₄ ⟩ app (○≺●ₗ pool) ●chs (⊎-comm σ₅))

enqueue : ∀[ Thread ⇒ State? St Emp ]
enqueue thr =
  onPool (wand λ pool σ → return (empty ×⟨ ⊎-idˡ ⟩ (app (append thr) pool σ)))

-- Smart reschedule of a thread:
-- Escalates out-of-fuel erros in threads, and discards terminated workers.
reschedule : ∀[ Thread ⇒ State? St Emp ]

reschedule (forked (partial (pure (inj₁ _))))  = raise outOfFuel
reschedule (forked (partial (pure (inj₂ tt)))) = return empty
reschedule thr@(forked (partial (impure _)))   = enqueue thr

reschedule (main (partial (pure (inj₁ _))))     = raise outOfFuel
reschedule thr@(main (partial (pure (inj₂ _)))) = enqueue thr
reschedule thr@(main (partial (impure _)))      = enqueue thr

{- Select the next thread that is not done -}
dequeue : ε[ State? St (Emp ∪ Thread) ]
dequeue =
  onPool (wandit (λ pool →
    case (find isImpure pool) of λ where
      (error e)              → return (inj₁ empty ×⟨ ⊎-idˡ ⟩ pool)
      (✓ (thr ×⟨ σ ⟩ pool')) → return (inj₂ thr ×⟨ σ ⟩ pool')))
  where
    isImpure : ∀ {Φ} → Thread Φ → Bool
    isImpure (main   (partial (pure _)))   = false
    isImpure (main   (partial (impure _))) = true
    isImpure (forked (partial (pure _)))   = false
    isImpure (forked (partial (impure _))) = true

module _ where

  handle : ∀ {Φ} → (c : Cmd Φ) → State? St (δ c) Φ
  handle (fork thr)           = trace "handle:fork"   $ enqueue (forked thr)
  handle (mkchan α)           = trace "handle:mkchan" $ onChannels newChan
  handle (send (ch ×⟨ σ ⟩ v)) = trace "handle:send"   $ onChannels (app (send! ch) v σ)
  handle (receive ch)         = trace "handle:recv"   $ onChannels (receive? ch)
  handle (close ch)           = trace "handle:close"  $ onChannels (closeChan ch)

  step : ∀[ Thread ⇒ State? St Thread ]
  step thr@(main (partial c))   = do
    c' ← Free.step handle c
    return (main (partial c'))
  step (forked (partial c)) = do
    c' ← Free.step handle c
    return (forked (partial c'))

  -- try the first computation; if it fails with a 'delay' exception,
  -- then queue t
  _orDelay_ : ∀[ State? St Emp ⇒ Thread ⇒ State? St Emp ]
  c orDelay t = do
    c orElse λ where
      delay     → enqueue t
      outOfFuel → raise outOfFuel

  -- Run a pool of threads in round-robing fashion
  -- until all have terminated, or fuel runs out
  run : ℕ → ε[ State? St Emp ]
  run zero    = raise outOfFuel
  run (suc n) = do
    inj₂ thr ← dequeue
      -- if we cannot dequeue a thunked thread, we're done
      where (inj₁ e) → return e

    -- otherwise we take a step
    empty ← trace "run:step" (do thr' ← step thr; enqueue thr') orDelay thr

    -- rinse and repeat
    run n

  start : ℕ → Thread ε → ∃ λ Φ → Except Exc (● St) Φ
  start n thr = -, do
    let μ = lift (snd [ thr ] ×⟨ ⊎-idʳ ⟩ nil) ⊎-idʳ
    inj empty ×⟨ σ ⟩ μ ← app (run n) μ (offerᵣ ⊎-idˡ)
    case ⊎-id⁻ˡ σ of λ where
      refl → return μ

    where open ExceptMonad {A = Market RCtx} Exc


text:
module nat-log where

open import bool
open import eq
open import nat
open import nat-thms
open import nat-division
open import product

data log-result (x : ℕ)(b : ℕ) : Set where
  pos-power : (e : ℕ) → (s : ℕ) → b pow e + s ≡ x → log-result x b
  no-power : x < b ≡ tt → log-result x b

-- as a first version, we do not try to prove termination of this function
{-# NON_TERMINATING #-}
log : (x : ℕ) → (b : ℕ) → x =ℕ 0 ≡ ff → b =ℕ 0 ≡ ff → log-result x b
log x b p1 p2 with x ÷ b ! p2
log x b p1 p2 | 0 , r , u1 , u2 rewrite u1 = no-power u2
log x b p1 p2 | (suc q) , r , u1 , u2 with log (suc q) b refl p2
log x b p1 p2 | (suc q) , r , u1 , u2 | no-power u rewrite sym u1 =
  pos-power 1 (b * q + r) lem
  where lem : b * 1 + (b * q + r) ≡ b + q * b + r
        lem rewrite *1{b} | *comm b q = +assoc b (q * b) r
log x b p1 p2 | (suc q) , r , u1 , u2 | pos-power e s u rewrite sym u1 =
  pos-power (suc e) (b * s + r) lem
  where lem : b * b pow e + (b * s + r) ≡ b + q * b + r
        lem rewrite +assoc (b * b pow e) (b * s) r | sym (*distribl b (b pow e) s) | *comm b (b pow e + s) =
          sym (cong (λ i → i * b + r) (sym u))

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module Data.Vec where

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

infixl 90 _#_
infixr 50 _::_
infixl 45 _!_ _[!]_

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

-- Indexing
_!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A
x :: xs ! fzero  = x
x :: xs ! fsuc i = xs ! i

-- Insertion
insert : {n : Nat}{A : Set} -> Fin (suc n) -> A -> Vec A n -> Vec A (suc n)
insert fzero	y  xs	    = y :: xs
insert (fsuc i) y (x :: xs) = x :: insert i y xs

-- Index view
data IndexView {A : Set} : {n : Nat}(i : Fin n) -> Vec A n -> Set where
   ixV : {n : Nat}{i : Fin (suc n)}(x : A)(xs : Vec A n) ->
	 IndexView i (insert i x xs)

_[!]_ : {A : Set}{n : Nat}(xs : Vec A n)(i : Fin n) -> IndexView i xs
x :: xs	[!] fzero  = ixV x xs
x :: xs [!] fsuc i = aux xs i (xs [!] i)
  where
    aux : {n : Nat}(xs : Vec _ n)(i : Fin n) ->
	  IndexView i xs -> IndexView (fsuc i) (x :: xs)
    aux .(insert i y xs) i (ixV y xs) = ixV y (x :: xs)

-- Build a vector from an indexing function (inverse of _!_)
build : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n
build {zero } f = []
build {suc _} f = f fzero :: build (f ∘ fsuc)

-- Constant vectors
vec : {n : Nat}{A : Set} -> A -> Vec A n
vec {zero } _ = []
vec {suc m} x = x :: vec x

-- Vector application
_#_ : {n : Nat}{A B : Set} -> Vec (A -> B) n -> Vec A n -> Vec B n
[]	  # []	      = []
(f :: fs) # (x :: xs) = f x :: fs # xs

-- Vectors of length n form an applicative structure
ApplicativeVec : {n : Nat} -> Applicative (\A -> Vec A n)
ApplicativeVec {n} = applicative (vec {n}) (_#_ {n})

-- Map
map : {n : Nat}{A B : Set} -> (A -> B) -> Vec A n -> Vec B n
map f xs = vec f # xs

-- Zip
zip : {n : Nat}{A B C : Set} -> (A -> B -> C) -> Vec A n -> Vec B n -> Vec C n
zip f xs ys = vec f # xs # ys

module Elem where

  infix 40 _∈_ _∉_

  data _∈_ {A : Set}(x : A) : {n : Nat}(xs : Vec A n) -> Set where
    hd : {n : Nat}	 {xs : Vec A n}		  -> x ∈ x :: xs
    tl : {n : Nat}{y : A}{xs : Vec A n} -> x ∈ xs -> x ∈ y :: xs

  data _∉_ {A : Set}(x : A) : {n : Nat}(xs : Vec A n) -> Set where
    nl	: x ∉ []
    cns : {n : Nat}{y : A}{xs : Vec A n} -> x ≢ y -> x ∉ xs -> x ∉ y :: xs

  ∉=¬∈ : {A : Set}{x : A}{n : Nat}{xs : Vec A n} -> x ∉ xs -> ¬ (x ∈ xs)
  ∉=¬∈ nl	       ()
  ∉=¬∈ {A} (cns x≠x _) hd    = elim-False (x≠x refl)
  ∉=¬∈ {A} (cns _ ne) (tl e) = ∉=¬∈ ne e

  ∈=¬∉ : {A : Set}{x : A}{n : Nat}{xs : Vec A n} -> x ∈ xs -> ¬ (x ∉ xs)
  ∈=¬∉ e ne = ∉=¬∈ ne e

  find : {A : Set}{n : Nat} -> ((x y : A) -> x ≡ y \/ x ≢ y) ->
	 (x : A)(xs : Vec A n) -> x ∈ xs \/ x ∉ xs
  find _  _ []	      = \/-IR nl
  find eq y (x :: xs) = aux x y (eq y x) (find eq y xs) where
    aux : forall x y -> y ≡ x \/ y ≢ x -> y ∈ xs \/ y ∉ xs -> y ∈ x :: xs \/ y ∉ x :: xs
    aux x .x (\/-IL refl)  _	       = \/-IL hd
    aux x y  (\/-IR y≠x)  (\/-IR y∉xs) = \/-IR (cns y≠x y∉xs)
    aux x y  (\/-IR _)	  (\/-IL y∈xs) = \/-IL (tl y∈xs)

  delete : {A : Set}{n : Nat}(x : A)(xs : Vec A (suc n)) -> x ∈ xs -> Vec A n
  delete	   .x (x :: xs)  hd    = xs
  delete {A}{zero } _  ._	(tl ())
  delete {A}{suc _} y (x :: xs) (tl p) = x :: delete y xs p

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of products
------------------------------------------------------------------------

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

module Data.Product.Properties where

open import Data.Product
open import Function using (_∘_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- Equality

module _ {a b} {A : Set a} {B : A → Set b} where

  ,-injectiveˡ : ∀ {a c} {b : B a} {d : B c} → (a , b) ≡ (c , d) → a ≡ c
  ,-injectiveˡ refl = refl

  -- See also Data.Product.Properties.WithK.,-injectiveʳ.


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

open import Common.Prelude
open import Common.Path

{-# BUILTIN REWRITE _≡_ #-}

postulate is-refl : ∀ {A : Set} {x : A} → (x ≡ x) → Bool
postulate is-refl-true : ∀ {A}{x} → is-refl {A} {x} refl ≡ true

{-# REWRITE is-refl-true #-}

test₁ : ∀ {x} → is-refl {Nat} {x} refl ≡ true
test₁ = refl

test₂ : is-refl {Nat} (λ _ → 42) ≡ true
test₂ = refl

postulate
    Cl : Set

module M (A B C : Set)(f : C -> A)(g : C -> B) where
  data PO : Set where
    inl : A → PO
    inr : B → PO
    push : (c : C) → inl (f c) ≡ inr (g c)

  -- elimination under clocks
  module E (D : (Cl → PO) → Set)
           (l : (x : Cl → A) → D (\ k → inl (x k)))
           (r : (x : Cl → B) → D (\ k → inr (x k)))
           (p : (x : Cl → C) → PathP (\ i → D (\ k → push (x k) i)) (l \ k → (f (x k))) (r \ k → (g (x k))))
     where

    postulate
      elim : (h : Cl → PO) → D h
      beta1 : (x : Cl → A) → elim (\ k → inl (x k)) ≡ l x
      beta2 : (x : Cl → B) → elim (\ k → inr (x k)) ≡ r x

    {-# REWRITE beta1 beta2 #-}

    _ : {x : Cl → A} → elim (\ k → inl (x k)) ≡ l x
    _ = refl
    _ : {x : Cl → B} → elim (\ k → inr (x k)) ≡ r x
    _ = refl

    postulate
      beta3 : (x : Cl → C)(i : I) → elim (\ k → push (x k) i) ≡ p x i

    {-# REWRITE beta3 #-}

    _ : {x : Cl → C}{i : I} → elim (\ k → push (x k) i) ≡ p x i
    _ = refl

-- Testing outside the module too

open M
open E

variable
  A B C : Set
  f : C → A
  g : C → B

_ : {x : Cl → A} →
    elim A B C f g (\ h → (k : Cl) → h k ≡ h k) (\ x k → refl) (\ _ _ → refl)
      (\ c i k → refl) (\ k → inl (x k)) ≡ \ k → refl
_ = refl

_ : {c : Cl → C}{i : I} →
    elim A B C f g (\ h → (k : Cl) → h k ≡ h k) (\ x k → refl) (\ _ _ → refl)
      (\ c i k → refl) (\ k → push (c k) i) ≡ \ k → refl
_ = refl


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

open import LogicalFormulae
open import Groups.Definition
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations

module Fields.FieldOfFractions.Addition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open import Fields.FieldOfFractions.Setoid I

fieldOfFractionsPlus : fieldOfFractionsSet → fieldOfFractionsSet → fieldOfFractionsSet
fieldOfFractionsSet.num (fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 })) = (a * d) + (b * c)
fieldOfFractionsSet.denom (fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 })) = b * d
fieldOfFractionsSet.denomNonzero (fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 })) = λ pr → exFalso (d!=0 (IntegralDomain.intDom I pr b!=0))

--record { num = ((a * d) + (b * c)) ; denom = b * d ; denomNonzero = λ pr → exFalso (d!=0 (IntegralDomain.intDom I pr b!=0)) }

plusWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsPlus a b) (fieldOfFractionsPlus c d)
plusWellDefined {record { num = a ; denom = b ; denomNonzero = b!=0 }} {record { num = c ; denom = d ; denomNonzero = d!=0 }} {record { num = e ; denom = f ; denomNonzero = f!=0 }} {record { num = g ; denom = h ; denomNonzero = h!=0 }} af=be ch=dg = need
  where
    open Setoid S
    open Ring R
    open Equivalence eq
    have1 : (c * h) ∼ (d * g)
    have1 = ch=dg
    have2 : (a * f) ∼ (b * e)
    have2 = af=be
    need : (((a * d) + (b * c)) * (f * h)) ∼ ((b * d) * (((e * h) + (f * g))))
    need = transitive (transitive (Ring.*Commutative R) (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) (transitive *Associative (transitive (*WellDefined (*Commutative) reflexive) (transitive (*WellDefined *Associative reflexive) (transitive (*WellDefined (*WellDefined have2 reflexive) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) reflexive) (symmetric *Associative))))))))) (transitive *Commutative (transitive (transitive (symmetric *Associative) (*WellDefined reflexive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (transitive (*WellDefined have1 reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))))))) *Associative))))) (symmetric (Ring.*DistributesOver+ R))


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

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

module Groups.Actions.Definition where

record GroupAction {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·_ : A → A → A} {B : Set n} (G : Group S _·_) (X : Setoid {n} {p} B) : Set (m ⊔ n ⊔ o ⊔ p) where
  open Group G
  open Setoid S renaming (_∼_ to _∼G_)
  open Setoid X renaming (_∼_ to _∼X_)
  field
    action : A → B → B
    actionWellDefined1 : {g h : A} → {x : B} → (g ∼G h) → action g x ∼X action h x
    actionWellDefined2 : {g : A} → {x y : B} → (x ∼X y) → action g x ∼X action g y
    identityAction : {x : B} → action 0G x ∼X x
    associativeAction : {x : B} → {g h : A} → action (g · h) x ∼X action g (action h x)


text:
-- A minor variant of code reported by Andreas Abel.

-- Andreas, 2011-10-04
--
-- Agda's coinduction is incompatible with initial algebras
--
-- Sized types are needed to formulate initial algebras in general:
--
{-# OPTIONS --sized-types #-}
--
-- We need to skip the positivity check since we cannot communicate
-- to Agda that we only want strictly positive F's in the definition of Mu
--
{-# OPTIONS --no-positivity-check #-}
--
module _ where

open import Agda.Builtin.Coinduction renaming (∞ to co)
open import Agda.Builtin.Size

-- initial algebras

data Mu (F : Set → Set) : Size → Set where
  inn : ∀ {i} → F (Mu F i) → Mu F (↑ i)

iter : ∀ {F : Set → Set}
         (map : ∀ {A B} → (A → B) → F A → F B)
         {A} → (F A → A) → ∀ {i} → Mu F i → A
iter map s (inn t) = s (map (iter map s) t)

-- the co functor (aka Lift functor)

F : Set → Set
F A = co A

map : ∀ {A B : Set} → (A → B) → co A → co B
map f a = ♯ f (♭ a)

-- the least fixed-point of co is inhabited

bla : Mu F ∞
bla = inn (♯ bla)

-- and goal!

data ⊥ : Set where

false : ⊥
false = iter map ♭ bla

-- note that co is indeed strictly positive, as the following
-- direct definition of Mu F ∞ is accepted

data Bla : Set where
  c : co Bla → Bla

{- -- if we inline ♭ map into iter, the termination checker detects the cheat
iter' : Bla → ⊥
iter' (c t) = ♭ (♯ iter' (♭ t))
-- iter' (c t) = ♭ (map iter' t)
-}

-- Again, I want to emphasize that the problem is not with sized types.
-- I have only used sized types to communicate to Agda that initial algebras
-- (F, iter) are ok.  Once we have initial algebras, we can form the
-- initial algebra of the co functor and abuse the guardedness checker
-- to construct an inhabitant in this empty initial algebra.
--
-- Agda's coinduction mechanism confuses constructor and coconstructors.
-- Convenient, but, as you have seen...

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
module Prelude where

  id : {a : Set} -> a -> a
  id x = x

  infixr 0 _$_

  _$_ : {a b : Set} -> (a -> b) -> a -> b
  f $ x = f x

  data Bool : Set where
    True  : Bool
    False : Bool

  _&&_ : Bool -> Bool -> Bool
  True  && b = b
  False && _ = False

  data Pair (a b : Set) : Set where
    pair : a -> b -> Pair a b

  fst : {a b : Set} -> Pair a b -> a
  fst (pair x y) = x

  snd : {a b : Set} -> Pair a b -> b
  snd (pair x y) = y

  data Either (a b : Set) : Set where
    left  : a -> Either a b
    right : b -> Either a b

  data Maybe (a : Set) : Set where
    Nothing : Maybe a
    Just    : a -> Maybe a

  data Unit : Set where
    unit : Unit

  data Absurd : Set where

  absurdElim : {whatever : Set} -> Absurd -> whatever
  absurdElim ()

--   data Pi {a : Set} (f : a -> Set) : Set where
--     pi : ((x : a) -> f x) -> Pi f
--
--   apply : {a : Set} -> {f : a -> Set} -> Pi f -> (x : a) -> f x
--   apply (pi f) x = f x

  T : Bool -> Set
  T True  = Unit
  T False = Absurd

  andT : {x y : Bool} -> T x -> T y -> T (x && y)
  andT {True}  {True}  _  _ = unit
  andT {True}  {False} _  ()
  andT {False} {_}     () _

  T' : {a : Set} -> (a -> a -> Bool) -> (a -> a -> Set)
  T' f x y = T (f x y)

  data Not (a : Set) : Set where
    not : (a -> Absurd) -> Not a

  -- Not : Set -> Set
  -- Not a = a -> Absurd

  contrapositive : {a b : Set} -> (a -> b) -> Not b -> Not a
  contrapositive p (not nb) = not (\a -> nb (p a))

  private
    notDistribOut' : {a b : Set} -> Not a -> Not b -> Either a b -> Absurd
    notDistribOut' (not na) _        (left a)  = na a
    notDistribOut' _        (not nb) (right b) = nb b

  notDistribOut : {a b : Set} -> Not a -> Not b -> Not (Either a b)
  notDistribOut na nb = not (notDistribOut' na nb)

  notDistribIn : {a b : Set} -> Not (Either a b) -> Pair (Not a) (Not b)
  notDistribIn (not nab) = pair (not (\a -> nab (left a)))
                                (not (\b -> nab (right b)))

  data _<->_ (a b : Set) : Set where
    iff : (a -> b) -> (b -> a) -> a <-> b

  iffLeft : {a b : Set} -> (a <-> b) -> (a -> b)
  iffLeft (iff l _) = l

  iffRight : {a b : Set} -> (a <-> b) -> (b -> a)
  iffRight (iff _ r) = r

  Dec : (A : Set) -> Set
  Dec A = Either A (Not A)


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

module Categories.Functor.Construction.PathsOf where

-- "Free Category on a Quiver" Construction, i.e. the category of paths of the quiver.

-- Note the use of Categories.Morphism.HeterogeneousIdentity as well as
-- Relation.Binary.PropositionalEquality.Subst.Properties which are needed
-- for F-resp-≈.
open import Level
open import Function using (_$_)
open import Relation.Binary.PropositionalEquality using (refl; sym)
open import Relation.Binary.PropositionalEquality.Subst.Properties using (module TransportStar)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
open import Data.Quiver
open import Data.Quiver.Morphism
open import Data.Quiver.Paths using (module Paths)

open import Categories.Category
import Categories.Category.Construction.PathCategory as PC
open import Categories.Category.Instance.Quivers
open import Categories.Category.Instance.StrictCats
open import Categories.Functor using (Functor)
open import Categories.Functor.Equivalence using (_≡F_)
import Categories.Morphism.HeterogeneousIdentity as HId
import Categories.Morphism.Reasoning as MR

private
  variable
    o o′ ℓ ℓ′ e e′ : Level
    G₁ G₂ : Quiver o ℓ e

⇒toPathF : {G₁ G₂ : Quiver o ℓ e} → Morphism G₁ G₂ → Functor (PC.PathCategory G₁) (PC.PathCategory G₂)
⇒toPathF {G₁ = G₁} {G₂} G⇒ = record
    { F₀ = F₀ G⇒
    ; F₁ = qmap G⇒
    ; identity = Paths.refl G₂
    ; homomorphism = λ {_} {_} {_} {f} {g} → Paths.≡⇒≈* G₂ $ gmap-◅◅ (F₀ G⇒) (F₁ G⇒) f g
    ; F-resp-≈ = λ { {f = f} → map-resp G⇒ f}
    }
    where open Morphism

⇒toPathF-resp-≃ : {f g : Morphism G₁ G₂} → f ≃ g → ⇒toPathF f ≡F ⇒toPathF g
⇒toPathF-resp-≃ {G₂ = G} {f} {g} f≈g = record
  { eq₀ = λ _ → F₀≡
  ; eq₁ = λ h →
    let open Category.HomReasoning (PC.PathCategory G)
        open HId      (PC.PathCategory G)
        open TransportStar (Quiver._⇒_ G)
    in begin
      qmap f h ◅◅ (hid F₀≡) ≈˘⟨ hid-subst-cod (qmap f h) F₀≡ ⟩
      qmap f h ▸* F₀≡       ≈⟨ map-F₁≡ f≈g h ⟩
      F₀≡ ◂* qmap g h       ≈⟨ hid-subst-dom F₀≡ (qmap g h) ⟩
      hid F₀≡ ◅◅ qmap g h   ∎
  }
  where
    open _≃_ f≈g

PathsOf : Functor (Quivers o ℓ e) (StrictCats o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e))
PathsOf = record
  { F₀ = PC.PathCategory
  ; F₁ = ⇒toPathF
  ; identity = λ {G} → record
    { eq₀ = λ _ → refl
    ; eq₁ = λ f → toSquare (PC.PathCategory G) (Paths.≡⇒≈* G $ gmap-id f)
    }
  ; homomorphism = λ {_} {_} {G} {f} {g} → record
    { eq₀ = λ _ → refl
    ; eq₁ = λ h → toSquare (PC.PathCategory G) (Paths.≡⇒≈* G (sym $ gmap-∘ (F₀ g) (F₁ g) (F₀ f) (F₁ f) h) )
    }
  ; F-resp-≈ = ⇒toPathF-resp-≃
  }
  where
  open Morphism using (F₀; F₁)
  open MR using (toSquare)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Data.Binary.Conversion.Strict where

open import Data.Binary.Definition
open import Data.Binary.Increment.Strict
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Data.Nat using (ℕ; suc; zero)
open import Data.Nat.Fold
open import Strict
open import Data.Nat.DivMod
open import Data.Bool

⟦_⇑⟧′ : ℕ → 𝔹
⟦_⇑⟧′ = foldl-ℕ inc′ 0ᵇ

⟦_⇓⟧′ : 𝔹 → ℕ
⟦ 0ᵇ ⇓⟧′ = zero
⟦ 1ᵇ xs ⇓⟧′ = let! xs′ =! ⟦ xs ⇓⟧′ in! 1 ℕ.+ xs′ ℕ.* 2
⟦ 2ᵇ xs ⇓⟧′ = let! xs′ =! ⟦ xs ⇓⟧′ in! 2 ℕ.+ xs′ ℕ.* 2

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Module for BCCs, CCCs and BCCCs
module CategoryTheory.BCCCs where

open import CategoryTheory.Categories
open import CategoryTheory.BCCCs.Cartesian public
open import CategoryTheory.BCCCs.Cocartesian public
open import CategoryTheory.BCCCs.Closed public

-- Bicartesian categories
record Bicartesian {n} (ℂ : Category n) : Set (lsuc n) where
    field
        cart   : Cartesian ℂ
        cocart : Cocartesian ℂ

-- Cartesian closed categories
record CartesianClosed {n} (ℂ : Category n) : Set (lsuc n) where
    field
        cart   : Cartesian ℂ
        closed : Closed cart

-- Bicartesian closed categories
record BicartesianClosed {n} (ℂ : Category n) : Set (lsuc n) where
    field
        cart   : Cartesian ℂ
        cocart : Cocartesian ℂ
        closed : Closed cart
    open Cartesian cart public
    open Cocartesian cocart public
    open Closed closed public

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:
{-
  Copyright 2019 Lisandra Silva

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

open import Prelude
open import Data.Bool renaming (_≟_ to _B≟_)
open import Data.Fin renaming (_≟_ to _F≟_)
open import Agda.Builtin.Sigma
open import Relation.Nullary.Negation using (contradiction ; contraposition)

open import StateMachineModel

{-
             PROCESS 0                   ||             PROCESS 1

    repeat                               ||    repeat
      s₀: thinking₀ = false;             ||      r₀: thinking₁ = false;
      s₁: turn = 1;                      ||      r₁: turn = 0;
      s₂: await thinking₁ ∨ turn ≡ 0;    ||      r₂: await thinking₀ ∨ turn ≡ 1;
            “critical section”;          ||            “critical section”;
      s₃: thinking₀ = true;              ||      r₃: thinking₁ = true;
    forever                              ||    forever

-}
module Examples.Peterson where

  {- Because of the atomicity assumptions, we can view a concurrent program as a
     state transition system. Simply associate with each process a control
     variable that indicates the atomic statement to be executed next by the
     process.
     The state of the program is defined by the values of the data variables and
     control variables.
  -}
  record State : Set where
    field
      -- Data variables : updated in assignemnt statements
      thinking₀ thinking₁ : Bool
      turn : Fin 2
      -- Control varibales : updated acording to the control flow of the program
      control₀ control₁ : Fin 4
  open State

  -- Events : corresponding to the atomic statements
  data MyEvent : Set where
    es₀ es₁ es₂₁ es₂₂ es₃ er₀ er₁ er₂₁ er₂₂ er₃ : MyEvent

  {- Enabled conditions : predicate on the state variables.
     In any state, an atomic statement can be executed if and only if it is
     pointed to by a control variable and is enabled.
  -}
  MyEnabled : MyEvent → State → Set
  MyEnabled es₀  st = control₀ st ≡ 0F
  MyEnabled es₁  st = control₀ st ≡ 1F
  MyEnabled es₂₁ st = control₀ st ≡ 2F × thinking₁ st ≡ true
  MyEnabled es₂₂ st = control₀ st ≡ 2F × turn st ≡ 0F
  MyEnabled es₃  st = control₀ st ≡ 3F
  MyEnabled er₀  st = control₁ st ≡ 0F
  MyEnabled er₁  st = control₁ st ≡ 1F
  MyEnabled er₂₁ st = control₁ st ≡ 2F × thinking₀ st ≡ true
  MyEnabled er₂₂ st = control₁ st ≡ 2F × turn st ≡ 1F
  MyEnabled er₃  st = control₁ st ≡ 3F

  {- Actions : executing the statement results in a new state.
     Thus each statement execution corresponds to a state transition.
  -}
  MyAction : ∀ {preState} {event} → MyEnabled event preState → State
  -- Process 1
  MyAction {ps} {es₀} x = record ps { thinking₀ = false -- want to access CS
                                    ; control₀  = 1F }  -- next statement

  MyAction {ps} {es₁} x = record ps { turn      = 1F    -- gives turn to other proc
                                    ; control₀  = 2F }  -- next stmt

  MyAction {ps} {es₂₁} x = record ps { control₀  = 3F }  -- next stmt

  MyAction {ps} {es₂₂} x = record ps { control₀  = 3F }  -- next stmt

  MyAction {ps} {es₃} x = record ps { thinking₀ = true  -- releases the CS
                                    ; control₀  = 0F }  -- loop
  -- Proccess 2
  MyAction {ps} {er₀} x = record ps { thinking₁ = false
                                    ; control₁  = 1F }

  MyAction {ps} {er₁} x = record ps { turn      = 0F
                                    ; control₁  = 2F }

  MyAction {ps} {er₂₁} x = record ps { control₁  = 3F }

  MyAction {ps} {er₂₂} x = record ps { control₁  = 3F }

  MyAction {ps} {er₃} x = record ps { thinking₁ = true
                                    ; control₁  = 0F }

  initialState : State
  initialState = record
                   { thinking₀ = true
                   ; thinking₁ = true
                   ; turn      = 0F
                   ; control₀  = 0F
                   ; control₁  = 0F
                   }

  MyStateMachine : StateMachine State MyEvent
  MyStateMachine = record
                     { initial = _≡ initialState
                     ; enabled = MyEnabled
                     ; action  = MyAction
                     }

  -- Each process has its own EventSet with its statements
  Proc0-EvSet : EventSet {Event = MyEvent}
  Proc0-EvSet ev = ev ≡ es₁ ⊎ ev ≡ es₂₁ ⊎ ev ≡ es₂₂ ⊎ ev ≡ es₃

  Proc1-EvSet : EventSet {Event = MyEvent}
  Proc1-EvSet ev = ev ≡ er₁ ⊎ ev ≡ er₂₁ ⊎ ev ≡ er₂₂ ⊎ ev ≡ er₃

  -- And both EventSets have weak-fairness
  data MyWeakFairness : EventSet → Set where
    wf-p0 : MyWeakFairness Proc0-EvSet
    wf-p1 : MyWeakFairness Proc1-EvSet

  MySystem : System State MyEvent
  MySystem = record
             { stateMachine = MyStateMachine
             ; weakFairness = MyWeakFairness
             }

   -----------------------------------------------------------------------------
   -- PROOFS
   -----------------------------------------------------------------------------

  open LeadsTo State MyEvent MySystem

  inv-c₁≡[0-4] : Invariant MyStateMachine λ st → ∃[ f ] (control₁ st ≡ f)-- ([∃ f ∶ (_≡ f) ∘ control₁ ])
  inv-c₁≡[0-4] (init refl) = 0F , refl
  inv-c₁≡[0-4] (step {event = es₀}  rs enEv) = inv-c₁≡[0-4] rs
  inv-c₁≡[0-4] (step {event = es₁}  rs enEv) = inv-c₁≡[0-4] rs
  inv-c₁≡[0-4] (step {event = es₂₁} rs enEv) = inv-c₁≡[0-4] rs
  inv-c₁≡[0-4] (step {event = es₂₂} rs enEv) = inv-c₁≡[0-4] rs
  inv-c₁≡[0-4] (step {event = es₃}  rs enEv) = inv-c₁≡[0-4] rs
  inv-c₁≡[0-4] (step {event = er₀}  rs enEv) = 1F , refl
  inv-c₁≡[0-4] (step {event = er₁}  rs enEv) = 2F , refl
  inv-c₁≡[0-4] (step {event = er₂₁} rs enEv) = 3F , refl
  inv-c₁≡[0-4] (step {event = er₂₂} rs enEv) = 3F , refl
  inv-c₁≡[0-4] (step {event = er₃}  rs enEv) = 0F , refl

  inv-¬think₁ : Invariant
                  MyStateMachine
                  λ st → control₀ st ≡ 1F ⊎ control₀ st ≡ 2F ⊎ control₀ st ≡ 3F
                       → thinking₀ st ≡ false
  inv-¬think₁ (init refl) (inj₂ (inj₁ ()))
  inv-¬think₁ (init refl) (inj₂ (inj₂ ()))
  inv-¬think₁ (step {event = es₀}  rs enEv) x = refl
  inv-¬think₁ (step {event = es₁}  rs enEv) x = inv-¬think₁ rs (inj₁ enEv)
  inv-¬think₁ (step {event = es₂₁} rs enEv) x = inv-¬think₁ rs (inj₂ (inj₁ (fst enEv)))
  inv-¬think₁ (step {event = es₂₂} rs enEv) x = inv-¬think₁ rs (inj₂ (inj₁ (fst enEv)))
  inv-¬think₁ (step {event = es₃}  rs enEv) (inj₂ (inj₁ ()))
  inv-¬think₁ (step {event = es₃}  rs enEv) (inj₂ (inj₂ ()))
  inv-¬think₁ (step {event = er₀}  rs enEv) x = inv-¬think₁ rs x
  inv-¬think₁ (step {event = er₁}  rs enEv) x = inv-¬think₁ rs x
  inv-¬think₁ (step {event = er₂₁} rs enEv) x = inv-¬think₁ rs x
  inv-¬think₁ (step {event = er₂₂} rs enEv) x = inv-¬think₁ rs x
  inv-¬think₁ (step {event = er₃}  rs enEv) x = inv-¬think₁ rs x

  inv-think₂ : Invariant
                  MyStateMachine
                  λ st → control₁  st ≡ 0F
                       → thinking₁ st ≡ true
  inv-think₂ (init refl) x = refl
  inv-think₂ (step {event = es₀}  rs enEv) x = inv-think₂ rs x
  inv-think₂ (step {event = es₁}  rs enEv) x = inv-think₂ rs x
  inv-think₂ (step {event = es₂₁} rs enEv) x = inv-think₂ rs x
  inv-think₂ (step {event = es₂₂} rs enEv) x = inv-think₂ rs x
  inv-think₂ (step {event = es₃}  rs enEv) x = inv-think₂ rs x
  inv-think₂ (step {event = er₃}  rs enEv) x = refl

  inv-¬think₂ : Invariant
                  MyStateMachine
                  λ st → control₁ st ≡ 1F ⊎ control₁ st ≡ 2F ⊎ control₁ st ≡ 3F
                       → thinking₁ st ≡ false
  inv-¬think₂ (init refl) (inj₂ (inj₁ ()))
  inv-¬think₂ (init refl) (inj₂ (inj₂ ()))
  inv-¬think₂ (step {event = es₀}  rs enEv) x = inv-¬think₂ rs x
  inv-¬think₂ (step {event = es₁}  rs enEv) x = inv-¬think₂ rs x
  inv-¬think₂ (step {event = es₂₁} rs enEv) x = inv-¬think₂ rs x
  inv-¬think₂ (step {event = es₂₂} rs enEv) x = inv-¬think₂ rs x
  inv-¬think₂ (step {event = es₃}  rs enEv) x = inv-¬think₂ rs x
  inv-¬think₂ (step {event = er₀}  rs enEv) x = refl
  inv-¬think₂ (step {event = er₁}  rs enEv) x = inv-¬think₂ rs (inj₁ enEv)
  inv-¬think₂ (step {event = er₂₁} rs enEv) x = inv-¬think₂ rs (inj₂ (inj₁ (fst enEv)))
  inv-¬think₂ (step {event = er₂₂} rs enEv) x = inv-¬think₂ rs (inj₂ (inj₁ (fst enEv)))
  inv-¬think₂ (step {event = er₃}  rs enEv) (inj₂ (inj₁ ()))
  inv-¬think₂ (step {event = er₃}  rs enEv) (inj₂ (inj₂ ()))

  proc0-1-l-t-2 : (_≡ 1F) ∘ control₀ l-t (_≡ 2F) ∘ control₀
  proc0-1-l-t-2 = viaEvSet
                    Proc0-EvSet
                    wf-p0
                    (λ { es₁  (inj₁ refl)               → hoare λ { _ _ → refl }
                       ; es₂₁ (inj₂ (inj₁ refl))        → hoare λ { refl () }
                       ; es₂₂ (inj₂ (inj₂ (inj₁ refl))) → hoare λ { refl () }
                       ; es₃  (inj₂ (inj₂ (inj₂ refl))) → hoare λ { refl () }
                       })
                    (λ { es₀  _ → hoare λ { () refl }
                       ; es₁  x → ⊥-elim (x (inj₁ refl))
                       ; es₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
                       ; es₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
                       ; es₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl))))
                       ; er₀  _ → hoare λ z _ → inj₁ z
                       ; er₁  _ → hoare λ z _ → inj₁ z
                       ; er₂₁ _ → hoare λ z _ → inj₁ z
                       ; er₂₂ _ → hoare λ z _ → inj₁ z
                       ; er₃  _ → hoare λ z _ → inj₁ z
                       })
                    λ _ x → es₁ , inj₁ refl , x

  P⊆P₀⊎P₁ : ∀ {ℓ} {A : Set ℓ} (x : Fin 2)
            → A → A × x ≡ 0F ⊎ A × x ≡ 1F
  P⊆P₀⊎P₁ 0F a = inj₁ (a , refl)
  P⊆P₀⊎P₁ 1F a = inj₂ (a , refl)

  -- y4

  turn≡0-l-t-Q : ((_≡ 2F) ∘ control₀ ∩ (_≡ 0F) ∘ turn ) l-t (_≡ 3F) ∘ control₀
  turn≡0-l-t-Q =
    viaEvSet
      Proc0-EvSet
      wf-p0
      (λ { es₁  (inj₁ refl)               → hoare λ { () refl }
         ; es₂₁ (inj₂ (inj₁ refl))        → hoare λ _ _ → refl
         ; es₂₂ (inj₂ (inj₂ (inj₁ refl))) → hoare λ _ _ → refl
         ; es₃  (inj₂ (inj₂ (inj₂ refl))) → hoare λ { () refl } })
      ( λ { es₀  _ → hoare λ { () refl }
          ; es₁  x → ⊥-elim (x (inj₁ refl))
          ; es₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
          ; es₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
          ; es₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl))))
          ; er₀  _ → hoare (λ z _ → inj₁ z)
          ; er₁  _ → hoare (λ z _ → inj₁ ((fst z) , refl) )
          ; er₂₁ _ → hoare (λ z _ → inj₁ z)
          ; er₂₂ _ → hoare (λ z _ → inj₁ z)
          ; er₃  _ → hoare (λ z _ → inj₁ z)
          } )
      λ { _ (c₀≡2 , tu≡0) → es₂₂ , inj₂ (inj₂ (inj₁ refl)) , c₀≡2 , tu≡0 }

  -- I think I could prove this with the Proc1EvSet

  Pl-tQ∨c₁≡1 : (λ preSt → ( control₀ preSt ≡ 2F × turn preSt ≡ 1F )
                  × control₁ preSt ≡ 0F)
       l-t
        λ posSt →   control₀ posSt ≡ 3F
                  ⊎ (( control₀ posSt ≡ 2F × turn posSt ≡ 1F )
                     × control₁ posSt ≡ 1F )
  Pl-tQ∨c₁≡1 =
    viaEvSet
      Proc0-EvSet
      wf-p0
      (λ { es₁  (inj₁ refl)               → hoare λ { () refl }
         ; es₂₁ (inj₂ (inj₁ refl))        → hoare λ { _ _ → inj₁ refl }
         ; es₂₂ (inj₂ (inj₂ (inj₁ refl))) → hoare λ { _ _ → inj₁ refl }
         ; es₃  (inj₂ (inj₂ (inj₂ refl))) → hoare λ { () refl } })
      ( λ { es₀  _ → hoare λ { () refl }
          ; es₁  x → ⊥-elim (x (inj₁ refl))
          ; es₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
          ; es₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
          ; es₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl))))
          ; er₀  _ → hoare λ { x₁ enEv → inj₂ (inj₂ (fst x₁ , refl)) }
          ; er₁  _ → hoare λ { () refl }
          ; er₂₁ _ → hoare λ { () (refl , _) }
          ; er₂₂ _ → hoare λ { () (refl , _) }
          ; er₃  _ → hoare λ { () refl }
          })
      λ { rs ((c₀≡2 , _) , c₁≡0)
             → es₂₁ , inj₂ (inj₁ refl) , c₀≡2 , inv-think₂ rs c₁≡0 }

  l-t-turn≡0 : ((_≡ 2F) ∘ control₀ ∩ (_≡ 1F) ∘ turn) ∩ (_≡ 1F) ∘ control₁
               l-t
               (_≡ 2F) ∘ control₀ ∩  (_≡ 0F) ∘ turn
  l-t-turn≡0 =
    viaUseInv
      inv-¬think₂
      ( viaEvSet
          Proc1-EvSet
          wf-p1
          ( λ { er₁  (inj₁ refl) → hoare λ { ((x , _) , _) _ _ → fst x , refl  }
              ; er₂₁ (inj₂ (inj₁ refl)) → hoare λ { () (refl , _) _ }
              ; er₂₂ (inj₂ (inj₂ (inj₁ refl))) → hoare λ { () (refl , _) _ }
              ; er₃  (inj₂ (inj₂ (inj₂ refl))) → hoare λ { () refl _ }
              }
          )
          ( λ { es₀  _ → hoare λ { () refl }
              ; es₁  _ → hoare λ { () refl }
              ; es₂₁ _ → hoare λ { ((_ , c₂≡2) , x) (_ , refl)
                                   → contradiction (x (inj₁ c₂≡2)) λ () }
              ; es₂₂ _ → hoare λ { () (_ , refl) }
              ; es₃  _ → hoare λ { () refl }
              ; er₀  _ → hoare λ { () refl }
              ; er₁  x → ⊥-elim (x (inj₁ refl))
              ; er₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
              ; er₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
              ; er₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl)))) }
          )
          λ _ x → er₁ , inj₁ refl , (snd ∘ fst) x
      )

  l-t-c₁≡3 : (λ preSt → ( control₀ preSt ≡ 2F × turn preSt ≡ 1F )
                  × control₁ preSt ≡ 2F)
       l-t
       (λ posSt → ( control₀ posSt ≡ 2F
                  × turn posSt ≡ 1F )
                  × control₁ posSt ≡ 3F)
  l-t-c₁≡3 =
    viaUseInv
      inv-¬think₂
      ( viaEvSet
          Proc1-EvSet
          wf-p1
          ( λ { er₁  (inj₁ refl) → hoare λ { () refl _ }
              ; er₂₁ (inj₂ (inj₁ refl))
                     → hoare λ { ((x , _) , _) _ _ → x , refl }
              ; er₂₂ (inj₂ (inj₂ (inj₁ refl)))
                     → hoare λ { ((x , _) , _) _ _ → x , refl }
              ; er₃  (inj₂ (inj₂ (inj₂ refl))) → hoare λ { () refl _ }
              }
          )
          ( λ { es₀  _ → hoare λ { () refl }
              ; es₁  _ → hoare λ { () refl }
              ; es₂₁ _ → hoare λ { ((_ , c₂≡3) , x) (_ , refl)
                                   → contradiction (x (inj₂ (inj₁ c₂≡3))) λ () }
              ; es₂₂ _ → hoare λ { () (_ , refl) }
              ; es₃  _ → hoare λ { () refl }
              ; er₀  _ → hoare λ { () refl }
              ; er₁  x → ⊥-elim (x (inj₁ refl))
              ; er₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
              ; er₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
              ; er₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl))))
              }
          )
          λ _ x → er₂₂ , inj₂ (inj₂ (inj₁ refl)) , (snd ∘ fst) x , (snd ∘ fst ∘ fst) x
      )

  l-t-c₁≡0 : (λ preSt → ( control₀ preSt ≡ 2F × turn preSt ≡ 1F )
                  × control₁ preSt ≡ 3F)
       l-t
       (λ posSt → ( control₀ posSt ≡ 2F × turn posSt ≡ 1F )
                  × control₁ posSt ≡ 0F)
  l-t-c₁≡0 =
    viaUseInv
      inv-¬think₂
      ( viaEvSet
          Proc1-EvSet
          wf-p1
          ( λ { er₁  (inj₁ refl)        → hoare λ { () refl _ }
              ; er₂₁ (inj₂ (inj₁ refl)) → hoare λ { () (refl , _) _ }
              ; er₂₂ (inj₂ (inj₂ (inj₁ refl))) → hoare λ { () (refl , _) _ }
              ; er₃  (inj₂ (inj₂ (inj₂ refl)))
                     → hoare λ { x _ _ → (fst ∘ fst) x , refl }
              }
          )
          ( λ { es₀  _ → hoare λ { () refl }
              ; es₁  _ → hoare λ { () refl }
              ; es₂₁ _ → hoare λ { ((_ , c₂≡4) , x) (_ , refl)
                                  → contradiction (x (inj₂ (inj₂ c₂≡4))) λ () }
              ; es₂₂ _ → hoare λ { () (_ , refl) }
              ; es₃  _ → hoare λ { () refl }
              ; er₀  _ → hoare λ { () refl }
              ; er₁  x → ⊥-elim (x (inj₁ refl))
              ; er₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
              ; er₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
              ; er₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl))))
              }
          )
          λ _ x → er₃ , inj₂ (inj₂ (inj₂ refl)) , (snd ∘ fst) x
      )

  P∧c₁≡1⇒Q : ((_≡ 2F) ∘ control₀ ∩ (_≡ 1F) ∘ turn) ∩ (_≡ 1F) ∘ control₁
             l-t
             (_≡ 3F) ∘ control₀
  P∧c₁≡1⇒Q = viaTrans l-t-turn≡0 turn≡0-l-t-Q

  P∧c₁≡0⇒Q : ((_≡ 2F) ∘ control₀ ∩ (_≡ 1F) ∘ turn) ∩ (_≡ 0F) ∘ control₁
             l-t
             (_≡ 3F) ∘ control₀
  P∧c₁≡0⇒Q = viaTrans2 Pl-tQ∨c₁≡1 P∧c₁≡1⇒Q

  P∧c₁≡3⇒Q : ((_≡ 2F) ∘ control₀ ∩ (_≡ 1F) ∘ turn) ∩ (_≡ 3F) ∘ control₁
             l-t
             (_≡ 3F) ∘ control₀
  P∧c₁≡3⇒Q = viaTrans l-t-c₁≡0 P∧c₁≡0⇒Q

  P∧c₁≡2⇒Q : ((_≡ 2F) ∘ control₀ ∩ (_≡ 1F) ∘ turn) ∩ (_≡ 2F) ∘ control₁
             l-t
             (_≡ 3F) ∘ control₀
  P∧c₁≡2⇒Q = viaTrans l-t-c₁≡3 P∧c₁≡3⇒Q

  P⊆c₂≡0⊎c₂≢0 : ∀ {ℓ} {A : Set ℓ} (x : Fin 4) → A
                  → A × x ≡ 0F ⊎ A × x ≢ 0F
  P⊆c₂≡0⊎c₂≢0 0F a = inj₁ (a , refl)
  P⊆c₂≡0⊎c₂≢0 (suc x) a = inj₂ (a , (λ ()))

  P⊆c₂≡1⊎c₂≢1 : ∀ {ℓ} {A : Set ℓ} (x : Fin 4) → A × x ≢ 0F
                  → A × x ≡ 1F ⊎ A × x ≢ 0F × x ≢ 1F
  P⊆c₂≡1⊎c₂≢1 0F (a , x≢0) = ⊥-elim (x≢0 refl)
  P⊆c₂≡1⊎c₂≢1 1F (a , x≢0) = inj₁ (a , refl)
  P⊆c₂≡1⊎c₂≢1 (suc (suc x)) (a , x≢0) = inj₂ (a , x≢0 , λ ())

  P⊆c₂≡2⊎c₂≡3 : ∀ {ℓ} {A : Set ℓ} (x : Fin 4) → A × x ≢ 0F × x ≢ 1F
                  → A × x ≡ 2F ⊎ A × x ≡ 3F
  P⊆c₂≡2⊎c₂≡3 0F (a , x≢0 , x≢1) = ⊥-elim (x≢0 refl)
  P⊆c₂≡2⊎c₂≡3 1F (a , x≢0 , x≢1) = ⊥-elim (x≢1 refl)
  P⊆c₂≡2⊎c₂≡3 2F (a , x≢0 , x≢1) = inj₁ (a , refl)
  P⊆c₂≡2⊎c₂≡3 3F (a , x≢0 , x≢1) = inj₂ (a , refl)

  turn≡1-l-t-Q :  ((_≡ 2F) ∘ control₀ ∩ (_≡ 1F) ∘ turn ) l-t (_≡ 3F) ∘ control₀
  turn≡1-l-t-Q = viaAllVal
                   inv-c₁≡[0-4]
                   λ { 0F → P∧c₁≡0⇒Q
                     ; 1F → P∧c₁≡1⇒Q
                     ; 2F → P∧c₁≡2⇒Q
                     ; 3F → P∧c₁≡3⇒Q }

  proc0-2-l-t-3 :  (_≡ 2F) ∘ control₀ l-t (_≡ 3F) ∘ control₀
  proc0-2-l-t-3 = viaDisj
                    (λ {st} c₀≡2 → P⊆P₀⊎P₁ (turn st) c₀≡2 )
                    turn≡0-l-t-Q
                    turn≡1-l-t-Q

  proc1-1-l-t-2 : (λ preSt → control₁ preSt ≡ 1F)
                  l-t
                  λ posSt →   control₁ posSt ≡ 2F
  proc1-1-l-t-2 =
    viaEvSet
      Proc1-EvSet
      wf-p1
      ( λ { er₁  (inj₁ refl) → hoare λ { x enEv → refl }
          ; er₂₁ (inj₂ (inj₁ refl)) → hoare λ { refl () }
          ; er₂₂ (inj₂ (inj₂ (inj₁ refl))) → hoare λ { refl () }
          ; er₃  (inj₂ (inj₂ (inj₂ refl))) → hoare λ { refl () }
          }
      )
      ( λ { es₀  _ → hoare λ z _ → inj₁ z
          ; es₁  _ → hoare λ z _ → inj₁ z
          ; es₂₁ _ → hoare λ z _ → inj₁ z
          ; es₂₂ _ → hoare λ z _ → inj₁ z
          ; es₃  _ → hoare λ z _ → inj₁ z
          ; er₀  _ → hoare λ _ _ → inj₁ refl
          ; er₁  x → ⊥-elim (x (inj₁ refl))
          ; er₂₁ x → ⊥-elim (x (inj₂ (inj₁ refl)))
          ; er₂₂ x → ⊥-elim (x (inj₂ (inj₂ (inj₁ refl))))
          ; er₃  x → ⊥-elim (x (inj₂ (inj₂ (inj₂ refl))))
          }
      )
      λ _ x → er₁ , inj₁ refl , x

  -- The proofs are the same as proc0-2-l-t-3 but symmetric.
  -- We will postulate by now!
  postulate
    proc1-2-l-t-3 : ( λ preSt →  control₁ preSt ≡ 2F )
                     l-t
                     λ posSt → control₁ posSt ≡ 3F

  -- We proved this via transitivity :
  -- control₀ fstSt ≡ 1F   l-t   control₀ someSt ≡ 2F   l-t   control₀ ≡ 3F
  proc0-live : (λ preSt → control₀ preSt ≡ 1F) l-t (λ posSt → control₀ posSt ≡ 3F)
  proc0-live = viaTrans proc0-1-l-t-2 proc0-2-l-t-3

  proc1-live : (λ preSt → control₁ preSt ≡ 1F) l-t (λ posSt → control₁ posSt ≡ 3F)
  proc1-live = viaTrans proc1-1-l-t-2 proc1-2-l-t-3

  ------------------------------------------------------------------------------
   -- Liveness property
  ------------------------------------------------------------------------------
  --   If Process 1 (Process 2) wants to access the critical section, which
  --   means its control variable is in 1F (it just expressed its will in
  --   accessing the CS in r₀) then it will eventually access the CS
  progress : ( (_≡ 1F) ∘ control₀ l-t (_≡ 3F) ∘ control₀ )
           × ( (_≡ 1F) ∘ control₁ l-t (_≡ 3F) ∘ control₁ )
  progress = proc0-live , proc1-live

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


text: module Interaction-and-input-file where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
-- Reported and fixed by Andrea Vezzosi.

module Issue898 where

id : {A : Set} -> A -> A
id = ?


text:
module Data.Word.Primitive where

postulate
  Word : Set
  Word8 : Set
  Word16 : Set
  Word32 : Set
  Word64 : Set

{-# FOREIGN GHC import qualified Data.Word #-}
{-# COMPILE GHC Word = type Data.Word.Word #-}
{-# COMPILE GHC Word8 = type Data.Word.Word8 #-}
{-# COMPILE GHC Word16 = type Data.Word.Word16 #-}
{-# COMPILE GHC Word32 = type Data.Word.Word32 #-}
{-# COMPILE GHC Word64 = type Data.Word.Word64 #-}

max_stars_repo_name: agda/agda-system-io

max_issues_repo_name: agda/agda-system-io

max_forks_repo_name: agda/agda-system-io