interval characterization proofs and worked examples

1 files changed, 33 insertions, 0 deletions

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)]