text:
module Data.Bindings.Everything where

import Data.ByteString
import Data.ByteString.Primitive
import Data.ByteString.UTF8
import Data.ByteString.UTF8.Primitive
import Data.Char.Classifier
import Data.Char.Classifier.Primitive
import Data.List.Primitive
import Data.Maybe.Primitive
import Data.Natural
import Data.Natural.Primitive
import Data.Strict
import Data.Strict.Primitive
import Data.Word
import Data.Word.Primitive

max_stars_repo_name: agda/agda-data-bindings

max_issues_repo_name: agda/agda-data-bindings

max_forks_repo_name: agda/agda-data-bindings


text:
------------------------------------------------------------------------
-- Suspensions
------------------------------------------------------------------------

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

-- The beginning of this module follows the HoTT book rather closely.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining suspensions uses path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq hiding (elim)

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

open import Bijection equality-with-J as Bijection using (_↔_)
open import Embedding equality-with-J as Embedding using (Embedding)
open import Equality.Decision-procedures equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Injection equality-with-J using (_↣_)
open import Interval eq as Interval using (Interval; [0]; [1]; 0≡1)
import Nat equality-with-J as Nat
open import Pointed-type equality-with-J
  using (Pointed-type; _→ᴮ_; Ω)
open import Surjection equality-with-J using (_↠_)

private
  variable
    a b ℓ ℓ₁ ℓ₂ p : Level
    A B           : Type a
    C             : Pointed-type a
    x y           : A
    f g           : A → B
    n             : ℕ

-- Suspensions.

data Susp (A : Type a) : Type a where
  north south : Susp A
  meridianᴾ   : A → north P.≡ south

-- Meridians.

meridian : A → _≡_ {A = Susp A} north south
meridian = _↔_.from ≡↔≡ ∘ meridianᴾ

-- A dependent eliminator, expressed using paths.

elimᴾ :
  (P : Susp A → Type p)
  (n : P north)
  (s : P south) →
  (∀ x → P.[ (λ i → P (meridianᴾ x i)) ] n ≡ s) →
  (x : Susp A) → P x
elimᴾ _ n s n≡s = λ where
  north           → n
  south           → s
  (meridianᴾ x i) → n≡s x i

-- A non-dependent eliminator, expressed using paths.

recᴾ : (n s : B) → (A → n P.≡ s) → Susp A → B
recᴾ = elimᴾ _

-- A dependent eliminator.

module Elim
  (P   : Susp A → Type p)
  (n   : P north)
  (s   : P south)
  (n≡s : ∀ x → subst P (meridian x) n ≡ s)
  where

  elim : ∀ x → P x
  elim = elimᴾ P n s (subst≡→[]≡ ∘ n≡s)

  -- "Computation" rule for meridians.

  elim-meridian : dcong elim (meridian x) ≡ n≡s x
  elim-meridian = dcong-subst≡→[]≡ (refl _)

open Elim public

-- A non-dependent eliminator.

module Rec
  {B : Type b}
  (n s : B)
  (n≡s : A → n ≡ s)
  where

  rec : Susp A → B
  rec = recᴾ n s (_↔_.to ≡↔≡ ∘ n≡s)

  rec-meridian : cong rec (meridian x) ≡ n≡s x
  rec-meridian = cong-≡↔≡ (refl _)

open Rec public

-- The universal property of suspensions.

universal-property :
  (Susp A → B) ↔ (∃ λ (n : B) → ∃ λ (s : B) → A → n ≡ s)
universal-property = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → f north , f south , cong f ∘ meridian
      ; from = λ { (n , s , f) → rec n s f }
      }
    ; right-inverse-of = λ { (n , s , f) →
        n , s , cong (rec n s f) ∘ meridian  ≡⟨ cong (λ f → n , s , f) $ ⟨ext⟩ (λ _ → rec-meridian n s f) ⟩∎
        n , s , f                            ∎ }
    }
  ; left-inverse-of = λ f →
      let module R = Rec (f north) (f south) (cong f ∘ meridian) in

      R.rec                                                        ≡⟨ ⟨ext⟩ $ elim _ (refl _) (refl _) (λ x →

          subst (λ x → R.rec x ≡ f x) (meridian x) (refl _)             ≡⟨ subst-in-terms-of-trans-and-cong ⟩

          trans (sym $ cong R.rec (meridian x))
                (trans (refl _) (cong f (meridian x)))                  ≡⟨ cong₂ (λ p q → trans (sym p) q) R.rec-meridian (trans-reflˡ _) ⟩

          trans (sym $ cong f (meridian x)) (cong f (meridian x))       ≡⟨ trans-symˡ _ ⟩∎

          refl _                                                        ∎) ⟩∎

      f                                                            ∎
  }

-- Based maps from suspensions of pointed types (using north as the
-- point) are isomorphic to based maps to loop spaces.

Susp→ᴮ↔ : (Susp A , north) →ᴮ C ↔ (A , x) →ᴮ Ω C
Susp→ᴮ↔ {A = A} {C = B , y} {x = x} =
  (Susp A , north) →ᴮ (B , y)                                            ↔⟨⟩
  (∃ λ (f : Susp A → B) → f north ≡ y)                                   ↝⟨ Σ-cong universal-property (λ _ → F.id) ⟩
  (∃ λ (f : ∃ λ n → ∃ λ s → A → n ≡ s) → proj₁ f ≡ y)                    ↝⟨ inverse Σ-assoc ⟩
  (∃ λ n → (∃ λ s → A → n ≡ s) × n ≡ y)                                  ↝⟨ (∃-cong λ _ → inverse Σ-assoc) ⟩
  (∃ λ n → ∃ λ s → (A → n ≡ s) × n ≡ y)                                  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩
  (∃ λ n → ∃ λ s → n ≡ y × (A → n ≡ s))                                  ↝⟨ (∃-cong λ _ → ∃-comm) ⟩
  (∃ λ n → n ≡ y × ∃ λ s → A → n ≡ s)                                    ↝⟨ Σ-assoc ⟩
  (∃ λ (p : ∃ λ n → n ≡ y) → ∃ λ s → A → proj₁ p ≡ s)                    ↝⟨ drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $ singleton-contractible _ ⟩
  (∃ λ s → A → y ≡ s)                                                    ↝⟨ (∃-cong λ _ → inverse $ drop-⊤-right λ _ → _⇔_.to contractible⇔↔⊤ $
                                                                             other-singleton-contractible _) ⟩
  (∃ λ s → ∃ λ (f : A → y ≡ s) → ∃ λ (eq : y ≡ s) → f x ≡ eq)            ↝⟨ (∃-cong λ _ → ∃-comm) ⟩
  (∃ λ s → ∃ λ (eq : y ≡ s) → ∃ λ (f : A → y ≡ s) → f x ≡ eq)            ↝⟨ Σ-assoc ⟩
  (∃ λ (p : ∃ λ s → y ≡ s) → ∃ λ (f : A → y ≡ proj₁ p) → f x ≡ proj₂ p)  ↝⟨ drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                                                                            other-singleton-contractible _ ⟩
  (∃ λ (f : A → y ≡ y) → f x ≡ refl y)                                   ↔⟨⟩
  (A , x) →ᴮ (Ω (B , y))                                                 □

-- The type of booleans can be expressed as a suspension.

Bool↔Susp-⊥ : Bool ↔ Susp (⊥ {ℓ = ℓ})
Bool↔Susp-⊥ = record
  { surjection = record
    { logical-equivalence = record
      { to   = if_then north else south
      ; from = rec true false (λ ())
      }
    ; right-inverse-of = elim _ (refl _) (refl _) (λ ())
    }
  ; left-inverse-of = λ where
      true  → refl _
      false → refl _
  }

private

  -- A lemma used in some proofs below.

  subst-in-terms-of-trans-and-cong′ :
    {x≡y : x ≡ y} {fgx≡x : f (g x) ≡ x} →
    subst (λ z → f (g z) ≡ z) x≡y fgx≡x ≡
    trans (sym (cong f (cong g x≡y))) (trans fgx≡x x≡y)
  subst-in-terms-of-trans-and-cong′
    {f = f} {g = g} {x≡y = x≡y} {fgx≡x = fgx≡x} =

    subst (λ z → f (g z) ≡ z) x≡y fgx≡x                         ≡⟨ subst-in-terms-of-trans-and-cong ⟩
    trans (sym (cong (f ∘ g) x≡y)) (trans fgx≡x (cong id x≡y))  ≡⟨ sym $ cong₂ (λ p q → trans (sym p) (trans fgx≡x q)) (cong-∘ _ _ _) (cong-id _) ⟩∎
    trans (sym (cong f (cong g x≡y))) (trans fgx≡x x≡y)         ∎

-- The remainder of this module is not based on the HoTT book.

-- The interval can be expressed as a suspension.

Interval↔Susp-⊤ : Interval ↔ Susp ⊤
Interval↔Susp-⊤ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = elim
        _
        (refl _)
        (refl _)
        (λ _ →
           subst (λ x → to (from x) ≡ x) (meridian tt) (refl _)           ≡⟨ subst-in-terms-of-trans-and-cong′ ⟩

           trans (sym (cong to (cong from (meridian tt))))
                 (trans (refl _) (meridian tt))                           ≡⟨ cong₂ (λ p q → trans (sym (cong to p)) q)
                                                                               (rec-meridian _ _ _)
                                                                               (trans-reflˡ _) ⟩
           trans (sym (cong to 0≡1)) (meridian tt)                        ≡⟨ cong (λ p → trans (sym p) (meridian tt)) $ Interval.rec-0≡1 _ _ _ ⟩

           trans (sym (meridian tt)) (meridian tt)                        ≡⟨ trans-symˡ _ ⟩∎

           refl _                                                         ∎)
    }
  ; left-inverse-of = Interval.elim
      _
      (refl _)
      (refl _)
      (subst (λ x → from (to x) ≡ x) 0≡1 (refl _)                  ≡⟨ subst-in-terms-of-trans-and-cong′ ⟩
       trans (sym (cong from (cong to 0≡1))) (trans (refl _) 0≡1)  ≡⟨ cong₂ (λ p q → trans (sym (cong from p)) q)
                                                                        (Interval.rec-0≡1 _ _ _)
                                                                        (trans-reflˡ _) ⟩
       trans (sym (cong from (meridian tt))) 0≡1                   ≡⟨ cong (λ p → trans (sym p) 0≡1) $ rec-meridian _ _ _ ⟩
       trans (sym 0≡1) 0≡1                                         ≡⟨ trans-symˡ _ ⟩∎
       refl _                                                      ∎)
  }
  where
  to   = Interval.rec north south (meridian tt)
  from = rec [0] [1] λ _ → 0≡1

-- A map function.

map : (A → B) → Susp A → Susp B
map A→B = rec north south (meridian ∘ A→B)

private

  -- A helper function used to implement cong-↠ and cong-↔.

  map∘map :
    (∀ x → f (g x) ≡ x) →
    ∀ x → map f (map g x) ≡ x
  map∘map {f = f} {g = g} hyp = elim
    _
    (refl _)
    (refl _)
    (λ x →
       subst (λ x → map f (map g x) ≡ x) (meridian x) (refl _)   ≡⟨ subst-in-terms-of-trans-and-cong′ ⟩

       trans (sym $ cong (map f) $ cong (map g) (meridian x))
             (trans (refl _) (meridian x))                       ≡⟨ cong₂ (λ p q → trans (sym $ cong (map f) p) q)
                                                                      (rec-meridian _ _ _)
                                                                      (trans-reflˡ _) ⟩

       trans (sym $ cong (map f) $ meridian (g x)) (meridian x)  ≡⟨ cong (λ p → trans (sym p) (meridian x)) $ rec-meridian _ _ _ ⟩

       trans (sym $ meridian (f (g x))) (meridian x)             ≡⟨ cong (λ y → trans (sym $ meridian y) (meridian x)) $ hyp x ⟩

       trans (sym $ meridian x) (meridian x)                     ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                    ∎)

-- Some preservation lemmas.

cong-⇔ : A ⇔ B → Susp A ⇔ Susp B
cong-⇔ A⇔B = record
  { to   = map (_⇔_.to   A⇔B)
  ; from = map (_⇔_.from A⇔B)
  }

cong-↠ : A ↠ B → Susp A ↠ Susp B
cong-↠ A↠B = record
  { logical-equivalence = cong-⇔ (_↠_.logical-equivalence A↠B)
  ; right-inverse-of    = map∘map (_↠_.right-inverse-of A↠B)
  }

cong-↔ : A ↔ B → Susp A ↔ Susp B
cong-↔ A↔B = record
  { surjection      = cong-↠ (_↔_.surjection A↔B)
  ; left-inverse-of = map∘map (_↔_.left-inverse-of A↔B)
  }

cong-≃ : A ≃ B → Susp A ≃ Susp B
cong-≃ = from-isomorphism ∘ cong-↔ ∘ from-isomorphism

private

  -- Lemmas used to implement ¬-cong-↣ and ¬-cong-Embedding.

  ⊥↣⊤ : ⊥ {ℓ = ℓ₁} ↣ ↑ ℓ₂ ⊤
  ⊥↣⊤ = record
    { to        = λ ()
    ; injective = λ {}
    }

  ¬Susp⊥↣Susp⊤ : ¬ (Susp (⊥ {ℓ = ℓ₁}) ↣ Susp (↑ ℓ₂ ⊤))
  ¬Susp⊥↣Susp⊤ =
    Susp ⊥ ↣ Susp (↑ _ ⊤)                                          ↝⟨ (λ f → from-isomorphism (cong-↔ Bijection.↑↔) F.∘ f F.∘
                                                                             from-isomorphism (cong-↔ ⊥↔⊥)) ⟩
    Susp ⊥₀ ↣ Susp ⊤                                               ↝⟨ (λ f → from-isomorphism (inverse Interval↔Susp-⊤) F.∘ f F.∘
                                                                             from-isomorphism Bool↔Susp-⊥) ⟩
    Bool ↣ Interval                                                ↝⟨ (λ inj → _↣_.to inj , _↣_.injective inj) ⟩
    (∃ λ (f : Bool → Interval) → f true ≡ f false → true ≡ false)  ↝⟨ Σ-map id (λ f → f (mono₁ 0 Interval.interval-contractible _ _)) ⟩
    (Bool → Interval) × true ≡ false                               ↝⟨ proj₂ ⟩
    true ≡ false                                                   ↝⟨ Bool.true≢false ⟩□
    ⊥                                                              □

-- Some negative preservation results.

¬-cong-↣ :
  ¬ (∀ {A : Type a} {B : Type b} → A ↣ B → Susp A ↣ Susp B)
¬-cong-↣ {a = a} {b = b} =
  (∀ {A B} → A ↣ B → Susp A ↣ Susp B)  ↝⟨ (λ hyp → hyp) ⟩
  (⊥ ↣ ↑ _ ⊤ → Susp ⊥ ↣ Susp (↑ _ ⊤))  ↝⟨ _$ ⊥↣⊤ ⟩
  Susp ⊥ ↣ Susp (↑ _ ⊤)                ↝⟨ ¬Susp⊥↣Susp⊤ ⟩□
  ⊥                                    □

¬-cong-Embedding :
  ¬ (∀ {A : Type a} {B : Type b} →
     Embedding A B → Embedding (Susp A) (Susp B))
¬-cong-Embedding =
  (∀ {A B} → Embedding A B → Embedding (Susp A) (Susp B))    ↝⟨ (λ hyp → hyp) ⟩
  (Embedding ⊥ (↑ _ ⊤) → Embedding (Susp ⊥) (Susp (↑ _ ⊤)))  ↝⟨ _$ Emb-⊥-⊤ ⟩
  Embedding (Susp ⊥) (Susp (↑ _ ⊤))                          ↝⟨ Embedding.injection ⟩
  Susp ⊥ ↣ Susp (↑ _ ⊤)                                      ↝⟨ ¬Susp⊥↣Susp⊤ ⟩□
  ⊥                                                          □
  where
  Emb-⊥-⊤ : Embedding ⊥ (↑ _ ⊤)
  Emb-⊥-⊤ =
    _↔_.to (Embedding.↣↔Embedding
              ext
              (mono₁ 1 ⊥-propositional)
              (mono (Nat.zero≤ 2) (↑-closure 0 ⊤-contractible)))
           ⊥↣⊤

ext: agda

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

import SecondOrder.Arity
import SecondOrder.MContext
import SecondOrder.Signature

module SecondOrder.Metavariable
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ

  open SecondOrder.MContext VContext sort public

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module BTree.Equality {A : Set} where

open import BTree {A}

data _≃_ : BTree → BTree → Set where
  ≃lf : leaf ≃ leaf
  ≃nd : {l r l' r' : BTree}
                    (x x' : A)
                   → l ≃ r
                   → l ≃ l'
                   → l' ≃ r'
                   → node x l r ≃ node x' l' r'

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

-- This module contains definitions of properties of only the behavior of the
-- handlers, nothing concerning the system state.

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Concrete.Records
open import LibraBFT.Impl.Consensus.ConsensusTypes.Block as Block
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Handle as Handle
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.KVMap                                   as Map
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open import LibraBFT.ImplShared.Util.HashCollisions Handle.InitHandler.initAndHandlers
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open        ParamsWithInitAndHandlers Handle.InitHandler.initAndHandlers
open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms
                      Handle.InitHandler.initAndHandlers
                      PeerCanSignForPK PeerCanSignForPK-stable

module LibraBFT.Impl.Properties.Util where

module Meta where
  getLastVoteEpoch : SafetyData → Epoch
  getLastVoteEpoch sd = (Maybe-maybe{B = const Epoch} (_^∙ vEpoch) (sd ^∙ sdEpoch)) ∘ (_^∙ sdLastVote) $ sd
  -- getLastVoteEpoch rm = (maybe{B = const Epoch} (_^∙ vEpoch) (rm ^∙ pssSafetyData-rm ∙ sdEpoch)) ∘ (_^∙ pssSafetyData-rm ∙ sdLastVote) $ rm

  getLastVoteRound : SafetyData → Round
  getLastVoteRound = (Maybe-maybe{B = const Round} (_^∙ vRound) 0) ∘ (_^∙ sdLastVote)
  -- getLastVoteRound = maybe{B = const Round} (_^∙ vRound) 0 ∘ (_^∙ pssSafetyData-rm ∙ sdLastVote)

  subst-getLastVoteRound : ∀ {sd1 sd2} → sd1 ≡ sd2 → getLastVoteRound sd1 ≡ getLastVoteRound sd2
  subst-getLastVoteRound refl = refl

module OutputProps where
  module _ (outs : List Output) where
    None : Set
    None = outs ≡ []

    NoVotes     = NoneOfKind outs isSendVote?
    NoProposals = NoneOfKind outs isBroadcastProposal?
    NoSyncInfos = NoneOfKind outs isBroadcastSyncInfo?
    NoMsgs      = NoneOfKind outs isOutputMsg?
    NoErrors    = NoneOfKind outs isLogErr?

    NoMsgs⇒× : NoMsgs → NoProposals × NoVotes × NoSyncInfos
    proj₁ (NoMsgs⇒× noMsgs) =
      filter-∪?-[]₁ outs isBroadcastProposal? _ noMsgs
    proj₁ (proj₂ (NoMsgs⇒× noMsgs)) =
      filter-∪?-[]₂ outs _ isSendVote?
        (filter-∪?-[]₂ outs _ _ noMsgs)
    proj₂ (proj₂ (NoMsgs⇒× noMsgs)) =
      filter-∪?-[]₁ outs isBroadcastSyncInfo? _
        (filter-∪?-[]₂ outs _ _ noMsgs)

    NoMsgs⇒NoProposals : NoMsgs → NoProposals
    NoMsgs⇒NoProposals = proj₁ ∘ NoMsgs⇒×

    NoMsgs⇒NoVotes : NoMsgs → NoVotes
    NoMsgs⇒NoVotes = proj₁ ∘ proj₂ ∘ NoMsgs⇒×

    OneVote : VoteMsg → List Author → Set
    OneVote vm pids = List-filter isSendVote? outs ≡ (SendVote vm pids ∷ [])

  ++-NoMsgs      = λ xs ys → ++-NoneOfKind xs ys isOutputMsg?
  ++-NoVotes     = λ xs ys → ++-NoneOfKind xs ys isSendVote?
  ++-NoProposals = λ xs ys → ++-NoneOfKind xs ys isBroadcastProposal?

  ++-NoVotes-OneVote : ∀ xs ys {vm} {pids} → NoVotes xs → OneVote ys vm pids
                       → OneVote (xs ++ ys) vm pids
  ++-NoVotes-OneVote xs ys nv ov
    rewrite List-filter-++ isSendVote? xs ys
    |       nv = ov

  ++-OneVote-NoVotes : ∀ xs {vm pids} ys → OneVote xs vm pids → NoVotes ys
                       → OneVote (xs ++ ys) vm pids
  ++-OneVote-NoVotes xs ys ov nv
    rewrite List-filter-++ isSendVote? xs ys
    |       nv
    |       ov = refl

module BlockProps (b : Block) where
  ∈BlockTree_      : BlockTree → Set
  ∈BlockTree bt    = ∃[ eb ] (btGetBlock (b ^∙ bId) bt ≡ just eb)

  ∈BlockStore_     : BlockStore → Set
  ∈BlockStore bs   = ∈BlockTree (bs ^∙ bsInner)

  ∈RoundManager_   : RoundManager → Set
  ∈RoundManager rm = ∈BlockStore (rm ^∙ lBlockStore)

module QCProps where

  data _∈BlockTree_ (qc : QuorumCert) (bt : BlockTree) : Set where
    inHQC : qc ≡ bt ^∙ btHighestQuorumCert → qc ∈BlockTree bt
    inHCC : qc ≡ bt ^∙ btHighestCommitCert → qc ∈BlockTree bt

  _∈RoundManager_ : (qc : QuorumCert) (rm : RoundManager) → Set
  qc ∈RoundManager rm =  qc ∈BlockTree (rm ^∙ lBlockStore ∙ bsInner)

  ∈Post⇒∈PreOr' : ∀ {A : Set} (_QC∈_ : QuorumCert → A → Set) (Q : QuorumCert → Set) (pre post : A) → Set
  ∈Post⇒∈PreOr' _QC∈_ Q pre post = ∀ qc → qc QC∈ post → qc QC∈ pre ⊎ Q qc

  ∈Post⇒∈PreOr'-∙ : ∀ {A B : Set}
                    → (l : Lens A B)
                    → (_QC∈B_ : QuorumCert → B → Set)
                    → (_QC∈A_ : QuorumCert → A → Set)
                    → (∀ {q st} → q QC∈B (st ^∙ l) → q QC∈A st)
                    → (∀ {q st} → q QC∈A st → q QC∈B (st ^∙ l))
                    → (Q : QuorumCert → Set)
                    → (pre post : A)
                    → ∈Post⇒∈PreOr' _QC∈B_ Q (pre ^∙ l) (post ^∙ l)
                    → ∈Post⇒∈PreOr' _QC∈A_ Q pre post
  ∈Post⇒∈PreOr'-∙ l _QC∈B_ _QC∈A_ prfBA prfAB Q pre post QCB qc qc∈Apost =
    ⊎-map₁ prfBA (QCB qc (prfAB qc∈Apost))

  ∈Post⇒∈PreOr-∙-BT-RM : _
  ∈Post⇒∈PreOr-∙-BT-RM = ∈Post⇒∈PreOr'-∙ lBlockTree _∈BlockTree_ _∈RoundManager_ id id

  ∈Post⇒∈PreOrBT : (Q : QuorumCert → Set) (pre post : BlockTree) → Set
  ∈Post⇒∈PreOrBT = ∈Post⇒∈PreOr' _∈BlockTree_

  ∈BlockTree-upd-hqc : ∀ {bt1 bt2}
                       → {Q : QuorumCert → Set}
                       → bt1 ≡L bt2 at btHighestCommitCert
                       → Q (bt2 ^∙ btHighestQuorumCert)
                       → ∈Post⇒∈PreOrBT Q bt1 bt2
  ∈BlockTree-upd-hqc refl Q _ (inHQC refl) = inj₂ Q
  ∈BlockTree-upd-hqc refl _ _ (inHCC refl) = inj₁ (inHCC refl)

  ∈BlockTree-upd-hcc : ∀ {bt1 bt2}
                       → {Q : QuorumCert → Set}
                       → bt1 ≡L bt2 at btHighestQuorumCert
                       → Q (bt2 ^∙ btHighestCommitCert)
                       → ∈Post⇒∈PreOrBT Q bt1 bt2
  ∈BlockTree-upd-hcc refl _ _ (inHQC refl) = inj₁ (inHQC refl)
  ∈BlockTree-upd-hcc refl Q _ (inHCC refl) = inj₂ Q

  ∈Post⇒∈PreOr : (Q : QuorumCert → Set) (pre post : RoundManager) → Set
  ∈Post⇒∈PreOr = ∈Post⇒∈PreOr' _∈RoundManager_

  ∈Post⇒∈PreOr'-refl : ∀ {A : Set}
                      → (_QC∈_ : QuorumCert → A → Set) (Q : QuorumCert → Set)
                      → ∀ {pre : A}
                      → ∈Post⇒∈PreOr' _QC∈_ Q pre pre
  ∈Post⇒∈PreOr'-refl _ _ _ = inj₁

  ∈Post⇒∈PreOrBT-QCs≡ : ∀ {bt1 bt2}
                        → (Q : QuorumCert → Set)
                        → bt1 ≡L bt2 at btHighestCommitCert
                        → bt1 ≡L bt2 at btHighestQuorumCert
                        → ∈Post⇒∈PreOrBT Q bt1 bt2
  ∈Post⇒∈PreOrBT-QCs≡ Q refl refl _ (inHQC refl) = inj₁ (inHQC refl)
  ∈Post⇒∈PreOrBT-QCs≡ Q refl refl _ (inHCC refl) = inj₁ (inHCC refl)

  ∈Post⇒∈PreOr'-trans : ∀ {A : Set}
                      → (_QC∈_ : QuorumCert → A → Set) (Q : QuorumCert → Set)
                      → ∀ {pre int post : A}
                      → ∈Post⇒∈PreOr' _QC∈_ Q pre int
                      → ∈Post⇒∈PreOr' _QC∈_ Q int post
                      → ∈Post⇒∈PreOr' _QC∈_ Q pre post
  ∈Post⇒∈PreOr'-trans _QC∈_ Q pre→int int→post qc qc∈post
     with int→post qc qc∈post
  ... | Right y = Right y
  ... | Left  x
     with pre→int qc x
  ... | Right y = Right y
  ... | Left x₁ = Left x₁

  ∈Post⇒∈PreOrBT-trans : ∀ (Q : QuorumCert → Set) {pre int post}
                       → ∈Post⇒∈PreOrBT Q pre int
                       → ∈Post⇒∈PreOrBT Q int post
                       → ∈Post⇒∈PreOrBT Q pre post
  ∈Post⇒∈PreOrBT-trans = ∈Post⇒∈PreOr'-trans _∈BlockTree_

  -- TODO-1: Factor out a property about a single output:
  -- λ out → ∃₂ λ qc nm → qc QC∈NM nm × nm Msg∈Out out
  OutputQc∈RoundManager : List Output → RoundManager → Set
  OutputQc∈RoundManager outs rm =
    All (λ out → ∀ qc nm → qc QC∈NM nm → nm Msg∈Out out → qc ∈RoundManager rm) outs

  ¬OutputQc : List Output → Set
  ¬OutputQc outs = All (λ out → ∀ qc nm → qc QC∈NM nm → nm Msg∈Out out → ⊥) outs

  ++-OutputQc∈RoundManager
    : ∀ {rm outs₁ outs₂}
      → OutputQc∈RoundManager outs₁ rm → OutputQc∈RoundManager outs₂ rm
      → OutputQc∈RoundManager (outs₁ ++ outs₂) rm
  ++-OutputQc∈RoundManager = All-++

  ++-¬OutputQc : ∀ {outs₁ outs₂} → ¬OutputQc outs₁ → ¬OutputQc outs₂
                 → ¬OutputQc (outs₁ ++ outs₂)
  ++-¬OutputQc = All-++

  NoMsgs⇒¬OutputQc : ∀ outs → OutputProps.NoMsgs outs → ¬OutputQc outs
  NoMsgs⇒¬OutputQc outs noMsgs =
    All-map help (noneOfKind⇒All¬ outs _ noMsgs)
    where
    help : ∀ {out : Output} → ¬ IsOutputMsg out → ∀ qc nm → qc QC∈NM nm → nm Msg∈Out out → ⊥
    help ¬msg qc .(P _) qc∈m inBP = ¬msg (Left tt)
    help ¬msg qc .(V _) qc∈m inSV = ¬msg (Right (Right tt))

  ¬OutputQc⇒OutputQc∈RoundManager : ∀ outs rm → ¬OutputQc outs → OutputQc∈RoundManager outs rm
  ¬OutputQc⇒OutputQc∈RoundManager outs rm noOutQcs =
    All-map (λ ¬outqc qc nm qc∈nm nm∈out → ⊥-elim (¬outqc qc nm qc∈nm nm∈out))
      noOutQcs

  NoMsgs⇒OutputQc∈RoundManager : ∀ outs rm → OutputProps.NoMsgs outs → OutputQc∈RoundManager outs rm
  NoMsgs⇒OutputQc∈RoundManager outs rm noMsgs =
    ¬OutputQc⇒OutputQc∈RoundManager outs rm (NoMsgs⇒¬OutputQc outs noMsgs)

  SigForVote∈Rm-SentB4 : Vote → PK → QuorumCert → RoundManager → SentMessages → Set
  SigForVote∈Rm-SentB4 v pk qc rm pool =
    qc ∈RoundManager rm
    → WithVerSig pk v →
    ∀ {vs : Author × Signature} → let (pid , sig) = vs in
      vs ∈ qcVotes qc → rebuildVote qc vs ≈Vote v
    → ¬(∈BootstrapInfo-impl fakeBootstrapInfo sig)
    → MsgWithSig∈ pk sig pool

  SigsForVotes∈Rm-SentB4 : SentMessages → RoundManager → Set
  SigsForVotes∈Rm-SentB4 pool rm = ∀ {qc v pk} → SigForVote∈Rm-SentB4 v pk qc rm pool

  ++-SigsForVote∈Rm-SentB4
    : ∀ {pool rm} → (msgs : SentMessages) → SigsForVotes∈Rm-SentB4 pool rm
      → SigsForVotes∈Rm-SentB4 (msgs ++ pool) rm
  ++-SigsForVote∈Rm-SentB4{pool} msgs sfvb4 qc∈rm sig vs∈qc rbld≈v ¬bootstrap =
    MsgWithSig∈-++ʳ{ms = msgs} (sfvb4 qc∈rm sig vs∈qc rbld≈v ¬bootstrap)

module Invariants where

  ------------ properties for BlockTree validity

  -- The property that a block tree `bt` has only valid QCs with respect to epoch config `𝓔`
  AllValidQCs : (𝓔 : EpochConfig) (bt : BlockTree) → Set
  AllValidQCs 𝓔 bt = (hash : HashValue) → Maybe-maybe (WithEC.MetaIsValidQC 𝓔) ⊤ (lookup hash (bt ^∙ btIdToQuorumCert))

  AllValidBlocks : BlockTree → Set
  AllValidBlocks bt = ∀ {bid eb}
                    → btGetBlock bid bt ≡ just eb
                    → BlockId-correct (eb ^∙ ebBlock) × BlockHash≡ (eb ^∙ ebBlock)  bid

  ------------ types for and definitions of invariants for BlockTree, BlockStore, SafetyData, SafetyRules

  record ECinfo : Set where
    constructor mkECinfo
    field
      ecVV : ValidatorVerifier
      ecEP : Epoch
  open ECinfo

  WithECinfo : Set → Set
  WithECinfo A = A × ECinfo

  BlockTree-EC  = WithECinfo BlockTree
  BlockStore-EC = WithECinfo BlockStore

  module _ (btEC : BlockTree-EC) where
    private
      bt  = proj₁ btEC
      eci = proj₂ btEC
      vv = ecVV eci
      ep = ecEP eci

    record BlockTreeInv : Set where
      constructor mkBlockTreeInv
      field
        allValidQCs    : (vvC : ValidatorVerifier-correct $ vv) → AllValidQCs (α-EC-VV (vv , vvC) ep) bt
        allValidBlocks : AllValidBlocks bt
  open BlockTreeInv

  module _ (bsEC : BlockStore-EC) where
    private
      bs   = proj₁ bsEC
      eci =  proj₂ bsEC

    record BlockStoreInv : Set where
      constructor mkBlockStoreInv
      field
        blockTreeValid : BlockTreeInv (bs ^∙ bsInner , eci)
  open BlockStoreInv

  module _ (sd : SafetyData) where
    -- SafetyRules invariants
    record SafetyDataInv : Set where
      constructor mkSafetyDataInv
      field
        lvEpoch≡ : Meta.getLastVoteEpoch sd ≡ sd ^∙ sdEpoch
        lvRound≤ : Meta.getLastVoteRound sd ≤ sd ^∙ sdLastVotedRound
  open SafetyDataInv

  subst-SafetyDataInv : ∀ {sd1 sd2}
                      → sd1 ^∙ sdLastVote       ≡ sd2 ^∙ sdLastVote
                      → sd1 ^∙ sdEpoch          ≡ sd2 ^∙ sdEpoch
                      → sd1 ^∙ sdLastVotedRound ≡ sd2 ^∙ sdLastVotedRound
                      → SafetyDataInv sd1 → SafetyDataInv sd2
  subst-SafetyDataInv refl refl refl (mkSafetyDataInv lvEpoch≡₁ lvRound≤₁) =
    mkSafetyDataInv lvEpoch≡₁ lvRound≤₁

  module _ (sr : SafetyRules) where
    -- SafetyRules invariants
    record SafetyRulesInv : Set where
      constructor mkSafetyRulesInv
      field
        sdInv : SafetyDataInv (sr ^∙ srPersistentStorage ∙ pssSafetyData)
  open SafetyRulesInv

  ------------ types for and definition of RoundManagerInv

  EpochsMatch : RoundManager → Set
  EpochsMatch rm = rm ^∙ rmEpochState ∙ esEpoch ≡ rm ^∙ pssSafetyData-rm ∙ sdEpoch

  rm→ECinfo : RoundManager → ECinfo
  rm→ECinfo rm = mkECinfo (rm ^∙ rmEpochState ∙ esVerifier) (rm ^∙ rmEpoch)

  rm→BlockTree-EC : RoundManager → BlockTree-EC
  rm→BlockTree-EC rm = (rm ^∙ lBlockStore ∙ bsInner , rm→ECinfo rm)

  rm→BlockStore-EC : RoundManager → BlockStore-EC
  rm→BlockStore-EC rm = (rm ^∙ lBlockStore , rm→ECinfo rm)

  -- NOTE: This will be proved by induction on reachable states using the
  -- property that peer handlers preserve invariants. That is to say, many of
  -- these cannot be proven as a post-condition of the peer handler: one can
  -- only prove of the handler that if the invariant holds for the prestate,
  -- then it holds for the poststate.

  record RoundManagerInv (rm : RoundManager) : Set where
    constructor mkRoundManagerInv
    field
      rmCorrect        : ValidatorVerifier-correct (rm ^∙ rmValidatorVerifer)
      rmEpochsMatch    : EpochsMatch rm
      rmBlockStoreInv  : BlockStoreInv  (rm→BlockStore-EC rm)
      rmSafetyRulesInv : SafetyRulesInv (rm ^∙ lSafetyRules)
  open RoundManagerInv

  -- This is just the beginning of the invariant for EpochManager, collecting properties we already
  -- expect to be required even though the top-level peer state is RoundManager for now (in future,
  -- when we prove properties related to epoch change, the peers state will become EpochManager).
  record EpochManagerInv (em : EpochManager) : Set where
    constructor mkEpochManagerInv
    field
      -- SafetyRule properties
      emiSRI : ∀ {sr} → em ^∙ emSafetyRulesManager ∙ srmInternalSafetyRules ≡ SRWLocal sr
                      → SafetyRulesInv sr × sr ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ nothing
  open EpochManagerInv

  hash≡⇒≈Block : ∀ {b1 b2 : Block}
               → BlockId-correct b1
               → BlockId-correct b2
               → BlockHash≡ b1 (b2 ^∙ bId)
               → b1 ≈Block b2
  hash≡⇒≈Block {b1} {b2} refl refl hashb1≡idb2
     with hashBD-inj hashb1≡idb2
  ...| bdInj = sameBlockData⇒≈ {b1} {b2} hashb1≡idb2 bdInj

  module Reqs (b : Block) (bt : BlockTree) where
    -- TODO: State and use assumptions about hash collisions.  The following is one example that will
    -- likely need to be refined.
    NoHC1 = ∀ {eb}
            → btGetBlock (b ^∙ bId) bt ≡ just eb
            → BlockId-correct b
            → (eb ^∙ ebBlock) ≈Block b

  -- TODO: probably don't need this generality, consider moving into Handle.Properties (only place
  -- it is used so far), then we could streamline as rmi is required only to avoid cyclic lookups
  module _ {st} (reach : ReachableSystemState st)
           {pm : ProposalMsg} {sndr : NodeId} (nm∈pool : (sndr , P pm) ∈ msgPool st)
           (pid : NodeId) (ini : initialised st pid ≡ initd) where

    open PerReachableState reach

    private
      rm  = peerStates st pid
      bt  = rm ^∙ lBlockTree
      b   = pm ^∙ pmProposal

    nohc : RoundManagerInv rm
         → rm ^∙ lBlockTree ≡ bt
         → BlockId-correct b
         → Reqs.NoHC1 b bt
    nohc rmi refl refl {eb} jeb refl
       with allValidBlocks (blockTreeValid (rmBlockStoreInv rmi)) jeb
    ...| bidCorr , bid
       with (blockData-bsl (b ^∙ bBlockData)) ≟-BSL (blockData-bsl (eb ^∙ ebBlock ∙ bBlockData))
    ...| yes bsls≡ = hash≡⇒≈Block {eb ^∙ ebBlock} {b} bidCorr refl bid
    ...| no  neq rewrite sym bid
       = ⊥-elim (meta-no-collision-in-sys (msgRmHC (inP nm∈pool (inPM inB))
                                                   ini
                                                   (inRM (inBS jeb inB))
                                                   (sym bid)
                                                   neq))

  -- Valid blocks have IDs computed by the hash of their BlockData
  -- These are passed as module parameters through the proofs

  ValidBlock = Σ Block BlockId-correct

  vbBlock : ValidBlock → Block
  vbBlock = proj₁

  vbValid : (vb : ValidBlock) → BlockId-correct (vbBlock vb)
  vbValid = proj₂

  ------------ Preserves and related definitions and utilities

  Preserves : ∀ {ℓ} {A : Set} → (P : A → Set ℓ) (pre post : A) → Set ℓ
  Preserves Pred pre post = Pred pre → Pred post

  PreservesL : ∀ {ℓ} {A B : Set}
               → (P : A → Set ℓ) (l : Lens A B)
               → (b₁ b₂ : B) → Set ℓ
  PreservesL Pred l b₁ b₂ = ∀ a → Preserves Pred (a & l ∙~ b₁) (a & l ∙~ b₂)

  reflPreserves : ∀ {ℓ} {A : Set} (P : A → Set ℓ) → Reflexive (Preserves P)
  reflPreserves Pred = id

  reflPreservesRoundManagerInv : Reflexive (Preserves RoundManagerInv)
  reflPreservesRoundManagerInv = reflPreserves RoundManagerInv

  transPreserves : ∀ {ℓ} {A : Set} (P : A → Set ℓ) → Transitive (Preserves P)
  transPreserves Pred p₁ p₂ = p₂ ∘ p₁

  transPreservesL : ∀ {ℓ} {A B : Set}
                  → (P : A → Set ℓ) (l : Lens A B)
                  → {b₁ b₂ b₃ : B}
                  → PreservesL P l b₁ b₂
                  → PreservesL P l b₂ b₃
                  → PreservesL P l b₁ b₃
  transPreservesL Pred l p₁ p₂ a = transPreserves Pred (p₁ a) (p₂ a)

  transPreservesRoundManagerInv : Transitive (Preserves RoundManagerInv)
  transPreservesRoundManagerInv = transPreserves RoundManagerInv

  BSInv⇒BTInv-pres : ∀ {eci} {pre post : BlockStore}
                   → Preserves BlockStoreInv (pre , eci) (post , eci)
                   → Preserves BlockTreeInv (pre ^∙ bsInner , eci) (post ^∙ bsInner , eci)
  BSInv⇒BTInv-pres presBS btiPre = BlockStoreInv.blockTreeValid (presBS $ mkBlockStoreInv btiPre)

  mkPreservesSafetyRulesInv
    : ∀ {pre post}
      → Preserves SafetyDataInv (pre ^∙ srPersistentStorage ∙ pssSafetyData) (post ^∙ srPersistentStorage ∙ pssSafetyData)
      → Preserves SafetyRulesInv pre post
  mkPreservesSafetyRulesInv lvP (mkSafetyRulesInv lv) = mkSafetyRulesInv (lvP lv)

  mkPreservesRoundManagerInv
    : ∀ {pre post}
      → Preserves ValidatorVerifier-correct (pre ^∙ rmValidatorVerifer) (post ^∙ rmValidatorVerifer)
      → Preserves EpochsMatch                pre                         post
      → Preserves BlockStoreInv             (rm→BlockStore-EC pre)      (rm→BlockStore-EC post)
      → Preserves SafetyRulesInv            (pre ^∙ rmSafetyRules)      (post ^∙ rmSafetyRules)
      → Preserves RoundManagerInv            pre                         post
  mkPreservesRoundManagerInv rmP emP bsP srP (mkRoundManagerInv rmCorrect epochsMatch bsInv srInv) =
    mkRoundManagerInv (rmP rmCorrect) (emP epochsMatch) (bsP bsInv) (srP srInv)

