lean2/doc/lean/declarations.org

* 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.

** Opaque definitions

Opaque definitions are similar to regular definitions, but they are
only _transparent_ in the module/file where they were defined.  The
idea is to allow us to prove theorems about the opaque definition =C=
in the module where it was defined. In other modules, we can only rely
on these theorems. That is, the actual definition is
hidden/encapsulated, and the module designer is free to change it
without affecting its "customers".

Actually, the opaque definition is only treated as transparent inside of
other opaque definitions/theorems in the same module.

Here is an example

#+BEGIN_SRC lean
    import data.nat
    opaque definition id {A : Type} (a : A) : A := a
    -- The following command is type correct since it is being executed in the
    -- same file where id was defined
    check λ (x : nat) (y : id nat), x = y

    -- The following theorem is also type correct since id is being treated as
    -- transparent only in the proof by reflexivity.
    theorem id_eq {A : Type} (a : A) : id a = a :=
    eq.refl a

    -- The following transparent definition is also type correct. It uses
    -- id but it can be type checked without unfolding id.
    definition id2 {A : Type} (a : A) : A :=
    id a

    -- The following definition is type incorrect. It only type checks if
    -- we unfold id, but it is not allowed because the definition is opaque.
    /-
    definition buggy_def {A : Type} (a : A) : Prop :=
    ∀ (b : id A), a = b
    -/
#+END_SRC

Theorems are always opaque, but we should be able to type check their type
in any module. The following theorem is type incorrect because we need to
unfold the opaque definition =id= to type check it.

#+BEGIN_SRC lean
    import data.unit
    opaque definition id {A : Type} (a : A) : A := a
    /-
    theorem buggy_thm (a : unit) (b : id unit) : a = b :=
    unit.equal a b
    -/
#+END_SRC

In contrast, the following theorem is type correct because =id= is
transparent in this example.

#+BEGIN_SRC lean
  import data.unit
  definition id {A : Type} (a : A) : A := a
  theorem simple (a : unit) (b : id unit) : a = b :=
  unit.equal a b
#+END_SRC

** 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