## 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: May 13 2021 at 05:21 UTC