tauto weaker than expected

Stream: general

[Neil Strickland]

I was surprised to find that tauto could not manage the following:

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
⟨λ h_p_to_pq hp,(h_p_to_pq.mp hp).right,
 λ h_p_to_q, ⟨λ hp,⟨hp,h_p_to_q hp⟩, λ hpq,hpq.left⟩⟩

Is there some straightforward rule about the kind of things that tauto can or cannot do?

[Kevin Buzzard]

cc, finish and simp can't do it either (unless I messed up)

[Kevin Buzzard]

import tactic.interactive

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
begin
  cases (classical.em p);
  cases (classical.em q),
  repeat {tauto},
  /- one goal lives on!
  p q : Prop,
  h : p,
  h_1 : ¬q
  ⊢ p ↔ p ∧ q ↔ p → q
  -/
  cc, -- does all of them
end

[Kevin Buzzard]

Once you split into cases, both cc and finish do everything.

[Jesse Michael Han]

It's situations like this for which I break out good ol' big_bertha:

-- uncomment in case of emergency
-- @[tidy] meta def big_bertha : tactic unit := `[finish]

viz.

@[tidy] meta def big_bertha : tactic unit := `[finish]

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
by tidy

[Simon Hudon]

Have you tried tauto!? With the exclamation mark, you allow tauto to use the excluded middle.

[Johan Commelin]

In the Netherlands "Bertha" is the universal name for a cow :cow: :grinning_face_with_smiling_eyes:

[Patrick Massot]

https://en.wikipedia.org/wiki/Big_Bertha_(howitzer)

[Patrick Massot]

This is what Bertha means in France

[Johan Commelin]

Aaah, didn't know that one...

[Kevin Buzzard]

Neil's proof doesn't seem to use classical logic

[Simon Hudon]

tauto is under-develop as far as constructive reasoning is concerned. Maybe I should remove the option

[Kevin Buzzard]

import tactic.tidy

@[tidy] meta def big_bertha : tactic unit := `[finish]

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
by tidy

#print axioms misc_tauto_a
-- all of them

I don't know if axioms are an issue for Neil.

[Simon Hudon]

I understand. What I'm saying is that the proof procedure is different if you don't have access to excluded middle. When you do have access to it, tauto applies it more than is necessary

[Jesse Michael Han]

finish invokes classical logic during its preprocessing step, but as Kevin observed, after enough splitting cc will close the goal (and tidy automates the splitting and intro-ing):

@[tidy]meta def not_as_big_bertha : tactic unit := `[cc]

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
by tidy

#print axioms misc_tauto_a
-- propext

[Simon Hudon]

is it fast?

[Jesse Michael Han]

tidy is pretty much always slow (in this case, according to the profiler, an order of magnitude slower than tauto!)

[Kevin Buzzard]

But in the future computers will be so fast that we won't notice the difference.

[Simon Hudon]

I don't know if you're being sincere but this is a pretty old refrain in computer science. The typical response to it is that software gets slow faster than hardware gets fast. Neglecting performances is not a great attitude

[Kevin Buzzard]

It sounds like I am simply being naive! This is perhaps not unexpected given my background. I was assuming you guys were tending to us -- our proofs run at infinite speed. A referee compiles them once, with quite a buggy and heuristic compiler, and then we have the bytecode forever in pdf form.

[Joseph Corneli]

Quick practical question:

(NB. I'm on Emacs)

If I write

lemma misc_tauto_a' (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
begin
 {! !}
end

and then run lean-hole with the cursor in the {! !} region,

lemma misc_tauto_a' (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
begin
 begin intros a end
end

However,

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
by tidy?

gives instead:

/- `tidy` says -/ fsplit, work_on_goal 0 { intros a a_1, cases a, simp at *, big_bertha }, intros a, fsplit, work_on_goal 0 { intros a_1, fsplit, work_on_goal 0 { assumption }, solve_by_elim }, intros a_1, cases a_1, assumption

Is this a known issue?

[Kevin Buzzard]

nice to see big bertha made it into your mathlib :-)

[Joseph Corneli]

Oops, how about this as a complete working example:

import tactic.tidy

@[tidy] meta def big_bertha : tactic unit := `[finish]

lemma misc_tauto_a (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
by tidy?

#print axioms misc_tauto_a

lemma misc_tauto_a' (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
begin
 {! !}
end

[Joseph Corneli]

I reproduced the same substitution on VS Code. Screen-Shot-2019-04-24-at-14.09.05.png

[Simon Hudon]

I don't think we can use Lean hole in tactic mode

[Joseph Corneli]

OK! Thanks!

lemma misc_tauto_a' (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
{! !}

... that comes up with the correct substitution, viz.,

lemma misc_tauto_a' (p q : Prop) : (p ↔ p ∧ q) ↔ (p → q) :=
begin fsplit, work_on_goal 0 { intros a a_1, cases a, simp at *, big_bertha }, intros a, fsplit, work_on_goal 0 { intros a_1, fsplit, work_on_goal 0 { assumption }, solve_by_elim }, intros a_1, cases a_1, assumption end