diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-15 10:35:43 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-15 10:35:43 +0200 |
| commit | d2548922c7abb20fee5633be6e654430517555af (patch) | |
| tree | 1d4d3c38c6f0f3b4832cb4d5135f6fea8b7f057a /FinMap.agda | |
| parent | b1b80567288030782231418407e7244b37227450 (diff) | |
| download | bidiragda-d2548922c7abb20fee5633be6e654430517555af.tar.gz | |
remove lemma-just≢nothing
Special case of contradiction.
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/FinMap.agda b/FinMap.agda index c8b078c..05b251e 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -57,9 +57,6 @@ delete i m = m [ i ]≔ nothing delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A delete-many = flip (foldr (const _) delete) -lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever -lemma-just≢nothing refl () - lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → (a : A) → lookupM f m ≡ just a → m ≡ insert f a m lemma-insert-same [] () a p lemma-insert-same {suc n} (x ∷ xs) zero a p = cong (flip _∷_ xs) p @@ -80,7 +77,7 @@ 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 (p ∘ cong suc) lemma-lookupM-restrict : {A : Set} {n : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a -lemma-lookupM-restrict i f [] a p = lemma-just≢nothing p (lemma-lookupM-empty i) +lemma-lookupM-restrict i f [] a p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ()) lemma-lookupM-restrict i f (i' ∷ is) a p with i ≟ i' lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = just-injective (begin just (f i) |