diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-10 11:09:38 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-10 11:09:38 +0100 |
| commit | d42ffc9d24adb2b416ff73708ae64c1d4ca50c30 (patch) | |
| tree | 48b105cf1f30c79c4a9869d954bdeb9c652e30f2 /CheckInsert.agda | |
| parent | 400b30320b90620e47a16f3f1ec4ce3dad37e8b0 (diff) | |
| download | bidiragda-d42ffc9d24adb2b416ff73708ae64c1d4ca50c30.tar.gz | |
reduce a precondition of lemma-checkInsert-lookupM
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 796bece..4083720 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -85,14 +85,9 @@ 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 ∎ +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 +lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y +lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just .x | yes refl = refl +lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≢y +lemma-lookupM-checkInsert-other i j i≢j x h .(insert j x h) refl | nothing = lemma-lookupM-insert-other i j x h i≢j |