From b7ab0a9d1f0275db32a526faf7cffe9d520b15c8 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 10:20:13 -0300 Subject: interval characterization proofs and worked examples --- examples/recursion.sol | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 examples/recursion.sol (limited to 'examples/recursion.sol') diff --git a/examples/recursion.sol b/examples/recursion.sol new file mode 100644 index 0000000..0a1c389 --- /dev/null +++ b/examples/recursion.sol @@ -0,0 +1,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)] -- cgit v1.2.3