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, 24 insertions, 23 deletions

diff --git a/Precond.agda b/Precond.agda
index cc81db4..07775ac 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -1,4 +1,5 @@
-open import Relation.Binary.Core using (Decidable ; _≡_)
+open import Relation.Binary.Core using (Decidable)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
@@ -21,29 +22,29 @@ open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
-open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Binary.PropositionalEquality as P using (inspect ; [_])
+open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
 open import Structures using (IsFunctor ; module Shaped ; Shaped)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
-open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
+open CheckInsert (P.decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
 import Bidir
-open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
+open Bidir (P.decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
 import GetTypes
 open GetTypes.PartialShapeShape using (Get ; module Get)
-open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
+open BFF.PartialShapeBFF (P.decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
 
 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
+lemma-maybe-just a (just x) = P.refl
+lemma-maybe-just a nothing  = P.refl
 
 lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
 lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin
       maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
-        ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
+        ≡⟨ P.cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
       maybe′ just (just (g f)) (lookupM f h)
         ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
       just (maybe′ id (g f) (lookupM f h)) ∎))
@@ -55,20 +56,20 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
   _ ∎)
   where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h)
         inner f with f ≟ i
-        inner .i | yes refl = begin
+        inner .i | yes P.refl = begin
           maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h)
-            ≡⟨ cong (maybe′ just _) px ⟩
+            ≡⟨ P.cong (maybe′ just _) px ⟩
           just x
-            ≡⟨ cong (maybe′ just _) (sym px) ⟩
+            ≡⟨ P.cong (maybe′ just _) (P.sym px) ⟩
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
-        inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
+        inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
 module _ (G : Get) where
   open Get G
   open Shaped ViewShapeT using () renaming (content to contentV)
 
   assoc-enough : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
-  assoc-enough {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
+  assoc-enough {i} j s v (h , p) = _ , P.cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
     where g′ = delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))
           t  = enumerate SourceShapeT (gl₁ j)
 
@@ -81,10 +82,10 @@ module _ (G : Get) where
     bff G i s v
       ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
     just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t)
-      ≡⟨ cong just (begin _
-          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+      ≡⟨ P.cong just (begin _
+          ≡⟨ P.cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
         fmapS (flip lookupM (union h g′)) t
-          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
+          ≡⟨ P.cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
         fmapS (flip lookupM (fromFunc (proj₁ wp))) t
           ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
         fmapS (Maybe.just ∘ proj₁ wp) t
@@ -101,9 +102,9 @@ data All-different {A : Set} : List A → Set where
   different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)
 
 lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing
-lemma-∉-lookupM-assoc i []         []         refl i∉is = lemma-lookupM-empty i
-lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs'
-lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ]
+lemma-∉-lookupM-assoc i []         []         P.refl i∉is = lemma-lookupM-empty i
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs')     ph i∉is with assoc is' xs' | inspect (assoc is') xs'
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs')     () i∉is | nothing | [ ph' ]
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ ph' ] = begin
   lookupM i h
     ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' ph ⟩
@@ -112,13 +113,13 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [
   nothing ∎
 
 different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → All-different (toList u) → ∃ λ h → assoc u v ≡ just h
-different-assoc []       []       p = empty , refl
+different-assoc []       []       p = empty , P.refl
 different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) with different-assoc us vs diff-us
 different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) | h , p' = insert u v h , (begin
   assoc (u ∷ us) (v ∷ vs)
-    ≡⟨ refl ⟩
+    ≡⟨ P.refl ⟩
   (assoc us vs >>= checkInsert u v)
-    ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩
+    ≡⟨ P.cong (flip _>>=_ (checkInsert u v)) p' ⟩
   checkInsert u v h
     ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs p' u∉us) ⟩
   just (insert u v h) ∎)