module InitProofDefs where
  open Invariants

-- RoundManager properties

  _IsNormalRoundManagerOf_ : RoundManager → EpochManager → Set
  _IsNormalRoundManagerOf_ rm em =
    em ^∙ emProcessor ≡ just (RoundProcessorNormal rm)

  IsNormalRoundManagerOf-inj :
    ∀ {em} {rm1} {rm2}
    → rm1 IsNormalRoundManagerOf em
    → rm2 IsNormalRoundManagerOf em
    → rm1 ≡ rm2
  IsNormalRoundManagerOf-inj refl refl = refl

  InitSdLV≡ : RoundManager → Maybe Vote → Set
  InitSdLV≡ rm mv = rm ^∙ rmSafetyRules ∙ srPersistentStorage
                        ∙ pssSafetyData ∙ sdLastVote ≡ mv

  InitSigs∈bs : RoundManager → Set
  InitSigs∈bs rm = ∀ {bsi vs qc}
                   → vs              ∈     qcVotes qc
                   → qc QCProps.∈RoundManager rm
                   → ∈BootstrapInfo-impl bsi (proj₂ vs)

  -- Message properties

  -- During epoch initialisation, no messages are sent
  -- EXCEPT the leader of Round 1 SENDS a ProposalMsg during initialization.
  -- Rust/Haskell impls do not include signatures in the genesis QC's LIWS.
  -- The initial proposal for (Epoch N) (Round 1) is built on a QC with empty signatures.

  InitIsInitPM' : NetworkMsg → Set
  InitIsInitPM' m = ∃[ pm ] ( m ≡ P pm
                            × ∀ {vs qc}
                            → vs   ∈ qcVotes qc
                            → qc QC∈NM       m
                            → ⊥)

  InitIsInitPM : List (Action NetworkMsg) → Set
  InitIsInitPM acts = ∀ {m}
                      → send m ∈ acts
                      → InitIsInitPM' m

  record InitContractOk (mv : Maybe Vote) (rm : RoundManager) (outs : List Output) : Set where
    constructor mkInitContractOk
    field
      rmInv       : RoundManagerInv rm
      sdLV≡       : InitSdLV≡ rm mv
      sigs∈bs     : InitSigs∈bs rm
      isInitPM    : InitIsInitPM (outputsToActions {State = rm} outs)
  open InitContractOk

  EMInitCond : Maybe Vote → EpochManager × List Output → Set
  EMInitCond mv (em , outs) = ∃[ rm ] ( rm IsNormalRoundManagerOf em × InitContractOk mv rm outs )

  InitContract : Maybe Vote → EitherD-Post ErrLog (EpochManager × List Output)
  InitContract _ (Left x)        = ⊤
  InitContract mv (Right em×outs) = EMInitCond mv em×outs

module RoundManagerTransProps where
  -- Relations between the pre/poststate which may or may not hold, depending on
  -- the particular peer handler invoked

  -- - The epoch is unchanged
  NoEpochChange : (pre post : RoundManager) → Set
  NoEpochChange pre post = pre ≡L post at rmEpoch

  reflNoEpochChange : Reflexive NoEpochChange
  reflNoEpochChange = refl

  transNoEpochChange : Transitive NoEpochChange
  transNoEpochChange = trans

  NoSafetyDataChange : (pre post : RoundManager) → Set
  NoSafetyDataChange pre post = pre ≡L post at pssSafetyData-rm

  reflNoSafetyDataChange : Reflexive NoSafetyDataChange
  reflNoSafetyDataChange = refl

  transNoSafetyDataChange : Transitive NoSafetyDataChange
  transNoSafetyDataChange = trans

  -- - state changes from generating or not generating a vote
  LastVoteIs : RoundManager → Vote → Set
  LastVoteIs rm v = just v ≡ rm ^∙ pssSafetyData-rm ∙ sdLastVote

  module _ (pre post : RoundManager) (vote : Vote) where

    record VoteOldGenerated : Set where
      constructor mkVoteOldGenerated
      field
        -- NOTE: The implementation maintains an invariant that the round
        -- associated with `sdLastVote` (if the vote exists) is less than or
        -- equal to the field `sdLastVotedRound`.
        lvr≡ : pre ≡L post at pssSafetyData-rm ∙ sdLastVotedRound
        lv≡  : pre ≡L post at pssSafetyData-rm ∙ sdLastVote

    record VoteNewGenerated : Set where
      constructor mkVoteNewGenerated
      field
        lvr< : pre [ _<_ ]L post at pssSafetyData-rm ∙ sdLastVotedRound
        lvr≡ : vote ^∙ vRound ≡ post ^∙ pssSafetyData-rm ∙ sdLastVotedRound

    -- NOTE: This is saying that /state changes/ associated to generating a vote
    -- have occurred, not that the generated vote has been sent.
    record VoteGenerated : Set where
      constructor mkVoteGenerated
      field
        lv≡v    : LastVoteIs post vote
        voteSrc : VoteOldGenerated ⊎ VoteNewGenerated

    isVoteNewGenerated : VoteGenerated → Bool
    isVoteNewGenerated = isRight ∘ VoteGenerated.voteSrc

  reflVoteOldGenerated : ∀ {v} → Reflexive (λ pre post → VoteOldGenerated pre post v)
  reflVoteOldGenerated = mkVoteOldGenerated refl refl

  VoteGeneratedNotSaved : (pre post : RoundManager) → Set
  VoteGeneratedNotSaved pre post = ∃[ v ] VoteGenerated pre post v

  module _ (pre post : RoundManager) where
    -- In
    -- `LibraBFT.Impl.Consensus.SafetyRules.SafetyRules.agda::contructAndSignVoteM`,
    -- it is possible for us to update the field `pssSafetyData-rm ∙ sdLastVotedRound`
    -- without actually returning a vote. Therefore, the most we can say after
    -- returing from this function is that this field in the poststate is greater
    -- than or equal to the value it started at in the prestate.
    --
    -- However, it is also possible to return a vote *without* updating the last
    -- voted round. Many functions in `LibraBFT.Impl.Consensus.RoundManager` neither
    -- return a vote nor update the last voted round, and the lemma
    -- `pseudotransVoteSent` in those cases -- but is unprovable if we do not
    -- distinguish the cases where the last voted round cannot be increased.
    -- Therefore, it is convenient to track in the type of `NoVoteSent`, with the
    -- parameter `lvr≡?`, which case we are dealing with
    record VoteNotGenerated  (lvr≡? : Bool) : Set where
      constructor mkVoteNotGenerated
      field
        lv≡  : pre ≡L post at pssSafetyData-rm ∙ sdLastVote
        lvr≤ : pre [ if lvr≡? then _≡_ else _<_ ]L post at pssSafetyData-rm ∙ sdLastVotedRound

  reflVoteNotGenerated : Reflexive (λ pre post → VoteNotGenerated pre post true)
  reflVoteNotGenerated = mkVoteNotGenerated refl refl

  transVoteNotGenerated
    : ∀ {s₁ s₂ s₃ lvr≡?₁ lvr≡?₂}
      → VoteNotGenerated s₁ s₂ lvr≡?₁ → VoteNotGenerated s₂ s₃ lvr≡?₂
      → VoteNotGenerated s₁ s₃ (lvr≡?₁ ∧ lvr≡?₂)
  transVoteNotGenerated {lvr≡?₁ = false} {false} (mkVoteNotGenerated lv≡ lvr≤) (mkVoteNotGenerated lv≡₁ lvr≤₁) =
    mkVoteNotGenerated (trans lv≡ lv≡₁) (<-trans lvr≤ lvr≤₁)
  transVoteNotGenerated {lvr≡?₁ = false} {true} (mkVoteNotGenerated lv≡ lvr≤) (mkVoteNotGenerated lv≡₁ lvr≤₁) =
    mkVoteNotGenerated (trans lv≡ lv≡₁) (≤-trans lvr≤ (≡⇒≤ lvr≤₁))
  transVoteNotGenerated {lvr≡?₁ = true} {false} (mkVoteNotGenerated lv≡ lvr≤) (mkVoteNotGenerated lv≡₁ lvr≤₁) =
    mkVoteNotGenerated (trans lv≡ lv≡₁) (≤-trans (s≤s (≡⇒≤ lvr≤)) lvr≤₁)
  transVoteNotGenerated {lvr≡?₁ = true} {true} (mkVoteNotGenerated lv≡ lvr≤) (mkVoteNotGenerated lv≡₁ lvr≤₁) =
    mkVoteNotGenerated (trans lv≡ lv≡₁) (trans lvr≤ lvr≤₁)

  glue-VoteGenerated-VoteNotGenerated
    : ∀ {s₁ s₂ s₃ v} → VoteGenerated s₁ s₂ v → VoteNotGenerated s₂ s₃ true
      → VoteGenerated s₁ s₃ v
  glue-VoteGenerated-VoteNotGenerated (mkVoteGenerated lv≡v (inj₁ (mkVoteOldGenerated lvr≡₁ lv≡₁))) (mkVoteNotGenerated lv≡ lvr≤) =
    mkVoteGenerated (trans lv≡v lv≡) (inj₁ (mkVoteOldGenerated (trans lvr≡₁ lvr≤) (trans lv≡₁ lv≡)))
  glue-VoteGenerated-VoteNotGenerated (mkVoteGenerated lv≡v (inj₂ (mkVoteNewGenerated lvr< lvr≡))) (mkVoteNotGenerated lv≡ lvr≤) =
    mkVoteGenerated ((trans lv≡v lv≡)) (inj₂ (mkVoteNewGenerated (≤-trans lvr< (≡⇒≤ lvr≤)) (trans lvr≡ lvr≤)))

  glue-VoteNotGenerated-VoteGenerated
    : ∀ {s₁ s₂ s₃ v} → VoteNotGenerated s₁ s₂ true → VoteGenerated s₂ s₃ v
      → VoteGenerated s₁ s₃ v
  glue-VoteNotGenerated-VoteGenerated (mkVoteNotGenerated lv≡ lvr≤) (mkVoteGenerated lv≡v (inj₁ (mkVoteOldGenerated lvr≡₁ lv≡₁))) =
    mkVoteGenerated lv≡v (inj₁ (mkVoteOldGenerated (trans lvr≤ lvr≡₁) (trans lv≡ lv≡₁)))
  glue-VoteNotGenerated-VoteGenerated (mkVoteNotGenerated lv≡ lvr≤) (mkVoteGenerated lv≡v (inj₂ (mkVoteNewGenerated lvr<₁ lvr≡₁))) =
    mkVoteGenerated lv≡v (inj₂ (mkVoteNewGenerated (≤-trans (s≤s (≡⇒≤ lvr≤)) lvr<₁) lvr≡₁))

  glue-VoteNotGenerated-VoteGeneratedNotSaved
    : ∀ {s₁ s₂ s₃} → VoteNotGenerated s₁ s₂ true → VoteGeneratedNotSaved s₂ s₃
      → VoteGeneratedNotSaved s₁ s₃
  glue-VoteNotGenerated-VoteGeneratedNotSaved vng (v , vg) =
    v , glue-VoteNotGenerated-VoteGenerated vng vg

