sym result of lemma-lookupM-{i,checkI}nsert-other
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 16 Oct 2014 08:57:31 +0000 (10:57 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 16 Oct 2014 08:57:31 +0000 (10:57 +0200)
Typically we have the complex term on the LHS and the simplified term on
the RHS. These lemmata did it otherwise and by symming them, we save two
syms.

CheckInsert.agda
FinMap.agda
Precond.agda

index 9dc8a60..52dffc4 100644 (file)
@@ -70,7 +70,7 @@ 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 = contradiction (trans (sym 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)
 lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = contradiction (trans (sym 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 i≢j) ⟩
+    ≡⟨ lemma-lookupM-insert-other i j y h i≢j ⟩
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
@@ -78,7 +78,7 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i
 
 lemma-lookupM-checkInsert i j x y h h' pl () | ._ | wrong _ _ _
 
 
 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 : {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 y | yes x≈y = refl
 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 y | yes x≈y = refl
index 05b251e..f9572b8 100644 (file)
@@ -70,7 +70,7 @@ lemma-lookupM-insert : {A : Set} {n : ℕ} → (i : Fin n) → (a : A) → (m :
 lemma-lookupM-insert zero    a (x ∷ xs) = refl
 lemma-lookupM-insert (suc i) a (x ∷ xs) = lemma-lookupM-insert i a xs
 
 lemma-lookupM-insert zero    a (x ∷ xs) = refl
 lemma-lookupM-insert (suc i) a (x ∷ xs) = lemma-lookupM-insert i a xs
 
-lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i m ≡ lookupM i (insert j a m)
+lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i (insert j a m) ≡ lookupM i m
 lemma-lookupM-insert-other zero    zero    a m        p = contradiction refl p
 lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
 lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl
 lemma-lookupM-insert-other zero    zero    a m        p = contradiction refl p
 lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
 lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl
@@ -87,7 +87,7 @@ lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = just-injective (begin
    just a ∎)
 lemma-lookupM-restrict i f (i' ∷ is) a p | no i≢i' = lemma-lookupM-restrict i f is a (begin
   lookupM i (restrict f is)
    just a ∎)
 lemma-lookupM-restrict i f (i' ∷ is) a p | no i≢i' = lemma-lookupM-restrict i f is a (begin
   lookupM i (restrict f is)
-    ≡⟨ lemma-lookupM-insert-other i i' (f i') (restrict f is) i≢i' ⟩
+    ≡⟨ sym (lemma-lookupM-insert-other i i' (f i') (restrict f is) i≢i') ⟩
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
@@ -123,7 +123,7 @@ lemma-disjoint-union {n} {m} f t = lemma-tabulate-∘ (lemma-inner t)
           lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
           lemma-inner (t ∷ ts) x | no ¬p = begin
             maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts))))
           lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
           lemma-inner (t ∷ ts) x | no ¬p = begin
             maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts))))
-              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩
+              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p) ⟩
             maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts)))
               ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩
             maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts)))
             maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts)))
               ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩
             maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts)))
index 85c955c..8d2eab2 100644 (file)
@@ -100,7 +100,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
 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-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph) ⟩
+    ≡⟨ 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 ∎
   lookupM i h'
     ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩
   nothing ∎