text:
------------------------------------------------------------------------
-- A comparison of the two alternative definitions of weak
-- bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Bisimilarity.Weak.Alternative.Comparison where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import H-level equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

import Bisimilarity
import Bisimilarity.Classical
import Bisimilarity.Comparison as Comp
import Bisimilarity.Weak.Alternative
import Bisimilarity.Weak.Alternative.Classical
open import Labelled-transition-system

module _ {ℓ} {lts : LTS ℓ} where

  open LTS lts

  private
    module Co = Bisimilarity.Weak.Alternative           lts
    module Cl = Bisimilarity.Weak.Alternative.Classical lts

  -- Classically weakly bisimilar processes are coinductively weakly
  -- bisimilar.

  cl⇒co : ∀ {i p q} → p Cl.≈ q → Co.[ i ] p ≈ q
  cl⇒co = Comp.cl⇒co

  -- Coinductively weakly bisimilar processes are classically weakly
  -- bisimilar.

  co⇒cl : ∀ {p q} → p Co.≈ q → p Cl.≈ q
  co⇒cl = Comp.co⇒cl

  -- The function cl⇒co is a left inverse of co⇒cl (up to pointwise
  -- bisimilarity).

  cl⇒co∘co⇒cl : ∀ {i p q}
                (p≈q : p Co.≈ q) →
                Co.[ i ] cl⇒co (co⇒cl p≈q) ≡ p≈q
  cl⇒co∘co⇒cl = Comp.cl⇒co∘co⇒cl

  -- If there are two processes that are not equal, but weakly
  -- bisimilar, then co⇒cl is not a left inverse of cl⇒co.

  co⇒cl∘cl⇒co : ∀ {p q} →
                p ≢ q → p Co.≈ q →
                ∃ λ (p≈p : p Cl.≈ p) → co⇒cl (cl⇒co p≈p) ≢ p≈p
  co⇒cl∘cl⇒co = Comp.co⇒cl∘cl⇒co

  -- The two definitions of weak bisimilarity are logically
  -- equivalent.

  classical⇔coinductive : ∀ {p q} → p Cl.≈ q ⇔ p Co.≈ q
  classical⇔coinductive = Comp.classical⇔coinductive

  -- There is a split surjection from the classical definition of
  -- bisimilarity to the coinductive one (assuming two kinds of
  -- extensionality).

  classical↠coinductive :
    Extensionality ℓ ℓ →
    Co.Extensionality →
    ∀ {p q} → p Cl.≈ q ↠ p Co.≈ q
  classical↠coinductive = Comp.classical↠coinductive

-- There is at least one LTS for which there is a split surjection
-- from the coinductive definition of weak bisimilarity to the
-- classical one.

coinductive↠classical :
  ∀ {p q} →
  Bisimilarity.Weak.Alternative._≈_           empty p q ↠
  Bisimilarity.Weak.Alternative.Classical._≈_ empty p q
coinductive↠classical {p = ()}

-- There is an LTS for which coinductive weak bisimilarity is
-- pointwise propositional (assuming two kinds of extensionality and
-- univalence).

coinductive-weak-bisimilarity-is-sometimes-propositional :
  Extensionality lzero (lsuc lzero) →
  Univalence lzero →
  let module Co = Bisimilarity.Weak.Alternative one-loop in
  Co.Extensionality → Is-proposition (tt Co.≈ tt)
coinductive-weak-bisimilarity-is-sometimes-propositional ext univ =
  subst (λ lts → let module Co = Bisimilarity lts in
                  ∀ p → Co.Extensionality → Is-proposition (p Co.∼ p))
        (sym $ weak≡id ext univ one-loop (λ _ ()))
        (λ _ → Comp.coinductive-bisimilarity-is-sometimes-propositional
                 (lower-extensionality _ _ ext))
        _

-- However, classical weak bisimilarity (of any size) is, for the same
-- LTS, not pointwise propositional (assuming extensionality and
-- univalence).

classical-weak-bisimilarity-is-not-propositional :
  Extensionality lzero (lsuc lzero) →
  Univalence lzero →
  let module Cl = Bisimilarity.Weak.Alternative.Classical one-loop in
  ∀ {ℓ} → ¬ Is-proposition (Cl.Weak-bisimilarity′ ℓ (tt , tt))
classical-weak-bisimilarity-is-not-propositional ext univ {ℓ} =
  subst (λ lts → let module Cl = Bisimilarity.Classical lts in
                 ∀ p → ¬ Is-proposition (Cl.Bisimilarity′ ℓ (p , p)))
        (sym $ weak≡id ext univ one-loop (λ _ ()))
        (λ _ → Comp.classical-bisimilarity-is-not-propositional)
        _

-- Thus, assuming two kinds of extensionality and univalence, there is
-- in general no split surjection from the coinductive definition of
-- weak bisimilarity to the classical one (of any size).

¬coinductive↠classical :
  Extensionality lzero (lsuc lzero) →
  Univalence lzero →
  Bisimilarity.Weak.Alternative.Extensionality one-loop →
  ∀ {ℓ} →
  ¬ (∀ {p q} →
     Bisimilarity.Weak.Alternative._≈_ one-loop p q ↠
     Bisimilarity.Weak.Alternative.Classical.Weak-bisimilarity′
       one-loop ℓ (p , q))
¬coinductive↠classical ext univ ext′ {ℓ} =
  subst (λ lts → Bisimilarity.Extensionality lts →
                 ¬ (∀ {p q} → Bisimilarity._∼_ lts p q ↠
                              Bisimilarity.Classical.Bisimilarity′
                                lts ℓ (p , q)))
        (sym $ weak≡id ext univ one-loop (λ _ ()))
        (λ ext′ → Comp.¬coinductive↠classical
                    (lower-extensionality _ _ ext) ext′)
        ext′

-- Note also that coinductive weak bisimilarity is not always
-- propositional (assuming extensionality and univalence).

coinductive-weak-bisimilarity-is-not-propositional :
  Extensionality lzero (lsuc lzero) →
  Univalence lzero →
  let open Bisimilarity.Weak.Alternative two-bisimilar-processes in
  ¬ (∀ {p q} → Is-proposition (p ≈ q))
coinductive-weak-bisimilarity-is-not-propositional ext univ =
  subst (λ lts → let open Bisimilarity lts in
                 ¬ (∀ {p q} → Is-proposition (p ∼ q)))
        (sym $ weak≡id ext univ two-bisimilar-processes (λ _ ()))
        Comp.coinductive-bisimilarity-is-not-propositional

-- In fact, for every type A there is a pointwise split surjection
-- from a certain instance of weak bisimilarity to equality on A
-- (assuming extensionality and univalence).

weak-bisimilarity↠equality :
  ∀ {a} →
  Extensionality a (lsuc a) →
  Univalence a →
  {A : Type a} →
  let open Bisimilarity.Weak.Alternative (bisimilarity⇔equality A) in
  {p q : A} → p ≈ q ↠ p ≡ q
weak-bisimilarity↠equality ext univ {A} =
  subst (λ lts → let open Bisimilarity lts in
                 ∀ {p q} → p ∼ q ↠ p ≡ q)
        (sym $ weak≡id ext univ (bisimilarity⇔equality A) (λ _ ()))
        (Comp.bisimilarity↠equality {A = A})

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Examples.Type where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.String using (_++_)
open import Luau.Type using (nil; _∪_; _∩_; _⇒_)
open import Luau.Type.ToString using (typeToString)

ex1 : typeToString(nil) ≡ "nil"
ex1 = refl

ex2 : typeToString(nil ⇒ nil) ≡ "(nil) -> nil"
ex2 = refl

ex3 : typeToString(nil ⇒ (nil ⇒ nil)) ≡ "(nil) -> (nil) -> nil"
ex3 = refl

ex4 : typeToString(nil ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> (nil) -> nil)?"
ex4 = refl

ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
ex5 = refl

ex6 : typeToString((nil ⇒ nil) ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)"
ex6 = refl

ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?"
ex7 = refl

ext: agda


text:
module Sets.BoolSet {ℓ ℓₑ} where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Logic using (_⟶_ ; _⟵_)
open        Data.Boolean.Operators.Programming hiding (_==_)
open import Data.Boolean.Stmt
open import Data.Boolean.Proofs
import      Data.List as List
import      Data.List.Functions as List
open import Logic
open import Functional
open import Operator.Equals
open import Structure.Setoid
open import Type

-- A function from a type T to a boolean value.
-- This can be interpreted as a computable set over T (a set with a computable containment relation).
BoolSet : ∀{ℓ} → Type{ℓ} → Type{ℓ}
BoolSet(T) = (T → Bool)

module _ {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  𝐔 : BoolSet(T)
  𝐔 = const(𝑇)

  ∅ : BoolSet(T)
  ∅ = const(𝐹)

  singleton : ⦃ _ : DecidableEquiv(T) ⦄ → T → BoolSet(T)
  singleton(t) = (_== t)

  enumeration : ⦃ _ : DecidableEquiv(T) ⦄ → List.List(T) → BoolSet(T)
  enumeration(l) = (x ↦ List.satisfiesAny(_== x)(l))

  _∈?_ : T → BoolSet(T) → Bool
  _∈?_ = apply

  _∉?_ : T → BoolSet(T) → Bool
  _∉?_ a set = !(a ∈? set)

  {- TODO: Define a FinitelyEnumerable relation
  _⊆?_ : BoolSet(T) → BoolSet(T) → Bool
  _⊆?_ A B = all(elem ↦ (elem ∈? A) ⟶ (elem ∈? B))

  _⊇?_ : BoolSet(T) → BoolSet(T) → Bool
  _⊇?_ A B = all(elem ↦ (elem ∈? A) ⟵ (elem ∈? B))
  -}

  _∈_ : T → BoolSet(T) → Stmt
  _∈_ a set = IsTrue(a ∈? set)

  _∉_ : T → BoolSet(T) → Stmt
  _∉_ a set = IsTrue(a ∉? set)

  _⊆_ : BoolSet(T) → BoolSet(T) → Stmt
  _⊆_ set₁ set₂ = (∀{a} → (a ∈ set₁) → (a ∈ set₂))

  _⊇_ : BoolSet(T) → BoolSet(T) → Stmt
  _⊇_ set₁ set₂ = _⊆_ set₂ set₁

  _∪_ : BoolSet(T) → BoolSet(T) → BoolSet(T)
  _∪_ A B = (elem ↦ (elem ∈? A) || (elem ∈? B))

  _∩_ : BoolSet(T) → BoolSet(T) → BoolSet(T)
  _∩_ A B = (elem ↦ (elem ∈? A) && (elem ∈? B))

  _∖_ : BoolSet(T) → BoolSet(T) → BoolSet(T)
  _∖_ A B = (elem ↦ (elem ∈? A) && !(elem ∈? B))

  ∁_ : BoolSet(T) → BoolSet(T)
  ∁_ A = (elem ↦ !(elem ∈? A))

  ℘_ : BoolSet(T) → BoolSet(BoolSet(T))
  ℘_ _ = const(𝑇)

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:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Empty
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.List using ([]; _∷_; _++_)

open import Relation.Nullary
open import Relation.Unary using (_∪_; _∩_; Satisfiable)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; ε; _◅_)

open import Common

module Session {ℙ : Set} (message : Message ℙ)
  where

open import Trace message
open import SessionType message
open import Transitions message
open import HasTrace message

data Session : Set where
  _#_  : (T : SessionType) (S : SessionType) -> Session

