move all postulates to one module

This should make it easier to see what is assumed.

4 files changed, 33 insertions, 19 deletions

diff --git a/BFF.agda b/BFF.agda
index 546782d..612c2c3 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -9,6 +9,7 @@ open import Function using (id ; _∘_ ; flip)
 
 open import FinMap
 open import CheckInsert
+import FreeTheorems
 
 _>>=_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B
 _>>=_ = flip (flip maybe′ nothing)
@@ -17,8 +18,7 @@ fmap : {A B : Set} → (A → B) → Maybe A → Maybe B
 fmap f = maybe′ (λ a → just (f a)) nothing
 
 module ListBFF where
-  get-type : Set₁
-  get-type = {A : Set} → List A → List A
+  open FreeTheorems.ListList public using (get-type)
 
   assoc : {A : Set} {n : ℕ} → EqInst A → List (Fin n) → List A → Maybe (FinMapMaybe n A)
   assoc _  []       []       = just empty
@@ -39,8 +39,7 @@ module ListBFF where
                    in fmap (flip map s′ ∘ flip lookup) h′
 
 module VecBFF where
-  get-type : (ℕ → ℕ) → Set₁
-  get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+  open FreeTheorems.VecVec public using (get-type)
 
   assoc : {A : Set} {n m : ℕ} → EqInst A → Vec (Fin n) m → Vec A m → Maybe (FinMapMaybe n A)
   assoc _  []V       []V       = just empty
diff --git a/Bidir.agda b/Bidir.agda
index a1f958c..2567d8f 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -19,12 +19,12 @@ open import Relation.Binary.Core using (_≡_ ; refl)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; _≗_ ; trans)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
+import FreeTheorems
+open FreeTheorems.VecVec using (get-type ; free-theorem)
 open import FinMap
 open import CheckInsert
-
 open import BFF using (_>>=_ ; fmap)
-
-open BFF.VecBFF using (get-type ; assoc ; enumerate ; denumerate ; bff)
+open BFF.VecBFF using (assoc ; enumerate ; denumerate ; bff)
 
 lemma-1 : {τ : Set} {m n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : Vec (Fin n) m) → assoc eq is (map f is) ≡ just (restrict f (toList is))
 lemma-1 eq f []        = refl
@@ -150,9 +150,6 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
     ≡⟨ refl ⟩
   map just (x ∷ xs) ∎
 
-postulate
-  free-theorem-list-list : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {m : ℕ} → (v : Vec α m) → get (map f v) ≡ map f (get v)
-
 lemma-map-denumerate-enumerate : {m : ℕ} {A : Set} → (as : Vec A m) → map (denumerate as) (enumerate as) ≡ as
 lemma-map-denumerate-enumerate []       = refl
 lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
@@ -173,7 +170,7 @@ theorem-1 get eq s = begin
   bff get eq s (get s)
     ≡⟨ cong (bff get eq s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
   bff get eq s (get (map (denumerate s) (enumerate s)))
-    ≡⟨ cong (bff get eq s) (free-theorem-list-list get (denumerate s) (enumerate s)) ⟩
+    ≡⟨ cong (bff get eq s) (free-theorem get (denumerate s) (enumerate s)) ⟩
   bff get eq s (map (denumerate s) (get (enumerate s)))
     ≡⟨ refl ⟩
   fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (denumerate s))) (assoc eq (get (enumerate s)) (map (denumerate s) (get (enumerate s)))))
@@ -237,7 +234,7 @@ theorem-2 get eq v s u p | h , ph = begin
      just (get (map (flip lookup (union h (fromFunc (denumerate s)))) (enumerate s)))
        ∎) ⟩
   get (map (flip lookup (union h (fromFunc (denumerate s)))) (enumerate s))
-    ≡⟨ free-theorem-list-list get (flip lookup (union h (fromFunc (denumerate s)))) (enumerate s) ⟩
+    ≡⟨ free-theorem get (flip lookup (union h (fromFunc (denumerate s)))) (enumerate s) ⟩
   map (flip lookup (union h (fromFunc (denumerate s)))) (get (enumerate s))
      ≡⟨ lemma-from-map-just (begin
        map just (map (flip lookup (union h (fromFunc (denumerate s)))) (get (enumerate s)))
diff --git a/FreeTheorems.agda b/FreeTheorems.agda
new file mode 100644
index 0000000..f37cada
--- /dev/null
+++ b/FreeTheorems.agda
@@ -0,0 +1,21 @@
+module FreeTheorems where
+
+open import Data.Nat using (ℕ)
+open import Data.List using (List ; map)
+open import Data.Vec using (Vec) renaming (map to mapV)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality using (_≗_)
+
+module ListList where
+  get-type : Set₁
+  get-type = {A : Set} → List A → List A
+
+  postulate
+    free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+
+module VecVec where
+  get-type : (ℕ → ℕ) → Set₁
+  get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+
+  postulate
+    free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
diff --git a/LiftGet.agda b/LiftGet.agda
index c4f1acd..b6d99de 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -11,9 +11,9 @@ open import Relation.Binary.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
-import BFF
-open BFF.ListBFF using (get-type)
-open BFF.VecBFF using () renaming (get-type to getV-type)
+import FreeTheorems
+open FreeTheorems.ListList using (get-type ; free-theorem)
+open FreeTheorems.VecVec using () renaming (get-type to getV-type)
 
 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
 getVec-to-getList get = toList ∘ get ∘ fromList
@@ -21,9 +21,6 @@ getVec-to-getList get = toList ∘ get ∘ fromList
 getList-to-getlen : get-type → ℕ → ℕ
 getList-to-getlen get = length ∘ get ∘ flip replicate tt
 
-postulate
-  free-theorem-list-list : {β γ : Set} → (get : get-type) → (f : β → γ) → get ∘ map f ≗ map f ∘ get
-
 replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
 replicate-length [] = refl
 replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)
@@ -33,7 +30,7 @@ getList-length get l = begin
   length (get l)
     ≡⟨ sym (length-map (const tt) (get l)) ⟩
   length (map (const tt) (get l))
-    ≡⟨ cong length (sym (free-theorem-list-list get (const tt) l)) ⟩
+    ≡⟨ cong length (sym (free-theorem get (const tt) l)) ⟩
   length (get (map (const tt) l))
     ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
   length (get (replicate (length l) tt)) ∎