CheckInsert.agda

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