-
Notifications
You must be signed in to change notification settings - Fork 28
/
conv_eval.lean
137 lines (116 loc) · 4.15 KB
/
conv_eval.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
set_option maxHeartbeats 10000000000
set_option maxRecDepth 10000000000
universe u v
def CBool := ∀ (B : Type), B → B → B
def ctrue : CBool := λ B t f => t
def cand : CBool → CBool → CBool := λ a b B t f => a B (b B t f) f
def the (A : Type u) (x : A) := x
def CEq {A : Type u}(x y : A) := ∀ (P : A → Type v), P x → P y
def crefl {A}{x:A} : CEq x x := λ P px => px
def CNat := ∀ (N : Type 2), (N → N) → N → N
def add : CNat → CNat → CNat := λ a b n s z => a n s (b n s z)
def mul : CNat → CNat → CNat := λ a b N s z => a N (b N s) z
def suc : CNat → CNat := λ a N s z => s (a N s z)
def n2 : CNat := λ N s z => s (s z)
def n3 : CNat := λ N s z => s (s (s z))
def n4 : CNat := λ N s z => s (s (s (s z)))
def n5 : CNat := λ N s z => s (s (s (s (s z))))
def n10 := mul n2 n5
def n10b := mul n5 n2
def n15 := add n10 n5
def n15b := add n10b n5
def n18 := add n15 n3
def n18b := add n15b n3
def n19 := add n15 n4
def n19b := add n15b n4
def n20 := mul n2 n10
def n20b := mul n2 n10b
def n21 := suc n20
def n21b := suc n20b
def n22 := suc n21
def n22b := suc n21b
def n23 := suc n22
def n23b := suc n22b
def n100 := mul n10 n10
def n100b := mul n10b n10b
def n10k := mul n100 n100
def n10kb := mul n100b n100b
def n100k := mul n10k n10
def n100kb := mul n10kb n10b
def n1M := mul n10k n100
def n1Mb := mul n10kb n100b
def n5M := mul n1M n5
def n5Mb := mul n1Mb n5
def n10M := mul n5M n2
def n10Mb := mul n5Mb n2
def Tree := ∀ (T : Type 1), (T → T → T) → T → T
def leaf : Tree := λ T n l => l
def node (t1 t2 : Tree) : Tree := λ T n l => n (t1 T n l) (t2 T n l)
def fullTree (n : CNat) : Tree := n Tree (λ t => node t t) leaf
def fullTree2 (n : CNat) : Tree := n Tree (λ t => node t (node t leaf)) leaf
-- full tree with given trees at bottom level
def fullTreeWithLeaf : Tree → CNat → Tree
:= λ bottom n => n Tree (λ t => node t t) bottom
def forceTree : Tree → Bool
:= λ t => t CBool cand ctrue _ true false
--------------------------------------------------------------------------------
def t15 := fullTree n15
def t15b := fullTree n15b
def t18 := fullTree n18
def t18b := fullTree n18b
def t19 := fullTree n19
def t19b := fullTree n19b
def t20 := fullTree n20
def t20b := fullTree n20b
def t21 := fullTree n21
def t21b := fullTree n21b
def t22 := fullTree n22
def t22b := fullTree n22b
def t23 := fullTree n23
def t23b := fullTree n23b
-- Nat conversion
--------------------------------------------------------------------------------
-- def convn1M : CEq n1M n1Mb := crefl
-- def convn5M : CEq n5M n5Mb := crefl
-- def convn10M : CEq n10M n10Mb := crefl
-- Full tree conversion
--------------------------------------------------------------------------------
-- def convt15 : CEq t15 t15b := crefl
-- def convt18 : CEq t18 t18b := crefl
-- def convt19 : CEq t19 t19b := crefl
-- def convt20 : CEq t20 t20b := crefl
-- def convt21 : CEq t21 t21b := crefl
-- def convt22 : CEq t22 t22b := crefl
-- def convt23 : CEq t23 t23b := crefl
-- Full meta-containing tree conversion
--------------------------------------------------------------------------------
-- def convmt15 := the (CEq t15b (fullTreeWithLeaf _ n15)) crefl
-- def convmt18 := the (CEq t18b (fullTreeWithLeaf _ n18)) crefl
-- def convmt19 := the (CEq t19b (fullTreeWithLeaf _ n19)) crefl
-- def convmt20 := the (CEq t20b (fullTreeWithLeaf _ n20)) crefl
-- def convmt21 := the (CEq t21b (fullTreeWithLeaf _ n21)) crefl
-- def convmt22 := the (CEq t22b (fullTreeWithLeaf _ n22)) crefl
-- def convmt23 := the (CEq t23b (fullTreeWithLeaf _ n23)) crefl
-- Full tree forcing
--------------------------------------------------------------------------------
-- #reduce forceTree t15
-- #reduce forceTree t18
-- #reduce forceTree t19
-- #reduce forceTree t20
-- #reduce forceTree t21
-- #reduce forceTree t22
-- #reduce forceTree t23
-- #reduce t15
-- #reduce t18
-- #reduce t19
-- #reduce t20
-- #reduce t21
-- #reduce t22
-- #reduce t23
-- #eval forceTree t15
-- #eval forceTree t18
-- #eval forceTree t19
-- #eval forceTree t20
-- #eval forceTree t21
-- #eval forceTree t22
-- #eval forceTree t23