abstract proofs over checkInsert

All proofs about expressions containing checkInsert share a common
pattern. There are three cases:
 1) Inserting a key-value-pair that is already present in the map.
 2) Inserting a new key into the map.
 3) Failure to insert a conflicting key-value pair in the map.

The checkInsertProof record enables to write three different cases
reducing the usage of "with" (and thus line length) in
lemma-checkInsert-restrict and lemma-lookupM-assoc.

1 files changed, 69 insertions, 19 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 163714a..0411ab6 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -7,11 +7,12 @@ open import Data.List using (List ; [] ; _∷_ ; map ; length)
 open import Data.List.Properties using (map-cong) renaming (map-compose to map-∘)
 open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec ; _∷_ to _∷V_)
 open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate)
+open import Data.Empty using (⊥-elim)
 open import Function using (id ; _∘_ ; flip)
-open import Relation.Nullary using (Dec ; yes ; no)
+open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.Core using (_≡_ ; refl)
-open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_ ; _≗_)
+open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_ ; _≗_ ; trans)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import FinMap
@@ -36,13 +37,54 @@ assoc _  []       []       = just empty
 assoc eq (i ∷ is) (b ∷ bs) = (assoc eq is bs) >>= (checkInsert eq i b)
 assoc _  _        _        = nothing
 
+record checkInsertProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (P : Set) : Set where
+  field
+     same : lookupM i m ≡ just x → P
+     new : lookupM i m ≡ nothing → P
+     wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x'  → P
+
+apply-checkInsertProof : {A P : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → checkInsertProof eq i x m P → P
+apply-checkInsertProof eq i x m rp with lookupM i m | inspect (lookupM i) m
+apply-checkInsertProof eq i x m rp | just x' | il with eq x x'
+apply-checkInsertProof eq i x m rp | just .x | Reveal_is_.[_] il | yes refl = checkInsertProof.same rp il
+apply-checkInsertProof eq i x m rp | just x' | Reveal_is_.[_] il | no x≢x' = checkInsertProof.wrong rp x' x≢x' il
+apply-checkInsertProof eq i x m rp | nothing | Reveal_is_.[_] il = checkInsertProof.new rp il
+
+lemma-checkInsert-same : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → lookupM i m ≡ just x → checkInsert eq i x m ≡ just m
+lemma-checkInsert-same eq i x m p with lookupM i m
+lemma-checkInsert-same eq i x m refl | .(just x) with eq x x
+lemma-checkInsert-same eq i x m refl | .(just x) | yes refl = refl
+lemma-checkInsert-same eq i x m refl | .(just x) | no x≢x = contradiction refl x≢x
+
+lemma-checkInsert-new : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → lookupM i m ≡ nothing → checkInsert eq i x m ≡ just (insert i x m)
+lemma-checkInsert-new eq i x m p with lookupM i m
+lemma-checkInsert-new eq i x m refl | .nothing = refl
+
+lemma-checkInsert-wrong : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → checkInsert eq i x m ≡ nothing
+lemma-checkInsert-wrong eq i x m x' d p with lookupM i m
+lemma-checkInsert-wrong eq i x m x' d refl | .(just x') with eq x x'
+lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | yes q = contradiction q d
+lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | no ¬q = refl
+
+record checkInsertEqualProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (e : Maybe (FinMapMaybe n A)) : Set where
+  field
+     same : lookupM i m ≡ just x → just m ≡ e
+     new : lookupM i m ≡ nothing → just (insert i x m) ≡ e
+     wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → nothing ≡ e
+
+lift-checkInsertProof : {A : Set} {n : ℕ} {eq : EqInst A} {i : Fin n} {x : A} {m : FinMapMaybe n A} {e : Maybe (FinMapMaybe n A)} → checkInsertEqualProof eq i x m e → checkInsertProof eq i x m (checkInsert eq i x m ≡ e)
+lift-checkInsertProof {_} {_} {eq} {i} {x} {m} o = record
+  { same  = λ p → trans (lemma-checkInsert-same eq i x m p) (checkInsertEqualProof.same o p)
+  ; new   = λ p → trans (lemma-checkInsert-new eq i x m p) (checkInsertEqualProof.new o p)
+  ; wrong = λ x' q p → trans (lemma-checkInsert-wrong eq i x m x' q p) (checkInsertEqualProof.wrong o x' q p)
+  }
+
 lemma-checkInsert-restrict : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (i : Fin n) → (is : List (Fin n)) → checkInsert eq i (f i) (restrict f is) ≡ just (restrict f (i ∷ is))
-lemma-checkInsert-restrict eq f i is with lookupM i (restrict f is) | inspect (lookupM i) (restrict f is)
-lemma-checkInsert-restrict eq f i is | nothing     | _ = refl
-lemma-checkInsert-restrict eq f i is | just x      | Reveal_is_.[_] prf with lemma-lookupM-restrict i f is x prf
-lemma-checkInsert-restrict eq f i is | just .(f i) | Reveal_is_.[_] prf | refl with eq (f i) (f i)
-lemma-checkInsert-restrict eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | yes refl = cong just (lemma-insert-same (restrict f is) i (f i) prf)
-lemma-checkInsert-restrict eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | no  ¬p   = contradiction refl ¬p
+lemma-checkInsert-restrict {τ} eq f i is = apply-checkInsertProof eq i (f i) (restrict f is) (lift-checkInsertProof record
+  { same  = λ lookupM≡justx → cong just (lemma-insert-same (restrict f is) i (f i) lookupM≡justx)
+  ; new   = λ lookupM≡nothing → refl
+  ; wrong = λ x' x≢x' lookupM≡justx' → contradiction (lemma-lookupM-restrict i f is x' lookupM≡justx') x≢x'
+  })
 
 lemma-1 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (restrict f is)
 lemma-1 eq f []        = refl
@@ -57,19 +99,27 @@ lemma-1 eq f (i ∷ is′) = begin
     ≡⟨ lemma-checkInsert-restrict eq f i is′ ⟩
   just (restrict f (i ∷ is′)) ∎
 
+lemma-just-nothing : {A : Set} → {a : A} → ¬ (_≡_ {_} {Maybe A} (just a) nothing)
+lemma-just-nothing ()
+
 lemma-lookupM-assoc : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (is : List (Fin n)) → (x : A) → (xs : List A) → (h : FinMapMaybe n A) → assoc eq (i ∷ is) (x ∷ xs) ≡ just h → lookupM i h ≡ just x
 lemma-lookupM-assoc eq i is x xs h    p with assoc eq is xs
-lemma-lookupM-assoc eq i is x xs h    ()   | nothing
-lemma-lookupM-assoc eq i is x xs h    p    | just h' with lookupM i h' | inspect (lookupM i) h'
-lemma-lookupM-assoc eq i is x xs .(insert i x h') refl | just h' | nothing | _ = lemma-lookupM-insert i x h'
-lemma-lookupM-assoc eq i is x xs h    p    | just h'   | just y  | _ with eq x y
-lemma-lookupM-assoc eq i is x xs h    ()   | just h'   | just y  | _ | no ¬prf
-lemma-lookupM-assoc eq i is x xs h    p    | just h'   | just .x | Reveal_is_.[_] p' | yes refl = begin
-  lookupM i h
-    ≡⟨ cong (lookupM i) (lemma-from-just (sym p)) ⟩
-  lookupM i h'
-    ≡⟨ p' ⟩
-  just x ∎
+lemma-lookupM-assoc eq i is x xs h    () | nothing
+lemma-lookupM-assoc eq i is x xs h    p | just h' = apply-checkInsertProof eq i x h' record
+  { same  = λ lookupM≡justx → begin
+      lookupM i h
+        ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym p) (lemma-checkInsert-same eq i x h' lookupM≡justx))) ⟩
+      lookupM i h'
+        ≡⟨ lookupM≡justx ⟩
+      just x ∎
+  ; new   = λ lookupM≡nothing → begin
+      lookupM i h
+        ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym p) (lemma-checkInsert-new eq i x h' lookupM≡nothing))) ⟩
+      lookupM i (insert i x h')
+        ≡⟨ lemma-lookupM-insert i x h' ⟩
+      just x ∎
+  ; wrong = λ x' x≢x' lookupM≡justx' → ⊥-elim (lemma-just-nothing (trans (sym p) (lemma-checkInsert-wrong eq i x h' x' x≢x' lookupM≡justx')))
+  }
 
 lemma-2 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (is : List (Fin n)) → (v : List τ) → (h : FinMapMaybe n τ) → assoc eq is v ≡ just h → map (flip lookupM h) is ≡ map just v
 lemma-2 eq []       []       h p = refl