text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Category where

open import Cubical.Foundations.Prelude

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.Categories.Category renaming (isUnivalent to isUnivalentCat)

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓ≅A ℓB ℓ≅B ℓ≅ᴰ : Level

-- every univalent 1-precategory gives a URGStr
Cat→𝒮 : (𝒞 : Precategory ℓ ℓ') → (uni : isUnivalentCat 𝒞) → URGStr (𝒞 .ob) ℓ'
Cat→𝒮 𝒞 uni
  = urgstr (CatIso {𝒞 = 𝒞}) idCatIso λ x y → isUnivalentCat.univ uni x y

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

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

open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Sets.EquivalenceRelations
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Sequences
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Functions.Definition
open import Fields.Orders.Total.Definition

module Fields.Orders.Limits.Definition {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {c} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {F : Field R} {pRing : PartiallyOrderedRing R pOrder} (oF : TotallyOrderedField F pRing) where

open Ring R
open TotallyOrderedField oF
open TotallyOrderedRing oRing
open PartiallyOrderedRing pRing
open import Rings.Orders.Total.Lemmas oRing
open import Rings.Orders.Total.AbsoluteValue oRing
open import Rings.Orders.Partial.Lemmas pRing
open SetoidTotalOrder total
open SetoidPartialOrder pOrder
open Group additiveGroup
open import Groups.Lemmas additiveGroup
open Setoid S
open Equivalence eq
open Field F
open import Fields.CauchyCompletion.Definition (TotallyOrderedField.oRing oF) F

_~>_ : Sequence A → A → Set (a ⊔ c)
x ~> c = (ε : A) → (0R < ε) → Sg ℕ (λ N → (n : ℕ) → (N <N n) → abs ((index x n) + inverse c) < ε)

1/2 : A
1/2 with allInvertible (1R + 1R) (orderedImpliesCharNot2 nontrivial)
... | a , _ = a

abstract
  1/2is1/2 : (1/2 * (1R + 1R)) ∼ 1R
  1/2is1/2 with allInvertible (1R + 1R) (orderedImpliesCharNot2 nontrivial)
  ... | a , pr = pr

  0<1/2 : 0R < 1/2
  0<1/2 = halvePositive 1/2 (<WellDefined reflexive (symmetric (transitive (transitive (+WellDefined (symmetric (transitive *Commutative identIsIdent)) (symmetric (transitive *Commutative identIsIdent))) (symmetric *DistributesOver+)) 1/2is1/2)) (0<1 nontrivial))

  halfHalves : {a : A} → (1/2 * (a + a)) ∼ a
  halfHalves {a} = transitive (*WellDefined reflexive (+WellDefined (symmetric identIsIdent) (symmetric identIsIdent))) (transitive (*WellDefined reflexive (symmetric *DistributesOver+')) (transitive *Associative (transitive (*WellDefined 1/2is1/2 reflexive) identIsIdent)))

abstract
  bothNearImpliesNear : {t r s : A} (e : A) .(0<e : 0R < e) → (abs (r + inverse t) < e) → (abs (s + inverse t) < e) → abs (r + inverse s) < (e + e)
  bothNearImpliesNear {t} {r} {s} e 0<e rNearT sNearT = u
    where
      pr : ((abs (r + inverse t)) + (abs (s + inverse t))) < (e + e)
      pr = ringAddInequalities rNearT sNearT
      t' : (abs (r + inverse t) + abs (t + inverse s)) < (e + e)
      t' = <WellDefined (+WellDefined reflexive (transitive (absNegation _) (absWellDefined _ _ (transitive invContravariant (+WellDefined (invTwice _) reflexive))))) reflexive pr
      u : abs (r + inverse s) < (e + e)
      u with triangleInequality (r + inverse t) (t + inverse s)
      ... | inl t'' = <Transitive (<WellDefined (absWellDefined _ _ (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive))) reflexive t'') t'
      ... | inr eq = <WellDefined (transitive (symmetric eq) (absWellDefined _ _ (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive)))) reflexive t'

private
  limitsUniqueLemma : (x : Sequence A) {r s : A} (xr : x ~> r) (xs : x ~> s) (r<s : r < s) → False
  limitsUniqueLemma x {r} {s} xr xs r<s = irreflexive (<WellDefined reflexive (symmetric prE) u')
    where
      e : A
      e = 1/2 * (s + inverse r)
      prE : (s + inverse r) ∼ (e + e)
      prE = transitive (symmetric halfHalves) *DistributesOver+
      0<e : 0R < e
      0<e = orderRespectsMultiplication 0<1/2 (moveInequality r<s)
      abstract
        N1 : ℕ
        N1 with xs e 0<e
        ... | x , _ = x
        N1prop : (n : ℕ) → (N1 <N n) → abs (index x n + inverse s) < e
        N1prop with xs e 0<e
        ... | x , pr = pr
        N2 : ℕ
        N2 with xr e 0<e
        ... | x , _ = x
        N2prop : (n : ℕ) → (N2 <N n) → abs (index x n + inverse r) < e
        N2prop with xr e 0<e
        ... | x , pr = pr
      good : ℕ
      good = succ (N1 +N N2)
      N1Good : abs (index x good + inverse s) < e
      N1Good = N1prop good (le N2 (applyEquality succ (Semiring.commutative ℕSemiring N2 N1)))
      N2Good : abs (index x good + inverse r) < e
      N2Good = N2prop good (le N1 refl)
      t : ((abs (index x good + inverse s)) + (abs (index x good + inverse r))) < (e + e)
      t = ringAddInequalities N1Good N2Good
      t' : ((abs (index x good + inverse s)) + (abs (r + inverse (index x good)))) < (e + e)
      t' = <WellDefined (+WellDefined reflexive (transitive (absNegation _) (absWellDefined _ _ (transitive invContravariant (+WellDefined (invTwice _) reflexive))))) reflexive t
      u : abs (inverse s + r) < (e + e)
      u with triangleInequality (index x good + inverse s) (r + inverse (index x good))
      ... | inl t'' = <Transitive (<WellDefined (absWellDefined _ _ (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined (symmetric +Associative) reflexive) (transitive (+WellDefined (transitive (+WellDefined reflexive invLeft) identRight) reflexive) groupIsAbelian))))) reflexive t'') t'
      ... | inr eq = <WellDefined (transitive (symmetric eq) (absWellDefined _ _ (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined (symmetric +Associative) reflexive) (transitive (+WellDefined (transitive (+WellDefined reflexive invLeft) identRight) reflexive) groupIsAbelian)))))) reflexive t'
      u' : (s + inverse r) < (e + e)
      u' = <WellDefined (transitive (absNegation _) (transitive (absWellDefined _ _ (transitive invContravariant (transitive groupIsAbelian (+WellDefined (invTwice _) reflexive)))) (symmetric (greaterZeroImpliesEqualAbs (moveInequality r<s))))) reflexive u

limitsAreUnique : (x : Sequence A) → {r s : A} → (x ~> r) → (x ~> s) → r ∼ s
limitsAreUnique x {r} {s} xr xs with totality r s
limitsAreUnique x {r} {s} xr xs | inl (inl r<s) = exFalso (limitsUniqueLemma x xr xs r<s)
limitsAreUnique x {r} {s} xr xs | inl (inr s<r) = exFalso (limitsUniqueLemma x xs xr s<r)
limitsAreUnique x {r} {s} xr xs | inr r=s = r=s

constantSequenceConverges : (a : A) → constSequence a ~> a
constantSequenceConverges a e 0<e = 0 , λ n _ → <WellDefined (symmetric (transitive (absWellDefined _ _ (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst a n)) reflexive) invRight)) absZeroIsZero)) reflexive 0<e

ext: agda


text:
module FStream.Clocked where

open import Library
open import FStream.Core

mutual
  record ClSF {i : Size} {ℓ₁ ℓ₂} {Cl : Set ℓ₂}  (C : Container ℓ₁) (cl : FStream C Cl) (A B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    inductive
    field
      inFCl : A → ⟦ C ⟧ (ClSF' {i} C cl A B)
  record ClSF' {i : Size} {ℓ₁ ℓ₂} {Cl : Set ℓ₂}  (C : Container ℓ₁) (cl : FStream C Cl) (A B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    coinductive
    field
      head : B
      tail : {j : Size< i} → ClSF {j} C cl A B
open FStream public
open FStream' public

_>>>_ : ∀ {i : Size} {ℓ₁ ℓ₂} {a b c Cl : Set ℓ₂} {C : Container ℓ₁} {cl : FStream C Cl} → ClSF {i} C cl a b → ClSF {i} C cl b c → ClSF {i} C cl a c
_>>>_ = {!!}

-- runClock : ∀ {i : Size} {ℓ₁ ℓ₂} {Cl B : Set ℓ₂} {C : Container ℓ₁} → (cl : FStream C Cl) → ClSF {i} C cl A B → FStream {i} C A -> FStream {i} C B
runClock : ∀ {i : Size} {ℓ₁ ℓ₂} {A B Cl : Set ℓ₂} {C : Container ℓ₁} → (cl : FStream C Cl) → ClSF {i} C cl A B → FStream {i} C A -> FStream {i} C B
runClock = {!!}

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


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

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

postulate
  A : Set
  a b c : A
  f g : A → A

  rew₁ : f a ≡ b
  rew₂ : ∀ {x} → f (g x) ≡ c
  rew₃ : g a ≡ a

{-# REWRITE rew₁ #-}
{-# REWRITE rew₂ #-}
{-# REWRITE rew₃ #-}

works : (x : A) → f (g x) ≡ c
works x = refl

works' : f (g a) ≡ c
works' = works a

fails : f (g a) ≡ c
fails = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Mendler (F : Set → Set) where
open import Data.Product using (_×_)

Alg : Set → Set₁
Alg X = ∀ (R : Set) → (R → X) → F R → X

test : Set → Set
test A = A × A

test′ : ∀ (R : Set) → Set
test′ A = A × A


text:
--{-# OPTIONS -vtc:50 #-}
{-# OPTIONS --double-check #-}

open import Agda.Primitive

postulate Id : (l : Level) (A : Set l) → A → A → Set l

postulate w/e : (l : Level) (A : Set l) → A

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

unbox : (l : Level) (A : Set l) → Box l A → A
unbox l A (box x) = x

record R l (A : Set l) : Set l where
  --no-eta-equality
  -- ^ works if eta is disabled
  field
    boxed : Box l A
    refl  : Id l A (w/e l A) (w/e l A)

postulate
  El    : (l : Level) (A : Set l) → A → A
  trans : (l : Level) (A : Set l) (x : A) → Id l A (w/e l A) (w/e l A) → Id l A (w/e l A) (w/e l A) → Id l A (w/e l A) (w/e l A)
  cong  : (l : Level) (A : Set l) (f : A → A) (x y : A) → Id l A x y → Id l A (f x) (f y)

module _ (l : Level) (BADNESS : Set) (A : Set l) (r : R l A) where

  open R r

  x = w/e l A

  p = trans l A (unbox l A boxed) refl refl

  lemma = El l
            (Id l (Id l A x x) p p)
            (cong l _ (λ p → trans l A (unbox l A boxed) p _) refl refl (w/e l (Id l (Id l A x x) refl refl)))
  -- ^ works if definition of lemma is removed

  test = λ _ → unbox _ _ boxed


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)

open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base -- Rel
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Function.Base using (_$_)

open import Cubical.Data.Nat hiding (min)
open import Cubical.Data.Nat.Order
-- open import Cubical.Data.Nat.Properties -- using (+-suc; injSuc; snotz; +-comm; +-assoc; +-zero; inj-m+)

open import MoreNatProperties

module Enumeration
  {ℓ}
  {A   : Type ℓ}
  (f   : A → ℕ)
  (f⁻¹ : ℕ → A)
  (isRetraction : ∀ x → f⁻¹ (f x) ≡ x)
  where

_≤'_ : Rel A A ℓ-zero
a ≤' b = (f a) ≤ (f b)

min' : A → A → A
min' a b = f⁻¹ (min (f a) (f b))

max' : A → A → A
max' a b = f⁻¹ (max (f a) (f b))

max'-sym : ∀ a b → max' a b ≡ max' b a
max'-sym a b with f a ≟ f b | f b ≟ f a
... | lt x | lt y = ⊥-elim {A = λ _ → f⁻¹ (f b) ≡ f⁻¹ (f a)} $  <-asymʷ _ _ x y
... | lt x | eq y = refl
... | lt x | gt y = refl
... | eq x | lt y = refl
... | eq x | eq y = cong f⁻¹ x
... | eq x | gt y = cong f⁻¹ x
... | gt x | lt y = refl
... | gt x | eq y = sym (cong f⁻¹ y)
... | gt x | gt y = ⊥-elim {A = λ _ → f⁻¹ (f a) ≡ f⁻¹ (f b)} $  <-asymʷ _ _ x y

max'-implies-≤'₁ : ∀ a b → a ≤' max' a b
max'-implies-≤'₁ a b with (f a) ≟ (f b)
... | lt (x , p) =  suc x ,  sym (+-suc _ _)  ∙ p ∙ cong f (sym (isRetraction b))
... | eq x = 0 , sym (cong f (isRetraction a) ∙ refl {x = f a})
... | gt x = 0 , sym (cong f (isRetraction a) ∙ refl {x = f a})

max-implies-≤' : ∀ a b → (a ≤' max' a b) × (b ≤' max' a b)
max-implies-≤' a b = max'-implies-≤'₁ a b , transport (λ i → b ≤' max'-sym b a i) (max'-implies-≤'₁ b a)

min'-sym : ∀ a b → min' a b ≡ min' b a
min'-sym a b with f a ≟ f b | f b ≟ f a
... | lt x | lt y = ⊥-elim {A = λ _ → f⁻¹ (f a) ≡ f⁻¹ (f b)} $  <-asymʷ _ _ x y
... | lt x | eq y = sym (cong f⁻¹ y)
... | lt x | gt y = refl
... | eq x | lt y = cong f⁻¹ x
... | eq x | eq y = cong f⁻¹ x
... | eq x | gt y = refl
... | gt x | lt y = refl
... | gt x | eq y = refl
... | gt x | gt y = ⊥-elim {A = λ _ → f⁻¹ (f b) ≡ f⁻¹ (f a)} $  <-asymʷ _ _ x y

min'-implies-≤'₁ : ∀ a b → min' a b ≤' a
min'-implies-≤'₁ a b with (f a) ≟ (f b)
... | lt x = 0 , cong f (isRetraction a) ∙ refl {x = f a}
... | eq x = 0 , cong f (isRetraction a) ∙ refl {x = f a}
... | gt (x , p) = suc x , (λ i → suc (x + cong f (sym (isRetraction b)) (~ i))) ∙ sym (+-suc _ _) ∙ p

min-implies-≤' : ∀ a b → (min' a b ≤' a) × (min' a b ≤' b)
min-implies-≤' a b = min'-implies-≤'₁ a b , transport (λ i → min'-sym b a i ≤' b) (min'-implies-≤'₁ b a)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module InterpretationEqualityExceptAtVariableName where

open import OscarPrelude
open import VariableName
open import FunctionName
open import PredicateName
open import Elements
open import Interpretation

record _≞_/_ (𝓘 : Interpretation) (I : Interpretation) (𝑥 : VariableName) : Set
 where
  field
    μEquality : {𝑥′ : VariableName} → 𝑥′ ≢ 𝑥 → μ⟦ 𝓘 ⟧ 𝑥 ≡ μ⟦ I ⟧ 𝑥′
    𝑓Equality : (𝑓 : FunctionName) (μs : Elements) → 𝑓⟦ 𝓘 ⟧ 𝑓 μs ≡ 𝑓⟦ I ⟧ 𝑓 μs
    𝑃Equality : (𝑃 : PredicateName) → (μs : Elements) → 𝑃⟦ 𝓘 ⟧ 𝑃 μs ≡ 𝑃⟦ I ⟧ 𝑃 μs


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.InftyMagma where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.FunExtEquiv

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

private
  variable
    ℓ ℓ' ℓ'' : Level

-- ∞-Magmas with SNS

∞-magma-structure : Type ℓ → Type ℓ
∞-magma-structure X = X → X → X

∞-Magma : Type (ℓ-suc ℓ)
∞-Magma {ℓ} = TypeWithStr ℓ ∞-magma-structure

∞-magma-iso : StrIso ∞-magma-structure ℓ
∞-magma-iso (X , _·_) (Y , _∗_) f =
  (x x' : X) → equivFun f (x · x') ≡ equivFun f x ∗ equivFun f x'

∞-magma-is-SNS : SNS {ℓ} ∞-magma-structure ∞-magma-iso
∞-magma-is-SNS f = SNS-≡→SNS-PathP ∞-magma-iso (λ _ _ → funExt₂Equiv) f

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module 060-commutative-group where

-- We need groups.

open import 050-group

record CommutativeGroup
  {M : Set}
  (_==_ : M -> M -> Set)
  (_*_ : M -> M -> M)
  (id : M)
  (invert : M -> M)
  : Set1 where

  field
    group : Group _==_ _*_ id invert
    comm : ∀ {r s} -> (r * s) == (s * r)

  open Group group public

  -- Nothing proven here yet.

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


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

open import Level.NP
open import Type hiding (★)
open import Data.Tree.Binary
open import Data.Zero
open import Data.One
open import Data.Sum
open import Data.Product

open import Relation.Binary.PropositionalEquality.NP
open import HoTT
open Equivalences
open import Type.Identities
open import Function
open import Function.Extensionality

open import Explore.Core
open import Explore.Properties
open import Explore.Zero
open import Explore.Sum
open import Explore.Isomorphism

fromBinTree : ∀ {m} {a} {A : ★ a} → BinTree A → Explore m A
fromBinTree empty      = empty-explore
fromBinTree (leaf x)   = point-explore x
fromBinTree (fork ℓ r) = merge-explore (fromBinTree ℓ) (fromBinTree r)

fromBinTree-ind : ∀ {m p a} {A : ★ a} (t : BinTree A) → ExploreInd p (fromBinTree {m} t)
fromBinTree-ind empty      = empty-explore-ind
fromBinTree-ind (leaf x)   = point-explore-ind x
fromBinTree-ind (fork ℓ r) = merge-explore-ind (fromBinTree-ind ℓ)
                                               (fromBinTree-ind r)

AnyP≡ΣfromBinTree : ∀ {a p}{A : ★ a}{P : A → ★ p}(xs : BinTree A) → Any P xs ≡ Σᵉ (fromBinTree xs) P
AnyP≡ΣfromBinTree empty    = idp
AnyP≡ΣfromBinTree (leaf x) = idp
AnyP≡ΣfromBinTree (fork xs xs₁) = ⊎= (AnyP≡ΣfromBinTree xs) (AnyP≡ΣfromBinTree xs₁)

module _ {{_ : UA}}{{_ : FunExt}}{A : ★ ₀} where

  exploreΣ∈ : ∀ {m} xs → Explore m (Σ A λ x → Any (_≡_ x) xs)
  exploreΣ∈ empty = explore-iso (coe-equiv (Lift≡id ∙ ! ×𝟘-snd  ∙ ×= idp (! Lift≡id))) Lift𝟘ᵉ
  exploreΣ∈ (leaf x) = point-explore (x , idp)
  exploreΣ∈ (fork xs xs₁) = explore-iso (coe-equiv (! Σ⊎-split)) (exploreΣ∈ xs ⊎ᵉ exploreΣ∈ xs₁)

  Σᵉ-adq-exploreΣ∈ : ∀ {m} xs → Adequate-Σ {m} (Σᵉ (exploreΣ∈ xs))
  Σᵉ-adq-exploreΣ∈ empty = Σ-iso-ok (coe-equiv (Lift≡id ∙ ! ×𝟘-snd ∙ ×= idp (! Lift≡id)))
    {Aᵉ = Lift𝟘ᵉ} ΣᵉLift𝟘-ok
  Σᵉ-adq-exploreΣ∈ (leaf x₁) F = ! Σ𝟙-snd ∙ Σ-fst≃ (≃-sym (Σx≡≃𝟙 x₁)) F
  Σᵉ-adq-exploreΣ∈ (fork xs xs₁) = Σ-iso-ok (coe-equiv (! Σ⊎-split)) {Aᵉ = exploreΣ∈ xs ⊎ᵉ exploreΣ∈ xs₁}
               (Σᵉ⊎-ok {eᴬ = exploreΣ∈ xs}{eᴮ = exploreΣ∈ xs₁} (Σᵉ-adq-exploreΣ∈ xs) (Σᵉ-adq-exploreΣ∈ xs₁))

module _ {{_ : UA}}{{_ : FunExt}}{A : ★ ₀}{P : A → ★ _}(explore-P : ∀ {m} x → Explore m (P x)) where
  open import Explore.Zero
  open import Explore.Sum
  open import Explore.Isomorphism

  exploreAny : ∀ {m} xs → Explore m (Any P xs)
  exploreAny empty         = Lift𝟘ᵉ
  exploreAny (leaf x)      = explore-P x
  exploreAny (fork xs xs₁) = exploreAny xs ⊎ᵉ exploreAny xs₁

  module _ (Σᵉ-adq-explore-P : ∀ {m} x → Adequate-Σ {m} (Σᵉ (explore-P x))) where
    Σᵉ-adq-exploreAny : ∀ {m} xs → Adequate-Σ {m} (Σᵉ (exploreAny xs))
    Σᵉ-adq-exploreAny empty F         = ! Σ𝟘-lift∘fst ∙ Σ-fst= (! Lift≡id) _
    Σᵉ-adq-exploreAny (leaf x₁) F     = Σᵉ-adq-explore-P x₁ F
    Σᵉ-adq-exploreAny (fork xs xs₁) F = ⊎= (Σᵉ-adq-exploreAny xs _) (Σᵉ-adq-exploreAny xs₁ _) ∙ ! dist-⊎-Σ

  exploreΣᵉ : ∀ {m} xs → Explore m (Σᵉ (fromBinTree xs) P)
  exploreΣᵉ {m} xs = fromBinTree-ind xs (λ e → Explore m (Σᵉ e P)) Lift𝟘ᵉ _⊎ᵉ_ explore-P

  module _ (Σᵉ-adq-explore-P : ∀ {m} x → Adequate-Σ {m} (Σᵉ (explore-P x))) where
    Σᵉ-adq-exploreΣᵉ : ∀ {m} xs → Adequate-Σ {m} (Σᵉ (exploreΣᵉ xs))
    Σᵉ-adq-exploreΣᵉ empty F         = ! Σ𝟘-lift∘fst ∙ Σ-fst= (! Lift≡id) _
    Σᵉ-adq-exploreΣᵉ (leaf x₁) F     = Σᵉ-adq-explore-P x₁ F
    Σᵉ-adq-exploreΣᵉ (fork xs xs₁) F = ⊎= (Σᵉ-adq-exploreΣᵉ xs _) (Σᵉ-adq-exploreΣᵉ xs₁ _) ∙ ! dist-⊎-Σ

data Path {a}{A : ★_ a} : BinTree A → ★_ a where
  leaf  : (x : A) → Path (leaf x)
  left  : {t u : BinTree A} (p : Path t) → Path (fork t u)
  right : {t u : BinTree A} (p : Path u) → Path (fork t u)

path : ∀ {a}{A : ★ a} → BinTree A → ★₀
path empty      = 𝟘
path (leaf x)   = 𝟙
path (fork t u) = path t ⊎ path u

path' : ∀{a}{A : ★ a} → BinTree A → ★₀
path' t = fromBinTree t 𝟘 _⊎_ (const 𝟙)

-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


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

open import Groups.Definition
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Rings.Definition

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

module Modules.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+R_ _*_) {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} (G : AbelianGroup G') (_·_ : A → M → M) where

record Module : Set (a ⊔ b ⊔ m ⊔ n) where
  field
    dotWellDefined : {r s : A} {t u : M} → Setoid._∼_ S r s → Setoid._∼_ T t u → Setoid._∼_ T (r · t) (s · u)
    dotDistributesLeft : {r : A} {x y : M} → Setoid._∼_ T (r · (x + y)) ((r · x) + (r · y))
    dotDistributesRight : {r s : A} {x : M} → Setoid._∼_ T ((r +R s) · x) ((r · x) + (s · x))
    dotAssociative : {r s : A} {x : M} → Setoid._∼_ T ((r * s) · x) (r · (s · x))
    dotIdentity : {x : M} → Setoid._∼_ T ((Ring.1R R) · x) x


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

open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans; subst₂)
open import Function using (_∘_)
open import Relation.Nullary.Negation using (contradiction)

module PiCalculus.Utils where

module ListInv {a} {A : Set a} where
  open import Data.List as List using (List; []; _∷_; [_]; _++_)
  import Data.List.Properties as Listₚ
  import Data.List.Membership.Propositional.Properties as ∈ₚ
  import Data.List.Relation.Unary.Any.Properties as Anyₚ
  open import Data.List.Relation.Unary.Any using (Any; here; there)
  open import Data.List.Membership.Propositional using (_∈_; _∉_)
  open import Data.List.Relation.Binary.Equality.Propositional {A = A} using (_≋_; []; _∷_; ≋⇒≡; ≡⇒≋; ≋-refl)

  inv-++ˡ' : ∀ lx ly {rx ry} s → s ∉ lx → s ∉ ly → lx ++ [ s ] ++ rx ≋ ly ++ [ s ] ++ ry → lx ≋ ly
  inv-++ˡ' [] [] s ∉lx ∉ly eq = []
  inv-++ˡ' [] (x ∷ ly) .x ∉lx ∉ly (refl ∷ eq) = contradiction (here refl) ∉ly
  inv-++ˡ' (x ∷ lx) [] .x ∉lx ∉ly (refl ∷ eq) = contradiction (here refl) ∉lx
  inv-++ˡ' (x ∷ lx) (.x ∷ ly) s ∉lx ∉ly (refl ∷ eq)
    rewrite ≋⇒≡ (inv-++ˡ' lx ly s (∉lx ∘ there) (∉ly ∘ there) eq) = ≋-refl

  inv-++ˡ : ∀ lx ly {rx ry} s → s ∉ lx → s ∉ ly → lx ++ [ s ] ++ rx ≡ ly ++ [ s ] ++ ry → lx ≡ ly
  inv-++ˡ lx ly s ∉lx ∉ly = ≋⇒≡ ∘ inv-++ˡ' lx ly s ∉lx ∉ly ∘ ≡⇒≋

  inv-++ʳ : ∀ lx ly {rx ry} s → s ∉ rx → s ∉ ry → lx ++ [ s ] ++ rx ≡ ly ++ [ s ] ++ ry → rx ≡ ry
  inv-++ʳ lx ly {rx} {ry} s ∉rx ∉ry
    = Listₚ.reverse-injective
    ∘ inv-++ˡ (List.reverse rx) (List.reverse ry) s (∉rx ∘ Anyₚ.reverse⁻) (∉ry ∘ Anyₚ.reverse⁻)
    ∘ subst₂ _≡_ (do-reverse lx _) (do-reverse ly _)
    ∘ cong List.reverse

    where do-reverse : ∀ (lx rx : List A) {s}
                     → List.reverse (lx ++ [ s ] ++ rx) ≡ List.reverse rx ++ [ s ] ++ List.reverse lx
          do-reverse lx rx {s} = trans (Listₚ.reverse-++-commute lx _)
                                       (trans (cong (_++ List.reverse lx) (Listₚ.unfold-reverse s rx))
                                              (Listₚ.++-assoc (List.reverse rx) _ _))

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

data ⊤ : Set where tt : ⊤

id : ⊤ → ⊤
id tt = tt

data Foo : ⊤ → Set where
  foo : {x : ⊤} → Foo (id x)

test : {x : Σ ⊤ Foo} → Set
test {x₁ , x₂} = {!x₂!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue639 where

postulate A : Set


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

data _≡P_ {A : Set} (x : A) : A → Prop where
  refl : x ≡P x

J-P : {A : Set} (x : A) (P : (y : A) → x ≡P y → Set)
    → P x refl → (y : A) (e : x ≡P y) → P y e
J-P x P p .x refl = p

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
module DuplicateConstructors where

data D : Set where
  c : D
  c : D

f : D -> D
f c = c


text:
-- Home to all functions creating, modifying or removing ScopeEnv or ScopeState
module ScopeState where
open import Data.List using (List) renaming ([] to emptyList ; map to listMap ; _∷_ to _cons_)
open import Data.String renaming (_++_ to _then_)
open import Data.Bool
open import Data.Nat
open import Data.Fin renaming (zero to fzero ; suc to fsuc) hiding (_+_)
open import Relation.Binary.PropositionalEquality
open import Data.Maybe renaming (map to maybemap) hiding (monad)
open import ParseTree
open import Data.List.Properties
open import Data.Vec hiding (_>>=_) renaming (lookup to veclookup)
open import Category.Monad.State
open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Data.Empty
open import Relation.Nullary
open import Category.Monad
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.TrustMe
open import Data.Unit
open import AgdaHelperFunctions
open import Data.Nat.Show
import IO.Primitive as Prim
open import ParseTreeOperations

data ScopeType : Set where
  funcDef : ScopeType
  moduleDef : (name : Identifier) -> ScopeType
  addFuncToModule : ScopeType
  addVariableToType : ScopeType
  topLevel : ScopeType

data Scope (maxVars : ℕ) (maxScopes : ℕ): Set where
 mkScope : (scopeType : ScopeType) ->
           (enclosing : Maybe (Fin maxScopes)) -> -- Nothing if this is the top scope
           (declaredVars : List (Fin maxVars)) -> -- the list of variables declared in this scope
           Scope maxVars maxScopes

getType : {m n : ℕ} -> Scope m n -> ScopeType
getType (mkScope scopeType enclosing declaredVars) = scopeType

--appendToDeclared : {m n : ℕ} -> Fin m -> Scope m n -> Scope m n
--appendToDeclared what (mkScope scopeType enclosing declaredVars) =
--  mkScope scopeType enclosing (what cons declaredVars)

getDeclared : {m n : ℕ} -> Scope m n -> List (Fin m)
getDeclared (mkScope scopeType enclosing declaredVars) = declaredVars

data ScopeEnv : Set where
  env : {numVars : ℕ} ->
        (vars : Vec String numVars) ->
        (maxScopes : ℕ) ->
        (scopes : Vec (Scope numVars maxScopes) maxScopes ) ->
        (current : Fin maxScopes) ->
        ScopeEnv

ScopeState : Set -> Set
ScopeState = StateT  (ScopeEnv) (λ x -> Prim.IO (String ⊎ x))

--open RawMonadState (StateTMonadState ScopeEnv {M = IOStringError} EitherOverIO) public

liftIO : {a : Set} -> Prim.IO a -> ScopeState a
liftIO action e = do
  a <- action
  return (inj₂ (a , e))
  where open RawMonad IOMonad

runScopeState : {a : Set} -> ScopeState a -> ScopeEnv -> Prim.IO (String ⊎ a)
runScopeState s e = do
  inj₂ ( result , e) <- s e
    where inj₁ e -> return $ inj₁ e
  return $ inj₂ result
  where open RawMonad IOMonad -- brings return and bind for the Prim.IO monad into scope
fail : {a : Set} -> String -> ScopeState a
fail message = λ x -> Prim.return $ inj₁ message

-- Try an action and return an error message on failure rather than
-- propagating the failure. All state changes are rolled back.
try : {a : Set} -> ScopeState a -> ScopeState (String ⊎ a)
try st environment = do
  inj₂ (x , newEnv) <- st environment
    where inj₁ error -> return $ inj₂ $ inj₁ error , environment
  return $ inj₂ $ inj₂ x , newEnv
  where open RawMonad IOMonad

open RawMonadState (StateTMonadState ScopeEnv (SumMonadT IOMonad String)) public

newEnv : ScopeEnv
newEnv = env [] 1 ((mkScope topLevel nothing emptyList) ∷ [])   fzero

-- Variable adding

newRaise : {n : ℕ} -> Fin n -> Fin (1 + n)
newRaise fzero = fzero
newRaise (fsuc f) = fsuc (newRaise f)

raiseScopeType : {n m : ℕ} -> Scope n m -> Scope (1 + n) m
raiseScopeType (mkScope t s declared) = mkScope t s (listMap newRaise declared)

raiseType : {n m : ℕ} -> (x : Scope n m) -> getType x ≡ getType (raiseScopeType x)
raiseType (mkScope scopeType enclosing declaredVars) = refl

mapRaiseType : {n m o : ℕ} -> (x : Vec (Scope n m) o) -> (curr : Fin o)
  -> getType (veclookup curr x) ≡ getType (veclookup curr (map raiseScopeType x))
mapRaiseType (x ∷ xs) fzero with veclookup fzero (x ∷ xs)
... | c = raiseType c
mapRaiseType (x ∷ xs) (fsuc curr) = mapRaiseType xs curr

addVarToScope : {n m : ℕ} -> (Scope n m) -> (what : Fin (1 + n))
          -> (Scope (1 + n) m)
addVarToScope (mkScope scopeType enclosing declaredVars) what =
    mkScope scopeType enclosing (what cons (listMap newRaise declaredVars))

addVar : {n m numScopes : ℕ}(xs : Vec (Scope n m) numScopes) ->
  (atPos : Fin numScopes) -> (what : Fin (1 + n)) ->
    Vec (Scope (1 + n) m) numScopes
addVar (x ∷ xs) fzero what = addVarToScope x what ∷ map raiseScopeType xs
addVar (x ∷ xs) (fsuc atPos) what = raiseScopeType x ∷ addVar xs atPos what

addExistingVarToScope : {n m : ℕ} -> (Scope n m) -> (what : Fin n)
          -> (Scope n m)
addExistingVarToScope (mkScope scopeType enclosing declaredVars) what =
    mkScope scopeType enclosing (what cons declaredVars)

addExistingVar : {n m numScopes : ℕ}(xs : Vec (Scope n m) numScopes) ->
  (atPos : Fin numScopes) -> (what : Fin n) ->
    Vec (Scope n m) numScopes
addExistingVar [] () what
addExistingVar (x ∷ xs) fzero what = (addExistingVarToScope x what) ∷ xs
addExistingVar (x ∷ xs) (fsuc atPos) what = x ∷ addExistingVar xs atPos what

-- returns input identifier with id and scope id filled in
addIdentifier :  Identifier -> ScopeState Identifier
addIdentifier (identifier name isInRange scope declaration {b}{c} {c2}) = do
  env {numVars} vars maxScopes scopes current <- get
  let newScopes = (addVar scopes current (fromℕ numVars))
  put (env (vars ∷ʳ name) maxScopes
     newScopes
       current)
  return (identifier name isInRange (toℕ current) numVars {b}{c} {c2})

raiseEnclosingScope : {maxVars maxScopes : ℕ} -> Scope maxVars maxScopes
    -> Scope maxVars (1 + maxScopes)
raiseEnclosingScope (mkScope scopeType enclosing declaredVars) =
    mkScope scopeType (maybemap newRaise enclosing) declaredVars

addScope : (b : ScopeType) ->  ScopeState ℕ
addScope scopeType = do
  env vars maxScopes scopes current <- get
  let newScopes = map raiseEnclosingScope scopes ∷ʳ
                   mkScope scopeType
                    (just (newRaise current)) emptyList
  put (env vars (1 + maxScopes)
                      newScopes
                      (fromℕ maxScopes)
                       )
  return maxScopes

castCurrent : {n m : ℕ} -> {A : Set} -> Vec A n -> Fin m -> ScopeState (Fin n)
castCurrent [] x = fail "Something went wrong with scope saving"
castCurrent (x ∷ vec) fzero = return fzero
castCurrent (x ∷ vec) (fsuc f) = do
  r <- castCurrent vec f
  return (fsuc r)

saveAndReturnToScope : {A : Set} -> ScopeState A -> ScopeState A
saveAndReturnToScope ss = do
  env vars maxScopes scopes current <- get
  c <- ss
  env vars₁ maxScopes₁ scopes₁ current₁ <- get
  newCurr <- castCurrent scopes₁ current
  let newEnv = env vars₁ maxScopes₁ scopes₁ newCurr
  put newEnv
  return c

setScope : (n : ℕ) -> ScopeState ℕ
setScope n (env vars maxScopes scopes current) with suc n Data.Nat.≤? maxScopes
setScope n (env vars maxScopes scopes current) | yes p = return n (env vars maxScopes scopes (fromℕ≤ p)) --inj₂ (n , (env vars maxScopes scopes (fromℕ≤ p)))
setScope n e | no ¬p = Prim.return $ inj₁ "Tried to set scope to invalid value" --inj₁ "Tried to set scope to invalid value"

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter f emptyList = emptyList
filter f (x cons l) = if (f x) then (x cons (filter f l)) else filter f l

-- this is the lookup function from Schäfer's algorithm
-- TODO: Simple dummy function, does not sufficiently reflect real
-- scoping rules
-- TODO: Agda does not understand that this terminates because
-- the fact that the enclosing scope must be farther to the front of
-- the scopes list is not encoded in the type yet
-- returns the declaration id the input string
{-# TERMINATING #-}
lookup : String -> ScopeState ℕ
lookup s = saveAndReturnToScope (do
  env vars maxScopes scopes current <- get
  mkScope scopeType enclosing decl <- return (veclookup current scopes)
  emptyList <- return ( filter (λ x -> veclookup x vars == s) decl)
    where x cons xs -> return (toℕ x)
  just n <- return enclosing
    where _ -> fail $ "There is no enclosing scope while looking up: " then s
  setScope (toℕ n)
  lookup s)

-- fill in the declaration and scope information in an identifier
-- given that the name has already been declared

fillInIdentifier : Identifier -> ScopeState Identifier
fillInIdentifier (identifier name isInRange scope declaration {b}{c} {c2}) = do
  x <- saveAndReturnToScope (lookup name)
  suc n <- return x
    where zero -> fail ("Identifier not found in file: " then name)
  env vars maxScopes scopes current <- get
  return (identifier name isInRange (toℕ current) (suc n) {b}{c} {c2})

-- at the place where something is declared, you can only use simple names.
-- TODO: Actually, this should be adequately bounded by the current scope. But how to implement?

access : Identifier -> ScopeState Identifier
access (identifier name isInRange scope declaration {b}{c} {c2}) = do
  env {numVars} vars maxScopes scopes current <- get
  yes p <- return (suc declaration Data.Nat.≤? numVars)
    where _ -> fail "Parse tree scoping has produced a nonsense declaration"
  let newName = veclookup (fromℕ≤ p) vars
  anything <- setScope scope
  identifier n r s d <- fillInIdentifier (identifier newName isInRange scope declaration {b}{c} {c2})
  yes x <- return (d Data.Nat.≟ declaration)
    where no y -> fail "Could not perform name change because this would change the meaning of the code"
  return (identifier n r s d {b}{c} {c2})

mapState : {A B : Set} -> (A -> ScopeState B) -> List A -> ScopeState (List B)
mapState f emptyList = return emptyList
mapState f (x cons list) = do
  x1 <- f x
  xs <- mapState f list
  return (x1 cons xs)

addContentReferenceToModuleTop : TypeSignature -> ScopeState ℕ
addContentReferenceToModuleTop (typeSignature (identifier name isInRange scope 0) funcType) = fail "Trying to add signature which has not been scoped"
addContentReferenceToModuleTop (typeSignature (identifier name isInRange scope declaration) funcType) = do
  env {numVars } vars maxScopes scopes current <- get
  yes p <- return (suc declaration Data.Nat.≤? numVars)
    where _ -> fail "Found messed-up scoping"
  let newScopes = addExistingVar scopes current (fromℕ≤ p)
  return declaration

_after_ : {A B C : Set} -> (B -> ScopeState C) -> (A -> ScopeState B) -> A -> ScopeState C
_after_ f g x = do
  prelim <- g x
  f prelim

getNameForId : ℕ -> ScopeState String
getNameForId n = do
  env {numVars } vars maxScopes scopes current <- get
  yes p <- return (suc n Data.Nat.≤? numVars)
    where _ -> fail "Can't get name for this invalid identifier"
  let r = veclookup (fromℕ≤ p) vars
  return r

replaceName : {A : Set} -> {n : ℕ} -> Fin n -> A -> Vec A n -> Vec A n
replaceName fzero a (x ∷ list) = a ∷ list
replaceName (fsuc n) a (x ∷ list) = x ∷ replaceName n a list

replaceID : ℕ -> String -> ScopeState String
replaceID which newName = do
  env {numVars} vars maxScopes scopes current <- get
  yes p <- return (suc which Data.Nat.≤? numVars)
    where _ -> fail "Can't rename this invalid identifier"
  let newList = replaceName (fromℕ≤ p) newName vars
  put (env {numVars } newList maxScopes scopes current)
  return newName

currentScopeTypeIsFuncDef : ScopeState Bool
currentScopeTypeIsFuncDef = do
  env {numVars } vars maxScopes scopes current <- get
  mkScope funcDef enclosing declaredVars <- return (veclookup current scopes)
    where _ -> fail "This is not the scope type you expected"
  return true

isNameInUse : String -> ScopeState Bool
isNameInUse s = do
  env vars maxScopes scopes current <- get
  return $ Data.List.any (λ x -> x == s) (Data.Vec.toList vars)

-- terminates because vars is not infinite.
{-# TERMINATING #-}
makeUniqueName : ℕ -> ScopeState String
makeUniqueName n = do
    let proposedName = Data.String.concat $ "renameMe" Data.List.∷ (Data.Nat.Show.show n) Data.List.∷ emptyList
    b <- isNameInUse proposedName
    if b
      then makeUniqueName $ suc n
      else return proposedName

getUniqueIdentifierWithInScope : Bool -> ScopeState Identifier
getUniqueIdentifierWithInScope b = do
  name <- makeUniqueName 0
  id <- addIdentifier $ identifier name (λ _ -> before) 0 0 {b}{emptyList} {emptyList}
  return id

getUniqueIdentifier : ScopeState Identifier
getUniqueIdentifier = getUniqueIdentifierWithInScope true


text:
{-
  Copyright 2019 Lisandra Silva

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

open import Prelude
open import Relation.Binary.HeterogeneousEquality
            using (_≅_)
            renaming (cong to ≅-cong; refl to ≅-refl)

open import StateMachineModel

module Examples.SMCounter where

  data MyEvent : Set where
    inc  : MyEvent
    inc2 : MyEvent

  data MyEnabled : MyEvent → ℕ → Set where
    tt : ∀ {e} {n} → MyEnabled e n

  MyEventSet : EventSet {Event = MyEvent}
  MyEventSet inc  = ⊤
  MyEventSet inc2 = ⊤

  MyAction : {preSt : ℕ} {ev : MyEvent} → MyEnabled ev preSt → ℕ
  MyAction {preSt} {inc} enEv = suc preSt
  MyAction {preSt} {inc2} enEv = suc (suc preSt)

  data MyWeakFairness : EventSet → Set where
    w0 : MyWeakFairness MyEventSet

  -- Another way of modelling the WeakFairness
  MyWeakFairness2 : EventSet {Event = MyEvent} → Set
  MyWeakFairness2 MyEventSet = ⊤

  MyStateMachine : StateMachine ℕ MyEvent
  MyStateMachine = record { initial = 2 ≡_
                          ; enabled = MyEnabled
                          ; action  = MyAction }

  mySystem : System ℕ MyEvent
  mySystem = record { stateMachine = MyStateMachine
                    ; weakFairness = MyWeakFairness }

  myInvariant : Invariant MyStateMachine (2 ≤_)
  myInvariant (init x) = ≤-reflexive x
  myInvariant (step {ps} {inc} rs enEv) = ≤-stepsˡ 1 (myInvariant rs)
  myInvariant (step {ps} {inc2} rs enEv) = ≤-stepsˡ 2 (myInvariant rs)

  open LeadsTo ℕ MyEvent mySystem

  -- A state equals to n leads to a state equals to (1 + n) or equals to (2 + n)
  progressDumb : ∀ {n : ℕ} → (n ≡_) l-t ((1 + n ≡_) ∪ (2 + n ≡_))
  progressDumb = viaEvSet MyEventSet w0
                           ( λ { inc  ⊤ → hoare λ { refl enEv → inj₁ refl}
                               ; inc2 ⊤ → hoare λ { refl enEv → inj₂ refl} })
                           ( λ { inc  ⊥ → ⊥-elim (⊥ tt)
                               ; inc2 ⊥ → ⊥-elim (⊥ tt)} )
                           λ rs n≡s → inc , tt , tt

  n<m+n : ∀ {n m} → 0 < m → n < m + n
  n<m+n {zero}  {suc m} x = s≤s z≤n
  n<m+n {suc n} {suc m} x = s≤s (m≤n+m (suc n) m)

  progress-< : ∀ n → (n ≡_) l-t (n <_)
  progress-< n = viaTrans
                   progressDumb
                   (viaInv (λ { rs (inj₁ refl) → s≤s ≤-refl
                              ; rs (inj₂ refl) → s≤s (m≤n+m n 1)}))

  {- A predicate on states, parameterized by m (target). The d parameter is the
     "distance" from the target m from state s.

     QUESTION : We are generalizing Z to be of a given type, however in myWFR
     we are using it knowing that is ℕ because we apply _≡_ and _+_
  -}
  F : ∀ {m} → ℕ → Z → Set
  F {m} d s = m ≡ d + s

  wfr-1 : ∀ {m} → (s : Z) → (m ≤ s) ⊎ ∃[ x ] F {m} x s
  wfr-1 {m} s with m ≤? s
  ... | yes yy  = inj₁ yy
  ... | no  s<m = inj₂ (m ∸ s , sym (m∸n+n≡m (≰⇒≥ s<m)) )

  progress-1st : ∀ {n m} → (n ≡_) l-t ( (m ≤_) ∪ [∃ x ∶ F {m} x ] )
  progress-1st {n} {m} = viaInv (λ {s} rs n≡s → wfr-1 s)

  -- A state which distance to m is 0 (if we are in the state m)
  -- leads to a state greater than m
  progress-d0 : ∀ {m} → F {m} 0 l-t ( (m ≤_) ∪ [∃ x ⇒ _< 0 ∶ F {m} x ] )
  progress-d0 {m} = viaInv (λ { {s} rs refl → inj₁ ≤-refl })

  progress-d1 : ∀ {m} → F {m} 1 l-t ((m ≤_) ∪ [∃ x ⇒ _< 1 ∶ F {m} x ] )
  progress-d1 {m} =
    viaEvSet
      MyEventSet
      w0
      (λ { inc  ⊤ → hoare (λ { refl _ → inj₁ ≤-refl })
         ; inc2 ⊤ → hoare (λ { refl _ → inj₁ (≤-step ≤-refl) })
         })
      (λ { inc  ⊥ → ⊥-elim (⊥ tt)
         ; inc2 ⊥ → ⊥-elim (⊥ tt)
         })
      λ _ _ → inc , tt , tt

  progress-d2 : ∀ {m w} → F {m} (2 + w) l-t ( (m ≤_) ∪ [∃ x ⇒ _< (2 + w) ∶ F {m} x ] )
  progress-d2 {m} {w} =
    viaEvSet
      MyEventSet
      w0
      (λ { inc ⊤ → hoare λ { {ps} refl _
                     → inj₂ (suc w , ≤-refl , cong suc (sym (+-suc w ps)) )}
         ; inc2 ⊤ → hoare λ { {ps} refl _
                     → inj₂ (w , ≤-step ≤-refl , sym (trans (+-suc w (suc ps))
                                                     (cong suc (+-suc w ps)))) }
         })
      (λ { inc  ⊥ → ⊥-elim (⊥ tt)
         ; inc2 ⊥ → ⊥-elim (⊥ tt) })
      λ _ _ → inc , tt , tt

  progress-2nd : ∀ {m w}
              → F {m} w
                l-t
                ((m ≤_) ∪ [∃ x ⇒ _< w ∶ F {m} x ] )
  progress-2nd {m} {zero}        = progress-d0
  progress-2nd {m} {suc zero}    = progress-d1
  progress-2nd {m} {suc (suc w)} = progress-d2

  -- A state equals to n leads to a state greater or equal to m, ∀ m.
  -- In other words, from n we can go to every possible state m steps
  -- away from n
  progress : ∀ {n m : ℕ} → (n ≡_) l-t (m ≤_)
  progress {n} {m} = viaWFR (F {m})
                             progress-1st
                             λ w → progress-2nd

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


text:
module Prelude.Strict where

open import Prelude.Equality
open import Agda.Builtin.Strict

force : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
force x f = primForce x f

force′ : ∀ {a b} {A : Set a} {B : A → Set b} → (x : A) → (∀ y → x ≡ y → B y) → B x
force′ x k = (force x λ y → k y) refl

forceLemma = primForceLemma

{-# INLINE force #-}

{-# DISPLAY primForce      = force #-}
{-# DISPLAY primForceLemma = forceLemma #-}

seq : ∀ {a b} {A : Set a} {B : Set b} → A → B → B
seq x y = force x (λ _ → y)

{-# INLINE seq #-}

infixr 0 _$!_
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $! x = force x f

{-# INLINE _$!_ #-}

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 --cubical --no-import-sorts --safe #-}
module Cubical.Data.Graph where

open import Cubical.Data.Graph.Base public
open import Cubical.Data.Graph.Examples public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The partiality monad's monad instance
------------------------------------------------------------------------

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

module Partiality-monad.Inductive.Monad where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
import Monad
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc hiding (_>>=′_)
open import Nat equality-with-J as Nat
open import Univalence-axiom equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Alternative-order
open import Partiality-monad.Inductive.Eliminators
open import Partiality-monad.Inductive.Monotone
open import Partiality-monad.Inductive.Omega-continuous

open [_⊥→_⊥]

------------------------------------------------------------------------
-- The monad instance

-- Functions of type A → B ⊥ can be lifted to /ω-continuous/ functions
-- from A ⊥ to B ⊥.

private

  =<<-args : ∀ {a b} {A : Type a} {B : Type b}
             (f : A → B ⊥) → Arguments-nd b b A
  =<<-args {B = B} f = record
    { P  = B ⊥
    ; Q  = _⊑_
    ; pe = never
    ; po = f
    ; pl = λ _ → ⨆
    ; pa = λ _ _ → antisymmetry
    ; ps = ⊥-is-set
    ; qr = λ _ → ⊑-refl
    ; qt = λ _ _ _ _ _ → ⊑-trans
    ; qe = λ _ → never⊑
    ; qu = λ _ → upper-bound
    ; ql = λ _ _ _ → least-upper-bound
    ; qp = λ _ _ → ⊑-propositional
    }

infix 50 _∗ _∗-inc_

_∗ : ∀ {a b} {A : Type a} {B : Type b} →
     (A → B ⊥) → [ A ⊥→ B ⊥]
f ∗ = record
  { monotone-function = record
    { function = ⊥-rec-nd (=<<-args f)
    ; monotone = ⊑-rec-nd (=<<-args f)
    }
  ; ω-continuous = λ s →
      ⊥-rec-nd (=<<-args f) (⨆ s)    ≡⟨ ⊥-rec-nd-⨆ (=<<-args f) s ⟩∎
      ⨆ (inc-rec-nd (=<<-args f) s)  ∎
  }

_∗-inc_ : ∀ {a b} {A : Type a} {B : Type b} →
          (A → B ⊥) → Increasing-sequence A → Increasing-sequence B
_∗-inc_ f = inc-rec-nd (=<<-args f)

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∀ {a b} {A : Type a} {B : Type b} →
         A ⊥ → (A → B ⊥) → B ⊥
x >>=′ f = function (f ∗) x

-- Join.

join : ∀ {a} {A : Type a} → A ⊥ ⊥ → A ⊥
join x = x >>=′ id

-- "Computation" rules for bind.

never->>= : ∀ {a b} {A : Type a} {B : Type b} {f : A → B ⊥} →
            never >>=′ f ≡ never
never->>= = ⊥-rec-nd-never (=<<-args _)

now->>= : ∀ {a b} {A : Type a} {B : Type b} {f : A → B ⊥} {x} →
          now x >>=′ f ≡ f x
now->>= = ⊥-rec-nd-now (=<<-args _) _

⨆->>= : ∀ {a b} {A : Type a} {B : Type b} {f : A → B ⊥} {s} →
        ⨆ s >>=′ f ≡ ⨆ (f ∗-inc s)
⨆->>= = ⊥-rec-nd-⨆ (=<<-args _) _

-- Bind is monotone.

infixl 5 _>>=-mono_

_>>=-mono_ :
  ∀ {a b} {A : Type a} {B : Type b} {x y : A ⊥} {f g : A → B ⊥} →
  x ⊑ y → (∀ z → f z ⊑ g z) → x >>=′ f ⊑ y >>=′ g
_>>=-mono_ {x = x} {y} {f} {g} x⊑y f⊑g =
  x >>=′ f ⊑⟨ monotone (f ∗) x⊑y ⟩
  y >>=′ f ⊑⟨ ⊥-rec-⊥ (record
                { P  = λ y → y >>=′ f ⊑ y >>=′ g
                ; pe = never >>=′ f  ≡⟨ never->>= ⟩⊑
                       never         ⊑⟨ never⊑ _ ⟩■
                       never >>=′ g  ■
                ; po = λ x →
                         now x >>=′ f  ≡⟨ now->>= ⟩⊑
                         f x           ⊑⟨ f⊑g x ⟩
                         g x           ≡⟨ sym now->>= ⟩⊑
                         now x >>=′ g  ■
                ; pl = λ s ih →
                         ⨆ s >>=′ f     ≡⟨ ⨆->>= ⟩⊑
                         ⨆ (f ∗-inc s)  ⊑⟨ ⨆-mono ih ⟩
                         ⨆ (g ∗-inc s)  ≡⟨ sym ⨆->>= ⟩⊑
                         ⨆ s >>=′ g     ■
                ; pp = λ _ → ⊑-propositional
                })
                y ⟩
  y >>=′ g ■

-- Instances of the monad laws with extra universe polymorphism.

module Monad-laws where

  left-identity : ∀ {a b} {A : Type a} {B : Type b} x (f : A → B ⊥) →
                  now x >>=′ f ≡ f x
  left-identity _ _ = now->>=

  right-identity : ∀ {a} {A : Type a} (x : A ⊥) →
                   x >>=′ now ≡ x
  right-identity = ⊥-rec-⊥
    (record
       { pe = never >>=′ now  ≡⟨ never->>= ⟩∎
              never           ∎
       ; po = λ x →
                now x >>=′ now  ≡⟨ now->>= ⟩∎
                now x           ∎
       ; pl = λ s hyp →
                ⨆ s >>=′ now        ≡⟨ ⨆->>= ⟩
                ⨆ (now ∗-inc s)     ≡⟨ cong ⨆ (_↔_.to equality-characterisation-increasing λ n →

                  s [ n ] >>=′ now       ≡⟨ hyp n ⟩∎
                  s [ n ]                ∎) ⟩∎

                ⨆ s                 ∎
       ; pp = λ _ → ⊥-is-set
       })

  associativity : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
                  (x : A ⊥) (f : A → B ⊥) (g : B → C ⊥) →
                  x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
  associativity x f g = ⊥-rec-⊥
    (record
       { pe = (never >>=′ λ x → f x >>=′ g)  ≡⟨ never->>= ⟩
              never                          ≡⟨ sym never->>= ⟩
              never >>=′ g                   ≡⟨ cong (_>>=′ g) $ sym never->>= ⟩∎
              never >>=′ f >>=′ g            ∎
       ; po = λ x →
                (now x >>=′ λ x → f x >>=′ g)  ≡⟨ now->>= ⟩
                f x >>=′ g                     ≡⟨ cong (_>>=′ g) $ sym now->>= ⟩∎
                now x >>=′ f >>=′ g            ∎
       ; pl = λ s hyp →
                (⨆ s >>=′ λ x → f x >>=′ g)        ≡⟨ ⨆->>= ⟩
                ⨆ ((λ x → f x >>=′ g) ∗-inc s)     ≡⟨ cong ⨆ (_↔_.to equality-characterisation-increasing λ n →

                  s [ n ] >>=′ (λ x → f x >>=′ g)       ≡⟨ hyp n ⟩∎
                  s [ n ] >>=′ f >>=′ g                 ∎) ⟩

                ⨆ (g ∗-inc (f ∗-inc s))            ≡⟨ sym ⨆->>= ⟩
                ⨆ (f ∗-inc s) >>=′ g               ≡⟨ cong (_>>=′ g) (sym ⨆->>=) ⟩∎
                ⨆ s >>=′ f >>=′ g                  ∎
       ; pp = λ _ → ⊥-is-set
       })
    x

open Monad equality-with-J hiding (map; map-id; map-∘)

instance

  -- The partiality monad's monad instance.

  partiality-raw-monad : ∀ {ℓ} → Raw-monad (_⊥ {a = ℓ})
  Raw-monad.return partiality-raw-monad = now
  Raw-monad._>>=_  partiality-raw-monad = _>>=′_

  partiality-monad : ∀ {ℓ} → Monad (_⊥ {a = ℓ})
  Monad.raw-monad      partiality-monad = partiality-raw-monad
  Monad.left-identity  partiality-monad = Monad-laws.left-identity
  Monad.right-identity partiality-monad = Monad-laws.right-identity
  Monad.associativity  partiality-monad = Monad-laws.associativity

------------------------------------------------------------------------
-- _⊥ is a functor

map : ∀ {a b} {A : Type a} {B : Type b} →
      (A → B) → [ A ⊥→ B ⊥]
map f = (return ∘ f) ∗

map-id : ∀ {a} {A : Type a} →
         map (id {A = A}) ≡ idω
map-id =
  return ∗  ≡⟨ _↔_.to equality-characterisation-continuous (λ x →

    x >>= return  ≡⟨ right-identity x ⟩∎
    x             ∎) ⟩∎

  idω       ∎

map-∘ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c}
        (f : B → C) (g : A → B) →
        map (f ∘ g) ≡ map f ∘ω map g
map-∘ f g =
  (now ∘ f ∘ g) ∗                ≡⟨ _↔_.to equality-characterisation-continuous (λ x →

    x >>=′ (now ∘ f ∘ g)                     ≡⟨ cong (x >>=′_) (⟨ext⟩ λ _ → sym now->>=) ⟩
    x >>=′ (λ x → now (g x) >>=′ (now ∘ f))  ≡⟨ Monad-laws.associativity x (now ∘ g) (now ∘ f) ⟩∎
    x >>=′ (now ∘ g) >>=′ (now ∘ f)          ∎) ⟩∎

  (now ∘ f) ∗ ∘ω (now ∘ g) ∗  ∎

------------------------------------------------------------------------
-- Some properties

-- A kind of inversion lemma for _⇓_.

>>=-⇓ :
  ∀ {a b} {A : Type a} {B : Type b}
    {x : A ⊥} {f : A → B ⊥} {y} →
  (x >>=′ f ⇓ y) ≃ ∥ ∃ (λ z → x ⇓ z × f z ⇓ y) ∥
>>=-⇓ {x = x} {f} {y} = ⊥-rec-⊥
  (record
     { P  = λ x → (x >>=′ f ⇓ y) ≃ ∥ ∃ (λ z → x ⇓ z × f z ⇓ y) ∥
     ; pe = never >>=′ f ⇓ y                   ↝⟨ ≡⇒↝ _ (cong (_⇓ y) never->>=) ⟩
            never ⇓ y                          ↝⟨ never⇓≃⊥ ⟩
            Prelude.⊥                          ↔⟨ inverse (not-inhabited⇒∥∥↔⊥ id) ⟩
            ∥ Prelude.⊥ ∥                      ↔⟨ ∥∥-cong (inverse ×-right-zero) ⟩
            ∥ ∃ (λ z → ⊥₀) ∥                   ↔⟨ ∥∥-cong (∃-cong (λ _ → inverse ×-left-zero)) ⟩
            ∥ ∃ (λ z → Prelude.⊥ × f z ⇓ y) ∥  ↝⟨ ∥∥-cong (∃-cong (λ _ → inverse never⇓≃⊥ ×-cong F.id)) ⟩□
            ∥ ∃ (λ z → never ⇓ z × f z ⇓ y) ∥  □
     ; po = λ x →
              now x >>=′ f ⇓ y                                   ↝⟨ ≡⇒↝ _ (cong (_⇓ y) now->>=) ⟩
              f x ⇓ y                                            ↔⟨ inverse (∥∥↔ ⊥-is-set) ⟩
              ∥ f x ⇓ y ∥                                        ↔⟨ ∥∥-cong (inverse $ drop-⊤-left-Σ $
                                                                      _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) ⟩
              ∥ ∃ (λ (p : ∃ (λ z → x ≡ z)) → f (proj₁ p) ⇓ y) ∥  ↔⟨ ∥∥-cong (inverse Σ-assoc) ⟩
              ∥ ∃ (λ z → x ≡ z × f z ⇓ y) ∥                      ↔⟨ inverse $ Trunc.flatten′
                                                                      (λ F → ∃ (λ _ → F (_ ≡ _) × _))
                                                                      (λ f → Σ-map id (Σ-map f id))
                                                                      (λ { (x , y , z) → ∥∥-map ((x ,_) ∘ (_, z)) y }) ⟩
              ∥ ∃ (λ z → ∥ x ≡ z ∥ × f z ⇓ y) ∥                  ↝⟨ ∥∥-cong (∃-cong λ _ → inverse now≡now≃∥≡∥ ×-cong F.id) ⟩□
              ∥ ∃ (λ z → now x ⇓ z × f z ⇓ y) ∥                  □
     ; pl = λ s ih →
              ⨆ s >>=′ f ⇓ y                                     ↝⟨ ≡⇒↝ _ (cong (_⇓ y) ⨆->>=) ⟩
              ⨆ (f ∗-inc s) ⇓ y                                  ↝⟨ ⨆⇓≃∥∃⇓∥ ⟩
              ∥ (∃ λ n → s [ n ] >>=′ f ⇓ y) ∥                   ↝⟨ ∥∥-cong (∃-cong ih) ⟩
              ∥ (∃ λ n → ∥ ∃ (λ z → s [ n ] ⇓ z × f z ⇓ y) ∥) ∥  ↔⟨ Trunc.flatten′ (λ F → ∃ λ _ → F (∃ λ _ → _ × _))
                                                                                (λ f → Σ-map id f)
                                                                                (uncurry λ x → ∥∥-map (x ,_)) ⟩
              ∥ (∃ λ n → ∃ λ z → s [ n ] ⇓ z × f z ⇓ y) ∥        ↔⟨ ∥∥-cong ∃-comm ⟩
              ∥ (∃ λ z → ∃ λ n → s [ n ] ⇓ z × f z ⇓ y) ∥        ↔⟨ ∥∥-cong (∃-cong λ _ → Σ-assoc) ⟩
              ∥ (∃ λ z → (∃ λ n → s [ n ] ⇓ z) × f z ⇓ y) ∥      ↔⟨ inverse $ Trunc.flatten′
                                                                      (λ F → (∃ λ _ → F (∃ λ _ → _ ⇓ _) × _))
                                                                      (λ f → Σ-map id (Σ-map f id))
                                                                      (λ { (x , y , z) → ∥∥-map ((x ,_) ∘ (_, z)) y }) ⟩
              ∥ (∃ λ z → ∥ (∃ λ n → s [ n ] ⇓ z) ∥ × f z ⇓ y) ∥  ↝⟨ ∥∥-cong (∃-cong λ _ → inverse ⨆⇓≃∥∃⇓∥ ×-cong F.id) ⟩□
              ∥ ∃ (λ z → ⨆ s ⇓ z × f z ⇓ y) ∥                    □
     ; pp = λ _ → Eq.right-closure ext 0 truncation-is-proposition
     })
  x

-- □ is closed, in a certain sense, under bind.

□->>= :
  ∀ {a b p q}
    {A : Type a} {B : Type b} {P : A → Type p} {Q : B → Type q}
    {x : A ⊥} {f : A → B ⊥} →
  (∀ x → Is-proposition (Q x)) →
  □ P x → (∀ {x} → P x → □ Q (f x)) → □ Q (x >>=′ f)
□->>= {Q = Q} {x} {f} Q-prop □-x □-f y =
  x >>=′ f ⇓ y                   ↔⟨ >>=-⇓ ⟩
  ∥ (∃ λ z → x ⇓ z × f z ⇓ y) ∥  ↝⟨ Trunc.rec (Q-prop y) (λ { (z , x⇓z , fz⇓y) → □-f (□-x z x⇓z) y fz⇓y }) ⟩□
  Q y                            □

-- ◇ is closed, in a certain sense, under bind.

◇->>= :
  ∀ {a b p q}
    {A : Type a} {B : Type b} {P : A → Type p} {Q : B → Type q}
    {x : A ⊥} {f : A → B ⊥} →
  ◇ P x → (∀ {x} → P x → ◇ Q (f x)) → ◇ Q (x >>=′ f)
◇->>= {x = x} {f} ◇-x ◇-f = Trunc.rec
  truncation-is-proposition
  (λ { (y , x⇓y , Py) →
       ∥∥-map (λ { (z , fy⇓z , Qz) →
                     z
                   , (x >>=′ f      ≡⟨ cong (_>>=′ f) x⇓y ⟩
                      now y >>=′ f  ≡⟨ now->>= ⟩
                      f y           ≡⟨ fy⇓z ⟩∎
                      now z         ∎)
                   , Qz
                 })
              (◇-f Py)
     })
  ◇-x

-- Certain nested occurrences of ⨆ can be replaced by a single one.

⨆>>=⨆≡⨆>>= :
  ∀ {a b} {A : Type a} {B : Type b} →
  ∀ (s : Increasing-sequence A) (f : A → Increasing-sequence B)
    {inc₁ inc₂} →
  ⨆ ((λ n → s [ n ] >>=′ ⨆ ∘ f) , inc₁) ≡
  ⨆ ((λ n → s [ n ] >>=′ λ y → f y [ n ]) , inc₂)
⨆>>=⨆≡⨆>>= s f = antisymmetry
  (least-upper-bound _ _ λ n →
   _≃_.to ≼≃⊑ $ λ z →

     s [ n ] >>=′ ⨆ ∘ f ⇓ z                                   ↔⟨ >>=-⇓ ⟩
     ∥ (∃ λ y → s [ n ] ⇓ y × ⨆ (f y) ⇓ z) ∥                  ↔⟨ ∥∥-cong (∃-cong λ _ → F.id ×-cong ⨆⇓≃∥∃⇓∥) ⟩
     ∥ (∃ λ y → s [ n ] ⇓ y × ∥ (∃ λ m → f y [ m ] ⇓ z) ∥) ∥  ↔⟨ Trunc.flatten′
                                                                   (λ F → ∃ λ _ → _ × F (∃ λ _ → _ ⇓ _))
                                                                   (λ f → Σ-map id (Σ-map id f))
                                                                   (λ { (y , p , q) → ∥∥-map ((y ,_) ∘ (p ,_)) q }) ⟩
     ∥ (∃ λ y → s [ n ] ⇓ y × ∃ λ m → f y [ m ] ⇓ z) ∥        ↔⟨ ∥∥-cong (∃-cong λ _ → ∃-comm) ⟩
     ∥ (∃ λ y → ∃ λ m → s [ n ] ⇓ y × f y [ m ] ⇓ z) ∥        ↝⟨ ∥∥-map (Σ-map id lemma) ⟩
     ∥ (∃ λ y → ∃ λ m → s [ m ] ⇓ y × f y [ m ] ⇓ z) ∥        ↔⟨ ∥∥-cong ∃-comm ⟩
     ∥ (∃ λ m → ∃ λ y → s [ m ] ⇓ y × f y [ m ] ⇓ z) ∥        ↔⟨ inverse $ Trunc.flatten′
                                                                   (λ F → ∃ λ _ → F (∃ λ _ → _ × _))
                                                                   (λ f → Σ-map id f)
                                                                   (λ { (m , p) → ∥∥-map (m ,_) p }) ⟩
     ∥ (∃ λ m → ∥ (∃ λ y → s [ m ] ⇓ y × f y [ m ] ⇓ z) ∥) ∥  ↔⟨ ∥∥-cong (∃-cong λ _ → inverse $ >>=-⇓) ⟩
     ∥ (∃ λ m → (s [ m ] >>=′ λ y → f y [ m ]) ⇓ z) ∥         ↔⟨ inverse ⨆⇓≃∥∃⇓∥ ⟩□
     ⨆ ((λ m → s [ m ] >>=′ λ y → f y [ m ]) , _) ⇓ z         □)

  (⨆-mono λ n →

    (s [ n ] >>=′ λ y → f y [ n ])  ⊑⟨ ⊑-refl (s [ n ]) >>=-mono (λ y → upper-bound (f y) n) ⟩■
    (s [ n ] >>=′ ⨆ ∘ f)            ■)

  where
  lemma :
    ∀ {n y z} →
    (∃ λ m → s [ n ] ⇓ y × f y [ m ] ⇓ z) →
    (∃ λ m → s [ m ] ⇓ y × f y [ m ] ⇓ z)
  lemma {n} (m , p , q) with Nat.total m n
  ... | inj₁ m≤n = n
                 , p
                 , _≃_.from ≼≃⊑ (later-larger (f _) m≤n) _ q
  ... | inj₂ n≤m = m
                 , _≃_.from ≼≃⊑ (later-larger s n≤m) _ p
                 , q

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
  postulate
    F : Set₂ → Set₃
    G : Set₁ → Set₂
    H : Set₀ → Set₁

  infix 1 F
  infix 2 G
  infix 3 H

  syntax F x = ! x
  syntax G x = # x
  syntax H x = ! x

  ok₁ : Set₀ → Set₂
  ok₁ X = # ! X

  ok₂ : Set₁ → Set₃
  ok₂ X = ! # X


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

module n2o.N2O where

open import proto.Base
open import proto.Core
open import proto.IO

open import n2o.Network.WebSocket
open import n2o.Network.Socket
open import n2o.Network.Core
open import n2o.Network.Internal

-- open import Infinity.Proto

postulate
    terminationCheck : IO ⊤

{-# FOREIGN GHC
import Control.Concurrent (threadDelay)
terminationCheck :: IO ()
terminationCheck = do
    putStrLn "sapere aude"
    threadDelay 1000000
    terminationCheck #-}

{-# COMPILE GHC terminationCheck = terminationCheck #-}

data Example : Set where
    Greet : Example

-- index Init = do
--   updateText "system" "What is your name?"
--   wire record { id_ = "send" , postback = Just Greet, source = "name" ∷ [] }
-- index (Message Greet) = do
--   Just name ← get "name"
--   updateText "system" ("Hello, " <> jsEscape name)
index : Event Example → IO ⊤
index ev = putStrLn "Unknown event" -- TODO : monoids

about : Event Example → IO ⊤
about ev = putStrLn "Unknown event"

-- route : Context N2OProto Example → Context N2OProto Example
-- route c with (unpack (Request.reqPath (Context.cxRequest c)))
-- ... | "/ws/samples/static/index.html" = about
-- ... | "/ws/samples/static/about.html" = about
-- ... | _ = about

-- router : Context N2OProto Example → Context N2OProto Example
-- router c = record c { handler = mkHandler route }

-- protocols :

-- cx : Cx Example
-- cx = mkCx h r m p a d
--   where h = ?
--         r = ?
--         m = route ∷ []
--         p = []
--         a = ?
--         d = ?

main : IO ⊤
main = do
    -- sock ← socket AF_INET Stream (+ 0)
    hPutStrLn stdout "asd"
    -- protoRun 0 protos
    terminationCheck
    putStrLn "[*] Done"

-- main : IO ⊤
-- main = getLine >>= λ s → putStrLn s


text:
module Syntax where

data S
  (A₁ : Set)
  (A₂ : A₁ → Set)
  : Set
  where

  _,_
    : (x₁ : A₁)
    → A₂ x₁
    → S A₁ A₂

syntax S A₁ (λ x → A₂)
  = x ∈ A₁ × A₂

module M where

  data S'
    (A₁ : Set)
    (A₂ : A₁ → Set)
    : Set
    where

    _,'_
      : (x₁ : A₁)
      → A₂ x₁
      → S' A₁ A₂

  syntax S' A₁ (λ x → A₂)
    = x ∈' A₁ ×' A₂

open M
  using (S')

postulate

  p1
    : {A₁ : Set}
    → {A₂ : A₁ → Set}
    → x₁ ∈ A₁ × A₂ x₁
    → A₁

  p1'
    : {A₁ : Set}
    → {A₂ : A₁ → Set}
    → x₁ ∈' A₁ ×' A₂ x₁
    → A₁

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
-- Andreas, Issue 1944, Bengtfest Marsstrand 2016-04-28

-- A reason why issue 1098 (automatic opening of record modules)
-- cannot easily be fixed

data Bool : Set where
  true false : Bool

if_then_else_ : ∀{A : Set} → Bool → A → A → A
if true  then t else e = t
if false then t else e = e

record Testable (A : Set) : Set where
  field
    test : A -> Bool
open Testable {{...}}
open Testable  -- overloading projection `test`

mytest : ∀{A} → Testable A → A → Bool
mytest dict = test dict  -- Should work.

t : ∀{A}{{_ : Testable A}} → A → A
t = λ x → if test x then x else x
-- This may fail when test is overloaded.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Functors on indexed sets (predicates)
------------------------------------------------------------------------

-- Note that currently the functor laws are not included here.

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

module Category.Functor.Predicate where

open import Function
open import Level
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (PT)

record RawPFunctor {i j ℓ₁ ℓ₂} {I : Set i} {J : Set j}
                   (F : PT I J ℓ₁ ℓ₂) : Set (i ⊔ j ⊔ suc ℓ₁ ⊔ suc ℓ₂)
                   where
  infixl 4 _<$>_ _<$_

  field
    _<$>_ : ∀ {P Q} → P ⊆ Q → F P ⊆ F Q

  _<$_ : ∀ {P Q} → (∀ {i} → P i) → F Q ⊆ F P
  x <$ y = const x <$> y


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

open import Categories.Category

module Categories.Monad.Duality {o ℓ e} (C : Category o ℓ e) where

open import Categories.Functor
open import Categories.NaturalTransformation
open import Categories.Monad
open import Categories.Comonad

private
  module C = Category C
  open C
  open HomReasoning

coMonad⇒Comonad : Monad C.op → Comonad C
coMonad⇒Comonad M = record
    { F         = Functor.op F
    ; ε         = NaturalTransformation.op η
    ; δ         = NaturalTransformation.op μ
    ; assoc     = M.sym-assoc
    ; sym-assoc = M.assoc
    ; identityˡ = M.identityˡ
    ; identityʳ = M.identityʳ
    }
  where module M = Monad M
        open M using (F; η; μ)

Comonad⇒coMonad : Comonad C → Monad C.op
Comonad⇒coMonad M = record
    { F         = Functor.op F
    ; η         = NaturalTransformation.op ε
    ; μ         = NaturalTransformation.op δ
    ; assoc     = M.sym-assoc
    ; sym-assoc = M.assoc
    ; identityˡ = M.identityˡ
    ; identityʳ = M.identityʳ
    }
  where module M = Comonad M
        open M using (F; ε; δ)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Reflection
open import Reflection.Term
open import Reflection.Universe
open import Reflection.Annotated
open import Agda.Builtin.Reflection using (withReconstructed; dontReduceDefs; onlyReduceDefs)
open import Relation.Nullary
open import Data.String as S
open import Data.Maybe hiding (_>>=_)
open import Data.Unit
open import Function
open import Data.List as L
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.Nat
open import Data.Product
open import Data.Bool

-- Get a reference to the local term such as where-function or
-- with- or rewrite- by its name.
get-defn : String → AnnotationFun (λ _ → Maybe Name)
get-defn n ⟨term⟩ (def f x) with showName f S.≟ n
...                         | yes _ = just f
...                         | no  _ = nothing
get-defn n u t = defaultAnn nothing _<∣>_ u t

do-get-defn : String → ∀ {u} → (t : ⟦ u ⟧) → Annotated (λ _ → Maybe Name) t
do-get-defn n = annotate (get-defn n)

to-pat-lam : Definition → TC (Maybe Term)
to-pat-lam (function cs) = return $ just (pat-lam cs [])
to-pat-lam _ = return $ nothing

tel-norm : Names → Telescope → Telescope → TC Telescope
tel-norm base-funs [] ctx = return []
tel-norm base-funs ((v , arg i x) ∷ tel) ctx = do
  x ← dontReduceDefs base-funs
      $ inContext (reverse $ L.map proj₂ ctx)
      $ withReconstructed
      $ normalise x
      --$ reduce x
  let p = (v , arg i x)
  tel ← tel-norm base-funs tel (ctx L.++ [ p ])
  return $! p ∷ tel

pat-lam-norm : Term → Names → TC Term
pat-lam-norm (pat-lam cs args) base-funs = do
  cs ← hlpr cs
  return $ pat-lam cs args
  where
    hlpr : List Clause → TC $ List Clause
    hlpr [] = return []
    hlpr (clause tel ps t ∷ l) = do
      --gctx ← getContext

      -- Try normalising telescope
      tel ← tel-norm base-funs tel []
      let ctx = reverse $ L.map proj₂ tel
      t ← dontReduceDefs base-funs
          $ inContext ctx --(gctx L.++ ctx)
          $ withReconstructed
          $ normalise t
          --$ reduce t
      l ← hlpr l
      return $! clause tel ps t ∷ l
    hlpr (absurd-clause tel ps ∷ l) = do
      l ← hlpr l
      return $! absurd-clause tel ps ∷ l
pat-lam-norm t _ = return t

get-term : (f : Name) (base-funs : List Name) → TC Term
get-term t bf = do
     td ← withReconstructed $ dontReduceDefs bf $ getDefinition t
     just te ← to-pat-lam td where _ → typeError [ strErr $ "get-term: " S.++ showName t S.++ " is not a function" ]
     te ← pat-lam-norm te bf
     return te

get-ty : (f : Name) (base-funs : List Name) → TC Term
get-ty t bf = do
     ty ← getType t
     withReconstructed $ dontReduceDefs bf $ normalise ty

-- A helper function to get a term or a type (first parameter true/false) using
-- the chain of names so that we could traverse into helper functions.  For example
-- assume that `f` has  `with-x` in its body which in turn has `rewrite-y` which we
-- want to obtain.  Then we should call frefln as follows:
--
--     frefln true ("with-x" ∷ "rewrite-y" ∷ []) (base-funs) (quote f)
frefln-h : Bool → (name-chain : List String) (base-funs : Names) → Name → TC Term
frefln-h true [] bf t  = get-term t bf
frefln-h false [] bf t = get-ty t bf
frefln-h te/ty (x ∷ ns) bf t = do
     xt ← get-term t bf
     case (ann $ do-get-defn x {⟨term⟩} xt) of λ where
       (nothing) → typeError [ strErr $ "frefln: cannot find name `" S.++ x S.++ "` in term " S.++ showName t ]
       (just f') → frefln-h te/ty ns bf f'

macro
  frefl : Name → List Name → Term → TC ⊤
  frefl n bf a = frefln-h true [] bf n >>= quoteTC >>= unify a

  fty : Name → List Name → Term → TC ⊤
  fty n bf a = frefln-h false [] bf n >>= quoteTC >>= unify a

  frefln : Name → List Name → List String → Term → TC ⊤
  frefln n bf ns a = frefln-h true ns bf n >>= quoteTC >>= unify a

  ftyn : Name → List Name → List String → Term → TC ⊤
  ftyn n bf ns a = frefln-h false ns bf n >>= quoteTC >>= unify a
{-
  -- For debugging purposes.
  frefl : Name → List Name → Term → TC ⊤
  frefl f base-funs a = do

     ty ← getType f
     ty ← withReconstructed $ dontReduceDefs base-funs $ normalise ty
     te ← withReconstructed $ getDefinition f >>= λ where
           (function cs) → return $ pat-lam cs []
           _ → return unknown
     te ← pat-lam-norm te base-funs
     q ← quoteTC te
     unify a q

  fty : Name → List Name → Term → TC ⊤
  fty f base-funs a = do
     ty ← getType f
     ty ← withReconstructed $ dontReduceDefs base-funs $ normalise ty
     q ← quoteTC ty
     unify a q

  -- XXX We can generalise this to List of names, then the local function can be
  -- at arbitrary depth.
  frefl2 : Name → String → Term → TC ⊤
  frefl2 f na a = do
     td ← withReconstructed $ getDefinition f
     just te ← to-pat-lam td where _ → typeError [ strErr "ERROR₁" ]
     te ← pat-lam-norm te []
     --te ← normalise te
     case (ann $ do-get-defn na {⟨term⟩} te) of λ where
       (nothing) → typeError [ strErr "ERROR₁" ]
       (just f') → do
          td' ← withReconstructed $ getDefinition f
          just te ← to-pat-lam td' where _ → typeError [ strErr "ERROR₃" ]
          quoteTC te >>= unify a

  fty2 : Name → String → Term → TC ⊤
  fty2 f na a = do
     td ← withReconstructed $ getDefinition f
     just te ← to-pat-lam td where _ → typeError [ strErr "ERROR₁" ]
     te ← pat-lam-norm te []
     --te ← normalise te
     case (ann $ do-get-defn na {⟨term⟩} te) of λ where
       (nothing) → typeError [ strErr "ERROR₁" ]
       (just f') → do
          ty ← getType f'
          ty ← withReconstructed $ normalise ty
          quoteTC ty >>= unify a
-}

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
------------------------------------------------------------------------------
-- The relation of divisibility on partial natural numbers
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Divisibility.By0 where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat

infix 4 _∣_

------------------------------------------------------------------------------
-- The relation of divisibility (the symbol is '\mid' not '|')
--
-- (See documentation in FOTC.Data.Nat.Divisibility.By0)
--
-- In our definition 0∣0, which is used to prove properties of the gcd
-- as it is in GHC ≥ 7.2.1, where gcd 0 0 = 0 (see
-- http://hackage.haskell.org/trac/ghc/ticket/3304).

-- Note that @k@ should be a total natural number.
_∣_ : D → D → Set
m ∣ n = ∃[ k ] N k ∧ n ≡ k * m

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module FFI.IO where

import      Lvl
open import Data
open import String
open import Type

postulate IO : ∀{a} → Type{a} → Type{a}
{-# BUILTIN IO IO #-}
{-# FOREIGN GHC type AgdaIO a b = IO b #-}
{-# COMPILE GHC IO = type AgdaIO #-}

{-# FOREIGN GHC import qualified Data.Text.IO #-}

postulate printStr : String → IO(Unit{Lvl.𝟎})
{-# COMPILE GHC printStr = Data.Text.IO.putStr #-}

postulate printStrLn : String → IO(Unit{Lvl.𝟎})
{-# COMPILE GHC printStrLn = Data.Text.IO.putStrLn #-}

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

open import lib.Basics
open import lib.NType2

-- [Subtype] is defined in lib.NType.

module lib.types.Subtype where

infix 40 _⊆_
_⊆_ : ∀ {i j₁ j₂} {A : Type i} → SubtypeProp A j₁ → SubtypeProp A j₂
  → Type (lmax i (lmax j₁ j₂))
P₁ ⊆ P₂ = ∀ a → SubtypeProp.prop P₁ a → SubtypeProp.prop P₂ a

infix 80 _∘sub_
_∘sub_ : ∀ {i j k} {A : Type i} {B : Type j}
  → SubtypeProp B k → (A → B) → SubtypeProp A k
P ∘sub f = SubtypeProp.prop P ∘ f , level where
  abstract level = SubtypeProp.level P ∘ f

{- Dependent paths in a Σ-type -}
module _ {i j k} {A : Type i} {B : A → Type j} (subB : (a : A) → SubtypeProp (B a) k)
  where

  ↓-Subtype-in : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : SubtypeProp.prop (subB x) r} {s' : SubtypeProp.prop (subB x') r'}
    (q : r == r' [ B ↓ p ])
    → (r , s) == (r' , s') [ (λ x → Subtype (subB x)) ↓ p ]
  ↓-Subtype-in {p = idp} q = Subtype=-out (subB _) q

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module _ where

module A where
  postulate
    Nat : Set
    suc : Nat → Nat

open A

syntax suc x = ⟦ x ⟧

-- Error WAS:
-- Names out of scope in fixity declarations: suc

-- Error SHOULD BE something like:
-- Name 'suc' not declared in same scope as its syntax declaration.


text:
{-# OPTIONS  --sized-types --show-implicit #-}
-- {-# OPTIONS -v tc.size.solve:60 #-}
module Issue300 where

open import Common.Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

-- Size meta used in a different context than the one created in

A : Set1
A = (Id : {i : Size} -> Nat {_} -> Set)
    (k : Size)(m : Nat {↑ k}) -> Id {k} m
    ->
    (j : Size)(n : Nat {j}) -> Id {j} n
-- should solve _ with ↑ i

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module sn-calculus-compatconf.base where

open import sn-calculus
open import utility renaming (_U̬_ to _∪_)

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
  using (Can ; Canₛ ; Canₛₕ ; Canₖ ; module CodeSet)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Context.Properties
  using (unplug ; unplugc ; plug ; plugc ; ⟦⟧e-to-⟦⟧c)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning)
open import Data.Bool
  using (Bool ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _∷_ ; [] ; _++_ ; map)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function using (_∘_ ; id ; _∋_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open EvaluationContext1
open _≐_⟦_⟧e
open Context1
open _≐_⟦_⟧c

open ListSet Data.Nat._≟_

data two-roads-diverged : EvaluationContext → Context → Set where
  divout-disjoint : ∀ {C₁ C}    → two-roads-diverged []                         (C₁ ∷ C)
  divpar-split₁   : ∀ {E C p q} → two-roads-diverged (epar₁ q ∷ E) (ceval (epar₂ p) ∷ C)
  divpar-split₂   : ∀ {E C p q} → two-roads-diverged (epar₂ p ∷ E) (ceval (epar₁ q) ∷ C)
  divseq-split    : ∀ {E C p q} → two-roads-diverged (eseq q  ∷ E) (cseq₂ p         ∷ C)
  divloop-splitˢ  : ∀ {E C p q} → two-roads-diverged (eloopˢ q  ∷ E) (cloopˢ₂ p       ∷ C)
  divin : ∀ {E₁ E C} → two-roads-diverged E C → two-roads-diverged (E₁ ∷ E) (ceval E₁ ∷ C)

data context-prefix : EvaluationContext → Context → Set where
  ecsame     : ∀ {E}       → context-prefix E                (map ceval E)
  ecin-lift  : ∀ {E E₁ E'} → context-prefix (E ++ (E₁ ∷ E')) (map ceval E)
  ecsplit    : ∀ {E C} → (div : two-roads-diverged E C) → context-prefix E C

get-context-prefix : ∀ {E C p q r} →
  p ≐ E ⟦ q ⟧e → p ≐ C ⟦ r ⟧c →
  context-prefix E C
get-context-prefix {[]} {[]} dehole p≐C⟦r⟧ = ecsame
get-context-prefix {[]} {C₁ ∷ C} dehole p≐C⟦r⟧ = ecsplit divout-disjoint
get-context-prefix {E₁ ∷ E} p≐E⟦q⟧ dchole = ecin-lift
get-context-prefix (depar₁ p≐E⟦q⟧) (dcpar₂ p≐C⟦r⟧) = ecsplit divpar-split₁
get-context-prefix (depar₂ p≐E⟦q⟧) (dcpar₁ p≐C⟦r⟧) = ecsplit divpar-split₂
get-context-prefix (deseq  p≐E⟦q⟧) (dcseq₂ p≐C⟦r⟧) = ecsplit divseq-split
get-context-prefix (deloopˢ p≐E⟦q⟧) (dcloopˢ₂ p≐C⟦r⟧) = ecsplit divloop-splitˢ
get-context-prefix (depar₁ p≐E⟦q⟧) (dcpar₁ p≐C⟦r⟧)
  with get-context-prefix p≐E⟦q⟧ p≐C⟦r⟧
... | ecsame         = ecsame
... | ecin-lift      = ecin-lift
... | ecsplit    div = ecsplit (divin div)
get-context-prefix (depar₂ p≐E⟦q⟧) (dcpar₂ p≐C⟦r⟧)
  with get-context-prefix p≐E⟦q⟧ p≐C⟦r⟧
... | ecsame         = ecsame
... | ecin-lift      = ecin-lift
... | ecsplit    div = ecsplit (divin div)
get-context-prefix (deloopˢ p≐E⟦q⟧)  (dcloopˢ₁ p≐C⟦r⟧)
  with get-context-prefix p≐E⟦q⟧ p≐C⟦r⟧
... | ecsame         = ecsame
... | ecin-lift      = ecin-lift
... | ecsplit    div = ecsplit (divin div)
get-context-prefix (deseq p≐E⟦q⟧)  (dcseq₁ p≐C⟦r⟧)
  with get-context-prefix p≐E⟦q⟧ p≐C⟦r⟧
... | ecsame         = ecsame
... | ecin-lift      = ecin-lift
... | ecsplit    div = ecsplit (divin div)
get-context-prefix (desuspend p≐E⟦q⟧) (dcsuspend p≐C⟦r⟧)
  with get-context-prefix p≐E⟦q⟧ p≐C⟦r⟧
... | ecsame         = ecsame
... | ecin-lift      = ecin-lift
... | ecsplit    div = ecsplit (divin div)
-- didn't directly pattern match on p≐C⟦r⟧ in order to get complete pattern matching coverage
get-context-prefix (detrap p≐E⟦q⟧) p≐trap[C⟦r⟧] with p≐trap[C⟦r⟧]
... | dchole       = ecin-lift
... | dctrap p≐C⟦r⟧ with get-context-prefix p≐E⟦q⟧ p≐C⟦r⟧
... | ecsame         = ecsame
... | ecin-lift      = ecin-lift
... | ecsplit    div = ecsplit (divin div)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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

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

import      LibraBFT.Impl.OBM.Genesis                      as Genesis
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.OBM.Util
import      LibraBFT.Impl.Types.OnChainConfig.ValidatorSet as ValidatorSet
import      LibraBFT.Impl.Types.ValidatorVerifier          as ValidatorVerifier
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.OBM.Util
import      LibraBFT.Impl.Types.OnChainConfig.ValidatorSet as ValidatorSet
import      LibraBFT.Impl.Types.ValidatorVerifier          as ValidatorVerifier
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Util.PKCS
open import Util.Prelude

module LibraBFT.Impl.IO.OBM.GenKeyFile where

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

EndpointAddress           = Author
AddressToSkAndPkAssocList = List (EndpointAddress × (SK × PK))

------------------------------------------------------------------------------
genKeys   : {-Crypto.SystemDRG →-} ℕ   → List (SK × PK)
mkAuthors : {-Crypto.SystemDRG →-} U64 → List EndpointAddress
          → Either ErrLog AddressToSkAndPkAssocList
mkValidatorSignersAndVerifierAndProposerElection
          : U64 → AddressToSkAndPkAssocList
          → Either ErrLog (List ValidatorSigner × ValidatorVerifier × ProposerElection)
------------------------------------------------------------------------------

NfLiwsVssVvPe =
  (U64 × LedgerInfoWithSignatures × List ValidatorSigner × ValidatorVerifier × ProposerElection)

NfLiwsVsVvPe =
  (U64 × LedgerInfoWithSignatures × ValidatorSigner × ValidatorVerifier × ProposerElection)

create'
  : U64 → List EndpointAddress {-→ SystemDRG-}
  → Either ErrLog
    ( U64 × AddressToSkAndPkAssocList
    × List ValidatorSigner × ValidatorVerifier × ProposerElection × LedgerInfoWithSignatures )
create' numFailures addresses {-drg-} = do
 authors       ← mkAuthors {-drg-} numFailures addresses
 (s , vv , pe) ← mkValidatorSignersAndVerifierAndProposerElection numFailures authors
 case Genesis.obmMkGenesisLedgerInfoWithSignatures s (ValidatorSet.obmFromVV vv) of λ where
       (Left err)   → Left err
       (Right liws) → pure (numFailures , authors , s , vv , pe , liws)

abstract
  create = create'
  create≡ : create ≡ create'
  create≡ = refl

mkAuthors {-drg-} numFailures0 addresses0 = do
  addrs <- checkAddresses
  checkBftAndRun numFailures0 addrs f
 where
  f : ℕ → List EndpointAddress → AddressToSkAndPkAssocList
  f _numFailures addresses = zip addresses (genKeys {-drg-} (length addresses))
  checkAddresses : Either ErrLog (List EndpointAddress)
  checkAddresses = pure addresses0

postulate -- Valid assumption: secret and public keys for each NodeId
  mkSK : NodeId → SK
  mkPK : NodeId → PK

genKeys    zero   = []
genKeys x@(suc n) = (mkSK x , mkPK x) ∷ genKeys n

mkValidatorSignersAndVerifierAndProposerElection numFaults ks = do
  -- IMPL-DIFF: Agda Author type does NOT contain a PK
  let allAuthors       = fmap fst ks
  validatorVerifier    ← ValidatorVerifier.initValidatorVerifier numFaults ks
  let authorKeyPairs   = fmap (λ (a , (sk , _)) → (a , sk)) ks
      validatorSigners = foldl' go [] authorKeyPairs
  pure (validatorSigners , validatorVerifier , ProposerElection∙new allAuthors)
 where
  go : List ValidatorSigner → (Author × SK) → List ValidatorSigner
  go acc (author , sk) = ValidatorSigner∙new author sk ∷ acc


text:
-- A simple word counter

open import Coinduction using ( ♯_ )
open import Data.Char.Classifier using ( isSpace )
open import Data.Bool using ( Bool ; true ; false )
open import Data.Natural using ( Natural ; show )
open import System.IO using ( Command )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; _⟫_ ; _⟨&⟩_ )
open import System.IO.Transducers.List using ( length )
open import System.IO.Transducers.Bytes using ( bytes )
open import System.IO.Transducers.IO using ( run )
open import System.IO.Transducers.UTF8 using ( split ; encode )
open import System.IO.Transducers.Session using ( ⟨_⟩ ; _&_ ; Bytes ; Strings )

module System.IO.Examples.WC where

words : Bytes ⇒ ⟨ Natural ⟩
words = split isSpace ⟫ inp (♯ length { Bytes })

-- TODO: this isn't exactly lovely user syntax.

report : ⟨ Natural ⟩ & ⟨ Natural ⟩ ⇒ Strings
report =
  (inp (♯ λ #bytes →
  (out true
  (out (show #bytes)
  (out true
  (out " "
  (inp (♯ λ #words →
  (out true
  (out (show #words)
  (out true
  (out "\n"
  (out false done)))))))))))))

wc : Bytes ⇒ Bytes
wc = bytes ⟨&⟩ words ⟫ report ⟫ inp (♯ encode)

main : Command
main = run wc

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module _ where

data D (@erased A : Set) : Set

-- The modality should not be repeated here
data D (@erased A) where
  mkD : D A


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

module Class.Monad.IO where

open import Class.Monad
open import IO
open import Level

record MonadIO {a} (M : Set a → Set a) {{_ : Monad M}} : Set (suc a) where
  field
    liftIO : ∀ {A} → IO A → M A

open MonadIO {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
open import FRP.JS.Float using ( ℝ ) renaming ( _/?_ to _/?r_ )
open import FRP.JS.Int using ( ℤ ; _-_ ) renaming ( float to floatz ; show to showz )
open import FRP.JS.Primitive using ( String )
open import FRP.JS.Bool using ( Bool ; _∨_ ; not )
open import FRP.JS.True using ( True )
open import FRP.JS.Maybe using ( Maybe )

module FRP.JS.Nat where

infixr 4 _≤_ _<_ _≟_ _≠_
infixl 6 _+_ _∸_
infixl 7 _*_ _/_ _/?_

open import FRP.JS.Primitive public using ( ℕ ; zero ; suc )

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

{-# BUILTIN NATPLUS _+_ #-}
{-# COMPILED_JS _+_ function (x) { return function (y) { return x+y; }; } #-}

_∸_ : ℕ → ℕ → ℕ
zero  ∸ n     = zero
suc m ∸ zero  = suc m
suc m ∸ suc n = m ∸ n

{-# BUILTIN NATMINUS _∸_ #-}
{-# COMPILED_JS _∸_ function (x) { return function (y) { return Math.max(0,x-y); }; } #-}

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + m * n

{-# BUILTIN NATTIMES _*_ #-}
{-# COMPILED_JS _*_ function (x) { return function (y) { return x*y; }; } #-}

private
 primitive
  primNatEquality : ℕ → ℕ → Bool
  primNatLess : ℕ → ℕ → Bool
  primNatToInteger : ℕ → ℤ
  primFloatDiv : ℝ → ℝ → ℝ

_≟_ = primNatEquality
_<_ = primNatLess
+_ = primNatToInteger

{-# COMPILED_JS _≟_ function (x) { return function (y) { return x === y; }; } #-}
{-# COMPILED_JS _<_ function (x) { return function (y) { return x < y; }; } #-}
{-# COMPILED_JS +_ function (x) { return x; } #-}

float : ℕ → ℝ
float x = floatz (+ x)

show : ℕ → String
show x = showz (+ x)

-_ : ℕ → ℤ
-_ x = (+ 0) - (+ x)

_≤_ : ℕ → ℕ → Bool
x ≤ y = not (y < x)

_≠_ : ℕ → ℕ → Bool
x ≠ y = not (x ≟ y)

_/_ : (x y : ℕ) → {y≠0 : True (y ≠ 0)} → ℝ
x / y = primFloatDiv (float x) (float y)

_/?_ : ℕ → ℕ → Maybe ℝ
x /? y = (float x) /?r (float y)

{-# COMPILED_JS float function (x) { return x; } #-}
{-# COMPILED_JS show function (x) { return x.toString(); } #-}
{-# COMPILED_JS -_ function (x) { return -x; } #-}
{-# COMPILED_JS _≤_ function (x) { return function (y) { return x <= y; }; } #-}
{-# COMPILED_JS _≠_ function (x) { return function (y) { return x !== y; }; } #-}
{-# COMPILED_JS _/_  function(x) { return function(y) { return function() { return x / y; }; }; } #-}
{-# COMPILED_JS _/?_  function(x) { return function(y) { if (y === 0) { return null; } else { return x / y; } }; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

open import Categories.Category.Core
open import Categories.Object.Zero

-- Normal Mono and Epimorphisms
-- https://ncatlab.org/nlab/show/normal+monomorphism
module Categories.Morphism.Normal {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Zero : Zero 𝒞) where

open import Level

open import Categories.Object.Kernel 𝒞-Zero
open import Categories.Object.Kernel.Properties 𝒞-Zero
open import Categories.Morphism 𝒞

open Category 𝒞

record IsNormalMonomorphism {A K : Obj} (k : K ⇒ A) : Set (o ⊔ ℓ ⊔ e) where
  field
    {B} : Obj
    arr : A ⇒ B
    isKernel : IsKernel k arr

  open IsKernel isKernel public

  mono : Mono k
  mono = Kernel-Mono (IsKernel⇒Kernel isKernel)

record NormalMonomorphism (K A : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    mor : K ⇒ A
    isNormalMonomorphism : IsNormalMonomorphism mor

  open IsNormalMonomorphism isNormalMonomorphism public

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:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

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

open import LibraBFT.Base.PKCS
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures as LedgerInfoWithSignatures
open import LibraBFT.ImplShared.Consensus.Types

module LibraBFT.Impl.Types.CryptoProxies where

addToLi : AccountAddress → Signature → LedgerInfoWithSignatures → LedgerInfoWithSignatures
addToLi = LedgerInfoWithSignatures.addSignature

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
module TerminationNoArgs where

loop : Set
loop = loop

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module lib.libraryDec where

-- old version of Dec
--

open import Data.Empty
open import Level
open import Relation.Nullary using ( ¬_ )

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p :  ¬ P) → Dec P

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module UselessPrivateImportAs where

private
  import Common.Prelude as P


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solver for equations over product and sum types
--
-- See examples at the bottom of the file for how to use this solver
------------------------------------------------------------------------

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

module Function.Related.TypeIsomorphisms.Solver where

open import Algebra using (CommutativeSemiring)
import Algebra.Solver.Ring.NaturalCoefficients.Default
open import Data.Empty using (⊥)
open import Data.Product using (_×_)
open import Data.Sum using (_⊎_)
open import Data.Unit using (⊤)
open import Level using (Level; Lift)
open import Function.Inverse as Inv using (_↔_)
open import Function.Related as Related
open import Function.Related.TypeIsomorphisms

------------------------------------------------------------------------
-- The solver

module ×-⊎-Solver (k : Symmetric-kind) {ℓ} =
  Algebra.Solver.Ring.NaturalCoefficients.Default
    (×-⊎-commutativeSemiring k ℓ)

------------------------------------------------------------------------
-- Tests

private

  -- A test of the solver above.

  test : {ℓ : Level} (A B C : Set ℓ) →
         (Lift ℓ ⊤ × A × (B ⊎ C)) ↔ (A × B ⊎ C × (Lift ℓ ⊥ ⊎ A))
  test = solve 3 (λ A B C → con 1 :* (A :* (B :+ C)) :=
                            A :* B :+ C :* (con 0 :+ A))
                 Inv.id
    where open ×-⊎-Solver bijection


text:
module Sized.ConsoleExample where

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

open import NativeIO

myProgram  :  ∀{i} → IOConsole i Unit
force myProgram  =  do'  getLine         λ line →
                    do  (putStrLn line)  λ _ →
                    do  (putStrLn line)  λ _ →
                    myProgram

main  :  NativeIO Unit
main  =  translateIOConsole myProgram


text:
module Calculator where

open import Human.Humanity hiding (_==_)
open import Human.Nat public hiding (_==_)
open import Human.Char public
open import Human.Equality public

--------- Data ---------
-- Generic proof to proof "Or" operation. Proof that one of the arguments must be true
data Either (A B : Set) : Set where
  fst : A -> Either A B
  snd : B -> Either A B

-- Declaring a set of operations
data Operation : Set where
  add sub mul : Operation

-- It's used to identify which number will be updated, the one on the right or left
data Side : Set where
  right left : Side

-- Can be a number, an operation symbol or execution command
data Event : Set where
  clr : Event -- base case
  num : Side -> Nat -> Event -- a digit
  ope : Operation -> Event -- operator

data State : Set where
  state : Operation → Nat → Nat → State

--------- Auxiliar properties ---------
-- Proof of commutativity of addition. Proof by beala
x+0 : (a : Nat) → (a + 0) == a
x+0 zero    = refl
x+0 (suc a) rewrite x+0 a = refl

-- Agda knows that 0 * a == 0, now we are telling that "a * 0 == 0 * a"
a*0 : (a : Nat) -> (a * 0) == 0
a*0 zero    = refl
a*0 (suc a) rewrite (a*0 a) = refl -- does that 0 * a == 0

-- Proof that 1 is identity element of multiply over nats. Proof by beala
a*1 : (a : Nat) -> (a * 1) == a
a*1 zero    = refl
a*1 (suc a) rewrite a*1 a | a*0 a | x+0 a = refl

-- Tells Agda that 1 * a == a
1*a : (a : Nat) -> (1 * a) == a
1*a zero    = refl
1*a (suc a) rewrite 1*a a = refl

--------- Calculator ---------
-- Initial state
init : State
init = (state add 0 0)

-- Calculates the operation related to a state
result : State -> Nat
result (state add a b) = (a + b)
result (state sub a b) = (a - b)
result (state mul a b) = (a * b)

-- Get the current State, an Event and update to a new State
updateState : State -> Event -> State
-- clear
updateState s               clr          = init
-- "num operation": update the numbers values
updateState (state op m n) (num right x) = (state op m x)
updateState (state op m n) (num left x)  = (state op x n)
-- execute an operation
updateState (state op m n) (ope e) = (state e m n)

--------- Testing Calculator ---------
testUpState0 : State -- add a number on the left
testUpState0 = (updateState init (num left 1))

testUpState1 : State -- add a number on the right
testUpState1 = (updateState testUpState0 (num right 1))

testUpState2 : State -- executes an operation on both numbers
testUpState2 = (updateState testUpState1 (ope add))

-- A type of test as is usually done in other programming languages. Given some input what do I expect as result?
testUpStateResult : (result (updateState testUpState1 (ope add))) == 2
testUpStateResult = refl

testUpState0a : State -- add a number on the left
testUpState0a = (updateState init (num left 3))

testUpState1a : State -- add a number on the right
testUpState1a = (updateState testUpState0a (num right 5))

testUpState2a : State -- executes an operation on both numbers
testUpState2a = (updateState testUpState1a (ope mul))

testUpState0b : State
testUpState0b = (updateState testUpState2a (clr))

--------- Theorems ---------
-- Proofs that the result showing up an operation will always do that operation --
theorem-0 : (s : State) -> (a b : Nat) -> (result (state add a b)) == (a + b)
theorem-0 s a b = refl

theorem-1 : (s : State) -> (a b : Nat) -> (result (state sub a b)) == (a - b)
theorem-1 s a b = refl

theorem-2 : (s : State) -> (a b : Nat) -> (result (state mul a b)) == (a * b)
theorem-2 s a b = refl

-- Given a and b and a proof that one of them is 0, then the result of multiplicating a and b must be 0
theorem-3 : ∀ (a b : Nat) -> Either (a == 0) (b == 0) -> (a * b) == 0
theorem-3 .0 b (fst refl) = refl -- Agda knows that 0 * n == 0 (refl)
theorem-3 a .0 (snd refl) = (a*0 a) -- then we proof that n * 0 is also 0

-- if a == 1: (mul a b) == b
-- if b == 1: (mul a b) == a
-- if a == 1 OR b == 1: Either ((mul a b) == b) ((mul a b) == a)
-- Given a and b and a proof that one of them is 1,
-- then the result of multiplicating a and b must be the number that is not 1
theorem-4 : ∀ (a b : Nat) -> Either (a == 1) (b == 1) -> Either ((a * b) == b) ((a * b) == a)
theorem-4 .1 b (fst refl) = fst (1*a b) -- A proof that 1 * b == b
theorem-4 a .1 (snd refl) = snd (a*1 a) -- A proof that b * 1 == b

-- Proof that update state works as expected
update-theorem : ∀ (x y : Nat) → (s : State) → (result (updateState (updateState (updateState s (num left x)) (ope add)) (num right y))) == (x + y)
update-theorem x y (state op m n) = refl

-- TODO --
-- -- Evaluates several expressions. E.g. (2 + 3) * 5
-- data Expression : Set where
--   num : Nat -> Expression
--   add : Expression -> Expression -> Expression
--   sub : Expression -> Expression -> Expression

----- VIEW? -----
-- main : Program
-- main _ = do
--
--   print "-- Calculator --"
--   -- Receives a number, an operation symbol and a execution command
--
--   let result = exe-operation 2 3 add
--   print (show result)

  -- let result2 = (primNatToChar (exe-operation 2 3 add))
  -- print (primShowChar result2)

  -- for i from 0 to 10 do:
  --   print ("i: " ++ show i)
  --
  -- if (2 == 2)
  --   (then: print "foo")
  --   (else: print "bar")
  --
  -- let num =
  --       init 0.0
  --       for i from 0 to 1000000 do:
  --         λ result → result f+ 1.0

  -- print (primShowFloat num)

max_stars_repo_name: MaisaMilena/AgdaCalculator

max_issues_repo_name: MaisaMilena/AgdaCalculator

max_forks_repo_name: MaisaMilena/AgdaCalculator


text:
open import level
open import bool
open import bool-thms
open import eq
open import eq-reasoning
open import sum
open import nat

data Lgc : Set where
  ttrue : Lgc
  ffalse : Lgc
  aand : Lgc → Lgc → Lgc
  oor : Lgc → Lgc → Lgc
  nnot : Lgc → Lgc

check_ : Lgc → 𝔹
check ttrue        = tt
check ffalse       = ff
check (aand c1 c2) = (check c1) && (check c2)
check (oor c1 c2)  = (check c1) || (check c2)
check (nnot c)     = ~(check c)

data _isTrue : Lgc → Set
data _isFalse : Lgc → Set

data _isTrue where

  c-tt :
          -----------
          ttrue isTrue

  c-and : ∀ {c1 c2 : Lgc}
          → c1 isTrue
          → c2 isTrue
          -----------------
          → (aand c1 c2) isTrue

  c-or₁ : ∀ {c1 c2 : Lgc}
          → c1 isTrue
          ---------------
          → (oor c1 c2) isTrue

  c-or₂ : ∀ {c1 c2 : Lgc}
          → c2 isTrue
          ----------------
          → (oor c1 c2) isTrue

  c-not : ∀ {c : Lgc}
          → c isFalse
          -------------
          → (nnot c) isTrue

data _isFalse where

  ~c-ff :
    --------------
    ffalse isFalse

  ~c-or : ∀ {c1 c2 : Lgc}
    → c1 isFalse
    → c2 isFalse
    ---------------------
    → (oor c1 c2) isFalse

  ~c-and₁ : ∀ {c1 c2 : Lgc}
    → c1 isFalse
    ----------------------
    → (aand c1 c2) isFalse

  ~c-and₂ : ∀ {c1 c2 : Lgc}
    → c2 isFalse
    -----------------
    → (aand c1 c2) isFalse

  ~c-not : ∀ {c : Lgc}
    → c isTrue
    -------------
    → (nnot c) isFalse

c-thm :  ∀ {c : Lgc} → c isTrue  → (check c ≡ tt)
~c-thm : ∀ {c : Lgc} → c isFalse → (check c ≡ ff)

c-thm (c-tt) =
  begin
    check ttrue
  ≡⟨ refl ⟩
    tt
  ∎
c-thm (c-and{c1}{c2} dat1 dat2) =
  begin
    check (aand c1 c2)
  ≡⟨ refl ⟩
    (check c1) && (check c2)
  ≡⟨ congf2{f = _&&_}{f' = _&&_} refl (c-thm dat1) (c-thm dat2) ⟩
    tt && tt
  ≡⟨ refl ⟩
    tt
  ∎
c-thm (c-or₁{c1}{c2} dat1) =
  begin
    check (oor c1 c2)
  ≡⟨ refl ⟩
    (check c1) || (check c2)
  ≡⟨ congf2{f = _||_}{f' = _||_} refl (c-thm dat1) refl ⟩
    tt || (check c2)
  ≡⟨ refl ⟩
    tt
  ∎
c-thm (c-or₂{c1}{c2} dat2) =
  begin
    check (oor c1 c2)
  ≡⟨ refl ⟩
    (check c1) || (check c2)
  ≡⟨ congf2{f = _||_}{f' = _||_} refl refl (c-thm dat2) ⟩
    (check c1) || tt
  ≡⟨ ||-tt (check c1)⟩
    tt
  ∎
c-thm (c-not{c} dat) =
  begin
    check (nnot c)
  ≡⟨ refl ⟩
    ~ (check c)
  ≡⟨ congf{f = ~_}{f' = ~_} refl (~c-thm dat) ⟩
    ~ ff
  ≡⟨ refl ⟩
    tt
  ∎

~c-thm (~c-ff) =
  begin
    check ffalse
  ≡⟨ refl ⟩
    ff
  ∎
~c-thm (~c-or{c1}{c2} dat1 dat2) =
  begin
    check (oor c1 c2)
  ≡⟨ refl ⟩
    (check c1) || (check c2)
  ≡⟨ congf2{f = _||_}{f' = _||_} refl (~c-thm dat1) (~c-thm dat2) ⟩
    ff || ff
  ≡⟨ refl ⟩
    ff
  ∎
~c-thm (~c-and₁{c1}{c2} dat1) =
  begin
    check (aand c1 c2)
  ≡⟨ refl ⟩
    (check c1) && (check c2)
  ≡⟨ congf2{f = _&&_}{f' = _&&_} refl (~c-thm dat1) refl ⟩
    ff && (check c2)
  ≡⟨ refl ⟩
    ff
  ∎
~c-thm (~c-and₂{c1}{c2} dat2) =
  begin
    check (aand c1 c2)
  ≡⟨ refl ⟩
    (check c1) && (check c2)
  ≡⟨ congf2{f = _&&_}{f' = _&&_} refl refl (~c-thm dat2) ⟩
    (check c1) && ff
  ≡⟨ &&-ff (check c1)⟩
    ff
  ∎

~c-thm (~c-not{c} dat) =
  begin
    check (nnot c)
  ≡⟨ refl ⟩
    ~ (check c)
  ≡⟨ congf{f = ~_}{f' = ~_} refl (c-thm dat) ⟩
    ~ tt
  ≡⟨ refl ⟩
    ff
  ∎

max_stars_repo_name: JimFixGroupResearch/imper-ial

max_issues_repo_name: JimFixGroupResearch/imper-ial

max_forks_repo_name: JimFixGroupResearch/imper-ial