diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-14 13:13:00 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-14 13:13:00 +0100 |
| commit | 9c2be74a5369c1bdb737a67c7c508cb50c62bd83 (patch) | |
| tree | 4b2972936dc6377e2df28b6da3b3485a50296813 /CheckInsert.agda | |
| parent | a01871259837d6e36c580338f6d29ea0b154ed04 (diff) | |
| download | bidiragda-9c2be74a5369c1bdb737a67c7c508cb50c62bd83.tar.gz | |
define a more useful version of lemma-just\==nnothing
If one had a parameter of type just x \== nothing it could be simply
refuted by case splitting. So the cases where lemma-just\==nnothing was
used always employed trans to combine two results. The new version takes
both results instead.
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 4083720..dd752be 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -74,7 +74,7 @@ lemma-checkInsert-restrict f i is = apply-checkInsertProof i (f i) (restrict f i lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h ≡ just x → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x lemma-lookupM-checkInsert i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j -lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing (trans (sym pl) pl') +lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing pl pl' lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no ¬p = begin lookupM i (insert j y h) ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩ |