Unfolding definitions after the fact

[TheoWinterhalter]

Disclaimer: This is a question I asked on Slack and which involved @hacklex and got a terrific answer from @aseemr.

Is there a way to mark function definitions as unfold after the fact? In other words have a

let foo = (* ... *)

and then suddenly have it behave as if it was

unfold let foo = (* ... *)

An instance I am interested in is to take

let n = 0
let m = 1

let foo = n + m

and produce a new version of foo where both n and m are directly unfolded:

unfold let foo' = 0 + 1

Typically, I would prove things about n, m and foo in ways that work better if they are kept abstract and do not flood the SMT solver with superfluous information. However at the end of the day, I want foo to be unfolded so that it generates SMT that do not require manually unfolding it.

[TheoWinterhalter]

Transcript from @aseemr's answer.

F* has a postprocess_with attribute that lets one run a meta-program (tactic) on a definition after it has type-checked. It has to solve a goal of the form e == ?u (where e is the body of the function), hence the trefl tactic at the end.

module Test

open FStar.Tactics

[@@ "opaque_to_smt"]
let n = 0

[@@ "opaque_to_smt"]
let m = 1

let t () : Tac unit = norm [delta_only [`%n; `%m]]; trefl ()

[@@ (postprocess_with t)]
let foo = n + m

let test () = assert (foo == 1)

The backtick followed by %n here quotes n.

The same method can be used to make a definition unfold after the fact:

module Test

open FStar.Tactics

[@@ "opaque_to_smt"]
let k = 0

let t () : Tac unit = norm [delta_only [`%k]]; trefl ()

[@@ (postprocess_with t)]
unfold
let k' = k

#set-options "--no_smt"
//With no smt, this proof relies on k' being unfolded in the typechecker
let test2 () = assert (k' == 0)