text:
module BTA9 where

----------------------------------------------
-- Preliminaries: Imports and List-utilities
----------------------------------------------

open import Data.Nat hiding  (_<_;_⊔_;_*_;equal)
open import Data.Bool hiding (_∧_;_∨_)
open import Function using (_∘_)
open import Data.List
open import Data.Nat.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty

open import Lib

---------------------------------------
-- Start of the development:
---------------------------------------

-- Intro/Objective:
-------------------
-- The following development defines a (verified) specializer/partial
-- evaluator for a simply typed lambda calculus embedded in Agda using
-- deBruijn indices.

-- The residual language.
-------------------------

-- The residual language is a standard simply typed λ-calculus.  The
-- types are integers,functions,pairs,and sums.
data Type : Set where
  Int : Type
  Fun : Type → Type → Type
    --pair type on the residual type level
  _•_ : Type  → Type  → Type
  --sum type on the residual type level
  _⊎_ : Type → Type → Type

Ctx = List Type

-- The type Exp describes the typed residual expressions. Variables
-- are represented by deBruijn indices that form references into the
-- typing context. The constructors and typing constraints are
-- standard.

-- TODO: citations for ``as usual'' and ``standard''
-- what?
data Exp (Γ : Ctx) : Type → Set where
  EVar : ∀ {τ} → τ ∈ Γ → Exp Γ τ
  EInt : ℕ → Exp Γ Int
  EAdd : Exp Γ Int → Exp Γ Int -> Exp Γ Int
  ELam : ∀ {τ τ'} → Exp (τ ∷ Γ) τ' → Exp Γ (Fun τ τ')
  EApp : ∀ {τ τ'} → Exp Γ (Fun τ τ')  → Exp Γ τ → Exp Γ τ'
  _,_  : ∀ {τ τ'} → Exp Γ τ → Exp Γ τ' → Exp Γ (τ • τ')
  Tl   : ∀ {τ τ'} → Exp Γ τ → Exp Γ (τ ⊎ τ')
  Tr   : ∀ {τ τ'} → Exp Γ τ' → Exp Γ (τ ⊎ τ')
  EFst : ∀ {τ τ'} → Exp Γ (τ • τ') → Exp Γ τ
  ESnd : ∀ {τ τ'} → Exp Γ (τ • τ') → Exp Γ τ'
  ECase : ∀ {τ τ' τ''} → Exp Γ (τ ⊎ τ') → Exp (τ ∷ Γ) τ'' → Exp (τ' ∷ Γ) τ'' → Exp Γ τ''

-- The standard functional semantics of the residual expressions.
-- TODO: citations for ``as usual'' and ``standard''
-- what?
module Exp-Eval where
  -- interpretation of Exp types
  EImp : Type → Set
  EImp Int = ℕ
  EImp (Fun ty ty₁) = EImp ty → EImp ty₁
  EImp (ty • ty₁) = EImp ty * EImp ty₁
  EImp (ty ⊎ ty₁) = EImp ty ⨄ EImp ty₁

  -- Environments containing values for free variables. An environment
  -- is indexed by a typing context that provides the types for the
  -- contained values.
  data Env : Ctx → Set where
    [] : Env []
    _∷_ : ∀ {τ Γ} → EImp τ → Env Γ → Env (τ ∷ Γ)

  -- Lookup a value in the environment, given a reference into the
  -- associated typing context.
  lookupE : ∀ { τ Γ } → τ ∈ Γ → Env Γ → EImp τ
  lookupE hd (x ∷ env) = x
  lookupE (tl v) (x ∷ env) = lookupE v env

  -- Evaluation of residual terms, given a suitably typed environment.
  ev : ∀ {τ Γ} → Exp Γ τ → Env Γ → EImp τ
  ev (EVar x) env = lookupE x env
  ev (EInt x) env = x
  ev (EAdd e e₁) env = ev e env + ev e₁ env
  ev (ELam e) env = λ x → ev e (x ∷ env)
  ev (EApp e e₁) env = ev e env (ev e₁ env)
  ev (e , e₁) env = ev e env , (ev e₁ env)
  ev (Tl e) env = tl (ev e env)
  ev (Tr e) env = tr (ev e env)
  ev (EFst e) env = fst (ev e env)
  ev (ESnd e) env = snd (ev e env)
  ev (ECase e e₁ e₂) env with ev e env
  ev (ECase e e₁ e₂) env | tl c  = (λ x → ev e₁ (x ∷ env)) c
  ev (ECase e e₁ e₂) env | tr c  = (λ x → ev e₂ (x ∷ env)) c

-- The binding-time-annotated language.
---------------------------------------

-- The type of a term determines the term's binding time. The type
-- constructors with an A-prefix denote statically bound integers and
-- functions. Terms with dynamic binding time have a `D' type. The `D'
-- type constructor simply wraps up a residual type.
data AType : Set where
    AInt  : AType
    AFun  : AType → AType → AType
    D     : Type → AType
    --pair type on the annotated type level
    _•_   : AType → AType → AType
    --sum  type on the annotated type level
    _⊎_   : AType → AType → AType

ACtx = List AType

-- The mapping from annotated types to residual types is straightforward.
typeof : AType → Type
typeof AInt = Int
typeof (AFun α₁ α₂) = Fun (typeof α₁) (typeof α₂)
typeof (D x) = x
typeof (α₁ • α₂) = typeof α₁ • typeof α₂
typeof (α₁ ⊎ α₂) = typeof α₁ ⊎ typeof α₂

-- The typed annotated terms: The binding times of variables is
-- determined by the corresponding type-binding in the context. In the
-- other cases, the A- and D-prefixes on term constructors inidicate
-- the corresponding binding times for the resulting terms.

  ------------------------------------------------------------------------------------------------
  -- Now the typed annotated terms are extended to inculde dynamic terms whose subterms are static
  ------------------------------------------------------------------------------------------------
  ---------------
  --Some examples
  ---------------
  --a. first-order static value in a dynamic environment
  -- DAdd (DInt 1) (AAdd (AInt 2) (AInt 3)) where AAdd (AInt 2) (AInt 3) : AExp [] AInt
  -- DAdd (DInt 1) (AApp (ALam (Var hd)) (AInt 5)) where AApp (ALam (Var hd)) (AInt 5) : AExp [] AInt
  --b. higher-order static value in a dynamic environment
  -- DApp (ALam (Var hd)) (DInt 5) where ALam (Var hd) : AExp [] (AFun (D Int) (D Int))
  -- DApp (ALam (ALam (AInt 0))) (DInt 5) where ALam (ALam (AInt 0)) : AExp [] (AFun (AFun (D Int) (D Int)) AInt)
  -- DApp (ALam (ALam (DInt 0))) (DInt 5) where ALam (ALam (DInt 0)) : AExp [] (AFun (AFun AInt (D Int)) (D Int))

  --Clearly these terms are not well-typed and we need to modify [AExp] such that they have the right types which are
  --compatible with the dynamic environment,or we can "lift" their static types to dynamic types so that they can be
  --used as dynamic sub-terms to be filled in the right dynamic environment. This,however,brings new difficulty when
  --we try to partially evaluate term who contains "lifted" subterms.

  ----------------
  --new difficulty
  ----------------
  --Consider the evaluation of the following term
  --DAdd (DInt 1) (Lift (AAdd (AInt 2) (AInt 3))) : AExp [] AInt
  --the expected type after evaluation is,
  --EAdd (EInt 1) ? : Exp [] Int where ? : Exp [] Int
  --and one good candidate for "?" as,
  --EInt (pe (AAdd (AInt 2) (AInt 3)) []) : Exp [] Int
  --where we wrap up the partial evaluation of the static subterm so
  --that it fits with the rest of evaluation.
  --However,we can not always "wrap up" a evaluated higher-order static
  --value so that it has the required residual type,
  --ALam (Var hd) : AExp [] (AFun AInt AInt)
  --the required type of its lifted term as,
  --? : Exp [] (Fun Int Int)
  --which can not be constructed from [λ Γ↝Γ' x → x : []↝Γ' → ℕ → ℕ]
  --for the input of the static function is evaluated to be a natural
  --number which can not be matched with the type of the input of the
  --required residual term. It is then clear that we need to impose
  --restriction upon terms to be lifted.
  -------------------------
  --restriction for lifting
  -------------------------
-------------------------------------------------------------
-- The interpretation of annotated types.
Imp : Ctx → AType → Set
Imp Γ (AInt) = ℕ
Imp Γ (AFun α₁ α₂) = ∀ {Γ'} → Γ ↝ Γ' → (Imp Γ' α₁ → Imp Γ' α₂)
Imp Γ (D σ) = Exp Γ σ
Imp Γ (α₁ • α₂) = (Imp Γ α₁) * (Imp Γ α₂)
Imp Γ (α₁ ⊎ α₂) = (Imp Γ α₁) ⨄ (Imp Γ α₂)

elevate-var : ∀ {Γ Γ'} {τ : Type} → Γ ↝ Γ' → τ ∈ Γ → τ ∈ Γ'
elevate-var ↝-refl x = x
elevate-var (↝-extend Γ↝Γ') x = tl (elevate-var Γ↝Γ' x)

elevate-var2 : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → τ ∈ Γ → τ ∈ Γ''
elevate-var2 (↝↝-base x) x₁ = elevate-var x x₁
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') hd = hd
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') (tl x) = tl (elevate-var2 Γ↝Γ'↝Γ'' x)

elevate : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → Exp Γ τ → Exp Γ'' τ
elevate Γ↝Γ'↝Γ'' (EVar x) = EVar (elevate-var2 Γ↝Γ'↝Γ'' x)
elevate Γ↝Γ'↝Γ'' (EInt x) = EInt x
elevate Γ↝Γ'↝Γ'' (EAdd e e₁) = EAdd (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)
elevate Γ↝Γ'↝Γ'' (ELam e) = ELam (elevate (↝↝-extend Γ↝Γ'↝Γ'') e)
elevate Γ↝Γ'↝Γ'' (EApp e e₁) = EApp (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)
elevate Γ↝Γ'↝Γ'' (e ,  e₁) =  ((elevate Γ↝Γ'↝Γ'' e) , (elevate Γ↝Γ'↝Γ'' e₁))
elevate Γ↝Γ'↝Γ'' (Tl e) = Tl (elevate Γ↝Γ'↝Γ'' e)
elevate Γ↝Γ'↝Γ'' (Tr e) = Tr (elevate Γ↝Γ'↝Γ'' e)
elevate Γ↝Γ'↝Γ'' (EFst e) = EFst (elevate Γ↝Γ'↝Γ'' e)
elevate Γ↝Γ'↝Γ'' (ESnd e) = ESnd (elevate Γ↝Γ'↝Γ'' e)
elevate Γ↝Γ'↝Γ'' (ECase c e₁ e₂) = ECase (elevate Γ↝Γ'↝Γ'' c) (elevate (↝↝-extend Γ↝Γ'↝Γ'') e₁) (elevate (↝↝-extend Γ↝Γ'↝Γ'') e₂)

liftE : ∀ {τ Γ Γ'} → Γ ↝ Γ' → Exp Γ τ → Exp Γ' τ
liftE Γ↝Γ' e = elevate (↝↝-base Γ↝Γ') e
-------------------------------------------------------------
-- --case 1. a first-order static value in a dynamic environment
-- lift1 : AExp [] AInt
-- lift1 = (AInt 0)

-- e1 : Imp [] AInt
-- e1 = 0

-- lifted1 : Exp [] (typeof AInt)
-- lifted1 = EInt e1
-- --case 2. higher-order static function in a dynamic environment
-- --a. a function whose input argument is of static integer
-- --lift2 : AExp [] (AFun AInt AInt)
-- --lift2 = ALam (Var hd)

-- --e2 : Imp [] (AFun AInt AInt)
-- --e2 = λ Γ↝Γ' x → x

-- --lifted2 : Exp [] (typeof (AFun AInt AInt))
-- --lifted2 = ELam {!!}
-- --Note that as explained above it is impossible to construct the right term using [e2]
-- --to fill in the above hole!

-- --b. a function whose input argument is of dynamic integer
-- --b.1. when return type is of dynamic integer
-- lift3 : AExp [] (AFun (D Int) (D Int))
-- lift3 = ALam (Var hd)

-- e3 : Imp [] (AFun (D Int) (D Int))
-- e3 =  λ Γ↝Γ' x → x

-- liftede3 : Exp [] (typeof (AFun (D Int) (D Int)))
-- liftede3 = ELam (e3 (↝-extend ↝-refl) (EVar hd))
-- --b.2. when return type is of static integer
-- lift4 : AExp [] (AFun (D Int) AInt)
-- lift4 = ALam (AInt 0)

-- e4 : Imp [] (AFun (D Int) AInt)
-- e4 = λ Γ↝Γ' x → 0

-- liftede4 : Exp [] (typeof (AFun (D Int) AInt))
-- liftede4 = ELam ( EInt {Int ∷ []} (e4 (↝-extend ↝-refl) (EVar hd)))

-- --c. a function whose input argument is of static function type
-- --c.1. static function type returns a static integer
-- --lift5 : AExp []  (AFun (AFun AInt AInt) AInt)
-- --lift5 = ALam (AApp (Var hd) (AInt 0))

-- --e5 : Imp []  (AFun (AFun AInt AInt) AInt)
-- --e5 = λ Γ↝Γ' x → x ↝-refl 0

-- --liftede5 : Exp [] (typeof ( AFun (AFun AInt AInt) AInt))
-- --liftede5 =  ELam (EInt (e5 (↝-extend {τ = Fun Int Int} ↝-refl) (λ Γ↝Γ' e' → {!!})))
-- --Note that again it is impossible to construct the right residual term

-- --c.2. static function type returns a dynamic integer
-- --c.2.1. the input of the function type is of static integer
-- lift6 : AExp []  (AFun (AFun AInt (D Int)) (D Int))
-- lift6 = ALam (AApp (Var hd) (AInt 0))

-- e6 : Imp []  (AFun (AFun AInt (D Int)) (D Int))
-- e6 = λ Γ↝Γ' x → x ↝-refl 0

-- liftede6 : Exp [] (typeof ( AFun (AFun AInt (D Int)) (D Int)))
-- liftede6 =  ELam ((e6 (↝-extend {τ = Fun Int Int} ↝-refl)
--                 (λ Γ↝Γ' e' → EApp (liftE Γ↝Γ' (EVar {Fun Int Int ∷ []} hd)) (EInt e'))))
-- --c.2.1. the input of the function type is of dynamic integer
-- lift7 : AExp []  (AFun (AFun (D Int) (D Int)) (D Int))
-- lift7 = ALam (AApp (Var hd) (DInt 0))

-- e7 : Imp []  (AFun (AFun (D Int) (D Int)) (D Int))
-- e7 = λ Γ↝Γ' x → x ↝-refl (EInt 0)

-- liftede7 : Exp [] (typeof ( AFun (AFun (D Int) (D Int)) (D Int)))
-- liftede7 =  ELam ((e7 (↝-extend {τ = Fun Int Int} ↝-refl)
--                 (λ Γ↝Γ' e' → EApp (liftE Γ↝Γ' (EVar {Fun Int Int ∷ []} hd)) e')))
-- --c.3. the output of the function type is of higher-order static value
-- --c.3.1 the return value has one static integer as input
-- -- lift8 : AExp []  (AFun (D Int) (AFun AInt (D Int)))
-- -- lift8 = ALam (ALam (Var (tl hd)))

-- -- e8 : Imp []  (AFun (D Int) (AFun AInt (D Int)))
-- -- e8 = λ Γ↝Γ' x Γ'↝Γ'' y → liftE Γ'↝Γ'' x

-- -- liftede8 : Exp [] (typeof ( AFun (D Int) (AFun AInt (D Int))))
-- -- liftede8 =  ELam (ELam (e8 (↝-extend (↝-extend ↝-refl)) (EVar (tl hd)) ↝-refl {!!}))

-- --c.3.2 the return value has one dynamic integer as input
-- lift9 : AExp []  (AFun (D Int) (AFun (D Int) (D Int)))
-- lift9 = ALam (ALam (Var (tl hd)))

-- e9 : Imp []  (AFun (D Int) (AFun (D Int) (D Int)))
-- e9 = λ Γ↝Γ' x Γ'↝Γ'' y → liftE Γ'↝Γ'' x

-- liftede9 : Exp [] (typeof ( AFun (D Int) (AFun (D Int) (D Int))))
-- liftede9 =  ELam (ELam (e9 (↝-extend (↝-extend ↝-refl)) (EVar (tl hd)) ↝-refl (EVar hd)))

-- --d. static pairs and sums in dynamic environment
-- --d.1. identity function with  static sum as its input
-- lift10 : AExp [] (AFun ((D Int) ⊎ (D Int)) ((D Int) ⊎ (D Int)))
-- lift10 = ALam (Var hd)

-- e10 : Imp [] (AFun ((D Int) ⊎ (D Int)) ((D Int) ⊎ (D Int)))
-- e10 =  λ Γ↝Γ' x → x

-- liftede10 : Exp [] (typeof (AFun ((D Int) ⊎ (D Int)) ((D Int) ⊎ (D Int))))
-- liftede10 = ELam {!e10!}

-- --d.1. identity function with  static sum as its input
-- lift11 : AExp [] (AFun ((D Int) • (D Int)) ((D Int) • (D Int)))
-- lift11 = ALam (Var hd)

-- e11 : Imp [] (AFun ((D Int) • (D Int)) ((D Int) • (D Int)))
-- e11 =  λ Γ↝Γ' x → x

-- liftede11 : Exp [] (typeof (AFun ((D Int) • (D Int)) ((D Int) • (D Int))))
-- liftede11 = ELam (fst (e11 (↝-extend ↝-refl) (EFst (EVar hd) , ESnd (EVar hd))) ,
--                     snd (e11 (↝-extend ↝-refl) (EFst (EVar hd) , ESnd (EVar hd))))

--Note that the above two examples in section "d" clearly shows that
--"static functions with inputs of static sum type are not liftable
-- while with inputs of static pair type are liftable ".

---------------------------
--summary on liftable terms
---------------------------
--a. Regarding static first-order static value (static integer) in dynamic environment
--   All terms of static integer type are liftable
--b. Regarding static higher-order static value in dynamic environment
--b.1. given that output value is liftable
--     • when input is of first-order dynamic type,liftable
--     • when input is of higher-order static type and output
--       of that input is of dynamic type,liftable
--b.2. given that input value is liftable
--     • when output is of first-order type,liftable
--     • when output is of higher-order type and inputs
--       of that type are of dynamic type,liftable

-------------------------------------------
--specification of the liftable restriction
-------------------------------------------
mutual
  data Liftable : AType → Set where
    D : ∀ τ → Liftable (D τ)
    AInt : Liftable AInt
    _⊎_ : ∀ {α₁ α₂} → Liftable α₁ → Liftable α₂ → Liftable (α₁ ⊎ α₂)
    _•_ : ∀ {α₁ α₂} → Liftable α₁ → Liftable α₂ → Liftable (α₁ • α₂)
    AFun : ∀ {α₁ α₂} → Liftable⁻ α₁ → Liftable α₂ → Liftable (AFun α₁ α₂)

  data Liftable⁻ : AType → Set where
    D : ∀ τ → Liftable⁻ (D τ)
    _•_ : ∀ {α₁ α₂} → Liftable⁻ α₁ → Liftable⁻ α₂ → Liftable⁻ (α₁ • α₂)
    AFun : ∀ {α₁ α₂} → Liftable α₁ → Liftable⁻ α₂ → Liftable⁻ (AFun α₁ α₂)
----------------------------------------
--[AExp] with liftable terms
----------------------------------------
data AExp (Δ : ACtx) : AType → Set where
  Var : ∀ {α} → α ∈ Δ → AExp Δ α
  AInt : ℕ → AExp Δ AInt
  AAdd : AExp Δ AInt → AExp Δ AInt → AExp Δ AInt
  ALam : ∀ {α₁ α₂}   → AExp (α₁ ∷ Δ) α₂ → AExp Δ (AFun α₁ α₂)
  AApp : ∀ {α₁ α₂}   → AExp Δ (AFun α₂ α₁) → AExp Δ α₂ → AExp Δ α₁
  DInt : ℕ → AExp Δ (D Int)
  DAdd : AExp Δ (D Int) → AExp Δ (D Int) → AExp Δ (D Int)
  DLam : ∀ {σ₁ σ₂}   → AExp ((D σ₁) ∷ Δ) (D σ₂) → AExp Δ (D (Fun σ₁ σ₂))
  DApp : ∀ {α₁ α₂}   → AExp Δ (D (Fun α₂ α₁)) → AExp Δ (D α₂) → AExp Δ (D α₁)
  -- Static pairs and sums
  _,_  : ∀ {α₁ α₂} → AExp Δ α₁ → AExp Δ α₂ → AExp Δ (α₁ • α₂)
  Tl   : ∀ {α₁ α₂} → AExp Δ α₁ → AExp Δ (α₁ ⊎ α₂)
  Tr   : ∀ {α₁ α₂} → AExp Δ α₂ → AExp Δ (α₁ ⊎ α₂)
  Fst  : ∀ {α₁ α₂} → AExp Δ (α₁ • α₂) → AExp Δ α₁
  Snd  : ∀ {α₁ α₂} → AExp Δ (α₁ • α₂) → AExp Δ α₂
  Case : ∀ {α₁ α₂ α₃} → AExp Δ (α₁ ⊎ α₂) → AExp (α₁ ∷ Δ) α₃ → AExp (α₂ ∷ Δ) α₃ → AExp Δ α₃
  -- Dynamic pairs and sums
  _ḋ_  : ∀ {σ₁ σ₂} → AExp Δ (D σ₁) → AExp Δ (D σ₂) → AExp Δ (D (σ₁ • σ₂))
  DTl   : ∀ {σ₁ σ₂} → AExp Δ (D σ₁) → AExp Δ (D (σ₁ ⊎ σ₂))
  DTr   : ∀ {σ₁ σ₂} → AExp Δ (D σ₂) → AExp Δ (D (σ₁ ⊎ σ₂))
  DFst  : ∀ {σ₁ σ₂} → AExp Δ (D (σ₁ • σ₂)) → AExp Δ (D σ₁)
  DSnd  : ∀ {σ₁ σ₂} → AExp Δ (D (σ₁ • σ₂)) → AExp Δ (D σ₂)
  DCase : ∀ {σ₁ σ₂ σ₃} → AExp Δ (D (σ₁ ⊎ σ₂)) → AExp ((D σ₁) ∷ Δ) (D σ₃) → AExp ((D σ₂) ∷ Δ) (D σ₃) → AExp Δ (D σ₃)
  -- Liftable static terms
  ↑     : ∀ {α} → Liftable α → AExp Δ α  → AExp Δ (D (typeof α))

-- The terms of AExp assign a binding time to each subterm. For
-- program specialization, we interpret terms with dynamic binding
-- time as the programs subject to specialization, and their subterms
-- with static binding time as statically known inputs. A partial
-- evaluation function (or specializer) then compiles the program into
-- a residual term for that is specialized for the static inputs. The
-- main complication when defining partial evaluation as a total,
-- primitively recursive function will be the treatment of the De
-- Bruijn variables of non-closed residual expressions.

lift : ∀ {Γ Γ'} α → Γ ↝ Γ' → Imp Γ α → Imp Γ' α
lift AInt p v = v
lift (AFun x x₁) Γ↝Γ' v = λ Γ'↝Γ'' → v (↝-trans Γ↝Γ' Γ'↝Γ'')
lift (D x₁) Γ↝Γ' v = elevate (↝↝-base Γ↝Γ') v
lift (α₁ • α₂) Γ↝Γ' (v₁ , v₂) = (lift α₁ Γ↝Γ' v₁) , (lift α₂ Γ↝Γ' v₂)
lift (α₁ ⊎ α₂) Γ↝Γ' (tl v) = tl (lift α₁ Γ↝Γ' v)
lift (α₁ ⊎ α₂) Γ↝Γ' (tr v) = tr (lift α₂ Γ↝Γ' v)

module SimpleAEnv where
  -- A little weaker, but much simpler
  data AEnv (Γ : Ctx) : ACtx → Set where
    [] : AEnv Γ []
    --cons : ∀ {Δ} (α : AType) → Imp Γ α → AEnv Γ Δ → AEnv Γ (α ∷ Δ)
    cons : ∀ {Δ} {α : AType} → Imp Γ α → AEnv Γ Δ → AEnv Γ (α ∷ Δ)

  lookup : ∀ {α Δ Γ} → AEnv Γ Δ → α ∈ Δ → Imp Γ α
  lookup [] ()
  --lookup {α} (cons .α  x aenv) hd = x
  --lookup {α} (cons .y  x aenv) (tl {.α} {y} id) = lookup aenv id
  lookup {α} (cons x aenv) hd = x
  lookup {α} (cons x aenv) (tl {.α} {y} id) = lookup aenv id

  liftEnv : ∀ {Γ Γ' Δ} → Γ ↝ Γ' → AEnv Γ Δ → AEnv Γ' Δ
  liftEnv Γ↝Γ' [] = []
  --liftEnv Γ↝Γ' (cons α x env) = cons α (lift α Γ↝Γ' x) (liftEnv Γ↝Γ' env)
  liftEnv Γ↝Γ' (cons {α = α} x env) = cons {α = α} (lift α Γ↝Γ' x) (liftEnv Γ↝Γ' env)

  consD : ∀ {Γ Δ} σ → AEnv Γ Δ → AEnv (σ ∷ Γ) (D σ ∷ Δ)
  --consD σ env = (cons (D σ) (EVar hd) (liftEnv (↝-extend {τ = σ} ↝-refl) env))
  consD σ env = (cons {α = D σ} (EVar hd) (liftEnv (↝-extend {τ = σ} ↝-refl) env))

----------------------------------------------
-- Helper for the evaluation of liftable terms
----------------------------------------------
  mutual
    lift' : ∀ {Γ α} → Liftable α → Imp Γ α → (Exp Γ (typeof α))
    lift' (D τ) v = v
    lift' AInt v = EInt v
    lift' (ty ⊎ ty₁) (tl a) = Tl (lift' ty a)
    lift' (ty ⊎ ty₁) (tr b) = Tr (lift' ty₁ b)
    lift' (ty • ty₁) (ffst , ssnd) = lift' ty ffst , lift' ty₁ ssnd
    lift' {Γ} (AFun {α₁} ty₁ ty₂) v = ELam
                                        ((λ x → lift' ty₂ (v (↝-extend {τ = typeof α₁} ↝-refl) x))
                                         (embed ty₁ (EVar {Γ = typeof α₁ ∷ Γ} hd)))

    embed : ∀ {Γ α} → Liftable⁻ α → Exp Γ (typeof α) → (Imp Γ α)
    embed (D τ) e = e
    -- embed (ty ⊎ ty₁) e = {!  (ECase e (EVar hd) ?)!}
    -- embed (ty ⊎ ty₁) (EVar x) = {!!}
    -- embed (ty ⊎ ty₁) (EApp e e₁) = {!!}
    -- embed (ty ⊎ ty₁) (Tl e) = tl (embed ty e)
    -- embed (ty ⊎ ty₁) (Tr e) = tr (embed ty₁ e)
    -- embed (ty ⊎ ty₁) (EFst e) = {!!}
    -- embed (ty ⊎ ty₁) (ESnd e) = {!!}
    -- embed (ty ⊎ ty₁) (ECase e e₁ e₂) = {!!}
    embed (ty • ty₁) e = embed ty (EFst e) , embed ty₁ (ESnd e)
    embed {Γ} (AFun {α} ty₁ ty₂) e =
      λ Γ↝Γ' v₁ → embed ty₂ (EApp (liftE Γ↝Γ' e) (lift' ty₁ v₁))
--------------------
-- Partial Evaluator
--------------------
  pe : ∀ {α Δ Γ} → AExp Δ α → AEnv Γ Δ → Imp Γ α
  pe (Var x) env = lookup env x
  pe (AInt x) env = x
  pe (AAdd e e₁) env = pe e env + pe e₁ env
  pe (ALam {α} e) env = λ Γ↝Γ' → λ y → pe e (cons {α = α} y (liftEnv Γ↝Γ' env))
  pe (AApp e e₁) env = pe e env ↝-refl (pe e₁ env)
  pe (DInt x) env = EInt x
  pe (DAdd e e₁) env = EAdd (pe e env) (pe e₁ env)
  pe (DLam {σ} e) env = ELam (pe e (consD σ env))
  pe (DApp e e₁) env = EApp (pe e env) (pe e₁ env)
  pe {Γ = Γ} (e , e₁) env = pe {Γ = Γ} e env , pe {Γ = Γ} e₁ env
  pe {α = α₁ ⊎ α₂} {Γ = Γ} (Tl e) env = tl (pe {α = α₁} {Γ = Γ} e env)
  pe {α = α₁ ⊎ α₂} {Γ = Γ} (Tr e) env = tr (pe {α = α₂} {Γ = Γ} e env)
  pe {Γ = Γ} (Fst e) env = fst (pe {Γ = Γ} e env)
  pe {Γ = Γ} (Snd e) env = snd (pe {Γ = Γ} e env)
  pe {Γ = Γ} (Case e e₁ e₂) env with pe {Γ = Γ} e env
  pe {Γ = Γ} (Case {α₁ = α} e e₁ e₂) env | tl y = (λ Γ↝Γ' → λ y → pe e₁ (cons {α = α} y (liftEnv Γ↝Γ' env))) ↝-refl y
  pe {Γ = Γ} (Case {α₂ = α} e e₁ e₂) env | tr y = (λ Γ↝Γ' → λ y → pe e₂ (cons {α = α} y (liftEnv Γ↝Γ' env))) ↝-refl y
  pe (e ḋ e₁) env = pe e env , pe e₁ env
  pe (DTl e) env = Tl (pe e env)
  pe (DTr e) env = Tr (pe e env)
  pe (DFst e) env = EFst (pe e env)
  pe (DSnd e) env = ESnd (pe e env)
  pe (DCase {σ₁} {σ₂} e e₁ e₂) env = ECase (pe e env) (pe e₁ (consD σ₁ env)) (pe e₂ (consD σ₂ env))
  pe (↑ x e) env = lift' x (pe e env)

-- Correctness proof

module Correctness where
  open SimpleAEnv
  open Exp-Eval

  -- TODO: rename occurences of stripα to typeof
  stripα = typeof

  stripΔ : ACtx → Ctx
  stripΔ = map stripα

  strip-lookup : ∀ { α Δ} → α ∈ Δ → stripα α ∈ stripΔ Δ
  strip-lookup hd = hd
  strip-lookup (tl x) = tl (strip-lookup x)

  strip : ∀ {α Δ} → AExp Δ α → Exp (stripΔ Δ) (stripα α)
  strip (Var x) = EVar (strip-lookup x)
  strip (AInt x) = EInt x
  strip (AAdd e e₁) = EAdd (strip e) (strip e₁)
  strip (ALam e) = ELam (strip e)
  strip (AApp e e₁)  = EApp (strip e) (strip e₁)
  strip (DInt x)  = EInt x
  strip (DAdd e e₁) = EAdd (strip e) (strip e₁)
  strip (DLam e)  = ELam (strip e)
  strip (DApp e e₁)  = EApp (strip e) (strip e₁)
  strip (e , e₁)  = strip e  , strip e₁
  strip (Tl e)  = Tl (strip e)
  strip (Tr e)  = Tr (strip e)
  strip (Fst e)  = EFst (strip e)
  strip (Snd e)  = ESnd (strip e)
  strip (Case e e₁ e₂)  = ECase (strip e) (strip e₁) (strip e₂)
  strip (e ḋ e₁)  = strip e  , strip e₁
  strip (DTl e)  = Tl (strip e)
  strip (DTr e)  = Tr (strip e)
  strip (DFst e)  = EFst (strip e)
  strip (DSnd e)  = ESnd (strip e)
  strip (DCase e e₁ e₂)  = ECase (strip e) (strip e₁) (strip e₂)
  strip (↑ x e) = strip e

  --liftE : ∀ {τ Γ Γ'} → Γ ↝ Γ' → Exp Γ τ → Exp Γ' τ
  --liftE Γ↝Γ' e = elevate (↝↝-base Γ↝Γ') e

  stripLift : ∀ {α Δ Γ} → stripΔ Δ ↝ Γ → AExp Δ α  → Exp Γ (stripα α)
  stripLift Δ↝Γ = liftE Δ↝Γ ∘ strip

  -- --------------------------------
  -- --"lift-strip" equivalence lemma
  -- --------------------------------
  -- ↑≡↓ : ∀ x e env env' aenv → Equiv-Env env' aenv env  → ev (lift' x (pe e aenv)) env'  ≡ ev (strip e) env
  -- ↑≡↓ x e env env' aenv eqenv = {!!}

  -- We want to show that pe preserves the semantics of the
  -- program. Roughly, Exp-Eval.ev-ing a stripped program is
  -- equivalent to first pe-ing a program and then Exp-Eval.ev-ing the
  -- result. But as the pe-result of a static function ``can do more''
  -- than the (ev ∘ strip)ped function we need somthing more refined.

  module Equiv where
    open import Relation.Binary.PropositionalEquality

    -- Extending a value environment according to an extension of a
    -- type environment
    data _⊢_↝_ {Γ} : ∀ {Γ'} → Γ ↝ Γ' → Env Γ → Env Γ' → Set where
      refl : ∀ env → ↝-refl ⊢ env ↝ env
      extend : ∀ {τ Γ' env env'} →  {Γ↝Γ' : Γ ↝ Γ'} →
                 (v : EImp τ) → (Γ↝Γ' ⊢  env ↝ env')  →
                 ↝-extend {Γ = Γ} {Γ' = Γ'} {τ = τ} Γ↝Γ' ⊢ env ↝ (v ∷ env')

    env↝trans : ∀ {Γ Γ' Γ''} {Γ↝Γ' : Γ ↝ Γ'} {Γ'↝Γ'' : Γ' ↝ Γ''}
                  {env env' env''} →
                  Γ↝Γ' ⊢ env ↝ env' → Γ'↝Γ'' ⊢ env' ↝ env'' →
                  let Γ↝Γ'' = ↝-trans Γ↝Γ' Γ'↝Γ'' in
                  Γ↝Γ'' ⊢ env ↝ env''
    env↝trans {Γ} {.Γ''} {Γ''} {Γ↝Γ'} {.↝-refl} {env} {.env''} {env''} env↝env' (refl .env'') = env↝env'
    env↝trans env↝env' (extend v env'↝env'') = extend v (env↝trans env↝env' env'↝env'')

    -- Equivalent Imp Γ α and EImp τ values (where τ = stripα α). As
    -- (v : Imp Γ α) is not necessarily closed, equivalence is defined for
    -- the closure (Env Γ, ImpΓ α)
    Equiv : ∀ {α Γ} → Env Γ → Imp Γ α → EImp (stripα α) → Set
    Equiv {AInt} env av v = av ≡ v
    Equiv {AFun α₁ α₂} {Γ} env av v = ∀ {Γ' env' Γ↝Γ'} →
                                        (Γ↝Γ' ⊢ env ↝ env') →
                                        {av' : Imp Γ' α₁} →
                                        {v' : EImp (stripα α₁)} →
                                        Equiv {α₁} {Γ'} env' av' v' → Equiv {α₂} env' (av Γ↝Γ' av') (v v')
    Equiv {D x} env av v = ev av env ≡ v
    Equiv {α • α₁} env (ffst , ssnd) (ffst₁ , ssnd₁) = (Equiv {α} env ffst ffst₁) ∧ (Equiv {α₁} env ssnd ssnd₁)
    Equiv {α ⊎ α₁} env (tl a) (tl a₁) = Equiv {α} env a a₁
    --------------------------------------------------------------------
    Equiv {α ⊎ α₁} env (tl a) (tr b) = ⊥  -- Interesting case!
    Equiv {α ⊎ α₁} env (tr b) (tl a) = ⊥  -- Interesting case!
    --------------------------------------------------------------------
    Equiv {α ⊎ α₁} env (tr b) (tr b₁) = Equiv {α₁} env b b₁
   -- Equiv {AInt} env av v = av ≡ v
   -- Equiv {AFun α₁ α₂} {Γ} env av v = -- extensional equality, given -- an extended context
   --     ∀ {Γ' env' Γ↝Γ'} → (Γ↝Γ' ⊢ env ↝ env') →
   --     {av' : Imp Γ' α₁} → {v' : EImp (stripα α₁)} →
   --     Equiv env' av' v' → Equiv env' (av Γ↝Γ' av') (v v')
   -- Equiv {D x} {Γ} env av v = ev av env ≡ v -- actually we mean extensional equality
                                             -- TODO: Define a proper equivalence for EImps

    -- Equivalence of AEnv and Env environments. They need to provide
    -- Equivalent bindings for a context Δ/stripΔ Δ. Again, the
    -- equivalence is defined for a closure (Env Γ', AEnv Γ' Δ).
    data Equiv-Env {Γ' : _} (env' : Env Γ') :
      ∀ {Δ} → let Γ = stripΔ Δ in
      AEnv Γ' Δ → Env Γ → Set where
      [] : Equiv-Env env' [] []
      cons : ∀ {α Δ} → let τ = stripα α
                           Γ = stripΔ Δ in
              {env : Env Γ} → {aenv : AEnv Γ' Δ} →
              Equiv-Env env' aenv env →
              (va : Imp (Γ') α) → (v : EImp τ) →
              Equiv {α} {Γ'} env' va v →
              --Equiv-Env env' (cons α va (aenv)) (v ∷ env)
              Equiv-Env env' (cons {α = α} va (aenv)) (v ∷ env)

  --------------------------------
  --"lift-strip" equivalence lemma
  --------------------------------
    -- ↑≡↓ : ∀ {Γ' Δ α} x e env env' aenv → Equiv-Env {Γ'} env' {Δ} aenv env  → ev (lift' {Γ = Γ'} {α = α} x (pe e aenv)) env'  ≡ ev (strip e) env
    -- ↑≡↓ x e env env' aenv eqenv = {!!}

  -- Now for the proof...
  module Proof where
    open Equiv
    open import Relation.Binary.PropositionalEquality

    -- Extensional equality as an axiom to prove the Equivalence of
    -- function values.  We could (should?) define it locally for
    -- Equiv.
    postulate ext : ∀ {τ₁ τ₂} {f g : EImp τ₁ → EImp τ₂} →
                    (∀ x → f x ≡ g x) → f ≡ g

    -- Ternary helper relation for environment extensions, analogous to _↝_↝_ for contexts
    data _⊢_↝_↝_⊣ : ∀ { Γ Γ' Γ''} → Γ ↝ Γ' ↝ Γ'' → Env Γ → Env Γ' → Env Γ'' → Set where
      refl : ∀ {Γ Γ''} {Γ↝Γ'' : Γ ↝ Γ''} { env env'' } →
             Γ↝Γ'' ⊢ env ↝ env'' →
             ↝↝-base Γ↝Γ'' ⊢ env ↝ [] ↝ env'' ⊣
      extend : ∀ {Γ Γ' Γ'' τ} {Γ↝Γ'↝Γ'' : Γ ↝ Γ' ↝ Γ''} { env env' env'' } →
               Γ↝Γ'↝Γ'' ⊢ env ↝ env' ↝ env'' ⊣ →
               (v : EImp τ) → ↝↝-extend {Γ = Γ} {Γ' = Γ'} {Γ'' = Γ''} {τ = τ} Γ↝Γ'↝Γ'' ⊢ (v ∷ env) ↝ (v ∷ env') ↝ (v ∷ env'') ⊣

    -- the following lemmas are strong versions of the shifting
    -- functions, proving that consistent variable renaming preserves
    -- equivalence (and not just typing).
    lookup-elevate-≡ : ∀ {τ Γ Γ'} {Γ↝Γ' : Γ ↝ Γ'}
                       {env : Env Γ} {env' : Env Γ'} →
                       Γ↝Γ' ⊢ env ↝ env' →
                       (x : τ ∈ Γ) → lookupE x env ≡ lookupE (elevate-var Γ↝Γ' x) env'
    lookup-elevate-≡ {τ} {.Γ'} {Γ'} {.↝-refl} {.env'} {env'} (refl .env') x = refl
    lookup-elevate-≡ (extend v env↝env') x = lookup-elevate-≡ env↝env' x

    lookup-elevate2-≡ : ∀ {τ Γ Γ' Γ''} {Γ↝Γ'↝Γ'' : Γ ↝ Γ' ↝ Γ''}
                       {env : Env Γ} {env' : Env Γ'} {env'' : Env Γ''} →
                       Γ↝Γ'↝Γ'' ⊢ env ↝ env' ↝ env'' ⊣ →
                       (x : τ ∈ Γ) → lookupE x env ≡ lookupE (elevate-var2 Γ↝Γ'↝Γ'' x) env''
    lookup-elevate2-≡ (refl Γ↝Γ') x = lookup-elevate-≡ Γ↝Γ' x
    lookup-elevate2-≡ (extend env↝env'↝env'' v) hd = refl
    lookup-elevate2-≡ (extend env↝env'↝env'' _) (tl x)
      rewrite lookup-elevate2-≡ env↝env'↝env'' x = refl

    lem-elevate-≡ : ∀ {τ Γ Γ' Γ''}
                      {Γ↝Γ'↝Γ'' : Γ ↝ Γ' ↝ Γ''}
                      {env : Env Γ} {env' : Env Γ'} {env'' : Env Γ''} →
                      Γ↝Γ'↝Γ'' ⊢ env ↝ env' ↝ env'' ⊣ →
                      (e : Exp Γ τ) →
                      ev e env ≡ ev (elevate Γ↝Γ'↝Γ'' e) env''
    lem-elevate-≡ env↝env' (EVar x) = lookup-elevate2-≡ env↝env' x
    lem-elevate-≡ env↝env' (EInt x) = refl
    lem-elevate-≡ env↝env' (EAdd e e₁) with lem-elevate-≡ env↝env' e | lem-elevate-≡ env↝env' e₁
    ... | IA1 | IA2 = cong₂ _+_ IA1 IA2
    lem-elevate-≡ {Fun τ₁ τ₂} {Γ↝Γ'↝Γ'' = Γ↝Γ'↝Γ''}
                  {env = env}
                  {env'' = env''}
                  env↝env' (ELam e) = ext {τ₁} {τ₂} lem-elevate-≡-body
       where lem-elevate-≡-body : ∀ x → ev e (x ∷ env) ≡ ev (elevate (↝↝-extend Γ↝Γ'↝Γ'') e) (x ∷ env'')
             lem-elevate-≡-body x = lem-elevate-≡ (extend env↝env' x) e
    lem-elevate-≡ env↝env' (EApp e e₁) with lem-elevate-≡ env↝env' e | lem-elevate-≡ env↝env' e₁
    ... | IA1 | IA2  = cong₂ (λ f₁ x → f₁ x) IA1 IA2
    lem-elevate-≡ env↝env' (e , e₁) with lem-elevate-≡ env↝env' e | lem-elevate-≡ env↝env' e₁
    ... | IA1 | IA2  = cong₂ (λ x y → x , y) IA1 IA2
    lem-elevate-≡ env↝env' (Tl e) with lem-elevate-≡ env↝env' e
    ... | IA  = cong (λ x → tl x) IA
    lem-elevate-≡ env↝env' (Tr e) with lem-elevate-≡ env↝env' e
    ... | IA  = cong (λ x → tr x) IA
    lem-elevate-≡ env↝env' (EFst e) with lem-elevate-≡ env↝env' e
    ... | IA  = cong (λ x → fst x) IA
    lem-elevate-≡ env↝env' (ESnd e) with lem-elevate-≡ env↝env' e
    ... | IA  = cong (λ x → snd x) IA
    lem-elevate-≡ {Γ↝Γ'↝Γ'' = Γ↝Γ'↝Γ''}
                  {env = env}
                  {env'' = env''}
                  env↝env' (ECase e e₁ e₂) with ev e env | ev (elevate Γ↝Γ'↝Γ'' e) env'' | lem-elevate-≡ env↝env' e
    ... | tl c | tl c' | IA rewrite (→tl {x' = c} {y' = c'} (tl c) (tl c') IA refl refl) = lem-elevate-≡-body c'
         where lem-elevate-≡-body : ∀ x → ev e₁ (x ∷ env) ≡ ev (elevate (↝↝-extend Γ↝Γ'↝Γ'') e₁) (x ∷ env'')
               lem-elevate-≡-body x = lem-elevate-≡ (extend env↝env' x) e₁
    ... | tl c | tr c' | ()
    ... | tr c | tl c' | ()
    ... | tr c | tr c' | IA rewrite (→tr {x' = c} {y' = c'} (tr c) (tr c') IA refl refl) = lem-elevate-≡-body c'
         where lem-elevate-≡-body : ∀ x → ev e₂ (x ∷ env) ≡ ev (elevate (↝↝-extend Γ↝Γ'↝Γ'') e₂) (x ∷ env'')
               lem-elevate-≡-body x = lem-elevate-≡ (extend env↝env' x) e₂

    lem-lift-refl-id : ∀ {α Γ} → let τ = stripα α in
                       (env : Env Γ) →
                       (v : EImp τ) (va : Imp Γ α) →
                       Equiv {α} {Γ} env va v →
                       Equiv {α} {Γ} env (lift α ↝-refl va) v
    lem-lift-refl-id {AInt} env v va eq = eq
    lem-lift-refl-id {AFun α α₁} {Γ} env v va eq = body
        where body : ∀ {Γ'} {env' : Env Γ'} {Γ↝Γ' : Γ ↝ Γ'} →
                     Γ↝Γ' ⊢ env ↝ env' →
                     {av' : Imp Γ' α} {v' : EImp (stripα α)} →
                     Equiv {α} {Γ'} env' av' v' → Equiv {α₁} {Γ'} env' (va (↝-trans ↝-refl Γ↝Γ') av') (v v')
              body {Γ↝Γ' = Γ↝Γ'} env↝env' eq' rewrite sym (lem-↝-refl-id Γ↝Γ') = eq env↝env' eq'

    lem-lift-refl-id {D x} env v va eq rewrite sym eq = sym (lem-elevate-≡ (refl (refl env)) va)
    lem-lift-refl-id {α • α₁} env (ffst , ssnd) (ffst₁ , ssnd₁) (∧-intro x x₁) =
                    ∧-intro (lem-lift-refl-id {α} env ffst ffst₁ x)
                             (lem-lift-refl-id {α₁} env ssnd ssnd₁ x₁)
    lem-lift-refl-id {α ⊎ α₁} env (tl a) (tl a₁) eq = lem-lift-refl-id {α}  env a a₁ eq
    lem-lift-refl-id {α ⊎ α₁} env (tl a) (tr b) ()
    lem-lift-refl-id {α ⊎ α₁} env (tr b) (tl a) ()
    lem-lift-refl-id {α ⊎ α₁} env (tr b) (tr b₁) eq = lem-lift-refl-id {α₁} env b b₁ eq

    -- lifting an Imp does not affect equivalence
    lem-lift-equiv : ∀ {α Γ Γ'} → let τ = stripα α in
                     {Γ↝Γ' : Γ ↝ Γ'} →
                     (va : Imp Γ α) (v : EImp τ) →
                     {env : Env Γ} {env' : Env Γ'} →
                     Γ↝Γ' ⊢ env ↝ env' →
                     Equiv {α} {Γ} env va v →
                     Equiv {α} {Γ'} env' (lift α Γ↝Γ' va) v
    lem-lift-equiv {α} va v {.env'} {env'} (refl .env') eq = lem-lift-refl-id {α} env' v va eq
    lem-lift-equiv {AInt} va v (extend v₁ env↝env') eq = eq
    lem-lift-equiv {AFun α α₁} va v (extend v₁ env↝env') eq =
      λ v₁env₁↝env' eq₁ → eq (env↝trans (extend v₁ env↝env') v₁env₁↝env') eq₁
    lem-lift-equiv {D x} va v (extend v₁ env↝env') eq rewrite sym eq = sym (lem-elevate-≡ (refl (extend v₁ env↝env')) va)
    lem-lift-equiv {α • α₁} (ffst , ssnd) (ffst₁ , ssnd₁) (extend v₁ env↝env') (∧-intro x x₁) =
      ∧-intro (lem-lift-equiv {α} ffst ffst₁ (extend v₁ env↝env') x)
               (lem-lift-equiv {α₁} ssnd ssnd₁ (extend v₁ env↝env') x₁)
    lem-lift-equiv {α ⊎ α₁} (tl a) (tl a₁) (extend v₁ env↝env') eq = lem-lift-equiv {α} a a₁ (extend v₁ env↝env') eq
    lem-lift-equiv {α ⊎ α₁} (tl a) (tr b) (extend v₁ env↝env') ()
    lem-lift-equiv {α ⊎ α₁} (tr b) (tl a) (extend v₁ env↝env') ()
    lem-lift-equiv {α ⊎ α₁} (tr b) (tr b₁) (extend v₁ env↝env') eq = lem-lift-equiv {α₁} b b₁ (extend v₁ env↝env') eq

    lem-equiv-lookup : ∀ {α Δ Γ'} → let Γ = stripΔ Δ in
                       { aenv : AEnv Γ' Δ } {env : Env Γ} →
                       (env' : Env Γ') →
                       Equiv-Env env' aenv env →
                       ∀ (x : α ∈ Δ) → Equiv {α} env' (lookup aenv x) (lookupE (strip-lookup x) env)
    lem-equiv-lookup env' [] ()
    lem-equiv-lookup env' (cons  enveq va v eq) hd = eq
    lem-equiv-lookup env' (cons  enveq va v eq) (tl x) = lem-equiv-lookup env' enveq x

    lem-equiv-env-lift-extend :
      ∀ {σ Γ' Δ} (env' : Env Γ') → let Γ = stripΔ Δ in
        {env : Env Γ} {aenv : AEnv Γ' Δ} →
        Equiv-Env env' aenv env → (x : EImp σ) →
        Equiv-Env {σ ∷ Γ'} (x ∷ env') (liftEnv (↝-extend ↝-refl) aenv) env
    lem-equiv-env-lift-extend _ [] x = []
    lem-equiv-env-lift-extend env' (cons {α} eqenv va v x) x₁ =
      cons (lem-equiv-env-lift-extend env' eqenv x₁)
           (lift α (↝-extend ↝-refl) va) v (lem-lift-equiv {α} va v (extend x₁ (refl env')) x)

    lem-equiv-env-lift-lift :
      ∀ {Γ' Γ'' Δ} → let Γ = stripΔ Δ in
        {Γ↝Γ' : Γ' ↝ Γ''}
        {env' : Env Γ'} {env'' : Env Γ''}
        (env'↝env'' : Γ↝Γ' ⊢ env' ↝ env'') →
        {env : Env Γ} {aenv : AEnv Γ' Δ} →
        Equiv-Env env' aenv env →
        Equiv-Env env'' (liftEnv Γ↝Γ' aenv) env
    lem-equiv-env-lift-lift env'↝env'' [] = []
    lem-equiv-env-lift-lift {Γ↝Γ' = Γ↝Γ'} env'↝env'' (cons {α} eqenv va v x)
      with lem-equiv-env-lift-lift env'↝env'' eqenv
    ... | IA = cons IA (lift α Γ↝Γ' va) v (lem-lift-equiv {α} va v env'↝env'' x)

  --------------------------------
  --"lift-correct" equivalence lemma
  --------------------------------
    open import Data.Product
    mutual
      lift-correct : ∀ {Γ α} (lft : Liftable α) (env : Env Γ) (av : Imp Γ α) (v : EImp (typeof α)) →
                     Equiv {α} {Γ} env av v → (Equiv {D (typeof α)} {Γ} env (lift' lft av) v)
      lift-correct (D τ) env av v eq = eq
      lift-correct AInt env av v eq = eq
      lift-correct (lft ⊎ lft₁) env (tl a) (tl a₁) eq with lift-correct lft env a a₁
      ... | IA rewrite IA eq = refl
      lift-correct (lft ⊎ lft₁) env (tr b) (tl a) ()
      lift-correct (lft ⊎ lft₁) env (tl a) (tr b) ()
      lift-correct (lft ⊎ lft₁) env (tr b) (tr b₁) eq with lift-correct lft₁ env b b₁
      ... | IA rewrite IA eq = refl
      lift-correct (lft • lft₁) env (ffst , ssnd) (ffst₁ , ssnd₁) (∧-intro x x₁)
        rewrite lift-correct lft env ffst ffst₁ x | lift-correct lft₁ env ssnd ssnd₁ x₁ = refl
      lift-correct {Γ} {AFun x lft} (AFun y y') env av v eq =
        ext  {typeof x} {typeof lft} (λ x₁ →
               lift-correct y' (x₁ ∷ env)
               (av (↝-extend ↝-refl) (embed y (EVar hd))) (v x₁) (eq (extend x₁ (refl env)) (embed-correct {typeof x ∷ Γ} {x} y (x₁ ∷ env) (EVar hd) x₁ refl)))

      embed-correct : ∀ {Γ α} (lft : Liftable⁻ α) (env : Env Γ) →  (e : Exp Γ (typeof α)) → (v : EImp (typeof α)) →
                      ev e env  ≡ v → Equiv {α} {Γ} env (embed lft e) v
      embed-correct (D τ) env e v eq rewrite eq = refl
      embed-correct (lft • lft₁) env e (fstv , sndv) eq  = ∧-intro (embed-correct lft env (EFst e) fstv (subst (λ x → ffst x ≡ fstv) (sym eq) refl))
                                                                   (embed-correct lft₁ env (ESnd e) sndv
                                                                      (subst (λ x → ssnd x ≡ sndv) (sym eq) refl))
      embed-correct {α = AFun α₁ α₂} (AFun x lft) env e v eq = f
        where

              f : ∀ {Γ' env' Γ↝Γ'} (x₁ : Γ↝Γ' ⊢ env ↝ env') {x₂ : Imp Γ' α₁} {x₃ : EImp (typeof α₁)}
                    (x₄ : Equiv {α₁} {Γ'} env' x₂ x₃) →
                    Equiv  {α₂} {Γ'} env'
                    (embed lft (EApp (elevate (↝↝-base Γ↝Γ') e) (lift' x x₂))) (v x₃)
              f {Γ'} {env'} {Γext} envext {av'} {v'} eq' =
                embed-correct lft env' (EApp (elevate (↝↝-base Γext) e) (lift' x av')) (v v') g
                where g : ev (elevate (↝↝-base Γext) e) env' (ev (lift' x av') env') ≡ v v'
                      g rewrite lift-correct x env' av' v' eq'
                              | sym (cong (λ f → f v') (lem-elevate-≡ (refl envext) e))
                              |  (cong (λ f → f v') eq) = refl
                      --g = {!!}

    ---------------------------------------
    --Correctness proof with liftable terms
    ---------------------------------------

    -- When we partially evaluate somthing under an environment , it
    -- will give equivalent results to a ``complete'' evaluation under
    -- an equivalent environment
    pe-correct : ∀ { α Δ Γ' } → (e : AExp Δ α) →
                 let Γ = stripΔ Δ in
                 {aenv : AEnv Γ' Δ} → {env : Env Γ} →
                 (env' : Env Γ') →
                 Equiv-Env env' aenv env →
                 Equiv {α} {Γ'} env' (pe e aenv) (ev (strip e) env)
    pe-correct (Var x) env' eqenv = lem-equiv-lookup env' eqenv x
    pe-correct (AInt x) env' eqenv = refl
    pe-correct (AAdd e e₁) env' eqenv
      rewrite pe-correct e env' eqenv | pe-correct e₁ env' eqenv = refl
    pe-correct (ALam e) env' eqenv =
     λ {_} {env''} env'↝env'' {av'} {v'} eq →
         let eqenv' : _
             eqenv' = lem-equiv-env-lift-lift env'↝env'' eqenv
             eqenv'' : _
             eqenv'' = cons eqenv' av' v' eq
         in pe-correct e env'' eqenv''
    pe-correct (AApp e e₁) env' eqenv
      with pe-correct e env' eqenv | pe-correct e₁ env' eqenv
    ... | IAe | IAf = IAe (refl env') IAf
    pe-correct (DInt x) env' eqenv = refl
    pe-correct (DAdd e e₁) env' eqenv
      rewrite pe-correct e env' eqenv | pe-correct e₁ env' eqenv = refl
    pe-correct {α = D (Fun σ₁ σ₂)} (DLam e) env' eqenv =
     ext {σ₁} {σ₂}
      (λ x →
         let eqenv₁ : _
             eqenv₁ = lem-equiv-env-lift-extend env' eqenv x
             eqenv₂ : _
             eqenv₂ = cons eqenv₁ (EVar hd) x refl
         in pe-correct e (x ∷ env') eqenv₂)
    pe-correct (DApp e e₁) env' eqenv
      with pe-correct e₁ env' eqenv | pe-correct e env' eqenv
    ... | IA' | IA = cong₂ (λ f x → f x) IA IA'
    pe-correct (e , e₁) env' eqenv = ∧-intro (pe-correct e env' eqenv) (pe-correct e₁ env' eqenv)
    pe-correct (Tl e) env' eqenv = pe-correct e env' eqenv
    pe-correct (Tr e) env' eqenv = pe-correct e env' eqenv
    pe-correct (Fst (e , e₁)) env' eqenv = pe-correct e env' eqenv
    pe-correct (Fst e) {aenv = aenv} {env = env} env' eqenv with pe e aenv | ev (strip e) env | pe-correct e env' eqenv
    ... | e₁ , e₂ | e₁' , e₂' | ∧-intro A B = A
    pe-correct (Snd (e , e₁)) env' eqenv = pe-correct e₁ env' eqenv
    pe-correct (Snd e) {aenv = aenv} {env = env} env' eqenv with pe e aenv | ev (strip e) env | pe-correct e env' eqenv
    ... | e₁ , e₂ | e₁' , e₂' | ∧-intro A B = B
    pe-correct {α} (Case e e₁ e₂) {aenv = aenv} {env = env} env' eqenv with pe e aenv | ev (strip e) env | pe-correct e env' eqenv
    ... | tl c | tl c' | L = pe-correct e₁ {aenv = cons c (liftEnv ↝-refl aenv)}
                               {env = c' ∷ env} env'
                               (cons (lem-equiv-env-lift-lift (refl env') eqenv) c c' L)
    ... | tr c | tr c' | R = pe-correct e₂ {aenv = cons c (liftEnv ↝-refl aenv)}
                               {env = c' ∷ env} env'
                               (cons (lem-equiv-env-lift-lift (refl env') eqenv) c c' R)
    ... | tr c | tl c' | ()
    ... | tl c | tr c' | ()
    pe-correct (e ḋ e₁) env' eqenv with pe-correct e env' eqenv | pe-correct e₁ env' eqenv
    ... | IA | IA' rewrite IA | IA' = refl
    pe-correct (DTl e) env' eqenv with pe-correct e env' eqenv
    ... | IA rewrite IA = refl
    pe-correct (DTr e) env' eqenv with pe-correct e env' eqenv
    ... | IA rewrite IA = refl
    pe-correct (DFst e) env' eqenv with pe-correct e env' eqenv
    ... | IA rewrite IA = refl
    pe-correct (DSnd e) env' eqenv with pe-correct e env' eqenv
    ... | IA rewrite IA = refl
    pe-correct (DCase e e₁ e₂) {aenv = aenv} {env = env} env' eqenv with ev (pe e aenv) env' | ev (strip e) env | pe-correct e env' eqenv
    ... | tl c | tl c' | IA rewrite (→tl {x' = c} {y' = c'} (tl c) (tl c') IA refl refl) =
      pe-correct e₁
        {aenv = cons (EVar hd) (liftEnv (↝-extend ↝-refl) aenv)}
        {env = c' ∷ env} (c' ∷ env') (cons (lem-equiv-env-lift-lift (extend c' (refl env')) eqenv) (EVar hd) c' refl)
    ... | tr c | tr c' | IA rewrite (→tr {x' = c} {y' = c'} (tr c) (tr c') IA refl refl) =
      pe-correct e₂
        {aenv = cons (EVar hd) (liftEnv (↝-extend ↝-refl) aenv)}
        {env = c' ∷ env} (c' ∷ env')
        (cons (lem-equiv-env-lift-lift (extend c' (refl env')) eqenv)
         (EVar hd) c' refl)
    ... | tl c | tr c' | ()
    ... | tr c | tl c' | ()
    pe-correct (↑ x e) {aenv = aenv} {env = env} env' eqenv
      with pe-correct e env' eqenv
    ... | IA = lift-correct x env' (pe e aenv) (ev (strip e) env) IA

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


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

module subgroups where

import 15-groups
open 15-groups public

{- Subsets of groups -}

subset-Group :
  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
subset-Group l G = type-Group G → UU-Prop l

is-set-subset-Group :
  (l : Level) {l1 : Level} (G : Group l1) → is-set (subset-Group l G)
is-set-subset-Group l G =
  is-set-function-type (is-set-UU-Prop l)

{- Defining subgroups -}

contains-unit-subset-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) → UU l2
contains-unit-subset-Group G P = type-Prop (P (unit-Group G))

is-prop-contains-unit-subset-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) →
  is-prop (contains-unit-subset-Group G P)
is-prop-contains-unit-subset-Group G P = is-prop-type-Prop (P (unit-Group G))

closed-under-mul-subset-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) → UU (l1 ⊔ l2)
closed-under-mul-subset-Group G P =
  (x y : type-Group G) →
  type-Prop (P x) → type-Prop (P y) → type-Prop (P (mul-Group G x y))

is-prop-closed-under-mul-subset-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) →
  is-prop (closed-under-mul-subset-Group G P)
is-prop-closed-under-mul-subset-Group G P =
  is-prop-Π (λ x →
    is-prop-Π (λ y →
      is-prop-function-type
        ( is-prop-function-type
          ( is-prop-type-Prop (P (mul-Group G x y))))))

closed-under-inv-subset-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) → UU (l1 ⊔ l2)
closed-under-inv-subset-Group G P =
  (x : type-Group G) → type-Prop (P x) → type-Prop (P (inv-Group G x))

is-prop-closed-under-inv-subset-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) →
  is-prop (closed-under-inv-subset-Group G P)
is-prop-closed-under-inv-subset-Group G P =
  is-prop-Π
    ( λ x → is-prop-function-type (is-prop-type-Prop (P (inv-Group G x))))

is-subgroup-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) → UU (l1 ⊔ l2)
is-subgroup-Group G P =
  ( contains-unit-subset-Group G P) ×
  ( ( closed-under-mul-subset-Group G P) ×
    ( closed-under-inv-subset-Group G P))

is-prop-is-subgroup-Group :
  {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) →
  is-prop (is-subgroup-Group G P)
is-prop-is-subgroup-Group G P =
  is-prop-prod
    ( is-prop-contains-unit-subset-Group G P)
    ( is-prop-prod
      ( is-prop-closed-under-mul-subset-Group G P)
      ( is-prop-closed-under-inv-subset-Group G P))

{- Introducing the type of all subgroups of a group G -}

Subgroup :
  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
Subgroup l G = Σ (type-Group G → UU-Prop l) (is-subgroup-Group G)

subset-Subgroup :
  {l1 l2 : Level} (G : Group l1) →
  ( Subgroup l2 G) → ( subset-Group l2 G)
subset-Subgroup G = pr1

is-emb-subset-Subgroup :
  {l1 l2 : Level} (G : Group l1) → is-emb (subset-Subgroup {l2 = l2} G)
is-emb-subset-Subgroup G = is-emb-pr1-is-subtype (is-prop-is-subgroup-Group G)

type-subset-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  (type-Group G → UU l2)
type-subset-Subgroup G P x = type-Prop (subset-Subgroup G P x)

is-prop-type-subset-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  (x : type-Group G) → is-prop (type-subset-Subgroup G P x)
is-prop-type-subset-Subgroup G P x =
  is-prop-type-Prop (subset-Subgroup G P x)

is-subgroup-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  is-subgroup-Group G (subset-Subgroup G P)
is-subgroup-Subgroup G = pr2

contains-unit-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  contains-unit-subset-Group G (subset-Subgroup G P)
contains-unit-Subgroup G P = pr1 (is-subgroup-Subgroup G P)

closed-under-mul-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  closed-under-mul-subset-Group G (subset-Subgroup G P)
closed-under-mul-Subgroup G P = pr1 (pr2 (is-subgroup-Subgroup G P))

closed-under-inv-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  closed-under-inv-subset-Group G (subset-Subgroup G P)
closed-under-inv-Subgroup G P = pr2 (pr2 (is-subgroup-Subgroup G P))

{- Given a subgroup, we construct a group -}

type-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) → UU (l1 ⊔ l2)
type-group-Subgroup G P =
  Σ (type-Group G) (type-subset-Subgroup G P)

incl-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  type-group-Subgroup G P → type-Group G
incl-group-Subgroup G P = pr1

is-emb-incl-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  is-emb (incl-group-Subgroup G P)
is-emb-incl-group-Subgroup G P =
  is-emb-pr1-is-subtype (is-prop-type-subset-Subgroup G P)

eq-subgroup-eq-group :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  {x y : type-group-Subgroup G P} →
  Id (incl-group-Subgroup G P x) (incl-group-Subgroup G P y) → Id x y
eq-subgroup-eq-group G P {x} {y} =
  inv-is-equiv (is-emb-incl-group-Subgroup G P x y)

set-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) → Subgroup l2 G → UU-Set (l1 ⊔ l2)
set-group-Subgroup G P =
  pair ( type-group-Subgroup G P)
       ( λ x y →
         is-prop-is-equiv
           ( Id (pr1 x) (pr1 y))
           ( ap (incl-group-Subgroup G P))
           ( is-emb-incl-group-Subgroup G P x y)
           ( is-set-type-Group G (pr1 x) (pr1 y)))

unit-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) → type-group-Subgroup G P
unit-group-Subgroup G P =
  pair ( unit-Group G)
       ( contains-unit-Subgroup G P)

mul-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  ( x y : type-group-Subgroup G P) → type-group-Subgroup G P
mul-group-Subgroup G P x y =
  pair ( mul-Group G (pr1 x) (pr1 y))
       ( closed-under-mul-Subgroup G P (pr1 x) (pr1 y) (pr2 x) (pr2 y))

inv-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  type-group-Subgroup G P → type-group-Subgroup G P
inv-group-Subgroup G P x =
  pair (inv-Group G (pr1 x)) (closed-under-inv-Subgroup G P (pr1 x) (pr2 x))

is-associative-mul-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  ( x y z : type-group-Subgroup G P) →
  Id (mul-group-Subgroup G P (mul-group-Subgroup G P x y) z)
     (mul-group-Subgroup G P x (mul-group-Subgroup G P y z))
is-associative-mul-group-Subgroup G P x y z =
  eq-subgroup-eq-group G P (is-associative-mul-Group G (pr1 x) (pr1 y) (pr1 z))

left-unit-law-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  ( x : type-group-Subgroup G P) →
  Id (mul-group-Subgroup G P (unit-group-Subgroup G P) x) x
left-unit-law-group-Subgroup G P x =
  eq-subgroup-eq-group G P (left-unit-law-Group G (pr1 x))

right-unit-law-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  ( x : type-group-Subgroup G P) →
  Id (mul-group-Subgroup G P x (unit-group-Subgroup G P)) x
right-unit-law-group-Subgroup G P x =
  eq-subgroup-eq-group G P (right-unit-law-Group G (pr1 x))

left-inverse-law-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  ( x : type-group-Subgroup G P) →
  Id ( mul-group-Subgroup G P (inv-group-Subgroup G P x) x)
     ( unit-group-Subgroup G P)
left-inverse-law-group-Subgroup G P x =
  eq-subgroup-eq-group G P (left-inverse-law-Group G (pr1 x))

right-inverse-law-group-Subgroup :
  {l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  ( x : type-group-Subgroup G P) →
  Id ( mul-group-Subgroup G P x (inv-group-Subgroup G P x))
     ( unit-group-Subgroup G P)
right-inverse-law-group-Subgroup G P x =
  eq-subgroup-eq-group G P (right-inverse-law-Group G (pr1 x))

group-Subgroup :
  {l1 l2 : Level} (G : Group l1) → Subgroup l2 G → Group (l1 ⊔ l2)
group-Subgroup G P =
  pair
    ( pair
      ( set-group-Subgroup G P)
      ( pair
        ( mul-group-Subgroup G P)
        ( is-associative-mul-group-Subgroup G P)))
    ( pair
      ( pair
        ( unit-group-Subgroup G P)
        ( pair
          ( left-unit-law-group-Subgroup G P)
          ( right-unit-law-group-Subgroup G P)))
      ( pair
        ( inv-group-Subgroup G P)
        ( pair
          ( left-inverse-law-group-Subgroup G P)
          ( right-inverse-law-group-Subgroup G P))))

{- We show that the inclusion from group-Subgroup G P → G is a group
   homomorphism -}

preserves-mul-incl-group-Subgroup :
  { l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  preserves-mul-Group (group-Subgroup G P) G (incl-group-Subgroup G P)
preserves-mul-incl-group-Subgroup G P (pair x p) (pair y q) = refl

hom-group-Subgroup :
  { l1 l2 : Level} (G : Group l1) (P : Subgroup l2 G) →
  hom-Group (group-Subgroup G P) G
hom-group-Subgroup G P =
  pair (incl-group-Subgroup G P) (preserves-mul-incl-group-Subgroup G P)

{- We define another type of subgroups of G as the type of group inclusions -}

emb-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
emb-Group G H = Σ (hom-Group G H) (λ f → is-emb (map-hom-Group G H f))

emb-Group-Slice :
  (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1)
emb-Group-Slice l G =
  Σ ( Group l)
    ( λ H → emb-Group H G)

emb-group-slice-Subgroup :
  { l1 l2 : Level} (G : Group l1) →
  Subgroup l2 G → emb-Group-Slice (l1 ⊔ l2) G
emb-group-slice-Subgroup G P =
  pair
    ( group-Subgroup G P)
    ( pair
      ( hom-group-Subgroup G P)
      ( is-emb-incl-group-Subgroup G P))

ext: agda

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
module Basic.AST where

import Data.Bool as Bool using (not)
open import Data.Bool hiding (not; if_then_else_)
open import Data.Fin using (Fin; suc; zero; #_)
open import Data.Nat
open import Data.Vec
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Utils.Decidable

{-
This module covers the first chapter of the book.

We omitted a couple of proofs that are present in the chapter.

In particular, determinism and totality of the evaluation of expressions
is a trivial consequence of Agda's totality, so there's no need to bother
with it here. Also, the notion of "composionality" as mentioned in book corresponds
simply to structural recursion in Agda.

Also, we skipped the proofs about the evaluation of expression with substitutions
(exercise 1.14) and contexts with substitutions (exercise 1.13), since we make
no use of these in other proofs.
-}

-- Our type universe (it's not a large one).
data Ty : Set where
  bool nat : Ty

{-
Interpretation of types into Agda sets.
Note that we use natural numbers instead of integers, since naturals are
much simpler to handle in formal contexts (also, there's not enough Agda library
support for integers).
-}

⟦_⟧ᵗ : Ty → Set
⟦ nat  ⟧ᵗ = ℕ
⟦ bool ⟧ᵗ = Bool

{-
This is a point where we make a departure from the book. The book defines states as:

State = String → ℕ

This is supposed to be a total funuction, and the book doesn't concern itself with scope
errors or shadowing, but we certainly have to do so in Agda.

So we opt for de Bruijn indices as variables and a finite vector as State. These are as
simple to handle as it can get, and we also get alpha equality of programs for free.

On the flip side, we have much less readable programs.
-}

State : ℕ → Set
State = Vec ℕ

{-
In the book there's a mutual definition of boolean and numeric expressions.
We instead have a single universe-indexed type family. It's more convenient, and
it's also equivalent to the mutual definition (it's a standard Agda/Haskell trick
to encode multiple types data as a single indexed type).
-}
data Exp (n : ℕ) : Ty → Set where
  lit         : ℕ → Exp n nat
  add mul sub : Exp n nat → Exp n nat → Exp n nat
  var         : Fin n → Exp n nat
  tt ff       : Exp n bool
  eq lte lt   : Exp n nat → Exp n nat → Exp n bool
  and         : Exp n bool → Exp n bool → Exp n bool
  not         : Exp n bool → Exp n bool

{-
Statements are parameterized by the size of the State they operate on. Since the
vanilla "While" language has no declarations or other features that might change
the size of the state, we are fine with this. It also allows us to use finite numbers
as de Bruijn indices.
-}

infixr 5 _:=_
infixr 4 _,_
data St (n : ℕ) : Set where
  _:=_          : Fin n → Exp n nat → St n
  skip          : St n
  _,_           : St n → St n → St n
  if_then_else_ : Exp n bool → St n → St n → St n
  while_do_     : Exp n bool → St n → St n

{-
The semantics of expressions follows the book exactly.
-}

⟦_⟧ᵉ : ∀ {n t} → Exp n t → State n → ⟦ t ⟧ᵗ
⟦ lit x   ⟧ᵉ s = x
⟦ add a b ⟧ᵉ s = ⟦ a ⟧ᵉ s + ⟦ b ⟧ᵉ s
⟦ mul a b ⟧ᵉ s = ⟦ a ⟧ᵉ s * ⟦ b ⟧ᵉ s
⟦ sub a b ⟧ᵉ s = ⟦ a ⟧ᵉ s ∸ ⟦ b ⟧ᵉ s
⟦ var x   ⟧ᵉ s = lookup x s
⟦ tt      ⟧ᵉ s = true
⟦ ff      ⟧ᵉ s = false
⟦ eq  a b ⟧ᵉ s = ⌊ ⟦ a ⟧ᵉ s ≡⁇ ⟦ b ⟧ᵉ s ⌋
⟦ lte a b ⟧ᵉ s = ⌊ ⟦ a ⟧ᵉ s ≤⁇ ⟦ b ⟧ᵉ s ⌋
⟦ lt  a b ⟧ᵉ s = ⌊ ⟦ a ⟧ᵉ s <⁇ ⟦ b ⟧ᵉ s ⌋
⟦ and a b ⟧ᵉ s =   ⟦ a ⟧ᵉ s ∧  ⟦ b ⟧ᵉ s
⟦ not e   ⟧ᵉ s = Bool.not (⟦ e ⟧ᵉ s)

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Adjoint.Compose where

-- Composition of Adjoints

open import Level

open import Data.Product using (_,_; _×_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality using (Π; _⟶_)
import Function.Inverse as FI
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

-- be explicit in imports to 'see' where the information comes from
open import Categories.Adjoint using (Adjoint; _⊣_)
open import Categories.Category.Core using (Category)
open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Category.Instance.Setoids
open import Categories.Morphism
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Hom using (Hom[_][-,-])
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ₕ_; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
  renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; unitorˡ; unitorʳ; associator; _≃_)
import Categories.Morphism.Reasoning as MR

private
  variable
    o o′ o″ ℓ ℓ′ ℓ″ e e′ e″ : Level
    C D E : Category o ℓ e

-- Adjoints compose; we can't be sloppy, so associators and unitors must be inserted.
-- Use single letters in pairs, so L & M on the left, and R & S on the right
_∘⊣_ : {L : Functor C D} {R : Functor D C} {M : Functor D E} {S : Functor E D} →
  L ⊣ R → M ⊣ S → (M ∘F L) ⊣ (R ∘F S)
_∘⊣_ {C = C} {D = D} {E = E} {L = L} {R} {M} {S} LR MS = record
  { unit =  ((F⇐G (associator _ S R) ∘ᵥ R ∘ˡ (F⇒G (associator L M S))) ∘ᵥ
            (R ∘ˡ (MSη′ ∘ʳ L)) ∘ᵥ (R ∘ˡ (F⇐G unitorˡ))) ∘ᵥ LRη′
  ; counit = MSε′ ∘ᵥ (((F⇒G (unitorʳ {F = M}) ∘ʳ S) ∘ᵥ ((M ∘ˡ LRε′) ∘ʳ S)) ∘ᵥ
             (F⇒G (associator R L M) ∘ʳ S) ) ∘ᵥ F⇐G (associator S R (M ∘F L) )
  ; zig = λ {A} → zig′ {A}
  ; zag = λ {B} → zag′ {B}
  }
  where
    open NaturalIsomorphism using (F⇒G; F⇐G)
    module LR = Adjoint LR using (zig; zag) renaming (unit to LRη′; counit to LRε′)
    module MS = Adjoint MS using (zig; zag) renaming (unit to MSη′; counit to MSε′)
    module LRη = NaturalTransformation (Adjoint.unit LR) using () renaming (η to ηLR)
    module MSη = NaturalTransformation (Adjoint.unit MS) using (commute) renaming (η to ηMS)
    module LRε = NaturalTransformation (Adjoint.counit LR) using (commute) renaming (η to εLR)
    module MSε = NaturalTransformation (Adjoint.counit MS) using () renaming (η to εMS)
    module C = Category C using (Obj; id; _∘_; _≈_; sym-assoc; ∘-resp-≈ˡ; ∘-resp-≈;
      ∘-resp-≈ʳ; identityˡ; identityʳ; module HomReasoning)
    module D = Category D using (id; _∘_; ∘-resp-≈ˡ; sym-assoc; ∘-resp-≈ʳ; identityˡ;
      module HomReasoning; assoc)
    module E = Category E using (Obj; id; _∘_; _≈_; identityˡ; ∘-resp-≈ʳ; module HomReasoning;
      assoc; sym-assoc; identityʳ)
    module L = Functor L using (homomorphism; F-resp-≈) renaming (F₀ to L₀; F₁ to L₁)
    module M = Functor M using (F-resp-≈; identity; homomorphism) renaming (F₀ to M₀; F₁ to M₁)
    module R = Functor R using (F-resp-≈; identity; homomorphism) renaming (F₀ to R₀; F₁ to R₁)
    module S = Functor S using (F-resp-≈; homomorphism) renaming (F₀ to S₀; F₁ to S₁)
    open LR; open MS; open LRη; open LRε; open MSε; open MSη; open L; open M; open R; open S

    zig′ : {A : C.Obj} → (εMS (M₀ (L₀ A)) E.∘
       ((E.id E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))))) E.∘ E.id) E.∘ E.id)
      E.∘ M₁ (L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
      E.≈ E.id
    -- use "inverted" format here, where rules are out-dented
    zig′ {A} = begin
        (εMS (M₀ (L₀ A)) E.∘ ((E.id E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))))) E.∘ E.id) E.∘ E.id)
        E.∘ M₁ (L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
      ≈⟨  ( refl⟩∘⟨ (E.identityʳ ○ E.identityʳ ○ E.identityˡ)) ⟩∘⟨refl ⟩  -- get rid of those pesky E.id
        (εMS (M₀ (L₀ A)) E.∘ M₁ (εLR (S₀ (M₀ (L₀ A)))))
        E.∘ M₁ (L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
      ≈⟨ E.assoc ○ E.∘-resp-≈ʳ (⟺ M.homomorphism) ⟩
        εMS (M₀ (L₀ A)) E.∘
        M₁ (εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
         -- below: get rid of lots of pesky id. Nasty bit of nested equational reasoning, but nothing deep
      ≈⟨  refl⟩∘⟨ M.F-resp-≈ (D.∘-resp-≈ʳ (L.F-resp-≈
             (C.∘-resp-≈ˡ (C.∘-resp-≈ C.identityˡ (C.∘-resp-≈ʳ R.identity) C.HomReasoning.○
                let _⊚_ = C.HomReasoning._○_ in C.∘-resp-≈ R.identity C.identityʳ ⊚ C.identityˡ)))) ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ ((R₁ (ηMS (L₀ A))) C.∘ ηLR A))
      ≈⟨  refl⟩∘⟨ M.F-resp-≈ (D.∘-resp-≈ʳ L.homomorphism) ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ (R₁ (ηMS (L₀ A))) D.∘ L₁ (ηLR A))
      ≈⟨ refl⟩∘⟨ M.F-resp-≈ D.sym-assoc ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ ((εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ (R₁ (ηMS (L₀ A)))) D.∘ L₁ (ηLR A))
      ≈⟨  refl⟩∘⟨ M.F-resp-≈ (D.∘-resp-≈ˡ (LRε.commute _)) ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ ( (_ D.∘ εLR _) D.∘ L₁ (ηLR A))
      ≈⟨  refl⟩∘⟨ M.homomorphism ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ (_ D.∘ εLR _) E.∘ M₁ (L₁ (ηLR A))
      ≈⟨  refl⟩∘⟨ ( M.homomorphism ⟩∘⟨refl ) ⟩
        εMS (M₀ (L₀ A)) E.∘ (M₁ (ηMS (L₀ A)) E.∘ M₁ (εLR _)) E.∘ M₁ (L₁ (ηLR A))
      ≈⟨ E.∘-resp-≈ʳ E.assoc ○ E.sym-assoc ⟩
        (εMS (M₀ (L₀ A)) E.∘ M₁ (ηMS (L₀ A))) E.∘ (M₁ (εLR _) E.∘ M₁ (L₁ (ηLR A)))
      ≈⟨ MS.zig ⟩∘⟨refl ⟩
        E.id E.∘ (M₁ (εLR _) E.∘ M₁ (L₁ (ηLR A)))
      ≈⟨ E.identityˡ ⟩
        M₁ (εLR _) E.∘ M₁ (L₁ (ηLR A))
      ≈˘⟨ M.homomorphism ⟩
        M₁ (εLR _ D.∘ L₁ (ηLR A))
      ≈⟨ M.F-resp-≈ LR.zig ○ M.identity ⟩
        E.id ∎
      where open E.HomReasoning

    zag′ : {B : E.Obj} → R₁ (S₁ (εMS B E.∘ ((E.id E.∘ M₁ (εLR (S₀ B))) E.∘ E.id) E.∘ E.id))
      C.∘ ((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B)))) C.∘ R₁ D.id) C.∘
      ηLR (R₀ (S₀ B)) C.≈ C.id
    zag′ {B} =
      let _⊚_ = E.HomReasoning._○_ in
      begin
         R₁ (S₁ (εMS B E.∘ ((E.id E.∘ M₁ (εLR (S₀ B))) E.∘ E.id) E.∘ E.id))
          C.∘ ((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B)))) C.∘ R₁ D.id) C.∘
          ηLR (R₀ (S₀ B)) -- get rid of all those id
      ≈⟨ R.F-resp-≈ (S.F-resp-≈ (E.∘-resp-≈ʳ (E.identityʳ ⊚ (E.identityʳ ⊚ E.identityˡ)))) ⟩∘⟨
         C.∘-resp-≈ˡ (C.∘-resp-≈ C.identityˡ (C.∘-resp-≈ʳ R.identity) ○
          C.∘-resp-≈ R.identity C.identityʳ ○ C.identityˡ) ⟩
         R₁ (S₁ (εMS B E.∘ M₁ (εLR (S₀ B)))) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ C.sym-assoc ⟩
         (R₁ (S₁ (εMS B E.∘ M₁ (εLR (S₀ B)))) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B))))) C.∘ ηLR (R₀ (S₀ B))
      ≈˘⟨  R.homomorphism ⟩∘⟨refl ⟩
         R₁ (S₁ (εMS B E.∘ M₁ (εLR (S₀ B))) D.∘ ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ (D.∘-resp-≈ˡ S.homomorphism) ⟩∘⟨refl ⟩
        R₁ ((S₁ (εMS B) D.∘ (S₁ (M₁ (εLR (S₀ B))))) D.∘ ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ D.assoc ⟩∘⟨refl ⟩
        R₁ (S₁ (εMS B) D.∘ S₁ (M₁ (εLR (S₀ B))) D.∘ ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ (D.∘-resp-≈ʳ (D.HomReasoning.⟺ (MSη.commute (εLR (S₀ B))))) ⟩∘⟨refl ⟩
         R₁ (S₁ (εMS B) D.∘ ηMS (S₀ B) D.∘ εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ D.sym-assoc ⟩∘⟨refl ⟩
         R₁ ((S₁ (εMS B) D.∘ ηMS (S₀ B)) D.∘ εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ (D.∘-resp-≈ˡ MS.zag) ⟩∘⟨refl ⟩
         R₁ (D.id D.∘ εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ C.∘-resp-≈ˡ (R.F-resp-≈ D.identityˡ) ⟩
         R₁ (εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ LR.zag ⟩
         C.id ∎
      where open C.HomReasoning

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module #6 where

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

{-
Exercise 1.6. Show that if we define A × B :≡ ∏(x:2) rec2(U, A, B, x), then we can give a
definition of indA×B for which the definitional equalities stated in §1.5 hold propositionally (i.e. using equality
types). (This requires the function extensionality axiom, which is introduced in §2.9.)
-}

rec₂ : ∀{c}{C : Set c} → C → C → Bool → C
rec₂ c₀ c₁ true = c₁
rec₂ c₀ c₁ false = c₀

ind₂ : ∀{c}(C : Bool → Set c) → C false → C true → (x : Bool) → C x
ind₂ C c₀ c₁ true = c₁
ind₂ C c₀ c₁ false = c₀

_×_ : ∀ {i} → Set i → Set i → Set i
A × B = (b : Bool) → if b then A else B

module ProductTwo {a}{A B : Set a} where

  _,_ : A → B → A × B
  _,_ x y true = x
  _,_ x y false = y

  proj₁ : A × B → A
  proj₁ x = x true

  proj₂ : A × B → B
  proj₂ x = x false

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

  indₓ₂ : ∀{c}{C : A × B -> Set c} → (f : (x : A)(y : B) → C (x , y)) → (x : A × B) → C (proj₁ x , proj₂ x)
  indₓ₂ f x = f (proj₁ x) (proj₂ x)

  indₓ₂-β : ∀{c}{C : A × B -> Set c} → (f : (x : A)(y : B) → C (x , y)) → (x : A × B) → indₓ₂ {C = C} f x ≡ f (proj₁ x) (proj₂ x)
  indₓ₂-β f x = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
{-# OPTIONS --without-K #-}
module sets.finite.infinite where

open import sum
open import equality.core
open import function.isomorphism.core
open import function.isomorphism.utils
open import sets.nat
open import sets.empty
open import sets.unit
open import sets.fin.core
open import sets.fin.properties
open import sets.fin.universe
open import sets.finite.core

ℕ-not-finite : ¬ (IsFinite ℕ)
ℕ-not-finite (n , fℕ) = suc-fixpoint (sym (Fin-inj iso-suc))
  where
    iso-suc : Fin n ≅ Fin (suc n)
    iso-suc = sym≅ fℕ
           ·≅ isoℕ
           ·≅ ⊎-ap-iso refl≅ fℕ
           ·≅ sym≅ fin-struct-iso

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use `Algebra` or `Algebra.Core`
-- instead.
------------------------------------------------------------------------

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

module Algebra.FunctionProperties.Core where

{-# WARNING_ON_IMPORT
"Algebra.FunctionProperties.Core was deprecated in v1.2.
Use Algebra.Core instead."
#-}

open import Algebra.Core public


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

   Copyright (c) 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.Base.Types
import      LibraBFT.Impl.Consensus.RecoveryData                 as RecoveryData
import      LibraBFT.Impl.Consensus.TestUtils.MockSharedStorage  as MockSharedStorage
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Storage.DiemDB.LedgerStore.LedgerStore as LedgerStore
import      LibraBFT.Impl.Types.LedgerInfo                       as LedgerInfo
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
import      Util.KVMap                                           as Map
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                          using (String)

module LibraBFT.Impl.Consensus.TestUtils.MockStorage where

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

postulate -- TODO-2: sortOn
  sortOn : (Block → Round) → List Block → List Block

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

start : MockStorage → Either ErrLog RecoveryData

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

newWithLedgerInfo : MockSharedStorage → LedgerInfo → Either ErrLog MockStorage
newWithLedgerInfo sharedStorage ledgerInfo = do
  li      ← if ledgerInfo ^∙ liEndsEpoch
            then pure ledgerInfo
            else LedgerInfo.mockGenesis (just (sharedStorage ^∙ mssValidatorSet))
  let lis = LedgerInfoWithSignatures∙new li Map.empty
  pure $ MockStorage∙new
      (sharedStorage & mssLis %~ Map.insert (lis ^∙ liwsLedgerInfo ∙ liVersion) lis)
      li
      (DiemDB∙new LedgerStore.new)

getLedgerRecoveryData : MockStorage → LedgerRecoveryData
getLedgerRecoveryData self =
  LedgerRecoveryData∙new (self ^∙ msStorageLedger)

tryStart : MockStorage → Either ErrLog RecoveryData
tryStart self =
  withErrCtx' (here' []) $
  RecoveryData.new
    (self ^∙ msSharedStorage ∙ mssLastVote)
    (getLedgerRecoveryData self)
    (sortOn (_^∙ bRound) (Map.elems (self ^∙ msSharedStorage ∙ mssBlock)))
    RootMetadata∙new
    (Map.elems (self ^∙ msSharedStorage ∙ mssQc))
    (self ^∙ msSharedStorage ∙ mssHighestTimeoutCertificate)
 where
  here' : List String → List String
  here' t = "MockStorage" ∷ "tryStart" ∷ t

startForTesting : ValidatorSet → Maybe LedgerInfoWithSignatures
                → Either ErrLog (RecoveryData × PersistentLivenessStorage)
startForTesting validatorSet obmMLIWS = do
  (sharedStorage , genesisLi) ←
    case obmMLIWS of λ where
        nothing     → do
          g ← LedgerInfo.mockGenesis (just validatorSet)
          pure (MockSharedStorage.new validatorSet            , g)
        (just liws) →
          pure (MockSharedStorage.newObmWithLIWS validatorSet liws , liws ^∙ liwsLedgerInfo)
  storage ← newWithLedgerInfo sharedStorage genesisLi
  ss      ← withErrCtx' (here' []) (start storage)
  pure (ss , storage)
 where
  here' : List String → List String
  here' t = "MockStorage" ∷ "startForTesting" ∷ t

abstract
  startForTesting-ed-abs : ValidatorSet → Maybe LedgerInfoWithSignatures
                         → EitherD ErrLog (RecoveryData × PersistentLivenessStorage)
  startForTesting-ed-abs vs mliws = fromEither $ startForTesting vs mliws

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

saveTreeE
  : List Block → List QuorumCert → MockStorage
  → Either ErrLog MockStorage

saveTreeM
  : List Block → List QuorumCert → MockStorage
  → LBFT (Either ErrLog MockStorage)
saveTreeM bs qcs db = do
  logInfo fakeInfo -- [ "MockStorage", "saveTreeM", show (length bs), show (length qcs) ]
  pure (saveTreeE bs qcs db)

saveTreeE bs qcs db =
  pure (db & msSharedStorage ∙ mssBlock %~ insertBs
           & msSharedStorage ∙ mssQc    %~ insertQCs)
 where
  insertBs : Map.KVMap HashValue Block → Map.KVMap HashValue Block
  insertBs  m = foldl' (λ acc b  → Map.insert (b ^∙ bId)                      b  acc) m bs

  insertQCs : Map.KVMap HashValue QuorumCert → Map.KVMap HashValue QuorumCert
  insertQCs m = foldl' (λ acc qc → Map.insert (qc ^∙ qcCertifiedBlock ∙ biId) qc acc) m qcs

pruneTreeM
  : List HashValue → MockStorage
  → LBFT (Either ErrLog MockStorage)
pruneTreeM ids db = do
  logInfo fakeInfo -- ["MockStorage", "pruneTreeM", show (fmap lsHV ids)]
  ok (db & msSharedStorage ∙ mssBlock %~ deleteBs
         & msSharedStorage ∙ mssQc    %~ deleteQCs)
  -- TODO : verifyConsistency
 where
  deleteBs : Map.KVMap HashValue Block → Map.KVMap HashValue Block
  deleteBs  m = foldl' (flip Map.delete) m ids

  deleteQCs : Map.KVMap HashValue QuorumCert → Map.KVMap HashValue QuorumCert
  deleteQCs m = foldl' (flip Map.delete) m ids

saveStateM
  : Vote → MockStorage
  → LBFT (Either ErrLog MockStorage)
saveStateM v db = do
  logInfo fakeInfo -- ["MockStorage", "saveStateM", lsV v]
  ok (db & msSharedStorage ∙ mssLastVote ?~ v)

start  = tryStart

saveHighestTimeoutCertificateM
  : TimeoutCertificate → MockStorage
  → LBFT (Either ErrLog MockStorage)
saveHighestTimeoutCertificateM tc db = do
  logInfo fakeInfo -- ["MockStorage", "saveHighestTimeoutCertificateM", lsTC tc]
  ok (db & msSharedStorage ∙ mssHighestTimeoutCertificate ?~ tc)

retrieveEpochChangeProofED
  : Version → MockStorage
  → EitherD ErrLog EpochChangeProof
retrieveEpochChangeProofED v db = case Map.lookup v (db ^∙ msSharedStorage ∙ mssLis) of λ where
  nothing    → LeftD fakeErr -- ["MockStorage", "retrieveEpochChangeProofE", "not found", show v])
  (just lis) → pure (EpochChangeProof∙new (lis ∷ []) false)

abstract
  retrieveEpochChangeProofED-abs = retrieveEpochChangeProofED
  retrieveEpochChangeProofED-abs-≡ : retrieveEpochChangeProofED-abs ≡ retrieveEpochChangeProofED
  retrieveEpochChangeProofED-abs-≡ = refl


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

module Generics.Constructions.Injective where

open import Generics.Prelude hiding (lookup; pi; curry; icong)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc
open import Relation.Binary.PropositionalEquality.Properties

PathOver : ∀ {i j} {A : Set i} (B : A → Set j) {x y : A}
            (p : x ≡ y)
            (u : B x) (v : B y)
         → Set j
PathOver B refl u v = u ≡ v

module _
  {P I ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {ℓ} A)
  {p}
  where

  open HasDesc H

  private
    variable
      V       : ExTele P
      i i₁ i₂ : ⟦ I ⟧tel p
      v v₁ v₂ : ⟦ V ⟧tel p
      c ℓ′    : Level

  countArgs : ConDesc P V I → ℕ
  countArgs (var _) = zero
  countArgs (π _ _ C) = suc (countArgs C)
  countArgs (_ ⊗ B) = suc (countArgs B)

  -- | Compute level of projection
  levelProj : (C : ConDesc P V I) (m : Fin (countArgs C)) → Level
  levelProj (π {ℓ′} ai S C) zero = ℓ′
  levelProj (π ai S C) (suc m) = levelProj C m
  levelProj (A ⊗ B) zero = levelIndArg A ℓ
  levelProj (A ⊗ B) (suc m) = levelProj B m

  -- TODO (for Lucas of tomorrow):
  -- ⟦ v₁ ≡ v₂ ⟧

  -- private
  --   proj₂-id : ∀ {a} {A : Set a} {ℓB : A → Level} {B : ∀ x → Set (ℓB x)}
  --              {k : A} {x y : B k}
  --            → _≡ω_ {A = Σℓω A B} (k , x) (k , y)
  --            → x ≡ y
  --   proj₂-id refl = refl

  --   unconstrr : ∀ {k i} {x : ⟦ _ ⟧Con A′ (p , tt , i)}
  --                       {y : ⟦ _ ⟧Con A′ (p , tt , i)}
  --             → constr (k , x) ≡ constr (k , y)
  --             → x ≡ y
  --   unconstrr p = proj₂-id (constr-injective p)

  -- unconstr : ∀ {i₁ i₂} (ieq : i₁ ≡ i₂) {k}
  --            {x₁ : ⟦ lookupCon D k ⟧Con A′ (p , tt , i₁)}
  --            {x₂ : ⟦ lookupCon D k ⟧Con A′ (p , tt , i₂)}
  --          → subst (A′ ∘ (p ,_)) ieq (constr (k , x₁)) ≡ constr (k , x₂)
  --          → subst (λ i → ⟦ lookupCon D k ⟧Con A′ (p , tt , i)) ieq x₁ ≡ x₂
  -- unconstr refl p = proj₂-id (constr-injective p)

  -------------------------------
  -- Types of injectivity proofs

  levelInjective : (C : ConDesc P V I) → Level → Level
  levelInjective (var x) c = levelOfTel I ⊔ ℓ ⊔ c
  levelInjective (π {ℓ′} ai S C) c = ℓ′ ⊔ levelInjective C c
  levelInjective (A ⊗ B) c = levelIndArg A ℓ ⊔ levelInjective B c

  mutual
    InjectiveCon
      : (C : ConDesc P V I) (m : Fin (countArgs C))
        (mk₁ : ∀ {i₁} → ⟦ C ⟧Con A′ (p , v₁ , i₁) → A′ (p , i₁))
        (mk₂ : ∀ {i₂} → ⟦ C ⟧Con A′ (p , v₂ , i₂) → A′ (p , i₂))
      → Set (levelInjective C (levelProj C m))
    InjectiveCon {V} {v₁} {v₂} (π {ℓ′} (n , ai) S C) (suc m) mk₁ mk₂
      = {s₁ : < relevance ai > S (_ , v₁)}
        {s₂ : < relevance ai > S (_ , v₂)}
      → InjectiveCon C m (λ x → mk₁ (s₁ , x)) (λ x → mk₂ (s₂ , x))
    InjectiveCon {V} {v₁} {v₂} (A ⊗ B) (suc m) mk₁ mk₂
      = {f₁ : ⟦ A ⟧IndArg A′ (_ , v₁)}
        {f₂ : ⟦ A ⟧IndArg A′ (_ , v₂)}
      → InjectiveCon B m (λ x → mk₁ (f₁ , x)) (λ x → mk₂ (f₂ , x))
    InjectiveCon (A ⊗ B) zero mk₁ mk₂ = {!!}
    InjectiveCon (π ai S C) zero mk₁ mk₂ = {!!}

    InjectiveConLift
      : ∀ {V V′ : ExTele P} (C : ConDesc P V′ I) {c}
        {v₁  v₂  : ⟦ V  ⟧tel p}
        {v′₁ v′₂ : ⟦ V′ ⟧tel p}
        {X : ⟦ P , V ⟧xtel → Set c}
        (mk₁ : ∀ {i₁} → ⟦ C ⟧Con A′ (p , v′₁ , i₁) → A′ (p , i₁))
        (mk₂ : ∀ {i₂} → ⟦ C ⟧Con A′ (p , v′₂ , i₂) → A′ (p , i₂))
        (x₁ : X (p , v₁))
        (x₂ : X (p , v₂))
        (v≡v : v₁ ≡ v₂)
      → Set (levelInjective C c)
    InjectiveConLift (var f) {v′₁ = v′₁} {v′₂} {X} mk₁ mk₂ x₁ x₂ v≡v
      = (ieq : f (p , v′₁) ≡ f (p , v′₂))
        (ceq : subst (A′ ∘ (p ,_)) ieq (mk₁ refl) ≡ mk₂ refl)
      → subst (X ∘ (p ,_)) v≡v x₁ ≡ x₂
    InjectiveConLift (π (n , ai) S C) {X = X} mk₁ mk₂ x₁ x₂ v≡v
      = {s₁ : < relevance ai > S (p , _)}
        {s₂ : < relevance ai > S (p , _)}
      → InjectiveConLift C {X = X} (λ x → mk₁ (s₁ , x)) (λ x → mk₂ (s₂ , x)) x₁ x₂ v≡v
    InjectiveConLift (A ⊗ B) {v′₁ = v′₁} {v′₂} {X} mk₁ mk₂ x₁ x₂ v≡v
      = {f₁ : ⟦ A ⟧IndArg A′ (_ , v′₁)}
        {f₂ : ⟦ A ⟧IndArg A′ (_ , v′₂)}
      → InjectiveConLift B {X = X} (λ x → mk₁ (f₁ , x)) (λ x → mk₂ (f₂ , x)) x₁ x₂ v≡v

    -- first, we gather all arguments for left and right A′ values

    -- InjectiveCon C′ m mk (π (n , ai) S C) mk₁ mk₂
    --   = {s₁ : < relevance ai > S _}
    --     {s₂ : < relevance ai > S _}
    --   → InjectiveCon C′ m mk C (λ x → mk₁ (s₁ , x)) λ x → mk₂ (s₂ , x)
    -- InjectiveCon C′ m mk (A ⊗ B) mk₁ mk₂
    --   = {f₁ : ⟦ A ⟧IndArg A′ _}
    --     {f₂ : ⟦ A ⟧IndArg A′ _}
    --   → InjectiveCon C′ m mk B (λ x → mk₁ (f₁ , x)) λ x → mk₂ (f₂ , x)

    -- -- we now have all arguments to prouce two values of A′
    -- -- for the same kth constructor
    -- -- it's time to find the type of the proof

    -- -- base case: projecting on first arg, no lifting necessary
    -- InjectiveCon {V} {v₁} {v₂} (π ai S C) zero mk (var f) mk₁ mk₂
    --   = (ieq : f (p , v₁) ≡ f (p , v₂))
    --   → subst (A′ ∘ (p ,_)) ieq (mk (mk₁ refl)) ≡ mk (mk₂ refl)
    --   → proj₁ (mk₁ refl) ≡ proj₁ (mk₂ refl)
    -- InjectiveCon {V} {v₁} {v₂} (A ⊗ B) zero mk (var f) mk₁ mk₂
    --   = (ieq : f (p , v₁) ≡ f (p , v₂))
    --   → subst (A′ ∘ (p ,_)) ieq (mk (mk₁ refl)) ≡ mk (mk₂ refl)
    --   → proj₁ (mk₁ refl) ≡ proj₁ (mk₂ refl)

    -- otherwise, we have to lift a few things
    -- InjectiveCon {V} {v₁} {v₂} (π ai S C) (suc m) mk (var f) mk₁ mk₂
    --   = (ieq : f (p , v₁) ≡ f (p , v₂))
    --   → subst (A′ ∘ (p ,_)) ieq (mk (mk₁ refl)) ≡ mk (mk₂ refl)
    --   → InjectiveConLift C m {!!} {!!} {!!} {!!}
    -- InjectiveCon {V} {v₁} {v₂} (A ⊗ B) (suc m) mk (var f) mk₁ mk₂
    --   = (ieq : f (p , v₁) ≡ f (p , v₂))
    --   → subst (A′ ∘ (p ,_)) ieq (mk (mk₁ refl)) ≡ mk (mk₂ refl)
    --   → {!!}

  -- Injective : ∀ k (let C = lookupCon D k) (m : Fin (countArgs C))
  --           → Set (levelInjective C (levelProj C m))
  -- Injective k m = InjectiveCon _ m (λ x → constr (k , x)) _ id id

{-

  deriveInjective : ∀ k m → Injective k m
  deriveInjective k m = injCon (lookupCon D k) m (lookupCon D k)
    where
      injCon
        : (C′  : ConDesc P ε I) (m : Fin (countArgs C′))
          {mk  : ∀ {i} → ⟦ C′ ⟧Con A′ (p , tt , i) → A′ (p , i)}
          (C   : ConDesc P V I)
          {mk₁ : ∀ {i₁} → ⟦ C ⟧Con A′ (p , v₁ , i₁) → ⟦ C′ ⟧Con A′ (p , tt , i₁)}
          {mk₂ : ∀ {i₂} → ⟦ C ⟧Con A′ (p , v₂ , i₂) → ⟦ C′ ⟧Con A′ (p , tt , i₂)}
        → InjectiveCon C′ m mk C mk₁ mk₂

      -- we proceed until the end of the constructor
      injCon C′ m (π ai S C) = injCon C′ m C
      injCon C′ m (A ⊗ B)    = injCon C′ m B

      -- at the end, base case when projecting on fist arg
      injCon (π ai S C) zero (var x) ieq xeq = {!!}
      injCon (A ⊗ B)    zero (var x) ieq xeq = {!!}

      -- else, LIFT
      injCon (π ai S C′) (suc m) (var x) = {!!}
      injCon (C′ ⊗ C′₁) (suc m) (var x) = {!!}
{-

  deriveInjective′ : ∀ k m
                    (ieq : i₁ ≡ i₂)
                    {x₁ : ⟦ _ ⟧Con A′ (p , tt , i₁)}
                    {x₂ : ⟦ _ ⟧Con A′ (p , tt , i₂)}
                   → subst (λ i → ⟦ _ ⟧Con A′ (p , tt , i)) ieq x₁ ≡ x₂
                   → {!!}
  deriveInjective′ = {!!}

-}

-}

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


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

module Data.Nat.Properties where

open import Data.Nat.Base
open import Agda.Builtin.Nat using () renaming (_<_ to _<ᴮ_; _==_ to _≡ᴮ_) public
open import Prelude
open import Cubical.Data.Nat using (caseNat; znots; snotz; injSuc) public

pred : ℕ → ℕ
pred (suc n) = n
pred zero = zero

correct-== : ∀ n m → Reflects (n ≡ m) (n ≡ᴮ m)
correct-== zero zero = ofʸ refl
correct-== zero (suc m) = ofⁿ znots
correct-== (suc n) zero = ofⁿ snotz
correct-== (suc n) (suc m) =
  map-reflects (cong suc) (λ contra prf  → contra (cong pred prf)) (correct-== n m)

discreteℕ : Discrete ℕ
discreteℕ n m .does = n ≡ᴮ m
discreteℕ n m .why  = correct-== n m

isSetℕ : isSet ℕ
isSetℕ = Discrete→isSet discreteℕ

+-suc : ∀ x y → x + suc y ≡ suc (x + y)
+-suc zero y = refl
+-suc (suc x) y = cong suc (+-suc x y)

+-idʳ : ∀ x → x + 0 ≡ x
+-idʳ zero     = refl
+-idʳ (suc x)  = cong suc (+-idʳ x)

+-comm : ∀ x y → x + y ≡ y + x
+-comm x zero = +-idʳ x
+-comm x (suc y) = +-suc x y ; cong suc (+-comm x y)

infix 4 _<_
_<_ : ℕ → ℕ → Type₀
n < m = T (n <ᴮ m)

_≤ᴮ_ : ℕ → ℕ → Bool
zero  ≤ᴮ m = true
suc n ≤ᴮ m = n <ᴮ m

+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
+-assoc zero y z = refl
+-assoc (suc x) y z = cong suc (+-assoc x y z)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

   Copyright (c) 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.Base.PKCS
open import LibraBFT.Base.Types
import      LibraBFT.Yasm.Base   as LYB
import      LibraBFT.Yasm.System as LYS

-- This module provides a single import for all Yasm modules

module LibraBFT.Yasm.Yasm
   (ℓ-PeerState : Level)
   (ℓ-VSFP      : Level)
   (parms       : LYB.SystemParameters ℓ-PeerState)
   (ValidSenderForPK        : LYS.ValidSenderForPK-type        ℓ-PeerState ℓ-VSFP parms)
   (ValidSenderForPK-stable : LYS.ValidSenderForPK-stable-type ℓ-PeerState ℓ-VSFP parms ValidSenderForPK)
  where
 open LYB.SystemParameters parms
 open import LibraBFT.Yasm.Base                                                                        public
 open import LibraBFT.Yasm.System     ℓ-PeerState ℓ-VSFP parms                                          public
 open import LibraBFT.Yasm.Properties ℓ-PeerState ℓ-VSFP parms ValidSenderForPK ValidSenderForPK-stable public
 open import Util.FunctionOverride    PeerId _≟PeerId_                                                 public

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 -v tc.constr.findInScope:50 #-}
module 06-listEquality where

infixr 5 _∷_

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

data Bool : Set where
  true : Bool
  false : Bool

id : {A : Set} → A → A
id v = v

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

and : Bool → Bool → Bool
and false _ = false
and _ false = false
and true true = false

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

record Eq (A : Set) : Set where
  field eq : A → A → Bool

listEq : {A : Set} → Eq A → Eq (List A)
listEq {A} eqA = record { eq = eq' } where
  eq' : List A → List A → Bool
  eq' [] [] = true
  eq' (a ∷ as) (b ∷ bs) = and (Eq.eq eqA a b) (eq' as bs)
  eq' _ _ = false

primEqBool : Bool → Bool → Bool
primEqBool true = id
primEqBool false = not

eqBool : Eq Bool
eqBool = record { eq = primEqBool }

open Eq {{...}}

test = eq (true ∷ false ∷ true ∷ []) (true ∷ false ∷ [])
  where listBoolEq = listEq eqBool

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Proof: insertion sort computes a permutation of the input list

module sortnat where

open import bool
open import eq
open import nat
open import list
open import nondet
open import nondet-thms

-- non-deterministic insert.
--This takes a nondeterministic list because I need to be able to call it with the result of perm
--
--implementation in curry:
-- ndinsert x [] = []
-- ndinsert x (y:ys) = (x : y : xs) ? (y : insert x ys)
ndinsert : {A : Set} → A → 𝕃 A → ND (𝕃 A)
ndinsert x []        = Val ( x :: [])
ndinsert x (y :: ys) = (Val ( x :: y :: ys ))
                    ?? ((_::_ y) $* (ndinsert x ys))

--non-deterministic permutation
--this is identical to the curry code (except for the Val constructor)
perm : {A : Set} → (𝕃 A) → ND (𝕃 A)
perm []        = Val []
perm (x :: xs) = (ndinsert x) *$* (perm xs)

--insert a value into a sorted list.
--this is identical to curry or haskell code.
--
--note that the structure here is identical to ndinsert
insert : ℕ → 𝕃 ℕ → 𝕃 ℕ
insert x []        = x :: []
insert x (y :: ys) = if x < y then (x :: y :: ys)
                              else (y :: insert x ys)

--simple insertion sort
--again this is identical to curry or haskell
--also, note that the structure is identical to perm
sort : 𝕃 ℕ → 𝕃 ℕ
sort []     = []
sort (x :: xs) = insert x (sort xs)

--If introduction rule for non-deterministic values.
--if x and y are both possible values in z then
--∀ c. if c then x else y will give us either x or y, so it must be a possible value of z.
--
ifIntro : {A : Set} → (x : A) → (y : A) → (nx : ND A)
       → x ∈ nx → y ∈ nx → (c : 𝔹) → (if c then x else y) ∈ nx
ifIntro x y nx p q tt = p
ifIntro x y nx p q ff = q

---------------------------------------------------------------------------
--
-- this should prove that if xs ∈ nxs then, insert x xs ∈ ndinsert x nxs
-- parameters:
-- x         : the value we are inserting into the list
-- xs        : the list
--
--returns: insert x xs ∈ ndinsert x xs
--  a proof that inserting a value in a list is ok with non-deterministic lists

insert=ndinsert : (y : ℕ) → (xs : 𝕃 ℕ) → (insert y xs) ∈ (ndinsert y xs)

-- the first case is simple: inserting into an empty list is trivial
insert=ndinsert y [] = ndrefl

--The recursive case is the interesting one.
--The list to insert an element has the form (x :: xs)
--At this point we have two possible cases.
--Either y is smaller then every element in (x :: xs), in which case it's inserted at the front,
--or y is larger than x, in which case it's inserted somewhere in xs.
--Since both of these cases are covered by ndinsert we can invoke the ifIntro lemma, to say that we don't care which case it is.
--
--variables:
-- step    : one step of insert
-- l       : the left hand side of insert y xs (the then branch)
-- r       : the right hand side of insert y xs (the else branch)
-- nr      : a non-deterministic r
-- (Val l) : a non-deterministic l (but since ndinsert only has a deterministic value on the left it's not very interesting)
-- rec     : The recursive call.  If y isn't inserted into the front, then we need to find it.
-- l∈step : a proof that l is a possible value for step
-- r∈step : a proof that r is a possible value for step
insert=ndinsert y (x :: xs) = ifIntro l r step l∈step r∈step (y < x)
  where step   = ndinsert y (x :: xs)
        l      = (y :: x :: xs)
        r      = x :: insert y xs
        nl     = Val l
        nr     = (_::_ x) $* (ndinsert y xs)
        rec    = ∈-$* (_::_ x) (insert y xs) (ndinsert y xs)
                      (insert=ndinsert y xs)
        l∈step = left  nl nr ndrefl
        r∈step = right nl nr rec

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

-- Main theorem: Sorting a list preserves permutations
-- all of the work is really done by insert=ndinsert
sortPerm : (xs : 𝕃 ℕ) → sort xs ∈ perm xs
sortPerm []        = ndrefl
sortPerm (x :: xs) = ∈-*$* (sort xs) (perm xs) (insert x) (ndinsert x)
                           (sortPerm xs) (insert=ndinsert x (sort xs))

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
open import Common.Prelude hiding (tt)
open import Common.Reflection
open import Common.Equality

tt : ⊤
tt = record{}

NoConf : Nat → Nat → Set
NoConf zero zero = ⊤
NoConf zero (suc n) = ⊥
NoConf (suc m) zero = ⊥
NoConf (suc m) (suc n) = m ≡ n

pattern `Nat = def (quote Nat) []

infixr 0 Π
syntax Π x a b = [ x ∈ a ]→ b
Π : String → Type → Type → Type
Π x a b = pi (vArg a) (abs x b)

-- noConf : (m n : ℕ) → m ≡ n → NoConfusion-ℕ m n
-- noConf zero .zero refl = tt
-- noConf (suc m) .(suc m) refl = refl

noConf : FunDef
noConf = funDef
  ([ "A" ∈ `Nat ]→ [ "B" ∈ `Nat ]→
   [ "C" ∈ def (quote _≡_) (vArg (var 1 []) ∷ vArg (var 0 []) ∷ []) ]→
   def (quote NoConf) (vArg (var 2 []) ∷ vArg (var 1 []) ∷ []))
  ( clause (vArg (con (quote zero) []) ∷ vArg dot ∷ vArg (con (quote refl) []) ∷ [])
           (def (quote tt) [])
  ∷ clause (vArg (con (quote suc) (vArg (var "m") ∷ [])) ∷ vArg dot ∷ vArg (con (quote refl) []) ∷ [])
           (def (quote refl) [])
  ∷ [])

unquoteDecl test = define (vArg test) noConf

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module z where

------------------------------------------------------------------------------
-- inductive data types and function that are defined by pattern matching

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

_+_ : ℕ → ℕ → ℕ
zero  + n =          n
suc m + n = suc (m + n)

data List {ℓ} (A : Set ℓ) : Set ℓ where
  []   :                         List A
  _::_ : (x : A) (xs : List A) → List A

_#_ : {A : Set} → List A → List A → List A
[]        # ys =            ys
(x :: xs) # ys = x :: (xs # ys)

sum : List ℕ → List ℕ → List ℕ
sum       []        ys  =                   ys
sum (x :: xs)       []  =  x      ::     xs
sum (x :: xs) (y :: ys) = (x + y) :: sum xs ys

-- inductively defined predicates
-- P over S is a data type S -> Set

data _reverseOf_ {A : Set} : List A → List A → Set where
  rev-Λ :       []  reverseOf  []
  rev-t : {x : A} {xs ys : List A}
        →       xs  reverseOf  ys
        → (x :: xs) reverseOf (ys # (x :: []))

data _⊆_ {A : Set} : List A → List A → Set where
  sub-Λ     : [] ⊆ []
  sub-right : {n : A} {ys xs : List A}
            → ys ⊆ xs →       ys  ⊆ (n :: xs)
  sub-ind   : {n : A} {ys xs : List A}
            → ys ⊆ xs → (n :: ys) ⊆ (n :: xs)

------------------------------------------------------------------------------
-- coinductive records and copattern matching

-- inductive pair
record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

-- coinductive infinite list (e.g., "stream")
record Stream (A : Set) : Set where
  coinductive
  field
    hd :        A
    tl : Stream A
open Stream

-- functions cannot be defined inductively (by pattern matching).
-- use copattern matching [APTS13]
-- - specify how the result of the function will be observed

zeros : Stream ℕ
hd zeros = zero
tl zeros = zeros

natsFrom : ℕ → Stream ℕ
hd (natsFrom n) = n
tl (natsFrom n) = natsFrom (suc n)

sumS : Stream ℕ → Stream ℕ → Stream ℕ
hd (sumS a b) =       hd a + hd b
tl (sumS a b) = sumS (tl a) (tl b)

------------------------------------------------------------------------------
-- possibly infinite streams

--open import Codata.Thunk
open import Size
open import Relation.Unary

{-
A thunk is a coinductive record with only one field, the suspended computation.
Takes a function from Size to Set (e.g., Colist A).
Accessing forces the computation and implicitly decreases the size.
'Size < i' represents all the sizes smaller than i.
-}
record Thunk {ℓ} (F : Size → Set ℓ) (i : Size) : Set ℓ where
  coinductive
  field force : {j : Size< i} → F j
open Thunk public

-- 'Size' represents an approximation level.
-- - Can be ∞.
-- - Can help termination checker by tracking depth of data structures.
-- 'Thunk' simulates laziness
data Colist {a} (A : Set a) (i : Size) : Set a where
  []   : Colist A i
  _::_ : A → Thunk (Colist A) i → Colist A i

{-
Alternative Colist impl: follows pattern used for coinductive types.
To represent a structure which can be either finite or infinite, use a coinductive record
with a field representing the whole observation which can be made on the structure.
This field is typically a variant type, since the observation can take different shapes,
e.g., if colist is non-empty then observe the pair consisting of head and tail, otherwise nothing.
-}
open import Data.Maybe
open import Data.Product

record MyColist (A : Set) : Set where
  constructor CoL_
  coinductive
  field
    list : Maybe (A × MyColist A)

-- Either of these two approaches can be used for possibly infinite structures.

data StreamT {ℓ} (A : Set ℓ) (i : Size) : Set ℓ where
  _::_ : A → Thunk (StreamT A) i → StreamT A i

record MyStream_bis (A : Set) : Set where
  coinductive
  field
    stream : A × (MyStream_bis A)

------------------------------------------------------------------------------
-- equality properties

-- stdlib equality and properties

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

-- Each property is a function that takes proofs as input and returns a new proof.

sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

------------------------------------------------------------------------------
-- Chapter 2 - Inductive reasoning

data _memberOf_ {A : Set} : A → List A → Set where
  mem-h : {x   : A} → {xs : List A} → x memberOf     (x            :: xs)
  mem-t : {x y : A} → {xs : List A} → x memberOf xs → x memberOf(y :: xs)

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Converting reflection machinery to strings
------------------------------------------------------------------------

-- Note that Reflection.termErr can also be used directly in tactic
-- error messages.

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

module Reflection.Show where

import Data.Char as Char
import Data.Float as Float
open import Data.List hiding (_++_; intersperse)
import Data.Nat as ℕ
import Data.Nat.Show as ℕ
open import Data.String as String
import Data.Word as Word
open import Relation.Nullary using (yes; no)
open import Function.Base using (_∘′_)

open import Reflection.Abstraction hiding (map)
open import Reflection.Argument hiding (map)
open import Reflection.Argument.Relevance
open import Reflection.Argument.Visibility
open import Reflection.Argument.Information
open import Reflection.Definition
open import Reflection.Literal
open import Reflection.Pattern
open import Reflection.Term

------------------------------------------------------------------------
-- Re-export primitive show functions

open import Agda.Builtin.Reflection public
  using () renaming
  ( primShowMeta  to showMeta
  ; primShowQName to showName
  )

------------------------------------------------------------------------
-- Non-primitive show functions

showRelevance : Relevance → String
showRelevance relevant   = "relevant"
showRelevance irrelevant = "irrelevant"

showRel : Relevance → String
showRel relevant   = ""
showRel irrelevant = "."

showVisibility : Visibility → String
showVisibility visible   = "visible"
showVisibility hidden    = "hidden"
showVisibility instance′ = "instance"

showLiteral : Literal → String
showLiteral (nat x)    = ℕ.show x
showLiteral (word64 x) = ℕ.show (Word.toℕ x)
showLiteral (float x)  = Float.show x
showLiteral (char x)   = Char.show x
showLiteral (string x) = String.show x
showLiteral (name x)   = showName x
showLiteral (meta x)   = showMeta x

mutual

  showPatterns : List (Arg Pattern) → String
  showPatterns []       = ""
  showPatterns (a ∷ ps) = showArg a <+> showPatterns ps
    where
    showArg : Arg Pattern → String
    showArg (arg (arg-info visible r) p)   = showRel r ++ showPattern p
    showArg (arg (arg-info hidden r) p)    = braces (showRel r ++ showPattern p)
    showArg (arg (arg-info instance′ r) p) = braces (braces (showRel r ++ showPattern p))

  showPattern : Pattern → String
  showPattern (con c []) = showName c
  showPattern (con c ps) = parens (showName c <+> showPatterns ps)
  showPattern dot        = "._"
  showPattern (var s)    = s
  showPattern (lit l)    = showLiteral l
  showPattern (proj f)   = showName f
  showPattern absurd     = "()"

private
  -- add appropriate parens depending on the given visibility
  visibilityParen : Visibility → String → String
  visibilityParen visible   s = parensIfSpace s
  visibilityParen hidden    s = braces s
  visibilityParen instance′ s = braces (braces s)

mutual

  showTerms : List (Arg Term) → String
  showTerms []             = ""
  showTerms (arg i t ∷ ts) = visibilityParen (visibility i) (showTerm t) <+> showTerms ts

  showTerm : Term → String
  showTerm (var x args)         = "var" <+> ℕ.show x <+> showTerms args
  showTerm (con c args)         = showName c <+> showTerms args
  showTerm (def f args)         = showName f <+> showTerms args
  showTerm (lam v (abs s x))    = "λ" <+> visibilityParen v s <+> "→" <+> showTerm x
  showTerm (pat-lam cs args)    =
    "λ {" <+> showClauses cs <+> "}" <+> showTerms args
  showTerm (Π[ x ∶ arg i a ] b) =
    "Π (" ++ visibilityParen (visibility i) x <+> ":" <+>
    parensIfSpace (showTerm a) ++ ")" <+> parensIfSpace (showTerm b)
  showTerm (sort s)             = showSort s
  showTerm (lit l)              = showLiteral l
  showTerm (meta x args)        = showMeta x <+> showTerms args
  showTerm unknown              = "unknown"

  showSort : Sort → String
  showSort (set t) = "Set" <+> parensIfSpace (showTerm t)
  showSort (lit n) = "Set" ++ ℕ.show n -- no space to disambiguate from set t
  showSort unknown = "unknown"

  showClause : Clause → String
  showClause (clause ps t)      = showPatterns ps <+> "→" <+> showTerm t
  showClause (absurd-clause ps) = showPatterns ps

  showClauses : List Clause → String
  showClauses []       = ""
  showClauses (c ∷ cs) = showClause c <+> ";" <+> showClauses cs

showDefinition : Definition → String
showDefinition (function cs)       = "function" <+> braces (showClauses cs)
showDefinition (data-type pars cs) =
 "datatype" <+> ℕ.show pars <+> braces (intersperse ", " (map showName cs))
showDefinition (record′ c fs)      =
 "record" <+> showName c <+> braces (intersperse ", " (map (showName ∘′ unArg) fs))
showDefinition (constructor′ d)    = "constructor" <+> showName d
showDefinition axiom               = "axiom"
showDefinition primitive′          = "primitive"


text:
{-# OPTIONS --copatterns #-}
module CoinductiveUnitRecord where

import Common.Level
open import Common.Equality

record Unit : Set where
  coinductive
  constructor delay
  field force : Unit
open Unit

good : Unit
force good = good

bad : Unit
bad = delay bad
-- should not termination check ...

bad' : Unit
bad' = delay bad'

-- ... because this loops:
-- loop : bad ≡ bad'
-- loop = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda