Axioms used by csimp are not reported

Stream: lean4

[Eric Wieser]

Here's a proof of false that smuggles an axiom through csimp:

def one := 1
def bad_one := 2

axiom cheating : False

@[csimp] theorem oops : one = bad_one := cheating.elim

theorem ohno : one = 2 := by native_decide

/-- info: 'ohno' depends on axioms: [Lean.ofReduceBool] -/
#guard_msgs in
#print axioms ohno

Should ofReduceBool somehow track the other axioms it uses?

[Kim Morrison]

An alternative might be to modify the csimp attribute itself to ban the use of nonstandard axioms in tagged lemmas.

[Eric Wieser]

Banning is probably overkill, but it could emit a warning that it is no safer than implemented_by if it detects such axioms

[Eric Wieser]

I don't think we should force the user to replace @[csimp] + sorry+ --TODO with implemented_by

[Kim Morrison]

I agree a warning is better. But sorryAx should probably count as a "standard axiom" for this check.

[Kim Morrison]

issue/PR welcome.

[Eric Wieser]

Kim Morrison said:

sorryAx should probably count as a "standard axiom" for this check.

Well then you can conclude that your theorem is "sorry free" when actually you just hid your sorry behind a csimp!

[Kim Morrison]

Indeed, I'm always in the mind set that sorry can't ever hit a master branch... For projects that work otherwise, I agree.

[Eric Wieser]

lean4#7463