diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 41 |
1 files changed, 22 insertions, 19 deletions
@@ -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′)) |