module fsbxia where

import Level
import Category.Functor
import Category.Monad

open import Function using (id)

open Function using (const)

open import Data.Nat using (ℕ ; zero ; suc)

open import Data.Fin using (Fin ; zero ; suc)

open import Data.List using (List ; [] ; _∷_)

open import Data.Vec using (Vec ; [] ; _∷_)
open Data.Vec using () renaming (_∷_ to _∷V_)

open Data.List using (length)

open Data.Vec using (lookup)

open import Relation.Binary.Core using (_≡_ ; refl)

open import Data.Empty using (⊥)

import Relation.Nullary
open Relation.Nullary using (¬_)

import Relation.Binary.Core
open Relation.Binary.Core using (_≢_)

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

FinMap : ℕ → Set → Set
FinMap m A = Vec A m

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

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

FinMapMaybe : ℕ → Set → Set
FinMapMaybe m A = Vec (Maybe A) m

empty : {m : ℕ} → {A : Set} → FinMapMaybe m A
empty {zero}   = []
empty {suc m}  = nothing ∷ empty

insert :  {m : ℕ} → {A : Set} → Fin m → A → FinMapMaybe m A →
          FinMapMaybe m A
insert zero     a (x ∷ xs) = just a ∷ xs
insert (suc i)  a (x ∷ xs) = x ∷ insert i a xs

open import Data.Product using (_×_ ; _,_)

fromAscList : {m : ℕ} → {A : Set} → List (Fin m × A) → FinMapMaybe m A
fromAscList []              = empty
fromAscList ((i , a) ∷ xs)  = insert i a (fromAscList xs)

open import Function using (_∘_)
open import Data.Vec using (tabulate)

open import Data.Maybe using () renaming (maybe′ to maybe)

union :  {m : ℕ} → {A : Set} → FinMapMaybe m A → FinMap m A →
         FinMap m A
union h₁ h₂ = tabulate (λ i → maybe id (lookup i h₂) (lookup i h₁))

open import Data.Bool using (Bool ; true ; false)
open import Relation.Nullary.Core using (Dec ; yes ; no)

postulate

  Carrier : Set
  deq : (b c : Carrier) → Dec (b ≡ c)

open import Data.Fin.Props using (_≟_)

checkInsert :  {m : ℕ} → Fin m → Carrier → FinMapMaybe m Carrier →
               Maybe (FinMapMaybe m Carrier)
checkInsert i b h  with lookup i h
...                | nothing = just (insert i b h)
...                | just c  with deq b c
...                          | yes b≡c  = just h
...                          | no b≢c   = nothing

open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
assoc :  {n m : ℕ} → Vec (Fin m) n → Vec Carrier n →
         Maybe (FinMapMaybe m Carrier)
assoc {zero}   []        []        = just empty
assoc {suc n}  (i ∷ is)  (b ∷ bs)  = assoc is bs >>= checkInsert i b

open import Data.Vec using () renaming (map to mapV)

open import Data.List using (zip) renaming (map to mapL)

restrict :  {A : Set} → {m : ℕ} → (Fin m → A) → List (Fin m) →
            FinMapMaybe m A
restrict f is = fromAscList (zip is (mapL f is))

open import Data.Vec using (toList)

lemma-1 :  {m n : ℕ} → (is : Vec (Fin m) n) → (f : Fin m → Carrier) →
           assoc is (mapV f is) ≡ just (restrict f (toList is))

open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)

import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality using (cong)

lemma-checkInsert-restrict : {m : ℕ} →
  (f : Fin m → Carrier) → (i : Fin m) → (is : List (Fin m)) →
  checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ is))

lemma-1 []        f = refl
lemma-1 (i ∷ is)  f = begin
  (assoc is (mapV f is) >>= checkInsert i (f i))
    ≡⟨ cong (λ h → h >>= checkInsert i (f i)) (lemma-1 is f) ⟩
  (just (restrict f (toList is)) >>= checkInsert i (f i))
    ≡⟨ refl ⟩
  checkInsert i (f i) (restrict f (toList is))
    ≡⟨ lemma-checkInsert-restrict f i (toList is) ⟩
  just (insert i (f i) (restrict f (toList is))) ∎

