diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-11-22 15:20:29 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-11-22 15:20:29 +0100 |
| commit | e309253739ad0e3d9172e0b29156a5c88bbc9dbb (patch) | |
| tree | d4613832c8edc390fd229e8c1f583b83775af359 /FinMap.agda | |
| parent | b9ce912e6a50be76ad2495fb110a79e93c591401 (diff) | |
| download | bidiragda-e309253739ad0e3d9172e0b29156a5c88bbc9dbb.tar.gz | |
shorten line lengths lemma-union-restrict
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/FinMap.agda b/FinMap.agda index c085b24..bdead33 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -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 f 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 f [] 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 f (i ∷ is) j with j ≟ i - lemma-inner f (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (restrict f is)) - lemma-inner f (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 f is j ⟩ + ≡⟨ lemma-inner is j ⟩ f j ∎ |