diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2013-12-17 08:49:24 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2013-12-17 08:49:24 +0100 |
| commit | 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 (patch) | |
| tree | 434e67b2e485bee51268cedef1b417424466f958 /Bidir.agda | |
| parent | 066861f9cdde4ded6c5442508bef1a27576c68d7 (diff) | |
| download | bidiragda-88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907.tar.gz | |
refactor to get rid of FinMap without Maybe entirely
The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -113,20 +113,20 @@ theorem-1 get s = begin ≡⟨ 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 ⟩ - (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ - (h′↦r ∘ just) (partialize (fromFunc (denumerate s))) + (h′↦r ∘ just) (fromFunc (denumerate s)) ≡⟨ refl ⟩ - mapMV (flip lookupVec (partialize (fromFunc (denumerate s)))) (enumerate s) - ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-partialize-fromFunc (denumerate s)) ⟩ - mapMV (flip lookupVec (fromFunc (Maybe.just ∘ denumerate s))) (enumerate s) + mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s) + ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩ + mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s) ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ denumerate s)) (enumerate s) ⟩ mapMV (Maybe.just ∘ denumerate s) (enumerate s) ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩ just (map (denumerate s) (enumerate s)) ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩ just s ∎ - where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) |