cheat tactic

Stream: general

[Kevin Buzzard]

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]

have you tried it?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

`[exact C]?

[Matt Earnshaw]

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]

can we ban this tactic?

[Ryan Lahfa]

in the competitive international Lean speedruns preferably

[Mario Carneiro]

I'd rather ban the constant

[Kevin Buzzard]

You can always check to see which axioms a proof used

[Kevin Buzzard]

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

[Matt Earnshaw]

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

[Matt Earnshaw]

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

[Ryan Lahfa]

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

[Ryan Lahfa]

(and even the whole club itself…)

[Ryan Lahfa]

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