shorten line lengths lemma-union-restrict
authorHelmut Grohne <helmut@subdivi.de>
Thu, 22 Nov 2012 14:20:29 +0000 (15:20 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 22 Nov 2012 14:20:29 +0000 (15:20 +0100)
FinMap.agda

index c085b24..bdead33 100644 (file)
@@ -101,14 +101,14 @@ lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = begin
   g zero ∷ tabulate (g ∘ suc) ∎
 
 lemma-union-restrict : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (restrict f is) (fromFunc f) ≡ fromFunc f
-lemma-union-restrict f is = begin
+lemma-union-restrict {n} f is = begin
   union (restrict f is) (fromFunc f)
     ≡⟨ refl ⟩
   tabulate (λ j → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)))
-    ≡⟨ lemma-tabulate-∘ (lemma-inner is) ⟩
+    ≡⟨ lemma-tabulate-∘ (lemma-inner is) ⟩
   tabulate f ∎
-    where lemma-inner : {n : ℕ} {A : Set} (f : Fin n → A) → (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j
-          lemma-inner []       j = begin
+    where lemma-inner : (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j
+          lemma-inner []       j = begin
             maybe′ id (lookup j (fromFunc f)) (lookupM j empty)
               ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-empty j) ⟩
             maybe′ id (lookup j (fromFunc f)) nothing
@@ -116,11 +116,11 @@ lemma-union-restrict f is = begin
             lookup j (fromFunc f)
               ≡⟨ lookup∘tabulate f j ⟩
             f j ∎
-          lemma-inner (i ∷ is)  j with j ≟ i
-          lemma-inner (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (restrict f is))
-          lemma-inner (i ∷ is)  j | no j≢i = begin
+          lemma-inner (i ∷ is)  j with j ≟ i
+          lemma-inner (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (restrict f is))
+          lemma-inner (i ∷ is)  j | no j≢i = begin
             maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is)))
               ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) j≢i)) ⟩
             maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is))
-              ≡⟨ lemma-inner is j ⟩
+              ≡⟨ lemma-inner is j ⟩
             f j ∎