From 71025b5f1d0a11b0cf373192210b293a77d45c04 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 27 Jan 2014 09:31:56 +0100 Subject: cleanup unused functions and useless steps --- Bidir.agda | 10 +--------- Generic.agda | 10 ---------- Precond.agda | 26 ++++++++++---------------- 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) -- cgit v1.2.3