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, 19 insertions, 20 deletions

diff --git a/CheckInsert.agda b/CheckInsert.agda
index 316d8b1..6a1300b 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -13,9 +13,8 @@ open import Data.Vec.Properties using (lookup∘update′)
 open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary using (Setoid ; module DecSetoid)
-open import Relation.Binary.Core using (refl ; _≡_ ; _≢_)
 import Relation.Binary.EqReasoning as EqR
-open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning)
 
 open import FinMap
 
@@ -43,44 +42,44 @@ insertionresult i x h | nothing | [ il ] = new il
 
 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
 lemma-checkInsert-same i x m p with lookupM i m
-lemma-checkInsert-same i x m refl | .(just x) with deq x x
-lemma-checkInsert-same i x m refl | .(just x) | yes x≈x = refl
-lemma-checkInsert-same i x m refl | .(just x) | no x≉x = contradiction A.refl x≉x
+lemma-checkInsert-same i x m P.refl | .(just x) with deq x x
+lemma-checkInsert-same i x m P.refl | .(just x) | yes x≈x = P.refl
+lemma-checkInsert-same i x m P.refl | .(just x) | no x≉x = contradiction A.refl x≉x
 
 lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m)
 lemma-checkInsert-new i x m p with lookupM i m
-lemma-checkInsert-new i x m refl | .nothing = refl
+lemma-checkInsert-new i x m P.refl | .nothing = P.refl
 
 lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing
 lemma-checkInsert-wrong i x m x' d p with lookupM i m
-lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x'
-lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d
-lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl
+lemma-checkInsert-wrong i x m x' d P.refl | .(just x') with deq x x'
+lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | yes q = contradiction q d
+lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | no ¬q = P.refl
 
 lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is))
 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
-lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (trans p (cong just (sym (lemma-lookupM-restrict i f is p)))))
-lemma-checkInsert-restrict f i is | ._ | new _ = refl
+lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = P.cong just (lemma-insert-same _ i (P.trans p (P.cong just (P.sym (lemma-lookupM-restrict i f is p)))))
+lemma-checkInsert-restrict f i is | ._ | new _ = P.refl
 lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is p)) fi≉x
 
 lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
 lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h
-lemma-lookupM-checkInsert i j h pl y refl | ._ | same _ _ _ = pl
-lemma-lookupM-checkInsert i j h pl y ph'  | ._ | new _ with i ≟ j
-lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
-lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin
+lemma-lookupM-checkInsert i j h     pl y P.refl | ._ | same _ _ _ = pl
+lemma-lookupM-checkInsert i j h     pl y ph'    | ._ | new _ with i ≟ j
+lemma-lookupM-checkInsert i .i h    pl y ph'    | ._ | new pl' | yes P.refl = contradiction (P.trans (P.sym pl) pl') (λ ())
+lemma-lookupM-checkInsert i j h {x} pl y P.refl | ._ | new _ | no i≢j = begin
   lookupM i (insert j y h)
     ≡⟨ lookup∘update′ i≢j h (just y) ⟩
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
-  where open Relation.Binary.PropositionalEquality.≡-Reasoning
+  where open ≡-Reasoning
 
 lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _
 
 lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h
 lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
-lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y
-lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl
-lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y
-lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lookup∘update′ i≢j h (just x)
+lemma-lookupM-checkInsert-other i j i≢j x h ph'    | just y with deq x y
+lemma-lookupM-checkInsert-other i j i≢j x h P.refl | just y | yes x≈y = P.refl
+lemma-lookupM-checkInsert-other i j i≢j x h ()     | just y | no x≉y
+lemma-lookupM-checkInsert-other i j i≢j x h P.refl | nothing = lookup∘update′ i≢j h (just x)