reduce usage of sym
authorHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 14:22:09 +0000 (15:22 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 14:22:09 +0000 (15:22 +0100)
Try to always construct statements of the form
  complex expression \== simple expression.

Bidir.agda

index 274710f..bc00eea 100644 (file)
@@ -71,20 +71,20 @@ assoc _  _        _        = nothing
 generate : {A : Set} {n : â„•} â†’ (Fin n â†’ A) â†’ List (Fin n) â†’ FinMapMaybe n A
 generate f is = fromAscList (zip is (map f is))
 
-lemma-insert-same : {Ï„ : Set} {n : â„•} â†’ (m : FinMapMaybe n Ï„) â†’ (f : Fin n) â†’ (a : Ï„) â†’ just a â‰¡ lookupM f m â†’ m â‰¡ insert f a m
+lemma-insert-same : {Ï„ : Set} {n : â„•} â†’ (m : FinMapMaybe n Ï„) â†’ (f : Fin n) â†’ (a : Ï„) â†’ lookupM f m â‰¡ just a â†’ m â‰¡ insert f a m
 lemma-insert-same []               ()      a p
 lemma-insert-same (.(just a) âˆ· xs) zero    a refl = refl
 lemma-insert-same (x âˆ· xs)         (suc i) a p    = cong (_∷_ x) (lemma-insert-same xs i a p)
 
-lemma-lookupM-empty : {A : Set} {n : â„•} â†’ (i : Fin n) â†’ nothing â‰¡ lookupM {A} i empty
+lemma-lookupM-empty : {A : Set} {n : â„•} â†’ (i : Fin n) â†’ lookupM {A} i empty â‰¡ nothing
 lemma-lookupM-empty zero    = refl
 lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
 
 lemma-from-just : {A : Set} â†’ {x y : A} â†’ _≡_ {_} {Maybe A} (just x) (just y) â†’ x â‰¡ y
 lemma-from-just refl = refl
 
-lemma-lookupM-insert : {A : Set} {n : â„•} â†’ (i : Fin n) â†’ (a : A) â†’ (m : FinMapMaybe n A) â†’ just a â‰¡ lookupM i (insert i a m)
-lemma-lookupM-insert zero    _ (_ âˆ· _)  = sym refl
+lemma-lookupM-insert : {A : Set} {n : â„•} â†’ (i : Fin n) â†’ (a : A) â†’ (m : FinMapMaybe n A) â†’ lookupM i (insert i a m) â‰¡ just a
+lemma-lookupM-insert zero    _ (_ âˆ· _)  = refl
 lemma-lookupM-insert (suc i) a (_ âˆ· 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)
@@ -93,40 +93,40 @@ 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 (suc i) (suc j) a (x âˆ· xs) p = lemma-lookupM-insert-other i j a xs (contraposition (cong suc) p)
 
-lemma-lookupM-generate : {A : Set} {n : â„•} â†’ (i : Fin n) â†’ (f : Fin n â†’ A) â†’ (is : List (Fin n)) â†’ (a : A) â†’ just a â‰¡ lookupM i (generate f is) â†’ a â‰¡ f i
+lemma-lookupM-generate : {A : Set} {n : â„•} â†’ (i : Fin n) â†’ (f : Fin n â†’ A) â†’ (is : List (Fin n)) â†’ (a : A) â†’ lookupM i (generate f is) â‰¡ just a â†’ f i â‰¡ a
 lemma-lookupM-generate {A} i f [] a p with begin
   just a
-    â‰¡âŸ¨ p âŸ©
+    â‰¡âŸ¨ sym p âŸ©
   lookupM i (generate f [])
     â‰¡âŸ¨ refl âŸ©
   lookupM i empty
-    â‰¡âŸ¨ sym (lemma-lookupM-empty i) âŸ©
+    â‰¡âŸ¨ lemma-lookupM-empty i âŸ©
   nothing âˆŽ
 lemma-lookupM-generate i f [] a p | ()
 lemma-lookupM-generate i f (i' âˆ· is) a p with i â‰ŸF i'
 lemma-lookupM-generate i f (.i âˆ· is) a p | yes refl = lemma-from-just (begin
-   just a
-     â‰¡âŸ¨ p âŸ©
-   lookupM i (generate f (i âˆ· is))
-     â‰¡âŸ¨ refl âŸ©
-   lookupM i (insert i (f i) (generate f is))
+   just (f i)
      â‰¡âŸ¨ sym (lemma-lookupM-insert i (f i) (generate f is)) âŸ©
-   just (f i) âˆŽ)
+   lookupM i (insert i (f i) (generate f is))
+     â‰¡âŸ¨ refl âŸ©
+   lookupM i (generate f (i âˆ· is))
+     â‰¡âŸ¨ p âŸ©
+   just a âˆŽ)
 lemma-lookupM-generate i f (i' âˆ· is) a p | no Â¬p2 = lemma-lookupM-generate i f is a (begin
-  just a
-    â‰¡âŸ¨ p âŸ©
-  lookupM i (generate f (i' âˆ· is))
-    â‰¡âŸ¨ refl âŸ©
+  lookupM i (generate f is)
+    â‰¡âŸ¨ lemma-lookupM-insert-other i i' (f i') (generate f is) Â¬p2 âŸ©
   lookupM i (insert i' (f i') (generate f is))
-    â‰¡âŸ¨ sym (lemma-lookupM-insert-other i i' (f i') (generate f is) Â¬p2) âŸ©
-  lookupM i (generate f is) âˆŽ)
+    â‰¡âŸ¨ refl âŸ©
+  lookupM i (generate f (i' âˆ· is))
+    â‰¡âŸ¨ p âŸ©
+  just a âˆŽ)
 
 lemma-checkInsert-generate : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (f : Fin n â†’ Ï„) â†’ (i : Fin n) â†’ (is : List (Fin n)) â†’ checkInsert eq i (f i) (generate f is) â‰¡ just (generate f (i âˆ· is))
 lemma-checkInsert-generate eq f i is with lookupM i (generate f is) | inspect (lookupM i) (generate f is)
 lemma-checkInsert-generate eq f i is | nothing | _ = refl
-lemma-checkInsert-generate eq f i is | just x | Reveal_is_.[_] prf with lemma-lookupM-generate i f is x (sym prf)
+lemma-checkInsert-generate eq f i is | just x | Reveal_is_.[_] prf with lemma-lookupM-generate i f is x prf
 lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl with eq (f i) (f i)
-lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | yes refl = cong just (lemma-insert-same (generate f is) i (f i) (sym prf))
+lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | yes refl = cong just (lemma-insert-same (generate f is) i (f i) prf)
 lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | no ¬p = contradiction refl ¬p
 
 lemma-1 : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (f : Fin n â†’ Ï„) â†’ (is : List (Fin n)) â†’ assoc eq is (map f is) â‰¡ just (generate f is)