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/quantifiers.sol | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 examples/quantifiers.sol (limited to 'examples/quantifiers.sol') 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]] -- cgit v1.2.3