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.

1 files changed, 30 insertions, 30 deletions

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)