Classical if then else

Stream: Is there code for X?

[Stepan Nesterov]

docs#ite requires proposition P to be decidable in order to form an "if then else" function. I can cheat in non-decidable propositions by using open Classical, as in

import Mathlib

open Classical in
theorem finrank_hom_isIrreducible_isIrreducible [IsIrreducible σ] :
    Module.finrank (IntertwiningMap ρ σ) = if Nonempty (Equiv ρ σ) then 1 else 0 := by
  sorry

abd then it works fine. However, I'm worried if this is another Fintype/Finset kind of situation where I'm conjuring data out of the axiom of choice, and hurting the constructive intent of docs#ite. Is there a nonconstructive version of "if then else" then I should use or is this fine?

[Eric Wieser]

It's slightly better to write that as

theorem finrank_hom_isIrreducible_isIrreducible [IsIrreducible σ] :
    Module.finrank (IntertwiningMap ρ σ) = open Classical in if Nonempty (Equiv ρ σ) then 1 else 0 := by
  sorry

though arguably you should really write

theorem finrank_hom_isIrreducible_isIrreducible [Decidable (Nonempty (Equiv ρ σ))] :
    Module.finrank (IntertwiningMap ρ σ) = if Nonempty (Equiv ρ σ) then 1 else 0 := by
  sorry

[Weiyi Wang]

Or maybe this should be two theorems, one for empty and one for nonempty?

[Robin Arnez]

Well, as long as nobody will ever write a Decidable instance for Nonempty (Equiv _ _), this is probably fine

[Yury G. Kudryashov]

There can be an instance assuming that both types are Fintypes, then you'll have conflicting instances.

[Robin Arnez]

I see, in that case the Decidable hypothesis is probably the best way to go