text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.UnivalenceId where

open import Cubical.Core.Glue
  renaming ( isEquiv      to isEquivPath
           ; _≃_          to EquivPath
           ; equivFun     to equivFunPath )
open import Cubical.Core.Id

open import Cubical.Foundations.Prelude public
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ )
open import Cubical.Foundations.Id
open import Cubical.Foundations.Equiv
  renaming ( isPropIsEquiv to isPropIsEquivPath )
open import Cubical.Foundations.Univalence
  renaming ( EquivContr   to EquivContrPath )
open import Cubical.Foundations.Isomorphism

path≡Id : ∀ {ℓ} {A B : Type ℓ} → Path _ (Path _ A B) (Id A B)
path≡Id = isoToPath (iso pathToId idToPath idToPathToId pathToIdToPath )

equivPathToEquivPath : ∀ {ℓ} {A : Type ℓ} {B : Type ℓ} → (p : EquivPath A B) →
                       Path _ (equivToEquivPath (equivPathToEquiv p)) p
equivPathToEquivPath (f , p) i =
  ( f , isPropIsEquivPath f (equivToEquivPath (equivPathToEquiv (f , p)) .snd) p i )

equivPath≡Equiv : ∀ {ℓ} {A B : Type ℓ} → Path _ (EquivPath A B) (A ≃ B)
equivPath≡Equiv {ℓ} = isoToPath (iso (equivPathToEquiv {ℓ}) equivToEquivPath equivToEquiv equivPathToEquivPath)

univalenceId : ∀ {ℓ} {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
univalenceId {ℓ} {A = A} {B = B} = equivPathToEquiv rem
  where
  rem0 : Path _ (Lift (EquivPath A B)) (Lift (A ≃ B))
  rem0 = congPath Lift equivPath≡Equiv

  rem1 : Path _ (Id A B) (Lift (A ≃ B))
  rem1 i = hcomp (λ j → λ { (i = i0) → path≡Id {A = A} {B = B} j
                          ; (i = i1) → rem0 j })
                 (univalencePath {A = A} {B = B} i)

  rem : EquivPath (Id A B) (A ≃ B)
  rem = compEquiv (eqweqmap rem1) (invEquiv LiftEquiv)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Ual.Void where

data ⊥ : Set where

¬ : Set → Set
¬ p = p → ⊥

ext: agda

max_stars_repo_name: brunoczim/ual

max_issues_repo_name: brunoczim/ual

max_forks_repo_name: brunoczim/ual


text:
module Arity where

open import OscarPrelude

record Arity : Set
 where
  constructor ⟨_⟩
  field
    arity : Nat

open Arity public

instance EqArity : Eq Arity
Eq._==_ EqArity _ = decEq₁ (cong arity) ∘ (_≟_ on arity $ _)


text:
open import Common.Reflect
open import Common.Prelude

data Z : Set where
  zero : Z

foo : QName → Bool → Bool
foo (quote Nat.zero) b = {!b!}
foo _ _ = false

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Leftunit
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transitivity
open import Oscar.Class.Transleftidentity

module Oscar.Class.Transleftidentity.ToLeftunit where

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ}
  {ε : Reflexivity.type _∼_}
  {transitivity : Transitivity.type _∼_}
  where
  instance
    toLeftunitFromTransleftidentity :
      ⦃ _ : Transleftidentity.class _∼_ _∼̇_ ε transitivity ⦄
      → ∀ {x y} {f : x ∼ y} → Leftunit.class _∼̇_ ε (flip transitivity) f
    toLeftunitFromTransleftidentity .⋆ = transleftidentity


text:
------------------------------------------------------------------------
-- A map function for the substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Function.Map
  {i u e} {Uni : IndexedUniverse i u e} where

import Axiom.Extensionality.Propositional as E
import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Function.Basics
open import Function using (_$_)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

