begin [object_logic]

Stream: Is there code for X?

[Paweł Balawender]

Hey! I stumbled upon this code, used for using a smaller logic inside of Lean 3, such that you define some axioms and inference rules, and instead of proving a goal of the form "Using inference rules, from the axioms Gamma you can infer sentence phi", you just assume Gamma and prove phi. But I'm unable to find documentation for this feature (begin [modal]) and I'm unsure if it even exists in Lean 4. Do you know how it's called and if it's available in Lean 4?
image.png
image.png
these are from this presentation: https://lean-forward.github.io/lean-together/2019/slides/hudon.pdf

[Robin Arnez]

I think this may be part of a library? At least not core lean

[Robin Arnez]

Not sure whether it has been ported to lean 4

[Paweł Balawender]

Cool! I will be happy to try porting it if you have any pointers where's the original documentation for this syntax

[Kyle Miller]

It's a Lean 3 feature that doesn't exist in Lean 4.

The way Lean 3's tactics work is namespace-based. I think begin ... end is the same as begin [tactic] ... end (maybe I got tactic itself wrong), and then the main tactic parser looked in that namespace for tactic definitions. This let you create, for example, a namespace of temporal tactics. Every tactic you see there as a temporal equivalent, or at least it's the corresponding tactic tactic redeclared in the temporal namespace.

One of the main uses of this was conv mode, if I remember correctly.

There's no direct equivalent in Lean 4. You could make a by_temporal syntax with a custom temporalTactic syntax category, and then build a custom tactic executor. It could be that temporal => ... is the tactic that goes into "temporal mode". You could model the whole thing on how conv => ... works. There's no framework for doing this, but all the metaprogramming API is there to make it possible.

Probably easier is to make tactics for temporal reasoning and use them as normal tactics.

[Kevin Buzzard]

NNG3 used begin [natnumgame] internally to cripple rw.

[Mario Carneiro]

nowadays you can use syntax overrides for that

[Mario Carneiro]

One of the main uses of this was conv mode, if I remember correctly.

I don't think conv mode was using this feature, although it did bear some other similarities to "tactic namespaces". The main tactic namespace used in lean 3 was [smt] (and it wasn't used at all :skull: )

[Paweł Balawender]

Thank you for the informative answer @Kyle Miller ! Do I understand correctly that defining a new syntactic category also enables you to prevent the "user" from using tactics from outside of the pre-defined set? This is actually the most important to me; to guarantee to the reader that a proof does not use anything except a couple "easy" tactics

[Paweł Balawender]

Mario Carneiro said:

One of the main uses of this was conv mode, if I remember correctly.

I don't think conv mode was using this feature, although it did bear some other similarities to "tactic namespaces". The main tactic namespace used in lean 3 was [smt] (and it wasn't used at all :skull: )

oh nice! i just saw a paper about using a smt-solver for lean proofs from may 21 (https://arxiv.org/pdf/2505.15796 ) - it's not relevant to my work though

[Kyle Miller]

Yes, you can definitely make your own tactic language using your own syntax category.

Maybe easiest is to implement it using macros that expand your locked-down language to the "real" tactics. (On my phone, otherwise I'd make you a simple example.)

[Paweł Balawender]

Okay, I managed to write some code for it and it looks really promising! I run into an issue I'm not sure how to fix though. First, what I did:

• I defined 2 new syntactic categories: 1) to express logical formulas (theorem statements) in my small logic 2) to express proofs in my proof system
• I added elaboration rules for them

• I have a nice working example:
  image.png
  image.png

  
  

• the whole code is here: live.lean-lang.org/..

But what's problematic is that currently the whole block inside begin_min is evaluated at once. Namely, I have implemented the begin_min block like:

elab_rules : tactic
  | `(tactic| begin_min $[$tacs:minitactic]*) => do
      let mut tacList : Array (TSyntax `tactic) := #[]
      for tacNode in tacs do
        let newTac : TSyntax `tactic ← match tacNode with
          | `(minitactic| introduce $h:term)       => `(tactic| intro $h:term)
[...]

which seems to make the whole block a single tactic; the proof state changes with adding / removing minitactics from the block, but it doesn't change when traversing the proof interactively (just using keyboard arrows to go up/down). For now, I don't see how to fix that without moving into the open world of tactic syntactic category, but maybe a solution would be to 'break' the proof state by changing the goal which is not provable from anything except my minitactics? then redefine my minitactics into normal tactics from the tactic category. Do you have any idea how to make it more interactive? :)

Btw, I think it would be really nice to have such embeddings for popular logics (modal, minimal, linear, classical) inside mathlib: Mathlib.ProofTheory, complementary to Mathlib.ModelTheory

[Aaron Liu]

You should output the state at points inside the begin_min block

[Aaron Liu]

The rw tactic does it using docs#Lean.Elab.Tactic.withTacticInfoContext

[Paweł Balawender]

Wow thanks @Aaron Liu ! Now it really is interactive :)

declare_syntax_cat minitactic
syntax "assume " ident " : " term                       : minitactic
syntax "introa " ident                                  : minitactic
syntax "introduce " term                                : minitactic
syntax "apply " ident                                   : minitactic
syntax "exact " ident                                   : minitactic
syntax "split"                                          : minitactic
syntax "left"                                           : minitactic
syntax "right"                                          : minitactic
syntax "cases " ident                                   : minitactic
syntax "done"                                           : minitactic

syntax "begin_min " (minitactic)*  : tactic


elab_rules : tactic
  | `(tactic| begin_min $[$tacs:minitactic]*) => do
      let mut tacList : Array (TSyntax `tactic) := #[]
      for tacNode in tacs do
        let newTac : TSyntax `tactic ← match tacNode with
          | `(minitactic| assume $h:ident : $ty) => `(tactic| have $h : $ty := sorry)
          | `(minitactic| introa $h:ident)       => `(tactic| intro a)
          | `(minitactic| introduce $h:term)       => `(tactic| intro $h:term)
          | `(minitactic| apply $h:ident)       => `(tactic| apply $h)
          | `(minitactic| exact $h:ident)       => `(tactic| exact $h)
          | `(minitactic| split)                => `(tactic| constructor)
          | `(minitactic| left)                 => `(tactic| apply Or.inl)
          | `(minitactic| right)                => `(tactic| apply Or.inr)
          -- | `(minitactic| cases $h:ident)       => `(tactic| cases $h)
          | `(minitactic| done)                 => `(tactic| assumption)
          | _ => throwError m!"Unsupported mini tactic: {tacNode}"
        tacList := tacList.push newTac
        withTacticInfoContext tacNode do
          evalTactic newTac

example (P Q : Prop) : [Logic| P → (Q → P)] := by
  begin_min
    introduce p
    introduce q