rewrite lemma-disjoint-union in a more compositional way

1 files changed, 55 insertions, 26 deletions

diff --git a/FinMap.agda b/FinMap.agda
index b4441f5..cbe24c5 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -2,24 +2,41 @@ module FinMap where
 
 open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ ; zero ; suc)
-open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) renaming (setoid to MaybeEq)
+open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
 open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Properties using (_≟_)
-open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip) renaming (lookup to lookupVec ; map to mapV)
+open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
 open import Data.Vec.Equality using ()
-open Data.Vec.Equality.Equality using (_∷-cong_)
-open import Data.Vec.Properties using (lookup∘tabulate)
 open import Data.Product using (_×_ ; _,_)
+open import Data.List.All as All using (All)
+import Data.List.All.Properties as AllP
+import Data.List.Any as Any
 open import Function using (id ; _∘_ ; flip ; const)
+open import Function.Equality using (module Π)
+open import Function.Surjection using (module Surjection)
 open import Relation.Nullary using (yes ; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary using (Setoid ; module Setoid)
-open import Relation.Binary.Core using (_≡_ ; refl ; _≢_)
-open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans ; cong₂)
-open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Binary.Core using (_≡_ ; refl ; _≢_ ; Decidable)
+open import Relation.Binary.PropositionalEquality as P using (cong ; sym ; _≗_ ; trans ; cong₂)
+open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import Generic using (just-injective)
 
+_∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set
+_∈_ {A} x xs = Any.Membership._∈_ (P.setoid A) x (toList xs)
+
+_∉_ : {A : Set} {n : ℕ} → A → Vec A n → Set
+_∉_ {A} x xs = All (_≢_ x) (toList xs)
+
+data Dec∈ {A : Set} {n : ℕ} (x : A) (xs : Vec A n) : Set where
+  yes-∈ : x ∈ xs → Dec∈ x xs
+  no-∉ : x ∉ xs → Dec∈ x xs
+
+is-∈ : {A : Set} {n : ℕ} → Decidable (_≡_ {A = A}) → (x : A) → (xs : Vec A n) → Dec∈ x xs
+is-∈ eq? x xs with Any.any (eq? x) (toList xs)
+...     | yes x∈xs = yes-∈ x∈xs
+...     | no  x∉xs = no-∉ (Π._⟨$⟩_ (Surjection.to AllP.¬Any↠All¬) x∉xs)
+
 FinMapMaybe : ℕ → Set → Set
 FinMapMaybe n A = Vec (Maybe A) n
 
@@ -90,6 +107,20 @@ lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restric
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
+lemma-lookupM-restrict-∈ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∈ js → lookupM i (restrict f js) ≡ just (f i)
+lemma-lookupM-restrict-∈ i f [] ()
+lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
+lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes refl = lemma-lookupM-insert i (f i) (restrict f js)
+lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
+lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p)  | no i≢j =
+  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) i≢j)
+        (lemma-lookupM-restrict-∈ i f js p)
+
+lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
+lemma-lookupM-restrict-∉ i f []       i∉[]  = lemma-lookupM-empty i
+lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
+  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) (All.head i∉jjs))
+        (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
 
 lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
 lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
@@ -105,26 +136,24 @@ lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
 lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = refl
 lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc)
 
+lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h
+lemma-lookupM-delete-many {n} h i []       i∉[]  = refl
+lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs =
+  trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs))
+        (lemma-lookupM-delete-many h i js (All.tail i∉jjs))
+
 lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m
 lemma-reshape-id []       = refl
 lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs)
 
 lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f
-lemma-disjoint-union {n} {m} f t = lemma-tabulate-∘ (lemma-inner t)
-    where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x)
-          lemma-inner [] x = begin
-            maybe′ just (lookupM x (fromFunc f)) (lookupM x empty)
-              ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩
-            lookupM x (fromFunc f)
-              ≡⟨ 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 ts))
-          lemma-inner (t ∷ ts) x | no ¬p = begin
-            maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (t ∷ ts)))
-              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (lemma-lookupM-insert-other x t (f t) (restrict f ts) ¬p) ⟩
-            maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f ts))
-              ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f ts))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩
-            maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f ts))
-              ≡⟨ lemma-inner ts x ⟩
-            just (f x) ∎
+lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner
+  where inner : (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t)) ≡ just (f x)
+        inner x with is-∈ _≟_ x t
+        inner x | yes-∈ x∈t = cong (maybe′ just (lookupM x (delete-many t (fromFunc f)))) (lemma-lookupM-restrict-∈ x f t x∈t)
+        inner x | no-∉ x∉t = begin
+          maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f t))
+            ≡⟨ cong₂ (maybe′ just) (lemma-lookupM-delete-many (fromFunc f) x t x∉t) (lemma-lookupM-restrict-∉ x f t x∉t) ⟩
+          maybe′ just (lookupM x (fromFunc f)) nothing
+            ≡⟨ lemma-lookupM-fromFunc f x ⟩
+          just (f x) ∎