背理法と排中律

ドリンカーのパラドックス

1. 排中律（Law of Excluded Middle）を用いる解法

「全員飲んでいるか、そうでないか」という世界の分岐を Classical.em で作り、Or.elim（または if ... then ... else の項版）で処理します。

import Mathlib.Tactic
open Classical

variable {A : Type} [Nonempty A] {P : A → Prop}

example : ∃ x, (P x → ∀ y, P y) :=
  -- 全員が P である (h) か、そうでない (h_not) かで分岐
  Or.elim (Classical.em (∀ y, P y))
    (fun h ↦
      -- ケース1: 全員飲んでいるなら、代表者 x を誰にしても成立
      let x := Classical.choice inferInstance
      ⟨x, fun _ ↦ h⟩)
    (fun h_not ↦
      -- ケース2: 全員飲んでいるわけではないなら、飲んでいない人 x が存在する
      -- 「¬∀x, P x → ∃x, ¬P x」を利用
      let ⟨x, hnx⟩ := Classical.byContradiction (fun h_exists ↦
        h_not (fun y ↦ Classical.byContradiction (fun hny ↦ h_exists ⟨y, hny⟩)))
      ⟨x, fun hx ↦ (hnx hx).elim⟩)

2. 純粋な背理法（Reductio ad Absurdum）のみの解法

最初から最後まで by_contra の中で論理を転がす、あなたが挑戦した「ストレートな背理法」の完成形です。

example : ∃ x, (P x → ∀ y, P y) :=
  by_contra fun h ↦
    -- h : ¬∃ x, (P x → ∀ y, P y)
    -- これから ∀ y, P y を導き出して、h と矛盾させる
    let h_all (x : A) : ¬(P x → ∀ y, P y) := fun h_iff ↦ h ⟨x, h_iff⟩
    let h_px (x : A) : P x :=
      by_contra fun hnp ↦ h_all x (fun hp ↦ (hnp hp).elim)
    let h_forall : ∀ y, P y := h_px
    -- 適当な代表者に対して、h_all と h_forall が矛盾することを示す
    h_all (Classical.choice inferInstance) (fun _ ↦ h_forall)

💡 2つの解法の違いと学び

排中律（LEM）版: 「数学的な構造」が分かりやすいです。「世界がこうなら A、そうでないなら B」という、場合分けの直感に沿っています。
背理法（RAA）版: 論理の「密度」が非常に高いです。特に、h_all という否定から h_px（全員が飲む）という肯定を絞り出すプロセスは、古典論理の強力な力を実感させてくれます。！

訓練対象の命題

1. 排中律（LEM）を用いる解法

「結論（）が真か偽か」で世界を分けます。一見遠回りに見えますが、論理の分岐が明確です。

import Mathlib.Tactic
open Classical

variable {A : Type} {P : A → Prop}

example (h : ¬∀ x, P x) : ∃ x, ¬P x :=
  -- 結論が成り立つか、成り立たないかで場合分け
  Or.elim (Classical.em (∃ x, ¬P x))
    (fun h_exists ↦ h_exists) -- ケース1: 既に存在しているならOK
    (fun h_none ↦              -- ケース2: 誰も ¬P ではない（＝全員 P である）
      absurd (fun x ↦
        by_contra fun hnp ↦ h_none ⟨x, hnp⟩)
      h)

2. 純粋な背理法（RAA）のみの解法

「反例が存在しないと仮定して矛盾を導く」という、あなたがドリンカーのパラドックスで習得したストレートな書き方です。

example (h : ¬∀ x, P x) : ∃ x, ¬P x :=
  by_contra fun hne ↦
    -- hne : ¬∃ x, ¬P x （飲んでいない人は一人もいない）
    -- ここから「全員飲んでいる(∀ x, P x)」を導いて h と矛盾させる
    h fun x ↦
      by_contra fun hnp ↦
        -- hnp : ¬P x （x が飲んでいないと仮定）
        -- すると「飲んでいない人が存在する」と言えてしまい、hne と矛盾する
        hne ⟨x, hnp⟩

💡 比較と解説