data InsertionResult {m : ℕ} (i : Fin m) (b : Carrier)
  (h : FinMapMaybe m Carrier) : Maybe (FinMapMaybe m Carrier) → Set where
  same   :  lookup i h ≡ just b → InsertionResult i b h (just h)
  new    :  lookup i h ≡ nothing → InsertionResult i b h (just (insert i b h))
  wrong  :  (c : Carrier) → b ≢ c → lookup i h ≡ just c →
            InsertionResult i b h nothing

insertionresult :  {m : ℕ} → (i : Fin m) → (b : Carrier) →
                   (h : FinMapMaybe m Carrier) →
                   InsertionResult i b h (checkInsert i b h)

open import Relation.Binary.PropositionalEquality using (inspect ; [_])

insertionresult i b h  with lookup i h  | inspect (lookup i) h
insertionresult i b h  | nothing        | [ p ] = new p
insertionresult i b h  | just c         | [ p ]  with deq b c
insertionresult i b h  | just c         | [ p ]  | no b≢c   = wrong c b≢c p

insertionresult i b h  | just .b        | [ p ]  | yes refl  = same p

lemma-insert-same :  {τ : Set} {m : ℕ} → (h : FinMapMaybe m τ) →
  (i : Fin m) → (a : τ) → lookup i h ≡ just a → h ≡ insert i a h

lemma-insert-same  []                        ()       a p
lemma-insert-same  (.        (just a) ∷ xs)  zero     a refl  = refl
lemma-insert-same  (x ∷ xs)                  (suc i)  a p     =
                   cong (_∷_ x) (lemma-insert-same xs i a p)

lemma-lookup-restrict : {A : Set} {m : ℕ} → (i : Fin m) → (f : Fin m → A) →
  (is : List (Fin m)) → (a : A) → lookup i (restrict f is) ≡ just a → f i ≡ a

lemma-lookup-empty : {A : Set} {m : ℕ} → (i : Fin m) →
  lookup {A = Maybe A} i empty ≡ nothing
lemma-lookup-insert : {A : Set} {m : ℕ} → (i : Fin m) → (a : A) →
  (h : FinMapMaybe m A) → lookup i (insert i a h) ≡ just a
lemma-lookup-insert-other : {A : Set} {m : ℕ} → (i j : Fin m) → (a : A) →
  (h : FinMapMaybe m A) → i ≢ j → lookup i h ≡ lookup i (insert j a h)

import Relation.Nullary.Negation
open Relation.Nullary.Negation using (contradiction)
lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing  → Whatever
lemma-just≢nothing refl ()

lemma-lookup-empty zero    = refl
lemma-lookup-empty (suc i) = lemma-lookup-empty i

just-injective : {A : Set} → {x y : A} → (Maybe.just x) ≡ (Maybe.just y) → x ≡ y
just-injective refl = refl

lemma-lookup-insert zero    a (x ∷ xs) = refl
lemma-lookup-insert (suc i) a (x ∷ xs) = lemma-lookup-insert i a xs

lemma-lookup-insert-other zero    zero    a h        p = contradiction refl p
lemma-lookup-insert-other zero    (suc j) a (x ∷ xs) p = refl
lemma-lookup-insert-other (suc i) zero    a (x ∷ xs) p = refl
lemma-lookup-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookup-insert-other i j a xs (p ∘ cong suc)

lemma-lookup-restrict i f []        a p = lemma-just≢nothing p (lemma-lookup-empty i)
lemma-lookup-restrict i f (i′ ∷ is) a p with i ≟ i′
lemma-lookup-restrict i f (.i ∷ is) a p | yes refl = just-injective (begin
   just (f i)
     ≡⟨ sym (lemma-lookup-insert i (f i) (restrict f is)) ⟩
   lookup i (insert i (f i) (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
lemma-lookup-restrict i f (i′ ∷ is) a p | no i≢i′ = lemma-lookup-restrict i f is a (begin
  lookup i (restrict f is)
    ≡⟨ lemma-lookup-insert-other i i′ (f i′) (restrict f is) i≢i′ ⟩
  lookup i (insert i′ (f i′) (restrict f is))
    ≡⟨ p ⟩
  just a ∎)

lemma-checkInsert-restrict f i is  with checkInsert i (f i) (restrict f is)
                                   | insertionresult i (f i) (restrict f is)
lemma-checkInsert-restrict f i is  | ._ | same p = cong just
                                   (lemma-insert-same _ i (f i) p)
lemma-checkInsert-restrict f i is  | ._ | new _ = refl
lemma-checkInsert-restrict f i is  | ._ | wrong c fi≢c p = contradiction
                                   (lemma-lookup-restrict i f is c p) fi≢c

open import Function using (flip)

lemma-2 : {m n : ℕ} → (is : Vec (Fin m) n) → (v : Vec Carrier n) →
  (h : FinMapMaybe m Carrier) → assoc is v ≡ just h →
  mapV (flip lookup h) is ≡ mapV just v

lemma-lookup-assoc :  {m n : ℕ} → (i : Fin m) → (is : Vec (Fin m) n) →
  (b : Carrier) → (bs : Vec Carrier n) → (h : FinMapMaybe m Carrier) →
  assoc (i ∷ is) (b ∷ bs) ≡ just h → lookup i h ≡ just b

lemma-lookup-assoc i is b bs h  p   with assoc is bs
lemma-lookup-assoc i is b bs h  ()   | nothing
lemma-lookup-assoc i is b bs h  p    | just h′ with checkInsert i b h′ | insertionresult i b h′
lemma-lookup-assoc i is b bs .h refl | just h  | ._ | same pl = pl
lemma-lookup-assoc i is b bs ._ refl | just h′ | ._ | new _   = lemma-lookup-insert i b h′
lemma-lookup-assoc i is b bs h  ()   | just h′ | ._ | wrong _ _ _

lemma-2-change-mapping : {m n : ℕ} → (i : Fin m) → (is : Vec (Fin m) n) →
  (b : Carrier) → (bs : Vec Carrier n) → (h : FinMapMaybe m Carrier) →
  (h′ : FinMapMaybe m Carrier) → assoc is bs ≡ just h′ →
  checkInsert i b h′ ≡ just h →
  mapV (flip lookup h) is ≡ mapV (flip lookup h′) is

lemma-2 []       []       h ph = refl
lemma-2 (i ∷ is) (b ∷ bs) h ph with assoc is bs | inspect (assoc is) bs
lemma-2 (i ∷ is) (b ∷ bs) h () | nothing        | [ ph′ ]

lemma-2 (i ∷ is) (b ∷ bs) h ph | just h′ | [ ph′ ] = begin
  lookup i h ∷ mapV (flip lookup h) is
    ≡⟨ cong  (flip _∷V_ (mapV (flip lookup h) is))
             (lemma-lookup-assoc i is b bs h origph) ⟩
  just b ∷ mapV (flip lookup h) is
    ≡⟨ cong (_∷_ (just b)) (lemma-2-change-mapping i is b bs h h′ ph′ ph) ⟩
  just b ∷ mapV (flip lookup h′) is
    ≡⟨ cong (_∷_ (just b)) (lemma-2 is bs h′ ph′) ⟩
  just b ∷ mapV just bs ∎
    where origph = trans (cong (flip _>>=_ (checkInsert i b)) ph′) ph

open import Data.List.All using (All ; [] ; _∷_)

open Data.List.All using () renaming (map to mapA)

open import Data.Product using (Σ ; _,_ ; proj₁ ; proj₂)

open Data.Product using (∃)

_in-domain-of_ :  {m : ℕ} → (is : List (Fin m)) → (FinMapMaybe m Carrier) →
                  Set
_in-domain-of_ is h = All (λ i → ∃ λ x → lookup i h ≡ just x) is

lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin m) n) →
  (bs : Vec Carrier n) → (h : FinMapMaybe m Carrier) → assoc is bs ≡ just h →
  (toList is) in-domain-of h

lemma-lookup-checkInsert : {m : ℕ} → (i j : Fin m) → (b c : Carrier) →
  (h h′ : FinMapMaybe m Carrier) → lookup i h ≡ just b →
  checkInsert j c h ≡ just h′ → lookup i h′ ≡ just b

lemma-lookup-checkInsert i j b c h h′ pl ph′ with checkInsert j c h | insertionresult j c h
lemma-lookup-checkInsert i j b c h .h pl refl | ._ | same _ = pl
lemma-lookup-checkInsert i j b c h h′ pl ph′  | ._ | new _ with i ≟ j
lemma-lookup-checkInsert i .i b c h h′ pl ph′ | ._ | new pl′ | yes refl = lemma-just≢nothing pl pl′
lemma-lookup-checkInsert i j b c h .(insert j c h) pl refl | ._ | new _ | no i≢j = begin
  lookup i (insert j c h)
    ≡⟨ sym (lemma-lookup-insert-other i j c h i≢j) ⟩
  lookup i h
    ≡⟨ pl ⟩
  just b ∎
lemma-lookup-checkInsert i j b c h h′ pl () | ._ | wrong _ _ _

lemma-assoc-domain []        []        h ph = []
lemma-assoc-domain (i ∷ is)  (b ∷ bs)  h ph  with assoc is bs  | inspect (assoc is) bs
lemma-assoc-domain (i ∷ is)  (b ∷ bs)  h ()  | nothing         | [ ph′ ]

lemma-assoc-domain (i ∷ is) (b ∷ bs) h    ph    | just h′ | [ ph′ ] with checkInsert i b h′
  | inspect (checkInsert i b) h′ | insertionresult i b h′
lemma-assoc-domain (i ∷ is) (b ∷ bs) h    ()    | just h′ | [ ph′ ] | ._
  | _       | wrong _ _ _
lemma-assoc-domain (i ∷ is) (b ∷ bs) .h′  refl  | just h′ | [ ph′ ] | ._
  | _       | same pl = (b , pl) ∷ (lemma-assoc-domain is bs h′ ph′)

lemma-assoc-domain (i ∷ is) (b ∷ bs) ._ refl | just h′ | [ ph′ ] | ._ | [ pc ]
  | new _ =  (b , lemma-lookup-insert i b h′) ∷
             (mapA
               (λ {j} p →  proj₁ p ,
                           lemma-lookup-checkInsert  j i (proj₁ p) b h′
                                                     (insert i b h′) (proj₂ p) pc)
               (lemma-assoc-domain is bs h′ ph′))

lemma-map-lookup-assoc : {m n : ℕ} → (i : Fin m) → (b : Carrier) →
  (h h′ : FinMapMaybe m Carrier) → checkInsert i b h′ ≡ just h →
  (js : Vec (Fin m) n) → (toList js) in-domain-of h′ →
  mapV (flip lookup h) js ≡ mapV (flip lookup h′) js

lemma-2-change-mapping i is b bs h h′ ph′ ph =
  lemma-map-lookup-assoc i b h h′ ph is (lemma-assoc-domain is bs h′ ph′)

open Relation.Binary.PropositionalEquality using (cong₂)

lemma-map-lookup-assoc i b h h′ ph []        pj = refl
lemma-map-lookup-assoc i b h h′ ph (j ∷ js)  ((c , pl) ∷ pj) = cong₂ _∷_
  (trans (lemma-lookup-checkInsert j i c b h′ h pl ph) (sym pl))
  (lemma-map-lookup-assoc i b h h′ ph js pj)

postulate
  free-theoremL : (get : {A : Set} → List A → List A) → {B C : Set} →
    (f : B → C) → (l : List B) → get (mapL f l) ≡ mapL f (get l)

open import Data.List using () renaming (replicate to replicateL)
open import Data.Unit using (tt)

getList-to-getlen : ({A : Set} → List A → List A) → ℕ → ℕ
getList-to-getlen get = length ∘ get ∘ flip replicateL tt

getList-length :  (get : {A : Set} → List A → List A) →
                  {B : Set} → (l : List B) →
                  length (get l) ≡ getList-to-getlen get (length l)

open import Data.List.Properties using (length-map)

replicate-length :  {A : Set} → (l : List A) →
                    mapL (const tt) l ≡ replicateL (length l) tt

replicate-length [] = refl
replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)

getList-length get l = begin
  length (get l)
    ≡⟨ sym (length-map (const tt) (get l)) ⟩
  length (mapL (const tt) (get l))
    ≡⟨ cong length (sym (free-theoremL get (const tt) l)) ⟩
  length (get (mapL (const tt) l))
    ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
  length (get (replicateL (length l) tt)) ∎

bff :  {getlen : ℕ → ℕ} →
       ({A : Set} → {n : ℕ} → Vec A n → Vec A (getlen n)) →
       {n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)

enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n
enumerate _ = tabulate id

denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
denumerate = flip lookup

lemma-map-denumerate-enumerate :  {n : ℕ} → (bs : Vec Carrier n) →
                                  mapV (denumerate bs) (enumerate bs) ≡ bs

open import Data.Vec.Properties using (map-∘ ; tabulate-∘)

lemma-map-denumerate-enumerate []       = refl
lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
  mapV (flip lookup (a ∷ as)) (tabulate suc)
    ≡⟨ cong (mapV (flip lookup (a ∷ as))) (tabulate-∘ suc id) ⟩
  mapV (flip lookup (a ∷ as)) (mapV suc (tabulate id))
    ≡⟨ refl ⟩
  mapV (flip lookup (a ∷ as)) (mapV suc (enumerate as))
    ≡⟨ sym (map-∘ _ _ (enumerate as)) ⟩
  mapV (flip lookup (a ∷ as) ∘ suc) (enumerate as)
    ≡⟨ refl ⟩
  mapV (denumerate as) (enumerate as)
    ≡⟨ lemma-map-denumerate-enumerate as ⟩
  as ∎)

open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)

bff get s v =  let  s′  = enumerate s
                    g   = tabulate (denumerate s)
                    h   = assoc (get s′) v
                    h′  = (flip union g) <$> h
               in (flip mapV s′ ∘ flip lookup) <$> h′

lemma-assoc-enough : {getlen : ℕ → ℕ} →
  (get : {A : Set} → {n : ℕ} → Vec A n → Vec A (getlen n)) →
  {n : ℕ} → (s : Vec Carrier n) → (v : Vec Carrier (getlen n)) →
  ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff get s v ≡ just u
lemma-assoc-enough get s v (h , p) =
    u , cong (_<$>_ (flip mapV s′ ∘ flip lookup) ∘ _<$>_ (flip union g)) p
    where  s′  = enumerate s
           g   = tabulate (denumerate s)
           u   = mapV (flip lookup (union h g)) s′

theorem-1 :  {getlen : ℕ → ℕ} →
             (get : {A : Set} → {n : ℕ} → Vec A n → Vec A (getlen n)) →
             {n : ℕ} → (s : Vec Carrier n) → bff get s (get s) ≡ just s

postulate
  free-theoremV : {getlen : ℕ → ℕ} →
    (get : {A : Set} → {n : ℕ} → Vec A n → Vec A (getlen n)) →
    {B C : Set} → (f : B → C) → {n : ℕ} → (l : Vec B n) →
    get (mapV f l) ≡ mapV f (get l)

lemma-union-restrict :  {m : ℕ} → {A : Set} →
                        (f : Fin m → A) → (is : List (Fin m)) →
                        union (restrict f is) (tabulate f) ≡ tabulate f

open Relation.Binary.PropositionalEquality using (_≗_)

open Data.Vec.Properties using (lookup∘tabulate ; map-cong)

theorem-1 get s =  let    h↦h′  = _<$>_ (flip union (tabulate (denumerate s)))
                          h′↦r  = _<$>_ (flip mapV (enumerate s) ∘ flip lookup)
                   in begin
  bff get s (get s)
    ≡⟨ cong (bff get s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
  bff get s (get (mapV (denumerate s) (enumerate s)))
    ≡⟨ cong (bff get s) (free-theoremV get (denumerate s) (enumerate s)) ⟩
  bff get s (mapV (denumerate s) (get (enumerate s)))
    ≡⟨ refl ⟩
  (h′↦r ∘ h↦h′) (assoc  (get (enumerate s))
                        (mapV (denumerate s) (get (enumerate s))))
    ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (get (enumerate s)) (denumerate s)) ⟩
  (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s))))
    ≡⟨ refl ⟩
  (h′↦r ∘ just) (union   (restrict (denumerate s) (toList (get (enumerate s))))
                         (tabulate (denumerate s)))
    ≡⟨ cong (h′↦r ∘ just) (lemma-union-restrict  (denumerate s)
                                                 (toList (get (enumerate s)))) ⟩
  (h′↦r ∘ just) (tabulate (denumerate s))
    ≡⟨ refl ⟩
  just (mapV (flip lookup (tabulate (denumerate s))) (enumerate s))
    ≡⟨ cong just (map-cong (lookup∘tabulate (denumerate s)) (enumerate s)) ⟩
  just (mapV (denumerate s) (enumerate s))
    ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
  just s ∎

lemma-tabulate-∘ : {m : ℕ} {A : Set} {f g : Fin m → A} →
  f ≗ g → tabulate f ≡ tabulate g

lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
lemma-tabulate-∘ {suc m} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))

lemma-union-restrict {m} f is = lemma-tabulate-∘ (lemma-inner is)
    where lemma-inner : (is : List (Fin m)) → (j : Fin m) → maybe id (lookup j (tabulate f)) (lookup j (restrict f is)) ≡ f j
          lemma-inner []       j = begin
            maybe id (lookup j (tabulate f)) (lookup j empty)
              ≡⟨ cong (maybe id (lookup j (tabulate f))) (lemma-lookup-empty j) ⟩
            maybe id (lookup j (tabulate f)) nothing
              ≡⟨ refl ⟩
            lookup j (tabulate f)
              ≡⟨ lookup∘tabulate f j ⟩
            f j ∎
          lemma-inner (i ∷ is)  j with j ≟ i
          lemma-inner (.j ∷ is) j | yes refl = cong (maybe id (lookup j (tabulate f)))
                                                    (lemma-lookup-insert j (f j) (restrict f is))
          lemma-inner (i ∷ is)  j | no j≢i = begin
            maybe id (lookup j (tabulate f)) (lookup j (insert i (f i) (restrict f is)))
              ≡⟨ cong (maybe id (lookup j (tabulate f))) (sym (lemma-lookup-insert-other j i (f i) (restrict f is) j≢i)) ⟩
            maybe id (lookup j (tabulate f)) (lookup j (restrict f is))
              ≡⟨ lemma-inner is j ⟩
            f j ∎

theorem-2 :  {getlen : ℕ → ℕ} →
             (get : {A : Set} → {n : ℕ} → Vec A n → Vec A (getlen n)) →
             {n : ℕ} → (s : Vec Carrier n) → (v : Vec Carrier (getlen n)) →
             (u : Vec Carrier n) → bff get s v ≡ just u → get u ≡ v

lemma-<$>-just :  {A B : Set} {f : A → B} {b : B} {ma : Maybe A} →
                  f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
lemma-<$>-just {ma = just x}   _ = x , refl
lemma-<$>-just {ma = nothing}  ()

lemma-union-not-used : {m n : ℕ} (h : FinMapMaybe m Carrier) →
  (g : FinMap m Carrier)
  (is : Vec (Fin m) n) → (toList is) in-domain-of h →
  mapV just (mapV (flip lookup (union h g)) is) ≡ mapV (flip lookup h) is

lemma-union-not-used h h′ []        p = refl
lemma-union-not-used h h′ (i ∷ is′) (All._∷_ (b , pb) p′) = cong₂ _∷_ (begin
      just (lookup i (union h h′))
        ≡⟨ cong just (lookup∘tabulate (λ j → maybe id (lookup j h′) (lookup j h)) i) ⟩
      just (maybe id (lookup i h′) (lookup i h))
        ≡⟨ cong just (cong (maybe id (lookup i h′)) pb) ⟩
      just (maybe id (lookup i h′) (just b))
        ≡⟨ sym pb ⟩
      lookup i h ∎)
  (lemma-union-not-used h h′ is′ p′)

map-just-injective :  {A : Set} {n : ℕ} {xs ys : Vec A n} →
                      mapV Maybe.just xs ≡ mapV Maybe.just ys → xs ≡ ys

∷-injective : {A : Set} {n : ℕ} {x y : A} {xs ys : Vec A n} → (x ∷V xs) ≡ (y ∷V ys) → x ≡ y × xs ≡ ys
∷-injective refl = refl , refl

map-just-injective {xs = []}      {ys = []}       p  = refl
map-just-injective {xs = x ∷ xs′} {ys = y ∷ ys′}  p with ∷-injective p
map-just-injective {xs = x ∷ xs′} {ys = .x ∷ ys′} p | refl , p′ = cong (_∷_ x) (map-just-injective p′)

