search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
84 stars 18 forks source link

Definition specialization #39

Closed Vtec234 closed 1 year ago

Vtec234 commented 1 year ago

Adds a partial evaluator with an associated specialize_def tactic. For an explanation of how it works, please see Playground/WHNFExamples.lean. It is helpful on some small goals, but unfortunately has inadequate performance on any large expression (e.g. a crypto algorithm). The F* community uses an NbE evaluator for this sort of thing, and we may need one as well.

Depends on #37.

Vtec234 commented 1 year ago

@abdoo8080 this PR is not a priority so no rush with the review. I am not sure we should even merge it given the performance issues which I'll get back to in September. I think the only generally applicable change is in Smt/Term.lean, everything else is partial evaluation stuff.