tauto is a decision procedure?

Stream: general

[Alexandre Rademaker]

In Coq, the tauto tactic implements a decision procedure, https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html. What about the tauto of Lean? The https://leanprover-community.github.io/mathlib_docs/tactics.html#tautology is not clear. I was not able to prove some theorems of http://www.iltp.de/ using auto as expected if tauto is a decision procedure.

[Eric Rodriguez]

dec_trivial may be more like what Coq's tauto does

[Alexandre Rademaker]

It doesn't solve:

namespace t1

variables p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 f : Prop

variable h :
  (( p1 ∧ ( p2 ∧ ( p3 ∧ ( p4 ∧ ( p5 ∧ ( p6 ∧ ( p7 ∧ ( p8 ∧ ( p9 ∧ ( p10 ∧ p11 )))))))))) ∨
  (( ¬(¬(p1)) → f)  ∨ (( p2 → f)  ∨ (( p3 → f) ∨ (( p4 → f) ∨ (( p5 → f) ∨ (( p6 → f) ∨
  (( p7 → f)  ∨ (( p8 → f)  ∨ (( p9 → f) ∨ (( p10 → f) ∨ (p11 → f)))))))))))) → f

include p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 f h

example : f :=
begin
 apply h, clear h,
 tauto,
end

end t1

If I replace variables with constants, it still doesn't solve:

namespace t1

constants p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 f : Prop

axiom h :
  (( p1 ∧ ( p2 ∧ ( p3 ∧ ( p4 ∧ ( p5 ∧ ( p6 ∧ ( p7 ∧ ( p8 ∧ ( p9 ∧ ( p10 ∧ p11 )))))))))) ∨
  (( ¬(¬(p1)) → f)  ∨ (( p2 → f)  ∨ (( p3 → f) ∨ (( p4 → f) ∨ (( p5 → f) ∨ (( p6 → f) ∨
  (( p7 → f)  ∨ (( p8 → f)  ∨ (( p9 → f) ∨ (( p10 → f) ∨ (p11 → f)))))))))))) → f

example : f :=
begin
 apply h,
 tauto,
end

end t1

[Alexandre Rademaker]

But tauto solves if I introduce the propositions as variables and h as axiom:

namespace t1

variables p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 f : Prop

axiom h :
  (( p1 ∧ ( p2 ∧ ( p3 ∧ ( p4 ∧ ( p5 ∧ ( p6 ∧ ( p7 ∧ ( p8 ∧ ( p9 ∧ ( p10 ∧ p11 )))))))))) ∨
  (( ¬(¬(p1)) → f)  ∨ (( p2 → f)  ∨ (( p3 → f) ∨ (( p4 → f) ∨ (( p5 → f) ∨ (( p6 → f) ∨
  (( p7 → f)  ∨ (( p8 → f)  ∨ (( p9 → f) ∨ (( p10 → f) ∨ (p11 → f)))))))))))) → f

example : f :=
begin
 apply h,
 tauto,
end

end t1

[Alexandre Rademaker]

dec_trivial does not solve the last one.

[Alexandre Rademaker]

Only finish solves when the propositions and h are passed as arguments:

example (p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 f : Prop)
        (h : (( p1 ∧ ( p2 ∧ ( p3 ∧ ( p4 ∧ ( p5 ∧ ( p6 ∧ ( p7 ∧ ( p8 ∧ ( p9 ∧ ( p10 ∧ p11 )))))))))) ∨
             (( ¬(¬(p1)) → f)  ∨ (( p2 → f)  ∨ (( p3 → f) ∨ (( p4 → f) ∨ (( p5 → f) ∨ (( p6 → f) ∨
             (( p7 → f)  ∨ (( p8 → f)  ∨ (( p9 → f) ∨ (( p10 → f) ∨ (p11 → f)))))))))))) → f) : f :=
begin
  apply h,
  finish,
end

[Mario Carneiro]

tauto is not a decision procedure, although I think it should be

[Greg Price]

The docstring of finish says:

finish is complete for propositional logic.

So that may be the decision procedure you're looking for.

[Greg Price]

Here's a shortened version of the same example:

example (p1 p2 f : Prop) : (p1 ∧ p2) ∨ (¬¬p1 → f) ∨ (p2 → f) :=
by finish

example (p1 p2 f : Prop) : (p1 ∧ p2) ∨ (¬¬p1 → f) ∨ (p2 → f) :=
by tauto -- fails

[Alexandre Rademaker]

finish uses by_contradiction. This is an Intuitionistic theorem.

