text:
module Selective.Examples.Bookstore where

open import Selective.ActorMonad
open import Selective.Libraries.Call using (UniqueTag ; call)
open import Prelude

open import Data.Nat
  using ( _≟_ ; pred ; ⌈_/2⌉ ; _≤?_ ; _∸_ ; _≤_ ; z≤n ; s≤s ; _<_ ; _≰_  )
open import Data.Nat.Properties
  using (≤-antisym ; ≰⇒>)
open import Data.Nat.Show
  using (show)
open import Data.String
  using (primStringEquality)

open import Debug

BookTitle = String
Money = ℕ

data BuyerRole : Set where
  Buyer1 Buyer2 : BuyerRole

record Book : Set where
  field
    title : BookTitle
    price : Money

-- ===========
--  GET QUOTE
-- ===========

GetQuoteReply : MessageType
GetQuoteReply = ValueType UniqueTag ∷ [ ValueType (Maybe Book) ]ˡ

GetQuoteReplyInterface : InboxShape
GetQuoteReplyInterface = [ GetQuoteReply ]ˡ

GetQuote : MessageType
GetQuote = ValueType UniqueTag ∷ ReferenceType GetQuoteReplyInterface ∷ [ ValueType BookTitle ]ˡ

-- ======================
--  PROPOSE CONTRIBUTION
-- ======================

record Contribution : Set where
  field
    book : Book
    money : Money

ContributionMessage : MessageType
ContributionMessage = [ ValueType Contribution ]ˡ

-- ===============
--  AGREE OR QUIT
-- ===============

data AgreeChoice : Set where
  AGREE QUIT : AgreeChoice

AgreeDecision : MessageType
AgreeDecision = [ ValueType AgreeChoice ]ˡ

-- ================
--  TRANSFER MONEY
-- ================

Transfer : MessageType
Transfer = ValueType BuyerRole ∷  [ ValueType Contribution ]ˡ

-- ============
--  INTERFACES
-- ============

Buyer1-to-Seller : InboxShape
Buyer1-to-Seller = GetQuote ∷ [ Transfer ]ˡ

Buyer2-to-Seller : InboxShape
Buyer2-to-Seller = AgreeDecision ∷ [ Transfer ]ˡ

Buyer1-to-Buyer2 : InboxShape
Buyer1-to-Buyer2 = [ ContributionMessage ]ˡ

Buyer2-to-Buyer1 : InboxShape
Buyer2-to-Buyer1 = [ AgreeDecision ]ˡ

SellerInterface : InboxShape
SellerInterface = GetQuote ∷ AgreeDecision ∷ [ Transfer ]ˡ

Buyer1Interface : InboxShape
Buyer1Interface = [ ReferenceType Buyer1-to-Seller ]ˡ ∷  [ ReferenceType Buyer1-to-Buyer2 ]ˡ ∷ GetQuoteReply ∷ [ AgreeDecision ]ˡ

Buyer2Interface : InboxShape
Buyer2Interface = [ ReferenceType Buyer2-to-Seller ]ˡ ∷ [ ReferenceType Buyer2-to-Buyer1 ]ˡ ∷ [ ContributionMessage ]ˡ

-- ========
--  COMMON
-- ========

book1 : BookTitle
book1 = "Crime and Punishment"

transfer-money : ∀ {i IS Seller Γ} →
                 Γ ⊢ Seller →
                 [ Transfer ]ˡ <: Seller →
                 BuyerRole →
                 Book →
                 Money →
                 ∞ActorM i IS ⊤₁ Γ (λ _ → Γ)
transfer-money p sub role book money = p ![t: translate-⊆ sub Z ] ((lift role) ∷ [ lift record { book = book ; money = money } ]ᵃ)

-- ========
--  SELLER
-- ========

same-buyer-role : BuyerRole → BuyerRole → Bool
same-buyer-role Buyer1 Buyer1 = true
same-buyer-role Buyer1 Buyer2 = false
same-buyer-role Buyer2 Buyer1 = false
same-buyer-role Buyer2 Buyer2 = true

data TransactionStatus (book : Book) (c1 c2 : Contribution) : Set where
  TooLittleMoney : (Contribution.money c1 + Contribution.money c2) < (Book.price book) → TransactionStatus book c1 c2
  Accepted : (Contribution.money c1 + Contribution.money c2) ≡ (Book.price book) → TransactionStatus book c1 c2
  TooMuchMoney : (Book.price book) < (Contribution.money c1 + Contribution.money c2) → TransactionStatus book c1 c2

transaction-status? : ∀ book c1 c2 → TransactionStatus book c1 c2
transaction-status? book c1 c2 with (Contribution.money c1 + Contribution.money c2 ≤? Book.price book) | (Book.price book ≤? Contribution.money c1 + Contribution.money c2)
transaction-status? book c1 c2 | yes p | yes q = Accepted (≤-antisym p q)
transaction-status? book c1 c2 | yes p | no ¬p = TooLittleMoney (≰⇒> ¬p)
transaction-status? book c1 c2 | no ¬p | q = TooMuchMoney (≰⇒> ¬p)

seller : ∀ {i} → ActorM i SellerInterface ⊤₁ [] (λ _ → [])
seller = begin do
    record {msg = Msg Z (tag ∷ _ ∷ title ∷ []) } ← selective-receive select-quote
      where
        record { msg = (Msg (S _) _) ; msg-ok = () }
    let maybe-book = find-book known-books title
    (Z ![t: Z ] (lift tag ∷ [ lift maybe-book ]ᵃ))
    after-book-quote maybe-book
  where
    select-quote : MessageFilter SellerInterface
    select-quote (Msg Z _) = true
    select-quote _ = false
    known-books : List Book
    known-books = [ record { title = book1 ; price = 37 } ]ˡ
    find-book : List Book → BookTitle → Maybe Book
    find-book [] title = nothing
    find-book (book ∷ books) title with (primStringEquality (Book.title book) title)
    ... | true = just book
    ... | false = find-book books title
    select-decision : MessageFilter SellerInterface
    select-decision (Msg (S Z) _) = true
    select-decision _ = false
    wait-for-decision : ∀ {i Γ} →
                        ∞ActorM i SellerInterface (Lift (lsuc lzero) AgreeChoice) Γ (λ _ → Γ)
    wait-for-decision = do
      record { msg = Msg (S Z) (ac ∷ []) } ← (selective-receive select-decision)
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S (S _)) _) ; msg-ok = () }
      return ac
    select-contribution-from : BuyerRole → MessageFilter SellerInterface
    select-contribution-from br (Msg (S (S Z)) (br' ∷ _)) = same-buyer-role br br'
    select-contribution-from _ _ = false
    wait-for-money-from : ∀ {i Γ} →
                          BuyerRole →
                          ∞ActorM i SellerInterface (Lift (lsuc lzero) Contribution) Γ (λ _ → Γ)
    wait-for-money-from br = do
      record { msg = Msg (S (S Z)) (_ ∷ contribution ∷ []) } ← (selective-receive (select-contribution-from br))
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S Z) _) ; msg-ok = () }
          record { msg = (Msg (S (S (S _))) _) ; msg-ok = () }
      return contribution
    transaction-message : Book → Contribution → Contribution → String
    transaction-message book c1 c2 with (transaction-status? book c1 c2)
    ... | Accepted _ = "Accepted purchase of " || Book.title book || " for $" || show (Book.price book)
    ... | TooLittleMoney p = "Received too little money for " || Book.title book || ". $" || show (Book.price book) || " - $" || show (Contribution.money c1) || " - $" || show (Contribution.money c2) || " = $" || show (Book.price book ∸ Contribution.money c1 ∸ Contribution.money c2)
    ... | TooMuchMoney p = "Received too much money for " || Book.title book || ". $" || show (Book.price book) || " - $" || show (Contribution.money c1) || " - $" || show (Contribution.money c2) || " = -$" || show ((Contribution.money c1 + Contribution.money c2) ∸ Book.price book)
    after-book-quote : ∀ {i} →
                       Maybe Book →
                       ∞ActorM i SellerInterface ⊤₁ [ GetQuoteReplyInterface ]ˡ (λ _ → [])
    after-book-quote (just book) = do
      lift AGREE ← wait-for-decision
        where
          lift QUIT → debug "seller sees that transaction was quit" (strengthen [])
      lift contrib1 ← wait-for-money-from Buyer1
      lift contrib2 ← wait-for-money-from Buyer2
      debug (transaction-message book contrib1 contrib2) (strengthen [])
    after-book-quote nothing = strengthen []

-- =========
--  BUYER 1
-- =========

buyer1 : ∀ {i} → ActorM i Buyer1Interface ⊤₁ [] (λ _ → [])
buyer1 = begin do
    wait-for-seller
    lift (just book) ← get-quote Z 0 book1
      where
        (lift nothing) → strengthen []
    wait-for-buyer2
    let my-contribution = ⌈ Book.price book /2⌉
    send-contribution Z book my-contribution
    lift AGREE ← wait-for-decision
      where
        lift QUIT → debug "buyer1 sees that transaction was quit" (strengthen [])
    (transfer-money (S Z) (⊆-suc ⊆-refl) Buyer1 book my-contribution)
    (strengthen [])
  where
    select-seller : MessageFilter Buyer1Interface
    select-seller (Msg Z _) = true
    select-seller (Msg (S _) _) = false
    wait-for-seller : ∀ {i Γ} → ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Buyer1-to-Seller ∷ Γ)
    wait-for-seller = do
      record { msg = Msg Z _ } ← (selective-receive select-seller)
        where
          record { msg = (Msg (S _) _) ; msg-ok = () }
      return _
    select-buyer2 : MessageFilter Buyer1Interface
    select-buyer2 (Msg (S Z) _) = true
    select-buyer2 _ = false
    wait-for-buyer2 : ∀ {i Γ} → ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Buyer1-to-Buyer2 ∷ Γ)
    wait-for-buyer2 = do
      record {msg = Msg (S Z) _ } ← selective-receive select-buyer2
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S (S _)) _) ; msg-ok = () }
      return _
    get-quote : ∀ {i Γ} →
               Γ ⊢ Buyer1-to-Seller →
               UniqueTag →
               BookTitle →
               ∞ActorM i Buyer1Interface (Lift (lsuc lzero) (Maybe Book)) Γ (λ _ → Γ)
    get-quote p tag title = do
      record { msg = Msg (S (S Z)) (_ ∷ book ∷ []) ; msg-ok = msg-ok } ← call p Z tag [ lift title ]ᵃ [ S (S Z) ]ᵐ Z
        where
          record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () }
          record { msg = (Msg (S Z) (_ ∷ _)) ; msg-ok = () }
          record { msg = (Msg (S (S (S Z))) _) ; msg-ok = () }
          record { msg = (Msg (S (S (S (S _)))) _) ; msg-ok = () }
      return book
    send-contribution : ∀ {i Γ} →
                       Γ ⊢ Buyer1-to-Buyer2 →
                       Book →
                       Money →
                       ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Γ)
    send-contribution p book money = p ![t: Z ] [ lift record { book = book ; money = money } ]ᵃ
    select-decision : MessageFilter Buyer1Interface
    select-decision (Msg (S (S (S Z))) _) = true
    select-decision _ = false
    wait-for-decision : ∀ {i Γ} →
                        ∞ActorM i Buyer1Interface (Lift (lsuc lzero) AgreeChoice) Γ (λ _ → Γ)
    wait-for-decision = do
      record {msg = Msg (S (S (S Z))) (ac ∷ []) } ← (selective-receive select-decision)
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S Z) _) ; msg-ok = () }
          record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
          record { msg = (Msg (S (S (S (S _)))) _) ; msg-ok = () }
      return ac

-- =========
--  BUYER 2
-- =========

