Zulip Chat Archive

Stream: general

Topic: tauto weaker than expected


Neil Strickland (Mar 20 2019 at 13:19):

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 (Mar 20 2019 at 13:25):

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

Kevin Buzzard (Mar 20 2019 at 13:29):

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 (Mar 20 2019 at 13:30):

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

Jesse Michael Han (Mar 20 2019 at 17:58):

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 (Mar 20 2019 at 18:00):

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

Johan Commelin (Mar 20 2019 at 18:04):

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

Patrick Massot (Mar 20 2019 at 18:05):

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

Patrick Massot (Mar 20 2019 at 18:05):

This is what Bertha means in France

Johan Commelin (Mar 20 2019 at 18:05):

Aaah, didn't know that one...

Kevin Buzzard (Mar 20 2019 at 18:17):

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

Simon Hudon (Mar 20 2019 at 18:33):

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

Kevin Buzzard (Mar 20 2019 at 19:33):

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 (Mar 20 2019 at 19:36):

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 (Mar 20 2019 at 19:40):

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 (Mar 20 2019 at 19:58):

is it fast?

Jesse Michael Han (Mar 20 2019 at 20:05):

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

Kevin Buzzard (Mar 20 2019 at 20:09):

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

Simon Hudon (Mar 20 2019 at 22:29):

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 (Mar 20 2019 at 22:34):

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 (Apr 24 2019 at 12:01):

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 (Apr 24 2019 at 12:06):

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

Joseph Corneli (Apr 24 2019 at 13:02):

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 (Apr 24 2019 at 13:09):

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

Simon Hudon (Apr 24 2019 at 13:16):

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

Joseph Corneli (Apr 24 2019 at 13:27):

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

Last updated: Dec 20 2023 at 11:08 UTC