text:
module Category.Profunctor where
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Data.Product using (_,_; _×_)
open import Function using (id)
open import Relation.Binary.PropositionalEquality using (_≡_)

Dimap : ∀ {a b} (p : Set a → Set a → Set b) → Set (lsuc a ⊔ b)
Lmap : ∀ {a b} (p : Set a → Set a → Set b) → Set (lsuc a ⊔ b)
Rmap : ∀ {a b} (p : Set a → Set a → Set b) → Set (lsuc a ⊔ b)

Dimap p = ∀ {x y z w} → (f : x -> y) -> (h : z -> w) -> (g : p y z) → p x w
Lmap  p = ∀ {x y   w} → (f : x -> y) ->                 (g : p y w) → p x w
Rmap  p = ∀ {x z   w} →                 (h : z -> w) -> (g : p x z) → p x w

record ProfunctorImp {a b : Level} (p : Set a → Set a → Set b) : Set (lsuc (a ⊔ b)) where
  field
    dimap : Dimap p
    lmap  : Lmap  p
    rmap  : Rmap  p

dimapFromLmapRmap : ∀ {a b} {p : Set a → Set a → Set b} (lmap : Lmap p) (rmap : Rmap p) → Dimap p
dimapFromLmapRmap lmap rmap f h g = rmap h (lmap f g)

lmapRmapFromDimap : ∀ {a b} {p : Set a → Set a → Set b} (dimap : Dimap p) → (Lmap p × Rmap p)
lmapRmapFromDimap dimap = (λ f → dimap f id) , dimap id

module Profunctor {a b : Level} {p : Set a → Set a → Set b} (isProfunctor : ProfunctorImp p) where
  open ProfunctorImp isProfunctor public

record LawfulProfunctorImp {a b} {p : Set a → Set a → Set b} (isProfunctor : ProfunctorImp p) : Set (lsuc (a ⊔ b)) where
  open Profunctor isProfunctor
  field
    lmapId : ∀ {a b} {g : p a b} → lmap id g ≡ g
    rmapId : ∀ {a b} {g : p a b} → rmap id g ≡ g
    dimapLmapRmap : ∀ {a b c d} {f : a → b} {g : p b c} {h : c → d} → dimap f h g ≡ lmap f (rmap h g)

module LawfulProfunctor {a b} {p : Set a → Set a → Set b} {isProfunctor : ProfunctorImp p} (isLawful : LawfulProfunctorImp isProfunctor) where
  open Profunctor isProfunctor public
  open LawfulProfunctorImp isLawful public

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
module Cats.Category.Op where

open import Relation.Binary using (Rel ; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality as ≡
open import Level

open import Cats.Category
open import Cats.Category.Cat using (Cat)

module _  {lo la l≈} (C : Category lo la l≈) where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module C = Category C
    module ≈ = C.≈

  Obj : Set lo
  Obj = C.Obj

  _⇒_ : Obj → Obj → Set la
  A ⇒ B = B C.⇒ A

  id : ∀ {A} → A ⇒ A
  id = C.id

  _∘_ : ∀ {A B C : Obj} → (B ⇒ C) → (A ⇒ B) → A ⇒ C
  f ∘ g = g C.∘ f

  _≈_ : ∀ {A B} → Rel (A ⇒ B) l≈
  _≈_ = C._≈_

  ∘-resp : ∀ {A B C} → _∘_ {A} {B} {C} Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
  ∘-resp {x = f} {g} {h} {i} f≈g h≈i = C.∘-resp h≈i f≈g

  assoc : ∀ {A B C D} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
    → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
  assoc = C.unassoc

  _ᵒᵖ : Category lo la l≈
  _ᵒᵖ = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = λ f g → g C.∘ f
      ; equiv = C.equiv
      ; ∘-resp = ∘-resp
      ; id-r = C.id-l
      ; id-l = C.id-r
      ; assoc = assoc
      }

module _ {lo la l≈ : Level} where

  private module Cat = Category (Cat lo la l≈)

  op-involution : {C : Category lo la l≈} → ((C ᵒᵖ) ᵒᵖ) Cat.≅ C
  op-involution {C} = record
      { forth = record
          { fobj = λ x → x
          ; fmap = λ f → f
          ; fmap-resp = λ eq → eq
          ; fmap-id = C.≈.reflexive ≡.refl
          ; fmap-∘ = C.≈.reflexive ≡.refl
          }
      ; back = record
          { fobj = λ x → x
          ; fmap = λ f → f
          ; fmap-resp = λ eq → eq
          ; fmap-id = C.≈.reflexive ≡.refl
          ; fmap-∘ = C.≈.reflexive ≡.refl
          }
      -- TODO This sort of natural iso comes up all the time. Can we abstract it
      -- out?
      ; back-forth = record
          { iso = Coo.≅.refl
          ; forth-natural = C.≈.trans C.id-l (C.≈.sym C.id-r)
          }
      ; forth-back = record
          { iso = C.≅.refl
          ; forth-natural = C.≈.trans C.id-l (C.≈.sym C.id-r)
          }
      }
    where
      module C = Category C
      module Coo = Category ((C ᵒᵖ)ᵒᵖ)
      module ≈ = C.≈

ext: agda

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module AgdalightTelescopeSyntax where

postulate
  A : Set
  B : A -> Set
  g : (x y : A; z : B x) -> A
-- this is Agdalight syntax, should not parse

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Graph.Examples where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Empty
open import Cubical.Data.Unit renaming (Unit to ⊤)
open import Cubical.Data.Nat
open import Cubical.Data.SumFin
open import Cubical.Relation.Nullary

open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Data.Graph.Base

-- Some small graphs of common shape

⇒⇐ : Graph ℓ-zero ℓ-zero
Node ⇒⇐ = Fin 3
Edge ⇒⇐ fzero               (fsuc fzero) = ⊤
Edge ⇒⇐ (fsuc (fsuc fzero)) (fsuc fzero) = ⊤
Edge ⇒⇐ _ _ = ⊥

⇐⇒ : Graph ℓ-zero ℓ-zero
Node ⇐⇒ = Fin 3
Edge ⇐⇒ (fsuc fzero) fzero               = ⊤
Edge ⇐⇒ (fsuc fzero) (fsuc (fsuc fzero)) = ⊤
Edge ⇐⇒ _ _ = ⊥

-- paralell pair graph
⇉ : Graph ℓ-zero ℓ-zero
Node ⇉ = Fin 2
Edge ⇉ fzero (fsuc fzero) = Fin 2
Edge ⇉ _ _ = ⊥

-- The graph ω = 0 → 1 → 2 → ···

data Adj : ℕ → ℕ → Type₀ where
  adj : ∀ n → Adj n (suc n)

areAdj : ∀ m n → Dec (Adj m n)
areAdj zero zero          = no λ ()
areAdj zero (suc zero)    = yes (adj zero)
areAdj zero (suc (suc n)) = no λ ()
areAdj (suc m) zero       = no λ ()
areAdj (suc m) (suc n)    = mapDec (λ { (adj .m) → adj (suc m) })
                                   (λ { ¬a (adj .(suc m)) → ¬a (adj m) })
                                   (areAdj m n)

ωGr : Graph ℓ-zero ℓ-zero
Node ωGr = ℕ
Edge ωGr m n with areAdj m n
... | yes _ = ⊤ -- if n ≡ (suc m)
... | no  _ = ⊥ -- otherwise

record ωDiag ℓ : Type (ℓ-suc ℓ) where
  field
    ωNode : ℕ → Type ℓ
    ωEdge : ∀ n → ωNode n → ωNode (suc n)

  asDiag : Diag ℓ ωGr
  asDiag $ n = ωNode n
  _<$>_ asDiag {m} {n} f with areAdj m n
  asDiag <$> tt | yes (adj m) = ωEdge m

-- The finite connected subgraphs of ω: 𝟘,𝟙,𝟚,𝟛,...

data AdjFin : ∀ {k} → Fin k → Fin k → Type₀ where
  adj : ∀ {k} (n : Fin k) → AdjFin (finj n) (fsuc n)

adj-fsuc : ∀ {k} {m n : Fin k} → AdjFin (fsuc m) (fsuc n) → AdjFin m n
adj-fsuc {suc k} {.(finj n)} {fsuc n} (adj .(fsuc n)) = adj n

areAdjFin : ∀ {k} (m n : Fin k) → Dec (AdjFin m n)
areAdjFin {suc k}       fzero fzero           = no λ ()
areAdjFin {suc (suc k)} fzero (fsuc fzero)    = yes (adj fzero)
areAdjFin {suc (suc k)} fzero (fsuc (fsuc n)) = no λ ()
areAdjFin {suc k}       (fsuc m) fzero        = no λ ()
areAdjFin {suc k}       (fsuc m) (fsuc n)     = mapDec (λ { (adj m) → adj (fsuc m) })
                                                       (λ { ¬a a → ¬a (adj-fsuc a) })
                                                       (areAdjFin {k} m n)

[_]Gr : ℕ → Graph ℓ-zero ℓ-zero
Node [ k ]Gr = Fin k
Edge [ k ]Gr m n with areAdjFin m n
... | yes _ = ⊤ -- if n ≡ (suc m)
... | no  _ = ⊥ -- otherwise

𝟘Gr 𝟙Gr 𝟚Gr 𝟛Gr : Graph ℓ-zero ℓ-zero
𝟘Gr = [ 0 ]Gr; 𝟙Gr = [ 1 ]Gr; 𝟚Gr = [ 2 ]Gr; 𝟛Gr = [ 3 ]Gr

record [_]Diag ℓ (k : ℕ) : Type (ℓ-suc ℓ) where
  field
    []Node : Fin (suc k) → Type ℓ
    []Edge : ∀ (n : Fin k) → []Node (finj n) → []Node (fsuc n)

  asDiag : Diag ℓ [ suc k ]Gr
  asDiag $ n = []Node n
  _<$>_ asDiag {m} {n} f with areAdjFin m n
  _<$>_ asDiag {.(finj n)} {fsuc n} f | yes (adj .n) = []Edge n

-- Disjoint union of graphs

module _ {ℓv ℓe ℓv' ℓe'} where

  _⊎Gr_ : ∀ (G : Graph ℓv ℓe) (G' : Graph ℓv' ℓe') → Graph (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe')
  Node (G ⊎Gr G') = Node G ⊎ Node G'
  Edge (G ⊎Gr G') (inl x) (inl y) = Lift {j = ℓe'} (Edge G x y)
  Edge (G ⊎Gr G') (inr x) (inr y) = Lift {j = ℓe } (Edge G' x y)
  Edge (G ⊎Gr G') _ _ = Lift ⊥

  record ⊎Diag ℓ (G : Graph ℓv ℓe) (G' : Graph ℓv' ℓe')
               : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe'))) where
    field
      ⊎Node : Node G ⊎ Node G' → Type ℓ
      ⊎Edgel : ∀ {x y} → Edge G  x y → ⊎Node (inl x) → ⊎Node (inl y)
      ⊎Edger : ∀ {x y} → Edge G' x y → ⊎Node (inr x) → ⊎Node (inr y)

    asDiag : Diag ℓ (G ⊎Gr G')
    asDiag $ x = ⊎Node x
    _<$>_ asDiag {inl x} {inl y} f = ⊎Edgel (lower f)
    _<$>_ asDiag {inr x} {inr y} f = ⊎Edger (lower f)

-- Cartesian product of graphs

module _ {ℓv ℓe ℓv' ℓe'} where

  -- We need decidable equality in order to define the cartesian product
  DecGraph : ∀ ℓv ℓe → Type (ℓ-suc (ℓ-max ℓv ℓe))
  DecGraph ℓv ℓe = Σ[ G ∈ Graph ℓv ℓe ] Discrete (Node G)

  _×Gr_ : (G : DecGraph ℓv ℓe) (G' : DecGraph ℓv' ℓe') → Graph (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe')
  Node (G ×Gr G') = Node (fst G) × Node (fst G')
  Edge (G ×Gr G') (x , x') (y , y') with snd G x y | snd G' x' y'
  ... | yes _ | yes _ = Edge (fst G) x y ⊎ Edge (fst G') x' y'
  ... | yes _ | no  _ = Lift {j = ℓe } (Edge (fst G') x' y')
  ... | no  _ | yes _ = Lift {j = ℓe'} (Edge (fst G) x y)
  ... | no  _ | no  _ = Lift ⊥

  record ×Diag ℓ (G : DecGraph ℓv ℓe) (G' : DecGraph ℓv' ℓe')
               : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe'))) where
    field
      ×Node : Node (fst G) × Node (fst G') → Type ℓ
      ×Edge₁ : ∀ {x y} (f : Edge (fst G) x y) (x' : Node (fst G'))    → ×Node (x , x') → ×Node (y , x')
      ×Edge₂ : ∀ (x : Node (fst G)) {x' y'} (f : Edge (fst G') x' y') → ×Node (x , x') → ×Node (x , y')

    asDiag : Diag ℓ (G ×Gr G')
    asDiag $ x = ×Node x
    _<$>_ asDiag {x , x'} {y , y'} f with snd G x y | snd G' x' y'
    _<$>_ asDiag {x , x'} {y , y'} (inl f) | yes _ | yes p' = subst _ p' (×Edge₁ f x')
    _<$>_ asDiag {x , x'} {y , y'} (inr f) | yes p | yes _  = subst _ p  (×Edge₂ x f )
    _<$>_ asDiag {x , x'} {y , y'} f | yes p | no  _  = subst _ p  (×Edge₂ x (lower f) )
    _<$>_ asDiag {x , x'} {y , y'} f | no  _ | yes p' = subst _ p' (×Edge₁ (lower f) x')

max_stars_repo_name: FernandoLarrain/cubical


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

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

module Fields.CauchyCompletion.Multiplication {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F
open import Fields.Orders.Lemmas {F = F} record { oRing = order }
open import Fields.Orders.Total.Lemmas {F = F} record { oRing = order }

open import Fields.Lemmas F
open import Rings.Orders.Partial.Lemmas pRing
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.Cauchy order
open import Rings.Orders.Total.AbsoluteValue order
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Setoid order F
open import Fields.CauchyCompletion.Approximation order F

0!=1 : {e : A} → (0G < e) → 0R ∼ 1R → False
0!=1 {e} 0<e 0=1 = irreflexive (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<e)

private
  littleLemma : {a b c d : A} → ((a * b) + inverse (c * d)) ∼ ((a * (b + inverse d)) + (d * (a + inverse c)))
  littleLemma {a} {b} {c} {d} = Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq identLeft) (+WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq (ringMinusExtracts R) (inverseWellDefined additiveGroup *Commutative)) (Equivalence.reflexive eq)) (invLeft {d * a}))) (Equivalence.transitive eq (Equivalence.symmetric eq (ringMinusExtracts' R)) *Commutative))) (Equivalence.symmetric eq +Associative))) (+Associative)) (Equivalence.symmetric eq (+WellDefined (*DistributesOver+) (*DistributesOver+)))

  timesConverges : (a b : CauchyCompletion) → cauchy (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b))
  timesConverges record { elts = a ; converges = aConv } record { elts = b ; converges = bConv } e 0<e with boundModulus record { elts = a ; converges = aConv }
  ... | aBound , (Na , prABound) with boundModulus record { elts = b ; converges = bConv }
  ... | bBound , (Nb , prBBound) = N , ans
    where
      boundBoth : A
      boundBoth = aBound + bBound
      abstract
        ab<bb : aBound < boundBoth
        ab<bb = <WellDefined identLeft groupIsAbelian (orderRespectsAddition {0R} {bBound} (greaterThanAbsImpliesGreaterThan0 (prBBound (succ Nb) (le 0 refl))) aBound)
        bb<bb : bBound < boundBoth
        bb<bb = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition {0R} {aBound} (greaterThanAbsImpliesGreaterThan0 (prABound (succ Na) (le 0 refl))) bBound)
        0<boundBoth : 0R < boundBoth
        0<boundBoth = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (greaterThanAbsImpliesGreaterThan0 (prABound (succ Na) (le 0 refl))) (greaterThanAbsImpliesGreaterThan0 (prBBound (succ Nb) (le 0 refl))))
      abstract
        1/boundBoothAndPr : Sg A λ i → i * (aBound + bBound) ∼ 1R
        1/boundBoothAndPr = allInvertible boundBoth λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<boundBoth)
        1/boundBooth : A
        1/boundBooth with 1/boundBoothAndPr
        ... | a , _ = a
        1/boundBoothPr : 1/boundBooth * (aBound + bBound) ∼ 1R
        1/boundBoothPr with 1/boundBoothAndPr
        ... | _ , pr = pr
        0<1/boundBooth : 0G < 1/boundBooth
        0<1/boundBooth = inversePositiveIsPositive 1/boundBoothPr 0<boundBoth
      abstract
        miniEAndPr : Sg A (λ i → (i + i) ∼ (e * 1/boundBooth))
        miniEAndPr = halve charNot2 (e * 1/boundBooth)
        miniE : A
        miniE with miniEAndPr
        ... | a , _ = a
        miniEPr : (miniE + miniE) ∼ (e * 1/boundBooth)
        miniEPr with miniEAndPr
        ... | _ , pr = pr
        0<miniE : 0R < miniE
        0<miniE = halvePositive miniE (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq miniEPr) (orderRespectsMultiplication 0<e 0<1/boundBooth))
      abstract
        reallyNAAndPr : Sg ℕ (λ N → {m n : ℕ} → N <N m → N <N n → abs (index a m + inverse (index a n)) < miniE)
        reallyNAAndPr = aConv miniE 0<miniE
        reallyNa : ℕ
        reallyNa with reallyNAAndPr
        ... | a , _ = a
        reallyNaPr : {m n : ℕ} → reallyNa <N m → reallyNa <N n → abs (index a m + inverse (index a n)) < miniE
        reallyNaPr with reallyNAAndPr
        ... | _ , pr = pr
        reallyNBAndPr : Sg ℕ (λ N → {m n : ℕ} → N <N m → N <N n → abs (index b m + inverse (index b n)) < miniE)
        reallyNBAndPr = bConv miniE 0<miniE
        reallyNb : ℕ
        reallyNb with reallyNBAndPr
        ... | a , _ = a
        reallyNbPr : {m n : ℕ} → reallyNb <N m → reallyNb <N n → abs (index b m + inverse (index b n)) < miniE
        reallyNbPr with reallyNBAndPr
        ... | _ , pr = pr
      N : ℕ
      N = (Na +N (Nb +N (reallyNa +N reallyNb)))
      ans : {m : ℕ} {n : ℕ} → N <N m → N <N n → abs (index (apply _*_ a b) m + inverse (index (apply _*_ a b) n)) < e
      ans {m} {n} N<m N<n rewrite indexAndApply a b _*_ {m} | indexAndApply a b _*_ {n} = ans'''
        where
          Na<m : Na <N m
          Na<m = inequalityShrinkLeft N<m
          Nb<n : Nb <N n
          Nb<n = inequalityShrinkLeft (inequalityShrinkRight {Na} N<n)
          abstract
            sum : {m n : ℕ} → (reallyNa +N reallyNb) <N m → (reallyNa +N reallyNb) <N n → (boundBoth * ((abs (index b m + inverse (index b n))) + (abs (index a m + inverse (index a n))))) < e
            sum {m} {n} <m <n = <WellDefined *Commutative (Equivalence.transitive eq (*WellDefined miniEPr (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) 1/boundBoothPr) *Commutative) (identIsIdent)))) (ringCanMultiplyByPositive {c = boundBoth} 0<boundBoth (ringAddInequalities (reallyNbPr {m} {n} (inequalityShrinkRight <m) (inequalityShrinkRight <n)) (reallyNaPr {m} {n} (inequalityShrinkLeft <m) (inequalityShrinkLeft <n))))
          q : ((boundBoth * (abs (index b m + inverse (index b n)))) + (boundBoth * (abs (index a m + inverse (index a n))))) < e
          q = <WellDefined *DistributesOver+ (Equivalence.reflexive eq) (sum {m} {n} (inequalityShrinkRight {Nb} (inequalityShrinkRight {Na} N<m)) (inequalityShrinkRight {Nb} (inequalityShrinkRight {Na} N<n)))
          p : ((abs (index a m) * abs (index b m + inverse (index b n))) + (abs (index b n) * abs (index a m + inverse (index a n)))) < e
          p with totality 0R (index b m + inverse (index b n))
          p | inl (inl 0<bm-bn) with totality 0R (index a m + inverse (index a n))
          p | inl (inl 0<bm-bn) | inl (inl 0<am-an) = SetoidPartialOrder.<Transitive pOrder (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn)) (ringCanMultiplyByPositive 0<bm-bn (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) ab<bb))) (<WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<am-an)) (ringCanMultiplyByPositive 0<am-an (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb)))) q
          p | inl (inl 0<bm-bn) | inl (inr am-an<0) = SetoidPartialOrder.<Transitive pOrder (ringAddInequalities (<WellDefined (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (greaterZeroImpliesEqualAbs 0<bm-bn))) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn) 0<bm-bn) (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) ab<bb))) (<WellDefined (*WellDefined (Equivalence.reflexive eq) (lessZeroImpliesEqualNegAbs am-an<0)) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lessZeroImpliesEqualNegAbs am-an<0)) (lemm2 _ am-an<0)) (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb)))) q
          p | inl (inl 0<bm-bn) | inr 0=am-an = <WellDefined (+WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) 0=am-an)) (Equivalence.reflexive eq) (<WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq timesZero)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq identRight) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq absZeroIsZero) (absWellDefined _ _ 0=am-an)))) (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq timesZero)) (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq identRight) (<WellDefined (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (greaterZeroImpliesEqualAbs 0<bm-bn))) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (greaterZeroImpliesEqualAbs 0<bm-bn) 0<bm-bn) (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) ab<bb)))))) q)))
          p | inl (inr bm-bn<0) = SetoidPartialOrder.<Transitive pOrder ans'' q
            where
              bar : ((abs (index a m)) * (inverse (index b m + inverse (index b n)))) < (boundBoth * abs (index b m + inverse (index b n)))
              bar = <WellDefined (*WellDefined (Equivalence.reflexive eq) (lessZeroImpliesEqualNegAbs bm-bn<0)) (Equivalence.reflexive eq) (ringCanMultiplyByPositive (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lessZeroImpliesEqualNegAbs bm-bn<0)) (lemm2 _ bm-bn<0)) (SetoidPartialOrder.<Transitive pOrder (prABound m Na<m) (ab<bb)))
              foo : (((abs (index b n)) * (abs (index a m + inverse (index a n)))) < (boundBoth * abs (index a m + inverse (index a n)))) || (((abs (index b n)) * (abs (index a m + inverse (index a n)))) ∼ (boundBoth * abs (index a m + inverse (index a n))))
              foo with totality 0R (index a m + inverse (index a n))
              foo | inl (inl 0<am-an) = inl (ringCanMultiplyByPositive 0<am-an (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb))
              foo | inl (inr am-an<0) = inl (ringCanMultiplyByPositive (lemm2 _ am-an<0) (SetoidPartialOrder.<Transitive pOrder (prBBound n Nb<n) bb<bb))
              foo | inr 0=am-an = inr (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=am-an)) (Equivalence.transitive eq (Equivalence.transitive eq timesZero (Equivalence.symmetric eq timesZero)) (*WellDefined (Equivalence.reflexive eq) 0=am-an)))
              ans'' : _
              ans'' with foo
              ... | inl pr = ringAddInequalities bar pr
              ... | inr pr = <WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) pr) (orderRespectsAddition bar ((abs (index b n)) * (abs (index a m + inverse (index a n)))))
          p | inr 0=bm-bn = ans''
            where
              bar : (boundBoth * abs (index b m + inverse (index b n))) ∼ 0R
              bar = Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.symmetric eq 0=bm-bn)) (absZeroIsZero))) timesZero
              bar' : (abs (index a m) * (index b m + inverse (index b n))) ∼ 0R
              bar' = Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=bm-bn)) timesZero
              foo : (((abs (index b n)) * (abs (index a m + inverse (index a n)))) < (boundBoth * abs (index a m + inverse (index a n)))) || (0R ∼ (index a m + inverse (index a n)))
              foo with totality 0R (index a m + inverse (index a n))
              foo | inl (inl 0<am-an) = inl (SetoidPartialOrder.<Transitive pOrder (ringCanMultiplyByPositive 0<am-an (prBBound n Nb<n)) (ringCanMultiplyByPositive 0<am-an bb<bb))
              foo | inl (inr am-an<0) = inl (SetoidPartialOrder.<Transitive pOrder (ringCanMultiplyByPositive (lemm2 _ am-an<0) (prBBound n Nb<n)) (ringCanMultiplyByPositive (lemm2 _ am-an<0) bb<bb))
              foo | inr 0=am-an = inr 0=am-an
              ans'' : _
              ans'' with foo
              ... | inl pr = SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (<WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bar')) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bar)) (orderRespectsAddition pr 0R))) q
              ... | inr pr = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.symmetric eq bar') (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.symmetric eq pr)) absZeroIsZero)) timesZero)))) (Equivalence.reflexive eq) 0<e
          ans''' : abs ((index a m * index b m) + inverse (index a n * index b n)) < e
          ans''' with triangleInequality (index a m * (index b m + inverse (index b n))) (index b n * (index a m + inverse (index a n)))
          ... | inl less = <WellDefined (Equivalence.symmetric eq (absWellDefined ((index a m * index b m) + (inverse (index a n * index b n))) (((index a m) * (index b m + (inverse (index b n)))) + ((index b n) * (index a m + inverse (index a n)))) littleLemma)) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder less (<WellDefined (+WellDefined (Equivalence.symmetric eq (absRespectsTimes (index a m) _)) (Equivalence.symmetric eq (absRespectsTimes (index b n) _))) (Equivalence.reflexive eq) p))
          ... | inr equal = <WellDefined {_ + _} {abs _} {e} {e} (symmetric (transitive (transitive (absWellDefined ((index a m * index b m) + (inverse (index a n * index b n))) (((index a m) * (index b m + (inverse (index b n)))) + ((index b n) * (index a m + inverse (index a n)))) littleLemma) equal) (+WellDefined (absRespectsTimes (index a m) _) (absRespectsTimes (index b n) _)))) reflexive p

_*C_ : CauchyCompletion → CauchyCompletion → CauchyCompletion
CauchyCompletion.elts (record { elts = a ; converges = aConv } *C record { elts = b ; converges = bConv }) = apply _*_ a b
CauchyCompletion.converges (a *C b) = timesConverges a b

*CCommutative : {a b : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a *C b) (b *C a)
*CCommutative {a} {b} ε 0<e = 0 , ans
  where
    foo : {x y : A} → (x * y) + inverse (y * x) ∼ 0G
    foo = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (inverseWellDefined additiveGroup *Commutative)) invRight
    ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (a *C b)) (map inverse (CauchyCompletion.elts (b *C a)))) m) < ε
    ans {m} 0<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts a))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts a)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts a) _*_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ foo) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

private

  multiplicationWellDefinedLeft' : (0!=1 : 0R ∼ 1R → False) (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
  multiplicationWellDefinedLeft' 0!=1 a b c a=b ε 0<e = N , ans
    where
      abstract
        cBoundAndPr : Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts c) m)) < b))
        cBoundAndPr = boundModulus c
        cBound : A
        cBound with cBoundAndPr
        ... | a , _ = a
        cBoundN : ℕ
        cBoundN with cBoundAndPr
        ... | _ , (N , _) = N
        cBoundPr : (m : ℕ) → (cBoundN <N m) → (abs (index (CauchyCompletion.elts c) m)) < cBound
        cBoundPr with cBoundAndPr
        ... | _ , (_ , pr) = pr
      0<cBound : 0G < cBound
      0<cBound with totality 0G cBound
      0<cBound | inl (inl 0<cBound) = 0<cBound
      0<cBound | inl (inr cBound<0) = exFalso (absNonnegative (SetoidPartialOrder.<Transitive pOrder (cBoundPr (succ cBoundN) (le 0 refl)) cBound<0))
      0<cBound | inr 0=cBound = exFalso (absNonnegative (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=cBound) (cBoundPr (succ cBoundN) (le 0 refl))))
      e/c : A
      e/c with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
      ... | (1/c , _) = ε * 1/c
      e/cPr : e/c * cBound ∼ ε
      e/cPr with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
      ... | (1/c , pr) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (*WellDefined (Equivalence.reflexive eq) pr)) *Commutative) (identIsIdent)
      0<e/c : 0G < e/c
      0<e/c = ringCanCancelPositive {0G} {e/c} 0<cBound (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (Equivalence.symmetric eq e/cPr) 0<e)
      abBound : ℕ
      abBound with a=b e/c 0<e/c
      ... | Na=b , _ = Na=b
      abPr : {m : ℕ} → (abBound <N m) → abs (index (apply _+_ (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b))) m) < e/c
      abPr with a=b e/c 0<e/c
      ... | Na=b , pr = pr
      N : ℕ
      N = abBound +N cBoundN
      cBounded : (m : ℕ) → (N <N m) → abs (index (CauchyCompletion.elts c) m) < cBound
      cBounded m N<m = cBoundPr m (inequalityShrinkRight N<m)
      a-bSmall : (m : ℕ) → N <N m → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts b) m)) < e/c
      a-bSmall m N<m = <WellDefined (absWellDefined _ _ (transitive (identityOfIndiscernablesLeft _∼_ reflexive (equalityCommutative (indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m}))) (+WellDefined reflexive (identityOfIndiscernablesLeft _∼_ reflexive (mapAndIndex (CauchyCompletion.elts b) inverse m))))) reflexive (abPr {m} (inequalityShrinkLeft N<m))
      ans : {m : ℕ} → N <N m → abs (index (apply _+_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)))) m) < ε
      ans {m} N<m = <WellDefined (absWellDefined _ _ (transitive (+WellDefined (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply _ _ _*_ {m})) (transitive (transitive (ringMinusExtracts' R) (inverseWellDefined additiveGroup (identityOfIndiscernablesRight _∼_ reflexive (equalityCommutative (indexAndApply _ _ _*_ {m}))))) (identityOfIndiscernablesLeft _∼_ reflexive (equalityCommutative (mapAndIndex _ inverse m))))) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply _ _ _+_ {m})))) reflexive (<WellDefined (absWellDefined ((index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts b) m)) * index (CauchyCompletion.elts c) m) _ (Equivalence.transitive eq (Equivalence.transitive eq *Commutative *DistributesOver+) (+WellDefined *Commutative *Commutative))) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq (absRespectsTimes _ _)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.reflexive eq) e/cPr (ans' (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) (index (CauchyCompletion.elts c) m) (a-bSmall m N<m) (cBounded m N<m)))))
        where
          ans' : (a b c : A) → abs (a + inverse b) < e/c → abs c < cBound → (abs (a + inverse b) * abs c) < (e/c * cBound)
          ans' a b c a-b<e/c c<bound with totality 0R c
          ans' a b c a-b<e/c c<bound | inl (inl 0<c) with totality 0G (a + inverse b)
          ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b 0<c a-b<e/c c<bound
          ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) 0<c a-b<e/c c<bound
          ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
          ans' a b c a-b<e/c c<bound | inl (inr c<0) with totality 0G (a + inverse b)
          ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b (lemm2 c c<0) a-b<e/c c<bound
          ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) (lemm2 c c<0) a-b<e/c c<bound
          ans' a b c a-b<e/c c<bound | inl (inr c<0) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
          ans' a b c a-b<e/c c<bound | inr 0=c = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=c)) timesZero)) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)

  multiplicationWellDefinedLeft : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
  multiplicationWellDefinedLeft with totality 0R 1R
  ... | inl (inl 0<1') = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<1'))
  ... | inl (inr 1<0) = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.symmetric eq pr) (Equivalence.reflexive eq) 1<0))
  ... | inr (0=1) = λ a b c a=b → Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {injection 0G} {b *C c} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {injection 0G} {a *C c} (trivialIfInputTrivial 0=1 (a *C c))) (trivialIfInputTrivial 0=1 (b *C c))

  multiplicationPreservedLeft : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (injection a *C c) (injection b *C c)
  multiplicationPreservedLeft {a} {b} {c} a=b = multiplicationWellDefinedLeft (injection a) (injection b) c (injectionPreservesSetoid a b a=b)

  multiplicationPreservedRight : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (c *C injection a) (c *C injection b)
  multiplicationPreservedRight {a} {b} {c} a=b = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {c *C injection a} {injection a *C c} {c *C injection b} (*CCommutative {c} {injection a}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a *C c} {injection b *C c} {c *C injection b} (multiplicationPreservedLeft {a} {b} {c} a=b) (*CCommutative {injection b} {c}))

multiplicationPreserved : {a b c d : A} → (a ∼ b) → (c ∼ d) → Setoid._∼_ cauchyCompletionSetoid (injection a *C injection c) (injection b *C injection d)
multiplicationPreserved {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a *C injection c} {injection a *C injection d} {injection b *C injection d} (multiplicationPreservedRight {c} {d} {injection a} c=d) (multiplicationPreservedLeft {a} {b} {injection d} a=b)

private
  multiplicationWellDefinedRight : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid b c → Setoid._∼_ cauchyCompletionSetoid (a *C b) (a *C c)
  multiplicationWellDefinedRight a b c b=c = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C b} {b *C a} {a *C c} (*CCommutative {a} {b}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {b *C a} {c *C a} {a *C c} (multiplicationWellDefinedLeft b c a b=c) (*CCommutative {c} {a}))

multiplicationWellDefined : {a b c d : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid c d → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C d)
multiplicationWellDefined {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {a *C d} {b *C d} (multiplicationWellDefinedRight a c d c=d) (multiplicationWellDefinedLeft a b d a=b)


text:
open import Common.IO
open import Common.Unit
open import Common.String

-- Currently, it is not actually a test.
-- I need a wat to check that Erasure does not happen when it normally would.

{-# FOREIGN OCaml

type i =
  | Bar of string;;

#-}

data I : Set where
  bar : String → I

{-# COMPILE OCaml I No-Erasure #-}

showI : I → String
showI (bar x) = x

main : IO Unit
main = putStr (showI (bar "hello")) >>= λ _ → return unit

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
------------------------------------------------------------------------------
-- The LTC-PCF Booleans type
------------------------------------------------------------------------------

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

-- N.B. This module is re-exported by LTC-Bool.Data.Bool.

module LTC-PCF.Data.Bool.Type where

open import LTC-PCF.Base

------------------------------------------------------------------------------
-- The LTC-PCF Booleans type (inductive predicate for total Booleans).
data Bool : D → Set where
  btrue : Bool true
  bfalse : Bool false

-- The rule of proof by case analysis.
Bool-ind : (A : D → Set) → A true → A false → ∀ {b} → Bool b → A b
Bool-ind A At Af btrue  = At
Bool-ind A At Af bfalse = Af

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- An ATP conjecture cannot have duplicate local hints.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadLocalHint2 where

postulate
  D   : Set
  foo : D
  bar : D

{-# ATP prove foo bar bar #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
module tuple where

data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

_+_ : ℕ -> ℕ ->  ℕ
n + Z   = n
n + S m = S (n + m)

infixr 30 _+_

data Nil : Set where
  [] : Nil

infix 20 _::_

data Cons (A B : Set) : Set where
  _::_ : A -> B -> Cons A B

Tuple : Set -> ℕ -> Set
Tuple A Z     = Nil
Tuple A (S n) = Cons A (Tuple A n)

sumℕTuple : {n : ℕ} -> Tuple ℕ n -> Tuple ℕ n -> Tuple ℕ n
sumℕTuple {Z} []       []         = []
sumℕTuple {S n} (m :: l) (m' :: l')
            = m + m' :: (sumℕTuple l l')

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
-- Andreas, 2012-09-15
module InstanceArgumentsDontDiscardCandidateUponUnsolvedConstraints where

import Common.Level

data ⊥ : Set where
record ⊤ : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_≤_ : Nat → Nat → Set
zero    ≤ m       = ⊤
(suc n) ≤ zero    = ⊥
(suc n) ≤ (suc m) = n ≤ m

data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)

lookup : {A : Set}{n : Nat} (m : Nat) {{m≤n : suc m ≤ n}} → Vec A n → A
lookup m {{()}} []
lookup zero     (a ∷ as) = a
lookup (suc m)  (a ∷ as) = lookup m as
-- the instance in the recursive call is only found
-- if the candiate  m≤n : suc m ≤ _n  is kept
-- until the blocking _n has been solved

max_stars_repo_name: larrytheliquid/agda


text:
module SN.AntiRename where

open import Relation.Unary using (_∈_; _⊆_)

open import Library
open import Terms
open import Substitution
open import SN

mutual

  -- To formulate this, we need heterogeneous SNholes, going from Γ to Δ

  -- unRenameSNh : ∀{a b Γ Δ} (ρ : Δ ≤ Γ) {t : Tm Γ b} {E : ECxt Γ a b} {t' : Tm Γ a} →
  --   SNhole (subst ρ t) (λ t' → subst ρ (E t')) t' → SNhole t E t'
  -- unRenameSNh = TODO

  unRenameSNe : ∀{a Γ Δ} {ρ : Δ ≤ Γ} {t : Tm Γ a}{t'} → IndRen ρ t t' →
                SNe t' → SNe t
  unRenameSNe (var x x₁)     (var y)           = var x
  unRenameSNe (app is is₁)   (elim 𝒏 (appl 𝒖)) = elim (unRenameSNe is 𝒏) (appl (unRenameSN is₁ 𝒖))

  unRenameSN : ∀{a Γ Δ} {ρ : Δ ≤ Γ} {t : Tm Γ a} {t'} → IndRen ρ t t'
    → SN t' → SN t
  -- neutral cases:
  unRenameSN n           (ne 𝒏)       = ne (unRenameSNe n 𝒏)
  -- redex cases:
  unRenameSN is           (exp t⇒ 𝒕)   = exp (unRename⇒1 is t⇒) (unRenameSN (proj₂ (unRename⇒0 is t⇒)) 𝒕)
  -- constructor cases:
  unRenameSN (abs t)      (abs 𝒕)      = abs (unRenameSN t 𝒕)

  unRename⇒0 : ∀{a Γ Δ} {ρ : Δ ≤ Γ} {t : Tm Γ a} {t' : Tm Δ a}{tρ} → IndRen ρ t tρ
              → tρ ⟨ _ ⟩⇒ t' → Σ _ \ s → IndRen ρ s t'
  unRename⇒0 {ρ = ρ} (app {u = u} (abs {t = t} is) is₁)  (β 𝒖)  = _ , prop→Ind ρ (≡.trans (≡.sym (sgs-lifts-term {σ = ρ} {u = u} {t = t}))
                                                                      (≡.cong₂ (λ t₁ u₁ → subst (sgs u₁) t₁) (Ind→prop _ is) (Ind→prop _ is₁)))
  unRename⇒0 (app is is₁)        (cong (appl u) (appl .u) tρ→t') = let s , iss = unRename⇒0 is tρ→t' in app s _ , app iss is₁

  unRename⇒1 : ∀{a Γ Δ} {ρ : Δ ≤ Γ} {t : Tm Γ a} {t' : Tm Δ a}{tρ} → (is : IndRen ρ t tρ)
              → (t⇒ : tρ ⟨ _ ⟩⇒ t') → t ⟨ _  ⟩⇒ proj₁ (unRename⇒0 is t⇒)
  unRename⇒1 (app (abs is) is₁) (β 𝒖) = β (unRenameSN is₁ 𝒖)
  unRename⇒1 (app is is₁)        (cong (appl u) (appl .u) tρ→t') = cong (appl _) (appl _) (unRename⇒1 is tρ→t')

-- Extensionality of SN for function types:
-- If t x ∈ SN then t ∈ SN.

absVarSNe : ∀{Γ a b}{t : Tm (a ∷ Γ) (a →̂ b)} → app t (var (zero)) ∈ SNe → t ∈ SNe
absVarSNe (elim 𝒏 (appl 𝒖)) = 𝒏

absVarSN : ∀{Γ a b}{t : Tm (a ∷ Γ) (a →̂ b)} → app t (var (zero)) ∈ SN → t ∈ SN
absVarSN (ne 𝒖)                                                   = ne (absVarSNe 𝒖)
absVarSN (exp (β {t = t} 𝒖) 𝒕′)                                   = abs (unRenameSN (prop→Ind contract (subst-ext contract-sgs t)) 𝒕′)
absVarSN (exp (cong (appl ._) (appl ._) t⇒) 𝒕′) = exp t⇒ (absVarSN 𝒕′)

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
-- Andreas, 2016-12-29, issue #2363

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

test : Nat → Nat
test (suc n) with zero
test zero | q = zero
test zero = zero

-- Error WAS:
-- With clause pattern zero is not an instance of its parent pattern (suc "n")

-- Expected error:
-- With clause pattern zero is not an instance of its parent pattern (suc n)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Oscar.Class.AlphaConversion where

open import Oscar.Data.Nat
open import Oscar.Data.Fin
open import Oscar.Data.Equality
open import Oscar.Function
open import Oscar.Relation
open import Oscar.Level

record AlphaConversion {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
  infixr 19 _◂_
  field
    _◂_ : ∀ {m n} → m ⟨ B ⟩→ n → m ⟨ C ⟩→ n
    ◂-identity : ∀ {m} (x : C m) → id ◂ x ≡ x
    ◂-associativity : ∀ {l m n} (f : l ⟨ B ⟩→ m) (g : m ⟨ B ⟩→ n) (x : C l) → (g ∘ f) ◂ x ≡ g ◂ f ◂ x
    ◂-extensionality : ∀ {m n} {f g : m ⟨ B ⟩→ n} → f ≡̇ g → f ◂_ ≡̇ g ◂_

open AlphaConversion ⦃ … ⦄ public

instance AlphaConversion⋆ : ∀ {a} {A : Set a} {bc} {BC : A → Set bc} → AlphaConversion BC BC
AlphaConversion._◂_ AlphaConversion⋆ = id
AlphaConversion.◂-identity AlphaConversion⋆ _ = refl
AlphaConversion.◂-associativity AlphaConversion⋆ _ _ _ = refl
AlphaConversion.◂-extensionality AlphaConversion⋆ f≡̇g x = f≡̇g x


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sigma.Base where

open import Cubical.Core.Primitives public

-- Σ-types are defined in Core/Primitives as they are needed for Glue types.

_×_ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
A × B = Σ A (λ _ → B)

infixr 5 _×_


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

module StrictApplication where

open import Data.Nat

{-# NON_TERMINATING #-}
loop : ℕ
loop = loop

foo : ℕ
foo = (λ _ → 0) loop


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of rose trees
------------------------------------------------------------------------

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

module Data.Tree.Rose.Properties where

open import Level using (Level)
open import Size
open import Data.List.Base as List using (List)
open import Data.List.Extrema.Nat
import Data.List.Properties as Listₚ
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Tree.Rose
open import Function.Base
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

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

------------------------------------------------------------------------
-- map properties

map-compose : (f : A → B) (g : B → C) →
              map {i = i} (g ∘′ f) ≗ map {i = i} g ∘′ map {i = i} f
map-compose f g (node a ts) = cong (node (g (f a))) $ begin
  List.map (map (g ∘′ f)) ts             ≡⟨ Listₚ.map-cong (map-compose f g) ts ⟩
  List.map (map g ∘ map f) ts            ≡⟨ Listₚ.map-compose ts ⟩
  List.map (map g) (List.map (map f) ts) ∎

depth-map : (f : A → B) (t : Rose A i) → depth {i = i} (map {i = i} f t) ≡ depth {i = i} t
depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin
  List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩
  List.map (depth ∘′ map f) ts         ≡⟨ Listₚ.map-cong (depth-map f) ts ⟩
  List.map depth ts ∎

------------------------------------------------------------------------
-- foldr properties

foldr-map : (f : A → B) (n : B → List C → C) (ts : Rose A i) →
            foldr {i = i} n (map {i = i} f ts) ≡ foldr {i = i} (n ∘′ f) ts
foldr-map f n (node a ts) = cong (n (f a)) $ begin
  List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩
  List.map (foldr n ∘′ map f) ts           ≡⟨ Listₚ.map-cong (foldr-map f n) ts ⟩
  List.map (foldr (n ∘′ f)) ts             ∎


text:
module Day2 where

open import Data.String as String
open import Data.Maybe
open import Foreign.Haskell using (Unit)
open import Data.List as List hiding (fromMaybe)
open import Data.Nat
open import Data.Nat.DivMod
import Data.Nat.Show as ℕs
open import Data.Char
open import Data.Vec as Vec renaming (_>>=_ to _VV=_ ; toList to VecToList)
open import Data.Product
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Bool.Base
open import AocIO
open import AocUtil
open import AocVec
import Data.Fin as Fin

natDiff : ℕ → ℕ → ℕ
natDiff zero y = y
natDiff x zero = x
natDiff (suc x) (suc y) = natDiff x y

fromMaybe :  ∀ {a} {A : Set a} → A → Maybe A → A
fromMaybe v (just x) = x
fromMaybe v nothing = v

find : ∀ {a} {A : Set a} → (A → Bool) → List A → Maybe A
find pred [] = nothing
find pred (x ∷ ls) with (pred x)
... | false = find pred ls
... | true = just x

dividesEvenly : ℕ → ℕ → Bool
dividesEvenly zero zero = true
dividesEvenly zero dividend = false
dividesEvenly (suc divisor) dividend with (dividend mod (suc divisor))
... | Fin.Fin.zero = true
... | Fin.Fin.suc p = false

oneDividesTheOther : ℕ → ℕ → Bool
oneDividesTheOther x y = dividesEvenly x y ∨ dividesEvenly y x

main2 : IO Unit
main2 = mainBuilder (readFileMain processFile)
  where
    parseLine : List Char → List ℕ
    parseLine ls with (words ls)
    ... | line-words = List.map unsafeParseNat line-words
    minMax : {n : ℕ} → Vec ℕ (suc n) → (ℕ × ℕ)
    minMax {0} (x ∷ []) = x , x
    minMax {suc _} (x ∷ ls) with (minMax ls)
    ... | min , max = (min ⊓ x) , (max ⊔ x)
    minMaxDiff : List ℕ → ℕ
    minMaxDiff ls = helper (Vec.fromList ls)
      where
        helper : {n : ℕ} → Vec ℕ n → ℕ
        helper [] = 0
        helper (x ∷ vec) with (minMax (x ∷ vec))
        ... | min , max = natDiff min max
    lineDiff : List Char → ℕ
    lineDiff s = minMaxDiff (parseLine s)
    processFile : String → IO Unit
    processFile file-content with (lines (String.toList file-content))
    ... | file-lines with (List.map lineDiff file-lines)
    ... | line-diffs = printString (ℕs.show (List.sum line-diffs))

main : IO Unit
main = mainBuilder (readFileMain processFile)
  where
    parseLine : List Char → List ℕ
    parseLine ls with (words ls)
    ... | line-words = List.map unsafeParseNat line-words
    pierreDiv : ℕ → ℕ → ℕ
    pierreDiv x y with (x ⊓ y) | (x ⊔ y)
    ... | 0 | _ = 0
    ... | _ | 0 = 0
    ... | (suc min) | (suc max) = (suc max) div (suc min)
    lineDivider : List ℕ → Maybe ℕ
    lineDivider [] = nothing
    lineDivider (x ∷ ln) with (find (oneDividesTheOther x) ln)
    ... | nothing = lineDivider ln
    ... | just y = just (pierreDiv x y)
    lineScore : List Char → ℕ
    lineScore s = fromMaybe 0 (lineDivider (parseLine s))
    processFile : String → IO Unit
    processFile file-content with (lines (String.toList file-content))
    ... | file-lines with (List.map lineScore file-lines)
    ... | line-scores = printString (ℕs.show (List.sum line-scores))


text:
module OlderBasicILP.Indirect where

open import Common.Context public

-- Propositions of intuitionistic logic of proofs, without ∨, ⊥, or +.

infixr 10 _⦂_
infixl 9 _∧_
infixr 7 _▻_
data Ty (X : Set) : Set where
  α_  : Atom → Ty X
  _▻_ : Ty X → Ty X → Ty X
  _⦂_ : X → Ty X → Ty X
  _∧_ : Ty X → Ty X → Ty X
  ⊤  : Ty X

module _ {X : Set} where
  infix 7 _▻◅_
  _▻◅_ : Ty X → Ty X → Ty X
  A ▻◅ B = (A ▻ B) ∧ (B ▻ A)

  -- Additional useful propositions.

  _⦂⋆_ : ∀ {n} → VCx X n → VCx (Ty X) n → Cx (Ty X)
  ∅        ⦂⋆ ∅       = ∅
  (TS , T) ⦂⋆ (Ξ , A) = (TS ⦂⋆ Ξ) , (T ⦂ A)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------------
-- Group theory properties using Agsy
------------------------------------------------------------------------------

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

-- Tested with the development version of the Agda standard library on
-- 02 February 2012.

module Agsy.GroupTheory where

open import Data.Product

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

infix  8 _⁻¹
infixl 7 _·_

------------------------------------------------------------------------------
-- Group theory axioms

postulate
  G   : Set        -- The universe.
  ε   : G          -- The identity element.
  _·_ : G → G → G  -- The binary operation.
  _⁻¹ : G → G      -- The inverse function.

  assoc         : ∀ x y z → x · y · z    ≡ x · (y · z)
  leftIdentity  : ∀ x     →     ε · x    ≡ x
  rightIdentity : ∀ x     →     x · ε    ≡ x
  leftInverse   : ∀ x     →  x ⁻¹ · x    ≡ ε
  rightInverse  : ∀ x     →  x    · x ⁻¹ ≡ ε

-- Properties

y≡x⁻¹[xy] : ∀ a b → b ≡ a ⁻¹ · (a · b)
y≡x⁻¹[xy] a b = {!-t 20 -m!}  -- Agsy fails

x≡[xy]y⁻¹ : ∀ a b → a ≡ (a · b) · b ⁻¹
x≡[xy]y⁻¹ a b = {!-t 20 -m!}  -- Agsy fails

rightIdentityUnique : Σ G λ u → (∀ x → x · u ≡ x) ×
                                (∀ u' → (∀ x → x · u' ≡ x) → u ≡ u')
rightIdentityUnique = {!-t 20 -m!}  -- Agsy fails
  -- ε
  -- , rightIdentity
  -- , λ x x' → begin
  --              ε     ≡⟨ sym (x' ε) ⟩
  --              ε · x ≡⟨ leftIdentity x ⟩
  --              x
  --            ∎

rightIdentityUnique' : ∀ x u → x · u ≡ x → ε ≡ u
rightIdentityUnique' x u xu≡x = {!-t 20 -m!}  -- Agsy fails

leftIdentityUnique : Σ G λ u → (∀ x → u · x ≡ x) ×
                               (∀ u' → (∀ x → u' · x ≡ x) → u ≡ u')
leftIdentityUnique = {!-t 20 -m!}  -- Agsy fails
  -- ε
  -- , leftIdentity
  -- , λ x x' → begin
  --              ε     ≡⟨ sym (x' ε) ⟩
  --              x · ε ≡⟨ rightIdentity x ⟩
  --              x
  --            ∎

leftIdentityUnique' : ∀ x u → u · x ≡ x → ε ≡ u
leftIdentityUnique' x u ux≡x = {!-t 20 -m!}

rightCancellation : ∀ x y z → y · x ≡ z · x → y ≡ z
rightCancellation x y z = λ hyp → {!-t 20 -m!} -- Agsy fails

leftCancellation : ∀ x y z → x · y ≡ x · z → y ≡ z
leftCancellation x y z = λ hyp → {!-t 20 -m!}  -- Agsy fails

leftCancellationER : (x y z : G) → x · y ≡ x · z → y ≡ z
leftCancellationER x y z x·y≡x·z =
  begin
    y              ≡⟨ sym (leftIdentity y) ⟩
    ε · y          ≡⟨ subst (λ t → ε · y ≡ t · y) (sym (leftInverse x)) refl ⟩
    x ⁻¹ · x · y   ≡⟨ assoc (x ⁻¹) x y ⟩
    x ⁻¹ · (x · y) ≡⟨ subst (λ t → x ⁻¹ · (x · y) ≡ x ⁻¹ · t) x·y≡x·z refl ⟩
    x ⁻¹ · (x · z) ≡⟨ sym (assoc (x ⁻¹) x z) ⟩
    x ⁻¹ · x · z   ≡⟨ subst (λ t → x ⁻¹ · x · z ≡ t · z) (leftInverse x) refl ⟩
    ε · z          ≡⟨ leftIdentity z ⟩
    z
  ∎

rightInverseUnique : ∀ x → Σ G λ r → (x · r ≡ ε) ×
                                     (∀ r' → x · r' ≡ ε → r ≡ r')
rightInverseUnique x = {!-t 20 -m!}  -- Agsy fails

rightInverseUnique' : ∀ x r → x · r ≡ ε → x ⁻¹ ≡ r
rightInverseUnique' x r = λ hyp → {!-t 20 -m!}  -- Agsy fails

leftInverseUnique : ∀ x → Σ G λ l → (l · x ≡ ε) ×
                                    (∀ l' → l' · x ≡ ε → l ≡ l')
leftInverseUnique x = {!-t 20 -m!}  -- Agsy fails

⁻¹-involutive : ∀ x  → x ⁻¹ ⁻¹ ≡ x
⁻¹-involutive x = {!-t 20 -m!}  -- Agsy fails

inverseDistribution : ∀ x y → (x · y) ⁻¹ ≡ y ⁻¹ · x ⁻¹
inverseDistribution x y = {!-t 20 -m!}  -- Agsy fails

-- If the square of every element is the identity, the system is
-- commutative. From: TPTP 6.4.0. File: Problems/GRP/GRP001-2.p
x²≡ε→comm : (∀ a → a · a ≡ ε) → ∀ {b c d} → b · c ≡ d → c · b ≡ d
x²≡ε→comm hyp {b} {c} {d} bc≡d = {!-t 20 -m!}  -- Agsy fails


text:
data Bool : Set where
  true false : Bool

data Eq : Bool → Bool → Set where
  refl : (x : Bool) → Eq x x

test : (x : Bool) → Eq true x → Set
test _ (refl false) = Bool


text:
------------------------------------------------------------------------
-- Some decision procedures for equality
------------------------------------------------------------------------

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

open import Equality

module Equality.Decision-procedures
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Equality.Decidable-UIP eq
open import Prelude
  hiding (module ⊤; module ⊥; module ↑; module ℕ; module Σ; module List)

------------------------------------------------------------------------
-- The unit type

module ⊤ where

  -- Equality of values of the unit type is decidable.

  infix 4 _≟_

  _≟_ : Decidable-equality ⊤
  _ ≟ _ = yes (refl _)

------------------------------------------------------------------------
-- The empty type

module ⊥ {ℓ} where

  -- Equality of values of the empty type is decidable.

  infix 4 _≟_

  _≟_ : Decidable-equality (⊥ {ℓ = ℓ})
  () ≟ ()

------------------------------------------------------------------------
-- Lifting

module ↑ {a ℓ} {A : Type a} where

  -- ↑ preserves decidability of equality.

  module Dec (dec : Decidable-equality A) where

    infix 4 _≟_

    _≟_ : Decidable-equality (↑ ℓ A)
    lift x ≟ lift y = ⊎-map (cong lift) (_∘ cong lower) (dec x y)

------------------------------------------------------------------------
-- Booleans

module Bool where

  -- The values true and false are distinct.

  abstract

    true≢false : true ≢ false
    true≢false true≡false = subst T true≡false _

  -- Equality of booleans is decidable.

  infix 4 _≟_

  _≟_ : Decidable-equality Bool
  true  ≟ true  = yes (refl _)
  false ≟ false = yes (refl _)
  true  ≟ false = no true≢false
  false ≟ true  = no (true≢false ∘ sym)

------------------------------------------------------------------------
-- Σ-types

module Σ {a b} {A : Type a} {B : A → Type b} where

  -- Two variants of Dec._≟_ (which is defined below).

  set⇒dec⇒dec⇒dec :
    {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂} →
    Is-set A →
    Dec (x₁ ≡ x₂) →
    (∀ eq → Dec (subst B eq y₁ ≡ y₂)) →
    Dec ((x₁ , y₁) ≡ (x₂ , y₂))
  set⇒dec⇒dec⇒dec set₁ (no  x₁≢x₂) dec₂ = no (x₁≢x₂ ∘ cong proj₁)
  set⇒dec⇒dec⇒dec set₁ (yes x₁≡x₂) dec₂ with dec₂ x₁≡x₂
  … | yes cast-y₁≡y₂ = yes (Σ-≡,≡→≡ x₁≡x₂ cast-y₁≡y₂)
  … | no  cast-y₁≢y₂ =
    no (cast-y₁≢y₂ ∘
        subst (λ p → subst B p _ ≡ _) (set₁ _ _) ∘
        proj₂ ∘ Σ-≡,≡←≡)

  decidable⇒dec⇒dec :
    {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂} →
    Decidable-equality A →
    (∀ eq → Dec (subst B eq y₁ ≡ y₂)) →
    Dec ((x₁ , y₁) ≡ (x₂ , y₂))
  decidable⇒dec⇒dec dec =
    set⇒dec⇒dec⇒dec (decidable⇒set dec) (dec _ _)

  -- Σ preserves decidability of equality.

  module Dec (_≟A_ : Decidable-equality A)
             (_≟B_ : {x : A} → Decidable-equality (B x)) where

    infix 4 _≟_

    _≟_ : Decidable-equality (Σ A B)
    _ ≟ _ = decidable⇒dec⇒dec _≟A_ (λ _ → _ ≟B _)

------------------------------------------------------------------------
-- Binary products

module × {a b} {A : Type a} {B : Type b} where

  -- _,_ preserves decided equality.

  dec⇒dec⇒dec :
    {x₁ x₂ : A} {y₁ y₂ : B} →
    Dec (x₁ ≡ x₂) →
    Dec (y₁ ≡ y₂) →
    Dec ((x₁ , y₁) ≡ (x₂ , y₂))
  dec⇒dec⇒dec (no  x₁≢x₂) _           = no (x₁≢x₂ ∘ cong proj₁)
  dec⇒dec⇒dec _           (no  y₁≢y₂) = no (y₁≢y₂ ∘ cong proj₂)
  dec⇒dec⇒dec (yes x₁≡x₂) (yes y₁≡y₂) = yes (cong₂ _,_ x₁≡x₂ y₁≡y₂)

  -- _×_ preserves decidability of equality.

  module Dec (_≟A_ : Decidable-equality A)
             (_≟B_ : Decidable-equality B) where

    infix 4 _≟_

    _≟_ : Decidable-equality (A × B)
    _ ≟ _ = dec⇒dec⇒dec (_ ≟A _) (_ ≟B _)

------------------------------------------------------------------------
-- Binary sums

module ⊎ {a b} {A : Type a} {B : Type b} where

  abstract

    -- The values inj₁ x and inj₂ y are never equal.

    inj₁≢inj₂ : {x : A} {y : B} → inj₁ x ≢ inj₂ y
    inj₁≢inj₂ = Bool.true≢false ∘ cong (if_then true else false)

  -- The inj₁ and inj₂ constructors are cancellative.

  cancel-inj₁ : {x y : A} → _≡_ {A = A ⊎ B} (inj₁ x) (inj₁ y) → x ≡ y
  cancel-inj₁ {x = x} = cong {A = A ⊎ B} {B = A} [ id , const x ]

  cancel-inj₂ : {x y : B} → _≡_ {A = A ⊎ B} (inj₂ x) (inj₂ y) → x ≡ y
  cancel-inj₂ {x = x} = cong {A = A ⊎ B} {B = B} [ const x , id ]

  -- _⊎_ preserves decidability of equality.

  module Dec (_≟A_ : Decidable-equality A)
             (_≟B_ : Decidable-equality B) where

    infix 4 _≟_

    _≟_ : Decidable-equality (A ⊎ B)
    inj₁ x ≟ inj₁ y = ⊎-map (cong (inj₁ {B = B})) (λ x≢y → x≢y ∘ cancel-inj₁) (x ≟A y)
    inj₂ x ≟ inj₂ y = ⊎-map (cong (inj₂ {A = A})) (λ x≢y → x≢y ∘ cancel-inj₂) (x ≟B y)
    inj₁ x ≟ inj₂ y = no inj₁≢inj₂
    inj₂ x ≟ inj₁ y = no (inj₁≢inj₂ ∘ sym)

------------------------------------------------------------------------
-- Lists

module List {a} {A : Type a} where

  abstract

    -- The values [] and x ∷ xs are never equal.

    []≢∷ : ∀ {x : A} {xs} → [] ≢ x ∷ xs
    []≢∷ = Bool.true≢false ∘
             cong (λ { [] → true; (_ ∷ _) → false })

  -- The _∷_ constructor is cancellative in both arguments.

  private

    head? : A → List A → A
    head? x []      = x
    head? _ (x ∷ _) = x

    tail? : List A → List A
    tail? []       = []
    tail? (_ ∷ xs) = xs

  cancel-∷-head : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y
  cancel-∷-head {x} = cong (head? x)

  cancel-∷-tail : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
  cancel-∷-tail = cong tail?

  abstract

    -- An η-like result for the cancellation lemmas.

    unfold-∷ : ∀ {x y : A} {xs ys} (eq : x ∷ xs ≡ y ∷ ys) →
               eq ≡ cong₂ _∷_ (cancel-∷-head eq) (cancel-∷-tail eq)
    unfold-∷ {x} eq =
      eq                                             ≡⟨ sym $ trans-reflʳ eq ⟩
      trans eq (refl _)                              ≡⟨ sym $ cong (trans eq) sym-refl ⟩
      trans eq (sym (refl _))                        ≡⟨ sym $ trans-reflˡ _ ⟩
      trans (refl _) (trans eq (sym (refl _)))       ≡⟨ sym $ cong-roughly-id (λ xs → head? x xs ∷ tail? xs)
                                                                              non-empty eq tt tt lemma₁ ⟩
      cong (λ xs → head? x xs ∷ tail? xs) eq         ≡⟨ lemma₂ _∷_ (head? x) tail? eq ⟩∎
      cong₂ _∷_ (cong (head? x) eq) (cong tail? eq)  ∎
      where
      non-empty : List A → Bool
      non-empty []      = false
      non-empty (_ ∷ _) = true

      lemma₁ : (xs : List A) →
               if non-empty xs then ⊤ else ⊥ →
               head? x xs ∷ tail? xs ≡ xs
      lemma₁ []      ()
      lemma₁ (_ ∷ _) _ = refl _

      lemma₂ : {A B C D : Type a} {x y : A}
               (f : B → C → D) (g : A → B) (h : A → C) →
               (eq : x ≡ y) →
               cong (λ x → f (g x) (h x)) eq ≡
               cong₂ f (cong g eq) (cong h eq)
      lemma₂ f g h =
        elim (λ eq → cong (λ x → f (g x) (h x)) eq ≡
                     cong₂ f (cong g eq) (cong h eq))
             (λ x → cong (λ x → f (g x) (h x)) (refl x)          ≡⟨ cong-refl (λ x → f (g x) (h x)) ⟩
                    refl (f (g x) (h x))                         ≡⟨ sym $ cong₂-refl f ⟩
                    cong₂ f (refl (g x)) (refl (h x))            ≡⟨ sym $ cong₂ (cong₂ f) (cong-refl g) (cong-refl h) ⟩∎
                    cong₂ f (cong g (refl x)) (cong h (refl x))  ∎)

  -- List preserves decidability of equality.

  module Dec (_≟A_ : Decidable-equality A) where

    infix 4 _≟_

    _≟_ : Decidable-equality (List A)
    []       ≟ []       = yes (refl [])
    []       ≟ (_ ∷ _)  = no []≢∷
    (_ ∷ _)  ≟ []       = no ([]≢∷ ∘ sym)
    (x ∷ xs) ≟ (y ∷ ys) with x ≟A y
    ... | no  x≢y = no (x≢y ∘ cancel-∷-head)
    ... | yes x≡y with xs ≟ ys
    ...   | yes xs≡ys = yes (cong₂ _∷_ x≡y xs≡ys)
    ...   | no  xs≢ys = no  (xs≢ys ∘ cancel-∷-tail)

------------------------------------------------------------------------
-- Finite sets

module Fin where

  -- Equality of finite numbers is decidable.

  infix 4 _≟_

  _≟_ : ∀ {n} → Decidable-equality (Fin n)
  _≟_ {zero}  = λ ()
  _≟_ {suc n} = ⊎.Dec._≟_ (λ _ _ → yes (refl tt)) (_≟_ {n})

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Cats.Category.Cat.Facts.Exponential where

open import Data.Product using (_,_)
open import Level using (_⊔_)
open import Relation.Binary using (IsEquivalence)

open import Cats.Bifunctor using
  (Bifunctor ; Bifunctor→Functor₁ ; transposeBifunctor₁ ; transposeBifunctor₁-resp)
open import Cats.Category
open import Cats.Category.Cat as Cat using
  (Cat ; Functor ; _∘_ ; _≈_) renaming
  (id to Id)
open import Cats.Category.Cat.Facts.Product using (hasBinaryProducts ; ⟨_×_⟩)
open import Cats.Category.Fun using (Fun ; Trans ; ≈-intro ; ≈-elim)
open import Cats.Category.Fun.Facts using (NatIso→≅)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Trans.Iso as NatIso using (NatIso)
open import Cats.Util.Conv
open import Cats.Util.Simp using (simp!)

import Cats.Category.Base as Base
import Cats.Category.Constructions.Unique as Unique
import Cats.Category.Constructions.Iso as Iso

open Functor
open Trans
open Iso.Build._≅_

infixr 1 _↝_

_↝_ : ∀ {lo la l≈ lo′ la′ l≈′}
  → Category lo la l≈
  → Category lo′ la′ l≈′
  → Category (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′) (lo ⊔ la ⊔ la′ ⊔ l≈′) (lo ⊔ l≈′)
_↝_ = Fun

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

  private
    module B = Category B
    module C = Category C
    module B↝C = Category (Fun B C)

  Eval : Bifunctor (B ↝ C) B C
  Eval = record
      { fobj = λ where
          (F , x) → fobj F x
      ; fmap = λ where
          {F , a} {G , b} (θ , f) → fmap G f C.∘ component θ a
      ; fmap-resp = λ where
          {F , a} {G , b} {θ , f} {ι , g} (θ≈ι , f≈g) →
            C.∘-resp (fmap-resp G f≈g) (≈-elim θ≈ι)
      ; fmap-id = λ { {F , b} → C.≈.trans (C.∘-resp-l (fmap-id F)) C.id-l }
      ; fmap-∘ = λ where
          {F , a} {G , b} {H , c} {θ , f} {ι , g} →
            begin
              (fmap H f C.∘ component θ b) C.∘ (fmap G g C.∘ component ι a)
            ≈⟨ C.∘-resp-l (C.≈.sym (natural θ)) ⟩
              (component θ c C.∘ fmap G f) C.∘ (fmap G g C.∘ component ι a)
            ≈⟨ simp! C ⟩
              component θ c C.∘ (fmap G f C.∘ fmap G g) C.∘ component ι a
            ≈⟨ C.∘-resp-r (C.∘-resp-l (fmap-∘ G)) ⟩
              component θ c C.∘ (fmap G (f B.∘ g)) C.∘ component ι a
            ≈⟨ simp! C ⟩
              (component θ c C.∘ fmap G (f B.∘ g)) C.∘ component ι a
            ≈⟨ C.∘-resp-l (natural θ) ⟩
              (fmap H (f B.∘ g) C.∘ component θ a) C.∘ component ι a
            ≈⟨ simp! C ⟩
              fmap H (f B.∘ g) C.∘ component θ a C.∘ component ι a
            ∎
      }
    where
      open C.≈-Reasoning

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

  private
    module B = Category B
    module C = Category C
    module D = Category D
    module C↝D = Category (Fun C D)

  Curry : Bifunctor B C D → Functor B (C ↝ D)
  Curry F = transposeBifunctor₁ F

  Curry-resp : ∀ {F G} → F ≈ G → Curry F ≈ Curry G
  Curry-resp = transposeBifunctor₁-resp

  Curry-correct : ∀ {F} → Eval ∘ ⟨ Curry F × Id ⟩ ≈ F
  Curry-correct {F} = record
      { iso = D.≅.refl
      ; forth-natural = λ where
        {a , a′} {b , b′} {f , f′} →
          begin
            D.id D.∘ fmap F (B.id , f′) D.∘ fmap F (f , C.id)
          ≈⟨ D.≈.trans D.id-l (fmap-∘ F) ⟩
            fmap F (B.id B.∘ f , f′ C.∘ C.id)
          ≈⟨ fmap-resp F (B.id-l , C.id-r) ⟩
            fmap F (f , f′)
          ≈⟨ D.≈.sym D.id-r ⟩
            fmap F (f , f′) D.∘ D.id
          ∎
      }
    where
      open D.≈-Reasoning

  Curry-unique : ∀ {F Curry′}
    → Eval ∘ ⟨ Curry′ × Id ⟩ ≈ F
    → Curry′ ≈ Curry F
  Curry-unique {F} {Curry′} eq@record { iso = iso ; forth-natural = fnat } = record
      { iso = λ {x} →
          let open C↝D.≅-Reasoning in
          C↝D.≅.sym (
            begin
              fobj (Curry F) x
            ≈⟨ NatIso.iso (Curry-resp (sym-Cat eq)) ⟩
              fobj (Curry (Eval ∘ ⟨ Curry′ × Id ⟩)) x
            ≈⟨ NatIso→≅ (lem x) ⟩
              fobj Curry′ x
            ∎
          )
      ; forth-natural = λ {a} {b} {f} → ≈-intro λ {x} →
          -- TODO We need a simplification tactic.
          let open D.≈-Reasoning in
          triangle (forth iso D.∘ component (fmap Curry′ f) x)
          ( begin
              ((forth iso D.∘
                 (fmap (fobj Curry′ b) C.id D.∘ component (fmap Curry′ B.id) x) D.∘ D.id) D.∘
               D.id D.∘ D.id) D.∘
              component (fmap Curry′ f) x
            ≈⟨ ∘-resp-l (trans (∘-resp-r id-l) (trans id-r (trans (∘-resp-r
                 (trans id-r (trans (∘-resp (fmap-id (fobj Curry′ b))
                    (≈-elim (fmap-id Curry′))) id-l))) id-r))) ⟩
              forth iso D.∘ component (fmap Curry′ f) x
            ∎
          )
          ( begin
              fmap F (f , C.id) D.∘
              (forth iso D.∘ (fmap (fobj Curry′ a) C.id D.∘ component (fmap Curry′ B.id) x) D.∘ D.id) D.∘
              D.id D.∘ D.id
            ≈⟨ ∘-resp-r (trans (∘-resp-r id-r) (trans id-r (trans (∘-resp-r
                 (trans id-r (trans (∘-resp-l (fmap-id (fobj Curry′ a)))
                    (trans id-l (≈-elim (fmap-id Curry′)))))) id-r))) ⟩
              fmap F (f , C.id) D.∘ forth iso
            ≈⟨ sym fnat ⟩
              forth iso D.∘ fmap (fobj Curry′ b) C.id D.∘ component (fmap Curry′ f) x
            ≈⟨ ∘-resp-r (trans (∘-resp-l (fmap-id (fobj Curry′ b))) id-l) ⟩
              forth iso D.∘ component (fmap Curry′ f) x
            ∎
          )
      }
    where
      open D using (id-l ; id-r ; ∘-resp ; ∘-resp-l ; ∘-resp-r)
      open D.≈ using (sym ; trans)
      open IsEquivalence Cat.equiv using () renaming (sym to sym-Cat)

      lem : ∀ x
        → NatIso (Bifunctor→Functor₁ (Eval ∘ ⟨ Curry′ × Id ⟩) x) (fobj Curry′ x)
      lem x = record
          { iso = D.≅.refl
          ; forth-natural = D.≈.trans D.id-l (D.∘-resp-r (≈-elim (fmap-id Curry′)))
          }

instance
  hasExponentials : ∀ l → HasExponentials (Cat l l l)
  hasExponentials l = record
      { _↝′_ = λ B C → record
          { Cᴮ = B ↝ C
          ; eval = Eval
          ; curry′ = λ F → record
              { arr = Curry F
              ; prop = Curry-correct {F = F}
              ; unique = λ {g} eq →
                  let open IsEquivalence Cat.equiv using (sym) in
                  sym (Curry-unique eq)
              }
          }
      }


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

open import Categories.Category using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)

module Categories.Category.Monoidal.Utilities {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level
open import Function using (_$_)
open import Data.Product using (_×_; _,_; curry′)

open import Categories.Category.Product
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor; appˡ; appʳ)
open import Categories.Functor.Properties using ([_]-resp-≅)
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
  hiding (unitorˡ; unitorʳ; associator; _≃_)

infixr 10 _⊗ᵢ_

open import Categories.Morphism C using (_≅_; module ≅)
open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟)
open import Categories.Morphism.Isomorphism C using (_∘ᵢ_; lift-triangle′; lift-pentagon′)
open import Categories.Morphism.Reasoning C

private
  module C = Category C

open C hiding (id; identityˡ; identityʳ; assoc)
open Commutation

private
  variable
    X Y Z W A B : Obj
    f g h i a b : X ⇒ Y

open Monoidal M
module ⊗ = Functor ⊗

-- for exporting, it makes sense to use the above long names, but for
-- internal consumption, the traditional (short!) categorical names are more
-- convenient. However, they are not symmetric, even though the concepts are, so
-- we'll use ⇒ and ⇐ arrows to indicate that

module Shorthands where

  λ⇒ = unitorˡ.from
  λ⇐ = unitorˡ.to
  ρ⇒ = unitorʳ.from
  ρ⇐ = unitorʳ.to
  -- eta expansion fixes a problem in 2.6.1, will be reported
  α⇒ = λ {X} {Y} {Z} → associator.from {X} {Y} {Z}
  α⇐ = λ {X} {Y} {Z} → associator.to {X} {Y} {Z}

open Shorthands

private
  [x⊗y]⊗z : Bifunctor (Product C C) C C
  [x⊗y]⊗z = ⊗ ∘F (⊗ ⁂ idF)

  -- note how this one needs re-association to typecheck (i.e. be correct)
  x⊗[y⊗z] : Bifunctor (Product C C) C C
  x⊗[y⊗z] = ⊗ ∘F (idF ⁂ ⊗) ∘F assocˡ _ _ _

unitor-coherenceʳ : [ (A ⊗₀ unit) ⊗₀ unit ⇒ A ⊗₀ unit ]⟨ ρ⇒ ⊗₁ C.id ≈ ρ⇒ ⟩
unitor-coherenceʳ = cancel-fromˡ unitorʳ unitorʳ-commute-from

unitor-coherenceˡ : [ unit ⊗₀ unit ⊗₀ A ⇒ unit ⊗₀ A ]⟨ C.id ⊗₁ λ⇒ ≈ λ⇒ ⟩
unitor-coherenceˡ = cancel-fromˡ unitorˡ unitorˡ-commute-from

-- All the implicits below can be inferred, but being explicit is clearer
unitorˡ-naturalIsomorphism : NaturalIsomorphism (unit ⊗-) idF
unitorˡ-naturalIsomorphism = record
  { F⇒G = ntHelper record
    { η       = λ X → λ⇒ {X}
    ; commute = λ f → unitorˡ-commute-from {f = f}
    }
  ; F⇐G = ntHelper record
    { η       = λ X → λ⇐ {X}
    ; commute = λ f → unitorˡ-commute-to {f = f}
    }
  ; iso = λ X →  unitorˡ.iso {X}
  }

unitorʳ-naturalIsomorphism : NaturalIsomorphism (-⊗ unit) idF
unitorʳ-naturalIsomorphism = record
  { F⇒G = ntHelper record
    { η       = λ X → ρ⇒ {X}
    ; commute = λ f → unitorʳ-commute-from {f = f}
    }
  ; F⇐G = ntHelper record
    { η       = λ X → ρ⇐ {X}
    ; commute = λ f → unitorʳ-commute-to {f = f}
    }
  ; iso = λ X → unitorʳ.iso {X}
  }

-- skipping the explicit arguments here, it does not increase understandability
associator-naturalIsomorphism : NaturalIsomorphism [x⊗y]⊗z x⊗[y⊗z]
associator-naturalIsomorphism = record
  { F⇒G = ntHelper record
    { η       = λ { ((X , Y) , Z) → α⇒ {X} {Y} {Z}}
    ; commute = λ _ → assoc-commute-from
    }
  ; F⇐G = ntHelper record
    { η       = λ _ → α⇐
    ; commute = λ _ → assoc-commute-to
    }
  ; iso = λ _ → associator.iso
  }

module unitorˡ-natural = NaturalIsomorphism unitorˡ-naturalIsomorphism
module unitorʳ-natural = NaturalIsomorphism unitorʳ-naturalIsomorphism
module associator-natural = NaturalIsomorphism associator-naturalIsomorphism

_⊗ᵢ_ : X ≅ Y → Z ≅ W → X ⊗₀ Z ≅ Y ⊗₀ W
f ⊗ᵢ g = [ ⊗ ]-resp-≅ record
  { from = from f , from g
  ; to   = to f , to g
  ; iso  = record
    { isoˡ = isoˡ f , isoˡ g
    ; isoʳ = isoʳ f , isoʳ g
    }
  }
  where open _≅_

triangle-iso : ≅.refl ⊗ᵢ unitorˡ ∘ᵢ associator ≃ unitorʳ {X} ⊗ᵢ ≅.refl {Y}
triangle-iso = lift-triangle′ triangle

pentagon-iso :
    ≅.refl ⊗ᵢ associator ∘ᵢ associator ∘ᵢ associator {X} {Y} {Z} ⊗ᵢ ≅.refl {W}
  ≃ associator ∘ᵢ associator
pentagon-iso = lift-pentagon′ pentagon

refl⊗refl≃refl : ≅.refl {A} ⊗ᵢ ≅.refl {B} ≃ ≅.refl
refl⊗refl≃refl = ⌞ ⊗.identity ⌟

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- A library of parser combinators
------------------------------------------------------------------------

-- This module also provides examples of parsers for which the indices
-- cannot be inferred.

module RecursiveDescent.Hybrid.Lib where

open import RecursiveDescent.Hybrid
import RecursiveDescent.Hybrid.Type as Type
open import RecursiveDescent.Index
open import Utilities

open import Data.Nat hiding (_≟_)
open import Data.Vec  using (Vec;  []; _∷_)
open import Data.Vec1 using (Vec₁; []; _∷_; map₀₁)
open import Data.List using (List; []; _∷_; foldr; reverse)
open import Data.Product.Record hiding (_×_)
open import Data.Product using (_×_) renaming (_,_ to pair)
open import Data.Bool hiding (_≟_)
open import Data.Function
open import Data.Maybe
open import Data.Unit hiding (_≟_)
open import Data.Bool.Properties as Bool
import Data.Char as Char
open Char using (Char; _==_)
open import Algebra
private
  module BCS = CommutativeSemiring Bool.commutativeSemiring-∨-∧
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (refl)

------------------------------------------------------------------------
-- Applicative functor parsers

-- We could get these for free with better library support.

infixl 50 _⊛_ _⊛!_ _<⊛_ _⊛>_ _<$>_ _<$_ _⊗_ _⊗!_

_⊛_ : forall {tok nt i₁ i₂ r₁ r₂} ->
      Parser tok nt i₁ (r₁ -> r₂) ->
      Parser tok nt i₂ r₁ ->
      Parser tok nt _  r₂
p₁ ⊛ p₂ = p₁ >>= \f -> p₂ >>= \x -> return (f x)

-- A variant: If the second parser does not accept the empty string,
-- then neither does the combination. (This is immediate for the first
-- parser, but for the second one a small lemma is needed, hence this
-- variant.)

_⊛!_ : forall {tok nt i₁ c₂ r₁ r₂} ->
       Parser tok nt i₁ (r₁ -> r₂) ->
       Parser tok nt (false , c₂) r₁ ->
       Parser tok nt (false , _)  r₂
_⊛!_ {i₁ = i₁} p₁ p₂ = cast (BCS.*-comm (proj₁ i₁) false) refl
                            (p₁ ⊛ p₂)

_<$>_ : forall {tok nt i r₁ r₂} ->
        (r₁ -> r₂) ->
        Parser tok nt i r₁ ->
        Parser tok nt _ r₂
f <$> x = return f ⊛ x

_<⊛_ : forall {tok nt i₁ i₂ r₁ r₂} ->
       Parser tok nt i₁ r₁ ->
       Parser tok nt i₂ r₂ ->
       Parser tok nt _ r₁
x <⊛ y = const <$> x ⊛ y

_⊛>_ : forall {tok nt i₁ i₂ r₁ r₂} ->
       Parser tok nt i₁ r₁ ->
       Parser tok nt i₂ r₂ ->
       Parser tok nt _ r₂
x ⊛> y = flip const <$> x ⊛ y

_<$_ : forall {tok nt i r₁ r₂} ->
       r₁ ->
       Parser tok nt i r₂ ->
       Parser tok nt _ r₁
x <$ y = const x <$> y

_⊗_ : forall {tok nt i₁ i₂ r₁ r₂} ->
      Parser tok nt i₁ r₁ -> Parser tok nt i₂ r₂ ->
      Parser tok nt _ (r₁ × r₂)
p₁ ⊗ p₂ = pair <$> p₁ ⊛ p₂

_⊗!_ : forall {tok nt i₁ c₂ r₁ r₂} ->
      Parser tok nt i₁ r₁ -> Parser tok nt (false , c₂) r₂ ->
      Parser tok nt (false , _) (r₁ × r₂)
p₁ ⊗! p₂ = pair <$> p₁ ⊛! p₂

------------------------------------------------------------------------
-- Parsing sequences

infix 55 _⋆ _+

-- Not accepted by the productivity checker:

-- mutual

--   _⋆ : forall {tok r d} ->
--        Parser tok (false , d) r     ->
--        Parser tok _           (List r)
--   p ⋆ ~ return [] ∣ p +

--   _+ : forall {tok r d} ->
--        Parser tok (false , d) r     ->
--        Parser tok _           (List r)
--   p + ~ _∷_ <$> p ⊛ p ⋆

-- By inlining some definitions we can show that the definitions are
-- productive, though. The following definitions have also been
-- simplified:

mutual

  _⋆ : forall {tok nt r d} ->
       Parser tok nt (false , d) r     ->
       Parser tok nt _           (List r)
  p ⋆ ~ Type.alt _ _ (return []) (p +)

  _+ : forall {tok nt r d} ->
       Parser tok nt (false , d) r     ->
       Parser tok nt _           (List r)
  p + ~ Type._!>>=_ p     \x  ->
        Type._?>>=_ (p ⋆) \xs ->
        return (x ∷ xs)

-- p sepBy sep parses one or more ps separated by seps.

_sepBy_ : forall {tok nt r r' i d} ->
          Parser tok nt i r -> Parser tok nt (false , d) r' ->
          Parser tok nt _ (List r)
p sepBy sep = _∷_ <$> p ⊛ (sep ⊛> p) ⋆

-- Note that the index of atLeast is only partly inferred; the
-- recursive structure of atLeast-index is given manually.

atLeast-index : Corners -> ℕ -> Index
atLeast-index c zero    = _
atLeast-index c (suc n) = _

-- At least n occurrences of p.

atLeast : forall {tok nt c r} (n : ℕ) ->
          Parser tok nt (false , c) r ->
          Parser tok nt (atLeast-index c n) (List r)
atLeast zero    p = p ⋆
atLeast (suc n) p = _∷_ <$> p ⊛ atLeast n p

-- Chains at least n occurrences of op, in an a-associative
-- manner. The ops are surrounded by ps.

chain≥ : forall {tok nt c₁ i₂ r} (n : ℕ) ->
         Assoc ->
         Parser tok nt (false , c₁) r ->
         Parser tok nt i₂ (r -> r -> r) ->
         Parser tok nt _ r
chain≥ n a p op = chain≥-combine a <$> p ⊛ atLeast n (op ⊗! p)

-- exactly n p parses n occurrences of p.

exactly-index : Index -> ℕ -> Index
exactly-index i zero    = _
exactly-index i (suc n) = _

exactly : forall {tok nt i r} n ->
          Parser tok nt i r ->
          Parser tok nt (exactly-index i n) (Vec r n)
exactly zero    p = return []
exactly (suc n) p = _∷_ <$> p ⊛ exactly n p

-- A function with a similar type:

sequence : forall {tok nt i r n} ->
           Vec₁ (Parser tok nt i r) n ->
           Parser tok nt (exactly-index i n) (Vec r n)
sequence []       = return []
sequence (p ∷ ps) = _∷_ <$> p ⊛ sequence ps

-- p between ps parses p repeatedly, between the elements of ps:
--   ∙ between (x ∷ y ∷ z ∷ []) ≈ x ∙ y ∙ z.

between-corners : Corners -> ℕ -> Corners
between-corners c′ zero    = _
between-corners c′ (suc n) = _

_between_ : forall {tok nt i r c′ r′ n} ->
            Parser tok nt i r ->
            Vec₁ (Parser tok nt (false , c′) r′) (suc n) ->
            Parser tok nt (false , between-corners c′ n) (Vec r n)
p between (x ∷ [])     = [] <$ x
p between (x ∷ y ∷ xs) = _∷_ <$> (x ⊛> p) ⊛ (p between (y ∷ xs))

------------------------------------------------------------------------
-- N-ary variants of _∣_

-- choice ps parses one of the elements in ps.

choice-corners : Corners -> ℕ -> Corners
choice-corners c zero    = _
choice-corners c (suc n) = _

choice : forall {tok nt c r n} ->
         Vec₁ (Parser tok nt (false , c) r) n ->
         Parser tok nt (false , choice-corners c n) r
choice []       = fail
choice (p ∷ ps) = p ∣ choice ps

-- choiceMap f xs ≈ choice (map f xs), but avoids use of Vec₁ and
-- fromList.

choiceMap-corners : forall {a} -> (a -> Corners) -> List a -> Corners
choiceMap-corners c []       = _
choiceMap-corners c (x ∷ xs) = _

choiceMap : forall {tok nt r a} {c : a -> Corners} ->
            ((x : a) -> Parser tok nt (false , c x) r) ->
            (xs : List a) ->
            Parser tok nt (false , choiceMap-corners c xs) r
choiceMap f []       = fail
choiceMap f (x ∷ xs) = f x ∣ choiceMap f xs

------------------------------------------------------------------------
-- sat and friends

sat : forall {tok nt r} ->
      (tok -> Maybe r) -> Parser tok nt (0I ·I 1I) r
sat {tok} {nt} {r} p = symbol !>>= \c -> ok (p c)
  where
  okIndex : Maybe r -> Index
  okIndex nothing  = _
  okIndex (just _) = _

  ok : (x : Maybe r) -> Parser tok nt (okIndex x) r
  ok nothing  = fail
  ok (just x) = return x

sat' : forall {tok nt} -> (tok -> Bool) -> Parser tok nt _ ⊤
sat' p = sat (boolToMaybe ∘ p)

any : forall {tok nt} -> Parser tok nt _ tok
any = sat just

------------------------------------------------------------------------
-- Token parsers

module Token (a : DecSetoid) where

  open DecSetoid a using (_≟_) renaming (carrier to tok)

  -- Parses a given token (or, really, a given equivalence class of
  -- tokens).

  sym : forall {nt} -> tok -> Parser tok nt _ tok
  sym x = sat p
    where
    p : tok -> Maybe tok
    p y with x ≟ y
    ... | yes _ = just y
    ... | no  _ = nothing

  -- Parses a sequence of tokens.

  string : forall {nt n} -> Vec tok n -> Parser tok nt _ (Vec tok n)
  string cs = sequence (map₀₁ sym cs)

------------------------------------------------------------------------
-- Character parsers

digit : forall {nt} -> Parser Char nt _ ℕ
digit = 0 <$ sym '0'
      ∣ 1 <$ sym '1'
      ∣ 2 <$ sym '2'
      ∣ 3 <$ sym '3'
      ∣ 4 <$ sym '4'
      ∣ 5 <$ sym '5'
      ∣ 6 <$ sym '6'
      ∣ 7 <$ sym '7'
      ∣ 8 <$ sym '8'
      ∣ 9 <$ sym '9'
  where open Token Char.decSetoid

number : forall {nt} -> Parser Char nt _ ℕ
number = toNum <$> digit +
  where
  toNum = foldr (\n x -> 10 * x + n) 0 ∘ reverse

-- whitespace recognises an incomplete but useful list of whitespace
-- characters.

whitespace : forall {nt} -> Parser Char nt _ ⊤
whitespace = sat' isSpace
  where
  isSpace = \c ->
    (c == ' ') ∨ (c == '\t') ∨ (c == '\n') ∨ (c == '\r')

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
  open import Data.Proofs
  open import Function.Proofs
  open import Logic.Propositional.Theorems
  open import Structure.Container.SetLike
  open import Structure.Relator
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  instance
    ImageSet-setLike : SetLike(_∈_ {ℓᵢ})
    SetLike._⊆_ ImageSet-setLike A B = ∀{x} → (x ∈ A) → (x ∈ B)
    SetLike._≡_ ImageSet-setLike A B = ∀{x} → (x ∈ A) ↔ (x ∈ B)
    SetLike.[⊆]-membership ImageSet-setLike = [↔]-reflexivity
    SetLike.[≡]-membership ImageSet-setLike = [↔]-reflexivity
  private open module ImageSet-SetLike {ℓᵢ} = SetLike(ImageSet-setLike{ℓᵢ}) public
  open import Structure.Container.SetLike.Proofs using ([⊇]-membership) public
  module _ {ℓᵢ} where
    instance [⊆]-binaryRelator  = Structure.Container.SetLike.Proofs.[⊆]-binaryRelator  ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [⊇]-binaryRelator  = Structure.Container.SetLike.Proofs.[⊇]-binaryRelator  ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [≡]-to-[⊆]         = Structure.Container.SetLike.Proofs.[≡]-to-[⊆]         ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [≡]-to-[⊇]         = Structure.Container.SetLike.Proofs.[≡]-to-[⊇]         ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [⊆]-reflexivity    = Structure.Container.SetLike.Proofs.[⊆]-reflexivity    ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [⊆]-antisymmetry   = Structure.Container.SetLike.Proofs.[⊆]-antisymmetry   ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [⊆]-transitivity   = Structure.Container.SetLike.Proofs.[⊆]-transitivity   ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [⊆]-partialOrder   = Structure.Container.SetLike.Proofs.[⊆]-partialOrder   ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [≡]-reflexivity    = Structure.Container.SetLike.Proofs.[≡]-reflexivity    ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [≡]-symmetry       = Structure.Container.SetLike.Proofs.[≡]-symmetry       ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [≡]-transitivity   = Structure.Container.SetLike.Proofs.[≡]-transitivity   ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [≡]-equivalence    = Structure.Container.SetLike.Proofs.[≡]-equivalence    ⦃ ImageSet-setLike{ℓᵢ} ⦄
    instance [∈]-unaryOperatorᵣ = Structure.Container.SetLike.Proofs.[∈]-unaryOperatorᵣ ⦃ ImageSet-setLike{ℓᵢ} ⦄

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:
module Issue180 where

module Example₁ where

  data C : Set where
    c : C → C

  data Indexed : (C → C) → Set where
    i : Indexed c

  foo : Indexed c → Set
  foo i = C

module Example₂ where

  data List (A : Set) : Set where
    nil  : List A
    cons : A → List A → List A

  postulate
    A : Set
    x : A

  T : Set
  T = List A → List A

  data P : List T → Set where
    p : (f : T) → P (cons f nil)

  data S : (xs : List T) → P xs → Set where
    s : (f : T) → S (cons f nil) (p f)

  foo : S (cons (cons x) nil) (p (cons x)) → A
  foo (s ._) = x


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Hash
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig

-- This module defines an abstract system state given a reachable
-- concrete system state.

module LibraBFT.Concrete.System where

 ℓ-VSFP : Level
 ℓ-VSFP = 1ℓ ℓ⊔ ℓ-RoundManager

 open import LibraBFT.Yasm.Base
 import      LibraBFT.Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms as LYS

 -- What EpochConfigs are known in the system?  For now, only the initial one.  Later, we will add
 -- knowledge of subsequent EpochConfigs known via EpochChangeProofs.
 data EpochConfig∈Sys (st : LYS.SystemState) (𝓔 : EpochConfig) : Set ℓ-EC where
   inGenInfo : init-EC genInfo ≡ 𝓔 → EpochConfig∈Sys st 𝓔
   -- inECP  : ∀ {ecp} → ecp ECP∈Sys st → verify-ECP ecp 𝓔 → EpochConfig∈Sys

 -- A peer pid can sign a new message for a given PK if pid is the owner of a PK in a known
 -- EpochConfig.
 record PeerCanSignForPK (st : LYS.SystemState) (v : Vote) (pid : NodeId) (pk : PK) : Set ℓ-VSFP where
   constructor mkPCS4PK
   field
     𝓔       : EpochConfig
     𝓔id≡    : epoch 𝓔 ≡ v ^∙ vEpoch
     𝓔inSys  : EpochConfig∈Sys st 𝓔
     mbr      : Member 𝓔
     nid≡     : toNodeId  𝓔 mbr ≡ pid
     pk≡      : getPubKey 𝓔 mbr ≡ pk
 open PeerCanSignForPK

 PCS4PK⇒NodeId-PK-OK : ∀ {st v pid pk} → (pcs : PeerCanSignForPK st v pid pk) → NodeId-PK-OK (𝓔 pcs) pk pid
 PCS4PK⇒NodeId-PK-OK (mkPCS4PK _ _ _ mbr n≡ pk≡) = mbr , n≡ , pk≡

 -- This is super simple for now because the only known EpochConfig is dervied from genInfo, which is not state-dependent
 PeerCanSignForPK-stable : LYS.ValidSenderForPK-stable-type PeerCanSignForPK
 PeerCanSignForPK-stable _ _ (mkPCS4PK 𝓔₁ 𝓔id≡₁ (inGenInfo refl) mbr₁ nid≡₁ pk≡₁) = (mkPCS4PK 𝓔₁ 𝓔id≡₁ (inGenInfo refl) mbr₁ nid≡₁ pk≡₁)

 open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK
                                                                  (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})

 -- An implementation must prove that, if one of its handlers sends a
 -- message that contains a vote and is signed by a public key pk, then
 -- either the vote's author is the peer executing the handler, the
 -- epochId is in range, the peer is a member of the epoch, and its key
 -- in that epoch is pk; or, a message with the same signature has been
 -- sent before.  This is represented by StepPeerState-AllValidParts.
 module WithSPS (sps-corr : StepPeerState-AllValidParts) where

   -- Bring in 'unwind', 'ext-unforgeability' and friends
   open Structural sps-corr

   -- TODO-1: refactor this somewhere else?  Maybe something like
   -- LibraBFT.Impl.Consensus.Types.Properties?
   sameSig⇒sameVoteData : ∀ {v1 v2 : Vote} {pk}
                        → WithVerSig pk v1
                        → WithVerSig pk v2
                        → v1 ^∙ vSignature ≡ v2 ^∙ vSignature
                        → NonInjective-≡ sha256 ⊎ v2 ^∙ vVoteData ≡ v1 ^∙ vVoteData
   sameSig⇒sameVoteData {v1} {v2} wvs1 wvs2 refl
      with verify-bs-inj (verified wvs1) (verified wvs2)
        -- The signable fields of the votes must be the same (we do not model signature collisions)
   ...| bs≡
        -- Therefore the LedgerInfo is the same for the new vote as for the previous vote
        = sym <⊎$> (hashVote-inj1 {v1} {v2} (sameBS⇒sameHash bs≡))

   -- We are now ready to define an 'IntermediateSystemState' view for a concrete
   -- reachable state.  We will do so by fixing an epoch that exists in
   -- the system, which will enable us to define the abstract
   -- properties. The culminaton of this 'PerEpoch' module is seen in
   -- the 'IntSystemState' "function" at the bottom, which probably the
   -- best place to start uynderstanding this.  Longer term, we will
   -- also need higher-level, cross-epoch properties.
   module PerState (st : SystemState)(r : ReachableSystemState st) where

    -- TODO-3: Remove this postulate when we are satisfied with the
    -- "hash-collision-tracking" solution. For example, when proving voo
    -- (in LibraBFT.LibraBFT.Concrete.Properties.VotesOnce), we
    -- currently use this postulate to eliminate the possibility of two
    -- votes that have the same signature but different VoteData
    -- whenever we use sameSig⇒sameVoteData.  To eliminate the
    -- postulate, we need to refine the properties we prove to enable
    -- the possibility of a hash collision, in which case the required
    -- property might not hold.  However, it is not sufficient to simply
    -- prove that a hash collision *exists* (which is obvious,
    -- regardless of the LibraBFT implementation).  Rather, we
    -- ultimately need to produce a specific hash collision and relate
    -- it to the data in the system, so that we can prove that the
    -- desired properties hold *unless* an actual hash collision is
    -- found by the implementation given the data in the system.  In
    -- the meantime, we simply require that the collision identifies a
    -- reachable state; later "collision tracking" will require proof
    -- that the colliding values actually exist in that state.
    postulate  -- temporary assumption that hash collisions don't exist (see comment above)
      meta-sha256-cr : ¬ (NonInjective-≡ sha256)

    sameSig⇒sameVoteDataNoCol : ∀ {v1 v2 : Vote} {pk}
                              → WithVerSig pk v1
                              → WithVerSig pk v2
                              → v1 ^∙ vSignature ≡ v2 ^∙ vSignature
                              → v2 ^∙ vVoteData ≡ v1 ^∙ vVoteData
    sameSig⇒sameVoteDataNoCol {v1} {v2} wvs1 wvs2 refl
       with sameSig⇒sameVoteData {v1} {v2} wvs1 wvs2 refl
    ...| inj₁ hb = ⊥-elim (meta-sha256-cr hb)
    ...| inj₂ x = x

    module PerEpoch (𝓔 : EpochConfig) where

     open import LibraBFT.Abstract.Abstract     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs hiding (qcVotes; Vote)
     open import LibraBFT.Concrete.Intermediate                   𝓔 (ConcreteVoteEvidence 𝓔)
     open import LibraBFT.Concrete.Records                        𝓔

     -- * Auxiliary definitions;
     -- Here we capture the idea that there exists a vote message that
     -- witnesses the existence of a given Abs.Vote
     record ∃VoteMsgFor (v : Abs.Vote) : Set where
       constructor mk∃VoteMsgFor
       field
         -- A message that was actually sent
         nm            : NetworkMsg
         cv            : Vote
         cv∈nm         : cv ⊂Msg nm
         -- And contained a valid vote that, once abstracted, yeilds v.
         vmsgMember    : EpochConfig.Member 𝓔
         vmsgSigned    : WithVerSig (getPubKey 𝓔 vmsgMember) cv
         vmsg≈v        : α-ValidVote 𝓔 cv vmsgMember ≡ v
         vmsgEpoch     : cv ^∙ vEpoch ≡ epoch 𝓔
     open ∃VoteMsgFor public

     record ∃VoteMsgSentFor (sm : SentMessages)(v : Abs.Vote) : Set where
       constructor mk∃VoteMsgSentFor
       field
         vmFor        : ∃VoteMsgFor v
         vmSender     : NodeId
         nmSentByAuth : (vmSender , (nm vmFor)) ∈ sm
     open ∃VoteMsgSentFor public

     ∃VoteMsgSentFor-stable : ∀ {pre : SystemState} {post : SystemState} {v}
                            → Step pre post
                            → ∃VoteMsgSentFor (msgPool pre) v
                            → ∃VoteMsgSentFor (msgPool post) v
     ∃VoteMsgSentFor-stable theStep (mk∃VoteMsgSentFor sndr vmFor sba) =
                                     mk∃VoteMsgSentFor sndr vmFor (msgs-stable theStep sba)

     ∈QC⇒sent : ∀{st : SystemState} {q α}
              → Abs.Q q α-Sent (msgPool st)
              → Meta-Honest-Member α
              → (vα : α Abs.∈QC q)
              → ∃VoteMsgSentFor (msgPool st) (Abs.∈QC-Vote q vα)
     ∈QC⇒sent vsent@(ws {sender} {nm} e≡ nm∈st (qc∈NM {cqc} {q} .{nm} valid cqc∈nm q≡)) ha va
       with All-reduce⁻ {vdq = Any-lookup va} (α-Vote cqc valid) All-self
                        (subst (Any-lookup va ∈_) (cong Abs.qVotes q≡) (Any-lookup-correctP va))
     ...| as , as∈cqc , α≡
       with  α-Vote-evidence cqc valid  as∈cqc | inspect
            (α-Vote-evidence cqc valid) as∈cqc
     ...| ev | [ refl ]
        with vote∈qc {vs = as} as∈cqc refl cqc∈nm
     ...| v∈nm = mk∃VoteMsgSentFor
                   (mk∃VoteMsgFor nm (₋cveVote ev) v∈nm
                                  (₋ivvMember (₋cveIsValidVote ev))
                                  (₋ivvSigned (₋cveIsValidVote ev)) (sym α≡)
                                  (₋ivvEpoch (₋cveIsValidVote ev)))
                   sender
                   nm∈st

     -- Finally, we can define the abstract system state corresponding to the concrete state st
     IntSystemState : IntermediateSystemState ℓ0
     IntSystemState = record
       { InSys           = λ { r → r α-Sent (msgPool st) }
       ; HasBeenSent     = λ { v → ∃VoteMsgSentFor (msgPool st) v }
       ; ∈QC⇒HasBeenSent = ∈QC⇒sent {st = st}
       }

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda