rewrite lemma-map-lookupM-assoc

Indeed the usage of is in two different places can be disentangled. What
we need is that all lookupM succeed. We already know how to express
this: _in-domain-of_. So use a separate list js to map over and require
js in-domain-of h'. This is what the original proof actually did. Just
now we can drop ph' and therefore is and xs. Also
lemma-map-lookupM-insert vanishes, because this generalized form permits
direct induction.

1 files changed, 12 insertions, 20 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 4428bba..807105e 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -72,25 +72,17 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ |
     (lemma-assoc-domain is' xs' h' ph'))
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
-lemma-map-lookupM-insert : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (h : FinMapMaybe n Carrier) → i ∉ (toList is) → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is
-lemma-map-lookupM-insert i []         x h i∉is = refl
-lemma-map-lookupM-insert i (i' ∷ is') x h i∉is = cong₂ _∷_
-  (sym (lemma-lookupM-insert-other i' i x h (i∉is ∘ here ∘ sym)))
-  (lemma-map-lookupM-insert i is' x h (i∉is ∘ there))
-
-lemma-map-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → (h' : FinMapMaybe n Carrier) → assoc is xs ≡ just h' → checkInsert i x h' ≡ just h → map (flip lookupM h) is ≡ map (flip lookupM h') is
-lemma-map-lookupM-assoc i is x xs h h' ph' ph with any (_≟_ i) (toList is)
-lemma-map-lookupM-assoc i is x xs h h' ph' ph | yes p with Data.List.All.lookup (lemma-assoc-domain is xs h' ph') p
-lemma-map-lookupM-assoc i is x xs h h' ph' ph | yes p | (x'' , p') with lookupM i h' 
-lemma-map-lookupM-assoc i is x xs h h' ph' ph | yes p | (x'' , refl) | .(just x'') with deq x x''
-lemma-map-lookupM-assoc i is x xs h .h ph' refl | yes p | (.x , refl) | .(just x)  | yes refl = refl
-lemma-map-lookupM-assoc i is x xs h h' ph' () | yes p | (x'' , refl) | .(just x'') | no ¬p
-lemma-map-lookupM-assoc i is x xs h h' ph' ph | no ¬p rewrite lemma-∉-lookupM-assoc i is xs h' ph' ¬p = begin
-  map (flip lookupM h) is
-    ≡⟨ map-cong (λ i'' → cong (lookupM i'') (just-injective (sym ph))) is ⟩
-  map (flip lookupM (insert i x h')) is
-    ≡⟨ lemma-map-lookupM-insert i is x h' ¬p ⟩
-  map (flip lookupM h') is ∎
+lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → (h' : FinMapMaybe m Carrier) → checkInsert i x h' ≡ just h → {n : ℕ} → (js : Vec (Fin m) n) → (toList js) in-domain-of h' → map (flip lookupM h) js ≡ map (flip lookupM h') js
+lemma-map-lookupM-assoc i x h h' ph js pj with any (_≟_ i) (toList js)
+lemma-map-lookupM-assoc i x h h' ph js pj | yes p with Data.List.All.lookup pj p
+lemma-map-lookupM-assoc i x h h' ph js pj | yes p | x'' , p' with lookupM i h'
+lemma-map-lookupM-assoc i x h h' ph js pj | yes p | x'' , refl | .(just x'') with deq x x''
+lemma-map-lookupM-assoc i x h .h refl js pj | yes p | .x , refl | .(just x) | yes refl = refl
+lemma-map-lookupM-assoc i x h h' () js pj | yes p | x'' , refl | .(just x'') | no ¬p
+lemma-map-lookupM-assoc i x h h' ph [] pj | no ¬p = refl
+lemma-map-lookupM-assoc i x h h' ph (j ∷ js) pj | no ¬p = cong₂ _∷_
+  (sym (lemma-lookupM-checkInsert-other j i (¬p ∘ here ∘ sym) x h' h ph))
+  (lemma-map-lookupM-assoc i x h h' ph js (Data.List.All.tail pj))
 
 lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → map (flip lookupM h) is ≡ map just v
 lemma-2 []       []       h p = refl
@@ -105,7 +97,7 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
         ≡⟨ p ⟩
       just h ∎) ) ⟩
   just x ∷ map (flip lookupM h) is
-    ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i is x xs h h' ir p) ⟩
+    ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h h' p is (lemma-assoc-domain is xs h' ir)) ⟩
   just x ∷ map (flip lookupM h') is
     ≡⟨ cong (_∷_ (just x)) (lemma-2 is xs h' ir) ⟩
   just x ∷ map just xs ∎