Fin.elim0

Stream: lean4

[Kenny Lau]

This is probably a nofix, but I'll just put it here as a record.

universe u

def Fin.elim0' {C : Fin 0 → Sort u} (x : Fin 0) : C x := x.elim0

def C : Fin 0 → Prop := sorry

theorem foo1 : ∀ x : Fin 0, C x :=
  Fin.elim0 -- fails

theorem foo2 : ∀ x : Fin 0, C x :=
  (Fin.elim0 ·)

theorem foo3 : ∀ x : Fin 0, C x :=
  Fin.elim0'

theorem foo4 : ∀ x : Fin 0, C x :=
  (Fin.elim0' ·)

def P : Prop := sorry

theorem foo5 : Fin 0 → P :=
  Fin.elim0

theorem foo6 : Fin 0 → P :=
  (Fin.elim0 ·)

theorem foo7 : Fin 0 → P :=
  Fin.elim0'

theorem foo8 : Fin 0 → P :=
  (Fin.elim0' ·) -- fails, needs @[elab_as_elim]

[Aaron Liu]

We do have docs#Fin.rec0

[Kenny Lau]

Basically, because of how Fin.elim0 is set up, it can fail to prove certain things. I see that it is in init so probably there is no access to @[elab_as_elim], so I tried to provide another version Fin.elim0' that works for the previously failed case, but since there is no @[elab_as_elim] then it fails in the opposite case.

[Aaron Liu]

Fin.rec0 isn't @[elab_as_elim], though

[Kenny Lau]

Aaron Liu said:

We do have docs#Fin.rec0

Thanks, you helped me golf off 5 bytes :upside_down:

[Aaron Liu]

It's actually 6 bytes if you account for utf-8 encoding

[Mario Carneiro]

have you tried nofun? that might golf some more

[Kenny Lau]

@Yaël Dillies what does that reaction mean?

[Yaël Dillies]

That there is no fun

[Aaron Liu]

Not everyone will know what nofun does (it's fun x1 x2 x3 ... => nomatch x1 x2 x3 ...)

[Kenny Lau]

Mario Carneiro said:

have you tried nofun? that might golf some more

Done :slight_smile:

[Mario Carneiro]

also known as "my favorite proof term", which you used to be able to write by just finishing your proof with . instead of := proof

[Aaron Liu]

Unfortunately it's deprecated, which I only know because sometimes the parser messes up and thinks I'm trying to use it when in reality I'm just not done writing yet.

[Kyle Miller]

@Kenny Lau What was the issue here? That Fin.elim0 is a nondependent eliminator and you were looking for Fin.rec0?

If so, then yes, this is a nofix.

Probably Fin.rec0 could stand to have elab_as_elim (no, there are no staging difficulties to add this attribute, it is builtin).