85341d02ac
This PR gives a simpler semantics to `noncomputable`, improving predictability as well as preparing codegen to be moved into a separate build step without breaking immediate generation of error messages. Specifically, `noncomputable` is now needed whenever an axiom or another `noncomputable` def is used by a def except for the following special cases: * uses inside proofs, types, type formers, and constructor arguments corresponding to (fixed) inductive parameters are ignored * uses of functions marked `@[extern]/@[implemented_by]/@[csimp]` are ignored * for applications of a function marked `@[macro_inline]`, noncomputability of the inlining is instead inspected # Breaking change After this change, more `noncomputable` annotations than before may be required in exchange for improved future stability.
43 lines
1.2 KiB
Text
43 lines
1.2 KiB
Text
import Lean
|
|
|
|
/-!
|
|
This was once an exploit of a bug in the Lean kernel relying on the Lean kernel
|
|
falsely interpreting an expression as a Nat literal.
|
|
-/
|
|
|
|
noncomputable def g.{u} : PUnit.{u} → Nat := fun _ => open Classical in if Type = Type then 0 else 0
|
|
|
|
-- Just writing `Nat.pow (Nat.pow 10 8) 502` would also work; `Nat.pow (Nat.pow 10 8) 503` wouldn't
|
|
def T : Nat → Prop := fun x => if x = 0 then False else True
|
|
|
|
-- The kernel reduces this to a number between 10^8032 and 10^8048
|
|
noncomputable def POW! := Nat.pow (g.{0} ⟨⟩) 1
|
|
|
|
elab "#inject_bad_proof" : command => do
|
|
let decl : Lean.Declaration := .defnDecl {
|
|
name := `mythm,
|
|
hints := .regular 0,
|
|
safety := .safe,
|
|
type := (.app (.const `T []) (.const `POW! [])),
|
|
levelParams := [],
|
|
value := (.const `True.intro [])
|
|
}
|
|
Lean.Elab.Command.liftCoreM (Lean.addDecl decl)
|
|
|
|
/--
|
|
error: (kernel) declaration type mismatch, 'mythm' has type
|
|
True
|
|
but it is expected to have type
|
|
T POW!
|
|
-/
|
|
#guard_msgs in
|
|
#inject_bad_proof
|
|
|
|
theorem g_eq_zero : g.{u} n = 0 := by
|
|
unfold g
|
|
split <;> rfl
|
|
|
|
theorem show_false : False := by
|
|
change T (Nat.pow 0 1)
|
|
rw [← g_eq_zero]
|
|
exact mythm
|