93 lines
2.9 KiB
Org Mode
93 lines
2.9 KiB
Org Mode
* Lean declarations
|
|
|
|
** Definitions
|
|
|
|
The command =definition= declares a new constant/function. The identity function is defined as
|
|
|
|
#+BEGIN_SRC lean
|
|
definition id {A : Type} (a : A) : A := a
|
|
#+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. 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
|
|
import data.vector data.nat
|
|
open nat
|
|
check λ (v : vector nat (2+3)) (w : vector nat 5), v = w
|
|
#+END_SRC
|
|
|
|
Similarly, the following definition only type checks because =id= is transparent, and the type checker can establish that
|
|
=nat= and =id nat= are definitionally equal, that is, they are the "same".
|
|
|
|
#+BEGIN_SRC lean
|
|
import data.nat
|
|
definition id {A : Type} (a : A) : A := a
|
|
check λ (x : nat) (y : id nat), x = y
|
|
#+END_SRC
|
|
|
|
** Theorems
|
|
|
|
In Lean, a theorem is just an =opaque= definition. We usually use
|
|
=theorem= for declaring propositions. The idea is that users don't
|
|
really care about the actual proof, only about its existence. As
|
|
described in previous sections, =Prop= (the type of all propositions)
|
|
is _proof irrelevant_. If we had defined =id= using a theorem the
|
|
previous example would produce a typing error because the type checker
|
|
would be unable to unfold =id= and establish that =nat= and =id nat=
|
|
are definitionally equal.
|
|
|
|
** Private definitions and theorems
|
|
|
|
Sometimes it is useful to hide auxiliary definitions and theorems from
|
|
the module interface. The keyword =private= allows us to declare local
|
|
hidden definitions and theorems. A private definition is always
|
|
opaque. The name of a =private= definition is only visible in the
|
|
module/file where it was declared.
|
|
|
|
#+BEGIN_SRC lean
|
|
import data.nat
|
|
open nat
|
|
private definition inc (x : nat) := x + 1
|
|
private theorem inc_eq_succ (x : nat) : succ x = inc x :=
|
|
rfl
|
|
|
|
-- The definition inc and theorem inc_eq_succ are not visible/accessible
|
|
-- in modules that import this one.
|
|
#+END_SRC
|
|
|
|
** Protected definitions and theorems
|
|
|
|
Declarations can be be organized into namespaces. In the previous
|
|
examples, we have been using the namespace =nat=. It contains
|
|
definitions such as =nat.succ= and =nat.add=. The command =open=
|
|
creates the aliases =succ= and =add= to these definitions. An alias
|
|
will not be created for a _protected definition_ unless the user
|
|
explicitly request it.
|
|
|
|
#+BEGIN_SRC lean
|
|
import data.nat
|
|
open nat
|
|
namespace foo
|
|
definition two : nat := 2
|
|
protected definition three : nat := 3
|
|
end foo
|
|
open foo
|
|
check two
|
|
|
|
-- The following command produces a 'unknown identifier' error
|
|
/-
|
|
check three
|
|
-/
|
|
|
|
-- We have to use its fully qualified name to access three
|
|
check foo.three
|
|
|
|
-- If the user explicitly request three, then an alias is created
|
|
open foo (three)
|
|
check three
|
|
#+END_SRC
|