diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-05 11:59:31 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-05 11:59:31 +0100 |
| commit | 2b05019648523ab260b21e8f0199447b8124d332 (patch) | |
| tree | a6d37ef742d1de8fd85e04a67a21833ee26b73f4 | |
| parent | 87e863b864a75d89bb54f1f7a5522d24f0fa75fc (diff) | |
| download | bidiragda-2b05019648523ab260b21e8f0199447b8124d332.tar.gz | |
shrink lemma-tabulate-\circ using cong\_2
| -rw-r--r-- | FinMap.agda | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/FinMap.agda b/FinMap.agda index 861076a..2b50920 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -12,7 +12,7 @@ open import Function using (id ; _∘_ ; flip) open import Relation.Nullary using (yes ; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Core using (_≡_ ; refl ; _≢_) -open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans) +open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans ; cong₂) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) FinMapMaybe : ℕ → Set → Set @@ -93,12 +93,7 @@ lemma-lookupM-restrict i f (i' ∷ is) a p | no ¬p2 = lemma-lookupM-restrict i lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl -lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = begin - f zero ∷ tabulate (f ∘ suc) - ≡⟨ cong (flip Vec._∷_ (tabulate (f ∘ suc))) (f≗g zero) ⟩ - g zero ∷ tabulate (f ∘ suc) - ≡⟨ cong (Vec._∷_ (g zero)) (lemma-tabulate-∘ (f≗g ∘ suc)) ⟩ - g zero ∷ tabulate (g ∘ suc) ∎ +lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗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 {n} f is = begin |