Basic dependent types question

Stream: general

[James Sully]

abbrev T : Bool → Type
| true => Nat
| false => Unit

def f (b : Bool) : T b := match b with
| true => 1
| false => ()

def f' (b : Bool) : T b := if h : b
  then 1
  else ()

Why does f typecheck, but f' doesn't?

[Kyle Miller]

match replaces b in the expected type with each case, but for if the expected type is T b in both cases. When b is replaced with true/false, then T b reduces to Nat or Unit.

[James Sully]

Thanks. Is there some reason if can't do the same thing?

[James Sully]

workaround:

def f' (b : Bool) : T b := if h : b
  then
    have hNat : T b = Nat := by rw [h]
    by
      rw [hNat]
      exact 1

  else
    have hUnit : T b = Unit := by simp only [h]
    by
      rw [hUnit]
      exact ()

[Kyle Miller]

James Sully said:

Is there some reason if can't do the same thing?

The basic reason is that if is not encoded in a way where the return type can depend on the condition value.

#check ite
-- ite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α
#check dite
-- dite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : ¬c → α) : α

It's just α no matter what c, t, and e are.

[Kenny Lau]

then you can do #print f' to check what the term actually was

[Kenny Lau]

recall that tactics are just fancy ways to generate terms

[Kyle Miller]

The if could insert casts in the t and e cases, but casts make reasoning harder.

Plus, b is a bool and if expects a Prop, so b is 'actually' b = true. Should if have special knowledge of bool and undo the coercion to find b and then look for occurrences of b in the expected types to replace with true/false? How often do arbitrary if conditions appear in expected types?

[Kyle Miller]

For match, the usual case is matching on a variable. For if, the usual case is a complex condition.

[James Sully]

Thanks, that's helpful, although I don't fully grasp what's going on.