diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-18 08:28:08 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-18 08:28:08 +0200 |
| commit | 511c9d49c5f9dc4e3df11d718bd98a95acc77a7d (patch) | |
| tree | 65ba13c84a25e140698eca8e1655fc4acb1c279d /CheckInsert.agda | |
| parent | 99e4f3024fd5542b6f33ed3b756db6eb97201c39 (diff) | |
| download | bidiragda-511c9d49c5f9dc4e3df11d718bd98a95acc77a7d.tar.gz | |
one more application of lemma-just\==nnothing
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 6c168e2..408a5b2 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -75,8 +75,7 @@ lemma-checkInsert-restrict {τ} eq f i is = apply-checkInsertProof eq i (f i) (r lemma-lookupM-checkInsert : {A : Set} {n : ℕ} → (eq : EqInst A) → (i j : Fin n) → (x y : A) → (h h' : FinMapMaybe n A) → lookupM i h ≡ just x → checkInsert eq j y h ≡ just h' → lookupM i h' ≡ just x lemma-lookupM-checkInsert eq i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j -lemma-lookupM-checkInsert eq i .i x y h .(insert i y h) pl refl | nothing | Reveal_is_.[_] pl' | yes refl with begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ nothing ∎ -... | () +lemma-lookupM-checkInsert eq i .i x y h .(insert i y h) pl refl | nothing | Reveal_is_.[_] pl' | yes refl = lemma-just≢nothing (begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ (nothing ∎)) lemma-lookupM-checkInsert eq 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) ⟩ |