## Stream: general

### Topic: exfalso determinstic timeout!

#### Kevin Buzzard (Feb 03 2022 at 18:32):

@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 (Feb 03 2022 at 19:00):

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 (Feb 03 2022 at 19:21):

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 (Feb 03 2022 at 19:28):

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 (Feb 03 2022 at 19:30):

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 (Feb 04 2022 at 08:55):

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 (Feb 04 2022 at 11:32):

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 (Feb 04 2022 at 18:39):

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 (Feb 04 2022 at 18:40):

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 (Feb 04 2022 at 19:50):

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 (Feb 04 2022 at 19:52):

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 (Feb 04 2022 at 19:53):

(because I have contradictory hypotheses)

Last updated: Dec 20 2023 at 11:08 UTC