Importing a file changed `dite` if macro semantics

Stream: mathlib4

[Yakov Pechersky]

Consider:

import Mathlib.Init.Data.Nat.Lemmas
-- comment out to make `extend_apply` work and `extend_apply_noninj` break

def Function.Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

@[simp] theorem exists_apply_eq_apply' (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩

noncomputable section Extend

attribute [local instance] Classical.propDecidable

def extend (f : α → β) (g : α → γ) (e' : β → γ) : β → γ := fun b =>
  if h : ∃ a, f a = b then g (Classical.choose h) else e' b

def extend' (f : α → β) (g : α → γ) (e' : β → γ) : β → γ := fun b =>
  @dite γ (∃ a, f a = b) (Classical.propDecidable _) (fun h => g (Classical.choose h)) (fun _ => e' b)

theorem extend_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [Decidable (∃ a, f a = b)] :
    extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b := by
  unfold extend
  congr

theorem extend'_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [Decidable (∃ a, f a = b)] :
    extend' f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b := by
  unfold extend'
  congr

@[simp]
theorem extend_apply {f} (hf : Function.Injective f) (g : α → γ) (e' : β → γ) (a : α) :
    extend f g e' (f a) = g a := by
  simp only [extend_def, dif_pos, exists_apply_eq_apply']
  exact congrArg g (hf $ Classical.choose_spec (exists_apply_eq_apply' f a))

@[simp]
theorem extend_apply_noninj (f : α → β) (g : α → γ) (e' : β → γ) (a : α) :
    extend f g e' (f a) = g a := by
  rw [extend_def, dif_pos (exists_apply_eq_apply' f a)]

@[simp]
theorem extend'_apply {f} (hf : Function.Injective f) (g : α → γ) (e' : β → γ) (a : α) :
    extend' f g e' (f a) = g a := by
  simp only [extend'_def, dif_pos, exists_apply_eq_apply']
  exact congrArg g (hf $ Classical.choose_spec (exists_apply_eq_apply' f a))

[Yakov Pechersky]

I think this change in the if macro also affects other porting attempts. Right now, the obvious definition of invFun results in specializing the α to Prop for some reason. Making the definition explicitly go through @dite avoids that

[Yakov Pechersky]

import Std.Logic -- comment out to make invFun work with Sort, Sort

@[reducible]
protected noncomputable def Classical.arbitrary (α) [h : Nonempty α] : α :=
  Classical.choice h

noncomputable section Extend

attribute [local instance] Classical.propDecidable

noncomputable def invFun [Nonempty α] (f : α → β) : β → α :=
  fun y => if h : (∃ x, f x = y) then (Classical.choose h) else Classical.arbitrary α

noncomputable def invFun' [Nonempty α] (f : α → β) : β → α :=
  fun y => @dite α (∃ x, f x = y) (Classical.propDecidable _)
    Classical.choose (fun _ => Classical.arbitrary _)

#check @invFun -- Prop, Sort
#check @invFun' -- Sort, Sort

[Mario Carneiro]

It appears to be the fault of exists_prop_decidable:

-- Comment this out to make invFun work with Sort, Sort
instance exists_prop_decidable {p} (P : p → Prop)
  [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
if h : p then
  decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩
else isFalse fun ⟨h', _⟩ => h h'

@[reducible]
protected noncomputable def Classical.arbitrary (α) [h : Nonempty α] : α :=
  Classical.choice h

noncomputable section Extend

attribute [local instance] Classical.propDecidable

noncomputable def invFun [Nonempty α] (f : α → β) : β → α :=
  fun y => if h : (∃ x, f x = y) then (Classical.choose h) else Classical.arbitrary α

noncomputable def invFun' [Nonempty α] (f : α → β) : β → α :=
  fun y => @dite α (∃ x, f x = y) (Classical.propDecidable _)
    Classical.choose (fun _ => Classical.arbitrary _)

#check @invFun -- Prop, Sort
#check @invFun' -- Sort, Sort

[Mario Carneiro]

and it makes some sense too: with that instance available invFun will use it, and this unifies the universe metavar in {α : Sort _}

[Mario Carneiro]

I think this should be classed as a bug though, because definitions with a given (explicit) type are supposed to be fully elaborated using only their types

[Yakov Pechersky]

Yeah, I noticed that too here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Decidable.20of.20Exists.20changes.20.60if.60.20macro.20semantics