text:
{-# OPTIONS --without-K --safe #-}
-- The Underlying category of an Enriched category over a Monoidal category V
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Core renaming (Category to Setoid-Category)

module Categories.Enriched.Category.Underlying {o ℓ e} {V : Setoid-Category o ℓ e}
                                    (M : Monoidal V) where

open import Level
open import Function using (_$_)

open import Categories.Enriched.Category
open import Categories.Category.Helper
open import Categories.Category.Monoidal.Properties M using (module Kelly's)
open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
open import Categories.Morphism.Reasoning V
import Categories.Morphism.IsoEquiv V as IsoEquiv

open Setoid-Category V renaming (Obj to ObjV; id to idV)
open Monoidal M
open Shorthands
open IsoEquiv._≃_

-- A V-category C does not have morphisms of its own, but the
-- collection of V-morphisms from the monoidal unit into the
-- hom-objects of C forms a setoid.  This induces the *underlying*
-- category of C.

Underlying : {c : Level} (C : Category M c) → Setoid-Category c ℓ e
Underlying C = categoryHelper (record
  { Obj = Obj
  ; _⇒_ = λ A B → unit ⇒ hom A B
  ; _≈_ = λ f g → f ≈ g
  ; id  = id
  ; _∘_ = λ f g → ⊚ ∘ f ⊗₁ g ∘ λ⇐
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} →
    begin
      ⊚ ∘ (⊚ ∘ h ⊗₁ g ∘ λ⇐) ⊗₁ f ∘ λ⇐                 ≈˘⟨ refl⟩∘⟨ assoc ⟩⊗⟨refl ⟩∘⟨refl ⟩
      ⊚ ∘ ((⊚ ∘ h ⊗₁ g) ∘ λ⇐) ⊗₁ f ∘ λ⇐                ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩
      ⊚ ∘ (⊚ ∘ h ⊗₁ g) ⊗₁ f ∘ (λ⇐ ⊗₁ idV) ∘ λ⇐        ≈⟨ pullˡ ⊚-assoc-var ⟩
      (⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ α⇒) ∘ (λ⇐ ⊗₁ idV) ∘ λ⇐ ≈˘⟨ pushˡ (pushʳ (pushʳ
                                                            (switch-tofromˡ associator (to-≈ Kelly's.coherence-iso₁)))) ⟩
      (⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ λ⇐) ∘ λ⇐                ≈⟨ pullʳ (pullʳ unitorˡ-commute-to) ⟩
      ⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ idV ⊗₁ λ⇐ ∘ λ⇐           ≈˘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
      ⊚ ∘ h ⊗₁ ((⊚ ∘ g ⊗₁ f) ∘ λ⇐) ∘ λ⇐                ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩
      ⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f ∘ λ⇐) ∘ λ⇐
    ∎
  ; identityˡ = λ {_} {_} {f} → begin
      ⊚ ∘ id ⊗₁ f ∘ λ⇐                 ≈⟨ refl⟩∘⟨ serialize₁₂ ⟩∘⟨refl ⟩
      ⊚ ∘ (id ⊗₁ idV ∘ idV ⊗₁ f) ∘ λ⇐  ≈˘⟨ refl⟩∘⟨ pushʳ unitorˡ-commute-to ⟩
      ⊚ ∘ id ⊗₁ idV ∘ λ⇐ ∘ f           ≈⟨ pullˡ unitˡ ⟩
      λ⇒ ∘ λ⇐ ∘ f                       ≈⟨ cancelˡ unitorˡ.isoʳ ⟩
      f                                ∎
  ; identityʳ = λ {_} {_} {f} → begin
      ⊚ ∘ f ⊗₁ id ∘ λ⇐                 ≈⟨ refl⟩∘⟨ serialize₂₁ ⟩∘⟨refl ⟩
      ⊚ ∘ (idV ⊗₁ id ∘ f ⊗₁ idV) ∘ λ⇐  ≈⟨ pullˡ (pullˡ unitʳ) ⟩
      (unitorʳ.from ∘ f ⊗₁ idV) ∘ λ⇐   ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟩
      (f ∘ unitorʳ.from) ∘ λ⇐          ≈˘⟨ (refl⟩∘⟨ Kelly's.coherence₃) ⟩∘⟨refl ⟩
      (f ∘ λ⇒) ∘ λ⇐                    ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
      f                                ∎
  ; equiv    = equiv
  ; ∘-resp-≈ = λ eq₁ eq₂ → ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ⊗-resp-≈ eq₁ eq₂
  })
  where open Category C

module Underlying {c} (C : Category M c) = Setoid-Category (Underlying C)

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax UTLC | Λ

type
  * : 0-ary

term
  app  : *  *  ->  * | _$_ l20
  lam  : *.*  ->  * | ƛ_ r10

theory
  (ƛβ) b : *.*  a : * |> app (lam (x.b[x]), a) = b[a]
  (ƛη) f : *          |> lam (x.app (f, x))    = f
  (lβ) b : *.*  a : * |> letd (a, x. b) = b[a]
-}

module UTLC.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data Λₒ : Set where
  appₒ lamₒ : Λₒ

-- Term signature
Λ:Sig : Signature Λₒ
Λ:Sig = sig λ
  {  appₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  lamₒ   → (* ⊢₁ *) ⟼₁ *
  }

open Signature Λ:Sig public

ext: agda

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module InterpretCommand where

open import ParseTree
open import Data.List
open import Data.Nat
open import ScopeState
open import Data.Sum hiding (map)
open import Data.Bool
open import Data.String hiding (_++_)
open import Data.Maybe hiding (map)
open import Data.Product hiding (map)
open import AgdaHelperFunctions

getRange : ParseTree -> Range
getRange (signature _ range₁) = range₁
getRange (functionDefinition _ _ _ range₁) = range₁
getRange (dataStructure _ _ _ _ range₁) = range₁
getRange (pragma _ range₁) = range₁
getRange (openImport _ _ _ range₁) = range₁
getRange (moduleName _ range₁) = range₁

_<=_ : ℕ -> ℕ -> Bool
zero <= zero = true
zero <= suc m = true
suc n <= zero = false
suc n <= suc m = n <= m

isInRange : Range -> ℕ -> Bool
isInRange (range lastUnaffected lastAffected) what = ((lastUnaffected + 1) <= what) ∧ (what <= (lastAffected + 1))

firstActualValue : {A : Set} -> List (Maybe A) -> Maybe A
firstActualValue [] = nothing
firstActualValue (just x ∷ list) = just x
firstActualValue (nothing ∷ list) = firstActualValue list

findInIdentifier : ℕ -> Identifier -> Maybe ℕ
findInIdentifier n (identifier name isInRange₁ scope declaration)
  with isInRange₁ n
... | inside = just declaration
... | x = nothing

findInSignature : ℕ -> TypeSignature -> Maybe ℕ

findInExpr : ℕ -> Expr -> Maybe ℕ
findInExpr n numLit = nothing
findInExpr n (ident i) = findInIdentifier n i
findInExpr n hole = nothing
findInExpr n (functionApp e e₁) = firstActualValue (findInExpr n e ∷ findInExpr n e₁ ∷ [])
findInExpr n (implicit e) = findInExpr n e
findInExpr n underscore = nothing
findInExpr n (namedArgument arg) = findInSignature n arg

findInSignature n (typeSignature funcName funcType) =
  firstActualValue (findInIdentifier n funcName ∷ findInExpr n funcType ∷ [])

findInParseTree : ℕ -> ParseTree -> Maybe ℕ
findInParseTree n (signature signature₁ range₁) = findInSignature n signature₁
findInParseTree n (functionDefinition definitionOf params body range₁) =
  firstActualValue (findInIdentifier n definitionOf ∷ findInExpr n body ∷ map (findInExpr n) params)
findInParseTree n (dataStructure dataName parameters indexInfo constructors range₁) = firstActualValue ((findInIdentifier n dataName ∷ findInExpr n indexInfo ∷ map (findInSignature n) parameters) ++ map (findInSignature n) constructors)
findInParseTree n (pragma (builtin concept definition) range₁) =
  findInIdentifier n definition
findInParseTree _ _ = nothing

getDeclarationIDForPoint : List ParseTree -> ℕ -> Maybe ℕ
getDeclarationIDForPoint [] point = nothing
getDeclarationIDForPoint (x ∷ list) point with isInRange (getRange x) point
getDeclarationIDForPoint (x ∷ list) point | false =
  getDeclarationIDForPoint list point
getDeclarationIDForPoint (x ∷ list) point | true = findInParseTree point x

-- for argument rearranging

--TODO fix this when adding more detailed source position data
getArgNumber : ℕ -> ℕ -> Expr -> ScopeState ℕ
getArgNumber point currArgNumber (functionApp t t₁ {true}) = do
  just _ <- return $ findInExpr point t
    where _ -> getArgNumber point (currArgNumber + 1) t₁
  return currArgNumber
getArgNumber point currArgNumber t = fail "Point seems to be in result."

getFuncIdAndArgNumberInParseTree : ℕ -> ParseTree -> ScopeState (ℕ × ℕ)
getFuncIdAndArgNumberInParseTree n (signature (typeSignature (identifier name isInRange₁ scope declaration) funcType) range₁) = do
    argNum <- getArgNumber n zero funcType
    return $ declaration , argNum
getFuncIdAndArgNumberInParseTree _ _ = fail "Point not in signature"

getFuncIdAndArgNumber : List ParseTree -> ℕ -> ScopeState (ℕ × ℕ)
getFuncIdAndArgNumber [] point = fail "Point not in code"
getFuncIdAndArgNumber (x ∷ list) point with isInRange (getRange x) point
getFuncIdAndArgNumber (x ∷ list) point | false =
  getFuncIdAndArgNumber list point
getFuncIdAndArgNumber (x ∷ list) point | true = getFuncIdAndArgNumberInParseTree point x


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

open import Fragment.Algebra.Signature

module Fragment.Equational.Theory.Laws (Σ : Signature) where

open import Fragment.Equational.Theory.Base using (Eq)

open import Function using (_∘_)
open import Data.Empty using (⊥)
open import Data.Fin using (#_)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (_,_)
import Relation.Binary.PropositionalEquality as PE

open import Fragment.Algebra.Free Σ
open import Fragment.Algebra.Free.Syntax Σ (PE.setoid ⊥)

module _ where

  private
    a = # 0

  dne : ops Σ 1 → Eq Σ 1
  dne ~ = ⟨ ~ ⟩₁ ⟨ ~ ⟩₁ ⟨ a ⟩ , ⟨ a ⟩

module _ (e : ops Σ 0) where

  private
    a = # 0

  idₗ : ops Σ 2 → Eq Σ 1
  idₗ • = ⟨ e ⟩₀ ⟨ • ⟩₂ ⟨ a ⟩ , ⟨ a ⟩

  idᵣ : ops Σ 2 → Eq Σ 1
  idᵣ • = ⟨ a ⟩ ⟨ • ⟩₂ ⟨ e ⟩₀ , ⟨ a ⟩

  anₗ : ops Σ 2 → Eq Σ 1
  anₗ • = ⟨ e ⟩₀ ⟨ • ⟩₂ ⟨ a ⟩ , ⟨ e ⟩₀

  anᵣ : ops Σ 2 → Eq Σ 1
  anᵣ • = ⟨ a ⟩ ⟨ • ⟩₂ ⟨ e ⟩₀ , ⟨ e ⟩₀

  invₗ : ops Σ 1 → ops Σ 2 → Eq Σ 1
  invₗ ~ • = (⟨ ~ ⟩₁ ⟨ a ⟩) ⟨ • ⟩₂ ⟨ a ⟩ , ⟨ e ⟩₀

  invᵣ : ops Σ 1 → ops Σ 2 → Eq Σ 1
  invᵣ ~ • = ⟨ a ⟩ ⟨ • ⟩₂ (⟨ ~ ⟩₁ ⟨ a ⟩) , ⟨ e ⟩₀

module _ where

  private

    a = # 0
    b = # 1
    c = # 2

  hom : ops Σ 1 → ∀ {n} → ops Σ n → Eq Σ n
  hom h {n} f =
      ⟨ h ⟩₁ term f (map ⟨_⟩ (allFin n))
    ,
      term f (map (⟨ h ⟩₁_ ∘ ⟨_⟩) (allFin n))
    where open import Data.Vec using (map; allFin)

  comm : ops Σ 2 → Eq Σ 2
  comm • = ⟨ a ⟩ ⟨ • ⟩₂ ⟨ b ⟩ , ⟨ b ⟩ ⟨ • ⟩₂ ⟨ a ⟩

  assoc : ops Σ 2 → Eq Σ 3
  assoc • =
      (⟨ a ⟩ ⟨ • ⟩₂ ⟨ b ⟩) ⟨ • ⟩₂ ⟨ c ⟩
    ,
      ⟨ a ⟩ ⟨ • ⟩₂ (⟨ b ⟩ ⟨ • ⟩₂ ⟨ c ⟩)

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------------
-- Properties of the mirror function
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesATP using ( reverse-[x]≡[x] )
open import FOTC.Program.Mirror.Forest.PropertiesATP
open import FOTC.Program.Mirror.Forest.TotalityATP
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Tree.TotalityATP
open import FOTC.Program.Mirror.Type

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

mirror-involutive : ∀ {t} → Tree t → mirror · (mirror · t) ≡ t
helper            : ∀ {ts} → Forest ts →
                    reverse (map mirror (reverse (map mirror ts))) ≡ ts

mirror-involutive (tree d fnil) = prf
  where postulate prf : mirror · (mirror · node d []) ≡ node d []
        {-# ATP prove prf #-}

mirror-involutive (tree d (fcons {t} {ts} Tt Fts)) = prf
  where postulate prf : mirror · (mirror · node d (t ∷ ts)) ≡ node d (t ∷ ts)
        {-# ATP prove prf helper #-}

helper fnil = prf
  where postulate prf : reverse (map mirror (reverse (map mirror []))) ≡ []
        {-# ATP prove prf #-}

helper (fcons {t} {ts} Tt Fts) =
  prf (map-++ mirror
              mirror-Tree
              (reverse-Forest (map-Forest mirror mirror-Tree Fts))
              (mirror · t ∷ []))
      (mirror-involutive Tt)
      (helper Fts)
  where
  postulate
    -- We help the ATPs proving the first hypothesis.
    prf : (map mirror (reverse (map mirror ts) ++ (mirror · t ∷ [])) ≡
          map mirror
              (reverse (map mirror ts)) ++ (map mirror (mirror · t ∷ []))) →
          mirror · (mirror · t) ≡ t →
          reverse (map mirror (reverse (map mirror ts))) ≡ ts →
          reverse (map mirror (reverse (map mirror (t ∷ ts)))) ≡ t ∷ ts
  {-# ATP prove prf reverse-∷ mirror-Tree map-Forest reverse-++
                    reverse-Forest reverse-[x]≡[x] #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module RecordUpdateSyntax where

open import Common.Prelude
open import Common.Equality

data Param : Nat → Set where
  param : ∀ n → Param (suc n)

record R : Set where
  field
    {i} : Nat
    p : Param i
    s : Nat

old : R
old = record { p = param 0; s = 1 }

-- Simple update, it should be able to infer the type and the implicit.
new : _
new = record old { p = param 1 }

new′ : R
new′ = record { i = 2; p = param 1; s = 1 }

-- Here's a needlessly complex update.
upd-p-s : _ → _ → _ → R
upd-p-s zero s r = record r { p = param zero; s = s }
upd-p-s (suc n) s r = record (upd-p-s n 0 r) { p = param n; s = s }

eq₁ : new ≡ new′
eq₁ = refl

eq₂ : upd-p-s zero 1 (record new { s = 0 }) ≡ old
eq₂ = refl

-- Check that instance arguments are handled properly
postulate
  T : Nat → Set
  instance
    t0 : T 0
    t1 : T 1

record Instance : Set where
  field
    n : Nat
    {{t}} : T n

r0 : Instance
r0 = record { n = 0 }

r1 : Instance
r1 = record r0 { n = 1 }

check : Instance.t r1 ≡ t1
check = refl


text:
module Thesis.Derive where

open import Thesis.Lang
open import Thesis.Changes
open import Thesis.LangChanges
open import Thesis.LangOps
open import Relation.Binary.PropositionalEquality

Γ≼ΔΓ : ∀ {Γ} → Γ ≼ ΔΓ Γ
Γ≼ΔΓ {∅} = ∅
Γ≼ΔΓ {τ • Γ} = drop Δt τ • keep τ • Γ≼ΔΓ

fit : ∀ {τ Γ} → Term Γ τ → Term (ΔΓ Γ) τ
fit = weaken Γ≼ΔΓ

⟦Γ≼ΔΓ⟧ : ∀ {Γ ρ1 ρ2 dρ} → (dρρ : [ Γ ]Γ dρ from ρ1 to ρ2) →
  ρ1 ≡ ⟦ Γ≼ΔΓ ⟧≼ dρ
⟦Γ≼ΔΓ⟧ v∅ = refl
⟦Γ≼ΔΓ⟧ (dvv v• dρρ) = cong₂ _•_ refl (⟦Γ≼ΔΓ⟧ dρρ)

fit-sound : ∀ {Γ τ} → (t : Term Γ τ) →
  ∀ {dρ ρ1 ρ2} → [ Γ ]Γ dρ from ρ1 to ρ2 →
  ⟦ t ⟧Term ρ1 ≡ ⟦ fit t ⟧Term dρ
fit-sound t dρρ = trans
  (cong ⟦ t ⟧Term (⟦Γ≼ΔΓ⟧ dρρ))
  (sym (weaken-sound t _))

deriveConst : ∀ {τ} →
  Const τ →
  Term ∅ (Δt τ)

deriveConst unit = const unit
deriveConst (lit n) = const (lit (+ 0))
deriveConst plus = abs (abs (abs (abs (app₂ (const plus) (var (that (that this))) (var this)))))
-- minus = λ m n → m - n
-- dminus = λ m dm n dn → (m + dm) - (n + dn) - (m - n) = dm - dn
deriveConst minus = abs (abs (abs (abs (app₂ (const minus) (var (that (that this))) (var this)))))
deriveConst cons = abs (abs (abs (abs (app (app (const cons) (var (that (that this)))) (var this)))))
deriveConst fst = abs (abs (app (const fst) (var this)))
deriveConst snd = abs (abs (app (const snd) (var this)))
deriveConst linj = abs (abs (app (const linj) (app (const linj) (var this))))
deriveConst rinj = abs (abs (app (const linj) (app (const rinj) (var this))))
deriveConst (match {t1} {t2} {t3}) =
  -- λ s ds f df g dg →
  abs (abs (abs (abs (abs (abs
    -- match ds
    (app₃ (const match) (var (that (that (that (that this)))))
      -- λ ds₁ → match ds₁
      (abs (app₃ (const match) (var this)
        -- case inj₁ da → absV 1 (λ da → match s
        (abs (app₃ (const match) (var (that (that (that (that (that (that (that this))))))))
          -- λ a → app₂ df a da
          (abs (app₂ (var (that (that (that (that (that this)))))) (var this) (var (that this))))
          -- absurd: λ b → dg b (nil b)
          (abs (app₂ (var (that (that (that this)))) (var this) (app (onilτo t2) (var this))))))
        -- case inj₂ db → absV 1 (λ db → match s
        (abs (app₃ (const match) (var (that (that (that (that (that (that (that this))))))))
          -- absurd: λ a → df a (nil a)
          (abs (app₂ (var (that (that (that (that (that this)))))) (var this) (app (onilτo t1) (var this))))
          -- λ b → app₂ dg b db
          (abs (app₂ (var (that (that (that this)))) (var this) (var (that this))))))))
      -- recomputation branch:
      -- λ s2 → ominus (match s2 (f ⊕ df) (g ⊕ dg)) (match s f g)
      (abs (app₂ (ominusτo t3)
        -- (match s2 (f ⊕ df) (g ⊕ dg))
        (app₃ (const match)
          (var this)
          (app₂ (oplusτo (t1 ⇒ t3))
            (var (that (that (that (that this)))))
            (var (that (that (that this)))))
          (app₂ (oplusτo (t2 ⇒ t3))
            (var (that (that this)))
            (var (that this))))
        -- (match s f g)
        (app₃ (const match)
          (var (that (that (that (that (that (that this)))))))
          (var (that (that (that (that this)))))
          (var (that (that this))))))))))))

{-
derive (λ s f g → match s f g) =
λ s ds f df g dg →
case ds of
 ch1 da →
   case s of
     inj1 a → df a da
     inj2 b → {- absurd -} dg b (nil b)
  ch2 db →
   case s of
     inj2 b → dg b db
     inj1 a → {- absurd -} df a (nil a)
  rp s2 →
    match (f ⊕ df) (g ⊕ dg) s2 ⊝
    match f g s
-}

derive-var : ∀ {Γ τ} → Var Γ τ → Var (ΔΓ Γ) (Δt τ)
derive-var this = this
derive-var (that x) = that (that (derive-var x))

derive : ∀ {Γ τ} → Term Γ τ → Term (ΔΓ Γ) (Δt τ)
derive (const c) = weaken (∅≼Γ {ΔΓ _}) (deriveConst c)
derive (var x) = var (derive-var x)
derive (app s t) = app (app (derive s) (fit t)) (derive t)
derive (abs t) = abs (abs (derive t))

⟦_⟧ΔVar : ∀ {Γ τ} → (x : Var Γ τ) → (ρ : ⟦ Γ ⟧Context) (dρ : ChΓ Γ) → Chτ τ
⟦ x ⟧ΔVar ρ dρ = ⟦ derive-var x ⟧Var dρ

⟦_⟧ΔTerm : ∀ {Γ τ} → (t : Term Γ τ) → (ρ : ⟦ Γ ⟧Context) (dρ : ChΓ Γ) → Chτ τ
⟦ t ⟧ΔTerm ρ dρ = ⟦ derive t ⟧Term dρ

⟦_⟧ΔConst : ∀ {τ} (c : Const τ) → Chτ τ
⟦ c ⟧ΔConst = ⟦ deriveConst c ⟧Term ∅

⟦_⟧ΔConst-rewrite : ∀ {τ Γ} (c : Const τ) (ρ : ⟦ Γ ⟧Context) dρ → ⟦_⟧ΔTerm (const c) ρ dρ ≡ ⟦ c ⟧ΔConst
⟦ c ⟧ΔConst-rewrite ρ dρ rewrite weaken-sound {Γ₁≼Γ₂ = ∅≼Γ} (deriveConst c) dρ | ⟦∅≼Γ⟧-∅ dρ = refl

module _ {t1 t2 t3 : Type}
  (f : ⟦ t1 ⟧Type → ⟦ t3 ⟧Type)
  (df : Chτ (t1 ⇒ t3))
  (g : ⟦ t2 ⟧Type → ⟦ t3 ⟧Type)
  (dg : Chτ (t2 ⇒ t3))
  where
  private
    Γ : Context
    Γ = sum t1 t2 •
      (t2 ⇒ Δt t2 ⇒ Δt t3) •
      (t2 ⇒ t3) •
      (t1 ⇒ Δt t1 ⇒ Δt t3) •
      (t1 ⇒ t3) •
      sum (sum (Δt t1) (Δt t2)) (sum t1 t2) •
      sum t1 t2 • ∅
  module _ where
    private
      Γ′ Γ′′ : Context
      Γ′ = t2 • (t2 ⇒ Δt t2 ⇒ Δt t3) • (t2 ⇒ t3) • Γ
      Γ′′ = t2 • Γ′
    changeMatchSem-lem1 :
      ∀ a1 b2 →
        ⟦ match ⟧ΔConst (inj₁ a1) (inj₂ (inj₂ b2)) f df g dg
      ≡
        g b2 ⊕ dg b2 (nil b2) ⊝ f a1
    changeMatchSem-lem1 a1 b2 rewrite ominusτ-equiv-ext t2 Γ′′ | oplusτ-equiv-ext t3 Γ′ | ominusτ-equiv-ext t3 Γ = refl
  module _ where
    private
      Γ′ Γ′′ : Context
      Γ′ = t1 • (t1 ⇒ Δt t1 ⇒ Δt t3) • (t1 ⇒ t3) • Γ
      Γ′′ = t1 • Γ′
    changeMatchSem-lem2 :
      ∀ b1 a2 →
        ⟦ match ⟧ΔConst (inj₂ b1) (inj₂ (inj₁ a2)) f df g dg
      ≡
        f a2 ⊕ df a2 (nil a2) ⊝ g b1
    changeMatchSem-lem2 b1 a2 rewrite ominusτ-equiv-ext t1 Γ′′ | oplusτ-equiv-ext t3 Γ′ | ominusτ-equiv-ext t3 Γ = refl
  module _ where
    private
      Γ′ Γ′′ : Context
      Γ′ = t1 • (t1 ⇒ Δt t1 ⇒ Δt t3) • (t1 ⇒ t3) • Γ
      Γ′′ = t1 • Γ′
    changeMatchSem-lem3 :
      ∀ a1 a2 →
        ⟦ match ⟧ΔConst (inj₁ a1) (inj₂ (inj₁ a2)) f df g dg ≡
        f a2 ⊕ df a2 (nil a2) ⊝ f a1
    changeMatchSem-lem3 a1 a2 rewrite ominusτ-equiv-ext t1 Γ′′ | oplusτ-equiv-ext t3 Γ′ | ominusτ-equiv-ext t3 Γ = refl
  module _ where
    private
      Γ′ Γ′′ : Context
      Γ′ = t2 • (t2 ⇒ Δt t2 ⇒ Δt t3) • (t2 ⇒ t3) • Γ
      Γ′′ = t2 • Γ′
    changeMatchSem-lem4 :
      ∀ b1 b2 →
        ⟦ match ⟧ΔConst (inj₂ b1) (inj₂ (inj₂ b2)) f df g dg
      ≡
        g b2 ⊕ dg b2 (nil b2) ⊝ g b1
    changeMatchSem-lem4 b1 b2 rewrite ominusτ-equiv-ext t2 Γ′′ | oplusτ-equiv-ext t3 Γ′ | ominusτ-equiv-ext t3 Γ = refl

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module z where

------------------------------------------------------------------------------
-- 1 intro

-- data types

data Nat : Set where
  zero :       Nat
  suc  : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

--------------------------------------------------
-- begin : from later - here to use in tests
data Bool : Set where
  true  : Bool
  false : Bool

data IsTrue : Bool → Set where
  is-true : IsTrue true

_=Nat_ : Nat → Nat → Bool
zero    =Nat  zero   = true
(suc x) =Nat (suc y) = x =Nat y
_       =Nat  _      = false
-- end : from later
--------------------------------------------------

-- pattern matching

_+_ : Nat → Nat → Nat
zero    + y =          y
(suc x) + y = suc (x + y)
infixl 9 _+_
-- {-# BUILTIN NATPLUS _+_ #-}

-- ex 1.1
halve : Nat → Nat
halve       zero    = zero
halve (suc  zero)   = zero
halve (suc (suc n)) = suc (halve n)

halve-0  : IsTrue (halve   0 =Nat 0)
halve-0  = is-true
halve-1  : IsTrue (halve   1 =Nat 0)
halve-1  = is-true
halve-2  : IsTrue (halve   2 =Nat 1)
halve-2  = is-true
halve-3  : IsTrue (halve   3 =Nat 1)
halve-3  = is-true
halve-4  : IsTrue (halve   4 =Nat 2)
halve-4  = is-true
halve-14 : IsTrue (halve  14 =Nat 7)
halve-14 = is-true
halve-15 : IsTrue (halve  15 =Nat 7)
halve-15 = is-true
halve-16 : IsTrue (halve  16 =Nat 8)
halve-16 = is-true

-- ex 1.2
_*_ : Nat → Nat → Nat
zero    * y    = zero
(suc x) * y = y + (x * y)

2*0 : IsTrue ((2 * 0) =Nat  0)
2*0 = is-true
2*1 : IsTrue ((2 * 1) =Nat  2)
2*1 = is-true
2*2 : IsTrue ((2 * 2) =Nat  4)
2*2 = is-true
3*3 : IsTrue ((3 * 3) =Nat  9)
3*3 = is-true
4*4 : IsTrue ((4 * 4) =Nat 16)
4*4 = is-true

{-
-- ex 1.3
data Bool : Set where
  true  : Bool
  false : Bool
-}

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

_&&_ : Bool → Bool → Bool
_&&_ true  y = y
_&&_ false _ = false

_||_ : Bool → Bool → Bool
_||_ true  _ = true
_||_ false y = y

-- types are 1st class
-- equivalent to Haskell type alias : type MyNat = Nat
MyNat : Set
MyNat = Nat

-- Set used to implement polymorphic functions
idA : (A : Set) → A → A
idA _ x = x

-- implicit args
id : {A : Set} → A → A
id  x = x

-- polymorphic data types
data List (A : Set) : Set where
  []   :              List A
  _::_ : A → List A → List A
infixr 5 _::_

-- ex 1.4
length : {A : Set} → List A → Nat
length       []  = zero
length (_ :: xs) = 1 + length xs

_++_ :  {A : Set} → List A → List A → List A
_++_       []  l2 =            l2
_++_ (x :: xs) l2 = x :: xs ++ l2

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

-- ex 1.5
data Maybe (A : Set) : Set where
  just    : A → Maybe A
  nothing :     Maybe A

lookup : {A : Set} → List A → Nat → Maybe A
lookup       []       _  = nothing
lookup (x ::  _)  zero   = just x
lookup (_ :: xs) (suc n) = lookup xs n

_=List-Nat_ : List Nat → List Nat → Bool
[]        =List-Nat       []  = true
(x :: xs) =List-Nat (y :: ys) = (x =Nat y) && (xs =List-Nat ys)
_         =List-Nat        _  = false

ex-xs  : List Nat
ex-xs  = 0 :: 1 :: 2 :: 3 :: []

length++ : IsTrue ((length ex-xs + length ex-xs) =Nat (length (ex-xs ++ ex-xs)))
length++ = is-true

map2* : IsTrue (map (2 *_) ex-xs =List-Nat (0 :: 2 :: 4 :: 6 :: []))
map2* = is-true

_=Maybe-Nat_ : Maybe Nat → Maybe Nat → Bool
nothing   =Maybe-Nat  nothing  = true
(just x)  =Maybe-Nat  (just y) = x =Nat y
_         =Maybe-Nat        _  = false

lookup[]0    : IsTrue (lookup    [] 0 =Maybe-Nat nothing)
lookup[]0    = is-true
lookupex-xs0 : IsTrue (lookup ex-xs 0 =Maybe-Nat (just 0))
lookupex-xs0 = is-true
lookupex-xs1 : IsTrue (lookup ex-xs 1 =Maybe-Nat (just 1))
lookupex-xs1 = is-true
lookupex-xs9 : IsTrue (lookup ex-xs 9 =Maybe-Nat nothing)
lookupex-xs9 = is-true

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B
infixr 4 _,_

fst : {A B : Set} → A × B → A
fst (a , _) = a

snd : {A B : Set} → A × B → B
snd (_ , b) = b

-- ex 1.6
-- NO.  Regardless of the value of 'Nat', there is NO way to construct an A if given [].

------------------------------------------------------------------------------
-- 2 dependent types

--      parameter         : bound for ENTIRE def
--                  index : varies according to constructor
--          v         v
data Vec (A : Set) : Nat → Set where              -- Vec is dependent TYPE
  []   :                           Vec A 0
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)
--infixr 5 _::_

-- dependent FUNCTION : return TYPE depends on inputs
zeroes : (n : Nat) → Vec Nat n
zeroes  zero   = []
zeroes (suc n) = 0 :: zeroes n

-- ex 2.1
downFrom : (n : Nat) → Vec Nat n
downFrom   zero  = []
downFrom (suc n) = n :: downFrom n

_=Vec-Nat_ : {n : Nat} → Vec Nat n → Vec Nat n → Bool
[]        =Vec-Nat       []  = true
(x :: xs) =Vec-Nat (y :: ys) = (x =Nat y) && (xs =Vec-Nat ys)

downFrom0 : IsTrue (downFrom 0 =Vec-Nat                                     [])
downFrom0 = is-true
downFrom1 : IsTrue (downFrom 1 =Vec-Nat                               (0 :: []))
downFrom1 = is-true
downFrom2 : IsTrue (downFrom 2 =Vec-Nat                          (1 :: 0 :: []))
downFrom2 = is-true
downFrom3 : IsTrue (downFrom 3 =Vec-Nat                     (2 :: 1 :: 0 :: []))
downFrom3 = is-true
downFrom7 : IsTrue (downFrom 7 =Vec-Nat (6 :: 5 :: 4 :: 3 :: 2 :: 1 :: 0 :: []))
downFrom7 = is-true

-- ex 2.2
tail : {A : Set} {n : Nat} → Vec A (suc n) → Vec A n
tail (_ :: xs) = xs

-- ex 2.3
dotProduct : {n : Nat} → Vec Nat n → Vec Nat n → Nat
dotProduct       []        []  = 0
dotProduct (x :: xs) (y :: ys) = (x * y) + dotProduct xs ys

dotProduct32 : IsTrue (dotProduct (1 :: 2 :: 3 :: []) (1 :: 5 :: 7 :: []) =Nat 32)
dotProduct32 = is-true

-- finite type family
data Fin : Nat → Set where
  zero : {n : Nat} →         Fin (suc n)
  suc  : {n : Nat} → Fin n → Fin (suc n)

lookupVec : {A : Set} {n : Nat} → Vec A n → Fin n → A
lookupVec       []   ()
lookupVec (x ::  _)  zero   = x
lookupVec (_ :: xs) (suc i) = lookupVec xs i

-- ex 2.4
putVec : {A : Set} {n : Nat} → Fin n → A → Vec A n → Vec A n
putVec  zero   a (_ :: xs) = a ::            xs
putVec (suc i) a (x :: xs) = x :: putVec i a xs

ex-vxs  : Vec Nat 4
ex-vxs  = 0 :: 1 :: 2 :: 3 :: []

lookupVecex-vxs0 : IsTrue (lookupVec ex-vxs                zero    =Nat 0)
lookupVecex-vxs0 = is-true
lookupVecex-vxs3 : IsTrue (lookupVec ex-vxs (suc (suc (suc zero))) =Nat 3)
lookupVecex-vxs3 = is-true

putVecex-vxs3 : IsTrue (putVec (suc (suc zero)) 22 ex-vxs  =Vec-Nat (0 :: 1 :: 22 :: 3 :: []))
putVecex-vxs3 = is-true

{-
dependent pair type - aka Σ type

aka Σ type because can be seen as sum (or disjoint union) of all the types B x
- where 1st component is viewed as a label indicating
  which type of the family the 2nd belong to

generalization of pair type A × B
- where type of 2nd component can be different depending on value of 1st
- e.g.,                   Σ Nat (Vec Bool)
        (or equivalently, Σ Nat (λn → Vec Bool n))
 contains elements
        2 , (true :: false :: [])
 and
        0 , []
 but not
        2 , [] (since [] does not have type Vec Bool 2).
-}

--               function
--                  v
data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

-- see Σ as generalization of normal pair : normal pair ignores its input
_×'_ : (A B : Set) → Set
A ×' B = Σ A (λ _ → B)

-- ex 2.5
×-to-×' : {A B : Set} → (A × B) → (A ×' B)
×-to-×' (a , b) =  a , b

×'-to-× : {A B : Set} → (A ×' B) → (A × B)
×'-to-× (a , b) =  a , b

-- Σ USE CASE : hide type info

-- e.g., hide length of vector

List' : (A : Set) → Set
List' A = Σ Nat (Vec A)

-- ex 2.6
list-to-vec : {A : Set} → (l : List A) → Vec A (length l)
list-to-vec       []  = []
list-to-vec (x :: xs) = x :: list-to-vec xs

vec-to-list : {A : Set} {n : Nat} → Vec A n → List A
vec-to-list       []  = []
vec-to-list (x :: xs) = x :: vec-to-list xs

list-to-list' : {A : Set} → List A → List' A
list-to-list' l = length l , list-to-vec l

list'-to-list : {A : Set} → List' A → List A
list'-to-list (_ , v) = vec-to-list v

-- if Nat relations existed at this point this function would be very different
lookup-List' : {A : Set} → List' A -> Nat -> Maybe A
lookup-List' (_ ,       [])       _  =  nothing
lookup-List' (_ , (x ::  _))  zero   = just x
lookup-List' (_ , (_ :: xs)) (suc n) = lookup-List' ((list-to-list' (vec-to-list xs))) n

ex-l'xs  : List' Nat
ex-l'xs  = (4 , 0 :: 1 :: 2 :: 3 :: [])

lookup-List'[]0      : IsTrue (lookup-List' (0 , []) 0 =Maybe-Nat nothing)
lookup-List'[]0      = is-true
lookup-List'ex-l'xs0 : IsTrue (lookup-List'  ex-l'xs 0 =Maybe-Nat (just 0))
lookup-List'ex-l'xs0 = is-true
lookup-List'ex-l'xs1 : IsTrue (lookup-List'  ex-l'xs 1 =Maybe-Nat (just 1))
lookup-List'ex-l'xs1 = is-true
lookup-List'ex-l'xs9 : IsTrue (lookup-List'  ex-l'xs 9 =Maybe-Nat nothing)
lookup-List'ex-l'xs9 = is-true

------------------------------------------------------------------------------
-- 3 The Curry-Howard correspondence
-- can interpret logical propositions — such as “P and Q”, “not P”, “P implies Q”, ...
-- as types whose inhabitants are valid proofs of that proposition.

--------------------------------------------------
-- PROPOSITIONAL LOGIC

-- ex 3.1
data Either (A B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

cases : {A B C : Set} → Either A B → (A → C) → (B → C) → C
cases (left  a) fac   _ = fac a
cases (right b) _   fbc = fbc b

cases-left  : IsTrue (cases (left  3) (2 +_) (2 *_) =Nat 5)
cases-left  = is-true
cases-right : IsTrue (cases (right 3) (2 +_) (2 *_) =Nat 6)
cases-right = is-true

{-
-------------------------
TRUTH : true : the proposition that always holds no matter what.
Proving it is straightforward: do not need to provide any assumptions.
Assuming true in a proof does not provide any new information.
'true' corresponds to the unit type
-}

data ⊤ : Set where
  tt : ⊤

{-
-------------------------
FALSITY. the proposition that is never true.
There are no ways to prove it.
Represented by empty type : datatype with no constructors
-}

data ⊥ : Set where

{-
given a proof p of “false” (which can't happen because no constructors)
- “ex falso quodlibet” : “from falsity follows anything”)
- can can get a proof of any proposition
-}
absurd : {A : Set} → ⊥ → A
absurd ()

{-
-------------------------
NEGATION : the type P → ⊥
EQUIVALENCE. “P is equivalent to Q” as (P → Q) × (Q → P)

Propositional logic versus boolean logic.

types ⊤ and ⊥ seem similar to booleans true and false
- true and false are VALUES : can manipulate and return
- ⊤    and and ⊥ are TYPES
  - not possible to check whether a given type ⊤ or ⊥
-}

curryCompose : {P Q R : Set} → (P → Q) × (Q → R) -> (P → R)
curryCompose (f , g) = λ x → g (f x)

-- ex 3.2
if-A-then-B-implies-A : {A B : Set} → A → (B → A)
if-A-then-B-implies-A a = λ _ → a

if-A-and-true-then-A-or-false : {A : Set} → (A × ⊤) → Either A ⊥
if-A-and-true-then-A-or-false (a , ⊤) = left a

uncurry : {A B C : Set} → (A → (B → C)) → (A × B) → C
uncurry f = λ a×b → f (fst a×b) (snd a×b)

ex32x : {A B C : Set} → (A × Either B C) → Either (A × B) (A × C)
ex32x (a , left  b) = left  (a , b)
ex32x (a , right c) = right (a , c)

ex32y : {A B C D : Set} → ((A → C) × (B → D)) → (A × B) → (C × D)
ex32y (ac , bd) (a , b) = ac a , bd b

{-
--------------------------------------------------
-- PREDICATE LOGIC

to prove propositions that say something about a given VALUE or FUNCTION

e.g., 6 is even
      length (map f xs) is equal to length xs for all xs
      there exists a number n such that n + n = 12

Curry-Howard : propositions are types

can define new propositions by defining new data types

e.g.,
-}

--           index
--             v
data IsEven : Nat → Set where
  even-zero :                        IsEven  zero
  even-suc2 : {n : Nat} → IsEven n → IsEven (suc (suc n))

6-is-even : IsEven 6
6-is-even = even-suc2 (even-suc2 (even-suc2 even-zero))

7-is-not-even : IsEven 7 → ⊥
7-is-not-even (even-suc2 (even-suc2 (even-suc2 ())))
--                                             ^   -- absurb pattern as arg

{-
-- useful predicate
-- states that a given Bool is true
data IsTrue : Bool → Set where
  is-true : IsTrue true

_=Nat_ : Nat → Nat → Bool
zero    =Nat  zero   = true
(suc x) =Nat (suc y) = x =Nat y
_       =Nat  _      = false
-}

length-is-3 : IsTrue (length (1 :: 2 :: 3 :: []) =Nat 3)
length-is-3 = is-true

{-
Defining properties as functions.

Can define properties as
- data types, or
- functions that return a value of type Set
e..g.,
-}

IsTrue’ : Bool → Set
IsTrue’ true  = ⊤
IsTrue’ false = ⊥

{-
Function approach often results in proofs that are shorter, but less readable.

Also less general, as some types (e.g., identity type in next section)
can only be defined as a data type.

BEST PRACTICE: use data types (not functions)

--------------------------------------------------
UNIVERSAL QUANTIFICATION : “∀ x of type A, P(x)”

to prove : provide proof of P(v) for EVERY concrete value v : A.

i.e., a function λv → P v

in opposite direction
assume a f of “∀ x of type A, P(x)”
and given a concrete v : A
then can the proof to the case of v to get a proof f v of P(v)

under Curry-Howard, universal quantification corresponds to dependent function
  (x : A) → P x
-}

double : Nat → Nat
double  zero   = zero
double (suc n) = suc (suc (double n))

-- ∀ n : Nat, double n is an even number
-- 'double-is-even' is a dependent function : return TYPE depends on input VALUE
-- pattern matching here is "proof by cases"
-- recursion here is "induction on n"
double-is-even : (n : Nat) → IsEven (double n)
double-is-even  zero   = even-zero
double-is-even (suc m) = even-suc2 (double-is-even m)

n-equals-n : (n : Nat) → IsTrue (n =Nat n)
n-equals-n  zero   = is-true
n-equals-n (suc m) = n-equals-n m

{-
--------------------------------------------------
EXISTENTIAL QUANTIFICATION : “∃ a x : A such that P( x )”

to prove : provide a concrete v : A, and a proof that P(v) holds

i.e. a pair (v : A, P v)

in opposite direction
given proof z of “∃ a x : A such that P( x )”
then extract the witness fst z : A
and the proof snd z : P (fst z)

under Curry-Howard, existential quantification corresponds to the dependent pair type
  Σ A ( λ x → P x ).
-}

-- ∃ an n such that n + n = 12
half-a-dozen : Σ Nat (λ n → IsTrue ((n + n) =Nat 12))
half-a-dozen = 6 , is-true

-- any number n is either 0 or the successor of another number m
-- ∀ n, n is 0
-- or ∃ m such that n is suc m
zero-or-suc : (n : Nat) → Either (IsTrue (n =Nat 0))
                                 (Σ Nat (λ m → IsTrue (n =Nat (suc m))))
zero-or-suc  zero   = left is-true
zero-or-suc (suc m) = right (m , n-equals-n m)

{-
--------------------------------------------------

Propositional logic                              Type System
------------------------------------------------------------
proposition                  P                   type
proof of a proposition       p : P               program of a type
conjunction                  P × Q               pair type
disjunction                  Either P Q          either type
implication                  P → Q               function type
truth                        ⊤                   unit type
falsity                      ⊥                   empty type
negation                     P → ⊥               function to ⊥
equivalence                  (P → Q) × (Q → P)   pair of two functions
------------------------------------------------------------
Predicate log
universal quantification     (x : A) → P x       dependent function type
existential quantification   Σ A (λ x → P x )    dependent pair type

--------------------------------------------------
-- IDENTITY TYPE : EQUALITY at any type (to avoid =Nat, =Vec-Nat, ...)

Martin-Löf introduced a new type x ≡ y, called the IDENTITY TYPE (NOT FUNCTION)

if x and y are equal, then x ≡ y has a single inhabitant refl
- behaves like the unit type ⊤

if x and y are distinct, then x ≡ y has no constructors
- behaves like the empty type ⊥
-}

data _≡_ {A : Set} : A → A → Set where
  -- ‘reflexivity’
  refl : {x : A} → x ≡ x
infix 4 _≡_
{-# BUILTIN EQUALITY _≡_ #-}

one-plus-one-IsTrue : IsTrue ((1 + 1) =Nat 2)
one-plus-one-IsTrue = is-true

one-plus-one : 1 + 1 ≡ 2
one-plus-one = refl

{-
zero-not-one-not-IsTrue : IsTrue (0 =Nat 1)
zero-not-one-not-IsTrue = {!!}
-}

zero-not-one : 0 ≡ 1 → ⊥
zero-not-one ()

-- prove facts about polymorphic types
id-returns-input : {A : Set}
                 → (x : A)
                 → id x ≡ x
id-returns-input _ = refl

-- unit tests using identity type
length-test1 : length (1 :: 2 :: []) ≡ 2
length-test1 = refl

-- symmetry of equality
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

-- transitivity of equality
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

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

{-
If a and b can be unified by instantiating some of the variables, then can match on refl.
If a and b are different (e.g. different constructors), then match on absurb pattern ().
Agda canNOT always tell if they are different.
-}

------------------------------------------------------------------------------
-- 4 EQUATIONAL REASONING

begin_ : {A : Set} → {x y : A} → x ≡ y → x ≡ y
begin p = p

_end : {A : Set} → (x : A) → x ≡ x
x end = refl

_=⟨_⟩_ : {A : Set} → (x : A) → {y z : A} → x ≡ y → y ≡ z → x ≡ z
x =⟨ p ⟩ q = trans p q

_=⟨⟩_  : {A : Set} → (x : A) → {y   : A} → x ≡ y         → x ≡ y
x =⟨⟩ q = x =⟨ refl ⟩ q

infix 1 begin_
infix 3 _end
infixr 2 _=⟨_⟩_
infixr 2 _=⟨⟩_

-- create singleton list
[_] : {A : Set} → A → List A
[ x ] = x :: []

reverse : {A : Set} → List A → List A
reverse       []  = []
reverse (x :: xs) = reverse xs ++ [ x ]

-- reverse has no effect on singleton lists
reverse-singleton : {A : Set}
                  → (x : A)
                  → reverse [ x ] ≡ [ x ]
reverse-singleton x =
  begin
  reverse       [ x ]  =⟨⟩ -- definition of [_]
  reverse   (x :: [])  =⟨⟩ -- applying reverse (second clause)
  reverse [] ++ [ x ]  =⟨⟩ -- applying reverse (first clause)
          [] ++ [ x ]  =⟨⟩ -- applying _++_
                [ x ]
  end

-- proof by cases and induction
not-not : (b : Bool)
        → not (not b) ≡ b

not-not true  =
  begin
  not (not true) =⟨⟩
       not false =⟨⟩ -- apply inner not
           true      -- apply not
  end

not-not false =
  begin
  not (not false) =⟨⟩
       not true   =⟨⟩
           false
  end

-- prove fact about Nat by induction (i.e., recursion)
add-n-zero : (n : Nat)
           → n + zero ≡ n
add-n-zero  zero   =
  begin
  zero + zero =⟨⟩
  zero        =⟨⟩
  zero
  end

add-n-zero (suc n) =
  begin
  (suc n) + zero  =⟨⟩                          -- applying +
  suc (n  + zero) =⟨ cong suc (add-n-zero n) ⟩ -- using induction hypothesis
  suc n
  end

add-n-zero' : (n : Nat)
            → n + zero ≡ n
add-n-zero'  zero   = refl
add-n-zero' (suc n) = cong suc (add-n-zero' n)

add-assoc : (x y z : Nat)
          → x + (y + z) ≡ (x + y) + z
add-assoc zero y z =
  begin
  zero + (y + z) =⟨⟩ -- def of +
          y + z  =⟨⟩ -- unapply +
  (zero + y) + z
  end
add-assoc (suc x) y z =
  begin
     (suc   x) + (y   + z)  =⟨⟩ -- def of +
      suc  (x  + (y   + z)) =⟨ cong suc (add-assoc x y z) ⟩ -- inductive hypo
      suc ((x  +  y)  + z)  =⟨⟩ -- unapply outer add
     (suc  (x  +  y)) + z   =⟨⟩ -- unapply inner add
    ((suc   x) +  y)  + z
  end

-- ex 4.1
add-suc : (m n : Nat)
        → m + suc n ≡ suc (m + n)
add-suc zero n    =
  begin
  zero + suc n =⟨⟩ -- def of +
         suc n =⟨⟩
  suc (zero + n)
  end
add-suc (suc m) n = -- cong suc (add-suc m n)
  begin
  suc m + suc n    =⟨⟩ -- def of +
  suc (m + suc n)  =⟨ cong suc (add-suc m n) ⟩
  suc (suc m + n)
  end

--use add-suc and add-n-zero
+-comm : (m n : Nat)
       → m + n ≡ n + m
+-comm zero n = sym (add-n-zero n)
+-comm (suc m) n
  rewrite                 -- suc  m     +     n  ≡ n + suc m
                          -- suc (m     +     n) ≡ n + suc m
    +-comm m n            -- suc (n     +     m) ≡ n + suc m
  | sym (add-suc n m)     --      n     + suc m  ≡ n + suc m
  = refl

+-comm' : (m n : Nat)
        → m + n ≡ n + m
+-comm' zero n =
  begin
  zero + n =⟨⟩                     -- def of +
         n =⟨ sym (add-n-zero n) ⟩ -- add zero to right
  n + zero
  end
+-comm' (suc m) n =
  begin
  suc  m     +     n  =⟨⟩ -- def of +
  suc (m     +     n) =⟨ cong suc (+-comm m n) ⟩
  suc (n     +     m) =⟨ sym (add-suc n m) ⟩
       n     + suc m
  end

--------------------------------------------------
-- induction on lists

-- ex 4.2
replicate : {A : Set} → Nat → A → List A
replicate  zero   x = []
replicate (suc n) x = x :: replicate n x

length-replicate : {A : Set} {a : A}
                 → (n : Nat)
                 → length (replicate n a) ≡ n
length-replicate  zero   = refl
length-replicate (suc n) = cong suc (length-replicate n)

-- ex 4.3
append-[] : {A : Set}
          → (xs : List A)
          → xs ++ [] ≡ xs
append-[]       []  = refl
append-[] (x :: xs) = cong (x ::_) (append-[] xs)

append-assoc : {A : Set}
             → (xs ys zs : List A)
             → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
append-assoc       []  ys zs = refl
append-assoc (x :: xs) ys zs -- (((x ::   xs) ++ ys) ++ zs) ≡ ((x ::  xs) ++ (ys ++ zs))
                             --    x :: ((xs  ++ ys) ++ zs) ≡   x :: (xs  ++ (ys ++ zs))
  = cong (x ::_) (append-assoc xs ys zs)

reverse-distributivity : {A : Set}
                       → (xs ys : List A)
                       → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-distributivity       []  ys = sym (append-[] (reverse ys))
reverse-distributivity (x :: xs) ys
                   -- reverse ((x :: xs) ++ ys)         ≡ (reverse ys ++  reverse       (x :: xs))
                   -- (reverse (xs ++ ys) ++ (x :: [])) ≡ (reverse ys ++ (reverse xs ++ (x :: [])))
  rewrite
    reverse-distributivity xs ys
                   -- ((reverse ys ++ reverse xs) ++ (x :: []))
                   --                                   ≡ (reverse ys ++ (reverse xs ++ (x :: [])))
  | sym (append-assoc (reverse ys) (reverse xs) (x :: []))
  = refl

reverse-reverse : {A : Set}
                → (xs : List A)
                → reverse (reverse xs) ≡ xs
reverse-reverse       [] = refl
reverse-reverse (x :: xs) -- reverse (reverse (x :: xs))       ≡ x :: xs
                          -- reverse (reverse xs ++ (x :: [])) ≡ x :: xs
  rewrite
    --                       NOTE
    --                        v
    reverse-distributivity (reverse xs) [ x ]
                          --         x :: reverse (reverse xs) ≡ x :: xs
-- can rewrite here then refl
--| reverse-reverse xs    --                          x :: xs  ≡ x :: xs
--= refl
-- or use 'cong' on rightof '='
  = cong (x ::_) (reverse-reverse xs)

{-
map satisfies functor laws:
- identity    : map id      = id
- composition : map (g . h) = map g . h
-}

map-id : {A : Set}
       → (xs : List A)
       → map id xs ≡ xs
map-id       []  = refl
map-id (x :: xs) --         map id (x :: xs) ≡ x :: xs
                 -- id x :: map id       xs  ≡ x :: xs
  = cong (x ::_) (map-id xs)

_◦_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
g ◦ h = λ x → g (h x)

map-compose : {A B C : Set}
            → (f : B → C) → (g : A → B) → (xs : List A)
            → map (f ◦ g) xs ≡ map f (map g xs)
map-compose f g       [] = refl
map-compose f g (x :: xs)
                         --              map (f ◦ g) (x :: xs) ≡            map f (map g (x :: xs))
                         -- (f ◦ g) x :: map (f ◦ g)       xs  ≡ f (g x) :: map f (map g       xs)
{- this
  rewrite
    sym (map-compose f g xs)
                         --   f (g x) :: map (λ x₁ → f (g x₁)) xs ≡
                              f (g x) :: map (λ x₁ → f (g x₁)) xs
  = refl
-}
  -- or this
  = cong (f (g x) ::_) (map-compose f g xs)

-- ex 4.4
length-map : {A B : Set} {f : A → B}
           → (xs : List A)
           → length (map f xs) ≡ length xs
length-map       []  = refl
length-map (x :: xs) --      length (map f (x :: xs)) ≡      length (x :: xs)
                     -- suc (length (map f       xs)) ≡ suc (length       xs)
  = cong suc (length-map xs)

-- ex 4.5
take : {A : Set} → List A → Nat → List A
take        _   zero   = []
take       []  (suc n) = []
take (x :: xs) (suc n) = x :: take xs n

take-0 : take ex-xs 0 ≡ []
take-0 = refl
take-1 : take ex-xs 1 ≡ 0 :: []
take-1 = refl
take-2 : take ex-xs 2 ≡ 0 :: 1 :: []
take-2 = refl
take-3 : take ex-xs 3 ≡ 0 :: 1 :: 2 :: []
take-3 = refl
take-4 : take ex-xs 4 ≡ ex-xs
take-4 = refl
take-5 : take ex-xs 5 ≡ ex-xs
take-5 = refl

drop : {A : Set} → List A → Nat → List A
drop       xs   zero   = xs
drop       []  (suc x) = []
drop (_ :: xs) (suc n) = drop xs n

drop-0 : drop ex-xs 0 ≡ ex-xs
drop-0 = refl
drop-1 : drop ex-xs 1 ≡ 1 :: 2 :: 3 :: []
drop-1 = refl
drop-2 : drop ex-xs 2 ≡      2 :: 3 :: []
drop-2 = refl
drop-3 : drop ex-xs 3 ≡           3 :: []
drop-3 = refl
drop-4 : drop ex-xs 4 ≡                []
drop-4 = refl
drop-5 : drop ex-xs 5 ≡                []
drop-5 = refl

take-drop : {A : Set} → (xs : List A) → (n : Nat) → take xs n ++ drop xs n ≡ xs
take-drop       []   zero   = refl
take-drop       []  (suc n) = refl
take-drop (x :: xs)  zero   = refl
take-drop (x :: xs) (suc n) --      (take (x :: xs) (suc n) ++ drop (x :: xs) (suc n)) ≡ x :: xs
                            -- x :: (take       xs       n  ++ drop       xs       n)  ≡ x :: xs
  = cong (x ::_) (take-drop xs n)

--------------------------------------------------
-- verifying optimizations

-- list optimization

reverse-acc : {A : Set} → List A → List A → List A
reverse-acc       []  ys = ys
reverse-acc (x :: xs) ys = reverse-acc xs (x :: ys)

reverse' : {A : Set} → List A → List A
reverse' xs = reverse-acc xs []

reverse-acc-lemma : {A : Set}
                  → (xs ys : List A)
                  → reverse-acc xs ys ≡ reverse xs ++ ys
reverse-acc-lemma       []   _ = refl
reverse-acc-lemma (x :: xs) ys   -- reverse-acc (x :: xs) ys  ≡  (reverse (x :: xs)        ++ ys)
                                 -- reverse-acc xs (x :: ys)  ≡ ((reverse xs ++ (x :: [])) ++ ys)
  rewrite
    append-assoc (reverse xs) [ x ] ys
                                 -- reverse-acc xs (x :: ys)  ≡ (reverse xs ++ (x :: ys))
  | reverse-acc-lemma xs (x :: ys)
                                 -- (reverse xs ++ (x :: ys)) ≡ (reverse xs ++ (x :: ys))
  = refl

reverse'-reverse : {A : Set}
                 → (xs : List A)
                 → reverse' xs ≡ reverse xs
reverse'-reverse       []  = refl
reverse'-reverse (x :: xs)     --  reverse' (x :: xs)       ≡  reverse (x :: xs)
                               --  reverse' (x :: xs)       ≡ (reverse xs ++ (x :: []))
  rewrite
    reverse-acc-lemma xs [ x ] -- (reverse xs ++ (x :: [])) ≡ (reverse xs ++ (x :: []))
  = refl

-- tree optimization

data Tree (A : Set) : Set where
  leaf : A               → Tree A
  node : Tree A → Tree A → Tree A

flatten : {A : Set} → Tree A → List A
flatten (leaf a)     = [ a ]
flatten (node t1 t2) = flatten t1 ++ flatten t2

flatten-acc : {A : Set} → Tree A → List A → List A
flatten-acc (leaf x)     xs = x :: xs
flatten-acc (node t1 t2) xs = flatten-acc t1 (flatten-acc t2 xs)

flatten' : {A : Set} → Tree A → List A
flatten' t = flatten-acc t []

flatten-acc-lemma : {A : Set}
                  → (t : Tree A) → (ys : List A)
                  → flatten-acc t ys ≡ flatten t ++ ys
flatten-acc-lemma (leaf x)    _ = refl
flatten-acc-lemma (node t1 t2) ys
                     --  flatten-acc (node t1 t2) ys         ≡  (flatten (node t1 t2)      ++ ys)
                     --  flatten-acc t1 (flatten-acc t2 ys)  ≡ ((flatten t1 ++ flatten t2) ++ ys)
  rewrite
    flatten-acc-lemma t1 (flatten-acc t2 ys)
                     -- (flatten t1 ++   flatten-acc t2 ys)  ≡ ((flatten t1 ++ flatten t2) ++ ys)
  | flatten-acc-lemma t2 ys
                     -- (flatten t1 ++  (flatten t2 ++  ys)) ≡ ((flatten t1 ++ flatten t2) ++ ys)
  | append-assoc (flatten t1) (flatten t2) ys
                     -- (flatten t1 ++  (flatten t2 ++  ys)) ≡  (flatten t1 ++ (flatten t2 ++ ys))
  = refl

flatten-acc-flatten : {A : Set}
                    → (t : Tree A) → (ys : List A)
                    → flatten-acc t ys ≡ flatten t ++ ys
flatten-acc-flatten (leaf x)     ys = refl
                      --  flatten-acc (leaf x)           ys   ≡  (flatten (leaf x)          ++ ys)
flatten-acc-flatten (node t1 t2) ys
                      --  flatten-acc (node t1 t2)       ys   ≡  (flatten (node t1 t2)      ++ ys)
                      --  flatten-acc t1 (flatten-acc t2 ys)  ≡ ((flatten t1 ++ flatten t2) ++ ys)
  rewrite
    flatten-acc-lemma t2 ys
                      --  flatten-acc t1 (flatten t2 ++  ys)  ≡ ((flatten t1 ++ flatten t2) ++ ys)
  | flatten-acc-lemma t1 (flatten t2 ++ ys)
                      -- (flatten t1 ++  (flatten t2 ++  ys)) ≡ ((flatten t1 ++ flatten t2) ++ ys)

  | append-assoc (flatten t1) (flatten t2) ys
                      -- (flatten t1 ++  (flatten t2 ++  ys)) ≡  (flatten t1 ++ (flatten t2 ++ ys))
  = refl

-- ex 4.6
flatten'-flatten : {A : Set}
                 → (t : Tree A)
                 → flatten' t ≡ flatten t
flatten'-flatten (leaf x)     = refl
flatten'-flatten (node t1 t2)
                    -- flatten' (node t1 t2)              ≡  flatten (node t1 t2)
                    -- flatten' (node t1 t2)              ≡ (flatten t1 ++ flatten t2)
  rewrite
    sym (flatten-acc-flatten t1 (flatten t2))
                    -- flatten-acc t1 (flatten-acc t2 []) ≡ flatten-acc t1 (flatten t2)
  | flatten-acc-flatten t2 []
                    -- flatten-acc t1 (flatten t2 ++  []) ≡ flatten-acc t1 (flatten t2)
  | append-[] (flatten t2)
                    -- flatten-acc t1 (flatten t2)        ≡ flatten-acc t1 (flatten t2)
  = refl

--------------------------------------------------
-- compiler correctness

data Expr : Set where
  valE : Nat  →        Expr
  addE : Expr → Expr → Expr

eval : Expr → Nat
eval (valE x)     = x
eval (addE e1 e2) = eval e1 + eval e2

data Op : Set where
  PUSH : Nat → Op
  ADD  : Op

Stack = List Nat
Code  = List Op

exec : Code → Stack → Stack
exec []                       s  = s
exec (PUSH x :: c)            s  = exec c (x :: s)
exec (ADD :: c)    (m :: n :: s) = exec c (n + m :: s)
exec (ADD :: c)               _  = []

compile' : Expr → Code → Code
compile' (valE x) c = PUSH x :: c
compile' (addE e1 e2) c = compile' e1 (compile' e2 (ADD :: c))

compile : Expr → Code
compile e = compile' e []

compile'-exec-eval : (e : Expr) → (s : Stack) → (c : Code)
                   → exec (compile' e c) s ≡ exec c (eval e :: s)
compile'-exec-eval (valE _)     _ _ = refl
compile'-exec-eval (addE e1 e2) s c
        -- exec (compile' (addE e1 e2) c)              s ≡ exec c (eval (addE e1 e2) :: s)
        -- exec (compile' e1 (compile' e2 (ADD :: c))) s ≡ exec c (eval e1 + eval e2 :: s)
  rewrite
    compile'-exec-eval e1 s (compile' e2 (ADD :: c))
        -- exec (compile' e2 (ADD :: c)) (eval e1 :: s)  ≡ exec c (eval e1 + eval e2 :: s)
  | compile'-exec-eval e2 (eval e1 :: s) (ADD :: c)
        -- exec c (eval e1 + eval e2 :: s)               ≡ exec c (eval e1 + eval e2 :: s)
  = refl

compile-exec-eval : (e : Expr) → exec (compile e) [] ≡ [ eval e ]
compile-exec-eval e = compile'-exec-eval e [] []

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

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

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


text:
module hott.topology.theorems where

open import hott.topology
open import hott.topology.loopspace.theorems public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


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

module Cubical.Axiom.Omniscience where

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

open import Cubical.Data.Bool
  renaming (Bool to 𝟚; Bool→Type to ⟨_⟩)
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum as Sum

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Relation.Nullary

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- Lesser limited principle of omniscience
--
-- If two decidable predicates cannot both be satisfied, we can
-- determine that one predicate cannot be satisfied.
LLPO : Type ℓ → Type ℓ
LLPO A
  = ∀(P Q : A → 𝟚)
  → (∀ x y → ⟨ P x ⟩ → ⟨ Q y ⟩ → ⊥)
  → ∥ (∀ x → ¬ ⟨ P x ⟩) ⊎ (∀ y → ¬ ⟨ Q y ⟩) ∥₁

isPropLLPO : isProp (LLPO A)
isPropLLPO = isPropΠ3 λ _ _ _ → squash₁

-- As above, but without ensuring propositionality
LLPO∞ : Type ℓ → Type ℓ
LLPO∞ A
  = ∀(P Q : A → 𝟚)
  → (∀ x y → ⟨ P x ⟩ → ⟨ Q y ⟩ → ⊥)
  → (∀ x → ¬ ⟨ P x ⟩) ⊎ (∀ y → ¬ ⟨ Q y ⟩)

LLPO∞→LLPO : LLPO∞ A → LLPO A
LLPO∞→LLPO llpo' P Q ¬both = ∣ llpo' P Q ¬both ∣₁

-- Weak limited principle of omniscience
--
-- It is decidable whether or not a decidable predicate never holds.
WLPO : Type ℓ → Type ℓ
WLPO A = ∀(P : A → 𝟚) → Dec (∀ x → ¬ ⟨ P x ⟩)

WLPO' : Type ℓ → Type ℓ
WLPO' A = ∀(P : A → 𝟚) → Dec (P ≡ const false)

isPropWLPO : isProp (WLPO A)
isPropWLPO = isPropΠ λ P → isPropDec (isPropΠ λ x → isProp¬ ⟨ P x ⟩)

isPropWLPO' : isProp (WLPO' A)
isPropWLPO' = isPropΠ λ P → isPropDec (isSet→ isSetBool P (const false))

module WLPO≃ where
  points : (P : A → 𝟚) → P ≡ const false → ∀ x → ¬ ⟨ P x ⟩
  points P p x = subst (λ Q → ⟨ Q x ⟩) p

  total : (P : A → 𝟚) → (∀ x → ¬ ⟨ P x ⟩) → P ≡ const false
  total P never i x with P x | never x
  ... | false | _ = false
  ... | true  | ¬⊤ = Empty.rec {A = true ≡ false} (¬⊤ _) i

  open Iso

  total≡points : ∀(P : A → 𝟚) → (P ≡ const false) ≡ (∀ x → ¬ ⟨ P x ⟩)
  total≡points P = isoToPath λ where
    .fun → points P
    .inv → total P
    .rightInv never → isPropΠ (λ x → isProp¬ ⟨ P x ⟩) _ never
    .leftInv α≡f → isSet→ isSetBool P (const false) _ α≡f

WLPO≡WLPO' : WLPO A ≡ WLPO' A
WLPO≡WLPO' {A = A} i = (P : A → 𝟚) → Dec (WLPO≃.total≡points P (~ i))

WLPO→LLPO∞ : WLPO A → LLPO∞ A
WLPO→LLPO∞ {A = A} womn P Q ¬both with womn P
... | yes ∀¬P = inl ∀¬P
... | no ¬∀¬P = inr ∀¬Q where
  ∀¬Q : ∀ y → ¬ ⟨ Q y ⟩
  ∀¬Q y Qy = ¬∀¬P (λ x Px → ¬both x y Px Qy)

-- Limited principle of omniscience
--
-- Either a decidable predicate never holds, or it does
LPO : Type ℓ → Type ℓ
LPO A = ∀(P : A → 𝟚) → (∀ x → ¬ ⟨ P x ⟩) ⊎ ∥ Σ[ x ∈ A ] ⟨ P x ⟩ ∥₁

LPO→WLPO : LPO A → WLPO A
LPO→WLPO omn P with omn P
... | inl ∀¬P = yes ∀¬P
... | inr ∃P  = no λ ∀¬P → PT.rec isProp⊥ (uncurry ∀¬P) ∃P

-- As above, but without truncation.
LPO∞ : Type ℓ → Type ℓ
LPO∞ A = ∀(P : A → 𝟚) → (∀ x → ¬ ⟨ P x ⟩) ⊎ (Σ[ x ∈ A ] ⟨ P x ⟩)

LPO∞→LPO : LPO∞ A → LPO A
LPO∞→LPO omn P = Sum.map (idfun _) ∣_∣₁ (omn P)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------------
-- Properties of the divisibility relation
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Divisibility.NotBy0.Properties where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Properties
open import LTC-PCF.Data.Nat.Divisibility.NotBy0
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Data.Nat.Properties

------------------------------------------------------------------------------
-- Any positive number divides 0.
S∣0 : ∀ {n} → N n → succ₁ n ∣ zero
S∣0 {n} Nn = S≢0 , _ , nzero , sym (*-leftZero (succ₁ n))

-- 0 doesn't divide any number.
0∤x : ∀ {n} → ¬ (zero ∣ n)
0∤x (0≢0 , _) = ⊥-elim (0≢0 refl)

-- The divisibility relation is reflexive for positive numbers.
∣-refl-S : ∀ {n} → N n → succ₁ n ∣ succ₁ n
∣-refl-S {n} Nn = S≢0 , _ , nsucc nzero , sym (*-leftIdentity (nsucc Nn))

-- If x divides y and z then x divides y ∸ z.
x∣y→x∣z→x∣y∸z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                       n ≡ k * succ₁ m →
                       o ≡ k' * succ₁ m →
                       n ∸ o ≡ (k ∸ k') * succ₁ m
x∣y→x∣z→x∣y∸z-helper {m} {n} {o} {k} {k'} Nm Nk Nk' h₁ h₂ =
  n ∸ o                          ≡⟨ ∸-leftCong h₁ ⟩
  k * succ₁ m ∸ o                ≡⟨ ∸-rightCong h₂ ⟩
  (k * succ₁ m) ∸ (k' * succ₁ m) ≡⟨ sym (*∸-leftDistributive Nk Nk' (nsucc Nm)) ⟩
  (k ∸ k') * succ₁ m             ∎

x∣y→x∣z→x∣y∸z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n ∸ o
x∣y→x∣z→x∣y∸z nzero Nn No (0≢0 , _) m∣o = ⊥-elim (0≢0 refl)
x∣y→x∣z→x∣y∸z {n = n} {o} (nsucc {m} Nm) Nn No
              (_ , k , Nk , h₁)
              (_ , k' , Nk' , h₂) =
  (λ S≡0 → ⊥-elim (S≢0 S≡0))
  , k ∸ k' , ∸-N Nk Nk' , x∣y→x∣z→x∣y∸z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and z then x divides y + z.
x∣y→x∣z→x∣y+z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                       n ≡ k * succ₁ m →
                       o ≡ k' * succ₁ m →
                       n + o ≡ (k + k') * succ₁ m
x∣y→x∣z→x∣y+z-helper {m} {n} {o} {k} {k'} Nm Nk Nk' h₁ h₂ =
  n + o                          ≡⟨ +-leftCong h₁ ⟩
  k * succ₁ m + o                ≡⟨ +-rightCong h₂ ⟩
  (k * succ₁ m) + (k' * succ₁ m) ≡⟨ sym (*+-leftDistributive Nk Nk' (nsucc Nm)) ⟩
  (k + k') * succ₁ m             ∎

x∣y→x∣z→x∣y+z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n + o
x∣y→x∣z→x∣y+z             nzero          Nn No (0≢0 , _) m∣o = ⊥-elim (0≢0 refl)
x∣y→x∣z→x∣y+z {n = n} {o} (nsucc {m} Nm) Nn No
              (_ , k , Nk , h₁)
              (_ , k' , Nk' , h₂) =
  (λ S≡0 → ⊥-elim (S≢0 S≡0))
  , k + k' , +-N Nk Nk' , x∣y→x∣z→x∣y+z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and y is positive, then x ≤ y.
x∣S→x≤S : ∀ {m n} → N m → N n → m ∣ (succ₁ n) → m ≤ succ₁ n
x∣S→x≤S  nzero         Nn (0≢0 , _)                     = ⊥-elim (0≢0 refl)
x∣S→x≤S (nsucc {m} Nm) Nn (_ , .zero , nzero , Sn≡0*Sm) =
  ⊥-elim (0≢S (trans (sym (*-leftZero (succ₁ m))) (sym Sn≡0*Sm)))
x∣S→x≤S (nsucc {m} Nm) Nn (_ , .(succ₁ k) , nsucc {k} Nk , Sn≡Sk*Sm) =
  subst (λ t₁ → succ₁ m ≤ t₁)
        (sym Sn≡Sk*Sm)
        (subst (λ t₂ → succ₁ m ≤ t₂)
               (sym (*-Sx k (succ₁ m)))
               (x≤x+y (nsucc Nm) (*-N Nk (nsucc Nm))))


text:
{-

Finite Types

This file formalize the notion of Rijke finite type,
which is a direct generalization of Bishop finite set.
Basically, a type is (Rijke) n-finite if its i-th order
homotopy groups πᵢ are Bishop finite for i ≤ n.

Referrences:
  https://github.com/EgbertRijke/OEIS-A000001

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinType.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure

open import Cubical.HITs.SetTruncation

open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.FinSet

private
  variable
    ℓ ℓ' : Level
    n : ℕ
    X : Type ℓ

-- the (Rijke) finite type

isFinType : (n : ℕ) → Type ℓ → Type ℓ
isFinType 0 X = isFinSet ∥ X ∥₂
isFinType (suc n) X = (isFinType 0 X) × ((a b : X) → isFinType n (a ≡ b))

isPropIsFinType : isProp (isFinType n X)
isPropIsFinType {n = 0} = isPropIsFinSet
isPropIsFinType {n = suc n} = isProp× isPropIsFinSet (isPropΠ2 (λ _ _ → isPropIsFinType {n = n}))

-- the type of finite types

FinType : (ℓ : Level)(n : ℕ) → Type (ℓ-suc ℓ)
FinType ℓ n = TypeWithStr ℓ (isFinType n)

-- basic numerical implications

isFinTypeSuc→isFinType : isFinType (suc n) X → isFinType n X
isFinTypeSuc→isFinType {n = 0} p = p .fst
isFinTypeSuc→isFinType {n = suc n} p .fst = p .fst
isFinTypeSuc→isFinType {n = suc n} p .snd a b = isFinTypeSuc→isFinType {n = n} (p .snd a b)

isFinType→isFinType0 : isFinType n X → isFinType 0 X
isFinType→isFinType0 {n = 0} p = p
isFinType→isFinType0 {n = suc n} p = p .fst

isFinTypeSuc→isFinType1 : isFinType (suc n) X → isFinType 1 X
isFinTypeSuc→isFinType1 {n = 0} p = p
isFinTypeSuc→isFinType1 {n = suc n} p .fst = p .fst
isFinTypeSuc→isFinType1 {n = suc n} p .snd a b = isFinType→isFinType0 {n = suc n} (p .snd a b)


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

module Strict where

open import Agda.Builtin.Strict public
open import Level

infixr 0 _$!_
_$!_ : {A : Type a} {B : A → Type b} → (∀ x → B x) → ∀ x → B x
f $! x = primForce x f
{-# INLINE _$!_ #-}

infixr 0 let-bang
let-bang : {A : Type a} {B : A → Type b} → ∀ x → (∀ x → B x) → B x
let-bang = primForce
{-# INLINE let-bang #-}

syntax let-bang v (λ x → e) = let! x =! v in! e

infixr 0 lambda-bang
lambda-bang : {A : Type a} {B : A → Type b} → (∀ x → B x) → ∀ x → B x
lambda-bang f x = primForce x f
{-# INLINE lambda-bang #-}

syntax lambda-bang (λ x → e) = λ! x →! e

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module lambda.stack where

open import Relation.Binary.PropositionalEquality

infixr 40 _▸_
infixl 35 _∈_

data stack (T : Set) : Set where
  ε : stack T
  _▸_ : stack T → T → stack T

data _∈_ {T : Set} (x : T) : stack T → Set where
  here : ∀ {Γ} → x ∈ Γ ▸ x
  there : ∀ {Γ y} → x ∈ Γ → x ∈ Γ ▸ y

data _⊇_ {T : Set} : stack T → stack T → Set where
  bot : ε ⊇ ε
  skip : ∀ {Γ Δ x} → Γ ⊇ Δ → Γ ▸ x ⊇ Δ
  keep : ∀ {Γ Δ x} → Γ ⊇ Δ → Γ ▸ x ⊇ Δ ▸ x

module _ {T : Set} where

  id : ∀ {Γ : stack T} → Γ ⊇ Γ
  id {ε} = bot
  id {Γ ▸ x} = keep id

  shift : ∀ {Γ Δ} {x : T} → Γ ⊇ Δ → x ∈ Δ → x ∈ Γ
  shift bot ()
  shift (skip x) v = there (shift x v)
  shift (keep _) here = here
  shift (keep x) (there y) = there (shift x y)

  shift-id : ∀ {Γ : stack T} {x} → (e : x ∈ Γ) → shift id e ≡ e
  shift-id here = refl
  shift-id (there e) = cong there (shift-id e)

  _∘⊇_ : {Γ Δ Λ : stack T} → Γ ⊇ Δ → Δ ⊇ Λ → Γ ⊇ Λ
  bot ∘⊇ bot = bot
  skip x ∘⊇ y = skip (x ∘⊇ y)
  keep x ∘⊇ skip y = skip (x ∘⊇ y)
  keep x ∘⊇ keep y = keep (x ∘⊇ y)

  ∘⊇-idˡ : {Γ Δ : stack T} → (w : Γ ⊇ Δ) → id ∘⊇ w ≡ w
  ∘⊇-idˡ bot = refl
  ∘⊇-idˡ (skip x) = cong skip (∘⊇-idˡ x)
  ∘⊇-idˡ (keep x) = cong keep (∘⊇-idˡ x)

  ∘⊇-idʳ : {Δ Γ : stack T} → (w : Γ ⊇ Δ) → w ∘⊇ id ≡ w
  ∘⊇-idʳ bot = refl
  ∘⊇-idʳ (skip x) = cong skip (∘⊇-idʳ x)
  ∘⊇-idʳ (keep x) = cong keep (∘⊇-idʳ x)

  ∘⊇-assoc : {Γ Δ Λ Ω : stack T} → (w₁ : Γ ⊇ Δ) → (w₂ : Δ ⊇ Λ) → (w₃ : Λ ⊇ Ω) → (w₁ ∘⊇ w₂) ∘⊇ w₃ ≡ w₁ ∘⊇ (w₂ ∘⊇ w₃)
  ∘⊇-assoc bot bot bot = refl
  ∘⊇-assoc (skip w₁) w₂ w₃ = cong skip (∘⊇-assoc w₁ w₂ w₃)
  ∘⊇-assoc (keep w₁) (skip w₂) w₃ = cong skip (∘⊇-assoc w₁ w₂ w₃)
  ∘⊇-assoc (keep w₁) (keep w₂) (skip w₃) = cong skip (∘⊇-assoc w₁ w₂ w₃)
  ∘⊇-assoc (keep w₁) (keep w₂) (keep w₃) = cong keep (∘⊇-assoc w₁ w₂ w₃)


text:
data ⊥ : Set where

p0 : Set → Set
p0 A = A

p1 : ⊥ → Set
p1 ()

p2 : ⊥ → ⊥
p2 ()

p3 : Set → ⊥
p3 = ?

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
record Additive {ℓ} (A : Set ℓ) : Set ℓ where
  field
    zero : A
    _+_ : A → A → A

open Additive {{...}} public

record Subtractive {ℓ} (A : Set ℓ) {{ADD : Additive A}} : Set ℓ where
  field
    _-_ : A → A → A

  neg : A → A
  neg x = zero - x

open Subtractive {{...}} public

check : ∀ ℓ (A : Set ℓ) (ADD : Additive A) (SUB : Subtractive A {{ADD}}) → A → A
check ℓ A ADD SUB x = Subtractive.neg {ℓ} {A} {{ADD}} SUB x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Prod renaming (_×_ to _×'_)
open import Cubical.Data.Int renaming (_+_ to _+Int_ ; _-_ to _-Int_)
open import Cubical.Data.Unit

open import Cubical.Algebra.Monoid hiding (⟨_⟩)
open import Cubical.Algebra.Semigroup hiding (⟨_⟩)
open import Cubical.Foundations.HLevels

private
  variable
    ℓ : Level

record IsGroup {G : Type ℓ}
               (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where

  no-eta-equality
  constructor isgroup

  field
    isMonoid  : IsMonoid 0g _+_
    inverse   : (x : G) → (x + (- x) ≡ 0g) × ((- x) + x ≡ 0g)

  open IsMonoid isMonoid public

  infixl 6 _-_

  _-_ : G → G → G
  x - y = x + (- y)

  invl : (x : G) → (- x) + x ≡ 0g
  invl x = inverse x .snd

  invr : (x : G) → x + (- x) ≡ 0g
  invr x = inverse x .fst

η-isGroup : {G : Type ℓ} {0g 0g' : G} {_+_ _+'_  : G → G → G} { -_ -'_  : G → G}
         → 0g ≡ 0g'
         → _+_ ≡ _+'_
         → -_ ≡ -'_
         → IsGroup 0g _+_ -_ ≡ IsGroup 0g' _+'_ -'_
η-isGroup id1 id2 id3 i = IsGroup (id1 i) (id2 i) (id3 i)

record Group : Type (ℓ-suc ℓ) where
  no-eta-equality
  constructor group
  field
    Carrier : Type ℓ
    0g      : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    isGroup : IsGroup 0g _+_ -_

  infix  8 -_
  infixr 7 _+_

  open IsGroup isGroup public

Group₀ : Type₁
Group₀ = Group {ℓ-zero}

-- Extractor for the carrier type
⟨_⟩ : Group → Type ℓ
⟨_⟩ = Group.Carrier

isSetGroup : (G : Group {ℓ}) → isSet ⟨ G ⟩
isSetGroup G = Group.isGroup G .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsGroup : {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
              (is-setG : isSet G)
              (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
              (rid : (x : G) → x + 0g ≡ x)
              (lid : (x : G) → 0g + x ≡ x)
              (rinv : (x : G) → x + (- x) ≡ 0g)
              (linv : (x : G) → (- x) + x ≡ 0g)
            → IsGroup 0g _+_ -_
IsGroup.isMonoid (makeIsGroup is-setG assoc rid lid rinv linv) = makeIsMonoid is-setG assoc rid lid
IsGroup.inverse (makeIsGroup is-setG assoc rid lid rinv linv) = λ x → rinv x , linv x

makeGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
            (is-setG : isSet G)
            (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
            (rid : (x : G) → x + 0g ≡ x)
            (lid : (x : G) → 0g + x ≡ x)
            (rinv : (x : G) → x + (- x) ≡ 0g)
            (linv : (x : G) → (- x) + x ≡ 0g)
          → Group
Group.Carrier (makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv) = _
Group.0g (makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv) = 0g
Group._+_ (makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv) = _+_
Group.- makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv = -_
Group.isGroup (makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv) = makeIsGroup is-setG assoc rid lid rinv linv

makeGroup-right : ∀ {ℓ} {A : Type ℓ}
  → (id : A)
  → (comp : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → comp a (comp b c) ≡ comp (comp a b) c)
  → (rUnit : ∀ a → comp a id ≡ a)
  → (rCancel : ∀ a → comp a (inv a) ≡ id)
  → Group
makeGroup-right {A = A} id comp inv set assoc rUnit rCancel =
  makeGroup id comp inv set assoc rUnit lUnit rCancel lCancel
  where
    _⨀_ = comp
    abstract
      lCancel : ∀ a → comp (inv a) a ≡ id
      lCancel a =
        inv a ⨀ a
          ≡⟨ sym (rUnit (comp (inv a) a))  ⟩
        (inv a ⨀ a) ⨀ id
          ≡⟨ cong (comp (comp (inv a) a)) (sym (rCancel (inv a))) ⟩
        (inv a ⨀ a) ⨀ (inv a ⨀ (inv (inv a)))
          ≡⟨ assoc _ _ _ ⟩
        ((inv a ⨀ a) ⨀ (inv a)) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → □ ⨀ _) (sym (assoc _ _ _)) ⟩
        (inv a ⨀ (a ⨀ inv a)) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → (inv a ⨀ □) ⨀ (inv (inv a))) (rCancel a) ⟩
        (inv a ⨀ id) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → □ ⨀ (inv (inv a))) (rUnit (inv a)) ⟩
        inv a ⨀ (inv (inv a))
          ≡⟨ rCancel (inv a) ⟩
        id
          ∎

      lUnit : ∀ a → comp id a ≡ a
      lUnit a =
        id ⨀ a
          ≡⟨ cong (λ b → comp b a) (sym (rCancel a)) ⟩
        (a ⨀ inv a) ⨀ a
          ≡⟨ sym (assoc _ _ _) ⟩
        a ⨀ (inv a ⨀ a)
          ≡⟨ cong (comp a) (lCancel a) ⟩
        a ⨀ id
          ≡⟨ rUnit a ⟩
        a
          ∎

makeGroup-left : ∀ {ℓ} {A : Type ℓ}
  → (id : A)
  → (comp : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → comp a (comp b c) ≡ comp (comp a b) c)
  → (lUnit : ∀ a → comp id a ≡ a)
  → (lCancel : ∀ a → comp (inv a) a ≡ id)
  → Group
makeGroup-left {A = A} id comp inv set assoc lUnit lCancel =
  makeGroup id comp inv set assoc rUnit lUnit rCancel lCancel
  where
    abstract
      rCancel : ∀ a → comp a (inv a) ≡ id
      rCancel a =
        comp a (inv a)
          ≡⟨ sym (lUnit (comp a (inv a)))  ⟩
        comp id (comp a (inv a))
          ≡⟨ cong (λ b → comp b (comp a (inv a))) (sym (lCancel (inv a))) ⟩
        comp (comp (inv (inv a)) (inv a)) (comp a (inv a))
          ≡⟨ sym (assoc (inv (inv a)) (inv a) (comp a (inv a))) ⟩
        comp (inv (inv a)) (comp (inv a) (comp a (inv a)))
          ≡⟨ cong (comp (inv (inv a))) (assoc (inv a) a (inv a)) ⟩
        comp (inv (inv a)) (comp (comp (inv a) a) (inv a))
          ≡⟨ cong (λ b → comp (inv (inv a)) (comp b (inv a))) (lCancel a) ⟩
        comp (inv (inv a)) (comp id (inv a))
          ≡⟨ cong (comp (inv (inv a))) (lUnit (inv a)) ⟩
        comp (inv (inv a)) (inv a)
          ≡⟨ lCancel (inv a) ⟩
        id
          ∎

      rUnit : ∀ a → comp a id ≡ a
      rUnit a =
        comp a id
          ≡⟨ cong (comp a) (sym (lCancel a)) ⟩
        comp a (comp (inv a) a)
          ≡⟨ assoc a (inv a) a ⟩
        comp (comp a (inv a)) a
          ≡⟨ cong (λ b → comp b a) (rCancel a) ⟩
        comp id a
          ≡⟨ lUnit a ⟩
        a
          ∎

open Group
open IsGroup

η-Group : {G H : Group {ℓ}}
       → (p : ⟨ G ⟩ ≡ ⟨ H ⟩)
       → (q : PathP (λ i → p i) (0g G) (0g H))
       → (r : PathP (λ i → (p i) → (p i) → (p i)) (_+_ G) (_+_ H))
       → (s : PathP (λ i → p i → p i) (-_ G) (-_ H))
       → PathP (λ i → IsGroup (q i) (r i) (s i)) (isGroup G) (isGroup H)
       → G ≡ H
Carrier (η-Group p _ _ _ _ i) = p i
0g (η-Group _ q _ _ _ i) = q i
_+_ (η-Group _ _ r _ _ i) = r i
- η-Group _ _ _ s t i = s i
isGroup (η-Group _ _ _ _ t i) = t i

isSetCarrier : ∀ {ℓ} → (G : Group {ℓ}) → isSet ⟨ G ⟩
isSetCarrier G = IsSemigroup.is-set (IsMonoid.isSemigroup (isMonoid G))

open IsMonoid
open IsSemigroup
dirProd : ∀ {ℓ ℓ'} → Group {ℓ} → Group {ℓ'} → Group
Carrier (dirProd A B) = Carrier A × Carrier B
0g (dirProd A B) = (0g A) , (0g B)
_+_ (dirProd A B) a b = (_+_ A (fst a) (fst b)) , _+_ B (snd a) (snd b)
-_ (dirProd A B) a = (-_ A (fst a)) , (-_ B (snd a))
is-set (isSemigroup (isMonoid (isGroup (dirProd A B)))) =
  isOfHLevelΣ 2 (isSetCarrier A) λ _ → isSetCarrier B
assoc (isSemigroup (isMonoid (isGroup (dirProd A B)))) x y z i =
  assoc (isGroup A) (fst x) (fst y) (fst z) i , assoc (isGroup B) (snd x) (snd y) (snd z) i
identity (isMonoid (isGroup (dirProd A B))) x =
   (λ i → IsGroup.rid (isGroup A) (fst x) i , IsGroup.rid (isGroup B) (snd x) i)
 , λ i → IsGroup.lid (isGroup A) (fst x) i , IsGroup.lid (isGroup B) (snd x) i
inverse (isGroup (dirProd A B)) x =
    (λ i → (fst (inverse (isGroup A) (fst x)) i) , (fst (inverse (isGroup B) (snd x)) i))
  , λ i → (snd (inverse (isGroup A) (fst x)) i) , (snd (inverse (isGroup B) (snd x)) i)

trivialGroup : Group₀
Carrier trivialGroup = Unit
0g trivialGroup = _
_+_ trivialGroup _ _ = _
-_ trivialGroup _ = _
is-set (isSemigroup (isMonoid (isGroup trivialGroup))) = isSetUnit
assoc (isSemigroup (isMonoid (isGroup trivialGroup))) _ _ _ = refl
identity (isMonoid (isGroup trivialGroup)) _ = refl , refl
inverse (isGroup trivialGroup) _ = refl , refl

intGroup : Group₀
Carrier intGroup = Int
0g intGroup = 0
_+_ intGroup = _+Int_
- intGroup = 0 -Int_
is-set (isSemigroup (isMonoid (isGroup intGroup))) = isSetInt
assoc (isSemigroup (isMonoid (isGroup intGroup))) = +-assoc
identity (isMonoid (isGroup intGroup)) x = refl , (+-comm (pos 0) x)
inverse (isGroup intGroup) x = +-comm x (pos 0 -Int x) ∙ minusPlus x 0 , (minusPlus x 0)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Sets.PredicateSet.Proofs where

import      Lvl
open import Functional
import      Logic.Propositional          as Logic
import      Logic.Propositional.Theorems as Logic
import      Logic.Predicate
import      Sets.PredicateSet
import      Structure.Relator.Properties
import      Type

-- [⊆][⊇]-equivalence : ∀{A}{B} → (A ⊆ B) ↔ (B ⊇ A)

module _ {ℓₗ}{ℓₒ} {T : Set(ℓₒ)} where
  open Sets.PredicateSet
  open Structure.Relator.Properties

  private
    Stmt = Logic.Stmt{ℓₗ Lvl.⊔ ℓₒ}

    PredSet' : Set(Lvl.𝐒(ℓₗ Lvl.⊔ ℓₒ))
    PredSet' = PredSet{ℓₗ}{ℓₒ} (T)

    _⊆'_ : PredSet' → PredSet' → Stmt
    _⊆'_ = _⊆_ {ℓₗ}{ℓₗ} {ℓₒ} {T}

    _⊇'_ : PredSet' → PredSet' → Stmt
    _⊇'_ = _⊇_ {ℓₗ}{ℓₗ} {ℓₒ} {T}

    _≡'_ : PredSet' → PredSet' → Stmt
    _≡'_ = _≡_ {ℓₗ}{ℓₗ} {ℓₒ} {T}

    -- TODO: PredSet' has a greater level than Stmt? Not possible with Reflexivity or even Logic.Predicate
    -- Refl : (PredSet' → PredSet' → Stmt) → Stmt
    -- Refl(_▫_) = Reflexivity{_}{_} {PredSet'} (_▫_)

    -- TODO: This is alright...
    -- Refl : (T → T → Stmt) → Stmt
    -- Refl(_▫_) = (∀{x : T} → (x ▫ x))

    -- ...but not this
    -- Refl : (PredSet' → PredSet' → Stmt) → Stmt
    -- Refl(_▫_) = (∀{x : PredSet'} → (x ▫ x))

  [⊆]-reflexivity : ∀{A} → (A ⊆' A)
  [⊆]-reflexivity = id

  [⊆]-transitivity : ∀{A B C} → (A ⊆' B) → (B ⊆' C) → (A ⊆' C)
  [⊆]-transitivity ab bc = bc ∘ ab

  [⊆]-antisymmetry : ∀{A B} → (A ⊇' B) → (A ⊆' B) → (A ≡' B)
  [⊆]-antisymmetry = Logic.[∧]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module AsP where

f
  : {A : Set}
  → A
  → A
  → A
f x@y z@w
  = x

g
  : {A : Set}
  → A
  → A
  → A
g x@y z'@w'
  with y
... | _
  = x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
module Lemmachine.Resource where
import Lemmachine.Resource.Universe
open import Data.Product
open import Data.List

private
  module U = Lemmachine.Resource.Universe
  open U using (Code; El)

Hook = Σ Code El
Hooks = List Hook

_⇒_ : {A : Set}{B : A → Set} → (a : A) → B a → (Σ A B)
_⇒_ = _,_

record Resource : Set where
  field
    resourceExists : El U.resourceExists
    serviceAvailable : El U.serviceAvailable
    isAuthorized : El U.isAuthorized
    forbidden : El U.forbidden
    allowMissingPost : El U.allowMissingPost
    malformedRequest : El U.malformedRequest
    uriTooLong : El U.uriTooLong
    knownContentType : El U.knownContentType
    validContentHeaders : El U.validContentHeaders
    validEntityLength : El U.validEntityLength
    options : El U.options
    allowedMethods : El U.allowedMethods
    knownMethods : El U.knownMethods
    deleteResource : El U.deleteResource
    deleteCompleted : El U.deleteCompleted
    postIsCreate : El U.postIsCreate
    createPath : El U.createPath
    processPost : El U.processPost
    contentTypesProvided : El U.contentTypesProvided
    languageAvailable : El U.languageAvailable
    contentTypesAccepted : El U.contentTypesAccepted
    charsetsProvided : El U.charsetsProvided
    encodingsProvided : El U.encodingsProvided
    variances : El U.variances
    isConflict : El U.isConflict
    multipleChoices : El U.multipleChoices
    previouslyExisted : El U.previouslyExisted
    movedPermanently : El U.movedPermanently
    movedTemporarily : El U.movedTemporarily
    lastModified : El U.lastModified
    expires : El U.expires
    generateETag : El U.generateETag
    finishRequest : El U.finishRequest
    body : El U.body

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module _ where

postulate
  U : Set
  u : U

module M (x : U) where
  postulate f : U → U

module M₁ = M (M.f u u)  -- this caused a 'recursive display form' error

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --rewriting #-}
open import HoTT

open import stash.modalities.gbm.GbmUtil

module stash.modalities.JoinAdj {i j k}
  (A : Type i) (B : Type j) (C : Type k) where

  private

    module From (f : B → C) (γ : A → hfiber cst f)
      = JoinRec (fst ∘ γ) f (λ a b → app= (snd (γ a)) b)

    from-β : (f : B → C) (γ : A → hfiber cst f)
             (a : A) (b : B) → ap (From.f f γ) (jglue a b) == app= (snd (γ a)) b
    from-β f γ a b = From.glue-β f γ a b

    to : (A * B → C) → Σ (B → C) (λ f → A → hfiber cst f)
    to φ = φ ∘ right , (λ a → φ (left a) , λ= (λ b → ap φ (glue (a , b))))

    from : Σ (B → C) (λ f → A → hfiber cst f) → A * B → C
    from (f , γ) = From.f f γ

    abstract

      to-from : (ψ : Σ (B → C) (λ f → A → hfiber cst f)) → to (from ψ) == ψ
      to-from (f , γ) = pair= idp (λ= coh)

        where coh : (a : A) → from (f , γ) (left a) , λ= (λ b → ap (from (f , γ)) (glue (a , b))) == γ a
              coh a = pair= idp (ap λ= (λ= (λ b → from-β f γ a b)) ∙ ! (λ=-η (snd (γ a))))

      from-to : (φ : A * B → C) → from (to φ) == φ
      from-to φ = λ= (Join-elim (λ a → idp) (λ b → idp) (λ a b → ↓-==-in (coh a b)))

        where coh : ∀ a b → ap φ (jglue a b) == ap (from (to φ)) (jglue a b) ∙ idp
              coh a b = ap φ (jglue a b)
                           =⟨ ! (app=-β (λ b → ap φ (jglue a b)) b) ⟩
                        app= (λ= (λ b → ap φ (jglue a b))) b
                           =⟨ ! (from-β (fst (to φ)) (snd (to φ)) a b) ⟩
                        ap (From.f (fst (to φ)) (snd (to φ))) (jglue a b)
                           =⟨ ! (∙-unit-r (ap (from (to φ)) (jglue a b))) ⟩
                        ap (from (to φ)) (jglue a b) ∙ idp
                           =∎

  join-adj : (A * B → C) ≃ Σ (B → C) (λ f → A → hfiber cst f)
  join-adj = equiv to from to-from from-to

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- A virtual machine
------------------------------------------------------------------------

module Lambda.VirtualMachine where

open import Category.Monad
open import Category.Monad.Partiality as P
  using (_⊥; never); open P._⊥
open import Codata.Musical.Notation
open import Data.Empty using (⊥-elim)
open import Data.Fin
open import Data.List hiding (lookup)
open import Data.Maybe
open import Data.Nat
open import Data.Product as Prod
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Function.Base
import Level
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  hiding (return)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Relation.Nullary

open RawMonad (P.monad {f = Level.zero})

open import Lambda.Syntax
private module C = Closure Tm

------------------------------------------------------------------------
-- Instruction set

mutual

  -- Instructions.

  data Instr (n : ℕ) : Set where
    var : (x : Fin n) → Instr n
    con : (i : ℕ) → Instr n
    clo : (c : Code (suc n)) → Instr n
    app : Instr n
    ret : Instr n

  -- Code.

  Code : ℕ → Set
  Code n = List (Instr n)

-- Environments and values.

open Closure Code

------------------------------------------------------------------------
-- Compiler

-- The compiler takes a code continuation.

comp : ∀ {n} → Tm n → Code n → Code n
comp (con i)   c = con i ∷ c
comp (var x)   c = var x ∷ c
comp (ƛ t)     c = clo (comp t [ ret ]) ∷ c
comp (t₁ · t₂) c = comp t₁ (comp t₂ (app ∷ c))

-- Environments and values can also be compiled.

mutual

  comp-env : ∀ {n} → C.Env n → Env n
  comp-env []      = []
  comp-env (v ∷ ρ) = comp-val v ∷ comp-env ρ

  comp-val : C.Value → Value
  comp-val (C.con i) = con i
  comp-val (C.ƛ t ρ) = ƛ (comp t [ ret ]) (comp-env ρ)

-- lookup x is homomorphic with respect to comp-env/comp-val.

lookup-hom : ∀ {n} (x : Fin n) ρ →
             lookup (comp-env ρ) x ≡ comp-val (lookup ρ x)
lookup-hom zero    (v ∷ ρ) = PE.refl
lookup-hom (suc x) (v ∷ ρ) = lookup-hom x ρ

------------------------------------------------------------------------
-- Stacks and states

-- Stacks.

data StackElement : Set where
  val : (v : Value) → StackElement
  ret : ∀ {n} (c : Code n) (ρ : Env n) → StackElement

Stack : Set
Stack = List StackElement

-- States.

data State : Set where
  ⟨_,_,_⟩ : ∀ {n} (c : Code n) (s : Stack) (ρ : Env n) → State

------------------------------------------------------------------------
-- Relational semantics of the VM

module Relational where

  infix 4 _⟶_

  data _⟶_ : State → State → Set where
    var : ∀ {n} {x : Fin n} {c s ρ} →
          ⟨ var x ∷ c , s , ρ ⟩ ⟶ ⟨ c , val (lookup ρ x) ∷ s , ρ ⟩
    con : ∀ {n i} {c : Code n} {s ρ} →
          ⟨ con i ∷ c , s , ρ ⟩ ⟶ ⟨ c , val (con i) ∷ s , ρ ⟩
    clo : ∀ {n} {c : Code n} {c′ s ρ} →
          ⟨ clo c′ ∷ c , s , ρ ⟩ ⟶ ⟨ c , val (ƛ c′ ρ) ∷ s , ρ ⟩
    app : ∀ {n} {c : Code n} {v n′} {c′ : Code (suc n′)} {ρ′ s ρ} →
          ⟨ app ∷ c , val v ∷ val (ƛ c′ ρ′) ∷ s , ρ ⟩ ⟶ ⟨ c′ , ret c ρ ∷ s , v ∷ ρ′ ⟩
    ret : ∀ {n} {c : Code n} {v n′} {c′ : Code n′} {ρ′ s ρ} →
          ⟨ ret ∷ c , val v ∷ ret c′ ρ′ ∷ s , ρ ⟩ ⟶ ⟨ c′ , val v ∷ s , ρ′ ⟩

  -- Final (stuck) states.

  Final : State → Set
  Final s = ∄ λ s′ → s ⟶ s′

  -- s ⇓ v means that s is a successful final state, and that the
  -- corresponding value is v.

  infix 4 _⇓_

  data _⇓_ : State → Value → Set where
    final : ∀ {v} → ⟨ [] , val v ∷ [] , [] ⟩ ⇓ v

  -- Sanity check.

  ⇓-final : ∀ {s v} → s ⇓ v → Final s
  ⇓-final final (_ , ())

  -- Crashing stuck states.

  Stuck : State → Set
  Stuck s = Final s × ∄ (λ v → s ⇓ v)

  -- Reflexive transitive closure.

  infix 4 _⟶⋆_

  _⟶⋆_ : State → State → Set
  _⟶⋆_ = Star _⟶_

  -- Infinite sequences of steps.

  infixr 5 _◅_
  infix  4 _⟶∞

  data _⟶∞ : State → Set where
    _◅_ : ∀ {s₁ s₂} (s₁⟶s₂ : s₁ ⟶ s₂) (s₂⟶∞ : ∞ (s₂ ⟶∞)) → s₁ ⟶∞

  -- A variant of _⟶∞ which is easier to use.

  module InfiniteSequence where

    infix  4 _⟶∞′
    infix  3 _⟶∞⟨_⟩
    infixr 2 _⟶⟨_⟩′_ _⟶⋆⟨_⟩′_

    data _⟶∞′ : State → Set where
      _⟶⟨_⟩′_  : ∀ s₁ {s₂} (s₁⟶s₂ : s₁ ⟶ s₂) (s₂⟶∞ : ∞ (s₂ ⟶∞′)) → s₁ ⟶∞′
      _⟶⋆⟨_⟩′_ : ∀ s₁ {s₂} (s₁⟶⋆s₂ : s₁ ⟶⋆ s₂) (s₂⟶∞ : s₂ ⟶∞′) → s₁ ⟶∞′
      _⟶∞⟨_⟩   : ∀ s (s⟶∞ : s ⟶∞′) → s ⟶∞′

    sound : ∀ {s} → s ⟶∞′ → s ⟶∞
    sound (s₁ ⟶⟨ s₁⟶s₂ ⟩′ s₂⟶∞)           = s₁⟶s₂ ◅ ♯ (sound (♭ s₂⟶∞))
    sound (s  ⟶⋆⟨ ε ⟩′ s⟶∞)               = sound s⟶∞
    sound (s₁ ⟶⋆⟨ s₁⟶s₂ ◅ s₂⟶⋆s₃ ⟩′ s₃⟶∞) = s₁⟶s₂ ◅ ♯ (sound (_ ⟶⋆⟨ s₂⟶⋆s₃ ⟩′ s₃⟶∞))
    sound (s  ⟶∞⟨ s⟶∞ ⟩)                  = sound s⟶∞

    complete : ∀ {s} → s ⟶∞ → s ⟶∞′
    complete (s₁⟶s₂ ◅ s₂⟶∞) = _ ⟶⟨ s₁⟶s₂ ⟩′ ♯ complete (♭ s₂⟶∞)

------------------------------------------------------------------------
-- Functional semantics of the VM

module Functional where

  -- The result of running the VM one step.

  data Result : Set where
    continue : (s : State) → Result
    done     : (v : Value) → Result
    crash    : Result

  -- A single step of the computation.

  step : State → Result
  step ⟨ []         ,                 val v ∷ [] , [] ⟩ = done v
  step ⟨ var x  ∷ c ,                          s , ρ  ⟩ = continue ⟨ c  , val (lookup ρ x) ∷ s ,     ρ  ⟩
  step ⟨ con i  ∷ c ,                          s , ρ  ⟩ = continue ⟨ c  , val (con i)      ∷ s ,     ρ  ⟩
  step ⟨ clo c′ ∷ c ,                          s , ρ  ⟩ = continue ⟨ c  , val (ƛ c′ ρ)     ∷ s ,     ρ  ⟩
  step ⟨ app    ∷ c , val v ∷ val (ƛ c′ ρ′) ∷  s , ρ  ⟩ = continue ⟨ c′ , ret c ρ          ∷ s , v ∷ ρ′ ⟩
  step ⟨ ret    ∷ c , val v ∷ ret c′ ρ′     ∷  s , ρ  ⟩ = continue ⟨ c′ , val v            ∷ s ,     ρ′ ⟩
  step _                                                = crash

  -- The VM.

  exec : State → Maybe Value ⊥
  exec s with step s
  ... | continue s′ = later (♯ exec s′)
  ... | done v      = return (just v)
  ... | crash       = return nothing

  -- Equality for partial computations returning Maybe Value.
  --
  -- Note that propositional equality is used for the underlying
  -- values, which can include code components. In other words, if
  -- v₁ ≈ v₂, then any code components in these values have to be
  -- /syntactically/ equal.

  module Equality where

    private
      open module PEq {A : Set} = P.Equality {A = A} _≡_ public
        using (_≈_; now; later; laterˡ)

    open P public using (later⁻¹; now≉never)

    module EqReasoning {A : Set} = P.Reasoning {A = A} PE.isEquivalence

------------------------------------------------------------------------
-- Equivalence proof

module Equivalence where

  open Relational
  open Functional
  open Functional.Equality

  ----------------------------------------------------------------------
  -- Classification of states

  -- Inductive characterisation of states which are stuck and not
  -- final.

  data Crashing : State → Set where
    crash₁  : ∀ {n ρ}                → Crashing (⟨_,_,_⟩ {    n}        []                            []        ρ )
    crash₂  : ∀ {n n′ c ρ′ s ρ}      → Crashing (⟨_,_,_⟩ {    n}        [] (         ret {n′} c ρ′  ∷ s )       ρ )
    crash₃  : ∀ {n v e s ρ}          → Crashing (⟨_,_,_⟩ {    n}        [] (val v  ∷ e              ∷ s )       ρ )
    crash₄  : ∀ {n v₁ v₂ ρ}          → Crashing (⟨_,_,_⟩ {suc n}        [] (         val v₁         ∷ []) (v₂ ∷ ρ))
    crash₅  : ∀ {n c ρ}              → Crashing (⟨_,_,_⟩ {    n} (app ∷ c)                            []        ρ )
    crash₆  : ∀ {n c v ρ}            → Crashing (⟨_,_,_⟩ {    n} (app ∷ c) (         val v          ∷ [])       ρ )
    crash₇  : ∀ {n c n′ c′ ρ′ s ρ}   → Crashing (⟨_,_,_⟩ {    n} (app ∷ c) (         ret {n′} c′ ρ′ ∷ s )       ρ )
    crash₈  : ∀ {n c v i s ρ}        → Crashing (⟨_,_,_⟩ {    n} (app ∷ c) (val v  ∷ val (con i)    ∷ s )       ρ )
    crash₉  : ∀ {n c v n′ c′ ρ′ s ρ} → Crashing (⟨_,_,_⟩ {    n} (app ∷ c) (val v  ∷ ret {n′} c′ ρ′ ∷ s )       ρ )
    crash₁₀ : ∀ {n c ρ}              → Crashing (⟨_,_,_⟩ {    n} (ret ∷ c)                            []        ρ )
    crash₁₁ : ∀ {n c v ρ}            → Crashing (⟨_,_,_⟩ {    n} (ret ∷ c) (         val v          ∷ [])       ρ )
    crash₁₂ : ∀ {n c n′ c′ ρ′ s ρ}   → Crashing (⟨_,_,_⟩ {    n} (ret ∷ c) (         ret {n′} c′ ρ′ ∷ s )       ρ )
    crash₁₃ : ∀ {n c v₁ v₂ s ρ}      → Crashing (⟨_,_,_⟩ {    n} (ret ∷ c) (val v₁ ∷ val v₂         ∷ s )       ρ )

  -- There are three kinds of states.

  data Kind (s : State) : Set where
    done     : ∀ {v} (s⇓v : s ⇓ v)    → Kind s
    continue : ∀ {s′} (s⟶s′ : s ⟶ s′) → Kind s
    crash    : (s↯ : Crashing s)      → Kind s

  -- We can assign (at least) one kind to every state.

  kind : ∀ s → Kind s
  kind ⟨ []         ,                 val v ∷ [] , [] ⟩ = done final
  kind ⟨ var x  ∷ c ,                          s , ρ  ⟩ = continue var
  kind ⟨ con i  ∷ c ,                          s , ρ  ⟩ = continue con
  kind ⟨ clo c′ ∷ c ,                          s , ρ  ⟩ = continue clo
  kind ⟨ app    ∷ c , val v ∷ val (ƛ c′ ρ′) ∷  s , ρ  ⟩ = continue app
  kind ⟨ ret    ∷ c , val v ∷ ret c′ ρ′     ∷  s , ρ  ⟩ = continue ret

  kind ⟨ []      ,                       [] , _     ⟩ = crash crash₁
  kind ⟨ []      ,         ret _ _     ∷ _  , _     ⟩ = crash crash₂
  kind ⟨ []      , val _ ∷ _           ∷ _  , _     ⟩ = crash crash₃
  kind ⟨ []      ,         val _       ∷ [] , _ ∷ _ ⟩ = crash crash₄
  kind ⟨ app ∷ _ ,                       [] , _     ⟩ = crash crash₅
  kind ⟨ app ∷ _ ,         val _       ∷ [] , _     ⟩ = crash crash₆
  kind ⟨ app ∷ _ ,         ret _ _     ∷ _  , _     ⟩ = crash crash₇
  kind ⟨ app ∷ _ , val _ ∷ val (con _) ∷ _  , _     ⟩ = crash crash₈
  kind ⟨ app ∷ _ , val _ ∷ ret _ _     ∷ _  , _     ⟩ = crash crash₉
  kind ⟨ ret ∷ _ ,                       [] , _     ⟩ = crash crash₁₀
  kind ⟨ ret ∷ _ ,         val _       ∷ [] , _     ⟩ = crash crash₁₁
  kind ⟨ ret ∷ _ ,         ret _ _     ∷ _  , _     ⟩ = crash crash₁₂
  kind ⟨ ret ∷ _ , val _ ∷ val _       ∷ _  , _     ⟩ = crash crash₁₃

  -- The functional semantics crashes for crashing states.

  exec-crashes : ∀ {s} → Crashing s → exec s ≈ return nothing
  exec-crashes crash₁  = now PE.refl
  exec-crashes crash₂  = now PE.refl
  exec-crashes crash₃  = now PE.refl
  exec-crashes crash₄  = now PE.refl
  exec-crashes crash₅  = now PE.refl
  exec-crashes crash₆  = now PE.refl
  exec-crashes crash₇  = now PE.refl
  exec-crashes crash₈  = now PE.refl
  exec-crashes crash₉  = now PE.refl
  exec-crashes crash₁₀ = now PE.refl
  exec-crashes crash₁₁ = now PE.refl
  exec-crashes crash₁₂ = now PE.refl
  exec-crashes crash₁₃ = now PE.refl

  -- The relational semantics also crashes for crashing states.

  ⟶-crashes : ∀ {s} → Crashing s → Stuck s
  ⟶-crashes s↯ = (helper₁ s↯ , helper₂ s↯)
    where
    helper₁ : ∀ {s} → Crashing s → Final s
    helper₁ crash₁  (_ , ())
    helper₁ crash₂  (_ , ())
    helper₁ crash₃  (_ , ())
    helper₁ crash₄  (_ , ())
    helper₁ crash₅  (_ , ())
    helper₁ crash₆  (_ , ())
    helper₁ crash₇  (_ , ())
    helper₁ crash₈  (_ , ())
    helper₁ crash₉  (_ , ())
    helper₁ crash₁₀ (_ , ())
    helper₁ crash₁₁ (_ , ())
    helper₁ crash₁₂ (_ , ())
    helper₁ crash₁₃ (_ , ())

    helper₂ : ∀ {s} → Crashing s → ∄ λ v → s ⇓ v
    helper₂ crash₁  (_ , ())
    helper₂ crash₂  (_ , ())
    helper₂ crash₃  (_ , ())
    helper₂ crash₄  (_ , ())
    helper₂ crash₅  (_ , ())
    helper₂ crash₆  (_ , ())
    helper₂ crash₇  (_ , ())
    helper₂ crash₈  (_ , ())
    helper₂ crash₉  (_ , ())
    helper₂ crash₁₀ (_ , ())
    helper₂ crash₁₁ (_ , ())
    helper₂ crash₁₂ (_ , ())
    helper₂ crash₁₃ (_ , ())

  ----------------------------------------------------------------------
  -- The relational semantics is sound with respect to the functional
  -- one

  -- Note that these proofs implicitly establish that the relational
  -- semantics is deterministic.

  ⇒⇓ : ∀ {s s′ v} → s ⟶⋆ s′ → s′ ⇓ v → exec s ≈ return (just v)
  ⇒⇓ ε           final = now PE.refl
  ⇒⇓ (var ◅ s⟶⋆) ⇓     = laterˡ (⇒⇓ s⟶⋆ ⇓)
  ⇒⇓ (con ◅ s⟶⋆) ⇓     = laterˡ (⇒⇓ s⟶⋆ ⇓)
  ⇒⇓ (clo ◅ s⟶⋆) ⇓     = laterˡ (⇒⇓ s⟶⋆ ⇓)
  ⇒⇓ (app ◅ s⟶⋆) ⇓     = laterˡ (⇒⇓ s⟶⋆ ⇓)
  ⇒⇓ (ret ◅ s⟶⋆) ⇓     = laterˡ (⇒⇓ s⟶⋆ ⇓)

  ⇒⇑ : ∀ {s} → s ⟶∞ → exec s ≈ never
  ⇒⇑ (var ◅ s⟶∞) = later (♯ (⇒⇑ (♭ s⟶∞)))
  ⇒⇑ (con ◅ s⟶∞) = later (♯ (⇒⇑ (♭ s⟶∞)))
  ⇒⇑ (clo ◅ s⟶∞) = later (♯ (⇒⇑ (♭ s⟶∞)))
  ⇒⇑ (app ◅ s⟶∞) = later (♯ (⇒⇑ (♭ s⟶∞)))
  ⇒⇑ (ret ◅ s⟶∞) = later (♯ (⇒⇑ (♭ s⟶∞)))

  ⇒↯ : ∀ {s} → ∃ (λ s′ → s ⟶⋆ s′ × Stuck s′) → exec s ≈ return nothing
  ⇒↯ (_ , var ◅ s⟶⋆ , ↯) = laterˡ (⇒↯ (_ , s⟶⋆ , ↯))
  ⇒↯ (_ , con ◅ s⟶⋆ , ↯) = laterˡ (⇒↯ (_ , s⟶⋆ , ↯))
  ⇒↯ (_ , clo ◅ s⟶⋆ , ↯) = laterˡ (⇒↯ (_ , s⟶⋆ , ↯))
  ⇒↯ (_ , app ◅ s⟶⋆ , ↯) = laterˡ (⇒↯ (_ , s⟶⋆ , ↯))
  ⇒↯ (_ , ret ◅ s⟶⋆ , ↯) = laterˡ (⇒↯ (_ , s⟶⋆ , ↯))
  ⇒↯ (s , ε          , ↯) with kind s
  ... | done s⇓v       = ⊥-elim (proj₂ ↯ (-, s⇓v))
  ... | continue s₁⟶s₂ = ⊥-elim (proj₁ ↯ (-, s₁⟶s₂))
  ... | crash s↯       = exec-crashes s↯

  ----------------------------------------------------------------------
  -- The relational semantics is complete with respect to the
  -- functional one

  ⇐⇓ : ∀ {s v} → exec s ≈ return (just v) → ∃ λ s′ → s ⟶⋆ s′ × s′ ⇓ v
  ⇐⇓ {s = s} ⇓ with kind s
  ⇐⇓ (now PE.refl) | done final   = (_ , ε , final)
  ⇐⇓ (laterˡ ⇓)    | continue var = Prod.map id (Prod.map (_◅_ var) id) (⇐⇓ ⇓)
  ⇐⇓ (laterˡ ⇓)    | continue con = Prod.map id (Prod.map (_◅_ con) id) (⇐⇓ ⇓)
  ⇐⇓ (laterˡ ⇓)    | continue clo = Prod.map id (Prod.map (_◅_ clo) id) (⇐⇓ ⇓)
  ⇐⇓ (laterˡ ⇓)    | continue app = Prod.map id (Prod.map (_◅_ app) id) (⇐⇓ ⇓)
  ⇐⇓ (laterˡ ⇓)    | continue ret = Prod.map id (Prod.map (_◅_ ret) id) (⇐⇓ ⇓)
  ⇐⇓ {s} {v} ⇓     | crash s↯      with
    return (just v)  ≈⟨ sym ⇓ ⟩
    exec s           ≈⟨ exec-crashes s↯ ⟩
    return nothing   ∎
    where open EqReasoning
  ... | now ()

  ⇐⇑ : ∀ {s} → exec s ≈ never → s ⟶∞
  ⇐⇑ {s = s} ⇑ with kind s
  ⇐⇑         ⇑ | done final   = ⊥-elim (now≉never ⇑)
  ⇐⇑         ⇑ | continue var = var ◅ ♯ ⇐⇑ (later⁻¹ ⇑)
  ⇐⇑         ⇑ | continue con = con ◅ ♯ ⇐⇑ (later⁻¹ ⇑)
  ⇐⇑         ⇑ | continue clo = clo ◅ ♯ ⇐⇑ (later⁻¹ ⇑)
  ⇐⇑         ⇑ | continue app = app ◅ ♯ ⇐⇑ (later⁻¹ ⇑)
  ⇐⇑         ⇑ | continue ret = ret ◅ ♯ ⇐⇑ (later⁻¹ ⇑)
  ⇐⇑ {s}     ⇑ | crash s↯     = ⊥-elim (now≉never (
    return nothing  ≈⟨ sym $ exec-crashes s↯ ⟩
    exec s          ≈⟨ ⇑ ⟩
    never           ∎))
    where open EqReasoning

  ⇐↯ : ∀ {s} → exec s ≈ return nothing → ∃ λ s′ → s ⟶⋆ s′ × Stuck s′
  ⇐↯ {s = s} ↯ with kind s
  ⇐↯ (now ())   | done final
  ⇐↯ (laterˡ ↯) | continue var = Prod.map id (Prod.map (_◅_ var) id) $ ⇐↯ ↯
  ⇐↯ (laterˡ ↯) | continue con = Prod.map id (Prod.map (_◅_ con) id) $ ⇐↯ ↯
  ⇐↯ (laterˡ ↯) | continue clo = Prod.map id (Prod.map (_◅_ clo) id) $ ⇐↯ ↯
  ⇐↯ (laterˡ ↯) | continue app = Prod.map id (Prod.map (_◅_ app) id) $ ⇐↯ ↯
  ⇐↯ (laterˡ ↯) | continue ret = Prod.map id (Prod.map (_◅_ ret) id) $ ⇐↯ ↯
  ⇐↯         ↯  | crash s↯     = (_ , ε , ⟶-crashes s↯)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --without-K --safe #-}
module FreshUtil where

open import Level using (Level; _⊔_; Lift)
open import Data.Empty
open import Data.Product using (∃; _,_; -,_)
open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Unary  as U
open import Relation.Binary as B using (Rel)

open import Data.List.Fresh.Relation.Unary.Any
open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
open import Relation.Binary.PropositionalEquality hiding ( [_] )

private
  variable
    ax px rx ay py ry az pz rz : Level
    AX : Set ax
    AY : Set ay
    AZ : Set az

module _ {AX : Set ax} {RX : Rel AX rx} (PX : Pred AX px) {AY : Set ay} {RY : Rel AY ry} (PY : Pred AY py) {AZ : Set az} {RZ : Rel AZ rz} (PZ : Pred AZ pz) where

        -------------
        FLinsert : AZ → List# AZ RZ  → List# AZ RZ
        FLfresh :  (a x : AZ ) → (y :  List# AZ RZ ) → RZ a x
             -- → # AZ ? a y → fresh AZ ? a (FLinsert x y)
        FLinsert = {!!}
        FLfresh = {!!}

        x∈FLins : (x : AZ)    → (xs : List# AZ RZ)  → Any (x ≡_) (FLinsert x xs)
        x∈FLins = {!!}
        insAny :  {x h : AZ } → (xs : List# AZ RZ)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
        insAny = {!!}

--        FLinsert {zero} f0 y = f0 ∷# []
--        FLinsert {suc n} x [] = x ∷# []
--        FLinsert {suc n} x (cons a y x₁) with FLcmp x a
--        ... | tri≈ ¬a b ¬c  = cons a y x₁
--        ... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁)
--        FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
--        FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
--
--        FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
--        FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
--        ... | tri< x<b ¬b ¬c  = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
--        ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
--        ... | tri> ¬a ¬b b<x =  Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
--        FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
--        ... | tri< x<b ¬b ¬c =  Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
--        ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
--        FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
--            Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
--        FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
--            Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y

        -- all cobmbination in P and Q (could be more general)
        record AnyPair (X :  List# AX RX ) (Y :  List# AY RY ) (fpq : (p : AX) (q : AY) → AZ) : Set
                         (ax  ⊔ px  ⊔ rx  ⊔ ay  ⊔ py  ⊔ ry  ⊔ az  ⊔ pz  ⊔ rz ) where
           field
             pairList :   List# AZ RZ
             pairAny : (p : AX) (q : AY)
                 → Any ( p ≡_ ) X →  Any ( q ≡_ ) Y
                 → Any (fpq p q ≡_) pairList

        -------------
        --    (p,q)   (p,qn) ....           (p,q0)
        --    pn,q
        --     :        AnyPair FL0 FL0 P  Q
        --    p0,q

        open AnyPair
        anyPair : (P : List# AX RX) (Q : List# AY RY) → (fpq : (p : AX) (q : AY) → AZ)  → AnyPair P Q fpq
        anyPair [] [] _ = record { pairList = [] ; pairAny = λ _ _ () }
        anyPair [] (cons q Q qr) _ = record { pairList = [] ; pairAny = λ _ _ () }
        anyPair (cons p P pr) [] _ = record { pairList = [] ; pairAny = λ _ _ _ () }
        anyPair (cons p P pr) (cons q Q qr) fpq = record { pairList = FLinsert (fpq p q) (pairListQ Q)  ; pairAny = anyc0n } where
          pairListP : (P1 : List# AX RX) → List# AZ RZ
          pairListP [] = pairList (anyPair P Q fpq)
          pairListP (cons p₁ P1 x) =  FLinsert (fpq p₁ q) (pairListP P1)
          pairListQ : (Q1 : List# AY RY) → List# AZ RZ
          pairListQ [] = pairListP P
          pairListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (pairListQ Q1)
          anyc0n : (p₁ : AX) (q₁ : AY) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr)
            → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (pairListQ Q))
          anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (pairListQ Q )
          anyc0n p₁ q₁ (here refl) (there anyq) = insAny (pairListQ Q) (anyc01 Q anyq) where
             anyc01 : (Q1 : List# AY RY) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (pairListQ Q1)
             anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _
             anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any)
          anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where
             anyc03 : (P1 : List# AX RX) → Any (_≡_ p₁) P1  → Any (_≡_ (fpq p₁ q₁)) (pairListP P1)
             anyc03 (cons a P1 x) (here refl) = x∈FLins _ _
             anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any)
             anyc02 : (Q1 : List# AY RY) → Any (_≡_ (fpq p₁ q₁)) (pairListQ Q1)
             anyc02 [] = anyc03 P anyp
             anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1)
          anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (pairListQ Q) (anyc04 Q) where
             anyc05 : (P1 : List# AX RX) → Any (_≡_ (fpq p₁ q₁)) (pairListP P1)
             anyc05 [] = pairAny (anyPair P Q fpq) p₁ q₁ anyp anyq
             anyc05 (cons a P1 x) = insAny _ (anyc05 P1)
             anyc04 : (Q1 : List# AY RY) → Any (_≡_ (fpq p₁ q₁)) (pairListQ Q1)
             anyc04 [] = anyc05 P
             anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois