Mercurial > hg > Members > atton > agda-proofs

comparison cbc/maybe-subtype.agda @ 57:75f9f71f364a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define maybe-subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2017 01:04:59 +0000
parents
children 352e8a724829
comparison
equal deleted inserted replaced
56:ddcd652969e0 57:75f9f71f364a
1 module maybe-subtype (A : Set) where
2
3 open import Level
4 open import Function using (id)
5 open import Relation.Binary.PropositionalEquality
6
7 data Maybe (A : Set) : Set where
8 nothing : Maybe A
9 just : A -> Maybe A
10
11
12 record Context (A : Set) : Set where
13 field
14 maybeElem : Maybe A
15
16 open import subtype (Context A) as N
17
18
19 record Meta (A : Set) : Set where
20 field
21 context : Context A
22
23
24 open import subtype (Meta A) as M
25
26 instance
27 MetaIsMetaDataSegment : M.DataSegment (Meta A)
28 MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
29 ContextIsMetaDataSegment : M.DataSegment (Context A)
30 ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
31
32 return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A
33 return {c} {mc} {{nd}} {{md}} a = record {context = record {maybeElem = just a}}
34
35 fmap' : {B : Set} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}} -> (A -> B) -> Context A -> Context B
36 fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)}
37 fmap' f record { maybeElem = nothing } = record {maybeElem = nothing}
38
39
40
41 fmap : {c : Context A} {B : Set}
42 {{_ : N.DataSegment A}} {{_ : N.DataSegment B}} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}}
43 -> N.CodeSegment A B -> M.CodeSegment (Context A) (Context B)
44 fmap {c} {B} {{na}} {{nb}} {{ma}} {{mb}} (N.cs f) = M.cs {{ma}} (fmap' {B} {{ma}} {{mb}} f)
45
46
47
48 open ≡-Reasoning
49
50 exec-id : (x : Meta A) -> M.exec (M.cs {zero} {zero} {Context A} id) x ≡ x
51 exec-id record { context = context } = refl
52
53
54 maybe-preserve-id : {{na : N.DataSegment A}} {{ma : M.DataSegment A}} {{mx : M.DataSegment (Context A)}}
55 -> (x : Context A)
56 -> M.exec {{mx}} {{mx}} (fmap {x} {{na}}{{na}}{{mx}}{{mx}} (N.cs id)) (record {context = x})
57 ≡
58 M.exec {{mx}} {{mx}} (M.cs {{mx}} {{mx}} id) (record {context = x})
59
60 maybe-preserve-id {{na}} {{ma}} {{mx}} record { maybeElem = nothing } = begin
61 M.exec {{mx}} {{mx}} (fmap {record { maybeElem = nothing }} {{na}}{{na}}{{mx}}{{mx}} (N.cs id)) (record {context = record { maybeElem = nothing }})
62 ≡⟨ refl ⟩
63 M.DataSegment.set mx (record { context = record { maybeElem = nothing } }) ((fmap' {{mx}} {{mx}} id) (M.DataSegment.get mx (record { context = record { maybeElem = nothing } })))
64 ≡⟨ {!!} ⟩
65 record {context = record { maybeElem = nothing }}
66 ≡⟨ sym (exec-id (record {context = record {maybeElem = nothing}})) ⟩
67 M.exec {{mx}} {{mx}} (M.cs {{mx}} {{mx}} id) (record {context = record { maybeElem = nothing }})
68 ∎
69 maybe-preserve-id record { maybeElem = (just x) } = {!!}
70 {-
71 maybe-preserve-id {{na}} {{ma}} {{mx}} record { maybeElem = nothing } = begin
72 M.exec (fmap {record {maybeElem = nothing}} (N.cs id)) record {context = record { maybeElem = nothing}}
73 ≡⟨ refl ⟩
74 M.exec (M.cs (fmap' id)) record {context = record {maybeElem = nothing}}
75 ≡⟨ refl ⟩
76 M.DataSegment.set mx (record { context = record { maybeElem = nothing } }) ((fmap' id) (M.DataSegment.get mx (record { context = record { maybeElem = nothing } })))
77 ≡⟨ {!!} ⟩
78 record { context = record { maybeElem = nothing }}
79 ≡⟨ {!!} ⟩
80 M.exec {zero} {zero} {A} {A} (M.cs id) (record { context = record { maybeElem = nothing } })
81 ∎
82 maybe-preserve-id record { maybeElem = (just x) } = {!!}
83
84
85 -}