private
 module Dummy
   {t₁} {T₁ : Term-like t₁}
   {t₂} {T₂ : Term-like t₂}
   where

  open Term-like T₁ using ()
                    renaming (_⊢_ to _⊢₁_; _≅-⊢_ to _≅-⊢₁_; [_] to [_]₁)
  open Term-like T₂ using () renaming (_≅-⊢_ to _≅-⊢₂_)

  -- Map.

  map : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
        [ T₁ ⟶ T₂ ] ρ̂₂ → (ρ₁ : Sub T₁ ρ̂₁) → Sub T₂ (ρ̂₁ ∘̂ ρ̂₂)
  map f ρ₁ = f [∘] ρ₁

  abstract

    -- An unfolding lemma.

    map-▻ :
      E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t₂) →
      ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {σ}
      (f : [ T₁ ⟶ T₂ ] ρ̂₂) (ρ : Sub T₁ ρ̂₁) t →
      map f (ρ ▻⇨[ σ ] t) ≅-⇨ map f ρ ▻⇨[ σ ] f · t
    map-▻ ext {Γ} {σ = σ} f ρ t = extensionality ext P.refl lemma
      where
      lemma : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
              f · (x /∋ (ρ ▻⇨ t)) ≅-⊢₂ x /∋ (map f ρ ▻⇨ f · t)
      lemma zero    = P.refl
      lemma (suc x) = P.refl

  -- A congruence lemma.

  map-cong : ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
               {f₁ : [ T₁ ⟶ T₂ ] ρ̂₂₁} {ρ₁ : Sub T₁ ρ̂₁₁}
               {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
               {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂₂} {ρ₂ : Sub T₁ ρ̂₁₂} →
             f₁ ≅-⟶ f₂ → ρ₁ ≅-⇨ ρ₂ → map f₁ ρ₁ ≅-⇨ map f₂ ρ₂
  map-cong {f₁ = _ , _} {ρ₁ = _ , _} {f₂ = ._ , _} {ρ₂ = ._ , _}
           [ P.refl ] [ P.refl ] = [ P.refl ]

  abstract

    -- Variants which only require that the functions are
    -- extensionally equal.

    map-cong-ext₁ : E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t₂) →
                    ∀ {Γ₁ Δ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ} {ρ̂₂₁ : Δ ⇨̂ Ε₁}
                      {f₁ : [ T₁ ⟶ T₂ ] ρ̂₂₁} {ρ₁ : Sub T₁ ρ̂₁₁}
                      {Γ₂   Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ} {ρ̂₂₂ : Δ ⇨̂ Ε₂}
                      {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂₂} {ρ₂ : Sub T₁ ρ̂₁₂} →
                    Ε₁ ≅-Ctxt Ε₂ →
                    (∀ {σ} (t : Δ ⊢₁ σ) → f₁ · t ≅-⊢₂ f₂ · t) →
                    ρ₁ ≅-⇨ ρ₂ → map f₁ ρ₁ ≅-⇨ map f₂ ρ₂
    map-cong-ext₁ ext {ρ₁ = ρ} {ρ₂ = ._ , _} Ε₁≅Ε₂ f₁≅f₂ [ P.refl ] =
      extensionality ext Ε₁≅Ε₂ (λ x → f₁≅f₂ (x /∋ ρ))

    map-cong-ext₂ : E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t₂) →
                    ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
                      {f₁ : [ T₁ ⟶ T₂ ] ρ̂₂₁} {ρ₁ : Sub T₁ ρ̂₁₁}
                      {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
                      {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂₂} {ρ₂ : Sub T₁ ρ̂₁₂} →
                    Δ₁ ≅-Ctxt Δ₂ → Ε₁ ≅-Ctxt Ε₂ →
                    (∀ {σ₁ σ₂} {t₁ : Δ₁ ⊢₁ σ₁} {t₂ : Δ₂ ⊢₁ σ₂} →
                       t₁ ≅-⊢₁ t₂ → f₁ · t₁ ≅-⊢₂ f₂ · t₂) →
                    ρ₁ ≅-⇨ ρ₂ → map f₁ ρ₁ ≅-⇨ map f₂ ρ₂
    map-cong-ext₂ ext P.refl Ε₁≅Ε₂ f₁≅f₂ ρ₁≅ρ₂ =
      map-cong-ext₁ ext Ε₁≅Ε₂ (λ t → f₁≅f₂ (P.refl {x = [ t ]₁})) ρ₁≅ρ₂

  -- Some sort of naturality statement for _/∋_. (Note that this lemma
  -- holds definitionally. This is not the case for the corresponding
  -- lemma in deBruijn.Substitution.Data.Map.)

  /∋-map : ∀ {Γ Δ Ε σ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
           (x : Γ ∋ σ) (f : [ T₁ ⟶ T₂ ] ρ̂₂) (ρ : Sub T₁ ρ̂₁) →
           x /∋ map f ρ ≅-⊢₂ f · (x /∋ ρ)
  /∋-map x f ρ = P.refl

open Dummy public

-- Map is functorial.

map-[id] : ∀ {t} {T : Term-like t} {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
           (ρ : Sub T ρ̂) →
           map ([id] {T = T}) ρ ≅-⇨ ρ
map-[id] = [id]-[∘]

map-[∘] :
  ∀ {t₁} {T₁ : Term-like t₁}
    {t₂} {T₂ : Term-like t₂}
    {t₃} {T₃ : Term-like t₃}
    {Γ Δ Ε Ζ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {ρ̂₃ : Ε ⇨̂ Ζ}
  (f₂ : [ T₂ ⟶ T₃ ] ρ̂₃) (f₁ : [ T₁ ⟶ T₂ ] ρ̂₂)
  (ρ : Sub T₁ ρ̂₁) →
  map (f₂ [∘] f₁) ρ ≅-⇨ map f₂ (map f₁ ρ)
map-[∘] f₂ f₁ ρ = sym-⟶ $ [∘]-[∘] f₂ f₁ ρ

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
{-# OPTIONS --sized-types #-}
module SList.Properties (A : Set) where

open import Data.List
open import List.Permutation.Base A
open import SList

lemma-unsize-size : (xs : List A) → xs ∼ unsize A (size A xs)
lemma-unsize-size [] = ∼[]
lemma-unsize-size (x ∷ xs) = ∼x /head  /head (lemma-unsize-size xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Relation.Unary using ( ∅ ; _∪_ )
open import Web.Semantic.DL.Concept using ( Concept )
open import Web.Semantic.DL.Role using ( Role )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( Subset ; ⁅_⁆ )

module Web.Semantic.DL.TBox where

infixl 5 _⊑₁_ _⊑₂_
infixr 4 _,_

data TBox (Σ : Signature) : Set where
  ε : TBox Σ
  _,_ : (T U : TBox Σ) → TBox Σ
  _⊑₁_ : (C D : Concept Σ) → TBox Σ
  _⊑₂_ : (Q R : Role Σ) → TBox Σ
  Ref : (R : Role Σ) → TBox Σ
  Irr : (R : Role Σ) → TBox Σ
  Tra : (R : Role Σ) → TBox Σ
  Dis : (Q R : Role Σ) → TBox Σ

Axioms : ∀ {Σ} → TBox Σ → Subset (TBox Σ)
Axioms ε         = ∅
Axioms (T , U)   = (Axioms T) ∪ (Axioms U)
Axioms (C ⊑₁ D)  = ⁅ C ⊑₁ D ⁆
Axioms (Q ⊑₂ R)  = ⁅ Q ⊑₂ R ⁆
Axioms (Ref R)   = ⁅ Ref R ⁆
Axioms (Irr R)   = ⁅ Irr R ⁆
Axioms (Tra R)   = ⁅ Tra R ⁆
Axioms (Dis Q R) = ⁅ Dis Q R ⁆

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module GUIgeneric.GUIFeatures where

open import GUIgeneric.Prelude

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib
open import StateSizedIO.GUI.WxGraphicsLibLevel3

open Interfaceˢ public

-- Components
--
frameAndOKButton : ComponentEls _
frameAndOKButton = add (create-button "OK button") create-frame notOptimzed

exampleOneButton : Frame
exampleOneButton = frameAndOKButton

exampleTwoButtons : Frame
exampleTwoButtons = add (create-button "Cancel button") frameAndOKButton notOptimzed

exampleThreeButtons : Frame
exampleThreeButtons = add (create-button "Cancel button") (frameAndOKButton) notOptimzed

getFrame : Frame → ComponentEls frame
getFrame (createC tt) = create-frame
getFrame (add' buttonFrame f f₁ _) = f₁

data StateV : Set where
      s0 s1 s2 : StateV

data StateTea : Set where
      s0 s1 s2 s3 : StateTea

data FeatureTea : Set where
  yesTea noTea : FeatureTea

data FeatureFree : Set where
  yesFree noFree : FeatureFree

data FeatureCancel : Set where
  yesCancel noCancel : FeatureCancel

record FeatureVendingMachine (BaseState : Set) : Set₁ where
  field  Features : Set
         AddState : Set
         guiVendingMachine : (f : Features) → BaseState ⊎ AddState → Frame
  NewState : Set
  NewState =  BaseState ⊎ AddState

open FeatureVendingMachine public

base : FeatureVendingMachine StateV
base .Features = ⊤
base .AddState = ⊥
base .guiVendingMachine f (inj₁ s0) = exampleOneButton
base .guiVendingMachine f (inj₁ s1) = exampleOneButton
base .guiVendingMachine f (inj₁ s2) = exampleTwoButtons
base .guiVendingMachine f (inj₂ ())

upgradeFeatureVM : (baseState : Set)(vm : FeatureVendingMachine baseState)
                   → FeatureVendingMachine (baseState ⊎ vm .AddState)
upgradeFeatureVM baseState vm .Features = vm .Features
upgradeFeatureVM baseState vm .AddState = ⊥
upgradeFeatureVM baseState vm .guiVendingMachine f (inj₁ (inj₁ s)) = vm .guiVendingMachine f (inj₁ s)
upgradeFeatureVM baseState vm .guiVendingMachine f (inj₁ (inj₂ s)) = vm .guiVendingMachine f (inj₂ s)
upgradeFeatureVM baseState vm .guiVendingMachine f (inj₂ ())

changeBaseState : (baseState : Set)(vm : FeatureVendingMachine baseState)
                  (newState : Set)
                  (new2base : newState → baseState)
                  → FeatureVendingMachine newState
changeBaseState baseState vm newState new2base  .Features = vm .Features
changeBaseState baseState vm newState new2base .AddState  = vm .AddState
changeBaseState baseState vm newState new2base .guiVendingMachine f (inj₁ x) = vm .guiVendingMachine f (inj₁ (new2base x))
changeBaseState baseState vm newState new2base .guiVendingMachine f (inj₂ y) = vm .guiVendingMachine f (inj₂ y)

upgradeFeatureVM+ : (baseState : Set)(vm : FeatureVendingMachine baseState)
                    (newBaseState : Set)
                    (newAddState : Set)
                    (new2base : newBaseState ⊎ newAddState → baseState ⊎ vm .AddState)
                     → FeatureVendingMachine newBaseState
Features (upgradeFeatureVM+ baseState vm newBaseState newAddState new2Base) = vm .Features
AddState (upgradeFeatureVM+ baseState vm newBaseState newAddState new2Base) = newAddState
guiVendingMachine (upgradeFeatureVM+ baseState vm newBaseState newAddState new2Base)  f s = vm .guiVendingMachine f (new2Base s)

tea : FeatureVendingMachine StateV → FeatureVendingMachine StateV
tea otherVM .Features = otherVM .Features × FeatureTea
tea otherVM .AddState = otherVM .AddState ⊎ ⊤
tea otherVM .guiVendingMachine (f , yesTea) (inj₁ s1) = exampleThreeButtons
tea otherVM .guiVendingMachine (f , _) (inj₁ s) = otherVM .guiVendingMachine f (inj₁ s)
tea otherVM .guiVendingMachine (f , _) (inj₂ (inj₁ s)) = otherVM .guiVendingMachine f (inj₂ s)
tea otherVM .guiVendingMachine (f , _) (inj₂ (inj₂ _)) = exampleOneButton -- new state

cancel : FeatureVendingMachine StateV → FeatureVendingMachine StateV
cancel otherVM .Features = otherVM .Features × FeatureCancel
cancel otherVM .AddState = otherVM .AddState ⊎ ⊤
cancel otherVM .guiVendingMachine (f , yesCancel) (inj₁ s1) = exampleThreeButtons
cancel otherVM .guiVendingMachine (f , _) (inj₁ s) = otherVM .guiVendingMachine f (inj₁ s)
cancel otherVM .guiVendingMachine (f , _) (inj₂ (inj₁ s)) = otherVM .guiVendingMachine f (inj₂ s)
cancel otherVM .guiVendingMachine (f , _) (inj₂ (inj₂ _)) = exampleOneButton -- new state

teaBase : FeatureVendingMachine StateV
teaBase = tea base

StateTeaAux  : Set
StateTeaAux = StateV ⊎ (⊥ ⊎ ⊤)

teaBaseUnified : FeatureVendingMachine StateTeaAux
teaBaseUnified = upgradeFeatureVM StateV teaBase

stateTeaToPrevState : StateTea → StateTeaAux
stateTeaToPrevState s0 = inj₁ s0
stateTeaToPrevState s1 = inj₁ s1
stateTeaToPrevState s2 = inj₁ s2
stateTeaToPrevState s3 = inj₂ (inj₂ _)

teaBaseImproved : FeatureVendingMachine StateTea
teaBaseImproved = changeBaseState
                       StateTeaAux
                       teaBaseUnified StateTea stateTeaToPrevState

teaBaseNewToOld : StateTea ⊎ ⊥ → StateV ⊎ teaBase .AddState
teaBaseNewToOld (inj₁ s0) = inj₁ s0
teaBaseNewToOld (inj₁ s1) = inj₁ s1
teaBaseNewToOld (inj₁ s2) = inj₁ s2
teaBaseNewToOld (inj₁ s3) = inj₂ (inj₂ _)
teaBaseNewToOld (inj₂ ())

teaBaseImproved+ : FeatureVendingMachine StateTea
teaBaseImproved+  = upgradeFeatureVM+ StateV teaBase StateTea ⊥ teaBaseNewToOld

cancelTeaBase = cancel (tea base)

module base' where
  NewFeatures' : Set
  NewFeatures' = ⊤

  guiVendingMachine' : (f : NewFeatures') → StateV → Frame
  guiVendingMachine' f s0 = exampleOneButton
  guiVendingMachine' f s1 = exampleOneButton
  guiVendingMachine' f s2 = exampleTwoButtons

module tea' (OtherFeatures : Set)
           (oldV : OtherFeatures  → StateV → Frame) where
  NewFeatures' : Set
  NewFeatures' = OtherFeatures × FeatureTea

  guiVendingMachine' : (f : NewFeatures')(s : StateV) → Frame
  guiVendingMachine' (f , yesTea) s1 = exampleThreeButtons
  guiVendingMachine' (f , _) s = oldV f s

module cancel' (OtherFeatures : Set)
              (oldV : OtherFeatures → StateV → Frame) where
  NewFeatures' : Set
  NewFeatures' = OtherFeatures × FeatureCancel

  guiVendingMachine' : (f : NewFeatures')(s : StateV) → Frame
  guiVendingMachine' (f , yesCancel) s1 = exampleThreeButtons
  guiVendingMachine' (f , _) s = oldV f s

module teaBase' (OtherFeatures : Set) where
  open base' renaming (guiVendingMachine' to baseGUIVendingMachine; NewFeatures' to BaseFeatures)
  open tea' BaseFeatures baseGUIVendingMachine public

module cancelTeaBase' (OtherFeatures : Set) where
  open teaBase' OtherFeatures renaming (guiVendingMachine' to teaBaseGUIVendingMachine; NewFeatures' to TeaBaseFeatures)
  open cancel' TeaBaseFeatures teaBaseGUIVendingMachine

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


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

{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.
   Copyright (c) 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 Haskell.Modules.RWS
open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.BlockStorage.BlockStore          as BlockStore
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.Liveness.ExponentialTimeInterval as ExponentialTimeInterval
import      LibraBFT.Impl.Consensus.Liveness.RoundState              as RoundState
import      LibraBFT.Impl.Consensus.MetricsSafetyRules               as MetricsSafetyRules
import      LibraBFT.Impl.Consensus.RoundManager                     as RoundManager
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRulesManager   as SafetyRulesManager
import      LibraBFT.Impl.Consensus.TestUtils.MockStorage            as MockStorage
open import LibraBFT.Impl.IO.OBM.Messages
import      LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-1  as ECP-LBFT-OBM-Diff-1
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.OBM.Rust.Duration                          as Duration
open import LibraBFT.Impl.OBM.Rust.RustTypes
import      LibraBFT.Impl.Storage.DiemDB.DiemDB                      as DiemDB
import      LibraBFT.Impl.Types.BlockInfo                            as BlockInfo
import      LibraBFT.Impl.Types.EpochChangeProof                     as EpochChangeProof
import      LibraBFT.Impl.Types.ValidatorVerifier                    as ValidatorVerifier
open import LibraBFT.Impl.Types.Verifier
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                              using (String)

module LibraBFT.Impl.Consensus.EpochManager where

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

data RlecState : Set where
  RSNothing  : RlecState
  RSNeedECP  : ReconfigEventEpochChange → RlecState
  RSNeedRLEC : EpochChangeProof         → RlecState

data ProcessMessageAction : Set where
  PMContinue        : ProcessMessageAction
  PMInput           : Input            → ProcessMessageAction
  PMNewEpoch        : EpochManager     → List Output    → ProcessMessageAction
  PMSendECP         : EpochChangeProof → AccountAddress → Author {-Text-} → Epoch → Round → ProcessMessageAction
  PMSendEpochRRq    : EpRRqWire        → AccountAddress → ProcessMessageAction

data PMOutput : Set where
  PMErr  : ErrLog  → PMOutput
  PMInfo : InfoLog → PMOutput

EM : Set → Set₁
EM = RWS Unit PMOutput RlecState

runEM : ∀ {r}
      → EM r
      → RlecState
      → (r × RlecState × List PMOutput)
runEM f = RWS-run f unit

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

expectNewEpoch
  : EpochManager → Instant → ReconfigEventEpochChange → LedgerInfoWithSignatures
  → Either ErrLog ProcessMessageAction

startProcessor-ed
  : EpochManager → Instant → OnChainConfigPayload
  → ObmNeedFetch → ProposalGenerator → LedgerInfoWithSignatures
  → EitherD ErrLog  (EpochManager × List Output)

startRoundManager'-ed-abs
  : EpochManager → Instant → RecoveryData → EpochState
  → ObmNeedFetch → ProposalGenerator → Version
  → EitherD ErrLog (EpochManager × List Output)

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

new
  : NodeConfig → StateComputer → PersistentLivenessStorage → Author → SK
  → Either ErrLog EpochManager
new nodeConfig stateComputer persistentLivenessStorage obmAuthor obmSK = do
  let -- author = node_config.validator_network.as_ref().unwrap().peer_id();
      config = nodeConfig ^∙ ncConsensus
  safetyRulesManager ← SafetyRulesManager.new (config ^∙ ccSafetyRules) obmAuthor obmSK
  pure $ mkEpochManager
    obmAuthor
    config
    stateComputer
    persistentLivenessStorage
    safetyRulesManager
    nothing

epochState : EpochManager → Either ErrLog EpochState
epochState self = case self ^∙ emProcessor of λ where
  nothing                           → Left fakeErr -- ["EpochManager not started yet"]
  (just (RoundProcessorNormal   p)) → pure (p ^∙ rmEpochState)
  (just (RoundProcessorRecovery p)) → pure (p ^∙ rcmEpochState)

epoch : EpochManager → Either ErrLog Epoch
epoch self = (_^∙ esEpoch) <$> epochState self

createRoundState : EpochManager → Instant → RoundState
createRoundState self now =
  let timeInterval = ExponentialTimeInterval.new
        (Duration.fromMillis (self ^∙ emConfig ∙ ccRoundInitialTimeoutMS))
        1.2
        6
   in RoundState.new timeInterval now

abstract
  createRoundState-abs = createRoundState
  createRoundState-abs-≡ : createRoundState-abs ≡ createRoundState
  createRoundState-abs-≡ = refl

createProposerElection : EpochState → ProposerElection
createProposerElection epochState0 =
  ProposerElection∙new
  (ValidatorVerifier.getOrderedAccountAddressesObmTODO (epochState0 ^∙ esVerifier))

processEpochRetrieval
  : EpochManager {-Text-} → EpRRqWire → AccountAddress → EM ProcessMessageAction
processEpochRetrieval self {-wireOrInternal-} (EpRRqWire∙new {-why fromE fromR-} request) peerAddress = do
  tell (PMInfo fakeInfo ∷ [])
    -- ["Enter", wireOrInternal, why, lsA peerAddress, lsE fromE, lsR fromR, lsEpochRRq request]))]
  case DiemDB.getEpochEndingLedgerInfos
         (self ^∙ emStorage ∙ msObmDiemDB) (request ^∙ eprrqStartEpoch) (request ^∙ eprrqEndEpoch) of λ where
    (Left e) → do
      tell ( (PMErr (withErrCtx (here'
               ("failed to get epoch proof" {-lsA peerAddress, why, lsEpochRRq request-} ∷ [])) e))
           ∷ [])
      pure PMContinue
    (Right (liws , more)) →
      eitherSD (self ^∙ emEpoch) (λ err -> do tell (PMErr (withErrCtx (here' []) err) ∷ []); pure PMContinue) $ λ e -> do
          let ecp = EpochChangeProof∙new liws more
              me  = self ^∙ emAuthor
              r   = eitherS (self ^∙ emObmRoundManager) (const {-Round-} 0) (_^∙ rmRound)
          tell (PMInfo fakeInfo {-["Exit", "SendEpochRRp", why, lsA peerAddress, lsECP ecp]-} ∷ [])
          pure (PMSendECP ecp peerAddress me {-why-} e r)
 where
  here' : List String → List String
  here' t = "EpochManager" ∷ "processEpochRetrieval" ∷ t

processDifferentEpoch
  : EpochManager → Input → AccountAddress → Epoch → Round
  → EM ProcessMessageAction
processDifferentEpoch self obmI peerAddress peerDifferentEpoch obmPeerRound = do
  tell (PMInfo fakeInfo -- (here [ "ReceiveMessageFromDifferentEpoch", lsA peerAddress
                        --       , lsE peerDifferentEpoch, lsR obmPeerRound, logShowI obmI ])
                        ∷ [])
  eitherSD (self ^∙ emEpoch)               pmerr $ λ epoch' →
    eitherSD (self ^∙ emObmRoundManager) pmerr $ λ rm-NotUsedInAgda-OnlyLoggingInHaskell →
      case compare peerDifferentEpoch epoch' of λ where
        LT → do -- help nodes that have lower epoch
          -- LBFT-OBM-DIFF : not sure if this is different, but the message that causes
          -- this request will be dropped.
          -- await (Rust comment)
          processEpochRetrieval
            self {-"diffE"-}
            (EpRRqWire∙new {-why epoch' (self^.emObmRoundManagerErrExit.rmRound)-}
              (EpochRetrievalRequest∙new peerDifferentEpoch epoch'))
            peerAddress
        GT → do
          -- LBFT-OBM-DIFF : message dropped in this case too
          let epRrq  = EpochRetrievalRequest∙new epoch' peerDifferentEpoch
              epprqw = EpRRqWire∙new {-why epoch' (self^.emObmRoundManagerErrExit.rmRound)-} epRrq
          tell (PMInfo fakeInfo ∷ [])
                     -- (here [ "SendEpochRRq", lsA peerAddress, lsEpochRRq epRrq
                     --       , "request proof to join higher epoch because", logShowI obmI ]))]
          -- TODO-1
          pure (PMSendEpochRRq epprqw peerAddress)
        EQ → do
          tell (PMErr fakeErr ∷ []) -- (here ["EQ should not happen"])
          pure PMContinue
 where
  here' : List String → List String
  here' t = "EpochManager" ∷ "processDifferentEpoch" ∷ t
  pmerr : ErrLog → EM ProcessMessageAction
  pmerr err = do tell (PMErr (withErrCtx (here' []) err) ∷ []); pure PMContinue
{-
  why    = show (msgType obmI)               <> "/" <>
           peerAddress^.aAuthorName          <> "/" <>
           show (peerDifferentEpoch^.eEpoch) <> "/" <>
           show (obmPeerRound^.rRound)
-}

startNewEpoch
  : EpochManager → Instant → Maybe ReconfigEventEpochChange → EpochChangeProof
  → Either ErrLog ProcessMessageAction
startNewEpoch self now mrlec proof = do
  es   ← epochState self
  liws ← withErrCtx' (here' ("invalid EpochChangeProof" ∷ []))
                     (EpochChangeProof.verify proof es)
  -- --------------------------------------------------
  -- LBFT-OBM-DIFF: scSyncTo, rather than syncing world state to another node,
  -- it just gets the NextEpochState from the given LIWS.
  -- --------------------------------------------------
  -- Independently, the world state is synced to the Version/LeadCount contained in 'liws'.
  -- See 'obmVersion' setting in startRoundManager' below.
  rlec ← case mrlec of λ where
           (just rlec) → pure rlec
           nothing     → eitherS (Left "fakeErr") -- TODO-2 ((self^.emStateComputer.scSyncTo) liws)
                                 (λ e → Left fakeErr) -- (ErrL (here (lsLIWS liws ∷ e))))
                                 Right
  self' ← ECP-LBFT-OBM-Diff-1.e_EpochManager_startNewEpoch self proof
  pure PMContinue
  expectNewEpoch self' now rlec liws
 where
  here' : List String → List String
  here' t = "EpochManager" ∷ "startNewEpoch" ∷ t

startRoundManager-ed
  : EpochManager → Instant → RecoveryData → EpochState
  → ObmNeedFetch → ProposalGenerator → Version
  → EitherD ErrLog (EpochManager × List Output)
startRoundManager-ed self0 now recoveryData epochState0 obmNeedFetch obmProposalGenerator obmVersion =
  let self = case self0 ^∙ emProcessor of λ where
               (just (RoundProcessorNormal rm)) →
                 self0 & emStorage               ∙~ rm ^∙ rmBlockStore ∙ bsStorage
                       & emStorage ∙ msObmDiemDB ∙~ self0 ^∙ emStorage ∙ msObmDiemDB
               _ →
                 self0
      -- OBM-DIFF : use the version in the ledger info of the EpochChangeProof
      obv  = eitherS (self ^∙ emObmRoundManager) (const BlockInfo.gENESIS_VERSION) (const obmVersion)

   in startRoundManager'-ed-abs self now recoveryData epochState0 obmNeedFetch
                                (obmProposalGenerator & pgLastRoundGenerated ∙~ {-Round-} 0)
                                obv

module startRoundManager'-ed
  (self : EpochManager)
  (now  : Instant)
  (recoveryData : RecoveryData)
  (epochState0 : EpochState)
  (obmNeedFetch : ObmNeedFetch)
  (obmProposalGenerator : ProposalGenerator)
  (obmVersion           : Version)
  where

  continue2 continue2-abs : Maybe Vote → BlockStore → SafetyRules → EitherD ErrLog (EpochManager × List Output)
  continue1 continue1-abs : Maybe Vote → BlockStore → EitherD ErrLog (EpochManager × List Output)
  err : ∀ {B} → List String → ErrLog → EitherD ErrLog B
  here' : List String → List String

  step₀ = do
    let lastVote = recoveryData ^∙ rdLastVote
    case BlockStore.new-e-abs  -- Either version so we only get Left and Right cases
           (self ^∙ emStorage)
           recoveryData
           -- TODO-2 : use real StateComputer when it exists
           stateComputer -- (self ^∙ emStateComputer & scObmVersion .~ obv) TODO-2
           (self ^∙ emConfig ∙ ccMaxPrunedBlocksInMem) of λ where
      (Left  e) → err ("BlockStore.new" ∷ []) e
      (Right bs) → continue1-abs lastVote bs

  err  t = withErrCtxD' t ∘ Left
  here' t = "EpochManager" ∷ "startRoundManager" ∷ t

  continue1 lastVote blockStore = do
    --------------------------------------------------
    let safetyRules = {-MetricsSafetyRules::new-}
          SafetyRulesManager.client (self ^∙ emSafetyRulesManager) -- self.storage.clone());
    case MetricsSafetyRules.performInitialize-abs safetyRules (self ^∙ emStorage) of λ where
      (Left e)             → err (here' ("MetricsSafetyRules.performInitialize" ∷ [])) e
      (Right safetyRules') → continue2-abs lastVote blockStore safetyRules'

  continue2 lastVote blockStore safetyRules = do
    --------------------------------------------------
    let proposalGenerator = obmProposalGenerator
    --------------------------------------------------
    let roundState = createRoundState-abs self now
    --------------------------------------------------
    let proposerElection = createProposerElection epochState0
    --------------------------------------------------
    let processor = RoundManager∙new
          obmNeedFetch
          epochState0
          blockStore
          roundState
          proposerElection
          proposalGenerator
          (safetyRules & srPersistentStorage ∙ pssSafetyData ∙ sdEpoch ∙~ epochState0 ^∙ esEpoch)
          (self ^∙ emConfig ∙ ccSyncOnly)
    --------------------------------------------------
    let (_ , processor' , output) = LBFT-run (RoundManager.start-abs now lastVote) processor
    case find' logErrMB output of λ where
      (just e) → err (here' ("RoundManager.start" ∷ [])) e
      nothing  → pure ( (self & emProcessor ?~ RoundProcessorNormal processor')
                      , output )

  abstract
    continue1-abs = continue1
    continue1-abs-≡ : continue1-abs ≡ continue1
    continue1-abs-≡ = refl

    continue2-abs = continue2
    continue2-abs-≡ : continue2-abs ≡ continue2
    continue2-abs-≡ = refl

abstract
  startRoundManager'-ed-abs = startRoundManager'-ed.step₀
  startRoundManager'-ed-abs-≡ : startRoundManager'-ed-abs ≡ startRoundManager'-ed.step₀
  startRoundManager'-ed-abs-≡ = refl

startProcessor-ed self now payload obmNeedFetch obmProposalGenerator obmLedgerInfoWithSignatures = do
  let validatorSet = payload ^∙ occpObmValidatorSet
  vv               ← ValidatorVerifier.from-ed-abs validatorSet
  let epochState0  = EpochState∙new (payload ^∙ occpEpoch) vv
      -- OBM TODO case storage.start of RecoveryData | LedgerRecoveryData
  (initialData , _pls)
                   ← MockStorage.startForTesting-ed-abs validatorSet
                                                        (just obmLedgerInfoWithSignatures)
  startRoundManager-ed self now initialData epochState0 obmNeedFetch obmProposalGenerator
                       (obmLedgerInfoWithSignatures ^∙ liwsLedgerInfo ∙ liVersion)

abstract
  startProcessor-e-abs
    : EpochManager → Instant → OnChainConfigPayload
    → ObmNeedFetch → ProposalGenerator → LedgerInfoWithSignatures
    → Either ErrLog  (EpochManager × List Output)
  startProcessor-e-abs em now payload nf pg liws = toEither $
     startProcessor-ed em now payload nf pg liws
  startProcessor-ed-abs = startProcessor-ed
  startProcessor-ed-abs-≡ : startProcessor-ed-abs ≡ startProcessor-ed
  startProcessor-ed-abs-≡ = refl

{-
Currently, the implementation is hooked up to the system model in
   'LibraBFT.Impl.Handle.InitAndHandlers'
It does so such that
- 'RoundManager' is the top-level state, and
- 'LibraBFT.Impl.IO.OBM.InputOutputHandlers.handle' is the top-level entry into the implementation.

In the future, when epoch changes are taken into account (and proved),
- 'EpochManager' will become the top-level state
- 'EpochManager.processMessage' will become the top-level entry into the implementation.

That said, when that change is made, there will be a new obligation.
Currently, when 'InputOutputHandlers.handle' cases have been covered, a proof is done.
But, in the future, when proving properties of 'EpochManager.processMessage'
(besides covering the epoch change properties) when the output is 'PMInput' it will be necessary
to "pass" that input to the 'RoundManager' level and continue proving from there.
-}
processMessage
  : EpochManager → Instant → Input
  → EM ProcessMessageAction
processMessage self now = λ where
  a@(IBlockRetrievalRequest  _ _) → pure (PMInput a)
  a@(IBlockRetrievalResponse _ _) → pure (PMInput a)
  (IEpochChangeProof from (ECPWire∙new {-why e r-} ecp))
                                  → do
                                    tell (PMInfo fakeInfo ∷ [])
                                     --[ "processEpochChangeProof"
                                     -- , why, lsA from, lsE e, lsR r, lsECP ecp ]))]
                                    doECP ecp
  (IEpochRetrievalRequest frm a@(EpRRqWire∙new {- _why _e _r -} epRrq))
                                  → eitherSD (self ^∙ emEpoch)
                                             (λ e -> do tell (PMErr (withErrCtx (here' []) e) ∷ [])
                                                        pure PMContinue)
                                             $ λ epoch' →
                                        ifD (epRrq ^∙ eprrqEndEpoch >? epoch')
                                        then (do
                                          tell (PMInfo fakeInfo ∷ [])
                                             --["EpochRRq beyond ours", why, lsE (epRrq^.eprrqEndEpoch)]))]
                                          pure PMContinue)
                                        else processEpochRetrieval self {-"wire"-} a frm
  a@(IInit _)                     → pure (PMInput a)
  a@(IProposal _ from pm)         → maybeDifferentEpoch a from (pm ^∙ pmEpoch) (pm ^∙ pmRound)
  (IReconfigLocalEpochChange rlec) → do
                                     tell (PMInfo fakeInfo ∷ []) --(here ["receive", lsRLEC rlec]))]
                                     doRLEC rlec
  a@(ISyncInfo _ from si)         → case
                                      ECP-LBFT-OBM-Diff-1.e_EpochManager_processMessage_ISyncInfo
                                        self si of λ where
                                      (Left  e) → do tell (PMErr e ∷ [])
                                                     pure PMContinue
                                      (Right _) →
                                        maybeDifferentEpoch a from (si ^∙ siEpoch) (si ^∙ siObmRound)
  a@(ITimeout _ _ _ _)            → pure (PMInput a)
  a@(IVote _ from vm)             → maybeDifferentEpoch a from (vm ^∙ vmEpoch) (vm ^∙ vmRound)
 where
  doRlecEcp : Maybe ReconfigEventEpochChange → EpochChangeProof → EM ProcessMessageAction

  here' : List String → List String
  here' t = "EpochManager" ∷ "processMessage" ∷ t

  maybeDifferentEpoch : Input → AccountAddress → Epoch → Round → EM ProcessMessageAction
  maybeDifferentEpoch a from e r =
    eitherSD (self ^∙ emEpoch) (λ err → do tell (PMErr (withErrCtx (here' []) err) ∷ []); pure PMContinue) $ λ epoch' →
        ifD e == epoch'
        then pure (PMInput a)
        else processDifferentEpoch self a from e r

  doECP : EpochChangeProof → EM ProcessMessageAction
  doECP ecp = get >>= λ where
    RSNothing → case ECP-LBFT-OBM-Diff-1.e_EpochManager_checkEpc self ecp of λ where
      (Left e)  → do
        tell (PMErr e ∷ [])
        pure PMContinue
      (Right _) → do
       eitherSD (ECP-LBFT-OBM-Diff-1.e_EpochManager_doECP_waitForRlec self ecp)
                (λ e → do tell (PMErr (withErrCtx (here' []) e) ∷ []); pure PMContinue)
                $ λ b →
        ifD b
          then (do
          tell (PMInfo fakeInfo ∷ []) -- [ "doECP", "got ECP", "waiting for RLEC"
                                      -- , "my epoch", lsEE (self^.emEpoch), lsECP ecp])]
          put (RSNeedRLEC ecp)
          pure PMContinue)
          else do
          tell (PMInfo fakeInfo ∷ []) -- ["doECP", "got ECP", "NOT waiting for RLEC"
                                      -- , "my epoch", lsEE (self^.emEpoch), lsECP ecp])]
          put RSNothing
          doRlecEcp nothing ecp
    (RSNeedRLEC ecpX) → do
        tell (PMInfo fakeInfo ∷ []) -- ["got another ECP while waiting for RLEC", lsECP ecp, lsECP ecpX])]
        pure PMContinue  -- TODO
    (RSNeedECP rlec) → do
        put RSNothing
        doRlecEcp (just rlec) ecp

  doRLEC : ReconfigEventEpochChange → EM ProcessMessageAction
  doRLEC rlec = get >>= λ where
    RSNothing → do
        tell (PMInfo fakeInfo ∷ []) -- ["doRLEC", "got RLEC", "waiting for ECP", lsRLEC rlec])]
        put (RSNeedECP rlec)
        pure PMContinue
    (RSNeedRLEC ecp) → do
        put  RSNothing
        doRlecEcp (just rlec) ecp
    (RSNeedECP rlecX) → do
        tell (PMInfo fakeInfo ∷ [])
             -- ["doRLEC", "got another RLEC while waiting for ECP", lsRLEC rlec, lsRLEC rlecX])]
        pure PMContinue  -- TODO

  doRlecEcp rlec ecp =
    case startNewEpoch self now rlec ecp of λ where
      (Left err) → do
        tell (PMErr err ∷ [])
        pure PMContinue
      (Right r) → pure r

expectNewEpoch self now (ReconfigEventEpochChange∙new payload) obmLedgerInfoWithSignatures = do
  rm       ← self ^∙ emObmRoundManager
  (em , o) ← startProcessor-e-abs self now payload
               (rm ^∙ rmObmNeedFetch)
               (rm ^∙ rmProposalGenerator)
               obmLedgerInfoWithSignatures
  pure (PMNewEpoch em o)

start-ed
  : EpochManager → Instant
  → OnChainConfigPayload → ObmNeedFetch → ProposalGenerator → LedgerInfoWithSignatures
  → EitherD ErrLog (EpochManager × List Output)
start-ed self0 now obmPayload obmNeedFetch obmProposalGenerator obmLedgerInfoWithSignatures =
  startProcessor-ed self0 now obmPayload obmNeedFetch obmProposalGenerator obmLedgerInfoWithSignatures

------------------------------------------------------------------------------
-- IMPL-DIFF
{-
'obmStartLoop' is the function that
- gets input (e.g., from the network)
- runs that input through the EpochManager in the 'EM' monad
- logs any errors that happen in the EpochManager
- dispatches on the output of the EpochManager
  - in some  cases it runs the RoundManager in the LBFT monad
  - in other cases it sends messages (via 'stps') to other nodes

The following "implementation" compiles, but has lots of TEMPORARY things to get it to compile.
In the proofs, the System Model "handles" input and output.
Therefore 'obmStartLoop' will not be implemented nor "proved".
It is here to show what is done in the Haskell code.
If the Agda code were ever to be extracted to executable Haskell code,
then this code would be completed.

The system model will be instantiated with 'EpochManager.processMessage'
and that will be the system about which properties are proved.
See the comments before that function.
-}

IO : Set → Set₁
IO = RWS Unit Unit Unit

{-# TERMINATING #-}
obmStartLoop
  : EpochManager → List Output
  {-→ CLI.FakeNetworkDelay → DAR.DispatchConfig a → INPUT_CHANNEL_READ a-}
  → IO Unit
obmStartLoop self initializationOutput
             {-(CLI.FakeNetworkDelay fnd)
             (DAR.DispatchConfig _rm0 toDAR ih oh lg lc stps m)
             lbftInR-} = do
  eitherS (self ^∙ emObmRoundManager) ee $ λ rm → do
    -- This line roughly corresponds to Rust expect_new_epoch.
    -- It processes the output from start/startProcessor above.
    -- TODO (rm' , to') ← DAR.runOutputHandler rm toDAR pe initializationOutput oh
    rm'                 ← pure rm -- TEMPORARY for previous line
    loop (setProcessor self rm') {-to'-} RSNothing
 where
  show : ∀ {A : Set} → A → String
  show _ = ""

  singleShow : ∀ {A : Set} → A → List String
  singleShow {A} x = show {A} x ∷ []

  errorExit : List String → IO Unit
  errorExit _ = pure unit

  here' : List String → List String
  here' t = "EpochManager" ∷ "obmStartLoop" ∷ t

  ee : ErrLog → IO Unit
  ee = errorExit ∘ here' ∘ singleShow

  setProcessor : EpochManager → RoundManager → EpochManager
  setProcessor em p = em & emProcessor ?~ RoundProcessorNormal p

  loop : EpochManager {-→ Map ScheduledInputKey ThreadId-} → RlecState → IO Unit
  loop em {-to-} rlec0 = do
    -- i ← U.readChan lbftInR
    i ← pure (IInit 0) -- TEMPORARY for previous line
    -- when (fnd > 0) $
    --  threadDelay (fnd * oneMillisecond)
    -- now                    ← Time.getCurrentInstant
    now                    ← pure (0) -- TEMPORARY for previous line
    let (pma , rlec , pmo) = runEM (processMessage em now i) rlec0
    let myName             = em ^∙ emAuthor ∙ aAuthorName
    forM_ pmo $ λ where
      -- (PMErr  (ErrInfo (lc', x)) → Logger.log (lg myName) lc (LogInfo lc' x)
      (PMErr  x)                        → pure unit -- Logger.log (lg myName) lc (LogErr      x)
      (PMInfo x)                        → pure unit -- Logger.log (lg myName) lc (LogInfo lEC x)
    case pma of λ where
      PMContinue →
        loop em {-to-} rlec
      (PMInput i') →
       eitherSD (em ^∙ emObmRoundManager) ee $ λ rm → do
        --(rm'  ,    o) ← DAR.runInputHandler  rm  to pe i' ih
        --(rm'' , to'') ← DAR.runOutputHandler rm' to pe o  oh
        rm'' ← pure rm -- TEMPORARY for previous two lines
        loop (setProcessor em rm'') {-to''-} rlec
      (PMNewEpoch em' newEpochInitializationOutput) → do
       eitherSD (em' ^∙ emObmRoundManager) ee $ λ rm → do
        -- (rm', to') ← DAR.runOutputHandler   rm  to pe newEpochInitializationOutput oh
        rm' ← pure rm -- TEMPORARY for previous line
        loop (setProcessor em' rm') {-to'-} RSNothing -- reset RLEC state
      (PMSendECP ecp peerAddress me {-why-} e r) → do
        -- stps [peerAddress ^∙ aAuthorName] (Messages.mkIEpochChangeProof me why e r ecp)
        loop em {-to-} rlec
      (PMSendEpochRRq epRrq sendTo) → do
        -- stps [sendTo ^∙ aAuthorName] (IEpochRetrievalRequest (em ^∙ emAuthor) epRrq)
        loop em {-to-} rlec
{-
  pe = PeerEnv
    (""::Text)
    Map.empty
    (RunEnv
      (lg (self ^∙ emAuthor.aAuthorName))
      lc
      (Just stps)
      (Just m))
-}


text:
------------------------------------------------------------------------
-- From the Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------

module Common.Size where

open import Agda.Builtin.Size public renaming (ω to ∞; SizeU to SizeUniv)


text:
module cfg1 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat  hiding ( _≟_ )
-- open import Data.Fin
-- open import Data.Product
open import Data.List
open import Data.Maybe
-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import logic

--
--   Java → Java Byte Code
--
--   CFG    Stack Machine (PDA)
--

data Node (Symbol  : Set) : Set where
    T : Symbol → Node Symbol
    N : Symbol → Node Symbol

data Seq (Symbol  : Set) : Set where
    _，_   :  Symbol  → Seq Symbol  → Seq Symbol
    _．    :  Symbol  → Seq Symbol
    Error    :  Seq Symbol

data Body (Symbol  : Set) : Set where
    _｜_   :  Seq Symbol  → Body Symbol  → Body Symbol
    _；    :  Seq Symbol  → Body Symbol

record CFGGrammer  (Symbol  : Set) : Set where
   field
      cfg : Symbol → Body Symbol
      top : Symbol
      eq? : Symbol → Symbol → Bool
      typeof : Symbol →  Node Symbol

infixr  80 _｜_
infixr  90 _；
infixr  100 _，_
infixr  110 _．

open CFGGrammer

-----------------
--
-- CGF language
--
-----------------

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] /\ y []
split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

cfg-language0 :  {Symbol  : Set} → CFGGrammer Symbol   → Body Symbol  →  List Symbol → Bool

{-# TERMINATING #-}
cfg-language1 :  {Symbol  : Set} → CFGGrammer Symbol   → Seq Symbol  →  List Symbol → Bool
cfg-language1 cg Error x = false
cfg-language1 cg (S ， seq) x with typeof cg S
cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eq? cg x x' /\ cfg-language1 cg seq t
cfg-language1 cg (_ ， seq) [] | T x = false
cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
cfg-language1 cg (S ．) x with typeof cg S
cfg-language1 cg (_ ．) (x' ∷ []) | T x =  eq? cg x x'
cfg-language1 cg (_ ．) _ | T x = false
cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x

cfg-language0 cg _ [] = false
cfg-language0 cg (rule ｜ b) x =
     cfg-language1 cg rule x  \/ cfg-language0 cg b x
cfg-language0 cg (rule ；) x = cfg-language1 cg rule x

cfg-language :  {Symbol  : Set} → CFGGrammer Symbol   → List Symbol → Bool
cfg-language cg = cfg-language0 cg (cfg cg (top cg ))

data IFToken : Set where
   EA : IFToken
   EB : IFToken
   EC : IFToken
   IF : IFToken
   THEN : IFToken
   ELSE : IFToken
   SA : IFToken
   SB : IFToken
   SC : IFToken
   expr : IFToken
   statement : IFToken

token-eq? : IFToken → IFToken → Bool
token-eq? EA EA = true
token-eq? EB EB = true
token-eq? EC EC =  true
token-eq? IF IF =  true
token-eq? THEN THEN =  true
token-eq? ELSE ELSE = true
token-eq? SA SA =  true
token-eq? SB SB =  true
token-eq? SC SC = true
token-eq? expr expr = true
token-eq? statement statement = true
token-eq? _ _ = false

typeof-IFG : IFToken → Node IFToken
typeof-IFG expr = N expr
typeof-IFG statement = N statement
typeof-IFG x = T x

IFGrammer : CFGGrammer IFToken
IFGrammer = record {
      cfg = cfg'
    ; top = statement
    ; eq? = token-eq?
    ; typeof = typeof-IFG
   } where
     cfg' : IFToken → Body IFToken
     cfg' expr =  EA ． ｜  EB ．  ｜   EC ． ；
     cfg' statement =
           SA ． ｜   SB ．  ｜   SC ．
         ｜  IF ，  expr ， THEN ， statement ．
         ｜  IF ，  expr ， THEN ， statement  ，  ELSE  ，  statement ．
         ；
     cfg' x =  Error  ；

cfgtest1 = cfg-language IFGrammer (  SA ∷ [] )

cfgtest2 = cfg-language1 IFGrammer ( SA   ．) (  SA ∷ [] )

cfgtest3 = cfg-language1 IFGrammer ( SA    ．  ) (  SA ∷ [] )

cfgtest4 = cfg-language IFGrammer  (IF  ∷ EA ∷ THEN  ∷ SA ∷ [] )

cfgtest5 = cfg-language1 IFGrammer ( IF  ，  expr  ， THEN ，  statement  ． ) (IF  ∷ EA ∷ THEN  ∷ SA ∷ [] )
cfgtest6 = cfg-language1 IFGrammer ( statement  ．)(IF  ∷ EA ∷ SA ∷ [] )
cfgtest7 = cfg-language1 IFGrammer ( IF   ，   expr   ， THEN   ，   statement   ，   ELSE    ，   statement   ． )
    (IF  ∷ EA ∷ THEN   ∷ SA ∷ ELSE  ∷ SB  ∷ [] )
cfgtest8 = cfg-language IFGrammer  (IF ∷ EA ∷ THEN  ∷ IF ∷ EB ∷ THEN  ∷ SA ∷ ELSE  ∷ SB  ∷ [] )
cfgtest9 = cfg-language IFGrammer  (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE  ∷ SB  ∷ [] )

data E1Token : Set where
   e1 : E1Token
   e[ : E1Token
   e] : E1Token
   expr : E1Token
   term : E1Token

E1-token-eq? : E1Token → E1Token → Bool
E1-token-eq? e1 e1 = true
E1-token-eq? e[ e] = true
E1-token-eq? e] e] = true
E1-token-eq? expr expr = true
E1-token-eq? term term = true
E1-token-eq? _ _ = false

typeof-E1 : E1Token → Node E1Token
typeof-E1 expr = N expr
typeof-E1 term = N term
typeof-E1 x = T x

E1Grammer : CFGGrammer E1Token
E1Grammer = record {
      cfg = cfgE
    ; top = expr
    ; eq? = E1-token-eq?
    ; typeof = typeof-E1
   } where
     cfgE : E1Token → Body E1Token
     cfgE expr = term ．
       ；
     cfgE term = e1  ．
       ｜   e[   ， expr  ，  e]   ．
       ；
     cfgE x = Error  ；

ecfgtest1 = cfg-language E1Grammer (  e1 ∷ [] )
ecfgtest2 = cfg-language E1Grammer (  e[ ∷ e1 ∷ e] ∷ [] )
ecfgtest3 = cfg-language E1Grammer (  e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] )
ecfgtest4 = cfg-language E1Grammer (  e[ ∷ e1 ∷ [] )

open import Function

left : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
left ( e[ ∷ t ) fail next = next t
left t fail next = fail t

right : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
right ( e] ∷ t ) fail next = next t
right t fail next = fail t

{-# TERMINATING #-}
expr1 : {t : Set } → List E1Token → ( fail next : List E1Token → t ) → t
expr1 ( e1 ∷ t ) fail next = next t
expr1 ( expr ∷ t ) fail next = next t
expr1 ( term  ∷ t ) fail next = next t
expr1 x fail next = left x fail $ λ x → expr1 x fail $ λ x → right x fail $ next
-- expr1 x fail next = left x fail ( λ x → expr1 x fail ( λ x → right x fail ( next )))

cfgtest01  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ )
cfgtest02  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x →  ⟪ true , x ⟫ )
cfgtest03  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x →  ⟪ true , x ⟫ )

open import pushdown

data CG1 : Set where
   ce : CG1
   c1 : CG1

pd  : CG1 → E1Token → CG1 → CG1 ∧ PushDown CG1
pd c1 e[ s = ⟪ c1 , push c1 ⟫
pd c1 e] c1 = ⟪ c1 , pop ⟫
pd c1 e1 c1 = ⟪ c1 , none ⟫
pd s expr s1 = ⟪ c1 , none ⟫
pd s term s1 = ⟪ c1 , none ⟫
pd s _ s1 = ⟪ ce , none ⟫

pok  : CG1 → Bool
pok c1  = true
pok s  = false

pnc : PushDownAutomaton CG1 E1Token CG1
pnc = record {
         pδ  = pd
      ;  pempty = ce
      ;  pok = pok
   }

pda-ce-test1 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) []
pda-ce-test2 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) []
pda-ce-test3 = PushDownAutomaton.paccept pnc c1 ( e[ ∷ e1 ∷ e] ∷ e1 ∷ [] ) []

record PNC (accept : Bool )  : Set where
  field
    orig-x : List E1Token
    pnc-q : CG1
    pnc-st : List CG1
    pnc-p : CG1 → List CG1 → Bool
    success : accept ≡ true  → pnc-p pnc-q pnc-st ≡ true  → PushDownAutomaton.paccept pnc c1 orig-x []  ≡ true
    failure : accept ≡ false → pnc-p pnc-q pnc-st ≡ false → PushDownAutomaton.paccept pnc c1 orig-x [] ≡ false

open import Data.Unit

{-# TERMINATING #-}
expr1P : {n : Level } {t : Set n } → (x : List E1Token ) → PNC true
    → ( fail : List E1Token → PNC false → t ) → ( next : List E1Token → PNC true → t ) → t
expr1P x _ _ _ = {!!}

expr1P-test : (x : List E1Token ) →  ⊤
expr1P-test x = expr1P x record { orig-x = x ; pnc-q = c1 ; pnc-st = []
      ; pnc-p = λ q st → PushDownAutomaton.paccept pnc q x st ; success = λ _ p → p ; failure = λ _ p → p }
      (λ x p → {!!} ) (λ x p → {!!} )

----
--
--  CFG to PDA
--

cfg→pda-state :  {Symbol  : Set} → CFGGrammer Symbol → Set
cfg→pda-state cfg = {!!}

cfg→pda-start :  {Symbol  : Set} → (cfg : CFGGrammer Symbol) → cfg→pda-state cfg
cfg→pda-start cfg = {!!}

cfg→pda :  {Symbol  : Set} → (cfg : CFGGrammer Symbol) → PDA (cfg→pda-state cfg) Symbol (cfg→pda-state cfg)
cfg→pda cfg = {!!}

cfg->pda : {Symbol  : Set} → (input : List Symbol)
    → (cfg : CFGGrammer Symbol)
    → PDA.paccept (cfg→pda cfg ) (cfg→pda-start cfg) input [] ≡  cfg-language cfg input
cfg->pda = {!!}

----
--
--  PDA to CFG
--
open import pushdown

pda→cfg :  {Symbol  : Set} { Q : Set} → (pda : PDA Q Symbol Q) → CFGGrammer Symbol
pda→cfg pda = record {
      cfg = {!!}
    ; top = {!!}
    ; eq? = {!!}
    ; typeof = {!!}
   }

pda->cfg : {Symbol  : Set} { Q : Set} → (start : Q) →  (input : List Symbol)
    → (pda : PDA  Q Symbol Q)
    → PDA.paccept pda start input [] ≡  cfg-language (pda→cfg pda) input
pda->cfg = {!!}

record CDGGrammer  (Symbol  : Set) : Set where
   field
      cdg : Seq Symbol  → Body Symbol
      top : Symbol
      eq? : Symbol → Symbol → Bool
      typeof : Symbol →  Node Symbol

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
open import Agda.Builtin.Equality

variable
  A B : Set
  f g : A

postulate
  F   : Set → Set
  map : (A → B) → F A → F B

lemma : (x : F A) → map (λ x → f (g x)) x ≡ map f (map g x) → F A
lemma {A = A} {f = f} {g = g} x _ = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Coinductive higher lenses with erased "proofs"
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Coinductive.Erased
  {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

import Colimit.Sequential.Very-erased eq as CS
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages.Cubical eq
  using (_⁻¹ᴱ_)
open import Erased.Cubical eq
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.Erased eq as T
  using (∥_∥ᴱ; ∣_∣)
import H-level.Truncation.Propositional.Non-recursive.Erased eq as N
open import H-level.Truncation.Propositional.One-step eq as O
  using (∣_∣; ∥_∥¹-out-^; ∥_∥¹-in-^; ∣_,_∣-in-^)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher.Erased eq as Higher
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant eq
  as V
open import Lens.Non-dependent.Higher.Coherently.Coinductive eq
import Lens.Non-dependent.Higher.Coinductive eq as C
import Lens.Non-dependent.Higher.Coinductive.Small eq as S

private
  variable
    a b p : Level
    A B   : Type a
    n     : ℕ

------------------------------------------------------------------------
-- The lemma ∥∥ᴱ→≃

private

  -- A lemma used in the implementation of ∥∥ᴱ→≃.
  --
  -- This definition is erased because its implementation makes use of
  -- code related to O.∥_∥¹ (a HIT with a non-erased higher
  -- constructor).

  @0 ∥∥ᴱ→≃-lemma :
    Block "∥∥ᴱ→≃-lemma" →
    (f₀ : A → B) →
    (∃ λ (f₊ : ∀ n → ∥ A ∥¹-out-^ (1 + n) → B) →
       (∀ x → f₊ zero ∣ x ∣ ≡ f₀ x) ×
       (∀ n x → f₊ (suc n) ∣ x ∣ ≡ f₊ n x)) ≃
    (∃ λ (f₊ : ∀ n → ∥ A ∥¹-in-^ (1 + n) → B) →
       (∀ x → f₊ zero ∣ x ∣ ≡ f₀ x) ×
       (∀ n x → f₊ (suc n) ∣ n , x ∣-in-^ ≡ f₊ n x))
  ∥∥ᴱ→≃-lemma ⊠ _ =
    inverse $
    Σ-cong {k₁ = equivalence}
      (∀-cong ext λ n →
       →-cong₁ ext (inverse $ O.∥∥¹-out-^≃∥∥¹-in-^ (suc n))) λ f →
    ∃-cong λ _ → ∀-cong ext λ n →
    Π-cong-contra ext (O.∥∥¹-out-^≃∥∥¹-in-^ (suc n)) λ x →
    ≡⇒≃ $ cong (λ y → f (suc n) y ≡
                      f n (_≃_.to (O.∥∥¹-out-^≃∥∥¹-in-^ (suc n)) x)) $
    sym $ O.∣∣≡∣,∣-in-^ (1 + n)

-- Functions from ∥ A ∥ᴱ can be expressed as coherently constant
-- functions from A with erased "proofs" (assuming univalence).

∥∥ᴱ→≃ :
  Block "∥∥ᴱ→≃" →
  {A : Type a} {B : Type b} →
  @0 Univalence (a ⊔ b) →
  (∥ A ∥ᴱ → B)
    ≃
  (∃ λ (f : A → B) → Erased (C.Coherently-constant f))
∥∥ᴱ→≃ bl {A = A} {B = B} univ =
  (∥ A ∥ᴱ → B)                                                 ↝⟨ →-cong ext T.∥∥ᴱ≃∥∥ᴱ F.id ⟩

  (N.∥ A ∥ᴱ → B)                                               ↝⟨ CS.universal-property ⟩

  (∃ λ (f₀ : A → B) →
     Erased (∃ λ (f₊ : ∀ n → ∥ A ∥¹-out-^ (1 + n) → B) →
               (∀ x → f₊ zero ∣ x ∣ ≡ f₀ x) ×
               (∀ n x → f₊ (suc n) ∣ x ∣ ≡ f₊ n x)))           ↝⟨ ∃-cong (λ f → Erased-cong (∥∥ᴱ→≃-lemma bl f)) ⟩

  (∃ λ (f₀ : A → B) →
     Erased (∃ λ (f₊ : ∀ n → ∥ A ∥¹-in-^ (1 + n) → B) →
               (∀ x → f₊ zero ∣ x ∣ ≡ f₀ x) ×
               (∀ n x → f₊ (suc n) ∣ n , x ∣-in-^ ≡ f₊ n x)))  ↝⟨ ∃-cong (λ f → Erased-cong (inverse $
                                                                  C.Coherently-constant′≃ bl)) ⟩

  (∃ λ (f : A → B) → Erased (C.Coherently-constant′ f))        ↝⟨ ∃-cong (λ f → Erased-cong (inverse $
                                                                  C.Coherently-constant≃Coherently-constant′ bl univ)) ⟩□
  (∃ λ (f : A → B) → Erased (C.Coherently-constant f))         □

-- A "computation" rule for ∥∥ᴱ→≃.

@0 cong-from-∥∥ᴱ→≃-truncation-is-proposition :
  (bl : Block "∥∥ᴱ→≃")
  {A : Type a} {B : Type b}
  (univ : Univalence (a ⊔ b)) →
  {f : A → B} {c : C.Coherently-constant f}
  {x y : A} {p : ∣ x ∣ ≡ ∣ y ∣} →
  cong (_≃_.from (∥∥ᴱ→≃ bl univ) (f , [ c ])) p ≡
  c .property x y
cong-from-∥∥ᴱ→≃-truncation-is-proposition
  bl {A = A} univ {f = f} {c = c} {x = x} {y = y} {p = p} =
  cong (_≃_.from (∥∥ᴱ→≃ bl univ) (f , [ c ])) p                         ≡⟨⟩

  cong (_≃_.from CS.universal-property (f , [ g bl ]) ∘
        _≃_.to T.∥∥ᴱ≃∥∥ᴱ)
    p                                                                   ≡⟨ sym $ cong-∘ _ _ _ ⟩

  (cong (_≃_.from CS.universal-property (f , [ g bl ])) $
   cong (_≃_.to T.∥∥ᴱ≃∥∥ᴱ) p)                                           ≡⟨ cong (cong _) $ mono₁ 1 N.∥∥ᴱ-proposition _ _ ⟩

  cong (_≃_.from CS.universal-property (f , [ g bl ]))
    (N.∥∥ᴱ-proposition N.∣ x ∣ N.∣ y ∣)                                 ≡⟨⟩

  cong (_≃_.from CS.universal-property (f , [ g bl ]))
    (trans (sym (CS.∣∣₊≡∣∣₀ x))
       (trans (cong CS.∣_∣₊ (O.∣∣-constant x y))
          (CS.∣∣₊≡∣∣₀ y)))                                              ≡⟨ trans (cong-trans _ _ _) $
                                                                           cong₂ trans
                                                                             (cong-sym _ _)
                                                                             (trans (cong-trans _ _ _) $
                                                                              cong (flip trans _) $
                                                                              cong-∘ _ _ _) ⟩
  trans
    (sym $ cong (_≃_.from CS.universal-property (f , [ g bl ]))
             (CS.∣∣₊≡∣∣₀ x))
    (trans
       (cong (_≃_.from CS.universal-property (f , [ g bl ]) ∘ CS.∣_∣₊)
          (O.∣∣-constant x y))
       (cong (_≃_.from CS.universal-property (f , [ g bl ]))
          (CS.∣∣₊≡∣∣₀ y)))                                              ≡⟨ cong₂ trans
                                                                             (cong sym CS.rec-∣∣₊≡∣∣₀)
                                                                             (cong (trans _) CS.rec-∣∣₊≡∣∣₀) ⟩
  trans (sym $ proj₁ (proj₂ (g bl)) x)
    (trans (cong (proj₁ (g bl) 0) (O.∣∣-constant x y))
       (proj₁ (proj₂ (g bl)) y))                                        ≡⟨ lemma bl ⟩∎

  c .property x y                                                       ∎
  where
  g : ∀ _ → _
  g bl =
    _≃_.from (∥∥ᴱ→≃-lemma bl _) $
    _≃_.to (C.Coherently-constant′≃ bl) $
    _≃_.to (C.Coherently-constant≃Coherently-constant′ bl univ) c

  lemma :
    ∀ bl →
    trans (sym $ proj₁ (proj₂ (g bl)) x)
      (trans (cong (proj₁ (g bl) 0) (O.∣∣-constant x y))
         (proj₁ (proj₂ (g bl)) y)) ≡
    c .property x y
  lemma bl@⊠ =
    trans (sym $ proj₁ (proj₂ (g bl)) x)
      (trans (cong (proj₁ (g bl) 0) (O.∣∣-constant x y))
         (proj₁ (proj₂ (g bl)) y))                                ≡⟨⟩

    trans (sym $ refl _)
      (trans (cong (O.rec′ f (c .property)) (O.∣∣-constant x y))
         (refl _))                                                ≡⟨ trans (cong₂ trans sym-refl (trans-reflʳ _)) $
                                                                     trans-reflˡ _ ⟩

    cong (O.rec′ f (c .property)) (O.∣∣-constant x y)             ≡⟨ O.rec-∣∣-constant ⟩∎

    c .property x y                                               ∎

------------------------------------------------------------------------
-- Coherently-constant

-- Coherently constant type-valued functions.

Coherently-constant :
  {A : Type a} → (A → Type p) → Type (a ⊔ lsuc p)
Coherently-constant P =
  ∃ λ (f : ∀ x y → P x → P y) →
  Erased (∃ λ (c : C.Coherently-constant P) →
          ∀ x y → f x y ≡ subst id (c .property x y))

-- Coherently-constant is pointwise equivalent (with erased proofs) to
-- V.Coherently-constant (assuming univalence).

Coherently-constant≃ᴱCoherently-constant :
  {A : Type a} {P : A → Type p} →
  @0 Univalence (a ⊔ lsuc p) →
  @0 Univalence p →
  Coherently-constant P ≃ᴱ V.Coherently-constant P
Coherently-constant≃ᴱCoherently-constant
  {a = a} {p = p} {A = A} {P = P} univ′ univ =
  block λ bl →

  Coherently-constant P                                                 ↔⟨⟩

  (∃ λ (P-const : ∀ x y → P x → P y) →
   Erased (
   ∃ λ (c : C.Coherently-constant P) →
   ∀ x y →
   P-const x y ≡ subst id (c .property x y)))                           ↔⟨ (∃-cong λ P-const → Erased-cong (
                                                                            ∃-cong λ c → ∀-cong ext λ x → ∀-cong ext λ y →
                                                                            ≡⇒≃ $ cong (P-const x y ≡_) (
      subst id (c .property x y)                                            ≡⟨ cong (subst id) $ sym $
                                                                                cong-from-∥∥ᴱ→≃-truncation-is-proposition bl univ′ ⟩
      subst id
        (cong (_≃_.from (∥∥ᴱ→≃ bl univ′) (P , [ c ]))
           (T.truncation-is-proposition ∣ x ∣ ∣ y ∣))                       ≡⟨ (⟨ext⟩ λ _ → sym $
                                                                                subst-∘ _ _ _) ⟩∎
      subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (P , [ c ]))
        (T.truncation-is-proposition ∣ x ∣ ∣ y ∣)                           ∎))) ⟩

  (∃ λ (P-const : ∀ x y → P x → P y) →
   Erased (
   ∃ λ (c : C.Coherently-constant P) →
   ∀ x y →
   P-const x y ≡
   subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (P , [ c ]))
     (T.truncation-is-proposition ∣ x ∣ ∣ y ∣)))                        ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ →
                                                                            Eq.extensionality-isomorphism bad-ext F.∘
                                                                            (∀-cong ext λ _ → Eq.extensionality-isomorphism bad-ext))) ⟩
  (∃ λ (P-const : ∀ x y → P x → P y) →
   Erased (
   ∃ λ (c : C.Coherently-constant P) →
   P-const ≡
   λ x y →
   subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (P , [ c ]))
     (T.truncation-is-proposition ∣ x ∣ ∣ y ∣)))                        ↔⟨ (∃-cong λ P-const → Erased-cong (
                                                                            ∃-cong λ c → ≡⇒≃ $ cong (P-const ≡_) $ sym $
                                                                            ⟨ext⟩ λ x → ⟨ext⟩ λ y →
                                                                            cong₂ (λ (f : P y → P y) (g : P x → P x) →
                                                                                f ∘
                                                                                subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (P , [ c ]))
                                                                                (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
                                                                                g)
                                                                              (cong _≃_.to $
                                                                               trans (cong ≡⇒≃ $ cong-refl (_$ y)) $
                                                                               ≡⇒↝-refl)
                                                                              (cong _≃_.from $
                                                                               trans (cong ≡⇒≃ $ cong-refl (_$ x)) $
                                                                               ≡⇒↝-refl))) ⟩
  (∃ λ (P-const : ∀ x y → P x → P y) →
   Erased (
   ∃ λ (c : C.Coherently-constant P) →
   P-const ≡
   λ x y →
   ≡⇒→ (cong (_$ y) (refl P)) ∘
   subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (P , [ c ]))
     (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
   _≃_.from (≡⇒≃ (cong (_$ x) (refl P)))))                              ↝⟨ (∃-cong λ P-const → inverse $
                                                                            EEq.drop-⊤-left-Σ-≃ᴱ-Erased
                                                                              (EEq.other-singleton-with-Π-≃ᴱ-≃ᴱ-⊤ ext univ)) ⟩
  (∃ λ (P-const : ∀ x y → P x → P y) →
   ∃ λ ((Q , P≃) : ∃ λ (Q : A → Type p) → ∀ x → P x ≃ᴱ Q x) →
   Erased (
   ∃ λ (c : C.Coherently-constant Q) →
   P-const ≡
   λ x y →
   _≃ᴱ_.from (P≃ y) ∘
   subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (Q , [ c ]))
     (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
   _≃ᴱ_.to (P≃ x)))                                                     ↔⟨ (∃-cong λ _ →
                                                                            Σ-assoc F.∘
                                                                            (∃-cong λ _ → ∃-comm) F.∘
                                                                            inverse Σ-assoc F.∘
                                                                            (∃-cong λ _ → Erased-Σ↔Σ)) ⟩
  (∃ λ (P-const : ∀ x y → P x → P y) →
   ∃ λ ((Q , c) : ∃ λ (Q : A → Type p) →
                  Erased (C.Coherently-constant Q)) →
   ∃ λ (P≃ : ∀ x → P x ≃ᴱ Q x) →
   Erased (P-const ≡
           λ x y →
           _≃ᴱ_.from (P≃ y) ∘
           subst (_≃_.from (∥∥ᴱ→≃ bl univ′) (Q , c))
             (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
           _≃ᴱ_.to (P≃ x)))                                             ↔⟨ (∃-cong λ _ →
                                                                            Σ-cong (inverse $ ∥∥ᴱ→≃ bl univ′) λ _ → Eq.id) ⟩
  (∃ λ (P-const : ∀ x y → P x → P y) →
   ∃ λ (Q : ∥ A ∥ᴱ → Type p) →
   ∃ λ (P≃ : ∀ x → P x ≃ᴱ Q ∣ x ∣) →
   Erased (P-const ≡
           λ x y →
           _≃ᴱ_.from (P≃ y) ∘
           subst Q (T.truncation-is-proposition ∣ x ∣ ∣ y ∣) ∘
           _≃ᴱ_.to (P≃ x)))                                             ↔⟨⟩

  V.Coherently-constant′ P                                              ↝⟨ inverse V.Coherently-constant≃ᴱCoherently-constant′ ⟩□

  V.Coherently-constant P                                               □

------------------------------------------------------------------------
-- The lens type family

-- Coinductive lenses.

Lens : Type a → Type b → Type (lsuc (a ⊔ b))
Lens A B = ∃ λ (get : A → B) → Coherently-constant (get ⁻¹ᴱ_)

-- Some derived definitions.

module Lens {A : Type a} {B : Type b} (l : Lens A B) where

  -- A getter.

  get : A → B
  get = proj₁ l

  -- One can convert from any "preimage" (with an erased proof) of the
  -- getter to any other.

  get⁻¹ᴱ-const : (b₁ b₂ : B) → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂
  get⁻¹ᴱ-const b₁ b₂ = proj₁ (proj₂ l) b₁ b₂

  -- A setter.

  set : A → B → A
  set a b =                      $⟨ get⁻¹ᴱ-const (get a) b ⟩
    (get ⁻¹ᴱ get a → get ⁻¹ᴱ b)  ↝⟨ _$ (a , [ refl _ ]) ⟩
    get ⁻¹ᴱ b                    ↝⟨ proj₁ ⟩□
    A                            □

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 = Lens.get
    ; set = Lens.set
    }

-- Lens A B is equivalent to V.Lens A B (with erased proofs, assuming
-- univalence).

Lens≃ᴱLens :
  Block "Lens≃ᴱLens" →
  {A : Type a} {B : Type b} →
  @0 Univalence (lsuc (a ⊔ b)) →
  @0 Univalence (a ⊔ b) →
  Lens A B ≃ᴱ V.Lens A B
Lens≃ᴱLens ⊠ {A = A} {B = B} univ′ univ =
  (∃ λ (get : A → B) → Coherently-constant (get ⁻¹ᴱ_))    ↝⟨ (∃-cong λ _ →
                                                              Coherently-constant≃ᴱCoherently-constant univ′ univ) ⟩□
  (∃ λ (get : A → B) → V.Coherently-constant (get ⁻¹ᴱ_))  □

-- The right-to-left direction of the equivalence preserves getters
-- and setters.

from-Lens≃ᴱLens-preserves-getters-and-setters :
  (bl : Block "Lens≃ᴱLens")
  {A : Type a} {B : Type b}
  (@0 univ′ : Univalence (lsuc (a ⊔ b)))
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-→ A B
    (_≃ᴱ_.from (Lens≃ᴱLens bl univ′ univ))
from-Lens≃ᴱLens-preserves-getters-and-setters ⊠ _ _ l =
    refl _
  , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
    proj₁ (get⁻¹ᴱ-const (get a) b (a , [ refl (get a) ]))  ∎
  where
  open V.Lens l

-- In erased contexts the equivalence preserves getters and setters.
--
-- (I do not know if this result can be proved in non-erased
-- contexts.)

@0 Lens≃ᴱLens-preserves-getters-and-setters :
  (bl : Block "Lens≃ᴱLens")
  {A : Type a} {B : Type b}
  (@0 univ′ : Univalence (lsuc (a ⊔ b)))
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱLens bl univ′ univ))
Lens≃ᴱLens-preserves-getters-and-setters bl univ′ univ =
  Preserves-getters-and-setters-⇔-inverse
    {f = _≃ᴱ_.logical-equivalence
           (inverse $ Lens≃ᴱLens bl univ′ univ)} $
  Preserves-getters-and-setters-→-↠-⇔
    (_≃_.surjection (EEq.≃ᴱ→≃ $ inverse $ Lens≃ᴱLens bl univ′ univ))
    (from-Lens≃ᴱLens-preserves-getters-and-setters bl univ′ univ)

-- Lens A B is equivalent to Higher.Lens A B (with erased proofs,
-- assuming univalence).

Lens≃ᴱHigher-lens :
  Block "Lens≃ᴱHigher-Lens" →
  {A : Type a} {B : Type b} →
  @0 Univalence (lsuc (a ⊔ b)) →
  @0 Univalence (a ⊔ b) →
  Lens A B ≃ᴱ Higher.Lens A B
Lens≃ᴱHigher-lens bl {A = A} {B = B} univ′ univ =
  Lens A B         ↝⟨ Lens≃ᴱLens bl univ′ univ ⟩
  V.Lens A B       ↝⟨ V.Lens≃ᴱHigher-lens bl univ ⟩□
  Higher.Lens A B  □

-- In erased contexts the equivalence preserves getters and setters.

@0 Lens≃ᴱHigher-lens-preserves-getters-and-setters :
  (bl : Block "Lens≃ᴱHigher-lens")
  {A : Type a} {B : Type b}
  (@0 univ′ : Univalence (lsuc (a ⊔ b)))
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱHigher-lens bl univ′ univ))
Lens≃ᴱHigher-lens-preserves-getters-and-setters bl univ′ univ =
  Preserves-getters-and-setters-⇔-∘
    {f = _≃ᴱ_.logical-equivalence $ V.Lens≃ᴱHigher-lens bl univ}
    {g = _≃ᴱ_.logical-equivalence $ Lens≃ᴱLens bl univ′ univ}
    (V.Lens≃ᴱHigher-lens-preserves-getters-and-setters bl univ)
    (Lens≃ᴱLens-preserves-getters-and-setters bl univ′ univ)

------------------------------------------------------------------------
-- H-levels

-- If P has h-level n (pointwise), then Coherently-constant P has
-- h-level n (assuming univalence).

H-level-Coherently-constant :
  {A : Type a} {P : A → Type p} →
  @0 Univalence (lsuc (a ⊔ p)) →
  @0 Univalence (a ⊔ lsuc p) →
  @0 Univalence p →
  ((a : A) → H-level n (P a)) →
  H-level n (Coherently-constant P)
H-level-Coherently-constant {n = n} univ₁ univ₂ univ₃ h =
  Σ-closure n
    (Π-closure ext n λ _ →
     Π-closure ext n λ _ →
     Π-closure ext n λ _ →
     h _) λ _ →
  H-level-Erased n (
  Σ-closure n
    (S.H-level-Coinductive-Coherently-constant
       univ₁ univ₂ univ₃ h) λ _ →
  Π-closure ext n λ _ →
  Π-closure ext n λ _ →
  H-level.⇒≡ n $
  Π-closure ext n λ _ →
  h _)

-- If A and B have h-level n given the assumption that the other type
-- is inhabited, then Lens A B has h-level n (assuming univalence).

lens-preserves-h-level :
  {A : Type a} {B : Type b} →
  @0 Univalence (lsuc (a ⊔ b)) →
  @0 Univalence (a ⊔ b) →
  ∀ n → (B → H-level n A) → (A → H-level n B) →
  H-level n (Lens A B)
lens-preserves-h-level univ₁ univ₂ n hA hB =
  Σ-closure n
    (Π-closure ext n λ a →
     hB a) λ _ →
  H-level-Coherently-constant univ₁ univ₁ univ₂ λ b →
  Σ-closure n (hA b) λ a →
  H-level-Erased n (
  H-level.⇒≡ n (hB a))

-- If the domain of a lens is inhabited and has h-level n, then the
-- codomain also has h-level n (in erased contexts, assuming
-- univalence).

@0 h-level-respects-lens-from-inhabited :
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  Univalence (a ⊔ b) →
  ∀ n → Lens A B → A → H-level n A → H-level n B
h-level-respects-lens-from-inhabited univ′ univ n =
  Higher.h-level-respects-lens-from-inhabited n ∘
  _≃ᴱ_.to (Lens≃ᴱHigher-lens ⊠ univ′ univ)

-- If A has positive h-level n, then Lens A B also has h-level n (in
-- erased contexts, assuming univalence).

@0 lens-preserves-h-level-of-domain :
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  Univalence (a ⊔ b) →
  ∀ n → H-level (1 + n) A → H-level (1 + n) (Lens A B)
lens-preserves-h-level-of-domain univ′ univ n hA =
  H-level.[inhabited⇒+]⇒+ n λ l →
  lens-preserves-h-level univ′ univ (1 + n) (λ _ → hA) λ a →
  h-level-respects-lens-from-inhabited univ′ univ _ l a hA

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


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

open import LogicalFormulae
open import Categories.Definition
open import Categories.Functor.Definition

module Categories.Functor.Lemmas where

functorCompose : {a b c d e f : _} {B : Category {a} {b}} {C : Category {c} {d}} {D : Category {e} {f}} → (Functor C D) → (Functor B C) → (Functor B D)
functorCompose G F = record { onObj = λ x → Functor.onObj G (Functor.onObj F x) ; onArrow = λ f → Functor.onArrow G (Functor.onArrow F f) ; mapId = λ {T} → mapIdHelp G F T ; mapCompose = λ r s → mapComposeHelp G F r s }
  where
    mapIdHelp : {a b c d e f : _} {B : Category {a} {b}} {C : Category {c} {d}} {D : Category {e} {f}} → (G : Functor C D) → (F : Functor B C) → (T : Category.objects B) → Functor.onArrow G (Functor.onArrow F (Category.id B T)) ≡ Category.id D (Functor.onObj G (Functor.onObj F T))
    mapIdHelp {B = B} {C} {D} record { onObj = onObjG ; onArrow = onArrowG ; mapId = mapIdG ; mapCompose = mapComposeG } record { onObj = onObj ; onArrow = onArrow ; mapId = mapId ; mapCompose = mapCompose } T rewrite mapId {T} = mapIdG {onObj T}
    mapComposeHelp : {a b c d e f : _} {B : Category {a} {b}} {C : Category {c} {d}} {D : Category {e} {f}} → (G : Functor C D) → (F : Functor B C) → {S T U : Category.objects B} → (r : Category.arrows B S T) → (s : Category.arrows B T U) → (Functor.onArrow G (Functor.onArrow F (Category._∘_ B s r))) ≡ (Category._∘_ D (Functor.onArrow G (Functor.onArrow F s)) (Functor.onArrow G (Functor.onArrow F r)))
    mapComposeHelp {B = record { objects = objectsB ; arrows = arrowsB ; id = idB ; _∘_ = _∘B_ ; rightId = rightIdB ; leftId = leftIdB ; compositionAssociative = associativeB }} {record { objects = objectsC ; arrows = arrowsC ; id = idC ; _∘_ = _∘C_ ; rightId = rightIdC ; leftId = leftIdC ; compositionAssociative = associativeC }} {record { objects = objectsD ; arrows = arrowsD ; id = idD ; _∘_ = _∘D_ ; rightId = rightIdD ; leftId = leftIdD ; compositionAssociative = associativeD }} record { onObj = onObjG ; onArrow = onArrowG ; mapId = mapIdG ; mapCompose = mapComposeG } record { onObj = onObjF ; onArrow = onArrowF ; mapId = mapIdF ; mapCompose = mapComposeF } {S} {T} {U} r s rewrite mapComposeF r s | mapComposeG (onArrowF r) (onArrowF s) = refl

idFunctor : {a b : _} (C : Category {a} {b}) → Functor C C
Functor.onObj (idFunctor C) = λ x → x
Functor.onArrow (idFunctor C) = λ f → f
Functor.mapId (idFunctor C) = refl
Functor.mapCompose (idFunctor C) = λ f g → refl


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

module Pi0Examples where

open import PiU using (U; ZERO; ONE; PLUS; TIMES)
open import PiLevel0
  using (_⟷_;
         unite₊l; uniti₊l; unite₊r; uniti₊r; swap₊; assocl₊; assocr₊;
         unite⋆l; uniti⋆l; unite⋆r; uniti⋆r; swap⋆; assocl⋆; assocr⋆;
         absorbr; absorbl; factorzr; factorzl;
         dist; factor; distl; factorl;
         id⟷; _◎_; _⊕_; _⊗_)

------------------------------------------------------------------------------
-- Example circuits on booleans

BOOL : U
BOOL  = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

-- Nicer syntax that shows intermediate values instead of the above
-- point-free notation of permutations

infixr 2  _⟷⟨_⟩_
infix  3  _□

_⟷⟨_⟩_ : (t₁ : U) {t₂ : U} {t₃ : U} →
          (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
_ ⟷⟨ α ⟩ β = α ◎ β

_□ : (t : U) → {t : U} → (t ⟷ t)
_□ t = id⟷

foldBool unfoldBool : BOOL ⟷ BOOL
foldBool = id⟷
unfoldBool = id⟷

------------------------------------------------------------------------------
-- Many ways of negating a BOOL.

NOT : BOOL ⟷ BOOL
NOT = unfoldBool ◎ swap₊ ◎ foldBool
-- spec: (false , true) ∷ (true , false) ∷ []

NEG1 NEG2 NEG3 NEG4 NEG5 : BOOL ⟷ BOOL
NEG1 = unfoldBool ◎ swap₊ ◎ foldBool
-- spec: (false , true) ∷ (true , false) ∷ []
NEG2 = id⟷ ◎ NOT
-- spec: (false , true) ∷ (true , false) ∷ []
NEG3 = NOT ◎ NOT ◎ NOT
-- spec: (false , true) ∷ (true , false) ∷ []
NEG4 = NOT ◎ id⟷
-- spec: (false , true) ∷ (true , false) ∷ []
NEG5 = uniti⋆l ◎ swap⋆ ◎ (NOT ⊗ id⟷) ◎ swap⋆ ◎ unite⋆l
-- spec: (false , true) ∷ (true , false) ∷ []
NEG6 = uniti⋆r ◎ (NOT ⊗ id⟷) ◎ unite⋆r -- same as above, but shorter

-- CNOT

CNOT : BOOL² ⟷ BOOL²
CNOT = TIMES BOOL BOOL
         ⟷⟨ unfoldBool ⊗ id⟷ ⟩
       TIMES (PLUS x y) BOOL
         ⟷⟨ dist ⟩
       PLUS (TIMES x BOOL) (TIMES y BOOL)
         ⟷⟨ id⟷ ⊕ (id⟷ ⊗ NOT) ⟩
       PLUS (TIMES x BOOL) (TIMES y BOOL)
         ⟷⟨ factor ⟩
       TIMES (PLUS x y) BOOL
         ⟷⟨ foldBool ⊗ id⟷ ⟩
       TIMES BOOL BOOL □
  where x = ONE; y = ONE

-- spec:
-- ((false , false) , false , false) ∷
-- ((false , true)  , false , true)  ∷
-- ((true  , false) , true  , true)  ∷
-- ((true  , true)  , true  , false) ∷ []

-- TOFFOLI

TOFFOLI : TIMES BOOL BOOL² ⟷ TIMES BOOL BOOL²
TOFFOLI = TIMES BOOL BOOL²
            ⟷⟨ unfoldBool ⊗ id⟷ ⟩
          TIMES (PLUS x y) BOOL²
            ⟷⟨ dist ⟩
          PLUS (TIMES x BOOL²) (TIMES y BOOL²)
            ⟷⟨ id⟷ ⊕ (id⟷ ⊗ CNOT) ⟩
          PLUS (TIMES x BOOL²) (TIMES y BOOL²)
            ⟷⟨ factor ⟩
          TIMES (PLUS x y) BOOL²
            ⟷⟨ foldBool ⊗ id⟷ ⟩
         TIMES BOOL BOOL² □
  where x = ONE; y = ONE

-- spec:
-- ((false , false , false) , false , false , false) ∷
-- ((false , false , true)  , false , false , true)  ∷
-- ((false , true  , false) , false , true  , false) ∷
-- ((false , true  , true)  , false , true  , true)  ∷
-- ((true  , false , false) , true  , false , false) ∷
-- ((true  , false , true)  , true  , false , true)  ∷
-- ((true  , true  , false) , true  , true  , true)  ∷
-- ((true  , true  , true)  , true  , true  , false) ∷ []

-- Swaps for the type 1+(1+1)
-- We have three values in the type 1+(1+1)
-- Let's call them a, b, and c
-- There 6 permutations. Using the swaps below we can express every permutation:
-- a b c id⟷
-- a c b SWAP23
-- b a c SWAP12
-- b c a ROTL
-- c a b ROTR
-- c b a SWAP13

SWAP12 SWAP23 SWAP13 ROTL ROTR :
  PLUS ONE (PLUS ONE ONE) ⟷ PLUS ONE (PLUS ONE ONE)
SWAP12 = assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊
-- spec:
-- (inj₁ tt        , inj₂ (inj₁ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₁ tt)        ∷
-- (inj₂ (inj₂ tt) , inj₂ (inj₂ tt)) ∷ []
SWAP23 = id⟷ ⊕ swap₊
-- spec:
-- (inj₁ tt        , inj₁ tt)        ∷
-- (inj₂ (inj₁ tt) , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₂ tt) , inj₂ (inj₁ tt)) ∷ []
SWAP13 = SWAP23 ◎ SWAP12 ◎ SWAP23
-- spec:
-- (inj₁ tt        , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₂ (inj₁ tt)) ∷
-- (inj₂ (inj₂ tt) , inj₁ tt)        ∷ []
ROTR   = SWAP12 ◎ SWAP23
-- spec:
-- (inj₁ tt        , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₁ tt)        ∷
-- (inj₂ (inj₂ tt) , inj₂ (inj₁ tt)) ∷ []
ROTL   = SWAP13 ◎ SWAP23
-- spec:
-- (inj₁ tt        , inj₂ (inj₁ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₂ tt) , inj₁ tt)        ∷ []

-- The Peres gate is a universal gate: it takes three inputs a, b, and c, and
-- produces a, a xor b, (a and b) xor c

PERES : TIMES (TIMES BOOL BOOL) BOOL ⟷ TIMES (TIMES BOOL BOOL) BOOL
PERES = (id⟷ ⊗ NOT) ◎ assocr⋆ ◎ (id⟷ ⊗ swap⋆) ◎
        TOFFOLI ◎
        (id⟷ ⊗ (NOT ⊗ id⟷)) ◎
        TOFFOLI ◎
        (id⟷ ⊗ swap⋆) ◎ (id⟷ ⊗ (NOT ⊗ id⟷)) ◎
        TOFFOLI ◎
        (id⟷ ⊗ (NOT ⊗ id⟷)) ◎ assocl⋆
-- spec:
-- (((false , false) , false) , (false , false) , false) ∷
-- (((false , false) , true)  , (false , false) , true)  ∷
-- (((false , true)  , false) , (false , true)  , false) ∷
-- (((false , true)  , true)  , (false , true)  , true)  ∷
-- (((true  , false) , false) , (true  , true)  , false) ∷
-- (((true  , false) , true)  , (true  , true)  , true)  ∷
-- (((true  , true)  , false) , (true  , false) , true)  ∷
-- (((true  , true)  , true)  , (true  , false) , false) ∷ []

-- A reversible full adder: See http://arxiv.org/pdf/1008.3533.pdf
-- Input: (z, ((n1, n2), cin)))
-- Output (g1, (g2, (sum, cout)))
-- where sum = n1 xor n2 xor cin
-- and cout = ((n1 xor n2) and cin) xor (n1 and n2) xor z
FULLADDER : TIMES BOOL (TIMES (TIMES BOOL BOOL) BOOL) ⟷
            TIMES BOOL (TIMES BOOL (TIMES BOOL BOOL))
FULLADDER =
  -- (z,((n1,n2),cin))
  swap⋆ ◎
  -- (((n1,n2),cin),z)
  (swap⋆ ⊗ id⟷) ◎
  -- ((cin,(n1,n2)),z)
  assocr⋆ ◎
  -- (cin,((n1,n2),z))
  swap⋆ ◎
  -- (((n1,n2),z),cin)
  (PERES ⊗ id⟷) ◎
  -- (((n1,n1 xor n2),(n1 and n2) xor z),cin)
  assocr⋆ ◎
  -- ((n1,n1 xor n2),((n1 and n2) xor z,cin))
  (id⟷ ⊗ swap⋆) ◎
  -- ((n1,n1 xor n2),(cin,(n1 and n2) xor z))
  assocr⋆ ◎
  -- (n1,(n1 xor n2,(cin,(n1 and n2) xor z)))
  (id⟷ ⊗ assocl⋆) ◎
  -- (n1,((n1 xor n2,cin),(n1 and n2) xor z))
  (id⟷ ⊗ PERES) ◎
  -- (n1,((n1 xor n2,n1 xor n2 xor cin),
  --      ((n1 xor n2) and cin) xor (n1 and n2) xor z))
  (id⟷ ⊗ assocr⋆)
  -- (n1,(n1 xor n2,
  --      (n1 xor n2 xor cin,((n1 xor n2) and cin) xor (n1 and n2) xor z)))
-- spec:
-- ((false , (false , false) , false) , false , false , false , false) ∷
-- ((false , (false , false) , true)  , false , false , true  , false) ∷
-- ((false , (false , true)  , false) , false , true  , true  , false) ∷
-- ((false , (false , true)  , true)  , false , true  , false , true)  ∷
-- ((false , (true  , false) , false) , true  , true  , true  , false) ∷
-- ((false , (true  , false) , true)  , true  , true  , false , true)  ∷
-- ((false , (true  , true)  , false) , true  , false , false , true)  ∷
-- ((false , (true  , true)  , true)  , true  , false , true  , true)  ∷
-- ((true  , (false , false) , false) , false , false , false , true)  ∷
-- ((true  , (false , false) , true)  , false , false , true  , true)  ∷
-- ((true  , (false , true)  , false) , false , true  , true  , true)  ∷
-- ((true  , (false , true)  , true)  , false , true  , false , false) ∷
-- ((true  , (true  , false) , false) , true  , true  , true  , true)  ∷
-- ((true  , (true  , false) , true)  , true  , true  , false , false) ∷
-- ((true  , (true  , true)  , false) , true  , false , false , false) ∷
-- ((true  , (true  , true)  , true)  , true  , false , true  , false) ∷ []

------------------------------------------------------------------------------
-- Generalized CNOT and TOFFOLI

ttt : {t₁ t₂ t₃ t₄ : U} →
  (TIMES (PLUS t₁ t₂) (PLUS t₃ t₄)) ⟷
  (PLUS (PLUS (PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)) (TIMES t₁ t₄))) (TIMES t₂ t₄)
ttt {t₁} {t₂} {t₃} {t₄} =
  (distl ◎ (dist {t₁} {t₂} {t₃} ⊕ dist {t₁} {t₂} {t₄})) ◎ assocl₊

-- generalized CNOT

gcnot : {A B C : U} →
        (TIMES (PLUS A B) (PLUS C C)) ⟷ (TIMES (PLUS A B) (PLUS C C))
gcnot = dist ◎ (id⟷ ⊕ (id⟷ ⊗ swap₊)) ◎ factor

-- Generalized Toffolli gate.  See what 'arithmetic' it performs.

GToffoli : {A B C D E : U} →
           TIMES (PLUS A B) (TIMES (PLUS C D) (PLUS E E)) ⟷
           TIMES (PLUS A B) (TIMES (PLUS C D) (PLUS E E))
GToffoli = dist ◎ (id⟷ ⊕ (id⟷ ⊗ gcnot)) ◎ factor

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
import      Lvl
open import Data.Boolean
open import Type

module Data.List.Sorting.MergeSort {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

open import Data.List
open import Data.List.Functions as List
open import Data.List.Relation.Membership as Membership using (_∈_ ; use ; skip)
open import Data.List.Relation.Membership.Proofs
open import Data.List.Sorting.Functions(_≤?_)
open import Relator.Equals.Proofs
open import Structure.Relator.Ordering

module _
  (split : List(T) → List(List(T)))
  (_<_ : _)
  ⦃ well-founded : Strict.Properties.WellFounded{ℓ₂ = ℓ}(_<_) ⦄
  ⦃ shrinking-proof : ∀{l}{ll} → ⦃ _ : (ll ∈ split(l)) ⦄ → (ll < l) ⦄
  where

  import Data.List.FunctionsProven as Listₚ

  -- Definition without using well-founded recursion:
  --   merge-sort = Sorted.concat ∘ List.map merge-sort ∘ split
  -- TODO: Correctness requires proof of split(l) being a partition of l
  merge-sort : List(T) → List(T)
  merge-sort = Strict.Properties.wellfounded-recursion(_<_) f where
    f : (l : List(T)) → ((prev : List(T)) → ⦃ _ : prev < l ⦄ → List(T)) → List(T)
    f(l) rec = mergeAll(Listₚ.map (\ll p → rec ll ⦃ shrinking-proof ⦃ p ⦄ ⦄) (split l) [∈]-self)

module Proofs where
  open import Data.Boolean.Stmt
  open import Data.List.Relation.Permutation
  open import Data.List.Sorting(_≤?_)
  open import Data.List.Sorting.Proofs(_≤?_)
  open import Functional using (_∘₂_)
  open import Logic.Propositional
  open import Relator.Equals
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  module _ (asym : ∀{x y} → (x ≤? y ≡ not(y ≤? x))) where -- TODO: Use Structure.Relator.Properties.Asymmetry by the relation (IsTrue ∘₂ (_≤?_))
  -- module _ (asym : ∀{x y} → (x ≤? y ≡ not(y ≤? x))) (trans : ∀{x y z} → IsTrue(x ≤? y) → IsTrue(y ≤? z) → IsTrue(x ≤? z)) where
    {-
    merge-sort-sorted-proof : ∀{l} → Sorted(merge-sort l)
    merge-sort-sorted-proof {∅}         = Sorted.empty
    merge-sort-sorted-proof {a ⊰ ∅}     = single
    merge-sort-sorted-proof l@{_ ⊰ _ ⊰ _} with Tuple.map1 merge-sort (split2 l)
    ... | (a , b) = Sorted.merge-sorted-proof asym trans (merge-sort-sorted-proof{l = ∅}) (merge-sort-sorted-proof{l = l})
    -}

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:
{-

This file contains basic theory about subgroups.

The definition is the same as the first definition of subgroups in:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#subgroups-sip

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Subgroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

private
  variable
    ℓ : Level

-- We assume an ambient group
module _ (G' : Group ℓ) where

  open GroupStr (snd G')
  private G = ⟨ G' ⟩

  record isSubgroup (H : ℙ G) : Type ℓ where
    field
      id-closed  : (1g ∈ H)
      op-closed  : {x y : G} → x ∈ H → y ∈ H → x · y ∈ H
      inv-closed : {x : G} → x ∈ H → inv x ∈ H

  open isSubgroup

  Subgroup : Type (ℓ-suc ℓ)
  Subgroup = Σ[ H ∈ ℙ G ] isSubgroup H

  isPropIsSubgroup : (H : ℙ G) → isProp (isSubgroup H)
  id-closed (isPropIsSubgroup H h1 h2 i) =
    ∈-isProp H 1g (h1 .id-closed) (h2 .id-closed) i
  op-closed (isPropIsSubgroup H h1 h2 i) Hx Hy =
    ∈-isProp H _ (h1 .op-closed Hx Hy) (h2 .op-closed Hx Hy) i
  inv-closed (isPropIsSubgroup H h1 h2 i) Hx =
    ∈-isProp H _ (h1 .inv-closed Hx) (h2 .inv-closed Hx) i

  isSetSubgroup : isSet Subgroup
  isSetSubgroup = isSetΣ isSetℙ λ x → isProp→isSet (isPropIsSubgroup x)

  Subgroup→Group : Subgroup → Group ℓ
  Subgroup→Group (H , Hh) = makeGroup-right 1HG _·HG_ invHG isSetHG assocHG ridHG invrHG
    where
    HG = Σ[ x ∈ G ] ⟨ H x ⟩
    isSetHG = isSetΣ is-set (λ x → isProp→isSet (H x .snd))

    1HG : HG
    1HG = (1g , (id-closed Hh))

    _·HG_ : HG → HG → HG
    (x , Hx) ·HG (y , Hy) = (x · y) , (op-closed Hh Hx Hy)

    invHG : HG → HG
    invHG (x , Hx) = inv x , inv-closed Hh Hx

    assocHG : (x y z : HG) → x ·HG (y ·HG z) ≡ (x ·HG y) ·HG z
    assocHG (x , Hx) (y , Hy) (z , Hz) =
      ΣPathP (·Assoc x y z , isProp→PathP (λ i → H (·Assoc x y z i) .snd) _ _)

    ridHG : (x : HG) → x ·HG 1HG ≡ x
    ridHG (x , Hx) = ΣPathP (·IdR x , isProp→PathP (λ i → H (·IdR x i) .snd) _ _)

    invrHG : (x : HG) → x ·HG invHG x ≡ 1HG
    invrHG (x , Hx) = ΣPathP (·InvR x , isProp→PathP (λ i → H (·InvR x i) .snd) _ _)

⟪_⟫ : {G' : Group ℓ} → Subgroup G' → ℙ (G' .fst)
⟪ H , _ ⟫ = H

module _ {G' : Group ℓ} where

  open GroupStr (snd G')
  open isSubgroup
  open GroupTheory G'
  private G = ⟨ G' ⟩

  isNormal : Subgroup G' → Type ℓ
  isNormal H = (g h : G) → h ∈ ⟪ H ⟫ → g · h · inv g ∈ ⟪ H ⟫

  isPropIsNormal : (H : Subgroup G') → isProp (isNormal H)
  isPropIsNormal H = isPropΠ3 λ g h _ → ∈-isProp ⟪ H ⟫ (g · h · inv g)

  ·CommNormalSubgroup : (H : Subgroup G') (Hnormal : isNormal H) {x y : G}
                      → x · y ∈ ⟪ H ⟫ → y · x ∈ ⟪ H ⟫
  ·CommNormalSubgroup H Hnormal {x = x} {y = y} Hxy =
    subst-∈ ⟪ H ⟫ rem (Hnormal (inv x) (x · y) Hxy)
      where
      rem : inv x · (x · y) · inv (inv x) ≡ y · x
      rem = inv x · (x · y) · inv (inv x) ≡⟨ ·Assoc _ _ _ ⟩
            (inv x · x · y) · inv (inv x) ≡⟨ (λ i → ·Assoc (inv x) x y i · invInv x i) ⟩
            ((inv x · x) · y) · x         ≡⟨ cong (λ z → (z · y) · x) (·InvL x) ⟩
            (1g · y) · x                  ≡⟨ cong (_· x) (·IdL y) ⟩
            y · x                         ∎

  -- Examples of subgroups

  -- We can view all of G as a subset of itself
  groupSubset : ℙ G
  groupSubset x = (x ≡ x) , is-set x x

  isSubgroupGroup : isSubgroup G' groupSubset
  id-closed isSubgroupGroup = refl
  op-closed isSubgroupGroup _ _ = refl
  inv-closed isSubgroupGroup _ = refl

  groupSubgroup : Subgroup G'
  groupSubgroup = groupSubset , isSubgroupGroup

  -- The trivial subgroup
  trivialSubset : ℙ G
  trivialSubset x = (x ≡ 1g) , is-set x 1g

  isSubgroupTrivialGroup : isSubgroup G' trivialSubset
  id-closed isSubgroupTrivialGroup = refl
  op-closed isSubgroupTrivialGroup hx hy = cong (_· _) hx ∙∙ ·IdL _ ∙∙ hy
  inv-closed isSubgroupTrivialGroup hx = cong inv hx ∙ inv1g

  trivialSubgroup : Subgroup G'
  trivialSubgroup = trivialSubset , isSubgroupTrivialGroup

  isNormalTrivialSubgroup : isNormal trivialSubgroup
  isNormalTrivialSubgroup g h h≡1 =
    (g · h · inv g)  ≡⟨ (λ i → g · h≡1 i · inv g) ⟩
    (g · 1g · inv g) ≡⟨ ·Assoc _ _ _ ∙ cong (_· inv g) (·IdR g) ⟩
    (g · inv g)      ≡⟨ ·InvR g ⟩
    1g ∎

NormalSubgroup : (G : Group ℓ) → Type _
NormalSubgroup G = Σ[ G ∈ Subgroup G ] isNormal G

-- Can one get this to work with different universes for G and H?
module _ {G H : Group ℓ} (ϕ : GroupHom G H) where

  open isSubgroup
  open GroupTheory

  private
    module G = GroupStr (snd G)
    module H = GroupStr (snd H)
    f = ϕ .fst
    module ϕ = IsGroupHom (ϕ .snd)

  imSubset : ℙ ⟨ H ⟩
  imSubset x = isInIm ϕ x , isPropIsInIm ϕ x

  isSubgroupIm : isSubgroup H imSubset
  id-closed isSubgroupIm = ∣ G.1g , ϕ.pres1 ∣₁
  op-closed isSubgroupIm =
    map2 λ { (x , hx) (y , hy) → x G.· y , ϕ.pres· x y ∙ λ i → hx i H.· hy i }
  inv-closed isSubgroupIm = map λ { (x , hx) → G.inv x , ϕ.presinv x ∙ cong H.inv hx }

  imSubgroup : Subgroup H
  imSubgroup = imSubset , isSubgroupIm

  imGroup : Group ℓ
  imGroup = Subgroup→Group _ imSubgroup

  isNormalIm : ((x y : ⟨ H ⟩) → x H.· y ≡ y H.· x)
            → isNormal imSubgroup
  isNormalIm comm x y =
    map λ {(g , p)
      → g ,
      (ϕ .fst g                  ≡⟨ p ⟩
      y                          ≡⟨ sym (H.·IdR y) ⟩
      (y H.· H.1g)               ≡⟨ cong (y H.·_) (sym (H.·InvR x)) ⟩
      (y H.· (x H.· H.inv x))    ≡⟨ H.·Assoc y x (H.inv x) ⟩
      ((y H.· x) H.· H.inv x)    ≡⟨ cong (H._· H.inv x) (comm y x) ⟩
      ((x H.· y) H.· H.inv x)    ≡⟨ sym (H.·Assoc x y (H.inv x)) ⟩
      x H.· y H.· H.inv x        ∎ )}

  kerSubset : ℙ ⟨ G ⟩
  kerSubset x = isInKer ϕ x , isPropIsInKer ϕ x

  isSubgroupKer : isSubgroup G kerSubset
  id-closed isSubgroupKer = ϕ.pres1
  op-closed isSubgroupKer {x} {y} hx hy =
    ϕ.pres· x y ∙∙ (λ i → hx i H.· hy i) ∙∙ H.·IdR _
  inv-closed isSubgroupKer hx = ϕ.presinv _ ∙∙ cong H.inv hx ∙∙ inv1g H

  kerSubgroup : Subgroup G
  kerSubgroup = kerSubset , isSubgroupKer

  isNormalKer : isNormal kerSubgroup
  isNormalKer x y hy =
    f (x G.· y G.· G.inv x)         ≡⟨ ϕ.pres· _ _ ⟩
    f x H.· f (y G.· G.inv x)       ≡⟨ cong (f x H.·_) (ϕ.pres· _ _) ⟩
    f x H.· f y H.· f (G.inv x)     ≡⟨ (λ i → f x H.· hy i H.· f (G.inv x)) ⟩
    f x H.· (H.1g H.· f (G.inv x))  ≡⟨ cong (f x H.·_) (H.·IdL _) ⟩
    f x H.· f (G.inv x)             ≡⟨ cong (f x H.·_) (ϕ.presinv x) ⟩
    f x H.· H.inv (f x)             ≡⟨ H.·InvR _ ⟩
    H.1g                            ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical