F* tactics proposal

Would like to design and implement a tactic language for F* inspired by the tactics of Lean. This is the summary of a discussion in Redmond on Nov 30, 2016, and some more thinking afterwards. Some more thoughts here https://github.com/FStarLang/FStar/wiki/A-roadmap-for-F*#tactics-and-meta-f

Effect order

Pure <: ML <: Tactic <: Meta

Meta effect

This is the ML effect (divergence, exceptions, state) with additional support for reading and writing the type-checker's internal state. This is useful for implementing tactics (see below) as well as other meta-programs such as:

• Dijkstra monad transformations
• deriving things like hasEq (mk_dec_eq_instance.lean) or Low*'s is_first_order check
• parser and pretty printer extensions
• program generation, e.g. by lightweight modular staging
• ...

Internal state of the type-checker includes:

• list of imported modules
• list of previous top-level definitions for current module
• typing context (bound variables)
• for tactics: the statement we're trying to prove (Lean has: list of proof goals and a distinguished final one)

As in Lean, we will provide a term datatype that exposes the internal term representation of F* (called expr in Lean). Uses of term are compiled directly to uses of F*'s internal term/term' datatype. The representation of terms in tactics could be named and only behind the scenes desugar to locally nameless.

TODO: Discuss quoting and anti-quoting constructs; Lean inserts this automatically, but we could write them explicitly at first.

Implementation strategy

By dynamically linking the OCaml native code compiler in the F* binary, per discussion with Jonathan. A bit technical but doesn't seem too hard.

Longer-term we could implement the same story in F# too, so that we can still use the F# type-checker for debugging even programs that have tactics in them.

Tactic effect

The Tactic effect is a sub-effect of Meta aimed at preserving soundness, by only allowing the type-checker's internal state to be changed in safe ways. It can still read the type-checker's state without further restrictions. This seems like a pragmatic way to ensure soundness without going into the pain of having proof terms or even a small LCF-style kernel.

Operations we envision exporting for the Tactic effect:

• print/show ... could start more specialized
• reading the state (e.g. get_local in Lean)
• z3 : unit -> Tactic unit
• exact (t : term) : Tactic unit = if type_of t <: goal then ...
• normalize: term -> Tactic term
• unify: term -> term -> Tactic unit (with a variant for definitional equality, which doesn't instantiate unification variables)
• intro: name -> Tactic unit
• revert
• type_of: term -> Tactic term
• sorry/admit - allows the user to cheat, but should issue a warning
• ... (here are Lean's combinators)

First use case of this (April-May demo?)

let f (x:t) = e <: ST t wp by <tactic>

Where <tactic> ∈ {z3, lean, christoph, nonlinear}

Editor integration / User interaction story

To be determined, but of course very important. Could start with a tactic that prints the current proof goal for "printf tactic debugging".

Board pictures

Learning Lean tactics

Some starting points

• https://github.com/leanprover/lean/blob/master/library/init/meta/tactic.lean
• https://github.com/leanprover/lean/blob/master/library/init/meta/mk_dec_eq_instance.lean
• https://github.com/leanprover/lean/blob/master/library/init/meta/converter.lean
• https://github.com/leanprover/lean/blob/master/tests/lean/run/converter.lean
• https://github.com/leanprover/lean/blob/master/library/init/monad.lean (gone?)

Bigger examples

• https://github.com/leanprover/library_dev
• https://github.com/avigad/auto