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

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

open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
import      LibraBFT.Concrete.Properties.Common        as Common
import      LibraBFT.Concrete.Properties.VotesOnce     as VO
open import LibraBFT.Impl.Consensus.Network            as Network
open import LibraBFT.Impl.Consensus.Network.Properties as NetworkProps
open import LibraBFT.Impl.Consensus.RoundManager
import      LibraBFT.Impl.Handle                       as Handle
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
open import LibraBFT.Impl.IO.OBM.Properties.InputOutputHandlers
open import LibraBFT.Impl.Handle.Properties
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open Invariants
open RoundManagerTransProps

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId

open        ParamsWithInitAndHandlers Handle.InitHandler.initAndHandlers
open        PeerCanSignForPK

open import LibraBFT.ImplShared.Util.HashCollisions Handle.InitHandler.initAndHandlers

open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms
                      Handle.InitHandler.initAndHandlers
                      PeerCanSignForPK PeerCanSignForPK-stable
open import LibraBFT.Impl.Handle.InitProperties
open        initHandlerSpec

-- This module contains definitions and lemmas used by proofs of the
-- implementation obligations for VotesOnce and PreferredRoundRule.

module LibraBFT.Impl.Properties.Common where

postulate -- TODO-3: prove (note: advanced; waiting on: `handle`)
  -- This will require updates to the existing proofs for the peer handlers. We
  -- will need to show that honest peers sign things only for their only PK, and
  -- that they either resend messages signed before or if sending a new one,
  -- that signature hasn't been sent before
  impl-sps-avp : StepPeerState-AllValidParts

open Structural impl-sps-avp