theorem-2 get s v u p with lemma-<$>-just (proj₂ (lemma-<$>-just p))
theorem-2 get s v u p | h , ph =  let  s′    = enumerate s
                                       g     = tabulate (denumerate s)
                                       h↦h′  = flip union g
                                       h′↦r  = flip mapV s′ ∘ flip lookup
                                  in begin
  get u
    ≡⟨ just-injective (begin
      get <$> (just u)
        ≡⟨ cong (_<$>_ get) (sym p) ⟩
      get <$> (bff get s v)
        ≡⟨ cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
      get <$> (h′↦r <$> (h↦h′ <$> just h)) ∎) ⟩
  get (mapV (flip lookup (h↦h′ h)) s′)
    ≡⟨ free-theoremV get (flip lookup (h↦h′ h)) s′ ⟩
  mapV (flip lookup (h↦h′ h)) (get s′)
     ≡⟨ map-just-injective (begin
       mapV just (mapV (flip lookup (union h g)) (get s′))
         ≡⟨ lemma-union-not-used   h g (get s′)
                                   (lemma-assoc-domain (get s′) v h ph) ⟩
       mapV (flip lookup h) (get s′)
         ≡⟨ lemma-2 (get s′) v h ph ⟩
       mapV just v
         ∎) ⟩
  v ∎

import Data.List.Any
open Data.List.Any using (Any ; here ; there)

open Data.List.Any.Membership-≡ using (_∈_ ; _∉_)

data All-different {A : Set} : List A → Set where
  different-[]  :  All-different []
  different-∷   :  {x : A} {xs : List A} →
                   x ∉ xs → All-different xs → All-different (x ∷ xs)

different-assoc :  {m n : ℕ} → (u : Vec (Fin m) n) → (v : Vec Carrier n) →
                   All-different (toList u) → ∃ λ h → assoc u v ≡ just h

lemma-checkInsert-new : {m : ℕ} → (i : Fin m) → (b : Carrier) →
  (h : FinMapMaybe m Carrier) → lookup i h ≡ nothing →
  checkInsert i b h ≡ just (insert i b h)

lemma-checkInsert-new i b h p with lookup i h
lemma-checkInsert-new i b h refl | ._ = refl

lemma-∉-lookup-assoc : {m n : ℕ} → (i : Fin m) → (is : Vec (Fin m) n) →
  (bs : Vec Carrier n) → (h : FinMapMaybe m Carrier) →
  assoc is bs ≡ just h → (i ∉ toList is) → lookup i h ≡ nothing

different-assoc  []        []        _ = empty , refl
different-assoc  (u ∷ us)  (v ∷ vs)  (different-∷ u∉us diff-us)
                 with different-assoc us vs diff-us
different-assoc  (u ∷ us)  (v ∷ vs)  (different-∷ u∉us diff-us)
                 | h , p = insert u v h , (begin
  (assoc us vs >>= checkInsert u v)
    ≡⟨ cong (flip _>>=_ (checkInsert u v)) p ⟩
  checkInsert u v h
    ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookup-assoc u us vs h p u∉us) ⟩
  just (insert u v h) ∎)

lemma-lookup-checkInsert-other : {m : ℕ} → (i j : Fin m) → i ≢ j →
  (b : Carrier) → (h h′ : FinMapMaybe m Carrier) → checkInsert j b h ≡ just h′ →
  lookup i h ≡ lookup i h′

lemma-lookup-checkInsert-other i j i≢j b h h′ ph′ with lookup j h
lemma-lookup-checkInsert-other i j i≢j b h h′ ph′ | just c with deq b c
lemma-lookup-checkInsert-other i j i≢j b h .h refl | just .b | yes refl = refl
lemma-lookup-checkInsert-other i j i≢j b h h′ () | just c | no b≢c
lemma-lookup-checkInsert-other i j i≢j b h .(insert j b h) refl | nothing = lemma-lookup-insert-other i j b h i≢j

lemma-∉-lookup-assoc  i []          []          .empty  refl  i∉is
                      = lemma-lookup-empty i
lemma-∉-lookup-assoc  i (i′ ∷ is′)  (b′ ∷ bs′)  h       ph    i∉is
                      with assoc is′ bs′  | inspect (assoc is′) bs′
lemma-∉-lookup-assoc  i (i′ ∷ is′)  (b′ ∷ bs′)  h       ()    i∉is
                      | nothing           | [ ph′ ]
lemma-∉-lookup-assoc  i (i′ ∷ is′)  (b′ ∷ bs′)  h       ph    i∉is
                      | just h′           | [ ph′ ] = begin
  lookup i h
    ≡⟨ sym (lemma-lookup-checkInsert-other i i′ (i∉is ∘ here) b′ h′ h ph) ⟩
  lookup i h′
    ≡⟨ lemma-∉-lookup-assoc i is′ bs′ h′ ph′ (i∉is ∘ there) ⟩
  nothing ∎