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

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

-- This module provides some definitions and properties that facilitate
-- proofs of properties about a distributed system modeled by Yasm.System
-- paramaterized by some SystemParameters.

module LibraBFT.Yasm.Properties
   (ℓ-PeerState : Level)
   (ℓ-VSFP : Level)
   (parms       : LYB.SystemParameters ℓ-PeerState)
   -- In addition to the parameters used by the rest of the system model, this module
   -- needs to relate Members to PKs and PeerIds, so that StepPeerState-AllValidParts
   -- can be defined.  This enables the application to prove that honest peers sign
   -- new messages only for their own public key.  The system model does not know that
   -- directly.
 -- A ValidPartForPK collects the assumptions about what a /part/ in the outputs of an honest verifier
 -- satisfies: (i) the epoch field is consistent with the existent epochs and (ii) the verifier is
 -- a member of the associated epoch config, and (iii) has the given PK in that epoch.

   (ValidSenderForPK        : LYS.ValidSenderForPK-type        ℓ-PeerState ℓ-VSFP parms)
 -- A valid part remains valid across state transitions (including cheat steps)
   (ValidSenderForPK-stable : LYS.ValidSenderForPK-stable-type ℓ-PeerState ℓ-VSFP parms ValidSenderForPK)
  where
 open LYB.SystemParameters parms
 open import LibraBFT.Yasm.Base
 open import LibraBFT.Yasm.System ℓ-PeerState ℓ-VSFP parms
 open import Util.FunctionOverride PeerId _≟PeerId_

 -- A few handy properties for transporting information about whether a Signature is ∈GenInfo to
 -- another type containing the same signature
 transp-∈GenInfo₀ : ∀ {pk p1 p2}
                  → (ver1 : WithVerSig {Part} ⦃ Part-sig ⦄ pk p1)
                  → (ver2 : WithVerSig {Part} ⦃ Part-sig ⦄ pk p2)
                  → ver-signature ver1 ≡ ver-signature ver2
                  → ∈GenInfo (ver-signature ver1)
                  → ∈GenInfo (ver-signature ver2)
 transp-∈GenInfo₀ ver1 ver2 sigs≡ init = subst ∈GenInfo sigs≡ init

 transp-¬∈GenInfo₁ : ∀ {pk pool sig}
                  → ¬ ∈GenInfo sig
                  → (mws : MsgWithSig∈ pk sig pool)
                  → ¬ ∈GenInfo (ver-signature (msgSigned mws))
 transp-¬∈GenInfo₁ ¬init mws rewrite sym (msgSameSig mws) = ¬init

 transp-¬∈GenInfo₂ : ∀ {pk sig1 sig2 pool}
                  → (mws1 : MsgWithSig∈ pk sig1 pool)
                  → ¬ (∈GenInfo (ver-signature (msgSigned mws1)))
                  → (mws2 : MsgWithSig∈ pk sig2 pool)
                  → sig2 ≡ sig1
                  → ¬ (∈GenInfo (ver-signature (msgSigned mws2)))
 transp-¬∈GenInfo₂ mws1 ¬init mws2 refl = ¬subst {P = ∈GenInfo} ¬init (trans (msgSameSig mws2) (sym (msgSameSig mws1)))

 ¬cheatForgeNew : ∀ {pid pk vsig mst outs m}{st : SystemState}
                → (sp : StepPeer st pid mst outs)
                → outs ≡ LYT.send m ∷ []
                → (ic : isCheat sp)
                → Meta-Honest-PK pk
                → (mws : MsgWithSig∈ pk vsig ((pid , m) ∷ msgPool st))
                → ¬ (∈GenInfo (ver-signature (msgSigned mws)))
                → MsgWithSig∈ pk vsig (msgPool st)
 ¬cheatForgeNew {st = st} sc@(step-cheat isch) refl _ hpk mws ¬init
    with msg∈pool mws
 ...| there m∈pool = mkMsgWithSig∈ (msgWhole mws) (msgPart mws) (msg⊆ mws) (msgSender mws) m∈pool (msgSigned mws) (msgSameSig mws)
 ...| here m∈pool
    with cong proj₂ m∈pool
 ...| refl
    with isch (msg⊆ mws) (msgSigned mws) ¬init
 ...| inj₁ dis = ⊥-elim (hpk dis)
 ...| inj₂ mws' rewrite msgSameSig mws = mws'

 ValidSenderForPK-stable-* : ∀{st : SystemState}{st' : SystemState}
                           → ReachableSystemState st
                           → Step* st st' → ∀{part α pk}
                           → ValidSenderForPK st  part α pk
                           → ValidSenderForPK st' part α pk
 ValidSenderForPK-stable-* _ step-0 v = v
 ValidSenderForPK-stable-* r (step-s {pre = st''} st''reach x) {part} {α} {pk} v =
                           ValidSenderForPK-stable (Step*-trans r st''reach) x
                                                   (ValidSenderForPK-stable-* r st''reach v)

 -- We say that an implementation produces only valid parts iff all parts of every message in the
 -- output of a 'StepPeerState' are either: (i) a valid new part (i.e., the part is valid and no
 -- message with the same signature has been sent previously), or (ii) a message has been sent
 -- with the same signature.
 StepPeerState-AllValidParts : Set (ℓ-VSFP ℓ⊔ ℓ+1 ℓ-PeerState)
 StepPeerState-AllValidParts = ∀{s m part pk outs}{α}{st : SystemState}
   → (r : ReachableSystemState st)
   → Meta-Honest-PK pk
   → (sps : StepPeerState α (msgPool st) (initialised st) (peerStates st α) (s , outs))
   → LYT.send m ∈ outs → part ⊂Msg m → (ver : WithVerSig pk part)
   → ¬ (∈GenInfo (ver-signature ver))
     -- Note that we require that α can send for the PK according to the *post* state.  This allows
     -- sufficient generality to ensure that a peer can sign and send a message for an epoch even if
     -- it changed to the epoch in the same step.  If this is too painful, we could require that the
     -- peer can sign for the PK already in the prestate, which would require, for example,
     -- initialising a peer to be a separate step from sending its first signed message, which in
     -- turn could preclude some valid implementations.
   → (ValidSenderForPK (StepPeer-post {pre = st} (step-honest sps)) part α pk × ¬ (MsgWithSig∈ pk (ver-signature ver) (msgPool st)))
   ⊎ MsgWithSig∈ pk (ver-signature ver) (msgPool st)

 -- A /part/ was introduced by a specific step when:
 IsValidNewPart : ∀{pre : SystemState}{post : SystemState} → Signature → PK → Step pre post → Set (ℓ-VSFP ℓ⊔ ℓ+1 ℓ-PeerState)
 -- said step is a /step-peer/ and
 IsValidNewPart {pre} {post} sig pk (step-peer {pid = pid} pstep)
    -- the part has never been seen before
    = ReachableSystemState pre
    × ¬ ∈GenInfo sig
    × ¬ (MsgWithSig∈ pk sig (msgPool pre))
    × Σ (MsgWithSig∈ pk sig (msgPool (StepPeer-post pstep)))
        (λ m → msgSender m ≡ pid × initialised post pid ≡ initd × ValidSenderForPK post (msgPart m) (msgSender m) pk)

 mwsAndVspk-stable : ∀{st : SystemState}{st' : SystemState}
                   → ReachableSystemState st
                   → Step* st st'
                   → ∀ {pk sig}
                   → (mws : MsgWithSig∈ pk sig (msgPool st))
                   → initialised st (msgSender mws) ≡ initd
                   → ValidSenderForPK st (msgPart mws) (msgSender mws) pk
                   → Σ (MsgWithSig∈ pk sig (msgPool st')) λ mws' →
                       ValidSenderForPK st' (msgPart mws') (msgSender mws') pk
 mwsAndVspk-stable {_} {st'} r tr {pk} {sig} mws ini vpk = MsgWithSig∈-Step* tr mws
                                                     , subst₂ (λ p s → ValidSenderForPK st' p s pk)
                                                              (MsgWithSig∈-Step*-part tr mws)
                                                              (MsgWithSig∈-Step*-sender tr mws)
                                                              (ValidSenderForPK-stable-* r tr vpk)

 -- When we can prove that the implementation provided by 'parms' at the
 -- top of this module satisfies 'StepPeerState-AllValidParts', we can
 -- prove a number of useful structural properties:

 -- TODO-2: Refactor into a file (LibraBFT.Yasm.Properties.Structural) later on
 -- if this grows too large.
 module Structural (sps-avp      : StepPeerState-AllValidParts) where
     -- We can unwind the state and highlight the step where a part was
     -- originally sent. This 'unwind' function combined with Any-Step-elim
     -- enables a powerful form of reasoning. The 'honestVoteEpoch' below
     -- exemplifies this well.
     unwind : ∀{st : SystemState}(tr : ReachableSystemState st)
            → ∀{p m σ pk} → Meta-Honest-PK pk
            → p ⊂Msg m → (σ , m) ∈ msgPool st → (ver : WithVerSig pk p)
            → ¬ ∈GenInfo (ver-signature ver)
            → Any-Step (IsValidNewPart (ver-signature ver) pk) tr
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) hpk p⊂m m∈sm sig ¬init
       with Any-++⁻ (actionsToSentMessages β outs) {msgPool pre} m∈sm
     ...| inj₂ furtherBack = step-there (unwind tr hpk p⊂m furtherBack sig ¬init)
     ...| inj₁ thisStep
       with sp
     ...| step-cheat isCheat
       with thisStep
     ...| here refl
       with isCheat p⊂m sig ¬init
     ...| inj₁ abs    = ⊥-elim (hpk abs)
     ...| inj₂ sentb4
       with unwind tr {p = msgPart sentb4} hpk (msg⊆ sentb4) (msg∈pool sentb4) (msgSigned sentb4)
                                           (transp-¬∈GenInfo₁ ¬init sentb4)
     ...| res rewrite msgSameSig sentb4 = step-there res
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) hpk p⊂m m∈sm sig ¬init
        | inj₁ thisStep
        | step-honest x
       with senderMsgPair∈⇒send∈ outs thisStep
     ...| m∈outs , refl
       with sps-avp tr hpk x m∈outs p⊂m sig ¬init
     ...| inj₂ sentb4 with unwind tr {p = msgPart sentb4} hpk (msg⊆ sentb4) (msg∈pool sentb4) (msgSigned sentb4)
                                  (¬subst {P = ∈GenInfo} ¬init (msgSameSig sentb4))
     ...| res rewrite msgSameSig sentb4 = step-there res
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) {p} hpk p⊂m m∈sm sig ¬init
        | inj₁ thisStep
        | step-honest x
        | m∈outs , refl
        | inj₁ (valid-part , notBefore) = step-here tr (tr , ¬init , notBefore , mws∈pool , refl , override-target-≡ , valid-part)
        where mws∈pool : MsgWithSig∈ _ (WithSig.signature Part-sig _ (isSigned sig)) (actionsToSentMessages β outs ++ msgPool pre)
              mws∈pool = MsgWithSig∈-++ˡ (mkMsgWithSig∈ _ _ p⊂m β thisStep sig refl)

     -- Unwind is inconvenient to use by itself because we have to do
     -- induction on Any-Step-elim. The 'honestPartValid' property below
     -- provides a fairly general result conveniently: for every part
     -- verifiable with an honest PK, there is a msg with the same
     -- signature that is valid for some pid.

     honestPartValid : ∀ {st} → ReachableSystemState st → ∀ {pk nm v sender}
                     → Meta-Honest-PK pk
                     → v ⊂Msg nm → (sender , nm) ∈ msgPool st → (ver : WithVerSig pk v)
                     → ¬ ∈GenInfo (ver-signature ver)
                     → Σ (MsgWithSig∈ pk (ver-signature ver) (msgPool st))
                         (λ msg → (ValidSenderForPK st (msgPart msg) (msgSender msg) pk))
     honestPartValid {st} r {pk = pk} hpk v⊂m m∈pool ver ¬init
     -- We extract two pieces of important information from the place where the part 'v'
     -- was first sent: (a) there is a message with the same signature /in the current pool/
     -- and (b) its epoch is less than e.
        = Any-Step-elim (λ { {st = step-peer {pid = pid} (step-honest sps)} (preReach , ¬init , ¬sentb4 , new , refl , ini , valid) tr
                             → mwsAndVspk-stable (step-s preReach (step-peer (step-honest sps))) tr new ini valid
                           ; {st = step-peer {pid = pid} {pre = pre} (step-cheat {pid} sps)} (preReach , ¬init , ¬sentb4 , new , refl , valid) tr
                            → ⊥-elim (¬sentb4 (¬cheatForgeNew {st = pre} (step-cheat sps) refl unit hpk new (transp-¬∈GenInfo₁ ¬init new)))
                        })
                        (unwind r hpk v⊂m m∈pool ver ¬init)

     -- Unforgeability is also an important property stating that every part that is
     -- verified with an honest public key has either been sent by α or is a replay
     -- of another message sent before.
     ext-unforgeability'
       : ∀{α m part pk}{st : SystemState} → ReachableSystemState st
       -- If a message m has been sent by α, containing part
       → (α , m) ∈ msgPool st → part ⊂Msg m
       -- And the part can be verified with an honest public key,
       → (sig : WithVerSig pk part) → ¬ ∈GenInfo (ver-signature sig)
       → Meta-Honest-PK pk
       -- then either the part is a valid part by α (meaning that α can
       -- sign the part itself) or a message with the same signature has
       -- been sent previously.
       → ValidSenderForPK st part α pk
       ⊎ MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     ext-unforgeability' {part = part} (step-s st (step-peer {pid = β} {outs = outs} {pre = pre} sp)) m∈sm p⊆m sig ¬init hpk
       with Any-++⁻ (actionsToSentMessages β outs) {msgPool pre} m∈sm
     ...| inj₂ furtherBack = MsgWithSig∈-++ʳ <⊎$> ⊎-map (ValidSenderForPK-stable st (step-peer sp)) id
                                                        (ext-unforgeability' st furtherBack p⊆m sig ¬init hpk)
     ...| inj₁ thisStep
       with sp
     ...| step-cheat isCheat
       with thisStep
     ...| here refl
       with isCheat p⊆m sig ¬init
     ...| inj₁ abs    = ⊥-elim (hpk abs)
     ...| inj₂ sentb4 = inj₂ (MsgWithSig∈-++ʳ sentb4)
     ext-unforgeability' {α = α} {m = m} {part = part} (step-s st (step-peer {pid = β} {outs = outs} {pre = pre} sp)) m∈sm p⊆m sig ¬init hpk
        | inj₁ thisStep
        | step-honest x
       with senderMsgPair∈⇒send∈ outs thisStep
     ...| m∈outs , refl = ⊎-map proj₁ MsgWithSig∈-++ʳ (sps-avp st hpk x m∈outs p⊆m sig ¬init)

     -- The ext-unforgeability' property can be collapsed in a single clause.

     -- TODO-2: so far, ext-unforgeability is used only to get a MsgWithSig∈ that is passed to
     -- msgWithSigSentByAuthor, which duplicates some of the reasoning in the proof of
     -- ext-unforgeability'; should these properties possibly be combined into one simpler proof?
     ext-unforgeability
       : ∀{α₀ m part pk}{st : SystemState} → ReachableSystemState st
       → (α₀ , m) ∈ msgPool st → part ⊂Msg m
       → (sig : WithVerSig pk part) → ¬ ∈GenInfo (ver-signature sig)
       → Meta-Honest-PK pk
       → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     ext-unforgeability {α₀} {m} {st = st} rst m∈sm p⊂m sig ¬init hpk
       with ext-unforgeability' rst m∈sm p⊂m sig ¬init hpk
     ...| inj₁ p
        = mkMsgWithSig∈ _ _ p⊂m α₀ m∈sm sig refl
     ...| inj₂ sentb4 = sentb4

     msgWithSigSentByAuthor : ∀ {pk sig}{st : SystemState}
                            → ReachableSystemState st
                            → Meta-Honest-PK pk
                            → (mws : MsgWithSig∈ pk sig (msgPool st))
                            → ¬ (∈GenInfo (ver-signature (msgSigned mws)))
                            → (Σ (MsgWithSig∈ pk sig (msgPool st))
                                 λ mws' → ValidSenderForPK st (msgPart mws') (msgSender mws') pk)
     msgWithSigSentByAuthor step-0 _ ()
     msgWithSigSentByAuthor {pk} {sig} (step-s {pre = pre} preach (step-peer theStep@(step-cheat cheatCons))) hpk mws ¬init
        with (¬cheatForgeNew theStep refl unit hpk mws ¬init)
     ...| mws'
        with msgWithSigSentByAuthor preach hpk mws' (transp-¬∈GenInfo₂ mws ¬init (MsgWithSig∈-++ʳ mws') refl)
     ...| (mws'' , vpb'') = MsgWithSig∈-++ʳ mws'' , ValidSenderForPK-stable preach (step-peer theStep) vpb''
     msgWithSigSentByAuthor (step-s {pre = pre} preach theStep@(step-peer {pid = pid} {outs = outs} (step-honest sps))) hpk mws ¬init
       with Any-++⁻ (actionsToSentMessages pid outs) {msgPool pre} (msg∈pool mws)
     ...| inj₂ furtherBack
       with msgWithSigSentByAuthor preach hpk (MsgWithSig∈-transp mws furtherBack) ¬init
     ...| (mws' , vpb') = MsgWithSig∈-++ʳ mws' , ValidSenderForPK-stable preach theStep vpb'
     msgWithSigSentByAuthor (step-s {pre = pre} preach theStep@(step-peer {pid = pid} {outs = outs} (step-honest sps))) hpk mws ¬init
        | inj₁ thisStep
       with senderMsgPair∈⇒send∈ outs thisStep
     ...| m∈outs , refl
        with sps-avp preach hpk sps m∈outs (msg⊆ mws) (msgSigned mws) ¬init
     ...| inj₁ (vpbα₀ , _) = mws , vpbα₀
     ...| inj₂ mws'
        with msgWithSigSentByAuthor preach hpk mws' (transp-¬∈GenInfo₂ mws ¬init (MsgWithSig∈-++ʳ mws') (msgSameSig mws))
     ...| (mws'' , vpb'') rewrite sym (msgSameSig mws) = MsgWithSig∈-++ʳ mws'' , ValidSenderForPK-stable preach theStep vpb''

     newMsg⊎msgSentB4 :  ∀ {pk v m pid sndr s' outs} {st : SystemState}
                      → (r : ReachableSystemState st)
                      → (stP : StepPeerState pid (msgPool st) (initialised st) (peerStates st pid) (s' , outs))
                      → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                      → ¬ (∈GenInfo (ver-signature sig))
                      → v ⊂Msg m → (sndr , m) ∈ msgPool (StepPeer-post {pre = st} (step-honest stP))
                      → ( LYT.send m ∈ outs × ValidSenderForPK (StepPeer-post {pre = st} (step-honest stP)) v pid pk
                        × ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool st)))
                        ⊎ MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     newMsg⊎msgSentB4 {pk} {v} {m} {pid} {sndr} {s'} {outs} {st} r stP pkH sig ¬init v⊂m m∈post
        with Any-++⁻ (actionsToSentMessages pid outs) m∈post
     ...| inj₂ m∈preSt = inj₂ (mkMsgWithSig∈ m v v⊂m sndr m∈preSt sig refl)
     ...| inj₁ nm∈outs
        with senderMsgPair∈⇒send∈ outs nm∈outs
     ...| m∈outs , refl
        with sps-avp r pkH stP m∈outs v⊂m sig ¬init
     ...| inj₁ newVote = inj₁ (m∈outs , newVote)
     ...| inj₂ msb4    = inj₂ msb4

 -- This could potentially be more general, for example covering the whole SystemState, rather than
  -- just one peer's state.  However, this would put more burden on the user and is not required so
 -- far.
 CarrierProp : Set (1ℓ ℓ⊔ ℓ-PeerState)
 CarrierProp = Part → PeerState → Set

 module _ (P   : CarrierProp) where

  record PropCarrier (pk : PK) (sig : Signature) (st : SystemState) : Set (ℓ-VSFP ℓ⊔ ℓ+1 ℓ-PeerState) where
    constructor mkCarrier
    field
      carrStReach : ReachableSystemState st -- Enables use of invariants when proving that steps preserve carrProp
      carrSent    : MsgWithSig∈ pk sig (msgPool st)
      carrInitd   : initialised st (msgSender carrSent) ≡ initd
      carrValid   : ValidSenderForPK st (msgPart carrSent) (msgSender carrSent) pk
      carrProp    : P (msgPart carrSent) (peerStates st (msgSender carrSent))
  open PropCarrier public

  PeerStepPreserves : Set (ℓ-VSFP ℓ⊔ ℓ+1 ℓ-PeerState)
  PeerStepPreserves = ∀ {ps' outs pk sig}{pre : SystemState}
                      → (r : ReachableSystemState pre)
                      → (pc : PropCarrier pk sig pre)
                      → (sps : StepPeerState     (msgSender (carrSent pc))
                                                 (msgPool pre)
                                                 (initialised pre)
                                                 (peerStates pre (msgSender (carrSent pc)))
                                                 (ps' , outs))
                      → P (msgPart (carrSent pc)) ps'

  module _ (PSP : PeerStepPreserves) where

    Carrier-transp : ∀ {pk sig} {pre : SystemState}{post : SystemState}
                   → (theStep : Step pre post)
                   → PropCarrier pk sig pre
                   → PropCarrier pk sig post
    Carrier-transp {pk} {pre = pre} {post} theStep@(step-peer {pid = pid} {st'} {pre = .pre} sps) pc@(mkCarrier r mws ini vpk prop)
       with step-s r theStep
    ...| postReach
       with sps
    ...| cheatStep@(step-cheat isch) = mkCarrier postReach (MsgWithSig∈-++ʳ mws)
                                 (trans (cong (λ f → f (msgSender mws)) (cheatStepDNMInitialised cheatStep unit)) ini)      -- PeerStates not changed by cheat steps
                                 (ValidSenderForPK-stable {pre} r (step-peer cheatStep) vpk)
                                 (subst (λ ps → P (msgPart mws) (ps (msgSender mws))) (sym (cheatStepDNMPeerStates {pre = pre} (step-cheat isch) unit)) prop)
    ...| honStep@(step-honest {st = st} sps')
       with msgSender mws ≟PeerId pid
    ...| no neq   = mkCarrier postReach (MsgWithSig∈-++ʳ mws) (trans (sym (override-target-≢ neq)) ini)
                              (ValidSenderForPK-stable {pre} r (step-peer (step-honest sps')) vpk)
                              (subst (λ ps → P (msgPart mws) ps) (override-target-≢ {f = peerStates pre} neq) prop)
    ...| yes refl = mkCarrier postReach (MsgWithSig∈-++ʳ mws) override-target-≡
                              (ValidSenderForPK-stable {part = msgPart mws} {pk = pk} r (step-peer honStep) vpk)
                              (subst (λ ps → P (msgPart mws) ps) (sym override-target-≡) (PSP r pc sps'))

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
open import Type
open import Structure.Relator
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)

module Structure.Sets.ZFC.Classical {ℓₛ ℓₗ ℓₑ} {S : Type{ℓₛ}} ⦃ equiv : Equiv{ℓₑ}(S) ⦄ (_∈_ : S → S → Type{ℓₗ}) ⦃ [∈]-binaryRelator : BinaryRelator(_∈_) ⦄ where

open import Data.Either as Either using ()
open import Functional
open import Logic.Classical
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
import      Lvl
open import Structure.Operator
open import Structure.Relator.Proofs
open import Structure.Relator.Properties
import      Structure.Sets.Names
open        Structure.Sets.Names.From-[∈] (_∈_)
open        Structure.Sets.Names.Relations (_∈_)
open import Structure.Sets.ZFC(_∈_) ⦃ [∈]-binaryRelator ⦄
open import Syntax.Function
open import Syntax.Implication
open import Syntax.Transitivity

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x : S

module _ ⦃ zfc : ZFC ⦄ where
  open ZFC(zfc)

  -- ZFC implies excluded middle.
  -- Note that this only requires the following set related axioms:
  -- • Set extensionality (Not really neccessary if every equality is replaced with set equality instead).
  -- • Axiom of choice (TODO: Is this really neccessary? The proof only uses the choice function on finite sets? Further investigation on choice functions for finite sets would clear this up).
  -- • Choice functions are functions.
  -- • Restricted set comprehension.
  -- • Existence of at least two different sets (In this proof, ∅ and {∅} (𝑇 and 𝐹) is used).
  -- • Existence of a set containing the two different sets, and the existence of all subsets of this set.
  -- Also called: Diaconescu's theorem, Goodman–Myhill theorem.
  excluded-middle-by-choice : ∀{P : Type{ℓ}} → Classical(P)
  excluded-middle-by-choice{P = P} = intro $ᵢₙₛₜ
    let
      instance
        pos-rel : UnaryRelator(x ↦ P ∨ (x ≡ 𝑇))
        pos-rel = [∨]-unaryRelator ⦃ rel-Q = binary-unaryRelatorᵣ ⦄

      instance
        neg-rel : UnaryRelator(x ↦ P ∨ (x ≡ 𝐹))
        neg-rel = [∨]-unaryRelator ⦃ rel-Q = binary-unaryRelatorᵣ ⦄

      pos = filter (x ↦ P ∨ (x ≡ 𝑇)) BoolSet
      neg = filter (x ↦ P ∨ (x ≡ 𝐹)) BoolSet

      -- The contents of pos by definition. A subset of BoolSet which is equal to BoolSet when P, {𝑇} otherwise.
      pos-containment : (x ∈ pos) ↔ (x ∈ BoolSet) ∧ (P ∨ (x ≡ 𝑇))
      pos-containment = restricted-comprehension

      -- The contents of neg by definition. A subset of BoolSet which is equal to BoolSet when P, {𝐹} otherwise.
      neg-containment : (x ∈ neg) ↔ (x ∈ BoolSet) ∧ (P ∨ (x ≡ 𝐹))
      neg-containment = restricted-comprehension

      -- pos is non-empty because it should at least contain 𝑇 from filtering BoolSet.
      instance
        ne-pos : NonEmpty(pos)
        ne-pos = [↔]-to-[←] (nonEmpty-filter) ([∃]-intro 𝑇 ⦃ [∧]-intro 𝑇-in-BoolSet ([∨]-introᵣ (\{_} → [↔]-reflexivity)) ⦄)

      -- neg is non-empty because it should at least contain 𝐹 from filtering BoolSet.
      instance
        ne-neg : NonEmpty(neg)
        ne-neg = [↔]-to-[←] (nonEmpty-filter) ([∃]-intro 𝐹 ⦃ [∧]-intro 𝐹-in-BoolSet ([∨]-introᵣ (\{_} → [↔]-reflexivity)) ⦄)

      -- Chooses an element in respective sets pos and neg.
      pos-choose = choose (pair pos neg) pos
      neg-choose = choose (pair pos neg) neg

      -- By definition of pos, either P holds or pos-choose have to be 𝑇.
      pos-choice : P ∨ (pos-choose ≡ 𝑇)
      pos-choice = [∧]-elimᵣ ([↔]-to-[→] pos-containment (choice {pair pos neg} {pos} ⦃ ne-pos ⦄ ⦃ pair-contains-left ⦄))

      -- By definition of neg, either P holds or neg-choose have to be 𝐹.
      neg-choice : P ∨ (neg-choose ≡ 𝐹)
      neg-choice = [∧]-elimᵣ ([↔]-to-[→] neg-containment (choice {pair pos neg} {neg} ⦃ ne-neg ⦄ ⦃ pair-contains-right ⦄))
    in
      • ( -- Contrapositive of the argument below states that if pos-choose and neg-choose is inequal, then (¬ P)
        (_⇒ -- When P holds, both pos and neg is BoolSet, so they are equal. The pos-choose and neg-choose is the choice function applied to the equal sets pos and neg respectively, and because choose is a function (it respects equality, specifically set equality), pos-choose and neg-choose is also equal.
          P                          ⇒-[ (\p {x} → [↔]-transitivity (pos-containment {x}) ([↔]-transitivity ([∧]-mapᵣ-[↔] ([↔]-intro (const([∨]-introₗ p)) (const([∨]-introₗ p)))) ([↔]-symmetry (neg-containment {x})))) ]
          (pos ≡ neg)                ⇒-[ [↔]-to-[←] set-extensionality ]
          (pos ≡ₑ neg)               ⇒-[ congruence₂(choose) (reflexivity(_≡ₑ_)) ]
          (pos-choose ≡ₑ neg-choose) ⇒-end
        ) ⇒
        (P → (pos-choose ≡ₑ neg-choose))    ⇒-[ contrapositiveᵣ ]
        ((¬ P) ← (pos-choose ≢ neg-choose)) ⇒-end
      )
      • ( -- The case other than P is that pos and neg only contains 𝑇 and 𝐹 respectively. This forces pos-choose and neg-choose to be 𝑇 and 𝐹 respectively, which means that they are inequal.
        • pos-choice
        • neg-choice
        ⇒₂-[ [∧]-intro ]
        (P ∨ (pos-choose ≡ 𝑇)) ∧ (P ∨ (neg-choose ≡ 𝐹)) ⇒-[ [↔]-to-[←] [∨][∧]-distributivityₗ ]
        P ∨ ((pos-choose ≡ 𝑇) ∧ (neg-choose ≡ 𝐹))       ⇒-[ Either.mapRight (\{([∧]-intro p0 n1) → [≡][≢]-semitransitivityᵣ([≡][≢]-semitransitivityₗ ([↔]-to-[←] set-extensionality p0) zero-one-ineq) (symmetry(_≡ₑ_) ([↔]-to-[←] set-extensionality n1))}) ]
        P ∨ (pos-choose ≢ neg-choose)                   ⇒-end
      )
      ⇒₂-[ Either.mapRight ]
      (P ∨ (¬ P)) ⇒-end

ext: agda

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:
------------------------------------------------------------------------------
-- Division program
------------------------------------------------------------------------------

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

-- This module define a division program using repeated subtraction
-- (Dybjer 1985).

-- Peter Dybjer. Program verification in a logical theory of
-- constructions. In Jean-Pierre Jouannaud, editor. Functional
-- Programming Languages and Computer Architecture, volume 201 of
-- LNCS, 1985, pages 334-349. Appears in revised form as Programming
-- Methodology Group Report 26, June 1986.

module FOTC.Program.Division.Division where

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

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

postulate
  div    : D → D → D
  div-eq : ∀ i j → div i j ≡ (if (lt i j) then zero else succ₁ (div (i ∸ j) j))
{-# ATP axiom div-eq #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Data.ByteString.Primitive.Lazy where

open import Data.Word8.Primitive using (Word8)
open import Agda.Builtin.Nat using (Nat)
open import Data.Colist using (Colist)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.IO using (IO)
open import Data.Tuple.Base using (Pair)

{-# FOREIGN GHC import qualified Data.Word    #-}
{-# FOREIGN GHC import qualified Data.Text    #-}
{-# FOREIGN GHC import qualified Data.ByteString.Lazy    #-}
open import Foreign.Haskell using (Unit)

open import Data.ByteString.Primitive.Int

postulate
  ByteStringLazy : Set
  readBinaryFileLazy    : String → IO ByteStringLazy
  writeBinaryFileLazy   : String → ByteStringLazy → IO Unit
  Colist←Lazy : ByteStringLazy → Colist Word8
  Colist→Lazy : Colist Word8 → ByteStringLazy
  emptyLazy : ByteStringLazy
  nullLazy : ByteStringLazy → Bool
  lengthLazy : ByteStringLazy → Int64
  headLazy : ByteStringLazy → Word8
  tailLazy : ByteStringLazy → ByteStringLazy
  indexLazy : ByteStringLazy → Int64 → Word8
  splitAtLazy : Int64 → ByteStringLazy → Pair ByteStringLazy ByteStringLazy
  appendLazy : ByteStringLazy → ByteStringLazy → ByteStringLazy

{-# COMPILE GHC ByteStringLazy = type
    Data.ByteString.Lazy.ByteString
#-}
{-# COMPILE GHC readBinaryFileLazy =
    ( Data.ByteString.Lazy.readFile
    . Data.Text.unpack
    )
#-}
{-# COMPILE GHC writeBinaryFileLazy =
    ( Data.ByteString.Lazy.writeFile
    . Data.Text.unpack
    )
#-}
{-# COMPILE GHC Colist←Lazy =
    ( Data.ByteString.Lazy.unpack ) #-}
{-# COMPILE GHC Colist→Lazy =
    ( Data.ByteString.Lazy.pack ) #-}
{-# COMPILE GHC emptyLazy = (Data.ByteString.Lazy.empty) #-}
{-# COMPILE GHC nullLazy = (Data.ByteString.Lazy.null) #-}
{-# COMPILE GHC lengthLazy = (Data.ByteString.Lazy.length) #-}
{-# COMPILE GHC headLazy = (Data.ByteString.Lazy.head) #-}
{-# COMPILE GHC tailLazy = (Data.ByteString.Lazy.tail) #-}
{-# COMPILE GHC indexLazy = (Data.ByteString.Lazy.index) #-}
{-# COMPILE GHC appendLazy = (Data.ByteString.Lazy.append) #-}
{-# COMPILE GHC splitAtLazy = (Data.ByteString.Lazy.splitAt) #-}

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
module Oscar.Data.Permutation.Properties where

open import Data.Permutation.Properties public

open import Data.Nat
open import Oscar.Data.Vec renaming (delete to deleteV)
open import Oscar.Data.Vec.Properties
open import Oscar.Data.Permutation

∈-enum : ∀ {n m} (i : Inj n m) → i ∈ enum n m
∈-enum {zero} [] = here
∈-enum {suc n} (i ∷ is) = ∈-map₂ _∷_ (∈-allFin i) (∈-enum is)

open import Data.Fin
open import Relation.Binary.PropositionalEquality

permute-correct : ∀ {a n} {A : Set a} → (p : Permutation n) → (v : Vec A n) →
                  [ v ≡Permutation permute p v ] p
permute-correct [] [] = λ ()
permute-correct (p ∷ ps) (_ ∷ _) zero = here
permute-correct (p ∷ ps) v@(_ ∷ _) (suc f) =
  let bs = permute ps (deleteV p v)
      delresult = permute-correct ps (deleteV p v)
  in
  there ((subst (bs [ f ]=_) (lookup-delete-thin p (< ps > f) v) ((delresult f))))

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

enumPermutations-complete : ∀ {a n} {A : Set a} → (xs : Vec A n) → ∀ ys → xs ∃≡Permutation ys → ys ∈ enumPermutations xs
enumPermutations-complete [] [] ([] , xs=ys|p) = here
enumPermutations-complete (x ∷ xs) (y ∷ ys) (p ∷ ps , xs=ys|p∷ps) = {!!}


text:
module SubstTheory where

open import Prelude
open import T

-- I originally used postulated extensional equality to reason about
-- identical substitutions. As it turns out, it's actually somewhat
-- cleaner to appeal to a proof that using identically performing subst
-- functions produce the same outputs.

---- (Lots of theory. *Lots*. Too much. Sigh.)

module SubstTheory where

  Ren≡ : ∀ {Γ Γ'}(f g : TRen Γ Γ') → Set
  Ren≡ f g = ∀ {A} x → f {A} x ≡ g {A} x

  -- Some theorems about renamings
  wkeq : ∀{Γ Γ' A} {f g : TRen Γ Γ'} → Ren≡ f g → Ren≡ (wk {A = A} f) (wk g)
  wkeq eq Z = Refl
  wkeq eq (S n) = resp S (eq n)

  -- Prove that applying equal renamings produces equal outputs
  reneq : ∀{Γ Γ' A} {f g : TRen Γ Γ'} → Ren≡ f g → (e : TExp Γ A) → ren f e ≡ ren g e
  reneq eq (var x) = resp var (eq x)
  reneq eq (Λ e) = resp Λ (reneq (wkeq eq) e)
  reneq eq (e₁ $ e₂) = resp2 _$_ (reneq eq e₁) (reneq eq e₂)
  reneq eq zero = Refl
  reneq eq (suc e) = resp suc (reneq eq e)
  reneq eq (rec e e₀ es) = resp3 rec (reneq eq e) (reneq eq e₀) (reneq (wkeq eq) es)

  wkid : ∀{Γ A C} (x : A ∈ C :: Γ) → wk renId x ≡ renId x
  wkid Z = Refl
  wkid (S n) = Refl

  renid : ∀{Γ A} (e : TExp Γ A) → ren renId e ≡ id _ e
  renid (var x) = Refl
  renid (Λ e) = resp Λ (reneq wkid e ≡≡ renid e)
  renid (e₁ $ e₂) = resp2 _$_ (renid e₁) (renid e₂)
  renid zero = Refl
  renid (suc e) = resp suc (renid e)
  renid (rec e e₀ es) = resp3 rec (renid e) (renid e₀)
                        (reneq wkid es ≡≡ renid es)

  wkcomp : ∀ {B Γ Γ'}(f : TRen Γ Γ')(g : TRen B Γ) {C A} (x : A ∈ (C :: B)) →
             wk (renComp f g) x ≡ (wk f o wk g) x
  wkcomp f g Z = Refl
  wkcomp f g (S n) = Refl

  rencomp : ∀ {B Γ Γ'}(f : TRen Γ Γ')(g : TRen B Γ) {A} (e : TExp B A) →
             ren (renComp f g) e ≡ (ren f o ren g) e
  rencomp f g (var x) = Refl
  rencomp f g (Λ e) = resp Λ (reneq (wkcomp f g) e
                              ≡≡ (rencomp (wk f) (wk g) e))
  rencomp f g (e₁ $ e₂) = resp2 _$_ (rencomp f g e₁) (rencomp f g e₂)
  rencomp f g zero = Refl
  rencomp f g (suc e) = resp suc (rencomp f g e)
  rencomp f g (rec e e₀ es) = resp3 rec (rencomp f g e) (rencomp f g e₀)
                              (reneq (wkcomp f g) es
                               ≡≡ (rencomp (wk f) (wk g) es))

  Sub≡ : ∀ {Γ Γ'}(f g : TSubst Γ Γ') → Set
  Sub≡ f g = ∀ {A} x → f {A} x ≡ g {A} x

  lifteq : ∀{Γ Γ' A} {f g : TSubst Γ Γ'} → Sub≡ f g → Sub≡ (liftγ {A = A} f) (liftγ g)
  lifteq eq Z = Refl
  lifteq eq (S n) = resp (λ x → ren S x) (eq n)

  -- Prove that applying equal substs produces equal outputs
  subeq : ∀{Γ Γ' A} {f g : TSubst Γ Γ'} → Sub≡ f g → (e : TExp Γ A) → ssubst f e ≡ ssubst g e
  subeq eq (var x) = eq x
  subeq eq (Λ e) = resp Λ (subeq (lifteq eq) e)
  subeq eq (e₁ $ e₂) = resp2 _$_ (subeq eq e₁) (subeq eq e₂)
  subeq eq zero = Refl
  subeq eq (suc e) = resp suc (subeq eq e)
  subeq eq (rec e e₀ es) = resp3 rec (subeq eq e) (subeq eq e₀) (subeq (lifteq eq) es)

  -- Theorems about renaming and substitution
  renwklift : ∀{K Γ Δ C}(f : TRen Γ Δ)(g : TSubst K Γ){A}(x : A ∈ (C :: K)) →
          (ren (wk f) o (liftγ g)) x ≡ liftγ (ren f o g) x
  renwklift f g Z = Refl
  renwklift f g (S n) = symm (rencomp (wk f) S (g n)) ≡≡ rencomp S f (g n)

  rensub : ∀{B Γ Δ}(f : TRen Γ Δ)(g : TSubst B Γ){A}(e : TExp B A) →
          (ren f o ssubst g) e ≡ ssubst (ren f o g) e
  rensub f g (var x) = Refl
  rensub f g (Λ e) = resp Λ ((rensub (wk f) (liftγ g) e) ≡≡
                             subeq (renwklift f g) e)
  rensub f g (e₁ $ e₂) = resp2 _$_ (rensub f g e₁) (rensub f g e₂)
  rensub f g zero = Refl
  rensub f g (suc e) = resp suc (rensub f g e)
  rensub f g (rec e e₀ es) = resp3 rec (rensub f g e) (rensub f g e₀)
                              ((rensub (wk f) (liftγ g) es) ≡≡
                               subeq (renwklift f g) es)

  liftwk : ∀{K Γ Δ C}(f : TSubst Γ Δ)(g : TRen K Γ){A}(x : A ∈ (C :: K)) →
                     (liftγ f o wk g) x ≡ liftγ (f o g) x
  liftwk f g Z = Refl
  liftwk f g (S n) = Refl

  subren : ∀{B Γ Δ}(f : TSubst Γ Δ)(g : TRen B Γ){A}(e : TExp B A) →
          (ssubst f o ren g) e ≡ ssubst (f o g) e
  subren f g (var x) = Refl
  subren f g (Λ e) = resp Λ ((subren (liftγ f) (wk g) e) ≡≡
                             subeq (liftwk f g) e)
  subren f g (e₁ $ e₂) = resp2 _$_ (subren f g e₁) (subren f g e₂)
  subren f g zero = Refl
  subren f g (suc e) = resp suc (subren f g e)
  subren f g (rec e e₀ es) = resp3 rec (subren f g e) (subren f g e₀)
                             ((subren (liftγ f) (wk g) es) ≡≡
                              subeq (liftwk f g) es)

  -- first monad law, the second holds definitionally
  liftid : ∀{Γ A C} (x : A ∈ C :: Γ) → liftγ emptyγ x ≡ emptyγ x
  liftid Z = Refl
  liftid (S n) = Refl

  subid : ∀{Γ}{A} (e : TExp Γ A) → ssubst emptyγ e ≡ id _ e
  subid (var x) = Refl
  subid (Λ e) = resp Λ (subeq liftid e ≡≡ subid e)
  subid (e₁ $ e₂) = resp2 _$_ (subid e₁) (subid e₂)
  subid zero = Refl
  subid (suc e) = resp suc (subid e)
  subid (rec e e₀ es) = resp3 rec (subid e) (subid e₀)
                        (subeq liftid es ≡≡ subid es)

  -- third monad law
  liftcomp : ∀ {B Γ Γ'}(f : TSubst Γ Γ')(g : TSubst B Γ) {C A} (x : A ∈ (C :: B)) →
             liftγ (subComp f g) x ≡ (ssubst (liftγ f) o liftγ g) x
  liftcomp f g Z = Refl
  liftcomp f g (S n) = rensub S f (g n) ≡≡ symm (subren (liftγ f) S (g n))

  subcomp : ∀{B Γ Γ'}(f : TSubst Γ Γ')(g : TSubst B Γ){A}(t : TExp B A) →
         ssubst (subComp f g) t ≡ (ssubst f o ssubst g) t
  subcomp f g (var x) = Refl
  subcomp f g (Λ e) = resp Λ (subeq (liftcomp f g) e
                              ≡≡ (subcomp (liftγ f) (liftγ g) e))
  subcomp f g (e₁ $ e₂) = resp2 _$_ (subcomp f g e₁) (subcomp f g e₂)
  subcomp f g zero = Refl
  subcomp f g (suc e) = resp suc (subcomp f g e)
  subcomp f g (rec e e₀ es) = resp3 rec (subcomp f g e) (subcomp f g e₀)
                              (subeq (liftcomp f g) es
                               ≡≡ (subcomp (liftγ f) (liftγ g) es))

  -- The lemma about combining substitutions that we are actually
  -- going to need. Being able to prove this lemma was the cause
  -- of most of the grief during this proof.
  combine-subst-noob : ∀ {Γ A C} → (γ : TSubst Γ []) →
                    (e : TExp (A :: Γ) C) →
                    (e' : TCExp A) →
                    ssubst (extendγ γ e') e ≡
                    ssubst (singγ e') (ssubst (liftγ γ) e)
  combine-subst-noob γ e e' = subcomp (singγ e') (liftγ γ) e

  -- A lemma we need to define our relations on substs that respect relns
  extend-nofail-s : ∀{Γ Γ' A B} → (γ : TSubst Γ Γ') → (e : TExp Γ' A) → (n : B ∈ Γ) →
                    γ n ≡ (extendγ γ e) (S n)
  extend-nofail-s γ e n = symm (subren (singγ e) S (γ n) ≡≡ subid (γ n))

  -- A closed subst is the identity
  closed-is-empty-ren : (γ : TRen [] []) → Ren≡ γ renId
  closed-is-empty-ren γ ()
  closed-is-empty : (γ : TSubst [] []) → Sub≡ γ emptyγ
  closed-is-empty γ ()

  -- A substitution made on a closed term is the identity substitution
  closed-ren : ∀{A} → (γ : TRen [] []) → (e : TCExp A) → ren γ e ≡ e
  closed-ren γ e = reneq (closed-is-empty-ren γ) e ≡≡ renid e
  closed-subst : ∀{A} → (γ : TSubst [] []) → (e : TCExp A) → ssubst γ e ≡ e
  closed-subst γ e = subeq (closed-is-empty γ) e ≡≡ subid e

  -- lift of a closed subst, also identity - feel like there is a nicer way to do this
  lift-closed-is-empty : ∀{A} (γ : TSubst [] []) → Sub≡ (liftγ {A = A} γ) emptyγ
  lift-closed-is-empty γ Z = Refl
  lift-closed-is-empty γ (S x) = resp (ren _) (closed-is-empty γ x)
  lift-closed-subst : ∀{A B} → (γ : TSubst [] []) → (e : TExp (B :: []) A) → ssubst (liftγ γ) e ≡ e
  lift-closed-subst γ e = subeq (lift-closed-is-empty γ) e ≡≡ subid e

  compose-subst-noob : ∀{Γ} {C} → (γ : TSubst Γ []) →
                        (e : TExp Γ C) →
                        {A : TTp} → (x : A ∈ C :: Γ) →
                        subComp (singγ (ssubst γ e)) (liftγ γ) x ≡
                        subComp γ (singγ e) x
  compose-subst-noob γ e Z = Refl
  compose-subst-noob γ e (S x) = subren (singγ (ssubst γ e)) (λ y → S y) (γ x) ≡≡ subid (γ x)

  drop-fix : ∀{Γ A} → (γ : TSubst (A :: Γ) []) → Sub≡ γ (subComp (singγ (γ Z)) (liftγ (dropγ γ)))
  drop-fix γ Z = Refl
  drop-fix γ (S x) = symm (subren (singγ (γ Z)) S (γ (S x)) ≡≡ subid (γ (S x)))

open SubstTheory public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Half adjoint equivalences
------------------------------------------------------------------------

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

module Function.HalfAdjointEquivalence where

open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Level
open import Relation.Binary.PropositionalEquality

-- Half adjoint equivalences (see the HoTT book).

record _≃_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  field
    to               : A → B
    from             : B → A
    left-inverse-of  : ∀ x → from (to x) ≡ x
    right-inverse-of : ∀ x → to (from x) ≡ x
    left-right       :
      ∀ x → cong to (left-inverse-of x) ≡ right-inverse-of (to x)

  -- Half adjoint equivalences can be turned into inverses.

  inverse : A ↔ B
  inverse = Inv.inverse to from left-inverse-of right-inverse-of

  -- The forward direction of a half adjoint equivalence is injective.

  injective : ∀ {x y} → to x ≡ to y → x ≡ y
  injective {x} {y} to-x≡to-y =
    x            ≡⟨ sym (left-inverse-of _) ⟩
    from (to x)  ≡⟨ cong from to-x≡to-y ⟩
    from (to y)  ≡⟨ left-inverse-of _ ⟩
    y            ∎
    where
    open ≡-Reasoning

-- Inverses can be turned into half adjoint equivalences.
--
-- (This proof is based on one in the HoTT book.)

↔→≃ : ∀ {a b} {A : Set a} {B : Set b} → A ↔ B → A ≃ B
↔→≃ A↔B = record
  { to               = to   ⟨$⟩_
  ; from             = from ⟨$⟩_
  ; left-inverse-of  = left-inverse-of
  ; right-inverse-of = right-inverse-of
  ; left-right       = left-right
  }
  where
  open ≡-Reasoning
  open module A↔B = Inverse A↔B using (to; from; left-inverse-of)

  right-inverse-of : ∀ x → to ⟨$⟩ (from ⟨$⟩ x) ≡ x
  right-inverse-of x =
    to ⟨$⟩ (from ⟨$⟩ x)                      ≡⟨ sym (A↔B.right-inverse-of _) ⟩
    to ⟨$⟩ (from ⟨$⟩ (to ⟨$⟩ (from ⟨$⟩ x)))  ≡⟨ cong (to ⟨$⟩_) (left-inverse-of _) ⟩
    to ⟨$⟩ (from ⟨$⟩ x)                      ≡⟨ A↔B.right-inverse-of _ ⟩
    x                                        ∎

  left-right :
    ∀ x →
    cong (to ⟨$⟩_) (left-inverse-of x) ≡ right-inverse-of (to ⟨$⟩ x)
  left-right x =
    cong (to ⟨$⟩_) (left-inverse-of x)               ≡⟨⟩

    trans refl (cong (to ⟨$⟩_) (left-inverse-of _))  ≡⟨ cong (λ p → trans p (cong (to ⟨$⟩_) _))
                                                          (sym (trans-symˡ (A↔B.right-inverse-of _))) ⟩
    trans (trans (sym (A↔B.right-inverse-of _))
               (A↔B.right-inverse-of _))
      (cong (to ⟨$⟩_) (left-inverse-of _))           ≡⟨ trans-assoc (sym (A↔B.right-inverse-of _)) ⟩

    trans (sym (A↔B.right-inverse-of _))
      (trans (A↔B.right-inverse-of _)
         (cong (to ⟨$⟩_) (left-inverse-of _)))       ≡⟨ cong (trans (sym (A↔B.right-inverse-of _))) lemma ⟩

    trans (sym (A↔B.right-inverse-of _))
      (trans (cong (to ⟨$⟩_) (left-inverse-of _))
         (trans (A↔B.right-inverse-of _) refl))      ≡⟨⟩

    right-inverse-of (to ⟨$⟩ x)                      ∎
    where
    lemma =
      trans (A↔B.right-inverse-of _)
        (cong (to ⟨$⟩_) (left-inverse-of _))             ≡⟨ cong (trans (A↔B.right-inverse-of _)) (sym (cong-id _)) ⟩

      trans (A↔B.right-inverse-of _)
        (cong id (cong (to ⟨$⟩_) (left-inverse-of _)))   ≡⟨ sym (naturality A↔B.right-inverse-of) ⟩

      trans (cong ((to ⟨$⟩_) ∘ (from ⟨$⟩_))
                 (cong (to ⟨$⟩_) (left-inverse-of _)))
        (A↔B.right-inverse-of _)                         ≡⟨ cong (λ p → trans p (A↔B.right-inverse-of _))
                                                              (sym (cong-∘ _)) ⟩
      trans (cong ((to ⟨$⟩_) ∘ (from ⟨$⟩_) ∘ (to ⟨$⟩_))
                      (left-inverse-of _))
        (A↔B.right-inverse-of _)                         ≡⟨ cong (λ p → trans p (A↔B.right-inverse-of _))
                                                              (cong-∘ _) ⟩
      trans (cong (to ⟨$⟩_)
                 (cong ((from ⟨$⟩_) ∘ (to ⟨$⟩_))
                    (left-inverse-of _)))
        (A↔B.right-inverse-of _)                         ≡⟨ cong (λ p → trans (cong (to ⟨$⟩_) p) _)
                                                              (cong-≡id left-inverse-of) ⟩
      trans (cong (to ⟨$⟩_) (left-inverse-of _))
        (A↔B.right-inverse-of _)                         ≡⟨ cong (trans (cong (to ⟨$⟩_) (left-inverse-of _)))
                                                              (sym (trans-reflʳ _)) ⟩
      trans (cong (to ⟨$⟩_) (left-inverse-of _))
        (trans (A↔B.right-inverse-of _) refl)            ∎


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

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive
open import Agda.Primitive.Cubical
open import Agda.Builtin.Bool

variable
  a p         : Level
  A           : Set a
  P           : A → Set p
  x y : A

refl : x ≡ x
refl {x = x} = λ _ → x

data Interval : Set where
  left right : Interval
  line : left ≡ right

h2 : Bool → Interval
h2 true = left
h2 false = right

-- `left` and `right` are distinct canonical forms,
-- so `h2 ? = left` imples `? = true`.
--
-- Added this test to make sure we do not always give up on
-- injectivity when targeting a HIT.
_ : h2 _ ≡ left
_ = refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --sized-types #-}
module SList.Order {A : Set}(_≤_ : A → A → Set) where

open import List.Sorted _≤_
open import Size
open import SList

data _*≤_ : {ι : Size} → A → SList A {ι} → Set where
  genx : {ι : Size}{b : A}
                   → (_*≤_) {↑ ι} b snil
  gecx : {ι : Size}{b x : A}{xs : SList A {ι}}
                   → b ≤ x
                   → b *≤ xs
                   → b *≤ (x ∙ xs)

data _≤*_ : {ι : Size} → SList A {ι} → A → Set where
  lenx : {ι : Size}{t : A}
                   → (_≤*_) {↑ ι} snil t
  lecx : {ι : Size}{x t : A}{xs : SList A {ι}}
                   → x ≤ t
                   → xs ≤* t
                   → (x ∙ xs) ≤* t

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --copatterns #-}

module examplesPaperJFP.IOGraphicsLib where

open import Data.Bool.Base
open import Data.Char.Base
open import Data.Nat.Base hiding (_⊓_; _+_; _*_)
open import Data.List.Base hiding (_++_)
open import Data.Integer.Base hiding (suc)
open import Data.String.Base
open import Data.Maybe.Base

open import Function

open import Size

open import SizedIO.Base
open import SizedIO.IOGraphicsLib hiding (GraphicsCommands; GraphicsResponses; GraphicsInterface; IOGraphics) renaming (Size to WindowSize)

open import NativeInt --PrimTypeHelpers
open import NativeIO

data GraphicsCommands  :  Set where
  getWindowEvent  :  Window  →  GraphicsCommands
  openWindow      :  String  →  Maybe Point  →  ℕ  → ℕ
                             →  RedrawMode   →  Maybe Word32
                             →  GraphicsCommands
  closeWindow     :  Window  →  GraphicsCommands
  drawInWindow    :  Window  →  Graphic → GraphicsCommands

GraphicsResponses  :                       GraphicsCommands → Set
GraphicsResponses  (getWindowEvent _)        =  Event
GraphicsResponses  (openWindow _ _ _ _ _ _)  =  Window
GraphicsResponses  (closeWindow _)           =  Unit
GraphicsResponses  (drawInWindow _ _)        =  Unit

GraphicsInterface            :  IOInterface
Command   GraphicsInterface  =  GraphicsCommands
Response  GraphicsInterface  =  GraphicsResponses

IOGraphics : Size → Set → Set
IOGraphics i = IO GraphicsInterface i

translateNative : (c : GraphicsCommands) → NativeIO (GraphicsResponses c)

translateNative  (getWindowEvent w)               =  nativeGetWindowEvent w
translateNative  (openWindow str point n1 n2 m w)  =  nativeOpenWindowExNat str point n1 n2 m w
translateNative  (closeWindow w)                  =  nativeCloseWindow w
translateNative  (drawInWindow w g)               =  nativeDrawInWindow w g

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module Cubical.HITs.Modulo.Base where

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

open import Cubical.Data.Empty
open import Cubical.Data.Fin
open import Cubical.Data.Nat
open import Cubical.Data.Unit renaming (Unit to ⊤)

open import Cubical.Relation.Nullary

NonZero : ℕ → Type₀
NonZero 0 = ⊥
NonZero _ = ⊤

private
  variable
    ℓ : Level
    k : ℕ

-- The Modulo type is similar to the Fin type, but instead of being
-- inhabited by canonical values, the inhabitants are all naturals,
-- and paths are added between numbers that have the same residue.
--
-- This representation makes it easier to do certain arithmetic
-- without changing the modulus. For instance, we can just add any
-- natural to a Modulo k to get another, whereas with Fin k, we must
-- calculate the canonical representative.
--
-- The reason the path constructor is guarded is to avoid adding
-- non-trivial path structure to the k=0 case. If it were not guarded,
-- each `Modulo 0` would become like the circle, and guarding the
-- constructor is somewhat easier to work with than truncation.
--
-- Note also that unlike `Fin 0`, `Modulo 0` is equivalent to the naturals.
data Modulo (k : ℕ) : Type₀ where
  embed : (n : ℕ) → Modulo k
  pre-step : NonZero k → (n : ℕ) → embed n ≡ embed (k + n)

-- When we are working with k = suc k₀, the `step` alias is much
-- we can use this alias.
pattern step n i = pre-step _ n i

-- Helper to avoid having to case on `k` in certain places.
ztep : ∀{k} n → Path (Modulo k) (embed n) (embed (k + n))
ztep {0}     n = refl
ztep {suc k} n = step n

-- The standard eliminator for `Modulo`.
elim
  : (P : ∀ k → Modulo k → Type ℓ)
  → (e : ∀ k n → P k (embed n))
  → (st : ∀ k n → PathP (λ i → P (suc k) (step n i)) (e (suc k) n) (e (suc k) (suc k + n)))
  → (m : Modulo k) → P k m
elim P e st (embed n) = e _ n
elim {k = suc k} P e st (step n i) = st k n i

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
------------------------------------------------------------------------
-- The list container
------------------------------------------------------------------------

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

open import Equality

module Container.List
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_; module _⇔_)
open import Prelude as P hiding (List; []; _∷_; id; _∘_)

open import Bag-equivalence eq
  using () renaming (_≈-bag_ to _≈-bagL_; _∈_ to _∈L_; Any to AnyL)
open import Bijection eq using (_↔_; module _↔_; Σ-≡,≡↔≡)
open import Container eq
open import Fin eq
open import Function-universe eq
open import H-level.Closure eq
import List eq as L
open import Surjection eq using (_↠_)

------------------------------------------------------------------------
-- The type

-- Lists.

List : Container lzero
List = ℕ ▷ Fin

------------------------------------------------------------------------
-- The definitions of lists and bag equivalence for lists given in
-- Container/Container.List and in Prelude/Bag-equivalence are closely
-- related

-- There is a split surjection from ⟦ List ⟧ A to P.List A.

List↠List : {A : Type} → ⟦ List ⟧ A ↠ P.List A
List↠List {A} = record
  { logical-equivalence = record
    { to   = uncurry to
    ; from = from
    }
  ; right-inverse-of = to∘from
  }
  where
  to : (n : ℕ) → (Fin n → A) → P.List A
  to zero    f = P.[]
  to (suc n) f = P._∷_ (f fzero) (to n (f ∘ fsuc))

  from = λ xs → (L.length xs , L.index xs)

  to∘from : ∀ xs → uncurry to (from xs) ≡ xs
  to∘from P.[]         = refl _
  to∘from (P._∷_ x xs) = cong (P._∷_ x) (to∘from xs)

-- If we assume that equality of functions is extensional, then we can
-- also prove that the two definitions are isomorphic.

List↔List : Extensionality lzero lzero →
            {A : Type} → ⟦ List ⟧ A ↔ P.List A
List↔List ext {A} = record
  { surjection      = List↠List
  ; left-inverse-of = uncurry from∘to
  }
  where
  open _↠_ List↠List

  from∘to : ∀ n f → from (to (n , f)) ≡ (n , f)
  from∘to zero    f = cong (_,_ _) (apply-ext ext λ ())
  from∘to (suc n) f =
    (suc (L.length (to xs)) , L.index (P._∷_ x (to xs)))  ≡⟨ elim¹ (λ {ys} _ → _≡_ {A = ⟦ List ⟧ A}
                                                                                (suc (L.length (to xs)) , L.index (P._∷_ x (to xs)))
                                                                                (suc (proj₁ ys) , [ (λ _ → x) , proj₂ ys ]))
                                                                   (cong (suc (L.length (to xs)) ,_) $ apply-ext ext
                                                                      [ (λ _ → refl _) , (λ _ → refl _) ])
                                                                   (from∘to n (f ∘ inj₂)) ⟩
    (suc n                  , [ (λ _ → x) , f ∘ inj₂ ])   ≡⟨ cong (_,_ _) (apply-ext ext [ (λ _ → refl _) , (λ _ → refl _) ]) ⟩∎
    (suc n                  , f)                          ∎
    where
    x  = f (inj₁ tt)
    xs = (n , f ∘ inj₂)

-- The two definitions of Any are isomorphic (both via "to" and
-- "from").

Any↔Any-to : {A : Type} (P : A → Type) (xs : ⟦ List ⟧ A) →
             Any P xs ↔ AnyL P (_↠_.to List↠List xs)
Any↔Any-to {A} P = uncurry Any↔Any-to′
  where
  Any↔Any-to′ : (n : ℕ) (lkup : Fin n → A) →
                Any {C = List} P (n , lkup) ↔
                AnyL P (_↠_.to List↠List (n , lkup))
  Any↔Any-to′ zero lkup =
    (∃ λ (p : Fin zero) → P (lkup p))  ↔⟨ ∃-Fin-zero _ ⟩
    ⊥                                  □
  Any↔Any-to′ (suc n) lkup =
    (∃ λ (p : Fin (suc n)) → P (lkup p))                          ↔⟨ ∃-Fin-suc _ ⟩
    P (lkup fzero) ⊎ Any {C = List} P (n , lkup ∘ fsuc)           ↔⟨ id ⊎-cong Any↔Any-to′ n (lkup ∘ fsuc) ⟩
    P (lkup fzero) ⊎ AnyL P (_↠_.to List↠List (n , lkup ∘ fsuc))  □

Any-from↔Any : {A : Type} (P : A → Type) (xs : P.List A) →
               Any P (_↠_.from List↠List xs) ↔ AnyL P xs
Any-from↔Any P P.[] =
  (∃ λ (p : Fin zero) → P (L.index P.[] p))  ↔⟨ ∃-Fin-zero _ ⟩
  ⊥                                          □
Any-from↔Any P (P._∷_ x xs) =
  (∃ λ (p : Fin (suc (L.length xs))) → P (L.index (P._∷_ x xs) p))  ↔⟨ ∃-Fin-suc _ ⟩
  P x ⊎ Any {C = List} P (_↠_.from List↠List xs)                    ↔⟨ id ⊎-cong Any-from↔Any P xs ⟩
  P x ⊎ AnyL P xs                                                   □

-- The definition of bag equivalence in Bag-equivalence and the one in
-- Container, instantiated with the List container, are logically
-- equivalent (both via "to" and "from").

≈-⇔-to-≈-to :
  {A : Type} {xs ys : ⟦ List ⟧ A} →
  xs ≈-bag ys ⇔ _↠_.to List↠List xs ≈-bagL _↠_.to List↠List ys
≈-⇔-to-≈-to {xs = xs} {ys} = record
  { to   = λ xs≈ys z →
             z ∈L (_↠_.to List↠List xs)  ↔⟨ inverse $ Any↔Any-to _ xs ⟩
             z ∈ xs                      ↔⟨ xs≈ys z ⟩
             z ∈ ys                      ↔⟨ Any↔Any-to _ ys ⟩
             z ∈L (_↠_.to List↠List ys)  □
  ; from = λ xs≈ys z →
             z ∈ xs                      ↔⟨ Any↔Any-to _ xs ⟩
             z ∈L (_↠_.to List↠List xs)  ↔⟨ xs≈ys z ⟩
             z ∈L (_↠_.to List↠List ys)  ↔⟨ inverse $ Any↔Any-to _ ys ⟩
             z ∈ ys                      □
  }

≈-⇔-from-≈-from :
  {A : Type} {xs ys : P.List A} →
  xs ≈-bagL ys ⇔ _↠_.from List↠List xs ≈-bag _↠_.from List↠List ys
≈-⇔-from-≈-from {xs = xs} {ys} = record
  { to   = λ xs≈ys z →
             z ∈ (_↠_.from List↠List xs)  ↔⟨ Any-from↔Any _ xs ⟩
             z ∈L xs                      ↔⟨ xs≈ys z ⟩
             z ∈L ys                      ↔⟨ inverse $ Any-from↔Any _ ys ⟩
             z ∈ (_↠_.from List↠List ys)  □
  ; from = λ xs≈ys z →
             z ∈L xs                      ↔⟨ inverse $ Any-from↔Any _ xs ⟩
             z ∈ (_↠_.from List↠List xs)  ↔⟨ xs≈ys z ⟩
             z ∈ (_↠_.from List↠List ys)  ↔⟨ Any-from↔Any _ ys ⟩
             z ∈L ys                      □
  }

------------------------------------------------------------------------
-- Constructors

[] : {A : Type} → ⟦ List ⟧ A
[] = (zero , λ ())

infixr 5 _∷_

_∷_ : {A : Type} → A → ⟦ List ⟧ A → ⟦ List ⟧ A
x ∷ (n , lkup) = (suc n , [ (λ _ → x) , lkup ])

-- Even if we don't assume extensionality we can prove that
-- intensionally distinct implementations of the constructors are bag
-- equivalent.

[]≈ : {A : Type} {lkup : _ → A} →
      _≈-bag_ {C₂ = List} [] (zero , lkup)
[]≈ _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (() , _) }
      ; from = λ { (() , _) }
      }
    ; right-inverse-of = λ { (() , _) }
    }
  ; left-inverse-of = λ { (() , _) }
  }

∷≈ : ∀ {A : Type} {n} {lkup : _ → A} →
     _≈-bag_ {C₂ = List}
             (lkup (inj₁ tt) ∷ (n , lkup ∘ inj₂))
             (suc n , lkup)
∷≈ _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (inj₁ tt , eq) → (inj₁ tt , eq)
                 ; (inj₂ s  , eq) → (inj₂ s  , eq)
                 }
      ; from = λ { (inj₁ tt , eq) → (inj₁ tt , eq)
                 ; (inj₂ s  , eq) → (inj₂ s  , eq)
                 }
      }
    ; right-inverse-of = λ { (inj₁ tt , eq) → refl _
                           ; (inj₂ s  , eq) → refl _
                           }
    }
  ; left-inverse-of = λ { (inj₁ tt , eq) → refl _
                        ; (inj₂ s  , eq) → refl _
                        }
  }

-- Any lemmas for the constructors.

Any-[] : {A : Type} (P : A → Type) →
         Any P [] ↔ ⊥₀
Any-[] _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (() , _) }
      ; from = λ ()
      }
    ; right-inverse-of = λ ()
    }
  ; left-inverse-of = λ { (() , _) }
  }

Any-∷ : ∀ {A : Type} (P : A → Type) {x xs} →
        Any P (x ∷ xs) ↔ P x ⊎ Any P xs
Any-∷ _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (inj₁ tt , eq) → inj₁ eq
                 ; (inj₂ s  , eq) → inj₂ (s , eq)
                 }
      ; from = λ { (inj₁ eq)       → (inj₁ tt , eq)
                 ; (inj₂ (s , eq)) → (inj₂ s  , eq)
                 }
      }
    ; right-inverse-of = λ { (inj₁ eq)       → refl _
                           ; (inj₂ (s , eq)) → refl _
                           }
    }
  ; left-inverse-of = λ { (inj₁ tt , eq) → refl _
                        ; (inj₂ s  , eq) → refl _
                        }
  }

------------------------------------------------------------------------
-- More functions

-- A fold for lists. (Well, this is not a catamorphism, it is a
-- paramorphism.)

fold : {A B : Type} → B → (A → ⟦ List ⟧ A → B → B) → ⟦ List ⟧ A → B
fold {A} {B} nl cns = uncurry fold′
  where
  fold′ : (n : ℕ) → (Fin n → A) → B
  fold′ zero    lkup = nl
  fold′ (suc n) lkup =
    cns (lkup fzero) (n , lkup ∘ fsuc) (fold′ n (lkup ∘ fsuc))

-- A lemma which can be used to prove properties about fold.
--
-- The "respects bag equivalence" argument could be omitted if
-- equality of functions were extensional.

fold-lemma : ∀ {A B : Type} {nl : B} {cns : A → ⟦ List ⟧ A → B → B}
             (P : ⟦ List ⟧ A → B → Type) →
             (∀ xs ys → xs ≈-bag ys → ∀ b → P xs b → P ys b) →
             P [] nl →
             (∀ x xs b → P xs b → P (x ∷ xs) (cns x xs b)) →
             ∀ xs → P xs (fold nl cns xs)
fold-lemma {A} {nl = nl} {cns} P resp P-nl P-cns = uncurry fold′-lemma
  where
  fold′-lemma : ∀ n (lkup : Fin n → A) →
                P (n , lkup) (fold nl cns (n , lkup))
  fold′-lemma zero    lkup = resp _ _ []≈ _ P-nl
  fold′-lemma (suc n) lkup = resp _ _ ∷≈ _ $
    P-cns _ _ _ $ fold′-lemma n (lkup ∘ fsuc)

-- Why have I included both fold and fold-lemma rather than simply a
-- dependent eliminator? I tried this, and could easily define the
-- functions I wanted to define. However, the functions were defined
-- together with (partial) correctness proofs, and were unnecessarily
-- hard to read. I wanted to be able to define functions which were
-- easy to read, like the _++_ function below, and then have the
-- option to prove properties about them, like Any-++.
--
-- Unfortunately this turned out to be harder than expected. When
-- proving the Any-++ lemma it seemed as if I had to prove that _++_
-- preserves bag equivalence in its first argument in order to
-- instantiate the "respects bag equivalence" argument. However, my
-- preferred proof of this property uses Any-++…
--
-- An alternative could be to assume that equality of functions is
-- extensional, in which case the "respects bag equivalence" argument
-- could be removed. Another option would be to listen to Conor
-- McBride and avoid higher-order representations of first-order data.

-- Append.

infixr 5 _++_

_++_ : {A : Type} → ⟦ List ⟧ A → ⟦ List ⟧ A → ⟦ List ⟧ A
xs ++ ys = fold ys (λ z _ zs → z ∷ zs) xs

-- An Any lemma for append.

Any-++ : ∀ {A : Type} (P : A → Type) xs ys →
         Any P (xs ++ ys) ↔ Any P xs ⊎ Any P ys
Any-++ P xs ys = fold-lemma
  (λ xs xs++ys → Any P xs++ys ↔ Any P xs ⊎ Any P ys)

  (λ us vs us≈vs us++ys hyp →
    Any P us++ys         ↔⟨ hyp ⟩
    Any P us ⊎ Any P ys  ↔⟨ _⇔_.to (∼⇔∼″ us vs) us≈vs P ⊎-cong id ⟩
    Any P vs ⊎ Any P ys  □)

  (Any P ys             ↔⟨ inverse ⊎-left-identity ⟩
   ⊥ ⊎ Any P ys         ↔⟨ inverse (Any-[] P) ⊎-cong id ⟩
   Any P [] ⊎ Any P ys  □)

  (λ x xs xs++ys ih →
     Any P (x ∷ xs++ys)           ↔⟨ Any-∷ P ⟩
     P x ⊎ Any P xs++ys           ↔⟨ id ⊎-cong ih ⟩
     P x ⊎ Any P xs ⊎ Any P ys    ↔⟨ ⊎-assoc ⟩
     (P x ⊎ Any P xs) ⊎ Any P ys  ↔⟨ inverse (Any-∷ P) ⊎-cong id ⟩
     Any P (x ∷ xs) ⊎ Any P ys    □)

  xs

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Music where

open import Data.Nat     using (ℕ; zero; suc; _+_; _*_; _≤_; _≤?_)
open import Data.Integer using (ℤ; +_)
open import Data.List    using (List; foldr; []; _∷_; reverse; sum; map)
open import Data.Product using (_×_; _,_)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Vec     using (Vec; []; _∷_; replicate; concat; zipWith; toList; _++_; foldr₁; take; drop) renaming (map to vmap)
open import Function     using (_∘_)

open import Data.Nat.Properties using (<⇒≤)
open import Relation.Nullary    using (yes; no)

open import Relation.Binary.PropositionalEquality using (sym; subst)

open import Nat
open import Note
open import Pitch
open import Interval

-- A point in the music grid, which can either be a tone,
-- a continuation of a previous tone, or a rest.
data Point : Set where
  tone : Pitch → Point
  hold : Pitch → Point
  rest : Point

data Melody (n : ℕ) : Set where
  melody : Vec Point n → Melody n

unmelody : {n : ℕ} → Melody n → Vec Point n
unmelody (melody ps) = ps

infixr 5 _m++_
_m++_ : {m n : ℕ} → Melody m → Melody n → Melody (m + n)
melody a m++ melody b = melody (a ++ b)

note→melody : (n : Note) → Melody (noteDuration n)
note→melody (tone zero    p) = melody []
note→melody (tone (suc d) p) = melody (tone p ∷ replicate (hold p))
note→melody (rest _)         = melody (replicate rest)

notes→melody : (ns : List Note) → Melody (sum (map noteDuration ns))
notes→melody []       = melody []
notes→melody (n ∷ ns) = note→melody n m++ notes→melody ns

pitches→melody : {n : ℕ} → (d : Duration) → (ps : Vec Pitch n) → Melody (n * d)
pitches→melody d ps = melody (concat (vmap (unmelody ∘ note→melody ∘ tone d) ps))

-- Assumes melody is well-formed in that a held note has the
-- same pitch as the note before it.
-- Does not consolidate rests.
melody→notes : {n : ℕ} → Melody n → List Note
melody→notes (melody m) = (reverse ∘ mn 0 ∘ reverse ∘ toList) m
  where mn : ℕ → List Point → List Note -- c is the number of held points
        mn c []            = []
        mn c (tone p ∷ ps) = tone (suc c) p ∷ mn 0 ps
        mn c (hold _ ∷ ps) = mn (suc c) ps
        mn c (rest ∷ ps)   = rest 1 ∷ mn 0 ps

transposePoint : ℤ → Point → Point
transposePoint k (tone p) = tone (transposePitch k p)
transposePoint k (hold p) = hold (transposePitch k p)
transposePoint k rest     = rest

transposeMelody : {n : ℕ} → ℤ → Melody n → Melody n
transposeMelody k = melody ∘ vmap (transposePoint k) ∘ unmelody

data Chord (n : ℕ) : Set where
  chord : Vec Point n → Chord n

unchord : {n : ℕ} → Chord n → Vec Point n
unchord (chord ps) = ps

-- We represent music as a v × d grid where v is the number of voices and d is the duration.
-- The primary representation is as parallel melodies (counterpoint).
data Counterpoint (v : ℕ) (d : ℕ): Set where
  cp : Vec (Melody d) v → Counterpoint v d

uncp : {v d : ℕ} → Counterpoint v d → Vec (Melody d) v
uncp (cp m) = m

-- An alternative representation of music is as a series of chords (harmonic progression).
data Harmony (v : ℕ) (d : ℕ): Set where
  harmony : Vec (Chord v) d → Harmony v d

unharmony : {v d : ℕ} → Harmony v d → Vec (Chord v) d
unharmony (harmony h) = h

pitches→harmony : {n : ℕ} (d : Duration) → (ps : Vec Pitch n) → Harmony n d
pitches→harmony zero    ps = harmony []
pitches→harmony (suc d) ps = harmony (chord (vmap tone ps) ∷ replicate (chord (vmap hold ps)))

pitchPair→Harmony : (d : Duration) → PitchPair → Harmony 2 d
pitchPair→Harmony d (p , q) = pitches→harmony d (p ∷ q ∷ [])

pitchInterval→Harmony : (d : Duration) → PitchInterval → Harmony 2 d
pitchInterval→Harmony d = pitchPair→Harmony d ∘ pitchIntervalToPitchPair

{-
pitchIntervalsToCounterpoint : PitchInterval → Counterpoint
pitchIntervalsToCounterpoint = pitchPairToCounterpoint ∘ pitchIntervalToPitchPair
-}

addEmptyVoice : {v d : ℕ} → Harmony v d → Harmony (suc v) d
addEmptyVoice (harmony h) = harmony (vmap (chord ∘ (rest ∷_) ∘ unchord) h)

infixl 5 _+H+_
_+H+_ : {v d d' : ℕ} → Harmony v d → Harmony v d' → Harmony v (d + d')
h +H+ h' = harmony (unharmony h ++ unharmony h')

foldIntoHarmony : {k n : ℕ} (ds : Vec Duration (suc k)) → (pss : Vec (Vec Pitch n) (suc k)) → Harmony n (foldr₁ _+_ ds)
foldIntoHarmony (d ∷ [])      (ps ∷ [])        = pitches→harmony d ps
foldIntoHarmony (d ∷ d' ∷ ds) (ps ∷ ps' ∷ pss) = (pitches→harmony d ps) +H+ (foldIntoHarmony (d' ∷ ds) (ps' ∷ pss))

-- matrix transposition
mtranspose : {A : Set}{m n : ℕ} → Vec (Vec A n) m → Vec (Vec A m) n
mtranspose []         = replicate []
mtranspose (xs ∷ xss) = zipWith _∷_ xs (mtranspose xss)

counterpoint→harmony : {v d : ℕ} → Counterpoint v d → Harmony v d
counterpoint→harmony = harmony ∘ vmap chord ∘ mtranspose ∘ vmap unmelody ∘ uncp

harmony→counterpoint : {v d : ℕ} → Harmony v d → Counterpoint v d
harmony→counterpoint = cp ∘ vmap melody ∘ mtranspose ∘ vmap unchord ∘ unharmony

-- Fix length of a melody, either truncating or padding with rests
fixLength : {m : ℕ} → (n : ℕ) → Melody m → Melody n
fixLength {m} n (melody ns) with <-∨-≥ n m
... | inj₁ n<m = melody (take n (subst (Vec Point) (sym (m+n-m=n n m {<⇒≤ n<m})) ns))
... | inj₂ m≤n = melody (subst (Vec Point) (m+n-m=n m n) (ns ++ replicate {n = n - m ⟨ m≤n ⟩} rest))

holdToTone : Point → Point
holdToTone (tone p) = tone p
holdToTone (hold p) = tone p
holdToTone rest     = rest

firstHoldToTone : {n : ℕ} → Melody n → Melody n
firstHoldToTone (melody [])       = melody []
firstHoldToTone (melody (x ∷ xs)) = melody (holdToTone x ∷ xs)

-- Drop points, but convert any held tones to tones.
dropPoints : {n : ℕ} → (m : ℕ) → Melody (m + n) → Melody n
dropPoints m = firstHoldToTone ∘ melody ∘ drop m ∘ unmelody

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module tests.String where

open import Prelude.IO
open import Prelude.List
open import Prelude.String
open import Prelude.Unit

testString : String
testString = "To boldly go where no man gone before"

printList : forall {A} -> (A -> IO Unit) -> List A -> IO Unit
printList p [] = return unit
printList p (x :: xs) =
    p x ,,
    printList p xs

main : IO Unit
main =
    putStrLn testString ,,
    printList printChar (fromString testString) ,,
    putStrLn "" ,,
    putStrLn (fromList (fromString testString)) ,,
    return unit

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe --without-K #-}
open import Relation.Binary
module Data.List.Membership.Setoid.Trans {a p} (S : Setoid a p) where
open Setoid S
open import Data.List.Membership.Setoid (S)
open import Data.List.Any

≈-trans-∈ : ∀ {x y xs} → x ≈ y → y ∈ xs → x ∈ xs
≈-trans-∈ x≈y (here px) = here (trans x≈y px)
≈-trans-∈ x≈y (there p) = there (≈-trans-∈ x≈y p)

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
-- {-# OPTIONS --no-coverage-check #-}
-- {-# OPTIONS -v tc.lhs:40 #-}
module FlexibleFunArity where

open import Common.Equality

data Bool : Set where true false : Bool

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

Case : {A : Set} → Maybe A → Set → Set → Set
Case nothing  B C = B
Case (just _) B C = C

sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool)
sample (just a) (just b) = true
sample (just a) nothing  = false
sample nothing           = true

g : Bool -> Bool -> Bool
g false true  = false
g true = \ x -> true
g false false = true
-- g true false = false -- Unreachable clause

testg1 : ∀ {x} → g true x ≡ true
testg1 = refl

testg2 : g false true ≡ false
testg2 = refl

testg3 : g false false ≡ true
testg3 = refl

T : Bool -> Set
T true  = Bool
T false = Bool -> Bool

f : (b : Bool) -> T b
f false true  = false
f false false = true
f true = true

testf1 : f true ≡ true
testf1 = refl

testf2 : f false true ≡ false
testf2 = refl

testf3 : f false false ≡ true
testf3 = refl

{- checking clause

  f false true

starts with

  f (b : Bool) : T b

splits on b

  f true   -- no match, discard
  f false  -- matches

instantiate type

  f false : T false = Bool -> Bool

extend clause

  f false (y : Bool) : Bool

split on y

  f false true  -- matches
  f false false -- no match, discard

done
-}

{- coverage check starts with

  f (x : Bool)

splits on x

  f true   -- finds clause 1
  f false

NEW: remaing clauses have bigger arity, so expands to

  f false (y : Bool)

splits on y

  f false true  -- finds clause 2
  f false false -- finds clause 3

done
-}

max_stars_repo_name: larrytheliquid/agda


text:
-- Andreas, 2019-02-23, issue #3578.
-- Preserve types as much as possible during pattern matching.
-- New unifier (from Agda 2.5.1) was normalizing too much.

-- {-# OPTIONS -v tc.lhs.unify:45 #-}

data Nat : Set where
  zero : Nat

postulate
  MustNotBeNamed : Set

A = MustNotBeNamed

data P : Nat → Set where
  z : A → P zero

test : ∀{n} → P n → Set
test (z x) = {!x!}   -- C-c C-,

-- EXPECTED:
--
-- Goal: Set
-- ——————————————
-- x : A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.HITs.SetTruncation.Base public
open import Cubical.HITs.SetTruncation.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Testing termination using subpatterns
module TerminationSubpattern where

-- a list with two different conses
data EOList (A : Set) : Set where
    Nil : EOList A
    ECons : A -> EOList A -> EOList A
    OCons : A -> EOList A -> EOList A

butLastWithDefault : {A : Set} -> A -> EOList A -> A
butLastWithDefault a Nil = a
butLastWithDefault a (ECons b l) = butLastWithDefault b l
butLastWithDefault a (OCons b l) = butLastWithDefault b l

-- a very stupid implementation:
butLastWithDefault' : {A : Set} -> A -> EOList A -> A
butLastWithDefault' a Nil = a
butLastWithDefault' a (ECons b Nil) = b
butLastWithDefault' a (OCons b Nil) = b
butLastWithDefault' a (ECons b (OCons c l)) = butLastWithDefault' b (OCons c l)
butLastWithDefault' a (ECons b (ECons c l)) = butLastWithDefault' b (ECons c l)
butLastWithDefault' a (OCons b (OCons c l)) = butLastWithDefault' b (OCons c l)
butLastWithDefault' a (OCons b (ECons c l)) = butLastWithDefault' b (ECons c l)

-- terminates, because, e.g. in the last line
--
--   ECons c l   is a subpattern of   OCons b (ECons c l)

-- another justification is with structured orders
-- if all constructors are considered equivalent

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Lemmachine.Runner where
{-# IMPORT Lemmachine.FFI #-}
open import Lemmachine.Resource
open import Lemmachine.Resource.Configure
open import Lemmachine.Request
open import Lemmachine.Response
open import Lemmachine.Utils
open import Lemmachine.Resolve
open import Data.Unit
open import Data.Nat
open import Data.String
open import Data.Function
open import Foreign.Haskell
open import IO.Primitive

private
  data Data-Request : Set where
    request :
      Method →
      Version →
      IP →
      LocalPath →
      Path →
      RawPath →
      PathTokens →
      RequestHeaders →
      Body →
      Cookie →
      QueryString →
      Port →
      Data-Request

  {-# COMPILED_DATA Data-Request
      Lemmachine.FFI.Request
      Lemmachine.FFI.Request
  #-}

  toRequest : Data-Request → Request
  toRequest (request
    method
    version
    peer
    dispPath
    path
    rawPath
    pathTokens
    headers
    body
    cookie
    queryString
    port
    ) = record {
      method = method
    ; version = version
    ; peer = peer
    ; dispPath = dispPath
    ; path = path
    ; rawPath = rawPath
    ; pathTokens = pathTokens
    ; headers = headers
    ; reqBody = body
    ; cookie = cookie
    ; queryString = queryString
    ; port = port
    }

  data Data-Response : Set where
    response : String → ResponseHeaders → String → Data-Response

  {-# COMPILED_DATA Data-Response
      Lemmachine.FFI.Response
      Lemmachine.FFI.Response
  #-}

  fromResponse : Response → Data-Response
  fromResponse resp = response
    (showStatus $ Response.status resp)
    (Response.headers resp)
    (Response.body resp)

  Data-resolve : Application → Data-Request → Data-Response
  Data-resolve app req = fromResponse $ app (toRequest req)

  postulate run : (Data-Request → Data-Response) → IO Unit
  {-# COMPILED run Lemmachine.FFI.run #-}

runResolve : Application → IO Unit
runResolve app = run $ Data-resolve app

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Common.MAlonzo where

open import Common.Prelude hiding (putStrLn)
open import Common.Coinduction

{-# IMPORT Data.Text.IO #-}

postulate
  putStrLn : ∞ String → IO Unit

{-# COMPILED putStrLn Data.Text.IO.putStrLn #-}

main = putStrLn (♯ "This is a dummy main routine.")

mainPrint : String → _
mainPrint s = putStrLn (♯ s)

mainPrintNat : Nat → _
mainPrintNat n = putStrLn (♯ (natToString n))


text:
import cedille-options
open import general-util
open import lib

module process-cmd
  (options : cedille-options.options)
  {mF : Set → Set}
  {{_ : monad mF}}
  (progress-update : string → 𝔹 → mF ⊤) where

--open import cedille-find
open import cedille-types
open import classify options {mF}
open import constants
open import conversion
open import ctxt
open import is-free
open import spans options {mF}
open import syntax-util
open import toplevel-state options {mF}
-- open import to-string

import cws-types
import cws

-- generate spans from the given comments-and-whitespace syntax tree
process-cwst-etys : cws-types.entities → spanM ⊤
process-cwst-ety : cws-types.entity → spanM ⊤
process-cwst-etys (cws-types.Entity ety etys) = (process-cwst-ety ety) ≫span process-cwst-etys etys
process-cwst-etys cws-types.EndEntity = spanMr triv
process-cwst-ety cws-types.EntityNonws = spanMr triv
process-cwst-ety (cws-types.EntityWs pi pi') = spanMr triv -- spanM-add (whitespace-span pi pi')
process-cwst-ety (cws-types.EntityComment pi pi') = spanM-add (comment-span pi pi')

process-cwst : toplevel-state → filepath → spanM toplevel-state
process-cwst s filename with include-elt.cwst (get-include-elt s filename)
process-cwst s filename | nothing = spanMr s
process-cwst s filename | just (cws-types.File etys) = process-cwst-etys etys ≫span spanMr s

process-t : Set → Set
process-t X = toplevel-state → X → (need-to-check : 𝔹) → spanM toplevel-state

check-and-add-params : posinfo → params → spanM (𝕃 (string × restore-def))
check-and-add-params pi' (ParamsCons p@(Decl pi1 pi1' me x atk pi2) ps') =
  check-tk atk ≫span
  spanM-add (Decl-span param pi1 x atk pi' {- make this span go to the end of the def, so nesting will work
                                              properly for computing the context in the frontend -}) ≫span
  add-tk' (me-erased me) pi1' x atk ≫=span λ mi →
  check-and-add-params pi' ps' ≫=span λ ms → spanMr ((x , mi) :: ms)
check-and-add-params _ ParamsNil = spanMr []

dont-check-and-add-params : posinfo → params → spanM (𝕃 (string × restore-def))
dont-check-and-add-params pi' (ParamsCons p@(Decl pi1 pi1' me x atk pi2) ps') =
  add-tk' (me-erased me) pi1' x atk ≫=span λ mi →
  dont-check-and-add-params pi' ps' ≫=span λ ms → spanMr ((x , mi) :: ms)
dont-check-and-add-params _ ParamsNil = spanMr []

optAs-posinfo-var : optAs → (posinfo × var) → spanM (posinfo × var)
optAs-posinfo-var NoOptAs = spanMr
optAs-posinfo-var (SomeOptAs pi x) orig = get-ctxt λ Γ →
  spanM-add (Import-module-span Γ orig ParamsNil [ not-for-navigation ] nothing) ≫span spanMr (pi , x)

add-params-kind : params → kind → kind
add-params-kind (ParamsCons (Decl pi pi' m v k'  pi'') ps) k =
  KndPi pi pi' v k' (add-params-kind ps k)
add-params-kind ParamsNil k = k

{-# TERMINATING #-}
process-consts : dataConsts → params → spanM ⊤
process-cmd : process-t cmd
process-cmds : process-t cmds
process-params : process-t (posinfo × params)
process-start : toplevel-state → filepath → (progress-name : string) → start → (need-to-check : 𝔹) → spanM toplevel-state
process-file : toplevel-state → filepath → (progress-name : string) → mF (toplevel-state × mod-info)

process-cmd (mk-toplevel-state ip fns is Γ) (DefTermOrType op (DefTerm pi x (SomeType tp) t) pi') tt {- check -} =
  set-ctxt Γ ≫span
  check-type tp (just star) ≫span
  let tp' = qualif-type Γ tp in
  check-term t (just tp') ≫span
  check-erased-margs t (just tp') ≫span
  get-ctxt (λ Γ →
    let Γ' = ctxt-term-def pi globalScope op x t tp' Γ in
      spanM-add (DefTerm-span Γ' pi x checking (just tp) t pi' []) ≫span
      check-redefined pi x (mk-toplevel-state ip fns is Γ)
        (spanM-add (uncurry (Var-span Γ' pi x checking) (compileFail-in Γ t)) ≫span
         spanMr (mk-toplevel-state ip fns is Γ')))

process-cmd (mk-toplevel-state ip fns is Γ) (DefTermOrType op (DefTerm pi x (SomeType tp) t) pi') ff {- skip checking -} =
  let tp' = qualif-type Γ tp in
    check-redefined pi x (mk-toplevel-state ip fns is Γ)
      (spanMr (mk-toplevel-state ip fns is (ctxt-term-def pi globalScope op x t tp' Γ)))

process-cmd (mk-toplevel-state ip fns is Γ) (DefTermOrType op (DefTerm pi x NoType t) pi') _ =
  set-ctxt Γ ≫span
  check-term t nothing ≫=span λ mtp →
  check-erased-margs t nothing ≫span
  get-ctxt (λ Γ →
      let Γ' = maybe-else
                 (ctxt-term-udef pi globalScope op x t Γ)
                 (λ tp → ctxt-term-def pi globalScope op x t tp Γ) mtp in
      spanM-add (DefTerm-span Γ' pi x synthesizing mtp t pi' []) ≫span
      check-redefined pi x (mk-toplevel-state ip fns is Γ)
        (spanM-add (uncurry (Var-span Γ' pi x synthesizing) (compileFail-in Γ t)) ≫span
         spanMr (mk-toplevel-state ip fns is Γ')))

process-cmd (mk-toplevel-state ip fns is Γ) (DefTermOrType op (DefType pi x k tp) pi') tt {- check -} =
    set-ctxt Γ ≫span
    check-kind k ≫span
    let k' = qualif-kind Γ k in
    check-type tp (just k') ≫span
    get-ctxt (λ Γ →
      let Γ' = ctxt-type-def pi globalScope op x tp k' Γ in
        spanM-add (DefType-span Γ' pi x checking (just k) tp pi' []) ≫span
        check-redefined pi x (mk-toplevel-state ip fns is Γ)
          (spanM-add (TpVar-span Γ' pi x checking [] nothing) ≫span
           spanMr (mk-toplevel-state ip fns is Γ')))

process-cmd (mk-toplevel-state ip fns is Γ) (DefTermOrType op (DefType pi x k tp) pi') ff {- skip checking -} =
  let k' = qualif-kind Γ k in
    check-redefined pi x (mk-toplevel-state ip fns is Γ)
      (spanMr (mk-toplevel-state ip fns is (ctxt-type-def pi globalScope op x tp k' Γ)))

process-cmd (mk-toplevel-state ip fns is Γ) (DefKind pi x ps k pi') tt {- check -} =
  set-ctxt Γ ≫span
  check-and-add-params pi' ps ≫=span λ ms →
  check-kind k ≫span
  get-ctxt (λ Γ →
    let Γ' = ctxt-kind-def pi x ps k Γ in
      spanM-add (DefKind-span Γ' pi x k pi') ≫span
      check-redefined pi x (mk-toplevel-state ip fns is Γ)
       (spanM-add (KndVar-span Γ' (pi , x) (posinfo-plus-str pi x) ps checking [] nothing) ≫span
        spanMr (mk-toplevel-state ip fns is (ctxt-restore-info* Γ' ms))))

process-cmd (mk-toplevel-state ip fns is Γ) (DefKind pi x ps k pi') ff {- skip checking -} =
  set-ctxt Γ ≫span
  dont-check-and-add-params pi' ps ≫=span λ ms →
  get-ctxt (λ Γ →
    let Γ' = ctxt-kind-def pi x ps k Γ in
      check-redefined pi x (mk-toplevel-state ip fns is Γ)
        (spanMr (mk-toplevel-state ip fns is (ctxt-restore-info* Γ' ms))))

-- TODO ignore checking but still gen spans if need-to-check false?
process-cmd s (ImportCmd (Import pi op pi' x oa as pi'')) _ =
  let fnₒ = ctxt-get-current-filename (toplevel-state.Γ s)
      ie = get-include-elt s fnₒ in
  case trie-lookup (include-elt.import-to-dep ie) x of λ where
    nothing → spanM-add (Import-span pi "missing" pi'' [] (just ("File not found: " ^ x)))
      ≫span spanMr (set-include-elt s fnₒ (record ie {err = tt}))
    (just fnᵢ) Γ ss →
      process-file s fnᵢ x ≫=monad uncurry λ s _ →
        (let s-e = scope-file s fnₒ fnᵢ oa (qualif-args (toplevel-state.Γ s) as) in
         process-import op oa fnₒ fnᵢ (lookup-mod-params (toplevel-state.Γ s) fnᵢ) (maybe-else' (lookup-mod-params (toplevel-state.Γ s) fnₒ) ParamsNil id) ≫=span λ e →
         spanM-add (Import-span pi fnᵢ pi'' [] (snd s-e maybe-or e)) ≫span spanMr (fst s-e)) Γ ss
  where
  -- When importing a file publicly, you may use any number of arguments as long as the
  -- parameters of the current module are not free in them.
  -- You may then use any number of single-variable parameters from the current module
  -- as arguments as long as they retain the same order as before and have no non-parameter
  -- arguments between them
  -- (so parameters A, B, C, ..., Z can be used as arguments ∙ C ∙ X, but not ∙ X ∙ C)
  public-import-params-ok : params → args → err-m
  public-import-params-ok ps = h nothing where
    err = just "You can only use parameters for arguments to public imports if the are in order at the end"
    params-order : params → trie ℕ
    params-order = h 0 where
      h : ℕ → params → trie ℕ
      h n ParamsNil = empty-trie
      h n (ParamsCons (Decl _ _ me x atk _) ps) = trie-insert (h (suc n) ps) x n
    arg-var : arg → maybe var
    arg-var (TermArg me (Var pi x)) = just x
    arg-var (TypeArg (TpVar pi x)) = just x
    arg-var _ = nothing
    pso = params-order ps
    ps-free : arg → err-m → err-m
    ps-free a e = if ~ are-free-in-args check-erased pso (ArgsCons a ArgsNil) then e else err
    h : maybe ℕ → args → err-m
    h c (ArgsCons a as) =
      maybe-else' (arg-var a ≫=maybe trie-lookup pso)
        (maybe-else' c (ps-free a $ h nothing as) λ _ → err) λ aₙ →
      maybe-else' c (h (just aₙ) as) λ cₙ →
      if cₙ ≥ aₙ then err else h (just aₙ) as
    h n ArgsNil = nothing

  process-import : optPublic → optAs → (cur imp : filepath) → maybe params → params → spanM err-m
  process-import op oa fnₒ fnᵢ nothing _ = spanMr (just "Undefined module import (this probably shouldn't happen?)")
  -- process-import op oa fnₒ fnᵢ (just psᵢ) nothing = spanMr (just "Current module undefined (this shouldn't happen!)")
  process-import IsPublic (SomeOptAs _ _) fnₒ fnᵢ (just psᵢ) {-(just-} psₒ {-)-} = spanMr (just "Public import aren't allowed to be qualified")
  process-import op oa fnₒ fnᵢ (just psᵢ) {-(just-} psₒ {-)-} =
    optAs-posinfo-var oa (pi' , x) ≫=span λ pi-v →
    with-ctxt (toplevel-state.Γ s)
      (check-args-against-params (just (location-data (fnᵢ , first-position))) pi-v psᵢ as) ≫span
    spanMr (maybe-if (optPublic-is-public op) ≫maybe
            public-import-params-ok psₒ (qualif-args (toplevel-state.Γ s) as))

process-cmd (mk-toplevel-state ip fns is Γ) (DefDatatype dd@(Datatype pi pix x ps k cs _) pi') _  =
    set-ctxt Γ ≫span
    check-kind (add-params-kind ps k) ≫span --
    get-ctxt (λ Γ →
      let Γ' = ctxt-datatype-def pi x (qualif-params Γ ps) (qualif-kind Γ (add-params-kind ps k)) (Datatype pi pix x ps k cs pi') Γ in
        set-ctxt Γ'                                          ≫span
        spanM-add (DefDatatype-span pi pix x pi')            ≫span
        spanM-add (TpVar-span Γ' pix x checking [] nothing)  ≫span
        process-consts cs ps                                 ≫span
        get-ctxt (λ Γ →
          spanMr (mk-toplevel-state ip fns is Γ))) --(ctxt-restore-info* Γ ms))))

-- the call to ctxt-update-symbol-occurrences is for cedille-find functionality
process-cmds (mk-toplevel-state include-path files is Γ) (CmdsNext c cs) need-to-check =
  process-cmd (mk-toplevel-state include-path files is Γ) c need-to-check ≫=span λ s →
  process-cmds s cs need-to-check
process-cmds s CmdsStart need-to-check = set-ctxt (toplevel-state.Γ s) ≫span spanMr s

-- TODO ignore checking but still qualify if need-to-check false?
process-params s (pi , ps) need-to-check =
  set-ctxt (toplevel-state.Γ s) ≫span
  check-and-add-params pi ps ≫=span λ _ →
  spanM-set-params ps ≫span
  get-ctxt λ Γ →
  spanMr (record s {Γ = ctxt-add-current-params Γ})

process-start s filename pn (File pi0 is pi1 pi2 mn ps cs pi3) need-to-check =
  λ Γ ss → progress-update pn need-to-check ≫monad
  (process-cmds s (imps-to-cmds is) need-to-check ≫=span λ s →
   process-params s (pi0 , ps) need-to-check ≫=span λ s →
   process-cmds s cs need-to-check ≫=span λ s →
   process-cwst s filename ≫=span λ s →
     spanM-add (File-span (toplevel-state.Γ s) pi0 (posinfo-plus pi3 1) filename) ≫span
     let pi2' = posinfo-plus-str pi2 mn in
     spanM-add (Module-span pi2 pi2') ≫span
     spanM-add (Module-header-span pi1 pi2') ≫span
     spanMr s) Γ ss

{- process (type-check if necessary) the given file.
   We assume the given top-level state has a syntax tree associated with the file. -}
process-file s filename pn with get-include-elt s filename
process-file s filename pn | ie =
  proceed s (include-elt.ast ie) (set-need-to-add-symbols-to-context-include-elt ie ff) ≫=monad λ where
    (s , ie , ret-mod) → returnM (set-include-elt s filename ie , ret-mod)
        {- update the include-elt and the toplevel state (but we will push the updated include-elt into the toplevel state
           just above, after proceed finishes. -}
  where proceed : toplevel-state → maybe start → include-elt → mF (toplevel-state × include-elt × mod-info)
        proceed s nothing ie' = progress-update filename tt ≫monad returnM (s , ie' , ctxt-get-current-mod (toplevel-state.Γ s)) {- should not happen -}
        proceed s (just x) ie' with include-elt.need-to-add-symbols-to-context ie {- this indeed should be ie, not ie' -}
        proceed (mk-toplevel-state ip fns is Γ) (just x) ie' | tt
          with include-elt.do-type-check ie | ctxt-get-current-mod Γ
        proceed (mk-toplevel-state ip fns is Γ) (just x) ie' | tt | do-check | prev-mod =
         let Γ = ctxt-initiate-file Γ filename (start-modname x) in
           process-start (mk-toplevel-state ip fns (trie-insert is filename ie') Γ)
                   filename pn x do-check Γ empty-spans ≫=monad cont
           where cont : toplevel-state × ctxt × spans → mF (toplevel-state × include-elt × mod-info)
                 cont (mk-toplevel-state ip fns is Γ , Γ' @ (mk-ctxt ret-mod _ _ _ _) , ss) =
                   progress-update pn do-check ≫monad returnM
                     (mk-toplevel-state ip (if do-check then (filename :: fns) else fns) is
                       (ctxt-set-current-mod Γ prev-mod) ,
                     (if do-check then set-spans-include-elt ie' ss else ie') , ret-mod)
        proceed s (just x) ie' | _ = returnM (s , ie' , ctxt-get-current-mod (toplevel-state.Γ s))

process-consts DataNull ps = spanMok
process-consts (DataCons (DataConst pi c tp) cs) ps =
      get-ctxt (λ Γ →
        let t = abs-expand-type' ps tp in -- add-param-type ps (qualif-type Γ tp)
        check-type t (just star) ≫span
        set-ctxt (ctxt-const-def pi c (qualif-type Γ t) Γ) ≫span
        spanM-add (DefDataConst-span pi c)  ≫span
        process-consts cs ps)

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
------------------------------------------------------------------------------
-- All the distributive laws modules
------------------------------------------------------------------------------

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

module DistributiveLaws.Everything where

open import DistributiveLaws.Base
open import DistributiveLaws.Base.Consistency.Axioms
open import DistributiveLaws.PropertiesI

open import DistributiveLaws.Lemma3-ATP
open import DistributiveLaws.Lemma4-ATP
open import DistributiveLaws.Lemma5-ATP
open import DistributiveLaws.Lemma6-ATP

open import DistributiveLaws.TaskB-AllStepsATP
open import DistributiveLaws.TaskB-HalvedStepsATP
open import DistributiveLaws.TaskB-I
open import DistributiveLaws.TaskB-TopDownATP
open import DistributiveLaws.TaskB.UnprovedATP


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

module FOT.FOTC.Program.McCarthy91.WF-Relation.Induction.NonAcc.TerminationCheckIssue
  where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

postulate someℕ : ℕ

{-# TERMINATING #-}
foo : ℕ → ℕ → ℕ
foo n        zero    = 10
foo zero     (succ m) = foo zero someℕ
foo (succ n) (succ m) = foo n (succ m)

{-# TERMINATING #-}
bar : ℕ → ℕ → ℕ
bar n        zero    = 10
bar zero     (succ m) = bar m someℕ
bar (succ n) (succ m) = bar n (succ m)

{-# TERMINATING #-}
foobar : ℕ → ℕ → ℕ
foobar n zero = 10
foobar zero (succ m) with someℕ
... | zero   = 10
... | succ o = foobar m (succ o)
foobar (succ n) (succ m) = foobar n (succ m)


text:
-- Andreas, 2016-12-20, issue #2349

{-# OPTIONS --show-implicit #-}

open import Agda.Primitive
open import Agda.Builtin.Equality

data D {{a}} (A : Set a) : Set a where
  c : {{a : A}} (b : A) → D A

test : ∀ ℓ (A : Set ℓ) (x : D A) (a : A) → x ≡ c {{ℓ}} {{a = a}} a
test ℓ A x a = refl

-- ERROR:
-- x != c {{a}} of type D {{ℓ}} A
-- when checking that the expression refl has type
-- _≡_ {ℓ} {D {{ℓ}} A} x (c {{a}})

-- Note that (c {{a}}) is ill-typed here.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2012-09-15
-- Positive effects of making Agda recognize constant functions.
-- Arguments to constant functions are ignored in definitional equality.
{-# OPTIONS --copatterns #-}
module NonvariantPolarity where

open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where
  constructor trivial

data Bool : Set where
  true false : Bool

True : Bool → Set
True true  = ⊤
True false = ⊥

module IgnoreArg where

  -- A function ignoring its first argument
  knot : Bool → Bool → Bool
  knot x true  = false
  knot x false = true

  test : (y : Bool) → knot true y ≡ knot false y
  test y = refl

module UnusedModulePar where

  -- An unused module parameter
  module M (x : Bool) where

    not : Bool → Bool
    not true  = false
    not false = true

  open M true
  open M false renaming (not to not′)

  test : (y : Bool) → not y ≡ not′ y
  test y = refl

module CoinductiveUnit where

  record Unit : Set where
    coinductive
    constructor delay
    field force : Unit
  open Unit

  -- The identity on Unit does not match on its argument, so it is constant.
  id : Unit → Unit
  force (id x) = id (force x)

  idConst : (x y : Unit) → id x ≡ id y
  idConst x y = refl

  -- That does not imply x ≡ y (needs bisimulation).


text:
{-

This file contains:
  - Pushout-products of two maps;
  - The connectivity of pushout-product maps.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.Pushout.PushoutProduct where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.HITs.Pushout.Base
open import Cubical.HITs.Pushout.Properties

open import Cubical.Homotopy.Connected

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level
    A : Type ℓ
    B : Type ℓ'
    X : Type ℓ''
    Y : Type ℓ'''

-- The definition of pushout-product

PushProd : (f : X → A)(g : Y → B) → Type _
PushProd f g = Pushout (map-× (idfun _) g) (map-× f (idfun _))

_×̂_ : (f : X → A)(g : Y → B) → PushProd f g → A × B
(f ×̂ g) (inl (x , b)) = f x , b
(f ×̂ g) (inr (a , y)) = a , g y
(f ×̂ g) (push (x , y) i) = f x , g y

infixr 5 _×̂_

module _
  (m n : ℕ)(f : X → A)(g : Y → B)
  (connf : isConnectedFun m f)
  (conng : isConnectedFun n g)
  (P : A × B → TypeOfHLevel ℓ (m + n)) where

  module _
    (sec : (x : PushProd f g) → P ((f ×̂ g) x) .fst) where

    private
      fam : A → Type _
      fam a = Σ[ k ∈ ((b : B) → P (a , b) .fst) ] ((y : Y) → k (g y) ≡ sec (inr (a , y)))

      open Iso

      fiberEquiv : (a : A)
        → fam a ≃ fiber (λ(s : (b : B) → P (a , b) .fst) → s ∘ g) (λ y → sec (inr (a , y)))
      fiberEquiv a =  isoToEquiv
        (iso (λ (k , p) → k , λ i y → p y i)
             (λ (k , p) → k , λ y i → p i y)
             (λ _ → refl) (λ _ → refl))

      is-m-trunc-fam : (a : A) → isOfHLevel m (fam a)
      is-m-trunc-fam a =
        isOfHLevelRespectEquiv _ (invEquiv (fiberEquiv a))
          (isOfHLevelPrecomposeConnected m n (λ b → P (a , b)) g conng _)

      sec-fam : (x : X) → fam (f x)
      sec-fam x = (λ b → sec (inl (x , b))) , (λ y i → sec (push (x , y) i))

      map-iso = elim.isIsoPrecompose f _ (λ a → fam a , is-m-trunc-fam a) connf

      k = map-iso .inv sec-fam
      ϕ = map-iso .rightInv sec-fam

    ext : (x : A × B) → P x .fst
    ext (a , b) = k a .fst b

    ext-path : (x : PushProd f g) → ext ((f ×̂ g) x) ≡ sec x
    ext-path (inl (x , b)) i = ϕ i x .fst b
    ext-path (inr (a , y)) i = k a .snd y i
    ext-path (push (x , y) i) j =
      hcomp (λ k → λ
        { (i = i0) → ϕ j x .snd y i0
        ; (i = i1) → ϕ i0 x .snd y (j ∨ ~ k)
        ; (j = i0) → ϕ i0 x .snd y (i ∧ ~ k)
        ; (j = i1) → ϕ i1 x .snd y i })
      (ϕ j x .snd y i)

  lifting : hasSection (λ(s : (x : A × B) → P x .fst) → s ∘ (f ×̂ g))
  lifting .fst sec = ext sec
  lifting .snd sec i x = ext-path sec x i

-- The connectivity of pushout-product

isConnected×̂ : {m n : ℕ}{f : A → B}{g : X → Y}
  → isConnectedFun m f → isConnectedFun n g
  → isConnectedFun (m + n) (f ×̂ g)
isConnected×̂ congf congg =
  elim.isConnectedPrecompose _ _ (lifting _ _ _ _ congf congg)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module SystemF.SmallStep where

open import Prelude

open import Data.Sum
open import Data.Product
open import Data.Vec hiding ([_])

open import SystemF.WellTyped
open import SystemF.Substitutions
open import SystemF.Substitutions.Lemmas

infixl 4 _≻_

-- irreducible System F terms
data Value {ν n} : Term ν n → Set where
  λ' : ∀ τ t → Value (λ' τ t)
  Λ : ∀ t → Value (Λ t)

-- single step reduction of System F terms
data _≻_ {ν n} : Term ν n → Term ν n → Set where
  -- redexes
  reduce-[] : ∀ t a → (Λ t) [ a ] ≻ t tm[/tp a ]
  reduce-· : ∀ a t {u} → (λ' a t) · u ≻ t tm[/tm u ]

  -- contextual closure
  step-·₁ : ∀ {t t' u} → t ≻ t' → t · u ≻ t' · u
  step-·₂ : ∀ {t u u'} → u ≻ u' → t · u ≻ t · u'
  step-λ-body : ∀ {a t t'} → t ≻ t' → λ' a t ≻ λ' a t'
  step-Λ-body : ∀ {t t'} → t ≻ t' → Λ t ≻ Λ t'
  step-[] : ∀ {t t' a} → t ≻ t' → t [ a ] ≻ t' [ a ]

-- multi-step reductions
data _≻⋆_ {ν n} : Term ν n → Term ν n → Set where
  ≻-step : ∀ {t u} → t ≻ u → t ≻⋆ u
  ≻-trans : ∀ {t u v} → t ≻⋆ u → u ≻⋆ v → t ≻⋆ v

∀'-value-lemma : ∀ {ν n} {Γ : Ctx ν n} {t a} → Γ ⊢ t ∈ ∀' a → Value t → ∃ λ e → t ≡ Λ e
∀'-value-lemma () (λ' τ t)
∀'-value-lemma (Λ t∈∀a) (Λ t) = t , refl

→'-value-lemma : ∀ {ν n} {Γ : Ctx ν n} {t a b} → Γ ⊢ t ∈ (a →' b) → Value t →
                 ∃ λ e → (t ≡ λ' a e) × ((a ∷ Γ) ⊢ e ∈ b)
→'-value-lemma () (Λ t)
→'-value-lemma (λ' a ⊢t∈a→b) (λ' .a t) = t , refl , ⊢t∈a→b

-- progress: welltyped terms are either values or can be reduced
progress : ∀ {ν τ} {t : Term ν 0} → [] ⊢ t ∈ τ → Value t ⊎ ∃ (_≻_ t)
progress (var ())
progress (Λ {t = t} ⊢t) = inj₁ (Λ t)
progress (λ' {t = t} a ⊢t) = inj₁ (λ' a t)
progress (_[_] ⊢t a) with progress ⊢t

-- we can rule out the possibility that t is both well typed and a value,
-- but not a lambda
-- leaving only cases that can make progress
progress (_[_] ⊢t a ) | inj₁ (λ' τ t') with ∀'-value-lemma ⊢t (λ' τ t')
progress (() [ a ]) | inj₁ (λ' τ t') | t≡Λe
progress (⊢t [ a ]) | inj₁ (Λ t) = inj₂ (, reduce-[] t a)
progress (⊢t [ a ]) | inj₂ (_ , y≻y') = inj₂ (, step-[] y≻y')

-- similar to above
progress (⊢f · ⊢t) with progress ⊢f | progress ⊢t
progress (⊢f · ⊢t) | inj₁ (λ' τ t) | inj₁ y-isval = inj₂ (, reduce-· τ t)
progress (⊢f · ⊢t) | inj₁ (Λ t) | inj₁ y-isval with →'-value-lemma ⊢f (Λ t)
progress (() · ⊢t) | inj₁ (Λ t) | inj₁ y-isval | f≡a→'b
progress (_·_ {f = f} wf-f ⊢t) | _ | inj₂ (_ , y≻y') = inj₂ (, step-·₂ y≻y')
progress (_·_ {t = t} ⊢f ⊢t) | inj₂ (_ , f≻f') | _ = inj₂ (, step-·₁ f≻f')

-- preservation: reduction preserves well-typedness
≻-preserves : ∀ {ν n} {Γ : Ctx ν n} {t t' τ} → Γ ⊢ t ∈ τ → t ≻ t' → Γ ⊢ t' ∈ τ
≻-preserves (var x) ()
≻-preserves (Λ ⊢t) (step-Λ-body t≻t') = Λ (≻-preserves ⊢t t≻t')
≻-preserves (λ' a ⊢t) (step-λ-body t≻t') = λ' a (≻-preserves ⊢t t≻t')
-- goal: (Λ t) [ a ] and t tm[/tp a ] have the same type
≻-preserves (⊢t [ a ]) (reduce-[] t .a) = WtTypeLemmas.tm[/tp]-preserves ⊢t a
≻-preserves (⊢t [ a ]) (step-[] t≻t') = (≻-preserves ⊢t t≻t') [ a ]
-- goal: (λ' a t) · u and t tm[/tm u ] have the same type
≻-preserves (λ' a ⊢t · ⊢u) (reduce-· .a t₁) = WtTermLemmas.tm[/tm]-preserves ⊢t ⊢u
≻-preserves (⊢t · ⊢u) (step-·₁ t≻t') = (≻-preserves ⊢t t≻t') · ⊢u
≻-preserves (⊢t · ⊢u) (step-·₂ u≻u') = ⊢t · (≻-preserves ⊢u u≻u')