Zulip Chat Archive

Stream: general

Topic: cheat tactic


view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 21 2020 at 10:36):

have you tried it?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 21 2020 at 10:41):

`[exact C]?

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 21 2020 at 21:29):

can we ban this tactic?

view this post on Zulip Ryan Lahfa (May 21 2020 at 21:29):

in the competitive international Lean speedruns preferably

view this post on Zulip Mario Carneiro (May 21 2020 at 21:30):

I'd rather ban the constant

view this post on Zulip Kevin Buzzard (May 21 2020 at 22:29):

You can always check to see which axioms a proof used

view this post on Zulip Kevin Buzzard (May 21 2020 at 22:30):

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

view this post on Zulip Matt Earnshaw (May 21 2020 at 22:34):

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

view this post on Zulip Matt Earnshaw (May 21 2020 at 22:34):

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

view this post on Zulip Ryan Lahfa (May 21 2020 at 23:25):

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

view this post on Zulip Ryan Lahfa (May 21 2020 at 23:25):

(and even the whole club itself…)

view this post on Zulip 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: May 13 2021 at 05:21 UTC