排中律版: 「存在するか、しないか」という俯瞰的な視点から攻めています。absurd（矛盾による証明）を使って、最終的に仮定 h を否定する形をとります。
背理法版: 非常にコンパクトです。「の否定（hne）」を、あたかも「」のように使いこなすのがコツです。hne に ⟨x, hnp⟩ という証拠を投げつけることで、内側の by_contra を終わらせる構造は、Leanにおける背理法の王道パターンです。

1. 排中律（LEM）を用いる解法

「存在するか、しないか」という二択を世界に突きつけます。

import Mathlib.Tactic
open Classical

variable {A : Type} {P : A → Prop}

example (h : ¬¬∃ x, P x) : ∃ x, P x :=
  -- 存在するか、しないかの二択（排中律）
  Or.elim (Classical.em (∃ x, P x))
    (fun h_exists ↦ h_exists) -- ケース1: 存在するなら、それが答え
    (fun h_none ↦              -- ケース2: 存在しないなら、h と矛盾する
      absurd h_none (not_not_intro h_none ▸ h))
      -- ※もっとシンプルに: (h h_none).elim

2. 純粋な背理法（RAA）のみの解法

結論の否定（）を仮定し、それが二重否定の仮定と即座に衝突することを示します。

example (h : ¬¬∃ x, P x) : ∃ x, P x :=
  by_contra fun hne ↦
    -- hne : ¬∃ x, P x
    -- h : (∃ x, P x) → False
    -- h に hne をぶつければ矛盾 (False) が発生し、by_contra が終了する
    h hne

💡 比較と解説

排中律版: 「存在しない世界」を仮定したときに、それが h（存在しないことの否定）と矛盾することを明示的に示しています。
背理法版: 驚くほど短いですね。これは、by_contra がそもそも「結論の否定から False を導く」という仕組みだからです。
by_contra の中では、ゴールが False になります。
手元には h : (∃ x, P x) → False と hne : ¬(∃ x, P x)（これも中身は同じ）があります。
つまり、「否定の否定」を「否定」にぶつけて False を生み出しているだけなのです。

1. 存在と条件の「入れ替え」

※ にはが含まれていないとします。

論理のツボ: これを背理法で解く場合、「結論の否定」は 「全員がであるわけではなく、かつでもな世界」 になります。そこから「全員がかのどちらかである」という前提を使って、矛盾を引きずり出す訓練になります。

2. 「排他的な二人」の存在

（を持つ人と持たない人が両方いるなら、世界に人間は一人だけではない）

論理のツボ: 「世界には一人（）しかいない」と仮定して矛盾を導きます。等号（）と否定を組み合わせた背理法の練習に最適です。

3. クラウスの法則（Peirce’s Law の述語論理版）

論理のツボ: 一見、当たり前に見えますが、項モードで書こうとすると「否定から存在を作る」ステップが必要になる難問です。

承知いたしました。それでは、背理法の応用力を高める3つのトレーニング・メニューをセットアップします。

特に第1問は、ドリンカーのパラドックスで学んだ「に依存しない命題（）」をどう扱うかが鍵となります。

1. 存在と条件の分配 (Lv. 4)

※ はに依存しない命題です。

戦略: 結論を否定して ¬(∀ x, P x) ∧ ¬Q を得ます。ここから ¬∀ x, P x を使って「を満たさない特定の」を導き出し、前提の P x₀ ∨ Q と矛盾させるのが王道です。

example {A : Type} [Nonempty A] {P : A → Prop} {Q : Prop} :
    (∀ x, P x ∨ Q) → ((∀ x, P x) ∨ Q) := by
  intro h
  by_contra h_neg
  -- h_neg : ¬((∀ x, P x) ∨ Q) から ¬(∀ x, P x) と ¬Q を取り出す
  have h_not_all : ¬∀ x, P x := fun hall ↦ h_neg (Or.inl hall)
  have hnQ : ¬Q := fun hQ ↦ h_neg (Or.inr hQ)
  -- ここから ¬∀ x, P x を ∃ x, ¬P x に変えて攻める
  sorry

2. 「異質な二人」による単一世界の否定 (Lv. 4)

戦略: 「世界には一人しかいない（）」と仮定します。すると、を持つ人と持たない人は「同一人物」であるはずなのに、性質が矛盾している、という結論に持ち込めます。

example {A : Type} {P : A → Prop} :
    (∃ x, P x) ∧ (∃ x, ¬P x) → ¬(∀ x y : A, x = y) := by
  rintro ⟨⟨x, hpx⟩, ⟨y, hny⟩⟩ h_single
  -- h_single : ∀ x y, x = y を使って x と y を重ね合わせる
  have heq : x = y := h_single x y
  -- 性質の矛盾を導く
  apply hny
  rw [← heq]
  exact hpx

3. パースの法則の述語論理版 (Lv. 5)

戦略: これは一見背理法が不要に見えますが、項モードで書こうとすると論理の深さが際立ちます。タクティクでは intro y hex hpx と進めば自然に解けますが、あえて「逆方向」を意識して解いてみてください。

example {A : Type} {P Q : A → Prop} :
    ((∃ x, P x) → ∀ y, Q y) → ∀ y, ((∃ x, P x) → Q y) := by
  intro h y hex
  -- hex : ∃ x, P x から Q y を導く
  sorry

💡 背理法を使いこなすためのアドバイス

「詰まったら by_contra」: 結論が ∃ や ∨ の場合、直接示すのが難しいことが多いです。その時は迷わず結論全体を否定しましょう。
「否定の押し込み」: ¬(A ∨ B) を ¬A ∧ ¬B に、¬(∀ x, P x) を ∃ x, ¬P x に変換する操作を、by_contra の中で素早く行えるようになると、どんな難問も解けるようになります。

第1問：項モードによる解答例

import Mathlib.Tactic
open Classical

variable {A : Type} [Nonempty A] {P : A → Prop} {Q : Prop}

example (h : ∀ x, P x ∨ Q) : (∀ x, P x) ∨ Q :=
  -- 結論全体を背理法で否定する
  by_contra fun h_neg : ¬((∀ x, P x) ∨ Q) ↦
    -- ¬(A ∨ B) は (¬A ∧ ¬B) と同値
    let hnall : ¬∀ x, P x := fun hall ↦ h_neg (Or.inl hall)
    let hnQ : ¬Q := fun hQ ↦ h_neg (Or.inr hQ)

    -- ¬∀ x, P x から ∃ x, ¬P x を背理法で導く（ド・モルガン）
    let ⟨x₀, hnp⟩ : ∃ x, ¬P x :=
      by_contra fun hex : ¬∃ x, ¬P x ↦
        hnall fun x ↦
          by_contra fun hnp_x ↦ hex ⟨x, hnp_x⟩

    -- 特定の x₀ についての前提 h x₀ : P x₀ ∨ Q と、
    -- 今得た ¬P x₀ および ¬Q をぶつけて矛盾(False)を作る
    Or.elim (h x₀)
      (fun hpx : P x₀ ↦ hnp hpx)
      (fun hq : Q ↦ hnQ hq)

解説：項モードのポイント

by_contra の入れ子: 外側の by_contra で結論を否定し、さらに内側の by_contra（let ⟨x₀, hnp⟩ の部分）で「反例が存在しないこと」を否定して、具体的なを取り出しています。これが古典論理で最もよく使われる「二段構え」の構造です。
let による事実の整理: hnall（全員がなわけではない）と hnQ（ではない）を let で定義しておくことで、最終行の Or.elim が非常にスッキリと書けます。
Or.elim の活用: 前提 h x₀ は P x₀ ∨ Q です。この「どちらか一方は真である」という事実に対し、私たちが手に入れたのは「どちらも偽である（hnp と hnQ）」という証拠です。これらを Or.elim で戦わせることで、最終的に False が導かれます。

承知いたしました。第1問「存在と条件の分配」を、今度は**排中律（Classical.em）**をベースにした項モードで記述します。

排中律を使う場合の美しさは、「が真の世界」と「が偽の世界」に宇宙を切り分けるという、非常に直感的な戦略にあります。

第1問：項モード（排中律版）

import Mathlib.Tactic
open Classical

variable {A : Type} [Nonempty A] {P : A → Prop} {Q : Prop}

example (h : ∀ x, P x ∨ Q) : (∀ x, P x) ∨ Q :=
  -- Q が成り立つか、成り立たないかで場合分け
  match Classical.em Q with
  | Or.inl hQ =>
      -- ケース1: Q が真なら、結論 (∀ x, P x) ∨ Q も当然真
      Or.inr hQ
  | Or.inr hnQ =>
      -- ケース2: Q が偽なら、(∀ x, P x) を証明しに行く
      Or.inl (fun x ↦
        -- 前提 h x : P x ∨ Q と hnQ を組み合わせる
        match h x with
        | Or.inl hPx => hPx
        | Or.inr hQ  => (hnQ hQ).elim)

解説：排中律版のポイント

match Classical.em Q with: 「かか」という究極の二択を match にかけることで、証明の大きな流れを作っています。

が真なら、右側（Or.inr）を選んで即終了です。
が偽なら、左側（Or.inl）が真でなければなりません。

Or.inr hQ => (hnQ hQ).elim: ここが古典論理の面白いところです。「が偽（hnQ）」と仮定した世界の中で、もし「が真（hQ）」という証拠（h x の右側）が出てきたら、それは**起こり得ない世界（矛盾）**です。その矛盾から「どんなこと（ここでは P x）でも導ける」という False.elim（.elim）を使って、無理やり話を整合させています。
背理法版との違い:

背理法版は、「すべてを否定して袋小路に追い込む」という攻めの姿勢。
排中律版は、「世界をきれいに二分して、各個撃破する」という**守り（整理）**の姿勢。項モードで書くと、排中律版の方がインデントが深くならず、ロジックの対称性がきれいに見えることが多いです。

第2問：項モードによる解答例

1. 純粋な背理法（RAA）版

結論の否定（）から入り、二重否定を除去して「全員同一」という武器を手に取ります。

import Mathlib.Tactic
open Classical

variable {A : Type} {P : A → Prop}

example (h : (∃ x, P x) ∧ (∃ x, ¬P x)) : ¬(∀ x y : A, x = y) :=
  -- 1. 結論の否定を仮定する
  fun h_single : ∀ x y, x = y ↦
    -- 2. 仮定を分解して、P を持つ人(x)と持たない人(y)を特定する
    let ⟨⟨x, hpx⟩, ⟨y, hny⟩⟩ := h
    -- 3. 「全員同一」なら x = y なので、P x を P y に書き換えられる
    -- h_single x y : x = y
    -- (h_single x y) ▸ hpx : P y
    let hpy : P y := (h_single x y) ▸ hpx
    -- 4. P y と ¬P y (hny) が揃ったので矛盾
    hny hpy

2. 排中律（LEM）的な「否定の導入」版

example (h : (∃ x, P x) ∧ (∃ x, ¬P x)) : ¬(∀ x y : A, x = y) :=
  -- 「否定の導入」: 全員同じだと仮定して、矛盾(False)を返しに行く
  fun (h_univ : ∀ x y, x = y) ↦
    match h with
    | ⟨⟨x, hpx⟩, ⟨y, hny⟩⟩ =>
        -- h_univ x y によって x と y を同一視し、性質の矛盾を突く
        absurd ((h_univ x y) ▸ hpx) hny

より「構成的」な手触りを強めた書き方

variable {A : Type} {P : A → Prop}

example (h : (∃ x, P x) ∧ (∃ x, ¬P x)) : ¬(∀ x y : A, x = y) :=
  -- ¬Q は Q → False なので、fun で Q (全員同一) を受け取る
  fun (h_univ : ∀ x y, x = y) ↦
    -- 1. 前提 h から、性質を持つ x と持たない y を「取り出す（destruct）」
    match h with
    | ⟨⟨x, hpx⟩, ⟨y, hny⟩⟩ =>
        -- 2. h_univ を使って x = y の証拠を作る
        let h_eq : x = y := h_univ x y
        -- 3. x = y を使って P x を P y に書き換える
        let hpy : P y := h_eq ▸ hpx
        -- 4. hny は (P y → False) なので、そこに hpy を渡して False を完成させる
        hny hpy