buyer2 : ∀ {i} → ActorM i Buyer2Interface ⊤₁ [] (λ _ → [])
buyer2 = begin do
    wait-for-seller
    wait-for-buyer1
    lift contribution ← wait-for-contribution
    handle-contribution (S Z) Z contribution
    strengthen []
  where
    select-seller : MessageFilter Buyer2Interface
    select-seller (Msg Z _) = true
    select-seller (Msg (S _) _) = false
    wait-for-seller : ∀ {i Γ} → ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Buyer2-to-Seller ∷ Γ)
    wait-for-seller = do
      record { msg = Msg Z _ } ← (selective-receive select-seller)
        where
          record { msg = (Msg (S _) _) ; msg-ok = () }
      return _
    select-buyer1 : MessageFilter Buyer2Interface
    select-buyer1 (Msg (S Z) _) = true
    select-buyer1 _ = false
    wait-for-buyer1 : ∀ {i Γ} → ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Buyer2-to-Buyer1 ∷ Γ)
    wait-for-buyer1 = do
      record {msg = Msg (S Z) _ } ← selective-receive select-buyer1
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S (S _)) _) ; msg-ok = () }
      return _
    select-contribution : MessageFilter Buyer2Interface
    select-contribution (Msg (S (S Z)) _) = true
    select-contribution _ = false
    wait-for-contribution : ∀ {i Γ} → ∞ActorM i Buyer2Interface (Lift (lsuc lzero) Contribution) Γ (λ _ → Γ)
    wait-for-contribution = do
      record { msg = Msg (S (S Z)) (cc ∷ []) } ← (selective-receive select-contribution)
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S Z) _) ; msg-ok = () }
          record { msg = (Msg (S (S (S _))) _) ; msg-ok = () }
      return cc
    contribution-is-fair : Money → Money → Bool
    contribution-is-fair price money = ⌊ price ∸ money ≤? money ⌋
    handle-contribution : ∀ {i Γ} →
                          Γ ⊢ Buyer2-to-Seller →
                          Γ ⊢ Buyer2-to-Buyer1 →
                          Contribution →
                          ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Γ)
    handle-contribution seller buyer1 record { book = book ; money = money } with (contribution-is-fair (Book.price book) money)
    ... | true = do
      buyer1 ![t: Z ] [ lift AGREE ]ᵃ
      seller ![t: Z ] [ lift AGREE ]ᵃ
      transfer-money seller (⊆-suc ⊆-refl) Buyer2 book ((Book.price book) ∸ money)
    ... | false = do
      buyer1 ![t: Z ] [ lift QUIT ]ᵃ
      seller ![t: Z ] [ lift QUIT ]ᵃ

-- ============
--  SUPERVISOR
-- ============

bookstore-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → [])
bookstore-supervisor = do
  spawn seller
  spawn buyer1
  spawn buyer2
  Z ![t: Z ]  [ [ (S (S Z)) ]>: ( S Z ∷ [ S (S Z) ]ᵐ)]ᵃ
  Z ![t: S Z ] [ [ S Z ]>: [ S (S (S Z)) ]ᵐ ]ᵃ
  (S Z) ![t: Z ] [ [ S (S Z) ]>: (Z ∷ [ S (S Z) ]ᵐ) ]ᵃ
  (S Z) ![t: S Z ] [ [ Z ]>: [ S (S Z) ]ᵐ ]ᵃ
  (strengthen [])

max_stars_repo_name: Zalastax/singly-typed-actors


text:
open import Mockingbird.Forest using (Forest)

-- Is There a Sage Bird?
module Mockingbird.Problems.Chapter10 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_,_; proj₁; proj₂; ∃-syntax)
open import Function using (_$_)

open import Mockingbird.Forest.Birds forest

open Forest forest

module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasLark ⦄ where
  private
    hasMockingbirdComposer : ∃[ A ] (∀ x y → A ∙ x ∙ y ≈ x ∙ (M ∙ y))
    hasMockingbirdComposer = (L , isMockingbirdComposer)
      where
        isMockingbirdComposer = λ x y → begin
          L ∙ x ∙ y    ≈⟨ isLark x y ⟩
          x ∙ (y ∙ y)  ≈˘⟨ congˡ $ isMockingbird y ⟩
          x ∙ (M ∙ y)  ∎

  hasSageBird : HasSageBird
  hasSageBird = record
    { Θ = M ∘ L
    ; isSageBird = λ x → begin
        x ∙ ((M ∘ L) ∙ x)        ≈⟨ congˡ $ isComposition M L x ⟩
        x ∙ (M ∙ (L ∙ x))        ≈⟨ congˡ $ isMockingbird (L ∙ x) ⟩
        x ∙ ((L ∙ x) ∙ (L ∙ x))  ≈˘⟨ isLark x (L ∙ x) ⟩
        (L ∙ x) ∙ (L ∙ x)        ≈˘⟨ isMockingbird (L ∙ x) ⟩
        M ∙ (L ∙ x)              ≈˘⟨ isComposition M L x ⟩
        (M ∘ L) ∙ x              ∎
    }

module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄
         (hasMockingbirdComposer : ∃[ A ] (∀ x y → A ∙ x ∙ y ≈ x ∙ (M ∙ y))) where

  private
    A = proj₁ hasMockingbirdComposer
    [Ax]y≈x[My] = proj₂ hasMockingbirdComposer

    instance
      hasLark : HasLark
      hasLark = record
        { L = A
        ; isLark = λ x y → begin
            (A ∙ x) ∙ y  ≈⟨ [Ax]y≈x[My] x y ⟩
            x ∙ (M ∙ y)  ≈⟨ congˡ $ isMockingbird y ⟩
            x ∙ (y ∙ y)  ∎
        }

  hasSageBird′ : HasSageBird
  hasSageBird′ = hasSageBird

ext: agda

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text: _ : Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module eq-reas-nouni {A : Set} where

  open import eq

  infix  1 begin_
  infixr 2 _equiv[]_ _equiv[_]_
  infix  3 _qed

  begin_ : ∀ {x y : A}
    → x ≡ y
    -----
    → x ≡ y
  begin x≡y  =  x≡y

  _equiv[]_ : ∀ (x : A) {y : A}
    → x ≡ y
    -----
    → x ≡ y
  x equiv[] x≡y  =  x≡y

  _equiv[_]_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
    -----
    → x ≡ z
  x equiv[ x≡y ] y≡z  =  trans x≡y y≡z

  _qed : ∀ (x : A)
    -----
    → x ≡ x
  x qed  =  refl

max_stars_repo_name: JimFixGroupResearch/imper-ial

max_issues_repo_name: JimFixGroupResearch/imper-ial

max_forks_repo_name: JimFixGroupResearch/imper-ial


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

module Haskell.Modules.FunctorApplicativeMonad where

open import Haskell.Modules.Either
------------------------------------------------------------------------------
open import Data.List
open import Data.Maybe renaming (_>>=_ to _Maybe->>=_)
open import Function
open import Level renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)

