From 7ba21759412a8b356f7790ac5f5e413302331183 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 5 Oct 2012 12:47:09 +0200 Subject: [PATCH] move all postulates to one module This should make it easier to see what is assumed. --- BFF.agda | 7 +++---- Bidir.agda | 13 +++++-------- FreeTheorems.agda | 21 +++++++++++++++++++++ LiftGet.agda | 11 ++++------- 4 files changed, 33 insertions(+), 19 deletions(-) create mode 100644 FreeTheorems.agda 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)) ∎ -- 2.20.1