reorganize equality imports
[~helmut/bidiragda.git] / 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)