record Functor  {ℓ₁ ℓ₂ : Level} (F : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
  infixl 4 _<$>_
  field
    _<$>_ : ∀ {A B : Set ℓ₁} → (A → B) → F A → F B
  fmap = _<$>_
open Functor ⦃ ... ⦄ public

record Applicative {ℓ₁ ℓ₂ : Level} (F : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
  infixl 4 _<*>_
  field
    pure  : ∀ {A : Set ℓ₁} → A → F A
    _<*>_ : ∀ {A B : Set ℓ₁} → F (A → B) → F A → F B
open Applicative ⦃ ... ⦄ public
instance
  ApplicativeFunctor : ∀ {ℓ₁ ℓ₂} {F : Set ℓ₁ → Set ℓ₂} ⦃ _ : Applicative F ⦄ → Functor F
  Functor._<$>_ ApplicativeFunctor f xs = pure f <*> xs

record Monad {ℓ₁ ℓ₂ : Level} (M : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
  infixl 1 _>>=_ _>>_
  field
    return : ∀ {A : Set ℓ₁} → A → M A
    _>>=_  : ∀ {A B : Set ℓ₁} → M A → (A → M B) → M B

  _>>_ : ∀ {A B : Set ℓ₁} → M A → M B → M B
  m₁ >> m₂ = m₁ >>= λ _ → m₂
open Monad ⦃ ... ⦄ public
instance
  MonadApplicative : ∀ {ℓ₁ ℓ₂} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : Monad M ⦄ → Applicative M
  Applicative.pure  MonadApplicative       = return
  Applicative._<*>_ MonadApplicative fs xs = do
    f ← fs
    x ← xs
    return (f x)

instance
  Monad-Either : ∀ {ℓ}{C : Set ℓ} → Monad{ℓ}{ℓ} (Either C)
  Monad.return (Monad-Either{ℓ}{C}) = Right
  Monad._>>=_  (Monad-Either{ℓ}{C}) = either (const ∘ Left) _|>_

  Monad-Maybe : ∀ {ℓ} → Monad {ℓ} {ℓ} Maybe
  Monad.return (Monad-Maybe{ℓ}) = just
  Monad._>>=_  (Monad-Maybe{ℓ}) = _Maybe->>=_

  Monad-List : ∀ {ℓ} → Monad {ℓ}{ℓ} List
  Monad.return Monad-List x   = x ∷ []
  Monad._>>=_  Monad-List x f = concat (Data.List.map f x)


text:
module Issue279-4 where

module M (X : Set) where

  data R : Set where
    r : X → R

postulate
  P Q : Set

open M P using (r)

shouldn't-check : M.R Q → Q
shouldn't-check (r q) = q

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Colists
------------------------------------------------------------------------

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

module Codata.Colist.Bisimilarity where

open import Level using (Level; _⊔_)
open import Size
open import Codata.Thunk
open import Codata.Colist
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
open import Data.List.NonEmpty as List⁺  using (List⁺; _∷_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

private
  variable
    a b c p q r : Level
    A : Set a
    B : Set b
    C : Set c
    i : Size

data Bisim {A : Set a} {B : Set b} (R : REL A B r) (i : Size) :
           REL (Colist A ∞) (Colist B ∞) (r ⊔ a ⊔ b) where
  []  : Bisim R i [] []
  _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys →
        Bisim R i (x ∷ xs) (y ∷ ys)

module _ {R : Rel A r} where

 reflexive : Reflexive R → Reflexive (Bisim R i)
 reflexive refl^R {[]}     = []
 reflexive refl^R {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R

module _ {P : REL A B p} {Q : REL B A q} where

 symmetric : Sym P Q → Sym (Bisim P i) (Bisim Q i)
 symmetric sym^PQ []       = []
 symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force)

module _ {P : REL A B p} {Q : REL B C q} {R : REL A C r} where

 transitive : Trans P Q R → Trans (Bisim P i) (Bisim Q i) (Bisim R i)
 transitive trans^PQR []       []       = []
 transitive trans^PQR (p ∷ ps) (q ∷ qs) =
   trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force)

------------------------------------------------------------------------
-- Congruence rules

module _ {R : REL A B r} where

  ++⁺ : ∀ {as bs xs ys} → Pointwise R as bs →
        Bisim R i xs ys → Bisim R i (fromList as ++ xs) (fromList bs ++ ys)
  ++⁺ []       rs = rs
  ++⁺ (r ∷ pw) rs = r ∷ λ where .force → ++⁺ pw rs

  ⁺++⁺ : ∀ {as bs xs ys} → Pointwise R (List⁺.toList as) (List⁺.toList bs) →
         Thunk^R (Bisim R) i xs ys → Bisim R i (as ⁺++ xs) (bs ⁺++ ys)
  ⁺++⁺ (r ∷ pw) rs = r ∷ λ where .force → ++⁺ pw (rs .force)

------------------------------------------------------------------------
-- Pointwise Equality as a Bisimilarity

module _ {A : Set a} where

  infix 1 _⊢_≈_
  _⊢_≈_ : ∀ i → Colist A ∞ → Colist A ∞ → Set a
  _⊢_≈_ = Bisim _≡_

  refl : Reflexive (i ⊢_≈_)
  refl = reflexive Eq.refl

  fromEq : ∀ {as bs} → as ≡ bs → i ⊢ as ≈ bs
  fromEq Eq.refl = refl

  sym : Symmetric (i ⊢_≈_)
  sym = symmetric Eq.sym

  trans : Transitive (i ⊢_≈_)
  trans = transitive Eq.trans

isEquivalence : {R : Rel A r} → IsEquivalence R → IsEquivalence (Bisim R i)
isEquivalence equiv^R = record
  { refl  = reflexive equiv^R.refl
  ; sym   = symmetric equiv^R.sym
  ; trans = transitive equiv^R.trans
  } where module equiv^R = IsEquivalence equiv^R

setoid : Setoid a r → Size → Setoid a (a ⊔ r)
setoid S i = record
  { isEquivalence = isEquivalence {i = i} (Setoid.isEquivalence S)
  }

module ≈-Reasoning {a} {A : Set a} {i} where

  open import Relation.Binary.Reasoning.Setoid (setoid (Eq.setoid A) i) public


text:
module LC.Example where

open import LC.Base
open import LC.Subst
open import LC.Reduction
open import LC.Reasoning

test-1 : ((ƛ var 0) ∙ var 0) β→* ((var 0) [ var 0 ])
test-1 =
  begin
    (ƛ var 0) ∙ var 0
  →⟨ β-ƛ-∙ ⟩
    (var 0) [ var 0 ]
  ∎

test-0 : ƛ (ƛ var 0 ∙ var 1) ∙ (ƛ var 0 ∙ var 1) β→* ƛ var 0 ∙ var 0
test-0 =
    begin
        ƛ (ƛ var 0 ∙ var 1) ∙ (ƛ var 0 ∙ var 1)
    →⟨ β-ƛ β-ƛ-∙ ⟩
        ƛ (var 0 ∙ var 1) [ ƛ var 0 ∙ var 1 ]
    →⟨⟩
        ƛ (var 0 ∙ var 1) [ ƛ var 0 ∙ var 1 / 0 ]
    →⟨⟩
        ƛ (var 0) [ ƛ var 0 ∙ var 1 / 0 ] ∙ (var 1) [ ƛ var 0 ∙ var 1 / 0 ]
    →⟨⟩
        ƛ lift 0 0 (ƛ var 0 ∙ var 1) ∙ var 0
    →⟨⟩
        ƛ (ƛ lift 0 0 (var 0 ∙ var 1)) ∙ var 0
    →⟨⟩
        ƛ (ƛ lift 0 0 (var 0) ∙ lift 0 0 (var 1)) ∙ var 0
    →⟨⟩
        ƛ ((ƛ var 0 ∙ var 1) ∙ var 0)
    →⟨ β-ƛ β-ƛ-∙ ⟩
        ƛ (var 0 ∙ var 1) [ var 0 / 0 ]
    →⟨⟩
        ƛ var 0 ∙ var 0
    ∎

Z : Term
Z = ƛ ƛ var 0

SZ : Term
SZ = ƛ ƛ var 1 ∙ var 0

PLUS : Term
PLUS = ƛ ƛ ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)

test-2 : PLUS ∙ Z ∙ SZ β→* SZ
test-2 =
  begin
    PLUS ∙ Z ∙ SZ
  →⟨ β-∙-l β-ƛ-∙ ⟩
    (ƛ ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 0 ] ∙ SZ
  →⟨⟩
    (ƛ ((ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 1 ])) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 2 ])) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ ((var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)) [ ƛ ƛ var 0 / 3 ])))) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ (var 3) [ ƛ ƛ var 0 / 3 ] ∙ (var 1) [ ƛ ƛ var 0 / 3 ] ∙ (var 2 ∙ var 1 ∙ var 0) [ ƛ ƛ var 0 / 3 ]))) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ (lift 0 3 (ƛ (ƛ var 0))) ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ (ƛ (ƛ (var 0))) ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
  →⟨ β-∙-l (β-ƛ (β-ƛ (β-ƛ (β-∙-l β-ƛ-∙)))) ⟩
    (ƛ (ƛ (ƛ (ƛ var 0) [ var 1 / 0 ] ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ (ƛ (var 0) [ var 1 / 1 ]) ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ (ƛ var 0) ∙ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
  →⟨ β-∙-l (β-ƛ (β-ƛ (β-ƛ β-ƛ-∙))) ⟩
    (ƛ (ƛ (ƛ (var 0) [ var 2 ∙ var 1 ∙ var 0 / 0 ]))) ∙ SZ
  →⟨⟩
    (ƛ (ƛ (ƛ (var 2 ∙ var 1 ∙ var 0)))) ∙ SZ
  →⟨ β-ƛ-∙ ⟩
    (ƛ (ƛ (var 2 ∙ var 1 ∙ var 0))) [ SZ / 0 ]
  →⟨⟩
    ƛ (ƛ (var 2 ∙ var 1 ∙ var 0) [ SZ / 2 ])
  →⟨⟩
    ƛ (ƛ lift 0 2 SZ ∙ var 1 ∙ var 0)
  →⟨⟩
    ƛ (ƛ (ƛ ƛ var 1 ∙ var 0) ∙ var 1 ∙ var 0)
  →⟨ β-ƛ (β-ƛ (β-∙-l β-ƛ-∙)) ⟩
    ƛ (ƛ (ƛ var 1 ∙ var 0) [ var 1 / 0 ] ∙ var 0)
  →⟨⟩
    ƛ (ƛ (ƛ ((var 1 ∙ var 0) [ var 1 / 1 ])) ∙ var 0)
  →⟨⟩
    ƛ (ƛ (ƛ ((var 1) [ var 1 / 1 ] ∙ (var 0) [ var 1 / 1 ])) ∙ var 0)
  →⟨⟩
    ƛ (ƛ (ƛ (lift 0 1 (var 1) ∙ var 0)) ∙ var 0)
  →⟨⟩
    ƛ (ƛ (ƛ (var 2 ∙ var 0)) ∙ var 0)
  →⟨ β-ƛ (β-ƛ β-ƛ-∙) ⟩
    ƛ (ƛ (var 2 ∙ var 0) [ var 0 / 0 ])
  →⟨⟩
    ƛ (ƛ (var 2) [ var 0 / 0 ] ∙ var 0)
  →⟨⟩
    ƛ (ƛ var 1 ∙ var 0)
  ∎

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
module Data.Num.Digit where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra
open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤; toℕ; zero; suc)
open import Data.Fin.Properties as FinProps using (bounded; toℕ-fromℕ≤)

open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

--------------------------------------------------------------------------------
-- Digits
--------------------------------------------------------------------------------

Digit : ℕ → Set
Digit = Fin

-- converting to and from ℕ
Digit-toℕ : ∀ {d} → Digit d → ℕ → ℕ
Digit-toℕ x o = toℕ x + o

Digit-fromℕ : ∀ {d} → (n o : ℕ) → d + o ≥ n → Digit (suc d)
Digit-fromℕ {d} n o upper-bound with n ∸ o ≤? d
Digit-fromℕ {d} n o upper-bound | yes p = fromℕ≤ (s≤s p)
Digit-fromℕ {d} n o upper-bound | no ¬p = contradiction p ¬p
    where   p : n ∸ o ≤ d
            p = start
                    n ∸ o
                ≤⟨ ∸n-mono o upper-bound ⟩
                    (d + o) ∸ o
                ≈⟨ m+n∸n≡m d o ⟩
                    d
                □

Digit-fromℕ-toℕ : ∀ {d o}
    → (n : ℕ)
    → (lower-bound :     o ≤ n)
    → (upper-bound : d + o ≥ n)
    → Digit-toℕ (Digit-fromℕ {d} n o upper-bound) o ≡ n
Digit-fromℕ-toℕ {d} {o} n lb ub with n ∸ o ≤? d
Digit-fromℕ-toℕ {d} {o} n lb ub | yes q =
    begin
        toℕ (fromℕ≤ (s≤s q)) + o
    ≡⟨ cong (λ x → x + o) (toℕ-fromℕ≤ (s≤s q)) ⟩
        n ∸ o + o
    ≡⟨ m∸n+n≡m lb ⟩
        n
    ∎
Digit-fromℕ-toℕ {d} {o} n lb ub | no ¬q = contradiction q ¬q
    where   q : n ∸ o ≤ d
            q = +n-mono-inverse o $
                start
                    n ∸ o + o
                ≈⟨ m∸n+n≡m lb ⟩
                    n
                ≤⟨ ub ⟩
                    d + o
                □

--------------------------------------------------------------------------------
-- Properties of all Digits
--------------------------------------------------------------------------------

Digit-upper-bound : ∀ {d} → (o : ℕ) → (x : Digit d) → Digit-toℕ x o < d + o
Digit-upper-bound {d} o x = +n-mono o (bounded x)

Digit-lower-bound : ∀ {d} → (o : ℕ) → (x : Digit d) → Digit-toℕ x o ≥ o
Digit-lower-bound {d} o x = n≤m+n (toℕ x) o

--------------------------------------------------------------------------------
-- Special Digits
--------------------------------------------------------------------------------

-- A digit at its greatest
Greatest : ∀ {d} (x : Digit d) → Set
Greatest {d} x = suc (toℕ x) ≡ d

Greatest? : ∀ {d} (x : Digit d) → Dec (Greatest x)
Greatest? {d} x = suc (toℕ x) ≟ d

greatest-digit : ∀ d → Digit (suc d)
greatest-digit d = Fin.fromℕ d

greatest-digit-toℕ : ∀ {d o}
    → (x : Digit (suc d))
    → Greatest x
    → Digit-toℕ x o ≡ d + o
greatest-digit-toℕ {d} {o} x greatest = cancel-suc $
    begin
        suc (Digit-toℕ x o)
    ≡⟨ cong (λ w → w + o) greatest ⟩
        suc (d + o)
    ∎

greatest-of-all : ∀ {d} (o : ℕ) → (x y : Digit d) → Greatest x → Digit-toℕ x o ≥ Digit-toℕ y o
greatest-of-all o zero    zero     refl = ≤-refl
greatest-of-all o zero    (suc ()) refl
greatest-of-all o (suc x) zero     greatest = +n-mono o {zero} {suc (toℕ x)} z≤n
greatest-of-all o (suc x) (suc y)  greatest = s≤s (greatest-of-all o x y (cancel-suc greatest))

greatest-digit-is-the-Greatest : ∀ d → Greatest (greatest-digit d)
greatest-digit-is-the-Greatest d = cong suc (FinProps.to-from d)

-- carry, 1 `max` o, in case that the least digit "o" is 0
carry : ℕ → ℕ
carry o = 1 ⊔ o

carry-lower-bound : ∀ {o} → carry o ≥ o
carry-lower-bound {o} = m≤n⊔m o 1

carry-upper-bound : ∀ {d o} → 2 ≤ suc d + o → carry o ≤ d + o
carry-upper-bound {d} {zero}  proper = ≤-pred proper
carry-upper-bound {d} {suc o} proper = n≤m+n d (suc o)

carry-digit : ∀ d o → 2 ≤ suc d + o → Digit (suc d)
carry-digit d o proper = Digit-fromℕ (carry o) o (carry-upper-bound {d} proper)

carry-digit-toℕ : ∀ d o
    → (proper : 2 ≤ suc (d + o))
    → Digit-toℕ (carry-digit d o proper) o ≡ carry o
carry-digit-toℕ d o proper = Digit-fromℕ-toℕ (carry o) (m≤n⊔m o 1) (carry-upper-bound {d} proper)

-- LCD-upper-bound-prim d zero    proper = ≤-pred proper
-- LCD-upper-bound-prim d (suc o) proper = n≤m+n (suc o) d
--
-- LCD : ∀ d o → 2 ≤ suc d + o → Digit (suc d)
-- LCD d o proper = Digit-fromℕ (1 ⊔ o) o (LCD-upper-bound-prim d o proper)
--
-- LCD-toℕ : ∀ d o
--     → (proper : 2 ≤ suc (d + o))
--     → Digit-toℕ (LCD d o proper) o ≡ 1 ⊔ o
-- LCD-toℕ d o proper = Digit-fromℕ-toℕ (1 ⊔ o) (m≤n⊔m o 1) (LCD-upper-bound-prim d o proper)
--
-- LCD-upper-bound : ∀ {d o}
--     → (proper : 2 ≤ suc (d + o))
--     → Digit-toℕ (LCD d o proper) o ≤ d + o
-- LCD-upper-bound {d} {o} proper =
--     start
--         Digit-toℕ (LCD d o proper) o
--     ≈⟨ LCD-toℕ d o proper ⟩
--         1 ⊔ o
--     ≤⟨ LCD-upper-bound-prim d o proper ⟩
--         d + o
--     □

--------------------------------------------------------------------------------
-- Functions on Digits
--------------------------------------------------------------------------------

-- +1
digit+1 : ∀ {d} → (x : Digit d) → (¬greatest : ¬ (Greatest x)) → Fin d
digit+1 x ¬greatest = fromℕ≤ {suc (toℕ x)} (≤∧≢⇒< (bounded x) ¬greatest)

digit+1-toℕ : ∀ {d o}
    → (x : Digit d)
    → (¬greatest : ¬ (Greatest x))
    → Digit-toℕ (digit+1 x ¬greatest) o ≡ suc (Digit-toℕ x o)
digit+1-toℕ {d} {o} x ¬greatest =
    begin
        Digit-toℕ (digit+1 x ¬greatest) o
    ≡⟨ cong (λ w → w + o) (toℕ-fromℕ≤ (≤∧≢⇒< (bounded x) ¬greatest)) ⟩
        suc (Digit-toℕ x o)
    ∎

digit+1-n-lemma : ∀ {d}
    → (x : Digit d)
    → Greatest x
    → (n : ℕ)
    → n > 0
    → suc (toℕ x) ∸ n < d
digit+1-n-lemma {zero } () greatest n n>0
digit+1-n-lemma {suc d} x greatest n n>0 = s≤s $ start
        suc (toℕ x) ∸ n
    ≤⟨ ∸n-mono n (bounded x) ⟩
        suc d ∸ n
    ≤⟨ n∸-mono (suc d) n>0 ⟩
        suc d ∸ 1
    ≤⟨ ≤-refl ⟩
        d
    □

-- +1 and then -n, useful for handling carrying on increment
digit+1-n : ∀ {d}
    → (x : Digit d)
    → Greatest x
    → (n : ℕ)
    → n > 0
    → Digit d
digit+1-n x greatest n n>0 = fromℕ≤ (digit+1-n-lemma x greatest n n>0)

digit+1-n-toℕ : ∀ {d o}
    → (x : Digit d)
    → (greatest : Greatest x)
    → (n : ℕ)
    → (n>0 : n > 0)
    → n ≤ d
    → Digit-toℕ (digit+1-n x greatest n n>0) o ≡ suc (Digit-toℕ x o) ∸ n
digit+1-n-toℕ {zero}  {o} () greatest n n>0 n≤d
digit+1-n-toℕ {suc d} {o} x greatest n n>0  n≤d =
    begin
        toℕ (digit+1-n x greatest n n>0) + o
    ≡⟨ cong (λ w → w + o) (toℕ-fromℕ≤ (digit+1-n-lemma x greatest n n>0)) ⟩
        suc (toℕ x) ∸ n + o
    ≡⟨ +-comm (suc (toℕ x) ∸ n) o ⟩
        o + (suc (toℕ x) ∸ n)
    ≡⟨ sym (+-∸-assoc o {suc (toℕ x)} {n} $
        start
            n
        ≤⟨ n≤d ⟩
            suc d
        ≈⟨ sym greatest ⟩
            suc (toℕ x)
        □)
    ⟩
        (o + suc (toℕ x)) ∸ n
    ≡⟨ cong (λ w → w ∸ n) (+-comm o (suc (toℕ x))) ⟩
        suc (toℕ x) + o ∸ n
    ∎

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module IID-Proof-Setup where

open import LF
open import Identity
open import IID
open import IIDr
open import DefinitionalEquality

OPg : Set -> Set1
OPg I = OP I I

-- Encoding indexed inductive types as non-indexed types.
ε : {I : Set}(γ : OPg I) -> OPr I
ε (ι i)     j = σ (i == j) (\_ -> ι ★)
ε (σ A γ)   j = σ A (\a -> ε (γ a) j)
ε (δ H i γ) j = δ H i (ε γ j)

-- Adds a reflexivity proof.
g→rArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (a : Args γ U) ->
	      rArgs (ε γ) U (index γ U a)
g→rArgs (ι e)     U arg	= (refl , ★)
g→rArgs (σ A γ)   U arg = (π₀ arg , g→rArgs (γ (π₀ arg)) U (π₁ arg))
g→rArgs (δ H i γ) U arg = (π₀ arg , g→rArgs γ U (π₁ arg))

-- Strips the equality proof.
r→gArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (i : I)(a : rArgs (ε γ) U i) ->
	      Args γ U
r→gArgs (ι i)     U j _	  = ★
r→gArgs (σ A γ)   U j arg = (π₀ arg , r→gArgs (γ (π₀ arg)) U j (π₁ arg))
r→gArgs (δ H i γ) U j arg = (π₀ arg , r→gArgs γ U j (π₁ arg))

-- Converting an rArgs to a gArgs and back is (provably, not definitionally)
-- the identity.
r←→gArgs-subst :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (C : (i : I) -> rArgs (ε γ) U i -> Set)
  (i : I)(a : rArgs (ε γ) U i) ->
  (C (index γ U (r→gArgs γ U i a))
     (g→rArgs γ U (r→gArgs γ U i a))
  ) -> C i a

r←→gArgs-subst {I} (ι i) U C j arg m =
  elim== i (\k q -> C k (q , ★)) m j (π₀ arg)

r←→gArgs-subst (σ A γ)   U C j arg m =
  r←→gArgs-subst (γ (π₀ arg)) U (\i c -> C i (π₀ arg , c)) j (π₁ arg) m

r←→gArgs-subst (δ H i γ) U C j arg m =
  r←→gArgs-subst γ U (\i c -> C i (π₀ arg , c)) j (π₁ arg) m

-- r←→gArgs-subst eliminates the identity proof stored in the rArgs. If this proof is
-- by reflexivity r←→gArgs-subst is a definitional identity. This is the case
-- when a = g→rArgs a'
r←→gArgs-subst-identity :
  {I  : Set}(γ : OPg I)(U : I -> Set)
  (C  : (i : I) -> rArgs (ε γ) U i -> Set)
  (a' : Args γ U) ->
  let a = g→rArgs γ U a'
      i = index γ U a' in
  (h : C (index γ U (r→gArgs γ U i a))
	 (g→rArgs γ U (r→gArgs γ U i a))
  ) -> r←→gArgs-subst γ U C i a h ≡ h
r←→gArgs-subst-identity (ι i)	  U C _   h = refl-≡
r←→gArgs-subst-identity (σ A γ)	  U C arg h = r←→gArgs-subst-identity (γ (π₀ arg)) U C' (π₁ arg) h
  where C' = \i c -> C i (π₀ arg , c)
r←→gArgs-subst-identity (δ H i γ) U C arg h = r←→gArgs-subst-identity γ U C' (π₁ arg) h
  where C' = \i c -> C i (π₀ arg , c)

-- Going the other way around is definitionally the identity.
g←→rArgs-identity :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (a : Args γ U) ->
  r→gArgs γ U (index γ U a) (g→rArgs γ U a) ≡ a
g←→rArgs-identity (ι i)	    U _	  = refl-≡
g←→rArgs-identity (σ A γ)   U arg = cong-≡ (\ ∙ -> (π₀ arg , ∙)) (g←→rArgs-identity (γ (π₀ arg)) U (π₁ arg))
g←→rArgs-identity (δ H i γ) U arg = cong-≡ (\ ∙ -> (π₀ arg , ∙)) (g←→rArgs-identity γ U (π₁ arg))

-- Corresponding conversion functions for assumptions to inductive occurrences.
-- Basically an identity function.
g→rIndArg : {I : Set}(γ : OPg I)(U : I -> Set)
        (i : I)(a : rArgs (ε γ) U i) ->
        IndArg γ U (r→gArgs γ U i a) -> IndArg (ε γ i) U a
g→rIndArg (ι j)	    U i _ ()
g→rIndArg (σ A γ)   U i arg v       = g→rIndArg (γ (π₀ arg)) U i (π₁ arg) v
g→rIndArg (δ A j γ) U i arg (inl a) = inl a
g→rIndArg (δ A j γ) U i arg (inr v) = inr (g→rIndArg γ U i (π₁ arg) v)

-- Basically we can substitute general inductive occurences for the encoded
-- restricted inductive occurrences.
g→rIndArg-subst :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i)
    (v : IndArg γ U (r→gArgs γ U i a)) ->
    C (IndIndex (ε γ i) U a (g→rIndArg γ U i a v))
      (Ind	(ε γ i) U a (g→rIndArg γ U i a v)) ->
    C (IndIndex γ U (r→gArgs γ U i a) v)
      (Ind	γ U (r→gArgs γ U i a) v)
g→rIndArg-subst (ι j)	  U C i _ ()	    h
g→rIndArg-subst (σ A γ)	  U C i arg v	    h = g→rIndArg-subst (γ (π₀ arg)) U C i (π₁ arg) v h
g→rIndArg-subst (δ A j γ) U C i arg (inl a) h = h
g→rIndArg-subst (δ A j γ) U C i arg (inr v) h = g→rIndArg-subst γ U C i (π₁ arg) v h

-- g→rIndArg-subst is purely book-keeping. On the object level it's definitional identity.
g→rIndArg-subst-identity :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i)
    (v : IndArg γ U (r→gArgs γ U i a))
    (h : C (IndIndex (ε γ i) U a (g→rIndArg γ U i a v))
	   (Ind	(ε γ i) U a (g→rIndArg γ U i a v))
    ) -> g→rIndArg-subst γ U C i a v h ≡ h
g→rIndArg-subst-identity (ι j)	   U C i _   ()	   h
g→rIndArg-subst-identity (σ A γ)   U C i arg v	   h =
  g→rIndArg-subst-identity (γ (π₀ arg)) U C i (π₁ arg) v h
g→rIndArg-subst-identity (δ A j γ) U C i arg (inl a) h = refl-≡
g→rIndArg-subst-identity (δ A j γ) U C i arg (inr v) h =
  g→rIndArg-subst-identity γ U C i (π₁ arg) v h

-- And finally conversion of induction hypotheses. This goes the other direction.
r→gIndHyp :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i) ->
    IndHyp (ε γ i) U C a -> IndHyp γ U C (r→gArgs γ U i a)
