text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous equality
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.HeterogeneousEquality where

import Axiom.Extensionality.Heterogeneous as Ext
open import Data.Product
open import Data.Unit.NonEta
open import Function
open import Function.Inverse using (Inverse)
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Indexed.Heterogeneous
  using (IndexedSetoid)
open import Relation.Binary.Indexed.Heterogeneous.Construct.At
  using (_atₛ_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

import Relation.Binary.HeterogeneousEquality.Core as Core

------------------------------------------------------------------------
-- Heterogeneous equality

infix 4 _≇_

open Core public using (_≅_; refl)

-- Nonequality.

_≇_ : ∀ {ℓ} {A : Set ℓ} → A → {B : Set ℓ} → B → Set ℓ
x ≇ y = ¬ x ≅ y

------------------------------------------------------------------------
-- Conversion

open Core public using (≅-to-≡; ≡-to-≅)

≅-to-type-≡ : ∀ {a} {A B : Set a} {x : A} {y : B} →
                x ≅ y → A ≡ B
≅-to-type-≡ refl = refl

≅-to-subst-≡ : ∀ {a} {A B : Set a} {x : A} {y : B} → (p : x ≅ y) →
                 P.subst (λ x → x) (≅-to-type-≡ p) x ≡ y
≅-to-subst-≡ refl = refl

------------------------------------------------------------------------
-- Some properties

reflexive : ∀ {a} {A : Set a} → _⇒_ {A = A} _≡_ (λ x y → x ≅ y)
reflexive refl = refl

sym : ∀ {ℓ} {A B : Set ℓ} {x : A} {y : B} → x ≅ y → y ≅ x
sym refl = refl

trans : ∀ {ℓ} {A B C : Set ℓ} {x : A} {y : B} {z : C} →
        x ≅ y → y ≅ z → x ≅ z
trans refl eq = eq

subst : ∀ {a} {A : Set a} {p} → Substitutive {A = A} (λ x y → x ≅ y) p
subst P refl p = p

subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
         ∀ {x₁ x₂ y₁ y₂} → x₁ ≅ x₂ → y₁ ≅ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

subst-removable : ∀ {a p} {A : Set a}
                  (P : A → Set p) {x y} (eq : x ≅ y) z →
                  subst P eq z ≅ z
subst-removable P refl z = refl

≡-subst-removable : ∀ {a p} {A : Set a}
                    (P : A → Set p) {x y} (eq : x ≡ y) z →
                    P.subst P eq z ≅ z
≡-subst-removable P refl z = refl

cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}
       (f : (x : A) → B x) → x ≅ y → f x ≅ f y
cong f refl = refl

cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
           f ≅ g → (x : A) → f x ≅ g x
cong-app refl x = refl

cong₂ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c}
          {x y u v}
        (f : (x : A) (y : B x) → C x y) → x ≅ y → u ≅ v → f x u ≅ f y v
cong₂ f refl refl = refl

resp₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ (λ x y → x ≅ y)
resp₂ _∼_ = subst⟶resp₂ _∼_ subst

icong : ∀ {a b ℓ} {I : Set ℓ}
        (A : I → Set a) {B : {k : I} → A k → Set b}
        {i j : I} {x : A i} {y : A j} →
        i ≡ j →
        (f : {k : I} → (z : A k) → B z) →
        x ≅ y →
        f x ≅ f y
icong _ refl _ refl = refl

icong₂ : ∀ {a b c ℓ} {I : Set ℓ}
         (A : I → Set a)
         {B : {k : I} → A k → Set b}
         {C : {k : I} → (a : A k) → B a → Set c}
         {i j : I} {x : A i} {y : A j} {u : B x} {v : B y} →
         i ≡ j →
         (f : {k : I} → (z : A k) → (w : B z) → C z w) →
         x ≅ y → u ≅ v →
         f x u ≅ f y v
icong₂ _ refl _ refl refl = refl

icong-subst-removable : ∀ {a b ℓ}
                        {I : Set ℓ}
                        (A : I → Set a) {B : {k : I} → A k → Set b}
                        {i j : I} (eq : i ≅ j)
                        (f : {k : I} → (z : A k) → B z)
                        (x : A i) →
                        f (subst A eq x) ≅ f x
icong-subst-removable _ refl _ _ = refl

icong-≡-subst-removable : ∀ {a b ℓ}
                          {I : Set ℓ}
                          (A : I → Set a) {B : {k : I} → A k → Set b}
                          {i j : I} (eq : i ≡ j)
                          (f : {k : I} → (z : A k) → B z)
                          (x : A i) →
                          f (P.subst A eq x) ≅ f x
icong-≡-subst-removable _ refl _ _ = refl

------------------------------------------------------------------------
--Proof irrelevance

≅-irrelevant : ∀ {ℓ} {A B : Set ℓ} → Irrelevant ((A → B → Set ℓ) ∋ λ a → a ≅_)
≅-irrelevant refl refl = refl

module _ {ℓ} {A₁ A₂ A₃ A₄ : Set ℓ} {a₁ : A₁} {a₂ : A₂} {a₃ : A₃} {a₄ : A₄} where

 ≅-heterogeneous-irrelevant : (p : a₁ ≅ a₂) (q : a₃ ≅ a₄) → a₂ ≅ a₃ → p ≅ q
 ≅-heterogeneous-irrelevant refl refl refl = refl

 ≅-heterogeneous-irrelevantˡ : (p : a₁ ≅ a₂) (q : a₃ ≅ a₄) → a₁ ≅ a₃ → p ≅ q
 ≅-heterogeneous-irrelevantˡ refl refl refl = refl

 ≅-heterogeneous-irrelevantʳ : (p : a₁ ≅ a₂) (q : a₃ ≅ a₄) → a₂ ≅ a₄ → p ≅ q
 ≅-heterogeneous-irrelevantʳ refl refl refl = refl

------------------------------------------------------------------------
-- Structures

isEquivalence : ∀ {a} {A : Set a} →
                IsEquivalence {A = A} (λ x y → x ≅ y)
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = λ x y → x ≅ y
  ; isEquivalence = isEquivalence
  }

indexedSetoid : ∀ {a b} {A : Set a} → (A → Set b) → IndexedSetoid A _ _
indexedSetoid B = record
  { Carrier       = B
  ; _≈_           = λ x y → x ≅ y
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }

≡↔≅ : ∀ {a b} {A : Set a} (B : A → Set b) {x : A} →
      Inverse (P.setoid (B x)) ((indexedSetoid B) atₛ x)
≡↔≅ B = record
  { to         = record { _⟨$⟩_ = id; cong = ≡-to-≅ }
  ; from       = record { _⟨$⟩_ = id; cong = ≅-to-≡ }
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl
    ; right-inverse-of = λ _ → refl
    }
  }

decSetoid : ∀ {a} {A : Set a} →
            Decidable {A = A} {B = A} (λ x y → x ≅ y) →
            DecSetoid _ _
decSetoid dec = record
  { _≈_              = λ x y → x ≅ y
  ; isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = dec
      }
  }

isPreorder : ∀ {a} {A : Set a} →
             IsPreorder {A = A} (λ x y → x ≅ y) (λ x y → x ≅ y)
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  }

isPreorder-≡ : ∀ {a} {A : Set a} →
               IsPreorder {A = A} _≡_ (λ x y → x ≅ y)
isPreorder-≡ = record
  { isEquivalence = P.isEquivalence
  ; reflexive     = reflexive
  ; trans         = trans
  }

preorder : ∀ {a} → Set a → Preorder _ _ _
preorder A = record
  { Carrier    = A
  ; _≈_        = _≡_
  ; _∼_        = λ x y → x ≅ y
  ; isPreorder = isPreorder-≡
  }

------------------------------------------------------------------------
-- Convenient syntax for equational reasoning

module ≅-Reasoning where

  -- The code in `Relation.Binary.Reasoning.Setoid` cannot handle
  -- heterogeneous equalities, hence the code duplication here.

  infix  4 _IsRelatedTo_
  infix  3 _∎
  infixr 2 _≅⟨_⟩_ _≅˘⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
  infix  1 begin_

  data _IsRelatedTo_ {ℓ} {A : Set ℓ} (x : A) {B : Set ℓ} (y : B) :
                     Set ℓ where
    relTo : (x≅y : x ≅ y) → x IsRelatedTo y

  begin_ : ∀ {ℓ} {A : Set ℓ} {x : A} {B} {y : B} →
           x IsRelatedTo y → x ≅ y
  begin relTo x≅y = x≅y

  _≅⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} {C} {z : C} →
           x ≅ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)

  _≅˘⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} {C} {z : C} →
            y ≅ x → y IsRelatedTo z → x IsRelatedTo z
  _ ≅˘⟨ y≅x ⟩ relTo y≅z = relTo (trans (sym y≅x) y≅z)

  _≡⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y C} {z : C} →
           x ≡ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≡⟨ x≡y ⟩ relTo y≅z = relTo (trans (reflexive x≡y) y≅z)

  _≡˘⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y C} {z : C} →
            y ≡ x → y IsRelatedTo z → x IsRelatedTo z
  _ ≡˘⟨ y≡x ⟩ relTo y≅z = relTo (trans (sym (reflexive y≡x)) y≅z)

  _≡⟨⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} →
          x IsRelatedTo y → x IsRelatedTo y
  _ ≡⟨⟩ x≅y = x≅y

  _∎ : ∀ {a} {A : Set a} (x : A) → x IsRelatedTo x
  _∎ _ = relTo refl

------------------------------------------------------------------------
-- Inspect

-- Inspect can be used when you want to pattern match on the result r
-- of some expression e, and you also need to "remember" that r ≡ e.

