フィールド記法の説明を「構文」カテゴリに移動させる

LeanByExample/Attribute/InheritDoc.lean

@@ -9,8 +9,6 @@ def greet := "hello"
 -- `greet` のドキュメントコメントを引き継ぐ
 @[inherit_doc greet] abbrev greet' := greet
 
-section
-
 open Lean Elab Command in
 
 /-- ドキュメントコメントを取得して表示するコマンド -/
@@ -19,8 +17,6 @@ elab "#doc " x:ident : command => do
   if let some s ← findDocString? (← getEnv) name then
   logInfo m!"{s}"
 
-end
-
 /-- info: 最初に与えた doc コメント -/
 #guard_msgs in #doc greet'
 

LeanByExample/Declarative/Structure.lean

@@ -29,39 +29,14 @@ example : Point.x origin = 0 := by rfl
 #check (Point.mk : {α : Type} → α → α → Point α)
 
 /- コンストラクタに `mk` 以外の名前を使いたい場合、`::` を使って次のようにします。-/
-namespace Hidden --#
 
-structure Prod (α : Type) (β : Type) where
+structure MyProd (α : Type) (β : Type) where
   gen ::
   fst : α
   snd : β
 
 -- コンストラクタの名前が gen になっている
-#check Prod.gen
-
-end Hidden --#
-/- ## フィールド記法 { #FieldNotation }
-構造体 `S` の項 `s : S` に `x` というフィールドがあるとき、`S.x s` の代わりに `s.x` と書くことができます。これにより、`s : S` におけるフィールド `x` の値を取得することができます。この関数適用を省略して「あたかもフィールドのように」値にアクセスする記法のことを **フィールド記法(field notation)** といいます。
-
-Nim 言語や D 言語における [Uniform Function Call Syntax](https://ja.wikipedia.org/wiki/Uniform_Function_Call_Syntax) に似た仕様です。
--/
-
--- `.x` を付けるだけで値にアクセスできる
-#guard origin.x = 0
-
-/- 構造体のフィールドへのアクセスが典型的な使い方ですが、より一般の型に対してもフィールド記法は使用できます。
-
-名前空間 `T` にある関数 `f` があって、項 `t : T` があったとします。このとき「`f` の `T` 型の非暗黙の引数のうち、最初のものに `x` を代入したもの」を `x.f` で表すことができます。-/
-
-/-- 点が原点かどうか判定する。以下の２点に注意：
-* 名前空間 `Point` の直下に定義されていること
-* `Point α` 型の引数を持つこと
--/
-def Point.isOrigin (p : Point Int) : Bool :=
-  p.x = 0 && p.y = 0
-
--- フィールド記法が使える！
-#guard origin.isOrigin
+#check MyProd.gen
 
 /- ## 項を定義する様々な構文
 構造体の項を定義したい場合、複数の方法があります。波括弧記法が好まれますが、フィールド名が明らかな状況であれば[無名コンストラクタ](#{root}/Parser/AnonymousConstructor.md)を使用することもあります。-/
@@ -139,10 +114,10 @@ def Point'.x {α : Type} (p : Point' α) : α :=
 この `structure` コマンドの代わりに `inductive` コマンドを用いる方法は、定義しようとしている構造体が命題をパラメータに持っているときに必要になります。[`Prop` の Large Elimination が許可されていない](#{root}/Type/Prop.md#NoLargeElim)ことにより、この場合はアクセサ関数が生成できないので `structure` コマンドが使用できず、エラーになります。 -/
 
 -- `w` はデータなので、アクセサ関数が生成できなくてエラーになる
-/-- error: failed to generate projections for 'Prop' structure, field 'w' is not a proof -/
-#guard_msgs in
-  structure Exists'.{v} {α : Sort v} (p : α → Prop) : Prop where
-    intro ::
+/-⋆-//-- error: failed to generate projections for 'Prop' structure, field 'w' is not a proof -/
+#guard_msgs in --#
+structure MyExists.{v} {α : Sort v} (p : α → Prop) : Prop where
+  intro ::
 
-    w : α
-    h : p w
+  w : α
+  h : p w

LeanByExample/Parser/FieldNotation.lean

@@ -0,0 +1,116 @@
+/- # フィールド記法
+
+**フィールド記法(field notation)** とは、大雑把に言えば `T` が `e` の型であるときに、関数適用 `T.f e` を `e.f` と書き表せるという記法のことです。あたかも `f` が `e` のフィールドであるかのように見えるのでこの名前があります。
+
+典型的な例は、[構造体](#{root}/Declarative/Structure.md) `S` の項 `e : S` に対して、構造体のフィールドのアクセサ関数 `S.f` の適用を `e.f` と書けることです。
+-/
+import Lean --#
+
+structure Foo where
+  x : Nat
+  y : String
+
+/-- Foo の項 -/
+def bar : Foo := { x := 0, y := "" }
+
+-- Foo のフィールドのアクセサ関数
+#check Foo.x
+#check Foo.y
+
+-- フィールド記法を使ってアクセスすることができる
+#guard bar.x = Foo.x bar
+#guard bar.y = Foo.y bar
+
+/- ここで `S` は構造体である必要はなく、任意の型で構いません。すなわち任意の型 `S` とその項 `e : S` に対して、`e.f` は `S.f (p := e)` と解釈されます。ただし、ここで `p` は関数 `S.f` の型 `S` を持つような最初の明示的引数です。 -/
+
+/-- 例示のための意味のない帰納型 -/
+inductive S where
+  | fst (n : Nat)
+  | snd (s : String) (n : Nat)
+
+/-- `_x : Unit` という余計な引数を持つ関数 -/
+def S.toNat (_x : Unit) (s : S) : Nat :=
+  match s with
+  | S.fst n => n
+  | S.snd _ n => n
+
+#guard
+  let e : S := S.fst 42
+
+  -- フィールド記法が使える
+  e.toNat () = 42
+
+/- ## 関数型に対して
+
+`e` が関数であるとき、`e.f` は `Function.f (p := e)` に翻訳されます。ただし、ここで `p` は関数 `Function.f` の、関数型を持つような最初の明示的引数です。
+-/
+section
+  variable {α β γ : Type}
+
+  /-- 関数の単射性 -/
+  def Function.injective (f : α → β) : Prop := ∀ {x y}, f x = f y → x = y
+
+  example (f : α → β) (g : β → γ) : (g ∘ f).injective → f.injective := by
+    -- `g ∘ f` が単射だと仮定する。
+    intro h
+
+    -- このとき `f` は単射である。
+    exact show f.injective from by
+      -- なぜなら、仮に `f x = f y` とすると
+      intro x y hg
+
+      -- `(g ∘ f) x = (g ∘ f) y` が成り立っており
+      have : (g ∘ f) x = (g ∘ f) y := by simp [hg]
+
+      -- `g ∘ f` が単射であることから `x = y` が導かれるため。
+      exact h this
+
+end
+/- ## パラメータを取る型に対して
+
+`e` が `T ...` の項であり、かつ関数 `T.f` が存在するとき、`e.f` は `T.f (p := e)` に翻訳されます。ただし、ここで `p` は関数 `T.f` の型 `T ...` を持つような最初の明示的引数です。
+-/
+
+/-- リストの最小値をそのインデックスと共に出力する -/
+def List.minIdx? {α : Type} [LE α] [DecidableLE α] (xs : List α) : Option (Nat × α) :=
+  loop xs 0
+where
+  loop : List α → Nat → Option (Nat × α)
+  | [], _ => none
+  | x :: xs, i =>
+    match loop xs (i + 1) with
+    | none => some (i, x)
+    | some (j, y) =>
+      if x ≤ y then (i, x) else some (j, y)
+
+-- フィールド記法が使用できている
+#guard
+  let e := [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
+  e.minIdx? = some (1, 1)
+
+/- ## 詳細な仕様
+詳細な仕様は、パーサのドキュメントコメントに書かれています。 -/
+
+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: The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
+More precisely,
+* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
+  where `p` is the first explicit parameter of function type
+* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
+  `e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
+* otherwise, if `e` is of a structure type,
+  the above is repeated for every base type of the structure.
+
+The field index notation `e.i`, where `i` is a positive number,
+is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type.
+-/
+#guard_msgs in
+  #doc Lean.Parser.Term.proj

booksrc/SUMMARY.md

@@ -72,6 +72,7 @@
   - [⟨x₁, x₂, ..⟩: 無名コンストラクタ](./Parser/AnonymousConstructor.md)
   - [`{x y : A}`: 暗黙の引数](./Parser/ImplicitBinder.md)
   - [by: タクティクモードに入る](./Parser/By.md)
+  - [e.f: フィールド記法](./Parser/FieldNotation.md)
   - [show .. from: 項の型を明示](./Parser/Show.md)
 
 - [属性](./Attribute/README.md)