<commit_before>#+Title: Theorem Proving in Lean
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]]

* Interacting with Lean

You are now familiar with the fundamentals of dependent type theory,
both as a language for defining mathematical objects and a language
for constructing proofs. The one thing you are missing is a mechanism
for defining new data types. We will fill this gap in the next chapter,
which introduces the notion of an /inductive data type/. But first, in
this chapter, we take a break from the mechanics of type theory to
explore some pragmatic aspects of interacting with Lean.

** Displaying Information
:PROPERTIES:
  :CUSTOM_ID: Displaying_Information
:END:

There are a number of ways in which you can query Lean for information
about its current state and the objects and theorems that are
available in the current context. You have already seen two of the
most common ones, =check= and =eval=. Remember that =check= is often
used in conjunction with the =@= operator, which makes all of the
arguments to a theorem or definition explicit. In addition, you can
use the =print= command to get information about any identifier. If
the identifier denotes a definition or theorem, Lean prints the type
of the symbol, and its definition; if it is a constant or axiom, Lean
indicates that fact, and shows the type.
#+BEGIN_SRC lean
import data.nat

-- examples with equality
check eq
check @eq
check eq.symm
check @eq.symm

print eq.symm

-- examples with and
check and
check and.intro
check @and.intro

-- examples with addition
open nat
check add
check @add
eval add 3 2
print definition add

-- a user-defined function
definition foo {A : Type} (x : A) : A := x

check foo
check @foo
eval foo
eval (foo @nat.zero)
print foo
#+END_SRC

There are other useful =print= commands:
#+BEGIN_SRC text
print notation               : display all notation
print notation <tokens>      : display notation using any of the tokens
print axioms                 : display assumed axioms
print options                : display options set by user or emacs mode
print prefix <namespace>     : display all declarations in the namespace
print coercions              : display all coercions
print coercions <source>     : display only the coercions from <source>
print classes                : display all classes
print instances <class name> : display all instances of the given class
print fields <structure>     : display all "fields" of a structure
#+END_SRC
We will discuss classes, instances, and structures in Chapter [[file:09_Type_Classes.org::#Type_Classes][Type
Classes]]. Here are examples of how the =print= commands are used:
#+BEGIN_SRC lean
import standard algebra.ring
open prod sum int nat algebra

print notation
print notation + * -
print axioms
print options
print prefix nat
print prefix nat.le
print coercions
print coercions num
print classes
print instances ring
print fields ring
#+END_SRC

Another useful command, although the implementation is still
rudimentary at this stage, is the =find decl= command. This can be
used to find theorems whose conclusion matches a given pattern.
The syntax is as follows:
#+BEGIN_SRC text
find_decl <pattern>  [, filter]*
#+END_SRC
where =<pattern>= is an expression with "holes" (underscores),
and a filter is of the form
#+BEGIN_SRC text
+ id  (id is a substring of the declaration)
- id  (id is not a substring of the declaration)
  id  (id is a substring of the declaration)
#+END_SRC
For example:
#+BEGIN_SRC lean
import data.nat
open nat

find_decl ((_ * _) = (_ * _))
find_decl (_ * _) = _, +assoc
find_decl (_ * _) = _, -assoc

find_decl _ < succ _, +imp, -le
#+END_SRC

** Setting Options
:PROPERTIES:
  :CUSTOM_ID: Setting_Options
:END:

Lean maintains a number of internal variables that can be set by users
to control its behavior. The syntax for doing so is as follows:
#+BEGIN_SRC text
set_option <name> <value>
#+END_SRC

One very useful family of options controls the way Lean's /pretty-
printer/ displays terms. The following options take an input of true
or false:
#+BEGIN_SRC text
pp.implicit  : display implicit arguments
pp.universes : display hidden universe parameters
pp.coercions : show coercions
pp.notation  : display output using defined notations
pp.beta      : beta reduce terms before displaying them
#+END_SRC
In Lean, /coercions/ can be inserted automatically to cast an element
of one data type to another, for example, to cast an element of =nat=
to an element of =int=. We will say more about them later in this
chapter. This list is not exhaustive; you can see a complete list by
typing =set_option pp.= and then using tab-completion in the Emacs
mode for Lean, also discussed below.

As an example, the following settings yield much longer output:
#+BEGIN_SRC lean
import data.nat
open nat

set_option pp.implicit true
set_option pp.universes true
set_option pp.notation false
set_option pp.numerals false

check 2 + 2 = 4
eval (λ x, x + 2) = (λ x, x + 3)

set_option pp.beta true
check (λ x, x + 1) 1
#+END_SRC
Pretty printing additional information is often very useful when you
are debugging a proof, or trying to understand a cryptic error
message. Too much information can be overwhelming, though, and Lean's
defaults are generally sufficient for ordinary interactions.

** Using the Library

To use Lean effectively you will inevitably need to make use of
definitions and theorems in the library. Recall that the =import=
command at the beginning of a file imports previously compiled results
from other files, and that importing is transitive; if you import
=foo= and =foo= imports =bar=, then the definitions and theorems from
=bar= are available to you as well. But the act of opening a namespace
--- which provides shorter names, notations, rewrite rules, and more
--- does not carry over. In each file, you need to open the namespaces
you wish to use.

The command =import standard= imports the essential parts of the
standard library, and by now you have seen many of the namespaces you
will need. For exmaple, you should =open nat= for notation when you
are working with the natural numbers, and =open int= when you are
working with the integers. In general, however, it is important for
you to be familiar with the library and its contents, so you know what
theorems, definitions, notations, and resources are available to
you. Below we will see that Lean's Emacs mode can also help you find
things you need, but studying the contents of the library directly is
often unavoidable.
<commit_msg>typo: exmaple --> example<commit_after>#+Title: Theorem Proving in Lean
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]]

* Interacting with Lean

You are now familiar with the fundamentals of dependent type theory,
both as a language for defining mathematical objects and a language
for constructing proofs. The one thing you are missing is a mechanism
for defining new data types. We will fill this gap in the next chapter,
which introduces the notion of an /inductive data type/. But first, in
this chapter, we take a break from the mechanics of type theory to
explore some pragmatic aspects of interacting with Lean.

** Displaying Information
:PROPERTIES:
  :CUSTOM_ID: Displaying_Information
:END:

There are a number of ways in which you can query Lean for information
about its current state and the objects and theorems that are
available in the current context. You have already seen two of the
most common ones, =check= and =eval=. Remember that =check= is often
used in conjunction with the =@= operator, which makes all of the
arguments to a theorem or definition explicit. In addition, you can
use the =print= command to get information about any identifier. If
the identifier denotes a definition or theorem, Lean prints the type
of the symbol, and its definition; if it is a constant or axiom, Lean
indicates that fact, and shows the type.
#+BEGIN_SRC lean
import data.nat

-- examples with equality
check eq
check @eq
check eq.symm
check @eq.symm

print eq.symm

-- examples with and
check and
check and.intro
check @and.intro

-- examples with addition
open nat
check add
check @add
eval add 3 2
print definition add

-- a user-defined function
definition foo {A : Type} (x : A) : A := x

check foo
check @foo
eval foo
eval (foo @nat.zero)
print foo
#+END_SRC

There are other useful =print= commands:
#+BEGIN_SRC text
print notation               : display all notation
print notation <tokens>      : display notation using any of the tokens
print axioms                 : display assumed axioms
print options                : display options set by user or emacs mode
print prefix <namespace>     : display all declarations in the namespace
print coercions              : display all coercions
print coercions <source>     : display only the coercions from <source>
print classes                : display all classes
print instances <class name> : display all instances of the given class
print fields <structure>     : display all "fields" of a structure
#+END_SRC
We will discuss classes, instances, and structures in Chapter [[file:09_Type_Classes.org::#Type_Classes][Type
Classes]]. Here are examples of how the =print= commands are used:
#+BEGIN_SRC lean
import standard algebra.ring
open prod sum int nat algebra

