From: Helmut Grohne Date: Thu, 9 Feb 2012 11:35:10 +0000 (+0100) Subject: started proving theorem-1 X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=commitdiff_plain;h=7309d04bb2eb5bfcbf9eb1e7f1f92fc1bdd470f2 started proving theorem-1 As in the bff paper expand s using lemma-map-denumerate-enumerate and apply free-theorem-list-list to commute get and map. --- diff --git a/Bidir.agda b/Bidir.agda index 0c9f0e5..db78f9e 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -131,4 +131,11 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin as ∎) theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (s : List τ) → bff get eq s (get s) ≡ just s -theorem-1 get eq s = {!!} +theorem-1 get eq s = begin + bff get eq s (get s) + ≡⟨ cong (bff get eq s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ + 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))) + ≡⟨ {!!} ⟩ + just s ∎