From 99e4f3024fd5542b6f33ed3b756db6eb97201c39 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 17 Sep 2012 22:17:02 +0200 Subject: save a with in lemma-\inn-lookupM-assoc Since \negp can be written as i\innis \circ here. --- Bidir.agda | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index c7171a4..50e3fae 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -68,11 +68,9 @@ lemma-∉-lookupM-assoc eq i [] [] h ph i∉is = begin nothing ∎ lemma-∉-lookupM-assoc eq i [] (x' ∷ xs') h () i∉is lemma-∉-lookupM-assoc eq i (i' ∷ is') [] h () i∉is -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is with i ≟ i' -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | yes p = contradiction (here p) i∉is -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p with assoc eq is' xs' | inspect (assoc eq is') xs' -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h () i∉is | no ¬p | nothing | Reveal_is_.[_] ph' -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p | just h' | Reveal_is_.[_] ph' = apply-checkInsertProof eq i' x' h' record { +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc eq is' xs' | inspect (assoc eq is') xs' +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | Reveal_is_.[_] ph' +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | Reveal_is_.[_] ph' = apply-checkInsertProof eq i' x' h' record { same = λ lookupM-i'-h'≡just-x' → begin lookupM i h ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-same eq i' x' h' lookupM-i'-h'≡just-x'))) ⟩ @@ -83,7 +81,7 @@ lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p | ju lookupM i h ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-new eq i' x' h' lookupM-i'-h'≡nothing))) ⟩ lookupM i (insert i' x' h') - ≡⟨ sym (lemma-lookupM-insert-other i i' x' h' ¬p) ⟩ + ≡⟨ sym (lemma-lookupM-insert-other i i' x' h' (i∉is ∘ here)) ⟩ lookupM i h' ≡⟨ lemma-∉-lookupM-assoc eq i is' xs' h' ph' (i∉is ∘ there) ⟩ nothing ∎ -- cgit v1.2.3