Mercurial > hg > Members > atton > agda > systemF

annotate systemF.agda @ 20:de9e05b25acf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define List
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 10 Apr 2014 14:29:37 +0900
parents 9eb6fcf6fc7d
children 25b62c46081b
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
4 module systemF where
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 T : Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 T = \{X : Set} -> \(x : X) -> \y -> x
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 F : Bool
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 F = \{X : Set} -> \x -> \(y : X) -> y
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 D : {X : Set} -> (U V : X) -> Bool -> X
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 D {X} u v bool = bool {X} u v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 lemma-bool-t = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 lemma-bool-f = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 -- Product
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
27 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
28 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
30 <_,_> : {l : Level} -> {U : Set l} -> {V : Set l} -> U -> V -> (U × V)
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
31 <_,_> {l} {U} {V} u v = \{X : Set l} -> \(x : U -> V -> X) -> x u v
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
33 π1 : {l : Level} -> {U : Set l} -> {V : Set l} -> (U × V) -> U
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
34 π1 {l} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
36 π2 : {l : Level} -> {U : Set l} -> {V : Set l} -> (U × V) -> V
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
37 π2 {l} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
15
8c735b9ebf5a Add lemma for Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
39 lemma-product : {l : Level} {U V : Set l} -> U -> V -> U × V
8c735b9ebf5a Add lemma for Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
40 lemma-product u v = < u , v >
8c735b9ebf5a Add lemma for Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
41
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
42 lemma-product-pi1 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
0
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 lemma-product-pi1 = refl
b7c49383e386 Bool and Product in System F
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
45 lemma-product-pi2 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
2
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
46 lemma-product-pi2 = refl
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
47
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
48 -- Empty
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
49
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
50
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
51 -- Sum
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
52
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
53 _+_ : {l : Level} -> Set l -> Set l -> Set (suc l)
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
54 _+_ {l} U V = {X : Set l} -> (U -> X) -> (V -> X) -> X
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
55
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
56 ι1 : {l : Level} {U V : Set l} -> U -> (U + V)
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
57 ι1 {l} {U} {V} u = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u
2
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
58
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
59 ι2 : {l : Level} {U V : Set l} -> V -> (U + V)
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
60 ι2 {l} {U} {V} v = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v
2
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
61
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
62 δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
63 δ {l} {U} {V} {X} u v t = t {X} u v
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
64
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
65 lemma-sum-iota1 : {l : Level} {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u
2
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
66 lemma-sum-iota1 = refl
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
67
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
68 lemma-sum-iota2 : {l : Level} {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
2
bbf889402b64 wrote Sum Type
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
69 lemma-sum-iota2 = refl
3
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
70
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
71
3
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
72 -- Existential
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
73
5
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
74 data V {l} (X : Set l) : Set l
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
75 where
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
76 v : X -> V X
3
26cf9069f70a Wrote Sigma in Existional
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
77
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
78 Σ_,_ : {l : Level} (X : Set l) -> V X -> Set (suc l)
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
79 Σ_,_ {l} U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y
5
63e982ff38a5 Rewrite Existential by data constructor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
80
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
81 ⟨_,_⟩ : {l : Level} (U : Set l) -> (u : V U) -> Σ U , u
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
82 ⟨_,_⟩ {l} U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
83
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
84 ∇_,_,_ : {l : Level} {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u -> W
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
85 ∇_,_,_ {l} {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
86
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
87 {-
7
aac0c4fc941c Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
88 lemma-nabla on proofs and types
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
89 (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
7
aac0c4fc941c Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
90 w[U/X][u/x^[U/X]]
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
91 -}
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
92
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
93 lemma-nabla : {l : Level} {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {l} {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
6
e6a39088cb0a Wrote lemmna-nabla
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
94 lemma-nabla = refl
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
95
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
96
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
97 -- Int
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
98
13
4977c5873660 Add lemma-it of Int, but has yellow
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
99 Int : {l : Level} -> {X : Set l} -> Set l
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
100 Int {l} {X} = X -> (X -> X) -> X
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
101
13
4977c5873660 Add lemma-it of Int, but has yellow
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
102 O : {l : Level} -> {X : Set l} -> Int
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
103 O {l} {X} = \(x : X) -> \(y : X -> X) -> x
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
104
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
105 S : {l : Level} -> {X : Set l} -> Int -> Int
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
106 S {l} {X} t = \(x : X) -> \(y : X -> X) -> y (t x y)
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
107
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
108 It : {l : Level} {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
109 It {l} {U} u f t = t u f
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
110
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
111 lemma-it-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
8
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
112 lemma-it-o = refl
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
113
14
491a08669724 Delete definition global Level
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
114 lemma-it-s-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
9
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
115 lemma-it-s-o = refl
64182a3d9a49 Trying g of Int. but not completed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
116
12
627da4867e5b Delete multiple levels on Product
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
117 g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int)
13
4977c5873660 Add lemma-it of Int, but has yellow
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
118 g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
4977c5873660 Add lemma-it of Int, but has yellow
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
119
16
93705fd8f577 Add comment to g
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
120 -- cannot prove general Int
93705fd8f577 Add comment to g
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
121 -- lemma-it-n : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n >
93705fd8f577 Add comment to g
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
122 -- lemma-it-n = refl
17
cc34bf8772a9 Define R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
123
18
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
124 R : {l : Level} -> {U : Set l} -> U -> (U -> Int -> U) -> Int -> U
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
125 R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {_} {_} {f}) t)
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
126
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
127 lemma-R-O : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} -> R u f O ≡ u
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
128 lemma-R-O = refl
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
129
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
130 lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) (n < u , O > (g {l} {U} {f}) (\u n -> π2 < u , n > ))
08b8ced4e90e lemma-R
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
131 lemma-R-n = refl
19
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
132
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
133 -- Proofs And Types Style lemma-R-n
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
134 -- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
135 -- n in (S n) and (R u f n) has (U × Int), but last n has Int.
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
136 -- regenerate same (n : Int) by used g, <_,_>
20
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
137 -- NOTE : Proofs And Types say "equation for recursion is satisfied by values only"
19
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
138
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
139
20
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
140 -- List
19
9eb6fcf6fc7d Add comments
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
141
20
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
142 List : {l : Level} -> (U : Set l) -> Set (suc l)
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
143 List {l} U = {X : Set l} -> X -> (U -> X -> X) -> X
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
144
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
145 nil : {l : Level} {U : Set l} -> List U
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
146 nil {l} {U} = \{X : Set l} -> \(x : X) -> \(y : U -> X -> X) -> x
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
147
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
148 cons : {l : Level} {U : Set l} -> U -> List U -> List U
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
149 cons {l} {U} u t = \{X : Set l} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
150
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
151 ListIt : {l : Level} {U W : Set l} -> W -> (U -> W -> W) -> List U -> W
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
152 ListIt {l} {U} {W} w f t = t {W} w f
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
153
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
154 lemma-list-it-nil : {l : Level} {U W : Set l} {w : W} {f : U -> W -> W} -> ListIt w f nil ≡ w
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
155 lemma-list-it-nil = refl
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
156
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
157 lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
de9e05b25acf Define List
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
158 lemma-list-it-cons = refl