Remove hypothesis in absurd tactic

Stream: batteries

[Jakub Nowak]

I think absurd tactic should also try to remove the hypothesis it have been passed. This would be analogous to a very similar tactic contrapose! from mathlib. What other people think?

[Aaron Liu]

I don't see why this is helpful?

[Jakub Nowak]

And why is it helpful that contrapose doesn't leave original assumptions? I find it easier to write proofs by removing unneeded noise form the context.

[Jakub Nowak]

An example of absurd vs contrapose!.

import Mathlib.Tactic.Contrapose

variable (n m : Nat)

example (h₁ : n ≠ 1) : m ≠ 2 := by
  contrapose! h₁ with h₂

example (h₁ : n ≠ 1) : m ≠ 2 := by
  absurd h₁

contrapose! turns

h₁ : n ≠ 1
⊢ m ≠ 2

into

h₂ : m = 2
⊢ n = 1

absurd turns

h₁ : n ≠ 1
⊢ m ≠ 2

into

h₁ : n ≠ 1
⊢ n = 1

while I think it would be better to turn it into

⊢ n = 1

[Kyle Miller]

I think that makes sense, since it's like you've 'consumed' the fact. It's not so different from revert. In fact, absurd h could be implemented as exfalso; revert h, supposing h is a variable, for the first case mentioned in the docstring. (lean4#8522 would enable using revert for arbitrary terms; it's a draft PR since there haven't been strong use cases for it)

Looking at the absurd source code, the comment we can't use `( :)` here as that would make `·` behave weirdly. is now out of date, and (... :) is ok in this context.

There was another discussion about absurd not too long ago. It would be nice if absurd could take two arguments. #general > ✔ Application-like list of terms in a macro @ 💬

[Jakub Nowak]

Indeed, absurd is just like exfalso; revert h, but it also deals with double negation.

Kyle Miller said:

Looking at the absurd source code, the comment we can't use `( :)` here as that would make `·` behave weirdly. is now out of date, and (... :) is ok in this context.

I don't know what ( :) means?

[Kyle Miller]

Here's a version using a comma for the two-argument version, to maintain backwards compatibility:

-- (high priority for testing, to override current batteries version)
syntax (priority := high) "absurd " term (", " term)? : tactic

macro_rules
  | `(tactic| absurd $t1:ident) =>
    `(tactic| refine absurd $t1 ?_; (try apply not_not.mpr); (try clear $t1))
  | `(tactic| absurd $t1) =>
    `(tactic| have := $t1; absurd this)
  | `(tactic| absurd $t1, $t2) =>
    `(tactic| first | exact absurd $t1 $t2 | exact absurd $t2 $t1)

example (n m : Nat) (h₁ : n ≠ 1) : m ≠ 2 := by
  absurd h₁
  /-
  n m : ℕ
  ⊢ n = 1
  -/

example (n m : Nat) (h₁ : n = 1) : m ≠ 2 := by
  absurd h₁
  /-
  n m : ℕ
  ⊢ ¬n = 1
  -/

example (n m : Nat) (h₁ : n ≠ 1) : m ≠ 2 := by
  absurd id h₁
  /-
  n m : ℕ
  h₁ : n ≠ 1
  ⊢ n = 1
  -/

example (n : Nat) (h₁ : n ≠ 1) (h₂ : n = 1) : n = 3 := by
  absurd h₁, h₂

example (n : Nat) (h₁ : n ≠ 1) (h₂ : n = 1) : n = 3 := by
  absurd h₂, h₁

The use of not_not could be replaced with first trying a decidable version, in case people want to try avoiding the axiom of choice when possible.

[Kyle Miller]

It's too bad that push_neg is a mathlib tactic, otherwise push_neg would be a great tactic to use here. Maybe mathlib can have absurd! for doing absurd then push_neg, like contrapose!.

[Kyle Miller]

It's probably worth seeing if anything breaks with a no-comma version:

syntax "absurd " term:arg (term:arg)? : tactic

That way exact absurd h h' can always be replaced with absurd h h'.

[Kyle Miller]

MrQubo said:

Is this 2-argument absurd useful though? contradiction should be able to deal with such cases.

The contradiction tactic can do it, but I figure if you know what the contradiction is, it's clearer (and slightly more efficient) to be able to say what the absurdity is directly.

[Jakub Nowak]

Makes sense. Though, both problems could be solved (albeit, very not trivially). IDE could display contradicting hypotheses to make it clear what they are. Efficiency is probably very negligible and caching would also help.

[Kyle Miller]

contradiction does many things, not just absurd, plus it's inherently an O(n^2) algorithm, where n is the number of local hypotheses; it uses definitional equality to find an absurd pair. It's definitely not negligible in general (though I imagine it's negligible in most cases).

[Kyle Miller]

While an IDE feature would be nice, the absurd pair is not listed in the source code; from the perspective of proof maintenance, if details change (e.g. Lean version, simp sets, etc.) then you won't know what the contradictory pair is supposed to be without some more investigation.

[Jakub Nowak]

Kyle Miller said:

then you won't know what the contradictory pair is supposed to be without some more investigation.

IDE could display information from the cache though.

[Kyle Miller]

Here's the story:

1. You have a project
2. You update Lean/mathlib/etc.
3. A contradiction tactic fails.
4. Now what? How can you figure out why it doesn't work anymore?

There's no caching system available for this; nowhere for Lean to look to see how contradiction used to succeed. You might not even have any oleans from before updating.

This doesn't mean you shouldn't use contradiction, but it does mean that there's a reason people might want an explicit absurd.

The comparison shouldn't be absurd vs contradiction (then why not tauto, etc.?)

Beyond the clarity of explicit proofs, the other value of two-argument absurd is that you don't have to remember the correct order for the arguments. I know I often write exact (hn h).elim instead of exact absurd h hn just to avoid accidentally writing exact absurd hn h.

[Violeta Hernández]

I find it a bit odd that we have exfalso and absurd as tactics to begin with, when both are essentially just applying a single lemma.

[Jakub Nowak]

absurd is not just applying lemma, it also does it in a order that avoids double negation.
rfl is also just applying a single lemma.
I use them often enough to appreciate the fact, that I can write exfalso instead of apply False.elim.

[Mario Carneiro]

I almost never need to use exfalso, I just change the last exact to cases

[Jakub Nowak]

I use exfalso when after doing some case-splitting I know some case is impossible. I add exfalso at the begging of the proof for this case, so whoever's reading the proof will know, that I'm trying to prove that this case is impossible. Also it's probably efficient to forget about the goal.

[Aaron Liu]

I use exfalso to clear dependencies of the goal on the hypotheses