Zulip Chat Archive

Stream: general

Topic: cheat tactic


Kevin Buzzard (May 21 2020 at 10:36):

If I allow a constant C : false then I can prove anything in term mode using false.elim and I won't get warnings every time I want to skip a proof.

Kenny Lau (May 21 2020 at 10:36):

have you tried it?

Kevin Buzzard (May 21 2020 at 10:36):

Can I have an analogous constant tactic which closes any goal without triggering a warning that I'm using sorry?

Kevin Buzzard (May 21 2020 at 10:37):

That's what I want. I am trying to write some teaching material and I don't want to enter term mode

Kevin Buzzard (May 21 2020 at 10:37):

I just want to write nlinarith and the goal is closed and no warning about cheating, but I used a constant somehow.

Reid Barton (May 21 2020 at 10:41):

`[exact C]?

Matt Earnshaw (May 21 2020 at 15:55):

constant C : false
meta def cheat : tactic unit := `[exfalso, exact C]
example (n : ) : (n^2  2) :=
begin
  cheat,
end

my first tactic, but it does not feel like a great achievement

Ryan Lahfa (May 21 2020 at 21:29):

can we ban this tactic?

Ryan Lahfa (May 21 2020 at 21:29):

in the competitive international Lean speedruns preferably

Mario Carneiro (May 21 2020 at 21:30):

I'd rather ban the constant

Kevin Buzzard (May 21 2020 at 22:29):

You can always check to see which axioms a proof used

Kevin Buzzard (May 21 2020 at 22:30):

@Matt Earnshaw many thanks! I'll drop it in tomorrow

Matt Earnshaw (May 21 2020 at 22:34):

I would say no worries, but this tactic concerns me :+)

Matt Earnshaw (May 21 2020 at 22:34):

http://inutile.club/estatis/falso/

Ryan Lahfa (May 21 2020 at 23:25):

OMG, I know the author of this piece :^)

Ryan Lahfa (May 21 2020 at 23:25):

(and even the whole club itself…)

Ryan Lahfa (May 21 2020 at 23:28):

a bit off-topic, but from the same author: https://github.com/a3nm/academia/blob/master/CONTRIBUTING.md


Last updated: Dec 20 2023 at 11:08 UTC