Vectors and dependent function types

Ordinary mathematical functions have a domain and a codomain. In Lean, we write f : α → β to denote that f is a function with domain α and codomain β. More briefly, that f is a function from α to β.

The following is a simple example of a function from ℕ to ℤ that we’ve called double.

def double (n : ℕ) : ℤ := 2 * n

We can check that double has the expected type by issuing the command #check double. This displays double : ℕ → ℤ. Alternatively, we can prove that double has the expected type, as in the following example.

example : ℕ → ℤ := double

The odd-looking statement above says, “Here’s an example, I’m going to produce a term of type ℕ → ℤ. And double is just such a term”. Lean’s type-checking mechanism goes to work. It finds no errors and stays quiet. Were you to replace ℤ above with an ℕ, you’d get an error message. Try it and see.

Lean permits a more general definition of function. The codomain of a so-called dependent function can depend on the type of its argument. Our aim in this post is to fill in the sorry below to define a dependent function.

def zero_vec (n : ℕ) : vector ℝ n := sorry

Important: if you’re following along at home, you’ll need to place import data.vector data.real.basic at the top of your Lean file.

The function zero_vec should map its input n to a length n zero vector of real numbers. The domain of the function is still ℕ, but codomain vector ℝ n depends on the value n.

Lists and vectors

To start, we’ll define a function that produces a list of length n consisting of real zeros. Below, note that the codomain is list ℝ, the type of lists with real entries.

def zero_list (n : ℕ) : list ℝ := list.repeat 0 n

This is a simple application of one of the core Lean functions for working with lists. I’m sure you can guess what list.repeat does. To check our intuition, we have the following special case.

example : zero_list 5 = [0,0,0,0,0] := rfl

The rfl here is a proof by reflexivity, an (iterated) application of the definitions until the computer is left with two terms that are clearly equal.

What’s the difference between a vector on length n and a list of length n? The list type doesn’t “know” about the length of its terms. A term of type vector ℝ n consists of two items of information: (1) a list and (2) a proof that the list has length n. Here’s an example.

def myvec : vector ℝ 5 := ⟨[5,10,15,20,25], rfl⟩

The vector myvec consists of the vector [5,10,15,20,25] and rfl, the proof that this vector has length 5.

Using the same idea, we construct a vector of length 100, consisting of zeros.

example : vector ℝ 100 := ⟨zero_list 100, rfl⟩

So surely, it’s now a simple matter of replacing 100 with n to produce a vector of length n. But the following doesn’t work.

example (n : ℕ) : vector ℝ n := ⟨zero_list n, rfl⟩

Why not? A proof by rfl involves a finite computation. You can see this in action if you replace 100 above with a larger number. The proof takes longer and longer until you hit your computer’s limit. On my computer, using 5000 produces a “deep recursion” error.

When we replace 100 with n, we’re asking for something entirely different. We’re asking for a proof that works when n is arbitrary. This is not the same as fixing n and asking a proof for that particular n. In much the same way, it’s a finite computation to determine, for any given even number \(n > 2\) whether \(n\) is a sum of two primes. However, it’s quite a different thing to do that for an arbitrary \(n\).

Conveniently, core Lean has a lemma list.length_repeat that shows a list produced by repeating a single term n times has length n.

Dependent functions

Using list.length_repeat to provide the proof, we can finally define our function.

def zero_vec (n : ℕ) : vector ℝ n :=
⟨zero_list n, list.length_repeat 0 n⟩

Issuing the #check zero_vec command produces:

zero_vec : Π (n : ℕ), vector ℝ n

The Pi-binder Π is merely a fancy notation for writing a dependent function type. It shouldn’t be confused with the use of Π in mathematics to denote a product. For the dependent function zero_vec, the domain is ℕ, but we label it with a name (here n) to be used as an argument for the codomain vector ℝ n. There’s nothing special about n. The following proves that zero_vec has type Π (m : ℕ), vector ℝ m.

example : Π (m : ℕ), vector ℝ m := zero_vec

In fact, all functions in Lean have a dependent function type. It just so happens that the codomain is a constant ‘function’ of the input value for ordinary functions.

Consider again our function double.

example : Π (n : ℕ), ℤ := double

The above shows that double is a dependent function, albeit one in which the codomain ℤ does not depend on n.

