choose operator in Boole

[kondylidou]

Summary

choose-function declarations (command_choosefndef)

Introduces function f(params) : R := choose z : T . pred(z, params); as a
first-class Boole construct for defining functions by a property rather than an
implementation — similar to Verus spec choose.

Lowering (in StrataBoole/Verify.lean):

1. An uninterpreted function declaration for f.
2. An axiom in 3-forall form:
   ∀ p1:T1, …, ∀ pn:Tn, ∀ z:Tz, (z = f(p1,…,pn)) → pred(z,p1,…,pn)

The 3-forall form avoids de Bruijn index shifting: pred's natural bvar indices
(0 = z, 1 = pn, …, n = p1) match the quantifier nesting exactly.

DDM scope chain: @[scope(b)] v + @[scope(v)] pred gives pred transitive
access to all parameters via resultContext chaining.

Dot separator for choose

Extends normalizeUnicodeQuantifierSeparators (and its byte-position companion
normalizedQuantifierSepStep) in StrataDDM/Elab.lean to recognise the keyword
choose as a binder, rewriting choose z : T . pred → choose z : T :: pred
before DDM parsing. Mirrors the existing ∀/∃ dot normalization.

Both choose_assign and command_choosefndef now accept . or ::.

Files changed

• StrataDDM/StrataDDM/Elab.lean — state-machine extension for choose keyword
• StrataBoole/StrataBoole/Grammar.lean — new command_choosefndef op
• StrataBoole/StrataBoole/Verify.lean — lowering for command_choosefndef
• StrataBooleTest/FeatureRequests/choose_fn.lean — new test
• StrataBooleTest/FeatureRequests/choose_operator.lean — updated to . syntax

[joscoh]

Could you explain why we need separate syntax for functions defined by choose and why we can't use use an inlined function with the existing choose expressions?

[joscoh]

Should this be in FeatureRequests or just regular tests?

[kondylidou]

Merged into choose_operator.lean (which is already imported by StrataBooleTest.lean).
The file wasn't imported before, so its tests weren't running.

[joscoh]

It would be good to see the failing/unknown result if this precondition is omitted.

[kondylidou]

Added chooseFnNoPrecondSeed — without the precondition the ensures still passes,
because the axiom unconditionally asserts good(best(x), x). Comment explains this.

[joscoh]

I know this is ultimately a style preference, and maybe there are other considerations, but I would rather just use \epsilon to avoid this hardcoded 5-character matching. Then choose can be handled exactly like quantifiers.

[kondylidou]

Done, thanks! I replaced the 5-state machine with a single ch == 'ε' check alongside ∀/∃.
Updated Grammar.lean surface syntax and all test programs accordingly.

[joscoh]

Why don't you need an assumption that pred is inhabited?

[kondylidou]

Added a comment: unlike w := ε z . pred (which guards with an existence assertion),
the function form emits the axiom unconditionally. Soundness requires the caller to
guarantee inhabitation, e.g. via requires ∃ z . pred(z, params).

[joscoh]

I don't quite understand this. When you say "Soundness requires the caller to
guarantee inhabitation", is there anything enforcing this or is it up to the user to make sure they don't declare unsound function definitions. In the latter case, how is this better than just writing an axiom directly?

[kondylidou]

Nothing enforces it. You're right that it's essentially syntactic sugar for:

function f(params) : R; -- uninterpreted
axiom ∀ params, pred(f(params), params);

The benefit over writing those two lines directly is just convenience. Soundness is the user's responsibility exactly as with axiom. We could require a proof obligation ∃ z . pred(z, params) at the declaration site, but that would need quantifier alternation (∀ params, ∃ z . pred) which is harder to discharge automatically. For now the design mirrors Verus spec functions, where choose-based definitions are also trusted by convention.