-
Notifications
You must be signed in to change notification settings - Fork 67
/
Lean_part_1.html
343 lines (291 loc) · 39.4 KB
/
Lean_part_1.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width,initial-scale=1">
<title>Δ ℚuantitative √ourney | Learning Lean (Part 1)</title>
<link rel="shortcut icon" type="image/png" href="http://outlace.com/favicon.png">
<link rel="shortcut icon" type="image/x-icon" href="http://outlace.com/favicon.ico">
<link href="http://outlace.com/feeds/all.atom.xml" type="application/atom+xml" rel="alternate" title="Δ ℚuantitative √ourney Full Atom Feed" />
<link rel="stylesheet" href="http://outlace.com/theme/css/screen.css" type="text/css" />
<link rel="stylesheet" href="http://outlace.com/theme/css/pygments.css" type="text/css" />
<link rel="stylesheet" href="http://outlace.com/theme/css/print.css" type="text/css" media="print" />
<meta name="generator" content="Pelican" />
<meta name="description" content="" />
<meta name="author" content="Brandon Brown" />
<meta name="keywords" content="Lean" />
</head>
<body>
<header>
<nav>
<ul>
<li><a href="http://outlace.com/">Home</a></li>
<li><a href="http://outlace.com/pages/about.html">About</a></li>
<li><a href="http://outlace.com/tags/">Tags</a></li>
<li><a href="http://outlace.com/categories/">Categories</a></li>
<li><a href="http://outlace.com/archives/{slug}/">Archives</a></li>
</ul>
</nav>
<div class="header_box">
<h1><a href="http://outlace.com/">Δ ℚuantitative √ourney</a></h1>
<h2>Science, Math, Statistics, Machine Learning ...</h2>
</div>
</header>
<div id="wrapper">
<div id="content"> <h4 class="date">Jul 04, 2022</h4>
<article class="post">
<h2 class="title">
<a href="http://outlace.com/Lean_part_1.html" rel="bookmark" title="Permanent Link to "Learning Lean (Part 1)"">Learning Lean (Part 1)</a>
</h2>
<p>I'm going to be starting a series of blog posts on Lean 4, a dependently typed functional programming language and theorem prover. If none of that sounds familiar, no problem, we'll get to that. First, Lean 4 has not been officially released as a 1.0, so breaking changes to the code in these posts may occur, but I'll try to update from time to time. The current stable release of Lean is Lean 3.</p>
<p>Let me also preface that these blog posts, although meant to be instructive, mirror my own learning of Lean. I've been playing with Lean off and on since April 2020 but I am currently <em>not</em> an expert at Lean or functional programming in general, so there are likely going to be instances of me writing non-idiomatic Lean and doing things in not the most efficient way. Also, my goal in learning Lean was mostly to learn formalizing mathematics rather than functional programming, so these blogs will hence be mostly focused on the mathematics use of Lean. In terms of pre-requisites if you want to be able to follow along, anyone with a background programming in <em>some</em> programming language and at least a high school mathematics background should be able to follow along.</p>
<p>Go ahead and get Lean installed by following the guide here: <a href="https://leanprover.github.io/lean4/doc/quickstart.html">Lean Setup Guide</a>.</p>
<p>There's also a lively online community for Lean where friendly individuals from around the world will answer your questions surprisingly quickly: <a href="https://leanprover.zulipchat.com/">https://leanprover.zulipchat.com/</a></p>
<h3>What is Lean?</h3>
<p>Lean is a programming language. More specifically, Lean is a functional programming language. Probably the most well-known (at least to me) functional programming language is Haskell. A functional programming language usually refers to a <strong><em>purely</em></strong> functional programming language. Many programming languages support functions as first-class citizens, allowing functions to be passed as arguments and returned, but a purely functional language imposes that all functions have a well-specified and static type signature and no other side effects can occur within a function (e.g. writing to disk, playing a sound file, etc.). These are called pure functions. Moreover, the only data these pure functions have access to is what gets explicitly passed as an argument. And every expression in Lean has a type, including types themselves.</p>
<p>The mandate that all functions are pure is quite onerous coming from typical imperative programming languages such as C or Python. It is no longer trivial in a pure functional language to do something like read an input string, do some computation, write to a log and return a value. The benefit is that pure functions are completely predictable at compile-time, preventing a whole class of bugs.</p>
<p>Lean is not only a functional programming language, but a dependently-typed functional programming language. This means that types can depend on other types and values. For example, in Lean, you can define a type of list of integers of length 3, and thus if you try to construct an instance of that type by giving it 4 integers, it will fail. In essence, dependent types give you extreme expressiveness and granularity when defining new types.</p>
<h3>Why should you learn Learn?</h3>
<p>I think Lean is going to be <em>the next big thing</em> in the functional programming world and hopefully the formal software verification and mathematics world. So if any of those things interest you, it may be worth learning Lean.</p>
<p>One goal for me in learning Lean is to learn proofs in mathematics. I do data analysis, statistics and machine learning so my understanding of mathematics is very applied and calculational. I want to get a flavor of pure mathematics and how mathematical structures are made and theorems are proved. Because Lean is a dependently typed pure functional programming language, it can be used to encode all of modern mathematics using its type theory in place of traditional set theory.</p>
<p>In any case, doing math in Lean is actually <em>fun</em> a lot of the time. It's like a programming and logic puzzle. So stop with the Sudoku and just prove theorems in Lean instead.</p>
<h3>Natural Numbers</h3>
<p>Before we can do much of anything in mathematics, we're going to need some numbers. Now Lean already has numbers defined, of course, but we will pretend it doesn't.</p>
<p>Let's define the natural numbers, that is, the set of numbers 0, 1, 2, 3 ..., or the counting numbers.</p>
<div class="highlight"><pre><span></span><span class="nf">namespace</span><span class="w"> </span><span class="kt">Tutorial</span>
<span class="nf">inductive</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="kr">where</span><span class="w"> </span>
<span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span>
<span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span>
<span class="nf">end</span><span class="w"> </span><span class="kt">Tutorial</span>
</pre></div>
<p>The namespace section is what it sounds like and works similarly to how namespaces work in other programming languages. Outside the namespace you have to refer to identifiers inside the namespace by prefixing <code>[namespace name].[identifier]</code> (without the brackets). We enclose our code in this namespace to avoid name clashes because we are defining types and functions that already exist in Lean with the same names.</p>
<p>First, the keyword <code>inductive</code> means we are defining a new (inductive) type. In Lean's type theory, there are basically just two kinds of types, inductive types and function types, so we will use <strong><em>inductive</em></strong> a lot.</p>
<p>After the keyword <code>inductive</code> comes the name of the type we are defining, in this case, we are calling it <code>Nat</code>, for natural numbers. After the name of the type comes a colon and the keyword <code>Type</code>. </p>
<p>Recall, <em>every expression in Lean must have a type</em>, even the new type we are defining must itself be assigned a type. So in general, new inductive types will by default be assigned the type <code>Type</code>, which is an alias for <code>Type 0</code>, because if you ask Lean what the type of <code>Type</code> is, it must give you an answer, so it just creates an infinite hierarchy of types <code>Type : Type 1, Type 1 : Type 2</code> etc., meaning that the type of <code>Type</code> is <code>Type 1</code>.</p>
<p>You can ask Lean what the type of an expression is by using the <code>#check</code> command.</p>
<div class="highlight"><pre><span></span><span class="o">#</span><span class="n">check</span><span class="w"> </span><span class="kt">Nat</span>
<span class="c1">--Output: Nat : Type</span>
<span class="o">#</span><span class="n">check</span><span class="w"> </span><span class="kt">Type</span>
<span class="c1">--Output: Type : Type 1</span>
</pre></div>
<p>Now Lean tries to be smart and save you keystokes, so whenever possible, it will infer types when it can do so unambiguously. So it is fine to also declare our <code>Nat</code> type without explicitly assigning its type:</p>
<div class="highlight"><pre><span></span><span class="c1">-- This also works</span>
<span class="nf">inductive</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kr">where</span>
<span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span>
<span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span>
</pre></div>
<p>And two dashes is how you start a comment line. Or a multiline comment can be delimited using </p>
<div class="highlight"><pre><span></span>/-
Multi
line
comment
-/
</pre></div>
<p>Back to our new type.</p>
<div class="highlight"><pre><span></span><span class="nf">inductive</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="kr">where</span><span class="w"> </span>
<span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span>
<span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span>
</pre></div>
<p>After assigning <code>Nat</code> as being the type <code>Type</code> is the keyword <code>where</code> which is also optional, as this is also valid:</p>
<div class="highlight"><pre><span></span><span class="nf">inductive</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span>
<span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span>
<span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span>
</pre></div>
<p>I guess <code>where</code> is mostly of descriptive use, as you can translate the type declaration into English as "We are making a new inductive type named <code>Nat</code> of type <code>Type</code> where <code>zero</code> is declared to be of type <code>Nat</code> and <code>succ</code> is a function that maps values of type <code>Nat</code> to values of type <code>Nat</code>.</p>
<p>Back to the more verbose type declaration:</p>
<div class="highlight"><pre><span></span><span class="nf">inductive</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="kr">where</span><span class="w"> </span>
<span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span>
<span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span>
</pre></div>
<p>So after the <code>where</code> keyword, we start a new line beginning with the pipe <code>|</code> character. Each line beginning with <code>|</code> is called a <em>constructor</em> since these lines specify how to construct terms (aka elements, values or members) of the new inductive type.</p>
<p>First, we invent a name for a value of type <code>Nat</code>, in this case I am declaring that the string of characters <code>zero</code> is hereby defined to be a term (or value) of type <code>Nat</code>. </p>
<p>We could stop here and we'd have a new (inductive) type with a single value, but that wouldn't help us create numbers, which we expect to be indefinite (infinite).</p>
<p>Next, we start a new line beginning with a pipe, and this time instead of declaring a new term of type <code>Nat</code>, we declare the first function that operates on terms of type <code>Nat</code>. We call this function <code>succ</code> (short for successor). We know that <code>succ</code> is a function and not a term because we assign it the type <code>Nat → Nat</code> after the colon. Whenever you see the pattern <em>some type</em> → <em>some type</em>, you're looking at a function type. </p>
<p>Functions are programs that map terms from one type to another (or the same) type. In this case, <code>succ</code> is a function that does not compute anything, in fact it doesn't do anything at all. All we can do with it is <strong><em>apply</em></strong> it.</p>
<div class="highlight"><pre><span></span><span class="o">#</span><span class="n">check</span><span class="w"> </span><span class="kt">Nat</span><span class="o">.</span><span class="n">succ</span><span class="w"> </span><span class="p">(</span><span class="kt">Nat</span><span class="o">.</span><span class="n">succ</span><span class="w"> </span><span class="kt">Nat</span><span class="o">.</span><span class="n">zero</span><span class="p">)</span>
<span class="c1">--- Output: Nat.succ (Nat.succ Nat.zero) : Nat</span>
</pre></div>
<p>As you can see, we apply a function by putting the function name, a space, and then the term (value). To avoid ambiguity we must use parentheses when applying multiple times. Declaring the type <code>Nat</code> creates a local namespace <code>Nat</code> so we must prefix references to the value <code>zero</code> or function <code>succ</code> with <code>Nat.</code> e.g. <code>Nat.zero</code></p>
<p>We can save keystokes by opening the namespace.</p>
<div class="highlight"><pre><span></span><span class="nf">open</span><span class="w"> </span><span class="kt">Nat</span>
<span class="c1">--- Now we can do this</span>
<span class="o">#</span><span class="n">check</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="p">(</span><span class="n">succ</span><span class="w"> </span><span class="n">zero</span><span class="p">)</span>
<span class="c1">--- Output: succ (succ zero) : Nat</span>
</pre></div>
<p>Now we have defined the natural numbers, 0, 1, 2, ... and so on, identified in our new type as <code>zero, succ (zero), succ (succ (zero))</code>. Obviously writing numbers using function application is not as convenient as using our normal numerals 1, 2 etc. There is a way to map numerals to our more verbose natural numbers, but we will wait awhile before doing that.</p>
<p>When I first understood what was going on here in this very simple inductive type, it was quite profound. By declaring this empty function <code>succ</code> and applying it to the only "real" term of type <code>Nat</code>, we get an infinite new set of terms of type <code>Nat</code>. Any string of characters that fits the pattern <code>succ x</code> where <code>x</code> is either <code>zero</code> or also of the pattern <code>succ (succ ... zero )</code> is also of type <code>Nat</code>.</p>
<p>You can think of types as specifiying a pattern of characters, a type-checker as checking whether some expression matches a particular pattern, and a value or term is just an expression that matches a particular type pattern. So <code>succ (succ zero)</code> is of type <code>Nat</code> because that pattern of characters matches the pattern we defined as type <code>Nat</code>.</p>
<p>Let's define our first function on our new <code>Nat</code> type. In Lean, all functions are pure as we discussed earlier, and they are also <em>total</em>. A total function is one where every possible input term gets mapped to an output term. That means for a function of type <code>Nat → Nat</code>, every natural number must get mapped to some output term that is also a natural number. You cannot have input terms that are left undefined. In mathematics, if we treat division as a function, we say that <span class="math">\(\frac{x}{0}\)</span> is <em>undefined</em>. In Lean, that is not acceptable, even <span class="math">\(\frac{x}{0}\)</span> is defined.</p>
<p>Total functions can sometimes be an onerous constraint when using Lean for non-mathematical purposes, especially as you have to prove to Lean that your function is total, so Lean does provide a way to define <em>partial</em> functions, but we will not address that yet.</p>
<p>Here's our first function:</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">natId</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span><span class="w"> </span><span class="n">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">x</span>
</pre></div>
<p>First we define a new function using the <code>def</code> keyword, then the name of our function, in this case we're calling it <code>natId</code>, then we have a colon, which indicates we're going to be assigning a type and after the colon we have the type <code>Nat → Nat</code>. Following that, we have the symbol <code>:=</code> which is an assignment operator, and then we have the body of the function which is <code>fun x : Nat => x</code></p>
<p>This last part is called an anonymous function (or lambda function). An anonymous function is a function expression without giving it a name. As is clear, an anonymous function is declared using the <code>fun</code> keyword, following by an identifier (can be more than one) representing the input, then its type annotation, then the <code>=></code> symbol following by the function body, which in this case just returns the input <code>x</code>, and hence this is defining the identity function that does nothing but return its input unadulterated.</p>
<p>One challenge when getting started with Lean is that Lean has a lot of syntactic sugar, so there are often multiple ways to express the same thing. Here are 3 other ways we could have defined the same identity function:</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">natId2</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span>
<span class="w"> </span><span class="n">fun</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">=></span>
<span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">with</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span>
</pre></div>
<p>And:</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">natId3</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span>
<span class="o">|</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span>
</pre></div>
<p>And:</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">natId4</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span><span class="w"> </span><span class="n">a</span>
</pre></div>
<p>The first of these alternatives also uses an anonymous function but then has a <code>match ... with</code> pattern. As we discussed, inductive types are essentially defined as a set of base terms and then one or more functions that define a pattern for creating other terms of that type using the base terms. So since we construct types by defining base terms and patterns over those base terms, we also define functions on types by deconstructing types into their base terms and patterns over those base terms, and then map each deconstructed pattern into terms of another type.</p>
<p>Notice that the variable <code>a</code> after <code>fun</code> represents the input term and we can name it whatever we want. For multiple input functions we will have to introduce multiple input variables after <code>fun</code>.</p>
<p>Also we can check how Lean actually defines types by using the <code>#print</code> command. Let's check the last of these alternatives for <code>idNat4</code></p>
<div class="highlight"><pre><span></span><span class="o">#</span><span class="n">print</span><span class="w"> </span><span class="n">natId4</span>
<span class="o">/-</span><span class="w"> </span>
<span class="kt">Output:</span><span class="w"> </span>
<span class="nf">def</span><span class="w"> </span><span class="kt">Tutorial</span><span class="o">.</span><span class="n">natId4</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span><span class="w"> </span><span class="n">fun</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span><span class="w"> </span>
<span class="o">-/</span>
</pre></div>
<p>As you can see, even though Lean lets us omit the explicit anonymous function, behind the scenes it is filling in the anonymous function for us.</p>
<p>Okay, moving on. Let's write a simple function that just subtracts one from any natural number.</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">subOne</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="err">→</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span>
<span class="w"> </span><span class="n">fun</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">=></span>
<span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">with</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">zero</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">b</span>
</pre></div>
<p>We define a function called <code>subOne</code> with the type <code>Nat → Nat</code>. We implement the function by assigning it to an anonymous function that takes an input variable <code>a</code> (which must be of type <code>Nat</code> according to the function type signature) and matches it against the patterns that a term of type <code>Nat</code> can have, namely it can either be the base term <code>zero</code> or of the pattern <code>succ b</code> where <code>b</code> is just a placeholder for whatever is inside the <code>succ</code> function. We could have also used <code>a</code> in place of <code>b</code> and Lean is smart enough to figure out what we mean based on the context.</p>
<p>If the input <code>a</code> happens to be <code>zero</code> then we just return <code>zero</code> since natural numbers don't get any lower than <code>zero</code>. If the input <code>a</code> happens to be <code>succ b</code> with <code>b</code> being a term of type <code>Nat</code> then we return <code>b</code>, which effectively removes one application of <code>succ</code> and thus decrements the number by one.</p>
<p>There are no other possible patterns that a term of type <code>Nat</code> could be and since we covered them in our function pattern match, Lean is satisfied our function is total.</p>
<p>We can ask Lean to evaluate our function on the input <code>zero.succ.succ</code> (the number 2) by using the <code>#reduce</code> command.</p>
<div class="highlight"><pre><span></span><span class="o">#</span><span class="n">reduce</span><span class="w"> </span><span class="n">subOne</span><span class="w"> </span><span class="n">zero</span><span class="o">.</span><span class="n">succ</span><span class="o">.</span><span class="n">succ</span>
<span class="c1">--Output: succ zero</span>
</pre></div>
<p>It works, if we subtract one from 2 we get 1. Notice that the expression <code>zero.succ.succ</code> is equivalent to <code>succ (succ zero)</code> but easier to read as it avoids parentheses. Again, this is one challenge in learning Lean; there are many ways to do the same thing. But ultimately these are ways to save keystrokes and improve readability, at the expense of taking longer to learn.</p>
<p>We can also write a function where we explicitly name the inputs and then pattern match on them:</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">subOne</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span>
<span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">with</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">zero</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">b</span>
</pre></div>
<p>In this style we name the inputs and annotate their types and then we give the output type after the last free colon.</p>
<p>Now let's define the addition function on natural numbers.</p>
<div class="highlight"><pre><span></span><span class="nf">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kt">Nat</span><span class="w"> </span><span class="kt">:=</span>
<span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">with</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">a</span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="p">(</span><span class="n">add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">c</span><span class="p">)</span>
</pre></div>
<p>We define our function <code>add</code> to take two inputs named <code>a</code> and <code>b</code> and both are of type <code>Nat</code> so we include them together separated by a space. The output type of our function is also of type <code>Nat</code>. We then match the pattern of input <code>b</code> to define the computation of the function.</p>
<p>If the second input <code>b</code> is zero, then that means we are dealing with <code>a + 0</code> and that obviously just equals <code>a</code>, so we return <code>a</code>. </p>
<p>If <code>b</code> is greater than 0, i.e. of the form <code>succ c</code> where <code>c</code> is another natural number, then we add together <code>a</code> and <code>c</code> (and <code>c = b - 1</code>), then we apply <code>succ</code> to the result, which is the same as adding one.</p>
<p>In other words, we are recursively doing <code>1 + (a + (b - 1))</code>. Because we are in a purely functional programming language, we do not have access to things like <code>for</code> loops or <code>while</code> loops. Any iterative computations must be done using recursive (self-referential) function calls.</p>
<p>When we compute <code>1 + (a + (b - 1))</code>, Lean will then call the <code>add</code> function again, with input <code>a</code> (the same as the original input <code>a</code>), and the second input will be <code>b - 1</code>. It keeps recursively calling itself until <code>b - 1 = 0</code> and then we hit the base case where the second input is <code>0</code> and <code>add</code> just returns the first input <code>a</code>.</p>
<div class="highlight"><pre><span></span><span class="o">#</span><span class="n">reduce</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">zero</span><span class="o">.</span><span class="n">succ</span><span class="w"> </span><span class="n">zero</span><span class="o">.</span><span class="n">succ</span>
<span class="c1">--Output: succ (succ zero)</span>
</pre></div>
<p>As you can see, our function successfully computes <code>1 + 1 = 2</code>. Let's do it by hand to make sure we really understand what is going on.</p>
<p>First,
<code>add zero.succ zero.succ</code> (again, this represents <code>1 + 1</code>)
will pattern match on the second argument <code>b = zero.succ</code>, so it will return <code>succ (add zero.succ zero)</code> since the pattern match will "pull off" a <code>succ</code> from the input <code>b</code>.</p>
<p>So now we're calling <code>add</code> within itself, namely <code>add zero.succ zero</code> (<code>1 + 0</code>). Now again, we pattern match on the second input <code>b = zero</code> and that matches the base case where we just return <code>a</code>. So <code>add zero.succ zero = zero.succ</code>. </p>
<p>Now we substitute that into the expression above, <code>succ (add zero.succ zero)</code>, so we get <code>succ (succ zero)</code>, which is the final answer. So the <code>add</code> function works by recursively decrementing <code>b</code> by 1 while adding 1 to <code>a</code> until <code>b = 0</code>.</p>
<p>In order for functions to be total (as described above), they need to be terminating. Lean has a component called a <strong>termination checker</strong> that makes sure every function you define will terminate in a finite number of steps. It does this by making sure that when you're recursively calling a function that the input arguments are <strong><em>structurally decreasing</em></strong>. In the case of the <code>add</code> function, the second input <code>b</code> will structurally decrease each recursive call of <code>add</code> because a <code>succ</code> is "pulled off" (i.e. <code>b</code> becomes <code>b - 1</code> each call). Once <code>b = zero</code> in the recursive calls then the function terminates.</p>
<p>We'll end this post here, but we have a lot more to learn. In the next post we'll prove our first theorems about the natural numbers and learn a lot more Lean along the way.</p>
<p>PS: My goal with these <em>Learning Lean</em> posts are to assume as few pre-requisites as possible, so please leave a comment or email me if anything needs additional explanation and you meet the pre-requisites of knowing how to program in some language and having a high school math background.</p>
<script type="text/javascript">if (!document.getElementById('mathjaxscript_pelican_#%@#$@#')) {
var align = "center",
indent = "0em",
linebreak = "false";
if (false) {
align = (screen.width < 768) ? "left" : align;
indent = (screen.width < 768) ? "0em" : indent;
linebreak = (screen.width < 768) ? 'true' : linebreak;
}
var mathjaxscript = document.createElement('script');
mathjaxscript.id = 'mathjaxscript_pelican_#%@#$@#';
mathjaxscript.type = 'text/javascript';
mathjaxscript.src = 'https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.3/latest.js?config=TeX-AMS-MML_HTMLorMML';
var configscript = document.createElement('script');
configscript.type = 'text/x-mathjax-config';
configscript[(window.opera ? "innerHTML" : "text")] =
"MathJax.Hub.Config({" +
" config: ['MMLorHTML.js']," +
" TeX: { extensions: ['AMSmath.js','AMSsymbols.js','noErrors.js','noUndefined.js'], equationNumbers: { autoNumber: 'none' } }," +
" jax: ['input/TeX','input/MathML','output/HTML-CSS']," +
" extensions: ['tex2jax.js','mml2jax.js','MathMenu.js','MathZoom.js']," +
" displayAlign: '"+ align +"'," +
" displayIndent: '"+ indent +"'," +
" showMathMenu: true," +
" messageStyle: 'normal'," +
" tex2jax: { " +
" inlineMath: [ ['\\\\(','\\\\)'] ], " +
" displayMath: [ ['$$','$$'] ]," +
" processEscapes: true," +
" preview: 'TeX'," +
" }, " +
" 'HTML-CSS': { " +
" availableFonts: ['STIX', 'TeX']," +
" preferredFont: 'STIX'," +
" styles: { '.MathJax_Display, .MathJax .mo, .MathJax .mi, .MathJax .mn': {color: 'inherit ! important'} }," +
" linebreaks: { automatic: "+ linebreak +", width: '90% container' }," +
" }, " +
"}); " +
"if ('default' !== 'default') {" +
"MathJax.Hub.Register.StartupHook('HTML-CSS Jax Ready',function () {" +
"var VARIANT = MathJax.OutputJax['HTML-CSS'].FONTDATA.VARIANT;" +
"VARIANT['normal'].fonts.unshift('MathJax_default');" +
"VARIANT['bold'].fonts.unshift('MathJax_default-bold');" +
"VARIANT['italic'].fonts.unshift('MathJax_default-italic');" +
"VARIANT['-tex-mathit'].fonts.unshift('MathJax_default-italic');" +
"});" +
"MathJax.Hub.Register.StartupHook('SVG Jax Ready',function () {" +
"var VARIANT = MathJax.OutputJax.SVG.FONTDATA.VARIANT;" +
"VARIANT['normal'].fonts.unshift('MathJax_default');" +
"VARIANT['bold'].fonts.unshift('MathJax_default-bold');" +
"VARIANT['italic'].fonts.unshift('MathJax_default-italic');" +
"VARIANT['-tex-mathit'].fonts.unshift('MathJax_default-italic');" +
"});" +
"}";
(document.body || document.getElementsByTagName('head')[0]).appendChild(configscript);
(document.body || document.getElementsByTagName('head')[0]).appendChild(mathjaxscript);
}
</script>
<div class="clear"></div>
<div class="info">
<a href="http://outlace.com/Lean_part_1.html">posted at 14:35</a>
by Brandon Brown
· <a href="http://outlace.com/category/lean/" rel="tag">Lean</a>
·
<a href="http://outlace.com/tag/lean/" class="tags">Lean</a>
</div>
<div id="disqus_thread"></div>
<script type="text/javascript">
var disqus_shortname = 'outlace';
(function() {
var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true;
dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js';
(document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq);
})();
</script>
<noscript>Please enable JavaScript to view the <a href="https://disqus.com/?ref_noscript" rel="nofollow">comments powered by Disqus.</a></noscript>
</article>
<div class="clear"></div>
<footer>
<p>
<!--- <a href="http://outlace.com/feeds/all.atom.xml" rel="alternate">Atom Feed</a> --->
<a href="mailto:outlacedev@gmail.com"><i class="svg-icon email"></i></a>
<a href="http://github.com/outlace"><i class="svg-icon github"></i></a>
<a href="http://outlace.com/feeds/all.atom.xml"><i class="svg-icon rss"></i></a>
</footer>
</div>
<div class="clear"></div>
</div>
<script type="text/javascript">
var gaJsHost = (("https:" == document.location.protocol) ? "https://ssl." : "http://www.");
document.write(unescape("%3Cscript src='" + gaJsHost + "google-analytics.com/ga.js' type='text/javascript'%3E%3C/script%3E"));
</script>
<script type="text/javascript">
try {
var pageTracker = _gat._getTracker("UA-65814776-1");
pageTracker._trackPageview();
} catch(err) {}</script>
</body>
</html>