diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-02-01 13:13:01 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-02-01 13:13:01 +0100 |
| commit | 9b158c066d8801b6bf4bfb007702a076b017efd3 (patch) | |
| tree | 5e1c4c42a68c7b449e5a359fdd9386d0966e42da /CheckInsert.agda | |
| parent | df1c4f99c384e2e94c1e05ebf79e29947a6f5d83 (diff) | |
| download | bidiragda-9b158c066d8801b6bf4bfb007702a076b017efd3.tar.gz | |
employ insertionresult in lemma-lookupM-checkInsert
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 142cc61..6926587 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -57,18 +57,17 @@ lemma-checkInsert-restrict f i is | ._ | new _ = refl lemma-checkInsert-restrict f i is | ._ | wrong x fi≢x p = contradiction (lemma-lookupM-restrict i f is x p) fi≢x lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h ≡ just x → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x -lemma-lookupM-checkInsert i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h -lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j -lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing pl pl' -lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no ¬p = begin +lemma-lookupM-checkInsert i j x y h h' pl ph' with checkInsert j y h | insertionresult j y h +lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ = pl +lemma-lookupM-checkInsert i j x y h h' pl ph' | ._ | new _ with i ≟ j +lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = lemma-just≢nothing pl pl' +lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin lookupM i (insert j y h) - ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩ + ≡⟨ sym (lemma-lookupM-insert-other i j y h i≢j) ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ -lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z -lemma-lookupM-checkInsert i j x y h .h pl refl | just .y | pl' | yes refl = pl -lemma-lookupM-checkInsert i j x y h h' pl () | just z | pl' | no ¬p +lemma-lookupM-checkInsert i j x y h h' pl () | ._ | wrong _ _ _ lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h ≡ lookupM i h' lemma-lookupM-checkInsert-other i j i≢j x h h' ph' with lookupM j h |