michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(doc/lean): typos

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-20 07:44:48 -07:00
parent 0faa48c5b8
commit 7262cce37a
2 changed files with 17 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
doc/lean/declarations.org
View file

@ -2,14 +2,18 @@
** Definitions ** Definitions
The command =definition= declares a new constrant/function. The identity function is defined as The command =definition= declares a new constant/function. The identity function is defined as
#+BEGIN_SRC lean #+BEGIN_SRC lean
definition id (A : Type) (a : A) : A := a definition id (A : Type) (a : A) : A := a
#+END_SRC #+END_SRC
We say definitions are "transparent", because the type checker can unfold them. The following declaration only type checks because =+= is a transparent definition. We say definitions are "transparent", because the type checker can
Otherwise, the type checker would reject the expression =v = w= since it would not be able to stablish that =2+3= and =5= are "identical". In Lean, we say they are _definitionally equal_. unfold them. The following declaration only type checks because =+= is
a transparent definition. Otherwise, the type checker would reject
the expression =v = w= since it would not be able to establish that
=2+3= and =5= are "identical". In type theory, we say they are
_definitionally equal_.
#+BEGIN_SRC lean #+BEGIN_SRC lean
import data.vector data.nat import data.vector data.nat
@ -17,7 +21,7 @@ Otherwise, the type checker would reject the expression =v = w= since it would n
check λ (v : vector nat (2+3)) (w : vector nat 5), v = w check λ (v : vector nat (2+3)) (w : vector nat 5), v = w
#+END_SRC #+END_SRC
Similarly, the followin definition only type checks because =id= is transparent, and the type checker can stablish that Similarly, the following definition only type checks because =id= is transparent, and the type checker can establish that
=nat= and =id Type nat= are definitionally equal, that is, they are the "same". =nat= and =id Type nat= are definitionally equal, that is, they are the "same".
#+BEGIN_SRC lean #+BEGIN_SRC lean
@ -29,12 +33,12 @@ Similarly, the followin definition only type checks because =id= is transparent,
** Theorems ** Theorems
In Lean, a theorem is just an =opaque= definition. We usually use In Lean, a theorem is just an =opaque= definition. We usually use
=theorem= for declarating propositions. The idea is that users don't =theorem= for declaring propositions. The idea is that users don't
really care about the actual proof, only about its existence. As really care about the actual proof, only about its existence. As
described in previous sections, =Prop= (the type of all propositions) described in previous sections, =Prop= (the type of all propositions)
is _proof irrelevant_. If we had defined =id= using a theorem the is _proof irrelevant_. If we had defined =id= using a theorem the
previous example would produce a typing error because the type checker previous example would produce a typing error because the type checker
would be unable to unfold =id= and stablish that =nat= and =id Type would be unable to unfold =id= and establish that =nat= and =id Type
nat= are definitionally equal. nat= are definitionally equal.
** Opaque definitions ** Opaque definitions
@ -70,7 +74,7 @@ Here is an example
id A a id A a
-- The following definition is type incorrect. It only type checks if -- The following definition is type incorrect. It only type checks if
-- we unfold id, but it is not allowed because the definition is transparent. -- we unfold id, but it is not allowed because the definition is opaque.
/- /-
definition buggy_def (A : Type) (a : A) : Prop := definition buggy_def (A : Type) (a : A) : Prop :=
∀ (b : id Type A), a = b ∀ (b : id Type A), a = b
@ -102,7 +106,7 @@ transparent in this example.
** Private definitions and theorems ** Private definitions and theorems
Sometimes it is useful to hide auxiliary definitions and theorems form Sometimes it is useful to hide auxiliary definitions and theorems from
the module interface. The keyword =private= allows us to declare local the module interface. The keyword =private= allows us to declare local
hidden definitions and theorems. A private definition is always hidden definitions and theorems. A private definition is always
opaque. The name of a =private= definition is only visible in the opaque. The name of a =private= definition is only visible in the

10
doc/lean/reducible.org
View file

@ -3,7 +3,7 @@
Lean automation can be configured using different commands and Lean automation can be configured using different commands and
annotations. The =reducible= hint/annotation instructs automation annotations. The =reducible= hint/annotation instructs automation
which declarations can be freely unfolded. One of the main components which declarations can be freely unfolded. One of the main components
of the Lean elaborator is a procedure for solving simulateneous of the Lean elaborator is a procedure for solving simultaneous
higher-order unification constraints. Higher-order unification is a higher-order unification constraints. Higher-order unification is a
undecidable problem. Thus, the procedure implemented in Lean is undecidable problem. Thus, the procedure implemented in Lean is
clearly incomplete, that is, it may fail to find a solution for a set clearly incomplete, that is, it may fail to find a solution for a set
@ -19,9 +19,9 @@ The higher-order unification procedure has to perform case-analysis.
The procedure is essentially implementing a backtracking search. This The procedure is essentially implementing a backtracking search. This
procedure has to decide whether a definition =C= should be unfolded or procedure has to decide whether a definition =C= should be unfolded or
not. Here, we roughly divide this decision in two groups: _simple_ not. Here, we roughly divide this decision in two groups: _simple_
and _complex_. We say a unfolding decision is _simple_ if the and _complex_. We say an unfolding decision is _simple_ if the
procedure does not have to consider an extra case (aka procedure does not have to consider an extra case (aka
case-split). That is, it does not increase the search space. We say a case-split). That is, it does not increase the search space. We say an
unfolding decision is _complex_ if it produces at least one extra unfolding decision is _complex_ if it produces at least one extra
case, and consequently increases the search space. case, and consequently increases the search space.
@ -30,7 +30,7 @@ We write =reducible(C)= to denote that =C= was marked as reducible by the user,
and =irreducible(C)= to denote that =C= was marked as irreducible by the user. and =irreducible(C)= to denote that =C= was marked as irreducible by the user.
Theorems are never unfolded. For a transparent definition =C=, the Theorems are never unfolded. For a transparent definition =C=, the
higher-order unification procedure uses the following decisition tree. higher-order unification procedure uses the following decision tree.
#+BEGIN_SRC #+BEGIN_SRC
if simple unfolding decision then if simple unfolding decision then
@ -88,7 +88,7 @@ modification permanent, and save it in the .olean file.
irreducible [persistent] pr2 irreducible [persistent] pr2
#+END_SRC #+END_SRC
The reducible and irreducible annotations can be removed using the modifer =[none]=. The reducible and irreducible annotations can be removed using the modifier =[none]=.
#+BEGIN_SRC lean #+BEGIN_SRC lean
definition pr2 (A : Type) (a b : A) : A := b definition pr2 (A : Type) (a b : A) : A := b