remove lemma-\in-lookupM-assoc
authorHelmut Grohne <helmut@subdivi.de>
Fri, 20 Apr 2012 10:15:33 +0000 (12:15 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 20 Apr 2012 10:15:33 +0000 (12:15 +0200)
It is a special case of lemma-assoc-domain.

Bidir.agda

index ebe6f27..9bb2952 100644 (file)
@@ -143,20 +143,6 @@ lemma-lookupM-checkInsert eq i j x y h h' pl ph' | just .y | pl' | yes refl = be
   just x βˆŽ
 lemma-lookupM-checkInsert eq i j x y h h' pl () | just z | pl' | no ¬p
 
-lemma-∈-lookupM-assoc : {A : Set} {n : β„•} β†’ (eq : EqInst A) β†’ (i : Fin n) β†’ (is : List (Fin n)) β†’ (xs : List A) β†’ (h : FinMapMaybe n A) β†’ assoc eq is xs β‰‘ just h β†’ (i βˆˆ is) β†’ (βˆƒ Ξ» x β†’ lookupM i h β‰‘ just x)
-lemma-∈-lookupM-assoc eq i [] [] h ph ()
-lemma-∈-lookupM-assoc eq i (i' βˆ· is) [] h () i∈is
-lemma-∈-lookupM-assoc eq i [] (x βˆ· xs) h () i∈is
-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 | ph'
-lemma-∈-lookupM-assoc eq i (.i βˆ· is) (x βˆ· xs) h ph (here refl) | just h' | ph' with lookupM i h' | inspect (lookupM i) h'
-lemma-∈-lookupM-assoc eq i (.i βˆ· is) (x βˆ· xs) h ph (here refl) | just h' | ph' | just x' | px with eq x x' 
-lemma-∈-lookupM-assoc eq i (.i βˆ· is) (x βˆ· xs) h refl (here refl) | just .h | ph' | just .x | Reveal_is_.[_] px | yes refl = x , px
-lemma-∈-lookupM-assoc eq i (.i βˆ· is) (x βˆ· xs) h () (here refl) | just h' | ph' | just x' | px | no Β¬p
-lemma-∈-lookupM-assoc eq i (.i βˆ· is) (x βˆ· xs) .(insert i x h') refl (here refl) | just h' | ph' | nothing | px = x , lemma-lookupM-insert i x h'
-lemma-∈-lookupM-assoc eq i (i' βˆ· is) (x βˆ· xs) h ph (there pxs) | just h' | Reveal_is_.[_] ph' with lemma-∈-lookupM-assoc eq i is xs h' ph' pxs
-lemma-∈-lookupM-assoc eq i (i' βˆ· is) (x βˆ· xs) h ph (there pxs) | just h' | Reveal_is_.[_] ph' | x' , px' = x' , lemma-lookupM-checkInsert eq i i' x' x h' h px' ph
-
 lemma-βˆ‰-lookupM-assoc : {A : Set} {n : β„•} β†’ (eq : EqInst A) β†’ (i : Fin n) β†’ (is : List (Fin n)) β†’ (xs : List A) β†’ (h : FinMapMaybe n A) β†’ assoc eq is xs β‰‘ just h β†’ (i βˆ‰ is) β†’ lookupM i h β‰‘ nothing
 lemma-βˆ‰-lookupM-assoc eq i []         []         h ph iβˆ‰is = begin
   lookupM i h
@@ -223,7 +209,7 @@ lemma-map-lookupM-assoc eq i []         x []         h h' ph' ph = refl
 lemma-map-lookupM-assoc eq i []         x (x' βˆ· xs') h h' ()  ph
 lemma-map-lookupM-assoc eq i (i' βˆ· is') x []         h h' ()  ph
 lemma-map-lookupM-assoc eq i (i' βˆ· is') x (x' βˆ· xs') h h' ph' ph with any (_β‰Ÿ_ i) (i' βˆ· is')
-lemma-map-lookupM-assoc eq i (i' βˆ· is') x (x' βˆ· xs') h h' ph' ph | yes p with lemma-∈-lookupM-assoc eq i (i' βˆ· is') (x' βˆ· xs') h' ph' p
+lemma-map-lookupM-assoc eq i (i' βˆ· is') x (x' βˆ· xs') h h' ph' ph | yes p with Data.List.All.lookup (lemma-assoc-domain eq (i' βˆ· is') (x' βˆ· xs') h' ph') p
 lemma-map-lookupM-assoc eq i (i' βˆ· is') x (x' βˆ· xs') h h' ph' ph | yes p | (x'' , p') with lookupM i h' 
 lemma-map-lookupM-assoc eq i (i' βˆ· is') x (x' βˆ· xs') h h' ph' ph | yes p | (x'' , refl) | .(just x'') with eq x x''
 lemma-map-lookupM-assoc eq i (i' βˆ· is') x (x' βˆ· xs') h .h ph' refl | yes p | (.x , refl) | .(just x)  | yes refl = refl