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. --- CheckInsert.agda | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) (limited to 'CheckInsert.agda') 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) -- cgit v1.2.3