Infrastructure changes from PR 385

[keyboardDrummer]

Contains a subset of the changes from #385

Changes

1. NewlineSepBy separator type for formatting preservation
2. Java codegen: list separator preservation, SourceRange overloads
3. Improved pretty printing for C_Simp, B3, Core
4. Fixed SMT encoding for multi-argument functions and Map type
5. Added substFvarLifting for proper de Bruijn index handling

Testing

1. Possibly covered by existing tests
2. Tested on the Java side
3. Covered by existing tests - which were updated
4. Added tests
5. Added tests

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[joehendrix]

Precedence change breaks associativity and same-precedence parenthesization

The change from innerPrec ≤ prec to innerPrec < prec causes the formatter to drop parentheses that are needed to preserve expression structure.

1. Non-associative operators at the same precedence

B3 == and != are both @[prec(15)] with no associativity annotation. For non-associative binary operators, both argument positions get required prec = 15, and both operators output precedence 15.

Formatting (a == b) != c — i.e. not_equal(equal(a, b), c):

Check	prec	innerPrec	Result	Output
Old ≤	15	15	15 ≤ 15 → parens	(a == b) != c ✓
New <	15	15	15 < 15 → no parens	a == b != c ✗

The output a == b != c is genuinely ambiguous — there's no associativity convention to disambiguate it.

2. Associative operators

B3 ==> is @[prec(5), rightassoc]. The DDM precedence convention (DialectM.lean:560-576) assigns:

• Left arg (non-associative side): required prec = 5
• Right arg (associative side): required prec - 1 = 4
• Output precedence: 5

Formatting (true ==> false) ==> true — i.e. implies(implies(true, false), true):

Check	prec	innerPrec	Result	Output
Old ≤	5	5	5 ≤ 5 → parens	(true ==> false) ==> true ✓
New <	5	5	5 < 5 → no parens	true ==> false ==> true ✗

Since ==> is right-associative, true ==> false ==> true parses as true ==> (false ==> true) — a different logical proposition. The same issue affects left-associative operators symmetrically (e.g. B3 <==).

Root cause: The DDM precedence convention lowers the associative side by 1 and relies on ≤ triggering parens when innerPrec == prec on the non-associative side. Changing to < breaks that invariant.

[joehendrix]

substFvarLifting assumes to has no bvars referring to binders inside e

The call liftBVars depth to uses the default cutoff of 0, which shifts all bvars in to. This is incorrect when to has bvars that refer to binders shared with e.

Concrete example:

e  = quant(app(fvar "x", bvar 0))    -- bvar 0 bound by the quant
to = bvar 0                           -- intended to also refer to the quant

substFvarLifting e "x" (bvar 0) descends under the quant (depth = 1), then calls liftBVars 1 (bvar 0) with cutoff 0. Since 0 ≥ 0, the bvar is shifted to bvar 1 — but it should remain bvar 0 since it refers to the quant binder right above.

Adding a cutoff parameter (defaulting to 0) and passing it through to liftBVars would handle this. The current call site in SMTEncoder.lean:539 is safe because its to values (bvar 0, bvar 1, ...) always refer to the outer function definition, not to binders inside body.

This doesn't need to block the PR — at minimum, a doc comment noting the restriction (that to's bvars must be external to e) would prevent misuse.

[joehendrix]

This PR bundles infrastructure improvements including a new NewlineSepBy separator, SMT encoding fixes for multi-argument functions and Map types, and a substFvarLifting utility for de Bruijn index handling.

Two issues were found (the second is minor):

• Precedence bug in Format.lean:321: Changing ≤ to < drops parentheses needed to preserve same-precedence grouping and non-default associativity — e.g., (true ==> false) ==> true formats as true ==> false ==> true, which parses as a different proposition.
• substFvarLifting limitation in LExprWF.lean:334: The liftBVars call uses default cutoff 0, which incorrectly shifts bvars in the replacement term that refer to binders shared with the target expression; the current SMT encoder call site is safe but the restriction should be documented or addressed with a cutoff parameter.

[aqjune-aws]

I think the user must be able to choose which encoding option to use for Map. One option is Array, but another option is to use the axiomatized expression in SMT. This is being tracked in Asana & I am working on this too.

[aqjune-aws]

Can we have extra panic! here checking that the range of sm does not include any .bvar?

[aqjune-aws]

This function will return an ill-formed expression because WF in LExprWF.lean states:

An `LExpr e` is well-formed if it has no dangling bound variables.

but if sm's range has a bound variable, after lifting there will be dangling bound variables. The LExprs are designed to have locally nameless representation: https://chargueraud.org/research/2009/ln/main.pdf

Let's make it clear that substFvarsLifting may break wellformedness.