CheckInsert.agda

   1 open import Level using () renaming (zero to ℓ₀)
   2 open import Relation.Binary using (DecSetoid)
   3
   4 module CheckInsert (A : DecSetoid ℓ₀ ℓ₀) where
   5
   6 open import Data.Nat using (ℕ)
   7 open import Data.Fin using (Fin)
   8 open import Data.Fin.Properties using (_≟_)
   9 open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
  10 open import Data.Vec using (Vec) renaming (_∷_ to _∷V_)
  11 open import Data.Vec.Equality using () renaming (module Equality to VecEq)
  12 open import Data.Vec.Properties using (lookup∘update′)
  13 open import Relation.Nullary using (Dec ; yes ; no ; �_)
  14 open import Relation.Nullary.Negation using (contradiction)
  15 open import Relation.Binary using (Setoid ; module DecSetoid)
  16 import Relation.Binary.EqReasoning as EqR
  17 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; inspect ; [_] ; module ≡-Reasoning)
  18
  19 open import FinMap
  20
  21 private
  22   open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq)
  23
  24 checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier)
  25 checkInsert i b m with lookupM i m
  26 ...               | nothing = just (insert i b m)
  27 ...               | just c with deq b c
  28 ...                         | yes b≈c = just m
  29 ...                         | no b≉c  = nothing
  30
  31 data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where
  32   same : (x' : Carrier) → x ≈ x' → lookupM i h ≡ just x' → InsertionResult i x h (just h)
  33   new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h))
  34   wrong : (x' : Carrier) → ¬ (x ≈ x') → lookupM i h ≡ just x' → InsertionResult i x h nothing
  35
  36 insertionresult : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → InsertionResult i x h (checkInsert i x h)
  37 insertionresult i x h with lookupM i h | inspect (lookupM i) h
  38 insertionresult i x h | just x' | _ with deq x x'
  39 insertionresult i x h | just x' | [ il ] | yes x≈x' = same x' x≈x' il
  40 insertionresult i x h | just x' | [ il ] | no x≉x' = wrong x' x≉x' il
  41 insertionresult i x h | nothing | [ il ] = new il
  42
  43 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
  44 lemma-checkInsert-same i x m p with lookupM i m
  45 lemma-checkInsert-same i x m P.refl | .(just x) with deq x x
  46 lemma-checkInsert-same i x m P.refl | .(just x) | yes x≈x = P.refl
  47 lemma-checkInsert-same i x m P.refl | .(just x) | no x≉x = contradiction A.refl x≉x
  48
  49 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)
  50 lemma-checkInsert-new i x m p with lookupM i m
  51 lemma-checkInsert-new i x m P.refl | .nothing = P.refl
  52
  53 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
  54 lemma-checkInsert-wrong i x m x' d p with lookupM i m
  55 lemma-checkInsert-wrong i x m x' d P.refl | .(just x') with deq x x'
  56 lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | yes q = contradiction q d
  57 lemma-checkInsert-wrong i x m x' d P.refl | .(just x') | no �q = P.refl
  58
  59 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))
  60 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
  61 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)))))
  62 lemma-checkInsert-restrict f i is | ._ | new _ = P.refl
  63 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
  64
  65 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
  66 lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h
  67 lemma-lookupM-checkInsert i j h     pl y P.refl | ._ | same _ _ _ = pl
  68 lemma-lookupM-checkInsert i j h     pl y ph'    | ._ | new _ with i ≟ j
  69 lemma-lookupM-checkInsert i .i h    pl y ph'    | ._ | new pl' | yes P.refl = contradiction (P.trans (P.sym pl) pl') (λ ())
  70 lemma-lookupM-checkInsert i j h {x} pl y P.refl | ._ | new _ | no i≢j = begin
  71   lookupM i (insert j y h)
  72     ≡⟨ lookup∘update′ i≢j h (just y) ⟩
  73   lookupM i h
  74     ≡⟨ pl ⟩
  75   just x ∎
  76   where open ≡-Reasoning
  77
  78 lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _
  79
  80 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
  81 lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
  82 lemma-lookupM-checkInsert-other i j i≢j x h ph'    | just y with deq x y
  83 lemma-lookupM-checkInsert-other i j i≢j x h P.refl | just y | yes x≈y = P.refl
  84 lemma-lookupM-checkInsert-other i j i≢j x h ()     | just y | no x≉y
  85 lemma-lookupM-checkInsert-other i j i≢j x h P.refl | nothing = lookup∘update′ i≢j h (just x)