CheckInsert.agda

   1 open import Relation.Binary.Core using (Decidable ; _≡_)
   2
   3 module CheckInsert (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
   4
   5 open import Data.Nat using (ℕ)
   6 open import Data.Fin using (Fin)
   7 open import Data.Fin.Props using (_≟_)
   8 open import Data.Maybe using (Maybe ; nothing ; just)
   9 open import Data.List using (List ; [] ; _∷_)
  10 open import Relation.Nullary using (Dec ; yes ; no)
  11 open import Relation.Nullary.Negation using (contradiction)
  12 open import Relation.Binary.Core using (refl ; _≢_)
  13 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)
  14 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
  15
  16 open import FinMap
  17
  18 checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier)
  19 checkInsert i b m with lookupM i m
  20 ...               | nothing = just (insert i b m)
  21 ...               | just c with deq b c
  22 ...                         | yes b≡c = just m
  23 ...                         | no b≢c  = nothing
  24
  25 record checkInsertProof {n : ℕ} (i : Fin n) (x : Carrier) (m : FinMapMaybe n Carrier) (P : Set) : Set where
  26   field
  27      same : lookupM i m ≡ just x → P
  28      new : lookupM i m ≡ nothing → P
  29      wrong : (x' : Carrier) → x ≢ x' → lookupM i m ≡ just x'  → P
  30
  31 apply-checkInsertProof : {P : Set} {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → checkInsertProof i x m P → P
  32 apply-checkInsertProof i x m rp with lookupM i m | inspect (lookupM i) m
  33 apply-checkInsertProof i x m rp | just x' | il with deq x x'
  34 apply-checkInsertProof i x m rp | just .x | [ il ] | yes refl = checkInsertProof.same rp il
  35 apply-checkInsertProof i x m rp | just x' | [ il ] | no x≢x' = checkInsertProof.wrong rp x' x≢x' il
  36 apply-checkInsertProof i x m rp | nothing | [ il ] = checkInsertProof.new rp il
  37
  38 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
  39 lemma-checkInsert-same i x m p with lookupM i m
  40 lemma-checkInsert-same i x m refl | .(just x) with deq x x
  41 lemma-checkInsert-same i x m refl | .(just x) | yes refl = refl
  42 lemma-checkInsert-same i x m refl | .(just x) | no x≢x = contradiction refl x≢x
  43
  44 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)
  45 lemma-checkInsert-new i x m p with lookupM i m
  46 lemma-checkInsert-new i x m refl | .nothing = refl
  47
  48 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
  49 lemma-checkInsert-wrong i x m x' d p with lookupM i m
  50 lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x'
  51 lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d
  52 lemma-checkInsert-wrong i x m x' d refl | .(just x') | no �q = refl
  53
  54 record checkInsertEqualProof {n : ℕ} (i : Fin n) (x : Carrier) (m : FinMapMaybe n Carrier) (e : Maybe (FinMapMaybe n Carrier)) : Set where
  55   field
  56      same : lookupM i m ≡ just x → just m ≡ e
  57      new : lookupM i m ≡ nothing → just (insert i x m) ≡ e
  58      wrong : (x' : Carrier) → x ≢ x' → lookupM i m ≡ just x' → nothing ≡ e
  59
  60 lift-checkInsertProof : {n : ℕ} {i : Fin n} {x : Carrier} {m : FinMapMaybe n Carrier} {e : Maybe (FinMapMaybe n Carrier)} → checkInsertEqualProof i x m e → checkInsertProof i x m (checkInsert i x m ≡ e)
  61 lift-checkInsertProof {_} {i} {x} {m} o = record
  62   { same  = λ p → trans (lemma-checkInsert-same i x m p) (checkInsertEqualProof.same o p)
  63   ; new   = λ p → trans (lemma-checkInsert-new i x m p) (checkInsertEqualProof.new o p)
  64   ; wrong = λ x' q p → trans (lemma-checkInsert-wrong i x m x' q p) (checkInsertEqualProof.wrong o x' q p)
  65   }
  66
  67 lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ is))
  68 lemma-checkInsert-restrict f i is = apply-checkInsertProof i (f i) (restrict f is) (lift-checkInsertProof record
  69   { same  = λ lookupM≡justx → cong just (lemma-insert-same (restrict f is) i (f i) lookupM≡justx)
  70   ; new   = λ lookupM≡nothing → refl
  71   ; wrong = λ x' x≢x' lookupM≡justx' → contradiction (lemma-lookupM-restrict i f is x' lookupM≡justx') x≢x'
  72   })
  73
  74 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
  75 lemma-lookupM-checkInsert i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h
  76 lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j
  77 lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing (begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ (nothing ∎))
  78 lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no �p = begin
  79   lookupM i (insert j y h)
  80     ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩
  81   lookupM i h
  82     ≡⟨ pl ⟩
  83   just x ∎
  84 lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z
  85 lemma-lookupM-checkInsert i j x y h h' pl ph' | just .y | pl' | yes refl = begin
  86   lookupM i h'
  87     ≡⟨ cong (lookupM i) (just-injective (sym ph')) ⟩
  88   lookupM i h
  89     ≡⟨ pl ⟩
  90   just x ∎
  91 lemma-lookupM-checkInsert i j x y h h' pl () | just z | pl' | no �p