remove lemma-just≢nothing
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 15 Oct 2014 08:35:43 +0000 (10:35 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 15 Oct 2014 08:35:43 +0000 (10:35 +0200)
Special case of contradiction.

CheckInsert.agda
FinMap.agda

index 16bcc8e..9dc8a60 100644 (file)
@@ -67,7 +67,7 @@ lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) →
 lemma-lookupM-checkInsert i j x y h h' pl ph' with checkInsert j y h | insertionresult j y h
 lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ _ _ = pl
 lemma-lookupM-checkInsert i j x y h h' pl ph'  | ._ | new _ with i ≟ j
-lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = lemma-just≢nothing pl pl'
+lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
 lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin
   lookupM i (insert j y h)
     ≡⟨ sym (lemma-lookupM-insert-other i j y h i≢j) ⟩
index c8b078c..05b251e 100644 (file)
@@ -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)