diff options
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/Precond.agda b/Precond.agda index a6f2871..787f010 100644 --- a/Precond.agda +++ b/Precond.agda @@ -34,8 +34,9 @@ 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) - -open BFF.PartialVecBFF (decSetoid deq) using (get-type ; assoc ; enumerate ; denumerate ; bff) +import GetTypes +open GetTypes.PartialVecVec using (Get ; module Get) +open BFF.PartialVecBFF (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) lemma-lookup-map-just zero (x ∷ xs) = refl @@ -73,9 +74,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 : {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 +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 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 ⟩ mapMV (flip lookupM (union h g′)) s′ ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩ @@ -88,7 +89,8 @@ assoc-enough gl₁ gl₂ get s v (h , p) = let w , pw = lemma-union-delete-fromF sequenceV (map Maybe.just (map (flip lookup w) s′)) ≡⟨ lemma-just-sequence (map (flip lookup w) s′) ⟩ just (map (flip lookup w) s′) ∎) - where s′ = enumerate s + where open Get G + s′ = enumerate s g = fromFunc (denumerate s) g′ = delete-many (get s′) g |