diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-04-20 12:15:33 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-04-20 12:15:33 +0200 |
| commit | 1a8af12f97732cf087264f79483ee1d9aa035b3d (patch) | |
| tree | 50a9a41ac4aaf876cb053b988ff4d51c5d114050 /Bidir.agda | |
| parent | b2eb5eef26787fcb9ff0778f82473b0fc2dc4caa (diff) | |
| download | bidiragda-1a8af12f97732cf087264f79483ee1d9aa035b3d.tar.gz | |
remove lemma-\in-lookupM-assoc
It is a special case of lemma-assoc-domain.
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 16 |
1 files changed, 1 insertions, 15 deletions
@@ -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 |