From c9ddcf0abbb2e82eafc6dc24872244374c4f43c2 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 7 Feb 2014 18:32:54 +0100 Subject: replace rewrite with cong where feasible --- Generic.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Generic.agda') diff --git a/Generic.agda b/Generic.agda index 748a49a..b1ab8dd 100644 --- a/Generic.agda +++ b/Generic.agda @@ -37,8 +37,8 @@ mapMV-cong f≗g (x ∷V xs) | just y | .(just y) | refl = cong (_<$>_ (_∷V_ y mapMV-cong f≗g (x ∷V xs) | nothing | .nothing | refl = refl mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v) -mapMV-purity f []V = refl -mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl +mapMV-purity f []V = refl +mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs) maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (PropEq A) ∋ a ≈ b maybeEq-from-≡ {a = just x} {b = .(just x)} refl = just refl -- cgit v1.2.3 From 0a1558b7cb0bccbe4a8c8411ac08d11a87547eea Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 7 Feb 2014 18:55:23 +0100 Subject: eliminate useless withs --- FinMap.agda | 3 +-- Generic.agda | 10 ++++------ 2 files changed, 5 insertions(+), 8 deletions(-) (limited to 'Generic.agda') diff --git a/FinMap.agda b/FinMap.agda index ce76f18..c46e637 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -103,8 +103,7 @@ lemma-fromFunc-tabulate {zero} f = refl lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc)) lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f -lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p with p refl -... | () +lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction refl p 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) diff --git a/Generic.agda b/Generic.agda index b1ab8dd..b29f47d 100644 --- a/Generic.agda +++ b/Generic.agda @@ -8,12 +8,12 @@ open import Data.Nat using (ℕ ; zero ; suc) open import Data.Product using (_×_ ; _,_) open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) open import Data.Vec.Equality using () renaming (module Equality to VecEq) -open import Function using (_∘_ ; id) +open import Function using (_∘_ ; id ; flip) open import Level using () renaming (zero to ℓ₀) open import Relation.Binary using (Setoid ; module Setoid) open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to PropEq) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans ; cong₂) renaming (setoid to PropEq) open Setoid using () renaming (_≈_ to _∋_≈_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) @@ -31,10 +31,8 @@ mapMV f []V = just []V mapMV f (x ∷V xs) = (f x) >>= (λ y → (_∷V_ y) <$> (mapMV f xs)) mapMV-cong : {A B : Set} {f g : A → Maybe B} → f ≗ g → {n : ℕ} → mapMV {n = n} f ≗ mapMV g -mapMV-cong f≗g []V = refl -mapMV-cong {f = f} {g = g} f≗g (x ∷V xs) with f x | g x | f≗g x -mapMV-cong f≗g (x ∷V xs) | just y | .(just y) | refl = cong (_<$>_ (_∷V_ y)) (mapMV-cong f≗g xs) -mapMV-cong f≗g (x ∷V xs) | nothing | .nothing | refl = refl +mapMV-cong f≗g []V = refl +mapMV-cong f≗g (x ∷V xs) = cong₂ _>>=_ (f≗g x) (cong (flip (_<$>_ ∘ _∷V_)) (mapMV-cong f≗g xs)) mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v) mapMV-purity f []V = refl -- cgit v1.2.3