text:
module Data.QuadTree.Implementation.DataLenses where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.Implementation.PropDepthRelation
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic

import Data.QuadTree.Implementation.Definition
import Data.QuadTree.Implementation.ValidTypes
import Data.QuadTree.Implementation.QuadrantLenses
#-}

---- Functions for whether a coordinate is inside

isInsideQuadTree : {t : Set} -> (Nat × Nat) -> QuadTree t -> Bool
isInsideQuadTree (x , y) (Wrapper (w , h) _) = x < w && y < h

isInsidePow : (Nat × Nat) -> Nat -> Bool
isInsidePow (x , y) deps = x < pow 2 deps && y < pow 2 deps

insideQTtoInsidePow : {t : Set} {{eqT : Eq t}} -> (loc : Nat × Nat) -> {dep : Nat} -> (vqt : VQuadTree t {dep})
  -> IsTrue (isInsideQuadTree loc (qtFromSafe vqt))
  -> IsTrue (isInsidePow loc dep)
insideQTtoInsidePow (x , y) {dep} (CVQuadTree (Wrapper (w , h) qd) {p} {q}) it =
  let
    p1 : IsTrue (pow 2 dep >= (max w h))
    p1 = log2upPow dep (max w h) (eqToGte dep (log2up (max w h)) q)

    p2 : IsTrue ((max w h) <= pow 2 dep)
    p2 = gteInvert (pow 2 dep) (max w h) p1

    p3 : IsTrue (w <= pow 2 dep && h <= pow 2 dep)
    p3 = useEq (sym $ propMaxLte w h (pow 2 dep)) p2
  in andCombine
    ( ltLteTransitive x w (pow 2 dep) (andFst {x < w} it) (andFst p3) )
    ( ltLteTransitive y h (pow 2 dep) (andSnd {x < w} it) (andSnd p3) )

---- Data access

-- Lens into the leaf quadrant corresponding to a location in a quadrant
go : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> (dep : Nat)
  -> {.(IsTrue (isInsidePow loc dep))}
  -> Lens (VQuadrant t {dep}) t
go _ Z = lensLeaf
go {t} (x , y) (S deps) =
  let
    mid = pow 2 deps
    gorec = go {t} (mod x mid {pow_not_zero_cv deps} , mod y mid {pow_not_zero_cv deps}) deps
      {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}
  in
    if (y < mid)
      then if x < mid
        then (lensA ∘ gorec)
        else (lensB ∘ gorec)
      else if x < mid
        then (lensC ∘ gorec)
        else (lensD ∘ gorec)
{-# COMPILE AGDA2HS go #-}

-- Lenses into the root quadrant of a quadtree
lensWrappedTree : {t : Set} {{eqT : Eq t}}
  -> {dep : Nat}
  -> Lens (VQuadTree t {dep}) (VQuadrant t {dep})
lensWrappedTree fun (CVQuadTree (Wrapper (w , h) qd) {p} {q}) =
  fmap
    (λ where (CVQuadrant qd {p}) → CVQuadTree (Wrapper (w , h) qd) {p} {q})
    (fun (CVQuadrant qd {p}))
{-# COMPILE AGDA2HS lensWrappedTree #-}

-- Lens into the leaf quadrant corresponding to a location in a quadtree
atLocation : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> (dep : Nat)
  -> {.(IsTrue (isInsidePow loc dep))}
  -> Lens (VQuadTree t {dep}) t
atLocation index dep {p} = lensWrappedTree ∘ (go index dep {p})
{-# COMPILE AGDA2HS atLocation #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Unit.Base where
open import Cubical.Foundations.Prelude

-- Obtain Unit
open import Agda.Builtin.Unit public
  renaming ( ⊤ to Unit )

-- Universe polymorphic version
Unit* : {ℓ : Level} → Type ℓ
Unit* = Lift Unit

pattern tt* = lift tt

-- Universe polymorphic version without definitional equality
-- Allows us to "lock" proofs. See "Locking, unlocking" in
-- https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html
data lockUnit {ℓ} : Type ℓ where
  unlock : lockUnit

ext: agda

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:
{-# OPTIONS --without-K #-}

module PiLevel0 where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong₂; module ≡-Reasoning)
--  using (_≡_; refl; sym; trans; cong₂; proof-irrelevance; module ≡-Reasoning)
--open import Data.Nat.Properties.Simple
--  using (+-right-identity; +-suc; +-assoc; +-comm;
--        *-assoc; *-comm; *-right-zero; distribʳ-*-+)

--open import Data.Bool using (Bool; false; true; _∧_; _∨_)
open import Data.Nat using (ℕ) -- ; _+_; _*_)

--open import Data.Vec
--  using (Vec; []; _∷_)
-- renaming (_++_ to _++V_; map to mapV; concat to concatV)

--open import Data.Empty   using (⊥; ⊥-elim)
--open import Data.Unit    using (⊤; tt)
--open import Data.Sum     using (_⊎_; inj₁; inj₂)
--open import Data.Product using (_×_; _,_; proj₁; proj₂)

--open import Proofs using (
  -- FinNatLemmas
--     distribˡ-*-+; *-right-identity
--  )

open import PiU using (U; ZERO; ONE; PLUS; TIMES; toℕ)

------------------------------------------------------------------------------
-- Level 0 of Pi
--
{--

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

-- Abbreviations for examples

BOOL : U
BOOL  = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

-- false⟷ true⟷ : ⟦ BOOL ⟧
-- false⟷ = inj₁ tt
-- true⟷  = inj₂ tt

-- For any finite type (t : U) there is no non-trivial path structure
-- between the elements of t. All such finite types are discrete
-- groupoids
--
-- For U, there are non-trivial paths between its points. In the
-- conventional HoTT presentation, a path between t₁ and t₂ is
-- postulated by univalence for each equivalence between t₁ and t₂. In
-- the context of finite types, an equivalence corresponds to a
-- permutation as each permutation has a unique inverse
-- permutation. Thus instead of the detour using univalence, we can
-- give an inductive definition of all possible permutations between
-- finite types which naturally induces paths between the points of U,
-- i.e., the finite types. More precisely, two types t₁ and t₂ have a
-- path between them if there is a permutation (c : t₁ ⟷ t₂). The fact
-- that c is a permutation guarantees, by construction, that (c ◎ ! c
-- ∼ id⟷) and (! c ◎ c ∼ id⟷). A complete set of generators for all
-- possible permutations between finite types is given by the
-- following definition. Note that these permutations do not reach
-- inside the types and hence do not generate paths between the points
-- within the types. The paths are just between the types themselves.

--}

size : U → ℕ
size = toℕ

infix  30 _⟷_
infixr 50 _◎_

-- Combinators, permutations, or paths depending on the perspective

data _⟷_ : U → U → Set where
  unite₊l : {t : U} → PLUS ZERO t ⟷ t
  uniti₊l : {t : U} → t ⟷ PLUS ZERO t
  unite₊r : {t : U} → PLUS t ZERO ⟷ t
  uniti₊r : {t : U} → t ⟷ PLUS t ZERO
  swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
  assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
  assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
  unite⋆l  : {t : U} → TIMES ONE t ⟷ t
  uniti⋆l  : {t : U} → t ⟷ TIMES ONE t
  unite⋆r : {t : U} → TIMES t ONE ⟷ t
  uniti⋆r : {t : U} → t ⟷ TIMES t ONE
  swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
  assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
  assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
  absorbr : {t : U} → TIMES ZERO t ⟷ ZERO
  absorbl : {t : U} → TIMES t ZERO ⟷ ZERO
  factorzr : {t : U} → ZERO ⟷ TIMES t ZERO
  factorzl : {t : U} → ZERO ⟷ TIMES ZERO t
  dist    : {t₁ t₂ t₃ : U} →
            TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
  factor  : {t₁ t₂ t₃ : U} →
            PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
  distl   : {t₁ t₂ t₃ : U } →
            TIMES t₁ (PLUS t₂ t₃) ⟷ PLUS (TIMES t₁ t₂) (TIMES t₁ t₃)
  factorl : {t₁ t₂ t₃ : U } →
            PLUS (TIMES t₁ t₂) (TIMES t₁ t₃) ⟷ TIMES t₁ (PLUS t₂ t₃)
  id⟷    : {t : U} → t ⟷ t
  _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)

{--

-- Syntactic equality of combinators

comb= : {t₁ t₂ t₃ t₄ : U} → (t₁ ⟷ t₂) → (t₃ ⟷ t₄) → Bool
comb= unite₊l unite₊l = true
comb= uniti₊l uniti₊l = true
comb= swap₊ swap₊ = true
comb= assocl₊ assocl₊ = true
comb= assocr₊ assocr₊ = true
comb= unite⋆l unite⋆l = true
comb= unite⋆r unite⋆r = true
comb= uniti⋆l uniti⋆l = true
comb= uniti⋆r uniti⋆r = true
comb= swap⋆ swap⋆ = true
comb= assocl⋆ assocl⋆ = true
comb= assocr⋆ assocr⋆ = true
comb= absorbl absorbl = true
comb= absorbr absorbr = true
comb= factorzl factorzl = true
comb= factorzr factorzr = true
comb= dist dist = true
comb= factor factor = true
comb= id⟷ id⟷ = true
comb= (c₁ ◎ c₂) (c₃ ◎ c₄) = comb= c₁ c₃ ∧ comb= c₂ c₄
comb= (c₁ ⊕ c₂) (c₃ ⊕ c₄) = comb= c₁ c₃ ∧ comb= c₂ c₄
comb= (c₁ ⊗ c₂) (c₃ ⊗ c₄) = comb= c₁ c₃ ∧ comb= c₂ c₄
comb= _ _ = false

-- Extensional evaluator for testing: serves as a specification

-- A canonical representation of each type as a vector of values. This
-- fixes a canonical order for the elements of the types: each value
-- has a canonical index.

utoVec : (t : U) → Vec ⟦ t ⟧ (size t)
utoVec ZERO          = []
utoVec ONE           = tt ∷ []
utoVec (PLUS t₁ t₂)  = mapV inj₁ (utoVec t₁) ++V mapV inj₂ (utoVec t₂)
utoVec (TIMES t₁ t₂) =
  concatV (mapV (λ v₁ → mapV (λ v₂ → (v₁ , v₂)) (utoVec t₂)) (utoVec t₁))

-- Combinators are always between types of the same size
-- Paths preserve sizes

size≡ : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (size t₁ ≡ size t₂)
-- the composition case must be the first one
-- otherwise Agda will not unfold (c ◎ id⟷)
-- See "inconclusive matching" at
-- http://wiki.portal.chalmers.se/agda/
-- pmwiki.php?n=ReferenceManual.PatternMatching
size≡ (c₁ ◎ c₂) = trans (size≡ c₁) (size≡ c₂)
size≡ {PLUS ZERO t} {.t} unite₊l = refl
size≡ {t} {PLUS ZERO .t} uniti₊l = refl
size≡ {PLUS t ZERO} unite₊r = +-right-identity (size t)
size≡ {t} uniti₊r = sym (+-right-identity (size t))
size≡ {PLUS t₁ t₂} {PLUS .t₂ .t₁} swap₊ = +-comm (size t₁) (size t₂)
size≡ {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃} assocl₊ =
  sym (+-assoc (size t₁) (size t₂) (size t₃))
size≡ {PLUS (PLUS t₁ t₂) t₃} {PLUS .t₁ (PLUS .t₂ .t₃)} assocr₊ =
  +-assoc (size t₁) (size t₂) (size t₃)
size≡ {TIMES ONE t} {.t} unite⋆l = +-right-identity (size t)
size≡ {t} {TIMES ONE .t} uniti⋆l = sym (+-right-identity (size t))
size≡ {TIMES t ONE} {.t} unite⋆r = *-right-identity (size t)
size≡ {t} {TIMES .t ONE} uniti⋆r = sym (*-right-identity (size t))
size≡ {TIMES t₁ t₂} {TIMES .t₂ .t₁} swap⋆ = *-comm (size t₁) (size t₂)
size≡ {TIMES t₁ (TIMES t₂ t₃)} {TIMES (TIMES .t₁ .t₂) .t₃} assocl⋆ =
  sym (*-assoc (size t₁) (size t₂) (size t₃))
size≡ {TIMES (TIMES t₁ t₂) t₃} {TIMES .t₁ (TIMES .t₂ .t₃)} assocr⋆ =
  *-assoc (size t₁) (size t₂) (size t₃)
size≡ {TIMES .ZERO t} {ZERO} absorbr = refl
size≡ {TIMES t .ZERO} {ZERO} absorbl = *-right-zero (size t)
size≡ {ZERO} {TIMES ZERO t} factorzl = refl
size≡ {ZERO} {TIMES t ZERO} factorzr = sym (*-right-zero (size t))
size≡ {TIMES (PLUS t₁ t₂) t₃} {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)} dist =
  distribʳ-*-+ (size t₃) (size t₁) (size t₂)
size≡ {PLUS (TIMES t₁ t₃) (TIMES t₂ .t₃)} {TIMES (PLUS .t₁ .t₂) .t₃} factor =
  sym (distribʳ-*-+ (size t₃) (size t₁) (size t₂))
size≡ {TIMES t₁ (PLUS t₂ t₃)} distl = distribˡ-*-+ (size t₁) (size t₂) (size t₃)
size≡ {PLUS (TIMES t₁ t₂) (TIMES .t₁ t₃)} factorl =
  sym (distribˡ-*-+ (size t₁) (size t₂) (size t₃))
size≡ {t} {.t} id⟷ = refl
size≡ {PLUS t₁ t₂} {PLUS t₃ t₄} (c₁ ⊕ c₂) = cong₂ _+_ (size≡ c₁) (size≡ c₂)
size≡ {TIMES t₁ t₂} {TIMES t₃ t₄} (c₁ ⊗ c₂) = cong₂ _*_ (size≡ c₁) (size≡ c₂)

-- All proofs about sizes are "the same"

size∼ : {t₁ t₂ : U} → (c₁ c₂ : t₁ ⟷ t₂) → (size≡ c₁ ≡ size≡ c₂)
size∼ c₁ c₂ = proof-irrelevance (size≡ c₁) (size≡ c₂)

------------------------------------------------------------------------------
-- Examples of Pi programs

-- Nicer syntax that shows intermediate values instead of the above
-- point-free notation of permutations

infixr 2  _⟷⟨_⟩_
infix  2  _□

_⟷⟨_⟩_ : (t₁ : U) {t₂ : U} {t₃ : U} →
          (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
_ ⟷⟨ α ⟩ β = α ◎ β

_□ : (t : U) → {t : U} → (t ⟷ t)
_□ t = id⟷

-- calculate and print specification of a combinator

spec : {t₁ t₂ : U} → (t₁ ⟷ t₂) → Vec (⟦ t₁ ⟧ × ⟦ t₂ ⟧) (size t₁)
spec {t₁} {t₂} c = mapV (λ v₁ → (v₁ , eval c v₁)) (utoVec t₁)

-- For easier manipulation of Bool
foldBool unfoldBool : BOOL ⟷ BOOL
foldBool = id⟷
unfoldBool = id⟷

-- Many ways of negating a BOOL. Again, it is absolutely critical that there
-- is NO path between false⟷ and true⟷. These permutations instead are based
-- on paths between x and neg (neg x) which are the trivial paths on each of
-- the two points in BOOL.

NOT : BOOL ⟷ BOOL
NOT = unfoldBool ◎ swap₊ ◎ foldBool
-- spec: (false , true) ∷ (true , false) ∷ []

NEG1 NEG2 NEG3 NEG4 NEG5 : BOOL ⟷ BOOL
NEG1 = unfoldBool ◎ swap₊ ◎ foldBool
-- spec: (false , true) ∷ (true , false) ∷ []
NEG2 = id⟷ ◎ NOT
-- spec: (false , true) ∷ (true , false) ∷ []
NEG3 = NOT ◎ NOT ◎ NOT
-- spec: (false , true) ∷ (true , false) ∷ []
NEG4 = NOT ◎ id⟷
-- spec: (false , true) ∷ (true , false) ∷ []
NEG5 = uniti⋆l ◎ swap⋆ ◎ (NOT ⊗ id⟷) ◎ swap⋆ ◎ unite⋆l
-- spec: (false , true) ∷ (true , false) ∷ []
NEG6 = uniti⋆r ◎ (NOT ⊗ id⟷) ◎ unite⋆r -- same as above, but shorter

-- CNOT

CNOT : BOOL² ⟷ BOOL²
CNOT = TIMES BOOL BOOL
         ⟷⟨ unfoldBool ⊗ id⟷ ⟩
       TIMES (PLUS x y) BOOL
         ⟷⟨ dist ⟩
       PLUS (TIMES x BOOL) (TIMES y BOOL)
         ⟷⟨ id⟷ ⊕ (id⟷ ⊗ NOT) ⟩
       PLUS (TIMES x BOOL) (TIMES y BOOL)
         ⟷⟨ factor ⟩
       TIMES (PLUS x y) BOOL
         ⟷⟨ foldBool ⊗ id⟷ ⟩
       TIMES BOOL BOOL □
  where x = ONE; y = ONE
-- spec:
-- ((false , false) , false , false) ∷
-- ((false , true)  , false , true)  ∷
-- ((true  , false) , true  , true)  ∷
-- ((true  , true)  , true  , false) ∷ []

-- TOFFOLI

TOFFOLI : TIMES BOOL BOOL² ⟷ TIMES BOOL BOOL²
TOFFOLI = TIMES BOOL BOOL²
            ⟷⟨ unfoldBool ⊗ id⟷ ⟩
          TIMES (PLUS x y) BOOL²
            ⟷⟨ dist ⟩
          PLUS (TIMES x BOOL²) (TIMES y BOOL²)
            ⟷⟨ id⟷ ⊕ (id⟷ ⊗ CNOT) ⟩
          PLUS (TIMES x BOOL²) (TIMES y BOOL²)
            ⟷⟨ factor ⟩
          TIMES (PLUS x y) BOOL²
            ⟷⟨ foldBool ⊗ id⟷ ⟩
         TIMES BOOL BOOL² □
  where x = ONE; y = ONE
-- spec:
-- ((false , false , false) , false , false , false) ∷
-- ((false , false , true)  , false , false , true)  ∷
-- ((false , true  , false) , false , true  , false) ∷
-- ((false , true  , true)  , false , true  , true)  ∷
-- ((true  , false , false) , true  , false , false) ∷
-- ((true  , false , true)  , true  , false , true)  ∷
-- ((true  , true  , false) , true  , true  , true)  ∷
-- ((true  , true  , true)  , true  , true  , false) ∷ []

-- Swaps for the type 1+(1+1)
-- We have three values in the type 1+(1+1)
-- Let's call them a, b, and c
-- There 6 permutations. Using the swaps below we can express every permutation:
-- a b c id⟷
-- a c b SWAP23
-- b a c SWAP12
-- b c a ROTL
-- c a b ROTR
-- c b a SWAP13

SWAP12 SWAP23 SWAP13 ROTL ROTR :
  PLUS ONE (PLUS ONE ONE) ⟷ PLUS ONE (PLUS ONE ONE)
SWAP12 = assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊
-- spec:
-- (inj₁ tt        , inj₂ (inj₁ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₁ tt)        ∷
-- (inj₂ (inj₂ tt) , inj₂ (inj₂ tt)) ∷ []
SWAP23 = id⟷ ⊕ swap₊
-- spec:
-- (inj₁ tt        , inj₁ tt)        ∷
-- (inj₂ (inj₁ tt) , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₂ tt) , inj₂ (inj₁ tt)) ∷ []
SWAP13 = SWAP23 ◎ SWAP12 ◎ SWAP23
-- spec:
-- (inj₁ tt        , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₂ (inj₁ tt)) ∷
-- (inj₂ (inj₂ tt) , inj₁ tt)        ∷ []
ROTR   = SWAP12 ◎ SWAP23
-- spec:
-- (inj₁ tt        , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₁ tt)        ∷
-- (inj₂ (inj₂ tt) , inj₂ (inj₁ tt)) ∷ []
ROTL   = SWAP13 ◎ SWAP23
-- spec:
-- (inj₁ tt        , inj₂ (inj₁ tt)) ∷
-- (inj₂ (inj₁ tt) , inj₂ (inj₂ tt)) ∷
-- (inj₂ (inj₂ tt) , inj₁ tt)        ∷ []

-- The Peres gate is a universal gate: it takes three inputs a, b, and c, and
-- produces a, a xor b, (a and b) xor c

PERES : TIMES (TIMES BOOL BOOL) BOOL ⟷ TIMES (TIMES BOOL BOOL) BOOL
PERES = (id⟷ ⊗ NOT) ◎ assocr⋆ ◎ (id⟷ ⊗ swap⋆) ◎
        TOFFOLI ◎
        (id⟷ ⊗ (NOT ⊗ id⟷)) ◎
        TOFFOLI ◎
        (id⟷ ⊗ swap⋆) ◎ (id⟷ ⊗ (NOT ⊗ id⟷)) ◎
        TOFFOLI ◎
        (id⟷ ⊗ (NOT ⊗ id⟷)) ◎ assocl⋆
-- spec:
-- (((false , false) , false) , (false , false) , false) ∷
-- (((false , false) , true)  , (false , false) , true)  ∷
-- (((false , true)  , false) , (false , true)  , false) ∷
-- (((false , true)  , true)  , (false , true)  , true)  ∷
-- (((true  , false) , false) , (true  , true)  , false) ∷
-- (((true  , false) , true)  , (true  , true)  , true)  ∷
-- (((true  , true)  , false) , (true  , false) , true)  ∷
-- (((true  , true)  , true)  , (true  , false) , false) ∷ []

-- A reversible full adder: See http://arxiv.org/pdf/1008.3533.pdf
-- Input: (z, ((n1, n2), cin)))
-- Output (g1, (g2, (sum, cout)))
-- where sum = n1 xor n2 xor cin
-- and cout = ((n1 xor n2) and cin) xor (n1 and n2) xor z
FULLADDER : TIMES BOOL (TIMES (TIMES BOOL BOOL) BOOL) ⟷
            TIMES BOOL (TIMES BOOL (TIMES BOOL BOOL))
FULLADDER =
  -- (z,((n1,n2),cin))
  swap⋆ ◎
  -- (((n1,n2),cin),z)
  (swap⋆ ⊗ id⟷) ◎
  -- ((cin,(n1,n2)),z)
  assocr⋆ ◎
  -- (cin,((n1,n2),z))
  swap⋆ ◎
  -- (((n1,n2),z),cin)
  (PERES ⊗ id⟷) ◎
  -- (((n1,n1 xor n2),(n1 and n2) xor z),cin)
  assocr⋆ ◎
  -- ((n1,n1 xor n2),((n1 and n2) xor z,cin))
  (id⟷ ⊗ swap⋆) ◎
  -- ((n1,n1 xor n2),(cin,(n1 and n2) xor z))
  assocr⋆ ◎
  -- (n1,(n1 xor n2,(cin,(n1 and n2) xor z)))
  (id⟷ ⊗ assocl⋆) ◎
  -- (n1,((n1 xor n2,cin),(n1 and n2) xor z))
  (id⟷ ⊗ PERES) ◎
  -- (n1,((n1 xor n2,n1 xor n2 xor cin),
  --      ((n1 xor n2) and cin) xor (n1 and n2) xor z))
  (id⟷ ⊗ assocr⋆)
  -- (n1,(n1 xor n2,
  --      (n1 xor n2 xor cin,((n1 xor n2) and cin) xor (n1 and n2) xor z)))
-- spec:
-- ((false , (false , false) , false) , false , false , false , false) ∷
-- ((false , (false , false) , true)  , false , false , true  , false) ∷
-- ((false , (false , true)  , false) , false , true  , true  , false) ∷
-- ((false , (false , true)  , true)  , false , true  , false , true)  ∷
-- ((false , (true  , false) , false) , true  , true  , true  , false) ∷
-- ((false , (true  , false) , true)  , true  , true  , false , true)  ∷
-- ((false , (true  , true)  , false) , true  , false , false , true)  ∷
-- ((false , (true  , true)  , true)  , true  , false , true  , true)  ∷
-- ((true  , (false , false) , false) , false , false , false , true)  ∷
-- ((true  , (false , false) , true)  , false , false , true  , true)  ∷
-- ((true  , (false , true)  , false) , false , true  , true  , true)  ∷
-- ((true  , (false , true)  , true)  , false , true  , false , false) ∷
-- ((true  , (true  , false) , false) , true  , true  , true  , true)  ∷
-- ((true  , (true  , false) , true)  , true  , true  , false , false) ∷
-- ((true  , (true  , true)  , false) , true  , false , false , false) ∷
-- ((true  , (true  , true)  , true)  , true  , false , true  , false) ∷ []

--}
------------------------------------------------------------------------------
-- Every permutation has an inverse. There are actually many syntactically
-- different inverses but they are all equivalent.

-- Alternative view: this corresponds to Lemma 2.1.1 In our notation,
-- for every path t₁ ⟷ t₂, we have a path t₂ ⟷ t₁ such that (! id⟷)
-- reduces to id⟷.

! : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊l   = uniti₊l
! uniti₊l   = unite₊l
! unite₊r   = uniti₊r
! uniti₊r   = unite₊r
! swap₊     = swap₊
! assocl₊   = assocr₊
! assocr₊   = assocl₊
! unite⋆l    = uniti⋆l
! uniti⋆l    = unite⋆l
! unite⋆r = uniti⋆r
! uniti⋆r = unite⋆r
! swap⋆     = swap⋆
! assocl⋆   = assocr⋆
! assocr⋆   = assocl⋆
! absorbl     = factorzr
! absorbr     = factorzl
! factorzl  = absorbr
! factorzr = absorbl
! dist      = factor
! factor    = dist
! distl     = factorl
! factorl   = distl
! id⟷      = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (c₁ ⊕ c₂) = (! c₁) ⊕ (! c₂)
! (c₁ ⊗ c₂) = (! c₁) ⊗ (! c₂)

!! : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → ! (! c) ≡ c
!! {c = unite₊l} = refl
!! {c = uniti₊l} = refl
!! {c = unite₊r} = refl
!! {c = uniti₊r} = refl
!! {c = swap₊}   = refl
!! {c = assocl₊} = refl
!! {c = assocr₊} = refl
!! {c = unite⋆l}  = refl
!! {c = uniti⋆l}  = refl
!! {c = unite⋆r} = refl
!! {c = uniti⋆r} = refl
!! {c = swap⋆}   = refl
!! {c = assocl⋆} = refl
!! {c = assocr⋆} = refl
!! {c = absorbr}   = refl
!! {c = absorbl}  = refl
!! {c = factorzl}  = refl
!! {c = factorzr} = refl
!! {c = dist}    = refl
!! {c = factor}  = refl
!! {c = distl}   = refl
!! {c = factorl} = refl
!! {c = id⟷}    = refl
!! {c = c₁ ◎ c₂} =
  begin (! (! (c₁ ◎ c₂))
           ≡⟨ refl ⟩
         ! (! c₂ ◎ ! c₁)
           ≡⟨ refl ⟩
         ! (! c₁) ◎ ! (! c₂)
           ≡⟨ cong₂ _◎_ (!! {c = c₁}) (!! {c = c₂}) ⟩
         c₁ ◎ c₂ ∎)
  where open ≡-Reasoning
!! {c = c₁ ⊕ c₂} =
  begin (! (! (c₁ ⊕ c₂))
           ≡⟨ refl ⟩
         ! (! c₁) ⊕ ! (! c₂)
           ≡⟨ cong₂ _⊕_ (!! {c = c₁}) (!! {c = c₂}) ⟩
         c₁ ⊕ c₂ ∎)
  where open ≡-Reasoning
!! {c = c₁ ⊗ c₂} =
  begin (! (! (c₁ ⊗ c₂))
           ≡⟨ refl ⟩
         ! (! c₁) ⊗ ! (! c₂)
           ≡⟨ cong₂ _⊗_ (!! {c = c₁}) (!! {c = c₂}) ⟩
         c₁ ⊗ c₂ ∎)
  where open ≡-Reasoning

{--

-- size≡ and !

size≡! : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (size t₂ ≡ size t₁)
size≡! c = sym (size≡ c)

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

ttt : {t₁ t₂ t₃ t₄ : U} →
  (TIMES (PLUS t₁ t₂) (PLUS t₃ t₄)) ⟷
  (PLUS (PLUS (PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)) (TIMES t₁ t₄))) (TIMES t₂ t₄)
ttt {t₁} {t₂} {t₃} {t₄} =
  (distl ◎ (dist {t₁} {t₂} {t₃} ⊕ dist {t₁} {t₂} {t₄})) ◎ assocl₊

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

-- generalized CNOT
gcnot : {A B C : U} → (TIMES (PLUS A B) (PLUS C C)) ⟷ (TIMES (PLUS A B) (PLUS C C))
gcnot = dist ◎ (id⟷ ⊕ (id⟷ ⊗ swap₊)) ◎ factor

-- Generalized Toffolli gate.  See what 'arithmetic' it performs.
GToffoli : {A B C D E : U} → TIMES (PLUS A B) (TIMES (PLUS C D) (PLUS E E)) ⟷ TIMES (PLUS A B) (TIMES (PLUS C D) (PLUS E E))
GToffoli = dist ◎ (id⟷ ⊕ (id⟷ ⊗ gcnot)) ◎ factor

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Prelude.Alternative where

open import Agda.Primitive
open import Prelude.Bool
open import Prelude.Maybe
open import Prelude.List
open import Prelude.Sum
open import Prelude.Decidable
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.Function
open import Prelude.Monoid

module _ {a b} (F : Set a → Set b) where
  record FunctorZero : Set (lsuc a ⊔ b) where
    field
      empty : ∀ {A} → F A
      overlap {{super}} : Functor F

  record Alternative : Set (lsuc a ⊔ b) where
    infixl 3 _<|>_
    field
      _<|>_ : ∀ {A} → F A → F A → F A
      overlap {{super}} : FunctorZero

open FunctorZero {{...}} public

open Alternative {{...}} public

{-# DISPLAY FunctorZero.empty _     = empty   #-}
{-# DISPLAY Alternative._<|>_ _ x y = x <|> y #-}

instance
  FunctorZeroMaybe : ∀ {a} → FunctorZero (Maybe {a})
  empty {{FunctorZeroMaybe}} = nothing

  -- Left-biased choice
  AlternativeMaybe : ∀ {a} → Alternative (Maybe {a})
  _<|>_ {{AlternativeMaybe}} nothing y = y
  _<|>_ {{AlternativeMaybe}} x       y = x

  FunctorZeroList : ∀ {a} → FunctorZero (List {a})
  empty {{FunctorZeroList}} = []

  AlternativeList : ∀ {a} → Alternative (List {a})
  _<|>_ {{AlternativeList}} = _++_

  FunctorZeroEither : ∀ {a b} {E : Set b} {{_ : Monoid E}} → FunctorZero (Either {b = a} E)
  empty {{FunctorZeroEither}}     = left mempty

  AlternativeEither : ∀ {a b} {E : Set b} {{_ : Monoid E}} → Alternative (Either {b = a} E)
  _<|>_ {{AlternativeEither}} x y = either (const y) right x

module _ {a b} {F : Set a → Set b} {A : Set a} {{_ : FunctorZero F}} where
  guard! : Bool → F A → F A
  guard! true  x = x
  guard! false _ = empty

  guard : ∀ {p} {P : Set p} (d : Dec P) → ({{_ : P}} → F A) → F A
  guard (yes p) x = x {{p}}
  guard (no  _) _ = empty

module _ {a b} {F : Set a → Set b} {A : Set a} {{_ : Alternative F}} where
  choice : List (F A) → F A
  choice = foldr _<|>_ empty

  maybeA : {{_ : Applicative F}} → F A → F (Maybe A)
  maybeA x = just <$> x <|> pure nothing

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


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

open import Agda.Builtin.Nat

record R : Set where
  field
    r₁ : Nat
    r₂ : Nat
open R

h : (n : Nat) → R
r₁ (h zero) = {!!}
r₂ (h zero) = {!!}
h (suc n) = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Classical Propositional Logic.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Classical ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n

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

postulate
  PEM : ∀ {Γ} {φ}
      → Γ ⊢ φ ∨ ¬ φ

-- Theorem.
RAA
  : ∀ {Γ} {φ}
  → Γ , ¬ φ ⊢ ⊥
  → Γ ⊢ φ

-- Proof.
RAA {φ = φ} Γ¬φ⊢⊥ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (assume φ)
        (⊥-elim φ Γ¬φ⊢⊥)))
    PEM
-------------------------------------------------------------------------- ∎

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
open import Coinduction using ( ♭ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import System.IO.Transducers.Lazy using ()
  renaming ( done to doneL ; _⟫_ to _⟫L_ )
open import System.IO.Transducers.Strict using ()
  renaming ( done to doneS ; _⟫_ to _⟫S_ )
open import System.IO.Transducers.Session using ( Session ; I ; Σ )
open import System.IO.Transducers.Trace using ( Trace )

module System.IO.Transducers where

open System.IO.Transducers.Lazy public
  using ( _⇒_ ; inp ; out ; ⟦_⟧ ; _≃_ )

open System.IO.Transducers.Strict public
  using ( _⇛_ )

data Style : Set where
  lazy strict : Style

_⇒_is_ : Session → Session → Style → Set₁
S ⇒ T is lazy   = S ⇒ T
S ⇒ T is strict = S ⇛ T

done : ∀ {s S} → (S ⇒ S is s)
done {lazy}   = doneL
done {strict} = doneS

_⟫_ : ∀ {s S T U} → (S ⇒ T is s) → (T ⇒ U is s) → (S ⇒ U is s)
_⟫_ {lazy}   = _⟫L_
_⟫_ {strict} = _⟫S_

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:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Rationals.SigmaQ.Properties where

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

open import Cubical.HITs.Ints.QuoInt
import Cubical.HITs.SetQuotients as SetQuotient

open import Cubical.Data.Nat as ℕ hiding (_·_)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma

open import Cubical.Data.Nat.GCD
open import Cubical.Data.Nat.Coprime

open import Cubical.HITs.Rationals.QuoQ as Quo using (ℕ₊₁→ℤ)
import Cubical.HITs.Rationals.SigmaQ.Base as Sigma

reduce : Quo.ℚ → Sigma.ℚ
reduce = SetQuotient.rec Sigma.isSetℚ Sigma.[_]
  (λ { (a , b) (c , d) p →   sym (Sigma.[]-cancelʳ (a , b) d)
                           ∙ (λ i → Sigma.[ p i , ·₊₁-comm b d i ])
                           ∙ Sigma.[]-cancelʳ (c , d) b })

private
  toCoprime-eq₁ : ∀ s ((a , b) : ℕ × ℕ₊₁)
                  → signed s (toCoprime (a , b) .fst) · ℕ₊₁→ℤ b
                  ≡ signed s a · ℕ₊₁→ℤ (toCoprime (a , b) .snd)
  toCoprime-eq₁ s (a , b) =
    signed s c₁ · ℕ₊₁→ℤ b              ≡⟨ ·-signed-pos c₁ (ℕ₊₁→ℕ b) ⟩
    signed s (c₁ ℕ.· ℕ₊₁→ℕ b)          ≡[ i ]⟨ signed s (c₁ ℕ.· p₂ (~ i)) ⟩
    signed s (c₁ ℕ.· (ℕ₊₁→ℕ c₂ ℕ.· d)) ≡[ i ]⟨ signed s (c₁ ℕ.· ℕ.·-comm (ℕ₊₁→ℕ c₂) d i) ⟩
    signed s (c₁ ℕ.· (d ℕ.· ℕ₊₁→ℕ c₂)) ≡[ i ]⟨ signed s (ℕ.·-assoc c₁ d (ℕ₊₁→ℕ c₂) i) ⟩
    signed s ((c₁ ℕ.· d) ℕ.· ℕ₊₁→ℕ c₂) ≡[ i ]⟨ signed s (p₁ i ℕ.· ℕ₊₁→ℕ c₂) ⟩
    signed s (a ℕ.· ℕ₊₁→ℕ c₂)          ≡⟨ sym (·-signed-pos a (ℕ₊₁→ℕ c₂)) ⟩
    signed s a · ℕ₊₁→ℤ c₂ ∎
    where open ToCoprime (a , b)

[]-reduce : ∀ x → Quo.[ reduce x .fst ] ≡ x
[]-reduce = SetQuotient.elimProp (λ _ → Quo.isSetℚ _ _)
  (λ { (signed s a , b) → Quo.eq/ _ _ (toCoprime-eq₁ s (a , b))
     ; (posneg i , b) j → isSet→isSet' Quo.isSetℚ
         (Quo.eq/ (fst (reduce Quo.[ pos 0 , b ])) (pos 0 , b) (toCoprime-eq₁ spos (0 , b)))
         (Quo.eq/ (fst (reduce Quo.[ neg 0 , b ])) (neg 0 , b) (toCoprime-eq₁ sneg (0 , b)))
         (λ i → Quo.[ reduce (Quo.[ posneg i , b ]) .fst ]) (λ i → Quo.[ posneg i , b ]) i j })

private
  toCoprime-eq₂ : ∀ s ((a , b) : ℕ × ℕ₊₁) (cp : areCoprime (a , ℕ₊₁→ℕ b))
                  → Sigma.signedPair s (toCoprime (a , b)) ≡ Sigma.signedPair s (a , b)
  toCoprime-eq₂ s (a , b) cp i = Sigma.signedPair s (toCoprime-idem (a , b) cp i)

reduce-[] : ∀ x → reduce Quo.[ x .fst ] ≡ x
     -- equivalent to: Sigma.[ s .fst ] ≡ x
reduce-[] ((signed s a , b) , cp) =
  Σ≡Prop (λ _ → isPropIsGCD) (toCoprime-eq₂ s (a , b) cp)
reduce-[] ((posneg i , b) , cp) j =
  isSet→isSet' Sigma.isSetℚ
    (Σ≡Prop (λ _ → isPropIsGCD) (toCoprime-eq₂ spos (0 , b) cp))
    (Σ≡Prop (λ _ → isPropIsGCD) (toCoprime-eq₂ sneg (0 , b) cp))
    (λ i → Sigma.[ posneg i , b ]) (λ i → (posneg i , b) , cp) i j

Quoℚ-iso-Sigmaℚ : Iso Quo.ℚ Sigma.ℚ
Iso.fun Quoℚ-iso-Sigmaℚ = reduce
Iso.inv Quoℚ-iso-Sigmaℚ = Quo.[_] ∘ fst
Iso.rightInv Quoℚ-iso-Sigmaℚ = reduce-[]
Iso.leftInv  Quoℚ-iso-Sigmaℚ = []-reduce

Quoℚ≃Sigmaℚ : Quo.ℚ ≃ Sigma.ℚ
Quoℚ≃Sigmaℚ = isoToEquiv Quoℚ-iso-Sigmaℚ

Quoℚ≡Sigmaℚ : Quo.ℚ ≡ Sigma.ℚ
Quoℚ≡Sigmaℚ = isoToPath Quoℚ-iso-Sigmaℚ


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

module Luau.RuntimeError.ToString where

open import Agda.Builtin.Float using (primShowFloat)
open import FFI.Data.String using (String; _++_)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
open import Luau.RuntimeType.ToString using (runtimeTypeToString)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Syntax.ToString using (valueToString; exprToString)
open import Luau.Var.ToString using (varToString)
open import Luau.Syntax using (var; val; addr; binexp; block_is_end; local_←_; return; _∙_; name; _$_; ··)

errToStringᴱ : ∀ {a H} M → RuntimeErrorᴱ {a} H M → String
errToStringᴮ : ∀ {a H} B → RuntimeErrorᴮ {a} H B → String

errToStringᴱ (var x) (UnboundVariable) = "variable " ++ varToString x ++ " is unbound"
errToStringᴱ (val (addr a)) (SEGV p) = "address " ++ addrToString a ++ " is unallocated"
errToStringᴱ (M $ N) (FunctionMismatch v w p) = "value " ++ (valueToString v) ++ " is not a function"
errToStringᴱ (M $ N) (app₁ E) = errToStringᴱ M E
errToStringᴱ (M $ N) (app₂ E) = errToStringᴱ N E
errToStringᴱ (binexp M ·· N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a string"
errToStringᴱ (binexp M ·· N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a string"
errToStringᴱ (binexp M op N) (BinOpMismatch₁ v w p) = "value " ++ (valueToString v) ++ " is not a number"
errToStringᴱ (binexp M op N) (BinOpMismatch₂ v w p) = "value " ++ (valueToString w) ++ " is not a number"
errToStringᴱ (binexp M op N) (bin₁ E) = errToStringᴱ M E
errToStringᴱ (binexp M op N) (bin₂ E) = errToStringᴱ N E
errToStringᴱ (block b is B end) (block E) = errToStringᴮ B E ++ "\n  in call of function " ++ varToString (name b)

errToStringᴮ (local x ← M ∙ B) (local E) = errToStringᴱ M E ++ "\n  in definition of " ++ varToString (name x)
errToStringᴮ (return M ∙ B) (return E) = errToStringᴱ M E ++ "\n  in return statement"

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module DeadCodePatSyn.Lib where

private
  data Hidden : Set where
    hidden : Hidden

pattern not-hidden = hidden


text:
open import Data.Product using (∃; ∃-syntax; _×_; _,_)

open import DeBruijn
open import Parallel
open import Beta
open import Takahashi

par-triangle : ∀ {n} {M N : Term n}
  → M ⇉ N
    -------
  → N ⇉ M *
par-triangle {M = # x} ⇉-c = ⇉-c
par-triangle {M = ƛ M} (⇉-ƛ M⇉N) = ⇉-ƛ (par-triangle M⇉N)
par-triangle {M = (ƛ M) · N} (⇉-β M⇉M′ N⇉N′) = sub-par (par-triangle M⇉M′) (par-triangle N⇉N′)
par-triangle {M = # _   · N} (⇉-ξ M⇉M′ N⇉N′)       = ⇉-ξ (par-triangle M⇉M′) (par-triangle N⇉N′)
par-triangle {M = _ · _ · N} (⇉-ξ M⇉M′ N⇉N′)       = ⇉-ξ (par-triangle M⇉M′) (par-triangle N⇉N′)
par-triangle {M = (ƛ _) · N} (⇉-ξ (⇉-ƛ M⇉M′) N⇉N′) = ⇉-β (par-triangle M⇉M′) (par-triangle N⇉N′)

par-diamond : ∀ {n} {M A B : Term n}
  →         M ⇉ A → M ⇉ B
    ----------------------
  → ∃[ N ] (A ⇉ N × B ⇉ N)
par-diamond {M = M} M⇉A M⇉B = M * , par-triangle M⇉A , par-triangle M⇉B

strip : ∀ {n} {M A B : Term n}
  →         M ⇉  A → M ⇉* B
    ------------------------
  → ∃[ N ] (A ⇉* N × B ⇉  N)
strip {A = A} M⇉A (M ∎) = A , (A ∎) , M⇉A
strip {A = A} M⇉A (M ⇉⟨　M⇉M′ ⟩ M′⇉*B)
    with par-diamond M⇉A M⇉M′
... | N , A⇉N , M′⇉N
      with strip M′⇉N M′⇉*B
...   | N′ , N⇉*N′              , B⇉N′ =
        N′ , (A ⇉⟨ A⇉N ⟩ N⇉*N′) , B⇉N′

par-confluence : ∀ {n} {M A B : Term n}
  →         M ⇉* A → M ⇉* B
    ------------------------
  → ∃[ N ] (A ⇉* N × B ⇉* N)
par-confluence {B = B} (M ∎) M⇉*B = B , M⇉*B , (B ∎)
par-confluence {B = B} (M ⇉⟨ M⇉A ⟩ A⇉*A′) M⇉*B
    with strip M⇉A M⇉*B
... | N , A⇉*N , B⇉N
      with par-confluence A⇉*A′ A⇉*N
...   | N′ , A′⇉*N′ , N⇉*N′ =
        N′ , A′⇉*N′ , (B ⇉⟨ B⇉N ⟩ N⇉*N′)

confluence : ∀ {n} {M A B : Term n}
  →         M —↠ A → M —↠ B
    ------------------------
  → ∃[ N ] (A —↠ N × B —↠ N)
confluence M—↠A M—↠B
    with par-confluence (betas-pars M—↠A) (betas-pars M—↠B)
... | N , A⇉*N , B⇉*N =
      N , pars-betas A⇉*N , pars-betas B⇉*N

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
module Issue1258 where

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

data Bool : Set where
  true false : Bool

postulate f : (A : Set) -> A -> Bool

Foo : Bool -> Set
Foo true = Bool
Foo false = Bool

Alpha : Bool
Beta : Foo Alpha

test : f (Foo Alpha) Beta == f Bool false

Alpha = _
Beta = Alpha
test = refl

-- Normalizing Alpha yields a metavariable, but normalizing Beta yields
-- false.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module non-regular where

open import Data.Nat
open import Data.Empty
open import Data.List
open import Data.Maybe hiding ( map )
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import automaton
open import automaton-ex
open import finiteSetUtil
open import finiteSet
open import Relation.Nullary
open import regular-language
open import nat

open FiniteSet

inputnn :  List  In2 → Maybe (List In2)
inputnn [] = just []
inputnn  (i1 ∷ t) = just (i1 ∷ t)
inputnn  (i0 ∷ t) with inputnn t
... | nothing = nothing
... | just [] = nothing
... | just (i0 ∷ t1) = nothing   -- can't happen
... | just (i1 ∷ t1) = just t1   -- remove i1 from later part

inputnn1 :  List  In2 → Bool
inputnn1  s with inputnn  s
... | nothing = false
... | just [] = true
... | just _ = false

t1 = inputnn1 ( i0 ∷ i1 ∷ [] )
t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )

inputnn0 : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ ) → List  Σ → List  Σ
inputnn0 zero {_} _ _ s = s
inputnn0 (suc n) x y s = x  ∷ ( inputnn0 n x y ( y  ∷ s ) )

t4 : inputnn1 ( inputnn0 5 i0 i1 [] ) ≡ true
t4 = refl

t5 : ( n : ℕ ) → Set
t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true

--
--  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
--  The function is determinted by inputs,
--

open RegularLanguage
open Automaton

open _∧_

data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → Q → Set where
    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
    tnext : (q : Q) → {i : Σ} { is : List Σ}
        → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q

tr-len :  { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is )
tr-len {Q} {Σ} fa .[] q (tend x) = refl
tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t)

tr-accept→ : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
tr-accept→ {Q} {Σ} fa [] q (tend x)  = x
tr-accept→ {Q} {Σ} fa (i ∷ is) q  (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr

tr-accept← : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
tr-accept← {Q} {Σ} fa [] q ac = tend ac
tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac )
tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac)

tr→qs : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → Trace fa is q → List Q
tr→qs fa [] q (tend x) = []
tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr

tr→qs=is : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡  length (tr→qs fa is q tr)
tr→qs=is fa .[] q (tend x) = refl
tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is  (δ fa q i) tr)

open Data.Maybe

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
open import Relation.Binary.Definitions
open import Data.Unit using (⊤ ; tt)
open import Data.Nat.Properties

data QDSEQ { Q : Set } { Σ : Set  } { fa : Automaton  Q  Σ} ( finq : FiniteSet Q) (qd : Q) (z1 :  List Σ) :
       {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
   qd-nil :  (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
   qd-next : {i : Σ} (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false
       → QDSEQ finq qd z1 tr
       → QDSEQ finq qd z1 (tnext q tr)

record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
    field
       y z : List Σ
       yz=is : y ++ z ≡ is
       trace-z    : Trace fa z  qd
       trace-yz   : Trace fa (y ++ z)  q
       q=qd : QDSEQ finq qd z trace-yz

--
-- using accept ≡ true may simplify the pumping-lemma
-- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧  ...
--
-- like this ...
-- record TA2 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
--     field
--        y z : List Σ
--        yz=is : y ++ z ≡ is
--        trace-z    : accpet fa z qd ≡ true
--        trace-yz   : accept fa (y ++ z)  q ≡ true
--        q=qd  : last (tr→qs fa q trace-yz) ≡ just qd
--        ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd

record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
    field
       x y z : List Σ
       xyz=is : x ++ y ++ z ≡ is
       trace-xyz  : Trace fa (x ++ y ++ z)  q
       trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
       non-nil-y : ¬ (y ≡ [])

pumping-lemma : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ)
     → (tr : Trace fa is q )
     → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
     → TA fa q is
pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
   open TA
   tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q )
       → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
        ; trace-z  = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
   ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
       ; q=qd = tra-08
       ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
            ta : TA1 fa finq (δ fa q i) qd is
            ta = tra-phase2 (δ fa q i) is tr p
            tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
            tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
            tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
            tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p))  ne (TA1.q=qd ta)
   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q is
   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
   ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
           ; non-nil-y = λ ()
           ; trace-xyz  = tnext q (TA1.trace-yz ta)
           ; trace-xyyz = tnext q tra-05 } where
        ta : TA1 fa finq (δ fa q i ) qd is
        ta = tra-phase2 (δ fa q i ) is tr p
        y1 = TA1.y ta
        z1 = TA1.z ta
        tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
        tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
        tryz : Trace fa (i ∷ y1 ++ z1) qd
        tryz = tnext qd tryz0
        -- create Trace (y ++ y ++ z)
        tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
               →  QDSEQ finq qd z1 {q} {y2} tr
               → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
        tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
        ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
        ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  refl x₁ )
        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl )
        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq )
        tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
        tra-05 with equal→refl finq eq
        ... | refl = tra-04 y1  (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
   ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta)
           ; non-nil-y = non-nil-y ta
            ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
        ta : TA fa (δ fa q i ) is
        ta = tra-phase1 (δ fa q i ) is tr p

open RegularLanguage
open import Data.Nat.Properties
open import nat

lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r )
lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) {!!} (tr-accept→ (automaton r) _  (astart r) (TA.trace-xyz TAnn) )
       (tr-accept→ (automaton r) _  (astart r) (TA.trace-xyyz TAnn) ) where
    n : ℕ
    n = suc (finite (afin r))
    nn =  inputnn0 n i0 i1 []
    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
    nn01 zero = refl
    nn01 (suc i) = {!!} where
      nn02 : (i : ℕ) → ( x : List In2) → inputnn ( inputnn0 i i0 i1 x ) ≡ inputnn x
      nn02 zero _ = refl
      nn02 (suc i) x with inputnn (inputnn0 (suc i) i0 i1 x)
      ... | nothing = {!!}
      ... | just []  = {!!}
      ... | just (i0 ∷ t1)   = {!!}
      ... | just (i1 ∷ t1)   = {!!}
    nn03 : accept (automaton r) (astart r) nn ≡ true
    nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
    nn09 : (n m : ℕ) → n ≤ n + m
    nn09 zero m = z≤n
    nn09 (suc n) m = s≤s (nn09 n m)
    nn04 :  Trace (automaton r) nn (astart r)
    nn04 = tr-accept← (automaton r) nn (astart r) nn03
    nntrace = tr→qs (automaton r) nn (astart r) nn04
    nn07 : (n : ℕ) →  length (inputnn0 n i0 i1 []) ≡ n + n
    nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where
       nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s
       nn08 zero s = refl
       nn08 (suc n) s = begin
         length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩
         suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩
         suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _  ⟩
         suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n  _ _))  ⟩
         suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩
         suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n)  _ _) ⟩
         suc n + suc n + length s  ∎  where open ≡-Reasoning
    nn05 : length nntrace > finite (afin r)
    nn05 = begin
         suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
         n + n   ≡⟨ sym (nn07 n) ⟩
         length (inputnn0 n i0 i1 []) ≡⟨ tr→qs=is (automaton r) (inputnn0 n i0 i1 []) (astart r) nn04 ⟩
         length nntrace ∎  where open ≤-Reasoning
    nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04)
    nn06 = dup-in-list>n (afin r) nntrace nn05
    TAnn : TA (automaton r) (astart r) nn
    TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)
    count : In2 → List In2 → ℕ
    count _ [] = 0
    count i0 (i0 ∷ s) = suc (count i0 s)
    count i1 (i1 ∷ s) = suc (count i1 s)
    count x (_ ∷ s) = count x s
    nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
    nn11 {x} [] t = refl
    nn11 {i0} (i0 ∷ s) t = cong suc ( nn11 s t )
    nn11 {i0} (i1 ∷ s) t = nn11 s t
    nn11 {i1} (i0 ∷ s) t = nn11 s t
    nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t )
    nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
    nn10 s p = nn101 s (subst (λ k → k ≡ true) (sym (Rg s)) p ) where
        nn101 : (s : List In2) → inputnn1 s ≡ true →  count i0 s ≡ count i1 s
        nn101 [] p = refl
        nn101 (x ∷ s) p = {!!}
    i1-i0? : List In2 → Bool
    i1-i0? [] = false
    i1-i0? (i1 ∷ []) = false
    i1-i0? (i0 ∷ []) = false
    i1-i0? (i1 ∷ i0 ∷ s) = true
    i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)
    nn20 : {s s0 s1 : List In2} → accept (automaton r) (astart r) s ≡ true → ¬ ( s ≡ s0 ++ i1 ∷ i0 ∷ s1 )
    nn20 {s} {s0} {s1} p np = {!!}
    mono-color : List In2 → Bool
    mono-color [] = true
    mono-color (i0 ∷ s) = mono-color0 s where
        mono-color0 : List In2 → Bool
        mono-color0 [] = true
        mono-color0 (i1 ∷ s) = false
        mono-color0 (i0 ∷ s) = mono-color0 s
    mono-color (i1 ∷ s) = mono-color1 s where
        mono-color1 : List In2 → Bool
        mono-color1 [] = true
        mono-color1 (i0 ∷ s) = false
        mono-color1 (i1 ∷ s) = mono-color1 s
    record Is10 (s : List In2) : Set where
       field
           s0 s1 : List In2
           is-10 :  s ≡ s0 ++ i1 ∷ i0 ∷ s1
    not-mono : { s : List In2 } → ¬ (mono-color s ≡ true)  → Is10 (s ++ s)
    not-mono = {!!}
    mono-count : { s : List In2 } → mono-color s ≡ true   → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s)
    mono-count = {!!}
    tann : {x y z : List In2} → ¬ y ≡ []
       → x ++ y ++ z ≡ nn
       → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z)  ≡ true )
    tann {x} {y} {z} ny eq axyz axyyz with mono-color y
    ... | true = {!!}
    ... | false = {!!}

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
{-# OPTIONS --no-qualified-instances #-}
module CF.Transform.UnCo where

open import Data.Product
open import Data.List
open import Data.List.Relation.Unary.All
open import Data.List.Membership.Propositional

open import Relation.Unary hiding (_∈_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad hiding (unit)
open import Relation.Ternary.Monad.Weakening
open import Relation.Ternary.Data.Bigstar hiding ([_])

open import CF.Types
open import CF.Syntax.Hoisted as Hoisted
open import CF.Contexts.Lexical
open import CF.Transform.Hoist
open import CF.Syntax.DeBruijn as Tgt
open Hoisted

open import Relation.Ternary.Data.Allstar Ty

{-# TERMINATING #-}
mutual
  uncoₑ : ∀[ Hoisted.Exp a ⇑ ⇒ Tgt.Exp a ]
  uncoₑ (unit ⇈ wk)     = unit
  uncoₑ (num x ⇈ wk)    = num x
  uncoₑ (bool x ⇈ wk)   = bool x
  uncoₑ (Exp.var' vars ⇈ wk)  = Tgt.var' (member wk)
  uncoₑ (bop f e₁✴e₂ ⇈ wk) with e₁ , e₂ ← unstar (e₁✴e₂ ⇈ wk) = bop f (uncoₑ e₁) (uncoₑ e₂)
  uncoₑ (ifthenelse c✴e₁✴e₂ ⇈ wk) = let
    c  , e₁✴e₂ = unstar (c✴e₁✴e₂ ⇈ wk)
    e₁ , e₂    = unstar e₁✴e₂
    in ifthenelse (uncoₑ c) (uncoₑ e₁) (uncoₑ e₂)

  uncos : ∀[ (Allstar Hoisted.Exp as) ⇑ ⇒ Exps as ]
  uncos (nil       ⇈ wk) = []
  uncos (cons e✴es ⇈ wk) with e , es ← unstar (e✴es ⇈ wk) = uncoₑ e ∷ uncos es

{-# TERMINATING #-}
mutual
  uncoₛ : ∀[ Hoisted.Stmt r ⇑ ⇒ Tgt.Stmt r ]
  uncoₛ (run x ⇈ wk) = run (uncoₑ (x ⇈ wk))
  uncoₛ (asgn v✴e ⇈ wk) with unstar (v✴e ⇈ wk)
  ... | vars ⇈ wk' , e⇑ = asgn (member wk') (uncoₑ e⇑)
  uncoₛ (ifthenelse c✴s₁✴s₂ ⇈ wk) = let
    c  , s₁✴s₂ = unstar (c✴s₁✴s₂ ⇈ wk)
    s₁ , s₂    = unstar s₁✴s₂
    in ifthenelse (uncoₑ c) (uncoₛ s₁) (uncoₛ s₂)
  uncoₛ (while c✴s ⇈ wk) with c , s ← unstar (c✴s ⇈ wk) = while (uncoₑ c) (uncoₛ s)
  uncoₛ (block x ⇈ wk) = block (unco' (x ⇈ wk))

  unco' : ∀[ Hoisted.Block r ⇑ ⇒ Tgt.Block r ]
  unco' (nil ⇈ wk) = nil
  unco' (cons s✴b ⇈ wk) with s , b ← unstar (s✴b ⇈ wk) = uncoₛ s ⍮⍮ unco' b

unco : ∀[ Hoisted.Block r ⇒ Tgt.Block r ]
unco bl = unco' (return bl)


text:
-- Andreas, 2014-09-02
-- Up to today, there was no implementation of shadowing local variables
-- (e.g., λ-bound variables) by local imports.

-- {-# OPTIONS -v scope.locals:10 #-}

module _ where

module M where

  A = Set1

test : (A : Set) → let open M in A
test A = Set

-- The A exported by M is in competition with the local A.
-- Ambiguous name should be reported.


text:
import Imports.Issue5357-B
import Imports.Issue5357-C

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module WrongMetaLeft where

open import Imports.Level

postulate
  ∃₂ : ∀ {a c : Level} {A : Set a} {B : Set}
         (C : A → B → Set c) → Set (a ⊔ c)
  proj₂ : ∀ {a c}{A : Set a}{B : Set}{C : A → B → Set c} → ∃₂ {a}{c}{A}{B} C → B

postulate
  Position : Set
  Result   : Set
  _≡_      : Result → Result → Set

postulate
  Mono : {p : Level} (P : Position → Position → Set p) → Set p

postulate
  Fun : ∀ {a : Level} {A : Set a} →
          (A → A → Set) → (A → Result) → Set a

-- The problem is that the "wrong" meta is left unsolved. It's really the
-- level of _<P_ that's not getting solved but it's instantiated to the
-- sort of the type of resultsEqual, so the yellow ends up in a weird place.
postulate
  Monad :
    (_<P_ : Position → Position → Set _) →
    (Key : Mono _<P_ -> Result -> Set)
    (_≈_ : ∃₂ Key → ∃₂ Key → Set)
    (resultsEqual : Fun {_} {∃₂ {_}{_}{Mono _<P_}{Result} Key}
                        _≈_ (\(rfk : ∃₂ Key) ->
                            proj₂ {_}{_}{_}{Result}{_} rfk))
    → Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --universe-polymorphism #-}

module LLev where

--****************
-- Universe polymorphism
--****************

data Level : Set where
      ze : Level
      su  : Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO ze  #-}
{-# BUILTIN LEVELSUC  su   #-}

max : Level -> Level -> Level
max  ze     m     = m
max (su n)  ze    = su n
max (su n) (su m) = su (max n m)

{-# BUILTIN LEVELMAX max #-}

record Up {l : Level} (A : Set l) : Set (su l) where
  constructor up
  field down : A
open Up

record Sg {l : Level}(S : Set l)(T : S -> Set l) : Set l where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg
_*_ : {l : Level} -> Set l -> Set l -> Set l
S * T = Sg S \ _ -> T
infixr 4 _*_ _,_

data Zero : Set where

record One {l : Level} : Set l where
  constructor <>

data Desc {l : Level}(I : Set l) : Set (su l) where
  var : (i : I) -> Desc I
  con : (A : Set l) -> Desc I
  sg pi : (S : Set l)(T : S -> Desc I) -> Desc I
  _**_ : (S T : Desc I) -> Desc I
infixr 4 _**_

[!_!] : {l : Level}{I : Set l} -> Desc I -> (I -> Set l) -> Set l
[! var i !] X = X i
[! con A !] X = A
[! sg S T !] X = Sg S \ s -> [! T s !] X
[! pi S T !] X = (s : S) -> [! T s !] X
[! S ** T !] X = [! S !] X * [! T !] X

{-
data Mu {l : Level}(I : Set l)(F : I -> Desc I)(i : I) : Set l where
  <_> : [! F i !] (Mu I F) -> Mu I F i
-}

All : {l : Level}{I : Set l}
      (D : Desc I)(X : I -> Set l) -> [! D !] X -> Desc (Sg I X)
All (var i) X x = var (i , x)
All (con A) X d = con One
All (sg S T) X (s , t) = All (T s) X t
All (pi S T) X f = pi S \ s -> All (T s) X (f s)
All (S ** T) X (s , t) = All S X s ** All T X t

all : {l : Level}{I : Set l}
      (D : Desc I)(X : I -> Set l)(P : Sg I X -> Set l) ->
      ((ix : Sg I X) -> P ix) ->
      (d : [! D !] X) -> [! All D X d !] P
all (var i) X P p x = p (i , x)
all (con A) X P p d = _
all (sg S T) X P p (s , t) = all (T s) X P p t
all (pi S T) X P p f = \ s -> all (T s) X P p (f s)
all (S ** T) X P p (s , t) = all S X P p s , all T X P p t

{-
induction :  {l : Level}{I : Set l}{F : I -> Desc I}
             (P : Sg I (Mu I F) -> Set l) ->
             ((i : I)(d : [! F i !] (Mu I F)) ->
               [! All (F i) (Mu I F) d !] P -> P (i , < d >)) ->
             (ix : Sg I (Mu I F)) -> P ix
induction {F = F} P p (i , < d >) = p i d (all (F i) (Mu _ F) P (induction P p) d)
-}

{-
mutual
  induction :  {l : Level}{I : Set l}{F : I -> Desc I}
               (P : Sg I (Mu I F) -> Set l) ->
               ((i : I)(d : [! F i !] (Mu I F)) ->
                 [! All (F i) (Mu I F) d !] P -> P (i , < d >)) ->
               {i : I}(x : Mu I F i) -> P (i , x)
  induction {F = F} P p {i} < d > = p i d (allInduction F P p (F i) d)
  allInduction : {l : Level}{I : Set l}(F : I -> Desc I)
                 (P : Sg I (Mu I F) -> Set l) ->
                 ((i : I)(d : [! F i !] (Mu I F)) ->
                    [! All (F i) (Mu I F) d !] P -> P (i , < d >)) ->
                 (D : Desc I) ->
                 (d : [! D !] (Mu I F)) -> [! All D (Mu I F) d !] P
  allInduction F P p (var i) d = induction P p d
  allInduction F P p (con A) d = _
  allInduction F P p (sg S T) (s , t) = allInduction F P p (T s) t
  allInduction F P p (pi S T) f = \ s -> allInduction F P p (T s) (f s)
  allInduction F P p (S ** T) (s , t) = allInduction F P p S s , allInduction F P p T t
-}

data List {l : Level}(X : Set l) : Set l where
  [] : List X
  _::_ : X -> List X -> List X
infixr 3 _::_

map : {k l : Level}{X : Set k}{Y : Set l} -> (X -> Y) -> List X -> List Y
map f [] = []
map f (x :: xs) = f x :: map f xs

data UId {l : Level} : Set l where
  ze : UId
  su : UId {l} -> UId

data # {l : Level} : List {l} UId -> Set l where
  ze : forall {x xs} -> # (x :: xs)
  su : forall {x xs} -> # xs -> # (x :: xs)

Constrs : {l : Level} -> Set l -> Set (su l)
Constrs I = List (Up UId * Desc I)

Constr : {l : Level}{I : Set l} -> Constrs I -> Set l
Constr uDs = # (map (\ uD -> down (fst uD)) uDs)

ConD : {l : Level}{I : Set l}(uDs : Constrs I) -> Constr uDs -> Desc I
ConD [] ()
ConD (uD :: _)  ze     = snd uD
ConD (_ :: uDs) (su c) = ConD uDs c

data Data {l : Level}{I : Set l}(F : I -> Constrs I)(i : I) : Set l where
  _/_ : (u : Constr (F i))(d : [! ConD (F i) u !] (Data F)) -> Data F i

{-
DataD : {l : Level}{I : Set l} -> Constrs I -> Desc I
DataD uDs = sg (Constr uDs) (ConD uDs)

Data : {l : Level}{I : Set l}(F : I -> Constrs I)(i : I) -> Set l
Data F = Mu _ \ i -> DataD (F i)
-}

MethodD : {l : Level}{I : Set l}(X : I -> Set l)
          (uDs : Constrs I)
          (P : Sg I X -> Set l)
          (i : I) -> ((u : Constr uDs)(d : [! ConD uDs u !] X) -> X i) -> Set l
MethodD X [] P i c = One
MethodD X ((u , D) :: uDs) P i c
  = ((d : [! D !] X) -> [! All D X d !] P -> P (i , c ze d))
  * MethodD X uDs P i (\ u d -> c (su u) d)

mutual
  induction : {l : Level}{I : Set l}{F : I -> Constrs I}{i : I}(x : Data F i)
              (P : Sg I (Data F) -> Set l)
              (ps : (i : I) -> MethodD (Data F) (F i) P i _/_)
              -> P (i , x)
  induction {F = F}{i = i}(u / d) P ps = indMethod P ps (F i) _/_ (ps i) u d
  indMethod : {l : Level}{I : Set l}{F : I -> Constrs I}{i : I}
              (P : Sg I (Data F) -> Set l)
              (ps : (i : I) -> MethodD (Data F) (F i) P i _/_)
              (uDs : Constrs I)
              (c : (u : Constr uDs) -> [! ConD uDs u !] (Data F) -> Data F i)
              (ms : MethodD (Data F) uDs P i c)
              (u : Constr uDs)
              (d : [! ConD uDs u !] (Data F))
              -> P (i , c u d)
  indMethod P ps [] c ms () d
  indMethod P ps ((u , D) :: _) c (p , ms) ze d = p d (indHyps P ps D d)
  indMethod P ps ((_ , _) :: uDs) c (m , ms) (su u) d
    = indMethod P ps uDs _ ms u d
  indHyps : {l : Level}{I : Set l}{F : I -> Constrs I}
            (P : Sg I (Data F) -> Set l)
            (ps : (i : I) -> MethodD (Data F) (F i) P i _/_)
            (D : Desc I)
            (d : [! D !] (Data F))
            -> [! All D (Data F) d !] P
  indHyps P ps (var i) x = induction x P ps
  indHyps P ps (con A) a = _
  indHyps P ps (sg S T) (s , t) = indHyps P ps (T s) t
  indHyps P ps (pi S T) f = \ s -> indHyps P ps (T s) (f s)
  indHyps P ps (S ** T) (s , t) = indHyps P ps S s , indHyps P ps T t

zi : {l : Level} -> UId {l}
zi = ze

si : {l : Level} -> UId {l}
si = su ze

data UQ {l : Level}(x : UId {l}) : UId {l} -> Set l where
  yes : UQ x x
  no  : {y : UId {l}} -> UQ x y

uq : {l : Level}(x y : UId {l}) -> UQ x y
uq ze ze = yes
uq ze (su y) = no
uq (su x) ze = no
uq (su x) (su y) with uq x y
uq (su x) (su .x) | yes = yes
uq (su x) (su y)  | no  = no

UIn : {l : Level}(x : UId {l}) -> List (UId {l}) -> Set
UIn x [] = Zero
UIn x (y :: ys) with uq x y
UIn x (.x :: _) | yes = One
UIn x (_ :: ys) | no = UIn x ys

uin : {l : Level}(x : UId {l})(ys : List (UId {l})) -> UIn x ys -> # ys
uin x [] ()
uin x (y :: ys) p with uq x y
uin x (.x :: _) _ | yes = ze
uin x (_ :: ys) p | no  = su (uin x ys p)

_!_ : {l : Level}{I : Set l}{F : I -> Constrs I}{i : I} ->
      let us = map (\ uD -> down (fst uD)) (F i) in
      (u : UId {l}){p : UIn u us} ->
      [! ConD (F i) (uin u us p) !] (Data F) ->
      Data F i
_!_ {l}{I}{F}{i} u {p} d = uin u (map (\ uD -> down (fst uD)) (F i)) p / d

infixr 3 _!_

NAT : {l : Level} -> One {l} -> Constrs {l} One
NAT _ = up zi , con One
     :: up si , var _ ** con One
     :: []

ZE : {l : Level} -> Data {l} NAT <>
ZE = zi ! <>

SU : {l : Level} -> Data {l} NAT <> -> Data {l} NAT <>
SU n = si ! n , <>

vari : {l : Level} -> UId {l}
vari = ze
coni : {l : Level} -> UId {l}
coni = su ze
sgi : {l : Level} -> UId {l}
sgi = su (su ze)
pii : {l : Level} -> UId {l}
pii = su (su (su ze))
asti : {l : Level} -> UId {l}
asti = su (su (su (su ze)))

DESC : {l : Level}(I : Set l) -> One {su l} -> Constrs {su l} One
DESC I _ = up vari , con (Up I) ** con One
        :: up coni , con (Set _) ** con One
        :: up sgi , (sg (Set _) \ S -> (pi (Up S) \ _ -> var _) ** con One)
        :: up pii , (sg (Set _) \ S -> (pi (Up S) \ _ -> var _) ** con One)
        :: up asti , var _ ** var _ ** con One
        :: []


text:
postulate
  A : Set
  a : A

data D : Set where
  d : D

data E : Set where
  e₀ : E
  e₁ : E → E
  e₂ : E → E → E

_[_] : E → E → E
e₀       [ y ] = y
e₁ x     [ y ] = e₁ x
e₂ x₁ x₂ [ y ] = e₂ (x₁ [ y ]) (x₂ [ y ])

data P : E → Set where
  p₁ : ∀ x₁ x₂ → P x₁ → P x₂ → P (e₂ x₁ x₂)
  p₂ : ∀ x → P (x [ e₁ x ]) → P (e₁ x)
  p₃ : ∀ x → P (e₁ x)

module M (_ : A) where

  record R (A B : Set) : Set where
    field f : A → B

  instance
    r₁ : R D D
    R.f r₁ d = d

open M a

open R ⦃ … ⦄ public

r₂ : R D E
R.f r₂ d = e₀

instance

  r₃ : {A : Set} ⦃ c : R A D ⦄ → R A E
  R.f (r₃ ⦃ c ⦄) x = R.f r₂ (R.f c x)

f′ : {A : Set} ⦃ c : R A D ⦄ → A → E
f′ = f

postulate
  p : {A : Set} ⦃ c : R A D ⦄ (x : A) → P (f′ x)

rejected : P (e₂ (e₁ e₀) (f d))
rejected = p₁ _ (f′ d) (p₂ _ (p₃ e₀)) (p d)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Semi-heterogeneous vector equality
------------------------------------------------------------------------

module Data.Vec.Equality where

open import Data.Vec
open import Data.Nat using (suc)
open import Function
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module Equality {s₁ s₂} (S : Setoid s₁ s₂) where

  private
    open module SS = Setoid S
      using () renaming (_≈_ to _≊_; Carrier to A)

  infix 4 _≈_

  data _≈_ : ∀ {n¹} → Vec A n¹ →
             ∀ {n²} → Vec A n² → Set (s₁ ⊔ s₂) where
    []-cong  : [] ≈ []
    _∷-cong_ : ∀ {x¹ n¹} {xs¹ : Vec A n¹}
                 {x² n²} {xs² : Vec A n²}
                 (x¹≈x² : x¹ ≊ x²) (xs¹≈xs² : xs¹ ≈ xs²) →
                 x¹ ∷ xs¹ ≈ x² ∷ xs²

  length-equal : ∀ {n¹} {xs¹ : Vec A n¹}
                   {n²} {xs² : Vec A n²} →
                 xs¹ ≈ xs² → n¹ ≡ n²
  length-equal []-cong        = P.refl
  length-equal (_ ∷-cong eq₂) = P.cong suc $ length-equal eq₂

  refl : ∀ {n} (xs : Vec A n) → xs ≈ xs
  refl []       = []-cong
  refl (x ∷ xs) = SS.refl ∷-cong refl xs

  sym : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
        xs ≈ ys → ys ≈ xs
  sym []-cong                = []-cong
  sym (x¹≡x² ∷-cong xs¹≈xs²) = SS.sym x¹≡x² ∷-cong sym xs¹≈xs²

  trans : ∀ {n m l} {xs : Vec A n} {ys : Vec A m} {zs : Vec A l} →
          xs ≈ ys → ys ≈ zs → xs ≈ zs
  trans []-cong            []-cong            = []-cong
  trans (x≈y ∷-cong xs≈ys) (y≈z ∷-cong ys≈zs) =
    SS.trans x≈y y≈z ∷-cong trans xs≈ys ys≈zs

  _++-cong_ : ∀ {n₁¹ n₂¹} {xs₁¹ : Vec A n₁¹} {xs₂¹ : Vec A n₂¹}
                {n₁² n₂²} {xs₁² : Vec A n₁²} {xs₂² : Vec A n₂²} →
              xs₁¹ ≈ xs₁² → xs₂¹ ≈ xs₂² →
              xs₁¹ ++ xs₂¹ ≈ xs₁² ++ xs₂²
  []-cong          ++-cong eq₃ = eq₃
  (eq₁ ∷-cong eq₂) ++-cong eq₃ = eq₁ ∷-cong (eq₂ ++-cong eq₃)

module DecidableEquality {d₁ d₂} (D : DecSetoid d₁ d₂) where

  private module DS = DecSetoid D
  open DS using () renaming (_≟_ to _≟′_ ; Carrier to A)
  open Equality DS.setoid
  open import Relation.Nullary

  _≟_ : ∀ {n m} (xs : Vec A n) (ys : Vec A m) → Dec (xs ≈ ys)
  _≟_ []       []       = yes []-cong
  _≟_ []       (y ∷ ys) = no (λ())
  _≟_ (x ∷ xs) []       = no (λ())
  _≟_ (x ∷ xs) (y ∷ ys) with xs ≟ ys | x ≟′ y
  ... | yes xs≈ys | yes x≊y = yes (x≊y ∷-cong xs≈ys)
  ... | no ¬xs≈ys | _       = no helper
    where
    helper : ¬ (x ∷ xs ≈ y ∷ ys)
    helper (_ ∷-cong xs≈ys) = ¬xs≈ys xs≈ys
  ... | _         | no ¬x≊y = no helper
    where
    helper : ¬ (x ∷ xs ≈ y ∷ ys)
    helper (x≊y ∷-cong _) = ¬x≊y x≊y

module PropositionalEquality {a} {A : Set a} where

  open Equality (P.setoid A) public

  to-≡ : ∀ {n} {xs ys : Vec A n} → xs ≈ ys → xs ≡ ys
  to-≡ []-cong                 = P.refl
  to-≡ (P.refl ∷-cong xs¹≈xs²) = P.cong (_∷_ _) $ to-≡ xs¹≈xs²

  from-≡ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≈ ys
  from-≡ P.refl = refl _


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Strict

foo : Nat → Nat
foo n = primForce (n + n) (λ _ → 0)
      -- Don't get rid of the seq!


text:
module Lec6 where

open import CS410-Prelude
open import CS410-Functor
open import CS410-Monoid
open import CS410-Nat

data Maybe (X : Set) : Set where
  yes  : X -> Maybe X
  no   : Maybe X

maybeFunctor : Functor Maybe
maybeFunctor = record
 { map      = \ { f (yes x) -> yes (f x)
                ; f no      -> no
                }
 ; mapid    = \ { (yes x) -> refl ; no -> refl }
 ; mapcomp  = \ { f g (yes x) -> refl ; f g no -> refl } }

open Functor maybeFunctor

data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_

may-take : {X : Set} -> Nat -> List X -> Maybe (List X)
may-take zero xs = yes []
may-take (suc n) [] = no
may-take (suc n) (x :: xs) = map (_::_ x) (may-take n xs)

data Hutton : Set where
  val : Nat -> Hutton
  _+H_ : Hutton -> Hutton -> Hutton
  fail : Hutton

maybeApplicative : Applicative Maybe
maybeApplicative = record
                     { pure = yes
                     ; _<*>_ = \ { no mx -> no
                                 ; (yes f) no -> no
                                 ; (yes f) (yes x) -> yes (f x)
                                 }
                     ; identity = \ {(yes x) -> refl ; no -> refl}
                     ; composition = \
                        { (yes f) (yes g) (yes x) -> refl
                        ; (yes f) (yes g) no -> refl
                        ; (yes x) no mx -> refl
                        ; no mg mx -> refl
                        }
                     ; homomorphism = \ f x -> refl
                     ; interchange = \ { (yes f) y -> refl ; no y → refl }
                     }

module Eval where
  open Applicative maybeApplicative public

  eval : Hutton -> Maybe Nat
  eval (val x) = yes x
  eval (h +H h') = pure _+N_ <*> eval h <*> eval h'
  eval fail = no

listTrav : forall {F} -> Applicative F -> forall {A B} ->
           (A -> F B) -> List A -> F (List B)
listTrav {F} appF = trav where
  open Applicative appF
  trav : forall {A B} -> (A -> F B) -> List A -> F (List B)
  trav f []         = pure []
  trav f (a :: as)  = pure _::_ <*> f a <*> trav f as

listTraversable : Traversable List
listTraversable = record { traverse = listTrav }

I : Set -> Set
I X = X

iApplicative : Applicative I
iApplicative = record
  { pure = id
  ; _<*>_ = id
  ; identity = \ v -> refl
  ; composition = \ f g v -> refl
  ; homomorphism = \ f x -> refl
  ; interchange = \ u y -> refl
  }

lmap : forall {A B} -> (A -> B) -> List A -> List B
lmap = traverse iApplicative where
  open Traversable listTraversable

MonCon : forall {X} -> Monoid X -> Applicative \_ -> X
MonCon M = record
             { pure          = {!!}
             ; _<*>_         = op
             ; identity      = {!!}
             ; composition   = {!!}
             ; homomorphism  = {!!}
             ; interchange   = {!!}
             } where open Monoid M

lCombine : forall {A X} -> Monoid X -> (A -> X) -> List A -> X
lCombine M = traverse (MonCon M) {B = One} where
  open Traversable listTraversable

CurryApplicative : forall {E} -> Applicative \X -> E -> X
CurryApplicative = record
                     { pure = \ x e -> x  -- K
                     ; _<*>_ = \ ef ex e -> ef e (ex e)  -- S
                     ; identity = λ {X} v → refl
                     ; composition = λ {X} {Y} {Z} u v w → refl
                     ; homomorphism = λ {X} {Y} f x → refl
                     ; interchange = λ {X} {Y} u y → refl
                     }


text:
module Issue4267.A0 where

record RA0 : Set₁ where
  field
    A : Set


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

module Number.InclusionModules where

import Number.Postulates
import Number.Inclusions

-- NOTE: the following takes a very long time to typecheck
-- see https://lists.chalmers.se/pipermail/agda-dev/2015-September/000201.html
-- see https://github.com/agda/agda/issues/1646
--     Exponential module chain leads to infeasible scope checking

module Isℕ↪ℤ = Number.Inclusions.IsROrderedCommSemiringInclusion Number.Postulates.ℕ↪ℤinc
module Isℕ↪ℚ = Number.Inclusions.IsROrderedCommSemiringInclusion Number.Postulates.ℕ↪ℚinc
module Isℕ↪ℂ = Number.Inclusions.Isℕ↪ℂ                           Number.Postulates.ℕ↪ℂinc
module Isℕ↪ℝ = Number.Inclusions.IsROrderedCommSemiringInclusion Number.Postulates.ℕ↪ℝinc
module Isℤ↪ℚ = Number.Inclusions.IsROrderedCommRingInclusion     Number.Postulates.ℤ↪ℚinc
module Isℤ↪ℝ = Number.Inclusions.IsROrderedCommRingInclusion     Number.Postulates.ℤ↪ℝinc
module Isℤ↪ℂ = Number.Inclusions.Isℤ↪ℂ                           Number.Postulates.ℤ↪ℂinc
module Isℚ↪ℝ = Number.Inclusions.IsROrderedFieldInclusion        Number.Postulates.ℚ↪ℝinc
module Isℚ↪ℂ = Number.Inclusions.IsRFieldInclusion               Number.Postulates.ℚ↪ℂinc
module Isℝ↪ℂ = Number.Inclusions.IsRFieldInclusion               Number.Postulates.ℝ↪ℂinc

{-
-- NOTE: the following is a little faster but does not help us

module Isℕ↪ℤ = Number.Inclusions.IsROrderedCommSemiringInclusion
module Isℕ↪ℚ = Number.Inclusions.IsROrderedCommSemiringInclusion
module Isℕ↪ℂ = Number.Inclusions.Isℕ↪ℂ
module Isℕ↪ℝ = Number.Inclusions.IsROrderedCommSemiringInclusion
module Isℤ↪ℚ = Number.Inclusions.IsROrderedCommRingInclusion
module Isℤ↪ℝ = Number.Inclusions.IsROrderedCommRingInclusion
module Isℤ↪ℂ = Number.Inclusions.Isℤ↪ℂ
module Isℚ↪ℝ = Number.Inclusions.IsROrderedFieldInclusion
module Isℚ↪ℂ = Number.Inclusions.IsRFieldInclusion
module Isℝ↪ℂ = Number.Inclusions.IsRFieldInclusion
-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of binary operators to binary relations via the right
-- natural order.
------------------------------------------------------------------------

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

open import Relation.Binary
open import Algebra.FunctionProperties using (Op₂)

module Relation.Binary.Construct.NaturalOrder.Right
  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A) where

open import Data.Product using (_,_; _×_)
open import Data.Sum using (inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Algebra.FunctionProperties _≈_
open import Algebra.Structures _≈_
import Relation.Binary.Reasoning.Setoid as EqReasoning

------------------------------------------------------------------------
-- Definition

infix 4 _≤_

_≤_ : Rel A ℓ
x ≤ y = x ≈ (y ∙ x)

------------------------------------------------------------------------
-- Relational properties

reflexive : IsMagma _∙_ → Idempotent _∙_ → _≈_ ⇒ _≤_
reflexive magma idem {x} {y} x≈y = begin
  x     ≈⟨ sym (idem x) ⟩
  x ∙ x ≈⟨ ∙-cong x≈y refl ⟩
  y ∙ x ∎
  where open IsMagma magma; open EqReasoning setoid

refl : Symmetric _≈_ → Idempotent _∙_ → Reflexive _≤_
refl sym idem {x} = sym (idem x)

antisym : IsEquivalence _≈_ → Commutative _∙_ → Antisymmetric _≈_ _≤_
antisym isEq comm {x} {y} x≤y y≤x = begin
  x     ≈⟨ x≤y ⟩
  y ∙ x ≈⟨ comm y x ⟩
  x ∙ y ≈⟨ sym y≤x ⟩
  y     ∎
  where open IsEquivalence isEq; open EqReasoning (record { isEquivalence = isEq })

total : Symmetric _≈_ → Transitive _≈_ → Selective _∙_ → Commutative _∙_ → Total _≤_
total sym trans sel comm x y with sel x y
... | inj₁ x∙y≈x = inj₁ (trans (sym x∙y≈x) (comm x y) )
... | inj₂ x∙y≈y = inj₂ (sym x∙y≈y)

trans : IsSemigroup _∙_ → Transitive _≤_
trans semi {x} {y} {z} x≤y y≤z = begin
  x           ≈⟨ x≤y ⟩
  y ∙ x       ≈⟨ ∙-cong y≤z S.refl ⟩
  (z ∙ y) ∙ x ≈⟨ assoc z y x ⟩
  z ∙ (y ∙ x) ≈⟨ ∙-cong S.refl (sym x≤y) ⟩
  z ∙ x       ∎
  where open module S = IsSemigroup semi; open EqReasoning S.setoid

respʳ : IsMagma _∙_ → _≤_ Respectsʳ _≈_
respʳ magma {x} {y} {z} y≈z x≤y = begin
  x     ≈⟨ x≤y ⟩
  y ∙ x ≈⟨ ∙-cong y≈z M.refl ⟩
  z ∙ x ∎
  where open module M = IsMagma magma; open EqReasoning M.setoid

respˡ : IsMagma _∙_ → _≤_ Respectsˡ _≈_
respˡ magma {x} {y} {z} y≈z y≤x = begin
  z     ≈⟨ sym y≈z ⟩
  y     ≈⟨ y≤x ⟩
  x ∙ y ≈⟨ ∙-cong M.refl y≈z ⟩
  x ∙ z ∎
  where open module M = IsMagma magma; open EqReasoning M.setoid

resp₂ : IsMagma _∙_ →  _≤_ Respects₂ _≈_
resp₂ magma = respʳ magma , respˡ magma

dec : Decidable _≈_ → Decidable _≤_
dec _≟_ x y = x ≟ (y ∙ x)

------------------------------------------------------------------------
-- Structures

isPreorder : IsBand _∙_ → IsPreorder _≈_ _≤_
isPreorder band = record
  { isEquivalence = isEquivalence
  ; reflexive     = reflexive isMagma idem
  ; trans         = trans isSemigroup
  }
  where open IsBand band hiding (reflexive; trans)

isPartialOrder : IsSemilattice _∙_ → IsPartialOrder _≈_ _≤_
isPartialOrder semilattice = record
  { isPreorder = isPreorder isBand
  ; antisym    = antisym isEquivalence comm
  }
  where open IsSemilattice semilattice

isDecPartialOrder : IsSemilattice _∙_ → Decidable _≈_ →
                    IsDecPartialOrder _≈_ _≤_
isDecPartialOrder semilattice _≟_ = record
  { isPartialOrder = isPartialOrder semilattice
  ; _≟_            = _≟_
  ; _≤?_           = dec _≟_
  }

isTotalOrder : IsSemilattice _∙_ → Selective _∙_ → IsTotalOrder _≈_ _≤_
isTotalOrder latt sel  = record
  { isPartialOrder = isPartialOrder latt
  ; total          = total sym S.trans sel comm
  }
  where open module S = IsSemilattice latt

isDecTotalOrder : IsSemilattice _∙_ → Selective _∙_ →
                  Decidable _≈_ → IsDecTotalOrder _≈_ _≤_
isDecTotalOrder latt sel _≟_ = record
  { isTotalOrder = isTotalOrder latt sel
  ; _≟_          = _≟_
  ; _≤?_         = dec _≟_
  }

------------------------------------------------------------------------
-- Packages

preorder : IsBand _∙_ → Preorder a ℓ ℓ
preorder band = record
  { isPreorder = isPreorder band
  }

poset : IsSemilattice _∙_ → Poset a ℓ ℓ
poset latt = record
  { isPartialOrder = isPartialOrder latt
  }

decPoset : IsSemilattice _∙_ → Decidable _≈_ → DecPoset a ℓ ℓ
decPoset latt dec = record
  { isDecPartialOrder = isDecPartialOrder latt dec
  }

totalOrder : IsSemilattice _∙_ → Selective _∙_ → TotalOrder a ℓ ℓ
totalOrder latt sel = record
  { isTotalOrder = isTotalOrder latt sel
  }

decTotalOrder : IsSemilattice _∙_ → Selective _∙_ →
                Decidable _≈_ → DecTotalOrder a ℓ ℓ
decTotalOrder latt sel dec = record
  { isDecTotalOrder = isDecTotalOrder latt sel dec
  }


text:
-- Andreas, 2011-10-06
module Issue483b where

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

postulate
  A : Set
  f : .A → A

test : let X : .A → A
           X = _
       in .(x : A) → X (f x) ≡ f x
test x = refl
-- this gave an internal error before because X _ = f x
-- was solved by X = λ _ → f __IMPOSSIBLE__
--
-- Now one should get an unsolved meta

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-
  USES WITH
-}
{-

  A simple bidirectional type checker for simply typed lambda calculus which is
  sound by construction.

-}
module SimpleTypes where

infix 10 _==_

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

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A -> Maybe A

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (suc n)
  fsuc  : {n : Nat} -> Fin n -> Fin (suc n)

data List (A : Set) : Set where
  ε   : List A
  _,_ : List A -> A -> List A

length : forall {A} -> List A -> Nat
length ε        = zero
length (xs , x) = suc (length xs)

infixl 25 _,_

-- Raw terms

data Expr : Set where
  varʳ : Nat -> Expr
  _•ʳ_ : Expr -> Expr -> Expr
  ƛʳ_  : Expr -> Expr

infixl 90 _•ʳ_
infix  50 ƛʳ_

-- Types

data Type : Set where
  ι : Type
  _⟶_ : Type -> Type -> Type

infixr 40 _⟶_

-- Typed terms

Ctx = List Type

data Var : Ctx -> Type -> Set where
  vz : forall {Γ τ} -> Var (Γ , τ) τ
  vs : forall {Γ τ σ} -> Var Γ τ -> Var (Γ , σ) τ

data Term : Ctx -> Type -> Set where
  var : forall {Γ τ} -> Var Γ τ -> Term Γ τ
  _•_ : forall {Γ τ σ} -> Term Γ (τ ⟶ σ) -> Term Γ τ -> Term Γ σ
  ƛ_  : forall {Γ τ σ} -> Term (Γ , σ) τ -> Term Γ (σ ⟶ τ)

infixl 90 _•_
infix  50 ƛ_

-- Type erasure

⌊_⌋ˣ : forall {Γ τ} -> Var Γ τ -> Nat
⌊ vz   ⌋ˣ = zero
⌊ vs x ⌋ˣ = suc ⌊ x ⌋ˣ

⌊_⌋ : forall {Γ τ} -> Term Γ τ -> Expr
⌊ var v ⌋ = varʳ ⌊ v ⌋ˣ
⌊ s • t ⌋ = ⌊ s ⌋ •ʳ ⌊ t ⌋
⌊ ƛ t   ⌋ = ƛʳ ⌊ t ⌋

-- Type equality

infix 30 _≟_

_≟_ : (σ τ : Type) -> Maybe (σ == τ)
ι       ≟ ι       = just refl
σ₁ ⟶ τ₁ ≟ σ₂ ⟶ τ₂ with σ₁ ≟ σ₂ | τ₁ ≟ τ₂
σ  ⟶ τ  ≟ .σ ⟶ .τ | just refl | just refl = just refl
_  ⟶ _  ≟ _  ⟶ _  | _         | _         = nothing
_       ≟ _       = nothing

-- The type checked view

  -- ok  : forall {Γ τ e} -> Check ⌊ e ⌋ -- unsolved metas with no range!

data Check (Γ : Ctx)(τ : Type) : Expr -> Set where
  ok  : (t : Term Γ τ) -> Check Γ τ ⌊ t ⌋
  bad : {e : Expr} -> Check Γ τ e

data Infer (Γ : Ctx) : Expr -> Set where
  yes : (τ : Type)(t : Term Γ τ) -> Infer Γ ⌊ t ⌋
  no  : {e : Expr} -> Infer Γ e

data Lookup (Γ : Ctx) : Nat -> Set where
  found      : (τ : Type)(x : Var Γ τ) -> Lookup Γ ⌊ x ⌋ˣ
  outofscope : {n : Nat} -> Lookup Γ n

lookup : (Γ : Ctx)(n : Nat) -> Lookup Γ n
lookup ε n = outofscope
lookup (Γ , τ) zero = found τ vz
lookup (Γ , σ) (suc n) with lookup Γ n
lookup (Γ , σ) (suc .(⌊ x ⌋ˣ)) | found τ x  = found τ (vs x)
lookup (Γ , σ) (suc n)         | outofscope = outofscope

infix 20 _⊢_∋_ _⊢_∈

_⊢_∈ : (Γ : Ctx)(e : Expr) -> Infer Γ e

_⊢_∋_ : (Γ : Ctx)(τ : Type)(e : Expr) -> Check Γ τ e
Γ ⊢ ι       ∋ ƛʳ e = bad
Γ ⊢ (σ ⟶ τ) ∋ ƛʳ e with Γ , σ ⊢ τ ∋ e
Γ ⊢ (σ ⟶ τ) ∋ ƛʳ .(⌊ t ⌋) | ok t = ok (ƛ t)
Γ ⊢ (σ ⟶ τ) ∋ ƛʳ _        | bad  = bad
Γ ⊢ τ ∋ e with Γ ⊢ e ∈
Γ ⊢ τ ∋ .(⌊ t ⌋) | yes σ t with τ ≟ σ
Γ ⊢ τ ∋ .(⌊ t ⌋) | yes .τ t | just refl = ok t
Γ ⊢ τ ∋ .(⌊ t ⌋) | yes σ t  | nothing   = bad
Γ ⊢ τ ∋ e | no = bad

Γ ⊢ varʳ i         ∈ with lookup Γ i
Γ ⊢ varʳ .(⌊ x ⌋ˣ) ∈ | found τ x  = yes τ (var x)
Γ ⊢ varʳ _         ∈ | outofscope = no
Γ ⊢ e₁        •ʳ e₂ ∈        with Γ ⊢ e₁ ∈
Γ ⊢ e₁        •ʳ e₂ ∈        | no       = no
Γ ⊢ .(⌊ t₁ ⌋) •ʳ e₂ ∈        | yes ι t₁ = no
Γ ⊢ .(⌊ t₁ ⌋) •ʳ e₂ ∈        | yes (σ ⟶ τ) t₁ with Γ ⊢ σ ∋ e₂
Γ ⊢ .(⌊ t₁ ⌋) •ʳ .(⌊ t₂ ⌋) ∈ | yes (σ ⟶ τ) t₁ | ok t₂ = yes τ (t₁ • t₂)
Γ ⊢ .(⌊ t₁ ⌋) •ʳ _         ∈ | yes (σ ⟶ τ) t₁ | bad   = no
Γ ⊢ ƛʳ e     ∈ = no

-- Proving completeness (for normal terms)

-- Needs magic with

{-
mutual
  data Nf : forall {Γ τ} -> Term Γ τ -> Set where
    ƛ-nf  : forall {Γ σ τ} -> {t : Term (Γ , σ) τ} -> Nf t -> Nf (ƛ t)
    ne-nf : forall {Γ τ} -> {t : Term Γ τ} -> Ne t -> Nf t

  data Ne : forall {Γ τ} -> Term Γ τ -> Set where
    •-ne : forall {Γ σ τ} ->
           {t₁ : Term Γ (σ ⟶ τ)} -> Ne t₁ ->
           {t₂ : Term Γ σ} -> Nf t₂ -> Ne (t₁ • t₂)
    var-ne : forall {Γ τ} -> {x : Var Γ τ} -> Ne (var x)

mutual
  complete-check : forall {Γ τ} -> (t : Term Γ τ) -> Nf t ->
                   Γ ⊢ τ ∋ ⌊ t ⌋ == ok t
  complete-check ._ (ƛ-nf t) = {! !}
  complete-check _ (ne-nf n) with complete-infer _ n
  complete-check t (ne-nf n) | p = {! !}

  complete-infer : forall {Γ τ} -> (t : Term Γ τ) -> Ne t ->
                   Γ ⊢ ⌊ t ⌋ ∈ == yes τ t
  complete-infer t ne = {! !}
-}

-- Testing

test1 = ε ⊢ ι ⟶ ι ∋ ƛʳ varʳ zero
test2 = ε , ι , ι ⟶ ι ⊢ varʳ zero •ʳ varʳ (suc zero) ∈

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module Prelude.Applicative.Indexed {i} {I : Set i} where

open import Agda.Primitive
open import Prelude.Unit
open import Prelude.Functor
open import Prelude.Function
open import Prelude.Equality
open import Prelude.Number
open import Prelude.Semiring
open import Prelude.Fractional

record IApplicative {a b} (F : I → I → Set a → Set b) : Set (i ⊔ lsuc a ⊔ b) where
  infixl 4 _<*>_ _<*_ _*>_
  field
    pure  : ∀ {A i} → A → F i i A
    _<*>_ : ∀ {A B i j k} → F i j (A → B) → F j k A → F i k B
    overlap {{super}} : ∀ {i j} → Functor (F i j)

  _<*_ : ∀ {A B i j k} → F i j A → F j k B → F i k A
  a <* b = ⦇ const a b ⦈

  _*>_ : ∀ {A B i j k} → F i j A → F j k B → F i k B
  a *> b = ⦇ (const id) a b ⦈

open IApplicative {{...}} public

{-# DISPLAY IApplicative.pure  _ = pure  #-}
{-# DISPLAY IApplicative._<*>_ _ = _<*>_ #-}
{-# DISPLAY IApplicative._<*_  _ = _<*_  #-}
{-# DISPLAY IApplicative._*>_  _ = _*>_  #-}

-- Level polymorphic functors
record IApplicative′ {a b} (F : ∀ {a} → I → I → Set a → Set a) : Set (i ⊔ lsuc (a ⊔ b)) where
  infixl 4 _<*>′_
  field
    _<*>′_ : {A : Set a} {B : Set b} {i j k : I} → F i j (A → B) → F j k A → F i k B
    overlap {{super}} : ∀ {i j} → Functor′ {a} {b} (F i j)

open IApplicative′ {{...}} public

module _ {F : ∀ {a} → I → I → Set a → Set a}
         {{_ : ∀ {a} → IApplicative {a = a} F}}
         {{_ : ∀ {a b} → IApplicative′ {a = a} {b = b} F}}
         {a b} {A : Set a} {B : Set b} {i j k} where

  infixl 4 _<*′_ _*>′_
  _<*′_ : F i j A → F j k B → F i k A
  a <*′ b = pure const <*>′ a <*>′ b

  _*>′_ : F i j A → F j k B → F i k B
  a *>′ b = pure (const id) <*>′ a <*>′ b

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------
-- A very brief treatment of different kinds of term equivalences,
-- including contextual equivalence and applicative bisimilarity
------------------------------------------------------------------------

module Lambda.Closure.Equivalences where

open import Category.Monad.Partiality as Partiality
  using (_⊥; later⁻¹; laterˡ⁻¹; laterʳ⁻¹)
open import Codata.Musical.Notation
open import Data.Fin using (Fin; zero)
open import Data.Maybe hiding (_>>=_)
open import Data.Maybe.Relation.Binary.Pointwise as Maybe
  using (just; nothing)
open import Data.Nat
open import Data.Product as Prod
open import Data.Unit
open import Data.Vec using ([]; _∷_)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open Partiality._⊥
private
  open module EP {A : Set} = Partiality.Equality (_≡_ {A = A})
  open module RP {A : Set} =
    Partiality.Reasoning (P.isEquivalence {A = A})

  open module RC {A : Set} =
    Partiality.Reasoning {_∼_ = λ (_ _ : A) → ⊤} _
      using () renaming (_≈⟨_⟩_ to _≈○⟨_⟩_; _∎ to _∎○)

open import Lambda.Closure.Functional
open PF using (return; _>>=_; fail)
open import Lambda.Syntax
open Closure Tm

------------------------------------------------------------------------
-- Two equivalent notions of equivalence of partial values

-- _≈○_ is a notion of weak bisimilarity which identifies all values.

open module EC {A : Set} = Partiality.Equality (λ (_ _ : A) → ⊤)
  using () renaming (_≈_ to _≈○_)

-- _≈○_ is equivalent to "terminates iff terminates".

≈○⇔⇓≈⇓ : {A : Set} {x y : A ⊥} → x ≈○ y ⇔ (x ⇓ ⇔ y ⇓)
≈○⇔⇓≈⇓ {A} = equivalence
  (λ x≈y → equivalence (h₁ x≈y) (h₁ (RC.sym x≈y)))
  (h₂ _ _)
  where
  h₁ : {x y : A ⊥} → x ≈○ y → x ⇓ → y ⇓
  h₁ (EC.now _)      (v , now P.refl) = -, now P.refl
  h₁ (EC.later  x≈y) (v , laterˡ x⇓v) = Prod.map id laterˡ $ h₁ (♭ x≈y) (v , x⇓v)
  h₁ (EC.laterʳ x≈y) (v , x⇓v)        = Prod.map id laterˡ $ h₁    x≈y  (v , x⇓v)
  h₁ (EC.laterˡ x≈y) (v , laterˡ x⇓v) =                      h₁    x≈y  (v , x⇓v)

  h₂ : (x y : A ⊥) → x ⇓ ⇔ y ⇓ → x ≈○ y
  h₂ (now v) y x⇓⇔y⇓ =
    now v  ≈○⟨ EC.now _ ⟩
    now _  ≈○⟨ Partiality.map _ (sym $ proj₂ $ Equivalence.to   x⇓⇔y⇓ ⟨$⟩ (-, now P.refl)) ⟩
    y      ∎○

  h₂ x (now v) x⇓⇔y⇓ =
    x      ≈○⟨ Partiality.map _ (      proj₂ $ Equivalence.from x⇓⇔y⇓ ⟨$⟩ (-, now P.refl)) ⟩
    now _  ≈○⟨ EC.now _ ⟩
    now v  ∎○

  h₂ (later x) (later y) x⇓⇔y⇓ = EC.later (♯
    h₂ (♭ x) (♭ y)
       (equivalence (lemma (_⟨$⟩_ (Equivalence.to   x⇓⇔y⇓)))
                    (lemma (_⟨$⟩_ (Equivalence.from x⇓⇔y⇓)))))
    where
    lemma : {A : Set} {x y : ∞ (A ⊥)} →
            (later x ⇓ → later y ⇓) → (♭ x ⇓ → ♭ y ⇓)
    lemma hyp (v , x⇓) = Prod.map id laterˡ⁻¹ $ hyp (v , laterˡ x⇓)

------------------------------------------------------------------------
-- Two equivalent definitions of contextual equivalence

-- Context m n consists of contexts with zero or more holes. The holes
-- expect terms of type Tm m, and if we fill those holes we get a term
-- of type Tm n.

infixl 9 _·_

data Context (m : ℕ) : ℕ → Set where
  •   : Context m m
  con : ∀ {n} (i : ℕ) → Context m n
  var : ∀ {n} (x : Fin n) → Context m n
  ƛ   : ∀ {n} (C : Context m (suc n)) → Context m n
  _·_ : ∀ {n} (C₁ C₂ : Context m n) → Context m n

-- Fills all the holes.

infix 10 _[_]

_[_] : ∀ {m n} → Context m n → Tm m → Tm n
•         [ t ] = t
con i     [ t ] = con i
var x     [ t ] = var x
ƛ C       [ t ] = ƛ (C [ t ])
(C₁ · C₂) [ t ] = C₁ [ t ] · C₂ [ t ]

-- Contextual equivalence.
--
-- Termination is the only observation. This is perhaps a bit strange:
-- there is no way to observe the difference between con i and con j
-- for i ≢ j.

infix 4 _≈C_

_≈C_ : ∀ {n} → Tm n → Tm n → Set
t₁ ≈C t₂ = ∀ C → ⟦ C [ t₁ ] ⟧ [] ≈○ ⟦ C [ t₂ ] ⟧ []

-- Alternative definition of contextual equivalence.

infix 4 _≈C′_

_≈C′_ : ∀ {n} → Tm n → Tm n → Set
t₁ ≈C′ t₂ = ∀ C → ⟦ C [ t₁ ] ⟧ [] ⇓ ⇔ ⟦ C [ t₂ ] ⟧ [] ⇓

-- These definitions are equivalent.

≈C⇔≈C′ : ∀ {n} {t₁ t₂ : Tm n} → t₁ ≈C t₂ ⇔ t₁ ≈C′ t₂
≈C⇔≈C′ = equivalence
  (λ t₁≈t₂ C → Equivalence.to   ≈○⇔⇓≈⇓ ⟨$⟩ t₁≈t₂ C)
  (λ t₁≈t₂ C → Equivalence.from ≈○⇔⇓≈⇓ ⟨$⟩ t₁≈t₂ C)

------------------------------------------------------------------------
-- A very strict term equivalence

-- A term equivalence defined directly on top of the semantics.

infix 4 _≈!_

_≈!_ : ∀ {n} → Tm n → Tm n → Set
t₁ ≈! t₂ = ∀ ρ → ⟦ t₁ ⟧ ρ ≈ ⟦ t₂ ⟧ ρ

-- This equivalence is not compatible.
--
-- Note that the proof does not use constants (con).

¬-compatible : ¬ ((t₁ t₂ : Tm 1) → t₁ ≈! t₂ → ƛ t₁ ≈! ƛ t₂)
¬-compatible ƛ-cong with
  ƛ-cong (ƛ (vr 1) · ƛ (ƛ (vr 0))) (ƛ (vr 1) · ƛ (vr 0))
         (λ _ → later (♯ now P.refl))
         []
... | now ()

------------------------------------------------------------------------
-- Incorrect definition of applicative bisimilarity

-- The difference between this definition and the one below is that in
-- this definition ƛ is inductive rather than coinductive.

module Incorrect where

  infix 4 _≈mv_ _≈v_

  -- _≈mv_, _≈c_ and _≈v_ are defined mutually (coinductively).

  data _≈v_ : Value → Value → Set

  -- Equivalence of possibly exceptional values.

  _≈mv_ : Maybe Value → Maybe Value → Set
  _≈mv_ = Maybe.Pointwise _≈v_

  -- Equivalence of computations.

  open module EA = Partiality.Equality _≈mv_
    using () renaming (_≈_ to _≈c_)

  -- Equivalence of values.

  data _≈v_ where
    con : ∀ {i} → con i ≈v con i
    ƛ   : ∀ {n₁} {t₁ : Tm (1 + n₁)} {ρ₁} {n₂} {t₂ : Tm (1 + n₂)} {ρ₂}
          (t₁≈t₂ : ∀ v → ⟦ t₁ ⟧ (v ∷ ρ₁) ≈c ⟦ t₂ ⟧ (v ∷ ρ₂)) →
          ƛ t₁ ρ₁ ≈v ƛ t₂ ρ₂

  -- Applicative bisimilarity.

  infix 4 _≈t_

  _≈t_ : ∀ {n} → Tm n → Tm n → Set
  t₁ ≈t t₂ = ∀ ρ → ⟦ t₁ ⟧ ρ ≈c ⟦ t₂ ⟧ ρ

  -- This notion of applicative bisimilarity is not reflexive.
  --
  -- Note that the definition above is a bit strange in Agda: it is
  -- subject to the quantifier inversion described by Thorsten
  -- Altenkirch and myself in "Termination Checking in the Presence of
  -- Nested Inductive and Coinductive Types". However, for this proof
  -- it does not matter if _≈c_ is seen as having the form
  -- μX.νY.μZ. F X Y Z or νX.μY. F X Y; the ν part is never used.

  mutual

    distinct-c : ¬ now (just (ƛ (var zero) [])) ≈c
                   now (just (ƛ (var zero) []))
    distinct-c (now eq) = distinct-mv eq

    distinct-mv : ¬ just (ƛ (var zero) []) ≈mv
                    just (ƛ (var zero) [])
    distinct-mv (just eq) = distinct-v eq

    distinct-v : ¬ ƛ (var zero) [] ≈v ƛ (var zero) []
    distinct-v (ƛ eq) = distinct-c (eq (ƛ (var zero) []))

  distinct-t : ¬ ƛ (var zero) ≈t (Tm 0 ∋ ƛ (var zero))
  distinct-t eq = distinct-c (eq [])

------------------------------------------------------------------------
-- Applicative bisimilarity

infix 4 _≈mv_ _≈v_

-- _≈mv_, _≈c_ and _≈v_ are defined mutually (coinductively).

data _≈v_ : Value → Value → Set

-- Equivalence of possibly exceptional values.

_≈mv_ : Maybe Value → Maybe Value → Set
_≈mv_ = Maybe.Pointwise _≈v_

-- Equivalence of computations.

open module EA = Partiality.Equality _≈mv_
  using () renaming (_≈_ to _≈c_)

-- Equivalence of values.

data _≈v_ where
  con : ∀ {i} → con i ≈v con i
  ƛ   : ∀ {n₁} {t₁ : Tm (1 + n₁)} {ρ₁} {n₂} {t₂ : Tm (1 + n₂)} {ρ₂}
        (t₁≈t₂ : ∀ v → ∞ (⟦ t₁ ⟧ (v ∷ ρ₁) ≈c ⟦ t₂ ⟧ (v ∷ ρ₂))) →
        ƛ t₁ ρ₁ ≈v ƛ t₂ ρ₂

-- Applicative bisimilarity.

infix 4 _≈t_

_≈t_ : ∀ {n} → Tm n → Tm n → Set
t₁ ≈t t₂ = ∀ ρ → ⟦ t₁ ⟧ ρ ≈c ⟦ t₂ ⟧ ρ

-- Applicative bisimilarity is reflexive.

mutual

  infix 3 _∎mv _∎c _∎v

  _∎mv : (v : Maybe Value) → v ≈mv v
  just v  ∎mv = just (v ∎v)
  nothing ∎mv = nothing

  _∎c : (x : Maybe Value ⊥) → x ≈c x
  now mv  ∎c = EA.now (mv ∎mv)
  later x ∎c = EA.later (♯ (♭ x ∎c))

  _∎v : (v : Value) → v ≈v v
  con i ∎v = con
  ƛ t ρ ∎v = ƛ (λ v → ♯ (⟦ t ⟧ (v ∷ ρ) ∎c))

infix 3 _∎t

_∎t : ∀ {n} (t : Tm n) → t ≈t t
t ∎t = λ ρ → ⟦ t ⟧ ρ ∎c

-- Applicative bisimilarity is symmetric.

mutual

  sym-mv : ∀ {v₁ v₂} → v₁ ≈mv v₂ → v₂ ≈mv v₁
  sym-mv (just v₁≈v₂) = just (sym-v v₁≈v₂)
  sym-mv nothing      = nothing

  sym-c : ∀ {x₁ x₂} → x₁ ≈c x₂ → x₂ ≈c x₁
  sym-c (EA.now v₁≈v₂)    = EA.now (sym-mv v₁≈v₂)
  sym-c (EA.later  x₁≈x₂) = EA.later (♯ sym-c (♭ x₁≈x₂))
  sym-c (EA.laterˡ x₁≈x₂) = EA.laterʳ  (sym-c    x₁≈x₂)
  sym-c (EA.laterʳ x₁≈x₂) = EA.laterˡ  (sym-c    x₁≈x₂)

  sym-v : ∀ {v₁ v₂} → v₁ ≈v v₂ → v₂ ≈v v₁
  sym-v con       = con
  sym-v (ƛ t₁≈t₂) = ƛ (λ v → ♯ sym-c (♭ (t₁≈t₂ v)))

sym-t : ∀ {n} {t₁ t₂ : Tm n} → t₁ ≈t t₂ → t₂ ≈t t₁
sym-t t₁≈t₂ = λ ρ → sym-c (t₁≈t₂ ρ)

-- Applicative bisimilarity is transitive.

mutual

  trans-mv : ∀ {v₁ v₂ v₃} → v₁ ≈mv v₂ → v₂ ≈mv v₃ → v₁ ≈mv v₃
  trans-mv (just v₁≈v₂) (just v₂≈v₃) = just (trans-v v₁≈v₂ v₂≈v₃)
  trans-mv nothing      nothing      = nothing

  private

    now-trans-c : ∀ {x₁ x₂ v₃} → x₁ ≈c x₂ → x₂ ≈c now v₃ → x₁ ≈c now v₃
    now-trans-c (EA.now    v₁≈v₂) (EA.now    v₂≈v₃) = EA.now (trans-mv       v₁≈v₂   v₂≈v₃)
    now-trans-c (EA.laterˡ x₁≈x₂)            x₂≈v₃  = EA.laterˡ (now-trans-c x₁≈x₂   x₂≈v₃)
    now-trans-c            x₁≈lx₂ (EA.laterˡ x₂≈v₃) = now-trans-c (laterʳ⁻¹  x₁≈lx₂) x₂≈v₃

    later-trans-c : ∀ {x₁ x₂ x₃} →
                    x₁ ≈c x₂ → x₂ ≈c later x₃ → x₁ ≈c later x₃
    later-trans-c (EA.later  x₁≈x₂)        lx₂≈lx₃ = EA.later  (♯ trans-c (♭ x₁≈x₂) (later⁻¹  lx₂≈lx₃))
    later-trans-c (EA.laterˡ x₁≈x₂)         x₂≈lx₃ = EA.later  (♯ trans-c    x₁≈x₂  (laterʳ⁻¹  x₂≈lx₃))
    later-trans-c (EA.laterʳ x₁≈x₂)        lx₂≈lx₃ =        later-trans-c    x₁≈x₂  (laterˡ⁻¹ lx₂≈lx₃)
    later-trans-c         x₁≈x₂  (EA.laterʳ x₂≈x₃) = EA.laterʳ (  trans-c    x₁≈x₂             x₂≈x₃ )

  trans-c : ∀ {x₁ x₂ x₃} → x₁ ≈c x₂ → x₂ ≈c x₃ → x₁ ≈c x₃
  trans-c {x₃ = now   v₃} x₁≈x₂ x₂≈v₃  = now-trans-c   x₁≈x₂ x₂≈v₃
  trans-c {x₃ = later z₃} x₁≈x₂ x₂≈lx₃ = later-trans-c x₁≈x₂ x₂≈lx₃

  trans-v : ∀ {v₁ v₂ v₃} → v₁ ≈v v₂ → v₂ ≈v v₃ → v₁ ≈v v₃
  trans-v con       con       = con
  trans-v (ƛ t₁≈t₂) (ƛ t₂≈t₃) =
    ƛ (λ v → ♯ trans-c (♭ (t₁≈t₂ v)) (♭ (t₂≈t₃ v)))

trans-t : ∀ {n} {t₁ t₂ t₃ : Tm n} → t₁ ≈t t₂ → t₂ ≈t t₃ → t₁ ≈t t₃
trans-t t₁≈t₂ t₂≈t₃ = λ ρ → trans-c (t₁≈t₂ ρ) (t₂≈t₃ ρ)

-- Bind preserves applicative bisimilarity.

infixl 1 _>>=-cong-c_

_>>=-cong-c_ : ∀ {x₁ x₂ f₁ f₂} →
               x₁ ≈c x₂ → (∀ {v₁ v₂} → v₁ ≈v v₂ → f₁ v₁ ≈c f₂ v₂) →
               (x₁ >>= f₁) ≈c (x₂ >>= f₂)
_>>=-cong-c_ {f₁ = f₁} {f₂} x₁≈x₂ f₁≈f₂ =
  Partiality._>>=-cong_ x₁≈x₂ helper
  where
  helper : ∀ {mv₁ mv₂} → mv₁ ≈mv mv₂ →
           maybe f₁ fail mv₁ ≈c maybe f₂ fail mv₂
  helper nothing      = EA.now nothing
  helper (just v₁≈v₂) = f₁≈f₂ v₁≈v₂

-- _≈!_ is stronger than applicative bisimilarity.

≈!⇒≈t : ∀ {n} {t₁ t₂ : Tm n} → t₁ ≈! t₂ → t₁ ≈t t₂
≈!⇒≈t t₁≈t₂ = λ ρ →
  Partiality.map (λ {v₁} v₁≡v₂ → P.subst (_≈mv_ v₁) v₁≡v₂ (v₁ ∎mv))
                 (t₁≈t₂ ρ)

¬≈t⇒≈! : ¬ ((t₁ t₂ : Tm 0) → t₁ ≈t t₂ → t₁ ≈! t₂)
¬≈t⇒≈! hyp with hyp t₁ t₂ bisimilar []
  where
  t₁ : Tm 0
  t₁ = ƛ (ƛ (vr 0)) · con 0

  t₂ : Tm 0
  t₂ = ƛ (vr 0)

  bisimilar : t₁ ≈t t₂
  bisimilar [] =
    EA.laterˡ (EA.now (just (ƛ (λ v → ♯ (return v ∎c)))))
... | laterˡ (now ())

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.Role using ( Role ; ⟨_⟩ ; ⟨_⟩⁻¹ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using ( Interp ; Δ ; rol ; _⊨_≈_ ; rol-≈ ; ≈-refl ; ≈-sym )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( _≲_ ; _≃_ ; ≲-resp-rol ; ≲-image² ; ≃-image ; ≃-image⁻¹ ; ≃-image² ;  ≃-image²⁻¹ ; ≃-impl-≲ ; ≃-iso⁻¹ )
open import Web.Semantic.Util using ( Subset ; _⁻¹ )

module Web.Semantic.DL.Role.Model {Σ : Signature} where

_⟦_⟧₂ : ∀ (I : Interp Σ) → Role Σ → Subset (Δ I × Δ I)
I ⟦ ⟨ r ⟩   ⟧₂ = rol I r
I ⟦ ⟨ r ⟩⁻¹ ⟧₂ = (rol I r)⁻¹

⟦⟧₂-resp-≈ : ∀ I R {w x y z} →
  (I ⊨ w ≈ x) → ((x , y) ∈ I ⟦ R ⟧₂) → (I ⊨ y ≈ z) → ((w , z) ∈ I ⟦ R ⟧₂)
⟦⟧₂-resp-≈ I ⟨ r ⟩   w≈x xy∈⟦r⟧ y≈z = rol-≈ I r w≈x xy∈⟦r⟧ y≈z
⟦⟧₂-resp-≈ I ⟨ r ⟩⁻¹ w≈x yx∈⟦r⟧ y≈z = rol-≈ I r (≈-sym I y≈z) yx∈⟦r⟧ (≈-sym I w≈x)

⟦⟧₂-resp-≲ : ∀ {I J : Interp Σ} → (I≲J : I ≲ J) → ∀ {xy} R →
  (xy ∈ I ⟦ R ⟧₂) → (≲-image² I≲J xy ∈ J ⟦ R ⟧₂)
⟦⟧₂-resp-≲ I≲J {x , y} ⟨ r ⟩   xy∈⟦r⟧ = ≲-resp-rol I≲J xy∈⟦r⟧
⟦⟧₂-resp-≲ I≲J {x , y} ⟨ r ⟩⁻¹ yx∈⟦r⟧ = ≲-resp-rol I≲J yx∈⟦r⟧

⟦⟧₂-resp-≃ : ∀ {I J : Interp Σ} → (I≃J : I ≃ J) → ∀ {xy} R →
  (xy ∈ I ⟦ R ⟧₂) → (≃-image² I≃J xy ∈ J ⟦ R ⟧₂)
⟦⟧₂-resp-≃ I≃J = ⟦⟧₂-resp-≲ (≃-impl-≲ I≃J)

⟦⟧₂-refl-≃ : ∀ {I J : Interp Σ} → (I≃J : I ≃ J) → ∀ {xy} R →
  (≃-image²⁻¹ I≃J xy ∈ I ⟦ R ⟧₂) → (xy ∈ J ⟦ R ⟧₂)
⟦⟧₂-refl-≃ {I} {J} I≃J {x , y} R xy∈⟦R⟧ =
  ⟦⟧₂-resp-≈ J R (≈-sym J (≃-iso⁻¹ I≃J x))
    (⟦⟧₂-resp-≃ I≃J R xy∈⟦R⟧) (≃-iso⁻¹ I≃J y)

⟦⟧₂-galois : ∀ {I J : Interp Σ} → (I≃J : I ≃ J) → ∀ {x y} R →
  ((≃-image⁻¹ I≃J x , y) ∈ I ⟦ R ⟧₂) → ((x , ≃-image I≃J y) ∈ J ⟦ R ⟧₂)
⟦⟧₂-galois {I} {J} I≃J {x} R xy∈⟦R⟧ =
  ⟦⟧₂-resp-≈ J R (≈-sym J (≃-iso⁻¹ I≃J x))
    (⟦⟧₂-resp-≲ (≃-impl-≲ I≃J) R xy∈⟦R⟧)
    (≈-refl J)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
-- Andreas, 2017-07-13, issue #2645

-- Agda accepted this definition:

record S : Set₁ where
  postulate
    field
      f : Set  -- Now: error raised here

s : Set → S
s A = record {f = A }


text:
-- Σ type (also used as existential) and
-- cartesian product (also used as conjunction).

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

module Tools.Product where

open import Data.Product public using (Σ; ∃; ∃₂; _×_; _,_; proj₁; proj₂)

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt