diff options
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 39 |
1 files changed, 19 insertions, 20 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 316d8b1..6a1300b 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -13,9 +13,8 @@ open import Data.Vec.Properties using (lookup∘update′) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary using (Setoid ; module DecSetoid) -open import Relation.Binary.Core using (refl ; _≡_ ; _≢_) import Relation.Binary.EqReasoning as EqR -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning) open import FinMap @@ -43,44 +42,44 @@ insertionresult i x h | nothing | [ il ] = new il lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m lemma-checkInsert-same i x m p with lookupM i m -lemma-checkInsert-same i x m refl | .(just x) with deq x x -lemma-checkInsert-same i x m refl | .(just x) | yes x≈x = refl -lemma-checkInsert-same i x m refl | .(just x) | no x≉x = contradiction A.refl x≉x +lemma-checkInsert-same i x m P.refl | .(just x) with deq x x +lemma-checkInsert-same i x m P.refl | .(just x) | yes x≈x = P.refl +lemma-checkInsert-same i x m P.refl | .(just x) | no x≉x = contradiction A.refl x≉x lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m) lemma-checkInsert-new i x m p with lookupM i m -lemma-checkInsert-new i x m refl | .nothing = refl +lemma-checkInsert-new i x m P.refl | .nothing = P.refl lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing lemma-checkInsert-wrong i x m x' d p with lookupM i m -lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x' -lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d -lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl +lemma-checkInsert-wrong i x m x' d P.refl | .(just x') with deq x x' +lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | yes q = contradiction q d +lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | no ¬q = P.refl lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is)) lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is) -lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (trans p (cong just (sym (lemma-lookupM-restrict i f is p))))) -lemma-checkInsert-restrict f i is | ._ | new _ = refl +lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = P.cong just (lemma-insert-same _ i (P.trans p (P.cong just (P.sym (lemma-lookupM-restrict i f is p))))) +lemma-checkInsert-restrict f i is | ._ | new _ = P.refl lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is p)) fi≉x lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h -lemma-lookupM-checkInsert i j h pl y refl | ._ | same _ _ _ = pl -lemma-lookupM-checkInsert i j h pl y ph' | ._ | new _ with i ≟ j -lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ()) -lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin +lemma-lookupM-checkInsert i j h pl y P.refl | ._ | same _ _ _ = pl +lemma-lookupM-checkInsert i j h pl y ph' | ._ | new _ with i ≟ j +lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes P.refl = contradiction (P.trans (P.sym pl) pl') (λ ()) +lemma-lookupM-checkInsert i j h {x} pl y P.refl | ._ | new _ | no i≢j = begin lookupM i (insert j y h) ≡⟨ lookup∘update′ i≢j h (just y) ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ - where open Relation.Binary.PropositionalEquality.≡-Reasoning + where open ≡-Reasoning lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _ lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h -lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y -lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl -lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y -lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lookup∘update′ i≢j h (just x) +lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y +lemma-lookupM-checkInsert-other i j i≢j x h P.refl | just y | yes x≈y = P.refl +lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y +lemma-lookupM-checkInsert-other i j i≢j x h P.refl | nothing = lookup∘update′ i≢j h (just x) |