import FormalLab.Mathematics.Sets import FormalLab.Mathematics.FunctionProperties import FormalLab.Mathematics.Relations import FormalLab.Mathematics.NaturalNumberInduction import FormalLab.Mathematics.Orders import FormalLab.Mathematics.Cardinality /-! # 全問題の解答：集合・関数・数学 ## 第20章：集合を述語として読む ### 問題1：集合演算を論理式へ翻訳する #### ヒント 集合 `A` を所属述語 `x ↦ x∈A` と読み、演算を論理結合子へ一つずつ移します。 #### 解答 `x∈A∩B ↔ x∈A ∧ x∈B`、`x∈A∪B ↔ x∈A ∨ x∈B`、`x∈Aᶜ ↔ ¬x∈A` です。 包含は `A⊆B ↔ ∀x, x∈A→x∈B`、差は `x∈A\B ↔ x∈A∧¬x∈B`、像は `y∈f '' A ↔ ∃x, x∈A∧f x=y`、逆像は `x∈f ⁻¹' B ↔ f x∈B` になります。集合等式は外延性により すべてのxについて所属が同値であることへ還元されます。 添字付き和と共通部分は存在量化と全称量化へ翻訳でき、極限に現れる集合族の記法も読めます。 ### 問題2：外延性が重ねて使われる箇所を追う #### ヒント 関数値が集合である等式では、関数外延性と集合外延性を順に適用します。 #### 解答 例えば `f ⁻¹' (B∩C) = f ⁻¹' B ∩ f ⁻¹' C` は集合外延性で任意のxの所属同値へ移り、定義展開だけで `f x∈B∧C ↔ f x∈B∧f x∈C` となります。一方、写像 `preimage f : Set Y→Set X` 同士の等式を示すなら、 まず関数外延性で任意のBを固定し、次に集合外延性で任意のxを固定します。二つの外延性は異なる型の等号を 一層ずつ観察可能な値へ下ろします。 自然変換の等号でも成分ごとの外延性、さらに関数や集合の外延性という層を順に下ります。 ### 問題3：補集合と古典論理の境目を特定する #### ヒント 補集合の定義自体と、二重否定除去や排中律を必要とする等式を区別します。 #### 解答 `Aᶜ={x|¬x∈A}` は構成的に定義できます。`A∩Aᶜ=∅` と `A⊆(Aᶜ)ᶜ` も矛盾導出だけで証明できます。 逆包含 `(Aᶜ)ᶜ⊆A` は各xについて `¬¬(x∈A)→x∈A` を要求し、一般には古典論理が必要です。 同様に `A∪Aᶜ=U` は所属命題についての排中律です。有限で所属が決定可能な集合なら、その決定手続きから 局所的に証明できます。 位相の閉包や論理の否定を扱うときも、古典的同値を無意識に使わず方向ごとの構成可能性を調べます。 ## 第21章：数学的関数とその性質 ### 問題1：左逆から単射を復元する #### ヒント `g∘f=id` と `f x=f y` をgで写します。 #### 解答 `f:A→B` と `g:B→A` が `∀x, g(f x)=x` を満たすとします。`f x=f y` なら合同性から `g(f x)=g(f y)` です。左逆の等式を両辺へ用いて `x=y` を得るのでfは単射です。逆に単射だけから B全体上の左逆を作るには、像の外の値へ送るAの要素が必要です。Aが空でBが非空なら単射は存在しても `B→A` は存在しません。 右逆から全射を得る双対的証明を書き、逆向きで選択が必要になる条件も比較します。 ### 問題2：像と逆像の量化を比較する #### ヒント 像には原像の証人が必要ですが、逆像は関数適用だけで判定できます。 #### 解答 `y∈f '' A` は `∃x, x∈A∧f x=y` という存在命題です。`x∈f ⁻¹' B` は単に `f x∈B` です。この差から 逆像は共通部分と和の両方を厳密に保存します。像は和を厳密に保存しますが、共通部分について一般には `f '' (A∩C) ⊆ f '' A∩f '' C` だけです。逆包含には、右辺の二つの存在証人を同じにするためfの単射が使えます。 随伴する像と逆像の包含 `f '' A⊆B ↔ A⊆f ⁻¹'B` を量化の変形だけで導きます。 ### 問題3：逆関数を選ぶために必要な仮定を調べる #### ヒント 全射の各値に対する原像の「存在」から、原像を返す一つの「関数」へ移る箇所を見ます。 #### 解答 全射 `∀y,∃x,f x=y` から右逆 `g:B→A` を作るには、各yについて証人xを選びます。依存選択関数 `choose : (∀y,∃x,P y x)→∀y,{x // P y x}` があれば `g y=(choose h y).1` と定義できます。有限型で探索が 可能、または各繊維に標準的な代表があれば選択公理は不要です。全単射の場合は単射性により原像は一意ですが、 存在から関数を抽出する原理は基礎体系に依存します。 商集合の代表元選択や基底選択でも、存在・一意性・計算可能な選択を別々に記録します。 ## 第22章：関係・同値・順序 ### 問題1：対称性と反対称性を反例で分ける #### ヒント 対称性は矢印を反転し、反対称性は両方向の矢印から頂点の一致を結論します。 #### 解答 整数の等差関係 `xRy ↔ x-y` が偶数は対称ですが、0と2が両方向に関係しても等しくないため反対称ではありません。 自然数の通常の順序≤は反対称ですが、`0≤1` に対し `1≤0` は偽なので対称ではありません。等号は両方を満たし、 空関係も両条件を空虚に満たします。性質名ではなく量化式を使えば混同を避けられます。 前順序から同値部分 `x≤y∧y≤x` を商にすると、反対称な半順序が得られる過程を追います。 ### 問題2：関数の核関係を証明する #### ヒント `x∼y ↔ f x=f y` と定義し、等号の三性質を移します。 #### 解答 反射性は `f x=f x`、対称性は `f x=f y` の対称、推移性は `f x=f y` と `f y=f z` の推移から従います。 従って核関係は同値関係です。さらに `x∼y ↔ f x=f y` なので、fは同値類上で一定です。逆に異なる同値類が 同じ像を持てば代表x,yが関係して同じ類になるため、商から像への誘導写像は単射になります。 群準同型の核や型の観察同値を、値ではなく区別不能性を集める同じ構成として比較します。 ### 問題3：同値関係から商へ進む理由を説明する #### ヒント 同値な代表を同じ対象として扱う操作が代表の選び方に依存しない条件を書きます。 #### 解答 同値関係だけでは元xとyは依然として別の値です。商 `A/∼` は同値類を一つの点として扱い、射影 `q:A→A/∼` は `x∼y` を `q x=q y` へ変えます。関数 `f:A→B` が同値類上で一定なら、かつそのときに限り `f= f̄∘q` となる一意な `f̄:A/∼→B` を定められます。この普遍性が、代表元によらない定義と証明を保証します。 余等化子は「二つの写像が同じになる最小の商」として、商の普遍性を圏論へ一般化します。 ## 第23章：自然数の再帰・場合分け・帰納法 ### 問題1：帰納法の四つの役割を分離する #### ヒント 対象の構成、関数の定義、命題の証明、計算規則を別の欄へ置きます。 #### 解答 帰納型宣言は0と後者で自然数を生成します。場合分けは入力が0か後者かを一層だけ観察します。再帰は0での値と、 nおよび再帰結果からn+1での値を与えて関数を定義します。帰納法は命題Pについて `P 0` と `∀n,P n→P(n+1)` から `∀n,P n` を示します。再帰子の計算規則は0と後者で定義がどう簡約するかを定めます。 リストや木でも同じ四分類を使い、データ定義とそれについての証明を混同しないようにします。 #### 補足 三角数のような例では、関数を作る段階は再帰、閉じた公式を示す段階は帰納です。後者の場合には再帰方程式で 左辺を一段計算し、帰納仮定で小さい入力の結果を置換してから算術を閉じます。`induction` と自動算術だけを 眺めず、どの行が構成、計算、帰納仮定の使用に当たるかを分けると、リストや木にも同じ証明設計を移せます。 ### 問題2：再帰計算と帰納証明を同じ構造から読む #### ヒント 加法 `add n m` の再帰式と、`add n 0=n` の帰納証明を0・後者の二行で並べます。 #### 解答 第一引数で再帰する加法を `add 0 m=m`、`add (n+1) m=add n m+1` とします。定理 `add n 0=n` は、0の場合に定義計算で成立します。後者の場合は定義式で `add (n+1) 0=add n 0+1` とし、帰納仮定で右辺を `n+1` にします。計算では再帰結果を値として使い、証明では 同じ小さい入力についての命題を等式書換えとして使います。 証明と計算の融合により、証明付きプログラムや依存消去子が同じ再帰原理から得られることを確認します。 ### 問題3：別の帰納型へ原理を移す #### ヒント 二分木の各構成子に対し、証明すべき場合と得られる帰納仮定を一つずつ用意します。 #### 解答 `Tree A ::= leaf a | node l r` とします。性質Pを全木で示すには、全aについて `P(leaf a)` を示し、全l,rについて `P l` と `P r` から `P(node l r)` を示します。節点数 `size` に対する `size t≥1` は葉で計算し、節点では二つの 帰納仮定と `size(node l r)=1+size l+size r` を使います。再帰位置が二つなので帰納仮定も二つです。 添字付き帰納族では各構成子が到達できる添字も帰納原理へ現れ、不可能な場合を消去できます。 ## 第24章：順序・上限・下限・極大原理 ### 問題1：上限の二条件を別々に検査する #### ヒント 上界であることと、すべての上界以下であることを分け、それぞれ片方だけ満たす候補を作ります。 #### 解答 実数集合 `S=(0,1)` では1は上界で、任意の上界uに対し1≤uなので上限です。2は上界ですが最小ではありません。 0は2以下を含む多くの上界以下ですが、Sの上界ではありません。従って候補sが上限であるには `∀x∈S,x≤s` と `∀u,(∀x∈S,x≤u)→s≤u` の両方が必要です。第二条件だけを「小さい」と読むと対象集合との 接続を失います。 圏論的極限でも錐であることと、任意の錐から一意に因子化することを同じ二段階で検査します。 ### 問題2：最大と極大の差を有限半順序で可視化する #### ヒント 互いに比較不能な二要素を上端に持つV字型の半順序を使います。 #### 解答 集合 `{a,b,c}` に `a notMember member · exact False.elim theorem unionComplement {α : Type} (set : PredSet α) : Union set (Complement set) = Universal := by classical funext x apply propext constructor · exact fun _ => trivial · intro _ exact Classical.em (set x) end FormalLab.Appendix.Solutions.Chapter020Exercise003 namespace FormalLab.Appendix.Solutions.Chapter021Exercise001 open FormalLab.Mathematics.FunctionProperties theorem inverseIsBijective {α β : Type} {f : α → β} {g : β → α} (left : IsLeftInverse g f) (right : IsRightInverse g f) : IsBijective g where injective := by intro x y equal calc x = f (g x) := (right x).symm _ = f (g y) := congrArg f equal _ = y := right y surjective := by intro x exact ⟨f x, left x⟩ end FormalLab.Appendix.Solutions.Chapter021Exercise001 namespace FormalLab.Appendix.Solutions.Chapter021Exercise002 open FormalLab.Mathematics.FunctionProperties open FormalLab.Mathematics.Sets def parity (n : Nat) : Nat := n % 2 example : Image parity (Singleton 3) 1 := by exact ⟨3, rfl, by decide⟩ example : Preimage parity (Singleton 0) 4 := by change 4 % 2 = 0 decide end FormalLab.Appendix.Solutions.Chapter021Exercise002 namespace FormalLab.Appendix.Solutions.Chapter022Exercise002 open FormalLab.Mathematics.FunctionProperties open FormalLab.Mathematics.Relations theorem kernelEquivalence {α β : Type} (f : α → β) : IsEquivalence (Kernel f) where reflexive := fun _ => rfl symmetric := fun _ _ equal => equal.symm transitive := fun _ _ _ first second => first.trans second theorem kernelEqualsEquality {α β : Type} {f : α → β} (injective : IsInjective f) (x y : α) : Kernel f x y ↔ x = y := by constructor · intro sameOutput exact injective sameOutput · intro equal exact congrArg f equal end FormalLab.Appendix.Solutions.Chapter022Exercise002 namespace FormalLab.Appendix.Solutions.Chapter023Exercise001 theorem addZero (n : Nat) : n + 0 = n := rfl theorem zeroAdd (n : Nat) : 0 + n = n := by induction n with | zero => rfl | succ n inductionHypothesis => exact congrArg Nat.succ inductionHypothesis def triangular : Nat → Nat | 0 => 0 | n + 1 => triangular n + (n + 1) theorem twiceTriangular (n : Nat) : 2 * triangular n = n * (n + 1) := by induction n with | zero => rfl | succ n inductionHypothesis => calc 2 * triangular (n + 1) = 2 * triangular n + 2 * (n + 1) := by rw [triangular, Nat.mul_add] _ = n * (n + 1) + 2 * (n + 1) := by rw [inductionHypothesis] _ = (n + 2) * (n + 1) := by rw [Nat.add_mul] _ = (n + 1 + 1) * (n + 1) := by congr 1 _ = (n + 1) * (n + 1 + 1) := Nat.mul_comm _ _ end FormalLab.Appendix.Solutions.Chapter023Exercise001 namespace FormalLab.Appendix.Solutions.Chapter023Exercise002 open FormalLab.Mathematics.NaturalNumberInduction #eval sumTo 3 example (n : Nat) : sumTo (n + 1) = sumTo n + (n + 1) := rfl end FormalLab.Appendix.Solutions.Chapter023Exercise002 namespace FormalLab.Appendix.Solutions.Chapter023Exercise003 inductive Sequence (α : Type) where | nil | cons (head : α) (tail : Sequence α) def Sequence.append : Sequence α → Sequence α → Sequence α | .nil, right => right | .cons head tail, right => .cons head (tail.append right) def Sequence.length : Sequence α → Nat | .nil => 0 | .cons _ tail => tail.length + 1 theorem lengthAppend (left right : Sequence α) : (left.append right).length = left.length + right.length := by induction left with | nil => simp [Sequence.append, Sequence.length] | cons head tail inductionHypothesis => simp only [Sequence.append, Sequence.length] omega end FormalLab.Appendix.Solutions.Chapter023Exercise003 namespace FormalLab.Appendix.Solutions.Chapter024Exercise002 open FormalLab.Mathematics.Relations inductive Fork where | bottom | left | right deriving DecidableEq def ForkLe (first second : Fork) : Prop := first = .bottom ∨ first = second theorem forkPartialOrder : IsPartialOrder ForkLe where reflexive := fun point => Or.inr rfl antisymmetric := by intro first second forward backward rcases forward with atBottom | equal · rcases backward with secondBottom | reverse · exact atBottom.trans secondBottom.symm · exact reverse.symm · exact equal transitive := by intro first second third firstSecond secondThird rcases firstSecond with atBottom | equal · exact Or.inl atBottom · subst second exact secondThird theorem leftAndRightIncomparable : ¬ForkLe .left .right ∧ ¬ForkLe .right .left := by simp [ForkLe] end FormalLab.Appendix.Solutions.Chapter024Exercise002 namespace FormalLab.Appendix.Solutions.Chapter025Exercise001 open FormalLab.Mathematics.Cardinality open FormalLab.Mathematics.FunctionProperties example : IsBijective toEven where injective := toEvenInjective surjective := by intro even exact ⟨fromEven even, toEvenFromEven even⟩ end FormalLab.Appendix.Solutions.Chapter025Exercise001 namespace FormalLab.Appendix.Solutions.Chapter025Exercise002 open FormalLab.Mathematics.Cardinality def table : Fin 3 → Fin 3 → Bool := fun row column => row = column example (row : Fin 3) : diagonal table ≠ table row := diagonalDiffers table row end FormalLab.Appendix.Solutions.Chapter025Exercise002 namespace FormalLab.Appendix.Solutions.Chapter025Exercise003 open FormalLab.Mathematics.FunctionProperties theorem liftBijective : IsBijective (ULift.up : Nat → ULift Nat) where injective := by intro left right equal exact congrArg ULift.down equal surjective := by intro lifted exact ⟨lifted.down, by cases lifted; rfl⟩ end FormalLab.Appendix.Solutions.Chapter025Exercise003