Skip to content

Latest commit

 

History

History
36 lines (21 loc) · 3.15 KB

README.md

File metadata and controls

36 lines (21 loc) · 3.15 KB

mm0-lean

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

Compilation

The mm0-lean directory is a lean 3 package with a leanpkg.toml file, so it should work out of the box to run lean --make in the subdirectory.

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/set.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.mmu -a .basic -c 2000 -n mm -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/meta/basic.lean and mm0/meta/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.