text:
{-

Technical results about row transformation applied to matrices

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Matrix.RowTransformation where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Nat hiding (_+_ ; _·_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma
open import Cubical.Data.Bool
open import Cubical.Data.FinData renaming (znots to znotsFin ; snotz to snotzFin)

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Matrix
open import Cubical.Algebra.RingSolver.Reflection

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.Reflection
open import Cubical.Algebra.Matrix.CommRingCoefficient

private
  variable
    ℓ : Level
    A : Type ℓ
    m n k l : ℕ

takeRows : FinMatrix A (suc (suc m)) n → FinMatrix A 2 n
takeRows M zero = M zero
takeRows M one  = M one

takeRowsᶜ : FinMatrix A (suc (suc m)) n → FinMatrix A (suc m) n
takeRowsᶜ M zero    = M zero
takeRowsᶜ M (suc i) = M (suc (suc i))

combRows : FinMatrix A (suc (suc m)) n → FinMatrix A 2 n → FinMatrix A (suc m) n
combRows M M₀ zero    = M₀ zero
combRows M M₀ (suc i) = M  (suc (suc i))

shufRows : FinMatrix A 2 n → FinMatrix A (suc m) n → FinMatrix A (suc (suc m)) n
shufRows M₀ M₁ zero = M₁ zero
shufRows M₀ M₁ one  = M₀ one
shufRows M₀ M₁ (suc (suc i)) = M₁ (suc i)

module _
  (T₀ : FinMatrix A 2 n → FinMatrix A 2 n)
  (M  : FinMatrix A (suc (suc m)) n) where

  private
    M₀ = T₀ (takeRows M)

  takeTrans : FinMatrix A (suc (suc m)) n
  takeTrans zero = M₀ zero
  takeTrans one  = M₀ one
  takeTrans (suc (suc i)) = M (suc (suc i))

module _
  (T₁ : FinMatrix A (suc m) n → FinMatrix A (suc m) n)
  (M  : FinMatrix A (suc (suc m)) n) where

  private
    M₁ = T₁ (takeRowsᶜ M)

  combTrans : FinMatrix A (suc (suc m)) n
  combTrans zero = M₁ zero
  combTrans one  = M  one
  combTrans (suc (suc i)) = M₁ (suc i)

module _
  (T₀ : FinMatrix A 2 n → FinMatrix A 2 n)
  (T₁ : FinMatrix A (suc m) n → FinMatrix A (suc m) n)
  (M  : FinMatrix A (suc (suc m)) n) where

  private
    M₀ = T₀ (takeRows M)
    M₁ = T₁ (combRows M M₀)

    helper : takeRowsᶜ (takeTrans T₀ M) ≡ combRows M M₀
    helper t zero    = M₀ zero
    helper t (suc i) = M (suc (suc i))

  takeCombShufRows : FinMatrix A (suc (suc m)) n
  takeCombShufRows = shufRows M₀ M₁

  takeCombShufEquiv : combTrans T₁ (takeTrans T₀ M) ≡ takeCombShufRows
  takeCombShufEquiv t zero = T₁ (helper t) zero
  takeCombShufEquiv t one  = M₀ one
  takeCombShufEquiv t (suc (suc i)) = T₁ (helper t) (suc i)

-- The iterated row transformation

module _
  (T : FinMatrix A 2 n → FinMatrix A 2 n) where

  transRows : FinMatrix A (suc m) n → FinMatrix A (suc m) n
  transRows {m = 0} M = M
  transRows {m = suc m} = takeCombShufRows T transRows

  -- Several induction principle to prove properties after transformation

  module _
    (invRow : (M : FinMatrix A 2 n) → M zero ≡ T M zero) where

    invRow₀ : (M : FinMatrix A (suc m) n) → M zero ≡ transRows M zero
    invRow₀ {m = 0}     _ = refl
    invRow₀ {m = suc m} M = invRow _ ∙ invRow₀ (combRows M _)

  module _
    (P : FinVec A n → Type ℓ)
    (indP : (M : FinMatrix A 2 n) → P (M zero) → P (T M zero)) where

    transRowsIndP : (M : FinMatrix A (suc m) n) → P (M zero) → P (transRows M zero)
    transRowsIndP {m = 0} _ h = h
    transRowsIndP {m = suc m} M h = transRowsIndP (combRows M _) (indP _ h)

  module _
    (P : FinVec A n → Type ℓ)
    (indP : (M : FinMatrix A 2 n) → P (T M one)) where

    transRowsIndP' : (M : FinMatrix A (suc m) n) → (i : Fin m) → P (transRows M (suc i))
    transRowsIndP' {m = suc m} M zero    = indP _
    transRowsIndP' {m = suc m} M (suc i) = transRowsIndP' _ i

  module _
    (Q : FinVec A n → Type ℓ)
    (P : FinVec A n → Type ℓ)
    (indQ : (M : FinMatrix A 2 n) → Q (M zero) → Q (T M zero))
    (indP : (M : FinMatrix A 2 n) → Q (M zero) → P (T M one )) where

    transRowsIndPQ : (M : FinMatrix A (suc m) n) → Q (M zero) → (i : Fin m) → P (transRows M (suc i))
    transRowsIndPQ {m = suc m} M p zero    = indP _ p
    transRowsIndPQ {m = suc m} M p (suc i) = transRowsIndPQ _ (indQ _ p) i

  module _
    (Q : FinVec A n → Type ℓ)
    (P : FinVec A n → Type ℓ)
    (indQ : (M : FinMatrix A 2 n) → Q (M zero) → Q (T M zero))
    (indP : (M : FinMatrix A 2 n) → P (M one ) → Q (T M zero)) where

    transRowsIndPQ' : (M : FinMatrix A (suc m) n) → (i : Fin m) → P (M (suc i)) → Q (transRows M zero)
    transRowsIndPQ' {m = suc m} M zero    p = transRowsIndP Q indQ (combRows M _) (indP _ p)
    transRowsIndPQ' {m = suc m} M (suc i) p = transRowsIndPQ' (combRows M _) _ p

  module _
    (Rel : FinVec A n → FinVec A n → Type ℓ)
    (indRel : (M : FinMatrix A 2 n) → Rel (M one) (T M one)) where

    transRowsIndRel : (M : FinMatrix A (suc m) n) → (i : Fin m) → Rel (M (suc i)) (transRows M (suc i))
    transRowsIndRel {m = suc m} M zero    = indRel _
    transRowsIndRel {m = suc m} M (suc i) = transRowsIndRel _ i

  module _
    (Rel3 : FinVec A n → FinVec A n → FinVec A n → Type ℓ)
    (invRow  : (M : FinMatrix A 2 n) → M zero ≡ T M zero)
    (indRel3 : (M : FinMatrix A 2 n) → Rel3 (M zero) (M one) (T M one)) where

    transRowsIndRel3 : (M : FinMatrix A (suc m) n) → (i : Fin m) → Rel3 (M zero) (M (suc i)) (transRows M (suc i))
    transRowsIndRel3 {m = suc m} M zero    = indRel3 _
    transRowsIndRel3 {m = suc m} M (suc i) =
      subst (λ V → Rel3 V (M (suc (suc i)))
        (transRows M (suc (suc i)))) (sym (invRow _)) (transRowsIndRel3 _ i)

  module _
    (Rel : FinVec A n → FinVec A n → Type ℓ)
    (indRel : (M : FinMatrix A 2 n) → Rel (M zero) (M one) → M zero ≡ T M zero) where

    transRowsIndRelInv :
        (M : FinMatrix A (suc m) n)
      → ((i : Fin m) → Rel (M zero) (M (suc i)))
      →  M zero ≡ transRows M zero
    transRowsIndRelInv {m = 0}     _ _   = refl
    transRowsIndRelInv {m = suc m} M rel =
      let invRow = indRel _ (rel zero)
          rel₁ = (λ i → subst (λ V → Rel V (M (suc (suc i)))) invRow (rel (suc i)))
      in  invRow ∙ transRowsIndRelInv _ rel₁

  module _
    (P : FinVec A n → Type ℓ)
    (Rel : FinVec A n → FinVec A n → Type ℓ)
    (indPRel : (M : FinMatrix A 2 n) → P (M zero) → Rel (M zero) (M one) → M zero ≡ T M zero) where

    transRowsIndPRelInv :
        (M : FinMatrix A (suc m) n)
      → P (M zero)
      → ((i : Fin m) → Rel (M zero) (M (suc i)))
      → M zero ≡ transRows M zero
    transRowsIndPRelInv {m = 0}     _ _ _   = refl
    transRowsIndPRelInv {m = suc m} M p rel =
      let invRow = indPRel _ p (rel zero)
          p₁   = subst P invRow p
          rel₁ = (λ i → subst (λ V → Rel V (M (suc (suc i)))) invRow (rel (suc i)))
      in  invRow ∙ transRowsIndPRelInv _ p₁ rel₁

  module _
    (P : FinVec A n → Type ℓ)
    (indP₀ : (M : FinMatrix A 2 n) → P (M zero) → P (M one) → P (T M zero))
    (indP₁ : (M : FinMatrix A 2 n) → P (M zero) → P (M one) → P (T M one )) where

    transRowsIndP₀ :
        (M : FinMatrix A (suc m) n)
      → P (M zero)
      → ((i : Fin m) → P (M (suc i)))
      → P (transRows M zero)
    transRowsIndP₀ {m = 0}     _ p _ = p
    transRowsIndP₀ {m = suc m} _ p q = transRowsIndP₀ _ (indP₀ _ p (q zero)) (q ∘ suc)

    transRowsIndP₁ :
        (M : FinMatrix A (suc m) n)
      → P (M zero)
      → ((i : Fin m) → P (M (suc i)))
      →  (i : Fin m) → P (transRows M (suc i))
    transRowsIndP₁ {m = 0}     _ _ q = q
    transRowsIndP₁ {m = suc m} _ p q zero    = indP₁ _ p (q zero)
    transRowsIndP₁ {m = suc m} M p q (suc i) = transRowsIndP₁ _ (indP₀ _ p (q zero)) (q ∘ suc) i

-- Row transformation of linear coefficient matrices

module LinearTransformation (𝓡 : CommRing ℓ) where

  private
    R = 𝓡 .fst
    𝑹 = CommRing→Ring 𝓡
    AbR = Ring→AbGroup 𝑹

  open CommRingStr       (𝓡 .snd) renaming ( is-set to isSetR )
  open CommRingTheory     𝓡
  open RingTheory         𝑹
  open KroneckerDelta     𝑹
  open Sum                𝑹

  open Coefficient        𝓡

  -- Definition of linear transformation

  record isLinear2×2 (T : Mat 2 n → Mat 2 n) : Type ℓ where
    field
      transMat : (M : Mat 2 n) → Mat 2 2
      transEq  : (M : Mat 2 n) → T M ≡ transMat M ⋆ M

  record isLinear (T : Mat m n → Mat k n) : Type ℓ where
    field
      transMat : (M : Mat m n) → Mat k m
      transEq  : (M : Mat m n) → T M ≡ transMat M ⋆ M

  open isLinear2×2
  open isLinear

  isLinearId : isLinear {m = m} {n = n} (idfun _)
  isLinearId .transMat _ = 𝟙
  isLinearId .transEq  _ = sym (⋆lUnit _)

  isInvId : (M : Mat (suc m) (suc n)) → isInv (isLinearId .transMat M)
  isInvId _ = isInv𝟙

  module _
    {T₁ : Mat (suc m) (suc n) → Mat (suc k) (suc n)}
    {T₂ : Mat (suc k) (suc n) → Mat (suc l) (suc n)}
    (isLinearT₁ : isLinear T₁)
    (isLinearT₂ : isLinear T₂) where

    isLinearComp : isLinear (T₂ ∘ T₁)
    isLinearComp .transMat M =
      let T₁M = isLinearT₁ .transMat M in
      isLinearT₂ .transMat (T₁ M) ⋆ T₁M
    isLinearComp .transEq  M =
        isLinearT₂ .transEq _
      ∙ (λ t → isLinearT₂ .transMat (T₁ M) ⋆ (isLinearT₁ .transEq M t))
      ∙ ⋆Assoc (isLinearT₂ .transMat _) (isLinearT₁ .transMat M) M

  module _
    {T₁ : Mat (suc m) (suc n) → Mat (suc m) (suc n)}
    {T₂ : Mat (suc m) (suc n) → Mat (suc m) (suc n)}
    (isLinearT₁ : isLinear T₁)
    (isLinearT₂ : isLinear T₂) where

    module _
      (isInvT₁ : (M : Mat (suc m) (suc n)) → isInv (isLinearT₁ .transMat M))
      (isInvT₂ : (M : Mat (suc m) (suc n)) → isInv (isLinearT₂ .transMat M)) where

      isInvComp : (M : Mat (suc m) (suc n)) → isInv (isLinearComp isLinearT₁ isLinearT₂ .transMat M)
      isInvComp M =
        let T₁M = isLinearT₁ .transMat M in
        isInv⋆ {M = isLinearT₂ .transMat (T₁ M)} {M' = T₁M} (isInvT₂ (T₁ M)) (isInvT₁ M)

    module _
      (P : FinVec R (suc n) → Type ℓ)
      (indP : (M : Mat (suc m) (suc n)) → P (M zero) → P (T₁ M zero))
      (isInvT₁ : (M : Mat (suc m) (suc n)) → P (M zero) → isInv (isLinearT₁ .transMat M))
      (isInvT₂ : (M : Mat (suc m) (suc n)) → P (M zero) → isInv (isLinearT₂ .transMat M)) where

      isInvCompInd : (M : Mat (suc m) (suc n)) → P (M zero) → isInv (isLinearComp isLinearT₁ isLinearT₂ .transMat M)
      isInvCompInd M p =
        let T₁M = isLinearT₁ .transMat M in
        isInv⋆ {M = isLinearT₂ .transMat (T₁ M)} {M' = T₁M} (isInvT₂ (T₁ M) (indP _ p)) (isInvT₁ M p)

  -- Linearity of row transformation

  takeTransMat : Mat 2 2 → Mat (suc (suc m)) (suc (suc m))
  takeTransMat P zero zero = P zero zero
  takeTransMat P one  zero = P one  zero
  takeTransMat P zero one  = P zero one
  takeTransMat P one  one  = P one  one
  takeTransMat _ zero (suc (suc j)) = 0r
  takeTransMat _ one  (suc (suc j)) = 0r
  takeTransMat _ (suc (suc i)) zero = 0r
  takeTransMat _ (suc (suc i)) one  = 0r
  takeTransMat _ (suc (suc i)) (suc (suc j)) = 𝟙 i j

  takeTransMat𝟙 : takeTransMat {m = m} 𝟙 ≡ 𝟙
  takeTransMat𝟙 t zero zero = 1r
  takeTransMat𝟙 t one  zero = 0r
  takeTransMat𝟙 t zero one  = 0r
  takeTransMat𝟙 t one  one  = 1r
  takeTransMat𝟙 t zero (suc (suc j)) = 0r
  takeTransMat𝟙 t one  (suc (suc j)) = 0r
  takeTransMat𝟙 t (suc (suc i)) zero = 0r
  takeTransMat𝟙 t (suc (suc i)) one  = 0r
  takeTransMat𝟙 t (suc (suc i)) (suc (suc j)) = δ i j

  module _
    (M N : Mat 2 2) where

    ⋆TakeTransMat : takeTransMat M ⋆ takeTransMat N ≡ takeTransMat {m = m} (M ⋆ N)
    ⋆TakeTransMat {m = m} t zero zero =
      M zero zero · N zero zero + (M zero one · N one zero + ∑Mul0r {n = m} (λ i → 0r) t)
    ⋆TakeTransMat {m = m} t one  zero =
      M one  zero · N zero zero + (M one one  · N one zero + ∑Mul0r {n = m} (λ i → 0r) t)
    ⋆TakeTransMat {m = m} t zero one  =
      M zero zero · N zero one  + (M zero one · N one one  + ∑Mul0r {n = m} (λ i → 0r) t)
    ⋆TakeTransMat {m = m} t one  one  =
      M one  zero · N zero one  + (M one one  · N one one  + ∑Mul0r {n = m} (λ i → 0r) t)
    ⋆TakeTransMat t zero (suc (suc j)) =
      (helper (M zero zero) (M zero one ) _ ∙ ∑Mul0r (λ i → 𝟙 i j)) t
      where helper : (a b c : R) → a · 0r + (b · 0r + c) ≡ c
            helper = solve 𝓡
    ⋆TakeTransMat t one  (suc (suc j)) =
      (helper (M one  zero) (M one  one ) _ ∙ ∑Mul0r (λ i → 𝟙 i j)) t
      where helper : (a b c : R) → a · 0r + (b · 0r + c) ≡ c
            helper = solve 𝓡
    ⋆TakeTransMat t (suc (suc i)) zero =
      (helper (N zero zero) (N one  zero) _ ∙ ∑Mulr0 (λ j → 𝟙 i j)) t
      where helper : (a b c : R) → 0r · a + (0r · b + c) ≡ c
            helper = solve 𝓡
    ⋆TakeTransMat t (suc (suc i)) one  =
      (helper (N zero one ) (N one  one ) _ ∙ ∑Mulr0 (λ j → 𝟙 i j)) t
      where helper : (a b c : R) → 0r · a + (0r · b + c) ≡ c
            helper = solve 𝓡
    ⋆TakeTransMat t (suc (suc i)) (suc (suc j)) =
        (helper _
      ∙ (λ t → ⋆lUnit 𝟙 t i j)) t
      where helper : (c : R) → 0r · 0r + (0r · 0r + c) ≡ c
            helper = solve 𝓡

  module _
    (T₀ : Mat 2 (suc n) → Mat 2 (suc n))
    (isLinear2×2T₀ : isLinear2×2 T₀) where

    module _
      (M : Mat (suc (suc m)) (suc n)) where

      private
        P = isLinear2×2T₀ .transMat (takeRows M)

      takeTransEquiv : takeTrans T₀ M ≡ takeTransMat P ⋆ M
      takeTransEquiv t zero j =
        ((λ t → isLinear2×2T₀ .transEq (takeRows M) t zero j)
        ∙ mul2 P (takeRows M) _ _
        ∙ helper _ _
        ∙ (λ t → P zero zero · M zero j + (P zero one · M one j
               + ∑Mul0r (λ i → M (suc (suc i)) j) (~ t)))) t
        where helper : (a b : R) → a + b ≡ a + (b + 0r)
              helper = solve 𝓡
      takeTransEquiv t one  j =
        ((λ t → isLinear2×2T₀ .transEq (takeRows M) t one  j)
        ∙ mul2 P (takeRows M) _ _
        ∙ helper _ _
        ∙ (λ t → P one  zero · M zero j + (P one  one · M one j
               + ∑Mul0r (λ i → M (suc (suc i)) j) (~ t)))) t
        where helper : (a b : R) → a + b ≡ a + (b + 0r)
              helper = solve 𝓡
      takeTransEquiv t (suc (suc i)) j =
        ((λ t → ⋆lUnit (λ i j → M (suc (suc i)) j) (~ t) i j)
        ∙ helper (M zero j) (M one  j) _) t
        where helper : (a b c : R) → c ≡ 0r · a + (0r · b + c)
              helper = solve 𝓡

    isLinearTakeRowsTrans : isLinear (takeTrans {m = m} T₀)
    isLinearTakeRowsTrans .transMat M = takeTransMat _
    isLinearTakeRowsTrans .transEq    = takeTransEquiv

  isInvTakeTransMat : (M : Mat 2 2)(isInvM : isInv M) → isInv (takeTransMat {m = m} M)
  isInvTakeTransMat M isInvM .fst = takeTransMat (isInvM .fst)
  isInvTakeTransMat M isInvM .snd .fst =
    ⋆TakeTransMat _ _ ∙ (λ t → takeTransMat (isInvM .snd .fst t)) ∙ takeTransMat𝟙
  isInvTakeTransMat M isInvM .snd .snd =
    ⋆TakeTransMat _ _ ∙ (λ t → takeTransMat (isInvM .snd .snd t)) ∙ takeTransMat𝟙

  combTransMat : Mat (suc m) (suc m) → Mat (suc (suc m)) (suc (suc m))
  combTransMat P zero zero = P zero zero
  combTransMat _ zero one  = 0r
  combTransMat _ one  zero = 0r
  combTransMat _ one  one  = 1r
  combTransMat P zero (suc (suc j)) = P zero (suc j)
  combTransMat _ one  (suc (suc j)) = 0r
  combTransMat P (suc (suc i)) zero = P (suc i) zero
  combTransMat _ (suc (suc i)) one  = 0r
  combTransMat P (suc (suc i)) (suc (suc j)) = P (suc i) (suc j)

  combTransMat𝟙 : combTransMat {m = m} 𝟙 ≡ 𝟙
  combTransMat𝟙 t zero zero = 1r
  combTransMat𝟙 t zero one  = 0r
  combTransMat𝟙 t one  zero = 0r
  combTransMat𝟙 t one  one  = 1r
  combTransMat𝟙 t zero (suc (suc j)) = 0r
  combTransMat𝟙 t one  (suc (suc j)) = 0r
  combTransMat𝟙 t (suc (suc i)) zero = 0r
  combTransMat𝟙 t (suc (suc i)) one  = 0r
  combTransMat𝟙 t (suc (suc i)) (suc (suc j)) = δ i j

  module _
    (M N : Mat (suc m) (suc m)) where

    ⋆CombTransMat : combTransMat M ⋆ combTransMat N ≡ combTransMat (M ⋆ N)
    ⋆CombTransMat t zero zero =
      helper (M zero zero · N zero zero) (∑ (λ l → M zero (suc l) · N (suc l) zero)) t
      where helper : (a c : R) → a + (0r · 0r + c) ≡ a + c
            helper = solve 𝓡
    ⋆CombTransMat t zero one  =
      (helper (M zero zero) _ ∙ ∑Mulr0 (λ j → M zero (suc j))) t
      where helper : (a c : R) → a · 0r + (0r · 1r + c) ≡ c
            helper = solve 𝓡
    ⋆CombTransMat t one  zero =
      (helper (N zero zero) _ ∙ ∑Mul0r (λ i → N (suc i) zero)) t
      where helper : (a c : R) → 0r · a + (1r · 0r + c) ≡ c
            helper = solve 𝓡
    ⋆CombTransMat t one  one  =
      ((λ t → 0r · 0r + (1r · 1r + ∑Mul0r {n = m} (λ i → 0r) t))
      ∙ helper) t
      where helper : 0r · 0r + (1r · 1r + 0r) ≡ 1r
            helper = solve 𝓡
    ⋆CombTransMat t zero (suc (suc j)) =
      helper (M zero zero · N zero (suc j)) (∑ (λ l → M zero (suc l) · N (suc l) (suc j))) t
      where helper : (a c : R) → a + (0r · 0r + c) ≡ a + c
            helper = solve 𝓡
    ⋆CombTransMat t one  (suc (suc j)) =
      (helper (N zero (suc j)) _ ∙ ∑Mul0r (λ i → N (suc i) (suc j))) t
      where helper : (a c : R) → 0r · a + (1r · 0r + c) ≡ c
            helper = solve 𝓡
    ⋆CombTransMat t (suc (suc i)) zero =
      helper (M (suc i) zero · N zero zero) (∑ (λ l → M (suc i) (suc l) · N (suc l) zero)) t
      where helper : (a c : R) → a + (0r · 0r + c) ≡ a + c
            helper = solve 𝓡
    ⋆CombTransMat t (suc (suc i)) one  =
      (helper (M (suc i) zero) _ ∙ ∑Mulr0 (λ j → M (suc i) (suc j))) t
      where helper : (a c : R) → a · 0r + (0r · 1r + c) ≡ c
            helper = solve 𝓡
    ⋆CombTransMat t (suc (suc i)) (suc (suc j)) =
      helper (M (suc i) zero · N zero (suc j)) (∑ (λ l → M (suc i) (suc l) · N (suc l) (suc j))) t
      where helper : (a c : R) → a + (0r · 0r + c) ≡ a + c
            helper = solve 𝓡

  module _
    (T₁ : Mat (suc m) (suc n) → Mat (suc m) (suc n))
    (isLinearT₁ : isLinear T₁) where

    module _
      (M : Mat (suc (suc m)) (suc n)) where

      private
        P = isLinearT₁ .transMat (takeRowsᶜ M)

      combTransEquiv : combTrans T₁ M ≡ combTransMat P ⋆ M
      combTransEquiv t zero j =
        ((λ t → isLinearT₁ .transEq (takeRowsᶜ M) t zero j)
        ∙ helper _ (M one j) _) t
        where helper : (a b c : R) → a + c ≡ a + (0r · b + c)
              helper = solve 𝓡
      combTransEquiv t one  j =
          (helper _ _
        ∙ (λ t → 0r · M zero j + (1r · M one j
               + ∑Mul0r (λ i → M (suc (suc i)) j) (~ t)))) t
        where helper : (a b : R) → b ≡ 0r · a + (1r · b + 0r)
              helper = solve 𝓡
      combTransEquiv t (suc (suc i)) j =
        ((λ t → isLinearT₁ .transEq (takeRowsᶜ M) t (suc i) j)
        ∙ helper _ (M one j) _) t
        where helper : (a b c : R) → a + c ≡ a + (0r · b + c)
              helper = solve 𝓡

    isLinearCombRowsTrans : isLinear (combTrans T₁)
    isLinearCombRowsTrans .transMat M = combTransMat _
    isLinearCombRowsTrans .transEq    = combTransEquiv

  isInvCombTransMat : (M : Mat (suc m) (suc m))(isInvM : isInv M) → isInv (combTransMat M)
  isInvCombTransMat M isInvM .fst = combTransMat (isInvM .fst)
  isInvCombTransMat M isInvM .snd .fst =
    ⋆CombTransMat _ _ ∙ (λ t → combTransMat (isInvM .snd .fst t)) ∙ combTransMat𝟙
  isInvCombTransMat M isInvM .snd .snd =
    ⋆CombTransMat _ _ ∙ (λ t → combTransMat (isInvM .snd .snd t)) ∙ combTransMat𝟙

  module _
    {T₁ : Mat 2 (suc n) → Mat 2 (suc n)}
    {T₂ : Mat (suc m) (suc n) → Mat (suc m) (suc n)}
    (isLinearT₁ : isLinear2×2 T₁)
    (isLinearT₂ : isLinear    T₂) where

    private
      compL = isLinearComp (isLinearTakeRowsTrans _ isLinearT₁) (isLinearCombRowsTrans _ isLinearT₂)

    isLinearTakeCombShufRows : isLinear (takeCombShufRows {m = m} T₁ T₂)
    isLinearTakeCombShufRows .transMat   = compL .transMat
    isLinearTakeCombShufRows .transEq  M = sym (takeCombShufEquiv _ _ _) ∙ compL .transEq _

  module _
    (T : Mat 2 (suc n) → Mat 2 (suc n))
    (isLinear2×2T : isLinear2×2 T) where

    isLinearTransRows : (m : ℕ) → isLinear (transRows T {m = m})
    isLinearTransRows 0       = isLinearId
    isLinearTransRows (suc m) = isLinearTakeCombShufRows isLinear2×2T (isLinearTransRows m)

    module _
      (isInvT : (M : Mat 2 (suc n)) → isInv (isLinear2×2T .transMat M)) where

      isInvTransRows : (M : Mat (suc m) (suc n)) → isInv (isLinearTransRows _ .transMat M)
      isInvTransRows {m = 0}     _ = isInv𝟙
      isInvTransRows {m = suc m} M =
        isInv⋆ {M = combTransMat _} {M' = takeTransMat _}
               (isInvCombTransMat _ (isInvTransRows _))
               (isInvTakeTransMat _ (isInvT _))

    module _
      (P : FinVec R (suc n) → Type ℓ)
      (indP   : (M : Mat 2 (suc n)) → P (M zero) → P (T M zero))
      (isInvT : (M : Mat 2 (suc n)) → P (M zero) → isInv (isLinear2×2T .transMat M)) where

      isInvTransRowsInd :
        (M : Mat (suc m) (suc n)) → P (M zero) → isInv (isLinearTransRows _ .transMat M)
      isInvTransRowsInd {m = 0} M _ = isInvId M
      isInvTransRowsInd {m = suc m} M p =
        isInv⋆ {M = combTransMat _} {M' = takeTransMat _}
               (isInvCombTransMat _ (isInvTransRowsInd _ (indP _ p)))
               (isInvTakeTransMat _ (isInvT _ p))

  -- Some useful properties of 2-rows transformation

  symδ : (i j : Fin m) → δ i j ≡ δ j i
  symδ zero    zero    = refl
  symδ zero    (suc _) = refl
  symδ (suc _) zero    = refl
  symδ (suc i) (suc j) = symδ i j

  diagδ : (i j : Fin m)(p : i ≡ j) → δ i j ≡ 1r
  diagδ zero    zero    _ = refl
  diagδ (suc _) zero    p = Empty.rec (snotzFin p)
  diagδ zero    (suc _) p = Empty.rec (znotsFin p)
  diagδ (suc i) (suc j) p = diagδ _ _ (injSucFin p)

  skewδ : (i j : Fin m)(p : ¬ i ≡ j) → δ i j ≡ 0r
  skewδ zero    zero    p = Empty.rec (p refl)
  skewδ (suc _) zero    _ = refl
  skewδ zero    (suc _) _ = refl
  skewδ (suc i) (suc j) p = skewδ _ _ (λ r → p (cong suc r))

  diagSet : (i₀ : Fin m)(a : R) → Mat m m
  diagSet {m = suc m} zero a zero    zero    = a
  diagSet {m = suc m} zero _ (suc i) zero    = 0r
  diagSet {m = suc m} zero _ zero    (suc j) = 0r
  diagSet {m = suc m} zero _ (suc i) (suc j) = δ i j
  diagSet {m = suc m} (suc i₀) _ zero    zero    = 1r
  diagSet {m = suc m} (suc i₀) _ (suc i) zero    = 0r
  diagSet {m = suc m} (suc i₀) _ zero    (suc j) = 0r
  diagSet {m = suc m} (suc i₀) a (suc i) (suc j) = diagSet i₀ a i j

  diagSet≡diagSetᵗ : (i₀ : Fin m)(a : R) → diagSet i₀ a ≡ (diagSet i₀ a)ᵗ
  diagSet≡diagSetᵗ {m = suc m} zero a t zero    zero    = a
  diagSet≡diagSetᵗ {m = suc m} zero _ t (suc i) zero    = 0r
  diagSet≡diagSetᵗ {m = suc m} zero _ t zero    (suc j) = 0r
  diagSet≡diagSetᵗ {m = suc m} zero _ t (suc i) (suc j) = symδ i j t
  diagSet≡diagSetᵗ {m = suc m} (suc i₀) _ t zero    zero    = 1r
  diagSet≡diagSetᵗ {m = suc m} (suc i₀) _ t (suc i) zero    = 0r
  diagSet≡diagSetᵗ {m = suc m} (suc i₀) _ t zero    (suc j) = 0r
  diagSet≡diagSetᵗ {m = suc m} (suc i₀) a t (suc i) (suc j) = diagSet≡diagSetᵗ i₀ a t i j

  diagSet1≡𝟙 : (i₀ : Fin m) → diagSet i₀ 1r ≡ 𝟙
  diagSet1≡𝟙 {m = suc m} zero t zero    zero    = 1r
  diagSet1≡𝟙 {m = suc m} zero t (suc i) zero    = 0r
  diagSet1≡𝟙 {m = suc m} zero t zero    (suc j) = 0r
  diagSet1≡𝟙 {m = suc m} zero t (suc i) (suc j) = δ i j
  diagSet1≡𝟙 {m = suc m} (suc i₀) t zero    zero    = 1r
  diagSet1≡𝟙 {m = suc m} (suc i₀) t (suc i) zero    = 0r
  diagSet1≡𝟙 {m = suc m} (suc i₀) t zero    (suc j) = 0r
  diagSet1≡𝟙 {m = suc m} (suc i₀) t (suc i) (suc j) = diagSet1≡𝟙 i₀ t i j

  module _
    (a b c : R) where

    ·DiagSetˡ : (i₀ : Fin m)(i : Fin m) → a · δ i₀ i + diagSet i₀ b i i₀ · c ≡ (a + (b · c + 0r)) · δ i₀ i
    ·DiagSetˡ {m = suc m} zero     zero    = helper _ _ _
      where helper : (a b c : R) → a · 1r + b · c ≡ (a + (b · c + 0r)) · 1r
            helper = solve 𝓡
    ·DiagSetˡ {m = suc m} (suc i₀) zero    = helper _ _ _
      where helper : (a b c : R) → a · 0r + 0r · c ≡ (a + (b · c + 0r)) · 0r
            helper = solve 𝓡
    ·DiagSetˡ {m = suc m} zero     (suc j) = helper _ _ _
      where helper : (a b c : R) → a · 0r + 0r · c ≡ (a + (b · c + 0r)) · 0r
            helper = solve 𝓡
    ·DiagSetˡ {m = suc m} (suc i₀) (suc j) = ·DiagSetˡ i₀ j

    ·DiagSetʳ : (i₀ : Fin m)(i : Fin m) → a · δ i₀ i + b · diagSet i₀ c i₀ i ≡ (a + (b · c + 0r)) · δ i₀ i
    ·DiagSetʳ {m = suc m} zero     zero    = helper _ _ _
      where helper : (a b c : R) → a · 1r + b · c ≡ (a + (b · c + 0r)) · 1r
            helper = solve 𝓡
    ·DiagSetʳ {m = suc m} (suc i₀) zero    = helper _ _ _
      where helper : (a b c : R) → a · 0r + b · 0r ≡ (a + (b · c + 0r)) · 0r
            helper = solve 𝓡
    ·DiagSetʳ {m = suc m} zero     (suc j) = helper _ _ _
      where helper : (a b c : R) → a · 0r + b · 0r ≡ (a + (b · c + 0r)) · 0r
            helper = solve 𝓡
    ·DiagSetʳ {m = suc m} (suc i₀) (suc j) = ·DiagSetʳ i₀ j

  module _
    (a b : R) where

    ⋆DiagSet : (i₀ : Fin m) → diagSet i₀ a ⋆ diagSet i₀ b ≡ diagSet i₀ (a · b)
    ⋆DiagSet {m = suc m} zero t zero    zero    =
      ((λ t → a · b + ∑Mul0r {n = m} (λ i → 0r) t) ∙ helper _) t
      where helper : (a : R) → a + 0r ≡ a
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} zero t (suc i) zero    =
      ((λ t → 0r · b + ∑Mulr0 (λ j → diagSet zero a (suc i) (suc j)) t) ∙ helper _) t
      where helper : (b : R) → 0r · b + 0r ≡ 0r
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} zero t zero    (suc j) =
      ((λ t → a · 0r + ∑Mul0r (λ i → diagSet zero b (suc i) (suc j)) t) ∙ helper _) t
      where helper : (a : R) → a · 0r + 0r ≡ 0r
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} zero t (suc i) (suc j) =
      ((λ t → 0r · 0r + ∑Mulr1 _ (λ l → δ i l) j t) ∙ helper _) t
      where helper : (d : R) → 0r · 0r + d ≡ d
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} (suc i₀) t zero    zero    =
      ((λ t → 1r · 1r + ∑Mul0r {n = m} (λ i → 0r) t) ∙ helper) t
      where helper : 1r · 1r + 0r ≡ 1r
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} (suc i₀) t (suc i) zero    =
      ((λ t → 0r · 1r + ∑Mulr0 (λ j → diagSet (suc i₀) a (suc i) (suc j)) t) ∙ helper) t
      where helper : 0r · 1r + 0r ≡ 0r
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} (suc i₀) t zero    (suc j) =
      ((λ t → 1r · 0r + ∑Mul0r (λ i → diagSet (suc i₀) b (suc i) (suc j)) t) ∙ helper) t
      where helper : 1r · 0r + 0r ≡ 0r
            helper = solve 𝓡
    ⋆DiagSet {m = suc m} (suc i₀) t (suc i) (suc j) =
      ((λ t → 0r · 0r + ⋆DiagSet i₀ t i j) ∙ helper _) t
      where helper : (a : R) → 0r · 0r + a ≡ a
            helper = solve 𝓡

  module _
    (a b c : R) where

    +DiagSet :
        (i₀ i j : Fin m)
      → (a · δ i₀ i) · (b · δ i₀ j) + diagSet i₀ c i j ≡ diagSet i₀ (a · b + (c + 0r)) i j
    +DiagSet {m = suc m} zero zero    zero    = helper _ _ _
      where helper : (a b c : R) → (a · 1r) · (b · 1r) + c ≡ a · b + (c + 0r)
            helper = solve 𝓡
    +DiagSet {m = suc m} zero (suc i) zero    = helper _ _
      where helper : (a b : R) → (a · 0r) · (b · 1r) + 0r ≡ 0r
            helper = solve 𝓡
    +DiagSet {m = suc m} zero zero    (suc j) = helper _ _
      where helper : (a b : R) → (a · 1r) · (b · 0r) + 0r ≡ 0r
            helper = solve 𝓡
    +DiagSet {m = suc m} zero (suc i) (suc j) = helper _ _ _
      where helper : (a b d : R) → (a · 0r) · (b · 0r) + d ≡ d
            helper = solve 𝓡
    +DiagSet {m = suc m} (suc i₀) zero    zero    = helper _ _
      where helper : (a b : R) → (a · 0r) · (b · 0r) + 1r ≡ 1r
            helper = solve 𝓡
    +DiagSet {m = suc m} (suc i₀) (suc i) zero    = helper _ _
      where helper : (a b : R) → a · (b · 0r) + 0r ≡ 0r
            helper = solve 𝓡
    +DiagSet {m = suc m} (suc i₀) zero    (suc j) = helper _ _
      where helper : (a b : R) → (a · 0r) · b + 0r ≡ 0r
            helper = solve 𝓡
    +DiagSet {m = suc m} (suc i₀) (suc i) (suc j) = +DiagSet i₀ i j

  module _
    (M : Mat 2 2)(i₀ : Fin m) where

    trans2RowsMat : Mat (suc m) (suc m)
    trans2RowsMat zero    zero    = M zero zero
    trans2RowsMat (suc i) zero    = M one zero · δ i₀ i
    trans2RowsMat zero    (suc j) = M zero one · δ i₀ j
    trans2RowsMat (suc i) (suc j) = diagSet i₀ (M one one) i j

  module _
    (i₀ : Fin m) where

    trans2RowsMat𝟙 : trans2RowsMat 𝟙 i₀ ≡ 𝟙
    trans2RowsMat𝟙 t zero    zero    = 1r
    trans2RowsMat𝟙 t (suc i) zero    = 0LeftAnnihilates (δ i₀ i) t
    trans2RowsMat𝟙 t zero    (suc j) = 0LeftAnnihilates (δ i₀ j) t
    trans2RowsMat𝟙 t (suc i) (suc j) = diagSet1≡𝟙 i₀ t i j

  module _
    (M N : Mat 2 2)(i₀ : Fin m) where

    private
      ∑helper00 : (x a b : R) → x + ∑(λ l → (a · δ i₀ l) · (b · δ i₀ l)) ≡ x + a · b
      ∑helper00 x a b =
          (λ t → x + ∑(λ l → helper a b (δ i₀ l) (δ i₀ l) t))
        ∙ (λ t → x + ∑Mul1r _ (λ l → (δ i₀ l · (a · b))) i₀ t)
        ∙ (λ t → x + diagδ i₀ i₀ refl t · (a · b))
        ∙ (λ t → x + ·Lid (a · b) t)
        where helper : (a b x y : R) → (a · x) · (b · y) ≡ x · (y · (a · b))
              helper = solve 𝓡

      ∑helper10 :
          (a b c : R)(K : Mat m m)(i : Fin m)
        → (a · δ i₀ i) · b + ∑ (λ l → K i l · (c · δ i₀ l)) ≡ (a · b) · δ i₀ i + K i i₀ · c
      ∑helper10 a b c K i =
          (λ t → helper1 a b (δ i₀ i) t + ∑ (λ l → helper2 (K i l) c (δ i₀ l) t))
        ∙ (λ t → (a · b) · δ i₀ i + ∑Mul1r _ (λ l → K i l · c) i₀ t)
        where helper1 : (a b c : R) → (a · c) · b ≡ (a · b) · c
              helper1 = solve 𝓡
              helper2 : (a b c : R) → a · (b · c) ≡ c · (a · b)
              helper2 = solve 𝓡

      ∑helper01 :
          (a b c : R)(K : Mat m m)(i : Fin m)
        → a · (b · δ i₀ i) + ∑ (λ l → (c · δ i₀ l) · K l i) ≡ (a · b) · δ i₀ i + c · K i₀ i
      ∑helper01 a b c K i =
          (λ t → helper1 a b (δ i₀ i) t + ∑ (λ l → helper2 c (K l i) (δ i₀ l) t))
        ∙ (λ t → (a · b) · δ i₀ i + ∑Mul1r _ (λ l → c · K l i) i₀ t)
        where helper1 : (a b c : R) → a · (b · c) ≡ (a · b) · c
              helper1 = solve 𝓡
              helper2 : (a b c : R) → (a · c) · b ≡ c · (a · b)
              helper2 = solve 𝓡

    ⋆Trans2RowsMat : trans2RowsMat M i₀ ⋆ trans2RowsMat N i₀ ≡ trans2RowsMat (M ⋆ N) i₀
    ⋆Trans2RowsMat t zero    zero    =
      (∑helper00 _ _ _ ∙ sym (mul2 M N zero zero)) t
    ⋆Trans2RowsMat t (suc i) zero    =
       (∑helper10 (M one  zero) (N zero zero)
                  (N one  zero) (diagSet i₀ (M one one)) i
      ∙ ·DiagSetˡ _ _ _ i₀ i) t
    ⋆Trans2RowsMat t zero    (suc j) =
       (∑helper01 (M zero zero) (N zero one)
                  (M zero one ) (diagSet i₀ (N one one)) j
      ∙ ·DiagSetʳ _ _ _ i₀ j) t
    ⋆Trans2RowsMat t (suc i) (suc j) =
      ((λ t → (M one zero · δ i₀ i) · (N zero one · δ i₀ j)
              + ⋆DiagSet (M one one) (N one one) i₀ t i j)
      ∙ +DiagSet _ _ _ i₀ i j) t

  isInvTrans2RowsMat : (M : Mat 2 2)(i₀ : Fin m)(isInvM : isInv M) → isInv (trans2RowsMat M i₀)
  isInvTrans2RowsMat M i₀ isInvM .fst = trans2RowsMat (isInvM .fst) i₀
  isInvTrans2RowsMat M i₀ isInvM .snd .fst =
    ⋆Trans2RowsMat _ _ _ ∙ (λ t → trans2RowsMat (isInvM .snd .fst t) i₀) ∙ trans2RowsMat𝟙 _
  isInvTrans2RowsMat M i₀ isInvM .snd .snd =
    ⋆Trans2RowsMat _ _ _ ∙ (λ t → trans2RowsMat (isInvM .snd .snd t) i₀) ∙ trans2RowsMat𝟙 _

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- AVL trees
------------------------------------------------------------------------

-- AVL trees are balanced binary search trees. The search tree
-- invariant is not statically enforced in the current implementation,
-- just the balance invariant.

open import Relation.Binary

module Data.AVL (OrderedKeySet : StrictTotalOrder)
                (Value : StrictTotalOrder.carrier OrderedKeySet → Set)
                where

open import Data.Nat hiding (compare)
open StrictTotalOrder OrderedKeySet renaming (carrier to Key)
open import Data.Product
open import Data.Maybe
open import Data.Bool
open import Data.List as List using (List)
import Data.DifferenceList as DiffList
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Types and functions which are used to keep track of invariants

module Invariants where

  -- Bits. (I would use Fin 2 instead if Agda had "defined patterns",
  -- so that I could pattern match on 1# instead of suc zero; the text
  -- "suc zero" takes up a lot more space.)

  data ℕ₂ : Set where
    0# : ℕ₂
    1# : ℕ₂

  -- Addition.

  infixl 6 _⊕_

  _⊕_ : ℕ₂ → ℕ → ℕ
  0# ⊕ n = n
  1# ⊕ n = 1 + n

  -- i ⊕ n -1 = pred (i ⊕ n).

  _⊕_-1 : ℕ₂ → ℕ → ℕ
  i ⊕ zero  -1 = 0
  i ⊕ suc n -1 = i ⊕ n

  infix 4 _∼_

  -- If m ∼ n, then the difference between m and n is at most 1. _∼_
  -- is used to record the balance factor of the AVL trees, and also
  -- to ensure that the absolute value of the balance factor is never
  -- more than 1.

  data _∼_ : ℕ → ℕ → Set where
    ∼+ : ∀ {n} →     n ∼ 1 + n
    ∼0 : ∀ {n} →     n ∼ n
    ∼- : ∀ {n} → 1 + n ∼ n

  -- The maximum of m and n.

  max : ∀ {m n} → m ∼ n → ℕ
  max (∼+ {n}) = 1 + n
  max (∼0 {n}) =     n
  max (∼- {n}) = 1 + n

  -- Some lemmas.

  1+ : ∀ {m n} → m ∼ n → 1 + m ∼ 1 + n
  1+ ∼+ = ∼+
  1+ ∼0 = ∼0
  1+ ∼- = ∼-

  max∼ : ∀ {i j} (bal : i ∼ j) → max bal ∼ i
  max∼ ∼+ = ∼-
  max∼ ∼0 = ∼0
  max∼ ∼- = ∼0

  ∼max : ∀ {i j} (bal : i ∼ j) → j ∼ max bal
  ∼max ∼+ = ∼0
  ∼max ∼0 = ∼0
  ∼max ∼- = ∼+

  max∼max : ∀ {i j} (bal : i ∼ j) → max (max∼ bal) ∼ max (∼max bal)
  max∼max ∼+ = ∼0
  max∼max ∼0 = ∼0
  max∼max ∼- = ∼0

  max-lemma : ∀ {m n} (bal : m ∼ n) →
              1 + max (1+ (max∼max bal)) ≡ 2 + max bal
  max-lemma ∼+ = refl
  max-lemma ∼0 = refl
  max-lemma ∼- = refl

------------------------------------------------------------------------
-- AVL trees

-- Key/value pairs.

KV : Set
KV = Σ Key Value

module Indexed where

  open Invariants

  -- The trees are indexed on their height. (bal is the balance
  -- factor.)

  data Tree : ℕ → Set where
    leaf : Tree 0
    node : ∀ {hˡ hʳ}
           (l : Tree hˡ) (k : KV) (r : Tree hʳ) (bal : hˡ ∼ hʳ) →
           Tree (1 + max bal)

  -- Various constant-time functions which construct trees out of
  -- smaller pieces, sometimes using rotation.

  joinˡ⁺ : ∀ {hˡ hʳ} →
           (∃ λ i → Tree (i ⊕ hˡ)) → KV → Tree hʳ → (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree (i ⊕ (1 + max bal))
  joinˡ⁺ (1# , node t₁ k₂
                 (node t₃ k₄ t₅ bal)
                             ∼+) k₆ t₇ ∼-  = (0# , subst Tree (max-lemma bal)
                                                     (node (node t₁ k₂ t₃ (max∼ bal))
                                                           k₄
                                                           (node t₅ k₆ t₇ (∼max bal))
                                                           (1+ (max∼max bal))))
  joinˡ⁺ (1# , node t₁ k₂ t₃ ∼-) k₄ t₅ ∼-  = (0# , node t₁ k₂ (node t₃ k₄ t₅ ∼0) ∼0)
  joinˡ⁺ (1# , node t₁ k₂ t₃ ∼0) k₄ t₅ ∼-  = (1# , node t₁ k₂ (node t₃ k₄ t₅ ∼-) ∼+)
  joinˡ⁺ (1# , t₁)               k₂ t₃ ∼0  = (1# , node t₁ k₂ t₃ ∼-)
  joinˡ⁺ (1# , t₁)               k₂ t₃ ∼+  = (0# , node t₁ k₂ t₃ ∼0)
  joinˡ⁺ (0# , t₁)               k₂ t₃ bal = (0# , node t₁ k₂ t₃ bal)

  joinʳ⁺ : ∀ {hˡ hʳ} →
           Tree hˡ → KV → (∃ λ i → Tree (i ⊕ hʳ)) → (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree (i ⊕ (1 + max bal))
  joinʳ⁺ t₁ k₂ (1# , node
                       (node t₃ k₄ t₅ bal)
                             k₆ t₇ ∼-) ∼+  = (0# , subst Tree (max-lemma bal)
                                                     (node (node t₁ k₂ t₃ (max∼ bal))
                                                           k₄
                                                           (node t₅ k₆ t₇ (∼max bal))
                                                           (1+ (max∼max bal))))
  joinʳ⁺ t₁ k₂ (1# , node t₃ k₄ t₅ ∼+) ∼+  = (0# , node (node t₁ k₂ t₃ ∼0) k₄ t₅ ∼0)
  joinʳ⁺ t₁ k₂ (1# , node t₃ k₄ t₅ ∼0) ∼+  = (1# , node (node t₁ k₂ t₃ ∼+) k₄ t₅ ∼-)
  joinʳ⁺ t₁ k₂ (1# , t₃)               ∼0  = (1# , node t₁ k₂ t₃ ∼+)
  joinʳ⁺ t₁ k₂ (1# , t₃)               ∼-  = (0# , node t₁ k₂ t₃ ∼0)
  joinʳ⁺ t₁ k₂ (0# , t₃)               bal = (0# , node t₁ k₂ t₃ bal)

  joinˡ⁻ : ∀ hˡ {hʳ} →
           (∃ λ i → Tree (i ⊕ hˡ -1)) → KV → Tree hʳ → (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree (i ⊕ max bal)
  joinˡ⁻ zero    (0# , t₁) k₂ t₃ bal = (1# , node t₁ k₂ t₃ bal)
  joinˡ⁻ zero    (1# , t₁) k₂ t₃ bal = (1# , node t₁ k₂ t₃ bal)
  joinˡ⁻ (suc _) (0# , t₁) k₂ t₃ ∼+  = joinʳ⁺ t₁ k₂ (1# , t₃) ∼+
  joinˡ⁻ (suc _) (0# , t₁) k₂ t₃ ∼0  = (1# , node t₁ k₂ t₃ ∼+)
  joinˡ⁻ (suc _) (0# , t₁) k₂ t₃ ∼-  = (0# , node t₁ k₂ t₃ ∼0)
  joinˡ⁻ (suc _) (1# , t₁) k₂ t₃ bal = (1# , node t₁ k₂ t₃ bal)

  joinʳ⁻ : ∀ {hˡ} hʳ →
           Tree hˡ → KV → (∃ λ i → Tree (i ⊕ hʳ -1)) → (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree (i ⊕ max bal)
  joinʳ⁻ zero    t₁ k₂ (0# , t₃) bal = (1# , node t₁ k₂ t₃ bal)
  joinʳ⁻ zero    t₁ k₂ (1# , t₃) bal = (1# , node t₁ k₂ t₃ bal)
  joinʳ⁻ (suc _) t₁ k₂ (0# , t₃) ∼-  = joinˡ⁺ (1# , t₁) k₂ t₃ ∼-
  joinʳ⁻ (suc _) t₁ k₂ (0# , t₃) ∼0  = (1# , node t₁ k₂ t₃ ∼-)
  joinʳ⁻ (suc _) t₁ k₂ (0# , t₃) ∼+  = (0# , node t₁ k₂ t₃ ∼0)
  joinʳ⁻ (suc _) t₁ k₂ (1# , t₃) bal = (1# , node t₁ k₂ t₃ bal)

  -- Extracts the smallest element from the tree, plus the rest.
  -- Logarithmic in the size of the tree.

  headTail : ∀ {h} → Tree (1 + h) →
             KV × ∃ λ i → Tree (i ⊕ h)
  headTail (node leaf k₁ t₂ ∼+) = (k₁ , 0# , t₂)
  headTail (node leaf k₁ t₂ ∼0) = (k₁ , 0# , t₂)
  headTail (node {hˡ = suc _} t₁₂ k₃ t₄ bal) with headTail t₁₂
  ... | (k₁ , t₂) = (k₁ , joinˡ⁻ _ t₂ k₃ t₄ bal)

  -- Extracts the largest element from the tree, plus the rest.
  -- Logarithmic in the size of the tree.

  initLast : ∀ {h} → Tree (1 + h) →
             ∃ (λ i → Tree (i ⊕ h)) × KV
  initLast (node t₁ k₂ leaf ∼-) = ((0# , t₁) , k₂)
  initLast (node t₁ k₂ leaf ∼0) = ((0# , t₁) , k₂)
  initLast (node {hʳ = suc _} t₁ k₂ t₃₄ bal) with initLast t₃₄
  ... | (t₃ , k₄) = (joinʳ⁻ _ t₁ k₂ t₃ bal , k₄)

  -- Another joining function. Logarithmic in the size of the tree.

  join : ∀ {hˡ hʳ} →
         Tree hˡ → Tree hʳ → (bal : hˡ ∼ hʳ) →
         ∃ λ i → Tree (i ⊕ max bal)
  join t₁ leaf ∼0 = (0# , t₁)
  join t₁ leaf ∼- = (0# , t₁)
  join {hʳ = suc _} t₁ t₂₃ bal with headTail t₂₃
  ... | (k₂ , t₃) = joinʳ⁻ _ t₁ k₂ t₃ bal

  -- An empty tree.

  empty : Tree 0
  empty = leaf

  -- A singleton tree.

  singleton : (k : Key) → Value k → Tree 1
  singleton k v = node leaf (k , v) leaf ∼0

  -- Inserts a key into the tree. If the key already exists, then it
  -- is replaced. Logarithmic in the size of the tree (assuming
  -- constant-time comparisons).

  insert : ∀ {h} → (k : Key) → Value k → Tree h →
           ∃ λ i → Tree (i ⊕ h)
  insert k v leaf             = (1# , singleton k v)
  insert k v (node l p r bal) with compare k (proj₁ p)
  ... | tri< _ _ _ = joinˡ⁺ (insert k v l) p r bal
  ... | tri≈ _ _ _ = (0# , node l (k , v) r bal)
  ... | tri> _ _ _ = joinʳ⁺ l p (insert k v r) bal

  -- Deletes the key/value pair containing the given key, if any.
  -- Logarithmic in the size of the tree (assuming constant-time
  -- comparisons).

  delete : ∀ {h} → Key → Tree h →
           ∃ λ i → Tree (i ⊕ h -1)
  delete k leaf             = (0# , leaf)
  delete k (node l p r bal) with compare k (proj₁ p)
  ... | tri< _ _ _ = joinˡ⁻ _ (delete k l) p r bal
  ... | tri≈ _ _ _ = join l r bal
  ... | tri> _ _ _ = joinʳ⁻ _ l p (delete k r) bal

  -- Looks up a key in the tree. Logarithmic in the size of the tree
  -- (assuming constant-time comparisons).

  lookup : ∀ {h} → (k : Key) → Tree h →
           Maybe (∃ λ k′ → Value k′ × k ≈ k′)
  lookup k leaf                  = nothing
  lookup k (node l (k′ , v) r _) with compare k k′
  ... | tri< _ _  _ = lookup k l
  ... | tri≈ _ eq _ = just (k′ , v , eq)
  ... | tri> _ _  _ = lookup k r

  -- Converts the tree to an ordered list. Linear in the size of the
  -- tree.

  open DiffList

  toDiffList : ∀ {h} → Tree h → DiffList KV
  toDiffList leaf           = []
  toDiffList (node l k r _) = toDiffList l ++ [ k ] ++ toDiffList r

------------------------------------------------------------------------
-- Types and functions with hidden indices

data Tree : Set where
  tree : ∀ {h} → Indexed.Tree h → Tree

empty : Tree
empty = tree Indexed.empty

singleton : (k : Key) → Value k → Tree
singleton k v = tree (Indexed.singleton k v)

insert : (k : Key) → Value k → Tree → Tree
insert k v (tree t) with Indexed.insert k v t
... | (_ , t′) = tree t′

delete : Key → Tree → Tree
delete k (tree t) with Indexed.delete k t
... | (_ , t′) = tree t′

lookup : (k : Key) → Tree → Maybe (∃ λ k′ → Value k′ × k ≈ k′)
lookup k (tree t) = Indexed.lookup k t

_∈?_ : Key → Tree → Bool
k ∈? t = maybeToBool (lookup k t)

headTail : Tree → Maybe (KV × Tree)
headTail (tree Indexed.leaf)  = nothing
headTail (tree {h = suc _} t) with Indexed.headTail t
... | (k , _ , t′) = just (k , tree t′)

initLast : Tree → Maybe (Tree × KV)
initLast (tree Indexed.leaf)  = nothing
initLast (tree {h = suc _} t) with Indexed.initLast t
... | ((_ , t′) , k) = just (tree t′ , k)

-- The input does not need to be ordered.

fromList : List KV → Tree
fromList = List.foldr (uncurry insert) empty

-- Returns an ordered list.

toList : Tree → List KV
toList (tree t) = DiffList.toList (Indexed.toDiffList t)

ext: agda

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module RandomAccessList.Zeroless.Core.Properties where

open import BuildingBlock
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)
open import RandomAccessList.Zeroless.Core

open import Data.Nat
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple

open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning
--------------------------------------------------------------------------------
-- On ⟦_⟧ and ⟦_⟧ₙ

-- identity
⟦[]⟧ₙ≡0 : ∀ {A n} → (xs : 1-2-RAL A n) → xs ≡ [] → ⟦ xs ⟧ₙ ≡ 0
⟦[]⟧ₙ≡0 []            p  = refl
⟦[]⟧ₙ≡0 (x 1∷ xs)     ()
⟦[]⟧ₙ≡0 (x , y 2∷ xs) ()

⟦[]⟧≡0 : ∀ {n A} → (xs : 1-2-RAL A n) → xs ≡ [] → ⟦ xs ⟧ ≡ 0
⟦[]⟧≡0 {zero}     [] p  = refl
⟦[]⟧≡0 {suc n}    [] p  = *-right-zero (2 * 2 ^ n)
⟦[]⟧≡0 (x     1∷ xs) ()
⟦[]⟧≡0 (x , y 2∷ xs) ()

{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------------
-- Inductive PA arithmetic properties using Agsy
------------------------------------------------------------------------------

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

-- Tested with the development version of the Agda standard library on
-- 02 February 2012.

module Agsy.PA.Inductive.Properties where

open import Data.Nat renaming ( suc to succ )

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

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

+-rightIdentity : ∀ n → n + zero ≡ n  -- via Agsy {-c}
+-rightIdentity zero     = refl
+-rightIdentity (succ n) = cong succ (+-rightIdentity n)

+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)  -- via Agsy {-c}
+-assoc zero     n o = refl
+-assoc (succ m) n o = cong succ (+-assoc m n o)

x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)  -- via Agsy {-c}
x+Sy≡S[x+y] zero     n = refl
x+Sy≡S[x+y] (succ m) n = cong succ (x+Sy≡S[x+y] m n)

+-comm : ∀ m n → m + n ≡ n + m  -- via Agsy {-c -m}
+-comm zero    n = sym (+-rightIdentity n)
+-comm (succ m) n =
  begin
    succ (m + n) ≡⟨ cong succ (+-comm m n) ⟩
    succ (n + m) ≡⟨ sym (x+Sy≡S[x+y] n m) ⟩
    n + succ m
  ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Categories.Functor.Instance.StrictCore where

-- The 'strict' core functor (from StrictCats to StrictGroupoids).
-- This is the right-adjoint of the forgetful functor from
-- StrictGroupoids to StrictCats
-- (see Categories.Functor.Adjoint.Instance.StrictCore)

open import Data.Product
open import Level using (_⊔_)
open import Function using (_on_; _$_) renaming (id to idf)
open import Relation.Binary.PropositionalEquality as ≡ using (cong; cong-id)

open import Categories.Category
import Categories.Category.Construction.Core as C
open import Categories.Category.Instance.StrictCats
open import Categories.Category.Instance.StrictGroupoids
open import Categories.Functor
open import Categories.Functor.Equivalence
open import Categories.Functor.Instance.Core renaming (Core to WeakCore)
open import Categories.Functor.Properties using ([_]-resp-≅)
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.HeterogeneousIdentity as HId
import Categories.Morphism.HeterogeneousIdentity.Properties as HIdProps
open import Categories.Morphism.IsoEquiv using (⌞_⌟)

Core : ∀ {o ℓ e} → Functor (Cats o ℓ e) (Groupoids o (ℓ ⊔ e) e)
Core {o} {ℓ} {e} = record
   { F₀ = F₀
   ; F₁ = F₁
   ; identity = λ {A} →
       record { eq₀ = λ _ → ≡.refl ; eq₁ = λ _ → ⌞ MR.id-comm-sym A ⌟ }
   ; homomorphism = λ {A B C} →
       record { eq₀ = λ _ → ≡.refl ; eq₁ = λ _ → ⌞ MR.id-comm-sym C ⌟ }
   ; F-resp-≈ = λ {A B F G} → CoreRespFEq {A} {B} {F} {G}
   }
   where
     open Functor WeakCore

     CoreRespFEq : {A B : Category o ℓ e} {F G : Functor A B} →
                   F ≡F G → F₁ F ≡F F₁ G
     CoreRespFEq {A} {B} {F} {G} F≡G = record
       { eq₀ = eq₀
       ; eq₁ = λ {X} {Y} f → ⌞ begin
           (from $ hid BC $ eq₀ Y) ∘ F.F₁ (from f)
         ≈⟨ ∘-resp-≈ˡ (hid-identity BC B from Equiv.refl (eq₀ Y)) ⟩
           (hid B $ ≡.cong idf $ eq₀ Y) ∘ F.F₁ (from f)
         ≡⟨ cong (λ p → hid B p ∘ _) (cong-id (eq₀ Y)) ⟩
           hid B (eq₀ Y) ∘ F.F₁ (from f)
         ≈⟨ eq₁ (from f) ⟩
           G.F₁ (from f) ∘ hid B (eq₀ X)
         ≡˘⟨ cong (λ p → _ ∘ hid B p) (cong-id (eq₀ X)) ⟩
           G.F₁ (from f) ∘ (hid B $ cong idf $ eq₀ X)
         ≈˘⟨ ∘-resp-≈ʳ (hid-identity BC B from Equiv.refl (eq₀ X)) ⟩
           G.F₁ (from f) ∘ (from $ hid BC $ eq₀ X)
         ∎ ⌟
       }
       where
         BC = C.Core B
         module F = Functor F
         module G = Functor G
         open Category B
         open HomReasoning hiding (refl)
         open HId
         open HIdProps
         open _≡F_ F≡G
         open Morphism._≅_

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition06 where

postulate
  D   : Set
  _≡_ : D → D → Set
  a c : D

b : D
b = a
{-# ATP definition b #-}

postulate
  foo : c ≡ b

-- We test the use of an ATP definition by a local hint.
postulate bar : c ≡ a
{-# ATP prove bar foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import Util.KVMap as Map
open import Util.Prelude

module LibraBFT.Impl.OBM.Prelude where

lookupOrInsert : ∀ {K V : Set} → K → V → Map.KVMap K V → Map.KVMap K V
lookupOrInsert k v m =
  if Map.kvm-member k m
  then m
  else Map.insert k v m


text:
-- 2012-10-20 Andreas
module Issue721b where

data Bool : Set where
  false true : Bool

record Foo (b : Bool) : Set where
  field
    _*_ : Bool → Bool → Bool

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

test : (F : Foo false) → let open Foo F in (x : Bool) → _*_ x ≡ (λ x → x)
test F x = x
  where open Foo F
-- Don't want to see any anonymous module

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- {-# OPTIONS -v tc.lhs:10 -v tc.lhs.split:50 #-}

postulate A : Set

record R : Set where
  field f : A

record S : Set where
  field f : A

test : _ → A
test record{f = a} = a

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Definition.Conversion.Stability where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Conversion
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Equality of contexts.
data ⊢_≡_ : (Γ Δ : Con Term) → Set where
  ε : ⊢ ε ≡ ε
  _∙_ : ∀ {Γ Δ A B r} → ⊢ Γ ≡ Δ → Γ ⊢ A ≡ B ^ r → ⊢ Γ ∙ A ^ r ≡ Δ ∙ B ^ r

mutual
  -- Syntactic validity and conversion substitution of a context equality.
  contextConvSubst : ∀ {Γ Δ} → ⊢ Γ ≡ Δ → ⊢ Γ × ⊢ Δ × Δ ⊢ˢ idSubst ∷ Γ
  contextConvSubst ε = ε , ε , id
  contextConvSubst (_∙_ {Γ} {Δ} {A} {B} Γ≡Δ A≡B) =
    let ⊢Γ , ⊢Δ , [σ] = contextConvSubst Γ≡Δ
        ⊢A , ⊢B = syntacticEq A≡B
        Δ⊢B = stability Γ≡Δ ⊢B
    in  ⊢Γ ∙ ⊢A , ⊢Δ ∙ Δ⊢B
        , (wk1Subst′ ⊢Γ ⊢Δ Δ⊢B [σ]
        , conv (var (⊢Δ ∙ Δ⊢B) here)
               (PE.subst (λ x → _ ⊢ _ ≡ x ^ _)
                         (wk1-tailId A)
                         (wkEq (step id) (⊢Δ ∙ Δ⊢B) (stabilityEq Γ≡Δ (sym A≡B)))))

  -- Stability of types under equal contexts.
  stability : ∀ {A rA Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ^ rA → Δ ⊢ A ^ rA
  stability Γ≡Δ A =
    let ⊢Γ , ⊢Δ , σ = contextConvSubst Γ≡Δ
        q = substitution A σ ⊢Δ
    in  PE.subst (λ x → _ ⊢ x ^ _) (subst-id _) q

  -- Stability of type equality.
  stabilityEq : ∀ {A B rA Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ≡ B ^ rA → Δ ⊢ A ≡ B ^ rA
  stabilityEq Γ≡Δ A≡B =
    let ⊢Γ , ⊢Δ , σ = contextConvSubst Γ≡Δ
        q = substitutionEq A≡B (substRefl σ) ⊢Δ
    in  PE.subst₂ (λ x y → _ ⊢ x ≡ y ^ _) (subst-id _) (subst-id _) q

-- Reflexivity of context equality.
reflConEq : ∀ {Γ} → ⊢ Γ → ⊢ Γ ≡ Γ
reflConEq ε = ε
reflConEq (⊢Γ ∙ ⊢A) = reflConEq ⊢Γ ∙ refl ⊢A

-- Symmetry of context equality.
symConEq : ∀ {Γ Δ} → ⊢ Γ ≡ Δ → ⊢ Δ ≡ Γ
symConEq ε = ε
symConEq (Γ≡Δ ∙ A≡B) = symConEq Γ≡Δ ∙ stabilityEq Γ≡Δ (sym A≡B)

-- Stability of terms.
stabilityTerm : ∀ {t A rA Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t ∷ A ^ rA → Δ ⊢ t ∷ A ^ rA
stabilityTerm Γ≡Δ t =
  let ⊢Γ , ⊢Δ , σ = contextConvSubst Γ≡Δ
      q = substitutionTerm t σ ⊢Δ
  in  PE.subst₂ (λ x y → _ ⊢ x ∷ y ^ _) (subst-id _) (subst-id _) q

-- Stability of term reduction.
stabilityRedTerm : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ → Γ ⊢ t ⇒ u ∷ A ^ l → Δ ⊢ t ⇒ u ∷ A ^ l
stabilityRedTerm Γ≡Δ (conv d x) =
  conv (stabilityRedTerm Γ≡Δ d) (stabilityEq Γ≡Δ x)
stabilityRedTerm Γ≡Δ (app-subst d x) =
  app-subst (stabilityRedTerm Γ≡Δ d) (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (β-red l< l<' x x₁ x₂) =
  β-red l< l<' (stability Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl x) x₁)
        (stabilityTerm Γ≡Δ x₂)
stabilityRedTerm Γ≡Δ (natrec-subst x x₁ x₂ d) =
  let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
  in  natrec-subst (stability (Γ≡Δ ∙ refl (univ (ℕⱼ ⊢Γ))) x) (stabilityTerm Γ≡Δ x₁)
                   (stabilityTerm Γ≡Δ x₂) (stabilityRedTerm Γ≡Δ d)
stabilityRedTerm Γ≡Δ (natrec-zero x x₁ x₂) =
  let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
  in  natrec-zero (stability (Γ≡Δ ∙ refl (univ (ℕⱼ ⊢Γ))) x) (stabilityTerm Γ≡Δ x₁)
                  (stabilityTerm Γ≡Δ x₂)
stabilityRedTerm Γ≡Δ (natrec-suc x x₁ x₂ x₃) =
  let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
  in  natrec-suc (stabilityTerm Γ≡Δ x) (stability (Γ≡Δ ∙ refl (univ (ℕⱼ ⊢Γ))) x₁)
                 (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
stabilityRedTerm Γ≡Δ (Id-subst X x x₁) = Id-subst (stabilityRedTerm Γ≡Δ X) (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
stabilityRedTerm Γ≡Δ (Id-ℕ-subst X x) = Id-ℕ-subst (stabilityRedTerm Γ≡Δ X) (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (Id-ℕ-0-subst X) = Id-ℕ-0-subst (stabilityRedTerm Γ≡Δ X)
stabilityRedTerm Γ≡Δ (Id-ℕ-S-subst x X) = Id-ℕ-S-subst (stabilityTerm Γ≡Δ x) (stabilityRedTerm Γ≡Δ X)
stabilityRedTerm Γ≡Δ (Id-U-subst X x) = Id-U-subst (stabilityRedTerm Γ≡Δ X) (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (Id-U-ℕ-subst X) = Id-U-ℕ-subst (stabilityRedTerm Γ≡Δ X)
stabilityRedTerm Γ≡Δ (Id-U-Π-subst x x₁ X) = Id-U-Π-subst (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁) (stabilityRedTerm Γ≡Δ X)
stabilityRedTerm Γ≡Δ (Id-Π l< l<' x x₁ x₂ x₃) = Id-Π l< l<' (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
stabilityRedTerm Γ≡Δ (Id-ℕ-00 x) = let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ in Id-ℕ-00 ⊢Δ
stabilityRedTerm Γ≡Δ (Id-ℕ-SS x x₁) = Id-ℕ-SS (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
stabilityRedTerm Γ≡Δ (Id-U-ΠΠ x x₁ x₂ x₃) = Id-U-ΠΠ (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm (Γ≡Δ ∙ refl (univ x₂)) x₃)
stabilityRedTerm Γ≡Δ (Id-U-ℕℕ x) = let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ in Id-U-ℕℕ ⊢Δ
stabilityRedTerm Γ≡Δ (Id-SProp x x₁) = Id-SProp (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
stabilityRedTerm Γ≡Δ (Id-ℕ-0S x) = Id-ℕ-0S (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (Id-ℕ-S0 x) = Id-ℕ-S0 (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (Id-U-ℕΠ x x₁) = Id-U-ℕΠ (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁)
stabilityRedTerm Γ≡Δ (Id-U-Πℕ x x₁) = Id-U-Πℕ (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁)
stabilityRedTerm Γ≡Δ (Id-U-ΠΠ!% x x₁ x₂ x₃ x₄) =
  Id-U-ΠΠ!% x (stabilityTerm Γ≡Δ x₁) (stabilityTerm (Γ≡Δ ∙ refl (univ x₁)) x₂) (stabilityTerm Γ≡Δ x₃) (stabilityTerm (Γ≡Δ ∙ refl (univ x₃)) x₄)
stabilityRedTerm Γ≡Δ (cast-subst X x x₁ x₂) = cast-subst (stabilityRedTerm Γ≡Δ X) (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁) (stabilityTerm Γ≡Δ x₂)
stabilityRedTerm Γ≡Δ (cast-ℕ-subst X x x₁) =
  cast-ℕ-subst (stabilityRedTerm Γ≡Δ X) (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
stabilityRedTerm Γ≡Δ (cast-Π-subst x x₁ X x₂ x₃) =
  cast-Π-subst (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁) (stabilityRedTerm Γ≡Δ X) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
stabilityRedTerm Γ≡Δ (cast-Π x x₁ x₂ x₃ x₄ x₅) =
  cast-Π (stabilityTerm Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl (univ x)) x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm (Γ≡Δ ∙ refl (univ x₂)) x₃) (stabilityTerm Γ≡Δ x₄) (stabilityTerm Γ≡Δ x₅)
stabilityRedTerm Γ≡Δ (cast-ℕ-0 x) = cast-ℕ-0 (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (cast-ℕ-S x x₁) = cast-ℕ-S (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
stabilityRedTerm Γ≡Δ (cast-ℕ-cong x X) = cast-ℕ-cong (stabilityTerm Γ≡Δ x) (stabilityRedTerm Γ≡Δ X)

-- Stability of type reductions.
stabilityRed : ∀ {A B r Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ⇒ B ^ r → Δ ⊢ A ⇒ B ^ r
stabilityRed Γ≡Δ (univ x) = univ (stabilityRedTerm Γ≡Δ x)

-- Stability of type reduction closures.
stabilityRed* : ∀ {A B r Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ⇒* B ^ r → Δ ⊢ A ⇒* B ^ r
stabilityRed* Γ≡Δ (id x) = id (stability Γ≡Δ x)
stabilityRed* Γ≡Δ (x ⇨ D) = stabilityRed Γ≡Δ x ⇨ stabilityRed* Γ≡Δ D

-- Stability of term reduction closures.
stabilityRed*Term : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ → Γ ⊢ t ⇒* u ∷ A ^ l → Δ ⊢ t ⇒* u ∷ A ^ l
stabilityRed*Term Γ≡Δ (id x) = id (stabilityTerm Γ≡Δ x)
stabilityRed*Term Γ≡Δ (x ⇨ d) = stabilityRedTerm Γ≡Δ x ⇨ stabilityRed*Term Γ≡Δ d

mutual
  -- Stability of algorithmic equality of neutrals.
  stability~↑! : ∀ {k l A Γ Δ lA}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ k ~ l ↑! A ^ lA
              → Δ ⊢ k ~ l ↑! A ^ lA
  stability~↑! Γ≡Δ (var-refl x x≡y) =
    var-refl (stabilityTerm Γ≡Δ x) x≡y
  stability~↑! Γ≡Δ (app-cong {rF = ! } k~l x) =
    app-cong (stability~↓! Γ≡Δ k~l) (stabilityConv↑Term Γ≡Δ x)
  stability~↑! Γ≡Δ (app-cong {rF = %} k~l x) =
    app-cong (stability~↓! Γ≡Δ k~l) (stability~↑% Γ≡Δ x)
  stability~↑! Γ≡Δ (natrec-cong x₁ x₂ x₃ k~l) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in natrec-cong (stabilityConv↑ (Γ≡Δ ∙ (refl (univ (ℕⱼ ⊢Γ)))) x₁)
                   (stabilityConv↑Term Γ≡Δ x₂)
                   (stabilityConv↑Term Γ≡Δ x₃)
                   (stability~↓! Γ≡Δ k~l)
  stability~↑! Γ≡Δ (Emptyrec-cong x₁ k~l) =
    Emptyrec-cong (stabilityConv↑ Γ≡Δ x₁)
                (stability~↑% Γ≡Δ k~l)
  stability~↑! Γ≡Δ (Id-cong X x x₁) = Id-cong (stability~↓! Γ≡Δ X) (stabilityConv↑Term Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁)
  stability~↑! Γ≡Δ (Id-ℕ X x) = Id-ℕ (stability~↓! Γ≡Δ X) (stabilityConv↑Term Γ≡Δ x)
  stability~↑! Γ≡Δ (Id-ℕ0 X) = Id-ℕ0 (stability~↓! Γ≡Δ X)
  stability~↑! Γ≡Δ (Id-ℕS x X) = Id-ℕS (stabilityConv↑Term Γ≡Δ x) (stability~↓! Γ≡Δ X)
  stability~↑! Γ≡Δ (Id-U X x) = Id-U (stability~↓! Γ≡Δ X) (stabilityConv↑Term Γ≡Δ x)
  stability~↑! Γ≡Δ (Id-Uℕ X) = Id-Uℕ (stability~↓! Γ≡Δ X)
  stability~↑! Γ≡Δ (Id-UΠ x X) = Id-UΠ (stabilityConv↑Term Γ≡Δ x) (stability~↓! Γ≡Δ X)
  stability~↑! Γ≡Δ (cast-cong X x x₁ x₂ x₃) = cast-cong (stability~↓! Γ≡Δ X) (stabilityConv↑Term Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
  stability~↑! Γ≡Δ (cast-ℕ X x x₁ x₂) = cast-ℕ (stability~↓! Γ≡Δ X) (stabilityConv↑Term Γ≡Δ x) (stabilityTerm Γ≡Δ x₁) (stabilityTerm Γ≡Δ x₂)
  stability~↑! Γ≡Δ (cast-ℕℕ X x x₁) = cast-ℕℕ (stability~↓! Γ≡Δ X) (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
  stability~↑! Γ≡Δ (cast-Π x X x₁ x₂ x₃) = cast-Π (stabilityConv↑Term Γ≡Δ x) (stability~↓! Γ≡Δ X) (stabilityConv↑Term Γ≡Δ x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
  stability~↑! Γ≡Δ (cast-Πℕ x x₁ x₂ x₃) = cast-Πℕ (stabilityConv↑Term Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
  stability~↑! Γ≡Δ (cast-ℕΠ x x₁ x₂ x₃) = cast-ℕΠ (stabilityConv↑Term Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
  stability~↑! Γ≡Δ (cast-ΠΠ%! x x₁ x₂ x₃ x₄) = cast-ΠΠ%! (stabilityConv↑Term Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityConv↑Term Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃) (stabilityTerm Γ≡Δ x₄)
  stability~↑! Γ≡Δ (cast-ΠΠ!% x x₁ x₂ x₃ x₄) = cast-ΠΠ!% (stabilityConv↑Term Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityConv↑Term Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃) (stabilityTerm Γ≡Δ x₄)

  stability~↑% : ∀ {k l A Γ Δ lA}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ k ~ l ↑% A ^ lA
              → Δ ⊢ k ~ l ↑% A ^ lA
  stability~↑% Γ≡Δ (%~↑ ⊢k ⊢l) = %~↑ (stabilityTerm Γ≡Δ ⊢k) (stabilityTerm Γ≡Δ ⊢l)

  stability~↑ : ∀ {k l A rA lA Γ Δ}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ k ~ l ↑ A ^ [ rA , lA ]
              → Δ ⊢ k ~ l ↑ A ^ [ rA , lA ]
  stability~↑ Γ≡Δ (~↑! x) = ~↑! (stability~↑! Γ≡Δ x)
  stability~↑ Γ≡Δ (~↑% x) = ~↑% (stability~↑% Γ≡Δ x)

  -- Stability of algorithmic equality of neutrals of types in WHNF.
  stability~↓! : ∀ {k l A lA Γ Δ}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ k ~ l ↓! A ^ lA
              → Δ ⊢ k ~ l ↓! A ^ lA
  stability~↓! Γ≡Δ ([~] A D whnfA k~l) =
    [~] A (stabilityRed* Γ≡Δ D) whnfA (stability~↑! Γ≡Δ k~l)

  -- Stability of algorithmic equality of types.
  stabilityConv↑ : ∀ {A B r Γ Δ}
                 → ⊢ Γ ≡ Δ
                 → Γ ⊢ A [conv↑] B ^ r
                 → Δ ⊢ A [conv↑] B ^ r
  stabilityConv↑ Γ≡Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    [↑] A′ B′ (stabilityRed* Γ≡Δ D) (stabilityRed* Γ≡Δ D′) whnfA′ whnfB′
        (stabilityConv↓ Γ≡Δ A′<>B′)

  -- Stability of algorithmic equality of types in WHNF.
  stabilityConv↓ : ∀ {A B r Γ Δ}
                 → ⊢ Γ ≡ Δ
                 → Γ ⊢ A [conv↓] B ^ r
                 → Δ ⊢ A [conv↓] B ^ r
  stabilityConv↓ Γ≡Δ (U-refl PE.refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  U-refl PE.refl ⊢Δ
  stabilityConv↓ Γ≡Δ (univ x) = univ (stabilityConv↓Term Γ≡Δ x)

  -- Stability of algorithmic equality of terms.
  stabilityConv↑Term : ∀ {t u A lA Γ Δ}
                     → ⊢ Γ ≡ Δ
                     → Γ ⊢ t [conv↑] u ∷ A ^ lA
                     → Δ ⊢ t [conv↑] u ∷ A ^ lA
  stabilityConv↑Term Γ≡Δ ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    [↑]ₜ B t′ u′ (stabilityRed* Γ≡Δ D) (stabilityRed*Term Γ≡Δ d)
                 (stabilityRed*Term Γ≡Δ d′) whnfB whnft′ whnfu′
                 (stabilityConv↓Term Γ≡Δ t<>u)

  -- Stability of algorithmic equality of terms in WHNF.
  stabilityConv↓Term : ∀ {t u A lA Γ Δ}
                     → ⊢ Γ ≡ Δ
                     → Γ ⊢ t [conv↓] u ∷ A ^ lA
                     → Δ ⊢ t [conv↓] u ∷ A ^ lA
  stabilityConv↓Term Γ≡Δ (U-refl PE.refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  U-refl PE.refl ⊢Δ
  stabilityConv↓Term Γ≡Δ (ne x) = ne (stability~↓! Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (ℕ-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  ℕ-refl ⊢Δ
  stabilityConv↓Term Γ≡Δ (Empty-refl x _) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  Empty-refl x ⊢Δ
  stabilityConv↓Term Γ≡Δ (Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' F A<>B A<>B₁) =
    Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' (stability Γ≡Δ F) (stabilityConv↑Term Γ≡Δ A<>B)
           (stabilityConv↑Term (Γ≡Δ ∙ refl F) A<>B₁)
  stabilityConv↓Term Γ≡Δ (∃-cong PE.refl F A<>B A<>B₁) =
    ∃-cong PE.refl (stability Γ≡Δ F) (stabilityConv↑Term Γ≡Δ A<>B)
           (stabilityConv↑Term (Γ≡Δ ∙ refl F) A<>B₁)
  stabilityConv↓Term Γ≡Δ (ℕ-ins x) =
    ℕ-ins (stability~↓! Γ≡Δ x)
  -- stabilityConv↓Term Γ≡Δ (Empty-ins x) =
  --   Empty-ins (stability~↓% Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (ne-ins t u neN x) =
    ne-ins (stabilityTerm Γ≡Δ t) (stabilityTerm Γ≡Δ u) neN (stability~↓! Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (zero-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  zero-refl ⊢Δ
  stabilityConv↓Term Γ≡Δ (suc-cong t<>u) = suc-cong (stabilityConv↑Term Γ≡Δ t<>u)
  stabilityConv↓Term Γ≡Δ (η-eq l< l<' F x x₁ y y₁ t<>u) =
    η-eq l< l<' (stability Γ≡Δ F) (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
         y y₁ (stabilityConv↑Term (Γ≡Δ ∙ refl F) t<>u)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

open import HoTT

module experimental.GlobularTypes where

{- Globular types as a coinductive record -}
record Glob (i : ULevel) : Type (suc i) where
  coinductive
  constructor glob
  field
    Ob : Type i
    Hom : (a b : Ob) → Glob i
open Glob public

{- The terminal globular type -}
Unit-glob : Glob zero
Ob Unit-glob = Unit
Hom Unit-glob _ _ = Unit-glob

{- The tower of identity types -}
Id-glob : ∀ {i} (A : Type i) → Glob zero
Ob (Id-glob A) = A
Hom (Id-glob A) a b = Id-glob (a == b)

{- Bisimulation between globular types -}
record _~_ {i} (G H : Glob i) : Type (suc i) where
  coinductive
  constructor glob~
  field
    Ob= : Ob G == Ob H
    Hom= : {a : Ob G} {a' : Ob H} (p : a == a' [ (λ x → x) ↓ Ob= ])
           {b : Ob G} {b' : Ob H} (q : b == b' [ (λ x → x) ↓ Ob= ])
           → Hom G a b ~ Hom H a' b'
open _~_ public

=-to-~ : ∀ {i} {G H : Glob i} → G == H → G ~ H
Ob= (=-to-~ p) = ap Ob p
Hom= (=-to-~ p) q r =
  =-to-~ (↓-app→cst-out (↓-→-out (apd Hom p)
                                 (↓-ap-out _ Ob p q))
                        (↓-ap-out _ Ob p r))
-- The definition of [Hom= (=-to-~ p) q r] would/should just be
-- [=-to-~ (apd Hom p q r)] in infinite-dimensional type theory, but here we
-- need to add a lot of non-sense to make it type-check.

{-
We postulate that bisimilarity is equality, because this should be true.
-}
postulate
  bisim-is-equiv : ∀ {i} {G H : Glob i} → is-equiv (=-to-~ :> (G == H → G ~ H))

bisim-equiv : ∀ {i} {G H : Glob i} → (G == H) ≃ (G ~ H)
bisim-equiv = (=-to-~ , bisim-is-equiv)

bisim : ∀ {i} {G H : Glob i} → (G ~ H) → G == H
bisim e = <– bisim-equiv e

{-
The type of globular types is the terminal coalgebra of the appropriate thing.
This is proved in the following two lemmas.
-}

Glob-corec : ∀ {i} {A : Type (suc i)} (Ob* : A → Type i)
  (Hom* : (x : A) (a b : Ob* x) → A) → (A → Glob i)
Ob (Glob-corec Ob* Hom* x) = Ob* x
Hom (Glob-corec Ob* Hom* x) a b = Glob-corec Ob* Hom* (Hom* x a b)

eta : ∀ {i} {A : Type (suc i)} (Ob* : A → Type i)
  (Hom* : (x : A) (a b : Ob* x) → A)
  (f g : A → Glob i) (s : (x : A) → f x ~ g x) → f == g
eta Ob* Hom* f g s = funext (λ x → bisim (s x))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------
-- The delay monad defined as the greatest fixpoint of an indexed
-- container
------------------------------------------------------------------------

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

module Indexed-container.Delay-monad where

open import Equality.Propositional as E using (_≡_; refl)
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bijection E.equality-with-J as Bijection using (_↔_)
open import Function-universe E.equality-with-J as F hiding (_∘_)

open import Delay-monad
open import Delay-monad.Bisimilarity as B

open import Indexed-container
open import Indexed-container.Combinators as C hiding (_∘_)
open import Relation

-- A container for the delay monad.

DelayC : ∀ {ℓ} → Type ℓ → Container (↑ ℓ ⊤) (↑ ℓ ⊤)
DelayC A =
  (λ _ → Maybe A) ◁ λ { (just _) _ → ⊥; nothing _ → ↑ _ ⊤ }

-- An alternative definition.

DelayC′ : ∀ {ℓ} → Type ℓ → Container (↑ ℓ ⊤) (↑ ℓ ⊤)
DelayC′ A = C.id ⊕ C.const (λ _ → A)

-- The two containers' interpretations are pointwise logically
-- equivalent, and in the presence of extensionality they are
-- pointwise isomorphic.

⟦DelayC⟧↔⟦DelayC′⟧ :
  ∀ {k a x} {A : Type a} {X : Rel x (↑ a ⊤)} {i} →
  Extensionality? k a (a ⊔ x) →
  ⟦ DelayC A ⟧ X i ↝[ k ] ⟦ DelayC′ A ⟧ X i
⟦DelayC⟧↔⟦DelayC′⟧ {k} {a} {A = A} {X} {i} ext =
  ⟦ DelayC A ⟧ X i                                              ↔⟨⟩
  (∃ λ (s : Maybe A) → Container.Position (DelayC A) s ⊆ X)     ↝⟨ Σ-cong (inverse Bijection.↑↔ ⊎-cong F.id)
                                                                     [ (λ _ → implicit-∀-cong ext $
                                                                              Π-cong (lower-extensionality? k lzero a ext) lemma λ _ →
                                                                              F.id)
                                                                     , (λ _ → F.id)
                                                                     ] ⟩
  (∃ λ (s : ↑ _ ⊤ ⊎ A) → [ (λ _ → _ ≡_) , (λ _ _ → ⊥) ] s ⊆ X)  ↔⟨⟩
  ⟦ DelayC′ A ⟧ X i                                             □
  where
  lemma : ↑ a ⊤ ↔ lift {ℓ = a} tt ≡ lift tt
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to = λ _ → refl
        }
      ; right-inverse-of = λ { refl → refl }
      }
    ; left-inverse-of = λ _ → refl
    }

-- An unfolding lemma.

νDelayC↔ : ∀ {k a i} {A : Type a} →
           Extensionality? k a a →
           ν (DelayC A) i _ ↝[ k ] A ⊎ ν′ (DelayC A) i _
νDelayC↔ {i = i} {A} ext =
  ν (DelayC A) i _                           ↔⟨⟩

  ⟦ DelayC  A ⟧ (ν′ (DelayC A) i) _          ↝⟨ ⟦DelayC⟧↔⟦DelayC′⟧ ext ⟩

  ⟦ DelayC′ A ⟧ (ν′ (DelayC A) i) _          ↔⟨ ⟦⊕⟧↔ C.id (C.const (λ _ → A)) ⟩

  ⟦ C.id ⟧ (ν′ (DelayC A) i) _ ⊎
  ⟦ C.const (λ _ → A) ⟧ (ν′ (DelayC A) i) _  ↝⟨ ⟦id⟧↔ ext ⊎-cong ⟦const⟧↔ _ ext ⟩

  ν′ (DelayC A) i _ ⊎ A                      ↔⟨ ⊎-comm ⟩□

  A ⊎ ν′ (DelayC A) i _                      □

-- There is a (size-preserving) logical equivalence between the direct
-- definition of the delay monad and an indirect definition using the
-- container DelayC and ν.

mutual

  Delay⇔νDelayC : ∀ {a i} {A : Type a} → Delay A i ⇔ ν (DelayC A) i _
  Delay⇔νDelayC {i = i} {A} =
    Delay A i              ↔⟨ Delay↔ ⟩
    A ⊎ Delay′ A i         ↝⟨ F.id ⊎-cong Delay′⇔ν′DelayC ⟩
    A ⊎ ν′ (DelayC A) i _  ↝⟨ inverse $ νDelayC↔ _ ⟩□
    ν (DelayC A) i _       □

  Delay′⇔ν′DelayC :
    ∀ {a i} {A : Type a} → Delay′ A i ⇔ ν′ (DelayC A) i _
  Delay′⇔ν′DelayC = record
    { to   = λ x → λ { .force → _⇔_.to   Delay⇔νDelayC (force x) }
    ; from = λ x → λ { .force → _⇔_.from Delay⇔νDelayC (force x) }
    }

-- The two components of Delay⇔νDelayC {i = ∞} are inverses up to
-- (strong) bisimilarity.

Delay⇔νDelayC-inverses :
  ∀ {a} {A : Type a} →
  let to   = _⇔_.to   (Delay⇔νDelayC {i = ∞})
      from = _⇔_.from (Delay⇔νDelayC {i = ∞})
  in
  (∀ x → ν-bisimilar ∞ (to (from x) , x))
    ×
  (∀ x → [ ∞ ] from (to x) ∼ x)
Delay⇔νDelayC-inverses {A = A} = to∘from , from∘to
  where
  to : ∀ {i} → Delay A i → ν (DelayC A) i _
  to = _⇔_.to Delay⇔νDelayC

  from : ∀ {i} → ν (DelayC A) i _ → Delay A i
  from = _⇔_.from Delay⇔νDelayC

  abstract

    from∘to : ∀ {i} x → [ i ] from (to x) ∼ x
    from∘to (now x)   = now x ∎
    from∘to (later x) = later λ { .force →
      from (to (force x))  ∼⟨ from∘to (force x) ⟩∼
      force x              ∎ }

    to∘from : ∀ {i} x → ν-bisimilar i (to (from x) , x)
    to∘from x@(just _ , _) =
      _⇔_.from (ν-bisimilar↔ _ (to (from x)) x)
        ( refl
        , λ ()
        )
    to∘from x@(nothing , f) =
      _⇔_.from (ν-bisimilar↔ _ (to (from x)) x)
        ( refl
        , λ p → λ { .force → to∘from (force (f p)) }
        )

-- There is an isomorphism between the direct definition of the delay
-- monad and an indirect definition using the container DelayC and ν
-- (assuming three kinds of extensionality).

Delay↔νDelayC :
  ∀ {a} {A : Type a} →
  E.Extensionality a a →
  B.Extensionality a →
  ν′-extensionality (DelayC A) →
  Delay A ∞ ↔ ν (DelayC A) ∞ _
Delay↔νDelayC ext ∼-ext ν′-ext = record
  { surjection = record
    { logical-equivalence = Delay⇔νDelayC
    ; right-inverse-of    = ν-extensionality ext ν′-ext ∘
                            proj₁ Delay⇔νDelayC-inverses
    }
  ; left-inverse-of = ∼-ext ∘ proj₂ Delay⇔νDelayC-inverses
  }

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

module Light.Library.Relation.Binary where

open import Light.Level using (Setω ; Level)
open import Light.Variable.Levels
open import Light.Variable.Sets
open import Light.Library.Relation using (Base ; Index ; Proposition ; True ; _⇢_)

module _ ⦃ base : Base ⦄ where
      record Binary (𝕒 : Set aℓ) (𝕓 : Set bℓ) : Setω where
            field if : 𝕒 → 𝕓 → Index
            field are : ∀ a b → Proposition (if a b)

      SelfBinary : Set aℓ → Setω
      SelfBinary 𝕒 = Binary 𝕒 𝕒

      open Binary using (are)

      private variable a : 𝕒
      private variable b : 𝕓
      private variable c : 𝕔

      record Transitive
            (a‐b‐valid : Binary 𝕒 𝕓)
            (b‐c‐valid : Binary 𝕓 𝕔)
            (a‐c‐valid : Binary 𝕒 𝕔)
            : Setω where

            field transitivity : True (are a‐b‐valid a b ⇢ (are b‐c‐valid b c ⇢ are a‐c‐valid a c))

      record Symmetric
            (a‐b‐valid : Binary 𝕒 𝕓)
            (b‐a‐valid : Binary 𝕓 𝕒)
            : Setω where

            field symmetry : True (are a‐b‐valid a b ⇢ are b‐a‐valid b a)

      record Reflexive (valid : SelfBinary 𝕒) : Setω where
            field reflexivity : True (are valid a a)

      SelfTransitive : ∀ (valid : SelfBinary 𝕒) → Setω
      SelfTransitive valid = Transitive valid valid valid

      SelfSymmetric : ∀ (valid : SelfBinary 𝕒) → Setω
      SelfSymmetric valid = Symmetric valid valid

      record Preserved
            (f : 𝕒 → 𝕓) (g : 𝕔 → 𝕕)
            (a‐c‐valid : Binary 𝕒 𝕔)
            (b‐d‐valid : Binary 𝕓 𝕕)
            : Setω where

            field preservation : True (are a‐c‐valid a c ⇢ are b‐d‐valid (f a) (g c))
            congruence = preservation

      CongruentFor :
            (𝕒 → 𝕓)
            → SelfBinary 𝕒
            → SelfBinary 𝕓
            → Setω
      CongruentFor f = Preserved f f

      SelfCongruentFor :
            (𝕒 → 𝕒)
            → SelfBinary 𝕒
            → Setω
      SelfCongruentFor f 𝕒 = CongruentFor f 𝕒 𝕒

      record Bijective
            (f : 𝕒 → 𝕓) (g : 𝕔 → 𝕕)
            (b‐d‐valid : Binary 𝕓 𝕕)
            (a‐c‐valid : Binary 𝕒 𝕔)
            : Setω where

            field bijectivity : True (are b‐d‐valid (f a) (g c) ⇢ are a‐c‐valid a c)
            injectivity = bijectivity

      Injective :
            (𝕒 → 𝕓)
            → SelfBinary 𝕓
            → SelfBinary 𝕒
            → Setω
      Injective f = Bijective f f

      SelfInjective :
            (𝕒 → 𝕒)
            → SelfBinary 𝕒
            → Setω
      SelfInjective f 𝕒 = Injective f 𝕒 𝕒

open Transitive ⦃ ... ⦄ public
open Symmetric ⦃ ... ⦄ public
open Reflexive ⦃ ... ⦄ public
open Preserved ⦃ ... ⦄ public
open Bijective ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
import Agda.Builtin.Size

postulate
  F : (A : Set) (B : A → Set) → ((x : A) → B x) → Set

variable
  A : Set
  P : A → Set

postulate
  f : (r : (x : _) → P x) → F _ P (λ x → r x)


text:
-- {-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v tc.lhs:20 #-}

open import Common.Size

record Stream (i : Size) (A : Set) : Set where
  coinductive
  constructor _::_
  field
    head  : A
    tail  : ∀ {j : Size< i} → Stream j A
open Stream public

-- size forgetful cons
cons : ∀ i {A} → A → Stream i A → Stream (↑ i) A
cons i a as = a :: as

-- Should work


text:
-- Properties of insertion sort

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

open import Relation.Binary as B

module Algorithms.List.Sort.Insertion.Properties
  {c ℓ₁ ℓ₂} (DTO : DecTotalOrder c ℓ₁ ℓ₂)
  where

-- agda-stdlib
open import Level

open import Data.Bool hiding (_≤_; _≤?_; _<_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List
import      Data.List.Properties as Listₚ
import      Data.Nat as ℕ
import      Data.Nat.Properties as ℕₚ
open import Data.Product hiding (swap)
open import Data.Sum using (_⊎_; inj₁; inj₂)

import      Data.List.Relation.Binary.Equality.Setoid as ListSetoidEquality
import      Data.List.Relation.Binary.Permutation.Setoid as PermutationSetoid
import      Data.List.Relation.Binary.Permutation.Setoid.Properties
  as PermutationSetoidProperties
open import Data.List.Relation.Unary.All as All
import      Data.List.Relation.Unary.All.Properties as Allₚ
open import Data.List.Relation.Unary.Linked as Linked
open import      Data.List.Relation.Unary.Linked.Properties as Linkedₚ
open import Data.List.Relation.Unary.AllPairs as AllPairs
import      Data.List.Relation.Unary.AllPairs.Properties as AllPairsₚ

open import Function.Base using (_∘_; _$_; flip)

import      Relation.Binary.Properties.DecTotalOrder as DecTotalOrderProperties
open import Relation.Binary.PropositionalEquality using (_≡_)
import      Relation.Binary.PropositionalEquality as ≡ hiding ([_])
import      Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Nullary
open import Relation.Unary as U

-- agda-misc
open import Algorithms.List.Sort.Common DTO
open import Algorithms.List.Sort.Insertion
open import Experiment.ListRelationProperties
  using (foldr-preservesʳ; Linked-∷⁻ʳ; Linked-resp-≋)

open DecTotalOrder DTO renaming (Carrier to A)
open DecTotalOrderProperties DTO
open PermutationSetoid Eq.setoid renaming (refl to PSrefl; trans to PStrans)
open PermutationSetoidProperties Eq.setoid
open ListSetoidEquality Eq.setoid
open InsertionSortOperation _≤?_

private
  _≰_ : Rel A _
  x ≰ y = ¬ (x ≤ y)

  -- stdlib
  <⇒≤ : ∀ {x y} → x < y → x ≤ y
  <⇒≤ = proj₁

  ≰⇒≥ : ∀ {x y} → x ≰ y → y ≤ x
  ≰⇒≥ = <⇒≤ ∘ ≰⇒>

  ≰∧≱⇒⊥ : ∀ {x y} → x ≰ y → y ≰ x → ⊥
  ≰∧≱⇒⊥ x≰y y≰x = x≰y (≰⇒≥ y≰x)

  ≰⇒≉ : ∀ {x y} → x ≰ y → ¬ (x ≈ y)
  ≰⇒≉ x≰y x≈y = x≰y (≤-respʳ-≈ x≈y refl)

  ≱⇒≉ : ∀ {x y} → y ≰ x → ¬ (x ≈ y)
  ≱⇒≉ x≱y x≈y = ≰⇒≉ x≱y (Eq.sym x≈y)

  -- stdlib
  _≈?_ : ∀ x y → Dec (x ≈ y)
  x ≈? y with x ≤? y | y ≤? x
  ... | yes x≤y | yes y≤x = yes (antisym x≤y y≤x)
  ... | yes x≤y | no  y≰x = no (≱⇒≉ y≰x)
  ... | no  x≰y | yes y≤x = no (≰⇒≉ x≰y)
  ... | no  x≰y | no  y≰x = ⊥-elim $ ≰∧≱⇒⊥ x≰y y≰x

  ≤⇒<∨≈ : ∀ {x y} → x ≤ y → x < y ⊎ x ≈ y
  ≤⇒<∨≈ {x} {y} x≤y with x ≈? y
  ... | yes x≈y = inj₂ x≈y
  ... | no  x≉y = inj₁ (≤∧≉⇒< x≤y x≉y)

insert-permutation : ∀ x xs → insert x xs ↭ x ∷ xs
insert-permutation x []       = ↭-refl
insert-permutation x (y ∷ ys) with x ≤? y
... | true  because _ = ↭-refl
... | false because _ = ↭-trans (prep Eq.refl (insert-permutation x ys))
                      (swap Eq.refl Eq.refl ↭-refl)

insert-pres-Sorted : ∀ x {xs} → Sorted xs → Sorted (insert x xs)
insert-pres-Sorted x {[]}     _ = [-]
insert-pres-Sorted x {y ∷ ys} xs-Sorted with x ≤? y
... | yes x≤y = x≤y ∷ xs-Sorted
... | no  x≰y = Linkedₚ.AllPairs⇒Linked (hd ∷ tl)
  where
  y≤x : y ≤ x
  y≤x = ≰⇒≥ x≰y
  lem : All (y ≤_) ys
  lem = AllPairs.head (toAllPairs xs-Sorted)
  hd : All (y ≤_) (insert x ys)
  hd = All-resp-↭ ≤-respʳ-≈ (↭-sym (insert-permutation x ys)) (y≤x ∷ lem)
  insert[x,ys]-Sorted : Sorted (insert x ys)
  insert[x,ys]-Sorted = insert-pres-Sorted x {ys} (Linked-∷⁻ʳ xs-Sorted)
  tl : AllPairs _≤_ (insert x ys)
  tl = toAllPairs insert[x,ys]-Sorted

sort-Sorted : ∀ xs → Sorted (sort xs)
sort-Sorted xs = foldr-preservesʳ insert-pres-Sorted [] xs

sort-permutation : ∀ xs → sort xs ↭ xs
sort-permutation []       = ↭-refl
sort-permutation (x ∷ xs) = begin
  sort (x ∷ xs)      ≡⟨⟩
  insert x (sort xs) ≈⟨ insert-permutation x (sort xs) ⟩
  x ∷ sort xs        ≈⟨ prep Eq.refl (sort-permutation xs) ⟩
  x ∷ xs             ∎
  where open SetoidReasoning ↭-setoid

insert-cong-≋ : ∀ {x y xs ys} → x ≈ y → xs ≋ ys → insert x xs ≋ insert y ys
insert-cong-≋ {x} {y} {[]}      {[]}      x≈y xs≋ys = x≈y ∷ []
insert-cong-≋ {x} {y} {x₁ ∷ xs} {y₁ ∷ ys} x≈y (x₁≈y₁ ∷ xs≋ys) with x ≤? x₁ | y ≤? y₁
... | yes p | yes p₁ = x≈y ∷ x₁≈y₁ ∷ xs≋ys
... | yes p | no ¬p  = ⊥-elim (¬p (≤-respʳ-≈ x₁≈y₁ (≤-respˡ-≈ x≈y p)))
... | no ¬p | yes p  = ⊥-elim (¬p (≤-respʳ-≈ (Eq.sym x₁≈y₁) (≤-respˡ-≈ (Eq.sym x≈y) p)))
... | no ¬p | no ¬p₁ = x₁≈y₁ ∷ insert-cong-≋ x≈y xs≋ys

insert-stop : ∀ {x y} ys → x ≤ y → insert x (y ∷ ys) ≋ x ∷ y ∷ ys
insert-stop {x} {y} ys x≤y with x ≤? y
... | yes _   = ≋-refl
... | no  x≰y = ⊥-elim (x≰y x≤y)

insert-into : ∀ {x y} ys → x ≰ y → insert x (y ∷ ys) ≋ y ∷ insert x ys
insert-into {x} {y} ys x≰y with x ≤? y
... | yes x≤y = ⊥-elim (x≰y x≤y)
... | no  _   = ≋-refl

Sorted-insert : ∀ {x xs} → Sorted (x ∷ xs) → insert x xs ≋ x ∷ xs
Sorted-insert {x} {[]}     _         = ≋-refl
Sorted-insert {x} {y ∷ ys} (x≤y ∷ _) = insert-stop ys x≤y

sort-Sorted-id : ∀ xs → Sorted xs → sort xs ≋ xs
sort-Sorted-id []       xs-Sorted   = ≋-refl
sort-Sorted-id (x ∷ xs) x∷xs-Sorted = begin
  sort (x ∷ xs)
    ≡⟨⟩
  insert x (sort xs)
    ≈⟨ insert-cong-≋ Eq.refl
                     (sort-Sorted-id xs (Linked-∷⁻ʳ x∷xs-Sorted)) ⟩
  insert x xs
    ≈⟨ Sorted-insert x∷xs-Sorted ⟩
  x ∷ xs
    ∎
  where open SetoidReasoning ≋-setoid

sort-idem : ∀ xs → sort (sort xs) ≋ sort xs
sort-idem xs = sort-Sorted-id (sort xs) (sort-Sorted xs)

module _ where
  open SetoidReasoning ≋-setoid

  insert-swap : ∀ x y xs → insert x (insert y xs) ≋ insert y (insert x xs)
  insert-swap x y [] with x ≤? y | y ≤? x
  ... | yes x≤y | yes y≤x = x≈y ∷ Eq.sym x≈y ∷ []
    where x≈y = antisym x≤y y≤x
  ... | yes _   | no  _   = ≋-refl
  ... | no  _   | yes _   = ≋-refl
  ... | no  x≰y | no  y≰x = ⊥-elim $ ≰∧≱⇒⊥ x≰y y≰x
  insert-swap x y (z ∷ zs) with y ≤? z | x ≤? z
  insert-swap x y (z ∷ zs) | yes _   | yes _ with x ≤? y | y ≤? x
  insert-swap x y (z ∷ zs) | yes y≤z | yes x≤z | yes x≤y | yes y≤x =
    x≈y ∷ Eq.sym x≈y ∷ ≋-refl
    where x≈y = antisym x≤y y≤x
  insert-swap x y (z ∷ zs) | yes y≤z | yes _   | yes _  | no _ = begin
    x ∷ y ∷ z ∷ zs        ≈˘⟨ Eq.refl ∷ insert-stop zs y≤z ⟩
    x ∷ insert y (z ∷ zs) ∎
  insert-swap x y (z ∷ zs) | yes _   | yes x≤z | no _   | yes _ = begin
    y ∷ insert x (z ∷ zs) ≈⟨ Eq.refl ∷ insert-stop zs x≤z ⟩
    y ∷ x ∷ z ∷ zs        ∎
  insert-swap x y (z ∷ zs) | yes y≤z | yes x≤z | no x≰y | no y≰x =
    ⊥-elim $ ≰∧≱⇒⊥ x≰y y≰x
  insert-swap x y (z ∷ zs) | yes _   | no  _ with x ≤? y
  insert-swap x y (z ∷ zs) | yes y≤z | no  x≰z | yes x≤y =
    ⊥-elim $ x≰z (trans x≤y y≤z)
  insert-swap x y (z ∷ zs) | yes y≤z | no  x≰z | no  x≰y = begin
    y ∷ insert x (z ∷ zs)      ≈⟨ Eq.refl ∷ insert-into zs x≰z ⟩
    y ∷ z ∷ insert x zs        ≈˘⟨ insert-stop (insert x zs) y≤z ⟩
    insert y (z ∷ insert x zs) ∎
  insert-swap x y (z ∷ zs) | no _   | yes _ with y ≤? x
  insert-swap x y (z ∷ zs) | no y≰z | yes x≤z | yes y≤x =
    ⊥-elim (y≰z (trans y≤x x≤z))
  insert-swap x y (z ∷ zs) | no y≰z | yes x≤z | no  _   = begin
    insert x (z ∷ insert y zs) ≈⟨ insert-stop (insert y zs) x≤z ⟩
    x ∷ z ∷ insert y zs        ≈˘⟨ Eq.refl ∷ insert-into zs y≰z ⟩
    x ∷ insert y (z ∷ zs)      ∎
  insert-swap x y (z ∷ zs) | no y≰z | no  x≰z = begin
    insert x (z ∷ insert y zs) ≈⟨ insert-into (insert y zs) x≰z ⟩
    z ∷ insert x (insert y zs) ≈⟨ Eq.refl ∷ insert-swap x y zs ⟩
    z ∷ insert y (insert x zs) ≈˘⟨ insert-into (insert x zs) y≰z ⟩
    insert y (z ∷ insert x zs) ∎

sort-cong-↭-≋ : ∀ {xs ys} → xs ↭ ys → sort xs ≋ sort ys
sort-cong-↭-≋ {xs}         {.xs}          PSrefl               = ≋-refl
sort-cong-↭-≋ {_ ∷ _}      {_ ∷ _}        (prep eq xs↭ys)      =
  insert-cong-≋ eq (sort-cong-↭-≋ xs↭ys)
sort-cong-↭-≋ {x ∷ y ∷ xs} {y′ ∷ x′ ∷ ys} (swap eq₁ eq₂ xs↭ys) = begin
  insert x  (insert y  (sort xs)) ≈⟨ insert-cong-≋ eq₁
                                    (insert-cong-≋ eq₂ (sort-cong-↭-≋ xs↭ys)) ⟩
  insert x′ (insert y′ (sort ys)) ≈⟨ insert-swap x′ y′ (sort ys) ⟩
  insert y′ (insert x′ (sort ys)) ∎
  where open SetoidReasoning ≋-setoid
sort-cong-↭-≋ {xs} {ys} (PStrans {ys = zs} xs↭zs zs↭ys) = begin
  sort xs ≈⟨ sort-cong-↭-≋ xs↭zs ⟩
  sort zs ≈⟨ sort-cong-↭-≋ zs↭ys ⟩
  sort ys ∎
  where open SetoidReasoning ≋-setoid

Sorted-unique : ∀ {xs ys} → xs ↭ ys → Sorted xs → Sorted ys → xs ≋ ys
Sorted-unique {xs} {ys} xs↭ys ixs iys = begin
  xs      ≈⟨ ≋-sym $ sort-Sorted-id xs ixs ⟩
  sort xs ≈⟨ sort-cong-↭-≋ xs↭ys ⟩
  sort ys ≈⟨ sort-Sorted-id ys iys ⟩
  ys      ∎
  where open SetoidReasoning ≋-setoid


text:
------------------------------------------------------------------------------
-- Stream properties
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Stream.PropertiesI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Colist.Type
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.Stream.PropertiesI
open import FOTC.Data.Stream.Type

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

{-# TERMINATING #-}
++-Stream : ∀ {xs ys} → Colist xs → Stream ys → Stream (xs ++ ys)
++-Stream {xs} {ys} CLxs Sys with Colist-out CLxs
... | inj₁ prf = subst Stream (sym prf₁) Sys
 where
 prf₁ : xs ++ ys ≡ ys
 prf₁ = trans (++-leftCong prf) (++-[] ys)

... | inj₂ (x' , xs' , prf , CLxs') = subst Stream (sym prf₁) prf₂
   where
   prf₁ : xs ++ ys ≡ x' ∷ (xs' ++ ys)
   prf₁ = trans (++-leftCong prf) (++-∷ x' xs' ys)

   prf₂ : Stream (x' ∷ xs' ++ ys)
   prf₂ = Stream-in (x' , (xs' ++ ys) , refl , ++-Stream CLxs' Sys)

-- ++-Stream with a diferent type.
{-# TERMINATING #-}
++-Stream' : ∀ {xs ys} → Stream xs → Stream ys → Stream (xs ++ ys)
++-Stream' {xs} {ys} Sxs Sys with Stream-out Sxs
... | x' , xs' , prf , Sxs' = subst Stream prf₁ prf₂
  where
  prf₁ : x' ∷ (xs' ++ ys) ≡ xs ++ ys
  prf₁ = trans (sym (++-∷ x' xs' ys)) (++-leftCong (sym prf))

  prf₂ : Stream (x' ∷ xs' ++ ys)
  prf₂ = Stream-in (x' , xs' ++ ys , refl , ++-Stream' Sxs' Sys)


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

open import NTypes.Contractible
open import PathOperations
open import PathStructure.Sigma
open import Types

-- Not strictly related to the lectures.
--
-- Here we show that the various forms of extending
-- pure ITT to propositionally extensional TT are
-- (logically) equivalent.

-- The most general form of axiom K.
K-gen : ∀ a p → Set _
K-gen a p = {A : Set a} (x : A) (P : x ≡ x → Set p) (h : x ≡ x) →
  P refl → P h

-- Specialized form of axiom K.
K : ∀ a → Set _
K a = {A : Set a} (x : A) (p : x ≡ x) → p ≡ refl

uip : ∀ a → Set _
uip a = {A : Set a} (x y : A) (p q : x ≡ y) → p ≡ q

π₂-Id : ∀ a b → Set _
π₂-Id a b = {A : Set a} {B : A → Set b} (a : A) (b₁ b₂ : B a) →
  Id (Σ A B) (a , b₁) (a , b₂) → b₁ ≡ b₂

-- Relation between K and its specialized version.
K-gen→K : ∀ {a} → K-gen a a → K a
K-gen→K K x p = K x (λ p → p ≡ refl) p refl

K→K-gen : ∀ {a p} → K a → K-gen a p
K→K-gen K x P h p = tr P (K x h ⁻¹) p

-- Relation between K and UIP.
K→uip : ∀ {a} → K a → uip a
K→uip K x y p q = J (λ _ _ p → ∀ q → q ≡ p) K _ _ q p

uip→K : ∀ {a} → uip a → K a
uip→K uip x p = uip x x p refl

-- Relation between K and π₂-Id.
K→π₂-Id : ∀ {a b} → K a → π₂-Id a b
K→π₂-Id K {B = B} _ b₁ b₂ p = tr
  (λ z → tr B z b₁ ≡ b₂)
  (K _ (π₁ (split-path p)))
  (π₂ (split-path p))

π₂-Id→K : ∀ {a} → π₂-Id a a → K a
π₂-Id→K πId x p =
  πId x p refl (π₂ (pp-space-contr x) (x , p) ⁻¹)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module zf where

open import Level

open import logic

open import Relation.Nullary
open import Relation.Binary hiding (_⇔_)
open import Data.Empty

record IsZF {n m : Level }
     (ZFSet : Set n)
     (_∋_ : ( A x : ZFSet  ) → Set m)
     (_≈_ : Rel ZFSet m)
     (∅  : ZFSet)
     (_,_ : ( A B : ZFSet  ) → ZFSet)
     (Union : ( A : ZFSet  ) → ZFSet)
     (Power : ( A : ZFSet  ) → ZFSet)
     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
     (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
     (infinite : ZFSet)
       : Set (suc (n ⊔ suc m)) where
  field
     isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
     -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t  ≈ y)
     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y )
     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t
     -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
     union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
  _∈_ : ( A B : ZFSet  ) → Set m
  A ∈ B = B ∋ A
  _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
  _⊆_ A B {x} = A ∋ x →  B ∋ x
  _∩_ : ( A B : ZFSet  ) → ZFSet
  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
  _∪_ : ( A B : ZFSet  ) → ZFSet
  A ∪ B = Union (A , B)
  ｛_｝ : ZFSet → ZFSet
  ｛ x ｝ = ( x ,  x )
  infixr  200 _∈_
  infixr  230 _∩_ _∪_
  infixr  220 _⊆_
  field
     empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x}
     power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t
     -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
     extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
     -- regularity without minimum
     ε-induction : { ψ : ZFSet → Set (suc m)}
              → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
              → (x : ZFSet ) → ψ x
     -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
     infinity∅ :  ∅ ∈ infinite
     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite
     selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ )
     -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
     replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ
     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )

record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where
  infixr  210 _,_
  infixl  200 _∋_
  infixr  220 _≈_
  field
     ZFSet : Set n
     _∋_ : ( A x : ZFSet  ) → Set m
     _≈_ : ( A B : ZFSet  ) → Set m
  -- ZF Set constructor
     ∅  : ZFSet
     _,_ : ( A B : ZFSet  ) → ZFSet
     Union : ( A : ZFSet  ) → ZFSet
     Power : ( A : ZFSet  ) → ZFSet
     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
     Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
     infinite : ZFSet
     isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
-- An implementation of Olivier Danvy's Type-Directed Partial Evaluation (POPL 1996)
-- for STLC with sum types using continuations in form of shift and reset.
--
-- The algorithm was originally for a two-level lambda-calculus.

-- Our use of Kripke semantics makes the effect of fresh variable generation explicit and formal.

open import Library

module DanvyShiftResetLiftable where

data Base : Set where
  α β : Base

open import Formulas    Base
open import Derivations Base

-- Continutation monad with answer type R.
-- (Cf. Haskell's Control.Monad.Cont.Cont = (A → R) → R).

record M (R A : Cxt → Set) (Γ : Cxt) : Set where
  constructor shift
  field run : KFun (KFun A R) R Γ
open M

-- shift : ∀{R A Γ} (f : KFun (KFun A R) R Γ) → M R A Γ
-- shift f .run σ k = f σ k

reset : ∀{A} → M A A →̇ A
reset m = m .run id≤ λ τ → id

return : ∀{R A} → □ A →̇ M R A
return x .run τ k = k id≤ (x τ)

return' : ∀{R A} → □ A →̇ M R (□ A)
return' x .run τ k = k id≤ λ τ₁ → x (τ₁ • τ)

-- Bind

_>>=_ : ∀{R A B Γ} (m : M R A Γ) (f : KFun A (M R B) Γ) → M R B Γ
(m >>= f) .run σ k = m .run σ λ τ a → f (τ • σ) a .run id≤ λ τ′ → k (τ′ • τ)

-- Map

_<$>_ : ∀{R A B} (f : A →̇ B) → M R A →̇ M R B
(f <$> m) .run σ k = m .run σ λ τ → k τ ∘ f

_<&>_ : ∀{R A B Γ} (m : M R A Γ) (f : A →̇ B) → M R B Γ
(m <&> f) .run σ k = m .run σ λ τ → k τ ∘ f

-- Kripke map

K$ : ∀{R A B} → KFun A B →̇ KFun (M R A) (M R B)
K$ f τ m .run σ k = m .run σ λ τ′ a →  k τ′ (f (τ′ • (σ • τ)) a)

-- We use a continuation monad with answer type Nf.

M' : (X : Cxt → Set) (Γ : Cxt) → Set
M' X Γ = ∀ {C} → M (Nf' C) X Γ

T⟦_⟧ : (A : Form) (Γ : Cxt) → Set
T⟦ Atom P ⟧ = □ (Nf' (Atom P))
T⟦ True   ⟧ Γ = ⊤
T⟦ False  ⟧ Γ = ⊥
T⟦ A ∨ B  ⟧ Γ = T⟦ A ⟧ Γ ⊎ T⟦ B ⟧ Γ
T⟦ A ∧ B  ⟧ Γ = T⟦ A ⟧ Γ × T⟦ B ⟧ Γ
T⟦ A ⇒ B  ⟧ Γ = ∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → M' T⟦ B ⟧ Δ

-- Monotonicity of the model is proven by induction on the proposition.

-- monT : ∀ A {Γ Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ → T⟦ A ⟧ Δ

monT : ∀ A → Mon T⟦ A ⟧
monT (Atom P) = mon□
monT True     = _
monT False  τ ()
monT (A ∨ B) τ = map-⊎ (monT A τ) (monT B τ)
monT (A ∧ B) τ (a , b) = monT A τ a , monT B τ b
monT (A ⇒ B) τ f σ = f (σ • τ)

fresh : ∀{A Γ} → □ (Ne' A) (Γ ∙ A)
fresh τ′ = hyp (monH τ′ top)

-- Reflection / reification, proven simultaneously by induction on the proposition.

-- Reflection is η-expansion (and recursively reflection);

mutual

  reflect : ∀ A → □ (Ne' A) →̇ M' T⟦ A ⟧
  reflect (Atom P) t = return' (ne ∘′ t) -- λ τ → ne (monNe τ t)
  reflect True     t = return _
  reflect False    t = shift λ τ k → falseE (t τ)
  reflect (A ∨ B)  t = shift λ τ k → orE (t τ)
    (reset (K$ k (weak id≤) (inj₁ <$> reflect A fresh)))
    (reset (K$ k (weak id≤) (inj₂ <$> reflect B fresh)))

    -- ((inj₂ <$> reflect B (hyp top)) .run λ τ → k (τ • weak id≤))
    -- Wrong:
    --     (reset (k (weak id≤) <$> (inj₁ <$> reflect A (hyp top))))

  -- reflect (A ∧ B) t = do
  --   a ← reflect A (andE₁ t)
  --   b ← reflect B (andE₂ t)
  --   return (a , b)

  reflect (A ∧ B) t =
    reflect A (                andE₁ ∘ t ) >>= λ τ a →
    reflect B (mon□ {Ne' B} τ (andE₂ ∘ t)) >>= λ τ′ b →
    return λ τ₁ → monT A (τ₁ • τ′) a , monT B τ₁ b

  reflect (A ⇒ B)  t = return' λ τ a → reflect B λ τ′ → impE (t (τ′ • τ)) (reify A a τ′)

  reify : ∀ A → T⟦ A ⟧ →̇ □ (Nf' A)

  reify (Atom P) t = t
  reify True     _       τ = trueI
  reify False   ()
  reify (A ∨ B) (inj₁ a) τ = orI₁ (reify A a τ)
  reify (A ∨ B) (inj₂ b) τ = orI₂ (reify B b τ)
  reify (A ∧ B) (a , b) τ = andI (reify A a τ) (reify B b τ)

  reify (A ⇒ B) f       τ = impI $ reset $
    reflect A fresh >>= λ τ′ a →
    f (τ′ • weak τ) a <&> λ b →
    reify B b id≤

-- Fundamental theorem

-- Delayed lifting

record ◇ (G : Cxt → Set) (Γ : Cxt) : Set where
  constructor dia; field
    {Δ} : Cxt
    τ   : Γ ≤ Δ
    γ   : G Δ

mon◇ : ∀{P} → Mon (◇ P)
mon◇ τ′ (dia τ p) = dia (τ′ • τ) p

-- NB: ◇ is a monad

module Monad◇ where

  return◇ : ∀{P} → P →̇ ◇ P
  return◇ = dia id≤

  join◇ : ∀{P} → ◇ (◇ P) →̇ ◇ P
  join◇ (dia τ d) = mon◇ τ d
  -- join◇ (dia τ (dia τ′ a)) = dia (τ • τ′) a

  map◇ : ∀{P Q} → (P →̇ Q) → ◇ P →̇ ◇ Q
  map◇ f (dia τ p) = dia τ (f p)

-- Extension of T⟦_⟧ to contexts to classify semantic environments.

G⟦_⟧ : ∀ (Γ Δ : Cxt) → Set
G⟦ ε     ⟧ _ = ⊤
G⟦ Γ ∙ A ⟧ = ◇ λ Δ → G⟦ Γ ⟧ Δ × T⟦ A ⟧ Δ

-- monG is lazy except for matching on the context.

monG : ∀{Γ} → Mon G⟦ Γ ⟧
monG {ε} τ _ = _
monG {Γ ∙ A} τ γ = mon◇ τ γ

-- Environment extension.

ext : ∀ A {Γ Δ₁ Δ} →
      (τ : Δ ≤ Δ₁) (γ : G⟦ Γ ⟧ Δ₁) →
      (a : T⟦ A ⟧ Δ) →
      □ G⟦ Γ ∙ A ⟧ Δ
ext A τ γ a τ′ = dia τ′ (monG τ γ , a)

-- Lookup in the environment.
-- Accumulates embedded weakenings from environment.

fundH : ∀{A Γ} (x : Hyp A Γ) → G⟦ Γ ⟧  →̇ □ T⟦ A ⟧
fundH {A} top (dia τ′ (_ , a)) τ = monT A (τ • τ′) a
fundH (pop x) (dia τ′ (γ , _)) τ = fundH x γ (τ • τ′)

-- The fundamental theorem:
-- A call-by-value interpreter.

fund :  ∀{Γ A} (t : Γ ⊢ A) → G⟦ Γ ⟧  →̇ M' T⟦ A ⟧

fund (hyp {A} x) γ = return (fundH x γ)
fund (impI {A} t) γ = return' λ τ a → fund t (ext A τ γ a id≤)

fund (impE t u)  γ =
  fund t γ          >>= λ τ f →
  fund u (monG τ γ) >>= λ τ′ a →
  f τ′ a

fund (andI {A} {B} t u) γ =
  fund t γ          >>= λ τ a →
  fund u (monG τ γ) >>= λ τ′ b →
  return λ τ₁ → monT A (τ₁ • τ′) a , monT B τ₁ b

fund (andE₁ t)    γ = proj₁ <$> fund t γ
fund (andE₂ t)    γ = proj₂ <$> fund t γ
fund (orI₁ t)     γ = inj₁  <$> fund t γ
fund (orI₂ t)     γ = inj₂  <$> fund t γ

fund (orE {A} {B} t u v) γ = fund t γ >>= λ τ →
  [ (λ a → fund u (ext A τ γ a id≤))
  , (λ b → fund v (ext B τ γ b id≤))
  ]

fund (falseE t)  γ = fund t γ >>= λ τ ()
fund trueI       γ = return _

-- Identity environment

ide : ∀ Γ → □ (M' G⟦ Γ ⟧) Γ
ide ε       τ = return _
ide (Γ ∙ A) τ =
  ide Γ (τ • weak id≤)           >>= λ τ₁ γ →
  reflect A (mon□ (τ₁ • τ) fresh) >>= λ τ₂ a →
  return (ext A τ₂ γ a)
  -- return λ τ₃ → dia τ₃ (monG τ₂ γ , a)

-- Normalization

norm : ∀{A Γ} (t : Γ ⊢ A) → Nf Γ A
norm {A} {Γ} t = reset $
  ide Γ id≤ >>= λ _ γ →
  fund t γ <&> λ a →
  reify A a id≤

-- Testing

idD : (A : Form) → ε ⊢ (A ⇒ A)
idD A = impI (hyp top)

test : let A = Atom α; B = Atom β in Nf ε (A ∨ B ⇒ A ∨ B)
test = norm (idD (Atom α ∨ Atom β))

test2 = norm (idD (Atom α ∨ Atom β ∨ Atom α))

test3 = norm (idD False)

-- Q.E.D. -}
-- -}
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.StrictPartialOrder module directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.StrictPartialOrderReasoning
         {p₁ p₂ p₃} (S : StrictPartialOrder p₁ p₂ p₃) where

open import Relation.Binary.Reasoning.StrictPartialOrder S public


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

open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

postulate
  X   : Set₁
  rew : X ≡ Set

{-# REWRITE rew #-}
{-# REWRITE rew #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda