formulate theorem-2
[~helmut/bidiragda.git] / Bidir.agda
1 module Bidir where
2
3 open import Data.Nat using (â„•)
4 open import Data.Fin using (Fin)
5 open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
6 open import Data.List using (List ; [] ; _∷_ ; map ; length)
7 open import Data.List.Properties using (map-cong) renaming (map-compose to map-∘)
8 open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec ; _∷_ to _∷V_)
9 open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate)
10 open import Function using (id ; _∘_ ; flip)
11 open import Relation.Nullary using (Dec ; yes ; no)
12 open import Relation.Nullary.Negation using (contradiction)
13 open import Relation.Binary.Core using (_≡_ ; refl)
14 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_)
15 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
16
17 open import FinMap
18
19 _>>=_ : {A B : Set} â†’ Maybe A â†’ (A â†’ Maybe B) â†’ Maybe B
20 _>>=_ = flip (flip maybe′ nothing)
21
22 fmap : {A B : Set} â†’ (A â†’ B) â†’ Maybe A â†’ Maybe B
23 fmap f = maybe′ (λ a â†’ just (f a)) nothing
24
25 EqInst : Set â†’ Set
26 EqInst A = (x y : A) â†’ Dec (x â‰¡ y)
27
28 checkInsert : {A : Set} {n : â„•} â†’ EqInst A â†’ Fin n â†’ A â†’ FinMapMaybe n A â†’ Maybe (FinMapMaybe n A)
29 checkInsert eq i b m with lookupM i m
30 checkInsert eq i b m | just c with eq b c
31 checkInsert eq i b m | just .b | yes refl = just m
32 checkInsert eq i b m | just c  | no ¬p    = nothing
33 checkInsert eq i b m | nothing = just (insert i b m)
34 assoc : {A : Set} {n : â„•} â†’ EqInst A â†’ List (Fin n) â†’ List A â†’ Maybe (FinMapMaybe n A)
35 assoc _  []       []       = just empty
36 assoc eq (i âˆ· is) (b âˆ· bs) = (assoc eq is bs) >>= (checkInsert eq i b)
37 assoc _  _        _        = nothing
38
39 lemma-checkInsert-generate : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (f : Fin n â†’ Ï„) â†’ (i : Fin n) â†’ (is : List (Fin n)) â†’ checkInsert eq i (f i) (generate f is) â‰¡ just (generate f (i âˆ· is))
40 lemma-checkInsert-generate eq f i is with lookupM i (generate f is) | inspect (lookupM i) (generate f is)
41 lemma-checkInsert-generate eq f i is | nothing     | _ = refl
42 lemma-checkInsert-generate eq f i is | just x      | Reveal_is_.[_] prf with lemma-lookupM-generate i f is x prf
43 lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl with eq (f i) (f i)
44 lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | yes refl = cong just (lemma-insert-same (generate f is) i (f i) prf)
45 lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | no  ¬p   = contradiction refl ¬p
46
47 lemma-1 : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (f : Fin n â†’ Ï„) â†’ (is : List (Fin n)) â†’ assoc eq is (map f is) â‰¡ just (generate f is)
48 lemma-1 eq f []        = refl
49 lemma-1 eq f (i âˆ· is′) = begin
50   (assoc eq (i âˆ· is′) (map f (i âˆ· is′)))
51     â‰¡âŸ¨ refl âŸ©
52   (assoc eq is′ (map f is′) >>= checkInsert eq i (f i))
53     â‰¡âŸ¨ cong (λ m â†’ m >>= checkInsert eq i (f i)) (lemma-1 eq f is′) âŸ©
54   (just (generate f is′) >>= (checkInsert eq i (f i)))
55     â‰¡âŸ¨ refl âŸ©
56   (checkInsert eq i (f i) (generate f is′))
57     â‰¡âŸ¨ lemma-checkInsert-generate eq f i is′ âŸ©
58   just (generate f (i âˆ· is′)) âˆŽ
59
60 lemma-lookupM-assoc : {A : Set} {n : â„•} â†’ (eq : EqInst A) â†’ (i : Fin n) â†’ (is : List (Fin n)) â†’ (x : A) â†’ (xs : List A) â†’ (h : FinMapMaybe n A) â†’ assoc eq (i âˆ· is) (x âˆ· xs) â‰¡ just h â†’ lookupM i h â‰¡ just x
61 lemma-lookupM-assoc eq i is x xs h    p with assoc eq is xs
62 lemma-lookupM-assoc eq i is x xs h    ()   | nothing
63 lemma-lookupM-assoc eq i is x xs h    p    | just h' with lookupM i h' | inspect (lookupM i) h'
64 lemma-lookupM-assoc eq i is x xs .(insert i x h') refl | just h' | nothing | _ = lemma-lookupM-insert i x h'
65 lemma-lookupM-assoc eq i is x xs h    p    | just h'   | just y  | _ with eq x y
66 lemma-lookupM-assoc eq i is x xs h    ()   | just h'   | just y  | _ | no ¬prf
67 lemma-lookupM-assoc eq i is x xs h    p    | just h'   | just .x | Reveal_is_.[_] p' | yes refl = begin
68   lookupM i h
69     â‰¡âŸ¨ cong (lookupM i) (lemma-from-just (sym p)) âŸ©
70   lookupM i h'
71     â‰¡âŸ¨ p' âŸ©
72   just x âˆŽ
73
74 lemma-2 : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (is : List (Fin n)) â†’ (v : List Ï„) â†’ (h : FinMapMaybe n Ï„) â†’ assoc eq is v â‰¡ just h â†’ map (flip lookupM h) is â‰¡ map just v
75 lemma-2 eq []       []       h p = refl
76 lemma-2 eq []       (x âˆ· xs) h ()
77 lemma-2 eq (x âˆ· xs) []       h ()
78 lemma-2 eq (i âˆ· is) (x âˆ· xs) h p with assoc eq is xs | inspect (assoc eq is) xs
79 lemma-2 eq (i âˆ· is) (x âˆ· xs) h () | nothing | _
80 lemma-2 eq (i âˆ· is) (x âˆ· xs) h p | just h' | Reveal_is_.[_] ir = begin
81   map (flip lookupM h) (i âˆ· is)
82     â‰¡âŸ¨ refl âŸ©
83   lookup i h âˆ· map (flip lookupM h) is
84     â‰¡âŸ¨ cong (flip _∷_ (map (flip lookup h) is)) (lemma-lookupM-assoc eq i is x xs h (begin
85       assoc eq (i âˆ· is) (x âˆ· xs)
86         â‰¡âŸ¨ cong (flip _>>=_ (checkInsert eq i x)) ir âŸ©
87       checkInsert eq i x h'
88         â‰¡âŸ¨ p âŸ©
89       just h âˆŽ) ) âŸ©
90   just x âˆ· map (flip lookupM h) is
91     â‰¡âŸ¨  cong (_∷_ (just x)) {!!} âŸ©
92   just x âˆ· map (flip lookupM h') is
93     â‰¡âŸ¨ cong (_∷_ (just x)) (lemma-2 eq is xs h' ir) âŸ©
94   just x âˆ· map just xs
95     â‰¡âŸ¨ refl âŸ©
96   map just (x âˆ· xs) âˆŽ
97
98 enumerate : {A : Set} â†’ (l : List A) â†’ List (Fin (length l))
99 enumerate l = toList (tabulate id)
100
101 denumerate : {A : Set} (l : List A) â†’ Fin (length l) â†’ A
102 denumerate l = flip lookupVec (fromList l)
103
104 bff : ({A : Set} â†’ List A â†’ List A) â†’ ({B : Set} â†’ EqInst B â†’ List B â†’ List B â†’ Maybe (List B))
105 bff get eq s v = let s′ = enumerate s
106                      g  = fromFunc (denumerate s)
107                      h  = assoc eq (get s′) v
108                      h′ = fmap (flip union g) h
109                  in fmap (flip map s′ âˆ˜ flip lookup) h′
110
111 postulate
112   free-theorem-list-list : {β Î³ : Set} â†’ (get : {α : Set} â†’ List Î± â†’ List Î±) â†’ (f : Î² â†’ Î³) â†’ (l : List Î²) â†’ get (map f l) â‰¡ map f (get l)
113
114 toList-map-commutes : {A B : Set} {n : â„•} â†’ (f : A â†’ B) â†’ (v : Data.Vec.Vec A n) â†’ (toList (Data.Vec.map f v)) â‰¡ map f (toList v)
115 toList-map-commutes f Data.Vec.[] = refl
116 toList-map-commutes f (x âˆ·V xs) = cong (_∷_ (f x)) (toList-map-commutes f xs)
117
118 lemma-map-denumerate-enumerate : {A : Set} â†’ (as : List A) â†’ map (denumerate as) (enumerate as) â‰¡ as
119 lemma-map-denumerate-enumerate [] = refl
120 lemma-map-denumerate-enumerate (a âˆ· as) = cong (_∷_ a) (begin
121   map (flip lookupVec (a âˆ·V (fromList as))) (toList (tabulate Fin.suc))
122     â‰¡âŸ¨ cong (map (flip lookupVec (a âˆ·V (fromList as))) âˆ˜ toList) (tabulate-∘ Fin.suc id) âŸ©
123   map (flip lookupVec (a âˆ·V (fromList as))) (toList (Data.Vec.map Fin.suc (tabulate id)))
124     â‰¡âŸ¨ cong (map (flip lookupVec (a âˆ·V fromList as))) (toList-map-commutes Data.Fin.suc (tabulate id)) âŸ©
125   map (flip lookupVec (a âˆ·V fromList as)) (map Fin.suc (enumerate as))
126     â‰¡âŸ¨ sym (map-∘ (enumerate as)) âŸ©
127   map (flip lookupVec (a âˆ·V (fromList as)) âˆ˜ Fin.suc) (enumerate as)
128     â‰¡âŸ¨ refl âŸ©
129   map (denumerate as) (enumerate as)
130     â‰¡âŸ¨ lemma-map-denumerate-enumerate as âŸ©
131   as âˆŽ)
132
133 theorem-1 : (get : {α : Set} â†’ List Î± â†’ List Î±) â†’ {Ï„ : Set} â†’ (eq : EqInst Ï„) â†’ (s : List Ï„) â†’ bff get eq s (get s) â‰¡ just s
134 theorem-1 get eq s = begin
135   bff get eq s (get s)
136     â‰¡âŸ¨ cong (bff get eq s âˆ˜ get) (sym (lemma-map-denumerate-enumerate s)) âŸ©
137   bff get eq s (get (map (denumerate s) (enumerate s)))
138     â‰¡âŸ¨ cong (bff get eq s) (free-theorem-list-list get (denumerate s) (enumerate s)) âŸ©
139   bff get eq s (map (denumerate s) (get (enumerate s)))
140     â‰¡âŸ¨ refl âŸ©
141   fmap (flip map (enumerate s) âˆ˜ flip lookup) (fmap (flip union (fromFunc (denumerate s))) (assoc eq (get (enumerate s)) (map (denumerate s) (get (enumerate s)))))
142     â‰¡âŸ¨ cong (fmap (flip map (enumerate s) âˆ˜ flip lookup) âˆ˜ fmap (flip union (fromFunc (denumerate s)))) (lemma-1 eq (denumerate s) (get (enumerate s))) âŸ©
143   fmap (flip map (enumerate s) âˆ˜ flip lookup) (fmap (flip union (fromFunc (flip lookupVec (fromList s)))) (just (generate (denumerate s) (get (enumerate s)))))
144     â‰¡âŸ¨ refl âŸ©
145   just ((flip map (enumerate s) âˆ˜ flip lookup) (union (generate (denumerate s) (get (enumerate s))) (fromFunc (denumerate s))))
146     â‰¡âŸ¨ cong just (cong (flip map (enumerate s) âˆ˜ flip lookup) (lemma-union-generate (denumerate s) (get (enumerate s)))) âŸ©
147   just ((flip map (enumerate s) âˆ˜ flip lookup) (fromFunc (denumerate s)))
148     â‰¡âŸ¨ refl âŸ©
149   just (map (flip lookup (fromFunc (denumerate s))) (enumerate s))
150     â‰¡âŸ¨ cong just (map-cong (lookup∘tabulate (denumerate s)) (enumerate s)) âŸ©
151   just (map (denumerate s) (enumerate s))
152     â‰¡âŸ¨ cong just (lemma-map-denumerate-enumerate s) âŸ©
153   just s âˆŽ
154
155 theorem-2 : (get : {α : Set} â†’ List Î± â†’ List Î±) â†’ {Ï„ : Set} â†’ (eq : EqInst Ï„) â†’ (v s u : List Ï„) â†’ bff get eq s v â‰¡ just u â†’ get u â‰¡ v
156 theorem-2 get eq v s u p = {!!}