diff options
| -rw-r--r-- | README.org | 5 | ||||
| -rw-r--r-- | examples/README.org | 52 | ||||
| -rw-r--r-- | examples/arithmetic.sol | 17 | ||||
| -rw-r--r-- | examples/constraints.sol | 27 | ||||
| -rw-r--r-- | examples/family.sol | 27 | ||||
| -rw-r--r-- | examples/integrity.sol | 35 | ||||
| -rw-r--r-- | examples/quantifiers.sol | 40 | ||||
| -rw-r--r-- | examples/recursion.sol | 33 | ||||
| -rw-r--r-- | theories/Interval.v | 80 | ||||
| -rw-r--r-- | theories/dune | 9 |
10 files changed, 323 insertions, 2 deletions
@@ -191,7 +191,10 @@ algebra. Build with =nix develop -c dune build=; run the tests with =nix develop -c dune runtest=; run a program with =dune exec sol -- -file.sol=. +file.sol=. Worked examples live in =examples/= (see +=examples/README.org=); machine checked proofs in =theories/= +(structural and lexicographic decrease, extracted into admission; +the interval characterizations behind propagation). Machine checked proofs live in =theories/=: the admission checker's core claim, that strict containment decreases a well founded 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)] diff --git a/theories/Interval.v b/theories/Interval.v new file mode 100644 index 0000000..7562170 --- /dev/null +++ b/theories/Interval.v @@ -0,0 +1,80 @@ +(* The integer-tightening facts behind the interval engine. + + Propagate.lower_int and Propagate.upper_int in lib/vm.ml convert + rational bounds into integer endpoints: a non-strict lower bound + q becomes ceiling q, a strict one becomes floor q + 1, and dually + for upper bounds. These four characterizations say the + conversions are exactly right: an integer satisfies the rational + bound iff it satisfies the tightened integer bound. Both + propagation (enumeration endpoints, contradiction detection) and + symbolic discharge (entailment over integer kinds) lean on + them. *) + +From Stdlib Require Import QArith Qround ZArith Lia. + +Lemma inject_Z_le : forall a b : Z, (a <= b)%Z <-> (inject_Z a <= inject_Z b)%Q. +Proof. intros a b; unfold Qle, inject_Z; simpl; lia. Qed. + +Lemma Qfloor_inject : forall z : Z, Qfloor (inject_Z z) = z. +Proof. intro z; unfold Qfloor, inject_Z; simpl; apply Z.div_1_r. Qed. + +Lemma Qceiling_inject : forall z : Z, Qceiling (inject_Z z) = z. +Proof. + intro z; unfold Qceiling, Qopp, Qfloor, inject_Z; simpl. + rewrite Z.div_1_r; lia. +Qed. + +(* Non-strict lower bound: q <= z iff ceiling q <= z. *) +Lemma lower_nonstrict : forall (q : Q) (z : Z), + (q <= inject_Z z)%Q <-> (Qceiling q <= z)%Z. +Proof. + intros q z; split; intro H. + - rewrite <- (Qceiling_inject z). apply Qceiling_resp_le; exact H. + - apply Qle_trans with (inject_Z (Qceiling q)); [ apply Qle_ceiling | ]. + exact (proj1 (inject_Z_le _ _) H). +Qed. + +(* Strict lower bound: q < z iff floor q + 1 <= z. *) +Lemma lower_strict : forall (q : Q) (z : Z), + (q < inject_Z z)%Q <-> (Qfloor q + 1 <= z)%Z. +Proof. + intros q z; split; intro H. + - assert (Hle : (Qfloor q <= z)%Z). + { rewrite <- (Qfloor_inject z). apply Qfloor_resp_le. + apply Qlt_le_weak; exact H. } + destruct (Z.eq_dec (Qfloor q) z) as [ Heq | ]; [ | lia ]. + exfalso. + apply (Qlt_irrefl (inject_Z z)). + eapply Qle_lt_trans; [ | exact H ]. + rewrite <- Heq. apply Qfloor_le. + - apply Qlt_le_trans with (inject_Z (Qfloor q + 1)); [ apply Qlt_floor | ]. + exact (proj1 (inject_Z_le _ _) H). +Qed. + +(* Non-strict upper bound: z <= q iff z <= floor q. *) +Lemma upper_nonstrict : forall (q : Q) (z : Z), + (inject_Z z <= q)%Q <-> (z <= Qfloor q)%Z. +Proof. + intros q z; split; intro H. + - rewrite <- (Qfloor_inject z). apply Qfloor_resp_le; exact H. + - apply Qle_trans with (inject_Z (Qfloor q)); [ | apply Qfloor_le ]. + exact (proj1 (inject_Z_le _ _) H). +Qed. + +(* Strict upper bound: z < q iff z <= ceiling q - 1. *) +Lemma upper_strict : forall (q : Q) (z : Z), + (inject_Z z < q)%Q <-> (z <= Qceiling q - 1)%Z. +Proof. + intros q z; split; intro H. + - assert (Hle : (z <= Qceiling q)%Z). + { rewrite <- (Qceiling_inject z). apply Qceiling_resp_le. + apply Qlt_le_weak; exact H. } + destruct (Z.eq_dec z (Qceiling q)) as [ Heq | ]; [ | lia ]. + exfalso. + apply (Qlt_irrefl (inject_Z z)). + eapply Qlt_le_trans; [ exact H | ]. + rewrite Heq. apply Qle_ceiling. + - apply Qle_lt_trans with (inject_Z (Qceiling q - 1)). + + exact (proj1 (inject_Z_le _ _) H). + + apply Qceiling_lt. +Qed. diff --git a/theories/dune b/theories/dune index 57cccb6..bde0f7f 100644 --- a/theories/dune +++ b/theories/dune @@ -22,6 +22,13 @@ (setenv OCAMLPATH "" (run coqc -q Lex.v)))) +(rule + (targets Interval.vo Interval.glob) + (deps Interval.v) + (action + (setenv OCAMLPATH "" + (run coqc -q Interval.v)))) + (alias (name default) - (deps Decrease.vo DecreaseChecker.vo Lex.vo)) + (deps Decrease.vo DecreaseChecker.vo Lex.vo Interval.vo)) |