diff options
| -rw-r--r-- | Bidir.agda | 56 | ||||
| -rw-r--r-- | Precond.agda | 31 |
2 files changed, 47 insertions, 40 deletions
@@ -26,7 +26,7 @@ import Relation.Binary.EqReasoning as EqR import GetTypes open GetTypes.PartialVecVec using (Get ; module Get) -open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid) +open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective) open import FinMap import CheckInsert open CheckInsert A @@ -212,36 +212,22 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) sequence-cong {S} (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v theorem-2 G j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p) theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′) -theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ - get <$> (just u) - ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩ - get <$> (just (map just u) >>= sequenceV) - ≡⟨ cong (_<$>_ get ∘ flip _>>=_ sequenceV) (sym p) ⟩ - get <$> (bff G j s v >>= sequenceV) - ≡⟨ cong (_<$>_ get ∘ flip _>>=_ sequenceV ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph ⟩ - get <$> sequenceV (h′↦r (h↦h′ h)) - ≡⟨ lemma-get-sequenceV G (begin⟨ EqSetoid _ ⟩ - sequenceV (h′↦r (h↦h′ h)) - ≡⟨ cong (flip _>>=_ sequenceV ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) (sym ph) ⟩ - (h′↦r <$> (h↦h′ <$> assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) >>= sequenceV) - ≡⟨ cong (flip _>>=_ sequenceV) p ⟩ - sequenceV (map just u) - ≡⟨ lemma-just-sequence u ⟩ - just u ∎) ⟩ - sequenceV (get (h′↦r (h↦h′ h))) +theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩ + get u + ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p)) + (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩ + get (h′↦r (h↦h′ h)) ≡⟨ refl ⟩ - sequenceV (get (map (flip lookupM (h↦h′ h)) t)) - ≡⟨ cong sequenceV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩ - sequenceV (map (flip lookupM (h↦h′ h)) (get t)) - ≡⟨ cong sequenceV (lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph)) ⟩ - sequenceV (map (flip lookupM h) (get t)) - ≈⟨ sequence-cong (lemma-2 (get t) v h ph) ⟩ - sequenceV (map just v) - ≡⟨ lemma-just-sequence v ⟩ - just v ∎) + get (map (flip lookupM (h↦h′ h)) t) + ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩ + map (flip lookupM (h↦h′ h)) (get t) + ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩ + map (flip lookupM h) (get t) + ≈⟨ lemma-2 (get t) v h ph ⟩ + map just v ∎ where open SetoidReasoning open Get G s′ = enumerate s @@ -250,3 +236,17 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid t = enumeratel (Get.|gl₁| G j) h↦h′ = flip union (reshape g′ (Get.|gl₁| G j)) h′↦r = flip map t ∘ flip lookupM + +theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2′ G j s v u p = drop-just (begin + get <$> just u + ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩ + get <$> sequenceV (map just u) + ≡⟨ lemma-get-sequenceV G (lemma-just-sequence u) ⟩ + sequenceV (get (map just u)) + ≈⟨ sequence-cong (theorem-2 G j s v (map just u) p) ⟩ + sequenceV (map just v) + ≡⟨ lemma-just-sequence v ⟩ + just v ∎) + where open EqR (MaybeSetoid (VecISetoid A.setoid at _)) + open Get G diff --git a/Precond.agda b/Precond.agda index 45076f3..ead2e18 100644 --- a/Precond.agda +++ b/Precond.agda @@ -62,19 +62,26 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎ inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i) -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 i s v ≡ just (map just u) -assoc-enough G {i} s v (h , p) = _ , (begin +assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u +assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (|gl₁| j)))) p + where open Get G + g′ = delete-many (get (enumerate s)) (fromFunc (denumerate s)) + t = enumeratel (|gl₁| j) + +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 (enumeratel (Get.|gl₁| G i))) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (map just u) +assoc-enough′ G {i} s v (h , p) = _ , (begin bff G i s v - ≡⟨ cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩ - just (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t) - ≡⟨ cong (Maybe.just ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ - just (map (flip lookupM (union h g′)) t) - ≡⟨ cong (Maybe.just ∘ flip map t ∘ flip lookupM) (proj₂ wp) ⟩ - just (map (flip lookupM (fromFunc (proj₁ wp))) t) - ≡⟨ cong Maybe.just (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t) ⟩ - just (map (Maybe.just ∘ proj₁ wp) t) - ≡⟨ cong just (map-∘ just (proj₁ wp) t) ⟩ - just (map Maybe.just (map (proj₁ wp) t)) ∎) + ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩ + just (map (flip lookupM (union h (reshape g′ (|gl₁| i)))) t) + ≡⟨ cong just (begin _ + ≡⟨ cong (flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ + map (flip lookupM (union h g′)) t + ≡⟨ cong (flip map t ∘ flip lookupM) (proj₂ wp) ⟩ + map (flip lookupM (fromFunc (proj₁ wp))) t + ≡⟨ map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ + map (Maybe.just ∘ proj₁ wp) t + ≡⟨ map-∘ just (proj₁ wp) t ⟩ + map Maybe.just (map (proj₁ wp) t) ∎) ⟩ _ ∎) where open Get G s′ = enumerate s g = fromFunc (denumerate s) |