From e0f83c9ca1816a4c0b3c030bb2cd562156311ecd Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 9 Feb 2012 14:59:32 +0100 Subject: [PATCH] prove theorem-1 assuming a lemma-union-generate --- Bidir.agda | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index db78f9e..4e7d46e 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -4,9 +4,9 @@ open import Data.Nat using (ℕ) open import Data.Fin using (Fin) open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) open import Data.List using (List ; [] ; _∷_ ; map ; length) -open import Data.List.Properties using () renaming (map-compose to map-∘) +open import Data.List.Properties using (map-cong) renaming (map-compose to map-∘) open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec ; _∷_ to _∷V_) -open import Data.Vec.Properties using (tabulate-∘) +open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate) open import Function using (id ; _∘_ ; flip) open import Relation.Nullary using (Dec ; yes ; no) open import Relation.Nullary.Negation using (contradiction) @@ -130,6 +130,9 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin ≡⟨ lemma-map-denumerate-enumerate as ⟩ as ∎) +lemma-union-generate : {A : Set} {n : ℕ} → (f : Fin n → A) → (is : List (Fin n)) → union (generate f is) (fromFunc f) ≡ fromFunc f +lemma-union-generate f is = {!!} + theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (s : List τ) → bff get eq s (get s) ≡ just s theorem-1 get eq s = begin bff get eq s (get s) @@ -137,5 +140,17 @@ theorem-1 get eq s = begin bff get eq s (get (map (denumerate s) (enumerate s))) ≡⟨ cong (bff get eq s) (free-theorem-list-list get (denumerate s) (enumerate s)) ⟩ bff get eq s (map (denumerate s) (get (enumerate s))) - ≡⟨ {!!} ⟩ + ≡⟨ refl ⟩ + fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (denumerate s))) (assoc eq (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 eq (denumerate s) (get (enumerate s))) ⟩ + fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (flip lookupVec (fromList s)))) (just (generate (denumerate s) (get (enumerate s))))) + ≡⟨ refl ⟩ + just ((flip map (enumerate s) ∘ flip lookup) (union (generate (denumerate s) (get (enumerate s))) (fromFunc (denumerate s)))) + ≡⟨ cong just (cong (flip map (enumerate s) ∘ flip lookup) (lemma-union-generate (denumerate s) (get (enumerate s)))) ⟩ + just ((flip map (enumerate s) ∘ flip lookup) (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 ∎ -- 2.20.1