Skip to content

Latest commit

 

History

History
43 lines (26 loc) · 3.62 KB

README.md

File metadata and controls

43 lines (26 loc) · 3.62 KB
Raw

mm0-lean

This is not a particular product, but rather a collection of scratch files and formalizations at different levels of interest.

Compilation

This has not been set up with a leanpkg.toml file, because I'm not sure how well leanpkg deals with projects that don't live at the root of the repo. Instead, I just use a leanpkg.path file. This file is not versioned, so if you want to compile the lean files, you should create a leanpkg.lean file at the root of the repo, containing:

builtin_path
path mm0-lean
path path/to/mathlib/src
path path/to/flypitch/src

You must have the mathlib and flypitch projects installed, and should point to them above relative to the mm0 base directory.

Points of interest

  • mm0/set is a framework for translating theorems from set.mm into lean.

    • mm0/set/basic.lean is the initial file, which contains lean definitions replacing all the metamath axioms (mostly "definition axioms").

    • mm0/set/set1.lean through mm0/set/set6.lean are autogenerated files, produced by translating set.mm to MM0, and from there to Lean, using mm0-hs as follows:

      stack exec -- mm0-hs from-mm set.mm -f dirith,elnnne0 -o out.mm0 out.mmu
stack exec -- mm0-hs to-lean out.mm0 out.mmu -a .basic -c 2000 -o mm0-lean/mm0/set/set.lean
      • The -f dirith,elnnne0 says we are interested in the theorems dirith and elnnne0 and their dependents (which is significantly less than all of set.mm, and generally preferred if you have a particular goal theorem).
      • The -c 2000 controls how many theorems appear in each lean file, because lean tends to choke on very large files.

    • mm0/set/post.lean is a manually written postprocessing file, that imports the autogenerated theorems and relates Metamath notions to Lean notions, so that one can obtain a native-Lean statement rather than a deep embedded Metamath statement in Lean. Currently, we are demonstrating this by proving theorem dirith' (Dirichlet's theorem), which uses only Lean definitions but is processed from the analogous MM theorem dirith.

  • mm0/basic.lean and mm0/meta.lean are an experimental framework for being able to write MM0 theorems by syntactic restriction of lean theorems, and mm0/set.lean is a demonstration.

  • mm0/mm0b.lean is a formalization of the MMB operational semantics in lean.

  • mm0/fol.lean is a syntactic model of MM0/ZFC in Lean using deep embedding to schemes in FOL in the language of ZFC. This is WIP but proves soundness of MM0 with set.mm axioms.

  • x86/ contains a number of experimental formalizations relating to verified compilation down to a model of x86-64.

  • x86/x86.lean is a formalization of the full x86 model that is of interest for the MM0 bootstrapping project. It is parallel to examples/x86.mm0.

  • x86/lemmas.lean proves some facts about the model, in particular determinism of the decoder.

  • x86/assembly.lean formalizes an initial assembly pass to make labels symbolic and remove explicit reference to the PC.

  • x86/matching.lean and x86/separation.lean are two competing formalizations for higher level constructs, based on matching logic (see K framework) and separation logic (see Iris et al.) respectively.