text:
module Esterel.Environment where

open import utility

open import Data.Empty
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)
open import Data.Product

import Data.FiniteMap
open import Data.Nat as Nat
  using (ℕ)
open import Data.List as List
  using (List ; [] ; _∷_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂ ; [_,_])

open import Function
  using (_∘_)
open import Relation.Nullary
  using (Dec ; yes ; no ; ¬_)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; sym ; module ≡-Reasoning ; trans ; subst ; inspect)
open import Data.List.Any
  using (Any)

open ≡-Reasoning using (_≡⟨_⟩_ ; _≡⟨⟩_ ; _∎ ; begin_)

module SigMap = Data.FiniteMap Signal.unwrap    Signal.wrap Signal.unwrap-injective Signal.bijective
module ShrMap = Data.FiniteMap SharedVar.unwrap SharedVar.wrap SharedVar.unwrap-injective SharedVar.bijective
module VarMap = Data.FiniteMap SeqVar.unwrap    SeqVar.wrap SeqVar.unwrap-injective SeqVar.bijective

record Env : Set where
  constructor Θ
  field
    sig  : SigMap.Map Signal.Status
    shr  : ShrMap.Map (SharedVar.Status × ℕ)
    var  : VarMap.Map ℕ

open Env public

-- A VarList is a three-tuple of lists of unwrapped signals,
-- shared variables and sequential variables.
VarList : Set
VarList = List ℕ × List ℕ × List ℕ

Dom : Env -> VarList
Dom (Θ sig shr var) = (SigMap.keys sig) , (ShrMap.keys shr) , (VarMap.keys var)

[]env = Θ [] [] []

Sig∈ : (S : Signal) →
       (e : Env) →
       Relation.Nullary.Dec
          (Any (SigMap.inj= S)
               (SigMap.keys (sig e)))
Sig∈ s e = SigMap.∈Check s (sig e)

Shr∈ : (s : SharedVar) → (e : Env) →
       Relation.Nullary.Dec
       (Any (ShrMap.inj= s)
            (ShrMap.keys (shr e)))
Shr∈ s e = ShrMap.∈Check s (shr e)

Var∈ : (x : SeqVar) → (e : Env) →
       Relation.Nullary.Dec
       (Any (VarMap.inj= x)
            (VarMap.keys (var e)))
Var∈ x e = VarMap.∈Check x (var e)

isSig∈ : (S : Signal) → (e : Env) → Set
isSig∈ S e = (SigMap.∈Dom S (sig e))

isShr∈ : SharedVar → Env → Set
isShr∈ s e = ShrMap.∈Dom s (shr e)

isVar∈ : SeqVar → Env → Set
isVar∈ x e = VarMap.∈Dom x (var e)

SigDomMap : ∀{a}{L : Set a} →  (θ : Env) → (f : (S : Signal) → isSig∈ S θ → L) → List L
SigDomMap = SigMap.key-map ∘ sig

ShrDomMap : ∀{a}{L : Set a} →  (θ : Env) → (f : (S : SharedVar) → isShr∈ S θ → L) → List L
ShrDomMap = ShrMap.key-map ∘ shr

SigDom : Env → List ℕ
SigDom (Θ sig shr var) = (SigMap.keys sig)
ShrDom : Env → List ℕ
ShrDom (Θ sig shr var) = (ShrMap.keys shr)
VarDom : Env → List ℕ
VarDom (Θ sig shr var) = (VarMap.keys var)

sig-stats : ∀{S} → (θ : Env) → (SigMap.∈Dom S (sig θ)) → Signal.Status
sig-stats{S} θ S∈ = SigMap.lookup{k = S} (sig θ) S∈

shr-stats : ∀{s} → (θ : Env) → (ShrMap.∈Dom s (shr θ)) → SharedVar.Status
shr-stats{s} θ s∈ = proj₁ (ShrMap.lookup{k = s} (shr θ) s∈)

shr-vals : ∀{s} → (θ : Env) → (ShrMap.∈Dom s (shr θ)) → ℕ
shr-vals{s} θ s∈ = proj₂ (ShrMap.lookup{k = s} (shr θ) s∈)

var-vals : ∀{x} → (θ : Env) → (VarMap.∈Dom x (var θ)) → ℕ
var-vals{x} θ x∈ = VarMap.lookup{k = x} (var θ) x∈

set-sig : ∀{S} → (θ : Env) → (SigMap.∈Dom S (sig θ)) → Signal.Status → Env
set-sig{S} (Θ sig shr var) S∈ status =
  Θ (SigMap.update sig S status) shr var

set-shr : ∀{s} → (θ : Env) → (ShrMap.∈Dom s (shr θ)) → SharedVar.Status → ℕ → Env
set-shr{s} (Θ sig shr var) s∈ status n =
  Θ sig (ShrMap.update shr s (status , n)) var

set-var : ∀{x} → (θ : Env) → (VarMap.∈Dom x (var θ)) → ℕ → Env
set-var{x} (Θ sig shr var) x∈ n =
  Θ sig shr (VarMap.update var x n)

_←_ : Env → Env → Env
Θ sig₁ shr₁ seq₁ ← Θ sig₂ shr₂ seq₂ =
  Θ (SigMap.union sig₁ sig₂)
    (ShrMap.union shr₁ shr₂)
    (VarMap.union seq₁ seq₂)

data EnvVar : Set where
 vsig : Signal → EnvVar
 vshr : SharedVar → EnvVar
 vvar : SeqVar → EnvVar

data ∈map : EnvVar → Env → Set where
  ∈sig : ∀{S θ} → (isSig∈ S θ) → ∈map (vsig S) θ
  ∈shr : ∀{s θ} → (isShr∈ s θ) → ∈map (vshr s) θ
  ∈var : ∀{x θ} → (isVar∈ x θ) → ∈map (vvar x) θ

-- thrms

sig-set-mono' : ∀{S S' θ stat} → ∀{S'∈ : (isSig∈ S' θ)} → (isSig∈ S θ) → (isSig∈ S (set-sig{S'} θ S'∈ stat))
sig-set-mono'{S}{S'}{θ}{stat}{S'∈} i =  SigMap.insert-mono{_}{k = S}{m = sig θ}{S'}{stat} i

shr-set-mono' : ∀{s s' θ stat n} → ∀{s'∈ : (isShr∈ s' θ)} → (isShr∈ s θ) → (isShr∈ s (set-shr{s'} θ s'∈ stat n))
shr-set-mono'{s}{s'}{θ}{stat}{n}{s'∈} i =  ShrMap.insert-mono{_}{k = s}{m = shr θ}{s'}{stat ,′ n} i

seq-set-mono' : ∀{x x' θ n} → ∀{x'∈ : (isVar∈ x' θ)} → (isVar∈ x θ) → (isVar∈ x (set-var{x'} θ x'∈ n))
seq-set-mono'{x}{x'}{θ}{n}{x'∈} i =  VarMap.insert-mono{_}{k = x}{m = var θ}{x'}{n} i