Exercise

  1. Generalise zero_vec to a function const_vec such that const_vec c n is a length n vector all of whose entries are c, for some real constant c. What is the type of const_vec?
  2. Generalise further to a function const_vec' where const_vec' c n is is a length n vector all of whose entries are c, for some c : α, for an arbitrary type α. What is the type of const_vec'?
  3. (Hard) Write a function that adds two vectors of natural numbers of length n. Do this by filling in the sorry below.
    def add_vec {n : ℕ} (v₁ v₂ : vector ℕ n) : vector ℕ n := sorry
    Run a test on your definition by ensuring the following gives no error.
    example : add_vec ⟨[0,1,2],rfl⟩ ⟨[5,6,7],rfl⟩ = ⟨[5,7,9], rfl⟩ := rfl
    You’ll need experience writing recursive definitions in Lean.
  4. (Harder) Having finished the exercise above, show that the nth entry of add_vec v₁ v₂ is the sum of the nth entries of v₁ and v₂. That is, fill in the sorry below:
    lemma nth_add_nth : Π {n : ℕ} (v₁ v₂ : vector ℕ n) (a : fin n),
    v₁.nth a + v₂.nth a = (add_vec v₁ v₂).nth a := sorry

Decidable propositions III

We’ve seen the basics of decidable in Decidable propositions I and if-then-else constructions in Decidable propostions II. Now, we’ll see how to prove results through type class inference.

If you’ve been following along and recreating decidable in your own hidden namespace, it’s now time to declare an important, albeit trivial, instance.

instance decidable_eq_self {α} (x : α) : decidable (x = x) := is_true rfl

That is, it is decidable whether x=x, for any x : α and for any Sort α. We’ll use this to show 5 ≠ 5 is decidable.

example : decidable (5 ≠ 5) := infer_instance

How did this work? Surely we can only prove 5=5 is decidable, not 5 ≠ 5? But recall we’ve already prove that ¬p is decidable if p is. Type class inference chains together these two instances.

True and false propositions

Consider the following proof:

example : ite (5 = 5) true false := trivial

The term trivial is a proof of true. But ite (5 = 5) true false is definitionally equal to true. Whence, trivial is an appropriate proof!

For the remainder of this post, we’ll use a stripped-down version of the natural numbers, mynat. We do this to hide the type class instances that Lean knows about for the ordinary natural number type. If you don’t want to use mynat, please just replace it everywhere below with nat.

Here’s our proof of decidable (a ≤ b).

instance decidable_mynat_le (a : mynat) : ∀ b : mynat,
decidable (a ≤ b) :=
begin
  induction a with a ha,
  { intro b, apply is_true, apply mynat.zero_le, },
  { intro b,
    induction b with b hb,
    { apply is_false, apply not_succ_le_zero, },
    { cases ha b with h h,
      { apply is_false, intro h₂,
        apply h, exact le_of_succ_le_succ h₂, },
      { apply is_true, exact succ_le_succ_of_le h, }, } },
end

Using this, we have,

example : ite ((20 : mynat) ≤ 30) true false := trivial

effectively showing that 20 ≤ 30 is a true decidable proposition.

Likewise,

example : ¬ ite ((30 : mynat) ≤ 20 ) true false := false.elim

proves that 30 ≤ 20 is a false decidable proposition.

Trying to get Lean to prove the truth of a false decidable proposition gives an error message. The following code

example : ite ((30 : mynat) ≤ 4) true false := trivial

gives the error message

type mismatch, term
  trivial
has type
  true
but is expected to have type
  ite (30 ≤ 4) true false

The previous examples were straightforward applications of single decidable instances. Of more interest, we have that (5 ≤ 6) ∧ (x = x) is a true decidable proposition for any x. We know this because the type class inference systems allows Lean to derive a decision procedure for (5 ≤ 6) ∧ (x = x) by chaining together decidability of 5 ≤ 6 and of x = x

example (x : mynat) : ite (((5 : mynat) ≤ 6) ∧ (x = x)) true false := trivial

We’ve seen enough of these examples to justify introducing the following standard Lean definition,

def as_true (c : Prop) [decidable c] : Prop := ite c true false

so that the above proof is more succinctly expressed as

example (x : mynat) : as_true (((5 : mynat) ≤ 6) ∧ (x = x)) := trivial

Proof of a true proposition

Really, we don’t want to prove as_true c, we want to prove c!

The following definition is a game-changer in this respect.

def of_as_true {c : Prop} [h₁ : decidable c] (h₂ : as_true c) : c :=
match h₁, h₂ with
| (is_true hc),  h₂ := hc
| (is_false _),  h₂ := false.elim h₂
end

At long last, here’s a proof of a true proposition, using type class inference. I’ve removed the mynat type annotation just to clarify the exposition.

example : (20 ≤ 30) ∧ (5 = 5) := of_as_true trivial

As an exercise, come up with an example where the second pattern in of_as_true is matched. You’ll end up proving a false statement, hence at least one of your hypotheses must be false.

Lean uses the notation dec_trivial as a shorthand for of_as_true trivial. 

example : (5 ≠ 7) ∧ (10 ≤ 20) := dec_trivial

