diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-09 23:26:46 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-10 00:09:03 +0100 |
| commit | 3badfdc549d717824f72b0c1df35c52e00ce6dbf (patch) | |
| tree | 2eb6f5f1d0296a9b0a3dae75605e5e37d525fabe | |
| parent | ec47ee14b9154410b7c72fb067671ea79fd71523 (diff) | |
| download | bidiragda-3badfdc549d717824f72b0c1df35c52e00ce6dbf.tar.gz | |
add new lemma-checkInsert-lookupM
Suggested by Joachim Breitner.
| -rw-r--r-- | CheckInsert.agda | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 7e3f3aa..796bece 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -84,3 +84,15 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no 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-checkInsert-lookupM : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (r : Maybe Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h' ≡ r → checkInsert j x h ≡ just h' → lookupM i h ≡ r +lemma-checkInsert-lookupM i j i≢j x r h h' pl ph' with lookupM j h +lemma-checkInsert-lookupM i j i≢j x r h h' pl ph' | just y with deq x y +lemma-checkInsert-lookupM i j i≢j x r h .h pl refl | just .x | yes refl = pl +lemma-checkInsert-lookupM i j i≢j x r h h' pl () | just y | no x≢y +lemma-checkInsert-lookupM i j i≢j x r h .(insert j x h) pl refl | nothing = begin + lookupM i h + ≡⟨ lemma-lookupM-insert-other i j x h i≢j ⟩ + lookupM i (insert j x h) + ≡⟨ pl ⟩ + r ∎ |