Mercurial > hg > Members > kono > Proof > category

comparison system-t.agda @ 315:0d7fa6fc5979

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
System T and System F
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Mar 2014 10:15:54 +0900
parents
children 6e9bca4e67a3
comparison
equal deleted inserted replaced
314:d1af69c4aaf8 315:0d7fa6fc5979
1 module system-t where
2 open import Relation.Binary.PropositionalEquality
3
4 record _×_ ( U : Set ) ( V : Set ) : Set where
5 field
6 π1 : U
7 π2 : V
8
9 <_,_> : {U V : Set} -> U -> V -> U × V
10 < u , v > = record {π1 = u ; π2 = v }
11
12 open _×_
13
14 postulate U : Set
15 postulate V : Set
16
17 postulate v : V
18 postulate u : U
19
20 f : U -> V
21 f = \u -> v
22
23
24 UV : Set
25 UV = U × V
26
27 uv : U × V
28 uv = < u , v >
29
30 lemma01 : π1 < u , v > ≡ u
31 lemma01 = refl
32
33 lemma02 : π2 < u , v > ≡ v
34 lemma02 = refl
35
36 lemma03 : (uv : U × V ) → < π1 uv , π2 uv > ≡ uv
37 lemma03 uv = refl
38
39 lemma04 : (λ x → f x ) u ≡ f u
40 lemma04 = refl
41
42 lemma05 : (λ x → f x ) ≡ f
43 lemma05 = refl
44
45 nn = λ (x : U ) → u
46 n1 = λ ( x : U ) → f x
47
48 data Bool : Set where
49 T : Bool
50 F : Bool
51
52 D : { U : Set } -> U -> U -> Bool -> U
53 D u v T = u
54 D u v F = v
55
56 data Int : Set where
57 zero : Int
58 S : Int → Int
59
60 pred : Int -> Int
61 pred zero = zero
62 pred (S t) = t
63
64 R : { U : Set } -> U -> ( U -> Int -> U ) -> Int -> U
65 R u v zero = u
66 R u v ( S t ) = v (R u v t) t
67
68 null : Int -> Bool
69 null zero = T
70 null (S _) = F
71
72 It : { T : Set } -> T -> (T -> T) -> Int -> T
73 It u v zero = u
74 It u v ( S t ) = v (It u v t )
75
76 R' : { T : Set } -> T -> ( T -> Int -> T ) -> Int -> T
77 R' u v t = π1 ( It ( < u , zero > ) (λ x → < v (π1 x) (π2 x) , S (π2 x) > ) t )
78
79 sum : Int -> Int -> Int
80 sum x y = R y ( λ z -> λ w -> S z ) x
81
82 mul : Int -> Int -> Int
83 mul x y = R zero ( λ z -> λ w -> sum y z ) x
84
85 sum' : Int -> Int -> Int
86 sum' x y = R' y ( λ z -> λ w -> S z ) x
87
88 mul' : Int -> Int -> Int
89 mul' x y = R' zero ( λ z -> λ w -> sum y z ) x
90
91 fact : Int -> Int
92 fact n = R (S zero) (λ z -> λ w -> mul (S w) z ) n
93
94 fact' : Int -> Int
95 fact' n = R' (S zero) (λ z -> λ w -> mul (S w) z ) n
96
97 f3 = fact (S (S (S zero)))
98 f3' = fact' (S (S (S zero)))
99
100 lemma21 : f3 ≡ f3'
101 lemma21 = refl
102
103 lemma07 : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t : Int ) ->
104 (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t )) ≡ t
105 lemma07 u v zero = refl
106 lemma07 u v (S t) = cong ( \x -> S x ) ( lemma07 u v t )
107
108 lemma06 : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t : Int ) -> ( (R u v t) ≡ (R' u v t ))
109 lemma06 u v zero = refl
110 lemma06 u v (S t) = trans ( cong ( \x -> v x t ) ( lemma06 u v t ) )
111 ( cong ( \y -> v (R' u v t) y ) (sym ( lemma07 u v t ) ) )
112
113 lemma08 : ( n m : Int ) -> ( sum' n m ≡ sum n m )
114 lemma08 zero _ = refl
115 lemma08 (S t) y = cong ( \x -> S x ) ( lemma08 t y )
116
117 lemma09 : ( n m : Int ) -> ( mul' n m ≡ mul n m )
118 lemma09 zero _ = refl
119 lemma09 (S t) y = cong ( \x -> sum y x) ( lemma09 t y )
120
121 lemma10 : ( n : Int ) -> ( fact n ≡ fact n )
122 lemma10 zero = refl
123 lemma10 (S t) = cong ( \x -> mul (S t) x ) ( lemma10 t )
124
125 lemma11 : ( n : Int ) -> ( fact n ≡ fact' n )
126 lemma11 n = lemma06 (S zero) (λ z -> λ w -> mul (S w) z ) n
127
128 lemma06' : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t : Int ) -> ( (R u v t) ≡ (R' u v t ))
129 lemma06' u v zero = refl
130 lemma06' u v (S t) = let open ≡-Reasoning in
131 begin
132 R u v (S t)
133 ≡⟨⟩
134 v (R u v t) t
135 ≡⟨ cong (\x -> v x t ) ( lemma06' u v t ) ⟩
136 v (R' u v t) t
137 ≡⟨ cong (\x -> v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩
138 v (R' u v t) (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t))
139 ≡⟨⟩
140 R' u v (S t)
141 ∎
142
143
144
145
146