import FormalLab.Foundation.TermsAndTypes import FormalLab.Foundation.Functions import FormalLab.Foundation.InductiveTypes import FormalLab.Foundation.UntypedLambdaCalculus import FormalLab.Foundation.Universes import FormalLab.Logic.Propositions import FormalLab.Logic.Connectives import FormalLab.Logic.Quantifiers import FormalLab.Logic.Equality import FormalLab.Logic.ProofSystems /-! # 全問題の解答：基礎と論理 この付録は、各章の全問題に対する解答を章番号と問題番号の順に収録します。問題を読んだ直後は、まず 「ヒント」だけを開いてください。「解答」には、問題が要求する論証、計算、反例またはLeanコードを置きます。 唯一の表現を指定するものではありません。独立して読む価値がある場合に限り、「別解」「反例」「補足」 「発展」などの見出しを加えます。 ## 第1章：型・項・定義・計算 ### 問題1：型判断の構造を復元する #### ヒント コロンの左右だけでなく、判断を成立させる文脈を明示します。加算規則の二つの前提が、同じ型を要求することに 注目してください。 #### 解答 式は形式言語の構文に従う記号列、型は式の使用法を分類する式、項はある型に分類された式です。判断は 「その分類が規則から成立する」という体系上の主張です。`Nat : Type` は型を宇宙へ、`two : Nat` は項を 自然数型へ分類します。文脈を $\Gamma=(n:\mathsf{Nat})$ とすると、変数規則と数値規則から $\Gamma\vdash n:\mathsf{Nat}$ と $\Gamma\vdash1:\mathsf{Nat}$ を得ます。加算規則により $\Gamma\vdash n+1:\mathsf{Nat}$ です。導出木として書けば $$ \frac{\Gamma\vdash n:\mathsf{Nat}\qquad\Gamma\vdash1:\mathsf{Nat}} {\Gamma\vdash n+1:\mathsf{Nat}} $$ となります。横線の上は規則の前提、下はその前提から得る結論です。`true` へ替えると、第二前提 $\Gamma\vdash\mathsf{true}:\mathsf{Nat}$ を作れません。 新しい構文を読むときも、構文、形成規則、導入規則、除去規則を分けます。エラーは「値が変」ではなく、 導出木のどの前提が欠けたかとして診断できます。 ### 問題2：型検査と評価を別の実験として設計する #### ヒント 型検査の出力は型、評価の出力は値です。両方が同じ式を入力にしても、答える問いは異なります。 #### 解答 `def triple (n : Nat) : Nat := n + n + n` と定義します。`#check triple 4` の結果は `triple 4 : Nat`、`#eval triple 4` の結果は `12` です。前者は式を自然数として使用できることを保証しますが、 値が12であるとは述べません。後者は閉じた式を計算しますが、全入力についての定理を証明しません。 `2 : Nat` と `3 : Nat` は同じ型を持ちますが、`2 = 3` は偽です。 #### 補足 抽象的な関数では型検査できても値を表示できない場合があります。その場合も、具体例の評価と一般定理の証明を 混同せず、必要な保証に対応するコマンドを選びます。 ### 問題3：拒否される定義を判断の不成立として診断する #### ヒント 宣言が要求する型と、本体から推論される型を別々に書きます。 #### 解答 `def bad : Nat := true` の期待型は `Nat`、本体 `true` の推論型は `Bool` です。成立させたい判断は `true : Nat` ですが、その導出規則はありません。`def goodBool : Bool := true` は期待型を本体へ合わせます。 `def goodNat : Nat := 0` は本体を期待型へ合わせます。どちらも宣言全体の型整合性を回復します。 関数本体のエラーでも、期待される出力型と各分岐の推論型を表にすると同じ診断ができます。最初に現れた エラー文だけでなく、要求された判断まで戻ることが重要です。 ## 第2章：関数・適用・合成 ### 問題1：合成の向きを型だけから復元する #### ヒント 合成の中央の型が一致するように、右側の関数から入力を流します。 #### 解答 $f:A\to B$ と $g:B\to C$ から作れる合成は $g\circ f:A\to C$ です。入力 $a:A$ をまず $f$ へ渡して $f(a):B$ を得て、それを $g$ へ渡します。逆向きの $f\circ g$ には、一般には $g$ の出力 `C` を $f$ の入力 `A` として使う根拠がありません。Leanの `compose g f x := g (f x)` も同じ順序です。 関手の合成や自然変換の垂直合成でも、中央の始域・終域を照合すれば向きを復元できます。記号の読み順より 先に型を並べます。 ### 問題2：カリー化と部分適用を実装と判断で区別する #### ヒント `A → B → C` を右結合で読み、一引数を与えた後に残る型を書きます。 #### 解答 カリー化された関数の型は $A\to(B\to C)$ です。`multiply : Nat → Nat → Nat` へ `2` を与えると、 `multiply 2 : Nat → Nat` という新しい関数が残ります。これが部分適用です。カリー化は多引数関数を一引数関数の 連鎖として表す変換、部分適用はその表現へ実際に一部の引数を与える操作です。 定理の暗黙引数や型クラス引数も、適用後に残る関数型を見れば同じ方法で追えます。どの引数が既に固定され、 どれがまだ量化されているかを区別します。 ### 問題3：合成の単位則を等式による証明とLean証明で対照する #### ヒント 関数等式を直接示す代わりに、任意の入力へ適用した値を比較します。 #### 解答 任意の $f:A\to B$ と $x:A$ について、$(\mathrm{id}_B\circ f)(x)=\mathrm{id}_B(f(x))=f(x)$ です。 同様に $(f\circ\mathrm{id}_A)(x)=f(\mathrm{id}_A(x))=f(x)$ です。点ごとの等式から関数外延性により $\mathrm{id}_B\circ f=f$ と $f\circ\mathrm{id}_A=f$ が従います。 結合則も三つの関数を任意の入力へ適用し、両辺が `h (g (f x))` へ簡約されることを示せます。 圏論ではこの点ごとの証明が射の単位則・結合則の原型になります。 ## 第3章：帰納型・場合分け・再帰・構造体 ### 問題1：四種類の規則から有限データ型を設計する #### ヒント 値を作る規則、全ての値を使う規則、値を計算へ渡す規則、構成子上の計算規則を分けます。 #### 解答 形成規則は $\mathsf{TrafficLight}:\mathsf{Type}$、導入規則は $\mathsf{red},\mathsf{yellow},\mathsf{green}:\mathsf{TrafficLight}$ です。任意の型 $C$ と $c_r,c_y,c_g:C$ から、全ての $t:\mathsf{TrafficLight}$ に対する値を作れるのが除去規則です。 各構成子へ適用した結果が対応する分岐へ簡約される三式が計算規則になります。 列挙型の構成子を増やす場合も、各構成子に一つの分岐と計算規則を対応させます。再帰的な構成子を加えると、 除去規則には再帰結果または帰納仮定も現れます。 ### 問題2：場合分けと構造再帰を呼出し関係で見分ける #### ヒント 右辺が元の関数を小さい部分構造へ再び呼び出しているかを調べます。 #### 解答 `toggle` は入力の最上位構成子だけを見て値を返すため場合分けです。`factorial (n+1)` は `factorial n` を使い、`listLength (x :: xs)` は `listLength xs` を使うため構造再帰です。 どちらも構成子ごとに分岐しますが、再帰では構成子の引数に含まれる小さいデータへ呼出し辺があります。 木の高さや式の評価器でも、各再帰呼出しが直下の部分木へ向くかを確認します。単に `match` があるかではなく、 呼出し関係で分類します。 ### 問題3：帰納型の無限と余帰納的観察を混同しない #### ヒント 「値の個数が無限」と「一つの値を無限に観察できる」を別の量化として書きます。 #### 解答 自然数型は有限個の構成子 `zero` と `succ` から生成されますが、`succ` を任意の有限回使えるため値の集合は 無限です。ただし各自然数値は有限の構成木です。ストリームは一つの値から先頭と次の状態を何度でも観察でき、 有限構成木として全体を展開し終えません。前者は基数の無限、後者は観察の非終端性です。 無限木や状態機械でも、状態数、生成される有限値の個数、一つの振舞いの観察長を別々に記述します。 ## 第4章：非型付きラムダ計算——束縛・代入・簡約 ### 問題1：名前付き項とde Bruijn添字を往復する #### ヒント 変数名ではなく、その変数を束縛するラムダまで何個の束縛を越えるかを数えます。 #### 解答 $\lambda x.x$ は `lam (var 0)`、$\lambda x.\lambda y.x$ は `lam (lam (var 1))` です。内側で `y` は 直近の束縛なので0、`x` は一つ外側なので1です。逆変換では束縛子へ新しい名前を割り当て、添字0から外側へ 環境を参照します。自由変数は現在の束縛深さ以上の添字として別に管理します。 型変数と項変数を同時に持つ体系では、二種類の束縛深さを分けます。名前を消す目的は捕獲をなくすことではなく、 捕獲回避を添字操作へ変換することです。 ### 問題2：シフトと代入の不変条件を一段ずつ追う #### ヒント ラムダの下へ入るとき、cutoffと代入対象の添字がともに一つ増える理由を追います。 #### 解答 自由変数を持つ項をラムダの下へ移す前に、cutoff以上の添字を1増やします。代入 $[j:=s]t$ でラムダの下へ入る場合は、対象を $j+1$ とし、置換項を `shift s` に替えます。 これにより、外側で自由だった変数が新しい束縛子の `var 0` に誤って捕獲されません。束縛変数はcutoff未満なので シフトされず、同じ束縛先を保ちます。 型代入や文脈への弱化でも、保ちたい不変条件を「各添字が同じ束縛を指す」と書けば、必要なシフト量を導けます。 ### 問題3：簡約規則から評価器の探索方針を分離する #### ヒント どの局所変形が許されるかと、複数の候補からどれを選ぶかを分けます。 #### 解答 β簡約規則は $(\lambda x.t)\,s\to t[x:=s]$ という局所変形を許します。これは項のどこを先に探すかを 指定しません。`contractHead?` は先頭がredexのときだけ縮約する関数です。完全な値呼び評価器なら関数位置、 次に引数を値まで評価し、その後にβ簡約します。名前呼びなら引数を先に評価せず代入します。 書換え系、証明簡約、最適化でも、関係を仕様、探索戦略を実装として分離します。完全性や決定性は別の定理です。 ## 第5章：宇宙階層と宇宙多相 ### 問題1：コロンの連鎖を三つの判断へ戻す #### ヒント `Nat : Type : Type 1` を一つの三項関係として読まず、隣接する二つの判断へ分けます。 #### 解答 第一の判断は `Nat : Type` で、自然数型を宇宙 `Type` の項として分類します。第二の判断は `Type : Type 1` で、その宇宙自身を一段上の宇宙へ分類します。項 `0 : Nat` を加えると、 `0 : Nat`、`Nat : Type`、`Type : Type 1` の三判断になります。`Type : Type` とはしないため、 自己包含に由来する不整合を避けます。 依存型の型を読むときも、項、型、型の属するsortを別の判断へ展開します。エラーが値の型か宇宙制約かを 切り分けられます。 ### 問題2：宇宙変数が一つでは足りない定義を診断する #### ヒント 二つの入力型が同じ宇宙に属する必要が本当にあるかを考えます。 #### 解答 定数関数や合成は、入力型と出力型が異なる宇宙にあっても構成できます。`α : Type u` と `β : Type v` を 一つの `u` に固定すると、定義に不要な同宇宙制約を課します。`polymorphicConstant` では `u` と `v`、 `polymorphicCompose` では `u`,`v`,`w` を独立に量化するのが一般的です。 圏の対象・射や型族でも、独立に選べる層には独立な宇宙変数を置きます。等しさが必要な制約だけを共有します。 ### 問題3：`max` と `imax` を仕様から読み、具体例へ適用する #### ヒント 直積型と依存関数型について、どの成分が `Prop` のとき宇宙が縮むかを比較します。 #### 解答 積 `α × β` は両方のデータを保持するため、`α : Type u` と `β : Type v` から `α × β : Type (max u v)` になります。依存関数型 `(x : α) → β x` の宇宙は通常 `imax u v` です。 終域が `Prop`、すなわち `v=0` のとき、全称命題も `Prop` に留まります。これが `imax u 0 = 0` の役割です。 #### 補足 宇宙式は暗記せず、構成がデータを保持するか、証明だけを要求するかから予測します。予測後にLeanの表示で 制約が解けることを確かめます。 ## 第6章：命題・証明・含意 ### 問題1：命題とその証明を異なるsortの対象として読む #### ヒント `P : Prop` と `p : P` のコロンを別々の分類として読みます。 #### 解答 命題 `P` は `Prop` に属する式であり、証明 `p` は型 `P` に属する項です。従って `P : Prop` は 「Pは命題」、`p : P` は「pはPの証明」という異なる判断です。`Prop : Type` はさらに命題のsortを 上位の宇宙へ分類します。真偽値 `Bool` の値を計算することと、命題型の項を構成することも別です。 存在命題では命題全体、証人、証人が性質を満たす証明を別々に分類します。依存型でも同じ読み方を保ちます。 ### 問題2：tactic状態をラムダ抽象と関数適用へ戻す #### ヒント `intro` が仮定を受け取る関数を作り、`exact` がその本体を与えると読んでください。 #### 解答 目標 `P → P` に対する `intro h` は、証明項 `fun h : P => ?_` を作り、残りの目標を `P` にします。 `exact h` は穴を仮定 `h` で埋めるため、完成項は `fun h : P => h` です。`apply implication` は 関数適用の結果を目標へ合わせ、引数に必要な証明を新しい目標として残します。 #### 補足 複雑なtactic証明でも、各操作をラムダ抽象、構成子適用、場合分けへ戻すと依存関係を説明できます。 ### 問題3：爆発原理の仮定を隠さずに追跡する #### ヒント 任意命題を得るために使う入力が `False` の証明であることを型に残します。 #### 解答 爆発原理は `False → P` であり、無条件に任意の `P` を与える定理ではありません。仮定 `h : False` を受け取れば、`False.elim h : P` を構成できます。矛盾を導いた前段の仮定も文脈に残るため、 結論だけを取り出して体系が自明だと解釈してはいけません。 背理法では、矛盾を作るために古典原理を使ったかも追跡します。爆発原理自体は構成論理でも成立します。 ## 第7章：命題論理と構成的・古典的推論 ### 問題1：導入規則と除去規則から証明の情報流を作る #### ヒント 各結合子について、作るときに必要な情報と、使うときに取り出せる情報を対にします。 #### 解答 `P ∧ Q` の導入は `P` と `Q` の両証明を要求し、除去はどちらの成分も取り出せます。`P ∨ Q` の導入は 左右どちらかの証明とタグを要求し、除去は二つの場合から同じ結論を作ります。`P → Q` の導入は `P` を 仮定して `Q` を作る関数、除去はその関数へ `P` の証明を適用する操作です。情報の作り方と利用法が対応します。 帰納型のAPIや圏論的普遍性でも、構成データと一意な利用原理を同じ二欄へ整理できます。 ### 問題2：分配則を導出木とLeanの場合分けで二重に記述する #### ヒント `P ∧ (Q ∨ R)` の連言を除去した後、選言のタグで場合分けします。 #### 解答 仮定から `p : P` と `qr : Q ∨ R` を得ます。`qr` が左なら `Or.inl ⟨p,q⟩`、右なら `Or.inr ⟨p,r⟩` を返します。従って `P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)` です。導出木では最初に 連言除去、次に選言除去を置き、二分岐の末端で連言導入と選言導入を使います。 逆向きの分配則も、外側の選言で場合分けし、各分岐から共通の `P` と内側の選言を構成します。 ### 問題3：古典原理を使った一点だけを定理の仮定へ抽出する #### ヒント 全体を `Classical` にする代わりに、場合分けに必要な命題の排中律だけを引数にします。 #### 解答 `¬(P ∧ Q) → ¬P ∨ ¬Q` の構成では、`P ∨ ¬P` を仮定に取れば十分です。`¬P` なら右側の結論が直ちに得られ、 `P` なら `Q` を仮定したとき `P ∧ Q` が矛盾するので `¬Q` を得ます。古典性を `emP : P ∨ ¬P` という一引数へ局所化できます。 選択公理や関数外延性でも、使用箇所に必要な原理を明示的な引数として切り出すと、定理の依存範囲を比較できます。 ## 第8章：述語・全称量化・存在量化 ### 問題1：全称量化を依存する関数として追跡する #### ヒント 入力 `x` によって出力型 `p x` が変わる関数として読みます。 #### 解答 `∀ x : α, p x` の証明は、任意の `x : α` を受け取って `p x` の証明を返す依存関数です。 利用時には特定の `a : α` へ適用して `p a` を得ます。`mapForall` は各 `x` で `p x → q x` を持ち、全称証明 `hp` から `fun x => step x (hp x)` を構成します。 依存関数型でも、引数に応じて結果型がどう置換されるかを同じ方法で追います。 ### 問題2：存在証明の証人を保存して性質だけを変換する #### ヒント 存在証明を証人 `x` と証拠 `p x` に分解し、証人はそのまま再利用します。 #### 解答 `∃ x, p x` から `⟨x,hp⟩` を取り出し、仮定 `∀ x, p x → q x` を同じ `x` と `hp` へ適用して `hq : q x` を得ます。返す存在証明は `⟨x,hq⟩ : ∃ x, q x` です。証人を選び直していないため、 変換は性質の証拠だけに作用します。 Σ型の写像でも第一成分を保存して第二成分だけ変換できます。ただし第二成分が計算データか命題の証明かは区別します。 ### 問題3：量化子の順序と限定量化の論理形を反例で固定する #### ヒント 証人が先行する変数を見て選べるかを比較し、二値の最小反例を作ります。 #### 解答 各自然数 `n` を受け取った後なら `m := n + 1` を選べるため、`∀ n, ∃ m, n < m` は真です。 一方、`∃ m, ∀ n, n < m` の証人候補 `m` には `n := m` を返すと `m < m` が必要になり、 反射律に反します。前者の証人は入力へ依存でき、後者では全入力より先に固定される点が違います。 極限の錐や一様連続性でも、対象ごとに選ぶデータと全対象に共通するデータを量化順序から判定します。 #### 別解 二値だけの模型でも差を確認できます。関係 `R(b,n)` を「`b=true` なら `n=0`、`b=false` なら `n=1`」と 定めます。各 `b` を見た後なら証人を選べるので `∀b,∃n,R(b,n)` は成立します。しかし一つの `n` を先に 選ぶと、`true` から `n=0`、`false` から `n=1` が同時に必要となるため `∃n,∀b,R(b,n)` は成立しません。 この最小模型は、量化順序の差が証人の依存可能性そのものであることを示します。 ## 第9章：等式・代入・外延性・一意存在 ### 問題1：等式除去を置き換えの原理として展開する #### ヒント 等式 `x = y` と `x` で成立する性質 `p x` から、`p y` を作ります。 #### 解答 等式除去は `h : x = y` に沿って証明 `px : p x` を輸送し、`p y` を得る原理です。`h` が `rfl` の場合、 始点と終点は同じなので結果は `px` そのものです。一般の `h` は等式帰納法によりこの反射の場合へ還元できます。 関数合同性 `f x = f y` も、性質を「出力が `f x` に等しい」と選ぶ置き換えです。 ベクトルの長さや依存対では、性質の結果型そのものが変わります。通常の書換えも輸送の特殊例として追えます。 ### 問題2：定義的等しさと外延性の役割分担を証明の各段で指す #### ヒント 計算だけで両辺が同じ式になる段階と、関数全体の等式へ持ち上げる段階を分けます。 #### 解答 合成の結合則を任意の `x` へ適用すると、両辺は定義の展開により `h (g (f x))` へ簡約されます。 この点ごとの等式は `rfl` で成立します。しかし関数 `h ∘ (g ∘ f)` と `(h ∘ g) ∘ f` 自体を同一視するには、 「全ての入力で等しい関数は等しい」という関数外延性を使います。計算と外延原理の役割は別です。 自然変換や構造体の等式でも、成分ごとの計算と、成分等式から全体等式を得る外延原理を分離します。 ### 問題3：存在と一意存在が持つ証拠の成分を分解する #### ヒント 一意存在には証人、存在性の証拠、任意の別証人が元の証人に等しい証拠があります。 #### 解答 `∃ x, p x` は `x` と `p x` の二成分です。一意存在はさらに、任意の `y` が `p y` を満たすなら `y = x` であるという一意性を持ちます。述語 `fun x : Nat => x + 1 = 3` では証人を `2` とし、 存在性は `2 + 1 = 3`、一意性は `y + 1 = 3` から `y = 2` を導く証明です。 普遍対象では「媒介射が存在する」と「その射が一意である」を同じ三成分で読みます。後の圏論でそのまま再利用します。 ## 第10章：自然演繹・シーケント計算・証明の正規化 ### 問題1：一つの含意証明を三表現で再構成する #### ヒント `A → A` を、導出木、ラムダ項、シーケントの三つで表し、仮定の導入と利用を対応させます。 #### 解答 自然演繹では `A ⟶ B` と `A` を仮定し、含意除去で `B` を得た後、二回の含意導入によって `⊢ (A ⟶ B) ⟶ A ⟶ B` を得ます。`NaturalDeduction` では二つの `.impIntro`、二つの `.hyp`、 それらを結ぶ `.impElim` が同じ導出木を表します。ラムダ項は `λf. λa. f a` です。 含意合成では二つの含意除去と一つの含意導入が、ラムダ項の二回適用、シーケントのcutへ対応します。 ### 問題2：正規化前後で結論と仮定を保存する #### ヒント 導入直後の除去を縮約し、消えた仮定が代入先で正しく使われるかを確認します。 #### 解答 証明項 `(λx.t) s` は `t[x:=s]` へ簡約されます。型付けで `x:A ⊢ t:B` と `⊢ s:A` があれば、 代入補題により `⊢ t[x:=s]:B` です。従って簡約前後で結論 `B` は保存されます。自由な仮定は代入で 捕獲されず、元の文脈に残ります。正規化は証明可能な結論を変えず、迂回した導入・除去だけを除きます。 プログラムのβ簡約では「結論」を型へ読み替えると保存定理になります。証明正規化と型安全性を同じ代入補題が支えます。 ### 問題3：cutの便利さと除去可能性を区別する #### ヒント 補題を一度証明して再利用する構成と、その補題なしの導出が存在するというメタ定理を分けます。 #### 解答 cut規則は `Γ ⊢ A` と `Δ,A ⊢ B` を合成し、`Γ,Δ ⊢ B` を得ます。中間命題 `A` を補題として使えるため、 導出を構造化するのに便利です。cut除去定理は、cutを使った任意の導出をcutなしの導出へ変換できると述べます。 これはcutが無意味だという主張ではなく、証明可能性を増やさないという保存的な主張です。 補題、局所定義、中間表現を除去できるという定理でも、記述上の有用性と表現力への影響を別々に評価します。 -/ namespace FormalLab.Appendix.Solutions.Chapter001Exercise002 def triple (n : Nat) : Nat := n + n + n #check triple 4 #eval triple 4 example : triple 4 = 12 := rfl end FormalLab.Appendix.Solutions.Chapter001Exercise002 namespace FormalLab.Appendix.Solutions.Chapter001Exercise003 def goodBool : Bool := true def goodNat : Nat := 1 #check goodBool #check goodNat end FormalLab.Appendix.Solutions.Chapter001Exercise003 namespace FormalLab.Appendix.Solutions.Chapter002Exercise002 def multiply : Nat → Nat → Nat := fun left right => left * right def doubleByMultiplication : Nat → Nat := multiply 2 def singleton {α : Type} (x : α) : List α := [x] #check multiply 2 #eval doubleByMultiplication 7 #check singleton true end FormalLab.Appendix.Solutions.Chapter002Exercise002 namespace FormalLab.Appendix.Solutions.Chapter002Exercise003 def identity {α : Type} (x : α) : α := x def compose {α β γ : Type} (g : β → γ) (f : α → β) : α → γ := fun x => g (f x) theorem leftIdentity {α β : Type} (f : α → β) : compose identity f = f := by funext x rfl theorem rightIdentity {α β : Type} (f : α → β) : compose f identity = f := by funext x rfl end FormalLab.Appendix.Solutions.Chapter002Exercise003 namespace FormalLab.Appendix.Solutions.Chapter003Exercise001 inductive TrafficLight where | red | yellow | green deriving DecidableEq def next : TrafficLight → TrafficLight | .red => .green | .green => .yellow | .yellow => .red example : next .red = .green := rfl example : next .green = .yellow := rfl example : next .yellow = .red := rfl end FormalLab.Appendix.Solutions.Chapter003Exercise001 namespace FormalLab.Appendix.Solutions.Chapter003Exercise002 def listLength {α : Type} : List α → Nat | [] => 0 | _ :: tail => listLength tail + 1 #eval listLength [10, 20, 30] end FormalLab.Appendix.Solutions.Chapter003Exercise002 namespace FormalLab.Appendix.Solutions.Chapter004Exercise002 open FormalLab.Foundation.UntypedLambdaCalculus def naiveSubstitute (index : Nat) (replacement : Term) : Term → Term | .var found => if found = index then replacement else .var found | .app function argument => .app (naiveSubstitute index replacement function) (naiveSubstitute index replacement argument) | .lam body => .lam (naiveSubstitute (index + 1) replacement body) example : naiveSubstitute 0 (.var 0) (.lam (.var 1)) = .lam (.var 0) := rfl example : substitute 0 (.var 0) (.lam (.var 1)) = .lam (.var 1) := rfl end FormalLab.Appendix.Solutions.Chapter004Exercise002 namespace FormalLab.Appendix.Solutions.Chapter004Exercise003 open FormalLab.Foundation.UntypedLambdaCalculus def functionFirst? : Term → Option Term | .app (.lam body) argument => some (substitute 0 argument body) | .app function argument => match contractHead? function with | some function' => some (.app function' argument) | none => (contractHead? argument).map (.app function) | _ => none def argumentFirst? : Term → Option Term | .app (.lam body) argument => some (substitute 0 argument body) | .app function argument => match contractHead? argument with | some argument' => some (.app function argument') | none => (contractHead? function).map (fun function' => .app function' argument) | _ => none def twoRedexes : Term := .app (.app identity constant) (.app identity identity) example : functionFirst? twoRedexes = some (.app constant (.app identity identity)) := rfl example : argumentFirst? twoRedexes = some (.app (.app identity constant) identity) := rfl end FormalLab.Appendix.Solutions.Chapter004Exercise003 namespace FormalLab.Appendix.Solutions.Chapter005Exercise001 #check Type #check Type 1 #check Type 2 universe u def universePolymorphicIdentity {α : Type u} (x : α) : α := x #check universePolymorphicIdentity (α := Type) Nat end FormalLab.Appendix.Solutions.Chapter005Exercise001 namespace FormalLab.Appendix.Solutions.Chapter005Exercise002 universe u v w def independentCompose {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) : α → γ := fun x => g (f x) def oneUniverseCompose {α β γ : Type u} (g : β → γ) (f : α → β) : α → γ := fun x => g (f x) #check independentCompose (α := Nat) (β := Type) (γ := Type 1) end FormalLab.Appendix.Solutions.Chapter005Exercise002 namespace FormalLab.Appendix.Solutions.Chapter005Exercise003 universe u v def universeProduct (α : Type u) (β : Type v) : Type (max u v) := α × β def allInUniverse {α : Type u} (p : α → Prop) : Prop := ∀ x, p x #check @universeProduct #check @allInUniverse end FormalLab.Appendix.Solutions.Chapter005Exercise003 namespace FormalLab.Appendix.Solutions.Chapter006Exercise001 theorem proofIrrelevance (P : Prop) (first second : P) : first = second := Subsingleton.elim first second example : (1 : Nat) ≠ 2 := by decide end FormalLab.Appendix.Solutions.Chapter006Exercise001 namespace FormalLab.Appendix.Solutions.Chapter006Exercise002 theorem identityTerm (P : Prop) : P → P := fun proof => proof theorem identityTactic (P : Prop) : P → P := by intro proof exact proof theorem compositionTerm (P Q R : Prop) : (P → Q) → (Q → R) → P → R := fun pq qr p => qr (pq p) theorem compositionTactic (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by intro pq qr p exact qr (pq p) end FormalLab.Appendix.Solutions.Chapter006Exercise002 namespace FormalLab.Appendix.Solutions.Chapter006Exercise003 theorem twoConsequences (P Q : Prop) (contradiction : False) : P ∧ Q := ⟨False.elim contradiction, False.elim contradiction⟩ end FormalLab.Appendix.Solutions.Chapter006Exercise003 namespace FormalLab.Appendix.Solutions.Chapter007Exercise001 theorem keepLeft (P Q : Prop) : P ∧ Q → P ∨ Q := fun conjunction => Or.inl conjunction.left theorem keepRight (P Q : Prop) : P ∧ Q → P ∨ Q := fun conjunction => Or.inr conjunction.right end FormalLab.Appendix.Solutions.Chapter007Exercise001 namespace FormalLab.Appendix.Solutions.Chapter007Exercise002 theorem distribute (P Q R : Prop) : P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) := by rintro ⟨proofP, proofQ | proofR⟩ · exact Or.inl ⟨proofP, proofQ⟩ · exact Or.inr ⟨proofP, proofR⟩ end FormalLab.Appendix.Solutions.Chapter007Exercise002 namespace FormalLab.Appendix.Solutions.Chapter007Exercise003 theorem deMorganFromExcludedMiddle (P Q : Prop) (emP : P ∨ ¬P) : ¬(P ∧ Q) → ¬P ∨ ¬Q := by intro notBoth cases emP with | inl proofP => exact Or.inr (fun proofQ => notBoth ⟨proofP, proofQ⟩) | inr notP => exact Or.inl notP end FormalLab.Appendix.Solutions.Chapter007Exercise003 namespace FormalLab.Appendix.Solutions.Chapter008Exercise001 theorem mapForall {α : Type} (p q : α → Prop) (transform : ∀ x, p x → q x) (allP : ∀ x, p x) : ∀ x, q x := fun x => transform x (allP x) theorem notExistsImpliesForallNot {α : Type} (p : α → Prop) : (¬∃ x, p x) → ∀ x, ¬p x := fun noWitness x proof => noWitness ⟨x, proof⟩ end FormalLab.Appendix.Solutions.Chapter008Exercise001 namespace FormalLab.Appendix.Solutions.Chapter008Exercise002 theorem swapExistsAndTerm {α : Type} (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := fun ⟨x, proofP, proofQ⟩ => ⟨x, proofQ, proofP⟩ theorem swapExistsAndTactic {α : Type} (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by rintro ⟨x, proofP, proofQ⟩ exact ⟨x, proofQ, proofP⟩ end FormalLab.Appendix.Solutions.Chapter008Exercise002 namespace FormalLab.Appendix.Solutions.Chapter008Exercise003 theorem everyNaturalHasLarger : ∀ n : Nat, ∃ m : Nat, n < m := fun n => ⟨n + 1, by omega⟩ theorem noLargestNatural : ¬∃ m : Nat, ∀ n : Nat, n < m := by rintro ⟨m, largest⟩ exact (Nat.lt_irrefl m) (largest m) def splitChoice (b : Bool) (n : Nat) : Prop := (b = true ∧ n = 0) ∨ (b = false ∧ n = 1) theorem pointwiseChoice : ∀ b : Bool, ∃ n : Nat, splitChoice b n := by intro b cases b <;> simp [splitChoice] theorem noUniformChoice : ¬∃ n : Nat, ∀ b : Bool, splitChoice b n := by rintro ⟨n, all⟩ have atTrue := all true have atFalse := all false simp [splitChoice] at atTrue atFalse omega end FormalLab.Appendix.Solutions.Chapter008Exercise003 namespace FormalLab.Appendix.Solutions.Chapter009Exercise001 theorem symmetryByElimination {α : Type} {x y : α} (equal : x = y) : y = x := by cases equal rfl theorem congruenceTwoWays {α β : Type} {x y : α} {f g : α → β} (equalInput : x = y) (equalFunction : f = g) : f x = g y := by cases equalInput cases equalFunction rfl theorem congruenceFunctionsFirst {α β : Type} {x y : α} {f g : α → β} (equalInput : x = y) (equalFunction : f = g) : f x = g y := by cases equalFunction cases equalInput rfl end FormalLab.Appendix.Solutions.Chapter009Exercise001 namespace FormalLab.Appendix.Solutions.Chapter009Exercise002 theorem compositionAssociative {α β γ δ : Type} (h : γ → δ) (g : β → γ) (f : α → β) : (fun x => h (g (f x))) = (fun x => (h ∘ g) (f x)) := by funext x rfl example : (fun _ : Bool => 0) false = (fun _ : Bool => 0) true := rfl example : false ≠ true := by decide end FormalLab.Appendix.Solutions.Chapter009Exercise002 namespace FormalLab.Appendix.Solutions.Chapter009Exercise003 def ExistsExactlyOne {α : Type} (p : α → Prop) : Prop := ∃ x, p x ∧ ∀ y, p y → y = x theorem uniqueSolution : ExistsExactlyOne (fun x : Nat => x + 1 = 3) := by refine ⟨2, by omega, ?_⟩ intro y satisfiesEquation omega end FormalLab.Appendix.Solutions.Chapter009Exercise003 namespace FormalLab.Appendix.Solutions.Chapter010Exercise001 open FormalLab.Logic.ProofSystems def implicationApplication (A B : Formula) : NaturalDeduction [] ((A ⟶ B) ⟶ A ⟶ B) := .impIntro <| .impIntro <| .impElim (.hyp (A := A ⟶ B) (by simp)) (.hyp (A := A) (by simp)) def implicationApplicationTerm : ProofTerm := .lam (.lam (.app (.var 1) (.var 0))) end FormalLab.Appendix.Solutions.Chapter010Exercise001 namespace FormalLab.Appendix.Solutions.Chapter010Exercise002 open FormalLab.Logic.ProofSystems example : contractIntroductionElimination? (.app (.lam (.var 0)) (.var 3)) = some (.var 3) := rfl example : contractIntroductionElimination? (.app (.lam (.lam (.var 1))) (.var 0)) = some (.lam (.var 1)) := rfl end FormalLab.Appendix.Solutions.Chapter010Exercise002 namespace FormalLab.Appendix.Solutions.Chapter010Exercise003 open FormalLab.Logic.ProofSystems def identityWithCut (A : Formula) : Sequent [] (A ⟶ A) := .cut (sequentIdentity A) (.ax (by simp)) def identityWithoutCut (A : Formula) : CutFree [] (A ⟶ A) := .impRight (.ax (by simp)) end FormalLab.Appendix.Solutions.Chapter010Exercise003