r→gIndHyp γ U C i a h v = g→rIndArg-subst γ U C i a v (h (g→rIndArg γ U i a v))

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Data.Boolean.Stmt where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Functional
open import Logic.Propositional
open import Type

IsTrue : Bool → Type
IsTrue = if_then ⊤ else ⊥

IsFalse : Bool → Type
IsFalse = IsTrue ∘ !

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module PathStructure.Coproduct {a b} {A : Set a} {B : Set b} where

open import Equivalence
open import PathOperations
open import Types

-- We need to use Lift here, because Agda doesn't have
-- cumulative universes.
F : A ⊎ B → A ⊎ B → Set (a ⊔ b)
F = case (λ _ → A ⊎ B → Set _)
  (λ a₁ → case (λ _ → Set _)
    (λ a₂ → Lift b (a₁ ≡ a₂))
    (λ _ → Lift _ ⊥))
  (λ b₁ → case (λ _ → Set _)
    (λ _ → Lift _ ⊥)
    (λ b₂ → Lift a (b₁ ≡ b₂)))

F-lemma : (x : A ⊎ B) → F x x
F-lemma = case (λ x → F x x) (λ _ → lift refl) (λ _ → lift refl)

split-path : {x y : A ⊎ B} → x ≡ y → F x y
split-path {x = x} p = tr (F x) p (F-lemma x)

merge-path : {x y : A ⊎ B} → F x y → x ≡ y
merge-path = case (λ x → ∀ y → F x y → x ≡ y)
  (λ a → case (λ y → F (inl a) y → inl a ≡ y)
    (λ _ → ap inl ∘ lower)
    (λ _ → 0-elim ∘ lower))
  (λ b → case (λ y → F (inr b) y → inr b ≡ y)
    (λ _ → 0-elim ∘ lower)
    (λ _ → ap inr ∘ lower))
  _ _

split-merge-eq : {x y : A ⊎ B} → (x ≡ y) ≃ F x y
split-merge-eq {x = x} {y = y}
  = split-path
  , (merge-path , λ f → case
      (λ x → ∀ y (f : F x y) → split-path (merge-path {x} {y} f) ≡ f)
      (λ a → case
        (λ y → (f : F (inl a) y) →
          split-path (merge-path {inl a} {y} f) ≡ f)
        (λ a′ p → J
          (λ a a′ p →
            split-path (merge-path {inl a} {inl a′} (lift p)) ≡ lift p)
          (λ _ → refl) _ _ (lower p))
        (λ _ → 0-elim ∘ lower))
      (λ b → case
        (λ y → (f : F (inr b) y) →
          split-path (merge-path {inr b} {y} f) ≡ f)
        (λ _ → 0-elim ∘ lower)
        (λ b′ p → J
          (λ b b′ p →
            split-path (merge-path {inr b} {inr b′} (lift p)) ≡ lift p)
          (λ _ → refl) _ _ (lower p)))
      x y f)
  , (merge-path , J (λ _ _ p → merge-path (split-path p) ≡ p)
      (case
        (λ x → merge-path {x} {x} (split-path {x} {x} refl) ≡ refl)
        (λ _ → refl)
        (λ _ → refl))
      _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module Lvl.Decidable where

open import Data.Boolean.Stmt
open import Logic.Propositional
open import Logic.Propositional.Theorems
import      Lvl
open import Type.Properties.Decidable
open import Type.Properties.Decidable.Proofs
open import Type

private variable ℓ ℓ₁ : Lvl.Level

-- Changing classical propositions' universe levels by using their boolean representation.
module _ (P : Type{ℓ}) ⦃ dec : Decidable(0)(P) ⦄ where
  Convert : Type{ℓ₁}
  Convert = Lvl.Up(IsTrue(decide(0)(P)))

  -- LvlConvert is satisfied whenever its proposition is.
  Convert-correctness : P ↔ Convert{ℓ₁}
  Convert-correctness = [↔]-transitivity decider-true ([↔]-intro Lvl.Up.obj Lvl.up)


text:
module Formalization.LambdaCalculus.Semantics where

open import Data
open import Formalization.LambdaCalculus
open import Syntax.Number
open import Type

-- A value in the language of lambda calculus is a irreducible term by a standard reduction definition.
-- It can also be defined as terms that are lambda abstractions because an application of a lambda is supposed to be β-reducible.
data Value : Expression → Type{0} where
  instance abs : ∀{body : Term(1)} → Value(Abstract body)


text:
module Cutting where

open import Basics
open import Ix
open import All

record _|>_ (I O : Set) : Set1 where
  field
    Cuts   : O -> Set
    inners : {o : O} -> Cuts o -> List I

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

record Cutting {I O}(C : I |> O)(P : I -> Set)(o : O) : Set where
  constructor _8><_
  open _|>_ C
  field
    cut     : Cuts o
    pieces  : All P (inners cut)
infixr 3 _8><_
open Cutting public

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- You can transform functions out of discrete
-- categories into functors.
module Categories.Functor.Construction.FromDiscrete {o ℓ e} (𝒞 : Category o ℓ e) where

open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Category.Discrete
open import Categories.Functor using (Functor)

private
  module 𝒞 = Category 𝒞

open Category 𝒞
open 𝒞.HomReasoning

FromDiscrete : ∀ {o} {A : Set o} → (A → Obj) → Functor (Discrete A) 𝒞
FromDiscrete {o} {A = A} select = record
  { F₀ = select
  ; F₁ = λ { ≡.refl → id }
  ; identity = refl
  ; homomorphism = λ { {_} {_} {_} {≡.refl} {≡.refl} → sym identity² }
  ; F-resp-≈ = λ { ≡.refl → refl }
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Dimension.PartialWeakening.Soundness where

  open import Exception -- using (Except; left; right; _<$>_; _>>=_)
  open import Injective

  -- Semantics given by application to a name in Fin n

  apply : ∀ {n m} (f : PWeak n m) (i : Fin n) → Except E (Fin m)
  apply []       ()
  apply (e ∷ f)  zero    = left e
  apply (e ∷ f)  (suc i) = apply f i
  apply (lift f) zero    = right zero
  apply (lift f) (suc i) = suc <$> apply f i
  apply (weak f) i       = suc <$> apply f i

  -- Proof of injectivity wrt. semantics

  injective : ∀ {n m} (f : PWeak n m) (i j : Fin n) →
    let k = apply f i in
    let l = apply f j in
    IsDefined k → k ≡ l → i ≡ j
  injective []       ()
  injective (e ∷ f) zero    j        () p
  injective (e ∷ f) (suc i) zero     fi p with apply f i
  injective (e ∷ f) (suc i) zero     () p  | left _
  injective (e ∷ f) (suc i) zero     fi () | right a
  injective (e ∷ f) (suc i) (suc j)  fi p = cong suc (injective f i j fi p)
  injective (lift f) zero   zero     fi p = refl
  injective (lift f) zero   (suc j)  fi p with apply f j
  injective (lift f) zero   (suc j)  fi p | left  _ = ⊥-elim (right≢left p)
  injective (lift f) zero   (suc j)  fi p | right l = ⊥-elim (zero≢suc (right-injective _ _ p))
  injective (lift f) (suc i) zero    fi p with apply f i
  injective (lift f) (suc i) zero    fi p | left  e = ⊥-elim (left≢right p)
  injective (lift f) (suc i) zero    fi p | right k = ⊥-elim (suc≢zero (right-injective _ _ p))
  injective (lift f) (suc i) (suc j) fi p = cong suc (injective f i j (map-def-inv _ fi) (map-injective suc-injective _ _ p))
  injective (weak f) i       j       fi p = injective f i j (map-def-inv _ fi) (map-injective suc-injective _ _ p)

  -- Soundness of id

  apply-id : ∀ n (i : Fin n) → apply id i ≡ return i
  apply-id 0       ()
  apply-id (suc n) zero    = refl
  apply-id (suc n) (suc i) with (apply id i) | (apply-id n i)
  apply-id (suc n) (suc i) | .(right i) | refl = refl

  -- Lemma: one inductive step

  lift-lift-suc : ∀ {n m l} (f : PWeak n m) {g : PWeak m l} {i : Fin n} →

    (ih : apply (comp f g) i ≡ apply f i >>= apply g) →

    apply (comp (lift f) (lift g)) (suc i)  ≡
    apply (lift f) (suc i) >>= apply (lift g)

  lift-lift-suc f {g = g} {i = i} ih = begin

      apply (comp (lift f) (lift g)) (suc i)

    ≡⟨⟩                                      -- definition of comp

      apply (lift (comp f g)) (suc i)

    ≡⟨⟩                                      -- definition of apply

      suc <$> apply (comp f g) i

    ≡⟨ cong (_<$>_ suc) ih ⟩                 -- induction hypothesis

      suc <$> (apply f i >>= apply g)

    ≡⟨ map-after-bind (apply f i) ⟩          -- map commutes with bind I

      (apply f i >>= λ j → suc <$> apply g j)

    ≡⟨⟩                                      -- definition of apply

      (apply f i >>= λ j → apply (lift g) (suc j))

    ≡⟨ sym (bind-after-map (apply f i)) ⟩    -- map commutes with bind II

      (suc <$> apply f i) >>= apply (lift g)

    ≡⟨⟩                                      -- definition of apply

      apply (lift f) (suc i) >>= apply (lift g)
    ∎

  -- Soundness of comp

  apply-comp : ∀ {n m l} (f : PWeak n m) (g : PWeak m l) (i : Fin n) →
    apply (comp f g) i ≡ apply f i >>= apply g
  apply-comp [] g ()
  apply-comp (e ∷ f) g zero = refl
  apply-comp (e ∷ f) g (suc i) = apply-comp f g i
--  apply-comp (lift f) (e ∷ g) i = {!!}
  apply-comp (lift f) (e ∷ g) zero = refl
  apply-comp (lift f) (e ∷ g) (suc i) with apply f i
  apply-comp (lift f) (e ∷ g) (suc i) | left e′ = {!!}
  apply-comp (lift f) (e ∷ g) (suc i) | right a = {!!}
  apply-comp (lift f) (lift g) zero = refl
  apply-comp (lift f) (lift g) (suc i) = lift-lift-suc f (apply-comp f g i)
  apply-comp (lift f) (weak g) i = begin

      suc <$> apply (comp (lift f) g) i

    ≡⟨ cong (_<$>_ suc) (apply-comp (lift f) g i) ⟩  -- ind. hyp.

      suc <$> (apply (lift f) i >>= apply g)

    ≡⟨ map-after-bind (apply (lift f) i) ⟩           -- move map

      apply (lift f) i >>= (λ j → suc <$> apply g j)
    ∎
  apply-comp (weak f) g i = {!!}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


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

module Examples.Exp2 where

open import Calf.CostMonoid
open import Calf.CostMonoids using (ℕ²-ParCostMonoid)

parCostMonoid = ℕ²-ParCostMonoid
open ParCostMonoid parCostMonoid

open import Calf costMonoid
open import Calf.ParMetalanguage parCostMonoid
open import Calf.Types.Bool
open import Calf.Types.Nat
open import Calf.Types.Bounded costMonoid
open import Calf.Types.BigO costMonoid

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning)
open import Data.Nat as Nat using (_+_; pred; _*_; _^_; _⊔_)
import Data.Nat.Properties as N
open import Data.Nat.PredExp2
open import Data.Product
open import Data.Empty

Correct : cmp (Π nat λ _ → F nat) → Set
Correct exp₂ = (n : ℕ) → ◯ (exp₂ n ≡ ret (2 ^ n))

module Slow where
  exp₂ : cmp (Π nat λ _ → F nat)
  exp₂ zero = ret (suc zero)
  exp₂ (suc n) =
    bind (F nat) (exp₂ n & exp₂ n) λ (r₁ , r₂) →
      step (F nat) (1 , 1) (ret (r₁ + r₂))

  exp₂/correct : Correct exp₂
  exp₂/correct zero    u = refl
  exp₂/correct (suc n) u =
    begin
      exp₂ (suc n)
    ≡⟨⟩
      (bind (F nat) (exp₂ n & exp₂ n) λ (r₁ , r₂) →
        step (F nat) (1 , 1) (ret (r₁ + r₂)))
    ≡⟨ Eq.cong (bind (F nat) (exp₂ n & exp₂ n)) (funext (λ (r₁ , r₂) → step/ext (F nat) _ (1 , 1) u)) ⟩
      (bind (F nat) (exp₂ n & exp₂ n) λ (r₁ , r₂) →
        ret (r₁ + r₂))
    ≡⟨ Eq.cong (λ e → bind (F nat) (e & e) _) (exp₂/correct n u) ⟩
      step (F nat) (𝟘 ⊗ 𝟘) (ret (2 ^ n + 2 ^ n))
    ≡⟨⟩
      ret (2 ^ n + 2 ^ n)
    ≡⟨ Eq.cong ret (lemma/2^suc n) ⟩
      ret (2 ^ suc n)
    ∎
      where open ≡-Reasoning

  exp₂/cost : cmp (Π nat λ _ → cost)
  exp₂/cost zero    = 𝟘
  exp₂/cost (suc n) =
    bind cost (exp₂ n & exp₂ n) λ (r₁ , r₂) → (exp₂/cost n ⊗ exp₂/cost n) ⊕
      ((1 , 1) ⊕ 𝟘)

  exp₂/cost/closed : cmp (Π nat λ _ → cost)
  exp₂/cost/closed n = pred[2^ n ] , n

  exp₂/cost≤exp₂/cost/closed : ∀ n → ◯ (exp₂/cost n ≤ exp₂/cost/closed n)
  exp₂/cost≤exp₂/cost/closed zero    u = ≤-refl
  exp₂/cost≤exp₂/cost/closed (suc n) u =
    let ≡ = exp₂/correct n u in
    let open ≤-Reasoning in
    begin
      exp₂/cost (suc n)
    ≡⟨⟩
      (bind cost (exp₂ n & exp₂ n) λ (r₁ , r₂) → (exp₂/cost n ⊗ exp₂/cost n) ⊕
        ((1 , 1) ⊕ 𝟘))
    ≡⟨ Eq.cong₂ (λ e₁ e₂ → bind cost (e₁ & e₂) λ (r₁ , r₂) → (exp₂/cost n ⊗ exp₂/cost n) ⊕ _) (≡) (≡) ⟩
      (exp₂/cost n ⊗ exp₂/cost n) ⊕ ((1 , 1) ⊕ 𝟘)
    ≡⟨ Eq.cong ((exp₂/cost n ⊗ exp₂/cost n) ⊕_) (⊕-identityʳ _) ⟩
      (exp₂/cost n ⊗ exp₂/cost n) ⊕ (1 , 1)
    ≤⟨ ⊕-monoˡ-≤ (1 , 1) (⊗-mono-≤ (exp₂/cost≤exp₂/cost/closed n u) (exp₂/cost≤exp₂/cost/closed n u)) ⟩
      (exp₂/cost/closed n ⊗ exp₂/cost/closed n) ⊕ (1 , 1)
    ≡⟨ Eq.cong₂ _,_ arithmetic/work arithmetic/span ⟩
        exp₂/cost/closed (suc n)
      ∎
      where
        arithmetic/work : proj₁ (exp₂/cost/closed n ⊗ exp₂/cost/closed n ⊕ (1 , 1)) ≡ proj₁ (exp₂/cost/closed (suc n))
        arithmetic/work =
          begin
            proj₁ (exp₂/cost/closed n ⊗ exp₂/cost/closed n ⊕ (1 , 1))
          ≡⟨⟩
            proj₁ (exp₂/cost/closed n) + proj₁ (exp₂/cost/closed n) + 1
          ≡⟨ N.+-comm _ 1 ⟩
            suc (proj₁ (exp₂/cost/closed n) + proj₁ (exp₂/cost/closed n))
          ≡⟨⟩
            suc (pred[2^ n ] + pred[2^ n ])
          ≡⟨ pred[2^suc[n]] n ⟩
            pred[2^ suc n ]
          ≡⟨⟩
            proj₁ (exp₂/cost/closed (suc n))
          ∎
            where open ≡-Reasoning

        arithmetic/span : proj₂ (exp₂/cost/closed n ⊗ exp₂/cost/closed n ⊕ (1 , 1)) ≡ proj₂ (exp₂/cost/closed (suc n))
        arithmetic/span =
          begin
            proj₂ (exp₂/cost/closed n ⊗ exp₂/cost/closed n ⊕ (1 , 1))
          ≡⟨⟩
            proj₂ (exp₂/cost/closed n) ⊔ proj₂ (exp₂/cost/closed n) + 1
          ≡⟨⟩
            n ⊔ n + 1
          ≡⟨ Eq.cong (_+ 1) (N.⊔-idem n) ⟩
            n + 1
          ≡⟨ N.+-comm _ 1 ⟩
            suc n
          ≡⟨⟩
            proj₂ (exp₂/cost/closed (suc n))
          ∎
            where open ≡-Reasoning

  exp₂≤exp₂/cost : ∀ n → IsBounded nat (exp₂ n) (exp₂/cost n)
  exp₂≤exp₂/cost zero    = bound/ret
  exp₂≤exp₂/cost (suc n) =
    bound/bind (exp₂/cost n ⊗ exp₂/cost n) _ (bound/par (exp₂≤exp₂/cost n) (exp₂≤exp₂/cost n)) λ (r₁ , r₂) →
      bound/step (1 , 1) 𝟘 bound/ret

  exp₂≤exp₂/cost/closed : ∀ n → IsBounded nat (exp₂ n) (exp₂/cost/closed n)
  exp₂≤exp₂/cost/closed n = bound/relax (exp₂/cost≤exp₂/cost/closed n) (exp₂≤exp₂/cost n)

  exp₂/asymptotic : given nat measured-via (λ n → n) , exp₂ ∈𝓞(λ n → 2 ^ n , n)
  exp₂/asymptotic = 0 ≤n⇒f[n]≤g[n]via λ n _ → bound/relax (λ u → N.pred[n]≤n , N.≤-refl) (exp₂≤exp₂/cost/closed n)

module Fast where

  exp₂ : cmp (Π nat λ _ → F nat)
  exp₂ zero = ret (suc zero)
  exp₂ (suc n) =
    bind (F nat) (exp₂ n) λ r →
      step (F nat) (1 , 1) (ret (r + r))

  exp₂/correct : Correct exp₂
  exp₂/correct zero    u = refl
  exp₂/correct (suc n) u =
    begin
      exp₂ (suc n)
    ≡⟨⟩
      (bind (F nat) (exp₂ n) λ r →
        step (F nat) (1 , 1) (ret (r + r)))
    ≡⟨ Eq.cong (bind (F nat) (exp₂ n)) (funext (λ r → step/ext (F nat) _ (1 , 1) u)) ⟩
      (bind (F nat) (exp₂ n) λ r →
        ret (r + r))
    ≡⟨ Eq.cong (λ e → bind (F nat) e _) (exp₂/correct n u) ⟩
      (bind (F nat) (ret {nat} (2 ^ n)) λ r →
        ret (r + r))
    ≡⟨⟩
      ret (2 ^ n + 2 ^ n)
    ≡⟨ Eq.cong ret (lemma/2^suc n) ⟩
      ret (2 ^ suc n)
    ∎
      where open ≡-Reasoning

  exp₂/cost : cmp (Π nat λ _ → cost)
  exp₂/cost zero    = 𝟘
  exp₂/cost (suc n) =
    bind cost (exp₂ n) λ r → exp₂/cost n ⊕
      ((1 , 1) ⊕ 𝟘)

  exp₂/cost/closed : cmp (Π nat λ _ → cost)
  exp₂/cost/closed n = n , n

  exp₂/cost≤exp₂/cost/closed : ∀ n → ◯ (exp₂/cost n ≤ exp₂/cost/closed n)
  exp₂/cost≤exp₂/cost/closed zero    u = ≤-refl
  exp₂/cost≤exp₂/cost/closed (suc n) u =
    let open ≤-Reasoning in
    begin
      exp₂/cost (suc n)
    ≡⟨⟩
      (bind cost (exp₂ n) λ r → exp₂/cost n ⊕
        ((1 , 1) ⊕ 𝟘))
    ≡⟨ Eq.cong (λ e → bind cost e λ r → exp₂/cost n ⊕ _) (exp₂/correct n u) ⟩
      exp₂/cost n ⊕ ((1 , 1) ⊕ 𝟘)
    ≤⟨ ⊕-monoˡ-≤ ((1 , 1) ⊕ 𝟘) (exp₂/cost≤exp₂/cost/closed n u) ⟩
      exp₂/cost/closed n ⊕ ((1 , 1) ⊕ 𝟘)
    ≡⟨ Eq.cong (exp₂/cost/closed n ⊕_) (⊕-identityʳ _) ⟩
      exp₂/cost/closed n ⊕ (1 , 1)
    ≡⟨ Eq.cong₂ _,_ (N.+-comm _ 1) (N.+-comm _ 1) ⟩
      exp₂/cost/closed (suc n)
    ∎

  exp₂≤exp₂/cost : ∀ n → IsBounded nat (exp₂ n) (exp₂/cost n)
  exp₂≤exp₂/cost zero    = bound/ret
  exp₂≤exp₂/cost (suc n) =
    bound/bind (exp₂/cost n) _ (exp₂≤exp₂/cost n) λ r →
      bound/step (1 , 1) 𝟘 bound/ret

  exp₂≤exp₂/cost/closed : ∀ n → IsBounded nat (exp₂ n) (exp₂/cost/closed n)
  exp₂≤exp₂/cost/closed n = bound/relax (exp₂/cost≤exp₂/cost/closed n) (exp₂≤exp₂/cost n)

  exp₂/asymptotic : given nat measured-via (λ n → n) , exp₂ ∈𝓞(λ n → n , n)
  exp₂/asymptotic = 0 ≤n⇒f[n]≤ 1 g[n]via λ n _ → Eq.subst (IsBounded _ _) (Eq.sym (⊕-identityʳ _)) (exp₂≤exp₂/cost/closed n)

slow≡fast : ◯ (Slow.exp₂ ≡ Fast.exp₂)
slow≡fast u = funext λ n →
  begin
    Slow.exp₂ n
  ≡⟨ Slow.exp₂/correct n u ⟩
    ret (2 ^ n)
  ≡˘⟨ Fast.exp₂/correct n u ⟩
    Fast.exp₂ n
  ∎
    where open ≡-Reasoning

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
------------------------------------------------------------------------
-- Semantics of the parsers
------------------------------------------------------------------------

module TotalParserCombinators.Semantics where

open import Codata.Musical.Notation
open import Data.List hiding (drop)
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe using (Maybe); open Data.Maybe.Maybe
open import Data.Product
open import Data.Unit using (⊤; tt)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_; module Equivalence)
open import Function.Inverse using (_↔_; module Inverse)
open import Function.Related as Related using (Related)
open import Level
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- Semantics

-- The semantics of the parsers. x ∈ p · s means that x can be the
-- result of applying the parser p to the string s. Note that the
-- semantics is defined inductively.

infix  60 <$>_
infixl 50 _⊛_   [_-_]_⊛_
infixl 10 _>>=_ [_-_]_>>=_
infix   4 _∈_·_

data _∈_·_ {Tok} :
       ∀ {R xs} → R → Parser Tok R xs → List Tok → Set₁ where
  return   : ∀ {R} {x : R} → x ∈ return x · []
  token    : ∀ {x} → x ∈ token · [ x ]
  ∣-left   : ∀ {R x xs₁ xs₂ s}
               {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
             (x∈p₁ : x ∈ p₁ · s) → x ∈ p₁ ∣ p₂ · s
  ∣-right  : ∀ {R x xs₂ s} xs₁
               {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
             (x∈p₂ : x ∈ p₂ · s) → x ∈ p₁ ∣ p₂ · s
  <$>_     : ∀ {R₁ R₂ x s xs} {p : Parser Tok R₁ xs} {f : R₁ → R₂}
             (x∈p : x ∈ p · s) → f x ∈ f <$> p · s
  _⊛_      : ∀ {R₁ R₂ f x s₁ s₂ fs xs}
               {p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)}
               {p₂ : ∞⟨ fs ⟩Parser Tok  R₁       (flatten xs)} →
             (f∈p₁ : f ∈ ♭? p₁ · s₁)
             (x∈p₂ : x ∈ ♭? p₂ · s₂) →
             f x ∈ p₁ ⊛ p₂ · s₁ ++ s₂
  _>>=_    : ∀ {R₁ R₂ x y s₁ s₂ xs} {f : Maybe (R₁ → List R₂)}
               {p₁ : ∞⟨ f ⟩Parser Tok R₁ (flatten xs)}
               {p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)}
             (x∈p₁ : x ∈ ♭? p₁ · s₁)
             (y∈p₂x : y ∈ ♭? (p₂ x) · s₂) →
             y ∈ p₁ >>= p₂ · s₁ ++ s₂
  nonempty : ∀ {R xs x y s} {p : Parser Tok R xs}
             (x∈p : y ∈ p · x ∷ s) → y ∈ nonempty p · x ∷ s
  cast     : ∀ {R xs₁ xs₂ x s}
               {xs₁≈xs₂ : xs₁ List-∼[ bag ] xs₂} {p : Parser Tok R xs₁}
             (x∈p : x ∈ p · s) → x ∈ cast xs₁≈xs₂ p · s

-- Some variants with fewer implicit arguments. (The arguments xs and
-- fs can usually not be inferred, but I do not want to mention them
-- in the paper, so I have made them implicit in the definition
-- above.)

[_-_]_⊛_ : ∀ {Tok R₁ R₂ f x s₁ s₂} xs fs
             {p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)}
             {p₂ : ∞⟨ fs ⟩Parser Tok  R₁       (flatten xs)} →
           f ∈ ♭? p₁ · s₁ → x ∈ ♭? p₂ · s₂ → f x ∈ p₁ ⊛ p₂ · s₁ ++ s₂
[ xs - fs ] f∈p₁ ⊛ x∈p₂ = _⊛_ {fs = fs} {xs = xs} f∈p₁ x∈p₂

[_-_]_>>=_ : ∀ {Tok R₁ R₂ x y s₁ s₂} (f : Maybe (R₁ → List R₂)) xs
               {p₁ : ∞⟨ f ⟩Parser Tok R₁ (flatten xs)}
               {p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)} →
             x ∈ ♭? p₁ · s₁ → y ∈ ♭? (p₂ x) · s₂ →
             y ∈ p₁ >>= p₂ · s₁ ++ s₂
[ f - xs ] x∈p₁ >>= y∈p₂x = _>>=_ {xs = xs} {f = f} x∈p₁ y∈p₂x

------------------------------------------------------------------------
-- Parser and language equivalence

infix 4 _∼[_]_ _≈_ _≅_ _≲_

-- There are two kinds of equivalences. Parser equivalences are
-- stronger, and correspond to bag equality. Language equivalences are
-- weaker, and correspond to set equality.

open Data.List.Relation.Binary.BagAndSetEquality public
  using (Kind)
  renaming ( bag      to parser
           ; set      to language
           ; subbag   to subparser
           ; subset   to sublanguage
           ; superbag to superparser
           ; superset to superlanguage
           )

