|
315
|
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
|
|
324
|
144 -- lemma14 : (x y : Int) -> sum x y ≡ sum y x
|
|
|
145 -- lemma14 zero zero = refl
|
|
|
146 -- lemma14 zero (S t) = cong (\x -> S x )( lemma14 zero t)
|
|
|
147 -- lemma14 (S t) t' = cong (\x -> {!!} ) (lemma14 t t')
|
|
315
|
148
|
|
|
149
|
|
|
150
|
