F* Lean Integration

Encoding F* obligations in Lean (Nov 30)

We need a way to convert the proof obligations obtained by the Dijkstra monads to Lean. These proof obligations do not include things like pattern matching and recursion. However, these proof obligations have to be checked in a context that includes arbitrary F* definitions with pattern matching and recursion.

There are more options for encoding these F* definitions:

• Olivier tried encoding them to induction principles and stuff
• we could turn them into equations that get converted to Lean using the same conversion as for proof obligations
  • but then we would be duplicating quite a lot of work that's already happening in Lean's equation compiler and we get none of the soundness guarantees it obtains by producing proof terms
  • the advantage of this would be for implementing fold/unfold tactics in F*
• Russel for Lean
  • direct encoding: F* match maps to Lean match, F* fixpoints map to Lean fixpoints
  • this requires extensions to the Lean equation compiler, but that's anyway good for making Lean easier to use

Challenges to overcome:

• extensional to intensional equality
  • semi-automatic casts in Lean (marking just position)
• refiments mapped to sigma types with calls to Lean automation (e.g. an untrusted Z3 tactic) for discharging the proof obligation
• semantic termination checking and termination metrics to accessibility predicates
• need to introduce coercions for subtyping?
• automation in Lean: done by calling Z3 at first
• ...

Demo for May

Prove some of the following using Lean:

• FStar.ListProperties.fst
• FStar.SeqProperties.fst
• FStar.Math.Lemmas.fst (stretch?)

Discussion from 2016-10-06

Translating F* pattern matches:

• F* does semantic exhaustiveness checking
  • Lean does it syntactically, so would need to synthethize a proof of false on all unreachable branches; using custom tactic
• in F* branches are ordered, and on each branch one assumes that the previous branches didn't match
  • Lean does smart expansion of overlapping branches, so should achieve a similar effect
• F* implicitly uses identities in context (extensional type theory)
  • make F* type-checker produce enough annotations in the elaborated proof term to be able to insert coercions in Lean
• Lean provides a way to annotate matches and F* encoding could use that

Translating F* fixpoints to Lean

• F* has built in well-founded order on terms
  • nat, subterm, lex, f x << x
  • in F* this ordering is heterogeneous (e.g. for mutual induction), but could we translate it to a homogeneous one in Lean?
• Lean work item: for each inductive generate subterm relation and well-formedness proof for it

Translating F* effects to Lean

[Tot t] = t
[Pure t wp] = forall p. wp p -> {x:t | wp p}

• use DM4F reification all the other terminating effects

Using F*/Lean tactics for discharging WPs

New syntax: <e>[tactic proof] desugars to let x = e in proof x; x

intuitively proof : A -> squash P(\x. e* Q)