text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties
------------------------------------------------------------------------

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

module Data.Bool.Properties where

open import Algebra.Bundles
open import Data.Bool.Base
open import Data.Empty
open import Data.Product
open import Data.Sum.Base
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Level using (Level; 0ℓ)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary using (ofʸ; ofⁿ; does; proof; yes; no)
open import Relation.Nullary.Decidable using (True)
import Relation.Unary as U

open import Algebra.Definitions {A = Bool} _≡_
open import Algebra.Structures {A = Bool} _≡_
open ≡-Reasoning

private
  variable
    a b : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Properties of _≡_

infix 4 _≟_

_≟_ : Decidable {A = Bool} _≡_
true  ≟ true  = yes refl
false ≟ false = yes refl
true  ≟ false = no λ()
false ≟ true  = no λ()

≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid Bool

≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_

------------------------------------------------------------------------
-- Properties of _≤_

-- Relational properties

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive refl = b≤b

≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl

≤-trans : Transitive _≤_
≤-trans b≤b p   = p
≤-trans f≤t b≤b = f≤t

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym b≤b _ = refl

≤-minimum : Minimum _≤_ false
≤-minimum false = b≤b
≤-minimum true  = f≤t

≤-maximum : Maximum _≤_ true
≤-maximum false = f≤t
≤-maximum true  = b≤b

≤-total : Total _≤_
≤-total false b = inj₁ (≤-minimum b)
≤-total true  b = inj₂ (≤-maximum b)

infix 4 _≤?_

_≤?_ : Decidable _≤_
false ≤? b     = yes (≤-minimum b)
true  ≤? false = no λ ()
true  ≤? true  = yes b≤b

≤-irrelevant : Irrelevant _≤_
≤-irrelevant {_}     f≤t f≤t = refl
≤-irrelevant {false} b≤b b≤b = refl
≤-irrelevant {true}  b≤b b≤b = refl

-- Structures

≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

-- Bundles

≤-poset : Poset 0ℓ 0ℓ 0ℓ
≤-poset = record
  { isPartialOrder = ≤-isPartialOrder
  }

≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
  { isPreorder = ≤-isPreorder
  }

≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  }

≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
  { isDecTotalOrder = ≤-isDecTotalOrder
  }

------------------------------------------------------------------------
-- Properties of _<_

-- Relational properties

<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl ()

<-asym : Asymmetric _<_
<-asym f<t ()

<-trans : Transitive _<_
<-trans f<t ()

<-transʳ : Trans _≤_ _<_ _<_
<-transʳ b≤b f<t = f<t

<-transˡ : Trans _<_ _≤_ _<_
<-transˡ f<t b≤b = f<t

<-cmp : Trichotomous _≡_ _<_
<-cmp false false = tri≈ (λ()) refl  (λ())
<-cmp false true  = tri< f<t   (λ()) (λ())
<-cmp true  false = tri> (λ()) (λ()) f<t
<-cmp true  true  = tri≈ (λ()) refl  (λ())

infix 4 _<?_

_<?_ : Decidable _<_
false <? false = no  (λ())
false <? true  = yes f<t
true  <? _     = no  (λ())

<-resp₂-≡ : _<_ Respects₂ _≡_
<-resp₂-≡ = subst (_ <_) , subst (_< _)

<-irrelevant : Irrelevant _<_
<-irrelevant f<t f<t = refl

-- Structures

<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
  { isEquivalence = isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans
  ; <-resp-≈      = <-resp₂-≡
  }

<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
  { isEquivalence = isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

-- Bundles

<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
<-strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder
  }

<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder
  }

------------------------------------------------------------------------
-- Properties of _∨_

∨-assoc : Associative _∨_
∨-assoc true  y z = refl
∨-assoc false y z = refl

∨-comm : Commutative _∨_
∨-comm true  true  = refl
∨-comm true  false = refl
∨-comm false true  = refl
∨-comm false false = refl

∨-identityˡ : LeftIdentity false _∨_
∨-identityˡ _ = refl

∨-identityʳ : RightIdentity false _∨_
∨-identityʳ false = refl
∨-identityʳ true  = refl

∨-identity : Identity false _∨_
∨-identity = ∨-identityˡ , ∨-identityʳ

∨-zeroˡ : LeftZero true _∨_
∨-zeroˡ _ = refl

∨-zeroʳ : RightZero true _∨_
∨-zeroʳ false = refl
∨-zeroʳ true  = refl

∨-zero : Zero true _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ

∨-inverseˡ : LeftInverse true not _∨_
∨-inverseˡ false = refl
∨-inverseˡ true  = refl

∨-inverseʳ : RightInverse true not _∨_
∨-inverseʳ x = ∨-comm x (not x) ⟨ trans ⟩ ∨-inverseˡ x

∨-inverse : Inverse true not _∨_
∨-inverse = ∨-inverseˡ , ∨-inverseʳ

∨-idem : Idempotent _∨_
∨-idem false = refl
∨-idem true  = refl

∨-sel : Selective _∨_
∨-sel false y = inj₂ refl
∨-sel true y  = inj₁ refl

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

∨-magma : Magma 0ℓ 0ℓ
∨-magma = record
  { isMagma = ∨-isMagma
  }

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

∨-semigroup : Semigroup 0ℓ 0ℓ
∨-semigroup = record
  { isSemigroup = ∨-isSemigroup
  }

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

∨-band : Band 0ℓ 0ℓ
∨-band = record
  { isBand = ∨-isBand
  }

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

∨-semilattice : Semilattice 0ℓ 0ℓ
∨-semilattice = record
  { isSemilattice = ∨-isSemilattice
  }

∨-isMonoid : IsMonoid _∨_ false
∨-isMonoid = record
  { isSemigroup = ∨-isSemigroup
  ; identity = ∨-identity
  }

∨-isCommutativeMonoid : IsCommutativeMonoid _∨_ false
∨-isCommutativeMonoid = record
  { isMonoid = ∨-isMonoid
  ; comm = ∨-comm
  }

∨-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
∨-commutativeMonoid = record
  { isCommutativeMonoid = ∨-isCommutativeMonoid
  }

∨-isIdempotentCommutativeMonoid :
  IsIdempotentCommutativeMonoid _∨_ false
∨-isIdempotentCommutativeMonoid = record
  { isCommutativeMonoid = ∨-isCommutativeMonoid
  ; idem                = ∨-idem
  }

∨-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
∨-idempotentCommutativeMonoid = record
  { isIdempotentCommutativeMonoid = ∨-isIdempotentCommutativeMonoid
  }

------------------------------------------------------------------------
-- Properties of _∧_

∧-assoc : Associative _∧_
∧-assoc true  y z = refl
∧-assoc false y z = refl

∧-comm : Commutative _∧_
∧-comm true  true  = refl
∧-comm true  false = refl
∧-comm false true  = refl
∧-comm false false = refl

∧-identityˡ : LeftIdentity true _∧_
∧-identityˡ _ = refl

∧-identityʳ : RightIdentity true _∧_
∧-identityʳ false = refl
∧-identityʳ true  = refl

∧-identity : Identity true _∧_
∧-identity = ∧-identityˡ , ∧-identityʳ

∧-zeroˡ : LeftZero false _∧_
∧-zeroˡ _ = refl

∧-zeroʳ : RightZero false _∧_
∧-zeroʳ false = refl
∧-zeroʳ true  = refl

∧-zero : Zero false _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ

∧-inverseˡ : LeftInverse false not _∧_
∧-inverseˡ false = refl
∧-inverseˡ true = refl

∧-inverseʳ : RightInverse false not _∧_
∧-inverseʳ x = ∧-comm x (not x) ⟨ trans ⟩ ∧-inverseˡ x

∧-inverse : Inverse false not _∧_
∧-inverse = ∧-inverseˡ , ∧-inverseʳ

∧-idem : Idempotent _∧_
∧-idem false = refl
∧-idem true  = refl

∧-sel : Selective _∧_
∧-sel false y = inj₁ refl
∧-sel true y  = inj₂ refl

∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
∧-distribˡ-∨ true  y z = refl
∧-distribˡ-∨ false y z = refl

∧-distribʳ-∨ : _∧_ DistributesOverʳ _∨_
∧-distribʳ-∨ x y z = begin
  (y ∨ z) ∧ x     ≡⟨ ∧-comm (y ∨ z) x ⟩
  x ∧ (y ∨ z)     ≡⟨ ∧-distribˡ-∨ x y z ⟩
  x ∧ y ∨ x ∧ z   ≡⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
  y ∧ x ∨ z ∧ x   ∎

∧-distrib-∨ : _∧_ DistributesOver _∨_
∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨

∨-distribˡ-∧ : _∨_ DistributesOverˡ _∧_
∨-distribˡ-∧ true  y z = refl
∨-distribˡ-∧ false y z = refl

∨-distribʳ-∧ : _∨_ DistributesOverʳ _∧_
∨-distribʳ-∧ x y z = begin
  (y ∧ z) ∨ x        ≡⟨ ∨-comm (y ∧ z) x ⟩
  x ∨ (y ∧ z)        ≡⟨ ∨-distribˡ-∧ x y z ⟩
  (x ∨ y) ∧ (x ∨ z)  ≡⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
  (y ∨ x) ∧ (z ∨ x)  ∎

∨-distrib-∧ : _∨_ DistributesOver _∧_
∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧

∧-abs-∨ : _∧_ Absorbs _∨_
∧-abs-∨ true  y = refl
∧-abs-∨ false y = refl

∨-abs-∧ : _∨_ Absorbs _∧_
∨-abs-∧ true  y = refl
∨-abs-∧ false y = refl

∨-∧-absorptive : Absorptive _∨_ _∧_
∨-∧-absorptive = ∨-abs-∧ , ∧-abs-∨

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

∧-magma : Magma 0ℓ 0ℓ
∧-magma = record
  { isMagma = ∧-isMagma
  }

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

∧-semigroup : Semigroup 0ℓ 0ℓ
∧-semigroup = record
  { isSemigroup = ∧-isSemigroup
  }

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

∧-band : Band 0ℓ 0ℓ
∧-band = record
  { isBand = ∧-isBand
  }

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

∧-semilattice : Semilattice 0ℓ 0ℓ
∧-semilattice = record
  { isSemilattice = ∧-isSemilattice
  }

∧-isMonoid : IsMonoid _∧_ true
∧-isMonoid = record
  { isSemigroup = ∧-isSemigroup
  ; identity = ∧-identity
  }

∧-isCommutativeMonoid : IsCommutativeMonoid _∧_ true
∧-isCommutativeMonoid = record
  { isMonoid = ∧-isMonoid
  ; comm = ∧-comm
  }

∧-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
∧-commutativeMonoid = record
  { isCommutativeMonoid = ∧-isCommutativeMonoid
  }

∧-isIdempotentCommutativeMonoid :
  IsIdempotentCommutativeMonoid _∧_ true
∧-isIdempotentCommutativeMonoid = record
  { isCommutativeMonoid = ∧-isCommutativeMonoid
  ; idem = ∧-idem
  }

∧-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
∧-idempotentCommutativeMonoid = record
  { isIdempotentCommutativeMonoid = ∧-isIdempotentCommutativeMonoid
  }

∨-∧-isSemiring : IsSemiring _∨_ _∧_ false true
∨-∧-isSemiring = record
  { isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = ∨-isCommutativeMonoid
    ; *-isMonoid = ∧-isMonoid
    ; distrib = ∧-distrib-∨
    }
  ; zero = ∧-zero
  }

∨-∧-isCommutativeSemiring
  : IsCommutativeSemiring _∨_ _∧_ false true
∨-∧-isCommutativeSemiring = record
  { isSemiring = ∨-∧-isSemiring
  ; *-comm = ∧-comm
  }

∨-∧-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
∨-∧-commutativeSemiring = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = false
  ; 1#                    = true
  ; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
  }

∧-∨-isSemiring : IsSemiring _∧_ _∨_ true false
∧-∨-isSemiring = record
  { isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = ∧-isCommutativeMonoid
    ; *-isMonoid = ∨-isMonoid
    ; distrib = ∨-distrib-∧
    }
  ; zero = ∨-zero
  }

∧-∨-isCommutativeSemiring
  : IsCommutativeSemiring _∧_ _∨_ true false
∧-∨-isCommutativeSemiring = record
  { isSemiring = ∧-∨-isSemiring
  ; *-comm = ∨-comm
  }

∧-∨-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
∧-∨-commutativeSemiring = record
  { _+_                   = _∧_
  ; _*_                   = _∨_
  ; 0#                    = true
  ; 1#                    = false
  ; isCommutativeSemiring = ∧-∨-isCommutativeSemiring
  }

∨-∧-isLattice : IsLattice _∨_ _∧_
∨-∧-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ∨-comm
  ; ∨-assoc       = ∨-assoc
  ; ∨-cong        = cong₂ _∨_
  ; ∧-comm        = ∧-comm
  ; ∧-assoc       = ∧-assoc
  ; ∧-cong        = cong₂ _∧_
  ; absorptive    = ∨-∧-absorptive
  }

∨-∧-lattice : Lattice 0ℓ 0ℓ
∨-∧-lattice = record
  { isLattice = ∨-∧-isLattice
  }

∨-∧-isDistributiveLattice : IsDistributiveLattice _∨_ _∧_
∨-∧-isDistributiveLattice = record
  { isLattice    = ∨-∧-isLattice
  ; ∨-distribʳ-∧ = ∨-distribʳ-∧
  }

∨-∧-distributiveLattice : DistributiveLattice 0ℓ 0ℓ
∨-∧-distributiveLattice = record
  { isDistributiveLattice = ∨-∧-isDistributiveLattice
  }

∨-∧-isBooleanAlgebra : IsBooleanAlgebra _∨_ _∧_ not true false
∨-∧-isBooleanAlgebra = record
  { isDistributiveLattice = ∨-∧-isDistributiveLattice
  ; ∨-complementʳ = ∨-inverseʳ
  ; ∧-complementʳ = ∧-inverseʳ
  ; ¬-cong        = cong not
  }

∨-∧-booleanAlgebra : BooleanAlgebra 0ℓ 0ℓ
∨-∧-booleanAlgebra = record
  { isBooleanAlgebra = ∨-∧-isBooleanAlgebra
  }

------------------------------------------------------------------------
-- Properties of _xor_

xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
xor-is-ok true  y = refl
xor-is-ok false y = sym (∧-identityʳ _)

xor-∧-commutativeRing : CommutativeRing 0ℓ 0ℓ
xor-∧-commutativeRing = commutativeRing
  where
  import Algebra.Properties.BooleanAlgebra as BA
  open BA ∨-∧-booleanAlgebra
  open XorRing _xor_ xor-is-ok

------------------------------------------------------------------------
-- Miscellaneous other properties

not-involutive : Involutive not
not-involutive true  = refl
not-involutive false = refl

not-injective : ∀ {x y} → not x ≡ not y → x ≡ y
not-injective {false} {false} nx≢ny = refl
not-injective {true}  {true}  nx≢ny = refl

not-¬ : ∀ {x y} → x ≡ y → x ≢ not y
not-¬ {true}  refl ()
not-¬ {false} refl ()

¬-not : ∀ {x y} → x ≢ y → x ≡ not y
¬-not {true}  {true}  x≢y = ⊥-elim (x≢y refl)
¬-not {true}  {false} _   = refl
¬-not {false} {true}  _   = refl
¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)

⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
⇔→≡ {true } {true }         hyp = refl
⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp ⟨$⟩ refl)
⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp ⟨$⟩ refl
⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp ⟨$⟩ refl
⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp ⟨$⟩ refl)
⇔→≡ {false} {false}         hyp = refl

T-≡ : ∀ {x} → T x ⇔ x ≡ true
T-≡ {false} = equivalence (λ ())       (λ ())
T-≡ {true}  = equivalence (const refl) (const _)

T-not-≡ : ∀ {x} → T (not x) ⇔ x ≡ false
T-not-≡ {false} = equivalence (const refl) (const _)
T-not-≡ {true}  = equivalence (λ ())       (λ ())

T-∧ : ∀ {x y} → T (x ∧ y) ⇔ (T x × T y)
T-∧ {true}  {true}  = equivalence (const (_ , _)) (const _)
T-∧ {true}  {false} = equivalence (λ ())          proj₂
T-∧ {false} {_}     = equivalence (λ ())          proj₁

T-∨ : ∀ {x y} → T (x ∨ y) ⇔ (T x ⊎ T y)
T-∨ {true}  {_}     = equivalence inj₁ (const _)
T-∨ {false} {true}  = equivalence inj₂ (const _)
T-∨ {false} {false} = equivalence inj₁ [ id , id ]

T-irrelevant : U.Irrelevant T
T-irrelevant {true}  _  _  = refl

T? : U.Decidable T
does  (T? b) = b
proof (T? true ) = ofʸ _
proof (T? false) = ofⁿ λ()

T?-diag : ∀ b → T b → True (T? b)
T?-diag true  _ = _

push-function-into-if : ∀ (f : A → B) x {y z} →
                        f (if x then y else z) ≡ (if x then f y else f z)
push-function-into-if _ true  = refl
push-function-into-if _ false = refl

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

