text:
module with-equalities where

open import Agda.Builtin.List

open import Common.Bool
open import Common.Equality

module _ {A : Set} where

  filter : (A → Bool) → List A → List A
  filter p []       = []
  filter p (x ∷ xs) =
    if p x then x ∷ filter p xs else filter p xs

  filter-filter : ∀ p xs → filter p (filter p xs) ≡ filter p xs
  filter-filter p []       = refl
  filter-filter p (x ∷ xs) with p x in eq
  ... | false = filter-filter p xs -- easy
  ... | true -- second filter stuck on `p x`: rewrite by `eq`!
    rewrite eq = cong (x ∷_) (filter-filter p xs)

open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma

double : Nat → Set
double m = Σ Nat λ n → n + n ≡ m

-- 2*_ : Nat → Σ Nat double
-- 2*_ n with m ← n + n = m , n , {!!}
--  At this point we do not remember that m ≡ n + n and cannot
--  conclude the proof.

-- If only we could give a name to the proof that
-- `p ≡ e` after a `with p ← e` clause !

2*_ : Nat → Σ Nat double
2*_ n with m ← n + n in eq = m , n , eq

data ⊥ : Set where
⊥-elim : ⊥ → {A : Set} → A
⊥-elim ()

¬odd0 : ∀ n → 2 * n + 1 ≡ 0 → ⊥
¬odd0 zero    ()
¬odd0 (suc n) ()

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

module _ {A : Set} where

  oddhead : ∀ {n} → Vec A (2 * n + 1) → A
  oddhead {n} xs
    -- here we cannot split on `xs` because Agda does not know
    -- whether `2 * n + 1` can unify with `0` or not

    -- A possible solution: abstract over p and then match on xs.
--      with p ← (2 * n + 1) | xs
--  ... | x ∷ _ = x
--  ... | []    = {!!}

    -- The problem however is that Agda insists we should consider
    -- two cases: `xs = []` and `xs = x ∷ _`. And in the `[]` branch
    -- we only know that:
    -- p  : Nat
    -- n  : Nat
    -- xs : Vec A 0
    -- If only we had somehow recorded that `p ← (2 * n + 1)` happened!
    -- This is what the inspect construct allows us to do.

    with p ← (2 * n + 1) in eq | xs
  ... | x ∷ _ = x
  -- we can now use this equality proof to dismiss the impossible case.
  ... | []    = ⊥-elim (¬odd0 n eq)

  -- If you do not want to name the nat corresponding to `2 * n + 1`,
  -- you can use inspect together with an implicit with

  oddhead' : ∀ {n} → Vec A (2 * n + 1) → A
  oddhead' {n} xs with {2 * n + 1} in eq | xs
  ... | x ∷ _ = x
  ... | []    = ⊥-elim (¬odd0 n eq)


text:
module Algebra.LabelledGraph.Theorems where

open import Algebra.LabelledGraph
open import Algebra.LabelledGraph.Reasoning
open import Algebra.Dioid
open import Algebra.Graph using (Graph)
import Algebra.Graph as Graph
import Algebra.Graph.Reasoning as Graph
import Algebra.Graph.Theorems as Graph
import Algebra.Dioid.Bool as Bool
import Algebra.Dioid.Bool.Theorems as Bool

-- | Laws of labelled graphs

associativity : ∀ {A D eq} {d : Dioid D eq} {a b c : LabelledGraph d A} {r : D} -> (a [ r ]> b) [ r ]> c ≡ a [ r ]> (b [ r ]> c)
associativity {_} {_} {_} {_} {a} {b} {c} {r} = right-decomposition >> symmetry left-decomposition

absorption : ∀ {A D eq} {d : Dioid D eq} {a b : LabelledGraph d A} {r : D} -> a [ r ]> b ≡ a [ r ]> b + a + b
absorption {_} {_} {_} {d} {a} {b} {r} =
  begin
    (a [ r ]> b) ≡⟨ symmetry right-identity ⟩
    (a [ r ]> b) [ Dioid.zero d ]> ε ≡⟨ right-decomposition ⟩
    (a [ r ]> b) + (a + ε) + (b + ε) ≡⟨ L (R right-identity ) ⟩
    (a [ r ]> b) + a + (b + ε) ≡⟨ R right-identity ⟩
    (a [ r ]> b) + a + b
  ∎

idempotence : ∀ {A D eq} {d : Dioid D eq} {a : LabelledGraph d A} -> a ≡ a + a
idempotence {_} {_} {_} {_} {a} =
  begin
    a ≡⟨ symmetry right-identity ⟩
    a + ε ≡⟨ symmetry right-identity ⟩
    a + ε + ε ≡⟨ right-decomposition ⟩
    (a + ε) + (a + ε) + (ε + ε) ≡⟨ right-congruence left-identity ⟩
    (a + ε) + (a + ε) + ε ≡⟨ right-identity ⟩
    (a + ε) + (a + ε) ≡⟨ right-congruence right-identity ⟩
    (a + ε) + a ≡⟨ left-congruence right-identity ⟩
    a + a
  ∎

left-absorption : ∀ {A D eq} {d : Dioid D eq} {a b : LabelledGraph d A} {r : D} -> a [ r ]> b ≡ a [ r ]> b + a
left-absorption {_} {_} {_} {_} {a} {b} {r} =
  begin
    (a [ r ]> b)                 ≡⟨ absorption ⟩
    (a [ r ]> b) + a + b         ≡⟨ L (R idempotence) ⟩
    (a [ r ]> b) + (a + a) + b   ≡⟨ associativity ⟩
    (a [ r ]> b) + (a + a + b)   ≡⟨ R zero-commutativity ⟩
    (a [ r ]> b) + (b + (a + a)) ≡⟨ R (symmetry associativity) ⟩
    (a [ r ]> b) + ((b + a) + a) ≡⟨ R (L zero-commutativity) ⟩
    (a [ r ]> b) + ((a + b) + a) ≡⟨ symmetry associativity ⟩
    (a [ r ]> b) + (a + b) + a   ≡⟨ L (symmetry associativity) ⟩
    (a [ r ]> b) + a + b + a     ≡⟨ L (symmetry absorption) ⟩
    (a [ r ]> b) + a
  ∎

right-absorption : ∀ {A D eq} {d : Dioid D eq} {a b : LabelledGraph d A} {r : D} -> a [ r ]> b ≡ a [ r ]> b + b
right-absorption {_} {_} {_} {_} {a} {b} {r} =
  begin
    (a [ r ]> b)               ≡⟨ absorption ⟩
    (a [ r ]> b) + a + b       ≡⟨ R idempotence ⟩
    (a [ r ]> b) + a + (b + b) ≡⟨ symmetry associativity ⟩
    (a [ r ]> b) + a + b + b   ≡⟨ L (symmetry absorption) ⟩
    (a [ r ]> b) + b
  ∎

right-distributivity : ∀ {A D eq} {d : Dioid D eq} {a b c : LabelledGraph d A} {r : D} -> (a + b) [ r ]> c ≡ a [ r ]> c + b [ r ]> c
right-distributivity {_} {_} {_} {_} {a} {b} {c} {r} =
  begin
    (a + b) [ r ]> c                       ≡⟨ right-decomposition ⟩
    a + b + (a [ r ]> c) + (b [ r ]> c)   ≡⟨ L zero-commutativity ⟩
    (a [ r ]> c) + (a + b) + (b [ r ]> c) ≡⟨ L (symmetry associativity) ⟩
    ((a [ r ]> c) + a) + b + (b [ r ]> c) ≡⟨ L (L (symmetry left-absorption)) ⟩
    (a [ r ]> c) + b + (b [ r ]> c)       ≡⟨ associativity ⟩
    (a [ r ]> c) + (b + (b [ r ]> c))     ≡⟨ R zero-commutativity ⟩
    (a [ r ]> c) + ((b [ r ]> c) + b)     ≡⟨ R (symmetry left-absorption) ⟩
    (a [ r ]> c) + (b [ r ]> c)
  ∎

left-distributivity : ∀ {A D eq} {d : Dioid D eq} {a b c : LabelledGraph d A} {r : D} -> a [ r ]> (b + c) ≡ a [ r ]> b + a [ r ]> c
left-distributivity {_} {_} {_} {_} {a} {b} {c} {r} =
  begin
    a [ r ]> (b + c)                   ≡⟨ left-decomposition ⟩
    a [ r ]> b + a [ r ]> c + (b + c) ≡⟨ symmetry associativity ⟩
    a [ r ]> b + a [ r ]> c + b + c   ≡⟨ L associativity ⟩
    a [ r ]> b + (a [ r ]> c + b) + c ≡⟨ L (R zero-commutativity) ⟩
    a [ r ]> b + (b + a [ r ]> c) + c ≡⟨ L (symmetry associativity) ⟩
    a [ r ]> b + b + a [ r ]> c + c   ≡⟨ L (L (symmetry right-absorption)) ⟩
    a [ r ]> b + a [ r ]> c + c       ≡⟨ associativity ⟩
    a [ r ]> b + (a [ r ]> c + c)     ≡⟨ R (symmetry right-absorption) ⟩
    a [ r ]> b + a [ r ]> c
  ∎

-- | Conversion functions
-- These allow for a conversion between LabelledGraphs labelled by Bools and ordinary Graphs.
-- As `graph-laws` and `labelled-graph-laws` demonstrates, these preserve their respective laws.

to-graph : ∀ {A} -> LabelledGraph Bool.bool-dioid A -> Graph A
to-graph ε = Graph.ε
to-graph (v x) = Graph.v x
to-graph (x [ Bool.false ]> y) = to-graph x Graph.+ to-graph y
to-graph (x [ Bool.true  ]> y) = to-graph x Graph.* to-graph y

labelled-graph-laws : ∀ {A} {x y : LabelledGraph Bool.bool-dioid A} -> x ≡ y -> (to-graph x) Graph.≡ (to-graph y)
labelled-graph-laws reflexivity = Graph.reflexivity
labelled-graph-laws (symmetry eq) = Graph.symmetry (labelled-graph-laws eq)
labelled-graph-laws (transitivity eq eq₁) = Graph.transitivity (labelled-graph-laws eq)
                                              (labelled-graph-laws eq₁)
labelled-graph-laws (left-congruence {r = r} eq) with r
... | Bool.true = Graph.*left-congruence (labelled-graph-laws eq)
... | Bool.false = Graph.+left-congruence (labelled-graph-laws eq)
labelled-graph-laws (right-congruence {r = r} eq) with r
... | Bool.true = Graph.*right-congruence (labelled-graph-laws eq)
... | Bool.false = Graph.+right-congruence (labelled-graph-laws eq)
labelled-graph-laws (dioid-congruence eq) = dioid-recur eq
  where
    dioid-recur : ∀ {A} {x y : LabelledGraph Bool.bool-dioid A} {r s : Bool.Bool}
               -> r Bool.≡ s -> (to-graph (x [ r ]> y)) Graph.≡ (to-graph (x [ s ]> y))
    dioid-recur Bool.reflexivity = Graph.reflexivity
    dioid-recur (Bool.symmetry eq) = Graph.symmetry (dioid-recur eq)
    dioid-recur (Bool.transitivity eq eq₁) = Graph.transitivity (dioid-recur eq) (dioid-recur eq₁)
labelled-graph-laws zero-commutativity = Graph.+commutativity
labelled-graph-laws (left-identity {r = r}) with r
... | Bool.true = Graph.*left-identity
... | Bool.false = Graph.+commutativity Graph.>> Graph.+identity
labelled-graph-laws (right-identity {r = r}) with r
... | Bool.true = Graph.*right-identity
... | Bool.false = Graph.+identity
labelled-graph-laws (left-decomposition {r = r} {s}) with r | s
... | Bool.true  | Bool.true  = Graph.*associativity Graph.>> Graph.decomposition
... | Bool.true  | Bool.false = Graph.*+ltriple
... | Bool.false | Bool.true  = Graph.+*ltriple
... | Bool.false | Bool.false = Graph.++ltriple
labelled-graph-laws (right-decomposition {r = r} {s}) with r | s
... | Bool.true  | Bool.true  = Graph.decomposition
... | Bool.true  | Bool.false = Graph.*+rtriple
... | Bool.false | Bool.true  = Graph.+*rtriple
... | Bool.false | Bool.false = Graph.++rtriple
labelled-graph-laws (label-addition {r = r} {s}) with r | s
... | Bool.true  | Bool.true  = Graph.+idempotence
... | Bool.true  | Bool.false = Graph.+associativity Graph.>> Graph.absorption
... | Bool.false | Bool.true  = (Graph.+commutativity Graph.>> Graph.+associativity) Graph.>> Graph.absorption
... | Bool.false | Bool.false = Graph.+idempotence

from-graph : ∀ {A D eq} {d : Dioid D eq} -> Graph A -> LabelledGraph d A
from-graph Graph.ε = ε
from-graph (Graph.v x) = v x
from-graph {_} {_} {_} {d} (x Graph.+ y) = from-graph x [ Dioid.zero d ]> from-graph y
from-graph {_} {_} {_} {d} (x Graph.* y) = from-graph x [ Dioid.one  d ]> from-graph y

graph-laws : ∀ {A D eq} {d : Dioid D eq} {x y : Graph A} -> x Graph.≡ y -> _≡_ {A} {D} {eq} {d} (from-graph x) (from-graph y)
graph-laws {x = x} {.x} Graph.reflexivity = reflexivity
graph-laws {x = x} {y} (Graph.symmetry eq) = symmetry (graph-laws eq)
graph-laws {x = x} {y} (Graph.transitivity eq eq₁) = transitivity (graph-laws eq) (graph-laws eq₁)
graph-laws {x = .(_ Graph.+ _)} {.(_ Graph.+ _)} (Graph.+left-congruence eq)  = left-congruence (graph-laws eq)
graph-laws {x = .(_ Graph.* _)} {.(_ Graph.* _)} (Graph.*left-congruence eq)  = left-congruence (graph-laws eq)
graph-laws {x = .(_ Graph.* _)} {.(_ Graph.* _)} (Graph.*right-congruence eq) = right-congruence (graph-laws eq)
graph-laws {x = .(_ Graph.+ _)} {.(_ Graph.+ _)} Graph.+commutativity = zero-commutativity
graph-laws {x = .(_ Graph.+ (_ Graph.+ _))} {.(_ Graph.+ _ Graph.+ _)} Graph.+associativity = symmetry associativity
graph-laws {x = .(Graph.ε Graph.* y)} {y} Graph.*left-identity = left-identity
graph-laws {x = .(y Graph.* Graph.ε)} {y} Graph.*right-identity = right-identity
graph-laws {x = .(_ Graph.* (_ Graph.* _))} {.(_ Graph.* _ Graph.* _)} Graph.*associativity = symmetry associativity
graph-laws {x = .(_ Graph.* (_ Graph.+ _))} {.(_ Graph.* _ Graph.+ _ Graph.* _)} Graph.left-distributivity = left-distributivity
graph-laws {x = .((_ Graph.+ _) Graph.* _)} {.(_ Graph.* _ Graph.+ _ Graph.* _)} Graph.right-distributivity = right-distributivity
graph-laws {x = .(_ Graph.* _ Graph.* _)} {.(_ Graph.* _ Graph.+ _ Graph.* _ Graph.+ _ Graph.* _)} Graph.decomposition = right-decomposition

to-from-identity : ∀ {A} {x : Graph A} -> (to-graph (from-graph x)) Graph.≡ x
to-from-identity {x = Graph.ε} = Graph.reflexivity
to-from-identity {x = Graph.v x} = Graph.reflexivity
to-from-identity {x = x₁ Graph.+ x₂} = Graph.symmetry (Graph.+left-congruence  (Graph.symmetry (to-from-identity {x = x₁})))
                              Graph.>> Graph.symmetry (Graph.+right-congruence (Graph.symmetry (to-from-identity {x = x₂})))
to-from-identity {x = x₁ Graph.* x₂} = Graph.symmetry (Graph.*left-congruence  (Graph.symmetry (to-from-identity {x = x₁})))
                              Graph.>> Graph.symmetry (Graph.*right-congruence (Graph.symmetry (to-from-identity {x = x₂})))

from-to-identity : ∀ {A} {x : LabelledGraph Bool.bool-dioid A} -> (from-graph (to-graph x)) ≡ x
from-to-identity {x = ε} = reflexivity
from-to-identity {x = v x} = reflexivity
from-to-identity {x = x₁ [ d ]> x₂} with d
... | Bool.true  = symmetry (left-congruence  (symmetry (from-to-identity {x = x₁})))
                >> symmetry (right-congruence (symmetry (from-to-identity {x = x₂})))
... | Bool.false = symmetry (left-congruence  (symmetry (from-to-identity {x = x₁})))
                >> symmetry (right-congruence (symmetry (from-to-identity {x = x₂})))

ext: agda

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs


text:
------------------------------------------------------------------------------
-- Examples of translation of logical schemata
------------------------------------------------------------------------------

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

module FOL.SchemataATP where

open import FOL.Base

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

module NonSchemas where

  postulate
    A B C    : Set
    A¹       : D → Set
    A² B²    : D → D → Set
    A³ B³ C³ : D → D → D → Set

  postulate id : A → A
  {-# ATP prove id #-}

  postulate id¹ : ∀ {x} → A¹ x → A¹ x
  {-# ATP prove id¹ #-}

  postulate id² : ∀ {x y} → A² x y → A² x y
  {-# ATP prove id² #-}

  postulate ∨-comm : A ∨ B → B ∨ A
  {-# ATP prove ∨-comm #-}

  postulate ∨-comm² : ∀ {x y} → A² x y ∨ B² x y → B² x y ∨ A² x y
  {-# ATP prove ∨-comm² #-}

  postulate ∧∨-dist : A ∧ (B ∨ C) ↔ A ∧ B ∨ A ∧ C
  {-# ATP prove ∧∨-dist #-}

  postulate
    ∧∨-dist³ : ∀ {x y z} →
               (A³ x y z ∧ (B³ x y z ∨ C³ x y z)) ↔
               (A³ x y z ∧ B³ x y z ∨ A³ x y z ∧ C³ x y z)
  {-# ATP prove ∧∨-dist³ #-}

module Schemas where

  postulate id : {A : Set} → A → A
  {-# ATP prove id #-}

  postulate id¹ : {A¹ : D → Set} → ∀ {x} → A¹ x → A¹ x
  {-# ATP prove id¹ #-}

  postulate id² : {A² : D → D → Set} → ∀ {x y} → A² x y → A² x y
  {-# ATP prove id² #-}

  postulate ∨-comm : {A B : Set} → A ∨ B → A ∨ B
  {-# ATP prove ∨-comm #-}

  postulate ∨-comm² : {A² B² : D → D → Set} → ∀ {x y} →
                      A² x y ∨ B² x y → B² x y ∨ A² x y
  {-# ATP prove ∨-comm² #-}

  postulate ∧∨-dist : {A B C : Set} → A ∧ (B ∨ C) ↔ A ∧ B ∨ A ∧ C
  {-# ATP prove ∧∨-dist #-}

  postulate ∧∨-dist³ : {A³ B³ C³ : D → D → D → Set} → ∀ {x y z} →
                       (A³ x y z ∧ (B³ x y z ∨ C³ x y z)) ↔
                       (A³ x y z ∧ B³ x y z ∨ A³ x y z ∧ C³ x y z)
  {-# ATP prove ∧∨-dist³ #-}

module SchemaInstances where

  -- A schema
  -- Current translation: ∀ p q x. app(p,x) → app(q,x).
  postulate schema : (A B : D → Set) → ∀ {x} → A x → B x

  -- Using the current translation, the ATPs can prove an instance of
  -- the schema.
  postulate
    d         : D
    A B       : D → Set
    instanceC : A d → B d
  {-# ATP prove instanceC schema #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

{-# OPTIONS --guardedness #-}

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

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

  private
    variable
      U : Set 𝓁

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

  {- Coinductive interpretation -}

  record CoInd⟦_⟧ {𝓁c 𝓁p 𝓁n : Level} (is : IS {𝓁c} {𝓁p} {𝓁n} U) (u : U) : Set (𝓁 ⊔ 𝓁c ⊔ 𝓁p ⊔ 𝓁n) where
    coinductive
    constructor cofold_
    field
      unfold : ISF[ is ] CoInd⟦ is ⟧ u

  {- Coinduction Principle -}

  coind[_] : ∀{𝓁c 𝓁p 𝓁n 𝓁'}
      → (is : IS {𝓁c} {𝓁p} {𝓁n} U)
      → (S : U → Set 𝓁')
      → (S ⊆ ISF[ is ] S)   -- S is consistent
      → S ⊆ CoInd⟦ is ⟧
  CoInd⟦_⟧.unfold (coind[ is ] S cn Su) with cn Su
  ... | rn , c , refl , pr = rn , c , refl , λ i → coind[ is ] S cn (pr i)

  {- Apply Rule -}

  apply-coind : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → (rn : is .Names) → RClosed (is .rules rn) CoInd⟦ is ⟧
  apply-coind {is = is} rn = prefix⇒closed (is .rules rn) {P = CoInd⟦ _ ⟧} λ{(c , refl , pr) → cofold (rn , c , refl , pr)}

  {- Postfix - Prefix -}

  coind-postfix : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → CoInd⟦ is ⟧ ⊆ ISF[ is ] CoInd⟦ is ⟧
  coind-postfix x = x .CoInd⟦_⟧.unfold

  coind-prefix : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → ISF[ is ] CoInd⟦ is ⟧ ⊆ CoInd⟦ is ⟧
  coind-prefix x = cofold x

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
{-# OPTIONS --without-K #-}
import Level as L
open L using (Lift; lift)
open import Type hiding (★)
open import Function.NP
open import Algebra
open import Algebra.FunctionProperties.NP
open import Data.Nat.NP hiding (_^_)
open import Data.Nat.Properties
open import Data.One hiding (_≤_)
open import Data.Sum
open import Data.Maybe.NP
open import Data.Product
open import Data.Bits
open import Data.Bool.NP as Bool
open import Data.Fin using (Fin)
open import Function.NP
open import Function.Equality using (_⟨$⟩_)
import Function.Inverse.NP as FI
open FI using (_↔_; inverses; module Inverse) renaming (_$₁_ to to; _$₂_ to from)
import Function.Related as FR
open import Function.Related.TypeIsomorphisms.NP
open import Relation.Binary.NP
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_; _≗_)
open import Search.Type
open import Search.Searchable renaming (Searchable to Searchable)
open import Search.Searchable.Product
open import Search.Searchable.Sum
open import Search.Searchable.Maybe
--open import Search.Searchable.Fin
open import Search.Derived

module sum where

_≈Sum_ : ∀ {A} → (sum₀ sum₁ : Sum A) → ★ _
sum₀ ≈Sum sum₁ = ∀ f → sum₀ f ≡ sum₁ f

_≈Search_ : ∀ {A} → (s₀ s₁ : Search _ A) → ★₁
s₀ ≈Search s₁ = ∀ {B} (op : Op₂ B) f → s₀ op f ≡ s₁ op f

_⊎'_ : ★₀ → ★₀ → ★₀
A ⊎' B = Σ Bool (cond A B)

_μ⊎'_ : ∀ {A B} → Searchable A → Searchable B → Searchable (A ⊎' B)
μA μ⊎' μB = μΣ μBit (λ { {true} → μA ; {false} → μB })

open import Data.Fin using (Fin; zero; suc)
open import Data.Vec.NP as Vec using (Vec; tabulate; _++_) renaming (map to vmap; sum to vsum; foldr to vfoldr; foldr₁ to vfoldr₁)

vmsum : ∀ {c ℓ} (m : Monoid c ℓ) {n} →
          let open Mon m in
          Vec C n → C
vmsum m = vfoldr _ _∙_ ε
  where open Mon m

vsgsum : ∀ {c ℓ} (sg : Semigroup c ℓ) {n} →
           let open Sgrp sg in
           Vec C (suc n) → C
vsgsum sg = vfoldr₁ _∙_
  where open Sgrp sg

-- let's recall that: tabulate f ≗ vmap f (allFin n)

-- searchMonFin : ∀ n → SearchMon (Fin n)
-- searchMonFin n m f = vmsum m (tabulate f)

searchFinSuc : ∀ {m} n → Search m (Fin (suc n))
searchFinSuc n _∙_ f = vfoldr₁ _∙_ (tabulate f)

searchVec : ∀ {m A} n → Search m A → Search m (Vec A n)
searchVec zero    searchᴬ op f = f []
searchVec (suc n) searchᴬ op f = searchᴬ op (λ x → searchVec n searchᴬ op (f ∘ _∷_ x))

searchVec-spec : ∀ {A} (μA : Searchable A) n → searchVec n (search μA) ≈Search search (μVec μA n)
searchVec-spec μA zero    op f = ≡.refl
searchVec-spec μA (suc n) op f = search-ext μA op (λ x → searchVec-spec μA n op (f ∘ _∷_ x))

searchVec-++ : ∀ {A} n {m} (μA : Searchable A) sg
               → let open Sgrp sg in
                 (f : Vec A (n + m) → C)
               → search (μVec μA (n + m)) _∙_ f
               ≈ search (μVec μA n) _∙_ (λ xs →
                   search (μVec μA m) _∙_ (λ ys →
                     f (xs ++ ys)))
searchVec-++ zero    μA sg f = Sgrp.refl sg
searchVec-++ (suc n) μA sg f = search-sg-ext μA sg (λ x →
                                 searchVec-++ n μA sg (f ∘ _∷_ x))

sumVec-swap : ∀ {A} n {m} (μA : Searchable A)(f : Vec A (n + m) → ℕ)
            → sum (μVec μA n) (λ xs → sum (μVec μA m) (λ ys → f (xs ++ ys)))
            ≡ sum (μVec μA m) (λ ys → sum (μVec μA n) (λ xs → f (xs ++ ys)))
sumVec-swap n {m} μA f = sum-swap (μVec μA n) (μVec μA m) (λ xs ys → f (xs ++ ys))

simple : ∀ {A : Set}{P : A → A → Set} → (∀ x → P x x) → {x y : A} → x ≡ y → P x y
simple r ≡.refl = r _
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import Coinduction hiding (unfold) renaming (♯_ to Thunk; ♭ to Force)

module Brainfuck where

---------- A very basic Prelude ----------

record Pair (a b : Set) : Set where
  constructor _,_
  field
    fst : a
    snd : b

data Maybe (a : Set) : Set where
  Nothing : Maybe a
  Just : (x : a) -> Maybe a

return : {a : Set} -> a -> Maybe a
return x = Just x

data Nat : Set where
  Zero : Nat
  Succ : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

data Bool : Set where
  True : Bool
  False : Bool

if_then_else : {a : Set} -> Bool -> a -> a -> a
if True then t else f = t
if False then t else f = f

data List (a : Set) : Set where
  Nil : List a
  Cons : a -> List a -> List a

---------- Bits and Bytes ----------

data Bit : Set where
  O : Bit
  I : Bit

data Vec (a : Set) : Nat -> Set where
  Nil : Vec a 0
  Cons : {n : Nat} -> (x : a) -> (xs : Vec a n) -> Vec a (Succ n)

Byte : Set
Byte = Vec Bit 8

incr : {n : Nat} -> Vec Bit n -> Vec Bit n
incr Nil = Nil
incr (Cons O xs) = Cons I xs
incr (Cons I xs) = Cons O (incr xs)

decr : {n : Nat} -> Vec Bit n -> Vec Bit n
decr Nil = Nil
decr (Cons O xs) = Cons I (decr xs)
decr (Cons I xs) = Cons O xs

isZero : {n : Nat} -> Vec Bit n -> Bool
isZero Nil = True
isZero (Cons O xs) = isZero xs
isZero (Cons I xs) = False

zero : {n : Nat} -> Vec Bit n
zero {Zero} = Nil
zero {Succ k} = Cons O zero

---------- The state of the machine ----------

data Stream (a : Set) : Set where
  Cons : a -> ∞ (Stream a) -> Stream a

zeros : Stream Byte
zeros = Cons zero (Thunk zeros)

record State : Set where
  constructor _,_,_,_,_
  field
    left : Stream Byte
    current : Byte
    right : Stream Byte
    stdin : Stream Byte
    stdout : List Byte

init : Stream Byte -> State
init stdin = zeros , zero , zeros , stdin , Nil

stepLeft : State -> State
stepLeft (Cons left lefts , current , right , stdin , stdout) =
  (Force lefts) , left , (Cons current (Thunk right)) , stdin , stdout

stepRight : State -> State
stepRight (left , current , Cons right rights , stdin , stdout) =
  Cons current (Thunk left) , right , Force rights , stdin , stdout

output : State -> State
output (left , current , right , stdin , stdout) =
  left , current , right , stdin , (Cons current stdout)

input : State -> State
input (left , current , right , Cons b stdin , stdout) =
  left , b , right , Force stdin , stdout

increment : State -> State
increment (left , current , right , stdin , stdout) =
  left , (incr current) , right , stdin , stdout

decrement : State -> State
decrement (left , current , right , stdin , stdout) =
  left , (decr current) , right , stdin , stdout

---------- The Brainfuck language ----------

data Command : Set where
  >_ : (c : Command) -> Command
  <_ : (c : Command) -> Command
  +_ : (c : Command) -> Command
  -_ : (c : Command) -> Command
  ·_ : (c : Command) -> Command
  ,_ : (c : Command) -> Command
  [_]_ : (body : Command) -> (c : Command) -> Command
  □ : Command

infix 25 [_]_

-- sequence c1 c2 computes a new command equivalent to c1 followed by c2
sequence : Command -> Command -> Command
sequence (> c) c' = > (sequence c c')
sequence (< c) c' = < (sequence c c')
sequence (+ c) c' = + (sequence c c')
sequence (- c) c' = - (sequence c c')
sequence (· c) c' = · (sequence c c')
sequence (, c) c' = , (sequence c c')
sequence ([ body ] c) c' = [ body ] (sequence c c')
sequence □ c' = c'

step : Pair Command State -> Maybe (Pair Command State)
step ((> cmd) , s) = return (cmd , stepRight s)
step ((< cmd) , s) = return (cmd , stepLeft s)
step ((+ cmd) , s) = return (cmd , increment s)
step ((- cmd) , s) = return (cmd , decrement s)
step ((· cmd) , s) = return (cmd , output s)
step ((, cmd) , s) = return (cmd , input s)
step ([ body ] cmd , s) = if isZero (State.current s)
                          then return (cmd , s)
                          else (return ((sequence body ([ body ] cmd)) , s))
step (□ , s) = Nothing

data Trace : Set where
  Step : State -> ∞ Trace -> Trace
  Stop : State -> Trace

run : Pair Command State -> Trace
run (cmd , s) with step (cmd , s)
run (cmd , s) | Nothing = Stop s
run (cmd , s) | Just x = Step s (Thunk (run x))

interpret : Command -> (stdin : Stream Byte) -> Trace
interpret c stdin = run (c , init stdin)

max_stars_repo_name: wouter-swierstra/Brainfuck

max_issues_repo_name: wouter-swierstra/Brainfuck

max_forks_repo_name: wouter-swierstra/Brainfuck


text:
------------------------------------------------------------------------
-- Various equality checkers (some complete, all sound)
------------------------------------------------------------------------

import Axiom.Extensionality.Propositional as E
import Level
open import Data.Universe

-- The code makes use of the assumption that propositional equality of
-- functions is extensional.

module README.DependentlyTyped.Equality-checker
  (Uni₀ : Universe Level.zero Level.zero)
  (ext : E.Extensionality Level.zero Level.zero)
  where

open import Category.Monad
open import Data.Maybe
import Data.Maybe.Categorical as Maybe
open import Data.Product
open import Function hiding (_∋_) renaming (const to k)
import README.DependentlyTyped.NBE as NBE; open NBE Uni₀ ext
import README.DependentlyTyped.NormalForm as NF; open NF Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary as Dec using (Dec; yes)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product

open P.≡-Reasoning
open RawMonadZero (Maybe.monadZero {f = Level.zero})

-- Decides if two "atomic type proofs" are equal.

infix 4 _≟-atomic-type_

_≟-atomic-type_ :
  ∀ {Γ σ} (σ′₁ σ′₂ : Γ ⊢ σ atomic-type) → Dec (σ′₁ ≡ σ′₂)
⋆  ≟-atomic-type ⋆  = yes P.refl
el ≟-atomic-type el = yes P.refl

mutual

  private

    -- A helper lemma.

    helper-lemma :
      ∀ {Γ₁ sp₁₁ sp₂₁ σ₁}
        (t₁₁ : Γ₁ ⊢ π sp₁₁ sp₂₁ , σ₁ ⟨ ne ⟩) (t₂₁ : Γ₁ ⊢ fst σ₁ ⟨ no ⟩)
        {Γ₂ sp₁₂ sp₂₂ σ₂}
        (t₁₂ : Γ₂ ⊢ π sp₁₂ sp₂₂ , σ₂ ⟨ ne ⟩) (t₂₂ : Γ₂ ⊢ fst σ₂ ⟨ no ⟩) →
      t₁₁ · t₂₁ ≅-⊢n t₁₂ · t₂₂ → t₁₁ ≅-⊢n t₁₂ × t₂₁ ≅-⊢n t₂₂
    helper-lemma _ _ ._ ._ P.refl = P.refl , P.refl

  -- Decides if two neutral terms are identical. Note that the terms
  -- must have the same context, but they do not need to have the same
  -- type.

  infix 4 _≟-⊢ne_

  _≟-⊢ne_ : ∀ {Γ σ₁} (t₁ : Γ ⊢ σ₁ ⟨ ne ⟩)
                {σ₂} (t₂ : Γ ⊢ σ₂ ⟨ ne ⟩) →
            Dec (t₁ ≅-⊢n t₂)
  var x₁ ≟-⊢ne var x₂ = Dec.map′ var-n-cong helper (x₁ ≟-∋ x₂)
    where
    helper : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
               {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
             var x₁ ≅-⊢n var x₂ → x₁ ≅-∋ x₂
    helper P.refl = P.refl

  t₁₁ · t₂₁ ≟-⊢ne t₁₂ · t₂₂ with t₁₁ ≟-⊢ne t₁₂
  ... | Dec.no neq = Dec.no (neq ∘ proj₁ ∘ helper-lemma _ t₂₁ _ t₂₂)
  ... | yes eq     = Dec.map′
    (·n-cong eq)
    (proj₂ ∘ helper-lemma t₁₁ _ t₁₂ _)
    (t₂₁ ≟-⊢no t₂₂ [ fst-cong $ indexed-type-cong $ helper eq ])
    where
    helper : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁ ⟨ ne ⟩}
               {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂ ⟨ ne ⟩} →
             t₁ ≅-⊢n t₂ → σ₁ ≅-Type σ₂
    helper P.refl = P.refl

  var _ ≟-⊢ne _ · _ = Dec.no λ ()
  _ · _ ≟-⊢ne var _ = Dec.no λ ()

  -- Decides if two normal forms are identical. Note that the terms
  -- must have the same type.

  infix 4 _≟-⊢no_[_]

  _≟-⊢no_[_] : ∀ {Γ₁ σ₁} (t₁ : Γ₁ ⊢ σ₁ ⟨ no ⟩)
                 {Γ₂ σ₂} (t₂ : Γ₂ ⊢ σ₂ ⟨ no ⟩) →
              σ₁ ≅-Type σ₂ → Dec (t₁ ≅-⊢n t₂)
  ne σ′₁ t₁ ≟-⊢no ne σ′₂ t₂ [ P.refl ] = ne≟ne σ′₁ σ′₂ (t₁ ≟-⊢ne t₂)
    where
    ne≟ne : ∀ {Γ σ} {t₁ t₂ : Γ ⊢ σ ⟨ ne ⟩}
            (σ′₁ : Γ ⊢ σ atomic-type) (σ′₂ : Γ ⊢ σ atomic-type) →
            Dec (t₁ ≅-⊢n t₂) → Dec (ne σ′₁ t₁ ≅-⊢n ne σ′₂ t₂)
    ne≟ne ⋆  ⋆  (yes P.refl) = yes P.refl
    ne≟ne el el (yes P.refl) = yes P.refl
    ne≟ne _  _  (Dec.no neq) = Dec.no (neq ∘ helper)
      where
      helper :
        ∀ {Γ₁ σ₁ σ′₁} {t₁ : Γ₁ ⊢ σ₁ ⟨ ne ⟩}
          {Γ₂ σ₂ σ′₂} {t₂ : Γ₂ ⊢ σ₂ ⟨ ne ⟩} →
        ne σ′₁ t₁ ≅-⊢n ne σ′₂ t₂ → t₁ ≅-⊢n t₂
      helper P.refl = P.refl

  ƛ t₁ ≟-⊢no ƛ t₂ [ eq ] =
    Dec.map′ ƛn-cong helper
             (t₁ ≟-⊢no t₂ [ snd-cong $ indexed-type-cong eq ])
    where
    helper :
      ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ▻ σ₁ ⊢ τ₁ ⟨ no ⟩}
        {Γ₂ σ₂ τ₂} {t₂ : Γ₂ ▻ σ₂ ⊢ τ₂ ⟨ no ⟩} →
      ƛ t₁ ≅-⊢n ƛ t₂ → t₁ ≅-⊢n t₂
    helper P.refl = P.refl

  ne _ _ ≟-⊢no ƛ _    [ _ ] = Dec.no λ ()
  ƛ _    ≟-⊢no ne _ _ [ _ ] = Dec.no λ ()

-- Tries to prove that two terms have the same semantics. The terms
-- must have the same type.

⟦_⟧≟⟦_⟧ : ∀ {Γ σ} (t₁ t₂ : Γ ⊢ σ) →
          Maybe (⟦ t₁ ⟧ ≅-Value ⟦ t₂ ⟧)
⟦ t₁ ⟧≟⟦ t₂ ⟧ with normalise t₁ ≟-⊢no normalise t₂ [ P.refl ]
... | Dec.no _ = ∅
... | yes eq   = return (begin
  [ ⟦ t₁ ⟧            ]  ≡⟨ normalise-lemma t₁ ⟩
  [ ⟦ normalise t₁ ⟧n ]  ≡⟨ ⟦⟧n-cong eq ⟩
  [ ⟦ normalise t₂ ⟧n ]  ≡⟨ P.sym $ normalise-lemma t₂ ⟩
  [ ⟦ t₂ ⟧            ]  ∎)

-- Tries to prove that two semantic types are equal, given
-- corresponding syntactic types. The types must have the same
-- context.

infix 4 _≟-Type_

_≟-Type_ : ∀ {Γ σ₁} (σ₁′ : Γ ⊢ σ₁ type)
               {σ₂} (σ₂′ : Γ ⊢ σ₂ type) →
           Maybe (σ₁ ≅-Type σ₂)
⋆ ≟-Type ⋆ = return P.refl

el t₁ ≟-Type el t₂ = helper <$> ⟦ t₁ ⟧≟⟦ t₂ ⟧
  where
  helper : ∀ {Γ₁} {v₁ : Value Γ₁ (⋆ , _)}
             {Γ₂} {v₂ : Value Γ₂ (⋆ , _)} →
           v₁ ≅-Value v₂ → (el , v₁) ≅-Type (el , v₂)
  helper P.refl = P.refl
π σ′₁ τ′₁ ≟-Type π σ′₂ τ′₂ = helper τ′₁ τ′₂ =<< σ′₁ ≟-Type σ′₂
  where
  helper :
    ∀ {Γ₁ σ₁ τ₁} (τ′₁ : Γ₁ ▻ σ₁ ⊢ τ₁ type)
      {Γ₂ σ₂ τ₂} (τ′₂ : Γ₂ ▻ σ₂ ⊢ τ₂ type) →
    σ₁ ≅-Type σ₂ → Maybe (Type-π σ₁ τ₁ ≅-Type Type-π σ₂ τ₂)
  helper τ′₁ τ′₂ P.refl = Type-π-cong <$> (τ′₁ ≟-Type τ′₂)

_ ≟-Type _ = ∅

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


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

module SetQuotientTest where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.NatPlusOne using (HasFromNat; 1+_; ℕ₊₁; ℕ₊₁→ℕ)
open import Cubical.HITs.Ints.QuoInt using (HasFromNat; signed) renaming
  ( abs to absᶻ
  ; pos to pos
  ; neg to neg
  )
open import Cubical.HITs.Ints.QuoInt hiding (_+_; -_; +-assoc; +-comm)
open import Cubical.HITs.Rationals.QuoQ using
    ( ℚ
    ; onCommonDenom
    ; onCommonDenomSym
    ; eq/
    ; _//_
    ; _∼_
    ; isSetℚ
    )
    renaming
    ( [_] to [_]ᶠ
    ; ℕ₊₁→ℤ to [1+_ⁿ]ᶻ
    )
open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)

postulate
  _<ᶻ_ : ℤ → ℤ → hProp ℓ-zero

_<'_ : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → hProp ℓ-zero
(aᶻ , aⁿ) <' (bᶻ , bⁿ) =
  let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
  in (aᶻ * bⁿᶻ) <ᶻ (bᶻ * aⁿᶻ)

postulate
  <'-respects-∼ˡ : ∀ a b x → a ∼ b → a <' x ≡ b <' x
  <'-respects-∼ʳ : ∀ x a b → a ∼ b → x <' a ≡ x <' b

_<_ : ℚ → ℚ → hProp ℓ-zero
a < b = SetQuotient.rec2 {R = _∼_} {B = hProp ℓ-zero} isSetHProp _<'_ <'-respects-∼ˡ <'-respects-∼ʳ a b

isProp⊎ˡ : ∀{ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → (A → ¬ᵗ B) → isProp (A ⊎ B)
isProp⊎ˡ pA pB A⇒¬B (inl x) (inl y) = cong inl (pA x y)
isProp⊎ˡ pA pB A⇒¬B (inr x) (inr y) = cong inr (pB x y)
isProp⊎ˡ pA pB A⇒¬B (inl x) (inr y) = ⊥-elim (A⇒¬B x y)
isProp⊎ˡ pA pB A⇒¬B (inr x) (inl y) = ⊥-elim (A⇒¬B y x)

⊎ᵖ-syntax : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → {[ P ] → [ ¬ Q ]} → hProp _
⊎ᵖ-syntax P Q {P⇒¬Q} = ([ P ] ⊎ [ Q ]) , isProp⊎ˡ (isProp[] P) (isProp[] Q) P⇒¬Q

syntax ⊎ᵖ-syntax P Q {P⇒¬Q} = [ P⇒¬Q ] P ⊎ᵖ Q

postulate
  <-asym : ∀ x y → [ x < y ] → [ ¬(y < x) ]

_#_ : ℚ → ℚ → hProp ℓ-zero
x # y = [ <-asym x y ] (x < y) ⊎ᵖ (y < x)

_⁻¹''' : (x : ℚ) → [ x # 0 ] → ℚ
_⁻¹''' = SetQuotient.elim {R = _∼_} {B = λ x → [ x # 0 ] → ℚ} φ _⁻¹'' ⁻¹''-respects-∼ where
  φ : ∀ x → isSet ([ x # 0 ] → ℚ)
  φ x = isSetΠ (λ _ → isSetℚ)
  _⁻¹''  : (a : ℤ × ℕ₊₁) → [ [ a ]ᶠ # 0 ] → ℚ
  x ⁻¹'' = {!!}
  ⁻¹''-respects-∼ : (a b : ℤ × ℕ₊₁) (r : a ∼ b)
                  → PathP (λ i → [ eq/ a b r i # 0 ] → ℚ) (a ⁻¹'') (b ⁻¹'')
  ⁻¹''-respects-∼ a b r = {!!}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat

-- setup

infixl 5 _>>=_
_>>=_ = bindTC

defToTerm : Name → Definition → List (Arg Term) → Term
defToTerm _ (function cs) as = pat-lam cs as
defToTerm _ (data-cons d) as = con d as
defToTerm _ _ _ = unknown

data Tm : Set where
  tm : Term → Tm

macro
  unfold : Name → Term → TC ⊤
  unfold x a = getDefinition x >>= λ d → unify a (defToTerm x d [])

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

Point = Vec Nat 3

renderBuffer : List Point → List Nat
renderBuffer [] = []
renderBuffer ((x ∷ y ∷ z ∷ []) ∷ xs) = x ∷ y ∷ z ∷ renderBuffer xs

renderBuffer' : List Point → List Nat
renderBuffer' = unfold renderBuffer

ps : List Point
ps = (1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ []

open import Agda.Builtin.Equality

check : renderBuffer' ps ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ []
check = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
--------------------------------------------------------------------------------
-- This file contains the definition of a context-free grammar, as well as a
-- parser for those grammars that are actually of LL1 type. There is currently
-- no check if the grammar is actually a LL1 grammar, so the parser might loop
-- indefinitely or return an error message in certain cases, even if the string
-- actually matches the grammar.
--------------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

module Parse.LL1 where

import Data.String as S
open import Data.Sum using (isInj₁)
open import Class.Monad.Except
open import Data.String using (fromList; toList; uncons)
open import Data.List using (boolDropWhile)
open import Data.Tree

open import Prelude

record CFG (V : Set) (MultiChar : Set) : Set₁ where
  field
    S : V
    R : V → Set
    AllRules : (v : V) → List (R v)

  -- whether to keep track of the result
  V' : Set
  V' = V × Bool

  field
    Rstring'' : {v : V} → R v → List (V' ⊎ MultiChar ⊎ String)

  Terminal : Set
  Terminal = MultiChar ⊎ String

  isMultiChar : Terminal → Bool
  isMultiChar (inj₁ _) = true
  isMultiChar (inj₂ _) = false

  terminalLength : Terminal → ℕ
  terminalLength (inj₁ x) = 1
  terminalLength (inj₂ y) = S.length y

  Rule : Set
  Rule = ∃[ v ] R v

  Rstring : {v : V} → R v → List (V ⊎ MultiChar ⊎ String)
  Rstring r = map (Data.Sum.map₁ proj₁) (Rstring'' r)

  Rstring' : Rule → List (V ⊎ Terminal)
  Rstring' (_ , r) = Rstring r

  SynTree : Set
  SynTree = Tree (Rule ⊎ Char)

  private variable v : V

  produces-ε : R v → Bool
  produces-ε = null ∘ Rstring

module _ {V MultiChar : Set} (showV : V → String)
  (matchMulti : MultiChar → Char → Bool) (showMulti : MultiChar → String)
  (G : CFG V MultiChar) (M : Set → Set) {{_ : Monad M}} {{_ : MonadExcept M String}} where
  -- we don't care if it is actually a LL1 grammar

  private variable v : V

  open CFG G

  showTerminal : Terminal → String
  showTerminal (inj₁ x) = showMulti x
  showTerminal (inj₂ y) = y

  match : String → Terminal → Bool
  match s (inj₁ x) with strHead s
  ... | nothing = false
  ... | just c  = matchMulti x c
  match s (inj₂ y) = strTake (S.length y) s ≣ y

  -- select the first rule satisfying the predicate
  firstRule : (v : V) → (R v → Bool) → Maybe (R v)
  firstRule v P = head $ boolDropWhile (not ∘ P) $ AllRules v

  {-# NON_TERMINATING #-}
  parsingTable : V → String → Maybe Rule
  parsingTable v' x = -,_ <$> firstRule v' (startWith x) <∣> firstRule v' produces-ε
                      -- select the first rule starting with x, or the first that is empty
    where
      startWith : String → R v → Bool
      startWith x = helper x ∘ Rstring
        where
          helper : String → List (V ⊎ Terminal) → Bool
          helper x [] = false
          helper x (inj₁ v ∷ rest) with boolFilter (startWith x) (AllRules v)
          ... | [] = if null $ boolFilter produces-ε (AllRules v) then false else helper x rest
          ... | _  = true
          helper x (inj₂ t ∷ _) = match x t

  {-# NON_TERMINATING #-}
  parseWithInitNT : V → String → M (SynTree × String)
  parseWithInitNT v a = do
    (y , rest) ← helper [ inj₁ v ] a
    maybe
      (λ z → return (z , rest)) (throwError "BUG: Error while creating syntax tree.")
      (resToTree y)
    where
      helper : List (V ⊎ Terminal) → String → M (List (Rule ⊎ Char) × String)
      helper [] s = return ([] , s)
      helper (inj₁ x ∷ stack) s with parsingTable x s
      ... | just r  = map₁ (inj₁ r ∷_) <$> helper (Rstring' r ++ stack) s
      ... | nothing = throwError $
          "No applicable rule found for non-terminal " + showV x + "\nRemaining:\n" + s
      helper (inj₂ y ∷ stack) s with uncons s | match s y
      ... | just (x , _) | true  = let prepend = if isMultiChar y then inj₂ x ∷_ else id
        in map₁ prepend <$> helper stack (strDrop (terminalLength y) s)
      ... | just       _ | false = throwError $
          "Mismatch while parsing characters: tried to parse " + showTerminal y +
          " but got '" + s + "'"
      ... | nothing | _ = throwError ("Unexpected end of input while trying to parse " + showTerminal y)

      resToTree : List (Rule ⊎ Char) → Maybe SynTree
      resToTree x = proj₁ <$> resToTree' x
        where
          needsChild : V' ⊎ Terminal → Bool
          needsChild (inj₁ x) = true
          needsChild (inj₂ (inj₁ x)) = true
          needsChild (inj₂ (inj₂ y)) = false

          attachChild : V' ⊎ Terminal → Bool
          attachChild (inj₁ (_ , b)) = b
          attachChild _              = true

          resToTree' : List (Rule ⊎ Char) → Maybe (SynTree × List (Rule ⊎ Char))
          ruleChildren : List (V' ⊎ Terminal) → List (Rule ⊎ Char) → Maybe (List SynTree × List (Rule ⊎ Char))

          resToTree' [] = nothing
          resToTree' (inj₁ l ∷ l₁) with ruleChildren (Rstring'' (proj₂ l)) l₁
          ... | just (fst , snd)   = just (Node (inj₁ l) fst , snd)
          ... | nothing            = nothing
          resToTree' (inj₂ l ∷ l₁) = just (Node (inj₂ l) [] , l₁)

          ruleChildren [] l = just ([] , l)
          ruleChildren (x ∷ s) l with needsChild x | resToTree' l
          ... | false | _               = ruleChildren s l
          ... | true  | just (t , rest) = (if attachChild x then map₁ (t ∷_) else id) <$> ruleChildren s rest
          ... | true  | nothing         = nothing

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Limits where

open import Cubical.Categories.Limits.Base public
open import Cubical.Categories.Limits.Initial public
open import Cubical.Categories.Limits.Terminal public
open import Cubical.Categories.Limits.Pullback public

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
------------------------------------------------------------------------
-- A terminating parser data type and the accompanying interpreter
------------------------------------------------------------------------

module RecursiveDescent.InductiveWithFix.Internal where

open import Data.Bool
open import Data.Product.Record
open import Data.Maybe
open import Data.BoundedVec.Inefficient
import Data.List as L
open import Data.Nat
open import Category.Applicative.Indexed
open import Category.Monad.Indexed
open import Category.Monad.State

open import RecursiveDescent.Index
open import Utilities

------------------------------------------------------------------------
-- Lifting non-terminals

-- Extends a non-terminal type with a fresh non-terminal.

data Lift (i : Index) (r : Set) (nt : ParserType₁) : ParserType₁ where
  fresh : Lift i r nt i r
  ↟     : forall {i' r'} -> nt i' r' -> Lift i r nt i' r'

------------------------------------------------------------------------
-- Parser data type

-- A type for parsers which can be implemented using recursive
-- descent. The types used ensure that the implementation below is
-- structurally recursive.

-- The parsers are indexed on a type of nonterminals.

data Parser (tok : Set) (nt : ParserType₁) : ParserType₁ where
  !_     :  forall {e c r}
         -> nt (e , c) r -> Parser tok nt (e , step c) r
  fix    :  forall {e c r}
         -> Parser tok (Lift (e , step c) r nt) (e , c) r
         -> Parser tok nt (e , step c) r
  symbol :  Parser tok nt (false , leaf) tok
  ret    :  forall {r} -> r -> Parser tok nt (true , leaf) r
  fail   :  forall {r} -> Parser tok nt (false , leaf) r
  bind₀  :  forall {c₁ e₂ c₂ r₁ r₂}
         -> Parser tok nt (true , c₁) r₁
         -> (r₁ -> Parser tok nt (e₂ , c₂) r₂)
         -> Parser tok nt (e₂ , node c₁ c₂) r₂
  bind₁  :  forall {c₁ r₁ r₂} {i₂ : r₁ -> Index}
         -> Parser tok nt (false , c₁) r₁
         -> ((x : r₁) -> Parser tok nt (i₂ x) r₂)
         -> Parser tok nt (false , step c₁) r₂
  alt₀   :  forall {c₁ e₂ c₂ r}
         -> Parser tok nt (true , c₁)         r
         -> Parser tok nt (e₂   , c₂)         r
         -> Parser tok nt (true , node c₁ c₂) r
  alt₁   :  forall {c₁} e₂ {c₂ r}
         -> Parser tok nt (false , c₁)         r
         -> Parser tok nt (e₂    , c₂)         r
         -> Parser tok nt (e₂    , node c₁ c₂) r

------------------------------------------------------------------------
-- Lifting parsers

Map : (ParserType₁ -> ParserType₁) -> Set2
Map F = forall {nt nt' i r} ->
        (nt i r -> nt' i r) -> (F nt i r -> F nt' i r)

liftMap : forall (F : ParserType₁ -> ParserType₁) {i' r'} ->
          Map F -> Map (Lift i' r' ∘₂ F)
liftMap F map g fresh = fresh
liftMap F map g (↟ x) = ↟ (map g x)

lift' : forall {tok nt i r i' r'}
        (F : ParserType₁ -> ParserType₁) -> Map F ->
        Parser tok (F nt) i r -> Parser tok (F (Lift i' r' nt)) i r
lift' F map (! x)               ~ ! (map ↟ x)
lift' F map (fix {e} {c} {r} p) ~ fix (lift' (Lift (e , step c) r ∘₂ F)
                                             (liftMap F map) p)
lift' F map symbol              ~ symbol
lift' F map (ret x)             ~ ret x
lift' F map fail                ~ fail
lift' F map (bind₀  p₁ p₂)      ~ bind₀  (lift' F map p₁) (\x -> lift' F map (p₂ x))
lift' F map (bind₁  p₁ p₂)      ~ bind₁  (lift' F map p₁) (\x -> lift' F map (p₂ x))
lift' F map (alt₀   p₁ p₂)      ~ alt₀   (lift' F map p₁) (lift' F map p₂)
lift' F map (alt₁ e p₁ p₂)      ~ alt₁ e (lift' F map p₁) (lift' F map p₂)

-- Note that lift p is linear in the size of p (in a sense; note that
-- p can contain higher-order components), assuming that p contains at
-- most <some constant> occurrences of fix.

lift : forall {tok nt i r i' r'} ->
       Parser tok nt i r -> Parser tok (Lift i' r' nt) i r
lift p = lift' (\nt -> nt) (\f -> f) p

------------------------------------------------------------------------
-- Run function for the parsers

-- Grammars.

Grammar : Set -> ParserType₁ -> Set1
Grammar tok nt = forall {i r} -> nt i r -> Parser tok nt i r

-- Extends a grammar with a case for a fresh non-terminal.

_▷_ : forall {tok nt i r} ->
      Grammar tok nt -> Parser tok nt i r ->
      Grammar tok (Lift i r nt)
(g ▷ p) fresh = lift p
(g ▷ p) (↟ x) = lift (g x)

-- Parser monad.

P : Set -> IFun ℕ
P tok = IStateT (BoundedVec tok) L.List

PIMonadPlus : (tok : Set) -> RawIMonadPlus (P tok)
PIMonadPlus tok = StateTIMonadPlus (BoundedVec tok) L.monadPlus

PIMonadState : (tok : Set) -> RawIMonadState (BoundedVec tok) (P tok)
PIMonadState tok = StateTIMonadState (BoundedVec tok) L.monad

private
  open module LM {tok} = RawIMonadPlus  (PIMonadPlus  tok)
  open module SM {tok} = RawIMonadState (PIMonadState tok)
                           using (get; put; modify)

-- For every successful parse the run function returns the remaining
-- string. (Since there can be several successful parses a list of
-- strings is returned.)

-- This function is structurally recursive with respect to the
-- following lexicographic measure:
--
-- 1) The upper bound of the length of the input string.
-- 2) The parser's proper left corner tree.

mutual
  parse : forall {tok nt} -> Grammar tok nt ->
          forall n {e c r} ->
          Parser tok nt (e , c) r ->
          P tok n (if e then n else pred n) r
  parse g n       (! x)              = parse g n (g x)
  parse g n       (fix p)            = parse (g ▷ fix p) n p
  parse g zero    symbol             = ∅
  parse g (suc n) symbol             = eat =<< get
  parse g n       (ret x)            = return x
  parse g n       fail               = ∅
  parse g n       (bind₀      p₁ p₂) = parse  g  n      p₁ >>= parse  g n ∘′ p₂
  parse g zero    (bind₁      p₁ p₂) = ∅
  parse g (suc n) (bind₁      p₁ p₂) = parse  g (suc n) p₁ >>= parse↑ g n ∘′ p₂
  parse g n       (alt₀       p₁ p₂) = parse  g  n      p₁ ∣   parse↑ g n    p₂
  parse g n       (alt₁ true  p₁ p₂) = parse↑ g  n      p₁ ∣   parse  g n    p₂
  parse g n       (alt₁ false p₁ p₂) = parse  g  n      p₁ ∣   parse  g n    p₂

  parse↑ : forall {tok nt} -> Grammar tok nt ->
           forall n {e c r} -> Parser tok nt (e , c) r -> P tok n n r
  parse↑ g n       {true}  p = parse g n p
  parse↑ g zero    {false} p = ∅
  parse↑ g (suc n) {false} p = parse g (suc n) p >>= \r ->
                               modify ↑ >>
                               return r

  eat : forall {tok n} -> BoundedVec tok (suc n) -> P tok (suc n) n tok
  eat []      = ∅
  eat (c ∷ s) = put s >> return c

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
-- This module proves the two "VotesOnce" proof obligations for our fake handler

open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS

import      LibraBFT.Concrete.Properties.VotesOnce as VO
open import LibraBFT.Impl.Base.Types

open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Consensus.RoundManager.Properties
open import LibraBFT.Impl.Handle
open import LibraBFT.Impl.Handle.Properties
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Util.Util
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Types
open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})
open        WithSPS impl-sps-avp
open        Structural impl-sps-avp

-- In this module, we prove the two implementation obligations for the VotesOnce rule.  Note
-- that it is not yet 100% clear that the obligations are the best definitions to use.  See comments
-- in Concrete.VotesOnce.  We will want to prove these obligations for the fake/simple
-- implementation (or some variant on it) and streamline the proof before we proceed to tackle more
-- ambitious properties.

module LibraBFT.Impl.Properties.VotesOnce where

  -- This is the information we can establish about the state after the first time a signature is
  -- sent, and that we can carry forward to subsequent states, so we can use it to prove
  -- VO.ImplObligation₁.
  LvrProp : CarrierProp
  LvrProp v rm = (  v ^∙ vEpoch ≢ (₋rmEC rm) ^∙ rmEpoch
                 ⊎ (v ^∙ vEpoch ≡ (₋rmEC rm) ^∙ rmEpoch × v ^∙ vRound ≤ (₋rmEC rm) ^∙ rmLastVotedRound))

  LvrCarrier = PropCarrier LvrProp

  firstSendEstablishes : Vote → PK → (origSt : SystemState) → SystemStateRel Step
  firstSendEstablishes _ _ _ (step-peer (step-cheat _)) = Lift (ℓ+1 ℓ-RoundManager) ⊥
  firstSendEstablishes   v' pk origSt sysStep@(step-peer {pid'} {pre = pre} pstep@(step-honest _)) =
                         ( ReachableSystemState pre
                         × ¬ MsgWithSig∈ pk (signature v' unit) (msgPool pre)
                         × LvrCarrier pk (₋vSignature v') (StepPeer-post pstep)
                         )
  open PeerCanSignForPK

  isValidNewPart⇒fSE : ∀ {pk v'}{pre : SystemState} {post : SystemState} {theStep : Step pre post}
                     → Meta-Honest-PK pk
                     → (ivnp : IsValidNewPart (₋vSignature v') pk theStep)
                     → firstSendEstablishes v' pk pre theStep
  isValidNewPart⇒fSE {pre = pre} {theStep = step-peer {pid = β} {outs = outs} pstep} hpk (_ , ¬init , ¬sentb4 , mws , _)
     with Any-++⁻ (actionsToSentMessages β outs) (msg∈pool mws)
     -- TODO-1 : Much of this proof is not specific to the particular property being proved, and could be
     -- refactored into Yasm.Properties.  See proof of unwind and refactor to avoid redundancy?
  ...| inj₂ furtherBack = ⊥-elim (¬sentb4 (MsgWithSig∈-transp mws furtherBack))
  ...| inj₁ thisStep
     with pstep
  ...| step-cheat isCheat
     with thisStep
  ...| here refl
     with isCheat (msg⊆ mws) (msgSigned mws) (transp-¬∈GenInfo₁ ¬init mws)
  ...| inj₁ dis = ⊥-elim (hpk dis)
  ...| inj₂ sentb4 rewrite msgSameSig mws = ⊥-elim (¬sentb4 sentb4)

  isValidNewPart⇒fSE {pk}{v'}{pre}{theStep = step-peer {β} {postst} {outs} {.pre} pstep} hpk (r , ¬init , ¬sentb4 , mws , refl , zefl , vpk)
     | inj₁ thisStep
     | step-honest {.β} hstep
     with senderMsgPair∈⇒send∈ outs thisStep
  ...| nm∈outs , refl
     with hstep
  ...| step-msg {_ , P m} m∈pool ini
     with impl-sps-avp {m = msgWhole mws} r hpk hstep nm∈outs (msg⊆ mws) (msgSigned mws) (transp-¬∈GenInfo₁ ¬init mws )
  ...| inj₂ sentb4 rewrite msgSameSig mws = ⊥-elim (¬sentb4 sentb4)
  ...| inj₁ (vpk' , _)
     with noEpochIdChangeYet {ppre = peerStates pre β} r refl hstep ini
  ...| eids≡
     with newVoteSameEpochGreaterRound r hstep (¬subst ¬init (msgSameSig mws)) hpk (msg⊆ mws) nm∈outs (msgSigned mws)
                                               (¬subst ¬sentb4 (msgSameSig mws))
  ...| refl , refl , newlvr
     with StepPeer-post-lemma pstep
  ...| post≡ = r , ¬sentb4 , mkCarrier (step-s r (step-peer (step-honest hstep)))
                                       mws
                                       (override-target-≡ {a = β})
                                       vpk'
                                       (inj₂ ( trans eids≡ (auxEid post≡)
                                             , ≤-reflexive (trans newlvr (auxLvr post≡))))
                                       where auxEid = cong (_^∙ rmEpoch ∘ ₋rmEC)
                                             auxLvr = cong (_^∙ rmLastVotedRound ∘ ₋rmEC)

  ImplPreservesLvr : PeerStepPreserves LvrProp
  -- We don't have a real model for the initial peer state, so we can't prove this case yet.
  -- Eventually, we'll prove something like a peer doesn't initialize to an epoch for which
  -- it has already sent votes.
  ImplPreservesLvr r prop (step-init uni) = ⊥-elim (uninitd≢initd (trans (sym uni) (carrInitd prop)))
  ImplPreservesLvr {pre = pre} r prop (step-msg {m} m∈pool inited)
     with carrProp prop
  ...| preprop
     with noEpochIdChangeYet r refl (step-msg m∈pool inited) (carrInitd prop)
  ...| eids≡
     with preprop
  ...| inj₁ diffEpoch = inj₁ λ x → diffEpoch (trans x (sym eids≡))
  ...| inj₂ (sameEpoch , rnd≤ppre)
     with (msgPart (carrSent prop)) ^∙ vEpoch ≟ (₋rmEC (peerStates pre (msgSender (carrSent prop)))) ^∙ rmEpoch
  ...| no neq = ⊥-elim (neq sameEpoch)
  ...| yes refl
     with lastVoteRound-mono r refl (step-msg m∈pool inited) (carrInitd prop)
  ...| es≡⇒lvr≤
     = inj₂ (eids≡ , ≤-trans rnd≤ppre (es≡⇒lvr≤ eids≡))

  LvrCarrier-transp* : ∀ {pk sig} {start : SystemState}{final : SystemState}
                     → LvrCarrier pk sig start
                     → (step* : Step* start final)
                     → LvrCarrier pk sig final
  LvrCarrier-transp* lvrc step-0 = lvrc
  LvrCarrier-transp* lvrc (step-s s* s) = Carrier-transp LvrProp ImplPreservesLvr s (LvrCarrier-transp* lvrc s*)

  fSE⇒rnd≤lvr : ∀ {v' pk}
              → {final : SystemState}
              → Meta-Honest-PK pk
              → ∀ {pre : SystemState}{post : SystemState}{theStep : Step pre post}
              → firstSendEstablishes v' pk post theStep
              → Step* post final
              → LvrCarrier pk (signature v' unit) final
  fSE⇒rnd≤lvr hpk {theStep = step-peer (step-honest _)} (_ , _ , lvrc) step* = LvrCarrier-transp* lvrc step*

  vo₁ : VO.ImplObligation₁
  -- Initialization doesn't send any messages at all so far; Agda figures that out so no proof
  -- required here.  In future it may send messages, but any verifiable Signatures for honest PKs
  -- they contain will be from GenesisInfo.
  vo₁ {pid} {pk = pk} {pre = pre} r sm@(step-msg {(_ , nm)} m∈pool pidini)
      {m = m} {v'} hpk v⊂m m∈outs sig ¬init ¬sentb4 vpb v'⊂m' m'∈pool sig' ¬init' refl rnds≡
     with msgsToSendWereSent {pid} {nm} m∈outs
  ...| _ , vm , _ , refl , _
     with newVoteSameEpochGreaterRound r (step-msg m∈pool pidini) ¬init hpk v⊂m m∈outs sig ¬sentb4
  ...| eIds≡' , suclvr≡v'rnd , _
     -- Use unwind to find the step that first sent the signature for v', then Any-Step-elim to
     -- prove that going from the poststate of that step to pre results in a state in which the
     -- round of v' is at most the last voted round recorded in the peerState of the peer that
     -- sent v'
     with Any-Step-elim {Q = LvrCarrier pk (₋vSignature v') pre}
                        (fSE⇒rnd≤lvr {v'} hpk)
                        (Any-Step-map (λ _ ivnp → isValidNewPart⇒fSE {v' = v'} hpk ivnp)
                                      (unwind r hpk v'⊂m' m'∈pool sig' ¬init'))
  ...| mkCarrier r' mws ini vpf' preprop
     -- The fake/trivial handler always sends a vote for its current epoch, but for a
     -- round greater than its last voted round
     with sameSig⇒sameVoteData (msgSigned mws) sig' (msgSameSig mws)
  ...| inj₁ hb = ⊥-elim (PerState.meta-sha256-cr pre r hb)
  ...| inj₂ refl
     with msgSender mws ≟NodeId pid
  ...| no neq =
     -- We know that *after* the step, pid can sign v (vpb is about the post-state).  For v', we
     -- know it about state "pre"; we transport this to the post-state using
     -- PeerCanSignForPK-Stable.  Because EpochConfigs known in a system state are consistent with
     -- each other (i.e., trivially, for now because only the initial EpochConfig is known), we can
     -- use PK-inj to contradict the assumption that v and v' were sent by different peers (neq).
     let theStep = step-peer (step-honest sm)
         vpf''   = PeerCanSignForPK-stable r theStep vpf'
         𝓔s≡     = availEpochsConsistent {pid} {msgSender mws} (step-s r theStep) vpb vpf''
     in  ⊥-elim (neq (trans (trans (sym (nid≡ vpf''))
                                   (PK-inj-same-ECs (sym 𝓔s≡)
                                                    (trans (pk≡ vpf'') (sym (pk≡ vpb)))))
                            (nid≡ vpb)))

  vo₁ {pid} {pk = pk} {pre = pre} r sm@(step-msg m∈pool ps≡)
      {v' = v'} hpk v⊂m m∈outs sig ¬init ¬sentb4 vpb v'⊂m' m'∈pool sig' _ refl rnds≡
     | _ , vm , _ , refl , _
     | eIds≡' , suclvr≡v'rnd , _
     | mkCarrier r' mws ini vpf' preprop
     | inj₂ refl
     | yes refl
     with preprop
  ...| inj₁ diffEpoch = ⊥-elim (diffEpoch eIds≡')
  ...| inj₂ (sameEpoch , v'rnd≤lvr)
                    -- So we have proved both that the round of v' is ≤ the lastVotedRound of
                    -- the peer's state and that the round of v' is one greater than that value,
                    -- which leads to a contradiction
                    = ⊥-elim (1+n≰n (≤-trans (≤-reflexive suclvr≡v'rnd)
                                             (≤-trans (≤-reflexive rnds≡) v'rnd≤lvr)))

  -- TODO-1: This proof should be refactored to reduce redundant reasoning about the two votes.  The
  -- newVoteSameEpochGreaterRound property uses similar reasoning.

  vo₂ : VO.ImplObligation₂
  vo₂ {pid = pid} {pk = pk} {pre = pre} r (step-msg {_ , nm} m∈pool pinit) {v = v} {m}
      hpk v⊂m m∈outs sig ¬init vnew vpk v'⊂m' m'∈outs sig' ¬init' v'new vpk' es≡ rnds≡
     with msgsToSendWereSent {pid} {nm} m∈outs
  ...| _ , vm , pm , refl , refl
    with proposalHandlerSentVote {pid} {0} {pm} {vm} {peerStates pre pid} m∈outs
  ...| _ , v∈outs
    with v⊂m
       -- Rebuilding keeps the same signature, and the SyncInfo included with the
       -- VoteMsg sent comprises QCs from the peer's state.  Votes represented in
       -- those QCS have signatures that have been sent before, contradicting the
       -- assumption that v's signature has not been sent before.
  ...| vote∈qc {vs = vs} {qc} vs∈qc v≈rbld (inV qc∈m)
                  rewrite cong ₋vSignature v≈rbld
                        | procPMCerts≡ {0} {pm} {peerStates pre pid} {vm} v∈outs
                        | SendVote-inj-v (Any-singleton⁻ v∈outs)
     with qcVotesSentB4 r pinit
                        (VoteMsgQCsFromRoundManager r (step-msg m∈pool pinit) hpk v⊂m m∈outs qc∈m) vs∈qc ¬init
  ...| mws = ⊥-elim (vnew mws)

  vo₂ {pid = pid} {pk = pk} {pre = pre} r (step-msg {_ , nm} m∈pool pinit) {v = v} {m} {v'} {m'}
      hpk v⊂m m∈outs sig ¬init vnew vpk v'⊂m' m'∈outs sig' ¬init' v'new vpk' es≡ rnds≡
     | _ , vm , pm , refl , refl
     | _ , v∈outs
     | vote∈vm
     with msgsToSendWereSent {pid} {nm} {m'} {st = peerStates pre pid} m'∈outs
  ...| _ , vm' , pm , refl , refl
    with proposalHandlerSentVote {pid} {0} {pm} {vm'} {peerStates pre pid} m'∈outs
  ...| _ , v'∈outs
       rewrite cong ₋vmVote (SendVote-inj-v (trans (Any-singleton⁻ v∈outs) (sym (Any-singleton⁻ v'∈outs))))
    with v'⊂m'
  ...| vote∈vm = refl
  ...| vote∈qc {vs = vs} {qc} vs∈qc v≈rbld (inV qc∈m)
                  rewrite cong ₋vSignature v≈rbld
                        | procPMCerts≡ {0} {pm} {peerStates pre pid} {vm} v∈outs
                        | SendVote-inj-v (Any-singleton⁻ v∈outs)
                        | cong ₋vmVote (SendVote-inj-v (trans (Any-singleton⁻ v∈outs) (sym (Any-singleton⁻ v'∈outs))))
    with qcVotesSentB4 r pinit
                       (VoteMsgQCsFromRoundManager r (step-msg m∈pool pinit) hpk v'⊂m' m'∈outs qc∈m) vs∈qc ¬init'
  ...| mws = ⊥-elim (v'new mws)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Prelude.Exit where

open import Prelude.Char
open import Prelude.IO
open import Prelude.Unit

postulate
  exit : Char → IO Unit

{-# COMPILED_EPIC exit (n : Int, u : Unit) ->
                       Unit = foreign Unit "exit" (n : Int) #-}

exitSuccess : Char
exitSuccess = '\NUL'

exitFailure : Char
exitFailure = '\SOH'


text:
-- Agda program using the Iowa Agda library

open import bool

module PROOF-evendoublecoin
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

add : ℕ → ℕ → ℕ
add zero x = x
add (suc y) z = suc (add y z)

coin : Choice → ℕ → ℕ
coin c1 x = if choose c1 then x else suc x

double : ℕ → ℕ
double x = add x x

even : ℕ → 𝔹
even zero = tt
even (suc zero) = ff
even (suc (suc x)) = even x

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

add-suc : ∀ (x y : ℕ) → add x (suc y) ≡ suc (add x y)
add-suc zero y = refl
add-suc (suc x) y rewrite add-suc x y = refl

-- auxiliary property for x+x instead of double:
even-add-x-x : ∀ (x : ℕ) → even (add x x) ≡ tt
even-add-x-x zero = refl
even-add-x-x (suc x) rewrite add-suc x x | even-add-x-x x = refl

evendoublecoin : (c1 : Choice) → (x : ℕ) → (even (double (coin c1 x))) ≡ tt
evendoublecoin c1 x rewrite even-add-x-x (coin c1 x) = refl

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


text:
-- Andreas, 2018-06-03, issue #3057 reported by nad.
-- We should not allow the public import of an ambiguous identifier

-- {-# OPTIONS -v scope:20 #-}

module Issue3057 where

module M where

  postulate
    A : Set
    a : A

open M public renaming (a to A)

-- Should fail

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This file contains:

- Definition of set truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetTruncation.Base where

open import Cubical.Core.Primitives

-- set truncation as a higher inductive type:

data ∥_∥₂ {ℓ} (A : Type ℓ) : Type ℓ where
  ∣_∣₂ : A → ∥ A ∥₂
  squash₂ : ∀ (x y : ∥ A ∥₂) (p q : x ≡ y) → p ≡ q

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

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

open import Prelude

open import Labelled-transition-system

module Bisimilarity.Classical.Equational-reasoning-instances
         {ℓ} {lts : LTS ℓ} where

open import Bisimilarity.Classical lts

open import Equational-reasoning

instance

  reflexive∼ : Reflexive _∼_
  reflexive∼ = is-reflexive reflexive-∼

  symmetric∼ : Symmetric _∼_
  symmetric∼ = is-symmetric symmetric-∼

  trans∼∼ : Transitive _∼_ _∼_
  trans∼∼ = is-transitive transitive-∼

  convert∼∼ : Convertible _∼_ _∼_
  convert∼∼ = is-convertible id

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-# OPTIONS -v 2 #-}
module Leftovers.Examples where

open import Leftovers.Utils
open import Leftovers.Leftovers
open import Leftovers.Equality

open import Data.Bool
open import Relation.Binary.PropositionalEquality

open import Data.Nat
open import Data.Product

open import Data.Unit

-- notNot :  ∀ b → not (not b) ≡ b
-- notNot = (by {A = ∀ b → not (not b) ≡ b} (cases (quote Bool)) {!!}) -- (refl , refl)

-- applyTo : ∀ {ℓ1 ℓ2} {X : Set ℓ1} { Y : Set ℓ2 } → (X → Y) → X → Y
-- applyTo f x = f x

-- infixr 40 applyTo
-- syntax applyTo e₁ (λ x → e₂) = x ≔ e₁ ︔ e₂

plusZero : ∀ n → n ≡ n + 0
plusZero =
   getNormal (by {A = ∀ n → n ≡ n + 0} (cases (quote ℕ)) ((λ x → cong suc (plusZero x)) , refl))
   -- (by {A = ∀ n → n ≡ n + 0} (cases (quote ℕ)) ((λ x → cong suc (plusZero x)) , refl))

-- plusZero' : ∀ n → n ≡ n + 0
-- plusZero' = getNormal
--   ((the ((zero ≡ zero × (∀ x → suc x ≡ suc x + 0)) → ∀ n → n ≡ n + 0) λ h → identity (λ { zero → proj₁ h ; (suc x) → (proj₂ h) x }))
--     (refl , λ x → cong suc (plusZero' x)))

-- -- plusZero'' : ∀ n → n ≡ n + 0
-- -- plusZero'' = (the (zero ≡ zero → (∀ x → suc x ≡ suc x + 0) → ∀ n → n ≡ n + 0) λ h1 h2 → (λ { zero → h1 ; (suc x) → h2 x})) refl  ((the (Dummy → ∀ x → suc x ≡ suc x + 0) (λ {dummy → λ x → cong suc (plusZero'' x)})) dummy)

-- -- plusZero' =
-- --   let
-- --     h : (zero ≡ zero × ∀ n → suc n ≡ (suc n) + 0)
-- --     h = refl , λ n → cong suc (plusZero' n)
-- --   in λ { zero → proj₁ h ; (suc x) → (proj₂ h) x}
-- -- plusZeroR : ∀ n → n + 0 ≡ n
-- -- plusZeroR = by (refl-cases (quote ℕ)) ?

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
-- This example comes from the discussion on Issue423.
module SolveNeutralApplication where

postulate
  A : Set
  a b : A
  T : A → Set
  mkT : ∀ a → T a
  phantom : A → A → A

data Bool : Set where
  true false : Bool

f : Bool → A → A
f true  x = phantom x a
f false x = phantom x b
-- Andreas, 2012-09-07: the original f did not have "phantom x",
-- thus, x was cleary unused.  With fixing issue 691 Agda tracks
-- constant functions in the type system, thus, reasoning as below
-- no longer works.  We have to make f use its second argument.

-- We can solve the constraint
--   f x _4 == f x y
-- with
--   _4 := y
-- since the application of f is neutral.
g : (x : Bool)(y : A) → T (f x y)
g x y = mkT (f x _)


text:
open import Coinduction using ( ∞ ; ♯_ ; ♭ )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
open import Data.Empty using ( ⊥ )
open import Data.Maybe using ( Maybe ; just ; nothing )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Natural using ( Natural ; # )
open import Data.String using ( String )
open import Data.ByteString using ( ByteString ; strict ; length )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

module System.IO.Transducers.Session where

-- Unidirectional sessions.  These can be viewed as trees,
-- where each node is labelled by a set A, and has a child
-- for each element of A.

-- These are a lot like session types, but are unidirectional,
-- not bidirectional, and are not designed to support session
-- mobility.

-- They are also a lot like arenas in game semantics, but again
-- are unidirectional.

-- They're a lot like the container types from Ghani, Hancock
-- and Pattison's "Continuous functions on final coalgebras".
-- Note that we are supporting weighted sets, similar to theirs,
-- in order to support induction over weights of input,
-- e.g. on bytestring input we can do induction over the length
-- of the bytestring.

-- Finally, they are a lot like automata: states are sessions,
-- acceptors are leaves, transitions correspond to children.

infixr 4 _∼_
infixr 6 _⊕_
infixr 7 _&_ _&*_

-- Weighting for a set

Weighted : Set → Set
Weighted A = A → Natural

-- Discrete weighting function

δ : ∀ {A} → (Weighted A)
δ a = # 1

-- Sessions are trees of weighted sets

data Session : Set₁ where
  I : Session
  Σ : {A : Set} → (W : Weighted A) → (F : ∞ (A → Session)) → Session

-- Equivalence of sessions

data _∼_ : Session → Session → Set₁ where
  I : I ∼ I
  Σ : {A : Set} → (W : Weighted A) → {F₁ F₂ : ∞ (A → Session)} →
    ∞ (∀ a → ♭ F₁ a ∼ ♭ F₂ a) → (Σ W F₁ ∼ Σ W F₂)

∼-refl : ∀ {S} → (S ∼ S)
∼-refl {I}     = I
∼-refl {Σ V F} = Σ V (♯ λ a → ∼-refl {♭ F a})

∼-sym : ∀ {S T} → (S ∼ T) → (T ∼ S)
∼-sym I       = I
∼-sym (Σ V F) = Σ V (♯ λ a → ∼-sym (♭ F a))

∼-trans : ∀ {S T U} → (S ∼ T) → (T ∼ U) → (S ∼ U)
∼-trans I       I        = I
∼-trans (Σ V F) (Σ .V G) = Σ V (♯ λ a → ∼-trans (♭ F a) (♭ G a))

-- Inital alphabet

Γ : Session → Set
Γ I           = ⊥
Γ (Σ {A} W F) = A

Δ : ∀ S → (Weighted (Γ S))
Δ I       ()
Δ (Σ W F) a = W a

_/_ : ∀ S → (Γ S) → Session
I       / ()
(Σ W F) / a = ♭ F a

-- IsI S is inhabited whenever S ≡ I

IsI : Session → Set
IsI I       = ⊤
IsI (Σ V F) = ⊥

-- IsΣ S is inhabited whenever S is of the form Σ V F

IsΣ : Session → Set
IsΣ I       = ⊥
IsΣ (Σ V F) = ⊤

-- IsΣ respects ≡.

IsΣ-≡ : ∀ {S} {isΣ : IsΣ S} {T} → (S ≡ T) → (IsΣ T)
IsΣ-≡ {Σ V F} refl = tt
IsΣ-≡ {I}  {} refl

-- Singletons

⟨_w/_⟩ : (A : Set) → (Weighted A) → Session
⟨ A w/ W ⟩ = Σ W (♯ λ a → I)

⟨_⟩ : Set → Session
⟨ A ⟩ = ⟨ A w/ δ ⟩

-- Sequencing

_&_ : Session → Session → Session
I       & T = T
(Σ V F) & T = Σ V (♯ λ a → ♭ F a & T)

-- Units and associativity

unit₁ : ∀ {S} → (I & S ∼ S)
unit₁ = ∼-refl

unit₂ : ∀ {S} → (S & I ∼ S)
unit₂ {I} = I
unit₂ {Σ V F} = Σ V (♯ λ a → unit₂ {♭ F a})

assoc : ∀ {S T U} → (S & (T & U) ∼ (S & T) & U)
assoc {I} = ∼-refl
assoc {Σ V F} = Σ V (♯ λ a → assoc {♭ F a})

-- Lazy choice

_+_ : Session → Session → Session
S + T = Σ δ (♯ λ b → if b then S else T)

-- Strict choice

_⊕_ : Session → Session → Session
I ⊕ T = I
S ⊕ I = I
S ⊕ T = S + T

-- Lazy option

¿ : Session → Session
¿ S = S + I

-- Lazy Kleene star

-- It would be nice if I could just define * S = ¿ (S & * S),
-- but that doesn't pass the termination checker, so I have
-- to expand out the definition.

hd : Session → Set
hd I           = Bool
hd (Σ {A} W F) = A

wt : ∀ S → (Weighted (hd S))
wt I       = δ
wt (Σ W F) = W

mutual

  tl : ∀ S T → (hd S) → Session
  tl I       T true  = T &* T
  tl I       T false = I
  tl (Σ W F) T a     = (♭ F a) &* T

  _&*_ : Session → Session → Session
  S &* T = Σ (wt S) (♯ tl S T)

* : Session → Session
* S = I &* S

+ : Session → Session
+ S = S &* S

-- Bytes

Bytes' : Session
Bytes' = + ⟨ ByteString strict w/ length ⟩

Bytes : Session
Bytes = * ⟨ ByteString strict w/ length ⟩

-- TODO: weight strings by their length?

Strings' : Session
Strings' = + ⟨ String ⟩

Strings : Session
Strings = * ⟨ String ⟩

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module Structure.Relator.Names where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Xor
open import Numeral.Natural
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Lvl.Level
private variable T A B C D E : Type{ℓ}

ConversePattern : (Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt{ℓ}) → (A → B → Stmt) → (B → A → Stmt) → Stmt
ConversePattern(_▫_)(_▫₁_)(_▫₂_) = ∀{x}{y} → (x ▫₁ y) ▫ (y ▫₂ x)

Subrelation : (A → B → Stmt{ℓ₁}) → (A → B → Stmt{ℓ₂}) → Stmt
Subrelation(_▫₁_)(_▫₂_) = ∀{x}{y} → (x ▫₁ y) → (x ▫₂ y)

TransitivityPattern : (A → B → Stmt{ℓ₁}) → (B → C → Stmt{ℓ₂}) → (A → C → Stmt{ℓ₃}) → Stmt
TransitivityPattern(_▫₁_)(_▫₂_)(_▫₃_) = ∀{x}{y}{z} → (x ▫₁ y) → (y ▫₂ z) → (x ▫₃ z)

FlippedTransitivityₗPattern : (A → C → Stmt{ℓ₁}) → (B → C → Stmt{ℓ₂}) → (A → B → Stmt{ℓ₃}) → Stmt
FlippedTransitivityₗPattern(_▫₁_)(_▫₂_)(_▫₃_) = ∀{x}{y}{z} → (x ▫₁ z) → (y ▫₂ z) → (x ▫₃ y)

FlippedTransitivityᵣPattern : (A → B → Stmt{ℓ₁}) → (A → C → Stmt{ℓ₂}) → (B → C → Stmt{ℓ₃}) → Stmt
FlippedTransitivityᵣPattern(_▫₁_)(_▫₂_)(_▫₃_) = ∀{x}{y}{z} → (x ▫₁ y) → (x ▫₂ z) → (y ▫₃ z)

module _ (_▫_ : T → T → Stmt{ℓ}) where
  Symmetry : Stmt
  Symmetry = ConversePattern(_→ᶠ_)(_▫_)(_▫_)

  Asymmetry : Stmt
  Asymmetry = ConversePattern(_→ᶠ_)(_▫_)((¬_) ∘₂ (_▫_))

  Reflexivity : Stmt
  Reflexivity = ∀{x : T} → (x ▫ x)

  Transitivity : Stmt
  Transitivity = TransitivityPattern(_▫_)(_▫_)(_▫_)

  SwappedTransitivity : Stmt
  SwappedTransitivity = ∀{x y z : T} → (y ▫ z) → (x ▫ y) → (x ▫ z)

  -- Also called: Left Euclidean.
  FlippedTransitivityₗ : Stmt
  FlippedTransitivityₗ = FlippedTransitivityₗPattern(_▫_)(_▫_)(_▫_)

  -- Also called: Right Euclidean.
  FlippedTransitivityᵣ : Stmt
  FlippedTransitivityᵣ = FlippedTransitivityᵣPattern(_▫_)(_▫_)(_▫_)

  Irreflexivity : Stmt
  Irreflexivity = ∀{x : T} → ¬(x ▫ x)

  -- Also called: Total, complete, connex.
  ConverseTotal : Stmt
  ConverseTotal = ConversePattern(_∨_)(_▫_)(_▫_)

  ConverseDichotomy : Stmt
  ConverseDichotomy = ConversePattern(_⊕_)(_▫_)(_▫_)

  -- Also called: Comparison.
  CoTransitivity : Stmt
  CoTransitivity = ∀{x y z : T} → (x ▫ z) → ((x ▫ y) ∨ (y ▫ z))

module _ (_▫₁_ : T → T → Stmt{ℓ₁}) (_▫₂_ : T → T → Stmt{ℓ₂}) where
  Antisymmetry : Stmt
  Antisymmetry = ∀{a b} → (a ▫₁ b) → (b ▫₁ a) → (a ▫₂ b)

  ConverseTrichotomy : Stmt
  ConverseTrichotomy = ∀{x y} → (x ▫₁ y) ∨ (x ▫₂ y) ∨ (y ▫₁ x)

module _ (_▫₁_ : A → B → Stmt{ℓ₁}) (_▫₂_ : A → A → Stmt{ℓ₂}) where
  Subtransitivityₗ : Stmt
  Subtransitivityₗ = TransitivityPattern(_▫₂_)(_▫₁_)(_▫₁_)

module _ (_▫₁_ : A → B → Stmt{ℓ₁}) (_▫₂_ : B → B → Stmt{ℓ₂}) where
  Subtransitivityᵣ : Stmt
  Subtransitivityᵣ = TransitivityPattern(_▫₁_)(_▫₂_)(_▫₁_)

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:
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.IO
open import Agda.Builtin.String

postulate
  putStr : String → IO ⊤

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

data Sing : Nat → Set where
  sing : Sing zero

data Vec : Nat → Set where
  nil : Vec zero
  cons : ∀ n → Vec n → Vec (suc n)

isTailNil : ∀ m n → Sing m → Vec n → Bool
isTailNil .0 .1 sing (cons zero v) = true  -- two `zero`s are buried in the dot patterns, which to resurrect?
isTailNil _ _ _ _ = false

shouldBeFalse = isTailNil 0 2 sing (cons 1 (cons 0 nil))

isFalse : false ≡ shouldBeFalse
isFalse = refl

magic : false ≡ true → String
magic ()

f : (b : Bool) → false ≡ b → String
f false eq = "Phew!"
f true  eq = magic eq

main = putStr (f shouldBeFalse refl)


text:
------------------------------------------------------------------------------
-- Elimination properties for the inequalities
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Inequalities.EliminationPropertiesI where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities

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

0<0→⊥ : ¬ (zero < zero)
0<0→⊥ 0<0 = t≢f (trans (sym 0<0) lt-00)

S<0→⊥ : ∀ {n} → ¬ (succ₁ n < zero)
S<0→⊥ {n} h = t≢f (trans (sym h) (lt-S0 n))

x<0→⊥ : ∀ {n} → N n → ¬ (n < zero)
x<0→⊥ nzero     0<0  = 0<0→⊥ 0<0
x<0→⊥ (nsucc _) Sn<0 = S<0→⊥ Sn<0

x<x→⊥ : ∀ {n} → N n → ¬ (n < n)
x<x→⊥ nzero          0<0   = 0<0→⊥ 0<0
x<x→⊥ (nsucc {n} Nn) Sn<Sn = ⊥-elim (x<x→⊥ Nn (trans (sym (lt-SS n n)) Sn<Sn))

0>0→⊥ : ¬ (zero > zero)
0>0→⊥ 0>0 = t≢f (trans (sym 0>0) lt-00)

0>S→⊥ : ∀ {n} → ¬ (zero > succ₁ n)
0>S→⊥ {n} h = t≢f (trans (sym h) (lt-S0 n))

0>x→⊥ : ∀ {n} → N n → ¬ (zero > n)
0>x→⊥ nzero     0>0  = 0>0→⊥ 0>0
0>x→⊥ (nsucc _) 0>Sn = 0>S→⊥ 0>Sn

x>x→⊥ : ∀ {n} → N n → ¬ (n > n)
x>x→⊥ Nn = x<x→⊥ Nn

S≤0→⊥ : ∀ {n} → N n → ¬ (succ₁ n ≤ zero)
S≤0→⊥ nzero S0≤0 = t≢f (trans (sym S0≤0) (trans (lt-SS zero zero) lt-00))
S≤0→⊥ (nsucc {n} _) SSn≤0 =
  t≢f (trans (sym SSn≤0) (trans (lt-SS (succ₁ n) zero) (lt-S0 n)))

0≥S→⊥ : ∀ {n} → N n → ¬ (zero ≥ succ₁ n)
0≥S→⊥ Nn 0≥Sn = S≤0→⊥ Nn 0≥Sn

x<y→y<x→⊥ : ∀ {m n} → N m → N n → m < n → ¬ (n < m)
x<y→y<x→⊥ nzero          Nn             0<n   n<0   = ⊥-elim (0>x→⊥ Nn n<0)
x<y→y<x→⊥ (nsucc Nm)     nzero          Sm<0  0<Sm  = ⊥-elim (0>x→⊥ (nsucc Nm) Sm<0)
x<y→y<x→⊥ (nsucc {m} Nm) (nsucc {n} Nn) Sm<Sn Sn<Sm =
  x<y→y<x→⊥ Nm Nn (trans (sym (lt-SS m n)) Sm<Sn) (trans (sym (lt-SS n m)) Sn<Sm)

S≯0→⊥ : ∀ {n} → ¬ (succ₁ n ≯ zero)
S≯0→⊥ {n} h = ⊥-elim (t≢f (trans (sym (lt-0S n)) h))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
data Bool : Set where
  true  : Bool
  false : Bool

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

data ℕ : Set where
  O : ℕ
  S : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
O   + a = a
S a + b = S (a + b)

_*_ : ℕ → ℕ → ℕ
O   * a = O
S a * b = a + (a * b)

_or_ : Bool → Bool → Bool
true  or _ = true
false or b = b

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y

infixl 60 _*_
infixl 40 _+_
infixr 20 _or_
infix  5 if_then_else_

infixr 40 _::_
data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

_∘_ : {A : Set} -> {B : A -> Set} -> {C : (x : A) -> B x -> Set} ->
      (f : {x : A} -> (y : B x) -> C x y) -> (g : (x : A) -> B x) ->
      (x : A) -> C x (g x)
_∘_ f g a = f (g a)

plus-two = S ∘ S

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

_++_ : {A : Set} -> List A -> List A -> List A
[]      ++ ys = ys
x :: xs ++ ys = x :: (xs ++ ys)

data Vec (A : Set) : ℕ -> Set where
  nil  : Vec A O
  cons : (n : ℕ) -> A -> Vec A n -> Vec A (S n)

head : {A : Set} {n : ℕ} -> Vec A (S n) -> A
head (cons n v vs) = v

vmap : {A B : Set} (n : ℕ) -> (A -> B) -> Vec A n -> Vec B n
vmap .O f nil = nil
vmap .(S n) f (cons n x xs) = cons n (f x) (vmap n f xs)

vmap′ : {A B : Set} (n : ℕ) -> (A -> B) -> Vec A n -> Vec B n
vmap′ O f nil = nil
vmap′ (S n) f (cons .n x xs) = cons n (f x) (vmap n f xs)

data Fin : ℕ -> Set where
  fzero : {n : ℕ} -> Fin (S n)
  fsuc  : {n : ℕ} -> Fin n -> Fin (S n)

_!_ : {n : ℕ}{A : Set} -> Vec A n -> Fin n -> A
nil ! ()
cons n x a ! fzero = x
cons n x a ! fsuc b = a ! b

tabulate : {n : ℕ}{A : Set} -> (Fin n -> A) -> Vec A n
tabulate {O} f = nil
tabulate {S n} f = cons n (f fzero) (tabulate (f ∘ fsuc))

data   False : Set where
record True  : Set where

trivial : True
trivial = _

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False

_<_ : ℕ -> ℕ -> Bool
_   < O   = false
O   < S n = true
S m < S n = m < n

length : {A : Set} -> List A -> ℕ
length [] = O
length (x :: xs) = S (length xs)

lookup : {A : Set}(xs : List A)(n : ℕ) -> isTrue (n < length xs) -> A
lookup (x :: xs) O b = x
lookup (x :: xs) (S n) b = lookup xs n b
lookup [] a ()

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

data _≤_ : ℕ -> ℕ -> Set where
  ≤O : {m n : ℕ} -> m == n -> m ≤ n
  ≤I : {m n : ℕ} -> m ≤  n -> m ≤ S n

leq-trans : {l m n : ℕ} -> l ≤ m -> m ≤ n -> l ≤ n
leq-trans a (≤O refl) = a
leq-trans a (≤I b)    = ≤I (leq-trans a b)

min : ℕ -> ℕ -> ℕ
min a b with a < b
min a b | true  = a
min a b | false = b

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter f [] = []
filter f (x :: xs) with f x
... | true  = x :: filter f xs
... | false =      filter f xs

data _≠_ : ℕ -> ℕ -> Set where
  z≠s : {n : ℕ}   -> O   ≠ S n
  s≠z : {n : ℕ}   -> S n ≠ O
  s≠s : {m n : ℕ} -> n   ≠ m → S n ≠ S m

data Equal? (n m : ℕ) : Set where
  eq  : n == m -> Equal? n m
  neq : n ≠  m -> Equal? n m

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
{- formatted printing like printf, except type-safe (as proposed
   in "Cayenne -- a language with dependent types" by Augustsson).

   The types of the rest of the arguments are computed from the
   format string.  -}
module string-format where

open import char
open import eq
open import list
open import nat

open import nat-to-string
open import string

{- We will first convert the format string to the following type,
   so we can avoid default cases in the definition of format-th
   (cf. string-format-issue.agda). -}
data format-d : Set where
  format-nat : format-d → format-d
  format-string : format-d → format-d
  not-format : (c : char) → format-d → format-d
  empty-format : format-d

format-cover : 𝕃 char → format-d
format-cover ('%' :: 'n' :: s) = format-nat (format-cover s)
format-cover ('%' :: 's' :: s) = format-string (format-cover s)
format-cover (c :: s) = not-format c (format-cover s)
format-cover [] = empty-format

format-th : format-d → Set
format-th (format-nat v) = ℕ → format-th v
format-th (format-string v) = string → format-th v
format-th (not-format c v) = format-th v
format-th empty-format = string

format-t : string → Set
format-t s = format-th (format-cover (string-to-𝕃char s))

format-h : 𝕃 char → (d : format-d) → format-th d
format-h s (format-nat v) = λ n → format-h (s ++ (string-to-𝕃char (ℕ-to-string n))) v
format-h s (format-string v) = λ s' → format-h (s ++ (string-to-𝕃char s')) v
format-h s (not-format c v) = format-h (s ++ [ c ] ) v
format-h s empty-format = 𝕃char-to-string s

format : (f : string) → format-t f
format f = format-h [] (format-cover (string-to-𝕃char f))

format-type-test : Set
format-type-test = format-t "%n% of the %ss are in the %s %s"

format-test : string
format-test = format "%n% of the %ss are in the %s %s" 25 "dog" "toasty" "doghouse"

format-test-lem : format-test ≡ "25% of the dogs are in the toasty doghouse"
format-test-lem = refl

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
-- Andreas, 2016-02-01, reported on 2014-12-08

module Issue1388 where

  indented = Set

not-indented = Set  -- This should be a parse error.


text:
module Languages.ILL.AgdaInterface where

open import nat

open import Utils.HaskellTypes
open import Utils.HaskellFunctions
open import Utils.Exception
open import Languages.ILL.Intermediate
open import Languages.ILL.Syntax
open import Languages.ILL.TypeSyntax
open import Languages.ILL.TypeCheck

{-# TERMINATING #-}
translate : ITerm → Either Exception Term
translate Triv = right Triv
translate (Var x) = right (FVar x)
translate (TTensor t₁ t₂) =
   (translate t₁)
     >>=E (λ e₁ → (translate t₂)
       >>=E (λ e₂ → right (Tensor e₁ e₂)))
translate (Lam x a t) =
  (translate t)
    >>=E (λ e → right (Lam x a (close-t 0 x BV x e)))
translate (Let t₁ a PTriv t₂) =
  (translate t₁)
    >>=E (λ e₁ → (translate t₂)
      >>=E (λ e₂ → right (Let e₁ a PTriv e₂)))
translate (Let t₁ a (PTensor (PVar x) (PVar y)) t₂) =
  (translate t₁)
    >>=E (λ e₁ → (translate t₂)
      >>=E (λ e₂ → right (Let e₁ a (PTensor x y) (close-t 0 x LLPV x (close-t 0 y RLPV y e₂)))))
translate (Let _ _ _ _) = error IllformedLetPattern
translate (App t₁ t₂) =
  (translate t₁)
    >>=E (λ e₁ → (translate t₂)
      >>=E (λ e₂ → right (App e₁ e₂)))
translate (Promote ts t) =
   tts >>=E
   (λ ttts → (translate t) >>=E
     (λ tt → right (Promote ttts (foldr aux tt ts)) ))
 where
   tts = commExpList (map (λ x → commExpTriple (fstMapT translate x)) ts)
   aux = (λ (x : Triple ITerm String Type) (v : Term) → close-t 0 (sndT x) PBV (sndT x) v)
translate (Copy t₁ x y t₂) =
  (translate t₁) >>=E
    (λ tt₁ → (translate t₂) >>=E
      (λ tt₂ → right (Copy tt₁ (x , y) (close-t 0 x LCPV x (close-t 0 y RCPV y tt₂)))))
translate (Discard t₁ t₂) =
  (translate t₁) >>=E
    (λ tt₁ → translate t₂ >>=E
      (λ tt₂ → right (Discard tt₁ tt₂)))
translate (Derelict t) =
  (translate t) >>=E (λ tt → right (Derelict tt))

{-# TERMINATING #-}
untranslate : Term → ITerm
untranslate Triv = Triv
untranslate (FVar x) = Var x
untranslate (BVar _ x _) = Var x
untranslate (Let t₁ a PTriv t₂) = Let (untranslate t₁) a PTriv (untranslate t₂)
untranslate (Let t₁ a (PTensor xs ys) t₂) = Let (untranslate t₁) a (PTensor (PVar xs) (PVar ys)) (untranslate t₂)
untranslate (Lam x a t) = Lam x a (untranslate t)
untranslate (App t₁ t₂) = App (untranslate t₁) (untranslate t₂)
untranslate (Tensor t₁ t₂) = TTensor (untranslate t₁) (untranslate t₂)
untranslate (Promote ts t) = Promote uts (untranslate t)
  where
   uts = map (fstMapT untranslate) ts
untranslate (Copy t₁ p t₂) = Copy (untranslate t₁) (fst p) (snd p) (untranslate t₂)
untranslate (Discard t₁ t₂) = Discard (untranslate t₁) (untranslate t₂)
untranslate (Derelict t) = Derelict (untranslate t)

runTypeCheck : ITerm → Either Exception Type
runTypeCheck it = (translate it) >>=E (λ t → typeCheck t)
{-# COMPILED_EXPORT runTypeCheck runTypeCheck #-}

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts

open import binders-disjoint-checks
open import exchange
open import lemmas-consistency
open import lemmas-disjointness
open import lemmas-subst-ta
open import type-assignment-unicity
open import weakening

module preservation where
  -- if d and d' both result from filling the hole in ε with terms of the
  -- same type, they too have the same type.
  wt-different-fill : ∀{Δ Γ d ε d1 d2 d' τ τ1} →
                      d == ε ⟦ d1 ⟧ →
                      Δ , Γ ⊢ d :: τ →
                      Δ , Γ ⊢ d1 :: τ1 →
                      Δ , Γ ⊢ d2 :: τ1 →
                      d' == ε ⟦ d2 ⟧ →
                      Δ , Γ ⊢ d' :: τ
  wt-different-fill FHOuter D1 D2 D3 FHOuter
    with type-assignment-unicity D1 D2
  ... | refl = D3
  wt-different-fill (FHPlus1 eps1) (TAPlus D1 D2) D3 D4 (FHPlus1 eps2) = TAPlus (wt-different-fill eps1 D1 D3 D4 eps2) D2
  wt-different-fill (FHPlus2 eps1) (TAPlus D1 D2) D3 D4 (FHPlus2 eps2) = TAPlus D1 (wt-different-fill eps1 D2 D3 D4 eps2)
  wt-different-fill (FHAp1 eps) (TAAp D1 D2) D3 D4 (FHAp1 D5) = TAAp (wt-different-fill eps D1 D3 D4 D5) D2
  wt-different-fill (FHAp2 eps) (TAAp D1 D2) D3 D4 (FHAp2 D5) = TAAp D1 (wt-different-fill eps D2 D3 D4 D5)
  wt-different-fill (FHInl eps1) (TAInl D) D1 D2 (FHInl eps2) = TAInl (wt-different-fill eps1 D D1 D2 eps2)
  wt-different-fill (FHInr eps1) (TAInr D) D1 D2 (FHInr eps2) = TAInr (wt-different-fill eps1 D D1 D2 eps2)
  wt-different-fill (FHCase eps1) (TACase D x D₁ x₁ D₂) D1 D2 (FHCase eps2) = TACase (wt-different-fill eps1 D D1 D2 eps2) x D₁ x₁ D₂
  wt-different-fill (FHPair1 eps1) (TAPair D D₁) D1 D2 (FHPair1 eps2) = TAPair (wt-different-fill eps1 D D1 D2 eps2) D₁
  wt-different-fill (FHPair2 eps1) (TAPair D D₁) D1 D2 (FHPair2 eps2) = TAPair D (wt-different-fill eps1 D₁ D1 D2 eps2)
  wt-different-fill (FHFst eps1) (TAFst D) D1 D2 (FHFst eps2) = TAFst (wt-different-fill eps1 D D1 D2 eps2)
  wt-different-fill (FHSnd eps1) (TASnd D) D1 D2 (FHSnd eps2) = TASnd (wt-different-fill eps1 D D1 D2 eps2)
  wt-different-fill (FHNEHole eps) (TANEHole x D1 x₁) D2 D3 (FHNEHole D4) = TANEHole x (wt-different-fill eps D1 D2 D3 D4) x₁
  wt-different-fill (FHCast eps) (TACast D1 x) D2 D3 (FHCast D4) = TACast (wt-different-fill eps D1 D2 D3 D4) x
  wt-different-fill (FHFailedCast x) (TAFailedCast y x₁ x₂ x₃) D3 D4 (FHFailedCast eps) = TAFailedCast (wt-different-fill x y D3 D4 eps) x₁ x₂ x₃

  -- if a well typed term results from filling the hole in ε, then the term
  -- that filled the hole is also well typed
  wt-filling : ∀{ε Δ Γ d τ d'} →
               Δ , Γ ⊢ d :: τ →
               d == ε ⟦ d' ⟧ →
               Σ[ τ' ∈ htyp ] (Δ , Γ ⊢ d' :: τ')
  wt-filling TANum FHOuter = _ , TANum
  wt-filling (TAPlus ta ta₁) FHOuter = num , TAPlus ta ta₁
  wt-filling (TAPlus ta ta₁) (FHPlus1 eps) = wt-filling ta eps
  wt-filling (TAPlus ta ta₁) (FHPlus2 eps) = wt-filling ta₁ eps
  wt-filling (TAVar x₁) FHOuter = _ , TAVar x₁
  wt-filling (TALam f ta) FHOuter = _ , TALam f ta
  wt-filling (TAAp ta ta₁) FHOuter = _ , TAAp ta ta₁
  wt-filling (TAAp ta ta₁) (FHAp1 eps) = wt-filling ta eps
  wt-filling (TAAp ta ta₁) (FHAp2 eps) = wt-filling ta₁ eps
  wt-filling (TAInl ta) FHOuter = _ , TAInl ta
  wt-filling (TAInl ta) (FHInl eps) = wt-filling ta eps
  wt-filling (TAInr ta) FHOuter = _ , TAInr ta
  wt-filling (TAInr ta) (FHInr eps) = wt-filling ta eps
  wt-filling (TACase ta x ta₁ x₁ ta₂) FHOuter = _ , TACase ta x ta₁ x₁ ta₂
  wt-filling (TACase ta x ta₁ x₁ ta₂) (FHCase eps) = wt-filling ta eps
  wt-filling (TAPair ta ta₁) FHOuter = _ , TAPair ta ta₁
  wt-filling (TAPair ta ta₁) (FHPair1 eps) = wt-filling ta eps
  wt-filling (TAPair ta ta₁) (FHPair2 eps) = wt-filling ta₁ eps
  wt-filling (TAFst ta) FHOuter = _ , TAFst ta
  wt-filling (TAFst ta) (FHFst eps) = wt-filling ta eps
  wt-filling (TASnd ta) FHOuter = _ , TASnd ta
  wt-filling (TASnd ta) (FHSnd eps) = wt-filling ta eps
  wt-filling (TAEHole x x₁) FHOuter = _ , TAEHole x x₁
  wt-filling (TANEHole x ta x₁) FHOuter = _ , TANEHole x ta x₁
  wt-filling (TANEHole x ta x₁) (FHNEHole eps) = wt-filling ta eps
  wt-filling (TACast ta x) FHOuter = _ , TACast ta x
  wt-filling (TACast ta x) (FHCast eps) = wt-filling ta eps
  wt-filling (TAFailedCast x y z w) FHOuter = _ , TAFailedCast x y z w
  wt-filling (TAFailedCast x x₁ x₂ x₃) (FHFailedCast y) = wt-filling x y

  -- instruction transitions preserve type
  preserve-trans : ∀{Δ Γ d τ d'} →
                   binders-unique d →
                   Δ , Γ ⊢ d :: τ →
                   d →> d' →
                   Δ , Γ ⊢ d' :: τ
  preserve-trans bd TANum ()
  preserve-trans bd (TAPlus ta TANum) (ITPlus x) = TANum
  preserve-trans bd (TAVar x₁) ()
  preserve-trans bd (TALam _ ta) ()
  preserve-trans (BUAp (BULam bd x₁) bd₁ (BDLam x₂ x₃)) (TAAp (TALam apt ta) ta₁) ITLam = lem-subst apt x₂ bd₁ ta ta₁
  preserve-trans bd (TAAp (TACast ta TCRefl) ta₁) ITApCast = TACast (TAAp ta (TACast ta₁ TCRefl)) TCRefl
  preserve-trans bd (TAAp (TACast ta (TCArr x x₁)) ta₁) ITApCast = TACast (TAAp ta (TACast ta₁ (~sym x))) x₁
  preserve-trans bd (TAEHole x x₁) ()
  preserve-trans bd (TANEHole x ta x₁) ()
  preserve-trans bd (TACast ta x) (ITCastID) = ta
  preserve-trans bd (TACast (TACast ta x) x₁) (ITCastSucceed x₂) = ta
  preserve-trans bd (TACast ta x) (ITGround (MGArr x₁)) = TACast (TACast ta (TCArr TCHole1 TCHole1)) TCHole1
  preserve-trans bd (TACast ta TCHole2) (ITExpand (MGArr x₁)) = TACast (TACast ta TCHole2) (TCArr TCHole2 TCHole2)
  preserve-trans bd (TACast (TACast ta x) x₁) (ITCastFail w y z) = TAFailedCast ta w y z
  preserve-trans bd (TAFailedCast x y z q) ()
  preserve-trans bd (TAInl ta) ()
  preserve-trans bd (TAInr ta) ()
  preserve-trans (BUCase (BUInl bd) bd₁ bd₂ (BDInl x₂) x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) (TACase (TAInl ta) x ta₁ x₁ ta₂) ITCaseInl = lem-subst x (binders-disjoint-sym x₂) bd ta₁ ta
  preserve-trans (BUCase (BUInr bd) bd₁ bd₂ (BDInr x₂) (BDInr x₃) x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) (TACase (TAInr ta) x ta₁ x₁ ta₂) ITCaseInr = lem-subst x₁ (binders-disjoint-sym x₃) bd ta₂ ta
  preserve-trans (BUCase (BUCast bd) bd₁ bd₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁) (TACase {Γ = Γ} (TACast ta x₂) x ta₁ x₁ ta₂) ITCaseCast
    with ~sum x₂
  ... | τ1~τ2 , τ3~τ4 = TACase ta x (lem-subst-cast-ta {Γ = Γ} x bd₁ τ1~τ2 ta₁) x₁ (lem-subst-cast-ta {Γ = Γ} x₁ bd₂ τ3~τ4 ta₂)
  preserve-trans bd (TAPair ta ta₁) ()
  preserve-trans bd (TAFst (TAPair ta ta₁)) ITFstPair = ta
  preserve-trans bd (TAFst (TACast ta x)) ITFstCast
    with ~prod x
  ... | τ1~τ2 , τ3~τ4 = TACast (TAFst ta) τ1~τ2
  preserve-trans bd (TASnd (TAPair ta ta₁)) ITSndPair = ta₁
  preserve-trans bd (TASnd (TACast ta x)) ITSndCast
    with ~prod x
  ... | τ1~τ2 , τ3~τ4 = TACast (TASnd ta) τ3~τ4
  preserve-trans bd (TACast ta TCRefl) (ITExpand ())
  preserve-trans bd (TACast ta TCHole1) (ITGround (MGSum x₁)) = TACast (TACast ta (TCSum TCHole1 TCHole1)) TCHole1
  preserve-trans bd (TACast ta TCHole1) (ITExpand ())
  preserve-trans bd (TACast ta TCHole2) (ITExpand (MGSum x₁)) = TACast (TACast ta TCHole2) (TCSum TCHole2 TCHole2)
  preserve-trans bd (TACast ta TCHole1) (ITGround (MGProd x₁)) = TACast (TACast ta (TCProd TCHole1 TCHole1)) TCHole1
  preserve-trans bd (TACast ta TCHole2) (ITExpand (MGProd x)) = TACast (TACast ta TCHole2) (TCProd TCHole2 TCHole2)

  lem-bd-ε1 : ∀{d ε d0} → d == ε ⟦ d0 ⟧ →
              binders-unique d →
              binders-unique d0
  lem-bd-ε1 FHOuter bd = bd
  lem-bd-ε1 (FHPlus1 eps) (BUPlus bd bd₁ x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHPlus2 eps) (BUPlus bd bd₁ x) = lem-bd-ε1 eps bd₁
  lem-bd-ε1 (FHAp1 eps) (BUAp bd bd₁ x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHAp2 eps) (BUAp bd bd₁ x) = lem-bd-ε1 eps bd₁
  lem-bd-ε1 (FHInl eps) (BUInl bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHInr eps) (BUInr bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHCase eps) (BUCase bd bd₁ bd₂ x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHPair1 eps) (BUPair bd bd₁ x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHPair2 eps) (BUPair bd bd₁ x) = lem-bd-ε1 eps bd₁
  lem-bd-ε1 (FHFst eps) (BUFst bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHSnd eps) (BUSnd bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHNEHole eps) (BUNEHole bd x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHCast eps) (BUCast bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHFailedCast eps) (BUFailedCast bd) = lem-bd-ε1 eps bd

  -- this is the main preservation theorem, gluing together the above
  preservation : {Δ : hctx} {d d' : ihexp} {τ : htyp} {Γ : tctx} →
                 binders-unique d →
                 Δ , Γ ⊢ d :: τ →
                 d ↦ d' →
                 Δ , Γ ⊢ d' :: τ
  preservation bd D (Step x x₁ x₂)
    with wt-filling D x
  ... | (_ , wt) = wt-different-fill x D wt (preserve-trans (lem-bd-ε1 x bd) wt x₁) x₂

  -- note that the exact statement of preservation in the paper, where Γ is
  -- empty indicating that the terms are closed, is an immediate corrolary
  -- of the slightly more general statement above.
  preservation' : {Δ : hctx} {d d' : ihexp} {τ : htyp} →
                  binders-unique d →
                  Δ , ∅ ⊢ d :: τ →
                  d ↦ d' →
                  Δ , ∅ ⊢ d' :: τ
  preservation' = preservation

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

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

module FOTC.Data.Nat.Divisibility.NotBy0 where

open import FOTC.Base
open import FOTC.Data.Nat

infix 4 _∣_

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

-- Note that @k@ should be a total natural number.
_∣_ : D → D → Set
m ∣ n =  (m ≢ zero) ∧ (∃[ k ] N k ∧ n ≡ k * m)
{-# ATP definition _∣_ #-}


text:
module Relation.Ternary.Separation.Monad where

open import Level
open import Data.Product
open import Function using (_∘_; case_of_)
open import Relation.Unary
open import Relation.Unary.PredicateTransformer hiding (_⊔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Morphisms

module Monads
  {a b} {A : Set a}  {B : Set b} {{r}} {u}
  {{as : IsUnitalSep {C = A} r u}}
  {{rb : RawSep B}}
  {{jm : Morphism A B}}
  {{bs : IsUnitalSep rb (Morphism.j jm u)}}
  where

  open Morphism jm

  RawMonad : ∀ {i} (I : Set i) → (ℓ : Level) → Set _
  RawMonad I ℓ = (i j : I) → PT A B ℓ ℓ

  {- strong indexed monads on predicates over PRSAs, relative to the functor induced by the PRSA morphism j -}
  record Monad {i} (I : Set i) ℓ (M : RawMonad I ℓ) : Set (a ⊔ b ⊔ suc ℓ ⊔ i) where
    field
      return : ∀ {P i₁}         → ∀[ P ⇒ⱼ M i₁ i₁ P ]
      bind   : ∀ {P i₁ i₂ i₃ Q} → ∀[ (P ─✴ⱼ M i₂ i₃ Q) ⇒ (M i₁ i₂ P ─✴ M i₁ i₃ Q) ]

    _=<<_ : ∀ {P Q i₁ i₂ i₃} → ∀[ P ⇒ⱼ M i₂ i₃ Q ] → ∀[ M i₁ i₂ P ⇒ M i₁ i₃ Q ]
    f =<< mp = app (bind (wand λ where px σ → case ⊎-id⁻ˡ σ of λ where refl → f px)) mp ⊎-idˡ

    _>>=_ : ∀ {Φ} {P Q i₁ i₂ i₃} → M i₁ i₂ P Φ → ∀[ P ⇒ⱼ M i₂ i₃ Q ] → M i₁ i₃ Q Φ
    mp >>= f = f =<< mp

    mapM′ : ∀ {P Q i₁ i₂} → ∀[ (P ─✴ Q) ⇒ⱼ (M i₁ i₂ P ─✴ M i₁ i₂ Q) ]
    mapM′ f = bind (wand λ where
      px σ →
         case j-⊎⁻ σ of λ where
           (_ , refl , σ') → return (app f px σ'))

    mapM : ∀ {Φ} {P Q i₁ i₂} → M i₁ i₂ P Φ → ∀[ P ⇒ Q ] → M i₁ i₂ Q Φ
    mapM mp f = mp >>= (return ∘ f)

  open Monad ⦃...⦄ public

  -- having the internal bind is enough to get strength
  module _ {i} {I : Set i} {i₁ i₂} {P} {M} {{ _ : Monad I a M }} where
    str  : ∀ {Q : Pred A a} → M i₁ i₂ P Φ₁ → Φ₁ ⊎ j Φ₂ ≣ Φ → Q Φ₂ → M i₁ i₂ (P ✴ Q) Φ
    str mp σ qx = app (bind (wand λ where
      px σ' → case j-⊎⁻ σ' of λ where
        (_ , refl , σ'') → return (px ×⟨ ⊎-comm σ'' ⟩ qx))
      ) mp (⊎-comm σ)

    typed-str : ∀ {Φ₁ Φ₂ Φ} (Q) → M i₁ i₂ P Φ₁ → Φ₁ ⊎ j Φ₂ ≣ Φ → Q Φ₂ → M i₁ i₂ (P ✴ Q) Φ
    typed-str Q mp σ qx = str {Q = Q} mp σ qx

    syntax str mp σ qx = mp &⟨ σ ⟩ qx
    syntax typed-str Q mp σ qx = mp &⟨ Q ∥ σ ⟩ qx

    _&_ : ∀ {Q} → M i₁ i₂ P ε → ∀[ Q ⇒ⱼ M i₁ i₂ (P ✴ Q) ]
    mp & q = mp &⟨ ⊎-idˡ ⟩ q


text:
{-# OPTIONS --cumulativity #-}

open import Agda.Builtin.Equality

mutual

  _X : (Set → Set) → Set₁ → Set
  _X f x = _

  test : (f : Set₁ → Set) (x : Set₁) → _X f x ≡ f x
  test f x = refl

Set' : Set
Set' = _X (λ X → X) Set

max_forks_repo_name: shlevy/agda