-
Notifications
You must be signed in to change notification settings - Fork 438
/
termination_by_where.lean
286 lines (235 loc) · 7.79 KB
/
termination_by_where.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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
/-!
This module systematically tests various indentation variants related to `where` and
`termination_by`/`decreasing_by`.
The naming convention is `Ex<a><b><c><d><e>.foo` where
* `a` is the column of `def`
* `b` is the column of `where
* `c` is the column of `bar` (or `h` if `bar` is hanging after the `where`)
* `d` is the column of `bar`’s `decreasing_by` (or `_` if `bar` is not recursive)
* `e` is the column of `foo`’s `decreasing_by` (or `_` if `foo` is not recursive)
-/
-- For concise recursive definition that need well-founded recursion
-- and `decreasing_by` tactics that would fail if run on the wrong function
opaque dec1 : Nat → Nat
axiom dec1_lt (n : Nat) : dec1 n < n
opaque dec2 : Nat → Nat
axiom dec2_lt (n : Nat) : dec2 n < n
def Ex00000.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex0000_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
-- This combination is not supported
def Ex000_0.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt -- picked up by bar
def Ex00002.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
-- This combination is not supported
def Ex000_2.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar m
decreasing_by apply dec1_lt -- picked up by bar
def Ex00020.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex0002_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
-- Not supported
def Ex00200.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- Not supported
def Ex0020_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
def Ex002_0.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt
-- Not supported
def Ex00202.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- This combination is not supported
def Ex002_2.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar m
decreasing_by apply dec1_lt -- picked up by bar
def Ex00220.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex00240.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex0022_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
def Ex0042_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
-- Not supported
def Ex02200.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- Not supported
def Ex0220_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
def Ex022_0.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt
-- Not supported
def Ex02202.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- This combination is not supported
def Ex022_2.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar m
decreasing_by apply dec1_lt -- picked up by bar
def Ex02220.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex02240.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex0222_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
def Ex0224_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
-- Not supported
def Ex02400.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- Not supported
def Ex0240_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
def Ex024_0.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt
-- Not supported
def Ex02402.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- This combination is not supported
def Ex024_2.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar m
decreasing_by apply dec1_lt -- picked up by bar
-- Not supported
def Ex02420.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
def Ex02440.foo (n : Nat) := foo (dec1 n) + bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
-- Not supported
def Ex0242_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
def Ex0244_.foo (n : Nat) := bar n
where
bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
-- Not supported
def Ex00h00.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- Not supported
def Ex00h0_.foo (n : Nat) := bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
def Ex00h_0.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := m
decreasing_by apply dec1_lt
-- Not supported
def Ex00h02.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
-- This combination is not supported
def Ex00h_2.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar m
decreasing_by apply dec1_lt -- picked up by bar
-- Not supported
def Ex00h20.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- needs to be indented
decreasing_by apply dec1_lt
def Ex00h40.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- Needs to be indented
decreasing_by apply dec1_lt
def Ex00h60.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
def Ex00h80.foo (n : Nat) := foo (dec1 n) + bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
decreasing_by apply dec1_lt
-- Not supported
def Ex00h2_.foo (n : Nat) := bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- Needs to be indented
-- Not supported
def Ex00h4_.foo (n : Nat) := bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt -- Needs to be indented
def Ex00h6_.foo (n : Nat) := bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt
def Ex00h8_.foo (n : Nat) := bar n
where bar (m : Nat) : Nat := bar (dec2 m)
decreasing_by apply dec2_lt