Stream: new members

Topic: basic dependent types question

Rado Kirov (Mar 27 2022 at 04:37):

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 (Mar 27 2022 at 06:04):

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 (Mar 27 2022 at 06:08):

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 (Mar 27 2022 at 06:09):

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

Kyle Miller (Mar 27 2022 at 06:15):

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 (Apr 03 2022 at 04:11):

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 (Apr 03 2022 at 04:33):

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 (Apr 03 2022 at 04:42):

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 (Apr 04 2022 at 18:40):

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

Last updated: Dec 20 2023 at 11:08 UTC