diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2015-07-02 11:51:37 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2015-07-02 11:51:37 +0200 |
| commit | ea60af21ae805f2b0921fe591210679935ce6556 (patch) | |
| tree | 0e688d1b54e2e8ce78872b2099eb541e52e2ee1b /FinMap.agda | |
| parent | 8c3cdca7cfe1173094ff42ca2f844a352153fc97 (diff) | |
| download | bidiragda-ea60af21ae805f2b0921fe591210679935ce6556.tar.gz | |
split lemma-union-not-used into lemma-exchange-maps
New type suggested by Janis Voigtländer.
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/FinMap.agda b/FinMap.agda index cbe24c5..ca7e73b 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -157,3 +157,7 @@ lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner maybe′ just (lookupM x (fromFunc f)) nothing ≡⟨ lemma-lookupM-fromFunc f x ⟩ just (f x) ∎ + +lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is +lemma-exchange-maps h≈h′ {[]} All.[] = refl +lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis) |