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

import      LibraBFT.Impl.Types.CryptoProxies              as CryptoProxies
import      LibraBFT.Impl.Types.LedgerInfo                 as LedgerInfo
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures   as LedgerInfoWithSignatures
import      LibraBFT.Impl.Types.ValidatorSigner            as ValidatorSigner
import      LibraBFT.Impl.Types.ValidatorVerifier          as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.OBM.Genesis where

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

obmMkLedgerInfoWithEpochState : ValidatorSet → Either ErrLog LedgerInfo

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

obmMkGenesisLedgerInfoWithSignatures
  : List ValidatorSigner → ValidatorSet → Either ErrLog LedgerInfoWithSignatures
obmMkGenesisLedgerInfoWithSignatures vss0 vs0 = do
  liwes    ← obmMkLedgerInfoWithEpochState vs0
  let sigs = fmap (λ vs → (vs ^∙ vsAuthor , ValidatorSigner.sign vs liwes)) vss0
  pure $ foldl' (λ acc (a , sig) → CryptoProxies.addToLi a sig acc)
                (LedgerInfoWithSignatures.obmNewNoSigs liwes)
                sigs

obmMkLedgerInfoWithEpochState vs = do
  li ← LedgerInfo.mockGenesis (just vs)
  vv ← ValidatorVerifier.from-e-abs vs
  pure (li
         & liCommitInfo ∙ biNextEpochState
        ?~ EpochState∙new (li ^∙ liEpoch) vv)


text:
module PreludeInt where
open import AlonzoPrelude
import RTP

int : Nat -> Int
int = RTP.primNatToInt

_+_ : Int -> Int -> Int
_+_ = RTP.primIntAdd

_-_ : Int -> Int -> Int
_-_ = RTP.primIntSub

_*_ : Int -> Int -> Int
_*_ = RTP.primIntMul

div : Int -> Int -> Int
div = RTP.primIntDiv

mod : Int -> Int -> Int
mod = RTP.primIntMod

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Some theory of equivalences with erased "proofs", defined in terms
-- of partly erased contractible fibres, developed using Cubical Agda
------------------------------------------------------------------------

-- This module instantiates and reexports code from
-- Equivalence.Erased.Contractible-preimages.

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

import Equality.Path as P

module Equivalence.Erased.Contractible-preimages.Cubical
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Erased.Cubical eq

import Equivalence.Erased.Contractible-preimages
open Equivalence.Erased.Contractible-preimages equality-with-J public
  hiding (module []-cong)
open Equivalence.Erased.Contractible-preimages.[]-cong
  equality-with-J instance-of-[]-cong-axiomatisation
  public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Integer.Difference where

open import Data.Product as Σ
open import Data.Product.Relation.Pointwise.NonDependent
open import Data.Unit
open import Equality
open import Natural as ℕ
open import Quotient as /
open import Relation.Binary
open import Syntax

infixl 6 _–_
pattern _–_ a b = _,_ a b

⟦ℤ⟧ = ℕ × ℕ
⟦ℤ²⟧ = ⟦ℤ⟧ × ⟦ℤ⟧

_≈_ : ⟦ℤ⟧ → ⟦ℤ⟧ → Set
(a – b) ≈ (c – d) = a + d ≡ c + b

≈-refl : ∀ {x} → x ≈ x
≈-refl = refl

ℤ = ⟦ℤ⟧ / _≈_
ℤ² = ⟦ℤ²⟧ / Pointwise _≈_ _≈_

instance
  ⟦ℤ⟧-Number : Number ⟦ℤ⟧
  ⟦ℤ⟧-Number = record { Constraint = λ _ → ⊤ ; fromNat = λ x → x – 0 }

  ℤ-Number : Number ℤ
  ℤ-Number = record { Constraint = λ _ → ⊤ ; fromNat = λ x → ⟦ fromNat x ⟧ }

  ⟦ℤ⟧-Negative : Negative ⟦ℤ⟧
  ⟦ℤ⟧-Negative = record { Constraint = λ _ → ⊤ ; fromNeg = λ x → 0 – x }

  ℤ-Negative : Negative ℤ
  ℤ-Negative = record { Constraint = λ _ → ⊤ ; fromNeg = λ x → ⟦ fromNeg x ⟧ }

suc–suc-injective : ∀ a b → Path ℤ ⟦ suc a – suc b ⟧ ⟦ a – b ⟧
suc–suc-injective a b = equiv (suc a – suc b) (a – b) (sym (+-suc a b ))

⟦negate⟧ : ⟦ℤ⟧ → ⟦ℤ⟧
⟦negate⟧ (a – b) = b – a

negate : ℤ → ℤ
negate =
  ⟦negate⟧ // λ where
    (a – b) (c – d) p →
      ⟨ +-comm b c ⟩ ≫ sym p ≫ ⟨ +-comm a d ⟩

⟦plus⟧ : ⟦ℤ²⟧ → ⟦ℤ⟧
⟦plus⟧ ((a – b) , (c – d)) = (a + c) – (d + b)

plus : ℤ² → ℤ
plus =
  ⟦plus⟧ // λ where
    ((a – b) , (c – d)) ((e – f) , (g – h)) (p , q) →
        (a + c) + (h + f)
      ≡⟨ sym (ℕ.+-assoc a _ _) ⟩
        a + (c + (h + f))
      ≡⟨ cong (a +_) (ℕ.+-assoc c _ _) ⟩
        a + ((c + h) + f)
      ≡⟨ cong (λ z → a + (z + f)) q ⟩
        a + ((g + d) + f)
      ≡⟨ cong (a +_) ⟨ ℕ.+-comm (g + d) _ ⟩ ⟩
        a + (f + (g + d))
      ≡⟨ ℕ.+-assoc a _ _ ⟩
        (a + f) + (g + d)
      ≡⟨ cong (_+ (g + d)) p ⟩
        (e + b) + (g + d)
      ≡⟨ ℕ.+-cross e _ _ _ ⟩
        (e + g) + (b + d)
      ≡⟨ cong ((e + g) +_) ⟨ ℕ.+-comm b _ ⟩ ⟩
        (e + g) + (d + b)
      ∎

instance
  ⟦ℤ⟧-plus-syntax : plus-syntax-simple ⟦ℤ⟧ ⟦ℤ⟧ ⟦ℤ⟧
  ⟦ℤ⟧-plus-syntax = λ where ._+_ x y → ⟦plus⟧ (x , y)

  ⟦ℤ⟧-minus-syntax : minus-syntax-simple ⟦ℤ⟧ ⟦ℤ⟧ ⟦ℤ⟧
  ⟦ℤ⟧-minus-syntax = λ where ._-_ x y → ⟦plus⟧ (x , ⟦negate⟧ y)

  ℕ-⟦ℤ⟧-minus-syntax : minus-syntax-simple ℕ ℕ ⟦ℤ⟧
  ℕ-⟦ℤ⟧-minus-syntax = λ where ._-_ → _–_

  ℤ-plus-syntax : plus-syntax-simple ℤ ℤ ℤ
  ℤ-plus-syntax = λ where ._+_ → /.uncurry refl refl plus

  ℤ-minus-syntax : minus-syntax-simple ℤ ℤ ℤ
  ℤ-minus-syntax = λ where ._-_ x y → x + negate y

  ℕ-ℤ-minus-syntax : minus-syntax-simple ℕ ℕ ℤ
  ℕ-ℤ-minus-syntax = λ where ._-_ x y → ⟦ x – y ⟧


text:
module MissingTypeSignature where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

pred zero    = zero
pred (suc n) = n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module ProofUtilities where

-- open import Data.Nat hiding (_>_)

open import StdLibStuff

open import Syntax
open import FSC

mutual
 hn-left-i : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α β : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t α) (F : Form Γ-t β) (G : Form Γ-t α) → Γ ⊢ α ∋ S (headNorm m F) ↔ G → Γ ⊢ α ∋ S F ↔ G
 hn-left-i m S (app F H) G p = hn-left-i m (λ x → S (app x H)) F G (hn-left-i' m S (headNorm m F) H G p)
 hn-left-i _ _ (var _ _) _ p = p
 hn-left-i _ _ N _ p = p
 hn-left-i _ _ A _ p = p
 hn-left-i _ _ Π _ p = p
 hn-left-i _ _ i _ p = p
 hn-left-i _ _ (lam _ _) _ p = p

 hn-left-i' : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α β γ : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t α) (F : Form Γ-t (γ > β)) (H : Form Γ-t γ) (G : Form Γ-t α) → Γ ⊢ α ∋ S (headNorm' m F H) ↔ G → Γ ⊢ α ∋ S (app F H) ↔ G
 hn-left-i' (suc m) S (lam _ F) H G p with hn-left-i m S (sub H F) G p
 hn-left-i' (suc _) S (lam _ _) _ _ _ |    p' = reduce-l {_} {_} {_} {_} {_} {_} {S} p'
 hn-left-i' 0 _ (lam _ _) _ _ p = p
 hn-left-i' zero _ (var _ _) _ _ p = p
 hn-left-i' (suc _) _ (var _ _) _ _ p = p
 hn-left-i' zero _ N _ _ p = p
 hn-left-i' (suc _) _ N _ _ p = p
 hn-left-i' zero _ A _ _ p = p
 hn-left-i' (suc _) _ A _ _ p = p
 hn-left-i' zero _ Π _ _ p = p
 hn-left-i' (suc _) _ Π _ _ p = p
 hn-left-i' zero _ i _ _ p = p
 hn-left-i' (suc _) _ i _ _ p = p
 hn-left-i' zero _ (app _ _) _ _ p = p
 hn-left-i' (suc _) _ (app _ _) _ _ p = p

hn-left : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α : Type n} (m : ℕ) (F : Form Γ-t α) (G : Form Γ-t α) → Γ ⊢ α ∋ headNorm m F ↔ G → Γ ⊢ α ∋ F ↔ G
hn-left m F G p = hn-left-i m (λ x → x) F G p

mutual
 hn-right-i : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α β : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t α) (F : Form Γ-t β) (G : Form Γ-t α) → Γ ⊢ α ∋ G ↔ S (headNorm m F) → Γ ⊢ α ∋ G ↔ S F
 hn-right-i m S (app F H) G p = hn-right-i m (λ x → S (app x H)) F G (hn-right-i' m S (headNorm m F) H G p)
 hn-right-i _ _ (var _ _) _ p = p
 hn-right-i _ _ N _ p = p
 hn-right-i _ _ A _ p = p
 hn-right-i _ _ Π _ p = p
 hn-right-i _ _ i _ p = p
 hn-right-i _ _ (lam _ _) _ p = p

 hn-right-i' : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α β γ : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t α) (F : Form Γ-t (γ > β)) (H : Form Γ-t γ) (G : Form Γ-t α) → Γ ⊢ α ∋ G ↔ S (headNorm' m F H) → Γ ⊢ α ∋ G ↔ S (app F H)
 hn-right-i' (suc m) S (lam _ F) H G p with hn-right-i m S (sub H F) G p
 hn-right-i' (suc _) S (lam _ _) _ _ _ |    p' = reduce-r {_} {_} {_} {_} {_} {_} {S} p'
 hn-right-i' 0 _ (lam _ _) _ _ p = p
 hn-right-i' zero _ (var _ _) _ _ p = p
 hn-right-i' (suc _) _ (var _ _) _ _ p = p
 hn-right-i' zero _ N _ _ p = p
 hn-right-i' (suc _) _ N _ _ p = p
 hn-right-i' zero _ A _ _ p = p
 hn-right-i' (suc _) _ A _ _ p = p
 hn-right-i' zero _ Π _ _ p = p
 hn-right-i' (suc _) _ Π _ _ p = p
 hn-right-i' zero _ i _ _ p = p
 hn-right-i' (suc _) _ i _ _ p = p
 hn-right-i' zero _ (app _ _) _ _ p = p
 hn-right-i' (suc _) _ (app _ _) _ _ p = p

