text:
{-# OPTIONS --allow-unsolved-metas #-}
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CS410 2017/18 Exercise 1  VECTORS AND FRIENDS (worth 25%)
------------------------------------------------------------------------------
------------------------------------------------------------------------------

-- NOTE (19/9/17) This file is currently incomplete: more will arrive on
-- GitHub.

-- MARK SCHEME (transcribed from paper): the (m) numbers add up to slightly
-- more than 25, so should be taken as the maximum number of marks losable on
-- the exercise. In fact, I did mark it negatively, but mostly because it was
-- done so well (with Agda's help) that it was easier to find the errors.

------------------------------------------------------------------------------
-- Dependencies
------------------------------------------------------------------------------

open import CS410-Prelude

------------------------------------------------------------------------------
-- Vectors
------------------------------------------------------------------------------

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_   -- the "cons" operator associates to the right

-- I like to use the asymmetric ,- to remind myself that the element is to
-- the left and the rest of the list is to the right.

-- Vectors are useful when there are important length-related safety
-- properties.

------------------------------------------------------------------------------
-- Heads and Tails
------------------------------------------------------------------------------

-- We can rule out nasty head and tail errors by insisting on nonemptiness!

--??--1.1-(2)-----------------------------------------------------------------

vHead : {X : Set}{n : Nat} -> Vec X (suc n) -> X
vHead xs = {!!}

vTail : {X : Set}{n : Nat} -> Vec X (suc n) -> Vec X n
vTail xs = {!!}

vHeadTailFact :  {X : Set}{n : Nat}(xs : Vec X (suc n)) ->
                 (vHead xs ,- vTail xs) == xs
vHeadTailFact xs = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Concatenation and its Inverse
------------------------------------------------------------------------------

--??--1.2-(2)-----------------------------------------------------------------

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
xs +V ys = {!!}
infixr 4 _+V_

vChop : {X : Set}(m : Nat){n : Nat} -> Vec X (m +N n) -> Vec X m * Vec X n
vChop m xs = {!!}

vChopAppendFact : {X : Set}{m n : Nat}(xs : Vec X m)(ys : Vec X n) ->
                  vChop m (xs +V ys) == (xs , ys)
vChopAppendFact xs ys = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Map, take I
------------------------------------------------------------------------------

-- Implement the higher-order function that takes an operation on
-- elements and does it to each element of a vector. Use recursion
-- on the vector.
-- Note that the type tells you the size remains the same.

-- Show that if the elementwise function "does nothing", neither does
-- its vMap. "map of identity is identity"

-- Show that two vMaps in a row can be collapsed to just one, or
-- "composition of maps is map of compositions"

--??--1.3-(2)-----------------------------------------------------------------

vMap : {X Y : Set} -> (X -> Y) -> {n : Nat} -> Vec X n -> Vec Y n
vMap f xs = {!!}

vMapIdFact : {X : Set}{f : X -> X}(feq : (x : X) -> f x == x) ->
             {n : Nat}(xs : Vec X n) -> vMap f xs == xs
vMapIdFact feq xs = {!!}

vMapCpFact : {X Y Z : Set}{f : Y -> Z}{g : X -> Y}{h : X -> Z}
               (heq : (x : X) -> f (g x) == h x) ->
             {n : Nat}(xs : Vec X n) ->
               vMap f (vMap g xs) == vMap h xs
vMapCpFact heq xs = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- vMap and +V
------------------------------------------------------------------------------

-- Show that if you've got two vectors of Xs and a function from X to Y,
-- and you want to concatenate and map, it doesn't matter which you do
-- first.

--??--1.4-(1)-----------------------------------------------------------------

vMap+VFact : {X Y : Set}(f : X -> Y) ->
             {m n : Nat}(xs : Vec X m)(xs' : Vec X n) ->
             vMap f (xs +V xs') == (vMap f xs +V vMap f xs')
vMap+VFact f xs xs' = {!!}

--??--------------------------------------------------------------------------

-- Think about what you could prove, relating vMap with vHead, vTail, vChop...
-- Now google "Philip Wadler" "Theorems for Free"

------------------------------------------------------------------------------
-- Applicative Structure (giving mapping and zipping cheaply)
------------------------------------------------------------------------------

--??--1.5-(2)-----------------------------------------------------------------

-- HINT: you will need to override the default invisibility of n to do this.
vPure : {X : Set} -> X -> {n : Nat} -> Vec X n
vPure x {n} = {!!}

_$V_ : {X Y : Set}{n : Nat} -> Vec (X -> Y) n -> Vec X n -> Vec Y n
fs $V xs = {!!}
infixl 3 _$V_  -- "Application associates to the left,
               --  rather as we all did in the sixties." (Roger Hindley)

-- Pattern matching and recursion are forbidden for the next two tasks.

-- implement vMap again, but as a one-liner
vec : {X Y : Set} -> (X -> Y) -> {n : Nat} -> Vec X n -> Vec Y n
vec f xs = {!!}

-- implement the operation which pairs up corresponding elements
vZip : {X Y : Set}{n : Nat} -> Vec X n -> Vec Y n -> Vec (X * Y) n
vZip xs ys = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Applicative Laws
------------------------------------------------------------------------------

-- According to "Applicative programming with effects" by
--   Conor McBride and Ross Paterson
-- some laws should hold for applicative functors.
-- Check that this is the case.

--??--1.6-(2)-----------------------------------------------------------------

vIdentity : {X : Set}{f : X -> X}(feq : (x : X) -> f x == x) ->
            {n : Nat}(xs : Vec X n) -> (vPure f $V xs) == xs
vIdentity feq xs = {!!}

vHomomorphism : {X Y : Set}(f : X -> Y)(x : X) ->
                {n : Nat} -> (vPure f $V vPure x) == vPure (f x) {n}
vHomomorphism f x {n} = {!!}

vInterchange : {X Y : Set}{n : Nat}(fs : Vec (X -> Y) n)(x : X) ->
               (fs $V vPure x) == (vPure (_$ x) $V fs)
vInterchange fs x = {!!}

vComposition : {X Y Z : Set}{n : Nat}
               (fs : Vec (Y -> Z) n)(gs : Vec (X -> Y) n)(xs : Vec X n) ->
               (vPure _<<_ $V fs $V gs $V xs) == (fs $V (gs $V xs))
vComposition fs gs xs = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Order-Preserving Embeddings (also known in the business as "thinnings")
------------------------------------------------------------------------------

-- What have these to do with Pascal's Triangle?

data _<=_ : Nat -> Nat -> Set where
  oz :                          zero  <= zero
  os : {n m : Nat} -> n <= m -> suc n <= suc m
  o' : {n m : Nat} -> n <= m ->     n <= suc m

-- Find all the values in each of the following <= types.
-- This is a good opportunity to learn to use C-c C-a with the -l option
--   (a.k.a. "google the type" without "I feel lucky")
-- The -s n option also helps.

--??--1.7-(1)-----------------------------------------------------------------

all0<=4 : Vec (0 <= 4) {!!}
all0<=4 = {!!}

all1<=4 : Vec (1 <= 4) {!!}
all1<=4 = {!!}

all2<=4 : Vec (2 <= 4) {!!}
all2<=4 = {!!}

all3<=4 : Vec (3 <= 4) {!!}
all3<=4 = {!!}

all4<=4 : Vec (4 <= 4) {!!}
all4<=4 = {!!}

-- Prove the following. A massive case analysis "rant" is fine.

no5<=4 : 5 <= 4 -> Zero
no5<=4 th = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Order-Preserving Embeddings Select From Vectors
------------------------------------------------------------------------------

-- Use n <= m to encode the choice of n elements from an m-Vector.
-- The os constructor tells you to take the next element of the vector;
-- the o' constructor tells you to omit the next element of the vector.

--??--1.8-(2)-----------------------------------------------------------------

_<?=_ : {X : Set}{n m : Nat} -> n <= m -> Vec X m
                     -> Vec X n
th <?= xs = {!!}

-- it shouldn't matter whether you map then select or select then map

vMap<?=Fact : {X Y : Set}(f : X -> Y)
              {n m : Nat}(th : n <= m)(xs : Vec X m) ->
              vMap f (th <?= xs) == (th <?= vMap f xs)
vMap<?=Fact f th xs = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Our Favourite Thinnings
------------------------------------------------------------------------------

-- Construct the identity thinning and the empty thinning.

--??--1.9-(1)-----------------------------------------------------------------

oi : {n : Nat} -> n <= n
oi {n}  = {!!}

oe : {n : Nat} -> 0 <= n
oe {n}  = {!!}

--??--------------------------------------------------------------------------

-- Show that all empty thinnings are equal to yours.

--??--1.10-(1)----------------------------------------------------------------

oeUnique : {n : Nat}(th : 0 <= n) -> th == oe
oeUnique i = {!!}

--??--------------------------------------------------------------------------

-- Show that there are no thinnings of form big <= small  (TRICKY)
-- Then show that all the identity thinnings are equal to yours.
-- Note that you can try the second even if you haven't finished the first.
-- HINT: you WILL need to expose the invisible numbers.
-- HINT: check CS410-Prelude for a reminder of >=

--??--1.11-(3)----------------------------------------------------------------

oTooBig : {n m : Nat} -> n >= m -> suc n <= m -> Zero
oTooBig {n} {m} n>=m th = {!!}

oiUnique : {n : Nat}(th : n <= n) -> th == oi
oiUnique th = {!!}

--??--------------------------------------------------------------------------

-- Show that the identity thinning selects the whole vector

--??--1.12-(1)----------------------------------------------------------------

id-<?= : {X : Set}{n : Nat}(xs : Vec X n) -> (oi <?= xs) == xs
id-<?= xs = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Composition of Thinnings
------------------------------------------------------------------------------

-- Define the composition of thinnings and show that selecting by a
-- composite thinning is like selecting then selecting again.
-- A small bonus applies to minimizing the length of the proof.
-- To collect the bonus, you will need to think carefully about
-- how to make the composition as *lazy* as possible.

--??--1.13-(3)----------------------------------------------------------------

_o>>_ : {p n m : Nat} -> p <= n -> n <= m -> p <= m
th o>> th' = {!!}

cp-<?= : {p n m : Nat}(th : p <= n)(th' : n <= m) ->
         {X : Set}(xs : Vec X m) ->
         ((th o>> th') <?= xs) == (th <?= (th' <?= xs))
cp-<?= th th' xs = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Thinning Dominoes
------------------------------------------------------------------------------

--??--1.14-(3)----------------------------------------------------------------

idThen-o>> : {n m : Nat}(th : n <= m) -> (oi o>> th) == th
idThen-o>> th = {!!}

idAfter-o>> : {n m : Nat}(th : n <= m) -> (th o>> oi) == th
idAfter-o>> th = {!!}

assoc-o>> : {q p n m : Nat}(th0 : q <= p)(th1 : p <= n)(th2 : n <= m) ->
            ((th0 o>> th1) o>> th2) == (th0 o>> (th1 o>> th2))
assoc-o>> th0 th1 th2 = {!!}

--??--------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Vectors as Arrays
------------------------------------------------------------------------------

-- We can use 1 <= n as the type of bounded indices into a vector and do
-- a kind of "array projection". First we select a 1-element vector from
-- the n-element vector, then we take its head to get the element out.

vProject : {n : Nat}{X : Set} -> Vec X n -> 1 <= n -> X
vProject xs i = vHead (i <?= xs)

-- Your (TRICKY) mission is to reverse the process, tabulating a function
-- from indices as a vector. Then show that these operations are inverses.

--??--1.15-(3)----------------------------------------------------------------

-- HINT: composition of functions
vTabulate : {n : Nat}{X : Set} -> (1 <= n -> X) -> Vec X n
vTabulate {n} f = {!!}

-- This should be easy if vTabulate is correct.
vTabulateProjections : {n : Nat}{X : Set}(xs : Vec X n) ->
                       vTabulate (vProject xs) == xs
vTabulateProjections xs = {!!}

-- HINT: oeUnique
vProjectFromTable : {n : Nat}{X : Set}(f : 1 <= n -> X)(i : 1 <= n) ->
                    vProject (vTabulate f) i == f i
vProjectFromTable f i = {!!}

--??--------------------------------------------------------------------------

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Vec
------------------------------------------------------------------------

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

module Data.Vec.Categorical {a n} where

open import Category.Applicative using (RawApplicative)
open import Category.Applicative.Indexed using (Morphism)
open import Category.Functor as Fun using (RawFunctor)
import Function.Identity.Categorical as Id
open import Category.Monad using (RawMonad)
open import Data.Fin using (Fin)
open import Data.Vec as Vec hiding (_⊛_)
open import Data.Vec.Properties
open import Function

------------------------------------------------------------------------
-- Functor and applicative

functor : RawFunctor (λ (A : Set a) → Vec A n)
functor = record
  { _<$>_ = map
  }

applicative : RawApplicative (λ (A : Set a) → Vec A n)
applicative = record
  { pure = replicate
  ; _⊛_  = Vec._⊛_
  }

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA : ∀ {A n} → Vec (F A) n → F (Vec A n)
  sequenceA []       = pure []
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs

  mapA : ∀ {a} {A : Set a} {B n} → (A → F B) → Vec A n → F (Vec B n)
  mapA f = sequenceA ∘ map f

  forA : ∀ {a} {A : Set a} {B n} → Vec A n → (A → F B) → F (Vec B n)
  forA = flip mapA

module _ {m M} (Mon : RawMonad {m} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : ∀ {A n} → Vec (M A) n → M (Vec A n)
  sequenceM = sequenceA App

  mapM : ∀ {a} {A : Set a} {B n} → (A → M B) → Vec A n → M (Vec B n)
  mapM = mapA App

  forM : ∀ {a} {A : Set a} {B n} → Vec A n → (A → M B) → M (Vec B n)
  forM = forA App

------------------------------------------------------------------------
-- Other

-- lookup is a functor morphism from Vec to Identity.

lookup-functor-morphism : (i : Fin n) → Fun.Morphism functor Id.functor
lookup-functor-morphism i = record
  { op     = flip lookup i
  ; op-<$> = lookup-map i
  }

-- lookup is an applicative functor morphism.

lookup-morphism : (i : Fin n) → Morphism applicative Id.applicative
lookup-morphism i = record
  { op      = flip lookup i
  ; op-pure = lookup-replicate i
  ; op-⊛    = lookup-⊛ i
  }

ext: agda


text:
-- A placeholder module so that we can write a main. Agda compilation
-- does not work without a main so batch compilation is bound to give
-- errors. For travis builds, we want batch compilation and this is
-- module can be imported to serve that purpose. There is nothing
-- useful that can be achieved from this module though.

module io.placeholder where

open import hott.core.universe

postulate
  Unit      : Type₀
  IO        : Type₀ → Type₀
  dummyMain : IO Unit

{-# COMPILED_TYPE Unit       ()           #-}
{-# COMPILED_TYPE IO         IO           #-}
{-# COMPILED      dummyMain  (return ())  #-}
{-# BUILTIN       IO         IO           #-}

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
open import Mockingbird.Forest using (Forest)
import Mockingbird.Forest.Birds as Birds

-- The Master Forest
module Mockingbird.Problems.Chapter18 {b ℓ} (forest : Forest {b} {ℓ})
                                      ⦃ _ : Birds.HasStarling forest ⦄
                                      ⦃ _ : Birds.HasKestrel forest ⦄ where

open import Data.Maybe using (Maybe; nothing; just)
open import Data.Product using (_×_; _,_; proj₁; ∃-syntax)
open import Data.Vec using (Vec; []; _∷_; _++_)
open import Data.Vec.Relation.Unary.Any.Properties using (++⁺ʳ)
open import Function using (_$_)
open import Level using (_⊔_)
open import Mockingbird.Forest.Combination.Vec forest using (⟨_⟩; here; there; [_]; _⟨∙⟩_∣_; _⟨∙⟩_; [#_])
open import Mockingbird.Forest.Combination.Vec.Properties forest using (subst′; weaken-++ˡ; weaken-++ʳ; ++-comm)
open import Relation.Unary using (_∈_)

open Forest forest
open import Mockingbird.Forest.Birds forest

problem₁ : HasIdentity
problem₁ = record
  { I = S ∙ K ∙ K
  ; isIdentity = λ x → begin
      S ∙ K ∙ K ∙ x    ≈⟨ isStarling K K x ⟩
      K ∙ x ∙ (K ∙ x)  ≈⟨ isKestrel x (K ∙ x) ⟩
      x                ∎
  }

private instance hasIdentity = problem₁

problem₂ : HasMockingbird
problem₂ = record
  { M = S ∙ I ∙ I
  ; isMockingbird = λ x → begin
      S ∙ I ∙ I ∙ x    ≈⟨ isStarling I I x ⟩
      I ∙ x ∙ (I ∙ x)  ≈⟨ congʳ $ isIdentity x ⟩
      x ∙ (I ∙ x)      ≈⟨ congˡ $ isIdentity x ⟩
      x ∙ x            ∎
  }

private instance hasMockingbird = problem₂

problem₃ : HasThrush
problem₃ = record
  { T = S ∙ (K ∙ (S ∙ I)) ∙ K
  ; isThrush = λ x y → begin
      S ∙ (K ∙ (S ∙ I)) ∙ K ∙ x ∙ y  ≈⟨ congʳ $ isStarling (K ∙ (S ∙ I)) K x ⟩
      K ∙ (S ∙ I) ∙ x ∙ (K ∙ x) ∙ y  ≈⟨ (congʳ $ congʳ $ isKestrel (S ∙ I) x) ⟩
      S ∙ I ∙ (K ∙ x) ∙ y            ≈⟨ isStarling I (K ∙ x) y ⟩
      I ∙ y ∙ (K ∙ x ∙ y)            ≈⟨ congʳ $ isIdentity y ⟩
      y ∙ (K ∙ x ∙ y)                ≈⟨ congˡ $ isKestrel x y ⟩
      y ∙ x                          ∎
  }

-- TODO: Problem 4.

I∈⟨S,K⟩ : I ∈ ⟨ S ∷ K ∷ [] ⟩
I∈⟨S,K⟩ = subst′ refl $ [# 0 ] ⟨∙⟩ [# 1 ] ⟨∙⟩ [# 1 ]

-- Try to strengthen a proof of X ∈ ⟨ y ∷ xs ⟩ to X ∈ ⟨ xs ⟩, which can be done
-- if y does not occur in X.
strengthen : ∀ {n X y} {xs : Vec Bird n} → X ∈ ⟨ y ∷ xs ⟩ → Maybe (X ∈ ⟨ xs ⟩)
-- NOTE: it could be the case that y ∈ xs, but checking that requires decidable
-- equality.
strengthen [ here X≈y ] = nothing
strengthen [ there X∈xs ] = just [ X∈xs ]
strengthen (Y∈⟨y,xs⟩ ⟨∙⟩ Z∈⟨y,xs⟩ ∣ YZ≈X) = do
  Y∈⟨xs⟩ ← strengthen Y∈⟨y,xs⟩
  Z∈⟨xs⟩ ← strengthen Z∈⟨y,xs⟩
  just $ Y∈⟨xs⟩ ⟨∙⟩ Z∈⟨xs⟩ ∣ YZ≈X
  where
    open import Data.Maybe.Categorical using (monad)
    open import Category.Monad using (RawMonad)
    open RawMonad (monad {b ⊔ ℓ})

eliminate : ∀ {n X y} {xs : Vec Bird n} → X ∈ ⟨ y ∷ xs ⟩ → ∃[ X′ ] (X′ ∈ ⟨ S ∷ K ∷ xs ⟩ × X′ ∙ y ≈ X)
eliminate {X = X} {y} [ here X≈y ] = (I , weaken-++ˡ I∈⟨S,K⟩ , trans (isIdentity y) (sym X≈y))
eliminate {X = X} {y} [ there X∈xs ] = (K ∙ X , [# 1 ] ⟨∙⟩ [ ++⁺ʳ (S ∷ K ∷ []) X∈xs ] , isKestrel X y)
eliminate {X = X} {y} (_⟨∙⟩_∣_ {Y} {Z} Y∈⟨y,xs⟩ [ here Z≈y ] YZ≈X) with strengthen Y∈⟨y,xs⟩
... | just Y∈⟨xs⟩ = (Y , weaken-++ʳ (S ∷ K ∷ []) Y∈⟨xs⟩ , trans (congˡ (sym Z≈y)) YZ≈X)
... | nothing =
  let (Y′ , Y′∈⟨S,K,xs⟩ , Y′y≈Y) = eliminate Y∈⟨y,xs⟩

      SY′Iy≈X : S ∙ Y′ ∙ I ∙ y ≈ X
      SY′Iy≈X = begin
        S ∙ Y′ ∙ I ∙ y    ≈⟨ isStarling Y′ I y ⟩
        Y′ ∙ y ∙ (I ∙ y)  ≈⟨ congʳ $ Y′y≈Y ⟩
        Y ∙ (I ∙ y)       ≈⟨ congˡ $ isIdentity y ⟩
        Y ∙ y             ≈˘⟨ congˡ Z≈y ⟩
        Y ∙ Z             ≈⟨ YZ≈X ⟩
        X                 ∎
  in (S ∙ Y′ ∙ I , [# 0 ] ⟨∙⟩ Y′∈⟨S,K,xs⟩ ⟨∙⟩ weaken-++ˡ I∈⟨S,K⟩ , SY′Iy≈X)
eliminate {X = X} {y} (_⟨∙⟩_∣_ {Y} {Z} Y∈⟨y,xs⟩ Z∈⟨y,xs⟩ YZ≈X) =
  let (Y′ , Y′∈⟨S,K,xs⟩ , Y′y≈Y) = eliminate Y∈⟨y,xs⟩
      (Z′ , Z′∈⟨S,K,xs⟩ , Z′y≈Z) = eliminate Z∈⟨y,xs⟩

      SY′Z′y≈X : S ∙ Y′ ∙ Z′ ∙ y ≈ X
      SY′Z′y≈X = begin
        S ∙ Y′ ∙ Z′ ∙ y    ≈⟨ isStarling Y′ Z′ y ⟩
        Y′ ∙ y ∙ (Z′ ∙ y)  ≈⟨ congʳ Y′y≈Y ⟩
        Y ∙ (Z′ ∙ y)       ≈⟨ congˡ Z′y≈Z ⟩
        Y ∙ Z              ≈⟨ YZ≈X ⟩
        X                  ∎
  in (S ∙ Y′ ∙ Z′ , [# 0 ] ⟨∙⟩ Y′∈⟨S,K,xs⟩ ⟨∙⟩ Z′∈⟨S,K,xs⟩ , SY′Z′y≈X)

module _ (x y : Bird) where
  -- Example: y-eliminating the expression y should give I.
  _ : proj₁ (eliminate {y = y} {xs = x ∷ []} $ [# 0 ]) ≈ I
  _ = refl

  -- Example: y-eliminating the expression x should give Kx.
  _ : proj₁ (eliminate {y = y} {xs = x ∷ []} $ [# 1 ]) ≈ K ∙ x
  _ = refl

  -- Example: y-eliminating the expression xy should give x (Principle 3).
  _ : proj₁ (eliminate {y = y} {xs = x ∷ []} $ [# 1 ] ⟨∙⟩ [# 0 ]) ≈ x
  _ = refl

  -- Example: y-eliminating the expression yx should give SI(Kx).
  _ : proj₁ (eliminate {y = y} {xs = x ∷ []} $ [# 0 ] ⟨∙⟩ [# 1 ]) ≈ S ∙ I ∙ (K ∙ x)
  _ = refl

  -- Example: y-eliminating the expression yy should give SII.
  _ : proj₁ (eliminate {y = y} {xs = x ∷ []} $ [# 0 ] ⟨∙⟩ [# 0 ]) ≈ S ∙ I ∙ I
  _ = refl

strengthen-SK : ∀ {n X y} {xs : Vec Bird n} → X ∈ ⟨ S ∷ K ∷ y ∷ xs ⟩ → Maybe (X ∈ ⟨ S ∷ K ∷ xs ⟩)
strengthen-SK {y = y} {xs} X∈⟨S,K,y,xs⟩ = do
  let X∈⟨y,xs,S,K⟩ = ++-comm (S ∷ K ∷ []) (y ∷ xs) X∈⟨S,K,y,xs⟩
  X∈⟨xs,S,K⟩ ← strengthen X∈⟨y,xs,S,K⟩
  let X∈⟨S,K,xs⟩ = ++-comm xs (S ∷ K ∷ []) X∈⟨xs,S,K⟩
  just X∈⟨S,K,xs⟩
  where
    open import Data.Maybe.Categorical using (monad)
    open import Category.Monad using (RawMonad)
    open RawMonad (monad {b ⊔ ℓ})

-- TODO: formulate eliminate or eliminate-SK in terms of the other.
eliminate-SK : ∀ {n X y} {xs : Vec Bird n} → X ∈ ⟨ S ∷ K ∷ y ∷ xs ⟩ → ∃[ X′ ] (X′ ∈ ⟨ S ∷ K ∷ xs ⟩ × X′ ∙ y ≈ X)
eliminate-SK {X = X} {y} [ here X≈S ] = (K ∙ S , [# 1 ] ⟨∙⟩ [# 0 ] , trans (isKestrel S y) (sym X≈S))
eliminate-SK {X = X} {y} [ there (here X≈K) ] = (K ∙ K , [# 1 ] ⟨∙⟩ [# 1 ] , trans (isKestrel K y) (sym X≈K))
eliminate-SK {X = X} {y} [ there (there (here X≈y)) ] = (I , weaken-++ˡ I∈⟨S,K⟩ , trans (isIdentity y) (sym X≈y))
eliminate-SK {X = X} {y} [ there (there (there X∈xs)) ] = (K ∙ X , ([# 1 ] ⟨∙⟩ [ (++⁺ʳ (S ∷ K ∷ []) X∈xs) ]) , isKestrel X y)
eliminate-SK {X = X} {y} (_⟨∙⟩_∣_ {Y} {Z} Y∈⟨S,K,y,xs⟩ [ there (there (here Z≈y)) ] YZ≈X) with strengthen-SK Y∈⟨S,K,y,xs⟩
... | just Y∈⟨S,K,xs⟩ = (Y , Y∈⟨S,K,xs⟩ , trans (congˡ (sym Z≈y)) YZ≈X)
... | nothing =
  let (Y′ , Y′∈⟨S,K,xs⟩ , Y′y≈Y) = eliminate-SK Y∈⟨S,K,y,xs⟩

      SY′Iy≈X : S ∙ Y′ ∙ I ∙ y ≈ X
      SY′Iy≈X = begin
        S ∙ Y′ ∙ I ∙ y    ≈⟨ isStarling Y′ I y ⟩
        Y′ ∙ y ∙ (I ∙ y)  ≈⟨ congʳ $ Y′y≈Y ⟩
        Y ∙ (I ∙ y)       ≈⟨ congˡ $ isIdentity y ⟩
        Y ∙ y             ≈˘⟨ congˡ Z≈y ⟩
        Y ∙ Z             ≈⟨ YZ≈X ⟩
        X                 ∎
  in (S ∙ Y′ ∙ I , [# 0 ] ⟨∙⟩ Y′∈⟨S,K,xs⟩ ⟨∙⟩ weaken-++ˡ I∈⟨S,K⟩ , SY′Iy≈X)
eliminate-SK {X = X} {y} (_⟨∙⟩_∣_ {Y} {Z} Y∈⟨S,K,y,xs⟩ Z∈⟨S,K,y,xs⟩ YZ≈X) =
  let (Y′ , Y′∈⟨S,K,xs⟩ , Y′y≈Y) = eliminate-SK Y∈⟨S,K,y,xs⟩
      (Z′ , Z′∈⟨S,K,xs⟩ , Z′y≈Z) = eliminate-SK Z∈⟨S,K,y,xs⟩

      SY′Z′y≈X : S ∙ Y′ ∙ Z′ ∙ y ≈ X
      SY′Z′y≈X = begin
        S ∙ Y′ ∙ Z′ ∙ y    ≈⟨ isStarling Y′ Z′ y ⟩
        Y′ ∙ y ∙ (Z′ ∙ y)  ≈⟨ congʳ Y′y≈Y ⟩
        Y ∙ (Z′ ∙ y)       ≈⟨ congˡ Z′y≈Z ⟩
        Y ∙ Z              ≈⟨ YZ≈X ⟩
        X                  ∎
  in (S ∙ Y′ ∙ Z′ , [# 0 ] ⟨∙⟩ Y′∈⟨S,K,xs⟩ ⟨∙⟩ Z′∈⟨S,K,xs⟩ , SY′Z′y≈X)

module _ (x y : Bird) where
  -- Example: y-eliminating the expression y should give I.
  _ : proj₁ (eliminate-SK {y = y} {xs = x ∷ []} $ [# 2 ]) ≈ I
  _ = refl

  -- Example: y-eliminating the expression x should give Kx.
  _ : proj₁ (eliminate-SK {y = y} {xs = x ∷ []} $ [# 3 ]) ≈ K ∙ x
  _ = refl

  -- Example: y-eliminating the expression xy should give x (Principle 3).
  _ : proj₁ (eliminate-SK {y = y} {xs = x ∷ []} $ [# 3 ] ⟨∙⟩ [# 2 ]) ≈ x
  _ = refl

  -- Example: y-eliminating the expression yx should give SI(Kx).
  _ : proj₁ (eliminate-SK {y = y} {xs = x ∷ []} $ [# 2 ] ⟨∙⟩ [# 3 ]) ≈ S ∙ I ∙ (K ∙ x)
  _ = refl

  -- Example: y-eliminating the expression yy should give SII.
  _ : proj₁ (eliminate-SK {y = y} {xs = x ∷ []} $ [# 2 ] ⟨∙⟩ [# 2 ]) ≈ S ∙ I ∙ I
  _ = refl

infixl 6 _∙ⁿ_
_∙ⁿ_ : ∀ {n} → (A : Bird) (xs : Vec Bird n) → Bird
A ∙ⁿ [] = A
A ∙ⁿ (x ∷ xs) = A ∙ⁿ xs ∙ x

eliminateAll′ : ∀ {n X} {xs : Vec Bird n} → X ∈ ⟨ S ∷ K ∷ xs ⟩ → ∃[ X′ ] (X′ ∈ ⟨ S ∷ K ∷ [] ⟩ × X′ ∙ⁿ xs ≈ X)
eliminateAll′ {X = X} {[]} X∈⟨S,K⟩ = (X , X∈⟨S,K⟩ , refl)
eliminateAll′ {X = X} {x ∷ xs} X∈⟨S,K,x,xs⟩ =
  let (X′ , X′∈⟨S,K,xs⟩ , X′x≈X) = eliminate-SK X∈⟨S,K,x,xs⟩
      (X″ , X″∈⟨S,K⟩ , X″xs≈X′) = eliminateAll′ X′∈⟨S,K,xs⟩

      X″∙ⁿxs∙x≈X : X″ ∙ⁿ xs ∙ x ≈ X
      X″∙ⁿxs∙x≈X = begin
        X″ ∙ⁿ xs ∙ x  ≈⟨ congʳ X″xs≈X′ ⟩
        X′ ∙ x           ≈⟨ X′x≈X ⟩
        X                ∎
  in (X″ , X″∈⟨S,K⟩ , X″∙ⁿxs∙x≈X)

-- TOOD: can we do this in some way without depending on xs : Vec Bird n?
eliminateAll : ∀ {n X} {xs : Vec Bird n} → X ∈ ⟨ xs ⟩ → ∃[ X′ ] (X′ ∈ ⟨ S ∷ K ∷ [] ⟩ × X′ ∙ⁿ xs ≈ X)
eliminateAll X∈⟨xs⟩ = eliminateAll′ $ weaken-++ʳ (S ∷ K ∷ []) X∈⟨xs⟩

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
-- Andreas, 2017-01-12, re #2386
-- Correct error message for wrong BUILTIN UNIT

data Bool : Set where
  true false : Bool

{-# BUILTIN UNIT Bool #-}

-- Error WAS:
-- The builtin UNIT must be a datatype with 1 constructors
-- when checking the pragma BUILTIN UNIT Bool

-- Expected error:
-- Builtin UNIT must be a singleton record type
-- when checking the pragma BUILTIN UNIT Bool

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import FRP.JS.Bool using ( not )
open import FRP.JS.Nat using ( ) renaming ( _≟_ to _≟n_ )
open import FRP.JS.String using ( _≟_ ; _≤_ ; _<_ ; length )
open import FRP.JS.QUnit using ( TestSuite ; ok ; test ; _,_ )

module FRP.JS.Test.String where

tests : TestSuite
tests =
  ( test "≟"
    ( ok "abc ≟ abc" ("abc" ≟ "abc")
    , ok "ε ≟ abc" (not ("" ≟ "abc"))
    , ok "a ≟ abc" (not ("a" ≟ "abc"))
    , ok "abc ≟ ABC" (not ("abc" ≟ "ABC")) )
  , test "length"
    ( ok "length ε" (length "" ≟n 0)
    , ok "length a" (length "a" ≟n 1)
    , ok "length ab" (length "ab" ≟n 2)
    , ok "length abc" (length "abc" ≟n 3)
    , ok "length \"\\\"" (length "\"\\\"" ≟n 3)
    , ok "length åäö⊢ξ∀" (length "åäö⊢ξ∀" ≟n 6)
    , ok "length ⟨line-terminators⟩" (length "\r\n\x2028\x2029" ≟n 4) )
  , test "≤"
    ( ok "abc ≤ abc" ("abc" ≤ "abc")
    , ok "abc ≤ ε" (not ("abc" ≤ ""))
    , ok "abc ≤ a" (not ("abc" ≤ "a"))
    , ok "abc ≤ ab" (not ("abc" ≤ "a"))
    , ok "abc ≤ ABC" (not ("abc" ≤ "ABC"))
    , ok "ε ≤ abc" ("" ≤ "abc")
    , ok "a ≤ abc" ("a" ≤ "abc")
    , ok "ab ≤ abc" ("a" ≤ "abc")
    , ok "ABC ≤ abc" ("ABC" ≤ "abc") )
  , test "<"
    ( ok "abc < abc" (not ("abc" < "abc"))
    , ok "abc < ε" (not ("abc" < ""))
    , ok "abc < a" (not ("abc" < "a"))
    , ok "abc < ab" (not ("abc" < "a"))
    , ok "abc < ABC" (not ("abc" < "ABC"))
    , ok "ε < abc" ("" < "abc")
    , ok "a < abc" ("a" < "abc")
    , ok "ab < abc" ("a" < "abc")
    , ok "ABC < abc" ("ABC" < "abc") ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Andreas, 2017-11-06, issue #2840 reported by wenkokke

Id : (F : Set → Set) → Set → Set
Id F = F

data D (A : Set) : Set where
  c : Id _ A

-- WAS: internal error in positivity checker

-- EXPECTED: success, or
-- The target of a constructor must be the datatype applied to its
-- parameters, _F_2 A isn't
-- when checking the constructor c in the declaration of D

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- This module proves that the context-sensitive language aⁿbⁿcⁿ can
-- be recognised
------------------------------------------------------------------------

-- This is obvious given the proof in
-- TotalRecognisers.LeftRecursion.ExpressiveStrength but the code
-- below provides a non-trivial example of the use of the parser
-- combinators.

module TotalRecognisers.LeftRecursion.NotOnlyContextFree where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool using (Bool; true; false; _∨_)
open import Function
open import Data.List as List using (List; []; _∷_; _++_; [_])
import Data.List.Properties
private
  module ListMonoid {A : Set} =
    Monoid (Data.List.Properties.++-monoid A)
open import Data.Nat as Nat using (ℕ; zero; suc; _+_)
import Data.Nat.Properties as NatProp
private
  module NatCS = CommutativeSemiring NatProp.+-*-commutativeSemiring
import Data.Nat.Solver
open Data.Nat.Solver.+-*-Solver
open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open ≡-Reasoning

import TotalRecognisers.LeftRecursion
import TotalRecognisers.LeftRecursion.Lib as Lib

------------------------------------------------------------------------
-- The alphabet

data Tok : Set where
  a b c : Tok

_≟_ : Decidable (_≡_ {A = Tok})
a ≟ a = yes refl
a ≟ b = no λ()
a ≟ c = no λ()
b ≟ a = no λ()
b ≟ b = yes refl
b ≟ c = no λ()
c ≟ a = no λ()
c ≟ b = no λ()
c ≟ c = yes refl

open TotalRecognisers.LeftRecursion Tok
open Lib Tok
private
  open module TokTok = Lib.Tok Tok _≟_ using (tok)

------------------------------------------------------------------------
-- An auxiliary definition and a boring lemma

infixr 8 _^^_

_^^_ : Tok → ℕ → List Tok
_^^_ = flip List.replicate

private

  shallow-comm : ∀ i n → i + suc n ≡ suc (i + n)
  shallow-comm i n =
    solve 2 (λ i n → i :+ (con 1 :+ n) := con 1 :+ i :+ n) refl i n

------------------------------------------------------------------------
-- Some lemmas relating _^^_, _^_ and tok

tok-^-complete : ∀ t i → t ^^ i ∈ tok t ^ i
tok-^-complete t zero    = empty
tok-^-complete t (suc i) =
  add-♭♯ ⟨ false ^ i ⟩-nullable TokTok.complete · tok-^-complete t i

tok-^-sound : ∀ t i {s} → s ∈ tok t ^ i → s ≡ t ^^ i
tok-^-sound t zero    empty     = refl
tok-^-sound t (suc i) (t∈ · s∈)
  with TokTok.sound (drop-♭♯ ⟨ false ^ i ⟩-nullable t∈)
... | refl = cong (_∷_ t) (tok-^-sound t i s∈)

------------------------------------------------------------------------
-- aⁿbⁿcⁿ

-- The context-sensitive language { aⁿbⁿcⁿ | n ∈ ℕ } can be recognised
-- using the parser combinators defined in this development.

private

  -- The two functions below are not actually mutually recursive, but
  -- are placed in a mutual block to ensure that the constraints
  -- generated by the second function can be used to instantiate the
  -- underscore in the body of the first.

  mutual

    aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index : ℕ → Bool
    aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index _ = _

    aⁿbⁱ⁺ⁿcⁱ⁺ⁿ : (i : ℕ) → P (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index i)
    aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i = cast lem (♯? (tok a) · ♯ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ (suc i))
                 ∣ tok b ^ i ⊙ tok c ^ i
      where lem = left-zero (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i))

aⁿbⁿcⁿ : P true
aⁿbⁿcⁿ = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ 0

-- Let us prove that aⁿbⁿcⁿ is correctly defined.

aⁿbⁿcⁿ-string : ℕ → List Tok
aⁿbⁿcⁿ-string n = a ^^ n ++ b ^^ n ++ c ^^ n

private

  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string : ℕ → ℕ → List Tok
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i = a ^^ n ++ b ^^ (i + n) ++ c ^^ (i + n)

aⁿbⁿcⁿ-complete : ∀ n → aⁿbⁿcⁿ-string n ∈ aⁿbⁿcⁿ
aⁿbⁿcⁿ-complete n = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete n 0
  where
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete : ∀ n i → aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i ∈ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete zero i with i + 0 | proj₂ NatCS.+-identity i
  ... | .i | refl = ∣-right {n₁ = false} (helper b · helper c)
    where
    helper = λ (t : Tok) →
      add-♭♯ ⟨ false ^ i ⟩-nullable (tok-^-complete t i)
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete (suc n) i with i + suc n | shallow-comm i n
  ... | .(suc i + n) | refl =
    ∣-left $ cast {eq = lem} (
      add-♭♯ (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) TokTok.complete ·
      aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete n (suc i))
    where lem = left-zero (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i))

aⁿbⁿcⁿ-sound : ∀ {s} → s ∈ aⁿbⁿcⁿ → ∃ λ n → s ≡ aⁿbⁿcⁿ-string n
aⁿbⁿcⁿ-sound = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound 0
  where
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound : ∀ {s} i → s ∈ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i →
                     ∃ λ n → s ≡ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound i (∣-left (cast (t∈ · s∈)))
    with TokTok.sound (drop-♭♯ (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) t∈)
  ... | refl with aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound (suc i) s∈
  ... | (n , refl) = suc n , (begin
    a ^^ suc n ++ b ^^ (suc i + n) ++ c ^^ (suc i + n)
      ≡⟨ cong (λ i → a ^^ suc n ++ b ^^ i ++ c ^^ i)
              (sym (shallow-comm i n)) ⟩
    a ^^ suc n ++ b ^^ (i + suc n) ++ c ^^ (i + suc n)
      ∎)
  aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound i (∣-right (_·_ {s₁} {s₂} s₁∈ s₂∈)) = 0 , (begin
    s₁ ++ s₂
      ≡⟨ cong₂ _++_ (tok-^-sound b i
                      (drop-♭♯ ⟨ false ^ i ⟩-nullable s₁∈))
                    (tok-^-sound c i
                      (drop-♭♯ ⟨ false ^ i ⟩-nullable s₂∈)) ⟩
    b ^^ i ++ c ^^ i
      ≡⟨ cong (λ i → b ^^ i ++ c ^^ i)
              (sym (proj₂ NatCS.+-identity i)) ⟩
    b ^^ (i + 0) ++ c ^^ (i + 0)
      ∎)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
postulate
  Nat : Set
  Fin : Nat → Set
  Finnat : Nat → Set
  fortytwo : Nat
  finnatic : Finnat fortytwo
  _==_ : Finnat fortytwo → Finnat fortytwo → Set

record Fixer : Set where
  field fix : ∀ {x} → Finnat x → Finnat fortytwo
open Fixer {{...}}

postulate
  Fixidentity : {{_ : Fixer}} → Set
  instance
    fixidentity : {{fx : Fixer}} {{fxi : Fixidentity}} {f : Finnat fortytwo} → fix f == f

  InstanceWrapper : Set
  iwrap : InstanceWrapper
  instance
    IrrFixerInstance : .InstanceWrapper → Fixer

instance
  FixerInstance : Fixer
  FixerInstance = IrrFixerInstance iwrap

instance
  postulate FixidentityInstance : Fixidentity

it : ∀ {a} {A : Set a} {{x : A}} → A
it {{x}} = x

fails : Fixer.fix FixerInstance finnatic == finnatic
fails = fixidentity

works : Fixer.fix FixerInstance finnatic == finnatic
works = fixidentity {{fx = it}}

works₂ : Fixer.fix FixerInstance finnatic == finnatic
works₂ = fixidentity {{fxi = it}}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solvers for equations over lists
------------------------------------------------------------------------

-- See README.Nat for examples of how to use similar solvers

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

module Data.List.Solver where

import Algebra.Solver.Monoid as Solver
open import Data.List.Properties using (++-monoid)

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _++_

module ++-Solver {a} {A : Set a} =
  Solver (++-monoid A) renaming (id to nil)


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Categories.Cube where

open import Cat.Prelude
open import Level
open import Data.Bool hiding (T)
open import Data.Sum hiding ([_,_])
open import Data.Unit
open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Decidable

open import Cat.Category
open import Cat.Category.Functor

-- See chapter 1 for a discussion on how presheaf categories are CwF's.

-- See section 6.8 in Huber's thesis for details on how to implement the
-- categorical version of CTT

open Category hiding (_<<<_)
open Functor

module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
  private
    -- Ns is the "namespace"
    ℓo = (suc zero ⊔ ℓ)

    FiniteDecidableSubset : Set ℓ
    FiniteDecidableSubset = Ns → Dec ⊤

    isTrue : Bool → Set
    isTrue false = ⊥
    isTrue true = ⊤

    elmsof : FiniteDecidableSubset → Set ℓ
    elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)

    𝟚 : Set
    𝟚 = Bool

    module _ (I J : FiniteDecidableSubset) where
      Hom' : Set ℓ
      Hom' = elmsof I → elmsof J ⊎ 𝟚
      isInl : {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} → A ⊎ B → Set
      isInl (inj₁ _) = ⊤
      isInl (inj₂ _) = ⊥

      Def : Set ℓ
      Def = (f : Hom') → Σ (elmsof I) (λ i → isInl (f i))

      rules : Hom' → Set ℓ
      rules f = (i j : elmsof I)
        → case (f i) of λ
          { (inj₁ (fi , _)) → case (f j) of λ
            { (inj₁ (fj , _)) → fi ≡ fj → i ≡ j
            ; (inj₂ _) → Lift _ ⊤
            }
          ; (inj₂ _) → Lift _ ⊤
          }

      Hom = Σ Hom' rules

    module Raw = RawCategory
    -- The category of names and substitutions
    Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
    Raw.Object Rawℂ = FiniteDecidableSubset
    Raw.Arrow Rawℂ = Hom
    Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
    Raw._<<<_ Rawℂ = {!!}

    postulate IsCategoryℂ : IsCategory Rawℂ

    ℂ : Category ℓ ℓ
    raw ℂ = Rawℂ
    isCategory ℂ = IsCategoryℂ

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Algebra.Magma

module Cubical.Algebra.Magma.Construct.Opposite {ℓ} (M : Magma ℓ) where

open import Cubical.Foundations.Prelude

open Magma M

_•ᵒᵖ_ : Op₂ Carrier
y •ᵒᵖ x = x • y

Op-isMagma : IsMagma Carrier _•ᵒᵖ_
Op-isMagma = record { is-set = is-set }

Mᵒᵖ : Magma ℓ
Mᵒᵖ = record { isMagma = Op-isMagma }


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Homomorphism.Setoid (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Homomorphism.Base Σ

open import Level using (Level; _⊔_)
open import Relation.Binary using (Rel; Setoid; IsEquivalence)

private
  variable
    a b ℓ₁ ℓ₂ : Level

module _
  {A : Algebra {a} {ℓ₁}}
  {B : Algebra {b} {ℓ₂}}
  where

  open Setoid ∥ B ∥/≈

  infix 4 _≗_

  _≗_ : Rel (A ⟿ B) (a ⊔ ℓ₂)
  f ≗ g = ∣ f ∣⃗ ~ ∣ g ∣⃗
    where open import Fragment.Setoid.Morphism renaming (_≗_ to _~_)

  ≗-refl : ∀ {f} → f ≗ f
  ≗-refl = refl

  ≗-sym : ∀ {f g} → f ≗ g → g ≗ f
  ≗-sym f≗g {x} = sym (f≗g {x})

  ≗-trans : ∀ {f g h} → f ≗ g → g ≗ h → f ≗ h
  ≗-trans f≗g g≗h {x} = trans (f≗g {x}) (g≗h {x})

  ≗-isEquivalence : IsEquivalence _≗_
  ≗-isEquivalence = record { refl  = λ {f} → ≗-refl {f}
                           ; sym   = λ {f g} → ≗-sym {f} {g}
                           ; trans = λ {f g h} → ≗-trans {f} {g} {h}
                           }

_⟿_/≗ : Algebra {a} {ℓ₁} → Algebra {b} {ℓ₂} → Setoid _ _
A ⟿ B /≗ = record { Carrier       = A ⟿ B
                   ; _≈_           = _≗_
                   ; isEquivalence = ≗-isEquivalence
                   }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

module Prelude where

open import Class.Equality public
open import Class.Functor public
open import Class.Monad public
open import Class.Monoid public
open import Class.Show public
open import Class.Traversable public

open import Data.Bool hiding (_≟_; _<_; _<?_; _≤_; _≤?_) public
open import Data.Bool.Instance public
open import Data.Char using (Char) public
open import Data.Char.Instance public
open import Data.Empty public
open import Data.Empty.Instance public
open import Data.Fin using (Fin) public
open import Data.List using (List; []; [_]; _∷_; drop; boolFilter; filter; head; reverse; _++_; zipWith; foldl; intersperse; map; null; span; break; allFin; length; mapMaybe; or; and) public
open import Data.List.Exts public
open import Data.List.Instance public
open import Data.Maybe using (Maybe; just; nothing; maybe; from-just; is-just; is-nothing; _<∣>_) public
open import Data.Maybe.Instance public
open import Data.Nat hiding (_+_; _≟_) public
open import Data.Nat.Instance public
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃-syntax; -,_; Σ; swap; Σ-syntax; map₁; map₂) public
open import Data.Product.Instance public
open import Data.String using (String; unwords; unlines; padRight; _<+>_) public
open import Data.String.Exts public
open import Data.String.Instance public
open import Data.Sum using (_⊎_; inj₁; inj₂; from-inj₁; from-inj₂) public
open import Data.Sum.Instance public
open import Data.Unit.Instance public
open import Data.Unit.Polymorphic using (⊤; tt) public
open import IO using (IO; putStr) public
open import IO.Finite using (getLine) public
open import IO.Exts public
open import IO.Instance public
open import System.Environment public
open import System.Exit public

open import Function public

open import Relation.Nullary using (Dec; yes; no) public
open import Relation.Nullary.Decidable using (⌊_⌋) public
open import Relation.Nullary.Negation public
open import Relation.Unary using (Decidable) public
open import Relation.Binary.PropositionalEquality using (_≡_; refl) public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for types of functions
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

-- Note that these bundles differ from those found elsewhere in other
-- library hierarchies as they take Setoids as parameters. This is
-- because a function is of no use without knowing what its domain and
-- codomain is, as well which equalities are being considered over them.
-- One consequence of this is that they are not built from the
-- definitions found in `Function.Structures` as is usually the case in
-- other library hierarchies, as this would duplicate the equality
-- axioms.

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

module Function.Bundles where

import Function.Definitions as FunctionDefinitions
import Function.Structures as FunctionStructures
open import Level using (Level; _⊔_; suc)
open import Data.Product using (proj₁; proj₂)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as ≡
  using (_≡_)
open Setoid using (isEquivalence)

private
  variable
    a b ℓ₁ ℓ₂ : Level

------------------------------------------------------------------------
-- Setoid bundles

module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where

  open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_)
  open Setoid To   using () renaming (Carrier to B; _≈_ to _≈₂_)
  open FunctionDefinitions _≈₁_ _≈₂_
  open FunctionStructures  _≈₁_ _≈₂_

  record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f           : A → B
      cong        : f Preserves _≈₁_ ⟶ _≈₂_
      injective   : Injective f

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)

    isInjection : IsInjection f
    isInjection = record
      { isCongruent = isCongruent
      ; injective   = injective
      }

  record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f          : A → B
      cong       : f Preserves _≈₁_ ⟶ _≈₂_
      surjective : Surjective f

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)

    isSurjection : IsSurjection f
    isSurjection = record
      { isCongruent = isCongruent
      ; surjective  = surjective
      }

  record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      cong      : f Preserves _≈₁_ ⟶ _≈₂_
      bijective : Bijective f

    injective : Injective f
    injective = proj₁ bijective

    surjective : Surjective f
    surjective = proj₂ bijective

    injection : Injection
    injection = record
      { cong      = cong
      ; injective = injective
      }

    surjection : Surjection
    surjection = record
      { cong       = cong
      ; surjective = surjective
      }

    open Injection  injection  public using (isInjection)
    open Surjection surjection public using (isSurjection)

    isBijection : IsBijection f
    isBijection = record
      { isInjection = isInjection
      ; surjective  = surjective
      }

    open IsBijection isBijection public using (module Eq₁; module Eq₂)

  record Equivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f     : A → B
      g     : B → A
      cong₁ : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂ : g Preserves _≈₂_ ⟶ _≈₁_

  record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      g         : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : g Preserves _≈₂_ ⟶ _≈₁_
      inverseˡ  : Inverseˡ f g

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong₁
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)

    isLeftInverse : IsLeftInverse f g
    isLeftInverse = record
      { isCongruent = isCongruent
      ; cong₂       = cong₂
      ; inverseˡ    = inverseˡ
      }

    equivalence : Equivalence
    equivalence = record
      { cong₁ = cong₁
      ; cong₂ = cong₂
      }

  record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      g         : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : g Preserves _≈₂_ ⟶ _≈₁_
      inverseʳ  : Inverseʳ f g

    isCongruent : IsCongruent f
    isCongruent = record
      { cong           = cong₁
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    isRightInverse : IsRightInverse f g
    isRightInverse = record
      { isCongruent = isCongruent
      ; cong₂       = cong₂
      ; inverseʳ    = inverseʳ
      }

    equivalence : Equivalence
    equivalence = record
      { cong₁ = cong₁
      ; cong₂ = cong₂
      }

  record BiEquivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f     : A → B
      g₁    : B → A
      g₂    : B → A
      cong₁ : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂ : g₁ Preserves _≈₂_ ⟶ _≈₁_
      cong₃ : g₂ Preserves _≈₂_ ⟶ _≈₁_

  record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      g₁        : B → A
      g₂        : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : g₁ Preserves _≈₂_ ⟶ _≈₁_
      cong₃     : g₂ Preserves _≈₂_ ⟶ _≈₁_
      inverseˡ  : Inverseˡ f g₁
      inverseʳ  : Inverseʳ f g₂

    f-isCongruent : IsCongruent f
    f-isCongruent = record
      { cong           = cong₁
      ; isEquivalence₁ = isEquivalence From
      ; isEquivalence₂ = isEquivalence To
      }

    isBiInverse : IsBiInverse f g₁ g₂
    isBiInverse = record
      { f-isCongruent = f-isCongruent
      ; cong₂         = cong₂
      ; inverseˡ      = inverseˡ
      ; cong₃         = cong₃
      ; inverseʳ      = inverseʳ
      }

    biEquivalence : BiEquivalence
    biEquivalence = record
      { cong₁ = cong₁
      ; cong₂ = cong₂
      ; cong₃ = cong₃
      }

  record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      f         : A → B
      f⁻¹       : B → A
      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
      cong₂     : f⁻¹ Preserves _≈₂_ ⟶ _≈₁_
      inverse   : Inverseᵇ f f⁻¹

    inverseˡ : Inverseˡ f f⁻¹
    inverseˡ = proj₁ inverse

    inverseʳ : Inverseʳ f f⁻¹
    inverseʳ = proj₂ inverse

    leftInverse : LeftInverse
    leftInverse = record
      { cong₁    = cong₁
      ; cong₂    = cong₂
      ; inverseˡ = inverseˡ
      }

    rightInverse : RightInverse
    rightInverse = record
      { cong₁    = cong₁
      ; cong₂    = cong₂
      ; inverseʳ = inverseʳ
      }

    open LeftInverse leftInverse   public using (isLeftInverse)
    open RightInverse rightInverse public using (isRightInverse)

    isInverse : IsInverse f f⁻¹
    isInverse = record
      { isLeftInverse = isLeftInverse
      ; inverseʳ      = inverseʳ
      }

    open IsInverse isInverse public using (module Eq₁; module Eq₂)

------------------------------------------------------------------------
-- Bundles specialised for propositional equality

infix 3 _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_

_↣_ : Set a → Set b → Set _
A ↣ B = Injection (≡.setoid A) (≡.setoid B)

_↠_ : Set a → Set b → Set _
A ↠ B = Surjection (≡.setoid A) (≡.setoid B)

_⤖_ : Set a → Set b → Set _
A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)

_⇔_ : Set a → Set b → Set _
A ⇔ B = Equivalence (≡.setoid A) (≡.setoid B)

_↩_ : Set a → Set b → Set _
A ↩ B = LeftInverse (≡.setoid A) (≡.setoid B)

_↪_ : Set a → Set b → Set _
A ↪ B = RightInverse (≡.setoid A) (≡.setoid B)

_↩↪_ : Set a → Set b → Set _
A ↩↪ B = BiInverse (≡.setoid A) (≡.setoid B)

_↔_ : Set a → Set b → Set _
A ↔ B = Inverse (≡.setoid A) (≡.setoid B)

-- We now define some constructors for the above that
-- automatically provide the required congruency proofs.

module _ {A : Set a} {B : Set b} where

  open FunctionDefinitions {A = A} {B} _≡_ _≡_

  mk↣ : ∀ {f : A → B} → Injective f → A ↣ B
  mk↣ {f} inj = record
    { f         = f
    ; cong      = ≡.cong f
    ; injective = inj
    }

  mk↠ : ∀ {f : A → B} → Surjective f → A ↠ B
  mk↠ {f} surj = record
    { f          = f
    ; cong       = ≡.cong f
    ; surjective = surj
    }

  mk⤖ : ∀ {f : A → B} → Bijective f → A ⤖ B
  mk⤖ {f} bij = record
    { f         = f
    ; cong      = ≡.cong f
    ; bijective = bij
    }

  mk⇔ : ∀ (f : A → B) (g : B → A) → A ⇔ B
  mk⇔ f g = record
    { f     = f
    ; g     = g
    ; cong₁ = ≡.cong f
    ; cong₂ = ≡.cong g
    }

  mk↩ : ∀ {f : A → B} {g : B → A} → Inverseˡ f g → A ↩ B
  mk↩ {f} {g} invˡ = record
    { f        = f
    ; g        = g
    ; cong₁    = ≡.cong f
    ; cong₂    = ≡.cong g
    ; inverseˡ = invˡ
    }

  mk↪ : ∀ {f : A → B} {g : B → A} → Inverseʳ f g → A ↪ B
  mk↪ {f} {g} invʳ = record
    { f        = f
    ; g        = g
    ; cong₁    = ≡.cong f
    ; cong₂    = ≡.cong g
    ; inverseʳ = invʳ
    }

  mk↩↪ : ∀ {f : A → B} {g₁ : B → A} {g₂ : B → A}
    → Inverseˡ f g₁ → Inverseʳ f g₂ → A ↩↪ B
  mk↩↪ {f} {g₁} {g₂} invˡ invʳ = record
    { f        = f
    ; g₁       = g₁
    ; g₂       = g₂
    ; cong₁    = ≡.cong f
    ; cong₂    = ≡.cong g₁
    ; cong₃    = ≡.cong g₂
    ; inverseˡ = invˡ
    ; inverseʳ = invʳ
    }

  mk↔ : ∀ {f : A → B} {f⁻¹ : B → A} → Inverseᵇ f f⁻¹ → A ↔ B
  mk↔ {f} {f⁻¹} inv = record
    { f       = f
    ; f⁻¹     = f⁻¹
    ; cong₁   = ≡.cong f
    ; cong₂   = ≡.cong f⁻¹
    ; inverse = inv
    }


text:
module NF.Product where

open import NF
open import Data.Product
open import Relation.Binary.PropositionalEquality

instance
  nf, : {A : Set}{B : A -> Set}{a : A}{b : B a}{{nfa : NF a}}{{nfb : NF b}} -> NF {Σ A B} (a , b)
  Sing.unpack (NF.!! (nf, {B = B} {a = a} {b = b} {{nfa}})) = nf a , subst B (sym nf≡) (nf b)
  Sing.eq (NF.!! (nf, {{nfa}} {{nfb}})) rewrite nf≡ {{nfa}} | nf≡ {{nfb}} = refl

  {-# INLINE nf, #-}

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
module Tactic.Nat.Coprime.Decide where

open import Prelude
open import Prelude.Equality.Unsafe
open import Prelude.List.Relations.Any
open import Prelude.List.Relations.All
open import Prelude.List.Relations.Properties

open import Numeric.Nat
open import Tactic.Nat.Coprime.Problem

private
  infix 4 _isIn_
  _isIn_ : Nat → Exp → Bool
  x isIn atom y = isYes (x == y)
  x isIn a ⊗ b = x isIn a || x isIn b

  proves : Nat → Nat → Formula → Bool
  proves x y (a ⋈ b) = x isIn a && y isIn b || x isIn b && y isIn a

  hypothesis : Nat → Nat → List Formula → Bool
  hypothesis x y Γ = any? (proves x y) Γ

  canProve' : List Formula → Exp → Exp → Bool
  canProve' Γ (atom x) (atom y) = hypothesis x y Γ
  canProve' Γ a (b ⊗ c) = canProve' Γ a b && canProve' Γ a c
  canProve' Γ (a ⊗ b) c = canProve' Γ a c && canProve' Γ b c

canProve : Problem → Bool
canProve (Γ ⊨ a ⋈ b) = canProve' Γ a b

-- Soundness proof --

private
  invert-&&₁ : ∀ {a b} → (a && b) ≡ true → a ≡ true
  invert-&&₁ {false} ()
  invert-&&₁ {true}  prf = refl

  invert-&&₂ : ∀ {a b} → (a && b) ≡ true → b ≡ true
  invert-&&₂ {false} ()
  invert-&&₂ {true} prf = prf

  invert-|| : ∀ a {b} → (a || b) ≡ true → Either (a ≡ true) (b ≡ true)
  invert-|| false prf = right prf
  invert-|| true  prf = left prf

  sound-eq : (a b : Nat) → isYes (a == b) ≡ true → a ≡ b
  sound-eq a b ok with a == b
  sound-eq a b ok | yes a=b = a=b
  sound-eq a b () | no _

  sound-any : ∀ {A : Set} (p : A → Bool) xs → any? p xs ≡ true → Any (λ x → p x ≡ true) xs
  sound-any p [] ()
  sound-any p (x ∷ xs) ok with p x | graphAt p x
  ... | false | _          = suc (sound-any p xs ok)
  ... | true  | ingraph eq = zero eq

private
  syntax WithHyps Γ (λ ρ → A) = ρ ∈ Γ ⇒ A
  WithHyps : List Formula → (Env → Set) → Set
  WithHyps Γ F = ∀ ρ → All (⟦_⟧f ρ) Γ → F ρ

  sound-isIn' : ∀ x y a b → (x isIn a) ≡ true → (y isIn b) ≡ true → ∀ ρ → ⟦ a ⋈ b ⟧f ρ → Coprime (ρ x) (ρ y)

  sound-isIn-⊗-l : ∀ x y a b c → (x isIn a) ≡ true → (y isIn b ⊗ c) ≡ true →
                                 ∀ ρ → ⟦ a ⋈ b ⊗ c ⟧f ρ → Coprime (ρ x) (ρ y)
  sound-isIn-⊗-l x y a b c oka okbc ρ H =
    case invert-|| (y isIn b) okbc of λ where
      (left okb)  → sound-isIn' x y a b oka okb ρ (mul-coprime-l (⟦ a ⟧e ρ) (⟦ b ⟧e ρ) (⟦ c ⟧e ρ) H)
      (right okc) → sound-isIn' x y a c oka okc ρ (mul-coprime-r (⟦ a ⟧e ρ) (⟦ b ⟧e ρ) (⟦ c ⟧e ρ) H)

  sound-isIn' x y (atom x') (atom y') oka okb ρ H =
    case₂ sound-eq x x' oka , sound-eq y y' okb of λ where
      refl refl → H
  sound-isIn' x y a@(atom _) (b ⊗ c) oka okbc ρ H = sound-isIn-⊗-l x y a b c oka okbc ρ H
  sound-isIn' x y a@(_ ⊗ _) (b ⊗ c) oka okbc ρ H = sound-isIn-⊗-l x y a b c oka okbc ρ H
  sound-isIn' x y (a ⊗ b) c@(atom _) okab okc ρ H =
    let nf = λ e → ⟦ e ⟧e ρ
        H' = coprime-sym _ (nf c) H
    in
    case invert-|| (x isIn a) okab of λ where
      (left  oka) → sound-isIn' x y a c oka okc ρ
                      (coprime-sym (nf c) _
                        (mul-coprime-l (nf c) (nf a) (nf b) H'))
      (right okb) → sound-isIn' x y b c okb okc ρ
                      (coprime-sym (nf c) _
                        (mul-coprime-r (nf c) (nf a) _ H'))

  sound-isIn : ∀ x y a b → (x isIn a && y isIn b) ≡ true → ∀ ρ → ⟦ a ⋈ b ⟧f ρ → Coprime (ρ x) (ρ y)
  sound-isIn x y a b ok = sound-isIn' x y a b (invert-&&₁ ok) (invert-&&₂ ok)

  sound-proves : ∀ x y φ → proves x y φ ≡ true → ∀ ρ → ⟦ φ ⟧f ρ → Coprime (ρ x) (ρ y)
  sound-proves x y (a ⋈ b) ok ρ H =
    case invert-|| (x isIn a && y isIn b) ok of λ where
      (left  ok) → sound-isIn x y a b ok ρ H
      (right ok) → sound-isIn x y b a ok ρ (coprime-sym (⟦ a ⟧e ρ) _ H)

  sound-hyp : ∀ x y Γ → hypothesis x y Γ ≡ true → ρ ∈ Γ ⇒ Coprime (ρ x) (ρ y)
  sound-hyp x y Γ ok ρ Ξ =
    case lookupAny Ξ (sound-any (proves x y) Γ ok) of λ where
      (φ , H , okφ) → sound-proves x y φ okφ ρ H

  sound' : ∀ Γ a b → canProve' Γ a b ≡ true → ρ ∈ Γ ⇒ ⟦ a ⋈ b ⟧f ρ

  sound-⊗-r : ∀ Γ a b c → (canProve' Γ a b && canProve' Γ a c) ≡ true → ρ ∈ Γ ⇒ ⟦ a ⋈ b ⊗ c ⟧f ρ
  sound-⊗-r Γ a b c ok ρ Ξ =
    let a⋈b : ⟦ a ⋈ b ⟧f ρ
        a⋈b = sound' Γ a b (invert-&&₁ ok) ρ Ξ
        a⋈c : ⟦ a ⋈ c ⟧f ρ
        a⋈c = sound' Γ a c (invert-&&₂ ok) ρ Ξ
    in coprime-mul-r (⟦ a ⟧e ρ) _ _ a⋈b a⋈c

  sound' Γ (atom x) (atom y) ok ρ Ξ = sound-hyp x y Γ ok ρ Ξ
  sound' Γ a@(atom _) (b ⊗ c) ok ρ Ξ = sound-⊗-r Γ a b c ok ρ Ξ
  sound' Γ a@(_ ⊗ _) (b ⊗ c) ok ρ Ξ = sound-⊗-r Γ a b c ok ρ Ξ
  sound' Γ (a ⊗ b) c@(atom _) ok ρ Ξ =
    let a⋈c : ⟦ a ⋈ c ⟧f ρ
        a⋈c = sound' Γ a c (invert-&&₁ ok) ρ Ξ
        b⋈c : ⟦ b ⋈ c ⟧f ρ
        b⋈c = sound' Γ b c (invert-&&₂ ok) ρ Ξ
    in coprime-mul-l (⟦ a ⟧e ρ) _ _ a⋈c b⋈c

sound : ∀ Q → canProve Q ≡ true → ∀ ρ → ⟦ Q ⟧p ρ
sound Q@(Γ ⊨ a ⋈ b) ok ρ = curryProblem Q ρ (sound' Γ a b ok ρ)

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module Network.Primitive where

open import Data.Nat
open import Data.String
open import Data.Unit
open import Foreign.Haskell
open import IO.Primitive

postulate
  withSocketsDo : ∀ {a} {A : Set a} → IO A → IO A
  connectTo     : String → Integer → IO Handle

{-# IMPORT Network #-}
{-# IMPORT Text.Read #-}
{-# COMPILED withSocketsDo (\_ _ -> Network.withSocketsDo) #-}
{-# COMPILED connectTo (\s i -> Network.connectTo s $ Network.PortNumber (fromIntegral i)) #-}

max_stars_repo_name: ilya-fiveisky/agda-network

max_issues_repo_name: ilya-fiveisky/agda-network

max_forks_repo_name: ilya-fiveisky/agda-network


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

module results-checks where
  Coerce-preservation : ∀{Δ Σ' r v τ} →
                          Δ , Σ' ⊢ r ·: τ →
                          Coerce r := v →
                          Σ' ⊢ v ::ⱽ τ
  Coerce-preservation (TAFix x x₁) ()
  Coerce-preservation (TAApp ta-r ta-r₁) ()
  Coerce-preservation TAUnit CoerceUnit = TSVUnit
  Coerce-preservation (TAPair ta-r1 ta-r2) (CoercePair c-r1 c-r2)
    = TSVPair (Coerce-preservation ta-r1 c-r1) (Coerce-preservation ta-r2 c-r2)
  Coerce-preservation (TAFst ta-r) ()
  Coerce-preservation (TASnd ta-r) ()
  Coerce-preservation (TACtor h1 h2 ta-r) (CoerceCtor c-r)
    = TSVCtor h1 h2 (Coerce-preservation ta-r c-r)
  Coerce-preservation (TACase x x₁ ta-r x₂ x₃) ()
  Coerce-preservation (TAHole x x₁) ()

  {- TODO : We should revive this - it's a good sanity check.
            Of course, we have to decide what version of "complete" we want to use
            for results
  -- all complete finals (that type-check) are values
  mutual
    complete-finals-values : ∀{Δ Σ' r τ} →
                               Δ , Σ' ⊢ r ·: τ →
                               r rcomplete →
                               r final →
                               r value
    complete-finals-values (TALam Γ⊢E _) (RCLam E-cmp e-cmp) (FLam E-fin) =
      VLam (env-complete-final-values Γ⊢E E-cmp E-fin) e-cmp
    complete-finals-values (TAFix Γ⊢E _) (RCFix E-cmp e-cmp) (FFix E-fin) =
      VFix (env-complete-final-values Γ⊢E E-cmp E-fin) e-cmp
    complete-finals-values (TAApp ta1 ta2) (RCAp cmp1 cmp2) (FAp fin1 fin2 h1 h2)
      with complete-finals-values ta1 cmp1 fin1
    complete-finals-values (TAApp ta1 ta2) (RCAp cmp1 cmp2) (FAp fin1 fin2 h1 h2) | VLam _ _ = abort (h1 refl)
    complete-finals-values (TAApp ta1 ta2) (RCAp cmp1 cmp2) (FAp fin1 fin2 h1 h2) | VFix _ _ = abort (h2 refl)
    complete-finals-values (TAApp () ta2) (RCAp cmp1 cmp2) (FAp fin1 fin2 h1 h2)  | VTpl _
    complete-finals-values (TAApp () ta2) (RCAp cmp1 cmp2) (FAp fin1 fin2 h1 h2)  | VCon _
    complete-finals-values (TAApp ta1 ta2) (RCAp cmp1 cmp2) (FAp fin1 fin2 h1 h2) | VPF _ = {!!}
    complete-finals-values (TATpl ∥rs⊫=∥τs∥ ta) (RCTpl h1) (FTpl h2) =
      VTpl λ {i} i<∥rs∥ → complete-finals-values (ta i<∥rs∥ (tr (λ y → i < y) ∥rs⊫=∥τs∥ i<∥rs∥)) (h1 i<∥rs∥) (h2 i<∥rs∥)
    complete-finals-values (TAGet i<∥τs∥ ta) (RCGet cmp) (FGet fin x) = {!!}
    complete-finals-values (TACtor _ _ ta) (RCCtor cmp) (FCon fin) =
      VCon (complete-finals-values ta cmp fin)
    complete-finals-values (TACase x x₁ ta x₂ x₃) (RCCase x₄ cmp x₅) (FCase fin x₆ x₇) = {!!}
    complete-finals-values (TAHole _ _) () fin
    complete-finals-values (TAPF x) (RCPF x₁) (FPF x₂) = {!!}

    env-complete-final-values : ∀{Δ Σ' Γ E} →
                                  Δ , Σ' , Γ ⊢ E →
                                  E env-complete →
                                  E env-final →
                                  E env-values
    env-complete-final-values ta (ENVC E-cmp) (EF E-fin) =
      EF (λ rx∈E → complete-finals-values (π2 (π2 (env-all-E ta rx∈E))) (E-cmp rx∈E) (E-fin rx∈E))
  -}

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
module Nats.Add.Invert where

open import Equality
open import Nats
open import Nats.Add.Comm
open import Function

------------------------------------------------------------------------
-- internal stuffs

private

  lemma′ : ∀ a b → (suc a ≡ suc b) → (a ≡ b)
  lemma′ _ _ refl = refl

  lemma : ∀ a b → (suc (a + suc a) ≡ suc (b + suc b)) → (a + a ≡ b + b)
  lemma a b
    rewrite nat-add-comm a $ suc a
          | nat-add-comm b $ suc b
            = lemma′ (a + a) (b + b) ∘ lemma′ (suc $ a + a) (suc $ b + b)

  +-invert : ∀ a b → (a + a ≡ b + b) → a ≡ b
  +-invert zero zero ev = refl
  +-invert zero (suc b) ()
  +-invert (suc a) zero ()
  +-invert (suc a) (suc b) = cong suc ∘ +-invert a b ∘ lemma a b

------------------------------------------------------------------------
-- public aliases

nat-add-invert : ∀ a b → (a + a ≡ b + b) → a ≡ b
nat-add-invert = +-invert

nat-add-invert-1 : ∀ a b → (suc a ≡ suc b) → (a ≡ b)
nat-add-invert-1 = lemma′


text:
-- Minimal propositional logic, vector-based de Bruijn approach, initial encoding

module Vi.Mp where

open import Lib using (Nat; suc; _+_; Fin; fin; Vec; _,_; proj; VMem; mem)

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Nat -> Set
Cx n = Vec Ty n

isTrue : forall {tn} -> Ty -> Fin tn -> Cx tn -> Set
isTrue a i tc = VMem a i tc

-- Terms

module Mp where
  infixl 1 _$_
  infixr 0 lam=>_
  data Tm {tn} (tc : Cx tn) : Ty -> Set where
    var    : forall {a i}   -> isTrue a i tc             -> Tm tc a
    lam=>_ : forall {a b}   -> Tm (tc , a) b             -> Tm tc (a => b)
    _$_    : forall {a b}   -> Tm tc (a => b) -> Tm tc a -> Tm tc b
    pair'  : forall {a b}   -> Tm tc a        -> Tm tc b -> Tm tc (a && b)
    fst    : forall {a b}   -> Tm tc (a && b)            -> Tm tc a
    snd    : forall {a b}   -> Tm tc (a && b)            -> Tm tc b
    left   : forall {a b}   -> Tm tc a                   -> Tm tc (a || b)
    right  : forall {a b}   -> Tm tc b                   -> Tm tc (a || b)
    case'  : forall {a b c} -> Tm tc (a || b) -> Tm (tc , a) c -> Tm (tc , b) c -> Tm tc c

  syntax pair' x y    = [ x , y ]
  syntax case' xy x y = case xy => x => y

  v : forall {tn} (k : Nat) {tc : Cx (suc (k + tn))} -> Tm tc (proj tc (fin k))
  v i = var (mem i)

  Thm : Ty -> Set
  Thm a = forall {tn} {tc : Cx tn} -> Tm tc a
open Mp public

-- Example theorems

c1 : forall {a b} -> Thm (a && b <=> b && a)
c1 =
  [ lam=> [ snd (v 0) , fst (v 0) ]
  , lam=> [ snd (v 0) , fst (v 0) ]
  ]

c2 : forall {a b} -> Thm (a || b <=> b || a)
c2 =
  [ lam=>
      (case v 0
        => right (v 0)
        => left  (v 0))
  , lam=>
      (case v 0
        => right (v 0)
        => left  (v 0))
  ]

i1 : forall {a} -> Thm (a && a <=> a)
i1 =
  [ lam=> fst (v 0)
  , lam=> [ v 0 , v 0 ]
  ]

i2 : forall {a} -> Thm (a || a <=> a)
i2 =
  [ lam=>
      (case v 0
        => v 0
        => v 0)
  , lam=> left (v 0)
  ]

l3 : forall {a} -> Thm ((a => a) <=> TRUE)
l3 =
  [ lam=> lam=> v 0
  , lam=> lam=> v 0
  ]

l1 : forall {a b c} -> Thm (a && (b && c) <=> (a && b) && c)
l1 =
  [ lam=>
      [ [ fst (v 0) , fst (snd (v 0)) ]
      , snd (snd (v 0))
      ]
  , lam=>
      [ fst (fst (v 0))
      , [ snd (fst (v 0)) , snd (v 0) ]
      ]
  ]

l2 : forall {a} -> Thm (a && TRUE <=> a)
l2 =
  [ lam=> fst (v 0)
  , lam=> [ v 0 , lam=> v 0 ]
  ]

l4 : forall {a b c} -> Thm (a && (b || c) <=> (a && b) || (a && c))
l4 =
  [ lam=>
      (case snd (v 0)
        => left  [ fst (v 1) , v 0 ]
        => right [ fst (v 1) , v 0 ])
  , lam=>
      (case v 0
        => [ fst (v 0) , left  (snd (v 0)) ]
        => [ fst (v 0) , right (snd (v 0)) ])
  ]

l6 : forall {a b c} -> Thm (a || (b && c) <=> (a || b) && (a || c))
l6 =
  [ lam=>
      (case v 0
        => [ left  (v 0)       , left  (v 0) ]
        => [ right (fst (v 0)) , right (snd (v 0)) ])
  , lam=>
      (case fst (v 0)
        => left (v 0)
        =>
          case snd (v 1)
            => left  (v 0)
            => right [ v 1 , v 0 ])
  ]

l7 : forall {a} -> Thm (a || TRUE <=> TRUE)
l7 =
  [ lam=> lam=> v 0
  , lam=> right (v 0)
  ]

l9 : forall {a b c} -> Thm (a || (b || c) <=> (a || b) || c)
l9 =
  [ lam=>
      (case v 0
        => left (left (v 0))
        =>
          case v 0
            => left  (right (v 0))
            => right (v 0))
  , lam=>
      (case v 0
        =>
          case v 0
            => left  (v 0)
            => right (left (v 0))
        => right (right (v 0)))
  ]

l11 : forall {a b c} -> Thm ((a => (b && c)) <=> (a => b) && (a => c))
l11 =
  [ lam=>
      [ lam=> fst (v 1 $ v 0)
      , lam=> snd (v 1 $ v 0)
      ]
  , lam=>
      lam=> [ fst (v 1) $ v 0 , snd (v 1) $ v 0 ]
  ]

l12 : forall {a} -> Thm ((a => TRUE) <=> TRUE)
l12 =
  [ lam=> lam=> v 0
  , lam=> lam=> v 1
  ]

l13 : forall {a b c} -> Thm ((a => (b => c)) <=> ((a && b) => c))
l13 =
  [ lam=>
      lam=> v 1 $ fst (v 0) $ snd (v 0)
  , lam=>
      lam=>
        lam=> v 2 $ [ v 1 , v 0 ]
  ]

l16 : forall {a b c} -> Thm (((a && b) => c) <=> (a => (b => c)))
l16 =
  [ lam=>
      lam=>
        lam=> v 2 $ [ v 1 , v 0 ]
  , lam=>
      lam=> v 1 $ fst (v 0) $ snd (v 0)
  ]

l17 : forall {a} -> Thm ((TRUE => a) <=> a)
l17 =
  [ lam=> v 0 $ (lam=> v 0)
  , lam=> lam=> v 1
  ]

l19 : forall {a b c} -> Thm (((a || b) => c) <=> (a => c) && (b => c))
l19 =
  [ lam=>
      [ lam=> v 1 $ left  (v 0)
      , lam=> v 1 $ right (v 0)
      ]
  , lam=>
      lam=>
        (case v 0
          => fst (v 2) $ (v 0)
          => snd (v 2) $ (v 0))
  ]

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Auto-EqualityReasoning where

-- equality reasoning, computation and induction

open import Auto.Prelude

module AdditionCommutative where

 lemma : ∀ n m → (n + succ m) ≡ succ (n + m)
 lemma n m = {!-c!}  -- h0
{-
 lemma zero m = refl
 lemma (succ x) m = cong succ (lemma x m)
-}

 lemma' : ∀ n m → (n + succ m) ≡ succ (n + m)
 lemma' zero m = refl
 lemma' (succ n) m = cong succ (lemma' n m)

 addcommut : ∀ n m → (n + m) ≡ (m + n)
 addcommut n m = {!-c lemma'!}  -- h1
{-
 addcommut zero zero = refl
 addcommut zero (succ x) = sym (cong succ (addcommut x zero))  -- solution does not pass termination check
 addcommut (succ x) m = begin (succ (x + m) ≡⟨ cong succ (addcommut x m) ⟩ (succ (m + x) ≡⟨ sym (lemma' m x) ⟩ ((m + succ x) ∎)))
-}


text:
open import Category

module Iso (ℂ : Cat) where

private open module C = Cat (η-Cat ℂ)

data _≅_ (A B : Obj) : Set where
  iso : (i : A ─→ B)(j : B ─→ A) ->
	i ∘ j == id -> j ∘ i == id ->
	A ≅ B

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Tactic.Nat.Refute where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection

open import Tactic.Nat.Reflect
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Tactic.Nat.Auto
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Simpl

data Impossible : Set where

invalidEquation : ⊤
invalidEquation = _

refutation : ∀ {a} {A : Set a} {Atom : Set} {{_ : Eq Atom}} {{_ : Ord Atom}} eq (ρ : Env Atom) →
               ¬ CancelEq eq ρ → ExpEq eq ρ → A
refutation exp ρ !eq eq = ⊥-elim (!eq (complicateEq exp ρ eq))

refute-tactic : Term → TC Term
refute-tactic prf =
  inferType prf >>= λ a →
  caseM termToEq a of λ
  { nothing → pure $ failedProof (quote invalidEquation) a
  ; (just (eqn , Γ)) → pure $
    def (quote refutation)
        $ vArg (` eqn)
        ∷ vArg (quotedEnv Γ)
        ∷ vArg absurd-lam
        ∷ vArg prf ∷ []
  }

macro
  refute : Term → Tactic
  refute prf hole = unify hole =<< refute-tactic prf

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- Up-to techniques for CCS
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.Up-to.CCS {ℓ} {Name : Type ℓ} where

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

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)

open import Bisimilarity.CCS
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Indexed-container
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity CCS
open import Bisimilarity.Step CCS _[_]⟶_ using (Step; Step↔StepC)
open import Bisimilarity.Up-to CCS

-- Up to context for a very simple kind of context.

Up-to-! : Trans₂ ℓ (Proc ∞)
Up-to-! R (P , Q) =
  ∃ λ P′ → ∃ λ Q′ → P ≡ ! P′ × R (P′ , Q′) × ! Q′ ≡ Q

-- This transformer is size-preserving.

up-to-!-size-preserving : Size-preserving Up-to-!
up-to-!-size-preserving R⊆∼i (P′ , Q′ , refl , P′RQ′ , refl) =
  !-cong (R⊆∼i P′RQ′)

-- Up to context for CCS (for polyadic contexts).

Up-to-context : Trans₂ ℓ (Proc ∞)
Up-to-context R (P , Q) =
  ∃ λ n →
  ∃ λ (C : Context ∞ n) →
  ∃ λ Ps →
  ∃ λ Qs →
  Equal ∞ P (C [ Ps ])
    ×
  Equal ∞ Q (C [ Qs ])
    ×
  ∀ x → R (Ps x , Qs x)

-- Up to context is monotone.

up-to-context-monotone : Monotone Up-to-context
up-to-context-monotone R⊆S =
  Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id
    (R⊆S ∘_)

-- Up to context is size-preserving.

up-to-context-size-preserving : Size-preserving Up-to-context
up-to-context-size-preserving
  R⊆∼i {P , Q} (_ , C , Ps , Qs , eq₁ , eq₂ , Ps∼Qs) =
    P         ∼⟨ ≡→∼ eq₁ ⟩
    C [ Ps ]  ∼⟨ C [ R⊆∼i ∘ Ps∼Qs ]-cong ⟩
    C [ Qs ]  ∼⟨ symmetric (≡→∼ eq₂) ⟩■
    Q

-- Note that up to context is not compatible (assuming that Name is
-- inhabited).
--
-- This counterexample is a minor variant of one due to Pous and
-- Sangiorgi, who state that up to context would have been compatible
-- if the Step function had been defined in a slightly different way
-- (see Remark 6.4.2 in "Enhancements of the bisimulation proof
-- method").

¬-up-to-context-compatible : Name → ¬ Compatible Up-to-context
¬-up-to-context-compatible x comp = contradiction
  where
  a = x , true
  b = x , false
  c = a
  d = a

  a≢b : ¬ a ≡ b
  a≢b ()

  data R : Rel₂ ℓ (Proc ∞) where
    base : R (! name a ∙ (b ∙) , ! name a ∙ (c ∙))

  data S₀ : Rel₂ ℓ (Proc ∞) where
    base : S₀ (! name a ∙ (b ∙) ∣ b ∙ , ! name a ∙ (c ∙) ∣ c ∙)

  S : Rel₂ ℓ (Proc ∞)
  S = Up-to-bisimilarity S₀

  d!ab[R]d!ac : Up-to-context R ( name d ∙ (! name a ∙ (b ∙))
                                , name d ∙ (! name a ∙ (c ∙))
                                )
  d!ab[R]d!ac =
      1
    , name d · (λ { .force → hole fzero })
    , (λ _ → ! name a ∙ (b ∙))
    , (λ _ → ! name a ∙ (c ∙))
    , refl · (λ { .force → Proc-refl _ })
    , refl · (λ { .force → Proc-refl _ })
    , (λ _ → base)

  ¬!ab[S]!ac : ¬ Up-to-context S (! name a ∙ (b ∙) , ! name a ∙ (c ∙))
  ¬!ab[S]!ac (n , C , Ps , Qs , !ab≡C[Ps] , !ac≡C[Qs] , PsSQs) =

                                    $⟨ Matches-[] C ⟩
    Matches ∞ (C [ Ps ]) C          ↝⟨ Matches-cong (Proc-sym !ab≡C[Ps]) ⟩
    Matches ∞ (! name a ∙ (b ∙)) C  ↝⟨ helper !ab≡C[Ps] !ac≡C[Qs] ⟩□
    ⊥                               □

    where

    helper : Equal ∞ (! name a ∙ (b ∙)) (C [ Ps ]) →
             Equal ∞ (! name a ∙ (c ∙)) (C [ Qs ]) →
             ¬ Matches ∞ (! name a ∙ (b ∙)) C

    helper !ab≡ _ (hole x) = case PsSQs x of λ where
      (_ , Ps[x]∼!ab∣b , _ , base , _) →
                                                    $⟨ Ps[x]∼!ab∣b ⟩
        Ps x ∼ ! name a ∙ (b ∙) ∣ b ∙               ↝⟨ transitive {a = ℓ} (≡→∼ !ab≡) ⟩
        ! name a ∙ (b ∙) ∼ ! name a ∙ (b ∙) ∣ b ∙   ↝⟨ (λ !ab∼!ab∣b → Σ-map id proj₁ $ StepC.right-to-left !ab∼!ab∣b (par-right action)) ⟩
        (∃ λ P′ → ! name a ∙ (b ∙) [ name b ]⟶ P′)  ↝⟨ cancel-name ∘ !-only ·-only ∘ proj₂ ⟩
        a ≡ b                                       ↝⟨ a≢b ⟩□
        ⊥                                           □

    helper (! ab≡) (! ac≡) (! hole x) = case PsSQs x of λ where
      (_ , Ps[x]∼!ab∣b , _ , base , _) →
                                                  $⟨ Ps[x]∼!ab∣b ⟩
        Ps x ∼ ! name a ∙ (b ∙) ∣ b ∙             ↝⟨ transitive {a = ℓ} (≡→∼ ab≡) ⟩
        name a ∙ (b ∙) ∼ ! name a ∙ (b ∙) ∣ b ∙   ↝⟨ (λ ab∼!ab∣b → Σ-map id proj₁ $ StepC.right-to-left ab∼!ab∣b (par-right action)) ⟩
        (∃ λ P′ → name a ∙ (b ∙) [ name b ]⟶ P′)  ↝⟨ cancel-name ∘ ·-only ∘ proj₂ ⟩
        a ≡ b                                     ↝⟨ a≢b ⟩□
        ⊥                                         □

    helper (! (_ · b≡′)) (! (_ · c≡′)) (! action {C = C} M) =
      case force C , force b≡′ , force c≡′ , force M {j = ∞} ⦂
             (∃ λ C → Equal ∞ _ (C [ Ps ]) ×
                      Equal ∞ _ (C [ Qs ]) × Matches ∞ _ C) of λ where

        (._ , b≡ , _ , hole x) → case PsSQs x of λ where
          (_ , Ps[x]∼!ab∣b , _ , base , _) →
                                           $⟨ Ps[x]∼!ab∣b ⟩
            Ps x ∼ ! name a ∙ (b ∙) ∣ b ∙  ↝⟨ transitive {a = ℓ} (≡→∼ b≡) ⟩
            b ∙ ∼ ! name a ∙ (b ∙) ∣ b ∙   ↝⟨ (λ b∼!ab∣b → Σ-map id proj₁ $
                                                             StepC.right-to-left b∼!ab∣b (par-left (replication (par-right action)))) ⟩
            (∃ λ P′ → b ∙ [ name a ]⟶ P′)  ↝⟨ cancel-name ∘ ·-only ∘ proj₂ ⟩
            b ≡ a                          ↝⟨ a≢b ∘ sym ⟩□
            ⊥                              □

        (._ , _ , c≡b · _ , action _) →
                           $⟨ c≡b ⟩
          name c ≡ name b  ↝⟨ cancel-name ⟩
          c ≡ b            ↝⟨ a≢b ⟩□
          ⊥                □

  R⊆StepS : R ⊆ ⟦ StepC ⟧ S
  R⊆StepS base = StepC.⟨ lr , rl ⟩
    where
    lr : ∀ {P′ μ} →
         ! name a ∙ (b ∙) [ μ ]⟶ P′ →
         ∃ λ Q′ → ! name a ∙ (c ∙) [ μ ]⟶ Q′ × S (P′ , Q′)
    lr {P′} {μ} !ab[μ]⟶P′ = case 6-1-3-2 !ab[μ]⟶P′ of λ where
      (inj₁ (.(b ∙) , action , P′∼!ab∣b)) →
          ! name a ∙ (c ∙) ∣ c ∙
        , replication (par-right action)
        , _
        , (P′                      ∼⟨ P′∼!ab∣b ⟩■
           ! name a ∙ (b ∙) ∣ b ∙)
        , _
        , base
        , (! name a ∙ (c ∙) ∣ c ∙  ■)

      (inj₂ (μ≡τ , _)) → ⊥-elim $ name≢τ (
        name a  ≡⟨ !-only ·-only !ab[μ]⟶P′ ⟩
        μ       ≡⟨ μ≡τ ⟩∎
        τ       ∎)

    rl : ∀ {Q′ μ} →
         ! name a ∙ (c ∙) [ μ ]⟶ Q′ →
         ∃ λ P′ → ! name a ∙ (b ∙) [ μ ]⟶ P′ × S (P′ , Q′)
    rl {Q′} {μ} !ac[μ]⟶Q′ = case 6-1-3-2 !ac[μ]⟶Q′ of λ where
      (inj₁ (.(c ∙) , action , Q′∼!ac∣c)) →
          ! name a ∙ (b ∙) ∣ b ∙
        , replication (par-right action)
        , _
        , (! name a ∙ (b ∙) ∣ b ∙  ■)
        , _
        , base
        , (! name a ∙ (c ∙) ∣ c ∙  ∼⟨ symmetric Q′∼!ac∣c ⟩■
           Q′)

      (inj₂ (μ≡τ , _)) → ⊥-elim $ name≢τ (
        name a  ≡⟨ !-only ·-only !ac[μ]⟶Q′ ⟩
        μ       ≡⟨ μ≡τ ⟩∎
        τ       ∎)

  -- Note the use of compatibility in [R]⊆Step[S].

  [R]⊆Step[S] : Up-to-context R ⊆ ⟦ StepC ⟧ (Up-to-context S)
  [R]⊆Step[S] =
    Up-to-context R              ⊆⟨ up-to-context-monotone (λ {x} → R⊆StepS {x}) ⟩
    Up-to-context (⟦ StepC ⟧ S)  ⊆⟨ comp ⟩∎
    ⟦ StepC ⟧ (Up-to-context S)  ∎

  contradiction : ⊥
  contradiction =
                                                               $⟨ d!ab[R]d!ac ⟩
    Up-to-context R ( name d ∙ (! name a ∙ (b ∙))
                    , name d ∙ (! name a ∙ (c ∙))
                    )                                          ↝⟨ [R]⊆Step[S] ⟩

    ⟦ StepC ⟧ (Up-to-context S) ( name d ∙ (! name a ∙ (b ∙))
                                , name d ∙ (! name a ∙ (c ∙))
                                )                              ↝⟨ (λ s → StepC.left-to-right s action) ⟩

    (∃ λ P → name d ∙ (! name a ∙ (c ∙)) [ name d ]⟶ P ×
             Up-to-context S (! name a ∙ (b ∙) , P))           ↝⟨ (λ { (P , d!ac[d]⟶P  , !ab[S]P) →
                                                                       subst (Up-to-context S ∘ (_ ,_)) (·-only⟶ d!ac[d]⟶P) !ab[S]P }) ⟩

    Up-to-context S (! name a ∙ (b ∙) , ! name a ∙ (c ∙))      ↝⟨ ¬!ab[S]!ac ⟩□

    ⊥                                                          □

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- Minimal propositional logic, de Bruijn approach, initial encoding

module Bi.Mp where

open import Lib using (List; _,_; LMem; lzero; lsuc)

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Set
Cx = List Ty

isTrue : Ty -> Cx -> Set
isTrue a tc = LMem a tc

-- Terms

module Mp where
  infixl 1 _$_
  infixr 0 lam=>_
  data Tm (tc : Cx) : Ty -> Set where
    var    : forall {a}     -> isTrue a tc               -> Tm tc a
    lam=>_ : forall {a b}   -> Tm (tc , a) b             -> Tm tc (a => b)
    _$_    : forall {a b}   -> Tm tc (a => b) -> Tm tc a -> Tm tc b
    pair'  : forall {a b}   -> Tm tc a        -> Tm tc b -> Tm tc (a && b)
    fst    : forall {a b}   -> Tm tc (a && b)            -> Tm tc a
    snd    : forall {a b}   -> Tm tc (a && b)            -> Tm tc b
    left   : forall {a b}   -> Tm tc a                   -> Tm tc (a || b)
    right  : forall {a b}   -> Tm tc b                   -> Tm tc (a || b)
    case'  : forall {a b c} -> Tm tc (a || b) -> Tm (tc , a) c -> Tm (tc , b) c -> Tm tc c

  syntax pair' x y    = [ x , y ]
  syntax case' xy x y = case xy => x => y

  v0 : forall {tc a} -> Tm (tc , a) a
  v0 = var lzero

  v1 : forall {tc a b} -> Tm (tc , a , b) a
  v1 = var (lsuc lzero)

  v2 : forall {tc a b c} -> Tm (tc , a , b , c) a
  v2 = var (lsuc (lsuc lzero))

  Thm : Ty -> Set
  Thm a = forall {tc} -> Tm tc a
open Mp public

-- Example theorems

c1 : forall {a b} -> Thm (a && b <=> b && a)
c1 =
  [ lam=> [ snd v0 , fst v0 ]
  , lam=> [ snd v0 , fst v0 ]
  ]

c2 : forall {a b} -> Thm (a || b <=> b || a)
c2 =
  [ lam=>
      (case v0
        => right v0
        => left  v0)
  , lam=>
      (case v0
        => right v0
        => left  v0)
  ]

i1 : forall {a} -> Thm (a && a <=> a)
i1 =
  [ lam=> fst v0
  , lam=> [ v0 , v0 ]
  ]

i2 : forall {a} -> Thm (a || a <=> a)
i2 =
  [ lam=>
      (case v0
        => v0
        => v0)
  , lam=> left v0
  ]

l3 : forall {a} -> Thm ((a => a) <=> TRUE)
l3 =
  [ lam=> lam=> v0
  , lam=> lam=> v0
  ]

l1 : forall {a b c} -> Thm (a && (b && c) <=> (a && b) && c)
l1 =
  [ lam=>
      [ [ fst v0 , fst (snd v0) ]
      , snd (snd v0)
      ]
  , lam=>
      [ fst (fst v0)
      , [ snd (fst v0) , snd v0 ]
      ]
  ]

l2 : forall {a} -> Thm (a && TRUE <=> a)
l2 =
  [ lam=> fst v0
  , lam=> [ v0 , lam=> v0 ]
  ]

l4 : forall {a b c} -> Thm (a && (b || c) <=> (a && b) || (a && c))
l4 =
  [ lam=>
      (case snd v0
        => left  [ fst v1 , v0 ]
        => right [ fst v1 , v0 ])
  , lam=>
      (case v0
        => [ fst v0 , left  (snd v0) ]
        => [ fst v0 , right (snd v0) ])
  ]

l6 : forall {a b c} -> Thm (a || (b && c) <=> (a || b) && (a || c))
l6 =
  [ lam=>
      (case v0
        => [ left  v0       , left  v0 ]
        => [ right (fst v0) , right (snd v0) ])
  , lam=>
      (case fst v0
        => left v0
        =>
          case snd v1
            => left  v0
            => right [ v1 , v0 ])
  ]

l7 : forall {a} -> Thm (a || TRUE <=> TRUE)
l7 =
  [ lam=> lam=> v0
  , lam=> right v0
  ]

l9 : forall {a b c} -> Thm (a || (b || c) <=> (a || b) || c)
l9 =
  [ lam=>
      (case v0
        => left (left v0)
        =>
          case v0
            => left  (right v0)
            => right v0)
  , lam=>
      (case v0
        =>
          case v0
            => left  v0
            => right (left v0)
        => right (right v0))
  ]

l11 : forall {a b c} -> Thm ((a => (b && c)) <=> (a => b) && (a => c))
l11 =
  [ lam=>
      [ lam=> fst (v1 $ v0)
      , lam=> snd (v1 $ v0)
      ]
  , lam=>
      lam=> [ fst v1 $ v0 , snd v1 $ v0 ]
  ]

l12 : forall {a} -> Thm ((a => TRUE) <=> TRUE)
l12 =
  [ lam=> lam=> v0
  , lam=> lam=> v1
  ]

l13 : forall {a b c} -> Thm ((a => (b => c)) <=> ((a && b) => c))
l13 =
  [ lam=>
      lam=> v1 $ fst v0 $ snd v0
  , lam=>
      lam=>
        lam=> v2 $ [ v1 , v0 ]
  ]

l16 : forall {a b c} -> Thm (((a && b) => c) <=> (a => (b => c)))
l16 =
  [ lam=>
      lam=>
        lam=> v2 $ [ v1 , v0 ]
  , lam=>
      lam=> v1 $ fst v0 $ snd v0
  ]

l17 : forall {a} -> Thm ((TRUE => a) <=> a)
l17 =
  [ lam=> v0 $ (lam=> v0)
  , lam=> lam=> v1
  ]

l19 : forall {a b c} -> Thm (((a || b) => c) <=> (a => c) && (b => c))
l19 =
  [ lam=>
      [ lam=> v1 $ left  v0
      , lam=> v1 $ right v0
      ]
  , lam=>
      lam=>
        (case v0
          => fst v2 $ v0
          => snd v2 $ v0)
  ]


text:
{-
  Function types
  A , B : Set -- Set = Type
  A → B : Set

  Products and sums
  A × B : Set
  A ⊎ B : Set -- disjoint union

  Don't have A ∪ B : Set! And neither A ∩ B : Set.
  These are evil operations, because they depend on elements.
-}

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_

variable
  A B C : Set

{-
  _,_ : A → B → A × B
  proj₁ (a , b) = a -- copattern matching
  proj₂ (a , b) = b
-}

curry : (A × B → C) → (A → B → C)
curry f a b = f (a , b)

uncurry : (A → B → C) → (A × B → C)
uncurry g x = g (proj₁ x) (proj₂ x)

{-
  These two functions are inverses.
  How is this isomorphism called? Adjunction.
  Explains the relation between functions and product.
  Functions are "right adjoint" to product.
-}

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

case : (A → C) → (B → C) → (A ⊎ B → C)
case f g (inj₁ a) = f a -- x C-c C-c
case f g (inj₂ b) = g b

-- uncurry case
uncase : (A ⊎ B → C) → (A → C) × (B → C)
proj₁ (uncase f) a = f (inj₁ a)
proj₂ (uncase f) b = f (inj₂ b)

{-
  These functions are inverse to each other they witness that ⊎ is a left
  adjoint (of the diagonal).
  If functions are the right adjoint of products what is the left adjoint of
  sums (⊎)?
-}

-- data is defined by constructors   _⊎_ , _×_
-- codata (record) is defined by destructors  _×_ , _→_
{-
  data _×'_ (A B : Set) : Set where
    _,_ : A → B → A ×' B
    proj₁' : A × B → A
    proj₁' (a , b) = a -- pattern matching
-}

-- What about nullary, empty product, empty sum?

record ⊤ : Set where -- the unit type, it has exactly one element tt.
  constructor tt
{-
  tt : ⊤
  tt = record {}
-}

data ⊥ : Set where -- this is the empty type, no elements.
case⊥ : ⊥ → C
case⊥ () -- impossible pattern

-- In classical propositional logic: prop = Bool
prop = Set -- the type of evidence: propositions as type explanations
-- in HoTT prop = hprop = types with at most inhabitant

variable
  P Q R : prop

infixl 5 _∧_
_∧_ : prop → prop → prop
P ∧ Q = P × Q

infixl 3 _∨_
_∨_ : prop → prop → prop
P ∨ Q = P ⊎ Q

infixr 2 _⇒_
_⇒_ : prop → prop → prop
P ⇒ Q = P → Q

True : prop
True = ⊤

False : prop
False = ⊥

¬ : prop → prop
¬ P = P ⇒ False

infix 1 _⇔_
_⇔_ : prop → prop → prop
P ⇔ Q = (P ⇒ Q) ∧ (Q ⇒ P)

deMorgan : ¬ (P ∨ Q) ⇔ ¬ P ∧ ¬ Q
proj₁ deMorgan x = (λ p → x (inj₁ p)) , λ q → x (inj₂ q)
proj₂ deMorgan y (inj₁ p) = proj₁ y p
proj₂ deMorgan y (inj₂ q) = proj₂ y q

-- the other direction is no logical truth in intuitionistic logic
deMorgan' : (¬ P ∨ ¬ Q) ⇒ ¬ (P ∧ Q)
deMorgan' (inj₁ x) z = x (proj₁ z)
deMorgan' (inj₂ x) z = x (proj₂ z)

max_stars_repo_path: Type Theory/notes-02-tuesday.agda

max_issues_repo_path: Type Theory/notes-02-tuesday.agda

max_forks_repo_path: Type Theory/notes-02-tuesday.agda