text:
import Level
open import Relation.Binary
  using (Decidable ; Rel ; IsStrictTotalOrder ; Tri)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; sym ; module ≡-Reasoning ; inspect ; subst)
open import Data.Nat as Nat
  using (ℕ ; suc ; zero ; _≤′_ ; _≤_ ; _+_ ; s≤s ; z≤n ; ≤′-refl ;
         ≤′-step)
open import Data.Nat.Properties as NatP
  using (≤⇒≤′ ; ≤′⇒≤ ;  m≤m+n ; s≤′s)
open import Data.Nat.Properties.Simple as NatPS
  using (+-comm ; +-suc)
open import Data.Product using (∃)

open import Relation.Nullary using (¬_ ; Dec ; yes ; no)
import Relation.Unary as U

open import Data.MoreNatProp

module Data.OrderedListMap
  (Key : Set)
  (inject : Key → ℕ)
  (Value : Set)
  where

open import utility

open import Data.Maybe using (just ; nothing ; Maybe)

open import Function
  using (_∘_ ; _∋_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _++_ ; [_] ; [] ; _∷_ ; map)
open import Data.List.All as All
  using (All)

open import Data.Product
  using (Σ ; Σ-syntax ; _,_ ; proj₁ ; proj₂ ; _×_ ; _,′_ ; ∃-syntax)
open import Data.Sum
  using (inj₁ ; inj₂ ; _⊎_)
open import Data.Unit
  using (⊤ ; tt)
open import Relation.Nullary
  using (yes ; no ; ¬_)
open import Data.List.Any using (here ; there)
open import Data.List.Any.Properties using (∷↔ ; ⊥↔Any[])
  renaming ( ++⁺ˡ  to ++ˡ ; ++⁺ʳ to ++ʳ )
open import Function using (_∘_)
open import Function.Inverse using (_↔_ ; Inverse)
open import Function.Equality using (Π)

open import Data.Bool using (Bool ; true ; false)

infix 6 _U_

LMap : Set
LMap = List (Maybe Value)

m-insert : Maybe Value → ℕ → LMap → LMap
m-insert v zero [] = [ v ]
m-insert nothing zero (x ∷ l) = x ∷ l
m-insert (just v) zero (x ∷ l) = (just v) ∷ l
m-insert v (suc n) [] = nothing ∷ (m-insert v n [])
m-insert v (suc n) (x ∷ l) = x ∷ (m-insert v n l)

insert : Key → Value → LMap → LMap
insert k v l = m-insert (just v) (inject k) l

Dom' : LMap → List ℕ
Dom' [] = []
Dom' ((just _) ∷ l) = 0 ∷ (map suc (Dom' l))
Dom' (nothing ∷ l) = (map suc (Dom' l))

_U_ : LMap → LMap → LMap
[] U m2 = m2
(x ∷ m1) U [] = (x ∷ m1)
(just x ∷ m1) U (just x₁ ∷ m2) = just x₁ ∷ (m1 U m2)
(just x ∷ m1) U (nothing ∷ m2) = just x ∷ (m1 U m2)
(nothing ∷ m1) U (just x ∷ m2) = just x ∷ (m1 U m2)
(nothing ∷ m1) U (nothing ∷ m2) = nothing ∷ (m1 U m2)

dist'::b : ∀{V1 V2 S1 S2} → (distinct'{ℕ} (S1 ∷ V1) (S2 ∷ V2)) → (distinct' V1 V2)
dist'::b d = dist'-sym (dist':: (dist'-sym (dist':: d)))

dist-cons : ∀{k k' l l'} → distinct'{ℕ} (k ∷ l) (k' ∷ l') → ¬ k ≡ k'
dist-cons {k} d refl = d k (here refl) (here refl)

data dist-dom : LMap → LMap → Set where
  el : ∀{l} → dist-dom [] l
  le : ∀{l} → dist-dom l []
  cl : ∀{l1 l2 v} → dist-dom l1 l2 → dist-dom (nothing ∷ l1) ((just v) ∷ l2)
  lc : ∀{l1 l2 v} → dist-dom l1 l2 → dist-dom ((just v) ∷ l1) (nothing ∷ l2)
  nn : ∀{l1 l2} → dist-dom l1 l2 → dist-dom (nothing ∷ l1) (nothing ∷ l2)

∈→⊥ : ∀{A} {z : A} → z ∈ [] → ⊥
∈→⊥{A}{z} ()

-- Π._⟨$⟩_ (Inverse.from (⊥↔Any[]{A = A}{P = _≡_ z})) x

dist-b : ∀{l l' x} → distinct' (x ∷ l) (x ∷ l') → ⊥
dist-b{x = x} d with (dist-cons d)
... | relf = d x (here refl) (here refl)

sucin : ∀{z n} → z ∈ n → (suc z) ∈ (map suc n)
sucin {z} {.(_ ∷ _)} (here px) rewrite px = here refl
sucin {z} {.(_ ∷ _)} (there I) = (there (sucin I))

suc≡ : ∀{z w} → suc z ≡ suc w → z ≡ w
suc≡ refl = refl

sucout : ∀{z n} → (suc z) ∈ (map suc n) → z ∈ n
sucout {z} {[]} ()
sucout {z} {x ∷ n} (here px) rewrite suc≡ px = (here refl)
sucout {z} {x ∷ n} (there I) = (there (sucout I))

dist-map : ∀{m n} → distinct' (map suc m) (map suc n) → distinct' m n
dist-map {[]} {[]} d = λ z x x₁ → ∈→⊥ x
dist-map {[]} {x ∷ n} d = λ z x₁ x₂ →  ∈→⊥ x₁
dist-map {x ∷ m} {[]} d = λ z x₁ x₂ → ∈→⊥ x₂
dist-map {zero ∷ m} {zero ∷ n} d =  ⊥-elim (dist-b d)
dist-map {zero ∷ m} {suc y ∷ n} d z x x₁ = d (suc z) (sucin x) (sucin x₁)
dist-map {suc y ∷ m} {zero ∷ n} d z x x₁ = d (suc z) (sucin x) (sucin x₁)
dist-map {suc _ ∷ m} {suc y ∷ n} d z x x₁ = d (suc z) (sucin x) (sucin x₁)

dist-in : ∀{m1 m2 x y} → distinct' (Dom' (x ∷ m1)) (Dom' (y ∷ m2)) → distinct' (Dom' m1) (Dom' m2)
dist-in {[]} {[]} {x} {y} dd = λ z x₁ x₂ → ∈→⊥ x₁
dist-in {[]} {x ∷ m2} {x₁} {y} dd = λ z x₂ x₃ → ∈→⊥ x₂
dist-in {x ∷ m1} {[]} {x₁} {y} dd = λ z x₂ x₃ → ∈→⊥ x₃
dist-in {h₁ ∷ m1} {h₂ ∷ m2} {just x} {just x₁} dd = ⊥-elim (dist-b dd)
dist-in {h₁ ∷ m1} {h₂ ∷ m2} {just x} {nothing} dd = λ z x₁ x₂ → (dist'-sym (dist':: (dist'-sym dd))) _ (sucin x₁) (sucin x₂)
dist-in {h₁ ∷ m1} {h₂ ∷ m2} {nothing} {just x} dd = λ z x₁ x₂ → (dist':: dd) _ (sucin x₁) (sucin x₂)
dist-in {h₁ ∷ m1} {h₂ ∷ m2} {nothing} {nothing} dd = dist-map dd
-- ((Π._⟨$⟩_ (Inverse.to (∷↔ (_≡_ _)))) (inj₂ x₂))

dist-gen : ∀{m1 m2} → distinct' (Dom' m1) (Dom' m2) → dist-dom m1 m2
dist-gen {[]} {[]} dd = el
dist-gen {[]} {x ∷ m2} dd = el
dist-gen {x ∷ m1} {[]} dd = le
dist-gen {just x ∷ m1} {just x₁ ∷ m2} dd = ⊥-elim (dist-b dd)
dist-gen {just x ∷ m1} {nothing ∷ m2} dd = lc (dist-gen (dist-in{m1}{m2}{just x}{nothing} dd))
dist-gen {nothing ∷ m1} {just x ∷ m2} dd = cl (dist-gen (dist-in{m1}{m2}{nothing}{just x} dd))
dist-gen {nothing ∷ m1} {nothing ∷ m2} dd = nn (dist-gen (dist-in{m1}{m2}{nothing}{nothing} dd))

U-comm' : ∀{m1 m2} → dist-dom m1 m2 → (m1 U m2) ≡ (m2 U m1)
U-comm' {.[]} {[]} el = refl
U-comm' {.[]} {x ∷ m2} el = refl
U-comm' {[]} {.[]} le = refl
U-comm' {x ∷ m1} {.[]} le = refl
U-comm' {.(nothing ∷ _)} {.(just _ ∷ _)} (cl dd) rewrite U-comm' dd = refl
U-comm' {.(just _ ∷ _)} {.(nothing ∷ _)} (lc dd) rewrite U-comm' dd = refl
U-comm' {.(nothing ∷ _)} {.(nothing ∷ _)} (nn dd) rewrite U-comm' dd = refl

U-comm : ∀{m1 m2} → distinct' (Dom' m1) (Dom' m2) → (m1 U m2) ≡ (m2 U m1)
U-comm{m1}{m2} dd = U-comm'{m1}{m2} (dist-gen dd)

U-assoc' : ∀ m1 m2 m3 → m1 U (m2 U m3) ≡ (m1 U m2) U m3
U-assoc' [] m2 m3 = refl
U-assoc' (x ∷ m1) [] m3 = refl
U-assoc' (x ∷ m1) (x₁ ∷ m2) []
  rewrite U-comm {(x ∷ m1) U (x₁ ∷ m2)} {[]} (λ _ _ ()) = refl
U-assoc' (just x ∷ m1) (just x₁ ∷ m2) (just x₂ ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (just x ∷ m1) (just x₁ ∷ m2) (nothing ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (just x ∷ m1) (nothing ∷ m2) (just x₁ ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (just x ∷ m1) (nothing ∷ m2) (nothing ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (nothing ∷ m1) (just x ∷ m2) (just x₁ ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (nothing ∷ m1) (just x ∷ m2) (nothing ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (nothing ∷ m1) (nothing ∷ m2) (just x ∷ m3) rewrite U-assoc' m1 m2 m3 = refl
U-assoc' (nothing ∷ m1) (nothing ∷ m2) (nothing ∷ m3) rewrite U-assoc' m1 m2 m3 = refl

U-assoc : ∀ m1 m2 m3 → m1 U (m2 U m3) ≡ (m1 U m2) U m3
U-assoc m1 m2 m3 = U-assoc' m1 m2 m3

0∈S : ∀{l} → 0 ∈ (map suc l) → ⊥
0∈S {[]} ()
0∈S {x ∷ l} (here ())
0∈S {x ∷ l} (there p) = 0∈S p

n∈S : ∀{n x l} → suc n ∈ Dom' (x ∷ l) → n ∈ Dom' l
n∈S {n} {just x} {[]} (here ())
n∈S {n} {just x} {[]} (there ())
n∈S {n} {just x} {x₁ ∷ l} (here ())
n∈S {n} {just x} {x₁ ∷ l} (there p) = sucout p
n∈S {n} {nothing} {[]} ()
n∈S {n} {nothing} {x ∷ l} p = sucout p

n+1∈S : ∀ {n x m} → n ∈ (Dom' m) → (suc n) ∈ (Dom' (x ∷ m))
n+1∈S {n} {just x} {m} n∈ = there (sucin n∈)
n+1∈S {n} {nothing} {m} n∈ = sucin n∈

deref : (n : ℕ) → (l : LMap) → n ∈ (Dom' l) → Value
deref zero [] ()
deref zero (just x ∷ l) p = x
deref zero (nothing ∷ l) p = ⊥-elim (0∈S p)
deref (suc n) [] ()
deref (suc n) (x ∷ l) p = deref n l (n∈S{n}{x}{l} p)

-- thrms
deref-∈-irr : ∀{k l} → (∈1 : k ∈ (Dom' l)) →  (∈2 : k ∈ (Dom' l)) → deref k l ∈1 ≡ deref k l ∈2
deref-∈-irr {zero} {[]} () ∈2
deref-∈-irr {suc k} {[]} () ∈2
deref-∈-irr {zero} {just x ∷ l} ∈1 ∈2 = refl
deref-∈-irr {zero} {nothing ∷ l} ∈1 ∈2 = ⊥-elim (0∈S ∈1)
deref-∈-irr {suc k} {x ∷ l} ∈1 ∈2 = deref-∈-irr (n∈S{k}{x}{l} ∈1) (n∈S{k}{x}{l} ∈2)

insert-mono' : ∀{l d l' d' n n' v} → n ∈ d → d ≡ (Dom' l) → d' ≡ (Dom' l') → l' ≡ (m-insert (just v) n' l) → n ∈ d'
insert-mono' {[]} {.[]} {[]} {.[]} {zero} {zero} () refl refl l'eq
insert-mono' {[]} {.[]} {[]} {.[]} {zero} {suc n'} () refl refl l'eq
insert-mono' {[]} {.[]} {[]} {.[]} {suc n} {zero} () refl refl l'eq
insert-mono' {[]} {.[]} {[]} {.[]} {suc n} {suc n'} () refl refl l'eq
insert-mono' {[]} {.[]} {x ∷ l'} {.(Dom' (x ∷ l'))} {zero} {zero} () refl refl l'eq
insert-mono' {[]} {.[]} {x ∷ l'} {.(Dom' (x ∷ l'))} {zero} {suc n'} () refl refl l'eq
insert-mono' {[]} {.[]} {x ∷ l'} {.(Dom' (x ∷ l'))} {suc n} {zero} () refl refl l'eq
insert-mono' {[]} {.[]} {x ∷ l'} {.(Dom' (x ∷ l'))} {suc n} {suc n'} () refl refl l'eq
insert-mono' {x ∷ l} {.(Dom' (x ∷ l))} {[]} {.[]} {zero} {zero} n∈ refl refl ()
insert-mono' {x ∷ l} {.(Dom' (x ∷ l))} {[]} {.[]} {zero} {suc n'} n∈ refl refl ()
insert-mono' {x ∷ l} {.(Dom' (x ∷ l))} {[]} {.[]} {suc n} {zero} n∈ refl refl ()
insert-mono' {x ∷ l} {.(Dom' (x ∷ l))} {[]} {.[]} {suc n} {suc n'} n∈ refl refl ()
insert-mono' {just x₁ ∷ l} {.(0 ∷ map suc (Dom' l))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {zero} {zero} {v} N∈ refl refl l'eq = here refl
insert-mono' {just x₁ ∷ l} {.(0 ∷ map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {zero} {zero} {v} N∈ refl refl ()
insert-mono' {nothing ∷ .l'} {.(map suc (Dom' l'))} {.(just _) ∷ l'} {.(0 ∷ map suc (Dom' l'))} {zero} {zero} n∈ refl refl refl = here refl
insert-mono' {just x₁ ∷ l} {.(0 ∷ map suc (Dom' l))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {zero} {suc n'} n∈ refl refl l'eq = here refl
insert-mono' {nothing ∷ l} {.(map suc (Dom' l))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {zero} {suc n'} n∈ refl refl l'eq = here refl
insert-mono' {just x₁ ∷ .l'} {.(0 ∷ map suc (Dom' l'))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {suc n} {zero} (here ()) refl refl refl
insert-mono' {just x₁ ∷ .l'} {.(0 ∷ map suc (Dom' l'))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {suc n} {zero} (there n∈) refl refl refl
    = there n∈
insert-mono' {nothing ∷ .l'} {.(map suc (Dom' l'))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {suc n} {zero} n∈ refl refl refl = there n∈
insert-mono' {just x ∷ l} {.(0 ∷ map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {suc n} {zero} n∈ refl refl ()
insert-mono' {nothing ∷ l} {.(map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {suc n} {zero} n∈ refl refl ()
insert-mono' {just x₁ ∷ l} {.(0 ∷ map suc (Dom' l))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {suc n} {suc n'} (here ()) refl refl l'eq
insert-mono' {just x₁ ∷ l} {.(0 ∷ map suc (Dom' l))} {just .x₁ ∷ .(m-insert (just _) n' l)} {.(0 ∷ map suc (Dom' (m-insert (just _) n' l)))} {suc n} {suc n'} {v} (there n∈) refl refl refl
  = there (sucin (insert-mono'{l = l}{l' = (m-insert (just _) n' l)}{n = n}{n' = n'}{v} (sucout n∈) refl refl refl))
insert-mono' {just x ∷ l} {.(0 ∷ map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {suc n} {suc n'} (here ()) refl refl l'eq
insert-mono' {just x ∷ l} {.(0 ∷ map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {suc n} {suc n'} {v} (there n∈) refl refl ()
insert-mono' {nothing ∷ l} {.(map suc (Dom' l))} {just x ∷ l'} {.(0 ∷ map suc (Dom' l'))} {suc n} {suc n'} n∈ refl refl ()
insert-mono' {nothing ∷ l} {.(map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {suc n} {suc n'} {v} n∈ refl refl refl
  =  sucin (insert-mono'{l = l}{l' = l'}{n = n}{n' = n'}{v = v} (sucout n∈) refl refl refl)
insert-mono' {just x ∷ l} {.(0 ∷ map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {zero} {suc n'} n∈ refl refl ()
insert-mono' {nothing ∷ l} {.(map suc (Dom' l))} {nothing ∷ l'} {.(map suc (Dom' l'))} {zero} {suc n'} n∈ refl refl l'eq = ⊥-elim (0∈S n∈)