data Reduction : Session -> Session -> Set where
  sync : ∀{α R R' T T'} (r : Transition R (co-action α) R') (t : Transition T α T') -> Reduction (R # T) (R' # T')

Reductions : Session -> Session -> Set
Reductions = Star Reduction

Reduce : Session -> Set
Reduce S = Satisfiable (Reduction S)

data Success : Session -> Set where
  win#def : ∀{T S} (w : Win T) (def : Defined S) -> Success (T # S)

ProgressS : Session -> Set
ProgressS = Success ∪ Reduce

MaySucceed : Session -> Set
MaySucceed S = Satisfiable (Reductions S ∩ Success)

InvariantS : (Session -> Set) -> Session -> Set
InvariantS P S = ∀{S'} -> Reductions S S' -> P S'

ImplyS : (Session -> Set) -> SessionType -> SessionType -> Set
ImplyS P T S = ∀{R} -> P (R # T) -> P (R # S)

ComplianceS : Session -> Set
ComplianceS = InvariantS ProgressS

FairComplianceS : Session -> Set
FairComplianceS = InvariantS MaySucceed

SubtypingS : SessionType -> SessionType -> Set
SubtypingS = ImplyS ComplianceS

FairSubtypingS : SessionType -> SessionType -> Set
FairSubtypingS = ImplyS FairComplianceS

ConvergenceS : SessionType -> SessionType -> Set
ConvergenceS T S = ∀{R} -> FairComplianceS (R # T) -> MaySucceed (R # S)

unzip-red* : ∀{T T' S S'} -> Reductions (T # S) (T' # S') ->
             ∃[ φ ] (Transitions T (co-trace φ) T' × Transitions S φ S')
unzip-red* ε = _ , refl , refl
unzip-red* (sync r t ◅ reds) =
  let _ , tr , sr = unzip-red* reds in
  _ , step r tr , step t sr

zip-red* : ∀{φ T T' S S'} ->
           Transitions T (co-trace φ) T' ->
           Transitions S φ S' ->
           Reductions (T # S) (T' # S')
zip-red* refl refl = ε
zip-red* (step t tr) (step s sr) = sync t s ◅ zip-red* tr sr

zip-traces :
  ∀{R T φ}
  (rφ : R HasTrace (co-trace φ))
  (tφ : T HasTrace φ) ->
  Reductions (R # T) (after rφ # after tφ)
zip-traces (_ , _ , rr) (_ , _ , tr) = zip-red* rr tr

success-not-reduce : ∀{S S'} → Success S → ¬ (Reduction S S')
success-not-reduce (win#def win _) (sync r _) = win-reduces-⊥ win r

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module _ where

open import Prelude
open import Numeric.Nat.Prime

2^44+7 2^46+15 2^48+21 : Nat
2^44+7  =  17592186044423
2^46+15 =  70368744177679
2^48+21 = 281474976710677

main : IO ⊤
main = print $ isPrime! 2^48+21

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

open import Relation.Binary using (Setoid)

-- Lifts a setoid into a 1-groupoid

module Categories.Category.Construction.0-Groupoid
  {c ℓ} e (S : Setoid c ℓ) where

open import Level using (Lift)
open import Data.Unit using (⊤)
open import Function using (flip)

open import Categories.Category.Groupoid using (Groupoid)

open Setoid S

0-Groupoid : Groupoid c ℓ e
0-Groupoid = record
  { category = record
    { Obj = Carrier
    ; _⇒_ = _≈_
    ; _≈_ = λ _ _ → Lift e ⊤
    ; id  = refl
    ; _∘_ = flip trans
    }
  ; isGroupoid = record { _⁻¹ = sym }
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module MapTm where

open import Prelude
open import Star
open import Modal
open import Examples
open import Lambda

open Term

eq⟶ : {ty : Set}(T : TyAlg ty){σ₁ σ₂ τ₁ τ₂ : ty} ->
         σ₁ == σ₂ -> τ₁ == τ₂ -> TyAlg._⟶_ T σ₁ τ₁ == TyAlg._⟶_ T σ₂ τ₂
eq⟶ T refl refl = refl

mapTm : {ty₁ ty₂ : Set}{T₁ : TyAlg ty₁}{T₂ : TyAlg ty₂}
        {Γ : List ty₁}{τ : ty₁}(F : T₁ =Ty=> T₂) ->
        Tm T₁ Γ τ -> Tm T₂ (map _ (TyArrow.apply F) Γ) (TyArrow.apply F τ)
mapTm {T₁ = T₁}{T₂}{Γ} F (var x) =
  var (mapAny (cong (TyArrow.apply F)) x)
mapTm {T₁ = T₁}{T₂}{Γ} F zz =
  subst (\τ -> Tm T₂ (map _ (TyArrow.apply F) Γ) τ)
        (TyArrow.respNat F) zz
mapTm {T₁ = T₁}{T₂}{Γ} F ss =
  subst Tm₂ (trans (TyArrow.resp⟶ F)
                   (TyArrow.respNat F -eq⟶ TyArrow.respNat F))
        ss
  where
    _-eq⟶_ = eq⟶ T₂
    Tm₂ = Tm T₂ (map _ (TyArrow.apply F) Γ)
mapTm {T₂ = T₂}{Γ} F (ƛ t)   =
  subst Tm₂ (TyArrow.resp⟶ F)
        (ƛ (mapTm F t))
  where Tm₂ = Tm T₂ (map _ (TyArrow.apply F) Γ)
mapTm {T₂ = T₂}{Γ} F (s $ t) =
  subst Tm₂ (sym (TyArrow.resp⟶ F)) (mapTm F s)
  $ mapTm F t
  where
    Tm₂ = Tm T₂ (map _ (TyArrow.apply F) Γ)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Sigma
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat

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

reverseAcc : {A : Set} → List A → List A → List A
reverseAcc [] ys = ys
reverseAcc (x ∷ xs) ys = reverseAcc xs (x ∷ ys)

reverse : {A : Set} → List A → List A
reverse xs = reverseAcc xs []

data Vec (A : Set) : Nat → Set where
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

postulate
  replicate : ∀ {A : Set} {n} → A → Vec A n
  zipWith : ∀ {A B C : Set} {n} → (A → B → C) → Vec A n → Vec B n → Vec C n

macro
  rtest : Name → Term → TC ⊤
  rtest f a = do
     (function (clause tel _ t ∷ [])) ← withReconstructed (getDefinition f) where
        _ → typeError (strErr "ERROR" ∷ [])
     t ← inContext (reverse tel) (normalise t)
     quoteTC t >>= unify a

transp : ∀ m n → Vec (Vec Nat n) m → Vec (Vec Nat m) n
transp .(suc m) n (_∷_ {m} x xs) = zipWith {Nat} {Vec Nat m} {Vec Nat (suc m)} {n} (_∷_ {Nat} {m}) x (transp _ n xs)

test : Term
test = rtest transp

max_stars_repo_name: sseefried/agda


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

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

open import LibraBFT.Abstract.Types
open EpochConfig

open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle sha256 sha256-cr

open import LibraBFT.Concrete.System.Parameters

open import LibraBFT.Yasm.Base
open import LibraBFT.Yasm.AvailableEpochs using (AvailableEpochs ; lookup'; lookup'')
open import LibraBFT.Yasm.System     ConcSysParms
open import LibraBFT.Yasm.Properties ConcSysParms

-- This module contains placeholders for the future analog of the
-- corresponding VotesOnce property.  Defining the implementation
-- obligation and proving that it is an invariant of an implementation
-- is a substantial undertaking.  We are working first on proving the
-- simpler VotesOnce property to settle down the structural aspects
-- before tackling the harder semantic issues.
module LibraBFT.Concrete.Properties.LockedRound where

 -- TODO-3: define the implementation obligation
 ImplObligation₁ : Set
 ImplObligation₁ = Unit

 -- Next, we prove that given the necessary obligations,
 module Proof
   (sps-corr : StepPeerState-AllValidParts)
   (Impl-LR1 : ImplObligation₁)
   where

  -- Any reachable state satisfies the LR rule for any epoch in the system.
  module _ {e}(st : SystemState e)(r : ReachableSystemState st)(eid : Fin e) where
   -- Bring in 'unwind', 'ext-unforgeability' and friends
   open Structural sps-corr

   -- Bring in ConcSystemState
   open import LibraBFT.Concrete.System sps-corr
   open PerState st r
   open PerEpoch eid

   open import LibraBFT.Abstract.Obligations.LockedRound 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔) as LR

   postulate  -- TODO-3: prove it
     lrr : LR.Type ConcSystemState


text:
module Cats.Trans.Iso where

open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Cats.Category.Base
open import Cats.Functor using (Functor)
open import Cats.Util.Simp using (simp!)
open import Cats.Trans using (Trans ; component ; natural)

import Cats.Category.Constructions.Iso as Iso

open Functor
open Iso.Build._≅_

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  where

  private
    module C = Category C
    module D = Category D
    open module D≅ = Iso.Build D using (_≅_)
    module ≅ = D≅.≅
    open D.≈-Reasoning

  record NatIso (F G : Functor C D) : Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′)
    where
    field
      iso : ∀ {c} → fobj F c ≅ fobj G c

      forth-natural : ∀ {c d} {f : c C.⇒ d}
        → forth iso D.∘ fmap F f D.≈ fmap G f D.∘ forth iso

    back-natural : ∀ {c d} {f : c C.⇒ d}
      → back iso D.∘ fmap G f D.≈ fmap F f D.∘ back iso
    back-natural {f = f} =
        begin
          back iso D.∘ fmap G f
        ≈⟨ D.∘-resp-r (D.≈.sym D.id-r) ⟩
          back iso D.∘ fmap G f D.∘ D.id
        ≈⟨ D.∘-resp-r (D.∘-resp-r (D.≈.sym (forth-back iso))) ⟩
          back iso D.∘ fmap G f D.∘ forth iso D.∘ back iso
        ≈⟨ simp! D ⟩
          back iso D.∘ (fmap G f D.∘ forth iso) D.∘ back iso
        ≈⟨ D.∘-resp-r (D.∘-resp-l (D.≈.sym forth-natural)) ⟩
          back iso D.∘ (forth iso D.∘ fmap F f) D.∘ back iso
        ≈⟨ simp! D ⟩
          (back iso D.∘ (forth iso)) D.∘ fmap F f D.∘ back iso
        ≈⟨ D.∘-resp-l (back-forth iso) ⟩
          D.id D.∘ fmap F f D.∘ back iso
        ≈⟨ D.id-l ⟩
          fmap F f D.∘ back iso
        ∎

    Forth : Trans F G
    Forth = record
        { component = λ _ → forth iso
        ; natural = forth-natural
        }

    Back : Trans G F
    Back = record
        { component = λ _ → back iso
        ; natural = back-natural
        }

  open NatIso public

  id : ∀ {F} → NatIso F F
  id = record
      { iso = ≅.refl
      ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }

  sym : ∀ {F G} → NatIso F G → NatIso G F
  sym θ = record
      { iso = ≅.sym (iso θ)
      ; forth-natural = back-natural θ
      }

  _∘_ : ∀ {F G H} → NatIso G H → NatIso F G → NatIso F H
  _∘_ {F} {G} {H} θ ι = record
      { iso = ≅.trans (iso ι) (iso θ)
      ; forth-natural = λ {_} {_} {f} →
          begin
            (forth (iso θ) D.∘ forth (iso ι)) D.∘ fmap F f
          ≈⟨ D.assoc ⟩
            forth (iso θ) D.∘ forth (iso ι) D.∘ fmap F f
          ≈⟨ D.∘-resp-r (forth-natural ι) ⟩
            forth (iso θ) D.∘ fmap G f D.∘ forth (iso ι)
          ≈⟨ D.unassoc ⟩
            (forth (iso θ) D.∘ fmap G f) D.∘ forth (iso ι)
          ≈⟨ D.∘-resp-l (forth-natural θ) ⟩
            (fmap H f D.∘ forth (iso θ)) D.∘ forth (iso ι)
          ≈⟨ D.assoc ⟩
            fmap H f D.∘ forth (iso θ) D.∘ forth (iso ι)
          ∎
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums (disjoint unions)
------------------------------------------------------------------------

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

module Data.Sum.Base where

open import Function using (_∘_; _-[_]-_ ; id)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Level using (_⊔_)

------------------------------------------------------------------------
-- Definition

infixr 1 _⊎_

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

------------------------------------------------------------------------
-- Functions

[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

[_,_]′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         (A → C) → (B → C) → (A ⊎ B → C)
[_,_]′ = [_,_]

swap : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → B ⊎ A
swap (inj₁ x) = inj₂ x
swap (inj₂ x) = inj₁ x

map : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
      (A → C) → (B → D) → (A ⊎ B → C ⊎ D)
map f g = [ inj₁ ∘ f , inj₂ ∘ g ]

map₁ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}→
       (A → C) → (A ⊎ B → C ⊎ B)
map₁ f = map f id

map₂ : ∀ {a b d} {A : Set a} {B : Set b} {D : Set d} →
       (B → D) → (A ⊎ B → A ⊎ D)
map₂ = map id

infixr 1 _-⊎-_
_-⊎-_ : ∀ {a b c d} {A : Set a} {B : Set b} →
        (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d))
f -⊎- g = f -[ _⊎_ ]- g

module _ {p} {P : Set p} where

-- Conversion back and forth with Dec

  fromDec : Dec P → P ⊎ ¬ P
  fromDec (yes p) = inj₁ p
  fromDec (no ¬p) = inj₂ ¬p

  toDec : P ⊎ ¬ P → Dec P
  toDec (inj₁ p)  = yes p
  toDec (inj₂ ¬p) = no ¬p


text:
------------------------------------------------------------------------------
-- Common FOL definitions
------------------------------------------------------------------------------

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

module Common.FOL where

infix  6 ∃
infix  4 _≡_
infixr 4 _,_

postulate D : Set

-- The existential quantifier type on D.
data ∃ (A : D → Set) : Set where
  _,_ : (t : D) → A t → ∃ A

-- The identity type on D.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude.Size

open import Labelled-transition-system

module Similarity.Equational-reasoning-instances
         {ℓ} {lts : LTS ℓ} {i : Size} where

open import Prelude

open import Bisimilarity lts
open import Equational-reasoning
open import Similarity lts

instance

  reflexive≤ : Reflexive [ i ]_≤_
  reflexive≤ = is-reflexive reflexive-≤

  reflexive≤′ : Reflexive [ i ]_≤′_
  reflexive≤′ = is-reflexive reflexive-≤′

  convert≤≤ : Convertible [ i ]_≤_ [ i ]_≤_
  convert≤≤ = is-convertible id

  convert≤′≤ : Convertible _≤′_ [ i ]_≤_
  convert≤′≤ = is-convertible λ p≤′q → force p≤′q

  convert≤≤′ : Convertible [ i ]_≤_ [ i ]_≤′_
  convert≤≤′ = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ≤ q → [ i ] p ≤′ q
    force (lemma p≤q) = p≤q

  convert≤′≤′ : Convertible [ i ]_≤′_ [ i ]_≤′_
  convert≤′≤′ = is-convertible id

  convert∼≤ : Convertible [ i ]_∼_ [ i ]_≤_
  convert∼≤ = is-convertible ∼⇒≤

  convert∼′≤ : Convertible _∼′_ [ i ]_≤_
  convert∼′≤ = is-convertible (convert ∘ ∼⇒≤′)

  convert∼≤′ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≤′_
  convert∼≤′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ∼ q → [ i ] p ≤′ q
    force (lemma p∼q) = ∼⇒≤ p∼q

  convert∼′≤′ : ∀ {i} → Convertible [ i ]_∼′_ [ i ]_≤′_
  convert∼′≤′ = is-convertible ∼⇒≤′

  trans≤≤ : Transitive [ i ]_≤_ [ i ]_≤_
  trans≤≤ = is-transitive transitive-≤

  trans≤′≤ : Transitive _≤′_ [ i ]_≤_
  trans≤′≤ = is-transitive λ p≤′q → transitive (force p≤′q)

  trans≤′≤′ : Transitive [ i ]_≤′_ [ i ]_≤′_
  trans≤′≤′ = is-transitive transitive-≤′

  trans≤≤′ : Transitive [ i ]_≤_ [ i ]_≤′_
  trans≤≤′ = is-transitive lemma
    where
    lemma : ∀ {p q r} → [ i ] p ≤ q → [ i ] q ≤′ r → [ i ] p ≤′ r
    force (lemma p≤q q≤′r) = transitive-≤ p≤q (force q≤′r)


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

module Dodo.Binary.Precedes where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Product using (_×_; _,_)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (REL; Rel)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_)
-- Local imports
open import Dodo.Binary.Transitive
open import Dodo.Binary.Immediate

-- # Definitions #

-- `¬ P x` before `¬ P y`
-- `P x`   before `¬ P y`
-- `P x`   before `P y`
⊤-Precedes-⊥ : {a ℓ₁ ℓ₂ : Level} {A : Set a} → Pred A ℓ₁ → Rel A ℓ₂ → Set _
⊤-Precedes-⊥ P R = ∀ {x y} → R x y → (P y → P x)

-- We could generalize `⊤-Precedes-⊥` to `Precedes` below:
--
-- Precedes : {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} → Pred A ℓ₁ → Pred A ℓ₂ → Rel A ℓ₃ → Set _
-- Precedes P Q R = ∀ {x y} → R x y → (P y → P x) × (Q x → Q y)
--
-- However, this is semantically a bit cumbersome, as P and Q are /not/ mutually exclusive.
-- Which means both P and Q may hold for an element.

-- # Helpers #

private
  identity : {a : Level} → {A : Set a} → A → A
  identity x = x

  contrapositive : ∀ {a b : Level} {A : Set a} {B : Set b}
    → ( A → B ) → ( ¬ B → ¬ A )
  contrapositive f ¬b a = ¬b (f a)

-- # Operations #

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} (R : Rel A ℓ₂) where

  ⊤prec⊥-invert : ⊤-Precedes-⊥ P R → {x y : A} → R x y → ¬ P x → ¬ P y
  ⊤prec⊥-invert ⊤prec⊥ Rxy ¬Px Py = contrapositive ¬Px identity (⊤prec⊥ Rxy Py)

-- # Properties #

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂} where

  ⊤prec⊥-⁺ : ⊤-Precedes-⊥ P R → ⊤-Precedes-⊥ P (TransClosure R)
  ⊤prec⊥-⁺ Pprec¬P [ x∼y ]      Py = Pprec¬P x∼y Py
  ⊤prec⊥-⁺ Pprec¬P (x∼y ∷ y~⁺z) Py = Pprec¬P x∼y (⊤prec⊥-⁺ Pprec¬P y~⁺z Py)

  ⊤prec⊥-imm : ⊤-Precedes-⊥ P R → ⊤-Precedes-⊥ P (immediate R)
  ⊤prec⊥-imm Pprec¬P (x~y , ¬∃z) Py = Pprec¬P x~y Py

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
-- Copyright 2020 Frederik Zipp. All rights reserved.
-- Use of this source code is governed by a BSD-style
-- license that can be found in the LICENSE file.

module GameOfLife where

open import Data.Bool using (Bool; _∨_; if_then_else_)
open import Data.Nat using (ℕ; suc; _+_; _<ᵇ_; _≡ᵇ_)
open import Data.List using (List; []; _∷_; length; zipWith; upTo; sum; map)
open import Data.Maybe using (Maybe; just; nothing; fromMaybe)
open import Data.String using (String; intersperse)
open import Function using (_∘_; id; _$_)
open import IO using (run; putStrLn)

---- Utility functions ----

mapWithIndex : ∀ {A B : Set} → (ℕ → A → B) → List A → List B
mapWithIndex f xs = zipWith f (upTo (length xs)) xs

_element_ : ∀ {A : Set} → List A → ℕ → Maybe A
[] element n = nothing
(x ∷ xs) element 0 = just x
(x ∷ xs) element suc n = xs element n

_-_ : ℕ → ℕ → Maybe ℕ
m - 0 = just m
0 - (suc n) = nothing
suc m - suc n = m - n

catMaybes : ∀ {A : Set} → List (Maybe A) → List A
catMaybes [] = []
catMaybes (nothing ∷ xs) = catMaybes xs
catMaybes (just x ∷ xs) = x ∷ catMaybes xs

---- Domain ----

data Cell : Set where
  □ : Cell
  ■ : Cell

aliveCount : Cell → ℕ
aliveCount □ = 0
aliveCount ■ = 1

Row : Set
Row = List Cell

Board : Set
Board = List Row

data Pos : Set where
  ⟨_,_⟩ : ℕ → ℕ → Pos

⟨_,_⟩? : Maybe ℕ → Maybe ℕ → Maybe Pos
⟨ just colᵢ , just rowᵢ ⟩? = just ⟨ colᵢ , rowᵢ ⟩
⟨ just colᵢ , nothing   ⟩? = nothing
⟨ nothing   , just rowᵢ ⟩? = nothing
⟨ nothing   , nothing   ⟩? = nothing

neighbourPositions : Pos → List Pos
neighbourPositions ⟨ colᵢ , rowᵢ ⟩ = catMaybes (
  ⟨      (colᵢ - 1) ,      (rowᵢ - 1) ⟩? ∷
  ⟨      (colᵢ - 1) , just (rowᵢ + 0) ⟩? ∷
  ⟨      (colᵢ - 1) , just (rowᵢ + 1) ⟩? ∷
  ⟨ just (colᵢ + 0) ,      (rowᵢ - 1) ⟩? ∷
  ⟨ just (colᵢ + 0) , just (rowᵢ + 1) ⟩? ∷
  ⟨ just (colᵢ + 1) ,      (rowᵢ - 1) ⟩? ∷
  ⟨ just (colᵢ + 1) , just (rowᵢ + 0) ⟩? ∷
  ⟨ just (colᵢ + 1) , just (rowᵢ + 1) ⟩? ∷
  [])

cellAt : Board → Pos → Cell
cellAt board ⟨ colᵢ , rowᵢ ⟩ = fromMaybe □ ((fromMaybe [] (board element rowᵢ)) element colᵢ)

aliveCountAt : Board → Pos → ℕ
aliveCountAt board = aliveCount ∘ cellAt board

neighbourCount : Board → Pos → ℕ
neighbourCount board pos = sum $ map (aliveCountAt board) (neighbourPositions pos)

nextCell : Cell → ℕ → Cell
nextCell ■ neighbours = if (neighbours <ᵇ 2) ∨ (3 <ᵇ neighbours) then □ else ■
nextCell □ neighbours = if (neighbours ≡ᵇ 3) then ■ else □

nextRow : Board → ℕ → Row → Row
nextRow board rowᵢ = mapWithIndex (λ colᵢ cell → nextCell cell (neighbourCount board ⟨ colᵢ , rowᵢ ⟩))

nextGen : Board → Board
nextGen board = mapWithIndex (nextRow board) board

nthGen : ℕ → Board → Board
nthGen 0 = id
nthGen (suc n) = nextGen ∘ nthGen n

---- "Tests" ----

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

-- Glider

gliderBoard : Board
gliderBoard = (
  (□ ∷ ■ ∷ □ ∷ □ ∷ []) ∷
  (□ ∷ □ ∷ ■ ∷ □ ∷ []) ∷
  (■ ∷ ■ ∷ ■ ∷ □ ∷ []) ∷
  (□ ∷ □ ∷ □ ∷ □ ∷ []) ∷
  (□ ∷ □ ∷ □ ∷ □ ∷ []) ∷
  [])

assertGliderGen4 : nthGen 4 gliderBoard ≡ (
  (□ ∷ □ ∷ □ ∷ □ ∷ []) ∷
  (□ ∷ □ ∷ ■ ∷ □ ∷ []) ∷
  (□ ∷ □ ∷ □ ∷ ■ ∷ []) ∷
  (□ ∷ ■ ∷ ■ ∷ ■ ∷ []) ∷
  (□ ∷ □ ∷ □ ∷ □ ∷ []) ∷
  [])
assertGliderGen4 = refl

-- Blinker

blinker_v : Board
blinker_v = (
  (□ ∷ ■ ∷ □ ∷ []) ∷
  (□ ∷ ■ ∷ □ ∷ []) ∷
  (□ ∷ ■ ∷ □ ∷ []) ∷
  [])

blinker_h : Board
blinker_h = (
  (□ ∷ □ ∷ □ ∷ []) ∷
  (■ ∷ ■ ∷ ■ ∷ []) ∷
  (□ ∷ □ ∷ □ ∷ []) ∷
  [])

assertBlinkerGen0 : nthGen 0 blinker_v ≡ blinker_v
assertBlinkerGen0 = refl

assertBlinkerGen1 : nthGen 1 blinker_v ≡ blinker_h
assertBlinkerGen1 = refl

assertBlinkerGen2 : nthGen 2 blinker_v ≡ blinker_v
assertBlinkerGen2 = refl

assertBlinkerGen3 : nthGen 3 blinker_v ≡ blinker_h
assertBlinkerGen3 = refl

gen0-ident : ∀ {b : Board} → nthGen 0 b ≡ b
gen0-ident = refl

---- Main ----

showCell : Cell → String
showCell □ = "□"
showCell ■ = "■"

showRow : Row → String
showRow = intersperse " " ∘ map showCell

showBoard : Board → String
showBoard = intersperse "\n" ∘ map showRow

main = run $ putStrLn ∘ showBoard ∘ nthGen 3 $ blinker_h

max_stars_repo_name: fzipp/agda-life

max_issues_repo_name: fzipp/agda-life

max_forks_repo_name: fzipp/agda-life


text:
module Structure.Function.Names where

open import Function.Names
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Structure.Setoid.Uniqueness
open import Structure.Setoid
open import Type

private variable ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₒ₄ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ ℓₗ₄ : Lvl.Level

module _ {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄ where
  Injective : (A → B) → Stmt
  Injective(f) = (∀{x y : A} → (f(x) ≡ f(y)) → (x ≡ y))

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄ where
  Surjective : (A → B) → Stmt
  Surjective(f) = (∀{y : B} → ∃(x ↦ f(x) ≡ y))

module _ {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄ where
  Bijective : (A → B) → Stmt
  Bijective(f) = (∀{y : B} → ∃!(x ↦ f(x) ≡ y))

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄ where
  InversesOn : (A → B) → (B → A) → B → Stmt
  InversesOn f g x = ((f ∘ g)(x) ≡ x)

  Inverses : (A → B) → (B → A) → Stmt
  Inverses f g = ∀¹(InversesOn f g)

  Constant : (A → B) → Stmt
  Constant(f) = (∀{x y : A} → (f(x) ≡ f(y)))

module _ {A : Type{ℓₒ}} ⦃ equiv : Equiv{ℓₗ}(A) ⦄ where
  Fixpoint : (A → A) → A → Stmt
  Fixpoint f(x) = (f(x) ≡ x)

  InvolutionOn : (A → A) → A → Stmt
  InvolutionOn f(x) = InversesOn f f x
  -- (f ∘ f)(x) ≡ x
  -- f(f(x)) ≡ x

  Involution : (A → A) → Stmt
  Involution(f) = Inverses f f

  IdempotentOn : (A → A) → A → Stmt
  IdempotentOn f(x) = Fixpoint f(f(x))
  -- (f ∘ f)(x) ≡ f(x)
  -- f(f(x)) ≡ f(x)

  Idempotent : (A → A) → Stmt
  Idempotent(f) = ∀ₗ(IdempotentOn f)

module _ {A : Type{ℓₒ₁}} ⦃ equiv-A : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄ where
  Congruence₁ : (A → B) → Stmt
  Congruence₁(f) = (∀{x y : A} → (x ≡ y) → (f(x) ≡ f(y)))

  module _ {C : Type{ℓₒ₃}} ⦃ _ : Equiv{ℓₗ₃}(C) ⦄ where
    Congruence₂ : (A → B → C) → Stmt
    Congruence₂(f) = (∀{x₁ y₁ : A}{x₂ y₂ : B} → (x₁ ≡ y₁) → (x₂ ≡ y₂) → (f x₁ x₂ ≡ f y₁ y₂))

    module _ {D : Type{ℓₒ₄}} ⦃ _ : Equiv{ℓₗ₄}(D) ⦄ where
      Congruence₃ : (A → B → C → D) → Stmt
      Congruence₃(f) = (∀{x₁ y₁ : A}{x₂ y₂ : B}{x₃ y₃ : C} → (x₁ ≡ y₁) → (x₂ ≡ y₂) → (x₃ ≡ y₃) → (f x₁ x₂ x₃ ≡ f y₁ y₂ y₃))

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ ⦃ _ : Equiv{ℓₗ₃}(A → B) ⦄ where
  FunctionExtensionalityOn : (A → B) → (A → B) → Stmt
  FunctionExtensionalityOn(f)(g) = ((f ⊜ g) → (f ≡ g))

  FunctionApplicationOn : (A → B) → (A → B) → Stmt
  FunctionApplicationOn(f)(g) = ((f ≡ g) → (f ⊜ g))

module _ (A : Type{ℓₒ₁}) (B : Type{ℓₒ₂}) ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ ⦃ _ : Equiv{ℓₗ₃}(A → B) ⦄ where
  FunctionExtensionality : Stmt
  FunctionExtensionality = ∀²(FunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})

  FunctionApplication : Stmt
  FunctionApplication = ∀²(FunctionApplicationOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})

module _ {A : Type{ℓₒ₁}} {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}((a : A) → B(a)) ⦄ where
  DependentFunctionExtensionalityOn : ((a : A) → B(a)) → ((a : A) → B(a)) → Stmt
  DependentFunctionExtensionalityOn(f)(g) = ((f ⊜ g) → (f ≡ g))

module _ (A : Type{ℓₒ₁}) (B : A → Type{ℓₒ₂}) ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}((a : A) → B(a)) ⦄ where
  DependentFunctionExtensionality : Stmt
  DependentFunctionExtensionality = ∀²(DependentFunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})

module _ {A : Type{ℓₒ₁}} {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}({a : A} → B(a)) ⦄ where
  DependentImplicitFunctionExtensionalityOn : ({a : A} → B(a)) → ({a : A} → B(a)) → Stmt
  DependentImplicitFunctionExtensionalityOn(f)(g) = (((\{a} → f{a}) ⊜ᵢ (\{a} → g{a})) → ((\{a} → f{a}) ≡ (\{a} → g{a})))

module _ (A : Type{ℓₒ₁}) (B : A → Type{ℓₒ₂}) ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}({a : A} → B(a)) ⦄ where
  DependentImplicitFunctionExtensionality : Stmt
  DependentImplicitFunctionExtensionality = ∀²(DependentImplicitFunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})

module _ {A : Type{ℓₒ₁}} {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}(⦃ a : A ⦄ → B(a)) ⦄ where
  DependentInstanceFunctionExtensionalityOn : (⦃ a : A ⦄ → B(a)) → (⦃ a : A ⦄ → B(a)) → Stmt
  DependentInstanceFunctionExtensionalityOn(f)(g) = (((\ ⦃ a ⦄ → f ⦃ a ⦄) ⦃⊜⦄ (\ ⦃ a ⦄ → g ⦃ a ⦄)) → ((\ ⦃ a ⦄ → f ⦃ a ⦄) ≡ (\ ⦃ a ⦄ → g ⦃ a ⦄)))

module _ (A : Type{ℓₒ₁}) (B : A → Type{ℓₒ₂}) ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}(⦃ a : A ⦄ → B(a)) ⦄ where
  DependentInstanceFunctionExtensionality : Stmt
  DependentInstanceFunctionExtensionality = ∀²(DependentInstanceFunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})


