Question about .rec: what’s special about false here?

Stream: general

[Mario Weitzer]

Why does this work (in Lean 3):

universe u
def false.elim‘ {C : Sort u} (h : false) : C := @false.rec C h

but this doesn‘t:

universe u
inductive test : Prop
def test.elim {C : Sort u} (h : test) : C := @test.rec C h

false is defined in exactly the same way as test after all. Also,

universe u
variables {C : Sort u} (h : test)
#check @test.rec C h

works just fine and gives type C.

[Reid Barton]

I think it's a bug/deficiency in the code generator that nobody ever got around to. You can use noncomputable! def as a workaround.

[Mario Weitzer]

This worked, thank you! A very strange bug. Wouldn’t this suggest that there’s something special about false internally even though it‘s just a regular inductive type?

[Reid Barton]

I think it's just the code generator that has special knowledge of it

[Mario Weitzer]

I see.

[Kyle Miller]

Interesting, even this isn't supported:

def test.elim {C : Type*} (h : test) : C := match h with end
/-
failed to generate bytecode for 'test.elim'
code generation failed, inductive predicate 'simple_graph.test' is not supported
-/

That suggests it's special handling of false

[Reid Barton]

Probably here and again ~25 lines later

[Mario Weitzer]

I also tried this (which doesn‘t work either, fails at assumption):

def test.elim {C : Sort u} (h : test) : C :=
begin
  have htC : test → C, from @test.rec C,
  have hc : C, from htC h,
  assumption
end

[Eric Wieser]

There is a hard-coded list of .recs that have native compiler support somewhere within Lean4

[Eric Wieser]

Notably List.rec and Nat.rec are also absent (edit: nevermind, Lean3)

[Kyle Miller]

Interestingly, this even though a custom false doesn't work, you're free to use a custom eq:

inductive test {α : Type*} : α → α → Prop | myrfl (x : α) : test x x

def test.elim (h : test 1 2) : ℕ := match h with end

[Mario Weitzer]

I‘m pretty new to Lean but hard coded facets which actually make a substantial difference are probably not the best idea.

[Reid Barton]

@Kyle Miller I guess that one's because the equation compiler proved false and then used false.rec?

[Anatole Dedecker]

Mario Weitzer said:

I‘m pretty new to Lean but hard coded facets which actually make a substantial difference are probably not the best idea.

Just to be clear, this "hard coded facet" has no incidence on the soundness of the system: Lean won't accept any proof about false that it wouldn't accept for your test. This is purely a code generation thing (i.e when you actually want to get an executable from your Lean code), so if you're not interested in that then it won't change anything.