doc(declarations): private, opaque, protected definitions

doc/lean/declarations.org

@@ -0,0 +1,152 @@
+* Lean declarations
+
+** Definitions
+
+The command =definition= declares a new constrant/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 stablish that =2+3= and =5= are "identical". In Lean, 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 followin definition only type checks because =id= is transparent, and the type checker can stablish that
+=nat= and =id Type 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 Type nat), x = y
+#+END_SRC
+
+** Theorems
+
+In Lean, a theorem is just an =opaque= definition. We usually use
+=theorem= for declarating 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 stablish that =nat= and =id Type
+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 Type 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 = 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 a
+
+    -- The following definition is type incorrect. It only type checks if
+    -- we unfold id, but it is not allowed because the definition is transparent.
+    /-
+    definition buggy_def (A : Type) (a : A) : Prop :=
+    ∀ (b : id Type 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 Type 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 Type unit) : a = b :=
+  unit.equal a b
+#+END_SRC
+
+** Private definitions and theorems
+
+Sometimes it is useful to hide auxiliary definitions and theorems form
+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