rewrite checkInsert using "... |" notation
[~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 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