Exercise

Referring to the definition of mynat, fill in the sorry below:

instance decidable_eq (x : mynat) : ∀ y : mynat, decidable (x = y) := sorry

Decidable propositions II

Recall from our previous post the definition of decidable.

class inductive decidable (p : Prop) : Type
| is_false  : ¬p → decidable
| is_true   : p → decidable

We’ll later discuss how this class works in conjunction with type class inference to automate proofs of decidable propositions. In this post, we show how conditionals are implemented in Lean using the decidable recursor.

If-then-else

The ite function is one of two Lean implementations of an ‘if-then-else’ construct.

def ite (c : Prop) [d : decidable c] {α} (t e : α) : α := decidable.rec_on d (λ hnc, e) (λ hc, t)

Given a decidable proposition c and terms t and e of some Sort α, the expression ite c t e reduces to e in the case that c ‘is false’ and to t in the case that c ‘is true’. By ‘is true’, I mean that the instance d results from the application of the is_false constructor of decidable. Likewise for ‘is true’.

In the following example application, the proposition c is 5 = 6. But where is the instance of decidable (5 = 6)?

lemma foo : ite (5 = 6) 10 20 = 20 := rfl

The answer is that Lean uses type class inference to provide the appropriate instance. You can see this in action by enabling the display of implicit parameters then printing the definition of foo.

set_option pp.implicit true

#print foo

Lean spits out (inter alia):

theorem foo : @ite ℕ (5 = 6) (nat.decidable_eq 5 6) 10 20 = 20
@rfl ℕ (@ite ℕ (5 = 6) (nat.decidable_eq 5 6) 10 20)

nat.decidable_eq 5 6 is an proof of decidable (5=6). This is a simple example, but Lean can use type class inference to chain instances:

lemma bar : ite (5 ≠ 6) 10 20 = 10 := rfl

The lemma bar has definition:

theorem bar : @ite ℕ (5 ≠ 6) (@ne.decidable ℕ (λ (a b : ℕ), nat.decidable_eq a b) 5 6) 10 20 = 10 :=
@rfl ℕ (@ite ℕ (5 ≠ 6) (@ne.decidable ℕ (λ (a b : ℕ), nat.decidable_eq a b) 5 6) 10 20)

Lean has chained ne.decidable and nat.decidable_eq to prove decidable (5 ≠ 6).

Dependent if-then-else

For some applications, it isn’t sufficient to know whether a proposition p is true of false, we may also need a proof of the truth or falsity of p. The solution is to use dite, the dependent if-then-else function.

def dite {α} (c : Prop) [h : decidable c] : (c → α) → (¬ c → α) → α := λ t e, decidable.rec_on h e t

Given a decidable proposition c, given t : c → α and e : ¬ c → α, the term dite c t e either to t hc, for a given proof hc : c or to e hnc, for a proof hnc : ¬c.

As an example, we prove the law of the excluded middle, that p ∨ ¬p for a decidable proposition p.

lemma em (p : Prop) [decidable p] : p ∨ ¬p
:= dite p (λ hp, or.inl hp) (λ hnp, or.inr hnp)

If-then-else notation

ite and dite are so important that Lean facilitates their use via special notation. Our lemma bar can be written in this notation as:

lemma bar : (if (5 ≠ 6) then 10 else 20) = 10 := rfl

Similarly, the law of the excluded middle has the following proof:

lemma em (p : Prop) [decidable p] : p ∨ ¬p :=
if hp : p then or.inl hp else or.inr hp

Take care with the latter notation: in the ‘then’ clause above, hp is a proof of p whereas hp is a proof of ¬p in the ‘else’ clause.

Using this notation, we define a function mod such that mod a b is be the least natural number c such that \(a\equiv c\pmod b\).

def mod : ℕ → ℕ → ℕ
| a 0       := a
| a (b + 1)   :=  
if h : a < (b + 1) then a else
  have a - (b + 1) < a, from nat.sub_lt (show 0 < a, by linarith) (show 0 < (b+1), by linarith),
  mod (a - (b + 1)) (b + 1)

The have expression above is needed for well-founded recursion.

Decidable propositions I

In our last post, we looked at relations and briefly showed how Lean can sometimes prove a relation is decidable. Here, we take a closer look at decidability, a concept that rests on three pillars:

  • An inductive type class through which propositions can be marked as decidable.
  • A type class inference system for automatically proving decidability of propositions. This system is not limited to decidable but pertains to all type classes.
  • A mechanism for automatically proving true decidable propositions via type class inference.

In this post, we discuss the first two points. The follow-on posts are Decidable propositions II and Decidable propositions III.

The decidable type class

decidable is an inductive type class with two constructors.

class inductive decidable (p : Prop) : Type
| is_false  : ¬p → decidable
| is_true   : p → decidable

Thus, to provide an instance of decidable p is either to prove ¬p or to prove p. For instance, we can produce instances of decidable true and decidable false.

instance decidable_true : decidable true := is_true trivial

instance decidable_false : decidable false :=
is_false (λ q, false.elim q)

Here, trivial is a proof of true.

Of greater interest, we can use instances to derive other instances. Below, we produce an instance of decidable ¬p, given an instance of decidable p.

instance decidable_not (p : Prop) [h : decidable p] : decidable ¬p :=
match h with
| (is_false hnp)  := is_true hnp
| (is_true hp)    := is_false (λ hnp, hnp hp)
end

Likewise, an instance of decidable (p ∧ q) can be produced from instances of decidable p and decidable q.

instance decidable_and (p q : Prop) [h₁ : decidable p]
[h₂ : decidable q] : decidable (p ∧ q) :=
match h₁, h₂ with
| (is_false hnp), h₂              := is_false (λ hpq, hnp hpq.left)
| (is_true hp),   (is_false hnq)  := is_false (λ hpq, hnq hpq.right)
| (is_true hp),   (is_true hq)    := is_true ⟨hp, hq⟩ 
end

Try proving decidable (p ∨ q) using the same idea.

Type class inference

Now the clever bit. To prove decidable (p → q), we can rewrite p → q as ¬p ∨ q (a task that, admittedly, requires decidability of p) and then ask Lean to apply the instances it already knows!

instance decidable_if (p q : Prop) [h₁ : decidable p]
[h₂ : decidable q] : decidable (p → q) :=
by { rw imp_iff_not_or, apply_instance }

Lean first reduces the problem to finding instances of decidable ¬p and decidable q. The latter is a hypothesis. The former, reduced (via our result decidable_not) to finding an instance of decidable p.

In term-mode, infer_instance plays the same role as the tactic apply_instance.

example (p q : Prop) [decidable p] [decidable q] :
decidable $ (p ∧ q) → q := infer_instance

Relations in Lean

What is a relation?

In a typical undergraduate mathematics course, a relation on a set \(A\) is defined to be a subset of \(A\times A\), the cartesian product of \(A\) with itself.

In the Lean approach, a relation on a type α is a function of type α → α → Prop. That is, a function that takes two terms x and y of type α and returns a Prop.

The Lean approach corresponds much more closely with the intuitive notion of relation than does the more traditional approach. Consider the following definition.

def near_to (x y : ℕ) : Prop := (x - y) < 5 ∧ (y - x) < 5

This defines a relation on natural numbers. It is reflexive and symmetric, but not transitive. Here’s a proof of reflexivity.

example : reflexive near_to :=
begin
  intro x, split; { rw nat.sub_self, norm_num }, 
end

What does this do? The definition of reflexive (which one finds by typing #print reflexive) is:

def reflexive : Π {β : Sort v}, (β → β → Prop) → Prop :=
λ {β : Sort v} (r : β → β → Prop), ∀ (x : β), r x x

So to prove that a relation on a type β is reflexive is precisely to show ∀ (x : β), r x x. Our proof begins by introducing a term x of type ℕ. To prove near_to x x is to show (x – x) < 5 ∧ (x – x) < 5. Each conjunct is dealt with identically.

As an exercise, fill in the sorrys in the following. Post your solutions as a comment!

example : symmetric near_to := sorry

example : ¬(transitive near_to) := sorry

Decidable relations

It would be nice if we could deduce simple numerical results with minimal effort. We’ll see how to do that and also introduce some nice notation.

The command below introduces the symbol ∼ to be used as an infix name for the relation near_to.

local infix `∼`:50 := near_to

With this notation, we’ll prove 5 is near to 7.

example : 5 ∼ 7 := by { split; norm_num }

Fine. But can’t Lean just see this obvious fact? It can if we can prove that near_to is a decidable_rel. That is, we must show for every x and y that near_to x y is decidable, a proposition for which there is an algorithm for determining its truth or falsity.

Fortunately, Lean provides a mechanism that can, in many cases, automatically derive that a relation (or Prop) is decidable. Having made the above definition, we can invoke the derive handler by adding the attribute [derive decidable_rel] to near_to. Make sure first to import tactic.

attribute [derive decidable_rel] near_to

Alternatively, the previous definition could be decorated:

@[derive decidable_rel]
def near_to (x y : ℕ) : Prop := (x - y) < 5 ∧ (y - x) < 5

Via either method, Lean will derive that a typeclass instance of decidable_rel near_to. After this, the previous numerical result can be proved using dec_trivial, 

example : 5 ∼ 7 := dec_trivial