Builder tactics [draft]

[icecream17]

Draft: I wrote a lot of text, but based on the closed issues I should probably compile the program first and try to make proofs, since the process will lead to a better understanding of rumm. I already see it uses a specific commit of metamath-knife, which might affect $j commands in some way I don't appreciate. I'm saving the issue for now

Currently, this might be somewhat outlandish, but I would like to share some ideas for tactics:

equality: equality builders

Somewhat similar to the find tactics. (I'm confused on why all tactics are referred to in their plural)

The $j command $j equality marks = and <-> as "equality symbols", these symbols will be denoted equiv

For statements of the form &1 equiv &2 and ( antecedent -> &1 equiv &2 ), it is often the case where you want to remove shared symbols in &1 and &2, which will now be called ph(&3) and ph(&4). This tactic attempts to find a theorem that reduces this to some smaller &3 and &4.

Cases like mpteq2dva vs mpteq2dv can be added later. It would obviously be easier to only find mpteq2dv for now. I think it is better in the long run if equality just does one syntax reduction, instead of as much as possible. Maybe in the future an option n can be provided to reduce (up to) n times. This way, if some live feedback is ever made, the number can simply be edited 1, 2, etc., which is very convenient.

This might require a new $j command "implication" to identify the antecedent and consequent of an implication, in order to keep database-independence

nf: "not free" builders i.e. does not depend on

Similar to equality. Tries to reduce F/ ph(&1) to some F/ &1, or F/_ A(&1) to some F/_ &1

Again, the $j commands (see link above) seem really useful. I know that the latest metamath-knife processes at least a few $j-commands

cbv: Change bound variable

Given a class A, replacing all x with y results in class B. This tactic tries to show A = B (or A. x ph <-> A. y ps?) by trying to prove x = y -> ph <-> ps using equality, and then using a theorem like cbvmpt.

Note: I have no idea how cbvmpt-like theorems would be found, so this is theoretical

Comments

Based on #9 it sounds like there is potential for quality-of-life improvements.

[tirix]

Yes nf and cbv are totally valid and interesting tactics ideas (it seems plural is the normal form for this word)!

For using the $j commands, yes, one could imagine a built-in equality tactics which uses those. I'm thinking later including more kinds of tactics, like SAT prover, Arithmetic prover, etc.