tracking reversible vs non-reversible tactics

Stream: new members

[Rado Kirov]

Say I have formulate some hypothesis and start working on a proof. After a number of tactics applied I reach to h: x and goal : \not x. This means the goal is not provable, but what do I know about the original hypothesis?

It seems to me that it depends on the transformations I did. If I only did rw, the hypothesis was false, but there other transformations that I could have done that led me to this state while the hypothesis was still correct. Some examples are apply or left/right.

Am I correct in this reasoning? Can Lean keep track of these for me automatically?

For a brief second I thought that's what the ! some tactics have is about, but now I don't know what ! means.

[Kyle Miller]

Rado Kirov said:

This means the goal is not provable

That's not necessarily the case, since there still might be a contradiction among the hypotheses. If you do intro h' then you'll get h h' : x and goal : False. If that's all you have as hypotheses, then sure, it's not provable, assuming x itself doesn't imply false.

[Kyle Miller]

! doesn't have a specific meaning. It depends on the tactic. I can't think of any tactics where the meaning has to do with reversibility.

[Rado Kirov]

That's not necessarily the case, since there still might be a contradiction among the hypotheses.

True, but that still means that either 1) at some point in my tactics I have introduced that or 2) it was present in the original hypotheses at the beginning of the proof. Certain tactics like rw, dsimp, unfold can be reversed so they cannot introduce a new contradiction thus if I only use those I know I am in case 2).

[Kyle Miller]

I used only rw here, does that mean that this goal is unprovable now?

def foo (p : Prop) := ¬ p

example {p : Prop} (h : p) (h' : ¬ p) : foo p := by
  rw [foo]
  /-
  p : Prop
  h : p
  h' : ¬p
  ⊢ ¬p
  -/

[Kyle Miller]

By the way, rw isn't necessarily reversible, since it allows conditional rewrites:

theorem weird_rfl {α : Sort _} (x : α) (h : False) : x = x := rfl

example : 5 = 5 := by
  rw [weird_rfl 5]
  -- ⊢ False

[Rado Kirov]

To your first point, that's a great example. I was wrong in saying This means the goal is not provable.

But I think my meta-statement can be corrected as - If you use only reversible tactics and reach a contradiction between proof state and goal it implies there was a contradiction in the original hypotheses and original goal.

You have shown that "contradiction between proof state and goal" doesn't equal "able to proof goal" (due to possible contradiction in hypotheses).

Your second point is more indeed damning, even rw can be non-reversible. Maybe there are so few reversible tactics for this to be useful.

[Robin Arnez]

Yeah, simp is the actual real reversible one

[Robin Arnez]

Or is it?

/--
error: unsolved goals
α✝ : Sort u_1
a b : α✝
h' : a ≠ b
h : True
⊢ False
-/
#guard_msgs in
example (h : a = b) (h' : a ≠ b) : False := by
  simp [h] at h

[Rado Kirov]

Maybe I should explain more on how this can be useful.

I am doing some exercises from https://github.com/teorth/analysis. I start with a theorem statement written by Tao and proceed towards a proof by applying tactics. Sometimes I arrive at an obvious contradiction between some proved prop and the goal (obvious meaning if the goal was an assumption contradiction will close any goal). What could have happened (from most to least likely):

1. I applied a tactic that took "a wrong turn" in the expected proof.

2. There was a typo in the original statement (less likely but it does happen). Technically it could of two flavors
   a) the contradiction was present (but not obvious, i.e. contradiction tactic won't solve it) in the original hypotheses and goal combined.

   b) the contradiction was present purely in the hypothesis, so all my tactics are suspect. This is even less likely than a) but technically possible.

Since 1) is much more likely than 2), what I do next is go over each line in my proof and look for tactics like apply, left/right, which can lead me to "take a wrong turn". Meanwhile, intro, simp, dsimp and rw are much less likely to lead me astray (although as you show above they could). If I can't find any suspicious tactics, I start looking for typos in the original statement.

This heuristic works alright for me so far, and I am wondering it could be "meta-formalized" and automated by Lean itself.

[Kyle Miller]

I'm sure someone could make something that tries to point out "wrong turns" with respect to a given point in a proof.

[Louis Cabarion]

@Rado Kirov I think such hints would be extremely helpful for newcomers, for whom the distinction between "(most likely) reversible" and "(most likely) non-reversible" tactic use is not obvious. I know they certainly would have helped me in the past.