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

-- A Beth model for normalization by evaluation

open import Library

module NbeModel (Base : Set) (B⦅_⦆ : Base → Set) where

import Formulas      ; open module Form = Formulas    Base hiding (Mon)
import Derivations   ; open module Der  = Derivations Base
import Interpretation; open module Intp = Interpretation Base B⦅_⦆

-- Form of Kripke predicates into a set S

KPred' : (S : Set) → Set₁
KPred' S = ∀ Γ → (C⦅ Γ ⦆ → S) → Set

-- Form of Kripke predicate on functions into type A
-- KPred A = ∀ Γ → Fun Γ A → Set

KPred : (A : Form) → Set₁
KPred A = KPred' T⦅ A ⦆

-- Pointwise inclusion of Kripke predicates

Sub : ∀ A (P Q : KPred A) → Set
Sub A P Q = ∀{Γ f} → P Γ f → Q Γ f

⟨_⟩_↪_ : ∀ A (P Q : KPred A) → Set
⟨ A ⟩ P ↪ Q = ∀{Γ f} → P Γ f → Q Γ f

_↪_ : ∀{A} (P Q : KPred A) → Set
P ↪ Q = ∀{Γ f} → P Γ f → Q Γ f

-- Conv generalizes _↪_ to move to a new proposition.

Conv : ∀{S T : Set} (f : S → T) (P : KPred' S) (Q : KPred' T) → Set
Conv {S} f P Q = ∀ {Γ} {g : C⦅ Γ ⦆ → S} (p : P Γ g) → Q Γ (f ∘ g)

⟪_⟫_↪_ = Conv

⟪_⟫₂_↪_↪_ : ∀{R S T : Set} (f : R → S → T) (𝓡 : KPred' R) (𝓢 : KPred' S) (𝓣 : KPred' T) → Set
⟪ f ⟫₂ 𝓡 ↪ 𝓢 ↪ 𝓣 = ∀{Γ g h} → 𝓡 Γ g → 𝓢 Γ h → 𝓣 Γ (λ γ → f (g γ) (h γ))

-- Statement of monotonicity for Kripke predicates

Mon : ∀{S} (𝓐 : KPred' S) → Set
Mon {S} 𝓐 = ∀ {Γ Δ} (τ : Δ ≤ Γ) {f : Fun' Γ S} → 𝓐 Γ f → 𝓐 Δ (f ∘ R⦅ τ ⦆)

-- Image under evaluation of a neutral term

NeImg : ∀ A → KPred A
NeImg A Γ f = ∃ λ (t : Ne Γ A) → Ne⦅ t ⦆ ≡ f

-- Image under evaluation of a normal term

NfImg : ∀ A → KPred A
NfImg A Γ f = ∃ λ (t : Nf Γ A) → Nf⦅ t ⦆ ≡ f

-- Being an image is Kripke (monotone in weakening)
-- ∀ (f : Fun Γ A) (τ : Δ ≤ Γ) → Img Γ A f → Img Δ A (f ∘ R⦅ τ ⦆)

monNeImg : ∀{A} → Mon (NeImg A)
monNeImg τ (t , refl) = monNe τ t , natD τ (ne[ t ])

monNfImg : ∀{A} → Mon (NfImg A)
monNfImg τ (t , refl) = monNf τ t , natD τ nf[ t ]

-- Extending the constructions of neutral and normal forms to images of such.

-- Neutrals of base type are normal

iNe : ∀{P} → NeImg (Atom P) ↪ NfImg (Atom P)
iNe (t , eq) =  ne t , eq

-- Variables are neutral

iHyp : ∀{Γ A} (x : Hyp A Γ) → NeImg A Γ H⦅ x ⦆
iHyp x = (hyp x , refl)

-- Abstraction operates on normal forms

iImpI : ∀{Γ A B f} → NfImg B (Γ ∙ A) f → NfImg (A ⇒ B) Γ (curry f)
iImpI (t , eq) = impI t , cong curry eq

-- Application of a neutral is neutral
-- iImpE : NeImg (A ⇒ B) Γ f → NfImg A Γ g → NeImg B Γ (apply f g)

iImpE : ∀{A B} → ⟪ _$_ ⟫₂ NeImg (A ⇒ B) ↪ NfImg A ↪ NeImg B
iImpE (t , eq) (u , eq') = (impE t u , cong₂ apply eq eq')

-- Empty tuple is normal

iTrueI : ∀{Γ f} → NfImg True Γ f
iTrueI = trueI , refl

-- Pairing operates on normal forms

iAndI : ∀{A B} → ⟪ _,_ ⟫₂ NfImg A ↪ NfImg B ↪ NfImg (A ∧ B)
iAndI (t , eq) (u , eq') = andI t u , cong₂ <_,_> eq eq'

-- Projection of a neutral is neutral

iAndE₁ : ∀{A B} → ⟪ proj₁ ⟫ NeImg (A ∧ B) ↪ NeImg A
iAndE₁ (t , eq) = andE₁ t , cong (proj₁ ∘_) eq

iAndE₂ : ∀{A B} → ⟪ proj₂ ⟫ NeImg (A ∧ B) ↪ NeImg B
iAndE₂ (t , eq) = andE₂ t , cong (proj₂ ∘_) eq

-- Injections operate on normal forms

iOrI₁ : ∀{A B} → ⟪ inj₁ ⟫ NfImg A ↪ NfImg (A ∨ B)
iOrI₁ (t , eq) = orI₁ t , cong (inj₁ ∘_) eq

iOrI₂ : ∀{A B} → ⟪ inj₂ ⟫ NfImg B ↪ NfImg (A ∨ B)
iOrI₂ (t , eq) = orI₂ t , cong (inj₂ ∘_) eq

-- Case splitting forms:

iOrE : ∀{Γ A B C f g h}
  → NeImg (A ∨ B) Γ f
  → NfImg C (Γ ∙ A) g
  → NfImg C (Γ ∙ B) h
  → NfImg C Γ (caseof f g h)
iOrE (t , eqt) (u , equ) (v , eqv) = orE t u v , cong₃ caseof eqt equ eqv

iFalseE : ∀{C} → ⟪ ⊥-elim ⟫ NeImg False ↪ NfImg C
iFalseE (t , eq) = falseE t , cong (⊥-elim ∘_) eq

-- For falseE, we can get the stronger:

iFalseE' : ∀{Γ C f}
  → Ne Γ False
  → NfImg C Γ (⊥-elim ∘ f)
iFalseE' t = falseE t , ⊥-elim-ext

-- Cover A (P : KPred A) : KPred A  is an extension of Kripke predicate P
-- (on functions into A) by case trees (whose leaves satisfy P).

data Cover (A : Form) (P : KPred A)  (Δ : Cxt) : (f : Fun Δ A) → Set where
  return : ∀{f} (p : P Δ f) → Cover A P Δ f
  falseC : (t : Ne Δ False) → Cover A P Δ (⊥-elim ∘ Ne⦅ t ⦆)
  orC    : ∀{C D} (t : Ne Δ (C ∨ D))
           {g} (cg : Cover A P (Δ ∙ C) g)
           {h} (ch : Cover A P (Δ ∙ D) h) → Cover A P Δ (caseof Ne⦅ t ⦆ g h)

-- Cover is monotone in P

mapC : ∀{A} {P Q : KPred A} (P⊂Q : ⟨ A ⟩ P ↪ Q) → ⟨ A ⟩ Cover A P ↪ Cover A Q
mapC P⊂Q (return p)    = return (P⊂Q p)
mapC P⊂Q (falseC t)    = falseC t
mapC P⊂Q (orC t cg ch) = orC t (mapC P⊂Q cg) (mapC P⊂Q ch)

-- Case trees can be composed, which makes  Cover A  a monad
-- in the category of kripke predicates  KPred A  and  their embeddings
-- ⟨ A ⟩.

joinC : ∀{A} {P : KPred A} → ⟨ A ⟩ Cover A (Cover A P) ↪ Cover A P
joinC (return c)    = c
joinC (falseC t)    = falseC t
joinC (orC t cg ch) = orC t (joinC cg) (joinC ch)

-- Weakening covers (Cover preserves Kripke)
-- (τ : Δ ≤ Γ) → Cover A Γ P f → Cover A Δ P (f ∘ R⦅ τ ⦆)

monC : ∀{A} {P : KPred A} (monP : Mon P) → Mon (Cover A P)
monC monP τ (return p)    = return (monP τ p)
monC monP τ (falseC t)    = subst (Cover _ _ _) ⊥-elim-ext (falseC (monNe τ t))
monC monP τ (orC t cg ch) = orC (monNe τ t) (monC monP (lift τ) cg) (monC monP (lift τ) ch)
  -- REWRITE monD-ne natD

-- Converting covers to a new target proposition

-- A (simple) converter for covers (pointwise in the context)

convC : ∀{A B} (g : T⦅ A ⦆ → T⦅ B ⦆) {P Q} (P⊂Q : ⟪ g ⟫ P ↪ Q) → ⟪ g ⟫ Cover A P ↪ Cover B Q
convC g P⊂Q (return p)    = return (P⊂Q p)
convC g P⊂Q (falseC t)    = subst (Cover _ _ _) ⊥-elim-ext (falseC t)
convC g P⊂Q (orC t cg ch) = subst (Cover _ _ _) (caseof-perm g {Ne⦅ t ⦆})
  (orC t (convC g P⊂Q cg) (convC g P⊂Q ch))

-- A general converter going to a new target proposition and an extended context at the same time.
-- (subsumes mapC, monC, convC).

record Converter A B (P : KPred A) (Q : KPred B) {Γ₀ Δ₀} (τ₀ : Δ₀ ≤ Γ₀) : Set where
  field
    -- Conversion functional
    φ      : ∀ {Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) → Fun Γ A → Fun Δ B

    -- φ distributes over case
    φ-case : ∀ {Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) →
             ∀ C D (f : Fun Γ (C ∨ D)) (g : Fun (Γ ∙ C) A) (h : Fun (Γ ∙ D) A)
             → caseof (f ∘ R⦅ τ ⦆) (φ (weak δ) (lift {C} τ) g)
                                  (φ (weak δ) (lift {D} τ) h) ≡ φ δ τ (caseof f g h)

    -- φ transports from P to Q
    P⊂Q   : ∀{Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) {f} → P Γ f → Q Δ (φ δ τ f)

-- The conversion is implemented by recursion over the case tree

module _ A B (P : KPred A) (Q : KPred B) {Γ₀ Δ₀} (τ₀ : Δ₀ ≤ Γ₀)
  (conv : Converter A B P Q τ₀) (open Converter conv) where

  convCov : ∀{Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) {f} → Cover A P Γ f → Cover B Q Δ (φ δ τ f)
  convCov {Γ} {Δ} δ τ (return p) = return (P⊂Q δ τ p)
  convCov {Γ} {Δ} δ τ (falseC t) = subst (Cover _ _ _) ⊥-elim-ext (falseC (monNe τ t))
  convCov {Γ} {Δ} δ τ (orC {C} {D} t {g} cg {h} ch) =
    subst (Cover _ _ _)
      (φ-case δ τ C D Ne⦅ t ⦆ g h)
      (orC (monNe τ t)
        (convCov (weak δ) (lift {C} τ) cg)
        (convCov (weak δ) (lift {D} τ) ch))

    -- Just for documentation:
    where
    τC = lift {C} τ
    cg' : Cover B Q (Δ ∙ C) (φ (weak δ) τC g)
    cg' = convCov (weak δ) τC cg

    τD = lift {D} τ
    ch' : Cover B Q (Δ ∙ D) (φ (weak δ) τD h)
    ch' = convCov (weak δ) τD ch

    c' : Cover B Q Δ (caseof (Ne⦅ t ⦆ ∘ R⦅ τ ⦆) (φ (weak δ) τC g) (φ (weak δ) τD h))
    c' = orC (monNe τ t) cg' ch'

-- Implementations in terms of convCov (all need monotonicity of P)

-- Cover is monotone in P

mapCᶜ : ∀{A} {P Q : KPred A} (monP : Mon P) (P⊂Q : ⟨ A ⟩ P ↪ Q) → ⟨ A ⟩ Cover A P ↪ Cover A Q
mapCᶜ {A} {P} {Q} monP P⊂Q {Γ} {f} c = convCov A A P Q id≤ conv id≤ id≤ c
  where
  conv : Converter A A P Q ( id≤ {Γ})
  conv = record
    { φ      = λ δ τ f         → f ∘ R⦅ τ ⦆
    ; φ-case = λ δ τ C D f g h → refl
    ; P⊂Q    = λ δ τ ⟦f⟧       → P⊂Q (monP τ ⟦f⟧)
    }

-- Weakening Covers

monCᶜ : ∀{A} {P : KPred A} (monP : Mon P) → Mon (Cover A P)
monCᶜ {A} {P} monP {Γ} {Δ} τ {f} c = convCov A A P P id≤ conv id≤ τ c
  where
  conv : Converter A A P P id≤
  conv = record
    { φ      = λ δ τ f         → f ∘ R⦅ τ ⦆
    ; φ-case = λ δ τ C D f g h → refl
    ; P⊂Q    = λ δ τ ⟦f⟧       → monP τ ⟦f⟧
    }

-- A converter for covers (pointwise in the context)

convCᶜ : ∀{A B} (g : T⦅ A ⦆ → T⦅ B ⦆) {P Q} (monP : Mon P) (P⊂Q : ⟪ g ⟫ P ↪ Q) → ⟪ g ⟫ Cover A P ↪ Cover B Q
convCᶜ {A} {B} g₀ {P} {Q} monP P⊂Q {Γ} {f} p = convCov A B P Q id≤ conv id≤ id≤ p
  where
  conv : Converter A B P Q id≤
  conv = record
    { φ      = λ δ τ f         → g₀ ∘ f ∘ R⦅ τ ⦆
    ; φ-case = λ δ τ C D f g h → caseof-perm g₀ {f ∘ R⦅ τ ⦆}
    ; P⊂Q    = λ δ τ ⟦f⟧       → P⊂Q (monP τ ⟦f⟧)
    }

-- Syntactic paste:
-- a case tree over normal forms is a normal form.

pasteNf : ∀{A} → ⟨ A ⟩ Cover A (NfImg A) ↪ NfImg A
pasteNf (return t)    = t
pasteNf (falseC t)    = iFalseE (t , refl)
pasteNf (orC t cg ch) = iOrE (t , refl) (pasteNf cg) (pasteNf ch)

-- Bicartesian closure of KPred

-- Semantic absurdity type (initial object)

Absurd : KPred False
Absurd _ _ = ⊥

-- Semantic disjunction type (coproduct)

data Disj A B (⟦A⟧ : KPred A) (⟦B⟧ : KPred B) Γ : Fun Γ (A ∨ B) → Set where
  left  : {g : Fun Γ A} (⟦g⟧ : ⟦A⟧ Γ g) → Disj _ _ _ _ _ (inj₁ ∘ g)
  right : {h : Fun Γ B} (⟦h⟧ : ⟦B⟧ Γ h) → Disj _ _ _ _ _ (inj₂ ∘ h)

monDisj : ∀{A B ⟦A⟧ ⟦B⟧} (monA : Mon ⟦A⟧) (monB : Mon ⟦B⟧) → Mon (Disj A B ⟦A⟧ ⟦B⟧)
monDisj monA monB τ (left  ⟦g⟧) = left  (monA τ ⟦g⟧)
monDisj monA monB τ (right ⟦h⟧) = right (monB τ ⟦h⟧)

-- Semantic truth type (terminal object)

Truth : KPred True
Truth _ _ = ⊤

-- Semantic conjunction type (product)

Conj : ∀ A B (⟦A⟧ : KPred A) (⟦B⟧ : KPred B) → KPred (A ∧ B)
Conj A B ⟦A⟧ ⟦B⟧ Γ f = ⟦A⟧ Γ (proj₁ ∘ f) × ⟦B⟧ Γ (proj₂ ∘ f)

-- Semantic implication type (exponential)

Imp : ∀ A B (⟦A⟧ : KPred A) (⟦B⟧ : KPred B) → KPred (A ⇒ B)
Imp A B ⟦A⟧ ⟦B⟧ Γ f = ∀{Δ} (τ : Δ ≤ Γ) {a : Fun Δ A} (⟦a⟧ : ⟦A⟧ Δ a) → ⟦B⟧ Δ (kapp A B f τ a)

-- The Beth model

T⟦_⟧ : (A : Form) → KPred A
T⟦ Atom P ⟧ = NfImg (Atom P)
T⟦ True   ⟧ = Truth
T⟦ False  ⟧ = Cover False   Absurd
T⟦ A ∨ B  ⟧ = Cover (A ∨ B) (Disj A B (T⟦ A ⟧) (T⟦ B ⟧))
T⟦ A ∧ B  ⟧ = Conj A B T⟦ A ⟧ T⟦ B ⟧
T⟦ A ⇒ B  ⟧ = Imp A B T⟦ A ⟧ T⟦ B ⟧

-- Monotonicity of semantics
-- (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ f → T⟦ A ⟧ Δ (f ∘ R⦅ τ ⦆)

monT : ∀ A → Mon T⟦ A ⟧
monT (Atom P)  = monNfImg
monT True      = _
monT False     = monC λ _ ()
monT (A ∨ B)   = monC (monDisj (monT A) (monT B))
monT (A ∧ B) τ = monT A τ ×̇ monT B τ
monT (A ⇒ B) τ f σ = f (σ • τ)

-- Reflection / reification

mutual

  reflect : ∀ A → ⟨ A ⟩ NeImg A ↪ T⟦ A ⟧
  reflect (Atom P)      = iNe
  reflect True          = _
  reflect False (t , _) = subst (Cover _ _ _) ⊥-elim-ext (falseC t)

  -- x : A ∨ B  is reflected as case(x, y. inl y, z. inr z)
  -- Need a proof of caseof x inj₁ inj₂ = x
  reflect (A ∨ B) (t , refl) = subst (Cover _ _ _) (caseof-eta Ne⦅ t ⦆)
    (orC t (return (left  (reflect A (iHyp top))))
           (return (right (reflect B (iHyp top)))))

  reflect (A ∧ B) i     = reflect A (iAndE₁ i) , reflect B (iAndE₂ i)
  reflect (A ⇒ B) i τ a = reflect B (iImpE (monNeImg τ i) (reify A a))

  reify : ∀ A → ⟨ A ⟩ T⟦ A ⟧ ↪ NfImg A
  reify (Atom P)        = id
  reify True _          = iTrueI
  reify False           = pasteNf ∘ mapC λ()
  reify (A ∨ B)         = pasteNf ∘ mapC reifyDisj
  reify (A ∧ B) (a , b) = iAndI (reify A a) (reify B b)
  reify (A ⇒ B) ⟦f⟧     = iImpI (reify B (⟦f⟧ (weak id≤) (reflect A (iHyp top))))

  reifyDisj : ∀{A B} → ⟨ A ∨ B ⟩ Disj A B T⟦ A ⟧ T⟦ B ⟧ ↪ NfImg (A ∨ B)
  reifyDisj {A} {B} (left  ⟦g⟧) = iOrI₁ (reify A ⟦g⟧)
  reifyDisj {A} {B} (right ⟦h⟧) = iOrI₂ (reify B ⟦h⟧)

-- Semantic paste

paste : ∀ A → ⟨ A ⟩ Cover A (T⟦ A ⟧) ↪ T⟦ A ⟧
paste (Atom P) = pasteNf
paste True     = _
paste False    = joinC
paste (A ∨ B)  = joinC
paste (A ∧ B)  = < paste A ∘ convC proj₁ proj₁ , paste B ∘ convC proj₂ proj₂ >
paste (A ⇒ B) {Γ₀} {f} c {Δ₀} τ₀ {a} ⟦a⟧ = paste B (convCov (A ⇒ B) B P Q τ₀ record{Conv} id≤ τ₀ c)
  where
  P = Imp A B T⟦ A ⟧ T⟦ B ⟧
  Q = T⟦ B ⟧

  module Conv where
    φ : ∀ {Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) → Fun Γ (A ⇒ B) → Fun Δ B
    φ δ τ f = kapp A B f τ (a ∘ R⦅ δ ⦆)

    P⊂Q : ∀ {Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) {f} → P Γ f → Q Δ (φ δ τ f)
    P⊂Q δ τ ⟦f⟧ = ⟦f⟧ τ (monT A δ ⟦a⟧)

    φ-case : ∀ {Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) →
             ∀ C D (f : Fun Γ (C ∨ D)) (g : Fun (Γ ∙ C) (A ⇒ B)) (h : Fun (Γ ∙ D) (A ⇒ B))
             → caseof (f ∘ R⦅ τ ⦆) (φ (weak δ) (lift {C} τ) g)
                                   (φ (weak δ) (lift {D} τ) h) ≡ φ δ τ (caseof f g h)

    φ-case δ τ C D f g h = caseof-kapply f g h R⦅ τ ⦆ (a ∘ R⦅ δ ⦆)

-- Fundamental theorem

-- Extension of T⟦_⟧ to contexts

G⟦_⟧ : ∀ Γ → KPred' C⦅ Γ ⦆
G⟦ ε     ⟧ Δ ρ = ⊤
G⟦ Γ ∙ A ⟧ Δ ρ = G⟦ Γ ⟧ Δ (proj₁ ∘ ρ) × T⟦ A ⟧ Δ (proj₂ ∘ ρ)

-- monG : ∀{Γ Δ Φ ρ} (τ : Φ ≤ Δ) → G⟦ Γ ⟧ Δ ρ → G⟦ Γ ⟧ Φ (ρ ∘ R⦅ τ ⦆)
monG : ∀{Γ} → Mon G⟦ Γ ⟧
monG {ε}     τ _       = _
monG {Γ ∙ A} τ (γ , a) = monG τ γ , monT A τ a

-- Variable case
-- fundH : (x : Hyp A Γ) (γ : G⟦ Γ ⟧ Δ ρ) → T⟦ A ⟧ Δ (H⦅ x ⦆ ∘ ρ)

fundH : ∀{Γ A} (x : Hyp A Γ) → ⟪ H⦅ x ⦆ ⟫ G⟦ Γ ⟧ ↪ T⟦ A ⟧
fundH top     = proj₂
fundH (pop x) = fundH x ∘ proj₁

-- orE case

orElim : ∀ E {Γ A B}
         {f} (⟦f⟧ : T⟦ A ∨ B ⟧ Γ f)
         {g} (⟦g⟧ : T⟦ A ⇒ E ⟧ Γ g)
         {h} (⟦h⟧ : T⟦ B ⇒ E ⟧ Γ h) →
         T⟦ E ⟧ Γ (caseof f (uncurry g) (uncurry h))
orElim E {Γ₀} {A} {B} ⟦f⟧ {g} ⟦g⟧ {h} ⟦h⟧ = paste E
  (convCov (A ∨ B) E P Q {Γ₀} id≤ record{Conv} id≤ id≤ ⟦f⟧)
  where

  P = Disj A B T⟦ A ⟧ T⟦ B ⟧
  Q = T⟦ E ⟧

  module Conv where

    φ : ∀ {Γ Δ} (δ : Δ ≤ Γ₀) (τ : Δ ≤ Γ) → Fun Γ (A ∨ B) → Fun Δ E
    φ δ τ f = caseof (f ∘ R⦅ τ ⦆) (uncurry (g ∘ R⦅ δ ⦆)) (uncurry (h ∘ R⦅ δ ⦆ ))

    P⊂Q : ∀{Γ Δ} (δ : Δ ≤ Γ₀) (τ : Δ ≤ Γ) {f} → P Γ f → Q Δ (φ δ τ f)
    P⊂Q δ τ (left  ⟦a⟧) = ⟦g⟧ δ (monT A τ ⟦a⟧)
    P⊂Q δ τ (right ⟦b⟧) = ⟦h⟧ δ (monT B τ ⟦b⟧)

    φ-case : ∀ {Γ Δ} (δ : Δ ≤ Γ₀) (τ : Δ ≤ Γ) →
      ∀ C D (k : Fun Γ (C ∨ D)) (i : Fun (Γ ∙ C) (A ∨ B)) (j : Fun (Γ ∙ D) (A ∨ B)) →

        caseof (k ∘ R⦅ τ ⦆) (φ (weak δ) (lift {C} τ) i)
                           (φ (weak δ) (lift {D} τ) j)
        ≡ φ δ τ (caseof k i j)

    φ-case δ τ C D k i j =
     caseof-swap
       (k ∘ R⦅ τ ⦆)
       (uncurry (curry i ∘ R⦅ τ ⦆))
       (uncurry (curry j ∘ R⦅ τ ⦆))
       (g ∘ R⦅ δ ⦆)
       (h ∘ R⦅ δ ⦆)

-- A lemma for the falseE case

falseElim : ∀ A → ⟪ ⊥-elim ⟫ T⟦ False ⟧ ↪ T⟦ A ⟧
falseElim A = paste A ∘ convC ⊥-elim ⊥-elim

-- The fundamental theorem

-- fund :  ∀{A Γ} (t : Γ ⊢ A) {Δ ρ} (γ : G⟦ Γ ⟧ Δ ρ) → T⟦ A ⟧ Δ (D⦅ t ⦆ ∘ ρ)
fund :  ∀{A Γ} (t : Γ ⊢ A) → ⟪ D⦅ t ⦆ ⟫ G⟦ Γ ⟧ ↪ T⟦ A ⟧
fund (hyp x)           = fundH x
fund (impI t) γ τ a    = fund t (monG τ γ , a)
fund (impE t u) γ      = fund t γ id≤ (fund u γ)
fund (andI t u)        = < fund t , fund u >
fund (andE₁ t)         = proj₁ ∘ fund t
fund (andE₂ t)         = proj₂ ∘ fund t
fund (orI₁ t) γ        = return (left  (fund t γ))
fund (orI₂ t) γ        = return (right (fund t γ))
fund {A} (orE t u v) γ =  orElim A (fund t γ)
  (λ τ a → fund u (monG τ γ , a))
  (λ τ b → fund v (monG τ γ , b))
fund {A} (falseE t) γ  =  falseElim A (fund t γ)
fund trueI γ           = _

-- Identity environment

ide : ∀ Γ → G⟦ Γ ⟧ Γ id
ide ε = _
ide (Γ ∙ A) = monG (weak id≤) (ide Γ) , reflect A (iHyp top)

-- Normalization by evaluation

norm : ∀{Γ A} (t : Γ ⊢ A) → NfImg A Γ D⦅ t ⦆
norm t = reify _ (fund t (ide _))

-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types #-}

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat
open import Data.Vec
open import Data.Fin
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Size
open import Codata.Thunk
open import Axiom.ExcludedMiddle
open import Level renaming (zero to ∅ ; suc to ++)

open import is-lib.SInfSys as IS
open import Examples.Lambda.Lambda
open import Examples.Lambda.BigStep renaming (U to BigStepU)
open import Examples.Lambda.SmallStep

module Examples.Lambda.Proofs where

  Spec : BigStepU → Set
  Spec (e , res x) = e ⇒* term x
  Spec (e , div) = ∀{i} → ⇒∞ e i

  {- Soundness -}
  Spec-val : BigStepU → Set
  Spec-val (e , v) = ∀{v'} → v ≡ res v' → Spec (e , v)

  Spec-closed : ISClosed (BigStepIS ∪ BigStepCOIS) Spec-val
  Spec-closed (inj₁ VAL) _ _ refl = ε
  Spec-closed (inj₁ APP) _ prem refl =
    let s-e1 = prem zero refl in
    let s-e2 = prem (suc zero) refl in
    let s-subst = prem (suc (suc zero)) refl in
    let subst = IS.fold (β , _ , refl , λ ()) in
    inj-l-app _ (prem zero refl) ◅◅ inj-r-app _ (prem (suc zero) refl) ◅◅ subst ◅ prem (suc (suc zero)) refl
  Spec-closed (inj₂ COA) s_ _ ()

  ⇓ᵢ-to-⇒* : ∀{e v} → e ⇓ᵢ v → Spec-val (e , v)
  ⇓ᵢ-to-⇒* = ind[ BigStepIS ∪ BigStepCOIS ] Spec-val Spec-closed

  bs-sound-v : ∀{e v} → (∀{i} → (e ⇓ (res v)) i) → e ⇒* (term v)
  bs-sound-v r = ⇓ᵢ-to-⇒* (sfcoind-to-ind r) refl

  subject-red-⇓ : ∀{e e' v} → (∀{i} → (e ⇓ v) i) → e ⇒ e' → (∀{i} → (e' ⇓ v) i)
  subject-red-⇓ bs (fold (β , (e , v) , eq , _)) with bs
  subject-red-⇓ bs (fold (β , (e , v) , () , _)) | sfold (VAL , (lambda x , _) , refl , prem)
  subject-red-⇓ bs (fold (β , (e , lambda x) , refl , _)) | sfold (APP , ((.(lambda e) , _ , .(lambda x) , v , _) , _) , refl , prem)
    with val-⇓-≡ (prem zero .force) | val-⇓-≡ (prem (suc zero) .force)
  subject-red-⇓ bs (fold (β , (e , lambda x) , refl , _)) | sfold (APP , ((.(lambda e) , .e , .(lambda x) , .(lambda x) , _) , _) , refl , prem) | refl | refl = prem (suc (suc zero)) .force
  subject-red-⇓ bs (fold (β , (e , v) , refl , _)) | sfold (L-DIV , _ , refl , prem) = ⊥-elim (val-not-reduce⇓ (prem zero .force))
  subject-red-⇓ bs (fold (β , (e , v) , refl , _)) | sfold (R-DIV , _ , refl , prem) = ⊥-elim (val-not-reduce⇓ (prem (suc zero) .force))
  subject-red-⇓ bs (fold (L-APP , c , eq , _)) with bs
  subject-red-⇓ bs (fold (L-APP , _ , () , _)) | sfold (VAL , (lambda _ , _) , refl , _)
  subject-red-⇓ bs (fold (L-APP , (e1 , e1' , e2) , refl , pr)) | sfold (APP , ((.e1 , e1'' , .e2 , lambda _ , _) , ind) , refl , prem) =
    let rec = subject-red-⇓ (prem zero .force) (pr zero) in
    let prems = λ{zero → rec ; (suc zero) → prem (suc zero) .force ; (suc (suc zero)) → prem (suc (suc zero)) .force} in
    apply-sfcoind APP _ prems
  subject-red-⇓ bs (fold (L-APP , (e1 , e1' , e2) , refl , pr)) | sfold (L-DIV , ((.e1 , .e2) , ind) , refl , prem) =
    let rec = subject-red-⇓ (prem zero .force) (pr zero) in
    apply-sfcoind L-DIV _ λ{zero → rec}
  subject-red-⇓ bs (fold (L-APP , (e1 , e1' , e2) , refl , pr)) | sfold (R-DIV , ((.e1 , .e2 , lambda v) , ind) , refl , prem) =
    let rec = subject-red-⇓ (prem zero .force) (pr zero) in
    let prems = λ{zero → rec ; (suc zero) → prem (suc zero) .force} in
    apply-sfcoind R-DIV _ prems
  subject-red-⇓ bs (fold (R-APP , (lambda _ , e2 , e2') , eq , pr)) with bs
  subject-red-⇓ bs (fold (R-APP , (lambda _ , _ , _) , refl , _)) | sfold (VAL , (lambda _ , _) , () , _)
  subject-red-⇓ bs (fold (R-APP , (lambda e1 , e2 , e2') , refl , pr)) | sfold (APP , ((.(lambda _) , e1' , .e2 , lambda _ , _) , ind) , refl , prem)
    with val-⇓-≡ (prem zero .force)
  subject-red-⇓ bs (fold (R-APP , (lambda e1 , e2 , e2') , refl , pr)) | sfold (APP , ((.(lambda e1) , .e1 , .e2 , lambda _ , _) , ind) , refl , prem) | refl =
    let rec = subject-red-⇓ (prem (suc zero) .force) (pr zero) in
    let prems = λ{zero → prem zero .force ; (suc zero) → rec ; (suc (suc zero)) → prem (suc (suc zero)) .force} in
    apply-sfcoind APP _ prems
  subject-red-⇓ bs (fold (R-APP , (lambda _ , e2 , e2') , refl , _)) | sfold (L-DIV , ((.(lambda _) , .e2) , _) , refl , prem) = ⊥-elim (val-not-reduce⇓ (prem zero .force))
  subject-red-⇓ bs (fold (R-APP , (lambda e , e2 , e2') , refl , pr)) | sfold (R-DIV , ((.(lambda e) , .e2 , v) , ind) , refl , prem) with val-⇓-≡ (prem zero .force)
  subject-red-⇓ bs (fold (R-APP , (lambda e , e2 , e2') , refl , pr)) | sfold (R-DIV , ((.(lambda e) , .e2 , .(lambda e)) , ind) , refl , prem) | refl =
    let rec = subject-red-⇓ (prem (suc zero) .force) (pr zero) in
    let prems = λ{zero → prem zero .force ; (suc zero) → rec} in
    apply-sfcoind R-DIV _ prems

  progress : ∀{e} →(∀{i} → (e ⇓ div) i) → Σ[ e' ∈ Term 0 ] (e ⇒ e')
  progress {e} bs with bs
  progress  bs | sfold (APP , _ , refl , prem) with bs-sound-v (prem zero .force)
  progress  bs | sfold (APP , ((_ , e1' , _ , _ , .div) , _) , refl , prem) | ε with bs-sound-v (prem (suc zero) .force)
  progress  bs | sfold (APP , ((.(lambda e1') , e1' , _ , v , .div) , _) , refl , prem) | ε | ε =
    _ , apply-ind β _ λ ()
  progress  bs | sfold (APP , ((.(lambda e1') , e1' , e2 , _ , .div) , _) , refl , prem) | ε | x ◅ _ =
    app (lambda e1') _ , apply-ind R-APP _ λ{zero → x}
  progress  bs | sfold (APP , ((e1 , _ , e2 , _ , .div) , _) , refl , prem) | x ◅ _ =
    app _ e2 , apply-ind L-APP _ λ{zero → x}
  progress  bs | sfold (L-DIV , ((e1 , e2) , _) , refl , prem) =
    let e1' , e1⇒e1' = progress (prem zero .force) in
    app e1' e2 , apply-ind L-APP _ λ{zero → e1⇒e1'}
  progress  bs | sfold (R-DIV , ((e1 , e2 , v) , _) , refl , prem) with bs-sound-v (prem zero .force)
  progress  bs | sfold (R-DIV , ((.(term _) , e2 , (lambda e)) , _) , refl , prem) | ε =
    let e2' , e2⇒e2' = progress (prem (suc zero) .force) in
    app (lambda e) e2' , apply-ind R-APP _ λ{zero → e2⇒e2'}
  progress  bs | sfold (R-DIV , ((e1 , e2 , (lambda e)) , _) , refl , prem) | x ◅ _ =
    app _ e2 , apply-ind L-APP _ λ{zero → x}

  bs-sound-∞ : ∀{e} → (∀{i} → (e ⇓ div) i) → (∀{i} → ⇒∞ e i)
  bs-sound-∞ bs with progress bs
  ... | e' , ss = step ss λ where .force → bs-sound-∞ (subject-red-⇓ bs ss)

  bs-sound : ∀{e v} → (∀{i} → (e ⇓ v) i) → Spec (e , v)
  bs-sound {_} {res _} = bs-sound-v
  bs-sound {_} {div} = bs-sound-∞

  {- Completeness -}
  inv-app : ∀{e1 e2 v} → (app e1 e2) ⇓ᵢ (res v) →
    Σ[ e1' ∈ Term 1 ] Σ[ e2' ∈ Value ]
      (e1 ⇓ᵢ res (lambda e1')) ×
      (e2 ⇓ᵢ (res e2')) ×
      (subst-0 e1' (term e2') ⇓ᵢ res v)
  -- Using consistency of inductive interpretation
  inv-app bs with ind-postfix bs
  inv-app bs | inj₁ VAL , lambda _ , () , _
  inv-app bs | inj₁ APP , _ , refl , pr = _ , _ , pr zero , pr (suc zero) , pr (suc (suc zero))
  inv-app bs | inj₂ COA , _ , () , _

  subject-exp : ∀{e e' v} → e ⇒ e' → e' ⇓ᵢ v → e ⇓ᵢ v
  subject-exp {.(app (lambda e1) (term v))} {_} {v'} (fold (β , (e1 , v) , refl , _)) bs =
    let prem-e1 = IS.fold (inj₁ VAL , lambda e1 , refl , λ ()) in
    let prem-e2 = IS.fold (inj₁ VAL , v , refl , λ ()) in
    let prems = λ{zero → prem-e1 ; (suc zero) → prem-e2 ; (suc (suc zero)) → bs} in
    apply-ind (inj₁ APP) _ prems
  subject-exp {.(app e1 e2)} {.(app e1' e2)} {res x} (fold (L-APP , (e1 , e1' , e2) , refl , pr)) bs =
    let e1'' , e2' , bs-e1' , bs-e2 , bs-subst = inv-app bs in
    let prems = λ{zero → subject-exp (pr zero) bs-e1' ; (suc zero) → bs-e2 ; (suc (suc zero)) → bs-subst} in
    apply-ind (inj₁ APP) _ prems
  subject-exp {.(app e1 e2)} {.(app e1' e2)} {div} (fold (L-APP , (e1 , e1' , e2) , refl , pr)) bs =
    apply-ind (inj₂ COA) _ λ ()
  subject-exp {.(app (term v) e2)} {.(app (term v) e2')} {res x} (fold (R-APP , (v , e2 , e2') , refl , pr)) bs =
    let e1' , e2'' , bs-e1 , bs-e2' , bs-subst = inv-app bs in
    let prems = λ{zero → bs-e1 ; (suc zero) → subject-exp (pr zero) bs-e2' ; (suc (suc zero)) → bs-subst} in
    apply-ind (inj₁ APP) _ prems
  subject-exp {.(app (term v) e2)} {.(app (term v) e2')} {div} (fold (R-APP , (v , e2 , e2') , refl , _)) bs =
    apply-ind (inj₂ COA) _ λ ()

  bounded-v : ∀{e v} → e ⇒* term v → e ⇓ᵢ res v
  bounded-v ε = apply-ind (inj₁ VAL) _ λ ()
  bounded-v (x ◅ ss) = subject-exp x (bounded-v ss)

  bounded-∞ : ∀{e} → (∀{i} → ⇒∞ e i) → e ⇓ᵢ div
  bounded-∞ {e} ss = apply-ind (inj₂ COA) _ λ ()

  bounded : ∀{e v} → Spec (e , v) → e ⇓ᵢ v
  bounded {_} {res _} = bounded-v
  bounded {_} {div} = bounded-∞

  get-prem-cons : ∀{e1 e2 v} → app e1 e2 ⇒* (term v) →
    Σ[ e1' ∈ Term 1 ] Σ[ e2' ∈ Value ]
      (e1 ⇒* lambda e1') ×
      (e2 ⇒* term e2') ×
      (subst-0 e1' (term e2') ⇒* (term v))
  get-prem-cons {.(lambda e1)} {.(term v)} {lambda _} (fold (β , (e1 , v) , refl , _) ◅ ss) =
    e1 , v , ε , ε , ss
  get-prem-cons {.e1} {.e2} {lambda _} (fold (L-APP , (e1 , e1' , e2) , refl , pr) ◅ ss) =
    let e1'' , e2' , rec-e1' , rec-e2 , rec-subst = get-prem-cons ss in
    e1'' , e2' , pr zero ◅ rec-e1' , rec-e2 , rec-subst
  get-prem-cons {.(term v)} {.e2} {lambda _} (fold (R-APP , (v , e2 , e2') , refl , pr) ◅ ss) =
    let e1' , e2'' , rec-e1 , rec-e2' , rec-subst = get-prem-cons ss in
    e1' , e2'' , rec-e1 , pr zero ◅ rec-e2' , rec-subst

  consistent-v : ∀{e v} → e ⇒* term v → IS.ISF[ BigStepIS ] Spec (e , res v)
  consistent-v {.(lambda _)} {lambda _} ε = VAL , _ , refl , λ ()
  consistent-v {lambda _} {lambda _} (x ◅ ss) = ⊥-elim (val-not-reduce⇒ x)
  consistent-v {app e1 e2} {lambda _} (x ◅ ss) =
    let e1' , e2' , e1⇒* , e2⇒* , subst⇒* = get-prem-cons (x ◅ ss) in
    let prems = λ{zero → e1⇒* ; (suc zero) → e2⇒* ; (suc (suc zero)) → subst⇒*} in
    APP , (e1 , e1' , e2 , e2' , _) , refl , prems

  postulate
    excluded-middle : ExcludedMiddle ∅

  lemma-divergence : ∀{e1 e2} → (∀{i} → ⇒∞ (app e1 e2) i) →
    (∀{i} → ⇒∞ e1 i) ⊎
    e1 ConvergesSS × (∀{i} → ⇒∞ e2 i) ⊎
    Σ[ t1 ∈ Term 1 ] Σ[ v ∈ Value ] (e1 ⇒* lambda t1) × (e2 ⇒* term v) × (∀{i} → ⇒∞ (subst-0 t1 (term v)) i)
  lemma-divergence {e1} {e2} ss with excluded-middle {e1 ConvergesSS}
  lemma-divergence {e1} {e2} ss | no ¬e1-conv = inj₁ (div-app-l-not-conv ss ¬e1-conv)
  lemma-divergence {e1} {e2} ss | yes e1-conv with excluded-middle {e2 ConvergesSS}
  lemma-divergence {e1} {e2} ss | yes e1-conv | no ¬e2-conv =
    inj₂ (inj₁ (e1-conv , div-app-r-not-conv ss (proj₂ e1-conv) ¬e2-conv))
  lemma-divergence {e1} {e2} ss | yes (lambda _ , red-e1) | yes (_ , red-e2) =
    inj₂ (inj₂ (_ , _ , ( red-e1 , red-e2 , app-subst-⇒∞₁ red-e1 red-e2 ss)))

  consistent-∞ : ∀{e} → (∀{i} → ⇒∞ e i) → IS.ISF[ BigStepIS ] Spec (e , div)
  consistent-∞ {e} ss with ss
  consistent-∞ {lambda e} ss | step x _ = ⊥-elim (val-not-reduce⇒ x)
  consistent-∞ {app e₁ e₂} ss | step x x₁ with lemma-divergence (step x x₁)
  consistent-∞ {app e₁ e₂} ss | step x x₁ | inj₁ e1-div =
    L-DIV , _ , refl , λ{zero → e1-div}
  consistent-∞ {app e₁ e₂} ss | step x x₁ | inj₂ (inj₁ (e1-conv , e2-div)) =
    R-DIV , _ , refl , λ{zero → proj₂ e1-conv ; (suc zero) → e2-div}
  consistent-∞ {app e₁ e₂} ss | step x x₁ | inj₂ (inj₂ (_ , _ , red-e1 , red-e2 , subst-div)) =
    APP , _ , refl , λ{zero → red-e1 ; (suc zero) → red-e2 ; (suc (suc zero)) → subst-div}

  consistent : ∀{e v} → Spec (e , v) → IS.ISF[ BigStepIS ] Spec (e , v)
  consistent {_} {res _} = consistent-v
  consistent {_} {div} = consistent-∞

  complete : ∀{e v} → Spec (e , v) → (∀{i} → (e ⇓ v) i)
  complete = bounded-scoind[ BigStepIS , BigStepCOIS ] Spec bounded consistent

ext: agda

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


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

module Container.Polynomial where

open import Prelude hiding (id; const; _×_; Π; _⊎_; Σ; _∘_; ⊤; ⊥)

open import Data.Unit.UniversePolymorphic
open import Data.Empty.UniversePolymorphic

import Prelude as P
open import Container

module _ {s p : Level} where

  id : Container s p
  id .fst = ⊤
  id .snd _ = ⊤

  const : Type s → Container s p
  const X .fst = X
  const X .snd _ = ⊥

infixr 9 _∘_

_∘_ : ∀ {s₁ s₂ p₁ p₂} → Container s₁ p₁ → Container s₂ p₂ →
      Container (s₁ ℓ⊔ s₂ ℓ⊔ p₁) (p₁ ℓ⊔ p₂)
(C₁ ∘ C₂) .fst = ⟦ C₁ ⟧ (fst C₂)
(C₁ ∘ C₂) .snd cx = ∃ x × (snd C₂ P.∘ snd cx) x

infixr 2 _×_

_×_ : ∀ {s₁ s₂ p₁ p₂} → Container s₁ p₁ → Container s₂ p₂ →
      Container (s₁ ℓ⊔ s₂) (p₁ ℓ⊔ p₂)
(C₁ × C₂) .fst = fst C₁ P.× fst C₂
(C₁ × C₂) .snd = P.uncurry λ s₁ s₂ → (snd C₁ s₁) P.⊎ (snd C₂ s₂)

Π : ∀ {i s p} (I : Type i) → (I → Container s p) → Container (i ℓ⊔ s) (i ℓ⊔ p)
Π I C .fst = ∀ i → fst (C i)
Π I C .snd = λ s → ∃ i × snd (C i) (s i)

infix 0 const[_]⟶_

const[_]⟶_ : ∀ {i s p} → Type i → Container s p → Container (i ℓ⊔ s) (i ℓ⊔ p)
const[ X ]⟶ C = Π X (P.const C)

infixr 1 _⊎_

_⊎_ : ∀ {s₁ s₂ p} → Container s₁ p → Container s₂ p → Container (s₁ ℓ⊔ s₂) p
(C₁ ⊎ C₂) .fst = (fst C₁ P.⊎ fst C₂)
(C₁ ⊎ C₂) .snd = either (snd C₁) (snd C₂)

Σ : ∀ {i s p} (I : Type i) → (I → Container s p) → Container (i ℓ⊔ s) p
Σ I C .fst = ∃ i × fst (C i)
Σ I C .snd s = snd (C (fst s)) (snd s)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Data.Collection.Core.Properties where

-- open import Data.List public using (List; []; _∷_)
-- open import Data.String public using (String; _≟_)
-- open import Level using (zero)
--
-- open import Function using (flip)
-- open import Relation.Nullary
-- open import Relation.Nullary.Negation
-- open import Relation.Nullary.Decidable renaming (map to mapDec; map′ to mapDec′)
-- open import Relation.Unary
-- open import Relation.Binary
-- open import Relation.Binary.PropositionalEquality

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
{-
  Mathematical Foundations of Programming (G54FOP)
  Nicolai Kraus
  Lecture 3, 7 Feb 2018

  ====================
  INTRODUCTION TO AGDA
  ====================

  Your G54FPP project could involve Agda. If you want.

  Btw, text in {- -} is a comment. So is text after --.

  links to help you install and learn Agda:
  http://wiki.portal.chalmers.se/agda/pmwiki.php
  http://agda.readthedocs.io/en/latest/getting-started/index.html
  https://github.com/agda/agda

  Agda standard library:
  https://github.com/agda/agda-stdlib

  Some key combinations, where C is ctrl,
  i.e. C-c C-l means:
    press control and keep it pressed,
    press and release c,
    press and release l,
    release control.
  C-c C-l   load file, replace ? by hole
  C-c C-,   show goal
  C-c C-.   show goal and input type
  C-c C-n   normalise expression
  C-c C-space   give current hole input to Agda
  see links above for more

  I recommend using a monospace font.
-}

module lec3FOP where

  data ℕ : Set where     -- type: \bN
    zero : ℕ
    suc : ℕ → ℕ          -- type: \to or \->
                         -- (or just use ->)

  infix 6 _+_
  _+_ : ℕ → ℕ → ℕ        -- the arguments go where _ is
  zero + n = n
  (suc m) + n = suc (m + n)

  {- type of equalities on natural numbers *which
     we need to prove*. Some equalities can be hard
     to prove, so we cannot assume that Agda would
     find them automatically! -}
  infix 3 _==_
  data _==_ : (m n : ℕ) → Set where
    refl : {m : ℕ} → m == m

  suc-lem : {m n : ℕ} → m == n → suc m == suc n
  suc-lem refl = refl

  +-is-associative : (k m n : ℕ)
      → k + (m + n) == (k + m) + n
  +-is-associative zero m n = refl
  +-is-associative (suc k) m n =
      suc-lem (+-is-associative k m n)

  {- Next: implement the language of expressions
     from the lecture
     This language was given by a BNF:
     E:= t | f | z | s E | p E | iz E | if E then E else E
  -}

  data Expr : Set where
    t : Expr
    f : Expr
    z : Expr
    s : Expr → Expr
    p : Expr → Expr
    iz : Expr → Expr
    if_then_else_ : Expr → Expr → Expr → Expr

  -- denotational semantics from last week:
  -- ⟦_⟧ : Expr → S       type: \[[_\]]
  -- S was {True, False, 0, 1, 2, ..., ⊥}

  data Bool : Set where
    True : Bool
    False : Bool

  data S : Set where
    bool : Bool → S
    number : ℕ → S
    ⊥ : S

  -- Here we go:
  ⟦_⟧ : Expr → S
  ⟦ t ⟧ = bool True
  ⟦ f ⟧ = bool False
  ⟦ z ⟧ = number zero
  ⟦ s e ⟧ with ⟦ e ⟧
  ⟦ s e ⟧ | number n = number (suc n)
  ⟦ s e ⟧ | _ = ⊥
  ⟦ _ ⟧ = ⊥  -- not what we want, but
             -- at least Agda accepts it.
             -- Exercise: complete this definition.


text:
------------------------------------------------------------------------------
-- Common definitions
------------------------------------------------------------------------------

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

module Common.DefinitionsI where

open import Common.FOL.FOL using ( ¬_ ; D )
open import Common.FOL.Relation.Binary.PropositionalEquality using ( _≡_ )

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Relation/Binary/Core.agda).
infix 7 _≢_

------------------------------------------------------------------------------
-- Inequality.
_≢_ : D → D → Set
x ≢ y = ¬ x ≡ y

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}
module Model.Stream where

open import Model.Size as MS using
  ( Size ; Sizes ; _≤_ ; _<_ ; ≤-IsProp ; ≤-trans ; nat )
open import Model.Type.Core
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.Prelude

import Data.Nat.Properties as ℕ

open Size

Colist : Size → Set
Colist n = ∀ m → nat m ≤ n → ℕ

abstract
  Colist-≡⁺ : ∀ {n} {xs ys : Colist n}
    → (∀ m m≤n → xs m m≤n ≡ ys m m≤n)
    → xs ≡ ys
  Colist-≡⁺ eq = funext λ m → funext λ m≤n → eq m m≤n

  Colist-≡⁻ : ∀ {n} {xs ys : Colist n}
    → xs ≡ ys
    → ∀ m m≤n₀ m≤n₁ → xs m m≤n₀ ≡ ys m m≤n₁
  Colist-≡⁻ {xs = xs} refl m m≤n₀ m≤n₁ = cong (xs m) (≤-IsProp _ _)

  Colist-IsSet : ∀ {n} → IsSet (Colist n)
  Colist-IsSet = ∀-IsSet λ m → ∀-IsSet λ m≤n → ℕ.≡-irrelevant

castColist : ∀ {n m} → n ≤ m → Colist m → Colist n
castColist n≤m xs k k≤n = xs k go
  where abstract go = ≤-trans k≤n n≤m

Stream : ⟦Type⟧ Sizes
Stream = record
  { ObjHSet = λ n → HLevel⁺ (Colist n) Colist-IsSet
  ; eqHProp = λ {n} {n′} _ xs ys
      → ∀-HProp ℕ λ m → ∀-HProp (nat m ≤ n) λ m≤n → ∀-HProp (nat m ≤ n′) λ m≤n′
      → HLevel⁺ (xs m m≤n ≡ ys m m≤n′) ℕ.≡-irrelevant
  ; eq-refl = λ x m m≤n m≤n′ → cong (x m) (≤-IsProp _ _)
  }

cons : ∀ {n} → ℕ → (∀ m → m < n → Colist m) → Colist n
cons x xs zero _ = x
cons x xs (suc k) Sk≤n = xs (nat k) go k MS.≤-refl
  where abstract go = MS.Sn≤m→n<m Sk≤n

head : ∀ {n} → Colist n → ℕ
head xs = xs 0 MS.0≤n

tail : ∀ {n} → Colist n → ∀ m → m < n → Colist m
tail xs m m<n k k≤m = xs (suc k) go
  where abstract go = MS.n<m→Sn≤m (MS.≤→<→< k≤m m<n)

abstract
  cons-≡⁺ : ∀ {n n′ i i′ is is′}
    → i ≡ i′
    → (∀ m (m<n : m < n) (m<n′ : m < n′) k k≤m
        → is m m<n k k≤m ≡ is′ m m<n′ k k≤m)
    → ∀ m m<n m<n′
    → cons i is m m<n ≡ cons i′ is′ m m<n′
  cons-≡⁺ i≡i′ is≡is′ zero m<n₀ m<n₁ = i≡i′
  cons-≡⁺ {is′ = is′} i≡i′ is≡is′ (suc m) m<n m<n′
    = trans (is≡is′ (nat m) (MS.Sn≤m→n<m m<n) (MS.Sn≤m→n<m m<n′) m MS.≤-refl)
        (cong (λ p → is′ _ p _ _) (MS.<-IsProp _ _))

  head-≡⁺ : ∀ {n n′ is is′}
    → (∀ m (m≤n : nat m ≤ n) (m≤n′ : nat m ≤ n′) → is m m≤n ≡ is′ m m≤n′)
    → head is ≡ head is′
  head-≡⁺ is≡is′ = is≡is′ 0 MS.0≤n MS.0≤n

  tail-≡⁺ : ∀ {n n′ is is′}
    → (∀ m (m≤n : nat m ≤ n) (m≤n′ : nat m ≤ n′)
        → is m m≤n ≡ is′ m m≤n′)
    → ∀ m m′ m<n m′<n′ k k≤m k≤m′
    → tail is m m<n k k≤m ≡ tail is′ m′ m′<n′ k k≤m′
  tail-≡⁺ {is′ = is′} is≡is′ m m′ m<n m′<n′ k k≤m k≤m′
    = trans (is≡is′ (suc k) _ (MS.n<m→Sn≤m (MS.≤→<→< k≤m′ m′<n′)))
        (cong (is′ (suc k)) (≤-IsProp _ _))

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------
-- Some cancellation lemmas
------------------------------------------------------------------------

open import Atom

module Cancellation (atoms : χ-atoms) where

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

open import Chi    atoms
open import Values atoms

cancel-const :
  ∀ {c₁ c₂ es₁ es₂} →
  Exp.const c₁ es₁ ≡ const c₂ es₂ →
  c₁ ≡ c₂ × es₁ ≡ es₂
cancel-const refl = refl , refl

cancel-lambda :
  ∀ {x₁ x₂ e₁ e₂} →
  Exp.lambda x₁ e₁ ≡ lambda x₂ e₂ →
  x₁ ≡ x₂ × e₁ ≡ e₂
cancel-lambda refl = refl , refl

cancel-rec :
  ∀ {x₁ x₂ e₁ e₂} →
  Exp.rec x₁ e₁ ≡ rec x₂ e₂ →
  x₁ ≡ x₂ × e₁ ≡ e₂
cancel-rec refl = refl , refl

cancel-apply :
  ∀ {e₁₁ e₁₂ e₂₁ e₂₂} →
  Exp.apply e₁₁ e₂₁ ≡ apply e₁₂ e₂₂ →
  e₁₁ ≡ e₁₂ × e₂₁ ≡ e₂₂
cancel-apply refl = refl , refl

cancel-case :
  ∀ {e₁ e₂ bs₁ bs₂} →
  Exp.case e₁ bs₁ ≡ case e₂ bs₂ →
  e₁ ≡ e₂ × bs₁ ≡ bs₂
cancel-case refl = refl , refl

cancel-var :
  ∀ {x₁ x₂} →
  Exp.var x₁ ≡ var x₂ → x₁ ≡ x₂
cancel-var refl = refl

cancel-branch :
  ∀ {c₁ c₂ xs₁ xs₂ e₁ e₂} →
  Br.branch c₁ xs₁ e₁ ≡ branch c₂ xs₂ e₂ →
  c₁ ≡ c₂ × xs₁ ≡ xs₂ × e₁ ≡ e₂
cancel-branch refl = refl , refl , refl

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
{-# OPTIONS --safe #-}
{-
This file models "ZF - powerset" in cubical agda, via a cumulative hierarchy, in the sense given
in the HoTT book §10.5 "The cumulative hierarchy".

A great amount of inspiration is taken from the Coq implementations found in
Jérémy Ledent, Modeling set theory in homotopy type theory, code of which can be found online at
https://github.com/jledent/vset
-}

module Cubical.HITs.CumulativeHierarchy.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv using (fiber)
open import Cubical.Functions.Logic
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as P hiding (elim; elim2)

import Cubical.HITs.PropositionalTruncation.Monad as PropMonad

private
  variable
    ℓ ℓ' : Level

infix 5 _∈_

-- set up the basic hierarchy definition and _∈_ as recursive, higher inductive types
data V (ℓ : Level) : Type (ℓ-suc ℓ)
_∈_ : (S T : V ℓ) → hProp (ℓ-suc ℓ)

eqImage : {X Y : Type ℓ} (ix : X → V ℓ) (iy : Y → V ℓ) → Type (ℓ-suc ℓ)
eqImage {X = X} {Y = Y} ix iy = (∀ (a : X) → ∥ fiber iy (ix a) ∥₁) ⊓′
                                (∀ (b : Y) → ∥ fiber ix (iy b) ∥₁)

data V ℓ where
  sett : (X : Type ℓ) → (X → V ℓ) → V ℓ
  seteq : (X Y : Type ℓ) (ix : X → V ℓ) (iy : Y → V ℓ) (eq : eqImage ix iy) → sett X ix ≡ sett Y iy
  setIsSet : isSet (V ℓ)

A ∈ sett X ix = ∥ Σ[ i ∈ X ] (ix i ≡ A) ∥ₚ
A ∈ seteq X Y ix iy (f , g) i =
  ⇔toPath {P = A ∈ sett X ix} {Q = A ∈ sett Y iy}
    (λ ax → do (x , xa) ← ax ; (y , ya) ← f x ; ∣ y , ya ∙ xa ∣₁)
    (λ ay → do (y , ya) ← ay ; (x , xa) ← g y ; ∣ x , xa ∙ ya ∣₁) i
  where open PropMonad
A ∈ setIsSet a b p q i j = isSetHProp (A ∈ a) (A ∈ b) (λ j → A ∈ p j) (λ j → A ∈ q j) i j

-- setup a general eliminator into h-sets
record ElimSet {Z : (s : V ℓ) → Type ℓ'}
               (isSetZ : ∀ s → isSet (Z s)) : Type (ℓ-max ℓ' (ℓ-suc ℓ)) where
  field
    ElimSett :
      ∀ (X : Type ℓ) (ix : X → V ℓ)
      -- ^ the structural parts of the set
      → (rec : ∀ x → Z (ix x))
      -- ^ a recursor into the elements
      → Z (sett X ix)
    ElimEq :
      ∀ (X₁ X₂ : Type ℓ) (ix₁ : X₁ → V ℓ) (ix₂ : X₂ → V ℓ) (eq : eqImage ix₁ ix₂)
      -- ^ the structural parts of the seteq path
      → (rc₁ : ∀ x₁ → Z (ix₁ x₁)) (rc₂ : ∀ x₂ → Z (ix₂ x₂))
      -- ^ recursors into the elements
      → ((x₁ : X₁) → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ] PathP (λ i → Z (p i)) (rc₂ x₂) (rc₁ x₁))
      → ((x₂ : X₂) → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ] PathP (λ i → Z (p i)) (rc₁ x₁) (rc₂ x₂))
      -- ^ proofs that the recursors have equal images
      → PathP (λ i → Z (seteq X₁ X₂ ix₁ ix₂ eq i)) (ElimSett X₁ ix₁ rc₁) (ElimSett X₂ ix₂ rc₂)

module _ {Z : (s : V ℓ) → Type ℓ'} {isSetZ : ∀ s → isSet (Z s)} (E : ElimSet isSetZ) where
  open ElimSet E
  elim : (s : V ℓ) → Z s
  elim (sett X ix) = ElimSett X ix (elim ∘ ix)
  elim (seteq X₁ X₂ ix₁ ix₂ eq i) =
    ElimEq X₁ X₂ ix₁ ix₂ eq (elim ∘ ix₁) (elim ∘ ix₂) rec₁→₂ rec₂→₁ i
    where
    rec₁→₂ :
      ∀ (x₁ : X₁)
      → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ] PathP (λ i → Z (p i)) (elim (ix₂ x₂)) (elim (ix₁ x₁))
    rec₂→₁ :
      ∀ (x₂ : X₂)
      → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ] PathP (λ i → Z (p i)) (elim (ix₁ x₁)) (elim (ix₂ x₂))
    -- using a local definition of Prop.rec satisfies the termination checker
    rec₁→₂ x₁ = localRec₁ (eq .fst x₁) where
      localRec₁ :
          ∥ fiber ix₂ (ix₁ x₁) ∥₁
        → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ] PathP (λ i → Z (p i)) (elim (ix₂ x₂)) (elim (ix₁ x₁))
      localRec₁ ∣ x₂ , xx ∣₁ = ∣ (x₂ , xx) , (λ i → elim (xx i)) ∣₁
      localRec₁ (squash₁ x y i) = squash₁ (localRec₁ x) (localRec₁ y) i
    rec₂→₁ x₂ = localRec₂ (eq .snd x₂) where
      localRec₂ :
          ∥ fiber ix₁ (ix₂ x₂) ∥₁
        → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ] PathP (λ i → Z (p i)) (elim (ix₁ x₁)) (elim (ix₂ x₂))
      localRec₂ ∣ x₁ , xx ∣₁ = ∣ (x₁ , xx) , (λ i → elim (xx i)) ∣₁
      localRec₂ (squash₁ x y i) = squash₁ (localRec₂ x) (localRec₂ y) i
  elim (setIsSet S T x y i j) = isProp→PathP propPathP (cong elim x) (cong elim y) i j where
    propPathP : (i : I) → isProp (PathP (λ j → Z (setIsSet S T x y i j)) (elim S) (elim T))
    propPathP _ = subst isProp (sym (PathP≡Path _ _ _)) (isSetZ _ _ _)

-- eliminator into propositions
elimProp : {Z : (s : V ℓ) → Type ℓ'} (isPropZ : ∀ s → isProp (Z s))
         → ((X : Type ℓ) → (ix : X → V ℓ) → (∀ x → Z (ix x)) → Z (sett X ix))
         → (s : V ℓ) → Z s
elimProp isPropZ algz (sett X ix) = algz X ix (λ x → elimProp isPropZ algz (ix x))
elimProp isPropZ algz (seteq X Y ix iy eq i) =
  isProp→PathP (λ i → isPropZ (seteq X Y ix iy eq i))
               (algz X ix (elimProp isPropZ algz ∘ ix))
               (algz Y iy (elimProp isPropZ algz ∘ iy)) i
elimProp isPropZ algz (setIsSet S T x y i j) =
  isProp→SquareP (λ i j → isPropZ (setIsSet S T x y i j))
                 (λ _ → elimProp isPropZ algz S)
                 (λ _ → elimProp isPropZ algz T)
                 (cong (elimProp isPropZ algz) x)
                 (cong (elimProp isPropZ algz) y) i j

-- eliminator for two sets at once
record Elim2Set {Z : (s t : V ℓ) → Type ℓ'}
                (isSetZ : ∀ s t → isSet (Z s t)) : Type (ℓ-max ℓ' (ℓ-suc ℓ)) where
  field
    ElimSett2 :
      ∀ (X : Type ℓ) (ix : X → V ℓ) (Y : Type ℓ) (iy : Y → V ℓ)
      -- ^ the structural parts of the set
      → (rec : ∀ x y → Z (ix x) (iy y))
      -- ^ a recursor into the elements
      → Z (sett X ix) (sett Y iy)
    -- path when the the first argument deforms along seteq and the second argument is held constant
    ElimEqFst :
      ∀ (X₁ X₂ : Type ℓ) (ix₁ : X₁ → V ℓ) (ix₂ : X₂ → V ℓ) (eq : eqImage ix₁ ix₂)
      -- ^ the structural parts of the seteq path
      → (Y : Type ℓ) (iy : Y → V ℓ)
      -- ^ the second argument held constant
      → (rec₁ : ∀ x₁ y → Z (ix₁ x₁) (iy y)) (rec₂ : ∀ x₂ y → Z (ix₂ x₂) (iy y))
      -- ^ recursors into the elements
      → (rec₁→₂ : (x₁ : X₁)
                → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ]
                     PathP (λ i → ∀ y → Z (p i) (iy y)) (λ y → rec₂ x₂ y) (λ y → rec₁ x₁ y))
      → (rec₂→₁ : (x₂ : X₂)
                → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ]
                     PathP (λ i → ∀ y → Z (p i) (iy y)) (λ y → rec₁ x₁ y) (λ y → rec₂ x₂ y))
      -- ^ proofs that the recursors have equal images
      → PathP (λ i → Z (seteq X₁ X₂ ix₁ ix₂ eq i) (sett Y iy))
              (ElimSett2 X₁ ix₁ Y iy rec₁)
              (ElimSett2 X₂ ix₂ Y iy rec₂)
    -- path when the the second argument deforms along seteq and the first argument is held constant
    ElimEqSnd :
      ∀ (X : Type ℓ) (ix : X → V ℓ)
      -- ^ the first argument held constant
      → (Y₁ Y₂ : Type ℓ) (iy₁ : Y₁ → V ℓ) (iy₂ : Y₂ → V ℓ) → (eq : eqImage iy₁ iy₂)
      -- ^ the structural parts of the seteq path
      → (rec₁ : ∀ x y₁ → Z (ix x) (iy₁ y₁)) (rec₂ : ∀ x y₂ → Z (ix x) (iy₂ y₂))
      -- ^ recursors into the elements
      → (rec₁→₂ : (y₁ : Y₁)
                → ∃[ (y₂ , p) ∈ fiber iy₂ (iy₁ y₁) ]
                     PathP (λ i → ∀ x → Z (ix x) (p i)) (λ x → rec₂ x y₂) (λ x → rec₁ x y₁))
      → (rec₂→₁ : (y₂ : Y₂)
                → ∃[ (y₁ , p) ∈ fiber iy₁ (iy₂ y₂) ]
                     PathP (λ i → ∀ x → Z (ix x) (p i)) (λ x → rec₁ x y₁) (λ x → rec₂ x y₂))
      -- ^ proofs that the recursors have equal images
      → PathP (λ i → Z (sett X ix) (seteq Y₁ Y₂ iy₁ iy₂ eq i))
              (ElimSett2 X ix Y₁ iy₁ rec₁)
              (ElimSett2 X ix Y₂ iy₂ rec₂)

module _ {Z : (s t : V ℓ) → Type ℓ'} {isSetZ : ∀ s t → isSet (Z s t)} (E : Elim2Set isSetZ) where
  open Elim2Set E
  open ElimSet

  elim2 : (s t : V ℓ) → Z s t
  elim2 = elim pElim where
    open PropMonad

    isSetPElim : ∀ s → isSet (∀ t → Z s t)
    isSetPElim s = isSetΠ (isSetZ s)

    eliminatorImplX : (X : Type ℓ) (ix : X → V ℓ)
                    → (rec : ∀ x y → Z (ix x) y)
                    → ElimSet (λ t → isSetZ (sett X ix) t)
    ElimSett (eliminatorImplX X ix rec) Y iy _ =
      ElimSett2 X ix Y iy (λ x → rec x ∘ iy)
    ElimEq (eliminatorImplX X ix rec) Y₁ Y₂ iy₁ iy₂ eq _ _ _ _ =
      ElimEqSnd X ix Y₁ Y₂ iy₁ iy₂ eq (λ x → rec x ∘ iy₁) (λ x → rec x ∘ iy₂) rec₁→₂ rec₂→₁
      where
      rec₁→₂ :
        ∀ (y₁ : Y₁)
        → ∃[ (y₂ , p) ∈ fiber iy₂ (iy₁ y₁) ]
             PathP (λ i → ∀ x → Z (ix x) (p i)) (λ x → rec x (iy₂ y₂)) (λ x → rec x (iy₁ y₁))
      rec₂→₁ :
        ∀ (y₂ : Y₂)
        → ∃[ (y₁ , p) ∈ fiber iy₁ (iy₂ y₂) ]
             PathP (λ i → ∀ x → Z (ix x) (p i)) (λ x → rec x (iy₁ y₁)) (λ x → rec x (iy₂ y₂))
      rec₁→₂ y₁ = do (y₂ , yy) ← fst eq y₁ ; ∣ (y₂ , yy) , (λ i x → rec x (yy i)) ∣₁
      rec₂→₁ y₂ = do (y₁ , yy) ← snd eq y₂ ; ∣ (y₁ , yy) , (λ i x → rec x (yy i)) ∣₁

    elimImplS :
      ∀ (X : Type ℓ) (ix : X → V ℓ)
      → (∀ x t₂ → Z (ix x) t₂)
      → (t : V ℓ) → Z (sett X ix) t
    elimImplS X ix rec = elim (eliminatorImplX X ix rec)

    elimImplSExt :
      ∀ (X₁ X₂ : Type ℓ) (ix₁ : X₁ → V ℓ) (ix₂ : X₂ → V ℓ) → (eq : eqImage ix₁ ix₂)
      → (rec₁ : ∀ x₁ t₂ → Z (ix₁ x₁) t₂) (rec₂ : ∀ x₂ t₂ → Z (ix₂ x₂) t₂)
      → ((x₁ : X₁) → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ]
                        PathP (λ i → ∀ t → Z (p i) t) (rec₂ x₂) (rec₁ x₁))
      → ((x₂ : X₂) → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ]
                        PathP (λ i → ∀ t → Z (p i) t) (rec₁ x₁) (rec₂ x₂))
      → (t : V ℓ)
      → PathP (λ i → Z (seteq X₁ X₂ ix₁ ix₂ eq i) t)
              (elimImplS X₁ ix₁ rec₁ t)
              (elimImplS X₂ ix₂ rec₂ t)
    elimImplSExt X₁ X₂ ix₁ ix₂ eq rec₁ rec₂ rec₁→₂ rec₂→₁ =
      elimProp propPathP (λ Y iy _ → elimImplSExtT Y iy)
      where
      propPathP : (t : V ℓ)
                → isProp (PathP (λ i → Z (seteq X₁ X₂ ix₁ ix₂ eq i) t)
                                (elimImplS X₁ ix₁ rec₁ t)
                                (elimImplS X₂ ix₂ rec₂ t))
      propPathP _ = subst isProp (sym (PathP≡Path _ _ _)) (isSetZ _ _ _ _)

      elimImplSExtT : (Y : Type ℓ) (iy : Y → V ℓ) → _ {- the appropriate path type -}
      elimImplSExtT Y iy =
        ElimEqFst X₁ X₂ ix₁ ix₂ eq Y iy (λ x₁ y → rec₁ x₁ (iy y))
                                        (λ x₂ y → rec₂ x₂ (iy y)) rec₁→₂Impl rec₂→₁Impl
        where
        rec₁→₂Impl :
          ∀ (x₁ : X₁)
          → ∃[ (x₂ , p) ∈ fiber ix₂ (ix₁ x₁) ]
               PathP (λ i → ∀ y → Z (p i) (iy y)) (λ y → rec₂ x₂ (iy y)) (λ y → rec₁ x₁ (iy y))
        rec₂→₁Impl :
          ∀ (x₂ : X₂)
          → ∃[ (x₁ , p) ∈ fiber ix₁ (ix₂ x₂) ]
               PathP (λ i → ∀ y → Z (p i) (iy y)) (λ y → rec₁ x₁ (iy y)) (λ y → rec₂ x₂ (iy y))
        rec₁→₂Impl x₁ = do ((x₂ , xx) , rx) ← rec₁→₂ x₁ ; ∣ (x₂ , xx) , (λ i y → rx i (iy y)) ∣₁
        rec₂→₁Impl x₂ = do ((x₁ , xx) , rx) ← rec₂→₁ x₂ ; ∣ (x₁ , xx) , (λ i y → rx i (iy y)) ∣₁

    pElim : ElimSet isSetPElim
    ElimSett pElim = elimImplS
    ElimEq pElim X₁ X₂ ix₁ ix₂ eq rec₁ rec₂ rec₁→₂ rec₂→₁ i t =
      elimImplSExt X₁ X₂ ix₁ ix₂ eq rec₁ rec₂ rec₁→₂ rec₂→₁ t i

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --safe #-}
{-
  This is inspired by/copied from:
  https://github.com/agda/agda-stdlib/blob/master/src/Tactic/MonoidSolver.agda

  Boilerplate code for calling the ring solver is constructed automatically
  with agda's reflection features.
-}
module Cubical.Algebra.RingSolver.ReflectionSolving where

open import Cubical.Foundations.Prelude hiding (Type)
open import Cubical.Functions.Logic

open import Agda.Builtin.Reflection hiding (Type)
open import Agda.Builtin.String

open import Cubical.Reflection.Base

open import Cubical.Data.Maybe
open import Cubical.Data.Sigma
open import Cubical.Data.List
open import Cubical.Data.Nat.Literals
open import Cubical.Data.Int.Base hiding (abs)
open import Cubical.Data.Int using (fromNegℤ; fromNatℤ)
open import Cubical.Data.Nat using (ℕ) renaming (_+_ to _+ℕ_)
open import Cubical.Data.FinData using () renaming (zero to fzero; suc to fsuc)
open import Cubical.Data.Bool
open import Cubical.Data.Bool.SwitchStatement
open import Cubical.Data.Vec using (Vec) renaming ([] to emptyVec; _∷_ to _∷vec_) public

open import Cubical.Algebra.RingSolver.AlgebraExpression
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.RawAlgebra
open import Cubical.Algebra.RingSolver.IntAsRawRing
open import Cubical.Algebra.RingSolver.CommRingSolver renaming (solve to ringSolve)

private
  variable
    ℓ : Level

  _==_ = primQNameEquality
  {-# INLINE _==_ #-}

  record VarInfo : Type ℓ-zero where
    field
      varName : String
      varType : Arg Term
      index : ℕ

  {-
    `getLastTwoArgsOf` maps a term 'def n (z₁ ∷ … ∷ zₙ ∷ x ∷ y ∷ [])' to the pair '(x,y)'
    non-visible arguments are ignored.
  -}
  getLastTwoArgsOf : Name → Term → Maybe (Term × Term)
  getLastTwoArgsOf n' (def n xs) =
    if n == n'
    then go xs
    else nothing
      where
      go : List (Arg Term) → Maybe (Term × Term)
      go (varg x ∷ varg y ∷ []) = just (x , y)
      go (x ∷ xs)               = go xs
      go _                      = nothing
  getLastTwoArgsOf n' _ = nothing

  {-
    `getArgs` maps a term 'x ≡ y' to the pair '(x,y)'
  -}
  getArgs : Term → Maybe (Term × Term)
  getArgs = getLastTwoArgsOf (quote PathP)

  firstVisibleArg : List (Arg Term) → Maybe Term
  firstVisibleArg [] = nothing
  firstVisibleArg (varg x ∷ l) = just x
  firstVisibleArg (x ∷ l) = firstVisibleArg l

  {-
    If the solver needs to be applied during equational reasoning,
    the right hand side of the equation to solve cannot be given to
    the solver directly. The folllowing function extracts this term y
    from a more complex expression as in:
      x ≡⟨ solve ... ⟩ (y ≡⟨ ... ⟩ z ∎)
  -}
  getRhs : Term → Maybe Term
  getRhs reasoningToTheRight@(def n xs) =
    if n == (quote _∎)
    then firstVisibleArg xs
    else (if n == (quote _≡⟨_⟩_)
         then firstVisibleArg xs
         else nothing)
  getRhs _ = nothing

  private
    solverCallAsTerm : Term → Arg Term → Term → Term → Term
    solverCallAsTerm R varList lhs rhs =
      def
         (quote ringSolve)
         (varg R ∷ varg lhs ∷ varg rhs
           ∷ varList
           ∷ varg (def (quote refl) []) ∷ [])

  solverCallWithLambdas : ℕ → List VarInfo → Term → Term → Term → Term
  solverCallWithLambdas n varInfos R lhs rhs =
    encloseWithIteratedLambda
      (map VarInfo.varName varInfos)
      (solverCallAsTerm R (variableList (rev varInfos)) lhs rhs)
    where
      encloseWithIteratedLambda : List String → Term → Term
      encloseWithIteratedLambda (varName ∷ xs) t = lam visible (abs varName (encloseWithIteratedLambda xs t))
      encloseWithIteratedLambda [] t = t

      variableList : List VarInfo → Arg Term
      variableList [] = varg (con (quote emptyVec) [])
      variableList (varInfo ∷ varInfos)
        = varg (con (quote _∷vec_) (varg (var (VarInfo.index varInfo) []) ∷ (variableList varInfos) ∷ []))

  solverCallByVarIndices : ℕ → List ℕ → Term → Term → Term → Term
  solverCallByVarIndices n varIndices R lhs rhs =
      solverCallAsTerm R (variableList (rev varIndices)) lhs rhs
      where
        variableList : List ℕ → Arg Term
        variableList [] = varg (con (quote emptyVec) [])
        variableList (varIndex ∷ varIndices)
          = varg (con (quote _∷vec_) (varg (var (varIndex) []) ∷ (variableList varIndices) ∷ []))

module pr (R : CommRing ℓ) {n : ℕ} where
  private
    νR = CommRing→RawℤAlgebra R

  open CommRingStr (snd R)

  0' : Expr ℤAsRawRing (fst R) n
  0' = K 0

  1' : Expr ℤAsRawRing (fst R) n
  1' = K 1

module _ (cring : Term) where
  private
    νR = def (quote CommRing→RawℤAlgebra) (varg cring ∷ [])

  open pr

  `0` : List (Arg Term) → Term
  `0` [] = def (quote 0') (varg cring ∷ [])
  `0` (varg fstcring ∷ xs) = `0` xs
  `0` (harg _ ∷ xs) = `0` xs
  `0` _ = unknown

  `1` : List (Arg Term) → Term
  `1` [] = def (quote 1') (varg cring ∷ [])
  `1` (varg fstcring ∷ xs) = `1` xs
  `1` (harg _ ∷ xs) = `1` xs
  `1` _ = unknown

  mutual

    `_·_` : List (Arg Term) → Term
    `_·_` (harg _ ∷ xs) = `_·_` xs
    `_·_` (varg _ ∷ varg x ∷ varg y ∷ []) =
      con
        (quote _·'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
    `_·_` _ = unknown

    `_+_` : List (Arg Term) → Term
    `_+_` (harg _ ∷ xs) = `_+_` xs
    `_+_` (varg _ ∷ varg x ∷ varg y ∷ []) =
      con
        (quote _+'_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
    `_+_` _ = unknown

    `-_` : List (Arg Term) → Term
    `-_` (harg _ ∷ xs) = `-_` xs
    `-_` (varg _ ∷ varg x ∷ []) =
      con
        (quote -'_) (varg (buildExpression x) ∷ [])
    `-_` _ = unknown

    K' : List (Arg Term) → Term
    K' xs = con (quote K) xs

    finiteNumberAsTerm : ℕ → Term
    finiteNumberAsTerm ℕ.zero = con (quote fzero) []
    finiteNumberAsTerm (ℕ.suc n) = con (quote fsuc) (varg (finiteNumberAsTerm n) ∷ [])

    buildExpression : Term → Term
    buildExpression (var index _) = con (quote ∣) (varg (finiteNumberAsTerm index) ∷ [])
    buildExpression t@(def n xs) =
      switch (n ==_) cases
        case (quote CommRingStr.0r)  ⇒ `0` xs     break
        case (quote CommRingStr.1r)  ⇒ `1` xs     break
        case (quote CommRingStr._·_) ⇒ `_·_` xs   break
        case (quote CommRingStr._+_) ⇒ `_+_` xs   break
        case (quote (CommRingStr.-_))  ⇒ `-_` xs    break
        default⇒ (K' xs)
    buildExpression t@(con n xs) =
      switch (n ==_) cases
        case (quote CommRingStr.0r)  ⇒ `0` xs     break
        case (quote CommRingStr.1r)  ⇒ `1` xs     break
        case (quote CommRingStr._·_) ⇒ `_·_` xs   break
        case (quote CommRingStr._+_) ⇒ `_+_` xs   break
        case (quote (CommRingStr.-_))  ⇒ `-_` xs    break
        default⇒ (K' xs)
    buildExpression t = unknown

  toAlgebraExpression : Maybe (Term × Term) → Maybe (Term × Term)
  toAlgebraExpression nothing = nothing
  toAlgebraExpression (just (lhs , rhs)) = just (buildExpression lhs , buildExpression rhs)

private
  adjustDeBruijnIndex : (n : ℕ) → Term → Term
  adjustDeBruijnIndex n (var k args) = var (k +ℕ n) args
  adjustDeBruijnIndex n _ = unknown

  extractVarIndices : Maybe (List Term) → Maybe (List ℕ)
  extractVarIndices (just ((var index _) ∷ l)) with extractVarIndices (just l)
  ... | just indices = just (index ∷ indices)
  ... | nothing = nothing
  extractVarIndices (just []) = just []
  extractVarIndices _ = nothing

  getVarsAndEquation : Term → Maybe (List VarInfo × Term)
  getVarsAndEquation t =
    let
      (rawVars , equationTerm) = extractVars t
      maybeVars = addIndices (length rawVars) rawVars
    in map-Maybe (_, equationTerm) maybeVars
    where
          extractVars : Term → List (String × Arg Term) × Term
          extractVars (pi argType (abs varName t)) with extractVars t
          ...                                         | xs , equation
                                                        = (varName , argType) ∷ xs , equation
          extractVars equation = [] , equation

          addIndices : ℕ → List (String × Arg Term) → Maybe (List VarInfo)
          addIndices ℕ.zero         []        = just []
          addIndices (ℕ.suc countVar) ((varName , argType) ∷ list) =
            map-Maybe (λ varList → record { varName = varName ; varType = argType ; index = countVar }
                                   ∷ varList)
                      (addIndices countVar list)
          addIndices _ _ = nothing

  toListOfTerms : Term → Maybe (List Term)
  toListOfTerms (con c []) = if (c == (quote [])) then just [] else nothing
  toListOfTerms (con c (varg t ∷ varg s ∷ args)) with toListOfTerms s
  ... | just terms = if (c == (quote _∷_)) then just (t ∷ terms) else nothing
  ... | nothing = nothing
  toListOfTerms (con c (harg t ∷ args)) = toListOfTerms (con c args)
  toListOfTerms _ = nothing

  solve-macro : Term → Term → TC Unit
  solve-macro cring hole =
    do
      hole′ ← inferType hole >>= normalise
      just (varInfos , equation) ← returnTC (getVarsAndEquation hole′)
        where
          nothing
            → typeError (strErr "Something went wrong when getting the variable names in "
                           ∷ termErr hole′ ∷ [])
      {-
        The call to the ring solver will be inside a lamba-expression.
        That means, that we have to adjust the deBruijn-indices of the variables in 'cring'
      -}
      adjustedCring ← returnTC (adjustDeBruijnIndex (length varInfos) cring)
      just (lhs , rhs) ← returnTC (toAlgebraExpression adjustedCring (getArgs equation))
        where
          nothing
            → typeError(
                strErr "Error while trying to build ASTs for the equation " ∷
                termErr equation ∷ [])
      let solution = solverCallWithLambdas (length varInfos) varInfos adjustedCring lhs rhs
      unify hole solution

  solveInPlace-macro : Term → Term → Term → TC Unit
  solveInPlace-macro cring varsToSolve hole =
    do
      equation ← inferType hole >>= normalise
      just varIndices ← returnTC (extractVarIndices (toListOfTerms varsToSolve))
        where
          nothing
            → typeError(
                strErr "Error reading variables to solve " ∷
                termErr varsToSolve ∷ [])
      just (lhs , rhs) ← returnTC (toAlgebraExpression cring (getArgs equation))
        where
          nothing
            → typeError(
                strErr "Error while trying to build ASTs for the equation " ∷
                termErr equation ∷ [])
      let solution = solverCallByVarIndices (length varIndices) varIndices cring lhs rhs
      unify hole solution

  solveEqReasoning-macro : Term → Term → Term → Term → Term → TC Unit
  solveEqReasoning-macro lhs cring varsToSolve reasoningToTheRight hole =
    do
      just varIndices ← returnTC (extractVarIndices (toListOfTerms varsToSolve))
        where
          nothing
            → typeError(
                strErr "Error reading variables to solve " ∷
                termErr varsToSolve ∷ [])
      just rhs ← returnTC (getRhs reasoningToTheRight)
        where
          nothing
            → typeError(
                strErr "Failed to extract right hand side of equation to solve from " ∷
                termErr reasoningToTheRight ∷ [])
      just (lhsAST , rhsAST) ← returnTC (toAlgebraExpression cring (just (lhs , rhs)))
        where
          nothing
            → typeError(
                strErr "Error while trying to build ASTs from " ∷
                termErr lhs ∷ strErr " and " ∷ termErr rhs ∷ [])
      let solverCall = solverCallByVarIndices (length varIndices) varIndices cring lhsAST rhsAST
      unify hole (def (quote _≡⟨_⟩_) (varg lhs ∷ varg solverCall ∷ varg reasoningToTheRight ∷ []))

macro
  solve : Term → Term → TC _
  solve = solve-macro

  solveInPlace : Term → Term → Term → TC _
  solveInPlace = solveInPlace-macro

  infixr 2 _≡⟨solveIn_withVars_⟩_
  _≡⟨solveIn_withVars_⟩_ : Term → Term → Term → Term → Term → TC Unit
  _≡⟨solveIn_withVars_⟩_ = solveEqReasoning-macro

fromℤ : (R : CommRing ℓ) → ℤ → fst R
fromℤ = scalar

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


text:
open import Nat
open import Prelude
open import List
open import judgemental-erase
open import moveerase
open import statics-checks
open import statics-core

module aasubsume-min where
  -- this predicate on derivations of actions bans the cases that induce
  -- non-determinism.
  mutual
    aasubmin-synth : ∀{Γ e t α e' t'} → (Γ ⊢ e => t ~ α ~> e' => t') → Set
    aasubmin-synth (SAZipAsc1 x) = aasubmin-ana x
    aasubmin-synth (SAZipLam2  x x₁ x₂ d) = aasubmin-synth d
    aasubmin-synth (SAZipApArr x x₁ x₂ d x₃) = aasubmin-synth d
    aasubmin-synth (SAZipApAna x x₁ x₂) = aasubmin-ana x₂
    aasubmin-synth (SAZipPlus1 x) = aasubmin-ana x
    aasubmin-synth (SAZipPlus2 x) = aasubmin-ana x
    aasubmin-synth (SAZipNEHole x x₁ d) = aasubmin-synth d
    aasubmin-synth (SAZipPair1 x x₁ d x₂) = aasubmin-synth d
    aasubmin-synth (SAZipPair2 x x₁ x₂ d) = aasubmin-synth d
    aasubmin-synth (SAZipFst x x₁ x₂ x₃ d) = aasubmin-synth d
    aasubmin-synth (SAZipSnd x x₁ x₂ x₃ d) = aasubmin-synth d
    aasubmin-synth _ = ⊤

    aasubmin-ana : ∀{Γ e α e' t} → (Γ ⊢ e ~ α ~> e' ⇐ t) → Set
    aasubmin-ana (AASubsume x x₁ SAConAsc x₃) = ⊥
    aasubmin-ana (AASubsume x x₁ SAConInl x₃) = ⊥
    aasubmin-ana (AASubsume x x₁ SAConInr x₃) = ⊥
    aasubmin-ana (AASubsume x x₁ (SAConLam x₃) x₄) = ⊥
    aasubmin-ana (AASubsume EETop SEHole (SAConCase1 a b c) x₄) = ⊥
    aasubmin-ana (AASubsume x x₁ s x₃) = aasubmin-synth s
    aasubmin-ana (AAZipLam x₁ x₂ d) = aasubmin-ana d
    aasubmin-ana (AAZipInl x y) = aasubmin-ana y
    aasubmin-ana (AAZipInr x y) = aasubmin-ana y
    aasubmin-ana (AAZipCase1 a b c d e f g h) = aasubmin-synth e
    aasubmin-ana (AAZipCase2 a b c d e) = aasubmin-ana e
    aasubmin-ana (AAZipCase3 a b c d f) = aasubmin-ana f
    aasubmin-ana _ = ⊤

  -- the minimization predicate propagates through subsumption rules
  min-ana-lem : ∀{e e' e◆ Γ t t' t'' α} {a : erase-e e e◆}
                 {b : Γ ⊢ e◆ => t'} {c : t ~ t''} →
                 (d : Γ ⊢ e => t' ~ α ~> e' => t'') →
                 aasubmin-ana (AASubsume a b d c) →
                 aasubmin-synth d
  min-ana-lem (SAMove x) min = <>
  min-ana-lem (SADel) min = <>
  min-ana-lem (SAConAsc) min = <>
  min-ana-lem (SAConVar p) min = <>
  min-ana-lem (SAConLam x₁) min = <>
  min-ana-lem (SAConApArr x) min = <>
  min-ana-lem (SAConApOtw x) min = <>
  min-ana-lem (SAConNumlit) min = <>
  min-ana-lem (SAConPlus1 x) min = <>
  min-ana-lem (SAConPlus2 x) min = <>
  min-ana-lem (SAConNEHole) min = <>
  min-ana-lem (SAFinish x) min = <>
  min-ana-lem (SAZipAsc1 x) min = min
  min-ana-lem (SAZipAsc2 x x₁ x₂ x₃) min = <>
  min-ana-lem (SAZipApArr x x₁ x₂ c x₃) min = min
  min-ana-lem (SAZipApAna x x₁ x₂) min = min
  min-ana-lem (SAZipPlus1 x) min = min
  min-ana-lem (SAZipPlus2 x) min = min
  min-ana-lem (SAZipNEHole x x₁ c) min = min
  min-ana-lem SAConInl _ = <>
  min-ana-lem SAConInr _ = <>
  min-ana-lem (SAConCase1 x₁ x₂ x₃) _ = <>
  min-ana-lem (SAConCase2 x₁ x₂ x₃) _ = <>
  min-ana-lem SAConPair _ = <>
  min-ana-lem (SAConFst1 pr) _ = <>
  min-ana-lem (SAConFst2 inc) _ = <>
  min-ana-lem (SAConSnd1 pr) _ = <>
  min-ana-lem (SAConSnd2 inc) _ = <>
  min-ana-lem (SAZipPair1 x x₁ x₂ x₃) min = min
  min-ana-lem (SAZipPair2 x x₁ x₂ x₃) min = min
  min-ana-lem (SAZipFst x x₁ x₂ x₃ x₄) min = min
  min-ana-lem (SAZipSnd x x₁ x₂ x₃ x₄) min = min
  min-ana-lem (SAZipLam1 x x₁ x₂ x₃ x₄ x₅) min = min
  min-ana-lem (SAZipLam2 x x₁ x₂ x₃) min = min

  -- any derivation of an action can be minimized to avoid this cases that
  -- induce non-determinism.
  mutual
    min-synth : ∀{Γ e t α e' t'} →
                (d : Γ ⊢ e => t ~ α ~> e' => t') →
                Σ[ e'' ∈ zexp ] Σ[ d' ∈ Γ ⊢ e => t ~ α ~> e'' => t' ] aasubmin-synth d'
    min-synth (SAMove x) = _ , SAMove x , <>
    min-synth SADel = _ , SADel , <>
    min-synth SAConAsc = _ , SAConAsc , <>
    min-synth (SAConVar p) = _ , SAConVar p , <>
    min-synth (SAConLam x₁) = _ , SAConLam x₁ , <>
    min-synth (SAConApArr x) = _ , SAConApArr x , <>
    min-synth (SAConApOtw x) = _ , SAConApOtw x , <>
    min-synth SAConNumlit = _ , SAConNumlit , <>
    min-synth (SAConPlus1 x) = _ , SAConPlus1 x , <>
    min-synth (SAConPlus2 x) = _ , SAConPlus2 x , <>
    min-synth SAConNEHole = _ , SAConNEHole , <>
    min-synth (SAFinish x) = _ , SAFinish x , <>
    min-synth (SAZipAsc2 x x₁ x₂ x₃) = _ , SAZipAsc2 x x₁ x₂ x₃ , <>
    min-synth (SAZipAsc1 x) with min-ana x
    ... | _ , a , b = _ ,  SAZipAsc1 a , b
    min-synth (SAZipApArr x x₁ x₂ d x₃) with min-synth d
    ... | _ , a , b = _ , (SAZipApArr x x₁ x₂ a x₃) , b
    min-synth (SAZipApAna x x₁ x₂) with min-ana x₂
    ... | _ , a , b = _ , SAZipApAna x x₁ a , b
    min-synth (SAZipPlus1 x) with min-ana x
    ... | _ , a , b = _ , SAZipPlus1 a , b
    min-synth (SAZipPlus2 x) with min-ana x
    ... | _ , a , b = _ , SAZipPlus2 a , b
    min-synth (SAZipNEHole x x₁ d) with min-synth d
    ... | _ , a , b = _ , SAZipNEHole x x₁ a , b
    min-synth SAConInl = _ , SAConInl , <>
    min-synth SAConInr = _ , SAConInr , <>
    min-synth (SAConCase1 a b c) = _ , SAConCase1 a b c , <>
    min-synth (SAConCase2 a b c) = _ , SAConCase2 a b c , <>
    min-synth SAConPair = _ , SAConPair , <>
    min-synth (SAConFst1 pr) = _ , SAConFst1 pr , <>
    min-synth (SAConFst2 inc) = _ , SAConFst2 inc , <>
    min-synth (SAConSnd1 pr) = _ , SAConSnd1 pr , <>
    min-synth (SAConSnd2 inc) = _ , SAConSnd2 inc , <>
    min-synth (SAZipPair1 x x₁ d x₃) with min-synth d
    ... | _ , a , b = _ , (SAZipPair1 x x₁ a x₃) , b
    min-synth (SAZipPair2 x x₁ x₂ d) with min-synth d
    ... | _ , a , b = _ , (SAZipPair2 x x₁ x₂ a) , b
    min-synth (SAZipFst x x₁ x₂ x₃ d) with min-synth d
    ... | _ , a , b = _ , (SAZipFst x x₁ x₂ x₃ a) , b
    min-synth (SAZipSnd x x₁ x₂ x₃ d) with min-synth d
    ... | _ , a , b = _ , (SAZipSnd x x₁ x₂ x₃ a) , b
    min-synth (SAZipLam1 x x₁ x₂ x₃ x₄ x₅) = _ , SAZipLam1 x x₁ x₂ x₃ x₄ x₅ , <>
    min-synth (SAZipLam2 x x₁ x₂ d) with min-synth d
    ... | _ , a , b = _ , SAZipLam2 x x₁ x₂ a , b

    min-ana : ∀{Γ e α e' t} →
              (d : Γ ⊢ e ~ α ~> e' ⇐ t) →
              Σ[ e'' ∈ zexp ] Σ[ d' ∈  Γ ⊢ e ~ α ~> e'' ⇐ t ] aasubmin-ana d'
    min-ana (AASubsume {Γ = Γ} x x₁ (SAMove x₂) x₃) = _ , AAMove x₂ , <>
    min-ana (AASubsume x x₁ (SADel) x₃) = _ , AADel , <>
    min-ana (AASubsume {Γ = Γ}  {t = t} {t' = t'}  x x₁ SAConAsc x₃) =
      _ , AAConAsc {Γ = Γ} {t = t} , <>
    min-ana (AASubsume x x₁ (SAConVar p) x₃) = _ , AASubsume x x₁ (SAConVar p) x₃ , <>
    min-ana (AASubsume EETop SEHole (SAConLam x₃) TCRefl) = _ , AAConLam1 x₃ MAArr , <>
    min-ana (AASubsume EETop SEHole (SAConLam x₃) TCHole2)  = _ , AAConLam1 x₃ MAHole , <>
    min-ana (AASubsume EETop SEHole (SAConLam x₃) (TCArr x₄ x₅)) = _ , AAConLam1 x₃ MAArr , <>
    min-ana (AASubsume x x₁ (SAConApArr x₂) x₃) =
      _ , AASubsume x x₁ (SAConApArr x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConApOtw x₂) x₃) =
      _ , AASubsume x x₁ (SAConApOtw x₂) x₃ , <>
    min-ana (AASubsume x x₁ SAConNumlit x₃) = _ , AASubsume x x₁ SAConNumlit x₃ , <>
    min-ana (AASubsume x x₁ (SAConPlus1 x₂) x₃) =
      _ , AASubsume x x₁ (SAConPlus1 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConPlus2 x₂) x₃) =
      _ , AASubsume x x₁ (SAConPlus2 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConNEHole) x₃) =
      _ , AASubsume x x₁ (SAConNEHole) x₃ , <>
    min-ana (AASubsume x x₁ (SAFinish x₂) x₃) = _ ,  AASubsume x x₁ (SAFinish x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAZipAsc2 x₂ x₃ x₄ x₅) x₆) =
      _ , AASubsume x x₁ (SAZipAsc2 x₂ x₃ x₄ x₅) x₆ , <>
    min-ana (AASubsume x x₁ (SAZipAsc1 x₂) x₃) with min-ana x₂
    ... | a , b , c = _ , AASubsume x x₁ (SAZipAsc1 b) x₃ , c
    min-ana (AASubsume x x₁ (SAZipApArr x₂ x₃ x₄ x₅ x₆) x₇) with min-synth x₅
    ... | a , b , c = _ , AASubsume x x₁ (SAZipApArr x₂ x₃ x₄ b x₆) x₇ , c
    min-ana (AASubsume x x₁ (SAZipApAna x₂ x₃ x₄) x₅) with min-ana x₄
    ... | a , b , c = _ , AASubsume x x₁ (SAZipApAna x₂ x₃ b) x₅ , c
    min-ana (AASubsume x x₁ (SAZipPlus1 x₂) x₃) with min-ana x₂
    ... | a , b , c = _ , AASubsume x x₁ (SAZipPlus1 b) x₃ , c
    min-ana (AASubsume x x₁ (SAZipPlus2 x₂) x₃) with min-ana x₂
    ... | a , b , c = _ , AASubsume x x₁ (SAZipPlus2 b) x₃ , c
    min-ana (AASubsume x x₁ (SAZipNEHole x₂ x₃ x₄) x₅) with min-synth x₄
    ... | a , b , c = _ , AASubsume x x₁ (SAZipNEHole x₂ x₃ b) x₅ , c
    min-ana (AASubsume EETop SEHole (SAConCase1 a b c) z) =
      _ , AAConCase a b , <>
    min-ana (AASubsume EETop (SAsc x₁) (SAConCase1 a b c) z) =
      _ , AASubsume EETop (SAsc x₁) (SAConCase1 a b c) z , <>
    min-ana (AASubsume EETop (SVar x₁) (SAConCase1 a b c) z) =
      _ , AASubsume EETop (SVar x₁) (SAConCase1 a b c) z , <>
    min-ana (AASubsume EETop (SLam x x₁) (SAConCase1 x₂ x₄ x₅) x₃) =
      _ , AASubsume EETop (SLam x x₁) (SAConCase1 x₂ x₄ x₅) x₃ , <>
    min-ana (AASubsume EETop (SAp y₁ x₁ x₂) (SAConCase1 a b c) z) =
      _ , AASubsume EETop (SAp y₁ x₁ x₂) (SAConCase1 a b c) z , <>
    min-ana (AASubsume EETop SNum (SAConCase1 a b c) z) =
      _ , AASubsume EETop SNum (SAConCase1 a b c) z , <>
    min-ana (AASubsume EETop (SPlus x₁ x₂) (SAConCase1 a b c) z) =
      _ , AASubsume EETop (SPlus x₁ x₂) (SAConCase1 a b c) z , <>
    min-ana (AASubsume EETop (SNEHole y₁) (SAConCase1 a b c) z) =
      _ , AASubsume EETop (SNEHole y₁) (SAConCase1 a b c) z , <>
    min-ana (AASubsume EETop (SPair x₁ x₆) (SAConCase1 x₂ x₄ x₅) x₃) =
      _ , (AASubsume EETop (SPair x₁ x₆) (SAConCase1 x₂ x₄ x₅) x₃) , <>
    min-ana (AASubsume EETop (SFst x x₁) (SAConCase1 x₂ x₃ x₄) x₅) =
      _ , AASubsume EETop (SFst x x₁) (SAConCase1 x₂ x₃ x₄) x₅ , <>
    min-ana (AASubsume EETop (SSnd x x₁) (SAConCase1 x₂ x₃ x₄) x₅) =
      _ , AASubsume EETop (SSnd x x₁) (SAConCase1 x₂ x₃ x₄) x₅ , <>
    min-ana (AASubsume x y (SAConCase2 a b c) z) =
      _ , AASubsume x y (SAConCase2 a b c) z , <>

    min-ana (AAMove x) = _ , AAMove x , <>
    min-ana AADel = _ , AADel , <>
    min-ana AAConAsc = _ , AAConAsc , <>
    min-ana (AAConVar x₁ p) = _ , AAConVar x₁ p , <>
    min-ana (AAConLam1 x₁ x₂) = _ , AAConLam1 x₁ x₂ , <>
    min-ana (AAConLam2 x₁ x₂) = _ , AAConLam2 x₁ x₂ , <>
    min-ana (AAConNumlit x) = _ , AAConNumlit x , <>
    min-ana (AAFinish x) = _ , AAFinish x , <>
    min-ana (AAZipLam x₁ x₂ d) with min-ana d
    ... | a , b , c = _ , AAZipLam x₁ x₂ b , c
    min-ana (AASubsume x x₁ SAConInl TCRefl) = _ , AAConInl1 MSSum , <>
    min-ana (AASubsume x x₁ SAConInl TCHole2) = _ , AAConInl1 MSHole , <>
    min-ana (AASubsume x x₁ SAConInl (TCSum x₃ x₄)) = _ , AAConInl1 MSSum , <>
    min-ana (AASubsume x x₁ SAConInr TCRefl) = _ , AAConInr1 MSSum , <>
    min-ana (AASubsume x x₁ SAConInr TCHole2) = _ , AAConInr1 MSHole , <>
    min-ana (AASubsume x x₁ SAConInr (TCSum x₃ x₄)) = _ , AAConInr1 MSSum , <>
    min-ana (AAConInl1 x) = _ , AAConInl1 x , <>
    min-ana (AAConInl2 x) = _ , AAConInl2 x , <>
    min-ana (AAConInr1 x) = _ , AAConInr1 x , <>
    min-ana (AAConInr2 x) = _ , AAConInr2 x , <>
    min-ana (AAConCase x₁ x₂) = _ , AAConCase x₁ x₂ , <>
    min-ana (AAZipInl x x₁) with min-ana x₁
    ... | a , b , c = _ , AAZipInl x b , c
    min-ana (AAZipInr x x₁) with min-ana x₁
    ... | a , b , c = _ , AAZipInr x b , c
    min-ana (AAZipCase1 x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) with min-synth x₅
    ... | a , b , c = _ , AAZipCase1 x₁ x₂ x₃ x₄ b x₆ x₇ x₈ , c
    min-ana (AAZipCase2 x₁ x₂ x₃ x₄ x₅) with min-ana x₅
    ... | a , b , c = _ , AAZipCase2 x₁ x₂ x₃ x₄ b , c
    min-ana (AAZipCase3 x₁ x₂ x₃ x₄ x₆) with min-ana x₆
    ... | a , b , c = _ , AAZipCase3 x₁ x₂ x₃ x₄ b , c

    min-ana (AASubsume x x₁ (SAZipLam1 x₂ x₄ x₅ x₆ x₇ x₈) x₃) =
      _ , AASubsume x x₁ (SAZipLam1 x₂ x₄ x₅ x₆ x₇ x₈) x₃ , <>
    min-ana (AASubsume x x₁ (SAZipLam2 x₂ x₄ x₅ x₆) x₃) with min-synth x₆
    ... | a , b , c = _ , AASubsume x x₁ (SAZipLam2 x₂ x₄ x₅ b) x₃ , c
    min-ana (AASubsume x x₁ SAConPair x₃) =
      _ , AASubsume x x₁ SAConPair x₃ , <>
    min-ana (AASubsume x x₁ (SAConFst1 x₂) x₃) = _ , AASubsume x x₁ (SAConFst1 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConFst2 x₂) x₃) =
      _ , AASubsume x x₁ (SAConFst2 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConSnd1 x₂) x₃) = _ , AASubsume x x₁ (SAConSnd1 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAConSnd2 x₂) x₃) =
      _ , AASubsume x x₁ (SAConSnd2 x₂) x₃ , <>
    min-ana (AASubsume x x₁ (SAZipPair1 x₂ x₃ x₄ x₅) x₆) with min-synth x₄
    ... | a , b , c = _ , (AASubsume x x₁ (SAZipPair1 x₂ x₃ b x₅) x₆) , c
    min-ana (AASubsume x x₁ (SAZipPair2 x₂ x₃ x₄ x₅) x₆) with min-synth x₅
    ... | a , b , c = _ , AASubsume x x₁ (SAZipPair2 x₂ x₃ x₄ b) x₆ , c
    min-ana (AASubsume x x₁ (SAZipFst x₂ x₃ x₄ x₅ x₆) x₇) with min-synth x₆
    ... | a , b , c = _ , AASubsume x x₁ (SAZipFst x₂ x₃ x₄ x₅ b) x₇ , c
    min-ana (AASubsume x x₁ (SAZipSnd x₂ x₃ x₄ x₅ x₆) x₇) with min-synth x₆
    ... | a , b , c = _ , AASubsume x x₁ (SAZipSnd x₂ x₃ x₄ x₅ b) x₇ , c

  -- these theorems argue that if a derivation is already subsumption
  -- minimal than the minimzer does not change the resultant
  -- expression--that it's conservative in this sense. they do not argue
  -- that the derivation that's computed is itself the same as the input
  -- derivation.
  mutual
    min-fixed-synth : ∀{Γ e t α e' t'} →
                      (d : Γ ⊢ e => t ~ α ~> e' => t') →
                      aasubmin-synth d →
                      e' == π1 (min-synth d)
    min-fixed-synth (SAMove x) min = refl
    min-fixed-synth SADel min = refl
    min-fixed-synth SAConAsc min = refl
    min-fixed-synth (SAConVar p) min = refl
    min-fixed-synth (SAConLam x₁) min = refl
    min-fixed-synth (SAConApArr x) min = refl
    min-fixed-synth (SAConApOtw x) min = refl
    min-fixed-synth SAConNumlit min = refl
    min-fixed-synth (SAConPlus1 x) min = refl
    min-fixed-synth (SAConPlus2 x) min = refl
    min-fixed-synth SAConNEHole min = refl
    min-fixed-synth (SAFinish x) min = refl
    min-fixed-synth (SAZipAsc1 x) min with min-fixed-ana x min
    ... | qq with min-ana x
    ... | (e'' , d' , min') = ap1 (λ q → q ·:₁ _) qq
    min-fixed-synth (SAZipAsc2 x x₁ x₂ x₃) min = refl
    min-fixed-synth (SAZipApArr x x₁ x₂ d x₃) min with min-fixed-synth d min
    ... | qq with min-synth d
    ... | (e'' , d' , min') = ap1 (λ q → q ∘₁ _) qq
    min-fixed-synth (SAZipApAna x x₁ x₂) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → _ ∘₂ q) qq
    min-fixed-synth (SAZipPlus1 x) min with min-fixed-ana x min
    ... | qq with min-ana x
    ... | (e'' , _ , _) = ap1 (λ q → q ·+₁ _) qq
    min-fixed-synth (SAZipPlus2 x) min with min-fixed-ana x min
    ... | qq with min-ana x
    ... | (e'' , _ , _) = ap1 (λ q → _ ·+₂ q) qq
    min-fixed-synth (SAZipNEHole x x₁ d) min with min-fixed-synth d min
    ... | qq with min-synth d
    ... | (e'' , _ , _) = ap1 ⦇⌜_⌟⦈[ _ ] qq
    min-fixed-synth SAConInl min = refl
    min-fixed-synth SAConInr min = refl
    min-fixed-synth (SAConCase1 x₁ x₂ x₃) min = refl
    min-fixed-synth (SAConCase2 x₁ x₂ x₃) min = refl
    min-fixed-synth SAConPair min = refl
    min-fixed-synth (SAConFst1 x₁) min = refl
    min-fixed-synth (SAConFst2 x₁) min = refl
    min-fixed-synth (SAConSnd1 x₁) min = refl
    min-fixed-synth (SAConSnd2 x₁) min = refl
    min-fixed-synth (SAZipPair1 x x₁ d x₃) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → ⟨ q , _ ⟩₁) qq
    min-fixed-synth (SAZipPair2 x x₁ x₂ d) min  with min-fixed-synth d min
    ... | qq = ap1 (λ q → ⟨ _ , q ⟩₂) qq
    min-fixed-synth (SAZipFst x x₁ x₂ x₃ d) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → fst q) qq
    min-fixed-synth (SAZipSnd x x₁ x₂ x₃ d) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → snd q) qq
    min-fixed-synth (SAZipLam1 x x₁ x₂ x₃ x₄ x₅) min = refl
    min-fixed-synth (SAZipLam2 x x₁ x₂ d) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → ·λ _ ·[ _ ]₂ q) qq

    min-fixed-ana : ∀{Γ e t α e' } →
                    (d : Γ ⊢ e ~ α ~> e' ⇐ t) →
                    aasubmin-ana d →
                    e' == π1 (min-ana d)
    min-fixed-ana (AASubsume x x₁ (SAMove x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SADel x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SAConAsc x₃) min = abort min
    min-fixed-ana (AASubsume x₁ x₂ (SAConVar p) x₃) min = refl
    min-fixed-ana (AASubsume x₁ x₂ (SAConLam x₃) x₄) min = abort min
    min-fixed-ana (AASubsume x x₁ (SAConApArr x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConApOtw x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SAConNumlit x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConPlus1 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConPlus2 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ SAConNEHole x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAFinish x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAZipAsc1 x₂) x₃) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → q ·:₁ _) qq
    min-fixed-ana (AASubsume x x₁ (SAZipAsc2 x₂ x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume x x₁ (SAZipApArr x₂ x₃ x₄ x₅ x₆) x₇) min with min-fixed-synth x₅ min
    ... | qq with min-synth x₅
    ... | (e'' , d' , min') = ap1 (λ q → q ∘₁ _) qq
    min-fixed-ana (AASubsume x x₁ (SAZipApAna x₂ x₃ x₄) x₅) min with min-fixed-ana x₄ min
    ... | qq with min-ana x₄
    ... | (e'' , _ , _) = ap1 (λ q → _ ∘₂ q) qq
    min-fixed-ana (AASubsume x x₁ (SAZipPlus1 x₂) x₃) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → q ·+₁ _) qq
    min-fixed-ana (AASubsume x x₁ (SAZipPlus2 x₂) x₃) min with min-fixed-ana x₂ min
    ... | qq with min-ana x₂
    ... | (e'' , _ , _) = ap1 (λ q → _ ·+₂ q) qq
    min-fixed-ana (AASubsume x x₁ (SAZipNEHole x₂ x₃ x₄) x₅) min with min-fixed-synth x₄ min
    ... | qq with min-synth x₄
    ... | (e'' , _ , _) = ap1 ⦇⌜_⌟⦈[ _ ] qq
    min-fixed-ana (AAMove x) min = refl
    min-fixed-ana AADel min = refl
    min-fixed-ana AAConAsc min = refl
    min-fixed-ana (AAConVar x₁ p) min = refl
    min-fixed-ana (AAConLam1 x₁ x₂) min = refl
    min-fixed-ana (AAConLam2 x₁ x₂) min = refl
    min-fixed-ana (AAConNumlit x) min = refl
    min-fixed-ana (AAFinish x) min = refl
    min-fixed-ana (AAZipLam x₁ x₂ d) min with min-fixed-ana d min
    ... | qq with min-ana d
    ... | (e'' , _ , _) = ap1 (λ q → ·λ _ q) qq
    min-fixed-ana (AASubsume x x₁ SAConInl x₃) min = abort min
    min-fixed-ana (AASubsume x x₁ SAConInr x₃) min = abort min
    min-fixed-ana (AASubsume EETop (SAsc x₁) (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume EETop (SVar x₁) (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume EETop (SLam x x₁) (SAConCase1 x₂ x₄ x₅) x₃) min = refl
    min-fixed-ana (AASubsume EETop (SPair x₁ x₆) (SAConCase1 x₂ x₄ x₅) x₃) min = refl
    min-fixed-ana (AASubsume EETop (SAp x₂ x₁ x₃) (SAConCase1 x₄ x₅ x₆) x₇) min = refl
    min-fixed-ana (AASubsume EETop SNum (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume EETop (SPlus x₁ x₂) (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume EETop SEHole (SAConCase1 x₃ x₄ x₅) x₆) min = abort min
    min-fixed-ana (AASubsume EETop (SNEHole x₂) (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume EETop (SFst x x₁) (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume EETop (SSnd x x₁) (SAConCase1 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AASubsume x₁ x₂ (SAConCase2 x₃ x₄ x₅) x₆) min = refl
    min-fixed-ana (AAConInl1 x) min = refl
    min-fixed-ana (AAConInl2 x) min = refl
    min-fixed-ana (AAConInr1 x) min = refl
    min-fixed-ana (AAConInr2 x) min = refl
    min-fixed-ana (AAConCase x₁ x₂) min = refl
    min-fixed-ana (AAZipInl x d) min with min-fixed-ana d min
    ... | qq with min-ana d
    ... | (e'' , _ , _) = ap1 inl qq
    min-fixed-ana (AAZipInr x d) min with min-fixed-ana d min
    ... | qq with min-ana d
    ... | (e'' , _ , _) = ap1 inr qq
    min-fixed-ana (AAZipCase1 x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) min with min-fixed-synth x₅ min
    ... | qq with min-synth x₅
    ... | (e'' , _ , _) = ap1 (λ q → case₁ q _ _ _ _) qq
    min-fixed-ana (AAZipCase2 x₁ x₂ x₃ x₄ d) min with min-fixed-ana d min
    ... | qq with min-ana d
    ... | (e'' , _ , _) = ap1 (λ q → case₂ _ _ q _ _) qq
    min-fixed-ana (AAZipCase3 x₁ x₂ x₃ x₄ d) min with min-fixed-ana d min
    ... | qq with min-ana d
    ... | (e'' , _ , _) = ap1 (λ q → case₃ _ _ _ _ q) qq

    min-fixed-ana (AASubsume x x₁ SAConPair x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConFst1 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConFst2 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConSnd1 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAConSnd2 x₂) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAZipPair1 x₂ x₄ d x₆) x₃) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → ⟨ q , _ ⟩₁) qq
    min-fixed-ana (AASubsume x x₁ (SAZipPair2 x₂ x₄ x₅ d) x₃) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → ⟨ _ , q ⟩₂) qq
    min-fixed-ana (AASubsume x x₁ (SAZipFst x₂ x₄ x₅ x₆ d) x₃) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → fst q) qq
    min-fixed-ana (AASubsume x x₁ (SAZipSnd x₂ x₄ x₅ x₆ d) x₃) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → snd q) qq
    min-fixed-ana (AASubsume x x₁ (SAZipLam1 x₂ x₄ x₅ x₆ x₇ x₈) x₃) min = refl
    min-fixed-ana (AASubsume x x₁ (SAZipLam2 x₂ x₄ x₅ d) x₃) min with min-fixed-synth d min
    ... | qq = ap1 (λ q → ·λ _ ·[ _ ]₂ q) qq

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.NatMinusTwo where

open import Cubical.Data.NatMinusTwo.Base public

open import Cubical.Data.NatMinusTwo.Properties public

open import Cubical.Data.NatMinusTwo.ToNatMinusOne using (1+_; ℕ₋₁→ℕ₋₂; -1+Path) public


text:
------------------------------------------------------------------------------
-- Mendelson's substitution
------------------------------------------------------------------------------

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

module FOT.FOL.MendelsonSubstATP where

-- First-order logic with equality.
open import Common.FOL.FOL-Eq public

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

-- Mendelson's [2015] substitution (p. 93).

--   (A7) x = y ⇒ (A(x,x) ⇒ B(x,y)) (substitutivity of equality)

postulate mendelsonSubst : (A : D → D → Set) → ∀ {x y} → x ≡ y → A x x → A x y

{-# ATP prove mendelsonSubst #-}

------------------------------------------------------------------------------
-- References

-- Mendelson, Elliott (2015). Introduction to Mathematical Logic. CRC
-- Press, 6th edition.


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

postulate
  A : Set
  P : A → Set
  Q : {x : A} → P x → P x → Set

variable
  B    : Set
  @0 q : B

postulate
  F : ∀ p → Q p q → Set

Test : {@0 x : A} ({q} p : P x) (q′ : Q p q) → Set
Test = F


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

open import Calf.CostMonoid

module Calf (costMonoid : CostMonoid) where

open CostMonoid costMonoid

open import Calf.Prelude public
open import Calf.Metalanguage public
open import Calf.PhaseDistinction public
open import Calf.Step costMonoid public

open import Calf.Noninterference costMonoid public

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
open import MLib.Finite

module MLib.Finite.Properties {c ℓ} (finiteSet : FiniteSet c ℓ) where

open import MLib.Prelude
import Data.Fin.Permutation as Perm

import Relation.Binary as B

open FE using (cong)
open LeftInverse using () renaming (_∘_ to _ⁱ∘_)

open Algebra using (IdempotentCommutativeMonoid)
open Table hiding (setoid)

open FiniteSet finiteSet renaming (Carrier to A)

private
  enumₜAt : ∀ {N} → OntoFin N → Table A N
  enumₜAt = tabulate ∘ _⟨$⟩_ ∘ LeftInverse.from

module _ {c ℓ} (icMonoid : IdempotentCommutativeMonoid c ℓ) where
  module S = IdempotentCommutativeMonoid icMonoid
  open S using (_∙_; ∙-cong) renaming (Carrier to S; _≈_ to _≈′_)
  open import Algebra.Operations.CommutativeMonoid S.commutativeMonoid
  open import Algebra.Properties.CommutativeMonoid S.commutativeMonoid

  foldMap : (A → S) → S
  foldMap f = sumₜ (Table.map f enumₜ)

  foldMap-cong : ∀ {f g} → (∀ x → f x ≈′ g x) → foldMap f ≈′ foldMap g
  foldMap-cong p = sumₜ-cong-≈ (p ∘ lookup enumₜ)

  private
    inhabited : ∀ {N} (i : Fin N) → ∃ λ n → N ≡ Nat.suc n
    inhabited Fin.zero = _ , ≡.refl
    inhabited (Fin.suc i) = _ , ≡.refl

  -- Folding with a constant function produces the constant.

  foldMap-const : ∀ {x} → x ∙ foldMap (λ _ → x) ≈′ x
  foldMap-const {x} =
    begin
      x ∙ foldMap (λ _ → x)                  ≡⟨⟩
      x ∙ sumₜ (Table.map (λ _ → x) enumₜ)   ≡⟨⟩
      x ∙ sumₜ (Table.replicate {N} x)       ≡⟨⟩
      sumₜ (Table.replicate {Nat.suc N} x)   ≈⟨ sumₜ-idem-replicate N (S.idem x) ⟩
      x                                      ∎
    where open EqReasoning S.setoid

  private
    module _ {n : ℕ} (ontoFin′ : OntoFin (Nat.suc n)) where
      from = LeftInverse.from ontoFin′ ⟨$⟩_
      to = LeftInverse.to ontoFin′ ⟨$⟩_
      from-to = LeftInverse.left-inverse-of ontoFin′

      enumₜ′ : Table A (Nat.suc n)
      enumₜ′ = enumₜAt ontoFin′

      ap : setoid ⟶ S.setoid → A → S
      ap = _⟨$⟩_

      enumₜ-complete′ : ∀ (func : setoid ⟶ S.setoid) x → (func ⟨$⟩ x) ∙ sumₜ (map (ap func) enumₜ′) ≈′ sumₜ (map (ap func) enumₜ′)
      enumₜ-complete′ func x =
        begin
          f x ∙ sumₜ (map f enumₜ′)                                        ≈⟨ ∙-cong S.refl (sumₜ-permute (map f enumₜ′) (Perm.transpose Fin.zero i)) ⟩
          f x ∙ sumₜ (permute (Perm.transpose Fin.zero i) (map f enumₜ′))  ≡⟨⟩
          f x ∙ (f (from (to x)) ∙ _)                                      ≈⟨ ∙-cong S.refl (∙-cong (cong func (from-to _)) S.refl) ⟩
          f x ∙ (f x ∙ _)                                                  ≈⟨ S.sym (S.assoc _ _ _) ⟩
          (f x ∙ f x) ∙ _                                                  ≈⟨ ∙-cong (S.idem _) S.refl ⟩
          f x ∙ _                                                          ≈⟨ ∙-cong (cong func (sym (from-to _))) S.refl ⟩
          f (from (to x)) ∙ _                                              ≡⟨⟩
          sumₜ (permute (Perm.transpose Fin.zero i) (map f enumₜ′))        ≈⟨ S.sym (sumₜ-permute (map f enumₜ′) (Perm.transpose Fin.zero i)) ⟩
          sumₜ (map f enumₜ′)                                              ∎
        where
          f = ap func
          i = to x

          open EqReasoning S.setoid

  private
    enumₜ-complete′′ :
      ∀ {N} (ontoFin′ : OntoFin N) (f : setoid ⟶ S.setoid) x
      → (f ⟨$⟩ x) ∙ sumₜ (Table.map (f ⟨$⟩_) (enumₜAt ontoFin′))
        ≈′ sumₜ (Table.map (f ⟨$⟩_) (enumₜAt ontoFin′))
    enumₜ-complete′′ ontoFin′ f x with inhabited (LeftInverse.to ontoFin′ ⟨$⟩ x)
    enumₜ-complete′′ ontoFin′ f x | n , ≡.refl = enumₜ-complete′ ontoFin′ f x

    sum/map-hom : ∀ {n} {a}{A : Set a} (f : A → S) (t : Table A n) → sumₗ (List.map f (toList t)) ≡ sumₜ (map f t)
    sum/map-hom f t =
      begin
        sumₗ (List.map f (toList t))   ≡⟨ ≡.cong sumₗ (Table.map-toList-hom t) ⟩
        sumₗ (toList (map f t))        ≡⟨ ≡.sym (sumₜ-toList (map f t)) ⟩
        sumₜ (map f t)                 ∎
      where
        open ≡.Reasoning

  -- Enumeration is complete: in any idempotent commutative monoid, adding one
  -- more element to the sum won't change it. In particular, this works in the
  -- powerset monoid, where 'f' is the singleton at its argument and addition
  -- is set union. This shows that every member of 'A' is present in the
  -- enumeration (even though the powerset monoid is quite difficult to
  -- implement in Agda so this proof is not present).

  enumₜ-complete : ∀ f x → (f ⟨$⟩ x) ∙ foldMap (f ⟨$⟩_) ≈′ foldMap (f ⟨$⟩_)
  enumₜ-complete = enumₜ-complete′′ ontoFin

  enumₗ-complete : ∀ (f : setoid ⟶ S.setoid) x → (f ⟨$⟩ x) ∙ sumₗ (List.map (f ⟨$⟩_) enumₗ) ≈′ sumₗ (List.map (f ⟨$⟩_) enumₗ)
  enumₗ-complete func x =
    begin
      f x ∙ sumₗ (List.map f enumₗ)           ≡⟨⟩
      f x ∙ sumₗ (List.map f (toList enumₜ))  ≡⟨ ≡.cong₂ _∙_ ≡.refl (sum/map-hom f enumₜ) ⟩
      f x ∙ sumₜ (map f enumₜ)                ≈⟨ enumₜ-complete func x ⟩
      sumₜ (map f enumₜ)                      ≡⟨ ≡.sym (sum/map-hom f enumₜ) ⟩
      sumₗ (List.map f enumₗ)                 ∎
    where
      f = func ⟨$⟩_
      open EqReasoning S.setoid

-- A finite set can be strictly totally ordered by its elements' indices

Ixorder : B.StrictTotalOrder _ _ _
Ixorder = record
  { _≈_ = _≈_
  ; _<_ = λ x y → toIx x Fin.< toIx y
  ; isStrictTotalOrder = record
    { isEquivalence = isEquivalence
    ; trans = Fin.<-trans
    ; compare = compare
    }
  }
  where
  compare : Trichotomous _≈_ (λ x y → toIx x Fin.< toIx y)
  compare x y with B.StrictTotalOrder.compare (Fin.<-strictTotalOrder N) (toIx x) (toIx y)
  compare x y | B.tri< a ¬b ¬c = B.tri< a (¬b ∘ cong (LeftInverse.to ontoFin)) ¬c
  compare x y | B.tri≈ ¬a b ¬c = B.tri≈ ¬a (LeftInverse.injective ontoFin b) ¬c
  compare x y | B.tri> ¬a ¬b c = B.tri> ¬a (¬b ∘ cong (LeftInverse.to ontoFin)) c

-- Equality between members of a finite set is decidable.

_≟_ : B.Decidable _≈_
_≟_ = B.StrictTotalOrder._≟_ Ixorder


text:
open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

module Issue2782 where

module Interval where
  private
    data I' : Set where
      Izero' : I'
      Ione'  : I'

  I : Set
  I = I'

  Izero : I
  Izero = Izero'

  Ione : I
  Ione = Ione'

  {--
  postulate
    Iseg : Izero ≡ Ione
  --}

  -- Fails when run with --safe flag in command-line

  unquoteDecl Iseg = declarePostulate (vArg Iseg) (def (quote _≡_) (vArg (def (quote Izero) []) ∷ vArg (def (quote Ione) []) ∷ []))

open Interval public

pf : Izero ≡ Ione
pf = Iseg

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Reflection using (Name)

-- See Tactic.Nat for a description of the various tactics.

module Tactic.Nat.Generic (`≤ `toLeq `fromLeq : Name) where

open import Prelude
open import Tactic.Reflection
open import Tactic.Nat.Induction using (nat-induction)
open import Tactic.Nat.Subtract using (autosub-tactic; by-tactic; refutesub-tactic; simplifygoal-tactic; simplifysub-tactic)

private
  a→0 : Type → Term
  a→0 (def op _) = ifYes op == `≤ then def₀ `toLeq else def₀ (quote id)
  a→0 _ = def₀ (quote id) -- TODO perhaps return unknown?

  0→a : Type → Term
  0→a (def op _) = ifYes op == `≤ then def₀ `fromLeq else def₀ (quote id)
  0→a _ = def₀ (quote id) -- TODO perhaps return unknown?

  applyTactic : (Type → TC Term) → Term → TC ⊤
  applyTactic tac hole = do
    goal ← inferType hole
    unify hole ∘ (0→a goal `$_) =<< tac =<< inferNormalisedType (a→0 goal `$ hole)

macro
  auto : Tactic
  auto hole = applyTactic autosub-tactic hole

  by : Term → Tactic
  by prf hole = do
    Prf ← inferNormalisedType prf
    applyTactic (by-tactic (a→0 Prf `$ prf)) hole

  refute : Term → Tactic
  refute prf hole = do
    Prf ← inferNormalisedType prf
    unify hole =<< refutesub-tactic (a→0 Prf `$ prf)

  simplify-goal : Tactic
  simplify-goal hole = do
    goal    ← inferFunRange hole
    s-goal₀ ← simplifygoal-tactic =<< inferFunRange (a→0 goal `∘ hole)
    hole =′ 0→a goal `∘ s-goal₀ `∘ a→0 goal

  simplify : Term → Tactic
  simplify prf hole = do
    goal    ← inferFunRange hole
    Prf     ← inferNormalisedType prf
    s-goal₀ ← simplifysub-tactic (a→0 Prf `$ prf) =<< inferFunRange (a→0 goal `∘ hole)
    hole =′ (`λ $ 0→a goal `$ weaken 1 s-goal₀ `$ `λ $ a→0 goal `$ var₁ 1 (0→a Prf `$ var₀ 0))

  induction : Tactic
  induction hole = do
    pi _ (abs _ goal) ← inferNormalisedType hole
      where meta x _ → blockOnMeta x
            _        → typeErrorS "Induction tactic must be applied to a function goal"
    hole₀ ← (a→0 goal `∘ hole) :′ unknown
    pi a b ← inferNormalisedType hole₀
      where meta x _ → blockOnMeta x
            _        → typeErrorS "Induction tactic must be applied to a function goal"
    let P = lam visible b
        inStepCxt : {A : Set} → TC A → TC A
        inStepCxt {_} = λ′ (vArg (quoteTerm Nat)) ∘
                        λ′ (vArg unknown)
    base ← unknown :′ unknown
    step ← inStepCxt $ unknown :′ unknown
    hole =′ 0→a goal `∘ def₃ (quote nat-induction)
                             P base (`λ $ `λ step)
    unify base =<< autosub-tactic =<< inferNormalisedType base
    inStepCxt (unify step =<< by-tactic (var₀ 0) =<< inferNormalisedType step)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module Issue550 where

data Box (A : Set) : Set where
  [_] : A → Box A

postulate
  A : Set
  B : Set
  b : B
  f : B -> A

⋯ : {{a : A}} → A
⋯ {{a = a}} = a

test : Box A
test =
  let a : A
      a = f b
  in [ ⋯ ]

-- should succeed.  Old message:
-- No variable of type A was found in scope.
-- when checking that the expression ⋯ has type A

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Base
open import HLevel

module Homotopy.Extensions.ToPropToConstSet {i}
  {A B : Set i} ⦃ B-is-set : is-set B ⦄
  (f : A → B) (f-is-const : ∀ a₁ a₂ → f a₁ ≡ f a₂) where

  open import Homotopy.Truncation
  open import Homotopy.Skeleton

  private
    skel : Set i
    skel = π₀ (skeleton₁ f)

    abstract
      skel-has-all-paths : has-all-paths skel
      skel-has-all-paths =
        π₀-extend ⦃ λ _ → Π-is-set λ _ → ≡-is-set $ π₀-is-set _ ⦄
          (skeleton₁-rec (λ s₁ → ∀ s₂ → proj s₁ ≡ s₂)
            (λ a₁ → π₀-extend ⦃ λ _ → ≡-is-set $ π₀-is-set _ ⦄
              (skeleton₁-rec (λ s₂ → proj (point a₁) ≡ proj s₂)
                (λ a₂ → ap proj $ link a₁ a₂ $ f-is-const a₁ a₂)
                (λ _ _ _ → prop-has-all-paths (π₀-is-set _ _ _) _ _)))
            (λ _ _ _ → funext λ _ → prop-has-all-paths (π₀-is-set _ _ _) _ _))

    skel-is-prop : is-prop skel
    skel-is-prop = all-paths-is-prop skel-has-all-paths

  cst-extend : [ A ] → B
  cst-extend = π₀-extend-nondep ⦃ B-is-set ⦄ skeleton₁-lifted
            ◯ []-extend-nondep ⦃ skel-is-prop ⦄ (proj ◯ point)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- The ATP pragma with the role <axiom> can be used with postulates.

module ATPAxiomPostulates where

postulate
  D    : Set
  zero : D
  succ : D → D
  N    : D → Set

postulate
  zN : N zero
  sN : ∀ {n} → N n → N (succ n)
{-# ATP axiom zN #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

module Tools.List where

open import Data.List public using (List; []; _∷_)

module L where
  open import Data.List public


text:
------------------------------------------------------------------------------
-- Conversion rules for the greatest common divisor
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Partial.ConversionRulesATP where

open import FOTC.Base
open import FOTC.Base.Loop
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Program.GCD.Partial.GCD

------------------------------------------------------------------------------
-- NB. These conversion rules are not used by the ATPs. They use the
-- official equation.
private
  postulate gcd-00 : gcd zero zero ≡ error
  {-# ATP prove gcd-00 #-}

  postulate gcd-S0 : ∀ n → gcd (succ₁ n) zero ≡ succ₁ n
  {-# ATP prove gcd-S0 #-}

  postulate gcd-0S : ∀ n → gcd zero (succ₁ n) ≡ succ₁ n
  {-# ATP prove gcd-0S #-}

  postulate
    gcd-S>S : ∀ m n → succ₁ m > succ₁ n →
              gcd (succ₁ m) (succ₁ n) ≡ gcd (succ₁ m ∸ succ₁ n) (succ₁ n)
  {-# ATP prove gcd-S>S #-}

  postulate
    gcd-S≯S : ∀ m n → succ₁ m ≯ succ₁ n →
              gcd (succ₁ m) (succ₁ n) ≡ gcd (succ₁ m) (succ₁ n ∸ succ₁ m)
  {-# ATP prove gcd-S≯S #-}


text:
-- Andreas, 2019-06-25, issue #3855 reported by nad
-- Constraint solver needs to respect erasure.

open import Agda.Builtin.Bool

module _ where

  record RB (b : Bool) : Set where
    bPar : Bool
    bPar = b

  myBPar : (@0 b : Bool) → RB b → Bool
  myBPar b r = RB.bPar {b = {!b!}} r         -- should be rejected