-- General definition of equivalence between parsers. (Note that this
-- definition also gives access to some ordering relations.)

_∼[_]_ : ∀ {Tok R xs₁ xs₂} →
         Parser Tok R xs₁ → Kind → Parser Tok R xs₂ → Set₁
p₁ ∼[ k ] p₂ = ∀ {x s} → Related k (x ∈ p₁ · s) (x ∈ p₂ · s)

-- Language equivalence. (Corresponds to set equality.)

_≈_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≈ p₂ = p₁ ∼[ language ] p₂

-- Parser equivalence. (Corresponds to bag equality.)

_≅_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≅ p₂ = p₁ ∼[ parser ] p₂

-- p₁ ≲ p₂ means that the language defined by p₂ contains all the
-- string/result pairs contained in the language defined by p₁.

_≲_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≲ p₂ = p₁ ∼[ sublanguage ] p₂

-- p₁ ≈ p₂ iff both p₁ ≲ p₂ and p₂ ≲ p₁.

≈⇔≲≳ : ∀ {Tok R xs₁ xs₂}
         {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
       p₁ ≈ p₂ ⇔ (p₁ ≲ p₂ × p₂ ≲ p₁)
≈⇔≲≳ = Eq.equivalence
  (λ p₁≈p₂  →
     ((λ {x s} → _⟨$⟩_ (Equivalence.to   (p₁≈p₂ {x = x} {s = s})))
     , λ {x s} → _⟨$⟩_ (Equivalence.from (p₁≈p₂ {x = x} {s = s}))))
  (λ p₁≲≳p₂ → λ {x s} → Eq.equivalence (proj₁ p₁≲≳p₂ {s = s})
                                       (proj₂ p₁≲≳p₂ {s = s}))

-- Parser equivalence implies language equivalence.

≅⇒≈ : ∀ {Tok R xs₁ xs₂}
        {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
      p₁ ≅ p₂ → p₁ ≈ p₂
≅⇒≈ p₁≅p₂ = Related.↔⇒ p₁≅p₂

-- Language equivalence does not (in general) imply parser
-- equivalence.

¬≈⇒≅ : ¬ (∀ {Tok R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
          p₁ ≈ p₂ → p₁ ≅ p₂)
¬≈⇒≅ hyp with Inverse.injective p₁≅p₂
                {∣-left return} {∣-right [ tt ] return} (lemma _ _)
  where
  p₁ : Parser ⊤ ⊤ _
  p₁ = return tt ∣ return tt

  p₂ : Parser ⊤ ⊤ _
  p₂ = return tt

  p₁≲p₂ : p₁ ≲ p₂
  p₁≲p₂ (∣-left     return) = return
  p₁≲p₂ (∣-right ._ return) = return

  p₁≅p₂ : p₁ ≅ p₂
  p₁≅p₂ = hyp $ Eq.equivalence p₁≲p₂ ∣-left

  lemma : ∀ {x s} (x∈₁ x∈₂ : x ∈ p₂ · s) → x∈₁ ≡ x∈₂
  lemma return return = P.refl

... | ()

------------------------------------------------------------------------
-- A simple cast lemma

cast∈ : ∀ {Tok R xs} {p p′ : Parser Tok R xs} {x x′ s s′} →
        x ≡ x′ → p ≡ p′ → s ≡ s′ → x ∈ p · s → x′ ∈ p′ · s′
cast∈ P.refl P.refl P.refl x∈ = x∈

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Agda should warn if a coinductive record is declared but neither
-- --guardedness nor --sized-types is enabled.

record R : Set where
  coinductive
  field
    r : R


text:
{-# OPTIONS --safe --no-qualified-instances #-}
{- Noop removal transformation on bytecode -}
module JVM.Transform.Noooops where

open import Data.Product
open import Data.Sum
open import Function using (case_of_)
open import Data.List
open import Relation.Unary hiding (Empty)
open import Relation.Binary.Structures
open import Relation.Binary.PropositionalEquality using (refl; _≡_)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax hiding (_∣_)

open import JVM.Types
open import JVM.Model StackTy
open import JVM.Syntax.Instructions

open import Relation.Ternary.Data.ReflexiveTransitive {{intf-rel}}

open IsEquivalence {{...}} using (sym)
open import Data.Maybe using (just; nothing; Maybe)

is-noop : ∀[ ⟨ 𝑭 ∣ ψ₁ ↝ ψ₂ ⟩ ⇒ (Empty (ψ₁ ≡ ψ₂) ∪ U) ]
is-noop noop = inj₁ (emp refl)
is-noop _    = inj₂ _

noooop : ∀[ ⟪ 𝑭 ∣ ψ₁ ↝ ψ₂ ⟫ ⇒ ⟪ 𝑭 ∣ ψ₁ ↝ ψ₂ ⟫ ]
noooop nil = nil

-- (1) not labeled
noooop (cons (instr (↓ i) ∙⟨ σ ⟩ is)) =
  case (is-noop i) of λ where
    (inj₂ _)          → instr (↓ i) ▹⟨ σ ⟩ noooop is
    (inj₁ (emp refl)) → coe (∙-id⁻ˡ σ) (noooop is)

-- (2) is labeled
noooop (cons (li@(labeled (l ∙⟨ σ₀ ⟩ ↓ i)) ∙⟨ σ ⟩ is)) =
  case (is-noop i) of λ where
    (inj₂ _)          → cons (li ∙⟨ σ ⟩ noooop is)
    (inj₁ (emp refl)) → label-start noop l ⟨ coe {{∙-respects-≈ˡ}} (≈-sym (∙-id⁻ʳ σ₀)) σ ⟩ (noooop is)


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

module Definition.Typed.Consequences.Equality where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

U≡A′ : ∀ {A Γ l} ([U] : Γ ⊩⟨ l ⟩U)
    → Γ ⊩⟨ l ⟩ U ≡ A / (U-intr [U])
    → A PE.≡ U
U≡A′ (noemb [U]) (U₌ [U≡A]) = [U≡A]
U≡A′ (emb 0<1 [U]) (ιx [U≡A]) = U≡A′ [U] [U≡A]

-- If A is judgmentally equal to U, then A is propsitionally equal to U.
U≡A : ∀ {A Γ}
    → Γ ⊢ U ≡ A
    → A PE.≡ U
U≡A {A} U≡A with reducibleEq U≡A
U≡A {A} U≡A | [U] , [A] , [U≡A] =
  U≡A′ (U-elim [U]) (irrelevanceEq [U] (U-intr (U-elim [U])) [U≡A])

ℕ≡A′ : ∀ {A Γ l} ([ℕ] : Γ ⊩⟨ l ⟩ℕ ℕ)
    → Γ ⊩⟨ l ⟩ ℕ ≡ A / (ℕ-intr [ℕ])
    → Whnf A
    → A PE.≡ ℕ
ℕ≡A′ (noemb x) (ιx (ℕ₌ [ℕ≡A])) whnfA = whnfRed* [ℕ≡A] whnfA
ℕ≡A′ (emb 0<1 [ℕ]) (ιx [ℕ≡A]) whnfA = ℕ≡A′ [ℕ] [ℕ≡A] whnfA

-- If A in WHNF is judgmentally equal to ℕ, then A is propsitionally equal to ℕ.
ℕ≡A : ∀ {A Γ}
    → Γ ⊢ ℕ ≡ A
    → Whnf A
    → A PE.≡ ℕ
ℕ≡A {A} ℕ≡A whnfA with reducibleEq ℕ≡A
ℕ≡A {A} ℕ≡A whnfA | [ℕ] , [A] , [ℕ≡A] =
  ℕ≡A′ (ℕ-elim [ℕ]) (irrelevanceEq [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [ℕ≡A]) whnfA

ne≡A′ : ∀ {A K Γ l}
     → ([K] : Γ ⊩⟨ l ⟩ne K)
     → Γ ⊩⟨ l ⟩ K ≡ A / (ne-intr [K])
     → Whnf A
     → ∃ λ M → Neutral M × A PE.≡ M
ne≡A′ (noemb [K]) (ιx (ne₌ M D′ neM K≡M)) whnfA =
  M , neM , (whnfRed* (red D′) whnfA)
ne≡A′ (emb 0<1 [K]) (ιx [K≡A]) whnfA = ne≡A′ [K] [K≡A] whnfA

-- If A in WHNF is judgmentally equal to K, then there exists a M such that
-- A is propsitionally equal to M.
ne≡A : ∀ {A K Γ}
    → Neutral K
    → Γ ⊢ K ≡ A
    → Whnf A
    → ∃ λ M → Neutral M × A PE.≡ M
ne≡A {A} neK ne≡A whnfA with reducibleEq ne≡A
ne≡A {A} neK ne≡A whnfA | [ne] , [A] , [ne≡A] =
  ne≡A′ (ne-elim neK [ne])
        (irrelevanceEq [ne] (ne-intr (ne-elim neK [ne])) [ne≡A]) whnfA

Π≡A′ : ∀ {A F G Γ l} ([Π] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
    → Γ ⊩⟨ l ⟩ Π F ▹ G ≡ A / (Π-intr [Π])
    → Whnf A
    → ∃₂ λ H E → A PE.≡ Π H ▹ E
Π≡A′ (noemb [Π]) (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) whnfA =
  F′ , G′ , whnfRed* D′ whnfA
Π≡A′ (emb 0<1 [Π]) (ιx [Π≡A]) whnfA = Π≡A′ [Π] [Π≡A] whnfA

-- If A is judgmentally equal to Π F ▹ G, then there exists H and E such that
-- A is propsitionally equal to  Π H ▹ E.
Π≡A : ∀ {A F G Γ}
    → Γ ⊢ Π F ▹ G ≡ A
    → Whnf A
    → ∃₂ λ H E → A PE.≡ Π H ▹ E
Π≡A {A} Π≡A whnfA with reducibleEq Π≡A
Π≡A {A} Π≡A whnfA | [Π] , [A] , [Π≡A] =
  Π≡A′ (Π-elim [Π]) (irrelevanceEq [Π] (Π-intr (Π-elim [Π])) [Π≡A]) whnfA

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

module Issue5470.Import where

open import Agda.Builtin.Nat

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

private
  postulate
    foo : Nat → Nat

bar : Nat → Nat
bar n = foo n

private
  postulate
    lemma : ∀ n → foo n ≡ n
  {-# REWRITE lemma #-}


text:
module ProposedSemantics where

open import Syntax public

-- Vindicative Kripke models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    World   : Set
    _≤_     : World → World → Set
    refl≤   : ∀ {w} → w ≤ w
    trans≤  : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″
    _R_     : World → World → Set
    reflR   : ∀ {w} → w R w
    transR  : ∀ {w w′ w″} → w R w′ → w′ R w″ → w R w″
    _⊩ᵅ_   : World → Atom → Set
    mono⊩ᵅ : ∀ {w w′ P} → w ≤ w′ → w ⊩ᵅ P → w′ ⊩ᵅ P

  -- Vindication, a consequence of brilliance and persistence.
  field
    ≤→R : ∀ {v′ w} → w ≤ v′ → w R v′

open Model {{…}} public

-- Forcing in a particular world of a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World → Type → Set
  w ⊩ α P    = w ⊩ᵅ P
  w ⊩ A ⇒ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
  w ⊩ □ A    = ∀ {v′} → w R v′ → v′ ⊩ A
  w ⊩ A ⩕ B  = w ⊩ A ∧ w ⊩ B
  w ⊩ ⫪     = ⊤
  w ⊩ ⫫     = ⊥
  w ⊩ A ⩖ B  = w ⊩ A ∨ w ⊩ B

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Stack Type → Set
  w ⊩⋆ ∅     = ⊤
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ ∧ w ⊩ A

-- Monotonicity of forcing with respect to constructive accessibility.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
  mono⊩ {α P}    ψ s       = mono⊩ᵅ ψ s
  mono⊩ {A ⇒ B} ψ f       = λ ψ′ a → f (trans≤ ψ ψ′) a
  mono⊩ {□ A}    ψ f       = λ ρ → f (transR (≤→R ψ) ρ)
  mono⊩ {A ⩕ B}  ψ (a , b) = mono⊩ {A} ψ a , mono⊩ {B} ψ b
  mono⊩ {⫪}     ψ ∙       = ∙
  mono⊩ {⫫}     ψ ()
  mono⊩ {A ⩖ B}  ψ (ι₁ a)  = ι₁ (mono⊩ {A} ψ a)
  mono⊩ {A ⩖ B}  ψ (ι₂ b)  = ι₂ (mono⊩ {B} ψ b)

  mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     ψ ∙       = ∙
  mono⊩⋆ {Ξ , A} ψ (ξ , s) = mono⊩⋆ {Ξ} ψ ξ , mono⊩ {A} ψ s

-- Additional equipment.

module _ {{_ : Model}} where
  lookup : ∀ {Ξ A w} → A ∈ Ξ → w ⊩⋆ Ξ → w ⊩ A
  lookup top     (ξ , s) = s
  lookup (pop i) (ξ , s) = lookup i ξ

-- Forcing in all worlds of all models, or semantic entailment.

infix 3 _⊨_
_⊨_ : Context → Type → Set₁
Γ ⁏ Δ ⊨ A = ∀ {{_ : Model}} {w} →
             w ⊩⋆ Γ →
             (∀ {v′} → w R v′ → v′ ⊩⋆ Δ) →
             w ⊩ A

-- Soundness of the semantics with respect to the syntax.

reflect : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊨ A
reflect (var i)      γ δ = lookup i γ
reflect (mvar i)     γ δ = lookup i (δ reflR)
reflect (lam d)      γ δ = λ ψ a → reflect d (mono⊩⋆ ψ γ , a)
                                              (λ ρ → δ (transR (≤→R ψ) ρ))
reflect (app d e)    γ δ = (reflect d γ δ) refl≤ (reflect e γ δ)
reflect (box d)      γ δ = λ ρ → reflect d ∙
                                            (λ ρ′ → δ (transR ρ ρ′))
reflect (unbox d e)  γ δ = reflect e γ (λ ρ → δ ρ , (reflect d γ δ) ρ)
reflect (pair d e)   γ δ = reflect d γ δ , reflect e γ δ
reflect (fst d)      γ δ = π₁ (reflect d γ δ)
reflect (snd d)      γ δ = π₂ (reflect d γ δ)
reflect unit         γ δ = ∙
reflect (boom d)     γ δ = elim⊥ (reflect d γ δ)
reflect (left d)     γ δ = ι₁ (reflect d γ δ)
reflect (right d)    γ δ = ι₂ (reflect d γ δ)
reflect (case d e f) γ δ = elim∨ (reflect d γ δ) (λ a → reflect e (γ , a) δ)
                                                 (λ b → reflect f (γ , b) δ)


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid.Base

private
  variable
    ℓ ℓ' : Level

module _
    (M : CommMonoid ℓ)
    (P : ⟨ M ⟩ → hProp ℓ')
    where
  open CommMonoidStr (snd M)
  module _
    (·Closed : (x y : ⟨ M ⟩) → ⟨ P x ⟩ → ⟨ P y ⟩ → ⟨ P (x · y) ⟩)
    (εContained : ⟨ P ε ⟩)
    where
    private
      subtype = Σ[ x ∈ ⟨ M ⟩ ] ⟨ P x ⟩

    makeSubCommMonoid : CommMonoid _
    fst makeSubCommMonoid = subtype
    CommMonoidStr.ε (snd makeSubCommMonoid) = ε , εContained
    CommMonoidStr._·_ (snd makeSubCommMonoid) (x , xContained) (y , yContained) =
      (x · y) , ·Closed x y xContained yContained
    IsCommMonoid.isMonoid (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) =
      makeIsMonoid
        (isOfHLevelΣ 2 (isSetFromIsCommMonoid isCommMonoid) λ _ → isProp→isSet (snd (P _)))
        (λ x y z → Σ≡Prop (λ _ → snd (P _)) (·Assoc (fst x) (fst y) (fst z)))
        (λ x → Σ≡Prop (λ _ → snd (P _)) (·IdR (fst x)))
        λ x → Σ≡Prop (λ _ → snd (P _)) (·IdL (fst x))
    IsCommMonoid.·Comm (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) =
      λ x y → Σ≡Prop (λ _ → snd (P _)) (·Comm (fst x) (fst y))

module CommMonoidTheory (M' : CommMonoid ℓ) where
 open CommMonoidStr (snd M')
 private M = ⟨ M' ⟩

 commAssocl : (x y z : M) → x · (y · z) ≡ y · (x · z)
 commAssocl x y z = ·Assoc x y z ∙∙ cong (_· z) (·Comm x y) ∙∙ sym (·Assoc y x z)

 commAssocr : (x y z : M) → x · y · z ≡ x · z · y
 commAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·Comm y z) ∙∙ ·Assoc x z y

 commAssocr2 : (x y z : M) → x · y · z ≡ z · y · x
 commAssocr2 x y z = commAssocr _ _ _ ∙∙ cong (_· y) (·Comm _ _) ∙∙ commAssocr _ _ _

 commAssocSwap : (x y z w : M) → (x · y) · (z · w) ≡ (x · z) · (y · w)
 commAssocSwap x y z w = ·Assoc (x · y) z w ∙∙ cong (_· w) (commAssocr x y z)
                                               ∙∙ sym (·Assoc (x · z) y w)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, Ulf, AIM XXIX, 2019-03-18, issue #3597

-- Eta-expansion of record metas disregards freezing.
-- Meta occurs check is then insufficient, leading to cyclic assignment.

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

-- {-# OPTIONS -v tc.meta:40 #-}
-- {-# OPTIONS -v tc.meta.assign:100 #-}
-- {-# OPTIONS -v tc.meta.eta:100 #-}

postulate P : (A : Set) → (a : A) → Set

record R : Set₁ where
  constructor c
  -- no-eta-equality -- WORKS without eta
  field
    A : Set
    a : A
    p : P A a → P A a

C : R
C = {!!}

module M = R C

test : P {!!} M.a → P {!!} M.a
test x = M.p x

-- WAS: cyclic assignment
--   C  = _5
--  _7 := _5 .A
--  _9 := _5 .A
--  _5 := c _10 _11 _12
-- _10 := C .A

-- NOW: frozed metas are eta-expanded to records of frozen metas


text:
module Generic.Lib.Data.Sum where

open import Data.Sum hiding (swap) renaming (map to smap) hiding (map₁; map₂; assocʳ; assocˡ; reduce) public

max_stars_repo_name: iblech/Generic

max_issues_repo_name: iblech/Generic

max_forks_repo_name: iblech/Generic


text:
module Lectures.Four where

open import Lectures.One public
open import Lectures.Two public
open import Lectures.Three public

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)

record _↔_ (A B : Set) : Set where
  constructor Isomorphism
  field
    to : A → B
    from : B → A
    from∘to : ∀ x → (from ∘ to) x ≡ x
    to∘from : ∀ y → (to ∘ from) y ≡ y

open List

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

foldr-ℕ : {A : Set} → (A → A) → A → ℕ → A
foldr-ℕ f z zero = z
foldr-ℕ f z (suc n) = f (foldr-ℕ f z n)

ℕ↔List⊤ : ℕ ↔ List ⊤
ℕ↔List⊤ = Isomorphism to from from∘to to∘from
  where

  to : ℕ → List ⊤
  to = foldr-ℕ (tt ∷_) []

  from : List ⊤ → ℕ
  from = foldr-List (λ _ → suc) 0

  from∘to : ∀ x → (from ∘ to) x ≡ x
  from∘to zero = refl
  from∘to (suc x) = cong suc (from∘to x)

  to∘from : ∀ x → (to ∘ from) x ≡ x
  to∘from [] = refl
  to∘from (tt ∷ xs) = cong (tt ∷_) (to∘from xs)

ℕ↔Even : ℕ ↔ Σ ℕ _isEven
ℕ↔Even = Isomorphism to from from∘to to∘from
  where

  to : ℕ → Σ ℕ _isEven
  to zero = zero , tt
  to (suc n) with to n
  to (suc n) | (2n , 2nEven) = (suc (suc 2n) , 2nEven)

  from : (Σ ℕ _isEven) → ℕ
  from (n , nEven) = half n nEven

  from∘to : ∀ x → (from ∘ to) x ≡ x
  from∘to zero = refl
  from∘to (suc n) with to n | from∘to n
  from∘to (suc .(half (proj₁ q) (proj₂ q))) | q | refl = refl

  to∘from : ∀ x → (to ∘ from) x ≡ x
  to∘from (zero , tt) = refl
  to∘from (suc (suc n) , nEven) rewrite to∘from (n , nEven) = refl

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc : ∀ {n} → Fin n → Fin (suc n)

noFin0 : Fin 0 → ⊥
noFin0 ()

open Vec
lookup : ∀ {n} {A : Set} → Vec A n → Fin n → A
lookup (x ∷ xs) zero = x
lookup (x ∷ xs) (suc i) = lookup xs i

-- For next time:
-- Fin
-- Constructive leq


text: module Issue2447.M where


text:
------------------------------------------------------------------------
-- Data and codata can sometimes be "unified"
------------------------------------------------------------------------

-- In Haskell one can define the partial list type once, and define
-- map once and for all for this type. In Agda one typically defines
-- the (finite) list type + map and separately the (potentially
-- infinite) colist type + map. This is not strictly necessary,
-- though: the two types can be unified. The gain may be small,
-- though.

module DataAndCodata where

open import Codata.Musical.Notation
open import Function
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Conditional coinduction

data Rec : Set where
  μ : Rec
  ν : Rec

∞? : Rec → Set → Set
∞? μ = id
∞? ν = ∞

♯? : ∀ (r : Rec) {A} → A → ∞? r A
♯? μ x = x
♯? ν x = ♯ x

♭? : ∀ (r : Rec) {A} → ∞? r A → A
♭? μ = id
♭? ν = ♭

------------------------------------------------------------------------
-- A type for definitely finite or potentially infinite lists

-- If the Rec parameter is μ, then the type contains finite lists, and
-- otherwise it contains potentially infinite lists.

infixr 5 _∷_

data List∞? (r : Rec) (A : Set) : Set where
  []  : List∞? r A
  _∷_ : A → ∞? r (List∞? r A) → List∞? r A

-- List equality.

infix 4 _≈_

data _≈_ {r A} : List∞? r A → List∞? r A → Set where
  []  : [] ≈ []
  _∷_ : ∀ {x y xs ys} →
        x ≡ y → ∞? r (♭? r xs ≈ ♭? r ys) → x ∷ xs ≈ y ∷ ys

-- μ-lists can be seen as ν-lists.

lift : ∀ {A} → List∞? μ A → List∞? ν A
lift []       = []
lift (x ∷ xs) = x ∷ ♯ lift xs

------------------------------------------------------------------------
-- The map function

-- Maps over any list. The definition contains separate cases for _∷_
-- depending on whether the Rec index is μ or ν, though.

map : ∀ {r A B} → (A → B) → List∞? r A → List∞? r B
map     f []       = []
map {μ} f (x ∷ xs) = f x ∷ map f xs        -- Structural recursion
                                           -- (guarded).
map {ν} f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)  -- Guarded corecursion.

-- In Haskell the map function is automatically (in effect) parametric
-- in the Rec parameter. Here this property is not automatic, so I
-- have proved it manually:

map-parametric : ∀ {A B} (f : A → B) (xs : List∞? μ A) →
                 map f (lift xs) ≈ lift (map f xs)
map-parametric f []       = []
map-parametric f (x ∷ xs) = refl ∷ ♯ map-parametric f xs

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --universe-polymorphism --allow-unsolved-metas #-}
module Issue253 where

open import Common.Level

data Id l (X : Set l)(x : X) : X → Set where
  refl : Id l X x x

resp : (A B : Set _) → Id _ (Set _) A B → Set
resp  _ _ eq with eq
resp ._ _ eq | refl = Level

{-
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Telescope.hs:51
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Record projections should be positive in their argument
module Issue602-2 where

record A : Set₁ where
  constructor mkA
  field
    f : Set

unA : A → Set
unA (mkA x) = x

data B (a : A) : Set where
  mkB : unA a → B a

data D : Set where
  d : B (mkA D) → D

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Luau.RuntimeError.ToString where

open import FFI.Data.String using (String; _++_)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Var.ToString using (varToString)

errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ H B → String

errToStringᴱ NilIsNotAFunction = "nil is not a function"
errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
errToStringᴱ (app E) = errToStringᴱ E
errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b

errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString x
errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau