From 06408f9f1556b1eb88dcf2597e549fc122fdb508 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 22 Nov 2012 14:42:16 +0100 Subject: shorten line length of theorem-1 --- Bidir.agda | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index 853d70e..cc6f75f 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -168,19 +168,21 @@ theorem-1 get s = begin ≡⟨ cong (bff get s) (free-theorem get (denumerate s) (enumerate s)) ⟩ bff get s (map (denumerate s) (get (enumerate s))) ≡⟨ refl ⟩ - fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (denumerate s))) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s))))) - ≡⟨ cong (fmap (flip map (enumerate s) ∘ flip lookup) ∘ fmap (flip union (fromFunc (denumerate s)))) (lemma-1 (denumerate s) (get (enumerate s))) ⟩ - fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (flip lookupVec s))) (just (restrict (denumerate s) (toList (get (enumerate s)))))) + (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))) ⟩ + (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s)))) ≡⟨ refl ⟩ - just ((flip map (enumerate s) ∘ flip lookup) (union (restrict (denumerate s) (toList (get (enumerate s)))) (fromFunc (denumerate s)))) - ≡⟨ cong just (cong (flip map (enumerate s) ∘ flip lookup) (lemma-union-restrict (denumerate s) (toList (get (enumerate s))))) ⟩ - just ((flip map (enumerate s) ∘ flip lookup) (fromFunc (denumerate s))) + (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (fromFunc (denumerate s))) + ≡⟨ cong (h′↦r ∘ just) (lemma-union-restrict (denumerate s) (toList (get (enumerate s)))) ⟩ + (h′↦r ∘ just) (fromFunc (denumerate s)) ≡⟨ refl ⟩ just (map (flip lookup (fromFunc (denumerate s))) (enumerate s)) ≡⟨ cong just (map-cong (lookup∘tabulate (denumerate s)) (enumerate s)) ⟩ just (map (denumerate s) (enumerate s)) ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩ just s ∎ + where h↦h′ = fmap (flip union (fromFunc (denumerate s))) + h′↦r = fmap (flip map (enumerate s) ∘ flip lookupVec) lemma-fmap-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → fmap f ma ≡ just b → ∃ λ a → ma ≡ just a lemma-fmap-just {ma = just x} fmap-f-ma≡just-b = x , refl -- cgit v1.2.3