Merge pull request #1284 from lean-ja/Seasawher/issue276

暗黙の引数 `{x y : A}` を紹介する

LeanByExample/Declarative/Def.lean

@@ -22,7 +22,7 @@ def add (n m : Nat) : Nat := n + m
 
 def threeAdd (n m l : Nat) : Nat := n + m + l
 
-/- ## where 句
+/- ## where 句 { #Where }
 `where` 句を使うと、定義をする前に変数を使用することができます。主に、ヘルパー関数を宣言するために使用されます。
 -/
 
@@ -51,7 +51,7 @@ where
       else
         loop (d + 1) (target / (d ^ m)) ((d, m) :: acc)
 
-/- ## termination_by 句
+/- ## termination_by 句 { #TerminationBy }
 `termination_by` 句は、再帰関数が有限回の再帰で停止することを Lean にわかってもらうために、「再帰のたびに減少する指標」を指定します。
 -/
 -- 何も指定しないと、停止することが Lean にはわからないのでエラーになる

LeanByExample/Declarative/Example.lean

@@ -1,19 +1,12 @@
 /- # example
-`example` は名前を付けずに命題の証明をすることができるコマンドです。
-
-より正確には、`example : T := t` は `t` が型 `T` を持っていることを確かめます。特に `T` の型が `Prop` であるときには、最初に述べた通り `t` は `T` の証明だとみなすことができます。
--/
+`example` は名前を付けずに命題の証明をすることができるコマンドです。 -/
 -- `1 + 1 = 2` は `rfl` で証明できる
 example : 1 + 1 = 2 := rfl
 
--- `rfl` という項の型が `1 + 1 = 2` であると言っても同じこと
-#check (rfl : 1 + 1 = 2)
-
 -- `n + 0 = n` は `rfl` で証明できる
 example {n : Nat} : n + 0 = n := rfl
 
--- `{n : Nat} → n + 0 = n` という依存関数型の項を `rfl` で構成できる、と言い換えられる
-#check (rfl : {n : Nat} → n + 0 = n)
+/- より正確には、`example : T := t` は `t` が型 `T` を持っていることを確かめます。特に `T` の型が [`Prop`](#{root}/Type/Prop.md) であるときには、最初に述べた通り `t` は `T` の証明だとみなすことができます。 -/
 
 -- `[1, 2, 3]` は `List Nat` 型の項
 example : List Nat := [1, 2, 3]

LeanByExample/Diagnostic/Check.lean

@@ -1,97 +1,52 @@
 /- # \#check
 
-`#check` コマンドは、項の型を表示します。Lean ではすべての項に型があるので、どんな項にも使えます。`#check term` というコマンドで、`term` の型を表示します。逆に `term` の型が `T` であることを確かめるには [`example`](../Declarative/Example.md) コマンドを使用して `example : T := term` とします。
+`#check` コマンドは、項の型を表示します。Lean ではすべての項に型があるので、どんな項にも使えます。`#check term` というコマンドで、`term` の型を表示します。-/
 
-## 基本的な項の型 -/
-
--- 文字
+-- 文字 `Char`
 #check 'a'
 
--- 文字列
+-- 文字列 String
 #check "Hello"
 
--- 自然数
+-- 自然数 Nat
 #check 1
 
--- 浮動小数点数
+-- 浮動小数点数 Float
 #check 1.0
 
--- 整数
+-- 整数 Int
 #check -2
 
 -- `1` はそのままだと自然数扱いになるが、整数にキャストできる
 #check (1 : Int)
 
 -- 自然数のリスト
-#check [1, 2, 3]
+#check ([1, 2, 3] : List Nat)
 
 -- 自然数の配列
-#check #[1, 2, 3]
+#check (#[1, 2, 3] : Array Nat)
 
 -- 関数
-#check fun x ↦ x + 42
+#check (fun x ↦ x + 42 : Nat → Nat)
 
--- Bool, 真偽値
+-- 真偽値 Bool
 #check true
 
--- 命題
+-- 命題 Prop
 #check True
 
-/- ## 型の型
-「すべての」項には型があるので、型も型を持ちます。
--/
--- 宇宙変数を宣言する
-universe u
-
-#check (Prop : Type)
-
--- Lean では `List` は Type を受け取って、Type を返す関数。
-#check (List : (α : Type u) → Type u)
+/- 逆に `term` の型が `T` であることを確かめるには [`example`](../Declarative/Example.md) コマンドを使用して `example : T := term` とします。 -/
 
--- 配列も同じ。型を型に変換する関数。
-#check (Array : (α : Type u) → Type u)
+example : Nat := 42
 
--- `Type` 自身も型を持っており…
-#check (Type : Type 1)
-
-#check (Type 1 : Type 2)
-
--- この調子で限りなく続く
-#check (Type u : Type (u + 1))
-
-/- ## 命題と証明
-Lean では命題やその証明にも型があります。命題の型は `Prop` で、命題の項が証明になっています。逆に言えば、Lean ではある命題 `P : Prop` を証明するということは、`P` という型を持つ項 `proof : P` を構成することと同じです。
--/
+example : Int := - 13
 
-#check (1 + 1 = 2 : Prop)
-
--- `1 + 1 = 2` の証明 `two_eq_add_one` を構成
-theorem two_eq_add_one : 2 = 1 + 1 := by rfl
-
--- 証明の型が命題になっている
-#check (two_eq_add_one : 2 = 1 + 1)
-
-/- ## 型としての True/False
-`True` は型としては一点集合であり、
-`False` は型としては空集合です。
--/
-
--- `trivial : True` は `True` 型を持つ項
-#check trivial
-
-/- ## 関数としての証明
-命題 `P → Q` の証明は、`P → Q` という型を持つ項です。
-つまり、`P` の証明 `h : P` に対して `Q` の証明を返す関数です。
+/- ## 型の型
+「すべての」項には型があるので、型も型を持ちます。多くの組み込み型の型は [`Type`](#{root}/Type/Type.md) になっています。
 -/
 
-theorem tautology : True -> True := fun a ↦ a
-
--- 暗黙の変数を明示的にするために `@` を付けた。
--- `tautology : True → True` と出力されるので、
--- `tautology` は `True → True` という関数であることがわかる
-#check (@tautology : True → True)
+-- 文字列型の型は Type
+#check (String : Type)
 
--- 実際に `trivial : True` を「代入」すると
--- `tautology trivial : True` となり、
--- 確かに `True` 型の項が得られていることがわかる。
-#check (tautology trivial : True)
+-- 自然数型の型は Type
+#check (Nat : Type)

LeanByExample/Parser/ImplicitBinder.lean

@@ -0,0 +1,86 @@
+/- # 暗黙の引数
+
+暗黙の引数とは、[`def`](#{root}/Declarative/Def.md) コマンドや [`theorem`](#{root}/Declarative/Theorem.md) コマンド、[`variable`](#{root}/Declarative/Variable.md) コマンドなどが受け取る構文の一つで、関数や定理の引数をユーザが明示的に与えなくても、Lean が文脈を読んで推論してくれるようになります。波括弧 `{}` で囲んで、`{x y : A}` のように書きます。
+
+## 典型的な使用例
+
+たとえば、暗黙の引数を使わなかった場合にどうなるかを見てみましょう。次の関数 `List.subs` は型パラメータ `α : Type` を受け取っていますが、第二引数 `xs : List α` を見れば `α : Type` が何であるかは分かるので、`List.subs` を使用する際に毎回 `α` を指定するのは冗長だと考えられます。
+-/
+import Lean --#
+
+/-- 与えられたリストの部分リストを全て返す(明示的引数バージョン) -/
+def List.subsₑ (α : Type) (xs : List α) : List (List α) :=
+  match xs with
+  | [] => [[]]
+  | x :: xs =>
+    let xss := subsₑ α xs
+    xss ++ xss.map (x :: ·)
+
+-- 型引数 α を明示的に与える必要がある
+#eval List.subsₑ Nat [1, 2]
+
+-- 型引数を与えないと（当然ながら）エラーになってしまう
+#guard_msgs (drop warning) in --#
+#check_failure List.subs [1, 2]
+
+/- 引数 `α` を暗黙の引数として受け取るように変更すれば、Lean が `α : Type` の内容を推論してくれるようになり、`α` を省略できるようになります。-/
+
+/-- 与えられたリストの部分リストを全て返す(暗黙引数バージョン) -/
+def List.subsᵢ {α : Type} (xs : List α) : List (List α) :=
+  match xs with
+  | [] => [[]]
+  | x :: xs =>
+    let xss := subsᵢ xs
+    xss ++ xss.map (x :: ·)
+
+-- 型引数を省略できるようになった
+#eval List.subsᵢ [1, 2]
+
+-- 逆に今度は型引数を与えるとエラーになる
+#guard_msgs (drop warning) in --#
+#check_failure List.subsᵢ Nat [1, 2]
+
+/- ## 明示引数モード
+
+暗黙の引数を受け取るものとして定義された関数や定理に対して、`@` 記号を先頭に付けると全ての暗黙の引数が明示的引数に変化します。
+-/
+
+-- 2 つの暗黙引数を持つ関数
+def List.map' {α β : Type} (f : α → β) : List α → List β
+  | [] => []
+  | x :: xs => f x :: map' f xs
+
+-- 普通は次のように使う
+#check List.map' (fun x => x == 1) [1, 2, 3]
+
+-- `@` 記号を付けると全ての引数が明示的引数に変化
+#check @List.map' Nat Bool (fun x => x == 1) [1, 2, 3]
+
+/- ## 構文についての補足
+
+`Lean.Parser.Term.implicitBinder` というパーサが暗黙引数の構文に対応しています。-/
+
+open Lean Elab Command in
+
+/-- ドキュメントコメントを取得して表示するコマンド -/
+elab "#doc " x:ident : command => do
+  let name ← liftCoreM do realizeGlobalConstNoOverload x
+  if let some s ← findDocString? (← getEnv) name then
+  logInfo m!"{s}"
+
+/--
+info: Implicit binder, like `{x y : A}` or `{x y}`.
+In regular applications, whenever all parameters before it have been specified,
+then a `_` placeholder is automatically inserted for this parameter.
+Implicit parameters should be able to be determined from the other arguments and the return type
+by unification.
+
+In `@` explicit mode, implicit binders behave like explicit binders.
+-/
+#guard_msgs in
+  #doc Lean.Parser.Term.implicitBinder
+
+/- 上記のドキュメントコメントにも書かれていますが、構文としては暗黙の引数に型を指定しないことも許されます。 -/
+
+-- `x : α` と書いたので、`α` が何かの型であることは分かる
+def myId {α} (x : α) := x

LeanByExample/Parser/README.lean

@@ -0,0 +1 @@
+/- # 構文 -/

LeanByExample/Type/Prop.lean

@@ -1,14 +1,34 @@
 /- # Prop
 `Prop` は、命題全体がなす型宇宙です。
 
-命題とは、直観的には「曖昧さなしに真か偽かが定まっているような文章」のことです。`1 + 1 = 2` は命題です。`1 + 1 = 3` も（偽ではありますが）命題です。
+命題とは、直観的には「曖昧さなしに真か偽かが定まっているような文章」のことです。たとえば `1 + 1 = 2` は命題です。`1 + 1 = 3` も（偽ではありますが）命題です。
 -/
 
 #check (1 + 1 = 2 : Prop)
 #check (1 + 1 = 3 : Prop)
 
+/- ## Curry Howard 同型対応
+
+Lean では、各命題 `P : Prop` は再び型になっています。これは通常の数学では考えないことなので慣れないとわかりにくいのですが、言い換えれば命題 `P` の項というものを考えることができます。
+
+たとえば、`1 + 1 = 2` という命題に対して、その項を構成することができます。
+-/
+
+-- `1 + 1 = 2` という型を持つ項を、`rfl` で構成できる
+#check (rfl : 1 + 1 = 2)
+
+-- 項に名前を付けた
+def one_and_one_eq_two : 1 + 1 = 2 := rfl
+
+/- 実は、いま構成した `1 + 1 = 2` という型の項は `1 + 1 = 2` の証明になっています。実際のところ、命題 `P : Prop` の証明とは、Lean においては項 `h : P` そのものです。このことを強調するために、**証明項**という呼び方をすることもあります。-/
+
+-- さっき構成した証明項で証明ができる
+example : 1 + 1 = 2 := one_and_one_eq_two
+
+/- このように命題を型として、証明を項として実装できるのは、そもそも直観主義論理と型付きラムダ計算の間に **Curry Howard 同型対応**が存在するからです。簡単に言えば、論理と計算（プログラム）は出自は全く異なるものの何故か同じ構造を持っており、同じものであると見なせるということです。-/
+
 /- ## 命題論理
-`Bool` には真と偽に対応する `true` と `false` という項がありますが、`Prop` では真偽は `True` と `False` で表されます。
+[`Bool`](#{root}/Type/Bool.md) には真と偽に対応する `true` と `false` という項がありますが、`Prop` では真偽は `True` と `False` で表されます。
 
 `P Q : Prop` があるとき、次のようにして新しい命題を得ることができます。
 

booksrc/SUMMARY.md

@@ -65,6 +65,9 @@
   - [protected: フルネームを強制する](./Modifier/Protected.md)
   - [scoped: 有効範囲を名前空間で限定](./Modifier/Scoped.md)
 
+- [構文](./Parser/README.md)
+  - [`{x y : A}`: 暗黙の引数](./Parser/ImplicitBinder.md)
+
 - [属性](./Attribute/README.md)
   - [app_unexpander: 関数適用の表示](./Attribute/AppUnexpander.md)
   - [cases_eliminator: 独自場合分け](./Attribute/CasesEliminator.md)