Proof extraction

Stream: lean4

[Henrik Böving]

I'm writing my semantic tableaux prover and it can now prove propositional logic statements so I decided to try and write a tactic that extracts its proof back into Lean for type checking. I decided to go with a set based tableaux for now since that seemed the easiest and also more performant in comparision to just always looking up the tableau tree for a contradiction again in every step (but maybe someone who knows more about this than me might be able to correct me on that). Furthermore at every node the prover records which term it eliminated with which rule (the rules right now are just basic cases on And and Or as well as double negation and de morgan laws for And and Or) and when closing a node it also records which terms it used to derive the contradiction.

Now since all of this is set based and my hypothesis don't really have names so I can just lookup the negation of a statement in the set to see whether I derived a contradiction, the easiest way to reconstruct the proof into Lean for me seems to just write out a tactic program that walks through the tableau, checks which rule with which parameter was applied, search for some term of that type in the local context, apply the rule to that type and continue recursively.

The only thing I'm worried about with this approach would be performance in bigger use cases since I would be looking through the local context lots of times there for every branch, step etc. Which would probably be much worse than if I constructed an Expr statically and gave it to Lean for type checking.

So my question would be, is this a valid performance concern? If it is, what do you think would be the best way to handle this in set based tableau? The only one I can see would be to implement some sort of local context myself or just let go of set based all together and instead work purely tree based.