also parameterize Precond

The import of CheckInsert was broken in previous commit.

1 files changed, 21 insertions, 18 deletions

diff --git a/Precond.agda b/Precond.agda
index 18d6a85..7976b0a 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -1,4 +1,6 @@
-module Precond where
+open import Relation.Binary.Core using (Decidable ; _≡_)
+
+module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
 open import Data.Nat using (ℕ) renaming (zero to nzero ; suc to nsuc)
 open import Data.Fin using (Fin ; zero ; suc)
@@ -8,29 +10,30 @@ 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.Core using (_≡_ ; _≢_)
+open import Relation.Binary.Core using (_≢_)
 open import Relation.Binary.PropositionalEquality using (refl ; cong)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import FinMap using (FinMap ; FinMapMaybe ; union ; fromFunc ; empty ; insert)
 open import CheckInsert using (EqInst ; checkInsert ; lemma-checkInsert-new)
 open import BFF using (fmap ; _>>=_)
-open import Bidir using (lemma-∉-lookupM-assoc)
+import Bidir
+open Bidir Carrier deq using (lemma-∉-lookupM-assoc)
 
 open BFF.VecBFF using (get-type ; assoc ; enumerate ; denumerate ; bff)
 
-assoc-enough : {getlen : ℕ → ℕ} (get : get-type getlen) → {B : Set} {m : ℕ} → (eq : EqInst B) → (s : Vec B m) → (v : Vec B (getlen m)) → (h : FinMapMaybe m B) → assoc eq (get (enumerate s)) v ≡ just h → ∃ λ u → bff get eq s v ≡ just u
-assoc-enough get {B} {m} eq s v h p = map (flip lookup (union h g)) s′ , (begin
-  bff get eq s v
+assoc-enough : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (getlen m)) → (h : FinMapMaybe m Carrier) → assoc deq (get (enumerate s)) v ≡ just h → ∃ λ u → bff get deq s v ≡ just u
+assoc-enough get {m} s v h p = map (flip lookup (union h g)) s′ , (begin
+  bff get deq s v
     ≡⟨ refl ⟩
-  fmap (flip map s′ ∘ flip lookup) (fmap (flip union g) (assoc eq (get s′) v))
+  fmap (flip map s′ ∘ flip lookup) (fmap (flip union g) (assoc deq (get s′) v))
     ≡⟨ cong (fmap (flip map s′ ∘ flip lookup)) (cong (fmap (flip union g)) p) ⟩
   fmap (flip map s′ ∘ flip lookup) (fmap (flip union g) (just h))
     ≡⟨ refl ⟩
   just (map (flip lookup (union h g)) s′) ∎)
     where s′ : Vec (Fin m) m
           s′ = enumerate s
-          g : FinMap m B
+          g : FinMap m Carrier
           g = fromFunc (denumerate s)
 
 all-different : {A : Set} {n : ℕ} → Vec A n → Set
@@ -58,14 +61,14 @@ different-∉ x [] p ()
 different-∉ x (y ∷ ys) p (here px) = p zero (suc zero) (λ ()) px
 different-∉ x (y ∷ ys) p (there pxs) = different-∉ x ys (different-drop y (x ∷ ys) (different-swap x y ys p)) pxs
 
-different-assoc : {B : Set} {m n : ℕ} → (eq : EqInst B) → (u : Vec (Fin n) m) → (v : Vec B m) → all-different u → ∃ λ h → assoc eq u v ≡ just h
-different-assoc eq []       []       p = empty , refl
-different-assoc eq (u ∷ us) (v ∷ vs) p with different-assoc eq us vs (λ i j i≢j → p (suc i) (suc j) (i≢j ∘ suc-injective))
-different-assoc eq (u ∷ us) (v ∷ vs) p | h , p' = insert u v h , (begin
-  assoc eq (u ∷ us) (v ∷ vs)
+different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → all-different u → ∃ λ h → assoc deq u v ≡ just h
+different-assoc []       []       p = empty , refl
+different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (λ i j i≢j → p (suc i) (suc j) (i≢j ∘ suc-injective))
+different-assoc (u ∷ us) (v ∷ vs) p | h , p' = insert u v h , (begin
+  assoc deq (u ∷ us) (v ∷ vs)
     ≡⟨ refl ⟩
-  assoc eq us vs >>= checkInsert eq u v
-    ≡⟨ cong (flip _>>=_ (checkInsert eq u v)) p' ⟩
-  checkInsert eq u v h
-    ≡⟨ lemma-checkInsert-new eq u v h (lemma-∉-lookupM-assoc eq u us vs h p' (different-∉ u us p)) ⟩
-  just (insert u v h) ∎)
\ No newline at end of file
+  assoc deq us vs >>= checkInsert deq u v
+    ≡⟨ cong (flip _>>=_ (checkInsert deq u v)) p' ⟩
+  checkInsert deq u v h
+    ≡⟨ lemma-checkInsert-new deq u v h (lemma-∉-lookupM-assoc u us vs h p' (different-∉ u us p)) ⟩
+  just (insert u v h) ∎)