hn-right : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α : Type n} (m : ℕ) (F : Form Γ-t α) (G : Form Γ-t α) → Γ ⊢ α ∋ G ↔ headNorm m F → Γ ⊢ α ∋ G ↔ F
hn-right m F G p = hn-right-i m (λ x → x) F G p

mutual
 hn-succ-i : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {β : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t $o) (F : Form Γ-t β) → Γ ⊢ S (headNorm m F) → Γ ⊢ S F
 hn-succ-i m S (app F H) p = hn-succ-i m (λ x → S (app x H)) F (hn-succ-i' m S (headNorm m F) H p)
 hn-succ-i _ _ (var _ _) p = p
 hn-succ-i _ _ N p = p
 hn-succ-i _ _ A p = p
 hn-succ-i _ _ Π p = p
 hn-succ-i _ _ i p = p
 hn-succ-i _ _ (lam _ _) p = p

 hn-succ-i' : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {β γ : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t $o) (F : Form Γ-t (γ > β)) (H : Form Γ-t γ) → Γ ⊢ S (headNorm' m F H) → Γ ⊢ S (app F H)
 hn-succ-i' (suc m) S (lam _ F) H p with hn-succ-i m S (sub H F) p
 hn-succ-i' (suc _) S (lam _ _) _ _ |    p' = reduce {_} {_} {_} {_} {_} {S} p'
 hn-succ-i' 0 _ (lam _ _) _ p = p
 hn-succ-i' zero _ (var _ _) _ p = p
 hn-succ-i' (suc _) _ (var _ _) _ p = p
 hn-succ-i' zero _ N _ p = p
 hn-succ-i' (suc _) _ N _ p = p
 hn-succ-i' zero _ A _ p = p
 hn-succ-i' (suc _) _ A _ p = p
 hn-succ-i' zero _ Π _ p = p
 hn-succ-i' (suc _) _ Π _ p = p
 hn-succ-i' zero _ i _ p = p
 hn-succ-i' (suc _) _ i _ p = p
 hn-succ-i' zero _ (app _ _) _ p = p
 hn-succ-i' (suc _) _ (app _ _) _ p = p

hn-succ : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} (m : ℕ) (F : Form Γ-t $o) → Γ ⊢ headNorm m F → Γ ⊢ F
hn-succ m F p = hn-succ-i m (λ x → x) F p

mutual
 hn-ante-i : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {β : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t $o) (F : Form Γ-t β) (G : Form Γ-t $o) → Γ , S (headNorm m F) ⊢ G → Γ , S F ⊢ G
 hn-ante-i m S (app F H) G p = hn-ante-i m (λ x → S (app x H)) F G (hn-ante-i' m S (headNorm m F) H G p)
 hn-ante-i _ _ (var _ _) _ p = p
 hn-ante-i _ _ N _ p = p
 hn-ante-i _ _ A _ p = p
 hn-ante-i _ _ Π _ p = p
 hn-ante-i _ _ i _ p = p
 hn-ante-i _ _ (lam _ _) _ p = p

 hn-ante-i' : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {β γ : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t $o) (F : Form Γ-t (γ > β)) (H : Form Γ-t γ) (G : Form Γ-t $o) → Γ , S (headNorm' m F H) ⊢ G → Γ , S (app F H) ⊢ G
 hn-ante-i' (suc m) S (lam _ F) H G p with hn-ante-i m S (sub H F) G p
 hn-ante-i' (suc _) S (lam _ _) _ _ _ |    p' = reduce {_} {_} {_} {_} {_} {S} p'
 hn-ante-i' 0 _ (lam _ _) _ _ p = p
 hn-ante-i' zero _ (var _ _) _ _ p = p
 hn-ante-i' (suc _) _ (var _ _) _ _ p = p
 hn-ante-i' zero _ N _ _ p = p
 hn-ante-i' (suc _) _ N _ _ p = p
 hn-ante-i' zero _ A _ _ p = p
 hn-ante-i' (suc _) _ A _ _ p = p
 hn-ante-i' zero _ Π _ _ p = p
 hn-ante-i' (suc _) _ Π _ _ p = p
 hn-ante-i' zero _ i _ _ p = p
 hn-ante-i' (suc _) _ i _ _ p = p
 hn-ante-i' zero _ (app _ _) _ _ p = p
 hn-ante-i' (suc _) _ (app _ _) _ _ p = p

hn-ante : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} (m : ℕ) (F : Form Γ-t $o) (G : Form Γ-t $o) → Γ , headNorm m F ⊢ G → Γ , F ⊢ G
hn-ante m F G p = hn-ante-i m (λ x → x) F G p

mutual
 hn-ante-eq-i : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α β : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t $o) (F : Form Γ-t β) (G H : Form Γ-t α) → Γ , S (headNorm m F) ⊢ G == H → Γ , S F ⊢ G == H
 hn-ante-eq-i m S (app F I) G H p = hn-ante-eq-i m (λ x → S (app x I)) F G H (hn-ante-eq-i' m S (headNorm m F) I G H p)
 hn-ante-eq-i _ _ (var _ _) _ _ p = p
 hn-ante-eq-i _ _ N _ _ p = p
 hn-ante-eq-i _ _ A _ _ p = p
 hn-ante-eq-i _ _ Π _ _ p = p
 hn-ante-eq-i _ _ i _ _ p = p
 hn-ante-eq-i _ _ (lam _ _) _ _ p = p

 hn-ante-eq-i' : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α β γ : Type n} (m : ℕ) (S : Form Γ-t β → Form Γ-t $o) (F : Form Γ-t (γ > β)) (I : Form Γ-t γ) (G H : Form Γ-t α) → Γ , S (headNorm' m F I) ⊢ G == H → Γ , S (app F I) ⊢ G == H
 hn-ante-eq-i' (suc m) S (lam _ F) I G H p with hn-ante-eq-i m S (sub I F) G H p
 hn-ante-eq-i' (suc _) S (lam _ _) _ _ _ _ |    p' = reduce {_} {_} {_} {_} {_} {_} {S} p'
 hn-ante-eq-i' 0 _ (lam _ _) _ _ _ p = p
 hn-ante-eq-i' zero _ (var _ _) _ _ _ p = p
 hn-ante-eq-i' (suc _) _ (var _ _) _ _ _ p = p
 hn-ante-eq-i' zero _ N _ _ _ p = p
 hn-ante-eq-i' (suc _) _ N _ _ _ p = p
 hn-ante-eq-i' zero _ A _ _ _ p = p
 hn-ante-eq-i' (suc _) _ A _ _ _ p = p
 hn-ante-eq-i' zero _ Π _ _ _ p = p
 hn-ante-eq-i' (suc _) _ Π _ _ _ p = p
 hn-ante-eq-i' zero _ i _ _ _ p = p
 hn-ante-eq-i' (suc _) _ i _ _ _ p = p
 hn-ante-eq-i' zero _ (app _ _) _ _ _ p = p
 hn-ante-eq-i' (suc _) _ (app _ _) _ _ _ p = p

hn-ante-eq : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α : Type n} (m : ℕ) (F : Form Γ-t $o) (G H : Form Γ-t α) → Γ , headNorm m F ⊢ G == H → Γ , F ⊢ G == H
hn-ante-eq m F G H p = hn-ante-eq-i m (λ x → x) F G H p

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

head-& : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {F₁ F₂ G₁ G₂ : Form Γ-t $o} →
 Γ ⊢ $o ∋ F₁ == F₂ → Γ ⊢ $o ∋ G₁ == G₂ →
 Γ ⊢ $o ∋ (F₁ & G₁) ↔ (F₂ & G₂)
head-& p₁ p₂ = head-app _ _ _ _ _ _ (simp (head-const _ N)) (simp (head-app _ _ _ _ _ _ (simp (head-app _ _ _ _ _ _ (simp (head-const _ A)) (simp (head-app _ _ _ _ _ _ (simp (head-const _ N)) p₁)))) (simp (head-app _ _ _ _ _ _ (simp (head-const _ N)) p₂))))

head-|| : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {F₁ F₂ G₁ G₂ : Form Γ-t $o} →
 Γ ⊢ $o ∋ F₁ == F₂ → Γ ⊢ $o ∋ G₁ == G₂ →
 Γ ⊢ $o ∋ (F₁ || G₁) ↔ (F₂ || G₂)
head-|| p₁ p₂ = head-app _ _ _ _ _ _ (simp (head-app _ _ _ _ _ _ (simp (head-const _ A)) p₁)) p₂

head-=> : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {F₁ F₂ G₁ G₂ : Form Γ-t $o} →
 Γ ⊢ $o ∋ F₁ == F₂ → Γ ⊢ $o ∋ G₁ == G₂ →
 Γ ⊢ $o ∋ (F₁ => G₁) ↔ (F₂ => G₂)
head-=> p₁ p₂ = head-app _ _ _ _ _ _ (simp (head-app _ _ _ _ _ _ (simp (head-const _ A)) (simp (head-app _ _ _ _ _ _ (simp (head-const _ N)) p₁)))) p₂

head-~ : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {F₁ F₂ : Form Γ-t $o} →
 Γ ⊢ $o ∋ F₁ == F₂ →
 Γ ⊢ $o ∋ (~ F₁) ↔ (~ F₂)
head-~ p = head-app _ _ _ _ _ _ (simp (head-const _ N)) p

head-== : {n : ℕ} {Γ-t : Ctx n} {Γ : FSC-Ctx n Γ-t} {α : Type n} {F₁ F₂ G₁ G₂ : Form Γ-t α} →
 Γ ⊢ α ∋ F₁ == F₂ → Γ ⊢ α ∋ G₁ == G₂ →
 Γ ⊢ $o ∋ (F₁ == G₁) ↔ (F₂ == G₂)
head-== p₁ p₂ = head-app _ _ _ _ _ _ (simp (head-app _ _ _ _ _ _ (simp (head-const _ _)) p₁)) p₂

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Choice

module cohomology.Theory where

