What does `unsafe` imply?

Stream: general

[nrs]

It seems unsafe allows non-termination in functions and recursive occurrences in inductive type constructors that are not strictly positive. Do we have: an inductive type that can be defined with unsafe but not without it can imply False?

[Kyle Miller]

unsafe implies nothing, since you can't use it in proofs.

Here's an example of a type that you can't define without unsafe:

inductive Bad where
  | c (h : Bad → Empty)

If it existed, we could prove false:

axiom Bad : Type
axiom Bad.c (h : Bad → Empty) : Bad
axiom Bad.recOn {motive : Bad → Sort _} (b : Bad) (c : (h : Bad → Empty) → motive (Bad.c h)) : motive b

theorem Bad.false (b : Bad) : False := by
  apply Bad.recOn b
  intro h
  have := h (Bad.c h)
  cases this

example : False := by
  have := Bad.c (fun x => x.false.elim)
  exact this.false

[nrs]

Kyle Miller said:

unsafe implies nothing, since you can't use it in proofs.

Here's an example of a type that you can't define without unsafe:

inductive Bad where
  | c (h : Bad → Empty)

If it existed, we could prove false:

axiom Bad : Type
axiom Bad.c (h : Bad → Empty) : Bad
axiom Bad.recOn {motive : Bad → Sort _} (b : Bad) (c : (h : Bad → Empty) → motive (Bad.c h)) : motive b

theorem Bad.false (b : Bad) : False := by
  apply Bad.recOn b
  intro h
  have := h (Bad.c h)
  cases this

example : False := by
  have := Bad.c (fun x => x.false.elim)
  exact this.false

Ah I see, tyvm this example is very instructive! I gather then that we can't express unsafe internally in Lean, would it be possible instead to express the effect of unsafe on the type system in a metatheory of Lean?

another related question would be: we have above a particular case of an unsafe type that cannot be defined without it and it implies false if we axiomatize it. Do we have also the general case, that necessarily any such type, i.e. a type that cannot be expressed without unsafe, will prove False if it is added as an axiom?

[Kyle Miller]

Do we have also the general case, that necessarily any such type, i.e. a type that cannot be expressed without unsafe, will prove False if it is added as an axiom?

I doubt it. My understanding is that the positivity checker is conservative in what it accepts.

[Kyle Miller]

unsafe is an escape hatch for programming, and it's not meant for reasoning.

[nrs]

Kyle Miller said:

Do we have also the general case, that necessarily any such type, i.e. a type that cannot be expressed without unsafe, will prove False if it is added as an axiom?

I doubt it. My understanding is that the positivity checker is conservative in what it accepts.

Thanks a lot this is enough to get me started on a deeper incursion into Lean's implementation, ty for the help!!