Zulip Chat Archive

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 :=
  intros s S,
  exfalso, -- deterministic timeout

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

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 :=
  intros s S,
  exfalso, -- no timeout


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: Aug 03 2023 at 10:10 UTC