Unfold partial function

Stream: lean4

[David Hamelin]

Hello,

I'm trying to prove the following theorem:

partial def partial_fun : Nat → Nat
| 2 => partial_fun 2
| x => x

example: partial_fun 3 = 3 :=
by
  unfold partial_fun -- doesn't work
  sorry

However, unfold fails. I think it's because it tries to unfold iteratively, and might not terminate because partial_fun is partial.
I also tried delta, but it doesn't work either.

There used to be a unfold1 tactic in Lean 3, that unfold only once, but it seems to have been renamed/removed in Lean 4.

How can I work around this issue ?

Thanks in advance

[Horațiu Cheval]

As far as I know it's not possible to prove anything about the definition of a partial function, you can just evaluate it.

[Horațiu Cheval]

The reason being essentially that a partial definition is not really an expression that makes sense in Lean's type theory, so the kernel cannot access such a definition. For example #reduce partial_fun 4 just prints partial_fun 4 and does not reduce it to 4. I think a partial definition is a shorthand for

unsafe def unsafe_fun : Nat → Nat
| 2 => unsafe_fun 2
| x => x

@[implemented_by unsafe_fun]
opaque partial_fun : Nat → Nat

So the partial function does not actually have a definition, it's just an opaque constant that is evaluated by a unsafe function

[David Hamelin]

Horațiu Cheval said:

The reason being essentially that a partial definition is not really an expression that makes sense in Lean's type theory, so the kernel cannot access such a definition. For example #reduce partial_fun 4 just prints partial_fun 4 and does not reduce it to 4. I think a partial definition is a shorthand for

unsafe def unsafe_fun : Nat → Nat
| 2 => unsafe_fun 2
| x => x

@[implemented_by unsafe_fun]
opaque partial_fun : Nat → Nat

So the partial function does not actually have a definition, it's just an opaque constant that is evaluated by a unsafe function

I see, thank you, I will add a step argument