gen_smt_vcs: translate SMT datatypes to Lean inductives - #1480
kondylidou wants to merge 7 commits into
Conversation
Datatype sorts fell through to the uninterpreted-sort lookup and constructor, tester and selector applications had no translation case, so a VC over a datatype could not become a Lean goal. - Translate.lean: SanitizedDatatype, a datatype map in the translator state, cases for datatype sorts and datatype_op constructor/tester/selector. Fix: several modify/set sites rebuilt the state without `s with`, dropping every field but level/bvars at each binder. - MetaVerifier.lean: SanitizedContext.datatypes; ensureDatatypeDecls adds `inductive <thm>.DT.<d>` with casesOn-based testers and selectors before translation, under the current declaration's prefix. - Test: GenSMTVCsDatatypes.lean. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
joscoh
left a comment
joscoh
left a comment
There was a problem hiding this comment.
It's not super important, since they aren't used much, but Strata datatypes also generate an eliminator encoding the induction principle of the type. Maybe doesn't need to be added in this PR, but there should at least be a comment noting that it is unsupported.
Separately, it would be good to see an example of a recursive function over an inductive datatype and the Lean proof goals that result.
| let tyName := SanitizedDatatype.typeName ns dt.name | ||
| let sortExpr (t : TermType) : MetaM Lean.Expr := | ||
| Lean.ofExcept ((Translate.withDatatypes ns dts (Translate.translateSort t)).run' {}) | ||
| -- default witness: first constructor whose fields all have a default |
There was a problem hiding this comment.
If I understand correctly, this relies on the correctness of the datatype inhabitation check, right?
There was a problem hiding this comment.
You're right, and it matters more than I assumed. The selectors are total:
applied to the wrong constructor they return a fixed default. SMT-LIB leaves
that unspecified, so a VC is valid only if it holds for every choice. By
picking one, a Lean goal could be provable when the VC is not universally valid.
Strata's body_calls obligations mean well-formed programs never rely on it,
but that is practice, not soundness.
Fix: make the out-of-range result opaque, one opaque constant per selector, so
nothing can be proved about it. Inhabitation then only decides whether the
constant can be declared.
| -- declarations added programmatically | ||
| enableRealizationsForConst tyName | ||
| for c in ctors do enableRealizationsForConst c.name | ||
| mkCasesOn tyName |
There was a problem hiding this comment.
Is this creating the Lean definitional induction principle as well?
There was a problem hiding this comment.
addDecl on an .inductDecl has the kernel generate .rec, so the induction
principle is there; mkCasesOn adds casesOn. Not generated: brecOn, below,
.induct — nothing in a translated goal needs them.
| | is : DL.SMT.Sort → Translate.Var | ||
| deriving BEq, Hashable, Repr | ||
|
|
||
| /-- A datatype as the SMT query declared it, in the form the VC→Lean |
There was a problem hiding this comment.
I am confused why the SMT translation needs to change at all. I thought that this PR is only adding datatypes to the VC -> Lean path, not the SMT translation to a solver.
There was a problem hiding this comment.
The name is misleading: DL/SMT/Translate.lean is the VC → Lean translation.
The solver-facing encoder is DL/SMT/Encoder.lean and Core/SMTEncoder.lean,
neither touched here. translateQuery has one caller, MetaVerifier.createGoal.
Thanks for the eliminator, it's ignored here, and I'll note it in a comment rather |
A selector applied to another constructor now falls back to an `opaque` constant of its own rather than a concrete element. SMT-LIB leaves that application unspecified, so a verification condition is valid only if it holds whatever the value is; committing to one could make a Lean goal provable when the condition is not universally valid, and could collapse two selectors onto the same value. The witness is still computed, but only as what an `opaque` declaration needs in order to exist. Also notes that Strata's datatype eliminator is not translated, and adds a recursive function over a datatype to the test, whose termination and selector obligations become goals about the inductive itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t/smt-vcs-datatypes
This branch has not been deployed
3 participants
Closes #1472
Description:
gen_smt_vcshad no datatype support: a datatype sort fell through to the uninterpreted-sort lookup (variable 'Translate.Var.us …' not found) and constructor / tester / selector applications had no translation case, so a VC over adatatypecould not become a Lean goal.Each datatype a query uses now becomes a Lean inductive, generated in the tactic:
DL/SMT/Translate.lean:SanitizedDatatype(constructors and field sorts; non-parametric datatypes), a datatype map in the translator state, and translation cases for.constrsorts anddatatype_opconstructor / tester / selector.MetaVerifier.lean:SanitizedContext.datatypes(the plain projection that survives kernel reduction) andensureDatatypeDecls, which addsinductive <thm>.DT.<d>pluscasesOn-based testersis_<c> : … → Propand selectors before translation. Declarations live under the current theorem's prefix (the kernel restricts declarations added during elaboration), so no instances are registered; a selector applied to another constructor returns a fixed default element, matching SMT-LIB, which leaves that value unspecified.modify/setsites rebuiltTranslate.Statewithouts with, dropping every field butlevel/bvarsat each binder.GenSMTVCsDatatypes.lean: goals overOption,IntListandWrap(a datatype-typed field, declared across goals) with constructors, testers and selectors, discharged withcases+simpon the generated definitions.Not covered: parametric datatypes (left out of
SanitizedDatatype; their sorts are reported unknown as before).lake build/lake testpass.🤖 Generated with Claude Code