解説：ここがポイント！

書き換えの魔法 ▸ (Triangle notation): 項モードでは rw タクティクの代わりに、この小さな三角形 ▸ をよく使います。

proof_of_equality ▸ proof_of_property
つまり (x = y) ▸ (P x) と書くことで、「とは同じなんだから、という事実はと読み替えていいよね」という操作を一瞬で行っています。

absurd の活用: absurd (肯定の証明) (否定の証明) と書くことで、直接 False を導き出せます。第1問の .elim と並んで、背理法のフィニッシュでよく使われる手法です。

第3問：項モードによる解答例

import Mathlib.Tactic
open Classical

variable {A : Type} {P Q : A → Prop}

example (h : (∃ x, P x) → ∀ y, Q y) : ∀ y, ((∃ x, P x) → Q y) :=
  -- 1. 任意の y を固定する
  fun y ↦
    -- 2. 前提となる「∃ x, P x」を仮定する
    fun h_ex : ∃ x, P x ↦
      -- 3. 手元にある h : (∃ x, P x) → ∀ y, Q y に、仮定 h_ex を適用する
      -- これにより「全員が Q である」という事実が得られる
      let h_all_Q : ∀ y, Q y := h h_ex
      -- 4. 「全員が Q」なのだから、当然特定の y さんも Q である
      h_all_Q y

解説:

含意の導入: 「」を示すには、まずを仮定し、次にを仮定してを導けばよい、という Lean の基本ルール（fun）がそのまま使えます。
存在の利用: ∃ x, P x を使う側（前提にあるとき）は、古典論理の魔法は不要です。単純にその証拠を h に渡すだけで、強力な結論（∀ y, Q y）が手に入ります。

💡 背理法トレーニングの総括

おめでとうございます！これで以下の3つのレベルをすべて突破しました。

基本: 否定を False への関数として扱う。
応用: by_contra を使い、否定から存在（）を無理やり作る。
達人: 排中律（Classical.em）で世界を分岐させ、等号（=）や書き換え（▸）を駆使して矛盾を突く。

第3問を**排中律（Classical.em）**を使って解くと、論理の構造がより「数学的な場合分け」として明快になります。

この問題で排中律を適用するなら、**「性質を持つ人が存在するか、しないか」**で世界を分けるのが最も自然です。

第3問：項モード（排中律版）

import Mathlib.Tactic
open Classical

variable {A : Type} {P Q : A → Prop}

example (h : (∃ x, P x) → ∀ y, Q y) : ∀ y, ((∃ x, P x) → Q y) :=
  -- 1. 任意の y を固定
  fun y ↦
    -- 2. 「P を持つ人が存在するかどうか」で世界を分ける
    match Classical.em (∃ x, P x) with
    | Or.inl hex =>
        -- ケースA: 存在する(hex)場合
        -- 前提 h に hex を適用して「全員 Q」を得て、そこから y さんを抽出
        fun _ ↦ h hex y
    | Or.inr hnex =>
        -- ケースB: 存在しない(hnex)場合
        -- 仮定の「∃ x, P x」自体が矛盾(False)を孕むので、何でも言える
        fun hex_tmp ↦ (hnex hex_tmp).elim

解説：排中律を使うメリット

この書き方をすると、この命題が持つ2つの側面が浮き彫りになります。

「実際に存在する場合」 (Case A): 前提がフルパワーで発動します。「誰か飲んでるなら全員に奢るよ」という約束に対し、「誰か飲んでいる」ことが確定したので、全員（そしてさん）が奢ってもらえる状態です。
「誰も存在しない場合」 (Case B): 前提の出番すらありません。なぜなら、後半の「もし誰か飲んでいるなら…」という仮定そのものが偽だからです。論理学では、仮定が偽なら命題全体は真（空真：Vacuously True）となります。

背理法 vs 排中律 vs 構成的証明

