move generic functions to a new Generic module

4 files changed, 51 insertions, 31 deletions

diff --git a/Bidir.agda b/Bidir.agda
index f5f3769..9cc0ca6 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -22,6 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
+open import Generic using (just-injective ; map-just-injective)
 open import FinMap
 import CheckInsert
 open CheckInsert Carrier deq
@@ -128,14 +129,6 @@ lemma-<$>-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → f <$> ma â
 lemma-<$>-just {ma = just x}  f<$>ma≡just-b = x , refl
 lemma-<$>-just {ma = nothing} ()
 
-∷-injective : {A : Set} {n : ℕ} {x y : A} {xs ys : Vec A n} → (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
-∷-injective refl = refl , refl
-
-map-just-injective : {A : Set} {n : ℕ} {xs ys : Vec A n} → map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys
-map-just-injective {xs = []}      {ys = []}       p  = refl
-map-just-injective {xs = x ∷ xs'} {ys = y ∷ ys'}  p with ∷-injective p
-map-just-injective {xs = x ∷ xs'} {ys = .x ∷ ys'} p | refl , p' = cong (_∷_ x) (map-just-injective p')
-
 lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMap n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map just (map (flip lookup (union h h')) is) ≡ map (flip lookupM h) is
 lemma-union-not-used h h' []        p = refl
 lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin
diff --git a/FinMap.agda b/FinMap.agda
index a515a2f..46dbd1c 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -15,6 +15,8 @@ open import Relation.Binary.Core using (_≡_ ; refl ; _≢_)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans ; cong₂)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
+open import Generic using (just-injective)
+
 FinMapMaybe : ℕ → Set → Set
 FinMapMaybe n A = Vec (Maybe A) n
 
@@ -77,9 +79,6 @@ lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
 lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl
 lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc)
 
-just-injective : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y
-just-injective refl = refl
-
 lemma-lookupM-restrict : {A : Set} {n : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a
 lemma-lookupM-restrict i f []        a p = lemma-just≢nothing p (lemma-lookupM-empty i)
 lemma-lookupM-restrict i f (i' ∷ is) a p with i ≟ i'
diff --git a/Generic.agda b/Generic.agda
new file mode 100644
index 0000000..c7cbc45
--- /dev/null
+++ b/Generic.agda
@@ -0,0 +1,47 @@
+module Generic where
+
+open import Data.List using (List ; length ; replicate) renaming ([] to []L ; _∷_ to _∷L_)
+open import Data.Maybe using (Maybe ; just)
+open import Data.Nat using (â„• ; zero ; suc)
+open import Data.Product using (_×_ ; _,_)
+open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
+open import Function using (_∘_)
+open import Relation.Binary.Core using (_≡_ ; refl)
+open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans)
+
+∷-injective : {A : Set} {n : ℕ} {x y : A} {xs ys : Vec A n} →
+              (x ∷V xs) ≡ (y ∷V ys) → x ≡ y × xs ≡ ys
+∷-injective refl = refl , refl
+
+just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
+just-injective refl = refl
+
+length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
+length-replicate zero       = refl
+length-replicate (suc n) = cong suc (length-replicate n)
+
+map-just-injective : {A : Set} {n : ℕ} {xs ys : Vec A n} →
+                     map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys
+map-just-injective {xs = []V}      {ys = []V}       p  = refl
+map-just-injective {xs = x ∷V xs′} {ys = y ∷V ys′}  p with ∷-injective p
+map-just-injective {xs = x ∷V xs′} {ys = .x ∷V ys′} p | refl , p′ = cong (_∷V_ x) (map-just-injective p′)
+
+subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) →
+             f ∘ subst T p ≗ subst T (cong g p) ∘ f
+subst-cong T f refl _ = refl
+
+subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) →
+                 subst (Vec A) (cong length p) (fromList y) ≡ fromList x
+subst-fromList refl = refl
+
+subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′ : b ≡ c) → (x : T a) →
+              subst T p′ (subst T p x) ≡ subst T (trans p p′) x
+subst-subst T refl p′ x = refl
+
+toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
+toList-fromList []L       = refl
+toList-fromList (x ∷L xs) = cong (_∷L_ x) (toList-fromList xs)
+
+toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) →
+               toList (subst (Vec A) p v) ≡ toList v
+toList-subst v refl = refl
diff --git a/LiftGet.agda b/LiftGet.agda
index b6d99de..31a632e 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -12,6 +12,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; re
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 import FreeTheorems
+open import Generic using (length-replicate ; subst-cong ; subst-fromList ; subst-subst ; toList-fromList ; toList-subst)
 open FreeTheorems.ListList using (get-type ; free-theorem)
 open FreeTheorems.VecVec using () renaming (get-type to getV-type)
 
@@ -39,13 +40,6 @@ length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡
 length-toList []V = refl
 length-toList (x ∷V xs) = cong suc (length-toList xs) 
 
-toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
-toList-fromList []       = refl
-toList-fromList (x ∷ xs) = cong (_∷_ x) (toList-fromList xs)
-
-toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) → toList (subst (Vec A) p v) ≡ toList v
-toList-subst v refl = refl
-
 getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
 getList-to-getVec-length-property get {_} {m} v = begin
     length (get (toList v))
@@ -61,12 +55,6 @@ getList-to-getVec get = getlen , get'
         get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
         get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))
 
-subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p' : b ≡ c) → (x : T a)→ subst T p' (subst T p x) ≡ subst T (trans p p') x
-subst-subst T refl p' x = refl
-
-subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) → subst (Vec A) (cong length p) (fromList y) ≡ fromList x
-subst-fromList refl = refl
-
 get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ subst (Vec A) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))
 get-commut-1 get {A} l = begin
   fromList (get l)
@@ -100,13 +88,6 @@ get-trafo-1 get {B} l = begin
 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
 vec-len {_} {n} _ = n
 
-length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
-length-replicate 0       = refl
-length-replicate (suc n) = cong suc (length-replicate n)
-
-subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) → f ∘ subst T p ≗ subst T (cong g p) ∘ f
-subst-cong T f refl _ = refl
-
 fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≡ subst (Vec A) (sym (length-toList v)) v
 fromList-toList     []V       = refl
 fromList-toList {A} (x ∷V xs) = begin