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. --- Precond.agda | 47 ++++++++++++++++++++++++----------------------- 1 file changed, 24 insertions(+), 23 deletions(-) (limited to 'Precond.agda') 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) ∎) -- cgit v1.2.3