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.Records
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.Handle.Properties
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
open import LibraBFT.Impl.IO.OBM.Properties.InputOutputHandlers
open import LibraBFT.Impl.Properties.Common
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        ReachableSystemStateProps
open import LibraBFT.Impl.Properties.Util
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 import LibraBFT.ImplShared.Util.HashCollisions Handle.InitHandler.initAndHandlers

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

-- This module proves the two "VotesOnce" proof obligations for our handler.

module LibraBFT.Impl.Properties.VotesOnce (𝓔 : EpochConfig) where

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

newVote⇒lv≡
  : ∀ {pre : SystemState}{pid s' acts v m pk}
  → ReachableSystemState pre
  → StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , acts)
  → v ⊂Msg m
  → send m ∈ acts
  → (sig : WithVerSig pk v)
  → Meta-Honest-PK pk
  → ¬ (∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig))
  → ¬ MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
  → LastVoteIs s' v

newVote⇒lv≡ {pid = pid} preach (step-init rm×acts uni) v⊂m send∈acts sig hpk ¬bootstrap ¬mws∈pool
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  with initHandlerSpec.ContractOk.isInitPM init-contract send∈acts
...| (_ , refl , noSigs)
  with v⊂m
...| vote∈qc vs∈qc v≈rbld qc∈pm = ⊥-elim (noSigs vs∈qc qc∈pm)

newVote⇒lv≡{pre}{pid}{s'}{v = v}{m}{pk} preach sps@(step-msg{sndr , nm} m∈pool ini) (vote∈qc{vs}{qc} vs∈qc v≈rbld qc∈m) m∈acts sig hpk ¬bootstrap ¬msb4
   with cong _vSignature v≈rbld
...| refl = ⊥-elim ∘′ ¬msb4 $ qcVoteSigsSentB4-handle pid preach sps m∈acts qc∈m sig vs∈qc v≈rbld ¬bootstrap

newVote⇒lv≡{pre}{pid}{v = v} preach (step-msg{sndr , P pm} m∈pool ini) vote∈vm m∈acts sig hpk ¬bootstrap ¬msb4
  with handleProposalSpec.contract! 0 pm (msgPool pre) (peerStates pre pid)
...| handleProposalSpec.mkContract _ invalidProposal _ vac _ _
   -- TODO-2: DRY fail.  This pattern arises several times in this file, where we need to know that
   -- the proposal being processed is valid, and to use handleProposalSpec to derive a contradiction
   -- if is not.  Some are identical, some are not.
   with BlockId-correct? (pm ^∙ pmProposal)
...| no  ¬validProposal = ⊥-elim (sendVote∉actions {outs = handleOuts} {st = handlePre}
                                    (sym (proj₂ $ invalidProposal ¬validProposal)) m∈acts)
  where
  handlePre  = peerStates pre pid
  handleOuts = LBFT-outs (handle pid (P pm) 0) (peerStates pre pid)

...| yes refl
   with vac refl (nohc preach m∈pool pid ini (invariantsCorrect pid pre ini preach) refl refl)
...| Voting.mkVoteAttemptCorrectWithEpochReq (inj₁ (_ , voteUnsent)) sdEpoch≡? =
  ⊥-elim (¬voteUnsent voteUnsent)
  where
  handleOuts = LBFT-outs (handle pid (P pm) 0) (peerStates pre pid)

  ¬voteUnsent : ¬ Voting.VoteUnsentCorrect (peerStates pre pid) _ _ _ _
  ¬voteUnsent (Voting.mkVoteUnsentCorrect noVoteMsgOuts _) =
    sendVote∉actions{outs = handleOuts}{st = peerStates pre pid}
      (sym noVoteMsgOuts) m∈acts
...| Voting.mkVoteAttemptCorrectWithEpochReq (inj₂ (Voting.mkVoteSentCorrect (VoteMsg∙new v' _) rcvr voteMsgOuts vgCorrect)) sdEpoch≡? =
  sentVoteIsPostLV
  where
  handlePost = LBFT-post (handle pid (P pm) 0) (peerStates pre pid)
  handleOuts = LBFT-outs (handle pid (P pm) 0) (peerStates pre pid)

  sentVoteIsPostLV : LastVoteIs handlePost v
  sentVoteIsPostLV
    with Voting.VoteGeneratedCorrect.state vgCorrect
  ...| RoundManagerTransProps.mkVoteGenerated lv≡v _
    rewrite sym lv≡v
    = cong (just ∘ _^∙ vmVote) (sendVote∈actions{outs = handleOuts}{st = peerStates pre pid} (sym voteMsgOuts) m∈acts)

newVote⇒lv≡{pre}{pid}{s' = s'}{v = v} preach (step-msg{sndr , V vm} m∈pool ini) vote∈vm m∈outs sig hpk ¬bootstrap ¬msb4 =
  ⊥-elim (sendVote∉actions{outs = hvOut}{st = hvPre} (sym noVotes) m∈outs)
  where
  hvPre = peerStates pre pid
  hvOut = LBFT-outs (handleVote 0 vm) hvPre
  open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)

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

oldVoteRound≤lvr
  : ∀ {pid pk v}{pre : SystemState}
  → (r : ReachableSystemState pre)
  → Meta-Honest-PK pk
  → (sig : WithVerSig pk v)
  → ¬ (∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig))
  → MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
  → PeerCanSignForPK pre v pid pk
  → (peerStates pre pid) ^∙ rmEpoch ≡ (v ^∙ vEpoch)
  → v ^∙ vRound ≤ Meta.getLastVoteRound ((peerStates pre pid) ^∙ pssSafetyData-rm)

oldVoteRound≤lvr{pid} (step-s preach step@(step-peer{pid'} sp@(step-cheat  cmc))) hpk sig ¬bootstrap mws∈pool pcsfpk epoch≡
  -- `pid`'s state is untouched by this step
  rewrite cheatStepDNMPeerStates₁{pid = pid'}{pid' = pid} sp unit
  = oldVoteRound≤lvr preach hpk sig ¬bootstrap mws∈prePool pcsfpkPre epoch≡
  where
  -- The cheat step could not have been where the signed message was introduced,
  -- so there must be a signed message in the pool prior to this
  mws∈prePool = ¬cheatForgeNew sp refl unit hpk mws∈pool (¬subst ¬bootstrap (msgSameSig mws∈pool))
  -- `pid` can sign for the message in the previous system state
  pcsfpkPre   = PeerCanSignForPKProps.msb4 preach step pcsfpk hpk sig mws∈prePool

oldVoteRound≤lvr{pid}{v = v} step*@(step-s{pre = pre}{post = post@._} preach step@(step-peer{pid'} sp@(step-honest{st = ppost}{outs} sps))) hpk sig ¬bootstrap mws∈pool pcsfpk epoch≡
   with msgSameSig mws∈pool
...| refl
   with newMsg⊎msgSentB4 preach sps hpk (msgSigned mws∈pool) ¬bootstrap (msg⊆ mws∈pool) (msg∈pool mws∈pool)
...| Right msb4 = helpSentB4
   where
   pcsfpkPre : PeerCanSignForPK pre v pid _
   pcsfpkPre = PeerCanSignForPKProps.msb4 preach step pcsfpk hpk sig msb4

   ovrHyp : peerStates pre pid ^∙ rmEpoch ≡ v ^∙ vEpoch → v ^∙ vRound ≤ Meta.getLastVoteRound ((peerStates pre pid) ^∙ pssSafetyData-rm)
   ovrHyp ep≡ = oldVoteRound≤lvr{pre = pre} preach hpk sig ¬bootstrap msb4 pcsfpkPre ep≡

   helpSentB4 : v ^∙ vRound ≤ Meta.getLastVoteRound ((peerStates post pid) ^∙ pssSafetyData-rm)
   helpSentB4
      with pid ≟ pid'
   -- A step by `pid'` step cannot affect `pid`'s state
   ...| no  pid≢
      rewrite sym (pids≢StepDNMPeerStates{pre = pre} sps pid≢)
      = ovrHyp epoch≡
   ...| yes refl = ≤-trans (ovrHyp epochPre≡) lvr≤
     where
     -- If a vote signed by a peer exists in the past, and that vote has an
     -- epoch id associated to it that is the same as the peer's post-state
     -- epoch, then the peer has that same epoch id in its immediately preceding
     -- pre-state.
     epochPre≡ : peerStates pre pid ^∙ rmEpoch ≡ v ^∙ vEpoch
     epochPre≡ =
       ReachableSystemStateProps.mws∈pool⇒epoch≡{v = v}{ppost}{outs} preach sps
         pcsfpkPre hpk sig ¬bootstrap msb4 epoch≡'
       where
       open ≡-Reasoning
       epoch≡' : ppost ^∙ rmEpoch ≡ v ^∙ vEpoch
       epoch≡' = begin
         ppost                                         ^∙ rmEpoch ≡⟨ cong (_^∙ rmEpoch) (StepPeer-post-lemma sp) ⟩
         peerStates (StepPeer-post{pre = pre} sp) pid' ^∙ rmEpoch ≡⟨ epoch≡ ⟩
         v ^∙ vEpoch                                              ∎

     ini : initialised pre pid' ≡ initd
     ini = ReachableSystemStateProps.mws∈pool⇒initd preach pcsfpkPre hpk sig ¬bootstrap msb4

     lvr≤ : Meta.getLastVoteRound ((peerStates pre pid) ^∙ pssSafetyData-rm) ≤ Meta.getLastVoteRound ((peerStates post pid) ^∙ pssSafetyData-rm)
     lvr≤
       rewrite sym (StepPeer-post-lemma{pre = pre} sp)
       = lastVotedRound-mono pid' pre preach ini sps
           (trans epochPre≡ (sym epoch≡))
-- The vote was newly sent this round
...| Left (m∈outs , pcsfpkPost , ¬msb4)
-- ... and it really is the same vote, because there has not been a hash collision
   with sameSig⇒sameVoteData (msgSigned mws∈pool) sig (msgSameSig mws∈pool)
...| Left nonInjSHA256 = ⊥-elim (PerReachableState.meta-no-collision step* nonInjSHA256)
...| Right refl
   with PeerCanSignForPKProps.pidInjective pcsfpk pcsfpkPost refl
...| refl = ≡⇒≤ vr≡lvrPost
  where
    vr≡lvrPost : v ^∙ vRound ≡ Meta.getLastVoteRound ((peerStates (StepPeer-post sp) pid) ^∙ pssSafetyData-rm)
    vr≡lvrPost
      rewrite sym (StepPeer-post-lemma sp)
      with newVote⇒lv≡{pre = pre}{pid = pid} preach sps (msg⊆ mws∈pool) m∈outs (msgSigned mws∈pool) hpk ¬bootstrap ¬msb4
    ...| lastVoteIsJust
       with ppost ^∙ pssSafetyData-rm ∙ sdLastVote
    ...| nothing = absurd (just _ ≡ nothing) case lastVoteIsJust of λ ()
    ...| just _ rewrite just-injective (sym lastVoteIsJust) = refl

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

sameERasLV⇒sameId-lem₁ :
  ∀ {pid pid' pk s acts}{pre : SystemState}
  → ReachableSystemState pre
  → (sp : StepPeer pre pid' s acts)
  → ∀ {v v'} → Meta-Honest-PK pk
  → PeerCanSignForPK (StepPeer-post sp) v pid pk
  → (sig' : WithVerSig pk v') → ¬ (∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig'))
  → (mws : MsgWithSig∈ pk (ver-signature sig') (msgPool pre))
  → v ≡L v' at vEpoch → v ≡L v' at vRound
  → Σ[ mws ∈ MsgWithSig∈ pk (ver-signature sig') (msgPool pre) ]
      (¬ ∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature ∘ msgSigned $ mws)
       × PeerCanSignForPK pre v pid pk
       × v  ≡L msgPart mws at vEpoch
       × v  ≡L msgPart mws at vRound
       × msgPart mws ≡L v' at vProposedId)

sameERasLV⇒sameId-lem₁{pid}{pid'}{pk}{pre = pre} rss sp {v}{v'} hpk pcsfpk sig' ¬bootstrap mws ≡epoch ≡round =
  mws , ¬bootstrap' , pcsfpkPre
  , trans ≡epoch (cong (_^∙ vdProposed ∙ biEpoch) (sym ≡voteData))
  , trans ≡round (cong (_^∙ vdProposed ∙ biRound) (sym ≡voteData))
  ,               cong (_^∙ vdProposed ∙ biId)    (    ≡voteData)
  where
  -- That message has the same signature as `v'`, so it has the same vote data
  -- (unless there was a collision, which we currently assume does not occur).
  ≡voteData : msgPart mws ≡L v' at vVoteData
  ≡voteData = ⊎-elimˡ (PerReachableState.meta-no-collision rss) (sameSig⇒sameVoteData sig' (msgSigned mws) (sym ∘ msgSameSig $ mws))

  ¬bootstrap' : ¬ ∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature ∘ msgSigned $ mws)
  ¬bootstrap' rewrite msgSameSig mws = ¬bootstrap

  -- The peer can sign for `v` now, so it can sign for `v` in the preceeding
  -- step, because there is an honestly signed message part for the peer's pubkey in the
  -- current epoch already in the pool.
  pcsfpkPre : PeerCanSignForPK pre v pid pk
  pcsfpkPre = PeerCanSignForPKProps.msb4-eid≡ rss (step-peer sp) hpk pcsfpk ≡epoch sig' mws

sameERasLV⇒sameId
  : ∀ {pid pid' pk}{st : SystemState}
    → ReachableSystemState st
    → ∀{v v' m'} → Meta-Honest-PK pk
    → just v ≡ peerStates st pid ^∙ pssSafetyData-rm ∙ sdLastVote
    → PeerCanSignForPK st v pid pk
    → v' ⊂Msg m' → (pid' , m') ∈ (msgPool st)
    → (sig' : WithVerSig pk v') → ¬ (∈BootstrapInfo-impl fakeBootstrapInfo (ver-signature sig'))
    → v ≡L v' at vEpoch → v ≡L v' at vRound
    → v ≡L v' at vProposedId
-- Cheat steps cannot be where an honestly signed message originated.
sameERasLV⇒sameId{pid}{pid'}{pk} (step-s{pre = pre} rss (step-peer sp@(step-cheat cmc))) {v}{v'}{m'} hpk ≡pidLV pcsfpk v'⊂m' m'∈pool sig' ¬bootstrap ≡epoch ≡round
   with sameERasLV⇒sameId-lem₁ rss sp hpk pcsfpk sig' ¬bootstrap mws ≡epoch ≡round
   where
   -- Track down the honestly signed message which existed before.
   mws : MsgWithSig∈ pk (ver-signature sig') (msgPool pre)
   mws = ¬cheatForgeNew sp refl unit hpk (mkMsgWithSig∈ m' v' v'⊂m' pid' m'∈pool sig' refl) ¬bootstrap
...| mws , ¬bootstrap' , pcsfpkPre , ≡epoch' , ≡round' , v'id≡ =
   trans (sameERasLV⇒sameId rss hpk ≡pidLVPre pcsfpkPre (msg⊆ mws) (msg∈pool mws) (msgSigned mws) ¬bootstrap' ≡epoch' ≡round') v'id≡
   where
   -- The state of `pid` is unchanged
   ≡pidLVPre : just v ≡ peerStates pre pid ^∙ pssSafetyData-rm ∙ sdLastVote
   ≡pidLVPre = trans ≡pidLV (cong (_^∙ pssSafetyData-rm ∙ sdLastVote) (cheatStepDNMPeerStates₁ sp unit))

-- Initialization steps cannot be where an honestly signed message originated
sameERasLV⇒sameId {pid} {pid'} {pk}
                  (step-s rss step@(step-peer{pre = pre} sp@(step-honest{pid“} sps@(step-init {rm} rm×acts uni))))
                  {v} {v'} {m'} hpk ≡pidLV pcsfpk v'⊂m' m'∈pool sig' ¬bootstrap ≡epoch ≡round
   with pid ≟ pid“
   -- If this isn't `pid`, the step does not affect `pid`'s state
...| no  pid≢
   rewrite sym $ pids≢StepDNMPeerStates{pre = pre} sps pid≢
   = sameERasLV⇒sameId rss hpk ≡pidLV pcsfpkPre v'⊂m' (m'∈poolb4 v'⊂m') sig' ¬bootstrap ≡epoch ≡round
   where

   m'∈poolb4 : v' ⊂Msg m' → (pid' , m') ∈ (msgPool pre)
   m'∈poolb4 v'⊂m'
     with Any-++⁻ _ m'∈pool
   ...| inj₂ x = x
   ...| inj₁ x
      with initHandlerSpec.contract pid“ fakeBootstrapInfo rm×acts
   ...| init-contract
      with initHandlerSpec.ContractOk.isInitPM init-contract (proj₁ (senderMsgPair∈⇒send∈ _ x))
   ...| (pm , refl , noSigs)
      with v'⊂m'
   ...| vote∈qc vs∈qc v≈rbld qc∈nm
      = ⊥-elim (noSigs vs∈qc qc∈nm)

   mws : MsgWithSig∈ pk (ver-signature sig') (msgPool pre)
   mws = mkMsgWithSig∈ _ _ v'⊂m' _ (m'∈poolb4 v'⊂m') sig' refl

   pcsfpkPre : PeerCanSignForPK pre v pid pk
   pcsfpkPre = PeerCanSignForPKProps.msb4-eid≡ rss step hpk pcsfpk ≡epoch sig' mws
   -- If this is `pid`, the last vote cannot be a `just`!
...| yes refl
   rewrite sym (StepPeer-post-lemma sp)
   with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
   with initHandlerSpec.ContractOk.sdLVnothing init-contract
...| lv≡nothing
   = absurd just v ≡ nothing case trans ≡pidLV lv≡nothing of λ ()

sameERasLV⇒sameId{pid}{pid'}{pk} (step-s rss (step-peer{pre = pre} sp@(step-honest{pid“} sps@(step-msg{sndr , m} m∈pool ini)))) {v}{v'} hpk ≡pidLV pcsfpk v'⊂m' m'∈pool sig' ¬bootstrap ≡epoch ≡round
   with newMsg⊎msgSentB4 rss sps hpk sig' ¬bootstrap v'⊂m' m'∈pool
-- The message has been sent before
...| Right mws'
   with sameERasLV⇒sameId-lem₁ rss sp hpk pcsfpk sig' ¬bootstrap mws' ≡epoch ≡round
...| mws , ¬bootstrap' , pcsfpkPre , ≡epoch' , ≡round' , v'id≡
   with pid ≟ pid“
   -- If this isn't `pid`, the step does not affect `pid`'s state
...| no  pid≢
   rewrite sym $ pids≢StepDNMPeerStates{pre = pre} sps pid≢
   = trans (sameERasLV⇒sameId rss hpk ≡pidLV pcsfpkPre (msg⊆ mws) (msg∈pool mws) (msgSigned mws) ¬bootstrap' ≡epoch' ≡round') v'id≡
   -- This is `pid`, so we need to know what message it was processing
...| yes refl
   rewrite sym $ StepPeer-post-lemma{pre = pre} sp
   = trans (sameERasLV⇒sameId rss hpk (≡pidLVPre m m∈pool ≡pidLV) pcsfpkPre (msg⊆ mws) (msg∈pool mws) (msgSigned mws) ¬bootstrap' ≡epoch' ≡round') v'id≡
   where
   ≡pidLVPre : (m : NetworkMsg) → (sndr , m) ∈ msgPool pre  → just v ≡ LBFT-post (handle pid m 0) (peerStates pre pid) ^∙ pssSafetyData-rm ∙ sdLastVote → just v ≡ peerStates pre pid ^∙ pssSafetyData-rm ∙ sdLastVote
   -- Last vote doesn't change when processing a vote message
   ≡pidLVPre (V vm) m∈pool ≡pidLV = begin
      just v                                 ≡⟨ ≡pidLV ⟩
      hvPos ^∙ pssSafetyData-rm ∙ sdLastVote ≡⟨ cong (_^∙ sdLastVote) (sym noSDChange) ⟩
      hvPre ^∙ pssSafetyData-rm ∙ sdLastVote ∎
      where
      open ≡-Reasoning

      hvPre = peerStates pre pid
      hvPos = LBFT-post (handleVote 0 vm) hvPre
      hvOut = LBFT-outs (handleVote 0 vm) hvPre

      open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)

   -- Commit messages are only for reasoning about correctness
   ≡pidLVPre (C cm) m∈pool ≡pidLV = ≡pidLV

   ≡pidLVPre (P pm) m∈pool ≡pidLV = analyzeVoteAttempt
      where
      hpPre  = peerStates pre pid“
      hpPos  = LBFT-post (handleProposal 0 pm) hpPre

      open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm (msgPool pre) hpPre)
        renaming (rmInv to rmInvP)
      open Invariants.RoundManagerInv (invariantsCorrect pid“ pre ini rss)

      -- when the last vote is the same in pre and post states
      module OldVote (lv≡ : hpPre ≡L hpPos at pssSafetyData-rm ∙ sdLastVote) where
        open ≡-Reasoning
        ≡pidLVPre₁ : just v ≡ hpPre ^∙ pssSafetyData-rm ∙ sdLastVote
        ≡pidLVPre₁ = begin
          just v                                 ≡⟨ ≡pidLV ⟩
          hpPos ^∙ pssSafetyData-rm ∙ sdLastVote ≡⟨ sym lv≡ ⟩
          hpPre ^∙ pssSafetyData-rm ∙ sdLastVote ∎

      -- When a new vote is generated, its round is strictly greater than that of the previous vote we attempted to send.
      module NewVote
        (vote : Vote) (lv≡v : just vote ≡ hpPos ^∙ pssSafetyData-rm ∙ sdLastVote)
        (lvr< : hpPre [ _<_ ]L hpPos at pssSafetyData-rm ∙ sdLastVotedRound)
        (lvr≡ : vote ^∙ vRound ≡ hpPos ^∙ pssSafetyData-rm ∙ sdLastVotedRound)
        (sdEpoch≡ : hpPre ^∙ pssSafetyData-rm ∙ sdEpoch ≡ pm ^∙ pmProposal ∙ bEpoch)
        (blockTriggered : Voting.VoteMadeFromBlock vote (pm ^∙ pmProposal))
        where

        -- `vote` comes from the peer handler contract
        v≡vote : v ≡ vote
        v≡vote = just-injective $ begin
          just v                                 ≡⟨ ≡pidLV ⟩
          hpPos ^∙ pssSafetyData-rm ∙ sdLastVote ≡⟨ sym lv≡v ⟩
          just vote                              ∎
          where open ≡-Reasoning

        -- The round of `v'` must be less than the round of the vote stored in `sdLastVote`
        rv'≤lvrPre : v' ^∙ vRound ≤ Meta.getLastVoteRound (hpPre ^∙ pssSafetyData-rm)
        rv'≤lvrPre = oldVoteRound≤lvr rss hpk sig' ¬bootstrap mws pcsfpkPre'
                       (ReachableSystemStateProps.mws∈pool⇒epoch≡ rss (step-msg m∈pool ini)
                         pcsfpkPre' hpk sig' ¬bootstrap mws ≡epoch“)
          where
          pcsfpkPre' = peerCanSignEp≡ pcsfpkPre ≡epoch

          open ≡-Reasoning
          ≡epoch“ : hpPos ^∙ rmEpoch ≡ v' ^∙ vEpoch
          ≡epoch“ = begin
            hpPos ^∙ rmEpoch                    ≡⟨ sym noEpochChange ⟩
            hpPre ^∙ rmEpoch                    ≡⟨ rmEpochsMatch ⟩
            hpPre ^∙ pssSafetyData-rm ∙ sdEpoch ≡⟨ sdEpoch≡ ⟩
            pm    ^∙ pmProposal ∙ bEpoch        ≡⟨ sym $ Voting.VoteMadeFromBlock.epoch≡ blockTriggered ⟩
            vote  ^∙ vEpoch                     ≡⟨ cong (_^∙ vEpoch) (sym v≡vote) ⟩
            v     ^∙ vEpoch                     ≡⟨ ≡epoch ⟩
            v'    ^∙ vEpoch                     ∎

        rv'<rv : v' [ _<_ ]L v at vRound
        rv'<rv = begin
          (suc $ v' ^∙ vRound)                                      ≤⟨ s≤s rv'≤lvrPre ⟩
          (suc $ Meta.getLastVoteRound (hpPre ^∙ pssSafetyData-rm)) ≤⟨ s≤s lvRound≤ ⟩
          (suc $ hpPre ^∙ pssSafetyData-rm ∙ sdLastVotedRound)      ≤⟨ lvr< ⟩
          hpPos ^∙ pssSafetyData-rm ∙ sdLastVotedRound              ≡⟨ sym lvr≡ ⟩
          vote  ^∙ vRound                                           ≡⟨ sym (cong (_^∙ vRound) v≡vote) ⟩
          v     ^∙ vRound                                           ∎
          where
          open ≤-Reasoning
          open SafetyDataInv (SafetyRulesInv.sdInv rmSafetyRulesInv)

      analyzeVoteAttempt : just v ≡ peerStates pre pid ^∙ pssSafetyData-rm ∙ sdLastVote
      analyzeVoteAttempt
         with BlockId-correct? (pm ^∙ pmProposal)
      ...| no ¬validProposal rewrite sym (proj₁ (invalidProposal ¬validProposal)) = ≡pidLV
      ...| yes refl
         with voteAttemptCorrect refl (nohc rss m∈pool pid ini (invariantsCorrect pid pre ini rss) refl refl)
      ...| Voting.mkVoteAttemptCorrectWithEpochReq (Left (_ , Voting.mkVoteUnsentCorrect noVoteMsgOuts nvg⊎vgusc)) sdEpoch≡?
         with nvg⊎vgusc
      ...| Left (mkVoteNotGenerated lv≡ lvr≤) = OldVote.≡pidLVPre₁ lv≡
      ...| Right (Voting.mkVoteGeneratedUnsavedCorrect vote (Voting.mkVoteGeneratedCorrect (mkVoteGenerated lv≡v voteSrc) blockTriggered))
         with voteSrc
      ...| Left (mkVoteOldGenerated lvr≡ lv≡) = OldVote.≡pidLVPre₁ lv≡
      ...| Right (mkVoteNewGenerated lvr< lvr≡) =
         ⊥-elim (<⇒≢ (NewVote.rv'<rv vote lv≡v lvr< lvr≡ sdEpoch≡? blockTriggered) (sym ≡round))
      analyzeVoteAttempt | yes refl | Voting.mkVoteAttemptCorrectWithEpochReq (Right (Voting.mkVoteSentCorrect vm pid voteMsgOuts vgCorrect)) sdEpoch≡?
         with vgCorrect
      ...| Voting.mkVoteGeneratedCorrect (mkVoteGenerated lv≡v voteSrc) blockTriggered
         with voteSrc
      ...| Left (mkVoteOldGenerated lvr≡ lv≡) = OldVote.≡pidLVPre₁ lv≡
      ...| Right (mkVoteNewGenerated lvr< lvr≡) =
         ⊥-elim (<⇒≢ (NewVote.rv'<rv (vm ^∙ vmVote) lv≡v lvr< lvr≡ sdEpoch≡? blockTriggered) (sym ≡round))

-- This is the origin of the message
sameERasLV⇒sameId{pid}{pid'}{pk} (step-s rss (step-peer{pre = pre} sp@(step-honest{pid“} sps@(step-msg{sndr , m} m∈pool ini)))) {v}{v'} hpk ≡pidLV pcsfpk v'⊂m' m'∈pool sig' ¬bootstrap ≡epoch ≡round
   | Left (m'∈acts , pcsfpk' , ¬msb4)
   -- So `pid“` must be `pid`
   with PeerCanSignForPKProps.pidInjective pcsfpk pcsfpk' ≡epoch
...| refl
   with v'⊂m'
   -- QC vote signatures have been sent before
...| vote∈qc{qc = qc} vs∈qc v≈ qc∈m'
   rewrite cong _vSignature v≈
   = ⊥-elim ∘′ ¬msb4 $ qcVoteSigsSentB4-handle pid rss sps m'∈acts qc∈m' sig' vs∈qc v≈ ¬bootstrap
...| vote∈vm
   rewrite sym $ StepPeer-post-lemma{pre = pre} sp
   = sameId m m∈pool m'∈acts ≡pidLV
   where

   handlePre = peerStates pre pid

   handleOuts : NetworkMsg → List Output
   handleOuts m = LBFT-outs (handle sndr m 0) handlePre

   handlePst : NetworkMsg → RoundManager
   handlePst m = LBFT-post (handle sndr m 0) handlePre

   sameId : ∀ {sndr} m → (sndr , m) ∈ msgPool pre
          → send (V (VoteMsg∙new v' _)) ∈ outputsToActions{State = handlePre} (handleOuts m)
          → just v ≡ handlePst m ^∙ pssSafetyData-rm ∙ sdLastVote → v ≡L v' at vProposedId
   sameId (P pm) m∈pool m'∈acts ≡pidLV = analyzeVoteAttempt
     where
     open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm (msgPool pre) handlePre)

     analyzeVoteAttempt : v ≡L v' at vProposedId
     analyzeVoteAttempt
        with BlockId-correct? (pm ^∙ pmProposal)
     ...| no ¬validProposal = ⊥-elim (sendVote∉actions {outs = handleOuts (P pm)} {st = handlePre}
                                      (sym (proj₂ $ invalidProposal ¬validProposal)) m'∈acts)
     ...| yes refl
        with voteAttemptCorrect refl (nohc rss m∈pool pid ini (invariantsCorrect pid pre ini rss) refl refl)
     ...| Voting.mkVoteAttemptCorrectWithEpochReq (Left (_ , vuc)) sdEpoch≡? =
        ⊥-elim (sendVote∉actions {outs = handleOuts (P pm)} {st = handlePre} (sym $ Voting.VoteUnsentCorrect.noVoteMsgOuts vuc) m'∈acts)
     ...| Voting.mkVoteAttemptCorrectWithEpochReq (Right (Voting.mkVoteSentCorrect vm pid voteMsgOuts vgCorrect)) sdEpoch≡?
        with vgCorrect
     ...| Voting.mkVoteGeneratedCorrect (mkVoteGenerated lv≡v voteSrc) blockTriggered = cong (_^∙ vProposedId) v≡v'
        where
        open ≡-Reasoning

        v≡v' : v ≡ v'
        v≡v' = just-injective $ begin
          just v
            ≡⟨ ≡pidLV ⟩
          (handlePst (P pm)                              ^∙ pssSafetyData-rm ∙ sdLastVote)
            ≡⟨ sym lv≡v ⟩
          just (vm ^∙ vmVote)
            ≡⟨ cong (just ∘ _^∙ vmVote) (sym $ sendVote∈actions{outs = handleOuts (P pm)}{st = handlePre} (sym voteMsgOuts) m'∈acts) ⟩
          just v' ∎

   sameId (V vm) _ m'∈acts ≡pidLV =
     ⊥-elim (sendVote∉actions {outs = hvOuts} {st = peerStates pre pid} (sym noVotes) m'∈acts)
     where
     hvOuts = LBFT-outs (handleVote 0 vm) (peerStates pre pid)

     open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) handlePre)
   sameId (C x) _ ()

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

votesOnce₁ : Common.IncreasingRoundObligation Handle.InitHandler.initAndHandlers 𝓔

votesOnce₁ {pid = pid} {pid'} {pk = pk} {pre = pre} preach
           (step-init {rm} rm×acts uni)
           {v} {m} {v'} {m'} hpk v⊂MsgPpm m∈acts sig ¬bootstrap ¬msb pcspkv v'⊂m' m'∈pool sig' ¬bootstrap' eid≡
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  with initHandlerSpec.ContractOk.isInitPM init-contract m∈acts
...| (_ , _ , noSigs)
  with v⊂MsgPpm
...| vote∈qc vs∈qc v≈rbld qc∈nm
  = ⊥-elim (noSigs vs∈qc qc∈nm)

votesOnce₁ {pid = pid} {pid'} {pk = pk} {pre = pre} preach sps@(step-msg {sndr , P pm} m∈pool ini) {v} {m} {v'} {m'} hpk (vote∈qc {vs} {qc} vs∈qc v≈rbld qc∈m) m∈acts sig ¬bootstrap ¬msb pcspkv v'⊂m' m'∈pool sig' ¬bootstrap' eid≡
   with cong _vSignature v≈rbld
...| refl = ⊥-elim ∘′ ¬msb $ qcVoteSigsSentB4-handle pid preach sps m∈acts qc∈m sig vs∈qc v≈rbld ¬bootstrap

votesOnce₁ {pid = pid} {pid'} {pk = pk} {pre = pre} preach sps@(step-msg {sndr , P pm} m∈pool ini) {v} {.(V (VoteMsg∙new v _))} {v'} {m'} hpk vote∈vm m∈acts sig ¬bootstrap ¬msb pcspkv v'⊂m' m'∈pool sig' ¬bootstrap' eid≡
  with handleProposalSpec.contract! 0 pm (msgPool pre) (peerStates pre pid)
...| handleProposalSpec.mkContract _ invProp noEpochChange vac _ _
   with BlockId-correct? (pm ^∙ pmProposal)
...| no ¬validProposal = ⊥-elim (sendVote∉actions {outs = hpOut} {st = hpPre} (sym (proj₂ $ invProp ¬validProposal)) m∈acts )
   where
   hpPre  = peerStates pre pid
   hpOut  = LBFT-outs (handleProposal 0 pm) hpPre
...| yes refl
   with vac refl (nohc preach m∈pool pid ini (invariantsCorrect pid pre ini preach) refl refl)
...| Voting.mkVoteAttemptCorrectWithEpochReq (inj₁ (_ , Voting.mkVoteUnsentCorrect noVoteMsgOuts nvg⊎vgusc)) sdEpoch≡? =
     ⊥-elim (sendVote∉actions{outs = LBFT-outs (handleProposal 0 pm) (peerStates pre pid)}{st = peerStates pre pid} (sym noVoteMsgOuts) m∈acts)
...| Voting.mkVoteAttemptCorrectWithEpochReq (inj₂ (Voting.mkVoteSentCorrect vm pid₁ voteMsgOuts vgCorrect)) sdEpoch≡?
  with sendVote∈actions{outs = LBFT-outs (handleProposal 0 pm) (peerStates pre pid)}{st = peerStates pre pid} (sym voteMsgOuts) m∈acts
...| refl = ret
  where
  -- Some definitions
  step = step-peer (step-honest sps)
  rmPre  = peerStates pre pid
  rmPost = peerStates (StepPeer-post{pre = pre} (step-honest sps)) pid

  -- State invariants
  rmInvs      = invariantsCorrect pid pre ini preach
  open RoundManagerInv rmInvs

  -- Properties of `handleProposal`
  postLV≡ : just v ≡ (rmPost ^∙ pssSafetyData-rm ∙ sdLastVote)
  postLV≡ =
    trans (RoundManagerTransProps.VoteGenerated.lv≡v ∘ Voting.VoteGeneratedCorrect.state $ vgCorrect)
      (cong (_^∙ pssSafetyData-rm ∙ sdLastVote) (StepPeer-post-lemma (step-honest sps)))

  -- The proof
  m'mwsb : MsgWithSig∈ pk (ver-signature sig') (msgPool pre)
  m'mwsb = mkMsgWithSig∈ m' v' v'⊂m' pid' m'∈pool sig' refl

  pcspkv'-pre : PeerCanSignForPK pre v' pid pk
  pcspkv'-pre = PeerCanSignForPKProps.msb4 preach step (peerCanSignEp≡{v' = v'} pcspkv eid≡) hpk sig' m'mwsb

  rv'≤rv : v' ^∙ vRound ≤ v ^∙ vRound
  rv'≤rv =
    ≤-trans
      (oldVoteRound≤lvr preach hpk sig' ¬bootstrap' m'mwsb pcspkv'-pre (trans rmPreEsEpoch≡ eid≡))
      realLVR≤rv
    where
    open ≡-Reasoning
    -- TODO-1 : `rmPreSdEpoch≡` can be factored out into a lemma.
    -- Something like: for any reachable state where a peer sends a vote, the
    -- epoch for that vote is the peer's sdEpoch / esEpoch.
    rmPreSdEpoch≡ : rmPre ^∙ pssSafetyData-rm ∙ sdEpoch ≡ v ^∙ vEpoch
    rmPreSdEpoch≡
       with Voting.VoteGeneratedCorrect.state vgCorrect
       |    Voting.VoteGeneratedCorrect.blockTriggered vgCorrect
    ...| RoundManagerTransProps.mkVoteGenerated lv≡v (Left (RoundManagerTransProps.mkVoteOldGenerated lvr≡ lv≡)) | _
       with SafetyDataInv.lvEpoch≡ ∘ SafetyRulesInv.sdInv $ rmSafetyRulesInv
    ...| sdEpochInv rewrite trans lv≡ (sym lv≡v) = sym sdEpochInv
    rmPreSdEpoch≡
       | RoundManagerTransProps.mkVoteGenerated lv≡v (Right (RoundManagerTransProps.mkVoteNewGenerated lvr< lvr≡)) | bt =
      trans sdEpoch≡? (sym ∘ proj₁ ∘ Voting.VoteMadeFromBlock⇒VoteEpochRoundIs $ bt)

    rmPreEsEpoch≡ : rmPre ^∙ rmEpochState ∙ esEpoch ≡ v ^∙ vEpoch
    rmPreEsEpoch≡ =
      begin rmPre ^∙ rmEpochState ∙ esEpoch ≡⟨ rmEpochsMatch   ⟩
            rmPre ^∙ pssSafetyData-rm  ∙ sdEpoch ≡⟨ rmPreSdEpoch≡ ⟩
            v     ^∙ vEpoch                 ∎

    realLVR≤rv : Meta.getLastVoteRound (rmPre ^∙ pssSafetyData-rm) ≤ v ^∙ vRound
    realLVR≤rv
      with Voting.VoteGeneratedCorrect.state vgCorrect
    ...| RoundManagerTransProps.mkVoteGenerated lv≡v (inj₁ (RoundManagerTransProps.mkVoteOldGenerated lvr≡ lv≡))
      rewrite trans lv≡ (sym lv≡v)
        = ≤-refl
    ...| RoundManagerTransProps.mkVoteGenerated lv≡v (inj₂ (RoundManagerTransProps.mkVoteNewGenerated lvr< lvr≡))
       with rmPre ^∙ pssSafetyData-rm ∙ sdLastVote
       |    SafetyDataInv.lvRound≤ ∘ SafetyRulesInv.sdInv $ rmSafetyRulesInv
    ...| nothing | _ = z≤n
    ...| just lv | round≤ = ≤-trans (≤-trans round≤ (<⇒≤ lvr<)) (≡⇒≤ (sym lvr≡))

  ret : v' [ _<_ ]L v at vRound ⊎ Common.VoteForRound∈ Handle.InitHandler.initAndHandlers 𝓔 pk (v ^∙ vRound) (v ^∙ vEpoch) (v ^∙ vProposedId) (msgPool pre)
  ret
    with <-cmp (v' ^∙ vRound) (v ^∙ vRound)
  ...| tri< rv'<rv _ _ = Left rv'<rv
  ...| tri≈ _ rv'≡rv _
    = Right (Common.mkVoteForRound∈ _ v' v'⊂m' pid' m'∈pool sig' (sym eid≡) rv'≡rv
        (sym (sameERasLV⇒sameId (step-s preach step) hpk postLV≡ pcspkv v'⊂m' (Any-++ʳ _ m'∈pool) sig' ¬bootstrap' eid≡ (sym rv'≡rv) )))
  ...| tri> _ _ rv'>rv = ⊥-elim (≤⇒≯ rv'≤rv rv'>rv)

votesOnce₁{pid = pid}{pid'}{pk = pk}{pre = pre} preach sps@(step-msg{sndr , V vm} m∈pool ini){v}{m}{v'}{m'} hpk v⊂m m∈acts sig ¬bootstrap ¬msb vspk v'⊂m' m'∈pool sig' ¬bootstrap' eid≡
  with v⊂m
...| vote∈qc vs∈qc v≈rbld qc∈m rewrite cong _vSignature v≈rbld =
       ⊥-elim ∘′ ¬msb $ qcVoteSigsSentB4-handle pid preach sps m∈acts qc∈m sig vs∈qc v≈rbld ¬bootstrap
...| vote∈vm =
  ⊥-elim (sendVote∉actions{outs = hvOut}{st = hvPre} (sym noVotes) m∈acts)
  where
  hvPre = peerStates pre pid
  hvOut = LBFT-outs (handleVote 0 vm) hvPre
  open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)

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

votesOnce₂ : VO.ImplObligation₂ Handle.InitHandler.initAndHandlers 𝓔

votesOnce₂ {pid} {pk = pk} {pre} rss
           (step-init {rm} rm×acts uni)
           hpk v⊂m m∈acts sig ¬bootstrap ¬msb4 pcsfpk v'⊂m' m'∈acts sig' ¬bootstrap' ¬msb4' pcsfpk' ≡epoch ≡round
   with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
   with initHandlerSpec.ContractOk.isInitPM init-contract m∈acts
...| (_ , refl , noSigs)
  with v⊂m
...| vote∈qc vs∈qc v≈rbld qc∈pm = ⊥-elim (noSigs vs∈qc qc∈pm)

votesOnce₂{pid}{pk = pk}{pre} rss (step-msg{sndr , m“} m“∈pool ini){v}{v' = v'} hpk v⊂m m∈acts sig ¬bootstrap ¬msb4 pcsfpk v'⊂m' m'∈acts sig' ¬bootstrap' ¬msb4' pcsfpk' ≡epoch ≡round
   with v⊂m
...| vote∈qc vs∈qc v≈rbld qc∈m rewrite cong _vSignature v≈rbld =
       ⊥-elim ∘′ ¬msb4 $ qcVoteSigsSentB4-handle pid rss (step-msg m“∈pool ini) m∈acts qc∈m sig vs∈qc v≈rbld ¬bootstrap
...| vote∈vm
  with v'⊂m'
...| vote∈qc vs∈qc' v≈rbld' qc∈m' rewrite cong _vSignature v≈rbld' =
       ⊥-elim ∘′ ¬msb4' $ qcVoteSigsSentB4-handle pid rss (step-msg m“∈pool ini) m'∈acts qc∈m' sig' vs∈qc' v≈rbld' ¬bootstrap'
...| vote∈vm
  with m“
...| P pm = cong (_^∙ vProposedId) v≡v'
  where
  hpPool = msgPool pre
  hpPre  = peerStates pre pid
  hpOut  = LBFT-outs (handleProposal 0 pm) hpPre
  open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm hpPool hpPre)

  v≡v' : v ≡ v'
  v≡v'
    with BlockId-correct? (pm ^∙ pmProposal)
  ...| no ¬validProposal = ⊥-elim (sendVote∉actions {outs = hpOut} {st = hpPre} (sym (proj₂ $ invalidProposal ¬validProposal)) m∈acts)
  ...| yes refl
    with voteAttemptCorrect refl (nohc rss m“∈pool pid ini (invariantsCorrect pid pre ini rss) refl refl   )
  ...| Voting.mkVoteAttemptCorrectWithEpochReq (Left (_ , Voting.mkVoteUnsentCorrect noVoteMsgOuts _)) _ =
    ⊥-elim (sendVote∉actions{outs = hpOut}{st = hpPre} (sym noVoteMsgOuts) m∈acts)
  ...| Voting.mkVoteAttemptCorrectWithEpochReq (Right (Voting.mkVoteSentCorrect vm pid voteMsgOuts _)) _ = begin
    v            ≡⟨        cong (_^∙ vmVote) (sendVote∈actions{outs = hpOut}{st = hpPre} (sym voteMsgOuts) m∈acts) ⟩
    vm ^∙ vmVote ≡⟨ (sym $ cong (_^∙ vmVote) (sendVote∈actions{outs = hpOut}{st = hpPre} (sym voteMsgOuts) m'∈acts)) ⟩
    v'           ∎
    where
    open ≡-Reasoning
...| V vm = ⊥-elim (sendVote∉actions{outs = hvOut}{st = hvPre} (sym noVotes) m∈acts)
  where
  hvPre = peerStates pre pid
  hvOut = LBFT-outs (handle pid (V vm) 0) hvPre
  open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)


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

record R : Set1 where

  Bla : Set1
  Bla with Set
  ... | _ = Set

  field
    F : Set

-- Current error:
-- Missing definition for Bla

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

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Unary.All.Properties directly.
------------------------------------------------------------------------

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

module Data.Vec.All.Properties where

open import Data.Vec.Relation.Unary.All.Properties public

{-# WARNING_ON_IMPORT
"Data.Vec.All.Properties was deprecated in v1.0.
Use Data.Vec.Relation.Unary.All.Properties instead."
#-}


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

-- Theorems about noninterference.

open import Calf.CostMonoid

module Calf.Noninterference (costMonoid : CostMonoid) where

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.Step costMonoid
open import Calf.PhaseDistinction
open import Calf.Types.Eq

open import Data.Product
open import Relation.Binary.PropositionalEquality as P

oblivious : ∀ {A B} (f : cmp (F A) → val (◯⁺ B)) →
      ∀ c e → f (step (F A) c e) ≡ f e
oblivious {A} {B} f c e = funext/Ω (λ u →
  begin
  f (step (F A) c e) u ≡⟨ cong (λ e → f e u) (step/ext (F A) e c u) ⟩
  f e u
  ∎
  )
  where open ≡-Reasoning

unique : ∀ {A} → (a : val (● A)) → (u : ext) → a ≡ ∗ u
unique {A} a u =
  eq/ref
  (●/ind {A} a (λ a → F (eq (● A) a (∗ u)))
  (λ a → ret (eq/intro (η≡∗ a u)))
  (λ u → ret (eq/intro refl))
  (λ a u → eq/uni _ _ u))

constant : ∀ {A B} (f : val (● A) → val (◯⁺ B)) →
  Σ (val (◯⁺ B)) λ b → f ≡ λ _ → b
constant f =
  (λ u → f (∗ u) u) , funext (λ a → funext/Ω (λ u →
    P.cong (λ a → f a u) (unique a u)))

optimization : ∀ {C B : tp pos} {A : val C → tp pos}
  (f : val (Σ++ C λ c → ● (A c)) → val (◯⁺ B)) →
  Σ (val C → val (◯⁺ B)) λ f' → ∀ c a → f (c , a) ≡ f' c
optimization {C} {B} {A} f =
  (λ c →
    let g : val (● (A c)) → val (◯⁺ B)
        g a = f (c , a) in
    let (b , h) = constant {A c} {B} g in
    b) ,
    λ c a →
    let g : val (● (A c)) → val (◯⁺ B)
        g a = f (c , a) in
    let (b , h) = constant {A c} {B} g in
    P.cong-app h a

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Punctaffy.Hypersnippet.Hyperstack where

open import Level using (Level; _⊔_)

open import Punctaffy.Hypersnippet.Dim using (DimSys; dimLte)

data DimList {n l : Level} : DimSys {n} {l} → Set (n ⊔ l) → Set (n ⊔ l) where
  makeDimList : {ds : DimSys} → {a : Set (n ⊔ l)} → (len : DimSys.Carrier ds) → ((i : DimSys.Carrier ds) → dimLte {n} {l} {ds} i len → a) → DimList ds a

max_stars_repo_name: rocketnia/lexmeta

max_issues_repo_name: rocketnia/lexmeta

max_forks_repo_name: lathe/punctaffy-for-racket


text:
module Tests where
  open import BasicFunctions
  open import TransportLemmas
  open import EquivalenceType
  open import QuasiinverseType
  open import QuasiinverseLemmas
  open import HLevelTypes
  open import HLevelLemmas
  open import UnivalenceAxiom
  open import CoproductIdentities

  equiv-is-inj
    : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
    → (f : A → B) → isEquiv f
    → ∀ {x y : A} → (f x ≡ f y) → x ≡ y

  equiv-is-inj {A = A}{B} f f-is-equiv fx≡fy = ! cr · (ap f^-1 fx≡fy · cr)
    where
    f^-1 : B → A
    f^-1 = remap (f , f-is-equiv)

    cr : ∀ {x : A} → f^-1 (f x) ≡ x
    cr = rlmap-inverse (f , f-is-equiv)

  module _ {ℓ : Level} {A : Type ℓ} where
    equiv-induction
        : (P : (C : Type ℓ) → (A ≃ C) → Type ℓ)
        → P A idEqv
        → (C : Type ℓ)
        → (e : A ≃ C)
        -----------------------------
        → P C e

    equiv-induction P p-refl C e  = tr (P C) (ua-β e) g
      where
      open import HLevelLemmas
      P' :  (C : Type ℓ) → A ≡ C → Type ℓ
      P' C p = P C (idtoeqv p)

      b' : P A (idtoeqv idp)
      b' = tr (P A) (sameEqv idp) p-refl

      f' : (C : Type ℓ) → (p : A ≡ C) → P C (idtoeqv p)
      f' C idp = b'

      g : P C (idtoeqv (ua e))
      g = f' C (ua e)

    postcomp-is-equiv
      : (B : Type ℓ)
      → (e : A ≃ B)
      → ∀ {C : Type ℓ}
      → isEquiv {A = C → A} {B = C → B} (_:> (e ∙→))

    postcomp-is-equiv  B e
      = equiv-induction (λ C A≃C → isEquiv (_:> (A≃C ∙→) )) base-case B e
      where
      base-case : isEquiv (λ f x → π₁ idEqv (f x))
      base-case = π₂ idEqv

    postcomp-≃
      : (B : Type ℓ)
      → (e : A ≃ B)
      → (X : Type ℓ)
      → (X → A) ≃ (X → B)
    postcomp-≃ B e X  = (_:> (e ∙→)) , postcomp-is-equiv B e

    postcomp-is-inj
      : (B : Type ℓ)
      → (e : A ≃ B)
      → {C : Type ℓ}
      → (f g : C → A)
      → f :> (e ∙→) ≡ g :> (e ∙→)
      → f ≡ g

    postcomp-is-inj B e f g p =
      equiv-is-inj (_:> (e ∙→)) (postcomp-is-equiv B e) p

  --  The naive non-dependent function extensionality axiom
  funext'
    : {ℓ : Level} {A : Type ℓ}{B : Type ℓ}
    → (f g : A → B)
    → (h : ∏[ x ∶ A ] (f x ≡ g x))
    → f ≡ g

  funext' {A = A}{B} f g h = ap (_:> p₁) d≡e
    where
    d e : A → ∑[ (x , y ) ∶ (B × B) ] (x ≡ y)
    d = λ x → ((f x , f x)) , refl (f x)
    e = λ x → ((f x , g x)) , h x

    p₀ : ∑[ (x , y ) ∶ (B × B) ] (x ≡ y) → B
    p₀ ((x , y) , p) = x

    p₁ : ∑[ (x , y ) ∶ (B × B) ] (x ≡ y) → B
    p₁ ((x , y) , p) = y

    p₀-is-equiv : isEquiv p₀
    p₀-is-equiv
      = π₂ (qinv-≃ p₀ ((λ x → ((x , x) , (refl x) )) ,
          (λ {p → idp}) , (λ {((x , .x) , idp) → idp})))

    d:>p₀≡e:>p₀ : (d :> p₀) ≡ (e :> p₀)
    d:>p₀≡e:>p₀ = idp

    d≡e : d ≡ e
    d≡e = postcomp-is-inj B (p₀ , p₀-is-equiv) d e d:>p₀≡e:>p₀

  -- naive-funext implies weak extensionality:

  open import FibreType
  open import EquivalenceReasoning

  left-universal-property-of-idenity-type
    : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    → (a x : A)
    → (∑[ p ∶ a ≡ x ] B a) ≃  (∑[ b ∶ B a ] a ≡ x)
  left-universal-property-of-idenity-type a x
    = qinv-≃ f (g , ((λ {(_ , idp) → idp}) , λ { (idp , π₄) → idp}))
    where
    f = λ {(idp , b) → (b , idp)}
    g = λ {(b , p) → (p , b)}

  universal-property-of-identity-type
    : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    → (x : A)
    → B x ≃ (∑[ a ∶ A ] ∑[ p ∶ a ≡ x ] B a)
  universal-property-of-identity-type x = qinv-≃ f (g , (λ { (a , idp , π₄) → idp})  , λ {p → idp})
    where
    f = λ b → (x , (refl x , b))
    g = λ {(a , (idp , b)) → b}

  contr-fibers-gives-pr₁-equiv
    : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    → ((x : A) → isContr (B x)) → (pr₁ {A = A}{B}) is-equiv
  contr-fibers-gives-pr₁-equiv {A = A}{B} Bx-is-contr
    = λ x → equiv-preserves-contr (calculation x) (Bx-is-contr x)
    where
    open import SigmaEquivalence
    open import SigmaPreserves
    open import HLevelLemmas
    calculation : (x : A) → (B x) ≃ fib (pr₁ {A = A}{B}) x
    calculation x =
      begin≃
        B x
          ≃⟨ universal-property-of-identity-type {A = A}{B} x  ⟩
       ∑[ a ∶ A ] (∑[ p ∶ a ≡ x ] B a)
          ≃⟨ sigma-preserves (λ a → left-universal-property-of-idenity-type {A = A}{B} a x) ⟩
       ∑[ a ∶ A ] (∑[ b ∶ B a ] a ≡ x)
         ≃⟨⟩
       ∑[ a ∶ A ] (∑[ b ∶ B a ] (pr₁ {A = A}{B} (a , b) ≡ x) )
         ≃⟨  ∑-assoc ⟩
       (∑[ p ∶ ∑ A B ] (pr₁ p ≡ x))
          ≃⟨⟩
       fib (pr₁ {A = A}{B}) x
        ≃∎

  happly : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    → {f g : ∏ A B}
    → (f ≡ g)
    → (x : A) →  (f x ≡ g x)
  happly idp x = idp

  weak-extensionality pi-is-contr
    : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    →  ((x : A) → isContr (B x)) → isContr (Π A B)
  weak-extensionality {ℓ₁}{ℓ₂}{A}{B} Bx-is-contr
   = retract-of-singleton Π-is-retract fib-α-id-is-contr
    where
    open import SectionsAndRetractions

    α≃ : ((↑ ℓ₂ A) → ∑ (↑ ℓ₂ A) λ { (Lift a) → B a}) ≃ ((↑ ℓ₂ A) → ↑ ℓ₂ A)
    α≃ = postcomp-≃ (↑ ℓ₂ A)
      (pr₁ , contr-fibers-gives-pr₁-equiv
        (λ { (Lift a) → Bx-is-contr a})) (↑ ℓ₂ A)
    α = α≃ ∙→

    fib-α-id = fib α (id-on (↑ ℓ₂ A))
    fib-α-id-is-contr : isContr (fib-α-id)
    fib-α-id-is-contr = pr₂ α≃ (id-on (↑ ℓ₂ A))

    φ : fib-α-id → Π A B
    φ (g , p) = λ x → tr (λ { (Lift a) → B a}) (happly p (Lift x)) (pr₂ (g (Lift x)))

    ψ : (f : Π A B) → fib-α-id
    ψ f = ((λ {(Lift a) → (Lift a) , f a}) , refl (id-on (↑ ℓ₂ A)))

    Π-is-retract : retract (Π A B) of fib-α-id
    Π-is-retract = (φ , (ψ , λ f → idp))
  pi-is-contr = weak-extensionality

  funext
    : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    → (f g : ∏ A B)
    → (h : ∏[ x ∶ A ] (f x ≡ g x))
    → f ≡ g

  funext {ℓ₁}{ℓ₂}{A}{B} f g h = ap (_!-inv) p
    where
    hat : (∏ A B) → (↑ ℓ₂ A) → ∑ A B
    hat f (Lift a) = (a , f a)

    hat-f≡hat-g : (hat f) ≡ (hat g)
    hat-f≡hat-g = funext' (hat f) (hat g) (λ { (Lift a) → pair= (idp , h a)})

    _! : ∏ A B → ∑[ h ∶ ((↑ ℓ₂ A) → ∑ A B) ] (∏[ x ∶ (↑ ℓ₂ A) ] (π₁ (h x) ≡ lower x) )
    f ! = ( hat f , λ { (Lift a) → refl a})

    _!-inv : ∑[ h ∶ ((↑ ℓ₂ A) → ∑ A B) ] (∏[ x ∶ (↑ ℓ₂ A) ] (π₁ (h x) ≡ (lower x)) ) → ∏ A B
    _!-inv (h , p) = λ x → tr B (p (Lift x)) (π₂ (h (Lift x)))

    -- see that, the round trip gives.
    _ : ((f !) !-inv)  ≡ f
    _ = idp

    p : (f !) ≡ (g !)
    p = pair= (hat-f≡hat-g , q)
      where
      open import HLevelLemmas
      q : PathOver (λ h₁ → ∏ (↑ ℓ₂ A) (λ x → π₁ (h₁ x) ≡ lower x))
                    (π₂ (f !)) hat-f≡hat-g (π₂ (g !))
      q = contr-is-prop  (weak-extensionality (λ {(Lift a) → idp , λ { idp → idp}}))
        (tr (λ h → ∏ (↑ ℓ₂ A) λ x → π₁ (h x) ≡ lower x) hat-f≡hat-g (π₂ (f !))) (π₂ (g !))

  fiberwise-transformation fiberwise-map-from_to_
    : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
    → (P Q : A → Type ℓ₂)
    → Type (ℓ₁ ⊔ ℓ₂)
  fiberwise-transformation P Q = ∏[ x ] (P x → Q x)
  fiberwise-map-from_to_ = fiberwise-transformation

  total
    : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{P Q : A → Type ℓ₂}
    → (f : fiberwise-map-from P to Q)
    → ((∑ A P) → (∑ A Q))
  total f (a , p) = ( a , f a p)

  fib-total-≃fib-fiberwise
    : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{P Q : A → Type ℓ₂}
    → (f : fiberwise-map-from P to Q)
    → (x : A) (v : Q x)
    → fib (total f) (( x , v)) ≃ fib (f x) v

  fib-total-≃fib-fiberwise {P = P}{Q} f x v =
    qinv-≃ f' (g' , (λ {(p , idp) → idp}) , λ { (a , idp) → idp})
    where
    private
      f' = λ { ((a , p) , idp) → (p , idp)}
      g' = λ { (p , idp) → ( (x , p) , idp)}

  fib-total-equiv-from-fiberwise-equiv
    :  ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{P Q : A → Type ℓ₂}
    → (f : fiberwise-map-from P to Q)
    → ((x : A) → (f x) is-equiv)  -- this says f is fiberwise equivalence.
    →  ((total f) is-equiv)
  fib-total-equiv-from-fiberwise-equiv f f-fiberwise-equiv
    = λ x → equiv-preserves-contr
                    (≃-sym (fib-total-≃fib-fiberwise f (π₁ x) (π₂ x)))
                    (f-fiberwise-equiv (π₁ x) (π₂ x))

  fib-total-equiv-to-fiberwise-equiv
    :  ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{P Q : A → Type ℓ₂}
    → (f : fiberwise-map-from P to Q)
    → ((total f) is-equiv)
    → ((x : A) → (f x) is-equiv)
  fib-total-equiv-to-fiberwise-equiv f total-is-equiv
    = λ x → λ p → equiv-preserves-contr (fib-total-≃fib-fiberwise f x p) (total-is-equiv ((x , p)))

  happly-is-equiv
    :  ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : A → Type ℓ₂}
    → {f g : ∏ A B}
    → (happly {f = f} {g}) is-equiv

  happly-is-equiv {A = A}{B}{f = f}{g} h
    = fib-total-equiv-to-fiberwise-equiv s total-happly-is-equiv g h
    where
    open import SigmaEquivalence
    calculation
      : (∏[ x ∶ A ] (∑[ u ∶ B x ] (f x ≡ u)))
      ≃ (∑[ g ∶ ∏ A B ] (∏[ x ∶ A ] (f x ≡ g x)))
    calculation = choice

    α-codomain-is-contr : isContr ((∑[ g ∶ ∏ A B ] (∏[ x ∶ A ] (f x ≡ g x))))
    α-codomain-is-contr
     = equiv-preserves-contr
         choice
         (pi-is-contr (λ x → pathfrom-is-contr _ _))

    s : (g : (∏ A B)) → (f ≡ g) → (∏[ x ∶ A ] (f x ≡ g x))
    s g p = happly p

    α : (∑[ g ∶ (∏ A B) ] (f ≡ g)) → (∑[ g ∶  ∏ A B ] ∏[ x ∶ A ] (f x ≡ g x))
    α (g , p) = (g , happly p)

    total-happly-is-equiv : α is-equiv
    total-happly-is-equiv (g , p) =
      map-domain-and-codomain-contr-is-equiv
        α-domain-is-contr
        α-codomain-is-contr _ _
      where
      open import SectionsAndRetractions
      α-domain-is-contr : isContr (domain α)
      α-domain-is-contr = pathfrom-is-contr _ _

      map-domain-and-codomain-contr-is-equiv : ∀ {ℓ₁ ℓ₂ : Level}{X : Type ℓ₁}{Y : Type ℓ₂}
        → X is-contr
        → Y is-contr
        → (f : X → Y)
        → f is-equiv
      map-domain-and-codomain-contr-is-equiv {X = X}{Y} X-is-contr Y-is-contr f
        = λ y → ((center-of X-is-contr , contr-is-prop Y-is-contr _ _))
          , λ x → pair= (contr-is-prop X-is-contr _ _ ,
          prop-is-set (contr-is-prop Y-is-contr) _ _ _ _)

max_stars_repo_name: jonaprieto/mini-hott

max_issues_repo_name: jonaprieto/mini-hott

max_forks_repo_name: jonaprieto/mini-hott


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

module Light.Library.Relation.Decidable where

open import Light.Level using (Setω ; Level)
open import Light.Variable.Levels
open import Light.Variable.Sets
open import Light.Library.Relation using (Base ; Kind ; Style)
open import Light.Indexed using (Indexed ; thing ; indexed)
open import Light.Package using (Package)

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field base : Base

      open Style (base .Base.style) using (True ; False)
      open Kind (base .Base.kind) using (Index ; Proposition)

      field
            ℓf : Index → Level
            Decidable : ∀ {i} → Proposition i → Set (ℓf i)
      kind : Kind
      kind = record { Index = Indexed Index Proposition ; Proposition = λ i → Decidable (thing i) }
      field
            instance style : Style kind
            if′_then_else_ : ∀ {i} {𝕒 : Proposition i} → Decidable 𝕒 → 𝕓 → 𝕓 → 𝕓
            if_then_else_ :
                  ∀ {i} {𝕒 : Proposition i}
                  → Decidable 𝕒
                  → (∀ ⦃ witness : True 𝕒 ⦄ → 𝕓)
                  → (∀ ⦃ witness : False 𝕒 ⦄ → 𝕓)
                  → 𝕓

            to‐witness : ∀ {i} {𝕒 : Proposition i} {a? : Decidable 𝕒} ⦃ truth : Style.True style a? ⦄ → True 𝕒
            to‐false‐witness : ∀ {i} {𝕒 : Proposition i} {a? : Decidable 𝕒} ⦃ falsehood : Style.False style a? ⦄ → False 𝕒

            ⦃ from‐witness ⦄ : ∀ {i} {𝕒 : Proposition i} {a? : Decidable 𝕒} ⦃ witness : True 𝕒 ⦄ → Style.True style a?
            ⦃ from‐false‐witness ⦄ : ∀ {i} {𝕒 : Proposition i} {a? : Decidable 𝕒} ⦃ witness : False 𝕒 ⦄ → Style.False style a?

            yes : ∀ {i} {𝕒 : Proposition i} → True 𝕒 → Decidable 𝕒
            no : ∀ {i} {𝕒 : Proposition i} → False 𝕒 → Decidable 𝕒
      instance base′ = record { kind = kind ; style = style }

open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.Liveness.ProposerElection where

postulate -- TODO-1: Implement getValidProposer
  getValidProposer : ProposerElection → Round → Author

isValidProposerM : Author → Round → LBFT Bool
isValidProposer : ProposerElection → Author → Round → Bool

isValidProposalM : Block → LBFT (Either ObmNotValidProposerReason Unit)
isValidProposalM b =
  maybeSD (b ^∙ bAuthor) (bail ProposalDoesNotHaveAnAuthor) $ λ a → do
    -- IMPL-DIFF: `ifM` in Haskell means something else
    vp ← isValidProposerM a (b ^∙ bRound)
    ifD vp
      then ok unit
      else bail ProposerForBlockIsNotValidForThisRound

isValidProposerM a r = isValidProposer <$> use lProposerElection <*> pure a <*> pure r

isValidProposer pe a r = getValidProposer pe r == a


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

module Pi0Cat where

-- Proving that Pi at level 0 symmetric rig groupoid

open import Level using () renaming (zero to lzero)
open import Data.Unit using (tt)
open import Data.Product using (_,_)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Monoidal.Braided using (Braided)
open import Categories.Monoidal.Symmetric using (Symmetric)
open import Categories.RigCategory
  using (RigCategory; module BimonoidalHelperFunctors)

open import PiU using (U; PLUS; ZERO; TIMES; ONE)
open import PiLevel0 using (_⟷_; !; triv≡; triv≡Equiv;
  id⟷; _◎_;
  _⊕_; unite₊l; uniti₊l; unite₊r; uniti₊r; swap₊; assocr₊; assocl₊;
  _⊗_; unite⋆l; uniti⋆l; unite⋆r; uniti⋆r; swap⋆; assocr⋆; assocl⋆;
  absorbl; absorbr; factorzl; factorzr;
  dist; factor; distl; factorl)

------------------------------------------------------------------------------
-- It is a category...

PiCat : Category lzero lzero lzero
PiCat = record
  { Obj = U
  ; _⇒_ = _⟷_
  ; _≡_ = triv≡
  ; id = id⟷
  ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
  ; assoc = tt
  ; identityˡ = tt
  ; identityʳ = tt
  ; equiv = triv≡Equiv
  ; ∘-resp-≡ = λ _ _ → tt
  }

-- and a groupoid

PiGroupoid : Groupoid PiCat
PiGroupoid = record
  { _⁻¹ = !
  ; iso = record { isoˡ = tt ; isoʳ = tt }
  }

-- additive bifunctor and monoidal structure

⊕-bifunctor : Bifunctor PiCat PiCat PiCat
⊕-bifunctor = record
  { F₀ = λ {(u , v) → PLUS u v}
  ; F₁ = λ {(x⟷y , z⟷w) → x⟷y ⊕ z⟷w }
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

module ⊎h = MonoidalHelperFunctors PiCat ⊕-bifunctor ZERO

0⊕x≡x : NaturalIsomorphism ⊎h.id⊗x ⊎h.x
0⊕x≡x = record
  { F⇒G = record
    { η = λ X → unite₊l
    ; commute = λ _ → tt }
  ; F⇐G = record
    { η = λ X → uniti₊l
    ; commute = λ _ → tt }
  ; iso = λ X → record { isoˡ = tt; isoʳ = tt }
  }

x⊕0≡x : NaturalIsomorphism ⊎h.x⊗id ⊎h.x
x⊕0≡x = record
  { F⇒G = record
    { η = λ X → unite₊r
    ; commute = λ _ → tt
    }
  ; F⇐G = record
    { η = λ X → uniti₊r
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

[x⊕y]⊕z≡x⊕[y⊕z] : NaturalIsomorphism ⊎h.[x⊗y]⊗z ⊎h.x⊗[y⊗z]
[x⊕y]⊕z≡x⊕[y⊕z] = record
  { F⇒G = record
    { η = λ X → assocr₊
    ; commute = λ f → tt
    }
  ; F⇐G = record
    { η = λ X → assocl₊
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

M⊕ : Monoidal PiCat
M⊕ = record
  { ⊗ = ⊕-bifunctor
  ; id = ZERO
  ; identityˡ = 0⊕x≡x
  ; identityʳ = x⊕0≡x
  ; assoc = [x⊕y]⊕z≡x⊕[y⊕z]
  ; triangle = tt
  ; pentagon = tt
  }

-- multiplicative bifunctor and monoidal structure

⊗-bifunctor : Bifunctor PiCat PiCat PiCat
⊗-bifunctor =  record
  { F₀ = λ {(u , v) → TIMES u v}
  ; F₁ = λ {(x⟷y , z⟷w) → x⟷y ⊗ z⟷w }
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

module ⊗h = MonoidalHelperFunctors PiCat ⊗-bifunctor ONE

1⊗x≡x : NaturalIsomorphism ⊗h.id⊗x ⊗h.x
1⊗x≡x = record
  { F⇒G = record
    { η = λ X → unite⋆l
    ; commute = λ _ → tt }
  ; F⇐G = record
    { η = λ X → uniti⋆l
    ; commute = λ _ → tt }
  ; iso = λ X → record { isoˡ = tt; isoʳ = tt }
  }

x⊗1≡x : NaturalIsomorphism ⊗h.x⊗id ⊗h.x
x⊗1≡x = record
  { F⇒G = record
    { η = λ X → unite⋆r
    ; commute = λ _ → tt
    }
  ; F⇐G = record
    { η = λ X → uniti⋆r
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

[x⊗y]⊗z≡x⊗[y⊗z] : NaturalIsomorphism ⊗h.[x⊗y]⊗z ⊗h.x⊗[y⊗z]
[x⊗y]⊗z≡x⊗[y⊗z] = record
  { F⇒G = record
    { η = λ X → assocr⋆
    ; commute = λ f → tt
    }
  ; F⇐G = record
    { η = λ X → assocl⋆
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

M⊗ : Monoidal PiCat
M⊗ = record
  { ⊗ = ⊗-bifunctor
  ; id = ONE
  ; identityˡ = 1⊗x≡x
  ; identityʳ = x⊗1≡x
  ; assoc = [x⊗y]⊗z≡x⊗[y⊗z]
  ; triangle = tt
  ; pentagon = tt
  }

x⊕y≡y⊕x : NaturalIsomorphism ⊎h.x⊗y ⊎h.y⊗x
x⊕y≡y⊕x = record
  { F⇒G = record { η = λ X → swap₊ ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → swap₊ ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt } }

BM⊕ : Braided M⊕
BM⊕ = record { braid = x⊕y≡y⊕x ; unit-coh = tt; hexagon₁ = tt ; hexagon₂ = tt }

x⊗y≡y⊗x : NaturalIsomorphism ⊗h.x⊗y ⊗h.y⊗x
x⊗y≡y⊗x = record
  { F⇒G = record { η = λ X → swap⋆ ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → swap⋆ ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt } }

BM⊗ : Braided M⊗
BM⊗ = record { braid = x⊗y≡y⊗x ; unit-coh = tt; hexagon₁ = tt ; hexagon₂ = tt }

SBM⊕ : Symmetric BM⊕
SBM⊕ = record { symmetry = tt }

SBM⊗ : Symmetric BM⊗
SBM⊗ = record { symmetry = tt }

module r = BimonoidalHelperFunctors BM⊕ BM⊗

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record { η = λ X → absorbl ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factorzr ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record { η = λ X → absorbr ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factorzl ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record -- this probably says we need distl/distr
  { F⇒G = record { η = λ X → distl ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factorl ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record { η = λ X → dist ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factor ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

Pi0Rig : RigCategory SBM⊕ SBM⊗
Pi0Rig = record
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = 0⊗x≡0
  ; annᵣ = x⊗0≡0
  ; laplazaI = tt
  ; laplazaII = tt
  ; laplazaIV = tt
  ; laplazaVI = tt
  ; laplazaIX = tt
  ; laplazaX = tt
  ; laplazaXI = tt
  ; laplazaXIII = tt
  ; laplazaXV = tt
  ; laplazaXVI = tt
  ; laplazaXVII = tt
  ; laplazaXIX = tt
  ; laplazaXXIII = tt
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Coinduction using ( ∞ ; ♭ ; ♯_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; _≢_ ; refl )
open import Relation.Nullary using ( Dec ; yes ; no )
open import System.IO.Transducers.Session using ( Session ; I ; Σ ; Γ ; _/_ ; IsI )

module System.IO.Transducers.Trace where

infixr 4 _≤_ _⊑_ _⊨_⊑_ _⊨_✓ _✓
infixr 5 _∷_ _++_

-- The semantics of a session is its set of traces.
-- The name "trace" comes from process algebra,
-- it's called a play in games semantics, or a word of an automaton.

data Trace (S : Session) : Set where
  [] : Trace S
  _∷_ : (a : Γ S) (as : Trace (S / a)) → (Trace S)

-- Traces ending in [] at type I are completed traces

data _⊨_✓ : ∀ S → (Trace S) → Set₁ where
  [] : I ⊨ [] ✓
  _∷_ : ∀ {S} a {as} → (S / a ⊨ as ✓) → (S ⊨ a ∷ as ✓)

_✓ : ∀ {S} → (Trace S) → Set₁
_✓ {S} as = S ⊨ as ✓

-- Prefix order on traces

data _⊨_⊑_ : ∀ S → (Trace S) → (Trace S) → Set₁ where
  [] : ∀ {S as} → (S ⊨ [] ⊑ as)
  _∷_ : ∀ {S} a {as bs} → (S / a ⊨ as ⊑ bs) → (S ⊨ a ∷ as ⊑ a ∷ bs)

_⊑_ : ∀ {S} → (Trace S) → (Trace S) → Set₁
_⊑_ {S} as bs = S ⊨ as ⊑ bs

-- For building buffers, it is useful to provide
-- snoc traces as well as cons traces.

data _≤_ : Session → Session → Set₁ where
  [] : ∀ {S} → (S ≤ S)
  _∷_ : ∀ {S T} a (as : S ≤ T) → (S / a ≤ T)

-- Snoc traces form categories, where composition is concatenation.

_++_ : ∀ {S T U} → (S ≤ T) → (T ≤ U) → (S ≤ U)
[]       ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

-- snoc traces can be reversed to form cons traces

revApp : ∀ {S T} → (S ≤ T) → (Trace S) → (Trace T)
revApp []       bs = bs
revApp (a ∷ as) bs = revApp as (a ∷ bs)

reverse : ∀ {S T} → (S ≤ T) → (Trace T)
reverse as = revApp as []

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

{- Definition of SubCategory of a given Category C.

  Here a SubCategory is defined via
  - an index set I
  - a mapping I → Obj (not necessarily injective)
  - a proof (as a unary relation) that for all a, b : A, all arrows U a ⇒ U b belong to the SubCategory
    (note that this is 'backwards' from SubCategory at https://ncatlab.org/nlab/show/subcategory
     which would be
     (∀ {x y : Obj} (f : x ⇒ y) → R f → ∃ (A × B) (λ (a , b) → U a × U b))
     and that would be awkward to work with.
  - a proof that all objects pointed to by I have identity arrows that belong
  - a proof that composable arrows in the SubCategory are closed under composition

  It is simpler to package up all of that into a single record.
-}
module Categories.Category.SubCategory {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning using (refl; sym; trans)

open import Level
open import Data.Product

private
  variable
    i : Level

record SubCat {ℓ′} (I : Set i) : Set (o ⊔ ℓ ⊔ i ⊔ suc ℓ′) where
  field
    U : I → Obj
    R : {a b : I} → U a ⇒ U b → Set ℓ′
    Rid : {a : I} → R (id {U a})
    _∘R_ : {a b c : I} {f : U b ⇒ U c} {g : U a ⇒ U b} → R f → R g → R (f ∘ g)

SubCategory : {ℓ′ : Level} {I : Set i} → SubCat {ℓ′ = ℓ′} I → Category _ _ _
SubCategory {I = I} sc = let open SubCat sc in record
  { Obj       = I
  ; _⇒_       = λ a b → Σ (U a ⇒ U b) R
  ; _≈_       = λ f g → proj₁ f ≈ proj₁ g
  ; id        = id , Rid
  ; _∘_       = zip _∘_ _∘R_
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record -- need to expand this out, else the levels don't work out
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }

FullSubCategory : ∀ {I : Set i} → (U : I → Obj) → Category _ _ _
FullSubCategory {I = I} U = record
  { Obj       = I
  ; _⇒_       = λ x y → U x ⇒ U y
  ; _≈_       = _≈_
  ; id        = id
  ; _∘_       = _∘_
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; 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:
import Structure.Logic.Classical.NaturalDeduction

module Structure.Logic.Classical.SetTheory.Relation {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

open import Syntax.Function
open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic ⦄ (_∈_)

UnaryRelator : Set(_)
UnaryRelator = (Domain → Formula)

BinaryRelator : Set(_)
BinaryRelator = (Domain → Domain → Formula)

-- Containment
-- (a ∋ x) means that the set a contains the set x.
_∋_ : BinaryRelator
_∋_ a x = (x ∈ a)

-- Non-containment
_∌_ : BinaryRelator
_∌_ a x = ¬(x ∈ a)

-- Not element of
_∉_ : BinaryRelator
_∉_ x a = ¬(x ∈ a)

-- Subset of
_⊆_ : BinaryRelator
_⊆_ a b = ∀ₗ(x ↦ (x ∈ a) ⟶ (x ∈ b))

-- Superset of
_⊇_ : BinaryRelator
_⊇_ a b = ∀ₗ(x ↦ (x ∈ a) ⟵ (x ∈ b))

-- Equality of
_≡ₛ_ : BinaryRelator
_≡ₛ_ a b = ∀ₗ(x ↦ (x ∈ a) ⟷ (x ∈ b))

-- The statement that the set s is empty
Empty : UnaryRelator
Empty(s) = ∀ₗ(x ↦ ¬(x ∈ s))

-- The statement that the set s is non-empty
NonEmpty : UnaryRelator
NonEmpty(s) = ∃ₗ(x ↦ (x ∈ s))

-- The statement that the set s is a set that contains all sets
Universal : UnaryRelator
Universal(s) = ∀ₗ(x ↦ (x ∈ s))

-- The statement that the sets s₁ and s₂ are disjoint
Disjoint : BinaryRelator
Disjoint(s₁)(s₂) = ∀ₗ(x ↦ ¬((x ∈ s₁)∧(x ∈ s₂)))
-- ¬ ∃ₗ(x ↦ (x ∈ s₁)∧(x ∈ s₂))

-- The statement that the sets in ss are all pairwise disjoint
PairwiseDisjoint : UnaryRelator
PairwiseDisjoint(ss) = ∀ₛ(ss)(s₁ ↦ ∀ₛ(ss)(s₂ ↦ ∀ₗ(x ↦ (x ∈ s₁)∧(x ∈ s₂) ⟶ (s₁ ≡ s₂))))
-- ∀ₛ(ss)(s₁ ↦ ∀ₛ(ss)(s₂ ↦ (s₁ ≢ s₂) → Disjoint(s₁)(s₂)))

-- The statement that the relation predicate F can be interpreted as a partial function
PartialFunction : BinaryRelator → Domain → Formula
PartialFunction(F) (dom) = ∀ₛ(dom)(x ↦ Unique(y ↦ F(x)(y)))

-- The statement that the relation predicate F can be interpreted as a total function
TotalFunction : BinaryRelator → Domain → Formula
TotalFunction(F) (dom) = ∀ₛ(dom)(x ↦ ∃ₗ!(y ↦ F(x)(y)))

-- A binary relator modifier which makes the binary relator to a statement about all distinct pairs in a set.
-- Note: This is specifically for irreflexive binary relations.
Pairwise : BinaryRelator → UnaryRelator
Pairwise Related (S) = ∀ₛ(S)(a ↦ ∀ₛ(S)(b ↦ (a ≢ b) ⟶ Related(a)(b)))

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 --sized-types #-}

module FormalLanguage.Equals{ℓ} where

import      Lvl
open import FormalLanguage
open import Lang.Size
open import Logic.Propositional
open import Relator.Equals using ([≡]-intro) renaming (_≡_ to _≡ₑ_)
open import Relator.Equals.Proofs
import      Structure.Relator.Names as Names
open import Structure.Setoid
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type

private variable s : Size

module _ {Σ : Alphabet{ℓ}} where
  record _≅[_]≅_ (A : Language(Σ){∞ˢⁱᶻᵉ}) (s : Size) (B : Language(Σ){∞ˢⁱᶻᵉ}) : Type{ℓ} where
    constructor intro
    coinductive
    field
      accepts-ε   : Language.accepts-ε(A) ≡ₑ Language.accepts-ε(B)
      suffix-lang : ∀{c : Σ}{sₛ : <ˢⁱᶻᵉ s} → (Language.suffix-lang A c ≅[ sₛ ]≅ Language.suffix-lang B c)

  _≅_ : ∀{s : Size} → Language(Σ){∞ˢⁱᶻᵉ} → Language(Σ){∞ˢⁱᶻᵉ} → Type
  _≅_ {s} = _≅[ s ]≅_

  [≅]-reflexivity-raw : Names.Reflexivity(_≅[ s ]≅_)
  _≅[_]≅_.accepts-ε   ([≅]-reflexivity-raw) = [≡]-intro
  _≅[_]≅_.suffix-lang ([≅]-reflexivity-raw) = [≅]-reflexivity-raw

  [≅]-symmetry-raw : Names.Symmetry(_≅[ s ]≅_)
  _≅[_]≅_.accepts-ε   ([≅]-symmetry-raw ab) = symmetry(_≡ₑ_) (_≅[_]≅_.accepts-ε ab)
  _≅[_]≅_.suffix-lang ([≅]-symmetry-raw ab) = [≅]-symmetry-raw (_≅[_]≅_.suffix-lang ab)

  [≅]-transitivity-raw : Names.Transitivity(_≅[ s ]≅_)
  _≅[_]≅_.accepts-ε   ([≅]-transitivity-raw ab bc) = transitivity(_≡ₑ_) (_≅[_]≅_.accepts-ε ab) (_≅[_]≅_.accepts-ε bc)
  _≅[_]≅_.suffix-lang ([≅]-transitivity-raw ab bc) = [≅]-transitivity-raw (_≅[_]≅_.suffix-lang ab) (_≅[_]≅_.suffix-lang bc)

  instance
    [≅]-reflexivity : Reflexivity(_≅[ s ]≅_)
    Reflexivity.proof([≅]-reflexivity) = [≅]-reflexivity-raw

  instance
    [≅]-symmetry : Symmetry(_≅[ s ]≅_)
    Symmetry.proof([≅]-symmetry) = [≅]-symmetry-raw

  instance
    [≅]-transitivity : Transitivity(_≅[ s ]≅_)
    Transitivity.proof([≅]-transitivity) = [≅]-transitivity-raw

  instance
    [≅]-equivalence : Equivalence(_≅[ s ]≅_)
    [≅]-equivalence = record{}

  instance
    [≅]-equiv : let _ = s in Equiv(Language(Σ))
    [≅]-equiv {s = s} = intro(_≅[ s ]≅_) ⦃ [≅]-equivalence ⦄


text:
open import Agda.Primitive

module Experimental.Equality where

  data _≡_ {ℓ} {A : Set ℓ} : A → A → Set ℓ where
    refl : ∀ {x : A} → x ≡ x

  sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
  sym refl = refl

  tran : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  tran refl q = q

  ap : ∀ {ℓ k} {A : Set ℓ} {B : Set k} {x y : A} {f : A → B} → x ≡ y → f x ≡ f y
  ap refl = refl

  transport : ∀ {ℓ k} {A : Set ℓ} (B : A → Set k) {x y : A} → x ≡ y → B x → B y
  transport _ refl u = u

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module Generic.Test.Data.Maybe where

open import Generic.Main as Main hiding (Maybe; just; nothing)

Maybe : ∀ {α} -> Set α -> Set α
Maybe = readData Main.Maybe

pattern nothing = #₀ lrefl
pattern just x  = !#₁ (relv x , lrefl)

just′ : ∀ {α} {A : Set α} -> A -> Maybe A
just′ = just

nothing′ : ∀ {α} {A : Set α} -> Maybe A
nothing′ = nothing

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
--
-- Formalize correctness of differentiation for the source calculus in the
-- static caching paper (typed version).
--

module Thesis.ANormal where

open import Thesis.Types public
open import Thesis.Contexts public

open import Relation.Binary.PropositionalEquality

data Term (Γ : Context) (τ : Type) : Set where
  var : (x : Var Γ τ) →
    Term Γ τ
  lett : ∀ {σ τ₁} → (f : Var Γ (σ ⇒ τ₁)) → (x : Var Γ σ) → Term (τ₁ • Γ) τ → Term Γ τ

-- Also represent top-level definitions, so that we can somehow create functions
-- via syntax. Made up on the moment.

-- WARNING: this allows nested lambdas. That's more powerful than allowing only
-- closures whose bodies can't contain lambdas, like in the paper.
data Fun (Γ : Context) : (τ : Type) → Set where
  term : ∀ {τ} → Term Γ τ → Fun Γ τ
  abs : ∀ {σ τ} → Fun (σ • Γ) τ → Fun Γ (σ ⇒ τ)

-- Indeed, caching doesn't work there with Fun. It works on FunR. Eventually
-- should adapt definitions to FunR.
data FunR (Γ : Context) : (τ : Type) → Set where
  cabsterm : ∀ {σ τ} → Term (σ • Γ) τ → FunR Γ (σ ⇒ τ)

open import Thesis.Environments public

⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧Context → ⟦ τ ⟧Type
⟦ var x ⟧Term ρ = ⟦ x ⟧Var ρ
⟦ lett f x t ⟧Term ρ = ⟦ t ⟧Term (⟦ f ⟧Var ρ (⟦ x ⟧Var ρ) • ρ)

⟦_⟧Fun : ∀ {Γ τ} → Fun Γ τ → ⟦ Γ ⟧Context → ⟦ τ ⟧Type
⟦ term t ⟧Fun ρ = ⟦ t ⟧Term ρ
⟦ abs f ⟧Fun ρ = λ v → ⟦ f ⟧Fun (v • ρ)

-- Next steps:
-- 1. Add a functional big-step semantics for this language: DONE.
-- 2. Prove it sound wrt. the denotational semantics: DONE.
-- 3. Add an erasure to a uni-typed language. DONE.
-- 4. Redo 1 with an *untyped* functional big-step semantics.
-- 5. Prove that evaluation and erasure commute:
-- -- erasure-commute-term : ∀ {Γ τ} (t : T.Term Γ τ) ρ n →
-- --   erase-errVal (T.eval-term t ρ n) ≡ eval-term (erase-term t) (erase-env ρ) n
-- 6. Define new caching transformation into untyped language.
--
-- 7. Prove the new transformation correct in the untyped language, by reusing
-- evaluation on the source language.

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

-- The category of group objects with a cartesian category

open import Categories.Category
open import Categories.Category.Cartesian

module Categories.Category.Construction.Groups {o ℓ e} {𝒞 : Category o ℓ e} (C : Cartesian 𝒞) where

open import Level

open import Categories.Category.BinaryProducts 𝒞
open import Categories.Morphism.Reasoning 𝒞
open import Categories.Object.Group C
open import Categories.Object.Product.Morphisms 𝒞

open Category 𝒞
open Cartesian C
open BinaryProducts products
open Equiv
open HomReasoning
open Group using (μ)
open Group⇒

Groups : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
Groups = record
  { Obj = Group
  ; _⇒_ = Group⇒
  ; _≈_ = λ f g → arr f ≈ arr g
  ; id = record
    { arr = id
    ; preserves-μ = identityˡ ○ introʳ (id×id product)
    ; preserves-η = identityˡ
    ; preserves-ι = id-comm-sym
    }
  ; _∘_ = λ f g → record
    { arr = arr f ∘ arr g
    ; preserves-μ = glue (preserves-μ f) (preserves-μ g) ○ ∘-resp-≈ʳ ⁂∘⁂
    ; preserves-η = glueTrianglesˡ (preserves-η f) (preserves-η g)
    ; preserves-ι = glue (preserves-ι f) (preserves-ι g)
    }
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≈ = ∘-resp-≈
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- Parallel reduction in pure type systems (PTS)
------------------------------------------------------------------------

module Pts.Reduction.Parallel where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Relation
open import Data.Star using (Star; ε; _◅_; _◅◅_)
open import Data.Product using (_,_; ∃; _×_)
open import Data.Nat using (ℕ; _+_)
open import Data.Vec.All using (lookup₂)
import Function as Fun
open import Relation.Binary
open import Relation.Binary.EquivalenceClosure using (EqClosure)
open import Relation.Binary.SymmetricClosure using (fwd; bwd)
open import Relation.Binary.Reduction
import Relation.Binary.PropositionalEquality as P

open import Pts.Syntax

-- All remaining submodules are parametrized by a given set of sorts.
module _ {Sort : Set} where
  open Syntax       Sort
  open Substitution Sort using (_[_])

  ----------------------------------------------------------------------
  -- Parallel reduction

  infixl 9 _·_
  infix  5 _⇛_

  -- One-step parallel reduction.
  data _⇛_ {n : ℕ} : Term n → Term n → Set where
    refl : ∀ {a}                                 →       a ⇛ a
    Π    : ∀ {a₁ a₂ b₁ b₂}   → a₁ ⇛ a₂ → b₁ ⇛ b₂ → Π a₁ b₁ ⇛ Π a₂ b₂
    ƛ    : ∀ {a₁ a₂ b₁ b₂}   → a₁ ⇛ a₂ → b₁ ⇛ b₂ → ƛ a₁ b₁ ⇛ ƛ a₂ b₂
    _·_  : ∀ {a₁ a₂ b₁ b₂}   → a₁ ⇛ a₂ → b₁ ⇛ b₂ → a₁ · b₁ ⇛ a₂ · b₂
    cont : ∀ {a b₁ b₂ c₁ c₂} → b₁ ⇛ b₂ → c₁ ⇛ c₂ →
           (ƛ a b₁) · c₁ ⇛ b₂ [ c₂ ]

  reduction : Reduction Term
  reduction = record { _→1_ = _⇛_ }

  -- Parallel reduction and equivalence.
  open Reduction reduction public renaming (_→*_ to _⇛*_; _↔_ to _≡p_)

  ----------------------------------------------------------------------
  -- Simple properties of parallel reduction

  -- Inclusions.
  ⇛⇒⇛*  = →1⇒→* reduction
  ⇛*⇒≡p = →*⇒↔  reduction
  ⇛⇒≡p  = →1⇒↔  reduction

  -- parallel reduction is a preorder.
  ⇛*-predorder = →*-predorder reduction

  -- Terms together with parallel equivalence form a setoid.
  ≡p-setoid = ↔-setoid reduction

  open P using (_≡_)

  -- Shapes are preserved by one-step parallel reduction.

  sort-⇛ : ∀ {n s} {a : Term n} → sort s ⇛ a → sort s ≡ a
  sort-⇛ refl = P.refl

  ƛ-⇛ : ∀ {n} {a : Term n} {b c} → ƛ a b ⇛ c →
        ∃ λ a′ → ∃ λ b′ → a ⇛ a′ × b ⇛ b′ × ƛ a′ b′ ≡ c
  ƛ-⇛ refl          = _ , _ , refl , refl , P.refl
  ƛ-⇛ (ƛ a⇛a′ b⇛b′) = _ , _ , a⇛a′ , b⇛b′ , P.refl

  Π-⇛ : ∀ {n} {a : Term n} {b c} → Π a b ⇛ c →
        ∃ λ a′ → ∃ λ b′ → a ⇛ a′ × b ⇛ b′ × Π a′ b′ ≡ c
  Π-⇛ refl          = _ , _ , refl , refl , P.refl
  Π-⇛ (Π a⇛a′ b⇛b′) = _ , _ , a⇛a′ , b⇛b′ , P.refl

  -- Shapes are preserved by parallel reduction.

  sort-⇛* : ∀ {n s} {a : Term n} → sort s ⇛* a → sort s ≡ a
  sort-⇛* ε             = P.refl
  sort-⇛* (refl ◅ s⇛*b) = sort-⇛* s⇛*b

  ƛ-⇛* : ∀ {n} {a : Term n} {b c} → ƛ a b ⇛* c →
         ∃ λ a′ → ∃ λ b′ → a ⇛* a′ × b ⇛* b′ × ƛ a′ b′ ≡ c
  ƛ-⇛* ε                        = _ , _ , ε , ε , P.refl
  ƛ-⇛* (refl        ◅ λab⇛*d)   = ƛ-⇛* λab⇛*d
  ƛ-⇛* (ƛ a⇛a₁ b⇛b₁ ◅ λa₁b₁⇛*d) =
    let a₂ , b₂ , a₁⇛*a₂ , b₁⇛*b₂ , λa₂b₂≡d = ƛ-⇛* λa₁b₁⇛*d
    in a₂ , b₂ , a⇛a₁ ◅ a₁⇛*a₂ , b⇛b₁ ◅ b₁⇛*b₂ , λa₂b₂≡d

  Π-⇛* : ∀ {n} {a : Term n} {b c} → Π a b ⇛* c →
         ∃ λ a′ → ∃ λ b′ → a ⇛* a′ × b ⇛* b′ × Π a′ b′ ≡ c
  Π-⇛* ε                        = _ , _ , ε , ε , P.refl
  Π-⇛* (refl        ◅ Πab⇛*d)   = Π-⇛* Πab⇛*d
  Π-⇛* (Π a⇛a₁ b⇛b₁ ◅ Πa₁b₁⇛*d) =
    let a₂ , b₂ , a₁⇛*a₂ , b₁⇛*b₂ , Πa₂b₂≡d = Π-⇛* Πa₁b₁⇛*d
    in a₂ , b₂ , a⇛a₁ ◅ a₁⇛*a₂ , b⇛b₁ ◅ b₁⇛*b₂ , Πa₂b₂≡d

  ----------------------------------------------------------------------
  -- Substitutions lifted to parallel reduction
  --
  -- The application _/⇛_ below may be considered a substitution
  -- lemma, i.e. it establishes that substitutions of terms preserve
  -- parallel reduction:
  --
  --                                ⇛
  --                           a ------→ b
  --                           |         |
  --                       -/σ |         | -/σ
  --                           ↓    ⇛    ↓
  --                          a/σ ····→ b/σ
  --
  -- ∀ (a b : Term n) (σ : Sub Term m n).

  -- Application of generic substitutions lifted to reduction.
  record ParSubstApp {T₁ T₂} (R : TermRel T₁ T₂)
                     (l₁ : Lift T₁ Term) (l₂ : Lift T₂ Term)
                     (rl : RelLift R _⇛_ l₁ l₂) : Set where
    infix  10 _↑₂
    infixl 8  _/₁_ _/₂_ _/_ _/⇛_

    open Substitution Sort using (termSubst)
    private
      _/₁_ = TermSubst.app termSubst l₁
      _/₂_ = TermSubst.app termSubst l₂
      _↑₂  = Lift._↑ l₂
    open LiftTermRel T₁ T₂ using (_⟨_⟩_)
    open RelLift rl
    open P using (sym; subst)

    -- T₂-substitutions commute.
    field /₂-sub-↑ : ∀ {m n b} {σ : Sub T₂ m n} a →
                     (a [ b ]) /₂ σ ≡ (a /₂ (σ ↑₂)) [ b /₂ σ ]

    _/_ : ∀ {m n} {σ₁ : Sub T₁ m n} {σ₂ : Sub T₂ m n} →
          ∀ a → σ₁ ⟨ R ⟩ σ₂ → a /₁ σ₁ ⇛ a /₂ σ₂
    var x   / σ₁∼σ₂ = lift (lookup₂ x σ₁∼σ₂)
    sort s  / σ₁∼σ₂ = refl
    Π a b   / σ₁∼σ₂ = Π (a / σ₁∼σ₂) (b / σ₁∼σ₂ ↑)
    ƛ a b   / σ₁∼σ₂ = ƛ (a / σ₁∼σ₂) (b / σ₁∼σ₂ ↑)
    (a · b) / σ₁∼σ₂ = (a / σ₁∼σ₂) · (b / σ₁∼σ₂)

    _/⇛_ : ∀ {m n a₁ a₂} {σ₁ : Sub T₁ m n} {σ₂ : Sub T₂ m n} →
           a₁ ⇛ a₂ → σ₁ ⟨ R ⟩ σ₂ → a₁ /₁ σ₁ ⇛ a₂ /₂ σ₂
    refl {a}      /⇛ σ₁∼σ₂ = a / σ₁∼σ₂
    Π a₁⇛a₂ b₁⇛b₂ /⇛ σ₁∼σ₂ = Π (a₁⇛a₂ /⇛ σ₁∼σ₂) (b₁⇛b₂ /⇛ σ₁∼σ₂ ↑)
    ƛ a₁⇛a₂ b₁⇛b₂ /⇛ σ₁∼σ₂ = ƛ (a₁⇛a₂ /⇛ σ₁∼σ₂) (b₁⇛b₂ /⇛ σ₁∼σ₂ ↑)
    a₁⇛a₂ · b₁⇛b₂ /⇛ σ₁∼σ₂ = (a₁⇛a₂ /⇛ σ₁∼σ₂) · (b₁⇛b₂ /⇛ σ₁∼σ₂)
    cont {b₂ = b₂} a₁⇛a₂ b₁⇛b₂ /⇛ σ₁∼σ₂ =
      P.subst (_⇛_ _) (sym (/₂-sub-↑ b₂))
                   (cont (a₁⇛a₂ /⇛ σ₁∼σ₂ ↑) (b₁⇛b₂ /⇛ σ₁∼σ₂))

  -- Term substitutions lifted to parallel reduction.
  module ParSubstitution where
    open Substitution Sort using (termSubst; sub-commutes; varLiftSubLemmas)
    open P using (_≡_; refl)
    private
      module S = TermSubst termSubst
      module V = VarEqSubst

    varLift : RelLift _≡_ _⇛_ S.varLift S.varLift
    varLift = record { simple = V.simple; lift = lift }
      where
        lift : ∀ {n} {x₁ x₂ : Fin n} → x₁ ≡ x₂ → S.var x₁ ⇛ S.var x₂
        lift {x₁ = x} refl = refl

    varSubstApp : ParSubstApp _≡_ S.varLift S.varLift varLift
    varSubstApp = record { /₂-sub-↑ = λ a → /-sub-↑ a _ _ }
      where open LiftSubLemmas varLiftSubLemmas

    infix 8 _/Var-⇛_

    _/Var-⇛_ : ∀ {m n a₁ a₂} {σ₁ σ₂ : Sub Fin m n} →
               a₁ ⇛ a₂ → σ₁ V.⟨≡⟩ σ₂ → (a₁ S./Var σ₁) ⇛ (a₂ S./Var σ₂)
    _/Var-⇛_ = ParSubstApp._/⇛_ varSubstApp

    simple : RelSimple _⇛_ S.simple S.simple
    simple = record
      { extension = record { weaken = λ t₁⇛t₂ → t₁⇛t₂ /Var-⇛ V.wk }
      ; var       = λ x → refl {a = var x}
      }

    termLift : RelLift _⇛_ _⇛_ S.termLift S.termLift
    termLift = record { simple = simple; lift = Fun.id }

    termSubstApp : ParSubstApp _⇛_ S.termLift S.termLift termLift
    termSubstApp = record { /₂-sub-↑ = sub-commutes }

    open ParSubstApp termSubstApp public

    subst : RelSubst _⇛_ S.subst S.subst
    subst = record
      { simple      = simple
      ; application = record { _/_ = _/⇛_ }
      }

    open LiftTermRel Term Term public using (_⟨_⟩_)
    open RelSubst subst public hiding (var; simple; _/_)

    infix 10 _[⇛_]

    -- Shorthand for single-variable substitutions lifted to redcution.
    _[⇛_] : ∀ {n} {a₁ : Term (1 + n)} {a₂} {b₁ : Term n} {b₂} →
            a₁ ⇛ a₂ → b₁ ⇛ b₂ → a₁ S./ S.sub b₁ ⇛ a₂ S./ S.sub b₂
    a₁⇛a₂ [⇛ b₁⇛b₂ ] = a₁⇛a₂ /⇛ sub b₁⇛b₂

  open ParSubstitution

  ----------------------------------------------------------------------
  -- Confluence of parallel reduction
  --
  -- Parallel reduction enjoys the single-step diamond property,
  -- i.e. for any pair a ⇛ b₁, a ⇛ b₂ of parallel reductions, there is
  -- a term c, such that
  --
  --                                ⇛
  --                           a ------→ b₂
  --                           |         :
  --                         ⇛ |         : ⇛
  --                           ↓    ⇛    ↓
  --                           b₁ ·····→ c
  --
  -- commutes.  Confluence (aka the Church-Rosser property) then
  -- follows by pasting of diagrams.

  infixl 4 _⋄_

  -- Diamond property of one-step reduction.
  _⋄_ : ∀ {n} {a b₁ b₂ : Term n} → a ⇛ b₁ → a ⇛ b₂ → ∃ λ c → b₁ ⇛ c × b₂ ⇛ c
  refl ⋄ a⇛b  = _ , a⇛b  , refl
  a⇛b  ⋄ refl = _ , refl , a⇛b
  Π a₁⇛b₁₁ a₂⇛b₁₂ ⋄ Π a₁⇛b₂₁ a₂⇛b₂₂ =
    let c₁ , b₁₁⇛c₁ , b₂₁⇛c₁ = a₁⇛b₁₁ ⋄ a₁⇛b₂₁
        c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in Π c₁ c₂ , Π b₁₁⇛c₁ b₁₂⇛c₂ , Π b₂₁⇛c₁ b₂₂⇛c₂
  ƛ a₁⇛b₁₁ a₂⇛b₁₂ ⋄ ƛ a₁⇛b₂₁ a₂⇛b₂₂ =
    let c₁ , b₁₁⇛c₁ , b₂₁⇛c₁ = a₁⇛b₁₁ ⋄ a₁⇛b₂₁
        c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in ƛ c₁ c₂ , ƛ b₁₁⇛c₁ b₁₂⇛c₂ , ƛ b₂₁⇛c₁ b₂₂⇛c₂
  a₁⇛b₁₁ · a₂⇛b₁₂ ⋄ a₁⇛b₂₁ · a₂⇛b₂₂ =
    let c₁ , b₁₁⇛c₁ , b₂₁⇛c₁ = a₁⇛b₁₁ ⋄ a₁⇛b₂₁
        c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in c₁ · c₂ , b₁₁⇛c₁ · b₁₂⇛c₂ , b₂₁⇛c₁ · b₂₂⇛c₂
  refl · a₂⇛b₁₂ ⋄ cont {b₂ = b₂₁} a₁⇛b₂₁ a₂⇛b₂₂ =
    let c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in b₂₁ [ c₂ ] , cont a₁⇛b₂₁ b₁₂⇛c₂ , refl {a = b₂₁} [⇛ b₂₂⇛c₂ ]
  ƛ _ a₁⇛b₁₁ · a₂⇛b₁₂ ⋄ cont a₁⇛b₂₁ a₂⇛b₂₂ =
    let c₁ , b₁₁⇛c₁ , b₂₁⇛c₁ = a₁⇛b₁₁ ⋄ a₁⇛b₂₁
        c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in c₁ [ c₂ ] , cont b₁₁⇛c₁ b₁₂⇛c₂ , b₂₁⇛c₁ [⇛ b₂₂⇛c₂ ]
  cont {b₂ = b₁₁} a₁⇛b₁₁ a₂⇛b₁₂ ⋄ refl · a₂⇛b₂₂ =
    let c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in b₁₁ [ c₂ ] , refl {a = b₁₁} [⇛ b₁₂⇛c₂ ] , cont a₁⇛b₁₁ b₂₂⇛c₂
  cont a₁⇛b₁₁ a₂⇛b₁₂ ⋄ ƛ _ a₁⇛b₂₁ · a₂⇛b₂₂ =
    let c₁ , b₁₁⇛c₁ , b₂₁⇛c₁ = a₁⇛b₁₁ ⋄ a₁⇛b₂₁
        c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in c₁ [ c₂ ] , b₁₁⇛c₁ [⇛ b₁₂⇛c₂ ] , cont b₂₁⇛c₁ b₂₂⇛c₂
  cont a₁⇛b₁₁ a₂⇛b₁₂ ⋄ cont a₁⇛b₂₁ a₂⇛b₂₂ =
    let c₁ , b₁₁⇛c₁ , b₂₁⇛c₁ = a₁⇛b₁₁ ⋄ a₁⇛b₂₁
        c₂ , b₁₂⇛c₂ , b₂₂⇛c₂ = a₂⇛b₁₂ ⋄ a₂⇛b₂₂
    in c₁ [ c₂ ] , b₁₁⇛c₁ [⇛ b₁₂⇛c₂ ] , b₂₁⇛c₁ [⇛ b₂₂⇛c₂ ]

  -- A strip lemma.
  _⋄′_ : ∀ {n} {a b₁ b₂ : Term n} →
         a ⇛ b₁ → a ⇛* b₂ → ∃ λ c → b₁ ⇛* c × b₂ ⇛ c
  a⇛b  ⋄′ ε               = _ , ε , a⇛b
  a⇛b₁ ⋄′ (a⇛b₂ ◅ b₂⇛*c₂) =
    let c₁ , b₁⇛c₁ , b₂⇛c₁ = a⇛b₁ ⋄ a⇛b₂
        d  , c₁⇛*d , c₂⇛d  = b₂⇛c₁ ⋄′ b₂⇛*c₂
    in d , b₁⇛c₁ ◅ c₁⇛*d , c₂⇛d

  -- Confluence (aka the Church-Rosser property) of _⇛*_
  _⋄*_ : ∀ {n} {a b₁ b₂ : Term n} →
         a ⇛* b₁ → a ⇛* b₂ → ∃ λ c → b₁ ⇛* c × b₂ ⇛* c
  ε               ⋄* a⇛*b  = _ , a⇛*b , ε
  (a⇛b₁ ◅ b₁⇛*c₁) ⋄* a⇛*b₂ =
    let c₂ , b₁⇛*c₂ , b₂⇛c₂ = a⇛b₁ ⋄′ a⇛*b₂
        d  , c₁⇛*d  , c₂⇛*d = b₁⇛*c₁ ⋄* b₁⇛*c₂
    in d , c₁⇛*d , b₂⇛c₂ ◅ c₂⇛*d

  -- Factorization of equivalence into parallel reductions.
  ≡p⇒⇛* : ∀ {n} {a b : Term n} → a ≡p b → ∃ λ c → a ⇛* c × b ⇛* c
  ≡p⇒⇛* ε               = _ , ε , ε
  ≡p⇒⇛* (fwd a⇛b ◅ b≡c) =
    let d , b⇛*d , c⇛*d = ≡p⇒⇛* b≡c in d , a⇛b ◅ b⇛*d , c⇛*d
  ≡p⇒⇛* (bwd a⇚b ◅ b≡c) =
    let d , b⇛*d , c⇛*d = ≡p⇒⇛* b≡c
        e , a⇛*e , d⇛e  = a⇚b ⋄′ b⇛*d
    in e , a⇛*e , c⇛*d ◅◅ (d⇛e ◅ ε)

  -- Π-injectivity (with respect to ≡p).
  Π-inj : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} → Π a₁ b₁ ≡p Π a₂ b₂ →
          a₁ ≡p a₂ × b₁ ≡p b₂
  Π-inj Πa₁b₁≡Πa₂b₂ with ≡p⇒⇛* Πa₁b₁≡Πa₂b₂
  Π-inj Πa₁b₁≡Πa₂b₂ | c , Πa₁b₁⇛*c , Πa₂b₂⇛*c with
    Π-⇛* Πa₁b₁⇛*c | Π-⇛* Πa₂b₂⇛*c
  Π-inj Πa₁b₁≡Πa₂b₂ | Π a₃ b₃ , Πa₁b₁⇛*c , Πa₂b₂⇛*c |
    ._ , ._ , a₁⇛*a₃ , b₁⇛*b₃ , P.refl | ._ , ._ , a₂⇛*a₃ , b₂⇛*b₃ , P.refl =
    ⇛*⇒≡p a₁⇛*a₃ ◅◅ sym (⇛*⇒≡p a₂⇛*a₃) , ⇛*⇒≡p b₁⇛*b₃ ◅◅ sym (⇛*⇒≡p b₂⇛*b₃)
    where
      module ParSetoid {n} where
        open Setoid (≡p-setoid {n}) public
      open ParSetoid

  -- Parallel equivalence on sorts implies syntactic equivalence.
  sort-≡p : ∀ {n s₁ s₂} → sort {n} s₁ ≡p sort s₂ → s₁ ≡ s₂
  sort-≡p s₁≡s₂ with ≡p⇒⇛* s₁≡s₂
  sort-≡p s₁≡s₂ | c , s₁⇛*c , s₂⇛*c with sort-⇛* s₁⇛*c | sort-⇛* s₂⇛*c
  sort-≡p s₁≡s₂ | ._ , s₁⇛*c , s₂⇛*c | P.refl | P.refl = P.refl

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
------------------------------------------------------------------------
-- Safe modules that use --with-K
------------------------------------------------------------------------

{-# OPTIONS --safe --with-K #-}

module README.Safe.With-K where

-- Some theory of Erased, developed using the K rule and propositional
-- equality.

import Erased.With-K

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- Full β-reduction in pure type systems (PTS)
------------------------------------------------------------------------

module Pts.Reduction.Full where

open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Star using (ε; _◅_; map; gmap; _⋆)
open import Data.Sum using ([_,_])
open import Data.Product using (_,_; ∃; _×_)
open import Function using (_∘_)
open import Relation.Binary
import Relation.Binary.EquivalenceClosure as EqClos
import Relation.Binary.PropositionalEquality as P
import Relation.Binary.SymmetricClosure as SymClos
open import Relation.Binary.Reduction
import Function.Equivalence as Equiv

open import Pts.Syntax
open import Pts.Reduction.Parallel as Par hiding (reduction; _⋄*_; Π-inj)

-- All remaining submodules are parametrized by a given set of sorts.
module _ {Sort : Set} where

  open Syntax       Sort
  open Substitution Sort using (_[_])

  ----------------------------------------------------------------------
  -- Full β-reduction and equivalence relations

  infixl 9  _·₁_ _·₂_
  infix  5  _→β_

  -- One-step β-reduction.
  data _→β_ {n} : Term n → Term n → Set where
    cont : ∀ a b c                    → (ƛ a b) · c →β b [ c ]
    Π₁   : ∀ {a₁ a₂} → a₁ →β a₂ → ∀ b →      Π a₁ b →β Π a₂ b
    Π₂   : ∀ {b₁ b₂} a → b₁ →β b₂     →      Π a b₁ →β Π a b₂
    ƛ₁   : ∀ {a₁ a₂} → a₁ →β a₂ → ∀ b →      ƛ a₁ b →β ƛ a₂ b
    ƛ₂   : ∀ {b₁ b₂} a → b₁ →β b₂     →      ƛ a b₁ →β ƛ a b₂
    _·₁_ : ∀ {a₁ a₂} → a₁ →β a₂ → ∀ b →      a₁ · b →β a₂ · b
    _·₂_ : ∀ {b₁ b₂} a → b₁ →β b₂     →      a · b₁ →β a · b₂

  reduction : Reduction Term
  reduction = record { _→1_ = _→β_ }

  -- Full beta reduction and equivalence.
  open Reduction reduction public renaming (_→*_ to _→β*_; _↔_ to _≡β_)

  ----------------------------------------------------------------------
  -- Substitutions in full β-reductions/equivalence
  --
  -- The applications _/→β_, _/→β*_ and _/≡β_ below may be considered
  -- substitution lemmas, i.e. they establish the commutativity of the
  -- respective reductions/equivalence with substitutions.

  -- Application of generic substitutions to the
  -- reductions/equivalence.
  record BetaSubstApp {T} (l : Lift T Term) : Set where
    open Lift l
    open SubstApp Sort l
    open P hiding ([_])

    -- Substitutions commute.
    field /-sub-↑ : ∀ {m n} a b (σ : Sub T m n) →
                    a [ b ] / σ ≡ (a / σ ↑) [ b / σ ]

    infixl 8 _/→β_

    -- Substitution commutes with one-step β-reduction.
    _/→β_ : ∀ {m n a b} → a →β b → (σ : Sub T m n) → a / σ →β b / σ
    cont a b c /→β σ =
      subst (_→β_ _) (sym (/-sub-↑ b c σ)) (cont (a / σ) (b / σ ↑) (c / σ))
    Π₁ a₁→a₂ b /→β σ = Π₁ (a₁→a₂ /→β σ) (b / σ ↑)
    Π₂ a b₁→b₂ /→β σ = Π₂ (a / σ) (b₁→b₂ /→β σ ↑)
    ƛ₁ a₁→a₂ b /→β σ = ƛ₁ (a₁→a₂ /→β σ) (b / σ ↑)
    ƛ₂ a b₁→b₂ /→β σ = ƛ₂ (a / σ) (b₁→b₂ /→β σ ↑)
    a₁→a₂ ·₁ b /→β σ = (a₁→a₂ /→β σ) ·₁ (b / σ)
    a ·₂ b₁→b₂ /→β σ = (a / σ) ·₂ (b₁→b₂ /→β σ)

    redSubstApp : RedSubstApp reduction (record { _/_ = _/_ })
    redSubstApp = record { _/→1_ = _/→β_ }

    open RedSubstApp redSubstApp public
      hiding (_/→1_) renaming (_/→*_ to _/→β*_; _/↔_ to _/≡β_)

  -- Term substitutions in reductions/equivalences.
  module BetaSubstitution where
    open Substitution Sort
      using (termSubst; weaken; sub-commutes; varLiftSubLemmas)

    -- Application of renamings to reductions/equivalences.
    varSubstApp : BetaSubstApp (TermSubst.varLift termSubst)
    varSubstApp = record { /-sub-↑ = /-sub-↑ }
      where open LiftSubLemmas varLiftSubLemmas
    private module V = BetaSubstApp varSubstApp

    -- Weakening of one-step β-reductions.
    weaken-→β : ∀ {n} {a b : Term n} → a →β b → weaken a →β weaken b
    weaken-→β a→b = a→b V./→β VarSubst.wk

    -- Weakening of β-reductions.
    weaken-→β* : ∀ {n} {a b : Term n} → a →β* b → weaken a →β* weaken b
    weaken-→β* = gmap weaken weaken-→β

    -- Weakening of β-equivalences.
    weaken-≡β : ∀ {n} {a b : Term n} → a ≡β b → weaken a ≡β weaken b
    weaken-≡β = EqClos.gmap weaken weaken-→β

    -- Application of term substitutions to reductions/equivalences.
    termSubstApp : BetaSubstApp (TermSubst.termLift termSubst)
    termSubstApp = record { /-sub-↑ = λ a _ _ → sub-commutes a }
    open BetaSubstApp termSubstApp public

  ----------------------------------------------------------------------
  -- Simple properties of the β-reductions/equivalence

  -- Inclusions.
  →β⇒→β* = →1⇒→* reduction
  →β*⇒≡β = →*⇒↔  reduction
  →β⇒≡β  = →1⇒↔  reduction

  -- β-reduction is a preorder.
  →β*-predorder = →*-predorder reduction

  -- Preorder reasoning for β-reduction.
  module →β*-Reasoning = →*-Reasoning reduction

  -- Terms together with β-equivalence form a setoid.
  ≡β-setoid = ↔-setoid reduction

  -- Equational reasoning for β-equivalence.
  module ≡β-Reasoning = ↔-Reasoning reduction

  ----------------------------------------------------------------------
  -- Relationships between β-reduction and parallel reduction

  -- One-step β-reduction implies one-step parallel reduction.
  →β⇒⇛ : ∀ {n} {a b : Term n} → a →β b → a ⇛ b
  →β⇒⇛ (cont a b c) = cont refl refl
  →β⇒⇛ (Π₁ a₁→a₂ b) = Π (→β⇒⇛ a₁→a₂) refl
  →β⇒⇛ (Π₂ a b₁→b₂) = Π refl (→β⇒⇛ b₁→b₂)
  →β⇒⇛ (ƛ₁ a₁→a₂ b) = ƛ (→β⇒⇛ a₁→a₂) refl
  →β⇒⇛ (ƛ₂ a b₁→b₂) = ƛ refl (→β⇒⇛ b₁→b₂)
  →β⇒⇛ (a₁→a₂ ·₁ b) = →β⇒⇛ a₁→a₂ · refl
  →β⇒⇛ (a ·₂ b₁→b₂) = refl · →β⇒⇛ b₁→b₂

  -- β-reduction implies parallel reduction.
  →β*⇒⇛* : ∀ {n} {a b : Term n} → a →β* b → a ⇛* b
  →β*⇒⇛* = map →β⇒⇛

  -- β-equivalence implies parallel equivalence.
  ≡β⇒≡p : ∀ {n} {a b : Term n} → a ≡β b → a ≡p b
  ≡β⇒≡p = EqClos.map →β⇒⇛

  open →*-Reasoning reduction

  -- One-step parallel reduction implies β-reduction.
  ⇛⇒→β* : ∀ {n} {a b : Term n} → a ⇛ b → a →β* b
  ⇛⇒→β* refl            = ε
  ⇛⇒→β* (Π {a₁} {a₂} {b₁} {b₂} a₁⇛a₂ b₁⇛b₂) = begin
    Π a₁ b₁   ⟶⋆⟨ gmap (λ a → Π a _) (λ a₁→a₂ → Π₁ a₁→a₂ _) (⇛⇒→β* a₁⇛a₂) ⟩
    Π a₂ b₁   ⟶⋆⟨ gmap (Π _) (Π₂ _) (⇛⇒→β* b₁⇛b₂) ⟩
    Π a₂ b₂   ∎
  ⇛⇒→β* (ƛ {a₁} {a₂} {b₁} {b₂} a₁⇛a₂ b₁⇛b₂) = begin
    ƛ a₁ b₁   ⟶⋆⟨ gmap (λ a → ƛ a _) (λ a₁→a₂ → ƛ₁ a₁→a₂ _) (⇛⇒→β* a₁⇛a₂) ⟩
    ƛ a₂ b₁   ⟶⋆⟨ gmap (ƛ _) (ƛ₂ _) (⇛⇒→β* b₁⇛b₂) ⟩
    ƛ a₂ b₂   ∎
  ⇛⇒→β* (_·_ {a₁} {a₂} {b₁} {b₂} a₁⇛a₂ b₁⇛b₂) = begin
    a₁ · b₁   ⟶⋆⟨ gmap (λ a → a · _) (λ a₁→a₂ → a₁→a₂ ·₁ _) (⇛⇒→β* a₁⇛a₂) ⟩
    a₂ · b₁   ⟶⋆⟨ gmap (_·_ _) (_·₂_ _) (⇛⇒→β* b₁⇛b₂) ⟩
    a₂ · b₂   ∎
  ⇛⇒→β* (cont {a} {b₁} {b₂} {c₁} {c₂} b₁⇛b₂ c₁⇛c₂) = begin
    (ƛ a b₁) · c₁   ⟶⋆⟨ gmap (λ b → (ƛ _ b) · _)
                             (λ b₁→b₂ → (ƛ₂ _ b₁→b₂) ·₁ _) (⇛⇒→β* b₁⇛b₂) ⟩
    (ƛ a b₂) · c₁   ⟶⋆⟨ gmap (_·_ _) (_·₂_ _) (⇛⇒→β* c₁⇛c₂) ⟩
    (ƛ a b₂) · c₂   ⟶⟨ cont a b₂ c₂ ⟩
    b₂ [ c₂ ]       ∎

  -- Parallel reduction implies β-reduction.
  ⇛*⇒→β* : ∀ {n} {a b : Term n} → a ⇛* b → a →β* b
  ⇛*⇒→β* a⇛*b = (⇛⇒→β* ⋆) a⇛*b

  -- Parallel equivalence implies β-equivalence.
  ≡p⇒≡β : ∀ {n} {a b : Term n} → a ≡p b → a ≡β b
  ≡p⇒≡β a≡b = ([ ⇛⇒≡β , sym ∘ ⇛⇒≡β ] ⋆) a≡b
    where
      open Setoid ≡β-setoid using (sym)

      ⇛⇒≡β : ∀ {n} {a b : Term n} → a ⇛ b → a ≡β b
      ⇛⇒≡β = →*⇒↔ reduction ∘ ⇛⇒→β*

  open Equiv using (_⇔_; equivalence)

  -- Full β-reduction is equivalent to parallel reduction.
  →β*-⇛*-equivalence : ∀ {n} {a b : Term n} → a →β* b ⇔ a ⇛* b
  →β*-⇛*-equivalence = equivalence →β*⇒⇛* ⇛*⇒→β*

  -- β-equivalence is equivalent to parallel equivalence.
  ≡β-≡p-equivalence : ∀ {n} {a b : Term n} → a ≡β b ⇔ a ≡p b
  ≡β-≡p-equivalence = equivalence ≡β⇒≡p ≡p⇒≡β

  -- Shorthand for single-variable substitutions lifted to β-redcution.
  _[→β_] : ∀ {n} a {b₁ b₂ : Term n} → b₁ →β b₂ → a [ b₁ ] →β* a [ b₂ ]
  a [→β b₁→b₂ ] = ⇛⇒→β* (a / sub (→β⇒⇛ b₁→b₂))
    where open ParSubstitution using (_/_; sub)

  open P using (_≡_)

  -- Shapes are preserved by full β-reduction.

  sort-→β* : ∀ {n s} {a : Term n} → sort s →β* a → sort s ≡ a
  sort-→β* ε = P.refl
  sort-→β* (() ◅ _)

  ƛ-→β* : ∀ {n} {a : Term n} {b c} → ƛ a b →β* c →
          ∃ λ a′ → ∃ λ b′ → a →β* a′ × b →β* b′ × ƛ a′ b′ ≡ c
  ƛ-→β* λab→*c =
    let a′ , b′ , a⇛a′ , b⇛b′ , λa′b′≡c = ƛ-⇛* (→β*⇒⇛* λab→*c)
    in a′ , b′ , ⇛*⇒→β* a⇛a′ , ⇛*⇒→β* b⇛b′ , λa′b′≡c

  Π-→β* : ∀ {n} {a : Term n} {b c} → Π a b →β* c →
          ∃ λ a′ → ∃ λ b′ → a →β* a′ × b →β* b′ × Π a′ b′ ≡ c
  Π-→β* Πab→*c =
    let a′ , b′ , a⇛a′ , b⇛b′ , Πa′b′≡c = Π-⇛* (→β*⇒⇛* Πab→*c)
    in a′ , b′ , ⇛*⇒→β* a⇛a′ , ⇛*⇒→β* b⇛b′ , Πa′b′≡c

  ----------------------------------------------------------------------
  -- Confluence (aka the Church-Rosser property) of full β-reduction
  --
  -- Full β-reduction is confluent, i.e.  i.e. for any pair a →β* b₁,
  -- a →β* b₂ of parallel reductions, there is a term c, such that
  --
  --                               →β*
  --                           a ------→ b₂
  --                           |         :
  --                       →β* |         : →β*
  --                           ↓   →β*   ↓
  --                           b₁ ·····→ c
  --
  -- commutes.

  -- Confluence of _→β*_ (aka the Church-Rosser property).
  _⋄*_ : ∀ {n} {a b₁ b₂ : Term n} →
         a →β* b₁ → a →β* b₂ → ∃ λ c → b₁ →β* c × b₂ →β* c
  a→*b₁ ⋄* a→*b₂ =
    let c , b₁⇛*c , b₂⇛*c = (→β*⇒⇛* a→*b₁) Par.⋄* (→β*⇒⇛* a→*b₂)
    in c , ⇛*⇒→β* b₁⇛*c , ⇛*⇒→β* b₂⇛*c

  -- Factorization of β-equivalence into β-reductions.
  ≡β⇒→β* : ∀ {n} {a b : Term n} → a ≡β b → ∃ λ c → a →β* c × b →β* c
  ≡β⇒→β* a≡b =
    let c , a⇛*c , b⇛*c = ≡p⇒⇛* (≡β⇒≡p a≡b)
    in c , ⇛*⇒→β* a⇛*c , ⇛*⇒→β* b⇛*c

  -- Π-injectivity (with respect to ≡β).
  Π-inj : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} → Π a₁ b₁ ≡β Π a₂ b₂ →
          a₁ ≡β a₂ × b₁ ≡β b₂
  Π-inj Πa₁b₁≡Πa₂b₂ =
    let a₁≡a₂ , b₁≡b₂ = Par.Π-inj (≡β⇒≡p Πa₁b₁≡Πa₂b₂)
    in ≡p⇒≡β a₁≡a₂ , ≡p⇒≡β b₁≡b₂

  -- β-equivalence on sorts implies syntactic equivalence.
  sort-≡β : ∀ {n s₁ s₂} → sort {n} s₁ ≡β sort s₂ → s₁ ≡ s₂
  sort-≡β s₁≡βs₂ = Par.sort-≡p (≡β⇒≡p s₁≡βs₂)


text:
module Issue2447.Operator-error where

import Issue2447.M

_+_ : Set → Set → Set
A + _ = A

F : Set → Set
F A = A + A + A


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat renaming (_<_ to natLessThan)
open import Agda.Builtin.Int

_<_ : Int -> Int -> Bool
_<_ = \ where
  (pos m) (pos n) -> natLessThan m n
  (negsuc m) (negsuc n) -> natLessThan n m
  (negsuc _) (pos _) -> true
  (pos _) (negsuc _) -> false
{-# INLINE _<_ #-}

check : Int -> Bool
check n = pos 0 < n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- Verify that issue 3415 has been fixed by checking that the
-- computation rule for univalence holds up to a trivial transport (it
-- used to only hold up to a more complicated argument).
{-# OPTIONS --cubical #-}
module Issue3415 where

open import Agda.Primitive.Cubical public
open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.Glue public
open import Agda.Builtin.Sigma public

idIsEquiv : ∀ {ℓ} (A : Set ℓ) → isEquiv (λ (x : A) → x)
equiv-proof (idIsEquiv A) y =
  ((y , λ _ → y) , λ z i → z .snd (primINeg i)
  , λ j → z .snd (primIMax (primINeg i) j))

idEquiv : ∀ {ℓ} (A : Set ℓ) → A ≃ A
idEquiv A = ((λ x → x) , idIsEquiv A)

ua : ∀ {ℓ} {A B : Set ℓ} → A ≃ B → A ≡ B
ua {A = A} {B = B} e i =
  primGlue B (λ { (i = i0) → A ; (i = i1) → B })
             (λ { (i = i0) → e ; (i = i1) → (idEquiv B) })

transport : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
transport p a = primTransp (λ i → p i) i0 a

transportRefl : ∀ {ℓ}  {A : Set ℓ} → (x : A) → transport (λ _ → A) x ≡ x
transportRefl {A = A} x i = primTransp (λ _ → A) i x

uaβ : ∀ {ℓ} {A B : Set ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ e .fst x
uaβ e x = transportRefl (e .fst x)


text:
module BasicIS4.Metatheory.ClosedHilbert-TarskiClosedOvergluedImplicit where

open import BasicIS4.Syntax.ClosedHilbert public
open import BasicIS4.Semantics.TarskiClosedOvergluedImplicit public

open ImplicitSyntax (⊢_) public

-- Completeness with respect to a particular model.

module _ {{_ : Model}} where
  reify : ∀ {A} → ⊩ A → ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {□ A}   s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B} → ⊩ A → ⊩ B ▻ A
  ⟪K⟫ a = app ck (reify a) ⅋ K a

  ⟪S⟫′ : ∀ {A B C} → ⊩ A ▻ B ▻ C → ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ s₁ = app cs (reify s₁) ⅋ λ s₂ →
              app (app cs (reify s₁)) (reify s₂) ⅋ ⟪S⟫ s₁ s₂

  _⟪D⟫_ : ∀ {A B} → ⊩ □ (A ▻ B) → ⊩ □ A → ⊩ □ B
  (t ⅋ s) ⟪D⟫ (u ⅋ a) = app (app cdist t) u ⅋ s ⟪$⟫ a

  _⟪D⟫′_ : ∀ {A B} → ⊩ □ (A ▻ B) → ⊩ □ A ▻ □ B
  _⟪D⟫′_ s = app cdist (reify s) ⅋ _⟪D⟫_ s

  ⟪↑⟫ : ∀ {A} → ⊩ □ A → ⊩ □ □ A
  ⟪↑⟫ s = box (syn s) ⅋ s

  _⟪,⟫′_ : ∀ {A B} → ⊩ A → ⊩ B ▻ A ∧ B
  _⟪,⟫′_ a = app cpair (reify a) ⅋ _,_ a

-- Soundness with respect to all models, or evaluation, for closed terms only.

eval₀ : ∀ {A} → ⊢ A → ⊨ A
eval₀ (app t u) = eval₀ t ⟪$⟫ eval₀ u
eval₀ ci        = ci ⅋ I
eval₀ ck        = ck ⅋ ⟪K⟫
eval₀ cs        = cs ⅋ ⟪S⟫′
eval₀ (box t)   = box t ⅋ eval₀ t
eval₀ cdist     = cdist ⅋ _⟪D⟫′_
eval₀ cup       = cup ⅋ ⟪↑⟫
eval₀ cdown     = cdown ⅋ ⟪↓⟫
eval₀ cpair     = cpair ⅋ _⟪,⟫′_
eval₀ cfst      = cfst ⅋ π₁
eval₀ csnd      = csnd ⅋ π₂
eval₀ unit      = ∙

-- Correctness of evaluation with respect to conversion.

eval₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → eval₀ t ≡ eval₀ t′
eval₀✓ refl⋙           = refl
eval₀✓ (trans⋙ p q)    = trans (eval₀✓ p) (eval₀✓ q)
eval₀✓ (sym⋙ p)        = sym (eval₀✓ p)
eval₀✓ (congapp⋙ p q)  = cong² _⟪$⟫_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congi⋙ p)      = cong I (eval₀✓ p)
eval₀✓ (congk⋙ p q)    = cong² K (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congs⋙ p q r)  = cong³ ⟪S⟫ (eval₀✓ p) (eval₀✓ q) (eval₀✓ r)
eval₀✓ (congdist⋙ p q) = cong² _⟪D⟫_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congup⋙ p)     = cong ⟪↑⟫ (eval₀✓ p)
eval₀✓ (congdown⋙ p)   = cong ⟪↓⟫ (eval₀✓ p)
eval₀✓ (congpair⋙ p q) = cong² _,_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congfst⋙ p)    = cong π₁ (eval₀✓ p)
eval₀✓ (congsnd⋙ p)    = cong π₂ (eval₀✓ p)
eval₀✓ beta▻ₖ⋙         = refl
eval₀✓ beta▻ₛ⋙         = refl
eval₀✓ beta□⋙          = refl
eval₀✓ eta□⋙           = refl
eval₀✓ beta∧₁⋙         = refl
eval₀✓ beta∧₂⋙         = refl
eval₀✓ eta∧⋙           = refl
eval₀✓ eta⊤⋙          = refl

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_ = λ P → ⊢ α P
      }

-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ⊨ A → ⊢ A
quot₀ s = reify s

-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ⊢ A → ⊢ A
norm₀ = quot₀ ∘ eval₀

-- Correctness of normalisation with respect to conversion.

norm₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → norm₀ t ≡ norm₀ t′
norm₀✓ p = cong reify (eval₀✓ p)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module MonoidTactic where

open import Prelude
open import Container.Traversable
open import Tactic.Monoid
open import Tactic.Reflection

SemigroupAnd : Semigroup Bool
_<>_   {{SemigroupAnd}} = _&&_

MonoidAnd : Monoid Bool
Monoid.super MonoidAnd = SemigroupAnd
mempty {{MonoidAnd}} = true

Monoid/LawsAnd : Monoid/Laws Bool
Monoid/Laws.super Monoid/LawsAnd = MonoidAnd
left-identity {{Monoid/LawsAnd}} x = refl
right-identity {{Monoid/LawsAnd}} true = refl
right-identity {{Monoid/LawsAnd}} false = refl
monoid-assoc {{Monoid/LawsAnd}} true y z = refl
monoid-assoc {{Monoid/LawsAnd}} false y z = refl

test₁ : (a b : Bool) → (a && (b && a && true)) ≡ ((a && b) && a)
test₁ a b = auto-monoid {{Laws = Monoid/LawsAnd}}

test₂ : ∀ {a} {A : Set a} {{Laws : Monoid/Laws A}} →
          (x y : A) → x <> (y <> x <> mempty) ≡ (x <> y) <> x
test₂ x y = auto-monoid

test₃ : ∀ {a} {A : Set a} (xs ys zs : List A) → xs ++ ys ++ zs ≡ (xs ++ []) ++ (ys ++ []) ++ zs
test₃ xs ys zs = runT monoidTactic

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude