text:
{-# OPTIONS --allow-unsolved-metas #-}
module Formula where

module _ where

  open import VariableName
  open import PredicateName
  open import Term

  data Formula : Set
   where
    atomic : PredicateName → Terms → Formula
    logical : Formula →
              Formula →
              Formula
    quantified : VariableName → Formula → Formula

module _ where

  open import OscarPrelude

  formulaAtomic-inj₁ : ∀ {𝑃₁ τs₁ 𝑃₂ τs₂} → atomic 𝑃₁ τs₁ ≡ atomic 𝑃₂ τs₂ → 𝑃₁ ≡ 𝑃₂
  formulaAtomic-inj₁ refl = refl

  formulaAtomic-inj₂ : ∀ {𝑃₁ τs₁ 𝑃₂ τs₂} → atomic 𝑃₁ τs₁ ≡ atomic 𝑃₂ τs₂ → τs₁ ≡ τs₂
  formulaAtomic-inj₂ refl = refl

  formulaLogical-inj₁ : ∀ {φ₁₁ φ₁₂ φ₂₁ φ₂₂} → logical φ₁₁ φ₁₂ ≡ logical φ₂₁ φ₂₂ → φ₁₁ ≡ φ₂₁
  formulaLogical-inj₁ refl = refl

  formulaLogical-inj₂ : ∀ {φ₁₁ φ₁₂ φ₂₁ φ₂₂} → logical φ₁₁ φ₁₂ ≡ logical φ₂₁ φ₂₂ → φ₁₂ ≡ φ₂₂
  formulaLogical-inj₂ refl = refl

  formulaQuantified-inj₁ : ∀ {𝑥₁ φ₁ 𝑥₂ φ₂} → quantified 𝑥₁ φ₁ ≡ quantified 𝑥₂ φ₂ → 𝑥₁ ≡ 𝑥₂
  formulaQuantified-inj₁ refl = refl

  formulaQuantified-inj₂ : ∀ {𝑥₁ φ₁ 𝑥₂ φ₂} → quantified 𝑥₁ φ₁ ≡ quantified 𝑥₂ φ₂ → φ₁ ≡ φ₂
  formulaQuantified-inj₂ refl = refl

  instance EqFormula : Eq Formula
  Eq._==_ EqFormula (atomic 𝑃₁ τs₁)
                    (atomic 𝑃₂ τs₂)
                    = decEq₂ formulaAtomic-inj₁
                             formulaAtomic-inj₂
                             (𝑃₁ ≟ 𝑃₂)
                             (τs₁ ≟ τs₂)
  Eq._==_ EqFormula (logical φ₁₁ φ₁₂)
                    (logical φ₂₁ φ₂₂)
                    = decEq₂ formulaLogical-inj₁ formulaLogical-inj₂ (φ₁₁ ≟ φ₂₁) (φ₁₂ ≟ φ₂₂)
  Eq._==_ EqFormula (quantified 𝑥₁ φ₁) (quantified 𝑥₂ φ₂) = decEq₂ formulaQuantified-inj₁ formulaQuantified-inj₂ (𝑥₁ ≟ 𝑥₂) (φ₁ ≟ φ₂)
  Eq._==_ EqFormula (atomic _ _) (logical _ _) = no λ ()
  Eq._==_ EqFormula (atomic _ _) (quantified _ _) = no λ ()
  Eq._==_ EqFormula (logical _ _) (atomic _ _) = no λ ()
  Eq._==_ EqFormula (logical _ _) (quantified _ _) = no λ ()
  Eq._==_ EqFormula (quantified _ _) (atomic _ _) = no λ ()
  Eq._==_ EqFormula (quantified _ _) (logical _ _) = no λ ()

module _ where

  open import PredicateName
  open import Term

  𝑃[_♭_] : PredicateName → Terms → Formula
  𝑃[_♭_] = atomic

  {-# DISPLAY atomic = 𝑃[_♭_] #-}

module _ where

  open import HasNeitherNor

  instance HasNeitherNorFormula : HasNeitherNor Formula
  HasNeitherNor._⊗_ HasNeitherNorFormula = logical

  {-# DISPLAY logical = _⊗_ #-}

module _ where

  open import HasNeitherNor
  open import HasNegation

  instance HasNegationFormula : HasNegation Formula
  HasNegation.~ HasNegationFormula φ = φ ⊗ φ

module _ where

  open import OscarPrelude
  open import Term
  open import HasSatisfaction
  open import Interpretation
  open import Vector
  open import InterpretationEqualityExceptAtVariableName
  open import Elements
  open import TruthValue

  instance HasSatisfactionFormula : HasSatisfaction Formula
  HasSatisfaction._⊨_ HasSatisfactionFormula I (atomic 𝑃 τs) = 𝑃⟦ I ⟧ 𝑃 ⟨ ⟨ τ⟦ I ⟧ <$> vector (terms τs) ⟩ ⟩ ≡ ⟨ true ⟩
  HasSatisfaction._⊨_ HasSatisfactionFormula I (logical φ₁ φ₂) = ¬ I ⊨ φ₁ × ¬ I ⊨ φ₂
  HasSatisfaction._⊨_ HasSatisfactionFormula I (quantified 𝑥 φ) = (𝓘 : Interpretation) → 𝓘 ≞ I / 𝑥 → 𝓘 ⊨ φ

  instance HasDecidableSatisfactionFormula : HasDecidableSatisfaction Formula
  HasDecidableSatisfaction._⊨?_ HasDecidableSatisfactionFormula I (atomic 𝑃 τs) = {!!}
  HasDecidableSatisfaction._⊨?_ HasDecidableSatisfactionFormula I (logical φ₁ φ₂) = {!!}
  HasDecidableSatisfaction._⊨?_ HasDecidableSatisfactionFormula I (quantified 𝑥 φ) = {!!}

  instance HasDecidableValidationFormula : HasDecidableValidation Formula
  HasDecidableValidation.⊨?_ HasDecidableValidationFormula (atomic 𝑃 τs) = {!!}
  HasDecidableValidation.⊨?_ HasDecidableValidationFormula (logical φ₁ φ₂) = {!!}
  HasDecidableValidation.⊨?_ HasDecidableValidationFormula (quantified 𝑥 φ) = {!!}

module _ where

  open import OscarPrelude
  open import Relation.Binary.Core
  --open import PredicateName
  open import VariableName
  open import Arity
  open import Term
  open import Vector

  mutual

    notationalVariantTerm* : (VariableName → Maybe VariableName) → Term → Term → Set
    notationalVariantTerm* v (variable 𝑥₁) (variable 𝑥₂) = maybe 𝑥₁ id (v 𝑥₁) ≡ 𝑥₂
    notationalVariantTerm* v (function 𝑓₁ τs₁) (function 𝑓₂ τs₂) = 𝑓₁ ≡ 𝑓₂ × notationalVariantTerms* v τs₁ τs₂
    notationalVariantTerm* v (variable x) (function x₁ x₂) = ⊥
    notationalVariantTerm* v (function x x₁) (variable x₂) = ⊥

    notationalVariantTerms* : (VariableName → Maybe VariableName) → Terms → Terms → Set
    notationalVariantTerms* v (⟨_⟩ {a₁} terms₁) (⟨_⟩ {a₂} terms₂) with a₁ ≟ a₂
    notationalVariantTerms* v (⟨_⟩ {⟨ .0 ⟩} ⟨ [] ⟩) (⟨_⟩ {.(⟨ 0 ⟩)} ⟨ [] ⟩) | yes refl = ⊤
    notationalVariantTerms* v (⟨_⟩ {⟨ .(suc _) ⟩} ⟨ x ∷ vector₁ ⟩) (⟨_⟩ {.(⟨ suc _ ⟩)} ⟨ x₁ ∷ vector₂ ⟩) | yes refl = notationalVariantTerm* v x x₁ × notationalVariantTerms* v ⟨ ⟨ vector₁ ⟩ ⟩ ⟨ ⟨ vector₂ ⟩ ⟩
    … | no neq = ⊥

  mutual

    data Term⟦_/_≈_⟧ (v : VariableName → Maybe VariableName) : Term → Term → Set where
      variable : ∀ 𝑥₁ 𝑥₂ → maybe 𝑥₁ id (v 𝑥₁) ≡ 𝑥₂ → Term⟦ v / variable 𝑥₁ ≈ variable 𝑥₂ ⟧
      function : ∀ 𝑓 τs₁ τs₂ → Terms⟦ v / τs₁ ≈ τs₂ ⟧ → Term⟦ v / function 𝑓 τs₁ ≈ function 𝑓 τs₂ ⟧

    data Terms⟦_/_≈_⟧ (v : VariableName → Maybe VariableName) : Terms → Terms → Set where
      [] : Terms⟦ v / ⟨ ⟨ [] ⟩ ⟩ ≈ ⟨ ⟨ [] ⟩ ⟩ ⟧
      _∷_ : ∀ τ₁ τ₂ → Term⟦ v / τ₁ ≈ τ₂ ⟧ → ∀ τs₁ τs₂ → Terms⟦ v / τs₁ ≈ τs₂ ⟧ → Terms⟦ v / ⟨ ⟨ τ₁ ∷ vector (terms τs₁) ⟩ ⟩ ≈ ⟨ ⟨ τ₂ ∷ vector (terms τs₂) ⟩ ⟩ ⟧

  notationalVariantFormula* : (VariableName → Maybe VariableName) → Formula → Formula → Set
  notationalVariantFormula* v (atomic x x₁) (atomic x₂ x₃) = x ≡ x₂ × notationalVariantTerms* v x₁ x₃
  notationalVariantFormula* v (logical φ₁ φ₂) (logical φ₃ φ₄) = notationalVariantFormula* v φ₁ φ₃ × notationalVariantFormula* v φ₂ φ₄
  notationalVariantFormula* v (quantified x φ₁) (quantified x₁ φ₂) = notationalVariantFormula* (λ {v' → ifYes v' ≟ x then just x₁ else v v'}) φ₁ φ₂
  notationalVariantFormula* v (logical φ₁ φ₂) (atomic x x₁) = ⊥
  notationalVariantFormula* v (atomic x x₁) (logical φ₂ φ₃) = ⊥
  notationalVariantFormula* v (atomic x x₁) (quantified x₂ φ₂) = ⊥
  notationalVariantFormula* v (logical φ₁ φ₂) (quantified x φ₃) = ⊥
  notationalVariantFormula* v (quantified x φ₁) (atomic x₁ x₂) = ⊥
  notationalVariantFormula* v (quantified x φ₁) (logical φ₂ φ₃) = ⊥

  notationalVariantFormula : Formula → Formula → Set
  notationalVariantFormula φ₁ φ₂ = notationalVariantFormula* (const nothing) φ₁ φ₂

  private

    refl-notationalVariantTerms* : ∀ x₁ → notationalVariantTerms* (λ x₂ → nothing) ⟨ terms x₁ ⟩ ⟨ terms x₁ ⟩
    refl-notationalVariantTerms* (⟨_⟩ {arity = ⟨ .0 ⟩} ⟨ [] ⟩) = {!!}
    refl-notationalVariantTerms* (⟨_⟩ {arity = ⟨ .(suc _) ⟩} ⟨ _∷_ {n = n} x vector₁ ⟩) = {!!}
    {-
    refl-notationalVariantTerms* ⟨ ⟨ [] ⟩ ⟩ = tt
    refl-notationalVariantTerms* (⟨_⟩ {nx} ⟨ x ∷ vector₁ ⟩) = {!!}
    -}

    refl-notationalVariantFormula : (φ : Formula) → notationalVariantFormula φ φ
    refl-notationalVariantFormula (atomic x x₁) = {!!}
    refl-notationalVariantFormula (logical φ φ₁) = {!!}
    refl-notationalVariantFormula (quantified x φ) = {!!}

  isEquivalenceNotationalVariantFormula : IsEquivalence notationalVariantFormula
  isEquivalenceNotationalVariantFormula =
    record
    { refl = {!!} -- λ { {atomic _ _} → refl , {!!} ; {logical x x₁} → {!!} ; {quantified x x₁} → {!!} }
    ; sym = {!!}
    ; trans = {!!} }

  data Formula⟦_/_≈_⟧ (v : VariableName → Maybe VariableName) : Formula → Formula → Set where
    atomic : ∀ 𝑃 τs₁ τs₂ → Terms⟦ v / τs₁ ≈ τs₂ ⟧ → Formula⟦ v / atomic 𝑃 τs₁ ≈ atomic 𝑃 τs₂ ⟧
    logical : ∀ φ₁₁ φ₁₂ φ₂₁ φ₂₂ → Formula⟦ v / φ₁₁ ≈ φ₂₁ ⟧ → Formula⟦ v / φ₁₂ ≈ φ₂₂ ⟧ → Formula⟦ v / logical φ₁₁ φ₁₂ ≈ logical φ₂₁ φ₂₂ ⟧
    quantified : ∀ 𝑥₁ 𝑥₂ φ₁ φ₂ → Formula⟦ (λ {v' → ifYes v' ≟ 𝑥₁ then just 𝑥₂ else v v'}) / φ₁ ≈ φ₂ ⟧ → Formula⟦ v / quantified 𝑥₁ φ₁ ≈ quantified 𝑥₂ φ₂ ⟧

  data F⟦_NotationalVariant_⟧ : Formula → Formula → Set where
    basic : ∀ φ₁ φ₂ → Formula⟦ const nothing / φ₁ ≈ φ₂ ⟧ → F⟦ φ₁ NotationalVariant φ₂ ⟧

  private

    mutual
      refl-notVarTerms : ∀ x₁ → Terms⟦ const nothing / x₁ ≈ x₁ ⟧
      refl-notVarTerms ⟨ ⟨ [] ⟩ ⟩ = []
      refl-notVarTerms ⟨ ⟨ x ∷ vector₁ ⟩ ⟩ = (x ∷ x) (refl-notVarTerm x) ⟨ ⟨ vector₁ ⟩ ⟩ ⟨ ⟨ vector₁ ⟩ ⟩ (refl-notVarTerms ⟨ ⟨ vector₁ ⟩ ⟩)

      refl-notVarTerm : ∀ x₁ → Term⟦ const nothing / x₁ ≈ x₁ ⟧
      refl-notVarTerm (variable x) = variable x x refl
      refl-notVarTerm (function x x₁) = function x x₁ x₁ (refl-notVarTerms x₁)

    refl-notationalVariant' : (φ : Formula) → F⟦ φ NotationalVariant φ ⟧
    refl-notationalVariant' (atomic x x₁) = basic 𝑃[ x ♭ x₁ ] 𝑃[ x ♭ x₁ ] (atomic x x₁ x₁ (refl-notVarTerms x₁))
    refl-notationalVariant' (logical φ φ₁) = basic (logical φ φ₁) (logical φ φ₁) (logical φ φ₁ φ φ₁ {!!} {!!})
    refl-notationalVariant' (quantified x φ) = basic (quantified x φ) (quantified x φ) (quantified x x φ φ {!!})

  isEquivalenceNotationalVariant' : IsEquivalence F⟦_NotationalVariant_⟧
  isEquivalenceNotationalVariant' =
    record
    { refl = {!!} -- λ { {atomic _ _} → refl , {!!} ; {logical x x₁} → {!!} ; {quantified x x₁} → {!!} }
    ; sym = {!!}
    ; trans = {!!} }

module _ where

  open import HasSubstantiveDischarge
{-
  postulate
    instance cs : CanonicalSubstitution Formula
    instance hpu : HasPairUnification Formula (CanonicalSubstitution.S cs)
-}
  instance HasSubstantiveDischargeFormulaFormula : HasSubstantiveDischarge Formula
  HasSubstantiveDischarge.hasNegation HasSubstantiveDischargeFormulaFormula = {!!}
  --HasSubstantiveDischarge._o≽o_ HasSubstantiveDischargeFormulaFormula φ₁ φ₂ = {!!} -- ∃ λ υ → υ Unifies φ₁ and φ₂
  HasSubstantiveDischarge.≽-reflexive HasSubstantiveDischargeFormulaFormula = {!!}
  HasSubstantiveDischarge.≽-consistent HasSubstantiveDischargeFormulaFormula = {!!}
  HasSubstantiveDischarge.≽-contrapositive HasSubstantiveDischargeFormulaFormula = {!!}

  instance HasDecidableSubstantiveDischargeFormulaFormula : HasDecidableSubstantiveDischarge Formula
  HasDecidableSubstantiveDischarge.hasSubstantiveDischarge HasDecidableSubstantiveDischargeFormulaFormula = {!!}
  HasDecidableSubstantiveDischarge._≽?_ HasDecidableSubstantiveDischargeFormulaFormula = {!!}

module _ where

  open import VariableName

  ∀[_♭_] : VariableName → Formula → Formula
  ∀[_♭_] = quantified

  {-# DISPLAY Formula.quantified = ∀[_♭_] #-}

module _ where

  open import HasNegation
  open import HasNeitherNor

  _∧_ : Formula → Formula → Formula
  φ₁ ∧ φ₂ = ~ φ₁ ⊗ ~ φ₂

  _∨_ : Formula → Formula → Formula
  φ₁ ∨ φ₂ = ~ (φ₁ ⊗ φ₂)

  _⊃_ : Formula → Formula → Formula
  φ₁ ⊃ φ₂ = ~ φ₁ ∨ φ₂

  _⟷_ : Formula → Formula → Formula
  φ₁ ⟷ φ₂ = (φ₁ ⊗ (φ₂ ⊗ φ₂)) ⊗ ((φ₁ ⊗ φ₁) ⊗ φ₂) -- TODO check that this is logically equivalent to the more verbose, (φ₁ ⊃ φ₂) ∧ (φ₂ ⊃ φ₁)


text:
-- Andreas, 2018-03-19, issue #2971, reported by Ulf
-- Splitting on result should give proper error
-- when record type is weak, i.e. lacks projections.

{-# OPTIONS --no-irrelevant-projections #-}

-- {-# OPTIONS -v tc.cover:20 #-}

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

record Five : Set where
  field
    five : Nat
    .prf : five ≡ 5  -- No corresponding projection!

best-number : Five
best-number = {!!} -- C-c C-c (on result)

-- Error WAS:
-- Panic: Unbound name: NoIrrProj.Five.prf
-- [0,2,10]@5465979233139828506
-- when checking that the expression ? has type Five

-- Should give proper error message.

-- Cannot split on result here, because record has irrelevant fields,
-- but no corresponding projections
-- when checking that the expression ? has type Five

-- Testing similar errors:

not-record : Set
not-record = {!!}

-- Cannot split on result here, because target type  Set  is not a record type
-- when checking that the expression ? has type Set

ext: agda

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

module container.m where

open import container.m.coalgebra public
open import container.m.from-nat public
open import container.m.core public
open import container.m.extensionality public
open import container.m.level public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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 Haskell.Modules.RWS
open import Haskell.Modules.RWS.Lens
open import Haskell.Modules.RWS.RustAnyHow
open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.TestUtils.MockStorage as MockStorage
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.LBFT
open import Optics.All
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                   using (String)

module LibraBFT.Impl.Consensus.PersistentLivenessStorage where

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

obmUpdateM
  : ( PersistentLivenessStorage → LBFT (Either ErrLog PersistentLivenessStorage) )
  → LBFT (Either ErrLog Unit)

obmUpdateE
  : BlockStore
  → ( PersistentLivenessStorage
       → Either ErrLog PersistentLivenessStorage )
  -> Either ErrLog BlockStore

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

saveTreeM : List Block → List QuorumCert → LBFT (Either ErrLog Unit)
saveTreeM blocks qcs =
  obmUpdateM (MockStorage.saveTreeM blocks qcs)

saveTreeE : BlockStore → List Block → List QuorumCert → Either ErrLog BlockStore
saveTreeE bs blocks qcs =
  obmUpdateE bs (MockStorage.saveTreeE blocks qcs)

pruneTreeM : List HashValue → LBFT (Either ErrLog Unit)
pruneTreeM =
  obmUpdateM ∘ MockStorage.pruneTreeM

saveVoteM : Vote → LBFT (Either ErrLog Unit)
saveVoteM =
  obmUpdateM ∘ MockStorage.saveStateM

startM : LBFT (Either ErrLog RecoveryData)
startM =
  use (lBlockStore ∙ bsStorage) >>= λ s → pure (MockStorage.start s) ∙^∙ withErrCtx (here' [])
 where
  here' : List String → List String
  here' t = "PersistentLivenessStorage" ∷ "startM" ∷ t

saveHighestTimeoutCertM : TimeoutCertificate → LBFT (Either ErrLog Unit)
saveHighestTimeoutCertM =
  obmUpdateM ∘ MockStorage.saveHighestTimeoutCertificateM

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

obmUpdateM f = do
  s <- use (lBlockStore ∙ bsStorage)
  f s ∙?∙ λ s' → do lBlockStore ∙ bsStorage ∙= s'; ok unit

obmUpdateE bs f = do
  let s = bs ^∙ bsStorage
  s'    ← f s
  pure (bs & bsStorage ∙~ s')


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.String
open import Agda.Builtin.List
open import Agda.Builtin.Unit

impNames : Term → List String
impNames (pi (arg (arg-info hidden _) _) (abs x b)) = x ∷ impNames b
impNames _ = []

macro
  implicits : Name → Term → TC ⊤
  implicits x hole = do
    t ← getType x
    i ← quoteTC (impNames t)
    unify hole i

variable
  A : Set₁
  x : A

postulate
  f : (B : Set) → B ≡ B → Set

g : f _ x ≡ f _ x
g = refl

_ : implicits g ≡ "x.A.1" ∷ "x" ∷ []
_ = refl

postulate
  F : Set → Set₁
  P : {x : Set} → F x → Set
  Q : {x : Set₁} → x → Set
  p : P x
  q : Q x

_ : implicits p ≡ "x.A.1" ∷ "x" ∷ []
_ = refl

_ : implicits q ≡ "x.A" ∷ "x" ∷ []
_ = refl

fails : (A : Set) (f : F A) → P f
fails A f = p {x = f}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module BasicIPC.Metatheory.GentzenSpinalNormalForm-HereditarySubstitution where

open import BasicIPC.Syntax.GentzenSpinalNormalForm public

-- Hereditary substitution and reduction.

mutual
  [_≔_]ⁿᶠ_ : ∀ {A B Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ⁿᶠ A → Γ ⊢ⁿᶠ B → Γ ∖ i ⊢ⁿᶠ B
  [ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ j  xs) with i ≟∈ j
  [ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ .i xs) | same   = reduce s ([ i ≔ s ]ˢᵖ xs)
  [ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ ._ xs) | diff j = neⁿᶠ (spⁿᵉ j ([ i ≔ s ]ˢᵖ xs))
  [ i ≔ s ]ⁿᶠ lamⁿᶠ t           = lamⁿᶠ ([ pop i ≔ mono⊢ⁿᶠ weak⊆ s ]ⁿᶠ t)
  [ i ≔ s ]ⁿᶠ pairⁿᶠ t u        = pairⁿᶠ ([ i ≔ s ]ⁿᶠ t) ([ i ≔ s ]ⁿᶠ u)
  [ i ≔ s ]ⁿᶠ unitⁿᶠ            = unitⁿᶠ

  [_≔_]ˢᵖ_ : ∀ {A B C Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ⁿᶠ A → Γ ⊢ˢᵖ B ⦙ C → Γ ∖ i ⊢ˢᵖ B ⦙ C
  [ i ≔ s ]ˢᵖ nilˢᵖ      = nilˢᵖ
  [ i ≔ s ]ˢᵖ appˢᵖ xs u = appˢᵖ ([ i ≔ s ]ˢᵖ xs) ([ i ≔ s ]ⁿᶠ u)
  [ i ≔ s ]ˢᵖ fstˢᵖ xs   = fstˢᵖ ([ i ≔ s ]ˢᵖ xs)
  [ i ≔ s ]ˢᵖ sndˢᵖ xs   = sndˢᵖ ([ i ≔ s ]ˢᵖ xs)

  reduce : ∀ {A C Γ} → Γ ⊢ⁿᶠ A → Γ ⊢ˢᵖ A ⦙ C → Γ ⊢ⁿᶠ C
  reduce t            nilˢᵖ        = t
  reduce (lamⁿᶠ t)    (appˢᵖ xs u) = reduce ([ top ≔ u ]ⁿᶠ t) xs
  reduce (pairⁿᶠ t u) (fstˢᵖ xs)   = reduce t xs
  reduce (pairⁿᶠ t u) (sndˢᵖ xs)   = reduce u xs

-- Reduction-based normal forms.

appⁿᶠ : ∀ {A B Γ} → Γ ⊢ⁿᶠ A ▻ B → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᶠ B
appⁿᶠ t u = reduce t (appˢᵖ nilˢᵖ u)

fstⁿᶠ : ∀ {A B Γ} → Γ ⊢ⁿᶠ A ∧ B → Γ ⊢ⁿᶠ A
fstⁿᶠ t = reduce t (fstˢᵖ nilˢᵖ)

sndⁿᶠ : ∀ {A B Γ} → Γ ⊢ⁿᶠ A ∧ B → Γ ⊢ⁿᶠ B
sndⁿᶠ t = reduce t (sndˢᵖ nilˢᵖ)

-- Useful equipment for deriving neutrals.

≪appˢᵖ : ∀ {A B C Γ} → Γ ⊢ˢᵖ C ⦙ A ▻ B → Γ ⊢ⁿᶠ A → Γ ⊢ˢᵖ C ⦙ B
≪appˢᵖ nilˢᵖ        t = appˢᵖ nilˢᵖ t
≪appˢᵖ (appˢᵖ xs u) t = appˢᵖ (≪appˢᵖ xs t) u
≪appˢᵖ (fstˢᵖ xs)   t = fstˢᵖ (≪appˢᵖ xs t)
≪appˢᵖ (sndˢᵖ xs)   t = sndˢᵖ (≪appˢᵖ xs t)

≪fstˢᵖ : ∀ {A B C Γ} → Γ ⊢ˢᵖ C ⦙ A ∧ B → Γ ⊢ˢᵖ C ⦙ A
≪fstˢᵖ nilˢᵖ        = fstˢᵖ nilˢᵖ
≪fstˢᵖ (appˢᵖ xs u) = appˢᵖ (≪fstˢᵖ xs) u
≪fstˢᵖ (fstˢᵖ xs)   = fstˢᵖ (≪fstˢᵖ xs)
≪fstˢᵖ (sndˢᵖ xs)   = sndˢᵖ (≪fstˢᵖ xs)

≪sndˢᵖ : ∀ {A B C Γ} → Γ ⊢ˢᵖ C ⦙ A ∧ B → Γ ⊢ˢᵖ C ⦙ B
≪sndˢᵖ nilˢᵖ        = sndˢᵖ nilˢᵖ
≪sndˢᵖ (appˢᵖ xs u) = appˢᵖ (≪sndˢᵖ xs) u
≪sndˢᵖ (fstˢᵖ xs)   = fstˢᵖ (≪sndˢᵖ xs)
≪sndˢᵖ (sndˢᵖ xs)   = sndˢᵖ (≪sndˢᵖ xs)

-- Derived neutrals.

varⁿᵉ : ∀ {A Γ} → A ∈ Γ → Γ ⊢ⁿᵉ A
varⁿᵉ i = spⁿᵉ i nilˢᵖ

appⁿᵉ : ∀ {A B Γ} → Γ ⊢ⁿᵉ A ▻ B → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᵉ B
appⁿᵉ (spⁿᵉ i xs) t = spⁿᵉ i (≪appˢᵖ xs t)

fstⁿᵉ : ∀ {A B Γ} → Γ ⊢ⁿᵉ A ∧ B → Γ ⊢ⁿᵉ A
fstⁿᵉ (spⁿᵉ i xs) = spⁿᵉ i (≪fstˢᵖ xs)

sndⁿᵉ : ∀ {A B Γ} → Γ ⊢ⁿᵉ A ∧ B → Γ ⊢ⁿᵉ B
sndⁿᵉ (spⁿᵉ i xs) = spⁿᵉ i (≪sndˢᵖ xs)

-- Iterated expansion.

expand : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊢ⁿᶠ A
expand {α P}   t = neⁿᶠ t
expand {A ▻ B} t = lamⁿᶠ (expand (appⁿᵉ (mono⊢ⁿᵉ weak⊆ t) (expand (varⁿᵉ top))))
expand {A ∧ B} t = pairⁿᶠ (expand (fstⁿᵉ t)) (expand (sndⁿᵉ t))
expand {⊤}    t = unitⁿᶠ

-- Expansion-based normal forms.

varⁿᶠ : ∀ {A Γ} → A ∈ Γ → Γ ⊢ⁿᶠ A
varⁿᶠ i = expand (varⁿᵉ i)

-- Translation from simple terms to normal forms.

tm→nf : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ⁿᶠ A
tm→nf (var i)    = varⁿᶠ i
tm→nf (lam t)    = lamⁿᶠ (tm→nf t)
tm→nf (app t u)  = appⁿᶠ (tm→nf t) (tm→nf u)
tm→nf (pair t u) = pairⁿᶠ (tm→nf t) (tm→nf u)
tm→nf (fst t)    = fstⁿᶠ (tm→nf t)
tm→nf (snd t)    = sndⁿᶠ (tm→nf t)
tm→nf unit       = unitⁿᶠ

-- Normalisation by hereditary substitution.

norm : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ A
norm = nf→tm ∘ tm→nf

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --cubical --no-positivity-check --no-termination-check #-}

open import Prelude
open import Algebra
open import Algebra.Monus
open import Relation.Binary
open import Data.Maybe
open import Data.List using (List; _∷_; []; foldr)

module Control.Monad.HeapT
  {ℓ}
  (monoid : Monoid ℓ)
  (gmon : GradedMonad monoid ℓ ℓ)
  where

open Monoid monoid
open GradedMonad gmon

private
  variable
    w : 𝑆

infixr 5 _∷_
infixr 6 _⋊_

mutual
  record Root (A : Type ℓ) : Type ℓ where
    coinductive
    constructor _⋊_
    field
      weight : 𝑆
      step : 𝐹 weight (Branch A)

  data Node (A : Type ℓ) : Type ℓ where
    ⌊_⌋ : A → Node A
    ⌈_⌉ : Root A → Node A

  data Branch (A : Type ℓ) : Type ℓ where
    []  : Branch A
    _∷_ : Node A → 𝐹 ε (Branch A) → Branch A
open Root public

Heap : Type ℓ → Type ℓ
Heap A = 𝐹 ε (Branch A)

infixr 5 _++_
_++_ : 𝐹 w (Branch A) → 𝐹 ε (Branch A) → 𝐹 w (Branch A)
xs ++ ys =
  xs >>=ε λ  {  []       → ys
             ;  (x ∷ xs) → pure (x ∷ xs ++ ys) }

infixr 1 _>>=ᴺ_ _>>=ᴴ_
mutual
  _>>=ᴺ_ : Node A → (A → Heap B) → Heap B
  ⌊ x ⌋  >>=ᴺ f = f x
  ⌈ x ⌉  >>=ᴺ f = pure (⌈ weight x ⋊ (step x >>=ᴴ f) ⌉ ∷ pure [])

  _>>=ᴴ_ : 𝐹 w (Branch A) → (A → Heap B) → 𝐹 w (Branch B)
  xs >>=ᴴ f =
    xs >>=ε λ  {  []        → pure []
               ;  (x ∷ xs)  → (x >>=ᴺ f) ++ (xs >>=ᴴ f) }

pureᴴ : A → Heap A
pureᴴ x = pure (⌊ x ⌋ ∷ pure [])

liftᴴ : 𝐹 w A → Heap A
liftᴴ xs = pure (⌈ _ ⋊ map (λ x → ⌊ x ⌋ ∷ pure []) xs ⌉ ∷ pure [])

flatten : 𝐹 w (Branch A) → 𝐹 w (List A × List (Root A))
flatten xs =
  xs >>=ε λ  {  []            → pure ([] , [])
             ;  (⌊ x ⌋ ∷ xs)  → map (map₁ (x ∷_)) (flatten xs)
             ;  (⌈ x ⌉ ∷ xs)  → map (map₂ (x ∷_)) (flatten xs) }

module PopMin
  (_≤|≥_ : Total (λ x y → ∃ z × (y ≡ x ∙ z)))
  (decomp : ∀ {A B w₁ w₂ w₃} → 𝐹 (w₁ ∙ w₂) A → 𝐹 (w₁ ∙ w₃) B → 𝐹 w₁ (𝐹 w₂ A × 𝐹 w₃ B)) where

  _∪_ : Root A → Root A → Root A
  xs ∪ ys with weight xs ≤|≥ weight ys
  ... | inl (k , wʸ≡wˣ∙k) = weight xs ⋊ map (λ { (xs , ys) → ⌈ k ⋊ ys ⌉ ∷ xs }) (decomp (subst (flip 𝐹 _) (sym (∙ε _)) (step xs)) (subst (flip 𝐹 _) wʸ≡wˣ∙k (step ys)))
  ... | inr (k , wˣ≡wʸ∙k) = weight ys ⋊ map (λ { (ys , xs) → ⌈ k ⋊ xs ⌉ ∷ ys }) (decomp (subst (flip 𝐹 _) (sym (∙ε _)) (step ys)) (subst (flip 𝐹 _) wˣ≡wʸ∙k (step xs)))

  ⋃⁺ : Root A → List (Root A) → Root A
  ⋃⁺ x₁ []             = x₁
  ⋃⁺ x₁ (x₂ ∷ [])      = x₁ ∪ x₂
  ⋃⁺ x₁ (x₂ ∷ x₃ ∷ xs) = (x₁ ∪ x₂) ∪ ⋃⁺ x₃ xs

  ⋃ : List (Root A) → Maybe (Root A)
  ⋃ []       = nothing
  ⋃ (x ∷ xs) = just (⋃⁺ x xs)

  popMin : 𝐹 w (Branch A) → 𝐹 w (List A × Maybe (Root A))
  popMin = map (map₂ ⋃) ∘ flatten

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The min operator derived from an arbitrary total order
------------------------------------------------------------------------

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

open import Relation.Binary

module Algebra.Construct.NaturalChoice.Min
  {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂)
  where

open import Algebra
open import Data.Sum using (inj₁; inj₂; [_,_])
open import Data.Product using (_,_)
open import Function using (id)

open TotalOrder totalOrder renaming (Carrier to A)
open import Algebra.FunctionProperties _≈_
open import Algebra.Structures _≈_

----------------------------------------------------------------------------
-- Definition

infixl 7 _⊓_

_⊓_ : Op₂ A
x ⊓ y with total x y
... | inj₁ x≤y = x
... | inj₂ y≤x = y

----------------------------------------------------------------------------
-- Algebraic properties

⊓-sel : Selective _⊓_
⊓-sel x y with total x y
... | inj₁ x≤y = inj₁ Eq.refl
... | inj₂ y≤x = inj₂ Eq.refl

⊓-idem : Idempotent _⊓_
⊓-idem x with ⊓-sel x x
... | inj₁ x⊓x=x = x⊓x=x
... | inj₂ x⊓x=x = x⊓x=x

⊓-cong : Congruent₂ _⊓_
⊓-cong {w} {x} {y} {z} w≈x y≈z with total w y | total x z
... | inj₁ w≤y | inj₁ x≤z = w≈x
... | inj₁ w≤y | inj₂ z≤x = antisym (≤-respʳ-≈ y≈z w≤y) (≤-respʳ-≈ (Eq.sym w≈x) z≤x)
... | inj₂ y≤w | inj₁ x≤z = antisym (≤-respʳ-≈ w≈x y≤w) (≤-respʳ-≈ (Eq.sym y≈z) x≤z)
... | inj₂ y≤w | inj₂ z≤x = y≈z

⊓-comm : Commutative _⊓_
⊓-comm x y with total x y | total y x
... | inj₁ x≤y | inj₁ y≤x = antisym x≤y y≤x
... | inj₁ _   | inj₂ _   = Eq.refl
... | inj₂ _   | inj₁ _   = Eq.refl
... | inj₂ y≤x | inj₂ x≤y = antisym y≤x x≤y

⊓-assoc : Associative _⊓_
⊓-assoc x y z with total x y | total x z | total y z
⊓-assoc x y z | inj₁ x≤y | inj₁ x≤z | inj₁ y≤z with total x z | total x y
... | inj₁ x≤z₂ | inj₁ _    = Eq.refl
... | inj₁ x≤z₂ | inj₂ y≤x  = antisym x≤y y≤x
... | inj₂ z≤x  | inj₁ _    = antisym z≤x (trans x≤y y≤z)
... | inj₂ z≤x  | inj₂ y≤x  = antisym (trans z≤x x≤y) (trans y≤x x≤z)
⊓-assoc x y z | inj₁ x≤y | inj₁ x≤z | inj₂ z≤y with total x z
... | inj₁ _                = Eq.refl
... | inj₂ _                = Eq.refl
⊓-assoc x y z | inj₁ x≤y | inj₂ z≤x | inj₁ y≤z with total x z | total x y
... | inj₁ x≤z  | inj₁ _    = Eq.refl
... | inj₁ x≤z  | inj₂ y≤x  = antisym x≤y (trans y≤z z≤x)
... | inj₂ _    | inj₁ _    = antisym z≤x (trans x≤y y≤z)
... | inj₂ _    | inj₂ y≤x  = antisym (trans z≤x x≤y) y≤z
⊓-assoc x y z | inj₁ x≤y | inj₂ z≤x | inj₂ z≤y with total x z
... | inj₁ _                = Eq.refl
... | inj₂ _                = Eq.refl
⊓-assoc x y z | inj₂ y≤x | inj₁ x≤z | inj₁ y≤z with total y z | total x y
... | inj₁ _    | inj₁ x≤y  = antisym y≤x x≤y
... | inj₁ _    | inj₂ _    = Eq.refl
... | inj₂ z≤y  | inj₁ x≤y  = antisym (trans z≤y y≤x) (trans x≤y y≤z)
... | inj₂ z≤y  | inj₂ _    = antisym z≤y (trans y≤x x≤z)
⊓-assoc x y z | inj₂ y≤x | inj₁ x≤z | inj₂ z≤y with total y z | total x z
... | inj₁ y≤z  | inj₁ _    = antisym y≤x (trans x≤z z≤y)
... | inj₁ y≤z  | inj₂ z≤x  = antisym (trans y≤x x≤z) z≤y
... | inj₂ _    | inj₁ _    = antisym (trans z≤y y≤x) x≤z
... | inj₂ _    | inj₂ z≤x  = Eq.refl
⊓-assoc x y z | inj₂ y≤x | inj₂ z≤x | inj₁ y≤z with total y z | total x y
... | inj₁ _    | inj₁ x≤y  = antisym (trans y≤z z≤x) x≤y
... | inj₁ _    | inj₂ _    = Eq.refl
... | inj₂ z≤y  | inj₁ x≤y  = antisym (trans z≤y y≤x) (trans x≤y y≤z)
... | inj₂ z≤y  | inj₂ _    = antisym z≤y y≤z
⊓-assoc x y z | inj₂ y≤x | inj₂ z≤x | inj₂ z≤y with total y z | total x z
... | inj₁ y≤z  | inj₁ x≤z  = antisym (trans y≤z z≤x) (trans x≤z z≤y)
... | inj₁ y≤z  | inj₂ _    = antisym y≤z z≤y
... | inj₂ _    | inj₁ x≤z  = antisym (trans z≤y y≤x) x≤z
... | inj₂ _    | inj₂ _    = Eq.refl

⊓-identityˡ : ∀ {⊥} → Maximum _≤_ ⊥ → LeftIdentity ⊥ _⊓_
⊓-identityˡ {⊥} top x with total ⊥ x
... | inj₁ ⊥≤x = antisym ⊥≤x (top x)
... | inj₂ x≤⊥ = Eq.refl

⊓-identityʳ : ∀ {⊥} → Maximum _≤_ ⊥ → RightIdentity ⊥ _⊓_
⊓-identityʳ {⊥} top x with total x ⊥
... | inj₁ x≤⊥ = Eq.refl
... | inj₂ ⊥≤x = antisym ⊥≤x (top x)

⊓-identity : ∀ {⊥} → Maximum _≤_ ⊥ → Identity ⊥ _⊓_
⊓-identity top = (⊓-identityˡ top , ⊓-identityʳ top)

⊓-zeroˡ : ∀ {⊥} → Minimum _≤_ ⊥ → LeftZero ⊥ _⊓_
⊓-zeroˡ {⊥} bot x with total ⊥ x
... | inj₁ ⊥≤x = Eq.refl
... | inj₂ x≤⊥ = antisym x≤⊥ (bot x)

⊓-zeroʳ : ∀ {⊥} → Minimum _≤_ ⊥ → RightZero ⊥ _⊓_
⊓-zeroʳ {⊥} bot x with total x ⊥
... | inj₁ x≤⊥ = antisym x≤⊥ (bot x)
... | inj₂ ⊥≤x = Eq.refl

⊓-zero : ∀ {⊥} → Minimum _≤_ ⊥ → Zero ⊥ _⊓_
⊓-zero bot = (⊓-zeroˡ bot , ⊓-zeroʳ bot)

----------------------------------------------------------------------------
-- Algebraic structures

⊓-isMagma : IsMagma _⊓_
⊓-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = ⊓-cong
  }

⊓-isSemigroup : IsSemigroup _⊓_
⊓-isSemigroup = record
  { isMagma = ⊓-isMagma
  ; assoc   = ⊓-assoc
  }

⊓-isBand : IsBand _⊓_
⊓-isBand = record
  { isSemigroup = ⊓-isSemigroup
  ; idem        = ⊓-idem
  }

⊓-isSemilattice : IsSemilattice _⊓_
⊓-isSemilattice = record
  { isBand = ⊓-isBand
  ; comm   = ⊓-comm
  }

⊓-isMonoid : ∀ {⊥} → Maximum _≤_ ⊥ → IsMonoid _⊓_ ⊥
⊓-isMonoid top = record
  { isSemigroup = ⊓-isSemigroup
  ; identity    = ⊓-identity top
  }

----------------------------------------------------------------------------
-- Algebraic packages

⊓-magma : Magma a ℓ₁
⊓-magma = record
  { isMagma = ⊓-isMagma
  }

⊓-semigroup : Semigroup a ℓ₁
⊓-semigroup = record
  { isSemigroup = ⊓-isSemigroup
  }

⊓-band : Band a ℓ₁
⊓-band = record
  { isBand = ⊓-isBand
  }

⊓-semilattice : Semilattice a ℓ₁
⊓-semilattice = record
  { isSemilattice = ⊓-isSemilattice
  }

⊓-monoid : ∀ {⊥} → Maximum _≤_ ⊥ → Monoid a ℓ₁
⊓-monoid top = record
  { isMonoid = ⊓-isMonoid top
  }

----------------------------------------------------------------------------
-- Other properties

x⊓y≈y⇒y≤x : ∀ {x y} → x ⊓ y ≈ y → y ≤ x
x⊓y≈y⇒y≤x {x} {y} x⊓y≈y with total x y
... | inj₁ _   = reflexive (Eq.sym x⊓y≈y)
... | inj₂ y≤x = y≤x

x⊓y≈x⇒x≤y : ∀ {x y} → x ⊓ y ≈ x → x ≤ y
x⊓y≈x⇒x≤y {x} {y} x⊓y≈x with total x y
... | inj₁ x≤y = x≤y
... | inj₂ _   = reflexive (Eq.sym x⊓y≈x)


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Reflexivity {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.Untyped using (Con ; Term)

open import Tools.Nat
open import Tools.Product

private
  variable
    n : Nat
    Γ : Con Term n

-- Reflexivity of valid types.
reflᵛ : ∀ {A l}
        ([Γ] : ⊩ᵛ Γ)
        ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
      → Γ ⊩ᵛ⟨ l ⟩ A ≡ A / [Γ] / [A]
reflᵛ [Γ] [A] ⊢Δ [σ] =
  reflEq (proj₁ ([A] ⊢Δ [σ]))

-- Reflexivity of valid terms.
reflᵗᵛ : ∀ {A t l}
         ([Γ] : ⊩ᵛ Γ)
         ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
         ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A])
       → Γ ⊩ᵛ⟨ l ⟩ t ≡ t ∷ A / [Γ] / [A]
reflᵗᵛ [Γ] [A] [t] ⊢Δ [σ] =
  reflEqTerm (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ]))

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe of proposition functors, along with some properties
------------------------------------------------------------------------

module Relation.Nullary.Universe where

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.Simple
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)
open import Relation.Binary.Sum
open import Relation.Binary.Product.Pointwise
open import Data.Sum     as Sum  hiding (map)
open import Data.Product as Prod hiding (map)
open import Function
import Function.Equality as FunS
open import Data.Empty
open import Category.Applicative
open import Category.Monad
open import Level

infix  5 ¬¬_
infixr 4 _⇒_
infixr 3 _∧_
infixr 2 _∨_
infix  1 ⟨_⟩_≈_

-- The universe.

data PropF p : Set (suc p) where
  Id   : PropF p
  K    : (P : Set p) → PropF p
  _∨_  : (F₁ F₂ : PropF p) → PropF p
  _∧_  : (F₁ F₂ : PropF p) → PropF p
  _⇒_  : (P₁ : Set p) (F₂ : PropF p) → PropF p
  ¬¬_  : (F : PropF p) → PropF p

-- Equalities for universe inhabitants.

mutual

  setoid : ∀ {p} → PropF p → Set p → Setoid p p
  setoid Id        P = PropEq.setoid P
  setoid (K P)     _ = PropEq.setoid P
  setoid (F₁ ∨ F₂) P = (setoid F₁ P) ⊎-setoid (setoid F₂ P)
  setoid (F₁ ∧ F₂) P = (setoid F₁ P) ×-setoid (setoid F₂ P)
  setoid (P₁ ⇒ F₂) P = FunS.≡-setoid P₁
                         (Setoid.indexedSetoid (setoid F₂ P))
  setoid (¬¬ F)    P = Always-setoid (¬ ¬ ⟦ F ⟧ P)

  ⟦_⟧ : ∀ {p} → PropF p → (Set p → Set p)
  ⟦ F ⟧ P = Setoid.Carrier (setoid F P)

⟨_⟩_≈_ : ∀ {p} (F : PropF p) {P : Set p} → Rel (⟦ F ⟧ P) p
⟨_⟩_≈_ F = Setoid._≈_ (setoid F _)

-- ⟦ F ⟧ is functorial.

map : ∀ {p} (F : PropF p) {P Q} → (P → Q) → ⟦ F ⟧ P → ⟦ F ⟧ Q
map Id        f  p = f p
map (K P)     f  p = p
map (F₁ ∨ F₂) f FP = Sum.map  (map F₁ f) (map F₂ f) FP
map (F₁ ∧ F₂) f FP = Prod.map (map F₁ f) (map F₂ f) FP
map (P₁ ⇒ F₂) f FP = map F₂ f ∘ FP
map (¬¬ F)    f FP = ¬¬-map (map F f) FP

map-id : ∀ {p} (F : PropF p) {P} → ⟨ ⟦ F ⟧ P ⇒ F ⟩ map F id ≈ id
map-id Id        x        = refl
map-id (K P)     x        = refl
map-id (F₁ ∨ F₂) (inj₁ x) = ₁∼₁ (map-id F₁ x)
map-id (F₁ ∨ F₂) (inj₂ y) = ₂∼₂ (map-id F₂ y)
map-id (F₁ ∧ F₂) (x , y)  = (map-id F₁ x , map-id F₂ y)
map-id (P₁ ⇒ F₂) f        = λ x → map-id F₂ (f x)
map-id (¬¬ F)    ¬¬x      = _

map-∘ : ∀ {p} (F : PropF p) {P Q R} (f : Q → R) (g : P → Q) →
        ⟨ ⟦ F ⟧ P ⇒ F ⟩ map F f ∘ map F g ≈ map F (f ∘ g)
map-∘ Id        f g x        = refl
map-∘ (K P)     f g x        = refl
map-∘ (F₁ ∨ F₂) f g (inj₁ x) = ₁∼₁ (map-∘ F₁ f g x)
map-∘ (F₁ ∨ F₂) f g (inj₂ y) = ₂∼₂ (map-∘ F₂ f g y)
map-∘ (F₁ ∧ F₂) f g x        = (map-∘ F₁ f g (proj₁ x) ,
                                map-∘ F₂ f g (proj₂ x))
map-∘ (P₁ ⇒ F₂) f g h        = λ x → map-∘ F₂ f g (h x)
map-∘ (¬¬ F)    f g x        = _

-- A variant of sequence can be implemented for ⟦ F ⟧.

sequence : ∀ {p AF} → RawApplicative AF →
           (AF (Lift ⊥) → ⊥) →
           ({A B : Set p} → (A → AF B) → AF (A → B)) →
           ∀ F {P} → ⟦ F ⟧ (AF P) → AF (⟦ F ⟧ P)
sequence {AF = AF} A extract-⊥ sequence-⇒ = helper
  where
  open RawApplicative A

  helper : ∀ F {P} → ⟦ F ⟧ (AF P) → AF (⟦ F ⟧ P)
  helper Id        x        = x
  helper (K P)     x        = pure x
  helper (F₁ ∨ F₂) (inj₁ x) = inj₁ <$> helper F₁ x
  helper (F₁ ∨ F₂) (inj₂ y) = inj₂ <$> helper F₂ y
  helper (F₁ ∧ F₂) (x , y)  = _,_  <$> helper F₁ x ⊛ helper F₂ y
  helper (P₁ ⇒ F₂) f        = sequence-⇒ (helper F₂ ∘ f)
  helper (¬¬ F)    x        =
    pure (λ ¬FP → x (λ fp → extract-⊥ (lift ∘ ¬FP <$> helper F fp)))

-- Some lemmas about double negation.

private
  open module M {p} = RawMonad (¬¬-Monad {p = p})

¬¬-pull : ∀ {p} (F : PropF p) {P} →
          ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
¬¬-pull = sequence rawIApplicative
                   (λ f → f lower)
                   (λ f g → g (λ x → ⊥-elim (f x (λ y → g (λ _ → y)))))

¬¬-remove : ∀ {p} (F : PropF p) {P} →
            ¬ ¬ ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
¬¬-remove F = negated-stable ∘ ¬¬-pull (¬¬ F)


text:
module BFF where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Level using () renaming (zero to ℓ₀)
import Category.Monad
import Category.Functor
open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
open import Data.List using (List ; [] ; _∷_ ; map ; length)
open import Data.Vec using (Vec ; toList ; fromList ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
open import Function using (_∘_ ; flip)
open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)

open import FinMap
open import Generic using (sequenceV ; ≡-to-Π)
open import Structures using (Shaped ; module Shaped)
open import Instances using (VecShaped)
import CheckInsert
open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeShape)

module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
  open GetTypes.PartialShapeShape public using (Get ; module Get)
  open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
  open CheckInsert A

  assoc : {n m : ℕ} → Vec (Fin n) m → Vec Carrier m → Maybe (FinMapMaybe n Carrier)
  assoc []V       []V       = just empty
  assoc (i ∷V is) (b ∷V bs) = (assoc is bs) >>= (checkInsert i b)

  enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (s : S) → C (Fin (Shaped.arity ShapeT s)) s
  enumerate ShapeT s = fill s (allFin (arity s))
    where open Shaped ShapeT

  denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α
  denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c)

  bff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.gl₁ G j))
  bff G {i} j s v = let s′ = enumerate SourceShapeT (gl₁ i)
                        t′ = get s′
                        g  = fromFunc (denumerate SourceShapeT s)
                        g′ = delete-many (Shaped.content ViewShapeT t′) g
                        t  = enumerate SourceShapeT (gl₁ j)
                        h  = assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v)
                        h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j)))) <$> h
                    in ((λ f → fmapS f t) ∘ flip lookupM) <$> h′
    where open Get G

  sbff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G Carrier (Get.gl₁ G j))
  sbff G j s v = bff G j s v >>= Shaped.sequence (Get.SourceShapeT G)

module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
  open GetTypes.PartialVecVec public using (Get)
  open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
  open CheckInsert A

  open PartialShapeBFF A public using (assoc)

  enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n
  enumerate {n} _ = PartialShapeBFF.enumerate A VecShaped n

  enumeratel : (n : ℕ) → Vec (Fin n) n
  enumeratel = PartialShapeBFF.enumerate A VecShaped

  denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
  denumerate = PartialShapeBFF.denumerate A VecShaped

  bff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Vec Carrier (Get.gl₁ G i) → Vec Carrier (Get.gl₂ G j) → Maybe (Vec (Maybe Carrier) (Get.gl₁ G j))
  bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeShape G) j s v

  sbff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Vec Carrier (Get.gl₁ G i) → Vec Carrier (Get.gl₂ G j) → Maybe (Vec Carrier (Get.gl₁ G j))
  sbff  G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeShape G) j s v

module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
  open GetTypes.VecVec public using (Get)
  open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
  open CheckInsert A

  open PartialVecBFF A public using (assoc ; enumerate ; denumerate)

  bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec (Maybe Carrier) m)
  bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G)

  sbff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m)
  sbff G = PartialVecBFF.sbff A (VecVec-to-PartialVecVec G)

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
module MLib.Prelude.FromStdlib where

--------------------------------------------------------------------------------
--  Misc
--------------------------------------------------------------------------------

open import Level public
  using (Level)
  renaming ( zero to zeroˡ; suc to sucˡ; _⊔_ to _⊔ˡ_
           ; Lift to Liftˡ; lift to liftˡ; lower to lowerˡ)

--------------------------------------------------------------------------------
--  Data
--------------------------------------------------------------------------------

module Σ where
  open import Data.Product public
    hiding (module Σ)
  open import Data.Product.Relation.Pointwise.Dependent public
    using (_,_; Pointwise-≡⇒≡; ≡⇒Pointwise-≡)
  open import Data.Product.Relation.Pointwise.NonDependent public
    using (≡×≡⇒≡; ≡⇒≡×≡)
open Σ using (Σ; _×_; _,_; proj₁; proj₂; ∃; ∃₂; curry; uncurry) public

open import Data.Sum public
  using (_⊎_; inj₁; inj₂)

open import Data.Unit public
  using (⊤; tt)
open import Data.Empty public
  using (⊥; ⊥-elim)

module Bool where
  open import Data.Bool public
  open import Data.Bool.Properties public
open Bool using (Bool; true; false; if_then_else_) hiding (module Bool) public

module Nat where
  open import Data.Nat public
  open import Data.Nat.Properties public
open Nat using (ℕ; zero; suc) hiding (module ℕ) public

module Maybe where
  open import Data.Maybe public
open Maybe using (Maybe; just; nothing; maybe) hiding (module Maybe) public

module List where
  open import Data.List public
  open import Data.List.Properties public

  module All where
    open import Data.List.All public hiding (module All)
    open import Data.List.All.Properties public

    traverse : ∀ {a p p′} {A : Set a} {P : A → Set p} {P′ : A → Set p′} → (∀ {x} → P x → Maybe (P′ x)) → {xs : List A} → All P xs → Maybe (All P′ xs)
    traverse f [] = just []
    traverse f (px ∷ ap) with f px | traverse f ap
    traverse f (px ∷ ap) | just px′ | just ap′ = just (px′ ∷ ap′)
    traverse f (px ∷ ap) | _ | _ = nothing

  open All using (All) public

open List using (List; _∷_; []) hiding (module List) public

module Table where
  open import Data.Table public
  open import Data.Table.Properties public
  open import Data.Table.Relation.Equality public
open Table using (Table; tabulate; lookup) hiding (module Table) public

module Vec where
  open import Data.Vec public
    hiding (module Vec)
  open import Data.Vec.Properties public

  module Pointwise where
    open import Data.Vec.Relation.Pointwise.Inductive public
  open Pointwise public
    using (Pointwise; []; _∷_) hiding (module Pointwise)
open Vec public
  using (Vec; []; _∷_)

module FE where
  open import Function.Equality hiding (module Π) public
open FE using (_⟶_; _⟨$⟩_) public

module Inverse where
  open import Function.Inverse public
  open Inverse public
open Inverse using (Inverse; _↔_) hiding (module Inverse) public

module LeftInverse where
  open import Function.LeftInverse public
  open LeftInverse public
open LeftInverse using (LeftInverse; _↞_) hiding (module LeftInverse) public

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

module Function where
  open import Function public
open Function using (id; _∘_; case_of_) public

--------------------------------------------------------------------------------
--  Relations
--------------------------------------------------------------------------------

open import Relation.Nullary public
  using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable public
  using (⌊_⌋)

-- Export names that can only apply to binary relations; things like 'Decidable'
-- can apply to nullary or unary relations too!
open import Relation.Binary.Core public
  using (Reflexive; Symmetric; Transitive; Irreflexive; Antisymmetric; Asymmetric; Trichotomous)
open import Relation.Binary public
  using (Rel; Setoid; IsEquivalence; Poset; IsPartialOrder)

module EqReasoning {c ℓ} (setoid : Setoid c ℓ) where
  open import Relation.Binary.EqReasoning setoid public

module ≡ where
  open import Relation.Binary.PropositionalEquality public
    renaming (module ≡-Reasoning to Reasoning)
open ≡ using (_≡_) public

module ≅ where
  open import Relation.Binary.HeterogeneousEquality public
    renaming (module ≅-Reasoning to Reasoning)
open ≅ using (_≅_) public

--------------------------------------------------------------------------------
--  Algebra
--------------------------------------------------------------------------------

module Algebra where
  open import Algebra public
  open import Algebra.Structures public
  module FunctionProperties {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
    open import Algebra.FunctionProperties _≈_ public

--------------------------------------------------------------------------------
--  From Holes.Prelude
--------------------------------------------------------------------------------

open import Holes.Prelude public using
  ( RawMonad
  ; _>>=_
  ; return
  ; _<$>_
  ; join

  ; RawTraversable
  ; traverse
  ; sequence

  ; Choice
  ; _<|>_
  )

infixl 1 _>>=ₘ_ _>>=ₗ_

_>>=ₘ_ : ∀ {a b} {A : Set a} {B : Set b} → Maybe A → (A → Maybe B) → Maybe B
nothing >>=ₘ _ = nothing
just x >>=ₘ f = f x

_>>=ₗ_ : ∀ {a b} {A : Set a} {B : Set b} → List A → (A → List B) → List B
[] >>=ₗ _ = []
(x ∷ xs) >>=ₗ f = f x List.++ (xs >>=ₗ f)

instance
  Maybe-Monad : ∀ {a} → RawMonad {a} Maybe
  _>>=_  {{Maybe-Monad}} = _>>=ₘ_
  return {{Maybe-Monad}} = just

  List-Monad : ∀ {a} → RawMonad {a} List
  _>>=_  {{List-Monad}} = _>>=ₗ_
  return {{List-Monad}} x = x ∷ []

instance
  Maybe-Traversable : ∀ {a} → RawTraversable {a} Maybe
  traverse {{Maybe-Traversable}} f (just x) = just <$> f x
  traverse {{Maybe-Traversable}} f nothing = return nothing

  List-Traversable : ∀ {a} → RawTraversable {a} List
  traverse {{List-Traversable}} f [] = return []
  traverse {{List-Traversable}} f (x ∷ xs) =
    f x >>= λ x′ →
    traverse {{List-Traversable}} f xs >>= λ xs′ →
    return (x′ ∷ xs′)

instance
  Maybe-Choice : ∀ {a} → Choice {a} Maybe
  Choice._<|>_ Maybe-Choice (just x) _ = just x
  Choice._<|>_ Maybe-Choice nothing y = y

module List-All where
  open List
  open All using ([]; _∷_)

  traverse-map :
    ∀ {a p q r} {A : Set a} {P : A → Set p} {Q : A → Set q} {R : A → Set r}
    (g : ∀ {x} → Q x → Maybe (R x)) (f : ∀ {x} → P x → Q x)
    {xs : List A} (ap : All P xs) → All.traverse g (All.map f ap) ≡ All.traverse (g ∘ f) ap
  traverse-map g f [] = ≡.refl
  traverse-map g f (px ∷ ap) with g (f px)
  traverse-map g f (px ∷ ap) | just _ rewrite traverse-map g f ap = ≡.refl
  traverse-map g f (px ∷ ap) | nothing = ≡.refl

  traverse-just : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} (ap : All P xs) → All.traverse just ap ≡ just ap
  traverse-just [] = ≡.refl
  traverse-just (px ∷ ap) rewrite traverse-just ap = ≡.refl

  traverse-cong :
    ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
    (f g : ∀ {x} → P x → Maybe (Q x)) →
    (∀ {x} (p : P x) → f p ≡ g p) →
    ∀ {xs : List A} (ap : All P xs) →
    All.traverse f ap ≡ All.traverse g ap
  traverse-cong f g eq [] = ≡.refl
  traverse-cong f g eq (px ∷ ap) rewrite eq px | traverse-cong f g eq ap = ≡.refl


text:
module Categories.Agda.ISetoids.Complete where

open import Level
open import Relation.Binary using (Setoid; module Setoid; Preorder; module Preorder; Rel; _=[_]⇒_)
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Categories.Support.IProduct
-- import Relation.Binary.EqReasoning as EqReasoning

open import Categories.Support.Equivalence using (module I→R-Wrapper; setoid-i→r; Fam-setoid; ∀[_]-setoid_)
                                           renaming (Setoid to ISetoid; module Setoid to ISetoid)
open import Categories.Support.SetoidFunctions using (module _⟶_)
open import Categories.Support.PropositionalEquality
import Categories.Support.ZigZag as ZigZag

open import Categories.Category
open import Categories.Functor
import Categories.NaturalTransformation as NT
open import Categories.Agda
open import Categories.Colimit
open import Categories.Object.Initial
open import Categories.Cocones
open import Categories.Cocone

ISetoidsComplete : ∀ {o ℓ e c ℓ′} → Cocomplete o ℓ e (Category.op (ISetoids (c ⊔ ℓ′ ⊔ (o ⊔ ℓ ⊔ e)) (c ⊔ (o ⊔ ℓ ⊔ e))))
ISetoidsComplete {o} {ℓ} {e} {c} {cℓ} = record { colimit = colimit }
  where
  c′ = c ⊔ cℓ ⊔ (o ⊔ ℓ ⊔ e)
  ℓ′ = c ⊔ (o ⊔ ℓ ⊔ e)
  C = Category.op (ISetoids c′ ℓ′)
  colimit : ∀ {J : Category o ℓ e} (F : Functor J C) → Colimit F
  colimit {J} F = record { initial = record
    { ⊥ = record
          { N = Fam-setoid (Σ′ (∀ j → Carrier (F₀ j)) (λ f → ∀ {a b} (h : a J.⇒ b) → (F₀ a ≈ F₁ h ⟨$⟩ f b) (f a)))
                           (∀[ J.Obj ]-setoid F₀) proj₁′
          ; ψ = λ X → record
              { _⟨$⟩_ = λ f → proj₁′ f X
              ; cong  = λ eq → eq X
              }
          ; commute = λ {X} {Y} h {f} {g} f≈g → trans (F₀ X) (f≈g X) (sym (F₀ X) (proj₂′ g h))
          }
    ; ! = λ {A} → record
          { f = record
              { _⟨$⟩_ = λ X → (λ j → Cocone.ψ A j ⟨$⟩ X) , (λ {a} {b} h → sym (F₀ a) (Cocone.commute A h (refl (Cocone.N A))))
              ; cong  = λ i≈j a → cong (Cocone.ψ A a) i≈j
              }
           ; commute = λ {X} x≈y → cong (Cocone.ψ A X) x≈y
           }
    ; !-unique = λ {A} f x≈y a → sym (F₀ a) (CoconeMorphism.commute f (sym (Cocone.N A) x≈y))
    } }
    where
    module J = Category J
    open Functor F
    open ISetoid
    open _⟶_

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Tactic.Nat.NF where

open import Prelude
open import Tactic.Nat.Exp
open import Container.Bag

Tm : Set → Set
Tm Atom = List Atom

NF : Set → Set
NF Atom = Bag (Tm Atom)

product1 : List Nat → Nat
product1 [] = 1
product1 (x ∷ xs) = foldl (λ n x → n * x) x xs

module _ {Atom : Set} {{_ : Ord Atom}} where
  infixl 6 _+nf_
  infixl 7 _*nf_

  _+nf_ : NF Atom → NF Atom → NF Atom
  _+nf_ a b = union a b

  merge : Tm Atom → Tm Atom → Tm Atom
  merge x [] = x
  merge [] y = y
  merge (i ∷ x) (j ∷ y) =
    if i <? j then i ∷ merge x (j ∷ y)
              else j ∷ merge (i ∷ x) y

  nf-sort : NF Atom → NF Atom
  nf-sort [] = []
  nf-sort (x ∷ nf) = union [ x ] (nf-sort nf)

  mulTm : Nat × Tm Atom → Nat × Tm Atom → Nat × Tm Atom
  mulTm (a , x) (b , y) = a * b , merge x y

  _*nf_ : NF Atom → NF Atom → NF Atom
  []      *nf b = []
  (t ∷ a) *nf b = nf-sort (map (mulTm t) b) +nf (a *nf b)

  -- Normalising expressions --
  norm : Exp Atom → NF Atom
  norm (var x) = [ 1 , [ x ] ]
  norm (lit 0) = []
  norm (lit n) = [ n , [] ]
  norm (e ⟨+⟩ e₁) = norm e +nf norm e₁
  norm (e ⟨*⟩ e₁) = norm e *nf norm e₁

  ⟦_⟧t : Nat × Tm Atom → Env Atom → Nat
  ⟦ k , v ⟧t ρ = k * productR (map ρ v)

  ⟦_⟧n : NF Atom → Env Atom → Nat
  ⟦ nf ⟧n ρ = sumR (map (flip ⟦_⟧t ρ) nf)

  ⟦_⟧ts : Nat × Tm Atom → Env Atom → Nat
  ⟦ 1 , v ⟧ts ρ = product1 (map ρ v)
  ⟦ k , v ⟧ts ρ = product1 (map ρ v) * k

  ⟦_⟧ns : NF Atom → Env Atom → Nat
  ⟦ []     ⟧ns ρ = 0
  ⟦ t ∷ nf ⟧ns ρ = foldl (λ n t → n + ⟦ t ⟧ts ρ) (⟦ t ⟧ts ρ) nf

  cancel : NF Atom → NF Atom → NF Atom × NF Atom
  cancel nf₁ [] = nf₁ , []
  cancel [] nf₂ = [] , nf₂
  cancel ((i , x) ∷ nf₁) ((j , y) ∷ nf₂) with compare x y
  ... | less    _ = first  (_∷_ (i , x)) (cancel nf₁ ((j , y) ∷ nf₂))
  ... | greater _ = second (_∷_ (j , y)) (cancel ((i , x) ∷ nf₁) nf₂)
  ... | equal   _ with compare i j
  ...                | less    (diff k _) = second (_∷_ (suc k , y)) (cancel nf₁ nf₂)
  ...                | greater (diff k _) = first  (_∷_ (suc k , x)) (cancel nf₁ nf₂)
  ...                | equal    _         = cancel nf₁ nf₂

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --no-positivity-check #-}
module IIRDr where

import LF
import IIRD

open LF
open IIRD

-- Agda2 has restricted IIRDs so we can define Ur/Tr directly

mutual
  data Ur {I : Set}{D : I -> Set1}(γ : OPr I D)(i : I) : Set where
    intror : Hu γ (Ur γ) (Tr γ) i -> Ur {I}{D} γ i

  Tr : {I : Set}{D : I -> Set1}(γ : OPr I D)(i : I) -> Ur γ i -> D i
  Tr γ i (intror a) = Ht γ (Ur γ) (Tr γ) i a

-- Elimination rule
Rr : {I : Set}{D : I -> Set1}(γ : OPr I D)(F : (i : I) -> Ur γ i -> Set1)
     (h : (i : I)(a : Hu γ (Ur γ) (Tr γ) i) -> KIH (γ i) (Ur γ) (Tr γ) F a -> F i (intror a))
     (i : I)(u : Ur γ i) -> F i u
Rr γ F h i (intror a) = h i a (Kmap (γ i) (Ur γ) (Tr γ) F (Rr γ F h) a)

-- Helpers

ι★r : {I : Set}{D : I -> Set1} -> OP I D One'
ι★r = ι ★'

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Setoids.Orders.Partial.Definition
open import Setoids.Setoids
open import LogicalFormulae
open import Rings.Definition
open import Numbers.Rationals.Definition
open import Functions.Definition

module Numbers.Reals.Definition where

open import Fields.CauchyCompletion.Definition ℚOrdered ℚField
open import Fields.CauchyCompletion.Setoid ℚOrdered ℚField
open import Fields.CauchyCompletion.Addition ℚOrdered ℚField
open import Fields.CauchyCompletion.Multiplication ℚOrdered ℚField
open import Fields.CauchyCompletion.Ring ℚOrdered ℚField
open import Fields.CauchyCompletion.Comparison ℚOrdered ℚField

ℝ : Set
ℝ = CauchyCompletion

_+R_ : ℝ → ℝ → ℝ
_+R_ = _+C_

_*R_ : ℝ → ℝ → ℝ
_*R_ = _*C_

ℝSetoid = cauchyCompletionSetoid

_=R_ : ℝ → ℝ → Set
a =R b = Setoid._∼_ cauchyCompletionSetoid a b

ℝRing : Ring cauchyCompletionSetoid _+R_ _*R_
ℝRing = CRing

injectionR : ℚ → ℝ
injectionR = injection

injectionRInjective : Injection injectionR
injectionRInjective = CInjection'

0R : ℝ
0R = injection 0Q

_<R_ : ℝ → ℝ → Set
_<R_ = _<C_

ℝPartialOrder : SetoidPartialOrder cauchyCompletionSetoid _<C_
ℝPartialOrder = <COrder


text:
-- Andreas, 2016-07-28, issue #779

data D : Set where c : D

record R : Set1 where
  bla : D → D
  bla c = c
  field F : Set

-- Current:
-- Not a valid let-definition

-- Expected:
-- Success, or error outlawing pattern matching definition before last field.


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

open import Categories.Category

-- this module characterizes a category of all products indexed by I.
-- this notion formalizes a category with all products up to certain cardinal.
module Categories.Object.Product.Indexed {o ℓ e} (C : Category o ℓ e) where

open import Level

open import Categories.Morphism.Reasoning C

open Category C
open Equiv
open HomReasoning

record IndexedProductOf {i} {I : Set i} (P : I → Obj) : Set (i ⊔ o ⊔ e ⊔ ℓ) where
  field
    -- the product
    X : Obj

    π   : ∀ i → X ⇒ P i
    ⟨_⟩ : ∀ {Y} → (∀ i → Y ⇒ P i) → Y ⇒ X

    commute : ∀ {Y} (f : ∀ i → Y ⇒ P i) → ∀ i → π i ∘ ⟨ f ⟩ ≈ f i
    unique  : ∀ {Y} (h : Y ⇒ X) (f : ∀ i → Y ⇒ P i) → (∀ i → π i ∘ h ≈ f i) → ⟨ f ⟩ ≈ h

  η : ∀ {Y} (h : Y ⇒ X) → ⟨ (λ i → π i ∘ h) ⟩ ≈ h
  η h = unique _ _ λ _ → refl

  ⟨⟩∘ : ∀ {Y Z} (f : ∀ i → Y ⇒ P i) (g : Z ⇒ Y) → ⟨ f ⟩ ∘ g ≈ ⟨ (λ i → f i ∘ g) ⟩
  ⟨⟩∘ f g = ⟺ (unique _ _ λ i → pullˡ (commute _ _))

  ⟨⟩-cong : ∀ {Y} (f g : ∀ i → Y ⇒ P i) → (eq : ∀ i → f i ≈ g i) → ⟨ f ⟩ ≈ ⟨ g ⟩
  ⟨⟩-cong f g eq = unique _ _ λ i → trans (commute _ _) (⟺ (eq i))

  unique′ : ∀ {Y} (h h′ : Y ⇒ X) → (∀ i → π i ∘ h′ ≈ π i ∘ h) → h′ ≈ h
  unique′ h h′ f = trans (⟺ (unique _ _ f)) (η _)

record IndexedProduct {i} (I : Set i) : Set (i ⊔ o ⊔ e ⊔ ℓ) where
  field
    P         : I → Obj
    productOf : IndexedProductOf P

  open IndexedProductOf productOf public

AllProducts : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
AllProducts i = (I : Set i) → IndexedProduct I

AllProductsOf : ∀ i → Set (o ⊔ ℓ ⊔ e ⊔ suc i)
AllProductsOf i = ∀ {I : Set i} (P : I → Obj) → IndexedProductOf P

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K #-}
open import level
open import algebra.group.core
open import algebra.monoid.mset
open import algebra.monoid.morphism
open import function.extensionality
open import function.isomorphism
open import equality.calculus
open import equality.core
open import sum
open import hott.level
open import hott.equivalence
open import hott.univalence

module algebra.group.gset {i}(G : Set i) ⦃ gG : IsGroup G ⦄ where
  open IsGroup ⦃ ... ⦄

  IsGSet : ∀ {j}(X : Set j) → Set (i ⊔ j)
  IsGSet X = IsMSet G X

  GSet : ∀ j → Set (i ⊔ lsuc j)
  GSet j = Σ (Set j) IsGSet

  GSet₀ : ∀ j → Set (i ⊔ lsuc j)
  GSet₀ j = Σ (Type j 2) λ { (X , hX) → G → X → X }

  GSet₁ : ∀ {j} → GSet₀ j → Set (i ⊔ j)
  GSet₁ ((X , _) , _◂_) =
    ((g₁ g₂ : G)(x : X) → (g₁ * g₂) ◂ x ≡ g₁ ◂ (g₂ ◂ x))
    × ((x : X) → e ◂ x ≡ x)

  gset₁-level : ∀ {j}(X : GSet₀ j)
              → h 1 (GSet₁ X)
  gset₁-level ((X , hX) , act) = ×-level
    (Π-level λ g₁ → Π-level λ g₂ → Π-level λ x → hX _ _)
    (Π-level λ x → hX _ _)

  gset-struct-iso : ∀ {j} → GSet j ≅ Σ (GSet₀ j) GSet₁
  gset-struct-iso = record
    { to = λ { (X , xG) → (((X , IsMSet.mset-level xG) , IsMSet._◂_ xG) ,
                           (IsMSet.◂-hom xG , IsMSet.◂-id xG)) }
    ; from = λ { (((X , hX) , _◂_) , (◂-hom , ◂-id))
             → (X , mk-is-mset _◂_ ◂-hom ◂-id hX) }
    ; iso₁ = λ _ → refl
    ; iso₂ = λ _ → refl }

  open IsMSet ⦃ ... ⦄

  module _ {j k}
           {X : Set j} ⦃ xG : IsGSet X ⦄
           {Y : Set k} ⦃ yG : IsGSet Y ⦄ where
    IsGSetMorphism : (X → Y) → Set (i ⊔ j ⊔ k)
    IsGSetMorphism = IsMSetMorphism G

  module _ {j k}
           (X : Set j) ⦃ xG : IsGSet X ⦄
           (Y : Set k) ⦃ yG : IsGSet Y ⦄ where
    GSetMorphism : Set (i ⊔ j ⊔ k)
    GSetMorphism = Σ (X → Y) IsGSetMorphism

    gsetmorphism-equality : h 2 Y → {f g : X → Y}
      (f-mor : IsGSetMorphism f) (g-mor : IsGSetMorphism g)
      → f ≡ g
      → _≡_ {A = GSetMorphism}
        (f , f-mor)
        (g , g-mor)
    gsetmorphism-equality hY {f} f-mor g-mor refl =
      ap (λ m → (f , m)) (h1⇒prop (is-mset-morphism-level G hY f) _ _)

  module _ {j} (X : Set j) ⦃ xG : IsGSet X ⦄
               (Y : Set j) ⦃ yG : IsGSet Y ⦄ where
    𝑋 𝑌 : GSet j
    𝑋 = (X , xG)
    𝑌 = (Y , yG)

    X₀ Y₀ : GSet₀ j
    X₀ = ((X , IsMSet.mset-level xG) , _◂_)
    Y₀ = ((Y , IsMSet.mset-level yG) , _◂_)

    GSet-univalence : (𝑋 ≡ 𝑌)
                    ≅ (Σ (GSetMorphism X Y) λ { (f , _) → weak-equiv f })
    GSet-univalence = begin
        (𝑋 ≡ 𝑌)
      ≅⟨ iso≡ gset-struct-iso ·≅ sym≅ (subtype-equality gset₁-level) ⟩
        (X₀ ≡ Y₀)
      ≅⟨ sym≅ Σ-split-iso ⟩
        ( Σ (proj₁ X₀ ≡ proj₁ Y₀) λ p →
            subst (λ { (X , _) → G → X → X }) p (proj₂ X₀) ≡ proj₂ Y₀ )
      ≅⟨ ( Σ-ap-iso (sym≅ (subtype-equality λ X → hn-h1 2 X)) λ p
         → trans≡-iso (sym (subst-naturality (λ X → G → X → X)
                             proj₁ p (proj₂ X₀)))) ⟩
        ( Σ (X ≡ Y) λ p → subst (λ X → G → X → X) p (proj₂ X₀) ≡ proj₂ Y₀ )
      ≅⟨ Σ-ap-iso refl≅ (λ p → sym≅ (lem₁ p _ _)) ⟩
        ( Σ (X ≡ Y) λ p → ∀ g w → coerce p (proj₂ X₀ g w)
                                ≡ proj₂ Y₀ g (coerce p w) )
      ≅⟨ ( Σ-ap-iso uni-iso λ p → refl≅ ) ⟩
        ( Σ (X ≈ Y) λ f → ∀ g w → apply≈ f (proj₂ X₀ g w)
                                ≡ proj₂ Y₀ g (apply≈ f w))
      ≅⟨  record
            { to = λ { ((f , we), mor) → ((f , mor) , we) }
            ; from = λ { ((f , mor) , we) → ((f , we) , mor) }
            ; iso₁ = λ _ → refl
            ; iso₂ = λ _ → refl } ⟩
        (Σ (GSetMorphism X Y) λ { (f , _) → weak-equiv f })
      ∎
      where
        open ≅-Reasoning

        lem₁ : {U V : Set j}(p : U ≡ V)
             → (act : G → U → U)
             → (act' : G → V → V)
             → (∀ g u → coerce p (act g u) ≡ act' g (coerce p u))
             ≅ (subst (λ { X → G → X → X }) p act ≡ act')
        lem₁ refl act act' = (Π-ap-iso refl≅ λ g → strong-funext-iso)
          ·≅ strong-funext-iso

  instance
    GisGSet : IsGSet G
    GisGSet = record
      { _◂_ = _*_
      ; ◂-hom = assoc
      ; ◂-id = lunit
      ; mset-level = is-set }

  module _ {j} {X : Set j} (hX : h 2 X) ⦃ xG : IsGSet X ⦄ where
    GSet-repr : (ϕ : G → X) → IsGSetMorphism ϕ
              → (g : G) → ϕ g ≡ g ◂ ϕ e
    GSet-repr ϕ ϕ-mor g = ap ϕ (sym (runit g)) · ϕ-mor g e

    GSet-repr-iso : GSetMorphism G X ≅ X
    GSet-repr-iso = iso f g α β
      where
        f : GSetMorphism G X → X
        f (ϕ , _) = ϕ e

        g : X → GSetMorphism G X
        g x = (ϕ , ϕ-mor)
          where
            ϕ : G → X
            ϕ g = g ◂ x

            ϕ-mor : IsGSetMorphism ϕ
            ϕ-mor g₁ g₂ = ◂-hom g₁ g₂ x

        α : (ϕ : GSetMorphism G X) → g (f ϕ) ≡ ϕ
        α (ϕ , ϕ-mor) = gsetmorphism-equality G X hX _ _
          (funext λ g → sym (GSet-repr ϕ ϕ-mor g))

        β : (x : X) → f (g x) ≡ x
        β x = (IsMSet.◂-id xG) x

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-

Definition of finite sets

There are may different formulations of finite sets in constructive mathematics,
and we will use Bishop finiteness as is usually called in the literature.

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

module Cubical.Data.FinSet.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Data.Nat
open import Cubical.Data.Fin renaming (Fin to Finℕ) hiding (isSetFin)
open import Cubical.Data.SumFin
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ

-- definition of (Bishop) finite sets

-- this definition makes cardinality computation more efficient
isFinSet : Type ℓ → Type ℓ
isFinSet A = Σ[ n ∈ ℕ ] ∥ A ≃ Fin n ∥

isFinOrd : Type ℓ → Type ℓ
isFinOrd A = Σ[ n ∈ ℕ ] A ≃ Fin n

isFinOrd→isFinSet : isFinOrd A → isFinSet A
isFinOrd→isFinSet (_ , p) = _ , ∣ p ∣

-- finite sets are sets

isFinSet→isSet : isFinSet A → isSet A
isFinSet→isSet p = rec isPropIsSet (λ e → isOfHLevelRespectEquiv 2 (invEquiv e) isSetFin) (p .snd)

-- isFinSet is proposition

isPropIsFinSet : isProp (isFinSet A)
isPropIsFinSet p q = Σ≡PropEquiv (λ _ → isPropPropTrunc) .fst (
  Prop.elim2
    (λ _ _ → isSetℕ _ _)
    (λ p q → Fin-inj _ _ (ua (invEquiv (SumFin≃Fin _) ⋆ (invEquiv p) ⋆ q ⋆ SumFin≃Fin _)))
    (p .snd) (q .snd))

-- isFinOrd is Set
-- ordering can be seen as extra structures over finite sets

isSetIsFinOrd : isSet (isFinOrd A)
isSetIsFinOrd = isOfHLevelΣ 2 isSetℕ (λ _ → isOfHLevel⁺≃ᵣ 1 isSetFin)

-- alternative definition of isFinSet

isFinSet' : Type ℓ → Type ℓ
isFinSet' A = ∥ Σ[ n ∈ ℕ ] A ≃ Fin n ∥

isFinSet→isFinSet' : isFinSet A → isFinSet' A
isFinSet→isFinSet' (_ , p) = Prop.rec isPropPropTrunc (λ p → ∣ _ , p ∣) p

isFinSet'→isFinSet : isFinSet' A → isFinSet A
isFinSet'→isFinSet = Prop.rec isPropIsFinSet (λ (n , p) → _ , ∣ p ∣ )

isFinSet≡isFinSet' : isFinSet A ≡ isFinSet' A
isFinSet≡isFinSet' = hPropExt isPropIsFinSet isPropPropTrunc isFinSet→isFinSet' isFinSet'→isFinSet

-- the type of finite sets/propositions

FinSet : (ℓ : Level) → Type (ℓ-suc ℓ)
FinSet ℓ = TypeWithStr _ isFinSet

FinProp : (ℓ : Level) → Type (ℓ-suc ℓ)
FinProp ℓ = Σ[ P ∈ FinSet ℓ ] isProp (P .fst)

-- cardinality of finite sets

card : FinSet ℓ → ℕ
card X = X .snd .fst

-- equality between finite sets/propositions

FinSet≡ : (X Y : FinSet ℓ) → (X .fst ≡ Y .fst) ≃ (X ≡ Y)
FinSet≡ _ _ = Σ≡PropEquiv (λ _ → isPropIsFinSet)

FinProp≡ : (X Y : FinProp ℓ) → (X .fst .fst ≡ Y .fst .fst) ≃ (X ≡ Y)
FinProp≡ X Y = compEquiv (FinSet≡ (X .fst) (Y .fst)) (Σ≡PropEquiv (λ _ → isPropIsProp))

-- hlevels of FinSet and FinProp

isGroupoidFinSet : isGroupoid (FinSet ℓ)
isGroupoidFinSet X Y =
  isOfHLevelRespectEquiv 2 (FinSet≡ X Y)
    (isOfHLevel≡ 2 (isFinSet→isSet (X .snd)) (isFinSet→isSet (Y .snd)))

isSetFinProp : isSet (FinProp ℓ)
isSetFinProp X Y =
  isOfHLevelRespectEquiv 1 (FinProp≡ X Y) (isOfHLevel≡ 1 (X .snd) (Y .snd))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Luau.RuntimeError where

open import Agda.Builtin.Equality using (_≡_)
open import Luau.Heap using (Heap; lookup)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)

data RuntimeErrorᴮ (H : Heap) : Block → Set
data RuntimeErrorᴱ (H : Heap) : Expr → Set

data RuntimeErrorᴱ H where
  NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
  UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
  SEGV : ∀ a → (lookup H a ≡ nothing) → RuntimeErrorᴱ H (addr a)
  app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
  block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)

data RuntimeErrorᴮ H where
  local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
  return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Addition
open import Numbers.Naturals.Order
open import Numbers.Naturals.Multiplication
open import Semirings.Definition
open import Orders.Total.Definition

module Numbers.Naturals.Naturals where

record subtractionNResult (a b : ℕ) .(p : a ≤N b) : Set where
  field
    result : ℕ
    pr : a +N result ≡ b

subtractionNWellDefined : {a b : ℕ} → {p1 p2 : a ≤N b} → (s : subtractionNResult a b p1) → (t : subtractionNResult a b p2) → (subtractionNResult.result s ≡ subtractionNResult.result t)
subtractionNWellDefined {a} {b} {inl x} {pr2} record { result = result1 ; pr = pr1 } record { result = result ; pr = pr } = canSubtractFromEqualityLeft {a} (transitivity pr1 (equalityCommutative pr))
subtractionNWellDefined {a} {.a} {inr refl} {pr2} record { result = result1 ; pr = pr1 } record { result = result2 ; pr = pr } = transitivity g' (equalityCommutative g)
  where
    g : result2 ≡ 0
    g = canSubtractFromEqualityLeft {a} {_} {0} (transitivity pr (equalityCommutative (addZeroRight a)))
    g' : result1 ≡ 0
    g' = canSubtractFromEqualityLeft {a} {_} {0} (transitivity pr1 (equalityCommutative (addZeroRight a)))

-N : {a : ℕ} → {b : ℕ} → (pr : a ≤N b) → subtractionNResult a b pr
-N {zero} {b} prAB = record { result = b ; pr = refl }
-N {succ a} {zero} (inl ())
-N {succ a} {zero} (inr ())
-N {succ a} {succ b} (inl x) with -N {a} {b} (inl (canRemoveSuccFrom<N x))
-N {succ a} {succ b} (inl x) | record { result = result ; pr = pr } = record { result = result ; pr = applyEquality succ pr }
-N {succ a} {succ b} (inr pr) = record { result = 0 ; pr = transitivity (applyEquality succ (addZeroRight a)) pr }

addOneToWeakInequality : {a b : ℕ} → (a ≤N b) → (succ a ≤N succ b)
addOneToWeakInequality {a} {b} (inl ineq) = inl (succPreservesInequality ineq)
addOneToWeakInequality {a} {.a} (inr refl) = inr refl

bumpUpSubtraction : {a b : ℕ} → (p1 : a ≤N b) → (s : subtractionNResult a b p1) → Sg (subtractionNResult (succ a) (succ b) (addOneToWeakInequality p1)) (λ n → subtractionNResult.result n ≡ subtractionNResult.result s)
bumpUpSubtraction {a} {b} a<=b record { result = result ; pr = pr } = record { result = result ; pr = applyEquality succ pr } , refl

addMinus : {a : ℕ} → {b : ℕ} → (pr : a ≤N b) → subtractionNResult.result (-N {a} {b} pr) +N a ≡ b
addMinus {zero} {zero} p = refl
addMinus {zero} {succ b} pr = applyEquality succ (addZeroRight b)
addMinus {succ a} {zero} (inl (le x ()))
addMinus {succ a} {zero} (inr ())
addMinus {succ a} {succ b} (inl x) with (-N {succ a} {succ b} (inl x))
addMinus {succ a} {succ b} (inl x) | record { result = result ; pr = pr } = transitivity (transitivity (applyEquality (_+N succ a) (transitivity (subtractionNWellDefined {p1 = inl (canRemoveSuccFrom<N x)} {p2 = inl (canRemoveSuccFrom<N x)} (record { result = subtractionNResult.result (-N (inl (canRemoveSuccFrom<N x))) ; pr = transitivity (additionNIsCommutative a _) (addMinus (inl (canRemoveSuccFrom<N x)))}) previous) (equalityCommutative t))) (additionNIsCommutative result (succ a))) pr
  where
    pr'' : (a <N b) || (a ≡ b)
    pr'' = (inl (le (_<N_.x x) (transitivity (equalityCommutative (succExtracts (_<N_.x x) a)) (succInjective (_<N_.proof x)))))
    previous : subtractionNResult a b pr''
    previous = -N pr''
    next : Sg (subtractionNResult (succ a) (succ b) (addOneToWeakInequality pr'')) λ n → subtractionNResult.result n ≡ subtractionNResult.result previous
    next = bumpUpSubtraction pr'' previous
    t : result ≡ subtractionNResult.result (underlying next)
    t = subtractionNWellDefined {succ a} {succ b} {inl x} {addOneToWeakInequality pr''} (record { result = result ; pr = pr }) (underlying next)
addMinus {succ a} {succ .a} (inr refl) = refl

addMinus' : {a b : ℕ} → (pr : a ≤N b) → a +N subtractionNResult.result (-N {a} {b} pr) ≡ b
addMinus' {a} {b} pr rewrite additionNIsCommutative a (subtractionNResult.result (-N {a} {b} pr)) = addMinus {a} {b} pr

additionPreservesInequality : {a b : ℕ} → (c : ℕ) → a <N b → a +N c <N b +N c
additionPreservesInequality {a} {b} zero prAB rewrite additionNIsCommutative a 0 | additionNIsCommutative b 0 = prAB
additionPreservesInequality {a} {b} (succ c) (le x proof) = le x (transitivity (equalityCommutative (additionNIsAssociative (succ x) a (succ c))) (applyEquality (_+N succ c) proof))

additionPreservesInequalityOnLeft : {a b : ℕ} → (c : ℕ) → a <N b → c +N a <N c +N b
additionPreservesInequalityOnLeft {a} {b} c prAB = identityOfIndiscernablesRight (λ a b → a <N b) (identityOfIndiscernablesLeft (λ a b → a <N b) (additionPreservesInequality {a} {b} c prAB) (additionNIsCommutative a c)) (additionNIsCommutative b c)

multiplyIncreases : (a : ℕ) → (b : ℕ) → succ zero <N a → zero <N b → b <N a *N b
multiplyIncreases zero b (le x ()) prB
multiplyIncreases (succ zero) b (le zero ()) prb
multiplyIncreases (succ zero) b (le (succ x) ()) prb
multiplyIncreases (succ (succ a)) (succ b) prA prb = le (b +N a *N succ b) (applyEquality succ (transitivity (Semiring.commutative ℕSemiring _ (succ b)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b _)) (Semiring.commutative ℕSemiring _ b))))

canTimesOneOnLeft : {a b : ℕ} → (a <N b) → (a *N (succ zero)) <N b
canTimesOneOnLeft {a} {b} prAB = identityOfIndiscernablesLeft _<N_ prAB (equalityCommutative (productWithOneRight a))

canTimesOneOnRight : {a b : ℕ} → (a <N b) → a <N (b *N (succ zero))
canTimesOneOnRight {a} {b} prAB = identityOfIndiscernablesRight _<N_ prAB (equalityCommutative (productWithOneRight b))

canSwapAddOnLeftOfInequality : {a b c : ℕ} → (a +N b <N c) → (b +N a <N c)
canSwapAddOnLeftOfInequality {a} {b} {c} pr = identityOfIndiscernablesLeft _<N_ pr (additionNIsCommutative a b)

canSwapAddOnRightOfInequality : {a b c : ℕ} → (a <N b +N c) → (a <N c +N b)
canSwapAddOnRightOfInequality {a} {b} {c} pr = identityOfIndiscernablesRight _<N_ pr (additionNIsCommutative b c)

bumpDownOnRight : (a c : ℕ) → c *N succ a ≡ c *N a +N c
bumpDownOnRight a c = transitivity (multiplicationNIsCommutative c (succ a)) (transitivity refl (transitivity (additionNIsCommutative c (a *N c)) ((addingPreservesEqualityRight c (multiplicationNIsCommutative a c) ))))

succIsNonzero : {a : ℕ} → (succ a ≡ zero) → False
succIsNonzero {a} ()

lessImpliesNotEqual : {a b : ℕ} → (a <N b) → a ≡ b → False
lessImpliesNotEqual {a} {.a} prAB refl = TotalOrder.irreflexive ℕTotalOrder prAB

-NIsDecreasing : {a b : ℕ} → (prAB : succ a <N b) → subtractionNResult.result (-N (inl prAB)) <N b
-NIsDecreasing {a} {b} prAB with (-N (inl prAB))
-NIsDecreasing {a} {b} (le x proof) | record { result = result ; pr = pr } = record { x = a ; proof = pr }

sumZeroImpliesSummandsZero : {a b : ℕ} → (a +N b ≡ zero) → ((a ≡ zero) && (b ≡ zero))
sumZeroImpliesSummandsZero {zero} {zero} pr = record { fst = refl ; snd = refl }
sumZeroImpliesSummandsZero {zero} {(succ b)} pr = record { fst = refl ; snd = pr }
sumZeroImpliesSummandsZero {(succ a)} {zero} ()
sumZeroImpliesSummandsZero {(succ a)} {(succ b)} ()

productWithNonzeroZero : (a b : ℕ) → (a *N succ b ≡ zero) → a ≡ zero
productWithNonzeroZero zero b pr = refl
productWithNonzeroZero (succ a) b ()

productOneImpliesOperandsOne : {a b : ℕ} → (a *N b ≡ 1) → (a ≡ 1) && (b ≡ 1)
productOneImpliesOperandsOne {zero} {b} ()
productOneImpliesOperandsOne {succ a} {zero} pr = exFalso absurd''
  where
    absurd : zero *N (succ a) ≡ 1
    absurd' : 0 ≡ 1
    absurd'' : False
    absurd'' = succIsNonzero (equalityCommutative absurd')
    absurd = identityOfIndiscernablesLeft _≡_ pr (productZeroIsZeroRight a)
    absurd' = absurd
productOneImpliesOperandsOne {succ a} {succ b} pr = record { fst = r' ; snd = (applyEquality succ (_&&_.fst q)) }
  where
    p : b +N a *N succ b ≡ zero
    p = succInjective pr
    q : (b ≡ zero) && (a *N succ b ≡ zero)
    q = sumZeroImpliesSummandsZero p
    r : a ≡ zero
    r = productWithNonzeroZero a b (_&&_.snd q)
    r' : succ a ≡ 1
    r' = applyEquality succ r

oneTimesPlusZero : (a : ℕ) → a ≡ a *N succ zero +N zero
oneTimesPlusZero a = identityOfIndiscernablesRight _≡_ (equalityCommutative (productWithOneRight a)) (equalityCommutative (addZeroRight (a *N succ zero)))

equivalentSubtraction' : (a b c d : ℕ) → (a<c : a <N c) → (d<b : d <N b) → (subtractionNResult.result (-N {a} {c} (inl a<c))) ≡ (subtractionNResult.result (-N {d} {b} (inl d<b))) → a +N b ≡ c +N d
equivalentSubtraction' a b c d prac prdb eq with -N (inl prac)
equivalentSubtraction' a b c d prac prdb eq | record { result = result ; pr = pr } with -N (inl prdb)
equivalentSubtraction' a b c d prac prdb refl | record { result = .result ; pr = pr1 } | record { result = result ; pr = pr } rewrite (equalityCommutative pr) = go
  where
    go : a +N (d +N result) ≡ c +N d
    go rewrite (equalityCommutative pr1) = t
      where
        t : a +N (d +N result) ≡ (a +N result) +N d
        t rewrite (additionNIsAssociative a result d) = applyEquality (λ n → a +N n) (additionNIsCommutative d result)

lessThanMeansPositiveSubtr : {a b : ℕ} → (a<b : a <N b) → (subtractionNResult.result (-N (inl a<b)) ≡ 0) → False
lessThanMeansPositiveSubtr {a} {b} a<b pr with -N (inl a<b)
lessThanMeansPositiveSubtr {a} {b} a<b pr | record { result = result ; pr = sub } rewrite pr | addZeroRight a = lessImpliesNotEqual a<b sub

moveOneSubtraction : {a b c : ℕ} → {a<=b : a ≤N b} → (subtractionNResult.result (-N {a} {b} a<=b)) ≡ c → b ≡ a +N c
moveOneSubtraction {a} {b} {zero} {inl a<b} pr rewrite addZeroRight a = exFalso (lessThanMeansPositiveSubtr {a} {b} a<b pr)
moveOneSubtraction {a} {b} {succ c} {inl a<b} pr with -N (inl a<b)
moveOneSubtraction {a} {b} {succ c} {inl a<b} pr | record { result = result ; pr = sub } rewrite pr | sub = refl
moveOneSubtraction {a} {.a} {zero} {inr refl} pr = equalityCommutative (addZeroRight a)
moveOneSubtraction {a} {.a} {succ c} {inr refl} pr = identityOfIndiscernablesRight _≡_ (equalityCommutative (addZeroRight a)) (applyEquality (λ t → a +N t) pr')
  where
    selfSub : (r : ℕ) → subtractionNResult.result (-N {r} {r} (inr refl)) ≡ zero
    selfSub zero = refl
    selfSub (succ r) = refl
    pr' : 0 ≡ succ c
    pr' = transitivity (equalityCommutative (selfSub a)) pr

moveOneSubtraction' : {a b c : ℕ} → {a<=b : a ≤N b} → (b ≡ a +N c) → subtractionNResult.result (-N {a} {b} a<=b) ≡ c
moveOneSubtraction' {a} {b} {c} {inl x} pr with -N (inl x)
moveOneSubtraction' {a} {b} {c} {inl x} pr | record { result = result ; pr = pr1 } rewrite pr = canSubtractFromEqualityLeft pr1
moveOneSubtraction' {a} {b} {c} {inr x} pr with -N (inr x)
moveOneSubtraction' {a} {b} {c} {inr x} pr | record { result = result ; pr = pr1 } rewrite pr = canSubtractFromEqualityLeft pr1

equivalentSubtraction : (a b c d : ℕ) → (a<c : a <N c) → (d<b : d <N b) → a +N b ≡ c +N d → (subtractionNResult.result (-N {a} {c} (inl a<c))) ≡ (subtractionNResult.result (-N {d} {b} (inl d<b)))
equivalentSubtraction zero b c d prac (le x proof) eq with (-N (inl (le x proof)))
equivalentSubtraction zero b c d prac (le x proof) eq | record { result = result ; pr = pr } = equalityCommutative p''
  where
    p : d +N result ≡ c +N d
    p = transitivity pr eq
    p' : d +N result ≡ d +N c
    p' = transitivity p (additionNIsCommutative c d)
    p'' : result ≡ c
    p'' = canSubtractFromEqualityLeft {d} {result} {c} p'
equivalentSubtraction (succ a) b zero d (le x ()) prdb eq
equivalentSubtraction (succ a) b (succ c) d prac prdb eq with (-N (inl (canRemoveSuccFrom<N prac)))
equivalentSubtraction (succ a) b (succ c) d prac prdb eq | record { result = c-a ; pr = prc-a } with -N (inl prdb)
equivalentSubtraction (succ a) b (succ c) d prac prdb eq | record { result = c-a ; pr = prc-a } | record { result = result ; pr = pr } rewrite equalityCommutative prc-a | equalityCommutative pr | equalityCommutative (additionNIsAssociative a d result) | additionNIsCommutative (a +N c-a) d | equalityCommutative (additionNIsAssociative d a c-a) | additionNIsCommutative a d = equalityCommutative (canSubtractFromEqualityLeft eq)

leLemma : (b c : ℕ) → (b ≤N c) ≡ (b +N zero ≤N c +N zero)
leLemma b c rewrite addZeroRight c = q
  where
    q : (b ≤N c) ≡ (b +N zero ≤N c)
    q rewrite addZeroRight b = refl

lessCast : {a b c : ℕ} → (pr : a ≤N b) → (eq : a ≡ c) → c ≤N b
lessCast {a} {b} pr eq rewrite eq = pr

lessCast' : {a b c : ℕ} → (pr : a ≤N b) → (eq : b ≡ c) → a ≤N c
lessCast' {a} {b} pr eq rewrite eq = pr

subtractionCast : {a b c : ℕ} → {pr : a ≤N b} → (eq : a ≡ c) → (p : subtractionNResult a b pr) → Sg (subtractionNResult c b (lessCast pr eq)) (λ res → subtractionNResult.result p ≡ subtractionNResult.result res)
subtractionCast {a} {b} {c} {a<b} eq subt rewrite eq = (subt , refl)

subtractionCast' : {a b c : ℕ} → {pr : a ≤N b} → (eq : b ≡ c) → (p : subtractionNResult a b pr) → Sg (subtractionNResult a c (lessCast' pr eq)) (λ res → subtractionNResult.result p ≡ subtractionNResult.result res)
subtractionCast' {a} {b} {c} {a<b} eq subt rewrite eq = (subt , refl)

addToRightWeakInequality : (a : ℕ) → {b c : ℕ} → (pr : b ≤N c) → (b ≤N c +N a)
addToRightWeakInequality zero {b} {c} (inl x) rewrite (addZeroRight c) = inl x
addToRightWeakInequality (succ a) {b} {c} (inl x) = inl (TotalOrder.<Transitive ℕTotalOrder x (addingIncreases c a))
addToRightWeakInequality zero {b} {.b} (inr refl) = inr (equalityCommutative (addZeroRight b))
addToRightWeakInequality (succ a) {b} {.b} (inr refl) = inl (addingIncreases b a)

addAssocLemma : (a b c : ℕ) → (a +N b) +N c ≡ (a +N c) +N b
addAssocLemma a b c rewrite (additionNIsAssociative a b c) = g
  where
    g : a +N (b +N c) ≡ (a +N c) +N b
    g rewrite (additionNIsAssociative a c b) = applyEquality (λ t → a +N t) (additionNIsCommutative b c)

addIntoSubtraction : (a : ℕ) → {b c : ℕ} → (pr : b ≤N c) → a +N (subtractionNResult.result (-N {b} {c} pr)) ≡ subtractionNResult.result (-N {b} {c +N a} (addToRightWeakInequality a pr))
addIntoSubtraction a {b} {c} pr with (-N {b} {c} pr)
addIntoSubtraction a {b} {c} pr | record { result = c-b ; pr = prc-b } with (-N {b} {c +N a} (addToRightWeakInequality a pr))
addIntoSubtraction a {b} {c} pr | record { result = c-b ; pr = prc-b } | record { result = c+a-b ; pr = prcab } = equalityCommutative g'''
  where
    g : (b +N c+a-b) +N c-b ≡ c +N (a +N c-b)
    g rewrite (equalityCommutative (additionNIsAssociative c a c-b)) = applyEquality (λ t → t +N c-b) prcab
    g' : (b +N c-b) +N c+a-b ≡ c +N (a +N c-b)
    g' = identityOfIndiscernablesLeft _≡_ g (addAssocLemma b c+a-b c-b)
    g'' : c +N c+a-b ≡ c +N (a +N c-b)
    g'' = identityOfIndiscernablesLeft _≡_ g' (applyEquality (λ i → i +N c+a-b) prc-b)
    g''' : c+a-b ≡ a +N c-b
    g''' = canSubtractFromEqualityLeft {c} {c+a-b} {a +N c-b} g''

addStrongInequalities : {a b c d : ℕ} → (a<b : a <N b) → (c<d : c <N d) → (a +N c <N b +N d)
addStrongInequalities {zero} {zero} {c} {d} prab prcd = prcd
addStrongInequalities {zero} {succ b} {c} {d} prab prcd rewrite (additionNIsCommutative b d) = TotalOrder.<Transitive ℕTotalOrder prcd (cannotAddAndEnlarge d b)
addStrongInequalities {succ a} {zero} {c} {d} (le x ()) prcd
addStrongInequalities {succ a} {succ b} {c} {d} prab prcd = succPreservesInequality (addStrongInequalities (canRemoveSuccFrom<N prab) prcd)

addWeakInequalities : {a b c d : ℕ} → (a<=b : a ≤N b) → (c<=d : c ≤N d) → (a +N c) ≤N (b +N d)
addWeakInequalities {a} {b} {c} {d} (inl x) (inl y) = inl (addStrongInequalities x y)
addWeakInequalities {a} {b} {c} {.c} (inl x) (inr refl) = inl (additionPreservesInequality c x)
addWeakInequalities {a} {.a} {c} {d} (inr refl) (inl x) = inl (additionPreservesInequalityOnLeft a x)
addWeakInequalities {a} {.a} {c} {.c} (inr refl) (inr refl) = inr refl

addSubIntoSub : {a b c d : ℕ} → (a<b : a ≤N b) → (c<d : c ≤N d) → (subtractionNResult.result (-N {a} {b} a<b)) +N (subtractionNResult.result (-N {c} {d} c<d)) ≡ subtractionNResult.result (-N {a +N c} {b +N d} (addWeakInequalities a<b c<d))
addSubIntoSub {a}{b}{c}{d} a<b c<d with (-N {a} {b} a<b)
addSubIntoSub {a} {b} {c} {d} a<b c<d | record { result = b-a ; pr = prb-a } with (-N {c} {d} c<d)
addSubIntoSub {a} {b} {c} {d} a<b c<d | record { result = b-a ; pr = prb-a } | record { result = d-c ; pr = prd-c } with (-N {a +N c} {b +N d} (addWeakInequalities a<b c<d))
addSubIntoSub {a} {b} {c} {d} a<b c<d | record { result = b-a ; pr = prb-a } | record { result = d-c ; pr = prd-c } | record { result = b+d-a-c ; pr = pr } = equalityCommutative r
  where
    pr' : (a +N c) +N b+d-a-c ≡ (a +N b-a) +N d
    pr' rewrite prb-a = pr
    pr'' : a +N (c +N b+d-a-c) ≡ (a +N b-a) +N d
    pr'' rewrite (equalityCommutative (additionNIsAssociative a c b+d-a-c)) = pr'
    pr''' : a +N (c +N b+d-a-c) ≡ a +N (b-a +N d)
    pr''' rewrite (equalityCommutative (additionNIsAssociative a b-a d)) = pr''
    q : c +N b+d-a-c ≡ b-a +N d
    q = canSubtractFromEqualityLeft {a} pr'''
    q' : c +N b+d-a-c ≡ b-a +N (c +N d-c)
    q' rewrite prd-c = q
    q'' : c +N b+d-a-c ≡ (b-a +N c) +N d-c
    q'' rewrite additionNIsAssociative b-a c d-c = q'
    q''' : c +N b+d-a-c ≡ (c +N b-a) +N d-c
    q''' rewrite additionNIsCommutative c b-a = q''
    q'''' : c +N b+d-a-c ≡ c +N (b-a +N d-c)
    q'''' rewrite equalityCommutative (additionNIsAssociative c b-a d-c) = q'''
    r : b+d-a-c ≡ b-a +N d-c
    r = canSubtractFromEqualityLeft {c} q''''

subtractProduct : {a b c : ℕ} → (aPos : 0 <N a) → (b<c : b <N c) →
    (a *N (subtractionNResult.result (-N (inl b<c)))) ≡ subtractionNResult.result (-N {a *N b} {a *N c} (inl (lessRespectsMultiplicationLeft b c a b<c aPos)))
subtractProduct {zero} {b} {c} aPos b<c = refl
subtractProduct {succ zero} {b} {c} aPos b<c = s'
  where
    resbc = -N {b} {c} (inl b<c)
    resbc' : Sg (subtractionNResult (b +N 0 *N b) c (lessCast (inl b<c) (equalityCommutative (addZeroRight b)))) ((λ res → subtractionNResult.result resbc ≡ subtractionNResult.result res))
    resbc'' : Sg (subtractionNResult (b +N 0 *N b) (c +N 0 *N c) (lessCast' (lessCast (inl b<c) (equalityCommutative (addZeroRight b))) (equalityCommutative (addZeroRight c)))) (λ res → subtractionNResult.result (underlying resbc') ≡ subtractionNResult.result res)
    g : (rsbc' : Sg (subtractionNResult (b +N 0 *N b) c (lessCast (inl b<c) (equalityCommutative (addZeroRight b)))) (λ res → subtractionNResult.result resbc ≡ subtractionNResult.result res)) → subtractionNResult.result resbc ≡ subtractionNResult.result (underlying rsbc')
    g' : (rsbc'' : Sg (subtractionNResult (b +N 0 *N b) (c +N 0 *N c) (lessCast' (lessCast (inl b<c) (equalityCommutative (addZeroRight b))) (equalityCommutative (addZeroRight c)))) (λ res → subtractionNResult.result (underlying resbc') ≡ subtractionNResult.result res)) → subtractionNResult.result (underlying resbc') ≡ subtractionNResult.result (underlying rsbc'')
    q : subtractionNResult.result resbc ≡ subtractionNResult.result (underlying resbc'')
    r : subtractionNResult.result (underlying resbc'') ≡ subtractionNResult.result (-N {b +N 0 *N b} {c +N 0 *N c} (inl (lessRespectsMultiplicationLeft b c 1 b<c aPos)))
    s : subtractionNResult.result resbc ≡ subtractionNResult.result (-N {b +N 0 *N b} {c +N 0 *N c} (inl (lessRespectsMultiplicationLeft b c 1 b<c aPos)))
    s = transitivity q r
    s' : subtractionNResult.result resbc +N 0 ≡ subtractionNResult.result (-N {b +N 0 *N b} {c +N 0 *N c} (inl (lessRespectsMultiplicationLeft b c 1 b<c aPos)))
    s' = identityOfIndiscernablesLeft _≡_ s (equalityCommutative (addZeroRight _))
    r = subtractionNWellDefined {b +N 0 *N b} {c +N 0 *N c} {(lessCast' (lessCast (inl b<c) (equalityCommutative (addZeroRight b))) (equalityCommutative (addZeroRight c)))} {inl (lessRespectsMultiplicationLeft b c 1 b<c aPos)} (underlying resbc'') (-N {b +N 0 *N b} {c +N 0 *N c} (inl (lessRespectsMultiplicationLeft b c 1 b<c aPos)))
    g (a , b) = b
    g' (a , b) = b
    resbc'' = subtractionCast' {pr = inl (identityOfIndiscernablesLeft _<N_ b<c (equalityCommutative (addZeroRight b)))} (equalityCommutative (addZeroRight c)) (underlying resbc')
    q = transitivity {_} {_} {subtractionNResult.result resbc} {subtractionNResult.result (underlying resbc')} {subtractionNResult.result (underlying resbc'')} (g resbc') (g' resbc'')
    resbc' = subtractionCast {b} {c} {b +N 0 *N b} {inl b<c} (equalityCommutative (addZeroRight b)) resbc

subtractProduct {succ (succ a)} {b} {c} aPos b<c =
  let
    t : (succ a) *N subtractionNResult.result (-N {b} {c} (inl b<c)) ≡ subtractionNResult.result (-N {(succ a) *N b} {(succ a) *N c} (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a))))
    t = subtractProduct {succ a} {b} {c} (succIsPositive a) b<c
  in
    go t  --go t
    where
      go : (succ a) *N subtractionNResult.result (-N {b} {c} (inl b<c)) ≡ subtractionNResult.result (-N {(succ a) *N b} {(succ a) *N c} (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a)))) → (subtractionNResult.result (-N (inl b<c)) +N (subtractionNResult.result (-N (inl b<c)) +N a *N subtractionNResult.result (-N (inl b<c))) ≡ subtractionNResult.result (-N (inl (lessRespectsMultiplicationLeft b c (succ (succ a)) b<c aPos))))
      go t = transitivity {_} {_} {lhs} {middle2} {rhs} u' v
        where
          c-b = subtractionNResult.result (-N {b} {c} (inl b<c))
          lhs = c-b +N (succ a) *N c-b
          middle = subtractionNResult.result (-N {(succ a) *N b} {(succ a) *N c} (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a))))
          middle2 = subtractionNResult.result (-N {b +N (succ a *N b)} {c +N (succ a *N c)} (addWeakInequalities (inl b<c) (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a)))))
          rhs = subtractionNResult.result (-N {succ (succ a) *N b} {(succ (succ a)) *N c} (inl (lessRespectsMultiplicationLeft b c (succ (succ a)) b<c aPos)))
          lhs' : lhs ≡ c-b +N middle
          u : c-b +N middle ≡ middle2
          u' : lhs ≡ middle2
          v : middle2 ≡ rhs
          u'' : c-b +N subtractionNResult.result (-N {(succ a) *N b} {(succ a) *N c} (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a)))) ≡ rhs

          u'' rewrite equalityCommutative v = u
          u' rewrite equalityCommutative u = lhs'
          lhs' rewrite t = refl
          u = addSubIntoSub (inl b<c) (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a)))
          v = subtractionNWellDefined {succ (succ a) *N b} {succ (succ a) *N c} {addWeakInequalities (inl b<c) (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a)))} {inl (lessRespectsMultiplicationLeft b c (succ (succ a)) b<c aPos)} (-N {b +N (succ a *N b)} {c +N (succ a *N c)} (addWeakInequalities (inl b<c) (inl (lessRespectsMultiplicationLeft b c (succ a) b<c (succIsPositive a))))) (-N {(succ (succ a)) *N b} {(succ (succ a)) *N c} (inl (lessRespectsMultiplicationLeft b c (succ (succ a)) b<c aPos)))

subtractProduct' : {a b c : ℕ} → (aPos : 0 <N a) → (b<c : b <N c) →
  (subtractionNResult.result (-N (inl b<c))) *N a ≡ subtractionNResult.result (-N {a *N b} {a *N c} (inl (lessRespectsMultiplicationLeft b c a b<c aPos)))
subtractProduct' {a} aPos b<c = identityOfIndiscernablesLeft _≡_ (subtractProduct aPos b<c) (multiplicationNIsCommutative a _)

equalityDecidable : (a b : ℕ) → (a ≡ b) || ((a ≡ b) → False)
equalityDecidable zero zero = inl refl
equalityDecidable zero (succ b) = inr naughtE
equalityDecidable (succ a) zero = inr λ t → naughtE (equalityCommutative t)
equalityDecidable (succ a) (succ b) with equalityDecidable a b
equalityDecidable (succ a) (succ b) | inl x = inl (applyEquality succ x)
equalityDecidable (succ a) (succ b) | inr x = inr (λ t → x (succInjective t))

cannotAddKeepingEquality : (a b : ℕ) → (a ≡ a +N succ b) → False
cannotAddKeepingEquality zero zero pr = naughtE pr
cannotAddKeepingEquality (succ a) zero pr = cannotAddKeepingEquality a zero (succInjective pr)
cannotAddKeepingEquality zero (succ b) pr = naughtE pr
cannotAddKeepingEquality (succ a) (succ b) pr = cannotAddKeepingEquality a (succ b) (succInjective pr)

<NWellDefined' : {a b c d : ℕ} → a ≡ c → b ≡ d → a <N b → c <N d
<NWellDefined' {a} {b} {c} {d} a=c b=d a<b rewrite a=c | b=d = a<b


text:
module Prelude.Decidable where

open import Prelude.Empty

data Dec {a} (P : Set a) : Set a where
  yes : P → Dec P
  no  : ¬ P → Dec P

infix 0 ifYes_then_else_ ifNo_then_else_
ifYes_then_else_ : ∀ {a b} {A : Set a} {B : Set b} → Dec A → B → B → B
ifYes yes _ then x else _ = x
ifYes no  _ then _ else y = y

ifNo_then_else_ : ∀ {a b} {A : Set a} {B : Set b} → Dec A → B → B → B
ifNo d then x else y = ifYes d then y else x

FromDec : ∀ {a} {P : Set a} → Dec P → Set a
FromDec {P = P} (yes _) = P
FromDec {P = P} (no  _) = ¬ P

fromDec : ∀ {a} {P : Set a} (d : Dec P) → FromDec d
fromDec (yes x) = x
fromDec (no  x) = x

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --without-K #-}
open import Type
open import Function
open import Function.Extensionality
open import Data.Fin using (Fin)
open import Level.NP
open import Algebra
open import Algebra.FunctionProperties.NP
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat
open import Data.Product
open import Relation.Binary.NP

open import Explore.Core
open import Explore.Properties
open import Explore.Explorable
import Explore.Fin
open Explore.Fin.Regular
open import HoTT

module Explore.Function.Fin where

postulate
  Postulate-FinFunˢ-ok : ★
-- open ExplorableRecord

module _ {A : ★}(μA : Explorable A) where

  eᴬ = explore μA

  extend : ∀ {n} → A → (Fin n → A) → Fin (suc n) → A
  extend x g zero    = x
  extend x g (suc i) = g i

  ¬Fin0 : Fin 0 → A
  ¬Fin0 ()

  -- There is one function Fin 0 → A (called abs) so this should be fine
  -- if not there is a version below that forces the domain to be non-empty
  FinFunᵉ : ∀ n → Explore _ (Fin n → A)
  FinFunᵉ zero    z op f = f ¬Fin0
  FinFunᵉ (suc n) z op f = eᴬ z op (λ x → FinFunᵉ n z op (f ∘ extend x))

  FinFunⁱ : ∀ n → ExploreInd _ (FinFunᵉ n)
  FinFunⁱ zero    P Pz P∙ Pf = Pf _
  FinFunⁱ (suc n) P Pz P∙ Pf =
    explore-ind μA (λ sa → P (λ z op f → sa z op (λ x → FinFunᵉ n z op (f ∘ extend x))))
      Pz P∙
      (λ x → FinFunⁱ n (λ sf → P (λ z op f → sf z op (f ∘ extend x)))
        Pz P∙ (Pf ∘ extend x))

  FinFunˢ : ∀ n → Sum (Fin n → A)
  FinFunˢ n = FinFunᵉ n 0 _+_

  postulate
    FinFunˢ-ok : ∀ {{_ : Postulate-FinFunˢ-ok}} n → Adequate-sum (FinFunˢ n)

  μFinFun : ∀ {{_ : Postulate-FinFunˢ-ok}} {n} → Explorable (Fin n → A)
  μFinFun = mk _ (FinFunⁱ _) (FinFunˢ-ok _)

module BigDistr
  {{_ : Postulate-FinFunˢ-ok}} {{_ : FunExt}} {{_ : UA}}
  {A : ★}(μA : Explorable A)
  (cm           : CommutativeMonoid ₀ ₀)
  -- we want (open CMon cm) !!!
  (_◎_          : let open CMon cm in C → C → C)
  (ε-◎          : let open CMon cm in Zero _≈_ ε _◎_)
  (distrib      : let open CMon cm in _DistributesOver_ _≈_ _◎_ _∙_)
  (_◎-cong_     : let open CMon cm in _◎_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_) where

  open CMon cm renaming (sym to ≈-sym)

  μF→A = μFinFun μA

  -- Sum over A
  Σᴬ = explore μA ε _∙_

  -- Sum over (Fin(1+I)→A) functions
  Σ' : ∀ {I} → ((Fin I → A) → C) → C
  Σ' = explore μF→A ε _∙_

  -- Product over Fin(1+I) values
  Π' = λ I → explore (μFin I) ε _◎_

  bigDistr : ∀ I F → Π' I (Σᴬ ∘ F) ≈ Σ' (Π' I ∘ _ˢ_ F)
  bigDistr zero    _ = refl
  bigDistr (suc I) F
    = Σᴬ (F zero) ◎ Π' I (Σᴬ ∘ F ∘ suc)
    ≈⟨ refl ◎-cong bigDistr I (F ∘ suc) ⟩
      Σᴬ (F zero) ◎ Σ' (Π' I ∘ _ˢ_ (F ∘ suc))
    ≈⟨ ≈-sym (explore-linʳ μA monoid _◎_ (F zero) (Σ' (Π' I ∘ _ˢ_ (F ∘ suc))) (proj₁ ε-◎ _) (proj₂ distrib)) ⟩
      Σᴬ (λ j → F zero j ◎ Σ' (Π' I ∘ _ˢ_ (F ∘ suc)))
    ≈⟨ explore-mon-ext μA monoid (λ j → ≈-sym (explore-linˡ μF→A monoid _◎_ (Π' I ∘ _ˢ_ (F ∘ suc)) (F zero j) (proj₂ ε-◎ _) (proj₁ distrib))) ⟩
      (Σᴬ λ j → Σ' λ f → F zero j ◎ Π' I ((F ∘ suc) ˢ f))
    ∎

module _
  {{_ : Postulate-FinFunˢ-ok}}{{_ : UA}}{{_ : FunExt}} where

  FinDist : ∀ {n} → DistFun (μFin n) (λ μX → μFinFun μX)
  FinDist μB c ◎ distrib ◎-cong f = BigDistr.bigDistr μB c ◎ distrib ◎-cong f _

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
{-# OPTIONS --without-K -v 2 #-}
module Leftovers.Equality where

open import Leftovers.Utils
-- open import Leftovers.Leftovers

import Level as Level
-- open import Reflection
open import Reflection.Term
open import Reflection.Pattern as P
open import Reflection.TypeChecking.Monad.Instances

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary

open import Data.Unit
open import Data.Nat as Nat hiding (_⊓_)
open import Data.Bool
open import Data.Product
open import Data.List as List
open import Data.Char as Char
open import Data.String as String

open import Leftovers.Monad

import Data.List.Categorical
open Data.List.Categorical.TraversableM {m = Level.zero} leftoversMonad

--This file was adapted from https://github.com/alhassy/gentle-intro-to-reflection

open import Reflection.Show
import Data.Nat.Show as NShow

--Unify the goal with a function that does a case-split on an argument of the type with the given name
-- Return the metavariables, along with telescopes, for each branch
cases : Name → Term → Leftovers ⊤
cases typeName hole -- thm-you-hope-is-provable-by-refls
    = do
      -- let η = nom
      δ ← getDefinition typeName
      holeType ← inferType hole
      debugPrint "refl-cases" 2 (strErr " hole type to start " ∷ termErr holeType ∷ [])
      clauses ← forM (constructors δ) (mk-cls holeType)
      -- declareDef (vArg η) holeType
      let retFun = (pat-lam clauses [])
      normFun ← reduce retFun
      debugPrint "refl-cases" 2 (strErr "reflcases ret non-norm " ∷ termErr retFun ∷ [])
      unify hole normFun
      normHole ← reduce hole
      debugPrint "refl-cases" 2 (strErr "reflCases final " ∷ termErr normHole ∷ [])
    where
      -- For each constructor, generate the clause,
      -- along with the metavariable term for its right-hand side
      mk-cls : Type → Name → Leftovers (Clause )
      mk-cls holeType ctor =
         do
           debugPrint "mk-cls" 2 (strErr "mk-cls with ctor " ∷ nameErr ctor ∷ [])
           fullyApplied <- fully-applied-pattern ctor
           let
             patArgs = List.map CtorArg.pat fullyApplied
             patTerm = List.map CtorArg.term fullyApplied
             patTypes = List.map CtorArg.type fullyApplied
           extendContexts patTypes do
               debugPrint "" 2 (strErr "before retType " ∷ termErr holeType ∷ strErr "   and   " ∷ termErr (con ctor patTerm) ∷  [])
               retType ← returnTypeFor holeType (con ctor patTerm)
               debugPrint "mk-cls" 2 (strErr "retType is  " ∷ termErr retType ∷ [])
               -- Make the right-hand side in an extended context
               -- with new pattern-match variables
               rhs ← freshMeta retType
               let
                 teles =
                   List.map
                     (λ (x , n) → ( "arg" String.++ NShow.show n , x ))
                     (List.zip patTypes (List.upTo (List.length patTypes)))
               debugPrint "mk-cls" 2 (strErr "Pat" ∷ strErr (showPatterns patArgs) ∷ [] )
               let
                 ret =
                   (clause
                     teles
                     [ vArg (con ctor patArgs) ]
                     (rhs ⦂ retType))

               debugPrint "mk-cls" 2  (strErr "retClause" ∷ strErr (showClause ret) ∷ [])
               -- tryUnify rhs (con (quote refl) [])
               pure ret

-- ≡-type-info : Term → Leftovers (Arg Term × Arg Term × Term × Term)
-- ≡-type-info (def (quote _≡_) (𝓁 ∷ 𝒯 ∷ arg _ l ∷ arg _ r ∷ [])) = return (𝓁 , 𝒯 , l , r)
-- ≡-type-info _ = typeError [ strErr "Term is not a ≡-type." ]

-- {- If we have “f $ args” return “f”. -}
-- $-head : Term → Term
-- $-head (var v args) = var v []
-- $-head (con c args) = con c []
-- $-head (def f args) = def f []
-- $-head (pat-lam cs args) = pat-lam cs []
-- $-head t = t

-- import Agda.Builtin.Reflection as Builtin

-- _$-≟_ : Term → Term → Bool
-- con c args $-≟ con c′ args′ = Builtin.primQNameEquality c c′
-- def f args $-≟ def f′ args′ = Builtin.primQNameEquality f f′
-- var x args $-≟ var x′ args′ = does (x Nat.≟ x′)
-- _ $-≟ _ = false

-- {- Only gets heads and as much common args, not anywhere deep. :'( -}
-- infix 5 _⊓_
-- {-# TERMINATING #-} {- Fix this by adding fuel (con c args) ≔ 1 + length args -}
-- _⊓_ : Term → Term → Term
-- l ⊓ r with l $-≟ r | l | r
-- ...| false | x | y = unknown
-- ...| true | var f args | var f′ args′ = var f (List.zipWith (λ{ (arg i!! t) (arg j!! s) → arg i!! (t ⊓ s) }) args args′)
-- ...| true | con f args | con f′ args′ = con f (List.zipWith (λ{ (arg i!! t) (arg j!! s) → arg i!! (t ⊓ s) }) args args′)
-- ...| true | def f args | def f′ args′ = def f (List.zipWith (λ{ (arg i!! t) (arg j!! s) → arg i!! (t ⊓ s) }) args args′)
-- ...| true | ll | _ = ll {- Left biased; using ‘unknown’ does not ensure idempotence. -}

-- {- ‘unknown’ goes to a variable, a De Bruijn index -}
-- unknown-elim : ℕ → List (Arg Term) → List (Arg Term)
-- unknown-elim n [] = []
-- unknown-elim n (arg i unknown ∷ xs) = arg i (var n []) ∷ unknown-elim (n + 1) xs
-- unknown-elim n (arg i (var x args) ∷ xs) = arg i (var (n + suc x) args) ∷ unknown-elim n xs
-- unknown-elim n (arg i x ∷ xs)       = arg i x ∷ unknown-elim n xs
-- {- Essentially we want: body(unknownᵢ)  ⇒  λ _ → body(var 0)
--    However, now all “var 0” references in “body” refer to the wrong argument;
--    they now refer to “one more lambda away than before”. -}

-- unknown-count : List (Arg Term) → ℕ
-- unknown-count [] = 0
-- unknown-count (arg i unknown ∷ xs) = 1 + unknown-count xs
-- unknown-count (arg i _ ∷ xs) = unknown-count xs

-- unknown-λ : ℕ → Term → Term
-- unknown-λ zero body = body
-- unknown-λ (suc n) body = unknown-λ n (λv "section" ↦ body)

-- {- Replace ‘unknown’ with sections -}
-- patch : Term → Term
-- patch it@(def f args) = unknown-λ (unknown-count args) (def f (unknown-elim 0 args))
-- patch it@(var f args) = unknown-λ (unknown-count args) (var f (unknown-elim 0 args))
-- patch it@(con f args) = unknown-λ (unknown-count args) (con f (unknown-elim 0 args))
-- patch t = t

-- macro
--   spine : Term → Term → Leftovers ⊤
--   spine p goal =
--     do τ ← inferType p
--        _ , _ , l , r ← ≡-type-info τ
--        unify goal (patch (l ⊓ r))

-- macro
--   applyEq : Term → Term → Leftovers ⊤
--   applyEq p hole =
--     do
--        τ ← inferType hole
--        _ , _ , l , r ← ≡-type-info τ
--        unify hole ((def (quote cong) (vArg (patch (l ⊓ r)) ∷ vArg p ∷ [])))

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers