generalize checkInsert to arbitrary Setoids

This is another step towards permitting arbitrary Setoids in bff.

4 files changed, 62 insertions, 40 deletions

diff --git a/BFF.agda b/BFF.agda
index 0cdb231..984528a 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -12,6 +12,7 @@ open import Data.List using (List ; [] ; _∷_ ; map ; length)
 open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
 open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary.Core using (Decidable ; _≡_)
+open import Relation.Binary.PropositionalEquality using (decSetoid)
 
 open import FinMap
 import CheckInsert
@@ -19,7 +20,7 @@ import FreeTheorems
 
 module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
   open FreeTheorems.VecVec public using (get-type)
-  open CheckInsert Carrier deq
+  open CheckInsert (decSetoid deq)
 
   assoc : {n m : ℕ} → Vec (Fin n) m → Vec Carrier m → Maybe (FinMapMaybe n Carrier)
   assoc []V       []V       = just empty
diff --git a/Bidir.agda b/Bidir.agda
index 9cc0ca6..0b2967d 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -7,42 +7,56 @@ open import Data.Fin using (Fin)
 import Level
 import Category.Monad
 import Category.Functor
-open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
+open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) renaming (setoid to MaybeSetoid)
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open import Data.List using (List)
 open import Data.List.All using (All)
 open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; tabulate) renaming (lookup to lookupVec)
+open import Data.Vec.Equality using () renaming (module Equality to VecEq)
 open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary.Core using (refl)
-open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂)
+open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid) renaming (setoid to ≡-setoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Binary using (module Setoid)
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; map-just-injective)
+open import Generic using (just-injective ; map-just-injective ; vecIsSetoid)
 open import FinMap
 import CheckInsert
-open CheckInsert Carrier deq
+open CheckInsert (decSetoid deq)
 import BFF
 open BFF.VecBFF Carrier deq using (assoc ; enumerate ; denumerate ; bff)
 
+maybeSetoid-to-≡ : {A : Set} {x y : Setoid.Carrier (MaybeSetoid (≡-setoid A))} → Setoid._≈_ (MaybeSetoid (≡-setoid A)) x y → x ≡ y
+maybeSetoid-to-≡ (just refl) = refl
+maybeSetoid-to-≡ nothing = refl
+
+vecMaybeSetoid-to-≡ : {A : Set} {n : ℕ} {x y : Setoid.Carrier (vecIsSetoid (MaybeSetoid (≡-setoid A)) n)} → Setoid._≈_ (vecIsSetoid (MaybeSetoid (≡-setoid A)) n) x y → x ≡ y
+vecMaybeSetoid-to-≡ VecEq.[]-cong        = refl
+vecMaybeSetoid-to-≡ (p₁ VecEq.∷-cong p₂) = cong₂ _∷_ (maybeSetoid-to-≡ p₁) (vecMaybeSetoid-to-≡ p₂)
+
+maybeVecMaybeSetoid-to-≡ : {A : Set} {n : ℕ} {x y : Setoid.Carrier (MaybeSetoid (vecIsSetoid (MaybeSetoid (≡-setoid A)) n))} → Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid (≡-setoid A)) n)) x y → x ≡ y
+maybeVecMaybeSetoid-to-≡ (just p) rewrite vecMaybeSetoid-to-≡ p = refl
+maybeVecMaybeSetoid-to-≡ nothing = refl
+
 lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f (toList is))
 lemma-1 f []        = refl
 lemma-1 f (i ∷ is′) = begin
   (assoc is′ (map f is′) >>= checkInsert i (f i))
     ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩
   checkInsert i (f i) (restrict f (toList is′))
-    ≡⟨ lemma-checkInsert-restrict f i (toList is′) ⟩
+    ≡⟨ maybeVecMaybeSetoid-to-≡ (lemma-checkInsert-restrict f i (toList is′)) ⟩
   just (restrict f (toList (i ∷ is′))) ∎
 
 lemma-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc (i ∷ is) (x ∷ xs) ≡ just h → lookupM i h ≡ just x
 lemma-lookupM-assoc i is x xs h    p with assoc is xs
 lemma-lookupM-assoc i is x xs h    () | nothing
 lemma-lookupM-assoc i is x xs h    p | just h' with checkInsert i x h' | insertionresult i x h'
-lemma-lookupM-assoc i is x xs .h refl | just h | ._ | same pl = pl
+lemma-lookupM-assoc i is x xs .h refl | just h | ._ | same x' x≡x' pl = trans pl (cong just (sym x≡x'))
 lemma-lookupM-assoc i is x xs ._ refl | just h' | ._ | new _ = lemma-lookupM-insert i x h'
 lemma-lookupM-assoc i is x xs h () | just h' | ._ | wrong _ _ _
 
@@ -54,7 +68,7 @@ lemma-assoc-domain []         []         h ph = Data.List.All.[]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph with assoc is' xs' | inspect (assoc is') xs'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') .h refl | just h | [ ph' ] | ._ | _ | same pl = All._∷_ (x' , pl) (lemma-assoc-domain is' xs' h ph')
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') .h refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' h ph')
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
   (x' , lemma-lookupM-insert i' x' h')
   (Data.List.All.map
diff --git a/CheckInsert.agda b/CheckInsert.agda
index d82c40b..9302fc7 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -1,73 +1,78 @@
-open import Relation.Binary.Core using (Decidable ; _≡_)
+open import Level using () renaming (zero to ℓ₀)
+open import Relation.Binary using (DecSetoid)
 
-module CheckInsert (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
+module CheckInsert (A : DecSetoid ℓ₀ ℓ₀) 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) renaming (setoid to MaybeEq)
+open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq 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 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) renaming (setoid to PropEq)
-open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
+open import Relation.Binary using (Setoid ; IsPreorder ; 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 FinMap
-open import Generic using (maybeEq-from-≡ ; vecIsSetoid)
+open import Generic using (vecIsSetoid)
+
+private
+  open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq)
 
 checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier)
 checkInsert i b m with lookupM i m
 ...               | nothing = just (insert i b m)
 ...               | just c with deq b c
-...                         | yes b≡c = just m
-...                         | no b≢c  = nothing
+...                         | yes b≈c = just m
+...                         | no b≉c  = nothing
 
 data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where
-  same : lookupM i h ≡ just x → InsertionResult i x h (just h)
+  same : (x' : Carrier) → x ≈ x' → lookupM i h ≡ just x' → InsertionResult i x h (just h)
   new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h))
-  wrong : (x' : Carrier) → x ≢ x' → lookupM i h ≡ just x' → InsertionResult i x h nothing
+  wrong : (x' : Carrier) → ¬ (x ≈ x') → lookupM i h ≡ just x' → InsertionResult i x h nothing
 
 insertionresult : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → InsertionResult i x h (checkInsert i x h)
 insertionresult i x h with lookupM i h | inspect (lookupM i) h
 insertionresult i x h | just x' | _ with deq x x'
-insertionresult i x h | just .x | [ il ] | yes refl = same il
-insertionresult i x h | just x' | [ il ] | no x≢x' = wrong x' x≢x' il
+insertionresult i x h | just x' | [ il ] | yes x≈x' = same x' x≈x' il
+insertionresult i x h | just x' | [ il ] | no x≉x' = wrong x' x≉x' il
 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 refl = refl
-lemma-checkInsert-same i x m refl | .(just x) | no x≢x = contradiction refl 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-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-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 : {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
 
-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 : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) 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 (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
+lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = MaybeEq.just (lemma-insert-same _ i (f i) (begin
+  lookupM i (restrict f is)
+    ≡⟨ p ⟩
+  just x
+    ≈⟨ MaybeEq.just (Setoid.sym A.setoid fi≈x) ⟩
+  just (f i) ∎))
+  where open EqR (MaybeSetoid A.setoid)
+lemma-checkInsert-restrict f i is | ._ | new _ = Setoid.refl (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) _))
+lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (IsPreorder.reflexive (Setoid.isPreorder A.setoid) (lemma-lookupM-restrict i f is x p)) fi≉x
 
 lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h ≡ just x → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
 lemma-lookupM-checkInsert i j x y h h' pl ph' with checkInsert j y h | insertionresult j y h
-lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ = pl
+lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ _ _ = pl
 lemma-lookupM-checkInsert i j x y h h' pl ph'  | ._ | new _ with i ≟ j
 lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = lemma-just≢nothing pl pl'
 lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin
@@ -76,11 +81,13 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i�
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
+  where open Relation.Binary.PropositionalEquality.≡-Reasoning
+
 lemma-lookupM-checkInsert i j x y h h' pl () | ._ | wrong _ _ _
 
 lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h 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 h' ph' with lookupM j h
 lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y
-lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just .x | yes refl = refl
-lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≢y
+lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just y | yes x≈y = refl
+lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≉y
 lemma-lookupM-checkInsert-other i j i≢j x h .(insert j x h) refl | nothing = lemma-lookupM-insert-other i j x h i≢j
diff --git a/Precond.agda b/Precond.agda
index e4699dc..41e3407 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -17,12 +17,12 @@ open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_)
 open import Function using (flip ; _∘_)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
+open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty)
 import CheckInsert
-open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
+open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
 import Bidir