Lean の命題の読み方

この章では，Lean の構文そのものには深入りしません． ただし，証明例を読むために example と theorem の基本形だけ確認しておきます．

example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
  exact hPQ hP

これは，「P と Q を命題とし，hPQ : P → Q と hP : P を仮定すると，Q が証明できる」という意味です． (P Q : Prop) は「P と Q は命題である」という宣言です． (hPQ : P → Q) と (hP : P) は，それぞれ「P → Q の証明」と「P の証明」を仮定として受け取る，という意味です．

読み慣れないうちは，カッコで囲まれた部分をいったん飛ばして，カッコの外にある最後の : Q を「ゴールは Q」と読むとよいです． そのあとで，左から順にカッコ内を「使ってよい変数や仮定」として読み戻します． カッコの中の : は「左の名前が右の型をもつ」という型注釈で，最後の : Q はこの example 全体が示す命題です． := by 以降が証明本体で，by の後では tactic を使ってゴールを解いていきます．

theorem は，証明に名前を付ける点を除けば同じように読めます．

theorem modusPonensExample
    (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
  exact hPQ hP

example は名前のない練習用の定理で，後から参照することは通常しません． theorem modusPonensExample ... と書くと，証明した命題に modusPonensExample という名前が付き，別の場所でその名前を使えるようになります． この章では主に example を使いますが，読み方は theorem と同じです． 詳しいコマンドや型の読み方は Chapter 02 で扱います．