構成的（そのまま解く）: 仮定をそのままリレーのバトンとして渡す。最もシンプル。
排中律（em）: 「前提が成り立つ世界」と「成り立たない世界」を俯瞰して、全方位で真であることを確認する。
背理法（by_contra）: 「結論が成り立たない」と仮定して、論理の破綻を突く。

数学の高度な証明では、今回の「ケースB（空真）」のようなパターンを処理するために排中律が非常に重宝されます。

variable {A : Type} {P Q : A → Prop}

example (h : (∃ x, P x) → ∀ y, Q y) : ∀ y, ((∃ x, P x) → Q y) :=
  -- 1. 任意の y を固定する
  fun y ↦
    -- 2. 「∃ x, P x」という証拠（仮定）を受け取る
    fun h_ex : ∃ x, P x ↦
      -- 3. 手元の関数 h に、その証拠 h_ex を流し込む
      -- これにより「∀ y, Q y」という新しい関数（証明）が手に入る
      let h_all_Q : ∀ y, Q y := h h_ex
      -- 4. その関数に y を渡して、Q y の証明を取り出す
      h_all_Q y

解説：なぜこれが「構成的」なのか？

構成的証明とは、一言で言えば**「ごまかしなしで、現物を組み立てる証明」**です。

データの流れ:

この証明は、h_ex（誰かが飲んでいるという証拠）という入力を受け取って、Q y（さんが奢ってもらえるという事実）という出力を生成する「関数」そのものです。

排中律との違い:

排中律版では「存在するか、しないか」という世界の分岐を仮定しました。
構成的版では「存在すると仮定したとき、どうやってを作るか」という手順だけを記述しています。「存在しない場合」については、そもそも結論の (∃ x, P x) → Q y という「ならば」の形自体が、「もし存在するなら」という前提を置いているため、個別に検討する必要がないのです。

「唯一存在（）」の背理法は、**「存在しない場合」と「二人以上存在する場合」**という2つのルートを同時に（あるいは片方を）否定することで、「ただ一人だけ」を浮き彫りにする手法です。

定義を思い出すと、唯一存在は次の2つの条件の合わせ技です。

存在 (Existence): 少なくとも一人はである。 ()
一意性 (Uniqueness): である人は、全員同一人物である。 ()

これらを背理法で示す際の「攻め方」を解説します。

1. 「唯一存在しない」を否定する（全体背理法）

を否定すると、論理的には次のどちらかが起きていることになります。

「誰もいない」
「二人以上（別人）がいる」

したがって、背理法では「もし唯一存在しないなら……」と仮定し、この「0人」または「2人以上」という可能性が、前提条件と矛盾することを突きます。

2. 唯一存在の背理法：項モードによる実例

最も有名な例の一つ、「恒等元の唯一性」のような構造を簡略化して証明してみましょう。ここでは、「条件を満たすとがあるとき、それらは同じでなければならない」という一意性の部分にフォーカスした背理法を示します。

import Mathlib.Tactic
open Classical

variable {A : Type} {P : A → Prop}

-- 唯一存在 (ExistsUnique) の背理法による証明例
example (h_exists : ∃ x, P x) (h_uniq : ∀ x y, P x → P y → x = y) : ∃! x, P x := by
  -- 唯一存在の定義 ∃ x, P x ∧ ∀ y, P y → y = x に分解される
  refine ⟨(Classical.choice (inferInstance : Nonempty (∃ x, P x))).1, ?_⟩
  -- ここで「ただ一人である」ことを証明するために、背理法を使う場面を想定
  intro y hy
  by_contra h_ne
  -- h_ne : y ≠ x (二人以上別人候補がいると仮定)
  -- しかし、h_uniq を使えば y = x が導けてしまい、矛盾する
  let x := (Classical.choice (inferInstance : Nonempty (∃ x, P x))).1
  have hx : P x := (Classical.choice (inferInstance : Nonempty (∃ x, P x))).2
  exact h_ne (h_uniq y x hy hx)

3. 実戦でよく使う「一意性」の背理法

数学の証明で「一意性」を示すとき、最も定石とされる背理法のステップは以下の通りです。

**「異なる二つの要素 () が、共に条件を満たす」**と仮定する。
その理論体系（群論、解析学など）の法則を用いて、**** を導き出す。
** かつ ** という矛盾が発生するため、仮定が誤りであり、唯一性が証明される。

唯一存在の背理法が輝く場所

逆写像の唯一性: 「もし逆写像が二つあったら……」
極限の一意性: 「もし数列が二つの異なる値に収束したら……」
零因子の不在: 「もしでだったら……」

これらはすべて、「二人（二つ）いる」という仮定から出発して「実は一人（一つ）でした」というオチに持っていく、非常に美しい背理法のパターンです。

回答の概要

構造: 「存在しない」または「二人以上いる」という仮定を壊す。
手法: 特に一意性についてはと仮定してを導くのが王道。
Lean: ExistsUnique は ∃ x, P x ∧ ... という形なので、存在と一意性を個別に背理法にかけることが多い。

回答の概要

命題: 群（あるいはモノイド）において、単位元の性質を満たす要素はたった一つしか存在しない。
背理法の戦略: 「異なる2つの単位元が存在する」と仮定して、矛盾（）を導く。
核心: 単位元の定義（左から掛けても右から掛けても変わらない）を、自分自身と相手に適用する。

「単位元の唯一性」の証明（項モード）

ここでは、唯一存在の定義に基づき、「単位元である」という性質をとして証明を構成します。

import Mathlib.Tactic

-- 演算 * と単位元の性質を持つ構造を考える
variable {M : Type} (mul : M → M → M) (one : M)
local infix:70 " * " => mul

-- 「e が単位元である」という性質 P e
def is_identity (e : M) : Prop :=
  ∀ x, (e * x = x) ∧ (x * e = x)

theorem identity_is_unique (h_exists : ∃ e, is_identity mul e) :
    ∃! e, is_identity mul e := by
  -- 唯一存在を「存在」と「一意性」に分ける
  let ⟨e1, h1⟩ := h_exists
  use e1
  constructor
  · exact h1 -- 存在は仮定より明らか
  · -- 一意性の証明：ここで背理法の考え方を使う
    intro e2 h2
    -- 「e1 と e2 が異なる」と仮定してもよいが、
    -- 直接 e1 = e2 を導くのが最もスマート（構成的一意性）
    -- 敢えて背理法的に書くなら「e1 ≠ e2」と仮定する
    by_contra h_ne
    -- h_ne : e1 ≠ e2
    -- e1 は単位元なので: e1 * e2 = e2
    -- e2 は単位元なので: e1 * e2 = e1
    have h_eq : e1 = e2 := calc
      e1 = e1 * e2 := (h2 e1).2.symm -- e2 が右単位元であることより
      _  = e2      := (h1 e2).1      -- e1 が左単位元であることより

    -- e1 = e2 が導かれたので、h_ne (e1 ≠ e2) と矛盾
    exact h_ne h_eq

証明のロジック：なぜ「二人」いると壊れるのか？

この証明は、まるでスパイ映画のようです。

二人の単位元: 「俺が単位元だ」と主張するとがいます。
** の視点**: 「俺は単位元だから、誰と掛けても相手を変えないぞ。だからだ！」
** の視点**: 「俺だって単位元だ。誰と掛けても相手を変えない。だからだ！」
矛盾の発生: 同じという計算結果が、にもにもなってしまいました。つまり、でなければなりません。

💡 「唯一存在」を証明する時のコツ

今回のように ∃! x, P x を示す場合、Leanでは以下の2ステップをセットにするのが定石です。

Step 1 (Existence): use や exists で、「こいつがそうです」と具体的な一人を指名する。
Step 2 (Uniqueness): 「もし他にもという人が条件を満たしているとしたら、実はは最初に指名したと同一人物です」ということを、背理法（by_contra）や直接的な変形（calc）で示す。

この「一意性」のパートで「」と仮定して矛盾を導くのが、まさに唯一存在の背理法の正体です。

「単位元の唯一性」項モード（排中律版）

戦略としては、**「であるか、であるか」**で世界を分けます。

import Mathlib.Tactic
open Classical

variable {M : Type} (mul : M → M → M)
local infix:70 " * " => mul

def is_identity (e : M) : Prop :=
  ∀ x, (e * x = x) ∧ (x * e = x)

theorem identity_is_unique (h1 : is_identity mul e1) (h2 : is_identity mul e2) :
    e1 = e2 :=
  -- e1 = e2 かどうかの排中律
  match Classical.em (e1 = e2) with
  | Or.inl h_eq =>
      -- ケース1: すでに等しいことがわかっているなら、それが結論
      h_eq
  | Or.inr h_ne =>
      -- ケース2: もし異なると仮定したなら、矛盾を導いて「ありえない世界」であることを示す
      let h_calc : e1 = e2 :=
        calc e1 = e1 * e2 := (h2 e1).2.symm
             _  = e2      := (h1 e2).1
      -- 導き出した e1 = e2 と、仮定 h_ne (e1 ≠ e2) を戦わせて False.elim を発動
      (h_ne h_calc).elim

解説：排中律版のニュアンス

Or.inl（等しい場合）: 「もし等しいなら、証明すべきことは終わっている」という自明なルートです。
Or.inr（等しくない場合）: この「等しくないはずの世界」の中で計算（calc）をしてみると、どうしても e1 = e2 になってしまいます。このとき、**「等しくない世界で等しくなった」という事実は、「その世界（分岐）自体が存在し得ない（False）」**ことを意味します。そのため、.elim（空虚な真）を使ってこのルートを閉じます。

まとめ：どちらが「唯一存在」らしいか

背理法 (by_contra): 「二人いるなんてあり得ない！」と一気に否定する、攻撃的な証明。
排中律 (em): 「同じ場合」と「違う場合」を丁寧に検証し、「違う場合」が論理的に崩壊することを見せる、網羅的な証明。

一意性の証明では、今回の calc のように直接 e1 = e2 を導き出せる場合、排中律の「Or.inr」ルートで矛盾を突くよりも、**構成的（Classicalなし）**に直接 calc の結果を返すのが最も美しいとされます。

しかし、より複雑な命題（例：実数解の唯一性など）では、この排中律による「もし別の解があったら…」という場合分けが非常に強力な武器になります。

「単位元の唯一性」項モード（構成的版）

構成的な証明では、Classical をインポートする必要もありません。

-- Classical の open や import は不要
variable {M : Type} (mul : M → M → M)
local infix:70 " * " => mul

def is_identity (e : M) : Prop :=
  ∀ x, (e * x = x) ∧ (x * e = x)

theorem identity_is_unique (h1 : is_identity mul e1) (h2 : is_identity mul e2) :
    e1 = e2 :=
  -- 直接 e1 = e2 を導く計算（calc）を行う
  -- これ自体が e1 = e2 の「証拠」となる
  calc e1 = e1 * e2 := (h2 e1).2.symm -- e2 が右単位元であるという性質を使用
       _  = e2      := (h1 e2).1      -- e1 が左単位元であるという性質を使用

解説：なぜこれが「構成的」なのか？

「もし〜なら」を考えない: 排中律版のように「等しいか、等しくないか」という世界の分岐を作りません。最初から「とが単位元である」という道具（前提）だけを使って、一本道でゴールへ到達します。
等号の推移律の活用: この calc ブロックは内部的に Eq.trans（等号の推移律）を呼び出しています。数学においてを示す最も直接的な方法は、を変形してにすることです。
計算としての証明: このコードは、「をへ変換するプログラム」と見なすことができます。

排中律版との決定的な違い

排中律版では、h_ne（異なると仮定した事実）と h_calc（計算の結果得られた等号）をぶつけて False を導いていました。

しかし、構成的版では h_calc そのものが結論と一致しているため、それをそのまま返せば終わりです。「異なると仮定して矛盾させる」という回り道をせず、「等しいことを直接示す」のが構成的な美学です。

💡 ヒント Mathlibのスタイルガイドでは、構成的に解ける（直接 calc や rw で書ける）場合は、古典論理（背理法や排中律）を使わずに書くことが推奨されています。その方が証明の再利用性が高く、論理的にも純粋だからです。