of_decide_eq_true implementation

Stream: lean4

[Mike Schneeberger]

Why is the theorem of_decide_eq_true (from Prelude.lean) ...

theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun h =>
  match (generalizing := false) inst with
  | isTrue  h₁ => h₁
  | isFalse h₁ => absurd h (ne_true_of_eq_false (decide_eq_false h₁))

.... not simply implemented like this?

theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun h =>
  match inst with
  | isTrue (h1 : p) => h1
  | isFalse _ => Bool.noConfusion h

[Mario Carneiro]

you are welcome to PR it (no promises about it getting in though, I'm not the one with the big green button when it comes to changes to core)

[Mario Carneiro]

the main important aspect would be ensuring that both implementations compile to an unreachable, but I think that will be the case here

[Mario Carneiro]

actually since this is a theorem I guess the compilation doesn't even matter here. Proofs in core are sometimes a bit weird since they aren't the focus

[Mario Carneiro]

the more idiomatic proof would use nomatch h instead of noConfusion directly

[Mario Carneiro]

you might even be able to leave off the isFalse case entirely

[Reid Barton]

It may have been hand-ported from Lean 3 long ago and never given any further attention.

[Mike Schneeberger]

yes, nomatch h works as well:

theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun h =>
  match inst with
  | isTrue (h1 : p) => h1
  | isFalse _ => nomatch h

Concerning a PR, it says in the contribution guidelines to hold off on submitting PRs. I guess, the core team will eventually clean up Prelude.lean and simplify theorems like of_decide_eq_true that are hand-ported from Lean3 anyway. Or, what do you think?

Thanks a lot for the clarifications!

[Mario Carneiro]

It is unlikely that anything will happen to these proofs unless contributors care to make modifications (and there is a chance that such modifications will be seen as a nuisance), which is why they tend to sit unmodified for a long time

[Kevin Buzzard]

In case you hadn't seen from another thread, the main core lean developer has been in the process of changing jobs and there is a backlog of issues right now; this issue, whilst cool, can probably wait until the developers remove the warning that they are overwhelmed from the lean 4 contributions readme