split lemma-union-not-used into lemma-exchange-maps

New type suggested by Janis Voigtländer.

2 files changed, 14 insertions, 12 deletions

diff --git a/Bidir.agda b/Bidir.agda
index b0469fd..790f9b9 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -148,17 +148,15 @@ lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma �
 lemma-<$>-just (just x) f<$>ma≡just-b = x , refl
 lemma-<$>-just nothing  ()
 
-lemma-union-not-used : {m n : ℕ} {A : Set} (h h' : FinMapMaybe n A) → (is : Vec (Fin n) m) → is in-domain-of h → map (flip lookupM (union h h')) is ≡ map (flip lookupM h) is
-lemma-union-not-used         h h' []        p = refl
-lemma-union-not-used {n = n} h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin
-      lookupM i (union h h')
-        ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h') (lookupM j h)) i ⟩
-      maybe′ just (lookupM i h') (lookupM i h)
-        ≡⟨ cong (maybe′ just (lookupM i h')) px ⟩
-      maybe′ just (lookupM i h') (just x)
-        ≡⟨ sym px ⟩
-      lookupM i h ∎)
-  (lemma-union-not-used h h' is' p')
+lemma-union-not-used : {n : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → (i : Fin n) → ∃ (λ x → lookupM i h ≡ just x) → lookupM i (union h h′) ≡ lookupM i h
+lemma-union-not-used h h′ i (x , px) = begin
+  lookupM i (union h h′)
+    ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h′) (lookupM j h)) i ⟩
+  maybe′ just (lookupM i h′) (lookupM i h)
+    ≡⟨ cong (maybe′ just (lookupM i h′)) px ⟩
+  maybe′ just (lookupM i h′) (just x)
+    ≡⟨ sym px ⟩
+  lookupM i h ∎
   where open ≡-Reasoning
 
 lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a
@@ -276,7 +274,7 @@ module _ (G : Get) where
     contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
       ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
     map (flip lookupM (h↦h′ h)) (contentV (get t))
-      ≡⟨ lemma-union-not-used h (reshape g′ (arityS (gl₁ j))) (contentV (get t)) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
+      ≡⟨ lemma-exchange-maps (lemma-union-not-used h (reshape g′ (arityS (gl₁ j)))) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
     map (flip lookupM h) (contentV (get t))
       ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
     map just (contentV v)
diff --git a/FinMap.agda b/FinMap.agda
index cbe24c5..ca7e73b 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -157,3 +157,7 @@ lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner
           maybe′ just (lookupM x (fromFunc f)) nothing
             ≡⟨ lemma-lookupM-fromFunc f x ⟩
           just (f x) ∎
+
+lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
+lemma-exchange-maps h≈h′ {[]}     All.[]         = refl
+lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)