cleanup unused functions and useless steps

3 files changed, 11 insertions, 35 deletions

diff --git a/Bidir.agda b/Bidir.agda
index eef8bff..05ee066 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -22,7 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
+open import Generic using (just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
 open import FinMap
 import CheckInsert
 open CheckInsert Carrier deq
@@ -150,14 +150,6 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma
 lemma->>=-just (just a) p = a , refl
 lemma->>=-just nothing  ()
 
-lemma-mapMV-just : {A B : Set} {n : ℕ} {f : A → Maybe B} {s : Vec A n} {v : Vec B n} → mapMV f s ≡ just v → All (λ x → ∃ λ y → f x ≡ just y) (toList s)
-lemma-mapMV-just         {s = []}     p = Data.List.All.[]
-lemma-mapMV-just {f = f} {s = x ∷ xs} p with f x | inspect f x
-lemma-mapMV-just         {s = x ∷ xs} () | nothing | _
-lemma-mapMV-just {f = f} {s = x ∷ xs} p  | just y  | [ py ] with mapMV f xs | inspect (mapMV f) xs
-lemma-mapMV-just         {s = x ∷ xs} () | just y  | [ py ] | nothing | _
-lemma-mapMV-just         {s = x ∷ xs} p  | just y  | [ py ] | just ys | [ pys ] = (y , py) Data.List.All.∷ (lemma-mapMV-just pys)
-
 lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
 lemma-just-sequence [] = refl
 lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl
diff --git a/Generic.agda b/Generic.agda
index 2ef374c..4e55c21 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -15,10 +15,6 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ;
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 
-∷-injective : {A : Set} {n : ℕ} {x y : A} {xs ys : Vec A n} →
-              (x ∷V xs) ≡ (y ∷V ys) → x ≡ y × xs ≡ ys
-∷-injective refl = refl , refl
-
 just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
 just-injective refl = refl
 
@@ -26,12 +22,6 @@ length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) �
 length-replicate zero    = refl
 length-replicate (suc n) = cong suc (length-replicate n)
 
-map-just-injective : {A : Set} {n : ℕ} {xs ys : Vec A n} →
-                     map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys
-map-just-injective {xs = []V}      {ys = []V}       p  = refl
-map-just-injective {xs = x ∷V xs′} {ys = y ∷V ys′}  p with ∷-injective p
-map-just-injective {xs = x ∷V xs′} {ys = .x ∷V ys′} p | refl , p′ = cong (_∷V_ x) (map-just-injective p′)
-
 mapMV : {A B : Set} {n : ℕ} → (A → Maybe B) → Vec A n → Maybe (Vec B n)
 mapMV f []V = just []V
 mapMV f (x ∷V xs) = (f x) >>= (λ y → (_∷V_ y) <$> (mapMV f xs))
diff --git a/Precond.agda b/Precond.agda
index 90027b4..6aba291 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -18,7 +18,7 @@ import Data.List.All
 open import Data.List.Any using (here ; there)
 open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
-open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
+open import Data.Product using (∃ ; _,_ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
@@ -37,9 +37,6 @@ lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup
 lemma-lookup-map-just zero    (x ∷ xs) = refl
 lemma-lookup-map-just (suc f) (x ∷ xs) = lemma-lookup-map-just f xs
 
-fromMaybe : {A : Set} → A → Maybe A → A
-fromMaybe a ma = maybe′ id a ma
-
 lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
 lemma-maybe-just a (just x) = refl
 lemma-maybe-just a nothing = refl
@@ -52,16 +49,13 @@ lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
         ≡⟨ cong (flip (maybe′ just) (lookup f h)) (lemma-lookup-map-just f g) ⟩
       maybe′ just (just (lookup f g)) (lookup f h)
         ≡⟨ lemma-maybe-just (lookup f g) (lookup f h) ⟩
-      just (fromMaybe (lookup f g) (lookup f h)) ∎) ⟩
-  tabulate (λ f → just (fromMaybe (lookup f g) (lookup f h)))
-    ≡⟨ tabulate-∘ just (λ f → fromMaybe (lookup f g) (lookup f h)) ⟩
-  map just (tabulate (λ f → fromMaybe (lookup f g) (lookup f h))) ∎)
-lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List.All.∷ ps) = _ , (begin
+      just (maybe′ id (lookup f g) (lookup f h)) ∎) ⟩
+  tabulate (λ f → just (maybe′ id (lookup f g) (lookup f h)))
+    ≡⟨ tabulate-∘ just (λ f → maybe′ id (lookup f g) (lookup f h)) ⟩
+  map just (tabulate (λ f → maybe′ id (lookup f g) (lookup f h))) ∎)
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Data.List.All.∷ ps) = _ , (begin
   union h (delete i (delete-many is (map just g)))
-    ≡⟨ lemma-tabulate-∘ (λ f → (begin
-      maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h)
-        ≡⟨ inner f ⟩
-      maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) ∎)) ⟩
+    ≡⟨ lemma-tabulate-∘ inner ⟩
   union h (delete-many is (map just g))
     ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
   map just _ ∎)
@@ -69,9 +63,9 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List
         inner f with f ≟ i
         inner .i | yes refl = begin
           maybe′ just (lookupM i (delete i (delete-many is (map just g)))) (lookup i h)
-            ≡⟨ cong (maybe′ just _) (proj₂ p) ⟩
-          just (proj₁ p)
-            ≡⟨ cong (maybe′ just _) (sym (proj₂ p)) ⟩
+            ≡⟨ cong (maybe′ just _) px ⟩
+          just x
+            ≡⟨ cong (maybe′ just _) (sym px) ⟩
           maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i)