From a15cb32bae8098097cc1c1d4f74d137f6bfd73ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Sep 2014 17:10:27 -0700 Subject: [PATCH] doc(declarations): private, opaque, protected definitions --- doc/lean/declarations.org | 152 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 152 insertions(+) create mode 100644 doc/lean/declarations.org diff --git a/doc/lean/declarations.org b/doc/lean/declarations.org new file mode 100644 index 0000000000..a398e3b112 --- /dev/null +++ b/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