record Reveal_·_is_ {a b} {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (a ⊔ b) where
  constructor [_]
  field eq : f x ≅ y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

-- Example usage:

-- f x y with g x | inspect g x
-- f x y | c z | [ eq ] = ...

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

-- Version 0.15

proof-irrelevance = ≅-irrelevant
{-# WARNING_ON_USAGE proof-irrelevance
"Warning: proof-irrelevance was deprecated in v0.15.
Please use ≅-irrelevant instead."
#-}

-- Version 1.0

≅-irrelevance = ≅-irrelevant
{-# WARNING_ON_USAGE ≅-irrelevance
"Warning: ≅-irrelevance was deprecated in v1.0.
Please use ≅-irrelevant instead."
#-}
≅-heterogeneous-irrelevance = ≅-heterogeneous-irrelevant
{-# WARNING_ON_USAGE ≅-heterogeneous-irrelevance
"Warning: ≅-heterogeneous-irrelevance was deprecated in v1.0.
Please use ≅-heterogeneous-irrelevant instead."
#-}
≅-heterogeneous-irrelevanceˡ = ≅-heterogeneous-irrelevantˡ
{-# WARNING_ON_USAGE ≅-heterogeneous-irrelevanceˡ
"Warning: ≅-heterogeneous-irrelevanceˡ was deprecated in v1.0.
Please use ≅-heterogeneous-irrelevantˡ instead."
#-}
≅-heterogeneous-irrelevanceʳ = ≅-heterogeneous-irrelevantʳ
{-# WARNING_ON_USAGE ≅-heterogeneous-irrelevanceʳ
"Warning: ≅-heterogeneous-irrelevanceʳ was deprecated in v1.0.
Please use ≅-heterogeneous-irrelevantʳ instead."
#-}
Extensionality = Ext.Extensionality
{-# WARNING_ON_USAGE Extensionality
"Warning: Extensionality was deprecated in v1.0.
Please use Extensionality from `Axiom.Extensionality.Heterogeneous` instead."
#-}
≡-ext-to-≅-ext = Ext.≡-ext⇒≅-ext
{-# WARNING_ON_USAGE ≡-ext-to-≅-ext
"Warning: ≡-ext-to-≅-ext was deprecated in v1.0.
Please use ≡-ext⇒≅-ext from `Axiom.Extensionality.Heterogeneous` instead."
#-}


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

module Data.Word8.Primitive where

open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.Nat using (Nat)

{-# FOREIGN GHC import qualified Data.Word #-}
{-# FOREIGN GHC import qualified Data.Bits #-}
postulate
  Word8 : Set
  _==_ : Word8 → Word8 → Bool
  _/=_ : Word8 → Word8 → Bool
  _xor_ : Word8 → Word8 → Word8
  _and_ : Word8 → Word8 → Word8
  _or_ : Word8 → Word8 → Word8
{-# COMPILE GHC Word8 = type Data.Word.Word8 #-}
{-# COMPILE GHC _==_ = (Prelude.==) #-}
{-# COMPILE GHC _/=_ = (Prelude./=) #-}
{-# COMPILE GHC _xor_ = (Data.Bits.xor) #-}
{-# COMPILE GHC _and_ = (Data.Bits..&.) #-}
{-# COMPILE GHC _or_ = (Data.Bits..|.) #-}

postulate
  primWord8fromNat : Nat → Word8
  primWord8toNat : Word8 → Nat
{-# COMPILE GHC primWord8fromNat = (\n -> Prelude.fromIntegral n) #-}
{-# COMPILE GHC primWord8toNat = (\w -> Prelude.fromIntegral w) #-}

ext: agda

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
------------------------------------------------------------------------------
-- Testing the --schematic-propositional-symbols option
------------------------------------------------------------------------------

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

-- Fails because requires the above option.

module RequiredOption.SchematicPropositionalSymbols where

postulate D : Set

postulate id : (P : Set) → P → P
{-# ATP prove id #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Formalization.ClassicalPropositionalLogic.NaturalDeduction.Consistency where

import      Lvl
open import Formalization.ClassicalPropositionalLogic.NaturalDeduction
open import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Proofs
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Functional
open import Logic.Propositional as Logic using (_←_)
open import Logic.Propositional.Theorems as Logic using ()
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to singleton ; _≡_ to _≡ₛ_)
open import Type

private variable ℓₚ ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable P : Type{ℓₚ}
private variable Γ Γ₁ Γ₂ : Formulas(P){ℓ}
private variable φ ψ : Formula(P)

Inconsistent : Formulas(P){ℓ} → Type
Inconsistent(Γ) = Γ ⊢ ⊥

Consistent : Formulas(P){ℓ} → Type
Consistent(Γ) = Γ ⊬ ⊥

consistency-of-[∪]ₗ : Consistent(Γ₁ ∪ Γ₂) → Consistent(Γ₁)
consistency-of-[∪]ₗ con z = con (weaken-union z)

[⊢]-derivability-inconsistency : (Γ ⊢ φ) Logic.↔ Inconsistent(Γ ∪ singleton(¬ φ))
[⊢]-derivability-inconsistency = Logic.[↔]-intro [¬]-elim ([¬]-intro-converse ∘ [¬¬]-intro)

[⊢]-derivability-consistencyᵣ : Consistent(Γ) → ((Γ ⊢ φ) → Consistent(Γ ∪ singleton(φ)))
[⊢]-derivability-consistencyᵣ con Γφ Γφ⊥ = con([⊥]-intro Γφ ([¬]-intro Γφ⊥))

[⊢]-explosion-inconsistency : (∀{φ} → (Γ ⊢ φ)) Logic.↔ Inconsistent(Γ)
[⊢]-explosion-inconsistency {Γ} = Logic.[↔]-intro (λ z → [⊥]-elim z) (λ z → z)

[⊢]-compose-inconsistency : (Γ ⊢ φ) → Inconsistent(Γ ∪ singleton(φ)) → Inconsistent(Γ)
[⊢]-compose-inconsistency Γφ Γφ⊥ = [⊥]-intro Γφ ([¬]-intro Γφ⊥)

[⊢]-compose-consistency : (Γ ⊢ φ) → Consistent(Γ) → Consistent(Γ ∪ singleton(φ))
[⊢]-compose-consistency Γφ = Logic.contrapositiveᵣ ([⊢]-compose-inconsistency Γφ)

[⊢]-subset-consistency : (Γ₁ ⊆ Γ₂) → (Consistent(Γ₂) → Consistent(Γ₁))
[⊢]-subset-consistency sub con = con ∘ weaken sub

[⊢]-subset-inconsistency : (Γ₁ ⊆ Γ₂) → (Inconsistent(Γ₁) → Inconsistent(Γ₂))
[⊢]-subset-inconsistency sub = weaken sub

[⊬]-negation-consistency : (Γ ⊬ (¬ φ)) → Consistent(Γ ∪ singleton(φ))
[⊬]-negation-consistency = _∘ [¬]-intro

[⊢]-consistent-noncontradicting-membership : Consistent(Γ) → ((¬ φ) ∈ Γ) → (φ ∈ Γ) → Logic.⊥
[⊢]-consistent-noncontradicting-membership con Γ¬φ Γφ = con([⊥]-intro (direct Γφ) (direct Γ¬φ))

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:
open import Structure.Operator.Field
open import Structure.Setoid
open import Type

-- Operators for matrices over a field.
module Numeral.Matrix.OverField {ℓ ℓₑ}{T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_+ₛ_ _⋅ₛ_ : T → T → T} ⦃ field-structure : Field(_+ₛ_)(_⋅ₛ_) ⦄ where
open Field(field-structure) renaming (_−_ to _−ₛ_ ; −_ to −ₛ_ ; 𝟎 to 𝟎ₛ ; 𝟏 to 𝟏ₛ)

open import Data.Tuple as Tuple using (_,_)
open import Logic.Predicate
open import Numeral.Matrix
open import Numeral.Matrix.Proofs
open import Structure.Operator.Properties

𝟎 : ∀{s} → Matrix(s)(T)
𝟎 = fill(𝟎ₛ)

𝟏 : ∀{n} → Matrix(n , n)(T)
𝟏 = SquareMatrix.scalarMat(𝟎ₛ)(𝟏ₛ)

_+_ : ∀{s} → Matrix(s)(T) → Matrix(s)(T) → Matrix(s)(T)
_+_ = map₂(_+ₛ_)
infixr 1000 _+_

_−_ : ∀{s} → Matrix(s)(T) → Matrix(s)(T) → Matrix(s)(T)
_−_ = map₂(_−ₛ_)
infixr 1000 _−_

−_ : ∀{s} → Matrix(s)(T) → Matrix(s)(T)
−_ = map(−ₛ_)
infixr 1000 −_

_⨯_ : ∀{x y z} → Matrix(y , z)(T) → Matrix(x , y)(T) → Matrix(x , z)(T)
_⨯_ = multPattern(_+ₛ_)(_⋅ₛ_)(𝟎ₛ)
infixr 1000 _⨯_

_⁻¹ : ∀{n} → (M : Matrix(n , n)(T)) ⦃ inver : InvertibleElement(_⨯_) ⦃ [∃]-intro 𝟏 ⦃ {!matrix-multPattern-identity!} ⦄ ⦄ (M) ⦄ → Matrix(n , n)(T)
_⁻¹ _ ⦃ inver ⦄ = [∃]-witness inver


text:
module Five where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

import Data.Nat as ℕ
import Data.Nat.Properties as ℕₚ
import Data.List as List
import Data.List.Properties as Listₚ
import Data.Product as Product

open List using (List; []; _∷_; _++_)
open ℕ using (ℕ; zero; suc; _+_)
open Product using (Σ; _,_)

-- Our language consists of constants and addition
data Expr : Set where
  const : ℕ → Expr
  plus : Expr → Expr → Expr

-- Straightforward semantics
eval-expr : Expr → ℕ
eval-expr (const n) = n
eval-expr (plus e1 e2) = eval-expr e1 + eval-expr e2

data Instr : Set where
  push : ℕ → Instr
  add : Instr

Prog = List Instr

Stack = List ℕ

run : Prog → Stack → Stack
run [] s = s
run (push n ∷ p) s = run p (n ∷ s)
run (add ∷ p) (a1 ∷ a2 ∷ s) = run p (a1 + a2 ∷ s)
run (add ∷ p) s = run p s

compile : Expr → Prog
compile (const n) = push n ∷ []
compile (plus e1 e2) = compile e1 ++ compile e2 ++ add ∷ []

-- Task 2. Prove that you get the expected result when you compile and run the program.
compile-correct-split : ∀ p q s → run (p ++ q) s ≡ run q (run p s)
compile-correct-split = {!!}

compile-correct-exist : ∀ e s → Σ ℕ (λ m → run (compile e) s ≡ m ∷ s)
compile-correct-exist = {!!}

compile-correct-gen : ∀ e s → run (compile e) s ≡ run (compile e) [] ++ s
compile-correct-gen = {!!}

compile-correct : ∀ e → run (compile e) [] ≡ eval-expr e ∷ []
compile-correct = {!!}


text:
open import Prelude renaming (lift to finlift) hiding (id; subst)

module Implicits.Substitutions.Lemmas.LNMetaType where

open import Implicits.Syntax.LNMetaType
open import Implicits.Substitutions.LNMetaType

open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec.Properties
open import Data.Star using (Star; ε; _◅_)
open import Data.Nat.Properties
open import Data.Nat as Nat
open import Extensions.Substitution
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)
open import Relation.Binary.HeterogeneousEquality as H using ()
module HR = H.≅-Reasoning

typeLemmas : TermLemmas MetaType
typeLemmas = record { termSubst = typeSubst; app-var = refl ; /✶-↑✶ = Lemma./✶-↑✶ }
  where
    module Lemma {T₁ T₂} {lift₁ : Lift T₁ MetaType} {lift₂ : Lift T₂ MetaType} where

      open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
      open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

      /✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                          (∀ k x → (simpl (mvar x)) /✶₁ σs₁ ↑✶₁ k ≡ (simpl (mvar x)) /✶₂ σs₂ ↑✶₂ k) →
                          ∀ k t → t /✶₁ σs₁ ↑✶₁ k ≡ t /✶₂ σs₂ ↑✶₂ k
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (mvar x)) = hyp k x
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tvar x)) = begin
          simpl (tvar x) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ MetaTypeApp.tvar-/✶-↑✶ _ k ρs₁ ⟩
          simpl (tvar x)
          ≡⟨ sym $ MetaTypeApp.tvar-/✶-↑✶ _ k ρs₂ ⟩
          simpl (tvar x) /✶₂ ρs₂ ↑✶₂ k ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tc c)) = begin
          (simpl (tc c)) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ MetaTypeApp.tc-/✶-↑✶ _ k ρs₁ ⟩
          (simpl (tc c))
          ≡⟨ sym $ MetaTypeApp.tc-/✶-↑✶ _ k ρs₂ ⟩
          (simpl (tc c)) /✶₂ ρs₂ ↑✶₂ k ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (a →' b)) = begin
          (simpl (a →' b)) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ MetaTypeApp.→'-/✶-↑✶ _ k ρs₁ ⟩
          simpl ((a /✶₁ ρs₁ ↑✶₁ k) →' (b /✶₁ ρs₁ ↑✶₁ k))
          ≡⟨ cong₂ (λ a b → simpl (a →' b)) (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
          simpl ((a /✶₂ ρs₂ ↑✶₂ k) →' (b /✶₂ ρs₂ ↑✶₂ k))
          ≡⟨ sym (MetaTypeApp.→'-/✶-↑✶ _ k ρs₂) ⟩
          (simpl (a →' b)) /✶₂ ρs₂ ↑✶₂ k
          ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (a ⇒ b) = begin
          (a ⇒ b) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ MetaTypeApp.⇒-/✶-↑✶ _ k ρs₁ ⟩ --
          (a /✶₁ ρs₁ ↑✶₁ k) ⇒ (b /✶₁ ρs₁ ↑✶₁ k)
          ≡⟨ cong₂ _⇒_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
          (a /✶₂ ρs₂ ↑✶₂ k) ⇒ (b /✶₂ ρs₂ ↑✶₂ k)
          ≡⟨ sym (MetaTypeApp.⇒-/✶-↑✶ _ k ρs₂) ⟩
          (a ⇒ b) /✶₂ ρs₂ ↑✶₂ k
          ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (∀' a) = begin
          (∀' a) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ MetaTypeApp.∀'-/✶-↑✶ _ k ρs₁ ⟩
          ∀' (a /✶₁ ρs₁ ↑✶₁ k)
          ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp k a) ⟩
          ∀' (a /✶₂ ρs₂ ↑✶₂ k)
          ≡⟨ sym (MetaTypeApp.∀'-/✶-↑✶ _ k ρs₂) ⟩
          (∀' a) /✶₂ ρs₂ ↑✶₂ k
          ∎

open TermLemmas typeLemmas public hiding (var; id; _/_; _↑⋆_; wk; weaken; sub)
open AdditionalLemmas typeLemmas public

-- The above lemma /✶-↑✶ specialized to single substitutions
/-↑⋆ : ∀ {T₁ T₂} {lift₁ : Lift T₁ MetaType} {lift₂ : Lift T₂ MetaType} →
    let open Lifted lift₁ using () renaming (_↑⋆_ to _↑⋆₁_; _/_ to _/₁_)
        open Lifted lift₂ using () renaming (_↑⋆_ to _↑⋆₂_; _/_ to _/₂_)
    in
    ∀ {n k} (ρ₁ : Sub T₁ n k) (ρ₂ : Sub T₂ n k) →
    (∀ i x → (simpl (mvar x)) /₁ ρ₁ ↑⋆₁ i ≡ (simpl (mvar x)) /₂ ρ₂ ↑⋆₂ i) →
        ∀ i a → a /₁ ρ₁ ↑⋆₁ i ≡ a /₂ ρ₂ ↑⋆₂ i
/-↑⋆ ρ₁ ρ₂ hyp i a = /✶-↑✶ (ρ₁ ◅ ε) (ρ₂ ◅ ε) hyp i a

-- weakening a simple type gives a simple type
simpl-wk : ∀ {ν} k (τ : MetaSType (k N+ ν)) → ∃ λ τ' → (simpl τ) / wk ↑⋆ k ≡ simpl τ'
simpl-wk k (tc x) = , refl
simpl-wk k (mvar n) = , var-/-wk-↑⋆ k n
simpl-wk k (tvar n) = , refl
simpl-wk k (x →' x₁) = , refl

tclosed-wk : ∀ {ν m} {a : MetaType m} → TClosed ν a → TClosed (suc ν) a
tclosed-wk (a ⇒ b) = tclosed-wk a ⇒ tclosed-wk b
tclosed-wk (∀' x) = ∀' (tclosed-wk x)
tclosed-wk (simpl x) = simpl $ tclosed-wks x
  where
    tclosed-wks : ∀ {ν m} {τ : MetaSType m} → TClosedS ν τ → TClosedS (suc ν) τ
    tclosed-wks (tvar p) = tvar (≤-steps 1 p)
    tclosed-wks mvar = mvar
    tclosed-wks (a →' b) = (tclosed-wk a) →' (tclosed-wk b)
    tclosed-wks tc = tc

-- proper substitution doesn't affect the number of tvars
tclosed-/ : ∀ {m m' n} (a : MetaType m) {σ : Sub MetaType m m'} → TClosed n a →
            (∀ i → TClosed n (lookup i σ)) → TClosed n (a / σ)
tclosed-/ (a ⇒ b) (ca ⇒ cb) f = tclosed-/ a ca f ⇒ tclosed-/ b cb f
tclosed-/ (∀' a) (∀' x) f = ∀' (tclosed-/ a x (λ p → tclosed-wk (f p)))
tclosed-/ (simpl x) (simpl y) f = tclosed-/s x y f
  where
    tclosed-/s : ∀ {m m' n} (a : MetaSType m) {σ : Sub MetaType m m'} → TClosedS n a →
                 (∀ i → TClosed n (lookup i σ)) → TClosed n (a simple/ σ)
    tclosed-/s (tvar _) (tvar p) f = simpl (tvar p)
    tclosed-/s (mvar i) _ f = f i
    tclosed-/s (a →' b) (ca →' cb) f = simpl (tclosed-/ a ca f →' tclosed-/ b cb f)
    tclosed-/s (tc c) _ _ = simpl tc

-- opening any free tvar will reduce the number of free tvars
tclosed-open : ∀ {m ν} {a : MetaType m} k → k N< (suc ν) → TClosed (suc ν) a →
               TClosed ν (open-meta k a)
tclosed-open k k<ν (a ⇒ b) = (tclosed-open k k<ν a) ⇒ (tclosed-open k k<ν b)
tclosed-open k k<ν (∀' a) = ∀' (tclosed-open (suc k) (s≤s k<ν) a)
tclosed-open k k<ν (simpl (tvar {x = x} p)) with Nat.compare x k
tclosed-open .(suc (k' N+ k)) (s≤s k<ν) (simpl (tvar p)) | less k' k =
  simpl (tvar (≤-trans (m≤m+n (suc k') k) k<ν))
tclosed-open x k<ν (simpl (tvar x₁)) | equal .x = simpl mvar
tclosed-open m k<ν (simpl (tvar (s≤s p))) | greater .m k = simpl (tvar p)
tclosed-open k k<ν (simpl mvar) = simpl mvar
tclosed-open k k<ν (simpl (x →' x₁)) = simpl (tclosed-open k k<ν x →' tclosed-open k k<ν x₁)
tclosed-open k k<ν (simpl tc) = simpl tc

open-meta-◁m₁ : ∀ {m k} (a : MetaType m) → (open-meta k a) ◁m₁ ≡ a ◁m₁
open-meta-◁m₁ (a ⇒ b) = open-meta-◁m₁ b
open-meta-◁m₁ (∀' a) = cong suc (open-meta-◁m₁ a)
open-meta-◁m₁ (simpl x) = refl

lem : ∀ {m} n k (a : MetaType m) → open-meta n (open-meta (n N+ suc k) a) H.≅
                                    open-meta (n N+ k) (open-meta n a)
lem n k (a ⇒ b) = H.cong₂ _⇒_ (lem n k a) (lem n k b)
lem n k (∀' a) = H.cong ∀' (lem _ _ a)
lem n k (simpl (tvar x)) with Nat.compare x (n N+ (suc k))
lem n k (simpl (tvar x)) | z = {!z!}
lem n k (simpl (mvar x)) = H.refl
lem n k (simpl (a →' b)) = H.cong₂ (λ u v → simpl (u →' v)) (lem n k a) (lem n k b)
lem n k (simpl (tc x)) = H.refl

open-meta-◁m : ∀ {m} k (a : MetaType m) →
               ((open-meta k a) ◁m) H.≅ open-meta k (a ◁m)
open-meta-◁m k (a ⇒ b) = open-meta-◁m k b
open-meta-◁m k (∀' a) = HR.begin
  open-meta zero ((open-meta (suc k)) a ◁m)
    HR.≅⟨  {!!} ⟩
  open-meta zero (open-meta (suc k) (a ◁m))
    HR.≅⟨ lem zero k (a ◁m) ⟩
  open-meta k (open-meta zero (a ◁m)) HR.∎
open-meta-◁m k (simpl x) = H.refl

open import Implicits.Syntax.Type
open import Implicits.Substitutions.Type as TS using ()

lem₁ : ∀ {ν} k (a : Type (k N+ suc ν)) (b : Type ν) →
                (to-meta (a TS./ (TS.sub b) TS.↑⋆ k)) ≡
                  (open-meta k (to-meta a) / sub (to-meta b))
lem₁ k (simpl (tc x)) b = refl
lem₁ k (simpl (tvar n)) b with Nat.compare (toℕ n) k
lem₁ k (simpl (tvar n)) b | z = {!!}
lem₁ k (simpl (a →' b)) c = cong₂ (λ u v → simpl (u →' v)) (lem₁ k a c) (lem₁ k b c)
lem₁ k (a ⇒ b) c = cong₂ _⇒_ (lem₁ k a c) (lem₁ k b c)
lem₁ k (∀' a) b = cong ∀' (lem₁ (suc k) a b)


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

open import Categories.Category

module Categories.Category.CartesianClosed.Locally {o ℓ e} (C : Category o ℓ e) where

open import Level using (levelOfTerm)

open import Categories.Category.CartesianClosed
open import Categories.Category.Cartesian
open import Categories.Category.Cartesian.Properties C
open import Categories.Category.Complete.Finitely C
open import Categories.Category.Slice C
open import Categories.Category.Slice.Properties C

open import Categories.Object.Product
open import Categories.Object.Exponential
open import Categories.Object.Terminal C
import Categories.Diagram.Pullback as P
import Categories.Diagram.Pullback.Properties C as Pₚ
import Categories.Morphism.Reasoning as MR

open Category C

record Locally : Set (levelOfTerm C) where
  field
    sliceCCC : ∀ A → CartesianClosed (Slice A)

  module sliceCCC A = CartesianClosed (sliceCCC A)

  pullbacks : ∀ {X A B} (f : A ⇒ X) (g : B ⇒ X) → P.Pullback C f g
  pullbacks {X} f g = product⇒pullback product
    where C/X = sliceCCC X
          open CartesianClosed C/X using (product)

  -- the slice categories also have pullbacks, because slice of slice is slice.
  slice-pullbacks : ∀ {A} {B X Y : SliceObj A} (f : Slice⇒ X B) (g : Slice⇒ Y B) → P.Pullback (Slice A) f g
  slice-pullbacks {A} {B} {X} {Y} f g = record
    { P               = sliceobj (X.arr ∘ p.p₁)
    ; p₁              = slicearr refl
    ; p₂              = slicearr comm
    ; commute         = p.commute
    ; universal       = λ {Z} {h i} eq → slicearr {h = p.universal eq} (pullʳ p.p₁∘universal≈h₁ ○ Slice⇒.△ h)
    ; unique          = λ eq₁ eq₂ → p.unique eq₁ eq₂
    ; p₁∘universal≈h₁ = p.p₁∘universal≈h₁
    ; p₂∘universal≈h₂ = p.p₂∘universal≈h₂
    }
    where open HomReasoning
          module X = SliceObj X
          module Y = SliceObj Y
          module B = SliceObj B
          module f = Slice⇒ f
          module g = Slice⇒ g
          module p = P.Pullback (pullbacks f.h g.h)
          open MR C

          comm : Y.arr ∘ p.p₂ ≈ X.arr ∘ p.p₁
          comm = begin
            Y.arr ∘ p.p₂         ≈˘⟨ g.△ ⟩∘⟨refl ⟩
            (B.arr ∘ g.h) ∘ p.p₂ ≈˘⟨ pushʳ p.commute ⟩
            B.arr ∘ f.h ∘ p.p₁   ≈⟨ pullˡ f.△ ⟩
            X.arr ∘ p.p₁         ∎

module _ (LCCC : Locally) (t : Terminal) where
  open Locally LCCC
  open Terminal t
  open HomReasoning

  cartesian : Cartesian C
  cartesian = record
    { terminal = t
    ; products = record
      { product = λ {A B} → Pₚ.pullback-⊤⇒product t (product⇒pullback product)
      }
    }
    where open sliceCCC ⊤ using (product)

  private
    module cartesian = Cartesian cartesian

  cartesianClosed : CartesianClosed C
  cartesianClosed = record
    { cartesian = cartesian
    ; exp       = λ {A B} →
      let open Exponential (exp {sliceobj (! {A})} {sliceobj (! {B})})
      in record
      { B^A      = Y B^A
      ; product  =
        -- this is tricky. how product is implemented requires special care. for example, the following
        -- code also gives a product that type checks, but it is impossible to work with.
        -- Pₚ.pullback-⊤⇒product t (Pₚ.pullback-resp-≈ (product⇒pullback product) !-unique₂ refl)
        --
        -- another quirk of proof relevance.
        let open Product (Slice ⊤) (exp.product {sliceobj (! {A})} {sliceobj (! {B})})
        in record
           { A×B      = Y A×B
           ; π₁       = h π₁
           ; π₂       = h π₂
           ; ⟨_,_⟩    = λ f g → h ⟨ slicearr {h = f} (⟺ (!-unique _)) , slicearr {h = g} (⟺ (!-unique _)) ⟩
           ; project₁ = project₁
           ; project₂ = project₂
           ; unique   = λ eq eq′ → unique {h = slicearr (⟺ (!-unique _))} eq eq′
           }
      ; eval     = h eval
      ; λg       = λ {X} p f → h (λg (pullback⇒product′ t (Pₚ.product⇒pullback-⊤ t p)) (lift t f))
      ; β        = λ p → ∘-resp-≈ʳ (exp.product.⟨⟩-cong₂ refl refl) ○ β (pullback⇒product′ t (Pₚ.product⇒pullback-⊤ t p))
      ; λ-unique = λ p eq → λ-unique (pullback⇒product′ t (Pₚ.product⇒pullback-⊤ t p))
                                     {h = slicearr (⟺ (!-unique _))}
                                     (∘-resp-≈ʳ (exp.product.⟨⟩-cong₂ refl refl) ○ eq)
      }
    }
    where open sliceCCC ⊤ using (exp)
          open SliceObj
          open Slice⇒

  finitelyComplete : FinitelyComplete
  finitelyComplete = record
    { cartesian = cartesian
    ; equalizer = λ f g → prods×pullbacks⇒equalizers cartesian.products
                                                     (λ {_ _ X} h i → product⇒pullback (sliceCCC.product X))
    }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; sym; subst)
open import Function.Reasoning

import Data.Empty as Empty
import Data.Maybe as Maybe
import Data.Nat as Nat
import Data.Bool as Bool
import Data.Fin as Fin
import Data.Product as Product
import Data.Vec as Vec
import Data.Vec.Relation.Unary.All as All
import Data.Fin.Properties as Finₚ

open Empty using (⊥; ⊥-elim)
open Nat using (ℕ; zero; suc)
open Fin using (Fin ; zero ; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Product using (_×_; Σ-syntax; ∃-syntax; _,_; proj₁; proj₂)

open import PiCalculus.Syntax
open Scoped
open import PiCalculus.Semantics
open import PiCalculus.Semantics.Properties
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.SubjectReduction (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω
open import PiCalculus.LinearTypeSystem.Framing Ω
open import PiCalculus.LinearTypeSystem.Weakening Ω
open import PiCalculus.LinearTypeSystem.Strengthening Ω
open import PiCalculus.LinearTypeSystem.Substitution Ω
open import PiCalculus.LinearTypeSystem.SubjectCongruence Ω

SubjectReduction : Set
SubjectReduction = {n : ℕ} {γ : PreCtx n} {idxs : Idxs n} {idx : Idx} {Γ Γ' Ξ : Ctx idxs}
                   {c : Channel n} {P Q : Scoped n}
                 → maybe (Γ' ≡ Γ) (λ i → Γ' ∋[ i ] ℓ# {idx} ▹ Γ) c
                 → P =[ c ]⇒ Q
                 → γ ； Γ'  ⊢ P ▹ Ξ
                 → γ ； Γ   ⊢ Q ▹ Ξ

private
  variable
    n : ℕ
    i j : Fin n
    idxs : Idxs n
    P Q : Scoped n

extract-ℓ# : {Γ Ξ Δ Ψ Θ : Ctx idxs} {idx idx' : Idx}
           → Γ ∋[ i ] ℓᵢ {idx} ▹ Ξ
           → Ψ ∋[ i ] ℓₒ {idx'} ▹ Θ
           → Ξ ≔ Δ ⊗ Ψ
           → ∃[ z ] (All.lookup i Γ ≔ ℓ# ∙² z)
extract-ℓ# (zero x) (zero y) (_ , s) =
  let
    ⁇ , Ξ≔ℓₒ∙⁇ , _ = ∙²-assoc (∙²-comm s) y
    _ , Γ≔[ℓᵢℓₒ]∙⁇ , [ℓᵢℓₒ]≔ℓᵢ∙ℓₒ = ∙²-assoc⁻¹ x Ξ≔ℓₒ∙⁇
    ℓ#≡ℓᵢℓₒ = ∙²-unique [ℓᵢℓₒ]≔ℓᵢ∙ℓₒ (∙-idʳ , ∙-idˡ)
  in _ , subst (λ ● → _ ≔ ● ∙² ⁇) ℓ#≡ℓᵢℓₒ Γ≔[ℓᵢℓₒ]∙⁇
extract-ℓ# (suc i) (suc o) (s , _) = extract-ℓ# i o s

-- What we have: Γ' ---ℓᵢ--> Θ ---P--> Ξ ---ℓₒ--> Ψ
-- What we need: Γ' ---ℓ#--> Γ ---P--> Ψ
align : ∀ {i : Fin n} {γ : PreCtx n} {idxs : Idxs n} {Γ' Γ Ξ Θ Ψ : Ctx idxs} {idx' idx'' idx'''}
    → Γ' ∋[ i ] ℓᵢ {idx'} ▹ Θ
    → Ξ  ∋[ i ] ℓₒ {idx''} ▹ Ψ
    → Γ' ∋[ i ] ℓ# {idx'''} ▹ Γ
    → γ ； Θ ⊢ P ▹ Ξ
    → γ ； Γ ⊢ P ▹ Ψ
align i o io ⊢P with ∋-≡Idx io | ∋-≡Idx i | ∋-≡Idx o
align i o io ⊢P | refl | refl | refl =
  let
  Δi , Γ'≔Δi∙Θ , Δi≔ℓᵢ = ∋-⊗ i
  Δo , Ξ≔Δo∙Ψ , Δo≔ℓₒ = ∋-⊗ o
  Δio , Γ'≔Δio∙Γ , Δio≔ℓ# = ∋-⊗ io
  Δ⊢P , Θ≔Δ⊢P∙Ξ = ⊢-⊗ ⊢P
  ΨΔ⊢P , Θ≔Δo∙[ΨΔ⊢P] , ΨΔ⊢P≔Ψ∙Δ⊢P = ⊗-assoc (⊗-comm Θ≔Δ⊢P∙Ξ) Ξ≔Δo∙Ψ
  ΔiΔo , Γ'≔[ΔiΔo]∙[ΨΔ⊢P] , ΔiΔo≔ℓᵢℓₒ = ⊗-assoc⁻¹ Γ'≔Δi∙Θ Θ≔Δo∙[ΨΔ⊢P]
  Δio≔Δi∙Δo = ∙²-⊗ Δio≔ℓ# Δi≔ℓᵢ Δo≔ℓₒ (∙-idʳ , ∙-idˡ)
  ΔiΔo≡Δio = ⊗-unique ΔiΔo≔ℓᵢℓₒ Δio≔Δi∙Δo
  Γ'≔Δio∙[ΨΔ⊢P] = subst (λ ● → _ ≔ ● ⊗ _) ΔiΔo≡Δio Γ'≔[ΔiΔo]∙[ΨΔ⊢P]
  ΨΔ⊢P≡Γ = ⊗-uniqueˡ (⊗-comm Γ'≔Δio∙[ΨΔ⊢P]) (⊗-comm Γ'≔Δio∙Γ)
  Γ≔Ψ∙Δ⊢P = subst (λ ● → ● ≔ _ ⊗ _) ΨΔ⊢P≡Γ ΨΔ⊢P≔Ψ∙Δ⊢P
  in ⊢-frame Θ≔Δ⊢P∙Ξ (⊗-comm Γ≔Ψ∙Δ⊢P) ⊢P

comm-≥ℓ# : {γ : PreCtx n} {Γ Δ : Ctx idxs} {c : Channel n}
      → P =[ c ]⇒ Q → γ ； Γ ⊢ P ▹ Δ → c ≡ external i → ∃[ y ] (All.lookup i Γ ≔ ℓ# ∙² y)
comm-≥ℓ# {i = i} comm (((_ , x) ⦅⦆ ⊢P) ∥ ((_ , x') ⟨ _ ⟩ ⊢Q)) refl with ⊢-⊗ ⊢P
comm-≥ℓ# {i = i} comm (((_ , x) ⦅⦆ ⊢P) ∥ ((_ , x') ⟨ _ ⟩ ⊢Q)) refl | (_ -, _) , (Ξ≔ , _) = extract-ℓ# x x' Ξ≔
comm-≥ℓ# (par P→P') (⊢P ∥ ⊢Q) refl = comm-≥ℓ# P→P' ⊢P refl
comm-≥ℓ# (res_ {c = internal} P→Q) (ν t m μ ⊢P) ()
comm-≥ℓ# (res_ {c = external zero} P→Q) (ν t m μ ⊢P) ()
comm-≥ℓ# (res_ {c = external (suc i)} P→Q) (ν t m μ ⊢P) refl = comm-≥ℓ# P→Q ⊢P refl
comm-≥ℓ# (struct P≅P' P'→Q' P'≅Q ) ⊢P refl = comm-≥ℓ# P'→Q' (subject-cong P≅P' ⊢P) refl

subject-reduction : SubjectReduction
subject-reduction Γ'⇒Γ comm (((_⦅⦆_ {P = P} (tx , x) ⊢P)) ∥ ((tx' , x') ⟨ y ⟩ ⊢Q)) with trans (sym (∋-≡Type tx)) (∋-≡Type tx')
subject-reduction Γ'⇒Γ comm (((_⦅⦆_ {P = P} (tx , x) ⊢P)) ∥ ((tx' , x') ⟨ y ⟩ ⊢Q)) | refl = ⊢P' ∥ ⊢Q
  where ⊢P' = ⊢P
            |> align (suc x) (suc x') (suc Γ'⇒Γ)
            |> ⊢-subst y
            |> ⊢-strengthen zero (subst-unused (λ ()) P)
subject-reduction Γ'⇒Γ (par P→P') (⊢P ∥ ⊢Q) = subject-reduction Γ'⇒Γ P→P' ⊢P ∥ ⊢Q
subject-reduction {idx = idx} refl (res_ {c = internal} P→Q) (ν t m μ ⊢P)
  = ν t m μ (subject-reduction {idx = idx} refl P→Q ⊢P)
subject-reduction refl (res_ {c = external zero} P→Q) (ν t m μ ⊢P)
  = let (lμ' , rμ') , (ls , rs) = comm-≥ℓ# P→Q ⊢P refl
        rs' = subst (λ ● → _ ≔ _ ∙ ●) (∙-uniqueˡ (∙-comm rs) (∙-comm ls)) rs
     in ν t m lμ' (subject-reduction (zero (ls , rs')) P→Q ⊢P)
subject-reduction Γ'⇒Γ (res_ {c = external (suc i)} P→Q) (ν t m μ ⊢P)
  = ν t m μ (subject-reduction (suc Γ'⇒Γ) P→Q ⊢P)
subject-reduction Γ'⇒Γ (struct P≅P' P'→Q' Q'≅Q) ⊢P
  = subject-cong Q'≅Q (subject-reduction Γ'⇒Γ P'→Q' (subject-cong P≅P' ⊢P))

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-# OPTIONS --cubical --no-import-sorts --safe --postfix-projections #-}

open import Cubical.Foundations.Everything renaming (uncurry to λ⟨,⟩_)
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.CartesianKanOps

module Cubical.Modalities.Lex
  (◯ : ∀ {ℓ} → Type ℓ → Type ℓ)
  (η : ∀ {ℓ} {A : Type ℓ} → A → ◯ A)
  (isModal : ∀ {ℓ} → Type ℓ → Type ℓ)
  (let isModalFam = λ {ℓ ℓ′ : Level} {A : Type ℓ} (B : A → Type ℓ′) → (x : A) → isModal (B x))
  (idemp : ∀ {ℓ} {A : Type ℓ} → isModal (◯ A))
  (≡-modal : ∀ {ℓ} {A : Type ℓ} {x y : A} (A-mod : isModal A) → isModal (x ≡ y))
  (◯-ind : ∀ {ℓ ℓ′} {A : Type ℓ} {B : ◯ A → Type ℓ′} (B-mod : isModalFam B) (f : (x : A) → B (η x)) → ([x] : ◯ A) → B [x])
  (◯-ind-β : ∀ {ℓ ℓ′} {A : Type ℓ} {B : ◯ A → Type ℓ′} (B-mod : isModalFam B) (f : (x : A) → B (η x)) (x : A) → ◯-ind B-mod f (η x) ≡ f x)
  (let Type◯ = λ (ℓ : Level) → Σ (Type ℓ) isModal)
  (◯-lex : ∀ {ℓ} → isModal (Type◯ ℓ))
  where

private
  variable
     ℓ ℓ′ : Level

η-at : (A : Type ℓ) → A → ◯ A
η-at _ = η

module _ where
  private
    variable
      A : Type ℓ
      B : Type ℓ′

  module ◯-rec (B-mod : isModal B) (f : A → B) where
    abstract
      ◯-rec : ◯ A → B
      ◯-rec = ◯-ind (λ _ → B-mod) f

      ◯-rec-β : (x : A) → ◯-rec (η x) ≡ f x
      ◯-rec-β = ◯-ind-β (λ _ → B-mod) f

  open ◯-rec

  module ◯-map (f : A → B) where
    abstract
      ◯-map : ◯ A → ◯ B
      ◯-map = ◯-rec idemp λ x → η (f x)

      ◯-map-β : (x : A) → ◯-map (η x) ≡ η (f x)
      ◯-map-β x = ◯-rec-β idemp _ x

open ◯-rec
open ◯-map

module IsModalToUnitIsEquiv (A : Type ℓ) (A-mod : isModal A) where
  abstract
    inv : ◯ A → A
    inv = ◯-rec A-mod λ x → x

    η-retract : retract η inv
    η-retract = ◯-rec-β _ _

    η-section : section η inv
    η-section = ◯-ind (λ _ → ≡-modal idemp) λ x i → η (η-retract x i)

    η-iso : Iso A (◯ A)
    Iso.fun η-iso = η
    Iso.inv η-iso = inv
    Iso.rightInv η-iso = η-section
    Iso.leftInv η-iso = η-retract

    η-is-equiv : isEquiv (η-at A)
    η-is-equiv = isoToIsEquiv η-iso

abstract
  unit-is-equiv-to-is-modal : {A : Type ℓ} → isEquiv (η-at A) → isModal A
  unit-is-equiv-to-is-modal p = transport (cong isModal (sym (ua (η , p)))) idemp

  retract-is-modal
    : {A : Type ℓ} {B : Type ℓ′}
    → (A-mod : isModal A) (f : A → B) (g : B → A) (r : retract g f)
    → isModal B
  retract-is-modal {A = A} {B = B} A-mod f g r =
    unit-is-equiv-to-is-modal (isoToIsEquiv (iso η η-inv η-section η-retract))
    where
      η-inv : ◯ B → B
      η-inv = f ∘ ◯-rec A-mod g

      η-retract : retract η η-inv
      η-retract b = cong f (◯-rec-β A-mod g b) ∙ r b

      η-section : section η η-inv
      η-section = ◯-ind (λ _ → ≡-modal idemp) (cong η ∘ η-retract)

module LiftFam {A : Type ℓ} (B : A → Type ℓ′) where
  module M = IsModalToUnitIsEquiv (Type◯ ℓ′) ◯-lex

  abstract
    ◯-lift-fam : ◯ A → Type◯ ℓ′
    ◯-lift-fam = M.inv ∘ ◯-map (λ a → ◯ (B a) , idemp)

    ⟨◯⟩ : ◯ A → Type ℓ′
    ⟨◯⟩ [a] = ◯-lift-fam [a] .fst

    ⟨◯⟩-modal : isModalFam ⟨◯⟩
    ⟨◯⟩-modal [a] = ◯-lift-fam [a] .snd

    ⟨◯⟩-compute : (x : A) → ⟨◯⟩ (η x) ≡ ◯ (B x)
    ⟨◯⟩-compute x =
      ⟨◯⟩ (η x)
        ≡⟨ cong (fst ∘ M.inv) (◯-map-β _ _) ⟩
      M.inv (η (◯ (B x) , idemp)) .fst
        ≡⟨ cong fst (M.η-retract _) ⟩
      ◯ (B x) ∎

open LiftFam using (⟨◯⟩; ⟨◯⟩-modal; ⟨◯⟩-compute)

module LiftFamExtra {A : Type ℓ} {B : A → Type ℓ′} where
  ⟨◯⟩←◯ : ∀ {a} → ◯ (B a) → ⟨◯⟩ B (η a)
  ⟨◯⟩←◯ = transport (sym (⟨◯⟩-compute B _))

  ⟨◯⟩→◯ : ∀ {a} → ⟨◯⟩ B (η a) → ◯ (B a)
  ⟨◯⟩→◯ = transport (⟨◯⟩-compute B _)

  ⟨η⟩ : ∀ {a} → B a → ⟨◯⟩ B (η a)
  ⟨η⟩ = ⟨◯⟩←◯ ∘ η

  abstract
    ⟨◯⟩→◯-section : ∀ {a} → section (⟨◯⟩→◯ {a}) ⟨◯⟩←◯
    ⟨◯⟩→◯-section = transport⁻Transport (sym (⟨◯⟩-compute  _ _))

module Combinators where
  private
    variable
      ℓ′′ : Level
      A A′ : Type ℓ
      B : A → Type ℓ′
      C : Σ A B → Type ℓ′′

  λ/coe⟨_⟩_ : (p : A ≡ A′) → ((x : A′) → B (coe1→0 (λ i → p i) x)) → ((x : A) → B x)
  λ/coe⟨_⟩_ {B = B} p f = coe1→0 (λ i → (x : p i) → B (coei→0 (λ j → p j) i x)) f

open Combinators

module _ {A : Type ℓ} {B : A → Type ℓ′} where
  abstract
    Π-modal : isModalFam B → isModal ((x : A) → B x)
    Π-modal B-mod = retract-is-modal idemp η-inv η retr
      where
        η-inv : ◯ ((x : A) → B x) → (x : A) → B x
        η-inv [f] x = ◯-rec (B-mod x) (λ f → f x) [f]

        retr : retract η η-inv
        retr f = funExt λ x → ◯-rec-β (B-mod x) _ f

    Σ-modal : isModal A → isModalFam B → isModal (Σ A B)
    Σ-modal A-mod B-mod = retract-is-modal idemp η-inv η retr
      where
        h : ◯ (Σ A B) → A
        h = ◯-rec A-mod fst

        h-β : (x : Σ A B) → h (η x) ≡ fst x
        h-β = ◯-rec-β A-mod fst

        f : (i : I) (x : Σ A B) → B (h-β x i)
        f i x = coe1→i (λ j → B (h-β x j)) i (snd x)

        η-inv : ◯ (Σ A B) → Σ A B
        η-inv y = h y , ◯-ind (B-mod ∘ h) (f i0) y

        retr : (p : Σ A B) → η-inv (η p) ≡ p
        retr p =
          η-inv (η p)
            ≡⟨ ΣPathP (refl , ◯-ind-β _ _ _) ⟩
          h (η p) , f i0 p
            ≡⟨ ΣPathP (h-β _ , λ i → f i p) ⟩
          p ∎

module Σ-commute {A : Type ℓ} (B : A → Type ℓ′) where
  open LiftFamExtra

  ◯Σ = ◯ (Σ A B)

  module Σ◯ where
    Σ◯ = Σ (◯ A) (⟨◯⟩ B)
    abstract
      Σ◯-modal : isModal Σ◯
      Σ◯-modal = Σ-modal idemp (⟨◯⟩-modal _)

  open Σ◯

  η-Σ◯ : Σ A B → Σ◯
  η-Σ◯ (x , y) = η x , ⟨η⟩ y

  module Push where
    abstract
      fun : ◯Σ → Σ◯
      fun = ◯-rec Σ◯-modal η-Σ◯

      compute : fun ∘ η ≡ η-Σ◯
      compute = funExt (◯-rec-β _ _)

  module Unpush where
    abstract
      fun : Σ◯ → ◯Σ
      fun =
        λ⟨,⟩ ◯-ind (λ _ → Π-modal λ _ → idemp) λ x →
        λ/coe⟨ ⟨◯⟩-compute B x ⟩ ◯-map (x ,_)

      compute : fun ∘ η-Σ◯ ≡ η
      compute =
        funExt λ p →
        fun (η-Σ◯ p)
          ≡⟨ funExt⁻ (◯-ind-β _ _ _) _ ⟩
        transport refl (◯-map _ _)
          ≡⟨ transportRefl _ ⟩
        ◯-map _ (⟨◯⟩→◯ (⟨η⟩ _))
          ≡⟨ cong (◯-map _) (⟨◯⟩→◯-section _) ⟩
        ◯-map _ (η _)
          ≡⟨ ◯-map-β _ _ ⟩
        η p ∎

  push-unpush-compute : Push.fun ∘ Unpush.fun ∘ η-Σ◯ ≡ η-Σ◯
  push-unpush-compute =
    Push.fun ∘ Unpush.fun ∘ η-Σ◯
      ≡⟨ cong (Push.fun ∘_) Unpush.compute ⟩
    Push.fun ∘ η
      ≡⟨ Push.compute ⟩
    η-Σ◯ ∎

  unpush-push-compute : Unpush.fun ∘ Push.fun ∘ η ≡ η
  unpush-push-compute =
    Unpush.fun ∘ Push.fun ∘ η
      ≡⟨ cong (Unpush.fun ∘_) Push.compute ⟩
    Unpush.fun ∘ η-Σ◯
      ≡⟨ Unpush.compute ⟩
    η ∎

  is-section : section Unpush.fun Push.fun
  is-section = ◯-ind (λ x → ≡-modal idemp) λ x i → unpush-push-compute i x

  is-retract : retract Unpush.fun Push.fun
  is-retract =
    λ⟨,⟩ ◯-ind (λ _ → Π-modal λ _ → ≡-modal Σ◯-modal) λ x →
    λ/coe⟨ ⟨◯⟩-compute B x ⟩
     ◯-ind
      (λ _ → ≡-modal Σ◯-modal)
      (λ y i → push-unpush-compute i (x , y))

  push-sg-is-equiv : isEquiv Push.fun
  push-sg-is-equiv = isoToIsEquiv (iso Push.fun Unpush.fun is-retract is-section)

isConnected : Type ℓ → Type ℓ
isConnected A = isContr (◯ A)

module FormalDiskBundle {A : Type ℓ} where
  𝔻 : A → Type ℓ
  𝔻 a = Σ[ x ∈ A ] η a ≡ η x

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- Higher lenses, defined using the requirement that the remainder
-- function should be surjective
------------------------------------------------------------------------

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

import Equality.Path as P

module Lens.Non-dependent.Higher.Surjective-remainder
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq hiding (univ)
open import Equivalence equality-with-J as Eq using (_≃_; Is-equivalence)
open import Function-universe equality-with-J as F
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher eq as Higher

private
  variable
    a b : Level
    A B : Set a

-- A variant of the lenses defined in Lens.Non-dependent.Higher. In
-- this definition the function called inhabited is replaced by a
-- requirement that the remainder function should be surjective.

Lens : Set a → Set b → Set (lsuc (a ⊔ b))
Lens {a = a} {b = b} A B =
  ∃ λ (get       : A → B) →
  ∃ λ (R         : Set (a ⊔ b)) →
  ∃ λ (remainder : A → R) →
    Is-equivalence (λ a → remainder a , get a) ×
    Surjective remainder

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = λ (get , _) → get
    ; set = λ (_ , _ , rem , equiv , _) a b →
              _≃_.from Eq.⟨ _ , equiv ⟩ (rem a , b)
    }

-- Higher.Lens A B is isomorphic to Lens A B.

Higher-lens↔Lens : Higher.Lens A B ↔ Lens A B
Higher-lens↔Lens {A = A} {B = B} =

  Higher.Lens A B                                         ↝⟨ Higher.Lens-as-Σ ⟩

  (∃ λ (R : Set _) →
     (A ≃ (R × B)) ×
     (R → ∥ B ∥))                                         ↝⟨ (∃-cong λ _ → Eq.≃-as-Σ ×-cong F.id) ⟩

  (∃ λ (R : Set _) →
     (∃ λ (f : A → R × B) → Eq.Is-equivalence f) ×
     (R → ∥ B ∥))                                         ↝⟨ (∃-cong λ _ → inverse Σ-assoc) ⟩

  (∃ λ (R : Set _) →
   ∃ λ (f : A → R × B) →
     Eq.Is-equivalence f ×
     (R → ∥ B ∥))                                         ↝⟨ (∃-cong λ _ → Σ-cong ΠΣ-comm λ _ → F.id) ⟩

  (∃ λ (R  : Set _) →
   ∃ λ (rg : (A → R) × (A → B)) →
     Eq.Is-equivalence (λ a → proj₁ rg a , proj₂ rg a) ×
     (R → ∥ B ∥))                                         ↝⟨ (∃-cong λ _ → inverse Σ-assoc) ⟩

  (∃ λ (R         : Set _) →
   ∃ λ (remainder : A → R) →
   ∃ λ (get       : A → B) →
     Eq.Is-equivalence (λ a → remainder a , get a) ×
     (R → ∥ B ∥))                                         ↝⟨ (∃-cong λ _ → ∃-comm) ⟩

  (∃ λ (R         : Set _) →
   ∃ λ (get       : A → B) →
   ∃ λ (remainder : A → R) →
     Eq.Is-equivalence (λ a → remainder a , get a) ×
     (R → ∥ B ∥))                                         ↝⟨ ∃-comm ⟩

  (∃ λ (get       : A → B) →
   ∃ λ (R         : Set _) →
   ∃ λ (remainder : A → R) →
     Eq.Is-equivalence (λ a → remainder a , get a) ×
     (R → ∥ B ∥))                                         ↝⟨ (∃-cong λ get → ∃-cong λ R → ∃-cong λ rem → ∃-cong λ eq →
                                                              ∀-cong ext λ _ → ∥∥-cong $
                                                              lemma get R rem eq _) ⟩□
  (∃ λ (get       : A → B) →
   ∃ λ (R         : Set _) →
   ∃ λ (remainder : A → R) →
     Eq.Is-equivalence (λ a → remainder a , get a) ×
     Surjective remainder)                                □

  where
  lemma : ∀ _ _ _ _ _ → _
  lemma = λ _ _ remainder eq r →
    B                            ↝⟨ (inverse $ drop-⊤-right λ _ →
                                     _⇔_.to contractible⇔↔⊤ $
                                     singleton-contractible _) ⟩
    B × Singleton r              ↝⟨ Σ-assoc ⟩
    (∃ λ { (_ , r′) → r′ ≡ r })  ↝⟨ (Σ-cong ×-comm λ _ → F.id) ⟩
    (∃ λ { (r′ , _) → r′ ≡ r })  ↝⟨ (inverse $ Σ-cong Eq.⟨ _ , eq ⟩ λ _ → F.id) ⟩□
    (∃ λ a → remainder a ≡ r)    □

-- The isomorphism preserves getters and setters.

Higher-lens↔Lens-preserves-getters-and-setters :
  Preserves-getters-and-setters-⇔ A B
    (_↔_.logical-equivalence Higher-lens↔Lens)
Higher-lens↔Lens-preserves-getters-and-setters =
  Preserves-getters-and-setters-→-↠-⇔
    (_↔_.surjection Higher-lens↔Lens)
    (λ _ → refl _ , refl _)

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


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

open import Cubical.Algebra.Base public
open import Cubical.Algebra.Definitions public

open import Cubical.Algebra.Structures public using (IsMonoid; ismonoid)
open import Cubical.Algebra.Bundles public using (Monoid; mkmonoid; MonoidCarrier)
open import Cubical.Structures.Carrier public

open import Cubical.Algebra.Monoid.Properties public
open import Cubical.Algebra.Monoid.Morphism public
open import Cubical.Algebra.Monoid.MorphismProperties public hiding (isPropIsMonoid)


text:
open import Type
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)

-- Finite sets represented by lists
module Data.List.Relation.Membership {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T)⦄ where

open import Data.List
open import Data.List.Relation.Quantification using (ExistsElement ; ExistsUniqueElement)
open import Functional
open import Logic

_∈_ : T → List(T) → Stmt
_∈_ = ExistsElement ∘ (_≡ₑ_)
module _∈_ where
  pattern use  {x}{l} px = ExistsElement.•_ {x = x}{l = l} px
  pattern skip {x}{l} el = ExistsElement.⊰_ {l = l}{x = x} el

open _∈_ public
open import Relator.Sets(_∈_) public

_∈!_ : T → List(T) → Stmt
_∈!_ = ExistsUniqueElement ∘ (_≡ₑ_)


text:
module CS410-Nat where

open import CS410-Prelude
open import CS410-Monoid

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}
{-# COMPILED_DATA Nat HaskellSetup.Nat HaskellSetup.Zero HaskellSetup.Suc #-}

_+N_ : Nat -> Nat -> Nat
zero  +N n = n
suc m +N n = suc (m +N n)
infixr 3 _+N_

+Mon : Monoid Nat
+Mon = record
  { e = 0
  ; op = _+N_
  ; lunit = \ m -> refl
  ; runit = ruHelp
  ; assoc = asHelp
  } where
    ruHelp : (m : Nat) -> m +N 0 == m
    ruHelp zero     = refl
    ruHelp (suc m)  rewrite ruHelp m = refl
    asHelp : (m m' m'' : Nat) -> m +N (m' +N m'') == (m +N m') +N m''
    asHelp zero m' m'' = refl
    asHelp (suc m) m' m'' rewrite asHelp m m' m'' = refl

_*N_ : Nat -> Nat -> Nat
zero  *N n = zero
suc m *N n = m *N n +N n
infixr 4 _*N_

_N>=_ : Nat -> Nat -> Set
m      N>=  zero   =  One
zero   N>=  suc n  =  Zero
suc m  N>=  suc n  =  m N>= n

N>=Unique : (m n : Nat)(p q : m N>= n) -> p == q
N>=Unique m zero p q = refl
N>=Unique zero (suc n) () q
N>=Unique (suc m) (suc n) p q = N>=Unique m n p q

plusSucFact : (m n : Nat) -> m +N suc n == suc m +N n
plusSucFact zero n = refl
plusSucFact (suc m) n rewrite plusSucFact m n = refl

plusCommFact : (m n : Nat) -> m +N n == n +N m
plusCommFact m zero = Monoid.runit +Mon m
plusCommFact m (suc n) rewrite plusSucFact m n | plusCommFact m n = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Data.List.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
------------------------------------------------------------------------

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

module Data.List.Membership.Propositional {a} {A : Set a} where

open import Data.List.Relation.Unary.Any using (Any)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; setoid; subst)

import Data.List.Membership.Setoid as SetoidMembership

------------------------------------------------------------------------
-- Re-export contents of setoid membership

open SetoidMembership (setoid A) public hiding (lose)

------------------------------------------------------------------------
-- Different members

_≢∈_ : ∀ {x y : A} {xs} → x ∈ xs → y ∈ xs → Set _
_≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs

------------------------------------------------------------------------
-- Other operations

lose : ∀ {p} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
lose = SetoidMembership.lose (setoid A) (subst _)


text:
{-

This is the Agda formalization of

      NOTIONS OF ANONYMOUS EXISTENCE IN MARTIN-LOF TYPE THEORY

                              by

Nicolai Kraus, Martin Escardo, Thierry Coquand, Thorsten Altenkirch

This file stays very close to the article. Because of this, not all
proofs are given in the way that is most elegant for a formalization.
In fact, often re-ordering statements would lead to a shorter
presentation. The order that we have chosen in the article makes our
results, as we hope, understandable and gives sufficient motivation.

This file type check with Agda 2.4.2.5.
-}

module INDEX_NotionsOfAnonymousExistence where

-- We use the following library files:

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.types.Pi
open import library.types.Bool
open import library.NType2
open import library.types.Paths

-- OUR FORMALIZATION

-- Section 1: Introduction
-- (no formalization)

-- Section 2: Preliminaries
open import Sec2preliminaries

-- Section 3: Hedberg's Theorem
open import Sec3hedberg

-- Section 4: Collapsibility implies H-Stability
open import Sec4hasConstToSplit

-- Section 5: Factorizing Weakly Constant Functions
open import Sec5factorConst

-- Section 6: Populatedness
open import Sec6populatedness

-- Section 7: Taboos and Counter-Models
open import Sec7taboos

-- Section 8: Propositional Truncation with Judgmental Computation Rule
open import Sec8judgmentalBeta

-- Section 9: Conclusion and Open Problems
-- (no formalization)

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --safe --no-qualified-instances #-}
module CF.Transform.Compile.Statements where

open import Function using (_∘_)
open import Data.Unit using (⊤; tt)
open import Data.Product
open import Data.List hiding (null; [_])
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad

open import CF.Syntax.DeBruijn
open import CF.Transform.Compile.Expressions
open import CF.Types
open import CF.Transform.Compile.ToJVM

open import JVM.Types
open import JVM.Compiler
open import JVM.Contexts
open import JVM.Model StackTy
open import JVM.Syntax.Values
open import JVM.Syntax.Instructions

mutual
  {- Compiling statements -}
  compileₛ : ∀ {ψ : StackTy} {Γ r} → Stmt r Γ → ε[ Compiler ⟦ Γ ⟧ ψ ψ Emp  ]

  compileₛ (asgn x e) = do
    compileₑ e
    code (store ⟦ x ⟧)

  compileₛ (run e) = do
    compileₑ e
    code pop

  compileₛ (block x) = do
    compiler _ x

  compileₛ (while e body) = do
    -- condition
    lcond⁺ ∙⟨ σ ⟩ lcond⁻    ← freshLabel
    refl ∙⟨ σ ⟩ lcond⁻      ← attachTo lcond⁺ ⟨ ∙-idʳ ⟩ compileₑ e ⟨ Down _ # σ ⟩& lcond⁻
    (↓ lend⁻) ∙⟨ σ ⟩ labels ← (✴-rotateₗ ∘ ✴-assocᵣ) ⟨$⟩ (freshLabel ⟨ Down _ # σ ⟩& lcond⁻)
    (↓ lcond⁻) ∙⟨ σ ⟩ lend⁺ ← ✴-id⁻ˡ ⟨$⟩ (code (if eq lend⁻) ⟨ _ ✴ _  # σ ⟩& labels)

    -- body
    compileₛ body
    lend⁺                   ← ✴-id⁻ˡ ⟨$⟩ (code (goto lcond⁻) ⟨ Up _   # σ ⟩& lend⁺)
    attach lend⁺

  compileₛ (ifthenelse c e₁ e₂) = do
    -- condition
    compileₑ c
    lthen+ ∙⟨ σ ⟩ ↓ lthen-  ← freshLabel
    lthen+                  ← ✴-id⁻ˡ ⟨$⟩ (code (if ne lthen-) ⟨ Up _  # ∙-comm σ     ⟩& lthen+)

    -- else
    compileₛ e₂
    ↓ lend- ∙⟨ σ ⟩ labels   ← (✴-rotateₗ ∘ ✴-assocᵣ) ⟨$⟩ (freshLabel ⟨ Up _  # ∙-idˡ        ⟩& lthen+)

    -- then
    lthen+ ∙⟨ σ ⟩ lend+     ← ✴-id⁻ˡ ⟨$⟩ (code (goto lend-) ⟨ _ ✴ _ # σ ⟩& labels)
    lend+                   ← ✴-id⁻ˡ ⟨$⟩ (attach lthen+ ⟨ Up _  # σ ⟩& lend+)
    compileₛ e₁

    -- label the end
    attach lend+

  {- Compiling blocks -}
  compiler : ∀ (ψ : StackTy) {Γ r} → Block r Γ → ε[ Compiler ⟦ Γ ⟧ ψ ψ Emp ]

  compiler ψ (nil) = do
    return refl

  compiler ψ (s ⍮⍮ b) = do
    compileₛ s
    compiler _ b


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Hash
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap as KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Base.Types

open import Data.String using (String)

-- Defines the types that /DO NOT/ depend on an epoch config.
-- TODO-3: update types to reflect more recent version of LibraBFT.  This is
-- a substantial undertaking that should probably be led by someone who can
-- access our internal implementation.
module LibraBFT.Impl.Consensus.Types.EpochIndep where
  -- Below here is incremental progress towards something
  -- that will eventually mirror the types in LBFT.Consensus.Types
  -- that /DO NOT/ depend on the set of active authors
  -- or safety rules, which we call the /EpochConfig/.

  Author : Set
  Author = NodeId

  AccountAddress : Set
  AccountAddress = Author

  HashValue : Set
  HashValue = Hash

  TX : Set
  TX = ByteString

  Instant : Set
  Instant = ℕ   -- TODO-2: should eventually be a time stamp

  -----------------
  -- Information --
  -----------------

  record BlockInfo : Set where
    constructor BlockInfo∙new
    field
      ₋biEpoch : Epoch
      ₋biRound : Round
      ₋biId    : HashValue
      -- This has more fields...
  open BlockInfo public
  unquoteDecl biEpoch   biRound   biId = mkLens (quote BlockInfo)
             (biEpoch ∷ biRound ∷ biId ∷ [])
  postulate instance enc-BlockInfo : Encoder BlockInfo

  BlockInfo-η : ∀{e1 e2 r1 r2 i1 i2} → e1 ≡ e2 → r1 ≡ r2 → i1 ≡ i2
              → BlockInfo∙new e1 r1 i1 ≡ BlockInfo∙new e2 r2 i2
  BlockInfo-η refl refl refl = refl

  record LedgerInfo : Set where
    constructor LedgerInfo∙new
    field
      ₋liCommitInfo        : BlockInfo
      ₋liConsensusDataHash : HashValue
  open LedgerInfo public
  unquoteDecl liCommitInfo   liConsensusDataHash = mkLens (quote LedgerInfo)
             (liCommitInfo ∷ liConsensusDataHash ∷ [])
  postulate instance enc-LedgerInfo : Encoder LedgerInfo

  LedgerInfo-η : ∀ {ci1 ci2 : BlockInfo} {cdh1 cdh2 : Hash}
             → ci1  ≡ ci2
             → cdh1 ≡ cdh2
             → (LedgerInfo∙new ci1 cdh1) ≡ (LedgerInfo∙new ci2 cdh2)
  LedgerInfo-η refl refl = refl

  record LedgerInfoWithSignatures : Set where
    constructor LedgerInfoWithSignatures∙new
    field
      ₋liwsLedgerInfo : LedgerInfo
      ₋liwsSignatures : KVMap Author Signature
  open LedgerInfoWithSignatures public
  unquoteDecl liwsLedgerInfo   liwsSignatures = mkLens (quote LedgerInfoWithSignatures)
             (liwsLedgerInfo ∷ liwsSignatures ∷ [])
  postulate instance enc-LedgerInfoWithSignatures : Encoder LedgerInfoWithSignatures

  -------------------
  -- Votes and QCs --
  -------------------

  record VoteData : Set where
    constructor VoteData∙new
    field
      ₋vdProposed : BlockInfo
      ₋vdParent   : BlockInfo
  open VoteData public
  unquoteDecl vdProposed   vdParent = mkLens (quote VoteData)
             (vdProposed ∷ vdParent ∷ [])
  postulate instance enc-VoteData : Encoder VoteData

  VoteData-η : ∀ {pr1 par1 pr2 par2 : BlockInfo} → pr1  ≡ pr2 → par1 ≡ par2
             → (VoteData∙new pr1 par1) ≡ (VoteData∙new pr2 par2)
  VoteData-η refl refl = refl

  -- DESIGN NOTE: The ₋vAuthor field is included only to facilitate lookup of the public key against
  -- which to verify the signature.  An alternative would be to use an index into the members of the
  -- epoch config, which would save message space and therefore bandwidth.

  record Vote : Set where
    constructor Vote∙new
    field
      ₋vVoteData         : VoteData
      ₋vAuthor           : Author
      ₋vLedgerInfo       : LedgerInfo
      ₋vSignature        : Signature
      ₋vTimeoutSignature : Maybe Signature
  open Vote public
  unquoteDecl vVoteData   vAuthor   vLedgerInfo   vSignature   vTimeoutSignature = mkLens (quote Vote)
             (vVoteData ∷ vAuthor ∷ vLedgerInfo ∷ vSignature ∷ vTimeoutSignature ∷ [])
  postulate instance enc-Vote     : Encoder Vote

  vParent : Lens Vote BlockInfo
  vParent = vVoteData ∙ vdParent

  vProposed : Lens Vote BlockInfo
  vProposed = vVoteData ∙ vdProposed

  vParentId : Lens Vote Hash
  vParentId = vVoteData ∙ vdParent ∙ biId

  vParentRound : Lens Vote Round
  vParentRound = vVoteData ∙ vdParent ∙ biRound

  vProposedId : Lens Vote Hash
  vProposedId = vVoteData ∙ vdProposed ∙ biId

  vEpoch : Lens Vote Epoch
  vEpoch = vVoteData ∙ vdProposed ∙ biEpoch

  vdRound : Lens VoteData Round
  vdRound = vdProposed ∙ biRound

  vRound : Lens Vote Round
  vRound = vVoteData ∙ vdRound

  record QuorumCert : Set where
    constructor QuorumCert∙new
    field
      ₋qcVoteData         : VoteData
      ₋qcSignedLedgerInfo : LedgerInfoWithSignatures
  open QuorumCert public
  unquoteDecl qcVoteData   qcSignedLedgerInfo = mkLens (quote QuorumCert)
             (qcVoteData ∷ qcSignedLedgerInfo ∷ [])
  postulate instance enc-QuorumCert : Encoder QuorumCert

  -- Because QuorumCert has an injective encoding (postulated, for now),
  -- we can use it to determine equality of QuorumCerts.
  _≟QC_ : (q1 q2 : QuorumCert) → Dec (q1 ≡ q2)
  _≟QC_ = ≡-Encoder enc-QuorumCert

  _QCBoolEq_ : QuorumCert → QuorumCert → Bool
  _QCBoolEq_ q1 q2 = does (q1 ≟QC q2)

  qcCertifiedBlock : Lens QuorumCert BlockInfo
  qcCertifiedBlock = qcVoteData ∙ vdProposed

  -- Constructs a 'vote' that was gathered in a QC.
  rebuildVote : QuorumCert → Author × Signature → Vote
  rebuildVote qc (α , sig)
    = record { ₋vVoteData         = ₋qcVoteData qc
             ; ₋vAuthor           = α
             ; ₋vLedgerInfo       = qc ^∙ (qcSignedLedgerInfo ∙ liwsLedgerInfo)
             ; ₋vSignature        = sig
             ; ₋vTimeoutSignature = nothing -- Is this correct?  The original vote may have had a
                                            -- timeout signature, but we don't know.  Does it
                                            -- matter?
             }

  -- Two votes are equivalent if they are identical except they may differ on timeout signature
  _≈Vote_ : (v1 v2 : Vote) → Set
  v1 ≈Vote v2 = v2 ≡ record v1 { ₋vTimeoutSignature = ₋vTimeoutSignature v2 }

  qcVotesKV : QuorumCert → KVMap Author Signature
  qcVotesKV = ₋liwsSignatures ∘ ₋qcSignedLedgerInfo

  qcVotes : QuorumCert → List (Author × Signature)
  qcVotes qc = kvm-toList (qcVotesKV qc)

  qcCertifies : Lens QuorumCert  Hash
  qcCertifies = qcVoteData ∙ vdProposed ∙ biId

  qcRound : Lens QuorumCert Round
  qcRound = qcVoteData ∙ vdProposed ∙ biRound

  ₋qcCertifies : QuorumCert → Hash
  ₋qcCertifies q = q ^∙ qcCertifies

  ₋qcRound : QuorumCert → Round
  ₋qcRound q = q ^∙ qcRound

  ------------
  -- Blocks --
  ------------

  data BlockType : Set where
    Proposal : TX → Author → BlockType
    NilBlock : BlockType
    Genesis  : BlockType
  postulate instance enc-BlockType : Encoder BlockType

  record BlockData : Set where
    constructor BlockData∙new
    field
      ₋bdEpoch      : Epoch
      ₋bdRound      : Round
      -- QUESTION: How do we represent a block that extends the
      -- genesis block, which doesn't come with a QC.  Maybe the
      -- genesis block has an associated QC established for the epoch?
      ₋bdQuorumCert : QuorumCert
      ₋bdBlockType  : BlockType
  open BlockData public
  unquoteDecl bdEpoch   bdRound   bdQuorumCert   bdBlockType = mkLens (quote BlockData)
             (bdEpoch ∷ bdRound ∷ bdQuorumCert ∷ bdBlockType ∷ [])
  postulate instance enc-BlockData : Encoder BlockData

  bdParentId : Lens BlockData Hash
  bdParentId = bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId

  -- This is the id of a block
  bdBlockId : Lens BlockData Hash
  bdBlockId = bdQuorumCert ∙ qcVoteData ∙ vdProposed ∙ biId

  -- The signature is a Maybe to allow us to use 'nothing' as the
  -- 'bSignature' when constructing a block to sign later.  Also,
  -- "nil" blocks are not signed because they are produced
  -- independently by different validators.  This is to enable
  -- committing after an epoch-changing command is processed: we
  -- cannot add more commands, but we need to add some quorum
  -- certificates in order to commit the epoch-changing command.
  record Block : Set where
    constructor Block∙new
    field
      ₋bId        : HashValue
      ₋bBlockData : BlockData
      ₋bSignature : Maybe Signature
  open Block public
  unquoteDecl bId   bBlockData   bSignature = mkLens (quote Block)
             (bId ∷ bBlockData ∷ bSignature ∷ [])

  postulate instance enc : Encoder Block

  bQuorumCert : Lens Block QuorumCert
  bQuorumCert  = bBlockData ∙ bdQuorumCert

  bRound : Lens Block Round
  bRound =  bBlockData ∙ bdRound

  record SyncInfo : Set where
    constructor mkSyncInfo -- Bare constructor to enable pattern matching against SyncInfo; "smart"
                           -- constructor SyncInfo∙new is below
    field
      ₋siHighestQuorumCert  : QuorumCert
      ₋siHighestCommitCert  : Maybe QuorumCert
      -- ₋siHighestTimeoutCert : Mabe TimeoutCert -- Not used yet.
  open SyncInfo public
  -- Note that we do not automatically derive a lens for siHighestCommitCert;
  -- it is defined manually below.
  unquoteDecl siHighestQuorumCert   = mkLens (quote SyncInfo)
             (siHighestQuorumCert ∷ [])
  postulate instance enc-SyncInfo : Encoder SyncInfo

  SyncInfo∙new : QuorumCert → QuorumCert → SyncInfo
  SyncInfo∙new highestQuorumCert highestCommitCert =
    record { ₋siHighestQuorumCert = highestQuorumCert
           ; ₋siHighestCommitCert = if highestQuorumCert QCBoolEq highestCommitCert
                                    then nothing else (just highestCommitCert) }

  siHighestCommitCert : Lens SyncInfo QuorumCert
  siHighestCommitCert = mkLens' (λ x → fromMaybe (x ^∙ siHighestQuorumCert) (₋siHighestCommitCert x))
                                (λ x si → record x { ₋siHighestCommitCert = just si })

  ----------------------
  -- Network Messages --
  ----------------------

  record ProposalMsg : Set where
    constructor ProposalMsg∙new
    field
      ₋pmProposal : Block
      ₋pmSyncInfo : SyncInfo
  open ProposalMsg public
  unquoteDecl pmProposal   pmSyncInfo = mkLens (quote ProposalMsg)
             (pmProposal ∷ pmSyncInfo ∷ [])
  postulate instance enc-ProposalMsg : Encoder ProposalMsg

  record VoteMsg : Set where
    constructor  VoteMsg∙new
    field
      ₋vmVote     : Vote
      ₋vmSyncInfo : SyncInfo
  open VoteMsg public
  unquoteDecl vmVote   vmSyncInfo = mkLens (quote VoteMsg)
             (vmVote ∷ vmSyncInfo ∷ [])
  postulate instance enc-VoteMsg : Encoder VoteMsg

  vmProposed : Lens VoteMsg BlockInfo
  vmProposed = vmVote ∙ vVoteData ∙ vdProposed

  vmParent : Lens VoteMsg BlockInfo
  vmParent = vmVote ∙ vVoteData ∙ vdParent

  -- This is a notification of a commit.  It may not be explicitly included in an implementation,
  -- but we need something to be able to express correctness conditions.  It will
  -- probably have something different in it, but will serve the purpose for now.
  record CommitMsg : Set where
    constructor CommitMsg∙new
    field
      ₋cmEpoch   : Epoch
      ₋cmAuthor  : NodeId
      ₋cmRound   : Round
      ₋cmCert    : QuorumCert  -- We assume for now that a CommitMsg contains the QuorumCert of the head of the 3-chain
      ₋cmSigMB   : Maybe Signature
  open CommitMsg public
  unquoteDecl cmEpoch   cmAuthor   cmRound   cmCert   cmSigMB = mkLens (quote CommitMsg)
             (cmEpoch ∷ cmAuthor ∷ cmRound ∷ cmCert ∷ cmSigMB ∷ [])
  postulate instance enc-CommitMsg : Encoder CommitMsg

  record LastVoteInfo : Set where
    constructor LastVoteInfo∙new
    field
      ₋lviLiDigest  : HashValue
      ₋lviRound     : Round
      ₋lviIsTimeout : Bool
  open LastVoteInfo public

  record PendingVotes : Set where
    constructor PendingVotes∙new
    field
      ₋pvLiDigestToVotes   : KVMap HashValue LedgerInfoWithSignatures
      -- -pvMaybePartialTC : Maybe TimeoutCertificate
      ₋pvAuthorToVote      : KVMap Author Vote
  open PendingVotes public

  -- Note: this is a placeholder.
  -- We are not concerned for now with executing transactions, just ordering/committing them.
  -- This is outdated (see comment at top).
  data StateComputeResult : Set where
    stateComputeResult : StateComputeResult

  record ExecutedBlock : Set where
    constructor ExecutedBlock∙new
    field
      ₋ebBlock  : Block
      ₋ebOutput : StateComputeResult
  open ExecutedBlock public
  unquoteDecl ebBlock   ebOutput = mkLens (quote ExecutedBlock)
             (ebBlock ∷ ebOutput ∷ [])

  ebId : Lens ExecutedBlock HashValue
  ebId = ebBlock ∙ bId

  ebQuorumCert : Lens ExecutedBlock QuorumCert
  ebQuorumCert = ebBlock ∙ bQuorumCert

  ebParentId : Lens ExecutedBlock HashValue
  ebParentId = ebQuorumCert ∙ qcCertifiedBlock ∙ biId

  ebRound : Lens ExecutedBlock Round
  ebRound = ebBlock ∙ bRound

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

  record LinkableBlock : Set where
    constructor LinkableBlock₋new
    field
      ₋lbExecutedBlock : ExecutedBlock
      -- ₋lbChildren      : Set HashValue
  open LinkableBlock public
  unquoteDecl lbExecutedBlock = mkLens (quote LinkableBlock)
             (lbExecutedBlock ∷ [])

  lbId : Lens LinkableBlock HashValue
  lbId = lbExecutedBlock ∙ ebId

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

  -- Note BlockTree and BlockStore are defined in EpochDep.agda as they depend on an EpochConfig

  record SafetyData : Set where
    constructor SafetyData∙new
    field
      :sdEpoch          : Epoch
      :sdLastVotedRound : Round
      :sdPreferredRound : Round
      :sdLastVote       : Maybe Vote
  open SafetyData public
  unquoteDecl sdEpoch sdLastVotedRound sdPreferredRound sdLastVote =
    mkLens (quote SafetyData)
    (sdEpoch ∷ sdLastVotedRound ∷ sdPreferredRound ∷ sdLastVote ∷  [])

  record PersistentSafetyStorage : Set where
    constructor PersistentSafetyStorage∙new
    field
      :pssSafetyData : SafetyData
      :pssAuthor     : Author
      -- :pssWaypoint : Waypoint
  open PersistentSafetyStorage public
  unquoteDecl pssSafetyData pssAuthor = mkLens (quote PersistentSafetyStorage)
    (pssSafetyData ∷ pssAuthor ∷ [])

  record ValidatorSigner : Set where
    constructor ValidatorSigner∙new
    field
      :vsAuthor     : AccountAddress
      -- :vsPrivateKey : SK   -- Note that the SystemModel doesn't
                              -- allow one node to examine another's
                              -- state, so we don't model someone being
                              -- able to impersonate someone else unless
                              -- PK is "dishonest", which models the
                              -- possibility that the corresponding secret
                              -- key may have been leaked.
  open ValidatorSigner public

  record ValidatorConfig : Set where
    constructor ValidatorConfig∙new
    field
     :vcConsensusPublicKey : PK
  open ValidatorConfig public
  unquoteDecl vcConsensusPublicKey = mkLens (quote ValidatorConfig)
    (vcConsensusPublicKey ∷ [])

  record ValidatorInfo : Set where
    constructor ValidatorInfo∙new
    field
      -- :viAccountAddress       : AccountAddress
      -- :viConsensusVotingPower : Int -- TODO-2: Each validator has one vote. Generalize later.
      :viConfig : ValidatorConfig
  open ValidatorInfo public

  record ValidatorConsensusInfo : Set where
    constructor ValidatorConsensusInfo∙new
    field
     :vciPublicKey   : PK
     --:vciVotingPower : U64
  open ValidatorConsensusInfo public

  record ValidatorVerifier : Set where
    constructor ValidatorVerifier∙new
    field
      :vvAddressToValidatorInfo : (KVMap AccountAddress ValidatorConsensusInfo)
      :vvQuorumVotingPower      : ℕ  -- TODO-2: see above; for now, this is QuorumSize
      -- :vvTotalVotingPower    : ℕ  -- TODO-2: see above; for now, this is number of peers in EpochConfig
  open ValidatorVerifier public
  unquoteDecl vvAddressToValidatorInfo vvQuorumVotingPower = mkLens
    (quote ValidatorVerifier)
    (vvAddressToValidatorInfo ∷ vvQuorumVotingPower ∷ [])

  record SafetyRules : Set where
    constructor SafetyRules∙new
    field
      :srPersistentStorage : PersistentSafetyStorage
      -- :srValidatorSigner   : Maybe ValidatorSigner
  open SafetyRules public
  unquoteDecl srPersistentStorage = mkLens (quote SafetyRules)
   (srPersistentStorage ∷ [])

  data Output : Set where
    BroadcastProposal : ProposalMsg           → Output
    LogErr            : String                → Output
    -- LogInfo           : InfoLog a          → Output
    SendVote          : VoteMsg → List Author → Output
  open Output public

  SendVote-inj-v : ∀ {x1 x2 y1 y2} → SendVote x1 y1 ≡ SendVote x2 y2 → x1 ≡ x2
  SendVote-inj-v refl = refl

  SendVote-inj-si : ∀ {x1 x2 y1 y2} → SendVote x1 y1 ≡ SendVote x2 y2 → y1 ≡ y2
  SendVote-inj-si refl = refl

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Algebra`, unless
-- you want to parameterise it via the equality relation.

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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)

module Algebra.Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

-- The file is divided into sections depending on the arities of the
-- components of the algebraic structure.

open import Algebra.Core
open import Algebra.Definitions _≈_
import Algebra.Consequences.Setoid as Consequences
open import Data.Product using (_,_; proj₁; proj₂)
open import Level using (_⊔_)

------------------------------------------------------------------------
-- Structures with 1 binary operation
------------------------------------------------------------------------

record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∙-cong        : Congruent₂ ∙

  open IsEquivalence isEquivalence public

  setoid : Setoid a ℓ
  setoid = record { isEquivalence = isEquivalence }

  ∙-congˡ : LeftCongruent ∙
  ∙-congˡ y≈z = ∙-cong refl y≈z

  ∙-congʳ : RightCongruent ∙
  ∙-congʳ y≈z = ∙-cong y≈z refl

record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    assoc   : Associative ∙

  open IsMagma isMagma public

record IsBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    idem        : Idempotent ∙

  open IsSemigroup isSemigroup public

record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    comm        : Commutative ∙

  open IsSemigroup isSemigroup public

record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isBand : IsBand ∧
    comm   : Commutative ∧

  open IsBand isBand public
    renaming (∙-cong to ∧-cong; ∙-congˡ to ∧-congˡ; ∙-congʳ to ∧-congʳ)

record IsSelectiveMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    sel     : Selective ∙

  open IsMagma isMagma public

------------------------------------------------------------------------
-- Structures with 1 binary operation & 1 element
------------------------------------------------------------------------

record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identity    : Identity ε ∙

  open IsSemigroup isSemigroup public

  identityˡ : LeftIdentity ε ∙
  identityˡ = proj₁ identity

  identityʳ : RightIdentity ε ∙
  identityʳ = proj₂ identity

record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isMonoid : IsMonoid ∙ ε
    comm     : Commutative ∙

  open IsMonoid isMonoid public

  isCommutativeSemigroup : IsCommutativeSemigroup ∙
  isCommutativeSemigroup = record
    { isSemigroup = isSemigroup
    ; comm        = comm
    }

record IsIdempotentCommutativeMonoid (∙ : Op₂ A)
                                     (ε : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeMonoid : IsCommutativeMonoid ∙ ε
    idem                : Idempotent ∙

  open IsCommutativeMonoid isCommutativeMonoid public

-- Idempotent commutative monoids are also known as bounded lattices.
-- Note that the BoundedLattice necessarily uses the notation inherited
-- from monoids rather than lattices.

IsBoundedLattice = IsIdempotentCommutativeMonoid

module IsBoundedLattice {∙ : Op₂ A}
                        {ε : A}
                        (isIdemCommMonoid : IsIdempotentCommutativeMonoid ∙ ε) =
       IsIdempotentCommutativeMonoid isIdemCommMonoid

------------------------------------------------------------------------
-- Structures with 1 binary operation, 1 unary operation & 1 element
------------------------------------------------------------------------

record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  field
    isMonoid  : IsMonoid _∙_ ε
    inverse   : Inverse ε _⁻¹ _∙_
    ⁻¹-cong   : Congruent₁ _⁻¹

  open IsMonoid isMonoid public

  infixl 6 _-_
  _-_ : Op₂ A
  x - y = x ∙ (y ⁻¹)

  inverseˡ : LeftInverse ε _⁻¹ _∙_
  inverseˡ = proj₁ inverse

  inverseʳ : RightInverse ε _⁻¹ _∙_
  inverseʳ = proj₂ inverse

  uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
  uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique
                setoid ∙-cong assoc identity inverseʳ

  uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
  uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
                setoid ∙-cong assoc identity inverseˡ

record IsAbelianGroup (∙ : Op₂ A)
                      (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  field
    isGroup : IsGroup ∙ ε ⁻¹
    comm    : Commutative ∙

  open IsGroup isGroup public

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = isMonoid
    ; comm     = comm
    }

  open IsCommutativeMonoid isCommutativeMonoid public
    using (isCommutativeSemigroup)

------------------------------------------------------------------------
-- Structures with 2 binary operations
------------------------------------------------------------------------

-- Note that `IsLattice` is not defined in terms of `IsSemilattice`
-- because the idempotence laws of ∨ and ∧ can be derived from the
-- absorption laws, which makes the corresponding "idem" fields
-- redundant.  The derived idempotence laws are stated and proved in
-- `Algebra.Properties.Lattice` along with the fact that every lattice
-- consists of two semilattices.

record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∨-comm        : Commutative ∨
    ∨-assoc       : Associative ∨
    ∨-cong        : Congruent₂ ∨
    ∧-comm        : Commutative ∧
    ∧-assoc       : Associative ∧
    ∧-cong        : Congruent₂ ∧
    absorptive    : Absorptive ∨ ∧

  open IsEquivalence isEquivalence public

  ∨-absorbs-∧ : ∨ Absorbs ∧
  ∨-absorbs-∧ = proj₁ absorptive

  ∧-absorbs-∨ : ∧ Absorbs ∨
  ∧-absorbs-∨ = proj₂ absorptive

  ∧-congˡ : LeftCongruent ∧
  ∧-congˡ y≈z = ∧-cong refl y≈z

  ∧-congʳ : RightCongruent ∧
  ∧-congʳ y≈z = ∧-cong y≈z refl

  ∨-congˡ : LeftCongruent ∨
  ∨-congˡ y≈z = ∨-cong refl y≈z

  ∨-congʳ : RightCongruent ∨
  ∨-congʳ y≈z = ∨-cong y≈z refl

record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isLattice    : IsLattice ∨ ∧
    ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧

  open IsLattice isLattice public

  ∨-∧-distribʳ = ∨-distribʳ-∧
  {-# WARNING_ON_USAGE ∨-∧-distribʳ
  "Warning: ∨-∧-distribʳ was deprecated in v1.1.
  Please use ∨-distribʳ-∧ instead."
  #-}

------------------------------------------------------------------------
-- Structures with 2 binary operations & 1 element
------------------------------------------------------------------------

record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isMonoid    : IsMonoid + 0#
    *-isSemigroup : IsSemigroup *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

  open IsMonoid +-isMonoid public
    renaming
    ( assoc       to +-assoc
    ; ∙-cong      to +-cong
    ; ∙-congˡ     to +-congˡ
    ; ∙-congʳ     to +-congʳ
    ; identity    to +-identity
    ; identityˡ   to +-identityˡ
    ; identityʳ   to +-identityʳ
    ; isMagma     to +-isMagma
    ; isSemigroup to +-isSemigroup
    )

  open IsSemigroup *-isSemigroup public
    using ()
    renaming
    ( assoc    to *-assoc
    ; ∙-cong   to *-cong
    ; ∙-congˡ  to *-congˡ
    ; ∙-congʳ  to *-congʳ
    ; isMagma  to *-isMagma
    )

record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isSemigroup         : IsSemigroup *
    distrib               : * DistributesOver +
    zero                  : Zero 0# *

  open IsCommutativeMonoid +-isCommutativeMonoid public
    using ()
    renaming
    ( comm                   to +-comm
    ; isMonoid               to +-isMonoid
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    )

  zeroˡ : LeftZero 0# *
  zeroˡ = proj₁ zero

  zeroʳ : RightZero 0# *
  zeroʳ = proj₂ zero

  isNearSemiring : IsNearSemiring + * 0#
  isNearSemiring = record
    { +-isMonoid    = +-isMonoid
    ; *-isSemigroup = *-isSemigroup
    ; distribʳ      = proj₂ distrib
    ; zeroˡ         = zeroˡ
    }

  open IsNearSemiring isNearSemiring public
    hiding (+-isMonoid; zeroˡ)

record IsCommutativeSemiringWithoutOne
         (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
    *-comm               : Commutative *

  open IsSemiringWithoutOne isSemiringWithoutOne public

------------------------------------------------------------------------
-- Structures with 2 binary operations & 2 elements
------------------------------------------------------------------------

record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
                                         (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    -- Note that these structures do have an additive unit, but this
    -- unit does not necessarily annihilate multiplication.
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isMonoid            : IsMonoid * 1#
    distrib               : * DistributesOver +

  distribˡ : * DistributesOverˡ +
  distribˡ = proj₁ distrib

  distribʳ : * DistributesOverʳ +
  distribʳ = proj₂ distrib

  open IsCommutativeMonoid +-isCommutativeMonoid public
    renaming
    ( assoc                  to +-assoc
    ; ∙-cong                 to +-cong
    ; ∙-congˡ                to +-congˡ
    ; ∙-congʳ                to +-congʳ
    ; identity               to +-identity
    ; identityˡ              to +-identityˡ
    ; identityʳ              to +-identityʳ
    ; comm                   to +-comm
    ; isMagma                to +-isMagma
    ; isSemigroup            to +-isSemigroup
    ; isMonoid               to +-isMonoid
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    )

  open IsMonoid *-isMonoid public
    using ()
    renaming
    ( assoc       to *-assoc
    ; ∙-cong      to *-cong
    ; ∙-congˡ     to *-congˡ
    ; ∙-congʳ     to *-congʳ
    ; identity    to *-identity
    ; identityˡ   to *-identityˡ
    ; identityʳ   to *-identityʳ
    ; isMagma     to *-isMagma
    ; isSemigroup to *-isSemigroup
    )

record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero + * 0# 1#
    zero : Zero 0# *

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
  isSemiringWithoutOne = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isSemigroup         = *-isSemigroup
    ; distrib               = distrib
    ; zero                  = zero
    }

  open IsSemiringWithoutOne isSemiringWithoutOne public
    using
    ( isNearSemiring
    ; zeroˡ
    ; zeroʳ
    )

record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiring : IsSemiring + * 0# 1#
    *-comm     : Commutative *

  open IsSemiring isSemiring public

  isCommutativeSemiringWithoutOne :
    IsCommutativeSemiringWithoutOne + * 0#
  isCommutativeSemiringWithoutOne = record
    { isSemiringWithoutOne = isSemiringWithoutOne
    ; *-comm = *-comm
    }

  *-isCommutativeSemigroup : IsCommutativeSemigroup *
  *-isCommutativeSemigroup = record
    { isSemigroup = *-isSemigroup
    ; comm        = *-comm
    }

  *-isCommutativeMonoid : IsCommutativeMonoid * 1#
  *-isCommutativeMonoid = record
    { isMonoid = *-isMonoid
    ; comm     = *-comm
    }

------------------------------------------------------------------------
-- Structures with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-isMonoid       : IsMonoid * 1#
    distrib          : * DistributesOver +
    zero             : Zero 0# *

  open IsAbelianGroup +-isAbelianGroup public
    renaming
    ( assoc                  to +-assoc
    ; ∙-cong                 to +-cong
    ; ∙-congˡ                to +-congˡ
    ; ∙-congʳ                to +-congʳ
    ; identity               to +-identity
    ; identityˡ              to +-identityˡ
    ; identityʳ              to +-identityʳ
    ; inverse                to -‿inverse
    ; inverseˡ               to -‿inverseˡ
    ; inverseʳ               to -‿inverseʳ
    ; ⁻¹-cong                to -‿cong
    ; comm                   to +-comm
    ; isMagma                to +-isMagma
    ; isSemigroup            to +-isSemigroup
    ; isMonoid               to +-isMonoid
    ; isCommutativeMonoid    to +-isCommutativeMonoid
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    ; isGroup                to +-isGroup
    )

  open IsMonoid *-isMonoid public
    using ()
    renaming
    ( assoc       to *-assoc
    ; ∙-cong      to *-cong
    ; ∙-congˡ     to *-congˡ
    ; ∙-congʳ     to *-congʳ
    ; identity    to *-identity
    ; identityˡ   to *-identityˡ
    ; identityʳ   to *-identityʳ
    ; isMagma     to *-isMagma
    ; isSemigroup to *-isSemigroup
    )

  zeroˡ : LeftZero 0# *
  zeroˡ = proj₁ zero

  zeroʳ : RightZero 0# *
  zeroʳ = proj₂ zero

  isSemiringWithoutAnnihilatingZero
    : IsSemiringWithoutAnnihilatingZero + * 0# 1#
  isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isMonoid            = *-isMonoid
    ; distrib               = distrib
    }

  isSemiring : IsSemiring + * 0# 1#
  isSemiring = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    ; zero = zero
    }

  open IsSemiring isSemiring public
    using (distribˡ; distribʳ; isNearSemiring; isSemiringWithoutOne)

record IsCommutativeRing
         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isRing : IsRing + * - 0# 1#
    *-comm : Commutative *

  open IsRing isRing public

  *-isCommutativeMonoid : IsCommutativeMonoid * 1#
  *-isCommutativeMonoid =  record
    { isMonoid = *-isMonoid
    ; comm     = *-comm
    }

  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = isSemiring
    ; *-comm = *-comm
    }

  open IsCommutativeSemiring isCommutativeSemiring public
    using ( isCommutativeSemiringWithoutOne )

record IsBooleanAlgebra
         (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
  field
    isDistributiveLattice : IsDistributiveLattice ∨ ∧
    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
    ¬-cong                : Congruent₁ ¬

  open IsDistributiveLattice isDistributiveLattice public