blob: 0a1c38938b21d1cf38d99a3bdd6885de076236be (
plain) (
blame)
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
|
% Recursion is admitted only with a termination proof. Length
% decreases structurally: T sits strictly inside #(H | T), and the
% checker that validates this is extracted from Rocq.
Rule name: "an empty list has length zero"
head: [Length list: #() result: 0]
body: [True]
Rule name: "a cons adds one"
head: [Length list: #(H | T) result: R]
body: [Length list: T result: P] :and
[Plus left: 1 right: P result: R]
Query expression: [Length list: #(1 2 3) result: R]
Query expression: [Length list: #("a" "b") result: R]
% Mutual recursion under a shared lexicographic measure: Even and
% Odd pass a shrinking list back and forth.
Rule name: "the empty list is even"
head: [Even list: #()]
body: [True]
Rule name: "a cons flips even to odd"
head: [Even list: #(H | T)]
body: [Odd list: T]
Rule name: "a cons flips odd to even"
head: [Odd list: #(H | T)]
body: [Even list: T]
Query expression: [Even list: #(1 2 3 4)]
Query expression: [Even list: #(1 2 3)]
|
