From: Helmut Grohne Date: Thu, 26 Jan 2012 17:06:42 +0000 (+0100) Subject: recursion of lemma-2 X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=commitdiff_plain;h=3b01996ba5cc0037f1375d6784c33b3bbd2b7589 recursion of lemma-2 --- diff --git a/Bidir.agda b/Bidir.agda index 3123d5d..6bb6608 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -73,13 +73,22 @@ lemma-2 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (is : List (Fin n)) → lemma-2 eq [] [] h p = refl lemma-2 eq [] (x ∷ xs) h () lemma-2 eq (x ∷ xs) [] h () -lemma-2 eq (i ∷ is) (x ∷ xs) h p = begin +lemma-2 eq (i ∷ is) (x ∷ xs) h p with assoc eq is xs | inspect (assoc eq is) xs +lemma-2 eq (i ∷ is) (x ∷ xs) h () | nothing | _ +lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin map (flip lookupM h) (i ∷ is) ≡⟨ refl ⟩ lookup i h ∷ map (flip lookupM h) is - ≡⟨ cong (flip _∷_ (map (flip lookup h) is)) (lemma-lookupM-assoc eq i is x xs h p) ⟩ + ≡⟨ cong (flip _∷_ (map (flip lookup h) is)) (lemma-lookupM-assoc eq i is x xs h (begin + assoc eq (i ∷ is) (x ∷ xs) + ≡⟨ cong (flip _>>=_ (checkInsert eq i x)) ir ⟩ + checkInsert eq i x h' + ≡⟨ p ⟩ + just h ∎) ) ⟩ just x ∷ map (flip lookupM h) is - ≡⟨ cong (_∷_ (just x)) (lemma-2 eq is xs h {!!}) ⟩ + ≡⟨ cong (_∷_ (just x)) {!!} ⟩ + just x ∷ map (flip lookupM h') is + ≡⟨ cong (_∷_ (just x)) (lemma-2 eq is xs h' ir) ⟩ just x ∷ map just xs ≡⟨ refl ⟩ map just (x ∷ xs) ∎