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

1 files changed, 12 insertions, 3 deletions

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