-- We can prove this easily for the Agda model because (unlike the Haskell
-- prototype) it does not yet do epoch changes, so only the initial EC is
-- relevant. Later, this will require us to use the fact that epoch changes
-- require proof of committing an epoch-changing transaction.
availEpochsConsistent :
   ∀{pid pid' v v' pk}{st : SystemState}
   → (pkvpf  : PeerCanSignForPK st v  pid  pk)
   → (pkvpf' : PeerCanSignForPK st v' pid' pk)
   → v ^∙ vEpoch ≡ v' ^∙ vEpoch
   → pcs4𝓔 pkvpf ≡ pcs4𝓔 pkvpf'
availEpochsConsistent (mkPCS4PK _ (inBootstrapInfo refl) _) (mkPCS4PK _ (inBootstrapInfo refl) _) refl = refl

postulate -- TODO-1: Prove (waiting on: complete definition of `initRM`)
  uninitQcs∈Bootstrap
    : ∀ {pid qc vs}{st : SystemState}
      → ReachableSystemState st
      → initialised st pid ≡ uninitd
      → qc QCProps.∈RoundManager (peerStates st pid)
      → vs ∈ qcVotes qc
      → ∈BootstrapInfo-impl fakeBootstrapInfo (proj₂ vs)

module ∈BootstrapInfoProps where
  sameSig∉ : ∀ {pk} {v v' : Vote}
             → (sig : WithVerSig pk v) (sig' : WithVerSig pk v')
             → ¬ ∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig)
             → ver-signature sig' ≡ ver-signature sig
             → ¬ ∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig')
  sameSig∉ _ _ ¬bootstrap ≡sig rewrite ≡sig = ¬bootstrap

-- Lemmas for `PeerCanSignForPK`
module PeerCanSignForPKProps where
  msb4 -- NOTE: This proof requires updating when we model epoch changes.
    : ∀ {pid v pk}{pre post : SystemState}
      → ReachableSystemState pre
      → Step pre post
      → PeerCanSignForPK post v pid pk
      → Meta-Honest-PK pk → (sig : WithVerSig pk v)
      → MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
      → PeerCanSignForPK pre v pid pk
  msb4 preach step (mkPCS4PK 𝓔@._ (inBootstrapInfo refl) (mkPCS4PKin𝓔 𝓔id≡ mbr nid≡ pk≡)) hpk sig mws∈pool =
    mkPCS4PK 𝓔 (inBootstrapInfo refl) (mkPCS4PKin𝓔 𝓔id≡ mbr nid≡ pk≡)

  msb4-eid≡
    : ∀ {pre post : SystemState} {v v' pid pk}
      → ReachableSystemState pre
      → Step pre post
      → Meta-Honest-PK pk
      → PeerCanSignForPK post v pid pk
      → v ≡L v' at vEpoch
      → (sig' : WithVerSig pk v')
      → MsgWithSig∈ pk (ver-signature sig') (msgPool pre)
      → PeerCanSignForPK pre v pid pk
  msb4-eid≡ rss step hpk pcsfpk ≡eid sig' mws' =
    peerCanSignEp≡ (msb4 rss step (peerCanSignEp≡ pcsfpk ≡eid) hpk sig' mws') (sym ≡eid)

  pidInjective
    : ∀ {pid pid' pk v v'}{st : SystemState}
      → PeerCanSignForPK st v  pid  pk
      → PeerCanSignForPK st v' pid' pk
      → v ^∙ vEpoch ≡ v' ^∙ vEpoch
      → pid ≡ pid'
  pidInjective{pid}{pid'}{pk} pcsfpk₁ pcsfpk₂ ≡epoch = begin
    pid         ≡⟨ sym (nid≡ (pcs4in𝓔 pcsfpk₁)) ⟩
    pcsfpk₁∙pid ≡⟨ PK-inj-same-ECs{pcs4𝓔 pcsfpk₁}{pcs4𝓔 pcsfpk₂}
                     (availEpochsConsistent pcsfpk₁ pcsfpk₂ ≡epoch) pcsfpk∙pk≡ ⟩
    pcsfpk₂∙pid ≡⟨ nid≡ (pcs4in𝓔 pcsfpk₂) ⟩
    pid'        ∎
    where
    open ≡-Reasoning
    open PeerCanSignForPKinEpoch
    open PeerCanSignForPK

    pcsfpk₁∙pid  = EpochConfig.toNodeId  (pcs4𝓔 pcsfpk₁) (mbr (pcs4in𝓔 pcsfpk₁))
    pcsfpk₂∙pid  = EpochConfig.toNodeId  (pcs4𝓔 pcsfpk₂) (mbr (pcs4in𝓔 pcsfpk₂))
    pcsfpk₁∙pk   = EpochConfig.getPubKey (pcs4𝓔 pcsfpk₁) (mbr (pcs4in𝓔 pcsfpk₁))
    pcsfpk₂∙pk   = EpochConfig.getPubKey (pcs4𝓔 pcsfpk₂) (mbr (pcs4in𝓔 pcsfpk₂))

    pcsfpk∙pk≡ : pcsfpk₁∙pk ≡ pcsfpk₂∙pk
    pcsfpk∙pk≡ = begin
      pcsfpk₁∙pk ≡⟨ pk≡ (pcs4in𝓔 pcsfpk₁) ⟩
      pk         ≡⟨ sym (pk≡ (pcs4in𝓔 pcsfpk₂)) ⟩
      pcsfpk₂∙pk ∎

module ReachableSystemStateProps where
  mws∈pool⇒initd
    : ∀ {pid pk v}{st : SystemState}
    → ReachableSystemState st
    → PeerCanSignForPK st v pid pk
    → Meta-Honest-PK pk
    → (sig : WithVerSig pk v)
    → ¬ (∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig))
    → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
    → initialised st pid ≡ initd

  mws∈pool⇒initd{pk = pk}{v} (step-s{pre = pre} rss step@(step-peer sp@(step-cheat cmc))) pcsfpk hpk sig ¬bootstrap mws∈pool =
    peersRemainInitialized step (mws∈pool⇒initd rss (PeerCanSignForPKProps.msb4 rss step pcsfpk hpk sig mws∈poolPre) hpk sig ¬bootstrap mws∈poolPre)
    where
    ¬bootstrap' = ∈BootstrapInfoProps.sameSig∉ sig (msgSigned mws∈pool) ¬bootstrap (msgSameSig mws∈pool)

    mws∈poolPre : MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
    mws∈poolPre = ¬cheatForgeNew sp refl unit hpk mws∈pool ¬bootstrap'

  mws∈pool⇒initd{pid₁}{pk = pk} (step-s{pre = pre} rss step@(step-peer sp@(step-honest{pid₂} sps@(step-init {rm} rm×acts uni)))) pcsfpk hpk sig ¬bootstrap mws∈pool
     with pid₁ ≟ pid₂
  ...| yes refl = StepPeer-post-lemma2 {pre = pre} sps
  ...| no neq
     with newMsg⊎msgSentB4 rss sps hpk (msgSigned mws∈pool) ¬bootstrap' (msg⊆ mws∈pool) (msg∈pool mws∈pool)
     where
     ¬bootstrap' = ∈BootstrapInfoProps.sameSig∉ sig (msgSigned mws∈pool) ¬bootstrap (msgSameSig mws∈pool)
  ...| Right mws∈poolPre = peersRemainInitialized step (mws∈pool⇒initd rss (PeerCanSignForPKProps.msb4 rss step pcsfpk hpk sig mws∈poolPre') hpk sig ¬bootstrap mws∈poolPre')
     where
     mws∈poolPre' : MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
     mws∈poolPre' rewrite msgSameSig mws∈pool = mws∈poolPre
  ...| Left (send∈acts , _ , _)
     with initHandlerSpec.contract pid₂ fakeBootstrapInfo rm×acts
  ...| init-contract
     with msg⊆ mws∈pool
  ...| vote∈vm
     = ⊥-elim
       (P≢V (sym (proj₁ (proj₂ (initHandlerSpec.ContractOk.isInitPM init-contract send∈acts)))))
  ...| vote∈qc vs∈qc _ qc∈pm
     with initHandlerSpec.ContractOk.isInitPM init-contract send∈acts
  ...| (_ , refl , noSigs) = ⊥-elim (noSigs vs∈qc qc∈pm)

  mws∈pool⇒initd{pid₁}{pk}{v} (step-s{pre = pre} rss step@(step-peer{pid₂} sp@(step-honest sps@(step-msg _ ini)))) pcsfpk hpk sig ¬bootstrap mws∈pool
     with newMsg⊎msgSentB4 rss sps hpk (msgSigned mws∈pool) ¬bootstrap' (msg⊆ mws∈pool) (msg∈pool mws∈pool)
     where
     ¬bootstrap' = ∈BootstrapInfoProps.sameSig∉ sig (msgSigned mws∈pool) ¬bootstrap (msgSameSig mws∈pool)
  ...| Left (m∈outs , pcsfpk' , ¬msb4)
     with pid≡
     where
     vd₁≡vd₂ : v ≡L msgPart mws∈pool at vVoteData
     vd₁≡vd₂ = either (⊥-elim ∘ PerReachableState.meta-no-collision rss) id (sameSig⇒sameVoteData (msgSigned mws∈pool) sig (msgSameSig mws∈pool))

     pid≡ : pid₁ ≡ pid₂
     pid≡ = PeerCanSignForPKProps.pidInjective pcsfpk pcsfpk' (cong (_^∙ vdProposed ∙ biEpoch) vd₁≡vd₂)
  ...| refl rewrite StepPeer-post-lemma2{pid₂}{pre = pre} sps = refl

  mws∈pool⇒initd{pid₁}{pk}  (step-s{pre = pre} rss step@(step-peer{pid₂} sp@(step-honest sps@(step-msg _ ini)))) pcsfpk hpk sig ¬bootstrap mws∈pool | Right mws∈poolPre =
    peersRemainInitialized step (mws∈pool⇒initd rss (PeerCanSignForPKProps.msb4 rss step pcsfpk hpk sig mws∈poolPre') hpk sig ¬bootstrap mws∈poolPre')
    where
    mws∈poolPre' : MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
    mws∈poolPre' rewrite msgSameSig mws∈pool = mws∈poolPre

  mws∈pool⇒epoch≡
    : ∀ {pid v s' outs pk}{st : SystemState}
      → ReachableSystemState st
      → (sps : StepPeerState pid (msgPool st) (initialised st) (peerStates st pid) (s' , outs))
      → PeerCanSignForPK st v pid pk
      → Meta-Honest-PK pk → (sig : WithVerSig pk v)
      → ¬ (∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig))
      → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
      → s' ^∙ rmEpoch ≡ v ^∙ vEpoch
      → peerStates st pid ^∙ rmEpoch ≡ v ^∙ vEpoch
  mws∈pool⇒epoch≡ rss (step-init _ uni) pcsfpk hpk sig ¬bootstrap mws∈pool epoch≡ =
    absurd (uninitd ≡ initd) case (trans (sym uni) ini) of λ ()
    where
    ini = mws∈pool⇒initd rss pcsfpk hpk sig ¬bootstrap mws∈pool
  mws∈pool⇒epoch≡{pid}{v}{st = st} rss (step-msg{_ , P pm} m∈pool ini) pcsfpk hpk sig ¬bootstrap mws∈pool epoch≡ = begin
    hpPre ^∙ rmEpoch ≡⟨ noEpochChange ⟩
    hpPos ^∙ rmEpoch ≡⟨ epoch≡ ⟩
    v ^∙ vEpoch      ∎
    where
    hpPool = msgPool st
    hpPre  = peerStates st pid
    hpPos  = LBFT-post (handleProposal 0 pm) hpPre

    open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm hpPool hpPre)
    open ≡-Reasoning

  mws∈pool⇒epoch≡{pid}{v}{st = st} rss (step-msg{sndr , V vm} _ _) pcsfpk hpk sig ¬bootstrap mws∈pool epoch≡ = begin
    hvPre ^∙ rmEpoch ≡⟨ noEpochChange ⟩
    hvPos ^∙ rmEpoch ≡⟨ epoch≡ ⟩
    v ^∙ vEpoch      ∎
    where
    hvPre = peerStates st pid
    hvPos = LBFT-post (handleVote 0 vm) hvPre

    open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool st) hvPre)
    open ≡-Reasoning

  mws∈pool⇒epoch≡{pid}{v}{st = st} rss (step-msg{sndr , C cm} _ _) pcsfpk hpk sig ¬bootstrap mws∈pool epoch≡ = epoch≡


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst; setoid)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
import Function.Equality
open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian
import Categories.Category.Construction.Functors
import Categories.Category.Product
import Categories.NaturalTransformation
import Categories.NaturalTransformation.NaturalIsomorphism

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.RelativeMonadMorphism
import SecondOrder.Instantiation
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli
import SecondOrder.Mslot

module SecondOrder.MRelativeMonad
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  open SecondOrder.Mslot Σ
  open SecondOrder.Substitution Σ
  open SecondOrder.Instantiation Σ
  open import SecondOrder.RelativeMonadMorphism
  open Categories.Category
  open Categories.Functor using (Functor)
  open Categories.NaturalTransformation renaming (id to idNt)
  open Categories.NaturalTransformation.NaturalIsomorphism renaming (refl to reflNt; sym to symNt; trans to transNt)
  open Categories.Category.Construction.Functors
  open Categories.Category.Instance.Setoids
  open Categories.Category.Product
  open Function.Equality using () renaming (setoid to Π-setoid)
  open SecondOrder.IndexedCategory
  -- open import SecondOrder.RelativeKleisli

  module MTerm {Γ : VContext} where
    open Category
    open NaturalTransformation
    open Functor
    open Categories.Monad.Relative
    open Function.Equality using () renaming (setoid to Π-setoid)
    open Categories.Category.Equivalence using (StrongEquivalence)
    open SecondOrder.RelativeKleisli

    MMonad : Monad Mslots
    MMonad =
      let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
      record
      { F₀ = λ Θ A →
           record
           { F₀ = λ Ψ → record
                          { F₀ = λ Δ → Term-setoid (Θ ,, Ψ) (Γ ,, Δ) A
                          ; F₁ = λ {Δ} {Ξ} ρ → record { _⟨$⟩_ = [_]ᵛ_ (ʳ⇑ᵛ ρ) ; cong = λ t≈s → []ᵛ-resp-≈ t≈s }
                          ; identity = λ t≈s → ≈-trans ([]ᵛ-resp-≡ᵛ idᵛ+idᵛ) (≈-trans [idᵛ] t≈s)
                          ; homomorphism = λ t≈s → ≈-trans ([]ᵛ-resp-≈ t≈s) ∘ᵛ-resp-ʳ⇑ᵛ-term
                          ; F-resp-≈ = λ ρ≈τ t≈s → {!!}
                          }
           ; F₁ = λ ι → record
                         { η = λ Δ → record { _⟨$⟩_ = [_]ᵐ_ (ᵐ⇑ᵐ ι) ; cong = λ t≈s → []ᵐ-resp-≈ t≈s }
                         ; commute = λ ρ t≈s → ≈-trans ([]ᵐ-resp-≈ ([]ᵛ-resp-≈ t≈s)) vr-comm-mr
                         ; sym-commute = λ ρ t≈s → ≈-trans (≈-sym vr-comm-mr) ([]ᵐ-resp-≈ ([]ᵛ-resp-≈ t≈s))
                         }
           ; identity = λ t≈s → ≈-trans ([]ᵐ-resp-≈ t≈s) (≈-trans ([]ᵐ-resp-≡ᵐ ᵐ⇑ᵐ-resp-idᵐ) [idᵐ])
           ; homomorphism = λ t≈s → ≈-trans ([]ᵐ-resp-≈ t≈s) ∘ᵐ-resp-ᵐ⇑-term
           ; F-resp-≈ = λ ι≈μ t≈s → ≈-trans ([]ᵐ-resp-≈ t≈s) ([]ᵐ-resp-≡ᵐ (ᵐ⇑ᵐ-resp-≡ᵐ ι≈μ))
           }
      ; unit = λ A → record
                      { η = λ Θ →
                          record
                          { η = λ Δ → record { _⟨$⟩_ = [_]ᵛ_ inrᵛ ; cong = λ t≈s → []ᵛ-resp-≈ t≈s }
                          ; commute = λ ρ t≈s → ≈-trans ([]ᵛ-resp-≈ ([]ᵛ-resp-≈ t≈s)) (≈-sym ʳ⇑ᵛ-comm-inrᵛ-term)
                          ; sym-commute = λ ρ t≈s → ≈-trans ʳ⇑ᵛ-comm-inrᵛ-term ([]ᵛ-resp-≈ ([]ᵛ-resp-≈ t≈s))
                          }
                      ; commute = λ f t≈s → ≈-trans ([]ᵛ-resp-≈ ([]ᵐ-resp-≈ t≈s)) mr-comm-vr
                      ; sym-commute = λ f t≈s → ≈-trans ? ([]ᵛ-resp-≈ ([]ᵐ-resp-≈ t≈s))
                      }
      ; extend = λ I A → record
                          { η = λ Θ →
                              record
                              { η = λ Ψ → record { _⟨$⟩_ = [_]ⁱ_ {!!} ; cong = {!!} }
                              ; commute = {!!}
                              ; sym-commute = {!!}
                              }
                          ; commute = {!!}
                          ; sym-commute = {!!}
                          }
      ; identityʳ = {!!}
      ; identityˡ = {!!}
      ; assoc = {!!}
      ; extend-≈ = {!!}
      }

ext: agda

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module Tactic.Monoid.Exp where

open import Prelude
open import Tactic.Reflection.Quote
open import Tactic.Deriving.Quotable

data Exp : Set where
  var : Nat → Exp
  ε : Exp
  _⊕_ : Exp → Exp → Exp

unquoteDecl QuoteExp = deriveQuotable QuoteExp (quote Exp)

flatten : Exp → List Nat
flatten (var x) = x ∷ []
flatten ε = []
flatten (e ⊕ e₁) = flatten e ++ flatten e₁

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module cry.gfp where

-- open import Agda.Primitive using (lsuc; _⊔_)
open import Level

-- import Agda.Builtin.FromNat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Algebra.FunctionProperties.Core using (Op₁; Op₂)
open import Relation.Nullary
-- open import Relation.Binary.Core using (Rel; Decidable; Substitutive)
-- open import Relation.Binary.PropositionalEquality.Core using (subst)
Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = A → A → Set ℓ
Decidable : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)
_Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → Rel A ℓ₂ → Set _
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y
Substitutive : ∀ {a ℓ₁} {A : Set a} → Rel A ℓ₁ → (ℓ₂ : Level) → Set _
Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_

subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p
subst P refl p = p

record RawField c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  10 _⁻¹
  infix  9 -_
  infixl 8 _²
  infixl 7 _*_
  infixl 6 _+_ _-_
  infix  4 _≈_ _≈?_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _≈?_    : Decidable _≈_
    _?≈_    : Carrier → Carrier → Bool
    _+_     : Op₂ Carrier
    _-_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    _²      : Op₁ Carrier
    -_      : Op₁ Carrier
    _⁻¹     : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier

open import Agda.Builtin.Nat as N using () renaming (Nat to ℕ)

_mod_ : (dividend divisor : ℕ) → ℕ
(d mod 0) = 0
(d mod N.suc s) = N.mod-helper 0 s d s

_div_ : (dividend divisor : ℕ) → ℕ
(d div 0) = 0
(d div N.suc s) = N.div-helper 0 s d s

{-# TERMINATING #-}
times : ∀ {a} {A : Set a} →
  (one : A) (dbl : A → A) (add : A → A → A) →
  A → ℕ → A
times {A = A} one dbl add = mul where
  mul : A → ℕ → A
  f : A → ℕ → A
  -- f u n = uⁿ
  g : A → A → ℕ → A
  -- g t u n = uⁿ t

  mul x 0 = one
  mul x n = f x n

  f u 1 = u
  f u n with n mod 2
  ... | 0 = f (dbl u) (n div 2)
  ... | _ = g u (dbl u) ((n N.- 1) div 2)

  g t u 1 = add t u
  g t u n with n mod 2
  ... | 0 = g t (dbl u) (n div 2)
  ... | _ = g (add t u) (dbl u) ((n N.- 1) div 2)

module 𝔽ₚ (p : ℕ) where
    𝔽 : Set
    𝔽 = ℕ

    to𝔽 : ℕ → 𝔽
    to𝔽 i = i mod p

    _==_ : 𝔽 → 𝔽 → Set
    x == y = x ≡ y

    open N using (zero; suc)
    pred : ℕ → ℕ
    pred zero = 0
    pred (suc n) = n

    _≟_ : (x y : 𝔽) → Dec (x == y)
    zero  ≟ zero   = yes refl
    suc m ≟ suc n  with m ≟ n
    suc m ≟ suc .m | yes refl = yes refl
    suc m ≟ suc n  | no prf   = no λ x → prf ((λ p → subst (λ x → m ≡ pred x) p refl) x)
    zero  ≟ suc n  = no λ()
    suc m ≟ zero   = no λ()

    infix  10 _⁻¹
    infix  9 -_
    infixl 8 _²
    infixl 7 _*_
    infixl 6 _+_ _-_

    _+_ : 𝔽 → 𝔽 → 𝔽
    n + m = to𝔽 (n N.+ m)

    _*_ : 𝔽 → 𝔽 → 𝔽
    n * m = to𝔽 (n N.* m)

    _² : 𝔽 → 𝔽
    x ² = x * x

    -_ : 𝔽 → 𝔽
    - 0 = 0
    - N.suc n = (p N.- N.suc n)

    _-_ : 𝔽 → 𝔽 → 𝔽
    x - y = x + (- y)

    0# : 𝔽
    0# = 0

    1# : 𝔽
    1# = 1

    _^_ : 𝔽 → ℕ → 𝔽
    _^_ = times 1# _² _*_

    _⁻¹ : 𝔽 → 𝔽
    x ⁻¹ = x ^ (p N.- 2)

gfp : ℕ → RawField _ _
gfp p = record
  { Carrier = 𝔽
  ; _≈_ = _==_
  ; _≈?_ = _≟_
  ; _?≈_ = N._==_
  ; _+_ = _+_
  ; _-_ = _-_
  ; _*_ = _*_
  ; _² = _²
  ; -_ = -_
  ; _⁻¹ = _⁻¹
  ; 0# = 0#
  ; 1# = 1#
  } where open 𝔽ₚ p

max_stars_repo_name: semenov-vladyslav/cry-agda

max_issues_repo_name: semenov-vladyslav/cry-agda

max_forks_repo_name: semenov-vladyslav/cry-agda


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

module Fragment.Examples.Semigroup.Types where

open import Fragment.Prelude

open import Level using (zero)

open import Function.Related
open import Function.Related.TypeIsomorphisms
  using (×-isSemigroup; ⊎-isSemigroup)
open import Function.Inverse using (_↔_)

open import Data.Product using (_×_)
open import Data.Sum using (_⊎_)

×-semigroup = semigroup→model (×-isSemigroup bijection zero)
⊎-semigroup = semigroup→model (⊎-isSemigroup bijection zero)

×-assoc₁ : ∀ {A B C : Set} → (A × (B × C)) ↔ ((A × B) × C)
×-assoc₁ = fragment SemigroupFrex ×-semigroup

×-assoc₂ : ∀ {A B C : Set} → ((A × B) × (B × C)) ↔ (A × (B × B) × C)
×-assoc₂ = fragment SemigroupFrex ×-semigroup

⊎-assoc₁ : ∀ {A B C : Set} → (A ⊎ (B ⊎ C)) ↔ ((A ⊎ B) ⊎ C)
⊎-assoc₁ = fragment SemigroupFrex ⊎-semigroup

⊎-assoc₂ : ∀ {A B C : Set} → ((A ⊎ B) ⊎ (B ⊎ C)) ↔ (A ⊎ (B ⊎ B) ⊎ C)
⊎-assoc₂ = fragment SemigroupFrex ⊎-semigroup

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module QuoteTerm where

open import Common.Reflection
open import Common.Prelude renaming (Nat to ℕ; module Nat to ℕ)

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

test₁ : quoteTerm (λ {A : Set} (x : A) → x)
         ≡ lam hidden (abs "A" (lam visible (abs "x" (var 0 []))))
test₁ = refl

-- Local variables are de Bruijn indices, do not forget to shift
test₂ : (λ {A : Set} (x : A) → quoteTerm x) ≡ (λ x → var 0 [])
test₂ = refl

-- Terms are not normalized before being unquoted
test₃ : quoteTerm (1 + 1) ≡ lit (nat 2) → ⊥
test₃ ()

syntax id A x = x ∶ A
id : (A : Set) → A → A
id A x = x

-- _∶_ from the Function module can help in case of ambiguities
test₄ : quoteTerm (zero ∶ ℕ) ≡
        def (quote id)
            (vArg (def (quote ℕ) []) ∷
             vArg (con (quote zero) []) ∷
             [])
test₄ = refl

-- Andreas, 2020-06-05, issue #4734
-- Test that primShowQName prints something reasonable
-- for quoted names.

issue4734 : primShowQName (quote ℕ) ≡ "Agda.Builtin.Nat.ℕ"
issue4734 = refl

-- Not sure this response is very reasonable, since
-- it suggest a qualified name that does not exist.

max_stars_repo_name: pnlph/agda

max_issues_repo_name: pnlph/agda

max_forks_repo_name: pnlph/agda


text:
record ⊤ : Set where
  instance constructor tt

data ⊥ : Set where

data Inf : Set where
  -∞ ∞ : Inf

Less : Inf → Inf → Set
Less ∞ _ = ⊥
Less _ ∞ = ⊤
Less _ _ = ⊥

data Bounded : Inf → Set where
  bound : ∀ {b} {{lt : Less -∞ b}} → Bounded b

-- The first time around the target type is Less -∞ _b which results in no
-- candidates. Once _b gets solved candidates need to be recomputed.
foo : Bounded ∞
foo = bound

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates indexed binary structures at an index to the equivalent
-- non-indexed structures.
------------------------------------------------------------------------

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

module Relation.Binary.Indexed.Heterogeneous.Construct.At where

open import Relation.Binary
open import Relation.Binary.Indexed.Heterogeneous
  hiding (IsEquivalence; Setoid)

------------------------------------------------------------------------
-- Structures

module _ {a i} {I : Set i} {A : I → Set a} where

  isEquivalence : ∀ {ℓ} {_≈_ : IRel A ℓ} → IsIndexedEquivalence A _≈_ →
                  (index : I) → IsEquivalence (_≈_ {index})
  isEquivalence isEq index = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
    where open IsIndexedEquivalence isEq

  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_∼_ : IRel A ℓ₂} →
               IsIndexedPreorder A _≈_ _∼_ →
               (index : I) → IsPreorder (_≈_ {index}) _∼_
  isPreorder isPreorder index = record
    { isEquivalence = isEquivalence O.isEquivalence index
    ; reflexive     = O.reflexive
    ; trans         = O.trans
    }
    where module O = IsIndexedPreorder isPreorder

------------------------------------------------------------------------
-- Packages

module _ {a i} {I : Set i} where

  setoid : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
  setoid S index = record
    { Carrier       = S.Carrier index
    ; _≈_           = S._≈_
    ; isEquivalence = isEquivalence S.isEquivalence index
    }
    where module S = IndexedSetoid S

  preorder : ∀ {ℓ₁ ℓ₂} → IndexedPreorder I a ℓ₁ ℓ₂ → I → Preorder a ℓ₁ ℓ₂
  preorder O index = record
    { Carrier    = O.Carrier index
    ; _≈_        = O._≈_
    ; _∼_        = O._∼_
    ; isPreorder = isPreorder O.isPreorder index
    }
    where module O = IndexedPreorder O

------------------------------------------------------------------------
-- Some useful shorthand infix notation

module _ {a i} {I : Set i} where

  _atₛ_ : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
  _atₛ_ = setoid


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

data E (@0 A : Set) : Set where
  c₁ c₂ : A → E A
  @0 c₃ : A → E A


text:
module Relation.Ternary.Separation.Monad.Update where

open import Level hiding (Lift)
open import Function using (_∘_; case_of_)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Unary
open import Relation.Unary.PredicateTransformer hiding (_⊔_; [_])
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Monad

open import Data.Unit
open import Data.Product

module _ {a} {A : Set a} {{s : RawSep A}} {u} {{s : IsUnitalSep s u}} where
  instance
    ⤇-monad : Monad {I = ⊤} (λ _ _ → ⤇ {p = a})
    Monad.return ⤇-monad px   = local λ σ → -, -, σ , px
    app (Monad.bind ⤇-monad f) p σₚ = local λ fr →
      let
        _ , σ₁ , σ₂ = ⊎-assoc (⊎-comm σₚ) fr
        Δ , Σ , σ₃ , px = update p σ₁
        _ , σ₄ , σ₅ = ⊎-unassoc σ₃ σ₂
      in update (app f px (⊎-comm σ₄)) σ₅


text:
module Scratch.Data.List.Relation.Helpers where

open import Relation.Nullary
open import Relation.Nullary.Decidable

open import Relation.Unary
open import Relation.Binary hiding (Decidable)

open import Data.Product

open import Data.List.Base
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.All.Properties
open import Data.List.Relation.Unary.AllPairs

module _ {a ℓ ℓ₁ ℓ₂} {A : Set a}
         {R : Rel A ℓ₁} {S : Rel A ℓ₂}
         {P : Pred A ℓ} (P? : Decidable P) where

  filter⁺⁺ : ∀ {xs} → (∀ {x y} → P x → P y → R x y → S x y) →
            AllPairs R xs → AllPairs S (filter P? xs)
  filter⁺⁺ {[]} _ _ = []
  filter⁺⁺ {x ∷ xs} Δ (h ∷ t) with (P? x)
  ... | yes p = let
                  hf : All (R x) (filter P? xs)
                  hf = filter⁺ P? h
                  ap : All P (filter P? xs)
                  ap = all-filter P? xs
                  w : All (P ∩ R x) (filter P? xs)
                  w = All.zip ( ap , hf )
                  y : P ∩ R x ⊆ S x
                  y = λ z → Δ p (proj₁ z) (proj₂ z)
                  z : All (S x) (filter P? xs)
                  z =  All.map y w
                in z ∷ filter⁺⁺ {xs} Δ t
  ... | no  ¬p = filter⁺⁺ {xs} Δ t

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Functor.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

record Functor (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
  no-eta-equality
  open Precategory

  field
    F-ob : C .ob → D .ob
    F-hom : {x y : C .ob} → C [ x , y ] → D [(F-ob x) , (F-ob y)]
    F-id : {x : C .ob} → F-hom (C .id x) ≡ D .id (F-ob x)
    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ]) → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)

  isFull = (x y : _) (F[f] : D [(F-ob x) , (F-ob y)]) → ∃ (C [ x , y ]) (λ f → F-hom f ≡ F[f])
  isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g
  isEssentiallySurj = ∀ (d : D .ob) → Σ[ c ∈ C .ob ] CatIso {C = D} (F-ob c) d

private
  variable
    ℓ ℓ' : Level
    C D E : Precategory ℓ ℓ'

open Precategory
open Functor

-- Helpful notation

-- action on objects
infix 30 _⟅_⟆
_⟅_⟆ : (F : Functor C D)
     → C .ob
     → D .ob
_⟅_⟆ = F-ob

-- action on morphisms
infix 30 _⟪_⟫ -- same infix level as on objects since these will never be used in the same context
_⟪_⟫ : (F : Functor C D)
     → ∀ {x y}
     → C [ x , y ]
     → D [(F ⟅ x ⟆) , (F ⟅ y ⟆)]
_⟪_⟫ = F-hom

-- Functor constructions

𝟙⟨_⟩ : ∀ (C : Precategory ℓ ℓ') → Functor C C
𝟙⟨ C ⟩ .F-ob x = x
𝟙⟨ C ⟩ .F-hom f = f
𝟙⟨ C ⟩ .F-id = refl
𝟙⟨ C ⟩ .F-seq _ _ = refl

-- functor composition
funcComp : ∀ (G : Functor D E) (F : Functor C D) → Functor C E
(funcComp G F) .F-ob c = G ⟅ F ⟅ c ⟆ ⟆
(funcComp G F) .F-hom f = G ⟪ F ⟪ f ⟫ ⟫
(funcComp {D = D} {E = E} {C = C} G F) .F-id {c}
  = (G ⟪ F ⟪ C .id c ⟫ ⟫)
  ≡⟨ cong (G ⟪_⟫) (F .F-id) ⟩
    G .F-id
  --   (G ⟪ D .id (F ⟅ c ⟆) ⟫) -- deleted this cause the extra refl composition was annoying
  -- ≡⟨ G .F-id ⟩
  --   E .id (G ⟅ F ⟅ c ⟆ ⟆)
  -- ∎
(funcComp {D = D} {E = E} {C = C} G F) .F-seq {x} {y} {z} f g
  = (G ⟪ F ⟪ f ⋆⟨ C ⟩ g ⟫ ⟫)
  ≡⟨ cong (G ⟪_⟫) (F .F-seq _ _) ⟩
    G .F-seq _ _
  --   (G ⟪ (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) ⟫) -- deleted for same reason as above
  -- ≡⟨ G .F-seq _ _ ⟩
  --   (G ⟪ F ⟪ f ⟫ ⟫) ⋆⟨ E ⟩ (G ⟪ F ⟪ g ⟫ ⟫)
  -- ∎

infixr 30 funcComp
syntax funcComp G F = G ∘F F

_^opF : Functor C D → Functor (C ^op) (D ^op)
(F ^opF) .F-ob = F .F-ob
(F ^opF) .F-hom = F .F-hom
(F ^opF) .F-id = F .F-id
(F ^opF) .F-seq f g = F .F-seq g f

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module 14-implicitConfigurations where

postulate
  Integral : Set → Set
  add : ∀ {A} {{ intA : Integral A }} → A → A → A
  mul : ∀ {A} {{ intA : Integral A }} → A → A → A
  mod : ∀ {A} {{ intA : Integral A }} → A → A → A

  N : Set
  zero one two three : N
  nInt : Integral N

private postulate Token : Set

record Modulus (s : Token) (A : Set) : Set where
  field modulus : A

data M (s : Token) (A : Set) : Set where
  MkM : A → M s A

unMkM : ∀ {A s} → M s A → A
unMkM (MkM a) = a

private postulate theOnlyToken : Token

withModulus :
  ∀ {A} → {{ intA : Integral A }} → (modulus : A) →
  (∀ {s} → {{ mod : Modulus s A }} → M s A) → A
withModulus modulus f = unMkM
  (f {theOnlyToken} {{  record { modulus = modulus }  }})

open Modulus {{...}}

normalize : ∀ {s A} {{intA : Integral A}} {{mod : Modulus s A}} →
            A → M s A
normalize a = MkM (mod modulus a)

_+_ : ∀ {s A} {{intA : Integral A}} {{mod : Modulus s A}} →
      M s A → M s A → M s A
(MkM a) + (MkM b) = normalize (add a b)

_*_ : ∀ {s A} → {{intA : Integral A}} → {{mod : Modulus s A}} →
      M s A → M s A → M s A
(MkM a) * (MkM b) = normalize (mul a b)

test₁ : N
test₁ = withModulus two (let o = MkM one in (o + o)*(o + o))

testExpr : ∀ {s} → {{mod : Modulus s N}} → M s N
testExpr = let o = MkM one ; t = MkM two in
           (o + t) * t

test₂ : N
test₂ = withModulus three testExpr

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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.RustAnyHow
open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block                as Block
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert           as QuorumCert
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote                 as Vote
import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteData             as VoteData
import      LibraBFT.Impl.Consensus.SafetyRules.PersistentSafetyStorage as PersistentSafetyStorage
import      LibraBFT.Impl.OBM.Crypto                                    as Crypto
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.BlockInfo                               as BlockInfo
import      LibraBFT.Impl.Types.EpochChangeProof                        as EpochChangeProof
import      LibraBFT.Impl.Types.ValidatorSigner                         as ValidatorSigner
import      LibraBFT.Impl.Types.ValidatorVerifier                       as ValidatorVerifier
open import LibraBFT.Impl.Types.Verifier
import      LibraBFT.Impl.Types.Waypoint                                as Waypoint
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
import      LibraBFT.ImplShared.Util.Crypto                             as Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                                 using (String)
------------------------------------------------------------------------------

module LibraBFT.Impl.Consensus.SafetyRules.SafetyRules where

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

new : PersistentSafetyStorage → Bool → Either ErrLog SafetyRules
new persistentStorage exportConsensusKey = do
  pure $ mkSafetyRules
    persistentStorage
    exportConsensusKey
    nothing
    nothing

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

signer : SafetyRules → Either ErrLog ValidatorSigner
signer self = maybeS (self ^∙ srValidatorSigner) (Left fakeErr {- error: signer not initialized -}) Right

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

extensionCheck : VoteProposal → Either ErrLog VoteData
extensionCheck voteProposal = do
  let proposedBlock = voteProposal ^∙ vpBlock
      obmAEP        = voteProposal ^∙ vpAccumulatorExtensionProof
  -- IMPL-TODO: verify .accumulator_extension_proof().verify ...
   in pure
     (VoteData.new
       (Block.genBlockInfo
         proposedBlock
         -- OBM-LBFT-DIFF: completely different
         (Crypto.obmHashVersion (obmAEP ^∙ aepObmNumLeaves))
         (obmAEP ^∙ aepObmNumLeaves)
         (voteProposal ^∙ vpNextEpochState))
       (proposedBlock ^∙ bQuorumCert ∙ qcCertifiedBlock))

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

constructLedgerInfoM : Block → HashValue → LBFT (Either ErrLog LedgerInfo)
constructLedgerInfoM proposedBlock consensusDataHash = do
  let block2 = proposedBlock ^∙ bRound
      block1 = proposedBlock ^∙ bQuorumCert ∙ qcCertifiedBlock ∙ biRound
      block0 = proposedBlock ^∙ bQuorumCert ∙ qcParentBlock ∙ biRound
      commit = (block0 + 1 == block1) ∧ (block1 + 1 == block2)
  commitInfo ←
    if commit
    then (do
      let c = proposedBlock ^∙ bQuorumCert ∙ qcParentBlock
      logInfo fakeInfo -- lSR (Info3ChainDetected proposedBlock c)
      pure c)
    else
      pure BlockInfo.empty
  ok (LedgerInfo∙new commitInfo consensusDataHash)

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

-- PREFERRED ROUND RULE (2nd VOTING RULE) : this avoids voting to commit a conflicting Block
verifyAndUpdatePreferredRoundM : QuorumCert → SafetyData → LBFT (Either ErrLog SafetyData)
verifyAndUpdatePreferredRoundM quorumCert safetyData = do
  let preferredRound = safetyData ^∙ sdPreferredRound
      oneChainRound  = quorumCert ^∙ qcCertifiedBlock ∙ biRound
      twoChainRound  = quorumCert ^∙ qcParentBlock ∙ biRound
  -- LBFT-ALGO v3:p6: "... votes in round k only if the QC inside the k proposal
  -- is at least" PreferredRound."
  ifD oneChainRound <? preferredRound
    then bail fakeErr -- error: incorrect preferred round, QC round does not match preferred round
    else do
      updated ← case (compare twoChainRound preferredRound) of λ where
          GT → do
            logInfo fakeInfo -- updated preferred round
            pure (safetyData & sdPreferredRound ∙~ twoChainRound)
          LT → do
            logInfo fakeInfo  -- 2-chain round is lower than preferred round, but 1-chain is higher
            pure safetyData
          EQ →
            pure safetyData
      ok updated

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

verifyAuthorM : Maybe Author → LBFT (Either ErrLog Unit)
verifyAuthorM author = do
  vs ← use (lSafetyRules ∙ srValidatorSigner)
  maybeS vs (bail fakeErr) {-(ErrL (here' ["srValidatorSigner", "Nothing"]))-} $ λ validatorSigner →
    maybeSD
      author
      (bail fakeErr) -- (ErrL (here' ["InvalidProposal", "No author found in the proposal"])))
      (\a ->
        ifD validatorSigner ^∙ vsAuthor /= a
        then bail fakeErr -- (ErrL (here' ["InvalidProposal", "Proposal author is not validator signer"]))
        else ok unit)
 where
  here' : List String → List String
  here' t = "SafetyRules" ∷ "verifyAuthorM" ∷ t

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

verifyEpochM : Epoch → SafetyData → LBFT (Either ErrLog Unit)
verifyEpochM epoch safetyData =
  ifD epoch /= safetyData ^∙ sdEpoch
    then bail fakeErr -- incorrect epoch
    else ok unit

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

-- INCREASING ROUND RULE (1st VOTING RULE) : ensures voting only ONCE per round
verifyAndUpdateLastVoteRoundM : Round → SafetyData → LBFT (Either ErrLog SafetyData)
verifyAndUpdateLastVoteRoundM round safetyData =
  -- LBFT-ALGO v3:p6 : "... votes in round k it if is higher than" LastVotedRound
  ifD round >? (safetyData ^∙ sdLastVotedRound)
    then ok (safetyData & sdLastVotedRound ∙~ round )
    else bail fakeErr -- incorrect last vote round

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

verifyQcM : QuorumCert → LBFT (Either ErrLog Unit)
verifyQcM qc = do
  validatorVerifier ← use (lRoundManager ∙ srValidatorVerifier)
  pure (QuorumCert.verify qc validatorVerifier) ∙^∙ withErrCtx ("InvalidQuorumCertificate" ∷ [])

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

consensusState : SafetyRules → ConsensusState
consensusState self =
  ConsensusState∙new (self ^∙ srPersistentStorage ∙ pssSafetyData)
                     (self ^∙ srPersistentStorage ∙ pssWaypoint)

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

-- ** NOTE: PAY PARTICULAR ATTENTION TO THIS FUNCTION **
-- ** Because : it is long with lots of branches, so easy to transcribe wrong. **
-- ** And if initialization is wrong, everything is wrong. **
-- TODO: convert to EitherD (and perhaps break into more steps?)
initialize : SafetyRules → EpochChangeProof → Either ErrLog SafetyRules
initialize self proof = do
  let waypoint   = self ^∙ srPersistentStorage ∙ pssWaypoint
  lastLi         ← withErrCtx' (here' ("EpochChangeProof.verify" ∷ []))
                               (        EpochChangeProof.verify proof waypoint)
  let ledgerInfo = lastLi ^∙ liwsLedgerInfo
  epochState     ← maybeS (ledgerInfo ^∙ liNextEpochState)
                          (Left fakeErr) -- ["last ledger info has no epoch state"]
                          pure
  let currentEpoch = self ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdEpoch
  if-dec currentEpoch <? epochState ^∙ esEpoch
    then (do
      waypoint'  ← withErrCtx' (here' ("Waypoint.newEpochBoundary" ∷ []))
                               (        Waypoint.newEpochBoundary ledgerInfo)
      continue1 (self & srPersistentStorage ∙ pssWaypoint    ∙~ waypoint'
                      & srPersistentStorage ∙ pssSafetyData  ∙~
                          SafetyData∙new (epochState ^∙ esEpoch) {-Round-} 0 {-Round-} 0 nothing)
                epochState)
    else continue1 self epochState
 where
  continue2 : SafetyRules → EpochState → Either ErrLog SafetyRules
  here'     : List String → List String

  continue1 : SafetyRules → EpochState → Either ErrLog SafetyRules
  continue1 self1 epochState =
    continue2 (self1 & srEpochState ?~ epochState) epochState

  continue2 self2 epochState = do
    let author = self2 ^∙ srPersistentStorage ∙ pssAuthor
    maybeS (ValidatorVerifier.getPublicKey (epochState ^∙ esVerifier) author)
      (Left fakeErr) -- ["ValidatorNotInSet", lsA author] $
      λ expectedKey → do
        let currKey = eitherS (signer self2)
                      (const nothing)
                      (just ∘ ValidatorSigner.publicKey_USE_ONLY_AT_INIT)
        grd‖ currKey == just expectedKey ≔
             Right self2

           ‖ self2 ^∙ srExportConsensusKey ≔ (do
              consensusKey ← withErrCtx' (here' ("ValidatorKeyNotFound" ∷ []))
                (PersistentSafetyStorage.consensusKeyForVersion
                  (self2 ^∙ srPersistentStorage) expectedKey)
              Right (self2 & srValidatorSigner ?~ ValidatorSigner∙new author consensusKey))

           ‖ otherwise≔
             Left fakeErr -- ["srExportConsensusKey", "False", "NOT IMPLEMENTED"]
  here' t = "SafetyRules" ∷ "initialize" ∷ t

abstract
  initialize-e-abs = initialize

  -- TODO: temporary until initialize is converted to EitherD
  initialize-ed-abs : SafetyRules → EpochChangeProof → EitherD ErrLog SafetyRules
  initialize-ed-abs sr ecp = fromEither $ initialize sr ecp

  initialize-ed-abs-≡ : ∀ {sr ecp} → EitherD-run (initialize-ed-abs sr ecp) ≡ initialize sr ecp
  initialize-ed-abs-≡ {sr} {ecp}
     with initialize sr ecp
  ... | Left x  = refl
  ... | Right y = refl

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

constructAndSignVoteM-continue0 : VoteProposal → ValidatorSigner                       → LBFT (Either ErrLog Vote)
constructAndSignVoteM-continue1 : VoteProposal → ValidatorSigner →  Block → SafetyData → LBFT (Either ErrLog Vote)
constructAndSignVoteM-continue2 : VoteProposal → ValidatorSigner →  Block → SafetyData → LBFT (Either ErrLog Vote)

constructAndSignVoteM : MaybeSignedVoteProposal → LBFT (Either ErrLog Vote)
constructAndSignVoteM maybeSignedVoteProposal = do
  vs ← use (lSafetyRules ∙ srValidatorSigner)
  maybeS vs (bail fakeErr {- srValidatorSigner is nothing -}) λ validatorSigner → do
    let voteProposal = maybeSignedVoteProposal ^∙ msvpVoteProposal
    constructAndSignVoteM-continue0 voteProposal validatorSigner

module constructAndSignVoteM-continue0 (voteProposal : VoteProposal) (validatorSigner : ValidatorSigner) where
  step₀ : LBFT (Either ErrLog Vote)
  step₁ : SafetyData → LBFT (Either ErrLog Vote)

  proposedBlock = voteProposal ^∙ vpBlock

  step₀ = do
    safetyData0 ← use (lPersistentSafetyStorage ∙ pssSafetyData)
    verifyEpochM (proposedBlock ^∙ bEpoch) safetyData0 ∙?∙ λ _ → step₁ safetyData0

  step₁ safetyData0 = do
      caseMD (safetyData0 ^∙ sdLastVote) of λ where
        (just vote) →
          ifD vote ^∙ vVoteData ∙ vdProposed ∙ biRound == proposedBlock ^∙ bRound
            then ok vote
            else constructAndSignVoteM-continue1 voteProposal validatorSigner proposedBlock safetyData0
        nothing → constructAndSignVoteM-continue1 voteProposal validatorSigner proposedBlock safetyData0

constructAndSignVoteM-continue0 = constructAndSignVoteM-continue0.step₀

module constructAndSignVoteM-continue1
  (voteProposal  : VoteProposal) (validatorSigner : ValidatorSigner)
  (proposedBlock : Block)        (safetyData0     : SafetyData) where

  step₀ : LBFT (Either ErrLog Vote)
  step₁ : LBFT (Either ErrLog Vote)
  step₂ : ValidatorVerifier → LBFT (Either ErrLog Vote)
  step₃ : LBFT (Either ErrLog Vote)

  step₀ =
    verifyQcM (proposedBlock ^∙ bQuorumCert) ∙?∙ λ _ → step₁

  step₁ = do
      validatorVerifier ← use (lRoundManager ∙ srValidatorVerifier)
      step₂ validatorVerifier

  step₂ validatorVerifier =
      pure (Block.validateSignature proposedBlock validatorVerifier) ∙?∙ λ _ → step₃

  step₃ =
        verifyAndUpdatePreferredRoundM (proposedBlock ^∙ bQuorumCert) safetyData0 ∙?∙
        constructAndSignVoteM-continue2 voteProposal validatorSigner proposedBlock

constructAndSignVoteM-continue1 = constructAndSignVoteM-continue1.step₀

module constructAndSignVoteM-continue2 (voteProposal : VoteProposal) (validatorSigner : ValidatorSigner)
                                       (proposedBlock : Block) (safetyData : SafetyData) where
  step₀ : LBFT (Either ErrLog Vote)
  step₁ : SafetyData → LBFT (Either ErrLog Vote)
  step₂ : SafetyData → VoteData → LBFT (Either ErrLog Vote)
  step₃ : SafetyData → VoteData → Author → LedgerInfo → LBFT (Either ErrLog Vote)

  step₀ =
    verifyAndUpdateLastVoteRoundM (proposedBlock ^∙ bBlockData ∙ bdRound) safetyData ∙?∙ step₁

  step₁ safetyData1 = do
    pssSafetyData-rm ∙= safetyData1
    pure (extensionCheck voteProposal) ∙?∙ (step₂ safetyData1)

  step₂ safetyData1 voteData = do
      let author = validatorSigner ^∙ vsAuthor
      constructLedgerInfoM proposedBlock (Crypto.hashVD voteData)
                           ∙^∙ withErrCtx ("" ∷ []) ∙?∙ (step₃ safetyData1 voteData author)

  step₃ safetyData1 voteData author ledgerInfo = do
        let signature = ValidatorSigner.sign validatorSigner ledgerInfo
            vote      = Vote.newWithSignature voteData author ledgerInfo signature
        pssSafetyData-rm ∙= (safetyData1 & sdLastVote ?~ vote)
        logInfo fakeInfo -- InfoUpdateLastVotedRound
        ok vote

constructAndSignVoteM-continue2 = constructAndSignVoteM-continue2.step₀

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

signProposalM : BlockData → LBFT (Either ErrLog Block)
signProposalM blockData = do
 vs ← use (lSafetyRules ∙ srValidatorSigner)
 maybeS vs (bail fakeErr) {-ErrL (here' ["srValidatorSigner", "Nothing"])-} $ λ validatorSigner → do
  safetyData ← use (lPersistentSafetyStorage ∙ pssSafetyData)
  verifyAuthorM (blockData ^∙ bdAuthor) ∙?∙ λ _ →
    verifyEpochM (blockData ^∙ bdEpoch) safetyData ∙?∙ λ _ →
      ifD blockData ^∙ bdRound ≤?ℕ safetyData ^∙ sdLastVotedRound
      then bail fakeErr
      -- {-     ErrL (here' [ "InvalidProposal"
      --                    , "Proposed round is not higher than last voted round "
      --                    , lsR (blockData ^∙ bdRound), lsR (safetyData ^∙ sdLastVotedRound) ])-}
      else do
        verifyQcM (blockData ^∙ bdQuorumCert) ∙?∙ λ _ →
          verifyAndUpdatePreferredRoundM (blockData ^∙ bdQuorumCert) safetyData ∙?∙ λ safetyData1 → do
            pssSafetyData-rm ∙= safetyData1
            let signature  = ValidatorSigner.sign validatorSigner blockData
            ok (Block.newProposalFromBlockDataAndSignature blockData signature)
 where
  here' : List String → List String
  here' t = "SafetyRules" ∷ "signProposalM" ∷ t

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

signTimeoutM : Timeout → LBFT (Either ErrLog Signature)
signTimeoutM timeout = do
 vs ← use (lSafetyRules ∙ srValidatorSigner)
 maybeS vs (bail fakeErr) {-"srValidatorSigner", "Nothing"-} $ λ validatorSigner → do
   safetyData ← use (lPersistentSafetyStorage ∙ pssSafetyData)
   verifyEpochM (timeout ^∙ toEpoch) safetyData ∙^∙ withErrCtx (here' []) ∙?∙ λ _ → do
     ifD‖ timeout ^∙ toRound ≤? safetyData ^∙ sdPreferredRound ≔
          bail fakeErr
          --(ErrIncorrectPreferredRound (here []) (timeout ^∙ toRound) (safetyData ^∙ sdPreferredRound))
        ‖ timeout ^∙ toRound <? safetyData ^∙ sdLastVotedRound ≔
          bail fakeErr
          --(ErrIncorrectLastVotedRound (here []) (timeout ^∙ toRound) (safetyData ^∙ sdLastVotedRound))
        ‖ timeout ^∙ toRound >? safetyData ^∙ sdLastVotedRound ≔
          verifyAndUpdateLastVoteRoundM (timeout ^∙ toRound) safetyData
            ∙^∙ withErrCtx (here' [])
            ∙?∙ (λ safetyData1 → do
            pssSafetyData-rm ∙= safetyData1
            logInfo fakeInfo -- (InfoUpdateLastVotedRound (timeout ^∙ toRound))
            continue validatorSigner)

        ‖ otherwise≔
          continue validatorSigner
 where
  continue : ValidatorSigner → LBFT (Either ErrLog Signature)
  continue validatorSigner = do
    let signature = ValidatorSigner.sign validatorSigner timeout
    ok signature

  here' : List String → List String
  here' t = "SafetyRules" ∷ "signTimeoutM" ∷ {-lsTO timeout ∷-}   t


text:
module Base.Ascription where

-- Encode infix ascription.
as' : ∀ {ℓ} (A : Set ℓ) (a : A) → A
as' _ a = a
syntax as' A a = a as A

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module UnifyTermL (A : Set) where

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (∃; _,_; _×_)
open import Data.Empty using (⊥-elim)

data Term (n : ℕ) : Set where
  i : (x : Fin n) -> Term n
  leaf : A → Term n
  _fork_ : (s t : Term n) -> Term n

Term-leaf-inj : ∀ {n l₁ l₂} → leaf {n} l₁ ≡ leaf l₂ → l₁ ≡ l₂
Term-leaf-inj refl = refl

_~>_ : (m n : ℕ) -> Set
m ~> n = Fin m -> Term n

▹ : ∀ {m n} -> (r : Fin m -> Fin n) -> Fin m -> Term n
▹ r = i ∘ r

_◃_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
f ◃ i x = f x
f ◃ (leaf l) = leaf l
f ◃ (s fork t) = (f ◃ s) fork (f ◃ t)

_≐_ : {m n : ℕ} -> (Fin m -> Term n) -> (Fin m -> Term n) -> Set
f ≐ g = ∀ x -> f x ≡ g x

◃ext : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ t -> f ◃ t ≡ g ◃ t
◃ext p (i x) = p x
◃ext p (leaf l) = refl
◃ext p (s fork t) = cong₂ _fork_ (◃ext p s) (◃ext p t)

_◇_ : ∀ {l m n : ℕ } -> (f : Fin m -> Term n) (g : Fin l -> Term m) -> Fin l -> Term n
f ◇ g = (f ◃_) ∘ g

≐-cong : ∀ {m n o} {f : m ~> n} {g} (h : _ ~> o) -> f ≐ g -> (h ◇ f) ≐ (h ◇ g)
≐-cong h f≐g t = cong (h ◃_) (f≐g t)

≐-sym : ∀ {m n} {f : m ~> n} {g} -> f ≐ g -> g ≐ f
≐-sym f≐g = sym ∘ f≐g

module Sub where
  fact1 : ∀ {n} -> (t : Term n) -> i ◃ t ≡ t
  fact1 (i x) = refl
  fact1 (leaf l) = refl
  fact1 (s fork t) = cong₂ _fork_ (fact1 s) (fact1 t)

  fact2 : ∀ {l m n} -> (f : Fin m -> Term n) (g : _) (t : Term l)
    -> (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
  fact2 f g (i x) = refl
  fact2 f g (leaf l) = refl
  fact2 f g (s fork t) = cong₂ _fork_ (fact2 f g s) (fact2 f g t)

  fact3 : ∀ {l m n} (f : Fin m -> Term n) (r : Fin l -> Fin m) -> (f ◇ (▹ r)) ≡ (f ∘ r)
  fact3 f r = refl -- ext (λ _ -> refl)

◃ext' : ∀ {m n o} {f : Fin m -> Term n}{g : Fin m -> Term o}{h} -> f ≐ (h ◇ g) -> ∀ t -> f ◃ t ≡ h ◃ (g ◃ t)
◃ext' p t = trans (◃ext p t) (Sub.fact2 _ _ t)

open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

open import UnifyFin

check : ∀{n} (x : Fin (suc n)) (t : Term (suc n)) -> Maybe (Term n)
check x (i y) = i <$> thick x y
check x (leaf l) = just (leaf l)
check x (s fork t) = _fork_ <$> check x s ⊛ check x t

_for_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) -> Fin (suc n) -> Term n
(t' for x) y = maybe′ i t' (thick x y)

data AList : ℕ -> ℕ -> Set where
  anil : ∀ {n} -> AList n n
  _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
               -> AList (suc m) n

sub : ∀ {m n} (σ : AList m n) -> Fin m -> Term n
sub anil = i
sub (σ asnoc t' / x) = sub σ ◇ (t' for x)

_++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n
ρ ++ anil = ρ
ρ ++ (σ asnoc t' / x) = (ρ ++ σ) asnoc t' / x

++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) -> ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
++-assoc ρ σ anil = refl
++-assoc ρ σ (τ asnoc t / x) = cong (λ s -> s asnoc t / x) (++-assoc ρ σ τ)

module SubList where
  anil-id-l : ∀ {m n} (σ : AList m n) -> anil ++ σ ≡ σ
  anil-id-l anil = refl
  anil-id-l (σ asnoc t' / x) = cong (λ σ -> σ asnoc t' / x) (anil-id-l σ)

  fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> sub (ρ ++ σ) ≐ (sub ρ ◇ sub σ)
  fact1 ρ anil v = refl
  fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
    where
      t = (t' for x) v
      hyp-on-terms = ◃ext (fact1 r s) t
      ◃-assoc = Sub.fact2 (sub r) (sub s) t

_∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
  -> ∃ (AList (suc m))
(n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

flexFlex : ∀ {m} (x y : Fin m) -> ∃ (AList m)
flexFlex {suc m} x y with thick x y
...              | just y' = m , anil asnoc i y' / x
...              | nothing = suc m , anil
flexFlex {zero} () _

flexRigid : ∀ {m} (x : Fin m) (t : Term m) -> Maybe (∃(AList m))
flexRigid {suc m} x t with check x t
...                   | just t' = just (m , anil asnoc t' / x)
...                   | nothing = nothing
flexRigid {zero} () _


text:
module Numeral.Integer.Proofs where

import      Data.Either as Either
open import Data.Tuple  as Tuple using (_,_)
open import Logic
import      Lvl
open import Functional
open import Numeral.Integer
open import Numeral.Integer.Oper
open import Numeral.Integer.Sign
open import Numeral.Natural.Induction
open import Numeral.Natural as ℕ using (ℕ)
import      Numeral.Natural.Oper as ℕ
import      Numeral.Natural.Oper.Proofs as ℕ
import      Numeral.Natural.Relation.Order as ℕ
import      Numeral.Sign as Sign
import      Numeral.Sign.Oper0 as Sign
import      Numeral.Sign.Proofs as Sign
open import Lang.Inspect
open import Logic.IntroInstances
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Function.Multi
import      Structure.Function.Names as Names
open import Structure.Operator
open import Structure.Operator.Group
open import Structure.Operator.Monoid
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator.Proofs
open import Structure.Operator.Ring
open import Structure.OrderedField
open import Structure.Relator.Properties
open import Syntax.Number
open import Syntax.Transitivity
open import Type

private variable ℓ : Lvl.Level

-- TODO: Prove the usual structures for ℤ

instance
  [+ₙ][𝐒]-preserving : Preserving₁(+ₙ_) ℕ.𝐒 𝐒
  [+ₙ][𝐒]-preserving = intro [≡]-intro

instance
  [+ₙ][+]-preserving : Preserving₂(+ₙ_) (ℕ._+_) (_+_)
  [+ₙ][+]-preserving = intro [≡]-intro

instance
  [+ₙ][⋅]-preserving : Preserving₂(+ₙ_) (ℕ._⋅_) (_⋅_)
  Preserving.proof [+ₙ][⋅]-preserving {ℕ.𝟎}   {ℕ.𝟎}   = [≡]-intro
  Preserving.proof [+ₙ][⋅]-preserving {ℕ.𝟎}   {ℕ.𝐒 y} = [≡]-intro
  Preserving.proof [+ₙ][⋅]-preserving {ℕ.𝐒 x} {ℕ.𝟎}   = [≡]-intro
  Preserving.proof [+ₙ][⋅]-preserving {ℕ.𝐒 x} {ℕ.𝐒 y} = [≡]-intro

-- [−₀]-preserving : Preserving₂(+ₙ_) (_−₀ₙ_) (_−₀_)
-- [/₀]-preserving : Preserving₂(+ₙ_) (_/₀ₙ_) (_/₀_)

instance
  [−ₙ][𝐒][𝐏]-preserving : Preserving₁(−ₙ_) ℕ.𝐒 𝐏
  Preserving.proof [−ₙ][𝐒][𝐏]-preserving {ℕ.𝟎}   = [≡]-intro
  Preserving.proof [−ₙ][𝐒][𝐏]-preserving {ℕ.𝐒 x} = [≡]-intro

instance
  [−ₙ][+]-preserving : Preserving₂(−ₙ_) (ℕ._+_) (_+_)
  Preserving.proof [−ₙ][+]-preserving {ℕ.𝟎}    {ℕ.𝟎}    = [≡]-intro
  Preserving.proof [−ₙ][+]-preserving {ℕ.𝟎}    {ℕ.𝐒(_)} = [≡]-intro
  Preserving.proof [−ₙ][+]-preserving {ℕ.𝐒(_)} {ℕ.𝟎}    = [≡]-intro
  Preserving.proof [−ₙ][+]-preserving {ℕ.𝐒(_)} {ℕ.𝐒(_)} = [≡]-intro

instance
  [−][𝐒][𝐏]-preserving : Preserving₁(−_) 𝐒 𝐏
  Preserving.proof [−][𝐒][𝐏]-preserving {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [−][𝐒][𝐏]-preserving {+ₙ ℕ.𝐒 x}  = [≡]-intro
  Preserving.proof [−][𝐒][𝐏]-preserving {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Preserving.proof [−][𝐒][𝐏]-preserving {−𝐒ₙ ℕ.𝐒 x} = [≡]-intro

instance
  [−𝐒ₙ][𝐒][𝐏]-preserving : Preserving₁(−𝐒ₙ_) ℕ.𝐒 𝐏
  Preserving.proof [−𝐒ₙ][𝐒][𝐏]-preserving = [≡]-intro

instance
  [+𝐒ₙ][𝐒]-preserving : Preserving₁(+𝐒ₙ_) ℕ.𝐒 𝐒
  Preserving.proof [+𝐒ₙ][𝐒]-preserving = [≡]-intro

instance
  [−][+]-preserving : Preserving₂(−_) (_+_)(_+_)
  Preserving.proof [−][+]-preserving {x}{y} = p{x}{y} where
    [−ₙ]-distribute-[−] : ∀{x y} → (−(x −ₙ y) ≡ y −ₙ x)
    [−ₙ]-distribute-[−] {ℕ.𝟎}   {ℕ.𝟎}   = [≡]-intro
    [−ₙ]-distribute-[−] {ℕ.𝟎}   {ℕ.𝐒 x} = [≡]-intro
    [−ₙ]-distribute-[−] {ℕ.𝐒 x} {ℕ.𝟎}   = [≡]-intro
    [−ₙ]-distribute-[−] {ℕ.𝐒 x} {ℕ.𝐒 y} = [−ₙ]-distribute-[−] {x} {y}

    p : Names.Preserving₂(−_) (_+_)(_+_)
    p {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝟎}        = [≡]-intro
    p {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝐒 y}      = [≡]-intro
    p {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝟎}        = [≡]-intro
    p {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝐒 y}      = [≡]-intro
    p {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝟎}       = [≡]-intro
    p {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝐒 y}     = [≡]-intro
    p {+ₙ ℕ.𝐒 x}  {−𝐒ₙ y}         = [−ₙ]-distribute-[−] {x}{y}
    p {−𝐒ₙ x}     {+ₙ ℕ.𝐒 y}      = [−ₙ]-distribute-[−] {y}{x}
    p {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}        = [≡]-intro
    p {−𝐒ₙ ℕ.𝟎}   {−𝐒ₙ ℕ.𝟎}       = [≡]-intro
    p {−𝐒ₙ ℕ.𝟎}   {−𝐒ₙ ℕ.𝐒 y}     = [≡]-intro
    p {−𝐒ₙ ℕ.𝐒 x} {−𝐒ₙ ℕ.𝟎}       = [≡]-intro
    p {−𝐒ₙ ℕ.𝐒 x} {−𝐒ₙ ℕ.𝐒 y}     = [≡]-intro
    p {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}        = [≡]-intro

instance
  [absₙ][⋅]-preserving : Preserving₂(absₙ)(_⋅_)(ℕ._⋅_)
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝐒 y}  = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝐒 y}  = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {−𝐒ₙ x}     {−𝐒ₙ y}     = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝐒 y}  = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [absₙ][⋅]-preserving {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y}  = [≡]-intro

instance
  [sign0][⋅]-preserving : Preserving₂(sign0)(_⋅_)(Sign._⨯_)
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝐒 y}  = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝐒 y}  = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {−𝐒ₙ x}     {−𝐒ₙ y}     = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝐒 y}  = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}    = [≡]-intro
  Preserving.proof [sign0][⋅]-preserving {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y}  = [≡]-intro

[ℤ]-non-negative-induction : ∀{P : ℤ → Type{ℓ}} → P(𝟎) → (∀(n) → P(+ₙ(n)) → P(+𝐒ₙ(n))) → (∀{n} → P(+ₙ n))
[ℤ]-non-negative-induction {P = P} = [ℕ]-induction {φ = P ∘ +ₙ_}

[ℤ]-positive-induction : ∀{P : ℤ → Type{ℓ}} → P(+𝐒ₙ(ℕ.𝟎)) → (∀(n) → P(+𝐒ₙ(n)) → P(+𝐒ₙ(ℕ.𝐒(n)))) → (∀{n} → P(+𝐒ₙ n))
[ℤ]-positive-induction {P = P} [1] [+] {ℕ.𝟎}   = [1]
[ℤ]-positive-induction {P = P} [1] [+] {ℕ.𝐒 n} = [+] n ([ℤ]-positive-induction {P = P} [1] [+] {n})

[ℤ]-non-positive-induction : ∀{P : ℤ → Type{ℓ}} → P(𝟎) → (∀(n) → P(−ₙ(n)) → P(−𝐒ₙ(n))) → (∀{n} → P(−ₙ n))
[ℤ]-non-positive-induction {P = P} [0] [−] {ℕ.𝟎}   = [0]
[ℤ]-non-positive-induction {P = P} [0] [−] {ℕ.𝐒 n} = [−] n ([ℤ]-non-positive-induction {P = P} [0] [−] {n})

[ℤ]-negative-induction : ∀{P : ℤ → Type{ℓ}} → P(−𝐒ₙ(ℕ.𝟎)) → (∀(n) → P(−𝐒ₙ(n)) → P(−𝐒ₙ(ℕ.𝐒(n)))) → (∀{n} → P(−𝐒ₙ n))
[ℤ]-negative-induction {P = P} = [ℕ]-induction {φ = P ∘ −𝐒ₙ_}

-- An intuitive induction proof method on integers
[ℤ]-intuitive-induction : ∀{P : ℤ → Type{ℓ}} → (∀{n} → P(−ₙ n) → P(−𝐒ₙ(n))) → P(𝟎) → (∀{n} → P(+ₙ n) → P(+𝐒ₙ(n))) → (∀{n} → P(n))
[ℤ]-intuitive-induction {P = P} [−] [0] [+] {𝟎}           = [0]
[ℤ]-intuitive-induction {P = P} [−] [0] [+] {+𝐒ₙ(n)}      = [+] ([ℤ]-intuitive-induction {P = P} [−] [0] [+] {+ₙ n})
[ℤ]-intuitive-induction {P = P} [−] [0] [+] {−𝐒ₙ(ℕ.𝟎)}    = [−] ([0])
[ℤ]-intuitive-induction {P = P} [−] [0] [+] {−𝐒ₙ(ℕ.𝐒(n))} = [−] ([ℤ]-intuitive-induction {P = P} [−] [0] [+] {−𝐒ₙ(n)})

[−𝐒ₙ]-equality : ∀{n} → (−𝐒ₙ(n) ≡ −ₙ(ℕ.𝐒(n)))
[−𝐒ₙ]-equality = [≡]-intro

[+𝐒ₙ]-equality : ∀{n} → (+𝐒ₙ(n) ≡ +ₙ(ℕ.𝐒(n)))
[+𝐒ₙ]-equality = [≡]-intro

-- (−n)−1 = −(n+1)
[𝐏]-negative : ∀{n} → (𝐏(−ₙ n) ≡ −𝐒ₙ(n))
[𝐏]-negative {ℕ.𝟎}    = [≡]-intro
[𝐏]-negative {ℕ.𝐒(n)} = [≡]-intro

-- (−(n+1))+1 = −n
[𝐒][−𝐒ₙ]-negative-identity : ∀{n} → (𝐒(−𝐒ₙ(n)) ≡ −ₙ n)
[𝐒][−𝐒ₙ]-negative-identity {ℕ.𝟎}    = [≡]-intro
[𝐒][−𝐒ₙ]-negative-identity {ℕ.𝐒(n)} = [≡]-intro

instance
  [𝐒][𝐏]-inverse : Inverse(𝐒)(𝐏)
  Inverseᵣ.proof (Tuple.left [𝐒][𝐏]-inverse)  {+ₙ  ℕ.𝟎}   = [≡]-intro
  Inverseᵣ.proof (Tuple.left [𝐒][𝐏]-inverse)  {+ₙ  ℕ.𝐒 x} = [≡]-intro
  Inverseᵣ.proof (Tuple.left [𝐒][𝐏]-inverse)  {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Inverseᵣ.proof (Tuple.left [𝐒][𝐏]-inverse)  {−𝐒ₙ ℕ.𝐒 x} = [≡]-intro
  Inverseᵣ.proof (Tuple.right [𝐒][𝐏]-inverse) {+ₙ  ℕ.𝟎}   = [≡]-intro
  Inverseᵣ.proof (Tuple.right [𝐒][𝐏]-inverse) {+ₙ  ℕ.𝐒 x} = [≡]-intro
  Inverseᵣ.proof (Tuple.right [𝐒][𝐏]-inverse) {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
  Inverseᵣ.proof (Tuple.right [𝐒][𝐏]-inverse) {−𝐒ₙ ℕ.𝐒 x} = [≡]-intro

[−ₙ]-identityᵣ : ∀{x} → (x −ₙ ℕ.𝟎 ≡ +ₙ x)
[−ₙ]-identityᵣ = [≡]-intro

[−ₙ]-antiidentityₗ : ∀{x} → (ℕ.𝟎 −ₙ x ≡ −ₙ x)
[−ₙ]-antiidentityₗ {ℕ.𝟎}    = [≡]-intro
[−ₙ]-antiidentityₗ {ℕ.𝐒(_)} = [≡]-intro

[−ₙ][𝐒]-step : ∀{x y} → (ℕ.𝐒(x) −ₙ y ≡ 𝐒(x −ₙ y))
[−ₙ][𝐒]-step {ℕ.𝟎}   {ℕ.𝟎}    = [≡]-intro
[−ₙ][𝐒]-step {ℕ.𝟎}   {ℕ.𝐒(y)} = [−ₙ]-antiidentityₗ {y} 🝖 symmetry(_≡_) ([𝐒][−𝐒ₙ]-negative-identity{y})
[−ₙ][𝐒]-step {ℕ.𝐒(_)}{ℕ.𝟎}    = [≡]-intro
[−ₙ][𝐒]-step {ℕ.𝐒(x)}{ℕ.𝐒(y)} = [−ₙ][𝐒]-step {x}{y}

[−][−ₙ] : ∀{x} → (−(+ₙ x) ≡ −ₙ x)
[−][−ₙ] {ℕ.𝟎}    = [≡]-intro
[−][−ₙ] {ℕ.𝐒(_)} = [≡]-intro

instance
  [+ₙ]-injectivity : Injective(+ₙ_)
  Injective.proof [+ₙ]-injectivity [≡]-intro = [≡]-intro

instance
  [−𝐒ₙ]-injectivity : Injective(−𝐒ₙ_)
  Injective.proof [−𝐒ₙ]-injectivity [≡]-intro = [≡]-intro

instance
  [−ₙ]-injectivity : Injective(−ₙ_)
  Injective.proof [−ₙ]-injectivity {ℕ.𝟎}   {ℕ.𝟎}    xy        = [≡]-intro
  Injective.proof [−ₙ]-injectivity {ℕ.𝐒 x} {ℕ.𝐒 .x} [≡]-intro = [≡]-intro

instance
  [+𝐒ₙ]-injectivity : Injective(+𝐒ₙ_)
  Injective.proof [+𝐒ₙ]-injectivity [≡]-intro = [≡]-intro

[−ₙ]-self : ∀{x} → (x −ₙ x ≡ 𝟎)
[−ₙ]-self {ℕ.𝟎}    = [≡]-intro
[−ₙ]-self {ℕ.𝐒(x)} = [−ₙ]-self {x}

instance
  [+]-commutativity : Commutativity(_+_)
  [+]-commutativity = intro(\{x y} → p{x}{y}) where
    p : Names.Commutativity(_+_)
    p {+ₙ x}  {+ₙ y}  = congruence₁(+ₙ_) (commutativity(ℕ._+_) {x}{y})
    p {+ₙ _}  {−𝐒ₙ _} = [≡]-intro
    p {−𝐒ₙ _} {+ₙ _}  = [≡]-intro
    p {−𝐒ₙ x} {−𝐒ₙ y} = congruence₁(−𝐒ₙ_ ∘ ℕ.𝐒) (commutativity(ℕ._+_) {x}{y})

instance
  [+]-identityₗ : Identityₗ(_+_)(𝟎)
  Identityₗ.proof [+]-identityₗ {+ₙ _}  = [≡]-intro
  Identityₗ.proof [+]-identityₗ {−𝐒ₙ _} = [≡]-intro

instance
  [+]-identityᵣ : Identityᵣ(_+_)(𝟎)
  Identityᵣ.proof [+]-identityᵣ {+ₙ _}  = [≡]-intro
  Identityᵣ.proof [+]-identityᵣ {−𝐒ₙ _} = [≡]-intro

instance
  [+]-identity : Identity(_+_)(𝟎)
  [+]-identity = intro

instance
  [+]-inverseFunctionₗ : InverseFunctionₗ(_+_)(−_)
  InverseFunctionₗ.proof [+]-inverseFunctionₗ {+ₙ ℕ.𝟎}    = [≡]-intro
  InverseFunctionₗ.proof [+]-inverseFunctionₗ {+ₙ ℕ.𝐒(x)} = [−ₙ]-self {x}
  InverseFunctionₗ.proof [+]-inverseFunctionₗ {−𝐒ₙ(x)}    = [−ₙ]-self {x}

instance
  [+]-inverseFunctionᵣ : InverseFunctionᵣ(_+_)(−_)
  InverseFunctionᵣ.proof [+]-inverseFunctionᵣ {+ₙ ℕ.𝟎}    = [≡]-intro
  InverseFunctionᵣ.proof [+]-inverseFunctionᵣ {+ₙ ℕ.𝐒(x)} = [−ₙ]-self {x}
  InverseFunctionᵣ.proof [+]-inverseFunctionᵣ {−𝐒ₙ(x)}    = [−ₙ]-self {x}

instance
  [+]-inverseFunction : InverseFunction(_+_)(−_)
  [+]-inverseFunction = intro

instance
  [−]-involution : Involution(−_)
  Involution.proof [−]-involution {+ₙ ℕ.𝟎}    = [≡]-intro
  Involution.proof [−]-involution {+ₙ ℕ.𝐒(x)} = [≡]-intro
  Involution.proof [−]-involution {−𝐒ₙ x}     = [≡]-intro

instance
  [−]-injectivity : Injective(−_)
  Injective.proof [−]-injectivity {a}{b} p =
    a      🝖[ _≡_ ]-[ involution(−_) ]-sym
    −(− a) 🝖[ _≡_ ]-[ congruence₁(−_) p ]
    −(− b) 🝖[ _≡_ ]-[ involution(−_) ]
    b      🝖-end

instance
  [−]-surjectivity : Surjective(−_)
  Surjective.proof [−]-surjectivity {y} = [∃]-intro (− y) ⦃ involution(−_) ⦄

instance
  [−]-bijectivity : Bijective(−_)
  [−]-bijectivity = injective-surjective-to-bijective(−_)

instance
  abs-idempotent : Idempotent(abs)
  Idempotent.proof abs-idempotent {+ₙ x}  = [≡]-intro
  Idempotent.proof abs-idempotent {−𝐒ₙ x} = [≡]-intro

abs-injective-zero : ∀{n} → (abs(n) ≡ 𝟎) → (n ≡ 𝟎)
abs-injective-zero {𝟎} [≡]-intro = [≡]-intro

abs-[−] : ∀{n} → (abs(− n) ≡ abs(n))
abs-[−] {𝟎}      = [≡]-intro
abs-[−] {+𝐒ₙ(_)} = [≡]-intro
abs-[−] {−𝐒ₙ(_)} = [≡]-intro

abs-preserving : ∀{x} → (abs(x) ≡ +ₙ(absₙ(x)))
abs-preserving {𝟎}      = [≡]-intro
abs-preserving {+𝐒ₙ(_)} = [≡]-intro
abs-preserving {−𝐒ₙ(_)} = [≡]-intro

absₙ-zero : ∀{n} → (absₙ(n) ≡ ℕ.𝟎) → (n ≡ 𝟎)
absₙ-zero {𝟎}      ([≡]-intro) = [≡]-intro

[+][𝐒]-stepₗ : ∀{x y} → (𝐒(x) + y ≡ 𝐒(x + y))
[+][𝐒]-stepₗ {+ₙ x}       {+ₙ y}       = [≡]-intro
[+][𝐒]-stepₗ {+ₙ ℕ.𝟎   }  {−𝐒ₙ ℕ.𝟎   } = [≡]-intro
[+][𝐒]-stepₗ {+ₙ ℕ.𝟎   }  {−𝐒ₙ ℕ.𝐒(_)} = [≡]-intro
[+][𝐒]-stepₗ {+ₙ ℕ.𝐒(_)}  {−𝐒ₙ ℕ.𝟎   } = [≡]-intro
[+][𝐒]-stepₗ {+ₙ ℕ.𝐒(x)}  {−𝐒ₙ ℕ.𝐒(y)} = [−ₙ][𝐒]-step{x}{ℕ.𝐒(y)}
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝟎   } {+ₙ ℕ.𝟎   }  = [≡]-intro
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝐒(_)} {+ₙ ℕ.𝟎   }  = [≡]-intro
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝟎   } {+ₙ ℕ.𝐒(_)}  = [≡]-intro
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝐒(y)} {+ₙ ℕ.𝐒(x)}  = [−ₙ][𝐒]-step{x}{ℕ.𝐒(y)}
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝟎   } {−𝐒ₙ ℕ.𝟎   } = [≡]-intro
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝐒(_)} {−𝐒ₙ ℕ.𝟎   } = [≡]-intro
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝟎   } {−𝐒ₙ ℕ.𝐒(_)} = [≡]-intro
[+][𝐒]-stepₗ {−𝐒ₙ ℕ.𝐒(y)} {−𝐒ₙ ℕ.𝐒(x)} = [≡]-intro

instance
  [𝐒]-preserving-[+]ₗ : ∀{y} → Preserving₁(𝐒) (_+ y)(_+ y)
  Preserving.proof ([𝐒]-preserving-[+]ₗ {y}) {x} = symmetry(_≡_) ([+][𝐒]-stepₗ {x}{y})

[+][𝐒]-stepᵣ : ∀{x y} → (x + 𝐒(y) ≡ 𝐒(x + y))
[+][𝐒]-stepᵣ {+ₙ x}      {+ₙ y}     = [≡]-intro
[+][𝐒]-stepᵣ {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
[+][𝐒]-stepᵣ {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝐒 x} = [≡]-intro
[+][𝐒]-stepᵣ {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
[+][𝐒]-stepᵣ {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝐒 y} = [+][𝐒]-stepᵣ {−𝐒ₙ y}{+ₙ x}
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}    = [≡]-intro
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝐒 y}  = [≡]-intro
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}    = [≡]-intro
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y}  = [+][𝐒]-stepᵣ {−𝐒ₙ x}{+ₙ y}
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝟎}   {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝐒 x} {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝟎}   {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
[+][𝐒]-stepᵣ {−𝐒ₙ ℕ.𝐒 x} {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro

instance
  [𝐒]-preserving-[+]ᵣ : ∀{x} → Preserving₁(𝐒) (_+_ x)(_+_ x)
  Preserving.proof ([𝐒]-preserving-[+]ᵣ {x}) {y} = symmetry(_≡_) ([+][𝐒]-stepᵣ {x}{y})

[+][𝐏]-stepₗ : ∀{x y} → (𝐏(x) + y ≡ 𝐏(x + y))
[+][𝐏]-stepₗ {x}{y} =
  𝐏(x) + y                 🝖[ _≡_ ]-[ congruence₂(_+_) (congruence₁(𝐏) (involution(−_) {x})) (involution(−_) {y}) ]-sym
  𝐏(−(− x)) + (−(− y))     🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(−(− y)) (preserving₁(−_)(𝐒)(𝐏) {− x}) ]-sym
  (− 𝐒(− x)) + (−(− y))    🝖[ _≡_ ]-[ preserving₂(−_)(_+_)(_+_) {𝐒(− x)}{− y} ]-sym
  −(𝐒(− x) + (− y))        🝖[ _≡_ ]-[ congruence₁(−_) ([+][𝐒]-stepₗ {− x}{− y}) ]
  −(𝐒((− x) + (− y)))      🝖[ _≡_ ]-[ preserving₁(−_)(𝐒)(𝐏) ]
  𝐏(−((− x) + (− y)))      🝖[ _≡_ ]-[ congruence₁(𝐏) (preserving₂(−_)(_+_)(_+_) {− x}{− y}) ]
  𝐏(((−(− x)) + (−(− y)))) 🝖[ _≡_ ]-[ congruence₁(𝐏) (congruence₂(_+_) (involution(−_) {x}) (involution(−_) {y})) ]
  𝐏(x + y)                 🝖-end

instance
  [𝐏]-preserving-[+]ₗ : ∀{y} → Preserving₁(𝐏) (_+ y)(_+ y)
  Preserving.proof ([𝐏]-preserving-[+]ₗ {y}) {x} = symmetry(_≡_) ([+][𝐏]-stepₗ {x}{y})

[+][𝐏]-stepᵣ : ∀{x y} → (x + 𝐏(y) ≡ 𝐏(x + y))
[+][𝐏]-stepᵣ {x}{y} =
  x + 𝐏(y)                 🝖[ _≡_ ]-[ congruence₂(_+_) (involution(−_) {x}) (congruence₁(𝐏) (involution(−_) {y})) ]-sym
  (−(− x)) + 𝐏(−(− y))     🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(−(− x)) (preserving₁(−_)(𝐒)(𝐏) {− y}) ]-sym
  (−(− x)) + (− 𝐒(− y))    🝖[ _≡_ ]-[ preserving₂(−_)(_+_)(_+_) {− x}{𝐒(− y)} ]-sym
  −((− x) + 𝐒(− y))        🝖[ _≡_ ]-[ congruence₁(−_) ([+][𝐒]-stepᵣ {− x}{− y}) ]
  −(𝐒((− x) + (− y)))      🝖[ _≡_ ]-[ preserving₁(−_)(𝐒)(𝐏) ]
  𝐏(−((− x) + (− y)))      🝖[ _≡_ ]-[ congruence₁(𝐏) (preserving₂(−_)(_+_)(_+_) {− x}{− y}) ]
  𝐏(((−(− x)) + (−(− y)))) 🝖[ _≡_ ]-[ congruence₁(𝐏) (congruence₂(_+_) (involution(−_) {x}) (involution(−_) {y})) ]
  𝐏(x + y)                 🝖-end

instance
  [𝐏]-preserving-[+]ᵣ : ∀{x} → Preserving₁(𝐏) (_+_ x)(_+_ x)
  Preserving.proof ([𝐏]-preserving-[+]ᵣ {x}) {y} = symmetry(_≡_) ([+][𝐏]-stepᵣ {x}{y})

[−]-of-[+𝐒ₙ] : ∀{x y} → (+𝐒ₙ x) − (+𝐒ₙ y) ≡ (+ₙ x) − (+ₙ y)
[−]-of-[+𝐒ₙ] {y = ℕ.𝟎}   = [≡]-intro
[−]-of-[+𝐒ₙ] {y = ℕ.𝐒 _} = [≡]-intro

[+ₙ][−₀][−]-preserving : ∀{x y} → (x ℕ.≥ y) → ((+ₙ(x ℕ.−₀ y)) ≡ ((+ₙ x) − (+ₙ y)))
[+ₙ][−₀][−]-preserving ℕ.min = [≡]-intro
[+ₙ][−₀][−]-preserving {ℕ.𝐒 x}{ℕ.𝐒 y} (ℕ.succ p) = [+ₙ][−₀][−]-preserving {x}{y} p 🝖 symmetry(_≡_) ([−]-of-[+𝐒ₙ] {x}{y})

[−ₙ]-on-[+]ₗ-redundancy : ∀{a b c} → ((a ℕ.+ b) −ₙ (a ℕ.+ c) ≡ b −ₙ c)
[−ₙ]-on-[+]ₗ-redundancy{ℕ.𝟎}  {b}{c} = [≡]-intro
[−ₙ]-on-[+]ₗ-redundancy{ℕ.𝐒 a}{b}{c} = [−ₙ]-on-[+]ₗ-redundancy{a}{b}{c}

instance
  [+]-associativity : Associativity(_+_)
  [+]-associativity = intro(\{x y z} → p{x}{y}{z}) where
    postulate p : Names.Associativity(_+_)
    {-p {x} {y} {𝟎}     =
      (x + y) + 𝟎 🝖[ _≡_ ]-[ identityᵣ(_+_)(𝟎) ]
      x + y       🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x) (identityᵣ(_+_)(𝟎)) ]-sym
      x + (y + 𝟎) 🝖-end
    p {x} {y} {+𝐒ₙ z} =
      (x + y) + (+𝐒ₙ(z))   🝖[ _≡_ ]-[]
      (x + y) + 𝐒(+ₙ(z))   🝖[ _≡_ ]-[ [+][𝐒]-stepᵣ {x + y}{+ₙ(z)} ]
      𝐒((x + y) + (+ₙ(z))) 🝖[ _≡_ ]-[ congruence₁(𝐒) (p{x}{y}{+ₙ z}) ]
      𝐒(x + (y + (+ₙ(z)))) 🝖[ _≡_ ]-[ [+][𝐒]-stepᵣ {x}{y + (+ₙ z)} ]-sym
      x + 𝐒(y + (+ₙ(z)))   🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x) ([+][𝐒]-stepᵣ {y}{+ₙ z}) ]-sym
      x + (y + 𝐒(+ₙ(z)))   🝖[ _≡_ ]-[]
      x + (y + (+𝐒ₙ(z)))   🝖-end
    p {x} {y} {−𝐒ₙ z} =
      (x + y) + (−𝐒ₙ(z))   🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x + y) [𝐏]-negative ]-sym
      (x + y) + 𝐏(−ₙ(z))   🝖[ _≡_ ]-[ [+][𝐏]-stepᵣ {x + y}{−ₙ(z)} ]
      𝐏((x + y) + (−ₙ(z))) 🝖[ _≡_ ]-[ congruence₁(𝐏) (p{x}{y}{−ₙ z}) ]
      𝐏(x + (y + (−ₙ(z)))) 🝖[ _≡_ ]-[ [+][𝐏]-stepᵣ {x}{y + (−ₙ z)} ]-sym
      x + 𝐏(y + (−ₙ(z)))   🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x) ([+][𝐏]-stepᵣ {y}{−ₙ z}) ]-sym
      x + (y + 𝐏(−ₙ(z)))   🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x) (congruence₂ᵣ(_+_)(y) [𝐏]-negative) ]
      x + (y + (−𝐒ₙ(z)))   🝖-end
    -}

instance
  [+]-monoid : Monoid(_+_)
  [+]-monoid = intro

instance
  [+]-group : Group(_+_)
  [+]-group = intro

instance
  [+]-commutative-group : CommutativeGroup(_+_)
  [+]-commutative-group = intro

absₙ-of-[⋅] : ∀{x y} → (absₙ(x ⋅ y) ≡ absₙ(x) ℕ.⋅ absₙ(y))
absₙ-of-[⋅] {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝟎}    = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝐒 y}  = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝟎}    = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝐒 y}  = [≡]-intro
absₙ-of-[⋅] {−𝐒ₙ x}     {−𝐒ₙ y}     = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
absₙ-of-[⋅] {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
absₙ-of-[⋅] {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}    = [≡]-intro
absₙ-of-[⋅] {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝐒 y}  = [≡]-intro
absₙ-of-[⋅] {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}    = [≡]-intro
absₙ-of-[⋅] {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y}  = [≡]-intro

sign-of-[⋅] : ∀{x y} → (sign0(x ⋅ y) ≡ sign0(x) Sign.⨯ sign0(y))
sign-of-[⋅] {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝟎}    = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝟎}    {+ₙ ℕ.𝐒 y}  = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝟎}    = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝐒 x}  {+ₙ ℕ.𝐒 y}  = [≡]-intro
sign-of-[⋅] {−𝐒ₙ x}     {−𝐒ₙ y}     = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝟎}    {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝟎}   = [≡]-intro
sign-of-[⋅] {+ₙ ℕ.𝐒 x}  {−𝐒ₙ ℕ.𝐒 y} = [≡]-intro
sign-of-[⋅] {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}    = [≡]-intro
sign-of-[⋅] {−𝐒ₙ ℕ.𝟎}   {+ₙ ℕ.𝐒 y}  = [≡]-intro
sign-of-[⋅] {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}    = [≡]-intro
sign-of-[⋅] {−𝐒ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y}  = [≡]-intro

signed-inverse : ∀{x} → (signed0 (sign0 x) (absₙ x) ≡ x)
signed-inverse {+𝐒ₙ _} = [≡]-intro
signed-inverse {𝟎}     = [≡]-intro
signed-inverse {−𝐒ₙ _} = [≡]-intro

sign0-inverse : ∀{x}{y} → (sign0(signed0 x (ℕ.𝐒(y))) ≡ x)
sign0-inverse {Sign.➕} {y} = [≡]-intro
sign0-inverse {Sign.𝟎}  {y} = [≡]-intro
sign0-inverse {Sign.➖} {y} = [≡]-intro

absₙ-inverse : ∀{x}{y} → (x ≢ Sign.𝟎) → (absₙ(signed0 x y) ≡ y)
absₙ-inverse {Sign.➕} {ℕ.𝟎}   _ = [≡]-intro
absₙ-inverse {Sign.➕} {ℕ.𝐒 y} _ = [≡]-intro
absₙ-inverse {Sign.➖} {ℕ.𝟎}   _ = [≡]-intro
absₙ-inverse {Sign.➖} {ℕ.𝐒 y} _ = [≡]-intro
absₙ-inverse {Sign.𝟎} {ℕ.𝟎}    _ = [≡]-intro
absₙ-inverse {Sign.𝟎} {ℕ.𝐒 y}  p with () ← p [≡]-intro

absₙ-of-[−ₙ] : ∀{x} → (absₙ(−ₙ x) ≡ x)
absₙ-of-[−ₙ] {ℕ.𝟎}   = [≡]-intro
absₙ-of-[−ₙ] {ℕ.𝐒 x} = [≡]-intro

[⋅]-equality : ∀{x y z} → (x ⋅ y ≡ z) ↔ (sign0(x) Sign.⨯ sign0(y) ≡ sign0 z) ∧ (absₙ(x) ℕ.⋅ absₙ(y) ≡ absₙ(z))
[⋅]-equality {x}{y}{z} = [↔]-intro (Tuple.uncurry l) r where
  l : ∀{x y z} → (sign0(x) Sign.⨯ sign0(y) ≡ sign0 z) → (absₙ(x) ℕ.⋅ absₙ(y) ≡ absₙ(z)) → (x ⋅ y ≡ z)
  l{x}{y}{z} p q = congruence₂(signed0) p q 🝖 signed-inverse

  r : ∀{x y z} → (x ⋅ y ≡ z) → (sign0(x) Sign.⨯ sign0(y) ≡ sign0 z) ∧ (absₙ(x) ℕ.⋅ absₙ(y) ≡ absₙ(z))
  r{x}{y}{z} p = [∧]-intro (symmetry(_≡_) (preserving₂(sign0)(_⋅_)(Sign._⨯_)) 🝖 congruence₁(sign0) p) (symmetry(_≡_) (preserving₂(absₙ)(_⋅_)(ℕ._⋅_) {x}{y}) 🝖 congruence₁(absₙ) p)

instance
  [⋅]-identityₗ : Identityₗ(_⋅_)(𝟏)
  Identityₗ.proof [⋅]-identityₗ {x} with sign0 x | x
  ... | Sign.➕ | 𝟎     = [≡]-intro
  ... | Sign.➕ | +𝐒ₙ _ = [≡]-intro
  ... | Sign.➕ | −𝐒ₙ _ = [≡]-intro
  ... | Sign.𝟎 | 𝟎     = [≡]-intro
  ... | Sign.𝟎 | +𝐒ₙ _ = [≡]-intro
  ... | Sign.𝟎 | −𝐒ₙ _ = [≡]-intro
  ... | Sign.➖ | 𝟎     = [≡]-intro
  ... | Sign.➖ | +𝐒ₙ _ = [≡]-intro
  ... | Sign.➖ | −𝐒ₙ _ = [≡]-intro

instance
  [⋅]-identityᵣ : Identityᵣ(_⋅_)(𝟏)
  Identityᵣ.proof [⋅]-identityᵣ {x} with sign0 x | x
  ... | Sign.➕ | 𝟎     = [≡]-intro
  ... | Sign.➕ | +𝐒ₙ _ = [≡]-intro
  ... | Sign.➕ | −𝐒ₙ _ = [≡]-intro
  ... | Sign.𝟎 | 𝟎     = [≡]-intro
  ... | Sign.𝟎 | +𝐒ₙ _ = [≡]-intro
  ... | Sign.𝟎 | −𝐒ₙ _ = [≡]-intro
  ... | Sign.➖ | 𝟎     = [≡]-intro
  ... | Sign.➖ | +𝐒ₙ _ = [≡]-intro
  ... | Sign.➖ | −𝐒ₙ _ = [≡]-intro

instance
  [⋅]-commutativity : Commutativity(_⋅_)
  Commutativity.proof [⋅]-commutativity {x}{y} = congruence₂(signed0) (commutativity(Sign._⨯_)) (commutativity(ℕ._⋅_) {absₙ x}{absₙ y})

instance
  postulate [⋅]-associativity : Associativity(_⋅_)
  {-Associativity.proof [⋅]-associativity {x}{y}{z} =
    congruence₂(signed0)
      (congruence₂ₗ(Sign._⨯_)(sign0 z) sign0-inverse                                                  🝖 associativity(Sign._⨯_)                      🝖 symmetry(_≡_) (congruence₂ᵣ(Sign._⨯_)(sign0(x)) (sign-of-[⋅] {y}{z})))
      (congruence₂ₗ(ℕ._⋅_)   (absₙ(z)) (absₙ-inverse{sign0(x) Sign.⨯ sign0(y)}{absₙ(x) ℕ.⋅ absₙ(y)})  🝖 associativity(ℕ._⋅_){absₙ x}{absₙ y}{absₙ z} 🝖 symmetry(_≡_) (congruence₂ᵣ(ℕ._⋅_)   (absₙ (x)) (absₙ-of-[⋅] {y}{z})))
  -}

instance
  postulate [⋅][+]-distributivityₗ : Distributivityₗ(_⋅_)(_+_)
  {-[⋅][+]-distributivityₗ = intro p where
    p : Names.Distributivityₗ(_⋅_)(_+_)
    p {+ₙ ℕ.𝟎} {+ₙ ℕ.𝟎} {+ₙ ℕ.𝟎} = [≡]-intro
    p {+ₙ ℕ.𝟎} {+ₙ ℕ.𝟎} {+ₙ ℕ.𝐒 z} = [≡]-intro
    p {+ₙ ℕ.𝟎} {+ₙ ℕ.𝐒 y} {+ₙ ℕ.𝟎} = [≡]-intro
    p {+ₙ ℕ.𝟎} {+ₙ ℕ.𝐒 y} {+ₙ ℕ.𝐒 z} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎} {+ₙ ℕ.𝟎} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎} {+ₙ ℕ.𝐒 z} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y} {+ₙ ℕ.𝟎} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y} {+ₙ ℕ.𝐒 z} = {!!}
    p {+ₙ ℕ.𝟎} {+ₙ ℕ.𝟎} {−𝐒ₙ z} = [≡]-intro
    p {+ₙ ℕ.𝟎} {+ₙ ℕ.𝐒 y} {−𝐒ₙ z} = {!!}
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎} {−𝐒ₙ z} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y} {−𝐒ₙ z} = {!!}
    p {+ₙ ℕ.𝟎} {−𝐒ₙ y} {+ₙ ℕ.𝟎} = [≡]-intro
    p {+ₙ ℕ.𝟎} {−𝐒ₙ y} {+ₙ ℕ.𝐒 z} = {!!}
    p {+ₙ ℕ.𝐒 x} {−𝐒ₙ y} {+ₙ ℕ.𝟎} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {−𝐒ₙ y} {+ₙ ℕ.𝐒 z} = {!!}
    p {+ₙ ℕ.𝟎} {−𝐒ₙ y} {−𝐒ₙ z} = [≡]-intro
    p {+ₙ ℕ.𝐒 x} {−𝐒ₙ y} {−𝐒ₙ z} = {!!}
    p {−𝐒ₙ x} {+ₙ ℕ.𝟎} {+ₙ ℕ.𝟎} = [≡]-intro
    p {−𝐒ₙ x} {+ₙ ℕ.𝟎} {+ₙ ℕ.𝐒 z} = [≡]-intro
    p {−𝐒ₙ x} {+ₙ ℕ.𝐒 y} {+ₙ ℕ.𝟎} = [≡]-intro
    p {−𝐒ₙ x} {+ₙ ℕ.𝐒 y} {+ₙ ℕ.𝐒 z} = {!!}
    p {−𝐒ₙ x} {+ₙ ℕ.𝟎} {−𝐒ₙ z} = [≡]-intro
    p {−𝐒ₙ x} {+ₙ ℕ.𝐒 y} {−𝐒ₙ z} = {!!}
    p {−𝐒ₙ x} {−𝐒ₙ y} {+ₙ ℕ.𝟎} = [≡]-intro
    p {−𝐒ₙ x} {−𝐒ₙ y} {+ₙ ℕ.𝐒 z} = {!!}
    p {−𝐒ₙ x} {−𝐒ₙ y} {−𝐒ₙ z} = {!!}-}
  {-
    x ⋅ (y + z)                                                                                🝖[ _≡_ ]-[]
    signed0 ((sign0 x) Sign.⨯ (sign0(y + z))) ((absₙ x) ℕ.⋅ (absₙ(y + z)))                                                          🝖[ _≡_ ]-[ {!congruence₂(signed0) ? ?!} ]
    signed0 ((sign0 x) Sign.⨯ sign0(y + z)) ((absₙ x) ℕ.⋅ (absₙ(y + z)))                                                          🝖[ _≡_ ]-[ {!!} ]
    (signed0 ((sign0 x) Sign.⨯ (sign0 y)) ((absₙ x) ℕ.⋅ (absₙ y))) + (signed0 ((sign0 x) Sign.⨯ (sign0 z)) ((absₙ x) ℕ.⋅ (absₙ z))) 🝖[ _≡_ ]-[]
    (x ⋅ y) + (x ⋅ z)                                                                                🝖-end
    where
      sign0-proof : ∀{x y z} → ((sign0 x) Sign.⨯ sign0(y + z) ≡ (sign0(x) + sign0(z)) Sign.⨯ (sign0(x) + sign0(z)))
  -}

instance
  postulate [⋅][+]-distributivityᵣ : Distributivityᵣ(_⋅_)(_+_)

instance
  postulate [⋅][−]-distributivityₗ : Distributivityₗ(_⋅_)(_−_)

instance
  postulate [⋅][−]-distributivityᵣ : Distributivityᵣ(_⋅_)(_−_)

instance
  [+][⋅]-rng : Rng(_+_)(_⋅_)
  [+][⋅]-rng = record{}

instance
  [+][⋅]-ring-unity : Unity(_+_)(_⋅_)
  Unity.[⋅]-identity-existence [+][⋅]-ring-unity = [∃]-intro 𝟏 ⦃ intro ⦄

instance
  [+][⋅]-ring : Ring(_+_)(_⋅_)
  [+][⋅]-ring = record{}

import      Numeral.Natural.Relation.Order as ℕ
import      Numeral.Natural.Relation.Order.Proofs as ℕ
import      Structure.Relator.Ordering as Structure
data _≤_ : ℤ → ℤ → Type{Lvl.𝟎} where
  pos : ∀{a b} → (a ℕ.≤ b) → ((+ₙ a) ≤ (+ₙ b))
  neg : ∀{a b} → (a ℕ.≥ b) → ((−𝐒ₙ a) ≤ (−𝐒ₙ b))
  mix : ∀{a b} → ((−𝐒ₙ a) ≤ (+ₙ b))

instance
  [≤]-reflexivity : Reflexivity(_≤_)
  Reflexivity.proof [≤]-reflexivity {+ₙ  x} = pos (reflexivity(ℕ._≤_))
  Reflexivity.proof [≤]-reflexivity {−𝐒ₙ x} = neg (reflexivity(ℕ._≤_))

instance
  [≤]-transitivity : Transitivity(_≤_)
  Transitivity.proof [≤]-transitivity (pos p) (pos q) = pos(transitivity(ℕ._≤_) p q)
  Transitivity.proof [≤]-transitivity (neg p) (neg q) = neg(transitivity(ℕ._≤_) q p)
  Transitivity.proof [≤]-transitivity (neg p) mix     = mix
  Transitivity.proof [≤]-transitivity mix     (pos q) = mix

instance
  [≤]-antisymmetry : Antisymmetry(_≤_)(_≡_)
  Antisymmetry.proof [≤]-antisymmetry (pos {ℕ.𝟎}   {ℕ.𝟎}   p) (pos q) = [≡]-intro
  Antisymmetry.proof [≤]-antisymmetry (neg {ℕ.𝟎}   {ℕ.𝟎}   p) (neg q) = [≡]-intro
  Antisymmetry.proof [≤]-antisymmetry (pos {ℕ.𝐒 a} {ℕ.𝐒 b} p) (pos q) = congruence₁(+ₙ_)  (antisymmetry(ℕ._≤_)(_≡_) p q)
  Antisymmetry.proof [≤]-antisymmetry (neg {ℕ.𝐒 a} {ℕ.𝐒 b} p) (neg q) = congruence₁(−𝐒ₙ_) (antisymmetry(ℕ._≤_)(_≡_) q p)

instance
  [≤]-converseTotal : ConverseTotal(_≤_)
  ConverseTotal.proof [≤]-converseTotal {+ₙ  x} {+ₙ  y} = Either.map pos pos (converseTotal(ℕ._≤_))
  ConverseTotal.proof [≤]-converseTotal {+ₙ  x} {−𝐒ₙ y} = Either.Right mix
  ConverseTotal.proof [≤]-converseTotal {−𝐒ₙ x} {+ₙ  y} = Either.Left  mix
  ConverseTotal.proof [≤]-converseTotal {−𝐒ₙ x} {−𝐒ₙ y} = Either.map neg neg (converseTotal(ℕ._≤_))

instance
  [≤]-weakPartialOrder : Structure.Weak.PartialOrder(_≤_)(_≡_)
  [≤]-weakPartialOrder = record{}

instance
  [≤]-totalOrder : Structure.Weak.TotalOrder(_≤_)(_≡_)
  [≤]-totalOrder = record{}

instance
  [+][⋅][≤]-orderedRing : Ordered(_+_)(_⋅_)(_≤_)
  Ordered.[≤][+]ₗ-preserve  [+][⋅][≤]-orderedRing = p where
    postulate p : ∀{x y z} → (x ≤ y) → ((x + z) ≤ (y + z))
    {-p {+ₙ x}    {+ₙ y}     {+ₙ  z} (pos xy) = pos {!!}
    p {−𝐒ₙ x}   {−𝐒ₙ y}    {−𝐒ₙ z} (neg xy) = neg {!!}
    p {+ₙ ℕ.𝟎}  {+ₙ ℕ.𝟎}   {−𝐒ₙ z} (pos xy) = reflexivity(_≤_)
    p {+ₙ ℕ.𝟎}  {+ₙ ℕ.𝐒 y} {−𝐒ₙ z} (pos xy) = {!!}
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y}{−𝐒ₙ z} (pos xy) = {!!}
    p {.(−𝐒ₙ _)} {.(+ₙ _)} {+ₙ  z} mix = {!!}
    p {.(−𝐒ₙ _)} {.(+ₙ _)} {−𝐒ₙ z} mix = {!!}-}
  Ordered.[≤][⋅]-zero       [+][⋅][≤]-orderedRing = p where
    p : ∀{x y} → (𝟎 ≤ x) → (𝟎 ≤ y) → (𝟎 ≤ (x ⋅ y))
    p {+ₙ ℕ.𝟎}   {+ₙ ℕ.𝟎}   (pos px) (pos py) = pos py
    p {+ₙ ℕ.𝟎}   {+ₙ ℕ.𝐒 y} (pos px) (pos py) = pos px
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝟎}   (pos px) (pos py) = pos py
    p {+ₙ ℕ.𝐒 x} {+ₙ ℕ.𝐒 y} (pos px) (pos py) = pos ℕ.[≤]-minimum

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Representation-independent results for non-dependent lenses
------------------------------------------------------------------------

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

import Equality.Path as P

module Lens.Non-dependent
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bij using (module _↔_)
open import Equivalence equality-with-J using (_≃_)
open import Erased.Cubical eq
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import Surjection equality-with-J using (_↠_)

private
  variable
    a b c c₁ c₂ c₃    : Level
    A B               : Set a
    Lens₁ Lens₂ Lens₃ : Set a → Set b → Set c

------------------------------------------------------------------------
-- An existence result

-- There is, in general, no lens for the first projection from a
-- Σ-type, assuming that lenses with contractible domains have
-- contractible codomains.

no-first-projection-lens :
  (Lens : Set (a ⊔ b) → Set a → Set c) →
  @0 (∀ {A B} → Lens A B → Contractible A → Contractible B) →
  ∃ λ (A : Set a) → ∃ λ (B : A → Set b) →
    ¬ Lens (Σ A B) A
no-first-projection-lens {b = b} _ contractible-to-contractible =
  ↑ _ Bool ,
  (λ b → ↑ _ (lower b ≡ true)) ,
  λ l →                                           $⟨ singleton-contractible _ ⟩
     Contractible (Singleton true)                ↝⟨ H-level.respects-surjection surj 0 ⟩
     Contractible (∃ λ b → ↑ _ (lower b ≡ true))  ↝⟨ (λ hyp → [ contractible-to-contractible l hyp ]) ⟩
     Erased (Contractible (↑ _ Bool))             ↝⟨ Erased-cong (H-level.respects-surjection (_↔_.surjection Bij.↑↔) 0) ⟩
     Erased (Contractible Bool)                   ↝⟨ Erased-cong (mono₁ 0) ⟩
     Erased (Is-proposition Bool)                 ↝⟨ inverse-ext? ¬-Erased↔¬ _ ¬-Bool-propositional ⟩□
     ⊥                                            □
  where
  surj : Singleton true ↠ ∃ λ b → ↑ _ (lower b ≡ true)
  surj = record
    { logical-equivalence = record
      { to   = λ { (b , b≡true) → lift b , lift b≡true }
      ; from = λ { (lift b , lift b≡true) → b , b≡true }
      }
    ; right-inverse-of = refl
    }

------------------------------------------------------------------------
-- Statements of preservation results, and some related lemmas

-- Lens-like things with getters and setters.

record Has-getter-and-setter
         (Lens : Set a → Set b → Set c) :
         Set (lsuc (a ⊔ b ⊔ c)) where
  field
    -- Getter.
    get : {A : Set a} {B : Set b} → Lens A B → A → B

    -- Setter.
    set : {A : Set a} {B : Set b} → Lens A B → A → B → A

-- A statement of what it means for two lenses to have the same getter
-- and setter.

Same-getter-and-setter :
  {Lens₁ : Set a → Set b → Set c₁}
  {Lens₂ : Set a → Set b → Set c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  {A : Set a} {B : Set b} →
  Lens₁ A B → Lens₂ A B → Set (a ⊔ b)
Same-getter-and-setter ⦃ L₁ = L₁ ⦄ ⦃ L₂ = L₂ ⦄ l₁ l₂ =
  get L₁ l₁ ≡ get L₂ l₂ ×
  set L₁ l₁ ≡ set L₂ l₂
  where
  open Has-getter-and-setter

-- A statement of what it means for a function to preserve getters and
-- setters for all inputs.

Preserves-getters-and-setters-→ :
  {Lens₁ : Set a → Set b → Set c₁}
  {Lens₂ : Set a → Set b → Set c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  (A : Set a) (B : Set b) →
  (Lens₁ A B → Lens₂ A B) →
  Set (a ⊔ b ⊔ c₁)
Preserves-getters-and-setters-→ {Lens₁ = Lens₁} A B f =
  (l : Lens₁ A B) → Same-getter-and-setter (f l) l

-- A statement of what it means for a logical equivalence to preserve
-- getters and setters.

Preserves-getters-and-setters-⇔ :
  {Lens₁ : Set a → Set b → Set c₁}
  {Lens₂ : Set a → Set b → Set c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  (A : Set a) (B : Set b) →
  (Lens₁ A B ⇔ Lens₂ A B) →
  Set (a ⊔ b ⊔ c₁ ⊔ c₂)
Preserves-getters-and-setters-⇔ A B eq =
  Preserves-getters-and-setters-→ A B (_⇔_.to eq) ×
  Preserves-getters-and-setters-→ A B (_⇔_.from eq)

-- Composition preserves Preserves-getters-and-setters-→.

Preserves-getters-and-setters-→-∘ :
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  ⦃ L₃ : Has-getter-and-setter Lens₃ ⦄
  {f : Lens₂ A B → Lens₃ A B}
  {g : Lens₁ A B → Lens₂ A B} →
  Preserves-getters-and-setters-→ A B f →
  Preserves-getters-and-setters-→ A B g →
  Preserves-getters-and-setters-→ A B (f ∘ g)
Preserves-getters-and-setters-→-∘ p-f p-g _ =
    trans (proj₁ (p-f _)) (proj₁ (p-g _))
  , trans (proj₂ (p-f _)) (proj₂ (p-g _))

-- Composition preserves Preserves-getters-and-setters-⇔.

Preserves-getters-and-setters-⇔-∘ :
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  ⦃ L₃ : Has-getter-and-setter Lens₃ ⦄
  {f : Lens₂ A B ⇔ Lens₃ A B}
  {g : Lens₁ A B ⇔ Lens₂ A B} →
  Preserves-getters-and-setters-⇔ A B f →
  Preserves-getters-and-setters-⇔ A B g →
  Preserves-getters-and-setters-⇔ A B (f F.∘ g)
Preserves-getters-and-setters-⇔-∘ p-f p-g =
    Preserves-getters-and-setters-→-∘ (proj₁ p-f) (proj₁ p-g)
  , Preserves-getters-and-setters-→-∘ (proj₂ p-g) (proj₂ p-f)

-- The function inverse preserves Preserves-getters-and-setters-⇔.

Preserves-getters-and-setters-⇔-inverse :
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  {f : Lens₁ A B ⇔ Lens₂ A B} →
  Preserves-getters-and-setters-⇔ A B f →
  Preserves-getters-and-setters-⇔ A B (inverse f)
Preserves-getters-and-setters-⇔-inverse = swap

-- If the forward direction of a split surjection preserves getters
-- and setters, then both directions do.

Preserves-getters-and-setters-→-↠-⇔ :
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  (f : Lens₁ A B ↠ Lens₂ A B) →
  Preserves-getters-and-setters-→ A B (_↠_.to f) →
  Preserves-getters-and-setters-⇔ A B (_↠_.logical-equivalence f)
Preserves-getters-and-setters-→-↠-⇔ ⦃ L₁ = L₁ ⦄ ⦃ L₂ = L₂ ⦄ f p =
    p
  , λ l →
        (get L₁ (_↠_.from f l)             ≡⟨ sym $ proj₁ $ p (_↠_.from f l) ⟩
         get L₂ (_↠_.to f (_↠_.from f l))  ≡⟨ cong (get L₂) $ _↠_.right-inverse-of f _ ⟩∎
         get L₂ l                          ∎)
      , (set L₁ (_↠_.from f l)             ≡⟨ sym $ proj₂ $ p (_↠_.from f l) ⟩
         set L₂ (_↠_.to f (_↠_.from f l))  ≡⟨ cong (set L₂) $ _↠_.right-inverse-of f _ ⟩∎
         set L₂ l                          ∎)
  where
  open Has-getter-and-setter

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


text:
module _ where

open import Agda.Primitive

-- Named implicit parameters

data D₁ {a b} (A : Set a) (B : Set b) : Set (a ⊔ lsuc b)
data D₁ {b = c} X Y where
  mkD₁ : Set c → D₁ X Y

-- Trailing implicit parameters

data D₂ {a} : Set a
data D₂ where
  tt : D₂

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.List where

open import Data.List.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Data.Tuple.Function where

open import Data
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Type

module _ {ℓ₁ ℓ₂ ℓ₃} {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} where
  _,⃝_ : (T₁ → T₂) → (T₁ → T₃) → (T₁ → (T₂ ⨯ T₃))
  _,⃝_ f g x = (f(x) , g(x))

  left : (T₁ → (T₂ ⨯ T₃)) → (T₁ → T₂)
  left =  Tuple.left ∘_

  right : (T₁ → (T₂ ⨯ T₃)) → (T₁ → T₃)
  right =  Tuple.right ∘_


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Nat where

open import Cubical.Data.Nat.Base public

open import Cubical.Data.Nat.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- The <local hints> in an ATP pragma <prove> can be data constructors.

module ATPLocalHints1 where

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

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

postulate
  0-N : N zero
{-# ATP prove 0-N zN #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module UselessAbstractAbstract where

A : Set₁
abstract
  abstract
    A = Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Pair where

postulate
  _,_ : Set → Set → Set
  fst : {A B : Set} → (A , B) → A
  snd : {A B : Set} → (A , B) → B

{-# COMPILE GHC _,_ = type (,) #-}
{-# COMPILE GHC fst = \ _ _ -> fst #-}
{-# COMPILE GHC snd = \ _ _ -> snd #-}

max_stars_repo_name: cruhland/agda-editor

max_issues_repo_name: cruhland/agda-editor

max_forks_repo_name: cruhland/agda-editor


text:
-- Andreas, 2017-09-16, issue #2759
-- Allow empty declaration blocks in the parser.

open import Agda.Builtin.Nat

x0 = zero
mutual
x1 = suc x0
abstract
x2 = suc x1
private
x3 = suc x2
instance
x4 = suc x3
macro
x5 = suc x4
postulate
x6 = suc x5

-- Expected: 6 warnings about empty blocks

mutual
  postulate

-- Empty postulate block.

abstract private instance macro

-- Empty macro block.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Refl datatype and functions required for equational reasoning.   --
----------------------------------------------------------------------

module Basics.Reasoning where

open import Basics.Nat hiding (_≥_)
open import Basics.Ordering

-- Basic definition we will need in our proofs is propositional
-- equality (known as refl). Unlike refl definition provided by Agda's
-- standard library the definition below is not universe
-- polymorphic. It works only on Set, but not on Set1 and higher Sets
-- - this will be perfectly sufficient for our purposes. This datatype
-- allows to express equality between types belonging to Set.
data _≡_ {S : Set} (s : S) : S → Set where
  refl : s ≡ s

infixl 1 _≡_

-- Below we prove basic properties of relations: symmetry,
-- transitivity, congruence and substitution. If these proofs are not
-- familiar I encourage to take a look at tutorials on Agda Wiki. The
-- most useful source in my opinion are the online lecture notes for
-- the Computer Aided Formal Reasoning course by Thorsten Altenkirch:
--
-- http://www.cs.nott.ac.uk/~txa/g53cfr/
sym : {A : Set} → {a b : A} → a ≡ b → b ≡ a
sym refl = refl

trans : {A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

cong : {A B : Set} (f : A → B) → ∀ {a b} → a ≡ b → f a ≡ f b
cong f refl = refl

subst : {A : Set}(P : A → Set) → {a b : A} → a ≡ b → P a → P b
subst prp refl p = p

-- We prove some basic properties of addition that we will need later
-- in more complex proofs. I assume that you had previous exposure to
-- these basic proofs, but nevertheless I provide extensive
-- explanations. Make sure you understand how these proofs work before
-- proceeding with rest of the paper.

-- Note [0 is right identity of addition]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- The fact that 0 is left identity of addition (ie. 0 + a ≡ a)
-- follows directly from our definition of _+_:
--
--   _+_ : Nat → Nat → Nat
--   zero  + m = m
--   suc n + m = suc (n + m)
--
-- But we need a separate proof that 0 is also right identity of
-- addition, ie. a + 0 ≡ a. Proof proceeds by induction on a. If a is
-- zero then we have:
--
--   0 + 0 = 0
--
-- And the proof follows from the definition of addition - hence we
-- use refl. In a recursive case we have:
--
--   (suc a) + zero ≡ (suc a)
--
-- Applying definition of addition to LHS we have:
--
--   suc (a + zero) ≡ suc a
--
-- Since we have suc on both sides of the equality, we use
-- congruence. This leaves us with a proof that equality holds for the
-- parameters of suc:
--
--   a + zero ≡ a
--
-- But that happens to be the equality we are proving at the
-- moment. We therefore make a recursive call to (+0 a), which is
-- equivalent of applying inductive hypothesis in an inductive proof.
--
-- ∎

+0 : (a : Nat) → a + zero ≡ a -- See Note [0 is right identity of addition]
+0 zero    = refl
+0 (suc a) = cong suc (+0 a)

-- Note [1 + (a + b) equals a + (1 + b)]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- We will need this property surprisingly often. We proceed by
-- inductive proof on a. In the base case, when a = 0, we have:
--
--   suc (0 + b) ≡ 0 + (suc b)
--
-- Applying definition of + to both sides of equality we get:
--
--   suc b ≡ suc b
--
-- Which is true by definition, hence we use refl. In the recursive
-- case we have:
--
--   suc ((suc a) + b) ≡ (suc a) + (suc b)
--
-- We apply definition of + to both sides and get:
--
--   suc (suc (a + b)) ≡ suc (a + (suc b))
--
-- Again, since we have suc on both sides we use congruence and are
-- left with a proof:
--
--   suc (a + b) ≡ a + (suc b)
--
-- Which again is the equality we are proving. We appeal to inductive
-- hypothesis by making a recursive call.
--
-- ∎

+suc : (a b : Nat) → suc (a + b) ≡ a + (suc b)
+suc zero b    = refl
+suc (suc a) b = cong suc (+suc a b)

-- Note [Commutativity of addition]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- Everyone knows that a + b ≡ b + a. But Agda won't take our word and
-- requires a formal proof. Let's proceed by induction on second
-- argument. In the base case we have:
--
--   a + 0 ≡ 0 + a
--
-- Right side reduces by the definition of + which leaves us with
--
--   a + 0 ≡ a
--
-- We proved that earlier so we appeal to already existing proof. In
-- the inductive case we have:
--
--   a + suc b ≡ (suc b) + a      [1]
--
-- Right hand side reduces by definition of + giving us:
--
--   a + suc b ≡ suc (b + a)      [2]
--
-- [2] is therefore the equality we have to prove. From +suc we know
-- that
--
--   suc (a + b) ≡ a + (suc b)    [3]
--
-- And we can use that to transform left hand side of [1]. Note
-- however that in order to apply [3] to left hand side of [1] we need
-- to reverse sides of the equality [3]:
--
--   a + (suc b) ≡ suc (a + b)    [4]
--
-- We achieve this by using symmetry.
--
-- Looking at right hand sides of [2] and [4] we see they differ by
-- the order of arguments to +. We can prove them equal by using
-- congruence on suc and appealing to our inductive hypothesis of
-- commutativity of addition. This means we have proven two things:
--
--   a + (suc b) ≡ suc (a + b)   [4, repeated], from symmetry of +suc
--   suc (a + b) ≡ suc (b + a)   [5], from congruence on suc and
--                               inductive hypothesis
--
-- Combining [4] and [5] using transitivity yields the proof of [2].
--
-- ∎
--
-- Here is a diagram, showing how code relates to the proof:
--
--                                 a + b ≡ b + a
--                                   ____|____
--                                  /         \
-- trans (sym (+suc a b)) (cong suc (+comm a b))
--       ̲\_____________/   \__________________/
--              |                    |
--  a + (suc b) ≡ suc (a + b)        |
--                       suc (a + b) ≡ suc (b + a)

+comm : (a b : Nat) → a + b ≡ b + a
+comm a zero    = +0 a
+comm a (suc b) = trans (sym (+suc a b)) (cong suc (+comm a b))

-- Note [Associativity of addition]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- We proceed by induction on the first parameter. In the base case we
-- have a = 0:
--
--   0 + (b + c) ≡ (0 + b) + c
--
-- Both sides can be normalized using the definition of + giving us
--
--   b + c ≡ b + c
--
-- Since this is true by definition we use refl. In the inductive case
-- we have to prove:
--
--   suc a + (b + c) ≡ (suc a + b) + c
--
-- Again, Agda normalizes each side using definition of + :
--
--   LHS: suc a + (b + c) ≡ suc (a + (b + c))
--   RHS: (suc a + b) + c ≡ suc (a + b) + c ≡ suc ((a + b) + c)
--
-- This means we have to prove:
--
--   suc (a + (b + c)) ≡ suc ((a + b) + c)
--
-- We can use congruence to remove the outer suc on both sides which
-- leaves us with a proof of:
--
--   a + (b + c) ̄≡ (a + b) + c
--
-- Which happens to be our inductive hypothesis - hence a recursive
-- call to +assoc.
--
-- ∎

+assoc : (a b c : Nat) → a + (b + c) ≡ (a + b) + c
+assoc zero b c    = refl
+assoc (suc a) b c = cong suc (+assoc a b c)

-- Note [If numbers are equal they are in the greater-equal relation]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- Finally, we need a proof that if a = b then a ≥ b. This property is
-- specific to our task, so you most likely haven't seen it other
-- tutorials. There are three interesting things in this proof:
--
--  1) a value of type m ≥ n proves that m is greater-equal than n. We
--     therefore need to construct the value of this type.
--
--  2) since refl is the only constructor of type ≡ we always use refl
--     when pattern matching on a value of ≡. We also always pass refl
--     as a value of ≡ in calls.
--
--  3) we need to match on implicit parameters to construct a
--     proof. Note that although type signature specifies Nats m and
--     n, in the proof we require that these are always equal.  This
--     requirement comes from the fact that m ≡ n, i.e. that m and n
--     are equal.
--
-- In the base case we need to construct a proof that 0 ≥ 0, which we
-- do by using ge0. Inductive case simply applies geS to result of
-- recursive call to ≥sym.

≥sym : {m n : Nat} → m ≡ n → m ≥ n
≥sym {zero}     {zero}    refl = ge0
≥sym {.(suc n)} {(suc n)} refl = geS (≥sym {n} {n} refl)

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps