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

module Examples.New where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; subst)

open import Singleton
open import PiPointedFrac

------------------------------------------------------------------------------
-- Conventional PI examples

𝔹 : 𝕌
𝔹 = 𝟙 +ᵤ 𝟙

𝔹² : 𝕌
𝔹² = 𝔹 ×ᵤ 𝔹

𝔽 𝕋 : ⟦ 𝔹 ⟧
𝔽 = inj₁ tt
𝕋 = inj₂ tt

NOT : 𝔹 ⟷ 𝔹
NOT = swap₊

NEG1 NEG2 NEG3 NEG4 NEG5 : 𝔹 ⟷ 𝔹
NEG1 = swap₊
NEG2 = id⟷ ⊚ NOT
NEG3 = NOT ⊚ NOT ⊚ NOT
NEG4 = NOT ⊚ id⟷
NEG5 = uniti⋆l ⊚ swap⋆ ⊚ (NOT ⊗ id⟷) ⊚ swap⋆ ⊚ unite⋆l
NEG6 = uniti⋆r ⊚ (NOT ⊗ id⟷) ⊚ unite⋆r

CONTROL : {A : 𝕌} → (A ⟷ A) → (𝔹 ×ᵤ A ⟷ 𝔹 ×ᵤ A)
CONTROL f = dist ⊚ (id⟷ ⊕ (id⟷ ⊗ f)) ⊚ factor

CNOT : 𝔹² ⟷ 𝔹²
CNOT = CONTROL NOT

TOFFOLI : 𝔹 ×ᵤ 𝔹² ⟷ 𝔹 ×ᵤ 𝔹²
TOFFOLI = CONTROL (CONTROL NOT)

PERES : (𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹 ⟷ (𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹
PERES = (id⟷ ⊗ NOT) ⊚ assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ swap⋆) ⊚ (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚ assocl⋆

SWAP12 SWAP23 SWAP13 ROTL ROTR : 𝟙 +ᵤ 𝟙 +ᵤ 𝟙 ⟷ 𝟙 +ᵤ 𝟙 +ᵤ 𝟙
SWAP12 = assocl₊ ⊚ (swap₊ ⊕ id⟷) ⊚ assocr₊
SWAP23 = id⟷ ⊕ swap₊
SWAP13 = SWAP23 ⊚ SWAP12 ⊚ SWAP23
ROTR   = SWAP12 ⊚ SWAP23
ROTL   = SWAP13 ⊚ SWAP23

------------------------------------------------------------------------------
-- Pointed versions

∙TOFFOLI-1 : ∀ {b₁ b₂} →
           (𝔹 ×ᵤ 𝔹²) # (𝔽 , (b₁ , b₂)) ∙⟶ (𝔹 ×ᵤ 𝔹²) # (𝔽 , (b₁ , b₂))
∙TOFFOLI-1 = ∙c TOFFOLI

∙TOFFOLI-2 : ∀ {b} →
           (𝔹 ×ᵤ 𝔹²) # (𝕋 , (𝔽 , b)) ∙⟶ (𝔹 ×ᵤ 𝔹²) # (𝕋 , (𝔽 , b))
∙TOFFOLI-2 = ∙c TOFFOLI

∙TOFFOLI-3 : ∀ {b} →
           (𝔹 ×ᵤ 𝔹²) # (𝕋 , (𝕋 , b)) ∙⟶ (𝔹 ×ᵤ 𝔹²) # (𝕋 , (𝕋 , eval swap₊ b))
∙TOFFOLI-3 = ∙c TOFFOLI

-- Ancilla examples from literature

-- Fig. 2 in Ricercar

fig2a : 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ⟷
        𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹
fig2a = CONTROL (CONTROL (CONTROL NOT))

-- first write the circuit with the additional ancilla

fig2b' : ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) ⟷ ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹)
fig2b' =
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ CONTROL (CONTROL NOT))  -- first ccnot
  ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷)                        -- move it back
  ⊚
  (assocl⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ swap⋆) ⊚
  (id⟷ ⊗ CONTROL (CONTROL NOT))  -- second ccnot
  ⊚
  (id⟷ ⊗ swap⋆) ⊚
  assocl⋆ ⊚
  (assocr⋆ ⊗ id⟷)                      -- move it back
  ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ CONTROL (CONTROL NOT))  -- third ccnot
  ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷)                        -- move it back

-- then prove a theorem that specifies its semantics

fig2b'≡ : (a b c d : ⟦ 𝔹 ⟧) →
          proj₂ (eval fig2b' ((a , b , c , d) , 𝔽)) ≡ 𝔽
fig2b'≡ a         (inj₁ tt) c d = refl
fig2b'≡ (inj₁ tt) (inj₂ tt) c d = refl
fig2b'≡ (inj₂ tt) (inj₂ tt) c d = refl

-- generalize above?  Method:
-- for 'dist' to evaluate, need to split on b first
--   in first case, split on e (same reason)
--   in second case, split on a (same reason)
--     split on e
--     split on e
foo : (a b c d e : ⟦ 𝔹 ⟧) →
          proj₂ (eval fig2b' ((a , b , c , d) , e)) ≡ e
foo a         (inj₁ x) c d (inj₁ x₁) = refl
foo a         (inj₁ x) c d (inj₂ y)  = refl
foo (inj₁ x)  (inj₂ y) c d (inj₁ x₁) = refl
foo (inj₁ x)  (inj₂ y) c d (inj₂ y₁) = refl
foo (inj₂ y₁) (inj₂ y) c d (inj₁ x)  = refl
foo (inj₂ y₁) (inj₂ y) c d (inj₂ y₂) = refl

{--
postulate
  -- boring...
  tensor4 : ∀ {a b c d e} →
          (● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ])  ×ᵤ ● 𝔹 [ e ] ⟷
          ● ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) [ (a , b , c , d) , e ]
  itensor4 : ∀ {a b c d e} →
          ● ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) [ (a , b , c , d) , e ] ⟷
          (● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ])  ×ᵤ ● 𝔹 [ e ]
--}
-- now lift it
{--
fig2b : ∀ {a b c d e} →
        let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
        in
           ● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ] ⟷
           ● 𝔹 [ x ] ×ᵤ ● 𝔹 [ y ] ×ᵤ ● 𝔹 [ z ] ×ᵤ ● 𝔹 [ w ]
fig2b {a} {b} {c} {d} {e} =
  let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
  in    uniti⋆r ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝟙[e]
        (id⟷ ⊗ η e) ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × (●𝔹[e] x ●1/𝔹[e])
        assocl⋆ ⊚
        -- ((●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝔹[e) x ●1/𝔹[e]
        (tensor4 ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (a,b,c,d),e ] x ●1/𝔹[e]
        (lift fig2b' ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (((== id⟷ (cong (λ H → ((x , y , z , w)) , H) (foo a b c d e))) ⊗ id⟷)) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (itensor4 ⊗ id⟷) ⊚
         -- ((●𝔹[x] × ●𝔹[y] × ●𝔹[z] × ●𝔹[w]) × ●𝔹[e]) x ●1/𝔹[e]
        assocr⋆ ⊚
        (id⟷ ⊗ ε e) ⊚
        unite⋆r
--}
{--
-- This is mostly to show that == is really 'subst' in hiding.
fig2b₂ : ∀ {a b c d e} →
        let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
        in
           ● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ] ⟷
           ● 𝔹 [ x ] ×ᵤ ● 𝔹 [ y ] ×ᵤ ● 𝔹 [ z ] ×ᵤ ● 𝔹 [ w ]
fig2b₂ {a} {b} {c} {d} {e} =
  let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
  in    uniti⋆r ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝟙[e]
        (id⟷ ⊗ η e) ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × (●𝔹[e] x ●1/𝔹[e])
        assocl⋆ ⊚
        -- ((●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝔹[e) x ●1/𝔹[e]
        (tensor4 ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (a,b,c,d),e ] x ●1/𝔹[e]
        (lift fig2b' ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (itensor4 ⊗ id⟷) ⊚
         -- ((●𝔹[x] × ●𝔹[y] × ●𝔹[z] × ●𝔹[w]) × ●𝔹[e]) x ●1/𝔹[e]
        assocr⋆ ⊚
        (id⟷ ⊗ (subst (λ ee → ● 𝔹 [ ee ] ×ᵤ 𝟙/● 𝔹 [ e ] ⟷ 𝟙) (sym (foo a b c d e)) (ε e))) ⊚
        unite⋆r
--}
-- Examples

infixr 2  _→⟨_⟩_
infix  3  _□

_→⟨_⟩_ : (T₁ : ∙𝕌) → {T₂ T₃ : ∙𝕌} →
          (T₁ ∙⟶ T₂) → (T₂ ∙⟶ T₃) → (T₁ ∙⟶ T₃)
_ →⟨ α ⟩ β = α ∙⊚ β

_□ : (T : ∙𝕌) → {T : ∙𝕌} → (T ∙⟶ T)
_□ T = ∙id⟷

zigzag : ∀ b → 𝔹 # b ∙⟶ 𝔹 # b
zigzag b =
  (𝔹 # b)
        →⟨ (∙c uniti⋆l) ⟩
  (𝟙 ×ᵤ 𝔹) # (tt , b)
        →⟨ ∙times# ⟩
  (𝟙 # tt) ∙×ᵤ (𝔹 # b)
        →⟨ ∙id⟷ ∙⊗ return (𝔹 # b) ⟩
  (𝟙 # tt) ∙×ᵤ (Singᵤ (𝔹 # b))
        →⟨ η (𝔹 # b) ∙⊗ ∙id⟷ ⟩
  ((Singᵤ (𝔹 # b)) ∙×ᵤ (Recipᵤ (𝔹 # b))) ∙×ᵤ (Singᵤ (𝔹 # b))
        →⟨ ∙assocr⋆ ⟩
  Singᵤ (𝔹 # b) ∙×ᵤ (Recipᵤ (𝔹 # b) ∙×ᵤ (Singᵤ (𝔹 # b)))
        →⟨ ∙id⟷ ∙⊗ ∙swap⋆ ⟩
  Singᵤ (𝔹 # b) ∙×ᵤ ((Singᵤ (𝔹 # b)) ∙×ᵤ (Recipᵤ (𝔹 # b)))
        →⟨ ∙id⟷ ∙⊗ ε (𝔹 # b) ⟩
  Singᵤ (𝔹 # b) ∙×ᵤ (𝟙 # tt)
        →⟨ extract (𝔹 # b) ∙⊗ ∙id⟷ ⟩
  (𝔹 # b) ∙×ᵤ (𝟙 # tt)
        →⟨ ∙#times  ⟩
  (𝔹 ×ᵤ 𝟙) # (b , tt)
        →⟨ ∙c unite⋆r  ⟩
  (𝔹 # b) □

test1 : proj₁ (∙eval (zigzag 𝔽)) 𝔽 ≡ 𝔽
test1 = proj₂ (∙eval (zigzag 𝔽))

test2 : proj₁ (∙eval (zigzag 𝕋)) 𝕋 ≡ 𝕋
test2 = proj₂ (∙eval (zigzag 𝕋))

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Terminating parser "combinator" interface
------------------------------------------------------------------------

-- Use RecursiveDescent.Hybrid.Simple to actually run the parsers.

module RecursiveDescent.Hybrid where

open import RecursiveDescent.Index
import RecursiveDescent.Hybrid.Type as P
open P public using (Parser; Grammar)

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

------------------------------------------------------------------------
-- Exported combinators

infix  60 !_
infixl 40 _∣_
infixl 10 _>>=_ _!>>=_

!_ : forall {tok nt e c r} ->
     nt (e , c) r -> Parser tok nt (e , step c) r
!_ = P.!_

symbol : forall {tok nt} -> Parser tok nt 0I tok
symbol = P.symbol

return : forall {tok nt r} -> r -> Parser tok nt 1I r
return = P.return

fail : forall {tok nt r} -> Parser tok nt 0I r
fail = P.fail

_>>=_ : forall {tok nt e₁ c₁ i₂ r₁ r₂} -> let i₁ = (e₁ , c₁) in
        Parser tok nt i₁ r₁ ->
        (r₁ -> Parser tok nt i₂ r₂) ->
        Parser tok nt (i₁ ·I i₂) r₂
_>>=_ {e₁ = true } = P._?>>=_
_>>=_ {e₁ = false} = P._!>>=_

-- If the first parser is guaranteed to consume something, then the
-- second parser's index can depend on the result of the first parser.

_!>>=_ : forall {tok nt c₁ r₁ r₂} {i₂ : r₁ -> Index} ->
         let i₁ = (false , c₁) in
         Parser tok nt i₁ r₁ ->
         ((x : r₁) -> Parser tok nt (i₂ x) r₂) ->
         Parser tok nt (i₁ ·I 1I) r₂
_!>>=_ = P._!>>=_

_∣_ : forall {tok nt e₁ c₁ i₂ r} -> let i₁ = (e₁ , c₁) in
      Parser tok nt i₁ r ->
      Parser tok nt i₂ r ->
      Parser tok nt (i₁ ∣I i₂) r
_∣_ = P.alt _ _

cast : forall {tok nt e₁ e₂ c₁ c₂ r} ->
       e₁ ≡ e₂ -> c₁ ≡ c₂ ->
       Parser tok nt (e₁ , c₁) r -> Parser tok nt (e₂ , c₂) r
cast refl refl p = p

ext: agda

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------------
-- Testing Agda internal term: @Lam@
------------------------------------------------------------------------------

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

-- The following conjecture uses the internal Agda term @Lam@.

module Agda.InternalTerms.LamTerm where

postulate
  D : Set
  ∃ : (D → Set) → Set  -- The existential quantifier type on D.
  A : D → Set

postulate ∃-intro : (t : D) → A t → ∃ A
{-# ATP prove ∃-intro #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a strict partial order.

module Relation.Binary.Product.StrictLex where

open import Function
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Level
open import Relation.Nullary.Product
open import Relation.Nullary.Sum
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Product.Pointwise as Pointwise
  using (_×-Rel_)
open import Relation.Nullary

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

  ×-Lex : (_≈₁_ _<₁_ : Rel A₁ ℓ₁) → (_≤₂_ : Rel A₂ ℓ₂) →
          Rel (A₁ × A₂) _
  ×-Lex _≈₁_ _<₁_ _≤₂_ =
    (_<₁_ on proj₁) -⊎- (_≈₁_ on proj₁) -×- (_≤₂_ on proj₂)

  -- Some properties which are preserved by ×-Lex (under certain
  -- assumptions).

  ×-reflexive : ∀ _≈₁_ _∼₁_ {_≈₂_ : Rel A₂ ℓ₂} _≤₂_ →
                _≈₂_ ⇒ _≤₂_ → (_≈₁_ ×-Rel _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
  ×-reflexive _ _ _ refl₂ = λ x≈y →
    inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))

  _×-irreflexive_ : ∀ {_≈₁_ _<₁_}             → Irreflexive _≈₁_ _<₁_ →
                    ∀ {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Irreflexive _≈₂_ _<₂_ →
                    Irreflexive (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  (ir₁ ×-irreflexive ir₂) x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
  (ir₁ ×-irreflexive ir₂) x≈y (inj₂ x≈<y)  =
    ir₂ (proj₂ x≈y) (proj₂ x≈<y)

  ×-transitive :
    ∀ {_≈₁_ _<₁_} →
    IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ → Transitive _<₁_ →
    ∀ {_≤₂_} →
    Transitive _≤₂_ →
    Transitive (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-transitive {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} eq₁ resp₁ trans₁
               {_≤₂_ = _≤₂_} trans₂ {x} {y} {z} = trans {x} {y} {z}
    where
    module Eq₁ = IsEquivalence eq₁

    trans : Transitive (×-Lex _≈₁_ _<₁_ _≤₂_)
    trans (inj₁ x₁<y₁) (inj₁ y₁<z₁) = inj₁ (trans₁ x₁<y₁ y₁<z₁)
    trans (inj₁ x₁<y₁) (inj₂ y≈≤z)  =
      inj₁ (proj₁ resp₁ (proj₁ y≈≤z) x₁<y₁)
    trans (inj₂ x≈≤y)  (inj₁ y₁<z₁) =
      inj₁ (proj₂ resp₁ (Eq₁.sym $ proj₁ x≈≤y) y₁<z₁)
    trans (inj₂ x≈≤y)  (inj₂ y≈≤z)  =
      inj₂ ( Eq₁.trans (proj₁ x≈≤y) (proj₁ y≈≤z)
           , trans₂    (proj₂ x≈≤y) (proj₂ y≈≤z) )

  ×-antisymmetric :
    ∀ {_≈₁_ _<₁_} →
    Symmetric _≈₁_ → Irreflexive _≈₁_ _<₁_ → Asymmetric _<₁_ →
    ∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} →
    Antisymmetric _≈₂_ _≤₂_ →
    Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-antisymmetric {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} sym₁ irrefl₁ asym₁
                  {_≈₂_ = _≈₂_} {_≤₂_ = _≤₂_} antisym₂ {x} {y} =
    antisym {x} {y}
    where
    antisym : Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _≤₂_)
    antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) = ⊥-elim $ asym₁ x₁<y₁ y₁<x₁
    antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  = ⊥-elim $ irrefl₁ (sym₁ $ proj₁ y≈≤x) x₁<y₁
    antisym (inj₂ x≈≤y)  (inj₁ y₁<x₁) = ⊥-elim $ irrefl₁ (sym₁ $ proj₁ x≈≤y) y₁<x₁
    antisym (inj₂ x≈≤y)  (inj₂ y≈≤x)  =
      proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)

  ×-asymmetric :
    ∀ {_≈₁_ _<₁_} →
    Symmetric _≈₁_ → _<₁_ Respects₂ _≈₁_ → Asymmetric _<₁_ →
    ∀ {_<₂_} →
    Asymmetric _<₂_ →
    Asymmetric (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-asymmetric {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} sym₁ resp₁ asym₁
               {_<₂_ = _<₂_} asym₂ {x} {y} = asym {x} {y}
    where
    irrefl₁ : Irreflexive _≈₁_ _<₁_
    irrefl₁ = asym⟶irr resp₁ sym₁ asym₁

    asym : Asymmetric (×-Lex _≈₁_ _<₁_ _<₂_)
    asym (inj₁ x₁<y₁) (inj₁ y₁<x₁) = asym₁ x₁<y₁ y₁<x₁
    asym (inj₁ x₁<y₁) (inj₂ y≈<x)  = irrefl₁ (sym₁ $ proj₁ y≈<x) x₁<y₁
    asym (inj₂ x≈<y)  (inj₁ y₁<x₁) = irrefl₁ (sym₁ $ proj₁ x≈<y) y₁<x₁
    asym (inj₂ x≈<y)  (inj₂ y≈<x)  = asym₂ (proj₂ x≈<y) (proj₂ y≈<x)

  ×-≈-respects₂ :
    ∀ {_≈₁_ _<₁_} → IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ →
    {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → _<₂_ Respects₂ _≈₂_ →
    (×-Lex _≈₁_ _<₁_ _<₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_)
  ×-≈-respects₂ {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} eq₁ resp₁
                {_≈₂_ = _≈₂_} {_<₂_ = _<₂_}     resp₂ =
    (λ {x y z} → resp¹ {x} {y} {z}) ,
    (λ {x y z} → resp² {x} {y} {z})
    where
    _<_ = ×-Lex _≈₁_ _<₁_ _<₂_

    open IsEquivalence eq₁ renaming (sym to sym₁; trans to trans₁)

    resp¹ : ∀ {x} → (_<_ x) Respects (_≈₁_ ×-Rel _≈₂_)
    resp¹ y≈y' (inj₁ x₁<y₁) = inj₁ (proj₁ resp₁ (proj₁ y≈y') x₁<y₁)
    resp¹ y≈y' (inj₂ x≈<y)  =
      inj₂ ( trans₁ (proj₁ x≈<y) (proj₁ y≈y')
           , proj₁ resp₂ (proj₂ y≈y') (proj₂ x≈<y) )

    resp² : ∀ {y} → (flip _<_ y) Respects (_≈₁_ ×-Rel _≈₂_)
    resp² x≈x' (inj₁ x₁<y₁) = inj₁ (proj₂ resp₁ (proj₁ x≈x') x₁<y₁)
    resp² x≈x' (inj₂ x≈<y)  =
      inj₂ ( trans₁ (sym₁ $ proj₁ x≈x') (proj₁ x≈<y)
           , proj₂ resp₂ (proj₂ x≈x') (proj₂ x≈<y) )

  ×-decidable : ∀ {_≈₁_ _<₁_} → Decidable _≈₁_ → Decidable _<₁_ →
                ∀ {_≤₂_} → Decidable _≤₂_ →
                Decidable (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-decidable dec-≈₁ dec-<₁ dec-≤₂ = λ x y →
    dec-<₁ (proj₁ x) (proj₁ y)
      ⊎-dec
    (dec-≈₁ (proj₁ x) (proj₁ y)
       ×-dec
     dec-≤₂ (proj₂ x) (proj₂ y))

  ×-total : ∀ {_≈₁_ _<₁_} → Total _<₁_ →
            ∀ {_≤₂_} →
            Total (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-total {_≈₁_ = _≈₁_} {_<₁_ = _<₁_} total₁ {_≤₂_ = _≤₂_} = total
    where
    total : Total (×-Lex _≈₁_ _<₁_ _≤₂_)
    total x y with total₁ (proj₁ x) (proj₁ y)
    ... | inj₁ x₁<y₁ = inj₁ (inj₁ x₁<y₁)
    ... | inj₂ x₁>y₁ = inj₂ (inj₁ x₁>y₁)

  ×-compare :
    {_≈₁_ _<₁_ : Rel A₁ ℓ₁} → Symmetric _≈₁_ → Trichotomous _≈₁_ _<₁_ →
    {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Trichotomous _≈₂_ _<₂_ →
    Trichotomous (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-compare {_≈₁_} {_<₁_} sym₁ compare₁ {_≈₂_} {_<₂_} compare₂ = cmp
    where
    cmp″ : ∀ {x₁ y₁ x₂ y₂} →
           ¬ (x₁ <₁ y₁) → x₁ ≈₁ y₁ → ¬ (y₁ <₁ x₁) →
           Tri (x₂ <₂ y₂) (x₂ ≈₂ y₂) (y₂ <₂ x₂) →
           Tri (×-Lex _≈₁_ _<₁_ _<₂_ (x₁ , x₂) (y₁ , y₂))
               ((_≈₁_ ×-Rel _≈₂_) (x₁ , x₂) (y₁ , y₂))
               (×-Lex _≈₁_ _<₁_ _<₂_ (y₁ , y₂) (x₁ , x₂))
    cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (tri< x₂<y₂ x₂≉y₂ x₂≯y₂) =
      tri< (inj₂ (x₁≈y₁ , x₂<y₂))
           (x₂≉y₂ ∘ proj₂)
           [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
    cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (tri> x₂≮y₂ x₂≉y₂ x₂>y₂) =
      tri> [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
           (x₂≉y₂ ∘ proj₂)
           (inj₂ (sym₁ x₁≈y₁ , x₂>y₂))
    cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (tri≈ x₂≮y₂ x₂≈y₂ x₂≯y₂) =
      tri≈ [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
           (x₁≈y₁ , x₂≈y₂)
           [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]

    cmp′ : ∀ {x₁ y₁} → Tri (x₁ <₁ y₁) (x₁ ≈₁ y₁) (y₁ <₁ x₁) →
           ∀ x₂ y₂ →
           Tri (×-Lex _≈₁_ _<₁_ _<₂_ (x₁ , x₂) (y₁ , y₂))
               ((_≈₁_ ×-Rel _≈₂_) (x₁ , x₂) (y₁ , y₂))
               (×-Lex _≈₁_ _<₁_ _<₂_ (y₁ , y₂) (x₁ , x₂))
    cmp′ (tri< x₁<y₁ x₁≉y₁ x₁≯y₁) x₂ y₂ =
      tri< (inj₁ x₁<y₁) (x₁≉y₁ ∘ proj₁) [ x₁≯y₁ , x₁≉y₁ ∘ sym₁ ∘ proj₁ ]
    cmp′ (tri> x₁≮y₁ x₁≉y₁ x₁>y₁) x₂ y₂ =
      tri> [ x₁≮y₁ , x₁≉y₁ ∘ proj₁ ] (x₁≉y₁ ∘ proj₁) (inj₁ x₁>y₁)
    cmp′ (tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁) x₂ y₂ =
      cmp″ x₁≮y₁ x₁≈y₁ x₁≯y₁ (compare₂ x₂ y₂)

    cmp : Trichotomous (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
    cmp (x₁ , x₂) (y₁ , y₂) = cmp′ (compare₁ x₁ y₁) x₂ y₂

  -- Some collections of properties which are preserved by ×-Lex.

  _×-isPreorder_ : ∀ {_≈₁_ _∼₁_} → IsPreorder _≈₁_ _∼₁_ →
                   ∀ {_≈₂_ _∼₂_} → IsPreorder _≈₂_ _∼₂_ →
                   IsPreorder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _∼₁_ _∼₂_)
  _×-isPreorder_ {_≈₁_ = _≈₁_} {_∼₁_ = _∼₁_} pre₁ {_∼₂_ = _∼₂_} pre₂ =
    record
      { isEquivalence = Pointwise._×-isEquivalence_
                          (isEquivalence pre₁) (isEquivalence pre₂)
      ; reflexive     = λ {x y} →
                        ×-reflexive _≈₁_ _∼₁_ _∼₂_ (reflexive pre₂)
                                    {x} {y}
      ; trans         = λ {x y z} →
                        ×-transitive
                          (isEquivalence pre₁) (∼-resp-≈ pre₁)
                          (trans pre₁) {_≤₂_ = _∼₂_} (trans pre₂)
                          {x} {y} {z}
      }
    where open IsPreorder

  _×-isStrictPartialOrder_ :
    ∀ {_≈₁_ _<₁_} → IsStrictPartialOrder _≈₁_ _<₁_ →
    ∀ {_≈₂_ _<₂_} → IsStrictPartialOrder _≈₂_ _<₂_ →
    IsStrictPartialOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  _×-isStrictPartialOrder_ {_<₁_ = _<₁_} spo₁ {_<₂_ = _<₂_} spo₂ =
    record
      { isEquivalence = Pointwise._×-isEquivalence_
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; irrefl        = λ {x y} →
                        _×-irreflexive_ {_<₁_ = _<₁_} (irrefl spo₁)
                                        {_<₂_ = _<₂_} (irrefl spo₂)
                                        {x} {y}
      ; trans         = λ {x y z} →
                        ×-transitive
                          {_<₁_ = _<₁_} (isEquivalence spo₁)
                                        (<-resp-≈ spo₁) (trans spo₁)
                          {_≤₂_ = _<₂_} (trans spo₂) {x} {y} {z}
      ; <-resp-≈      = ×-≈-respects₂ (isEquivalence spo₁)
                                      (<-resp-≈ spo₁)
                                      (<-resp-≈ spo₂)
      }
    where open IsStrictPartialOrder

  _×-isStrictTotalOrder_ :
    ∀ {_≈₁_ _<₁_} → IsStrictTotalOrder _≈₁_ _<₁_ →
    ∀ {_≈₂_ _<₂_} → IsStrictTotalOrder _≈₂_ _<₂_ →
    IsStrictTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  _×-isStrictTotalOrder_ {_<₁_ = _<₁_} spo₁ {_<₂_ = _<₂_} spo₂ =
    record
      { isEquivalence = Pointwise._×-isEquivalence_
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; trans         = λ {x y z} →
                        ×-transitive
                          {_<₁_ = _<₁_} (isEquivalence spo₁)
                                        (<-resp-≈ spo₁) (trans spo₁)
                          {_≤₂_ = _<₂_} (trans spo₂) {x} {y} {z}
      ; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
                                                (compare spo₂)
      ; <-resp-≈      = ×-≈-respects₂ (isEquivalence spo₁)
                                      (<-resp-≈ spo₁)
                                      (<-resp-≈ spo₂)
      }
    where open IsStrictTotalOrder

-- "Packages" (e.g. preorders) can also be combined.

_×-preorder_ :
  ∀ {p₁ p₂ p₃ p₄} →
  Preorder p₁ p₂ _ → Preorder p₃ p₄ _ → Preorder _ _ _
p₁ ×-preorder p₂ = record
  { isPreorder = isPreorder p₁ ×-isPreorder isPreorder p₂
  } where open Preorder

_×-strictPartialOrder_ :
  ∀ {s₁ s₂ s₃ s₄} →
  StrictPartialOrder s₁ s₂ _ → StrictPartialOrder s₃ s₄ _ →
  StrictPartialOrder _ _ _
s₁ ×-strictPartialOrder s₂ = record
  { isStrictPartialOrder = isStrictPartialOrder s₁
                             ×-isStrictPartialOrder
                           isStrictPartialOrder s₂
  } where open StrictPartialOrder

_×-strictTotalOrder_ :
  ∀ {s₁ s₂ s₃ s₄} →
  StrictTotalOrder s₁ s₂ _ → StrictTotalOrder s₃ s₄ _ →
  StrictTotalOrder _ _ _
s₁ ×-strictTotalOrder s₂ = record
  { isStrictTotalOrder = isStrictTotalOrder s₁
                           ×-isStrictTotalOrder
                         isStrictTotalOrder s₂
  } where open StrictTotalOrder


text:
record R : Set₁ where
  field
    A     : Set
    {B}   : Set
    {{C}} : Set

open R

r : R
r = {!!}
-- C-c C-c produced
-- A r = {!!}
-- B {r} = {!!}
-- C {{r}} = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Example where

open import Bool
open import Nat hiding (_==_; _+_)
open import AC

open Provable

infix 40 _+_
infix 30 _==_

postulate
  X : Set
  _==_ : X -> X -> Set
  |0|  : X
  _+_  : X -> X -> X
  refl  : forall {x}     -> x == x
  sym   : forall {x y}   -> x == y -> y == x
  trans : forall {x y z} -> x == y -> y == z -> x == z
  idL   : forall {x}     -> |0| + x == x
  idR   : forall {x}     -> x + |0| == x
  comm  : forall {x y}   -> x + y == y + x
  assoc : forall {x y z} -> x + (y + z) == (x + y) + z
  congL : forall {x y z} -> y == z -> x + y == x + z
  congR : forall {x y z} -> x == y -> x + z == y + z

open Semantics
      _==_ _+_ |0| refl sym trans idL idR
      comm assoc congL congR

thm = theorem 11 \a b c d e f g h i j k ->
      j ○ (k ○ (((((h ○ (e ○ ((e ○ (a ○ (a ○ (b ○ ((c ○ (((c ○ (d ○ d)) ○ (((d
      ○ (d ○ ((d ○ ((e ○ k) ○ ((((a ○ b) ○ (((h ○ (k ○ f)) ○ (((d ○ ((j ○ (h ○
      (a ○ (((g ○ (k ○ g)) ○ ((b ○ (i ○ (i ○ ((i ○ ((k ○ (d ○ (b ○ ((b ○ ((h ○
      k) ○ e)) ○ a)))) ○ j)) ○ a)))) ○ i)) ○ h)))) ○ (g ○ h))) ○ f) ○ h)) ○ b))
      ○ f) ○ f))) ○ (e ○ d)))) ○ d) ○ c)) ○ c)) ○ b))))) ○ (((a ○ a) ○ k) ○
      e)))) ○ c) ○ h) ○ (d ○ a)) ○ (c ○ a)))
      ≡
      (j ○ (k ○ (((h ○ (h ○ e)) ○ ((((e ○ (((a ○ (b ○ ((b ○ c) ○ (((d ○ d) ○
      ((d ○ d) ○ ((((e ○ (e ○ (f ○ f))) ○ (((a ○ ((b ○ (h ○ (k ○ (h ○ ((f ○ ((h
      ○ ((h ○ (a ○ ((k ○ (g ○ (b ○ (k ○ ((((a ○ (((e ○ h) ○ k) ○ b)) ○ b) ○ d)
      ○ j))))) ○ ((((a ○ i) ○ i) ○ i) ○ i)))) ○ ((g ○ h) ○ g))) ○ (j ○ d))) ○
      f))))) ○ b)) ○ k) ○ d)) ○ d) ○ d))) ○ ((c ○ c) ○ c))))) ○ (a ○ a)) ○ a))
      ○ (k ○ e)) ○ c) ○ d)) ○ a))) ○ (c ○ a)

test = prove thm

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Level
open import Ordinals
module filter {n : Level } (O : Ordinals {n})   where

open import zf
open import logic
import OD

open import Relation.Nullary
open import Data.Empty
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
import BAlgbra

open BAlgbra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom

import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

import ODC
open ODC O

open _∧_
open _∨_
open Bool

-- Kunen p.76 and p.53, we use ⊆
record Filter  ( L : HOD  ) : Set (suc n) where
   field
       filter : HOD
       f⊆PL :  filter ⊆ Power L
       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)

open Filter

record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter P ∋ od∅)
       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )

record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter P ∋ od∅)
       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )

open _⊆_

∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )

∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }

∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }

q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
q∩q⊆q = record { incl = λ lt → proj1 lt }

open HOD

-----
--
--  ultra filter is prime
--

filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P
filter-lemma1 {L} P u = record {
         proper = ultra-filter.proper u
       ; prime = lemma3
    } where
  lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
  lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
  ... | case1 p∈P  = case1 p∈P
  ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
    lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
       ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
      } where
         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
         lemma4 x lt with proj1 lt
         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
         lemma4 x lt | case2 qx = qx
    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
    lemma6 = filter2 P lt ¬p∈P
    lemma7 : filter P ∋ (q ∩ (L ＼ p))
    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
    lemma8 : (q ∩ (L ＼ p)) ⊆ q
    lemma8 = q∩q⊆q

-----
--
--  if Filter contains L, prime filter is ultra
--

filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
filter-lemma2 {L} P f∋L prime = record {
         proper = prime-filter.proper prime
       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
   } where
        open _==_
        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p))
        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  ))
        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
        lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
        lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L

record Dense  (P : HOD ) : Set (suc n) where
   field
       dense : HOD
       d⊆P :  dense ⊆ Power P
       dense-f : HOD → HOD
       dense-d :  { p : HOD} → p ⊆ P → dense ∋ dense-f p
       dense-p :  { p : HOD} → p ⊆ P → p ⊆ (dense-f p)

record Ideal  ( L : HOD  ) : Set (suc n) where
   field
       ideal : HOD
       i⊆PL :  ideal ⊆ Power L
       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)

open Ideal

proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
proper-ideal {L} P {p} = ideal P ∋ od∅

prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )

----
--
-- Filter/Ideal without ZF
--     L have to be a Latice
--

record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
   field
       filter : L → Set n
       f⊆P :  PL filter
       filter1 : { p q : L } → PL (λ x → q ⊆ x )  → filter p →  p ⊆ q  → filter q
       filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)

Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
Filter-is-F {L} f = record {
       filter = λ x → Lift (suc n) ((filter f) ∋ x)
     ; f⊆P = λ x f∋x →  power→⊆ _ _ (incl ( f⊆PL f  ) (lower f∋x ))
     ; filter1 = λ {p} {q} q⊆L f∋p  p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
     ; filter2 = λ {p} {q} f∋p f∋q  → lift ( filter2 f (lower f∋p) (lower f∋q))
    }

record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
   field
       dense : L → Set n
       d⊆P :  PL dense
       dense-f : L → L
       dense-d :  { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p  )
       dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p)

Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
Dense-is-F {L} f = record {
       dense =  λ x → Lift (suc n) ((dense f) ∋ x)
    ;  d⊆P = λ x f∋x →  power→⊆ _ _ (incl ( d⊆P f  ) (lower f∋x ))
    ;  dense-f = λ x → dense-f f x
    ;  dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
    ;  dense-p = λ {p} d → dense-p f (d p refl-⊆)
  } where open Dense

record GenericFilter (P : HOD) : Set (suc n) where
    field
       genf : Filter P
       generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )

record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
       GFilter : F-Filter L PL _⊆_ _∩_
       Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
       Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
module Solution where

open import Data.Empty
open import Data.List
open import Data.Nat
open import Data.Bool hiding (_≟_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

data Subseq : List ℕ → List ℕ → Set where
  subseq-nil  :                            Subseq [] []
  subseq-take : ∀ a xs ys → Subseq xs ys → Subseq (a ∷ xs) (a ∷ ys)
  subseq-drop : ∀ a xs ys → Subseq xs ys → Subseq xs (a ∷ ys)

_⊂_ : List ℕ → List ℕ → Set
_⊂_ = Subseq

subseq-match : (xs ys : List ℕ) → Bool
subseq-match [] ys = true
subseq-match (x ∷ xs) [] = false
subseq-match (x ∷ xs) (y ∷ ys) with x ≟ y
... | yes _ = subseq-match xs ys
... | no  _ = subseq-match (x ∷ xs) ys

_⊂*_ : List ℕ → List ℕ → Bool
_⊂*_ = subseq-match

-- silly : ∀ (a : ℕ) (xs ys : List ℕ) → xs ⊂* ys ≡ (a ∷ xs) ⊂* (a ∷ ys)
-- silly a xs ys = ?

subseq-match⇒subseq : ∀ xs ys → xs ⊂* ys ≡ true → xs ⊂ ys
subseq-match⇒subseq []       []       H = subseq-nil
subseq-match⇒subseq []       (y ∷ ys) H = subseq-drop y [] ys (subseq-match⇒subseq [] ys H)
subseq-match⇒subseq (x ∷ xs) (y ∷ ys) H with x ≟ y
... | yes P rewrite sym P = subseq-take x xs ys (subseq-match⇒subseq xs ys H)
... | no  _               = subseq-drop y (x ∷ xs) ys (subseq-match⇒subseq (x ∷ xs) ys H)

subseq⇒subseq-match : ∀ xs ys → xs ⊂ ys → xs ⊂* ys ≡ true
subseq⇒subseq-match .[] .[] subseq-nil = refl
subseq⇒subseq-match (x ∷ xs) .(a ∷ ys) (subseq-take a xs ys H) with x ≟ a
... | yes refl  = subseq⇒subseq-match xs ys H
... | no absurd = ⊥-elim (absurd refl)
subseq⇒subseq-match [] .(a ∷ ys) (subseq-drop a .[] ys H) = refl
subseq⇒subseq-match (x ∷ xs) .(a ∷ ys) (subseq-drop a .(x ∷ xs) ys H) with x ≟ a
... | yes refl = {!!}
... | no _ = {!!}

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import Relation.Binary

module Relation.Binary.Equivalence.Reasoning {a} {𝑆 : Set a} {b} (equivalence : Equivalence 𝑆 b) where

open Equivalence equivalence
open import Function

import Path

infixr 2 ≋˘⟨⟩-syntax _≋⟨⟩_ ≋⟨∙⟩-syntax ≡⟨∙⟩-syntax

≋˘⟨⟩-syntax : ∀ (x : 𝑆) {y z} → y ≋ z → y ≋ x → x ≋ z
≋˘⟨⟩-syntax _ y≋z y≋x = sym y≋x ⟨ trans ⟩ y≋z

syntax ≋˘⟨⟩-syntax x y≋z y≋x = x ≋˘⟨ y≋x ⟩ y≋z

≋⟨∙⟩-syntax : ∀ (x : 𝑆) {y z} → y ≋ z → x ≋ y → x ≋ z
≋⟨∙⟩-syntax _ y≋z x≋y = x≋y ⟨ trans ⟩ y≋z

syntax ≋⟨∙⟩-syntax x y≋z x≋y = x ≋⟨ x≋y ⟩ y≋z

_≋⟨⟩_ : ∀ (x : 𝑆) {y} → x ≋ y → x ≋ y
_ ≋⟨⟩ x≋y = x≋y

≡⟨∙⟩-syntax : ∀ (x : 𝑆) {y z} → y ≋ z → x Path.≡ y → x ≋ z
≡⟨∙⟩-syntax _ y≋z x≡y = Path.subst (_≋ _) (Path.sym x≡y) y≋z

syntax ≡⟨∙⟩-syntax x y≋z x≡y = x ≡⟨ x≡y ⟩ y≋z

infix 2.5 _∎
_∎ : ∀ x → x ≋ x
x ∎ = refl

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Oscar.Prelude

-- meta-class
open import Oscar.Class

-- classes
open import Oscar.Class.Smap
open import Oscar.Class.Symmetry

-- individual instances
open import Oscar.Class.Hmap.Transleftidentity
open import Oscar.Class.Reflexivity.Function
open import Oscar.Class.Transitivity.Function

-- instance bundles
open import Oscar.Property.Functor.SubstitunctionExtensionTerm

open import Oscar.Data.Proposequality

module Test.ProblemWithDerivation-2 where

postulate
  A : Set
  B : Set
  _~A~_ : A → A → Set
  _~B~_ : B → B → Set
  s1 : A → B
  f1 : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y

instance

  𝓢urjectivity1 : Smap.class _~A~_ _~B~_ s1 s1
  𝓢urjectivity1 .⋆ _ _ = f1

-- Oscar.Property.Setoid.Proposextensequality
module _ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} where

  instance

    𝓢ymmetryProposextensequality : Symmetry.class Proposextensequality⟦ 𝔓 ⟧
    𝓢ymmetryProposextensequality .⋆ f₁≡̇f₂ x rewrite f₁≡̇f₂ x = ∅

test : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test {x} {y} = smap -- FIXME this works now. why?


text:
-- Records are allowed in mutual blocks.
module RecordInMutual where

mutual
  record A : Set where
    field x : B
  record B : Set where
    field x : A

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
module Ag09 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  = g (f x)

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

-- exercises

≃-implies-≲ : ∀ {A B : Set}
  → A ≃ B
  -----
  → A ≲ B

≃-implies-≲ A≃B =
  record
  { to = to A≃B
  ; from = from A≃B
  ; from∘to = from∘to A≃B
  }

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl =
  record
  { to = λ{x → x}
  ; from = λ{y → y}
  }

⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
⇔-sym A⇔B =
  record
    { to   = from A⇔B
    ; from = to A⇔B
    }

⇔-trans : ∀ {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
⇔-trans A⇔B B⇔C =
  record
  { to = to B⇔C ∘ to A⇔B
  ; from = from A⇔B ∘ from B⇔C
  }

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to      = from A≃B
    ; from    = to   A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
        begin
          (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
        ≡⟨⟩
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
     }

module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Integers.Definition
open import Semirings.Definition
open import Groups.Abelian.Definition
open import Groups.Definition
open import Setoids.Setoids

module Numbers.Integers.Addition where

infix 15 _+Z_
_+Z_ : ℤ → ℤ → ℤ
nonneg zero +Z b = b
nonneg (succ x) +Z nonneg y = nonneg (succ x +N y)
nonneg (succ x) +Z negSucc zero = nonneg x
nonneg (succ x) +Z negSucc (succ y) = nonneg x +Z negSucc y
negSucc x +Z nonneg zero = negSucc x
negSucc zero +Z nonneg (succ y) = nonneg y
negSucc (succ x) +Z nonneg (succ y) = negSucc x +Z nonneg y
negSucc x +Z negSucc y = negSucc (succ x +N y)

+Zinherits : (a b : ℕ) → nonneg (a +N b) ≡ (nonneg a) +Z (nonneg b)
+Zinherits zero b = refl
+Zinherits (succ a) b = refl

+ZCommutative : (a b : ℤ) → a +Z b ≡ b +Z a
+ZCommutative (nonneg zero) (nonneg zero) = refl
+ZCommutative (nonneg zero) (nonneg (succ y)) = applyEquality (λ i → nonneg (succ i)) (Semiring.commutative ℕSemiring 0 y)
+ZCommutative (nonneg (succ x)) (nonneg zero) = applyEquality (λ i → nonneg (succ i)) (Semiring.commutative ℕSemiring x 0)
+ZCommutative (nonneg (succ x)) (nonneg (succ y)) = applyEquality (λ i → nonneg (succ i)) (transitivity (Semiring.commutative ℕSemiring x (succ y)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring y x)) (Semiring.commutative ℕSemiring (succ x) y)))
+ZCommutative (nonneg zero) (negSucc y) = refl
+ZCommutative (nonneg (succ x)) (negSucc zero) = refl
+ZCommutative (nonneg (succ x)) (negSucc (succ y)) = +ZCommutative (nonneg x) (negSucc y)
+ZCommutative (negSucc x) (nonneg zero) = refl
+ZCommutative (negSucc zero) (nonneg (succ y)) = refl
+ZCommutative (negSucc (succ x)) (nonneg (succ y)) = +ZCommutative (negSucc x) (nonneg y)
+ZCommutative (negSucc x) (negSucc y) = applyEquality (λ i → negSucc (succ i)) (Semiring.commutative ℕSemiring x y)

+ZAssociative : (a b c : ℤ) → a +Z (b +Z c) ≡ (a +Z b) +Z c
+ZAssociative (nonneg zero) (nonneg b) (nonneg c) = refl
+ZAssociative (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.commutative ℕSemiring a 0 = refl
+ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality (λ i → nonneg (succ i)) (Semiring.+Associative ℕSemiring a (succ b) c)
+ZAssociative (nonneg zero) (nonneg b) (negSucc c) = refl
+ZAssociative (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.sumZeroRight ℕSemiring a = refl
+ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) = applyEquality nonneg (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a b)) (Semiring.commutative ℕSemiring (succ b) a))
+ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc (succ c)) = transitivity (+ZAssociative (nonneg (succ a)) (nonneg b) (negSucc c)) (applyEquality (λ i → nonneg i +Z negSucc c) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a b)) (Semiring.commutative ℕSemiring (succ b) a)))
+ZAssociative (nonneg zero) (negSucc b) c = refl
+ZAssociative (nonneg (succ a)) (negSucc zero) (nonneg zero) = +ZCommutative (nonneg 0) (nonneg a)
+ZAssociative (nonneg (succ a)) (negSucc zero) (nonneg (succ c)) = transitivity (applyEquality nonneg (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a c)) (Semiring.commutative ℕSemiring (succ c) a))) (+Zinherits a (succ c))
+ZAssociative (nonneg (succ a)) (negSucc zero) (negSucc c) = refl
+ZAssociative (nonneg (succ a)) (negSucc (succ b)) (nonneg zero) = +ZCommutative (nonneg 0) _
+ZAssociative (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ c)) = transitivity (applyEquality (nonneg (succ a) +Z_) (+ZCommutative (negSucc b) (nonneg c))) (transitivity (+ZAssociative (nonneg (succ a)) (nonneg c) (negSucc b)) (transitivity (transitivity (transitivity (transitivity (applyEquality (λ i → nonneg (succ i) +Z negSucc b) (Semiring.commutative ℕSemiring a c)) (+ZCommutative (nonneg (succ (c +N a))) (negSucc b))) (applyEquality (negSucc b +Z_) (+ZCommutative (nonneg (succ c)) (nonneg a)))) (+ZAssociative (negSucc b) (nonneg a) (nonneg (succ c)))) (applyEquality (_+Z nonneg (succ c)) (+ZCommutative (negSucc b) (nonneg a)))))
+ZAssociative (nonneg (succ a)) (negSucc (succ b)) (negSucc c) = +ZAssociative (nonneg a) (negSucc b) (negSucc c)
+ZAssociative (negSucc a) (nonneg zero) c = refl
+ZAssociative (negSucc zero) (nonneg (succ b)) (nonneg c) = +Zinherits b c
+ZAssociative (negSucc zero) (nonneg (succ b)) (negSucc zero) = +ZCommutative (negSucc 0) (nonneg b)
+ZAssociative (negSucc zero) (nonneg (succ b)) (negSucc (succ c)) = transitivity (+ZCommutative (negSucc 0) (nonneg b +Z negSucc c)) (transitivity (equalityCommutative (+ZAssociative (nonneg b) (negSucc c) (negSucc 0))) (applyEquality (λ i → nonneg b +Z negSucc (succ i)) (Semiring.sumZeroRight ℕSemiring c)))
+ZAssociative (negSucc (succ a)) (nonneg (succ b)) (nonneg zero) = transitivity (applyEquality (λ i → negSucc a +Z (nonneg i)) (Semiring.sumZeroRight ℕSemiring b)) (+ZCommutative (nonneg 0) (negSucc a +Z nonneg b))
+ZAssociative (negSucc (succ a)) (nonneg (succ b)) (nonneg (succ c)) = transitivity (applyEquality (negSucc a +Z_) (+Zinherits b (succ c))) (+ZAssociative (negSucc a) (nonneg b) (nonneg (succ c)))
+ZAssociative (negSucc (succ a)) (nonneg (succ b)) (negSucc zero) = transitivity (+ZCommutative (negSucc (succ a)) (nonneg b)) (transitivity (transitivity (applyEquality (λ i → nonneg b +Z negSucc (succ i)) (equalityCommutative (Semiring.sumZeroRight ℕSemiring a))) (+ZAssociative (nonneg b) (negSucc a) (negSucc 0))) (applyEquality (_+Z negSucc 0) (+ZCommutative (nonneg b) (negSucc a))))
+ZAssociative (negSucc (succ a)) (nonneg (succ b)) (negSucc (succ c)) = transitivity (+ZCommutative (negSucc (succ a)) (nonneg b +Z negSucc c)) (transitivity (transitivity (equalityCommutative (+ZAssociative (nonneg b) (negSucc c) (negSucc (succ a)))) (transitivity (applyEquality (λ i → nonneg b +Z negSucc i) (Semiring.commutative ℕSemiring (succ c) (succ a))) (+ZAssociative (nonneg b) (negSucc a) (negSucc (succ c))))) (applyEquality (_+Z negSucc (succ c)) (+ZCommutative (nonneg b) (negSucc a))))
+ZAssociative (negSucc a) (negSucc b) (nonneg zero) = refl
+ZAssociative (negSucc a) (negSucc zero) (nonneg (succ c)) = applyEquality (λ i → negSucc i +Z nonneg c) (Semiring.commutative ℕSemiring 0 a)
+ZAssociative (negSucc a) (negSucc (succ b)) (nonneg (succ c)) = transitivity (+ZAssociative (negSucc a) (negSucc b) (nonneg c)) (applyEquality (λ i → negSucc i +Z nonneg c) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring a b)) (Semiring.commutative ℕSemiring (succ b) a)))
+ZAssociative (negSucc a) (negSucc b) (negSucc c) = applyEquality (λ i → negSucc (succ i)) (transitivity (Semiring.+Associative ℕSemiring a (succ b) c) (applyEquality (_+N c) (transitivity (Semiring.commutative ℕSemiring a (succ b)) (applyEquality succ (Semiring.commutative ℕSemiring b a)))))

additiveInverseExists : (a : ℕ) → (negSucc a +Z nonneg (succ a)) ≡ nonneg 0
additiveInverseExists zero = refl
additiveInverseExists (succ a) = additiveInverseExists a

additiveInverse : (a : ℤ) → ℤ
additiveInverse (nonneg zero) = nonneg 0
additiveInverse (nonneg (succ x)) = negSucc x
additiveInverse (negSucc x) = nonneg (succ x)

ℤGroup : Group (reflSetoid ℤ) (_+Z_)
Group.+WellDefined ℤGroup refl refl = refl
Group.0G ℤGroup = nonneg 0
Group.inverse ℤGroup = additiveInverse
Group.+Associative ℤGroup {a} {b} {c} = +ZAssociative a b c
Group.identRight ℤGroup {nonneg zero} = refl
Group.identRight ℤGroup {nonneg (succ x)} = applyEquality (λ i → nonneg (succ i)) (Semiring.commutative ℕSemiring x 0)
Group.identRight ℤGroup {negSucc x} = refl
Group.identLeft ℤGroup = refl
Group.invLeft ℤGroup {nonneg zero} = refl
Group.invLeft ℤGroup {nonneg (succ x)} = additiveInverseExists x
Group.invLeft ℤGroup {negSucc x} = transitivity (+ZCommutative (nonneg (succ x)) (negSucc x)) (additiveInverseExists x)
Group.invRight ℤGroup {nonneg zero} = refl
Group.invRight ℤGroup {nonneg (succ x)} = transitivity (+ZCommutative (nonneg (succ x)) (negSucc x)) (additiveInverseExists x)
Group.invRight ℤGroup {negSucc x} = additiveInverseExists x

ℤAbGrp : AbelianGroup ℤGroup
ℤAbGrp = record { commutative = λ {a} {b} → +ZCommutative a b }


text:
module Cats.Util.Monad where

open import Category.Monad public

open import Data.List using (List ; [] ; _∷_ ; map)
open import Data.Unit using (⊤)
open import Function using (_∘_)
open import Level using (Lift ; lift)

open RawMonad {{...}} public

private
  _<*>_ = _⊛_

module _ {f} {M : Set f → Set f} {{_ : RawMonad M}} where

  sequence : ∀ {A} → List (M A) → M (List A)
  sequence [] = return []
  sequence (mx ∷ mxs) = ⦇ mx ∷ sequence mxs ⦈

  void : ∀ {A} → M A → M (Lift f ⊤)
  void m = m >>= λ _ → return _

  mapM : ∀ {a} {A : Set a} {B} → (A → M B) → List A → M (List B)
  mapM f = sequence ∘ map f

  mapM′ : ∀ {a} {A : Set a} {B} → (A → M B) → List A → M (Lift f ⊤)
  mapM′ f = void ∘ mapM f

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Localization.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.PathSplitEquiv
open isPathSplitEquiv

open import Cubical.HITs.Localization.Base

module _ {ℓα ℓs ℓt} {A : Type ℓα} {S : A → Type ℓs} {T : A → Type ℓt} where

  rec : ∀ {F : ∀ α → S α → T α} {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'}
        → (lY : isLocal F Y) → (X → Y) → Localize F X → Y
  rec lY g ∣ x ∣ = g x
  rec lY g (ext   α f t)   = fst (sec (lY α)) (λ s → rec lY g (f s)) t
  rec lY g (isExt α f s i) = snd (sec (lY α)) (λ s → rec lY g (f s)) i s
  rec lY f (≡ext   α g h p t i)   = fst (secCong (lY α) (λ t → rec lY f (g t)) (λ t → rec lY f (h t)))
                                        (λ i s → rec lY f (p s i)) i t
  rec lY f (≡isExt α g h p t i j) = snd (secCong (lY α) (λ t → rec lY f (g t)) (λ t → rec lY f (h t)))
                                        (λ i s → rec lY f (p s i)) i j t

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------------
-- The alternating bit protocol (ABP) is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the ABP following the
-- formalization in Dybjer and Sander (1989).

module FOTC.Program.ABP.CorrectnessProofI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Stream.Type
open import FOTC.Data.Stream.Equality.PropertiesI
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Lemma1I
open import FOTC.Program.ABP.Lemma2I
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- Main theorem.
abpCorrect : ∀ {b os₁ os₂ is} → Bit b → Fair os₁ → Fair os₂ → Stream is →
             is ≈ abpTransfer b os₁ os₂ is
abpCorrect {b} {os₁} {os₂} {is} Bb Fos₁ Fos₂ Sis = ≈-coind B h₁ h₂
  where
  h₁ : ∀ {ks ls} → B ks ls →
       ∃[ k' ] ∃[ ks' ] ∃[ ls' ] ks ≡ k' ∷ ks' ∧ ls ≡ k' ∷ ls' ∧ B ks' ls'
  h₁ {ks} {ls} (b , os₁ , os₂ , as , bs , cs , ds , Sks , Bb , Fos₁ , Fos₂ , h)
     with Stream-out Sks
  ... | (k' , ks' , ks≡k'∷ks' , Sks') =
    k' , ks' , ls' , ks≡k'∷ks' , ls≡k'∷ls' , Bks'ls'
    where
    S-helper : ks ≡ k' ∷ ks' →
               S b ks os₁ os₂ as bs cs ds ls →
               S b (k' ∷ ks') os₁ os₂ as bs cs ds ls
    S-helper h₁ h₂ = subst (λ t → S b t os₁ os₂ as bs cs ds ls) h₁ h₂

    S'-lemma₁ : ∃[ os₁' ] ∃[ os₂' ] ∃[ as' ] ∃[ bs' ] ∃[ cs' ] ∃[ ds' ] ∃[ ls' ]
                  Fair os₁'
                  ∧ Fair os₂'
                  ∧ S' b k' ks' os₁' os₂' as' bs' cs' ds' ls'
                  ∧ ls ≡ k' ∷ ls'
    S'-lemma₁ = lemma₁ Bb Fos₁ Fos₂ (S-helper ks≡k'∷ks' h)

    -- Following Martin Escardo advice (see Agda mailing list, heap
    -- mistery) we use pattern matching instead of ∃ eliminators to
    -- project the elements of the existentials.

    -- 2011-08-25 update: It does not seems strictly necessary because
    -- the Agda issue 415 was fixed.

    ls' : D
    ls' with S'-lemma₁
    ... | _ , _ , _ , _ , _ , _ , ls' , _ = ls'

    ls≡k'∷ls' : ls ≡ k' ∷ ls'
    ls≡k'∷ls' with S'-lemma₁
    ... | _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , prf = prf

    S-lemma₂ : ∃[ os₁'' ] ∃[ os₂'' ] ∃[ as'' ] ∃[ bs'' ] ∃[ cs'' ] ∃[ ds'' ]
                 Fair os₁''
                 ∧ Fair os₂''
                 ∧ S (not b) ks' os₁'' os₂'' as'' bs'' cs'' ds'' ls'
    S-lemma₂ with S'-lemma₁
    ... | _ , _ , _ , _ , _ , _ , _ , Fos₁' , Fos₂' , s' , _ =
      lemma₂ Bb Fos₁' Fos₂' s'

    Bks'ls' : B ks' ls'
    Bks'ls' with S-lemma₂
    ... | os₁'' , os₂'' , as'' , bs'' , cs'' , ds'' , Fos₁'' , Fos₂'' , s =
      not b , os₁'' , os₂'' , as'' , bs'' , cs'' , ds''
      , Sks' , not-Bool Bb , Fos₁'' , Fos₂'' , s

  h₂ : B is (abpTransfer b os₁ os₂ is)
  h₂ = b
       , os₁
       , os₂
       , has aux₁ aux₂ aux₃ aux₄ aux₅ is
       , hbs aux₁ aux₂ aux₃ aux₄ aux₅ is
       , hcs aux₁ aux₂ aux₃ aux₄ aux₅ is
       , hds aux₁ aux₂ aux₃ aux₄ aux₅ is
       , Sis
       , Bb
       , Fos₁
       , Fos₂
       , has-eq aux₁ aux₂ aux₃ aux₄ aux₅ is
       , hbs-eq aux₁ aux₂ aux₃ aux₄ aux₅ is
       , hcs-eq aux₁ aux₂ aux₃ aux₄ aux₅ is
       , hds-eq aux₁ aux₂ aux₃ aux₄ aux₅ is
       , trans (abpTransfer-eq b os₁ os₂ is)
           (transfer-eq aux₁ aux₂ aux₃ aux₄ aux₅ is)
    where
    aux₁ aux₂ aux₃ aux₄ aux₅ : D
    aux₁ = send b
    aux₂ = ack b
    aux₃ = out b
    aux₄ = corrupt os₁
    aux₅ = corrupt os₂

------------------------------------------------------------------------------
-- abpTransfer produces a Stream.
abpTransfer-Stream : ∀ {b os₁ os₂ is} →
                     Bit b →
                     Fair os₁ →
                     Fair os₂ →
                     Stream is →
                     Stream (abpTransfer b os₁ os₂ is)
abpTransfer-Stream Bb Fos₁ Fos₂ Sis = ≈→Stream₂ (abpCorrect Bb Fos₁ Fos₂ Sis)

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Pointed.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Foundations.Structure
open import Cubical.Foundations.Structure using (typ) public
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

Pointed : (ℓ : Level) → Type (ℓ-suc ℓ)
Pointed ℓ = TypeWithStr ℓ (λ x → x)

pt : ∀ {ℓ} (A∙ : Pointed ℓ) → typ A∙
pt = str

Pointed₀ = Pointed ℓ-zero

{- Pointed functions -}
_→∙_ : ∀{ℓ ℓ'} → (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
(A , a) →∙ (B , b) = Σ[ f ∈ (A → B) ] f a ≡ b

_→∙_∙ : ∀{ℓ ℓ'} → (A : Pointed ℓ) (B : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
(A →∙ B ∙) .fst = A →∙ B
(A →∙ B ∙) .snd .fst x = pt B
(A →∙ B ∙) .snd .snd = refl

idfun∙ : ∀ {ℓ} (A : Pointed ℓ) → A →∙ A
idfun∙ A .fst x = x
idfun∙ A .snd = refl

{- HIT allowing for pattern matching on pointed types -}
data Pointer {ℓ} (A : Pointed ℓ) : Type ℓ where
  pt₀ : Pointer A
  ⌊_⌋ : typ A → Pointer A
  id : ⌊ pt A ⌋ ≡ pt₀

IsoPointedPointer : ∀ {ℓ} {A : Pointed ℓ} → Iso (typ A) (Pointer A)
Iso.fun IsoPointedPointer = ⌊_⌋
Iso.inv (IsoPointedPointer {A = A}) pt₀ = pt A
Iso.inv IsoPointedPointer ⌊ x ⌋ = x
Iso.inv (IsoPointedPointer {A = A}) (id i) = pt A
Iso.rightInv IsoPointedPointer pt₀ = id
Iso.rightInv IsoPointedPointer ⌊ x ⌋ = refl
Iso.rightInv IsoPointedPointer (id i) j = id (i ∧ j)
Iso.leftInv IsoPointedPointer x = refl

Pointed≡Pointer : ∀ {ℓ} {A : Pointed ℓ} → typ A ≡ Pointer A
Pointed≡Pointer = isoToPath IsoPointedPointer

Pointer∙ : ∀ {ℓ} (A : Pointed ℓ) → Pointed ℓ
Pointer∙ A .fst = Pointer A
Pointer∙ A .snd = pt₀

Pointed≡∙Pointer : ∀ {ℓ} {A : Pointed ℓ} → A ≡ (Pointer A , pt₀)
Pointed≡∙Pointer {A = A} i = (Pointed≡Pointer {A = A} i) , helper i
  where
  helper : PathP (λ i → Pointed≡Pointer {A = A} i) (pt A) pt₀
  helper = ua-gluePath (isoToEquiv (IsoPointedPointer {A = A})) id

pointerFun : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
            → Pointer A → Pointer B
pointerFun f pt₀ = pt₀
pointerFun f ⌊ x ⌋ = ⌊ fst f x ⌋
pointerFun f (id i) = (cong ⌊_⌋ (snd f) ∙ id) i

pointerFun∙ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
             → Pointer∙ A →∙ Pointer∙ B
pointerFun∙ f .fst = pointerFun f
pointerFun∙ f .snd = refl

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
open import SOAS.Common
open import SOAS.Families.Core
import SOAS.Metatheory.MetaAlgebra

-- Shorthands for de Bruijn indices
module SOAS.Syntax.Shorthands {T : Set}
  {⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ}
  (open SOAS.Metatheory.MetaAlgebra ⅀F)
  {𝒜 : Familyₛ → Familyₛ}(𝒜ᵃ : (𝔛 : Familyₛ) → MetaAlg 𝔛 (𝒜 𝔛))
  where

open import SOAS.Context
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive
open import SOAS.Variable
open import Data.Nat

open import Relation.Nullary.Decidable using (True; toWitness)

private
  variable
    α β γ δ υ : T
    Γ Δ : Ctx

module _ {𝔛 : Familyₛ} where
  open MetaAlg 𝔛 (𝒜ᵃ 𝔛)

  -- Refer to variables via de Bruijn numerals: e.g. ` 2 = 𝑣𝑎𝑟 (old (old new))
  len : Ctx {T} → ℕ
  len ∅        =  ℕ.zero
  len (α ∙ Γ)  =  suc (len Γ)

  ix : {Γ : Ctx} → {n : ℕ} → (p : n < len Γ) → T
  ix {(α ∙ _)} {zero}    (s≤s z≤n)  =  α
  ix {(_ ∙ Γ)} {(suc n)} (s≤s p)    =  ix p

  deBruijn : ∀ {Γ} → {n : ℕ} → (p : n < len Γ) → ℐ (ix p) Γ
  deBruijn {_ ∙ _} {zero}    (s≤s z≤n)  =  new
  deBruijn {_ ∙ Γ} {(suc n)} (s≤s p)    =  old (deBruijn p)

  ′ : {Γ : Ctx}(n : ℕ){n∈Γ : True (suc n ≤? len Γ)} → 𝒜 𝔛 (ix (toWitness n∈Γ)) Γ
  ′ n {n∈Γ} = 𝑣𝑎𝑟 (deBruijn (toWitness n∈Γ))

  -- Explicit abbreviations for de Bruijn indices 0-4
  x₀ : 𝒜 𝔛 α (α ∙ Γ)
  x₀ = 𝑣𝑎𝑟 new
  x₁ : 𝒜 𝔛 β (α ∙ β ∙ Γ)
  x₁ = 𝑣𝑎𝑟 (old new)
  x₂ : 𝒜 𝔛 γ (α ∙ β ∙ γ ∙ Γ)
  x₂ = 𝑣𝑎𝑟 (old (old new))
  x₃ : 𝒜 𝔛 δ (α ∙ β ∙ γ ∙ δ ∙ Γ)
  x₃ = 𝑣𝑎𝑟 (old (old (old new)))
  x₄ : 𝒜 𝔛 υ (α ∙ β ∙ γ ∙ δ ∙ υ ∙ Γ)
  x₄ = 𝑣𝑎𝑟 (old (old (old (old new))))

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
import MJ.Classtable

import MJ.Syntax as Syntax
import MJ.Semantics.Values as Values
import MJ.Classtable.Core as Core
import MJ.Classtable.Code as Code

--
-- Substitution-free interpretation of welltyped MJ
--

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

open import Prelude hiding (_^_)
open import Data.Vec hiding (init; _>>=_)
open import Data.Vec.All.Properties.Extra as Vec∀++
open import Data.List hiding (null)
open import Data.List.Properties.Extra
open import Data.List.All.Properties.Extra
open import Data.List.Prefix
open import Data.List.First
open import Data.List.First.Properties
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Relation.Nullary.Decidable
open import Data.Star hiding (return; _>>=_)
open import Data.Sum using (_⊎_; inj₁; inj₂)

open Values Ct
open Syntax Ct
open Code Ct
open Core c
open Classtable Ct

open import MJ.Syntax.Program Ct
open import MJ.Classtable.Membership Ct
open import MJ.Types
open import MJ.LexicalScope c
open import MJ.Semantics.Environments Ct
open import MJ.Semantics.Objects Ct
open import MJ.Semantics.Objects.Flat Ct ℂ using (encoding)
open import Common.Weakening

{-
Make the object encoding API available;
-}
open ObjEncoding encoding

{-
The monad in which we define evaluation.
This encapsulates state, lexical environments, timeouts and exceptions.
-}
WSet = World c → Set

data Exception : Set where
  nullderef : Exception
  other     : Exception

data Result (W : World c)(A : WSet) : Set where
  exception : ∀ {W'} → W' ⊒ W → Store W' → Exception → Result W A
  timeout   : Result W A
  returns   : ∀ {W'} → W' ⊒ W → Store W' → A W' → Result W A

result-strengthen : ∀ {W W'}{A : WSet} → W ⊒ W' → Result W A → Result W' A
result-strengthen ext (exception ext' μ e) = exception (ext ⊚ ext') μ e
result-strengthen ext timeout = timeout
result-strengthen ext (returns ext' μ v) = returns (ext ⊚ ext') μ v

-- monad that threads a readonly environment, store and propagates
-- semantic errors
M : Ctx → World c → WSet → Set
M Γ W A = Env Γ W → Store W → Result W A

return  : ∀ {Γ W}{A : WSet} → A W → M Γ W A
return v _ μ = returns ⊑-refl μ v

doTimeout : ∀ {Γ W}{A : WSet} → M Γ W A
doTimeout _ _ = timeout

raiseM : ∀ {Γ W}{A : WSet} → Exception → M Γ W A
raiseM exc E μ = exception ⊑-refl μ exc

sval-weaken : ∀ {W W' a} → W' ⊒ W → StoreVal W a → StoreVal W' a
sval-weaken ext (val x) = val $ weaken-val ext x
sval-weaken ext (obj cid x) = obj cid (weaken-obj cid ext x)

instance
  storeval-weakenable : ∀ {a} → Weakenable (λ W → StoreVal W a)
  storeval-weakenable = record {wk = sval-weaken }

infixl 10 _>>=_
_>>=_   : ∀ {Γ W}{A B : WSet} → M Γ W A → (∀ {W'} → A W' → M Γ W' B) →
          M Γ W B
(k >>= f) E μ with k E μ
... | exception ext μ' e = exception ext μ' e
... | timeout = timeout
... | returns ext μ' v = result-strengthen ext $ f v (All.map (wk ext) E) μ'

infixl 10 _^_
_^_  :  ∀ {Σ Γ}{A B : WSet} ⦃ w : Weakenable B ⦄ → M Γ Σ A → B Σ → M Γ Σ (A ⊗ B)
(f ^ x) E μ with (f E μ)
...  | timeout = timeout
...  | exception ext μ' e = exception ext μ' e
...  | returns ext μ' v = returns ext μ' (v , wk ext x)

_recoverWith_ : ∀ {Γ W}{A : WSet} → M Γ W A →
                (∀ {W'} → Exception → W' ⊒ W → M Γ W' A) →
                M Γ W A
(k recoverWith f) E μ with k E μ
... | timeout = timeout
... | returns ext μ' x = returns ext μ' x
... | exception ext μ' e = result-strengthen ext $ f e ext (wk ext E) μ'

store   : ∀ {Γ W a} → StoreVal W a → M Γ W (λ W' → a ∈ W')
store {Γ}{W}{a} sv E μ =
  let
    ext = ∷ʳ-⊒ a W
    μ'  = (All.map (wk ext) μ) all-∷ʳ (wk ext sv)
  in returns ext μ' (∈-∷ʳ W a)

update   : ∀ {Γ W a} → a ∈ W → StoreVal W a → M Γ W (λ W' → ⊤)
update ptr v E μ = returns ⊑-refl (μ All.[ ptr ]≔ v) tt

deref : ∀ {Γ W a} → a ∈ W → M Γ W (flip StoreVal a)
deref ptr E μ = returns ⊑-refl μ (∈-all ptr μ)

getEnv : ∀ {Γ W}{A : WSet} → (Env Γ W → M Γ W A) → M Γ W A
getEnv f E μ = f E E μ

usingEnv : ∀ {Γ Γ' W}{A : WSet} → Env Γ' W → M Γ' W A → M Γ W A
usingEnv E e = const $ e E

store*  : ∀ {Γ W as} → All (λ a → StoreVal W (vty a)) as →
          M Γ W (λ W' → All (λ a → (vty a) ∈ W') as)
store* [] = return []
store* (v ∷ vs) =
  store v ^ vs >>= λ{ (r , vs) →
  store* vs ^ r >>= λ{ (rs , r) →
  return (r ∷ rs) }}

{-
Lifting of object getter/setter into the monad
-}
read-field : ∀ {Γ : Ctx}{C W f a} → IsMember C FIELD f a → Val W (ref C) →
            M Γ W (λ W → Val W a)
read-field m null = raiseM nullderef
read-field m (ref o C<:C') E μ with ∈-all o μ
read-field m (ref o C<:C') E μ | obj cid O = returns ⊑-refl μ (getter _ O (inherit' C<:C' m))

write-field : ∀ {Γ C W f a} → IsMember C FIELD f a → Val W (ref C) → Val W a →
            M Γ W (flip Val (ref C))
write-field m null v = raiseM nullderef
write-field m (ref o s) v E μ with ∈-all o μ
write-field m (ref o s) v E μ | obj cid O =
  let
    vobj = obj cid (setter _ O (inherit' s m) v)
    μ' = μ All.[ o ]≔ vobj
  in returns ⊑-refl μ' (ref o s)

-- Get the implementation of any method definition of a class
mbody : ∀ {m ty} cid → AccMember cid METHOD m ty → InheritedMethod cid m ty
mbody cid mb with toWitness mb
... | (pid , s , d∈decls) = pid , s , ∈-all (proj₁ (first⟶∈ d∈decls)) (Implementation.mbodies (ℂ pid))

{-
Refinements of bind and return for the nested monad for command evaluation
-}
_>>=c_ : ∀ {I O O' : Ctx}{W : World c}{a} →
          M I W (λ W → Val W a ⊎ Env O W) →
          (∀ {W'} → Env O W' → M I W' (λ W → Val W a ⊎ Env O' W)) →
          M I W (λ W → Val W a ⊎ Env O' W)
m >>=c f = m >>= λ{
  (inj₁ v) → return (inj₁ v) ;
  (inj₂ E) → f E }

continue : ∀ {Γ : Ctx}{W : World c}{a} → M Γ W (λ W → Val W a ⊎ Env Γ W)
continue = getEnv λ E → return (inj₂ E)

{-
Fueled interpreter
-}
mutual

  {-
  Arguments are passed as mutable and thus have to be evaluated, after which
  we store the values in the store and we pass the references.
  -}
  eval-args : ∀ {Γ as W} → ℕ → All (Expr Γ) as → M Γ W (λ W' → All (λ a → (vty a) ∈ W') as)
  eval-args k args =
    evalₑ* k args >>= λ vs →
    store* (All.map val vs)

  {-
  Object initialization:
  Creates a default object; stores a mutable reference to it on the heap; calls the constructor
  on the resulting reference.
  -}
  constructM : ℕ → ∀ cid → ∀ {W} → M (Class.constr (Σ cid)) W (flip Val (ref cid))
  constructM k cid with ℂ cid
  constructM k cid | (implementation construct mbodies) =
    store (obj _ (defaultObject cid)) >>= λ r →
    store (val (ref r ε)) ^ r >>= λ{ (r' , r) →
    getEnv λ E →
    usingEnv (E ⊕ r') (eval-constructor k ε r construct) ^ r >>= λ{ (_ , r) →
    return $ ref r ε }}

  {-
  Constructor interpretation:
  The difficult case being the one where we have a super call.
  -}
  eval-constructor : ∀ {cid' cid W} → ℕ → Σ ⊢ cid' <: cid → (obj cid') ∈ W → Constructor cid →
                     M (constrctx cid) W (flip Val void)
  eval-constructor zero _ _ _ = doTimeout
  eval-constructor {_}{Object} (suc k) _ _ _ = return unit
  eval-constructor {_}{cls cid} (suc k) s o∈W (super args then b) =
    -- evaluate super call
    let
      s'   = s ◅◅ super ◅ ε
      super-con = Implementation.construct (ℂ (Class.parent (Σ (cls cid))))
    in
    eval-args k args ^ o∈W >>= λ{ (rvs , o∈W) → -- arguments
    getEnv λ{ (self ∷ _) →
      -- store a parent pointer for passing to super
      store (val (ref o∈W s')) ^ o∈W ^ rvs >>= λ{ ((sup , o∈W) , rvs) →
      usingEnv (sup ∷ rvs) (eval-constructor k s' o∈W super-con) >>= λ _ →

      -- evaluate own body
      eval-body k b >>= λ _ →
      return unit
    }}}
  eval-constructor {_}{cls id} (suc k) _ _ (body x) =
    eval-body k x >>= λ _ →
    return unit

  {-
  Method evaluation including super calls.
  The difficult case again being the one where we have a super call.
  -}
  eval-method : ∀ {cid m as b pid W Γ} → ℕ →
                Σ ⊢ cid <: pid → (obj cid) ∈ W →
                All (λ ty → vty ty ∈ W) as →
                InheritedMethod pid m (as , b) → M Γ W (flip Val b)
  eval-method zero _ _ _ _ = doTimeout
  eval-method (suc k) s o args (pid' , pid<:pid' , body b) =
    store (val (ref o (s ◅◅ pid<:pid'))) ^ args >>= λ{ (mutself , args) →
    usingEnv (mutself ∷ args) (eval-body k b) }
  eval-method {_}{m}{as}{b} (suc k) s o args (Object , _ , super x ⟨ _ ⟩then _) rewrite Σ-Object =
    -- calling a method on Object is improbable...
    ⊥-elim (∉Object {METHOD}{m}{(as , b)}(sound x))
  eval-method (suc k) s o args (cls pid' , pid<:pid' , super x ⟨ supargs ⟩then b) =
    let super-met = mbody (Class.parent (Σ (cls pid'))) x in
      store (val (ref o (s ◅◅ pid<:pid'))) ^ (args , o) >>= λ{ (mutself , args , o) →
      -- eval super args in method context
      usingEnv (mutself ∷ args) (eval-args k supargs) ^ (args , o) >>= λ{ (rvs , args , o) →
      -- call super
      eval-method k (s ◅◅ pid<:pid' ◅◅ super ◅ ε) o rvs super-met ^ (args , o) >>= λ{ (retv , args , o) →
      -- store the super return value to be used as a mutable local
      store (val retv) ^ (args , o) >>= λ{ (mutret , args , o) →
      -- store the mutable "this"
      store (val (ref o (s ◅◅ pid<:pid'))) ^ (mutret , args) >>= λ{ (mutself' , mutret , args) →
      -- call body
      usingEnv (mutret ∷ mutself' ∷ args) (eval-body k b) }}}}}

  {-
  evaluation of expressions
  -}
  evalₑ : ∀ {Γ : Ctx}{a} → ℕ → Expr Γ a → ∀ {W} → M Γ W (flip Val a)
  evalₑ zero _ = doTimeout

  -- primitive values
  evalₑ (suc k) unit =
    return unit

  evalₑ (suc k) (num n) =
    return (num n)

  evalₑ (suc k) null =
    return null

  -- variable lookup
  evalₑ (suc k) (var x) =
    getEnv (λ E → return $ getvar x E) >>= λ v →
    deref v >>= λ{ (val w) →
    return w }

  evalₑ (suc k) (upcast ε e) = evalₑ k e
  evalₑ (suc k) (upcast s₁@(_ ◅ _) e) = evalₑ k e >>= λ{
      (ref o s₂ ) → return $ ref o (s₂ ◅◅ s₁) ;
      null → return null
    }

  -- binary interger operations
  evalₑ (suc k) (iop f l r) =
    evalₑ k l >>= λ{ (num vₗ) →
    evalₑ k r >>= λ{ (num vᵣ) →
    return (num (f vₗ vᵣ)) }}

  -- method calls
  evalₑ (suc k) (call e _ {acc = mtd} args) =
    evalₑ k e >>= λ{
      null → raiseM nullderef ;
      r@(ref {dyn-cid} o s₁) →
        -- evaluate the arguments
        eval-args k args ^ o >>= λ{ (rvs , o) →
        -- dynamic dispatch: dynamic lookup of the method on the runtime class of the reference
        -- and execution of the call
        (eval-method k ε o rvs (mbody dyn-cid (inherit _ s₁ mtd))) }}

  -- field lookup in the heap
  evalₑ (suc k) (get e _ {_}{fld}) =
    evalₑ k e >>= λ{
      null → raiseM nullderef ;
      (ref o s) →
        deref o >>= λ{ (obj c O) →
        return (getter _ O $ inherit' s (sound fld)) }}

  -- object allocation
  evalₑ (suc k) (new C args) =
    eval-args k args >>= λ rvs →
    usingEnv rvs (constructM k C)

  {-
  Statement evaluation
  -}
  evalc : ∀ {I : Ctx}{O : Ctx}{W : World c}{a} → ℕ →
          Stmt I a O → M I W (λ W → Val W a ⊎ Env O W)

  evalc zero _ = doTimeout

  evalc (suc k) raise = raiseM other

  evalc (suc k) (block stmts) =
    eval-stmts k stmts >>=c λ _ → continue

  evalc (suc k) (try cs catch cs') =
    (evalc k cs >>=c λ _ → continue)
    recoverWith (λ e ext → evalc k cs' >>= λ _ → continue)

  -- new local variable
  evalc (suc k) (loc a) =
    store (val $ default a) >>= λ r →
    getEnv λ E → return (inj₂ (E ⊕ r))

  -- assigning to a local
  evalc (suc k) (asgn x e) =
    evalₑ k e >>= λ v →
    getEnv (λ E → return $ getvar x E) ^ v >>= λ{ (addr , v) →
    update addr (val v) >>= λ _ →
    continue }

  -- setting a field
  evalc (suc k) (set r _ {_}{fld} e) =
    evalₑ k r >>= λ{
    null → raiseM nullderef ;
    r'@(ref _ _) →
      evalₑ k e ^ r' >>= λ{ (v , r') →
      write-field (sound fld) r' v >>= λ _ →
      continue }}

  -- side-effectful expressions
  evalc (suc k) (run e) =
    evalₑ k e >>= λ _ →
    continue

  -- early returns
  evalc (suc k) (ret e) =
    evalₑ k e >>= λ v →
    return (inj₁ v)

  -- if-then-else blocks
  evalc (suc k) (if e then cs else ds) =
    evalₑ k e >>= λ{
      (num zero) → evalc k cs ;
      (num (suc _)) → evalc k ds
    }

  -- while loops
  evalc (suc k) (while e run b) =
    evalₑ (suc k) e >>= λ{
      (num zero)    → evalc k b >>= λ _ → evalc k (while e run b) ;
      (num (suc _)) → continue
    }

  {-
  An helper for interpreting a sequence of statements
  -}
  eval-stmts : ∀ {Γ Γ' W a} → ℕ → Stmts Γ a Γ' → M Γ W (λ W → Val W a ⊎ Env Γ' W)
  eval-stmts k ε = continue
  eval-stmts k (x ◅ st) =
    evalc k x >>=c λ E' →
    usingEnv E' (eval-stmts k st)

  {-
  An helper for interpreting method bodies (i.e. sequence of Stmts optionally followed by a return).
  -}
  eval-body : ∀ {I : Ctx}{W : World c}{a} → ℕ → Body I a → M I W (λ W → Val W a)
  eval-body k (body ε re) = evalₑ k re
  eval-body k (body stmts@(_ ◅ _) e) =
    (eval-stmts k stmts) >>= λ{
      (inj₁ v) → return v ;
      (inj₂ E) → usingEnv E (evalₑ k e) }

  {-
  An helper for interpreting a list of expressions in the same context.
  -}
  evalₑ* : ∀ {Γ W as} → ℕ → All (Expr Γ) as → M Γ W (λ W → All (Val W) as)
  evalₑ* k [] = return []
  evalₑ* k (e ∷ es) =
    evalₑ k e >>= λ v →
    evalₑ* k es ^ v >>= λ{ (vs , v) →
    return (v ∷ vs) }

eval : ∀ {a} → ℕ → Prog a → Result [] (flip Val a)
eval k (lib , main) = eval-body k main [] []

{-
a few predicates on program interpretation:
... saying it will terminate succesfully in a state where P holds
-}
_⇓⟨_⟩_ : ∀ {a} → Prog a → ℕ → (P : ∀ {W} → Val W a → Set) → Set
p ⇓⟨ k ⟩ P with eval k p
p ⇓⟨ k ⟩ P | exception _ _ _ = ⊥
p ⇓⟨ k ⟩ P | timeout = ⊥
p ⇓⟨ k ⟩ P | returns ext μ v = P v

{-
...saying it will raise an exception in a state where P holds
-}
_⇓⟨_⟩!_ : ∀ {a} → Prog a → ℕ → (P : ∀ {W} → Store W → Exception → Set) → Set
p ⇓⟨ k ⟩! P with eval k p
p ⇓⟨ k ⟩! P | exception _ μ e = P μ e
p ⇓⟨ k ⟩! P | timeout = ⊥
p ⇓⟨ k ⟩! P | returns ext μ v = ⊥


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Data.Natural where

open import Light.Library.Data.Natural using (Library ; Dependencies)
import Light.Implementation.Relation.Decidable
import Light.Implementation.Relation.Binary.Equality.Propositional
import Light.Package
open import Light.Library.Relation.Decidable using (Decidable ; yes ; no ; if_then_else_)
import Light.Implementation.Relation.Binary.Equality.Propositional.Decidable as DecidablePropositional
open import Light.Library.Relation.Binary using (reflexivity ; congruence)
open import Light.Library.Relation.Binary.Equality using (_≈_ ; wrap)
open import Agda.Builtin.Equality using (refl)

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            data ℕ : Set where
                  zero : ℕ
                  successor : ℕ → ℕ

            {-# COMPILE JS
                  ℕ = (a, cons) => a === 0n ? cons.zero() : cons.successor(a - 1n)
            #-}
            {-# COMPILE JS zero = 0n #-}
            {-# COMPILE JS successor = a => a + 1n #-}

            postulate _+_ _∗_ _//_ _∸_ : ℕ → ℕ → ℕ

            {-# COMPILE JS _+_ = () => a => b => a + b #-}
            {-# COMPILE JS _∗_ = () => a => b => a * b #-}
            {-# COMPILE JS _//_ = () => a => b => a / b #-}
            {-# COMPILE JS _∸_ = () => a => b => a < b ? 0n : a - b #-}

            predecessor : _
            predecessor a = a ∸ successor zero

            private _≈?_ : ∀ (a b : ℕ) → Decidable (a ≈ b)
            zero ≈? zero = yes reflexivity
            successor _ ≈? zero = no λ ()
            zero ≈? successor _ = no λ ()
            successor a ≈? successor b =
                  if a ≈? b
                  then (λ ⦃ a‐≡‐b ⦄ → yes (congruence a‐≡‐b))
                  else (λ ⦃ f ⦄ → no λ {refl → f reflexivity})

            equals = record { equals = wrap (record { are = λ a b → a ≈? b }) }

            module EqualityProperties = DecidablePropositional.Main _≈?_

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module silly0 where

record SingleSortedAlgebra : Set₁ where
  field
    Carrier : Set
    _⊕_     : Carrier → Carrier → Carrier

{-

One of my aims to introduce construct “fields-of”:

    record SingleSortedAlgebraWithConstant : Set₁ where
       fields-of SingleSortedAlgebra renaming (_⊕_ to _⟨$⟩_)
       field
         ε : Carrier

Should have the same net result as:

    record SingleSortedAlgebraWithConstant : Set₁ where
       field
         Carrier : Set
         _⟨$⟩_   : Carrier → Carrier → Carrier
         ε       : Carrier

-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Boolean where

open import Light.Level using (Level ; Setω ; Lifted)
open import Light.Variable.Sets
open import Light.Library.Data.Unit as Unit using (Unit)
open import Light.Library.Data.Empty as Empty using (Empty)
open import Light.Package using (Package)
open import Light.Library.Relation.Binary
      using (SelfTransitive ; SelfSymmetric ; Reflexive)
open import Light.Library.Relation.Binary.Equality as ≈ using (_≈_)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableSelfEquality)
import Light.Library.Relation.Decidable
open import Light.Library.Relation using (False)

record Dependencies : Setω where
      field
            ⦃ unit‐package ⦄ : Package record { Unit }
            ⦃ empty‐package ⦄ : Package record { Empty }

record Library (dependencies : Dependencies) : Setω where
      field
            ℓ : Level
            Boolean : Set ℓ
            true false : Boolean
            if_then_else_ : Boolean → 𝕒 → 𝕒 → 𝕒
            ¬_ : Boolean → Boolean
            _∧_ _∨_ _⇢_ : Boolean → Boolean → Boolean
            true‐is‐true : if true then Lifted (Empty.ℓ) Unit else Lifted (Unit.ℓ) Empty
            false‐is‐false : if false then Lifted (Unit.ℓ) Empty else Lifted (Empty.ℓ) Unit
            ⦃ equals ⦄ : DecidableSelfEquality Boolean
            ⦃ ≈‐transitive ⦄ : SelfTransitive (≈.self‐relation Boolean)
            ⦃ ≈‐symmetric ⦄ : SelfSymmetric (≈.self‐relation Boolean)
            ⦃ ≈‐reflexive ⦄ : Reflexive (≈.self‐relation Boolean)
            true‐≉‐false : False (true ≈ false)

open Library ⦃ ... ⦄ public


text:
module Issue794 where

open import Common.Prelude
open import Common.MAlonzo

postulate A : Set

record R : Set where
  id : A → A
  id x = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module LeqLemmas where

open import Data.Nat
  using (ℕ; suc; _+_; _*_; _<_; _≤_; _≤?_; z≤n; s≤s; module ≤-Reasoning)
open import Data.Nat.Properties.Simple using (+-comm)
open import Data.Nat.Properties using (n≤m+n)
open import Relation.Binary using (Decidable)

------------------------------------------------------------------------------
-- Proofs and definitions about ≤ on natural numbers

_<?_ : Decidable _<_
i <? j = suc i ≤? j

cong+r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i + k ≤ j + k
cong+r≤ {0}     {j}     z≤n       k = n≤m+n j k
cong+r≤ {suc i} {0}     ()        k -- absurd
cong+r≤ {suc i} {suc j} (s≤s i≤j) k = s≤s (cong+r≤ {i} {j} i≤j k)

cong+l≤ : ∀ {i j} → i ≤ j → (k : ℕ) → k + i ≤ k + j
cong+l≤ {i} {j} i≤j k =
  begin (k + i
           ≡⟨ +-comm k i ⟩
         i + k
           ≤⟨ cong+r≤ i≤j k ⟩
         j + k
           ≡⟨ +-comm j k ⟩
         k + j ∎)
  where open ≤-Reasoning

cong*r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i * k ≤ j * k
cong*r≤ {0}     {j}     z≤n       k = z≤n
cong*r≤ {suc i} {0}     ()        k -- absurd
cong*r≤ {suc i} {suc j} (s≤s i≤j) k = cong+l≤ (cong*r≤ i≤j k) k

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

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use `Data.Vec.Functional` instead.
------------------------------------------------------------------------

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

module Data.Table.Base where

{-# WARNING_ON_IMPORT
"Data.Table.Base was deprecated in v1.2.
Use Data.Vec.Functional instead."
#-}

open import Data.Nat.Base
open import Data.Fin.Base
open import Data.Product using (_×_ ; _,_)
open import Data.List.Base as List using (List)
open import Data.Vec.Base as Vec using (Vec)
open import Function using (_∘_; flip)
open import Level using (Level)

private
  variable
    a b : Level
    A : Set a
    B : Set b

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

record Table (A : Set a) n : Set a where
  constructor tabulate
  field lookup : Fin n → A
open Table public

------------------------------------------------------------------------
-- Basic operations

head : ∀ {n} → Table A (suc n) → A
head t = lookup t zero

tail : ∀ {n} → Table A (suc n) → Table A n
tail t = tabulate (lookup t ∘ suc)

uncons : ∀ {n} → Table A (suc n) → A × Table A n
uncons t = head t , tail t

remove : ∀ {n} → Fin (suc n) → Table A (suc n) → Table A n
remove i t = tabulate (lookup t ∘ punchIn i)

------------------------------------------------------------------------
-- Operations for transforming tables

rearrange : ∀ {m n} → (Fin m → Fin n) → Table A n → Table A m
rearrange f t = tabulate (lookup t ∘ f)

map : ∀ {n} → (A → B) → Table A n → Table B n
map f t = tabulate (f ∘ lookup t)

_⊛_ : ∀ {n} → Table (A → B) n → Table A n → Table B n
fs ⊛ xs = tabulate λ i → lookup fs i (lookup xs i)

------------------------------------------------------------------------
-- Operations for reducing tables

foldr : ∀ {n} → (A → B → B) → B → Table A n → B
foldr {n = zero}  f z t = z
foldr {n = suc n} f z t = f (head t) (foldr f z (tail t))

foldl : ∀ {n} → (B → A → B) → B → Table A n → B
foldl {n = zero}  f z t = z
foldl {n = suc n} f z t = foldl f (f z (head t)) (tail t)

------------------------------------------------------------------------
-- Operations for building tables

replicate : ∀ {n} → A → Table A n
replicate x = tabulate (λ _ → x)

------------------------------------------------------------------------
-- Operations for converting tables

toList : ∀ {n} → Table A n → List A
toList = List.tabulate ∘ lookup

fromList : ∀ (xs : List A) → Table A (List.length xs)
fromList = tabulate ∘ List.lookup

fromVec : ∀ {n} → Vec A n → Table A n
fromVec = tabulate ∘ Vec.lookup

toVec : ∀ {n} → Table A n → Vec A n
toVec = Vec.tabulate ∘ lookup


text:
{-# OPTIONS --cubical-compatible #-}
-- Large indices are not allowed --cubical-compatible

data Singleton {a} {A : Set a} : A → Set where
  [_] : ∀ x → Singleton x


text:
------------------------------------------------------------------------
-- Bounded vectors (inefficient, concrete implementation)
------------------------------------------------------------------------

-- Vectors of a specified maximum length.

module Data.BoundedVec.Inefficient where

open import Data.Nat
open import Data.List

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

data BoundedVec (a : Set) : ℕ → Set where
  []  : ∀ {n} → BoundedVec a n
  _∷_ : ∀ {n} (x : a) (xs : BoundedVec a n) → BoundedVec a (suc n)

------------------------------------------------------------------------
-- Increasing the bound

-- Note that this operation is linear in the length of the list.

↑ : ∀ {a n} → BoundedVec a n → BoundedVec a (suc n)
↑ []       = []
↑ (x ∷ xs) = x ∷ ↑ xs

------------------------------------------------------------------------
-- Conversions

fromList : ∀ {a} → (xs : List a) → BoundedVec a (length xs)
fromList []       = []
fromList (x ∷ xs) = x ∷ fromList xs

toList : ∀ {a n} → BoundedVec a n → List a
toList []       = []
toList (x ∷ xs) = x ∷ toList xs

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Control.Monad.Levels.Mult where

open import Prelude
open import Control.Monad.Levels.Definition
open import Control.Monad.Levels.Eliminators
open import Control.Monad.Levels.Zipping
open import Data.Bag hiding (bind)
open import Path.Reasoning

open import Cubical.Foundations.HLevels using (isOfHLevelΠ)

bind-alg : (A → Levels B) → Levels-ϕ[ A ] Levels B
[ bind-alg f ]-set = trunc
[ bind-alg f ] x ∷ _ ⟨ xs ⟩ = zip (⟦ levels-cmon ⟧ trunc f x) ([] ∷ xs)
[ bind-alg f ][] = []
[ bind-alg f ]-trail = trail

bind : Levels A → (A → Levels B) → Levels B
bind xs f = bind-alg f ↓ xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground