text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Extensional pointwise lifting of relations to vectors
------------------------------------------------------------------------

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

module Data.Vec.Relation.Binary.Pointwise.Extensional where

open import Data.Fin using (zero; suc)
open import Data.Nat using (zero; suc)
open import Data.Vec as Vec hiding ([_]; head; tail; map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive as Inductive
  using ([]; _∷_)
  renaming (Pointwise to IPointwise)
open import Level using (_⊔_)
open import Function using (_∘_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv
  using (_⇔_; ⇔-setoid; equivalence; module Equivalence)
open import Level using (_⊔_) renaming (zero to ℓ₀)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.Construct.Closure.Transitive as Plus
  hiding (equivalent; map)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

record Pointwise {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ)
                 {n} (xs : Vec A n) (ys : Vec B n) : Set (a ⊔ b ⊔ ℓ)
                 where
  constructor ext
  field app : ∀ i → lookup xs i ∼ lookup ys i

------------------------------------------------------------------------
-- Operations

head : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ}
       {n x y xs} {ys : Vec B n} →
       Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
head (ext app) = app zero

tail : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ}
       {n x y xs} {ys : Vec B n} →
       Pointwise _∼_ (x ∷ xs) (y ∷ ys) → Pointwise _∼_ xs ys
tail (ext app) = ext (app ∘ suc)

map : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ _∼′_ : REL A B ℓ} {n} →
      _∼_ ⇒ _∼′_ → Pointwise _∼_ ⇒ Pointwise _∼′_ {n}
map ∼⇒∼′ xs∼ys = ext (∼⇒∼′ ∘ Pointwise.app xs∼ys)

gmap : ∀ {a b ℓ} {A : Set a} {B : Set b}
       {_∼_ : Rel A ℓ} {_∼′_ : Rel B ℓ} {f : A → B} {n} →
       _∼_ =[ f ]⇒ _∼′_ →
       Pointwise _∼_ =[ Vec.map {n = n} f ]⇒ Pointwise _∼′_
gmap {_}          ∼⇒∼′ {[]}      {[]}      xs∼ys = ext λ()
gmap {_∼′_ = _∼′_} ∼⇒∼′ {x ∷ xs} {y ∷ ys} xs∼ys = ext λ
  { zero    → ∼⇒∼′ (head xs∼ys)
  ; (suc i) → Pointwise.app (gmap {_∼′_ = _∼′_} ∼⇒∼′ (tail xs∼ys)) i
  }

------------------------------------------------------------------------
-- The inductive and extensional definitions are equivalent.

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  extensional⇒inductive : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
                           Pointwise _∼_ xs ys → IPointwise _∼_ xs ys
  extensional⇒inductive {zero} {[]}       {[]}      xs∼ys = []
  extensional⇒inductive {suc n} {x ∷ xs} {y ∷ ys} xs∼ys =
    (head xs∼ys) ∷ extensional⇒inductive (tail xs∼ys)

  inductive⇒extensional : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
                           IPointwise _∼_ xs ys → Pointwise _∼_ xs ys
  inductive⇒extensional []             = ext λ()
  inductive⇒extensional (x∼y ∷ xs∼ys) = ext λ
    { zero    → x∼y
    ; (suc i) → Pointwise.app (inductive⇒extensional xs∼ys) i
    }

  equivalent : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
               Pointwise _∼_ xs ys ⇔ IPointwise _∼_ xs ys
  equivalent = equivalence extensional⇒inductive inductive⇒extensional

------------------------------------------------------------------------
-- Relational properties

refl : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} →
       ∀ {n} → Reflexive _∼_ → Reflexive (Pointwise _∼_ {n = n})
refl ∼-rfl = ext (λ _ → ∼-rfl)

sym : ∀ {a b ℓ} {A : Set a} {B : Set b} {P : REL A B ℓ} {Q : REL B A ℓ}
      {n} → Sym P Q → Sym (Pointwise P) (Pointwise Q {n = n})
sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i)

trans : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
        {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {n} →
        Trans P Q R →
        Trans (Pointwise P) (Pointwise Q) (Pointwise R {n = n})
trans trns xs∼ys ys∼zs = ext λ i →
  trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i)

decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
            Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n})
decidable dec xs ys = Dec.map
  (Setoid.sym (⇔-setoid _) equivalent)
  (Inductive.decidable dec xs ys)

isEquivalence : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} →
                ∀ {n} → IsEquivalence _∼_ →
                IsEquivalence (Pointwise _∼_ {n = n})
isEquivalence equiv = record
  { refl  = refl  Eq.refl
  ; sym   = sym   Eq.sym
  ; trans = trans Eq.trans
  } where module Eq = IsEquivalence equiv

isDecEquivalence : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} →
                   ∀ {n} → IsDecEquivalence _∼_ →
                   IsDecEquivalence (Pointwise _∼_ {n = n})
isDecEquivalence decEquiv = record
  { isEquivalence = isEquivalence DecEq.isEquivalence
  ; _≟_           = decidable DecEq._≟_
  } where module DecEq = IsDecEquivalence decEquiv

------------------------------------------------------------------------
-- Pointwise _≡_ is equivalent to _≡_.

module _ {a} {A : Set a} where

  Pointwise-≡⇒≡ : ∀ {n} {xs ys : Vec A n} →
                     Pointwise _≡_ xs ys → xs ≡ ys
  Pointwise-≡⇒≡ {zero}  {[]}      {[]}      (ext app) = P.refl
  Pointwise-≡⇒≡ {suc n} {x ∷ xs} {y ∷ ys} xs∼ys =
    P.cong₂ _∷_ (head xs∼ys) (Pointwise-≡⇒≡ (tail xs∼ys))

  ≡⇒Pointwise-≡ : ∀ {n} {xs ys : Vec A n} →
                     xs ≡ ys → Pointwise _≡_ xs ys
  ≡⇒Pointwise-≡ P.refl = refl P.refl

  Pointwise-≡↔≡ : ∀ {n} {xs ys : Vec A n} →
                Pointwise _≡_ xs ys ⇔ xs ≡ ys
  Pointwise-≡↔≡ {ℓ} {A} =
    Equiv.equivalence Pointwise-≡⇒≡ ≡⇒Pointwise-≡

------------------------------------------------------------------------
-- Pointwise and Plus commute when the underlying relation is
-- reflexive.
module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where

  ⁺∙⇒∙⁺ : ∀ {n} {xs ys : Vec A n} →
          Plus (Pointwise _∼_) xs ys → Pointwise (Plus _∼_) xs ys
  ⁺∙⇒∙⁺ [ ρ≈ρ′ ]            = ext (λ x → [ Pointwise.app ρ≈ρ′ x ])
  ⁺∙⇒∙⁺ (ρ ∼⁺⟨ ρ≈ρ′ ⟩ ρ′≈ρ″) =  ext (λ x →
    _ ∼⁺⟨ Pointwise.app (⁺∙⇒∙⁺ ρ≈ρ′ ) x ⟩
         Pointwise.app (⁺∙⇒∙⁺ ρ′≈ρ″) x)

  ∙⁺⇒⁺∙ : ∀ {n} {xs ys : Vec A n} → Reflexive _∼_ →
          Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys
  ∙⁺⇒⁺∙ rfl =
    Plus.map (_⟨$⟩_ (Equivalence.from equivalent)) ∘
    helper ∘
    _⟨$⟩_ (Equivalence.to equivalent)
    where
    helper : ∀ {n} {xs ys : Vec A n} →
             IPointwise (Plus _∼_) xs ys → Plus (IPointwise _∼_) xs ys
    helper []                                                  = [ [] ]
    helper (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x∼y xs∼ys) =
      x ∷ xs  ∼⁺⟨ Plus.map (_∷ Inductive.refl rfl) x∼y ⟩
      y ∷ xs  ∼⁺⟨ Plus.map (rfl ∷_) (helper xs∼ys) ⟩∎
      y ∷ ys  ∎

-- ∙⁺⇒⁺∙ cannot be defined if the requirement of reflexivity
-- is dropped.
private

 module Counterexample where

  data D : Set where
    i j x y z : D

  data _R_ : Rel D ℓ₀ where
    iRj : i R j
    xRy : x R y
    yRz : y R z

  xR⁺z : x [ _R_ ]⁺ z
  xR⁺z =
    x  ∼⁺⟨ [ xRy ] ⟩
    y  ∼⁺⟨ [ yRz ] ⟩∎
    z  ∎

  ix : Vec D 2
  ix = i ∷ x ∷ []

  jz : Vec D 2
  jz = j ∷ z ∷ []

  ix∙⁺jz : IPointwise (Plus _R_) ix jz
  ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ []

  ¬ix⁺∙jz : ¬ Plus′ (IPointwise _R_) ix jz
  ¬ix⁺∙jz [ iRj ∷ () ∷ [] ]
  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ])
  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _)

  counterexample :
    ¬ (∀ {n} {xs ys : Vec D n} →
         Pointwise (Plus _R_) xs ys →
         Plus (Pointwise _R_) xs ys)
  counterexample ∙⁺⇒⁺∙ =
    ¬ix⁺∙jz (Equivalence.to Plus.equivalent ⟨$⟩
               Plus.map (_⟨$⟩_ (Equivalence.to equivalent))
                 (∙⁺⇒⁺∙ (Equivalence.from equivalent ⟨$⟩ ix∙⁺jz)))

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

Pointwise-≡ = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Pointwise-≡
"Warning: Pointwise-≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}


text:
module IPC.Metatheory.Hilbert-BasicTarski where

open import IPC.Syntax.Hilbert public
open import IPC.Semantics.BasicTarski public

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)   γ = lookup i γ
eval (app t u) γ = (eval t γ) (eval u γ)
eval ci        γ = I
eval ck        γ = K
eval cs        γ = S
eval cpair     γ = _,_
eval cfst      γ = π₁
eval csnd      γ = π₂
eval unit      γ = ∙
eval cboom     γ = elim𝟘
eval cinl      γ = ι₁
eval cinr      γ = ι₂
eval ccase     γ = elim⊎

-- Correctness of evaluation with respect to conversion.

eval✓ : ∀ {{_ : Model}} {A Γ} {t t′ : Γ ⊢ A} → t ⋙ t′ → eval t ≡ eval t′
eval✓ refl⋙                         = refl
eval✓ (trans⋙ p q)                  = trans (eval✓ p) (eval✓ q)
eval✓ (sym⋙ p)                      = sym (eval✓ p)
eval✓ (congapp⋙ {A} {B} p q)        = cong² (_⟦$⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congi⋙ p)                    = cong I (eval✓ p)
eval✓ (congk⋙ p q)                  = cong² K (eval✓ p) (eval✓ q)
eval✓ (congs⋙ {A} {B} {C} p q r)    = cong³ (⟦S⟧ {A} {B} {C}) (eval✓ p) (eval✓ q) (eval✓ r)
eval✓ (congpair⋙ {A} {B} p q)       = cong² (_⟦,⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congfst⋙ {A} {B} p)          = cong (⟦π₁⟧ {A} {B}) (eval✓ p)
eval✓ (congsnd⋙ {A} {B} p)          = cong (⟦π₂⟧ {A} {B}) (eval✓ p)
eval✓ (congboom⋙ {C} p)             = cong (⟦elim𝟘⟧ {C}) (eval✓ p)
eval✓ (conginl⋙ {A} {B} p)          = cong (⟦ι₁⟧ {A} {B}) (eval✓ p)
eval✓ (conginr⋙ {A} {B} p)          = cong (⟦ι₂⟧ {A} {B}) (eval✓ p)
eval✓ (congcase⋙ {A} {B} {C} p q r) = cong³ (⟦celim⊎⟧ {A} {B} {C}) (eval✓ p) (eval✓ q) (eval✓ r)
eval✓ beta▻ₖ⋙                       = refl
eval✓ beta▻ₛ⋙                       = refl
eval✓ beta∧₁⋙                       = refl
eval✓ beta∧₂⋙                       = refl
eval✓ eta∧⋙                         = refl
eval✓ eta⊤⋙                        = refl
eval✓ beta∨₁⋙                       = refl
eval✓ beta∨₂⋙                       = refl

ext: agda

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Definition
open import Groups.Abelian.Definition
open import Groups.FiniteGroups.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Setoids.Setoids
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Functions
open import Semirings.Definition
open import Numbers.Modulo.Definition
open import Numbers.Modulo.Addition
open import Orders.Total.Definition
open import Numbers.Modulo.ModuloFunction
open import Numbers.Integers.Definition
open import Numbers.Modulo.Group
open import Modules.Definition
open import Numbers.Integers.RingStructure.Ring

module Numbers.Modulo.ZModule {n : ℕ} (pr : 0 <N n) where

timesNat : ℕ → ℤn n pr → ℤn n pr
timesNat 0 b = record { x = 0 ; xLess = pr }
timesNat (succ x) b = _+n_ pr b (timesNat x b)

times : ℤ → ℤn n pr → ℤn n pr
times (nonneg x) b = timesNat x b
times (negSucc x) b = Group.inverse (ℤnGroup n pr) (timesNat (succ x) b)

dotDistributesLeft : (r : ℤ) → (x y : ℤn n pr) → times r ((_ +n x) y) ≡ (_ +n times r x) (times r y)
dotDistributesLeft (nonneg zero) x y = equalityCommutative (Group.identRight (ℤnGroup n pr))
dotDistributesLeft (nonneg (succ r)) x y rewrite dotDistributesLeft (nonneg r) x y = equalityZn (transitivity (equalityCommutative (modExtracts pr _ _)) (transitivity (applyEquality (mod n pr) (transitivity (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring (ℤn.x x) _ _)) (applyEquality (ℤn.x x +N_) (transitivity (Semiring.commutative ℕSemiring (ℤn.x y) _) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring _ (ℤn.x (timesNat r y)) (ℤn.x y))) (applyEquality (ℤn.x (timesNat r x) +N_) (Semiring.commutative ℕSemiring (ℤn.x (timesNat r y)) (ℤn.x y))))))) (Semiring.+Associative ℕSemiring (ℤn.x x) _ _))) (modExtracts pr _ _)))
dotDistributesLeft (negSucc r) x y = {!!}

ZnZModule : Module ℤRing (ℤnAbGroup n pr) times
Module.dotWellDefined (ZnZModule) refl refl = refl
Module.dotDistributesLeft (ZnZModule) {r} {x} {y} = dotDistributesLeft r x y
Module.dotDistributesRight (ZnZModule) = {!!}
Module.dotAssociative (ZnZModule) = {!!}
Module.dotIdentity (ZnZModule) {record { x = x ; xLess = xLess }} = {!!}


text:
------------------------------------------------------------------------------
-- Group theory properties
------------------------------------------------------------------------------

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

module GroupTheory.PropertiesATP where

open import GroupTheory.Base

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

postulate leftCancellation : ∀ {a b c} → a · b ≡ a · c → b ≡ c
{-# ATP prove leftCancellation #-}

postulate rightIdentity : ∀ a → a · ε ≡ a
{-# ATP prove rightIdentity #-}

postulate rightInverse : ∀ a → a · a ⁻¹ ≡ ε
{-# ATP prove rightInverse #-}

postulate rightCancellation : ∀ {a b c} → b · a ≡ c · a → b ≡ c
{-# ATP prove rightCancellation #-}

postulate y≡x⁻¹[xy] : ∀ a b → b ≡ a ⁻¹ · (a · b)
{-# ATP prove y≡x⁻¹[xy] #-}

postulate x≡[xy]y⁻¹ : ∀ a b → a ≡ (a · b) · b ⁻¹
{-# ATP prove x≡[xy]y⁻¹ #-}

postulate rightIdentityUnique : ∀ r → (∀ a → a · r ≡ a) → r ≡ ε
{-# ATP prove rightIdentityUnique #-}

-- A more appropiate version to be used in the proofs.
postulate rightIdentityUnique' : ∀ a r → a · r ≡ a → r ≡ ε
{-# ATP prove rightIdentityUnique' #-}

postulate leftIdentityUnique : ∀ l → (∀ a → l · a ≡ a) → l ≡ ε
{-# ATP prove leftIdentityUnique #-}

-- A more appropiate version to be used in the proofs.
postulate leftIdentityUnique' : ∀ a l → l · a ≡ a → l ≡ ε
{-# ATP prove leftIdentityUnique' #-}

postulate
  rightInverseUnique : ∀ {a} → ∃[ r ] (a · r ≡ ε) ∧ (∀ r' → a · r' ≡ ε → r ≡ r')
{-# ATP prove rightInverseUnique #-}

-- A more appropiate version to be used in the proofs.
postulate rightInverseUnique' : ∀ {a r} → a · r ≡ ε → a ⁻¹ ≡ r
{-# ATP prove rightInverseUnique' #-}

postulate
  leftInverseUnique : ∀ {a} → ∃[ l ] (l · a ≡ ε) ∧ (∀ l' → l' · a ≡ ε → l ≡ l')
{-# ATP prove leftInverseUnique #-}

-- A more appropiate version to be used in the proofs.
postulate leftInverseUnique' : ∀ {a l} → l · a ≡ ε → a ⁻¹ ≡ l
{-# ATP prove leftInverseUnique' #-}

postulate ⁻¹-involutive : ∀ a → a ⁻¹ ⁻¹ ≡ a
{-# ATP prove ⁻¹-involutive #-}

postulate identityInverse : ε ⁻¹ ≡ ε
{-# ATP prove identityInverse #-}

postulate inverseDistributive : ∀ a b → (a · b) ⁻¹ ≡ b ⁻¹ · a ⁻¹
{-# ATP prove inverseDistributive #-}

-- The equation xa = b has an unique solution.
postulate
  xa≡b-uniqueSolution : ∀ a b → ∃[ x ] (x · a ≡ b) ∧ (∀ x' → x' · a ≡ b → x ≡ x')
{-# ATP prove xa≡b-uniqueSolution #-}

-- The equation ax = b has an unique solution.
postulate
  ax≡b-uniqueSolution : ∀ a b → ∃[ x ] (a · x ≡ b) ∧ (∀ x' → a · x' ≡ b → x ≡ x')
{-# ATP prove ax≡b-uniqueSolution #-}

-- If the square of every element is the identity, the system is
-- commutative. From: TPTP 6.4.0 problem GRP/GRP001-2.p.
postulate x²≡ε→comm : (∀ a → a · a ≡ ε) → ∀ {b c d} → b · c ≡ d → c · b ≡ d
{-# ATP prove x²≡ε→comm #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Ring.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

open import Cubical.Data.Sigma
open import Cubical.Relation.Binary.Poset

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring.Base

open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level

{-
  some basic calculations (used for example in QuotientRing.agda),
  that should become obsolete or subject to change once we have a
  ring solver (see https://github.com/agda/cubical/issues/297)
-}
module RingTheory (R' : Ring ℓ) where

  open RingStr (snd R')
  private R = ⟨ R' ⟩
  implicitInverse : (x y : R)
                 → x + y ≡ 0r
                 → y ≡ - x
  implicitInverse x y p =
    y               ≡⟨ sym (+Lid y) ⟩
    0r + y          ≡⟨ cong (λ u → u + y) (sym (+Linv x)) ⟩
    (- x + x) + y   ≡⟨ sym (+Assoc _ _ _) ⟩
    (- x) + (x + y) ≡⟨ cong (λ u → (- x) + u) p ⟩
    (- x) + 0r      ≡⟨ +Rid _ ⟩
    - x             ∎

  equalByDifference : (x y : R)
                      → x - y ≡ 0r
                      → x ≡ y
  equalByDifference x y p =
    x               ≡⟨ sym (+Rid _) ⟩
    x + 0r          ≡⟨ cong (λ u → x + u) (sym (+Linv y)) ⟩
    x + ((- y) + y) ≡⟨ +Assoc _ _ _ ⟩
    (x - y) + y     ≡⟨ cong (λ u → u + y) p ⟩
    0r + y          ≡⟨ +Lid _ ⟩
    y               ∎

  0Selfinverse : - 0r ≡ 0r
  0Selfinverse = sym (implicitInverse _ _ (+Rid 0r))

  0Idempotent : 0r + 0r ≡ 0r
  0Idempotent = +Lid 0r

  +Idempotency→0 : (x : R) → x ≡ x + x → x ≡ 0r
  +Idempotency→0 x p =
    x               ≡⟨ sym (+Rid x) ⟩
    x + 0r          ≡⟨ cong (λ u → x + u) (sym (+Rinv _)) ⟩
    x + (x + (- x)) ≡⟨ +Assoc _ _ _ ⟩
    (x + x) + (- x) ≡⟨ cong (λ u → u + (- x)) (sym p) ⟩
    x + (- x)       ≡⟨ +Rinv _ ⟩
    0r              ∎

  -Idempotent : (x : R) → -(- x) ≡ x
  -Idempotent x =  - (- x)   ≡⟨ sym (implicitInverse (- x) x (+Linv _)) ⟩
                   x ∎

  0RightAnnihilates : (x : R) → x · 0r ≡ 0r
  0RightAnnihilates x =
              let x·0-is-idempotent : x · 0r ≡ x · 0r + x · 0r
                  x·0-is-idempotent =
                    x · 0r               ≡⟨ cong (λ u → x · u) (sym 0Idempotent) ⟩
                    x · (0r + 0r)        ≡⟨ ·Rdist+ _ _ _ ⟩
                    (x · 0r) + (x · 0r)  ∎
              in (+Idempotency→0 _ x·0-is-idempotent)

  0LeftAnnihilates : (x : R) → 0r · x ≡ 0r
  0LeftAnnihilates x =
              let 0·x-is-idempotent : 0r · x ≡ 0r · x + 0r · x
                  0·x-is-idempotent =
                    0r · x               ≡⟨ cong (λ u → u · x) (sym 0Idempotent) ⟩
                    (0r + 0r) · x        ≡⟨ ·Ldist+ _ _ _ ⟩
                    (0r · x) + (0r · x)  ∎
              in +Idempotency→0 _ 0·x-is-idempotent

  -DistR· : (x y : R) →  x · (- y) ≡ - (x · y)
  -DistR· x y = implicitInverse (x · y) (x · (- y))

                               (x · y + x · (- y)     ≡⟨ sym (·Rdist+ _ _ _) ⟩
                               x · (y + (- y))        ≡⟨ cong (λ u → x · u) (+Rinv y) ⟩
                               x · 0r                 ≡⟨ 0RightAnnihilates x ⟩
                               0r ∎)

  -DistL· : (x y : R) →  (- x) · y ≡ - (x · y)
  -DistL· x y = implicitInverse (x · y) ((- x) · y)

                              (x · y + (- x) · y     ≡⟨ sym (·Ldist+ _ _ _) ⟩
                              (x - x) · y            ≡⟨ cong (λ u → u · y) (+Rinv x) ⟩
                              0r · y                 ≡⟨ 0LeftAnnihilates y ⟩
                              0r ∎)

  -Swap· : (x y : R) → (- x) · y ≡ x · (- y)
  -Swap· _ _ = -DistL· _ _ ∙ sym (-DistR· _ _)

  -IsMult-1 : (x : R) → - x ≡ (- 1r) · x
  -IsMult-1 _ = sym (·Lid _) ∙ sym (-Swap· _ _)

  -Dist : (x y : R) → (- x) + (- y) ≡ - (x + y)
  -Dist x y =
    implicitInverse _ _
         ((x + y) + ((- x) + (- y)) ≡⟨ sym (+Assoc _ _ _) ⟩
          x + (y + ((- x) + (- y))) ≡⟨ cong
                                         (λ u → x + (y + u))
                                         (+Comm _ _) ⟩
          x + (y + ((- y) + (- x))) ≡⟨ cong (λ u → x + u) (+Assoc _ _ _) ⟩
          x + ((y + (- y)) + (- x)) ≡⟨ cong (λ u → x + (u + (- x)))
                                            (+Rinv _) ⟩
          x + (0r + (- x))           ≡⟨ cong (λ u → x + u) (+Lid _) ⟩
          x + (- x)                 ≡⟨ +Rinv _ ⟩
          0r ∎)

  translatedDifference : (x a b : R) → a - b ≡ (x + a) - (x + b)
  translatedDifference x a b =
              a - b                       ≡⟨ cong (λ u → a + u)
                                                  (sym (+Lid _)) ⟩
              (a + (0r + (- b)))          ≡⟨ cong (λ u → a + (u + (- b)))
                                                  (sym (+Rinv _)) ⟩
              (a + ((x + (- x)) + (- b))) ≡⟨ cong (λ u → a + u)
                                                  (sym (+Assoc _ _ _)) ⟩
              (a + (x + ((- x) + (- b)))) ≡⟨ (+Assoc _ _ _) ⟩
              ((a + x) + ((- x) + (- b))) ≡⟨ cong (λ u → u + ((- x) + (- b)))
                                                  (+Comm _ _) ⟩
              ((x + a) + ((- x) + (- b))) ≡⟨ cong (λ u → (x + a) + u)
                                                  (-Dist _ _) ⟩
              ((x + a) - (x + b)) ∎

  +Assoc-comm1 : (x y z : R) → x + (y + z) ≡ y + (x + z)
  +Assoc-comm1 x y z = +Assoc x y z ∙∙ cong (λ x → x + z) (+Comm x y) ∙∙ sym (+Assoc y x z)

  +Assoc-comm2 : (x y z : R) → x + (y + z) ≡ z + (y + x)
  +Assoc-comm2 x y z = +Assoc-comm1 x y z ∙∙ cong (λ x → y + x) (+Comm x z) ∙∙ +Assoc-comm1 y z x

  +ShufflePairs : (a b c d : R)
                → (a + b) + (c + d) ≡ (a + c) + (b + d)
  +ShufflePairs a b c d =
    (a + b) + (c + d) ≡⟨ +Assoc _ _ _ ⟩
    ((a + b) + c) + d ≡⟨ cong (λ u → u + d) (sym (+Assoc _ _ _)) ⟩
    (a + (b + c)) + d ≡⟨ cong (λ u → (a + u) + d) (+Comm _ _) ⟩
    (a + (c + b)) + d ≡⟨ cong (λ u → u + d) (+Assoc _ _ _) ⟩
    ((a + c) + b) + d ≡⟨ sym (+Assoc _ _ _) ⟩
    (a + c) + (b + d) ∎

  ·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w
  ·-assoc2 x y z w = ·Assoc (x · y) z w ∙ cong (_· w) (sym (·Assoc x y z))

module RingHoms where
  open IsRingHom

  idRingHom : (R : Ring ℓ) → RingHom R R
  fst (idRingHom R) = idfun (fst R)
  snd (idRingHom R) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)

  compIsRingHom : {A : Ring ℓ} {B : Ring ℓ'} {C : Ring ℓ''}
    {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩}
    → IsRingHom (B .snd) g (C .snd)
    → IsRingHom (A .snd) f (B .snd)
    → IsRingHom (A .snd) (g ∘ f) (C .snd)
  compIsRingHom {g = g} {f} gh fh .pres0 = cong g (fh .pres0) ∙ gh .pres0
  compIsRingHom {g = g} {f} gh fh .pres1 = cong g (fh .pres1) ∙ gh .pres1
  compIsRingHom {g = g} {f} gh fh .pres+ x y = cong g (fh .pres+ x y) ∙ gh .pres+ (f x) (f y)
  compIsRingHom {g = g} {f} gh fh .pres· x y = cong g (fh .pres· x y) ∙ gh .pres· (f x) (f y)
  compIsRingHom {g = g} {f} gh fh .pres- x = cong g (fh .pres- x) ∙ gh .pres- (f x)

  compRingHom : {R : Ring ℓ} {S : Ring ℓ'} {T : Ring ℓ''}
              → RingHom R S → RingHom S T → RingHom R T
  fst (compRingHom f g) x = g .fst (f .fst x)
  snd (compRingHom f g) = compIsRingHom (g .snd) (f .snd)

  syntax compRingHom f g = g ∘r f

  compIdRingHom : {R S : Ring ℓ} (φ : RingHom R S) → compRingHom (idRingHom R) φ ≡ φ
  compIdRingHom φ = RingHom≡ refl

  idCompRingHom : {R S : Ring ℓ} (φ : RingHom R S) → compRingHom φ (idRingHom S) ≡ φ
  idCompRingHom φ = RingHom≡ refl

  compAssocRingHom : {R S T U : Ring ℓ} (φ : RingHom R S) (ψ : RingHom S T) (χ : RingHom T U) →
                     compRingHom (compRingHom φ ψ) χ ≡ compRingHom φ (compRingHom ψ χ)
  compAssocRingHom _ _ _ = RingHom≡ refl

module RingEquivs where
  open RingStr
  open IsRingHom
  open RingHoms

  compIsRingEquiv : {A : Ring ℓ} {B : Ring ℓ'} {C : Ring ℓ''}
    {g : ⟨ B ⟩ ≃ ⟨ C ⟩} {f : ⟨ A ⟩ ≃ ⟨ B ⟩}
    → IsRingEquiv (B .snd) g (C .snd)
    → IsRingEquiv (A .snd) f (B .snd)
    → IsRingEquiv (A .snd) (compEquiv f g) (C .snd)
  compIsRingEquiv {g = g} {f} gh fh = compIsRingHom {g = g .fst} {f .fst} gh fh

  compRingEquiv : {A : Ring ℓ} {B : Ring ℓ'} {C : Ring ℓ''}
                → RingEquiv A B → RingEquiv B C → RingEquiv A C
  fst (compRingEquiv f g) = compEquiv (f .fst) (g .fst)
  snd (compRingEquiv f g) = compIsRingEquiv {g = g .fst} {f = f .fst} (g .snd) (f .snd)

  isRingHomInv : {A : Ring ℓ} → {B : Ring ℓ'} → (e : RingEquiv A B) → IsRingHom (snd B) (invEq (fst e)) (snd A)
  isRingHomInv {A = A} {B = B} e = makeIsRingHom
                         ((cong g (sym (pres1 fcrh))) ∙ retEq et (1r (snd A)))
                         (λ x y → g (snd B ._+_ x y)                 ≡⟨ cong g (sym (cong₂ (snd B ._+_) (secEq et x) (secEq et y))) ⟩
                                   g (snd B ._+_ (f (g x)) (f (g y))) ≡⟨ cong g (sym (pres+ fcrh (g x) (g y))) ⟩
                                   g (f (snd A ._+_ (g x) (g y)))     ≡⟨ retEq et (snd A ._+_ (g x) (g y)) ⟩
                                   snd A ._+_ (g x) (g y)  ∎)
                         (λ x y → g (snd B ._·_ x y)                 ≡⟨ cong g (sym (cong₂ (snd B ._·_) (secEq et x) (secEq et y))) ⟩
                                   g (snd B ._·_ (f (g x)) (f (g y))) ≡⟨ cong g (sym (pres· fcrh (g x) (g y))) ⟩
                                   g (f (snd A ._·_ (g x) (g y)))     ≡⟨ retEq et (snd A ._·_ (g x) (g y)) ⟩
                                   snd A ._·_ (g x) (g y)  ∎)
               where
               et = fst e
               f = fst et
               fcrh = snd e
               g = invEq et

  invEquivRing : {A : Ring ℓ} → {B : Ring ℓ'} → RingEquiv A B → RingEquiv B A
  fst (invEquivRing e) = invEquiv (fst e)
  snd (invEquivRing e) = isRingHomInv e

module RingHomTheory {R S : Ring ℓ} (φ : RingHom R S) where
  open RingTheory ⦃...⦄
  open RingStr ⦃...⦄
  open IsRingHom (φ .snd)
  private
    instance
      _ = R
      _ = S
      _ = snd R
      _ = snd S
    f = fst φ

  ker≡0→inj : ({x : ⟨ R ⟩} → f x ≡ 0r → x ≡ 0r)
            → ({x y : ⟨ R ⟩} → f x ≡ f y → x ≡ y)
  ker≡0→inj ker≡0 {x} {y} p = equalByDifference _ _ (ker≡0 path)
   where
   path : f (x - y) ≡ 0r
   path = f (x - y)     ≡⟨ pres+ _ _ ⟩
          f x + f (- y) ≡⟨ cong (f x +_) (pres- _) ⟩
          f x - f y     ≡⟨ cong (_- f y) p ⟩
          f y - f y     ≡⟨ +Rinv _ ⟩
          0r            ∎

-- the Ring version of uaCompEquiv
module RingUAFunctoriality where
 open RingStr
 open RingEquivs

 Ring≡ : (A B : Ring ℓ) → (
   Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
   Σ[ q0 ∈ PathP (λ i → p i) (0r (snd A)) (0r (snd B)) ]
   Σ[ q1 ∈ PathP (λ i → p i) (1r (snd A)) (1r (snd B)) ]
   Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
   Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
   Σ[ s ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
   PathP (λ i → IsRing (q0 i) (q1 i) (r+ i) (r· i) (s i)) (isRing (snd A)) (isRing (snd B)))
   ≃ (A ≡ B)
 Ring≡ A B = isoToEquiv theIso
   where
   open Iso
   theIso : Iso _ _
   fun theIso (p , q0 , q1 , r+ , r· , s , t) i = p i
                                                , ringstr (q0 i) (q1 i) (r+ i) (r· i) (s i) (t i)
   inv theIso x = cong ⟨_⟩ x , cong (0r ∘ snd) x , cong (1r ∘ snd) x
                , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (isRing ∘ snd) x
   rightInv theIso _ = refl
   leftInv theIso _ = refl

 caracRing≡ : {A B : Ring ℓ} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
 caracRing≡ {A = A} {B = B} p q P =
   sym (transportTransport⁻ (ua (Ring≡ A B)) p)
                                    ∙∙ cong (transport (ua (Ring≡ A B))) helper
                                    ∙∙ transportTransport⁻ (ua (Ring≡ A B)) q
     where
     helper : transport (sym (ua (Ring≡ A B))) p ≡ transport (sym (ua (Ring≡ A B))) q
     helper = Σ≡Prop
                (λ _ → isPropΣ
                          (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
                          λ _ → isOfHLevelPathP 1 (isPropIsRing _ _ _ _ _) _ _)
               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))

 uaCompRingEquiv : {A B C : Ring ℓ} (f : RingEquiv A B) (g : RingEquiv B C)
                  → uaRing (compRingEquiv f g) ≡ uaRing f ∙ uaRing g
 uaCompRingEquiv f g = caracRing≡ _ _ (
   cong ⟨_⟩ (uaRing (compRingEquiv f g))
     ≡⟨ uaCompEquiv _ _ ⟩
   cong ⟨_⟩ (uaRing f) ∙ cong ⟨_⟩ (uaRing g)
     ≡⟨ sym (cong-∙ ⟨_⟩ (uaRing f) (uaRing g)) ⟩
   cong ⟨_⟩ (uaRing f ∙ uaRing g) ∎)

open RingEquivs
open RingUAFunctoriality
recPT→Ring : {A : Type ℓ'} (𝓕  : A → Ring ℓ)
           → (σ : ∀ x y → RingEquiv (𝓕 x) (𝓕 y))
           → (∀ x y z → σ x z ≡ compRingEquiv (σ x y) (σ y z))
          ------------------------------------------------------
           → ∥ A ∥ → Ring ℓ
recPT→Ring 𝓕 σ compCoh = rec→Gpd isGroupoidRing 𝓕
  (3-ConstantCompChar 𝓕 (λ x y → uaRing (σ x y))
                          λ x y z → sym (  cong uaRing (compCoh x y z)
                                         ∙ uaCompRingEquiv (σ x y) (σ y z)))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module SystemF.Everything where

open import SystemF.Syntax public
open import SystemF.WellTyped public
open import SystemF.Substitutions.Lemmas public
open import SystemF.Substitutions public
open import SystemF.NormalForm public
open TypeLemmas public hiding (var)


text:
data Nat : Set where
  zero : Nat
  suc : Nat → Nat

test : ∀{N M : Nat} → Nat → Nat → Nat
test N M = {!.N N .M!}


text:
module nodcap.NF.Show where

open import Data.String using (String)

open import nodcap.Base
open import nodcap.NF.Typing

import nodcap.Show as S

showTerm : {Γ : Environment} → ⊢ⁿᶠ Γ → String
showTerm {Γ} x = S.showTerm (fromNF x)

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


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

-- This module shows that D<: typing is undecidable.
module DsubTermUndec where

open import Data.List as List
open import Data.List.All as All
open import Data.Nat as ℕ
open import Data.Maybe as Maybe
open import Data.Product
open import Data.Sum
open import Data.Empty renaming (⊥ to False)
open import Data.Vec as Vec renaming (_∷_ to _‼_ ; [] to nil) hiding (_++_)
open import Function

open import Data.Maybe.Properties as Maybeₚ
open import Data.Nat.Properties as ℕₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as ≡

open import DsubDef
open import DsubFull
open import DsubReduced
open import Dsub renaming (_⊢_<:_ to _⊢′_<:_)
open import Utils
open import DsubEquivSimpler

module DifferentProof where

  open import FsubMinus
  open FsubMinus.FsubMinus hiding (_↑_)
  open FsubMinusToDsubR
  open Undecidability′

  F<:⇒typing′ : ∀ {Γ S U} →
                  Γ ⊢F S <: U →
                  ⟪ Γ ⟫ ⊢ val ⟨A= ⟦ S ⟧ ⟩ ∶ ⟨A: ⊥ ⋯ ⟦ U ⟧ ⟩
  F<:⇒typing′ S<:U = <∶ ⟨A⟩-I (bnd ⊥<: (<:′⇒<: $ F<:⇒D<: S<:U))

  bnd<:⇒F<:′ : ∀ {Γ S U} →
                  ⟪ Γ ⟫ ⊢″ ⟨A: ⟦ S ⟧ ⋯ ⟦ S ⟧ ⟩ <: ⟨A: ⊥ ⋯ ⟦ U ⟧ ⟩ →
                  Γ ⊢F S <: U
  bnd<:⇒F<:′ {Γ} {S} {U} bnd<: = helper
    where open DsubInvProperties contraInvertible
          cΓ = ⟪⟫-contraEnv Γ
          helper : Γ ⊢F S <: U
          helper with ⟨A:⟩<:⟨A:⟩ (<:⇒<:ᵢ (<:″⇒<: bnd<:) cΓ) cΓ
          ... | _ , S<:U = D<:⇒F<: $ <:ᵢ⇒<: S<:U

  typing⇒F<:′ : ∀ {Γ S U} →
                  ⟪ Γ ⟫ ⊢ val ⟨A= ⟦ S ⟧ ⟩ ∶ ⟨A: ⊥ ⋯ ⟦ U ⟧ ⟩ →
                  Γ ⊢F S <: U
  typing⇒F<:′ typ = bnd<:⇒F<:′ $ <:⇒<:″ $ <:⇒<:′ (helper typ refl refl)
    where helper : ∀ {Γ Γ′ S S′ T} →
                     Γ′ ⊢ val ⟨A= S′ ⟩ ∶ T →
                     Γ′ ≡ ⟪ Γ ⟫ → S′ ≡ ⟦ S ⟧ →
                     ⟪ Γ ⟫ ⊢ ⟨A: ⟦ S ⟧ ⋯ ⟦ S ⟧ ⟩ <: T
          helper ⟨A⟩-I eqΓ refl = refl
          helper (<∶ typ x) refl eqS = tran _ (helper typ refl eqS) x


text:
{-# OPTIONS --warning=error --safe --without-K --guardedness #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Numbers.Integers.Integers
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Subtraction
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.Exponentiation
open import Numbers.Primes.PrimeNumbers
open import Maybe
open import Semirings.Definition
open import Numbers.Naturals.EuclideanAlgorithm
open import Sequences
open import Vectors

module LectureNotes.NumbersAndSets.Examples1 where

open Semiring ℕSemiring
open import Semirings.Solver ℕSemiring multiplicationNIsCommutative

private
  abstract
    q1Lemma1 : {q r : ℕ} → 3 *N succ q +N r ≡ succ (succ (succ (3 *N q +N r)))
    q1Lemma1 {q} {r} rewrite sumZeroRight q | commutative q (succ q) | commutative q (succ (succ (q +N q))) | +Associative q q q = refl

    q1Lemma : {n : ℕ} → (2 <N n) → ((3 ∣ n) || (3 ∣ (n +N 2))) || (3 ∣ (n +N 4))
    q1Lemma {zero} ()
    q1Lemma {succ zero} (le zero ())
    q1Lemma {succ zero} (le (succ x) ())
    q1Lemma {succ (succ zero)} (le (succ x) proof) rewrite Semiring.commutative ℕSemiring x 2 = exFalso (naughtE (equalityCommutative (succInjective (succInjective proof))))
    q1Lemma {succ (succ (succ zero))} 2<n = inl (inl (aDivA 3))
    q1Lemma {succ (succ (succ (succ zero)))} 2<n = inl (inr (divides (record { quot = 2 ; rem = zero ; pr = refl ; remIsSmall = inl (le 2 refl) ; quotSmall = inl (le 2 refl)}) refl))
    q1Lemma {succ (succ (succ (succ (succ zero))))} 2<n = inr (divides (record { quot = 3 ; rem = zero ; pr = refl ; remIsSmall = inl (le 2 refl) ; quotSmall = inl (le 2 refl)}) refl)
    q1Lemma {succ (succ (succ (succ (succ (succ n)))))} 2<n with q1Lemma {succ (succ (succ n))} (le n (applyEquality succ (Semiring.commutative ℕSemiring n 2)))
    q1Lemma {succ (succ (succ (succ (succ (succ n)))))} 2<n | inl (inl (divides record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } x)) = inl (inl (divides (record { quot = succ quot ; rem = rem ; pr = transitivity (q1Lemma1 {quot} {rem}) (applyEquality (λ x → succ (succ (succ x))) pr) ; remIsSmall = remIsSmall ; quotSmall = inl (le 2 refl) }) x))
    q1Lemma {succ (succ (succ (succ (succ (succ n)))))} 2<n | inl (inr (divides record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } x)) = inl (inr (divides record { quot = succ quot ; rem = rem ; pr = transitivity (q1Lemma1 {quot} {rem}) (applyEquality (λ x → succ (succ (succ x))) pr) ; remIsSmall = remIsSmall ; quotSmall = inl (le 2 refl) } x))
    q1Lemma {succ (succ (succ (succ (succ (succ n)))))} 2<n | inr (divides record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } x) = inr (divides record { quot = succ quot ; rem = rem ; pr = transitivity (q1Lemma1 {quot} {rem}) (applyEquality (λ x → succ (succ (succ x))) pr) ; remIsSmall = remIsSmall ; quotSmall = inl (le 2 refl) } x)

q1 : {n : ℕ} → Prime n → Prime (n +N 2) → Prime (n +N 4) → n ≡ 3
q1 {succ zero} record { p>1 = (le zero ()) ; pr = pr } pN+2 pN+4
q1 {succ zero} record { p>1 = (le (succ x) ()) ; pr = pr } pN+2 pN+4
q1 {succ (succ zero)} pN record { p>1 = p>1 ; pr = pr } pN+4 with pr {2} (divides (record { quot = 2 ; rem = zero ; pr = refl ; remIsSmall = inl (le 1 refl) ; quotSmall = inl (le 1 refl)}) refl) (le 1 refl) (le 1 refl)
q1 {succ (succ zero)} pN record { p>1 = p>1 ; pr = pr } pN+4 | ()
q1 {succ (succ (succ n))} pN pN+2 pN+4 with q1Lemma {succ (succ (succ n))} (le n (applyEquality succ (commutative n 2)))
q1 {succ (succ (succ n))} pN pN+2 pN+4 | inl (inl 3|n) = equalityCommutative (primeDivPrimeImpliesEqual threeIsPrime pN 3|n)
q1 {succ (succ (succ n))} pN pN+2 pN+4 | inl (inr 3|n+2) with primeDivPrimeImpliesEqual threeIsPrime pN+2 3|n+2
... | bl rewrite commutative n 2 = exFalso (naughtE (succInjective (succInjective (succInjective bl))))
q1 {succ (succ (succ n))} pN pN+2 pN+4 | inr 3|n+4 with primeDivPrimeImpliesEqual threeIsPrime pN+4 3|n+4
... | bl rewrite commutative n 4 = exFalso (naughtE (succInjective (succInjective (succInjective bl))))

q3Differences : ℕ → ℕ
q3Differences a = 2 *N a
q3Seq : (start : ℕ) → ℕ → ℕ
q3Seq start zero = start
q3Seq start (succ n) = q3Differences (succ n) +N q3Seq start n
q3SeqFirst : take 5 (funcToSequence (q3Seq 41)) ≡ 41 ,- 43 ,- 47 ,- 53 ,- 61 ,- []
q3SeqFirst = refl
q3N : (start : ℕ) (a : ℕ) → q3Seq start a ≡ start +N (a +N (a *N a))
q3N start zero = equalityCommutative (sumZeroRight start)
q3N start (succ a) rewrite q3N start a | sumZeroRight a =
  from (succ (plus (plus (const a) (succ (const a))) (plus (const start) (plus (const a) (times (const a) (const a))))))
  to (plus (const start) (succ (plus (const a) (succ (plus (const a) (times (const a) (succ (const a))))))))
  by applyEquality (λ i → succ (succ i)) (transitivity (+Associative (a +N a) start _) (transitivity (transitivity (applyEquality (_+N (a +N a *N a)) (commutative (a +N a) start)) (equalityCommutative (+Associative start _ _))) (applyEquality (start +N_) (equalityCommutative (+Associative a a (a +N a *N a))))))
q3NDivision : (start : ℕ) → start ∣ (q3Seq start start)
q3NDivision 0 = aDivA 0
q3NDivision (succ start) rewrite q3N (succ start) (succ start) = dividesBothImpliesDividesSum {succ start} {succ start} (aDivA (succ start)) (dividesBothImpliesDividesSum {succ start} {succ start} (aDivA (succ start)) (divides (record { quot = succ start ; rem = 0 ; pr = sumZeroRight _ ; remIsSmall = inl (succIsPositive start) ; quotSmall = inl (succIsPositive start) }) refl))

q3 : (start : ℕ) → ((n : ℕ) → Prime (q3Seq start n)) → False
q3 zero a with a 2
... | record { p>1 = p>1 ; pr = pr } with pr {2} (divides (record { quot = 3 ; rem = 0 ; pr = refl ; remIsSmall = inl (le 1 refl) ; quotSmall = inl (le 1 refl) }) refl) (le 3 refl) (succIsPositive 1)
... | ()
q3 (succ zero) a with a 0
... | record { p>1 = le zero () ; pr = pr }
... | record { p>1 = le (succ x) () ; pr = pr }
q3 (succ (succ start)) a with q3NDivision (succ (succ start))
... | r with a (succ (succ start))
... | s = compositeImpliesNotPrime (succ (succ start)) _ (succPreservesInequality (succIsPositive start)) (le (succ (succ start) +N ((start +N succ start) +N q3Seq (succ (succ start)) start)) (applyEquality (λ i → succ (succ i)) (from (succ (plus (plus (const start) (plus (plus (const start) (succ (const start))) (const (q3Seq (succ (succ start)) start)))) (succ (succ (const start))))) to plus (plus (const start) (succ (succ (plus (const start) zero)))) (succ (plus (plus (const start) (succ (plus (const start) zero))) (const (q3Seq (succ (succ start)) start)))) by applyEquality (λ i → succ (succ (succ (succ i)))) (transitivity (commutative _ start) (+Associative start start _))))) r s

q3' : ((n : ℕ) → Prime (q3Seq 41 n)) → False
q3' = q3 41

q6 : {n : ℕ} → 3 ∣ (n *N n) → 3 ∣ n
q6 {n} 3|n^2 with primesArePrime {3} {n} {n} threeIsPrime 3|n^2
q6 {n} 3|n^2 | inl x = x
q6 {n} 3|n^2 | inr x = x

_*q10_ : {a : ℕ} → {b : ℕ} → (0 <N a) → (0 <N b) → ℕ
*q10Pos : {a : ℕ} → {b : ℕ} → (0<a : 0 <N a) → (0<b : 0 <N b) → 0 <N (_*q10_ 0<a 0<b)

_*q10_ {succ zero} {succ b} 0<a 0<b = succ (succ b)
_*q10_ {succ (succ a)} {succ zero} 0<a 0<b = _*q10_ {succ a} {2} (le a (applyEquality succ (sumZeroRight a))) (le 1 refl)
_*q10_ {succ (succ a)} {succ (succ b)} 0<a 0<b = _*q10_ {succ a} {_*q10_ {succ (succ a)} {succ b} 0<a (le b (applyEquality succ (sumZeroRight b)))} (le a (applyEquality succ (sumZeroRight a))) (*q10Pos 0<a (le b (applyEquality succ (sumZeroRight b))))
*q10Pos {succ zero} {succ b} 0<a 0<b = le (succ b) (applyEquality (λ i → succ (succ i)) (sumZeroRight b))
*q10Pos {succ (succ a)} {succ zero} 0<a 0<b = *q10Pos (le a (applyEquality succ (sumZeroRight a))) (le 1 refl)
*q10Pos {succ (succ a)} {succ (succ b)} 0<a 0<b = *q10Pos (le a (applyEquality succ (sumZeroRight a))) (*q10Pos 0<a (le b (applyEquality succ (sumZeroRight b))))


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

syntax Monoid | M

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
-}

module Monoid.Signature where

open import SOAS.Context

open import SOAS.Common

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

-- Operator symbols
data Mₒ : Set where
  unitₒ addₒ : Mₒ

-- Term signature
M:Sig : Signature Mₒ
M:Sig = sig λ
  {  unitₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  }

open Signature M:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

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

open import Level using (0ℓ)

-- This module incldes various Agda lemmas that are independent of the project's domain

module LibraBFT.Lemmas where

 cong₃ : ∀{a b c d}{A : Set a}{B : Set b}{C : Set c}{D : Set d}
       → (f : A → B → C → D) → ∀{x y u v m n} → x ≡ y → u ≡ v → m ≡ n
       → f x u m ≡ f y v n
 cong₃ f refl refl refl = refl

 ≡-pi : ∀{a}{A : Set a}{x y : A}(p q : x ≡ y) → p ≡ q
 ≡-pi refl refl = refl

 Unit-pi : {u1 u2 : Unit}
         → u1 ≡ u2
 Unit-pi {unit} {unit} = refl

 ++-inj : ∀{a}{A : Set a}{m n o p : List A}
        → length m ≡ length n → m ++ o ≡ n ++ p
        → m ≡ n × o ≡ p
 ++-inj {m = []}     {x ∷ n} () hip
 ++-inj {m = x ∷ m}  {[]}    () hip
 ++-inj {m = []}     {[]}     lhip hip
   = refl , hip
 ++-inj {m = m ∷ ms} {n ∷ ns} lhip hip
   with ++-inj {m = ms} {ns} (suc-injective lhip) (proj₂ (∷-injective hip))
 ...| (mn , op) rewrite proj₁ (∷-injective hip)
    = cong (n ∷_) mn , op

 ++-abs : ∀{a}{A : Set a}{n : List A}(m : List A)
        → 1 ≤ length m → [] ≡ m ++ n → ⊥
 ++-abs [] ()
 ++-abs (x ∷ m) imp ()

 data All-vec {ℓ} {A : Set ℓ} (P : A → Set ℓ) : ∀ {n} → Vec {ℓ} A n → Set (Level.suc ℓ) where
   []  : All-vec P []
   _∷_ : ∀ {x n} {xs : Vec A n} (px : P x) (pxs : All-vec P xs) → All-vec P (x ∷ xs)

 ≤-unstep : ∀{m n} → suc m ≤ n → m ≤ n
 ≤-unstep (s≤s ss) = ≤-step ss

 ≡⇒≤ : ∀{m n} → m ≡ n → m ≤ n
 ≡⇒≤ refl = ≤-refl

 ∈-cong : ∀{a b}{A : Set a}{B : Set b}{x : A}{l : List A}
        → (f : A → B) → x ∈ l → f x ∈ List-map f l
 ∈-cong f (here px) = here (cong f px)
 ∈-cong f (there hyp) = there (∈-cong f hyp)

 All-self : ∀{a}{A : Set a}{xs : List A} → All (_∈ xs) xs
 All-self = All-tabulate (λ x → x)

 All-reduce⁺
   : ∀{a b}{A : Set a}{B : Set b}{Q : A → Set}{P : B → Set}
   → { xs : List A }
   → (f : ∀{x} → Q x → B)
   → (∀{x} → (prf : Q x) → P (f prf))
   → (all : All Q xs)
   → All P (All-reduce f all)
 All-reduce⁺ f hyp []         = []
 All-reduce⁺ f hyp (ax ∷ axs) = (hyp ax) ∷ All-reduce⁺ f hyp axs

 All-reduce⁻
   : ∀{a b}{A : Set a}{B : Set b}
     {Q : A → Set}
   → { xs : List A }
   → ∀ {vdq}
   → (f : ∀{x} → Q x → B)
   → (all : All Q xs)
   → vdq ∈ All-reduce f all
   → ∃[ v ] ∃[ v∈xs ] (vdq ≡ f {v} v∈xs)
 All-reduce⁻ {Q = Q} {(h ∷ _)} {vdq} f (px ∷ pxs) (here refl)  = h , px , refl
 All-reduce⁻ {Q = Q} {(_ ∷ t)} {vdq} f (px ∷ pxs) (there vdq∈) = All-reduce⁻ {xs = t} f pxs vdq∈

 List-index : ∀ {A : Set} → (_≟A_ : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)) → A → (l : List A) → Maybe (Fin (length l))
 List-index _≟A_ x l with break (_≟A x) l
 ...| not≡ , _ with length not≡ <? length l
 ...| no  _     = nothing
 ...| yes found = just ( fromℕ< {length not≡} {length l} found)

 nats : ℕ → List ℕ
 nats 0 = []
 nats (suc n) = (nats n) ++ (n ∷ [])

 _ : nats 4 ≡ 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
 _ = refl

 _ : Maybe-map toℕ (List-index _≟_ 2 (nats 4)) ≡ just 2
 _ = refl

 _ : Maybe-map toℕ (List-index _≟_ 4 (nats 4)) ≡ nothing
 _ = refl

 allDistinct : ∀ {A : Set} → List A → Set
 allDistinct l = ∀ (i j : Σ ℕ (_< length l)) →
                   proj₁ i ≡ proj₁ j
                   ⊎ List-lookup l (fromℕ< (proj₂ i)) ≢ List-lookup l (fromℕ< (proj₂ j))

 postulate -- TODO-1: currently unused; prove it, if needed
   allDistinct? : ∀ {A : Set} → {≟A : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)} → (l : List A) → Dec (allDistinct l)

  -- Extends an arbitrary relation to work on the head of
  -- the supplied list, if any.
 data OnHead {A : Set}(P : A → A → Set) (x : A) : List A → Set where
    []   : OnHead P x []
    on-∷ : ∀{y ys} → P x y → OnHead P x (y ∷ ys)

  -- Establishes that a list is sorted according to the supplied
  -- relation.
 data IsSorted {A : Set}(_<_ : A → A → Set) : List A → Set where
    []  : IsSorted _<_ []
    _∷_ : ∀{x xs} → OnHead _<_ x xs → IsSorted _<_ xs → IsSorted _<_ (x ∷ xs)

 OnHead-prop : ∀{A}(P : A → A → Set)(x : A)(l : List A)
             → Irrelevant P
             → isPropositional (OnHead P x l)
 OnHead-prop P x [] hyp [] [] = refl
 OnHead-prop P x (x₁ ∷ l) hyp (on-∷ x₂) (on-∷ x₃) = cong on-∷ (hyp x₂ x₃)

 IsSorted-prop : ∀{A}(_<_ : A → A → Set)(l : List A)
               → Irrelevant _<_
               → isPropositional (IsSorted _<_ l)
 IsSorted-prop _<_ [] hyp [] []                  = refl
 IsSorted-prop _<_ (x ∷ l) hyp (x₁ ∷ a) (x₂ ∷ b)
   = cong₂ _∷_ (OnHead-prop _<_ x l hyp x₁ x₂)
               (IsSorted-prop _<_ l hyp a b)

 IsSorted-map⁻ : {A : Set}{_≤_ : A → A → Set}
               → {B : Set}(f : B → A)(l : List B)
               → IsSorted (λ x y → f x ≤ f y) l
               → IsSorted _≤_ (List-map f l)
 IsSorted-map⁻ f .[] [] = []
 IsSorted-map⁻ f .(_ ∷ []) (x ∷ []) = [] ∷ []
 IsSorted-map⁻ f .(_ ∷ _ ∷ _) (on-∷ x ∷ (x₁ ∷ is)) = (on-∷ x) ∷ IsSorted-map⁻ f _ (x₁ ∷ is)

 transOnHead : ∀ {A} {l : List A} {y x : A} {_<_ : A → A → Set}
              → Transitive _<_
              → OnHead _<_ y l
              → x < y
              → OnHead _<_ x l
 transOnHead _ [] _ = []
 transOnHead trans (on-∷ y<f) x<y = on-∷ (trans x<y y<f)

 ++-OnHead : ∀ {A} {xs ys : List A} {y : A} {_<_ : A → A → Set}
           → OnHead _<_ y xs
           → OnHead _<_ y ys
           → OnHead _<_ y (xs ++ ys)
 ++-OnHead []         y<y₁ = y<y₁
 ++-OnHead (on-∷ y<x) _    = on-∷ y<x

 h∉t : ∀ {A} {t : List A} {h : A} {_<_ : A → A → Set}
     → Irreflexive _<_ _≡_ → Transitive _<_
     → IsSorted _<_ (h ∷ t)
     → h ∉ t
 h∉t irfl trans (on-∷ h< ∷ sxs) (here refl) = ⊥-elim (irfl h< refl)
 h∉t irfl trans (on-∷ h< ∷ (x₁< ∷ sxs)) (there h∈t)
   = h∉t irfl trans ((transOnHead trans x₁< h<) ∷ sxs) h∈t

 ≤-head : ∀ {A} {l : List A} {x y : A} {_<_ : A → A → Set} {_≤_ : A → A → Set}
        → Reflexive _≤_ → Trans _<_ _≤_ _≤_
        → y ∈ (x ∷ l) → IsSorted _<_ (x ∷ l)
        → _≤_ x y
 ≤-head ref≤ trans (here refl) _ = ref≤
 ≤-head ref≤ trans (there y∈) (on-∷ x<x₁ ∷ sl) = trans x<x₁ (≤-head ref≤ trans y∈ sl)

 -- TODO-1 : Better name and/or replace with library property
 Any-sym : ∀ {a b}{A : Set a}{B : Set b}{tgt : B}{l : List A}{f : A → B}
         → Any (λ x → tgt ≡ f x) l
         → Any (λ x → f x ≡ tgt) l
 Any-sym (here x)  = here (sym x)
 Any-sym (there x) = there (Any-sym x)

 Any-lookup-correct :  ∀ {a b}{A : Set a}{B : Set b}{tgt : B}{l : List A}{f : A → B}
                    → (p : Any (λ x → f x ≡ tgt) l)
                    → Any-lookup p ∈ l
 Any-lookup-correct (here px) = here refl
 Any-lookup-correct (there p) = there (Any-lookup-correct p)

 Any-lookup-correctP :  ∀ {a}{A : Set a}{l : List A}{P : A → Set}
                     → (p : Any P l)
                     → Any-lookup p ∈ l
 Any-lookup-correctP (here px) = here refl
 Any-lookup-correctP (there p) = there (Any-lookup-correctP p)

 Any-witness : ∀ {a b} {A : Set a} {l : List A} {P : A → Set b}
             → (p : Any P l) → P (Any-lookup p)
 Any-witness (here px) = px
 Any-witness (there x) = Any-witness x

 -- TODO-1: there is probably a library property for this.
 ∈⇒Any : ∀ {A : Set}{x : A}
       → {xs : List A}
       → x ∈ xs
       → Any (_≡ x) xs
 ∈⇒Any {x = x} (here refl) = here refl
 ∈⇒Any {x = x} {h ∷ t} (there xxxx) = there (∈⇒Any {xs = t} xxxx)

 false≢true : false ≢ true
 false≢true ()

 witness : {A : Set}{P : A → Set}{x : A}{xs : List A}
         → x ∈ xs → All P xs → P x
 witness x y = All-lookup y x

 maybe-⊥ : ∀{a}{A : Set a}{x : A}{y : Maybe A}
         → y ≡ just x
         → y ≡ nothing
         → ⊥
 maybe-⊥ () refl

 Maybe-map-cool : ∀ {S S₁ : Set} {f : S → S₁} {x : Maybe S} {z}
                → Maybe-map f x ≡ just z
                → x ≢ nothing
 Maybe-map-cool {x = nothing} ()
 Maybe-map-cool {x = just y} prf = λ x → ⊥-elim (maybe-⊥ (sym x) refl)

 Maybe-map-cool-1 : ∀ {S S₁ : Set} {f : S → S₁} {x : Maybe S} {z}
                  → Maybe-map f x ≡ just z
                  → Σ S (λ x' → f x' ≡ z)
 Maybe-map-cool-1 {x = nothing} ()
 Maybe-map-cool-1 {x = just y} {z = z} refl = y , refl

 Maybe-map-cool-2 : ∀ {S S₁ : Set} {f : S → S₁} {x : S} {z}
                  → f x ≡ z
                  → Maybe-map f (just x) ≡ just z
 Maybe-map-cool-2 {S}{S₁}{f}{x}{z} prf rewrite prf = refl

 T⇒true : ∀ {a : Bool} → T a → a ≡ true
 T⇒true {true} _ = refl

 isJust : ∀ {A : Set}{aMB : Maybe A}{a : A}
        → aMB ≡ just a
        → Is-just aMB
 isJust refl = just tt

 to-witness-isJust-≡ : ∀ {A : Set}{aMB : Maybe A}{a prf}
                     → to-witness (isJust {aMB = aMB} {a} prf) ≡ a
 to-witness-isJust-≡ {aMB = just a'} {a} {prf}
    with to-witness-lemma (isJust {aMB = just a'} {a} prf) refl
 ...| xxx = just-injective (trans (sym xxx) prf)

 deMorgan : ∀ {A B : Set} → (¬ A) ⊎ (¬ B) → ¬ (A × B)
 deMorgan (inj₁ ¬a) = λ a×b → ¬a (proj₁ a×b)
 deMorgan (inj₂ ¬b) = λ a×b → ¬b (proj₂ a×b)

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

 ∸-suc-≤ : ∀ (x w : ℕ) → suc x ∸ w ≤ suc (x ∸ w)
 ∸-suc-≤ x zero = ≤-refl
 ∸-suc-≤ zero (suc w) rewrite 0∸n≡0 w = z≤n
 ∸-suc-≤ (suc x) (suc w) = ∸-suc-≤ x w

 m∸n≤o⇒m∸o≤n : ∀ (x z w : ℕ) → x ∸ z ≤ w → x ∸ w ≤ z
 m∸n≤o⇒m∸o≤n x zero w p≤ rewrite m≤n⇒m∸n≡0 p≤ = z≤n
 m∸n≤o⇒m∸o≤n zero (suc z) w p≤ rewrite 0∸n≡0 w = z≤n
 m∸n≤o⇒m∸o≤n (suc x) (suc z) w p≤ = ≤-trans (∸-suc-≤ x w) (s≤s (m∸n≤o⇒m∸o≤n x z w p≤))

 tail-⊆ : ∀ {A : Set} {x} {xs ys : List A}
        → (x ∷ xs) ⊆List ys
        → xs ⊆List ys
 tail-⊆ xxs⊆ys x∈xs = xxs⊆ys (there x∈xs)

 allDistinctTail : ∀ {A : Set} {x} {xs : List A}
                 → allDistinct (x ∷ xs)
                 → allDistinct xs
 allDistinctTail allDist (i , i<l) (j , j<l)
   with allDist (suc i , s≤s i<l) (suc j , s≤s j<l)
 ...| inj₁ 1+i≡1+j = inj₁ (cong pred 1+i≡1+j)
 ...| inj₂ lookup≢ = inj₂ lookup≢

 ∈-Any-Index-elim : ∀ {A : Set} {x y} {ys : List A} (x∈ys : x ∈ ys)
                  → x ≢ y → y ∈ ys
                  → y ∈ ys ─ Any-index x∈ys
 ∈-Any-Index-elim (here refl)  x≢y (here refl)  = ⊥-elim (x≢y refl)
 ∈-Any-Index-elim (here refl)  _   (there y∈ys) = y∈ys
 ∈-Any-Index-elim (there _)    _   (here refl)  = here refl
 ∈-Any-Index-elim (there x∈ys) x≢y (there y∈ys) = there (∈-Any-Index-elim x∈ys x≢y y∈ys)

 ∉∧⊆List⇒∉ : ∀ {A : Set} {x} {xs ys : List A}
           → x ∉ xs → ys ⊆List xs
           → x ∉ ys
 ∉∧⊆List⇒∉ x∉xs ys∈xs x∈ys = ⊥-elim (x∉xs (ys∈xs x∈ys))

 allDistinctʳʳ : ∀ {A : Set} {x x₁ : A} {xs : List A}
               → allDistinct (x ∷ x₁ ∷ xs)
               → allDistinct (x ∷ xs)
 allDistinctʳʳ _ (zero , _) (zero , _) = inj₁ refl
 allDistinctʳʳ allDist (zero , i<l) (suc j , j<l)
   with allDist (0 , s≤s z≤n) (suc (suc j) , s≤s j<l)
 ...| inj₂ x≢lookup
      = inj₂ λ x≡lkpxs → ⊥-elim (x≢lookup x≡lkpxs)
 allDistinctʳʳ allDist (suc i , i<l) (zero , j<l)
   with allDist (suc (suc i) , s≤s i<l) (0 , s≤s z≤n)
 ...| inj₂ x≢lookup
      = inj₂ λ x≡lkpxs → ⊥-elim (x≢lookup x≡lkpxs)
 allDistinctʳʳ allDist (suc i , i<l) (suc j , j<l)
   with allDist (2 + i , (s≤s i<l)) (2 + j , s≤s j<l)
 ...| inj₁ si≡sj   = inj₁ (cong pred si≡sj)
 ...| inj₂ lookup≡ = inj₂ lookup≡

 allDistinct⇒∉ : ∀ {A : Set} {x} {xs : List A}
               → allDistinct (x ∷ xs)
               → x ∉ xs
 allDistinct⇒∉ allDist (here x≡x₁)
   with allDist (0 , s≤s z≤n) (1 , s≤s (s≤s z≤n))
 ... | inj₂ x≢x₁ = ⊥-elim (x≢x₁ x≡x₁)
 allDistinct⇒∉ allDist (there x∈xs)
   = allDistinct⇒∉ (allDistinctʳʳ allDist) x∈xs

 sumListMap : ∀ {A : Set} {x} {xs : List A} (f : A → ℕ) → (x∈xs : x ∈ xs)
            → f-sum f xs ≡ f x + f-sum f (xs ─ Any-index x∈xs)
 sumListMap _ (here refl)  = refl
 sumListMap {_} {x} {x₁ ∷ xs} f (there x∈xs)
   rewrite sumListMap f x∈xs
         | sym (+-assoc (f x) (f x₁) (f-sum f (xs ─ Any-index x∈xs)))
         | +-comm (f x) (f x₁)
         | +-assoc (f x₁) (f x) (f-sum f (xs ─ Any-index x∈xs)) = refl

 lookup⇒Any : ∀ {A : Set} {xs : List A} {P : A → Set} (i : Fin (length xs))
            → P (List-lookup xs i) → Any P xs
 lookup⇒Any {_} {_ ∷ _} zero    px = here px
 lookup⇒Any {_} {_ ∷ _} (suc i) px = there (lookup⇒Any i px)

 x∉→AllDistinct : ∀ {A : Set} {x} {xs : List A}
                → allDistinct xs
                → x ∉ xs
                → allDistinct (x ∷ xs)
 x∉→AllDistinct _ _ (0 , _) (0 , _) = inj₁ refl
 x∉→AllDistinct _ x∉xs (0 , _) (suc j , j<l)
   = inj₂ (λ x≡lkp → x∉xs (lookup⇒Any (fromℕ< (≤-pred j<l)) x≡lkp))
 x∉→AllDistinct _ x∉xs (suc i , i<l) (0 , _)
   = inj₂ (λ x≡lkp → x∉xs (lookup⇒Any (fromℕ< (≤-pred i<l)) (sym x≡lkp)))
 x∉→AllDistinct allDist x∉xs (suc i , i<l) (suc j , j<l)
   with allDist (i , (≤-pred i<l)) (j , (≤-pred j<l))
 ...| inj₁ i≡j   = inj₁ (cong suc i≡j)
 ...| inj₂ lkup≢ = inj₂ lkup≢

 module DecLemmas {A : Set} (_≟D_ : Decidable {A = A} (_≡_)) where

   _∈?_ : ∀ (x : A) → (xs : List A) → Dec (Any (x ≡_) xs)
   x ∈? xs = Any-any (x ≟D_) xs

   y∉xs⇒Allxs≢y : ∀ {xs : List A} {x y}
                → y ∉ (x ∷ xs)
                → x ≢ y × y ∉ xs
   y∉xs⇒Allxs≢y {xs} {x} {y} y∉
     with y ∈? xs
   ...| yes y∈xs = ⊥-elim (y∉ (there y∈xs))
   ...| no  y∉xs
     with x ≟D y
   ...| yes x≡y = ⊥-elim (y∉ (here (sym x≡y)))
   ...| no  x≢y = x≢y , y∉xs

   ⊆List-Elim :  ∀ {x} {xs ys : List A} (x∈ys : x ∈ ys)
              → x ∉ xs → xs ⊆List ys
              → xs ⊆List ys ─ Any-index x∈ys
   ⊆List-Elim (here refl) x∉xs xs∈ys x₂∈xs
     with xs∈ys x₂∈xs
   ...| here refl  = ⊥-elim (x∉xs x₂∈xs)
   ...| there x∈xs = x∈xs
   ⊆List-Elim (there x∈ys) x∉xs xs∈ys x₂∈xxs
     with x₂∈xxs
   ...| there x₂∈xs
         = ⊆List-Elim (there x∈ys) (proj₂ (y∉xs⇒Allxs≢y x∉xs)) (tail-⊆ xs∈ys) x₂∈xs
   ...| here refl
     with xs∈ys x₂∈xxs
   ...| here refl = here refl
   ...| there x₂∈ys
         = there (∈-Any-Index-elim x∈ys (≢-sym (proj₁ (y∉xs⇒Allxs≢y x∉xs))) x₂∈ys)

   sum-⊆-≤ : ∀ {ys} (xs : List A) (f : A → ℕ)
           → allDistinct xs
           → xs ⊆List ys
           → f-sum f xs ≤ f-sum f ys
   sum-⊆-≤ [] _ _ _ = z≤n
   sum-⊆-≤ (x ∷ xs) f dxs xs⊆ys
      rewrite sumListMap f (xs⊆ys (here refl))
      = let x∉xs    = allDistinct⇒∉ dxs
            xs⊆ysT  = tail-⊆ xs⊆ys
            xs⊆ys-x = ⊆List-Elim (xs⊆ys (here refl)) x∉xs xs⊆ysT
            disTail = allDistinctTail dxs
       in +-monoʳ-≤ (f x) (sum-⊆-≤ xs f disTail xs⊆ys-x)

   intersect : List A → List A → List A
   intersect xs [] = []
   intersect xs (y ∷ ys)
     with y ∈? xs
   ...| yes _ = y ∷ intersect xs ys
   ...| no  _ = intersect xs ys

   union : List A → List A → List A
   union xs [] = xs
   union xs (y ∷ ys)
     with y ∈? xs
   ...| yes _ = union xs ys
   ...| no  _ = y ∷ union xs ys

   ∈-intersect : ∀ (xs ys : List A) {α}
               → α ∈ intersect xs ys
               → α ∈ xs × α ∈ ys
   ∈-intersect xs (y ∷ ys) α∈int
     with y ∈? xs  | α∈int
   ...| no  y∉xs   | α∈        = ×-map₂ there (∈-intersect xs ys α∈)
   ...| yes y∈xs   | here refl = y∈xs , here refl
   ...| yes y∈xs   | there α∈  = ×-map₂ there (∈-intersect xs ys α∈)

   x∉⇒x∉intersect : ∀ {x} {xs ys : List A}
                    → x ∉ xs ⊎ x ∉ ys
                    → x ∉ intersect xs ys
   x∉⇒x∉intersect {x} {xs} {ys} x∉ x∈int
     = contraposition (∈-intersect xs ys) (deMorgan x∉) x∈int

   intersectDistinct : ∀ (xs ys : List A)
                     → allDistinct xs → allDistinct ys
                     → allDistinct (intersect xs ys)
   intersectDistinct xs (y ∷ ys) dxs dys
     with y ∈? xs
   ...| yes y∈xs = let distTail  = allDistinctTail dys
                       intDTail  = intersectDistinct xs ys dxs distTail
                       y∉intTail = x∉⇒x∉intersect (inj₂ (allDistinct⇒∉ dys))
                   in x∉→AllDistinct intDTail y∉intTail
   ...| no  y∉xs = intersectDistinct xs ys dxs (allDistinctTail dys)

   x∉⇒x∉union : ∀ {x} {xs ys : List A}
              → x ∉ xs × x ∉ ys
              → x ∉ union xs ys
   x∉⇒x∉union {_} {_} {[]} (x∉xs , _) x∈∪ = ⊥-elim (x∉xs x∈∪)
   x∉⇒x∉union {x} {xs} {y ∷ ys} (x∉xs , x∉ys) x∈union
     with y ∈? xs  | x∈union
   ...| yes y∈xs   | x∈∪
        = ⊥-elim (x∉⇒x∉union (x∉xs , (proj₂ (y∉xs⇒Allxs≢y x∉ys))) x∈∪)
   ...| no y∉xs    | here refl
        = ⊥-elim (proj₁ (y∉xs⇒Allxs≢y x∉ys) refl)
   ...| no y∉xs    | there x∈∪
        = ⊥-elim (x∉⇒x∉union (x∉xs , (proj₂ (y∉xs⇒Allxs≢y x∉ys))) x∈∪)

   unionDistinct : ∀ (xs ys : List A)
               → allDistinct xs → allDistinct ys
               → allDistinct (union xs ys)
   unionDistinct xs [] dxs dys = dxs
   unionDistinct xs (y ∷ ys) dxs dys
      with y ∈? xs
   ...| yes y∈xs = unionDistinct xs ys dxs (allDistinctTail dys)
   ...| no  y∉xs = let distTail  = allDistinctTail dys
                       uniDTail  = unionDistinct xs ys dxs distTail
                       y∉intTail = x∉⇒x∉union (y∉xs , allDistinct⇒∉ dys)
                   in x∉→AllDistinct uniDTail y∉intTail

   sumIntersect≤ : ∀ (xs ys : List A) (f : A → ℕ)
                 → f-sum f (intersect xs ys) ≤ f-sum f (xs ++ ys)
   sumIntersect≤ _ [] _ = z≤n
   sumIntersect≤ xs (y ∷ ys) f
     with y ∈? xs
   ...| yes y∈xs rewrite map-++-commute f xs (y ∷ ys)
                       | sum-++-commute (List-map f xs) (List-map f (y ∷ ys))
                       | sym (+-assoc (f-sum f xs) (f y) (f-sum f ys))
                       | +-comm (f-sum f xs) (f y)
                       | +-assoc (f y) (f-sum f xs) (f-sum f ys)
                       | sym (sum-++-commute (List-map f xs) (List-map f ys))
                       | sym (map-++-commute f xs ys)
                         = +-monoʳ-≤ (f y) (sumIntersect≤ xs ys f)
   ...| no  y∉xs rewrite map-++-commute f xs (y ∷ ys)
                       | sum-++-commute (List-map f xs) (List-map f (y ∷ ys))
                       | +-comm (f y) (f-sum f ys)
                       | sym (+-assoc (f-sum f xs) (f-sum f ys) (f y))
                       | sym (sum-++-commute (List-map f xs) (List-map f ys))
                       | sym (map-++-commute f xs ys)
                         = ≤-stepsʳ (f y) (sumIntersect≤ xs ys f)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

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

module Haskell.Modules.Eq where

open import Haskell.Modules.ToBool
------------------------------------------------------------------------------
open import Data.Bool hiding (_≟_; not)
open import Data.List                               as DL
open import Data.Maybe using (Maybe; just; nothing)
import      Data.Nat                                as DN
open import Function using (_$_; _∘_)
import      Relation.Binary.PropositionalEquality   as PE using (_≡_; refl)
import      Relation.Nullary                        as RN

record Eq {a} (A : Set a) : Set a where
  infix 4 _≟_ _==_ _/=_
  field
    _≟_ : (a b : A) → RN.Dec (a PE.≡ b)

  _==_   : A → A → Bool
  a == b = toBool $ a ≟ b

  _/=_ : A → A → Bool
  a /= b = not (a == b)
open Eq ⦃ ... ⦄ public

import Data.List.Relation.Unary.Any as Any using (any)

elem : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ → A → DL.List A → Bool
elem x = toBool ∘ Any.any (x ≟_)

instance
  Eq-Nat : Eq DN.ℕ
  Eq._≟_ Eq-Nat = DN._≟_

  Eq-Maybe : ∀ {a} {A : Set a} ⦃ _ : Eq A ⦄ → Eq (Maybe A)
  Eq._≟_ Eq-Maybe  nothing  nothing = RN.yes PE.refl
  Eq._≟_ Eq-Maybe (just _)  nothing = RN.no λ ()
  Eq._≟_ Eq-Maybe  nothing (just _) = RN.no λ ()
  Eq._≟_ Eq-Maybe (just a) (just b)
     with a ≟ b
  ... | RN.no  proof   = RN.no λ where PE.refl → proof PE.refl
  ... | RN.yes PE.refl = RN.yes PE.refl


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Cat.Facts.Exponential where

open import Data.Product using (_,_)
open import Level using (_⊔_)
open import Relation.Binary using (IsEquivalence)

open import Cats.Bifunctor using
  (Bifunctor ; Bifunctor→Functor₁ ; transposeBifunctor₁ ; transposeBifunctor₁-resp)
open import Cats.Category
open import Cats.Category.Cat as Cat′ using
  (Cat ; Functor ; _∘_ ; _≈_) renaming
  (id to Id)
open import Cats.Category.Cat.Facts.Product using (hasBinaryProducts ; ⟨_×_⟩)
open import Cats.Category.Fun using (_↝_ ; Trans ; ≈-intro ; ≈-elim)
open import Cats.Category.Fun.Facts.Iso using (≈→≅)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Trans.Iso as NatIso using (NatIso)
open import Cats.Util.Conv

import Cats.Category.Base as Base
import Cats.Category.Constructions.Unique as Unique
import Cats.Category.Constructions.Iso as Iso

open Functor
open Trans
open Iso.Iso

private
  module Cat≈ {lo la l≈ lo′ la′ l≈′}
    {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    = IsEquivalence (Cat′.equiv {C = C} {D})

  module Fun {lo la l≈ lo′ la′ l≈′}
    {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    = Category (C ↝ D)

module _ {lo la l≈ lo′ la′ l≈′}
  {B : Category lo la l≈} {C : Category lo′ la′ l≈′}
  where

  private
    module B = Category B
    module C = Category C

  Eval : Bifunctor (B ↝ C) B C
  Eval = record
      { fobj = λ where
          (F , x) → fobj F x
      ; fmap = λ where
          {F , a} {G , b} (θ , f) → fmap G f C.∘ component θ a
      ; fmap-resp = λ where
          {F , a} {G , b} {θ , f} {ι , g} (θ≈ι , f≈g) →
            C.∘-resp (fmap-resp G f≈g) (≈-elim θ≈ι)
      ; fmap-id = λ { {F , b} → C.≈.trans (C.∘-resp-l (fmap-id F)) C.id-l }
      ; fmap-∘ = λ where
          {F , a} {G , b} {H , c} {θ , f} {ι , g} →
            begin
              (fmap H f C.∘ component θ b) C.∘ (fmap G g C.∘ component ι a)
            ≈⟨ C.∘-resp-l (C.≈.sym (natural θ)) ⟩
              (component θ c C.∘ fmap G f) C.∘ (fmap G g C.∘ component ι a)
            ≈⟨ C.assoc ⟩
              component θ c C.∘ fmap G f C.∘ (fmap G g C.∘ component ι a)
            ≈⟨ C.∘-resp-r C.unassoc ⟩
              component θ c C.∘ (fmap G f C.∘ fmap G g) C.∘ component ι a
            ≈⟨ C.∘-resp-r (C.∘-resp-l (fmap-∘ G)) ⟩
              component θ c C.∘ fmap G (f B.∘ g) C.∘ component ι a
            ≈⟨ C.unassoc ⟩
              (component θ c C.∘ fmap G (f B.∘ g)) C.∘ component ι a
            ≈⟨ C.∘-resp-l (natural θ) ⟩
              (fmap H (f B.∘ g) C.∘ component θ a) C.∘ component ι a
            ≈⟨ C.assoc ⟩
              fmap H (f B.∘ g) C.∘ component θ a C.∘ component ι a
            ∎
      }
    where
      open C.≈-Reasoning

module _ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  {B : Category lo la l≈} {C : Category lo′ la′ l≈′} {D : Category lo″ la″ l≈″}
  where

  private
    module B = Category B
    module C = Category C
    module D = Category D

  Curry : Bifunctor B C D → Functor B (C ↝ D)
  Curry F = transposeBifunctor₁ F

  Curry-resp : ∀ {F G} → F ≈ G → Curry F ≈ Curry G
  Curry-resp = transposeBifunctor₁-resp

  Curry-correct : ∀ {F} → Eval ∘ ⟨ Curry F × Id ⟩ ≈ F
  Curry-correct {F} = record
      { iso = D.≅.refl
      ; forth-natural = λ where
        {a , a′} {b , b′} {f , f′} →
          begin
            D.id D.∘ fmap F (B.id , f′) D.∘ fmap F (f , C.id)
          ≈⟨ D.≈.trans D.id-l (fmap-∘ F) ⟩
            fmap F (B.id B.∘ f , f′ C.∘ C.id)
          ≈⟨ fmap-resp F (B.id-l , C.id-r) ⟩
            fmap F (f , f′)
          ≈⟨ D.≈.sym D.id-r ⟩
            fmap F (f , f′) D.∘ D.id
          ∎
      }
    where
      open D.≈-Reasoning

  Curry-unique : ∀ {F Curry′}
    → Eval ∘ ⟨ Curry′ × Id ⟩ ≈ F
    → Curry′ ≈ Curry F
  Curry-unique {F} {Curry′} eq@record { iso = iso ; forth-natural = fnat } = record
      { iso = λ {x} →
          let open Fun.≅-Reasoning in
          Fun.≅.sym (
            begin
              fobj (Curry F) x
            ≈⟨ NatIso.iso (Curry-resp (Cat≈.sym eq)) ⟩
              fobj (Curry (Eval ∘ ⟨ Curry′ × Id ⟩)) x
            ≈⟨ ≈→≅ (lem x) ⟩
              fobj Curry′ x
            ∎
          )
      ; forth-natural = λ {a} {b} {f} → ≈-intro λ {x} →
          -- TODO We need a simplification tactic.
          let open D.≈-Reasoning in
          triangle (forth iso D.∘ component (fmap Curry′ f) x)
          ( begin
              ((forth iso D.∘
                 (fmap (fobj Curry′ b) C.id D.∘ component (fmap Curry′ B.id) x) D.∘ D.id) D.∘
               D.id D.∘ D.id) D.∘
              component (fmap Curry′ f) x
            ≈⟨ D.∘-resp-l (D.≈.trans (D.∘-resp-r D.id-l) (D.≈.trans D.id-r
                (D.≈.trans (D.∘-resp-r (D.≈.trans D.id-r (D.≈.trans
                  (D.∘-resp (fmap-id (fobj Curry′ b))
                    (≈-elim (fmap-id Curry′))) D.id-l))) D.id-r))) ⟩
              forth iso D.∘ component (fmap Curry′ f) x
            ∎
          )
          ( begin
              fmap F (f , C.id) D.∘
              (forth iso D.∘ (fmap (fobj Curry′ a) C.id D.∘ component (fmap Curry′ B.id) x) D.∘ D.id) D.∘
              D.id D.∘ D.id
            ≈⟨ D.∘-resp-r (D.≈.trans (D.∘-resp-r D.id-r) (D.≈.trans D.id-r
                (D.≈.trans (D.∘-resp-r (D.≈.trans D.id-r (D.≈.trans
                  (D.∘-resp-l (fmap-id (fobj Curry′ a)))
                    (D.≈.trans D.id-l (≈-elim (fmap-id Curry′)))))) D.id-r))) ⟩
              fmap F (f , C.id) D.∘ forth iso
            ≈⟨ D.≈.sym fnat ⟩
              forth iso D.∘ fmap (fobj Curry′ b) C.id D.∘ component (fmap Curry′ f) x
            ≈⟨ D.∘-resp-r (D.≈.trans (D.∘-resp-l (fmap-id (fobj Curry′ b))) D.id-l) ⟩
              forth iso D.∘ component (fmap Curry′ f) x
            ∎
          )
      }
    where
      lem : ∀ x
        → NatIso (Bifunctor→Functor₁ (Eval ∘ ⟨ Curry′ × Id ⟩) x) (fobj Curry′ x)
      lem x = record
          { iso = D.≅.refl
          ; forth-natural = D.≈.trans D.id-l (D.∘-resp-r (≈-elim (fmap-id Curry′)))
          }

  -- We get the following lemmas for free from HasExponentials, but only when
  -- all the categories are at the same (single) level.

  Uncurry : Functor B (C ↝ D) → Bifunctor B C D
  Uncurry F = Eval ∘ ⟨ F × Id ⟩

  Curry∘Uncurry : {F : Functor B (C ↝ D)}
    → Curry (Uncurry F) ≈ F
  Curry∘Uncurry {F} = Cat≈.sym (Curry-unique {Curry′ = F} Cat≈.refl)

  Uncurry∘Curry : {F : Bifunctor B C D}
    → Uncurry (Curry F) ≈ F
  Uncurry∘Curry {F} = Curry-correct {F = F}

instance
  hasExponentials : ∀ {l} → HasExponentials (Cat l l l)
  hasExponentials {l} = record
      { _↝′_ = λ B C → record
          { Cᴮ = B ↝ C
          ; eval = Eval
          ; curry′ = λ {A} F → record
              { arr = Curry F
              ; prop = Curry-correct {B = A} {B} {C} {F}
              ; unique = λ {g} eq → Cat≈.sym (Curry-unique eq)
              }
          }
      }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
module OlderBasicILP.Indirect.Translation where

open import OlderBasicILP.Indirect public

import OlderBasicILP.Indirect.Hilbert.Sequential as HS
import OlderBasicILP.Indirect.Hilbert.Nested as HN
import OlderBasicILP.Indirect.Gentzen as G

open HS using () renaming (_⊢×_ to HS⟨_⊢×_⟩ ; _⊢_ to HS⟨_⊢_⟩) public
open HN using () renaming (_⊢_ to HN⟨_⊢_⟩ ; _⊢⋆_ to HN⟨_⊢⋆_⟩) public
open G using  () renaming (_⊢_ to G⟨_⊢_⟩ ; _⊢⋆_ to G⟨_⊢⋆_⟩) public

-- Translation from sequential Hilbert-style to nested.

hs→hnᵀᵐ : HS.Tm → HN.Tm
hs→hnᵀᵐ TS = aux TS 0
  where
    aux : HS.Tm → ℕ → HN.Tm
    aux HS.NIL         zero    = {!!}
    aux (HS.VAR I TS)  zero    = HN.VAR I
    aux (HS.MP I J TS) zero    = HN.APP (aux TS I) (aux TS J)
    aux (HS.CI TS)     zero    = HN.CI
    aux (HS.CK TS)     zero    = HN.CK
    aux (HS.CS TS)     zero    = HN.CS
    aux (HS.NEC SS TS) zero    = HN.BOX (aux SS 0)
    aux (HS.CDIST TS)  zero    = HN.CDIST
    aux (HS.CUP TS)    zero    = HN.CUP
    aux (HS.CDOWN TS)  zero    = HN.CDOWN
    aux (HS.CPAIR TS)  zero    = HN.CPAIR
    aux (HS.CFST TS)   zero    = HN.CFST
    aux (HS.CSND TS)   zero    = HN.CSND
    aux (HS.UNIT TS)   zero    = HN.UNIT
    aux HS.NIL         (suc K) = {!!}
    aux (HS.VAR I TS)  (suc K) = aux TS K
    aux (HS.MP I J TS) (suc K) = aux TS K
    aux (HS.CI TS)     (suc K) = aux TS K
    aux (HS.CK TS)     (suc K) = aux TS K
    aux (HS.CS TS)     (suc K) = aux TS K
    aux (HS.NEC SS TS) (suc K) = aux TS K
    aux (HS.CDIST TS)  (suc K) = aux TS K
    aux (HS.CUP TS)    (suc K) = aux TS K
    aux (HS.CDOWN TS)  (suc K) = aux TS K
    aux (HS.CPAIR TS)  (suc K) = aux TS K
    aux (HS.CFST TS)   (suc K) = aux TS K
    aux (HS.CSND TS)   (suc K) = aux TS K
    aux (HS.UNIT TS)   (suc K) = aux TS K

hs→hnᵀʸ : Ty HS.Tm → Ty HN.Tm
hs→hnᵀʸ (α P)   = α P
hs→hnᵀʸ (A ▻ B) = hs→hnᵀʸ A ▻ hs→hnᵀʸ B
hs→hnᵀʸ (T ⦂ A) = hs→hnᵀᵐ T ⦂ hs→hnᵀʸ A
hs→hnᵀʸ (A ∧ B) = hs→hnᵀʸ A ∧ hs→hnᵀʸ B
hs→hnᵀʸ ⊤      = ⊤

hs→hnᵀʸ⋆ : Cx (Ty HS.Tm) → Cx (Ty HN.Tm)
hs→hnᵀʸ⋆ ∅       = ∅
hs→hnᵀʸ⋆ (Γ , A) = hs→hnᵀʸ⋆ Γ , hs→hnᵀʸ A

hs→hnᴵˣ : ∀ {A Γ} → A ∈ Γ → hs→hnᵀʸ A ∈ hs→hnᵀʸ⋆ Γ
hs→hnᴵˣ top     = top
hs→hnᴵˣ (pop i) = pop (hs→hnᴵˣ i)

hs→hn : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → HN⟨ hs→hnᵀʸ⋆ Γ ⊢ hs→hnᵀʸ A ⟩
hs→hn (Ξ , ts) = aux ts top
  where
    aux : ∀ {A Γ Ξ} → HS⟨ Γ ⊢× Ξ ⟩ → A ∈ Ξ → HN⟨ hs→hnᵀʸ⋆ Γ ⊢ hs→hnᵀʸ A ⟩
    aux (HS.var i ts)  top     = HN.var (hs→hnᴵˣ i)
    aux (HS.mp i j ts) top     = HN.app (aux ts i) (aux ts j)
    aux (HS.ci ts)     top     = HN.ci
    aux (HS.ck ts)     top     = HN.ck
    aux (HS.cs ts)     top     = HN.cs
    aux (HS.nec ss ts) top     = {!HN.box (aux ss top)!}
    aux (HS.cdist ts)  top     = {!HN.cdist!}
    aux (HS.cup ts)    top     = {!HN.cup!}
    aux (HS.cdown ts)  top     = HN.cdown
    aux (HS.cpair ts)  top     = HN.cpair
    aux (HS.cfst ts)   top     = HN.cfst
    aux (HS.csnd ts)   top     = HN.csnd
    aux (HS.unit ts)   top     = HN.unit
    aux (HS.var i ts)  (pop k) = aux ts k
    aux (HS.mp i j ts) (pop k) = aux ts k
    aux (HS.ci ts)     (pop k) = aux ts k
    aux (HS.ck ts)     (pop k) = aux ts k
    aux (HS.cs ts)     (pop k) = aux ts k
    aux (HS.nec ss ts) (pop k) = aux ts k
    aux (HS.cdist ts)  (pop k) = aux ts k
    aux (HS.cup ts)    (pop k) = aux ts k
    aux (HS.cdown ts)  (pop k) = aux ts k
    aux (HS.cpair ts)  (pop k) = aux ts k
    aux (HS.cfst ts)   (pop k) = aux ts k
    aux (HS.csnd ts)   (pop k) = aux ts k
    aux (HS.unit ts)   (pop k) = aux ts k

-- Translation from nested Hilbert-style to sequential.

hn→hsᵀᵐ : HN.Tm → HS.Tm
hn→hsᵀᵐ (HN.VAR I)   = HS.VAR I HS.NIL
hn→hsᵀᵐ (HN.APP T U) = HS.APP (hn→hsᵀᵐ T) (hn→hsᵀᵐ U)
hn→hsᵀᵐ HN.CI        = HS.CI HS.NIL
hn→hsᵀᵐ HN.CK        = HS.CK HS.NIL
hn→hsᵀᵐ HN.CS        = HS.CS HS.NIL
hn→hsᵀᵐ (HN.BOX T)   = HS.BOX (hn→hsᵀᵐ T)
hn→hsᵀᵐ HN.CDIST     = HS.CDIST HS.NIL
hn→hsᵀᵐ HN.CUP       = HS.CUP HS.NIL
hn→hsᵀᵐ HN.CDOWN     = HS.CDOWN HS.NIL
hn→hsᵀᵐ HN.CPAIR     = HS.CPAIR HS.NIL
hn→hsᵀᵐ HN.CFST      = HS.CFST HS.NIL
hn→hsᵀᵐ HN.CSND      = HS.CSND HS.NIL
hn→hsᵀᵐ HN.UNIT      = HS.UNIT HS.NIL

hn→hsᵀʸ : Ty HN.Tm → Ty HS.Tm
hn→hsᵀʸ (α P)   = α P
hn→hsᵀʸ (A ▻ B) = hn→hsᵀʸ A ▻ hn→hsᵀʸ B
hn→hsᵀʸ (T ⦂ A) = hn→hsᵀᵐ T ⦂ hn→hsᵀʸ A
hn→hsᵀʸ (A ∧ B) = hn→hsᵀʸ A ∧ hn→hsᵀʸ B
hn→hsᵀʸ ⊤      = ⊤

hn→hsᵀʸ⋆ : Cx (Ty HN.Tm) → Cx (Ty HS.Tm)
hn→hsᵀʸ⋆ ∅       = ∅
hn→hsᵀʸ⋆ (Γ , A) = hn→hsᵀʸ⋆ Γ , hn→hsᵀʸ A

hn→hsᴵˣ : ∀ {A Γ} → A ∈ Γ → hn→hsᵀʸ A ∈ hn→hsᵀʸ⋆ Γ
hn→hsᴵˣ top     = top
hn→hsᴵˣ (pop i) = pop (hn→hsᴵˣ i)

hn→hs : ∀ {A Γ} → HN⟨ Γ ⊢ A ⟩ → HS⟨ hn→hsᵀʸ⋆ Γ ⊢ hn→hsᵀʸ A ⟩
hn→hs (HN.var i)   = ∅ , HS.var (hn→hsᴵˣ i) HS.nil
hn→hs (HN.app t u) = HS.app (hn→hs t) (hn→hs u)
hn→hs HN.ci        = ∅ , HS.ci HS.nil
hn→hs HN.ck        = ∅ , HS.ck HS.nil
hn→hs HN.cs        = ∅ , HS.cs HS.nil
hn→hs (HN.box t)   = {!HS.box (hn→hs t)!}
hn→hs HN.cdist     = ∅ , HS.cdist HS.nil
hn→hs HN.cup       = ∅ , HS.cup HS.nil
hn→hs HN.cdown     = ∅ , HS.cdown HS.nil
hn→hs HN.cpair     = ∅ , HS.cpair HS.nil
hn→hs HN.cfst      = ∅ , HS.cfst HS.nil
hn→hs HN.csnd      = ∅ , HS.csnd HS.nil
hn→hs HN.unit      = ∅ , HS.unit HS.nil

-- Deduction theorem for sequential Hilbert-style.

hs→hn→hsᵀᵐ : ∀ {TS} → hn→hsᵀᵐ (hs→hnᵀᵐ TS) ≡ TS
hs→hn→hsᵀᵐ {HS.NIL}       = {!refl!}
hs→hn→hsᵀᵐ {HS.VAR I TS}  = cong² HS.VAR refl {!!}
hs→hn→hsᵀᵐ {HS.MP I J TS} = {!!}
hs→hn→hsᵀᵐ {HS.CI TS}     = {!!}
hs→hn→hsᵀᵐ {HS.CK TS}     = {!!}
hs→hn→hsᵀᵐ {HS.CS TS}     = {!!}
hs→hn→hsᵀᵐ {HS.NEC SS TS} = {!!}
hs→hn→hsᵀᵐ {HS.CDIST TS}  = {!!}
hs→hn→hsᵀᵐ {HS.CUP TS}    = {!!}
hs→hn→hsᵀᵐ {HS.CDOWN TS}  = {!!}
hs→hn→hsᵀᵐ {HS.CPAIR TS}  = {!!}
hs→hn→hsᵀᵐ {HS.CFST TS}   = {!!}
hs→hn→hsᵀᵐ {HS.CSND TS}   = {!!}
hs→hn→hsᵀᵐ {HS.UNIT TS}   = {!!}

hs→hn→hsᵀʸ : ∀ {A} → hn→hsᵀʸ (hs→hnᵀʸ A) ≡ A
hs→hn→hsᵀʸ {α P}   = refl
hs→hn→hsᵀʸ {A ▻ B} = cong² _▻_ hs→hn→hsᵀʸ hs→hn→hsᵀʸ
hs→hn→hsᵀʸ {T ⦂ A} = cong² _⦂_ hs→hn→hsᵀᵐ hs→hn→hsᵀʸ
hs→hn→hsᵀʸ {A ∧ B} = cong² _∧_ hs→hn→hsᵀʸ hs→hn→hsᵀʸ
hs→hn→hsᵀʸ {⊤}    = refl

-- hs-lam : ∀ {A B Γ} → HS⟨ Γ , A ⊢ B ⟩ → HS⟨ Γ ⊢ A ▻ B ⟩
-- hs-lam t = {!hn→hs (HN.lam (hs→hn t))!}
-- hn→hs ∘ HN.lam ∘ hs→hn

-- Translation from nested Hilbert-style to Gentzen-style.

hn→gᵀᵐ : HN.Tm → G.Tm
hn→gᵀᵐ (HN.VAR I)   = G.VAR I
hn→gᵀᵐ (HN.APP T U) = G.APP (hn→gᵀᵐ T) (hn→gᵀᵐ U)
hn→gᵀᵐ HN.CI        = G.CI
hn→gᵀᵐ HN.CK        = G.CK
hn→gᵀᵐ HN.CS        = G.CS
hn→gᵀᵐ (HN.BOX T)   = G.BOX (hn→gᵀᵐ T)
hn→gᵀᵐ HN.CDIST     = G.CDIST
hn→gᵀᵐ HN.CUP       = G.CUP
hn→gᵀᵐ HN.CDOWN     = G.CDOWN
hn→gᵀᵐ HN.CPAIR     = G.CPAIR
hn→gᵀᵐ HN.CFST      = G.CFST
hn→gᵀᵐ HN.CSND      = G.CSND
hn→gᵀᵐ HN.UNIT      = G.UNIT

hn→gᵀʸ : Ty HN.Tm → Ty G.Tm
hn→gᵀʸ (α P)   = α P
hn→gᵀʸ (A ▻ B) = hn→gᵀʸ A ▻ hn→gᵀʸ B
hn→gᵀʸ (T ⦂ A) = hn→gᵀᵐ T ⦂ hn→gᵀʸ A
hn→gᵀʸ (A ∧ B) = hn→gᵀʸ A ∧ hn→gᵀʸ B
hn→gᵀʸ ⊤      = ⊤

hn→gᵀʸ⋆ : Cx (Ty HN.Tm) → Cx (Ty G.Tm)
hn→gᵀʸ⋆ ∅       = ∅
hn→gᵀʸ⋆ (Γ , A) = hn→gᵀʸ⋆ Γ , hn→gᵀʸ A

hn→gᴵˣ : ∀ {A Γ} → A ∈ Γ → hn→gᵀʸ A ∈ hn→gᵀʸ⋆ Γ
hn→gᴵˣ top     = top
hn→gᴵˣ (pop i) = pop (hn→gᴵˣ i)

hn→g : ∀ {A Γ} → HN⟨ Γ ⊢ A ⟩ → G⟨ hn→gᵀʸ⋆ Γ ⊢ hn→gᵀʸ A ⟩
hn→g (HN.var i)   = G.var (hn→gᴵˣ i)
hn→g (HN.app t u) = G.app (hn→g t) (hn→g u)
hn→g HN.ci        = G.ci
hn→g HN.ck        = G.ck
hn→g HN.cs        = G.cs
hn→g (HN.box t)   = {!G.box (hn→g t)!}
hn→g HN.cdist     = {!G.cdist!}
hn→g HN.cup       = {!G.cup!}
hn→g HN.cdown     = G.cdown
hn→g HN.cpair     = G.cpair
hn→g HN.cfst      = G.cfst
hn→g HN.csnd      = G.csnd
hn→g HN.unit      = G.unit

-- Translation from sequential Hilbert-style to Gentzen-style.

hs→gᵀʸ : Ty HS.Tm → Ty G.Tm
hs→gᵀʸ = hn→gᵀʸ ∘ hs→hnᵀʸ

hs→gᵀʸ⋆ : Cx (Ty HS.Tm) → Cx (Ty G.Tm)
hs→gᵀʸ⋆ = hn→gᵀʸ⋆ ∘ hs→hnᵀʸ⋆

hs→g : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → G⟨ hs→gᵀʸ⋆ Γ ⊢ hs→gᵀʸ A ⟩
hs→g = hn→g ∘ hs→hn

-- Translation from Gentzen-style to Hilbert-style.

mutual
  g→hnᵀᵐ : G.Tm → HN.Tm
  g→hnᵀᵐ (G.VAR I)         = HN.VAR I
  g→hnᵀᵐ (G.LAM T)         = HN.LAM (g→hnᵀᵐ T)
  g→hnᵀᵐ (G.APP T U)       = HN.APP (g→hnᵀᵐ T) (g→hnᵀᵐ U)
  g→hnᵀᵐ (G.MULTIBOX TS U) = HN.MULTIBOX (g→hnᵀᵐ⋆ TS) (g→hnᵀᵐ U)
  g→hnᵀᵐ (G.DOWN T)        = HN.DOWN (g→hnᵀᵐ T)
  g→hnᵀᵐ (G.PAIR T U)      = HN.PAIR (g→hnᵀᵐ T) (g→hnᵀᵐ U)
  g→hnᵀᵐ (G.FST T)         = HN.FST (g→hnᵀᵐ T)
  g→hnᵀᵐ (G.SND T)         = HN.SND (g→hnᵀᵐ T)
  g→hnᵀᵐ G.UNIT            = HN.UNIT

  g→hnᵀᵐ⋆ : Cx G.Tm → Cx HN.Tm
  g→hnᵀᵐ⋆ ∅        = ∅
  g→hnᵀᵐ⋆ (TS , T) = g→hnᵀᵐ⋆ TS , g→hnᵀᵐ T

g→hnᵀʸ : Ty G.Tm → Ty HN.Tm
g→hnᵀʸ (α P)   = α P
g→hnᵀʸ (A ▻ B) = g→hnᵀʸ A ▻ g→hnᵀʸ B
g→hnᵀʸ (T ⦂ A) = g→hnᵀᵐ T ⦂ g→hnᵀʸ A
g→hnᵀʸ (A ∧ B) = g→hnᵀʸ A ∧ g→hnᵀʸ B
g→hnᵀʸ ⊤      = ⊤

g→hnᵀʸ⋆ : Cx (Ty G.Tm) → Cx (Ty HN.Tm)
g→hnᵀʸ⋆ ∅       = ∅
g→hnᵀʸ⋆ (Γ , A) = g→hnᵀʸ⋆ Γ , g→hnᵀʸ A

g→hnᴵˣ : ∀ {A Γ} → A ∈ Γ → g→hnᵀʸ A ∈ g→hnᵀʸ⋆ Γ
g→hnᴵˣ top     = top
g→hnᴵˣ (pop i) = pop (g→hnᴵˣ i)

mutual
  g→hn : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → HN⟨ g→hnᵀʸ⋆ Γ ⊢ g→hnᵀʸ A ⟩
  g→hn (G.var i)         = HN.var (g→hnᴵˣ i)
  g→hn (G.lam t)         = HN.lam (g→hn t)
  g→hn (G.app t u)       = HN.app (g→hn t) (g→hn u)
  g→hn (G.multibox ts u) = {!HN.multibox (g→hn⋆ ts) (g→hn u)!}
  g→hn (G.down t)        = HN.down (g→hn t)
  g→hn (G.pair t u)      = HN.pair (g→hn t) (g→hn u)
  g→hn (G.fst t)         = HN.fst (g→hn t)
  g→hn (G.snd t)         = HN.snd (g→hn t)
  g→hn G.unit            = HN.unit

  g→hn⋆ : ∀ {Ξ Γ} → G⟨ Γ ⊢⋆ Ξ ⟩ → HN⟨ g→hnᵀʸ⋆ Γ ⊢⋆ g→hnᵀʸ⋆ Ξ ⟩
  g→hn⋆ {∅}     ∙        = ∙
  g→hn⋆ {Ξ , A} (ts , t) = g→hn⋆ ts , g→hn t

-- Translation from Gentzen-style to sequential Hilbert-style.

g→hsᵀʸ : Ty G.Tm → Ty HS.Tm
g→hsᵀʸ = hn→hsᵀʸ ∘ g→hnᵀʸ

g→hsᵀʸ⋆ : Cx (Ty G.Tm) → Cx (Ty HS.Tm)
g→hsᵀʸ⋆ = hn→hsᵀʸ⋆ ∘ g→hnᵀʸ⋆

g→hs : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → HS⟨ g→hsᵀʸ⋆ Γ ⊢ g→hsᵀʸ A ⟩
g→hs = hn→hs ∘ g→hn


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

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

test₁ : (A : Set) (x y : A) (z : Nat) → x ≡ y → x ≅ (suc z) → y ≅ 1 → Nat
test₁ A (suc z) (suc zero) .z refl refl refl = {!!}

test₂ : (A : Set) (x y : A) (z : Nat) → x ≡ y → x ≅ 1 → y ≅ (suc z) → Nat
test₂ A (suc zero) (suc z) .z refl refl refl = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda