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.Base.Types
open import LibraBFT.Concrete.Records
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.EpochManager
import      LibraBFT.Impl.Consensus.BlockStorage.BlockStore            as BlockStore
import      LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockStore as BlockStoreProps
import      LibraBFT.Impl.Consensus.ConsensusTypes.ExecutedBlock       as ExecutedBlock
import      LibraBFT.Impl.Consensus.Liveness.RoundState                as RoundState
import      LibraBFT.Impl.Consensus.Liveness.ProposerElection          as ProposerElection
import      LibraBFT.Impl.Consensus.PersistentLivenessStorage          as PersistentLivenessStorage
import      LibraBFT.Impl.Consensus.PersistentLivenessStorage.Properties as PersistentLivenessStorageProps
open import LibraBFT.Impl.Consensus.RoundManager
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRules            as SafetyRules
import      LibraBFT.Impl.Consensus.SafetyRules.Properties.SafetyRules as SafetyRulesProps
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Hash
open import Util.Lemmas
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open OutputProps
open Invariants
open RoundManagerTransProps

-- This module contains properties that are only about the behavior of the handlers, nothing to do
-- with system state

module LibraBFT.Impl.Consensus.RoundManager.Properties where

module executeAndVoteMSpec (vb : ValidBlock) where
  b = vbBlock vb

  open executeAndVoteM b
  open SafetyRulesProps
  open import LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockStore

  isbQc = (_≡ b ^∙ bQuorumCert)

  VoteResultCorrect : (pre post : RoundManager) (lvr≡? : Bool) (r : Either ErrLog Vote) → Set
  VoteResultCorrect pre post lvr≡? (Left _) =
    VoteNotGenerated pre post lvr≡? ⊎ Voting.VoteGeneratedUnsavedCorrect pre post b
  VoteResultCorrect pre post lvr≡? (Right vote) =
    Voting.VoteGeneratedCorrect pre post vote b

  module _ (pre : RoundManager) where

    open QCProps
    open Invariants.Reqs b (pre ^∙ lBlockTree)

    record Contract (r : Either ErrLog Vote) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General properties / invariants
        rmInv         : Preserves RoundManagerInv pre post
        noEpochChange : NoEpochChange pre post
        noMsgOuts     : OutputProps.NoMsgs outs
        -- Voting
        lvr≡?             : Bool
        voteResultCorrect : NoHC1 → VoteResultCorrect pre post lvr≡? r
        -- QCs
        qcPost : ∈Post⇒∈PreOr isbQc pre post

    contract' :
      LBFT-weakestPre (executeAndVoteM b) Contract pre
    contract' =
      executeAndInsertBlockMSpec.contract vb pre Post₀
        (λ where e ._ refl → contractBail [] refl)
        contract₁
      where
      Post₀ : LBFT-Post (Either ErrLog ExecutedBlock)
      Post₀ = RWS-weakestPre-∙^∙Post unit (withErrCtx ("" ∷ []))
                (RWS-weakestPre-ebindPost unit step₁ Contract)

      contractBail : ∀ {e} outs → OutputProps.NoMsgs outs → Contract (Left e) pre outs
      contractBail{e} outs noMsgOuts =
        mkContract
          reflPreservesRoundManagerInv (reflNoEpochChange{pre})
          noMsgOuts true (const vrc)
          qcPost
        where
        vrc : VoteResultCorrect pre pre true (Left e)
        vrc = inj₁ reflVoteNotGenerated

        qcPost : ∈Post⇒∈PreOr isbQc pre pre
        qcPost qc = Left

      module EAIBM = executeAndInsertBlockMSpec vb
      module EAIBE = executeAndInsertBlockESpec (EAIBM.bs pre) vb
      module _ (isOk : EAIBE.Ok) (con : EAIBE.ContractOk (proj₁ isOk) (proj₁ (proj₂ isOk))) where

        module EAIBECon = EAIBE.ContractOk con

        bs' = proj₁ isOk
        eb  = proj₁ (proj₂ isOk)

        pre₁ = pre & rmBlockStore ∙~ bs'

        -- State invariants
        module _  where
          bsP : Preserves BlockStoreInv (rm→BlockStore-EC pre) (rm→BlockStore-EC pre₁)
          bsP bsi = EAIBECon.bsInv bsi

          srP : Preserves SafetyRulesInv (pre ^∙ lSafetyRules) (pre₁ ^∙ lSafetyRules)
          srP = mkPreservesSafetyRulesInv id

        invP₁ : Preserves RoundManagerInv pre pre₁
        invP₁ = mkPreservesRoundManagerInv id id bsP srP

        qcPost-BT : _
        qcPost-BT = ∈Post⇒∈PreOrBT-QCs≡ isbQc
                                        (cong (_^∙ bsInner ∙ btHighestCommitCert) EAIBECon.bs≡x)
                                        (cong (_^∙ bsInner ∙ btHighestQuorumCert) EAIBECon.bs≡x)

        qcPost₁ : ∈Post⇒∈PreOr isbQc pre pre₁
        qcPost₁ = ∈Post⇒∈PreOr-∙-BT-RM isbQc pre pre₁ qcPost-BT

        -- For the case any of the checks in `step₁` fails
        contractBail₁ : ∀ {e} outs → OutputProps.NoMsgs outs → Contract (Left e) pre₁ outs
        contractBail₁ outs noMsgOuts =
          mkContract invP₁ refl
            noMsgOuts true (const $ inj₁ (mkVoteNotGenerated refl refl))
            qcPost₁

        contract₁ : Post₀ (Right eb) pre₁ []
        proj₁ (contract₁ ._ refl ._ refl ._ refl ._ refl ._ refl) _ = contractBail₁ [] refl
        proj₁ (proj₂ (contract₁ ._ refl ._ refl ._ refl ._ refl ._ refl) _) _ = contractBail₁ [] refl
        proj₂ (proj₂ (contract₁ ._ refl ._ refl ._ refl ._ refl ._ refl) _) _ = contract₂
          where
          maybeSignedVoteProposal' = ExecutedBlock.maybeSignedVoteProposal eb

          module CASV = constructAndSignVoteMSpec

          proposedBlock = CASV.proposedBlock maybeSignedVoteProposal'

          Post₂ : LBFT-Post (Either ErrLog Vote)
          Post₂ = RWS-weakestPre-ebindPost unit step₃ Contract

          contract₂ : RWS-weakestPre (step₂ eb) Contract unit pre₁

          contract₂⇒ : RWS-Post-⇒ (CASV.Contract pre₁ proposedBlock) Post₂
          contract₂⇒ r pre₃ outs con = contract₂⇒-help r CASVCon.voteResCorrect
            where
            module CASVCon = CASV.Contract con
            CASVouts = outs

            invP₂ = transPreservesRoundManagerInv invP₁ CASVCon.rmInv

            qcPost₂ : QCProps.∈Post⇒∈PreOr (_≡ b ^∙ bQuorumCert) pre pre₃
            qcPost₂ = obm-dangerous-magic' "TODO: waiting on `constructAndSignVoteM` contract"

            contract₂⇒-help :
              (r : Either ErrLog Vote) (vrc : CASV.VoteResultCorrect pre₁ pre₃ proposedBlock CASVCon.lvr≡? r)
              → RWS-weakestPre-ebindPost unit step₃ Contract r pre₃ outs
            contract₂⇒-help (Left _) vrc =
              mkContract invP₂ CASVCon.noEpochChange CASVCon.noMsgOuts
                CASVCon.lvr≡? (const ∘ Left $ (transVoteNotGenerated (mkVoteNotGenerated refl refl) vrc))
                qcPost₂
            contract₂⇒-help (Right vote) vrc ._ refl = contract₃
              where

              open RoundManagerInv
              open BlockStoreInv
              open BlockTreeInv

              contract₃ : RWS-weakestPre (step₃ vote) (RWS-Post++ Contract CASVouts) unit pre₃
              contract₃ =
                PersistentLivenessStorageProps.saveVoteMSpec.contract vote
                  Post₃ pre₃
                  contractBail₃ contractOk₃
                where
                Post₃ : LBFT-Post (Either ErrLog Unit)
                Post₃ = RWS-weakestPre-ebindPost unit (const $ ok vote) (RWS-Post++ Contract CASVouts)

                vgc₃ : NoHC1 → Voting.VoteGeneratedCorrect pre pre₃ vote b {- proposedBlock -}
                vgc₃ nohc =
                  Voting.glue-VoteNotGenerated-VoteGeneratedCorrect
                    (mkVoteNotGenerated refl refl)
                    (Voting.substVoteGeneratedCorrect proposedBlock b
                      (EAIBECon.ebBlock≈ nohc)
                      vrc)

                noMsgOutsBail₃ : ∀ outs → NoMsgs outs → NoMsgs (CASVouts ++ outs)
                noMsgOutsBail₃ outs noMsgs = ++-NoMsgs CASVouts outs CASVCon.noMsgOuts noMsgs

                noMsgOutsOk₃ : ∀ outs → NoMsgs outs → NoMsgs (CASVouts ++ outs ++ [])
                noMsgOutsOk₃ outs noMsgs rewrite ++-identityʳ outs = noMsgOutsBail₃ outs noMsgs

                contractBail₃ : ∀ outs → NoMsgs outs → NoErrors outs → Post₃ (Left fakeErr) pre₃ outs
                contractBail₃ outs noMsgOuts noErrOuts =
                  mkContract invP₂ CASVCon.noEpochChange (noMsgOutsBail₃ outs noMsgOuts)
                    CASVCon.lvr≡? ((Right ∘ Voting.mkVoteGeneratedUnsavedCorrect vote) ∘ vgc₃)
                    qcPost₂

                contractOk₃ : ∀ outs → NoMsgs outs → NoErrors outs → Post₃ (Right unit) pre₃ outs
                contractOk₃ outs noMsgs noErrs unit refl =
                  mkContract invP₂ CASVCon.noEpochChange (noMsgOutsOk₃ outs noMsgs)
                    CASVCon.lvr≡? vgc₃ qcPost₂

          contract₂ = constructAndSignVoteMSpec.contract maybeSignedVoteProposal' pre₁ Post₂ contract₂⇒

    contract
      : ∀ Post
        → RWS-Post-⇒ Contract Post
        → LBFT-weakestPre (executeAndVoteM b) Post pre
    contract Post pf =
      RWS-⇒ (executeAndVoteM b) unit pre contract' pf

module processProposalMSpec (vproposal : ValidBlock) where
  proposal = vbBlock vproposal

  open import LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockStore
  open import LibraBFT.Impl.Consensus.Liveness.Properties.ProposerElection
  open        LibraBFT.Impl.Consensus.RoundManager.processProposalM proposal

  module _ (pre : RoundManager) where

    open Invariants.Reqs (vbBlock vproposal) (pre ^∙ lBlockTree)

    record Contract (u : Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
         -- General properties / invariants
        rmInv         : Preserves RoundManagerInv pre post
        noEpochChange : NoEpochChange pre post
        noProposals   : OutputProps.NoProposals outs
        -- Voting
        voteAttemptCorrect : NoHC1 → Voting.VoteAttemptCorrect pre post outs proposal
        -- QCs
        outQcs∈RM : QCProps.OutputQc∈RoundManager outs post
        qcPost    : QCProps.∈Post⇒∈PreOr (_≡ proposal ^∙ bQuorumCert) pre post

    contract' : LBFT-weakestPre (processProposalM proposal) Contract pre
    contract' ._ refl =
      isValidProposalMSpec.contract proposal pre
        (RWS-weakestPre-bindPost unit (step₁ (pre ^∙ lBlockStore)) Contract)
        (λ where
          mAuthor≡nothing ._ refl → (λ _ → contractBail refl) , (λ where ()))
        (λ where
          notValid ._ refl → (λ _ → contractBail refl) , (λ where ()))
        λ where
          vp ._ refl →
            (λ where ())
            , (λ _ →
                 (λ _ → contractBail refl)
                 , (λ _ →
                      (λ _ → contractBail refl)
                      , (λ _ → contract-step₂)))
      where
      contractBail : ∀ {outs} → OutputProps.NoMsgs outs → Contract unit pre outs
      contractBail{outs} nmo =
        mkContract reflPreservesRoundManagerInv (reflNoEpochChange{pre})
          noProposals vac outQcs qcPost
        where
          noProposals : NoProposals outs
          noProposals = OutputProps.NoMsgs⇒NoProposals outs nmo

          vac : NoHC1 → Voting.VoteAttemptCorrect pre pre outs proposal
          vac _ = Voting.voteAttemptBailed outs (OutputProps.NoMsgs⇒NoVotes outs nmo)

          outQcs : QCProps.OutputQc∈RoundManager outs pre
          outQcs = QCProps.NoMsgs⇒OutputQc∈RoundManager outs pre nmo

          qcPost : QCProps.∈Post⇒∈PreOr _ pre pre
          qcPost qc = Left

      contract-step₂ : RWS-weakestPre (executeAndVoteM proposal >>= step₂) Contract unit pre
      contract-step₂ =
        executeAndVoteMSpec.contract vproposal pre
          (RWS-weakestPre-bindPost unit step₂ Contract) pf-step₂
        where
        module EAV = executeAndVoteMSpec vproposal

        pf-step₂ : RWS-Post-⇒ (EAV.Contract pre) (RWS-weakestPre-bindPost unit step₂ Contract)
        pf-step₂ r st outs con = pf r EAVSpec.voteResultCorrect
          where
          module EAVSpec = executeAndVoteMSpec.Contract con
          rmInv₂ = transPreservesRoundManagerInv reflPreservesRoundManagerInv EAVSpec.rmInv

          pf : (r : Either ErrLog Vote) (vrc : NoHC1 → EAV.VoteResultCorrect pre st EAVSpec.lvr≡? r)
               → RWS-weakestPre-bindPost unit step₂ Contract r st outs
          pf (Left _) vrc ._ refl =
            mkContract rmInv₂ EAVSpec.noEpochChange
              noProposals
              vac
              qcOuts EAVSpec.qcPost
            where
            noMsgs : NoMsgs (outs ++ LogErr _ ∷ [])
            noMsgs = ++-NoMsgs outs (LogErr _ ∷ []) EAVSpec.noMsgOuts refl

            noProposals : NoProposals (outs ++ LogErr _ ∷ [])
            noProposals = NoMsgs⇒NoProposals (outs ++ LogErr _ ∷ []) noMsgs

            vac : NoHC1 → Voting.VoteAttemptCorrect pre st (outs ++ LogErr _ ∷ []) proposal
            vac nohc =
              inj₁ (EAVSpec.lvr≡?
                   , Voting.mkVoteUnsentCorrect
                       (NoMsgs⇒NoVotes (outs ++ LogErr _ ∷ []) noMsgs) (vrc nohc))

            qcOuts : QCProps.OutputQc∈RoundManager (outs ++ LogErr _ ∷ []) st
            qcOuts = QCProps.NoMsgs⇒OutputQc∈RoundManager (outs ++ LogErr _ ∷ []) st noMsgs

          pf (Right vote) vrc ._ refl ._ refl ._ refl =
            syncInfoMSpec.contract (st & rsVoteSent-rm ?~ vote)
              (RWS-weakestPre-bindPost unit (step₃ vote) (RWS-Post++ Contract outs))
              contract-step₃
            where
            stUpdateRS = st & rsVoteSent-rm ?~ vote

            module _
              (si : SyncInfo)
              (si≡ : si ≡ SyncInfo∙new
                            (st ^∙ lBlockStore ∙ bsHighestQuorumCert)
                            (st ^∙ lBlockStore ∙ bsHighestCommitCert)
                            (st ^∙ lBlockStore ∙ bsHighestTimeoutCert))
              where
              contract-step₃ : RWS-weakestPre (step₃ vote si) (RWS-Post++ Contract outs) unit stUpdateRS
              contract-step₃ ._ refl ._ refl ._ refl ._ refl recipient@._ refl =
                mkContract rmInv₃
                  (transNoEpochChange{i = pre}{j = st}{k = stUpdateRS} EAVSpec.noEpochChange refl)
                  (OutputProps.++-NoProposals outs _ (OutputProps.NoMsgs⇒NoProposals outs EAVSpec.noMsgOuts) refl)
                  vac
                  outQcs qcPost
                where
                vm = VoteMsg∙new vote si

                vac : NoHC1 → Voting.VoteAttemptCorrect pre stUpdateRS (outs ++ SendVote vm _ ∷ []) proposal
                vac nohc =
                  inj₂ (Voting.mkVoteSentCorrect vm recipient
                         (OutputProps.++-NoVotes-OneVote outs _ (OutputProps.NoMsgs⇒NoVotes outs EAVSpec.noMsgOuts) refl)
                         (Voting.glue-VoteGeneratedCorrect-VoteNotGenerated{s₂ = st}
                           (vrc nohc) (mkVoteNotGenerated refl refl)))

                outQcs : QCProps.OutputQc∈RoundManager (outs ++ SendVote vm _ ∷ []) stUpdateRS
                outQcs =
                  QCProps.++-OutputQc∈RoundManager{stUpdateRS}{outs}
                    (QCProps.NoMsgs⇒OutputQc∈RoundManager outs stUpdateRS EAVSpec.noMsgOuts)
                    (outQcSendVote ∷ [])
                  where
                  outQcSendVote : ∀ qc nm → qc QC∈NM nm → nm Msg∈Out (SendVote vm _) → qc QCProps.∈RoundManager stUpdateRS
                  outQcSendVote qc .(V (VoteMsg∙new vote si)) (inSI inV (withVoteSIHighQC qc≡)) inSV rewrite si≡ =
                    QCProps.inHQC (sym qc≡)
                  outQcSendVote qc .(V (VoteMsg∙new vote si)) (inSI inV (withVoteSIHighCC qc≡)) inSV =
                    QCProps.inHCC (just-injective $
                      begin
                        just qc ≡⟨ lem₁ ⟩
                        sixxx   ≡⟨ lem₂ (cong is-just (sym lem₁)) ⟩
                        just (stUpdateRS ^∙ lBlockStore ∙ bsInner ∙ btHighestCommitCert) ∎)
                    where
                    open ≡-Reasoning
                    sixxx = if (st ^∙ lBlockStore ∙ bsHighestQuorumCert) QCBoolEq (st ^∙ lBlockStore ∙ bsHighestCommitCert)
                            then nothing
                            else (just $ (st ^∙ lBlockStore ∙ bsHighestCommitCert))

                    lem₁ : just qc ≡ sixxx
                    lem₁ = begin
                      just qc ≡⟨ sym qc≡ ⟩
                      vm ^∙ vmSyncInfo ∙ sixxxHighestCommitCert ≡⟨ cong (_^∙ sixxxHighestCommitCert) si≡ ⟩
                      sixxx ∎

                    lem₂ : is-just sixxx ≡ true
                           → sixxx ≡ just (stUpdateRS ^∙ lBlockStore ∙ bsInner ∙ btHighestCommitCert)
                    lem₂ isj
                        with (st ^∙ lBlockStore ∙ bsHighestQuorumCert) QCBoolEq (st ^∙ lBlockStore ∙ bsHighestCommitCert)
                    ... | false = refl
                    ... | true = absurd false ≡ true case isj of λ ()

                qcPost : QCProps.∈Post⇒∈PreOr (_≡ proposal ^∙ bQuorumCert) pre stUpdateRS
                qcPost qc qc∈stUpdateRS = EAVSpec.qcPost qc (qc∈st qc∈stUpdateRS)
                  where
                  qc∈st : qc QCProps.∈RoundManager stUpdateRS → qc QCProps.∈RoundManager st
                  qc∈st (QCProps.inHQC qc≡) = QCProps.inHQC qc≡
                  qc∈st (QCProps.inHCC qc≡) = QCProps.inHCC qc≡

                -- state invariants
                module _ where
                  bsP : Preserves BlockStoreInv (rm→BlockStore-EC st) (rm→BlockStore-EC stUpdateRS)
                  bsP = id

                  srP : Preserves SafetyRulesInv (st ^∙ lSafetyRules) (stUpdateRS ^∙ lSafetyRules)
                  srP = mkPreservesSafetyRulesInv id

                  rmInv₃ : Preserves RoundManagerInv pre stUpdateRS
                  rmInv₃ = transPreservesRoundManagerInv rmInv₂
                           (mkPreservesRoundManagerInv id id bsP srP)

    contract : ∀ Post → RWS-Post-⇒ Contract Post → LBFT-weakestPre (processProposalM proposal) Post pre
    contract Post pf = LBFT-⇒ (processProposalM proposal) pre contract' pf

module syncUpMSpec
  (now : Instant) (syncInfo : SyncInfo) (author : Author) (_helpRemote : Bool) where

  open syncUpM now syncInfo author _helpRemote
  open import LibraBFT.Impl.Consensus.ConsensusTypes.Properties.SyncInfo
  open import LibraBFT.Impl.Consensus.BlockStorage.Properties.SyncManager

  module _ (pre : RoundManager) where

    record Contract (r : Either ErrLog Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General invariants / properties
        rmInv         : Preserves RoundManagerInv pre post
        dnmBtIdToBlk  : post ≡L pre at (lBlockTree ∙ btIdToBlock)
        noEpochChange : NoEpochChange pre post
        noVoteOuts    : OutputProps.NoVotes outs
        -- Voting
        noVote        : VoteNotGenerated pre post true
        -- QCs
        noOutQcs : QCProps.¬OutputQc outs
        qcPost    : QCProps.∈Post⇒∈PreOr (_QC∈SyncInfo syncInfo) pre post

    contract' : LBFT-weakestPre (syncUpM now syncInfo author _helpRemote) Contract pre
    contract' =
      BlockStoreProps.syncInfoMSpec.contract pre
        (RWS-weakestPre-bindPost unit step₁ Contract)
        contract₁
      where
      localSyncInfo = BlockStoreProps.syncInfoMSpec.syncInfo pre

      contract₁ : RWS-weakestPre-bindPost unit step₁ Contract (BlockStoreProps.syncInfoMSpec.syncInfo pre) pre []
      proj₂ (contract₁ localSyncInfo lsi≡) hnc≡false =
        mkContract reflPreservesRoundManagerInv refl (reflNoEpochChange{pre}) refl
          (reflVoteNotGenerated{pre})
          [] qcPost
        where
        outQcs : QCProps.OutputQc∈RoundManager [] pre
        outQcs = QCProps.NoMsgs⇒OutputQc∈RoundManager [] pre refl

        qcPost : QCProps.∈Post⇒∈PreOr _ pre pre
        qcPost qc = Left
      proj₁ (contract₁ localSyncInfo lsi≡) hcn≡true vv@._ refl =
        verifyMSpec.contract syncInfo vv pre Post₁
          contract₃
        where
        Post₁ : LBFT-Post (Either ErrLog Unit)
        Post₁ = (RWS-weakestPre-∙^∙Post unit (withErrCtx (here' []))
                  (RWS-weakestPre-ebindPost unit (λ _ → step₃ localSyncInfo vv) Contract))

        contract₃ : RWS-Post-⇒ (verifyMSpec.Contract syncInfo vv pre) Post₁
        contract₃ r st outs con ._ refl
           with VSpec.noStateChange
           where module VSpec = verifyMSpec.Contract con
        contract₃ (Left x) st outs con ._ refl
           | refl
           = mkContract VSpec.rmInv (cong (_^∙ lBlockTree ∙ btIdToBlock) VSpec.noStateChange) (reflNoEpochChange{st})
               (++-NoVotes outs [] (NoMsgs⇒NoVotes outs VSpec.noMsgOuts) refl)
               (reflVoteNotGenerated{st})
               noOutQcs qcPost
           where
           module VSpec = verifyMSpec.Contract con
           noOutQcs : QCProps.¬OutputQc (outs ++ [])
           noOutQcs = QCProps.++-¬OutputQc (QCProps.NoMsgs⇒¬OutputQc outs VSpec.noMsgOuts) []

           qcPost : QCProps.∈Post⇒∈PreOr _ st st
           qcPost qc = Left
        contract₃ (Right y) st₃ outs₃ con₃ ._ refl
           | refl = λ where
             unit refl →
               addCertsMSpec.contract syncInfo retriever st₃
                 Post₃ contract₄
           where
           Post₃ : LBFT-Post (Either ErrLog Unit)
           Post₃ = (RWS-weakestPre-∙^∙Post unit (withErrCtx (here' []))
                     (RWS-weakestPre-ebindPost unit (λ _ → step₄ localSyncInfo vv)
                       (RWS-Post++ Contract (outs₃ ++ []))))

           retriever = BlockRetriever∙new now author

           contract₄ : RWS-Post-⇒ (addCertsMSpec.Contract syncInfo retriever st₃) Post₃
           contract₄ (Left  _) st₄ outs₄ con₄ ._ refl =
             mkContract AC.rmInv AC.dnmBtIdToBlk AC.noEpochChange noVotes₄ AC.noVote noOutQcs AC.qcPost
             where
             module AC    = addCertsMSpec.Contract con₄
             module VSpec = verifyMSpec.Contract con₃

             noVotes₄ : NoVotes $ (outs₃ ++ []) ++ outs₄ ++ []
             noVotes₄ =
               ++-NoVotes (outs₃ ++ []) (outs₄ ++ [])
                 (++-NoVotes outs₃ [] (NoMsgs⇒NoVotes outs₃ VSpec.noMsgOuts) refl)
                 (++-NoVotes outs₄ [] AC.noVoteOuts refl)

             noOutQcs : QCProps.¬OutputQc ((outs₃ ++ []) ++ outs₄ ++ [])
             noOutQcs =
               QCProps.++-¬OutputQc
                 (QCProps.++-¬OutputQc
                   (QCProps.NoMsgs⇒¬OutputQc outs₃ VSpec.noMsgOuts)
                   (QCProps.NoMsgs⇒¬OutputQc [] refl))
                 (QCProps.++-¬OutputQc
                   AC.noOutQc (QCProps.NoMsgs⇒¬OutputQc [] refl))

           contract₄ (Right _) st₄ outs₄ con₄ ._ refl =
             obm-dangerous-magic' "TODO: waiting on contract for `processCertificatesM`"

    contract
      : ∀ Post → RWS-Post-⇒ Contract Post
        → LBFT-weakestPre (syncUpM now syncInfo author _helpRemote) Post pre
    contract Post pf =
      LBFT-⇒ (syncUpM now syncInfo author _helpRemote) pre
        contract' pf

module ensureRoundAndSyncUpMSpec
  (now : Instant) (messageRound : Round) (syncInfo : SyncInfo)
  (author : Author) (helpRemote : Bool) where

  open ensureRoundAndSyncUpM now messageRound syncInfo author helpRemote

  module _ (pre : RoundManager) where

    record Contract (r : Either ErrLog Bool) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General invariants / properties
        rmInv         : Preserves RoundManagerInv pre post
        dnmBtIdToBlk  : post ≡L pre at (lBlockTree ∙ btIdToBlock)
        noEpochChange : NoEpochChange pre post
        noVoteOuts    : OutputProps.NoVotes outs
        -- Voting
        noVote        : VoteNotGenerated pre post true
        -- Signatures
        noOutQcs : QCProps.¬OutputQc outs
        qcPost   : QCProps.∈Post⇒∈PreOr (_QC∈SyncInfo syncInfo) pre post

    contract'
      : LBFT-weakestPre (ensureRoundAndSyncUpM now messageRound syncInfo author helpRemote) Contract pre
    proj₁ (contract' ._ refl) _         =
      mkContract id refl refl refl vng outqcs qcPost
      where
        vng : VoteNotGenerated pre pre true
        vng = mkVoteNotGenerated refl refl

        outqcs : QCProps.¬OutputQc []
        outqcs = []

        qcPost : QCProps.∈Post⇒∈PreOr _ pre pre
        qcPost qc = Left

    proj₂ (contract' ._ refl) mrnd≥crnd = contract-step₁
      where
      contract-step₁ : LBFT-weakestPre step₁ Contract pre
      contract-step₁ = syncUpMSpec.contract now syncInfo author helpRemote pre Post contract-step₁'
        where
        Post = RWS-weakestPre-ebindPost unit (const step₂) Contract

        contract-step₁' : _
        contract-step₁' (Left  _   ) st outs con =
          mkContract SU.rmInv SU.dnmBtIdToBlk SU.noEpochChange SU.noVoteOuts SU.noVote SU.noOutQcs SU.qcPost
          where
          module SU = syncUpMSpec.Contract con
        contract-step₁' (Right unit) st outs con = contract-step₂
          where
          module SU = syncUpMSpec.Contract con

          noVoteOuts' : NoVotes (outs ++ [])
          noVoteOuts' = ++-NoVotes outs [] SU.noVoteOuts refl

          noOutQcs : QCProps.¬OutputQc (outs ++ [])
          noOutQcs =
            QCProps.++-¬OutputQc SU.noOutQcs []

          contract-step₂ : Post (Right unit) st outs
          proj₁ (contract-step₂ ._ refl ._ refl) _ =
            mkContract SU.rmInv SU.dnmBtIdToBlk SU.noEpochChange noVoteOuts' SU.noVote
              noOutQcs SU.qcPost
          proj₂ (contract-step₂ ._ refl ._ refl) _ =
            mkContract SU.rmInv SU.dnmBtIdToBlk SU.noEpochChange noVoteOuts' SU.noVote
              noOutQcs SU.qcPost

    contract : ∀ Post → RWS-Post-⇒ Contract Post → LBFT-weakestPre (ensureRoundAndSyncUpM now messageRound syncInfo author helpRemote) Post pre
    contract Post pf =
      LBFT-⇒ (ensureRoundAndSyncUpM now messageRound syncInfo author helpRemote) pre contract' pf

module processProposalMsgMSpec
  (now : Instant) (pm : ProposalMsg) (vproposal : BlockId-correct (pm ^∙ pmProposal)) where

  proposal = pm ^∙ pmProposal
  open processProposalMsgM now pm

  module _ (pre : RoundManager) where

    open Invariants.Reqs proposal (pre ^∙ lBlockTree)

    record Contract (_ : Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General invariants / properties
        rmInv         : Preserves RoundManagerInv pre post
        noEpochChange : NoEpochChange pre post
        -- Voting
        voteAttemptCorrect : NoHC1 → Voting.VoteAttemptCorrect pre post outs proposal
        -- QCs
        outQcs∈RM : QCProps.OutputQc∈RoundManager outs post
        qcPost    : QCProps.∈Post⇒∈PreOr (_QC∈NM (P pm)) pre post

    contract' : LBFT-weakestPre (processProposalMsgM now pm) Contract pre
    contract' rewrite processProposalMsgM≡ = contract
      where
      contractBail : ∀ outs → OutputProps.NoMsgs outs → Contract unit pre outs
      contractBail outs nmo =
        mkContract reflPreservesRoundManagerInv (reflNoEpochChange{pre}) vac outqcs qcPost
        where
        vac : NoHC1 → Voting.VoteAttemptCorrect pre pre outs proposal
        vac _ = Voting.voteAttemptBailed outs (OutputProps.NoMsgs⇒NoVotes outs nmo)

        outqcs : QCProps.OutputQc∈RoundManager outs pre
        outqcs = QCProps.NoMsgs⇒OutputQc∈RoundManager outs pre nmo

        qcPost : QCProps.∈Post⇒∈PreOr _ pre pre
        qcPost qc = Left

      contract : LBFT-weakestPre step₀ Contract pre
      proj₁ contract ≡nothing = contractBail _ refl
      proj₂ contract = contract-step₁
        where
        -- These arguments come from the second proof obligation of RWS-weakestPre for RWS-maybe
        module _ (pAuthor : Author) (pAuthor≡ : pm ^∙ pmProposer ≡ just pAuthor) where
          pf-step₂ : RWS-Post-⇒ _ (RWS-weakestPre-bindPost unit step₂ Contract)

          contract-step₁ : LBFT-weakestPre (step₁ pAuthor) Contract pre
          contract-step₁ =
            ensureRoundAndSyncUpMSpec.contract now (pm ^∙ pmProposal ∙ bRound) (pm ^∙ pmSyncInfo) pAuthor true pre
            (RWS-weakestPre-bindPost unit step₂ Contract)
            pf-step₂

          pf-step₂ r st outs con = pf-step₂' r
            where
            module ERASU = ensureRoundAndSyncUpMSpec.Contract con
            contractBailAfterSync : ∀ outs' → OutputProps.NoMsgs outs' → RWS-Post++ Contract outs unit st outs'
            contractBailAfterSync outs' noMsgs' =
              mkContract ERASU.rmInv ERASU.noEpochChange vac outqcs qcPost
              where
              vac : NoHC1 → Voting.VoteAttemptCorrect pre st (outs ++ outs') proposal
              vac _ = Left (true , (Voting.mkVoteUnsentCorrect
                                     (OutputProps.++-NoVotes outs _ ERASU.noVoteOuts (OutputProps.NoMsgs⇒NoVotes outs' noMsgs'))
                                     (Left ERASU.noVote)))

              outqcs : QCProps.OutputQc∈RoundManager (outs ++ outs') st
              outqcs =
                QCProps.¬OutputQc⇒OutputQc∈RoundManager (outs ++ outs') st
                  (QCProps.++-¬OutputQc ERASU.noOutQcs
                    (QCProps.NoMsgs⇒¬OutputQc outs' noMsgs'))

              qcPost : QCProps.∈Post⇒∈PreOr (_QC∈NM (P pm)) pre st
              qcPost qc qc∈st
                 with ERASU.qcPost qc qc∈st
              ... | Left qc∈pre = Left qc∈pre
              ... | Right qc∈si = Right (inSI inP qc∈si)

            pf-step₂' : (r : Either ErrLog Bool) → RWS-weakestPre-bindPost unit step₂ Contract r st outs
            pf-step₂' (Left e) ._ refl =
              contractBailAfterSync _ refl
            pf-step₂' (Right false) ._ refl ._ refl =
              contractBailAfterSync _ refl
            pf-step₂' (Right true) ._ refl =
              processProposalMSpec.contract (proposal , vproposal)
                                            st
                                            (RWS-Post++ Contract outs)
                                            pf-step₃
              where

              pf-step₃ : RWS-Post-⇒
                           (processProposalMSpec.Contract (proposal , vproposal) _)
                           (RWS-Post++ Contract outs)
              pf-step₃ unit st' outs' con =
                mkContract
                  (transPreservesRoundManagerInv ERASU.rmInv (PP.rmInv con))
                  (transNoEpochChange{i = pre}{j = st}{k = st'} ERASU.noEpochChange (PP.noEpochChange con))
                  vac outqcs qcPost
                where
                module PP = processProposalMSpec.Contract
                vac : NoHC1 → Voting.VoteAttemptCorrect pre st' (outs ++ outs') proposal
                vac nohc rewrite sym ERASU.dnmBtIdToBlk =
                  Voting.glue-VoteNotGenerated-VoteAttemptCorrect{outs₁ = outs}
                    ERASU.noVote ERASU.noVoteOuts (PP.voteAttemptCorrect con nohc)

                outqcs : QCProps.OutputQc∈RoundManager (outs ++ outs') st'
                outqcs =
                  QCProps.++-OutputQc∈RoundManager {rm = st'}
                    (QCProps.¬OutputQc⇒OutputQc∈RoundManager outs st' ERASU.noOutQcs)
                    (PP.outQcs∈RM con)

                qcPost : QCProps.∈Post⇒∈PreOr (_QC∈NM (P pm)) pre st'
                qcPost qc qc∈st'
                   with PP.qcPost con qc qc∈st'
                ...| Right refl = Right inP
                ...| Left qc∈st
                   with ERASU.qcPost qc qc∈st
                ... | Right qc∈si = Right (inSI inP qc∈si)
                ... | Left qc∈pre = Left qc∈pre

    contract : ∀ Post → RWS-Post-⇒ Contract Post → LBFT-weakestPre (processProposalMsgM now pm) Post pre
    contract Post pf =
      LBFT-⇒ (processProposalMsgM now pm) pre contract' pf

module startSpec
  (now          : Instant)
  (lastVoteSent : Maybe Vote)
  where

  module _ (pre : RoundManager)
           (rmi : RoundManagerInv pre) -- preconditions needed to prove contract
    where

    open InitProofDefs

    open start now lastVoteSent

    Contract : LBFT-Post Unit
    Contract _ post outs = ∃[ e ] (find' logErrMB outs ≡ just e)
                         ⊎ find' logErrMB outs ≡ nothing × InitContractOk lastVoteSent post outs

    syncInfo = SyncInfo∙new (pre ^∙ (lBlockStore ∙ bsHighestQuorumCert))
                            (pre ^∙ (lBlockStore ∙ bsHighestCommitCert))
                            (pre ^∙ (lBlockStore ∙ bsHighestTimeoutCert))

    postulate
      contract-step₁ : LBFT-weakestPre (step₁-abs syncInfo) Contract pre

    contract' : LBFT-weakestPre (start-abs now lastVoteSent) Contract pre
              -- These are due to the various binds arising from syncInfoM, which is not abstract
              -- because it's more trouble than it's worth
    contract' rewrite start-abs-≡ =
      λ where ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl si refl → contract-step₁


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Coproducts {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

import Categories.Object.Initial as Initial
import Categories.Object.BinaryCoproducts as BinaryCoproducts

open Initial C
open BinaryCoproducts C

-- this should really be 'FiniteCoproducts', no?
record Coproducts : Set (o ⊔ ℓ ⊔ e) where
  field
    initial : Initial
    binary : BinaryCoproducts

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Categories.Category.Instance.FinCatShapes where

open import Data.Nat using (ℕ)
open import Data.Fin

open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality as ≡ using (refl; _≡_; module ≡-Reasoning)

open import Categories.Category
open import Categories.Category.Finite.Fin

open import Categories.Utils.EqReasoning

-- essentially a functor, but we don't need the congruence rule
record FinCatShape⇒ (X Y : FinCatShape) : Set where
  private
    module X = FinCatShape X
    module Y = FinCatShape Y

  field
    F₀ : Fin X.size → Fin Y.size
    F₁ : ∀ {x y} → x X.⇒ y → F₀ x Y.⇒ F₀ y

    identity : ∀ {x} → F₁ (X.id {x}) ≡ Y.id
    homomorphism : ∀ {x y z} {f : x X.⇒ y} {g : y X.⇒ z} →
                     F₁ (g X.∘ f) ≡ F₁ g Y.∘ F₁ f

record _≈_ {X Y} (f g : FinCatShape⇒ X Y) : Set where
  private
    module X = FinCatShape X
    module Y = FinCatShape Y
    module f = FinCatShape⇒ f
    module g = FinCatShape⇒ g

  field
    F₀≡ : ∀ x → f.F₀ x ≡ g.F₀ x
    F₁≡ : ∀ {x y} (w : x X.⇒ y) → ≡.subst₂ Y._⇒_ (F₀≡ x) (F₀≡ y) (f.F₁ w) ≡ g.F₁ w

private
  open ≡-Reasoning

  id : ∀ {A} → FinCatShape⇒ A A
  id {A} = record
    { F₀           = λ x → x
    ; F₁           = λ x → x
    ; identity     = refl
    ; homomorphism = refl
    }
    where open FinCatShape A

  comp : ∀ {A B C} → FinCatShape⇒ B C → FinCatShape⇒ A B → FinCatShape⇒ A C
  comp {A} {B} {C} f g = record
    { F₀           = λ a → f.F₀ (g.F₀ a)
    ; F₁           = λ w → f.F₁ (g.F₁ w)
    ; identity     = λ {a} → begin
      f.F₁ (g.F₁ A.id)                ≡⟨ ≡.cong f.F₁ g.identity  ⟩
      f.F₁ B.id                       ≡⟨ f.identity ⟩
      C.id                            ∎
    ; homomorphism = λ {a b c} {z w} → begin
      f.F₁ (g.F₁ (w A.∘ z))           ≡⟨ ≡.cong f.F₁ g.homomorphism ⟩
      f.F₁ (g.F₁ w B.∘ g.F₁ z)        ≡⟨ f.homomorphism ⟩
      f.F₁ (g.F₁ w) C.∘ f.F₁ (g.F₁ z) ∎
    }
    where module A = FinCatShape A
          module B = FinCatShape B
          module C = FinCatShape C
          module f = FinCatShape⇒ f
          module g = FinCatShape⇒ g

  assoc : ∀ {A B C D} {f : FinCatShape⇒ A B} {g : FinCatShape⇒ B C} {h : FinCatShape⇒ C D} →
            comp (comp h g) f ≈ comp h (comp g f)
  assoc {A} {B} {C} {D} {f} {g} {h} = record
    { F₀≡ = λ a → refl
    ; F₁≡ = λ w → refl
    }
    where module A = FinCatShape A
          module B = FinCatShape B
          module C = FinCatShape C
          module D = FinCatShape D
          module f = FinCatShape⇒ f
          module g = FinCatShape⇒ g
          module h = FinCatShape⇒ h

  identityˡ : ∀ {A B} {f : FinCatShape⇒ A B} → comp id f ≈ f
  identityˡ {A} {B} {f} = record
    { F₀≡ = λ x → refl
    ; F₁≡ = λ w → refl
    }
    where module A = FinCatShape A
          module B = FinCatShape B
          module f = FinCatShape⇒ f

  identityʳ : ∀ {A B} {f : FinCatShape⇒ A B} → comp f id ≈ f
  identityʳ {A} {B} {f} = record
    { F₀≡ = λ x → refl
    ; F₁≡ = λ w → refl
    }
    where module A = FinCatShape A
          module B = FinCatShape B
          module f = FinCatShape⇒ f

  equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  equiv {A} {B} = record
    { refl  = record
      { F₀≡ = λ x → refl
      ; F₁≡ = λ w → refl
      }
    ; sym   = λ {x y} eq →
      let module x = FinCatShape⇒ x
          module y = FinCatShape⇒ y
          open _≈_ eq
      in record
      { F₀≡ = λ z → ≡.sym (F₀≡ z)
      ; F₁≡ = λ {a b} w → begin
        ≡.subst₂ B._⇒_ (≡.sym (F₀≡ a)) (≡.sym (F₀≡ b)) (y.F₁ w)
          ≡˘⟨ ≡.cong (≡.subst₂ B._⇒_ (≡.sym (F₀≡ a)) (≡.sym (F₀≡ b))) (F₁≡ w) ⟩
        ≡.subst₂ B._⇒_ (≡.sym (F₀≡ a)) (≡.sym (F₀≡ b)) (≡.subst₂ B._⇒_ (F₀≡ a) (F₀≡ b) (x.F₁ w))
          ≡⟨ subst₂-sym-subst₂ B._⇒_ (F₀≡ a) (F₀≡ b) ⟩
        x.F₁ w
          ∎
      }
    ; trans = λ {x y z} eq eq′ →
      let module x   = FinCatShape⇒ x
          module y   = FinCatShape⇒ y
          module z   = FinCatShape⇒ z
          module eq  = _≈_ eq
          module eq′ = _≈_ eq′
      in record
      { F₀≡ = λ a → ≡.trans (eq.F₀≡ a) (eq′.F₀≡ a)
      ; F₁≡ = λ {a b} w → begin
        ≡.subst₂ B._⇒_ (≡.trans (eq.F₀≡ a) (eq′.F₀≡ a)) (≡.trans (eq.F₀≡ b) (eq′.F₀≡ b)) (x.F₁ w)
          ≡˘⟨ subst₂-subst₂ B._⇒_ (eq.F₀≡ a) (eq′.F₀≡ a) (eq.F₀≡ b) (eq′.F₀≡ b) ⟩
        ≡.subst₂ B._⇒_ (eq′.F₀≡ a) (eq′.F₀≡ b) (≡.subst₂ B._⇒_ (eq.F₀≡ a) (eq.F₀≡ b) (x.F₁ w))
          ≡⟨ ≡.cong (≡.subst₂ B._⇒_ (eq′.F₀≡ a) (eq′.F₀≡ b)) (eq.F₁≡ w) ⟩
        ≡.subst₂ B._⇒_ (eq′.F₀≡ a) (eq′.F₀≡ b) (y.F₁ w)
          ≡⟨ eq′.F₁≡ w ⟩
        z.F₁ w
          ∎
      }
    }
    where module A = FinCatShape A
          module B = FinCatShape B

  ∘-resp-≈ : ∀ {A B C} {f h : FinCatShape⇒ B C} {g i : FinCatShape⇒ A B} →
               f ≈ h → g ≈ i → comp f g ≈ comp h i
  ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} eq eq′ = record
    { F₀≡ = λ a → ≡.trans (≡.cong f.F₀ (eq′.F₀≡ a)) (eq.F₀≡ (i.F₀ a))
    ; F₁≡ = λ {x y} w → begin
      ≡.subst₂ C._⇒_
        (≡.trans (≡.cong f.F₀ (eq′.F₀≡ x)) (eq.F₀≡ (i.F₀ x)))
        (≡.trans (≡.cong f.F₀ (eq′.F₀≡ y)) (eq.F₀≡ (i.F₀ y)))
        (F₁ (comp f g) w)
        ≡˘⟨ subst₂-subst₂ C._⇒_ (≡.cong f.F₀ (eq′.F₀≡ x)) (eq.F₀≡ (i.F₀ x)) (≡.cong f.F₀ (eq′.F₀≡ y)) (eq.F₀≡ (i.F₀ y)) ⟩
      ≡.subst₂ C._⇒_ (eq.F₀≡ (i.F₀ x)) (eq.F₀≡ (i.F₀ y))
               (≡.subst₂ C._⇒_ (≡.cong f.F₀ (eq′.F₀≡ x)) (≡.cong f.F₀ (eq′.F₀≡ y))
                         (F₁ (comp f g) w))
        ≡⟨ ≡.cong (≡.subst₂ C._⇒_ (eq.F₀≡ (i.F₀ x)) (eq.F₀≡ (i.F₀ y))) (subst₂-app C._⇒_ (g.F₁ w) (λ _ _ → f.F₁) (eq′.F₀≡ x) (eq′.F₀≡ y)) ⟩
      ≡.subst₂ C._⇒_ (eq.F₀≡ (i.F₀ x)) (eq.F₀≡ (i.F₀ y))
               (f.F₁ (≡.subst₂ B._⇒_ (eq′.F₀≡ x) (eq′.F₀≡ y) (g.F₁ w)))
        ≡⟨ ≡.cong (λ j → ≡.subst₂ C._⇒_ (eq.F₀≡ (i.F₀ x)) (eq.F₀≡ (i.F₀ y)) (f.F₁ j)) (eq′.F₁≡ w) ⟩
      ≡.subst₂ C._⇒_ (eq.F₀≡ (i.F₀ x)) (eq.F₀≡ (i.F₀ y)) (f.F₁ (i.F₁ w))
        ≡⟨ eq.F₁≡ (i.F₁ w) ⟩
      h.F₁ (i.F₁ w)
        ∎
    }
    where module A   = FinCatShape A
          module B   = FinCatShape B
          module C   = FinCatShape C
          module f   = FinCatShape⇒ f
          module g   = FinCatShape⇒ g
          module h   = FinCatShape⇒ h
          module i   = FinCatShape⇒ i
          module eq  = _≈_ eq
          module eq′ = _≈_ eq′
          open FinCatShape⇒

FinCatShapes : Category _ _ _
FinCatShapes = categoryHelper record
  { Obj       = FinCatShape
  ; _⇒_       = FinCatShape⇒
  ; _≈_       = _≈_
  ; id        = id
  ; _∘_       = comp
  ; assoc     = λ {A B C D} {f g} {h} → assoc {f = f} {g} {h}
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv     = equiv
  ; ∘-resp-≈  = ∘-resp-≈
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text: (1 ∷ 4 ∷ []) ∷ (2 ∷ 5 ∷ []) ∷ (3 ∷ 6 ∷ []) ∷ []

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-# OPTIONS --without-K #-}
module sets.finite.core where

open import sum
open import function.isomorphism
open import sets.nat
open import sets.fin

IsOfSize : ∀ {i} → Set i → ℕ → Set i
IsOfSize A n = A ≅ Fin n

IsFinite : ∀ {i} → Set i → Set i
IsFinite A = Σ ℕ (IsOfSize A)

mk-is-finite : ∀ {i n}{A : Set i}
             → (A ≅ Fin n)
             → IsFinite A
mk-is-finite {n = n} enum = n , enum

fin-is-finite : ∀ {n} → IsFinite (Fin n)
fin-is-finite {n} = mk-is-finite refl≅

⊎-of-size : ∀ {i j n m}{A : Set i}{B : Set j}
          → IsOfSize A n
          → IsOfSize B m
          → IsOfSize (A ⊎ B) (n + m)
⊎-of-size isoA isoB = ⊎-ap-iso isoA isoB ·≅ fin-sum

⊎-finite : ∀ {i j}{A : Set i}{B : Set j}
         → IsFinite A → IsFinite B
         → IsFinite (A ⊎ B)
⊎-finite (_ , fA) (_ , fB) = mk-is-finite (⊎-of-size fA fB)

×-of-size : ∀ {i j n m}{A : Set i}{B : Set j}
          → IsOfSize A n
          → IsOfSize B m
          → IsOfSize (A × B) (n * m)
×-of-size isoA isoB = ×-ap-iso isoA isoB ·≅ fin-prod

×-finite : ∀ {i j}{A : Set i}{B : Set j}
         → IsFinite A → IsFinite B
         → IsFinite (A × B)
×-finite (_ , fA) (_ , fB) = mk-is-finite (×-of-size fA fB)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
open import FRP.JS.Bool using ( Bool )
open import FRP.JS.True using ( ⊤ ; tt )
open import FRP.JS.String using ( String )
open import FRP.JS.True using ( True )
open import FRP.JS.RSet
open import FRP.JS.Behaviour

module FRP.JS.QUnit where

infixr 4 _,_

data Test : Set where
  ε : Test
  _,_ : Test → Test → Test
  ok : String → (b : {t : ⊤} → Bool) → {b✓ : True b} → Test
  ok! : String → (b : {t : ⊤} → Bool) → Test
  ok◇ : String → (b : ⟦ Beh ⟨ Bool ⟩ ⟧) → Test

data TestSuite : Set where
  ε : TestSuite
  _,_ : TestSuite → TestSuite → TestSuite
  test : String → Test → TestSuite

data TestSuites : Set where
  ε : TestSuites
  _,_ : TestSuites → TestSuites → TestSuites
  suite : String → TestSuite → TestSuites

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
    module _ where

    module A where

      data D : Set₁ where
        !_ : Set → D

      infix 3 !_

    data C : Set₁ where
      #_ : A.D → C

    infix 2 #_

    module B where

      data D : Set₁ where
        !_ : C → D

      infix 1 !_

    open A
    open B

    ok₁ : B.D → B.D
    ok₁ (! # X) = ! # X

    ok₂ : C → C
    ok₂ (# ! X) = # ! X

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition

module Rings.Homomorphisms.Image {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_+A_ _*A_ : A → A → A} {_+B_ _*B_ : B → B → B} {R1 : Ring S _+A_ _*A_} {R2 : Ring T _+B_ _*B_} {f : A → B} (hom : RingHom R1 R2 f) where

open import Groups.Homomorphisms.Image (RingHom.groupHom hom)
open import Rings.Subrings.Definition

imageGroupSubring : Subring R2 imageGroupPred
Subring.isSubgroup imageGroupSubring = imageGroupSubgroup
Subring.containsOne imageGroupSubring = Ring.1R R1 , RingHom.preserves1 hom
Subring.closedUnderProduct imageGroupSubring {x} {y} (a , fa=x) (b , fb=y) = (a *A b) , transitive ringHom (Ring.*WellDefined R2 fa=x fb=y)
  where
    open Setoid T
    open Equivalence eq
    open RingHom hom


text:
open import Data.Nat
open import Data.Vec
open import Data.List

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

module DependentFold where

Nat = ℕ

dfold : ∀ {a : Set}
      → {k : Nat}
      → (p : Nat → Set)
      → ((l : Nat) → a → p l → p (1 + l))
      → p 0
      → Vec a k
      → p k
dfold {k = 0} p step base [] = base
dfold {k = suc n} p step base (x ∷ xs) = step n x (dfold p step base xs)

foldrₗ : {a b : Set} -> (a -> b -> b) -> b -> List a -> b
foldrₗ step base []       = base
foldrₗ step base (x ∷ xs) = step x (foldrₗ step base xs)

map_motive : Set -> Nat -> Set
map_motive a l = Vec a l

dmap : {a b : Set} → {n : ℕ} → (a → b) → Vec a n → Vec b n
dmap {a} {b} {n} f xs = dfold (map_motive b) (λ _ x xs → f x ∷ xs) [] xs

_ : dmap (λ x → x + 3) (1 ∷ 2 ∷ 3 ∷ []) ≡ (4 ∷ 5 ∷ 6 ∷ [])
_ = refl

dappend : {a : Set} → {m n : ℕ} → Vec a m → Vec a n → Vec a (m + n)
dappend {a} {m} {n} xs ys = dfold (λ l → Vec a (l + n)) (λ _ x xs → x ∷ xs) ys xs

_ : dappend (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []
_ = refl

ind : {a : Set} {p : List a → Set}
    → ((x : a) → {xs : List a} → p xs → p (x ∷ xs))
    → p []
    → (l : List a)
    → p l
ind step base [] = base
ind step base (x ∷ xs) = step x (ind step base xs)


text:
module Issue1251.NonTerminating where

open import Common.Prelude  -- an import is necessary to trigger internal error

-- a non-termination function using imported stuff
bla : Nat → Set
bla zero    = bla zero
bla (suc x) = bla x


text:
------------------------------------------------------------------------------
-- Well-founded relation on lists based on their structure
------------------------------------------------------------------------------

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

module FOTC.Data.List.WF-Relation.LT-Cons where

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- Well-founded relation on lists based on their structure.
LTC : D → D → Set
LTC xs ys = ∃[ x ] ys ≡ x ∷ xs

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --sized-types --type-in-type #-} -- Oh my Nathaniel Hawthorne

module n2o.Network.Internal where

open import proto.Base
open import proto.Map
open import proto.IO

{-# FOREIGN GHC import Network.N2O.Types #-}

postulate
  Header : Set

data Event (A : Set) : Set where
  Init      :     Event A
  Message   : A → Event A
  Terminate :     Event A

data Result (A : Set) : Set where
  Reply   : A → Result A
  Ok      :     Result A
  Unknown :     Result A
  Empty   :     Result A

record Request : Set where
  constructor Req
  field
    reqPath : ByteString Strict
    reqMeth : ByteString Strict
    reqVers : ByteString Strict
    reqHead : List Header

mutual
  data N2OT (S : Set) (M : Set → Set) (A : Set) : Set where
    runN2O : S → M A → N2OT S M A

  N2O : (F : Set → Set) (A : Set) → Set → Set
  N2O F A = N2OT (State F A) IO
  -- N2O F A = ReaderT (IORef (Context F A)) IO

  {-# NO_POSITIVITY_CHECK #-}
  record Context (F : Set → Set) (A : Set) : Set where
    constructor mkCx
    field
      cxHandler    : Event A → N2O F A (Result A) → Context F A   -- TODO : Strict Positivity
      cxRequest    : Request
      cxMiddleware : List (Context F A → Context F A)             -- TODO : Strict Positivity
      cxProtos     : List (Proto F A)                             -- TODO : Strict Positivity
      cxActions    : ByteString Strict
      cxDict       : Map (ByteString Strict) (ByteString Strict)

  State : (F : Set → Set) (A : Set) → Set
  State F A = IORef (Context F A) -- TODO : comp

  record Proto (F : Set → Set) (A : Set) : Set where
    inductive
    constructor proto
    field
      protoInfo : F A → N2O F A (Result (F A))

{-# COMPILE GHC Context = data Network.N2O.Types.Context (mkCx)                                      #-}
{-# COMPILE GHC  Header = type Network.N2O.Types.Header                                              #-}
{-# COMPILE GHC    N2OT = data Network.N2O.Types.N2OT    ( runN2O                                  ) #-}
{-# COMPILE GHC   Proto = data Network.N2O.Types.Proto   ( protoInfo                               ) #-}
{-# COMPILE GHC   Event = data Network.N2O.Types.Event   ( Init      | Message | Terminate         ) #-}
{-# COMPILE GHC Request = data Network.N2O.Types.Request ( Req                                     ) #-}
{-# COMPILE GHC  Result = data Network.N2O.Types.Result  ( Reply     | Ok      | Unknown   | Empty ) #-}


text:
module Issue1839.A where

postulate
  PrintThis : Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

-- open import Common.Prelude

module Id (A : Set) where

  id : A → A
  id x = x

module _ (A : Set) where
  open Id A

  id2 = id


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Nat where

open import Algebra.Group
open import Classes
open import Core
open import Data.Nat.Core
open import Data.Nat.Core public
  using (ℕ; ℕ-Number; ℕ-Plus; ℕ-Times;
         ℕ,≤; module ℕ,≤;
         suc; zero)

ℕ,+ : Monoid
ℕ,+ =
  record {
    semigroup = record {
      A = ℕ;
      Eq = PropEq ℕ;
      semigroupOver = record {
        _⋄_ = _+_;
        ⋄-cong = cong2 _+_;
        assoc = Props.+-assoc
      }
    };
    isMonoid = record {
      id = 0;
      left-id = Props.+-left-id;
      right-id = Props.+-right-id
    }
  }

module ℕ,+ = Monoid ℕ,+

ℕ,* : Monoid
ℕ,* =
  record {
    semigroup = record {
      A = ℕ;
      Eq = PropEq ℕ;
      semigroupOver = record {
        _⋄_ = _*_;
        ⋄-cong = cong2 _*_;
        assoc = Props.*-assoc
      }
    };
    isMonoid = record {
      id = 1;
      left-id = Props.*-left-id;
      right-id = Props.*-right-id
    }
  }

module ℕ,* = Monoid ℕ,*

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module RecordConstructorOutOfScope where

record R : Set where
  constructor con

  id : R
  id = con


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.RingStructure.CohomologyRing where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.Instances.NatPlusBis
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.DirectSumHIT

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.AbGroup.Instances.DirectSumHIT

open import Cubical.HITs.SetTruncation as ST

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

private variable
  ℓ ℓ' : Level

open Iso

-----------------------------------------------------------------------------
-- Definition Cohomology Ring

open PlusBis
open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆

module _ (A : Type ℓ) where

  H*R : Ring ℓ
  H*R = ⊕HITgradedRing-Ring
        NatPlusBis-Monoid
        (λ k → coHom k A)
        (λ k → snd (coHomGroup k A))
        1⌣
        _⌣_
        (λ {k} {l} → 0ₕ-⌣ k l)
        (λ {k} {l} → ⌣-0ₕ k l)
        (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ ((sym (+'-assoc _ _ _)) , (sym (assoc-⌣ _ _ _ _ _ _)))))
        (λ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _) , sym (lUnit⌣ _ _))))
        (λ _ → ΣPathTransport→PathΣ _ _ (refl , transportRefl _ ∙ rUnit⌣ _ _))
        (λ _ _ _ → leftDistr-⌣ _ _ _ _ _)
        λ _ _ _ → rightDistr-⌣ _ _ _ _ _

  H* : Type ℓ
  H* = fst H*R

module gradedRingProperties (A : Type ℓ) where
  open RingStr (snd (H*R A)) renaming (_·_ to _cup_)

-----------------------------------------------------------------------------
-- Graded Comutative Ring

  -- def + commutation with base
  -^-gen : (n m : ℕ) → (p : isEvenT n ⊎ isOddT n) → (q : isEvenT m ⊎ isOddT m)
          → H* A → H* A
  -^-gen n m (inl p)      q  x = x
  -^-gen n m (inr p) (inl q) x = x
  -^-gen n m (inr p) (inr q) x = - x

  -^_·_ : (n m : ℕ) → H* A → H* A
  -^_·_ n m x = -^-gen n m (evenOrOdd n) (evenOrOdd m) x

  -^-gen-base : {k : ℕ} → (n m : ℕ) → (p : isEvenT n ⊎ isOddT n) → (q : isEvenT m ⊎ isOddT m)
              (a : coHom k A) → -^-gen n m p q (base k a) ≡ base k (-ₕ^-gen n m p q a)
  -^-gen-base n m (inl p) q a = refl
  -^-gen-base n m (inr p) (inl q) a = refl
  -^-gen-base n m (inr p) (inr q) a = refl

  -^-base : {k : ℕ} → (n m : ℕ) → (a : coHom k A) → (-^ n · m) (base k a) ≡ base k ((-ₕ^ n · m) a)
  -^-base n m a = -^-gen-base n m (evenOrOdd n) (evenOrOdd m) a

  gradCommRing : (n m : ℕ) → (a : coHom n A) → (b : coHom m A) →
                 (base n a) cup (base m b) ≡ (-^ n · m) ((base m b) cup (base n a))
  gradCommRing n m a b = base (n +' m) (a ⌣ b)
                                 ≡⟨ cong (base (n +' m)) (gradedComm-⌣ n m a b) ⟩
                        base (n +' m) ((-ₕ^ n · m) (subst (λ n₁ → coHom n₁ A) (+'-comm m n) (b ⌣ a)))
                                 ≡⟨ sym (-^-base n m (subst (λ k → coHom k A) (+'-comm m n) (b ⌣ a))) ⟩
                        (-^ n · m)  (base (n +' m) (subst (λ k → coHom k A) (+'-comm m n) (b ⌣ a)))
                                 ≡⟨ cong (-^ n · m) (sym (constSubstCommSlice (λ k → coHom k A) (H* A) base (+'-comm m n) (b ⌣ a))) ⟩
                         (-^ n · m) (base (m +' n) (b ⌣ a)) ∎

-----------------------------------------------------------------------------
-- Equivalence of Type implies equivalence of Cohomology Ring

module CohomologyRing-Equiv
  {X : Type ℓ}
  {Y : Type ℓ'}
  (e : Iso X Y)
  where

  open IsGroupHom

  open RingStr (snd (H*R X)) using ()
    renaming
    ( 0r        to 0H*X
    ; 1r        to 1H*X
    ; _+_       to _+H*X_
    ; -_        to -H*X_
    ; _·_       to _cupX_
    ; +Assoc    to +H*XAssoc
    ; +IdR      to +H*XIdR
    ; +Comm     to +H*XComm
    ; ·Assoc    to ·H*XAssoc
    ; is-set    to isSetH*X     )

  open RingStr (snd (H*R Y)) using ()
    renaming
    ( 0r        to 0H*Y
    ; 1r        to 1H*Y
    ; _+_       to _+H*Y_
    ; -_        to -H*Y_
    ; _·_       to _cupY_
    ; +Assoc    to +H*YAssoc
    ; +IdR      to +H*YIdR
    ; +Comm     to +H*YComm
    ; ·Assoc    to ·H*YAssoc
    ; is-set    to isSetH*Y     )

  coHomGr-Iso : {n : ℕ} → GroupIso (coHomGr n X) (coHomGr n Y)
  fst (coHomGr-Iso {n}) = is
    where
    is : Iso (coHom n X) (coHom n Y)
    fun is = ST.rec squash₂ (λ f → ∣ (λ y → f (inv e y)) ∣₂)
    inv is = ST.rec squash₂ (λ g → ∣ (λ x → g (fun e x)) ∣₂)
    rightInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ f → cong ∣_∣₂ (funExt (λ y → cong f (rightInv e y))))
    leftInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ g → cong ∣_∣₂ (funExt (λ x → cong g (leftInv e x))))
  snd (coHomGr-Iso {n}) = makeIsGroupHom
                                        (ST.elim (λ _ → isProp→isSet λ u v i y → squash₂ _ _ (u y) (v y) i)
                                        (λ f → ST.elim (λ _ → isProp→isSet (squash₂ _ _))
                                        (λ f' → refl)))

  H*-X→H*-Y : H* X → H* Y
  H*-X→H*-Y = DS-Rec-Set.f _ _ _ _ isSetH*Y
               0H*Y
               (λ n a → base n (fun (fst coHomGr-Iso) a))
               _+H*Y_
               +H*YAssoc
               +H*YIdR
               +H*YComm
               (λ n → cong (base n) (pres1 (snd coHomGr-Iso)) ∙ base-neutral n)
               λ n a b → base-add _ _ _ ∙ cong (base n) (sym (pres· (snd coHomGr-Iso) a b))

  H*-Y→H*-X : H* Y → H* X
  H*-Y→H*-X = DS-Rec-Set.f _ _ _ _ isSetH*X
               0H*X
               (λ m a → base m (inv (fst coHomGr-Iso) a))
               _+H*X_
               +H*XAssoc
               +H*XIdR
               +H*XComm
               (λ m → cong (base m) (pres1 (snd (invGroupIso coHomGr-Iso))) ∙ base-neutral m)
               λ m a b → base-add _ _ _ ∙ cong (base m) (sym (pres· (snd (invGroupIso coHomGr-Iso)) a b))

  e-sect : (y : H* Y) → H*-X→H*-Y (H*-Y→H*-X y) ≡ y
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _)
           refl
           (λ m a → cong (base m) (rightInv (fst coHomGr-Iso) a))
           (λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V)

  e-retr : (x : H* X) → H*-Y→H*-X (H*-X→H*-Y x) ≡ x
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X _ _)
           refl
           (λ n a → cong (base n) (leftInv (fst coHomGr-Iso) a))
           (λ {U V} ind-U ind-V → cong₂ _+H*X_ ind-U ind-V)

  H*-X→H*-Y-pres1 : H*-X→H*-Y 1H*X ≡ 1H*Y
  H*-X→H*-Y-pres1 = refl

  H*-X→H*-Y-pres+ : (x x' : H* X) → H*-X→H*-Y (x +H*X x') ≡ H*-X→H*-Y x +H*Y H*-X→H*-Y x'
  H*-X→H*-Y-pres+ x x' = refl

  H*-X→H*-Y-pres· : (x x' : H* X) → H*-X→H*-Y (x cupX x') ≡ H*-X→H*-Y x cupY H*-X→H*-Y x'
  H*-X→H*-Y-pres· = DS-Ind-Prop.f _ _ _ _ (λ x u v i y → isSetH*Y _ _ (u y) (v y) i)
         (λ _ → refl)
         (λ n → ST.elim (λ x → isProp→isSet λ u v i y → isSetH*Y _ _ (u y) (v y) i)
                (λ f → DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _)
                        refl
                        (λ m → ST.elim (λ _ → isProp→isSet (isSetH*Y _ _))
                                (λ g → refl))
                        λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V) )
         (λ {U V} ind-U ind-V y → cong₂ _+H*Y_ (ind-U y) (ind-V y))

module _
  {X : Type ℓ}
  {Y : Type ℓ'}
  (e : Iso X Y)
  where

  open CohomologyRing-Equiv e

  CohomologyRing-Equiv : RingEquiv (H*R X) (H*R Y)
  fst CohomologyRing-Equiv = isoToEquiv is
    where
    is : Iso (H* X) (H* Y)
    fun is = H*-X→H*-Y
    inv is = H*-Y→H*-X
    rightInv is = e-sect
    leftInv is = e-retr
  snd CohomologyRing-Equiv = makeIsRingHom H*-X→H*-Y-pres1 H*-X→H*-Y-pres+ H*-X→H*-Y-pres·

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Relation.Binary

module Data.FingerTree.Relation.Binary.Reasoning.FasterInference.Setoid {ℓ₁ ℓ₂} (setoid : Setoid ℓ₁ ℓ₂) where

open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open Setoid setoid

infix  4 _IsRelatedTo_
infix  3 _∎
infixr 2 step-≈ step-≈˘ step-≡ step-≡˘
infixr 2 _≡⟨⟩_
infix  1 begin_

data _IsRelatedTo_ (x y : Carrier) : Set ℓ₂ where
  relTo : (x≈y : x ≈ y) → x IsRelatedTo y

begin_ : ∀ {x y} → x IsRelatedTo y → x ≈ y
begin relTo x≈y = x≈y

step-≈ : ∀ x {y z} → y IsRelatedTo z → x ≈ y → x IsRelatedTo z
step-≈ _ (relTo y≈z) x≈y = relTo (trans x≈y y≈z)

syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z

step-≈˘ : ∀ x {y z} → y IsRelatedTo z → y ≈ x → x IsRelatedTo z
step-≈˘ _ (relTo y≈z) y≈x = relTo (trans (sym y≈x) y≈z)

syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z

step-≡ : ∀ x {y z} → y IsRelatedTo z → x ≡ y → x IsRelatedTo z
step-≡ _ x≈z ≡.refl = x≈z

syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

step-≡˘ : ∀ x {y z} → y IsRelatedTo z → y ≡ x → x IsRelatedTo z
step-≡˘ _ x≈z ≡.refl = x≈z

syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

_≡⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x≈y = _ ≡⟨ ≡.refl ⟩ x≈y

_∎ : ∀ x → x IsRelatedTo x
_∎ _ = relTo refl

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
module Generic.Test.Data.Vec where

open import Generic.Main

import Data.Vec as Vec

infixr 5 _∷ᵥ_

Vec : ∀ {α} -> Set α -> ℕ -> Set α
Vec = readData Vec.Vec

-- []ᵥ : ∀ {α} {A : Set α} -> Vec A 0
pattern []ᵥ = #₀ lrefl

-- _∷ᵥ_ : ∀ {n α} {A : Set α} -> A -> Vec A n -> Vec A (suc n)
pattern _∷ᵥ_ {n} x xs = !#₁ (relv n , relv x , xs , lrefl)

elimVec : ∀ {n α π} {A : Set α}
        -> (P : ∀ {n} -> Vec A n -> Set π)
        -> (∀ {n} {xs : Vec A n} x -> P xs -> P (x ∷ᵥ xs))
        -> P []ᵥ
        -> (xs : Vec A n)
        -> P xs
elimVec P f z  []ᵥ      = z
elimVec P f z (x ∷ᵥ xs) = f x (elimVec P f z xs)

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
-- Andreas, issue reported by Matteo Acerbi, 2014-09-04.
-- Short summary: x = c x is not impossible for coinductive constructors c,
-- so x should not be considered a strictly rigid occurrence in (c x).

-- Matteo:

-- In the following I cannot understand what justifies the absurd pattern
-- in the definition of ¬id≡In: as νId is coinductive, elaboration of the
-- no-cycles check to eliminators should not be possible (as far as I know).

-- Any two inhabitants of νId are bisimilar, but it seems that current
-- pattern matching makes it inconsistent to assume that bisimilarity
-- implies equality for νId, which *might* upset some. :-)

{-# OPTIONS --copatterns #-}

-- False and equality.

⊥ = (X : Set) → X

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

-- The cofixpoint of the identity functor.

record νId : Set where
  coinductive
  constructor In
  field       Out : νId
open νId

-- The "only" inhabitant of νId.

tt : νId
Out tt = tt

-- x ≡ In x is considered absurd.

¬id≡In : {x : νId} → x ≡ In x → ⊥
¬id≡In ()

-- _≈_ is bisimilarity for elements of νId.

record _≈νId_ (x y : νId) : Set where
  coinductive
  field step : Out x ≈νId Out y
open _≈νId_

-- Any two elements are bisimilar.

trivial-≈νId : ∀ {x y} → x ≈νId y
step trivial-≈νId = trivial-≈νId

-- For νId it is not consistent to assume that bisimilarity implies
-- equality.

problem? : (ext : ∀ {x y} → x ≈νId y → x ≡ y) → ⊥
problem? ext = ¬id≡In {tt} (ext trivial-≈νId)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Common.Prelude
open import Common.Level
open import Common.Reflection
open import Common.Equality

test₁ : quoteTerm lzero ≡ def (quote lzero) []
test₁ = refl

foo : (l : Level) → Bool → Bool
foo _ false = true
foo _ true = false

test₂ : quoteTerm (foo lzero) ≡ def (quote foo) (arg (argInfo visible relevant) (def (quote lzero) []) ∷ [])
test₂ = refl

test₃ : unquote (give (quoteTerm lzero)) ≡ lzero
test₃ = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning uniqueness of identity proofs
------------------------------------------------------------------------

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

module Axiom.UniquenessOfIdentityProofs where

open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core

------------------------------------------------------------------------
-- Definition
--
-- Uniqueness of Identity Proofs (UIP) states that all proofs of
-- equality are themselves equal. In other words, the equality relation
-- is irrelevant. Here we define UIP relative to a given type.

UIP : ∀ {a} (A : Set a) → Set a
UIP A = Irrelevant {A = A} _≡_

------------------------------------------------------------------------
-- Properties

-- UIP always holds when using axiom K
-- (see `Axiom.UniquenessOfIdentityProofs.WithK`).

-- The existence of a constant function over proofs of equality for
-- elements in A is enough to prove UIP for A. Indeed, we can relate any
-- proof to its image via this function which we then know is equal to
-- the image of any other proof.

module Constant⇒UIP
  {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_)
  (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q)
  where

  ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p
  ≡-canonical refl = trans-symˡ (f refl)

  ≡-irrelevant : UIP A
  ≡-irrelevant p q = begin
    p                          ≡⟨ sym (≡-canonical p) ⟩
    trans (sym (f refl)) (f p) ≡⟨ cong (trans _) (f-constant p q) ⟩
    trans (sym (f refl)) (f q) ≡⟨ ≡-canonical q ⟩
    q                          ∎ where open ≡-Reasoning

-- If equality is decidable for a given type, then we can prove UIP for
-- that type. Indeed, the decision procedure allows us to define a
-- function over proofs of equality which is constant: it returns the
-- proof produced by the decision procedure.

module Decidable⇒UIP
  {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A}))
  where

  ≡-normalise : _≡_ {A = A} ⇒ _≡_
  ≡-normalise {a} {b} a≡b with a ≟ b
  ... | yes p = p
  ... | no ¬p = ⊥-elim (¬p a≡b)

  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
  ≡-normalise-constant {a} {b} p q with a ≟ b
  ... | yes _ = refl
  ... | no ¬p = ⊥-elim (¬p p)

  ≡-irrelevant : UIP A
  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant


text:
------------------------------------------------------------------------------
-- Commutativity of addition of total natural numbers
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.AddComm where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Nat

------------------------------------------------------------------------------
-- Auxiliary properties

succCong : ∀ {m n} → m ≡ n → succ₁ m ≡ succ₁ n
succCong refl = refl

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity n = +-0x n

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity Nn = N-ind A A0 is Nn
  where
  A : D → Set
  A i = i + zero ≡ i

  A0 : A zero
  A0 = +-leftIdentity zero

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = trans (+-Sx i zero) (succCong Ai)

x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y] Nm n = N-ind A A0 is Nm
  where
  A : D → Set
  A i = i + succ₁ n ≡ succ₁ (i + n)

  A0 : A zero
  A0 = zero + succ₁ n   ≡⟨ +-leftIdentity (succ₁ n) ⟩
       succ₁ n          ≡⟨ succCong (sym (+-leftIdentity n)) ⟩
       succ₁ (zero + n) ∎

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = succ₁ i + succ₁ n     ≡⟨ +-Sx i (succ₁ n) ⟩
              succ₁ (i + succ₁ n)   ≡⟨ succCong Ai ⟩
              succ₁ (succ₁ (i + n)) ≡⟨ succCong (sym (+-Sx i n)) ⟩
              succ₁ (succ₁ i + n)   ∎

+-comm-ind-instance :
  ∀ n →
  zero + n ≡ n + zero →
  (∀ {m} → m + n ≡ n + m → succ₁ m + n ≡ n + succ₁ m) →
  ∀ {m} → N m → m + n ≡ n + m
+-comm-ind-instance n = N-ind (λ i → i + n ≡ n + i)

------------------------------------------------------------------------------
-- Approach 1: Interactive proof using pattern matching

module M1 where

  +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
  +-comm {n = n} nzero Nn =
    zero + n ≡⟨ +-leftIdentity n ⟩
    n        ≡⟨ sym (+-rightIdentity Nn) ⟩
    n + zero ∎

  +-comm {n = n} (nsucc {m} Nm) Nn =
    succ₁ m + n   ≡⟨ +-Sx m n ⟩
    succ₁ (m + n) ≡⟨ succCong (+-comm Nm Nn) ⟩
    succ₁ (n + m) ≡⟨ sym (x+Sy≡S[x+y] Nn m) ⟩
    n + succ₁ m   ∎

------------------------------------------------------------------------------
-- Approach 2: Combined proof using pattern matching

module M2 where

  +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
  +-comm {n = n} nzero Nn = prf
    where postulate prf : zero + n ≡ n + zero
          {-# ATP prove prf +-rightIdentity #-}
  +-comm {n = n} (nsucc {m} Nm) Nn = prf (+-comm Nm Nn)
    where postulate prf : m + n ≡ n + m → succ₁ m + n ≡ n + succ₁ m
          {-# ATP prove prf x+Sy≡S[x+y] #-}

------------------------------------------------------------------------------
-- Approach 3: Interactive proof using the induction principle

module M3 where

  +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
  +-comm {n = n} Nm Nn = N-ind A A0 is Nm
    where
    A : D → Set
    A i = i + n ≡ n + i

    A0 : A zero
    A0 = zero + n ≡⟨ +-leftIdentity n ⟩
         n        ≡⟨ sym (+-rightIdentity Nn) ⟩
         n + zero ∎

    is : ∀ {i} → A i → A (succ₁ i)
    is {i} Ai = succ₁ i + n   ≡⟨ +-Sx i n ⟩
                succ₁ (i + n) ≡⟨ succCong Ai ⟩
                succ₁ (n + i) ≡⟨ sym (x+Sy≡S[x+y] Nn i) ⟩
                n + succ₁ i   ∎

------------------------------------------------------------------------------
-- Approach 4: Combined proof using the induction principle

module M4 where

  -- See Issue https://github.com/asr/apia/issues/81 .
  +-commA : D → D → Set
  +-commA n i = i + n ≡ n + i
  {-# ATP definition +-commA #-}

  +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
  +-comm {n = n} Nm Nn = N-ind (+-commA n) A0 is Nm
    where
    postulate A0 : +-commA n zero
    {-# ATP prove A0 +-rightIdentity #-}

    postulate is : ∀ {i} → +-commA n i → +-commA n (succ₁ i)
    {-# ATP prove is x+Sy≡S[x+y] #-}

------------------------------------------------------------------------------
-- Approach 5: Interactive proof using an instance of the induction
-- principle

module M5 where

  +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
  +-comm {n = n} Nm Nn = +-comm-ind-instance n A0 is Nm
    where
    A0 : zero + n ≡ n + zero
    A0 = zero + n ≡⟨ +-leftIdentity n ⟩
         n        ≡⟨ sym (+-rightIdentity Nn) ⟩
         n + zero ∎

    is : ∀ {i} → i + n ≡ n + i → succ₁ i + n ≡ n + succ₁ i
    is {i} ih = succ₁ i + n   ≡⟨ +-Sx i n ⟩
                succ₁ (i + n) ≡⟨ succCong ih ⟩
                succ₁ (n + i) ≡⟨ sym (x+Sy≡S[x+y] Nn i) ⟩
                n + succ₁ i   ∎

------------------------------------------------------------------------------
-- Approach 6: Combined proof using an instance of the induction
-- principle

module M6 where

  -- TODO (25 October 2012): Why is it not necessary the hypothesis
  -- +-rightIdentity?
  postulate +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
  {-# ATP prove +-comm +-comm-ind-instance x+Sy≡S[x+y] #-}


text:
module _ where

id : {A : Set} → A → A
id x = x
{-# INLINE id #-}

-- Adding COMPILE to an INLINE'd function has no effect, since the
-- treeless compiler will inline all uses of the function. Hence, we
-- warn the user that the pragma is pointless when compiling.
{-# COMPILE GHC id = \ _ x -> x #-}


text:
open import Data.Nat using ()
open import Data.Bool using (true; false)
open import Data.Product using (_×_; _,_)
open import Data.String using (String; _≟_)
open import Data.Empty using ()
open import Level using (suc; _⊔_)
open import Relation.Nullary           using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

open import IMP
open import OperationalSemantics

assn : ∀{l} → Set (suc l)
assn {a} = state → Set a

data ⊢[_]_[_] {l} : assn {l} → com → assn {l} → Set (suc l) where
  Skip : ∀{P}
     → ⊢[ P ] SKIP [ P ]
  Loc : ∀{Q a x}
     → ⊢[ (λ s → Q (s [ x ::= aval a s ])) ] (x ::= a) [ Q ]
  Comp : ∀{P Q R c₁ c₂}
     → ⊢[ P ] c₁ [ Q ]
     → ⊢[ Q ] c₂ [ R ]
     → ⊢[ P ] c₁ :: c₂ [ R ]
  If : ∀{P b c₁ Q c₂}
     → ⊢[ (λ s → P s × bval b s ≡ true)  ] c₁ [ Q ]
     → ⊢[ (λ s → P s × bval b s ≡ false) ] c₂ [ Q ]
     → ⊢[ P ] (IF b THEN c₁ ELSE c₂) [ Q ]
  While : ∀{P b c}
     → ⊢[ (λ s → P s × bval b s ≡ true) ] c [ P ]
     → ⊢[ P ] (WHILE b DO c) [ (λ s → P s × bval b s ≡ false) ]
  Conseq : ∀{P Q P′ Q′ : assn} {c}
     → (∀ s → P′ s → P s)
     → ⊢[ P  ] c [ Q  ]
     → (∀ s → Q s → Q′ s)
     → ⊢[ P′ ] c [ Q′ ]

⊨[_]_[_] : assn → com → assn → Set
⊨[ P ] c [ Q ] = ∀{s t} → P s → ⦅ c , s ⦆⇒ t → Q t

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
module Structure.Relator.Properties.Proofs where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic
-- open import Logic.Classical
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Structure.Relator.Properties
open import Structure.Relator
open import Structure.Setoid
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level
private variable T A B : Type{ℓ}
private variable _<_ _▫_ _▫₁_ _▫₂_ : T → T → Stmt{ℓ}
private variable f : T → T

[asymmetry]-to-irreflexivity : ⦃ _ : Asymmetry(_<_) ⦄ → Irreflexivity(_<_)
Irreflexivity.proof([asymmetry]-to-irreflexivity {_<_ = _<_}) = [→]-redundancy(asymmetry(_<_))

[irreflexivity,transitivity]-to-asymmetry : ⦃ irrefl : Irreflexivity(_<_) ⦄ ⦃ trans : Transitivity(_<_) ⦄ → Asymmetry(_<_)
Asymmetry.proof([irreflexivity,transitivity]-to-asymmetry {_<_ = _<_}) = Tuple.curry(irreflexivity(_<_) ∘ (Tuple.uncurry(transitivity(_<_))))

converseTotal-to-reflexivity : ⦃ convTotal : ConverseTotal(_<_) ⦄ → Reflexivity(_<_)
Reflexivity.proof(converseTotal-to-reflexivity {_<_ = _<_}) = [∨]-elim id id (converseTotal(_<_))

reflexivity-to-negated-irreflexivity : ⦃ refl : Reflexivity(_<_) ⦄ → Irreflexivity((¬_) ∘₂ (_<_))
Irreflexivity.proof (reflexivity-to-negated-irreflexivity {_<_ = _<_}) irrefl = irrefl(reflexivity(_<_))

negated-symmetry : ⦃ sym : Symmetry(_<_) ⦄ → Symmetry((¬_) ∘₂ (_<_))
Symmetry.proof (negated-symmetry {_<_ = _<_}) nxy yx = nxy(symmetry(_<_) yx)

antisymmetry-irreflexivity-to-asymmetry : ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ rel : BinaryRelator{A = T}(_<_) ⦄ ⦃ antisym : Antisymmetry(_<_)(_≡_) ⦄ ⦃ irrefl : Irreflexivity(_<_) ⦄ → Asymmetry(_<_)
Asymmetry.proof (antisymmetry-irreflexivity-to-asymmetry {_<_ = _<_}) xy yx = irreflexivity(_<_) (substitute₂ᵣ(_<_) (antisymmetry(_<_)(_≡_) xy yx) yx)

asymmetry-to-antisymmetry : ⦃ asym : Asymmetry(_<_) ⦄ → Antisymmetry(_<_)(_▫_)
Antisymmetry.proof (asymmetry-to-antisymmetry {_<_ = _<_}) ab ba = [⊥]-elim(asymmetry(_<_) ab ba)

subrelation-transitivity-to-subtransitivityₗ : ⦃ sub : (_▫₁_) ⊆₂ (_▫₂_) ⦄ ⦃ trans : Transitivity(_▫₂_) ⦄ → Subtransitivityₗ(_▫₂_)(_▫₁_)
Subtransitivityₗ.proof (subrelation-transitivity-to-subtransitivityₗ {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_}) xy yz = transitivity(_▫₂_) (sub₂(_▫₁_)(_▫₂_) xy) yz

subrelation-transitivity-to-subtransitivityᵣ : ⦃ sub : (_▫₁_) ⊆₂ (_▫₂_) ⦄ ⦃ trans : Transitivity(_▫₂_) ⦄ → Subtransitivityᵣ(_▫₂_)(_▫₁_)
Subtransitivityᵣ.proof (subrelation-transitivity-to-subtransitivityᵣ {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_}) xy yz = transitivity(_▫₂_) xy (sub₂(_▫₁_)(_▫₂_) yz)

-- TODO: https://proofwiki.org/wiki/Definition%3aRelation_Compatible_with_Operation and substitution. Special case for (≡) and function application: ∀(x∊T)∀(y∊T). (x ≡ y) → (∀(f: T→T). f(x) ≡ f(y))

instance
  -- A subrelation of a reflexive relation is reflexive.
  -- ∀{_□_ _△_ : T → T → Type} → ((_□_) ⊆₂ (_△_)) → (Reflexivity(_□_) → Reflexivity(_△_))
  subrelation-reflexivity : (_⊆₂_) ⊆₂ ((_→ᶠ_) on₂ Reflexivity{ℓ₂ = ℓ}{T = T})
  _⊆₂_.proof subrelation-reflexivity (intro ab) (intro ra) = intro (ab ra)

instance
  -- The negation of a subrelation is a superrelation.
  -- ∀{_□_ _△_ : T → T → Type} → ((_□_) ⊆₂ (_△_)) → (((¬_) ∘₂ (_△_)) ⊆₂ ((¬_) ∘₂ (_□_)))
  swapped-negated-subrelation : (_⊆₂_ {A = A}{B = B}{ℓ₁ = ℓ}) ⊆₂ ((_⊇₂_) on₂ ((¬_) ∘₂_))
  _⊆₂_.proof (_⊆₂_.proof swapped-negated-subrelation (intro sub)) = _∘ sub

swap-reflexivity : ⦃ refl : Reflexivity(_▫_) ⦄ → Reflexivity(swap(_▫_))
swap-reflexivity {_▫_ = _▫_} = intro(reflexivity(_▫_))

on₂-reflexivity : ∀{_▫_ : B → B → Stmt{ℓ}}{f : A → B} → ⦃ refl : Reflexivity(_▫_) ⦄ → Reflexivity((_▫_) on₂ f)
on₂-reflexivity {_▫_ = _▫_} = intro(reflexivity(_▫_))

on₂-symmetry : ∀{_▫_ : B → B → Stmt{ℓ}}{f : A → B} → ⦃ sym : Symmetry(_▫_) ⦄ → Symmetry((_▫_) on₂ f)
on₂-symmetry {_▫_ = _▫_} = intro(symmetry(_▫_))

on₂-transitivity : ∀{_▫_ : B → B → Stmt{ℓ}}{f : A → B} → ⦃ trans : Transitivity(_▫_) ⦄ → Transitivity((_▫_) on₂ f)
on₂-transitivity {_▫_ = _▫_} = intro(transitivity(_▫_))

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:
{-# OPTIONS --without-K --safe #-}

module Reasoning where

open import PiFrac

------------------------------------------------------------------------------
-- Useful for examples

infixr 2  _⟷⟨_⟩_
infix  3  _□

_⟷⟨_⟩_ : (t₁ : 𝕌) {t₂ : 𝕌} {t₃ : 𝕌} →
          (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
_ ⟷⟨ α ⟩ β = α ⊚ β

_□ : (t : 𝕌) → {t : 𝕌} → (t ⟷ t)
_□ t = id⟷

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Inductive directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Permutation.Inductive where

open import Data.List.Relation.Binary.Permutation.Inductive public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where all elements satisfy a given property
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.All where

open import Category.Applicative
open import Category.Monad
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product as Prod using (_,_)
open import Function
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary hiding (_∈_)
open import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- All P xs means that all elements in xs satisfy P.

infixr 5 _∷_

data All {a p} {A : Set a} (P : Pred A p) : Pred (List A) (a ⊔ p) where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

------------------------------------------------------------------------
-- Operations on All

head : ∀ {a p} {A : Set a} {P : Pred A p} {x xs} →
       All P (x ∷ xs) → P x
head (px ∷ pxs) = px

tail : ∀ {a p} {A : Set a} {P : Pred A p} {x xs} →
       All P (x ∷ xs) → All P xs
tail (px ∷ pxs) = pxs

lookup : ∀ {a p} {A : Set a} {P : Pred A p} {xs : List A} →
         All P xs → (∀ {x} → x ∈ xs → P x)
lookup []         ()
lookup (px ∷ pxs) (here refl)  = px
lookup (px ∷ pxs) (there x∈xs) = lookup pxs x∈xs

tabulate : ∀ {a p} {A : Set a} {P : Pred A p} {xs} →
           (∀ {x} → x ∈ xs → P x) → All P xs
tabulate {xs = []}     hyp = []
tabulate {xs = x ∷ xs} hyp = hyp (here refl) ∷ tabulate (hyp ∘ there)

map : ∀ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} →
      P ⊆ Q → All P ⊆ All Q
map g []         = []
map g (px ∷ pxs) = g px ∷ map g pxs

------------------------------------------------------------------------
-- (weak) updateAt

module _ {a p}{A : Set a}{P : Pred A p} where
  infixl 6 _[_]%=_ _[_]≔_

  updateAt : ∀ {x xs} → x ∈ xs → (P x → P x) → All P xs → All P xs
  updateAt () f []
  updateAt (here refl) f (px ∷ pxs) = f px ∷ pxs
  updateAt (there i)   f (px ∷ pxs) =   px ∷ updateAt i f pxs

  _[_]%=_ : ∀ {x xs} → All P xs → x ∈ xs → (P x → P x) → All P xs
  pxs [ i ]%= f = updateAt i f pxs

  _[_]≔_ : ∀ {x xs} → All P xs → x ∈ xs → P x → All P xs
  pxs [ i ]≔ px = pxs [ i ]%= const px

------------------------------------------------------------------------
-- (un/)zip(With/)

module _ {a p q r} {A : Set a} {P : Pred A p} {Q : Pred A q} {R : Pred A r} where

  zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
  zipWith f ([] , [])             = []
  zipWith f (px ∷ pxs , qx ∷ qxs) = f (px , qx) ∷ zipWith f (pxs , qxs)

  unzipWith : R ⊆ P ∩ Q → All R ⊆ All P ∩ All Q
  unzipWith f []         = [] , []
  unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (f rx) (unzipWith f rxs)

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  zip : All P ∩ All Q ⊆ All (P ∩ Q)
  zip = zipWith id

  unzip : All (P ∩ Q) ⊆ All P ∩ All Q
  unzip = unzipWith id

------------------------------------------------------------------------
-- Traversable-like functions

module _ {a} p {A : Set a} {P : Pred A (a ⊔ p)} {F}
         (App : RawApplicative {a ⊔ p} F) where

  open RawApplicative App

  sequenceA : All (F ∘′ P) ⊆ F ∘′ All P
  sequenceA []       = pure []
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs

  mapA : ∀ {q} {Q : Pred A q} → (Q ⊆ F ∘′ P) → All Q ⊆ (F ∘′ All P)
  mapA f = sequenceA ∘′ map f

  forA : ∀ {q} {Q : Pred A q} {xs} → All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
  forA qxs f = mapA f qxs

module _ {a} p {A : Set a} {P : Pred A (a ⊔ p)} {M}
         (Mon : RawMonad {a ⊔ p} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : All (M ∘′ P) ⊆ M ∘′ All P
  sequenceM = sequenceA p App

  mapM : ∀ {q} {Q : Pred A q} → (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
  mapM = mapA p App

  forM : ∀ {q} {Q : Pred A q} {xs} → All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
  forM = forA p App

------------------------------------------------------------------------
-- Properties of predicates preserved by All

module _ {a p} {A : Set a} {P : Pred A p} where

  all : Decidable P → Decidable (All P)
  all p []       = yes []
  all p (x ∷ xs) with p x
  ... | yes px = Dec.map′ (px ∷_) tail (all p xs)
  ... | no ¬px = no (¬px ∘ head)

  universal : Universal P → Universal (All P)
  universal u []       = []
  universal u (x ∷ xs) = u x ∷ universal u xs

  irrelevant : Irrelevant P → Irrelevant (All P)
  irrelevant irr []           []           = P.refl
  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
    P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)

  satisfiable : Satisfiable (All P)
  satisfiable = [] , []


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Instances.Initial where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Unit
open import Cubical.Data.Sigma.Properties using (Σ≡Prop)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom)
open import Cubical.Algebra.Algebra.Properties
open import Cubical.Algebra.CommAlgebra
import Cubical.Algebra.Algebra.Properties

open AlgebraHoms

private
  variable
    ℓ : Level

module _ (R : CommRing ℓ) where

  module _ where
    open CommRingStr (snd R)

    initialCAlg : CommAlgebra R ℓ
    initialCAlg .fst = fst R
    initialCAlg .snd .CommAlgebraStr.0a = _
    initialCAlg .snd .CommAlgebraStr.1a = _
    initialCAlg .snd .CommAlgebraStr._+_ = _
    initialCAlg .snd .CommAlgebraStr._·_ = _
    initialCAlg .snd .CommAlgebraStr.-_ = _
    initialCAlg .snd .CommAlgebraStr._⋆_ r x = r · x
    initialCAlg .snd .CommAlgebraStr.isCommAlgebra =
      makeIsCommAlgebra (isSetRing (CommRing→Ring R))
                         +Assoc +Rid +Rinv +Comm
                         ·Assoc ·Lid
                         ·Ldist+ ·Comm
                          (λ x y z → sym (·Assoc x y z)) ·Ldist+ ·Rdist+ ·Lid
                           λ x y z → sym (·Assoc x y z)

  module _ (A : CommAlgebra R ℓ) where
    open CommAlgebraStr ⦃... ⦄
    private
      instance
        _ : CommAlgebraStr R (fst A)
        _ = snd A
        _ : CommAlgebraStr R (fst R)
        _ = snd initialCAlg

    _*_ : fst R → (fst A) → (fst A)
    r * a = CommAlgebraStr._⋆_ (snd A) r a

    initialMap : CommAlgebraHom initialCAlg A
    initialMap =
      makeCommAlgebraHom {M = initialCAlg} {N = A}
        (λ r → r * 1a)
        (⋆-lid _)
        (λ x y → ⋆-ldist x y 1a)
        (λ x y →  (x · y) * 1a ≡⟨ ⋆-assoc _ _ _ ⟩
                           x * (y * 1a)                   ≡[ i ]⟨ x * (·Lid (y * 1a) (~ i)) ⟩
                           x * (1a · (y * 1a))            ≡⟨ sym (⋆-lassoc _ _ _) ⟩
                           (x * 1a) · (y * 1a) ∎)
        (λ r x → (r · x) * 1a   ≡⟨ ⋆-assoc _ _ _ ⟩
                         (r * (x * 1a)) ∎)

    initialMapEq : (f : CommAlgebraHom initialCAlg A)
                   → f ≡ initialMap
    initialMapEq f =
      let open IsAlgebraHom (snd f)
      in Σ≡Prop
           (isPropIsCommAlgebraHom {M = initialCAlg} {N = A})
             λ i x →
               ((fst f) x                              ≡⟨ cong (fst f) (sym (·Rid _)) ⟩
               fst f (x · 1a)                          ≡⟨ pres⋆ x 1a ⟩
               CommAlgebraStr._⋆_ (snd A) x (fst f 1a) ≡⟨ cong
                                                           (λ u → (snd A CommAlgebraStr.⋆ x) u)
                                                           pres1 ⟩
               (CommAlgebraStr._⋆_ (snd A) x 1a) ∎) i

    initialMapProp : (f g : CommAlgebraHom initialCAlg A)
                     → f ≡ g
    initialMapProp f g = initialMapEq f ∙ sym (initialMapEq g)

    initialityIso : Iso (CommAlgebraHom initialCAlg A) (Unit* {ℓ = ℓ})
    initialityIso = iso (λ _ → tt*)
                        (λ _ → initialMap)
                        (λ {tt*x → refl})
                        λ f → sym (initialMapEq f)

    initialityPath : CommAlgebraHom initialCAlg A ≡ Unit*
    initialityPath = isoToPath initialityIso

    initialityContr : isContr (CommAlgebraHom initialCAlg A)
    initialityContr = initialMap , λ ϕ → sym (initialMapEq ϕ)

  {-
    Show that any R-Algebra with the same universal property
    as the initial R-Algebra, is isomorphic to the initial
    R-Algebra.
  -}
  module _ (A : CommAlgebra R ℓ) where
    equivByInitiality :
      (isInitial : (B : CommAlgebra R ℓ) → isContr (CommAlgebraHom A B))
      → CommAlgebraEquiv A (initialCAlg)
    equivByInitiality isInitial = isoToEquiv asIso , snd to
      where
        open CommAlgebraHoms
        to : CommAlgebraHom A initialCAlg
        to = fst (isInitial initialCAlg)

        from : CommAlgebraHom initialCAlg A
        from = initialMap A

        asIso : Iso (fst A) (fst initialCAlg)
        Iso.fun asIso = fst to
        Iso.inv asIso = fst from
        Iso.rightInv asIso =
          λ x i → cong
                    fst
                    (isContr→isProp (initialityContr initialCAlg) (to ∘a from) (idCAlgHom initialCAlg))
                    i x
        Iso.leftInv asIso =
          λ x i → cong
                    fst
                    (isContr→isProp (isInitial A) (from ∘a to) (idCAlgHom A))
                    i x

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
module _ where

module Batch4 where
  data D1 (open Star) (A : ★) : ★ where
    c : (x : A) → D1 A

  data D2 (open Star) : ★ where

  data D3 (open Star) : ★₁ where
    c : (A : ★) → D3

  data D4 : (open Star) → ★ where

  data D0 (A : Set) (let B = A → A) : B → Set where
    c : (f : B) → D0 A f

  module _ where

    data D5 (open Star) (A : ★) (open MEndo A) : ★

    data D5 A (open MEndo A) where
      c : (f : Endo) → D5 A

  data D6 (open Star) (A : ★) (open MEndo A) : Endo → ★ where
    c : (f : Endo) → D6 A f

module Batch5 where
  data D1 (open Star) (A : ★) : ★

  data D1 A where
    c : (x : A) → D1 A

  data D2 (open Star) : ★
  data D2 where

  data D3 (open Star) : ★₁
  data D3 where
    c : (A : ★) → D3

  data D4 : (open Star) → ★
  data D4 where

open import Common.Equality

module Batch6 where

  BinOp : (A : Set) → Set
  BinOp A = A → A → A

  record IsAssoc {A : Set} (_∘_ : BinOp A) : Set where
    field
      assoc : ∀ {a b c} →
        ((a ∘ b) ∘ c) ≡ (a ∘ (b ∘ c))

  record RawSemiGroup : Set₁ where
    field
      Carrier : Set
      _∘_     : Carrier → Carrier → Carrier

  record SemiGroupLaws1 (G : RawSemiGroup) : Set where
    open RawSemiGroup G
    field
      isAssoc : IsAssoc _∘_

  module _ where
   record SemiGroupBLA
      (G : RawSemiGroup)
      (open RawSemiGroup G)
      (ass : IsAssoc _∘_) : Set
    where

  record SemiGroupLaws (G : RawSemiGroup) (open RawSemiGroup G) : Set where
    field
      isAssoc : IsAssoc {A = Carrier} _∘_

  record SemiGroup : Set₁ where
    field
      rawSemiGroup  : RawSemiGroup
      semiGroupLaws : SemiGroupLaws rawSemiGroup


text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym4 where

open import Symmetric
open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin
open import Data.Fin.Permutation hiding (_∘ₚ_)

infixr  200 _∘ₚ_
_∘ₚ_ = Data.Fin.Permutation._∘ₚ_

sym4solvable : solvable (Symmetric 4)
solvable.dervied-length sym4solvable = 3
solvable.end sym4solvable x d = solved1 x d where

   open import Data.List using ( List ; [] ; _∷_ )
   open Solvable (Symmetric 4)

   -- Klien
   --
   --  1                     (1,2),(3,4)           (1,3),(2,4)           (1,4),(2,3)
   --  0 ∷ 1 ∷ 2 ∷ 3 ∷ [] ,  1 ∷ 0 ∷ 3 ∷ 2 ∷ [] ,  2 ∷ 3 ∷ 0 ∷ 1 ∷ [] ,  3 ∷ 2 ∷ 1 ∷ 0 ∷ [] ,

   a0 =  pid {4}
   a1 =  pswap (pswap (pid {0}))
   a2 =  pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 )
   a3 =  pins (n≤ 3)  ∘ₚ  pins (n≤ 2) ∘ₚ pswap (pid {2})

   k3 = plist  (a1  ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3)  ∷ plist (a2 ∘ₚ a1 ) ∷  []

   open import FLutil
   open import Data.List.Fresh hiding ([_])
   open import Relation.Nary using (⌊_⌋)

   p0id :  FL→perm ((# 0) :: (# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
   p0id = pleq _ _ refl

   open import Data.List.Fresh.Relation.Unary.Any
   open import FLComm

   stage3FList : CommFListN 4 3 ≡ cons (zero :: zero :: zero :: zero :: f0) [] (Level.lift tt)
   stage3FList = refl

   st3 = proj₁ (toList ( CommFListN 4 2 ))
   -- st4 = {!!}

   solved1 :  (x : Permutation 4 4) → deriving 3 x → x =p= pid
   solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where
      --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
      solved2 : Any (perm→FL x ≡_) ( CommFListN 4 3 )
      solved2 = CommStage→ 4 3 x dr

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
open import Logic
open import Type

module Structure.Sets.Quantifiers {ℓₑ ℓₛ ℓₗ}{E : Type{ℓₑ}}{S : Type{ℓₛ}} (_∈_ : E → S → Stmt{ℓₗ}) where

import      Lvl
open import Logic.Propositional
open import Logic.Predicate
open import Syntax.Function

private variable ℓ : Lvl.Level

-- Set restricted existential quantifier.
∃ₛ : S → (E → Stmt{ℓ}) → Stmt
∃ₛ(A) P = ∃(x ↦ (x ∈ A) ∧ P(x))

-- Set restricted universal quantifier.
∀ₛ : S → (E → Stmt{ℓ}) → Stmt
∀ₛ(A) P = ∀ₗ(x ↦ ((x ∈ A) → P(x)))