drop the insert- prefix from the insertionresult ctors
[~helmut/bidiragda.git] / 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 data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where
26   same : lookupM i h ≡ just x → InsertionResult i x h (just h)
27   new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h))
28   wrong : (x' : Carrier) → x ≢ x' → lookupM i h ≡ just x' → InsertionResult i x h nothing
29
30 insertionresult : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → InsertionResult i x h (checkInsert i x h)
31 insertionresult i x h with lookupM i h | inspect (lookupM i) h
32 insertionresult i x h | just x' | _ with deq x x'
33 insertionresult i x h | just .x | [ il ] | yes refl = same il
34 insertionresult i x h | just x' | [ il ] | no x≢x' = wrong x' x≢x' il
35 insertionresult i x h | nothing | [ il ] = new il
36
37 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
38 lemma-checkInsert-same i x m p with lookupM i m
39 lemma-checkInsert-same i x m refl | .(just x) with deq x x
40 lemma-checkInsert-same i x m refl | .(just x) | yes refl = refl
41 lemma-checkInsert-same i x m refl | .(just x) | no x≢x = contradiction refl x≢x
42
43 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)
44 lemma-checkInsert-new i x m p with lookupM i m
45 lemma-checkInsert-new i x m refl | .nothing = refl
46
47 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
48 lemma-checkInsert-wrong i x m x' d p with lookupM i m
49 lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x'
50 lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d
51 lemma-checkInsert-wrong i x m x' d refl | .(just x') | no q = refl
52
53 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))
54 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
55 lemma-checkInsert-restrict f i is | ._ | same p = cong just (lemma-insert-same _ i (f i) p)
56 lemma-checkInsert-restrict f i is | ._ | new _ = refl
57 lemma-checkInsert-restrict f i is | ._ | wrong x fi≢x p = contradiction (lemma-lookupM-restrict i f is x p) fi≢x
58
59 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
60 lemma-lookupM-checkInsert i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h
61 lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j
62 lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing pl pl'
63 lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no p = begin
64   lookupM i (insert j y h)
65     ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩
66   lookupM i h
67     ≡⟨ pl ⟩
68   just x ∎
69 lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z
70 lemma-lookupM-checkInsert i j x y h .h pl refl | just .y | pl' | yes refl = pl
71 lemma-lookupM-checkInsert i j x y h h' pl () | just z | pl' | no p
72
73 lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h ≡ lookupM i h'
74 lemma-lookupM-checkInsert-other i j i≢j x h h' ph' with lookupM j h
75 lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y
76 lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just .x | yes refl = refl
77 lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≢y
78 lemma-lookupM-checkInsert-other i j i≢j x h .(insert j x h) refl | nothing = lemma-lookupM-insert-other i j x h i≢j