record CohomologyTheory i : Type (lsucc i) where
  field
    C : ℤ → Ptd i → Group i

  CEl : ℤ → Ptd i → Type i
  CEl n X = Group.El (C n X)

  Cid : (n : ℤ) (X : Ptd i) → CEl n X
  Cid n X = GroupStructure.ident (Group.group-struct (C n X))

  ⊙CEl : ℤ → Ptd i → Ptd i
  ⊙CEl n X = ⊙[ CEl n X , Cid n X ]

  field
    CF-hom : (n : ℤ) {X Y : Ptd i} → fst (X ⊙→ Y) → (C n Y →ᴳ C n X)

    CF-ident : (n : ℤ) {X : Ptd i}
      → CF-hom n {X} {X} (⊙idf X) == idhom (C n X)
    CF-comp : (n : ℤ) {X Y Z : Ptd i} (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
      → CF-hom n (g ⊙∘ f) == CF-hom n f ∘ᴳ CF-hom n g

  CF : (n : ℤ) {X Y : Ptd i} → fst (X ⊙→ Y) → fst (⊙CEl n Y ⊙→ ⊙CEl n X)
  CF n f = GroupHom.⊙f (CF-hom n f)

  field
    C-abelian : (n : ℤ) (X : Ptd i) → is-abelian (C n X)

    C-Susp : (n : ℤ) (X : Ptd i) → C (succ n) (⊙Susp X) == C n X

    C-exact : (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y))
      → is-exact (CF n (⊙cfcod f)) (CF n f)

    C-additive : (n : ℤ) {I : Type i} (Z : I → Ptd i)
      → ((W : I → Type i) → has-choice ⟨0⟩ I W)
      → C n (⊙BigWedge Z) == Πᴳ I (C n ∘ Z)

  {- A quick useful special case of C-additive:
     C n (X ∨ Y) == C n X × C n Y -}
  C-binary-additive : (n : ℤ) (X Y : Ptd i)
    → C n (X ⊙∨ Y) == C n X ×ᴳ C n Y
  C-binary-additive n X Y =
    ap (C n) (! (BigWedge-Bool-⊙path Pick))
    ∙ C-additive n _ (λ _ → Bool-has-choice)
    ∙ Πᴳ-Bool-is-×ᴳ (C n ∘ Pick)
    where
    Pick : Lift {j = i} Bool → Ptd i
    Pick (lift true) = X
    Pick (lift false) = Y

record OrdinaryTheory i : Type (lsucc i) where
  constructor ordinary-theory
  field
    cohomology-theory : CohomologyTheory i
  open CohomologyTheory cohomology-theory public
  field
    C-dimension : (n : ℤ) → n ≠ O → C n (⊙Sphere O) == 0ᴳ

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


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

module Relation.Nullary.Discrete.FromBoolean where

open import Prelude
open import Relation.Nullary.Discrete

module _ {a} {A : Type a}
             (_≡ᴮ_ : A → A → Bool)
             (sound : ∀ x y → T (x ≡ᴮ y) → x ≡ y)
             (complete : ∀ x → T (x ≡ᴮ x))
  where

  from-bool-eq : Discrete A
  from-bool-eq x y =
    iff-dec (sound x y iff flip (subst (λ z → T (x ≡ᴮ z))) (complete x)) (T? (x ≡ᴮ y))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module calculus-examples where

open import Data.List using (List ; _∷_ ; [] ; _++_)
open import Data.List.Any using (here ; there ; any)
open import Data.List.Any.Properties
open import Data.OrderedListMap
open import Data.Sum using (inj₁ ; inj₂ ; _⊎_)
open import Data.Maybe.Base
open import Data.Empty using (⊥ ; ⊥-elim)
open import Data.Bool.Base using (true ; false)
open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
open import Agda.Builtin.Equality using (refl ; _≡_)
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (subst ; cong ; sym ; trans)

open import calculus
open import utility

open import Esterel.Environment as Env
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ ; unknown ; present ; absent ; _≟ₛₜ_)
open import Esterel.Variable.Shared as SharedVar using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar using (SeqVar)

open import Esterel.Lang
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Properties
open import Esterel.Lang.CanFunction.SetSigMonotonic using (canₛ-set-sig-monotonic)
open import Esterel.Lang.Properties
open import Esterel.Lang.Binding
open import Esterel.Context
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import context-properties
open import Esterel.Lang.CanFunction.Base using (canₛ-⊆-FV)

open import Data.Nat as Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Nat.Properties.Simple
  using (+-comm)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_)

open import eval

{-

This example is not true (and not provable under the current calculus)

{- rewriting a present to the true branch -}
{- cannot prove without the `signal` form -}
ex1 : ∀ S p q -> CB p ->
    signl S (emit S >> (present S ∣⇒ p ∣⇒ q)) ≡ₑ
    signl S (emit S >> p) # []
ex1 S p q CBp = calc where

  θS→unk : Env
  θS→unk = Θ SigMap.[ S ↦ Signal.unknown ] [] []

  S∈θS→unk : SigMap.∈Dom S (sig θS→unk)
  S∈θS→unk = sig-∈-single S Signal.unknown

  θS→unk[S]≡unk : sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.unknown
  θS→unk[S]≡unk = sig-stats-1map' S Signal.unknown S∈θS→unk

  θS→pre : Env
  θS→pre = set-sig{S} θS→unk S∈θS→unk Signal.present

  S∈θS→pre : SigMap.∈Dom S (sig θS→pre)
  S∈θS→pre = sig-set-mono' {S} {S} {θS→unk} {Signal.present} {S∈θS→unk} S∈θS→unk

  θS→pre[S]≡pre : sig-stats{S = S} θS→pre S∈θS→pre ≡ Signal.present
  θS→pre[S]≡pre = sig-putget{S} {θS→unk} {Signal.present} S∈θS→unk S∈θS→pre

  θS→unk[S]≠absent : ¬ sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.absent
  θS→unk[S]≠absent is rewrite θS→unk[S]≡unk = unknotabs is where
    unknotabs : Signal.unknown ≡ Signal.absent → ⊥
    unknotabs ()

  CBsignalS[emitS>>p] : CB (signl S (emit S >> p))
  CBsignalS[emitS>>p]
   = CBsig (CBseq (CBemit{S}) CBp ((λ z → λ ()) , (λ z → λ ()) , (λ z → λ ())))

  calc : signl S (emit S >> (present S ∣⇒ p ∣⇒ q)) ≡ₑ
         signl S (emit S >> p) # []
  calc =
    ≡ₑtran {r = (ρ θS→unk · (emit S >> (present S ∣⇒ p ∣⇒ q)))}
           (≡ₑstep [raise-signal])
   (≡ₑtran {r = (ρ θS→pre · (nothin >> (present S ∣⇒ p ∣⇒ q)))}
           (≡ₑstep ([emit] S∈θS→unk θS→unk[S]≠absent (deseq dehole)))
   (≡ₑtran {r = (ρ θS→pre · (present S ∣⇒ p ∣⇒ q))}
           (≡ₑctxt (dcenv dchole) (dcenv dchole) (≡ₑstep [seq-done]))
   (≡ₑtran {r = (ρ θS→pre · p)}
           (≡ₑstep ([is-present] S S∈θS→pre θS→pre[S]≡pre dehole))
   (≡ₑsymm CBsignalS[emitS>>p]
           (≡ₑtran {r = (ρ θS→unk · (emit S >> p))}
                   (≡ₑstep [raise-signal])
           (≡ₑtran {r = (ρ θS→pre · (nothin >> p))}
                   (≡ₑstep ([emit] S∈θS→unk θS→unk[S]≠absent (deseq dehole)))
           (≡ₑtran {r = ρ θS→pre · p}
                   (≡ₑctxt (dcenv dchole) (dcenv dchole) (≡ₑstep [seq-done]))
           ≡ₑrefl)))))))
           -}

Canₛpresent-fact : ∀ S p q ->
  (Signal.unwrap S) ∈ Canₛ (present S ∣⇒ p ∣⇒ q) (Θ SigMap.[ S ↦ Signal.unknown ] [] []) ->
  (Signal.unwrap S ∈ Canₛ p (Θ SigMap.[ S ↦ Signal.unknown ] [] [])) ⊎
  (Signal.unwrap S ∈ Canₛ q (Θ SigMap.[ S ↦ Signal.unknown ] [] []))
Canₛpresent-fact S  p q S∈Canₛ[presentSpq]
  with Env.Sig∈ S (Θ SigMap.[ S ↦ Signal.unknown ] [] [])
Canₛpresent-fact S p q S∈Canₛ[presentSpq] | yes S∈
  with  ⌊ present ≟ₛₜ (Env.sig-stats{S} (Θ SigMap.[ S ↦ Signal.unknown ] [] []) S∈) ⌋
Canₛpresent-fact S p q S∈Canₛ[presentSpq] | yes S∈ | true
 = inj₁ S∈Canₛ[presentSpq]
Canₛpresent-fact S p q S∈Canₛ[presentSpq] | yes S∈ | false
  with ⌊ absent ≟ₛₜ Env.sig-stats{S} (Θ SigMap.[ S ↦ Signal.unknown ] [] []) S∈ ⌋
Canₛpresent-fact S p q S∈Canₛ[presentSpq] | yes S∈ | false | true
  = inj₂ S∈Canₛ[presentSpq]
Canₛpresent-fact S p q S∈Canₛ[presentSpq] | yes S∈ | false | false
  =  ++⁻ (Canₛ p (Θ SigMap.[ S ↦ Signal.unknown ] [] [])) S∈Canₛ[presentSpq]
Canₛpresent-fact S p q _ | no ¬p
  = ⊥-elim (¬p (SigMap.update-in-keys [] S unknown))

{- rewriting a present to the false branch -}
ex2b : ∀ S p q C -> CB (C ⟦ signl S q ⟧c) ->
   Signal.unwrap S ∉ (Canₛ p (Θ SigMap.[ S ↦ unknown ] [] [])) ->
   Signal.unwrap S ∉ (Canₛ q (Θ SigMap.[ S ↦ unknown ] [] [])) ->
   signl S (present S ∣⇒ p ∣⇒ q) ≡ₑ
   signl S q # C
ex2b S p q C CBq s∉Canₛp s∉Canₛq = calc where

 θS→unk : Env
 θS→unk = Θ SigMap.[ S ↦ Signal.unknown ] [] []

 S∈θS→unk : SigMap.∈Dom S (sig θS→unk)
 S∈θS→unk = sig-∈-single S Signal.unknown

 θS→unk[S]≡unk : sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.unknown
 θS→unk[S]≡unk = sig-stats-1map' S Signal.unknown S∈θS→unk

 θS→abs : Env
 θS→abs = set-sig{S} θS→unk S∈θS→unk Signal.absent

 S∈θS→abs : SigMap.∈Dom S (sig θS→abs)
 S∈θS→abs = sig-set-mono' {S} {S} {θS→unk} {Signal.absent} {S∈θS→unk} S∈θS→unk

 θS→abs[S]≡abs : sig-stats{S = S} θS→abs S∈θS→abs ≡ Signal.absent
 θS→abs[S]≡abs = sig-putget{S} {θS→unk} {Signal.absent} S∈θS→unk S∈θS→abs

 S∉Canθₛq : Signal.unwrap S ∉ Canθₛ SigMap.[ S ↦ unknown ] 0 q []env
 S∉Canθₛq S∈Canθₛq = s∉Canₛq (Canθₛunknown->Canₛunknown S q S∈Canθₛq)

 S∉CanθₛpresentSpq : Signal.unwrap S ∉ Canθₛ SigMap.[ S ↦ unknown ]
                                            0
                                            (present S ∣⇒ p ∣⇒ q)
                                            []env
 S∉CanθₛpresentSpq S∈Canθₛ
   with Canθₛunknown->Canₛunknown S (present S ∣⇒ p ∣⇒ q) S∈Canθₛ
 ... | fact
   with Canₛpresent-fact S p q fact
 ... | inj₁ s∈Canₛp = s∉Canₛp s∈Canₛp
 ... | inj₂ s∈Canₛq = s∉Canₛq s∈Canₛq

 bwd : signl S q ≡ₑ (ρ⟨ θS→abs , WAIT ⟩· q) # C
 bwd =
    ≡ₑtran (≡ₑstep [raise-signal])
   (≡ₑtran (≡ₑstep ([absence] S S∈θS→unk θS→unk[S]≡unk S∉Canθₛq))
    ≡ₑrefl)

 fwd : signl S (present S ∣⇒ p ∣⇒ q) ≡ₑ
       (ρ⟨ θS→abs , WAIT ⟩· q) # C
 fwd =
     ≡ₑtran (≡ₑstep [raise-signal])
    (≡ₑtran (≡ₑstep ([absence] S S∈θS→unk θS→unk[S]≡unk S∉CanθₛpresentSpq))
    (≡ₑtran (≡ₑstep ([is-absent] S S∈θS→abs θS→abs[S]≡abs dehole))
     ≡ₑrefl)) where

 calc :  signl S (present S ∣⇒ p ∣⇒ q) ≡ₑ
         signl S q # C
 calc = ≡ₑtran fwd (≡ₑsymm CBq bwd)

ex2 : ∀ S p q C ->
   CB (C ⟦ signl S q ⟧c) ->
   (∀ status -> Signal.unwrap S ∉ (Canₛ p (Θ SigMap.[ S ↦ status ] [] []))) ->
   (∀ status -> Signal.unwrap S ∉ (Canₛ q (Θ SigMap.[ S ↦ status ] [] []))) ->
   signl S (present S ∣⇒ p ∣⇒ q) ≡ₑ
   signl S q # C
ex2 S p q C CB noSp noSq = ex2b S p q C CB (noSp unknown) (noSq unknown)

{-
 Although true, the this example is not provable under the current calculus
{- lifting an emit out of a par -}
ex3 : ∀ S p q -> CB (p ∥ q) ->
  signl S ((emit S >> p) ∥ q) ≡ₑ
  signl S  (emit S >> (p ∥ q)) # []
ex3 S p q CBp∥q = calc where

  θS→unk : Env
  θS→unk = Θ SigMap.[ S ↦ Signal.unknown ] [] []

  S∈θS→unk : SigMap.∈Dom S (sig θS→unk)
  S∈θS→unk = sig-∈-single S Signal.unknown

  θS→unk[S]≡unk : sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.unknown
  θS→unk[S]≡unk = sig-stats-1map' S Signal.unknown S∈θS→unk

  θS→pre : Env
  θS→pre = set-sig{S} θS→unk S∈θS→unk Signal.present

  θS→unk[S]≠absent : ¬ sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.absent
  θS→unk[S]≠absent is rewrite θS→unk[S]≡unk = unknotabs is where
    unknotabs : Signal.unknown ≡ Signal.absent → ⊥
    unknotabs ()

  calc : signl S ((emit S >> p) ∥ q) ≡ₑ
         signl S  (emit S >> (p ∥ q)) # []
  calc =
    ≡ₑtran {r = ρ⟨ θS→unk · ((emit S >> p) ∥ q)}
           (≡ₑstep [raise-signal])
   (≡ₑtran {r = ρ θS→pre · (nothin >> p ∥ q)}
           (≡ₑstep ([emit]{S = S} S∈θS→unk θS→unk[S]≠absent (depar₁ (deseq dehole))))
   (≡ₑtran {r = ρ θS→pre · (p ∥ q)}
           (≡ₑctxt (dcenv (dcpar₁ dchole))
                   (dcenv (dcpar₁ dchole))
                   (≡ₑstep [seq-done]))
           (≡ₑsymm (CBsig (CBseq CBemit CBp∥q
                                 (((λ z → λ ()) ,
                                   (λ z → λ ()) ,
                                   (λ z → λ ())))))
                   (≡ₑtran {r = ρ θS→unk · (emit S >> (p ∥ q))}
                           (≡ₑstep [raise-signal])
                   (≡ₑtran (≡ₑstep ([emit] S∈θS→unk θS→unk[S]≠absent (deseq dehole)))
                           (≡ₑctxt (dcenv dchole)  (dcenv dchole) (≡ₑstep [seq-done])))))))
                           -}

{- pushing a trap across a par -}
ex4 : ∀ n p q -> CB p ->
      done q -> p ≡ₑ q # [] ->
      (trap (exit (suc n) ∥ p)) ≡ₑ (exit n ∥ trap p) # []

ex4 = ex4-split where

  basealwaysdistinct : ∀ x -> distinct base x
  basealwaysdistinct x = (λ { z () x₂ }) , (λ { z () x₂ }) , (λ { z () x₂})

  CBplugrpartrap : ∀ n -> ∀ {r r′ BVp FVp} ->
      CorrectBinding r BVp FVp →
      r′ ≐ ceval (epar₂ (exit n)) ∷ ceval etrap ∷ [] ⟦ r ⟧c →
      CB r′
  CBplugrpartrap n {p} {p′} {BVp} {FVp} CBp r′dc
    with BVFVcorrect p BVp FVp CBp | unplugc r′dc
  ... | refl , refl | refl = CBpar CBexit (CBtrap CBp)
                                   (basealwaysdistinct BVp)
                                   (basealwaysdistinct (BVars p))
                                   (basealwaysdistinct (FVars p))
                                   (λ { _ () _ })

  CBplugtraprpar : ∀ n -> {r r′ : Term}
      {BVp FVp : Σ (List ℕ) (λ x → List ℕ × List ℕ)} →
      CorrectBinding r BVp FVp →
      r′ ≐ ceval etrap ∷ ceval (epar₂ (exit (suc n))) ∷ [] ⟦ r ⟧c →
      CB r′
  CBplugtraprpar n {r} {r′} {BVp} {FVp} CBr r′C
    with unplugc r′C
  ... | refl
    with BVFVcorrect r BVp FVp CBr
  ... | refl , refl
   = CBtrap (CBpar CBexit CBr
                   (basealwaysdistinct BVp)
                   (basealwaysdistinct (BVars r))
                   (basealwaysdistinct (FVars r))
                   (λ { _ () _}))

  ex4-split : ∀ n p q -> CB p ->
              done q -> p ≡ₑ q # [] ->
              (trap (exit (suc n) ∥ p)) ≡ₑ (exit n ∥ trap p) # []
  ex4-split n p .nothin CBp (dhalted hnothin) p≡ₑnothin =
    ≡ₑtran {r = trap (exit (suc n) ∥ nothin)}
           (≡ₑctxt (dctrap (dcpar₂ dchole))
                   (dctrap (dcpar₂ dchole))
                   (≡ₑ-context [] _ (CBplugtraprpar n) p≡ₑnothin))
    (≡ₑtran {r = trap (exit (suc n))}
            (≡ₑctxt (dctrap dchole)
                    (dctrap dchole)
                    (≡ₑtran (≡ₑstep [par-swap])
                            (≡ₑstep ([par-nothing] (dhalted (hexit (suc n)))))))
    (≡ₑtran {r = exit n}
            (≡ₑstep ([trap-done] (hexit (suc n))))
    (≡ₑsymm (CBpar CBexit (CBtrap CBp)
                   (basealwaysdistinct (BVars p))
                   (basealwaysdistinct (BVars p))
                   (basealwaysdistinct (FVars p))
                   (λ { _ () _ }))
            (≡ₑtran {r = exit n ∥ trap nothin}
                    (≡ₑctxt (dcpar₂ (dctrap dchole))
                            (dcpar₂ (dctrap dchole))
                            (≡ₑ-context [] _ (CBplugrpartrap n) p≡ₑnothin))
            (≡ₑtran {r = exit n ∥ nothin}
                    (≡ₑctxt (dcpar₂ dchole) (dcpar₂ dchole) (≡ₑstep ([trap-done] hnothin)))
            (≡ₑtran {r = nothin ∥ exit n}
                    (≡ₑstep [par-swap])
            (≡ₑtran {r = exit n}
                    (≡ₑstep ([par-nothing] (dhalted (hexit n))))
            ≡ₑrefl)))))))

  ex4-split n p .(exit 0) CBp (dhalted (hexit 0)) p≡ₑexit0 =
    ≡ₑtran {r = trap (exit (suc n) ∥ exit 0) }
           (≡ₑctxt (dctrap (dcpar₂ dchole))
                   (dctrap (dcpar₂ dchole))
                   (≡ₑ-context [] _ (CBplugtraprpar n) p≡ₑexit0))
           (≡ₑtran {r = trap (exit (suc n))}
                   (≡ₑctxt (dctrap dchole) (dctrap dchole)
                           (≡ₑstep ([par-2exit] (suc n) zero)))
           (≡ₑtran {r = exit n}
                   (≡ₑstep ([trap-done] (hexit (suc n))))
           (≡ₑsymm (CBpar CBexit (CBtrap CBp)
                          (basealwaysdistinct (BVars p))
                          (basealwaysdistinct (BVars p))
                          (basealwaysdistinct (FVars p))
                          (λ { _ () _ }))
                   (≡ₑtran {r = exit n ∥ trap (exit 0)}
                           (≡ₑctxt (dcpar₂ (dctrap dchole))
                                   (dcpar₂ (dctrap dchole))
                                   (≡ₑ-context [] _ (CBplugrpartrap n) p≡ₑexit0))
                   (≡ₑtran {r = exit n ∥ nothin }
                           (≡ₑctxt (dcpar₂ dchole) (dcpar₂ dchole)
                                   (≡ₑstep ([trap-done] (hexit zero))))
                   (≡ₑtran {r = nothin ∥ exit n}
                           (≡ₑstep [par-swap])
                   (≡ₑtran {r = exit n}
                           (≡ₑstep ([par-nothing] (dhalted (hexit n))))
                   ≡ₑrefl)))))))

  ex4-split n p .(exit (suc m)) CBp (dhalted (hexit (suc m))) p≡ₑexitm =
    ≡ₑtran {r = trap (exit (suc n) ∥ exit (suc m)) }
           (≡ₑctxt (dctrap (dcpar₂ dchole))
                   (dctrap (dcpar₂ dchole))
                   (≡ₑ-context [] _ (CBplugtraprpar n) p≡ₑexitm))
    (≡ₑtran {r = trap (exit (suc n ⊔ℕ (suc m)))}
            (≡ₑctxt (dctrap dchole) (dctrap dchole)
                    (≡ₑstep ([par-2exit] (suc n) (suc m))))
    (≡ₑtran {r = ↓_ {p = (exit (suc n ⊔ℕ (suc m)))} (hexit (suc n ⊔ℕ (suc m))) }
            (≡ₑstep ([trap-done] (hexit (suc (n ⊔ℕ m)))))
    (≡ₑsymm (CBpar CBexit (CBtrap CBp)
                          (basealwaysdistinct (BVars p))
                          (basealwaysdistinct (BVars p))
                          (basealwaysdistinct (FVars p))
                          (λ { _ () _ }))
            (≡ₑtran {r = exit n ∥ trap (exit (suc m))}
                    (≡ₑctxt (dcpar₂ (dctrap dchole))
                            (dcpar₂ (dctrap dchole))
                            (≡ₑ-context [] _ (CBplugrpartrap n) p≡ₑexitm))
            (≡ₑtran {r = exit n ∥  ↓_ {p = exit (suc m)} (hexit (suc m))}
                    (≡ₑctxt (dcpar₂ dchole) (dcpar₂ dchole)
                            (≡ₑstep ([trap-done] (hexit (suc m)))) )
            (≡ₑtran {r =  ↓_ {p = (exit (suc n ⊔ℕ (suc m)))} (hexit (suc n ⊔ℕ (suc m))) }
                    (≡ₑstep ([par-2exit] n m))
            ≡ₑrefl))))))

  ex4-split n p q CBp (dpaused pausedq) p≡ₑq =
    ≡ₑtran {r = trap (exit (suc n) ∥ q)}
           (≡ₑctxt (dctrap (dcpar₂ dchole))
                   (dctrap (dcpar₂ dchole))
                   (≡ₑ-context [] _ (CBplugtraprpar n) p≡ₑq))
    (≡ₑtran {r = trap (exit (suc n))}
            (≡ₑctxt (dctrap dchole) (dctrap dchole)
                    (≡ₑstep ([par-1exit] (suc n) pausedq)))
    (≡ₑtran {r = exit n}
            (≡ₑstep ([trap-done] (hexit (suc n))))
    (≡ₑsymm (CBpar CBexit (CBtrap CBp)
                        (basealwaysdistinct (BVars p))
                        (basealwaysdistinct (BVars p))
                        (basealwaysdistinct (FVars p))
                        (λ { _ () _ }))
            (≡ₑtran {r = exit n ∥ trap q}
                    (≡ₑctxt (dcpar₂ (dctrap dchole))
                            (dcpar₂ (dctrap dchole))
                            (≡ₑ-context [] _ (CBplugrpartrap n) p≡ₑq))
            (≡ₑtran {r = exit n}
                    (≡ₑstep ([par-1exit] n (ptrap pausedq)))
            ≡ₑrefl)))))

