From c63ff4179147ab237afe7d21d9e3740737c9b942 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 09:02:06 +0100 Subject: pass get functions as records This allows passing both getlen and get as a single parameter. It also allows to make the free theorem a prerequisite instead of a postulate. --- Bidir.agda | 39 +++++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 18 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index e0960f5..42f8821 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -25,7 +25,7 @@ open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR import FreeTheorems -open FreeTheorems.VecVec using (get-type ; free-theorem) +open FreeTheorems.VecVec using (Get ; module Get) open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid) open import FinMap import CheckInsert @@ -125,13 +125,13 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin as ∎) where open ≡-Reasoning -theorem-1 : {getlen : ℕ → ℕ} → (get : get-type getlen) → {m : ℕ} → (s : Vec Carrier m) → bff get s (get s) ≡ just s -theorem-1 get s = begin - bff get s (get s) - ≡⟨ cong (bff get s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ - bff get s (get (map (denumerate s) (enumerate s))) - ≡⟨ cong (bff get s) (free-theorem get (denumerate s) (enumerate s)) ⟩ - bff get s (map (denumerate s) (get (enumerate s))) +theorem-1 : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → bff G s (Get.get G s) ≡ just s +theorem-1 G s = begin + bff G s (get s) + ≡⟨ cong (bff G s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ + bff G s (get (map (denumerate s) (enumerate s))) + ≡⟨ cong (bff G s) (free-theorem (denumerate s) (enumerate s)) ⟩ + bff G s (map (denumerate s) (get (enumerate s))) ≡⟨ refl ⟩ (h′↦r ∘ h↦h′) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s)))) ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩ @@ -151,6 +151,7 @@ theorem-1 get s = begin ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩ just s ∎ where open ≡-Reasoning + open Get G h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) @@ -189,8 +190,8 @@ lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] with l lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] | w , pw = y ∷ w , cong (_∷_ (just y)) pw -lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → {getlen : ℕ → ℕ} (get : get-type getlen) → get <$> mapMV f v ≡ mapMV f (get v) -lemma-get-mapMV {f = f} {v = v} p get = let w , pw = lemma-mapM-successful v p in begin +lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → (get : Get) → Get.get get <$> mapMV f v ≡ mapMV f (Get.get get v) +lemma-get-mapMV {f = f} {v = v} p G = let w , pw = lemma-mapM-successful v p in begin get <$> mapMV f v ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩ get <$> (sequenceV (map f v)) @@ -200,15 +201,16 @@ lemma-get-mapMV {f = f} {v = v} p get = let w , pw = lemma-mapM-successful v p i get <$> just w ≡⟨ sym (lemma-just-sequence (get w)) ⟩ sequenceV (map just (get w)) - ≡⟨ cong sequenceV (sym (free-theorem get just w)) ⟩ + ≡⟨ cong sequenceV (sym (free-theorem just w)) ⟩ sequenceV (get (map just w)) ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩ sequenceV (get (map f v)) - ≡⟨ cong sequenceV (free-theorem get f v) ⟩ + ≡⟨ cong sequenceV (free-theorem f v) ⟩ sequenceV (map f (get v)) ≡⟨ sequence-map f (get v) ⟩ mapMV f (get v) ∎ where open ≡-Reasoning + open Get G sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂ sequence-cong {S} VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _)) @@ -217,16 +219,16 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecE sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) sequence-cong {S} (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v : Vec Carrier (getlen m)) → (s u : Vec Carrier m) → bff get s v ≡ just u → VecISetoid A.setoid at _ ∋ get u ≈ v -theorem-2 get v s u p with (lemma->>=-just ((flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (get (enumerate s)) v)) p) -theorem-2 get v s u p | h′ , ph′ with (lemma-<$>-just (assoc (get (enumerate s)) v) ph′) -theorem-2 get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ +theorem-2 : (G : Get) → {m : ℕ} → (v : Vec Carrier (Get.getlen G m)) → (s u : Vec Carrier m) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2 G v s u p with (lemma->>=-just ((flip union (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (Get.get G (enumerate s)) v)) p) +theorem-2 G v s u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate s)) v) ph′) +theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ get <$> (just u) ≡⟨ cong (_<$>_ get) (sym p) ⟩ - get <$> (bff get s v) + get <$> (bff G s v) ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩ get <$> mapMV (flip lookupM (h↦h′ h)) s′ - ≡⟨ lemma-get-mapMV (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) get ⟩ + ≡⟨ lemma-get-mapMV (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) G ⟩ mapMV (flip lookupM (h↦h′ h)) (get s′) ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get s′)) ⟩ sequenceV (map (flip lookupM (h↦h′ h)) (get s′)) @@ -237,6 +239,7 @@ theorem-2 get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid ≡⟨ lemma-just-sequence v ⟩ just v ∎) where open SetoidReasoning + open Get G s′ = enumerate s g = fromFunc (denumerate s) g′ = delete-many (get s′) g -- cgit v1.2.3 From 19670abeff9895de593ef26ad2da247ae590ce90 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 09:13:11 +0100 Subject: allow importing of Bidir without any postulates --- BFF.agda | 4 ++-- Bidir.agda | 4 ++-- Everything.agda | 1 + FreeTheorems.agda | 13 ++++--------- GetTypes.agda | 20 ++++++++++++++++++++ Precond.agda | 4 ++-- 6 files changed, 31 insertions(+), 15 deletions(-) create mode 100644 GetTypes.agda (limited to 'Bidir.agda') diff --git a/BFF.agda b/BFF.agda index 79f3b3d..ddf2307 100644 --- a/BFF.agda +++ b/BFF.agda @@ -16,10 +16,10 @@ open import Relation.Binary using (DecSetoid ; module DecSetoid) open import FinMap open import Generic using (mapMV) import CheckInsert -import FreeTheorems +import GetTypes module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where - open FreeTheorems.VecVec public using (Get) + open GetTypes.VecVec public using (Get) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) open CheckInsert A diff --git a/Bidir.agda b/Bidir.agda index 42f8821..e792b3a 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -24,8 +24,8 @@ open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid) import Relation.Binary.EqReasoning as EqR -import FreeTheorems -open FreeTheorems.VecVec using (Get ; module Get) +import GetTypes +open GetTypes.VecVec using (Get ; module Get) open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid) open import FinMap import CheckInsert diff --git a/Everything.agda b/Everything.agda index 76beef6..7399254 100644 --- a/Everything.agda +++ b/Everything.agda @@ -4,6 +4,7 @@ module Everything where import Generic import FinMap import CheckInsert +import GetTypes import FreeTheorems import BFF import Bidir diff --git a/FreeTheorems.agda b/FreeTheorems.agda index d2ba3ef..2695491 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -6,14 +6,13 @@ open import Data.Vec using (Vec) renaming (map to mapV) open import Function using (_∘_) open import Relation.Binary.PropositionalEquality using (_≗_) +import GetTypes + module ListList where get-type : Set₁ get-type = {A : Set} → List A → List A - record Get : Set₁ where - field - get : {A : Set} → List A → List A - free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get + open GetTypes.ListList public postulate free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get @@ -25,11 +24,7 @@ module VecVec where get-type : (ℕ → ℕ) → Set₁ get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) - record Get : Set₁ where - field - getlen : ℕ → ℕ - get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) - free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + open GetTypes.VecVec public postulate free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get diff --git a/GetTypes.agda b/GetTypes.agda new file mode 100644 index 0000000..99675f9 --- /dev/null +++ b/GetTypes.agda @@ -0,0 +1,20 @@ +module GetTypes 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 + record Get : Set₁ where + field + get : {A : Set} → List A → List A + free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get + +module VecVec where + record Get : Set₁ where + field + getlen : ℕ → ℕ + get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get diff --git a/Precond.agda b/Precond.agda index a1f1081..2be3f3a 100644 --- a/Precond.agda +++ b/Precond.agda @@ -30,8 +30,8 @@ import CheckInsert open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) -import FreeTheorems -open FreeTheorems.VecVec using (Get ; module Get) +import GetTypes +open GetTypes.VecVec using (Get ; module Get) open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v) -- cgit v1.2.3