-- Properties for voting
module Voting where

  open Invariants

  VoteEpochIs : (vote : Vote) (e : Epoch) → Set
  VoteEpochIs vote e = vote ^∙ vEpoch ≡ e

  VoteRoundIs : (vote : Vote) (r : Round) → Set
  VoteRoundIs vote r = vote ^∙ vRound ≡ r

  record VoteMadeFromBlock (vote : Vote) (block : Block) : Set where
    constructor mkVoteMadeFromBlock
    field
      epoch≡      : vote ^∙ vEpoch ≡ block ^∙ bEpoch
      round≡      : vote ^∙ vRound ≡ block ^∙ bRound
      proposedId≡ : vote ^∙ vProposedId ≡ block ^∙ bId

  VoteMadeFromBlock⇒VoteEpochRoundIs : ∀ {v b} → VoteMadeFromBlock v b → VoteEpochIs v (b ^∙ bEpoch) × VoteRoundIs v (b ^∙ bRound)
  VoteMadeFromBlock⇒VoteEpochRoundIs (mkVoteMadeFromBlock epoch≡ round≡ proposedID) = epoch≡ , round≡

  VoteTriggeredByBlock : (vote : Vote) (block : Block) (new? : Bool) → Set
  VoteTriggeredByBlock vote block true = VoteMadeFromBlock vote block
  VoteTriggeredByBlock vote block false = VoteRoundIs vote (block ^∙ bRound)

  record VoteGeneratedCorrect (pre post : RoundManager) (vote : Vote) (block : Block) : Set where
    constructor mkVoteGeneratedCorrect
    field
      state          : RoundManagerTransProps.VoteGenerated pre post vote
    voteNew? = RoundManagerTransProps.isVoteNewGenerated pre post vote state
    field
      blockTriggered : VoteTriggeredByBlock vote block voteNew?

  substVoteGeneratedCorrect
    : ∀ {pre post vote} (block₁ block₂ : Block) → block₁ ≈Block block₂
      → VoteGeneratedCorrect pre post vote block₁ → VoteGeneratedCorrect pre post vote block₂
  substVoteGeneratedCorrect block₁ block₂ bd≡ (mkVoteGeneratedCorrect state blockTriggered)
     with state
  ...| RoundManagerTransProps.mkVoteGenerated lv≡v voteSrc
     with voteSrc
  ...| Left vog rewrite bd≡ =
     mkVoteGeneratedCorrect (RoundManagerTransProps.mkVoteGenerated lv≡v (Left vog)) blockTriggered
  ...| Right vng
     with blockTriggered
  ...| mkVoteMadeFromBlock epoch≡ round≡ proposedID rewrite bd≡
     = mkVoteGeneratedCorrect
         (RoundManagerTransProps.mkVoteGenerated lv≡v (Right vng))
         (mkVoteMadeFromBlock epoch≡ round≡ proposedID)

  record VoteGeneratedUnsavedCorrect (pre post : RoundManager) (block : Block) : Set where
    constructor mkVoteGeneratedUnsavedCorrect
    field
      vote           : Vote
      voteGenCorrect : VoteGeneratedCorrect pre post vote block

  glue-VoteGeneratedCorrect-VoteNotGenerated
    : ∀ {s₁ s₂ s₃ vote block}
      → VoteGeneratedCorrect s₁ s₂ vote block
      → RoundManagerTransProps.VoteNotGenerated s₂ s₃ true
      → VoteGeneratedCorrect s₁ s₃ vote block
  glue-VoteGeneratedCorrect-VoteNotGenerated vgc@(mkVoteGeneratedCorrect vg@(RoundManagerTransProps.mkVoteGenerated lv≡v (inj₁ oldVG)) blockTriggered) vng =
    mkVoteGeneratedCorrect (RoundManagerTransProps.glue-VoteGenerated-VoteNotGenerated vg vng) blockTriggered
  glue-VoteGeneratedCorrect-VoteNotGenerated vgc@(mkVoteGeneratedCorrect vg@(RoundManagerTransProps.mkVoteGenerated lv≡v (inj₂ newVG)) blockTriggered) vng =
    mkVoteGeneratedCorrect (RoundManagerTransProps.glue-VoteGenerated-VoteNotGenerated vg vng) blockTriggered

  glue-VoteNotGenerated-VoteGeneratedCorrect
    : ∀ {s₁ s₂ s₃ vote block}
      → RoundManagerTransProps.VoteNotGenerated s₁ s₂ true
      → VoteGeneratedCorrect s₂ s₃ vote block
      → VoteGeneratedCorrect s₁ s₃ vote block
  glue-VoteNotGenerated-VoteGeneratedCorrect vng (mkVoteGeneratedCorrect vg@(RoundManagerTransProps.mkVoteGenerated lv≡v (inj₁ oldVG)) blockTriggered) =
    mkVoteGeneratedCorrect (RoundManagerTransProps.glue-VoteNotGenerated-VoteGenerated vng vg) blockTriggered
  glue-VoteNotGenerated-VoteGeneratedCorrect vng (mkVoteGeneratedCorrect vg@(RoundManagerTransProps.mkVoteGenerated lv≡v (inj₂ newVG)) blockTriggered) =
    mkVoteGeneratedCorrect (RoundManagerTransProps.glue-VoteNotGenerated-VoteGenerated vng vg)
      blockTriggered

  glue-VoteNotGenerated-VoteGeneratedUnsavedCorrect
    : ∀ {s₁ s₂ s₃ block}
      → RoundManagerTransProps.VoteNotGenerated s₁ s₂ true
      → VoteGeneratedUnsavedCorrect s₂ s₃ block
      → VoteGeneratedUnsavedCorrect s₁ s₃ block
  glue-VoteNotGenerated-VoteGeneratedUnsavedCorrect vng (mkVoteGeneratedUnsavedCorrect vote voteGenCorrect) =
    mkVoteGeneratedUnsavedCorrect vote (glue-VoteNotGenerated-VoteGeneratedCorrect vng voteGenCorrect)

  -- The handler correctly voted (including state updates) on `block`, assuming
  -- the safety data epoch matches the block epoch.
  record VoteSentCorrect (pre post : RoundManager) (outs : List Output) (block : Block) : Set where
    constructor mkVoteSentCorrect
    field
      vm           : VoteMsg
      pid          : Author
      voteMsgOuts  : OutputProps.OneVote outs vm (pid ∷ [])
      vgCorrect    : VoteGeneratedCorrect pre post (vm ^∙ vmVote) block
    open VoteGeneratedCorrect vgCorrect

  -- The handler correctly did not vote on `block`
  record VoteUnsentCorrect (pre post : RoundManager) (outs : List Output) (block : Block) (lvr≡? : Bool) : Set where
    constructor mkVoteUnsentCorrect
    field
      noVoteMsgOuts : OutputProps.NoVotes outs
      nvg⊎vgusc    : RoundManagerTransProps.VoteNotGenerated pre post lvr≡? ⊎ VoteGeneratedUnsavedCorrect pre post block

  glue-VoteNotGenerated-VoteUnsentCorrect
    : ∀ {s₁ s₂ s₃ outs₁ outs₂ block lvr≡?}
      → RoundManagerTransProps.VoteNotGenerated s₁ s₂ true → OutputProps.NoVotes outs₁
      → VoteUnsentCorrect s₂ s₃ outs₂ block lvr≡?
      → VoteUnsentCorrect s₁ s₃ (outs₁ ++ outs₂) block lvr≡?
  glue-VoteNotGenerated-VoteUnsentCorrect{outs₁ = outs₁} vng₁ nvo (mkVoteUnsentCorrect noVoteMsgOuts (inj₁ vng₂)) =
    mkVoteUnsentCorrect (OutputProps.++-NoVotes outs₁ _ nvo noVoteMsgOuts) (inj₁ (RoundManagerTransProps.transVoteNotGenerated vng₁ vng₂))
  glue-VoteNotGenerated-VoteUnsentCorrect{outs₁ = outs₁} vng₁ nvo (mkVoteUnsentCorrect noVoteMsgOuts (inj₂ vgus)) =
    mkVoteUnsentCorrect ((OutputProps.++-NoVotes outs₁ _ nvo noVoteMsgOuts)) (inj₂ (glue-VoteNotGenerated-VoteGeneratedUnsavedCorrect vng₁ vgus))

  -- The handler correctly attempted to vote on `block`, assuming the safety
  -- data epoch matches the block epoch.
  VoteAttemptCorrect : (pre post : RoundManager) (outs : List Output) (block : Block) → Set
  VoteAttemptCorrect pre post outs block =
    (∃[ lvr≡? ] VoteUnsentCorrect pre post outs block lvr≡?) ⊎ VoteSentCorrect pre post outs block

  -- The voting process ended before `pssSafetyData-rm` could be updated
  voteAttemptBailed : ∀ {rm block} outs → OutputProps.NoVotes outs → VoteAttemptCorrect rm rm outs block
  voteAttemptBailed outs noVotesOuts = inj₁ (true , mkVoteUnsentCorrect noVotesOuts (inj₁ RoundManagerTransProps.reflVoteNotGenerated))

  glue-VoteNotGenerated-VoteAttemptCorrect
    : ∀ {s₁ s₂ s₃ outs₁ outs₂ block}
      → RoundManagerTransProps.VoteNotGenerated s₁ s₂ true → OutputProps.NoVotes outs₁
      → VoteAttemptCorrect s₂ s₃ outs₂ block
      → VoteAttemptCorrect s₁ s₃ (outs₁ ++ outs₂) block
  glue-VoteNotGenerated-VoteAttemptCorrect{outs₁ = outs₁} vng nvo (inj₁ (lvr≡? , vusCorrect)) =
    inj₁ (lvr≡? , glue-VoteNotGenerated-VoteUnsentCorrect{outs₁ = outs₁} vng nvo vusCorrect)
  glue-VoteNotGenerated-VoteAttemptCorrect{outs₁ = outs₁} vng nvo (inj₂ (mkVoteSentCorrect vm pid voteMsgOuts vgCorrect)) =
    inj₂ (mkVoteSentCorrect vm pid (OutputProps.++-NoVotes-OneVote outs₁ _ nvo voteMsgOuts) (glue-VoteNotGenerated-VoteGeneratedCorrect vng vgCorrect))

  VoteAttemptEpochReq : ∀ {pre post outs block} → VoteAttemptCorrect pre post outs block → Set
  VoteAttemptEpochReq (inj₁ (_ , mkVoteUnsentCorrect _ (inj₁ _))) =
    ⊤
  VoteAttemptEpochReq{pre}{block = block} (inj₁ (_ , mkVoteUnsentCorrect _ (inj₂ _))) =
    pre ^∙ pssSafetyData-rm ∙ sdEpoch ≡ (block ^∙ bEpoch)
  VoteAttemptEpochReq{pre}{block = block} (inj₂ _) =
    pre ^∙ pssSafetyData-rm ∙ sdEpoch ≡ (block ^∙ bEpoch)

  voteAttemptEpochReq!
    : ∀ {pre post outs block} → (vac : VoteAttemptCorrect pre post outs block)
      → pre ^∙ pssSafetyData-rm ∙ sdEpoch ≡ block ^∙ bEpoch → VoteAttemptEpochReq vac
  voteAttemptEpochReq! (inj₁ (_ , mkVoteUnsentCorrect _ (inj₁ _))) eq = tt
  voteAttemptEpochReq! (inj₁ (_ , mkVoteUnsentCorrect _ (inj₂ _))) eq = eq
  voteAttemptEpochReq! (inj₂ _) eq = eq

  record VoteAttemptCorrectWithEpochReq (pre post : RoundManager) (outs : List Output) (block : Block) : Set where
    constructor mkVoteAttemptCorrectWithEpochReq
    field
      voteAttempt : VoteAttemptCorrect pre post outs block
      sdEpoch≡?   : VoteAttemptEpochReq voteAttempt

  voteAttemptCorrectAndSent⇒voteSentCorrect : ∀ {pre post outs block vm}
                         → send (V vm) ∈ outputsToActions{pre} outs
                         → VoteAttemptCorrectWithEpochReq pre post outs block
                         → VoteSentCorrect                pre post outs block
  voteAttemptCorrectAndSent⇒voteSentCorrect{pre}{outs = outs} vm∈outs (mkVoteAttemptCorrectWithEpochReq (Left (_ , mkVoteUnsentCorrect noVoteMsgOuts _)) _) =
    ⊥-elim (sendVote∉actions{outs}{st = pre} (sym noVoteMsgOuts) vm∈outs)
  voteAttemptCorrectAndSent⇒voteSentCorrect{pre}{outs = outs}{vm = vm} vm∈outs (mkVoteAttemptCorrectWithEpochReq (Right vsc) _) = vsc


text:
module UselessPrivateImport2 where

private
  open import Common.Issue481ParametrizedModule Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module ATPRepeteadConjecture where

-- This error is detected by TypeChecking.Monad.Signature.

postulate
  D   : Set
  _≡_ : D → D → Set
  p   : ∀ d e → d ≡ e

-- The conjecture foo is rejected because it is repetead.
postulate foo : ∀ d e → d ≡ e
{-# ATP prove foo #-}
{-# ATP prove foo p #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
{-# OPTIONS --allow-exec #-}

open import Agda.Builtin.FromNat

open import Data.Bool.Base using (T; Bool; if_then_else_)
open import Data.String using (String; _++_; lines)
open import Data.Nat.Base using (ℕ)
open import Data.Fin using (Fin)
import Data.Fin.Literals as Fin
import Data.Nat.Literals as Nat
open import Data.Vec.Base using (Vec)
open import Data.Float.Base using (Float; _≤ᵇ_)
open import Data.List.Base using (List; []; _∷_)
open import Data.Unit.Base using (⊤; tt)
open import Relation.Nullary using (does)
open import Relation.Binary.Core using (Rel)

open import Reflection.Argument
open import Reflection.Term
open import Reflection.External
open import Reflection.TypeChecking.Monad
open import Reflection.TypeChecking.Monad.Syntax
open import Reflection.Show using (showTerm)

open import Vehicle.Utils

module Vehicle where

------------------------------------------------------------------------
-- Metadata
------------------------------------------------------------------------

VEHICLE_COMMAND : String
VEHICLE_COMMAND = "vehicle"

------------------------------------------------------------------------
-- Execution
------------------------------------------------------------------------

record EvaluateArgs : Set where
  field
    projectFile : String
    networkUUID  : String

evaluateCmd : EvaluateArgs → CmdSpec
evaluateCmd args = cmdSpec VEHICLE_COMMAND
  ( "evaluate"
  ∷ ("--databaseFile=" ++ projectFile)
  ∷ networkUUID
  ∷ []) ""
  where open EvaluateArgs args

-- TODO
postulate evaluate : EvaluateArgs →
                    ∀ {a b} {A : Set a} {B : Set b} →
                    A → B

------------------------------------------------------------------------
-- Checking
------------------------------------------------------------------------

record CheckArgs : Set where
  field
    projectFile  : String
    propertyUUID : String

checkCmd : CheckArgs → CmdSpec
checkCmd checkArgs = cmdSpec VEHICLE_COMMAND
  ( "check"
  ∷ ("--databaseFile=" ++ projectFile)
  ∷ ("--property=" ++ propertyUUID)
  ∷ []) ""
  where open CheckArgs checkArgs

checkSuccessful : String → Bool
checkSuccessful output = "Valid" ⊆ output

postulate valid : ∀ {a} {A : Set a} → A

`valid : Term
`valid = def (quote valid) (hArg unknown ∷ [])

checkPropertyMacro : CheckArgs → Term → TC ⊤
checkPropertyMacro args hole = do
  goal   ← inferType hole
  -- (showTerm goal)
  output ← runCmdTC (checkCmd args)
  if checkSuccessful output
    then unify hole `valid
    else typeError (strErr ("Error: " ++ output) ∷ [])

macro
  checkProperty : CheckArgs → Term → TC ⊤
  checkProperty = checkPropertyMacro

------------------------------------------------------------------------
-- Other
------------------------------------------------------------------------

instance
  finNumber : ∀ {n} -> Number (Fin n)
  finNumber {n} = Fin.number n

  natNumber : Number ℕ
  natNumber = Nat.number

ze : Fin 5
ze = 0

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


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

module Types where

import Level
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary

--

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

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

U∼ : U → Set₁
U∼ u = Rel ⟦ u ⟧ (Level.zero)

record Typ : Set₁ where
  field
    carr : U
    auto : U∼ carr

BOOL : U
BOOL = PLUS ONE ONE

FALSE TRUE : ⟦ BOOL ⟧
FALSE = inj₁ tt
TRUE  = inj₂ tt

data ONE∼ : U∼ ONE where
  id : ONE∼ tt tt

data BOOL∼ : U∼ BOOL where
  idff : BOOL∼ FALSE FALSE
  idft : BOOL∼ FALSE TRUE
  idtf : BOOL∼ TRUE  FALSE
  idtt : BOOL∼ TRUE  TRUE

--

{--
Then < Bool , ~* > is essentially < Unit , ~= >

Now we need to define what it means to say < U1, ~1> + < U2, ~2 > etc.
and then what it means for two types to be equivalent etc. etc. etc.
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Pi1Examples where

open import PiU using (U; ONE)
open import PiLevel0 using (_⟷_; _◎_; _⊗_; id⟷;
  swap₊; unite⋆l; unite⋆r;
  swap⋆; uniti⋆l; uniti⋆r)
open import Pi0Examples using (BOOL)
open import PiLevel1 using (_⇔_; id⇔; trans⇔; _⊡_;
  assoc◎l; swapl⋆⇔; assoc◎r; linv◎l; idl◎l; idr◎l; unitil⋆⇔l)

------------------------------------------------------------------------------
-- Better syntax for writing 2paths

infix  2  _▤
infixr 2  _⇔⟨_⟩_

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

_▤ : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → (c ⇔ c)
_▤ c = id⇔

------------------------------------------------------------------------------
-- a nice example of 2 paths

neg₁ neg₂ neg₃ neg₄ neg₅ : BOOL ⟷ BOOL
neg₁ = swap₊
neg₂ = id⟷ ◎ swap₊
neg₃ = swap₊ ◎ swap₊ ◎ swap₊
neg₄ = swap₊ ◎ id⟷
neg₅ = uniti⋆l ◎ swap⋆ ◎ (swap₊ ⊗ id⟷) ◎ swap⋆ ◎ unite⋆l
neg₆ = uniti⋆r ◎ (swap₊ {ONE} {ONE} ⊗ id⟷) ◎ unite⋆r

negEx : neg₅ ⇔ neg₁
negEx = uniti⋆l ◎ (swap⋆ ◎ ((swap₊ ⊗ id⟷) ◎ (swap⋆ ◎ unite⋆l)))
          ⇔⟨ id⇔ ⊡ assoc◎l ⟩
        uniti⋆l ◎ ((swap⋆ ◎ (swap₊ ⊗ id⟷)) ◎ (swap⋆ ◎ unite⋆l))
          ⇔⟨ id⇔ ⊡ (swapl⋆⇔ ⊡ id⇔) ⟩
        uniti⋆l ◎ (((id⟷ ⊗ swap₊) ◎ swap⋆) ◎ (swap⋆ ◎ unite⋆l))
          ⇔⟨ id⇔ ⊡ assoc◎r ⟩
        uniti⋆l ◎ ((id⟷ ⊗ swap₊) ◎ (swap⋆ ◎ (swap⋆ ◎ unite⋆l)))
          ⇔⟨ id⇔ ⊡ (id⇔ ⊡ assoc◎l) ⟩
        uniti⋆l ◎ ((id⟷ ⊗ swap₊) ◎ ((swap⋆ ◎ swap⋆) ◎ unite⋆l))
          ⇔⟨ id⇔ ⊡ (id⇔ ⊡ (linv◎l ⊡ id⇔)) ⟩
        uniti⋆l ◎ ((id⟷ ⊗ swap₊) ◎ (id⟷ ◎ unite⋆l))
          ⇔⟨ id⇔ ⊡ (id⇔ ⊡ idl◎l) ⟩
        uniti⋆l ◎ ((id⟷ ⊗ swap₊) ◎ unite⋆l)
          ⇔⟨ assoc◎l ⟩
        (uniti⋆l ◎ (id⟷ ⊗ swap₊)) ◎ unite⋆l
          ⇔⟨ unitil⋆⇔l ⊡ id⇔ ⟩
        (swap₊ ◎ uniti⋆l) ◎ unite⋆l
          ⇔⟨ assoc◎r ⟩
        swap₊ ◎ (uniti⋆l ◎ unite⋆l)
          ⇔⟨ id⇔ ⊡ linv◎l ⟩
        swap₊ ◎ id⟷
          ⇔⟨ idr◎l ⟩
        swap₊ ▤

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


text:
module FamilyPattern where

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

postulate C : {A : Set} -> A -> Set

-- We can't solve unify x = y since the type is a meta variable.
subst : {A : Set}{x y : A} -> x == y -> C y -> C x
subst refl cx = cx
-- subst {A}          refl cx = cx -- works
-- subst {x = x} .{x} refl cx = cx -- works

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym3n where

open import Symmetric
open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin
open import Data.Fin.Permutation hiding (_∘ₚ_)

infixr  200 _∘ₚ_
_∘ₚ_ = Data.Fin.Permutation._∘ₚ_

sym3solvable : solvable (Symmetric 3)
solvable.dervied-length sym3solvable = 2
solvable.end sym3solvable x d = solved1 x d where

   open import Data.List using ( List ; [] ; _∷_ )

   open Solvable (Symmetric 3)
   open import FLutil
   open import Data.List.Fresh hiding ([_])
   open import Relation.Nary using (⌊_⌋)

   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
   p0id = pleq _ _ refl

   open import Data.List.Fresh.Relation.Unary.Any
   open import FLComm

   stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
   stage3FList = refl

   solved1 :  (x : Permutation 3 3) → deriving 2 x → x =p= pid
   solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where
      solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
      solved2 = CommStage→ 3 2 x dr

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


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

module WithoutK-PatternMatchingLambdas2 where

-- Equality defined with two indices.
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

-- The --cubical-compatible option works with pattern matching lambdas.
K : (A : Set) (x : A) (P : x ≡ x → Set) → P (refl x) → (p : x ≡ x ) →  P p
K = λ { A .x P pr (refl x) → pr }


text:
module Sized.Parrot where

open import Data.Product
open import Data.String.Base

open import SizedIO.IOObject

open import SizedIO.Base
open import SizedIO.Console hiding (main)
open import SizedIO.ConsoleObject

open import NativeIO

open import Sized.SimpleCell hiding (program; main)

open import Size

record Wrap A : Set where
  constructor wrap
  field unwrap : A

parrotI = cellJ (Wrap String)

ParrotC : (i : Size) → Set
ParrotC i = ConsoleObject i parrotI

-- but reusing cellC from SimpleCell, as interface is ident!

-- class Parrot implements Cell {
--   Cell cell;
--   Parrot (Cell c) { cell = c; }
--   public String get() {
--     return "(" + cell.get() + ") is what parrot got";
--   }
--   public void put (String s) {
--     cell.put("parrot puts (" + s + ")");
--   }
-- }

-- parrotP is constructor for the consoleObject for interface (cellI String)

parrotP : ∀{i} (c : CellC i) → ParrotC i
(method (parrotP c) get) =
  method c get >>= λ { (s , c') →
  return (wrap ("(" ++ s ++ ") is what parrot got") ,  parrotP c' )  }
(method (parrotP c) (put (wrap s))) =
  method c (put ("parrot puts (" ++ s ++ ")")) >>= λ { (_ , c') →
  return (_ ,  parrotP c') }

--   public static void main (String[] args) {
--     Parrot c = new Parrot(new SimpleCell("Start"));
--     System.out.println(c.get());
--     c.put(args[1]);
--     System.out.println(c.get());
--   }
-- }

program : String → IOConsole ∞ Unit
program arg =
  let c₀ = parrotP (cellP "Start") in
  method c₀ get               >>= λ{ (wrap s   , c₁) →
  exec1 (putStrLn s)            >>
  method c₁ (put (wrap arg))  >>= λ{ (_        , c₂) →
  method c₂ get               >>= λ{ (wrap s'  , c₃) →
  exec1 (putStrLn s')           }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")

-- -}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import HoTT

module homotopy.FinWedge where

module _ {i} {I} (X : Fin I → Ptd i) where

  {- the function for cofiber -}
  finwedge-f : Fin I → Σ (Fin I) (de⊙ ∘ X)
  finwedge-f = bigwedge-f X

  FinWedge : Type i
  FinWedge = BigWedge X

  ⊙FinWedge : Ptd i
  ⊙FinWedge = ⊙BigWedge X

module _ {i} {I} {X : Fin I → Ptd i} where

  fwbase : FinWedge X
  fwbase = bwbase

  fwin : (<I : Fin I) → de⊙ (X <I) → FinWedge X
  fwin = bwin

  ⊙fwin : (<I : Fin I) → X <I ⊙→ ⊙FinWedge X
  ⊙fwin = ⊙bwin

  fwglue : (<I : Fin I) → fwbase == fwin <I (pt (X <I))
  fwglue = cfglue

module _ {i} {I} {X : Ptd i} where

  ⊙fwproj-in : Fin I → Fin I → X ⊙→ X
  ⊙fwproj-in = ⊙bwproj-in Fin-has-dec-eq

  module FinWedgeProj (<I : Fin I) = BigWedgeProj Fin-has-dec-eq {X = X} <I

  fwproj : Fin I → FinWedge (λ _ → X) → de⊙ X
  fwproj = FinWedgeProj.f

  ⊙fwproj : Fin I → ⊙FinWedge (λ _ → X) ⊙→ X
  ⊙fwproj <I = fwproj <I , idp

  fwproj-fwin-diag : (<I : Fin I) → fwproj <I ∘ fwin <I ∼ idf (de⊙ X)
  fwproj-fwin-diag <I = bwproj-bwin-diag Fin-has-dec-eq <I

  fwproj-fwin-≠ : ∀ {<I <I'} → <I ≠ <I' → fwproj <I ∘ fwin <I' ∼ cst (pt X)
  fwproj-fwin-≠ = bwproj-bwin-≠ Fin-has-dec-eq

module _ {i₀ i₁} {I} {X₀ : Fin I → Ptd i₀} {X₁ : Fin I → Ptd i₁}
  (Xeq : ∀ <I → X₀ <I ⊙≃ X₁ <I) where

  finwedge-span-emap-r : SpanEquiv (cofiber-span (finwedge-f X₀)) (cofiber-span (finwedge-f X₁))
  finwedge-span-emap-r = bigwedge-span-emap-r Xeq

  FinWedge-emap-r : FinWedge X₀ ≃ FinWedge X₁
  FinWedge-emap-r = BigWedge-emap-r Xeq

  ⊙FinWedge-emap-r : ⊙FinWedge X₀ ⊙≃ ⊙FinWedge X₁
  ⊙FinWedge-emap-r = ⊙BigWedge-emap-r Xeq

module _ {i j} {I} {X : Ptd i} (<I : Fin I) where
  abstract
    fwproj-FinWedge-emap-r-lift :
        fwproj {X = ⊙Lift {j = j} X} <I ∘ –> (FinWedge-emap-r (λ _ → ⊙lift-equiv {j = j}))
      ∼ lift {j = j} ∘ fwproj {X = X} <I
    fwproj-FinWedge-emap-r-lift = bwproj-BigWedge-emap-r-lift Fin-has-dec-eq <I

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import FRP.JS.RSet using ( RSet ; ⟦_⟧ ; _⇒_ )
open import FRP.JS.Time using ( Time )

module FRP.JS.Product where

-- We define _∧_ directly, rather than as λ t → (A t × B t)
-- in order to make _∧_ invertable. (If we used the obvious defn,
-- (A ∧ B) would only be invertable if A and B were invertable.

infixr 2 _∧_
infixr 4 _,_

data _∧_ (A B : RSet) (t : Time) : Set where
  _,_ : A t → B t → (A ∧ B) t

proj₁ : ∀ {A B} → ⟦ A ∧ B ⇒ A ⟧
proj₁ (a , b) = a

proj₂ : ∀ {A B} → ⟦ A ∧ B ⇒ B ⟧
proj₂ (a , b) = b

swap : ∀ {A B} →  ⟦ A ∧ B ⇒ B ∧ A ⟧
swap (a , b) = (b , a)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
{-# OPTIONS --type-in-type #-}  -- yes, there will be some cheating in this lecture

module Lec4 where

open import Lec1Done
open import Lec2Done
open import Lec3Done

-- the identity functor (the identity action on objects and arrows)
ID : {C : Category} -> C => C
ID = id~> where open Category CATEGORY

-- composition of functors (composition of actions on objects and arrows)
_>F>_ : {C D E : Category} -> (C => D) -> (D => E) -> (C => E)
F >F> G = F >~> G where open Category CATEGORY

-- EXAMPLES

data Maybe (X : Set) : Set where
  yes : (x : X) -> Maybe X
  no  : Maybe X
{-# COMPILE GHC Maybe = data Maybe (Just | Nothing) #-}

maybe : {X Y : Set} -> (X -> Y) -> Maybe X -> Maybe Y
maybe f (yes x) = yes (f x)
maybe f no      = no

MAYBE : SET => SET
MAYBE = record
  { F-Obj = Maybe
  ; F-map = maybe
  ; F-map-id~> = extensionality \ { (yes x) -> refl (yes x) ; no -> refl no }
  -- extensionality \ { (yes x) -> refl (yes x) ; no -> refl no }
  ; F-map->~> = \ f g -> extensionality \ { (yes x) -> refl (yes (g (f x))) ; no -> refl no }
  }

module MAYBE-CAT where
  open Category SET
  open _=>_ MAYBE

{-
  unMaybe : {T : Set} -> Maybe T -> T
  unMaybe (yes t) = t
  unMaybe no = {!!}
-}

  joinMaybe : {T : Set} -> Maybe (Maybe T) -> Maybe T
  joinMaybe (yes mt) = mt
  joinMaybe no = no

  MAYBE-CAT : Category
  MAYBE-CAT = record
                { Obj = Set
                ; _~>_ = \ S T -> S -> Maybe T
                ; id~> = yes
                ; _>~>_ = \ f g -> f >> (F-map g >> joinMaybe)
                ; law-id~>>~> = \ f -> refl f
                ; law->~>id~> = \ f -> extensionality \ x -> help f x
                ; law->~>>~> = \ f g h -> extensionality \ x -> yelp f g h x
                } where
                help : forall {S T} (f : S -> Maybe T)
                  (x : S) ->
                  joinMaybe (maybe yes (f x)) == f x
                help f x with f x
                help f x | yes y = refl (yes y)
                help f x | no = refl no
                yelp : forall {Q R S T}
                  (f : Q -> Maybe R) (g : R -> Maybe S)(h : S -> Maybe T)
                  (x : Q) ->
                  joinMaybe (maybe h (joinMaybe (maybe g (f x)))) ==
                  joinMaybe
                    (maybe (\ y → joinMaybe (maybe h (g y))) (f x))
                yelp f g h x with f x
                yelp f g h x | yes y = refl (joinMaybe (maybe h (g y)))
                yelp f g h x | no = refl no

open MAYBE-CAT

module NATURAL-TRANSFORMATION {C D : Category} where
  open Category
  open _=>_

  record _~~>_ (F G : C => D) : Set where
    field
      -- one operation
      xf : {X : Obj C} -> _~>_ D (F-Obj F X) (F-Obj G X)
      -- one law
      naturality : {X Y : Obj C}(f : _~>_ C X Y) ->
                   _>~>_ D (F-map F f) (xf {Y})
                   ==
                   _>~>_ D (xf {X}) (F-map G f)

module FUNCTOR-CP {C D E : Category} where
  open _=>_
  open Category

  _>=>_ : C => D  ->  D => E  ->  C => E

  F-Obj (F >=> G) = F-Obj F >> F-Obj G

  F-map (F >=> G) = F-map F >> F-map G

  F-map-id~> (F >=> G) =
    F-map G (F-map F (id~> C))
      =[ refl (F-map G) =$= F-map-id~> F >=
    F-map G (id~> D)
      =[ F-map-id~> G >=
    id~> E
      [QED]

  F-map->~> (F >=> G) f g =
    F-map G (F-map F (_>~>_ C f g))
      =[ refl (F-map G) =$= F-map->~> F f g >=
    F-map G (_>~>_ D (F-map F f) (F-map F g))
      =[ F-map->~> G (F-map F f) (F-map F g) >=
    _>~>_ E (F-map G (F-map F f)) (F-map G (F-map F g))
      [QED]

open FUNCTOR-CP

open NATURAL-TRANSFORMATION public
open _~~>_ public

UNIT-MAYBE : ID ~~> MAYBE
xf UNIT-MAYBE = yes
naturality UNIT-MAYBE f = refl _

MULT-MAYBE : (MAYBE >=> MAYBE) ~~> MAYBE
MULT-MAYBE = record { xf = joinMaybe
  ; naturality = \ f -> extensionality \ {
       (yes x) → refl (maybe f x)
      ; no → refl no } }

module MONAD {C : Category}(M : C => C) where
  open Category C
  open _=>_ M

  record Monad : Set where
    field
      unit :        ID ~~> M
      mult : (M >=> M) ~~> M

      unitMult : {X : Obj} -> (xf unit >~> xf mult) == id~> {F-Obj X}
      multUnit : {X : Obj} -> (F-map (xf unit) >~> xf mult) == id~> {F-Obj X}
      multMult : {X : Obj} -> (xf mult >~> xf mult) == (F-map (xf mult) >~> xf mult {X})

    KLEISLI : Category
    KLEISLI = record
      { Obj = Obj
      ; _~>_ = \ S T -> S ~> F-Obj T

      ; id~>  = xf unit
      ; _>~>_ = \ f g -> f >~> F-map g >~> xf mult

      ; law-id~>>~> = \ f ->
        xf unit >~> F-map f >~> xf mult
          =< law->~>>~> _ _ _ ]=
        (xf unit >~> F-map f) >~> xf mult
          =< refl (_>~> xf mult) =$= naturality unit f ]=
        (f >~> xf unit) >~> xf mult
          =[ law->~>>~> _ _ _ >=
        f >~> (xf unit >~> xf mult)

          =[ refl (f >~>_) =$= unitMult >=

        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]

      ; law->~>id~> = \ f ->
        f >~> (F-map (xf unit) >~> xf mult)

          =[ refl (f >~>_) =$= multUnit >=

        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]

      ; law->~>>~> = \ f g h ->
        (f >~> F-map g >~> xf mult) >~> F-map h >~> xf mult
          =[ law->~>>~> _ _ _ >=
        f >~> (F-map g >~> xf mult) >~> (F-map h >~> xf mult)
          =[ refl (\ x -> _ >~> x) =$= law->~>>~> _ _ _ >=
        f >~> F-map g >~> xf mult >~> F-map h >~> xf mult
          =< refl (\ x -> _ >~> _ >~> x) =$= assocn (naturality mult _) ]=
        f >~> F-map g >~> F-map (F-map h) >~> xf mult >~> xf mult

          =[ refl (\ x -> _ >~> _ >~> _ >~> x) =$= multMult >=

        f >~> F-map g >~> F-map (F-map h) >~> F-map (xf mult) >~> xf mult
          =< refl (\ x -> _ >~> _ >~> x) =$= law->~>>~> _ _ _ ]=
        f >~> F-map g >~> (F-map (F-map h) >~> F-map (xf mult)) >~> xf mult
          =< refl (\ x -> _ >~> _ >~> x >~> _) =$= F-map->~> _ _ ]=
        f >~> F-map g >~> F-map (F-map h >~> xf mult) >~> xf mult
          =< refl (\ x -> _ >~> x) =$= law->~>>~> _ _ _ ]=
        f >~> (F-map g >~> F-map (F-map h >~> xf mult)) >~> xf mult
          =< refl (\ x -> _ >~> x >~> _) =$= F-map->~> _ _ ]=
        f >~> F-map (g >~> F-map h >~> xf mult) >~> xf mult
          [QED]
      }

open MONAD public

MAYBE-Monad : Monad MAYBE
MAYBE-Monad = record
  { unit = UNIT-MAYBE
  ; mult = MULT-MAYBE
  ; unitMult = refl _
  ; multUnit = extensionality \ { (yes x) -> refl _ ; no -> refl _ }
  ; multMult = extensionality \ { (yes mmx) -> refl _ ; no -> refl _ }
  }

data List (X : Set) : Set where
  []   : List X
  _,-_ : (x : X)(xs : List X) -> List X
{-# COMPILE GHC List = data [] ([] | (:)) #-}

list : {X Y : Set} -> (X -> Y) -> List X -> List Y
list f []         = []
list f (x ,- xs)  = f x ,- list f xs

LIST : SET => SET
LIST = record
  { F-Obj = List
  ; F-map = list
  ; F-map-id~> = extensionality listId
  ; F-map->~> = \ f g -> extensionality (listCp f g)
  } where
  open Category SET
  listId : {T : Set}(xs : List T) -> list id xs == xs
  listId []        = refl []
  listId (x ,- xs) = refl (_,-_ x) =$= listId xs
  listCp : {R S T : Set} (f : R -> S) (g : S -> T) (xs : List R) →
           list (f >~> g) xs == (list f >~> list g) xs
  listCp f g [] = refl []
  listCp f g (x ,- xs) = refl (_,-_ (g (f x))) =$= listCp f g xs

data Two : Set where tt ff : Two
{- BUILTIN BOOL Two -}
{- BUILTIN FALSE ff -}
{- BUILTIN TRUE tt -}
{-# COMPILE GHC Two = data Bool (True | False) #-}

data BitProcess (X : Set) : Set where  -- in what way is X used?
  stop : (x : X) -> BitProcess X                       -- stop with value x
  send : (b : Two)(k : BitProcess X) -> BitProcess X   -- send b, continue as k
  recv : (kt kf : BitProcess X) -> BitProcess X        -- receive bit, continue as
                                                       --   kt if tt, kf if ff

{-(-}
send1 : (b : Two) -> BitProcess One
send1 b = send b (stop <>)
{-)-}

{-(-}
recv1 : BitProcess Two
recv1 = recv (stop tt) (stop ff)
{-)-}

{-(-}
bpRun : forall {X} ->  BitProcess X   -- a process to run
                   ->  List Two       -- a list of bits waiting to be input
                   ->  List Two       -- the list of bits output
                    *  Maybe          -- and, if we don't run out of input
                       (  X           -- the resulting value
                       *  List Two    -- and the unused input
                       )
bpRun (stop x) bs = [] , yes (x , bs)
bpRun (send b px) bs = let os , mz = bpRun px bs in (b ,- os) , mz
bpRun (recv pxt pxf) [] = [] , no
bpRun (recv pxt pxf) (tt ,- bs) = bpRun pxt bs
bpRun (recv pxt pxf) (ff ,- bs) = bpRun pxf bs
{-)-}

example = bpRun recv1 (tt ,- [])

bitProcess : {X Y : Set} -> (X -> Y) -> BitProcess X -> BitProcess Y
bitProcess f (stop x) = stop (f x)
bitProcess f (send b k) = send b (bitProcess f k)
bitProcess f (recv kt kf) = recv (bitProcess f kt) (bitProcess f kf)

BITPROCESS : SET => SET  -- actions on *values* lift to processes
BITPROCESS = record
  { F-Obj = BitProcess
  ; F-map = bitProcess
  ; F-map-id~> = extensionality helpId
  ; F-map->~> = \ f g -> extensionality (helpCp f g)
  } where
  open Category SET
  helpId : {T : Set} (p : BitProcess T) -> bitProcess id p == p
  helpId (stop x) = refl (stop x)
  helpId (send b k) rewrite helpId k = refl (send b k)
  helpId (recv kt kf) rewrite helpId kt | helpId kf = refl (recv kt kf)
  helpCp : {R S T : Set} (f : R -> S)(g : S -> T) (p : BitProcess R) ->
         bitProcess (f >~> g) p == (bitProcess f >~> bitProcess g) p
  helpCp f g (stop x) = refl (stop (g (f x)))
  helpCp f g (send b k) rewrite helpCp f g k = refl (send b (bitProcess g (bitProcess f k)))
  helpCp f g (recv kt kf) rewrite helpCp f g kt | helpCp f g kf
    = refl (recv (bitProcess g (bitProcess f kt)) (bitProcess g (bitProcess f kf)))

{-(-}
UNIT-BP : ID ~~> BITPROCESS
UNIT-BP = record { xf = stop
                 ; naturality = \ f -> refl _
                 }
{-)-}

join-BP : {X : Set} -> BitProcess (BitProcess X) -> BitProcess X
join-BP (stop px) = px
join-BP (send b ppx) = send b (join-BP ppx)
join-BP (recv ppxt ppxf) = recv (join-BP ppxt) (join-BP ppxf)

{-(-}
MULT-BP : (BITPROCESS >=> BITPROCESS) ~~> BITPROCESS
MULT-BP = record
  { xf = join-BP
  ; naturality = \ f -> extensionality (help f )
  } where
  help : ∀ {X Y} (f : X → Y) (x : BitProcess (BitProcess X)) →
       join-BP (bitProcess (bitProcess f) x) == bitProcess f (join-BP x)
  help f (stop x) = refl (bitProcess f x)
  help f (send b p) rewrite help f p
    = refl (send b (bitProcess f (join-BP p)))
  help f (recv pt pf) rewrite help f pf | help f pt
    = refl (recv (bitProcess f (join-BP pt)) (bitProcess f (join-BP pf)))
{-)-}

{-(-}
BITPROCESS-Monad : Monad BITPROCESS
BITPROCESS-Monad = record
  { unit = UNIT-BP
  ; mult = MULT-BP
  ; unitMult = refl id
  ; multUnit = extensionality help
  ; multMult = extensionality yelp
  } where

  help : ∀ {X} (x : BitProcess X) → join-BP (bitProcess stop x) == x
  help (stop x) = refl (stop x)
  help (send b p)  rewrite help p = refl (send b p)
  help (recv pt pf) rewrite help pt | help pf = refl (recv pt pf)

  yelp : ∀ {X} (x : BitProcess (BitProcess (BitProcess X))) →
       join-BP (join-BP x) == join-BP (bitProcess join-BP x)
  yelp (stop x) = refl _
  yelp (send b p)  rewrite yelp p = refl _
  yelp (recv pt pf) rewrite yelp pt | yelp pf = refl _

{-)-}

module BIND {F : SET => SET}(M : Monad F) where

  open _=>_ F public
  open Monad M public
  open Category KLEISLI public

  {-(-}
  _>>=_ : {S T : Set} -> F-Obj S -> (S -> F-Obj T) -> F-Obj T
  fs >>= k = (id >~> k) fs
  {-)-}

open BIND BITPROCESS-Monad

bpEcho : BitProcess One
bpEcho = recv1 >>= \ b ->
         send1 b

BP-SEM : Set -> Set
BP-SEM X = List Two       -- a list of bits waiting to be input
           ->  List Two       -- the list of bits output
           *  Maybe          -- and, if we don't run out of input
           (  X           -- the resulting value
           *  List Two    -- and the unused input
           )

record _**_ (S T : Set) : Set where
  constructor _,_
  field
    outl : S
    outr : T
open _**_
{-# COMPILE GHC _**_ = data (,) ((,)) #-}
infixr 4 _**_ _,_

postulate       -- Haskell has a monad for doing IO, which we use at the top level
  IO        : Set -> Set
  mainLoop  : {S : Set} -> S -> (S -> Two -> (List Two ** Maybe S)) -> IO One
  mainOutIn : {S : Set} -> S -> (S -> (List Two ** Maybe (Two -> S))) -> IO One

{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}
{-# COMPILE GHC mainLoop = (\ _ -> Lec4HS.mainLoop) #-}
{-# COMPILE GHC mainOutIn = (\ _ -> Lec4HS.mainOutIn) #-}
{-# FOREIGN GHC import qualified Lec4HS #-}

STATE : Set
STATE = Two -> BitProcess One

step : STATE -> Two -> (List Two ** Maybe STATE)
step s b = go (s b)
  where
    go : BitProcess One → List Two ** Maybe (Two → BitProcess One)
    go (stop <>) = [] , no
    go (send b p) with go p
    ...              | bs , ms = (b ,- bs) , ms
    go (recv pt pf) = [] , yes \ { tt → pt ; ff → pf }

myState : STATE
myState tt = bpEcho >>= \ _ -> bpEcho
myState ff = bpEcho

{-
main : IO One
main = mainLoop myState step
-}

example2 = bpRun (myState ff) (tt ,- ff ,- [])

outIn : BitProcess One -> List Two ** Maybe (Two -> BitProcess One)
outIn (stop <>) = [] , no
outIn (send b p) with outIn p
... | os , mk = (b ,- os) , mk
outIn (recv pt pf) = [] , yes \ { tt → pt ; ff → pf }

main : IO One
main = mainOutIn (send1 ff >>= \ _ -> bpEcho >>= \ _ -> bpEcho) outIn

_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> (I -> Set)
(S -:> T) i = S i -> T i

[_] : {I : Set} -> (I -> Set) -> Set
[ P ] = forall i -> P i    -- [_] {I} P = (i : I) -> P i

_->SET : Set -> Category
I ->SET = record
  { Obj    = I -> Set                 -- I-indexed sets
  ; _~>_   = \ S T -> [ S -:> T ]     -- index-respecting functions
  ; id~>   = \ i -> id                -- the identity at every index
  ; _>~>_  = \ f g i -> f i >> g i    -- composition at every index
  ; law-id~>>~> = refl                -- and the laws are very boring
  ; law->~>id~> = refl
  ; law->~>>~>  = \ f g h -> refl _
  }

All : {X : Set} -> (X -> Set) -> (List X -> Set)
All P [] = One
All P (x ,- xs) = P x * All P xs

example3 : All (Vec Two) (1 ,- 2 ,- 3 ,- [])
example3 = (tt ,- [])
         , (tt ,- ff ,- [])
         , (tt ,- ff ,- tt ,- [])
         , <>

record _|>_ (I O : Set) : Set where
  field
    Cuts   : O -> Set                      -- given o : O, how may we cut it?
    inners : {o : O} -> Cuts o -> List I   -- given how we cut it, what are
                                           --   the shapes of its pieces?

-- Let us have some examples right away!

copy : Nat -> List One
copy zero = []
copy (suc n) = <> ,- copy n

VecCut : One |> Nat              -- cut numbers into boring pieces
VecCut = record
  { Cuts = \ n -> One            -- there is one way to cut n
  ; inners = \ {n} _ -> copy n   -- and you get n pieces
  }

-- Here's a less boring example. You can cut a number into *two* pieces
-- by finding two numbers that add to it.

NatCut : Nat |> Nat
NatCut = record
  { Cuts = \ mn -> Sg Nat \ m -> Sg Nat \ n -> (m +N n) == mn
  ; inners = \ { (m , n , _) -> m ,- n ,- [] }
  }

-- The point is that we can make data structures that record how we
-- built an O-shaped thing from I-shaped pieces.

record Cutting {I O}(C : I |> O)(P : I -> Set)(o : O) : Set where
  constructor _8><_               -- "scissors"
  open _|>_ C
  field
    cut     : Cuts o              -- we decide how to cut o
    pieces  : All P (inners cut)  -- then we give all the pieces.
infixr 3 _8><_

example4 : Cutting NatCut (Vec Two) 5
example4 = (3 , 2 , refl 5) 8>< ((tt ,- tt ,- tt ,- []) , (ff ,- ff ,- []) , <>)

data Interior {I}(C : I |> I)(T : I -> Set)(i : I) : Set where
                                         -- either...
  tile : T i -> Interior C T i           -- we have a tile that fits, or...
  <_>  : Cutting C (Interior C T) i ->   -- ...we cut, then tile the pieces.
         Interior C T i

MayC : One |> One
MayC = record { Cuts = \ _ -> One ; inners = \ _ -> [] }

Maybe' : Set -> Set
Maybe' X = Interior MayC (\ _ -> X) <>

yes' : {X : Set} -> X -> Maybe' X
yes' x = tile x

no' : {X : Set} -> Maybe' X
no' = < <> 8>< <> >

BPC : One |> One
BPC = record { Cuts = \ _ -> Two + One
             ; inners = \ { (inl x) → <> ,- []
                          ; (inr x) → <> ,- <> ,- []
                          }
             }

data Type : Set where nat two : Type

Val : Type -> Set
Val nat = Nat
Val two = Two

data Op : Type -> Set where
  val : {T : Type} -> Val T -> Op T
  add : Op nat
  if : {T : Type} -> Op T

Syntax : Type |> Type
_|>_.Cuts Syntax T = Op T
_|>_.inners Syntax {T} (val x) = []
_|>_.inners Syntax {.nat} add = nat ,- nat ,- []
_|>_.inners Syntax {T} if = two ,- T ,- T ,- []

eval : {T : Type}{X : Type -> Set} -> Interior Syntax X T ->
       ({T : Type} -> X T -> Val T) -> Val T
eval (tile x) g = g x
eval < val v 8>< <> > g = v
eval < add 8>< e1 , e2 , <> > g = eval e1 g +N eval e2 g
eval < if 8>< e1 , e2 , e3 , <> > g with eval e1 g
eval < if 8>< e1 , e2 , e3 , <> > g | tt = eval e2 g
eval < if 8>< e1 , e2 , e3 , <> > g | ff = eval e3 g

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
------------------------------------------------------------------------
-- Code for converting Vec n A → B to and from n-ary functions
------------------------------------------------------------------------

module Data.Vec.N-ary where

open import Data.Nat
open import Data.Vec
open import Data.Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- N-ary functions

N-ary : ℕ → Set → Set → Set
N-ary zero    A B = B
N-ary (suc n) A B = A → N-ary n A B

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

curryⁿ : ∀ {n A B} → (Vec A n → B) → N-ary n A B
curryⁿ {zero}  f = f []
curryⁿ {suc n} f = λ x → curryⁿ (f ∘ _∷_ x)

_$ⁿ_ : ∀ {n A B} → N-ary n A B → (Vec A n → B)
f $ⁿ []       = f
f $ⁿ (x ∷ xs) = f x $ⁿ xs

------------------------------------------------------------------------
-- N-ary function equality

Eq : ∀ {A B} n → Rel B → (f g : N-ary n A B) → Set
Eq zero    _∼_ f g = f ∼ g
Eq (suc n) _∼_ f g = ∀ x → Eq n _∼_ (f x) (g x)

-- A variant where all the arguments are implicit (hidden).

Eqʰ : ∀ {A B} n → Rel B → (f g : N-ary n A B) → Set
Eqʰ zero    _∼_ f g = f ∼ g
Eqʰ (suc n) _∼_ f g = ∀ {x} → Eqʰ n _∼_ (f x) (g x)

------------------------------------------------------------------------
-- Some lemmas

-- The functions curryⁿ and _$ⁿ_ are inverses.

left-inverse : ∀ {n A B} (f : Vec A n → B) →
               ∀ xs → curryⁿ f $ⁿ xs ≡ f xs
left-inverse f []       = refl
left-inverse f (x ∷ xs) = left-inverse (f ∘ _∷_ x) xs

right-inverse : ∀ {A B} n (f : N-ary n A B) →
                Eq n _≡_ (curryⁿ (_$ⁿ_ {n} f)) f
right-inverse zero    f = refl
right-inverse (suc n) f = λ x → right-inverse n (f x)

-- Conversion preserves equality.

curryⁿ-pres : ∀ {n A B _∼_} (f g : Vec A n → B) →
              (∀ xs → f xs ∼ g xs) →
              Eq n _∼_ (curryⁿ f) (curryⁿ g)
curryⁿ-pres {zero}  f g hyp = hyp []
curryⁿ-pres {suc n} f g hyp = λ x →
  curryⁿ-pres (f ∘ _∷_ x) (g ∘ _∷_ x) (λ xs → hyp (x ∷ xs))

curryⁿ-pres⁻¹ : ∀ {n A B _∼_} (f g : Vec A n → B) →
                Eq n _∼_ (curryⁿ f) (curryⁿ g) →
                ∀ xs → f xs ∼ g xs
curryⁿ-pres⁻¹ f g hyp []       = hyp
curryⁿ-pres⁻¹ f g hyp (x ∷ xs) =
  curryⁿ-pres⁻¹ (f ∘ _∷_ x) (g ∘ _∷_ x) (hyp x) xs

appⁿ-pres : ∀ {n A B _∼_} (f g : N-ary n A B) →
            Eq n _∼_ f g →
            (xs : Vec A n) → (f $ⁿ xs) ∼ (g $ⁿ xs)
appⁿ-pres f g hyp []       = hyp
appⁿ-pres f g hyp (x ∷ xs) = appⁿ-pres (f x) (g x) (hyp x) xs

appⁿ-pres⁻¹ : ∀ {n A B _∼_} (f g : N-ary n A B) →
              ((xs : Vec A n) → (f $ⁿ xs) ∼ (g $ⁿ xs)) →
              Eq n _∼_ f g
appⁿ-pres⁻¹ {zero}  f g hyp = hyp []
appⁿ-pres⁻¹ {suc n} f g hyp = λ x →
  appⁿ-pres⁻¹ (f x) (g x) (λ xs → hyp (x ∷ xs))

-- Eq and Eqʰ are equivalent.

Eq-to-Eqʰ : ∀ {A B} n {_∼_ : Rel B} {f g : N-ary n A B} →
            Eq n _∼_ f g → Eqʰ n _∼_ f g
Eq-to-Eqʰ zero    eq = eq
Eq-to-Eqʰ (suc n) eq = Eq-to-Eqʰ n (eq _)

Eqʰ-to-Eq : ∀ {A B} n {_∼_ : Rel B} {f g : N-ary n A B} →
            Eqʰ n _∼_ f g → Eq n _∼_ f g
Eqʰ-to-Eq zero    eq = eq
Eqʰ-to-Eq (suc n) eq = λ _ → Eqʰ-to-Eq n eq

max_issues_repo_name: larrytheliquid/Lemmachine