reduce a precondition of lemma-checkInsert-lookupM
authorHelmut Grohne <helmut@subdivi.de>
Thu, 10 Jan 2013 10:09:38 +0000 (11:09 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 10 Jan 2013 10:09:38 +0000 (11:09 +0100)
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.

Bidir.agda
CheckInsert.agda

index 901e2d1..3dbdbdd 100644 (file)
@@ -62,7 +62,7 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc is' x
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | [ ph' ]
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = begin
   lookupM i h
-    ≡⟨ sym (lemma-checkInsert-lookupM i i' (i∉is ∘ here) x' (lookupVec i h) h' h refl ph) ⟩
+    ≡⟨ sym (lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph) ⟩
   lookupM i h'
     ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩
   nothing ∎
index 796bece..4083720 100644 (file)
@@ -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