Thanks for the PR <https://github.com/GinoGiotto/mm1_tactics/pull/1>. The tactic is now at least 6x faster than my original implementation, and I can definitely feel the difference on the VS Code LSP server side.
> If you leave off either mmb or mmu you get just the cost of compiling the file and running the tactics without any export, so that is going to reflect more of your code. This answers my question. Therefore, I will use "mm0-rs compile tauto.mm1" to extrapolate the time that the tactics spend for computing proofs. This will be useful for upcoming attempts. > MM0 generally produces better (shorter) proofs if you don't use its conversion facility. You also won't be able to translate these proofs easily to metamath; it's more straightforward if you only use unfolding in helper lemmas and have straight theorem applications in tactic-generated proofs. Looking at your code, I noticed that tauto_nhad is introduced as a standalone lemma even if its proof is just idi + unfolding. So, it seems that one should delegate definitional unfolding to already proved theorems as much as possible, even when refine could figure it out on its own. I was wondering initially what was the better performance trade-off between using conversion proofs and attempting more match clauses. > You can use MM1 to automatically generate conversion proofs if you just assert the type inside `refine`, like so: This would have been quite useful for my original implementation, since it took me a while to understand the syntax of conversion proofs. I initially looked at peano.mm1 as reference, but :conv appears only twice there and the unfolding seemed to be obscure. I ended up finding an explicit example by accident in an MMU file in the examples. > You have several occurrences of e.g. "(fn (refine t) (conclusion refine t))", this can be reduced to just "conclusion". You're right. I initially thought that binding a new refine was required to make the next tactic capture the goal at the current location, but the placement of the tactic inside the proof already gives that information, so calling it directly is enough. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/54fde17b-6164-4a55-b331-26f9ccc38308n%40googlegroups.com.