∧-∨-distˡ   = ∧-distribˡ-∨
{-# WARNING_ON_USAGE ∧-∨-distˡ
"Warning: ∧-∨-distˡ was deprecated in v0.15.
Please use ∧-distribˡ-∨ instead."
#-}
∧-∨-distʳ   = ∧-distribʳ-∨
{-# WARNING_ON_USAGE ∧-∨-distʳ
"Warning: ∧-∨-distʳ was deprecated in v0.15.
Please use ∧-distribʳ-∨ instead."
#-}
distrib-∧-∨ = ∧-distrib-∨
{-# WARNING_ON_USAGE distrib-∧-∨
"Warning: distrib-∧-∨ was deprecated in v0.15.
Please use ∧-distrib-∨ instead."
#-}
∨-∧-distˡ   = ∨-distribˡ-∧
{-# WARNING_ON_USAGE ∨-∧-distˡ
"Warning: ∨-∧-distˡ was deprecated in v0.15.
Please use ∨-distribˡ-∧ instead."
#-}
∨-∧-distʳ   = ∨-distribʳ-∧
{-# WARNING_ON_USAGE ∨-∧-distʳ
"Warning: ∨-∧-distʳ was deprecated in v0.15.
Please use ∨-distribʳ-∧ instead."
#-}
∨-∧-distrib = ∨-distrib-∧
{-# WARNING_ON_USAGE ∨-∧-distrib
"Warning: ∨-∧-distrib was deprecated in v0.15.
Please use ∨-distrib-∧ instead."
#-}
∨-∧-abs    = ∨-abs-∧
{-# WARNING_ON_USAGE ∨-∧-abs
"Warning: ∨-∧-abs was deprecated in v0.15.
Please use ∨-abs-∧ instead."
#-}
∧-∨-abs    = ∧-abs-∨
{-# WARNING_ON_USAGE ∧-∨-abs
"Warning: ∧-∨-abs was deprecated in v0.15.
Please use ∧-abs-∨ instead."
#-}
not-∧-inverseˡ = ∧-inverseˡ
{-# WARNING_ON_USAGE not-∧-inverseˡ
"Warning: not-∧-inverseˡ was deprecated in v0.15.
Please use ∧-inverseˡ instead."
#-}
not-∧-inverseʳ = ∧-inverseʳ
{-# WARNING_ON_USAGE not-∧-inverseʳ
"Warning: not-∧-inverseʳ was deprecated in v0.15.
Please use ∧-inverseʳ instead."
#-}
not-∧-inverse = ∧-inverse
{-# WARNING_ON_USAGE not-∧-inverse
"Warning: not-∧-inverse was deprecated in v0.15.
Please use ∧-inverse instead."
#-}
not-∨-inverseˡ = ∨-inverseˡ
{-# WARNING_ON_USAGE not-∨-inverseˡ
"Warning: not-∨-inverseˡ was deprecated in v0.15.
Please use ∨-inverseˡ instead."
#-}
not-∨-inverseʳ = ∨-inverseʳ
{-# WARNING_ON_USAGE not-∨-inverseʳ
"Warning: not-∨-inverseʳ was deprecated in v0.15.
Please use ∨-inverseʳ instead."
#-}
not-∨-inverse = ∨-inverse
{-# WARNING_ON_USAGE not-∨-inverse
"Warning: not-∨-inverse was deprecated in v0.15.
Please use ∨-inverse instead."
#-}
isCommutativeSemiring-∨-∧ = ∨-∧-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring-∨-∧
"Warning: isCommutativeSemiring-∨-∧ was deprecated in v0.15.
Please use ∨-∧-isCommutativeSemiring instead."
#-}
commutativeSemiring-∨-∧   =  ∨-∧-commutativeSemiring
{-# WARNING_ON_USAGE commutativeSemiring-∨-∧
"Warning: commutativeSemiring-∨-∧ was deprecated in v0.15.
Please use ∨-∧-commutativeSemiring instead."
#-}
isCommutativeSemiring-∧-∨ = ∧-∨-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring-∧-∨
"Warning: isCommutativeSemiring-∧-∨ was deprecated in v0.15.
Please use ∧-∨-isCommutativeSemiring instead."
#-}
commutativeSemiring-∧-∨   = ∧-∨-commutativeSemiring
{-# WARNING_ON_USAGE commutativeSemiring-∧-∨
"Warning: commutativeSemiring-∧-∨ was deprecated in v0.15.
Please use ∧-∨-commutativeSemiring instead."
#-}
isBooleanAlgebra          = ∨-∧-isBooleanAlgebra
{-# WARNING_ON_USAGE isBooleanAlgebra
"Warning: isBooleanAlgebra was deprecated in v0.15.
Please use ∨-∧-isBooleanAlgebra instead."
#-}
booleanAlgebra            = ∨-∧-booleanAlgebra
{-# WARNING_ON_USAGE booleanAlgebra
"Warning: booleanAlgebra was deprecated in v0.15.
Please use ∨-∧-booleanAlgebra instead."
#-}
commutativeRing-xor-∧     = xor-∧-commutativeRing
{-# WARNING_ON_USAGE commutativeRing-xor-∧
"Warning: commutativeRing-xor-∧ was deprecated in v0.15.
Please use xor-∧-commutativeRing instead."
#-}
proof-irrelevance = T-irrelevant
{-# WARNING_ON_USAGE proof-irrelevance
"Warning: proof-irrelevance was deprecated in v0.15.
Please use T-irrelevant instead."
#-}

-- Version 1.0

T-irrelevance = T-irrelevant
{-# WARNING_ON_USAGE T-irrelevance
"Warning: T-irrelevance was deprecated in v1.0.
Please use T-irrelevant instead."
#-}


text:
------------------------------------------------------------------------
-- A definitional interpreter
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Lambda.Simplified.Delay-monad.Interpreter where

open import Equality.Propositional
open import Prelude

open import Monad equality-with-J
open import Vec.Function equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Monad

open import Lambda.Simplified.Syntax

open Closure Tm

------------------------------------------------------------------------
-- The interpreter

infix 10 _∙_

mutual

  ⟦_⟧ : ∀ {i n} → Tm n → Env n → Delay Value i
  ⟦ var x ⟧   ρ = return (ρ x)
  ⟦ ƛ t ⟧     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ >>= λ v₁ →
                  ⟦ t₂ ⟧ ρ >>= λ v₂ →
                  v₁ ∙ v₂

  _∙_ : ∀ {i} → Value → Value → Delay Value i
  ƛ t₁ ρ ∙ v₂ = later λ { .force → ⟦ t₁ ⟧ (cons v₂ ρ) }

------------------------------------------------------------------------
-- An example

-- The semantics of Ω is the non-terminating computation never.

Ω-loops : ∀ {i} → [ i ] ⟦ Ω ⟧ nil ∼ never
Ω-loops = later λ { .force → Ω-loops }

ext: agda

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Serializer.VecBool where

open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Vec
open import Data.Bool
open import Function using (_∘_ ; _$_ ; _∋_ ; id ; const)
open import Function.Bijection
open import Function.Injection
open import Function.Surjection
open import Function.Equality using (_⟶_ ;  _⟨$⟩_ ; Π )
open import Function.LeftInverse hiding (_∘_)
open import Relation.Binary
open import Relation.Binary.EqReasoning
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; setoid )
import Relation.Binary.Indexed as I

open import Serializer
open import Helper.Fin
open import Serializer.Bool

open Serializer.Serializer {{...}}

2^ : ℕ -> ℕ
2^ zero = 1
2^ (suc b) = 2 * 2^ b

--fromVec : ∀ {a n} {A : Set a} -> Vec A n -> Fin n
fromVec : ∀ {n} -> Vec Bool n -> Fin (2^ n)
fromVec {zero} [] = zero
fromVec {suc n} (x ∷ x₁) = × 2 (2^ n) (from x) (fromVec x₁)

toVec` : ∀ {n} -> Fin (2^ n) -> Vec Bool n
toVec` {zero} x = []
toVec` {suc n} x with ⨂ 2 (2^ n) x
toVec` {suc n} .(× 2 (2^ n) i j) | is× i j = (to i) ∷ (toVec` j)

vec-from-cong : ∀ {n} -> Setoid._≈_ (setoid (Vec Bool n)) I.=[ fromVec ]⇒ Setoid._≈_ (setoid (Fin (2^ n)))
vec-from-cong refl = refl

vec-from-preserves-eq : ∀ {n} -> setoid (Vec Bool n) ⟶ setoid (Fin (2^ n))
vec-from-preserves-eq = record { _⟨$⟩_ = fromVec ; cong = vec-from-cong }

vec-from-injective : ∀ {n} -> Injective (vec-from-preserves-eq {n})
vec-from-injective {zero} {[]} {[]} p with fromVec []
... | p2 = refl
vec-from-injective {suc n} {x ∷ x₁} {y ∷ y₁} p with (⨂ 2 (2^ n) (fromVec (x ∷ x₁))) | (⨂ 2 (2^ n) (fromVec (y ∷ y₁)))
... | a1 | b2 with vec-from-injective {n} {x₁} {y₁}
... | c with c (×-equal₁ {x₁ = (fromBool x)} {x₂ = (fromBool y)} p) | (×-equal₂ {x₁ = (fromBool x)} {x₂ = (fromBool y)} p)
... | p1 | p2 with from-bool-injective p2
vec-from-injective {suc n} {x ∷ x₁} {.x ∷ .x₁} p | a1 | b2 | c | refl | p2 | refl = refl

vec-from-surjective : ∀ {n} -> Surjective (vec-from-preserves-eq {n})
vec-from-surjective {n} = record { from = preserves-eq-inv ; right-inverse-of = (inv {n}) }
  where
    cong-inverse : ∀ {n} -> Setoid._≈_ (setoid (Fin (2^ n))) I.=[ toVec` ]⇒ Setoid._≈_ (setoid (Vec Bool n))
    cong-inverse refl = refl

    preserves-eq-inv : ∀ {n} -> setoid (Fin  (2^ n)) ⟶ setoid (Vec Bool n)
    preserves-eq-inv = record { _⟨$⟩_ = toVec` ; cong = cong-inverse }

    inv : ∀ {n} -> (preserves-eq-inv {n}) RightInverseOf (vec-from-preserves-eq {n})
    inv {zero} zero = refl
    inv {zero} (suc ())
    inv {suc n₁} x with ⨂ 2 (2^ n₁) x
    inv {suc n₁} .(× 2 (2^ n₁) i j) | is× i j
      rewrite (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (bijection {Bool})))) i | (inv {n₁} j) = refl

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


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

open import HoTT

module homotopy.PushoutComm where

-- How do I prevent [to] from being exported?
private
 module _ {i j k} (s : Span {i} {j} {k}) where

  open Span s

  flip : Span
  flip = span B A C g f

  to : Pushout s → Pushout flip
  to = To.f  module M where

    module To = PushoutRec right left (λ (c : C) → ! (glue c))

  open M public

private
 module _ {i j k} (s : Span {i} {j} {k}) where

  to-to-flip : (x : Pushout (flip s)) → to s (to (flip s) x) == x
  to-to-flip = Pushout-elim (λ _ → idp) (λ _ → idp)
    (λ c → ↓-∘=idf-in (to s) (to (flip s))
      (ap (to s) (ap (to (flip s)) (glue c))   =⟨ To.glue-β (flip s) c |in-ctx ap (to s) ⟩
       ap (to s) (! (glue c))                  =⟨ ap-! (to s) (glue c) ⟩
       ! (ap (to s) (glue c))                  =⟨ To.glue-β s c |in-ctx ! ⟩
       ! (! (glue c))                          =⟨ !-! (glue c) ⟩
       glue c ∎))

module _ {i j k} (s : Span {i} {j} {k}) where

  Pushout-comm : Pushout s ≃ Pushout (flip s)
  Pushout-comm = equiv (to s) (to (flip s)) (to-to-flip s) (to-to-flip (flip s))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Extensions.ListFirstFunctional where

open import Prelude hiding (_⊔_)
open import Level

private
    lemma : ∀ {a b} {A : Set a} {P : A → Set b} (decP : ∀ a → (Dec $ P a)) v {x y} →
            any decP (x List.∷ v) ≡ yes (there {x = x} y) → ¬ P x
    lemma decP v {x} {y} eq p with decP x
    lemma decP v () p         | yes _
    lemma decP v eq p         | no ¬p = ¬p p

-- first is functionally defined as the element matched by 'any'
First : ∀ {a b} {A : Set a} {P : A → Set b} (decP : ∀ a → (Dec $ P a)) → List A → Set (a ⊔ b)
First f v = ∃ λ m → any f v ≡ yes m

private
    There : ∀ {a b} {A : Set a} {P : A → Set b} {f v} → (f : First {P = P} f v) → Set
    There (here px , _) = ⊥
    There (there _ , _) = ⊤

    head-first : ∀ {a b} {A : Set a} {P : A → Set b} {f v} → First {P = P} f v → A
    head-first (here {x} _ , _) = x
    head-first (there {x} _ , _) = x

-- we can recover the negative evidence even though Any does not "save it" for there-instances
there⟶¬x' : ∀ {a b} {A : Set a} {P : A → Set b} {decP v} →
            (f : First {P = P} decP v) → {x : There f} → ¬ P (head-first f)
there⟶¬x' (here px , proj₂) {x = ()}
there⟶¬x' {P = P} {decP = decP} (there {x = x'} {xs = xs} tail , proj₂) px with lemma decP xs
there⟶¬x' {P = P} {decP = decP} (there {x = x'} {xs = xs} tail , proj₂) px | ¬px = ¬px proj₂ px


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition07b where

open import Common.FOL

postulate
  P : D → Set

-- We test the translation of a definition where we need to erase
-- proof terms.
foo : ∀ {a} → P a → P a → a ≡ a
foo {a} Pa₁ Pa₂ = bar
  where
  c : D
  c = a
  {-# ATP definition c #-}

  postulate bar : c ≡ a
  {-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

open import HoTT
open import homotopy.FinWedge

module homotopy.Bouquet where

Rose : ∀ {i} (I : Type i) → Type i
Rose I = BigWedge {A = I} (λ _ → ⊙S¹)

Bouquet-family : ∀ {i} (I : Type i) (m : ℕ) → (I → Ptd₀)
Bouquet-family I m _ = ⊙Sphere m

Bouquet : ∀ {i} (I : Type i) (m : ℕ) → Type i
Bouquet I m = BigWedge (Bouquet-family I m)

⊙Bouquet : ∀ {i} (I : Type i) (m : ℕ) → Ptd i
⊙Bouquet I m = ⊙BigWedge (Bouquet-family I m)

BouquetLift-family : ∀ {i} (I : Type i) (m : ℕ) → (I → Ptd i)
BouquetLift-family {i} I m _ = ⊙Lift {j = i} (⊙Sphere m)

BouquetLift : ∀ {i} (I : Type i) (m : ℕ) → Type i
BouquetLift {i} I m = BigWedge (BouquetLift-family I m)

⊙BouquetLift : ∀ {i} (I : Type i) (m : ℕ) → Ptd i
⊙BouquetLift {i} I m = ⊙BigWedge (BouquetLift-family I m)

FinBouquetLift-family : ∀ {i} (I m : ℕ) → (Fin I → Ptd i)
FinBouquetLift-family {i} I m _ = ⊙Lift {j = i} (⊙Sphere m)

⊙FinBouquetLift : ∀ {i} (I m : ℕ) → Ptd i
⊙FinBouquetLift I m = ⊙FinWedge (FinBouquetLift-family I m)

FinBouquet-family : (I m : ℕ) → (Fin I → Ptd₀)
FinBouquet-family I m _ = ⊙Sphere m

FinBouquet : (I m : ℕ) → Type₀
FinBouquet I m = FinWedge (FinBouquet-family I m)

⊙FinBouquet : (I m : ℕ) → Ptd₀
⊙FinBouquet I m = ⊙FinWedge (FinBouquet-family I m)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Data.Nat.Extra where

open import Data.Nat
open import Data.Bool

isZero : ℕ → Bool
isZero 0 = true
isZero (suc _) = false


text:
module Tactic.Nat.Exp where

open import Prelude

Var = Nat

Env : Set → Set
Env Atom = Atom → Nat

infixl 6 _⟨+⟩_
infixl 7 _⟨*⟩_
data Exp (Atom : Set) : Set where
  var : (x : Atom) → Exp Atom
  lit : (n : Nat) → Exp Atom
  _⟨+⟩_ _⟨*⟩_ : (e e₁ : Exp Atom) → Exp Atom

⟦_⟧e : ∀ {Atom} → Exp Atom → Env Atom → Nat
⟦ var x ⟧e   ρ = ρ x
⟦ lit n ⟧e   ρ = n
⟦ e₁ ⟨+⟩ e₂ ⟧e ρ = ⟦ e₁ ⟧e ρ + ⟦ e₂ ⟧e ρ
⟦ e₁ ⟨*⟩ e₂ ⟧e ρ = ⟦ e₁ ⟧e ρ * ⟦ e₂ ⟧e ρ

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module DTGP.State where
open import Data.Product

infixl 1 _>>=_ _=<<_

data State (S A : Set) : Set where
  state : (S → A × S) → State S A

runState : ∀ {S A} → State S A → S → A × S
runState (state f) = f

return : ∀ {S A} → A → State S A
return a = state (λ s → a , s)

_>>=_ : {S A B : Set} → State S A → (A → State S B) → State S B
state h >>= f = state λ s →
  let a,newState = h s
      stateg = f (proj₁ a,newState)
  in
  runState stateg (proj₂ a,newState)

_=<<_ : {S A B : Set} → (A → State S B) → State S A → State S B
f =<< stateh = stateh >>= f

max_stars_repo_name: larrytheliquid/dtgp

max_issues_repo_name: larrytheliquid/dtgp

max_forks_repo_name: larrytheliquid/dtgp


text:
open import Nat
open import Prelude
open import List
open import Hazelnut-core

module Hazelnut-checks where
  -----------------------------------------------------------------------------

  -- these theorems aren't listed in the draft, but have been discussed
  -- since submission. broadly speaking, they act as sanity checks on the
  -- rules. if these properties can't be proven for any extensions to the
  -- language, then the rules are not good.

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

  -- movement doesn't change the term other than moving the focus around.
  moveerase : {e e' : ê} {δ : direction} {t : τ̇} →
            (e + move δ +>e e') →
            (e ◆e) == (e' ◆e)
  moveerase EMAscFirstChild = refl
  moveerase EMAscParent1 = refl
  moveerase EMAscParent2 = refl
  moveerase EMAscNextSib = refl
  moveerase EMAscPrevSib = refl
  moveerase EMLamFirstChild = refl
  moveerase EMLamParent = refl
  moveerase EMPlusFirstChild = refl
  moveerase EMPlusParent1 = refl
  moveerase EMPlusParent2 = refl
  moveerase EMPlusNextSib = refl
  moveerase EMPlusPrevSib = refl
  moveerase EMApFirstChild = refl
  moveerase EMApParent1 = refl
  moveerase EMApParent2 = refl
  moveerase EMApNextSib = refl
  moveerase EMApPrevSib = refl
  moveerase EMFHoleFirstChild = refl
  moveerase EMFHoleParent = refl

  -- describes lists of action whose semantics are composable
  data iterok : Set where

  -- iterates a list of actions that can be composed
  data iterate : iterok → ê → ê → Set where

  --constructability
  mutual
    constructable1 : {Γ : ·ctx} {e : ê} {t : τ̇} →
                     (wt : Γ ⊢ (e ◆e) => t) →
                      Σ[ αs ∈ iterok ]
                        (Σ[ e' ∈ ê ] ((iterate αs (▹ <||> ◃) e') ×
                                       ((e ◆e) == (e' ◆e))))
    constructable1 = {!!}

    constructable2 : {Γ : ·ctx} {e : ê} {t : τ̇} →
                     (wt : Γ ⊢ (e ◆e) <= t) →
                      Σ[ αs ∈ iterok ]
                        (Σ[ e' ∈ ê ] ((iterate αs (▹ <||> ◃) e') ×
                                       ((e ◆e) == (e' ◆e))))
    constructable2 = {!!}

  --reachability
  mutual
    reachable1 : {Γ : ·ctx} {e e' : ê} {t : τ̇}
                 (wt  : Γ ⊢ (e ◆e) <= t) →
                 (wt' : Γ ⊢ (e' ◆e) <= t) →
                 (p : (e ◆e) == (e' ◆e)) →
                 Σ[ αs ∈ iterok ] (iterate αs e e')
    reachable1 = {!!}

    reachable2 : {Γ : ·ctx} {e e' : ê} {t : τ̇}
                 (wt  : Γ ⊢ (e ◆e) => t) →
                 (wt' : Γ ⊢ (e' ◆e) => t) →
                 (p : (e ◆e) == (e' ◆e)) →
                 Σ[ αs ∈ iterok ] (iterate αs e e')
    reachable2 = {!!}


text:
-- Typing contexts and environments
module Syntax.Context where

open import Syntax.Types

open import Relation.Binary using (IsPreorder)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Sum

-- | Data types

-- A type judgement with temporal qualifiers:
-- a type is either inhabited now, or always
data Judgement : Set where
    _now    : Type -> Judgement
    _always : Type -> Judgement
infixl 60 _now
infixl 60 _always

-- Typing context as a list of types
data Context : Set where
    ∙ : Context
    _,_ : Context -> Judgement -> Context
infixl 50 _,_

-- | Context operations and predicates

-- Singleton context
[_] : Judgement -> Context
[ A ] = ∙ , A

-- Concatenation of contexts
_⌊⌋_ : Context -> Context -> Context
Γ ⌊⌋ ∙ = Γ
Γ ⌊⌋ (Γ′ , A) = (Γ ⌊⌋ Γ′) , A
infixl 45 _⌊⌋_

-- Type in the middle of a context
_⌊_⌋_ : Context -> Judgement -> Context -> Context
Γ ⌊ A ⌋ Γ′ = Γ , A ⌊⌋ Γ′
infixl 45 _⌊_⌋_

-- Stabilise the context by filtering out the stable types
_ˢ : Context -> Context
∙ ˢ              = ∙
(Γ , A now)    ˢ = Γ ˢ
(Γ , A always) ˢ = Γ ˢ , A always
infixl 60 _ˢ

-- Predicate for context membership
data _∈_ : Judgement -> Context -> Set where
    top : ∀{Γ A} -> A ∈ Γ , A
    pop : ∀{Γ A B} -> A ∈ Γ -> A ∈ Γ , B
infix 35 _∈_

-- Predicate for context subset relation
data _⊆_ : Context -> Context -> Set where
    refl : ∀{Γ} -> Γ ⊆ Γ
    keep : ∀{Γ Γ′ A} -> Γ ⊆ Γ′ -> Γ , A ⊆ Γ′ , A
    drop : ∀{Γ Γ′ A} -> Γ ⊆ Γ′ -> Γ     ⊆ Γ′ , A
infix 30 _⊆_

-- || Context lemmas

-- | Element and subcontext relations

-- Element of a subset is an element of a set.
∈-⊆-monotone : ∀{Γ Γ′ A} -> Γ ⊆ Γ′ -> A ∈ Γ -> A ∈ Γ′
∈-⊆-monotone refl e           = e
∈-⊆-monotone (keep p) top     = top
∈-⊆-monotone (keep p) (pop e) = pop (∈-⊆-monotone p e)
∈-⊆-monotone (drop p) e       = pop (∈-⊆-monotone p e)

-- Subset relation is reflexive
⊆-refl-eq : ∀{Γ Γ′} -> Γ ≡ Γ′ -> Γ ⊆ Γ′
⊆-refl-eq refl = refl

-- Subset relation is transitive
⊆-trans : ∀{Γ Δ Ξ} -> Γ ⊆ Δ -> Δ ⊆ Ξ -> Γ ⊆ Ξ
⊆-trans refl c2 = c2
⊆-trans c1 refl = c1
⊆-trans c1 (drop c2) = drop (⊆-trans c1 c2)
⊆-trans (keep c1) (keep c2) = keep (⊆-trans c1 c2)
⊆-trans (drop c1) (keep c2) = drop (⊆-trans c1 c2)

-- Subset relation is a preorder
⊆-po : IsPreorder _≡_ _⊆_
⊆-po = record
    { isEquivalence = isEquivalence
    ; reflexive = ⊆-refl-eq
    ; trans = ⊆-trans
    }

-- | Concatenation

-- Concatenation of two contexts is a superset of one of the contexts
Γ⊆Γ⌊⌋Δ : ∀(Γ Δ : Context) -> Γ ⊆ Γ ⌊⌋ Δ
Γ⊆Γ⌊⌋Δ Γ ∙       = refl
Γ⊆Γ⌊⌋Δ Γ (Δ , x) = drop (Γ⊆Γ⌊⌋Δ Γ Δ)

-- Concatenation of two contexts is associative
⌊⌋-assoc : ∀(Γ Δ Ξ : Context) -> (Γ ⌊⌋ Δ) ⌊⌋ Ξ ≡ Γ ⌊⌋ (Δ ⌊⌋ Ξ)
⌊⌋-assoc Γ Δ ∙ = refl
⌊⌋-assoc Γ Δ (Ξ , C) = cong (_, C) (⌊⌋-assoc Γ Δ Ξ)

-- Concatenation of two spliced contexts is associative
⌊A⌋-assoc : ∀(Γ Δ Ξ : Context) A B -> (Γ ⌊ A ⌋ Δ) ⌊ B ⌋ Ξ ≡ Γ ⌊ A ⌋ (Δ ⌊ B ⌋ Ξ)
⌊A⌋-assoc Γ Δ ∙ A B = refl
⌊A⌋-assoc Γ Δ (Ξ , C) A B = cong (_, C) (⌊A⌋-assoc Γ Δ Ξ A B)

-- | Stabilisation

-- Stabilised context is a subset of the full context
Γˢ⊆Γ : ∀ Γ -> Γ ˢ ⊆ Γ
Γˢ⊆Γ ∙ = refl
Γˢ⊆Γ (Γ , A now) = drop (Γˢ⊆Γ Γ)
Γˢ⊆Γ (Γ , A always) = keep (Γˢ⊆Γ Γ)

-- Stabilised spliced context is subset of full spliced context
Γˢ⊆Γ-mid : ∀ (Γ Γ′ : Context) {A} -> Γ ˢ ⌊ A ⌋ Γ′ ˢ ⊆ Γ ⌊ A ⌋ Γ′
Γˢ⊆Γ-mid Γ ∙ = keep (Γˢ⊆Γ Γ)
Γˢ⊆Γ-mid Γ (Γ′ , B now) = drop (Γˢ⊆Γ-mid Γ Γ′)
Γˢ⊆Γ-mid Γ (Γ′ , B always) = keep (Γˢ⊆Γ-mid Γ Γ′)

-- Stabilisation is idempotent
ˢ-idemp : ∀ Γ -> Γ ˢ ˢ ≡ Γ ˢ
ˢ-idemp ∙ = refl
ˢ-idemp (Γ , A now) = ˢ-idemp Γ
ˢ-idemp (Γ , A always) rewrite ˢ-idemp Γ = refl

-- Stabilisation preserves concatenation
ˢ-pres-⌊⌋ : ∀ (Γ Γ′ : Context) -> (Γ ⌊⌋ Γ′) ˢ ≡ Γ ˢ ⌊⌋ Γ′ ˢ
ˢ-pres-⌊⌋ Γ ∙ = refl
ˢ-pres-⌊⌋ Γ (Γ′ , A now) = ˢ-pres-⌊⌋ Γ Γ′
ˢ-pres-⌊⌋ Γ (Γ′ , A always) rewrite ˢ-pres-⌊⌋ Γ Γ′ = refl

-- Stabilisation preserves subcontext relation
ˢ-⊆-monotone : ∀{Γ Γ′} -> Γ ⊆ Γ′ -> Γ ˢ ⊆ Γ′ ˢ
ˢ-⊆-monotone refl = refl
ˢ-⊆-monotone (keep {Γ} {Γ′} {A now} s) = ˢ-⊆-monotone s
ˢ-⊆-monotone (keep {Γ} {Γ′} {A always} s) = keep (ˢ-⊆-monotone s)
ˢ-⊆-monotone (drop {Γ} {Γ′} {A now} s) = ˢ-⊆-monotone s
ˢ-⊆-monotone (drop {Γ} {Γ′} {A always} s) = drop (ˢ-⊆-monotone s)

-- The context of stable variables can be stabilised
ˢ-∈-always : ∀{Γ A} -> A always ∈ Γ -> A always ∈ Γ ˢ
ˢ-∈-always {.(_ , _ always)} top = top
ˢ-∈-always {Γ , B now} (pop e) = ˢ-∈-always e
ˢ-∈-always {Γ , B always} (pop e) = pop (ˢ-∈-always e)

-- | Other lemmas

-- If B ∈ Γ ⌊ A ⌋ Γ′ then either B is equal to A, or B is in Γ ⌊⌋ Γ′
var-disjoint : ∀(Γ Γ′ : Context) {A B} ->  B ∈ Γ ⌊ A ⌋ Γ′ -> (B ≡ A) ⊎ (B ∈ Γ ⌊⌋ Γ′)
var-disjoint Γ ∙ top = inj₁ refl
var-disjoint Γ ∙ (pop e) = inj₂ e
var-disjoint Γ (Γ′ , C) top = inj₂ top
var-disjoint Γ (Γ′ , C) (pop e) with var-disjoint Γ Γ′ e
var-disjoint Γ (Γ′ , C) (pop e) | inj₁ B≡A = inj₁ B≡A
var-disjoint Γ (Γ′ , C) (pop e) | inj₂ y = inj₂ (pop y)

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


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.Base.Types
import      LibraBFT.Yasm.Base as LYB

-- This module defines a model of a distributed system, parameterized by
-- SystemParameters, which establishes various application-dependent types,
-- handlers, etc.  The model supports a set of peers executing handlers in
-- response to messages received; these handlers can update the peer's
-- local state and/or send additional messages.  The model also enables
-- "cheat" steps, which can send arbitrary messages, except that they are
-- constrained to prevent a cheat step from introducing a new signature for
-- an "honest" public key.  The module also contains some structures for
-- proving properties of executions of the modeled system.

module LibraBFT.Yasm.System
   (ℓ-EC        : Level)
   (EpochConfig : Set ℓ-EC)
   (epochId     : EpochConfig → EpochId)
   (authorsN    : EpochConfig → ℕ)
   (parms : LYB.SystemParameters ℓ-EC EpochConfig epochId authorsN)
 where

 data InitStatus : Set where
   uninitd : InitStatus
   initd   : InitStatus

 open import LibraBFT.Yasm.Base            ℓ-EC EpochConfig epochId authorsN
 open SystemParameters parms
 open import LibraBFT.Yasm.AvailableEpochs PeerId ℓ-EC EpochConfig epochId authorsN
             using (AvailableEpochs) renaming (lookup'' to EC-lookup)
 import LibraBFT.Yasm.AvailableEpochs      PeerId ℓ-EC EpochConfig epochId authorsN as AE
 open import Util.FunctionOverride PeerId _≟PeerId_

 open import LibraBFT.Base.PKCS

 SenderMsgPair : Set
 SenderMsgPair = PeerId × Msg

 SentMessages : Set
 SentMessages = List SenderMsgPair

 -- The model supports sending messages that contain some fields that are
 -- /not/ covered by the message's signature.  Therefore, given a message
 -- with a verifiable signature, it is possible for a propositionally
 -- different message that verifies against the same signature to have been
 -- sent before, which is captured by the following definition.
 record MsgWithSig∈ (pk : PK)(sig : Signature)(pool : SentMessages) : Set where
   constructor mkMsgWithSig∈
   field
     msgWhole   : Msg
     msgPart    : Part
     msg⊆       : msgPart ⊂Msg msgWhole
     msgSender  : PeerId
     msg∈pool   : (msgSender , msgWhole) ∈ pool
     msgSigned  : WithVerSig pk msgPart
     msgSameSig : ver-signature msgSigned ≡ sig
 open MsgWithSig∈ public

 postulate  -- TODO-1: prove it
   MsgWithSig∈? : ∀ {pk} {sig} {pool} → Dec (MsgWithSig∈ pk sig pool)

 MsgWithSig∈-++ʳ : ∀{pk sig pool ms} → MsgWithSig∈ pk sig pool → MsgWithSig∈ pk sig (ms ++ pool)
 MsgWithSig∈-++ʳ {ms = pre} msig = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = Any-++ʳ pre (msg∈pool msig)
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 MsgWithSig∈-++ˡ : ∀{pk sig pool ms} → MsgWithSig∈ pk sig ms → MsgWithSig∈ pk sig (ms ++ pool)
 MsgWithSig∈-++ˡ {ms = pre} msig = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = Any-++ˡ (msg∈pool msig)
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 MsgWithSig∈-transp : ∀{pk sig pool pool'}
                    → (mws : MsgWithSig∈ pk sig pool)
                    → (msgSender mws , msgWhole mws) ∈ pool'
                    → MsgWithSig∈ pk sig pool'
 MsgWithSig∈-transp msig ∈pool' = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = ∈pool'
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 -- * Forbidding the Forging of Signatures
 --
 -- Whenever our reasoning must involve digital signatures, it is standard
 -- to talk about EUF-CMA resistant signature schemes. Informally, this captures
 -- signatures schemes that cannot be compromised by certain adversaries.
 -- Formally, it means that for any probabilistic-polynomial-time adversary 𝓐,
 -- and some security parameter k:
 --
 --      Pr[ EUF-CMA(k) ] ≤ ε(k) for ε a negigible function.
 --
 -- EUF-CMA is defined as:
 --
 -- EUF-CMA(k):                           |  O(m):
 --   L        ← ∅                        |    σ ← Sign(sk , m)
 --   (pk, sk) ← Gen(k)                   |    L ← L ∪ { m }
 --   (m , σ)  ← 𝓐ᴼ(pk)                   |    return σ
 --   return (Verify(pk, m, σ) ∧ m ∉ L)   |
 --
 -- This says that 𝓐 cannot create a message that has /not yet been signed/ and
 -- forge a signature for it. The list 'L' keeps track of the messages that 𝓐
 -- asked to be signed by the oracle.
 --
 -- Because the probability of the adversary to win the EUF-CMA(k) game
 -- approaches 0 as k increases; it is reasonable to assume that winning
 -- the game is /impossible/ for realistic security parameters.
 --
 -- EUF-CMA security is incorporated into our model by constraining messages
 -- sent by a cheat step to ensure that for every verifiably signed part of
 -- such a message, if there is a signature on the part, then it is either for
 -- a dishonest public key (in which cases it's secret key may have been leaked),
 -- or a message has been sent with the same signature before (in which case the
 -- signature is simply being "replayed" from a previous message).
 --
 -- Dishonest (or "cheat") messages are those that are not the result of
 -- a /handle/ or /init/ call, but rather are the result of a /cheat/ step.
 --
 -- A part of a cheat message can contain a verifiable signature only if it
 -- is for a dishonest public key, or a message with the same signature has
 -- been sent before (a cheater can "reuse" an honest signature sent
 -- before; it just can't produce a new one).  Note that this constraint
 -- precludes a peer sending a message that contains a new verifiable
 -- signature for an honest PK, even if the PK is the peer's own PK for
 -- some epoch (implying that the peer possesses the associated secret
 -- key).  In other words, a peer that is honest for a given epoch (by
 -- virtue of being a member of that epoch and being assigned an honest PK
 -- for the epoch), cannot send a message for that epoch using a cheat
 -- step.
 CheatPartConstraint : SentMessages → Part → Set
 CheatPartConstraint pool m = ∀{pk} → (ver : WithVerSig pk m)
                                    → Meta-Dishonest-PK pk
                                    ⊎ MsgWithSig∈ pk (ver-signature ver) pool

 -- The only constraints on messages sent by cheat steps are that:
 -- * the sender is not an honest member in the epoch of any part of the message
 -- * the signature on any part of the message satisfies CheatCanSign, meaning
 --   that it is not a new signature for an honest public key
 CheatMsgConstraint : SentMessages → Msg → Set
 CheatMsgConstraint pool m = ∀{part} → part ⊂Msg m → CheatPartConstraint pool part

 -- * The System State
 --
 -- A system consists in a partial map from PeerId to PeerState, a pool
 -- of sent messages and a number of available epochs.
 record SystemState (e : ℕ) : Set ℓ-EC where
   field
     peerStates  : PeerId → PeerState
     initialised : PeerId → InitStatus
     msgPool     : SentMessages          -- All messages ever sent
     availEpochs : AvailableEpochs e
 open SystemState public

 initialState : SystemState 0
 initialState = record
   { peerStates  = const initPS
   ; initialised = const uninitd
   ; msgPool     = []
   ; availEpochs = []
   }

 -- Convenience function for appending an epoch to the system state
 pushEpoch : ∀{e} → EpochConfigFor e → SystemState e → SystemState (suc e)
 pushEpoch 𝓔 st = record
   { peerStates  = peerStates st
   ; initialised = initialised st
   ; msgPool     = msgPool st
   ; availEpochs = AE.append 𝓔 (availEpochs st)
   }

 -- * Small Step Semantics
 --
 -- The small step semantics are divided into three datatypes:
 --
 -- i)   StepPeerState executes a step through init or handle
 -- ii)  StepPeer executes a step through StepPeerState or cheat
 -- iii) Step transitions the system state by a StepPeer or by
 --      bringing a new epoch into existence

 -- The pre and post states of Honest peers are related iff
 data StepPeerState {e}(pid : PeerId)(𝓔s : AvailableEpochs e)(pool : SentMessages)
                       (peerInits : PeerId → InitStatus) (ps : PeerState) :
                       (PeerId → InitStatus) → (PeerState × List Msg) → Set where
   -- The peer receives an "initialization package"; for now, this consists
   -- of the actual EpochConfig for the epoch being initialized.  Later, we
   -- may move to a more general scheme, enabled by assuming a function
   -- 'render : InitPackage -> EpochConfig'.
   step-init : ∀ (ix : Fin e)
             → StepPeerState pid 𝓔s pool peerInits ps ⟦ peerInits , pid ← initd ⟧ (init pid (AE.lookup' 𝓔s ix) ps)

   -- The peer processes a message in the pool
   step-msg  : ∀{m}
             → m ∈ pool
             → peerInits pid ≡ initd
             → StepPeerState pid 𝓔s pool peerInits ps peerInits (handle pid (proj₂ m) ps)

 -- The pre-state of the suplied PeerId is related to the post-state and list of output messages iff:
 data StepPeer {e}(pre : SystemState e) : PeerId → PeerState → List Msg → Set where
   -- it can be obtained by a handle or init call.
   step-honest : ∀{pid st outs init'}
               → StepPeerState pid (availEpochs pre) (msgPool pre) (initialised pre) (peerStates pre pid) init' (st , outs)
               → StepPeer pre pid st outs

   -- or the peer decides to cheat.  CheatMsgConstraint ensures it cannot
   -- forge signatures by honest peers.  Cheat steps do not modify peer
   -- state: these are maintained exclusively by the implementation
   -- handlers.
   step-cheat  : ∀{pid}
               → (fm : SentMessages → PeerState → Msg)
               → let m = fm (msgPool pre) (peerStates pre pid)
                  in CheatMsgConstraint (msgPool pre) m
                   → StepPeer pre pid (peerStates pre pid) (m ∷ [])

 isCheat : ∀ {e pre pid ms outs} → StepPeer {e} pre pid ms outs → Set
 isCheat (step-honest _)  = ⊥
 isCheat (step-cheat _ _) = Unit

 -- Computes the post-sysstate for a given step-peer.
 StepPeer-post : ∀{e pid st' outs}{pre : SystemState e}
               → StepPeer pre pid st' outs → SystemState e
 StepPeer-post {e} {pid} {st'} {outs} {pre} _ = record pre
   { peerStates = ⟦ peerStates pre , pid ← st' ⟧
   ; msgPool    = List-map (pid ,_) outs ++ msgPool pre
   }

 StepPeer-post-lemma : ∀{e pid st' outs}{pre : SystemState e}
               → (pstep : StepPeer pre pid st' outs)
               → st' ≡ peerStates (StepPeer-post pstep) pid
 StepPeer-post-lemma pstep = sym override-target-≡

 cheatStepDNMPeerStates : ∀{e pid st' outs}{pre : SystemState e}
                        → (theStep : StepPeer pre pid st' outs)
                        → isCheat theStep
                        → peerStates (StepPeer-post theStep) ≡ peerStates pre
 cheatStepDNMPeerStates {pid = pid} {pre = pre} (step-cheat _ _) _
   = overrideSameVal-correct-ext {f = peerStates pre} {pid}

 cheatStepDNMPeerStates₁ : ∀{e pid pid' st' outs}{pre : SystemState e}
                        → (theStep : StepPeer pre pid st' outs)
                        → isCheat theStep
                        → peerStates (StepPeer-post theStep) pid' ≡ peerStates pre pid'
 cheatStepDNMPeerStates₁ {_} {pid} {pid'} (step-cheat fm x₁) x
   = overrideSameVal-correct pid pid'

 data Step : ∀{e e'} → SystemState e → SystemState e' → Set ℓ-EC where
   step-epoch : ∀{e}{pre : SystemState e}
              → (𝓔 : EpochConfigFor e)
              -- TODO-3: Eventually, we'll condition this step to only be
              -- valid when peers on the previous epoch have agreed that 𝓔
              -- is the new one.  → ∃EnoughValidCommitMsgsFor pre 𝓔
              → Step pre (pushEpoch 𝓔 pre)

   step-peer : ∀{e pid st' outs}{pre : SystemState e}
             → (pstep : StepPeer pre pid st' outs)
             → Step pre (StepPeer-post pstep)

 msgs-stable : ∀ {e e'} {pre : SystemState e} {post : SystemState e'} {m}
             → (theStep : Step pre post)
             → m ∈ msgPool pre
             → m ∈ msgPool post
 msgs-stable (step-epoch _) m∈ = m∈
 msgs-stable (step-peer {pid = pid} {outs = outs} _) m∈ = Any-++ʳ (List-map (pid ,_) outs) m∈

 peersRemainInitialized : ∀ {pid} {e e'} {pre : SystemState e} {post : SystemState e'}
                        → (theStep : Step pre post)
                        → initialised pre pid ≡ initd
                        → initialised post pid ≡ initd
 peersRemainInitialized (step-epoch _) isInitd = isInitd
 peersRemainInitialized {pid} (step-peer step) isInitd
   with step
 ... | step-cheat _ _ = isInitd
 ... | step-honest {pidS} {st} {outs} stp
   with pid ≟PeerId pidS
 ...| yes refl = isInitd
 ...| no imp = isInitd

 -- not used yet, but some proofs could probably be cleaned up using this,
 -- e.g., prevVoteRnd≤-pred-step in Impl.VotesOnce
 sendMessages-target : ∀ {m : SenderMsgPair} {sm : SentMessages} {ml : List SenderMsgPair}
                     → ¬ (m ∈ sm)
                     → m ∈ (ml ++ sm)
                     → m ∈ ml
 sendMessages-target {ml = ml} ¬m∈sm m∈++
   with Any-++⁻ ml m∈++
 ...| inj₁ m∈ml = m∈ml
 ...| inj₂ m∈sm = ⊥-elim (¬m∈sm m∈sm)

 step-epoch-does-not-send : ∀ {e} (pre : SystemState e) (𝓔 : EpochConfigFor e)
                            → msgPool (pushEpoch 𝓔 pre) ≡ msgPool pre
 step-epoch-does-not-send _ _ = refl

 -- * Reflexive-Transitive Closure

 data Step* : ∀{e e'} → SystemState e → SystemState e' → Set ℓ-EC where
   step-0 : ∀{e}{pre : SystemState e}
          → Step* pre pre

   step-s : ∀{e e' e''}{fst : SystemState e}{pre : SystemState e'}{post : SystemState e''}
          → Step* fst pre
          → Step pre post
          → Step* fst post

 ReachableSystemState : ∀{e} → SystemState e → Set ℓ-EC
 ReachableSystemState = Step* initialState

 eventProcessorPostSt : ∀ {pid s' s outs init'} {e} {st : SystemState e}
                      → (r : ReachableSystemState st)
                      → (stP : StepPeerState pid (availEpochs st) (msgPool st) (initialised st)
                                             (peerStates st pid) init' (s' , outs))
                      → peerStates (StepPeer-post {pre = st} (step-honest stP)) pid ≡ s
                      → s ≡ s'
 eventProcessorPostSt _ _ ps≡s = trans (sym ps≡s) override-target-≡

 Step*-mono : ∀{e e'}{st : SystemState e}{st' : SystemState e'}
            → Step* st st' → e ≤ e'
 Step*-mono step-0 = ≤-refl
 Step*-mono (step-s tr (step-peer _)) = Step*-mono tr
 Step*-mono (step-s tr (step-epoch _)) = ≤-step (Step*-mono tr)

 MsgWithSig∈-Step* : ∀{e e' sig pk}{st : SystemState e}{st' : SystemState e'}
                   → Step* st st'
                   → MsgWithSig∈ pk sig (msgPool st)
                   → MsgWithSig∈ pk sig (msgPool st')
 MsgWithSig∈-Step* step-0        msig = msig
 MsgWithSig∈-Step* (step-s tr (step-epoch _)) msig
   = MsgWithSig∈-Step* tr msig
 MsgWithSig∈-Step* (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-++ʳ (MsgWithSig∈-Step* tr msig)

 MsgWithSig∈-Step*-part : ∀{e e' sig pk}{st : SystemState e}{st' : SystemState e'}
                        → (tr   : Step* st st')
                        → (msig : MsgWithSig∈ pk sig (msgPool st))
                        → msgPart msig ≡ msgPart (MsgWithSig∈-Step* tr msig)
 MsgWithSig∈-Step*-part step-0        msig = refl
 MsgWithSig∈-Step*-part (step-s tr (step-epoch _)) msig
   = MsgWithSig∈-Step*-part tr msig
 MsgWithSig∈-Step*-part (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-Step*-part tr msig

 MsgWithSig∈-Step*-sender : ∀{e e' sig pk}{st : SystemState e}{st' : SystemState e'}
                          → (tr   : Step* st st')
                          → (msig : MsgWithSig∈ pk sig (msgPool st))
                          → msgSender msig ≡ msgSender (MsgWithSig∈-Step* tr msig)
 MsgWithSig∈-Step*-sender step-0        msig = refl
 MsgWithSig∈-Step*-sender (step-s tr (step-epoch _)) msig
   = MsgWithSig∈-Step*-sender tr msig
 MsgWithSig∈-Step*-sender (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-Step*-sender tr msig

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

 -- Type synonym to express a relation over system states;
 SystemStateRel : (∀{e e'} → SystemState e → SystemState e' → Set ℓ-EC) → Set (ℓ+1 ℓ-EC)
 SystemStateRel P = ∀{e e'}{st : SystemState e}{st' : SystemState e'} → P st st' → Set ℓ-EC

 -- Just like Data.List.Any maps a predicate over elements to a predicate over lists,
 -- Any-step maps a relation over steps to a relation over steps in a trace.
 data Any-Step (P : SystemStateRel Step) : SystemStateRel Step* where
  step-here  : ∀{e e' e''}{fst : SystemState e}{pre : SystemState e'}{post : SystemState e''}
             → (cont : Step* fst pre)
             → {this : Step pre post}(prf  : P this)
             → Any-Step P (step-s cont this)

  step-there : ∀{e e' e''}{fst : SystemState e}{pre : SystemState e'}{post : SystemState e''}
             → {cont : Step* fst pre}
             → {this : Step pre post}
             → (prf  : Any-Step P cont)
             → Any-Step P (step-s cont this)

 Any-Step-⇒ : ∀ {P Q : SystemStateRel Step}
            → (∀ {e e'}{pre : SystemState e}{post : SystemState e'} → (x : Step pre post) → P {e} {e'} x → Q {e} {e'} x)
            → ∀ {e e' fst lst} {tr : Step* {e} {e'} fst lst}
            → Any-Step P tr
            → Any-Step Q tr
 Any-Step-⇒ p⇒q (step-here cont {this} prf) = step-here cont (p⇒q this prf)
 Any-Step-⇒ p⇒q (step-there anyStep) = step-there (Any-Step-⇒ p⇒q anyStep)

 Any-Step-elim
   : ∀{e₀ e₁}{st₀ : SystemState e₀}{st₁ : SystemState e₁}{P : SystemStateRel Step}{Q : Set ℓ-EC}
   → {r : Step* st₀ st₁}
   → (P⇒Q : ∀{d d'}{s : SystemState d}{s' : SystemState d'}{st : Step s s'}
          → P st → Step* s' st₁ → Q)
   → Any-Step P r → Q
 Any-Step-elim P⇒Q (step-here cont prf)
   = P⇒Q prf step-0
 Any-Step-elim P⇒Q (step-there {this = this} f)
   = Any-Step-elim (λ p s → P⇒Q p (step-s s this)) f

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

 module _ (P : ∀{e} → SystemState e → Set) where

   Step*-Step-fold : (∀{e}{st : SystemState e}
                        → ReachableSystemState st
                        → (𝓔 : EpochConfigFor e)
                        → P st
                        → P (pushEpoch 𝓔 st))
                   → (∀{e pid st' outs}{st : SystemState e}
                        → ReachableSystemState st
                        → (pstep : StepPeer st pid st' outs)
                        → P st
                        → P (StepPeer-post pstep))
                   → P initialState
                   → ∀{e}{st : SystemState e}
                   → (tr : ReachableSystemState st) → P st
   Step*-Step-fold fe fs p₀ step-0 = p₀
   Step*-Step-fold fe fs p₀ (step-s tr (step-epoch 𝓔)) = fe tr 𝓔 (Step*-Step-fold fe fs p₀ tr)
   Step*-Step-fold fe fs p₀ (step-s tr (step-peer p)) = fs tr p (Step*-Step-fold fe fs p₀ tr)

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
open import Data.Bool hiding (if_then_else_)
open import Data.Empty
open import Data.List
open import Data.List.Properties
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.Unit

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

module EffectAnnotations where

open import Axiom.Extensionality.Propositional
open import Axiom.UniquenessOfIdentityProofs

-- ASSUMING FUNCTION EXTENSIONALITY

postulate
  fun-ext : ∀ {a b} → Extensionality a b
  ifun-ext : ∀ {a b} → ExtensionalityImplicit a b

-- SIGNAL AND INTERRUPT NAMES

postulate Σₛ : Set

-- SIGNAL AND INTERRUPT NAMES HAVE DECIDABLE EQUALITY

postulate decₛ : (op op' : Σₛ) → Dec (op ≡ op')

if_≡_then_else_ : {A : Set} → Σₛ → Σₛ → A → A → A
if op ≡ op' then x else y with decₛ op op'
... | yes p = x
... | no ¬p = y

ite-≡ : {A : Set}
        {op : Σₛ}
        {x y : A} →
        -----------------------------
        if op ≡ op then x else y ≡ x

ite-≡ {A} {op} with decₛ op op
ite-≡ {A} {op} | yes p =
  refl
ite-≡ {A} {op} | no ¬p =
  ⊥-elim (¬p refl)

ite-≢ : {A : Set}
        {op op' : Σₛ}
        {x y : A} →
        op ≢ op' →
        ------------------------------
        if op ≡ op' then x else y ≡ y

ite-≢ {A} {op} {op'} p with decₛ op op'
ite-≢ {A} {op} {op'} p | yes q =
  ⊥-elim (p q)
ite-≢ {A} {op} {op'} p | no ¬q =
  refl

-- EFFECT ANNOTATIONS FOR OUTGOING SIGNALS (O) AND INTERRUPT HANDLERS (I)

mutual
  data O : Set where
    omap : (Σₛ → Maybe ⊤) → O

  data I : Set where
    imap : (Σₛ → Maybe (O × I)) → I

-- EMPTY EFFECT ANNOTATIONS

∅ₒ : O
∅ₒ = omap (λ _ → nothing)

∅ᵢ : I
∅ᵢ = imap (λ _ → nothing)

-- UNION OF EFFECT ANNOTATIONS

∪ₒ-aux' : (o o' : Maybe ⊤) → Maybe ⊤
∪ₒ-aux' nothing o' = o'
∪ₒ-aux' (just tt) o' = just tt

∪ₒ-aux : (o o' : Σₛ → Maybe ⊤) → Σₛ → Maybe ⊤
∪ₒ-aux o o' op =
  ∪ₒ-aux' (o op) (o' op)

_∪ₒ_ : O → O → O
(omap o) ∪ₒ (omap o') =
  omap (∪ₒ-aux o o')

mutual
  ∪ᵢ-aux : (i i' : Σₛ → Maybe (O × I)) → Σₛ → Maybe (O × I)
  ∪ᵢ-aux i i' op =
    ∪ᵢ-aux' (i op) (i' op)

  ∪ᵢ-aux' : (oi oi' : Maybe (O × I)) → Maybe (O × I)
  ∪ᵢ-aux' nothing oi' =
    oi'
  ∪ᵢ-aux' (just oi'') nothing =
    just oi''
  ∪ᵢ-aux' (just (o'' , (imap i''))) (just (o''' , (imap i'''))) =
    just (o'' ∪ₒ o''' , imap (∪ᵢ-aux i'' i'''))

_∪ᵢ_ : I → I → I
(imap i) ∪ᵢ (imap i') =
  imap (∪ᵢ-aux i i')

-- SETTING THE VALUE OF EFFECT ANNOTATION AT A SPECIFIC INTERRUPT NAME

_[_↦_]ᵢ : I → Σₛ → Maybe (O × I) → I
(imap i) [ op ↦ v ]ᵢ =
  imap (λ op' → if op ≡ op' then v else i op')

-- ACTION OF INTERRUPTS ON EFFECT ANNOTATIONS

infix 40 _↓ₑ_

↓ₑ-auxₒ : Σₛ → Maybe (O × I) → O → O
↓ₑ-auxₒ op nothing o =
  o
↓ₑ-auxₒ op (just (o' , i')) o =
  o ∪ₒ o'

↓ₑ-auxᵢ : Σₛ → Maybe (O × I) → I → I
↓ₑ-auxᵢ op nothing i =
  i
↓ₑ-auxᵢ op (just (o' , i')) i =
  (i [ op ↦ nothing ]ᵢ) ∪ᵢ i'

_↓ₑ_ : Σₛ → O × I → O × I
op ↓ₑ (omap o , imap i) =
  (↓ₑ-auxₒ op (i op) (omap o) , ↓ₑ-auxᵢ op (i op) (imap i))

-- GENERALISED ACTION OF INTERRUPTS ON EFFECT ANNOTATIONS

_↓↓ₑ_ : List Σₛ → O × I → O × I
[] ↓↓ₑ (o , i) =
  (o , i)
(op ∷ ops) ↓↓ₑ (o , i) =
  op ↓ₑ (ops ↓↓ₑ (o , i))

↓↓ₑ-act : {o : O}
          {i : I} →
          (ops ops' : List Σₛ) →
          ------------------------------------------------------
          (ops ++ ops') ↓↓ₑ (o , i) ≡ ops ↓↓ₑ (ops' ↓↓ₑ (o , i))

↓↓ₑ-act [] ops' =
  refl
↓↓ₑ-act (op ∷ ops) ops' =
  cong (λ oi → op ↓ₑ oi) (↓↓ₑ-act ops ops')

-- CHECKING THE CONTENTS OF EFFECT ANNOTATIONS

_∈ₒ_ : Σₛ → O → Set
op ∈ₒ (omap o) =
  o op ≡ just tt

lkpᵢ : Σₛ → I → Maybe (O × I)
lkpᵢ op (imap i) = i op

-- SUBTYPING RELATIONS FOR EFFECT ANNOTATIONS

_⊑ₒ_ : O → O → Set
o ⊑ₒ o' = (op : Σₛ) → op ∈ₒ o → op ∈ₒ o'

data _⊑ᵢ_ (i i' : I) : Set where
  rel : ((op : Σₛ) → {o : O} → {i'' : I} → lkpᵢ op i ≡ just (o , i'') →
          Σ[ o' ∈ O ] Σ[ i''' ∈ I ] (lkpᵢ op i' ≡ just (o' , i''') × o ⊑ₒ o' × i'' ⊑ᵢ i''')) →
        i ⊑ᵢ i'

-- SUBTYPING RELATIONS ARE PREORDERS

⊑ₒ-refl : {o : O} →
          ---------
          o ⊑ₒ o

⊑ₒ-refl =
  λ op p → p

⊑ₒ-trans : {o o' o'' : O} →
           o ⊑ₒ o' →
           o' ⊑ₒ o'' →
           ----------------
           o ⊑ₒ o''

⊑ₒ-trans p q =
  λ op r → q op (p op r)

⊑ᵢ-refl : {i : I} →
          ---------
          i ⊑ᵢ i

⊑ᵢ-refl {imap i} =
  rel (λ op {o'} → λ { {imap i'} → λ p → ⊑ᵢ-refl-aux (i op) p })

  where
    ⊑ᵢ-refl-aux : (oi : Maybe (O × I)) →
                  ----------------------------------------------------------------------------------
                  {o' : O} {i' : Σₛ → Maybe (O × I)} →
                  oi ≡ just (o' , imap i') →
                  Σ[ o'' ∈ O ] Σ[ i'' ∈ I ] (oi ≡ just (o'' , i'') × (o' ⊑ₒ o'') × (imap i' ⊑ᵢ i''))

    ⊑ᵢ-refl-aux (just .(o' , imap i')) {o'} {i'} refl =
      o' , (imap i' , (refl , (⊑ₒ-refl , ⊑ᵢ-refl {imap i'})))

⊑ᵢ-trans : {i i' i'' : I} →
           i ⊑ᵢ i' →
           i' ⊑ᵢ i'' →
           -----------------
           i ⊑ᵢ i''

⊑ᵢ-trans {i} {i'} {i''} (rel p) (rel q) =
  rel (λ op {o} {j} r → ⊑ᵢ-trans-aux o j op (p op r))

  where
    ⊑ᵢ-trans-aux' : (o : O) → (j : I) → (op : Σₛ) →
                    (o' : O) → (j' : I) → lkpᵢ op i' ≡ just (o' , j') → (o ⊑ₒ o') → (j ⊑ᵢ j') →
                    Σ[ o'' ∈ O ] Σ[ j'' ∈ I ] (lkpᵢ op i'' ≡ just (o'' , j'') × (o' ⊑ₒ o'') × (j' ⊑ᵢ j'')) →
                    Σ[ o'' ∈ O ] Σ[ j'' ∈ I ] (lkpᵢ op i'' ≡ just (o'' , j'') × (o ⊑ₒ o'') × (j ⊑ᵢ j''))

    ⊑ᵢ-trans-aux' o j op o' j' r' s t (o'' , j'' , r'' , s' , t') =
      o'' , j'' , r'' , ⊑ₒ-trans s s' , ⊑ᵢ-trans t t'

    ⊑ᵢ-trans-aux : (o : O) → (j : I) → (op : Σₛ) →
                    Σ[ o' ∈ O ] Σ[ j' ∈ I ] (lkpᵢ op i' ≡ just (o' , j') × (o ⊑ₒ o') × (j ⊑ᵢ j')) →
                    Σ[ o'' ∈ O ] Σ[ j'' ∈ I ] (lkpᵢ op i'' ≡ just (o'' , j'') × (o ⊑ₒ o'') × (j ⊑ᵢ j''))

    ⊑ᵢ-trans-aux o j op (o' , j' , r' , s , t) =
      ⊑ᵢ-trans-aux' o j op o' j' r' s t (q op r')

-- SUBTYPING RELATIONS ARE PROOF-IRRELEVANT

≡-uip : {X : Set}
        {x x' : X} →
        (p q : x ≡ x') →
        ----------------
        p ≡ q

≡-uip refl refl = refl

⊑ₒ-irrelevant : {o o' : O}
                (p q : o ⊑ₒ o') →
                -----------------
                p ≡ q

⊑ₒ-irrelevant {omap o} {omap o'} p q =
  fun-ext (λ op → fun-ext (λ r → ⊑ₒ-irrelevant-aux r))

  where

    ⊑ₒ-irrelevant-aux : {op : Σₛ} →
                        (r : op ∈ₒ (omap o)) →
                        ----------------------
                        p op r ≡ q op r

    ⊑ₒ-irrelevant-aux {op} r with p op r | q op r
    ... | s | t = ≡-uip s t

⊑ᵢ-irrelevant : {i i' : I}
                (p q : i ⊑ᵢ i') →
                -----------------
                p ≡ q

⊑ᵢ-irrelevant {imap i} {imap i'} (rel p) (rel q) =
  cong (λ r → rel r) (fun-ext (λ op → ifun-ext (λ {o''} → ifun-ext (λ {i''} → fun-ext (λ r → ⊑ᵢ-irrelevant-aux r)))))

  where

    ⊑ᵢ-irrelevant-aux : {op : Σₛ}
                        {o'' : O}
                        {i'' : I} →
                        (r : i op ≡ just (o'' , i'')) →
                        -------------------------------
                        p op r ≡ q op r

    ⊑ᵢ-irrelevant-aux {op} r with p op r | q op r
    ... | o''' , i''' , s , s' , s'' | o'''' , i'''' , t , t' , t'' with trans (sym s) t
    ... | refl with ⊑ₒ-irrelevant s' t'
    ... | refl with ⊑ᵢ-irrelevant s'' t''
    ... | refl with ≡-uip s t
    ... | refl = refl

-- LEFT UNIT FOR UNIONS OF EFFECT ANNOTATIONS

∪ₒ-lunit : (o : O) →
           -----------
           ∅ₒ ∪ₒ o ≡ o

∪ₒ-lunit (omap o) =
  cong omap (fun-ext ∪ₒ-lunit-aux)

  where
    ∪ₒ-lunit-aux : (op : Σₛ) →
                   ----------------------------------
                   ∪ₒ-aux (λ _ → nothing) o op ≡ o op

    ∪ₒ-lunit-aux op with o op
    ... | nothing =
      refl
    ... | just _ =
      refl

∪ᵢ-lunit : (i : I) →
           -----------
           ∅ᵢ ∪ᵢ i ≡ i

∪ᵢ-lunit (imap i) = cong imap (fun-ext ∪ᵢ-lunit-aux)

  where
    ∪ᵢ-lunit-aux : (op : Σₛ) →
                   ----------------------------------
                   ∪ᵢ-aux (λ _ → nothing) i op ≡ i op

    ∪ᵢ-lunit-aux op with i op
    ... | nothing =
      refl
    ... | just _ =
      refl

-- LEFT AND RIGHT INCLUSIONS INTO UNIONS OF EFFECT ANNOTATIONS

∪ₒ-inl : {o o' : O} →
         -------------
         o ⊑ₒ (o ∪ₒ o')

∪ₒ-inl {omap o} {omap o'} op with o op | o' op
... | nothing | nothing = λ p → p
... | nothing | just tt = λ _ → refl
... | just tt | nothing = λ p → p
... | just tt | just tt = λ p → p

∪ₒ-inr : {o o' : O} →
         -------------
         o' ⊑ₒ (o ∪ₒ o')

∪ₒ-inr {omap o} {omap o'} op with o op | o' op
... | nothing | nothing = λ p → p
... | nothing | just tt = λ p → p
... | just tt | nothing = λ _ → refl
... | just tt | just tt = λ p → p

∪ᵢ-inl : {i i' : I} →
        -------------
        i ⊑ᵢ (i ∪ᵢ i')

∪ᵢ-inl {imap i} {imap i'} =
  rel (λ op → ∪ᵢ-inl-aux (i op) (i' op))

  where
    ∪ᵢ-inl-aux : (oi oi' : Maybe (O × I)) →
                 {o : O} {i'' : I} →
                 oi ≡ just (o , i'') →
                 Σ[ o' ∈ O ] Σ[ i''' ∈ I ] (∪ᵢ-aux' oi oi' ≡ just (o' , i''') × (o ⊑ₒ o') × (i'' ⊑ᵢ i'''))

    ∪ᵢ-inl-aux (just .(o , i'')) nothing {o} {i''} refl =
      o , i'' , refl , ⊑ₒ-refl , ⊑ᵢ-refl
    ∪ᵢ-inl-aux (just .(o , imap i'')) (just (o' , imap i''')) {o} {imap i''} refl =
      o ∪ₒ o' , imap (∪ᵢ-aux i'' i''') , refl , ∪ₒ-inl , ∪ᵢ-inl

∪ᵢ-inr : {i i' : I} →
        -------------
        i' ⊑ᵢ (i ∪ᵢ i')

∪ᵢ-inr {imap i} {imap i'} =
  rel (λ op → ∪ᵢ-inr-aux (i op) (i' op))

  where
    ∪ᵢ-inr-aux : (oi oi' : Maybe (O × I)) →
                 {o : O} {i'' : I} →
                 oi' ≡ just (o , i'') →
                 Σ[ o' ∈ O ] Σ[ i''' ∈ I ] (∪ᵢ-aux' oi oi' ≡ just (o' , i''') × (o ⊑ₒ o') × (i'' ⊑ᵢ i'''))

    ∪ᵢ-inr-aux nothing (just .(o , i'')) {o} {i''} refl =
      o , i'' , refl , ⊑ₒ-refl , ⊑ᵢ-refl
    ∪ᵢ-inr-aux (just (o' , imap i''')) (just .(o , imap i'')) {o} {imap i''} refl =
      o' ∪ₒ o , imap (∪ᵢ-aux i''' i'') , refl , ∪ₒ-inr , ∪ᵢ-inr

-- COPAIRING FOR UNIONS OF EFFECT ANNOTATIONS

∪ₒ-copair : {o o' o'' : O} →
            o ⊑ₒ o'' →
            o' ⊑ₒ o'' →
            ----------------
            (o ∪ₒ o') ⊑ₒ o''

∪ₒ-copair {omap o} {omap o'} {omap o''} p q op =
  ∪ₒ-copair-aux (p op) (q op)

  where
    ∪ₒ-copair-aux : (p : op ∈ₒ (omap o) → op ∈ₒ (omap o'')) →
                    (q : op ∈ₒ (omap o') → op ∈ₒ (omap o'')) →
                    ---------------------------------------------
                    op ∈ₒ (omap (∪ₒ-aux o o')) → op ∈ₒ (omap o'')

    ∪ₒ-copair-aux p q with o op | o' op
    ... | nothing | nothing = q
    ... | nothing | just tt = q
    ... | just tt | nothing = p
    ... | just tt | just tt = p

inj-just : {X : Set} {x x' : X} → just x ≡ just x' → x ≡ x'
inj-just refl = refl

inj-pair₁ : {X Y : Set} {x x' : X} {y y' : Y} → (x , y) ≡ (x' , y') → x ≡ x'
inj-pair₁ refl = refl

inj-pair₂ : {X Y : Set} {x x' : X} {y y' : Y} → (x , y) ≡ (x' , y') → y ≡ y'
inj-pair₂ refl = refl

∪ᵢ-copair : {i i' i'' : I} →
            i ⊑ᵢ i'' →
            i' ⊑ᵢ i'' →
            ----------------
            (i ∪ᵢ i') ⊑ᵢ i''

∪ᵢ-copair {imap i} {imap i'} {imap i''} (rel p) (rel q) =
  rel (λ op {o'''} {i'''} r → ∪ᵢ-copair-aux op o''' i''' (i op) (i' op) (i'' op) refl refl refl r)

  where
    ∪ᵢ-copair-aux : (op : Σₛ) →
                    (o''' : O) →
                    (i''' : I)
                    (oi oi' oi'' : Maybe (O × I)) →
                    (oi ≡ i op) →
                    (oi' ≡ i' op) →
                    (oi'' ≡ i'' op) →
                    (r : ∪ᵢ-aux' oi oi' ≡ just (o''' , i''')) →
                    Σ[ o' ∈ O ] Σ[ i'''' ∈ I ] (oi'' ≡ just (o' , i'''') × (o''' ⊑ₒ o') × (i''' ⊑ᵢ i''''))

    ∪ᵢ-copair-aux op o''' i''' nothing (just oi') nothing r s t u with trans t (proj₁ (proj₂ (proj₂ (q op (trans (sym s) u)))))
    ... | ()
    ∪ᵢ-copair-aux op o''' i''' nothing (just oi') (just oi'') r s t u =
      proj₁ (q op (trans (sym s) u)) ,
      proj₁ (proj₂ (q op (trans (sym s) u))) ,
      trans t (proj₁ (proj₂ (proj₂ (q op (trans (sym s) u))))) ,
      proj₁ (proj₂ (proj₂ (proj₂ (q op (trans (sym s) u))))) ,
      proj₂ (proj₂ (proj₂ (proj₂ (q op (trans (sym s) u)))))
    ∪ᵢ-copair-aux op o''' i''' (just oi) nothing oi'' r s t u =
      proj₁ (p op (trans (sym r) u)) ,
      proj₁ (proj₂ (p op (trans (sym r) u))) ,
      trans t (proj₁ (proj₂ (proj₂ (p op (trans (sym r) u))))) ,
      proj₁ (proj₂ (proj₂ (proj₂ (p op (trans (sym r) u))))) ,
      proj₂ (proj₂ (proj₂ (proj₂ (p op (trans (sym r) u)))))
    ∪ᵢ-copair-aux op o''' i'''
                  (just (omap o'''' , imap i''''))
                  (just (omap o''''' , imap i'''''))
                  nothing r s t u
                  with trans t (proj₁ (proj₂ (proj₂ (p op (sym r)))))
    ... | ()
    ∪ᵢ-copair-aux op o''' i'''
                  (just (omap o'''' , imap i''''))
                  (just (omap o''''' , imap i'''''))
                  (just (omap o'''''' , imap i''''''))
                  r s t u =
      omap o'''''' ,
      imap i'''''' ,
      refl ,
      subst (λ o → o ⊑ₒ omap o'''''')
            (inj-pair₁ (inj-just u))
            (∪ₒ-copair (subst (λ o → omap o'''' ⊑ₒ o)
                              (inj-pair₁ (inj-just (sym (trans t (proj₁ (proj₂ (proj₂ (p op (sym r)))))))))
                              (proj₁ (proj₂ (proj₂ (proj₂ (p op (sym r)))))))
                       (subst (λ o → omap o''''' ⊑ₒ o)
                              (inj-pair₁ (inj-just (sym (trans t (proj₁ (proj₂ (proj₂ (q op (sym s)))))))))
                              (proj₁ (proj₂ (proj₂ (proj₂ (q op (sym s)))))))) ,
      subst (λ i → i ⊑ᵢ imap i'''''')
            (inj-pair₂ (inj-just u))
            (∪ᵢ-copair (subst (λ i → imap i'''' ⊑ᵢ i)
                               (inj-pair₂ (inj-just (sym (trans t (proj₁ (proj₂ (proj₂ (p op (sym r)))))))))
                               (proj₂ (proj₂ (proj₂ (proj₂ (p op (sym r)))))))
                       (subst (λ i → imap i''''' ⊑ᵢ i)
                               (inj-pair₂ (inj-just (sym (trans t (proj₁ (proj₂ (proj₂ (q op (sym s)))))))))
                               (proj₂ (proj₂ (proj₂ (proj₂ (q op (sym s))))))))

-- FUNCTORIALITY OF UNIONS OF EFFECT ANNOTATIONS

∪ₒ-fun : {o o' o'' o''' : O} →
         o ⊑ₒ o'' →
         o' ⊑ₒ o''' →
         --------------------------
         (o ∪ₒ o') ⊑ₒ (o'' ∪ₒ o''')

∪ₒ-fun p q =
  ∪ₒ-copair (⊑ₒ-trans p ∪ₒ-inl) (⊑ₒ-trans q ∪ₒ-inr)

∪ᵢ-fun : {i i' i'' i''' : I} →
         i ⊑ᵢ i'' →
         i' ⊑ᵢ i''' →
         --------------------------
         (i ∪ᵢ i') ⊑ᵢ (i'' ∪ᵢ i''')

∪ᵢ-fun p q =
  ∪ᵢ-copair (⊑ᵢ-trans p ∪ᵢ-inl) (⊑ᵢ-trans q ∪ᵢ-inr)

-- UNIONS OF INTERRUPT ANNOTATIONS ARE GIVEN BY POINTWISE UNIONS

∪ᵢ-∪ₒ : {op : Σₛ}
        {o'' o''' o'''' : O}
        {i i' i'' i''' i'''' : I} →
        lkpᵢ op (i ∪ᵢ i') ≡ just (o'' , i'') →
        lkpᵢ op i ≡ just (o''' , i''') →
        lkpᵢ op i' ≡ just (o'''' , i'''') →
        ---------------------------------------
        o'' ≡ o''' ∪ₒ o''''

∪ᵢ-∪ₒ {op} {o''} {o'''} {o''''} {imap i} {imap i'} p q r with i op | i' op
∪ᵢ-∪ₒ {op} {.(o''' ∪ₒ o'''')} {o'''} {o''''} {imap i} {imap i'} {_} {imap i'''} {imap i''''}
  refl refl refl | just .(o''' , imap i''') | just .(o'''' , imap i'''') =
    refl

∪ᵢ-∪ᵢ : {op : Σₛ}
        {o'' o''' o'''' : O}
        {i i' i'' i''' i'''' : I} →
        lkpᵢ op (i ∪ᵢ i') ≡ just (o'' , i'') →
        lkpᵢ op i ≡ just (o''' , i''') →
        lkpᵢ op i' ≡ just (o'''' , i'''') →
        ---------------------------------------
        i'' ≡ i''' ∪ᵢ i''''

∪ᵢ-∪ᵢ {op} {o''} {o'''} {o''''} {imap i} {imap i'} p q r with i op | i' op
∪ᵢ-∪ᵢ {op} {.(o''' ∪ₒ o'''')} {o'''} {o''''} {imap i} {imap i'} {_} {imap i'''} {imap i''''}
  refl refl refl | just .(o''' , imap i''') | just .(o'''' , imap i'''') =
    refl

-- INCLUSION INTO ACTED UPON EFFECT ANNOTATION

{- LEMMA 3.1 (1) -}

↓ₑ-⊑ₒ : {o : O}
        {i : I}
        {op : Σₛ} →
        --------------------------
        o ⊑ₒ proj₁ (op ↓ₑ (o , i))

↓ₑ-⊑ₒ {omap o} {imap i} {op} op' p with i (op)
... | nothing = p
... | just (o' , i') = ∪ₒ-inl op' p

{- LEMMA 3.1 (2) - the O part -}

↓ₑ-⊑ₒ-o' : {o o' : O}
           {i i' : I}
           {op : Σₛ} →
           lkpᵢ op i ≡ just (o' , i') →
           ---------------------------
           o' ⊑ₒ proj₁ (op ↓ₑ (o , i))

↓ₑ-⊑ₒ-o' {omap o} {omap o'} {imap i} {imap i'} {op} p with i (op)
↓ₑ-⊑ₒ-o' {omap o} {omap o'} {imap i} {imap i'} {op} refl | just .(omap o' , imap i') =
  ↓ₑ-⊑ₒ-o'-aux

  where
    ↓ₑ-⊑ₒ-o'-aux : (op' : Σₛ) → o' op' ≡ just tt → ∪ₒ-aux o o' op' ≡ just tt
    ↓ₑ-⊑ₒ-o'-aux op' p with o op'
    ↓ₑ-⊑ₒ-o'-aux op' p | nothing = p
    ↓ₑ-⊑ₒ-o'-aux op' p | just tt = refl

{- LEMMA 3.1 (2) - the I part -}

↓ₑ-⊑ₒ-i' : {o o' : O}
           {i i' : I}
           {op : Σₛ} →
           lkpᵢ op i ≡ just (o' , i') →
           ---------------------------
           i' ⊑ᵢ proj₂ (op ↓ₑ (o , i))

↓ₑ-⊑ₒ-i' {omap o} {omap o'} {imap i} {imap i'} {op} p with i (op)
↓ₑ-⊑ₒ-i' {omap o} {omap o'} {imap i} {imap i'} {op} refl | just .(omap o' , imap i') =
  rel ↓ₑ-⊑ₒ-i'-aux

  where
    ↓ₑ-⊑ₒ-i'-aux : (op' : Σₛ) {o'' : O} {i'' : I} →
      i' op' ≡ just (o'' , i'') →
      Σ[ o''' ∈ O ] Σ[ i''' ∈ I ] (∪ᵢ-aux (λ op' → if op ≡ op' then nothing else i op') i' op' ≡ just (o''' , i''') ×
                                  (o'' ⊑ₒ o''') × (i'' ⊑ᵢ i'''))
    ↓ₑ-⊑ₒ-i'-aux op' {o''} {i''} p with decₛ op op'
    ↓ₑ-⊑ₒ-i'-aux op' {o''} {i''} p | yes refl with i' (op)
    ↓ₑ-⊑ₒ-i'-aux op' {o''} {i''} refl | yes refl | just .(o'' , i'') =
      o'' , (i'' , refl , (⊑ₒ-refl , ⊑ᵢ-refl))
    ↓ₑ-⊑ₒ-i'-aux op' {o''} {i''} p | no ¬q with i (op') | i' (op')
    ↓ₑ-⊑ₒ-i'-aux op' {o''} {i''} refl | no ¬q | nothing | just .(o'' , i'') =
      o'' , (i'' , refl , (⊑ₒ-refl , ⊑ᵢ-refl))
    ↓ₑ-⊑ₒ-i'-aux op' {o''} {imap i''} refl | no ¬q | just (o''' , (imap i''')) | just .(o'' , (imap i'')) =
      (o''' ∪ₒ o'') , (imap (∪ᵢ-aux i''' i'') , (refl , (∪ₒ-inr , ∪ᵢ-inr)))

-- EFFECT ANNOTATION OF AN INTERRUPT THAT WAS NOT ACTED WITH

{- LEMMA 3.1 (3) -}

lkpᵢ-↓ₑ-neq : {o o' : O}
              {i i' : I} {op op' : Σₛ} →
              ¬ op ≡ op' →
              lkpᵢ op' i ≡ just (o' , i') →
              -------------------------------------------------------------------------------------------------------
              Σ[ o'' ∈ O ] Σ[ i'' ∈ I ] (lkpᵢ op' (proj₂ (op ↓ₑ (o , i))) ≡ just (o'' , i'') × o' ⊑ₒ o'' × i' ⊑ᵢ i'')

lkpᵢ-↓ₑ-neq {omap o} {o'} {imap i} {imap i'} {op} {op'} p q with i (op)
... | nothing =
  o' , imap i' , q , ⊑ₒ-refl , ⊑ᵢ-refl
lkpᵢ-↓ₑ-neq {omap o} {o'} {imap i} {imap i'} {op} {op'} p q | just (o'' , imap i'') with decₛ op op'
... | yes r with p r
... | ()
lkpᵢ-↓ₑ-neq {omap o} {o'} {imap i} {imap i'} {op} {op'} p q | just (o'' , imap i'') | no ¬r with i (op') | i'' (op')
lkpᵢ-↓ₑ-neq {omap o} {.o'''} {imap i} {imap i'} {op} {op'} p refl |
  just (o'' , imap i'') | no ¬r | just (o''' , .(imap i')) | nothing =
    o''' , imap i' , refl , ⊑ₒ-refl , ⊑ᵢ-refl
... | just (o''' , imap i''') | just (o'''' , imap i'''') with q
lkpᵢ-↓ₑ-neq {omap o} {.o'''} {imap i} {imap .i'''} {op} {op'} p q |
  just (o'' , imap i'') | no ¬r | just (o''' , imap i''') | just (o'''' , imap i'''') | refl =
    (o''' ∪ₒ o'''') , (imap i''') ∪ᵢ (imap i'''') , refl , ∪ₒ-inl , ∪ᵢ-inl

-- NEXT DEFINED EFFECT ANNOTATION UNDER SUBTYPING EFFECT ANNOTATIONS

lkpᵢ-nextₒ : {o'' : O} {i i' i'' : I} {op : Σₛ} →
            i ⊑ᵢ i' → lkpᵢ op i ≡ just (o'' , i'') → O

lkpᵢ-nextₒ {o''} {i} {i'} {i''} {op} (rel p) q =
  proj₁ (p op q)

lkpᵢ-nextᵢ : {o'' : O} {i i' i'' : I} {op : Σₛ} →
            i ⊑ᵢ i' → lkpᵢ op i ≡ just (o'' , i'') → I

lkpᵢ-nextᵢ {o''} {i} {i'} {i''} {op} (rel p) q =
  proj₁ (proj₂ (p op q))

lkpᵢ-next-eq : {o'' : O} {i i' i'' : I} {op : Σₛ} →
              (p : i ⊑ᵢ i') →
              (q : lkpᵢ op i ≡ just (o'' , i'')) →
              ------------------------------------------------
              lkpᵢ op i' ≡ just (lkpᵢ-nextₒ p q , lkpᵢ-nextᵢ p q)

lkpᵢ-next-eq {o''} {i} {i'} {i''} {op} (rel p) q =
  proj₁ (proj₂ (proj₂ (p op q)))

lkpᵢ-next-⊑ₒ : {o'' : O} {i i' i'' : I} {op : Σₛ} →
              (p : i ⊑ᵢ i') →
              (q : lkpᵢ op i ≡ just (o'' , i'')) →
              -----------------------------------
              o'' ⊑ₒ lkpᵢ-nextₒ p q

lkpᵢ-next-⊑ₒ {o''} {i} {i'} {i''} {op} (rel p) q =
  proj₁ (proj₂ (proj₂ (proj₂ (p op q))))

lkpᵢ-next-⊑ᵢ : {o'' : O} {i i' i'' : I} {op : Σₛ} →
              (p : i ⊑ᵢ i') →
              (q : lkpᵢ op i ≡ just (o'' , i'')) →
              -----------------------------------
              i'' ⊑ᵢ lkpᵢ-nextᵢ p q

lkpᵢ-next-⊑ᵢ {o''} {i} {i'} {i''} {op} (rel p) q =
  proj₂ (proj₂ (proj₂ (proj₂ (p op q))))

-- ACTION OF INTERRUPTS ON EFFECT ANNOTATIONS IS MONOTONIC

mutual
  ↓ₑ-monotonicₒ : {o o' : O}
                  {i i' : I}
                  {op : Σₛ} →
                  o ⊑ₒ o' →
                  i ⊑ᵢ i' →
                  ------------------------------------------------
                  proj₁ (op ↓ₑ (o , i)) ⊑ₒ proj₁ (op ↓ₑ (o' , i'))

  ↓ₑ-monotonicₒ {omap o} {omap o'} {imap i} {imap i'} {op} p (rel q) =
    ↓ₑ-monotonicₒ-aux (i op) (i' op) refl refl

    where
      ↓ₑ-monotonicₒ-aux : (oi oi' : Maybe (O × I)) →
                          i op ≡ oi →
                          i' op ≡ oi' →
                          ----------------------------
                          ↓ₑ-auxₒ op oi (omap o)
                          ⊑ₒ
                          ↓ₑ-auxₒ op oi' (omap o')

      ↓ₑ-monotonicₒ-aux nothing nothing r s =
        p
      ↓ₑ-monotonicₒ-aux nothing (just (omap o''' , imap i''')) r s =
        ⊑ₒ-trans p ∪ₒ-inl
      ↓ₑ-monotonicₒ-aux (just (omap o'' , imap i'')) nothing r s with trans (sym s) (proj₁ (proj₂ (proj₂ (q op r))))
      ... | ()
      ↓ₑ-monotonicₒ-aux (just (omap o'' , imap i'')) (just (omap o''' , imap i''')) r s with trans (sym s) (proj₁ (proj₂ (proj₂ (q op r))))
      ... | t =
        ∪ₒ-fun p (⊑ₒ-trans (proj₁ (proj₂ (proj₂ (proj₂ (q op r)))))
                           (subst (λ o → o ⊑ₒ omap o''') (inj-pair₁ (inj-just t)) ⊑ₒ-refl))

  ↓ₑ-monotonicᵢ : {o o' : O}
                {i i' : I}
                {op : Σₛ} →
                o ⊑ₒ o' →
                i ⊑ᵢ i' →
                ------------------------------------------------
                proj₂ (op ↓ₑ (o , i)) ⊑ᵢ proj₂ (op ↓ₑ (o' , i'))

  ↓ₑ-monotonicᵢ {omap o} {omap o'} {imap i} {imap i'} {op} p (rel q) =
    ↓ₑ-monotonicᵢ-aux (i op) (i' op) refl refl

    where
      ↓ₑ-monotonicᵢ-aux : (oi oi' : Maybe (O × I)) →
                          oi ≡ i op →
                          oi' ≡ i' op →
                          -----------------------------------------
                          ↓ₑ-auxᵢ op oi (imap i)
                          ⊑ᵢ
                          ↓ₑ-auxᵢ op oi' (imap i')

      ↓ₑ-monotonicᵢ-aux nothing nothing r s =
        rel q
      ↓ₑ-monotonicᵢ-aux nothing (just (omap o''' , imap i''')) r s =
        ⊑ᵢ-trans (rel (λ op' {o''''} {i''''} t → ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t))
                 (∪ᵢ-inl {(imap i') [ op ↦ nothing ]ᵢ} {imap i'''})

        where
          ↓ₑ-monotonicᵢ-aux' : (op' : Σₛ) →
                               (o'''' : O) →
                               (i'''' : I) →
                               i op' ≡ just (o'''' , i'''') →
                               --------------------------------------------------------------------
                               Σ[ o''''' ∈ O ] Σ[ i''''' ∈ I ]
                                 ((if op ≡ op' then nothing else i' op') ≡ just (o''''' , i''''') ×
                                  (o'''' ⊑ₒ o''''') × (i'''' ⊑ᵢ i'''''))

          ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t with decₛ op op'
          ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t | yes refl with trans r t
          ... | ()
          ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t | no ¬u =
            lkpᵢ-nextₒ (rel q) t ,
            lkpᵢ-nextᵢ (rel q) t ,
            lkpᵢ-next-eq (rel q) t ,
            lkpᵢ-next-⊑ₒ (rel q) t ,
            lkpᵢ-next-⊑ᵢ (rel q) t

      ↓ₑ-monotonicᵢ-aux (just (omap o'' , imap i'')) nothing r s with trans s (proj₁ (proj₂ (proj₂ (q op (sym r)))))
      ... | ()

      ↓ₑ-monotonicᵢ-aux (just (omap o'' , imap i'')) (just (omap o''' , imap i''')) r s =
        ∪ᵢ-fun {_}
               {imap i''}
               {_}
               {imap i'''}
               (rel λ op' {o''''} {i''''} t → ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t)
               (subst (λ i → imap i'' ⊑ᵢ i)
                      (sym (inj-pair₂ (inj-just (trans s (proj₁ (proj₂ (proj₂ (q op (sym r)))))))))
                      (proj₂ (proj₂ (proj₂ (proj₂ (q op (sym r)))))))

        where
          ↓ₑ-monotonicᵢ-aux' : (op' : Σₛ) →
                               (o'''' : O) →
                               (i'''' : I) →
                               lkpᵢ op' (imap i [ op ↦ nothing ]ᵢ)  ≡ just (o'''' , i'''') →
                               --------------------------
                               Σ[ o''''' ∈ O ] Σ[ i''''' ∈ I ]
                                 (lkpᵢ op' (imap i' [ op ↦ nothing ]ᵢ)
                                  ≡ just (o''''' , i''''') ×
                                  (o'''' ⊑ₒ o''''') × (i'''' ⊑ᵢ i'''''))

          ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t with decₛ op op'
          ↓ₑ-monotonicᵢ-aux' op' o'''' i'''' t | no ¬u =
            lkpᵢ-nextₒ (rel q) t ,
            lkpᵢ-nextᵢ (rel q) t ,
            lkpᵢ-next-eq (rel q) t ,
            lkpᵢ-next-⊑ₒ (rel q) t ,
            lkpᵢ-next-⊑ᵢ (rel q) t

-- GENERALISED ACTION OF INTERRUPTS ON EFFECT ANNOTATIONS IS MONOTONIC

mutual
  ↓↓ₑ-monotonicₒ : {o o' : O}
                   {i i' : I} →
                   (ops : List Σₛ) →
                   o ⊑ₒ o' →
                   i ⊑ᵢ i' →
                   ----------------------------------------------------
                   proj₁ (ops ↓↓ₑ (o , i)) ⊑ₒ proj₁ (ops ↓↓ₑ (o' , i'))

  ↓↓ₑ-monotonicₒ {omap o} {omap o'} {imap i} {imap i'} [] p q =
    p
  ↓↓ₑ-monotonicₒ (op ∷ ops) p q =
    ↓ₑ-monotonicₒ (↓↓ₑ-monotonicₒ ops p q) (↓↓ₑ-monotonicᵢ ops p q)

  ↓↓ₑ-monotonicᵢ : {o o' : O}
                   {i i' : I} →
                   (ops : List Σₛ) →
                   o ⊑ₒ o' →
                   i ⊑ᵢ i' →
                   ----------------------------------------------------
                   proj₂ (ops ↓↓ₑ (o , i)) ⊑ᵢ proj₂ (ops ↓↓ₑ (o' , i'))

  ↓↓ₑ-monotonicᵢ [] p q = q
  ↓↓ₑ-monotonicᵢ (op ∷ ops) p q =
    ↓ₑ-monotonicᵢ (↓↓ₑ-monotonicₒ ops p q) (↓↓ₑ-monotonicᵢ ops p q)

-- INCLUSION INTO GENERALLY ACTED UPON EFFECT ANNOTATION

↓↓ₑ-⊑ₒ : {o : O}
         {i : I} →
         (ops : List Σₛ) →
         --------------------------
         o ⊑ₒ proj₁ (ops ↓↓ₑ (o , i))

↓↓ₑ-⊑ₒ [] =
  ⊑ₒ-refl
↓↓ₑ-⊑ₒ (op ∷ ops) =
  ⊑ₒ-trans (↓↓ₑ-⊑ₒ ops) (↓ₑ-⊑ₒ {op = op})

-- A PATH OF INTERRUPT NAMES THAT REVEALS THE GIVEN SIGNAL IN AN EFFECT ANNOTATION

data _`at_`in_,_ (op : Σₛ) : List Σₛ → O → I → Set where

  stop : {o : O}
         {i : I} →
         op ∈ₒ o →
         -------------------
         op `at [] `in o , i

  next : {o o' : O}
         {i i' : I}
         {op' : Σₛ}
         {ops : List Σₛ} →
         lkpᵢ op' i ≡ just (o' , i') →
         op `at ops `in o' , i' →
         -----------------------------
         op `at (op' ∷ ops) `in o , i

-- ACTING ON AN ANNOTATION WITH EMPTY SIGNALS PART JUST REVEALS THE INNER LAYER IF THE INTERRUPTS MATCH

↓ₑ-∅-↦-≡ : {op : Σₛ}
           {o : O}
           {i : I} →
           -----------------------------
           op ↓ₑ (∅ₒ , imap (λ op' → if op' ≡ op then just (o , i) else nothing))
           ≡
           (o , i)

↓ₑ-∅-↦-≡ {op} {o} {i} with decₛ op op
↓ₑ-∅-↦-≡ {op} {omap o} {i} | yes refl =
  cong₂ (λ x y → x , y)
        (∪ₒ-lunit (omap o))
        (trans (cong (λ i' → i' ∪ᵢ i) ↓ₑ-∅-↦-≡-aux) (∪ᵢ-lunit i))

  where
    ↓ₑ-∅-↦-≡-aux : imap (λ op' → if op ≡ op' then nothing else (if op' ≡ op then just (omap o , i) else nothing))
                   ≡
                   ∅ᵢ

    ↓ₑ-∅-↦-≡-aux = cong imap (fun-ext ↓ₑ-∅-↦-≡-aux-aux)

      where
        ↓ₑ-∅-↦-≡-aux-aux : (op' : Σₛ) →
                           ---------------------------------------------------------------------------------
                           (if op ≡ op' then nothing else (if op' ≡ op then just (omap o , i) else nothing))
                           ≡
                           nothing

        ↓ₑ-∅-↦-≡-aux-aux op' with decₛ op op'
        ... | yes refl =
          refl
        ... | no ¬p =
          ite-≢ (λ q → ¬p (sym q))

↓ₑ-∅-↦-≡ {op} {o} {i} | no ¬p =
  ⊥-elim (¬p refl)

-- ACTING ON AN ANNOTATION WITH EMPTY SIGNALS IS IDEMPOTENT IF THE INTERRUPTS DO NOT MATCH

↓ₑ-∅-↦-≢ : {op op' : Σₛ}
           {o : O}
           {i : I} →
           op ≢ op' →
           -----------------------------
           op' ↓ₑ (∅ₒ , imap (λ op'' → if op'' ≡ op then just (o , i) else nothing))
           ≡
           (∅ₒ , imap (λ op'' → if op'' ≡ op then just (o , i) else nothing))

↓ₑ-∅-↦-≢ {op} {op'} p with decₛ op' op
↓ₑ-∅-↦-≢ {op} {.op} p | yes refl =
  ⊥-elim (p refl)
↓ₑ-∅-↦-≢ {op} {op'} p | no ¬q =
  refl

-- A MINIMAL EFFECT ANNOTATION SUCH THAT A GIVEN PATH OF INTERRUPTS REVEALS THE GIVEN SIGNAL NAME

mutual
  ⦃⦃_↦_⦄⦄ₒ : List Σₛ → Σₛ → O
  ⦃⦃ [] ↦ op ⦄⦄ₒ =
    omap (λ op' → if op ≡ op' then just tt else nothing)
  ⦃⦃ op' ∷ ops ↦ op ⦄⦄ₒ =
    ∅ₒ

  ⦃⦃_↦_⦄⦄ᵢ : List Σₛ → Σₛ → I
  ⦃⦃ [] ↦ op ⦄⦄ᵢ =
    ∅ᵢ
  ⦃⦃ op' ∷ ops ↦ op ⦄⦄ᵢ =
    imap (λ op'' → if op'' ≡ op' then just (⦃⦃ ops ↦ op ⦄⦄ₒ , ⦃⦃ ops ↦ op ⦄⦄ᵢ) else nothing)

-- IF THERE IS A PATH TO A SIGNAL IN AN EFFECT ANNOTATION, THE MINIMAL EFFECT ANNOTATION IS INCLUDED IN IT

mutual
  `at-minₒ : {op : Σₛ}
             {ops : List Σₛ}
             {o : O}
             {i : I} →
             op `at ops `in o , i →
             ----------------------
             ⦃⦃ ops ↦ op ⦄⦄ₒ ⊑ₒ o

  `at-minₒ {op} {_} {omap o} (stop p) op' with decₛ op op'
  `at-minₒ {.op'} {.[]} {omap o} (stop p) op' | yes refl =
    λ _ → p
  `at-minₒ {op} {.[]} {omap o} (stop p) op'' | no ¬q =
    λ ()
  `at-minₒ (next p q) op'' =
    λ ()

  `at-minᵢ : {op : Σₛ}
             {ops : List Σₛ}
             {o : O}
             {i : I} →
             op `at ops `in o , i →
             ----------------------
             ⦃⦃ ops ↦ op ⦄⦄ᵢ ⊑ᵢ i

  `at-minᵢ (stop p) =
    rel (λ op'' → λ ())
  `at-minᵢ {op} (next {o} {o'} {i} {i'} {op'} {ops} p q) =
    rel (λ op'' {o''} {i''} r → `at-minᵢ-aux r)

    where
      `at-minᵢ-aux : {op'' : Σₛ}
                     {o'' : O}
                     {i'' : I} →
                     lkpᵢ op'' ⦃⦃ op' ∷ ops ↦ op ⦄⦄ᵢ ≡ just (o'' , i'') →
                     ---------------------------------------------------
                     Σ[ o''' ∈ O ]
                     Σ[ i''' ∈ I ]
                     (lkpᵢ op'' i ≡ just (o''' , i''') ×
                      (o'' ⊑ₒ o''') ×
                      (i'' ⊑ᵢ i'''))

      `at-minᵢ-aux {op''} p with decₛ op'' op'
      `at-minᵢ-aux {op'} refl | yes refl =
        o' , i' , p , `at-minₒ q , `at-minᵢ q

-- SUBPATHS OF (INTERRUPT) NAMES

data _⊆_ : List Σₛ → List Σₛ → Set where

  [] : {ops' : List Σₛ} →
         ----------------
         [] ⊆ ops'

  ∷-≡  : {op : Σₛ}
         {ops ops' : List Σₛ} →
         ops ⊆ ops' →
         ------------------------
         (op ∷ ops) ⊆ (op ∷ ops')

  ∷-≢  : {op op' : Σₛ}
         {ops ops' : List Σₛ} →
         op ≢ op' →
         (op ∷ ops) ⊆ ops' →
         -------------------------
         (op ∷ ops) ⊆ (op' ∷ ops')

mutual
  ∷-≢-swap : {op op' : Σₛ}
             {ops ops' : List Σₛ} →
             op ≢ op' →
             (op ∷ ops) ⊆ (op' ∷ op ∷ ops') →
             --------------------------------
             (op ∷ ops) ⊆ (op ∷ op' ∷ ops')

  ∷-≢-swap {op} {.op} {ops} {ops'} p (∷-≡ q) =
    ∷-≡ q
  ∷-≢-swap {op} {op'} {ops} {ops'} p (∷-≢ q (∷-≡ r)) =
    ∷-≡ (∷-∷ r)
  ∷-≢-swap {op} {op'} {ops} {ops'} p (∷-≢ q (∷-≢ r s)) =
    ⊥-elim (r refl)

  ∷-∷ : {op' : Σₛ}
        {ops : List Σₛ} →
        {ops' : List Σₛ} →
        ops ⊆ ops' →
        -------------------
        ops ⊆ (op' ∷ ops')

  ∷-∷ [] = []
  ∷-∷ {op'} (∷-≡ {op} p) with decₛ op op'
  ∷-∷ {.op} (∷-≡ {op} p) | yes refl =
    ∷-≡ (∷-∷ p)
  ∷-∷ {op'} (∷-≡ {op} p) | no ¬q =
    ∷-≢ ¬q (∷-≡ p)
  ∷-∷ {op'} (∷-≢ {op} {op''} p q) with decₛ op op'
  ∷-∷ {.op} (∷-≢ {op} {op''} p q) | yes refl = ∷-≢-swap p (∷-≢ p (∷-∷ q))
  ∷-∷ {op'} (∷-≢ {op} {op''} p q) | no ¬r = ∷-≢ ¬r (∷-≢ p q)

-- IF A SUBPATH OF INTERRUPTS REVEALS A SIGNAL, THEN ACTING WITH THE WHOLE PATH ALSO REVEALS IT

⊆-↓↓ : {op : Σₛ}
       {ops ops' : List Σₛ} →
       ops ⊆ ops' →
       ---------------------------------------------------------------
       op ∈ₒ proj₁ (reverse ops' ↓↓ₑ (⦃⦃ ops ↦ op ⦄⦄ₒ , ⦃⦃ ops ↦ op ⦄⦄ᵢ))

⊆-↓↓ {op} {ops} {ops'} [] =
  (↓↓ₑ-⊑ₒ (reverse ops')) op ⊆-↓↓-aux

  where
    ⊆-↓↓-aux : (if op ≡ op then just tt else nothing) ≡ just tt
    ⊆-↓↓-aux with decₛ op op
    ⊆-↓↓-aux | yes refl =
      refl
    ⊆-↓↓-aux | no ¬p =
      ⊥-elim (¬p refl)

⊆-↓↓ {op} (∷-≡ {op'} {ops} {ops'} p) =
  subst (λ ops'' → op ∈ₒ proj₁ (ops'' ↓↓ₑ (⦃⦃ (op' ∷ ops) ↦ op ⦄⦄ₒ , ⦃⦃ (op' ∷ ops) ↦ op ⦄⦄ᵢ)))
        (sym (unfold-reverse op' ops'))
        (subst (λ oi → op ∈ₒ proj₁ oi)
               (sym (↓↓ₑ-act (reverse ops') [ op' ]))
               (subst (λ oi → op ∈ₒ proj₁ (reverse ops' ↓↓ₑ oi))
                      (sym ↓ₑ-∅-↦-≡)
                      (⊆-↓↓ p)))

⊆-↓↓ {op} (∷-≢ {op'} {op''} {ops} {ops'} p q) =
  subst (λ ops'' → op ∈ₒ proj₁ (ops'' ↓↓ₑ (⦃⦃ (op' ∷ ops) ↦ op ⦄⦄ₒ , ⦃⦃ (op' ∷ ops) ↦ op ⦄⦄ᵢ)))
        (sym (unfold-reverse op'' ops'))
        (subst (λ oi → op ∈ₒ proj₁ oi)
               (sym (↓↓ₑ-act (reverse ops') [ op'' ]))
               (subst (λ oi → op ∈ₒ proj₁ (reverse ops' ↓↓ₑ oi))
                      (sym (↓ₑ-∅-↦-≢ p))
                      (⊆-↓↓ q)))

-- IF A PATH REVEALS A SIGNAL IN A UNION OF EFFECT ANNOTATIONS, THE PATH REVEALS THE SIGNAL IN ONE OF THE SUMMANDS

`at-⊎ : {op : Σₛ}
        {ops : List Σₛ}
        {o o' : O}
        {i i' : I} →
        op `at ops `in (o ∪ₒ o') , (i ∪ᵢ i') →
        -------------------------------------------------
        (op `at ops `in o , i) ⊎ (op `at ops `in o' , i')

`at-⊎ {op} {ops} {omap o} {omap o'} {i} {i'} (stop p) =
  `at-⊎-aux p (o op) (o' op) refl refl

  where
    `at-⊎-aux : (∪ₒ-aux o o' op ≡ just tt) →
                (t t' : Maybe ⊤) →
                o op ≡ t →
                o' op ≡ t' →
                -----------------------------------------------------------
                (op `at ops `in omap o , i) ⊎ (op `at ops `in omap o' , i')

    `at-⊎-aux p nothing nothing q r with o op | o' op
    `at-⊎-aux () nothing nothing q r | nothing | nothing
    `at-⊎-aux p nothing nothing q () | nothing | just tt
    `at-⊎-aux p nothing (just tt) q r =
      inj₂ (stop r)
    `at-⊎-aux p (just tt) t' q r =
      inj₁ (stop q)

`at-⊎ {op} {_} {o} {o'} {imap i} {imap i'} (next {o''} {o'''} {i''} {i'''} {op'} {ops} p q) =
  `at-⊎-aux p q (i op') (i' op') refl refl

  where
    `at-⊎-aux : ∪ᵢ-aux i i' op' ≡ just (o''' , i''') →
                op `at ops `in o''' , i''' →
                (oi oi' : Maybe (O × I)) →
                i op' ≡ oi →
                i' op' ≡ oi' →
                ---------------------------------------------------------------------------
                (op `at (op' ∷ ops) `in o , imap i) ⊎ (op `at (op' ∷ ops) `in o' , imap i')

    `at-⊎-aux p q nothing nothing r s with i op' | i' op'
    `at-⊎-aux () q nothing nothing r s | nothing | nothing
    `at-⊎-aux p q nothing nothing r () | nothing | just _
    `at-⊎-aux p q nothing (just (o'''' , i'''')) r s =
      inj₂ (next (trans (sym (`at-⊎-aux-aux r s)) p) q)

      where
        `at-⊎-aux-aux : i op' ≡ nothing →
                        i' op' ≡ just (o'''' , i'''') →
                        -------------------------------
                        ∪ᵢ-aux i i' op' ≡ i' op'

        `at-⊎-aux-aux r s with i op' | i' op'
        `at-⊎-aux-aux r s | nothing | just _ =
          refl

    `at-⊎-aux p q (just (o'''' , i'''')) nothing r s =
      inj₁ (next (trans (sym (`at-⊎-aux-aux r s)) p) q)

      where
        `at-⊎-aux-aux : i op' ≡ just (o'''' , i'''') →
                        i' op' ≡ nothing →
                        -------------------------------
                        ∪ᵢ-aux i i' op' ≡ i op'

        `at-⊎-aux-aux r s with i op' | i' op'
        `at-⊎-aux-aux r s | just _ | nothing =
          refl

    `at-⊎-aux p q (just (o'''' , i'''')) (just (o''''' , i''''')) r s
      with ∪ᵢ-∪ₒ {i = imap i} {i' = imap i'} p r s | ∪ᵢ-∪ᵢ {i = imap i} {i' = imap i'} p r s
    ... | refl | refl with `at-⊎ q
    ... | inj₁ t =
      inj₁ (next r t)
    ... | inj₂ t =
      inj₂ (next s t)

-- IF ACTING WITH A PATH REVEALS A SIGNAL, THEN THERE IS A SUBPATH TO THAT SIGNAL

↓↓-⊆-rw : (o : O)
          (i : I)
          (op : Σₛ)
          (ops : List Σₛ) →
          ----------------------------------------------------------------
          reverse (op ∷ ops) ↓↓ₑ (o , i) ≡ reverse ops ↓↓ₑ (op ↓ₑ (o , i))

↓↓-⊆-rw o i op ops =
  trans (cong (λ ops' → ops' ↓↓ₑ (o , i)) (unfold-reverse op ops))
        (↓↓ₑ-act (reverse ops) [ op ])

↓↓-⊆ : {op : Σₛ} →
       (ops : List Σₛ) →
       {o : O}
       {i : I} →
       op ∈ₒ proj₁ (reverse ops ↓↓ₑ (o , i)) →
       ----------------------------------------------------------
       Σ[ ops' ∈ List Σₛ ] (ops' ⊆ ops × (op `at ops' `in o , i))

↓↓-⊆ [] p =
  [] , [] , stop p
↓↓-⊆ {op} (op' ∷ ops) {omap o} {imap i} p rewrite ↓↓-⊆-rw (omap o) (imap i) op' ops =
  ↓↓-⊆-aux (i op') refl

  where
    ↓↓-⊆-aux : (oi : Maybe (O × I)) →
               i op' ≡ oi →
               ----------------------------------------------------------------------------
               Σ[ ops' ∈ List Σₛ ] (ops' ⊆ (op' ∷ ops) × (op `at ops' `in omap o , imap i))

    ↓↓-⊆-aux nothing q with ↓↓-⊆ ops p
    ... | ops' , r , s rewrite q =
      ops' , ∷-∷ r , s
    ↓↓-⊆-aux (just (omap o' , imap i')) q with ↓↓-⊆ ops p
    ... | ops' , r , s rewrite q with `at-⊎ {o = omap o} {o' = omap o'} {i' = imap i'} s
    ... | inj₁ t =
      ↓↓-⊆-aux-aux ops' r t

      where
        ↓↓-⊆-aux-aux : (ops' : List Σₛ) →
                       ops' ⊆ ops →
                       (op `at ops' `in omap o , ((imap i) [ op' ↦ nothing ]ᵢ)) →
                       -------------------------------------------------------------------------------
                       Σ[ ops'' ∈ List Σₛ ] (ops'' ⊆ (op' ∷ ops) × (op `at ops'' `in omap o , imap i))

        ↓↓-⊆-aux-aux [] r (stop t) =
          [] , [] , stop t
        ↓↓-⊆-aux-aux (op'' ∷ ops'') r (next t u) with decₛ op' op''
        ... | no ¬v =
          op'' ∷ ops'' , ∷-≢ (λ w → ¬v (sym w)) r , next t u

    ... | inj₂ t =
      op' ∷ ops' , ∷-≡ r , next q t

-- ENVELOPING THE EFFECT ANNOTATION REDUCTION WITH MLTIPLE INTERRUPT ACTIONS

{- LEMMA 4.5 -}

↓↓ₑ-⊑ₒ-act : {o : O}
             {i : I} →
             (ops : List Σₛ) →
             (op : Σₛ) →
             ----------------------------------------------------------
             proj₁ (ops ↓↓ₑ (o , i)) ⊑ₒ proj₁ (ops ↓↓ₑ (op ↓ₑ (o , i)))

↓↓ₑ-⊑ₒ-act {o} {i} ops op op' p rewrite sym (reverse-involutive ops) with ↓↓-⊆ (reverse ops) p
... | ops' , q , r with ⊆-↓↓ {op'} (∷-∷ {op} q)
... | s with ↓↓ₑ-monotonicₒ (reverse (op ∷ reverse ops)) (`at-minₒ r) (`at-minᵢ r) op' s
... | t rewrite ↓↓-⊆-rw o i op (reverse ops) | reverse-involutive ops = t

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda