Mercurial > hg > Members > kono > Proof > category

comparison list-nat.agda @ 130:5f331dfc000b

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