[Mario Carneiro]

tauto is not a complete intuitionistic logic prover

[Mario Carneiro]

ifinish claimed to be but wasn't so it was removed

[Alexandre Rademaker]

thanks, Mario, so I assume there is a motivation for having such a decision procedure available, right?

[Mario Carneiro]

Yes, but someone has to write it

[Mario Carneiro]

But very few people around here care about intuitionistic logic so it's not a high priority

[Rob Lewis]

tauto is neither a decision procedure nor intuitionistic. I've been distracted by real life, but before that I was planning to propose removing tauto and replacing it with tauto!, which I think is complete for classical logic.

import tactic

example (p : Prop) : p ∨ ¬ p := by tauto

[Rob Lewis]

Alternatively, someone could fix whatever is leaking classical logic into tauto, but that will take someone who cares!

[Mario Carneiro]

Say hello to itauto: #7057

[Mario Carneiro]

theorem T (p : Prop) : ¬ (p ↔ ¬ p) := by itauto
#print T
-- theorem T : ∀ (p : Prop), ¬(p ↔ ¬p) :=
-- λ (p : Prop) (h0 : p ↔ ¬p), h0.mp (h0.mpr (λ (h1 : p), h0.mp h1 h1)) (h0.mpr (λ (h1 : p), h0.mp h1 h1))

[Kevin Buzzard]

Can you prove that it never uses classical axioms?

[Mario Carneiro]

Yeah, that's not too hard. It only uses exfalso (the tactic, although it could just be apply false.rec), triv (the tactic, but this one really is just apply trivial), intro, and.left/right/intro,or.inl/inr/elim, iff.mp/mpr/intro, and application (modus ponens)

[Mario Carneiro]

So I think it is actually a "no axioms" prover

[Mario Carneiro]

I was thinking about adding support for p = q by treating it like p <-> q, but this will require using propext sometimes

[Alexandre Rademaker]

Hi Mario, in http://www.iltp.de/formulae.html, one of the problems is

%--------------------------------------------------------------------------
% File     : SYJ203+1.006 : ILTP v1.1.2
% Domain   : Intuitionistic Syntactic
% Problem  : Formulae requiring many contractions
% Version  : Especial.
%            Problem formulation : Intuit. Valid  Size 6
% English  : (((&&_{i=1..N} p(i)) | (||_{i=1..N} (p(i)=>f)))=>f)=>f

% Refs     : [Dyc97] Roy Dyckhoff. Some benchmark formulas for
%                    intuitionistic propositional logic. At
%                    http://www.dcs.st-and.ac.uk/~rd/logic/marks.html
%          : [Fr88]  T. Franzen, Algorithmic Aspects of intuitionistic
%                    propositional logic, SICS Research Report R87010B,
%                    1988.
%          : [Fr89]  T. Franzen, Algorithmic Aspects of intuitionistic
%                    propositional logic II, SICS Research Report
%                    R-89/89006, 1989.
% Source   : [Dyc97]
% Names    : con_p6 : Dyckhoff's benchmark formulas (1997)
%
% Status (intuit.) : Theorem
% Rating (intuit.) : 0.00 v1.0.0
%

% Comments : "proof in LJ needs n contractions" [Dyc97]
%--------------------------------------------------------------------------
fof(axiom1,axiom,(
( ( ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & p6 ) ) ) ) ) | ( ( p1 => f)  | ( ( p2 => f)  | ( ( p3 => f)  | ( ( p4 => f)  | ( ( p5 => f)  | ( p6 => f)  ) ) ) ) ) ) => f) )).

fof(con,conjecture,(
f
)).

%--------------------------------------------------------------------------

Converted to Lean the new itauto proved it:

import tactic

theorem SYJ203_1_006 (f p1 p2 p3 p4 p5 p6 : Prop) :
  ((((p1 ∧ (p2 ∧ (p3 ∧ (p4 ∧ (p5 ∧ p6))))) ∨
   ((p1 → f) ∨ ((p2 → f) ∨ ((p3 → f) ∨ ((p4 → f) ∨ ((p5 → f) ∨ (p6 → f))))))) → f)) → (f) :=
begin
 itauto,
end

In https://github.com/leanprover-community/mathlib/pull/7057 I asked how to use your code but it seems that I made a workaround. I manually modified the src/tactic/basic.lean and added the src/tactic/itauto.lean. I don't know yet how to compile the files to produce the olean files for them. But restarting the lean process, I was able to prove the theorem above.

But I am getting warnings in the import tactic. See image.png