Mercurial > hg > Members > kono > Proof > category

comparison list-level.agda @ 153:3249aaddc405

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sync
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Aug 2013 21:09:34 +0900
parents
children d6a6dd305da2
comparison
equal deleted inserted replaced
152:5435469c6cf0 153:3249aaddc405
1 module list-level where
2
3 open import Level
4
5
6 postulate A : Set
7 postulate B : Set
8 postulate C : Set
9
10 postulate a : A
11 postulate b : A
12 postulate c : A
13
14
15 infixr 40 _::_
16 data List {a} (A : Set a) : Set a where
17 [] : List A
18 _::_ : A -> List A -> List A
19
20
21 infixl 30 _++_
22 _++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
23 [] ++ ys = ys
24 (x :: xs) ++ ys = x :: (xs ++ ys)
25
26 l1 = a :: []
27 l2 = a :: b :: a :: c :: []
28
29 l3 = l1 ++ l2
30
31 L1 = A :: []
32 L2 = A :: B :: A :: C :: []
33
34 L3 = L1 ++ L2
35
36 data Node {a} ( A : Set a ) : Set a where
37 leaf : A -> Node A
38 node : Node A -> Node A -> Node A
39
40 flatten : ∀{n} { A : Set n } -> Node A -> List A
41 flatten ( leaf a ) = a :: []
42 flatten ( node a b ) = flatten a ++ flatten b
43
44 n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c ))
45
46 open import Relation.Binary.PropositionalEquality
47
48 infixr 20 _==_
49
50 data _==_ {n} {A : Set n} : List A -> List A -> Set n where
51 reflection : {x : List A} -> x == x
52
53 cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
54 ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
55 cong1 f reflection = reflection
56
57 eq-cons : ∀{n} {A : Set n} {x y : List A} ( a : A ) -> x == y -> ( a :: x ) == ( a :: y )
58 eq-cons a z = cong1 ( \x -> ( a :: x) ) z
59
60 trans-list : ∀{n} {A : Set n} {x y z : List A} -> x == y -> y == z -> x == z
61 trans-list reflection reflection = reflection
62
63
64 ==-to-≡ : ∀{n} {A : Set n} {x y : List A} -> x == y -> x ≡ y
65 ==-to-≡ reflection = refl
66
67 list-id-l : { A : Set } -> { x : List A} -> [] ++ x == x
68 list-id-l = reflection
69
70 list-id-r : { A : Set } -> ( x : List A ) -> x ++ [] == x
71 list-id-r [] = reflection
72 list-id-r (x :: xs) = eq-cons x ( list-id-r xs )
73
74 list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
75 ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
76 list-assoc [] ys zs = reflection
77 list-assoc (x :: xs) ys zs = eq-cons x ( list-assoc xs ys zs )
78
79
80 module ==-Reasoning {n} (A : Set n ) where
81
82 infixr 2 _∎
83 infixr 2 _==⟨_⟩_ _==⟨⟩_
84 infix 1 begin_
85
86
87 data _IsRelatedTo_ (x y : List A) :
88 Set n where
89 relTo : (x≈y : x == y ) → x IsRelatedTo y
90
91 begin_ : {x : List A } {y : List A} →
92 x IsRelatedTo y → x == y
93 begin relTo x≈y = x≈y
94
95 _==⟨_⟩_ : (x : List A ) {y z : List A} →
96 x == y → y IsRelatedTo z → x IsRelatedTo z
97 _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
98
99 _==⟨⟩_ : (x : List A ) {y : List A}
100 → x IsRelatedTo y → x IsRelatedTo y
101 _ ==⟨⟩ x≈y = x≈y
102
103 _∎ : (x : List A ) → x IsRelatedTo x
104 _∎ _ = relTo reflection
105
106 lemma11 : ∀{n} (A : Set n) ( x : List A ) -> x == x
107 lemma11 A x = let open ==-Reasoning A in
108 begin x ∎
109
110 ++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
111 ++-assoc A [] ys zs = let open ==-Reasoning A in
112 begin -- to prove ([] ++ ys) ++ zs == [] ++ (ys ++ zs)
113 ( [] ++ ys ) ++ zs
114 ==⟨ reflection ⟩
115 ys ++ zs
116 ==⟨ reflection ⟩
117 [] ++ ( ys ++ zs )
118 ∎
119
120 ++-assoc A (x :: xs) ys zs = let open ==-Reasoning A in
121 begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
122 ((x :: xs) ++ ys) ++ zs
123 ==⟨ reflection ⟩
124 (x :: (xs ++ ys)) ++ zs
125 ==⟨ reflection ⟩
126 x :: ((xs ++ ys) ++ zs)
127 ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
128 x :: (xs ++ (ys ++ zs))
129 ==⟨ reflection ⟩
130 (x :: xs) ++ (ys ++ zs)
131 ∎
132
133
134
135 --data Bool : Set where
136 -- true : Bool
137 -- false : Bool
138
139
140 --postulate Obj : Set
141
142 --postulate Hom : Obj -> Obj -> Set
143
144
145 --postulate id : { a : Obj } -> Hom a a
146
147
148 --infixr 80 _○_
149 --postulate _○_ : { a b c : Obj } -> Hom b c -> Hom a b -> Hom a c
150
151 -- postulate axId1 : {a b : Obj} -> ( f : Hom a b ) -> f == id ○ f
152 -- postulate axId2 : {a b : Obj} -> ( f : Hom a b ) -> f == f ○ id
153
154 --assoc : { a b c d : Obj } ->
155 -- (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
156 -- (f ○ g) ○ h == f ○ ( g ○ h)
157
158
159 --a = Set
160
161 -- ListObj : {A : Set} -> List A
162 -- ListObj = List Set
163
164 -- ListHom : ListObj -> ListObj -> Set
165