text:
------------------------------------------------------------------------------
-- Totality of predecessor function
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.PredTotality where

open import FOTC.Base

data N : D → Set where
  nzero : N zero
  nsucc : ∀ {n} → N n → N (succ₁ n)

-- Induction principle generated by Coq 8.4pl4 when we define the data
-- type N in Prop.
N-ind₁ : (A : D → Set) →
         A zero →
         (∀ {n} → N n → A n → A (succ₁ n)) →
         ∀ {n} → N n → A n
N-ind₁ A A0 h nzero      = A0
N-ind₁ A A0 h (nsucc Nn) = h Nn (N-ind₁ A A0 h Nn)

-- The induction principle removing the hypothesis N n from the
-- inductive step.
N-ind₂ : (A : D → Set) →
         A zero →
         (∀ {n} → A n → A (succ₁ n)) →
         ∀ {n} → N n → A n
N-ind₂ A A0 h nzero      = A0
N-ind₂ A A0 h (nsucc Nn) = h (N-ind₂ A A0 h Nn)

-- Proof by pattern matching.
pred-N : ∀ {n} → N n → N (pred₁ n)
pred-N nzero          = subst N (sym pred-0) nzero
pred-N (nsucc {n} Nn) = subst N (sym (pred-S n)) Nn

-- Proof using N-ind₁.
pred-N₁ : ∀ {n} → N n → N (pred₁ n)
pred-N₁ = N-ind₁ A A0 is
  where
  A : D → Set
  A i = N (pred₁ i)

  A0 : A zero
  A0 = subst N (sym pred-0) nzero

  is : ∀ {i} → N i → A i → A (succ₁ i)
  is {i} Ni Ai = subst N (sym (pred-S i)) Ni

-- Proof using N-ind₂.
-- pred-N₂ : ∀ {n} → N n → N (pred₁ n)
-- pred-N₂ = N-ind₂ A A0 is
--   where
--   A : D → Set
--   A i = N (pred₁ i)

--   A0 : A zero
--   A0 = subst N (sym pred-0) nzero

--   is : ∀ {i} → A i → A (succ₁ i)
--   is {i} Ai = {!!}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
postulate
  F : Set → Set
  _ : {@0 A : Set} → F λ { → A }

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas 2019-11-06, issue #4172, examples by nad.

-- Single constructor matches for non-indexed types should be ok
-- even when argument is erased, as long as pattern variables
-- are only used in erased context on the rhs.

-- https://github.com/agda/agda/issues/4172#issue-517690102

record Erased (A : Set) : Set where
  constructor [_]
  field
    @0 erased : A

open Erased

data W (A : Set) (B : A → Set) : Set where
  sup : (x : A) → (B x → W A B) → W A B

lemma :
  {A : Set} {B : A → Set} →
  Erased (W A B) → W (Erased A) (λ x → Erased (B (erased x)))
lemma [ sup x f ] = sup [ x ] λ ([ y ]) → lemma [ f y ]

-- https://github.com/agda/agda/issues/4172#issuecomment-549768270

data ⊥ : Set where

data E : Set where
  c : E → E

magic : @0 E → ⊥
magic (c e) = magic e

max_stars_repo_name: strake/agda

max_issues_repo_name: strake/agda

max_forks_repo_name: strake/agda


text: S : Set; S = S

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- A formalization of the polymorphic lambda calculus extended with
-- iso-recursive types
------------------------------------------------------------------------

-- Author: Sandro Stucki
-- Copyright (c) 2015 EPFL

-- The code in this directory contains an Agda formalization of the
-- Girard-Reynolds polymorphic lambda calculus (System F) extended
-- with iso-recursive types.
--
-- The code makes heavy use of the Agda standard library, which is
-- freely available from
--
--   https://github.com/agda/agda-stdlib/
--
-- The code has been tested using Agda 2.6.0.1 and version 1.0.1 of the
-- Agda standard library.

module README where

------------------------------------------------------------------------
-- Module overview

-- The formalization is organized in the following modules.

-- Syntax for terms and types along with support for term/type
-- substitutions.  These modules also contain church/CPS encodings for
-- some other forms, such as existential types or tuples.
open import SystemF.Term
open import SystemF.Type

-- Typing derivations along with substitution/weakening lemmas.
open import SystemF.WtTerm

-- A (functional) call-by-value small-step semantics.  This module
-- also contains a type soundness proof with respect to to said
-- semantics as well as a proof of its equivalence (strong
-- bisimilarity) to the big-step semantics mentioned below.  The type
-- soundness proof uses the common progress & preservation
-- (i.e. subject reduction) structure.
open import SystemF.Reduction

-- Two equivalent versions of a (functional) call-by-value big-step
-- semantics along with corresponding type soundness proofs.  The
-- second version is formulated without the use of productivity
-- checker workarounds.  The latter module also contains an
-- equivalence proof of the two semantics.
open import SystemF.Eval
open import SystemF.Eval.NoWorkarounds

-- Decision procedures for type checking and a uniqueness proof for
-- typing derivations.
open import SystemF.TypeCheck

-- Danielsson's partiality-and-failure monad.  This monad provides the
-- domain in which functional operational semantics are formulated.
open import PartialityAndFailure

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


text:
-- Andreas, 2016-09-28
-- Level constraints X <= a and a <= X should solve X = a.

-- {-# OPTIONS -v tc.constr.add:40 #-}

open import Common.Level

module _ (a : Level) where
 mutual
  X : Level
  X = _

  data C : Set (lsuc X) where
    c : Set a → C  -- constrains X by a <= X

  data D : Set (lsuc a) where
    c : Set X → D  -- constrains X by X <= a

-- should succeed


text:
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --show-implicit #-}

module HeapProperties where
  open import HeapPropertiesDefs public
  open import HeapLemmasForSplitting public

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


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

open import HoTT

{- A proof that (A * B) * C ≃ (C * B) * A, which combined with commutativity
 - proves associativity.
 -
 - Agda has a hard time compiling this but sometimes it succeeds.
 -
 - Favonia (2016 May): I have consistent success in compiling this file.
 -
 -}

open import homotopy.JoinComm

module homotopy.JoinAssocCubical where

{- Square and cube lemmas. Some of these are probably generally useful -}
private

  app=cst-square : ∀ {i j} {A : Type i} {B : Type j}
    {b : B} {f : A → B} (p : ∀ a → f a == b)
    {a₁ a₂ : A} (q : a₁ == a₂)
    → Square (p a₁) (ap f q) idp (p a₂)
  app=cst-square p idp = hid-square

  app=cst-square= : ∀ {i j} {A : Type i} {B : Type j}
    {b : B} {f : A → B} {p₁ p₂ : ∀ a → f a == b}
    (α : ∀ a → p₁ a == p₂ a) {a₁ a₂ : A} (q : a₁ == a₂)
    → Cube (app=cst-square p₁ q)
           (app=cst-square p₂ q)
           (horiz-degen-square $ α a₁)
           hid-square
           hid-square
           (horiz-degen-square $ α a₂)
  app=cst-square= α idp = y-degen-cube idp

  app=cst-square-β : ∀ {i j} {A : Type i} {B : Type j} {b : B} {f : A → B}
    (g : (a : A) → f a == b) {x y : A} (p : x == y)
    {sq : Square (g x) (ap f p) idp (g y)}
    → apd g p == ↓-app=cst-from-square sq
    → app=cst-square g p == sq
  app=cst-square-β g idp α =
    ! horiz-degen-square-idp ∙ ap horiz-degen-square α ∙ horiz-degen-square-β _

  ap-∘-app=cst-square : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
    {b : B} {f : A → B} (h : B → C) (g : (a : A) → f a == b)
    {x y : A} (p : x == y)
    → Cube (app=cst-square (ap h ∘ g) p)
           (ap-square h (app=cst-square g p))
           hid-square
           (horiz-degen-square $ ap-∘ h f p)
           ids
           hid-square
  ap-∘-app=cst-square h g idp =
    cube-shift-right (! ap-square-hid) $
      cube-shift-top (! horiz-degen-square-idp) $
        x-degen-cube idp

  cube-to-↓-rtriangle : ∀ {i j} {A : Type i} {B : Type j}
    {b₀ b₁ : A → B} {b : B} {p₀₁ : (a : A) → b₀ a == b₁ a}
    {p₀ : (a : A) → b₀ a == b} {p₁ : (a : A) → b₁ a == b}
    {x y : A} {q : x == y}
    {sqx : Square (p₀₁ x) (p₀ x) (p₁ x) idp}
    {sqy : Square (p₀₁ y) (p₀ y) (p₁ y) idp}
    → Cube sqx sqy (natural-square p₀₁ q) (app=cst-square p₀ q)
                   (app=cst-square p₁ q) ids
    → sqx == sqy [ (λ z → Square (p₀₁ z) (p₀ z) (p₁ z) idp) ↓ q ]
  cube-to-↓-rtriangle {q = idp} cu = x-degen-cube-out cu

{- approximately, [massage] describes the action of
 - [switch : (A * B) * C → (C * B) * A] on the level of squares -}
private

  massage : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋
    → Square (! p₀₋) (p₋₁ ∙ ! p₁₋) idp (! p₋₀)
  massage ids = ids

  massage-massage : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₁₋ : a₁₀ == a₀₁}
    (sq : Square p₀₋ p₋₀ idp p₁₋)
    → Cube (massage (massage sq)) sq
           (horiz-degen-square (!-! p₀₋)) (horiz-degen-square (!-! p₋₀))
           ids (horiz-degen-square (!-! p₁₋))
  massage-massage = square-bot-J
    (λ sq → Cube (massage (massage sq)) sq
              (horiz-degen-square (!-! _)) (horiz-degen-square (!-! _))
              ids (horiz-degen-square (!-! _)))
    idc

  ap-square-massage : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
    {a₀₀ a₀₁ a₁₀ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₁₋ : a₁₀ == a₀₁}
    (sq : Square p₀₋ p₋₀ idp p₁₋)
    → Cube (ap-square f (massage sq)) (massage (ap-square f sq))
           (horiz-degen-square (ap-! f p₀₋))
           (horiz-degen-square (ap-! f p₁₋))
           ids
           (horiz-degen-square (ap-! f p₋₀))
  ap-square-massage f = square-bot-J
    (λ sq → Cube (ap-square f (massage sq)) (massage (ap-square f sq))
                 (horiz-degen-square (ap-! f _))
                 (horiz-degen-square (ap-! f _))
                 ids
                 (horiz-degen-square (ap-! f _)))
    idc

  massage-cube : ∀ {i} {A : Type i}
    {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
    {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
    {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
    {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

    {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
    {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
    {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

    {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
    {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
    {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
    {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
    {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
    {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube (massage sq₋₋₀) (massage sq₋₋₁)
           (!□v sq₀₋₋) (sq₋₁₋ ⊡v !□v sq₁₋₋) vid-square (!□v sq₋₀₋)
  massage-cube idc = idc

private
  module _  {i j k} {A : Type i} {B : Type j} {C : Type k} where

    {- Define an involutive map [switch] -}

    module SwitchLeft = PushoutRec {d = *-span A B} {D = (C * B) * A}
      (λ a → right a)
      (λ b → left (right b))
      (λ {(a , b) → ! (glue (right b , a))})

    switch-coh-fill : (a : A) (b : B) (c : C) → Σ
      (Square (! (glue (left c , a))) (ap SwitchLeft.f (glue (a , b)))
              idp (! (ap left (glue (c , b)))))
      (λ sq → Cube
        sq (massage $ app=cst-square (λ j → glue (j , a)) (glue (c , b)))
        hid-square (horiz-degen-square (SwitchLeft.glue-β (a , b)))
        ids hid-square)
    switch-coh-fill a b c = fill-cube-left _ _ _ _ _

    module SwitchCoh (c : C) = PushoutElim {d = *-span A B}
      {P = λ k → SwitchLeft.f k == left (left c)}
      (λ a → ! (glue (left c , a)))
      (λ b → ! (ap left (glue (c , b))))
      (↓-app=cst-from-square ∘ λ {(a , b) → fst (switch-coh-fill a b c)})

    module Switch = PushoutRec {d = *-span (A * B) C} {D = (C * B) * A}
      SwitchLeft.f
      (λ c → left (left c))
      (λ {(k , c) → SwitchCoh.f c k})

    switch = Switch.f

  module _ {i j k} {A : Type i} {B : Type j} {C : Type k} where

    {- Proof that [switch] is involutive. There are three squares involved:
     - one indexed by A × B, one indexed by A × C, and one by B × C.
     - These are related by a cube indexed by A × B × C.
     - We get the squares for free by defining the cube, as long as
     - we make sure the right faces are dependent on the right types. -}

    {- Three big square terms follow; unfortunately Agda can't figure out
     - what these have to be on its own. Don't worry about the defns. -}

    switch-inv-left-square : (a : A) (b : B)
      → Square idp (ap (switch {A = C} ∘ SwitchLeft.f) (glue (a , b)))
               (ap left (glue (a , b))) idp
    switch-inv-left-square a b = square-symmetry $
      (horiz-degen-square (ap-∘ switch SwitchLeft.f (glue (a , b))))
      ⊡h ap-square switch (horiz-degen-square (SwitchLeft.glue-β (a , b)))
      ⊡h horiz-degen-square (ap-! switch (glue (right b , a)))
      ⊡h !□v (!□h hid-square)
      ⊡h !□v (horiz-degen-square (Switch.glue-β (right b , a)))
      ⊡h !□v hid-square
      ⊡h horiz-degen-square (!-! _)

    switch-inv-coh-left : (c : C) (a : A)
      → Square idp (ap (switch {B = B}) (SwitchCoh.f c (left a)))
               (glue (left a , c)) idp
    switch-inv-coh-left c a = square-symmetry $
      hid-square
      ⊡h ap-square switch hid-square
      ⊡h horiz-degen-square (ap-! switch (glue (left c , a)))
      ⊡h !□v (!□h hid-square)
      ⊡h !□v (horiz-degen-square (Switch.glue-β (left c , a)))
      ⊡h !□v hid-square
      ⊡h horiz-degen-square (!-! _)

    switch-inv-coh-right : (c : C) (b : B)
      → Square idp (ap (switch {C = A}) (SwitchCoh.f c (right b)))
               (glue (right b , c)) idp
    switch-inv-coh-right c b = square-symmetry $
      hid-square
      ⊡h ap-square switch hid-square
      ⊡h horiz-degen-square (ap-! switch (ap left (glue (c , b))))
      ⊡h !□v (!□h (horiz-degen-square (ap-∘ switch left (glue (c , b)))))
      ⊡h !□v hid-square
      ⊡h !□v (horiz-degen-square (SwitchLeft.glue-β (c , b)))
      ⊡h horiz-degen-square (!-! _)

    module SwitchInvLeft = PushoutElim {d = *-span A B}
      {P = λ k → switch {A = C} (switch (left k)) == left k}
      (λ a → idp)
      (λ b → idp)
      (↓-='-from-square ∘ uncurry switch-inv-left-square)

    {- In very small steps, build up the cube -}
    module Coh (a : A) (b : B) (c : C) where

      step₁ : Cube
        (app=cst-square (ap switch ∘ SwitchCoh.f c) (glue (a , b)))
        (ap-square switch (app=cst-square (SwitchCoh.f c) (glue (a , b))))
        _ _ _ _
      step₁ = ap-∘-app=cst-square switch (SwitchCoh.f c) (glue (a , b))

      step₂ : Cube
        (ap-square switch (app=cst-square (SwitchCoh.f c) (glue (a , b))))
        (ap-square switch $ massage $
          app=cst-square (λ j → glue (j , a)) (glue (c , b)))
        _ _ _ _
      step₂ =
        cube-shift-left
          (! (ap (ap-square switch)
                 (app=cst-square-β (SwitchCoh.f c) (glue (a , b))
                                   (SwitchCoh.glue-β c (a , b)))))
          (ap-cube switch (snd (switch-coh-fill a b c)))

      step₃ : Cube
        (ap-square switch $ massage $
          app=cst-square (λ j → glue (j , a)) (glue (c , b)))
        (massage $ ap-square switch $
          app=cst-square (λ j → glue (j , a)) (glue (c , b)))
        _ _ _ _
      step₃ = ap-square-massage switch
                (app=cst-square (λ j → glue (j , a)) (glue (c , b)))

      step₄ : Cube
        (massage $ ap-square switch $
          app=cst-square (λ j → glue (j , a)) (glue (c , b)))
        (massage $
          app=cst-square (λ j → ap switch (glue (j , a))) (glue (c , b)))
        _ _ _ _
      step₄ = massage-cube $ cube-!-x $
        ap-∘-app=cst-square switch (λ j → glue (j , a)) (glue (c , b))

      step₅ : Cube
        (massage $
          app=cst-square (λ j → ap switch (glue (j , a))) (glue (c , b)))
        (massage $ app=cst-square (SwitchCoh.f a) (glue (c , b)))
        _ _ _ _
      step₅ = massage-cube $
        app=cst-square= (λ j → Switch.glue-β (j , a)) (glue (c , b))

      step₆ : Cube
        (massage $ app=cst-square (SwitchCoh.f a) (glue (c , b)))
        (massage $ massage $
          app=cst-square (λ k → glue (k , c)) (glue (a , b)))
        _ _ _ _
      step₆ = massage-cube $
        cube-shift-left
          (! (app=cst-square-β (SwitchCoh.f a) (glue (c , b))
                               (SwitchCoh.glue-β a (c , b))))
          (snd (switch-coh-fill c b a))

      step₇ : Cube
        (massage $ massage $
          app=cst-square (λ k → glue {d = *-span (A * B) C} (k , c))
                         (glue (a , b)))
        (app=cst-square (λ k → glue (k , c)) (glue (a , b)))
        _ _ _ _
      step₇ = massage-massage _

      switch-inv-cube : Cube
        (switch-inv-coh-left c a) (switch-inv-coh-right c b)
        (switch-inv-left-square a b)
        (app=cst-square (ap switch ∘ SwitchCoh.f c) (glue (a , b)))
        (app=cst-square (λ k → glue (k , c)) (glue (a , b)))
        ids
      switch-inv-cube = cube-rotate-x→z $
        step₁ ∙³x step₂ ∙³x step₃ ∙³x step₄ ∙³x step₅ ∙³x step₆ ∙³x step₇

    module SwitchInvCoh (c : C) = PushoutElim {d = *-span A B}
      {P = λ k → Square (SwitchInvLeft.f k) (ap switch (SwitchCoh.f c k))
                        (glue (k , c)) idp}
      (switch-inv-coh-left c)
      (switch-inv-coh-right c)
      (cube-to-↓-rtriangle ∘ λ {(a , b) →
        cube-shift-back
          (! (natural-square-β SwitchInvLeft.f (glue (a , b))
              (SwitchInvLeft.glue-β (a , b))))
          (Coh.switch-inv-cube a b c)})

    abstract
      switch-inv : (l : (A * B) * C) → switch (switch l) == l
      switch-inv = Pushout-elim
        SwitchInvLeft.f
        (λ c → idp)
        (↓-∘=idf-from-square switch switch ∘ λ {(k , c) →
          ap (ap switch) (Switch.glue-β (k , c)) ∙v⊡ SwitchInvCoh.f c k})

module _ {i j k} {A : Type i} {B : Type j} {C : Type k} where

  join-rearrange-equiv : (A * B) * C ≃ (C * B) * A
  join-rearrange-equiv = equiv switch switch switch-inv switch-inv

  join-rearrange-path : (A * B) * C == (C * B) * A
  join-rearrange-path = ua join-rearrange-equiv

  join-assoc-path : (A * B) * C == A * (B * C)
  join-assoc-path = join-rearrange-path ∙ swap-path ∙ ap (A *_) swap-path

  *-assoc = join-assoc-path

module _ {i j k} (X : Ptd i) (Y : Ptd j) (Z : Ptd k) where

  join-rearrange-⊙path : (X ⊙* Y) ⊙* Z == (Z ⊙* Y) ⊙* X
  join-rearrange-⊙path =
    ⊙ua (⊙≃-in join-rearrange-equiv (! (glue (left (snd Z), snd X))))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- {-# OPTIONS -v tc.meta:25 #-}
-- Andreas, 2013-05-23
module DontPruneBlocked where

open import Common.Equality
open import Common.Product

data Bool : Set where
  true false : Bool

if : {A : Set} → Bool → A → A → A
if true  a b = a
if false a b = b

test1 :
  let Fst : Bool → Bool → Bool
      Fst = _
      I : Bool → Bool
      I = _
  in  (a b : Bool) →
       (if (Fst true false) (Fst a b) (Fst b a) ≡ I a) ×  -- don't prune b from Fst!
       (a ≡ I a) ×
       (Fst a b ≡ a)
test1 a b = refl , refl , refl

test : (A : Set) →
  let X : Bool
      X = _
      Fst : A → A → A
      Fst = _
      Snd : A → A → A
      Snd = _
      I : A → A
      I = _
  in  (a b : A) →
       (if X (Fst a b) (Snd a b) ≡ I a) ×  -- don't prune a from Fst and Snd!
       (if X (Snd a b) (Fst a b) ≡ I b) ×  -- don't prune b from Fst and Snd!
       (a ≡ I a) ×
       (X ≡ true)
test A a b = refl , refl , refl , refl

-- Expected result: unsolved metas
--
-- (unless someone implemented unification that produces definitions by case).
--
-- The test case should prevent overzealous pruning:
-- If the first equation pruned away the b, then the second
-- would have an unbound rhs.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- The following file contains various examples of highlighting.
-- It does not necessarily typecheck (but it should parse)

a : A → Set
a b : A → Set
postulate a : A → Set
abstract a b : A → Set
abstracta : A → Set
postulate abstract a : A → Set
private
  a b : A → Set
  abstract a : A → Set
pattern-a : A → Set
abstractSet : Set
x-rewrite : abstractSet

max_stars_repo_name: agda/agda-github-syntax-highlighting


text:
-- Andreas, 2014-02-11 issue raised by Niccolo Veltri
-- {-# OPTIONS -v term.matrices:40 #-}

open import Common.Equality

data _=⟨_⟩⇒*_ {X : Set}(x : X)(f : X → X) : X → Set where
  done : x =⟨ f ⟩⇒* x
  next : ∀{y z} → f y ≡ z → x =⟨ f ⟩⇒* y → x =⟨ f ⟩⇒* z

trans* : ∀{X}{x y z}{f : X → X} → x =⟨ f ⟩⇒* y → y =⟨ f ⟩⇒* z → x =⟨ f ⟩⇒* z
trans* p done = p
trans* p (next r q) = next r (trans* p q)

const* : ∀{X}{x y}{f : X → X} → x =⟨ f ⟩⇒* y → f x ≡ x → x ≡ y
const* done q = refl
const* (next r p) q with const* p q
const* (next r p) q | refl = trans (sym q) r

bad : ∀{X}{x y z}{f : X → X} → x =⟨ f ⟩⇒* z → f z ≡ x → x =⟨ f ⟩⇒* y →
      y =⟨ f ⟩⇒* x
bad done p q rewrite const* q p = done
bad (next p q) r s =
  next r (bad (trans* (next r done) q) p (trans* (next r done) s))

{- PROBLEM WAS:

Interesting part of original call matrix (argss 2-7 of 0-8)

A
? ? = ? ? ?
? = ? ? ? ?
? ? ? ? < ?
? ? ? = ? ?
? ? ? ? ? ?
? ? ? ? < ?

A2 = A*A
? ? ? ? < ?
? = ? ? ? ?
? ? ? ? ? ?
? ? ? = ? ?
? ? ? ? ? ?
? ? ? ? ? ?

Funny, A4 would be worse than A2 why is ist not continuing to iterate?

==> BUG IN 'notWorse' for call graphs.

======================================================================
======================= Initial call matrices ========================
======================================================================

  Source: 0
  Target: 0
  Matrix: = ? ? ? ? ? ? ? ?
          ? = ? ? ? ? ? ? ?
          ? ? ? ? = ? ? ? ?
          ? ? ? = ? ? ? ? ?
          ? ? ? ? ? ? < ? ?
          ? ? ? ? ? = ? ? ?
          ? ? ? ? ? ? ? ? ?
          ? ? ? ? ? ? < ? ?
          ? ? ? ? ? ? ? ? ?
======================================================================
========================= New call matrices ==========================
======================================================================

  Source: 0
  Target: 0
  Matrix: = ? ? ? ? ? ? ? ?
          ? = ? ? ? ? ? ? ?
          ? ? ? ? ? ? < ? ?
          ? ? ? = ? ? ? ? ?
          ? ? ? ? ? ? ? ? ?
          ? ? ? ? ? = ? ? ?
          ? ? ? ? ? ? ? ? ?
          ? ? ? ? ? ? ? ? ?
          ? ? ? ? ? ? ? ? ?
Idempotent call matrices (no dot patterns):
Other call matrices (no dot patterns):
[the two matrices above]
-}

data Top : Set where
  tt : Top

id : Top → Top
id x = x

loop : tt =⟨ id ⟩⇒* tt
loop = bad (next refl done) refl done

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- This file comes from the agda class taught by Peter Selinger at
-- Dalhousie University. It contains a bonus question that
-- propostional logic is complete. We will show this in
-- Kalmar.agda.

-- The course link:
-- https://www.mathstat.dal.ca/~selinger/agda-lectures/

{-# OPTIONS --without-K --safe #-}
module PropLogic where

-- We replace the library (lib-3.0) used in class by the stdlib v2.

-- open import Equality
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; inspect ; [_] ; trans ; sym)

-- open import Nat
open import Data.Nat using (ℕ)

-- open import Bool
-- renaming and defining new connectives.
open import Data.Bool renaming(_∧_ to _and_ ; _∨_ to _or_) using (Bool ; not ; true ; false)
_implies_ : Bool → Bool → Bool
_implies_ a b = not a or b

-- ----------------------------------------------------------------------
-- * Introduction

-- In this project, we will formalize boolean (i.e., classical)
-- propositional logic, define a notion of derivation for the logic,
-- give a semantics for the logic in terms of truth tables (also known
-- as boolean assignments), and prove the soundness of the derivation
-- rules.

-- ----------------------------------------------------------------------
-- * The set of boolean formulas

-- We start by defining the set of boolean formulas. Informally, the
-- formulas are given by the following grammar:
--
-- Formula   A, B ::= P n | A ∧ B | A ⇒ B | ⊥ | ⊤
--
-- Here, n is a natural number, and P n is the nth propositional
-- symbol. A ∧ B is conjunction, A ⇒ B is implication, ⊥ is "false"
-- (also known as a contradiction), and ⊤ is "true". You can type
-- these symbols in Emacs Agda mode using \and, \=>, \bot, and \top.
-- Note that the symbol "⊤" is not the same as the capital letter "T".

-- The set of propositional formulas as an Agda datatype:
data Formula : Set where
  P : ℕ -> Formula
  _∧_ : Formula -> Formula -> Formula
  _⇒_ : Formula -> Formula -> Formula
  ⊥ : Formula
  ⊤ : Formula
  ¬_ : Formula -> Formula
  _∨_ : Formula -> Formula -> Formula

infixl 9 _∧_
infixr 8 _⇒_

infix 20 ¬_

-- ----------------------------------------------------------------------
-- * Derivations

-- The most important concept in logic is that of derivability.
-- "Derivation" is another word for "proof". If A₁, ..., Aₙ, B are
-- formulas, we write
--
--       A₁, ..., Aₙ ⊢
--
-- for the statement "the conclusion B can be derived from hypotheses
-- A₁, ..., Aₙ". The symbol "⊢" is pronounced "entails", and we also
-- say "A₁, ..., Aₙ entails B". You can type this symbol as \|- or
-- \entails or \vdash.
--
-- Although entailment "⊢" is somewhat similar to implication "⇒",
-- there is an important difference: an implication A ⇒ B is a
-- formula, so it could be used, for example, as a hypothesis or as a
-- conclusion in a proof. Entailment is a statement about formulas,
-- i.e., entailment means: there exists a proof of B from hypotheses
-- A₁, ..., Aₙ. Entailment is not itself a formula; it is a statement
-- about provability. Thus, entailment is a relation between a list of
-- formulas (the hypotheses) and a formula (the conclusion).

-- ----------------------------------------------------------------------
-- ** Contexts

-- Before we can formalize entailment, we must formalize lists of
-- formulas. A list of formulas is also called a "context". We
-- write Γ for an arbitrary context.
--
-- Because a context can also be empty (a list of zero formulas), it
-- is convenient to use the empty context as the base case. Then we
-- can give the following recursive definition of contexts: a context
-- is either the empty context, or it is obtained from another context
-- by adding one more formula on the right. In other words, we have
-- the following grammar for contexts:
--
-- Context   Γ ::= Empty | Γ, A
--
-- We formalize this as the following Agda datatype:

{-
data Context : Set where
  Empty : Context
  _,_ : Context -> Formula -> Context
-}

-- Modification: We use List Formula as Context instead of defining a
-- new data type. This will ease the proof using list with distinct
-- elements.

open import Data.List using (List ; _∷_ ; [])
Context = List Formula

infixl 7 _,_

-- _,_ : Context -> Formula -> Context
-- _,_ Γ F = F ∷ Γ

pattern _,_ Γ F = F ∷ Γ
pattern Empty = []

-- We also need the membership relation for contexts. We define the
-- relation A ∈ Γ to mean "the formula A is in the context Γ". The
-- symbol ∈ is typed as \in. The membership relation can be
-- recursively defined as follows: the empty context has no members,
-- and the members of the context Γ, A are A and the members of
-- Γ. More formally, we have the following inference rules for
-- membership:
--
-- ───────────── (∈-base)
--   A ∈ Γ, A
--
--
--     A ∈ Γ
-- ───────────── (∈-step)
--   A ∈ Γ, B
--
-- An inference rule, written with a horizontal line, has the
-- following meaning: if the (zero or more) statements above the line
-- are true, then the statement below the line is true. The statements
-- above the line are called the hypotheses of the inference rule, and
-- the statement below the line is called the conclusion. The name of
-- each inference rule (e.g., ∈-base, ∈-step) is written next to the
-- rule. We use inference rules to define a relation, in this case the
-- relation "∈". By definition, "∈" is the smallest relation
-- satisfying (∈-base) and (∈-step).
--
-- We can directly translate these inference rules into Agda as
-- follows:
data _∈_ : Formula -> Context -> Set where
  ∈-base : ∀ {A : Formula} {Γ : Context} -> A ∈ (Γ , A)
  ∈-step : ∀ {A B : Formula} {Γ : Context} -> A ∈ Γ -> A ∈ (Γ , B)

infixl 6 _∈_

-- ----------------------------------------------------------------------
-- ** Entailment

-- We now define the entailment relation. Recall that the entailment
-- relation Γ ⊢ A is supposed to mean "the conclusion A can be derived
-- from the hypotheses Γ". Defining entailment therefore requires us
-- to formalize what we mean by "derived". In other words, we have to
-- give a set of proof rules for propositional logic. Let me first
-- write these proof rules in the style of inference rules. These
-- rules define the relation "⊢":
--
--    A ∈ Γ
-- ───────────── (assump)
--    Γ ⊢ A
--
--
--   Γ ⊢ A   Γ ⊢ B
-- ───────────────── (∧-intro)
--     Γ ⊢ A ∧ B
--
--
--     Γ ⊢ A ∧ B
-- ───────────────── (∧-elim1)
--       Γ ⊢ A
--
--
--     Γ ⊢ A ∧ B
-- ───────────────── (∧-elim2)
--       Γ ⊢ B
--
--
--     Γ, A ⊢ B
-- ───────────────── (⇒-intro)
--     Γ ⊢ A ⇒ B
--
--
--     Γ ⊢ A ⇒ B    Γ ⊢ A
-- ────────────────────────── (⇒-elim)
--           Γ ⊢ B
--
--
--     Γ ⊢ (A ⇒ ⊥) ⇒ ⊥
-- ────────────────────── (double-negation)
--         Γ ⊢ A
--
--
-- ───────────────── (⊤-intro)
--      Γ ⊢ ⊤
--
--
-- The rule (assump) states that if A is one of the hypotheses, then A
-- can be derived from the hypothesis. Basically A is true "by assumption".
--
-- Several of the connectives, such as ∧ and ⇒, have an "introduction"
-- rule, which shows how to prove such a formula, and an "elimination"
-- rule, which shows how such a formula can be used to prove other
-- things. The rule (∧-intro) states that to prove A ∧ B from the
-- given hypotheses Γ, we must separately derive A and B. Conversely,
-- the rules (∧-elim1) and (∧-elim2) state that if we have already
-- derived A ∧ B, then we may separately conclude A and B. The rule
-- (⇒-intro) states that to prove an implication A ⇒ B, we must assume
-- A and prove B. In other words, to derive A ⇒ B from some hypotheses
-- Γ, we must prove B from the hypotheses Γ, A. The rule (⇒-elim) is
-- also known by its Latin name "modus ponens". It states that if we
-- can prove A ⇒ B and we can also prove A, then we may conclude
-- B. The rule (double-negation) is required to make the logic
-- classical.  Informally, it states that we can prove A by assuming
-- "not A" and deriving a contradiction. Remember that "not A" is an
-- abbreviation for (A ⇒ ⊥). The rule (⊤-intro) states that ⊤ can be
-- derived from any set of hypotheses.

-- We can directly translate the above rules into Agda:
data _⊢_ : Context -> Formula -> Set where
  assump : ∀ {Γ A} -> A ∈ Γ -> Γ ⊢ A
  ∧-intro : ∀ {Γ A B} -> Γ ⊢ A -> Γ ⊢ B -> Γ ⊢ A ∧ B
  ∧-elim1 : ∀ {Γ A B} -> Γ ⊢ A ∧ B -> Γ ⊢ A
  ∧-elim2 : ∀ {Γ A B} -> Γ ⊢ A ∧ B -> Γ ⊢ B
  ⇒-intro : ∀ {Γ A B} -> Γ , A ⊢ B -> Γ ⊢ A ⇒ B
  ⇒-elim : ∀ {Γ A B} -> Γ ⊢ A ⇒ B -> Γ ⊢ A -> Γ ⊢ B
  double-negation : ∀ {Γ A} -> Γ ⊢ (A ⇒ ⊥) ⇒ ⊥ -> Γ ⊢ A
  ⊤-intro : ∀ {Γ} -> Γ ⊢ ⊤
  ¬-intro : ∀ {Γ A} -> Γ , A ⊢ ⊥ -> Γ ⊢ ¬ A
  ¬-elim : ∀ {Γ A} -> Γ  ⊢ ¬ A -> Γ ⊢ A -> Γ ⊢ ⊥
  ∨-intro1 : ∀ {Γ A B} -> Γ ⊢ A -> Γ ⊢ A ∨ B
  ∨-intro2 : ∀ {Γ A B} -> Γ ⊢ B  -> Γ ⊢ A ∨ B
  ∨-elim : ∀ {Γ A B C} -> Γ ⊢ A ∨ B -> Γ , A ⊢ C -> Γ , B ⊢ C -> Γ ⊢ C

infixl 4 _⊢_

-- ----------------------------------------------------------------------
-- ** Weakening

-- "Weakening" is the property that if we add additional hypotheses to
-- an entailment (or change their order), the entailment remains valid.
-- More formally, weakening states that Γ ⊢ A and Γ ⊆ Γ' implies Γ' ⊢ A.
--
-- To state weakening, we must first define ⊆. The symbol ⊆ can be
-- typed as \subseteq or \seq.
_⊆_ : Context -> Context -> Set
Γ ⊆ Γ' = ∀ {A} -> A ∈ Γ -> A ∈ Γ'

infix 4 _⊆_

-- We need a lemma about ⊆:
lemma-⊆ : ∀ {Γ Γ' A} -> Γ ⊆ Γ' -> Γ , A ⊆ Γ' , A
lemma-⊆ hyp ∈-base = ∈-base
lemma-⊆ hyp (∈-step hyp2) = ∈-step (hyp hyp2)

lemma-⊆-ext : ∀ {Γ Γ' A} -> Γ ⊆ Γ' -> Γ ⊆ Γ' , A
lemma-⊆-ext hyp =  \ x -> ∈-step (hyp x)

lemma-⊆-ext' : ∀ {Γ A} -> Γ ⊆ Γ , A
lemma-⊆-ext' = lemma-⊆-ext \ x -> x

lemma-⊆-empty : ∀ {Γ} -> Empty ⊆ Γ
lemma-⊆-empty {Γ} {A} ()

-- Prove the weakening lemma:
weakening : ∀ {Γ Γ' A} -> Γ ⊢ A -> Γ ⊆ Γ' -> Γ' ⊢ A
weakening (assump x) w = assump (w x)
weakening (∧-intro d d₁) w = ∧-intro (weakening d w) (weakening d₁ w)
weakening (∧-elim1 d) w = ∧-elim1 (weakening d w )
weakening (∧-elim2 d) w = ∧-elim2 (weakening d w)
weakening (⇒-intro d) w = ⇒-intro (weakening d (lemma-⊆ w) )
weakening (⇒-elim d d₁) w = ⇒-elim (weakening d w ) (weakening d₁ w )
weakening (double-negation d) w = double-negation (weakening d w )
weakening ⊤-intro w = ⊤-intro
weakening (¬-intro d) w  = ¬-intro (weakening d (lemma-⊆ w ) )
weakening (¬-elim d e) w  = ( ¬-elim (weakening d w) (weakening e w))
weakening (∨-intro1 d) w  = ∨-intro1 (weakening d w)
weakening (∨-intro2 d) w  = ∨-intro2 (weakening d w)
weakening (∨-elim d e f) w  = ∨-elim (weakening d w) (weakening e (lemma-⊆ w)) (weakening f (lemma-⊆ w) )

-- ----------------------------------------------------------------------
-- ** A derived rule

-- Classical logic also has the following rule, called "ex falsum
-- quodlibet" or "⊥-elim".
--
--       Γ ⊢ ⊥
-- ───────────────── (⊥-elim)
--       Γ ⊢ A
--
-- The reason we did not include it in the proof rules in the above
-- definition of entailment it that it follows from the other rules.
-- Prove it:

⊥-elim : ∀ {Γ A} -> Γ ⊢ ⊥ -> Γ ⊢ A
⊥-elim {Γ} {A} a = double-negation a-⊥-⊥  where
  a-⊥ : Γ ⊢ A ⇒ ⊥
  a-⊥ = ⇒-intro (weakening a (lemma-⊆-ext \ x -> x ) )
  a-⊥-⊥ : Γ ⊢ (A ⇒ ⊥) ⇒ ⊥
  a-⊥-⊥ = ⇒-intro (weakening a (lemma-⊆-ext \ x -> x ) )

-- ----------------------------------------------------------------------
-- * Truth table semantics

-- ----------------------------------------------------------------------
-- ** Truth assignments and interpretation

-- Remember that the atomic formulas of our logic are P 0, P 1, P 2,
-- and so on. The fundamental concept of truth tables is that of a
-- "truth assignment", namely a map from atomic formulas to {T, F}.
-- We usually denote a truth assignment by the letter ρ = \rho.
--
-- We formalize truth assignments as maps from ℕ to Bool.
Assign : Set
Assign = ℕ -> Bool

-- Given a truth assignment ρ, we can compute the truth value (true or
-- false) of any given formula. This is called the "interpretation" of
-- formulas.

interp : Assign -> Formula -> Bool
interp ρ (P x) = ρ x
interp ρ (A ∧ B) = (interp ρ A) and (interp ρ B)
interp ρ (A ⇒ B) = (interp ρ A) implies (interp ρ B)
interp ρ ⊥ = false
interp ρ ⊤ = true
interp ρ (¬ A) = not (interp ρ A)
interp ρ (A ∨ B) = (interp ρ A) or (interp ρ B)

-- Lift the interp function to a list of formulas. We interpret a list
-- of formulas basically as the conjunction of the formulas, i.e., the
-- interpretation of Γ is true if and only if the interpretation of
-- all A ∈ Γ is true.
interps : Assign -> Context -> Bool
interps ρ Empty = true
interps ρ (c , x) = interps ρ c and interp ρ x

-- ----------------------------------------------------------------------
-- ** Semantic entailment

-- We write Γ ⊧ A if under all assignments ρ, if Γ is true, then A is true.
-- A special case is when the context Γ is empty. In that case, ⊧ A means
-- that A is true under all assignments, i.e., A is a tautology.
--
-- The symbol ⊧ is pronounced "models", and you can type it as
-- \models. Please note that this is a different symbol from ⊨ = \|=.
-- We use the symbol "⊧" here.
--
-- The relation ⊧ is also called "semantic entailment" or "truth table
-- entailment", to distinguish it from ⊢, which is "syntactic
-- entailment" or "derivability".

-- We define semantic entailment.
-- _⊧_ : Context -> Formula -> Set
-- Γ ⊧ A = ∀ ρ -> interps ρ Γ ≡ true -> interp ρ A ≡ true

_⊧_ : Context -> Formula -> Set
Γ ⊧ f = (ρ : Assign) -> interps ρ Γ ≡ true -> interp ρ f ≡ true

infix 4 _⊧_

-- ----------------------------------------------------------------------
-- * Soundness

-- ----------------------------------------------------------------------
-- ** Lemmas about the boolean connectives

-- The boolean functions 'and' and 'implies' are defined in Bool.agda.
-- We need to know certain ones of their properties.

boolCases : {p : Set} -> (a : Bool) -> (a ≡ true -> p) -> (a ≡ false -> p) -> p
boolCases true t f = t refl
boolCases false t f = f refl

lemma-and-1 : {a b : Bool} -> a ≡ true -> b ≡ true -> a and b ≡ true
lemma-and-1 refl refl = refl

lemma-and-2 : {a b : Bool} -> a and b ≡ true -> a ≡ true
lemma-and-2 {true} {true} abt = refl

lemma-and-3 : {a b : Bool} -> a and b ≡ true -> b ≡ true
lemma-and-3 {true} {true} abt = refl

lemma-imp-1 : {a b : Bool} -> a implies b ≡ true -> a ≡ true -> b ≡ true
lemma-imp-1 {true} {true} aibt at = refl

lemma-imp-2 : {a b : Bool} -> a ≡ false -> a implies b ≡ true
lemma-imp-2 {false} {true} af = refl
lemma-imp-2 {false} {false} af = refl

lemma-imp-3 : {a b : Bool} -> b ≡ true -> a implies b ≡ true
lemma-imp-3 {true} {true} bt = refl
lemma-imp-3 {false} {b} bt = refl

lemma-doubleNeg : {a : Bool} -> (a implies false) implies false ≡ true -> a ≡ true
lemma-doubleNeg {true} a-f-ft = refl

lemma-not-true : {a : Bool} -> a ≡ true -> not a ≡ false
lemma-not-true {.true} refl = refl

lemma-not-false : {a : Bool} -> a ≡ false -> not a ≡ true
lemma-not-false {.false} refl = refl

lemma-or-1 : {a b : Bool} -> a ≡ true -> a or b ≡ true
lemma-or-1 refl  = refl

lemma-or-2 : {a b : Bool} -> b ≡ true -> a or b ≡ true
lemma-or-2 {true} {.true} refl = refl
lemma-or-2 {false} {.true} refl = refl

-- like boolCases
lemma-or-3 : {C : Set} ->  {a b : Bool} -> a or b ≡ true -> (a ≡ true -> C) -> (b ≡ true -> C) -> C
lemma-or-3 {a = true} {true} aob ca cb = ca aob
lemma-or-3 {a = false} {true} aob ca cb = cb aob
lemma-or-3 {a = true} {false} aob ca cb = ca refl

-- ----------------------------------------------------------------------
-- ** Lemmas about the soundness of individual rules

-- Each of the proof rules of logic has a semantic counterpart.

lemma-assump : ∀ Γ A -> A ∈ Γ -> Γ ⊧ A
lemma-assump (._ , A) A ∈-base = \ ρ ct -> lemma-and-3 ct
lemma-assump (Γ' , B) A (∈-step hyp) = \ ρ ct -> (lemma-assump Γ' A hyp) ρ (lemma-and-2 ct )

lemma-∧-intro : ∀ Γ A B -> Γ ⊧ A -> Γ ⊧ B -> Γ ⊧ A ∧ B
lemma-∧-intro Γ A B as bs = \ ρ ct -> lemma-and-1 (as ρ ct ) (bs ρ ct )

lemma-∧-elim1 : ∀ Γ A B -> Γ ⊧ A ∧ B -> Γ ⊧ A
lemma-∧-elim1 Γ A B abs = \ ρ ct -> lemma-and-2 (abs ρ ct)

lemma-∧-elim2 : ∀ Γ A B -> Γ ⊧ A ∧ B -> Γ ⊧ B
lemma-∧-elim2 Γ A B abs = \ ρ ct -> lemma-and-3 (abs ρ ct)

lemma-⇒-intro' : ∀ Γ A B -> Γ , A ⊧ B -> Γ ⊧ A ⇒ B
lemma-⇒-intro' Γ A B a-bs ρ ct  = boolCases (interp ρ A) (\ x -> lemma-imp-3 (a-bs ρ (lemma-and-1 ct x ) ) ) \ x -> lemma-imp-2 x

lemma-⇒-intro : ∀ Γ A B -> Γ , A ⊧ B -> Γ ⊧ A ⇒ B
lemma-⇒-intro Γ A B a-bs ρ ct with (interp ρ) A | inspect (interp ρ) A
lemma-⇒-intro Γ A B a-bs ρ ct | true | [ eq ] = lemma-imp-3 (a-bs ρ (lemma-and-1 ct eq ) )
lemma-⇒-intro Γ A B a-bs ρ ct | false | [ eq ] = refl

lemma-⇒-elim : ∀ Γ A B -> Γ ⊧ A ⇒ B -> Γ ⊧ A -> Γ ⊧ B
lemma-⇒-elim Γ A B a-bs as = \ ρ ct -> lemma-imp-1 (a-bs ρ ct ) (as ρ ct )

lemma-double-negation : ∀ Γ A -> Γ ⊧ (A ⇒ ⊥) ⇒ ⊥ -> Γ ⊧ A
lemma-double-negation Γ A anns = \ ρ ct -> lemma-doubleNeg (anns ρ ct )

lemma-⊤-intro : ∀ Γ -> Γ ⊧ ⊤
lemma-⊤-intro Γ = \ ρ ct -> refl

lemma-¬-intro : ∀ Γ A -> Γ , A ⊧ ⊥ -> Γ ⊧ ¬ A
lemma-¬-intro Γ A a ρ ct with (interp ρ) A | inspect (interp ρ) A
lemma-¬-intro Γ A a ρ ct | true  | [ eq ] = a ρ (lemma-and-1 ct eq)
lemma-¬-intro Γ A a ρ ct | false | [ eq ] = refl

lemma-¬-intro' : ∀ Γ A -> Γ , A ⊧ ⊥ -> Γ ⊧ ¬ A
lemma-¬-intro' Γ A a ρ ct = boolCases (interp ρ A) (\x -> trans (lemma-not-true x ) (a ρ (lemma-and-1 ct x ) )  ) \ x -> lemma-not-false x

lemma-¬-elim : ∀ Γ A -> Γ ⊧ ¬ A -> Γ ⊧  A -> Γ ⊧ ⊥
lemma-¬-elim Γ A a b ρ ct = boolCases (interp ρ A) (\ x -> trans (sym (lemma-not-true x)) (a ρ ct )   ) \ x -> trans (sym  x ) (b ρ ct)

lemma-∨-intro1 : ∀ Γ A B -> Γ ⊧  A -> Γ ⊧  A ∨ B
lemma-∨-intro1 Γ A B a ρ ct = lemma-or-1 (a ρ ct )

lemma-∨-intro2 : ∀ Γ A B -> Γ ⊧  B -> Γ ⊧  A ∨ B
lemma-∨-intro2 Γ A B a ρ ct = lemma-or-2 (a ρ ct )

lemma-∨-elim : ∀ Γ A B C -> Γ ⊧  A ∨ B -> Γ , A ⊧  C -> Γ , B ⊧  C -> Γ ⊧ C
lemma-∨-elim Γ A B C aob ac bc ρ ct = lemma-or-3 (aob ρ ct) (\ x -> ac ρ (lemma-and-1 ct x )  ) \ x -> bc ρ (lemma-and-1 ct x )

-- ----------------------------------------------------------------------
-- * The soundness theorem of boolean logic.

-- Soundness states that Γ ⊢ A implies Γ ⊧ A, or equivalently:
-- everything that is provable is valid.

-- 4. Prove the soundness of boolean logic.
sound : ∀ Γ A -> Γ ⊢ A -> Γ ⊧ A
sound Γ A (assump x) = lemma-assump Γ A x
sound Γ (A ∧ B) (∧-intro hyp hyp₁) = lemma-∧-intro Γ A B (sound Γ A hyp) (sound Γ B hyp₁)
sound Γ A (∧-elim1 {B = B} hyp) = lemma-∧-elim1 Γ A B (sound Γ  (A ∧ B) hyp )
sound Γ A (∧-elim2 {A = A₁} hyp) = lemma-∧-elim2 Γ  A₁ A ((sound Γ  (A₁ ∧ A) hyp ) )
sound Γ (A ⇒ B) (⇒-intro hyp) = lemma-⇒-intro Γ A B (sound (Γ , A) B   hyp )
sound Γ A (⇒-elim {A = A₁} hyp hyp₁) = lemma-⇒-elim Γ A₁ A (sound Γ (A₁ ⇒ A) hyp ) (sound Γ A₁ hyp₁)
sound Γ A (double-negation hyp) = lemma-double-negation Γ A (sound Γ ((A ⇒ ⊥) ⇒ ⊥) hyp)
sound Γ .⊤ ⊤-intro = λ ρ _ → refl
sound Γ (¬ A) (¬-intro x) = lemma-¬-intro' Γ  A ((sound (Γ , A) ⊥  x ) )
sound Γ .⊥ (¬-elim {A = A} x y) = lemma-¬-elim Γ A (sound Γ (¬ A) x) (sound Γ  A y)
sound Γ (A ∨ B) (∨-intro1 x) = lemma-∨-intro1 Γ A B (sound Γ A x )
sound Γ (A ∨ B) (∨-intro2 x) = lemma-∨-intro2 Γ A B (sound Γ B x )
sound Γ C (∨-elim {A = A} {B} x y z) = lemma-∨-elim Γ A B C (sound Γ (A ∨ B) x ) (sound (Γ , A) C y ) (sound (Γ , B) C z)

-- ----------------------------------------------------------------------
-- * Bonus questions and beyond

-- If you feel adventurous, add more connectives, such as ¬A or A ∨ B,
-- to the boolean logic.
--
-- The proof rules are:
--
--    Γ, A ⊢ ⊥
-- ────────────── (¬-intro)
--     Γ ⊢ ¬A
--
--
--    Γ ⊢ ¬A     Γ ⊢ A
-- ───────────────────── (¬-elim)
--         Γ ⊢ ⊥
--
--
--      Γ ⊢ A
-- ───────────── (∨-intro1)
--    Γ ⊢ A ∨ B
--
--
--      Γ ⊢ B
-- ───────────── (∨-intro2)
--    Γ ⊢ A ∨ B
--
--
--    Γ ⊢ A ∨ B    Γ, A ⊢ C    Γ, B ⊢ C
-- ─────────────────────────────────────── (∨-elim)
--                  Γ ⊢ C

-- If you feel extremely ambitious, try to prove completeness, the
-- converse of soundness. Completeness is the statement that Γ ⊧ A
-- implies Γ ⊢ A.
--
-- Warning: this is extremely difficult and far more work than
-- soundness. Neither Frank nor I have been able to finish a proof of
-- completeness.

-- Actually, Peter had finished the proof a couple of days later using
-- conjunction normal form.

completeness-property : Set
completeness-property = ∀ Γ A -> Γ ⊧ A -> Γ ⊢ A

-- Now, I (Bian) will prove this property in Kalmar.agda using
-- Kalmar's lemma.

max_stars_repo_name: onestruggler/Kalmar

max_issues_repo_name: onestruggler/Kalmar

max_forks_repo_name: onestruggler/Kalmar


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

module Cubical.Data.Queue where

open import Cubical.Data.Queue.Base public
open import Cubical.Data.Queue.Finite public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

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

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum
open import Size
open import Codata.Thunk
open import Level
open import Relation.Unary using (_⊆_)

module is-lib.InfSys.FlexSCoinduction {𝓁} where

  private
    variable
      U : Set 𝓁

  open import is-lib.InfSys.Base {𝓁}
  open import is-lib.InfSys.Induction {𝓁}
  open import is-lib.InfSys.SCoinduction {𝓁}
  open MetaRule
  open IS

  {- Generalized inference systems -}

  SFCoInd⟦_,_⟧ : ∀{𝓁c 𝓁p 𝓁n 𝓁n'} → (I : IS {𝓁c} {𝓁p} {𝓁n} U) → (C : IS {𝓁c} {𝓁p} {𝓁n'} U) → U → Size → Set _
  SFCoInd⟦ I , C ⟧ = SCoInd⟦ I ⊓ Ind⟦ I ∪ C ⟧ ⟧

  {- Bounded Coinduction Principle -}

  bdc-lem : ∀{𝓁c 𝓁p 𝓁n 𝓁' 𝓁''}
      → (I : IS {𝓁c} {𝓁p} {𝓁n} U)
      → (S : U → Set 𝓁')
      → (Q : U → Set 𝓁'')
      → S ⊆ Q
      → S ⊆ ISF[ I ] S
      → S ⊆ ISF[ I ⊓ Q ] S
  bdc-lem _ _ _ bd cn Su with cn Su
  ... | rn , c , refl , pr = rn , (c , bd Su) , refl , pr

  bounded-scoind[_,_] : ∀{𝓁c 𝓁p 𝓁n 𝓁n' 𝓁'}
      → (I : IS {𝓁c} {𝓁p} {𝓁n} U)
      → (C : IS {𝓁c} {𝓁p} {𝓁n'} U)
      → (S : U → Set 𝓁')
      → S ⊆ Ind⟦ I ∪ C ⟧      -- S is bounded w.r.t. I ∪ C
      → S ⊆ ISF[ I ] S        -- S is consistent w.r.t. I
      → S ⊆ (λ u → ∀{i} → SFCoInd⟦ I , C ⟧ u i)
  bounded-scoind[ I , C ] S bd cn Su = scoind[ I ⊓ Ind⟦ I ∪ C ⟧ ] S (bdc-lem I S Ind⟦ I ∪ C ⟧ bd cn) Su

  {- Get Ind from SFCoInd -}

  sfcoind-to-ind : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → (λ u → ∀{i} → SFCoInd⟦ is , cois ⟧ u i) ⊆ Ind⟦ is ∪ cois ⟧
  sfcoind-to-ind co with co
  sfcoind-to-ind co | sfold (_ , (_ , sd) , refl , _) = sd

  {- Apply Rule -}

  apply-sfcoind : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → (rn : is .Names) → RClosed (is .rules rn) (λ u → ∀{i} → SFCoInd⟦ is , cois ⟧ u i)
  apply-sfcoind rn c pr = apply-scoind rn (c , apply-ind (inj₁ rn) c λ i → sfcoind-to-ind (pr i)) pr

  {- Postfix - Prefix -}

  sfcoind-postfix : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → (λ u → ∀{i} → SFCoInd⟦ is , cois ⟧ u i) ⊆ ISF[ is ] (λ u → ∀{i} → SFCoInd⟦ is , cois ⟧ u i)
  sfcoind-postfix SFCoInd with SFCoInd
  ... | sfold (rn , (c , _) , refl , pr) = rn , c , refl , λ i → (pr i) .force

  sfcoind-prefix : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
    → ISF[ is ] (λ u → ∀{i} → SFCoInd⟦ is , cois ⟧ u i) ⊆ λ u → ∀{i} → SFCoInd⟦ is , cois ⟧ u i
  sfcoind-prefix (rn , c , refl , pr) = apply-sfcoind rn c pr

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module ShadowModule where

module A where
  module B where
    data D : Set where

open A

module B where


text:
module Metalogic.Classical.Propositional.ProofSystem {ℓₚ} (Proposition : Set(ℓₚ)) where

import      Lvl
open import Data hiding (empty)
import      Data.List
open        Data.List using (List ; ∅ ; _⊰_ ; _++_ ; [_ ; _])
open        Data.List.Notation
import      Data.List.Relation.Membership
import      Data.List.Relation.Membership.Proofs
open import Metalogic.Classical.Propositional.Syntax(Proposition)
open import Functional

open        Data.List.Relation.Membership{ℓₚ} {Formula}
open        Data.List.Relation.Membership.Proofs{ℓₚ} {Formula}

module Meta where
  data _⊢_ : List(Formula) → Formula → Set(ℓₚ) where -- TODO: Reduce the number of rules
    [⊤]-intro : ∀{Γ} → (Γ ⊢ ⊤)

    [⊥]-intro : ∀{Γ}{φ} → (φ ∈ Γ) → ((¬ φ) ∈ Γ) → (Γ ⊢ ⊥)
    [⊥]-elim  : ∀{Γ}{φ} → (⊥ ∈ Γ) → (Γ ⊢ φ)

    [¬]-intro : ∀{Γ}{φ} → ((φ ∈ Γ) → (Γ ⊢ ⊥)) → (Γ ⊢ (¬ φ))
    [¬]-elim  : ∀{Γ}{φ} → (((¬ φ) ∈ Γ) → (Γ ⊢ ⊥)) → (Γ ⊢ φ)

    [∧]-intro : ∀{Γ}{φ₁ φ₂} → (φ₁ ∈ Γ) → (φ₂ ∈ Γ) → (Γ ⊢ (φ₁ ∧ φ₂))
    [∧]-elimₗ  : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∧ φ₂) ∈ Γ) → (Γ ⊢ φ₁)
    [∧]-elimᵣ  : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∧ φ₂) ∈ Γ) → (Γ ⊢ φ₂)

    [∨]-introₗ : ∀{Γ}{φ₁ φ₂} → (φ₁ ∈ Γ) → (Γ ⊢ (φ₁ ∨ φ₂))
    [∨]-introᵣ : ∀{Γ}{φ₁ φ₂} → (φ₂ ∈ Γ) → (Γ ⊢ (φ₁ ∨ φ₂))
    [∨]-elim   : ∀{Γ}{φ₁ φ₂ φ₃} → ((φ₁ ∈ Γ) → (Γ ⊢ φ₃)) → ((φ₂ ∈ Γ) → (Γ ⊢ φ₃)) → ((φ₁ ∨ φ₂) ∈ Γ) → (Γ ⊢ φ₃)

    [⇒]-intro : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∈ Γ) → (Γ ⊢ φ₂)) → (Γ ⊢ (φ₁ ⇒ φ₂))
    [⇒]-elim  : ∀{Γ}{φ₁ φ₂} → ((φ₁ ⇒ φ₂) ∈ Γ) → (φ₁ ∈ Γ) → (Γ ⊢ φ₂)

  [¬¬]-elim : ∀{Γ}{φ} → ((¬ ¬ φ) ∈ Γ) → (Γ ⊢ φ)
  [¬¬]-elim{Γ}{φ} ([¬¬φ]-in) =
    ([¬]-elim{Γ}{φ} ([¬φ]-in ↦
      ([⊥]-intro{Γ}{¬ φ}
        ([¬φ]-in)
        ([¬¬φ]-in)
      )
    ))

  _⊬_ : List(Formula) → Formula → Set(ℓₚ)
  _⊬_ Γ φ = (_⊢_ Γ φ) → Empty{ℓₚ}

  -- Consistency
  Inconsistent : List(Formula) → Set(ℓₚ)
  Inconsistent Γ = (Γ ⊢ ⊥)

  Consistent : List(Formula) → Set(ℓₚ)
  Consistent Γ = (Γ ⊬ ⊥)

module TruthTables where
  open Meta

-- Natural deduction proof trees.
-- This is a proof system that should reflect the semantic truth of formulas.
module NaturalDeduction where
  -- A `Tree` is associated with a formula.
  -- [Proposition without assumptions (Axiom)]
  --   Represented by the type `Tree(φ)`.
  --   It means that a tree with the formula φ at the bottom exists (is constructable).
  --   This represents that the formula φ is provable in the natural deduction proof system.
  -- [Proposition with an assumption]
  --   Represented by the type `Tree(φ₁) → Tree(φ₂)`.
  --   It means that a tree with φ₁ as a leaf and φ₂ at the bottom exists (is constructable).
  --   This represents that the formula φ₂ is provable if one can assume the formula φ₁.
  -- The constructors of `Tree` are all the possible ways to construct a natural deduction proof tree.
  -- If a tree with a certain formula cannot be constructed, then it means that the formula is not provable.
  {-# NO_POSITIVITY_CHECK #-} -- TODO: Could this be a problem? Maybe not? Classical logic is supposed to be consistent, but maybe that does not have anything to do with this?
  data Tree : Formula → Set(ℓₚ) where
    [⊤]-intro : Tree(⊤)

    [⊥]-intro : ∀{φ} → Tree(φ) → Tree(¬ φ) → Tree(⊥)

    [¬]-intro : ∀{φ} → (Tree(φ) → Tree(⊥)) → Tree(¬ φ)
    [¬]-elim  : ∀{φ} → (Tree(¬ φ) → Tree(⊥)) → Tree(φ)

    [∧]-intro : ∀{φ₁ φ₂} → Tree(φ₁) → Tree(φ₂) → Tree(φ₁ ∧ φ₂)
    [∧]-elimₗ  : ∀{φ₁ φ₂} → Tree(φ₁ ∧ φ₂) → Tree(φ₁)
    [∧]-elimᵣ  : ∀{φ₁ φ₂} → Tree(φ₁ ∧ φ₂) → Tree(φ₂)

    [∨]-introₗ : ∀{φ₁ φ₂} → Tree(φ₁) → Tree(φ₁ ∨ φ₂)
    [∨]-introᵣ : ∀{φ₁ φ₂} → Tree(φ₂) → Tree(φ₁ ∨ φ₂)
    [∨]-elim  : ∀{φ₁ φ₂ φ₃} → (Tree(φ₁) → Tree(φ₃)) → (Tree(φ₂) → Tree(φ₃)) → Tree(φ₁ ∨ φ₂) → Tree(φ₃)

    [⇒]-intro : ∀{φ₁ φ₂} → (Tree(φ₁) → Tree(φ₂)) → Tree(φ₁ ⇒ φ₂)
    [⇒]-elim  : ∀{φ₁ φ₂} → Tree(φ₁ ⇒ φ₂) → Tree(φ₁) → Tree(φ₂)

  -- Double negated proposition is positive.
  [¬¬]-elim : ∀{φ} → Tree(¬ (¬ φ)) → Tree(φ)
  [¬¬]-elim nna = [¬]-elim(na ↦ [⊥]-intro na nna)

  -- A contradiction can derive every formula.
  [⊥]-elim : ∀{φ} → Tree(⊥) → Tree(φ)
  [⊥]-elim bottom = [¬]-elim(_ ↦ bottom)

  -- List of natural deduction proof trees.
  -- A `Trees` is associated with a list of formulas.
  -- If all formulas in the list can be constructed, then all the formulas in the list are provable.
  -- This is used to express (⊢) using the usual conventions in formal logic.
  -- Trees(Γ) is the statement that all formulas in Γ have proof trees.
  Trees : List(Formula) → Set(ℓₚ)
  Trees(Γ) = (∀{γ} → (γ ∈ Γ) → Tree(γ))

  module Trees where
    tree : ∀{Γ}{φ} → Trees(Γ) → (φ ∈ Γ) → Tree(φ)
    tree f(x) = f(x)

    empty : Trees(∅)
    empty ()

    singleton : ∀{φ} → Tree(φ) → Trees([ φ ])
    singleton (φ-tree) (use) = φ-tree
    singleton (φ-tree) (skip ())

    -- TODO: This could possibly be generalized to: ∀{Γ₁ Γ₂}{F : T → Set} → (∀{a} → (a ∈ Γ₁) → (a ∈ Γ₂)) → ((∀{γ} → (γ ∈ Γ₂) → F(γ)) → (∀{γ} → (γ ∈ Γ₁) → F(γ)))
    from-[∈] : ∀{Γ₁ Γ₂} → (∀{a} → (a ∈ Γ₁) → (a ∈ Γ₂)) → (Trees(Γ₂) → Trees(Γ₁))
    from-[∈] (f) (Γ₂-trees) {γ} = liftᵣ (f{γ}) (Γ₂-trees)

    push : ∀{Γ}{φ} → Tree(φ) → Trees(Γ) → Trees(φ ⊰ Γ)
    push (φ-tree) (Γ-tree) (use) = φ-tree
    push (φ-tree) (Γ-tree) (skip membership) = Γ-tree (membership)

    pop : ∀{Γ}{φ} → Trees(φ ⊰ Γ) → Trees(Γ)
    pop = from-[∈] (skip)

    first : ∀{Γ}{φ} → Trees(φ ⊰ Γ) → Tree(φ)
    first(f) = f(use)

    -- TODO: Could be removed because liftᵣ is easier to use. ALthough a note/tip should be written for these purposes.
    -- formula-weaken : ∀{ℓ}{T : Set(ℓ)}{Γ₁ Γ₂} → (Trees(Γ₁) → Trees(Γ₂)) → (Trees(Γ₂) → T) → (Trees(Γ₁) → T)
    -- formula-weaken = liftᵣ

    [++]-commute : ∀{Γ₁ Γ₂} → Trees(Γ₁ ++ Γ₂) → Trees(Γ₂ ++ Γ₁)
    [++]-commute {Γ₁}{Γ₂} (trees) = trees ∘ ([∈][++]-commute{_}{Γ₂}{Γ₁})

    [++]-left : ∀{Γ₁ Γ₂} → Trees(Γ₁ ++ Γ₂) → Trees(Γ₁)
    [++]-left {Γ₁}{Γ₂} (trees) ([∈]-[Γ₁]) = trees ([∈][++]-expandᵣ {_}{Γ₁}{Γ₂} [∈]-[Γ₁])

    [++]-right : ∀{Γ₁ Γ₂} → Trees(Γ₁ ++ Γ₂) → Trees(Γ₂)
    [++]-right {Γ₁}{Γ₂} (trees) ([∈]-[Γ₂]) = trees ([∈][++]-expandₗ {_}{Γ₁}{Γ₂} [∈]-[Γ₂])

    [++]-deduplicate : ∀{Γ} → Trees(Γ ++ Γ) → Trees(Γ)
    [++]-deduplicate {Γ} (trees) {γ} = liftᵣ([∈][++]-expandₗ {γ}{Γ}{Γ})(trees{γ})

    [⊰]-reorderₗ : ∀{Γ₁ Γ₂}{φ} → Trees(Γ₁ ++ (φ ⊰ Γ₂)) → Trees(φ ⊰ (Γ₁ ++ Γ₂))
    [⊰]-reorderₗ {Γ₁}{Γ₂}{φ} (Γ₁φΓ₂-trees) = push (φ-tree) ([++]-commute{Γ₂}{Γ₁} Γ₂Γ₁-trees) where
      φΓ₂Γ₁-trees : Trees(φ ⊰ (Γ₂ ++ Γ₁))
      φΓ₂Γ₁-trees = [++]-commute{Γ₁}{φ ⊰ Γ₂} (Γ₁φΓ₂-trees)

      φ-tree : Tree(φ)
      φ-tree = first{Γ₂ ++ Γ₁}{φ} (φΓ₂Γ₁-trees)

      Γ₂Γ₁-trees : Trees(Γ₂ ++ Γ₁)
      Γ₂Γ₁-trees = pop{Γ₂ ++ Γ₁}{φ} (φΓ₂Γ₁-trees)
    -- Γ₁ ++ (φ ⊰ Γ₂) //assumption
    -- (φ ⊰ Γ₂) ++ Γ₁ //Trees.[++]-commute
    -- φ ⊰ (Γ₂ ++ Γ₁) //Definition: (++)
    -- φ ⊰ (Γ₁ ++ Γ₂) //Trees.[++]-commute

    push-many : ∀{Γ₁ Γ₂} → Trees(Γ₁) → Trees(Γ₂) → Trees(Γ₁ ++ Γ₂)
    push-many{∅}     {Γ₂} ([∅]-trees)    ([Γ₂]-trees) = [Γ₂]-trees
    push-many{φ ⊰ Γ₁}{Γ₂} ([φ⊰Γ₁]-trees) ([Γ₂]-trees) = [⊰]-reorderₗ{Γ₁}{Γ₂}{φ} (push-many{Γ₁}{φ ⊰ Γ₂} (pop [φ⊰Γ₁]-trees) (push (first [φ⊰Γ₁]-trees) [Γ₂]-trees))

  -- Derivability
  -- Proof of: If there exists a tree for every formula in Γ, then there exists a tree for the formula φ.
  data _⊢_ (Γ : List(Formula)) (φ : Formula) : Set(ℓₚ) where
    [⊢]-construct : (Trees(Γ) → Tree(φ)) → (Γ ⊢ φ)

  module Theorems where
    [⊢]-from-trees : ∀{Γ₁ Γ₂}{φ} → (Trees(Γ₂) → Trees(Γ₁)) → (Γ₁ ⊢ φ) → (Γ₂ ⊢ φ)
    [⊢]-from-trees (trees-fn) ([⊢]-construct (Γ₁⊢φ)) = [⊢]-construct ((Γ₁⊢φ) ∘ (trees-fn))

    [⊢]-formula-weaken : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → ((φ₂ ⊰ Γ) ⊢ φ₁)
    [⊢]-formula-weaken {_}{_}{φ₂} = [⊢]-from-trees (Trees.pop {_}{φ₂})

    [⊢]-weakenₗ : ∀{Γ₂}{φ} → (Γ₂ ⊢ φ) → ∀{Γ₁} → ((Γ₁ ++ Γ₂) ⊢ φ)
    [⊢]-weakenₗ {_} {_} (Γ₂⊢φ) {∅}       = (Γ₂⊢φ)
    [⊢]-weakenₗ {Γ₂}{φ} (Γ₂⊢φ) {φ₂ ⊰ Γ₁} = [⊢]-formula-weaken {Γ₁ ++ Γ₂} ([⊢]-weakenₗ (Γ₂⊢φ) {Γ₁})

    [⊢]-reorder-[++] : ∀{Γ₁ Γ₂}{φ} → ((Γ₁ ++ Γ₂) ⊢ φ) → ((Γ₂ ++ Γ₁) ⊢ φ)
    [⊢]-reorder-[++] {Γ₁}{Γ₂} = [⊢]-from-trees (Trees.[++]-commute {Γ₂}{Γ₁})

    [⊢]-apply : ∀{Γ}{φ} → (Γ ⊢ φ) → Trees(Γ) → Tree(φ)
    [⊢]-apply ([⊢]-construct [Γ]⊢[φ]) (Γ-trees) = ([Γ]⊢[φ]) (Γ-trees)

    [⊢]-apply-first : ∀{Γ}{φ₁ φ₂} → Tree(φ₁) → ((φ₁ ⊰ Γ) ⊢ φ₂) → (Γ ⊢ φ₂)
    [⊢]-apply-first ([φ₁]-tree) ([⊢]-construct ([φ₁⊰Γ]⊢[φ₂])) =
      [⊢]-construct([Γ]⊢[φ₂] ↦
        ([φ₁⊰Γ]⊢[φ₂]) (Trees.push ([φ₁]-tree) (\{γ} → [Γ]⊢[φ₂] {γ}))
      )

    [⊢]-apply-many : ∀{Γ₁ Γ₂}{φ} → Trees(Γ₁) → ((Γ₁ ++ Γ₂) ⊢ φ) → (Γ₂ ⊢ φ)
    [⊢]-apply-many ([Γ₁]-trees) ([⊢]-construct ([Γ₁++Γ₂]⊢[φ])) =
      [⊢]-construct([Γ₂]⊢[φ] ↦
        ([Γ₁++Γ₂]⊢[φ]) (Trees.push-many ([Γ₁]-trees) (\{γ} → [Γ₂]⊢[φ] {γ}))
      )

    [⊢]-reorderᵣ-[⊰] : ∀{Γ₁ Γ₂}{φ₁ φ₂} → ((Γ₁ ++ (φ₁ ⊰ Γ₂)) ⊢ φ₂) ← ((φ₁ ⊰ (Γ₁ ++ Γ₂)) ⊢ φ₂)
    [⊢]-reorderᵣ-[⊰] {Γ₁}{Γ₂}{φ₁} = [⊢]-from-trees (Trees.[⊰]-reorderₗ {Γ₁}{Γ₂}{φ₁})

    [⊢]-id : ∀{Γ}{φ} → (φ ∈ Γ) → (Γ ⊢ φ)
    [⊢]-id (φ-in) = [⊢]-construct ([∈]-proof ↦ [∈]-proof (φ-in))
    -- ((A → B) → B) → C
    -- f(g ↦ g(x))

    -- Almost like that cut rule.
    [⊢]-compose : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → ((φ₁ ⊰ Γ) ⊢ φ₂) → (Γ ⊢ φ₂)
    [⊢]-compose ([Γ]⊢[φ₁]) ([φ₁Γ]⊢[φ₂]) =
      [⊢]-construct ([Γ]-trees ↦
        let [φ₁]-tree = [⊢]-apply ([Γ]⊢[φ₁]) (\{γ} → [Γ]-trees {γ})
            [Γ]⊢[φ₂]  = [⊢]-apply-first ([φ₁]-tree) ([φ₁Γ]⊢[φ₂])
        in [⊢]-apply ([Γ]⊢[φ₂]) (\{γ} → [Γ]-trees {γ})
      )
    -- TODO: ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → ((φ₁ ∈ Γ) → (Γ ⊢ φ₂)) → (Γ ⊢ φ₂) Provable?

    [⊢]-membership-precedingₗ : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∈ Γ) → (Γ ⊢ φ₂)) ← ((φ₁ ⊰ Γ) ⊢ φ₂)
    [⊢]-membership-precedingₗ{Γ}{φ₁}{φ₂} ([φ₁Γ]⊢[φ₂]) ([φ₁]-in) =
      [⊢]-construct([Γ]-trees ↦
        [⊢]-apply ([φ₁Γ]⊢[φ₂]) (Trees.push ([Γ]-trees [φ₁]-in) (\{γ} → [Γ]-trees {γ}))
      )

    {- TODO: Maybe this is unprovable? And also false?
    postulate a : ∀{b : Set(ℓₚ)} → b
    [⊢]-membership-precedingᵣ : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∈ Γ) → (Γ ⊢ φ₂)) → ((φ₁ ⊰ Γ) ⊢ φ₂)
    [⊢]-membership-precedingᵣ{Γ}{φ₁}{φ₂} (incl) =
      [⊢]-construct ([φ₁Γ]-trees ↦
        let [Γ]-trees = Trees.pop (\{γ} → [φ₁Γ]-trees {γ})
            [φ₁]-in = a
            [Γ]⊢[φ₂] = incl([φ₁]-in)
        in [⊢]-apply ([Γ]⊢[φ₂]) ([Γ]-trees)
      )
    -}

    [⊢][⊤]-intro : ∀{Γ} → (Γ ⊢ ⊤)
    [⊢][⊤]-intro =
      [⊢]-construct(const [⊤]-intro)

    [⊢][⊥]-intro : ∀{Γ}{φ} → (φ ∈ Γ) → ((¬ φ) ∈ Γ) → (Γ ⊢ ⊥)
    [⊢][⊥]-intro ([φ]-in) ([¬φ]-in) =
      [⊢]-construct(assumption-trees ↦
        ([⊥]-intro
          (assumption-trees ([φ]-in))
          (assumption-trees ([¬φ]-in))
        )
      )

    [⊢][⊥]-elim : ∀{Γ}{φ} → (⊥ ∈ Γ) → (Γ ⊢ φ)
    [⊢][⊥]-elim ([⊥]-in) =
      [⊢]-construct(assumption-trees ↦
        ([⊥]-elim
          (assumption-trees ([⊥]-in))
        )
      )

    [⊢][¬]-intro : ∀{Γ}{φ} → ((φ ⊰ Γ) ⊢ ⊥) → (Γ ⊢ (¬ φ))
    [⊢][¬]-intro ([⊢]-construct φΓ⊢⊥) =
      [⊢]-construct(assumption-trees ↦
        ([¬]-intro (φ-tree ↦
          (φΓ⊢⊥) (Trees.push (φ-tree) (\{γ} → assumption-trees {γ}))
        ))
      )

    [⊢][¬]-elim : ∀{Γ}{φ} → (((¬ φ) ⊰ Γ) ⊢ ⊥) → (Γ ⊢ φ)
    [⊢][¬]-elim ([⊢]-construct ¬φΓ⊢⊥) =
      [⊢]-construct(assumption-trees ↦
        ([¬]-elim (φ-tree ↦
          (¬φΓ⊢⊥) (Trees.push (φ-tree) (\{γ} → assumption-trees {γ}))
        ))
      )

    [⊢][∧]-intro : ∀{Γ}{φ₁ φ₂} → (φ₁ ∈ Γ) → (φ₂ ∈ Γ) → (Γ ⊢ (φ₁ ∧ φ₂))
    [⊢][∧]-intro ([φ₁]-in) ([φ₂]-in) =
      [⊢]-construct(assumption-trees ↦
        ([∧]-intro
          (assumption-trees ([φ₁]-in))
          (assumption-trees ([φ₂]-in))
        )
      )

    [⊢][∧]-elimₗ : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∧ φ₂) ∈ Γ) → (Γ ⊢ φ₁)
    [⊢][∧]-elimₗ ([φ₁∧φ₂]-in) =
      [⊢]-construct(assumption-trees ↦
        [∧]-elimₗ (assumption-trees ([φ₁∧φ₂]-in))
      )

    [⊢][∧]-elimᵣ : ∀{Γ}{φ₁ φ₂} → ((φ₁ ∧ φ₂) ∈ Γ) → (Γ ⊢ φ₂)
    [⊢][∧]-elimᵣ ([φ₁∧φ₂]-in) =
      [⊢]-construct(assumption-trees ↦
        [∧]-elimᵣ (assumption-trees ([φ₁∧φ₂]-in))
      )

    [⊢][∨]-introₗ : ∀{Γ}{φ₁ φ₂} → (φ₁ ∈ Γ) → (Γ ⊢ (φ₁ ∨ φ₂))
    [⊢][∨]-introₗ ([φ₁]-in) =
      [⊢]-construct(assumption-trees ↦
        [∨]-introₗ (assumption-trees ([φ₁]-in))
      )

    [⊢][∨]-introᵣ : ∀{Γ}{φ₁ φ₂} → (φ₂ ∈ Γ) → (Γ ⊢ (φ₁ ∨ φ₂))
    [⊢][∨]-introᵣ ([φ₂]-in) =
      [⊢]-construct(assumption-trees ↦
        [∨]-introᵣ (assumption-trees ([φ₂]-in))
      )

    [⊢][∨]-elim : ∀{Γ₁ Γ₂}{φ₁ φ₂ φ₃} → ((φ₁ ⊰ Γ₁) ⊢ φ₃) → ((φ₂ ⊰ Γ₂) ⊢ φ₃) → (((φ₁ ∨ φ₂) ⊰ (Γ₁ ++ Γ₂)) ⊢ φ₃)
    [⊢][∨]-elim {Γ₁}{Γ₂} ([⊢]-construct φ₁Γ⊢φ₃) ([⊢]-construct φ₂Γ⊢φ₃) = [⊢]-construct
      (assumption-trees ↦ [∨]-elim
        (φ₁-tree ↦ (φ₁Γ⊢φ₃) (Trees.push (φ₁-tree) (Trees.[++]-left  {Γ₁}{Γ₂} (Trees.pop (\{γ} → assumption-trees {γ})))))
        (φ₂-tree ↦ (φ₂Γ⊢φ₃) (Trees.push (φ₂-tree) (Trees.[++]-right {Γ₁}{Γ₂} (Trees.pop (\{γ} → assumption-trees {γ})))))
        (assumption-trees (use))
      )

    [⊢][⇒]-intro : ∀{Γ}{φ₁ φ₂} → ((φ₁ ⊰ Γ) ⊢ φ₂) → (Γ ⊢ (φ₁ ⇒ φ₂))
    [⊢][⇒]-intro ([⊢]-construct φ₁Γ⊢φ₂) = [⊢]-construct
      (assumption-trees ↦ [⇒]-intro
        (φ-tree ↦ (φ₁Γ⊢φ₂) (Trees.push (φ-tree) (\{γ} → assumption-trees {γ})))
      )

    [⊢][⇒]-elim : ∀{Γ}{φ₁ φ₂} → ((φ₁ ⇒ φ₂) ∈ Γ) → (φ₁ ∈ Γ) → (Γ ⊢ φ₂)
    [⊢][⇒]-elim ([φ₁⇒φ₂]-in) ([φ₁]-in) =
      [⊢]-construct(assumption-trees ↦
        [⇒]-elim
          (assumption-trees ([φ₁⇒φ₂]-in))
          (assumption-trees ([φ₁]-in))
      )

    -- [⊢]-metaᵣ : ∀{a}{b} → _⊢_ a b → Meta._⊢_ a b
    -- [⊢]-metaₗ : ∀{a}{b} → _⊢_ a b ← Meta._⊢_ a b

    {-[⊢]-rules : Meta.[⊢]-rules (_⊢_)
    [⊢]-rules =
      record{
        [⊤]-intro  = \{Γ} → [⊢][⊤]-intro {Γ} ;
        [⊥]-intro  = \{Γ}{φ} → [⊢][⊥]-intro {Γ}{φ} ;
        [⊥]-elim   = \{Γ}{φ} → [⊢][⊥]-elim {Γ}{φ} ;
        [¬]-intro  = \{Γ}{φ} → [⊢][¬]-intro {Γ}{φ} ;
        [¬]-elim   = \{Γ}{φ} → [⊢][¬]-elim {Γ}{φ} ;
        [∧]-intro  = \{Γ}{φ₁}{φ₂} → [⊢][∧]-intro {Γ}{φ₁}{φ₂} ;
        [∧]-elimₗ  = \{Γ}{φ₁}{φ₂} → [⊢][∧]-elimₗ {Γ}{φ₁}{φ₂} ;
        [∧]-elimᵣ  = \{Γ}{φ₁}{φ₂} → [⊢][∧]-elimᵣ {Γ}{φ₁}{φ₂} ;
        [∨]-introₗ = \{Γ}{φ₁}{φ₂} → [⊢][∨]-introₗ {Γ}{φ₁}{φ₂} ;
        [∨]-introᵣ = \{Γ}{φ₁}{φ₂} → [⊢][∨]-introᵣ {Γ}{φ₁}{φ₂} ;
        [∨]-elim   = \{Γ₁}{Γ₂}{φ₁ φ₂ φ₃} → [⊢][∨]-elim {Γ₁}{Γ₂}{φ₁}{φ₂}{φ₃} ;
        [⇒]-intro  = \{Γ}{φ₁}{φ₂} → [⊢][⇒]-intro {Γ}{φ₁}{φ₂} ;
        [⇒]-elim   = \{Γ}{φ₁}{φ₂} → [⊢][⇒]-elim {Γ}{φ₁}{φ₂}
      }
    -}

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 nodcap.NF.Axiom where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺
open import Data.List as L using (List; []; _∷_; _++_)
open import Function using (_$_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Data.Environment
open import nodcap.Base
open import nodcap.NF.Typing

{-# TERMINATING #-}
-- Theorem:
--   Identity expansion.
--
-- Problematic calls:
--   * in the recursive calls under ⅋n and ⊗n, it is the
--     size of the resource index which is decreasing, not
--     the size of the type itself.
ax : {A : Type} → ⊢ⁿᶠ A ∷ A ^ ∷ []
ax { 𝟏 }
  = exch (bbl [])
  $ wait halt
ax { ⊥ }
  = wait halt
ax { 𝟎 }
  = exch (bbl [])
  $ loop
ax { ⊤ }
  = loop
ax { A ⊗ B }
  = exch (bbl [])
  $ recv
  $ exch (bwd [] (_ ∷ _ ∷ []))
  $ send ax ax
ax { A ⅋ B }
  = recv
  $ exch (bwd [] (_ ∷ _ ∷ []))
  $ send
  ( exch (bbl []) ax )
  ( exch (bbl []) ax )
ax { A ⊕ B }
  = exch (bbl [])
  $ case
  ( exch (bbl [])
  $ sel₁ ax
  )
  ( exch (bbl [])
  $ sel₂ ax
  )
ax { A & B }
  = case
  ( exch (bbl [])
  $ sel₁
  $ exch (bbl []) ax
  )
  ( exch (bbl [])
  $ sel₂
  $ exch (bbl []) ax
  )
ax { ![ suc zero ] A }
  = mk!₁
  $ exch (bbl [])
  $ mk?₁
  $ exch (bbl []) ax
ax { ![ suc (suc n) ] A }
  = exch (bbl [])
  $ cont {m = 1} {n = suc n}
  $ exch (bwd [] (_ ∷ _ ∷ []))
  $ pool {m = 1} {n = suc n}
  ( ax )
  ( ax )
ax { ?[ suc zero ] A }
  = mk?₁
  $ exch (bbl [])
  $ mk!₁
  $ exch (bbl []) ax
ax { ?[ suc (suc n) ] A }
  = cont {m = 1} {n = suc n}
  $ exch (bwd [] (_ ∷ _ ∷ []))
  $ pool {m = 1} {n = suc n}
  ( exch (bbl []) ax )
  ( exch (bbl []) ax )

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
module Levitation where

open import Data.Product

record ⊤ : Set1 where
  constructor tt

data Desc : Set2 where
  `1 : Desc
  `Σ : (S : Set1)(D : S → Desc) → Desc
  `ind× : (D : Desc) → Desc
  `hind× : (H : Set)(D : Desc) → Desc

⟦_⟧ : Desc → Set1 → Set1
⟦ `1 ⟧ X          = ⊤
⟦ `Σ S D ⟧ X      = Σ S (\s → ⟦ D s ⟧ X)
⟦ `ind× D ⟧ X     =  X × ⟦ D ⟧ X
⟦ `hind× H D ⟧ X  = (H → X) × ⟦ D ⟧ X

data Mu (D : Desc) : Set1 where
  con : ⟦ D ⟧ (Mu D) → Mu D

data DescDConst : Set1 where
  ``1 : DescDConst
  ``Σ : DescDConst
  ``ind× : DescDConst
  ``hind× : DescDConst

DescDChoice : DescDConst → Desc
DescDChoice ``1 = `1
DescDChoice ``Σ = `Σ Set (\S → `hind× S `1)
DescDChoice ``ind× = `ind× `1
DescDChoice ``hind× = `Σ Set (\_ → `ind× `1)

DescD : Desc
DescD = `Σ DescDConst DescDChoice

Desc' : Set1
Desc' = Mu DescD

`1' : Desc'
`1' = con (``1 , tt)

`Σ' : (S : Set)(D : S → Desc') → Desc'
`Σ' S D = con (``Σ , (S , (D , tt)))

`ind×' : (D : Desc') → Desc'
`ind×' D = con (``ind× , (D , tt))

`hind×' : (H : Set)(D : Desc') → Desc'
`hind×' H D = con (``hind× , (H , (D , tt)))

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2020-10-08
-- Connective
-- Author: dplaindoux
--

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

module Connective where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import Isomorphism using (_≃_; _≲_; extensionality)
open Isomorphism.≃-Reasoning

data _×_ (A B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B
proj₂ ⟨ x , y ⟩ = y

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
module Generic.Test.Elim where

open import Generic.Core
open import Generic.Function.Elim
open import Generic.Test.Data.Vec

-- Is it possible to get rid of these `lift`s?
elimVec′ : ∀ {n α π} {A : Set α}
         -> (P : ∀ {n} -> Vec A n -> Set π)
         -> (∀ {n} {xs : Vec A n} x -> P xs -> P (x ∷ᵥ xs))
         -> P []ᵥ
         -> (xs : Vec A n)
         -> P xs
elimVec′ P f z = elim P (lift z , λ x r -> lift (f x r))

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
------------------------------------------------------------------------
-- Some corollaries
------------------------------------------------------------------------

module TotalParserCombinators.Derivative.Corollaries where

open import Data.List
open import Function.Base
open import Function.Inverse using (_↔_)
import Function.Related as Related
import Relation.Binary.PropositionalEquality as P

open Related using (SK-sym)

open import TotalParserCombinators.Derivative.Definition
open import TotalParserCombinators.Derivative.LeftInverse
open import TotalParserCombinators.Derivative.RightInverse
open import TotalParserCombinators.Derivative.SoundComplete
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

-- D is correct.

correct : ∀ {Tok R xs x s} {t} {p : Parser Tok R xs} →
          x ∈ D t p · s ↔ x ∈ p · t ∷ s
correct {p = p} = record
  { to         = P.→-to-⟶ $ sound p
  ; from       = P.→-to-⟶ complete
  ; inverse-of = record
    { left-inverse-of  = complete∘sound p
    ; right-inverse-of = sound∘complete
    }
  }

-- D is monotone.

mono : ∀ {Tok R xs₁ xs₂ t}
         {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
       p₁ ≲ p₂ → D t p₁ ≲ D t p₂
mono p₁≲p₂ = complete ∘ p₁≲p₂ ∘ sound _

-- D preserves parser and language equivalence.

cong : ∀ {k Tok R xs₁ xs₂}
         {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
       p₁ ∼[ k ] p₂ → ∀ {t} → D t p₁ ∼[ k ] D t p₂
cong {p₁ = p₁} {p₂} p₁≈p₂ {t} {x} {s} =
  x ∈ D t p₁ · s  ↔⟨ correct ⟩
  x ∈ p₁ · t ∷ s  ∼⟨ p₁≈p₂ ⟩
  x ∈ p₂ · t ∷ s  ↔⟨ SK-sym correct ⟩
  x ∈ D t p₂ · s  ∎
  where open Related.EquationalReasoning

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --safe --sized-types #-}
module STLC.Operational where

open import STLC.Operational.Base

max_stars_repo_name: TypesLogicsCats/STLC

max_issues_repo_name: TrulyNonstrict/STLC

max_forks_repo_name: TrulyNonstrict/STLC


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

module WithoutK-PatternSynonyms2 where

-- Equality defined with two indices.
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

pattern r x = refl x

-- The --cubical-compatible option works with pattern synonyms.
K : (A : Set) (x : A) (P : x ≡ x → Set) → P (refl x) → (p : x ≡ x ) →  P p
K A .x P pr (r x) = pr


text:
open import Relation.Binary.Core

module BBHeap.Insert {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Properties _≤_
open import BBHeap.Subtyping.Properties _≤_ trans≤
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Bound.Lower.Order.Properties _≤_ trans≤
open import Data.Sum renaming (_⊎_ to _∨_)
open import Order.Total _≤_ tot≤

mutual
  insert : {b : Bound}{x : A} → LeB b (val x) → BBHeap b → BBHeap b
  insert b≤x leaf = left b≤x lf⋘
  insert {x = x} b≤x (left {x = y} b≤y l⋘r)
      with tot≤ x y
  ... | inj₁ x≤y
      with lemma-insert⋘ (lexy refl≤) l⋘r
  ... | inj₁ lᵢ⋘r = left b≤x (subtyping⋘ (lexy x≤y) (lexy x≤y) lᵢ⋘r)
  ... | inj₂ lᵢ⋗r = right b≤x (subtyping⋙ (lexy x≤y) (lexy x≤y) (lemma⋗ lᵢ⋗r))
  insert {x = x} b≤x (left {x = y} b≤y l⋘r) | inj₂ y≤x
      with lemma-insert⋘ (lexy y≤x) l⋘r
  ... | inj₁ lᵢ⋘r = left b≤y lᵢ⋘r
  ... | inj₂ lᵢ⋗r = right b≤y (lemma⋗ lᵢ⋗r)
  insert {x = x} b≤x (right {x = y} b≤y l⋙r)
      with tot≤ x y
  ... | inj₁ x≤y
      with lemma-insert⋙ (lexy refl≤) l⋙r
  ... | inj₁ l⋙rᵢ = right b≤x (subtyping⋙ (lexy x≤y) (lexy x≤y) l⋙rᵢ)
  ... | inj₂ l≃rᵢ = left b≤x (subtyping⋘ (lexy x≤y) (lexy x≤y) (lemma≃ l≃rᵢ))
  insert {x = x} b≤x (right {x = y} b≤y l⋙r) | inj₂ y≤x
      with lemma-insert⋙ (lexy y≤x) l⋙r
  ... | inj₁ l⋙rᵢ = right b≤y l⋙rᵢ
  ... | inj₂ l≃rᵢ = left b≤y (lemma≃ l≃rᵢ)

  lemma-insert⋘ : {b b' : Bound}{x : A}{h : BBHeap b}{h' : BBHeap b'} → (b≤x : LeB b (val x)) → h ⋘ h' → insert b≤x h ⋘ h' ∨ insert b≤x h ⋗ h'
  lemma-insert⋘ b≤x lf⋘ = inj₂ (⋗lf b≤x)
  lemma-insert⋘ {x = x} b≤x (ll⋘ {x = y} b≤y b'≤y' l⋘r l'⋘r' l'≃r' r≃l')
      with tot≤ x y
  ... | inj₁ x≤y
      with lemma-insert⋘ (lexy refl≤) l⋘r
  ... | inj₁ lᵢ⋘r = inj₁ (ll⋘ b≤x b'≤y' (subtyping⋘ (lexy x≤y) (lexy x≤y) lᵢ⋘r) l'⋘r' l'≃r' (subtyping≃l (lexy x≤y) r≃l'))
  ... | inj₂ lᵢ⋗r = inj₁ (lr⋘ b≤x b'≤y' (subtyping⋙ (lexy x≤y) (lexy x≤y) (lemma⋗ lᵢ⋗r)) l'⋘r' l'≃r' (subtyping⋗l (lexy x≤y) (lemma⋗≃ lᵢ⋗r r≃l')))
  lemma-insert⋘ {x = x} b≤x (ll⋘ {x = y} b≤y b'≤y' l⋘r l'⋘r' l'≃r' r≃l') | inj₂ y≤x
      with lemma-insert⋘ (lexy y≤x) l⋘r
  ... | inj₁ lᵢ⋘r = inj₁ (ll⋘ b≤y b'≤y' lᵢ⋘r l'⋘r' l'≃r' r≃l')
  ... | inj₂ lᵢ⋗r = inj₁ (lr⋘ b≤y b'≤y' (lemma⋗ lᵢ⋗r) l'⋘r' l'≃r' (lemma⋗≃ lᵢ⋗r r≃l'))
  lemma-insert⋘ {x = x} b≤x (lr⋘ {x = y} b≤y b'≤y' l⋙r l'⋘r' l'≃r' l⋗l')
      with tot≤ x y
  ... | inj₁ x≤y
      with lemma-insert⋙ (lexy refl≤) l⋙r
  ... | inj₁ l⋙rᵢ = inj₁ (lr⋘ b≤x b'≤y' (subtyping⋙ (lexy x≤y) (lexy x≤y) l⋙rᵢ) l'⋘r' l'≃r' (subtyping⋗l (lexy x≤y) l⋗l'))
  ... | inj₂ l≃rᵢ = inj₂ (⋗nd b≤x b'≤y' (subtyping⋘ (lexy x≤y) (lexy x≤y) (lemma≃ l≃rᵢ)) l'⋘r' (subtyping≃ (lexy x≤y) (lexy x≤y) l≃rᵢ) l'≃r' (subtyping⋗l (lexy x≤y) l⋗l'))
  lemma-insert⋘ {x = x} b≤x (lr⋘ {x = y} b≤y b'≤y' l⋙r l'⋘r' l'≃r' l⋗l') | inj₂ y≤x
      with lemma-insert⋙ (lexy y≤x) l⋙r
  ... | inj₁ l⋙rᵢ = inj₁ (lr⋘ b≤y b'≤y' l⋙rᵢ l'⋘r' l'≃r' l⋗l')
  ... | inj₂ l≃rᵢ = inj₂ (⋗nd b≤y b'≤y' (lemma≃ l≃rᵢ) l'⋘r' l≃rᵢ l'≃r' l⋗l')

  lemma-insert⋙ : {b b' : Bound}{x : A}{h : BBHeap b}{h' : BBHeap b'} → (b'≤x : LeB b' (val x)) → h ⋙ h' → h ⋙ insert b'≤x h' ∨ h ≃ insert b'≤x h'
  lemma-insert⋙ {x = x} b'≤x (⋙lf {x = y} b≤y) = inj₂ (≃nd b≤y b'≤x lf⋘ lf⋘ ≃lf ≃lf ≃lf)
  lemma-insert⋙ {x = x} b'≤x (⋙rl {x' = y'} b≤y b'≤y' l⋘r l≃r l'⋘r' l⋗r')
      with tot≤ x y'
  ... | inj₁ x≤y'
      with lemma-insert⋘ (lexy refl≤) l'⋘r'
  ... | inj₁ l'ᵢ⋘r' = inj₁ (⋙rl b≤y b'≤x l⋘r l≃r (subtyping⋘ (lexy x≤y') (lexy x≤y') l'ᵢ⋘r') (subtyping⋗r (lexy x≤y') l⋗r'))
  ... | inj₂ l'ᵢ⋗r' = inj₁ (⋙rr b≤y b'≤x l⋘r l≃r (subtyping⋙ (lexy x≤y') (lexy x≤y') (lemma⋗ l'ᵢ⋗r')) (subtyping≃r (lexy x≤y') (lemma⋗⋗ l⋗r' l'ᵢ⋗r')))
  lemma-insert⋙ {x = x} b'≤x (⋙rl {x' = y'} b≤y b'≤y' l⋘r l≃r l'⋘r' l⋗r') | inj₂ y'≤x
      with lemma-insert⋘ (lexy y'≤x) l'⋘r'
  ... | inj₁ l'ᵢ⋘r' = inj₁ (⋙rl b≤y b'≤y' l⋘r l≃r l'ᵢ⋘r' l⋗r')
  ... | inj₂ l'ᵢ⋗r' = inj₁ (⋙rr b≤y b'≤y' l⋘r l≃r (lemma⋗ l'ᵢ⋗r') (lemma⋗⋗ l⋗r' l'ᵢ⋗r'))
  lemma-insert⋙ {x = x} b'≤x (⋙rr {x' = y'} b≤y b'≤y' l⋘r l≃r l'⋙r' l≃l')
      with tot≤ x y'
  ... | inj₁ x≤y'
      with lemma-insert⋙ (lexy refl≤) l'⋙r'
  ... | inj₁ l'⋙r'ᵢ = inj₁ (⋙rr b≤y b'≤x l⋘r l≃r (subtyping⋙ (lexy x≤y') (lexy x≤y') l'⋙r'ᵢ) (subtyping≃r (lexy x≤y') l≃l'))
  ... | inj₂ l'≃r'ᵢ = inj₂ (≃nd b≤y b'≤x l⋘r (subtyping⋘ (lexy x≤y') (lexy x≤y') (lemma≃ l'≃r'ᵢ)) l≃r (subtyping≃ (lexy x≤y') (lexy x≤y') l'≃r'ᵢ) (subtyping≃r (lexy x≤y') l≃l'))
  lemma-insert⋙ {x = x} b'≤x (⋙rr {x' = y'} b≤y b'≤y' l⋘r l≃r l'⋙r' l≃l') | inj₂ y'≤x
      with lemma-insert⋙ (lexy y'≤x) l'⋙r'
  ... | inj₁ l'⋙r'ᵢ = inj₁ (⋙rr b≤y b'≤y' l⋘r l≃r l'⋙r'ᵢ l≃l')
  ... | inj₂ l'≃r'ᵢ = inj₂ (≃nd b≤y b'≤y' l⋘r (lemma≃ l'≃r'ᵢ) l≃r l'≃r'ᵢ l≃l')

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- Some definitions related to the binary sum type former
------------------------------------------------------------------------

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

open import Equality

module Sum {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude

private
  variable
    a           : Level
    A B         : Type a
    x           : A
    f₁ f₂ g₁ g₂ : A → B

-- Functor laws.

⊎-map-id : ⊎-map id id x ≡ x
⊎-map-id {x = inj₁ _} = refl _
⊎-map-id {x = inj₂ _} = refl _

⊎-map-∘ :
  ∀ x → ⊎-map (f₁ ∘ g₁) (f₂ ∘ g₂) x ≡ ⊎-map f₁ f₂ (⊎-map g₁ g₂ x)
⊎-map-∘ = [ (λ _ → refl _) , (λ _ → refl _) ]

-- If A can be decided, then ¬ A can be decided.

dec-¬ : Dec A → Dec (¬ A)
dec-¬ (yes p) = no (_$ p)
dec-¬ (no  p) = yes p

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module StdLibStuff where

{-
-- Data.Empty

data ⊥ : Set where

-- Relation.Nullary.Core

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

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

-- Relation.Binary.Core

infix 4 _≡_  -- _≢_

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

{-
_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y = ¬ x ≡ y

Decidable : {A : Set} → Set
Decidable {A} = (x y : A) → Dec (x ≡ y)
-}

-- equality properties

sym : {A : Set} → {x y : A} → x ≡ y → y ≡ x
sym refl = refl

subst : {A : Set} → {x y : A} → (p : A → Set) → x ≡ y → p x → p y
subst p refl h = h

cong : {A B : Set} → {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

trans : {A : Set} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl h = h

{-
-- Data.List

infixr 5 _∷_

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

data List₁ (A : Set₁) : Set₁ where
  []  : List₁ A
  _∷_ : (x : A) (xs : List₁ A) → List₁ A
-}

-- Data.Bool

infixr 5 _∨_

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

{-
-- Data.Product

infixr 4 _,_ _,′_

infixr 2 _×_

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

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

-- nondep product

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

open _×_ public

_,′_ : {A B : Set} → A → B → A × B
_,′_ = _,_

∃ : ∀ {A : Set} → (A → Set) → Set
∃ = Σ _

∃₁ : ∀ {A : Set₁} → (A → Set) → Set₁
∃₁ = Σ₁ _
-}

-- Data.Nat

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

-- Data.Fin

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

{-
-- Data.Vec

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

data Vec₁ (A : Set₁) : ℕ → Set₁ where
  []  : Vec₁ A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec₁ A n) → Vec₁ A (suc n)

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

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

-- Data.Sum

infixr 1 _⊎_

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

[_,_]′ : ∀ {A : Set} {B : Set} {C : Set} →
         (A → C) → (B → C) → (A ⊎ B → C)
[_,_]′ h₁ h₂ (inj₁ x) = h₁ x
[_,_]′ h₁ h₂ (inj₂ y) = h₂ y

--

_↔_ : Set → Set → Set
X ↔ Y = (X → Y) × (Y → X)

-- Misc

record ⊤ : Set where

-}

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


text:
-- Andreas, 2021-04-14, #1154
-- Andreas, 2021-04-12, BNFC/bnfc#354
-- Make sure we confirm tentative layout columns on first newline.

private private private A : Set
                        B : Set  -- all three blocks (8,16,24) should be confirmed here
                private          -- the column for this block needs to be > 16
  Bad : Set                      -- bad indentation, needs to be 0,8,16 or greater

-- Expected: Parse error after Bad

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module LC.Base where

open import Data.Nat

--------------------------------------------------------------------------------
-- de Bruijn indexed lambda calculus
infix  5 ƛ_
infixl 7 _∙_
infix  9 var_

data Term : Set where
  var_  : (x : ℕ) → Term
  ƛ_    : (M : Term) → Term
  _∙_   : (M : Term) → (N : Term) → Term

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
module posts.agda.typed-protocols where

open import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List
open import Data.Nat
open import Data.Unit using (⊤; tt)
open import Function.Base using (_$_; _|>_)

-- Client / server roles
--
data PeerRole : Set where
  ClientRole : PeerRole
  ServerRole : PeerRole

dual-role : PeerRole → PeerRole
dual-role ClientRole = ServerRole
dual-role ServerRole = ClientRole

-- Objective agency: who is responsible for sending next message.
--
data Agency : Set where
  ClientAgency : Agency
  ServerAgency : Agency
  NobodyAgency : Agency

-- Relative agency to the current 'PeerRole'.  It answer the question: are we
-- responsible for sending next message?
--
data RelativeAgency : Set where
  WeHaveAgency    : RelativeAgency
  TheyHaveAgency  : RelativeAgency
  NobodyHasAgency : RelativeAgency

relative : PeerRole   → Agency       → RelativeAgency

relative   ClientRole   ClientAgency = WeHaveAgency
relative   ClientRole   ServerAgency = TheyHaveAgency
relative   ClientRole   NobodyAgency = NobodyHasAgency

relative   ServerRole   ClientAgency = TheyHaveAgency
relative   ServerRole   ServerAgency = WeHaveAgency
relative   ServerRole   NobodyAgency = NobodyHasAgency

-- 'relative' function obeys the following three exclusion lemmas:
--
-- * it is an absurd if client and server have agency
-- * it is an absurd if 'WeHaveAgency'   and the dual role terminated
--   ('NobodyHasAgency')
-- * it is an absurd if 'TheyHaveAgency' and the dual role terminated
--   ('NobodyHasAgency')
--
-- Note that these lemmas are provided regardless of the protocol, unlike the
-- Haskell implementation which requires to prove them for each protocol.

exclusion-lemma-client-and-server-have-agency₁
  : ∀ {agency : Agency}
      {pr     : PeerRole}
  → WeHaveAgency ≡ relative            pr  agency
  → WeHaveAgency ≡ relative (dual-role pr) agency
  → ⊥
exclusion-lemma-client-and-server-have-agency₁
  {ClientAgency}
  {ClientRole}
  refl ()
exclusion-lemma-client-and-server-have-agency₁
  {ServerAgency}
  {ServerRole}
  refl ()

exclusion-lemma-client-and-server-have-agency₂
  : ∀ {agency : Agency}
      {pr     : PeerRole}
  → TheyHaveAgency ≡ relative            pr  agency
  → TheyHaveAgency ≡ relative (dual-role pr) agency
  → ⊥
exclusion-lemma-client-and-server-have-agency₂
  {ServerAgency}
  {ClientRole}
  refl ()
exclusion-lemma-client-and-server-have-agency₂
  {ClientAgency}
  {ServerRole}
  refl ()

exclusion-lemma-we-have-agency-and-nobody-has-agency
  : ∀ {agency  : Agency}
      {pr      : PeerRole}
      {pr'     : PeerRole}
  → WeHaveAgency    ≡ relative pr  agency
  → NobodyHasAgency ≡ relative pr' agency
  → ⊥
exclusion-lemma-we-have-agency-and-nobody-has-agency
  {ClientAgency}
  {ClientRole}
  {ServerRole}
  refl ()
exclusion-lemma-we-have-agency-and-nobody-has-agency
  {ServerAgency}
  {ServerRole}
  {ClientRole}
  refl ()

exclusion-lemma-they-have-agency-and-nobody-has-agency
  : ∀ {agency : Agency}
      {pr     : PeerRole}
      {pr'    : PeerRole}
  → TheyHaveAgency  ≡ relative pr  agency
  → NobodyHasAgency ≡ relative pr' agency
  → ⊥
exclusion-lemma-they-have-agency-and-nobody-has-agency
  {ServerAgency}
  {ClientRole}
  {ServerRole}
  refl ()
exclusion-lemma-they-have-agency-and-nobody-has-agency
  {ClientAgency}
  {ServerRole}
  {ClientRole}
  refl ()

-----------
-- Peer API
--

-- We index each primitive with 'IsPipelined'
--
data IsPipelined : Set where
  Pipelined    : IsPipelined
  NonPipelined : IsPipelined

-- Promised protocol transition
--
data Trans (ps : Set) : Set where
  Tr : ps → ps → Trans ps

-- 'Peer' explicitly indexed by:
-- * message type
-- * objective protocol agency
-- * peer role
-- * return type
-- * 'IsPipelined'
-- * queue of unrealised transitions, due to pipelining
-- * current state
--
data Peer {ps     : Set}
          (msg    : ps → ps → Set)
          (agency : ps → Agency)
          (pr     : PeerRole)
          (a      : Set)
        : IsPipelined
        → List (Trans ps)
        → ps
        → Set where

  --
  -- non-pipelined primitives
  --

  -- non-pipelined send a message
  Yield : ∀ {st st' : ps}
            {pl     : IsPipelined}
        → WeHaveAgency ≡ relative pr (agency st)
        → msg st st'
        → Peer msg agency pr a pl [] st'
        → Peer msg agency pr a pl [] st

  -- non-pipelined receive a message
  Await : ∀ {st : ps}
            {pl : IsPipelined}
        → TheyHaveAgency ≡ relative pr (agency st)
        → (∀ {st' : ps}
           → msg st st'
           → Peer msg agency pr a pl [] st'
          )
        → Peer    msg agency pr a pl [] st

  -- protocol termination
  Done  : ∀ {st : ps}
            {pl : IsPipelined}
        → NobodyHasAgency ≡ relative pr (agency st)
        → a
        → Peer msg agency pr a pl [] st

  --
  -- pipelining primitives
  --

  -- pipeline a single message
  YieldPipelined
        : ∀ {st st' st'' : ps}
            {q           : List (Trans ps)}
        → WeHaveAgency ≡ relative pr (agency st)
        → msg st st'
        → Peer msg agency pr a Pipelined (q ∷ʳ Tr st' st'') st''
        → Peer msg agency pr a Pipelined  q                 st

  -- partially collect a promissed transition
  Collect
        : ∀ {st st' st'' : ps}
            {q           : List (Trans ps)}
        → TheyHaveAgency ≡ relative pr (agency st')
        → (∀ {stNext : ps}
           → msg st' stNext
           → Peer msg agency pr a Pipelined (Tr stNext st'' ∷ q) st
          )
        → Peer    msg agency pr a Pipelined (Tr st'    st'' ∷ q) st

  -- collect the identity transition
  CollectDone
        : ∀ {st : ps}
            {q  : List (Trans ps)}
        → Peer msg agency pr a Pipelined             q  st
        → Peer msg agency pr a Pipelined (Tr st st ∷ q) st

--------------
-- PingPong v1
--

-- Protocol states
--
data PingPong : Set where
  StIdle : PingPong
  StBusy : PingPong
  StDone : PingPong

-- Agency of PingPong states
--
pingPongAgency : PingPong → Agency
pingPongAgency StIdle = ClientAgency
pingPongAgency StBusy = ServerAgency
pingPongAgency StDone = NobodyAgency

-- Protocol messages
--
data PingPongMsg : ∀ (st st' : PingPong) → Set where
  MsgPing : PingPongMsg StIdle StBusy
  MsgPong : PingPongMsg StBusy StIdle
  MsgDone : PingPongMsg StIdle StDone

--
-- PingPong v1, examples
--

-- ping client which computes unit (tt : ⊤)
--
ping : Peer PingPongMsg pingPongAgency ClientRole ⊤ NonPipelined [] StIdle
ping =
      Yield refl MsgPing
    $ await
    $ Yield refl MsgPing
    $ await
    $ Yield refl MsgDone
    $ Done refl tt
  where
    await : Peer PingPongMsg pingPongAgency ClientRole ⊤ NonPipelined [] StIdle
          → Peer PingPongMsg pingPongAgency ClientRole ⊤ NonPipelined [] StBusy
    await k = Await refl λ {MsgPong → k}

-- pipelined client which computes unit (tt : ⊤)
--
pipelinedPing
    : Peer PingPongMsg pingPongAgency ClientRole ⊤ Pipelined [] StIdle
pipelinedPing =
      YieldPipelined refl MsgPing
    $ YieldPipelined refl MsgPing
    $ YieldPipelined refl MsgPing
    $ collect
    $ collect
    $ collect
    $ Yield refl MsgDone
    $ Done  refl tt
  where
    collect : ∀ {q : List (Trans PingPong)}
            → Peer PingPongMsg pingPongAgency ClientRole ⊤ Pipelined q  StIdle
            → Peer PingPongMsg pingPongAgency ClientRole ⊤ Pipelined
                                                 (Tr StBusy StIdle ∷ q) StIdle
    collect k =
      Collect refl λ {MsgPong → CollectDone k}

--------------
-- PingPong v2
--
-- The same states and agency as PingPong v1, but with additional 'MsgBusy'
-- transition.

data PingPongMsg2 : ∀ (st st' : PingPong) → Set where
  MsgPingPong : ∀ {st st' : PingPong}
              → PingPongMsg st st' → PingPongMsg2 st st'
  MsgBusy     : PingPongMsg2 StBusy StBusy

-- we use unbounded recursion in 'pipelinedPing2'
{-# NON_TERMINATING #-}

-- pipelined ping client which computes the number of busy messages
--
pipelinedPing2
    : Peer PingPongMsg2 pingPongAgency ClientRole ℕ Pipelined [] StIdle
pipelinedPing2 =
      YieldPipelined refl (MsgPingPong MsgPing)
    $ YieldPipelined refl (MsgPingPong MsgPing)
    $ YieldPipelined refl (MsgPingPong MsgPing)
    $          collect 0
    $ λ { n1 → collect n1
      λ { n2 → collect n2
      λ { n3 → Yield refl (MsgPingPong MsgDone)
             $ Done  refl n3 }}}
  where
    collect : ∀ {q : List (Trans PingPong)}
            → ℕ
            → (ℕ → Peer PingPongMsg2 pingPongAgency ClientRole ℕ Pipelined q  StIdle)
            → Peer PingPongMsg2 pingPongAgency ClientRole ℕ Pipelined
                                                       (Tr StBusy StIdle ∷ q) StIdle
    collect n k =
      Collect refl
        λ {  MsgBusy              → collect (n + 1) k
          ; (MsgPingPong MsgPong) → CollectDone (k n)
          }

------------------------
-- Non-pipelined Duality
--

-- Termination witness
data Termination (ps     : Set)
                 (agency : ps → Agency)
                 (a      : Set)
                 (b      : Set)
               : Set where
  Terminated : ∀ {st : ps} {pr : PeerRole}
             → a
             → b
             → NobodyHasAgency ≡ relative            pr  (agency st)
             → NobodyHasAgency ≡ relative (dual-role pr) (agency st)
             → Termination ps agency a b

theorem-non-pipelined-duality
  : ∀ {ps     : Set}
      {msg    : ps → ps → Set}
      {agency : ps → Agency}
      {pr     : PeerRole}
      {a      : Set}
      {b      : Set}
      {st     : ps}
  → Peer msg agency            pr  a NonPipelined [] st
  → Peer msg agency (dual-role pr) b NonPipelined [] st
  → Termination ps agency a b

theorem-non-pipelined-duality (Yield _ msg k)  (Await _ k')     =
  theorem-non-pipelined-duality k (k' msg)

theorem-non-pipelined-duality (Await _ k)      (Yield _ msg k') =
  theorem-non-pipelined-duality (k msg) k'

theorem-non-pipelined-duality (Done termA a)   (Done termB b)   =
  Terminated a b termA termB

-- excluded cases

theorem-non-pipelined-duality (Yield weHaveAgency _ _)
                              (Yield theyHaveAgency _ _)  =
  ⊥-elim (exclusion-lemma-client-and-server-have-agency₁ weHaveAgency theyHaveAgency)

theorem-non-pipelined-duality (Await theyHaveAgency _)
                              (Await weHaveAgency _) =
  ⊥-elim (exclusion-lemma-client-and-server-have-agency₂ theyHaveAgency weHaveAgency)

theorem-non-pipelined-duality (Yield weHaveAgency _ _)
                              (Done nobodyHasAgency _) =
  ⊥-elim (exclusion-lemma-we-have-agency-and-nobody-has-agency
            weHaveAgency
            nobodyHasAgency)

theorem-non-pipelined-duality (Done nobodyHasAgency _)
                              (Yield weHaveAgency _ _) =
  ⊥-elim (exclusion-lemma-we-have-agency-and-nobody-has-agency
            weHaveAgency
            nobodyHasAgency)

theorem-non-pipelined-duality (Await theyHaveAgency _)
                              (Done nobodyHasAgency _) =
  ⊥-elim (exclusion-lemma-they-have-agency-and-nobody-has-agency
            theyHaveAgency
            nobodyHasAgency)

theorem-non-pipelined-duality (Done nobodyHasAgency _)
                              (Await theyHaveAgency _) =
  ⊥-elim (exclusion-lemma-they-have-agency-and-nobody-has-agency
            theyHaveAgency
            nobodyHasAgency)

--------------
-- Un-pipeline
--

-- Transition queue which allows to transform pipelined 'Peer' into
-- non-pipelined one.   Pipelined messages are pushed to the end together with
-- promised transitions to be collected.
--
data PrQueue {ps     : Set}
             (msg    : ps → ps → Set)
             (agency : ps -> Agency)
             (pr     : PeerRole)
           : ps
           → List (Trans ps)
           → ps
           → Set where

  ConsMsgQ : ∀ {st st' st'' : ps}
               {q           : List (Trans ps)}
           → WeHaveAgency ≡ relative pr (agency st)
           → msg st st'
           → PrQueue msg agency pr st' q st''
           → PrQueue msg agency pr st  q st''

  ConsTrQ  : ∀ {st st' st'' : ps}
               {q           : List (Trans ps)}
           → PrQueue msg agency pr st'             q  st''
           → PrQueue msg agency pr st (Tr st st' ∷ q) st''

  EmptyQ   : ∀ {st : ps}
           → PrQueue msg agency pr st [] st

snockMsgQ : ∀ {ps          : Set}
              {msg         : ps → ps → Set}
              {agency      : ps → Agency}
              {pr          : PeerRole}
              {st st' st'' : ps}
              {q           : List (Trans ps)}
          → WeHaveAgency ≡ relative pr (agency st')
          → msg st' st''
          → PrQueue msg agency pr st q st'
          → PrQueue msg agency pr st q st''
snockMsgQ tok msg (ConsMsgQ tok' msg' q) = ConsMsgQ tok' msg' (snockMsgQ tok msg q)
snockMsgQ tok msg (ConsTrQ q)            = ConsTrQ (snockMsgQ tok msg q)
snockMsgQ tok msg  EmptyQ                = ConsMsgQ tok msg EmptyQ

snockTrQ : ∀ {ps          : Set}
             {msg         : ps → ps → Set}
             {agency      : ps → Agency}
             {pr          : PeerRole}
             {st st' st'' : ps}
             {q           : List (Trans ps)}
         → PrQueue msg agency pr st  q st'
         → PrQueue msg agency pr st (q ∷ʳ Tr st' st'') st''
snockTrQ (ConsMsgQ tok msg q) = ConsMsgQ tok msg (snockTrQ q)
snockTrQ (ConsTrQ q)          = ConsTrQ (snockTrQ q)
snockTrQ  EmptyQ              = ConsTrQ EmptyQ

-- Every pipelined peer can be transformed into non-pipelined one, by
-- preserving the order of all transition.
--
theorem-unpipeline
  : ∀ {ps     : Set}
      {msg    : ps → ps → Set}
      {agency : ps → Agency}
      {pr     : PeerRole}
      {pl     : IsPipelined}
      {a      : Set}
      {stInit : ps}
  → Peer msg agency pr a pl           [] stInit
  → Peer msg agency pr a NonPipelined [] stInit
theorem-unpipeline = go EmptyQ
  where
    go : ∀ {ps     : Set}
           {msg    : ps → ps → Set}
           {agency : ps → Agency}
           {pr     : PeerRole}
           {pl     : IsPipelined}
           {a      : Set}
           {q      : List (Trans ps)}
           {st st' : ps}
      → PrQueue msg agency pr             st q  st'
      → Peer    msg agency pr a pl           q  st'
      → Peer    msg agency pr a NonPipelined [] st

    -- non-piplined primitives
    go EmptyQ (Done  tok a)     = Done tok a
    go EmptyQ (Yield tok msg k) = Yield tok msg (go EmptyQ k)
    go EmptyQ (Await tok k)     = Await tok λ {msg → go EmptyQ (k msg)}

    -- push msg and promised transition to back of the 'PrQueue'
    go q      (YieldPipelined tok msg k) =
      go (  q
         |> snockMsgQ tok msg
         |> snockTrQ
         )
         k

    go (ConsMsgQ tok msg q) k =
      Yield tok msg (go q k)

    go (ConsTrQ q) (Collect tok k) =
      Await tok λ {msg → go (ConsTrQ q) (k msg)}

    go (ConsTrQ q) (CollectDone k) =
      go q k

----------
-- Duality
--

theorem-pipelined-duality
  : ∀ {ps     : Set}
      {msg    : ps → ps → Set}
      {agency : ps → Agency}
      {pr     : PeerRole}
      {pl     : IsPipelined}
      {a      : Set}
      {b      : Set}
      {st     : ps}
  → Peer msg agency            pr  a pl [] st
  → Peer msg agency (dual-role pr) b pl [] st
  → Termination ps agency a b
theorem-pipelined-duality a b =
  theorem-non-pipelined-duality (theorem-unpipeline a)
                                (theorem-unpipeline b)

max_stars_repo_name: coot/homepage

max_issues_repo_name: coot/homepage

max_forks_repo_name: coot/homepage


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Pointwise.Extensional directly.
------------------------------------------------------------------------

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

module Data.Vec.Relation.Pointwise.Extensional where

open import Data.Vec.Relation.Binary.Pointwise.Extensional public

{-# WARNING_ON_IMPORT
"Data.Vec.Relation.Pointwise.Extensional was deprecated in v1.0.
Use Data.Vec.Relation.Binary.Pointwise.Extensional instead."
#-}


text:
open import MJ.Types
import MJ.Classtable.Core as Core

module MJ.Classtable.Code {c}(Ct : Core.Classtable c) where

open import Prelude
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Star as Star
open import Data.List
open import Data.List.Relation.Unary.All hiding (construct)
open import Data.List.Properties.Extra as List+
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.String

import Data.Vec.Relation.Unary.All as Vec∀

open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct
open import MJ.LexicalScope c
open import MJ.Syntax Ct

data Body (I : Ctx) : Ty c → Set where
  body : ∀ {r}{O : Ctx} → Stmts I r O → Expr O r → Body I r

{-
A helper to generate the shape of the context for method bodies
-}
methodctx : Cid c → List (Ty c) → Ctx
methodctx cid as = (ref cid ∷ as)

{-
A helper to generate the shape of the context for constructors
-}
constrctx : Cid c → Ctx
constrctx cid = let cl = Σ cid in (ref cid ∷ Class.constr cl)

-- A method is either just a body, or a body prefixed by a super call.
data Method (cid : Cid c)(m : String) : Sig c → Set where
  super_⟨_⟩then_ : ∀ {as b} →
                let
                  pid = Class.parent (Σ cid)
                  Γ   = methodctx cid as
                in
                  -- must have a super to call, with the same signature
                  AccMember pid METHOD m (as , b) →
                  -- super call arguments
                  All (Expr Γ) as →
                  -- body
                  Body (Γ +local b) b → Method cid m (as , b)
  body        : ∀ {as b} → Body (methodctx cid as) b → Method cid m (as , b)

-- Constructors are similar
data Constructor (cid : Cid c) : Set where
  super_then_ : let
                  pid = Class.parent (Σ cid)
                  pclass = Σ pid
                  Γ   = constrctx cid
                in
                  -- super call arguments
                  All (Expr Γ) (Class.constr pclass) →
                  -- body
                  Body Γ void →
                  Constructor cid
  body        : Body (constrctx cid) void → Constructor cid

{-
A class implementation consists of a constructor and a body for every
METHOD declaration.
-}
record Implementation (cid : Cid c) : Set where
  constructor implementation
  open Class (Σ cid) public
  field
    construct : Constructor cid
    mbodies   : All (λ{ (name , sig) → Method cid name sig }) (decls METHOD)

-- Code is a lookup table for class implementations for every class identifier
Code = ∀ cid → Implementation cid

-- Mirroring `IsMember METHOD` we define the notion of an inherited method body.
InheritedMethod : ∀ (cid : Cid c)(m : String) → Sig c → Set
InheritedMethod cid m s = ∃ λ pid → Σ ⊢ cid <: pid × Method pid m s


text:
-- Andreas, Jesper, 2017-05-13, issue #2578 reported by nad
-- Jesper, 2017-07-06, absurd clauses are no longer highlighted as catchall,
-- so the test case had to be changed to reproduce the intended behaviour.

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

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

Maybe : Set → Set
Maybe A = ⊤ ⊎ A

pattern nothing = inj₁ tt
pattern just x  = inj₂ x

Bool : Set
Bool = ⊤ ⊎ ⊤

pattern true  = inj₁ tt
pattern false = inj₂ tt

x : Maybe ⊥
x = nothing

_∋_ : ∀ {ℓ} → (A : Set ℓ) (a : A) → A
A ∋ a = a

A : Set₁
A with Bool ∋ false
A | true = Set
A | false with x | x
... | nothing | nothing = Set
... | just x | _ = {!!}
... | _ | just y = {!!}


text:
-- Check that errors from tactics are displayed properly.
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Equality
open import Common.Reflection

failTactic : Term → TC ⊤
failTactic hole =
  inferType hole >>= λ goal →
  typeError (strErr "Surprisingly the" ∷ nameErr (quote failTactic) ∷
             strErr "failed to prove" ∷ termErr goal ∷ [])

macro
  proveIt = failTactic

postulate
  ComplexityClass : Set
  P NP : ComplexityClass

thm : P ≡ NP → ⊥
thm = proveIt

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------

-- The definitions in this file are reexported by Data.Maybe.

module Data.Maybe.Core where

open import Level

data Maybe {a} (A : Set a) : Set a where
  just    : (x : A) → Maybe A
  nothing : Maybe A

{-# IMPORT Data.FFI #-}
{-# COMPILED_DATA Maybe Data.FFI.AgdaMaybe Just Nothing #-}


text:
module Type.Identity.Proofs where

import      Lvl
open import Structure.Function
open import Structure.Relator.Properties
open import Structure.Relator
open import Structure.Type.Identity
open import Type.Identity
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₚ : Lvl.Level
private variable T A B : Type{ℓ}
private variable P : T → Type{ℓ}
private variable _▫_ : A → B → Type{ℓ}

instance
  Id-reflexivity : Reflexivity(Id{T = T})
  Reflexivity.proof Id-reflexivity = intro

instance
  Id-identityEliminator : IdentityEliminator{ℓₚ = ℓₚ}(Id{T = T})
  IdentityEliminator.elim Id-identityEliminator = elim

instance
  Id-identityEliminationOfIntro : IdentityEliminationOfIntro{ℓₘ = ℓ}(Id{T = T})(Id)
  IdentityEliminationOfIntro.proof Id-identityEliminationOfIntro P p = intro

instance
  Id-identityType : IdentityType(Id)
  Id-identityType = intro

{-
open import Logic.Propositional
open import Logic.Propositional.Equiv
open import Relator.Equals.Proofs
open import Structure.Setoid

te : ⦃ equiv-A : Equiv{ℓₑ}(A)⦄ → ∀{f : A → Type{ℓ}} → Function ⦃ equiv-A ⦄ ⦃ [↔]-equiv ⦄ (f)

test : ⦃ equiv-A : Equiv{ℓₑ}(A)⦄ → ∀{P : A → Type{ℓ}} → UnaryRelator ⦃ equiv-A ⦄ (P)
UnaryRelator.substitution test eq p = [↔]-to-[→] (Function.congruence te eq) p
-}


text:
-- Abstract constructors
module Issue476c where

module M where
  data D : Set

  abstract
    data D where
      c : D

x : M.D
x = M.c

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda