basic dependent types question

Stream: new members

[Rado Kirov]

Hello, I am playing with LEAN and quite new to dependent types so I have some basic questions. A function that takes a value and returns a type makes sense to me

def f(x: Nat) = if x > 1 then Nat else Bool

but what is a value of type f x and how does one construct one? My simple attempt to construct a typed pair is not accepted by LEAN

def test := Sigma.mk 2 1

Adding explicit type assertion (1 : f 2) doesn't seem to help. Doesn't LEAN evaluate f 2 at type-checking time turn it into Nat and pass the checker?

[Kyle Miller]

What you're running into with (1 : f 2) is that there's a somewhat complicated system in Lean to turn numerals into values -- it's able to tell that f 2 is Nat, but that takes a stronger sort of evaluation than it's willing to do. The error I'm seeing is failed to synthesize instance OfNat (f 2) 1. That means it's trying to take the natural number 1 and interpret it as a f 2, which it doesn't immediately know how to do. You can help it out though with ((1 : Nat) : f 2).

[Kyle Miller]

With Sigma, Lean usually needs help to figure out which Sigma you mean (especially here -- how is it supposed to guess to use f?) Even so, you need to give it the (1 : Nat) hint to help it interpret the natural number literal.

def test : Sigma f := Sigma.mk 2 (1 : Nat)

[Kyle Miller]

That Sigma f can also be written using the Σ x, f x notation

[Kyle Miller]

This OfNat business doesn't apply to things that aren't literals. For example this passes the type checker:

def mk2 (n : Nat) : f 2 := n

[Rado Kirov]

Ah, makes sense. Extra confusion around literals. A quick follow up then. How would I tell LEAN that the following function has type (x: Nat) -> f x (where f x is above).

def fn(x: Nat) : f x = if x > 1 then (1 : Nat) else false

This doesn't seem to work.

[Kyle Miller]

It won't fix it, but make sure to use := instead of = for a definition.

The reason things worked with, for example, (true : f 0) is that Lean is able to compute what f 0 is. In an if expression, however, at best you have an additional assumption x > 1, but that's not enough for Lean to compute what f x might be (x is still a variable, it's not a literal number). You can help it out using tactics though:

def fn(x: Nat) : f x :=
  if h : x > 1
  then by
    simp [f, h]
    exact (1 : Nat)
  else by
    simp [f, h]
    exact false

I'm using the "dependent if" notation; here h is a proof of either x > 1 or its negation.

[Kyle Miller]

You can also define some constructors

def f (x : Nat) := if x > 1 then Nat else Bool

def f.mk_nat (x : Nat) (h : x > 1) (n : Nat) : f x := by
  simp [f, h]
  exact n

-- I wasn't sure whether to write this as `¬ x > 1` just to make the `if` more convenient.
def f.mk_bool (x : Nat) (h : x ≤ 1) (b : Bool) : f x := by
  rw [← Nat.not_lt_eq] at h
  simp [f, h]
  exact b

def fn (x: Nat) : f x :=
  if h : x > 1 then f.mk_nat x h 1 else f.mk_bool x (Nat.not_lt_eq _ _ ▸ h) false

[Rado Kirov]

I didn't know about the 'dependent if' notation, this makes a lot of sense. Thanks!