Mercurial > hg > Members > kono > Proof > category

comparison list-nat0.agda @ 300:d6a6dd305da2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arrow and lambda fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:01:07 +0900
parents 3249aaddc405
children
comparison
equal deleted inserted replaced
299:8c72f5284bc8 300:d6a6dd305da2
7 postulate b : Set 7 postulate b : Set
8 postulate c : Set 8 postulate c : Set
9 9
10 10
11 infixr 40 _::_ 11 infixr 40 _::_
12 data List ∀ {a} (A : Set a) : Set a where 12 data List {a} (A : Set a) : Set a where
13 [] : List A 13 [] : List A
14 _::_ : A -> List A -> List A 14 _::_ : A → List A → List A
15 15
16 16
17 infixl 30 _++_ 17 infixl 30 _++_
18 -- _++_ : {a : Level } -> {A : Set a} -> List A -> List A -> List A 18 -- _++_ : {a : Level } → {A : Set a} → List A → List A → List A
19 _++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A 19 _++_ : ∀ {a} {A : Set a} → List A → List A → List A
20 [] ++ ys = ys 20 [] ++ ys = ys
21 (x :: xs) ++ ys = x :: (xs ++ ys) 21 (x :: xs) ++ ys = x :: (xs ++ ys)
22 22
23 23
24 l1 = a :: [] 24 l1 = a :: []
26 26
27 l3 = l1 ++ l2 27 l3 = l1 ++ l2
28 28
29 infixr 20 _==_ 29 infixr 20 _==_
30 30
31 data _==_ {n} {A : Set n} : List A -> List A -> Set n where 31 data _==_ {n} {A : Set n} : List A → List A → Set n where
32 reflection : {x : List A} -> x == x 32 reflection : {x : List A} → x == x
33 eq-cons : {x y : List A} { a : A } -> x == y -> ( a :: x ) == ( a :: y ) 33 eq-cons : {x y : List A} { a : A } → x == y → ( a :: x ) == ( a :: y )
34 trans-list : {x y z : List A} { a : A } -> x == y -> y == z -> x == z 34 trans-list : {x y z : List A} { a : A } → x == y → y == z → x == z
35 -- eq-nil : [] == [] 35 -- eq-nil : [] == []
36 36
37 list-id-l : { A : Set } -> { x : List A} -> [] ++ x == x 37 list-id-l : { A : Set } → { x : List A} → [] ++ x == x
38 list-id-l = reflection 38 list-id-l = reflection
39 39
40 list-id-r : { A : Set } -> ( x : List A ) -> x ++ [] == x 40 list-id-r : { A : Set } → ( x : List A ) → x ++ [] == x
41 list-id-r [] = reflection 41 list-id-r [] = reflection
42 list-id-r (x :: xs) = eq-cons ( list-id-r xs ) 42 list-id-r (x :: xs) = eq-cons ( list-id-r xs )
43 43
44 44
45 -- listAssoc : { A : Set } -> { a b c : List A} -> ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) ) 45 -- listAssoc : { A : Set } → { a b c : List A} → ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) )
46 -- listAssoc = eq-reflection 46 -- listAssoc = eq-reflection
47 47
48 list-assoc : {A : Set } -> ( xs ys zs : List A ) -> 48 list-assoc : {A : Set } → ( xs ys zs : List A ) →
49 ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) ) 49 ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
50 list-assoc [] ys zs = reflection 50 list-assoc [] ys zs = reflection
51 list-assoc (x :: xs) ys zs = eq-cons ( list-assoc xs ys zs ) 51 list-assoc (x :: xs) ys zs = eq-cons ( list-assoc xs ys zs )
52 52
53 53
54 54
55 open import Relation.Binary.PropositionalEquality 55 open import Relation.Binary.PropositionalEquality
56 open ≡-Reasoning 56 open ≡-Reasoning
57 57
58 cong1 : ∀{a} {A : Set a } {b} { B : Set b } -> 58 cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
59 ( f : A -> B ) -> {x : A } -> {y : A} -> x ≡ y -> f x ≡ f y 59 ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y
60 cong1 f refl = refl 60 cong1 f refl = refl
61 61
62 lemma11 : ∀{n} -> ( Set n ) IsRelatedTo ( Set n ) 62 lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n )
63 lemma11 = relTo refl 63 lemma11 = relTo refl
64 64
65 lemma12 : {L : Set} ( x : List L ) -> x ++ x ≡ x ++ x 65 lemma12 : {L : Set} ( x : List L ) → x ++ x ≡ x ++ x
66 lemma12 x = begin x ++ x ∎ 66 lemma12 x = begin x ++ x ∎
67 67
68 68
69 ++-assoc : {L : Set} ( xs ys zs : List L ) -> (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) 69 ++-assoc : {L : Set} ( xs ys zs : List L ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
70 ++-assoc [] ys zs = -- {A : Set} -> -- let open ==-Reasoning A in 70 ++-assoc [] ys zs = -- {A : Set} → -- let open ==-Reasoning A in
71 begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs) 71 begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)
72 ( [] ++ ys ) ++ zs 72 ( [] ++ ys ) ++ zs
73 ≡⟨ refl ⟩ 73 ≡⟨ refl ⟩
74 ys ++ zs 74 ys ++ zs
75 ≡⟨ refl ⟩ 75 ≡⟨ refl ⟩
76 [] ++ ( ys ++ zs ) 76 [] ++ ( ys ++ zs )
77 ∎ 77 ∎
78 78
79 ++-assoc (x :: xs) ys zs = -- {A : Set} -> -- let open ==-Reasoning A in 79 ++-assoc (x :: xs) ys zs = -- {A : Set} → -- let open ==-Reasoning A in
80 begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs) 80 begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
81 ((x :: xs) ++ ys) ++ zs 81 ((x :: xs) ++ ys) ++ zs
82 ≡⟨ refl ⟩ 82 ≡⟨ refl ⟩
83 (x :: (xs ++ ys)) ++ zs 83 (x :: (xs ++ ys)) ++ zs
84 ≡⟨ refl ⟩ 84 ≡⟨ refl ⟩
98 -- false : Bool 98 -- false : Bool
99 99
100 100
101 --postulate Obj : Set 101 --postulate Obj : Set
102 102
103 --postulate Hom : Obj -> Obj -> Set 103 --postulate Hom : Obj → Obj → Set
104 104
105 105
106 --postulate id : { a : Obj } -> Hom a a 106 --postulate id : { a : Obj } → Hom a a
107 107
108 108
109 --infixr 80 _○_ 109 --infixr 80 _○_
110 --postulate _○_ : { a b c : Obj } -> Hom b c -> Hom a b -> Hom a c 110 --postulate _○_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c
111 111
112 -- postulate axId1 : {a b : Obj} -> ( f : Hom a b ) -> f == id ○ f 112 -- postulate axId1 : {a b : Obj} → ( f : Hom a b ) → f == id ○ f
113 -- postulate axId2 : {a b : Obj} -> ( f : Hom a b ) -> f == f ○ id 113 -- postulate axId2 : {a b : Obj} → ( f : Hom a b ) → f == f ○ id
114 114
115 --assoc : { a b c d : Obj } -> 115 --assoc : { a b c d : Obj } →
116 -- (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) -> 116 -- (f : Hom c d ) → (g : Hom b c) → (h : Hom a b) →
117 -- (f ○ g) ○ h == f ○ ( g ○ h) 117 -- (f ○ g) ○ h == f ○ ( g ○ h)
118 118
119 119
120 --a = Set 120 --a = Set
121 121
122 -- ListObj : {A : Set} -> List A 122 -- ListObj : {A : Set} → List A
123 -- ListObj = List Set 123 -- ListObj = List Set
124 124
125 -- ListHom : ListObj -> ListObj -> Set 125 -- ListHom : ListObj → ListObj → Set
126 126