interval characterization proofs and worked examples

7 files changed, 231 insertions, 0 deletions

diff --git a/examples/README.org b/examples/README.org
new file mode 100644
index 0000000..20b853a
--- /dev/null
+++ b/examples/README.org
@@ -0,0 +1,52 @@
+#+TITLE: Sol Examples
+
+* Running
+
+From the repository root, with Nix:
+
+#+BEGIN_SRC sh
+nix develop -c dune exec sol -- examples/family.sol
+#+END_SRC
+
+Or enter the shell once and run them all:
+
+#+BEGIN_SRC sh
+nix develop
+dune build
+for f in examples/*.sol; do echo "== $f"; dune exec sol -- "$f"; done
+#+END_SRC
+
+Without a file argument, =dune exec sol= starts a REPL: declarations
+accumulate, =Query expression: ...= runs immediately, one statement
+per line.
+
+* The files
+
+- =family.sol= :: relations, facts, a rule, joins through shared
+  variables, decidable denial with =:not=, and the =World= scoped
+  negation form.
+- =arithmetic.sol= :: =Plus= and =Times= evaluating forward and
+  solving backward through the rationals; minimal shape, where
+  =1/2 + 1/2= is the integer =1=.
+- =recursion.sol= :: structural recursion admitted by the decrease
+  checker extracted from Rocq, and Even/Odd mutual recursion under a
+  lexicographic measure.
+- =constraints.sol= :: membership is not generation: residuation,
+  interval propagation, finite ranges enumerating, contradictions
+  answering no, and explicit bounded generation with =Between=.
+- =quantifiers.sol= :: universals over infinite domains proven or
+  refuted symbolically, including the specification's own true and
+  false examples and the =Plus= identity; finite quantifiers simply
+  run.
+- =integrity.sol= :: schemas as membership: primitive domains, a
+  refinement, and a foreign key as a criterion. The comments at the
+  bottom show facts that make admission reject the whole program;
+  uncomment one and run again to see it happen.
+
+* Reading the answers
+
+Each query prints one line per answer: variable bindings in Sol
+notation, =yes.= for a closed query that holds, =no.= for one that
+does not. An answer conditioned on open membership prints its
+residual constraints after the bindings, as the propositions they
+are.
diff --git a/examples/arithmetic.sol b/examples/arithmetic.sol
new file mode 100644
index 0000000..a56d82e
--- /dev/null
+++ b/examples/arithmetic.sol
@@ -0,0 +1,17 @@
+% Arithmetic solves backward, and the numeric tower keeps its
+% minimal shape: an integer-valued rational IS the integer.
+
+% Forward: 3 + 4.
+Query expression: [Plus left: 3 right: 4 result: R]
+
+% Backward: what plus 5 gives 12?
+Query expression: [Plus left: X right: 5 result: 12]
+
+% Through the rationals: 3 * X = 2.
+Query expression: [Times left: 3 right: X result: 2]
+
+% Minimal shape: 1/2 + 1/2 is the integer 1, not the rational 2/2.
+Query expression: [Plus left: 1/2 right: 1/2 result: R]
+
+% Rationals reduce on sight: 2/4 equals 1/2.
+Query expression: [Equal left: 2/4 right: 1/2]
diff --git a/examples/constraints.sol b/examples/constraints.sol
new file mode 100644
index 0000000..676f4c1
--- /dev/null
+++ b/examples/constraints.sol
@@ -0,0 +1,27 @@
+% Membership is not generation. Open membership constrains; the
+% engine residuates, propagates, and enumerates only finite ranges.
+
+% An open constraint comes back as the answer's condition.
+Query expression: [Integer value: X]
+
+% A later equality grounds it and the residue discharges.
+Query expression: [Natural value: X] :and [Equal left: X right: 5]
+
+% Bounds that pin an integer into a finite range enumerate, the
+% same admissible enumeration Between performs explicitly.
+Query expression: [Natural value: X] :and [LessThan left: X right: 4]
+
+% Strict rational bounds tighten to integers: 1/2 < X <= 5/2.
+Query expression:
+  [Integer value: X] :and
+  [GreaterThan left: X right: 1/2] :and
+  [LessThanEqual left: X right: 5/2]
+
+% An empty interval is no, not a conditioned maybe.
+Query expression: [GreaterThan left: X right: 5] :and [LessThan left: X right: 3]
+
+% Explicit bounded generation.
+Query expression: [Between value: X lower: 1 upper: 4] :and [GreaterThan left: X right: 2]
+
+% Disjunction branches finitely.
+Query expression: [Equal left: X right: 1] :or [Equal left: X right: 2]
diff --git a/examples/family.sol b/examples/family.sol
new file mode 100644
index 0000000..8d1f7f9
--- /dev/null
+++ b/examples/family.sol
@@ -0,0 +1,27 @@
+% Relations, facts, rules, joins and negation.
+
+Relation named: Person schema: #(
+  [name domain: String]
+  [age domain: Integer]
+)
+
+[Person name: "Marcos" age: 30]
+[Person name: "Ana" age: 12]
+[Person name: "Rui" age: 70]
+
+Rule name: "an adult is a person of age at least 18"
+     head: [Adult name: N]
+     body: [Person name: N age: A] :and
+           [GreaterEqual left: A right: 18]
+
+% Everyone stored.
+Query expression: [Person name: N age: A]
+
+% The rule, joined through the shared variable N.
+Query expression: [Adult name: N]
+
+% Decidable denial: people who are not adults.
+Query expression: ([Person name: N age: A]) :not [Adult name: N]
+
+% The specification's negation form, scoped by the universe.
+Query expression: [World] :not [Adult name: "Ana"]
diff --git a/examples/integrity.sol b/examples/integrity.sol
new file mode 100644
index 0000000..2729f4b
--- /dev/null
+++ b/examples/integrity.sol
@@ -0,0 +1,35 @@
+% Schemas constrain by membership: primitive domains, refinements,
+% and foreign keys are one mechanism. A program whose facts violate
+% them gets no world at all; this one is admitted.
+
+Relation named: Department schema: #(
+  [id domain: Integer]
+  [title domain: String]
+)
+
+[Department id: 1 title: "Engineering"]
+[Department id: 2 title: "Design"]
+
+Relation named: Employee schema: #(
+  [name domain: String]
+  % A foreign key is a membership criterion, nothing more special.
+  % Only the subject D is free; other attributes stay existential.
+  [dept domain: ([Department id: D])]
+  % A refinement: a natural at most 100.
+  [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
+)
+
+[Employee name: "Marcos" dept: 1 score: 90]
+[Employee name: "Ana" dept: 2 score: 75]
+
+Query expression: [Employee name: N dept: D score: S]
+
+% Join through the foreign key.
+Query expression:
+  [Employee name: N dept: D score: S] :and
+  [Department id: D title: T]
+
+% Try it yourself: append one of these lines and watch admission
+% reject the whole program.
+%   [Employee name: "Ghost" dept: 9 score: 50]
+%   [Employee name: "Over" dept: 1 score: 101]
diff --git a/examples/quantifiers.sol b/examples/quantifiers.sol
new file mode 100644
index 0000000..3a65145
--- /dev/null
+++ b/examples/quantifiers.sol
@@ -0,0 +1,40 @@
+% Universals over infinite domains are proven or refuted
+% symbolically, never enumerated.
+
+% The specification's true example: every natural is at least zero.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Natural value: X]
+          body: [GreaterEqual left: X right: 0]]
+
+% The specification's false example: not every integer is.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Integer value: X]
+          body: [GreaterEqual left: X right: 0]]
+
+% Subtype inclusion, decided symbolically: every integer is a
+% rational, literally.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Integer value: X]
+          body: [Rational value: X]]
+
+% The algebra of Plus: adding zero is the identity, over all
+% integers, stated flat as membership.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Integer value: X]
+          body: [Plus left: X right: 0 result: X]]
+
+% Universals over finite quantifiers just run.
+Query expression:
+  [ForAll variable: X
+          quantifier: [Between value: X lower: 1 upper: 5]
+          body: [GreaterThan left: X right: 0]]
+
+% Existence, over a finite quantifier.
+Query expression:
+  [Exists variable: X
+          quantifier: [Between value: X lower: 1 upper: 10]
+          body: [Times left: X right: X result: 49]]
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)]