exfalso determinstic timeout!

Stream: general

[Kevin Buzzard]

@Billy Miao just showed me some Lean code at Xena where exfalso causes a determinstic timeout! This really surprised me because I thought exfalso would just be apply false.elim. Apparently not -- it seems to do something far more exotic involving the contradiction tactic, and contradiction also times out on the below goal.

import tactic
import data.real.basic

example (b : ℕ → ℝ) (M : ℝ) :
let s : finset ℕ := finset.range 101,
S : finset ℝ := finset.image (λ (n : ℕ), abs (b n)) s in
abs (b 100) ∈ S :=
begin
  intros s S,
  exfalso, -- deterministic timeout
end

[Reid Barton]

I think contradiction tries to check if you have both P and not P as hypotheses, or something? And maybe it tries to reduce s

[Kyle Miller]

Blocking reduction does eliminate the deterministic timeout (and it seems that s being reduced is the problem):

import tactic
import data.real.basic

@[irreducible]
def no_reduce {α : Type*} (x : α) : α := x

example (b : ℕ → ℝ) (M : ℝ) :
let s : finset ℕ := no_reduce $ finset.range 101,
S : finset ℝ := no_reduce $ finset.image (λ (n : ℕ), abs (b n)) s in
abs (b 100) ∈ S :=
begin
  intros s S,
  exfalso, -- no timeout

end

[Reid Barton]

Putting aside the question of what exfalso is doing in the first place, it seems reasonable that contradiction should do its work at "reducible" transparency level so this doesn't happen.

[Eric Rodriguez]

On a related but separate note, I always wished we could exfalso (_ : false); i dislike exact (...).elim and exfalso, exact as they often force awkward code

[Kevin Buzzard]

Billy actually found the timeout when applying the use tactic, a really common tactic amongst beginner mathematicians. Use tries triv which tries contradiction.

[Reid Barton]

Do you mean trivial? I didn't know about triv but from the documentation, its unique feature is that it doesn't try contradiction.

[Kyle Miller]

use now uses trivial' rather than triv (assuming you have a recent version of mathlib). use doesn't use trivial because it wants to be careful only to only look for things that are trivial with reducible visibility.

I recently renamed triv to trivial' and made a variant of trivial called triv that does everything but contradiction, since Kevin had wanted a tactic that really only looks for triviality. As far as I was able to tell, triv had only existed for the implementation of use.

[Kyle Miller]

Something that should still be done, I think, is make a variant of contradiction that similarly only looks at reducible visibility, then make trivial' use that instead.

[Kevin Buzzard]

Oh sorry, I might have been on an older mathlib when I wrote that post. The changes to triv came about from frustration that students were proving things accidentally using it

[Kevin Buzzard]

I was getting questions of the form "you said triv proves the goal when it's true but it also proves the goal when it's false"

[Kevin Buzzard]

(because I have contradictory hypotheses)