Gentzen calculus

Stream: general

[Martin Dvořák]

Is it possible to emulate the Gentzen calculus LK in Lean?

[Luigi Massacci]

I did a deep embedding of NJ in lean3 a bunch of time ago, though I'm afraid I nuked the repo at some point. In any case code-and-proofs-wise I was going off of this (the examples are in OCaml or Agda but very easy to adapt. Note that the book is publicly available online but the website of our CS department appears to be down right now).

I don't see why you couldn't do the same thing for LK. You just define the terms inductively and then essentially as far as lean is concerned you are manipulating syntax. If you want something more shallow, interacting with lean props, I imagine it's going to be more difficult. The deep embedding was fun at first but it got pretty boring pretty quickly.

[Luigi Massacci]

Also I think someone already did this in Coq if I’m not mistaken, so you might check that out.

[Floris van Doorn]

I did propositional calculus in natural deduction style, Hilbert style, and Gentzen sequence calculus style in Coq: https://arxiv.org/abs/1503.08744

Glimpse of Lean has some propositional calculus, but only natural deduction style: https://github.com/PatrickMassot/GlimpseOfLean/tree/master/GlimpseOfLean/Exercises/Topics

[Martin Dvořák]

You made a a system for developing a metatheory of propositional logic. This is an overkill for my purposes. I would just like to have a simple assistant for writing LK-like proofs in Lean, for classwork purposes.

[Martin Dvořák]

I am searching for something on this level:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Proving.20in.20Hilbert.20System

[Kishor DhawaIe]

How can I contribute to this website? I am new, and things here are making me lose direction.

[Martin Dvořák]

Kishor DhawaIe said:

How can I contribute to this website? I am new, and things here are making me lose direction.

Website?

[Kishor DhawaIe]

Sorry if I bother your work, I mean, this chatroom.

[Martin Dvořák]

You just did. Or did you want to contribute to mathlib?