From 1c3da162d500cfe885fa21b4d75847c4bcbb2aa1 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 28 Jan 2014 15:15:12 +0100 Subject: define bff on a partial getlen MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The representation chosen is to give both an injection gl₁ and a function gl₂ (formerly getlen), such that by choosing a non-identity for gl₁ partiality of getlen can be expressed. An alternative would have been to allow getlen to return a Maybe ℕ and have get return maybe (Vec A) ⊤ (getlen n) thus sending all inputs for which getlen yields nothing to tt. It seems that while there is no way to obtain a such a getlen predicate from an arbitrary index Setoid I, it should be possible to manufacture a Setoid from a predicate. Thanks to Stefan Mehner for the insightful discussion. --- BFF.agda | 22 +++++++++++++++++++++- FreeTheorems.agda | 27 +++++++++++++++++++++++++-- 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/BFF.agda b/BFF.agda index 61eeefd..0247bde 100644 --- a/BFF.agda +++ b/BFF.agda @@ -11,7 +11,11 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (id ; _∘_ ; flip) -open import Relation.Binary using (DecSetoid ; module DecSetoid) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_) +open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) +open import Relation.Binary.PropositionalEquality using () renaming (setoid to EqSetoid) +open Injection using (to) open import FinMap open import Generic using (mapMV) @@ -41,3 +45,19 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where h = assoc t′ v h′ = (flip union g′) <$> h in h′ >>= flip mapMV s′ ∘ flip lookupV + +module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where + open FreeTheorems.PartialVecVec public using (get-type) + open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) + open CheckInsert A + + open VecBFF A public using (assoc ; enumerate ; denumerate) + + bff : {I : Setoid ℓ₀ ℓ₀} {gl₁ : I ↪ (EqSetoid ℕ)} {gl₂ : I ⟶ EqSetoid ℕ} → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i))) + bff get s v = let s′ = enumerate s + t′ = get s′ + g = fromFunc (denumerate s) + g′ = delete-many t′ g + h = assoc t′ v + h′ = (flip union g′) <$> h + in h′ >>= flip mapMV s′ ∘ flip lookupV diff --git a/FreeTheorems.agda b/FreeTheorems.agda index f37cada..aacb95a 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -1,10 +1,15 @@ module FreeTheorems where +open import Level using () renaming (zero to ℓ₀) 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 (_≗_) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid) +open import Relation.Binary using (Setoid) +open Injection using (to) module ListList where get-type : Set₁ @@ -17,5 +22,23 @@ module VecVec where get-type : (ℕ → ℕ) → Set₁ get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + free-theorem-type : Set₁ + free-theorem-type = {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + + postulate + free-theorem : free-theorem-type + +module PartialVecVec where + get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁ + get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) + postulate - free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get + + open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type) + + ≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B + ≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f } + + VecVec-free-theorem : VecVec-free-theorem-type + VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get -- cgit v1.2.3 From 934f2003d4f47c2af3a91cd827d75caeded7ec7a Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 14:01:10 +0100 Subject: express VecBFF via PartialVecBFF --- BFF.agda | 28 +++++++++++----------------- FreeTheorems.agda | 5 ++--- Generic.agda | 10 +++++++--- 3 files changed, 20 insertions(+), 23 deletions(-) diff --git a/BFF.agda b/BFF.agda index 0247bde..bf8e751 100644 --- a/BFF.agda +++ b/BFF.agda @@ -12,18 +12,18 @@ open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (id ; _∘_ ; flip) open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) -open import Relation.Binary.PropositionalEquality using () renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid) open Injection using (to) open import FinMap -open import Generic using (mapMV) +open import Generic using (mapMV ; ≡-to-Π) import CheckInsert import FreeTheorems -module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where - open FreeTheorems.VecVec public using (get-type) +module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where + open FreeTheorems.PartialVecVec public using (get-type) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) open CheckInsert A @@ -37,7 +37,7 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) + bff : {I : Setoid ℓ₀ ℓ₀} {gl₁ : I ↪ (EqSetoid ℕ)} {gl₂ : I ⟶ EqSetoid ℕ} → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i))) bff get s v = let s′ = enumerate s t′ = get s′ g = fromFunc (denumerate s) @@ -46,18 +46,12 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where h′ = (flip union g′) <$> h in h′ >>= flip mapMV s′ ∘ flip lookupV -module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where - open FreeTheorems.PartialVecVec public using (get-type) +module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where + open FreeTheorems.VecVec public using (get-type) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) open CheckInsert A - open VecBFF A public using (assoc ; enumerate ; denumerate) + open PartialVecBFF A public using (assoc ; enumerate ; denumerate) - bff : {I : Setoid ℓ₀ ℓ₀} {gl₁ : I ↪ (EqSetoid ℕ)} {gl₂ : I ⟶ EqSetoid ℕ} → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i))) - bff get s v = let s′ = enumerate s - t′ = get s′ - g = fromFunc (denumerate s) - g′ = delete-many t′ g - h = assoc t′ v - h′ = (flip union g′) <$> h - in h′ >>= flip mapMV s′ ∘ flip lookupV + bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) + bff {getlen} get s v = PartialVecBFF.bff A {_} {id↪} {≡-to-Π getlen} get {_} s v diff --git a/FreeTheorems.agda b/FreeTheorems.agda index aacb95a..c22a68d 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -11,6 +11,8 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming open import Relation.Binary using (Setoid) open Injection using (to) +open import Generic using (≡-to-Π) + module ListList where get-type : Set₁ get-type = {A : Set} → List A → List A @@ -37,8 +39,5 @@ module PartialVecVec where open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type) - ≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B - ≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f } - VecVec-free-theorem : VecVec-free-theorem-type VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get diff --git a/Generic.agda b/Generic.agda index 81292ff..a734ec2 100644 --- a/Generic.agda +++ b/Generic.agda @@ -9,16 +9,20 @@ open import Data.Product using (_×_ ; _,_) open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Function using (_∘_ ; id) +open import Function.Equality using (_⟶_) open import Level using () renaming (zero to ℓ₀) open import Relation.Binary using (Setoid ; module Setoid) open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to PropEq) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to EqSetoid) open Setoid using () renaming (_≈_ to _∋_≈_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) +≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B +≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f } + just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y just-injective refl = refl @@ -40,11 +44,11 @@ mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → map mapMV-purity f []V = refl mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl -maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (PropEq A) ∋ a ≈ b +maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (EqSetoid A) ∋ a ≈ b maybeEq-from-≡ {a = just x} {b = .(just x)} refl = just refl maybeEq-from-≡ {a = nothing} {b = .nothing} refl = nothing -maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (PropEq A) ∋ a ≈ b → a ≡ b +maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (EqSetoid A) ∋ a ≈ b → a ≡ b maybeEq-to-≡ (just refl) = refl maybeEq-to-≡ nothing = refl -- cgit v1.2.3 From ffd72d6471ec0166b4dcb4f6b622bcc1c4aafcbf Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 14:04:29 +0100 Subject: make the getlen functions explicit in PartialVecBFF There is no way for Agda to infer these functions or even the intended index Setoid, so making these explicit is rather required. --- BFF.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/BFF.agda b/BFF.agda index bf8e751..b26cc92 100644 --- a/BFF.agda +++ b/BFF.agda @@ -37,8 +37,9 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : {I : Setoid ℓ₀ ℓ₀} {gl₁ : I ↪ (EqSetoid ℕ)} {gl₂ : I ⟶ EqSetoid ℕ} → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i))) - bff get s v = let s′ = enumerate s + bff : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ EqSetoid ℕ) → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i))) + bff gl₁ gl₂ get s v = + let s′ = enumerate s t′ = get s′ g = fromFunc (denumerate s) g′ = delete-many t′ g @@ -54,4 +55,4 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open PartialVecBFF A public using (assoc ; enumerate ; denumerate) bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) - bff {getlen} get s v = PartialVecBFF.bff A {_} {id↪} {≡-to-Π getlen} get {_} s v + bff {getlen} get s v = PartialVecBFF.bff A id↪ (≡-to-Π getlen) get {_} s v -- cgit v1.2.3 From e227314c11a17efa2e41ee8756041c4e5b747792 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 14:23:10 +0100 Subject: fully allow partial get functions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit By choosing gl₁ = suc and gl₂ = id, the tail function can now be bidirectionalized. --- Bidir.agda | 41 ++++++++++++++++++++++------------------- Precond.agda | 16 ++++++++++------ 2 files changed, 32 insertions(+), 25 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index e0960f5..7add8fd 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -18,6 +18,9 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_) +open Injection using (to) open import Relation.Binary.Core using (refl ; _≡_) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid) @@ -25,13 +28,13 @@ 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.PartialVecVec using (get-type ; free-theorem) open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid) open import FinMap import CheckInsert open CheckInsert A import BFF -open BFF.VecBFF A using (assoc ; enumerate ; denumerate ; bff) +open BFF.PartialVecBFF A using (assoc ; enumerate ; denumerate ; bff) open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) @@ -125,13 +128,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 : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (s : Vec Carrier (to gl₁ ⟨$⟩ i)) → bff gl₁ gl₂ get s (get s) ≡ just s +theorem-1 gl₁ gl₂ get s = begin + bff gl₁ gl₂ get s (get s) + ≡⟨ cong (bff gl₁ gl₂ get s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ + bff gl₁ gl₂ get s (get (map (denumerate s) (enumerate s))) + ≡⟨ cong (bff gl₁ gl₂ get s) (free-theorem gl₁ gl₂ get (denumerate s) (enumerate s)) ⟩ + bff gl₁ gl₂ get 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))) ⟩ @@ -189,8 +192,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} {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → {i : Setoid.Carrier I} {v : Vec A (to gl₁ ⟨$⟩ i)} {r : Vec B (to gl₁ ⟨$⟩ i)} → mapMV f v ≡ just r → (get : get-type gl₁ gl₂) → get <$> mapMV f v ≡ mapMV f (get v) +lemma-get-mapMV {f = f} gl₁ gl₂ {v = v} p get = 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,11 +203,11 @@ 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 gl₁ gl₂ get 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 gl₁ gl₂ get f v) ⟩ sequenceV (map f (get v)) ≡⟨ sequence-map f (get v) ⟩ mapMV f (get v) ∎ @@ -217,16 +220,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 : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (v : Vec Carrier (gl₂ ⟨$⟩ i)) → (s u : Vec Carrier (to gl₁ ⟨$⟩ i)) → bff gl₁ gl₂ get s v ≡ just u → VecISetoid A.setoid at _ ∋ get u ≈ v +theorem-2 gl₁ gl₂ 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 gl₁ gl₂ get v s u p | h′ , ph′ with (lemma-<$>-just (assoc (get (enumerate s)) v) ph′) +theorem-2 gl₁ gl₂ get 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 gl₁ gl₂ get 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 gl₁ gl₂ (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) get ⟩ 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′)) diff --git a/Precond.agda b/Precond.agda index 19329b5..a6f2871 100644 --- a/Precond.agda +++ b/Precond.agda @@ -6,7 +6,7 @@ open import Data.Nat using (ℕ) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Props using (_≟_) open import Data.List using (List ; [] ; _∷_) -import Level +open import Level using () renaming (zero to ℓ₀) import Category.Monad import Category.Functor open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) @@ -20,7 +20,11 @@ open Data.List.Any.Membership-≡ using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_ ; proj₂) open import Function using (flip ; _∘_ ; id) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_) +open Injection using (to) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) renaming (setoid to EqSetoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) @@ -31,7 +35,7 @@ open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; le import BFF open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) -open BFF.VecBFF (decSetoid deq) using (get-type ; assoc ; enumerate ; denumerate ; bff) +open BFF.PartialVecBFF (decSetoid deq) using (get-type ; 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) lemma-lookup-map-just zero (x ∷ xs) = refl @@ -69,9 +73,9 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Da maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎ inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i) -assoc-enough : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (getlen m)) → ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff get s v ≡ just u -assoc-enough get s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin - bff get s v +assoc-enough : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) → (get : get-type gl₁ gl₂) → {i : Setoid.Carrier I} → (s : Vec Carrier (to gl₁ ⟨$⟩ i)) → (v : Vec Carrier (gl₂ ⟨$⟩ i)) → ∃ (λ h → assoc (get (enumerate s)) v ≡ just h) → ∃ λ u → bff gl₁ gl₂ get s v ≡ just u +assoc-enough gl₁ gl₂ get s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin + bff gl₁ gl₂ get s v ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩ mapMV (flip lookupM (union h g′)) s′ ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩ -- cgit v1.2.3 From 20c176d383e59a0345f7425c5f14679906159a59 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 4 Feb 2014 10:52:49 +0100 Subject: add convenience members to PartialVecVec.Get --- BFF.agda | 2 +- Bidir.agda | 6 +++--- GetTypes.agda | 10 ++++++++-- Precond.agda | 2 +- 4 files changed, 13 insertions(+), 7 deletions(-) diff --git a/BFF.agda b/BFF.agda index 5bf756d..f5573ba 100644 --- a/BFF.agda +++ b/BFF.agda @@ -38,7 +38,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate = flip lookupV - bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i))) + bff : (G : Get) → ({i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))) bff G s v = let s′ = enumerate s t′ = Get.get G s′ g = fromFunc (denumerate s) diff --git a/Bidir.agda b/Bidir.agda index cb29420..a77a9db 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -128,7 +128,7 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin as ∎) where open ≡-Reasoning -theorem-1 : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → bff G s (Get.get G s) ≡ just s +theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → 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)) ⟩ @@ -192,7 +192,7 @@ lemma-mapM-successful (x ∷ xs) () | just y | nothing | _ lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] with lemma-mapM-successful xs p′ 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} → (G : Get) → {i : Setoid.Carrier (Get.I G)} {v : Vec A (to (Get.gl₁ G) ⟨$⟩ i)} {r : Vec B (to (Get.gl₁ G) ⟨$⟩ i)} → mapMV f v ≡ just r → Get.get G <$> mapMV f v ≡ mapMV f (Get.get G v) +lemma-get-mapMV : {A B : Set} {f : A → Maybe B} → (G : Get) → {i : Get.|I| G} {v : Vec A (Get.|gl₁| G i)} {r : Vec B (Get.|gl₁| G i)} → mapMV f v ≡ just r → Get.get G <$> mapMV f v ≡ mapMV f (Get.get G v) lemma-get-mapMV {f = f} G {v = v} p = let w , pw = lemma-mapM-successful v p in begin get <$> mapMV f v ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩ @@ -221,7 +221,7 @@ 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 : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → (s u : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2 : (G : Get) → {i : Get.|I| G} → (v : Vec Carrier (Get.|gl₂| G i)) → (s u : Vec Carrier (Get.|gl₁| G i)) → 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 _) ⟩ diff --git a/GetTypes.agda b/GetTypes.agda index a52ec24..eb72cea 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -32,8 +32,14 @@ module PartialVecVec where I : Setoid ℓ₀ ℓ₀ gl₁ : I ↪ EqSetoid ℕ gl₂ : I ⟶ EqSetoid ℕ - get : {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) - free-theorem : {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get + + |I| = Setoid.Carrier I + |gl₁| = _⟨$⟩_ (to gl₁) + |gl₂| = _⟨$⟩_ gl₂ + + field + get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i) + free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get VecVec-to-PartialVecVec G = record diff --git a/Precond.agda b/Precond.agda index 787f010..81c204b 100644 --- a/Precond.agda +++ b/Precond.agda @@ -74,7 +74,7 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Da maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎ inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i) -assoc-enough : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u +assoc-enough : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u assoc-enough G s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin bff G s v ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩ -- cgit v1.2.3 From ce4bbcc0c06b088a10881fcd66da5422571e7995 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 4 Feb 2014 11:12:42 +0100 Subject: remove unused imports Most of the became unused by using the convenience functions introduced in the parent commit. --- BFF.agda | 4 ---- Bidir.agda | 3 --- FreeTheorems.agda | 2 -- Precond.agda | 5 +---- 4 files changed, 1 insertion(+), 13 deletions(-) diff --git a/BFF.agda b/BFF.agda index f5573ba..ced6ebf 100644 --- a/BFF.agda +++ b/BFF.agda @@ -11,11 +11,7 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (id ; _∘_ ; flip) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) -open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid) -open Injection using (to) open import FinMap open import Generic using (mapMV ; ≡-to-Π) diff --git a/Bidir.agda b/Bidir.agda index a77a9db..cca2ba7 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -18,9 +18,6 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_) -open Injection using (to) open import Relation.Binary.Core using (refl ; _≡_) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid) diff --git a/FreeTheorems.agda b/FreeTheorems.agda index 2181163..d4eb174 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -11,8 +11,6 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming open import Relation.Binary using (Setoid) open Injection using (to) -open import Generic using (≡-to-Π) - import GetTypes module ListList where diff --git a/Precond.agda b/Precond.agda index 81c204b..ebb5412 100644 --- a/Precond.agda +++ b/Precond.agda @@ -20,11 +20,8 @@ open Data.List.Any.Membership-≡ using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_ ; proj₂) open import Function using (flip ; _∘_ ; id) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_) -open Injection using (to) open import Relation.Binary using (Setoid) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) -- cgit v1.2.3