annotate system-f.agda @ 332:fa179abb6161

factoral done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Mar 2014 13:55:26 +0700
parents f385a5821563
children 26f44a4fa494
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
4 module system-f where
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
6 Bool : {l : Level} (X : Set l) -> Set l
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
7 Bool = \{l : Level} -> \(X : Set l) -> X -> X -> X
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
9 T : {l : Level} (X : Set l) -> Bool X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
10 T X = \(x y : X) -> x
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
12 F : {l : Level} (X : Set l) -> Bool X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
13 F X = \(x y : X) -> y
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
15 D : {l : Level} -> {U : Set l} -> U -> U -> Bool U -> U
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
16 D u v t = t u v
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
18 lemma04 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (T U ) ≡ u
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 lemma04 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
21 lemma05 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (F U ) ≡ v
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 lemma05 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
24 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
25 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
27 <_,_> : {l : Level} {U V : Set l} -> U -> V -> (U × V)
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
28 <_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
30 π1 : {l : Level} {U V : Set l} -> (U × V) -> U
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
31 π1 {l} {U} {V} t = t {U} (\(x : U) -> \(y : V) -> x)
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
33 π2 : {l : Level} {U V : Set l} -> (U × V) -> V
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
34 π2 {l} {U} {V} t = t {V} (\(x : U) -> \(y : V) -> y)
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
36 lemma06 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡ u
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 lemma06 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
39 lemma07 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡ v
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 lemma07 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
42 hoge : {l : Level} {U V : Set l} -> U -> V -> (U × V)
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 hoge u v = < u , v >
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 -- lemma08 : (t : U × V) -> < π1 t , π2 t > ≡ t
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 -- lemma08 t = {!!}
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
47
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
48 -- Emp definision is still wrong...
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
49
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
50 Emp : {l : Level} {X : Set l} -> Set l
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
51 Emp {l} = \{X : Set l} -> X
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
52
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
53 -- ε : {l : Level} (U : Set l) {l' : Level} {U' : Set l'} -> Emp -> Emp
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
54 -- ε {l} U t = t
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
55
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
56 -- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} -> (t : Emp {l} {U} ) -> ε U (ε Emp t) ≡ ε U t
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
57 -- lemma09 t = refl
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
58
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
59 -- lemma10 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> U × V
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
60 -- lemma10 {l} {U} {V} t = ε (U × V) t
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
61
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
62 -- lemma10' : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> Emp
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
63 -- lemma10' {l} {U} {V} {X} t = ε (U × V) t
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
64
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
65 -- lemma100 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U}) -> Emp
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
66 -- lemma100 {l} {U} {V} t = ε U t
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
67
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
68 -- lemma101 : {l k : Level} {U V : Set l} -> (t : Emp {_} {U × V}) -> π1 (ε (U × V) t) ≡ ε U t
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
69 -- lemma101 t = refl
319
5791b7b04820 Emp in System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
70
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
71 -- lemma102 : {l k : Level} {U V : Set l} -> (t : Emp {_} {U × V}) -> π2 (ε (U × V) t) ≡ ε V t
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
72 -- lemma102 t = refl
321
33c6dd3598ca Emp with yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
73
327
7645185970f2 fix Emp commnet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 326
diff changeset
74 -- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
75 -- lemma103 u t = refl
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
76
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
77 _+_ : {l : Level} -> Set l -> Set l -> Set (suc l)
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
78 _+_ {l} U V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
79
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
80 ι1 : {l : Level } {U V : Set l} -> U -> U + V
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
81 ι1 {l} {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
82
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
83 ι2 : {l : Level } {U V : Set l} -> V -> U + V
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
84 ι2 {l} {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
85
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
86 δ : {l : Level} { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
87 δ {l} {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
88
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
89 lemma11 : {l : Level} { U V R S : Set _ } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ {l} {U} {V} {R} {S} u v ( ι1 r ) ≡ u r
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
90 lemma11 u v r = refl
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
91
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
92 lemma12 : {l : Level} { U V R S : Set _ } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ {l} {U} {V} {R} {S} u v ( ι2 s ) ≡ v s
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
93 lemma12 u v s = refl
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
94
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
95
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
96 _××_ : {l : Level} -> Set (suc l) -> Set l -> Set (suc l)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
97 _××_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
98
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
99 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} -> U -> V -> (U ×× V)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
100 <<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
101
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
102
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
103 Int : {l : Level } ( X : Set l ) -> Set l
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
104 Int {l} X = X -> ( X -> X ) -> X
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
105
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
106 Zero : {l : Level } -> { X : Set l } -> Int X
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
107 Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
108
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
109 S : {l : Level } -> { X : Set l } -> Int X -> Int X
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
110 S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
111
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
112 n0 : {l : Level} {X : Set l} -> Int X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
113 n0 = Zero
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 325
diff changeset
114
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
115 n1 : {l : Level } -> { X : Set l } -> Int X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
116 n1 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y x
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
117
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
118 n2 : {l : Level } -> { X : Set l } -> Int X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
119 n2 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
120
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
121 n3 : {l : Level } -> { X : Set l } -> Int X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
122 n3 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
123
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
124 lemma13 : {l : Level } -> { X : Set l } -> S (S (Zero {_} {X})) ≡ n2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
125 lemma13 = refl
322
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
126
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
127 It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int U -> U
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
128 It u f t = t u f
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
129
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
130 R : {l : Level} { U X : Set l} -> U -> ( U -> Int X -> U ) -> Int _ -> U
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
131 R {l} {U} {X} u v t = π1 ( It {suc l} {U × Int X} (< u , Zero >) (λ (x : U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t )
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
132
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
133 add : {l : Level} {X : Set l} -> Int (Int X) -> Int X -> Int X
332
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
134 add x y = It y S x
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
135
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
136 mul : {l : Level } {X : Set l} -> Int (Int X) -> Int (Int X) -> Int X
332
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
137 mul {l} {X} x y = It Zero (add x) y
324
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
138
332
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
139 fact : {l : Level} {X : Set l} -> Int _ -> Int (Int X)
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
140 fact {l} {X} n = R (S Zero) (λ (z : Int (Int X)) -> λ w -> mul w (S w) ) n
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 325
diff changeset
141
332
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
142 lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n3 ≡ mul n1 ( mul n2 n3)
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
143 lemma13' = refl
324
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
144
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
145 -- lemma14 : (x y : Int) -> mul x y ≡ mul y x
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 325
diff changeset
146 -- lemma14 x y = It {!!} {!!} {!!}
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
147
332
fa179abb6161 factoral done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
148 lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul n2 n3 ≡ mul {l} {X} n3 n2
324
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
149 lemma15 x y = refl
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
150
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
151 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X -> U ) -> R u v Zero ≡ u
324
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
152 lemma16 u v = refl
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
153
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
154 -- lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int -> U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
155 -- lemma17 u v t = refl
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
156
6e9bca4e67a3 R lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 323
diff changeset
157 -- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int -> U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t
316
7a3229b32b3c Emp and Sum first try
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
158
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
159 List : {l : Level} (U X : Set l) -> Set l
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
160 List {l} = \( U X : Set l) -> X -> ( U -> X -> X ) -> X
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
161
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
162 Nil : {l : Level} {U : Set l} {X : Set l} -> List U X
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
163 Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
164
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
165 Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List U X -> List U X
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
166 Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
167
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
168 l0 : {l : Level} {X X' : Set l} -> List (Int X) (X')
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
169 l0 = Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
170
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
171 l1 : {l : Level} {X X' : Set l} -> List (Int X) (X')
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
172 l1 = Cons n1 Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
173
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
174 l2 : {l : Level} {X X' : Set l} -> List (Int X) (X')
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
175 l2 = Cons n2 l1
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
176
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
177 l3 : {l : Level} {X X' : Set l} -> List (Int X) (X')
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
178 l3 = Cons n3 l2
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
179
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
180 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List U W -> W
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
181 ListIt w f t = t w f
323
d22a39e155c4 fact error on R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 322
diff changeset
182
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
183 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List U (Bool X) -> Bool _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
184 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) list
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
185
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
186 Append : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X -> List U _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
187 Append x y = \s t -> x (y s t) t
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
188
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
189 lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
328
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 327
diff changeset
190 lemma18 = refl
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 325
diff changeset
191
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
192 Reverse : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
193 Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( \u w -> Append w (Cons u Nil) ) x
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
194
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
195 lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
330
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
196 lemma19 = refl
fa018eb1723e remove module level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
197
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
198 Tree : {l : Level} -> Set l -> Set l -> Set l
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
199 Tree {l} = \( U X : Set l) -> X -> ( (U -> X) -> X ) -> X
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
200
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
201 NilTree : {l : Level} (U : Set l) (X : Set l) -> Tree U X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
202 NilTree U X = \(x : X) -> \(y : (U -> X) -> X) -> x
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
203
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
204 Collect : {l : Level} (U : Set l) (X : Set l) -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree U X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
205 Collect U X f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y )
325
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
206
331
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
207 TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree U W -> W
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
208 TreeIt w h t = t w h