insert-mono : ∀{m n n' v} → n ∈ (Dom' m) → n ∈ (Dom' (m-insert (just v) n' m))
insert-mono{m}{n}{n'}{v} i = insert-mono'{m}{Dom' m}{(m-insert (just v) n' m)}{(Dom' (m-insert (just v) n' m))}{n}{n'}{v} i refl refl refl

U-mono : ∀{m m' n} → n ∈ (Dom' m) → n ∈ (Dom' (m U m'))
U-mono {[]} {m'} {n} ()
U-mono {just x ∷ m} {[]} {n} (here px) = here px
U-mono {just x ∷ m} {just x₁ ∷ m'} {n} (here px) = here px
U-mono {just x ∷ m} {nothing ∷ m'} {n} (here px) = here px
U-mono {just x ∷ m} {[]} {n} (there ∈) = there ∈
U-mono {just x ∷ m} {just x₁ ∷ m'} {zero} (there ∈) = here refl
U-mono {just x ∷ m} {nothing ∷ m'} {zero} (there ∈) = here refl
U-mono {just x ∷ m} {just x₁ ∷ m'} {suc n} (there ∈) = there (sucin (U-mono{m}{m'}{n} (sucout ∈)))
U-mono {just x ∷ m} {nothing ∷ m'} {suc n} (there ∈) = there (sucin (U-mono{m}{m'}{n} (sucout ∈)))
U-mono {nothing ∷ m} {[]} {n} ∈ = ∈
U-mono {nothing ∷ m} {just x ∷ m'} {zero} ∈ = here refl
U-mono {nothing ∷ m} {just x ∷ m'} {suc n} ∈ = there (sucin (U-mono{m}{m'}{n} (sucout ∈)))
U-mono {nothing ∷ m} {nothing ∷ m'} {zero} ∈ = ⊥-elim (0∈S ∈)
U-mono {nothing ∷ m} {nothing ∷ m'} {suc n} ∈ = (sucin (U-mono{m}{m'}{n} (sucout ∈)))

U⁻ : ∀ {m m' n} → n ∈ Dom' (m U m') → (n ∈ Dom' m) ⊎ (n ∈ Dom' m')
U⁻ {[]} {[]} {n} n∈Dom⟨mUm'⟩ = inj₁ n∈Dom⟨mUm'⟩
U⁻ {[]} {x ∷ m'} {n} n∈Dom⟨mUm'⟩ = inj₂ n∈Dom⟨mUm'⟩
U⁻ {x ∷ m} {[]} {n} n∈Dom⟨mUm'⟩ = inj₁ n∈Dom⟨mUm'⟩
U⁻ {just x ∷ m} {just x₁ ∷ m'} {zero} n∈Dom⟨mUm'⟩ = inj₁ (here refl)
U⁻ {just x ∷ m} {just x₁ ∷ m'} {suc n} (here ())
U⁻ {just x ∷ m} {just x₁ ∷ m'} {suc n} (there n∈Dom⟨mUm'⟩) with U⁻ {m} {m'} {n} (sucout n∈Dom⟨mUm'⟩)
... | inj₁ ∈Dom-m  = inj₁ (there (sucin ∈Dom-m))
... | inj₂ ∈Dom-m' = inj₂ (there (sucin ∈Dom-m'))
U⁻ {just x ∷ m} {nothing ∷ m'} {zero} n∈Dom⟨mUm'⟩ = inj₁ (here refl)
U⁻ {just x ∷ m} {nothing ∷ m'} {suc n} (here ())
U⁻ {just x ∷ m} {nothing ∷ m'} {suc n} (there n∈Dom⟨mUm'⟩) with U⁻ {m} {m'} {n} (sucout n∈Dom⟨mUm'⟩)
... | inj₁ ∈Dom-m  = inj₁ (there (sucin ∈Dom-m))
... | inj₂ ∈Dom-m' = inj₂ (sucin ∈Dom-m')
U⁻ {nothing ∷ m} {just x ∷ m'} {zero} n∈Dom⟨mUm'⟩ = inj₂ (here refl)
U⁻ {nothing ∷ m} {just x ∷ m'} {suc n} (here ())
U⁻ {nothing ∷ m} {just x ∷ m'} {suc n} (there n∈Dom⟨mUm'⟩) with U⁻ {m} {m'} {n} (sucout n∈Dom⟨mUm'⟩)
... | inj₁ ∈Dom-m  = inj₁ (sucin ∈Dom-m)
... | inj₂ ∈Dom-m' = inj₂ (there (sucin ∈Dom-m'))
U⁻ {nothing ∷ m} {nothing ∷ m'} {zero} n∈Dom⟨mUm'⟩ = ⊥-elim (0∈S n∈Dom⟨mUm'⟩)
U⁻ {nothing ∷ m} {nothing ∷ m'} {suc n} n∈Dom⟨mUm'⟩ with U⁻ {m} {m'} {n} (sucout n∈Dom⟨mUm'⟩)
... | inj₁ ∈Dom-m  = inj₁ (sucin ∈Dom-m)
... | inj₂ ∈Dom-m' = inj₂ (sucin ∈Dom-m')

Dom'-1map : ∀ n v → Dom' (m-insert (just v) n []) ≡ (n ∷ [])
Dom'-1map zero v = refl
Dom'-1map (suc n) v rewrite Dom'-1map n v = refl

Dom'-2map : ∀ n₁ v₁ n₂ v₂ →
  (Dom' (m-insert (just v₂) n₂ (m-insert (just v₁) n₁ [])) ≡ n₁ ∷ [] × n₁ ≡ n₂) ⊎
  (Dom' (m-insert (just v₂) n₂ (m-insert (just v₁) n₁ [])) ≡ n₁ ∷ n₂ ∷ []) ⊎
  (Dom' (m-insert (just v₂) n₂ (m-insert (just v₁) n₁ [])) ≡ n₂ ∷ n₁ ∷ [])
Dom'-2map zero v₁ zero v₂ = inj₁ (refl , refl)
Dom'-2map zero v₁ (suc n₂) v₂ rewrite Dom'-1map n₂ v₂ = inj₂ (inj₁ refl)
Dom'-2map (suc n₁) v₁ zero v₂ rewrite Dom'-1map n₁ v₁ = inj₂ (inj₂ refl)
Dom'-2map (suc n₁) v₁ (suc n₂) v₂ with Dom'-2map n₁ v₁ n₂ v₂
... | inj₁ (xs≡[n₁] , refl)  rewrite xs≡[n₁] = inj₁ (refl , refl)
... | inj₂ (inj₁ xs≡[n₁,n₂]) rewrite xs≡[n₁,n₂] = inj₂ (inj₁ refl)
... | inj₂ (inj₂ xs≡[n₂,n₁]) rewrite xs≡[n₂,n₁] = inj₂ (inj₂ refl)

negsucun : ∀{k k'} → ¬ (suc k ≡ suc k') → k ≡ k' → ⊥
negsucun neg = (λ eq → neg (cong suc eq))

-- sucout : ∀{z n} → (suc z) ∈ (map suc n) → z ∈ n
sucinout : ∀{k nn}
           → (kin : (suc k) ∈ (map suc nn))
           → sucin (sucout kin) ≡ kin
sucinout {zero} {[]} ()
sucinout {zero} {.0 ∷ nn₁} (here refl) = refl
sucinout {zero} {x ∷ nn₁} (there kin) rewrite (sucinout{zero}{nn₁} kin) = refl
sucinout {suc k} {[]} ()
sucinout {suc k} {.(suc k) ∷ nn₁} (here refl) = refl
sucinout {suc k} {x ∷ nn₁} (there kin) rewrite (sucinout{(suc k)}{nn₁} kin) = refl

domzero : ∀{m} → zero ∈ (Dom' (nothing ∷ m)) → ⊥
domzero {[]} = λ ()
domzero {x ∷ m} = 0∈S

domin : ∀{x m z} → x ∈ Dom' m → suc x ∈ Dom' (z ∷ m)
domin {x} {m} {just z}  x∈Dom'm = there (sucin x∈Dom'm)
domin {x} {m} {nothing} x∈Dom'm = sucin x∈Dom'm

n∈Sbij : ∀{k x m} → ∀{kin : (suc k) ∈ (Dom' (x ∷ m))} → ∀{kin2 : (suc k) ∈ (Dom' (x ∷ m))} → (n∈S{k}{x}{m} kin) ≡ (n∈S{k}{x}{m} kin2) → kin ≡ kin2
n∈Sbij {k} {just x} {[]} {here ()} {kin2} eq
n∈Sbij {k} {just x} {[]} {there ()} {kin2} eq
n∈Sbij {k} {just x} {x₁ ∷ m} {here ()} {kin2} eq
n∈Sbij {k} {just x} {x₁ ∷ m} {there kin} {here ()} eq
n∈Sbij {k} {just x} {x₁ ∷ m} {there kin} {there kin2} eq with (cong sucin eq)
... | eq2 rewrite (sucinout kin) | (sucinout kin2) =  cong there eq2
n∈Sbij {k} {nothing} {[]} {kin} {()} eq
n∈Sbij {k} {nothing} {x ∷ m} {kin} {kin2} eq with cong sucin eq
... | eq2 rewrite (sucinout kin) | (sucinout kin2) = eq2

ineq : ∀{k m} → (kin1 : k ∈ (Dom' m)) → (kin2 : k ∈ (Dom' m)) → kin1 ≡ kin2
ineq {zero} {[]} () kin2
ineq {zero} {just x ∷ m} (here refl) (here refl) = refl
ineq {zero} {just x ∷ m} (here refl) (there kin2) = ⊥-elim (0∈S kin2)
ineq {zero} {just x ∷ m} (there kin1) (here px) = ⊥-elim (0∈S kin1)
ineq {zero} {just x ∷ m} (there kin1) (there kin2) = ⊥-elim (0∈S kin1)
ineq {zero} {nothing ∷ m} kin1 kin2 = ⊥-elim (domzero{m} kin1)
ineq {suc k} {[]} () kin2
ineq {suc k} {just x ∷ m} (here ()) (here px₁)
ineq {suc k} {just x ∷ m} (here ()) (there kin2)
ineq {suc k} {just x ∷ m} (there kin1) (here ())
ineq {suc k} {just x ∷ m} (there kin1) (there kin2) rewrite sym (sucinout kin1) | sym (sucinout kin2) = cong there (cong sucin (ineq{k}{m} (sucout kin1) (sucout kin2)))
ineq {suc k} {nothing ∷ m} kin1 kin2 = n∈Sbij{k}{nothing}{m} (ineq{k}{m} (n∈S{x = nothing}{l = m} kin1) (n∈S{x = nothing}{l = m} kin2))

Dom'-comm : ∀ m1 m2 → Dom' (m1 U m2) ≡ Dom' (m2 U m1)
Dom'-comm [] m2 rewrite U-comm {m2} {[]} (λ _ _ ()) = refl
Dom'-comm (x ∷ m1) [] = refl
Dom'-comm (just x ∷ m1) (just x₁ ∷ m2) rewrite Dom'-comm m1 m2 = refl
Dom'-comm (just x ∷ m1) (nothing ∷ m2) rewrite Dom'-comm m1 m2 = refl
Dom'-comm (nothing ∷ m1) (just x ∷ m2) rewrite Dom'-comm m1 m2 = refl
Dom'-comm (nothing ∷ m1) (nothing ∷ m2) rewrite Dom'-comm m1 m2 = refl

Dom'-assoc-comm : ∀ m1 m2 m3 → Dom' ((m1 U m2) U m3) ≡ Dom' ((m1 U m3) U m2)
Dom'-assoc-comm [] m2 m3 = Dom'-comm m2 m3
Dom'-assoc-comm (x ∷ m1) [] m3 rewrite Dom'-comm ((x ∷ m1) U m3) [] = refl
Dom'-assoc-comm (x ∷ m1) (x₁ ∷ m2) [] rewrite Dom'-comm ((x ∷ m1) U (x₁ ∷ m2)) [] = refl
Dom'-assoc-comm (just x ∷ m1) (just x₁ ∷ m2) (just x₂ ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (just x ∷ m1) (just x₁ ∷ m2) (nothing ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (just x ∷ m1) (nothing ∷ m2) (just x₁ ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (just x ∷ m1) (nothing ∷ m2) (nothing ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (nothing ∷ m1) (just x ∷ m2) (just x₁ ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (nothing ∷ m1) (just x ∷ m2) (nothing ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (nothing ∷ m1) (nothing ∷ m2) (just x ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl
Dom'-assoc-comm (nothing ∷ m1) (nothing ∷ m2) (nothing ∷ m3)
  rewrite Dom'-assoc-comm m1 m2 m3 = refl

putputget-neq : ∀{k k' m v v'}
                → ¬ (k ≡ k')
                → (kin : k ∈ (Dom' m))
                → (kin2 : k ∈ (Dom' (m-insert (just v') k' m)))
                → (deref k m kin) ≡ v
                → (deref k (m-insert (just v') k' m) kin2) ≡ v
putputget-neq {k} {k'} {[]} neq () kin2 eq
putputget-neq {.0} {zero} {just x ∷ m} neq (here refl) (here refl) refl = ⊥-elim (neq refl)
putputget-neq {.0} {zero} {just x ∷ m} neq (here refl) (there kin2) refl = ⊥-elim (neq refl)
putputget-neq {.0} {suc k'} {just x ∷ m} neq (here refl) (here refl) refl = refl
putputget-neq {.0} {suc k'} {just x ∷ m} neq (here refl) (there kin2) refl = refl
putputget-neq {zero} {zero} {just x ∷ m} neq (there kin) kin2 refl = ⊥-elim (neq refl)

putputget-neq {zero} {suc k'} {just x ∷ m} neq (there kin) kin2 refl = refl
putputget-neq {suc k} {suc k'} {just x ∷ m} neq (there kin) (here ()) refl
putputget-neq {zero} {zero} {nothing ∷ m} neq kin kin2 refl = ⊥-elim (neq refl)

putputget-neq {zero} {suc k'} {nothing ∷ m} neq kin kin2 refl = ⊥-elim (0∈S kin)
putputget-neq {suc k} {zero} {nothing ∷ m} neq kin (here ()) refl

putputget-neq {suc k} {suc k'} {just x ∷ m} {v} {v'} neq (there kin) (there kin2) refl
  rewrite ineq{k}{m-insert (just v') k' m} (n∈S{k}{just x}{m-insert (just v') k' m} (there kin2)) (sucout kin2)
     =  putputget-neq{k}{k'}{m}{v}{v'} (negsucun neq) (sucout kin) (sucout kin2) (deref-∈-irr{k}{m} (sucout kin) (n∈S{k}{x = just x}{m} (there kin)))
putputget-neq {suc k} {suc k'} {nothing ∷ m} {v} {v'} neq kin kin2 refl
  rewrite ineq{k}{m-insert (just v') k' m} (n∈S{k}{nothing}{m-insert (just v') k' m} kin2) (sucout kin2)
    = putputget-neq{k}{k'}{m} (negsucun neq) (sucout kin) ((sucout kin2)) ((deref-∈-irr{k}{m} (sucout kin) (n∈S{k}{x = nothing}{m} kin)))

putputget-neq {suc k} {zero} {x ∷ m} {v} {v'} neq kin kin2 refl =  deref-∈-irr{k}{m} (n∈S{k}{just v'}{m} kin2) (n∈S{k}{x}{m} kin)

putputget-eq : ∀ k m v v' →
               (m-insert (just v') k (m-insert (just v) k m))
                ≡ (m-insert (just v') k m)
putputget-eq zero [] v v' = refl
putputget-eq zero (x ∷ m) v v' = refl
putputget-eq (suc k) [] v v' rewrite putputget-eq k [] v v' = refl
putputget-eq (suc k) (x ∷ m) v v'  rewrite putputget-eq k m v v' = refl

getput : ∀ k m →
  (kin : k ∈ Dom' m) →
  m ≡ m-insert (just (deref k m kin)) k m
getput k [] ()
getput zero    (just x ∷ m)  kin = refl
getput zero    (nothing ∷ m) kin = ⊥-elim (0∈S kin)
getput (suc k) (just x ∷ m)  kin
  rewrite sym (getput k m (n∈S {k} {just x} {m} kin))
  = refl
getput (suc k) (nothing ∷ m) kin
  rewrite sym (getput k m (n∈S {k} {nothing} {m} kin))
  = refl

putget : ∀{k m v} → (kin : k ∈ (Dom' (m-insert (just v) k m))) → (deref k (m-insert (just v) k m) kin) ≡ v
putget {zero} {[]} {v} (here refl) = refl
putget {zero} {[]} {v} (there ())
putget {zero} {just x ∷ m} {v} (here refl) = refl
putget {zero} {just x ∷ m} {v} (there kin) = refl
putget {zero} {nothing ∷ m} {v} kin = refl
putget {suc k} {[]} {v} kin = putget{k}{[]}{v} ( (n∈S{k}{nothing}{(m-insert (just v) k [])} kin) )
putget {suc k} {x ∷ m} {v} kin = putget{k}{m}{v} ( (n∈S{k}{x} kin) )

put-U-U : ∀ k v m1 m2 →
  (kin1 : k ∈ Dom' m1) →
  (kin2 : k ∈ Dom' m2) →
    m1 U m2 ≡
    (m-insert (just v) k m1) U m2
put-U-U k v [] m2 () kin2
put-U-U k v (x ∷ m1) [] kin1 ()
put-U-U zero v (just x ∷ m1) (just x₁ ∷ m2) kin1 kin2 = refl
put-U-U zero v (just x ∷ m1) (nothing ∷ m2) kin1 kin2 = ⊥-elim (0∈S kin2)
put-U-U zero v (nothing ∷ m1) (x₁ ∷ m2) kin1 kin2 = ⊥-elim (0∈S kin1)
put-U-U (suc k) v (just x ∷ m1) (just x₁ ∷ m2) kin1 kin2
  rewrite put-U-U k v m1 m2
                  (n∈S {k} {just x}  {m1} kin1)
                  (n∈S {k} {just x₁} {m2} kin2)
  = refl
put-U-U (suc k) v (just x ∷ m1) (nothing ∷ m2) kin1 kin2
  rewrite put-U-U k v m1 m2
                  (n∈S {k} {just x}  {m1} kin1)
                  (n∈S {k} {nothing} {m2} kin2)
  = refl
put-U-U (suc k) v (nothing ∷ m1) (just x ∷ m2) kin1 kin2
  rewrite put-U-U k v m1 m2
                  (n∈S {k} {nothing} {m1} kin1)
                  (n∈S {k} {just x}  {m2} kin2)
  = refl
put-U-U (suc k) v (nothing ∷ m1) (nothing ∷ m2) kin1 kin2
  rewrite put-U-U k v m1 m2
                  (n∈S {k} {nothing} {m1} kin1)
                  (n∈S {k} {nothing} {m2} kin2)
  = refl

insert-comm : ∀{m k1 k2 v1 v2}
              → ¬ k1 ≡ k2
              → (m-insert (just v2) k2 (m-insert (just v1) k1 m)) ≡ (m-insert (just v1) k1 (m-insert (just v2) k2 m))
insert-comm {m} {zero} {zero} {v1} {v2} ¬k1≡k2 = ⊥-elim (¬k1≡k2 refl)
insert-comm {[]} {zero} {suc k2} {v1} {v2} ¬k1≡k2 = refl
insert-comm {x ∷ m} {zero} {suc k2} {v1} {v2} ¬k1≡k2 = refl
insert-comm {[]} {suc k1} {zero} {v1} {v2} ¬k1≡k2 = refl
insert-comm {x ∷ m} {suc k1} {zero} {v1} {v2} ¬k1≡k2 = refl
insert-comm {[]} {suc k1} {suc k2} {v1} {v2} ¬k1≡k2 rewrite insert-comm{[]}{k1}{k2}{v1}{v2} (λ x → ¬k1≡k2 (cong suc x)) = refl
insert-comm {x ∷ m} {suc k1} {suc k2} {v1} {v2} ¬k1≡k2 rewrite insert-comm{m}{k1}{k2}{v1}{v2} (λ x → ¬k1≡k2 (cong suc x)) = refl

insert-U-comm : ∀ k v m m' →
  ¬ (k ∈ Dom' m') →
    (m-insert (just v) k m) U m' ≡
    m-insert (just v) k (m U m')
insert-U-comm k v m [] k∉Domm'
  rewrite U-comm {m} {[]} (λ _ _ ())
        | U-comm {m-insert (just v) k m} {[]} (λ _ _ ())
  = refl
insert-U-comm zero v [] (just x ∷ m') k∉Domm' = ⊥-elim (k∉Domm' (here refl))
insert-U-comm zero v [] (nothing ∷ m') k∉Domm' = refl
insert-U-comm (suc k) v [] (just x ∷ m') k∉Domm'
  rewrite insert-U-comm k v [] m' (k∉Domm' ∘ there ∘ sucin {k} {Dom' m'})
  = refl
insert-U-comm (suc k) v [] (nothing ∷ m') k∉Domm'
  rewrite insert-U-comm k v [] m' (k∉Domm' ∘ sucin {k} {Dom' m'})
  = refl
insert-U-comm zero v (x ∷ m) (just x₁ ∷ m') k∉Domm' = ⊥-elim (k∉Domm' (here refl))
insert-U-comm zero v (just x ∷ m)  (nothing ∷ m') k∉Domm' = refl
insert-U-comm zero v (nothing ∷ m) (nothing ∷ m') k∉Domm' = refl
insert-U-comm (suc k) v (just x ∷ m)  (just x₁ ∷ m') k∉Domm'
  rewrite insert-U-comm k v m m' (k∉Domm' ∘ there ∘ sucin {k} {Dom' m'})
  = refl
insert-U-comm (suc k) v (nothing ∷ m) (just x₁ ∷ m') k∉Domm'
  rewrite insert-U-comm k v m m' (k∉Domm' ∘ there ∘ sucin {k} {Dom' m'})
  = refl
insert-U-comm (suc k) v (just x ∷ m)  (nothing ∷ m') k∉Domm'
  rewrite insert-U-comm k v m m' (k∉Domm' ∘ sucin {k} {Dom' m'})
  = refl
insert-U-comm (suc k) v (nothing ∷ m) (nothing ∷ m') k∉Domm'
  rewrite insert-U-comm k v m m' (k∉Domm' ∘ sucin {k} {Dom' m'})
  = refl

deref-U-right-irr : ∀ k m1 m2 kin12 kin2 →
  deref k (m1 U m2) kin12 ≡ deref k m2 kin2
deref-U-right-irr k m1 [] kin12 ()
deref-U-right-irr zero [] (x ∷ m2) kin12 kin2 = deref-∈-irr {l = x ∷ m2} kin12 kin2
deref-U-right-irr zero (just x ∷ m1)  (just x₁ ∷ m2) kin12 kin2 = refl
deref-U-right-irr zero (nothing ∷ m1) (just x ∷ m2)  kin12 kin2 = refl
deref-U-right-irr zero (x ∷ m1)       (nothing ∷ m2) kin12 kin2 = ⊥-elim (0∈S kin2)
deref-U-right-irr (suc k) [] (x ∷ m2) kin12 kin2 =
  deref-∈-irr {l = m2} (n∈S {k} {x} kin12) (n∈S {k} {x} kin2)
deref-U-right-irr (suc k) (just x ∷ m1)  (just x₁ ∷ m2) kin12 kin2 =
  deref-U-right-irr k m1 m2
    (n∈S {k} {just x₁} {m1 U m2} kin12) (n∈S {k} {just x₁} {m2} kin2)
deref-U-right-irr (suc k) (nothing ∷ m1) (just x₁ ∷ m2) kin12 kin2 =
  deref-U-right-irr k m1 m2
    (n∈S {k} {just x₁} {m1 U m2} kin12) (n∈S {k} {just x₁} {m2} kin2)
deref-U-right-irr (suc k) (just x ∷ m1)  (nothing ∷ m2) kin12 kin2 =
  deref-U-right-irr k m1 m2
    (n∈S {k} {just x} {m1 U m2} kin12) (n∈S {k} {nothing} {m2} kin2)
deref-U-right-irr (suc k) (nothing ∷ m1) (nothing ∷ m2) kin12 kin2 =
  deref-U-right-irr k m1 m2
    (n∈S {k} {nothing} {m1 U m2} kin12) (n∈S {k} {nothing} {m2} kin2)

∈-deref-U-irr : ∀ k m1 m2 m3 kin1 kin2 →
  (kin3 : k ∈ Dom' m3) →
  deref k (m1 U m3) kin1 ≡ deref k (m2 U m3) kin2
∈-deref-U-irr k [] m2 m3 kin1 kin2 kin3
  rewrite deref-U-right-irr k m2 m3 kin2 kin3
  = deref-∈-irr kin1 kin3
∈-deref-U-irr k (x ∷ m1) [] m3 kin1 kin2 kin3
  rewrite deref-U-right-irr k (x ∷ m1) m3 kin1 kin3
  = deref-∈-irr kin3 kin2
∈-deref-U-irr k (x ∷ m1) (x₁ ∷ m2) [] kin1 kin2 ()
∈-deref-U-irr zero (x ∷ m1) (x₁ ∷ m2) (nothing ∷ m3) kin1 kin2 kin3 = ⊥-elim (0∈S kin3)
∈-deref-U-irr zero (just x ∷ m1)  (just x₁ ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 = refl
∈-deref-U-irr zero (just x ∷ m1)  (nothing ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 = refl
∈-deref-U-irr zero (nothing ∷ m1) (just x₁ ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 = refl
∈-deref-U-irr zero (nothing ∷ m1) (nothing ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 = refl
∈-deref-U-irr (suc k) (just x ∷ m1) (just x₁ ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {just x₂} {m1 U m3} kin1)
    (n∈S {k} {just x₂} {m2 U m3} kin2)
    (n∈S {k} {just x₂} {m3} kin3)
∈-deref-U-irr (suc k) (just x ∷ m1) (nothing ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {just x₂} {m1 U m3} kin1)
    (n∈S {k} {just x₂} {m2 U m3} kin2)
    (n∈S {k} {just x₂} {m3} kin3)
∈-deref-U-irr (suc k) (nothing ∷ m1) (just x₁ ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {just x₂} {m1 U m3} kin1)
    (n∈S {k} {just x₂} {m2 U m3} kin2)
    (n∈S {k} {just x₂} {m3} kin3)
∈-deref-U-irr (suc k) (nothing ∷ m1) (nothing ∷ m2) (just x₂ ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {just x₂} {m1 U m3} kin1)
    (n∈S {k} {just x₂} {m2 U m3} kin2)
    (n∈S {k} {just x₂} {m3} kin3)
∈-deref-U-irr (suc k) (just x ∷ m1) (just x₁ ∷ m2) (nothing ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {just x} {m1 U m3} kin1)
    (n∈S {k} {just x₁} {m2 U m3} kin2)
    (n∈S {k} {nothing} {m3} kin3)
∈-deref-U-irr (suc k) (just x ∷ m1) (nothing ∷ m2) (nothing ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {just x} {m1 U m3} kin1)
    (n∈S {k} {nothing} {m2 U m3} kin2)
    (n∈S {k} {nothing} {m3} kin3)
∈-deref-U-irr (suc k) (nothing ∷ m1) (just x₁ ∷ m2) (nothing ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {nothing} {m1 U m3} kin1)
    (n∈S {k} {just x₁} {m2 U m3} kin2)
    (n∈S {k} {nothing} {m3} kin3)
∈-deref-U-irr (suc k) (nothing ∷ m1) (nothing ∷ m2) (nothing ∷ m3) kin1 kin2 kin3 =
  ∈-deref-U-irr k m1 m2 m3
    (n∈S {k} {nothing} {m1 U m3} kin1)
    (n∈S {k} {nothing} {m2 U m3} kin2)
    (n∈S {k} {nothing} {m3} kin3)

deref-U-both-irr : ∀ k m1 m2 m3 kin1 kin2 kin13 kin23 →
  deref k m1 kin1 ≡ deref k m2 kin2 →
  deref k (m1 U m3) kin13 ≡ deref k (m2 U m3) kin23
deref-U-both-irr k [] m2 m3 () kin2 kin13 kin23 m1[k]≡m2[k]
deref-U-both-irr k (x ∷ m1) [] m3 kin1 () kin13 kin23 m1[k]≡m2[k]
deref-U-both-irr k (x ∷ m1) (x₁ ∷ m2) [] kin1 kin2 kin13 kin23 m1[k]≡m2[k]
  rewrite deref-∈-irr {l = x ∷ m1} kin13 kin1 | deref-∈-irr {l = x₁ ∷ m2} kin23 kin2
  = m1[k]≡m2[k]
deref-U-both-irr zero (just x ∷ m1)  (just x₁ ∷ m2) (nothing ∷ m3) _ _ _ _ m1[k]≡m2[k] = m1[k]≡m2[k]
deref-U-both-irr zero (just x ∷ m1)  (just x₁ ∷ m2) (just x₂ ∷ m3) _    _ _ _ _ = refl
deref-U-both-irr zero (just x ∷ m1)  (nothing ∷ m2) (just x₂ ∷ m3) _    _ _ _ _ = refl
deref-U-both-irr zero (nothing ∷ m1) (just x ∷ m2)  (just x₂ ∷ m3) _    _ _ _ _ = refl
deref-U-both-irr zero (nothing ∷ m1) (nothing ∷ m2) (just x₂ ∷ m3) _    _ _ _ _ = refl
deref-U-both-irr zero (nothing ∷ m1) (just x ∷ m2)  (nothing ∷ m3) kin1 _ _ _ _ = ⊥-elim (0∈S kin1)
deref-U-both-irr zero (nothing ∷ m1) (nothing ∷ m2) (nothing ∷ m3) kin1 _ _ _ _ = ⊥-elim (0∈S kin1)
deref-U-both-irr zero (just x ∷ m1)  (nothing ∷ m2) (nothing ∷ m3) _ kin2 _ _ _ = ⊥-elim (0∈S kin2)
deref-U-both-irr (suc k) (just x ∷ m1) (just x₁ ∷ m2) (just x₂ ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {just x} {m1} kin1) (n∈S {k} {just x₁} {m2} kin2)
    (n∈S {k} {just x₂} {m1 U m3} kin13) (n∈S {k} {just x₂} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (just x ∷ m1) (nothing ∷ m2) (just x₂ ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {just x} {m1} kin1) (n∈S {k} {nothing} {m2} kin2)
    (n∈S {k} {just x₂} {m1 U m3} kin13) (n∈S {k} {just x₂} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (nothing ∷ m1) (just x ∷ m2) (just x₂ ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {nothing} {m1} kin1) (n∈S {k} {just x} {m2} kin2)
    (n∈S {k} {just x₂} {m1 U m3} kin13) (n∈S {k} {just x₂} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (nothing ∷ m1) (nothing ∷ m2) (just x₂ ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {nothing} {m1} kin1) (n∈S {k} {nothing} {m2} kin2)
    (n∈S {k} {just x₂} {m1 U m3} kin13) (n∈S {k} {just x₂} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (just x ∷ m1) (just x₁ ∷ m2) (nothing ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {just x} {m1} kin1) (n∈S {k} {just x₁} {m2} kin2)
    (n∈S {k} {just x} {m1 U m3} kin13) (n∈S {k} {just x₁} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (just x ∷ m1) (nothing ∷ m2) (nothing ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {just x} {m1} kin1) (n∈S {k} {nothing} {m2} kin2)
    (n∈S {k} {just x} {m1 U m3} kin13) (n∈S {k} {nothing} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (nothing ∷ m1) (just x ∷ m2) (nothing ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {nothing} {m1} kin1) (n∈S {k} {just x} {m2} kin2)
    (n∈S {k} {nothing} {m1 U m3} kin13) (n∈S {k} {just x} {m2 U m3} kin23)
    m1[k]≡m2[k]
deref-U-both-irr (suc k) (nothing ∷ m1) (nothing ∷ m2) (nothing ∷ m3)
               kin1 kin2 kin13 kin23 m1[k]≡m2[k] =
  deref-U-both-irr k m1 m2 m3
    (n∈S {k} {nothing} {m1} kin1) (n∈S {k} {nothing} {m2} kin2)
    (n∈S {k} {nothing} {m1 U m3} kin13) (n∈S {k} {nothing} {m2 U m3} kin23)
    m1[k]≡m2[k]

U-domout : ∀ {k m₁ m₂} x x₁ → suc k ∈ Dom' ((x ∷ m₁) U (x₁ ∷ m₂)) → k ∈ Dom' (m₁ U m₂)
U-domout (just x₂) (just x₃) (here ())
U-domout (just x₂) (just x₃) (there suck∈'') = sucout suck∈''
U-domout (just x₂) nothing (here ())
U-domout (just x₂) nothing (there suck∈'') = sucout suck∈''
U-domout nothing (just x₂) (here ())
U-domout nothing (just x₂) (there suck∈'') = sucout suck∈''
U-domout nothing   nothing   suck∈'' = sucout suck∈''

U-∉-irr-get-help-help : ∀ k x x₁ m₁ m₂ →
  (k∈ : suc k ∈ Dom' ((x ∷ m₁) U (x₁ ∷ m₂))) →
  deref (suc k) ((x ∷ m₁) U (x₁ ∷ m₂)) k∈ ≡
    deref k (m₁ U m₂) (U-domout x x₁ k∈)
U-∉-irr-get-help-help k (just x) (just x₁) m₁ m₂ (here ())
U-∉-irr-get-help-help k (just x) (just x₁) m₁ m₂ (there k∈) = deref-∈-irr {k} {m₁ U m₂} (n∈S {k} {just x₁} {m₁ U m₂} (there k∈)) (sucout k∈)
U-∉-irr-get-help-help k (just x) nothing m₁ m₂ (here ())
U-∉-irr-get-help-help k (just x) nothing m₁ m₂ (there k∈) = deref-∈-irr {k} {m₁ U m₂} (n∈S {k} {just x} {m₁ U m₂} (there k∈)) (sucout k∈)
U-∉-irr-get-help-help k nothing (just x) m₁ m₂ (here ())
U-∉-irr-get-help-help k nothing (just x) m₁ m₂ (there k∈) = deref-∈-irr {k} {m₁ U m₂} (n∈S {k} {just x} {m₁ U m₂} (there k∈)) (sucout k∈)
U-∉-irr-get-help-help k nothing nothing m₁ m₂ k∈ =  deref-∈-irr {k} {m₁ U m₂} (n∈S {k} {nothing} {m₁ U m₂} k∈) (sucout k∈)

U-∉-irr-get-help : ∀ {m₁ m₂ k} → (k∈ : k ∈ Dom' m₁) → k ∉ Dom' m₂ → (k∈' : k ∈ Dom' (m₁ U m₂))  → deref k m₁ k∈ ≡ deref k (m₁ U m₂) k∈'
U-∉-irr-get-help {[]} {[]} {k} () k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩
U-∉-irr-get-help {[]} {x ∷ m₂} {k} () k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩
U-∉-irr-get-help {x ∷ m₁} {[]}      {k} k∈Dom⟨m₁⟩ k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩
  rewrite deref-∈-irr {k} {x ∷ m₁} k∈Dom⟨m₁⟩ k∈Dom⟨m₁Um₂⟩ = refl
U-∉-irr-get-help {x ∷ m₁} {just x₁ ∷ m₂} {zero} k∈Dom⟨m₁⟩ k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩ = ⊥-elim (k∉Dom⟨m₂⟩ (here refl))
U-∉-irr-get-help {just x ∷ m₁}  {nothing ∷ m₂} {zero} k∈Dom⟨m₁⟩ k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩ = refl
U-∉-irr-get-help {nothing ∷ m₁} {nothing ∷ m₂} {zero} k∈Dom⟨m₁⟩ k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩ = ⊥-elim (0∈S k∈Dom⟨m₁⟩)
U-∉-irr-get-help {x ∷ m₁} {x₁ ∷ m₂} {suc k} k∈Dom⟨m₁⟩ k∉Dom⟨m₂⟩ k∈Dom⟨m₁Um₂⟩
  with U-∉-irr-get-help {m₁} {m₂} {k} (n∈S {k} {x} k∈Dom⟨m₁⟩) (λ x₂ → k∉Dom⟨m₂⟩ (domin {k} {m₂} {x₁} x₂)) (U-domout x x₁ k∈Dom⟨m₁Um₂⟩)
... | eq rewrite U-∉-irr-get-help-help k x x₁ m₁ m₂ k∈Dom⟨m₁Um₂⟩ = eq

U-∉-irr-get : ∀ {m₁ m₂ k} → (k∈ : k ∈ Dom' m₁) → k ∉ Dom' m₂ → ∃ λ k∈' → deref k m₁ k∈ ≡ deref k (m₁ U m₂) k∈'
U-∉-irr-get {m₁} {m₂} {k} k∈Dom'm₁ k∉Dom'm₂ =
  _ , U-∉-irr-get-help {m₁} {m₂} {k} k∈Dom'm₁ k∉Dom'm₂ (U-mono {m₁} {m₂} k∈Dom'm₁)

split : ∀{a b : ℕ} {l l'} → a ∷ l ≡ b ∷ l' → ((_≡_ a b) × (_≡_ l l'))
split refl = refl , refl

mapsuc≡ : ∀{l l'} → map suc l ≡ map suc l' → l ≡ l'
mapsuc≡ {[]} {[]} eq = refl
mapsuc≡ {[]} {x ∷ l'} ()
mapsuc≡ {x ∷ l} {[]} ()
mapsuc≡ {x ∷ l} {x₁ ∷ l'} eq with split eq
... | (a , b) rewrite (suc≡ a) | (mapsuc≡ b) = refl

U-=-irr : ∀ m m' → (Dom' m) ≡ (Dom' m') → ∀ k k∈ k∈2 → deref k (m U m') k∈ ≡ deref k m' k∈2
U-=-irr [] [] eq k ()
U-=-irr [] (nothing ∷ m') eq k x  with (subst (λ l → k ∈ l) (sym eq) x)
... | ()
U-=-irr [] (just x ∷ m') ()
U-=-irr (just x ∷ m) [] ()
U-=-irr (nothing ∷ m) [] eq k k∈ ()
U-=-irr (just x ∷ m) (nothing ∷ m') eq = ⊥-elim (0∈S{Dom' m'} (subst (λ x → 0 ∈ x) eq ((0 ∈ (0 ∷ (map suc (Dom' m)))) ∋ (here refl))))
U-=-irr (nothing ∷ m) (just x ∷ m') eq = ⊥-elim (0∈S{Dom' m} (subst (λ x → 0 ∈ x) (sym eq) ((0 ∈ (0 ∷ (map suc (Dom' m')))) ∋ (here refl))))
U-=-irr (nothing ∷ m) (nothing ∷ m') eq zero k∈ k∈2 = ⊥-elim (0∈S k∈)
U-=-irr (nothing ∷ m) (nothing ∷ m') eq (suc k) k∈ k∈2 = U-=-irr m m' (mapsuc≡ eq) k (n∈S{k}{nothing}{m U m'} k∈) (n∈S{k}{nothing}{m'} k∈2)
U-=-irr (just x ∷ m) (just x₁ ∷ m') eq zero = λ k∈ k∈2 → refl
U-=-irr (just x ∷ m) (just x₁ ∷ m') eq (suc k) k∈ k∈2 = U-=-irr m m' ((mapsuc≡ (proj₂ (split eq)))) k (n∈S{k}{just x₁}{m U m'} k∈) (n∈S{k}{just x₁}{m'} k∈2)

U-single-overwrite : ∀ k v1 v2 → (m-insert (just v1) k [])  U  (m-insert (just v2) k []) ≡ (m-insert (just v2) k [])
U-single-overwrite zero v1 v2 = refl
U-single-overwrite (suc k) v1 v2 rewrite U-single-overwrite k v1 v2 = refl

set-single-val : ∀ k v k∈ → (deref k (m-insert (just v) k []) k∈) ≡ v
set-single-val zero v (here refl) = refl
set-single-val zero v (there ())
set-single-val (suc k) v k∈ = set-single-val k v (n∈S{k}{nothing}{(m-insert (just v) k [])} k∈)

overwrite-single-val : ∀ k v m → k ∈ (Dom' m) → ((m-insert (just v) k []) U m) ≡ m
overwrite-single-val zero v [] ()
overwrite-single-val zero v (just x ∷ m) k∈ = refl
overwrite-single-val zero v (nothing ∷ m) k∈ = ⊥-elim (0∈S k∈)
overwrite-single-val (suc k) v [] ()
overwrite-single-val (suc k) v (just x ∷ m) (here ())
overwrite-single-val (suc k) v (just x ∷ m) (there k∈) rewrite overwrite-single-val k v m (sucout k∈) = refl
overwrite-single-val (suc k) v (nothing ∷ m) k∈ rewrite overwrite-single-val k v m (sucout k∈) = refl

U-insert-eq : ∀ k v m → (m-insert (just v) k m) ≡ m U (m-insert (just v) k [])
U-insert-eq zero v [] = refl
U-insert-eq zero v (just x ∷ m) rewrite U-comm{m}{[]} (λ z _ → λ ()) = refl
U-insert-eq zero v (nothing ∷ m) rewrite U-comm{m}{[]} (λ z _ → λ ()) = refl
U-insert-eq (suc k) v [] = refl
U-insert-eq (suc k) v (just x ∷ m) rewrite U-insert-eq k v m = refl
U-insert-eq (suc k) v (nothing ∷ m) rewrite U-insert-eq k v m = refl

insert-domain-eq : ∀ k v m → k ∈ (Dom' m) → (Dom' m) ≡ (Dom' (m-insert (just v) k m))
insert-domain-eq zero v [] ()
insert-domain-eq zero v (just x ∷ m) k∈ = refl
insert-domain-eq zero v (nothing ∷ m) k∈ = ⊥-elim (0∈S k∈)
insert-domain-eq (suc k) v [] ()
insert-domain-eq (suc k) v (just x ∷ m) (here ())
insert-domain-eq (suc k) v (just x ∷ m) (there k∈) rewrite insert-domain-eq k v m (sucout k∈) = refl
insert-domain-eq (suc k) v (nothing ∷ m) k∈ rewrite insert-domain-eq k v m (sucout k∈) = refl

insert-in-domain : ∀ m k v → k ∈ (Dom' (m-insert (just v) k m))
insert-in-domain [] zero v = here refl
insert-in-domain (x ∷ m) zero v = here refl
insert-in-domain [] (suc k) v = sucin (insert-in-domain [] k v)
insert-in-domain (x ∷ m) (suc k) v = domin{z = x} (insert-in-domain m k v)

insert-one-eq : ∀ k v k∈ → (deref k (m-insert (just v) k []) k∈) ≡ v
insert-one-eq zero v k∈ = refl
insert-one-eq (suc k) v k∈ = insert-one-eq k v (n∈S{k}{nothing}{(m-insert (just v) k [])} k∈)

insert-two-eq-one : ∀ k1 k2 v k1∈ → (deref k1 (m-insert (just v) k2 (m-insert (just v) k1 [])) k1∈) ≡ v
insert-two-eq-one zero zero v k1∈ = refl
insert-two-eq-one zero (suc k2) v k1∈ = refl
insert-two-eq-one (suc k1) zero v k1∈
  = insert-one-eq k1 v ( (n∈S{k1}{just v}{l = (m-insert (just v) k1 [])} k1∈) )
insert-two-eq-one (suc k1) (suc k2) v k1∈
     = insert-two-eq-one k1 k2 v ( (n∈S{k1}{nothing}{(m-insert (just v) k2 (m-insert (just v) k1 []))} k1∈))

insert-two-eq-two : ∀ k1 k2 v k2∈ → (deref k2 (m-insert (just v) k2 (m-insert (just v) k1 [])) k2∈) ≡ v
insert-two-eq-two zero zero v k2∈ = refl
insert-two-eq-two zero (suc k2) v k2∈
  = insert-one-eq k2 v ( (n∈S{k2}{just v}{l = (m-insert (just v) k2 [])} k2∈) )
insert-two-eq-two (suc k1) zero v k2∈ = refl
insert-two-eq-two (suc k1) (suc k2) v k2∈
     = insert-two-eq-two k1 k2 v ( (n∈S{k2}{nothing}{(m-insert (just v) k2 (m-insert (just v) k1 []))} k2∈))

data AllMap {i} (F : Value → Set i) : LMap → Set i where
  all : ∀ (m : LMap) → All (Data.Maybe.All F) m → AllMap F m

allMap : ∀ {i} m → {F : Value → Set i} → U.Decidable F → Dec (AllMap F m)
allMap m {F} dec with All.all (Data.Maybe.allDec dec)  m
allMap m {F} dec | yes p = yes (all m p)
allMap m {F} dec | no ¬p = no (λ { (all _ x) → ¬p x})

-- All.all (Data.Maybe.allDec F) m

deref∈ : ∀ {m} → (n : ℕ) → (n∈ : n ∈ (Dom' m)) → just (deref n m n∈) ∈ m
deref∈ {[]} zero ()
deref∈ {[]} (suc n) ()
deref∈ {just x ∷ m} zero n∈ = here refl
deref∈ {nothing ∷ m} zero n∈ = ⊥-elim (0∈S n∈)
deref∈ {just x ∷ m} (suc n) n∈ = there (deref∈ n (n∈S{n}{just x}{m} n∈))
deref∈ {nothing ∷ m} (suc n) n∈ = there (deref∈ n (n∈S{n}{nothing}{m} n∈))

allMap-lookup : ∀ {i} {F : Value → Set i} {m} → AllMap F m → ∀ (n : ℕ) → (k∈ : n ∈ (Dom' m)) → (F (deref n m k∈ ))
allMap-lookup {i} {F} (all m x) n n∈ with (All.lookup x) {just (deref n m n∈)} (deref∈ n n∈)
allMap-lookup {i} {F} (all m x) n n∈ | just px = px

allMap-tabulate : ∀ {i} {F : Value → Set i} {m} → (∀ (n : ℕ) → (k∈ : n ∈ (Dom' m)) → (F (deref n m k∈ ))) → AllMap F m
allMap-tabulate {m = []} FF = all [] All.[]
allMap-tabulate {F = F} {m = just x ∷ m} FF
   with allMap-tabulate{F = F} {m = m} (λ n k∈ →  subst F (deref-∈-irr (n∈S{n}{just x}{m} (there (sucin k∈))) k∈) (FF (suc n) (n+1∈S{n}{just x}{m} k∈)))
allMap-tabulate {_} {F} {just x ∷ m} FF | all .m x₁ = all (just x ∷ m) ((just (FF 0 (here refl))) All.∷ x₁)
allMap-tabulate {F = F} {m = nothing ∷ m} FF
   with allMap-tabulate {m = m} (λ n k∈ →  subst F (deref-∈-irr (n∈S{n}{nothing}{m} (sucin k∈)) k∈) (FF (suc n) (n+1∈S{n}{nothing}{m} k∈)) )
allMap-tabulate {_} {_} {nothing ∷ m} FF | all .m x = all (nothing ∷ m) (nothing All.∷ x)

andmap : ∀ {i} {F : Value → Set i} → U.Decidable F → (m : LMap) → Dec ∀ (n : ℕ) → (n∈ : n ∈ (Dom' m)) → (F (deref n m n∈))
andmap Fp m with allMap m Fp
andmap Fp m | yes p = yes (allMap-lookup p)
andmap Fp m | no ¬p = no (λ x → ¬p (allMap-tabulate x))

ocount : (Value -> Bool) -> LMap -> ℕ
ocount p [] = 0
ocount p (just x ∷ m) with p x
ocount p (just x ∷ m) | false = ocount p m
ocount p (just x ∷ m) | true = suc (ocount p m)
ocount p (nothing ∷ m) = ocount p m

change-one-ocount-goes-down :
  ∀ (m : LMap) ->
    (p : Value -> Bool) ->
    (n : ℕ) ->
    (k∈ : n ∈ (Dom' m)) ->
    p (deref n m k∈) ≡ true ->
    (v : Value) ->
    p v ≡ false ->
    ocount p m ≡ suc (ocount p (m-insert (just v) n m))
change-one-ocount-goes-down = f where
  f : ∀ (m : LMap) ->
    (p : Value -> Bool) ->
    (n : ℕ) ->
    (k∈ : n ∈ (Dom' m)) ->
    p (deref n m k∈) ≡ true ->
    (v : Value) ->
    p v ≡ false ->
    ocount p m ≡ suc (ocount p (m-insert (just v) n m))
  f [] p zero () p[derefnmk∈]≡true v pv≡false
  f (just x ∷ m) p zero k∈ p[derefnmk∈]≡true v pv≡false with p x
  ... | true with p v
  f (just x ∷ m) p zero k∈ p[derefnmk∈]≡true v () | true | true
  ... | false = refl
  f (just x ∷ m) p zero k∈ () v pv≡false | false
  f (nothing ∷ m) p zero k∈ p[derefnmk∈]≡true v pv≡false = ⊥-elim (0∈S k∈)
  f [] p (suc n) () p[derefnmk∈]≡true v pv≡false
  f (just x ∷ m) p (suc n) k∈ p[derefnmk∈]≡true v pv≡false with p x
  ... | true = cong suc (f m p n
                           (n∈S{x = just x}{l = m} k∈)
                           p[derefnmk∈]≡true v pv≡false)
  ... | false = f m p n (n∈S{x = just x}{l = m} k∈)
                  p[derefnmk∈]≡true v pv≡false
  f (nothing ∷ m) p (suc n) k∈ p[derefnmk∈]≡true v pv≡false
   = f m p n (n∈S{x = nothing}{l = m} k∈) p[derefnmk∈]≡true v pv≡false

change-nothing-ocount-stays-same :
  ∀ (m : LMap) ->
    (p : Value -> Bool) ->
    (n : ℕ) ->
    (k∈ : n ∈ (Dom' m)) ->
    (v : Value) ->
    p (deref n m k∈) ≡ p v ->
    ocount p m ≡ ocount p (m-insert (just v) n m)
change-nothing-ocount-stays-same = f where

  f : ∀ (m : LMap) ->
    (p : Value -> Bool) ->
    (n : ℕ) ->
    (k∈ : n ∈ (Dom' m)) ->
    (v : Value) ->
    p (deref n m k∈) ≡ p v ->
    ocount p m ≡ ocount p (m-insert (just v) n m)
  f [] p zero () v pold≡pv
  f (just x ∷ m) p zero k∈ v pold≡pv with p x | p v
  f (just x ∷ m) p zero k∈ v pold≡pv | false | false = refl
  f (just x ∷ m) p zero k∈ v () | false | true
  f (just x ∷ m) p zero k∈ v () | true | false
  f (just x ∷ m) p zero k∈ v pold≡pv | true | true = refl
  f (nothing ∷ m) p zero k∈ v pold≡pv with p v
  f (nothing ∷ m) p zero k∈ v pold≡pv | false = refl
  f (nothing ∷ m) p zero k∈ v pold≡pv | true = ⊥-elim (0∈S k∈)
  f [] p (suc n) () v pold≡pv
  f (just x ∷ m) p (suc n) k∈ v pold≡pv with p x
  f (just x ∷ m) p (suc n) k∈ v pold≡pv | true =
     cong suc (f m p n (n∈S{x = just x}{l = m} k∈) v pold≡pv)
  f (just x ∷ m) p (suc n) k∈ v pold≡pv | false =
     f m p n (n∈S{x = just x}{l = m} k∈) v pold≡pv
  f (nothing ∷ m) p (suc n) k∈ v pold≡pv =
    f m p n (n∈S{x = nothing}{l = m} k∈) v pold≡pv

ocount-merge≤′sum-ocount :
  ∀ (m1 m2 : LMap) ->
    (p : Value -> Bool) ->
    ocount p (m1 U m2) ≤′ ocount p m1 + ocount p m2
ocount-merge≤′sum-ocount = f where

  f : ∀ (m1 m2 : LMap) ->
        (p : Value -> Bool) ->
        ocount p (m1 U m2) ≤′ ocount p m1 + ocount p m2
  f [] [] p = ≤′-refl
  f [] (x ∷ m2) p = ≤′-refl
  f (x ∷ m1) [] p = ≤⇒≤′ (m≤m+n (ocount p (x ∷ m1)) 0)
  f (just x ∷ m1) (just x₁ ∷ m2) p with p x | p x₁ | f m1 m2 p
  f (just x ∷ m1) (just x₁ ∷ m2) p | false | false | R = R
  f (just x ∷ m1) (just x₁ ∷ m2) p | false | true | R =
     ≤′-trans {y = suc (ocount p m1 + ocount p m2)}
              (s≤′s R) (≡is≤′ (sym (+-suc (ocount p m1) (ocount p m2))))
  f (just x ∷ m1) (just x₁ ∷ m2) p | true | false | R =
    ≤′-step R
  f (just x ∷ m1) (just x₁ ∷ m2) p | true | true | R =
    s≤′s (≤′-trans {y = ocount p m1 + ocount p m2}
         R
         (≤′+r {ocount p m2} {suc (ocount p m2)} {ocount p m1} (≤′-step ≤′-refl)))
  f (just x ∷ m1) (nothing ∷ m2) p with p x | f m1 m2 p
  f (just x ∷ m1) (nothing ∷ m2) p | false | R = R
  f (just x ∷ m1) (nothing ∷ m2) p | true | R = s≤′s R
  f (nothing ∷ m1) (just x ∷ m2) p with p x | f m1 m2 p
  f (nothing ∷ m1) (just x ∷ m2) p | false | R = R
  f (nothing ∷ m1) (just x ∷ m2) p | true | R =
     ≤′-trans {y = suc (ocount p m1 + ocount p m2)}
              (s≤′s R) (≡is≤′ (sym (+-suc (ocount p m1) (ocount p m2))))
  f (nothing ∷ m1) (nothing ∷ m2) p with f m1 m2 p
  ... | R = R

Dom'+∈ : (L : LMap) → List (∃[ n ] (n ∈ (Dom' L)))
Dom'+∈ L = help (Dom' L)
 where
  help : (x : List ℕ) → (List (∃[ y ] (y ∈ x)))
  help [] = []
  help (x ∷ x₁) = (x , here refl) ∷ map (λ {(a , b) → a , there b}) (help x₁)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------------
-- Testing the class AgdaInternal.RemoveProofTerms.RemoveVar: Lam term
------------------------------------------------------------------------------

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

module RemoveVar.LamTerm where

-- We add 3 to the fixities of the standard library.
infixr 8 _∷_
infixr 7 _,_
infix  7 _≡_ _≈_
infixr 5 _∧_
infix 5  ∃

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

postulate
  D      : Set
  _∷_    : D → D → D
  Stream : D → Set
  _≈_    : D → D → Set

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

data ∃ (A : D → Set) : Set where
  _,_ : (t : D) → A t → ∃ A

syntax ∃ (λ x → e) = ∃[ x ] e

data _≡_ (x : D) : D → Set where
  refl : x ≡ x

postulate
  Stream-gfp₂ : (P : D → Set) →
                -- P is post-fixed point of StreamF.
                (∀ {xs} → P xs → ∃[ x' ] ∃[ xs' ] P xs' ∧ xs ≡ x' ∷ xs') →
                -- Stream is greater than P.
                ∀ {xs} → P xs → Stream xs

postulate
  ≈-gfp₁ : ∀ {xs ys} → xs ≈ ys →
           ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs' ≈ ys' ∧ xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys'
{-# ATP axiom ≈-gfp₁ #-}

-- See Issue #81.
P : D → Set
P ws = ∃[ zs ] ws ≈ zs
{-# ATP definition P #-}

≈→Stream : ∀ {xs ys} → xs ≈ ys → Stream xs
≈→Stream {xs} {ys} xs≈ys = Stream-gfp₂ P helper (ys , xs≈ys)
  where
  postulate helper : ∀ {ws} → P ws → ∃[ w' ] ∃[ ws' ] P ws' ∧ ws ≡ w' ∷ ws'
  {-# ATP prove helper #-}

ext: agda

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module modal-lob-reduced where
data TYP : Set where
  ARR : TYP → TYP → TYP -- the type of implications, or function types
  BOX : TYP → TYP -- the modal □ operator, denoted to TERM
  LӦB-SENTENCE : TYP → TYP -- the Lӧbian sentence "If this sentence is provable, then A"
                           -- this is the modal fixpoint of λ Ψ. □ Ψ → A

data TERM : TYP → Set where
  k : {A : TYP} → TERM A → TERM (BOX A) -- from A, we deduce □ A
  distr : {A B : TYP} → TERM (ARR (BOX (ARR A B)) (ARR (BOX A) (BOX B))) -- we deduce □ (A → B) → □ A → □ B
  s4 : {A : TYP} → TERM (ARR (BOX A) (BOX (BOX A))) -- we deduce □ A →  □ □ A
  app : {A B : TYP} → TERM (ARR A B) → TERM A → TERM B -- from A → B, and A, we deduce B
  lӧb→ : {A : TYP} → TERM (ARR (LӦB-SENTENCE A) (ARR (BOX (LӦB-SENTENCE A)) A)) -- LӦB-SENTENCE A is Ψ such that Ψ → (□ Ψ → A)
  lӧb← : {A : TYP} → TERM (ARR (ARR (BOX (LӦB-SENTENCE A)) A) (LӦB-SENTENCE A)) -- LӦB-SENTENCE A is Ψ such that (□ Ψ → A) → Ψ
  compose : {A B C : TYP} → TERM (ARR A B) → TERM (ARR B C) → TERM (ARR A C) -- from A → B and B → C, we deduce A → C
  compose2 : {A B C : TYP} → TERM (ARR A B) → TERM (ARR A (ARR B C)) → TERM (ARR A C) -- from A → B and A → B → C, we deduce A → C

⟦_⟧ᵀ : TYP → Set
⟦ ARR A B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
⟦ BOX T ⟧ᵀ = TERM T
⟦ LӦB-SENTENCE A ⟧ᵀ = TERM (LӦB-SENTENCE A) → ⟦ A ⟧ᵀ

⟦_⟧ᵗ : {T : TYP} → TERM T → ⟦ T ⟧ᵀ
⟦ k e ⟧ᵗ = e
⟦ distr ⟧ᵗ box-a-b box-a = app box-a-b box-a
⟦ s4 ⟧ᵗ = k
⟦ app f x ⟧ᵗ = ⟦ f ⟧ᵗ ⟦ x ⟧ᵗ
⟦ lӧb→ ⟧ᵗ = λ x → x -- this implication is true because on denotation, the two are judgmentally equal
⟦ lӧb← ⟧ᵗ = λ x → x -- this implication is true because on denotation, the two are judgmentally equal
⟦ compose f g ⟧ᵗ = λ x → ⟦ g ⟧ᵗ (⟦ f ⟧ᵗ x)
⟦ compose2 f g ⟧ᵗ = λ x → ⟦ g ⟧ᵗ x (⟦ f ⟧ᵗ x)

Lӧb′s-Theorem : {A : TYP} → TERM (ARR (BOX A) A) → TERM A -- from □ A → A, we deduce A
Lӧb′s-Theorem {A} interp = app prog (k (app lӧb← prog))
  where prog : TERM (ARR (BOX (LӦB-SENTENCE A)) A)
        prog = compose (compose2 s4 (compose (app distr (k lӧb→)) distr)) interp

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Notation for freely adding an infimum to any set
------------------------------------------------------------------------

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

module Relation.Nullary.Construct.Add.Infimum where

open import Relation.Nullary.Construct.Add.Point
  renaming (Pointed to _₋; ∙ to ⊥₋)
  public


text:
{- Copyright © 1992–2002 The University of Glasgow
Copyright © 2015 Benjamin Barenblat

Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
this file except in compliance with the License.  You may obtain a copy of the
License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed
under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
CONDITIONS OF ANY KIND, either express or implied.  See the License for the
specific language governing permissions and limitations under the License. -}

module B.Prelude.Monad where

import Category.Monad
import Data.List
import Data.Maybe
open import Function using (const)

open Category.Monad
  using (RawMonad)
  public

open Category.Monad.RawMonad ⦃...⦄
  using (_>>=_; _>>_; return)
  public

instance
  Monad-List : ∀ {ℓ} → RawMonad (Data.List.List {ℓ})
  Monad-List = Data.List.monad

  Monad-Maybe : ∀ {ℓ} → RawMonad (Data.Maybe.Maybe {ℓ})
  Monad-Maybe = Data.Maybe.monad

  Monad-Function : ∀ {ℓ} {r : Set ℓ} → RawMonad (λ s → (r → s))
  Monad-Function {r} = record { return = const {r}
                              ; _>>=_ = λ f k → λ r → k (f r) r }

max_stars_repo_name: bbarenblat/B

max_issues_repo_name: bbarenblat/B

max_forks_repo_name: bbarenblat/B


text:
------------------------------------------------------------------------
-- Up-to techniques via
------------------------------------------------------------------------

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

module Up-to.Via where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bijection equality-with-J as Bijection using (_↔_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level.Closure equality-with-J using (ext⁻¹)

open import Indexed-container
open import Indexed-container.Combinators
  hiding (id) renaming (_∘_ to _⊚_)
open import Relation
open import Up-to

-- The property of being an up-to technique via another (or the same)
-- relation transformer. This is an adaptation of Definition 6.3.25 in
-- Pous and Sangiorgi's "Enhancements of the bisimulation proof
-- method".

Up-to-technique-via :
  ∀ {ℓ} {I : Type ℓ} →
  Container I I → Trans ℓ I → Trans ℓ I → Type (lsuc ℓ)
Up-to-technique-via C F G =
  Extensive G
    ×
  (∀ R → R ⊆ ⟦ C ⟧ (F R) → G R ⊆ ⟦ C ⟧ (G R))

-- If F is an up-to technique via G, then F is an up-to technique.
--
-- A corresponding result is mentioned by Pous and Sangiorgi right
-- after Definition 6.3.25.

up-to-via→up-to :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F G} →
  Up-to-technique-via C F G → Up-to-technique C F
up-to-via→up-to {C = C} {F} {G} up-to {R} =
  R ⊆ ⟦ C ⟧ (F R)    ↝⟨ proj₂ up-to _ ⟩
  G R ⊆ ⟦ C ⟧ (G R)  ↝⟨ unfold C ⟩
  G R ⊆ ν C ∞        ↝⟨ (λ hyp {_} x → hyp (proj₁ up-to R x)) ⟩□
  R ⊆ ν C ∞          □

-- If F is an up-to technique, then F is an up-to technique via
-- _∪ ν C ∞.

up-to→up-to-via :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F} →
  Up-to-technique C F → Up-to-technique-via C F (_∪ ν C ∞)
up-to→up-to-via {C = C} {F} up-to =
    (λ R →
       R          ⊆⟨ inj₁ ⟩∎
       R ∪ ν C ∞  ∎)
  , λ R →
      R ⊆ ⟦ C ⟧ (F R)                ↝⟨ up-to ⟩
      R ⊆ ν C ∞                      ↝⟨ (λ hyp {_} →

          R ∪ ν C ∞                            ⊆⟨ [ hyp {_} , id ] ⟩
          ν C ∞                                ⊆⟨ ν-out _ ⟩
          ⟦ C ⟧ (ν C ∞)                        ⊆⟨ map C inj₂ ⟩∎
          ⟦ C ⟧ (R ∪ ν C ∞)                    ∎) ⟩

      R ∪ ν C ∞ ⊆ ⟦ C ⟧ (R ∪ ν C ∞)  □

-- A lemma that corresponds to Pous and Sangiorgi's Lemma 6.3.27: If G
-- satisfies certain properties, then Up-to-technique-via C F is
-- closed under G ∘_.

up-to-via-∘ :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F G H} →
  Extensive G →
  (∀ R → R ⊆ ⟦ C ⟧ R → G R ⊆ ⟦ C ⟧ (G R)) →
  Up-to-technique-via C F H →
  Up-to-technique-via C F (G ∘ H)
up-to-via-∘ {C = C} {F} {G} {H} extensive pres up-to =
    (λ R →
       R        ⊆⟨ proj₁ up-to _ ⟩
       H R      ⊆⟨ extensive _ ⟩∎
       G (H R)  ∎)
  , λ R →
      R ⊆ ⟦ C ⟧ (F R)            ↝⟨ proj₂ up-to _ ⟩
      H R ⊆ ⟦ C ⟧ (H R)          ↝⟨ pres _ ⟩□
      G (H R) ⊆ ⟦ C ⟧ (G (H R))  □

mutual

  -- If the container F is an up-to technique via a symmetric relation
  -- transformer, then ν ⟷[ C ⊚ F ] ∞ is contained in ν ⟷[ C ] ∞. This
  -- result corresponds to Pous and Sangiorgi's Proposition 6.3.28.

  up-to-via→ν-∘⊆ν :
    ∀ {ℓ} {I : Type ℓ} {C : Container (I × I) (I × I)} {F G} →
    Symmetric swap G →
    Up-to-technique-via C ⟦ F ⟧ G →
    ν ⟷[ C ⊚ F ] ∞ ⊆ ν ⟷[ C ] ∞
  up-to-via→ν-∘⊆ν symm up-to = up-to-via²→ν-∘⊆ν refl symm up-to up-to

  -- A generalisation of the result above.

  up-to-via²→ν-∘⊆ν :
    ∀ {ℓ} {I : Type ℓ} {C₁ C₂ : Container I I} {F₁ F₂ G} {f : I → I} →
    f ∘ f ≡ id →
    Symmetric f G →
    Up-to-technique-via C₁ ⟦ F₁ ⟧ G →
    Up-to-technique-via C₂ ⟦ F₂ ⟧ G →
    ν (C₁ ⊚ F₁ ⊗ reindex f (C₂ ⊚ F₂)) ∞ ⊆ ν (C₁ ⊗ reindex f C₂) ∞
  up-to-via²→ν-∘⊆ν {ℓ} {I} {C₁} {C₂} {F₁} {F₂} {G} {f}
                   inv symm up-to₁ up-to₂ =
                                                       $⟨ (λ {_} → ν-out _) ⟩
    R ⊆ ⟦ C₁ ⊚ F₁ ⊗ reindex f (C₂ ⊚ F₂) ⟧ R            ↝⟨ ⊆-congʳ _ $ ⟦⊗⟧↔ _ (C₁ ⊚ F₁) (reindex f (C₂ ⊚ F₂)) ⟩
    R ⊆ ⟦ C₁ ⊚ F₁ ⟧ R ∩ ⟦ reindex f (C₂ ⊚ F₂) ⟧ R      ↝⟨ from-isomorphism implicit-ΠΣ-comm F.∘
                                                          implicit-∀-cong _ (from-isomorphism ΠΣ-comm) ⟩
    R ⊆ ⟦ C₁ ⊚ F₁ ⟧ R × R ⊆ ⟦ reindex f (C₂ ⊚ F₂) ⟧ R  ↝⟨ Σ-map lemma₁ lemma₂ ⟩
    G R ⊆ ⟦ C₁ ⟧ (G R) × G R ⊆ ⟦ reindex f C₂ ⟧ (G R)  ↝⟨ _⇔_.from (from-isomorphism implicit-ΠΣ-comm F.∘
                                                                    implicit-∀-cong _ (from-isomorphism ΠΣ-comm)) ⟩
    G R ⊆ ⟦ C₁ ⟧ (G R) ∩ ⟦ reindex f C₂ ⟧ (G R)        ↝⟨ _⇔_.from $ ⊆-congʳ _ $ ⟦⊗⟧↔ _ C₁ (reindex f C₂) ⟩
    G R ⊆ ⟦ C₁ ⊗ reindex f C₂ ⟧ (G R)                  ↝⟨ unfold (C₁ ⊗ reindex f C₂) ⟩
    G R ⊆ ν (C₁ ⊗ reindex f C₂) ∞                      ↝⟨ (λ hyp {_} x → hyp (proj₁ up-to₁ R x)) ⟩□
    R ⊆ ν (C₁ ⊗ reindex f C₂) ∞                        □
    where
    R = ν (C₁ ⊚ F₁ ⊗ reindex f (C₂ ⊚ F₂)) ∞

    I↔I : I ↔ I
    I↔I = Bijection.bijection-from-involutive-family
            (λ _ _ → f) (λ _ _ → ext⁻¹ inv) tt tt

    ∘⊆⇔⊆∘ : {S₁ S₂ : Rel ℓ I} → S₁ ∘ f ⊆ S₂ ⇔ S₁ ⊆ S₂ ∘ f
    ∘⊆⇔⊆∘ {S₁ = S₁} {S₂} =
      (∀ {p} → S₁ (f p) → S₂ p)  ↔⟨ Bijection.implicit-Π↔Π ⟩
      (∀ p → S₁ (f p) → S₂ p)    ↝⟨ Π-cong _ I↔I (λ _ → →-cong _ F.id (≡⇒↝ _ $ cong S₂ $ ext⁻¹ (sym inv) _)) ⟩
      (∀ p → S₁ p → S₂ (f p))    ↔⟨ inverse Bijection.implicit-Π↔Π ⟩□
      (∀ {p} → S₁ p → S₂ (f p))  □

    lemma₁ =
      R ⊆ ⟦ C₁ ⊚ F₁ ⟧ R      ↝⟨ ⊆-congʳ _ (⟦∘⟧↔ _ C₁) ⟩
      R ⊆ ⟦ C₁ ⟧ (⟦ F₁ ⟧ R)  ↝⟨ proj₂ up-to₁ _ ⟩□
      G R ⊆ ⟦ C₁ ⟧ (G R)     □

    lemma₂ =
      R ⊆ ⟦ reindex f (C₂ ⊚ F₂) ⟧ R    ↝⟨ ⊆-congʳ _ $ ⟦reindex⟧↔ _ (C₂ ⊚ F₂) ⟩
      R ⊆ ⟦ C₂ ⊚ F₂ ⟧ (R ∘ f) ∘ f      ↝⟨ ⊆-congʳ _ (⟦∘⟧↔ _ C₂) ⟩
      R ⊆ ⟦ C₂ ⟧ (⟦ F₂ ⟧ (R ∘ f)) ∘ f  ↝⟨ _⇔_.from ∘⊆⇔⊆∘ ⟩
      R ∘ f ⊆ ⟦ C₂ ⟧ (⟦ F₂ ⟧ (R ∘ f))  ↝⟨ proj₂ up-to₂ _ ⟩
      G (R ∘ f) ⊆ ⟦ C₂ ⟧ (G (R ∘ f))   ↝⟨ involution→other-symmetry G inv symm _ ⊆-cong-→ ⟦⟧-cong _ C₂ (symm _) ⟩
      G R ∘ f ⊆ ⟦ C₂ ⟧ (G R ∘ f)       ↝⟨ _⇔_.to ∘⊆⇔⊆∘ ⟩
      G R ⊆ ⟦ C₂ ⟧ (G R ∘ f) ∘ f       ↝⟨ _⇔_.from $ ⊆-congʳ _ $ ⟦reindex⟧↔ _ C₂ ⟩
      G R ⊆ ⟦ reindex f C₂ ⟧ (G R)     □

-- If F is monotone and compatible, then F is an up-to technique via
-- F ^ω_. This result corresponds to Pous and Sangiorgi's
-- Theorem 6.3.26.

monotone→compatible→up-to-via :
  ∀ {ℓ} {I : Type ℓ} {C : Container I I} {F} →
  Monotone F →
  Compatible C F → Up-to-technique-via C F (F ^ω_)
monotone→compatible→up-to-via {C = C} {F} mono comp =
    (λ R →
       R       ⊆⟨ 0 ,_ ⟩∎
       F ^ω R  ∎)
  , λ R R⊆ →
      F ^ω R          ⊆⟨ compatible→^ω-post-fixpoint _ mono comp R⊆ ⟩∎
      ⟦ C ⟧ (F ^ω R)  ∎

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.System.Parameters
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block      as Block
import      LibraBFT.Impl.Consensus.ConsensusTypes.Properties.QuorumCert as QuorumCertProps
import      LibraBFT.Impl.Consensus.ConsensusTypes.Properties.VoteData as VoteDataProps
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert as QuorumCert
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote       as Vote
import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteData   as VoteData
open import LibraBFT.Impl.Consensus.SafetyRules.SafetyRules
import      LibraBFT.Impl.Handle                              as Handle
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.Impl.OBM.Crypto                          as Crypto
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures      as LedgerInfoWithSignatures
open import LibraBFT.Impl.Types.ValidatorSigner               as ValidatorSigner
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
import      LibraBFT.ImplShared.Util.Crypto                   as Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Hash
open import Util.KVMap                                        as Map
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open        ParamsWithInitAndHandlers Handle.InitHandler.initAndHandlers
open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms
                      Handle.InitHandler.initAndHandlers
                      PeerCanSignForPK PeerCanSignForPK-stable
open Invariants
open RoundManagerTransProps

module LibraBFT.Impl.Consensus.SafetyRules.Properties.SafetyRules where

module verifyAndUpdatePreferredRoundDefs (quorumCert : QuorumCert) (safetyData : SafetyData) where
  preferredRound = safetyData ^∙ sdPreferredRound
  oneChainRound  = quorumCert ^∙ qcCertifiedBlock ∙ biRound
  twoChainRound  = quorumCert ^∙ qcParentBlock ∙ biRound

  C₁ = oneChainRound < preferredRound
  C₂ = twoChainRound > preferredRound
  C₃ = twoChainRound < preferredRound
  C₄ = twoChainRound ≡ preferredRound

  safetyData' = safetyData & sdPreferredRound ∙~ twoChainRound

module verifyAndUpdatePreferredRoundMSpec (quorumCert : QuorumCert) (safetyData : SafetyData) where
  open verifyAndUpdatePreferredRoundDefs quorumCert safetyData

  module _ (pre : RoundManager) where
    record setPR (sd : SafetyData) : Set where
      field
        cond  : C₂
        eff   : sd ≡ safetyData'

    record noChanges (sd : SafetyData) : Set where
      field
        noUpd : sd ≡ safetyData

    record ConditionCorrectR (sd : SafetyData) : Set where
      field
        ep≡    : sd ≡L safetyData at sdEpoch
        qcr≤pr : quorumCert ^∙ qcParentBlock ∙ biRound ≤ sd ^∙ sdPreferredRound
        conds  : noChanges sd ⊎ setPR sd
    open ConditionCorrectR public

    ConditionCorrect : Either ErrLog SafetyData → Set
    ConditionCorrect (Left _)   = ⊤
    ConditionCorrect (Right sd) = ConditionCorrectR sd

    record Contract (r : Either ErrLog SafetyData) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        noOuts        : OutputProps.NoMsgs outs
        noEff         : post ≡ pre
        condCorr      : ConditionCorrect r

  contract
      : ∀ pre
        → LBFT-weakestPre (verifyAndUpdatePreferredRoundM quorumCert safetyData)
                          (Contract pre) pre
  proj₁ (contract pre) _ = mkContract refl refl tt
  proj₂ (contract pre) x rewrite x
     with <-cmp twoChainRound preferredRound
  ...| tri< lt _   _  = λ where ._ refl ._ refl → mkContract refl refl
                                                    (record { ep≡ = refl
                                                            ; qcr≤pr = <⇒≤ lt
                                                            ; conds = inj₁ (record { noUpd = refl }) })
  ...| tri≈ _ refl _  = λ where ._ refl         → mkContract refl refl
                                                    (record { ep≡ = refl
                                                            ; qcr≤pr = ≤-refl
                                                            ; conds = inj₁ (record { noUpd = refl }) })
  ...| tri> _ _    gt = λ where ._ refl ._ refl → mkContract refl refl
                                                    (record { ep≡ = refl
                                                            ; qcr≤pr = ≤-refl
                                                            ; conds = inj₂ (record { cond = gt ; eff = refl }) })

module extensionCheckSpec (voteProposal : VoteProposal) where
  proposedBlock = voteProposal ^∙ vpBlock
  obmAEP        = voteProposal ^∙ vpAccumulatorExtensionProof

  voteData      =
     (VoteData.new
       (Block.genBlockInfo
         proposedBlock
         -- OBM-LBFT-DIFF: completely different
         (Crypto.obmHashVersion (obmAEP ^∙ aepObmNumLeaves))
         (obmAEP ^∙ aepObmNumLeaves)
         (voteProposal ^∙ vpNextEpochState))
       (proposedBlock ^∙ bQuorumCert ∙ qcCertifiedBlock))

  contract -- TODO-1: refine (waiting on: extensionCheckM)
    : ∀ {ℓ} (Post : Either ErrLog VoteData → Set ℓ)
      → (∀ e → Post (Left e))
      → (Post (pure voteData))
      → Post (extensionCheck voteProposal)
  contract Post pfBail pfOk = pfOk

module constructLedgerInfoMSpec (proposedBlock : Block) (consensusDataHash : HashValue) where
  -- This is a place-holder contract that requires refinement once
  -- `constructLedgerInfoM is implemented.
  postulate -- TODO-1: refine and prove
    contract
      : ∀ P pre
        → P (inj₁ fakeErr) pre []
        → (∀ ledgerInfo → P (inj₂ ledgerInfo) pre [])
        → LBFT-weakestPre (constructLedgerInfoM proposedBlock consensusDataHash) P pre

-- TUTORIAL: Weakest preconditions generated from conditionals, translating a
-- boolean equality test to proofs of (in)equality.
module verifyEpochMSpec (epoch : Epoch) (safetyData : SafetyData) where
  -- The body of `verifyEpochM` is:
  -- > ifM not ⌊ epoch ≟ℕ safetyData ^∙ sdEpoch ⌋
  -- >   then bail fakeErr -- log: error: incorrect epoch
  -- >   else ok unit
  contract
    : ∀ P pre
      → (epoch ≢ safetyData ^∙ sdEpoch → P (inj₁ fakeErr) pre [])
      → (epoch ≡ safetyData ^∙ sdEpoch → P (inj₂ unit) pre [])
      → LBFT-weakestPre (verifyEpochM epoch safetyData) P pre
  -- The outermost node of the AST of `verifyEpochM` is `ifM_then_else_ ...`, so
  -- our goal is to return a product: one proof corresponding to the "then" case
  -- one and one proof corresponding to the "else" case.
  --
  -- 1. In the "then" case, we recieve a proof `e≢` that
  --    > toBool (not ⌊ epoch ≟ℕ safetyData ^∙ sdEpoch ⌋) ≡ true
  proj₁ (contract Post pre pfBail pfOk) e≢
  --    - abstract over the expression that prevents us from analyzing this evidence
     with epoch ≟ℕ safetyData ^∙ sdEpoch
  --    - Agda can tell that `yes pf` is not an option, since e≢ would have type
  --      `false ≡ true` in that case
  ...| no  pf = pfBail pf
  -- 2. In the "else" case, we receive a proof `e≡` that
  --    > toBool (not ⌊ epoch ≟ℕ safetyData ^∙ sdEpoch ⌋) ≡ false
  proj₂ (contract Post pre pfBail pfOk) e≡
  --    - perform the same `with` abstraction as the previous case
     with epoch ≟ℕ safetyData ^∙ sdEpoch
  --    - Agda can tell that `no pf` is not an option
  ...| yes pf = pfOk pf

-- TUTORIAL: Translating boolean comparison tests to proofs.
module verifyAndUpdateLastVoteRoundMSpec (round : Round) (safetyData : SafetyData) where
  safetyData' = safetyData & sdLastVotedRound ∙~ round
  -- This example shows that we could have further simplified the proof of the
  -- contract for `verifyEpochM`. In `Util.Prelude`, we define lemmas
  -- > toWitnessT : ∀{ℓ}{P : Set ℓ}{d : Dec P} → ⌊ d ⌋ ≡ true → P
  -- > toWitnessF : ∀{ℓ}{P : Set ℓ}{d : Dec P} → ⌊ d ⌋ ≡ false → ¬ P
  -- which extract the underlying proof used to construct `d` given evidence
  -- that "lowering" `d` to a boolean produces `true` or `false`.
  contract
    : ∀ P pre
      → ((r>lvr : round > safetyData ^∙ sdLastVotedRound) → P (Right safetyData') pre [])
      → ((r≤lvr : ¬ (round > safetyData ^∙ sdLastVotedRound)) → P (Left fakeErr) pre [])
      → LBFT-weakestPre (verifyAndUpdateLastVoteRoundM round safetyData) P pre
  proj₁ (contract Post pre pfOk pfBail) r>lvr = pfOk (toWitnessT r>lvr)
  proj₂ (contract Post pre pfOk pfBail) ¬r>lvr = pfBail (toWitnessF ¬r>lvr)

module verifyQcMSpec (self : QuorumCert) where
  getVv : RoundManager → ValidatorVerifier
  getVv = _^∙ (rmEpochState ∙ esVerifier)

  -- See comment on contract below to understand the motivation for stating and proving the property
  -- this way.

  Contract : RoundManager → RWS-Post Output RoundManager (Either ErrLog Unit)
  Contract pre (Left _)  post outs = post ≡ pre × outs ≡ []
  Contract pre (Right _) post outs = post ≡ pre × outs ≡ []
                                   × QuorumCertProps.Contract self (getVv pre)

  contract' : ∀ pre → RWS-weakestPre (verifyQcM self) (Contract pre) unit pre
  contract' _ _ _ (Left x₂) _ = refl , refl
  contract' pre vv refl (Right unit) x₁ = refl , refl , QuorumCertProps.contract self vv (Right unit) refl (sym x₁)

  -- Suppose verifyQcM runs from prestate pre, and we wish to ensure that postcondition Post holds
  -- afterwards.  If P holds provided verifyQcM does not modify the state and does not produce any
  -- Outputs, and, if verifyQcM succeeds (returns Right unit), P holds provided
  -- QuorumCertProps.Contract holds for the given QuorumCert and the ValidatorVerifier of the
  -- prestate, then verifyQcM ensures P holds.  Proving this directly is painful because it's
  -- difficult to construct a QuorumCertProps.Contract self (getVv pre) that Agda understands allows
  -- us to invoke the rPrf (condition on P in case verifyQcM succeeds).  Therefore, we restate the
  -- conditions on P (as P', above) and prove that P' implies P, and then use LBFT-⇒ to achieve
  -- the desired result.
  contract
    : ∀ P pre
    → (∀ {e} → P (Left e) pre [])  -- verifyQcM does not emit any outputs, it just propagates a Left ErrLog, hence []
    → (QuorumCertProps.Contract self (getVv pre) → P (Right unit) pre [])
    → RWS-weakestPre (verifyQcM self) P unit pre
  contract Post pre lPrf rPrf = LBFT-⇒ (verifyQcM self) pre
                                       (contract' pre)
                                       (λ { (Left x₁) st outs (refl , refl)          → lPrf
                                          ; (Right unit) st outs (refl , refl , prf) → rPrf prf })

module constructAndSignVoteMSpec where

  VoteResultCorrect : (pre post : RoundManager) (block : Block) (lvr≡? : Bool) (r : Either ErrLog Vote) → Set
  VoteResultCorrect pre post block lvr≡? (Left e) = VoteNotGenerated pre post lvr≡?
  VoteResultCorrect pre post block lvr≡? (Right vote) = Voting.VoteGeneratedCorrect pre post vote block

  record Contract (pre : RoundManager) (block : Block) (r : Either ErrLog Vote) (post : RoundManager) (outs : List Output) : Set where
    constructor mkContract
    field
      -- General properties / invariants
      rmInv          : Preserves RoundManagerInv pre post
      noEpochChange  : NoEpochChange pre post
      noMsgOuts      : OutputProps.NoMsgs outs
      -- Voting
      lvr≡?          : Bool
      voteResCorrect : VoteResultCorrect pre post block lvr≡? r

  private
    contractBail : ∀ {pre block e} outs → OutputProps.NoMsgs outs → Contract pre block (Left e) pre outs
    contractBail{pre} outs noMsgs =
      mkContract
        reflPreservesRoundManagerInv
        (reflNoEpochChange{pre})
        noMsgs
        true reflVoteNotGenerated

  module continue2
    (voteProposal : VoteProposal) (validatorSigner : ValidatorSigner)
    (proposedBlock : Block)       (safetyData : SafetyData) where

    open constructAndSignVoteM-continue2 voteProposal validatorSigner proposedBlock safetyData

    record Requirements (pre : RoundManager) : Set where
      constructor mkRequirements
      field
        es≡₁  : (pre ^∙ pssSafetyData-rm) ≡L safetyData at sdEpoch
        es≡₂  : voteProposal ^∙ vpBlock ∙ bEpoch ≡ safetyData ^∙ sdEpoch
        lv≡  : (pre ^∙ pssSafetyData-rm) ≡L safetyData at sdLastVote
        lvr≡ : (pre ^∙ pssSafetyData-rm) ≡L safetyData at sdLastVotedRound
        vp≡pb : proposedBlock ≡ voteProposal ^∙ vpBlock

    contract'
      : ∀ pre
        → Requirements pre
        → LBFT-weakestPre
            (constructAndSignVoteM-continue2 voteProposal validatorSigner proposedBlock safetyData)
            (Contract pre proposedBlock) pre
    contract' pre reqs =
      verifyAndUpdateLastVoteRoundMSpec.contract (proposedBlock ^∙ bRound) safetyData
        (RWS-weakestPre-ebindPost unit step₁ (Contract pre proposedBlock)) pre
        contract-step₁
        (λ r≤lvr → contractBail _ refl)
      where
      module _ (r>lvr : proposedBlock ^∙ bRound > safetyData ^∙ sdLastVotedRound) where
        -- Shared definitions
        module _ where
          safetyData1 = verifyAndUpdateLastVoteRoundMSpec.safetyData' (proposedBlock ^∙ bRound) safetyData
          preUpdatedSD = pre & pssSafetyData-rm ∙~ safetyData1
          author = validatorSigner ^∙ vsAuthor

        -- State invariants
        module _ where
          bsip₁ : Preserves BlockStoreInv (rm→BlockStore-EC pre) (rm→BlockStore-EC preUpdatedSD)
          bsip₁ = id

          emP : Preserves EpochsMatch pre preUpdatedSD
          emP eq = trans eq (Requirements.es≡₁ reqs)

          srPre  = pre ^∙ lSafetyRules
          srPost = preUpdatedSD ^∙ lSafetyRules

          srP : Preserves SafetyRulesInv srPre srPost
          srP = mkPreservesSafetyRulesInv λ where (mkSafetyDataInv epoch≡ round≤) →
                                                    mkSafetyDataInv (epoch≡P epoch≡) (round≤P round≤)
            where
            epoch≡P : Preserves (λ sd → Meta.getLastVoteEpoch sd ≡ sd ^∙ sdEpoch)
                                (srPre ^∙ (srPersistentStorage ∙ pssSafetyData))
                                (srPost ^∙ (srPersistentStorage ∙ pssSafetyData))
            epoch≡P epoch≡
              rewrite sym (Requirements.lv≡  reqs)
              |       sym (Requirements.es≡₁ reqs)
              = epoch≡
            round≤P : Preserves (λ sd → Meta.getLastVoteRound sd ≤ sd ^∙ sdLastVotedRound)
                                (srPre ^∙ (srPersistentStorage ∙ pssSafetyData))
                                (srPost ^∙ (srPersistentStorage ∙ pssSafetyData))
            round≤P round≤
               with pre ^∙ pssSafetyData-rm ∙ sdLastVote
               |    inspect (_^∙ pssSafetyData-rm ∙ sdLastVote) pre
            ...| nothing | [ lv≡ ] rewrite (trans (sym (Requirements.lv≡ reqs)) lv≡) = z≤n
            ...| just x  | [ lv≡ ] rewrite (trans (sym (Requirements.lv≡ reqs)) lv≡) =
              ≤-trans round≤ (≤-trans (≡⇒≤ (Requirements.lvr≡ reqs)) (<⇒≤ r>lvr))

          invP₁ : Preserves RoundManagerInv pre preUpdatedSD
          invP₁ = mkPreservesRoundManagerInv id emP bsip₁ srP

        -- Some lemmas
        module _ where
          lvr<pbr : pre ^∙ pssSafetyData-rm ∙ sdLastVotedRound < proposedBlock ^∙ bRound
          lvr<pbr rewrite (Requirements.lvr≡ reqs) = r>lvr

          vpr≡pbr : (voteProposal ^∙ vpBlock) ≡L proposedBlock at bRound
          vpr≡pbr rewrite Requirements.vp≡pb reqs = refl

        bailAfterSetSafetyData : ∀ e → Contract pre proposedBlock (Left e) preUpdatedSD []
        bailAfterSetSafetyData e =
          mkContract invP₁ refl refl false (mkVoteNotGenerated (Requirements.lv≡ reqs) lvr<pbr)

        contract-step₁ : RWS-weakestPre-ebindPost unit step₁ (Contract pre proposedBlock) (Right _) pre []
        contract-step₂ : RWS-weakestPre-ebindPost unit (step₂ safetyData1) (Contract pre proposedBlock) (Right _) preUpdatedSD []

        contract-step₁ ._ refl ._ refl .unit refl =
          extensionCheckSpec.contract voteProposal
            (λ r → RWS-weakestPre-ebindPost unit (step₂ safetyData1) (Contract pre proposedBlock) r preUpdatedSD [])
            bailAfterSetSafetyData contract-step₂

        contract-step₂ voteData@._ refl =
          constructLedgerInfoMSpec.contract proposedBlock (hashVD voteData)
            (RWS-weakestPre-∙^∙Post unit (withErrCtx ("" ∷ []))
              (RWS-weakestPre-ebindPost unit (step₃ safetyData1 voteData author) (Contract pre proposedBlock))) preUpdatedSD
              (λ where .(Left fakeErr) refl → bailAfterSetSafetyData fakeErr)
              contract-step₃
          where
          contract-step₃
            : ∀ ledgerInfo
              → RWS-weakestPre-∙^∙Post unit (withErrCtx ("" ∷ []))
                  (RWS-weakestPre-ebindPost unit (step₃ safetyData1 _ author) (Contract pre proposedBlock))
                  (Right ledgerInfo) preUpdatedSD []
          contract-step₃ ledgerInfo ._ refl ._ refl ._ refl .unit refl unit refl =
            mkContract invP₂ refl refl false
              (Voting.mkVoteGeneratedCorrect
                (mkVoteGenerated refl
                  (inj₂ (mkVoteNewGenerated lvr<pbr vpr≡pbr)))
              voteFromBlock)
            where
            vote = Vote.newWithSignature voteData author ledgerInfo (ValidatorSigner.sign validatorSigner ledgerInfo)
            preUpdatedSD₂ = preUpdatedSD & pssSafetyData-rm ∙~ (safetyData1 & sdLastVote ?~ vote)

            pb≡vpb = sym (Requirements.vp≡pb reqs)

            voteFromBlock : Voting.VoteMadeFromBlock vote proposedBlock
            voteFromBlock =
              Voting.mkVoteMadeFromBlock
                (cong (_^∙ bEpoch) pb≡vpb) (cong (_^∙ bRound) pb≡vpb) (cong (_^∙ bId) pb≡vpb)

            -- State invariants
            module _ where
              bsiP₂ : Preserves BlockStoreInv (rm→BlockStore-EC pre) (rm→BlockStore-EC preUpdatedSD₂)
              bsiP₂ = id

              srP₂ : Preserves SafetyRulesInv (pre ^∙ lSafetyRules) (preUpdatedSD₂ ^∙ lSafetyRules)
              srP₂ = mkPreservesSafetyRulesInv
                       (const $ mkSafetyDataInv (Requirements.es≡₂ reqs) (≡⇒≤ (cong (_^∙ bRound) pb≡vpb)))

              invP₂ : Preserves RoundManagerInv pre preUpdatedSD₂
              invP₂ = mkPreservesRoundManagerInv id emP bsiP₂ srP₂

    contract
      : ∀ pre Post
        → Requirements pre
        → RWS-Post-⇒ (Contract pre proposedBlock) Post
        → LBFT-weakestPre
            (constructAndSignVoteM-continue2 voteProposal validatorSigner proposedBlock safetyData)
            Post pre
    contract pre Post reqs pf =
      LBFT-⇒ (constructAndSignVoteM-continue2 voteProposal validatorSigner proposedBlock safetyData)
             pre (contract' pre reqs) pf

  module continue1
    (voteProposal  : VoteProposal) (validatorSigner : ValidatorSigner)
    (proposedBlock : Block)        (safetyData0     : SafetyData) where

    open constructAndSignVoteM-continue1 voteProposal validatorSigner proposedBlock safetyData0

    record Requirements (pre : RoundManager) : Set where
      constructor mkRequirements
      field
        sd≡   : pre ^∙ pssSafetyData-rm ≡ safetyData0
        es≡   : voteProposal ^∙ vpBlock ∙ bEpoch ≡ safetyData0 ^∙ sdEpoch
        vp≡pb : proposedBlock ≡ voteProposal ^∙ vpBlock

    contract
      : ∀ pre → Requirements pre
        → LBFT-weakestPre (constructAndSignVoteM-continue1 voteProposal validatorSigner proposedBlock safetyData0)
            (Contract pre proposedBlock) pre
    contract pre reqs =
      verifyQcMSpec.contract (proposedBlock ^∙ bQuorumCert)
        (RWS-weakestPre-ebindPost unit (λ _ → step₁) (Contract pre proposedBlock)) pre
        (contractBail _ refl)
        contract-step₁
      where
      contract-step₁ : QuorumCertProps.Contract _ _ → RWS-weakestPre-ebindPost unit (const step₁) (Contract pre proposedBlock) (Right unit) pre []
      contract-step₁ qcCon ._ refl validatorVerifier@._ refl
        with Block.validateSignature proposedBlock validatorVerifier
      ... | Left e = contractBail _ refl
      ... | Right unit = λ where ._ refl → contract-step₃
        where
        contract-step₃ : RWS-weakestPre step₃ (Contract pre proposedBlock) unit pre
        contract-step₃ =
          LBFT-⇒ (verifyAndUpdatePreferredRoundM (proposedBlock ^∙ bQuorumCert) safetyData0) pre
            (verifyAndUpdatePreferredRoundMSpec.contract (proposedBlock ^∙ bQuorumCert) safetyData0 pre) pf-step₃
          -- verifyAndUpdatePreferredRoundMSpec.contract (proposedBlock ^∙ bQuorumCert) safetyData0
          --   Pred pre (λ r≤pr → contractBail _ refl) cases
            where
            VAUPContract = verifyAndUpdatePreferredRoundMSpec.Contract (proposedBlock ^∙ bQuorumCert) safetyData0
            Pred = RWS-weakestPre-ebindPost unit
                     (constructAndSignVoteM-continue2 voteProposal validatorSigner proposedBlock)
                     (Contract pre proposedBlock)

            reqs₁ : continue2.Requirements voteProposal validatorSigner proposedBlock safetyData0 pre
            reqs₁
              with Requirements.sd≡ reqs
            ...| refl = continue2.mkRequirements refl (Requirements.es≡ reqs) refl refl (Requirements.vp≡pb reqs)

            reqs₂ : continue2.Requirements voteProposal validatorSigner proposedBlock
                      (verifyAndUpdatePreferredRoundDefs.safetyData' (proposedBlock ^∙ bQuorumCert) safetyData0)
                      pre
            reqs₂
              with Requirements.sd≡ reqs
            ...| refl = continue2.mkRequirements refl (Requirements.es≡ reqs) refl refl (Requirements.vp≡pb reqs)

            pf-step₃ : ∀ r st outs → VAUPContract pre r st outs → Pred r st outs
            pf-step₃ r st outs (verifyAndUpdatePreferredRoundMSpec.mkContract noOuts refl condCorr) = pf r condCorr
              where
              pf-Con++outs : RWS-Post-⇒ (Contract pre proposedBlock) (RWS-Post++ (Contract pre proposedBlock) outs)
              pf-Con++outs r' st' outs' (mkContract rmInv noEpochChange noMsgOuts lvr≡? voteResCorrect) =
                mkContract rmInv noEpochChange (OutputProps.++-NoMsgs outs outs' noOuts noMsgOuts) lvr≡? voteResCorrect

              pf : (r : Either ErrLog SafetyData) (cc : verifyAndUpdatePreferredRoundMSpec.ConditionCorrect _ _ pre r) → Pred r st outs
              pf (Left e) tt = contractBail outs noOuts
              pf (Right .safetyData0) record { ep≡ = ep≡ ; qcr≤pr = qcr≤pr ; conds = (Left record { noUpd = refl }) } ._ refl =
                continue2.contract voteProposal validatorSigner proposedBlock safetyData0 pre
                  (RWS-Post++ (Contract pre proposedBlock) outs) reqs₁
                  pf-Con++outs
              pf (Right safetyData1@._) record { ep≡ = ep≡ ; qcr≤pr = qcr≤pr ; conds = (Right record { eff = refl }) } ._ refl =
                continue2.contract voteProposal validatorSigner proposedBlock safetyData1 pre
                  (RWS-Post++ (Contract pre proposedBlock) outs)
                  reqs₂ pf-Con++outs

  module continue0
    (voteProposal  : VoteProposal) (validatorSigner : ValidatorSigner) where

    open constructAndSignVoteM-continue0 voteProposal validatorSigner

    contract
      : ∀ pre
        → LBFT-weakestPre
            (constructAndSignVoteM-continue0 voteProposal validatorSigner) (Contract pre proposedBlock) pre
    contract pre safetyData0@._ refl =
      -- NOTE: There is a redundant check for this (that the proposal epoch
      -- matches the safety data epoch) in `LibraBFT.Impl.Consensus.Network`
      verifyEpochMSpec.contract (proposedBlock ^∙ bEpoch) safetyData0
        (RWS-weakestPre-ebindPost unit (const (step₁ safetyData0)) (Contract pre proposedBlock)) pre
        (λ e≢sde → contractBail _ refl)
        contract-step₁
      where
      module _ (e≡sde : proposedBlock ^∙ bEpoch ≡ pre ^∙ pssSafetyData-rm ∙ sdEpoch) where
        contract-step₁
          : RWS-weakestPre-ebindPost unit (const (step₁ safetyData0)) (Contract pre proposedBlock) (Right unit) pre []
        proj₁ (contract-step₁ .unit refl) ≡nothing =
          continue1.contract voteProposal validatorSigner proposedBlock safetyData0 pre
            (continue1.mkRequirements refl e≡sde refl)
        proj₁ (proj₂ (contract-step₁ .unit refl) vote vote≡) lvr≡pbr =
          mkContract reflPreservesRoundManagerInv (reflNoEpochChange{pre}) refl
            true (Voting.mkVoteGeneratedCorrect
                   (mkVoteGenerated (sym vote≡)
                     (inj₁ reflVoteOldGenerated))
                   (toWitnessT lvr≡pbr))
        proj₂ (proj₂ (contract-step₁ .unit refl) vote vote≡) lvr≢pbr =
          continue1.contract voteProposal validatorSigner proposedBlock safetyData0 pre
            (continue1.mkRequirements refl e≡sde refl)

  module _ (maybeSignedVoteProposal : MaybeSignedVoteProposal) where

    voteProposal  = maybeSignedVoteProposal ^∙ msvpVoteProposal
    proposedBlock = voteProposal ^∙ vpBlock

    contract'
      : ∀ pre
        → LBFT-weakestPre (constructAndSignVoteM maybeSignedVoteProposal) (Contract pre proposedBlock) pre
    contract' pre nothing vs≡ =
      mkContract
        reflPreservesRoundManagerInv (reflNoEpochChange{pre})
        refl true reflVoteNotGenerated
    contract' pre (just validatorSigner) vs≡ = continue0.contract voteProposal validatorSigner pre

    contract
      : ∀ pre Post → RWS-Post-⇒ (Contract pre proposedBlock) Post
        → LBFT-weakestPre (constructAndSignVoteM maybeSignedVoteProposal) Post pre
    contract pre Post pf =
      RWS-⇒ (constructAndSignVoteM maybeSignedVoteProposal) unit pre (contract' pre) pf

private
  module Tutorial
    (voteProposal : VoteProposal) (validatorSigner : ValidatorSigner)
    (proposedBlock : Block)       (safetyData : SafetyData) where

    -- After some experience with these proofs, it (allegedly)
    -- becomes fairly straightforward to let Agda do a lot of the
    -- work, and unfold the proof as we go.  However, it is
    -- important to understand what's going on under the hood to be
    -- able to reliably do this.  For the proof below, we do it in
    -- excruciating detail "by hand" in comments as an example to
    -- help ourselves understand.

    -- For this example, we will prove that `step₃` of (and old version of)
    -- `constructAndSignVoteM-continue2` produces no output.

    Contract : LBFT-Post (Either ErrLog Vote)
    Contract x post outs = outs ≡ []

    step₃ : SafetyData → VoteData → Author → LedgerInfo → LBFT (Either ErrLog Vote)
    step₃ safetyData1 voteData author ledgerInfo = do
      let signature = ValidatorSigner.sign validatorSigner ledgerInfo
          vote      = Vote.newWithSignature voteData author ledgerInfo signature
      pssSafetyData-rm ∙= (safetyData1 & sdLastVote ?~ vote)
      ok vote

    step₃-contract
      : ∀ pre safetyData1 voteData author ledgerInfo
        → LBFT-weakestPre
            (step₃ safetyData1 voteData author ledgerInfo)
            Contract pre
    step₃-contract pre safetyData1 voteData author ledgerInfo
    {-
    The proof can be as simple as this:

       = λ _ _ _ _ → refl

    Easy, right?!  Oh, you want a little more detail?  Sure here you go:

       = λ where .pre refl →
                  λ where .unit refl →
                           refl   -- Indenting important for parsing

    Still not crystal clear?  OK, let's explore in a little more detail.

    The initial goal looks like this:

    RWS-weakestPre-bindPost unit
      (λ st →
         RWS-put
         (LibraBFT.ImplShared.Consensus.Types.s st
          ((λ { F rf f (SafetyRules∙new v vv vvv)
                  → (rf Category.Functor.RawFunctor.<$>
                     (λ y' → SafetyRules∙new y' vv vvv))
                    (f v)
              })
           (λ x → x) Optics.Functorial.if
           ((λ { F rf f (PersistentSafetyStorage∙new v vv)
                   → (rf Category.Functor.RawFunctor.<$>
                      (λ y' → PersistentSafetyStorage∙new y' vv))
                     (f v)
               })
            (λ x → x) Optics.Functorial.if
            (λ _ →
               safetyData1 &
               sdLastVote ?~
               Vote.newWithSignature voteData author ledgerInfo
               (ValidatorSigner.sign validatorSigner ledgerInfo)))
           (LibraBFT.ImplShared.Consensus.Types.g st))))
      (RWS-weakestPre-bindPost unit
       (λ _ →
          RWS-return
          (inj₂
           (Vote.newWithSignature voteData author ledgerInfo
            (ValidatorSigner.sign validatorSigner ledgerInfo))))
       Contract)
      pre pre []

   It looks a bit ugly, but if we use C-u C-c C-, we get a more
   readable version that is exactly what we expect:

     LBFT-weakestPre (step₃ safetyData1 voteData author ledgerInfo)
                     Contract
                     pre

   Let's start refining by hand to understand.

   By desugaring the definition of "step₃ safetyData voteData author
   ledgerInfo" a bit, we can see that it is (using some shorthand in
   "quotes" to keep it concise at the expense of accuracy):

      (RWS-bind
         (RWS-bind
            (RWS-gets id)                                                                -- Fetch the state.
            (λ st → RWS-put (st & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote")))-- Modify the state returned by RWS-get.
         (λ _ → RWS-return (inj₂ "vote"))                                                -- The Unit returned by RWS-bind
                                                                                -- via RWS-put is ignored

      Note that "vote" is: Vote.newWithSignature voteData author ledgerInfo
                             (ValidatorSigner.sign validatorSigner ledgerInfo)

   Rewriting our goal with this yields (the annotations on the right
   show how we instantiate the rules in the next step):

     RWS-weakestPre
      (RWS-bind
         (RWS-bind                                                              = m
            (RWS-gets id)
            (λ st → RWS-put (st & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote")))
         (λ _ → RWS-return (inj₂ "vote"))                                       = f
      Contract                                                                   = P
      unit                                                                       = ev
      pre                                                                        = st

   Applying the definition of RWS-weakestPre (RWS-bind...), we need:

     RWS-weakestPre
       (RWS-bind
            (RWS-gets id)                                                                 = m
            (λ st → RWS-put (st & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))) = f
       (RWS-weakestPre-bindPost unit                                                      = P
         (λ _ → RWS-return (inj₂ vote))
         Contract)
       unit                                                                                = ev
       pre                                                                                = pre

   Applying the definition of RWS-weakestPre (RWS-bind...) again, we have:

     RWS-weakestPre
       (RWS-gets id)
       (RWS-weakestPre-bindPost unit                                            = P
         (λ st → RWS-put (st & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote")))
         (RWS-weakestPre-bindPost unit
           (λ _ → RWS-return (inj₂ vote))
           Contract))
       unit                                                                      = ev
       pre                                                                       = pre

   Now applying the definition of RWS-weakestPre RWS-gets, we want:

     (RWS-weakestPre-bindPost
         unit                                                                           = ev
         (λ st → RWS-put (st & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))) = f
         (RWS-weakestPre-bindPost unit                                                 = Post
           (λ _ → RWS-return (inj₂ "vote"))
           Contract))
       pre                                                                              = x
       pre                                                                              = post
       []                                                                               = outs

   Take a moment to compare this with our initial goal above.  They
   look identical, except for the shorthand.

   Next, we apply the definition of RWS-weakestPre-bindPost:

     ∀ r → r ≡ pre →
       RWS-weakestPre
         (RWS-put (r & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote")))
         (RWS-Post++
           (RWS-weakestPre-bindPost unit                                        = P
             (λ _ → RWS-return (inj₂ "vote"))
             Contract)
           [])                                                                   = outs
         unit
         pre

   Notice that our "f" (the put operation) is applied to the quantified variable
   "r". This is to reduce the size of the refined goal after substitution
   (instead of "pre", in general "r" could be equal to a much more complex expression).

   Applying the definition of RWS-Post++, we have:

     ∀ r → r ≡ pre →
       RWS-weakestPre
         (RWS-put (r & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote")))
         (λ x post outs₁ → (RWS-weakestPre-bindPost unit
                             (λ _ → RWS-return (inj₂ "vote"))
                             Contract) x post ([] ++ outs₁))
         unit
         pre

   Our proof begins by peeling of the two first parameters, the first
   of which must be pre, due to the second:

   -}

       = λ where .pre refl →

   {-

   At this point, our goal looks like (using C-u C-c C-,):

   RWS-weakestPre
      (RWS-put
       (over pssSafetyData-rm
        (λ _ →
           safetyData1 &
           sdLastVote ?~
           Vote.newWithSignature voteData author ledgerInfo
           (ValidatorSigner.sign validatorSigner ledgerInfo))
        pre))
      (λ x post outs₁ →
         RWS-weakestPre-bindPost unit
         (λ _ →
            RWS-return
            (inj₂
             (Vote.newWithSignature voteData author ledgerInfo
              (ValidatorSigner.sign validatorSigner ledgerInfo))))
         Contract x post ([] ++ outs₁))
      unit pre

   We can see that this is a more precise version of what we have above (without the shorthand),
   repeated here:

       RWS-weakestPre
         (RWS-put (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))) = post
         (λ x post outs₁ → (RWS-weakestPre-bindPost unit                         = P
                             (λ _ → RWS-return (inj₂ "vote"))
                             Contract) x post ([] ++ outs₁))
         unit
         pre

   Next, we apply the definition of RWS-weakestPre (RWS-put ...)

      (λ x post outs₁ → (RWS-weakestPre-bindPost unit
                          (λ _ → RWS-return (inj₂ "vote"))
                          Contract) x post ([] ++ outs₁))
      unit
      (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))
      []

    Instantiating,

      RWS-weakestPre-bindPost
       unit                                                                   = ev
       (λ _ → RWS-return (inj₂ "vote"))                                      = f
       Contract                                                               = Post
       unit                                                                   = x
       (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))          = post
       ([] ++ []))                                                            = outs

    Applying the definition of RWS-weakestPre-bindPost once again, we have:

      ∀ r → r ≡ unit → RWS-weakestPre
                         (RWS-return (inj₂ "vote"))
                         (RWS-Post++
                           Contract                                           = P
                           ([] ++ [])))                                       = outs
                         unit
                         (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))

    And applying the definition of RWS-Post++ yields:

      ∀ r → r ≡ unit → RWS-weakestPre
                         (RWS-return (inj₂ "vote"))
                         (λ x post outs₁ → Contract rm x post ([] ++ [] ++ outs₁))
                         unit
                         (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))

    Peeling off another couple of parameters (the first must be unit because of the second):
 -}

                      λ where .unit refl →

 {-

 The goal now looks like (using C-c C-,):

    Contract
      (inj₂
       (Vote.newWithSignature voteData author ledgerInfo
        (ValidatorSigner.sign validatorSigner ledgerInfo)))
      (LibraBFT.ImplShared.Consensus.Types.s pre
       ((λ { F rf f (SafetyRules∙new v vv vvv)
               → (rf Category.Functor.RawFunctor.<$>
                  (λ y' → SafetyRules∙new y' vv vvv))
                 (f v)
           })
        (λ x → x) Optics.Functorial.if
        ((λ { F rf f (PersistentSafetyStorage∙new v vv)
                → (rf Category.Functor.RawFunctor.<$>
                   (λ y' → PersistentSafetyStorage∙new y' vv))
                  (f v)
            })
         (λ x → x) Optics.Functorial.if
         (λ _ →
            safetyData1 &
            sdLastVote ?~
            Vote.newWithSignature voteData author ledgerInfo
            (ValidatorSigner.sign validatorSigner ledgerInfo)))
        (LibraBFT.ImplShared.Consensus.Types.g pre)))
      []

 Applying our shorthand, this yields:

    Contract
      (inj₂ "vote")
      (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))
      []

 Or (using C-u C-c C-,), we have the following goal:

    RWS-weakestPre
      (RWS-return
       (inj₂
        (Vote.newWithSignature voteData author ledgerInfo
         (ValidatorSigner.sign validatorSigner ledgerInfo))))
      (λ x post outs₁ → Contract x post (([] ++ []) ++ outs₁)) unit
      (over pssSafetyData-rm
       (λ _ →
          safetyData1 &
          sdLastVote ?~
          Vote.newWithSignature voteData author ledgerInfo
          (ValidatorSigner.sign validatorSigner ledgerInfo))
       pre)

 Applying our shorthand, this yields:

     RWS-weakestPre
       (RWS-return (inj₂ "vote"))                                       = x
       (λ x post outs₁ → Contract x post ([] ++ [] ++ outs₁))            = P
       unit                                                              = ev
       (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))     = pre

   Again, this looks like what we expect from above, so we can press
   on.  Now, applying the definition of RWS-weakestPre (RWS-return ...):

     (λ x post outs₁ → Contract x post ([] ++ [] ++ outs₁))
        (RWS-return (inj₂ "vote"))
        (pre & pssSafetyData-rm ∙~ ("safetyData1" & sdLastVote ?~ "vote"))
        []

   Finally, this reduces to the goal of:

     [] ≡ []

   which we prove with
   -}
                               refl