F* Lean Integration

Encoding F* proof obligations in Lean

In any case 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 to have for Lean

Challenges to overcome:

• extensional to intensional equality
• refiments mapped to sigma types with calls to Lean automation (e.g. an untrusted Z3 tactic) for finding the witness
• semantic termination checking and termination metrics
• need to introduce coercions for subtyping
• ...

Demo for May

Prove some of the following using Lean:

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