Mercurial > hg > Members > atton > agda-proofs

annotate systemF/systemF.agda @ 6:90abb3f53c03

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add functor example
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 15 Jan 2015 17:27:25 +0900
parents 4c1a6ce23f9e
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
2
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module systemF where
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Bool
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 T : Bool
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 T = \{X : Set} -> \(x : X) -> \y -> x
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 F : Bool
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 F = \{X : Set} -> \x -> \(y : X) -> y
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 not : Bool -> Bool
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 not b = \{X : Set} -> \(x : X) -> \(y : X) -> b y x
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 D : {X : Set} -> (U V : X) -> Bool -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 D {X} u v bool = bool {X} u v
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 lemma-bool-t = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 lemma-bool-f = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 lemma-bool-not-D : {X : Set} {u v : X} {b : Bool} -> D u v b ≡ D v u (not b)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 lemma-bool-not-D = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 -- Product
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 _×_ : ∀ {l ll} -> Set l -> Set ll -> {lll : Level} -> Set (suc lll ⊔ (ll ⊔ l))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 _×_ {l} {ll} U V {lll} = {X : Set lll} -> (U -> V -> X) -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 <_,_> : ∀{l ll lll} -> {U : Set l} -> {V : Set ll} -> U -> V -> (U × V)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 <_,_> {l} {ll} {lll} {U} {V} u v = \{X : Set lll} -> \(x : U -> V -> X) -> x u v
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 π1 : ∀{l ll} -> {U : Set l} -> {V : Set ll} -> (U × V) -> U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 π1 {l} {ll} {U} {V} t = t {U} \(x : U) -> \(y : V) -> x
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 π2 : ∀{l ll} -> {U : Set l} -> {V : Set ll} -> (U × V) -> V
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 π2 {l} {ll} {U} {V} t = t {V} \(x : U) -> \(y : V) -> y
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 lemma-product : {l ll : Level} {U V : Set l} -> U -> V -> (U × V) {ll}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 lemma-product u v = < u , v >
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 lemma-product-pi1 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π1 (< u , v >) ≡ u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 lemma-product-pi1 = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 lemma-product-pi2 : {l : Level} {U V : Set l} -> {u : U} -> {v : V} -> π2 (< u , v >) ≡ v
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 lemma-product-pi2 = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 lemma-product-rebuild : {l : Level} {U V X : Set l} {u : U} {v : V} -> < π1 < u , v > , π2 < u , v > > {X} ≡ < u , v > {X}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 lemma-product-rebuild = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 -- Empty
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 -- Sum
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 _+_ : {l : Level} -> Set l -> Set l -> Set (suc l)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 _+_ {l} U V = {X : Set l} -> (U -> X) -> (V -> X) -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 ι1 : {l : Level} {U V : Set l} -> U -> (U + V)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 ι1 {l} {U} {V} u = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 ι2 : {l : Level} {U V : Set l} -> V -> (U + V)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ι2 {l} {U} {V} v = \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> y v
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 δ {l} {U} {V} {X} u v t = t {X} u v
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 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
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 lemma-sum-iota1 = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 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
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 lemma-sum-iota2 = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 -- Existential
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 data V {l} (X : Set l) : Set l
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 where
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 v : X -> V X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 Σ_,_ : {l : Level} (X : Set l) -> V X -> Set (suc l)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 Σ_,_ {l} U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 ⟨_,_⟩ : {l : Level} (U : Set l) -> (u : V U) -> Σ U , u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ⟨_,_⟩ {l} U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ∇_,_,_ : {l : Level} {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u -> W
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 ∇_,_,_ {l} {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 {-
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 lemma-nabla on proofs and types
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 w[U/X][u/x^[U/X]]
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 -}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 lemma-nabla : {l : Level} {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {l} {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 lemma-nabla = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 -- Int
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 Int : ∀{l} -> {X : Set l} -> Set l
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 Int {l} {X} = X -> (X -> X) -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 O : {l : Level} -> {X : Set l} -> Int
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 O {l} {X} = \(x : X) -> \(y : X -> X) -> x
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 S : ∀ {l X} -> Int {l} {X} -> Int
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 S {l} {X} t = \(x : X) -> \(y : X -> X) -> y (t x y)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 It : ∀{l} {U : Set l} -> (u : U) -> (U -> U) -> Int -> U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 It {l} {U} u f t = t u f
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 lemma-it-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 lemma-it-o = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 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)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 lemma-it-s-o = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 g : ∀{l ll U X} -> {f : U -> Int {l} {X} -> U} -> (U × Int) {l}-> (U × Int) {ll}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 g {l} {ll} {U} {X} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 lemma-g : ∀{l ll U X Y} {u : U} {n : Int} {f : U -> Int {l} {X} -> U} -> g {l} {ll} {U} {X} {f} < u , n > ≡ < f u n , S n > {Y}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 lemma-g = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 lemma-it-n : ∀{l ll U X Y} {u : U} {n : Int {l} {X}} {f : U -> Int {l} {X} -> U} -> (g {l} {ll} {U} {X} {f} < u , n >) ≡ < f u n , S n > {Y}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 lemma-it-n = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 R : ∀{l U X} -> (u : U) -> (U -> Int {_} {X} -> U) -> Int -> U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 R {l} {U} {X} u f t = π1 {l} (It {_} {U × Int} < u , O > (g {f = f}) t)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 lemma-R-O : ∀{l U X} {u : U} {f : (U -> Int {l} {X} -> U)} -> R u f O ≡ u
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 lemma-R-O = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 -- 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}) (↑ n -> π2 < u , n > ))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 -- not finished Proof lemma-R-n
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 -- If applied g for Int. I think Int has type of (Int {?} {U × Int}).
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 --lemma-R-n : ∀{u f}{n : Int} -> R u f (S n) ≡ f (R u f n) n
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 --lemma-R-n = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 -- Proofs And Types Style lemma-R-n
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 --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
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 -- n in (S n) and (R u f n) has (U × Int), but last n has Int.
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 -- regenerate same (n : Int) by used g, <_,_>
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 -- NOTE : Proofs And Types say "equation for recursion is satisfied by values only"
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 -- List
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 List : {l ll : Level} -> (U : Set l) -> Set (l ⊔ (suc ll))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 List {l} {ll} U = {X : Set ll} -> X -> (U -> X -> X) -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 nil : {l : Level} {U : Set l} {ll : Level} -> List U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 nil {l} {U} {ll} = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> x
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 cons : {l : Level} {U : Set l} {ll : Level}-> U -> List U -> List U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 cons {l} {U} {ll} u t = \{X : Set ll} -> \(x : X) -> \(y : U -> X -> X) -> y u (t {X} x y)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 ListIt : {l : Level} {U : Set l} {ll : Level} {W : Set ll} -> W -> (U -> W -> W) -> List U -> W
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 ListIt {l} {U} {ll} {W} w f t = t {W} w f
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 -- (u1 u2 nil)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 lemma-list : {l : Level} {U X : Set l} {u1 u2 : U} {x : X} {y : U -> X -> X} -> (cons u1 (cons u2 nil)) x y ≡ y u1 (y u2 x)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 lemma-list = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 lemma-list-it-nil : {l : Level} {U W : Set l} {w : W} {f : U -> W -> W} -> ListIt w f nil ≡ w
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 lemma-list-it-nil = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 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)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 lemma-list-it-cons = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 -- cannot proove gerenal list ...?
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 --lemma-list-nil-cons : {l ll : Level} {U : Set l} {t : List {l} {ll} U} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) t) ≡ t
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 --lemma-list-nil-cons = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 -- lemma-list-nil-cons for concrete list. has yellow.
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 --elem2-list : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 --elem2-list {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 --lemma-list-nil-cons-val : {l ll : Level} {U : Set l} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) elem2-list) ≡ elem2-list
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 --lemma-list-nil-cons-val = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 -- Binary Tree
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 data BinTree {l : Level} : Set (suc l) where
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 leaf : BinTree
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 couple : BinTree -> BinTree -> BinTree
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 BinTreeIt : {l : Level} -> {W : Set l} -> W -> (W -> W -> W) -> BinTree {l} -> W
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202 BinTreeIt w f (couple left right) = f (BinTreeIt w f left) (BinTreeIt w f right)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203 BinTreeIt w f leaf = w
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206 lemma-binary-tree-it-leaf : {l : Level} {W : Set l} {w : W} {f : W -> W -> W} -> BinTreeIt w f leaf ≡ w
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 lemma-binary-tree-it-leaf = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
208
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
209 lemma-binary-tree-it-tree : {l : Level} {W : Set l} {w : W} {f : W -> W -> W} {u v : BinTree} -> BinTreeIt w f (couple u v) ≡ f (BinTreeIt w f u) (BinTreeIt w f v)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
210 lemma-binary-tree-it-tree = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
211
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
212
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
213 -- Tree
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 Tree : {l : Level} -> (U : Set l) -> Set (suc l)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216 Tree {l} U = {X : Set l} -> X -> ((U -> X) -> X) -> X
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218 Leaf : {l : Level} {U : Set l} -> Tree U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
219 Leaf {l} {U} = \{X : Set l} -> \(x : X) -> \(y : (U -> X) -> X) -> x
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
220
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
221 collect : {l : Level} {U : Set l} -> (U -> Tree U) -> Tree U
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222 collect {l} {U} f = \{X : Set l} -> \(x : X) -> \(y : ((U -> X) -> X)) -> y (\(z : U) -> f z {X} x y)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
223
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224 TreeIt : {l : Level} {U W : Set l} -> W -> ((U -> W) -> W) -> Tree U -> W
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
225 TreeIt {l} {U} {W} w h t = t {W} w h
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
226
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
227 lemma-tree-it-nil : {l : Level} {U W : Set l} {w : W} {h : (U -> W) -> W} -> TreeIt {l} {U} {W} w h Leaf ≡ w
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
228 lemma-tree-it-nil = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
229
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
230 lemma-tree-it-collect : {l : Level} {U W : Set l} {w : W} {h : (U -> W) -> W} {f : U -> Tree U} -> (TreeIt w h (collect f)) ≡ (h (\(x : U) -> TreeIt w h (f x)))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
231 lemma-tree-it-collect = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
232
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
233