have

have は，証明の途中でわかることをローカルコンテキストに追加するコマンドです．

have h : P := ... で P という命題の証明を構成し，その証明に h という名前を付けることができます．

import Mathlib.Tactic.Ring -- `ring` のため

variable (P Q R : Prop)

example (hPQ: P → Q) (hQR: Q → R) : P → R := by
  -- 示したいことが `P → R` なので，`P` だと仮定する
  intro hP

  -- 仮定 `hPQ : P → Q` と `hP : P` から `Q` が導かれる
  have hQ : Q := by exact hPQ hP

  -- 仮定 `hQR : Q → R` と `hQ : Q` から `R` が導かれる
  exact hQR hQ

have で示した補題には必ず名前がつきます．名前を省略して have : P := ... とすると，自動的に this という名前になります．無名の補題が欲しい場合，代わりに show を検討してみてください．

また have で同じ名前を2回宣言すると，古い方はアクセス不能になってしまいます．ローカルコンテキストの補題の置き換えを行いたいときは，代わりに replace を使用してください．

無名コンストラクタ

P の証明 hp : P と Q の証明 hq : Q があるとき，P ∧ Q の証明は And.intro hp hq で構成できます．ここで And.intro は構造体 And 型のコンストラクタです．

これを, コンストラクタ名を明示せずにシンプルに ⟨hp, hq⟩ と書くことができます．これは無名コンストラクタと呼ばれるもので，And に限らず任意の構造体に使用することができます．

variable (hp : P) (hq : Q)

def hpq : P ∧ Q := ⟨hp, hq⟩
def hpq' : P ∧ Q := And.intro hp hq

無名コンストラクタを利用することで，記述を簡略化できます．

論理積 ∧

次のように，P ∧ Q という命題から P と Q を取り出すことができます．

example (hPQ : P ∧ Q) : P := by
  -- `P ∧ Q` という仮定を分解する
  -- `hQ : Q` は不要なのでアンダースコアに置き換える
  have ⟨ hP, _ ⟩ := hPQ

  assumption

存在 ∃

次のように，∃ x: X, P x という命題から，条件を満たす x を取り出すことができます．x : X と hx : P x がローカルコンテキストに追加されます．

-- `x`が偶数のとき`3 * x`も偶数
example (x : ℕ) (hx : ∃ y, x = 2 * y) : ∃ z, 3 * x = 2 * z := by
  -- `hx` で存在が主張されている `y` と，
  -- `x = 2 * y` という命題を得る
  have ⟨y, hy⟩ := hx
  exists 3 * y
  rw [hy]
  ring