From 48a000f3dc05a9117a9b72e250569c204a4d1371 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 16 Jan 2014 11:32:12 +0100 Subject: generalize lemma-insert-same to arbitrary Setoids The general idea is to enable bff to use arbitrary DecSetoids. * assoc needs to learn about DecSetoid * checkInsert needs to learn about DecSetoid * InsertionResult needs to learn about Setoid * Parameters to InsertionResult.same become weaker * lemma-checkInsert-restrict should work with weaker same * lemma-insert-same needs to learn about Setoid --- CheckInsert.agda | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'CheckInsert.agda') diff --git a/CheckInsert.agda b/CheckInsert.agda index 6926587..d82c40b 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -5,15 +5,19 @@ module CheckInsert (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where open import Data.Nat using (ℕ) open import Data.Fin using (Fin) open import Data.Fin.Props using (_≟_) -open import Data.Maybe using (Maybe ; nothing ; just) +open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeEq) open import Data.List using (List ; [] ; _∷_) +open import Data.Vec using () renaming (_∷_ to _∷V_) +open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Relation.Nullary using (Dec ; yes ; no) open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary using (Setoid) open import Relation.Binary.Core using (refl ; _≢_) -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) +open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) renaming (setoid to PropEq) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap +open import Generic using (maybeEq-from-≡ ; vecIsSetoid) checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier) checkInsert i b m with lookupM i m @@ -50,9 +54,14 @@ 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 +vecSetoidToProp : {A : Set} {n : ℕ} {x y : Setoid.Carrier (vecIsSetoid (MaybeEq (PropEq A)) n)} → Setoid._≈_ (vecIsSetoid (MaybeEq (PropEq A)) n) x y → x ≡ y +vecSetoidToProp VecEq.[]-cong = refl +vecSetoidToProp (just refl VecEq.∷-cong p) = cong (_∷V_ _) (vecSetoidToProp p) +vecSetoidToProp (nothing VecEq.∷-cong p) = cong (_∷V_ _) (vecSetoidToProp p) + lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ 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 p = cong just (lemma-insert-same _ i (f i) p) +lemma-checkInsert-restrict f i is | ._ | same p = cong just (vecSetoidToProp (lemma-insert-same _ i (f i) (maybeEq-from-≡ p))) lemma-checkInsert-restrict f i is | ._ | new _ = refl lemma-checkInsert-restrict f i is | ._ | wrong x fi≢x p = contradiction (lemma-lookupM-restrict i f is x p) fi≢x -- cgit v1.2.3