8
$\begingroup$

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.)
$\endgroup$

1 Answer 1

7
$\begingroup$

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.)

$\endgroup$
5
  • 1
    $\begingroup$ Great answer! It didn't occur to me to use an external verifier to generate the defeq traces. Yes, that seems like the best short-term solution (instead of hacking directly at Lean's or Coq's kernel). $\endgroup$
    – Jason Rute
    Feb 27 at 22:19
  • $\begingroup$ I've always wondered how explicit judgemental equalities might work. So basically if you have an explicit witness |- beta (x. e) e': (fun x => e) e' ~ [x := e'] e. Seems wonky. Would have to be an entirely different sort or universe to avoid weird issues too $\endgroup$ Mar 6 at 20:50
  • $\begingroup$ @MolossusSpondee There is no witness per se; instead there is a proof object entirely separate from the object logic. That is, typing and definitional equality proofs are proofs in the same sense as proofs in FOL: they are not terms that appear in the logic but meta-level objects. It just so happens that in many flavors of DTT the typing judgment is decidable, which is to say that there is an algorithm which maps expressions e to proofs p proves (Gamma |- e : t) where p is a proof object (a tree of DTT rule applications), but e and p are not identified. $\endgroup$ Mar 7 at 7:16
  • $\begingroup$ You can find an (experimental) axiomatization of Lean's type theory in MM0 here, where I've highlighted the conversion rule, and toward the end I work out a few simple typing and conversion proofs. $\endgroup$ Mar 7 at 7:24
  • $\begingroup$ If it helps, you can think of it as similar to a deep embedding of DTT inside a theorem prover (DTT or FOL or pick-your-favorite metalogic). Things like Gamma |- e : t are provable assertions in the logic, so they have proof objects, but these objects (of type Proof (Gamma |- e : t)) are not expressions (of type expr) like e and t. $\endgroup$ Mar 7 at 7:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.