add lemma-lookupM-fromFunc

The new lemma replaces two uses of lemma-fromFunc-tabulate, because the
latter exposes the implementation of FinMapMaybe, whereas the former
argues about the behaviour of FinMapMaybe. The aim of not exposing the
implementation (apart from brevity) is to enable refactoring.

2 files changed, 6 insertions, 6 deletions

diff --git a/Bidir.agda b/Bidir.agda
index e024aac..fae3b9e 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -142,9 +142,7 @@ theorem-1 G s = begin
   (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
   mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s)
-    ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩
-  mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s)
-    ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ denumerate s)) (enumerate s) ⟩
+    ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s) ⟩
   mapMV (Maybe.just ∘ denumerate s) (enumerate s)
     ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩
   just (map (denumerate s) (enumerate s))
diff --git a/FinMap.agda b/FinMap.agda
index 052ed6f..ce76f18 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -94,6 +94,10 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g →
 lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
 lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))
 
+lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ just ∘ f
+lemma-lookupM-fromFunc f zero = refl
+lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i
+
 lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (Maybe.just ∘ f)
 lemma-fromFunc-tabulate {zero}  f = refl
 lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc))
@@ -112,9 +116,7 @@ lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (s
             maybe′ just (lookupM x (fromFunc f)) (lookupM x empty)
               ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩
             lookupM x (fromFunc f)
-              ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩
-            lookupM x (tabulate (Maybe.just ∘ f))
-              ≡⟨ lookup∘tabulate (Maybe.just ∘ f) x ⟩
+              ≡⟨ lemma-lookupM-fromFunc f x ⟩
             just (f x) ∎
           lemma-inner (t ∷ ts) x with x ≟ t
           lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))