I made a MM1 tactic for finding proofs in classical propositional logic. The tactic is located in this repository <https://github.com/GinoGiotto/mm1_tactics>. It supports all main symbols used in set.mm, specifically: ->, -., /\ , \/, <->, -/\, -\/, \/_, T., F., if-, hadd, cadd (the symbols are slighly different in MM0, I made an explanatory table here <https://github.com/GinoGiotto/mm1_tactics/blob/main/tauto/README.md>). I took the name "tauto" from Lean tauto tactic <https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Tauto.html> that serves a similar purpose.
The goal statements can be of any shape or form you like, as long as they are provable. The only limitation is that it does not support rules of inference, so only statements in closed form can be proved (for now). It is required to use the latest MM0 version (commit 6d5f0d4 <https://github.com/digama0/mm0/tree/6d5f0d4fae8e2e3ae0b998bcbaa9d059cad99fad>) from the github repo. The MM0 extension on the marketplace won't work because the tauto tactic heavily depends on this issue <https://github.com/digama0/mm0/issues/174> being solved. To prove a theorem, you simply write "tauto" as its proof, examples: theorem id (ph: wff): $ ph -> ph $= tauto; theorem simplll (ph ps ch th: wff): $ ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph ) $= tauto; theorem trujust {x y: set}: $ ( ( A. x x =s x -> A. x x =s x ) <-> ( A. y y =s y -> A. y y =s y ) ) $= tauto; theorem falnantru: $ ( ( F. -/\ T. ) <-> T. ) $= tauto; theorem ifpfal (ph ps ch: wff): $ ( ~ ph -> ( ifp ph ps ch <-> ch ) ) $= tauto; theorem cadnot (ph ps ch: wff): $ ( ~ cad ph ps ch <-> cad (~ph) (~ps) (~ch) ) $= tauto; You can also attempt wild statements like: theorem _ (ph ps ch: wff): $ ~((~~((~~((ph -> ps) -> ~(ps -> ph)) -> ch) -> ~(ch -> ~~((ph -> ps) -> ~(ps -> ph)))) -> ~~(ph -> ~~((ps -> ch) -> ~(ch -> ps))) -> ~(~ph -> ~~~((ps -> ch) -> ~( ch -> ps)))) -> ~((~~(ph -> ~~((ps -> ch) -> ~(ch -> ps))) -> ~(~ph -> ~~~((ps -> ch) -> ~(ch -> ps)))) -> ~~((~~((ph -> ps) -> ~(ps -> ph)) -> ch) -> ~(ch -> ~~((ph -> ps) -> ~(ps -> ph)))))) $= tauto; To view the generated proofs, you can use the tactic below (borrowed from peano.mm1 <https://github.com/digama0/mm0/blob/master/examples/peano.mm1>). A tooltip will display the proof when hovering over the code. do { (def (get-proof x) (nth 1 @ @ nth 6 @ get-decl x)) (display @ pp @ get-proof 'pm2_48) }; In the example above, the generated proof of pm2_48 <https://us.metamath.org/mpeuni/pm2.48.html> is: (:conv (im (not (or ph ps)) (or ph (not ps))) (im (not (:unfold or (ph ps) (im (not ph) ps))) (:unfold or (ph (not ps)) (im (not ph) (not ps)))) (impneg (~ph) ps (~ph -> ~ps) (expn (~ph) ps (~ph -> ~ps) (expn (~(~ph -> ps)) ph (~ps) (impneg (~(~ph -> ps)) ph (~ps) (impneg (~ph) ps (~ph -> ~ps) (com23 (~ph) (~ph) (~ps) (~ps) (expi (~ph) (~ph) (~ps -> ~ps) (idd (~(~ph -> ~~ph)) (~ps)))))))))) The tactic is designed for generality rather than for producing short proofs. Most generated proofs will be longer than their set.mm counterparts. I tested the tactic against 786 theorems of set.mm (all theorems in closed form preceding the predicate logic section). The tactic successully found a proof for all of them. To check that the tactic was indeed successful, you can verify the proofs with the following commands (if mm0-c prints nothing then it means the databases have no errors): ./mm0-rs compile -W tauto.mm1 tauto.mmb ./mm0-c tauto.mmb < tauto.mm0 It's interesting to compare the MM1 tauto tactic with the Rumm tactics <https://groups.google.com/g/metamath/c/Dlc-Lf7MF1A> I wrote a year ago. The latter ones were tested against 112 theorems and solver1.rmm took about 2 seconds to compute all combined proofs while solver2.rmm took about 4 seconds. Note that the Rumm tactics only support primitive symbols, so every statement has to be written using implication "->" and negation "-." only. The general algorithm that I used in MM1 is roughly the same as the Rumm one. The tactic splits the main goal into statements in implicational normal form and then proves them. One of the main reasons I wanted to try out MM1 is that it supports work variables (see this issue <https://github.com/tirix/rumm/issues/12>), but I was also curious to see whether MM1 definitional unfolding makes the proof development easier (the only unfortunate aspect of MM1 is that it does not have a translator to MM, see this discussion <https://groups.google.com/g/metamath/c/T4oS4cQsz9I>). I'm not sure how to measure the time MM1 needs to generate proofs. One approach that I found reasonable is to run "mm0-rs compile tauto.mm1 tauto.mmu", which produces an MMU file containing all the generated proof objects from a MM1 file in a readable format. This command completes in about 2-3 seconds on my machine, so maybe I can claim that my tauto tactic proved all those 786 theorems in that amount of time. It would also be interesting to compare it to Lean's tauto tactic. I don’t know much about Lean at the moment, so I’m putting this forward as a question to people with more experience: how quickly would Lean’s tauto prove those 786 theorems from set.mm? What are its limitations? (I guess the Lean version is likely to be a lot more efficient than mine, given that it has a very active community of hundreds if not thousands of people constantly updating and optimizing the mathlib4 database). Perhaps, one idea to make the MM1 tauto faster would be to avoid doing definition unfolding explicitely. Normally, the MM1 refine tactic is able to unfold definitions on its own. The issue is that the match tactic does not unfold a goal when matched against a pattern, which is the main reason why I had to write the unfolding myself. Such feature could look like this: (match $ ,x /\ ,y $ [ $ ~(,x -> ~,y) $ #f] [ (unfold $ ~(,x -> ~,y) $) #t]) Where the above match returns #t rather than a matching failure. The MM1 tauto tactic can also be used as a SAT solver. To determine the satisfiability of a statement, it is sufficient to ask tauto to prove the negation of that statement. If it finds a proof, the original statement is unsatisfiable, if it does not find a proof then it is satisfiable. When tested against an unprovable statement, tauto should return the error "Statement not provable". If it returns an overflow error then it means I missed something (indeed, the "Statement not provable" error was put to avoid overflow). Due to MM0 approach to definitions, some theorems beyond propositional logic can be proved with tauto more easily, example: We first introduce class terms and define class equality (as done in the set.mm0 <https://github.com/digama0/mm0/blob/master/examples/set.mm0> file of the MM0 repo): strict sort class; term welc (a: set) (A: class): wff; infixl welc: $ec.$ prec 50; def wceq {.x: set} (A B: class): wff = $ A. x (x ec. A <-> x ec. B) $; infixl wceq: $=$ prec 50; And then we can prove some theorems of class equality with the help of tauto: theorem eqcid (A: class): $ A = A $= '(!! ax_gen x ,tauto); theorem eqscom (A B: class): $ A = B -> B = A $ = '(!! alimi x ,tauto); theorem eqscomb (A B: class): $ A = B <-> B = A $ = '(!! albii x ,tauto); theorem eqstr (A B C: class): $ A = B -> B = C -> A = C $ = '(!! al2imi x , tauto); theorem eqstr2 (A B C: class): $ A = B -> B = C -> C = A $ = '(!! al2imi x , tauto); theorem eqstr3 (A B C: class): $ B = A -> B = C -> A = C $ = '(!! al2imi x , tauto); theorem eqstr4 (A B C: class): $ A = B -> C = B -> A = C $ = '(!! al2imi x , tauto); In set.mm, those theorems would require all axioms up to ax-ext, while here they only require axioms up to ax-4. This is a very basic example of how one could use the tauto tactic for later developments. -- 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/73fef060-9fcc-4724-b5f7-2ac3f3460e72n%40googlegroups.com.
