How does Metamath Zero handle CIC as in Lean or Coq?

Question

Metamath Zero (MM0) is a proof assistant developed by Mario Carneiro. It has a metalogic very similar to the metalogic of MetaMath, but it also borrows design choices from Lean (and maybe other sources). It will also (when complete) have novel features such as a fully verified byte code kernel.

My understanding is that one use case of MM0 is as an external checker for other proof assistants. It should be able to take an exported kernel proof from one proof assistant and double check it with its own kernel. (Similarly, it can translate proofs from one axiom system to another in a low level way.)

However, if I understand correctly MM0 uses a rule based logic similar to that of Metamath. For example, one might have a rule that says if x and y are judgementally equal, then they are equal:

type A    x : A    y : A    x ≡ y
---------------------------------
            x = y 

While Martin-Löf type theory (and it's variations) provides the rules to derive that x ≡ y, my understanding is that CIC specifically doesn't require the user to supply a proof/derivation of, say 0 ≡ 0 + 0, but instead just checks it in real time by normalizing each term (or something along those lines). My understanding, for example, is that while Lean does store kernel level proofs for all its theorems (and exports them to the .olean format), it doesn't store the proofs/derivations of judgemental equality (or type checking) since those can be recomputed.

How does (or will) MM0 handle this sort of thing when checking Lean, Coq, or other CIC proofs?

I see a few possibilities:

• Extract the full proof from a modified Lean or Coq kernel including all step-by-step derivations of judgemental equality, type checking, etc.
• Use MM0 tactics to convert a Lean or Coq term proof into a full proof filling in all the gaps.
• MM0's kernel will already have direct support for computational rules similar for those needed to derive judgemental equality and type checking. (And if so, I guess MM0's kernel will be more flexible than Metamath's in that regard, since Metamath's requires one to spell out every little step.)

Answer 1

All three of your possibilities are potential options for future directions, although they get progressively more "future" as you go down the list.

Extract the full proof from a modified Lean or Coq kernel including all step-by-step derivations of judgemental equality, type checking, etc.

This is the current plan. We take an existing Lean/Coq verifier (I've been working with @ammkrn on using nanoda for this) and modify it to give a detailed trace of how each defeq was derived, and translate these 1-1 for MM0 axiom/theorem applications.

Use MM0 tactics to convert a Lean or Coq term proof into a full proof filling in all the gaps.

This is essentially the same as the first one, except that now the Lean kernel or kernel components are being integrated into the MM0 proof assistant. This would be useful for using MM0 as a frontend for a Lean-like language. This is not particularly practical in the near term, however, as MM0 can't possibly compete with Lean and Coq themselves for ease of use in the frontend. It might be usable for small patches on top of e.g. an imported mathlib, however, where for whatever reason you need to write MM0 / Lean glue code, which the MM0 proof assistant is in a better position to construct than Lean.

MM0's kernel will already have direct support for computational rules similar for those needed to derive judgemental equality and type checking. (And if so, I guess MM0's kernel will be more flexible than Metamath's in that regard, since Metamath's requires one to spell out every little step.)

This is on the agenda, but it's still quite pie-in-the-sky at the moment. More specifically, the base MM0 language will remain unchanged, but once the verified kernel is working, I would like to extend the proof to verify the correctness of a kernel with support for native computation a la Lean reduceBool or Coq vm_compute. Given such a kernel, you could write an actual Lean/Coq typechecker and run it, meaning that you could potentially check proofs just as fast as the real thing, with only an additive overhead to set up the kernel itself. (I'm especially excited to apply this technique to SAT solving, because these giant proofs are completely out of reach by traditional methods.)