{- lifting a signal out of an evaluation context -}
ex5 : ∀ S p q r E -> CB r ->
      q ≐ E ⟦(signl S p)⟧e ->
      r ≐ E ⟦ p ⟧e ->
      (ρ⟨ []env , WAIT ⟩· q) ≡ₑ (ρ⟨ []env , WAIT ⟩· (signl S r)) # []
ex5 S p q r E CBr decomp1 decomp2 = calc where

  θS→unk : Env
  θS→unk = Θ SigMap.[ S ↦ Signal.unknown ] [] []

  replugit : q ≐ Data.List.map ceval E ⟦ signl S p ⟧c ->
             E ⟦ ρ⟨ θS→unk , WAIT ⟩· p ⟧e ≐ Data.List.map ceval E ⟦ ρ⟨ θS→unk , WAIT ⟩· p ⟧c
  replugit x = ⟦⟧e-to-⟦⟧c Erefl

  calc : (ρ⟨ []env , WAIT ⟩· q) ≡ₑ (ρ⟨ []env , WAIT ⟩· (signl S r)) # []
  calc =
    ≡ₑtran {r = ρ⟨ []env , WAIT ⟩· (E ⟦ (ρ⟨ θS→unk , WAIT ⟩· p) ⟧e)}
           (≡ₑctxt (dcenv (⟦⟧e-to-⟦⟧c decomp1))
                   (dcenv (replugit (⟦⟧e-to-⟦⟧c decomp1)))
                   (≡ₑstep [raise-signal]))
   (≡ₑtran {r = ρ⟨ θS→unk , WAIT ⟩· (E ⟦ p ⟧e)}
           (≡ₑstep ([merge]{E = E} Erefl))
           (≡ₑsymm (CBρ (CBsig CBr))
                 (≡ₑtran {r = ρ⟨ []env , WAIT ⟩· (ρ⟨ θS→unk , WAIT ⟩· r)}
                         (≡ₑctxt (dcenv dchole) (dcenv dchole) (≡ₑstep [raise-signal]))
                         (≡ₑstep ([merge] {E = []}
                                          (subst (\ x ->
                                            ρ⟨ θS→unk , WAIT ⟩· x ≐ [] ⟦
                                            ρ⟨ θS→unk , WAIT ⟩· E ⟦ p ⟧e ⟧e)
                                            (unplug decomp2) dehole))))))

{- two specific examples of lifting a signal out of an evaluation context -}
ex6 : ∀ S p q -> CB (p ∥ q) ->
      (ρ⟨ []env , WAIT ⟩· ((signl S p) ∥ q)) ≡ₑ (ρ⟨ []env , WAIT ⟩· (signl S (p ∥ q))) # []
ex6 S p q CBp∥q =
  ex5 S p (signl S p ∥ q) (p ∥ q) ((epar₁ q) ∷ []) CBp∥q (depar₁ dehole) (depar₁ dehole)

ex7 : ∀ S p q -> CB (p >> q) ->
      (ρ⟨ []env , WAIT ⟩· ((signl S p) >> q)) ≡ₑ (ρ⟨ []env , WAIT ⟩· (signl S (p >> q))) # []
ex7 S p q CBp>>q =
  ex5 S p (signl S p >> q) (p >> q) ((eseq q) ∷ []) CBp>>q (deseq dehole) (deseq dehole)

{- pushing a seq into a binding form (a signal in this case).

   this shows the need for the outer environment ρ [} · _
   in order to manipulate the environment.
-}
ex8-worker : ∀ {BV FV} S p q ->
      CorrectBinding ((signl S  p) >> q) BV FV ->
      (ρ⟨ []env , WAIT ⟩· (signl S  p) >> q) ≡ₑ
      (ρ⟨ []env , WAIT ⟩·  signl S (p  >> q)) # []
ex8-worker S p q (CBseq {BVp = BVsigS·p} {FVq = FVq} (CBsig {BV = BVp} CBp) CBq BVsigS·p≠FVq) =
             ≡ₑtran {r = ρ⟨ []env , WAIT ⟩· (ρ⟨ [S]-env S , WAIT ⟩· p) >> q} {C = []}
               (≡ₑctxt {C = []} {C′ = cenv []env WAIT ∷ ceval (eseq q) ∷ []}
                 Crefl Crefl
                 (≡ₑstep ([raise-signal] {p} {S})))
            (≡ₑtran {r = ρ⟨ [S]-env S , WAIT ⟩· p >> q} {C = []}
               (≡ₑstep ([merge] (deseq dehole)))
            (≡ₑsymm
              (CBρ
                (CBsig
                  (CBseq CBp CBq
                    (⊆-respect-distinct-left (∪ʳ (+S S base) ⊆-refl) BVsigS·p≠FVq))))
            (≡ₑtran {r = ρ⟨ []env , WAIT ⟩· (ρ⟨ [S]-env S , WAIT ⟩· p >> q)} {C = []}
              (≡ₑctxt {C = []} {C′ = cenv []env WAIT ∷ []}
                Crefl Crefl
                (≡ₑstep ([raise-signal] {p >> q} {S})))
            (≡ₑstep ([merge] dehole)))))

ex8 : ∀ S p q ->
             CB ((signl S  p) >> q) ->
      (ρ⟨ []env , WAIT ⟩· (signl S  p) >> q) ≡ₑ
      (ρ⟨ []env , WAIT ⟩·  signl S (p  >> q)) # []
ex8 S p q cb = ex8-worker S p q cb

{- rearranging signal forms -}
ex9 : ∀ S1 S2 p ->
     CB p ->
     signl S1 (signl S2 p) ≡ₑ signl S2 (signl S1 p) # []
ex9 S1 S2 p CBp =
  ≡ₑtran {r = ρ⟨ (Θ SigMap.[ S1 ↦ Signal.unknown ] [] []) , WAIT ⟩· (signl S2 p)}
         (≡ₑstep [raise-signal])
 (≡ₑtran {r = (ρ⟨ Θ SigMap.[ S1 ↦ Signal.unknown ] [] [] , WAIT ⟩·
              (ρ⟨ Θ SigMap.[ S2 ↦ Signal.unknown ] [] [] , WAIT ⟩· p))}
         (≡ₑctxt (dcenv dchole) (dcenv dchole) (≡ₑstep [raise-signal]))
 (≡ₑtran {r = (ρ⟨ (Θ SigMap.[ S1 ↦ Signal.unknown ] [] []) ←
               (Θ SigMap.[ S2 ↦ Signal.unknown ] [] []) , A-max WAIT WAIT ⟩·
               p)}
         (≡ₑstep ([merge] dehole))
 (≡ₑsymm (CBsig (CBsig CBp))
         (≡ₑtran {r = ρ⟨ (Θ SigMap.[ S2 ↦ Signal.unknown ] [] []) , WAIT ⟩· (signl S1 p)}
                 (≡ₑstep [raise-signal])
         (≡ₑtran {r = (ρ⟨ Θ SigMap.[ S2 ↦ Signal.unknown ] [] [] , WAIT ⟩·
                        (ρ⟨ Θ SigMap.[ S1 ↦ Signal.unknown ] [] [] , WAIT ⟩· p))}
                 (≡ₑctxt (dcenv dchole) (dcenv dchole) (≡ₑstep [raise-signal]))
         (≡ₑtran {r = (ρ⟨ (Θ SigMap.[ S2 ↦ Signal.unknown ] [] []) ←
                        (Θ SigMap.[ S1 ↦ Signal.unknown ] [] []) ,
                        A-max WAIT WAIT ⟩·
                          p)}
                 (≡ₑstep ([merge] dehole))
                 (map-order-irr S1 S2 WAIT p))))))) where

  distinct-Ss-env'' : ∀ S1 S2 S3 ->
     ¬ Signal.unwrap S1 ≡ Signal.unwrap S2 ->
     Data.List.Any.Any (_≡_ S3) (Signal.unwrap S1 ∷ []) ->
     Data.List.Any.Any (_≡_ S3) (Signal.unwrap S2 ∷ []) ->
     ⊥
  distinct-Ss-env'' S1 S2 S3 S1≠S2 (here S3=S1) (here S3=S2) rewrite S3=S1 = S1≠S2 S3=S2
  distinct-Ss-env'' S1 S2 S3 S1≠S2 (here px) (there ())
  distinct-Ss-env'' S1 S2 S3 S1≠S2 (there ()) S3∈Domθ2

  distinct-Ss-env' : ∀ S1 S2 S3 ->
     ¬ Signal.unwrap S1 ≡ Signal.unwrap S2 ->
     Data.List.Any.Any (_≡_ S3) (Signal.unwrap S1 ∷ []) ->
     S3 ∈ proj₁ (Dom (Θ SigMap.[ S2 ↦ Signal.unknown ] [] [])) ->
     ⊥
  distinct-Ss-env' S1 S2 S3 S1≠S2 S3∈Domθ1 S3∈Domθ2
     rewrite SigMap.keys-1map S2 Signal.unknown =
       distinct-Ss-env'' S1 S2 S3 S1≠S2 S3∈Domθ1 S3∈Domθ2

  distinct-Ss-env : ∀ S1 S2 S3 ->
     ¬ Signal.unwrap S1 ≡ Signal.unwrap S2 ->
     S3 ∈ proj₁ (Dom (Θ SigMap.[ S1 ↦ Signal.unknown ] [] [])) ->
     S3 ∈ proj₁ (Dom (Θ SigMap.[ S2 ↦ Signal.unknown ] [] [])) ->
     ⊥
  distinct-Ss-env S1 S2 S3 S1≠S2 S3∈Domθ1 S3∈Domθ2
    rewrite SigMap.keys-1map S1 Signal.unknown =
      distinct-Ss-env' S1 S2 S3 S1≠S2 S3∈Domθ1 S3∈Domθ2

  distinct-doms : ∀ S1 S2 ->
    ¬ (Signal.unwrap S1 ≡ Signal.unwrap S2) ->
    distinct (Env.Dom (Θ SigMap.[ S1 ↦ Signal.unknown ] [] []))
             (Env.Dom (Θ SigMap.[ S2 ↦ Signal.unknown ] [] []))
  distinct-doms S1 S2 S1≠S2 =
    (λ {S3 S3∈θ1 S3∈θ2 -> distinct-Ss-env S1 S2 S3 S1≠S2 S3∈θ1 S3∈θ2})
    ,
    (λ x₁ x₂ → λ ())
    ,
    (λ x₁ x₂ → λ ())

  map-order-irr' : ∀ S1 S2 ->
     (Θ SigMap.[ S1 ↦ Signal.unknown ] [] []) ←
     (Θ SigMap.[ S2 ↦ Signal.unknown ] [] [])
     ≡
     (Θ SigMap.[ S2 ↦ Signal.unknown ] [] []) ←
     (Θ SigMap.[ S1 ↦ Signal.unknown ] [] [])
  map-order-irr' S1 S2 with (Signal.unwrap S1) Nat.≟ (Signal.unwrap S2)
  map-order-irr' S1 S2 | yes S1=S2 rewrite S1=S2 = refl
  map-order-irr' S1 S2 | no ¬S1=S2 =  Env.←-comm
                               ((Θ SigMap.[ S1 ↦ Signal.unknown ] [] []))
                               ((Θ SigMap.[ S2 ↦ Signal.unknown ] [] []))
                               (distinct-doms S1 S2 ¬S1=S2)

  map-order-irr : ∀ S1 S2 A p ->
       (ρ⟨
         Θ SigMap.[ S2 ↦ Signal.unknown ] [] [] ←
         Θ SigMap.[ S1 ↦ Signal.unknown ] [] []
         ,
         A ⟩· p)
        ≡ₑ
        (ρ⟨
         Θ SigMap.[ S1 ↦ Signal.unknown ] [] [] ←
         Θ SigMap.[ S2 ↦ Signal.unknown ] [] []
         ,
         A ⟩· p) # []
  map-order-irr S1 S2 A p rewrite map-order-irr' S1 S2 = ≡ₑrefl

{- dropping a loop whose body is just `exit` -}

ex10 : ∀ C n -> (loop (exit n)) ≡ₑ (exit n) # C
ex10 C n = ≡ₑtran (≡ₑstep [loop-unroll]) (≡ₑstep [loopˢ-exit])

{- (nothin ∥ p) ≡ₑ p, but only if we know that
   p goes to something that's done -}
ex11 : ∀ p q ->
  CB p -> done q -> p ≡ₑ q # [] ->
  (nothin ∥ p) ≡ₑ p # []
ex11 = calc where

  ex11-pq : ∀ q C -> done q -> (nothin ∥ q) ≡ₑ q # C
  ex11-pq .nothin C (dhalted hnothin) =
    ≡ₑtran (≡ₑstep [par-swap]) (≡ₑstep ([par-nothing] (dhalted hnothin)))
  ex11-pq .(exit n) C (dhalted (hexit n)) =
    ≡ₑstep ([par-nothing] (dhalted (hexit n)))
  ex11-pq q C (dpaused p/paused) =
   ≡ₑstep ([par-nothing] (dpaused p/paused))

  basealwaysdistinct : ∀ x -> distinct base x
  basealwaysdistinct x = (λ { z () x₂ }) , (λ { z () x₂ }) , (λ { z () x₂})

  CBp->CBnothingp : {r r′ : Term}
      {BVp FVp : Σ (List ℕ) (λ x → List ℕ × List ℕ)} →
      CorrectBinding r BVp FVp →
      r′ ≐ ceval (epar₂ nothin) ∷ [] ⟦ r ⟧c → CB r′
  CBp->CBnothingp {r} CBr r′dc
   with sym (unplugc r′dc) | BVFVcorrect _ _ _ CBr
  ... | refl | refl , refl
   = CBpar CBnothing CBr
      (basealwaysdistinct (BVars r))
      (basealwaysdistinct (BVars r))
      (basealwaysdistinct (FVars r))
      (λ { _ () _ })

  calc : ∀ p q ->
    CB p -> done q -> p ≡ₑ q # [] ->
    (nothin ∥ p) ≡ₑ p # []
  calc p q CBp doneq p≡ₑq =
    ≡ₑtran {r = (nothin ∥ q)}
           (≡ₑctxt (dcpar₂ dchole)
                   (dcpar₂ dchole)
                   (≡ₑ-context [] _ CBp->CBnothingp p≡ₑq))
           (≡ₑtran {r = q} (ex11-pq q [] doneq) (≡ₑsymm CBp p≡ₑq))

{- although true, can no longer prove
{- an emit (first) in sequence is the same as emit in parallel -}
ex12 : ∀ S p q ->
      CB p -> done q -> p ≡ₑ q # [] ->
      (signl S ((emit S) ∥ p)) ≡ₑ (signl S ((emit S) >> p)) # []
ex12 S p q CBp doneq p≡ₑq = calc where

  θS→unk : Env
  θS→unk = Θ SigMap.[ S ↦ Signal.unknown ] [] []

  S∈θS→unk : SigMap.∈Dom S (sig θS→unk)
  S∈θS→unk = sig-∈-single S Signal.unknown

  θS→unk[S]≡unk : sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.unknown
  θS→unk[S]≡unk = sig-stats-1map' S Signal.unknown S∈θS→unk

  θS→pre : Env
  θS→pre = set-sig{S} θS→unk S∈θS→unk Signal.present

  θS→unk[S]≠absent : ¬ sig-stats{S = S} θS→unk S∈θS→unk ≡ Signal.absent
  θS→unk[S]≠absent is rewrite θS→unk[S]≡unk = unknotabs is where
    unknotabs : Signal.unknown ≡ Signal.absent → ⊥
    unknotabs ()

  CBp->CBρθSp : {r r′ : Term}
      {BVp FVp : Σ (List ℕ) (λ x → List ℕ × List ℕ)} →
      CorrectBinding r BVp FVp → r′ ≐ cenv θS→pre ∷ [] ⟦ r ⟧c → CB r′
  CBp->CBρθSp {r} CBr r′dc
    with sym (unplugc r′dc) | BVFVcorrect _ _ _ CBr
  ... | refl | refl , refl = CBρ CBr

  basealwaysdistinct : ∀ x -> distinct base x
  basealwaysdistinct x = (λ { z () x₂ }) , (λ { z () x₂ }) , (λ { z () x₂})

  CBsiglSemitS>>p : CB (signl S (emit S >> p))
  CBsiglSemitS>>p =
    CBsig (CBseq CBemit CBp (basealwaysdistinct (FVars p)))

  calc : (signl S ((emit S) ∥ p)) ≡ₑ
         (signl S ((emit S) >> p)) # []
  calc =
     ≡ₑtran {r = ρ θS→unk · ((emit S) ∥ p)}
            (≡ₑstep [raise-signal])
    (≡ₑtran {r =  ρ θS→pre · (nothin ∥ p)}
            (≡ₑstep ([emit] S∈θS→unk θS→unk[S]≠absent (depar₁ dehole)))
    (≡ₑtran {r = ρ θS→pre · p}
            (≡ₑctxt (dcenv dchole) (dcenv dchole)
                    (≡ₑ-context [] (cenv _ ∷ [])
                                CBp->CBρθSp
                                (ex11 p q CBp doneq p≡ₑq)))
    (≡ₑsymm CBsiglSemitS>>p
            (≡ₑtran {r = ρ θS→unk · (emit S >> p)}
                    (≡ₑstep [raise-signal])
            (≡ₑtran {r = ρ θS→pre · nothin >> p}
                    (≡ₑstep ([emit] S∈θS→unk θS→unk[S]≠absent (deseq dehole)))
                    (≡ₑctxt (dcenv dchole) (dcenv dchole)
                            (≡ₑstep [seq-done])))))))

-}

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
interleaved mutual
  -- we don't do `data A : Set`
  data A where
    -- you don't have to actually define any constructor to trigger the error, the "where" is enough

  data B where
    b : B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module getline where

-- https://github.com/alhassy/AgdaCheatSheet#interacting-with-the-real-world-compilation-haskell-and-io

open import Data.Nat                 using (ℕ; suc)
open import Data.Nat.Show            using (show)
open import Data.Char                using (Char)
open import Data.List                as L using (map; sum; upTo)
open import Function                 using (_$_; const; _∘_)
open import Data.String              as S using (String; _++_; fromList)
open import Agda.Builtin.Unit        using (⊤)
open import Codata.Musical.Colist    using (take)
open import Codata.Musical.Costring  using (Costring)
open import Data.Vec.Bounded         as B using (toList)
open import Agda.Builtin.Coinduction using (♯_)
open import IO                       as IO using (run ; putStrLn ; IO)
import      IO.Primitive             as Primitive

infixr 1 _>>=_ _>>_

_>>=_ : ∀ {ℓ} {α β : Set ℓ} → IO α → (α → IO β) → IO β
this >>= f = ♯ this IO.>>= λ x → ♯ f x

_>>_ : ∀{ℓ} {α β : Set ℓ} → IO α → IO β → IO β
x >> y = x >>= const y

postulate
  getLine∞ : Primitive.IO Costring

{-# FOREIGN GHC
  toColist :: [a] -> MAlonzo.Code.Codata.Musical.Colist.AgdaColist a
  toColist []       = MAlonzo.Code.Codata.Musical.Colist.Nil
  toColist (x : xs) =
    MAlonzo.Code.Codata.Musical.Colist.Cons x (MAlonzo.RTE.Sharp (toColist xs))
#-}

{- Haskell's prelude is implicitly available; this is for demonstration. -}
{-# FOREIGN GHC import Prelude as Haskell #-}
{-# COMPILE GHC getLine∞  = fmap toColist Haskell.getLine #-}

-- (1)
-- getLine : IO Costring
-- getLine = IO.lift getLine∞

getLine : IO String
getLine = IO.lift
  $ getLine∞ Primitive.>>= (Primitive.return ∘ S.fromList ∘ B.toList ∘ take 100)

postulate readInt  : L.List Char → ℕ
{-# COMPILE GHC readInt = \x -> read x :: Integer  #-}

main : Primitive.IO ⊤
main = run do
  putStrLn "Hello, world! I'm a compiled Agda program!"

  IO.putStrLn "What is your name?:"
  name ← getLine

  IO.putStrLn "Please enter a number:"
  num ← getLine

  let tri = show $ sum $ upTo $ suc $ readInt $ S.toList num
  putStrLn $ "The triangle number of " ++ num ++ " is " ++ tri

  putStrLn ("Bye, " ++ name)
  -- IO.putStrLn∞ ("Bye, " ++ name)  {- If using approach (1) above. -}

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:
open import Level using () renaming (_⊔_ to _⊔ˡ_)
open import Relation.Binary using (_⇒_; TotalOrder; Reflexive; Symmetric; Transitive; IsEquivalence; IsPreorder; Antisymmetric)

module AKS.Extended {c ℓ₁ ℓ₂} (≤-totalOrder : TotalOrder c ℓ₁ ℓ₂) where

open TotalOrder ≤-totalOrder
  using (_≈_; _≤_; total; isEquivalence)
  renaming (Carrier to C; refl to ≤-refl; reflexive to ≤-reflexive; trans to ≤-trans )
open IsEquivalence isEquivalence
  using ()
  renaming (refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)

data Extended : Set c where
  -∞  : Extended
  ⟨_⟩ : C → Extended

infixl 4 _≈ᵉ_
data _≈ᵉ_ : Extended → Extended → Set (c ⊔ˡ ℓ₁) where
  -∞≈ : -∞ ≈ᵉ -∞
  ⟨_⟩ : ∀ {b t} → b ≈ t → ⟨ b ⟩ ≈ᵉ ⟨ t ⟩

≈ᵉ-refl : Reflexive _≈ᵉ_
≈ᵉ-refl { -∞} = -∞≈
≈ᵉ-refl {⟨ _ ⟩} = ⟨ ≈-refl ⟩

≈ᵉ-sym : Symmetric _≈ᵉ_
≈ᵉ-sym -∞≈ = -∞≈
≈ᵉ-sym ⟨ x≈y ⟩ = ⟨ ≈-sym x≈y ⟩

≈ᵉ-trans : Transitive _≈ᵉ_
≈ᵉ-trans -∞≈ -∞≈ = -∞≈
≈ᵉ-trans ⟨ x≈y ⟩ ⟨ y≈z ⟩ = ⟨ ≈-trans x≈y y≈z ⟩

≈ᵉ-isEquivalence : IsEquivalence _≈ᵉ_
≈ᵉ-isEquivalence = record
  { refl = ≈ᵉ-refl
  ; sym = ≈ᵉ-sym
  ; trans = ≈ᵉ-trans
  }

infixl 4 _≤ᵉ_
data _≤ᵉ_ : Extended → Extended → Set (c ⊔ˡ ℓ₂) where
  -∞≤_ : ∀ t → -∞ ≤ᵉ t
  ⟨_⟩  : ∀ {b t} → b ≤ t → ⟨ b ⟩ ≤ᵉ ⟨ t ⟩

≤ᵉ-refl : Reflexive _≤ᵉ_
≤ᵉ-refl { -∞} = -∞≤ -∞
≤ᵉ-refl {⟨ _ ⟩} = ⟨ ≤-refl ⟩

≤ᵉ-reflexive : _≈ᵉ_ ⇒ _≤ᵉ_
≤ᵉ-reflexive -∞≈ = -∞≤ -∞
≤ᵉ-reflexive ⟨ x≈y ⟩ = ⟨ ≤-reflexive x≈y ⟩

≤ᵉ-trans : Transitive _≤ᵉ_
≤ᵉ-trans {x} {y} {z} (-∞≤ _) (-∞≤ t) = -∞≤ t
≤ᵉ-trans {x} {y} {z} (-∞≤ _) ⟨ _ ⟩   = -∞≤ z
≤ᵉ-trans {x} {y} {z} ⟨ x≤y ⟩ ⟨ y≤z ⟩ = ⟨ (≤-trans x≤y y≤z) ⟩

≤ᵉ-isPreorder : IsPreorder _≈ᵉ_ _≤ᵉ_
≤ᵉ-isPreorder = record { isEquivalence = ≈ᵉ-isEquivalence ; reflexive = ≤ᵉ-reflexive ; trans = ≤ᵉ-trans }

module ≤ᵉ-Reasoning where
   open import Relation.Binary.Reasoning.Base.Double ≤ᵉ-isPreorder public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

open import lib.Basics
open import lib.NType2
open import lib.types.Empty
open import lib.types.Group
open import lib.types.Int
open import lib.types.List
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma

module lib.types.Word {i} where

module _ (A : Type i) where

  PlusMinus : Type i
  PlusMinus = Coprod A A

  Word : Type i
  Word = List PlusMinus

module _ {A : Type i} where

  flip : PlusMinus A → PlusMinus A
  flip (inl a) = inr a
  flip (inr a) = inl a

  flip-flip : ∀ x → flip (flip x) == x
  flip-flip (inl x) = idp
  flip-flip (inr x) = idp

  Word-flip : Word A → Word A
  Word-flip = map flip

  Word-flip-flip : ∀ w → Word-flip (Word-flip w) == w
  Word-flip-flip nil = idp
  Word-flip-flip (x :: l) = ap2 _::_ (flip-flip x) (Word-flip-flip l)

  Word-exp : A → ℤ → Word A
  Word-exp a (pos 0) = nil
  Word-exp a (pos (S n)) = inl a :: Word-exp a (pos n)
  Word-exp a (negsucc 0) = inr a :: nil
  Word-exp a (negsucc (S n)) = inr a :: Word-exp a (negsucc n)

module _ {A : Type i} {j} (G : Group j) where
  private
    module G = Group G

  PlusMinus-extendᴳ : (A → G.El) → (PlusMinus A → G.El)
  PlusMinus-extendᴳ f (inl a) = f a
  PlusMinus-extendᴳ f (inr a) = G.inv (f a)

  Word-extendᴳ : (A → G.El) → (Word A → G.El)
  Word-extendᴳ f = foldr G.comp G.ident ∘ map (PlusMinus-extendᴳ f)

  abstract
    Word-extendᴳ-++ : ∀ f l₁ l₂
      → Word-extendᴳ f (l₁ ++ l₂) == G.comp (Word-extendᴳ f l₁) (Word-extendᴳ f l₂)
    Word-extendᴳ-++ f nil l₂ = ! $ G.unit-l _
    Word-extendᴳ-++ f (x :: l₁) l₂ =
        ap (G.comp (PlusMinus-extendᴳ f x)) (Word-extendᴳ-++ f l₁ l₂)
      ∙ ! (G.assoc (PlusMinus-extendᴳ f x) (Word-extendᴳ f l₁)  (Word-extendᴳ f l₂))

module _ {A : Type i} {j} (G : AbGroup j) where
  private
    module G = AbGroup G

  abstract
    PlusMinus-extendᴳ-comp : ∀ (f g : A → G.El) x
      → PlusMinus-extendᴳ G.grp (λ a → G.comp (f a) (g a)) x
      == G.comp (PlusMinus-extendᴳ G.grp f x) (PlusMinus-extendᴳ G.grp g x)
    PlusMinus-extendᴳ-comp f g (inl a) = idp
    PlusMinus-extendᴳ-comp f g (inr a) = G.inv-comp (f a) (g a) ∙ G.comm (G.inv (g a)) (G.inv (f a))

    Word-extendᴳ-comp : ∀ (f g : A → G.El) l
      → Word-extendᴳ G.grp (λ a → G.comp (f a) (g a)) l
      == G.comp (Word-extendᴳ G.grp f l) (Word-extendᴳ G.grp g l)
    Word-extendᴳ-comp f g nil = ! (G.unit-l G.ident)
    Word-extendᴳ-comp f g (x :: l) =
        ap2 G.comp (PlusMinus-extendᴳ-comp f g x) (Word-extendᴳ-comp f g l)
      ∙ G.interchange (PlusMinus-extendᴳ G.grp f x) (PlusMinus-extendᴳ G.grp g x)
          (Word-extendᴳ G.grp f l) (Word-extendᴳ G.grp g l)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Common.Product

{-# TERMINATING #-}

Loop : Set
Loop = Loop

postulate
  loop : Loop

data Box (A : Set) : Set where
  box : A → Box A

{-# TERMINATING #-}

Boxed-loop : Set
Boxed-loop = Box Boxed-loop

postulate
  boxed-loop : Boxed-loop

test₁ : Boxed-loop
test₁ = quoteGoal g in boxed-loop

test₂ : Term
test₂ = quoteTerm Loop

test₃ : Loop → List (Arg Term)
test₃ _ = quoteContext

macro

  m₄ : Term → Term → TC ⊤
  m₄ _ hole = unify hole (def (quote ⊤) [])

test₄ : Set
test₄ = m₄ Loop

macro

  m₅ : Term → TC ⊤
  m₅ hole = bindTC (inferType (def (quote loop) [])) λ A →
            unify hole A

test₅ : Set
test₅ = m₅

macro

  m₆ : Term → TC ⊤
  m₆ hole =
    bindTC (checkType (def (quote Loop) []) (agda-sort (lit 0))) λ A →
    unify hole A

test₆ : Set
test₆ = m₆

macro

  m₇ : Term → TC ⊤
  m₇ hole =
    bindTC (quoteTC Loop) λ A →
    unify hole A

test₇ : Set
test₇ = m₇

Vec : Set → Nat → Set
Vec A zero    = ⊤
Vec A (suc n) = A × Vec A n

macro

  m₈ : Term → TC ⊤
  m₈ hole =
    bindTC (reduce V) λ V →
    unify hole V
    where
    varg = arg (arg-info visible relevant)
    V    = def (quote Vec) (varg (def (quote Boxed-loop) []) ∷
                            varg (lit (nat 1)) ∷
                            [])

test₈ : Set
test₈ = m₈

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
-- V: letpair (x,y) = (V,W) in E --> E[ V,W / x,y ]
module Properties.StepPair where

open import Data.List
open import Data.List.All
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Values
open import Session

open import Properties.Base

-- this will require multiple steps to execute
mklhs : ∀ {Φ t₁ t₂} → Expr (t₁ ∷ t₂ ∷ Φ) TUnit → Expr (t₁ ∷ t₂ ∷ Φ) TUnit
mklhs {Φ} E =
  letbind (left (left (split-all-right Φ))) (pair (left (rght [])) (here []) (here []))
  (letpair (left (split-all-right Φ)) (here []) E)

reduction :  ∀ {t₁ t₂}
  → (E : Expr (t₁ ∷ t₂ ∷ []) TUnit)
  → (v₁ : Val [] t₁)
  → (v₂ : Val [] t₂)
  → let ϱ = vcons ss-[] v₁ (vcons ss-[] v₂ (vnil []-inactive)) in
    let lhs = (run (left (left [])) ss-[] (mklhs E) ϱ (halt []-inactive UUnit)) in
    let rhs = (run (left (left [])) ss-[] E ϱ (halt []-inactive UUnit)) in
    restart lhs ≡
    rhs
reduction E v₁ v₂
  with split-env (left (left [])) (vcons ss-[] v₁ (vcons ss-[] v₂ (vnil []-inactive)))
... | spe
  = refl

reduction-open-type : Set
reduction-open-type = ∀ {Φ t₁ t₂}
  (E : Expr (t₁ ∷ t₂ ∷ Φ) TUnit)
  (ϱ : VEnv [] (t₁ ∷ t₂ ∷ Φ))
  →
    let lhs = run (left (left (split-all-left Φ))) ss-[] (mklhs E) ϱ (halt []-inactive UUnit) in
    let rhs = run (left (left (split-all-left _))) ss-[] E ϱ (halt []-inactive UUnit) in
    restart lhs ≡ rhs

reduction-open : reduction-open-type
reduction-open {Φ} E (vcons ss-[] v (vcons ss-[] v₁ ϱ))
  rewrite split-rotate-lemma {Φ}
  | split-env-right-lemma0 ϱ
  with ssplit-compose3 ss-[] ss-[]
... | ssc3
    rewrite split-env-right-lemma0 ϱ
     | split-rotate-lemma {Φ}
  = refl

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
{-# OPTIONS --without-K #-}
module Explore.README where

-- The core types behind exploration functions
open import Explore.Core

-- The core properties behind exploration functions
open import Explore.Properties

-- Lifting the dependent axiom of choice to sums and products
open import Explore.BigDistr

-- Constructions on top of exploration functions
open import Explore.Explorable

-- Specific constructions on top of summation functions
open import Explore.Summable

-- Exploration of Cartesian products (and Σ-types)
open import Explore.Product

-- Exploration of disjoint sums
open import Explore.Sum

-- Exploration of base types 𝟘, 𝟙, 𝟚, Fin n
open import Explore.Zero
open import Explore.One
open import Explore.Two
open import Explore.Fin

-- A type universe of explorable types
open import Explore.Universe.Type
open import Explore.Universe.Base
open import Explore.Universe

-- Transporting explorations across isomorphisms
open import Explore.Isomorphism

-- From binary trees to explorations and back
open import Explore.BinTree

-- Exploration functions form a monad
open import Explore.Monad

-- Some high-level properties about group homomorphisms and
-- group isomorphisms.
-- For instance the indistinguisability (One-time-pad like) for groups
open import Explore.Group

-- In a (bit) guessing game,
open import Explore.GuessingGameFlipping

-- An example with a specific type: 6 sided dice
open import Explore.Dice

-- TODO unfinished
-- BROKEN open import Explore.Function.Fin
open import Explore.Subset

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import Relation.Binary using (IsDecEquivalence)
open import Agda.Builtin.Equality

module UnifyMguCorrectG (FunctionName : Set) ⦃ isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName}) ⦄ (PredicateName VariableName : Set) where

open import UnifyTermF FunctionName
open import UnifyMguF FunctionName
open import UnifyMguCorrectF FunctionName

open import Data.Nat
open import Data.Vec
open import Function
open import Data.Fin renaming (thin to thinF; thick to thickF)

data Formula (n : ℕ) : Set
 where
  atomic : PredicateName → ∀ {t} → Vec (Term n) t → Formula n
  logical : Formula n →
            Formula n →
            Formula n
  quantified : Formula (suc n) → Formula n

open import Relation.Binary.PropositionalEquality

instance ThinFormula : Thin Formula
Thin.thin ThinFormula x (atomic x₁ x₂) = atomic x₁ (thin x x₂)
Thin.thin ThinFormula x (logical x₁ x₂) = logical (thin x x₁) (thin x x₂)
Thin.thin ThinFormula x (quantified x₁) = quantified (thin zero x₁)
Thin.thinfact1 ThinFormula f {atomic pn1 ts1} {atomic pn2 ts2} r = {!!}
Thin.thinfact1 ThinFormula f {atomic x x₁} {logical y y₁} ()
Thin.thinfact1 ThinFormula f {atomic x x₁} {quantified y} ()
Thin.thinfact1 ThinFormula f {logical x x₁} {atomic x₂ x₃} ()
Thin.thinfact1 ThinFormula f {logical x x₁} {logical y y₁} x₂ = {!!}
Thin.thinfact1 ThinFormula f {logical x x₁} {quantified y} ()
Thin.thinfact1 ThinFormula f {quantified x} {atomic x₁ x₂} ()
Thin.thinfact1 ThinFormula f {quantified x} {logical y y₁} ()
Thin.thinfact1 ThinFormula f {quantified x} {quantified y} x₁ = {!!}

foo~ : ∀ {m₁ n₁} →
       (Fin m₁ → Term n₁) →
       Fin (suc m₁) → Term (suc n₁)
foo~ f = (λ { zero → i zero ; (suc x) → thin zero (f x)})

foo~i≐i : ∀ {m} → foo~ {m} i ≐ i
foo~i≐i zero = refl
foo~i≐i (suc x) = refl

instance SubstitutionFormula : Substitution Formula
Substitution._◃_ SubstitutionFormula = _◃′_ where
  _◃′_ : ∀ {m n} -> (f : m ~> n) -> Formula m -> Formula n
  f ◃′ atomic 𝑃 τs = atomic 𝑃 (f ◃ τs)
  f ◃′ logical φ₁ φ₂ = logical (f ◃ φ₁) (f ◃ φ₂)
  f ◃′ quantified φ = quantified (foo~ f ◃ φ)

instance SubstitutionExtensionalityFormula : SubstitutionExtensionality Formula
SubstitutionExtensionality.◃ext SubstitutionExtensionalityFormula x (atomic x₁ x₂) = cong (atomic x₁) (◃ext x x₂)
SubstitutionExtensionality.◃ext SubstitutionExtensionalityFormula x (logical t t₁) = cong₂ logical (◃ext x t) (◃ext x t₁)
SubstitutionExtensionality.◃ext SubstitutionExtensionalityFormula x (quantified t) = cong quantified ((◃ext (λ { zero → refl ; (suc x₁) → cong (mapTerm suc) (x x₁)}) t)) --

instance SubFact1Formula : Sub.Fact1 Formula
Sub.Fact1.fact1 SubFact1Formula (atomic x x₁) = cong (atomic x) (Sub.fact1 x₁)
Sub.Fact1.fact1 SubFact1Formula (logical t t₁) = cong₂ logical (Sub.fact1 t) (Sub.fact1 t₁)
Sub.Fact1.fact1 SubFact1Formula {n} (quantified φ) = cong quantified (trans (◃ext {Formula} {_} {_} {foo~ {_} i} {i} (foo~i≐i {_}) φ) (Sub.fact1 φ))

Unifies⋆F : ∀ {m} (s t : Formula m) -> Property⋆ m
Unifies⋆F s t f = f ◃ s ≡ f ◃ t


text:
module Ordinals where

import Level
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Nat using (ℕ) renaming (zero to z; suc to s)
open import Data.Empty

postulate
  ext₀ : Extensionality Level.zero Level.zero
  ext₁ : Extensionality Level.zero (Level.suc Level.zero)

data Ord : Set₁ where
  zero : Ord
  succ : Ord → Ord
  sup  : (A : Set) → (f : A → Ord) → Ord

infixl 10 _≤_

module CountableOrdinals where
  inj-ℕ-Ord : ℕ → Ord
  inj-ℕ-Ord z     = zero
  inj-ℕ-Ord (s n) = succ (inj-ℕ-Ord n)

  ω : Ord
  ω = sup ℕ inj-ℕ-Ord

  _∔_ : Ord → ℕ → Ord
  α ∔ z     = α
  α ∔ (s n) = succ (α ∔ n)

  _ẋ_ : Ord → ℕ → Ord
  α ẋ z     = zero
  α ẋ (s n) = sup ℕ (λ k → (α ẋ n) ∔ k)

  _^^_ : Ord → ℕ → Ord
  α ^^ z     = succ zero
  α ^^ (s n) = sup ℕ (λ k → (α ^^ n) ẋ k)

  ω+ : ℕ → Ord
  ω+ n = ω ∔ n

  ω× : ℕ → Ord
  ω× n = ω ẋ n

  ω^ : ℕ → Ord
  ω^ n = ω ^^ n

  ω+1≢ω : sup ℕ (succ ∘ inj-ℕ-Ord) ≡ ω → ⊥
  ω+1≢ω p = {!!}

-- This should not be provable!
-- succ-sup : ∀ A f → sup A (succ ∘ f) ≡ succ (sup A f)
-- succ-sup A f = {!!}

_+_ : Ord → Ord → Ord
α + zero    = α
α + succ β  = succ (α + β)
α + sup A f = sup A (λ x → α + f x)

zeroₗ : ∀ α → zero + α ≡ α
zeroₗ zero      = refl
zeroₗ (succ α)  = cong succ (zeroₗ α)
zeroₗ (sup A f) = cong (sup A) (ext₁ (λ x → zeroₗ (f x)))

succₗ : ∀ α β → succ α + β ≡ succ (α + β)
succₗ α zero = refl
succₗ α (succ β) = cong succ (succₗ α β)
succₗ α (sup A f) = {!!}
-- trans (cong (sup A) (ext₁ (λ x → succₗ α (f x))))
                    --       (succ-sup A (λ x → α + f x))

_≤_ : Ord → Ord → Set₁
α ≤ β = ∃ λ γ → α + γ ≡ β

≤-refl : ∀ α → α ≤ α
≤-refl α = (zero , refl)

zero-min : ∀ α → zero ≤ α
zero-min α = (α , zeroₗ α)

≤-succ : ∀ α β → α ≤ β → succ α ≤ succ β
≤-succ α β (γ , p) = (γ , trans (succₗ α γ) (cong succ p))

≤-step : ∀ α β → α ≤ β → α ≤ succ β
≤-step α β (γ , p) = (succ γ , cong succ p)

≤-sup-step : ∀ α A f → (∀ x → α ≤ f x) → α ≤ sup A f
≤-sup-step α A f p = (sup A (proj₁ ∘ p) , cong (sup A) (ext₁ (proj₂ ∘ p)))

≤-supₗ : ∀ A f β → (∀ x → f x ≤ β) → sup A f ≤ β
≤-supₗ A f β p = (sup A (proj₁ ∘ p) , {!!})
  where
    q : (x : A) → (f x + proj₁ (p x)) ≡ β
    q = proj₂ ∘ p

≤-sup : ∀ A f g → (∀ x → f x ≤ g x) → sup A f ≤ sup A g
≤-sup A f g p = (sup A (proj₁ ∘ p) , {!!}) -- cong (sup A) (ext₁ {!!}))
  where
    q : (x : A) → (f x + proj₁ (p x)) ≡ g x
    q = proj₂ ∘ p

    q' : (x : A) → (sup A f + (proj₁ ∘ p) x) ≡ g x
    q' = {!!}

lem₁ : ∀ α β → α ≤ α + β
lem₁ α zero      = ≤-refl α
lem₁ α (succ β)  = ≤-step α (α + β) (lem₁ α β)
lem₁ α (sup A f) = ≤-sup-step α A (λ x → α + f x) (λ x → lem₁ α (f x))

lem₂ : ∀ α β → β ≤ α + β
lem₂ α zero = zero-min (α + zero)
lem₂ α (succ β) = ≤-succ β (α + β) (lem₂ α β)
lem₂ α (sup A f) = ≤-sup A f (λ x → α + f x) (λ x → lem₂ α (f x))

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox