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

module canonical-value-forms where
  canonical-value-forms-num : ∀{Δ d} →
                              Δ , ∅ ⊢ d :: num →
                              d val →
                              Σ[ n ∈ Nat ] (d == N n)
  canonical-value-forms-num TANum VNum = _ , refl
  canonical-value-forms-num (TAVar x₁) ()
  canonical-value-forms-num (TAAp wt wt₁) ()
  canonical-value-forms-num (TAEHole x x₁) ()
  canonical-value-forms-num (TANEHole x wt x₁) ()
  canonical-value-forms-num (TACast wt x) ()
  canonical-value-forms-num (TAFailedCast wt x x₁ x₂) ()

  canonical-value-forms-arr : ∀{Δ d τ1 τ2} →
                              Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                              d val →
                              Σ[ x ∈ Nat ] Σ[ d' ∈ ihexp ]
                                ((d == (·λ x ·[ τ1 ] d')) ×
                                 (Δ , ■ (x , τ1) ⊢ d' :: τ2))
  canonical-value-forms-arr (TAVar x₁) ()
  canonical-value-forms-arr {Δ = Δ} {d = ·λ x ·[ τ1 ] d} {τ1 = τ1} {τ2 = τ2} (TALam _ wt) VLam
    = _ , _ , refl , tr (λ Γ → Δ , Γ ⊢ d :: τ2) (extend-empty x τ1) wt
  canonical-value-forms-arr (TAAp wt wt₁) ()
  canonical-value-forms-arr (TAEHole x x₁) ()
  canonical-value-forms-arr (TANEHole x wt x₁) ()
  canonical-value-forms-arr (TACast wt x) ()
  canonical-value-forms-arr (TAFailedCast x x₁ x₂ x₃) ()

  canonical-value-form-sum : ∀{Δ d τ1 τ2} →
                              Δ , ∅ ⊢ d :: (τ1 ⊕ τ2) →
                              d val →
                              (Σ[ d' ∈ ihexp ] ((d == (inl τ2 d')) × (Δ , ∅ ⊢ d' :: τ1))) +
                              (Σ[ d' ∈ ihexp ] ((d == (inr τ1 d')) × (Δ , ∅ ⊢ d' :: τ2)))
  canonical-value-form-sum (TAInl wt) (VInl v) = Inl (_ , refl , wt)
  canonical-value-form-sum (TAInr wt) (VInr v) = Inr (_ , refl , wt)

  canonical-value-form-prod : ∀{Δ d τ1 τ2} →
                              Δ , ∅ ⊢ d :: (τ1 ⊠ τ2) →
                              d val →
                              Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ]
                                ((d == ⟨ d1 , d2 ⟩) ×
                                 (Δ , ∅ ⊢ d1 :: τ1) ×
                                 (Δ , ∅ ⊢ d2 :: τ2))
  canonical-value-form-prod (TAVar x) ()
  canonical-value-form-prod (TAAp wt wt₁) ()
  canonical-value-form-prod (TACase wt x wt₁ x₁ wt₂) ()
  canonical-value-form-prod (TAPair wt wt₁) (VPair v v₁) = _ , _ , refl , wt , wt₁
  canonical-value-form-prod (TAFst wt) ()
  canonical-value-form-prod (TASnd wt) ()
  canonical-value-form-prod (TAEHole x x₁) ()
  canonical-value-form-prod (TANEHole x wt x₁) ()
  canonical-value-form-prod (TACast wt x) ()
  canonical-value-form-prod (TAFailedCast wt x x₁ x₂) ()

  -- this argues (somewhat informally, because you still have to inspect
  -- the types of the theorems above and manually verify this property)
  -- that we didn't miss any cases above; this intentionally will make this
  -- file fail to typecheck if we added more types, hopefully forcing us to
  -- remember to add canonical forms lemmas as appropriate
  canonical-value-forms-coverage1 : ∀{Δ d τ} →
                                   Δ , ∅ ⊢ d :: τ →
                                   d val →
                                   τ ≠ num →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊕ τ2)) →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊠ τ2)) →
                                   ⊥
  canonical-value-forms-coverage1 TANum val nn na ns np = nn refl
  canonical-value-forms-coverage1 (TALam x wt) val nn na ns np = na _ _ refl
  canonical-value-forms-coverage1 (TAInl wt) val nn na ns np = ns _ _ refl
  canonical-value-forms-coverage1 (TAInr wt) val nn na ns np = ns _ _ refl
  canonical-value-forms-coverage1 (TAPair wt wt₁) val nn na ns np = np _ _ refl

  canonical-value-forms-coverage2 : ∀{Δ d} →
                                   Δ , ∅ ⊢ d :: ⦇-⦈ →
                                   d val →
                                   ⊥
  canonical-value-forms-coverage2 (TAVar x₁) ()
  canonical-value-forms-coverage2 (TAAp wt wt₁) ()
  canonical-value-forms-coverage2 (TAEHole x x₁) ()
  canonical-value-forms-coverage2 (TANEHole x wt x₁) ()
  canonical-value-forms-coverage2 (TACast wt x) ()
  canonical-value-forms-coverage2 (TAFailedCast wt x x₁ x₂) ()

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Meta.Isomorphism where

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

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Structures.Constant

open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓ≅B' ℓC ℓ≅C ℓ≅ᴰ ℓ≅ᴰ' : Level

open URGStr
open URGStrᴰ

----------------------------------------------
-- Pseudo-isomorphisms between URG structures
-- are relational isos of the underlying rel.
----------------------------------------------
𝒮-PIso : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
         {A' : Type ℓA'} (𝒮-A' : URGStr A' ℓ≅A')
         → Type (ℓ-max (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A'))
𝒮-PIso 𝒮-A 𝒮-A' = RelIso (URGStr._≅_ 𝒮-A) (URGStr._≅_ 𝒮-A')

----------------------------------------------
-- Since the relations are univalent,
-- a rel. iso induces an iso of the underlying
-- types.
----------------------------------------------
𝒮-PIso→Iso : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
             {A' : Type ℓA'} (𝒮-A' : URGStr A' ℓ≅A')
             (ℱ : 𝒮-PIso 𝒮-A 𝒮-A')
             → Iso A A'
𝒮-PIso→Iso 𝒮-A 𝒮-A' ℱ
  = RelIso→Iso (_≅_ 𝒮-A) (_≅_ 𝒮-A') (uni 𝒮-A) (uni 𝒮-A') ℱ

----------------------------------------------
-- From a DURG structure, extract the
-- relational family over the base type
----------------------------------------------
𝒮ᴰ→relFamily : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
               {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
               → RelFamily A ℓB ℓ≅B
-- define the type family, just B
𝒮ᴰ→relFamily {B = B} 𝒮ᴰ-B .fst = B
-- the binary relation is the displayed relation over ρ a
𝒮ᴰ→relFamily {𝒮-A = 𝒮-A} {B = B} 𝒮ᴰ-B .snd {a = a} b b'
  = 𝒮ᴰ-B ._≅ᴰ⟨_⟩_ b (𝒮-A .ρ a) b'

--------------------------------------------------------------
-- the type of relational isos between a DURG structure
-- and the pulled back relational family of another
--
-- ℱ will in applications always be an isomorphism,
-- but that's not needed for this definition.
--------------------------------------------------------------
𝒮ᴰ-♭PIso : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
           {A' : Type ℓA'} {𝒮-A' : URGStr A' ℓ≅A'}
           (ℱ : A → A')
           {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
           {B' : A' → Type ℓB'} (𝒮ᴰ-B' : URGStrᴰ 𝒮-A' B' ℓ≅B')
           → Type (ℓ-max ℓA (ℓ-max (ℓ-max ℓB ℓB') (ℓ-max ℓ≅B ℓ≅B')))
𝒮ᴰ-♭PIso ℱ 𝒮ᴰ-B 𝒮ᴰ-B'
  = ♭RelFiberIsoOver ℱ (𝒮ᴰ→relFamily 𝒮ᴰ-B) (𝒮ᴰ→relFamily 𝒮ᴰ-B')

---------------------------------------------------------
-- Given
-- - an isomorphism ℱ of underlying types A, A', and
-- - an 𝒮ᴰ-bPIso over ℱ
-- produce an iso of the underlying total spaces
---------------------------------------------------------
𝒮ᴰ-♭PIso-Over→TotalIso : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
                         {A' : Type ℓA'} {𝒮-A' : URGStr A' ℓ≅A'}
                         (ℱ : Iso A A')
                         {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                         {B' : A' → Type ℓB'} (𝒮ᴰ-B' : URGStrᴰ 𝒮-A' B' ℓ≅B')
                         (𝒢 : 𝒮ᴰ-♭PIso (Iso.fun ℱ) 𝒮ᴰ-B 𝒮ᴰ-B')
                         → Iso (Σ A B) (Σ A' B')
𝒮ᴰ-♭PIso-Over→TotalIso ℱ 𝒮ᴰ-B 𝒮ᴰ-B' 𝒢
  = RelFiberIsoOver→Iso ℱ
                        (𝒮ᴰ→relFamily 𝒮ᴰ-B) (𝒮ᴰ-B .uniᴰ)
                        (𝒮ᴰ→relFamily 𝒮ᴰ-B') (𝒮ᴰ-B' .uniᴰ)
                        𝒢

ext: agda

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Structure.Function.Multi where

open import Data
open import Data.Boolean
open import Data.Tuple.Raise
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Data.Tuple.RaiseTypeᵣ
import      Data.Tuple.RaiseTypeᵣ.Functions as RaiseType
open import Function.DomainRaise as DomainRaise using (_→̂_)
import      Function.Equals.Multi as Multi
open import Function.Multi
import      Function.Multi.Functions as Multi
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Structure.Setoid.Uniqueness
open import Structure.Setoid
open import Syntax.Number
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₗ : Lvl.Level
private variable n : ℕ

module Names where
  module _ {X : Type{ℓ₁}} {Y : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(Y) ⦄ where
    -- Definition of the relation between a function and an operation that says:
    -- The function preserves the operation.
    -- Often used when defining homomorphisms.
    -- Examples:
    --   Preserving(1) (f)(g₁)(g₂)
    --   = (∀{x} → (f ∘₁ g₁)(x) ≡ (g₂ on₁ f)(x))
    --   = (∀{x} → (f(g₁(x)) ≡ g₂(f(x)))
    --   Preserving(2) (f)(g₁)(g₂)
    --   = (∀{x y} → (f ∘₂ g₁)(x)(y) ≡ (g₂ on₂ f)(x)(y))
    --   = (∀{x y} → (f(g₁ x y) ≡ g₂ (f(x)) (f(y)))
    --   Preserving(3) (f)(g₁)(g₂)
    --   = (∀{x y z} → (f ∘₃ g₁)(x)(y)(z) ≡ (g₂ on₃ f)(x)(y)(z))
    --   = (∀{x y z} → (f(g₁ x y z) ≡ g₂ (f(x)) (f(y)) (f(z))))
    -- Alternative implementation:
    --   Preserving(n) (f)(g₁)(g₂) = Multi.Names.⊜₊(n) ([→̂]-to-[⇉] n (f DomainRaise.∘ g₁)) ([→̂]-to-[⇉] n (g₂ DomainRaise.on f))
    Preserving : (n : ℕ) → (f : X → Y) → (X →̂ X)(n) → (Y →̂ Y)(n) → Stmt{if positive?(n) then (ℓ₁ Lvl.⊔ ℓₑ₂) else ℓₑ₂}
    Preserving(𝟎)       (f)(g₁)(g₂) = (f(g₁) ≡ g₂)
    Preserving(𝐒(𝟎))    (f)(g₁)(g₂) = (∀{x} → f(g₁(x)) ≡ g₂(f(x)))
    Preserving(𝐒(𝐒(n))) (f)(g₁)(g₂) = (∀{x} → Preserving(𝐒(n)) (f) (g₁(x)) (g₂(f(x))))

    Preserving₀ = Preserving(0)
    Preserving₁ = Preserving(1)
    Preserving₂ = Preserving(2)
    Preserving₃ = Preserving(3)
    Preserving₄ = Preserving(4)
    Preserving₅ = Preserving(5)
    Preserving₆ = Preserving(6)
    Preserving₇ = Preserving(7)
    Preserving₈ = Preserving(8)
    Preserving₉ = Preserving(9)

  module _ where
    RelationReplacement : ∀{B : Type{ℓ}} → (B → B → Type{ℓₑ}) → (n : ℕ) → ∀{ℓ𝓈 ℓ𝓈ₑ}{As : Types{n}(ℓ𝓈)} → (RaiseType.mapWithLvls(\A ℓₑ → Equiv{ℓₑ}(A)) As ℓ𝓈ₑ) ⇉ᵢₙₛₜ ((As ⇉ B) → (As ⇉ B) → Stmt{Lvl.⨆(ℓ𝓈) Lvl.⊔ ℓₑ Lvl.⊔ Lvl.⨆(ℓ𝓈ₑ)})
    RelationReplacement(_▫_) 0         f g = f ▫ g
    RelationReplacement(_▫_) 1         f g = ∀{x y} → (x ≡ y) → (f(x) ▫ g(y))
    RelationReplacement(_▫_) (𝐒(𝐒(n)))     = Multi.expl-to-inst(𝐒(n)) (Multi.compose(𝐒(n)) (\R f g → ∀{x y} → (x ≡ y) → R (f(x)) (g(y))) (Multi.inst-to-expl(𝐒(n)) (RelationReplacement(_▫_) (𝐒(n)))))

    FunctionReplacement : (n : ℕ) → ∀{ℓ𝓈 ℓ𝓈ₑ}{As : Types{n}(ℓ𝓈)}{B : Type{ℓ}} → (RaiseType.mapWithLvls(\A ℓₑ → Equiv{ℓₑ}(A)) As ℓ𝓈ₑ) ⇉ᵢₙₛₜ (⦃ equiv-B : Equiv{ℓₑ}(B) ⦄ → (As ⇉ B) → (As ⇉ B) → Stmt{Lvl.⨆(ℓ𝓈) Lvl.⊔ ℓₑ Lvl.⊔ Lvl.⨆(ℓ𝓈ₑ)})
    FunctionReplacement 0         f g = f ≡ g
    FunctionReplacement 1         f g = ∀{x y} → (x ≡ y) → (f(x) ≡ g(y))
    FunctionReplacement (𝐒(𝐒(n)))     = Multi.expl-to-inst(𝐒(n)) (Multi.compose(𝐒(n)) (\R ⦃ equiv-B ⦄ f g → ∀{x y} → (x ≡ y) → R ⦃ equiv-B ⦄ (f(x)) (g(y))) (Multi.inst-to-expl(𝐒(n)) (FunctionReplacement (𝐒(n)))))

    -- Generalization of `Structure.Function.Function` for nested function types (or normally known as: functions of any number of arguments (n-ary functions)).
    -- Examples:
    --   Function(0) f g = f ≡ g
    --   Function(1) f g = ∀{x y} → (x ≡ y) → (f(x) ≡ g(y))
    --   Function(2) f g = ∀{x y} → (x ≡ y) → ∀{x₁ y₁} → (x₁ ≡ y₁) → (f(x)(x₁) ≡ g(y)(y₁))
    --   Function(3) f g = ∀{x y} → (x ≡ y) → ∀{x₁ y₁} → (x₁ ≡ y₁) → ∀{x₂ y₂} → (x₂ ≡ y₂) → (f(x)(x₁)(x₂) ≡ g(y)(y₁)(y₂))
    Function : (n : ℕ) → ∀{ℓ𝓈 ℓ𝓈ₑ}{As : Types{n}(ℓ𝓈)}{B : Type{ℓ}} → (RaiseType.mapWithLvls(\A ℓₑ → Equiv{ℓₑ}(A)) As ℓ𝓈ₑ) ⇉ᵢₙₛₜ (⦃ equiv-B : Equiv{ℓₑ}(B) ⦄ → (As ⇉ B) → Stmt)
    Function(n) = Multi.expl-to-inst(n) (Multi.compose(n) (\R ⦃ equiv-B ⦄ → R ⦃ equiv-B ⦄ $₂_) (Multi.inst-to-expl(n) (FunctionReplacement(n))))

  module _ where
    CompatibleReplacement : (n : ℕ) → ∀{ℓ𝓈 ℓ𝓈ₗ}{As : Types{n}(ℓ𝓈)}{B : Type{ℓ}} → (RaiseType.mapWithLvls(\A ℓₗ → A → A → Type{ℓₗ}) As ℓ𝓈ₗ) ⇉ ((B → B → Stmt{ℓₗ}) → (As ⇉ B) → (As ⇉ B) → Stmt{ℓₗ Lvl.⊔ Lvl.⨆(ℓ𝓈) Lvl.⊔ Lvl.⨆(ℓ𝓈ₗ)})
    CompatibleReplacement 0               (_▫_) f g = f ▫ g
    CompatibleReplacement 1         (_▫₀_)(_▫_) f g = ∀{x y} → (x ▫₀ y) → (f(x) ▫ g(y))
    CompatibleReplacement (𝐒(𝐒(n))) (_▫₀_)          = Multi.compose(𝐒(n)) (R ↦ _▫_ ↦ f ↦ g ↦ ∀{x y} → (x ▫₀ y) → R(_▫_) (f(x)) (g(y))) (CompatibleReplacement(𝐒(n)))

    Compatible : (n : ℕ) → ∀{ℓ𝓈 ℓ𝓈ₗ}{As : Types{n}(ℓ𝓈)}{B : Type{ℓ}} → (RaiseType.mapWithLvls(\A ℓₗ → A → A → Type{ℓₗ}) As ℓ𝓈ₗ) ⇉ ((B → B → Stmt{ℓₗ}) → (As ⇉ B) → Stmt)
    Compatible(n) = Multi.compose(n) ((_$₂_) ∘_) (CompatibleReplacement(n))

  module _ {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ where
    -- Definition of the relation between a function and an operation that says:
    -- The function preserves the operation.
    -- This is a special case of the (_preserves_)-relation that has the same operator inside and outside.
    -- Special cases:
    --   Additive function (Operator is a conventional _+_)
    --   Multiplicative function (Operator is a conventional _*_)
    -- ∀{x y} → (f(x ▫ y) ≡ f(x) ▫ f(y))
    _preserves_ : (T → T) → (T → T → T) → Stmt
    f preserves (_▫_) = Preserving(2) f (_▫_)(_▫_) --

module _ {X : Type{ℓ₁}} {Y : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(Y) ⦄ where
  module _ (n : ℕ) (f : X → Y) (g₁ : (X →̂ X)(n)) (g₂ : (Y →̂ Y)(n)) where
    record Preserving : Stmt{if positive?(n) then (ℓ₁ Lvl.⊔ ℓₑ₂) else ℓₑ₂} where -- TODO: Is it possible to prove for levels that an if-expression is less if both are less?
      constructor intro
      field proof : Names.Preserving(n) (f)(g₁)(g₂)
    preserving = inst-fn Preserving.proof

  Preserving₀ = Preserving(0)
  Preserving₁ = Preserving(1)
  Preserving₂ = Preserving(2)
  Preserving₃ = Preserving(3)
  Preserving₄ = Preserving(4)
  Preserving₅ = Preserving(5)
  Preserving₆ = Preserving(6)
  Preserving₇ = Preserving(7)
  Preserving₈ = Preserving(8)
  Preserving₉ = Preserving(9)

  preserving₀ = preserving(0)
  preserving₁ = preserving(1)
  preserving₂ = preserving(2)
  preserving₃ = preserving(3)
  preserving₄ = preserving(4)
  preserving₅ = preserving(5)
  preserving₆ = preserving(6)
  preserving₇ = preserving(7)
  preserving₈ = preserving(8)
  preserving₉ = preserving(9)

module _ {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (n : ℕ) (f : T → T) (_▫_ : T → T → T) where
  _preserves_ = Preserving(2) (f)(_▫_)(_▫_)

{-
module _ {T : Type{ℓ}} where
  module _ (n : ℕ) {ℓₗ} (_▫_ : T → T → Stmt{ℓₗ}) (f : RaiseType.repeat n T ⇉ T) where
    record Compatible : Stmt{ℓₗ Lvl.⊔ (if positive?(n) then ℓ else Lvl.𝟎)} where
      constructor intro
      field proof : Names.Compatible(n) (_▫_)(f)
    compatible = inst-fn Compatible.proof

  Compatible₀ = Compatible(0)
  Compatible₁ = Compatible(1)
  Compatible₂ = Compatible(2)
  Compatible₃ = Compatible(3)
  Compatible₄ = Compatible(4)
  Compatible₅ = Compatible(5)
  Compatible₆ = Compatible(6)
  Compatible₇ = Compatible(7)
  Compatible₈ = Compatible(8)
  Compatible₉ = Compatible(9)

  compatible₀ = compatible(0)
  compatible₁ = compatible(1)
  compatible₂ = compatible(2)
  compatible₃ = compatible(3)
  compatible₄ = compatible(4)
  compatible₅ = compatible(5)
  compatible₆ = compatible(6)
  compatible₇ = compatible(7)
  compatible₈ = compatible(8)
  compatible₉ = compatible(9)
-}

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:
------------------------------------------------------------------------
-- If the "Outrageous but Meaningful Coincidences" approach is used to
-- formalise a language, then you can end up with an extensional type
-- theory (with equality reflection)
------------------------------------------------------------------------

module README.DependentlyTyped.Extensional-type-theory where

import Axiom.Extensionality.Propositional as E
open import Data.Empty
open import Data.Product renaming (curry to c)
open import Data.Unit
open import Data.Universe.Indexed
import deBruijn.Context
open import Function hiding (_∋_) renaming (const to k)
import Level
import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- A non-indexed universe

mutual

  data U : Set where
    empty : U
    π     : (a : U) (b : El a → U) → U

  El : U → Set
  El empty   = ⊥
  El (π a b) = (x : El a) → El (b x)

Uni : IndexedUniverse _ _ _
Uni = record { I = ⊤; U = λ _ → U; El = El }

------------------------------------------------------------------------
-- Contexts and variables

-- We get these for free.

open deBruijn.Context Uni public
  renaming (_·_ to _⊙_; ·-cong to ⊙-cong)

-- Some abbreviations.

⟨empty⟩ : ∀ {Γ} → Type Γ
⟨empty⟩ = -, λ _ → empty

⟨π⟩ : ∀ {Γ} (σ : Type Γ) → Type (Γ ▻ σ) → Type Γ
⟨π⟩ σ τ = -, k π ˢ indexed-type σ ˢ c (indexed-type τ)

⟨π̂⟩ : ∀ {Γ} (σ : Type Γ) →
      ((γ : Env Γ) → El (indexed-type σ γ) → U) → Type Γ
⟨π̂⟩ σ τ = -, k π ˢ indexed-type σ ˢ τ

------------------------------------------------------------------------
-- Well-typed terms

mutual

  infixl 9 _·_
  infix  3 _⊢_

  -- Terms.

  data _⊢_ (Γ : Ctxt) : Type Γ → Set where
    var : ∀ {σ} (x : Γ ∋ σ) → Γ ⊢ σ
    ƛ   : ∀ {σ τ} (t : Γ ▻ σ ⊢ τ) → Γ ⊢ ⟨π⟩ σ τ
    _·_ : ∀ {σ τ} (t₁ : Γ ⊢ ⟨π̂⟩ σ τ) (t₂ : Γ ⊢ σ) → Γ ⊢ (-, τ ˢ ⟦ t₂ ⟧)

  -- Semantics of terms.

  ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Value Γ σ
  ⟦ var x   ⟧ γ = lookup x γ
  ⟦ ƛ t     ⟧ γ = λ v → ⟦ t ⟧ (γ , v)
  ⟦ t₁ · t₂ ⟧ γ = (⟦ t₁ ⟧ γ) (⟦ t₂ ⟧ γ)

------------------------------------------------------------------------
-- We can define looping terms (assuming extensionality)

module Looping (ext : E.Extensionality Level.zero Level.zero) where

  -- The casts are examples of the use of equality reflection: the
  -- casts are meta-language constructions, not object-language
  -- constructions.

  cast₁ : ∀ {Γ} →
          Γ ▻ ⟨empty⟩ ⊢ ⟨π⟩ ⟨empty⟩ ⟨empty⟩ → Γ ▻ ⟨empty⟩ ⊢ ⟨empty⟩
  cast₁ t = P.subst (_⊢_ _) (P.cong (_,_ tt) (ext (⊥-elim ∘ proj₂))) t

  cast₂ : ∀ {Γ} →
          Γ ▻ ⟨empty⟩ ⊢ ⟨empty⟩ → Γ ▻ ⟨empty⟩ ⊢ ⟨π⟩ ⟨empty⟩ ⟨empty⟩
  cast₂ t = P.subst (_⊢_ _) (P.cong (_,_ tt) (ext (⊥-elim ∘ proj₂))) t

  ω : ε ▻ ⟨empty⟩ ⊢ ⟨empty⟩
  ω = cast₁ (ƛ (cast₂ (var zero) · var zero))

  -- A simple example of a term which does not have a normal form.

  Ω : ε ▻ ⟨empty⟩ ⊢ ⟨empty⟩
  Ω = cast₂ ω · ω

  const-Ω : ε ⊢ ⟨π⟩ ⟨empty⟩ ⟨empty⟩
  const-Ω = ƛ Ω

-- Some observations:
--
-- * The language with spines (in README.DependentlyTyped.Term) does
--   not support terms like the ones above; in the casts one would
--   have to prove that distinct spines are equal.
--
-- * The spines ensure that the normaliser in
--   README.DependentlyTyped.NBE terminates. The existence of terms
--   like Ω implies that it is impossible to implement a normaliser
--   for the spine-less language defined in this module.

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module Issue888 (A : Set) where
-- Check that let-bound variables show up in "show context"

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

f : Set -> Set
f X = let Y : ℕ -> Set
          Y n = ℕ
          m : ℕ
          m = {!!}
      in {!!}

-- Issue 1112: dependent let-bindings

data Singleton : ℕ → Set where
  mkSingleton : (n : ℕ) -> Singleton n

g : ℕ -> ℕ
g x =
  let i = zero
      z = mkSingleton x
  in {!!}

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An explanation about the `Axiom` modules.
------------------------------------------------------------------------

module README.Axiom where

open import Level using (Level)

private variable ℓ : Level

------------------------------------------------------------------------
-- Introduction

-- Several rules that are used without thought in written mathematics
-- cannot be proved in Agda. The modules in the `Axiom` folder
-- provide types expressing some of these rules that users may want to
-- use even when they're not provable in Agda.

------------------------------------------------------------------------
-- Example: law of excluded middle

-- In classical logic the law of excluded middle states that for any
-- proposition `P` either `P` or `¬P` must hold. This is impossible
-- to prove in Agda because Agda is a constructive system and so any
-- proof of the excluded middle would have to build a term of either
-- type `P` or `¬P`. This is clearly impossible without any knowledge
-- of what proposition `P` is.

-- The types for which `P` or `¬P` holds is called `Dec P` in the
-- standard library (short for `Decidable`).

open import Relation.Nullary using (Dec)

-- The type of the proof of saying that excluded middle holds for
-- all types at universe level ℓ is therefore:
--
--   ExcludedMiddle ℓ = ∀ {P : Set ℓ} → Dec P
--
-- and this type is exactly the one found in `Axiom.ExcludedMiddle`:

open import Axiom.ExcludedMiddle

-- There are two different ways that the axiom can be introduced into
-- your Agda development. The first option is to postulate it:

postulate excludedMiddle : ExcludedMiddle ℓ

-- This has the advantage that it only needs to be postulated once
-- and it can then be imported into many different modules as with any
-- other proof. The downside is that the resulting Agda code will no
-- longer type check under the --safe flag.

-- The second approach is to pass it as a module parameter:

module Proof (excludedMiddle : ExcludedMiddle ℓ) where

-- The advantage of this approach is that the resulting Agda
-- development can still be type checked under the --safe flag.
-- Intuitively the reason for this is that when postulating it
-- you are telling Agda that excluded middle does hold (which is clearly
-- untrue as discussed above). In contrast when passing it as a module
-- parameter you are telling Agda that **if** excluded middle was true
-- then the following proofs would hold, which is logically valid.

-- The disadvantage of this approach is that it is now necessary to
-- include the excluded middle assumption as a parameter in every module
-- that you want to use it in. Additionally the modules can never
-- be fully instantiated (without postulating excluded middle).

------------------------------------------------------------------------
-- Other axioms

-- Double negation elimination
--   (∀ P → ¬ ¬ P → P)

import Axiom.DoubleNegationElimination

-- Function extensionality
--   (∀ f g → (∀ x → f x ≡ g x) → f ≡ g)

import Axiom.Extensionality.Propositional
import Axiom.Extensionality.Heterogeneous

-- Uniqueness of identity proofs (UIP)
--  (∀ x y (p q : x ≡ y) → p ≡ q)

import Axiom.UniquenessOfIdentityProofs


text:
module Human.String where

open import Human.Bool
open import Human.List renaming ( length to llength )
open import Human.Char
open import Human.Nat

postulate String : Set
{-# BUILTIN STRING String #-}

primitive
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool
  primShowChar       : Char → String
  primShowString     : String → String

{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-}
{-# COMPILE JS primStringFromList = function(x) { return x.join(""); } #-}
{-# COMPILE JS primStringAppend = function(x) { return function(y) { return x+y; }; } #-}
{-# COMPILE JS primStringEquality = function(x) { return function(y) { return x===y; }; } #-}
{-# COMPILE JS primShowChar = function(x) { return JSON.stringify(x); } #-}
{-# COMPILE JS primShowString = function(x) { return JSON.stringify(x); } #-}

toList : String → List Char
toList = primStringToList

{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-}

slength : String → Nat
slength s = llength (toList s)

{-# COMPILE JS slength = function(s) { return s.length; } #-}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Group where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.FunExtEquiv
open import Cubical.Data.Prod.Base hiding (_×_) renaming (_×Σ_ to _×_)

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.Monoid

private
  variable
    ℓ ℓ' : Level

group-axiom : (X : Type ℓ) → monoid-structure X → Type ℓ
group-axiom G ((e , _·_) , _) = ((x : G) → Σ G (λ x' → (x · x' ≡ e) × (x' · x ≡ e)))

group-structure : Type ℓ → Type ℓ
group-structure = add-to-structure (monoid-structure) group-axiom

Groups : Type (ℓ-suc ℓ)
Groups {ℓ} = TypeWithStr ℓ group-structure

-- Extracting components of a group

⟨_⟩ : Groups {ℓ} → Type ℓ
⟨ (G , _) ⟩ = G

id : (G : Groups {ℓ}) → ⟨ G ⟩
id (_ , ((e , _) , _) , _) = e

group-operation : (G : Groups {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
group-operation (_ , ((_ , f) , _) , _) = f

infixl 20 group-operation
syntax group-operation G x y = x ·⟨ G ⟩ y

group-is-set : (G : Groups {ℓ}) → isSet ⟨ G ⟩
group-is-set (_ , (_ , (P , _)) , _) = P

group-assoc : (G : Groups {ℓ})
            → (x y z : ⟨ G ⟩) → (x ·⟨ G ⟩ (y ·⟨ G ⟩ z)) ≡ ((x ·⟨ G ⟩ y) ·⟨ G ⟩ z)
group-assoc (_ , (_ , (_ , P , _)) , _) = P

group-runit : (G : Groups {ℓ})
            → (x : ⟨ G ⟩) → x ·⟨ G ⟩ (id G) ≡ x
group-runit (_ , (_ , (_ , _ , P , _)) , _) = P

group-lunit : (G : Groups {ℓ})
            → (x : ⟨ G ⟩) → (id G) ·⟨ G ⟩ x ≡ x
group-lunit (_ , (_ , (_ , _ , _ , P)) , _) = P

group-Σinv : (G : Groups {ℓ})
           → (x : ⟨ G ⟩) → Σ (⟨ G ⟩) (λ x' → (x ·⟨ G ⟩ x' ≡ (id G)) × (x' ·⟨ G ⟩ x ≡ (id G)))
group-Σinv (_ , _ , P) = P

-- Defining the inverse function

inv : (G : Groups {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩
inv (_ , _ , P) x = fst (P x)

group-rinv : (G : Groups {ℓ})
               → (x : ⟨ G ⟩) → x ·⟨ G ⟩ (inv G x) ≡ id G
group-rinv (_ , _ , P) x = fst (snd (P x))

group-linv : (G : Groups {ℓ})
               → (x : ⟨ G ⟩) → (inv G x) ·⟨ G ⟩ x ≡ id G
group-linv (_ , _ , P) x = snd (snd (P x))

-- Iso for groups are those for monoids

group-iso : StrIso group-structure ℓ
group-iso = add-to-iso monoid-structure monoid-iso group-axiom

-- Auxiliary lemmas for subtypes (taken from Escardo)

to-Σ-≡ : {X : Type ℓ} {A : X → Type ℓ'} {σ τ : Σ X A}
       → (Σ (fst σ ≡ fst τ) λ p → PathP (λ i → A (p i)) (snd σ) (snd τ))
       → σ ≡ τ
to-Σ-≡ (eq , p) = λ i → eq i , p i

to-subtype-≡ : {X : Type ℓ} {A : X → Type ℓ'} {x y : X}
               {a : A x} {b : A y}
             → ((x : X) → isProp (A x))
             → x ≡ y
             → Path (Σ X (λ x → A x)) (x , a) (y , b)
to-subtype-≡  {x = x} {y} {a} {b} f eq = to-Σ-≡ (eq , toPathP (f y _ b))
-- TODO: this proof without toPathP?

-- Group axiom isProp

group-axiom-isProp : (X : Type ℓ)
                   → (s : monoid-structure X)
                   → isProp (group-axiom X s)
group-axiom-isProp X (((e , _·_) , s@(isSet , assoc , rid , lid))) = isPropPi γ
  where
    γ : (x : X) → isProp (Σ X (λ x' → (x · x' ≡ e) × (x' · x ≡ e)))
    γ x (y , a , q) (z , p , b) = to-subtype-≡ u t
      where
        t : y ≡ z
        t = inv-lemma X e _·_ s x y z q p

        u : (x' : X) → isProp ((x · x' ≡ e) × (x' · x ≡ e))
        u x' = isPropΣ (isSet _ _)
               (λ _ →   isSet _ _)

-- Group paths equivalent to equality

group-is-SNS : SNS {ℓ} group-structure group-iso
group-is-SNS = add-axioms-SNS monoid-structure monoid-iso
               group-axiom group-axiom-isProp monoid-is-SNS

GroupPath : (M N : Groups {ℓ}) → (M ≃[ group-iso ] N) ≃ (M ≡ N)
GroupPath M N = SIP group-structure group-iso group-is-SNS M N

-- Trying to improve isomorphisms to only have to preserve
-- _·_

group-iso' : StrIso group-structure ℓ
group-iso' G S f =
  (x y : ⟨ G ⟩) → equivFun f (x ·⟨ G ⟩ y) ≡ equivFun f x ·⟨ S ⟩ equivFun f y

-- Trying to reduce isomorphisms to simpler ones
-- First we prove that both notions of group-iso are equal
-- since both are props and there is are functions from
-- one to the other

-- Functions

group-iso→group-iso' : (G S : Groups {ℓ}) (f : ⟨ G ⟩ ≃ ⟨ S ⟩)
                     → group-iso G S f → group-iso' G S f
group-iso→group-iso' G S f γ = snd γ

group-iso'→group-iso : (G S : Groups {ℓ}) (f : ⟨ G ⟩ ≃ ⟨ S ⟩)
                     → group-iso' G S f → group-iso G S f
group-iso'→group-iso G S f γ = η , γ
  where
  g : ⟨ G ⟩ → ⟨ S ⟩
  g = equivFun f

  e : ⟨ G ⟩
  e = id G

  d : ⟨ S ⟩
  d = id S

  δ : g e ≡ g e ·⟨ S ⟩ g e
  δ = g e ≡⟨ cong g (sym (group-lunit G _)) ⟩
      g (e ·⟨ G ⟩ e) ≡⟨ γ e e ⟩
      g e ·⟨ S ⟩ g e ∎

  η : g e ≡ d
  η = g e                                   ≡⟨ sym (group-runit S _) ⟩
      g e ·⟨ S ⟩ d                          ≡⟨ cong (λ - → g e ·⟨ S ⟩ -) (sym (group-rinv S _)) ⟩
      g e ·⟨ S ⟩ (g e ·⟨ S ⟩ (inv S (g e))) ≡⟨ group-assoc S _ _ _ ⟩
     (g e ·⟨ S ⟩ g e) ·⟨ S ⟩ (inv S (g e))  ≡⟨ cong (λ - → group-operation S - (inv S (g e))) (sym δ) ⟩
      g e ·⟨ S ⟩ (inv S (g e))              ≡⟨ group-rinv S _ ⟩
      d ∎

-- Both are Props

isProp-Iso : (G S : Groups {ℓ}) (f : ⟨ G ⟩ ≃ ⟨ S ⟩) → isProp (group-iso G S f)
isProp-Iso G S f = isPropΣ (group-is-set S _ _)
                   (λ _ → isPropPi (λ x → isPropPi λ y → group-is-set S _ _))

isProp-Iso' : (G S : Groups {ℓ}) (f : ⟨ G ⟩ ≃ ⟨ S ⟩) → isProp (group-iso' G S f)
isProp-Iso' G S f = isPropPi (λ x → isPropPi λ y → group-is-set S _ _)

-- Propositional equality

to-Prop-≡ : {X Y : Type ℓ} (f : X → Y) (g : Y → X)
          → isProp X → isProp Y
          → X ≡ Y
to-Prop-≡ {ℓ} {X} {Y} f g p q = isoToPath (iso f g aux₂ aux₁)
  where
  aux₁ : (x : X) → g (f x) ≡ x
  aux₁ x = p _ _

  aux₂ : (y : Y) → f (g y) ≡ y
  aux₂ y = q _ _

-- Finally both are equal

group-iso'≡group-iso : group-iso' {ℓ} ≡ group-iso
group-iso'≡group-iso = funExt₃ γ
  where
    γ : ∀ (G S : Groups {ℓ}) (f : ⟨ G ⟩ ≃ ⟨ S ⟩)
      → group-iso' G S f ≡ group-iso G S f
    γ G S f = to-Prop-≡ (group-iso'→group-iso G S f)
                        (group-iso→group-iso' G S f)
                        (isProp-Iso' G S f)
                        (isProp-Iso  G S f)

-- And Finally we have what we wanted

group-is-SNS' : SNS {ℓ} group-structure group-iso'
group-is-SNS' = transport γ group-is-SNS
  where
  γ : SNS {ℓ} group-structure group-iso ≡ SNS {ℓ} group-structure group-iso'
  γ = cong (SNS group-structure) (sym group-iso'≡group-iso)

GroupPath' : (M N : Groups {ℓ}) → (M ≃[ group-iso' ] N) ≃ (M ≡ N)
GroupPath' M N = SIP group-structure group-iso' group-is-SNS' M N

---------------------------------------------------------------------
-- Abelians group (just add one axiom and prove that it is a hProp)
---------------------------------------------------------------------

abelian-group-axiom : (X : Type ℓ) → group-structure X → Type ℓ
abelian-group-axiom G (((_ , _·_), _), _) = (x y : G) → x · y ≡ y · x

abelian-group-structure : Type ℓ → Type ℓ
abelian-group-structure = add-to-structure (group-structure) abelian-group-axiom

AbGroups : Type (ℓ-suc ℓ)
AbGroups {ℓ} = TypeWithStr ℓ abelian-group-structure

abelian-group-iso : StrIso abelian-group-structure ℓ
abelian-group-iso = add-to-iso group-structure group-iso abelian-group-axiom

abelian-group-axiom-isProp : (X : Type ℓ)
                           → (s : group-structure X)
                           → isProp (abelian-group-axiom X s)
abelian-group-axiom-isProp X ((_ , (group-isSet , _)) , _) =
  isPropPi (λ x → isPropPi λ y → group-isSet _ _)

abelian-group-is-SNS : SNS {ℓ} abelian-group-structure abelian-group-iso
abelian-group-is-SNS = add-axioms-SNS group-structure group-iso
               abelian-group-axiom abelian-group-axiom-isProp group-is-SNS

AbGroupPath : (M N : AbGroups {ℓ}) → (M ≃[ abelian-group-iso ] N) ≃ (M ≡ N)
AbGroupPath M N = SIP abelian-group-structure abelian-group-iso abelian-group-is-SNS M N

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
data D : Set where
  @0 c : D

-- The following definition should be rejected. Matching on an erased
-- constructor in an *erased* position should not on its own make it
-- possible to use erased definitions in the right-hand side.

f : @0 D → D
f c = c

x : D
x = f c

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Abstract.Types
open import LibraBFT.Abstract.Types.EpochConfig
open        WithAbsVote

-- This module contains properties about RecordChains, culminating in
-- theorem S5, which is the main per-epoch correctness condition.  The
-- properties are based on the original version of the LibraBFT paper,
-- which was current when they were developed:
-- https://developers.diem.com/docs/assets/papers/diem-consensus-state-machine-replication-in-the-diem-blockchain/2019-06-28.pdf
-- Even though the implementation has changed since that version of the
-- paper, we do not need to redo these proofs because that affects only
-- the concrete implementation.  This demonstrates one advantage of
-- separating these proofs into abstract and concrete pieces.

module LibraBFT.Abstract.RecordChain.Properties
  (UID    : Set)
  (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
  (NodeId : Set)
  (𝓔      : EpochConfig UID NodeId)
  (𝓥      : VoteEvidence UID NodeId 𝓔)
  where
 open import LibraBFT.Abstract.Types                   UID        NodeId 𝓔
 open import LibraBFT.Abstract.System                  UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.Records                 UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.Records.Extends         UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain             UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain.Assumptions UID _≟UID_ NodeId 𝓔 𝓥
 open        EpochConfig 𝓔

 module WithInvariants {ℓ}
   (InSys                 : Record → Set ℓ)
   (votes-only-once       : VotesOnlyOnceRule InSys)
   (preferred-round-rule  : PreferredRoundRule InSys)
   where
   open All-InSys-props InSys

   ----------------------
   -- Lemma 2

   -- Lemma 2 states that there can be at most one certified block per
   -- round.  If two blocks have a quorum certificate for the same round,
   -- then they are equal or their unique identifier is not
   -- injective. This is required because, on the concrete side, this bId
   -- will be a hash function which might yield collisions.
   lemmaS2 : {b₀ b₁ : Block}{q₀ q₁ : QC}
           → InSys (Q q₀) → InSys (Q q₁)
           → (p₀ : B b₀ ← Q q₀)
           → (p₁ : B b₁ ← Q q₁)
           → getRound b₀ ≡ getRound b₁
           → NonInjective-≡ bId ⊎ b₀ ≡ b₁
   lemmaS2 {b₀} {b₁} {q₀} {q₁} ex₀ ex₁ (B←Q refl h₀) (B←Q refl h₁) refl
     with b₀ ≟Block b₁
   ...| yes done = inj₂ done
   ...| no  imp
     with bft-assumption (qVotes-C1 q₀) (qVotes-C1 q₁)
   ...|  (a , (a∈q₀mem , a∈q₁mem , honest))
     with Any-sym (Any-map⁻ a∈q₀mem) | Any-sym (Any-map⁻ a∈q₁mem)
   ...| a∈q₀ | a∈q₁
      with All-lookup (qVotes-C3 q₀) (∈QC-Vote-correct q₀ a∈q₀) |
      All-lookup (qVotes-C3 q₁) (∈QC-Vote-correct q₁ a∈q₁)
   ...| a∈q₀rnd≡ | a∈q₁rnd≡
     with <-cmp (abs-vRound (∈QC-Vote q₀ a∈q₀)) (abs-vRound (∈QC-Vote q₁ a∈q₁))
   ...| tri< va<va' _ _ = ⊥-elim (<⇒≢ (subst₂ _<_ a∈q₀rnd≡ a∈q₁rnd≡ va<va') refl)
   ...| tri> _ _ va'<va = ⊥-elim (<⇒≢ (subst₂ _≤_ (cong suc a∈q₁rnd≡) a∈q₀rnd≡ va'<va) refl)
   ...| tri≈ _ v₀≡v₁ _ =
     let v₀∈q₀ = ∈QC-Vote-correct q₀ a∈q₀
         v₁∈q₁ = ∈QC-Vote-correct q₁ a∈q₁
         ppp   = trans h₀ (trans (vote≡⇒QPrevId≡ {q₀} {q₁} v₀∈q₀ v₁∈q₁ (votes-only-once a honest ex₀ ex₁ a∈q₀ a∈q₁ v₀≡v₁))
                                 (sym h₁))
     in inj₁ ((b₀ , b₁) , (imp , ppp))

   ----------------
   -- Lemma S3

   lemmaS3 : ∀{r₂ q'}
             {rc : RecordChain r₂}      → InSys r₂
           → (rc' : RecordChain (Q q')) → InSys (Q q')  -- Immediately before a (Q q), we have the certified block (B b), which is the 'B' in S3
           → (c3 : 𝕂-chain Contig 3 rc)                 -- This is B₀ ← C₀ ← B₁ ← C₁ ← B₂ ← C₂ in S3
           → round r₂ < getRound q'
           → NonInjective-≡ bId ⊎ (getRound (kchainBlock (suc (suc zero)) c3) ≤ prevRound rc')
   lemmaS3 {r₂} {q'} ex₀ (step rc' b←q') ex₁ (s-chain {rc = rc} {b = b₂} {q₂} r←b₂ _ b₂←q₂ c2) hyp
     with bft-assumption (qVotes-C1 q₂) (qVotes-C1 q')
   ...| (a , (a∈q₂mem , a∈q'mem , honest))
        with Any-sym (Any-map⁻ a∈q₂mem) | Any-sym (Any-map⁻ a∈q'mem)
   ...| a∈q₂ | a∈q'

     -- TODO-1: We have done similar reasoning on the order of votes for
     -- lemmaS2. We should factor out a predicate that analyzes the rounds
     -- of QC's and returns us a judgement about the order of the votes.
     with All-lookup (qVotes-C3 q') (∈QC-Vote-correct q' a∈q') |
          All-lookup (qVotes-C3 q₂) (∈QC-Vote-correct q₂ a∈q₂)
   ...| a∈q'rnd≡ | a∈q₂rnd≡
     with <-cmp (round r₂) (abs-vRound (∈QC-Vote q' a∈q'))
   ...| tri> _ _ va'<va₂
     with subst₂ _<_ a∈q'rnd≡ a∈q₂rnd≡   (≤-trans va'<va₂ (≤-reflexive (sym a∈q₂rnd≡)))
   ...| res = ⊥-elim (n≮n (getRound q') (≤-trans res (≤-unstep hyp)))
   lemmaS3 {q' = q'} ex₀ (step rc' b←q') ex₁ (s-chain {rc = rc} {b = b₂} {q₂} r←b₂ P b₂←q₂ c2) hyp
      | (a , (a∈q₂mem , a∈q'mem , honest))
      | a∈q₂ | a∈q'
      | a∈q'rnd≡ | a∈q₂rnd≡
      | tri≈ _ v₂≡v' _ =
     let v₂∈q₂ = ∈QC-Vote-correct q₂ a∈q₂
         v'∈q' = ∈QC-Vote-correct q' a∈q'
      in ⊥-elim (<⇒≢ hyp (vote≡⇒QRound≡ {q₂} {q'} v₂∈q₂ v'∈q'
                                        (votes-only-once a honest {q₂} {q'} ex₀ ex₁ a∈q₂ a∈q'
                                                         (trans a∈q₂rnd≡ v₂≡v'))))
   lemmaS3 {r} {q'} ex₀ (step rc' b←q') ex₁  (s-chain {rc = rc} {b = b₂} {q₂} r←b₂ P b₂←q₂ c2) hyp
      | (a , (a∈q₂mem , a∈q'mem , honest))
      | a∈q₂ | a∈q'
      | a∈q'rnd≡ | a∈q₂rnd≡
      | tri< va₂<va' _ _
     with b←q'
   ...| B←Q rrr xxx
      = preferred-round-rule a honest {q₂} {q'} ex₀ ex₁ (s-chain r←b₂ P b₂←q₂ c2) a∈q₂
                    (step rc' (B←Q rrr xxx)) a∈q'
                          (≤-trans (≤-reflexive (cong suc a∈q₂rnd≡))
                                   va₂<va')

  ------------------
  -- Proposition S4

   -- The base case for lemma S4 resorts to a pretty simple
   -- arithmetic statement.
   propS4-base-arith
     : ∀ n r
     → n ≤ r → r ≤ (suc (suc n))
     → r ∈ (suc (suc n) ∷ suc n ∷ n ∷ [])
   propS4-base-arith .0 .0 z≤n z≤n = there (there (here refl))
   propS4-base-arith .0 .1 z≤n (s≤s z≤n) = there (here refl)
   propS4-base-arith .0 .2 z≤n (s≤s (s≤s z≤n)) = here refl
   propS4-base-arith (suc r) (suc n) (s≤s h0) (s≤s h1)
     = ∈-cong suc (propS4-base-arith r n h0 h1)

   -- Which is then translated to LibraBFT lingo
   propS4-base-lemma-1
     : ∀{q}{rc : RecordChain (Q q)}
     → (c3 : 𝕂-chain Contig 3 rc) -- This is B₀ ← C₀ ← B₁ ← C₁ ← B₂ ← C₂ in S4
     → (r : ℕ)
     → getRound (c3 b⟦ suc (suc zero) ⟧) ≤ r
     → r ≤ getRound (c3 b⟦ zero ⟧)
     → r ∈ ( getRound (c3 b⟦ zero ⟧)
           ∷ getRound (c3 b⟦ (suc zero) ⟧)
           ∷ getRound (c3 b⟦ (suc (suc zero)) ⟧)
           ∷ [])
   propS4-base-lemma-1 (s-chain {b = b0} _ p0 (B←Q refl b←q0)
                       (s-chain {b = b1} r←b1 p1 (B←Q refl b←q1)
                       (s-chain {r = R} {b = b2} r←b2 p2 (B←Q refl b←q2)
                          0-chain))) r hyp0 hyp1
     rewrite p0 | p1 = propS4-base-arith (bRound b2) r hyp0 hyp1

   propS4-base-lemma-2
     : ∀{k r}
       {rc : RecordChain r} → All-InSys rc
     → (q' : QC) → InSys (Q q')
     → {b' : Block}
     → (rc' : RecordChain (B b')) → (ext : (B b') ← (Q q'))
     → (c  : 𝕂-chain Contig k rc)
     → (ix : Fin k)
     → getRound (kchainBlock ix c) ≡ getRound b'
     → NonInjective-≡ bId ⊎ (kchainBlock ix c ≡ b')
   propS4-base-lemma-2 {rc = rc} prev∈sys q' q'∈sys rc' ext (s-chain r←b prf b←q c) zero hyp
     = lemmaS2 (All-InSys⇒last-InSys prev∈sys) q'∈sys b←q ext hyp
   propS4-base-lemma-2 prev∈sys q' q'∈sys rc' ext (s-chain r←b prf b←q c) (suc ix)
     = propS4-base-lemma-2 (All-InSys-unstep (All-InSys-unstep prev∈sys)) q' q'∈sys rc' ext c ix

   propS4-base : ∀{q q'}
               → {rc : RecordChain (Q q)}   → All-InSys rc
               → (rc' : RecordChain (Q q')) → InSys (Q q')
               → (c3 : 𝕂-chain Contig 3 rc) -- This is B₀ ← C₀ ← B₁ ← C₁ ← B₂ ← C₂ in S4
               → getRound (c3 b⟦ suc (suc zero) ⟧) ≤ getRound q'
               → getRound q' ≤ getRound (c3 b⟦ zero ⟧)
               → NonInjective-≡ bId ⊎ B (c3 b⟦ suc (suc zero) ⟧) ∈RC rc'
   propS4-base {q' = q'} prev∈sys (step {B b} rc'@(step rc'' q←b) b←q@(B←Q refl _)) q'∈sys c3 hyp0 hyp1
     with propS4-base-lemma-1 c3 (getRound b) hyp0 hyp1
   ...| here r
     with propS4-base-lemma-2 prev∈sys q' q'∈sys rc' b←q c3 zero (sym r)
   ...| inj₁ hb = inj₁ hb
   ...| inj₂ res
     with 𝕂-chain-∈RC c3 zero (suc (suc zero)) z≤n res rc'
   ...| inj₁ hb   = inj₁ hb
   ...| inj₂ res' = inj₂ (there b←q res')
   propS4-base {q} {q'} prev∈sys (step rc' (B←Q refl x₀)) q'∈sys c3 hyp0 hyp1
      | there (here r)
     with propS4-base-lemma-2 prev∈sys q' q'∈sys rc' (B←Q refl x₀) c3 (suc zero) (sym r)
   ...| inj₁ hb = inj₁ hb
   ...| inj₂ res
     with 𝕂-chain-∈RC c3 (suc zero) (suc (suc zero)) (s≤s z≤n) res rc'
   ...| inj₁ hb   = inj₁ hb
   ...| inj₂ res' = inj₂ (there (B←Q refl x₀) res')
   propS4-base {q' = q'} prev∈sys (step rc' (B←Q refl x₀)) q'∈sys c3 hyp0 hyp1
      | there (there (here r))
     with propS4-base-lemma-2 prev∈sys q' q'∈sys rc' (B←Q refl x₀) c3 (suc (suc zero)) (sym r)
   ...| inj₁ hb = inj₁ hb
   ...| inj₂ res
     with 𝕂-chain-∈RC c3 (suc (suc zero)) (suc (suc zero)) (s≤s (s≤s z≤n)) res rc'
   ...| inj₁ hb   = inj₁ hb
   ...| inj₂ res' = inj₂ (there (B←Q refl x₀) res')

   propS4 : ∀{q q'}
          → {rc : RecordChain (Q q)}   → All-InSys rc
          → (rc' : RecordChain (Q q')) → All-InSys rc'
          → (c3 : 𝕂-chain Contig 3 rc) -- This is B₀ ← C₀ ← B₁ ← C₁ ← B₂ ← C₂ in S4
          → getRound (c3 b⟦ suc (suc zero) ⟧) ≤ getRound q'
          -- In the paper, the proposition states that B₀ ←⋆ B, yet, B is the block preceding
          -- C, which in our case is 'prevBlock rc''. Hence, to say that B₀ ←⋆ B is
          -- to say that B₀ is a block in the RecordChain that goes all the way to C.
          → NonInjective-≡ bId ⊎ B (c3 b⟦ suc (suc zero) ⟧) ∈RC rc'
   propS4 {q' = q'} {rc} prev∈sys (step rc' b←q') prev∈sys' c3 hyp
     with getRound q' ≤?ℕ getRound (c3 b⟦ zero ⟧)
   ...| yes rq≤rb₂ = propS4-base {q' = q'} prev∈sys (step rc' b←q') (All-InSys⇒last-InSys prev∈sys') c3 hyp rq≤rb₂
   propS4 {q' = q'} prev∈sys (step rc' b←q') all∈sys c3 hyp
      | no  rb₂<rq
     with lemmaS3 (All-InSys⇒last-InSys prev∈sys) (step rc' b←q')
                  (All-InSys⇒last-InSys all∈sys) c3
                  (subst (_< getRound q') (kchainBlockRoundZero-lemma c3) (≰⇒> rb₂<rq))
   ...| inj₁ hb = inj₁ hb
   ...| inj₂ ls3
     with rc' | b←q'
   ...| step rc'' q←b | (B←Q {b} rx x)
     with rc'' | q←b
   ...| empty | (I←B _ _)
      = contradiction (n≤0⇒n≡0 ls3)
                      (¬bRound≡0 (kchain-to-RecordChain-at-b⟦⟧ c3 (suc (suc zero))))
   ...| step {r = r} rc''' (B←Q {q = q''} refl bid≡) | (Q←B ry y)
     with propS4 {q' = q''} prev∈sys (step rc''' (B←Q refl bid≡)) (All-InSys-unstep (All-InSys-unstep all∈sys)) c3 ls3
   ...| inj₁ hb'   = inj₁ hb'
   ...| inj₂ final = inj₂ (there (B←Q rx x) (there (Q←B ry y) final))

   -------------------
   -- Theorem S5
   thmS5 : ∀{q q'}
         → {rc  : RecordChain (Q q )} → All-InSys rc
         → {rc' : RecordChain (Q q')} → All-InSys rc'
         → {b b' : Block}
         → CommitRule rc  b
         → CommitRule rc' b'
         → NonInjective-≡ bId ⊎ ((B b) ∈RC rc' ⊎ (B b') ∈RC rc) -- Not conflicting means one extends the other.
   thmS5 {rc = rc} prev∈sys {rc'} prev∈sys' (commit-rule c3 refl) (commit-rule c3' refl)
     with <-cmp (getRound (c3 b⟦ suc (suc zero) ⟧)) (getRound (c3' b⟦ suc (suc zero) ⟧))
   ...| tri≈ _ r≡r' _ = inj₁ <⊎$> (propS4 prev∈sys  rc' prev∈sys' c3  (≤-trans (≡⇒≤ r≡r')      (kchain-round-≤-lemma' c3' (suc (suc zero)))))
   ...| tri< r<r' _ _ = inj₁ <⊎$> (propS4 prev∈sys  rc' prev∈sys' c3  (≤-trans (≤-unstep r<r') (kchain-round-≤-lemma' c3' (suc (suc zero)))))
   ...| tri> _ _ r'<r = inj₂ <⊎$> (propS4 prev∈sys' rc  prev∈sys  c3' (≤-trans (≤-unstep r'<r) (kchain-round-≤-lemma' c3  (suc (suc zero)))))

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary
open import Cubical.Data.Empty
open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Bool

module Direction where

-- some nat things. move to own module?

sucn : (n : ℕ) → (ℕ → ℕ)
sucn n = iter n suc

sucnsuc : (n m : ℕ) → sucn n (suc m) ≡ suc (sucn n m)
sucnsuc zero m = refl
sucnsuc (suc n) m =
    sucn (suc n) (suc m)
  ≡⟨ refl ⟩
    suc (sucn n (suc m))
  ≡⟨ cong suc (sucnsuc n m) ⟩
    suc (suc (sucn n m))
  ∎

doublePred : (n : ℕ) → doubleℕ (predℕ n) ≡ predℕ (predℕ (doubleℕ n))
doublePred zero = refl
doublePred (suc n) = refl

-- doubleDoublesPred : (n : ℕ) → doublesℕ n 1 ≡
-- doubleDoublesPred zero = refl
-- doubleDoublesPred (suc n) = {!!}

sucPred : (n : ℕ) → ¬ (n ≡ zero) → suc (predℕ n) ≡ n
sucPred zero 0≠0 = ⊥-elim (0≠0 refl)
sucPred (suc n) sucn≠0 = refl

predSucSuc : (n : ℕ) → ¬ (predℕ (suc (suc n)) ≡ 0)
predSucSuc n = snotz

doubleDoubles : (n m : ℕ) → doubleℕ (doublesℕ n m) ≡ doublesℕ (suc n) m
doubleDoubles zero m = refl
doubleDoubles (suc n) m = doubleDoubles n (doubleℕ m)

doublePos : (n : ℕ) → ¬ (n ≡ 0) → ¬ (doubleℕ n ≡ 0)
doublePos zero 0≠0 = ⊥-elim (0≠0 refl)
doublePos (suc n) sn≠0 = snotz

doublesPos : (n m : ℕ) → ¬ (m ≡ 0) → ¬ (doublesℕ n m ≡ 0)
doublesPos zero m m≠0 = m≠0
doublesPos (suc n) m m≠0 = doublesPos n (doubleℕ m) (doublePos m (m≠0))

predDoublePos : (n : ℕ) → ¬ (n ≡ 0) → ¬ (predℕ (doubleℕ n)) ≡ 0
predDoublePos zero n≠0 = ⊥-elim (n≠0 refl)
predDoublePos (suc n) sn≠0 = snotz

doubleDoublesOne≠0 : (n : ℕ) → ¬ (doubleℕ (doublesℕ n (suc zero)) ≡ 0)
doubleDoublesOne≠0 zero = snotz
doubleDoublesOne≠0 (suc n) = doublePos (doublesℕ n 2) (doublesPos n 2 (snotz))

predDoubleDoublesOne≠0 : (n : ℕ) → ¬ (predℕ (doubleℕ (doublesℕ n (suc zero))) ≡ 0)
predDoubleDoublesOne≠0 zero = snotz
predDoubleDoublesOne≠0 (suc n) = predDoublePos (doublesℕ n 2) (doublesPos n 2 snotz)

doublesZero : (n : ℕ) → doublesℕ n zero ≡ zero
doublesZero zero = refl
doublesZero (suc n) = doublesZero n

-- 2^n(m+1) = (2^n)m + 2^n
-- doublesSuc : (n m : ℕ) → doublesℕ n (suc m) ≡ sucn (doublesℕ n 1) (doublesℕ n m)
-- doublesSuc zero m = refl
-- doublesSuc (suc n) m =
--     doublesℕ n (suc (suc (doubleℕ m)))
--   ≡⟨ doublesSuc n (suc (doubleℕ m)) ⟩
--     sucn (doublesℕ n 1) (doublesℕ n (suc (doubleℕ m)))
--   ≡⟨ cong (λ z → sucn (doublesℕ n 1) z) (doublesSuc n (doubleℕ m)) ⟩
--      sucn (doublesℕ n 1) (sucn (doublesℕ n 1) (doublesℕ n (doubleℕ m)))
--    ≡⟨ sucnDoubles n (doublesℕ n (doubleℕ m)) ⟩
--      sucn (doublesℕ n 2) (doublesℕ n (doubleℕ m))
--    ∎
--    where
--      sucnDoubles : (n m : ℕ) → sucn (doublesℕ n 1) (sucn (doublesℕ n 1) m) ≡ sucn (doublesℕ n 2) m
--      sucnDoubles zero m = refl
--      sucnDoubles (suc n) m =
--          sucn (doublesℕ n 2) (sucn (doublesℕ n 2) m)
--        ≡⟨ sym (sucnDoubles n (sucn (doublesℕ n 2) m)) ⟩
--          sucn (doublesℕ n 1) (sucn (doublesℕ n 1) (sucn (doublesℕ n 2) m))
--        ≡⟨ {!!} ⟩ {!!}

-- 2 * (i + n) = 2*i + 2*n
doubleSucn : (i n : ℕ) →  doubleℕ (sucn i n) ≡ sucn (doubleℕ i) (doubleℕ n)
doubleSucn zero n = refl
doubleSucn (suc i) n =
    suc (suc (doubleℕ (sucn i n)))
  ≡⟨ cong (λ z → suc (suc z)) (doubleSucn i n) ⟩
    suc (suc (sucn (doubleℕ i) (doubleℕ n)))
  ≡⟨ refl ⟩
    suc (sucn (suc (doubleℕ i)) (doubleℕ n))
  ≡⟨ cong suc refl ⟩
    sucn (suc (suc (doubleℕ i))) (doubleℕ n)
  ∎

doublesSucn : (i n m : ℕ) → doublesℕ n (sucn i m) ≡ sucn (doublesℕ n i) (doublesℕ n m)
doublesSucn i zero m = refl
doublesSucn i (suc n) m =
    doublesℕ n (doubleℕ (sucn i m))
  ≡⟨  cong (doublesℕ n) (doubleSucn i m) ⟩
    doublesℕ n (sucn (doubleℕ i) (doubleℕ m))
  ≡⟨ doublesSucn (doubleℕ i) n (doubleℕ m) ⟩
     sucn (doublesℕ n (doubleℕ i)) (doublesℕ n (doubleℕ m))
  ∎

-- 2^n * (m + 2) =
doublesSucSuc : (n m : ℕ) → doublesℕ n (suc (suc m)) ≡ sucn (doublesℕ (suc n) 1) (doublesℕ n m)
doublesSucSuc zero m = refl
doublesSucSuc (suc n) m =
    doublesℕ (suc n) (suc (suc m))
  ≡⟨ refl ⟩
    doublesℕ n (sucn 4 (doubleℕ m))
  ≡⟨ doublesSucn 4 n (doubleℕ m) ⟩
    sucn (doublesℕ n 4) (doublesℕ n (doubleℕ m))
  ∎

n+n≡2n : (n : ℕ) → sucn n n ≡ doubleℕ n
n+n≡2n zero = refl
n+n≡2n (suc n) =
    sucn (suc n) (suc n)
  ≡⟨ sucnsuc (suc n) n ⟩
    suc (sucn (suc n) n)
  ≡⟨ refl ⟩
   suc (suc (sucn n n))
  ≡⟨ cong (λ z → suc (suc z)) (n+n≡2n n) ⟩
   suc (suc (doubleℕ n))
  ∎

-- predDoubles : (n m : ℕ) → ¬ (n ≡ 0) → ¬ (m ≡ 0) → ¬ (predℕ (doublesℕ n m)) ≡ 0
-- predDoubles zero m n≠0 m≠0 = ⊥-elim (n≠0 refl)
-- predDoubles (suc n) m sn≠0 m≠0 = {!!}

-- "Direction" type for determining direction in spatial structures.
-- We interpret ↓ as 0 and ↑ as 1 when used in numerals in
-- numerical types.
data Dir : Type₀ where
  ↓ : Dir
  ↑ : Dir

caseDir : ∀ {ℓ} → {A : Type ℓ} → (ad au : A) → Dir → A
caseDir ad au ↓ = ad
caseDir ad au ↑ = au

¬↓≡↑ : ¬ ↓ ≡ ↑
¬↓≡↑ eq = subst (caseDir Dir ⊥) eq ↓

¬↑≡↓ : ¬ ↑ ≡ ↓
¬↑≡↓ eq = subst (caseDir ⊥ Dir) eq ↓

-- Dependent "directional numerals":
-- for natural n, obtain 2ⁿ "numerals".
-- This is basically a little-endian binary notation.
-- NOTE: Would an implementation of DirNum with dependent vectors be preferable
--       over using products?
DirNum : ℕ → Type₀
DirNum zero = Unit
DirNum (suc n) = Dir × (DirNum n)

sucDoubleDirNum+ : (r : ℕ) → DirNum r → DirNum (suc r)
sucDoubleDirNum+ r x = (↑ , x)

-- bad name, since this is doubling "to" suc r
doubleDirNum+ : (r : ℕ) → DirNum r → DirNum (suc r)
doubleDirNum+ r x = (↓ , x)

DirNum→ℕ : ∀ {n} → DirNum n → ℕ
DirNum→ℕ {zero} tt = zero
DirNum→ℕ {suc n} (↓ , d) = doublesℕ (suc zero) (DirNum→ℕ d)
DirNum→ℕ {suc n} (↑ , d) = suc (doublesℕ (suc zero) (DirNum→ℕ d))

double-lemma : ∀ {r} → (d : DirNum r) →
                doubleℕ (DirNum→ℕ d) ≡ DirNum→ℕ (doubleDirNum+ r d)
double-lemma {r} d = refl

¬↓,d≡↑,d′ : ∀ {n} → ∀ (d d′ : DirNum n) → ¬ (↓ , d) ≡ (↑ , d′)
¬↓,d≡↑,d′ {n} d d′ ↓,d≡↑,d′ = ¬↓≡↑ (cong proj₁ ↓,d≡↑,d′)

¬↑,d≡↓,d′ : ∀ {n} → ∀ (d d′ : DirNum n) → ¬ (↑ , d) ≡ (↓ , d′)
¬↑,d≡↓,d′ {n} d d′ ↑,d≡↓,d′ = ¬↑≡↓ (cong proj₁ ↑,d≡↓,d′)

-- dropping least significant bit preserves equality
dropLeast≡ : ∀ {n} → ∀ (ds ds′ : DirNum n) (d : Dir)
              → ((d , ds) ≡ (d , ds′)) → ds ≡ ds′
dropLeast≡ {n} ds ds′ d d,ds≡d,ds′ = cong proj₂ d,ds≡d,ds′

-- give the next numeral, cycling back to 0
-- in case of 2ⁿ - 1
next : ∀ {n} → DirNum n → DirNum n
next {zero} tt = tt
next {suc n} (↓ , ds) = (↑ , ds)
next {suc n} (↑ , ds) = (↓ , next ds)

prev : ∀ {n} → DirNum n → DirNum n
prev {zero} tt = tt
prev {suc n} (↓ , ds) = (↓ , prev ds)
prev {suc n} (↑ , ds) = (↓ , ds)

zero-n : (n : ℕ) → DirNum n
zero-n zero = tt
zero-n (suc n) = (↓ , zero-n n)

zero-n→0 : ∀ {r} → DirNum→ℕ (zero-n r) ≡ zero
zero-n→0 {zero} = refl
zero-n→0 {suc r} =
    doubleℕ (DirNum→ℕ (zero-n r))
  ≡⟨ cong doubleℕ (zero-n→0 {r}) ⟩
    doubleℕ zero
  ≡⟨ refl ⟩
    zero
  ∎

zero-n? : ∀ {n} → (x : DirNum n) → Dec (x ≡ zero-n n)
zero-n? {zero} tt = yes refl
zero-n? {suc n} (↓ , ds) with zero-n? ds
... | no ds≠zero-n = no (λ y →
                            ds≠zero-n (dropLeast≡ ds (zero-n n) ↓ y))
... | yes ds≡zero-n = yes (cong (λ y → (↓ , y)) ds≡zero-n)
zero-n? {suc n} (↑ , ds) = no ((¬↑,d≡↓,d′ ds (zero-n n)))

zero-n≡0 : {r : ℕ} → DirNum→ℕ (zero-n r) ≡ zero
zero-n≡0{zero} = refl
zero-n≡0 {suc r} =
    doubleℕ (DirNum→ℕ {r} (zero-n r))
  ≡⟨ cong doubleℕ (zero-n≡0 {r}) ⟩
   0
  ∎

-- x is doubleable as a DirNum precisely when x's most significant bit is 0
-- this should return a Dec
doubleable-n? : {n : ℕ} → (x : DirNum n) → Bool
doubleable-n? {zero} tt = false
doubleable-n? {suc n} (x , x₁) with zero-n? x₁
... | yes _ = true
... | no _ = doubleable-n? x₁

dropMost : {r : ℕ} → DirNum (suc r) → DirNum r
dropMost {zero} d = tt
dropMost {suc zero} (x , (x₁ , x₂)) = (x₁ , x₂)
dropMost {suc (suc r)} (x , x₁) = (x , dropMost x₁)

-- need to prove property about doubleable
--doubleDirNum : (r : ℕ) (d : DirNum r) → doubleable-n? {r} d ≡ true → DirNum r
-- bad:
doubleDirNum : (r : ℕ) (d : DirNum r) → DirNum r
doubleDirNum zero d  = tt
doubleDirNum (suc r) d  = doubleDirNum+ r (dropMost {r} d)
-- doubleDirNum zero d doubleable = ⊥-elim (false≢true doubleable)
-- doubleDirNum (suc r) d doubleable = doubleDirNum+ r (dropMost {r} d)

one-n : (n : ℕ) → DirNum n
one-n zero = tt
one-n (suc n) = (↑ , zero-n n)

-- numeral for 2ⁿ - 1
max-n : (n : ℕ) → DirNum n
max-n zero = tt
max-n (suc n) = (↑ , max-n n)

--half-n : (n : ℕ) → DirNum n

max→ℕ : (r : ℕ) → DirNum→ℕ (max-n r) ≡ predℕ (doublesℕ r 1)
max→ℕ zero = refl
max→ℕ (suc r) =
    suc (doubleℕ (DirNum→ℕ (max-n r)))
  ≡⟨ cong (λ z → suc (doubleℕ z)) (max→ℕ r) ⟩
    suc (doubleℕ (predℕ (doublesℕ r 1)))
  ≡⟨ cong suc (doublePred (doublesℕ r 1)) ⟩
    suc (predℕ (predℕ (doubleℕ (doublesℕ r 1))))
  ≡⟨ cong (λ z → suc (predℕ (predℕ z))) (doubleDoubles r 1) ⟩
    suc (predℕ (predℕ (doublesℕ (suc r) 1)))
  ≡⟨ refl ⟩
    suc (predℕ (predℕ (doublesℕ r 2)))
  ≡⟨ sucPred (predℕ (doublesℕ r 2)) H ⟩
    predℕ (doublesℕ r 2)
  ∎
  where
    G : (r : ℕ) → doubleℕ (doublesℕ r 1) ≡ doublesℕ r 2
    G zero = refl
    G (suc r) = doubleℕ (doublesℕ r 2) ≡⟨ doubleDoubles r 2 ⟩
                 doublesℕ (suc r) 2 ≡⟨ refl ⟩ doublesℕ r (doubleℕ 2) ∎
    H : ¬ predℕ (doublesℕ r 2) ≡ zero
    H = λ h → (predDoublePos (doublesℕ r 1) (doublesPos r 1 snotz)
        ((
          predℕ (doubleℕ (doublesℕ r 1)) ≡⟨ cong predℕ (G r) ⟩
          predℕ (doublesℕ r 2) ≡⟨ h ⟩
          0 ∎
         )))

max? : ∀ {n} → (x : DirNum n) → Dec (x ≡ max-n n)
max? {zero} tt = yes refl
max? {suc n} (↓ , ds) = no ((¬↓,d≡↑,d′ ds (max-n n)))
max? {suc n} (↑ , ds) with max? ds
... | yes ds≡max-n = yes (
          (↑ , ds)
        ≡⟨ cong (λ x → (↑ , x)) ds≡max-n ⟩
          (↑ , max-n n)
        ∎
      )
... | no ¬ds≡max-n = no (λ d,ds≡d,max-n →
                            ¬ds≡max-n ((dropLeast≡ ds (max-n n) ↑ d,ds≡d,max-n)))

maxn+1≡↑maxn : ∀ n → max-n (suc n) ≡ (↑ , (max-n n))
maxn+1≡↑maxn n = refl

maxr≡pred2ʳ : (r : ℕ) (d : DirNum r) →
           d ≡ max-n r → DirNum→ℕ d ≡ predℕ (doublesℕ r (suc zero))
maxr≡pred2ʳ zero d d≡max = refl
maxr≡pred2ʳ (suc r) (↓ , ds) d≡max = ⊥-elim ((¬↓,d≡↑,d′ ds (max-n r)) d≡max)
maxr≡pred2ʳ (suc r) (↑ , ds) d≡max =
     suc (doubleℕ (DirNum→ℕ ds))
   ≡⟨ cong (λ x → suc (doubleℕ x)) (maxr≡pred2ʳ r ds ds≡max) ⟩
     suc (doubleℕ (predℕ (doublesℕ r (suc zero)))) -- 2*(2^r - 1) + 1 = 2^r+1 - 1
   ≡⟨ cong suc (doublePred (doublesℕ r (suc zero))) ⟩
     suc (predℕ (predℕ (doubleℕ (doublesℕ r (suc zero)))))
   ≡⟨ sucPred (predℕ (doubleℕ (doublesℕ r (suc zero)))) (
              (predDoublePos (doublesℕ r (suc zero)) ((doublesPos r 1 snotz)))) ⟩
     predℕ (doubleℕ (doublesℕ r (suc zero)))
   ≡⟨ cong predℕ (doubleDoubles r (suc zero)) ⟩
     predℕ (doublesℕ (suc r) 1)
   ≡⟨ refl ⟩
     predℕ (doublesℕ r 2) -- 2^r*2 - 1 = 2^(r+1) - 1
   ∎
  where
    ds≡max : ds ≡ max-n r
    ds≡max = dropLeast≡ ds (max-n r) ↑ d≡max

-- TODO: rename
embed-next : (r : ℕ) → DirNum r → DirNum (suc r)
embed-next zero tt = (↓ , tt)
embed-next (suc r) (d , ds) with zero-n? ds
... | no _ = (d , embed-next r ds)
... | yes _ = (d , zero-n (suc r))

-- embed-next-thm : (r : ℕ) (d : DirNum r) → DirNum→ℕ d ≡ DirNum→ℕ (embed-next r d)
-- embed-next-thm zero d = refl
-- embed-next-thm (suc r) (d , ds) with zero-n? ds
-- ... | no _ = {!!}
-- ... | yes _ = {!!}

-- TODO: rename?
nextsuc-lemma : (r : ℕ) (x : DirNum r) →
         ¬ ((sucDoubleDirNum+ r x) ≡ max-n (suc r)) → ¬ (x ≡ max-n r)
nextsuc-lemma zero tt ¬H = ⊥-elim (¬H refl)
nextsuc-lemma (suc r) (↓ , x) ¬H = ¬↓,d≡↑,d′ x (max-n r)
nextsuc-lemma (suc r) (↑ , x) ¬H =
  λ h → ¬H (H (dropLeast≡ x (max-n r) ↑ h)) --⊥-elim (¬H H)
  where
    H : (x ≡ max-n r) →
         sucDoubleDirNum+ (suc r) (↑ , x) ≡ (↑ , (↑ , max-n r))
    H x≡maxnr =
        sucDoubleDirNum+ (suc r) (↑ , x)
      ≡⟨ cong (λ y → sucDoubleDirNum+ (suc r) (↑ , y)) x≡maxnr ⟩
        sucDoubleDirNum+ (suc r) (↑ , max-n r)
      ≡⟨ refl ⟩
        (↑ , (↑ , max-n r))
      ∎

next≡suc : (r : ℕ) (x : DirNum r) →
            ¬ (x ≡ max-n r) → DirNum→ℕ (next x) ≡ suc (DirNum→ℕ x)
next≡suc zero tt ¬x≡maxnr = ⊥-elim (¬x≡maxnr refl)
next≡suc (suc r) (↓ , x) ¬x≡maxnr = refl
next≡suc (suc r) (↑ , x) ¬x≡maxnr =
    doubleℕ (DirNum→ℕ (next x))
  ≡⟨ cong doubleℕ (next≡suc r x (nextsuc-lemma r x ¬x≡maxnr)) ⟩
    doubleℕ (suc (DirNum→ℕ x))
  ≡⟨ refl ⟩
    suc (suc (doubleℕ (DirNum→ℕ x)))
  ∎

-- doublesuclemma : (r : ℕ) (x : DirNum (suc r)) →
--          doubleℕ (DirNum→ℕ (next x)) ≡ suc (suc (doubleℕ (DirNum→ℕ x)))
-- doublesuclemma zero (↓ , x₁) = refl
-- doublesuclemma zero (↑ , x₁) = {!!}
-- doublesuclemma (suc r) x = {!!}
  --     doubleℕ (DirNum→ℕ (next x))
  -- ≡⟨ cong doubleℕ (next≡suc r x ¬x≡maxnr) ⟩
  --   doubleℕ (suc (DirNum→ℕ x))
  -- ≡⟨ refl ⟩
  --   suc (suc (doubleℕ (DirNum→ℕ x)))
  -- ∎

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
{-# OPTIONS --irrelevant-projections #-}

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

module Erased where

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

  open Erased

  record _↔_ (A B : Set) : Set where
    field
      to      : A → B
      from    : B → A
      to∘from : ∀ x → to (from x) ≡ x
      from∘to : ∀ x → from (to x) ≡ x

  postulate
    A : Set
    P : (B : Set) → (Erased A → B) → Set
    p : (B : Set) (f : Erased A ↔ B) → P B (_↔_.to f)

  fails : P (Erased (Erased A)) (λ (x : Erased A) → [ x ])
  fails =
    p _ (record
           { from    = λ ([ x ]) → [ erased x ]
           ; to∘from = refl
           ; from∘to = λ _ → refl _
           })

module Irrelevant where

  record Irrelevant (A : Set) : Set where
    constructor [_]
    field
      .irr : A

  open Irrelevant

  record _↔_ (A B : Set) : Set where
    field
      to      : A → B
      from    : B → A
      to∘from : ∀ x → to (from x) ≡ x
      from∘to : ∀ x → from (to x) ≡ x

  postulate
    A : Set
    P : (B : Set) → (Irrelevant A → B) → Set
    p : (B : Set) (f : Irrelevant A ↔ B) → P B (_↔_.to f)

  fails : P (Irrelevant (Irrelevant A)) (λ (x : Irrelevant A) → [ x ])
  fails =
    p _ (record
           { from    = λ ([ x ]) → [ irr x ]
           ; to∘from = refl
           ; from∘to = λ _ → refl _
           })


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

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

module Lambda.Simplified.Partiality-monad.Inductive.Virtual-machine
  where

open import Equality.Propositional
open import Prelude hiding (⊥)

open import Monad equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints

open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine

open Closure Code

-- A functional semantics for the VM.
--
-- For an alternative definition, see the semantics in
-- Lambda.Partiality-monad.Inductive.Virtual-machine, which is defined
-- without using a fixpoint combinator.

execP : State → Partial State (λ _ → Maybe Value) (Maybe Value)
execP s with step s
... | continue s′ = rec s′
... | done v      = return (just v)
... | crash       = return nothing

exec : State → Maybe Value ⊥
exec s = fixP execP s

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

open import HoTT
open import experimental.TwoConstancyHIT

module experimental.TwoConstancy
  {i j} {A : Type i} {B : Type j} (B-is-gpd : is-gpd B)
  (f : A → B)
  (f-is-const₀ : ∀ a₁ a₂ → f a₁ == f a₂)
  (f-is-const₁ : ∀ a₁ a₂ a₃
    → f-is-const₀ a₁ a₂ ∙' f-is-const₀ a₂ a₃ == f-is-const₀ a₁ a₃) where

  private
    abstract
      lemma₁ : ∀ a (t₂ : TwoConstancy A) → point a == t₂
      lemma₁ a = TwoConstancy-elim {P = λ t₂ → point a == t₂}
        (λ _ → =-preserves-level 1 TwoConstancy-level)
        (λ b → link₀ a b)
        (λ b₁ b₂ → ↓-cst=idf-in' $ link₁ a b₁ b₂)
        (λ b₁ b₂ b₃ → set-↓-has-all-paths-↓ $ TwoConstancy-level _ _ )

      lemma₂ : ∀ (a₁ a₂ : A) →
        lemma₁ a₁ == lemma₁ a₂ [ (λ t₁ → ∀ t₂ → t₁ == t₂) ↓ link₀ a₁ a₂ ]
      lemma₂ a₁ a₂ = ↓-cst→app-in $
        TwoConstancy-elim
          {P = λ t₂ → lemma₁ a₁ t₂ == lemma₁ a₂ t₂ [ (λ t₁ → t₁ == t₂) ↓ link₀ a₁ a₂ ]}
          (λ _ → ↓-preserves-level 1 λ _ → =-preserves-level 1 TwoConstancy-level)
          (λ b → ↓-idf=cst-in $ ! $ link₁ a₁ a₂ b)
          (λ b₁ b₂ → prop-has-all-paths-↓ $ ↓-level λ _ → TwoConstancy-level _ _)
          (λ b₁ b₂ b₃ → prop-has-all-paths-↓ $ contr-is-prop
            $ ↓-level λ _ → ↓-level λ _ → TwoConstancy-level _ _)

      TwoConstancy-has-all-paths : has-all-paths (TwoConstancy A)
      TwoConstancy-has-all-paths =
        TwoConstancy-elim {P = λ t₁ → ∀ t₂ → t₁ == t₂}
          (λ _ → Π-level λ _ → =-preserves-level 1 TwoConstancy-level)
          lemma₁
          lemma₂
          (λ a₁ a₂ a₃ → prop-has-all-paths-↓
            $ ↓-level λ t₁ → Π-is-set λ t₂ → TwoConstancy-level t₁ t₂)

  TwoConstancy-is-prop : is-prop (TwoConstancy A)
  TwoConstancy-is-prop = all-paths-is-prop TwoConstancy-has-all-paths

  cst-extend : Trunc -1 A → B
  cst-extend = TwoConstancy-rec B-is-gpd f f-is-const₀ f-is-const₁
             ∘ Trunc-rec TwoConstancy-is-prop point

  -- The beta rule.
  -- This is definitionally true, so you don't need it.
  cst-extend-β : cst-extend ∘ [_] == f
  cst-extend-β = idp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Applicative functors
------------------------------------------------------------------------

-- Note that currently the applicative functor laws are not included
-- here.

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

module Category.Applicative where

open import Data.Unit
open import Category.Applicative.Indexed

RawApplicative : ∀ {f} → (Set f → Set f) → Set _
RawApplicative F = RawIApplicative {I = ⊤} (λ _ _ → F)

module RawApplicative {f} {F : Set f → Set f}
                      (app : RawApplicative F) where
  open RawIApplicative app public

RawApplicativeZero : ∀ {f} → (Set f → Set f) → Set _
RawApplicativeZero F = RawIApplicativeZero {I = ⊤} (λ _ _ → F)

module RawApplicativeZero {f} {F : Set f → Set f}
                          (app : RawApplicativeZero F) where
  open RawIApplicativeZero app public

RawAlternative : ∀ {f} → (Set f → Set f) → Set _
RawAlternative F = RawIAlternative {I = ⊤} (λ _ _ → F)

module RawAlternative {f} {F : Set f → Set f}
                          (app : RawAlternative F) where
  open RawIAlternative app public


text:
------------------------------------------------------------------------
-- A definitional interpreter that is instrumented with information
-- about the number of steps required to run the compiled program
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Interpreter.Steps
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

import Equality.Propositional as E

open import Monad E.equality-with-J
open import Vec.Data E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity

open import Lambda.Delay-crash
import Lambda.Interpreter def as I

open Closure Tm

------------------------------------------------------------------------
-- The interpreter

-- A step annotation.

infix 1 ✓_

✓_ : ∀ {A i} → Delay-crash A i → Delay-crash A i
✓ x = later λ { .force → x }

-- The instrumented interpreter.

infix 10 _∙_

mutual

  ⟦_⟧ : ∀ {i n} → Tm n → Env n → Delay-crash Value i
  ⟦ var x ⟧       ρ = ✓ return (index ρ x)
  ⟦ lam t ⟧       ρ = ✓ return (lam t ρ)
  ⟦ t₁ · t₂ ⟧     ρ = do v₁ ← ⟦ t₁ ⟧ ρ
                         v₂ ← ⟦ t₂ ⟧ ρ
                         v₁ ∙ v₂
  ⟦ call f t ⟧    ρ = do v ← ⟦ t ⟧ ρ
                         lam (def f) [] ∙ v
  ⟦ con b ⟧       ρ = ✓ return (con b)
  ⟦ if t₁ t₂ t₃ ⟧ ρ = do v₁ ← ⟦ t₁ ⟧ ρ
                         ⟦if⟧ v₁ t₂ t₃ ρ

  _∙_ : ∀ {i} → Value → Value → Delay-crash Value i
  lam t₁ ρ ∙ v₂ = later λ { .force → ⟦ t₁ ⟧ (v₂ ∷ ρ) }
  con _    ∙ _  = crash

  ⟦if⟧ : ∀ {i n} →
         Value → Tm n → Tm n → Env n → Delay-crash Value i
  ⟦if⟧ (lam _ _)   _  _  _ = crash
  ⟦if⟧ (con true)  t₂ t₃ ρ = ✓ ⟦ t₂ ⟧ ρ
  ⟦if⟧ (con false) t₂ t₃ ρ = ✓ ⟦ t₃ ⟧ ρ

------------------------------------------------------------------------
-- The semantics given above gives the same (uninstrumented) result as
-- the one in Lambda.Interpreter

mutual

  -- The result of the instrumented interpreter is an expansion of
  -- that of the uninstrumented interpreter.

  ⟦⟧≳⟦⟧ :
    ∀ {i n} (t : Tm n) {ρ : Env n} →
    [ i ] ⟦ t ⟧ ρ ≳ I.⟦ t ⟧ ρ
  ⟦⟧≳⟦⟧ (var x)       = laterˡ (reflexive _)
  ⟦⟧≳⟦⟧ (lam t)       = laterˡ (reflexive _)
  ⟦⟧≳⟦⟧ (t₁ · t₂)     = ⟦⟧≳⟦⟧ t₁ >>=-cong λ _ →
                        ⟦⟧≳⟦⟧ t₂ >>=-cong λ _ →
                        ∙≳∙ _
  ⟦⟧≳⟦⟧ (call f t)    = ⟦⟧≳⟦⟧ t >>=-cong λ _ →
                        ∙≳∙ _
  ⟦⟧≳⟦⟧ (con b)       = laterˡ (reflexive _)
  ⟦⟧≳⟦⟧ (if t₁ t₂ t₃) = ⟦⟧≳⟦⟧ t₁ >>=-cong λ _ →
                        ⟦if⟧≳⟦if⟧ _ t₂ t₃

  ∙≳∙ :
    ∀ {i} (v₁ {v₂} : Value) →
    [ i ] v₁ ∙ v₂ ≳ v₁ I.∙ v₂
  ∙≳∙ (lam t₁ ρ) = later λ { .force → ⟦⟧≳⟦⟧ t₁ }
  ∙≳∙ (con _)    = reflexive _

  ⟦if⟧≳⟦if⟧ :
    ∀ {i n} v₁ (t₂ t₃ : Tm n) {ρ} →
    [ i ] ⟦if⟧ v₁ t₂ t₃ ρ ≳ I.⟦if⟧ v₁ t₂ t₃ ρ
  ⟦if⟧≳⟦if⟧ (lam _ _)   _  _  = reflexive _
  ⟦if⟧≳⟦if⟧ (con true)  t₂ t₃ = laterˡ (⟦⟧≳⟦⟧ t₂)
  ⟦if⟧≳⟦if⟧ (con false) t₂ t₃ = laterˡ (⟦⟧≳⟦⟧ t₃)

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
open import Agda.Primitive

postulate
  ∞  : ∀ {a} (A : Set a) → Set (lsuc a)

{-# BUILTIN INFINITY ∞  #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- {-# OPTIONS -v tc.lhs.problem:10 #-}
-- {-# OPTIONS --compile --ghc-flag=-i.. #-}
module Issue727 where

open import Common.Prelude renaming (Nat to ℕ)
open import Common.MAlonzo hiding (main)

Sum : ℕ → Set
Sum 0       = ℕ
Sum (suc n) = ℕ → Sum n

sum : (n : ℕ) → ℕ → Sum n
sum 0       acc   = acc
sum (suc n) acc m = sum n (m + acc)

main = mainPrintNat (sum 3 0 1 2 3)

max_stars_repo_name: larrytheliquid/agda


text:
 {-# OPTIONS --type-in-type #-}

module IDescTT where

--********************************************
-- Prelude
--********************************************

-- Some preliminary stuffs, to avoid relying on the stdlib

--****************
-- Sigma and friends
--****************

data Sigma (A : Set) (B : A -> Set) : Set where
  _,_ : (x : A) (y : B x) -> Sigma A B

_*_ : (A : Set)(B : Set) -> Set
A * B = Sigma A \_ -> B

fst : {A : Set}{B : A -> Set} -> Sigma A B -> A
fst (a , _) = a

snd : {A : Set}{B : A -> Set} (p : Sigma A B) -> B (fst p)
snd (a , b) = b

data Zero : Set where
data Unit  : Set where
  Void : Unit

--****************
-- Sum and friends
--****************

data _+_ (A : Set)(B : Set) : Set where
  l : A -> A + B
  r : B -> A + B

--****************
-- Equality
--****************

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

subst : forall {x y} -> x == y -> x -> y
subst refl x = x

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

cong2 : {A B C : Set}(f : A -> B -> C){x y : A}{z t : B} ->
        x == y -> z == t -> f x z == f y t
cong2 f refl refl = refl

postulate
  reflFun : {A B : Set}(f : A -> B)(g : A -> B)-> ((a : A) -> f a == g a) -> f == g

--****************
-- Meta-language
--****************

-- Note that we could define Nat, Bool, and the related operations in
-- IDesc. But it is awful to code with them, in Agda.

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

data Bool : Set where
  true : Bool
  false : Bool

plus : Nat -> Nat -> Nat
plus ze n' = n'
plus (su n) n' = su (plus n n')

le : Nat -> Nat -> Bool
le ze _ = true
le (su _) ze = false
le (su n) (su n') = le n n'

--********************************************
-- Desc code
--********************************************

data IDesc (I : Set) : Set where
  var : I -> IDesc I
  const : Set -> IDesc I
  prod : IDesc I -> IDesc I -> IDesc I
  sigma : (S : Set) -> (S -> IDesc I) -> IDesc I
  pi : (S : Set) -> (S -> IDesc I) -> IDesc I

--********************************************
-- Desc interpretation
--********************************************

[|_|] : {I : Set} -> IDesc I -> (I -> Set) -> Set
[| var i |] P = P i
[| const X |] P = X
[| prod D D' |] P = [| D |] P * [| D' |] P
[| sigma S T |] P = Sigma S (\s -> [| T s |] P)
[| pi S T |] P = (s : S) -> [| T s |] P

--********************************************
-- Fixpoint construction
--********************************************

data IMu {I : Set}(R : I -> IDesc I)(i : I) : Set where
  con : [| R i |] (\j -> IMu R j) -> IMu R i

--********************************************
-- Predicate: All
--********************************************

All : {I : Set}(D : IDesc I)(P : I -> Set) -> [| D |] P -> IDesc (Sigma I P)
All (var i)     P x        = var (i , x)
All (const X)   P x        = const Unit
All (prod D D') P (d , d') = prod (All D P d) (All D' P d')
All (sigma S T) P (a , b)  = All (T a) P b
All (pi S T)    P f        = pi S (\s -> All (T s) P (f s))

all : {I : Set}(D : IDesc I)(X : I -> Set)
      (R : Sigma I X -> Set)(P : (x : Sigma I X) -> R x) ->
      (xs : [| D |] X) -> [| All D X xs |] R
all (var i) X R P x = P (i , x)
all (const K) X R P k = Void
all (prod D D') X R P (x , y) = ( all D X R P x , all D' X R P y )
all (sigma S T) X R P (a , b) = all (T a) X R P b
all (pi S T) X R P f = \a -> all (T a) X R P (f a)

--********************************************
-- Elimination principle: induction
--********************************************

-- One would like to write the following:

{-
indI : {I : Set}
            (R : I -> IDesc I)
            (P : Sigma I (IMu R) -> Set)
            (m : (i : I)
                 (xs : [| R i |] (IMu R))
                 (hs : [| All (R i) (IMu R) xs |] P) ->
                 P ( i , con xs)) ->
            (i : I)(x : IMu R i) -> P ( i , x )
indI {I} R P m i (con xs) = m i xs (all (R i) (IMu R) P induct xs)
  where induct : (x : Sigma I (IMu R)) -> P x
        induct (i , xs) = indI R P m i xs
-}

-- But the termination-checker complains, so here we go
-- inductive-recursive:

module Elim {I : Set}
            (R : I -> IDesc I)
            (P : Sigma I (IMu R) -> Set)
            (m : (i : I)
                 (xs : [| R i |] (IMu R))
                 (hs : [| All (R i) (IMu R) xs |] P) ->
                 P ( i , con xs ))
       where

  mutual
    indI : (i : I)(x : IMu R i) -> P (i , x)
    indI i (con xs) = m i xs (hyps (R i) xs)

    hyps : (D : IDesc I) ->
           (xs : [| D |] (IMu R)) ->
           [| All D (IMu R) xs |] P
    hyps (var i) x = indI i x
    hyps (const X) x = Void
    hyps (prod D D') (d , d') =  hyps D d , hyps D' d'
    hyps (pi S R) f = \ s -> hyps (R s) (f s)
    hyps (sigma S R) ( a , b ) = hyps (R a) b

indI : {I : Set}
       (R : I -> IDesc I)
       (P : Sigma I (IMu R) -> Set)
       (m : (i : I)
            (xs : [| R i |] (IMu R))
            (hs : [| All (R i) (IMu R) xs |] P) ->
            P ( i , con xs)) ->
       (i : I)(x : IMu R i) -> P ( i , x )
indI = Elim.indI

--********************************************
-- Examples
--********************************************

--****************
-- Nat
--****************

data NatConst : Set where
  Ze : NatConst
  Su : NatConst

natCases : NatConst -> IDesc Unit
natCases Ze = const Unit
natCases Suc = var Void

NatD : Unit -> IDesc Unit
NatD Void = sigma NatConst  natCases

Natd : Unit -> Set
Natd x = IMu NatD x

zed : Natd Void
zed = con (Ze , Void)

sud : Natd Void -> Natd Void
sud n = con (Su , n)

--****************
-- Desc
--****************

data DescDConst : Set where
  lvar   : DescDConst
  lconst : DescDConst
  lprod  : DescDConst
  lpi    : DescDConst
  lsigma : DescDConst

descDChoice : Set -> DescDConst -> IDesc Unit
descDChoice I lvar = const I
descDChoice _ lconst = const Set
descDChoice _ lprod = prod (var Void) (var Void)
descDChoice _ lpi = sigma Set (\S -> pi S (\s -> var Void))
descDChoice _ lsigma = sigma Set (\S -> pi S (\s -> var Void))

descD : (I : Set) -> IDesc Unit
descD I = sigma DescDConst (descDChoice I)

IDescl0 : (I : Set) -> Unit -> Set
IDescl0 I = IMu (\_ -> descD I)

IDescl : (I : Set) -> Set
IDescl I = IDescl0 I _

varl : {I : Set}(i : I) -> IDescl I
varl i = con (lvar ,  i)

constl : {I : Set}(X : Set) -> IDescl I
constl X = con (lconst , X)

prodl : {I : Set}(D D' : IDescl I) -> IDescl I
prodl D D' = con (lprod , (D , D'))

pil : {I : Set}(S : Set)(T : S -> IDescl I) -> IDescl I
pil S T = con (lpi , ( S , T))

sigmal : {I : Set}(S : Set)(T : S -> IDescl I) -> IDescl I
sigmal S T = con (lsigma , ( S , T))

--****************
-- Vec (constraints)
--****************

data VecConst : Set where
  Vnil : VecConst
  Vcons : VecConst

vecDChoice : Set -> Nat -> VecConst -> IDesc Nat
vecDChoice X n Vnil = const (n == ze)
vecDChoice X n Vcons = sigma Nat (\m -> prod (var m) (const (n == su m)))

vecD : Set -> Nat -> IDesc Nat
vecD X n = sigma VecConst (vecDChoice X n)

vec : Set -> Nat -> Set
vec X n = IMu (vecD X) n

--****************
-- Vec (de-tagged, forced)
--****************

data VecConst2 : Nat -> Set where
  Vnil : VecConst2 ze
  Vcons : {n : Nat} -> VecConst2 (su n)

vecDChoice2 : Set -> (n : Nat) -> VecConst2 n -> IDesc Nat
vecDChoice2 X ze Vnil = const Unit
vecDChoice2 X (su n) Vcons = prod (const X) (var n)

vecD2 : Set -> Nat -> IDesc Nat
vecD2 X n = sigma (VecConst2 n) (vecDChoice2 X n)

vec2 : Set -> Nat -> Set
vec2 X n = IMu (vecD2 X) n

--****************
-- Fin (de-tagged)
--****************

data FinConst : Nat -> Set where
  Fz : {n : Nat} -> FinConst (su n)
  Fs : {n : Nat} -> FinConst (su n)

finDChoice : (n : Nat) -> FinConst n -> IDesc Nat
finDChoice ze ()
finDChoice (su n) Fz = const Unit
finDChoice (su n) Fs = var n

finD : Nat -> IDesc Nat
finD n = sigma (FinConst n) (finDChoice n)

fin : Nat -> Set
fin n = IMu finD n

--********************************************
-- Enumerations (hard-coded)
--********************************************

-- Unlike in Desc.agda, we don't carry the levitation of finite sets
-- here. We hard-code them and manipulate with standard Agda
-- machinery. Both presentation are isomorph but, in Agda, the coded
-- one quickly gets unusable.

data EnumU : Set where
  nilE : EnumU
  consE : EnumU -> EnumU

data EnumT : (e : EnumU) -> Set where
  EZe : {e : EnumU} -> EnumT (consE e)
  ESu : {e : EnumU} -> EnumT e -> EnumT (consE e)

spi : (e : EnumU)(P : EnumT e -> Set) -> Set
spi nilE P = Unit
spi (consE e) P = P EZe * spi e (\e -> P (ESu e))

switch : (e : EnumU)(P : EnumT e -> Set)(b : spi e P)(x : EnumT e) -> P x
switch nilE P b ()
switch (consE e) P b EZe = fst b
switch (consE e) P b (ESu n) = switch e (\e -> P (ESu e)) (snd b) n

_++_ : EnumU -> EnumU -> EnumU
nilE ++ e' = e'
(consE e) ++ e' = consE (e ++ e')

-- A special switch, for tagged descriptions. Switching on a
-- concatenation of finite sets:
sswitch : (e : EnumU)(e' : EnumU)(P : Set)
       (b : spi e (\_ -> P))(b' : spi e' (\_ -> P))(x : EnumT (e ++ e')) -> P
sswitch nilE nilE P b b' ()
sswitch nilE (consE e') P b b' EZe = fst b'
sswitch nilE (consE e') P b b' (ESu n) = sswitch nilE e' P b (snd b') n
sswitch (consE e) e' P b b' EZe = fst b
sswitch (consE e) e' P b b' (ESu n) = sswitch e e' P (snd b) b' n

--********************************************
-- Tagged indexed description
--********************************************

FixMenu : Set -> Set
FixMenu I = Sigma EnumU (\e -> (i : I) -> spi e (\_ -> IDesc I))

SensitiveMenu : Set -> Set
SensitiveMenu I = Sigma (I -> EnumU) (\F -> (i : I) -> spi (F i) (\_ -> IDesc I))

TagIDesc : Set -> Set
TagIDesc I = FixMenu I * SensitiveMenu I

toIDesc : (I : Set) -> TagIDesc I -> (I -> IDesc I)
toIDesc I ((E , ED) , (F , FD)) i = sigma (EnumT (E ++ F i))
                                          (\x -> sswitch E (F i) (IDesc I) (ED i) (FD i) x)

--********************************************
-- Catamorphism
--********************************************

cata : (I : Set)
       (R : I -> IDesc I)
       (T : I -> Set) ->
       ((i : I) -> [| R i |] T -> T i) ->
       (i : I) -> IMu R i -> T i
cata I R T phi i x = indI R (\it -> T (fst it)) (\i xs ms -> phi i (replace (R i) T xs ms)) i x
  where replace : (D : IDesc I)(T : I -> Set)
                  (xs : [| D |] (IMu R))
                  (ms : [| All D (IMu R) xs |] (\it -> T (fst it))) ->
                  [| D |] T
        replace (var i) T x y = y
        replace (const Z) T z z' = z
        replace (prod D D') T (x , x') (y , y') = replace D T x y , replace D' T x' y'
        replace (sigma A B) T (a , b) t = a , replace (B a) T b t
        replace (pi A B) T f t = \s -> replace (B s) T (f s) (t s)

--********************************************
-- Hutton's razor
--********************************************

--********************************
-- Types code
--********************************

data Type : Set where
  nat : Type
  bool : Type
  pair : Type -> Type -> Type

--********************************
-- Typed expressions
--********************************

Val : Type -> Set
Val nat = Nat
Val bool = Bool
Val (pair x y) = (Val x) * (Val y)

-- Fix menu:
exprFixMenu : FixMenu Type
exprFixMenu = ( consE (consE nilE) ,
                \ty -> (const (Val ty),                           -- Val t
                       (prod (var bool) (prod (var ty) (var ty)), -- if b then t1 else t2
                       Void)))

-- Indexed menu:
choiceMenu : Type -> EnumU
choiceMenu nat = consE nilE
choiceMenu bool = consE nilE
choiceMenu (pair x y) = nilE

choiceDessert : (ty : Type) -> spi (choiceMenu ty) (\ _ -> IDesc Type)
choiceDessert nat = (prod (var nat) (var nat) , Void)
choiceDessert bool = (prod (var nat) (var nat) , Void )
choiceDessert (pair x y) = Void

exprSensitiveMenu : SensitiveMenu Type
exprSensitiveMenu = ( choiceMenu ,  choiceDessert )

-- Expression:
expr : TagIDesc Type
expr = exprFixMenu , exprSensitiveMenu

exprIDesc : TagIDesc Type -> (Type -> IDesc Type)
exprIDesc D = toIDesc Type D

--********************************
-- Closed terms
--********************************

closeTerm : Type -> IDesc Type
closeTerm = exprIDesc expr

--********************************
-- Closed term evaluation
--********************************

eval : {ty : Type} -> IMu closeTerm ty -> Val ty
eval {ty} term = cata Type closeTerm Val evalOneStep ty term
        where evalOneStep : (ty : Type) -> [| closeTerm ty |] Val -> Val ty
              evalOneStep _ (EZe , t) = t
              evalOneStep _ ((ESu EZe) , (true , ( x , _))) = x
              evalOneStep _ ((ESu EZe) , (false , ( _ , y ))) = y
              evalOneStep nat ((ESu (ESu EZe)) , (x , y)) = plus x y
              evalOneStep nat ((ESu (ESu (ESu ()))) , t)
              evalOneStep bool ((ESu (ESu EZe)) , (x , y) ) =   le x y
              evalOneStep bool ((ESu (ESu (ESu ()))) , _)
              evalOneStep (pair x y) (ESu (ESu ()) , _)

--********************************************
-- Free monad construction
--********************************************

_**_ : {I : Set} (R : TagIDesc I)(X : I -> Set) -> TagIDesc I
((E , ED) , FFD) ** X = ((( consE E ,  \ i -> ( const (X i) , ED i ))) , FFD)

--********************************************
-- Substitution
--********************************************

apply : {I : Set}
        (R : TagIDesc I)(X Y : I -> Set) ->
        ((i : I) -> X i -> IMu (toIDesc I (R ** Y)) i) ->
        (i : I) ->
        [| toIDesc I (R ** X) i |] (IMu (toIDesc I (R ** Y))) ->
        IMu (toIDesc I (R ** Y)) i
apply (( E , ED) , (F , FD)) X Y sig i (EZe , x) = sig i x
apply (( E , ED) , (F , FD)) X Y sig i (ESu n , t) = con (ESu n , t)

substI : {I : Set} (X Y : I -> Set)(R : TagIDesc I)
         (sigma : (i : I) -> X i -> IMu (toIDesc I (R ** Y)) i)
         (i : I)(D : IMu (toIDesc I (R ** X)) i) ->
         IMu (toIDesc I (R ** Y)) i
substI {I} X Y R sig i term = cata I (toIDesc I (R ** X)) (IMu (toIDesc I (R ** Y))) (apply R X Y sig) i term

--********************************************
-- Hutton's razor is free monad
--********************************************

Empty : Type -> Set
Empty _ = Zero

closeTerm' : Type -> IDesc Type
closeTerm' = toIDesc Type (expr ** Empty)

update : {ty : Type} -> IMu closeTerm ty -> IMu closeTerm' ty
update {ty} tm = cata Type closeTerm (IMu closeTerm') (\ _ tagTm -> con (ESu (fst tagTm) , (snd tagTm))) ty tm

--********************************
-- Closed term' evaluation
--********************************

eval' : {ty : Type} -> IMu closeTerm' ty -> Val ty
eval' {ty} term = cata Type closeTerm' Val evalOneStep ty term
        where evalOneStep : (ty : Type) -> [| closeTerm' ty |] Val -> Val ty
              evalOneStep _ (EZe , ())
              evalOneStep _ (ESu EZe , t) = t
              evalOneStep _ ((ESu (ESu EZe)) , (true , ( x , _))) = x
              evalOneStep _ ((ESu (ESu EZe)) , (false , ( _ , y ))) = y
              evalOneStep nat ((ESu (ESu (ESu EZe))) , (x , y)) = plus x y
              evalOneStep nat (((ESu (ESu (ESu (ESu ()))))) , t)
              evalOneStep bool ((ESu (ESu (ESu EZe))) , (x , y) ) =   le x y
              evalOneStep bool ((ESu (ESu (ESu (ESu ())))) , _)
              evalOneStep (pair x y) (ESu (ESu (ESu ())) , _)

--********************************
-- Open terms
--********************************

-- A context is a snoc-list of types
-- put otherwise, a context is a type telescope
data Context : Set where
  [] : Context
  _,_ : Context -> Type -> Context

-- The environment realizes the context, having a value for each type
Env : Context -> Set
Env []      = Unit
Env (G , S)  = Env G * Val S

-- A typed-variable indexes into the context, obtaining a proof that
-- what we get is what you want (WWGIWYW)
Var : Context -> Type -> Set
Var []      T = Zero
Var (G , S) T = Var G T + (S == T)

-- The lookup gets into the context to extract the value
lookup : (G : Context) -> Env G -> (T : Type) -> Var G T -> Val T
lookup []        _       T ()
lookup (G , .T)  (g , t) T (r refl) = t
lookup (G , S)   (g , t) T (l x)    = lookup G g T x

-- Open term: holes are either values or variables in a context
openTerm : Context -> Type -> IDesc Type
openTerm c = toIDesc Type (expr ** (Var c))

--********************************
-- Evaluation of open terms
--********************************

-- |discharge| is the local substitution expected by |substI|. It is
-- just sugar around context lookup
discharge : (context : Context) ->
            Env context ->
            (ty : Type) ->
            Var context ty ->
            IMu closeTerm' ty
discharge ctxt env ty variable = con (ESu EZe , lookup ctxt env ty variable )

-- |substExpr| is the specialized |substI| to expressions. We get it
-- generically from the free monad construction.
substExpr : {ty : Type}
            (context : Context)
            (sigma : (ty : Type) ->
                     Var context ty ->
                     IMu closeTerm' ty) ->
            IMu (openTerm context) ty ->
            IMu closeTerm' ty
substExpr {ty} c sig term =
    substI (Var c) Empty expr sig ty term

-- By first doing substitution to close the term, we can use
-- evaluation of closed terms, obtaining evaluation of open terms
-- under a valid context.
evalOpen : {ty : Type}(context : Context) ->
           Env context ->
           IMu (openTerm context) ty ->
           Val ty
evalOpen ctxt env tm = eval' (substExpr ctxt (discharge ctxt env) tm)

--********************************
-- Tests
--********************************

-- Test context:
-- V 0 :-> true, V 1 :-> 2, V 2 :-> ( false , 1 )
testContext : Context
testContext = (([] , bool) , nat) , pair bool nat
testEnv : Env testContext
testEnv = ((Void , true ) , su (su ze)) , (false , su ze)

-- V 1
test1 : IMu (openTerm testContext) nat
test1 = con (EZe , ( l (r refl) ) )

testSubst1 : IMu closeTerm' nat
testSubst1 = substExpr testContext
                       (discharge testContext testEnv)
                       test1
-- = 2
testEval1 : Val nat
testEval1 = evalOpen testContext testEnv test1

-- add 1 (V 1)
test2 : IMu (openTerm testContext) nat
test2 = con (ESu (ESu (ESu EZe)) , (con (ESu EZe , su ze) , con ( EZe , l (r refl) )) )

testSubst2 : IMu closeTerm' nat
testSubst2 = substExpr testContext
                       (discharge testContext testEnv)
                        test2

-- = 3
testEval2 : Val nat
testEval2 = evalOpen testContext testEnv test2

-- if (V 0) then (V 1) else 0
test3 : IMu (openTerm testContext) nat
test3 = con (ESu (ESu EZe) , (con (EZe , l (l (r refl))) ,
                             (con (EZe , l (r refl)) ,
                              con (ESu EZe , ze))))

testSubst3 : IMu closeTerm' nat
testSubst3 = substExpr testContext
                       (discharge testContext testEnv)
                       test3

-- = 2
testEval3 : Val nat
testEval3 = evalOpen testContext testEnv test3

-- V 2
test4 : IMu (openTerm testContext) (pair bool nat)
test4 = con (EZe ,  r refl  )

testSubst4 : IMu closeTerm' (pair bool nat)
testSubst4 = substExpr testContext
                       (discharge testContext testEnv)
                       test4
-- = (false , 1)
testEval4 : Val (pair bool nat)
testEval4 = evalOpen testContext testEnv test4

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram