started proving theorem-1
[~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 () 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-∘)
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     ≡⟨ {!!} ⟩
141   just s ∎