print notation
print notation + * -
print axioms
print options
print prefix nat
print prefix nat.le
print coercions
print coercions num
print classes
print instances ring
print fields ring
#+END_SRC

Another useful command, although the implementation is still
rudimentary at this stage, is the =find decl= command. This can be
used to find theorems whose conclusion matches a given pattern.
The syntax is as follows:
#+BEGIN_SRC text
find_decl <pattern>  [, filter]*
#+END_SRC
where =<pattern>= is an expression with "holes" (underscores),
and a filter is of the form
#+BEGIN_SRC text
+ id  (id is a substring of the declaration)
- id  (id is not a substring of the declaration)
  id  (id is a substring of the declaration)
#+END_SRC
For example:
#+BEGIN_SRC lean
import data.nat
open nat

find_decl ((_ * _) = (_ * _))
find_decl (_ * _) = _, +assoc
find_decl (_ * _) = _, -assoc

find_decl _ < succ _, +imp, -le
#+END_SRC

** Setting Options
:PROPERTIES:
  :CUSTOM_ID: Setting_Options
:END:

Lean maintains a number of internal variables that can be set by users
to control its behavior. The syntax for doing so is as follows:
#+BEGIN_SRC text
set_option <name> <value>
#+END_SRC

One very useful family of options controls the way Lean's /pretty-
printer/ displays terms. The following options take an input of true
or false:
#+BEGIN_SRC text
pp.implicit  : display implicit arguments
pp.universes : display hidden universe parameters
pp.coercions : show coercions
pp.notation  : display output using defined notations
pp.beta      : beta reduce terms before displaying them
#+END_SRC
In Lean, /coercions/ can be inserted automatically to cast an element
of one data type to another, for example, to cast an element of =nat=
to an element of =int=. We will say more about them later in this
chapter. This list is not exhaustive; you can see a complete list by
typing =set_option pp.= and then using tab-completion in the Emacs
mode for Lean, also discussed below.

As an example, the following settings yield much longer output:
#+BEGIN_SRC lean
import data.nat
open nat

set_option pp.implicit true
set_option pp.universes true
set_option pp.notation false
set_option pp.numerals false

check 2 + 2 = 4
eval (λ x, x + 2) = (λ x, x + 3)

set_option pp.beta true
check (λ x, x + 1) 1
#+END_SRC
Pretty printing additional information is often very useful when you
are debugging a proof, or trying to understand a cryptic error
message. Too much information can be overwhelming, though, and Lean's
defaults are generally sufficient for ordinary interactions.

** Using the Library

To use Lean effectively you will inevitably need to make use of
definitions and theorems in the library. Recall that the =import=
command at the beginning of a file imports previously compiled results
from other files, and that importing is transitive; if you import
=foo= and =foo= imports =bar=, then the definitions and theorems from
=bar= are available to you as well. But the act of opening a namespace
--- which provides shorter names, notations, rewrite rules, and more
--- does not carry over. In each file, you need to open the namespaces
you wish to use.

The command =import standard= imports the essential parts of the
standard library, and by now you have seen many of the namespaces you
will need. For example, you should =open nat= for notation when you
are working with the natural numbers, and =open int= when you are
working with the integers. In general, however, it is important for
you to be familiar with the library and its contents, so you know what
theorems, definitions, notations, and resources are available to
you. Below we will see that Lean's Emacs mode can also help you find
things you need, but studying the contents of the library directly is
often unavoidable.

{'fraction_non_alphanumeric': 0.057173513182096874, 'fraction_numerical': 0.0016860821581851624, 'mean_word_length': 4.190533015115354, 'pattern_counts': {'":': 0, '<': 27, '<?xml version=': 0, '>': 26, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1977378', 'n_tokens_mistral': 3614, 'n_tokens_neox': 3451, 'n_words': 1954}