From c835e655a05c73f7dd2dc46c652be3d43e91a4b7 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 25 Nov 2018 10:35:23 +0100 Subject: reorganize equality imports Since we are working with multiple setoids now, it makes more sense to qualify their members. Follow the "as P" pattern from the standard library. Also stop importing those symbols from Relation.Binary.Core as later agda-stdlib versions will move them away. Rather than EqSetoid or PropEq, use P.setoid consistently. --- FinMap.agda | 60 ++++++++++++++++++++++++++++++------------------------------ 1 file changed, 30 insertions(+), 30 deletions(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index 8322b79..57d3ecf 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -18,8 +18,8 @@ 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.Core using (_≡_ ; refl ; _≢_ ; Decidable) -open import Relation.Binary.PropositionalEquality as P using (cong ; sym ; _≗_ ; trans ; cong₂) +open import Relation.Binary.Core using (Decidable) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_) open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Generic using (just-injective) @@ -77,79 +77,79 @@ delete-many = flip (foldr (const _) delete) lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m lemma-insert-same [] () p -lemma-insert-same {suc n} (x ∷ xs) zero p = cong (flip _∷_ xs) p -lemma-insert-same (x ∷ xs) (suc i) p = cong (_∷_ x) (lemma-insert-same xs i p) +lemma-insert-same {suc n} (x ∷ xs) zero p = P.cong (flip _∷_ xs) p +lemma-insert-same (x ∷ xs) (suc i) p = P.cong (_∷_ x) (lemma-insert-same xs i p) lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing -lemma-lookupM-empty zero = refl +lemma-lookupM-empty zero = P.refl lemma-lookupM-empty (suc i) = lemma-lookupM-empty i lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a -lemma-lookupM-restrict i f [] p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ()) +lemma-lookupM-restrict i f [] p = contradiction (P.trans (P.sym p) (lemma-lookupM-empty i)) (λ ()) lemma-lookupM-restrict i f (i' ∷ is) p with i ≟ i' -lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin +lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes P.refl = just-injective (begin just (f i) - ≡⟨ sym (lookup∘update i (restrict f is) (just (f i))) ⟩ + ≡⟨ P.sym (lookup∘update i (restrict f is) (just (f i))) ⟩ lookupM i (insert i (f i) (restrict f is)) ≡⟨ p ⟩ just a ∎) lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin lookupM i (restrict f is) - ≡⟨ sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩ + ≡⟨ P.sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩ 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 = lookup∘update i (restrict f js) (just (f i)) +lemma-lookupM-restrict-∈ i f (.i ∷ js) p | yes P.refl = lookup∘update i (restrict f js) (just (f i)) 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 (lookup∘update′ i≢j (restrict f js) (just (f j))) - (lemma-lookupM-restrict-∈ i f js p) + P.trans (lookup∘update′ i≢j (restrict f js) (just (f 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 (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j))) - (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs)) + P.trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j))) + (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 -lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) +lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = P.refl +lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = P.cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ Maybe.just ∘ f -lemma-lookupM-fromFunc f zero = refl +lemma-lookupM-fromFunc f zero = P.refl lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i 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 = 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) +lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction P.refl p +lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = P.refl +lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = P.refl +lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ 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 [] i∉[] = P.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)) + P.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-reshape-id [] = P.refl +lemma-reshape-id (x ∷ xs) = P.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} 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 | yes-∈ x∈t = P.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) ⟩ + ≡⟨ P.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) ∎ lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is -lemma-exchange-maps h≈h′ {[]} All.[] = refl -lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis) +lemma-exchange-maps h≈h′ {[]} All.[] = P.refl +lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis) -- cgit v1.2.3