Home
September 29, 2025

How ProofSouq Transpiles a Proof of the Associativity of Addition

In this post, I’ll take a very simple Rocq proof of the associativity of addition and explain how ProofSouq.com transpiles it to Lean.

Rocq Input

This earth-shattering revelation proves that addition is associative, i.e., (a + b) + c = a + (b + c):

Require Import Stdlib.Init.Nat.
Require Import Stdlib.Arith.Arith.

Check plus_n_O.
Check plus_n_Sm.

Theorem my_add_assoc (a b c : nat) : a + b + c = a + (b + c).
Proof.
  induction c as [ | c' IHc ].
  - rewrite <- plus_n_O.
    rewrite <- plus_n_O.
    reflexivity.
  - rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite IHc.
    reflexivity.
Qed.

Check my_add_assoc.
Print my_add_assoc.

Compiling to IR

ProofSouq’s compiler for Rocq parses the above proof and compiles it to the following intermediate representation (IR):

IrRoot
|-@commands
| |-[0]:CheckCommand
| | |-@term : AutogenSymmEqualPropIdentifier
| | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_0_equals_n
| |-[1]:CheckCommand
| | |-@term : AutogenSymmEqualPropIdentifier
| | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| |-[2]:TheoremCommand
| | |-@name : NewDefinitionIdentifier @text=my_add_assoc
| | |-@parameters
| | | |-[0]:ProofParameterIdentifier @text=a @type=Nat
| | | |-[1]:ProofParameterIdentifier @text=b @type=Nat
| | | |-[2]:ProofParameterIdentifier @text=c @type=Nat
| | |-@proposition : BinaryArithmeticExpression @op=Add
| | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | |-@rhs : BinaryEqualityExpression
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | |-@rhs : ParenthesizedExpression
| | | | |-@expression : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat
| | |-@steps : ProofStepList
| | | |-@steps
| | | | |-[0]:InductionBranchlessProofStep
| | | | | |-@term : InductiveTermIdentifier @text=c @type=Nat
| | | | | |-@patterns
| | | | | | |-[0]:InductionPattern @constructorName=(empty)
| | | | | | | |-@constructorArgNames @inductiveHypothesis=(empty)
| | | | | | |-[1]:InductionPattern @constructorName=(empty)
| | | | | | | |-@constructorArgNames
| | | | | | | | |-[0]:InductiveConstructorParameterIdentifier
| | | | | | | | | |-@text : IdentifierText @rawText=c'
| | | | | | | |-@inductiveHypothesis : InductiveHypothesisIdentifier @text=IHc
| | | | |-[1]:ProofBullet (singleton)
| | | | |-[2]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_0_equals_n
| | | | |-[3]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_0_equals_n
| | | | |-[4]:ReflexivityProofStep (singleton)
| | | | |-[5]:ProofBullet (singleton)
| | | | |-[6]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| | | | |-[7]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| | | | |-[8]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| | | | |-[9]:RewriteProofStep @direction=LeftToRight
| | | | | |-@equalityProposition : InductiveHypothesisIdentifier @text=IHc
| | | | |-[10]:ReflexivityProofStep (singleton)
| |-[3]:CheckCommand
| | |-@term : NewDefinitionIdentifier @text=my_add_assoc
| |-[4]:PrintCommand
| | |-@term : ExpressionIdentifier
| | | |-@identifier : NewDefinitionIdentifier @text=my_add_assoc

I’ll break the above IR tree down by section and note some salient points:

Check commands

The commands Check plus_n_O and Check plus_n_Sm compile to:

| |-[0]:CheckCommand
| | |-@term : AutogenSymmEqualPropIdentifier
| | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_0_equals_n
| |-[1]:CheckCommand
| | |-@term : AutogenSymmEqualPropIdentifier
| | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen

Why the application of symmetric equality here? Looking at the @text attributes of the CoreEqualityPropositionIdentifiers, ProofSouq’s core IR states that:

  • n_plus_0_equals_n represents n + 0 = n
  • n_plus_S_m_equal_S_lparen_n_plus_m_rparen represents n + (m + 1) = (n + m) + 1

These equalities are commutative; rather than maintaining two variants for each direction of a core equality proposition, ProofSouq chooses one canonical direction in its IR and requires sources to compile to that direction. The upshot: if a source language chooses a direction other than the one defined in IR, that fact must be preserved by the compiler so that transformers and emitters are aware of it. Indeed, looking at Rocq’s standard library, we see:

  • Lemma plus_n_O : forall n:nat, n = n + 0. (docref)
  • Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. (docref)

These are both commuted from the corresponding definitions in ProofSouq’s IR. The Rocq compiler therefore selects the appropriate IR definition, but wraps each in an AutogenSymmEqualPropIdentifier, representing the fact that the source included a reference to the symmetric (commuted) version of the core IR definition.

TheoremCommand

The @name, @parameters, and @proposition of the TheoremCommand are all rather straightforward:

| |-[2]:TheoremCommand
| | |-@name : NewDefinitionIdentifier @text=my_add_assoc
| | |-@parameters
| | | |-[0]:ProofParameterIdentifier @text=a @type=Nat
| | | |-[1]:ProofParameterIdentifier @text=b @type=Nat
| | | |-[2]:ProofParameterIdentifier @text=c @type=Nat
| | |-@proposition : BinaryArithmeticExpression @op=Add
| | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | |-@rhs : BinaryEqualityExpression
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | |-@rhs : ParenthesizedExpression
| | | | |-@expression : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat

We have a Nat type in IR representing the natural numbers, to which Rocq’s nat type is compiled.

ProofStepList

The @steps of the TheoremCommand are more interesting:

| | |-@steps : ProofStepList
| | | |-@steps
| | | | |-[0]:InductionBranchlessProofStep
| | | | | |-@term : InductiveTermIdentifier @text=c @type=Nat
| | | | | |-@patterns
| | | | | | |-[0]:InductionPattern @constructorName=(empty)
| | | | | | | |-@constructorArgNames @inductiveHypothesis=(empty)
| | | | | | |-[1]:InductionPattern @constructorName=(empty)
| | | | | | | |-@constructorArgNames
| | | | | | | | |-[0]:InductiveConstructorParameterIdentifier
| | | | | | | | | |-@text : IdentifierText @rawText=c'
| | | | | | | |-@inductiveHypothesis : InductiveHypothesisIdentifier @text=IHc
| | | | |-[1]:ProofBullet (singleton)
| | | | |-[2]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_0_equals_n
| | | | |-[3]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_0_equals_n
| | | | |-[4]:ReflexivityProofStep (singleton)
| | | | |-[5]:ProofBullet (singleton)
| | | | |-[6]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| | | | |-[7]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| | | | |-[8]:RewriteProofStep @direction=RightToLeft
| | | | | |-@equalityProposition : AutogenSymmEqualPropIdentifier
| | | | | | |-@coreEqualityPropIdent : CoreEqualityPropositionIdentifier @text=n_plus_S_m_equal_S_lparen_n_plus_m_rparen
| | | | |-[9]:RewriteProofStep @direction=LeftToRight
| | | | | |-@equalityProposition : InductiveHypothesisIdentifier @text=IHc
| | | | |-[10]:ReflexivityProofStep (singleton)

Two big things stick out here:

  • Rocq’s induction tactic is branch-less, in the sense that the branch patterns are defined up-front, with the proof steps themselves following separately. To be specific: [ | c' IHc ] defines the branch patterns, where | separates the empty pattern for 0 from the pattern for Nat’s only other constructor n + 1. Proof bullets in Rocq are purely visual elements, they aren’t actually part of the induction tactic. This contrasts with Lean’s induction tactic, which groups steps with their corresponding pattern. A transformer will thus be needed to realize the prerequisites needed to emit Lean’s version, which is why we keep the ProofBullets around in IR rather than lexing them out in the Rocq compiler.
  • We have a bunch of rewrites using the symmetric (commuted) versions of core equality propositions. In both Rocq and Lean, it’s possible to rewrite a goal using either side of an equality proposition by specifying the desired side/direction; we’ll take advantage of this fact in a transformer to clean this IR up and avoid needing to emit symmetric versions of the core equality propositions referenced here.

Transforming the IR

Here’s the IR tree after the ProofSouq transformer suite has run:

IrRoot
|-@commands
| |-[0]:CheckCommand
| | |-@term : CoreEqualityPropositionIdentifier @text=Nat.add_zero
| |-[1]:CheckCommand
| | |-@term : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| |-[2]:TheoremCommand
| | |-@name : NewDefinitionIdentifier @text=my_add_assoc
| | |-@parameters
| | | |-[0]:ProofParameterIdentifier @text=a @type=Nat
| | | |-[1]:ProofParameterIdentifier @text=b @type=Nat
| | | |-[2]:ProofParameterIdentifier @text=c @type=Nat
| | |-@proposition : BinaryArithmeticExpression @op=Add
| | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | |-@rhs : BinaryEqualityExpression
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | |-@rhs : ParenthesizedExpression
| | | | |-@expression : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat
| | |-@steps : ProofStepList
| | | |-@steps
| | | | |-[0]:InductionBranchedProofStep
| | | | | |-@term : InductiveTermIdentifier @text=c @type=Nat
| | | | | |-@branches
| | | | | | |-[0]:InductionBranch
| | | | | | | |-@pattern : InductionPattern
| | | | | | | | |-@constructorName : InductiveConstructorIdentifier
| | | | | | | | | |-@text : IdentifierText @rawText=zero
| | | | | | | | |-@constructorArgNames @inductiveHypothesis=(empty)
| | | | | | | |-@steps : ProofStepList
| | | | | | | | |-@steps
| | | | | | | | | |-[0]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_zero
| | | | | | | | | |-[1]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_zero
| | | | | | | | | |-[2]:TryProofStep
| | | | | | | | | | |-@step : ReflexivityProofStep (singleton)
| | | | | | |-[1]:InductionBranch
| | | | | | | |-@pattern : InductionPattern
| | | | | | | | |-@constructorName : InductiveConstructorIdentifier
| | | | | | | | | |-@text : IdentifierText @rawText=succ
| | | | | | | | |-@constructorArgNames
| | | | | | | | | |-[0]:InductiveConstructorParameterIdentifier
| | | | | | | | | | |-@text : IdentifierText @rawText=c'
| | | | | | | | |-@inductiveHypothesis : InductiveHypothesisIdentifier @text=IHc
| | | | | | | |-@steps : ProofStepList
| | | | | | | | |-@steps
| | | | | | | | | |-[0]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| | | | | | | | | |-[1]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| | | | | | | | | |-[2]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| | | | | | | | | |-[3]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : InductiveHypothesisIdentifier @text=IHc
| | | | | | | | | |-[4]:TryProofStep
| | | | | | | | | | |-@step : ReflexivityProofStep (singleton)
| |-[3]:CheckCommand
| | |-@term : NewDefinitionIdentifier @text=my_add_assoc
| |-[4]:PrintCommand
| | |-@term : ExpressionIdentifier
| | | |-@identifier : NewDefinitionIdentifier @text=my_add_assoc

Transformed CheckCommands

A transformer has elided the symmetric application from around the core propositions referenced in the Rocq input, and another transformer has specialized those references to Lean’s:

| |-[0]:CheckCommand
| | |-@term : CoreEqualityPropositionIdentifier @text=Nat.add_zero
| |-[1]:CheckCommand
| | |-@term : CoreEqualityPropositionIdentifier @text=Nat.add_succ

Why were the symmetric applications elided? The argument is that these are just CheckCommands, which are purely informational, so there’s no harm in emitting their commuted versions in the target, i.e., whether LHS = RHS or RHS = LHS is printed to stdout makes no material difference. There’s another argument that says, “why not emit a local definition that commutes the core proposition, proves its validity by applying reflexivity, and then have the CheckCommand reference that local definition?” ProofSouq may take this approach in the future, but for now, and for simplicity, it takes the first approach.

Transformed TheoremCommand

Nothing changed in the TheoremCommand prelude:

| |-[2]:TheoremCommand
| | |-@name : NewDefinitionIdentifier @text=my_add_assoc
| | |-@parameters
| | | |-[0]:ProofParameterIdentifier @text=a @type=Nat
| | | |-[1]:ProofParameterIdentifier @text=b @type=Nat
| | | |-[2]:ProofParameterIdentifier @text=c @type=Nat
| | |-@proposition : BinaryArithmeticExpression @op=Add
| | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | |-@lhs : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | |-@rhs : BinaryEqualityExpression
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=a @type=Nat
| | | |-@rhs : ParenthesizedExpression
| | | | |-@expression : BinaryArithmeticExpression @op=Add
| | | | | |-@lhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=b @type=Nat
| | | | | |-@rhs : ExpressionIdentifier
| | | | | | |-@identifier : ProofParameterIdentifier @text=c @type=Nat

Transformed ProofStepList

On the other hand, much has changed in the ProofStepList:

| | |-@steps : ProofStepList
| | | |-@steps
| | | | |-[0]:InductionBranchedProofStep
| | | | | |-@term : InductiveTermIdentifier @text=c @type=Nat
| | | | | |-@branches
| | | | | | |-[0]:InductionBranch
| | | | | | | |-@pattern : InductionPattern
| | | | | | | | |-@constructorName : InductiveConstructorIdentifier
| | | | | | | | | |-@text : IdentifierText @rawText=zero
| | | | | | | | |-@constructorArgNames @inductiveHypothesis=(empty)
| | | | | | | |-@steps : ProofStepList
| | | | | | | | |-@steps
| | | | | | | | | |-[0]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_zero
| | | | | | | | | |-[1]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_zero
| | | | | | | | | |-[2]:TryProofStep
| | | | | | | | | | |-@step : ReflexivityProofStep (singleton)
| | | | | | |-[1]:InductionBranch
| | | | | | | |-@pattern : InductionPattern
| | | | | | | | |-@constructorName : InductiveConstructorIdentifier
| | | | | | | | | |-@text : IdentifierText @rawText=succ
| | | | | | | | |-@constructorArgNames
| | | | | | | | | |-[0]:InductiveConstructorParameterIdentifier
| | | | | | | | | | |-@text : IdentifierText @rawText=c'
| | | | | | | | |-@inductiveHypothesis : InductiveHypothesisIdentifier @text=IHc
| | | | | | | |-@steps : ProofStepList
| | | | | | | | |-@steps
| | | | | | | | | |-[0]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| | | | | | | | | |-[1]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| | | | | | | | | |-[2]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : CoreEqualityPropositionIdentifier @text=Nat.add_succ
| | | | | | | | | |-[3]:RewriteProofStep @direction=LeftToRight
| | | | | | | | | | |-@equalityProposition : InductiveHypothesisIdentifier @text=IHc
| | | | | | | | | |-[4]:TryProofStep
| | | | | | | | | | |-@step : ReflexivityProofStep (singleton)
  • The InductionBranchlessProofStep has been replaced by an InductionBranchedProofStep. All the steps that appeared after the former have been grouped into one of two branches of the latter. The transformer that did this used the ProofBullets from the Rocq source to infer the structure of these branches.
  • The RewriteProofSteps that previously applied a symmetric (commuted) version of a core equality proposition from @direction=RightToLeft now apply the core equality proposition directly from @direction=LeftToRight, simplifying the IR considerably. A transformer also specialized the names of the core equality propositions involved to the names used in Lean.
  • Easy to miss, but important to note, is the wrapping of the ReflexivityProofSteps in a TryProofStep. In Lean, unlike Rocq, definitional equality is automatically checked/applied in many places, eliminating the need to explicitly apply rfl. A transformer therefore runs to wrap these explicit uses in try to prevent them from failing in places where a goal has already been resolved using implicitly-applied reflexivity. Even better might be to just eliminate these uses entirely, which ProofSouq may eventually do in the future.

Emitting the IR

With the transformations applied, the IR is now ready to be emitted as Lean code:

#check Nat.add_zero
#check Nat.add_succ
theorem my_add_assoc (a : Nat) (b : Nat) (c : Nat) : a + b + c = a + (b + c) := by
  induction c with
    | zero =>
      rw [Nat.add_zero]
      rw [Nat.add_zero]
      try rfl
    | succ c' IHc =>
      rw [Nat.add_succ]
      rw [Nat.add_succ]
      rw [Nat.add_succ]
      rw [IHc]
      try rfl
#check my_add_assoc
#print my_add_assoc

No surprises here; all the heavy-lifting was performed by the transformers that ran previously, with the emitter simply applying Lean-specific syntax and symbol names.

Future Ideas

It might be preferable to simplify the chains of rw [<prop>] in the emitted Lean output to simp only [<prop>]. It’s a minor detail for a simple proof like this, but would be somewhat more beneficial in longer / more complex proofs.

A more interesting idea would be to make the goals/state of the prover available to certain transformations which would benefit from them. This would require actually executing tactics, and so would incur a performance cost, but this cost would be somewhat mitigated by the fact that we wouldn’t need to execute the entirety of a proof, just the ancestral parts leading up to the specific goal(s) we’re interested in.

A good example of where partial proof execution might be useful is in the transformer that coverts branchless induction to branched: if the Rocq input for this example hadn’t included the proof bullets, it would still have been valid, as again, these are merely visual aids in Rocq. But without them, the ProofSouq transformer wouldn’t have succeeded in deducing the structure of the branches, resulting in invalid Lean output from the emitter. If instead the transformer had the ability to request access to the prover state/goals, it could have done so as a last resort. The transformer could then have applied each step until the goal for the first induction case was resolved, at which point it would know the steps for the first branch, then repeat this process for all remaining branches.

In future posts, we’ll cover proofs of higher complexity to which these ideas may be applicable.

← return home