text:
module Acc where

data Acc ( A : Set ) ( Lt : A -> A -> Set) : A -> Set where
  acc :    (   b : A )
        -> ( ( a : A ) -> Lt a b  ->  Acc A Lt a )
        -> ( Acc A Lt b )

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

data Lt : Nat -> Nat -> Set where
  ltzero : ( x : Nat ) -> Lt zero (succ x)
  ltsucc : ( x : Nat ) -> (y : Nat) -> Lt x y -> Lt (succ x) (succ y)

notLt0 : ( x : Nat ) -> Lt x zero -> (C : Set) -> C
notLt0 x ()

accLt : ( x : Nat ) -> Acc Nat Lt x
accLt zero = acc zero (\a -> \p -> notLt0 a p (Acc Nat Lt a) )
accLt (succ x) = acc (succ x) (\a -> \p -> (accLt a))

----

data WO ( A : Set ) ( Lt : A -> A -> Set ) : Set where
  wo : ((x : A) -> Acc A Lt x) -> WO A Lt

woLt : WO Nat Lt
woLt = wo accLt

max_stars_repo_name: andreasabel/miniagda

max_issues_repo_name: andreasabel/miniagda

max_forks_repo_name: andreasabel/miniagda


text:
{-# OPTIONS --safe #-}
module JVM.Printer.Jasmin where

open import Function
open import Data.Nat
open import Data.Integer
open import Data.Nat.Show as NatShow
open import Data.String as S using (String)
open import Data.List as List

open import JVM.Types
open import JVM.Builtins

sep : List (List String) → List String
sep = List.concat ∘ List.intersperse [ " " ]

Words = List String

abstract
  Line  = String
  Lines = List String

  unwords : Words → Line
  unwords = S.unwords

  line : String → Line
  line = id

  lines : List Line → Lines
  lines = id

  unlines : Lines → String
  unlines = S.unlines

  infixr 4 _<+_
  _<+_ : Line → Lines → Lines
  l <+ ls = l ∷ ls

  infixl 6 _+>_
  _+>_ : Lines → Line → Lines
  ls +> l = ls ∷ʳ l

  infixl 4 _<>_
  _<>_ : Lines → Lines → Lines
  ls <> js = ls ++ js

  pars : List Lines → Lines
  pars = concat

  ident : Line → Line
  ident = "\t" S.++_

  indent : Lines → Lines
  indent = List.map ident

record ClassSpec : Set where
  constructor class
  field
    class_name : String

  out : Line
  out = unwords $ ".class" ∷ "public" ∷ class_name ∷ []

record SuperSpec : Set where
  constructor super
  field
    class_name : String

  out : Line
  out = unwords  $ ".super" ∷ class_name ∷ []

record Header : Set where
  field
    class_spec : ClassSpec
    super_spec : SuperSpec

  out : Lines
  out = lines $ ClassSpec.out class_spec
      ∷ SuperSpec.out super_spec
      ∷ []

module Descriptor where

  type-desc : Ty → String
  type-desc boolean   = "Z"
  type-desc byte      = "B"
  type-desc short     = "S"
  type-desc int       = "I"
  type-desc long      = "J"
  type-desc char      = "C"
  type-desc (array t) = "[" S.++ type-desc t
  type-desc (ref cls) = S.concat $ "L" ∷ cls ∷ ";" ∷ []

  ret-desc : Ret → String
  ret-desc void   = "V"
  ret-desc (ty t) = type-desc t

  out : List Ty → Ret → String
  out as r = args as S.++ ret-desc r
    where
      args : List Ty → String
      args d = "(" S.++ (S.intersperse ";" (List.map type-desc d)) S.++ ")"

data Comparator : Set where
  eq ne lt ge gt le : Comparator
  icmpge icmpgt icmpeq icmpne icmplt icmple : Comparator

open import JVM.Types using (Fun)

module Comp where

  out : Comparator → String
  out eq = "eq"
  out ne = "ne"
  out lt = "lt"
  out ge = "ge"
  out gt = "gt"
  out le = "le"
  out icmpge = "_icmpge"
  out icmpgt = "_icmpgt"
  out icmpeq = "_icmpeq"
  out icmpne = "_icmpne"
  out icmplt = "_icmplt"
  out icmple = "_icmple"

data Instr : Set where
  nop pop dup swap ret : Instr

  aconst_null                      : Instr
  bipush sipush                    : ℤ → Instr
  iconstm1 iconst0 iconst1 iconst2 : Instr

  aaload  aload  iload             : ℕ → Instr
  aastore astore istore            : ℕ → Instr

  new                              : String → Instr

  goto                             : String     → Instr
  if                               : Comparator → String → Instr

  iadd isub imul idiv ixor         : Instr

  invokevirtual invokespecial invokestatic : Fun → Instr

module Funs where

  out : Fun → String
  out (c / m :⟨ as ⟩ r) = c S.++ "/" S.++ m S.++ Descriptor.out as r

module Instruction where

  lbl : String → String
  lbl x = "label_" S.++ x

  showInt : ℤ → String
  showInt (+ n) = NatShow.show n
  showInt (-[1+ n ]) = "-" S.++ NatShow.show (ℕ.suc n)

  out : Instr → Line
  out nop         = line "nop"
  out pop         = line "pop"
  out dup         = line "dup"
  out swap        = line "swap"
  out ret         = line "return"
  out aconst_null = line "aconst_null"

  out (bipush n)  = unwords $ "sipush" ∷ showInt n ∷ []
  out (sipush n)  = unwords $ "bipush" ∷ showInt n ∷ []
  out (aload n)   = unwords $ "aload"  ∷ NatShow.show n ∷ []
  out (astore n)  = unwords $ "astore" ∷ NatShow.show n ∷ []
  out (iload n)   = unwords $ "iload"  ∷ NatShow.show n ∷ []
  out (istore n)  = unwords $ "istore" ∷ NatShow.show n ∷ []
  out (aaload n)  = unwords $ "aaload" ∷ NatShow.show n ∷ []
  out (aastore n) = unwords $ "astore" ∷ NatShow.show n ∷ []

  out iconstm1    = line "iconstm1"
  out iconst0     = line "iconst_0"
  out iconst1     = line "iconst_1"
  out iconst2     = line "iconst_2"

  out (goto l)    = unwords $ "goto" ∷ lbl l ∷ []
  out (if c l)    = unwords $ ("if" S.++ Comp.out c) ∷ lbl l ∷ []

  out iadd        = line "iadd"
  out isub        = line "isub"
  out imul        = line "imul"
  out idiv        = line "idiv"
  out ixor        = line "ixor"

  out (new c)     = unwords $ "new" ∷ c ∷ []

  out (invokespecial sf) = unwords $ "invokespecial" ∷ Funs.out sf ∷ []
  out (invokestatic  sf) = unwords $ "invokestatic"  ∷ Funs.out sf ∷ []
  out (invokevirtual sf) = unwords $ "invokevirtual" ∷ Funs.out sf ∷ []

data Stat : Set where
  label : String → Stat
  instr : Instr  → Stat

module Statement where

  out : Stat → Line
  out (label x) = line $ Instruction.lbl x S.++ ":"
  out (instr x) = Instruction.out x

record ClassField : Set where
  constructor clsfield
  field
    name   : String
    access : List String
    f_ty   : Ty

  out : Line
  out = unwords
      $ ".field"
      ∷ access
     ++ name
      ∷ Descriptor.type-desc f_ty
      ∷ []

record Method : Set where
  constructor method
  field
    name       : String
    access     : List String
    locals     : ℕ
    stacksize  : ℕ
    m_args     : List Ty
    m_ret      : Ret
    body       : List Stat

  out : Lines
  out =  (unwords $ ".method" ∷ (S.unwords access) ∷ (name S.++ Descriptor.out m_args m_ret) ∷ [])
      <+ (ident $ unwords $ ".limit locals" ∷ NatShow.show locals ∷ [])
      <+ (ident $ unwords $ ".limit stack"  ∷ NatShow.show stacksize ∷ [])
      <+ (lines $ List.map (ident ∘ Statement.out) body)
      +> (line $ ".end method")

record Jasmin : Set where
  constructor jasmin
  field
    header  : Header
    fields  : List ClassField
    methods : List Method

  out : Lines
  out = Header.out header
      <> lines (List.map ClassField.out fields)
      <> pars (List.map Method.out methods)

module _ where

  defaultInit : Method
  defaultInit = method "<init>" [ "public" ] 1 1 [] void
              ( instr (aload 0)
              ∷ instr (invokespecial (Object / "<init>" :⟨ [] ⟩ void))
              ∷ instr ret
              ∷ []
              )

  procedure : (name : String) → ℕ → ℕ → List Stat → Jasmin
  procedure name locals stack st =
    jasmin
      (record { class_spec = class name ; super_spec = super Object })
      []
      ( method "apply" ("public" ∷ "static" ∷ []) locals stack [] void (st ∷ʳ instr ret)
      ∷ defaultInit
      ∷ method "main" ("public" ∷ "static" ∷ []) 1 0 [ array (ref "java/lang/String") ] void
        ( instr (invokestatic (name / "apply" :⟨ [] ⟩ void))
        ∷ instr ret
        ∷ []
        )
      ∷ []
      )


text:
{-# OPTIONS --safe --no-guardedness #-}

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A

open Stream

repeat : ∀ {A} → A → Stream A
repeat x .head = x
repeat x .tail = repeat x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- An alternative backend
------------------------------------------------------------------------

-- Acknowledgements:
--
-- • The use of parsing "processes" is based on implementation C from
--   Koen Claessen's paper Parallel parsing processes.
--
-- • The idea to use toProc is due to Jean-Philippe Bernardy.

-- It is not obvious how to adapt this backend so that it can handle
-- parsers which are simultaneously left and right recursive, like
-- TotalRecognisers.LeftRecursion.leftRight.

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

module TotalRecognisers.Simple.AlternativeBackend
         (Tok : Set)
         (_≟_ : Decidable (_≡_ {A = Tok}))
         -- The tokens must come with decidable equality.
         where

open import Codata.Musical.Notation
open import Data.Bool hiding (_≟_)
open import Data.List
open import Relation.Nullary.Decidable

import TotalRecognisers.Simple as S
open S Tok _≟_ hiding (_∈?_)

------------------------------------------------------------------------
-- Parsing "processes"

data Proc : Set where
  tokenBind : (p : Tok → ∞ Proc) → Proc
  emptyOr   : (p : Proc) → Proc
  fail      : Proc

-- The semantics of Proc is given by run: run p s is true iff s is a
-- member of the language defined by p.

run : Proc → List Tok → Bool
run (tokenBind p) (c ∷ s) = run (♭ (p c)) s
run (emptyOr p)   s       = null s ∨ run p s
run _             _       = false

------------------------------------------------------------------------
-- Parsers can be turned into processes

-- Here I use my technique for "beating the productivity checker".

-- Process "programs".

infixl 5 _∣_

data ProcP : Set where
  -- Process primitives.
  tokenBind : (p : Tok → ∞ ProcP) → ProcP
  emptyOr   : (p : ProcP) → ProcP
  fail      : ProcP

  -- Symmetric choice.
  _∣_     : (p₁ p₂ : ProcP) → ProcP

  -- Embedding of parsers.
  toProc  : ∀ {n} (p : P n) (κ : ProcP) → ProcP

-- WHNFs.

data ProcW : Set where
  tokenBind : (p : Tok → ∞ ProcP) → ProcW
  emptyOr   : (p : ProcW) → ProcW
  fail      : ProcW

-- WHNFs can be turned into programs.

program : ProcW → ProcP
program (tokenBind p) = tokenBind p
program (emptyOr p)   = emptyOr (program p)
program fail          = fail

-- Symmetric choice for WHNFs.

_∣W_ : ProcW → ProcW → ProcW
tokenBind p₁ ∣W tokenBind p₂ = tokenBind (λ c → ♯ (♭ (p₁ c) ∣ ♭ (p₂ c)))
emptyOr p₁   ∣W emptyOr p₂   = emptyOr (p₁ ∣W p₂)
emptyOr p₁   ∣W p₂           = emptyOr (p₁ ∣W p₂)
p₁           ∣W emptyOr p₂   = emptyOr (p₁ ∣W p₂)
fail         ∣W p₂           = p₂
p₁           ∣W fail         = p₁

-- Interpretation of toProc.

mutual

  toProcW′ : ∀ {n} → P n → if n then ProcW else ProcP → ProcW
  toProcW′ fail                                  κ = fail
  toProcW′ empty                                 κ = κ
  toProcW′ (tok t)                               κ = tokenBind (λ t′ →
                                                       if ⌊ t ≟ t′ ⌋ then ♯ κ else ♯ fail)
  toProcW′ (_∣_ {n₁ = true } {n₂ = true } p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW′ p₂ κ
  toProcW′ (_∣_ {n₁ = true } {n₂ = false} p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW  p₂ κ
  toProcW′ (_∣_ {n₁ = false} {n₂ = true } p₁ p₂) κ = toProcW  p₁ κ ∣W toProcW′ p₂ κ
  toProcW′ (_∣_ {n₁ = false} {n₂ = false} p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW′ p₂ κ
  toProcW′ (_·_ {n₁ = true }              p₁ p₂) κ = toProcW′ p₁ (toProcW′  p₂  κ)
  toProcW′ (_·_ {n₁ = false}              p₁ p₂) κ = toProcW′ p₁ (toProc (♭ p₂) κ)

  toProcW : ∀ {n} → P n → ProcW → ProcW
  toProcW {true } p κ = toProcW′ p          κ
  toProcW {false} p κ = toProcW′ p (program κ)

-- Programs can be turned into WHNFs.

whnf : ProcP → ProcW
whnf (tokenBind p) = tokenBind p
whnf (emptyOr p)   = emptyOr (whnf p)
whnf fail          = fail
whnf (p₁ ∣ p₂)     = whnf p₁ ∣W whnf p₂
whnf (toProc p κ)  = toProcW p (whnf κ)

-- Programs can be turned into processes.

mutual

  ⟦_⟧W : ProcW → Proc
  ⟦ tokenBind p ⟧W = tokenBind (λ c → ♯ ⟦ ♭ (p c) ⟧P)
  ⟦ emptyOr p   ⟧W = emptyOr ⟦ p ⟧W
  ⟦ fail        ⟧W = fail

  ⟦_⟧P : ProcP → Proc
  ⟦ p ⟧P = ⟦ whnf p ⟧W

------------------------------------------------------------------------
-- Alternative backend

-- I have not proved that this implementation is correct.

infix 4 _∈?_

_∈?_ : ∀ {n} → List Tok → P n → Bool
s ∈? p = run ⟦ toProc p (emptyOr fail) ⟧P s

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

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

-- The ground types that are common across Abstract, Concrete and Impl
-- and some utility types
module LibraBFT.Base.Types where

  Epoch : Set
  Epoch = ℕ

  Round : Set
  Round = ℕ

  -- This was intended to be a simple way to flag meta-information without having it
  -- getting in the way.  It's important to ensure that an implementation does not
  -- use various information, such as who is honest.  However, we found this got in
  -- the way too much during development, so for now we get a similar effect by using
  -- a naming convention and enforcement via grep and eyeballs.  Maybe one day...
  Meta : ∀{ℓ} → Set ℓ → Set ℓ
  Meta x = x

  -- An EPRound is a 'compound round'; that is,
  -- is a round coupled with an epoch id.  As most of our
  -- proofs are per-epoch so far, these are not used, but
  -- they may be in future.
  EpRound : Set
  EpRound = Epoch × Round

  sucr : EpRound → EpRound
  sucr (e , r) = (e , suc r)

  epr-epoch : EpRound → Epoch
  epr-epoch = proj₁

  epr-round : EpRound → Round
  epr-round = proj₂

  epr₀ : EpRound
  epr₀ = (0 , 0)

  -- Compound rounds admit a total order
  data _<ER_ : EpRound → EpRound → Set where
    ince : ∀{e₀ e₁ r₀ r₁} → e₀ < e₁ → (e₀ , r₀) <ER (e₁ , r₁)
    incr : ∀{e r₀ r₁}     → r₀ < r₁ → (e  , r₀) <ER (e  , r₁)

  <ER-irrelevant : Irrelevant _<ER_
  <ER-irrelevant (ince x) (ince x₁) = cong ince (<-irrelevant x x₁)
  <ER-irrelevant (ince x) (incr x₁) = ⊥-elim (<-irrefl refl x)
  <ER-irrelevant (incr x) (ince x₁) = ⊥-elim (<-irrefl refl x₁)
  <ER-irrelevant (incr x) (incr x₁) = cong incr (<-irrelevant x x₁)

  <ER-asym : Asymmetric _<ER_
  <ER-asym (ince x) (ince x₁) = <-asym x x₁
  <ER-asym (ince x) (incr x₁) = <-irrefl refl x
  <ER-asym (incr x) (ince x₁) = <-irrefl refl x₁
  <ER-asym (incr x) (incr x₁) = <-asym x x₁

  <ER-trans : Transitive _<ER_
  <ER-trans (ince x) (ince x₁) = ince (<-trans x x₁)
  <ER-trans (ince x) (incr x₁) = ince x
  <ER-trans (incr x) (ince x₁) = ince x₁
  <ER-trans (incr x) (incr x₁) = incr (<-trans x x₁)

  <ER-irrefl : Irreflexive _≡_ _<ER_
  <ER-irrefl refl (ince x) = <-irrefl refl x
  <ER-irrefl refl (incr x) = <-irrefl refl x

  postulate -- prove, if needed/used
    <ER-cmp : Trichotomous _≡_ _<ER_
{- This <ER relation is not currently used. If it turns out to be
   used: TODO-1: finish this proof
    <ER-cmp (e₀ , r₀) (e₁ , r₁) with <-cmp e₀ e₁
    ...| tri≈ e₀≮e₁ refl e₁≮e₀ = {!!} {!!} {!!}
    ...| tri< e₀<e₁ e₀≢e₁ e₁≮e₀ = tri< (ince e₀<e₁) {!!} {!!}
    ...| tri> e₀≮e₁ e₀≢e₁ e₁<e₀ = {!!}

-}
  ep≮epr₀ : ∀{ep} → ¬ (ep <ER epr₀)
  ep≮epr₀ (ince ())
  ep≮epr₀ (incr ())

  _≤ER_ : EpRound → EpRound → Set
  er₀ ≤ER er₁ = er₀ ≡ er₁ ⊎ er₀ <ER er₁

  ≤ER⇒epoch≤ : ∀{er₀ er₁} → er₀ ≤ER er₁ → epr-epoch er₀ ≤ epr-epoch er₁
  ≤ER⇒epoch≤ (inj₁ refl) = ≤-refl
  ≤ER⇒epoch≤ (inj₂ (ince x)) = <⇒≤ x
  ≤ER⇒epoch≤ (inj₂ (incr x)) = ≤-refl

  ≤ER⇒round≤ : ∀{er₀ er₁} → er₀ ≤ER er₁ → epr-epoch er₀ ≡ epr-epoch er₁ → epr-round er₀ ≤ epr-round er₁
  ≤ER⇒round≤ (inj₁ refl) hyp1 = ≤-refl
  ≤ER⇒round≤ (inj₂ (ince x)) refl = ⊥-elim (<-irrefl refl x)
  ≤ER⇒round≤ (inj₂ (incr x)) hyp1 = <⇒≤ x

  ≤ER-intro : ∀{e₀ e₁ r₀ r₁} → e₀ ≤ e₁ → r₀ ≤ r₁ → (e₀ , r₀) ≤ER (e₁ , r₁)
  ≤ER-intro {e0} {e1} {r0} {r1} e r
    with e0 ≟ℕ e1
  ...| no le    = inj₂ (ince (≤∧≢⇒< e le))
  ...| yes refl
    with r0 ≟ℕ r1
  ...| no le    = inj₂ (incr (≤∧≢⇒< r le))
  ...| yes refl = inj₁ refl

  er≤0⇒er≡0 : ∀{er} → er ≤ER epr₀ → er ≡ epr₀
  er≤0⇒er≡0 (inj₁ x) = x
  er≤0⇒er≡0 (inj₂ (ince ()))
  er≤0⇒er≡0 (inj₂ (incr ()))

  <⇒≤ER : ∀{er₀ er₁} → er₀ <ER er₁ → er₀ ≤ER er₁
  <⇒≤ER = inj₂

  ≤ER-refl : Reflexive _≤ER_
  ≤ER-refl = inj₁ refl

  postulate  -- prove, if needed/used
    ≤ER-trans : Transitive _≤ER_

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

module free-group where

import 15-groups
open 15-groups public

{- We state the universal property of the free group on a set X -}

precomp-universal-property-free-group :
  {l1 l2 l3 : Level} (X : UU-Set l1) (F : Group l2) (G : Group l3)
  (f : type-hom-Set X (set-Group F)) →
  hom-Group F G → type-hom-Set X (set-Group G)
precomp-universal-property-free-group X F G f g = (map-hom-Group F G g) ∘ f

universal-property-free-group :
  (l : Level) {l1 l2 : Level} (X : UU-Set l1) (F : Group l2)
  (f : type-hom-Set X (set-Group F)) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-free-group l X F f =
  (G : Group l) → is-equiv (precomp-universal-property-free-group X F G f)

{- We state the universal property of the initial set equipped with a point
   and an automorphism for each x : X. -}

universal-property-initial-pset-with-automorphisms :
  (l : Level) {l1 l2 : Level} (X : UU-Set l1) (Y : UU-Set l2)
  (pt-Y : type-Set Y) (f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-initial-pset-with-automorphisms l X Y pt-Y f =
  (Z : UU-Set l) (pt-Z : type-Set Z) (g : type-Set X → (type-Set Z ≃ type-Set Z)) →
  is-contr
    ( Σ ( type-hom-Set Y Z)
        ( λ h →
          ( Id (h pt-Y) pt-Z) ×
          ( (x : type-Set X) (y : type-Set Y) →
            Id (h (map-equiv (f x) y)) (map-equiv (g x) (h y)))))

map-initial-pset-with-automorphisms :
  { l1 l2 l3 : Level} (X : UU-Set l1) (Y : UU-Set l2) (pt-Y : type-Set Y)
  ( f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  ( {l : Level} →
    universal-property-initial-pset-with-automorphisms l X Y pt-Y f) →
  ( Z : UU-Set l3) (pt-Z : type-Set Z)
  ( g : type-Set X → (type-Set Z ≃ type-Set Z)) →
  type-hom-Set Y Z
map-initial-pset-with-automorphisms
  X Y pt-Y f up-Y Z pt-Z g = pr1 (center (up-Y Z pt-Z g))

preserves-point-map-initial-pset-with-automorphisms :
  { l1 l2 l3 : Level} (X : UU-Set l1) (Y : UU-Set l2) (pt-Y : type-Set Y)
  ( f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  ( up-Y : {l : Level} →
    universal-property-initial-pset-with-automorphisms l X Y pt-Y f) →
  ( Z : UU-Set l3) (pt-Z : type-Set Z)
  ( g : type-Set X → (type-Set Z ≃ type-Set Z)) →
  Id (map-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g pt-Y) pt-Z
preserves-point-map-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g =
  pr1 (pr2 (center (up-Y Z pt-Z g)))

htpy-map-initial-pset-with-automorphisms :
  { l1 l2 l3 : Level} (X : UU-Set l1) (Y : UU-Set l2) (pt-Y : type-Set Y)
  ( f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  ( up-Y : {l : Level} →
    universal-property-initial-pset-with-automorphisms l X Y pt-Y f) →
  ( Z : UU-Set l3) (pt-Z : type-Set Z)
  ( g : type-Set X → (type-Set Z ≃ type-Set Z)) →
  ( x : type-Set X) (y : type-Set Y) →
  Id ( map-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g
       ( map-equiv (f x) y))
     ( map-equiv (g x)
       ( map-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g y))
htpy-map-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g =
  pr2 (pr2 (center (up-Y Z pt-Z g)))

{- We show a dependent elimination property for the initial pointed set with
   an automorphism for each x : X. -}

dependent-up-initial-pset-with-automorphisms :
  { l1 l2 l3 l4 : Level} (X : UU-Set l1) (Y : UU-Set l2) (pt-Y : type-Set Y)
  ( f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  ( up-Y : {l : Level} →
    universal-property-initial-pset-with-automorphisms l X Y pt-Y f) →
  ( Z : UU-Set l3) (pt-Z : type-Set Z)
  ( g : type-Set X → (type-Set Z ≃ type-Set Z)) →
  ( P : type-Set Z → UU-Set l4)
  ( p : type-Set (P pt-Z))
  ( e : (x : type-Set X) (z : type-Set Z) →
        type-Set (P z) ≃ type-Set (P (map-equiv (g x) z))) →
  ( y : type-Set Y) →
  type-Set (P (map-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g y))
dependent-up-initial-pset-with-automorphisms X Y pt-Y f up-Y Z pt-Z g P p e =
  {!!}

{- We show that the initial set equipped with a point and an automorphism for
   each x : X is a group. -}

mul-initial-pset-with-automorphisms :
  {l1 l2 : Level} (X : UU-Set l1) (Y : UU-Set l2)
  (pt-Y : type-Set Y) (f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  ( {l : Level} →
    universal-property-initial-pset-with-automorphisms l X Y pt-Y f) →
  type-Set Y → type-Set Y → type-Set Y
mul-initial-pset-with-automorphisms {l1} {l2} X Y pt-Y f up-Y =
  map-initial-pset-with-automorphisms
    X Y pt-Y f up-Y (hom-Set Y Y) id
    ( λ x → equiv-postcomp (type-Set Y) (f x))

associative-mul-initial-pset-with-automorphisms :
  {l1 l2 : Level} (X : UU-Set l1) (Y : UU-Set l2)
  (pt-Y : type-Set Y) (f : type-Set X → (type-Set Y ≃ type-Set Y)) →
  ( up-Y : {l : Level} →
    universal-property-initial-pset-with-automorphisms l X Y pt-Y f) →
  ( x y z : type-Set Y) →
  Id ( mul-initial-pset-with-automorphisms X Y pt-Y f up-Y
       ( mul-initial-pset-with-automorphisms X Y pt-Y f up-Y x y) z)
     ( mul-initial-pset-with-automorphisms X Y pt-Y f up-Y x
       ( mul-initial-pset-with-automorphisms X Y pt-Y f up-Y y z))
associative-mul-initial-pset-with-automorphisms X Y pt-Y f up-Y x y z = {!refl!}

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
------------------------------------------------------------------------------
-- Propositional logic theorems
------------------------------------------------------------------------------

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

-- This module contains some examples showing the use of the ATPs to
-- prove theorems from propositional logic.

module FOL.PropositionalLogic.TheoremsATP where

open import FOL.Base

------------------------------------------------------------------------------
-- We postulate some propositional formulae (which are translated as
-- 0-ary predicates).
postulate P Q R : Set

------------------------------------------------------------------------------
-- The introduction and elimination rules for the intuitionist
-- propositional connectives are theorems.

postulate
  →I  : (P → Q) → P → Q
  →E  : (P → Q) → P → Q
  →I' : (P → Q) → P → Q
  →E' : (P ⇒ Q) ⇒ P ⇒ Q
{-# ATP prove →I #-}
{-# ATP prove →E #-}
{-# ATP prove →I' #-}
{-# ATP prove →E' #-}

postulate
  ∧I   : P → Q → P ∧ Q
  ∧E₁  : P ∧ Q → P
  ∧E₂  : P ∧ Q → Q
  ∧I'  : P ⇒ Q ⇒ P ∧ Q
  ∧E₂' : P ∧ Q ⇒ Q
  ∧E₁' : P ∧ Q ⇒ P
{-# ATP prove ∧I #-}
{-# ATP prove ∧E₁ #-}
{-# ATP prove ∧E₂ #-}
{-# ATP prove ∧I' #-}
{-# ATP prove ∧E₁' #-}
{-# ATP prove ∧E₂' #-}

postulate
  ∨I₁  : P → P ∨ Q
  ∨I₂  : Q → P ∨ Q
  ∨E   : (P → R) → (Q → R) → P ∨ Q → R
  ∨I₁' : P ⇒ P ∨ Q
  ∨I₂' : Q ⇒ P ∨ Q
  ∨E'  : (P ⇒ R) ⇒ (Q ⇒ R) ⇒ P ∨ Q ⇒ R
{-# ATP prove ∨I₁ #-}
{-# ATP prove ∨I₂ #-}
{-# ATP prove ∨E #-}
{-# ATP prove ∨I₁' #-}
{-# ATP prove ∨I₂' #-}
{-# ATP prove ∨E' #-}

postulate
  ⊥E  : ⊥ → P
  ⊥E' : ⊥ ⇒ P
{-# ATP prove ⊥E #-}
{-# ATP prove ⊥E' #-}

------------------------------------------------------------------------------
-- Boolean laws (there are some non-intuitionistic laws)

postulate
  ∧-ident : P ∧ ⊤       ↔ P
  ∨-ident : P ∨ ⊥       ↔ P
  ∧-dom   : P ∧ ⊥       ↔ ⊥
  ∨-dom   : P ∨ ⊤       ↔ ⊤
  ∧-idemp : P ∧ P       ↔ P
  ∨-idemp : P ∨ P       ↔ P
  dn      : ¬ ¬ P       ↔ P
  ∧-comm  : P ∧ Q       → Q ∧ P
  ∨-comm  : P ∨ Q       → Q ∨ P
  ∧-assoc : (P ∧ Q) ∧ R ↔ P ∧ Q ∧ R
  ∨-assoc : (P ∨ Q) ∨ R ↔ P ∨ Q ∨ R
  ∧∨-dist : P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R
  ∨∧-dist : P ∨ Q ∧ R   ↔ (P ∨ Q) ∧ (P ∨ R)
  DM₁     : ¬ (P ∨ Q)   ↔ ¬ P ∧ ¬ Q
  DM₂     : ¬ (P ∧ Q)   ↔ ¬ P ∨ ¬ Q
  abs₁    : P ∨ P ∧ Q   ↔ P
  abs₂    : P ∧ (P ∨ Q) ↔ P
  ∧-neg   : P ∧ ¬ P     ↔ ⊥
  ∨-neg   : P ∨ ¬ P     ↔ ⊤
{-# ATP prove ∧-ident #-}
{-# ATP prove ∨-ident #-}
{-# ATP prove ∧-dom #-}
{-# ATP prove ∨-dom #-}
{-# ATP prove ∧-idemp #-}
{-# ATP prove ∨-idemp #-}
{-# ATP prove dn #-}
{-# ATP prove ∧-comm #-}
{-# ATP prove ∨-comm #-}
{-# ATP prove ∧-assoc #-}
{-# ATP prove ∨-assoc #-}
{-# ATP prove ∧∨-dist #-}
{-# ATP prove ∨∧-dist #-}
{-# ATP prove DM₁ #-}
{-# ATP prove DM₂ #-}
{-# ATP prove abs₁ #-}
{-# ATP prove abs₂ #-}
{-# ATP prove ∧-neg #-}
{-# ATP prove ∨-neg #-}

------------------------------------------------------------------------------
-- Theorems related with the definition of logical connectives in
-- terms of others

postulate
  ↔-def  : (P ↔ Q) ↔ (P → Q) ∧ (Q → P)
  →-def  : P → Q   ↔ ¬ P ∨ Q
  ∨₁-def : P ∨ Q   ↔ ¬ P → Q
  ∨₂-def : P ∨ Q   ↔ ¬ (¬ P ∧ ¬ Q)
  ∧-def  : P ∧ Q   ↔ ¬ (¬ P ∨ ¬ Q)
  ¬-def  : ¬ P     ↔ P → ⊥
  ⊥-def  : ⊥       ↔ P ∧ ¬ P
  ⊤-def  : ⊤       ↔ ¬ ⊥
{-# ATP prove ↔-def #-}
{-# ATP prove →-def #-}
{-# ATP prove ∨₁-def #-}
{-# ATP prove ∨₂-def #-}
{-# ATP prove ∧-def #-}
{-# ATP prove ¬-def #-}
{-# ATP prove ⊥-def #-}
{-# ATP prove ⊤-def #-}

------------------------------------------------------------------------------
-- Some intuitionistic theorems

postulate →-transposition : (P → Q) → ¬ Q → ¬ P
{-# ATP prove →-transposition #-}

postulate
  i₁ : P → Q → P
  i₂ : (P → Q → R) → (P → Q) → P → R
  i₃ : P → ¬ ¬ P
  i₄ : ¬ ¬ ¬ P → ¬ P
  i₅ : ((P ∧ Q) → R) ↔ (P → (Q → R))
  i₆ : ¬ ¬ (P ∨ ¬ P)
  i₇ : (P ∨ ¬ P) → ¬ ¬ P → P
{-# ATP prove i₁ #-}
{-# ATP prove i₂ #-}
{-# ATP prove i₃ #-}
{-# ATP prove i₄ #-}
{-# ATP prove i₅ #-}
{-# ATP prove i₆ #-}
{-# ATP prove i₇ #-}

------------------------------------------------------------------------------
-- Some non-intuitionistic theorems

postulate ←-transposition : (¬ Q → ¬ P) → P → Q
{-# ATP prove ←-transposition #-}

postulate
  ni₁ : ((P → Q) → P) → P
  ni₂ : P ∨ ¬ P
  ni₃ : ¬ ¬ P → P
  ni₄ : (P → Q) → (¬ P → Q) → Q
  ni₅ : (P ∨ Q → P) ∨ (P ∨ Q → Q)
  ni₆ : (¬ ¬ P → P) → P ∨ ¬ P
{-# ATP prove ni₁ #-}
{-# ATP prove ni₂ #-}
{-# ATP prove ni₃ #-}
{-# ATP prove ni₄ #-}
{-# ATP prove ni₅ #-}
{-# ATP prove ni₆ #-}

------------------------------------------------------------------------------
-- The principle of the excluded middle implies the double negation
-- elimination
postulate
  pem→¬¬-elim : (P ∨ ¬ P) → ¬ ¬ P → P
{-# ATP prove pem→¬¬-elim #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Product where

open import Base
open import Category
open import Unique
open import Dual

module Prod (ℂ : Cat) where

  private
    ℂ' = η-Cat ℂ
    open module C = Cat ℂ'
    open module U = Uniq ℂ'

  data _×_ (A B : Obj) : Set1 where
    prod : (AB : Obj)
	   (π₀ : AB ─→ A)
	   (π₁ : AB ─→ B) ->
	   ((X : Obj)(f : X ─→ A)(g : X ─→ B) ->
	    ∃! \(h : X ─→ AB) -> π₀ ∘ h == f /\ π₁ ∘ h == g
	   ) -> A × B

  Product : {A B : Obj} -> A × B -> Obj
  Product (prod AB _ _ _) = AB

  π₀ : {A B : Obj}(p : A × B) -> Product p ─→ A
  π₀ (prod _ p _ _) = p

  π₁ : {A B : Obj}(p : A × B) -> Product p ─→ B
  π₁ (prod _ _ q _) = q

module Sum (ℂ : Cat) = Prod (η-Cat ℂ op)
    renaming ( _×_     to _+_
	     ; prod    to sum
	     ; Product to Sum
	     ; π₀      to inl
	     ; π₁      to inr
	     )

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

module FinEquivPlusTimes where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_,_; _×_; proj₁; proj₂)

open import Data.Nat
  using (ℕ; zero; suc; _+_; _*_; _<_; _≤_; ≤-pred; _≥_; _≤?_;
         module ≤-Reasoning)
open import Data.Nat.DivMod using (_divMod_; result)
open import Data.Nat.Properties using (≰⇒>; 1+n≰n; m≤m+n; ¬i+1+j≤i)
open import Data.Nat.Properties.Simple
  using (+-assoc; +-suc; +-comm; *-right-zero)

open import Data.Fin
  using (Fin; zero; suc; inject+; raise; toℕ; fromℕ≤; reduce≥)
open import Data.Fin.Properties
  using (bounded; inject+-lemma; toℕ-raise; toℕ-injective; toℕ-fromℕ≤)

open import Function using (_∘_; id; case_of_)
open import Relation.Nullary using (yes; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; subst;
         module ≡-Reasoning; inspect; [_])

--

open import Equiv using (_∼_; _≃_; qinv; id≃; sym≃; _●_; _⊎≃_)

open import Proofs using (
  -- LeqLemmas
  _<?_; cong+r≤; cong+l≤; cong*r≤;
  -- FinNatLemmas
  inj₁-≡; inj₂-≡; inject+-injective; raise-injective; addMul-lemma
  )

------------------------------------------------------------------------------
-- Additive unit and multiplicative unit are Fin 0 and Fin 1 which are
-- equivalent to ⊥ and ⊤

abstract

  Fin0-⊥ : Fin 0 → ⊥
  Fin0-⊥ ()

  F0≃⊥ : Fin 0 ≃ ⊥
  F0≃⊥ = f , qinv g α β
    where
      f : Fin 0 → ⊥
      f ()
      g : ⊥ → Fin 0
      g ()
      α : f ∘ g ∼ id
      α ()
      β : g ∘ f ∼ id
      β ()

  Fin1≃⊤ : Fin 1 ≃ ⊤
  Fin1≃⊤ = f , qinv g α β
    where
      f : Fin 1 → ⊤
      f zero = tt
      f (suc ())
      g : ⊤ → Fin 1
      g tt = zero
      α : f ∘ g ∼ id
      α tt = refl
      β : g ∘ f ∼ id
      β zero = refl
      β (suc ())

------------------------------------------------------------------------------
-- Additive monoid

module Plus where

  -- Main goal is to show (Fin m ⊎ Fin n) ≃ Fin (m + n) It is then
  -- fairly easy to show that ⊎ satisfies the commutative monoid
  -- axioms

  private

    fwd : {m n : ℕ} → (Fin m ⊎ Fin n) → Fin (m + n)
    fwd {m} {n} (inj₁ x) = inject+ n x
    fwd {m} {n} (inj₂ y) = raise m y

    bwd : {m n : ℕ} → Fin (m + n) → (Fin m ⊎ Fin n)
    bwd {m} {n} = λ i → case (toℕ i <? m) of λ
      { (yes p) → inj₁ (fromℕ≤ p)
       ; (no ¬p) → inj₂ (reduce≥ i (≤-pred (≰⇒> ¬p)))
       }

    fwd∘bwd~id : {m n : ℕ} → fwd {m} {n} ∘ bwd ∼ id
    fwd∘bwd~id {m} i with toℕ i <? m
    fwd∘bwd~id i | yes p = sym (inj₁-≡ i p)
    fwd∘bwd~id i | no ¬p = sym (inj₂-≡ i (≤-pred (≰⇒> ¬p)))

    bwd∘fwd~id : {m n : ℕ} → bwd {m} {n} ∘ fwd ∼ id
    bwd∘fwd~id {m} {n} (inj₁ x) with toℕ (inject+ n x) <? m
    bwd∘fwd~id {n = n} (inj₁ x) | yes p =
       cong inj₁
         (inject+-injective (fromℕ≤ p) x (sym (inj₁-≡ (inject+ n x) p)))
    bwd∘fwd~id {m} {n} (inj₁ x) | no ¬p = ⊥-elim (1+n≰n pf)
     where
       open ≤-Reasoning
       pf : suc (toℕ x) ≤ toℕ x
       pf = let q =  (≤-pred (≰⇒> ¬p)) in
              begin (
                suc (toℕ x)
                  ≤⟨ bounded x ⟩
                m
                  ≤⟨ q ⟩
                toℕ (inject+ n x)
                  ≡⟨ sym (inject+-lemma n x) ⟩
                toℕ x ∎ )
    bwd∘fwd~id {m} {n} (inj₂ y) with toℕ (raise m y) <? m
    bwd∘fwd~id {m} {n} (inj₂ y) | yes p = ⊥-elim (1+n≰n pf)
     where
       open ≤-Reasoning
       pf : suc m ≤ m
       pf = begin (
               suc m
                   ≤⟨ m≤m+n (suc m) (toℕ y) ⟩
               suc (m + toℕ y)
                   ≡⟨ cong suc (sym (toℕ-raise m y)) ⟩
               suc (toℕ (raise m y))
                   ≤⟨ p ⟩
               m ∎)
    bwd∘fwd~id {m} {n} (inj₂ y) | no ¬p =
       cong inj₂
         (raise-injective {m}
           (reduce≥ (raise m y) (≤-pred (≰⇒> ¬p)))
           y
           (sym (inj₂-≡ (raise m y) (≤-pred (≰⇒> ¬p)))))

   -- the main equivalence
  abstract
    fwd-iso : {m n : ℕ} → (Fin m ⊎ Fin n) ≃ Fin (m + n)
    fwd-iso {m} {n} = fwd , qinv bwd (fwd∘bwd~id {m}) (bwd∘fwd~id {m})

  -- aliases for the above which are more convenient
  ⊎≃+ : {m n : ℕ} → (Fin m ⊎ Fin n) ≃ Fin (m + n)
  ⊎≃+ = fwd-iso

  +≃⊎ : {m n : ℕ} → Fin (m + n) ≃ (Fin m ⊎ Fin n)
  +≃⊎ = sym≃ fwd-iso

-----------------------------------------------------------------------------
-- Multiplicative monoid

module Times where

  -- main goal is to show (Fin m × Fin n) ≃ Fin (m * n) It is then
  -- fairly easy to show that × satisfies the commutative monoid
  -- axioms

  private

    fwd : {m n : ℕ} → (Fin m × Fin n) → Fin (m * n)
    fwd {suc m} {n} (zero , k) = inject+ (m * n) k
    fwd {n = n} (suc i , k) = raise n (fwd (i , k))

    soundness : ∀ {m n} (i : Fin m) (j : Fin n) →
                toℕ (fwd (i , j)) ≡ toℕ i * n + toℕ j
    soundness {suc m} {n} zero     j = sym (inject+-lemma (m * n) j)
    soundness {n = n} (suc i) j
      rewrite toℕ-raise n (fwd (i , j)) | soundness i j
      = sym (+-assoc n (toℕ i * n) (toℕ j))

    absurd-quotient : (m n q : ℕ) (r : Fin (suc n)) (k : Fin (m * suc n))
         (k≡r+q*sn : toℕ k ≡ toℕ r + q * suc n) (p : m ≤ q) → ⊥
    absurd-quotient m n q r k k≡r+q*sn p = ¬i+1+j≤i (toℕ k) {toℕ r} k≥k+sr
      where k≥k+sr : toℕ k ≥ toℕ k + suc (toℕ r)
            k≥k+sr = begin (toℕ k + suc (toℕ r)
                       ≡⟨ +-suc (toℕ k) (toℕ r) ⟩
                     suc (toℕ k) + toℕ r
                       ≤⟨ cong+r≤ (bounded k) (toℕ r) ⟩
                     (m * suc n) + toℕ r
                       ≡⟨ +-comm (m * suc n) (toℕ r) ⟩
                     toℕ r + (m * suc n)
                       ≡⟨ refl ⟩
                     toℕ r + m * suc n
                       ≤⟨ cong+l≤ (cong*r≤ p (suc n)) (toℕ r) ⟩
                     toℕ r + q * suc n
                       ≡⟨ sym k≡r+q*sn ⟩
                     toℕ k ∎)
                      where open ≤-Reasoning

    elim-right-zero : ∀ {ℓ} {Whatever : Set ℓ}
                      (m : ℕ) → Fin (m * 0) → Whatever
    elim-right-zero m i = ⊥-elim (Fin0-⊥ (subst Fin (*-right-zero m) i))

    bwd : {m n : ℕ} → Fin (m * n) → (Fin m × Fin n)
    bwd {m} {0} k = elim-right-zero m k
    bwd {m} {suc n} k with toℕ k | inspect toℕ k | (toℕ k) divMod (suc n)
    bwd {m} {suc n} k | .(toℕ r + q * suc n) | [ pf ] | result q r refl =
      (fromℕ≤ {q} {m} q<m , r)
      where q<m : q < m
            q<m with suc q ≤? m
            ... | no ¬p = ⊥-elim (absurd-quotient m n q r k pf (≤-pred (≰⇒> ¬p)))
            ... | yes p = p

    fwd∘bwd~id : {m n : ℕ} → fwd {m} {n} ∘ bwd ∼ id
    fwd∘bwd~id {m} {zero} i = elim-right-zero m i
    fwd∘bwd~id {m} {suc n} i with toℕ i | inspect toℕ i | (toℕ i) divMod (suc n)
    fwd∘bwd~id {m} {suc n} i | .(toℕ r + q * suc n) | [ eq ] | result q r refl
      with suc q ≤? m
    ... | no ¬p = ⊥-elim (absurd-quotient m n q r i eq (≤-pred (≰⇒> ¬p)))
    ... | yes p = toℕ-injective (
       begin (
          toℕ (fwd (fromℕ≤ {q} {m} p , r))
            ≡⟨ soundness (fromℕ≤ p) r ⟩
          toℕ (fromℕ≤ p) * (suc n) + toℕ r
            ≡⟨ cong (λ x → x * (suc n) + toℕ r) (toℕ-fromℕ≤ p) ⟩
          q * (suc n) + toℕ r
            ≡⟨ +-comm _ (toℕ r) ⟩
          toℕ r  + q * (suc n)
            ≡⟨ sym eq ⟩
          toℕ i ∎))
       where open ≡-Reasoning

    bwd∘fwd~id : {m n : ℕ} → (x : Fin m × Fin n) →
        bwd {m} {n} (fwd x) ≡ id x
    bwd∘fwd~id {m} {zero} (b , ())
    bwd∘fwd~id {m} {suc n} (b , d) with toℕ (fwd (b , d)) | inspect toℕ (fwd (b , d)) | (toℕ (fwd (b , d)) divMod (suc n))
    bwd∘fwd~id {m} {suc n} (b , d) | .(toℕ r + q * suc n) | [ eqk ] | result q r refl with q <? m
    ... | no ¬p = ⊥-elim (absurd-quotient m n q r (fwd (b , d)) eqk (≤-pred (≰⇒> ¬p)))
    ... | yes p =
        begin (
          (fromℕ≤ {q} {m} p , r)
            ≡⟨ cong₂ _,_ pf₁ (proj₁ same-quot) ⟩
          (b , d) ∎)
      where
        open ≡-Reasoning
        eq' : toℕ d + toℕ b * suc n ≡ toℕ r + q * suc n
        eq' = begin (
          toℕ d + toℕ b * suc n
            ≡⟨ +-comm (toℕ d) _ ⟩
          toℕ b * suc n + toℕ d
            ≡⟨ sym (soundness b d) ⟩
          toℕ (fwd (b , d))
            ≡⟨ eqk ⟩
          toℕ r + q * suc n ∎ )
        same-quot : (r ≡ d) × (q ≡ toℕ b)
        same-quot = addMul-lemma q (toℕ b) n r d ( sym eq' )
        pf₁ = toℕ-injective (trans (toℕ-fromℕ≤ p) (proj₂ same-quot))

  abstract
    fwd-iso : {m n : ℕ} → (Fin m × Fin n) ≃ Fin (m * n)
    fwd-iso {m} {n} = fwd , qinv bwd (fwd∘bwd~id {m}) (bwd∘fwd~id {m})

  -- convenient aliases
  ×≃* : {m n : ℕ} → (Fin m × Fin n) ≃ Fin (m * n)
  ×≃* = fwd-iso

  *≃× : {m n : ℕ} → Fin (m * n) ≃ (Fin m × Fin n)
  *≃× = sym≃ ×≃*

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Data.Product using ( _×_ ; _,_ ; swap )
open import Relation.Nullary using ( ¬_ )
open import Web.Semantic.DL.ABox using ( ABox ; ε ; _,_ ; _∼_ ; _∈₁_ ; _∈₂_ )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ )
open import Web.Semantic.DL.Concept using
  ( Concept ; ⟨_⟩ ; ¬⟨_⟩ ; ⊤ ; ⊥ ; _⊔_ ; _⊓_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1 ; >1 ; neg )
open import Web.Semantic.DL.KB using ( KB ; tbox ; abox )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Role using ( Role ; ⟨_⟩ ; ⟨_⟩⁻¹ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using
  ( TBox ; ε ; _,_ ; _⊑₁_ ; _⊑₂_ ; Dis ; Ref ; Irr ; Tra )

module Web.Semantic.DL.Integrity.Closed.Alternate
  {Σ : Signature} {X : Set} where

-- An alternate definition of closed-world integrity.

infixr 4 _,_
infix 2 _⊫_∈₂_ _⊫_∈₁_ _⊫a_ _⊫t_

data _⊫_∼_ (K : KB Σ X) (x y : X) : Set₁ where
  eq : (∀ I → (I ⊨ K) → (I ⊨a x ∼ y)) → (K ⊫ x ∼ y)

data _⊫_∈₂_ (K : KB Σ X) (xy : X × X) : Role Σ → Set₁ where
  rel : ∀ {r} → (∀ I → (I ⊨ K) → (I ⊨a xy ∈₂ r)) → (K ⊫ xy ∈₂ ⟨ r ⟩)
  rev : ∀ {r} → (∀ I → (I ⊨ K) → (I ⊨a swap xy ∈₂ r)) → (K ⊫ xy ∈₂ ⟨ r ⟩⁻¹)

data _⊫_∈₁_ (K : KB Σ X) (x : X) : Concept Σ → Set₁ where
  +atom : ∀ {c} → (∀ I → (I ⊨ K) → (I ⊨a x ∈₁ c)) → (K ⊫ x ∈₁ ⟨ c ⟩)
  -atom : ∀ {c} → ¬(∀ I → (I ⊨ K) → (I ⊨a x ∈₁ c)) → (K ⊫ x ∈₁ ¬⟨ c ⟩)
  top : (K ⊫ x ∈₁ ⊤)
  inj₁ : ∀ {C D} → (K ⊫ x ∈₁ C) → (K ⊫ x ∈₁ C ⊔ D)
  inj₂ : ∀ {C D} → (K ⊫ x ∈₁ D) → (K ⊫ x ∈₁ C ⊔ D)
  _,_ : ∀ {C D} → (K ⊫ x ∈₁ C) → (K ⊫ x ∈₁ D) → (K ⊫ x ∈₁ C ⊓ D)
  all : ∀ {R C} → (∀ y → (K ⊫ (x , y) ∈₂ R) → (K ⊫ y ∈₁ C)) → (K ⊫ x ∈₁ ∀[ R ] C)
  ex : ∀ {R C} y → (K ⊫ (x , y) ∈₂ R) → (K ⊫ y ∈₁ C) → (K ⊫ x ∈₁ ∃⟨ R ⟩ C)
  uniq : ∀ {R} → (∀ y z → (K ⊫ (x , y) ∈₂ R) → (K ⊫ (x , z) ∈₂ R) → (K ⊫ y ∼ z)) → (K ⊫ x ∈₁ ≤1 R)
  ¬uniq : ∀ {R} y z → (K ⊫ (x , y) ∈₂ R) → (K ⊫ (x , z) ∈₂ R) → ¬(K ⊫ y ∼ z) → (K ⊫ x ∈₁ >1 R)

data _⊫a_ (K : KB Σ X) : ABox Σ X → Set₁ where
  ε : (K ⊫a ε)
  _,_ : ∀ {A B} → (K ⊫a A) → (K ⊫a B) → (K ⊫a A , B)
  eq : ∀ x y → (K ⊫ x ∼ y) → (K ⊫a x ∼ y)
  rl : ∀ xy r → (K ⊫ xy ∈₂ ⟨ r ⟩) → (K ⊫a xy ∈₂ r)
  cn : ∀ x c → (K ⊫ x ∈₁ ⟨ c ⟩) → (K ⊫a x ∈₁ c)

data _⊫t_ (K : KB Σ X) : TBox Σ → Set₁ where
  ε : (K ⊫t ε)
  _,_ : ∀ {T U} → (K ⊫t T) → (K ⊫t U) → (K ⊫t T , U)
  rl : ∀ Q R → (∀ xy → (K ⊫ xy ∈₂ Q) → (K ⊫ xy ∈₂ R)) → (K ⊫t Q ⊑₂ R)
  cn : ∀ C D → (∀ x → (K ⊫ x ∈₁ neg C ⊔ D)) → (K ⊫t C ⊑₁ D)
  dis : ∀ Q R → (∀ xy → (K ⊫ xy ∈₂ Q) → ¬(K ⊫ xy ∈₂ R)) → (K ⊫t Dis Q R)
  ref : ∀ R → (∀ x → (K ⊫ (x , x) ∈₂ R)) → (K ⊫t Ref R)
  irr : ∀ R → (∀ x → ¬(K ⊫ (x , x) ∈₂ R)) → (K ⊫t Irr R)
  tra : ∀ R → (∀ x y z → (K ⊫ (x , y) ∈₂ R) → (K ⊫ (y , z) ∈₂ R) → (K ⊫ (x , z) ∈₂ R)) → (K ⊫t Tra R)

data _⊫k_ (K L : KB Σ X) : Set₁ where
  _,_ : (K ⊫t tbox L) → (K ⊫a abox L) → (K ⊫k L)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Ag02 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎

+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

+-identityʳ : ∀ (m : ℕ) → m + 0 ≡ m
+-identityʳ zero =
  begin
    zero + 0
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ +-assoc m n (p + q) ⟩
    m + (n + (p + q))
  ≡⟨ cong (m +_) (sym (+-assoc n p q)) ⟩
    m + ((n + p) + q)
  ≡⟨ sym (+-assoc m (n + p) q) ⟩
    m + (n + p) + q
  ∎

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p                           = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p rewrite sym (+-assoc m n p) | +-comm m n | +-assoc n m p = refl

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ 0 n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc 0 n p = refl
*-assoc (suc m) n p rewrite  *-distrib-+ n (m * n) p | *-assoc m n p = refl

*-identityʳ : ∀ (n : ℕ) → n * 0 ≡ 0
*-identityʳ 0 = refl
*-identityʳ (suc n) rewrite *-identityʳ n = refl

*-suc : ∀ (m n : ℕ) → m * (suc n) ≡ m + m * n
*-suc 0 n = refl
*-suc (suc m) n rewrite *-suc m n | +-swap n m (m * n) = refl

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm 0 n rewrite *-identityʳ n = refl
*-comm (suc m) n rewrite *-comm m n | *-suc n m = refl

∸-n : ∀ (n : ℕ) → 0 ∸ n ≡ 0
∸-n zero = refl
∸-n (suc n) = refl

∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc zero n p rewrite ∸-n n | ∸-n p | ∸-n (n + p) = refl
∸-+-assoc (suc m) zero p = refl
∸-+-assoc (suc m) (suc n) p rewrite ∸-+-assoc m n p = refl

^-distrib-+ : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
^-distrib-+ m 0 p rewrite +-identityʳ (m ^ p) = refl
^-distrib-+ m (suc n) p rewrite ^-distrib-+ m n p | *-assoc m (m ^ n) (m ^ p) = refl

^-distrib-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
^-distrib-* m n zero = refl
^-distrib-* m n (suc p) rewrite ^-distrib-* m n p | sym (*-assoc (m * n) (m ^ p) (n ^ p))
  | *-assoc m n (m ^ p) | *-comm n (m ^ p) | *-assoc m ((m ^ p) * n) (n ^ p) | *-assoc (m ^ p) n (n ^ p)
  | *-assoc m (m ^ p) (n * (n ^ p)) = refl

^-identity : ∀ (p : ℕ) → 1 ^ p ≡ 1
^-identity zero = refl
^-identity (suc p) rewrite ^-identity p = refl

^-*-plus : ∀ (m n p : ℕ) → m ^ (n * p) ≡ (m ^ n) ^ p
^-*-plus m zero p rewrite ^-identity p = refl
^-*-plus m (suc n) p rewrite ^-distrib-+ m p (n * p) | ^-*-plus m n p | sym (^-distrib-* m (m ^ n) p) = refl

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil    = x1 nil
inc (x1 b) = x0 (inc b)
inc (x0 b) = x1 b

to : ℕ → Bin
to zero = nil
to (suc m) = inc (to m)

from : Bin → ℕ
from nil      = zero
from (x1 b)   = suc (2 * (from b))
from (x0 b)   = 2 * (from b)

inc-suc : ∀ (x : Bin) → from (inc x) ≡ suc (from x)
inc-suc nil = refl
inc-suc (x0 x) = refl
inc-suc (x1 x) rewrite inc-suc x | +-suc (from x) (from x + 0) = refl

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import Categories.Category.Core

-- Kernel Pair - a Pullback of a morphism along itself
-- https://ncatlab.org/nlab/show/kernel+pair
module Categories.Diagram.KernelPair {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Diagram.Pullback 𝒞

open Category 𝒞

private
  variable
    A B : Obj

-- Make it a pure synonym
KernelPair : (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e)
KernelPair f = Pullback f f

max_stars_repo_name: Trebor-Huang/agda-categories


text:
------------------------------------------------------------------------
-- Total recognisers based on the same principles as the parsers in
-- TotalParserCombinators.Parser
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Recognisers are less complicated than parsers, and the following
-- code should (generally) be easier to follow than the code under
-- TotalParserCombinators.

module TotalRecognisers where

------------------------------------------------------------------------
-- Recognisers which do not support left recursion

-- Very simple recognisers, including a formal semantics and a proof
-- of decidability.

import TotalRecognisers.Simple

-- Proof showing that the set of languages accepted by these
-- recognisers is exactly the set of languages which can be decided by
-- Agda programs (when the alphabet is {true, false}).

import TotalRecognisers.Simple.ExpressiveStrength

-- An example: a right recursive expression grammar.

import TotalRecognisers.Simple.Expression

-- An alternative backend (without correctness proof).

import TotalRecognisers.Simple.AlternativeBackend

------------------------------------------------------------------------
-- Recognisers which do support left recursion

-- More complicated recognisers, which can handle left recursion. (The
-- set of basic combinators is also different: tok has been replaced
-- by sat, and nonempty and cast have been added.)

import TotalRecognisers.LeftRecursion

-- These recognisers have the same (maximal) expressive strength as
-- the simple ones, as long as the alphabet is finite. For infinite
-- alphabets it is shown that the expressive strength is not maximal.

import TotalRecognisers.LeftRecursion.ExpressiveStrength

-- A tiny library of derived combinators.

import TotalRecognisers.LeftRecursion.Lib

-- An example: a left recursive expression grammar.

import TotalRecognisers.LeftRecursion.Expression

-- An example of how nonempty can be used: parsing of matching
-- parentheses, along with a correctness proof.

import TotalRecognisers.LeftRecursion.MatchingParentheses

-- The recognisers form a *-continuous Kleene algebra.

import TotalRecognisers.LeftRecursion.KleeneAlgebra

-- A direct proof which shows that the context-sensitive language
-- { aⁿbⁿcⁿ | n ∈ ℕ } can be decided.

import TotalRecognisers.LeftRecursion.NotOnlyContextFree

max_stars_repo_name: yurrriq/parser-combinators