sig-set-mono : ∀{V S' θ stat} → ∀{S'∈ : (isSig∈ S' θ)} → ∈map V θ → (∈map V (set-sig{S'} θ S'∈ stat))
sig-set-mono{S' = S'}{θ}{S'∈ = S'∈} (∈sig{S} x) = ∈sig{S} (sig-set-mono'{S = S}{S' = S'}{θ = θ}{S'∈ = S'∈} x)
sig-set-mono (∈shr x) = ∈shr x
sig-set-mono (∈var x₁) = ∈var x₁

shr-set-mono : ∀{V s' θ stat n} → ∀{s'∈ : (isShr∈ s' θ)} → (∈map V θ) → (∈map V (set-shr{s'} θ s'∈ stat n))
shr-set-mono (∈sig x) = ∈sig x
shr-set-mono{s' = s'}{θ}{stat}{n}{s'∈}(∈shr{s} x) = ∈shr{s} (shr-set-mono'{s}{s'}{θ}{stat}{n}{s'∈}  x)
shr-set-mono (∈var x₁) = ∈var x₁

seq-set-mono : ∀{V x' θ n} → ∀{x'∈ : (isVar∈ x' θ)} → (∈map V θ) → (∈map V (set-var{x'} θ x'∈ n))
seq-set-mono (∈sig x) = ∈sig x
seq-set-mono (∈shr x) = ∈shr x
seq-set-mono{x' = x'}{θ}{n}{x'∈} (∈var{x} x₁) = ∈var {x} (seq-set-mono'{x}{x'}{θ}{n}{x'∈} x₁)

←-mono : ∀{θ θ' V} → ∈map V θ → ∈map V (θ ← θ')
←-mono{θ}{θ'}{vsig S}  (∈sig x) = ∈sig{S}{(θ ← θ')} (SigMap.U-mono{_}{sig θ}{sig θ'}{S} x)
←-mono{θ}{θ'}{vshr s} (∈shr x) = ∈shr{s}{(θ ← θ')} (ShrMap.U-mono{_}{shr θ}{shr θ'}{s} x)
←-mono{θ}{θ'}{vvar x} (∈var x₁) = ∈var{x}{(θ ← θ')} (VarMap.U-mono{_}{var θ}{var θ'}{x} x₁)

←-comm : ∀ θ θ' → distinct (Dom θ) (Dom θ') → (θ ← θ') ≡ (θ' ← θ)
←-comm (Θ Ss ss xs) (Θ Ss' ss' xs') (Ss≠Ss' , ss≠ss' , xs≠xs')
  rewrite SigMap.union-comm Ss Ss' Ss≠Ss'
        | ShrMap.union-comm ss ss' ss≠ss'
        | VarMap.union-comm xs xs' xs≠xs' = refl

←-assoc : ∀ θ θ' θ'' → (θ ← (θ' ← θ'')) ≡ ((θ ← θ') ← θ'')
←-assoc (Θ Ss ss xs) (Θ Ss' ss' xs') (Θ Ss'' ss'' xs'')
  rewrite SigMap.union-assoc Ss Ss' Ss''
        | ShrMap.union-assoc ss ss' ss''
        | VarMap.union-assoc xs xs' xs'' = refl

←-assoc-comm : ∀ θ θ' θ'' → distinct (Dom θ') (Dom θ'') → ((θ ← θ') ← θ'') ≡ ((θ ← θ'') ← θ')
←-assoc-comm θ θ' θ'' Domθ'≠Domθ'' =
    (θ ← θ') ← θ''
   ≡⟨ sym (←-assoc θ θ' θ'') ⟩
     θ ← (θ' ← θ'')
   ≡⟨ cong (θ ←_) (←-comm θ' θ'' Domθ'≠Domθ'') ⟩
     θ ← (θ'' ← θ')
   ≡⟨ ←-assoc θ θ'' θ' ⟩
     (θ ← θ'') ← θ' ∎

Dom-←-assoc-comm : ∀ θ θ' θ'' → Dom ((θ ← θ') ← θ'') ≡ Dom ((θ ← θ'') ← θ')
Dom-←-assoc-comm (Θ Ss ss xs) (Θ Ss' ss' xs') (Θ Ss'' ss'' xs'')
  rewrite SigMap.keys-assoc-comm Ss Ss' Ss''
        | ShrMap.keys-assoc-comm ss ss' ss''
        | VarMap.keys-assoc-comm xs xs' xs'' = refl

Dom-←-comm : ∀ θ θ' → Dom (θ ← θ') ≡ Dom (θ' ← θ)
Dom-←-comm θ θ' = Dom-←-assoc-comm []env θ θ'

sig-←-monoʳ : ∀ S θ θ' → isSig∈ S θ → isSig∈ S (θ' ← θ)
sig-←-monoʳ S θ θ' S∈Domθ
  rewrite cong proj₁ (Dom-←-comm θ' θ)
  = SigMap.U-mono {_} {Env.sig θ} {Env.sig θ'} {S} S∈Domθ

shr-←-monoʳ : ∀ s θ θ' → isShr∈ s θ → isShr∈ s (θ' ← θ)
shr-←-monoʳ s θ θ' s∈Domθ
  rewrite cong (proj₁ ∘ proj₂) (Dom-←-comm θ' θ)
  = ShrMap.U-mono {_} {Env.shr θ} {Env.shr θ'} {s} s∈Domθ

seq-←-monoʳ : ∀ x θ θ' → isVar∈ x θ → isVar∈ x (θ' ← θ)
seq-←-monoʳ x θ θ' x∈Domθ
  rewrite cong (proj₂ ∘ proj₂) (Dom-←-comm θ' θ)
  = VarMap.U-mono {_} {var θ} {var θ'} {x} x∈Domθ

sig-←-monoˡ : ∀ S θ θ' → isSig∈ S θ → isSig∈ S (θ ← θ')
sig-←-monoˡ S θ θ' S∈Domθ
  = SigMap.U-mono {_} {Env.sig θ} {Env.sig θ'} {S} S∈Domθ

shr-←-monoˡ : ∀ s θ θ' → isShr∈ s θ → isShr∈ s (θ ← θ')
shr-←-monoˡ s θ θ' s∈Domθ
  = ShrMap.U-mono {_} {Env.shr θ} {Env.shr θ'} {s} s∈Domθ

seq-←-monoˡ : ∀ x θ θ' → isVar∈ x θ → isVar∈ x (θ ← θ')
seq-←-monoˡ x θ θ' x∈Domθ
  = VarMap.U-mono {_} {var θ} {var θ'} {x} x∈Domθ

sig-←⁻ : ∀ {θ₁ θ₂} S → isSig∈ S (θ₁ ← θ₂) → isSig∈ S θ₁ ⊎ isSig∈ S θ₂
sig-←⁻ {θ₁} {θ₂} S = SigMap.U⁻-m {Signal.Status} {sig θ₁} {sig θ₂} {S}

shr-←⁻ : ∀ {θ₁ θ₂} s → isShr∈ s (θ₁ ← θ₂) → isShr∈ s θ₁ ⊎ isShr∈ s θ₂
shr-←⁻ {θ₁} {θ₂} s = ShrMap.U⁻-m {_} {shr θ₁} {shr θ₂} {s}

seq-←⁻ : ∀ {θ₁ θ₂} x → isVar∈ x (θ₁ ← θ₂) → isVar∈ x θ₁ ⊎ isVar∈ x θ₂
seq-←⁻ {θ₁} {θ₂} x = VarMap.U⁻-m {_} {var θ₁} {var θ₂} {x}

sig-↚⁻ : ∀ {θ₁ θ₂} S → ¬ isSig∈ S θ₁ → ¬ isSig∈ S θ₂ → ¬ isSig∈ S (θ₁ ← θ₂)
sig-↚⁻ {θ₁} {θ₂} S S∉Domθ₁ S∉Domθ₂ = [ S∉Domθ₁ , S∉Domθ₂ ] ∘ sig-←⁻ {θ₁} {θ₂} S

sig-stats-∈-irr : ∀{S θ} → (∈1 : (SigMap.∈Dom S (sig θ))) → (∈2 : (SigMap.∈Dom S (sig θ))) → sig-stats{S} θ ∈1 ≡ sig-stats{S} θ ∈2
sig-stats-∈-irr{S} {θ} ∈1 ∈2 = SigMap.lookup-∈-irr{k = S}{m = (sig θ)} ∈1 ∈2

shr-stats-∈-irr : ∀{s θ} → (∈1 : ShrMap.∈Dom s (shr θ)) → (∈2 : ShrMap.∈Dom s (shr θ)) → shr-stats{s} θ ∈1 ≡ shr-stats{s} θ ∈2
shr-stats-∈-irr{s}{θ} ∈1 ∈2 = cong proj₁ (ShrMap.lookup-∈-irr{k = s}{m = (shr θ)} ∈1 ∈2)
shr-vals-∈-irr : ∀{s θ} → (∈1 : ShrMap.∈Dom s (shr θ)) → (∈2 : ShrMap.∈Dom s (shr θ)) → shr-vals{s} θ ∈1 ≡ shr-vals{s} θ ∈2
shr-vals-∈-irr{s}{θ} ∈1 ∈2 = cong proj₂ (ShrMap.lookup-∈-irr{k = s}{m = (shr θ)} ∈1 ∈2)

var-vals-∈-irr : ∀{x θ} → (∈1 : VarMap.∈Dom x (var θ)) →  (∈2 : VarMap.∈Dom x (var θ)) → var-vals{x} θ ∈1 ≡ var-vals{x} θ ∈2
var-vals-∈-irr{x} {θ} ∈1 ∈2 = VarMap.lookup-∈-irr{_}{x}{var θ} ∈1 ∈2

sig-←-∉-irr-stats' : ∀ S θ θ' →
  (S∈ : isSig∈ S θ) →
  (S∉ : ¬ isSig∈ S θ') →
  (S∈Dom⟨θ←θ'⟩ : isSig∈ S (θ ← θ')) →
  sig-stats {S} θ S∈ ≡ sig-stats {S} (θ ← θ') S∈Dom⟨θ←θ'⟩
sig-←-∉-irr-stats' S θ θ' S∈ S∉ S∈' =
  SigMap.U-∉-irr-get-help-m {_} {Env.sig θ} {Env.sig θ'} {S} S∈ S∉ S∈'

sig-←-∉-irr-stats : ∀ S θ θ' →
  (S∈ : isSig∈ S θ) →
  (S∉ : ¬ isSig∈ S θ') →
  ∃ λ S∈Dom⟨θ←θ'⟩ →
    sig-stats {S} θ S∈ ≡ sig-stats {S} (θ ← θ') S∈Dom⟨θ←θ'⟩
sig-←-∉-irr-stats S θ θ' S∈ S∉ =
  SigMap.U-∉-irr-get-m {_} {Env.sig θ} {Env.sig θ'} {S} S∈ S∉

shr-←-∉-irr-stats' : ∀ s θ θ' →
  (s∈ : isShr∈ s θ) →
  (s∉ : ¬ isShr∈ s θ') →
  (s∈Dom⟨θ←θ'⟩ : isShr∈ s (θ ← θ')) →
  shr-stats {s} θ s∈ ≡ shr-stats {s} (θ ← θ') s∈Dom⟨θ←θ'⟩
shr-←-∉-irr-stats' s θ θ' s∈ s∉ s∈'
  rewrite ShrMap.U-∉-irr-get-help-m {_} {Env.shr θ} {Env.shr θ'} {s} s∈ s∉ s∈'
  = refl

shr-←-∉-irr-stats : ∀ s θ θ' →
  (s∈ : isShr∈ s θ) →
  (s∉ : ¬ isShr∈ s θ') →
  ∃ λ s∈Dom⟨θ←θ'⟩ →
    shr-stats {s} θ s∈ ≡ shr-stats {s} (θ ← θ') s∈Dom⟨θ←θ'⟩
shr-←-∉-irr-stats s θ θ' s∈ s∉
  rewrite proj₂ (ShrMap.U-∉-irr-get-m {_} {Env.shr θ} {Env.shr θ'} {s} s∈ s∉)
  = (_ , refl)

shr-←-∉-irr-vals' : ∀ s θ θ' →
  (s∈ : isShr∈ s θ) →
  (s∉ : ¬ isShr∈ s θ') →
  (s∈Dom⟨θ←θ'⟩ : isShr∈ s (θ ← θ')) →
  shr-vals {s} θ s∈ ≡ shr-vals {s} (θ ← θ') s∈Dom⟨θ←θ'⟩
shr-←-∉-irr-vals' s θ θ' s∈ s∉ s∈'
  rewrite ShrMap.U-∉-irr-get-help-m {_} {Env.shr θ} {Env.shr θ'} {s} s∈ s∉ s∈'
  = refl

shr-←-∉-irr-vals : ∀ s θ θ' →
  (s∈ : isShr∈ s θ) →
  (s∉ : ¬ isShr∈ s θ') →
  ∃ λ s∈Dom⟨θ←θ'⟩ →
    shr-vals {s} θ s∈ ≡ shr-vals {s} (θ ← θ') s∈Dom⟨θ←θ'⟩
shr-←-∉-irr-vals s θ θ' s∈ s∉
  rewrite proj₂ (ShrMap.U-∉-irr-get-m {_} {Env.shr θ} {Env.shr θ'} {s} s∈ s∉)
  = (_ , refl)

var-←-∉-irr-vals' : ∀ x θ θ' →
  (x∈ : isVar∈ x θ) →
  (x∉ : ¬ isVar∈ x θ') →
  (x∈Dom⟨θ←θ'⟩ : isVar∈ x (θ ← θ')) →
  var-vals {x} θ x∈ ≡ var-vals {x} (θ ← θ') x∈Dom⟨θ←θ'⟩
var-←-∉-irr-vals' x θ θ' x∈ x∉ x∈' =
  VarMap.U-∉-irr-get-help-m {_} {Env.var θ} {Env.var θ'} {x} x∈ x∉ x∈'

var-←-∉-irr-vals : ∀ x θ θ' →
  (x∈ : isVar∈ x θ) →
  (x∉ : ¬ isVar∈ x θ') →
  ∃ λ x∈Dom⟨θ←θ'⟩ →
    var-vals {x} θ x∈ ≡ var-vals {x} (θ ← θ') x∈Dom⟨θ←θ'⟩
var-←-∉-irr-vals x θ θ' x∈ x∉ =
  VarMap.U-∉-irr-get-m {_} {Env.var θ} {Env.var θ'} {x} x∈ x∉

sig-stats-←-right-irr' : ∀ S θ θ' →
  (S∈  : isSig∈ S θ') →
  (S∈' : isSig∈ S (θ ← θ')) →
  sig-stats {S} (θ ← θ') S∈' ≡ sig-stats {S} θ' S∈
sig-stats-←-right-irr' S θ θ' S∈ S∈' =
  SigMap.get-U-right-irr-m S (Env.sig θ) (Env.sig θ') S∈' S∈

sig-stats-←-right-irr : ∀ S θ θ' →
  (S∈  : isSig∈ S θ') →
  ∃ λ S∈' →
    sig-stats {S} (θ ← θ') S∈' ≡ sig-stats {S} θ' S∈
sig-stats-←-right-irr S θ θ' S∈ =
  sig-←-monoʳ S θ' θ S∈ ,
  SigMap.get-U-right-irr-m S (Env.sig θ) (Env.sig θ') (sig-←-monoʳ S θ' θ S∈) S∈

shr-stats-←-right-irr' : ∀ s θ θ' →
  (s∈  : isShr∈ s θ') →
  (s∈' : isShr∈ s (θ ← θ')) →
  shr-stats {s} (θ ← θ') s∈' ≡ shr-stats {s} θ' s∈
shr-stats-←-right-irr' s θ θ' s∈ s∈'
  rewrite ShrMap.get-U-right-irr-m s (Env.shr θ) (Env.shr θ') s∈' s∈
  = refl

shr-stats-←-right-irr : ∀ s θ θ' →
  (s∈ : isShr∈ s θ') →
  ∃ λ s∈' →
    shr-stats {s} (θ ← θ') s∈' ≡ shr-stats {s} θ' s∈
shr-stats-←-right-irr s θ θ' s∈ =
  shr-←-monoʳ s θ' θ s∈ ,
  cong proj₁
    (ShrMap.get-U-right-irr-m s (Env.shr θ) (Env.shr θ')
      (shr-←-monoʳ s θ' θ s∈) s∈)

shr-vals-←-right-irr' : ∀ s θ θ' →
  (s∈  : isShr∈ s θ') →
  (s∈' : isShr∈ s (θ ← θ')) →
  shr-vals {s} (θ ← θ') s∈' ≡ shr-vals {s} θ' s∈
shr-vals-←-right-irr' s θ θ' s∈ s∈'
  rewrite ShrMap.get-U-right-irr-m s (Env.shr θ) (Env.shr θ') s∈' s∈
  = refl

shr-vals-←-right-irr : ∀ s θ θ' →
  (s∈ : isShr∈ s θ') →
  ∃ λ s∈' →
    shr-vals {s} (θ ← θ') s∈' ≡ shr-vals {s} θ' s∈
shr-vals-←-right-irr s θ θ' s∈ =
  shr-←-monoʳ s θ' θ s∈ ,
  cong proj₂
    (ShrMap.get-U-right-irr-m s (Env.shr θ) (Env.shr θ')
      (shr-←-monoʳ s θ' θ s∈) s∈)

var-vals-←-right-irr' : ∀ x θ θ' →
  (x∈  : isVar∈ x θ') →
  (x∈' : isVar∈ x (θ ← θ')) →
  var-vals {x} (θ ← θ') x∈' ≡ var-vals {x} θ' x∈
var-vals-←-right-irr' x θ θ' x∈ x∈' =
  VarMap.get-U-right-irr-m x (Env.var θ) (Env.var θ') x∈' x∈

var-vals-←-right-irr : ∀ x θ θ' →
  (x∈  : isVar∈ x θ') →
  ∃ λ x∈' →
    var-vals {x} (θ ← θ') x∈' ≡ var-vals {x} θ' x∈
var-vals-←-right-irr x θ θ' x∈ =
  seq-←-monoʳ x θ' θ x∈ ,
  VarMap.get-U-right-irr-m x (Env.var θ) (Env.var θ') (seq-←-monoʳ x θ' θ x∈) x∈

sig-stats-←-irr' : ∀ S θ θ' θ'' →
  (S∈   : isSig∈ S θ'') →
  (S∈'  : isSig∈ S (θ  ← θ'')) →
  (S∈'' : isSig∈ S (θ' ← θ'')) →
  sig-stats {S} (θ ← θ'') S∈' ≡ sig-stats {S} (θ' ← θ'') S∈''
sig-stats-←-irr' S θ θ' θ'' S∈ S∈' S∈'' =
  SigMap.∈-get-U-irr-m S (sig θ) (sig θ') (sig θ'') S∈' S∈'' S∈

sig-stats-←-irr : ∀ S θ θ' θ'' →
  (S∈   : isSig∈ S θ'') →
  ∃ λ S∈' →
    ∃ λ S∈'' →
      sig-stats {S} (θ ← θ'') S∈' ≡ sig-stats {S} (θ' ← θ'') S∈''
sig-stats-←-irr S θ θ' θ'' S∈ =
  sig-←-monoʳ S θ'' θ S∈ ,
  sig-←-monoʳ S θ'' θ' S∈ ,
  SigMap.∈-get-U-irr-m S (sig θ) (sig θ') (sig θ'')
    (sig-←-monoʳ S θ'' θ S∈) (sig-←-monoʳ S θ'' θ' S∈) S∈

shr-stats-←-irr' : ∀ s θ θ' θ'' →
  (s∈   : isShr∈ s θ'') →
  (s∈'  : isShr∈ s (θ  ← θ'')) →
  (s∈'' : isShr∈ s (θ' ← θ'')) →
  shr-stats {s} (θ ← θ'') s∈' ≡ shr-stats {s} (θ' ← θ'') s∈''
shr-stats-←-irr' s θ θ' θ'' s∈ s∈' s∈''
  rewrite ShrMap.∈-get-U-irr-m s (shr θ) (shr θ') (shr θ'') s∈' s∈'' s∈
  = refl

shr-stats-←-irr : ∀ s θ θ' θ'' →
  (s∈   : isShr∈ s θ'') →
  ∃ λ s∈' →
    ∃ λ s∈'' →
      shr-stats {s} (θ ← θ'') s∈' ≡ shr-stats {s} (θ' ← θ'') s∈''
shr-stats-←-irr s θ θ' θ'' s∈ =
  shr-←-monoʳ s θ'' θ s∈ ,
  shr-←-monoʳ s θ'' θ' s∈ ,
  cong proj₁
    (ShrMap.∈-get-U-irr-m s (shr θ) (shr θ') (shr θ'')
      (shr-←-monoʳ s θ'' θ s∈) (shr-←-monoʳ s θ'' θ' s∈) s∈)

shr-vals-←-irr' : ∀ s θ θ' θ'' →
  (s∈   : isShr∈ s θ'') →
  (s∈'  : isShr∈ s (θ  ← θ'')) →
  (s∈'' : isShr∈ s (θ' ← θ'')) →
  shr-vals {s} (θ ← θ'') s∈' ≡ shr-vals {s} (θ' ← θ'') s∈''
shr-vals-←-irr' s θ θ' θ'' s∈ s∈' s∈''
  rewrite ShrMap.∈-get-U-irr-m s (shr θ) (shr θ') (shr θ'') s∈' s∈'' s∈
  = refl

shr-vals-←-irr : ∀ s θ θ' θ'' →
  (s∈   : isShr∈ s θ'') →
  ∃ λ s∈' →
    ∃ λ s∈'' →
      shr-vals {s} (θ ← θ'') s∈' ≡ shr-vals {s} (θ' ← θ'') s∈''
shr-vals-←-irr s θ θ' θ'' s∈ =
  shr-←-monoʳ s θ'' θ s∈ ,
  shr-←-monoʳ s θ'' θ' s∈ ,
  cong proj₂
    (ShrMap.∈-get-U-irr-m s (shr θ) (shr θ') (shr θ'')
      (shr-←-monoʳ s θ'' θ s∈) (shr-←-monoʳ s θ'' θ' s∈) s∈)

var-vals-←-irr' : ∀ x θ θ' θ'' →
  (x∈   : isVar∈ x θ'') →
  (x∈'  : isVar∈ x (θ  ← θ'')) →
  (x∈'' : isVar∈ x (θ' ← θ'')) →
  var-vals {x} (θ ← θ'') x∈' ≡ var-vals {x} (θ' ← θ'') x∈''
var-vals-←-irr' x θ θ' θ'' x∈ x∈' x∈'' =
  VarMap.∈-get-U-irr-m x (var θ) (var θ') (var θ'') x∈' x∈'' x∈

var-vals-←-irr : ∀ x θ θ' θ'' →
  (x∈   : isVar∈ x θ'') →
  ∃ λ x∈' →
    ∃ λ x∈'' →
      var-vals {x} (θ ← θ'') x∈' ≡ var-vals {x} (θ' ← θ'') x∈''
var-vals-←-irr x θ θ' θ'' x∈ =
  seq-←-monoʳ x θ'' θ x∈ ,
  seq-←-monoʳ x θ'' θ' x∈ ,
  VarMap.∈-get-U-irr-m x (var θ) (var θ') (var θ'')
    (seq-←-monoʳ x θ'' θ x∈) (seq-←-monoʳ x θ'' θ' x∈) x∈

sig-stats-←-both-irr' : ∀ S θ θ' θ'' S∈ S∈' S∈Dom⟨θ←θ''⟩ S∈Dom⟨θ'←θ''⟩ →
  sig-stats {S} θ S∈ ≡ sig-stats {S} θ' S∈' →
    sig-stats {S} (θ ← θ'') S∈Dom⟨θ←θ''⟩ ≡ sig-stats {S} (θ' ← θ'') S∈Dom⟨θ'←θ''⟩
sig-stats-←-both-irr' S θ θ' θ'' S∈ S∈' S∈Dom⟨θ←θ''⟩ S∈Dom⟨θ'←θ''⟩ θS≡θ'S =
  SigMap.get-U-both-irr-m S (Env.sig θ) (Env.sig θ') (Env.sig θ'')
    S∈ S∈' S∈Dom⟨θ←θ''⟩ S∈Dom⟨θ'←θ''⟩ θS≡θ'S

sig-stats-←-both-irr : ∀ S θ θ' θ'' S∈ S∈' →
  sig-stats {S} θ S∈ ≡ sig-stats {S} θ' S∈' →
  ∃ λ S∈Dom⟨θ←θ''⟩ → ∃ λ S∈Dom⟨θ'←θ''⟩ →
    sig-stats {S} (θ ← θ'') S∈Dom⟨θ←θ''⟩ ≡ sig-stats {S} (θ' ← θ'') S∈Dom⟨θ'←θ''⟩
sig-stats-←-both-irr S θ θ' θ'' S∈ S∈' θS≡θ'S =
  S∈Dom⟨θ←θ''⟩ ,
  S∈Dom⟨θ'←θ''⟩ ,
  SigMap.get-U-both-irr-m S (Env.sig θ) (Env.sig θ') (Env.sig θ'')
    S∈ S∈' S∈Dom⟨θ←θ''⟩ S∈Dom⟨θ'←θ''⟩ θS≡θ'S
  where S∈Dom⟨θ←θ''⟩  = sig-←-monoˡ S θ  θ'' S∈
        S∈Dom⟨θ'←θ''⟩ = sig-←-monoˡ S θ' θ'' S∈'

shr-stats-←-both-irr' : ∀ s θ θ' θ'' s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ →
  shr-stats {s} θ s∈ ≡ shr-stats {s} θ' s∈' →
  shr-vals {s} θ s∈ ≡ shr-vals {s} θ' s∈' →
    shr-stats {s} (θ ← θ'') s∈Dom⟨θ←θ''⟩ ≡ shr-stats {s} (θ' ← θ'') s∈Dom⟨θ'←θ''⟩
shr-stats-←-both-irr' s θ θ' θ'' s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's =
  cong proj₁
    (ShrMap.get-U-both-irr-m s (Env.shr θ) (Env.shr θ') (Env.shr θ'')
      s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ (prod-ind proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's))
  where prod-ind : {A B : Set} {x,y x',y' : A × B} →
          proj₁ x,y ≡ proj₁ x',y' → proj₂ x,y ≡ proj₂ x',y' → x,y ≡ x',y'
        prod-ind {_} {_} {x , y} {x' , y'} refl refl = refl

shr-stats-←-both-irr : ∀ s θ θ' θ'' s∈ s∈' →
  shr-stats {s} θ s∈ ≡ shr-stats {s} θ' s∈' →
  shr-vals {s} θ s∈ ≡ shr-vals {s} θ' s∈' →
  ∃ λ s∈Dom⟨θ←θ''⟩ → ∃ λ s∈Dom⟨θ'←θ''⟩ →
    shr-stats {s} (θ ← θ'') s∈Dom⟨θ←θ''⟩ ≡ shr-stats {s} (θ' ← θ'') s∈Dom⟨θ'←θ''⟩
shr-stats-←-both-irr s θ θ' θ'' s∈ s∈' proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's =
  s∈Dom⟨θ←θ''⟩ ,
  s∈Dom⟨θ'←θ''⟩ ,
  cong proj₁
    (ShrMap.get-U-both-irr-m s (Env.shr θ) (Env.shr θ') (Env.shr θ'')
      s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ (prod-ind proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's))
  where s∈Dom⟨θ←θ''⟩  = shr-←-monoˡ s θ  θ'' s∈
        s∈Dom⟨θ'←θ''⟩ = shr-←-monoˡ s θ' θ'' s∈'
        prod-ind : {A B : Set} {x,y x',y' : A × B} →
          proj₁ x,y ≡ proj₁ x',y' → proj₂ x,y ≡ proj₂ x',y' → x,y ≡ x',y'
        prod-ind {_} {_} {x , y} {x' , y'} refl refl = refl

shr-vals-←-both-irr' : ∀ s θ θ' θ'' s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ →
  shr-stats {s} θ s∈ ≡ shr-stats {s} θ' s∈' →
  shr-vals {s} θ s∈ ≡ shr-vals {s} θ' s∈' →
    shr-vals {s} (θ ← θ'') s∈Dom⟨θ←θ''⟩ ≡ shr-vals {s} (θ' ← θ'') s∈Dom⟨θ'←θ''⟩
shr-vals-←-both-irr' s θ θ' θ'' s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's =
  cong proj₂
    (ShrMap.get-U-both-irr-m s (Env.shr θ) (Env.shr θ') (Env.shr θ'')
      s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ (prod-ind proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's))
  where prod-ind : {A B : Set} {x,y x',y' : A × B} →
          proj₁ x,y ≡ proj₁ x',y' → proj₂ x,y ≡ proj₂ x',y' → x,y ≡ x',y'
        prod-ind {_} {_} {x , y} {x' , y'} refl refl = refl

shr-vals-←-both-irr : ∀ s θ θ' θ'' s∈ s∈' →
  shr-stats {s} θ s∈ ≡ shr-stats {s} θ' s∈' →
  shr-vals {s} θ s∈ ≡ shr-vals {s} θ' s∈' →
  ∃ λ s∈Dom⟨θ←θ''⟩ → ∃ λ s∈Dom⟨θ'←θ''⟩ →
    shr-vals {s} (θ ← θ'') s∈Dom⟨θ←θ''⟩ ≡ shr-vals {s} (θ' ← θ'') s∈Dom⟨θ'←θ''⟩
shr-vals-←-both-irr s θ θ' θ'' s∈ s∈' proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's =
  s∈Dom⟨θ←θ''⟩ ,
  s∈Dom⟨θ'←θ''⟩ ,
  cong proj₂
    (ShrMap.get-U-both-irr-m s (Env.shr θ) (Env.shr θ') (Env.shr θ'')
      s∈ s∈' s∈Dom⟨θ←θ''⟩ s∈Dom⟨θ'←θ''⟩ (prod-ind proj₁θs≡proj₁θ's proj₂θs≡proj₂θ's))
  where s∈Dom⟨θ←θ''⟩  = shr-←-monoˡ s θ  θ'' s∈
        s∈Dom⟨θ'←θ''⟩ = shr-←-monoˡ s θ' θ'' s∈'
        prod-ind : {A B : Set} {x,y x',y' : A × B} →
          proj₁ x,y ≡ proj₁ x',y' → proj₂ x,y ≡ proj₂ x',y' → x,y ≡ x',y'
        prod-ind {_} {_} {x , y} {x' , y'} refl refl = refl

var-vals-←-both-irr' : ∀ x θ θ' θ'' x∈ x∈' x∈Dom⟨θ←θ''⟩ x∈Dom⟨θ'←θ''⟩ →
  var-vals {x} θ x∈ ≡ var-vals {x} θ' x∈' →
    var-vals {x} (θ ← θ'') x∈Dom⟨θ←θ''⟩ ≡ var-vals {x} (θ' ← θ'') x∈Dom⟨θ'←θ''⟩
var-vals-←-both-irr' x θ θ' θ'' x∈ x∈' x∈Dom⟨θ←θ''⟩ x∈Dom⟨θ'←θ''⟩ θx≡θ'x =
  VarMap.get-U-both-irr-m x (Env.var θ) (Env.var θ') (Env.var θ'')
    x∈ x∈' x∈Dom⟨θ←θ''⟩ x∈Dom⟨θ'←θ''⟩ θx≡θ'x

var-vals-←-both-irr : ∀ x θ θ' θ'' x∈ x∈' →
  var-vals {x} θ x∈ ≡ var-vals {x} θ' x∈' →
  ∃ λ x∈Dom⟨θ←θ''⟩ → ∃ λ x∈Dom⟨θ'←θ''⟩ →
    var-vals {x} (θ ← θ'') x∈Dom⟨θ←θ''⟩ ≡ var-vals {x} (θ' ← θ'') x∈Dom⟨θ'←θ''⟩
var-vals-←-both-irr x θ θ' θ'' x∈ x∈' θx≡θ'x =
  S∈Dom⟨θ←θ''⟩ ,
  S∈Dom⟨θ'←θ''⟩ ,
  VarMap.get-U-both-irr-m x (Env.var θ) (Env.var θ') (Env.var θ'')
    x∈ x∈' S∈Dom⟨θ←θ''⟩ S∈Dom⟨θ'←θ''⟩ θx≡θ'x
  where S∈Dom⟨θ←θ''⟩  = seq-←-monoˡ x θ  θ'' x∈
        S∈Dom⟨θ'←θ''⟩ = seq-←-monoˡ x θ' θ'' x∈'

sig-putputget : ∀{S S' θ stat1 stat2}
                → ¬ S ≡ S'
                → (∈1  : SigMap.∈Dom S (sig θ))
                → (∈S' : SigMap.∈Dom S' (sig θ))
                → (∈2  : SigMap.∈Dom S (sig (set-sig{S'} θ ∈S' stat2)))
                → sig-stats{S} θ ∈1 ≡ stat1
                → sig-stats{S} (set-sig{S'} θ ∈S' stat2) ∈2 ≡ stat1
sig-putputget {θ = θ} neq ∈1 ∈S' ∈2 eq = SigMap.putputget {m = (sig θ)} neq ∈1 ∈2 eq

sig-putputget/m : ∀{S S' θ stat2}
                → ¬ S ≡ S'
                → (∈1  : SigMap.∈Dom S (sig θ))
                → (∈S' : SigMap.∈Dom S' (sig θ))
                → (∈2  : SigMap.∈Dom S (sig (set-sig{S'} θ ∈S' stat2)))
                → sig-stats{S} (set-sig{S'} θ ∈S' stat2) ∈2 ≡ sig-stats{S} θ ∈1
sig-putputget/m {S}{S'}{θ} neq ∈1 ∈S' ∈2 with sig-stats{S} θ ∈1 | inspect (sig-stats{S} θ) ∈1
sig-putputget/m {S} {S'} {θ} neq ∈1 ∈S' ∈2 | k | Relation.Binary.PropositionalEquality.[ eq ] = SigMap.putputget {m = (sig θ)} neq ∈1 ∈2 eq

shr-putputget : ∀{s s' θ v1l v1r v2l v2r}
                → ¬ s ≡ s'
                → (∈1  : ShrMap.∈Dom s (shr θ))
                → (∈s' : ShrMap.∈Dom s' (shr θ))
                → (∈2  : ShrMap.∈Dom s (shr (set-shr{s'} θ ∈s' v2l v2r)))
                → shr-stats{s} θ ∈1 ≡ v1l
                → shr-vals{s} θ ∈1 ≡ v1r
                → (shr-stats{s} (set-shr{s'} θ ∈s' v2l v2r) ∈2) ≡ v1l × (shr-vals{s} (set-shr{s'} θ ∈s' v2l v2r) ∈2) ≡ v1r
shr-putputget {θ = θ}{v1l}{v1r}{v2l}{v2r} neq ∈1 ∈S' ∈2 refl refl with ShrMap.putputget {m = (shr θ)}{v = (v1l ,′ v1r)}{(v2l ,′ v2r)} neq ∈1 ∈2 refl
... | res = (cong proj₁ res) ,′ (cong proj₂ res)

seq-putputget : ∀{x x' θ v1 v2}
                → ¬ x ≡ x'
                → (∈1  : VarMap.∈Dom x  (var θ))
                → (∈x' : VarMap.∈Dom x' (var θ))
                → (∈2  : VarMap.∈Dom x  (var (set-var{x'} θ ∈x' v2)))
                → var-vals{x} θ ∈1 ≡ v1
                → var-vals{x} (set-var{x'} θ ∈x' v2) ∈2 ≡ v1
seq-putputget {θ = θ} neq ∈1 ∈x' ∈2 eq = VarMap.putputget {m = (var θ)} neq ∈1 ∈2 eq

sig-getput : ∀ {θ} S →
  (S∈ : isSig∈ S θ) →
  θ ≡ set-sig {S} θ S∈ (sig-stats {S} θ S∈)
sig-getput {θ} S S∈
  rewrite sym (SigMap.getput-m S (Env.sig θ) S∈)
  = refl

shr-getput : ∀ {θ} s →
  (s∈ : isShr∈ s θ) →
    θ ≡
      set-shr {s} θ s∈
        (shr-stats {s} θ s∈)
        (shr-vals {s} θ s∈)
shr-getput {θ} s s∈
  rewrite sym (ShrMap.getput-m s (Env.shr θ) s∈)
  = refl

var-getput : ∀ {θ} x →
  (x∈ : isVar∈ x θ) →
  θ ≡ set-var {x} θ x∈ (var-vals {x} θ x∈)
var-getput {θ} x x∈
  rewrite sym (VarMap.getput-m x (Env.var θ) x∈)
  = refl

sig-putget : ∀{S θ stat}
             → (∈1 : SigMap.∈Dom S (sig θ))
             → (∈2 : SigMap.∈Dom S (sig (set-sig{S} θ ∈1 stat)))
             → (sig-stats{S} (set-sig{S} θ ∈1 stat) ∈2) ≡ stat
sig-putget {S}{θ}{stat} ∈1 ∈2 = SigMap.putget-m{_}{(sig θ)}{S}{stat} ∈2

shr-putget : ∀{s θ stat n}
             → (∈1 : ShrMap.∈Dom s (shr θ))
             → (∈2 : ShrMap.∈Dom s (shr (set-shr{s} θ ∈1 stat n)))
             → (shr-stats{s} (set-shr{s} θ ∈1 stat n) ∈2) ≡ stat × (shr-vals{s} (set-shr{s} θ ∈1 stat n) ∈2) ≡ n
shr-putget {s}{θ}{stat}{n} ∈1 ∈2 with ShrMap.putget-m{_}{(shr θ)}{s}{stat ,′ n} ∈2
... | eq rewrite eq = refl , refl

shr-putput-overwrite : ∀ s θ stat1 n1 stat2 n2
                       → (∈1 : (isShr∈ s θ))
                       → (∈2 : isShr∈ s (set-shr{s} θ ∈1 stat1 n1))
                       → (set-shr{s} (set-shr{s} θ ∈1 stat1 n1) ∈2 stat2 n2)
                         ≡ (set-shr{s} θ ∈1 stat2 n2)
shr-putput-overwrite s θ stat1 n1 stat2 n2 _ _ rewrite
  ShrMap.putput-overwrite (shr θ) s (stat1 ,′ n1) (stat2 ,′ n2) = refl

sig-set-←-← : ∀ S v θ θ' →
  (S∈Domθ  : isSig∈ S θ) →
  (S∈Domθ' : isSig∈ S θ') →
    θ ← θ' ≡
    (set-sig {S} θ S∈Domθ v) ← θ'
sig-set-←-← S v θ θ' S∈Domθ S∈Domθ'
  rewrite SigMap.update-union-union S v (Env.sig θ) (Env.sig θ') S∈Domθ S∈Domθ'
  = refl

shr-set-←-← : ∀ s v n θ θ' →
  (s∈Domθ  : isShr∈ s θ) →
  (s∈Domθ' : isShr∈ s θ') →
    θ ← θ' ≡
    (set-shr {s} θ s∈Domθ v n) ← θ'
shr-set-←-← s v n θ θ' s∈Domθ s∈Domθ'
  rewrite ShrMap.update-union-union s (v , n) (Env.shr θ) (Env.shr θ') s∈Domθ s∈Domθ'
  = refl

var-set-←-← : ∀ x v θ θ' →
  (x∈Domθ  : isVar∈ x θ) →
  (x∈Domθ' : isVar∈ x θ') →
    θ ← θ' ≡
    (set-var {x} θ x∈Domθ v) ← θ'
var-set-←-← x v θ θ' x∈Domθ x∈Domθ'
  rewrite VarMap.update-union-union x v (Env.var θ) (Env.var θ') x∈Domθ x∈Domθ'
  = refl

sig∈-eq : ∀{S θ} → (∈1 : SigMap.∈Dom S (sig θ)) → (∈2 : SigMap.∈Dom S (sig θ)) → ∈1 ≡ ∈2
sig∈-eq {S}{θ} ∈1 ∈2 = SigMap.ineq-m{_}{S}{sig θ} ∈1 ∈2

shr∈-eq : ∀{s θ} → (∈1 : ShrMap.∈Dom s (shr θ)) → (∈2 : ShrMap.∈Dom s (shr θ)) → ∈1 ≡ ∈2
shr∈-eq {s}{θ} ∈1 ∈2 = ShrMap.ineq-m{_}{s}{shr θ} ∈1 ∈2

seq∈-eq : ∀{x θ} → (∈1 : VarMap.∈Dom x (var θ)) → (∈2 : VarMap.∈Dom x (var θ)) → ∈1 ≡ ∈2
seq∈-eq {x}{θ} ∈1 ∈2 = VarMap.ineq-m{_}{x}{var θ} ∈1 ∈2

sig∈-eq' : ∀{S θ} → (∈1 : SigMap.∈Dom{Signal.Status} S θ) → (∈2 : SigMap.∈Dom S θ) → ∈1 ≡ ∈2
sig∈-eq' {S}{θ} ∈1 ∈2 = SigMap.ineq-m{_}{S}{θ} ∈1 ∈2

shr∈-eq' : ∀{s θ} → (∈1 : ShrMap.∈Dom{(SharedVar.Status × ℕ)} s θ) → (∈2 : ShrMap.∈Dom s θ) → ∈1 ≡ ∈2
shr∈-eq' {s}{θ} ∈1 ∈2 = ShrMap.ineq-m{_}{s}{θ} ∈1 ∈2

seq∈-eq' : ∀{x : SeqVar} {θ : VarMap.Map ℕ} → (∈1 : VarMap.∈Dom{ℕ} x θ) → (∈2 : VarMap.∈Dom x θ) → ∈1 ≡ ∈2
seq∈-eq' {x}{θ} ∈1 ∈2 = VarMap.ineq-m{_}{x}{θ} ∈1 ∈2

sig-set-comm : ∀{θ S1 S2 stat1 stat2} → (S1∈ : isSig∈ S1 θ) → (S2∈ : isSig∈ S2 θ)
               → ¬ S1 ≡ S2 → ∃ λ S1∈' → ∃ λ S2∈'
               → (set-sig{S2} (set-sig{S1} θ S1∈ stat1) S2∈' stat2) ≡ (set-sig{S1} (set-sig{S2} θ S2∈ stat2) S1∈' stat1)
sig-set-comm{θ}{S1}{S2}{stat1}{stat2} S1∈ S2∈ ¬S1≡S2
    rewrite SigMap.put-comm{_}{sig θ}{S1}{S2}{stat1}{stat2} ¬S1≡S2 = sig-set-mono'{S1}{S2}{θ}{stat2}{S2∈} S1∈ , sig-set-mono'{S2}{S1}{θ}{S'∈ = S1∈} S2∈ , refl

shr-set-comm : ∀ θ s1 s2 stat1 n1 stat2 n2 → (s1∈ : isShr∈ s1 θ) → (s2∈ : isShr∈ s2 θ)
               → ¬ s1 ≡ s2 → ∃ λ s1∈' → ∃ λ s2∈'
               → (set-shr{s2} (set-shr{s1} θ s1∈ stat1 n1) s2∈' stat2 n2) ≡ (set-shr{s1} (set-shr{s2} θ s2∈ stat2 n2) s1∈' stat1 n1)
shr-set-comm θ s1 s2 stat1 n1 stat2 n2 s1∈ s2∈ ¬s1≡s2
    rewrite ShrMap.put-comm{_}{shr θ}{s1}{s2}{stat1 , n1}{stat2 , n2} ¬s1≡s2 = shr-set-mono'{s1}{s2}{θ}{_}{_}{s2∈} s1∈ , shr-set-mono'{s2}{s1}{θ}{s'∈ = s1∈} s2∈ , refl

seq-set-comm : ∀ θ x1 x2 n1 n2 → (x1∈ : isVar∈ x1 θ) → (x2∈ : isVar∈ x2 θ)
               → ¬ x1 ≡ x2 → ∃ λ x1∈' → ∃ λ x2∈'
               → (set-var{x2} (set-var{x1} θ x1∈ n1) x2∈' n2) ≡ (set-var{x1} (set-var{x2} θ x2∈ n2) x1∈' n1)
seq-set-comm θ x1 x2 n1 n2  x1∈ x2∈ ¬x1≡x2
    rewrite VarMap.put-comm{_}{var θ}{x1}{x2}{n1}{n2} ¬x1≡x2 = seq-set-mono'{x1}{x2}{θ}{n2}{x2∈} x1∈ , seq-set-mono'{x2}{x1}{θ}{x'∈ = x1∈} x2∈ , refl

sig-←-irr-get : ∀ {θ₁ θ₂ S} → (S∈Domθ₁ : isSig∈ S θ₁) → ¬ (isSig∈ S θ₂) → ∃ λ S∈Dom⟨θ₁←θ₂⟩ → sig-stats {S} θ₁ S∈Domθ₁ ≡ sig-stats {S} (θ₁ ← θ₂) S∈Dom⟨θ₁←θ₂⟩
sig-←-irr-get {θ₁@(Θ Ss _ _)} {θ₂@(Θ Ss' _ _)} {S} S∈Domθ₁ S∉Domθ₂ with SigMap.U-∉-irr-get-m {_} {Ss} {Ss'} {S} S∈Domθ₁ S∉Domθ₂
... | a , b rewrite b = a , refl

shr-←-irr-get : ∀ {θ₁ θ₂ s} → (s∈Domθ₁ : isShr∈ s θ₁) → ¬ (isShr∈ s θ₂) → ∃ λ s∈Dom⟨θ₁←θ₂⟩ → shr-stats {s} θ₁ s∈Domθ₁ ≡ shr-stats {s} (θ₁ ← θ₂) s∈Dom⟨θ₁←θ₂⟩
shr-←-irr-get {θ₁@(Θ _ ss _)} {θ₂@(Θ _ ss' _)} {s} s∈Domθ₁ s∉Domθ₂ with ShrMap.U-∉-irr-get-m {_} {ss} {ss'} {s} s∈Domθ₁ s∉Domθ₂
... | a , b rewrite b = a , refl

seq-←-irr-get : ∀ {θ₁ θ₂ x} → (x∈Domθ₁ : isVar∈ x θ₁) → ¬ (isVar∈ x θ₂) → ∃ λ x∈Dom⟨θ₁←θ₂⟩ → var-vals {x} θ₁ x∈Domθ₁ ≡ var-vals {x} (θ₁ ← θ₂) x∈Dom⟨θ₁←θ₂⟩
seq-←-irr-get {θ₁@(Θ _ _ xs)} {θ₂@(Θ _ _ xs')} {x} x∈Domθ₁ x∉Domθ₂ with VarMap.U-∉-irr-get-m {_} {xs} {xs'} {x} x∈Domθ₁ x∉Domθ₂
... | a , b rewrite b = a , refl

sig-←-irr-get' : ∀ {θ₁ θ₂ S} → (S∈Domθ₁ : isSig∈ S θ₁) → ¬ (isSig∈ S θ₂) → (S∈Dom⟨θ₁←θ₂⟩ : isSig∈ S (θ₁ ← θ₂)) → sig-stats {S} θ₁ S∈Domθ₁ ≡ sig-stats {S} (θ₁ ← θ₂) S∈Dom⟨θ₁←θ₂⟩
sig-←-irr-get' {θ₁@(Θ Ss _ _)} {θ₂@(Θ Ss' _ _)} {S} S∈Domθ₁ S∉Domθ₂ S∈Dom⟨θ₁←θ₂⟩ with SigMap.U-∉-irr-get-m {_} {Ss} {Ss'} {S} S∈Domθ₁ S∉Domθ₂
... | a , b rewrite b | sig∈-eq{S}{θ₁ ← θ₂} a S∈Dom⟨θ₁←θ₂⟩ = refl

shr-←-irr-get' : ∀ {θ₁ θ₂ s} → (s∈Domθ₁ : isShr∈ s θ₁) → ¬ (isShr∈ s θ₂) → (s∈Dom⟨θ₁←θ₂⟩ : isShr∈ s (θ₁ ← θ₂)) → shr-stats {s} θ₁ s∈Domθ₁ ≡ shr-stats {s} (θ₁ ← θ₂) s∈Dom⟨θ₁←θ₂⟩
shr-←-irr-get' {θ₁@(Θ _ ss _)} {θ₂@(Θ _ ss' _)} {s} s∈Domθ₁ s∉Domθ₂ s∈Dom⟨θ₁←θ₂⟩ with ShrMap.U-∉-irr-get-m {_} {ss} {ss'} {s} s∈Domθ₁ s∉Domθ₂
... | a , b rewrite (cong proj₁ b) | shr∈-eq{s}{θ₁ ← θ₂} a s∈Dom⟨θ₁←θ₂⟩ = refl

shr-←-irr-get/vals' : ∀ {θ₁ θ₂ s} → (s∈Domθ₁ : isShr∈ s θ₁) → ¬ (isShr∈ s θ₂) → (s∈Dom⟨θ₁←θ₂⟩ : isShr∈ s (θ₁ ← θ₂)) → shr-vals {s} θ₁ s∈Domθ₁ ≡ shr-vals {s} (θ₁ ← θ₂) s∈Dom⟨θ₁←θ₂⟩
shr-←-irr-get/vals' {θ₁@(Θ _ ss _)} {θ₂@(Θ _ ss' _)} {s} s∈Domθ₁ s∉Domθ₂ s∈Dom⟨θ₁←θ₂⟩ with ShrMap.U-∉-irr-get-m {_} {ss} {ss'} {s} s∈Domθ₁ s∉Domθ₂
... | a , b rewrite (cong proj₂ b) | shr∈-eq{s}{θ₁ ← θ₂} a s∈Dom⟨θ₁←θ₂⟩ = refl

seq-←-irr-get' : ∀ {θ₁ θ₂ x} → (x∈Domθ₁ : isVar∈ x θ₁) → ¬ (isVar∈ x θ₂) → (x∈Dom⟨θ₁←θ₂⟩ : isVar∈ x (θ₁ ← θ₂)) → var-vals {x} θ₁ x∈Domθ₁ ≡ var-vals {x} (θ₁ ← θ₂) x∈Dom⟨θ₁←θ₂⟩
seq-←-irr-get' {θ₁@(Θ _ _ xs)} {θ₂@(Θ _ _ xs')} {x} x∈Domθ₁ x∉Domθ₂ x∈Dom⟨θ₁←θ₂⟩ with VarMap.U-∉-irr-get-m {_} {xs} {xs'} {x} x∈Domθ₁ x∉Domθ₂
... | a , b rewrite b | seq∈-eq{x}{θ₁ ← θ₂} a x∈Dom⟨θ₁←θ₂⟩ = refl

sig-set-←-comm' : ∀ S v θ θ' →
  (S∈ : isSig∈ S θ) →
  ¬ (isSig∈ S θ') →
  (S∈' : isSig∈ S (θ ← θ')) →
    (set-sig {S} θ S∈ v) ← θ' ≡
    set-sig {S} (θ ← θ') S∈' v
sig-set-←-comm' S v θ θ' S∈ S∉Domθ' S∈'
  rewrite SigMap.put-union-comm {_} S v (Env.sig θ) (Env.sig θ') S∉Domθ'
  = refl

sig-set-←-comm : ∀ S v θ θ' →
  (S∈ : isSig∈ S θ) →
  ¬ (isSig∈ S θ') →
  ∃ λ S∈Dom⟨θ←θ'⟩ →
    (set-sig {S} θ S∈ v) ← θ' ≡
    set-sig {S} (θ ← θ') S∈Dom⟨θ←θ'⟩ v
sig-set-←-comm S v θ θ' S∈ S∉Domθ'
  rewrite SigMap.put-union-comm {_} S v (Env.sig θ) (Env.sig θ') S∉Domθ'
  = SigMap.U-mono {_} {Env.sig θ} {Env.sig θ'} {S} S∈ , refl

shr-set-←-comm' : ∀ s v n θ θ' →
  (s∈ : isShr∈ s θ) →
  ¬ (isShr∈ s θ') →
  (s∈' : isShr∈ s (θ ← θ')) →
  (set-shr {s} θ s∈ v n) ← θ' ≡
  set-shr {s} (θ ← θ') s∈' v n
shr-set-←-comm' s v n θ θ' s∈ s∉Domθ' s∈'
  rewrite ShrMap.put-union-comm {_} s (v , n) (Env.shr θ) (Env.shr θ') s∉Domθ'
  = refl

shr-set-←-comm : ∀ s v n θ θ' →
  (s∈ : isShr∈ s θ) →
  ¬ (isShr∈ s θ') →
  ∃ λ s∈Dom⟨θ←θ'⟩ →
    (set-shr {s} θ s∈ v n) ← θ' ≡
    set-shr {s} (θ ← θ') s∈Dom⟨θ←θ'⟩ v n
shr-set-←-comm s v n θ θ' s∈ s∉Domθ'
  rewrite ShrMap.put-union-comm {_} s (v , n) (Env.shr θ) (Env.shr θ') s∉Domθ'
  = ShrMap.U-mono {_} {Env.shr θ} {Env.shr θ'} {s} s∈ , refl

var-set-←-comm' : ∀ x v θ θ' →
  (x∈ : isVar∈ x θ) →
  ¬ (isVar∈ x θ') →
  (x∈' : isVar∈ x (θ ← θ')) →
    (set-var {x} θ x∈ v) ← θ' ≡
    set-var {x} (θ ← θ') x∈' v
var-set-←-comm' x v θ θ' x∈ x∉Domθ' x∈'
  rewrite VarMap.put-union-comm {_} x v (Env.var θ) (Env.var θ') x∉Domθ'
  = refl

var-set-←-comm : ∀ x v θ θ' →
  (x∈ : isVar∈ x θ) →
  ¬ (isVar∈ x θ') →
  ∃ λ x∈Dom⟨θ←θ'⟩ →
    (set-var {x} θ x∈ v) ← θ' ≡
    set-var {x} (θ ← θ') x∈Dom⟨θ←θ'⟩ v
var-set-←-comm x v θ θ' x∈ x∉Domθ'
  rewrite VarMap.put-union-comm {_} x v (Env.var θ) (Env.var θ') x∉Domθ'
  = VarMap.U-mono {_} {Env.var θ} {Env.var θ'} {x} x∈ , refl

lookup-S-eq : ∀{a b} θ S S∈ S∈₁ → sig-stats{S = S} θ S∈ ≡ a → sig-stats{S = S} θ S∈₁ ≡ b → ¬ a ≡ b → ⊥
lookup-S-eq θ S S∈ S∈' eq1 eq2 neg rewrite sig∈-eq{S}{θ} S∈ S∈'  = neg (trans (sym eq1) eq2)

lookup-s-eq : ∀{a b} θ s s∈ s∈₁ → shr-stats{s = s} θ s∈ ≡ a → shr-stats{s = s} θ s∈₁ ≡ b → ¬ a ≡ b → ⊥
lookup-s-eq θ s s∈ s∈' eq1 eq2 neg rewrite shr∈-eq{s}{θ} s∈ s∈'  = neg (trans (sym eq1) eq2)

lookup-S-¬eq : ∀{a b} θ S S' S∈ S'∈ → sig-stats{S = S} θ S∈ ≡ a → sig-stats{S = S'} θ S'∈ ≡ b → ¬ a ≡ b → ¬ S ≡ S'
lookup-S-¬eq θ S S' S∈ S'∈ S≡ S'≡ a≠b with S Signal.≟ S'
... | yes refl = ⊥-elim (lookup-S-eq θ S S∈ S'∈ S≡ S'≡ a≠b)
... | no x = x

lookup-s-stat-¬eq : ∀{a b} θ s s' s∈ s'∈ → shr-stats{s = s} θ s∈ ≡ a → shr-stats{s = s'} θ s'∈ ≡ b → ¬ a ≡ b → ¬ s ≡ s'
lookup-s-stat-¬eq θ s s' s∈ s'∈ s≡ s'≡ a≠b with s SharedVar.≟ s'
... | yes refl = ⊥-elim (lookup-s-eq θ s s∈ s'∈ s≡ s'≡ a≠b)
... | no x = x

←-=-irr-S : ∀ θ θ' → (Dom θ) ≡ (Dom θ') → ∀ S → (S∈ : isSig∈ S (θ ← θ')) → (S∈2 : isSig∈ S θ')
            → sig-stats{S} (θ ← θ') S∈ ≡ sig-stats{S} θ' S∈2
←-=-irr-S θ θ' eq = SigMap.union-=-irr (sig θ) (sig θ') (cong proj₁ eq)

←-=-irr-s-stats : ∀ θ θ' → (Dom θ) ≡ (Dom θ') → ∀ s → (s∈ : isShr∈ s (θ ← θ')) → (s∈2 : isShr∈ s θ')
            → shr-stats{s} (θ ← θ') s∈ ≡ shr-stats{s} θ' s∈2
←-=-irr-s-stats θ θ' eq a b = (cong proj₁) ∘ (ShrMap.union-=-irr (shr θ) (shr θ') (cong (proj₁ ∘ proj₂) eq) a b)
←-=-irr-s-vals : ∀ θ θ' → (Dom θ) ≡ (Dom θ') → ∀ s → (s∈ : isShr∈ s (θ ← θ')) → (s∈2 : isShr∈ s θ')
            → shr-vals{s} (θ ← θ') s∈ ≡ shr-vals{s} θ' s∈2
←-=-irr-s-vals θ θ' eq a b = (cong proj₂) ∘ (ShrMap.union-=-irr (shr θ) (shr θ') (cong (proj₁ ∘ proj₂) eq) a b)

←-=-irr-x : ∀ θ θ' → (Dom θ) ≡ (Dom θ') → ∀ x → (x∈ : isVar∈ x (θ ← θ')) → (x∈2 : isVar∈ x θ')
            → var-vals{x} (θ ← θ') x∈ ≡ var-vals{x} θ' x∈2
←-=-irr-x θ θ' eq = (VarMap.union-=-irr (var θ) (var θ') (cong (proj₂ ∘ proj₂) eq))

←-single-overwrite-sig : ∀ S stat θ → isSig∈ S θ → ((Θ SigMap.[ S ↦ stat ] [] []) ← θ) ≡ θ
←-single-overwrite-sig S stat θ k∈ rewrite SigMap.single-val-overwrite S stat (sig θ) k∈ = refl

←-single-overwrite-shr : ∀ s stat v θ → isShr∈ s θ → ((Θ [] ShrMap.[ s ↦ (stat ,′ v) ] []) ← θ) ≡ θ
←-single-overwrite-shr s stat v θ k∈ rewrite ShrMap.single-val-overwrite s (stat ,′ v) (shr θ) k∈ = refl

←-single-overwrite-seq : ∀ x n θ → isVar∈ x θ → ((Θ [] [] VarMap.[ x ↦ n ]) ← θ) ≡ θ
←-single-overwrite-seq x n θ k∈ rewrite VarMap.single-val-overwrite x n (var θ) k∈ = refl

sig-set=← : ∀ θ S stat → (S∈ : isSig∈ S θ) → (set-sig{S = S} θ S∈ stat) ≡ (θ ← (Θ SigMap.[ S ↦ stat ] [] []))
sig-set=← θ S stat S∈
    rewrite SigMap.union-insert-eq S stat (sig θ)
          | ShrMap.union-comm (shr θ) [] (λ z _ → λ ())
          | VarMap.union-comm (var θ) [] (λ z _ → λ ())
    = refl

shr-set=← : ∀ θ s stat n → (s∈ : isShr∈ s θ) → (set-shr{s = s} θ s∈ stat n) ≡ (θ ← (Θ [] ShrMap.[ s ↦ (stat ,′ n) ] []))
shr-set=← θ s stat n s∈
    rewrite ShrMap.union-insert-eq s (stat ,′ n) (shr θ)
          | SigMap.union-comm (sig θ) [] (λ z _ → λ ())
          | VarMap.union-comm (var θ) [] (λ z _ → λ ())
    = refl

seq-set=← : ∀ θ x n → (x∈ : isVar∈ x θ) → (set-var{x = x} θ x∈ n) ≡ (θ ← (Θ [] [] VarMap.[ x ↦ n ]))
seq-set=← θ x n x∈
    rewrite VarMap.union-insert-eq x n (var θ)
          | SigMap.union-comm (sig θ) [] (λ z _ → λ ())
          | ShrMap.union-comm (shr θ) [] (λ z _ → λ ())
    = refl

sig-set-clobber : ∀ S stat θ θi S∈ → isSig∈ S θi → (set-sig{S = S} θ S∈ stat) ← θi ≡ θ ← θi
sig-set-clobber S stat θ θi S∈θ S∈θi
  =
   (set-sig{S = S} θ S∈θ stat) ← θi
   ≡⟨ cong (_← θi)(sig-set=← θ S stat S∈θ) ⟩
   (θ ← θ2) ← θi
   ≡⟨ sym (←-assoc θ θ2 θi) ⟩
   (θ ← (θ2 ← θi))
   ≡⟨ cong (θ ←_) (←-single-overwrite-sig S stat θi S∈θi) ⟩
   (θ ← θi) ∎
 where θ2 = Θ SigMap.[ S ↦ stat ] [] []

shr-set-clobber : ∀ v stat n θ θi v∈ → isShr∈ v θi → (set-shr{s = v} θ v∈ stat n) ← θi ≡ θ ← θi
shr-set-clobber v stat n θ θi v∈θ v∈θi
  =
   (set-shr{s = v} θ v∈θ stat n) ← θi
   ≡⟨ cong (_← θi) (shr-set=← θ v stat n v∈θ) ⟩
   (θ ← θ2) ← θi
   ≡⟨ sym (←-assoc θ θ2 θi) ⟩
   (θ ← (θ2 ← θi))
   ≡⟨ cong (θ ←_) (←-single-overwrite-shr v stat n θi v∈θi) ⟩
   (θ ← θi) ∎
 where θ2 = Θ [] ShrMap.[ v ↦ (stat ,′ n) ] []

seq-set-clobber : ∀ v n θ θi v∈ → isVar∈ v θi → (set-var{x = v} θ v∈ n) ← θi ≡ θ ← θi
seq-set-clobber v n θ θi v∈θ v∈θi
  =
   (set-var{x = v} θ v∈θ n) ← θi
   ≡⟨ cong (_← θi) (seq-set=← θ v n v∈θ) ⟩
   (θ ← θ2) ← θi
   ≡⟨ sym (←-assoc θ θ2 θi) ⟩
   (θ ← (θ2 ← θi))
   ≡⟨ cong (θ ←_) (←-single-overwrite-seq v n θi v∈θi) ⟩
   (θ ← θi) ∎
 where θ2 = Θ [] [] VarMap.[ v ↦ n ]

sig-switch : ∀ S stat θ θi S∈ S∈2 → ¬ isSig∈ S θi → set-sig{S = S} (θ ← θi) S∈2 stat ≡ (set-sig{S = S} θ S∈ stat) ← θi
sig-switch S stat θ θi S∈ S∈2 S∉
  = set-sig{S = S} (θ ← θi) S∈2 stat
   ≡⟨ sig-set=← (θ ← θi) S stat S∈2 ⟩
    (θ ← θi) ← θ2
   ≡⟨ ←-assoc-comm θ θi θ2 ((λ z x x₁ → S∉ (subst (_∈ (SigMap.keys (sig θi))) (∈:: (subst (z ∈_) (SigMap.keys-1map S stat) x₁)) x)) , ((λ x x₁ → λ ()) , (λ x x₁ → λ ()))) ⟩
    (θ ← θ2) ← θi
   ≡⟨ cong (_← θi) (sym (sig-set=← θ S stat S∈ )) ⟩
   (set-sig{S = S} θ S∈ stat) ← θi ∎
  where θ2 = Θ SigMap.[ S ↦ stat ] [] []

shr-switch : ∀ s stat n θ θi s∈ s∈2 → ¬ isShr∈ s θi → set-shr{s = s} (θ ← θi) s∈2 stat n ≡ (set-shr{s = s} θ s∈ stat n) ← θi
shr-switch s stat n θ θi s∈ s∈2 s∉
  = set-shr{s = s} (θ ← θi) s∈2 stat n
   ≡⟨ shr-set=← (θ ← θi) s stat n s∈2 ⟩
    (θ ← θi) ← θ2
   ≡⟨ ←-assoc-comm θ θi θ2 ((λ x x₁ → λ ()) , ((λ z x x₁ → s∉ (subst (_∈ (ShrMap.keys (shr θi))) (∈:: (subst (z ∈_) (ShrMap.keys-1map s (stat ,′ n)) x₁)) x)) , (λ x x₁ → λ ()))) ⟩
    (θ ← θ2) ← θi
   ≡⟨ cong (_← θi) (sym (shr-set=← θ s stat n s∈ )) ⟩
   (set-shr{s = s} θ s∈ stat n) ← θi ∎
  where θ2 = Θ [] ShrMap.[ s ↦ (stat ,′ n) ] []

seq-switch : ∀ x n θ θi x∈ x∈2 → ¬ isVar∈ x θi → set-var{x = x} (θ ← θi) x∈2 n ≡ (set-var{x = x} θ x∈ n) ← θi
seq-switch x n θ θi x∈ x∈2 x∉
  = set-var{x = x} (θ ← θi) x∈2 n
   ≡⟨ seq-set=← (θ ← θi) x n x∈2 ⟩
    (θ ← θi) ← θ2
   ≡⟨ ←-assoc-comm θ θi θ2 ((λ x x₁ → λ ()) , ((λ x x₁ → λ ()) , (λ z j x₁ → x∉ (subst (_∈ (VarMap.keys (var θi))) (∈:: (subst (z ∈_) (VarMap.keys-1map x n) x₁)) j)))) ⟩
    (θ ← θ2) ← θi
   ≡⟨ cong (_← θi) (sym (seq-set=← θ x n x∈ )) ⟩
   (set-var{x = x} θ x∈ n) ← θi ∎
  where θ2 = Θ [] [] VarMap.[ x ↦ n ]

sig-switch-right : ∀ S stat θl θr S∈ S∈2 → (θl ← (set-sig{S} θr S∈ stat)) ≡ (set-sig{S} (θl ← θr) S∈2 stat)
sig-switch-right S stat θl θr S∈ S∈2 =
  (θl ← (set-sig{S} θr S∈ stat))
  ≡⟨ cong (θl ←_) (sig-set=← θr S stat S∈) ⟩
  (θl ← (θr ← (Θ SigMap.[ S ↦ stat ] [] [])))
  ≡⟨ ←-assoc θl θr _ ⟩
  ((θl ← θr) ← (Θ SigMap.[ S ↦ stat ] [] []))
  ≡⟨ sym (sig-set=← (θl ← θr) S stat S∈2) ⟩
  (set-sig{S} (θl ← θr) S∈2 stat) ∎

shr-switch-right : ∀ s stat n θl θr s∈ s∈2 → (θl ← (set-shr{s} θr s∈ stat n)) ≡ (set-shr{s} (θl ← θr) s∈2 stat n)
shr-switch-right s stat n θl θr s∈ s∈2 =
  (θl ← (set-shr{s} θr s∈ stat n))
  ≡⟨ cong (θl ←_) (shr-set=← θr s stat n s∈) ⟩
  (θl ← (θr ← (Θ [] ShrMap.[ s ↦ (stat ,′ n) ] [])))
  ≡⟨ ←-assoc θl θr _ ⟩
  ((θl ← θr) ← (Θ [] ShrMap.[ s ↦ (stat ,′ n) ] []))
  ≡⟨ sym (shr-set=← (θl ← θr) s stat n s∈2) ⟩
  (set-shr{s} (θl ← θr) s∈2 stat n) ∎

seq-switch-right : ∀ x n θl θr x∈ x∈2 → (θl ← (set-var{x} θr x∈ n)) ≡ (set-var{x} (θl ← θr) x∈2 n)
seq-switch-right x n θl θr x∈ x∈2 =
  (θl ← (set-var{x} θr x∈ n))
  ≡⟨ cong (θl ←_) (seq-set=← θr x n x∈) ⟩
  (θl ← (θr ← (Θ [] [] VarMap.[ x ↦ n ])))
  ≡⟨ ←-assoc θl θr _ ⟩
  ((θl ← θr) ← (Θ [] [] VarMap.[ x ↦ n ]))
  ≡⟨ sym (seq-set=← (θl ← θr) x n x∈2) ⟩
  (set-var{x} (θl ← θr) x∈2 n) ∎

sig-set-dom-eq : ∀ S stat θ S∈ → (Dom θ) ≡ (Dom (set-sig{S = S} θ S∈ stat))
sig-set-dom-eq S stat θ S∈ rewrite SigMap.update-domain-eq S stat (sig θ) S∈ = refl

shr-set-dom-eq : ∀ s stat n θ s∈ → (Dom θ) ≡ (Dom (set-shr{s = s} θ s∈ stat n))
shr-set-dom-eq s stat n θ s∈ rewrite ShrMap.update-domain-eq s (stat ,′ n) (shr θ) s∈ = refl

seq-set-dom-eq : ∀ x n θ x∈ → (Dom θ) ≡ (Dom (set-var{x = x} θ x∈ n))
seq-set-dom-eq x n θ x∈ rewrite VarMap.update-domain-eq x n (var θ) x∈ = refl

sig-∉-maint : ∀ S S' stat θ S'∈ → ¬ isSig∈ S θ → ¬ isSig∈ S (set-sig{S = S'} θ S'∈ stat)
sig-∉-maint S S' stat θ S'∈ S∉ x rewrite cong proj₁ (sig-set-dom-eq S' stat θ S'∈) = S∉ x

shr-∉-maint : ∀ s s' stat n θ s'∈ → ¬ isShr∈ s θ → ¬ isShr∈ s (set-shr{s = s'} θ s'∈ stat n)
shr-∉-maint s s' stat n θ s'∈ s∉ x rewrite cong snd (shr-set-dom-eq s' stat n θ s'∈) = s∉ x

sig-∉-single : ∀ S S' stat → ¬ S ≡ S' → ¬ isSig∈ S (Θ SigMap.[ S' ↦ stat ] [] [])
sig-∉-single S S' stat neg x rewrite SigMap.keys-1map S' stat with x
... | Any.here px = (Signal.unwrap-neq neg) px
... | Any.there ()

shr-∉-single : ∀ s s' stat n → ¬ s ≡ s' → ¬ isShr∈ s (Θ [] ShrMap.[ s' ↦ (stat ,′ n) ] [])
shr-∉-single s s' stat n neg x rewrite ShrMap.keys-1map s' (stat ,′ n) with x
... | Any.here px = (SharedVar.unwrap-neq neg) px
... | Any.there ()

sig-∈-single : ∀ S stat →  isSig∈ S (Θ SigMap.[ S ↦ stat ] [] [])
sig-∈-single S stat rewrite SigMap.keys-1map S stat = Data.List.Any.here refl

sig-∈-single-right-← : ∀ S stat θ → isSig∈ S (θ ← (Θ SigMap.[ S ↦ stat ] [] []))
sig-∈-single-right-← S stat θ = sig-←-monoʳ S (Θ SigMap.[ S ↦ stat ] [] []) θ (sig-∈-single S stat)

shr-∈-single : ∀ s stat n →  isShr∈ s (Θ [] ShrMap.[ s ↦ (stat ,′ n) ] [])
shr-∈-single s stat n rewrite ShrMap.keys-1map s (stat ,′ n) = Data.List.Any.here refl

sig-single-∈-eq : ∀ S S' stat' →
  isSig∈ S (Θ SigMap.[ S' ↦ stat' ] [] []) →
  Signal.unwrap S ≡ Signal.unwrap S'
sig-single-∈-eq S S' stat' S∈Dom[S'] rewrite SigMap.keys-1map S' stat' = ∈:: S∈Dom[S']

sig-put-mby-overwrite : ∀ S S' θ statneq statput S∈ S'∈ S∈2
                        → ¬ statneq ≡ statput
                        → ¬ (sig-stats{S} θ S∈ ≡ statneq)
                        → ¬ (sig-stats{S} (set-sig{S'} θ S'∈ statput) S∈2 ≡ statneq)
sig-put-mby-overwrite S S' θ statneq statput S∈ S'∈ S∈2 neq≠put ¬ref ref
  with S Signal.≟ S'
... | yes refl = lookup-S-eq (set-sig{S} θ S'∈ statput) S S∈2 S∈2 (sig-putget{S}{θ}{statput} S'∈ S∈2) ref (neq≠put ∘ sym)
... | no ¬refl = ¬ref (trans (sym (sig-putputget/m{S}{S'}{θ} ¬refl S∈ S'∈ S∈2)) ref)

sig-stats-1map' : ∀ S status →
  (S∈ : isSig∈ S (Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty)) →
  sig-stats {S} (Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty) S∈
    ≡ status
sig-stats-1map' S status S∈ = SigMap.putget-m {_} {SigMap.empty} {S} {status} S∈

sig-stats-1map-right-← : ∀ S status θ →
   (S∈ : isSig∈ S (θ ← (Θ SigMap.[ S ↦ status ] [] []))) →
   (sig-stats{S} (θ ← (Θ SigMap.[ S ↦ status ] [] [])) S∈ ≡ status)
sig-stats-1map-right-← S stat θ S∈
  = trans (sig-stats-←-right-irr' S θ (Θ SigMap.[ S ↦ stat ] [] []) (sig-∈-single S stat) S∈) (sig-stats-1map' S stat (sig-∈-single S stat))

sig-put-1map-overwrite' : ∀ S status status' →
  (S∈ : isSig∈ S (Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty)) →
  set-sig {S} (Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty) S∈ status'
    ≡ Θ SigMap.[ S ↦ status' ] ShrMap.empty VarMap.empty
sig-put-1map-overwrite' S status status' S∈
  rewrite SigMap.putput-overwrite SigMap.empty S status status'
  = refl

-- ←-comm : ∀ θ θ' → distinct (Dom θ) (Dom θ') → (θ ← θ') ≡ (θ' ← θ)
sig-set-inner-clobber : ∀ θ θ' θ'' S stat → isSig∈ S θ''
                        → ((θ ← (Θ SigMap.[ S ↦ stat ] [] [])) ← θ') ← θ''
                          ≡
                          ((θ ← θ') ← θ'')
sig-set-inner-clobber θ θ' θ'' S stat S∈θ'' with Sig∈ S θ'
... | yes S∈θ' = (((θ ← (Θ SigMap.[ S ↦ stat ] [] [])) ← θ') ← θ'')
                 ≡⟨ cong (λ x → (x ← θ'')) (sym (←-assoc θ (Θ SigMap.[ S ↦ stat ] [] []) θ')) ⟩
                 ((θ ← ((Θ SigMap.[ S ↦ stat ] [] []) ← θ')) ← θ'')
                 ≡⟨ cong (λ x → (θ ← x) ← θ'' )
                         (←-single-overwrite-sig S stat (Θ (sig θ') (shr θ') (var θ')) S∈θ') ⟩
                 ((θ ← θ') ← θ'') ∎
... | no  S∉θ'  = (((θ ← (Θ SigMap.[ S ↦ stat ] [] [])) ← θ') ← θ'')
                  ≡⟨ cong (λ x → (x ← θ'')) (sym (←-assoc θ (Θ SigMap.[ S ↦ stat ] [] []) θ')) ⟩
                  ((θ ← ((Θ SigMap.[ S ↦ stat ] [] []) ← θ')) ← θ'')
                  ≡⟨ cong (λ x → (θ ← x) ← θ'' )
                          ( ←-comm (Θ SigMap.[ S ↦ stat ] [] []) θ' (ds , ((λ z → λ ()) , (λ z → λ ())))) ⟩
                  ((θ ← (θ' ← (Θ SigMap.[ S ↦ stat ] [] []))) ← θ'')
                  ≡⟨ cong (_← θ'') (←-assoc θ θ' (Θ SigMap.[ S ↦ stat ] [] [])) ⟩
                  (((θ ← θ') ← (Θ SigMap.[ S ↦ stat ] [] [])) ← θ'')
                  ≡⟨ sym (←-assoc (θ ← θ') (Θ SigMap.[ S ↦ stat ] [] []) θ'')  ⟩
                  ((θ ← θ') ← ((Θ SigMap.[ S ↦ stat ] [] []) ← θ''))
                  ≡⟨ cong ((θ ← θ') ←_) (←-single-overwrite-sig S stat (Θ (sig θ'') (shr θ'') (var θ''))
                                           S∈θ'') ⟩
                  ((θ ← θ') ← θ'')
                  ∎
             where
               ds : distinct' (proj₁ (Dom (Θ SigMap.[ S ↦ stat ] [] []))) (proj₁ (Dom θ'))
               ds z x y rewrite SigMap.keys-1map S stat with x
               ... | Any.here refl = ⊥-elim (S∉θ' y)
               ... | Any.there ()

sig-single-notin-distinct : ∀ S status θ →
  Signal.unwrap S ∉ proj₁ (Dom θ) →
  distinct (Dom (Θ SigMap.[ S ↦ status ] [] [])) (Dom θ)
sig-single-notin-distinct S status θ S∉Domθ =
  (λ S'' S''∈[S] S''∈Domθ →
    S∉Domθ
      (subst (_∈ proj₁ (Dom θ))
        (∈:: (subst (S'' ∈_) (SigMap.keys-1map S status) S''∈[S]))
        S''∈Domθ)) ,′
  (λ _ ()) ,′
  (λ _ ())

-- a special case of sig-single-notin-distinct
sig-single-noteq-distinct : ∀ S status S' status' →
  ¬ Signal.unwrap S ≡ Signal.unwrap S' →
  distinct (Dom (Θ SigMap.[ S ↦ status ] [] [])) (Dom (Θ SigMap.[ S' ↦ status' ] [] []))
sig-single-noteq-distinct S status S' status' S≢S' =
  (λ S'' S''∈[S] S''∈[S'] →
    S≢S'
      (trans
        (sym (∈:: (subst (S'' ∈_) (SigMap.keys-1map S status) S''∈[S])))
        (∈:: (subst (S'' ∈_) (SigMap.keys-1map S' status') S''∈[S'])))) ,′
  (λ _ ()) ,′
  (λ _ ())

sig-single-←-←-overwrite : ∀ θ S status status' →
  (θ ← Θ SigMap.[ S ↦ status ] [] []) ← Θ SigMap.[ S ↦ status' ] [] [] ≡
  θ ← Θ SigMap.[ S ↦ status' ] [] []
sig-single-←-←-overwrite θ S status status'
  rewrite sym (←-assoc θ (Θ SigMap.[ S ↦ status ] [] []) (Θ SigMap.[ S ↦ status' ] [] []))
  = cong (θ ←_)
      (←-single-overwrite-sig S status (Θ SigMap.[ S ↦ status' ] [] [])
        (sig-∈-single S status'))

sig-set-clobber-single-as-← : ∀ S status status' θ S∈ → (set-sig{S} (θ ← (Θ SigMap.[ S ↦ status' ] [] [])) S∈ status) ≡ (θ ← (Θ SigMap.[ S ↦ status ] [] []))
sig-set-clobber-single-as-← S status status' θ S∈
  =(begin
     (set-sig{S} (θ ← θs1) ((sig-∈-single-right-← S status' θ)) status)
     ≡⟨  sym (sig-switch-right S status θ θs1 ((sig-∈-single S status')) ((sig-∈-single-right-← S status' θ)))  ⟩
     (θ ← (set-sig{S} θs1 ((sig-∈-single S status')) status))
     ≡⟨  cong (_←_ θ) (sig-put-1map-overwrite' S status' status ((sig-∈-single S status')))  ⟩
     (θ ← θs2) ∎)
   where
     θs1 = (Θ SigMap.[ S ↦ status' ] [] [])
     θs2 = (Θ SigMap.[ S ↦ status ] [] [])

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DistLattice.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice.Base

open Iso

private
  variable
    ℓ ℓ' : Level

record IsDistLattice {L : Type ℓ}
                     (0l 1l : L) (_∨l_ _∧l_ : L → L → L) : Type ℓ where

  constructor isdistlattice

  field
    isLattice : IsLattice 0l 1l _∨l_ _∧l_
    ∨l-dist-∧l : (x y z : L) → (x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z))
                              × ((y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x))
    ∧l-dist-∨l : (x y z : L) → (x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z))
                              × ((y ∨l z) ∧l x ≡ (y ∧l x) ∨l (z ∧l x))

  open IsLattice isLattice public

  ∨lLdist∧l :  (x y z : L) → x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z)
  ∨lLdist∧l x y z = ∨l-dist-∧l x y z .fst

  ∨lRdist∧l : (x y z : L) → (y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x)
  ∨lRdist∧l x y z = ∨l-dist-∧l x y z .snd

  ∧lLdist∨l : (x y z : L) → x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z)
  ∧lLdist∨l x y z = ∧l-dist-∨l x y z .fst

  ∧lRdist∨l : (x y z : L) → (y ∨l z) ∧l x ≡ (y ∧l x) ∨l (z ∧l x)
  ∧lRdist∨l x y z = ∧l-dist-∨l x y z .snd

record DistLatticeStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor distlatticestr

  field
    0l            : A
    1l            : A
    _∨l_         : A → A → A
    _∧l_         : A → A → A
    isDistLattice : IsDistLattice 0l 1l _∨l_ _∧l_

  infix 7 _∨l_
  infix 6 _∧l_

  open IsDistLattice isDistLattice public

DistLattice : ∀ ℓ → Type (ℓ-suc ℓ)
DistLattice ℓ = TypeWithStr ℓ DistLatticeStr

isSetDistLattice : (L : DistLattice ℓ) → isSet ⟨ L ⟩
isSetDistLattice L = L .snd .DistLatticeStr.is-set

-- when proving the axioms for a distributive lattice
-- we use the fact that from distributivity and absorption
-- of ∧l over ∨l we can derive distributivity and absorption
-- of ∨l over ∧l and vice versa. We give provide thus two
-- ways of making a distributive lattice...
makeIsDistLattice∧lOver∨l : {L : Type ℓ} {0l 1l : L} {_∨l_ _∧l_ : L → L → L}
             (is-setL : isSet L)
             (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
             (∨l-rid : (x : L) → x ∨l 0l ≡ x)
             (∨l-comm : (x y : L) → x ∨l y ≡ y ∨l x)
             (∧l-assoc : (x y z : L) → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l z)
             (∧l-rid : (x : L) → x ∧l 1l ≡ x)
             (∧l-comm : (x y : L) → x ∧l y ≡ y ∧l x)
             (∧l-absorb-∨l : (x y : L) → x ∧l (x ∨l y) ≡ x)
             (∧l-ldist-∨l : (x y z : L) → x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z))
           → IsDistLattice 0l 1l _∨l_ _∧l_
makeIsDistLattice∧lOver∨l {_∨l_ = _∨l_} {_∧l_ = _∧l_} is-setL
                                                      ∨l-assoc ∨l-rid ∨l-comm
                                                      ∧l-assoc ∧l-rid ∧l-comm
                                                      ∧l-absorb-∨l ∧l-ldist-∨l =
 isdistlattice (makeIsLattice is-setL ∨l-assoc ∨l-rid (λ x → ∨l-comm _ x ∙ ∨l-rid x) ∨l-comm
                                      ∧l-assoc ∧l-rid (λ x → ∧l-comm _ x ∙ ∧l-rid x) ∧l-comm
                                      ∨l-absorb-∧l ∧l-absorb-∨l)
               (λ x y z → ∨l-ldist-∧l _ _ _ , ∨l-rdist-∧l _ _ _)
               (λ x y z → ∧l-ldist-∨l _ _ _ , ∧l-rdist-∨l _ _ _)
 where
 ∧l-idem : ∀ x → x ∧l x ≡ x
 ∧l-idem x = cong (x ∧l_) (sym (∨l-rid _)) ∙ ∧l-absorb-∨l _ _

 ∨l-absorb-∧l : ∀ x y → x ∨l (x ∧l y) ≡ x
 ∨l-absorb-∧l x y =
              cong (_∨l (x ∧l y)) (sym (∧l-idem _)) ∙∙ sym (∧l-ldist-∨l _ _ _) ∙∙ ∧l-absorb-∨l _ _

 ∧l-rdist-∨l : ∀ x y z → (y ∨l z) ∧l x ≡ (y ∧l x) ∨l (z ∧l x)
 ∧l-rdist-∨l _ _ _ = ∧l-comm _ _ ∙∙ ∧l-ldist-∨l _ _ _ ∙∙ cong₂ (_∨l_) (∧l-comm _ _) (∧l-comm _ _)

 ∨l-ldist-∧l : ∀ x y z → x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z)
 ∨l-ldist-∧l x y z = x ∨l (y ∧l z)
                   ≡⟨ cong (_∨l (y ∧l z)) (sym (∨l-absorb-∧l _ _)) ⟩
                     (x ∨l (x ∧l z)) ∨l (y ∧l z)
                   ≡⟨ sym (∨l-assoc _ _ _) ⟩
                     x ∨l ((x ∧l z) ∨l (y ∧l z))
                   ≡⟨ cong (_∨l ((x ∧l z) ∨l (y ∧l z))) (sym (∧l-comm _ _ ∙ ∧l-absorb-∨l _ _)) ⟩
                     ((x ∨l y) ∧l x) ∨l ((x ∧l z) ∨l (y ∧l z))
                   ≡⟨ cong (((x ∨l y) ∧l x) ∨l_) (sym (∧l-rdist-∨l _ _ _)) ⟩
                     ((x ∨l y) ∧l x) ∨l ((x ∨l y) ∧l z)
                   ≡⟨ sym (∧l-ldist-∨l _ _ _) ⟩
                     (x ∨l y) ∧l (x ∨l z) ∎

 ∨l-rdist-∧l : ∀ x y z → (y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x)
 ∨l-rdist-∧l x y z = ∨l-comm _ x ∙∙ ∨l-ldist-∧l _ _ _ ∙∙ cong₂ (_∧l_) (∨l-comm _ _) (∨l-comm _ _)

makeDistLattice∧lOver∨l : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L)
             (is-setL : isSet L)
             (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
             (∨l-rid : (x : L) → x ∨l 0l ≡ x)
             (∨l-comm : (x y : L) → x ∨l y ≡ y ∨l x)
             (∧l-assoc : (x y z : L) → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l z)
             (∧l-rid : (x : L) → x ∧l 1l ≡ x)
             (∧l-comm : (x y : L) → x ∧l y ≡ y ∧l x)
             (∧l-absorb-∨l : (x y : L) → x ∧l (x ∨l y) ≡ x)
             (∧l-ldist-∨l : (x y z : L) → x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z))
           → DistLattice ℓ
makeDistLattice∧lOver∨l 0l 1l _∨l_ _∧l_ is-setL ∨l-assoc ∨l-rid ∨l-comm
                                                   ∧l-assoc ∧l-rid ∧l-comm
                                                   ∧l-absorb-∨l ∧l-ldist-∨l =
                _ , distlatticestr _ _ _ _
                (makeIsDistLattice∧lOver∨l is-setL ∨l-assoc ∨l-rid ∨l-comm
                                                    ∧l-assoc ∧l-rid ∧l-comm
                                                    ∧l-absorb-∨l ∧l-ldist-∨l)

makeIsDistLattice∨lOver∧l : {L : Type ℓ} {0l 1l : L} {_∨l_ _∧l_ : L → L → L}
                    (is-setL : isSet L)
                    (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
                    (∨l-rid : (x : L) → x ∨l 0l ≡ x)
                    (∨l-comm : (x y : L) → x ∨l y ≡ y ∨l x)
                    (∧l-assoc : (x y z : L) → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l z)
                    (∧l-rid : (x : L) → x ∧l 1l ≡ x)
                    (∧l-comm : (x y : L) → x ∧l y ≡ y ∧l x)
                    (∨l-absorb-∧l : (x y : L) → x ∨l (x ∧l y) ≡ x)
                    (∨l-ldist-∧l : (x y z : L) → x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z))
                  → IsDistLattice 0l 1l _∨l_ _∧l_
makeIsDistLattice∨lOver∧l {_∨l_ = _∨l_} {_∧l_ = _∧l_} is-setL
                                                      ∨l-assoc ∨l-rid ∨l-comm
                                                      ∧l-assoc ∧l-rid ∧l-comm
                                                      ∨l-absorb-∧l ∨l-ldist-∧l =
  isdistlattice
  (makeIsLattice is-setL ∨l-assoc ∨l-rid (λ x → ∨l-comm _ x ∙ ∨l-rid x) ∨l-comm
                         ∧l-assoc ∧l-rid (λ x → ∧l-comm _ x ∙ ∧l-rid x) ∧l-comm
                         ∨l-absorb-∧l ∧l-absorb-∨l)
                         (λ x y z → ∨l-ldist-∧l _ _ _ , ∨l-rdist-∧l _ _ _)
                         (λ x y z → ∧l-ldist-∨l _ _ _ , ∧l-rdist-∨l _ _ _)
  where
  ∨l-idem : ∀ x → x ∨l x ≡ x
  ∨l-idem x = cong (x ∨l_) (sym (∧l-rid _)) ∙ ∨l-absorb-∧l _ _

  ∧l-absorb-∨l : ∀ x y → x ∧l (x ∨l y) ≡ x
  ∧l-absorb-∨l x y =
    cong (_∧l (x ∨l y)) (sym (∨l-idem _)) ∙∙ sym (∨l-ldist-∧l _ _ _) ∙∙ ∨l-absorb-∧l _ _

  ∨l-rdist-∧l : ∀ x y z → (y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x)
  ∨l-rdist-∧l _ _ _ = ∨l-comm _ _ ∙∙ ∨l-ldist-∧l _ _ _ ∙∙ cong₂ (_∧l_) (∨l-comm _ _) (∨l-comm _ _)

  ∧l-ldist-∨l : ∀ x y z → x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z)
  ∧l-ldist-∨l x y z = x ∧l (y ∨l z)
                    ≡⟨ cong (_∧l (y ∨l z)) (sym (∧l-absorb-∨l _ _)) ⟩
                      (x ∧l (x ∨l z)) ∧l (y ∨l z)
                    ≡⟨ sym (∧l-assoc _ _ _) ⟩
                      x ∧l ((x ∨l z) ∧l (y ∨l z))
                    ≡⟨ cong (_∧l ((x ∨l z) ∧l (y ∨l z))) (sym (∨l-comm _ _ ∙ ∨l-absorb-∧l _ _)) ⟩
                      ((x ∧l y) ∨l x) ∧l ((x ∨l z) ∧l (y ∨l z))
                    ≡⟨ cong (((x ∧l y) ∨l x) ∧l_) (sym (∨l-rdist-∧l _ _ _)) ⟩
                      ((x ∧l y) ∨l x) ∧l ((x ∧l y) ∨l z)
                    ≡⟨ sym (∨l-ldist-∧l _ _ _) ⟩
                      (x ∧l y) ∨l (x ∧l z) ∎

  ∧l-rdist-∨l : ∀ x y z → (y ∨l z) ∧l x ≡ (y ∧l x) ∨l (z ∧l x)
  ∧l-rdist-∨l x y z = ∧l-comm _ x ∙∙ ∧l-ldist-∨l _ _ _ ∙∙ cong₂ (_∨l_) (∧l-comm _ _) (∧l-comm _ _)

makeDistLattice∨lOver∧l : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L)
                    (is-setL : isSet L)
                    (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
                    (∨l-rid : (x : L) → x ∨l 0l ≡ x)
                    (∨l-comm : (x y : L) → x ∨l y ≡ y ∨l x)
                    (∧l-assoc : (x y z : L) → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l z)
                    (∧l-rid : (x : L) → x ∧l 1l ≡ x)
                    (∧l-comm : (x y : L) → x ∧l y ≡ y ∧l x)
                    (∨l-absorb-∧l : (x y : L) → x ∨l (x ∧l y) ≡ x)
                    (∨l-ldist-∧l : (x y z : L) → x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z))
                  → DistLattice ℓ
makeDistLattice∨lOver∧l  0l 1l _∨l_ _∧l_ is-setL ∨l-assoc ∨l-rid ∨l-comm
                                                    ∧l-assoc ∧l-rid ∧l-comm
                                                    ∨l-absorb-∧l ∨l-ldist-∧l =
                _ , distlatticestr _ _ _ _
                (makeIsDistLattice∨lOver∧l is-setL ∨l-assoc ∨l-rid ∨l-comm
                                            ∧l-assoc ∧l-rid ∧l-comm ∨l-absorb-∧l ∨l-ldist-∧l)

DistLatticeStr→LatticeStr : {A : Type ℓ} → DistLatticeStr A → LatticeStr A
DistLatticeStr→LatticeStr (distlatticestr  _ _ _ _ H) =
                           latticestr  _ _ _ _ (IsDistLattice.isLattice H)

DistLattice→Lattice : DistLattice ℓ → Lattice ℓ
DistLattice→Lattice (_ , distlatticestr _ _ _ _  H) =
                     _ , latticestr  _ _ _ _ (IsDistLattice.isLattice H)

DistLatticeHom : (L : DistLattice ℓ) (M : DistLattice ℓ') → Type (ℓ-max ℓ ℓ')
DistLatticeHom L M = LatticeHom (DistLattice→Lattice L) (DistLattice→Lattice M)

IsDistLatticeEquiv : {A : Type ℓ} {B : Type ℓ'}
  (L : DistLatticeStr A) (e : A ≃ B) (M : DistLatticeStr B) → Type (ℓ-max ℓ ℓ')
IsDistLatticeEquiv L e M =
                   IsLatticeHom (DistLatticeStr→LatticeStr L) (e .fst) (DistLatticeStr→LatticeStr M)

DistLatticeEquiv : (L : DistLattice ℓ) (M : DistLattice ℓ') → Type (ℓ-max ℓ ℓ')
DistLatticeEquiv L M = Σ[ e ∈ (L .fst ≃ M .fst) ] IsDistLatticeEquiv (L .snd) e (M .snd)

isPropIsDistLattice : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L)
             → isProp (IsDistLattice 0l 1l _∨l_ _∧l_)
isPropIsDistLattice 0l 1l _∨l_ _∧l_ (isdistlattice LL LD1 LD2) (isdistlattice ML MD1 MD2) =
  λ i → isdistlattice (isPropIsLattice _ _ _ _ LL ML i) (isPropDist1 LD1 MD1 i)
                                                        (isPropDist2 LD2 MD2 i)
  where
  isSetL : isSet _
  isSetL = LL .IsLattice.joinSemilattice .IsSemilattice.isCommMonoid .IsCommMonoid.isMonoid
              .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropDist1 : isProp ((x y z : _) → (x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z))
                                    × ((y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x)))
  isPropDist1 = isPropΠ3 (λ _ _ _ → isProp× (isSetL _ _) (isSetL _ _))

  isPropDist2 : isProp ((x y z : _) → (x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z))
                                    × ((y ∨l z) ∧l x ≡ (y ∧l x) ∨l (z ∧l x)))
  isPropDist2 = isPropΠ3 (λ _ _ _ → isProp× (isSetL _ _) (isSetL _ _))

𝒮ᴰ-DistLattice : DUARel (𝒮-Univ ℓ) DistLatticeStr ℓ
𝒮ᴰ-DistLattice =
  𝒮ᴰ-Record (𝒮-Univ _) IsDistLatticeEquiv
    (fields:
      data[ 0l ∣ null ∣ pres0 ]
      data[ 1l ∣ null ∣ pres1 ]
      data[ _∨l_ ∣ bin ∣ pres∨l ]
      data[ _∧l_ ∣ bin ∣ pres∧l ]
      prop[ isDistLattice ∣ (λ _ _ → isPropIsDistLattice  _ _ _ _) ])
 where
  open DistLatticeStr
  open IsLatticeHom

  -- faster with some sharing
  null = autoDUARel (𝒮-Univ _) (λ A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

DistLatticePath : (L M : DistLattice ℓ) → DistLatticeEquiv L M ≃ (L ≡ M)
DistLatticePath = ∫ 𝒮ᴰ-DistLattice .UARel.ua

ext: agda


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

module Cubical.Relation.Binary.Raw.Construct.Intersection where

open import Cubical.Core.Everything
open import Cubical.Foundations.Function using (_∘_)

open import Cubical.Data.Prod
open import Cubical.Data.Sum.Base using (_⊎_; inl; inr; rec)
open import Cubical.Relation.Binary.Raw
open import Cubical.Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- Definition

_∩_ : ∀ {a b ℓ₁ ℓ₂} {A : Type a} {B : Type b} →
      RawREL A B ℓ₁ → RawREL A B ℓ₂ → RawREL A B (ℓ-max ℓ₁ ℓ₂)
L ∩ R = λ i j → L i j × R i j

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

module _ {a ℓ₁ ℓ₂} {A : Type a} (L : RawRel A ℓ₁) (R : RawRel A ℓ₂) where

  reflexive : Reflexive L → Reflexive R → Reflexive (L ∩ R)
  reflexive L-refl R-refl = L-refl , R-refl

  symmetric : Symmetric L → Symmetric R → Symmetric (L ∩ R)
  symmetric L-sym R-sym = map L-sym R-sym

  transitive : Transitive L → Transitive R → Transitive (L ∩ R)
  transitive L-trans R-trans (xLy , xRy) (yLz , yRz) = L-trans xLy yLz , R-trans xRy yRz

  respects : ∀ {p} (P : A → Type p) →
             P Respects L ⊎ P Respects R → P Respects (L ∩ R)
  respects P resp (Lxy , Rxy) = rec (λ x → x Lxy) (λ x → x Rxy) resp

  min : ∀ {⊤} → Minimum L ⊤ → Minimum R ⊤ → Minimum (L ∩ R) ⊤
  min L-min R-min = intro L-min R-min

  max : ∀ {⊥} → Maximum L ⊥ → Maximum R ⊥ → Maximum (L ∩ R) ⊥
  max L-max R-max = intro L-max R-max

  toNotEq : ToNotEq L ⊎ ToNotEq R → ToNotEq (L ∩ R)
  toNotEq tonoteq (Lxy , Rxy) x≡y = rec (λ x → x Lxy x≡y) (λ y → y Rxy x≡y) tonoteq

  irreflexive : Irreflexive L ⊎ Irreflexive R → Irreflexive (L ∩ R)
  irreflexive irrefl (xLx , xRx) = rec (λ x → x xLx) (λ y → y xRx) irrefl

  antisymmetric : Antisymmetric L ⊎ Antisymmetric R → Antisymmetric (L ∩ R)
  antisymmetric (inl L-antisym) (Lxy , _) (Lyx , _) = L-antisym Lxy Lyx
  antisymmetric (inr R-antisym) (_ , Rxy) (_ , Ryx) = R-antisym Rxy Ryx

module _ {a b ℓ₁ ℓ₂ ℓ₃} {A : Type a} {B : Type b}
         (≈ : RawREL A B ℓ₁) {L : RawREL A B ℓ₂} {R : RawREL A B ℓ₃} where

  implies : (≈ ⇒ L) → (≈ ⇒ R) → ≈ ⇒ (L ∩ R)
  implies ≈⇒L ≈⇒R = intro ≈⇒L ≈⇒R

module _ {a ℓ₁ ℓ₂ ℓ₃} {A : Type a}
         (≈ : RawRel A ℓ₁) (L : RawRel A ℓ₂) (R : RawRel A ℓ₃) where

  respectsˡ : L Respectsˡ ≈ → R Respectsˡ ≈ → (L ∩ R) Respectsˡ ≈
  respectsˡ L-resp R-resp x≈y = map (L-resp x≈y) (R-resp x≈y)

  respectsʳ : L Respectsʳ ≈ → R Respectsʳ ≈ → (L ∩ R) Respectsʳ ≈
  respectsʳ L-resp R-resp x≈y = map (L-resp x≈y) (R-resp x≈y)

  respects₂ : L Respects₂ ≈ → R Respects₂ ≈ → (L ∩ R) Respects₂ ≈
  respects₂ (Lʳ , Lˡ) (Rʳ , Rˡ) = respectsʳ Lʳ Rʳ , respectsˡ Lˡ Rˡ

module _ {a b ℓ₁ ℓ₂} {A : Type a} {B : Type b} {L : RawREL A B ℓ₁} {R : RawREL A B ℓ₂} where

  decidable : Decidable L → Decidable R → Decidable (L ∩ R)
  decidable L? R? x y = ×-dec (L? x y) (R? x y)

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

module _ {a ℓ₁ ℓ₂} {A : Type a} {L : RawRel A ℓ₁} {R : RawRel A ℓ₂} where

  isPartialEquivalence : IsPartialEquivalence L → IsPartialEquivalence R → IsPartialEquivalence (L ∩ R)
  isPartialEquivalence eqₗ eqᵣ = record
    { symmetric  = symmetric  L R Eqₗ.symmetric  Eqᵣ.symmetric
    ; transitive = transitive L R Eqₗ.transitive Eqᵣ.transitive
    }
    where module Eqₗ = IsPartialEquivalence eqₗ; module Eqᵣ = IsPartialEquivalence eqᵣ

  isEquivalence : IsEquivalence L → IsEquivalence R → IsEquivalence (L ∩ R)
  isEquivalence eqₗ eqᵣ = record
    { isPartialEquivalence = isPartialEquivalence Eqₗ.isPartialEquivalence Eqᵣ.isPartialEquivalence
    ; reflexive            = reflexive L R Eqₗ.reflexive Eqᵣ.reflexive
    }
    where module Eqₗ = IsEquivalence eqₗ; module Eqᵣ = IsEquivalence eqᵣ

  isDecEquivalence : IsDecEquivalence L → IsDecEquivalence R → IsDecEquivalence (L ∩ R)
  isDecEquivalence eqₗ eqᵣ = record
    { isEquivalence = isEquivalence Eqₗ.isEquivalence Eqᵣ.isEquivalence
    ; _≟_           = decidable Eqₗ._≟_ Eqᵣ._≟_
    }
    where module Eqₗ = IsDecEquivalence eqₗ; module Eqᵣ = IsDecEquivalence eqᵣ

  isPreorder : IsPreorder L → IsPreorder R → IsPreorder (L ∩ R)
  isPreorder Oₗ Oᵣ = record
    { reflexive  = reflexive L R Oₗ.reflexive Oᵣ.reflexive
    ; transitive = transitive L R Oₗ.transitive Oᵣ.transitive
    }
    where module Oₗ = IsPreorder Oₗ; module Oᵣ = IsPreorder Oᵣ

  isPartialOrderˡ : IsPartialOrder L → IsPreorder R → IsPartialOrder (L ∩ R)
  isPartialOrderˡ Oₗ Oᵣ = record
    { isPreorder = isPreorder Oₗ.isPreorder Oᵣ
    ; antisym    = antisymmetric L R (inl Oₗ.antisym)
    }
    where module Oₗ = IsPartialOrder Oₗ; module Oᵣ = IsPreorder Oᵣ

  isPartialOrderʳ : IsPreorder L → IsPartialOrder R → IsPartialOrder (L ∩ R)
  isPartialOrderʳ Oₗ Oᵣ = record
    { isPreorder = isPreorder Oₗ Oᵣ.isPreorder
    ; antisym    = antisymmetric L R (inr Oᵣ.antisym)
    }
    where module Oₗ = IsPreorder Oₗ; module Oᵣ = IsPartialOrder Oᵣ

  isStrictPartialOrderˡ : IsStrictPartialOrder L → Transitive R → IsStrictPartialOrder (L ∩ R)
  isStrictPartialOrderˡ Oₗ transitiveᵣ = record
    { irrefl     = irreflexive L R (inl Oₗ.irrefl)
    ; transitive = transitive L R Oₗ.transitive transitiveᵣ
    }
    where module Oₗ = IsStrictPartialOrder Oₗ

  isStrictPartialOrderʳ : Transitive L → IsStrictPartialOrder R → IsStrictPartialOrder (L ∩ R)
  isStrictPartialOrderʳ transitiveₗ Oᵣ = record
    { irrefl     = irreflexive L R (inr Oᵣ.irrefl)
    ; transitive = transitive L R transitiveₗ Oᵣ.transitive
    }
    where module Oᵣ = IsStrictPartialOrder Oᵣ


text:
-- Andreas & Jesper, 2018-05-11, issue #3052 reported by identicalsnowflake
--
-- The problem here was that free variable collection had the standard
-- monoid instance of IntMap, which is just "randomly" picking one variant.
-- Thus, if we have both irrelevant and relevant occurrences of a variable,
-- we get whatever.
-- Now we keep the stronger information (relevant, see maxVarOcc).

{-# OPTIONS --show-irrelevant #-}
-- {-# OPTIONS -v tc.meta.assign:100 -v tc.meta.occurs:45 #-}
-- {-# OPTIONS -v tc.lhs:100 #-}

postulate
  A : Set
  B : A → Set

record Σ : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁
open Σ public

record Foo : Set where
  constructor foo
  field
    .theFoo : Σ

test : Foo → Foo
test (foo (a , b)) = foo (a , thm a b) -- Error at b
  -- Constraint: a, b ⊢ ?0 .a .b a = B a : Set
  -- Note the irrelevant occurrence .a and the relevant occurrence a
  -- on the lhs of this constraint!
  where
    -- Meta ?0 : [.a, .b, x] Set
    postulate thm : (x : A) (y : _) → B x
    -- Underscore should solved by B x
    -- thm x y = y -- WAS: Worked only if definition is given (which

-- Should succeed.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Ex3Lec where

----------------------------------------------------------------------------
-- EXERCISE 3 -- MONADS FOR HUTTON'S RAZOR
--
-- VALUE:     15%
-- DEADLINE:  5pm, Friday 20 November (week 9)
--
-- DON'T SUBMIT, COMMIT!
--
-- The purpose of this exercise is to introduce you to some useful
-- mathematical structures and build good tools for working with
-- vectors
----------------------------------------------------------------------------

open import CS410-Prelude
open import CS410-Monoid
open import CS410-Nat
open import CS410-Vec
open import CS410-Functor

-- HINT: your tasks are heralded with the eminently searchable tag, "???"

----------------------------------------------------------------------------
-- HUTTON'S RAZOR
----------------------------------------------------------------------------

HVal : Set   -- the set of *values* for Hutton's Razor
HVal = Two + Nat   -- Booleans or natural numbers

foo : HVal
foo = tt , ff

goo : HVal
goo = ff , 42

data HExp (X : Set) : Set where
  var        : X -> HExp X                  -- variables
  val        : HVal -> HExp X               -- values
  _+H_ _>=H_ : (e1 e2 : HExp X) -> HExp X   -- addition, comparison
  ifH_then_else_ : (e1 e2 e3 : HExp X) -> HExp X  -- conditional

_>=2_ : Nat -> Nat -> Two
x      >=2  zero   = tt
zero   >=2  suc _  = ff
suc m  >=2  suc n  = m >=2 n

----------------------------------------------------------------------------
-- ??? 3.1 the HExp syntax-with-substitution monad            (score: ? / 2)
----------------------------------------------------------------------------

-- Show that HExp is a monad, where the "bind" operation performs
-- simultaneous substitution (transforming all the variables in a term).

hExpMonad : Monad HExp
hExpMonad = record { return = {!!} ; _>>=_ = {!!} }

----------------------------------------------------------------------------
-- ??? 3.2 the error management monad                         (score: ? / 1)
----------------------------------------------------------------------------

-- show that "+ E" is monadic, generalising the "Maybe" monad by allowing
-- some sort of error report

errorMonad : (E : Set) -> Monad \ V -> V + E   -- "value or error"
errorMonad E = {!!}

----------------------------------------------------------------------------
-- ??? 3.3 the environment monad transformer                   (score: ? / 1)
----------------------------------------------------------------------------

-- show that "+ E" is monadic, generalising the "Maybe" monad by allowing
-- some sort of error report

envMonad : (G : Set){M : Set -> Set} -> Monad M ->
           Monad \ V -> G -> M V      -- "computation in an environment"
envMonad G MM = {!!} where
  open Monad MM

----------------------------------------------------------------------------
-- ??? 3.4 interpreting Hutton's Razor                        (score: ? / 3)
----------------------------------------------------------------------------

-- Implement an interpreter for Hutton's Razor.
-- You will need to construct a type to represent possible run-time errors.
-- Ensure that addition and comparison act on numbers, not Booleans.
-- Ensure that the condition in an "if" is a Boolean, not a number.

data InterpretError : Set where

-- helpful things to build

Env : Set -> Set    -- an environment for a given set of variables
Env X = X -> HVal

Compute : Set{- variables -} -> Set{- values -} -> Set
Compute X V = Env X -> V + InterpretError  -- how to compute a V

computeMonad : {X : Set} -> Monad (Compute X)
computeMonad = {!!} -- build this from the above parts

-- This operation should explain how to get the value of a variable
-- from the environment.
varVal : {X : Set} -> X -> Compute X HVal
varVal x = {!!}

-- These operations should ensure that you get the sort of value
-- that you want, in order to ensure that you don't do bogus
-- computation.
mustBeNat : {X : Set} -> HVal -> Compute X Nat
mustBeNat v = {!!}

mustBeTwo : {X : Set} -> HVal -> Compute X Two
mustBeTwo v = {!!}

-- Now, you're ready to go. Don't introduce the environent explicitly.
-- Use the monad to thread it.

interpret : {X : Set} -> HExp X -> Compute X HVal
interpret {X} = go where
  open Monad (envMonad (Env X) (errorMonad InterpretError))
  go : HExp X -> Env X -> HVal + InterpretError
  go t = {!!}


text:
{-# OPTIONS --type-in-type #-}

open import Data.Product

data ⊥ : Set where

-- f doesn't type check unless we put the equality type in Set
data _≡_ {ℓ} {A : Set ℓ} (a : A) : A → Set where
  refl : a ≡ a

subst : ∀ {ℓ ℓ′} {A : Set ℓ} {a b : A} → (P : A → Set ℓ′) → (p : a ≡ b) → P a → P b
subst _ refl pa = pa

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ A = A → ⊥

℘ : ∀ {ℓ} → Set ℓ → Set _
℘ {ℓ} S = S → Set

{-# NO_POSITIVITY_CHECK #-}
record Bad : Set₁ where
  constructor mkBad
  field bad : ℘ (℘ Bad)

f : ℘ Bad → Bad
f p = mkBad (_≡ p)

fInj : ∀ {p q} → f p ≡ f q → p ≡ q
fInj {p} fp≡fq = subst (λ p≡ → p≡ p) (badInj fp≡fq) refl
  where
  badInj : ∀ {a b} → mkBad a ≡ mkBad b → a ≡ b
  badInj refl = refl

-- type-in-type is for here onwards
P₀ : ℘ Bad
P₀ x = Σ[ P ∈ ℘ Bad ] x ≡ f P × ¬ (P x)

x₀ : Bad
x₀ = f P₀

P₀x₀→¬P₀x₀ : P₀ x₀ → ¬ P₀ x₀
P₀x₀→¬P₀x₀ (P , x₀≡fP , ¬Px₀) P₀x₀ = ¬Px₀ (subst (λ P → P x₀) (fInj x₀≡fP) P₀x₀)

¬P₀x₀→P₀x₀ : ¬ P₀ x₀ → P₀ x₀
¬P₀x₀→P₀x₀ ¬P₀x₀ = P₀ , refl , ¬P₀x₀

¬P₀x₀ : ¬ P₀ x₀
¬P₀x₀ P₀x₀ = P₀x₀→¬P₀x₀ P₀x₀ P₀x₀

false : ⊥
false = ¬P₀x₀ (¬P₀x₀→P₀x₀ ¬P₀x₀)


text:
open import System.IO using ( _>>_ ; putStr ; commit )
open import Data.Natural using ( show )
open import System.IO.Examples.Four using ( four )

module System.IO.Examples.HelloFour where

main = putStr "Hello, " >> putStr (show four) >> putStr ".\n" >> commit

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

open import LogicalFormulae
open import Monoids.Definition

module Semirings.Definition where

record Semiring {a : _} {A : Set a} (Zero One : A) (_+_ : A → A → A) (_*_ : A → A → A) : Set a where
  field
    monoid : Monoid Zero _+_
    commutative : (a b : A) → a + b ≡ b + a
    multMonoid : Monoid One _*_
    productZeroLeft : (a : A) → Zero * a ≡ Zero
    productZeroRight : (a : A) → a * Zero ≡ Zero
    +DistributesOver* : (a b c : A) → a * (b + c) ≡ (a * b) + (a * c)
    +DistributesOver*' : (a b c : A) → (a + b) * c ≡ (a * c) + (b * c)
  +Associative = Monoid.associative monoid
  *Associative = Monoid.associative multMonoid
  productOneLeft = Monoid.idLeft multMonoid
  productOneRight = Monoid.idRight multMonoid
  sumZeroLeft = Monoid.idLeft monoid
  sumZeroRight = Monoid.idRight monoid
  +WellDefined : {a b c d : A} → (a ≡ c) → (b ≡ d) → (a + b) ≡ (c + d)
  +WellDefined refl refl = refl

-- (b+c)(a+a) == b(a+a) + c(a+a) == ba+ba+ca+ca == (ba+ca) + (ba+ca)
-- (b+c)(a+a) ==? (b+c)a+(b+c)a


text:
{-# OPTIONS --type-in-type --rewriting #-}

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

coe : {A B : Set} → A ≡ B → A → B
coe refl x = x

{-# BUILTIN REWRITE _≡_ #-}

Tel = Set
U = Set

variable
  Δ : Tel
  A B : Δ → U
  δ₀ δ₁ : Δ

postulate
  IdTel : (Δ : Tel)(δ₀ δ₁ : Δ) → Tel
  Id : (A : Δ → U){δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → A δ₀ → A δ₁ → U
  ap : {A : Δ → U}(a : (δ : Δ) → A δ)
       → {δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → Id A δ₂ (a δ₀) (a δ₁)

  idTel-sigma : {a₀ : A δ₀}{a₁ : A δ₁}
                → IdTel (Σ Δ A) (δ₀ , a₀) (δ₁ , a₁)
                  ≡ Σ (IdTel Δ δ₀ δ₁) (λ δ₂ → Id A δ₂ a₀ a₁)
  {-# REWRITE idTel-sigma #-}

  id-u : {A₀ A₁ : U}{δ₂ : IdTel Δ δ₀ δ₁}
         → Id {Δ = Δ}(λ _ → U) δ₂ A₀ A₁ ≡ (A₀ → A₁ → U)
  {-# REWRITE id-u #-}

  id-ap : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
          → Id A δ₂ a₀ a₁ ≡ ap {A = λ _ → U} A δ₂ a₀ a₁

  ap-sigma : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
             {B : (δ : Δ) → A δ → U}
             {b₀ : B δ₀ a₀}{b₁ : B δ₁ a₁}→
             ap {Δ = Δ}{A = λ _ → U} (λ δ → Σ (A δ) (B δ))
                δ₂ (a₀ , b₀) (a₁ , b₁) ≡
                Σ (Id A δ₂ a₀ a₁) λ a₂ → Id {Δ = Σ Δ A} (λ (δ , a) → B δ a) (δ₂ , a₂) b₀ b₁
  {-# REWRITE ap-sigma #-}
  {-# REWRITE id-ap #-}

  ap-proj₁ : {δ₂ : IdTel Δ δ₀ δ₁}
             {B : (δ : Δ) → A δ → U}
             {ab : (δ : Δ) → Σ (A δ) (B δ)}
             → ap {Δ = Δ}{A = A}(λ δ → fst (ab δ)) δ₂
               ≡ fst (ap ab δ₂)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

module Issue1719.Spans where

open import Issue1719.Common

record Span : Set₁ where
  constructor span
  field
    A B C : Set
    f : C → A
    g : C → B
open Span public


text:
------------------------------------------------------------------------
-- Products
------------------------------------------------------------------------

module Data.Product where

open import Data.Function
open import Relation.Nullary.Core

infixr 4 _,_
infix  4 ,_
infixr 2 _×_ _-×-_ _-,-_

------------------------------------------------------------------------
-- Definition

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) (y : B x) → Σ A B

∃ : {A : Set} → (A → Set) → Set
∃ = Σ _

∄ : {A : Set} → (A → Set) → Set
∄ P = ¬ ∃ P

∃₂ : {A : Set} {B : A → Set} (C : (x : A) → B x → Set) → Set
∃₂ C = ∃ λ a → ∃ λ b → C a b

_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)

------------------------------------------------------------------------
-- Functions

-- Sometimes the first component can be inferred.

,_ : ∀ {A} {B : A → Set} {x} → B x → ∃ B
, y = _ , y

proj₁ : ∀ {A B} → Σ A B → A
proj₁ (x , y) = x

proj₂ : ∀ {A B} → (p : Σ A B) → B (proj₁ p)
proj₂ (x , y) = y

<_,_> : ∀ {A} {B : A → Set} {C : ∀ {x} → B x → Set}
        (f : (x : A) → B x) → ((x : A) → C (f x)) →
        ((x : A) → Σ (B x) C)
< f , g > x = (f x , g x)

map : ∀ {A B P Q} →
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g = < f ∘ proj₁ , g ∘ proj₂ >

zip : ∀ {A B C P Q R} →
      (_∙_ : A → B → C) →
      (∀ {x y} → P x → Q y → R (x ∙ y)) →
      Σ A P → Σ B Q → Σ C R
zip _∙_ _∘_ p₁ p₂ = (proj₁ p₁ ∙ proj₁ p₂ , proj₂ p₁ ∘ proj₂ p₂)

swap : ∀ {A B} → A × B → B × A
swap = < proj₂ , proj₁ >

_-×-_ : ∀ {A B} → (A → B → Set) → (A → B → Set) → (A → B → Set)
f -×- g = f -[ _×_ ]₁- g

_-,-_ : ∀ {A B C D} → (A → B → C) → (A → B → D) → (A → B → C × D)
f -,- g = f -[ _,_ ]- g

curry : {A : Set} {B : A → Set} {C : Σ A B → Set} →
        ((p : Σ A B) → C p) →
        ((x : A) → (y : B x) → C (x , y))
curry f x y = f (x , y)

uncurry : {A : Set} {B : A → Set} {C : Σ A B → Set} →
          ((x : A) → (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f (p₁ , p₂) = f p₁ p₂

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Equiv.Base where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude

open import Cubical.Core.Glue public
  using ( isEquiv ; equiv-proof ; _≃_ ; equivFun ; equivProof )

fiber : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) (y : B) → Type (ℓ-max ℓ ℓ')
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

-- The identity equivalence
idIsEquiv : ∀ {ℓ} (A : Type ℓ) → isEquiv (idfun A)
equiv-proof (idIsEquiv A) y =
  ((y , refl) , λ z i → z .snd (~ i) , λ j → z .snd (~ i ∨ j))

idEquiv : ∀ {ℓ} (A : Type ℓ) → A ≃ A
idEquiv A .fst = idfun A
idEquiv A .snd = idIsEquiv A

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Prelude.List.Base where

open import Prelude.Nat
open import Prelude.Bool
open import Prelude.Maybe
open import Prelude.Product
open import Prelude.Empty
open import Prelude.Function
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.Monad
open import Prelude.Decidable
open import Prelude.Equality
open import Prelude.Ord
open import Prelude.Semiring
open import Prelude.Strict
open import Prelude.Variables

open import Agda.Builtin.List public

infixr 5 _++_

pattern [_] x = x ∷ []

singleton : A → List A
singleton x = x ∷ []

map : (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

_++_ : List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

length : List A → Nat
length []       = 0
length (x ∷ xs) = 1 + length xs

foldr : (A → B → B) → B → List A → B
foldr f z []       = z
foldr f z (x ∷ xs) = f x (foldr f z xs)

foldl : (B → A → B) → B → List A → B
foldl f z []       = z
foldl f z (x ∷ xs) = foldl f (f z x) xs

foldl! : (B → A → B) → B → List A → B
foldl! f z []       = z
foldl! f z (x ∷ xs) = force (f z x) λ z′ → foldl! f z′ xs

reverse : List A → List A
reverse xs = foldl (flip _∷_) [] xs

concat : List (List A) → List A
concat = foldr _++_ []

concatMap : (A → List B) → List A → List B
concatMap f = concat ∘ map f

filter : (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) = if p x then x ∷ filter p xs
                           else filter p xs

catMaybes : List (Maybe A) → List A
catMaybes [] = []
catMaybes (x ∷ xs) = maybe (catMaybes xs) (_∷ catMaybes xs) x

all? : (A → Bool) → List A → Bool
all? p []       = true
all? p (x ∷ xs) = p x && all? p xs

any? : (A → Bool) → List A → Bool
any? p []       = false
any? p (x ∷ xs) = p x || any? p xs

take : Nat → List A → List A
take zero    _        = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

drop : Nat → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

takeWhile : (A → Bool) → List A → List A
takeWhile p []       = []
takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs
                              else []

dropWhile : (A → Bool) → List A → List A
dropWhile p [] = []
dropWhile p (x ∷ xs) = if p x then dropWhile p xs
                              else x ∷ xs

splitAt : Nat → List A → List A × List A
splitAt zero    xs       = [] , xs
splitAt (suc n) []       = [] , []
splitAt (suc n) (x ∷ xs) = first (x ∷_) (splitAt n xs)

null : List A → Bool
null []      = true
null (_ ∷ _) = false

elem : ⦃ Eq A ⦄ → A → List A → Bool
elem x xs = not (null (filter (isYes ∘ _==_ x) xs))

lookup : ⦃ Eq A ⦄ → List (A × B) → A → Maybe B
lookup [] _ = nothing
lookup ((x₁ , v) ∷ xs) x = ifYes (x == x₁) then just v else lookup xs x

nub : ⦃ Eq A ⦄ → List A → List A
nub [] = []
nub (x ∷ xs) = x ∷ filter (isNo ∘ (x ==_)) (nub xs)

index : List A → Nat → Maybe A
index [] _             = nothing
index (x ∷ xs) 0       = just x
index (x ∷ xs) (suc i) = index xs i

replicate : Nat → A → List A
replicate zero x = []
replicate (suc n) x = x ∷ replicate n x

zipWith : (A → B → C) → List A → List B → List C
zipWith f [] _ = []
zipWith f _ [] = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

zip : List A → List B → List (A × B)
zip = zipWith _,_

punctuate : A → List A → List A
punctuate z []       = []
punctuate z [ x ]    = [ x ]
punctuate z (x ∷ xs) = x ∷ z ∷ punctuate z xs

replicateA : ⦃ Applicative F ⦄ → Nat → F A → F (List A)
replicateA zero    _ = pure []
replicateA (suc n) x = pure _∷_ <*> x <*> replicateA n x

module _ ⦃ _ : Semiring A ⦄ where

  sum : List A → A
  sum = foldl! _+_ zro

  product : List A → A
  product = foldl! _*_ one

  sumR : List A → A
  sumR = foldr _+_ zro

  productR : List A → A
  productR = foldr _*_ one

module _ ⦃ _ : Ord A ⦄ where

  insert : A → List A → List A
  insert x [] = x ∷ []
  insert x (y ∷ xs) = if x <? y then x ∷ y ∷ xs else y ∷ insert x xs

  sort : List A → List A
  sort [] = []
  sort (x ∷ xs) = insert x (sort xs)

infix 10 from_for_ from_to_ from_for_step_ from-to-step
from_for_ : Nat → Nat → List Nat
from 0 for 0     = []  -- make strict
from a for 0     = []
from a for suc d = a ∷ from suc a for d

from_for_step_ : Nat → Nat → Nat → List Nat
from 0 for 0     step _  = []  -- make strict
from a for 0     step _  = []
from a for suc c step d = a ∷ from a + d for c step d

from_to_ : Nat → Nat → List Nat
from a to b = from a for (suc b - a)

syntax from-to-step d a b = from a to b step d
from-to-step : (d : Nat) {{_ : NonZero d}} → Nat → Nat → List Nat
from-to-step d a b = from a for 1 + (b - a) div d step d

--- Equality ---

cons-inj-tail : x ∷ xs ≡ y ∷ ys → xs ≡ ys
cons-inj-tail refl = refl

cons-inj-head : x ∷ xs ≡ y ∷ ys → x ≡ y
cons-inj-head refl = refl

private
  dec-∷ : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y ∷ ys)
  dec-∷ (yes refl) (yes refl) = yes refl
  dec-∷ _ (no neq) = no λ eq → neq (cons-inj-tail eq)
  dec-∷ (no neq) _ = no λ eq → neq (cons-inj-head eq)

  eqList : ⦃ Eq A ⦄ → (xs ys : List A) → Dec (xs ≡ ys)
  eqList [] [] = yes refl
  eqList [] (_ ∷ _) = no (λ ())
  eqList (_ ∷ _) [] = no (λ ())
  eqList (x ∷ xs) (y ∷ ys) = dec-∷ (x == y) (eqList xs ys)

instance
  EqList : ⦃ Eq A ⦄ → Eq (List A)
  _==_ {{EqList}} = eqList

--- Ord ---

data LessList (_<_ : A → A → Set ℓ) : List A → List A → Set ℓ where
  nil<cons : LessList _<_ [] (x ∷ xs)
  head<    : x < y → LessList _<_ (x ∷ xs) (y ∷ ys)
  tail<    : LessList _<_ xs ys → LessList _<_ (x ∷ xs) (x ∷ ys)

compareCons : ∀ {_<_ : A → A → Set ℓ} →
                Comparison _<_ x y →
                Comparison (LessList _<_) xs ys →
                Comparison (LessList _<_) (x ∷ xs) (y ∷ ys)
compareCons (less lt)    _            = less (head< lt)
compareCons (greater gt) _            = greater (head< gt)
compareCons (equal refl) (less lt)    = less (tail< lt)
compareCons (equal refl) (greater gt) = greater (tail< gt)
compareCons (equal refl) (equal refl) = equal refl

compareList : ∀ {_<_ : A → A → Set ℓ} (cmp : ∀ x y → Comparison _<_ x y) (xs ys : List A) →
              Comparison (LessList _<_) xs ys
compareList cmp [] [] = equal refl
compareList cmp [] (x ∷ ys) = less nil<cons
compareList cmp (x ∷ xs) [] = greater nil<cons
compareList cmp (x ∷ xs) (y ∷ ys) = compareCons (cmp x y) (compareList cmp xs ys)

instance
  OrdList : ⦃ Ord A ⦄ → Ord (List A)
  OrdList = defaultOrd (compareList compare)

  OrdListLaws : ⦃ Ord/Laws A ⦄ → Ord/Laws (List A)
  Ord/Laws.super OrdListLaws = it
  less-antirefl {{OrdListLaws {A = A}}} (head< hd) = less-antirefl {A = A} hd
  less-antirefl {{OrdListLaws {A = A}}} (tail< tl) = less-antirefl {A = List A} tl
  less-trans {{OrdListLaws}} nil<cons   (head< hd)  = nil<cons
  less-trans {{OrdListLaws}} nil<cons   (tail< tl)  = nil<cons
  less-trans {{OrdListLaws {A = A}}} (head< hd) (head< hd₁) = head< (less-trans {A = A} hd hd₁)
  less-trans {{OrdListLaws {A = A}}} (head< hd) (tail< tl)  = head< hd
  less-trans {{OrdListLaws {A = A}}} (tail< tl) (head< hd)  = head< hd
  less-trans {{OrdListLaws {A = A}}} (tail< tl) (tail< tl₁) = tail< (less-trans {A = List A} tl tl₁)

--- Functor ---

instance
  FunctorList : Functor (List {ℓ})
  fmap {{FunctorList}} = map

  FunctorList′ : Functor′ {ℓ₁} {ℓ₂} List
  fmap′ {{FunctorList′}} = map

  ApplicativeList : Applicative (List {ℓ})
  pure  {{ApplicativeList}} x = x ∷ []
  _<*>_ {{ApplicativeList}} = monadAp (flip concatMap)

  ApplicativeList′ : Applicative′ {ℓ₁} {ℓ₂} List
  _<*>′_ {{ApplicativeList′}} = monadAp′ (flip concatMap)

  MonadList : Monad (List {ℓ})
  _>>=_  {{MonadList}} xs f = concatMap f xs

  MonadList′ : Monad′ {ℓ₁} {ℓ₂} List
  _>>=′_ {{MonadList′}} xs f = concatMap f xs

--- More functions ---

IsPrefixOf : {A : Set ℓ} → List A → List A → Set ℓ
IsPrefixOf xs ys = ∃ zs , ys ≡ xs ++ zs

isPrefixOf : ⦃ Eq A ⦄ → (xs ys : List A) → Dec (IsPrefixOf xs ys)
isPrefixOf []       ys = yes (ys , refl)
isPrefixOf (x ∷ xs) [] = no λ where (zs , ())
isPrefixOf (x ∷ xs) (y ∷ ys) with y == x | isPrefixOf xs ys
... | yes y=x | yes (zs , xs⊑ys) = yes (zs , (_∷_ $≡ y=x *≡ xs⊑ys))
... | _       | no noprefix      = no λ where (zs , eq) → noprefix ((zs , cons-inj-tail eq))
... | no  y≠x | _                = no λ where (zs , eq) → y≠x (cons-inj-head eq)

isPrefixOf? : ⦃ Eq A ⦄ → List A → List A → Bool
isPrefixOf? xs ys = isYes (isPrefixOf xs ys)

dropPrefix : ⦃ Eq A ⦄ → List A → List A → Maybe (List A)
dropPrefix xs ys =
  case isPrefixOf xs ys of λ where
    (yes (tl , _)) → just tl
    (no _)         → nothing

commonPrefix : ⦃ Eq A ⦄ → (xs ys : List A) → ∃ zs , IsPrefixOf zs xs × IsPrefixOf zs ys
commonPrefix [] ys = [] , (_ , refl) , (_ , refl)
commonPrefix xs [] = [] , (_ , refl) , (_ , refl)
commonPrefix (x ∷ xs) (y ∷ ys) with y == x | commonPrefix xs ys
... | yes y=x | zs , (xs₁ , eqx) , (ys₁ , eqy) = (x ∷ zs) , (xs₁ , (x ∷_ $≡ eqx)) , (ys₁ , (_∷_ $≡ y=x *≡ eqy))
... | no  _   | _                              = [] , (_ , refl) , (_ , refl)

commonPrefix! : ⦃ Eq A ⦄ → (xs ys : List A) → List A
commonPrefix! xs ys = fst (commonPrefix xs ys)

wordsBy : (A → Bool) → List A → List (List A)
wordsBy {A = A} p = go in-word ∘ dropWhile p
  where
    data Mode : Set where
      in-word in-space : Mode

    cons : A → List (List A) → List (List A)
    cons x []         = [ x ] ∷ []
    cons x (xs ∷ xss) = (x ∷ xs) ∷ xss

    go : Mode → List A → List (List A)
    go _    []       = []
    go mode     (x ∷ xs) with p x
    go mode     (x ∷ xs) | false = cons x (go in-word xs)
    go in-word  (x ∷ xs) | true  = [] ∷ go in-space xs
    go in-space (x ∷ xs) | true  = go in-space xs

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Product using (∃; _,_)

+-assoc : ∀ (m n p : ℕ) → m + (n + p) ≡ (m + n) + p
+-assoc zero n p =
  begin
    zero + (n + p)
  ≡⟨⟩
    n + p
  ≡⟨⟩
    (zero + n) + p
  ∎
+-assoc (suc m) n p =
  begin
    suc m + (n + p)
  ≡⟨⟩
    suc (m + (n + p))
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc ((m + n) + p)
  ≡⟨⟩
    (suc m + n) + p
  ∎

+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-identity zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identity (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identity m) ⟩
    suc m
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p =
  begin
    (zero + n) * p
  ≡⟨⟩
    n * p
  ≡⟨⟩
    zero * p + n * p
  ∎
*-distrib-+ (suc m) n p =
  begin
    (suc m + n) * p
  ≡⟨⟩
    p + (m + n) * p
  ≡⟨ cong (_+_ p) (*-distrib-+ m n p) ⟩
    p + (m * p + n * p)
  ≡⟨ +-assoc p (m * p) (n * p) ⟩
    (p + m * p) + n * p
  ≡⟨⟩
    suc m * p + n * p
  ∎

data even : ℕ → Set where
  ev0 : even zero
  ev+2 : ∀ {n : ℕ} → even n → even (suc (suc n))

lemma : ∀ (m : ℕ) → 2 * suc m ≡ suc (suc (2 * m))
lemma m =
  begin
    2 * suc m
  ≡⟨⟩
    suc m + (suc m + zero)
  ≡⟨⟩
    suc (m + (suc (m + zero)))
  ≡⟨ cong suc (+-suc m (m + zero)) ⟩
    suc (suc (m + (m + zero)))
  ≡⟨⟩
    suc (suc (2 * m))
  ∎

ev-ex : ∀ {n : ℕ} → even n → ∃(λ (m : ℕ) → 2 * m ≡ n)
ev-ex ev0 =  (0 , refl)
ev-ex (ev+2 ev) with ev-ex ev
... | (m , refl) = (suc m , lemma m)

ex-ev : ∀ {n : ℕ} → ∃(λ (m : ℕ) → 2 * m ≡ n) → even n
ex-ev (zero , refl) = ev0
ex-ev (suc m , refl) rewrite lemma m = ev+2 (ex-ev (m , refl))

-- I can't see how to avoid using rewrite in the second proof,
-- or how to use rewrite in the first proof!


text:
module ExportTestAgda where

open import Common.Prelude

itWorksText : String
itWorksText = "It works!"

{-# COMPILED_EXPORT itWorksText itWorksText #-}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- There was a bug when unifying things of function type during pattern matching
-- (the T argument to P is unified with D below)
module Issue199 where

data D (A : Set) : Set where

data P {A : Set} : {T : Set → Set} → T A → Set where
 p : ∀ d → P {_} {D} d

foo : ∀ {A} {l : D A} → P l → Set₁
foo (p _) = Set


text:
open import Type

module Relator.Converse {ℓ₁ ℓ₂} {T : Type{ℓ₁}} (_▫_ : T → T → Type{ℓ₂}) where

import      Lvl
open import Functional

Converse : T → T → Type{ℓ₂}
Converse = swap(_▫_)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Issue4954 where

open import Issue4954.M Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda