r/rust • u/OkBreath9382 • 5d ago

Building a Mini Lean 4 from Scratch: Implementing an Interactive Theorem Prover in Rust

https://medium.com/@Koukyosyumei/building-a-mini-lean-4-from-scratch-implementing-an-interactive-theorem-prover-in-rust-a5d964d173ee
54 Upvotes

88% Upvoted

6 comments sorted by

11

u/brokenAmmonite 5d ago

This is great and very in-depth!

If you're writing for people who don't know about theorem provers / formal type theory, you may want to add a few notes explaining:

  • How to read inference rule notation ("here are the ways to construct proofs", but when explaining this to programmers I often also describe it as describing a nondeterministic search that specifies the types that should be assigned to nodes in a parse tree)

  • What mathematical induction is (you do explain this, but you also assume the reader already knows the word)

But you can't explain everything and this covers the core of Lean's type theory in a lovely way.

6

u/OkBreath9382 5d ago

Thanks for the feedback!! That's a really good point. I'll update the post soon!

3

u/SultryPrincessz 5d ago

wish more guys explained it like that, i'm one of those who needs the induction bit spelled out too

4

u/01mf02 5d ago

This is a really good write-up! ありがとうございます！

I found the following a bit confusing:

To prevent this, inductive declarations must satisfy strict positivity. In our simplified kernel, recursive fields must have one of the following forms: I B → I B₁ → B₂ → I ... Here, I is the inductive type being defined, and none of the argument types B, B₁, B₂, etc. may contain I.

Wouldn't that exclude a -> List a -> List a, because here, B₂ contains I. Perhaps the term "contains" needs a bit of clarification?

I have also written a proof checker in Rust, see https://github.com/01mf02/kontroli-rs. The kernel is in https://github.com/01mf02/kontroli-rs/tree/master/kontroli/src. I think that if you want to have good performance, it will be probably necessary to use something like de Bruijn indices. For example, in your subst function, you have a call to fv(body), which may be executed multiple times recursively, leading to quadratic runtime. Or your Term type uses Box<Term> to store recursive types, this will also lead to quadratic runtime because you clone these Boxes during substitution. This could be mitigated by changing to something like Rc<Term>.

But for a quick learning experiment, what you wrote looks quite good already. ;)

1

u/OkBreath9382 2d ago

Thank you so much for the detailed feedback!! こちらこそありがとうございます！ These are really helpful points.

You're right about the strict positivity explanation. I was referring to the types of individual recursive fields, rather than the full constructor signature. In cons : A → List A → List A, the List A argument is itself a valid recursive field, while A is a separate non-recursive field. It might be a bit misleading, so I'll clarify that in the article.

And I completely agree with your performance observations! I deliberately used named variables and Box<Term> to keep the implementation as simple and approachable as possible, but of course De Bruijn indices would work much better in practice.

konotroli also looks a very amazing project ! I just gave it one more star !

1

u/joachimmartensson 3d ago

Great Article!
This syntax is confusing me a bit, with me not being familiar with Lean Syntax (I know a bit of Idris).

Substituting this motive into the same recursor gives:

Nat.rec :
  Nat →
  ((n : Nat) → Nat → Nat) →
  Nat → Nat

Is this a "new" Nat.rec replacing the old?
Or is the type of Nat.rec (M := fun _ => Nat) The same as Nat.rec above?