diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 9b28cc9f..b76d75df 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -11,13 +11,11 @@ > 開発に使用する mdbook のバージョンは `0.4.35` に固定してください。`0.4.35` 以外のバージョンではレイアウトが崩れます。 * [mdgen](https://github.com/Seasawher/mdgen) を Lean ファイルから markdown ファイルを生成するために使用しています。 -* [mk_exercise](https://github.com/Seasawher/mk-exercise) を使い、Lean の解答ファイルから演習問題ファイルを生成しています。 ## 開発の流れ * このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に `lake exe cache get` を実行してください。 -* `LeanByExample/Tutorial/Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。 -* 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば mk_exercise の実行と markdown の生成と `mdbook build` が一括実行されます。 +* 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば markdown の生成と `mdbook build` が一括実行されます。 ## ルール diff --git a/.github/workflows/sync.yml b/.github/workflows/sync.yml deleted file mode 100644 index d6032bf8..00000000 --- a/.github/workflows/sync.yml +++ /dev/null @@ -1,46 +0,0 @@ -name: sync exercise and solutions - -concurrency: - group: ${{ github.workflow }}-${{ github.ref }} - cancel-in-progress: true - -on: - pull_request: - branches: - - main - push: - branches: - - main - workflow_dispatch: - -permissions: - contents: write - pages: write - id-token: write - -jobs: - sync_exercise: - runs-on: ubuntu-latest - steps: - - name: checkout - uses: actions/checkout@v4 - with: - ref: ${{ github.event.pull_request.head.ref }} - - - name: Install elan - run: | - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none - echo "$HOME/.elan/bin" >> $GITHUB_PATH - - # ファイル名変更により解答と対応しない演習問題が残ることを避けるため、 - # いったん演習ファイルを全て削除している - - name: run mk_exercise - run: | - rm -r LeanByExample/Tutorial/Exercise - lake exe mk_exercise LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise - - - name: detect diff - id: diff - run: | - git add -N LeanByExample/Tutorial/Exercise - git diff --name-only --exit-code diff --git a/LeanByExample/Reference/Attribute/AppUnexpander.lean b/LeanByExample/Attribute/AppUnexpander.lean similarity index 100% rename from LeanByExample/Reference/Attribute/AppUnexpander.lean rename to LeanByExample/Attribute/AppUnexpander.lean diff --git a/LeanByExample/Reference/Attribute/CasesEliminator.lean b/LeanByExample/Attribute/CasesEliminator.lean similarity index 100% rename from LeanByExample/Reference/Attribute/CasesEliminator.lean rename to LeanByExample/Attribute/CasesEliminator.lean diff --git a/LeanByExample/Reference/Attribute/Coe.lean b/LeanByExample/Attribute/Coe.lean similarity index 100% rename from LeanByExample/Reference/Attribute/Coe.lean rename to LeanByExample/Attribute/Coe.lean diff --git a/LeanByExample/Reference/Attribute/Csimp.lean b/LeanByExample/Attribute/Csimp.lean similarity index 100% rename from LeanByExample/Reference/Attribute/Csimp.lean rename to LeanByExample/Attribute/Csimp.lean diff --git a/LeanByExample/Reference/Attribute/DefaultInstance.lean b/LeanByExample/Attribute/DefaultInstance.lean similarity index 100% rename from LeanByExample/Reference/Attribute/DefaultInstance.lean rename to LeanByExample/Attribute/DefaultInstance.lean diff --git a/LeanByExample/Reference/Attribute/InductionEliminator.lean b/LeanByExample/Attribute/InductionEliminator.lean similarity index 100% rename from LeanByExample/Reference/Attribute/InductionEliminator.lean rename to LeanByExample/Attribute/InductionEliminator.lean diff --git a/LeanByExample/Reference/Attribute/InheritDoc.lean b/LeanByExample/Attribute/InheritDoc.lean similarity index 100% rename from LeanByExample/Reference/Attribute/InheritDoc.lean rename to LeanByExample/Attribute/InheritDoc.lean diff --git a/LeanByExample/Reference/Attribute/MacroInline.lean b/LeanByExample/Attribute/MacroInline.lean similarity index 100% rename from LeanByExample/Reference/Attribute/MacroInline.lean rename to LeanByExample/Attribute/MacroInline.lean diff --git a/LeanByExample/Reference/Attribute/MatchPattern.lean b/LeanByExample/Attribute/MatchPattern.lean similarity index 100% rename from LeanByExample/Reference/Attribute/MatchPattern.lean rename to LeanByExample/Attribute/MatchPattern.lean diff --git a/LeanByExample/Reference/Attribute/README.lean b/LeanByExample/Attribute/README.lean similarity index 100% rename from LeanByExample/Reference/Attribute/README.lean rename to LeanByExample/Attribute/README.lean diff --git a/LeanByExample/Reference/Attribute/Simps.lean b/LeanByExample/Attribute/Simps.lean similarity index 100% rename from LeanByExample/Reference/Attribute/Simps.lean rename to LeanByExample/Attribute/Simps.lean diff --git a/LeanByExample/Reference/Declarative/Abbrev.lean b/LeanByExample/Declarative/Abbrev.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Abbrev.lean rename to LeanByExample/Declarative/Abbrev.lean diff --git a/LeanByExample/Reference/Declarative/AddAesopRules.lean b/LeanByExample/Declarative/AddAesopRules.lean similarity index 100% rename from LeanByExample/Reference/Declarative/AddAesopRules.lean rename to LeanByExample/Declarative/AddAesopRules.lean diff --git a/LeanByExample/Reference/Declarative/Attribute.lean b/LeanByExample/Declarative/Attribute.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Attribute.lean rename to LeanByExample/Declarative/Attribute.lean diff --git a/LeanByExample/Reference/Declarative/Axiom.lean b/LeanByExample/Declarative/Axiom.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Axiom.lean rename to LeanByExample/Declarative/Axiom.lean diff --git a/LeanByExample/Reference/Declarative/Class.lean b/LeanByExample/Declarative/Class.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Class.lean rename to LeanByExample/Declarative/Class.lean diff --git a/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean b/LeanByExample/Declarative/DeclareAesopRuleSets.lean similarity index 93% rename from LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean rename to LeanByExample/Declarative/DeclareAesopRuleSets.lean index e197c2d3..0c00ab4a 100644 --- a/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean +++ b/LeanByExample/Declarative/DeclareAesopRuleSets.lean @@ -1,6 +1,6 @@ /- # declare_aesop_rule_sets -`declare_aesop_rule_sets` コマンドは、[`aesop`](#{root}/Reference/Tactic/Aesop.md) タクティクで使用させるための特定のルールセットを宣言します。 +`declare_aesop_rule_sets` コマンドは、[`aesop`](#{root}/Tactic/Aesop.md) タクティクで使用させるための特定のルールセットを宣言します。 ```admonish warning title="注意" このページの内容は ボタンから Lean 4 Web で実行することができません。 @@ -18,7 +18,7 @@ declare_aesop_rule_sets [HogeRules] このとき、以下のように `aesop` の `rule_sets` に `HogeRules` を渡すことで、`HogeRules` に登録されたルールセットを使用することができます。 -/ -import LeanByExample.Reference.Declarative.DeclareAesopRuleSetsLib --# +import LeanByExample.Declarative.DeclareAesopRuleSetsLib --# import Mathlib.Tactic.Says --# example : True := by diff --git a/LeanByExample/Reference/Declarative/DeclareAesopRuleSetsLib.lean b/LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean similarity index 100% rename from LeanByExample/Reference/Declarative/DeclareAesopRuleSetsLib.lean rename to LeanByExample/Declarative/DeclareAesopRuleSetsLib.lean diff --git a/LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean b/LeanByExample/Declarative/DeclareSyntaxCat.lean similarity index 100% rename from LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean rename to LeanByExample/Declarative/DeclareSyntaxCat.lean diff --git a/LeanByExample/Reference/Declarative/Def.lean b/LeanByExample/Declarative/Def.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Def.lean rename to LeanByExample/Declarative/Def.lean diff --git a/LeanByExample/Reference/Declarative/Deriving.lean b/LeanByExample/Declarative/Deriving.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Deriving.lean rename to LeanByExample/Declarative/Deriving.lean diff --git a/LeanByExample/Reference/Declarative/Elab.lean b/LeanByExample/Declarative/Elab.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Elab.lean rename to LeanByExample/Declarative/Elab.lean diff --git a/LeanByExample/Reference/Declarative/Example.lean b/LeanByExample/Declarative/Example.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Example.lean rename to LeanByExample/Declarative/Example.lean diff --git a/LeanByExample/Reference/Declarative/Export.lean b/LeanByExample/Declarative/Export.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Export.lean rename to LeanByExample/Declarative/Export.lean diff --git a/LeanByExample/Reference/Declarative/Inductive.lean b/LeanByExample/Declarative/Inductive.lean similarity index 97% rename from LeanByExample/Reference/Declarative/Inductive.lean rename to LeanByExample/Declarative/Inductive.lean index d4f7a44e..ec941a5b 100644 --- a/LeanByExample/Reference/Declarative/Inductive.lean +++ b/LeanByExample/Declarative/Inductive.lean @@ -93,7 +93,7 @@ def even : Nat → Bool /- 両者の違いは何でしょうか？双方にメリットとデメリットがあります。 -再帰関数として定義するメリットとして、計算可能になることが挙げられます。再帰関数として定義されていれば [`#eval`](#{root}/Reference/Diagnostic/Eval.md) コマンドなど、Lean に組み込まれた機能を使って計算を行うことができます。一方で帰納的述語として定義されていると、計算をさせるための準備をこちらで行う必要があります。-/ +再帰関数として定義するメリットとして、計算可能になることが挙げられます。再帰関数として定義されていれば [`#eval`](#{root}/Diagnostic/Eval.md) コマンドなど、Lean に組み込まれた機能を使って計算を行うことができます。一方で帰納的述語として定義されていると、計算をさせるための準備をこちらで行う必要があります。-/ -- すぐに計算できる #guard even 4 diff --git a/LeanByExample/Reference/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Infix.lean rename to LeanByExample/Declarative/Infix.lean diff --git a/LeanByExample/Reference/Declarative/Instance.lean b/LeanByExample/Declarative/Instance.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Instance.lean rename to LeanByExample/Declarative/Instance.lean diff --git a/LeanByExample/Reference/Declarative/Local.lean b/LeanByExample/Declarative/Local.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Local.lean rename to LeanByExample/Declarative/Local.lean diff --git a/LeanByExample/Reference/Declarative/Macro.lean b/LeanByExample/Declarative/Macro.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Macro.lean rename to LeanByExample/Declarative/Macro.lean diff --git a/LeanByExample/Reference/Declarative/MacroRules.lean b/LeanByExample/Declarative/MacroRules.lean similarity index 100% rename from LeanByExample/Reference/Declarative/MacroRules.lean rename to LeanByExample/Declarative/MacroRules.lean diff --git a/LeanByExample/Reference/Declarative/Namespace.lean b/LeanByExample/Declarative/Namespace.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Namespace.lean rename to LeanByExample/Declarative/Namespace.lean diff --git a/LeanByExample/Reference/Declarative/Noncomputable.lean b/LeanByExample/Declarative/Noncomputable.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Noncomputable.lean rename to LeanByExample/Declarative/Noncomputable.lean diff --git a/LeanByExample/Reference/Declarative/Notation.lean b/LeanByExample/Declarative/Notation.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Notation.lean rename to LeanByExample/Declarative/Notation.lean diff --git a/LeanByExample/Reference/Declarative/Opaque.lean b/LeanByExample/Declarative/Opaque.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Opaque.lean rename to LeanByExample/Declarative/Opaque.lean diff --git a/LeanByExample/Reference/Declarative/Open.lean b/LeanByExample/Declarative/Open.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Open.lean rename to LeanByExample/Declarative/Open.lean diff --git a/LeanByExample/Reference/Declarative/Partial.lean b/LeanByExample/Declarative/Partial.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Partial.lean rename to LeanByExample/Declarative/Partial.lean diff --git a/LeanByExample/Reference/Declarative/Postfix.lean b/LeanByExample/Declarative/Postfix.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Postfix.lean rename to LeanByExample/Declarative/Postfix.lean diff --git a/LeanByExample/Reference/Declarative/Prefix.lean b/LeanByExample/Declarative/Prefix.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Prefix.lean rename to LeanByExample/Declarative/Prefix.lean diff --git a/LeanByExample/Reference/Declarative/Private.lean b/LeanByExample/Declarative/Private.lean similarity index 93% rename from LeanByExample/Reference/Declarative/Private.lean rename to LeanByExample/Declarative/Private.lean index 9b5a5d07..5e08cffa 100644 --- a/LeanByExample/Reference/Declarative/Private.lean +++ b/LeanByExample/Declarative/Private.lean @@ -3,7 +3,7 @@ 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。 -/ -import LeanByExample.Reference.Declarative.Protected -- protected のページをインポート +import LeanByExample.Declarative.Protected -- protected のページをインポート import Lean namespace Private --# diff --git a/LeanByExample/Reference/Declarative/ProofWanted.lean b/LeanByExample/Declarative/ProofWanted.lean similarity index 100% rename from LeanByExample/Reference/Declarative/ProofWanted.lean rename to LeanByExample/Declarative/ProofWanted.lean diff --git a/LeanByExample/Reference/Declarative/Protected.lean b/LeanByExample/Declarative/Protected.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Protected.lean rename to LeanByExample/Declarative/Protected.lean diff --git a/LeanByExample/Reference/Declarative/README.lean b/LeanByExample/Declarative/README.lean similarity index 100% rename from LeanByExample/Reference/Declarative/README.lean rename to LeanByExample/Declarative/README.lean diff --git a/LeanByExample/Reference/Declarative/Scoped.lean b/LeanByExample/Declarative/Scoped.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Scoped.lean rename to LeanByExample/Declarative/Scoped.lean diff --git a/LeanByExample/Reference/Declarative/Section.lean b/LeanByExample/Declarative/Section.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Section.lean rename to LeanByExample/Declarative/Section.lean diff --git a/LeanByExample/Reference/Declarative/SetOption.lean b/LeanByExample/Declarative/SetOption.lean similarity index 100% rename from LeanByExample/Reference/Declarative/SetOption.lean rename to LeanByExample/Declarative/SetOption.lean diff --git a/LeanByExample/Reference/Declarative/Structure.lean b/LeanByExample/Declarative/Structure.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Structure.lean rename to LeanByExample/Declarative/Structure.lean diff --git a/LeanByExample/Reference/Declarative/Syntax.lean b/LeanByExample/Declarative/Syntax.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Syntax.lean rename to LeanByExample/Declarative/Syntax.lean diff --git a/LeanByExample/Reference/Declarative/TerminationBy.lean b/LeanByExample/Declarative/TerminationBy.lean similarity index 100% rename from LeanByExample/Reference/Declarative/TerminationBy.lean rename to LeanByExample/Declarative/TerminationBy.lean diff --git a/LeanByExample/Reference/Declarative/Theorem.lean b/LeanByExample/Declarative/Theorem.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Theorem.lean rename to LeanByExample/Declarative/Theorem.lean diff --git a/LeanByExample/Reference/Declarative/Variable.lean b/LeanByExample/Declarative/Variable.lean similarity index 100% rename from LeanByExample/Reference/Declarative/Variable.lean rename to LeanByExample/Declarative/Variable.lean diff --git a/LeanByExample/Reference/Diagnostic/Check.lean b/LeanByExample/Diagnostic/Check.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Check.lean rename to LeanByExample/Diagnostic/Check.lean diff --git a/LeanByExample/Reference/Diagnostic/CheckFailure.lean b/LeanByExample/Diagnostic/CheckFailure.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/CheckFailure.lean rename to LeanByExample/Diagnostic/CheckFailure.lean diff --git a/LeanByExample/Reference/Diagnostic/Eval.lean b/LeanByExample/Diagnostic/Eval.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Eval.lean rename to LeanByExample/Diagnostic/Eval.lean diff --git a/LeanByExample/Reference/Diagnostic/Find.lean b/LeanByExample/Diagnostic/Find.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Find.lean rename to LeanByExample/Diagnostic/Find.lean diff --git a/LeanByExample/Reference/Diagnostic/Guard.lean b/LeanByExample/Diagnostic/Guard.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Guard.lean rename to LeanByExample/Diagnostic/Guard.lean diff --git a/LeanByExample/Reference/Diagnostic/GuardMsgs.lean b/LeanByExample/Diagnostic/GuardMsgs.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/GuardMsgs.lean rename to LeanByExample/Diagnostic/GuardMsgs.lean diff --git a/LeanByExample/Reference/Diagnostic/Help.lean b/LeanByExample/Diagnostic/Help.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Help.lean rename to LeanByExample/Diagnostic/Help.lean diff --git a/LeanByExample/Reference/Diagnostic/Html.lean b/LeanByExample/Diagnostic/Html.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Html.lean rename to LeanByExample/Diagnostic/Html.lean diff --git a/LeanByExample/Reference/Diagnostic/Instances.lean b/LeanByExample/Diagnostic/Instances.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Instances.lean rename to LeanByExample/Diagnostic/Instances.lean diff --git a/LeanByExample/Reference/Diagnostic/Lint.lean b/LeanByExample/Diagnostic/Lint.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Lint.lean rename to LeanByExample/Diagnostic/Lint.lean diff --git a/LeanByExample/Reference/Diagnostic/Print.lean b/LeanByExample/Diagnostic/Print.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Print.lean rename to LeanByExample/Diagnostic/Print.lean diff --git a/LeanByExample/Reference/Diagnostic/README.lean b/LeanByExample/Diagnostic/README.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/README.lean rename to LeanByExample/Diagnostic/README.lean diff --git a/LeanByExample/Reference/Diagnostic/Reduce.lean b/LeanByExample/Diagnostic/Reduce.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Reduce.lean rename to LeanByExample/Diagnostic/Reduce.lean diff --git a/LeanByExample/Reference/Diagnostic/Synth.lean b/LeanByExample/Diagnostic/Synth.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Synth.lean rename to LeanByExample/Diagnostic/Synth.lean diff --git a/LeanByExample/Reference/Diagnostic/Time.lean b/LeanByExample/Diagnostic/Time.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Time.lean rename to LeanByExample/Diagnostic/Time.lean diff --git a/LeanByExample/Reference/Diagnostic/Version.lean b/LeanByExample/Diagnostic/Version.lean similarity index 100% rename from LeanByExample/Reference/Diagnostic/Version.lean rename to LeanByExample/Diagnostic/Version.lean diff --git a/LeanByExample/Reference/Diagnostic/Whnf.lean b/LeanByExample/Diagnostic/Whnf.lean similarity index 91% rename from LeanByExample/Reference/Diagnostic/Whnf.lean rename to LeanByExample/Diagnostic/Whnf.lean index 08961b5d..5475fe4f 100644 --- a/LeanByExample/Reference/Diagnostic/Whnf.lean +++ b/LeanByExample/Diagnostic/Whnf.lean @@ -62,7 +62,7 @@ instance instMonadMany : Monad Many where pure := Many.one bind := Many.bind -/- `Monad` 型クラスは [`Functor`](#{root}/Reference/TypeClass/Functor.md) クラスや `Applicative` クラスの実装を含むので、`Many` は `Functor` や `Applicative` のインスタンスでもあります。このインスタンスは次のように `inferInstance` という関数で構成することができますが、その中身を `#print` で出力してみても実装がわかりません。-/ +/- `Monad` 型クラスは [`Functor`](#{root}/TypeClass/Functor.md) クラスや `Applicative` クラスの実装を含むので、`Many` は `Functor` や `Applicative` のインスタンスでもあります。このインスタンスは次のように `inferInstance` という関数で構成することができますが、その中身を `#print` で出力してみても実装がわかりません。-/ def instManyFunctor : Functor Many := inferInstance diff --git a/LeanByExample/Reference/Option/AutoImplicit.lean b/LeanByExample/Option/AutoImplicit.lean similarity index 100% rename from LeanByExample/Reference/Option/AutoImplicit.lean rename to LeanByExample/Option/AutoImplicit.lean diff --git a/LeanByExample/Reference/Option/Flexible.lean b/LeanByExample/Option/Flexible.lean similarity index 82% rename from LeanByExample/Reference/Option/Flexible.lean rename to LeanByExample/Option/Flexible.lean index 26e25c00..636e580b 100644 --- a/LeanByExample/Reference/Option/Flexible.lean +++ b/LeanByExample/Option/Flexible.lean @@ -4,7 +4,7 @@ ## 背景 -証明を書く際のベストプラクティスとして、[`simp`](#{root}/Reference/Tactic/Simp.md) タクティクのような柔軟性のあるタクティクは、証明の末尾以外で使わないほうがよいということが知られています。[^non-terminal-simp] `simp` タクティクはどういう補題が `[simp]` 属性で登録されているかに応じて挙動が変わるため、引用しているライブラリに `simp` 補題が新たに追加されたり、削除されたりするたびに挙動が変わってしまうためです。 +証明を書く際のベストプラクティスとして、[`simp`](#{root}/Tactic/Simp.md) タクティクのような柔軟性のあるタクティクは、証明の末尾以外で使わないほうがよいということが知られています。[^non-terminal-simp] `simp` タクティクはどういう補題が `[simp]` 属性で登録されているかに応じて挙動が変わるため、引用しているライブラリに `simp` 補題が新たに追加されたり、削除されたりするたびに挙動が変わってしまうためです。 たとえば、以下のような証明を考えてみます。 -/ @@ -46,7 +46,7 @@ end --# これは `simp` が柔軟(flexible)なタクティクであることが原因で、対策として次のような方法が知られています。 * 証明末でしか `simp` タクティクを使わない。証明末であれば、「壊れる前の証明において `simp` が何を行っていたか」は常に「残りのゴールを閉じる」であり明確で、ライブラリの変更があってもどう修正すればいいかがわかりやすいからです。 -* [`have`](#{root}/Reference/Tactic/Have.md) タクティクや [`suffices`](#{root}/Reference/Tactic/Suffices.md) タクティクを使って証明末そのものを増やす。 +* [`have`](#{root}/Tactic/Have.md) タクティクや [`suffices`](#{root}/Tactic/Suffices.md) タクティクを使って証明末そのものを増やす。 * `simp only` 構文を使って、ライブラリ側に変更があっても `simp` タクティクの挙動が変わらないようにする。 * `simpa` タクティクのような、ゴールを閉じなければならないという制約を持つタクティクで書き換える。 -/ diff --git a/LeanByExample/Reference/Option/Hygiene.lean b/LeanByExample/Option/Hygiene.lean similarity index 100% rename from LeanByExample/Reference/Option/Hygiene.lean rename to LeanByExample/Option/Hygiene.lean diff --git a/LeanByExample/Reference/Option/MultiGoal.lean b/LeanByExample/Option/MultiGoal.lean similarity index 100% rename from LeanByExample/Reference/Option/MultiGoal.lean rename to LeanByExample/Option/MultiGoal.lean diff --git a/LeanByExample/Reference/Option/README.lean b/LeanByExample/Option/README.lean similarity index 100% rename from LeanByExample/Reference/Option/README.lean rename to LeanByExample/Option/README.lean diff --git a/LeanByExample/Reference/Option/RelaxedAutoImplicit.lean b/LeanByExample/Option/RelaxedAutoImplicit.lean similarity index 100% rename from LeanByExample/Reference/Option/RelaxedAutoImplicit.lean rename to LeanByExample/Option/RelaxedAutoImplicit.lean diff --git a/LeanByExample/Reference/TypeClass/README.lean b/LeanByExample/Reference/TypeClass/README.lean deleted file mode 100644 index 0c719d57..00000000 --- a/LeanByExample/Reference/TypeClass/README.lean +++ /dev/null @@ -1,6 +0,0 @@ -/- # 型クラス - -型クラスとは、和や積、逆数を取る演算など、複数の型に対してそれぞれのやり方で実装されるような演算を定義するものです。 - -型クラスは主に [`class`](#{root}/Reference/Declarative/Class.md) コマンドで定義され、インスタンスを宣言するには [`instance`](#{root}/Reference/Declarative/Instance.md) コマンドを使用します。 --/ diff --git a/LeanByExample/Reference/Tactic/AcRfl.lean b/LeanByExample/Tactic/AcRfl.lean similarity index 100% rename from LeanByExample/Reference/Tactic/AcRfl.lean rename to LeanByExample/Tactic/AcRfl.lean diff --git a/LeanByExample/Reference/Tactic/Aesop.lean b/LeanByExample/Tactic/Aesop.lean similarity index 96% rename from LeanByExample/Reference/Tactic/Aesop.lean rename to LeanByExample/Tactic/Aesop.lean index 2b2889a4..cfcdf3ee 100644 --- a/LeanByExample/Reference/Tactic/Aesop.lean +++ b/LeanByExample/Tactic/Aesop.lean @@ -42,7 +42,7 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f /- 上記の例により、とくに `aesop` が実行の過程で [`simp_all`](./SimpAll.md) タクティクや `intro` タクティク等を使用することがわかります。 特に、`aesop` は `simp_all` の強化版であるということができます。 -実際には `aesop` は `simp_all` とは異なり、単純化だけでなく「試行錯誤しながらよい証明を探索する」ということができます。これについて詳しくは [`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) のページを参照してください。-/ +実際には `aesop` は `simp_all` とは異なり、単純化だけでなく「試行錯誤しながらよい証明を探索する」ということができます。これについて詳しくは [`add_aesop_rules`](#{root}/Declarative/AddAesopRules.md) のページを参照してください。-/ /- ## カスタマイズ `aesop` はユーザがカスタマイズ可能です。補題やタクティクを登録することで、証明可能な命題を増やすことができます。 diff --git a/LeanByExample/Reference/Tactic/AllGoals.lean b/LeanByExample/Tactic/AllGoals.lean similarity index 100% rename from LeanByExample/Reference/Tactic/AllGoals.lean rename to LeanByExample/Tactic/AllGoals.lean diff --git a/LeanByExample/Reference/Tactic/Apply.lean b/LeanByExample/Tactic/Apply.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Apply.lean rename to LeanByExample/Tactic/Apply.lean diff --git a/LeanByExample/Reference/Tactic/ApplyAssumption.lean b/LeanByExample/Tactic/ApplyAssumption.lean similarity index 100% rename from LeanByExample/Reference/Tactic/ApplyAssumption.lean rename to LeanByExample/Tactic/ApplyAssumption.lean diff --git a/LeanByExample/Reference/Tactic/ApplyAt.lean b/LeanByExample/Tactic/ApplyAt.lean similarity index 100% rename from LeanByExample/Reference/Tactic/ApplyAt.lean rename to LeanByExample/Tactic/ApplyAt.lean diff --git a/LeanByExample/Reference/Tactic/ApplyQuestion.lean b/LeanByExample/Tactic/ApplyQuestion.lean similarity index 100% rename from LeanByExample/Reference/Tactic/ApplyQuestion.lean rename to LeanByExample/Tactic/ApplyQuestion.lean diff --git a/LeanByExample/Reference/Tactic/Assumption.lean b/LeanByExample/Tactic/Assumption.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Assumption.lean rename to LeanByExample/Tactic/Assumption.lean diff --git a/LeanByExample/Reference/Tactic/By.lean b/LeanByExample/Tactic/By.lean similarity index 100% rename from LeanByExample/Reference/Tactic/By.lean rename to LeanByExample/Tactic/By.lean diff --git a/LeanByExample/Reference/Tactic/ByCases.lean b/LeanByExample/Tactic/ByCases.lean similarity index 100% rename from LeanByExample/Reference/Tactic/ByCases.lean rename to LeanByExample/Tactic/ByCases.lean diff --git a/LeanByExample/Reference/Tactic/ByContra.lean b/LeanByExample/Tactic/ByContra.lean similarity index 100% rename from LeanByExample/Reference/Tactic/ByContra.lean rename to LeanByExample/Tactic/ByContra.lean diff --git a/LeanByExample/Reference/Tactic/Calc.lean b/LeanByExample/Tactic/Calc.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Calc.lean rename to LeanByExample/Tactic/Calc.lean diff --git a/LeanByExample/Reference/Tactic/Cases.lean b/LeanByExample/Tactic/Cases.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Cases.lean rename to LeanByExample/Tactic/Cases.lean diff --git a/LeanByExample/Reference/Tactic/CasesAp.lean b/LeanByExample/Tactic/CasesAp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/CasesAp.lean rename to LeanByExample/Tactic/CasesAp.lean diff --git a/LeanByExample/Reference/Tactic/Choose.lean b/LeanByExample/Tactic/Choose.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Choose.lean rename to LeanByExample/Tactic/Choose.lean diff --git a/LeanByExample/Reference/Tactic/Clear.lean b/LeanByExample/Tactic/Clear.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Clear.lean rename to LeanByExample/Tactic/Clear.lean diff --git a/LeanByExample/Reference/Tactic/Congr.lean b/LeanByExample/Tactic/Congr.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Congr.lean rename to LeanByExample/Tactic/Congr.lean diff --git a/LeanByExample/Reference/Tactic/Constructor.lean b/LeanByExample/Tactic/Constructor.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Constructor.lean rename to LeanByExample/Tactic/Constructor.lean diff --git a/LeanByExample/Reference/Tactic/Contradiction.lean b/LeanByExample/Tactic/Contradiction.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Contradiction.lean rename to LeanByExample/Tactic/Contradiction.lean diff --git a/LeanByExample/Reference/Tactic/Contrapose.lean b/LeanByExample/Tactic/Contrapose.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Contrapose.lean rename to LeanByExample/Tactic/Contrapose.lean diff --git a/LeanByExample/Reference/Tactic/Conv.lean b/LeanByExample/Tactic/Conv.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Conv.lean rename to LeanByExample/Tactic/Conv.lean diff --git a/LeanByExample/Reference/Tactic/Convert.lean b/LeanByExample/Tactic/Convert.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Convert.lean rename to LeanByExample/Tactic/Convert.lean diff --git a/LeanByExample/Reference/Tactic/Decide.lean b/LeanByExample/Tactic/Decide.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Decide.lean rename to LeanByExample/Tactic/Decide.lean diff --git a/LeanByExample/Reference/Tactic/Done.lean b/LeanByExample/Tactic/Done.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Done.lean rename to LeanByExample/Tactic/Done.lean diff --git a/LeanByExample/Reference/Tactic/Dsimp.lean b/LeanByExample/Tactic/Dsimp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Dsimp.lean rename to LeanByExample/Tactic/Dsimp.lean diff --git a/LeanByExample/Reference/Tactic/Exact.lean b/LeanByExample/Tactic/Exact.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Exact.lean rename to LeanByExample/Tactic/Exact.lean diff --git a/LeanByExample/Reference/Tactic/ExactQuestion.lean b/LeanByExample/Tactic/ExactQuestion.lean similarity index 100% rename from LeanByExample/Reference/Tactic/ExactQuestion.lean rename to LeanByExample/Tactic/ExactQuestion.lean diff --git a/LeanByExample/Reference/Tactic/Exfalso.lean b/LeanByExample/Tactic/Exfalso.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Exfalso.lean rename to LeanByExample/Tactic/Exfalso.lean diff --git a/LeanByExample/Reference/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Exists.lean rename to LeanByExample/Tactic/Exists.lean diff --git a/LeanByExample/Reference/Tactic/Ext.lean b/LeanByExample/Tactic/Ext.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Ext.lean rename to LeanByExample/Tactic/Ext.lean diff --git a/LeanByExample/Reference/Tactic/FieldSimp.lean b/LeanByExample/Tactic/FieldSimp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/FieldSimp.lean rename to LeanByExample/Tactic/FieldSimp.lean diff --git a/LeanByExample/Reference/Tactic/FinCases.lean b/LeanByExample/Tactic/FinCases.lean similarity index 100% rename from LeanByExample/Reference/Tactic/FinCases.lean rename to LeanByExample/Tactic/FinCases.lean diff --git a/LeanByExample/Reference/Tactic/FunProp.lean b/LeanByExample/Tactic/FunProp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/FunProp.lean rename to LeanByExample/Tactic/FunProp.lean diff --git a/LeanByExample/Reference/Tactic/Funext.lean b/LeanByExample/Tactic/Funext.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Funext.lean rename to LeanByExample/Tactic/Funext.lean diff --git a/LeanByExample/Reference/Tactic/Gcongr.lean b/LeanByExample/Tactic/Gcongr.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Gcongr.lean rename to LeanByExample/Tactic/Gcongr.lean diff --git a/LeanByExample/Reference/Tactic/Generalize.lean b/LeanByExample/Tactic/Generalize.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Generalize.lean rename to LeanByExample/Tactic/Generalize.lean diff --git a/LeanByExample/Reference/Tactic/GuardHyp.lean b/LeanByExample/Tactic/GuardHyp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/GuardHyp.lean rename to LeanByExample/Tactic/GuardHyp.lean diff --git a/LeanByExample/Reference/Tactic/Have.lean b/LeanByExample/Tactic/Have.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Have.lean rename to LeanByExample/Tactic/Have.lean diff --git a/LeanByExample/Reference/Tactic/Hint.lean b/LeanByExample/Tactic/Hint.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Hint.lean rename to LeanByExample/Tactic/Hint.lean diff --git a/LeanByExample/Reference/Tactic/Induction.lean b/LeanByExample/Tactic/Induction.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Induction.lean rename to LeanByExample/Tactic/Induction.lean diff --git a/LeanByExample/Reference/Tactic/InductionAp.lean b/LeanByExample/Tactic/InductionAp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/InductionAp.lean rename to LeanByExample/Tactic/InductionAp.lean diff --git a/LeanByExample/Reference/Tactic/Intro.lean b/LeanByExample/Tactic/Intro.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Intro.lean rename to LeanByExample/Tactic/Intro.lean diff --git a/LeanByExample/Reference/Tactic/Itauto.lean b/LeanByExample/Tactic/Itauto.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Itauto.lean rename to LeanByExample/Tactic/Itauto.lean diff --git a/LeanByExample/Reference/Tactic/Left.lean b/LeanByExample/Tactic/Left.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Left.lean rename to LeanByExample/Tactic/Left.lean diff --git a/LeanByExample/Reference/Tactic/Linarith.lean b/LeanByExample/Tactic/Linarith.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Linarith.lean rename to LeanByExample/Tactic/Linarith.lean diff --git a/LeanByExample/Reference/Tactic/NativeDecide.lean b/LeanByExample/Tactic/NativeDecide.lean similarity index 100% rename from LeanByExample/Reference/Tactic/NativeDecide.lean rename to LeanByExample/Tactic/NativeDecide.lean diff --git a/LeanByExample/Reference/Tactic/Nlinarith.lean b/LeanByExample/Tactic/Nlinarith.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Nlinarith.lean rename to LeanByExample/Tactic/Nlinarith.lean diff --git a/LeanByExample/Reference/Tactic/NormCast.lean b/LeanByExample/Tactic/NormCast.lean similarity index 100% rename from LeanByExample/Reference/Tactic/NormCast.lean rename to LeanByExample/Tactic/NormCast.lean diff --git a/LeanByExample/Reference/Tactic/NthRw.lean b/LeanByExample/Tactic/NthRw.lean similarity index 100% rename from LeanByExample/Reference/Tactic/NthRw.lean rename to LeanByExample/Tactic/NthRw.lean diff --git a/LeanByExample/Reference/Tactic/Obtain.lean b/LeanByExample/Tactic/Obtain.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Obtain.lean rename to LeanByExample/Tactic/Obtain.lean diff --git a/LeanByExample/Reference/Tactic/Omega.lean b/LeanByExample/Tactic/Omega.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Omega.lean rename to LeanByExample/Tactic/Omega.lean diff --git a/LeanByExample/Reference/Tactic/Plausible.lean b/LeanByExample/Tactic/Plausible.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Plausible.lean rename to LeanByExample/Tactic/Plausible.lean diff --git a/LeanByExample/Reference/Tactic/Positivity.lean b/LeanByExample/Tactic/Positivity.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Positivity.lean rename to LeanByExample/Tactic/Positivity.lean diff --git a/LeanByExample/Reference/Tactic/PushNeg.lean b/LeanByExample/Tactic/PushNeg.lean similarity index 100% rename from LeanByExample/Reference/Tactic/PushNeg.lean rename to LeanByExample/Tactic/PushNeg.lean diff --git a/LeanByExample/Reference/Tactic/Qify.lean b/LeanByExample/Tactic/Qify.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Qify.lean rename to LeanByExample/Tactic/Qify.lean diff --git a/LeanByExample/Reference/Tactic/README.lean b/LeanByExample/Tactic/README.lean similarity index 100% rename from LeanByExample/Reference/Tactic/README.lean rename to LeanByExample/Tactic/README.lean diff --git a/LeanByExample/Reference/Tactic/Rcases.lean b/LeanByExample/Tactic/Rcases.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Rcases.lean rename to LeanByExample/Tactic/Rcases.lean diff --git a/LeanByExample/Reference/Tactic/Refine.lean b/LeanByExample/Tactic/Refine.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Refine.lean rename to LeanByExample/Tactic/Refine.lean diff --git a/LeanByExample/Reference/Tactic/Rel.lean b/LeanByExample/Tactic/Rel.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Rel.lean rename to LeanByExample/Tactic/Rel.lean diff --git a/LeanByExample/Reference/Tactic/RenameI.lean b/LeanByExample/Tactic/RenameI.lean similarity index 100% rename from LeanByExample/Reference/Tactic/RenameI.lean rename to LeanByExample/Tactic/RenameI.lean diff --git a/LeanByExample/Reference/Tactic/Repeat.lean b/LeanByExample/Tactic/Repeat.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Repeat.lean rename to LeanByExample/Tactic/Repeat.lean diff --git a/LeanByExample/Reference/Tactic/Replace.lean b/LeanByExample/Tactic/Replace.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Replace.lean rename to LeanByExample/Tactic/Replace.lean diff --git a/LeanByExample/Reference/Tactic/Rfl.lean b/LeanByExample/Tactic/Rfl.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Rfl.lean rename to LeanByExample/Tactic/Rfl.lean diff --git a/LeanByExample/Reference/Tactic/Right.lean b/LeanByExample/Tactic/Right.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Right.lean rename to LeanByExample/Tactic/Right.lean diff --git a/LeanByExample/Reference/Tactic/Ring.lean b/LeanByExample/Tactic/Ring.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Ring.lean rename to LeanByExample/Tactic/Ring.lean diff --git a/LeanByExample/Reference/Tactic/Rw.lean b/LeanByExample/Tactic/Rw.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Rw.lean rename to LeanByExample/Tactic/Rw.lean diff --git a/LeanByExample/Reference/Tactic/RwSearch.lean b/LeanByExample/Tactic/RwSearch.lean similarity index 100% rename from LeanByExample/Reference/Tactic/RwSearch.lean rename to LeanByExample/Tactic/RwSearch.lean diff --git a/LeanByExample/Reference/Tactic/Says.lean b/LeanByExample/Tactic/Says.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Says.lean rename to LeanByExample/Tactic/Says.lean diff --git a/LeanByExample/Reference/Tactic/SeqFocus.lean b/LeanByExample/Tactic/SeqFocus.lean similarity index 100% rename from LeanByExample/Reference/Tactic/SeqFocus.lean rename to LeanByExample/Tactic/SeqFocus.lean diff --git a/LeanByExample/Reference/Tactic/Set.lean b/LeanByExample/Tactic/Set.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Set.lean rename to LeanByExample/Tactic/Set.lean diff --git a/LeanByExample/Reference/Tactic/Show.lean b/LeanByExample/Tactic/Show.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Show.lean rename to LeanByExample/Tactic/Show.lean diff --git a/LeanByExample/Reference/Tactic/Simp.lean b/LeanByExample/Tactic/Simp.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Simp.lean rename to LeanByExample/Tactic/Simp.lean diff --git a/LeanByExample/Reference/Tactic/SimpAll.lean b/LeanByExample/Tactic/SimpAll.lean similarity index 100% rename from LeanByExample/Reference/Tactic/SimpAll.lean rename to LeanByExample/Tactic/SimpAll.lean diff --git a/LeanByExample/Reference/Tactic/Sorry.lean b/LeanByExample/Tactic/Sorry.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Sorry.lean rename to LeanByExample/Tactic/Sorry.lean diff --git a/LeanByExample/Reference/Tactic/Split.lean b/LeanByExample/Tactic/Split.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Split.lean rename to LeanByExample/Tactic/Split.lean diff --git a/LeanByExample/Reference/Tactic/Suffices.lean b/LeanByExample/Tactic/Suffices.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Suffices.lean rename to LeanByExample/Tactic/Suffices.lean diff --git a/LeanByExample/Reference/Tactic/Tauto.lean b/LeanByExample/Tactic/Tauto.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Tauto.lean rename to LeanByExample/Tactic/Tauto.lean diff --git a/LeanByExample/Reference/Tactic/Trans.lean b/LeanByExample/Tactic/Trans.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Trans.lean rename to LeanByExample/Tactic/Trans.lean diff --git a/LeanByExample/Reference/Tactic/Trivial.lean b/LeanByExample/Tactic/Trivial.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Trivial.lean rename to LeanByExample/Tactic/Trivial.lean diff --git a/LeanByExample/Reference/Tactic/Try.lean b/LeanByExample/Tactic/Try.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Try.lean rename to LeanByExample/Tactic/Try.lean diff --git a/LeanByExample/Reference/Tactic/Unfold.lean b/LeanByExample/Tactic/Unfold.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Unfold.lean rename to LeanByExample/Tactic/Unfold.lean diff --git a/LeanByExample/Reference/Tactic/WithReducible.lean b/LeanByExample/Tactic/WithReducible.lean similarity index 100% rename from LeanByExample/Reference/Tactic/WithReducible.lean rename to LeanByExample/Tactic/WithReducible.lean diff --git a/LeanByExample/Reference/Tactic/Wlog.lean b/LeanByExample/Tactic/Wlog.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Wlog.lean rename to LeanByExample/Tactic/Wlog.lean diff --git a/LeanByExample/Reference/Tactic/Zify.lean b/LeanByExample/Tactic/Zify.lean similarity index 100% rename from LeanByExample/Reference/Tactic/Zify.lean rename to LeanByExample/Tactic/Zify.lean diff --git a/LeanByExample/Tutorial/Exercise/BarberParadox.lean b/LeanByExample/Tutorial/Exercise/BarberParadox.lean deleted file mode 100644 index c49fe40f..00000000 --- a/LeanByExample/Tutorial/Exercise/BarberParadox.lean +++ /dev/null @@ -1,39 +0,0 @@ -/- # 床屋のパラドックス -集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。 - -この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。 - -以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。 - -その内容は自然言語では次のように説明できます。 - -```admonish info title="" -ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？ - -仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。 - -いずれにせよ矛盾が生じてしまうので、そんな床屋は存在しません！ -``` - -この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。 --/ -namespace Barber -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- 全体集合となる人々の集合 -/ -opaque Person : Type - -/-- p さんが q さんの髭を剃るという述語 -/ -opaque shave (p q : Person) : Prop - --- 床屋が存在するという仮定 -variable (barber : Person) - --- 床屋の信念を仮定として表現したもの -variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p) - -example : False := by - sorry - -end Barber diff --git a/LeanByExample/Tutorial/Exercise/CantorPairing.lean b/LeanByExample/Tutorial/Exercise/CantorPairing.lean deleted file mode 100644 index aa77aeb3..00000000 --- a/LeanByExample/Tutorial/Exercise/CantorPairing.lean +++ /dev/null @@ -1,156 +0,0 @@ -/- # Cantor の対関数とその全単射性 - -## はじめに - -有限集合 `A` と `B` に対して、`A` と `B` の要素数が等しいということは、`|A| = |B| = n` となる自然数 `n` が存在するということと同値です。無限集合 `X` に対しては `|X| = n` となる自然数 `n` は存在しないので、一見すると集合の要素数という概念は無限集合には拡張できないように思えます。 - -しかし、`A` と `B` の要素数が等しいということは、「`A` と `B` の間の一対一で漏れのない対応が存在する」ということとも同値です。この定義は `A` と `B` が無限集合であっても意味をなすので、この解釈をつかって集合の要素数が等しいという概念を無限集合にも拡張することができます。 - -だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。 - -無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note] - -## 問1: sum 関数 - -まず後で使うために `0` から `n` までの自然数の和を計算する関数 `sum` を定義します。演習として、以下の `sorry` を埋めてみてください。 --/ -import Mathlib.Tactic -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- `0` から `n` までの自然数の和 -/ -def sum (n : ℕ) : ℕ := - match n with - | 0 => 0 - | n + 1 => (n + 1) + sum n - -/-- `sum n = 0` となることと `n = 0` は同値 -/ -@[simp] theorem sum_zero_iff_zero {n : ℕ} : sum n = 0 ↔ n = 0 := by - sorry - -/- ## 対関数とその逆関数 -上記で定義した `sum` を使いつつ、Cantor の対関数 `pair` とその逆関数 `unpair` を定義します。座標平面の中心からスタートして、折れ曲がりながら右上に向かうような動きをイメージするとわかりやすいかもしれません。 --/ - -/-- Cantor の対関数 -/ -def pair : ℕ × ℕ → ℕ - | (m, n) => sum (m + n) + m - -@[simp] theorem pair_zero : pair 0 = 0 := by rfl - -/-- カントールの対関数の逆関数 -/ -def unpair : ℕ → ℕ × ℕ - | 0 => (0, 0) - | x + 1 => - let (m, n) := unpair x - if n = 0 then (0, m + 1) - else (m + 1, n - 1) - -@[simp] theorem unpair_zero : unpair 0 = 0 := by rfl - -/- ## 問2: pair の全射性 -では `pair` が全射であることを示してみましょう。`pair ∘ unpair = id` が成り立つことを示せば十分です。以下の `sorry` の部分を埋めて証明を完成させてください。 --/ - -/-- `pair ∘ unpair = id` が成り立つ。特に `pair` は全射。-/ -theorem pair_unpair_eq_id (x : ℕ) : pair (unpair x) = x := by - -- `x` に対する帰納法を使う - induction' x with x ih - - -- `x = 0` の場合は明らか - case zero => sorry - - -- `x` まで成り立つと仮定して `x + 1` でも成り立つことを示そう。 - case succ => - -- まず `unpair` の定義を展開する。 - dsimp [unpair] - split_ifs - - -- 見やすさのために `(m, n) := unpair x` とおく． - all_goals - set m := (unpair x).fst with mh - set n := (unpair x).snd with nh - - -- `n = 0` の場合 - case pos h => - -- `pair (0, m + 1) = x + 1` を示せばよい。 - show pair (0, m + 1) = x + 1 - - -- `pair` の定義を展開して、示すべきことを `sum` を使って書き直すと - -- `sum (m + 1) = x + 1` を示せば良いことが分かる。 - suffices sum (m + 1) = x + 1 from by - sorry - - -- 帰納法の仮定の主張に対しても、 - -- `pair` から `sum` に書き換えることができて、 - -- `sum m + m = x` であることが分かる。 - replace ih : sum m + m = x := by - sorry - - -- 後は `sum` の定義から明らか。 - sorry - - -- `n ≠ 0` の場合 - case neg h => - -- `pair (m + 1, n - 1) = x + 1` を示せばよい。 - show pair (m + 1, n - 1) = x + 1 - - -- `pair` の定義を展開して、示すべきことを `sum` を使って書き直すと - -- `sum (m + n) + m = x` を示せば良いことが分かる。 - suffices sum (m + n) + m = x from by - sorry - - -- 帰納法の仮定の主張に対しても、 - -- `pair` から `sum` に書き換えることができて、 - -- `sum (m + n) + m = x` が成り立つことが分かる。 - replace ih : sum (m + n) + m = x := by - sorry - - -- 従って示すべきことが言えた。 - assumption - -/- ## 問3: 対関数の単射性 -最後に `pair` が単射であることを示してみましょう。`unpair ∘ pair = id` が成り立つことを示せば十分です。以下の `sorry` の部分を埋めて証明を完成させてください。 --/ - -/-- `unpair ∘ pair = id` が成り立つ。特に `pair` は単射。-/ -theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by - -- `x = pair (m, n)` として `x` に対する帰納法を利用する - induction' h : pair (m, n) with x ih generalizing m n - - -- `pair (m, n) = 0` のときは - -- `pair` の定義から明らか。 - case zero => sorry - - -- `pair (m, n) = x + 1` のとき - case succ => - -- `m` がゼロかそうでないかで場合分けする - match m with - - -- `m = 0` のとき - | 0 => - -- `pair (0, n) = x + 1` により `n > 0` が成り立つ。 - have npos : n > 0 := by - sorry - - -- よって `sum n = sum (n - 1) + n` と書くことができて、 - have lem : sum n = sum (n - 1) + n := by - sorry - - -- `pair (n - 1, 0) = x` が結論できる。 - have : pair (n - 1, 0) = x := by - sorry - - -- 後は帰納法の仮定から従う。 - sorry - - -- `m = m' + 1` のとき - | m' + 1 => - -- `pair` の定義から `pair (m', n + 1) = x` が成り立つ。 - have : pair (m', n + 1) = x := by - sorry - - -- 後は帰納法の仮定から従う。 - sorry - -/- [^note]: 本項での証明を書くにあたって [Cantor の対関数の全単射性の証明](http://iso.2022.jp/math/pairing_function.pdf) を参考にいたしました。 -/ diff --git a/LeanByExample/Tutorial/Exercise/CantorTheorem.lean b/LeanByExample/Tutorial/Exercise/CantorTheorem.lean deleted file mode 100644 index 4d1cf68f..00000000 --- a/LeanByExample/Tutorial/Exercise/CantorTheorem.lean +++ /dev/null @@ -1,211 +0,0 @@ -/- # Cantor の定理 - -Cantor の定理とは、次のような定理です。 - -```admonish info title="" -どんな集合 `A` に対しても `A` より `A` のベキ集合 `𝒫 A` の方が真に濃度が大きくなります。 - -ただしここで「真に濃度が大きい」とは、 - -1. `A` から `𝒫 A` への全射が存在しない -1. `𝒫 A` から `A` への単射が存在しない - -ということを意味しています。 -``` - -「濃度」とは、集合の「要素の個数」という概念を無限集合にも拡張したものであり、おおむね「一対一で漏れのない対応がつけられるならば、要素数が等しいと言ってよいだろう」というアイデアに基づくものです。 - -この Cantor の定理はよく知られたものであり、Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。 --/ - -/- ## 集合論の形式化 - -### 全体集合を固定する - -まず、集合の概念を Lean で表現する必要があります。 - -Lean の型 `T : Type` は直観的には「項の集まり」を意味するので、これをそのまま集合だと考えてしまって、`t : T` をもって `t ∈ T` であると見なせばよいように思えるかもしれません。しかし Lean の型システムの性質上、この解釈は途中で破綻します。 - -たとえば `S T : Type` に対して共通部分の `S ∩ T` の要素は `S` にも `T` にも属していなくてはいけませんが、これは型の一意性から実現できません。`S ∪ T` についても同様で、`S` にも `S ∪ T` にも属している要素に正しく型をつけることができません。 - -そこで全体集合 `α : Type` を固定して、その中に含まれる集まりだけを考えることにします。 --/ -import Lean --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- α を全体集合として、その部分集合の全体。 -α の部分集合と α 上の述語を同一視していることに注意。 -/ -def Set (α : Type) := α → Prop - -variable {α : Type} - -/-- `a : α` は集合 `s` に属する。数学では普通 `a ∈ s` と書かれる。 -/ -def Set.mem (s : Set α) (a : α) : Prop := s a - -/-- `s a` を `a ∈ s` と書けるようにする。 -/ -instance : Membership α (Set α) := ⟨Set.mem⟩ - -/-- `A B : Set α` に対する共通部分 -/ -def Set.inter (A B : Set α) : Set α := fun x => x ∈ A ∧ x ∈ B - -/-- `A B : Set α` に対する合併 -/ -def Set.union (A B : Set α) : Set α := fun x => x ∈ A ∨ x ∈ B - -/- このようにしておくと、上記の問題は回避することができ、`S T : Set α` の共通部分や合併をとることができます。 - -### 内包記法の定義 - -「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 `p : α → Prop` に対して内包記法 `{x : α | p x}` が使用できるようにしましょう。 - -Lean のメタプログラミングフレームワークの力を借りれば、そうしたことも可能です。 --/ -section --# - -variable {α : Type} - -/-- 述語 `p : α → Prop` に対応する集合 -/ -def setOf {α : Type} (p : α → Prop) : Set α := p - -/-- 内包表記 `{ x : α | p x }` の `x : α` の部分のための構文。 -`: α` の部分はあってもなくてもよいので `( )?` で囲っている。-/ -syntax extBinder := ident (" : " term)? - -/-- 内包表記 `{ x : α | p x }` の `{ | }` の部分のための構文。 -/ -syntax (name := setBuilder) "{" extBinder " | " term "}" : term - -/-- 内包表記の意味をマクロとして定義する -/ -macro_rules - | `({ $x:ident : $type | $p }) => `(setOf (fun ($x : $type) => $p)) - | `({ $x:ident | $p }) => `(setOf (fun ($x : _) => $p)) - --- 内包表記が使えるようになったが、コマンドの出力や infoview では --- いま定義した記法が使われないという問題がある -/-- info: setOf fun n => ∃ m, n = 2 * m : Set Nat -/ -#guard_msgs in - #check {n : Nat | ∃ m, n = 2 * m} - -/-- infoview やコマンドの出力でも内包表記を使用するようにする -/ -@[app_unexpander setOf] -def setOf.unexpander : Lean.PrettyPrinter.Unexpander - | `($_ fun $x:ident => $p) => `({ $x:ident | $p }) - | `($_ fun ($x:ident : $ty:term) => $p) => `({ $x:ident : $ty:term | $p }) - | _ => throw () - --- 正常に動作することを確認 - -/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/ -#guard_msgs in - #check {n | ∃ m, n = 2 * m} - -/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/ -#guard_msgs in - #check {n : Nat | ∃ m, n = 2 * m} - -end --# - -/- ### 全射と単射 -関数 `f : A → B` が全射であるとは、任意の `b : B` に対して `f a = b` となる `a : A` が存在することです。また、`f` が単射であるとは、任意の `a₁, a₂ : A` に対して `f a₁ = f a₂` ならば `a₁ = a₂` となることです。 - -これを Lean で表現すると次のようになります。 --/ -section --# - -variable {α β : Type} - -/-- 関数の全射性 -/ -def Function.Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b - -/-- 関数の単射性 -/ -def Function.Injective (f : α → β) : Prop := ∀ {a₁ a₂ : α}, f a₁ = f a₂ → a₁ = a₂ - -end --# -/- -```admonish warning title="注意" -上記の定義を見て、関数の定義域と値域が `A B : Set α` ではなくて `α β : Type` であることに違和感を感じられたかもしれません。型と集合は異なると上で書いたばかりなのに、なぜここでは型を使っているのでしょうか？ - -実際に `A B : Set α` に対して関数の集合 `Hom A B` を定義しようとすると、その理由がわかるかもしれません。 - -`f ∈ Hom A B` が持つべき性質として `a ∈ A → f a ∈ B` があります。`A : Set α` と `B : Set α` をそれぞれ部分型 `{ a : α // a ∈ A }`, `{b : α // b ∈ B}` と同一視すれば、`Hom A B` は関数型 `{ a : α // a ∈ A } → { b : α // b ∈ B }` になります。 - -結局関数型を考えていることになるので、`α β : Type` について考えれば十分だということになるわけです。 -``` --/ - -/- ## 問1: 全射バージョン -以上の準備のもとで、Cantor の定理を証明することができます。まずは全射バージョンから示しましょう。次の `sorry` の部分を埋めてください。 --/ -section --# - -variable {α : Type} - -open Function - -/-- ある集合からそのベキ集合への全射は存在しない -/ -theorem cantor_surjective (f : α → Set α) : ¬ Surjective f := by - -- `f` が全射であると仮定する - intro hsurj - - -- 反例になる集合 `A` を構成する - let A : Set α := sorry - - -- `f` は全射なので、ある `a` が存在して `f a = A` - obtain ⟨a, ha⟩ := hsurj A - - -- `a ∈ A` は `a ∉ A` と同値である - have : a ∈ A ↔ a ∉ A := by - sorry - - -- これは矛盾 - simp at this - -/- ## 問2: 単射バージョン -単射バージョンも示すことができます。次の `sorry` の部分を埋めてください。 --/ - -/-- ベキ集合から元の集合への単射は存在しない -/ -theorem cantor_injective (f : Set α → α) : ¬ Injective f := by - -- `f` が単射だと仮定する - intro hinj - - -- 反例になる集合 `A` を構成する - let A : Set α := sorry - - -- このとき `f A ∈ A` と `f A ∉ A` が同値になる - have : (f A ∈ A) ↔ (f A ∉ A) := by - sorry - - -- これは矛盾である - simp at this -end --# - -/- -```admonish warning title="注意" -[全射(単射)が存在することと、逆方向の単射(全射)が存在することはほぼ同値](./InverseSurjInj.md)なので、それを使えば全射バージョンに帰着して示せることにお気づきでしょうか。しかし、それをそのまま使うと選択原理を使用することになります。ここでは選択原理は必要ありません。 -``` --/ - ---#-- -section -/- ## 選択原理を使用していないことを確認するコマンド -/ - -open Lean Elab Command - -elab "#detect_classical " id:ident : command => do - let constName ← liftCoreM <| realizeGlobalConstNoOverload id - let axioms ← collectAxioms constName - if axioms.isEmpty then - logInfo m!"'{constName}' does not depend on any axioms" - return () - let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm - if caxes.isEmpty then - logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}" - else - throwError m!"'{constName}' depends on classical axioms: {caxes.toList}" - -end - --- 選択原理を使用していないことを確認 -#detect_classical cantor_surjective -#detect_classical cantor_injective ---#-- diff --git a/LeanByExample/Tutorial/Exercise/DoubtImplication.lean b/LeanByExample/Tutorial/Exercise/DoubtImplication.lean deleted file mode 100644 index 335e88a2..00000000 --- a/LeanByExample/Tutorial/Exercise/DoubtImplication.lean +++ /dev/null @@ -1,99 +0,0 @@ -/- # 「ならば」の定義を疑う - -## イントロダクション - -論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学や Lean では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。 - -自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！ - -この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。 - -## 含意が満たしていて欲しい性質 - -まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2変数関数になっているとします。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。 --/ -import Lean --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# --- 含意が満たすべき性質を満たす「何か」 -opaque Imp (P Q : Prop) : Prop - --- 含意っぽい記法の導入 --- `v` は `virtual` の略 -infixr:40 " →ᵥ " => Imp - -/- これだけだと型があるだけで中身がないので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？ `P →ᵥ Q` がおおよそ「`P` を仮定すると `Q` が示せる」という意味になるようにしたいと考えると、次のようなものが考えられるでしょう。 -/ -namespace Imp --# - -variable {P Q R : Prop} - -/-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/ -axiom imp_reflexive : P →ᵥ P - -/-- 含意は推移的 -/ -axiom imp_transitive (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R - -/-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/ -axiom imp_elim (hpq : P →ᵥ Q) (hP : P) : Q - -/-- 結論が無条件に正しいなら、仮定をつけても正しい -/ -axiom imp_intro (hQ : Q) : P →ᵥ Q - -/-- ある前提から `Q` と `R` が導出できるなら、`Q ∧ R` も導出できる -/ -axiom intro_and (hpq : P →ᵥ Q) (hpr : P →ᵥ R) : P →ᵥ (Q ∧ R) - -/-- ある前提から `Q ∧ R` が導出できるなら、`Q` も導出できる -/ -axiom elim_and_left (h : P →ᵥ (Q ∧ R)) : P →ᵥ Q - -/-- ある前提から `Q ∧ R` が導出できるなら、`R` も導出できる -/ -axiom elim_and_right (h : P →ᵥ (Q ∧ R)) : P →ᵥ R - -/-- ある前提から `Q` が導出できるなら、`Q ∨ R` が導出できる -/ -axiom intro_or_left (h : P →ᵥ Q) : P →ᵥ (Q ∨ R) - -/-- ある前提から `R` が導出できるなら、`Q ∨ R` が導出できる -/ -axiom intro_or_right (h : P →ᵥ R) : P →ᵥ (Q ∨ R) - -end Imp --# - -/- ## 問題 -以上の要請のもとで、`P →ᵥ Q` が `P → Q` に一致することが証明できます。 - -以下の `sorry` を埋めてみてください。ただし、以下のことに注意してください。 - -* 仮定した要請を全部使う必要はありません。 -* 古典論理に限った話ではないので、排中律を使わずに証明してみてください。 - --/ - -variable {P Q : Prop} - -open Imp - -/-- 上記の要請を満たす `→ᵥ` は通常の含意と一致する -/ -theorem imp_valid {P Q : Prop} : (P →ᵥ Q) ↔ (P → Q) := by - sorry - ---#-- -section -/- ## 選択原理を使用していないことを確認するコマンド -/ - -open Lean Elab Command - -elab "#detect_classical " id:ident : command => do - let constName ← liftCoreM <| realizeGlobalConstNoOverload id - let axioms ← collectAxioms constName - if axioms.isEmpty then - logInfo m!"'{constName}' does not depend on any axioms" - return () - let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm - if caxes.isEmpty then - logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}" - else - throwError m!"'{constName}' depends on classical axioms: {caxes.toList}" - -end - --- 選択原理を使用していないことを確認 -#detect_classical imp_valid ---#-- diff --git a/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean b/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean deleted file mode 100644 index b377c49e..00000000 --- a/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean +++ /dev/null @@ -1,318 +0,0 @@ -/- # Heyting 代数と Bool 代数 -直観主義論理において、排中律 `P ∨ ¬ P` は独立な命題であることが知られています。つまり、証明も反証(否定を証明すること)もできません。今回の演習問題では、それに関連した話題として、Bool 代数ではない Heyting 代数が存在することを示します。 - -ここでは Mathlib をなぞるように理論を構成していきます。 - -## 半順序集合 -まず準備として、半順序集合を定義します。半順序集合には順序が定義されていますが、要素を2つ与えられたときにどちらが大きいのか比較できるとは限らないことに注意してください。 --/ -import Aesop --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- 半順序集合 -/ -class PartialOrder (α : Type) extends LE α, LT α where - /-- `≤` は反射的である -/ - le_refl : ∀ a : α, a ≤ a - - /-- `≤` は推移的である -/ - le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c - - /-- `<` のデフォルト実装 -/ - lt := fun a b => a ≤ b ∧ ¬ b ≤ a - - /-- `<` と `≤` の関係 -/ - lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a - - /-- `≤` は半対称的 -/ - le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b - -/- ## 束 -半順序集合であって、任意の2つの要素 `a, b` に対して上限 `a ⊔ b` と下限 `a ⊓ b` が存在するものを束といいます。上限は最小の上界を意味し、下限は最大の下界を意味します。 - -上限の記号 `⊔` は論理和 `∨` に、下限の記号 `⊓` は論理積 `∧` に、それぞれ似ています。またそれぞれ集合の合併 `∪` と共通部分 `∩` にも似ています。これは、`Prop` と `Set α` がともに束になっていることと整合性があります。 --/ - -section Lattice - -/-- `⊔` という記号のための型クラス -/ -class Sup (α : Type) where - /-- 最小上界、上限 -/ - sup : α → α → α - -/-- `⊓` という記号のための型クラス -/ -class Inf (α : Type) where - /-- 最大下界、下限 -/ - inf : α → α → α - -@[inherit_doc] infixl:68 " ⊔ " => Sup.sup - -@[inherit_doc] infixl:69 " ⊓ " => Inf.inf - -/-- 任意の2つの要素 `a, b` に対して上限 `a ⊔ b` が存在するような半順序集合 -/ -class SemilatticeSup (α : Type) extends Sup α, PartialOrder α where - /-- `a ⊔ b` は `a` と `b` の上界になっている -/ - le_sup_left : ∀ a b : α, a ≤ a ⊔ b - - /-- `a ⊔ b` は `a` と `b` の上界になっている -/ - le_sup_right : ∀ a b : α, b ≤ a ⊔ b - - /-- `a ⊔ b` は `a`, `b` の上界の中で最小のもの -/ - sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c - -/-- 任意の2つの要素 `a, b` に対して下限 `a ⊓ b` が存在するような半順序集合 -/ -class Semilatticeinf (α : Type) extends Inf α, PartialOrder α where - /-- `a ⊓ b` は `a` と `b` の下界になっている -/ - inf_le_left : ∀ a b : α, a ⊓ b ≤ a - - /-- `a ⊓ b` は `a` と `b` の下界になっている -/ - inf_le_right : ∀ a b : α, a ⊓ b ≤ b - - /-- `a ⊓ b` は `a`, `b` の下界の中で最大のもの -/ - le_inf : ∀ a b c : α, c ≤ a → c ≤ b → c ≤ a ⊓ b - -set_option structureDiamondWarning false in --# -/-- 束 -/ -class Lattice (α : Type) extends SemilatticeSup α, Semilatticeinf α - -end Lattice - -/- ## Heyting 代数 -ここまでの準備の下、Heyting 代数を定義することができます。Heyting 代数とは束であって、以下の条件を満たすものです。 - -1. 最大の要素 `⊤` が存在する。 -2. 最小の要素 `⊥` が存在する。 -3. 下限 `· ⊓ b` の右随伴 `b ⇨ ·` が存在する。つまり任意の `a, b, c` に対して `a ⊓ b ≤ c` と `a ≤ b ⇨ c` が同値。 --/ - -section HeytingAlgebra - -/-- `⊤` という記号のための型クラス -/ -class Top (α : Type) where - /-- 最大元 -/ - top : α - -@[inherit_doc] notation "⊤" => Top.top - -/-- `⊥` という記号のための型クラス -/ -class Bot (α : Type) where - /-- 最小元 -/ - bot : α - -@[inherit_doc] notation "⊥" => Bot.bot - -/-- `⇨` という記号のための型クラス -/ -class HImp (α : Type) where - /-- Heyting 含意 `⇨` -/ - himp : α → α → α - -@[inherit_doc] infixr:60 " ⇨ " => HImp.himp - -/-- `ᶜ` という記号のためのクラス -/ -class HasCompl (α : Type) where - /-- 補元 -/ - compl : α → α - -@[inherit_doc] postfix:1024 "ᶜ" => HasCompl.compl - -/-- Heyting 代数 -/ -class HeytingAlgebra (α : Type) extends Lattice α, Top α, Bot α, HasCompl α, HImp α where - /-- ⊤ は最大元 -/ - le_top : ∀ a : α, a ≤ ⊤ - - /-- ⊥ は最小元 -/ - bot_le : ∀ a : α, ⊥ ≤ a - - /-- `· ⊓ b` の右随伴 `b ⇨ ·` が存在する -/ - le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c - - /-- 補元の定義 -/ - himp_bot (a : α) : a ⇨ ⊥ = aᶜ - -end HeytingAlgebra - -/- ## 問1 Prop は Heyting 代数 - -いよいよ問題です。`Prop` が Heyting 代数のインスタンスであることを示しましょう。 - -しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。 - -こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) の記事が参考になると思います。 - -### 問1.1 半順序集合であること --/ -section PropInstance --# - -/-- `P Q : Prop` に対して、順序関係 `P ≤ Q` を -`P → Q` が成り立つこととして定める -/ -instance : LE Prop where - le a b := a → b - -/-- `P < Q` の定義は `P → Q` かつ同値ではないこと -/ -instance : LT Prop where - lt a b := (a → b) ∧ ¬ (b → a) - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 --- 以下に示すのは一例です: -local add_aesop_rules unsafe 50% tactic [(by apply True.intro)] - -/-- 上記の定義のもとで `Prop` は半順序集合 -/ -instance : PartialOrder Prop where - le_refl := by aesop - le_trans := by aesop - lt_iff_le_not_le := by aesop - le_antisymm := by aesop - -/- ### 問1.2 束であること -/ - -/-- 論理和 `∨` を上限とする -/ -instance : Sup Prop where - sup a b := a ∨ b - -/-- 論理積 `∧` を下限とする -/ -instance : Inf Prop where - inf a b := a ∧ b - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 --- 以下に示すのは一例です: -local add_aesop_rules safe tactic [(by simp only [Nat.add_zero])] - -/-- 上記の定義のもとで `Prop` は束 -/ -instance : Lattice Prop where - le_sup_left := by aesop - le_sup_right := by aesop - sup_le := by aesop - inf_le_left := by aesop - inf_le_right := by aesop - le_inf := by aesop - -/- ### 問1.3 Heyting 代数であること -/ - -/-- `a ⇨ b` には `a → b` を対応させる -/ -instance : HImp Prop where - himp a b := a → b - -/-- `aᶜ` には `¬ a` を対応させる -/ -instance : HasCompl Prop where - compl a := ¬ a - -/-- True が最大元 -/ -instance : Top Prop where - top := True - -/-- False が最小元 -/ -instance : Bot Prop where - bot := False - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 --- 以下に示すのは一例です: -local add_aesop_rules norm simp [Nat.add_zero] - -instance : HeytingAlgebra Prop where - le_top := by aesop - bot_le := by aesop - le_himp_iff := by aesop - himp_bot := by aesop - -end PropInstance --# -/- ## 問2 Bool 代数でない Heyting 代数 -Bool 代数を定義し、Heyting 代数であって Bool 代数でない例を具体的に構成します。これにより、Heyting 代数の公理から Bool 代数の公理を証明することができないことが分かります。 - -反例の集合はシンプルで、３つの要素からなる集合として構成することができます。 --/ -section BooleanCounterExample --# - -/-- Bool 代数 -/ -class BooleanAlgebra (α : Type) extends HeytingAlgebra α where - /-- `x ⊓ xᶜ = ⊥` が成り立つ -/ - inf_compl_le_bot : ∀ x : α, x ⊓ xᶜ ≤ ⊥ - - /-- `⊤ = x ⊔ xᶜ` が成り立つ -/ - top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ - -/-- `{0, 1, 2}` という集合。これが反例になる。 -/ -abbrev Three := Fin 3 - -/- ### 問2.1 半順序集合であること -/ - --- 順序関係が既に定義されている -#synth LE Three - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 - -instance : PartialOrder Three where - le_refl := by aesop - le_trans := by aesop - le_antisymm := by aesop - lt_iff_le_not_le := by aesop - -/- ### 問2.2 束であること -/ - -/-- 上限の定義 -/ -instance : Sup Three where - sup a b := { - val := max a.val b.val - isLt := by omega - } - -/-- 下限の定義 -/ -instance : Inf Three where - inf a b := { - val := min a.val b.val - isLt := by omega - } - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 - -/-- 束になる -/ -instance : Lattice Three where - le_sup_left := by aesop - le_sup_right := by aesop - sup_le := by aesop - inf_le_left := by aesop - inf_le_right := by aesop - le_inf := by aesop - -/- ### 問2.3 Heyting 代数であるが Bool 代数ではないこと -/ - -/-- 最大元は2 -/ -instance : Top Three where - top := 2 - -/-- 最小元は0 -/ -instance : Bot Three where - bot := 0 - -/-- Heyting 含意の定義 -/ -instance : HImp Three where - himp a b := { - val := if a ≤ b then 2 else b.val - isLt := by aesop - } - -/-- 補元の定義 -/ -instance : HasCompl Three where - compl a := { - val := if a = 0 then 2 else 0 - isLt := by aesop - } - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 - -/-- Heyting 代数になる -/ -instance : HeytingAlgebra Three where - le_top := by aesop - bot_le := by aesop - le_himp_iff := by aesop - himp_bot := by aesop - -/-- Three は上記の構成の下で Bool 代数ではない -/ -theorem three_not_boolean : (1 : Three) ⊔ 1ᶜ ≠ ⊤ := by aesop - -end BooleanCounterExample --# diff --git a/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean b/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean deleted file mode 100644 index 60da256b..00000000 --- a/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean +++ /dev/null @@ -1,76 +0,0 @@ -/- # 全射・単射と左逆・右逆写像 - -関数 `f : A → B` が**全射**であるとは、任意の `b : B` に対して `f a = b` となる `a : A` が存在することをいいます。また、`f` が**単射**であるとは、任意の `a₁, a₂ : A` に対して `f a₁ = f a₂` ならば `a₁ = a₂` となることをいいます。 - -これを Lean で表現すると次のようになります。 --/ -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -variable {A B : Type} - -/-- 関数の全射性 -/ -def Function.Surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b - -/-- 関数の単射性 -/ -def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a₂ → a₁ = a₂ - -/- 一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。 - -しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](#{root}/Reference/Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。 - -ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。 --/ - -/- ## 問1: 全射から逆方向の単射 -まずは、全射 `f : A → B` が存在すれば逆方向の単射 `g : B → A` も存在することを示しましょう。 - -実際にはより強く、`f ∘ g = id` を満たすような `g` が構成できます。一般に、`f ∘ g = id` が成り立つとき、`g` を `f` の右逆写像であるとか、切断(section)であるとかいいます。 --/ - --- 選択原理を使用する -open Function Classical - -/-- 全射 `f : A → B` があれば、選択原理を使用することにより -単射 `g : B → A` を作ることができる。-/ -theorem surj_to_inj (f : A → B) (hsurj : Surjective f) - : ∃ g : B → A, Injective g := by - -- まず `g` を構成する。 - -- 任意の `b : B` に対して `f` の全射性より - -- `f a = b` となる `a : A` が存在するのでそれを返す。 - let g : B → A := fun b => sorry - - -- `g` の定義と `f` の全射性から、`f (g b) = b` が成り立つ。 - have gdef : ∀ b, f (g b) = b := by - sorry - - -- `f ∘ g = id` を使って、 - -- `g` が単射であることを示す。 - sorry - -/- ## 問2: 単射から逆方向の全射 -次に `f : A → B` が単射であれば、逆方向の全射 `g : B → A` も存在することを示しましょう。 - -これも実際にはより強く、`g ∘ f = id` を満たすような `g` が構成できます。一般に、`g ∘ f = id` が成り立つとき、`g` を `f` の左逆写像であるとか、引き込み(retraction)であるとかいいます。 - -```admonish warning title="注意" -`A` が空の時には関数 `g : B → A` は構成することができないため、`A` が空でないという仮定が必要です。それは `Inhabited A` という引数により表現されています。 -``` --/ - -/-- 単射 `f : A → B` があれば、選択原理を使用することにより -全射 `g : B → A` を作ることができる。 -/ -theorem inj_to_surj [Inhabited A] (f : A → B) (hinj : Injective f) - : ∃ g : B → A, Surjective g := by - -- まず `g` を構成する。 - -- `g b` の値を構成するために、`b : B` が `f` の像に入っているかで場合分けをし、 - -- 入っていなければ適当な値、入っていれば `b = f a` となる `a` を返すようにする。 - let g : B → A := fun b => sorry - - -- `g` の定義と `f` の単射性から、`g (f a) = a` が成り立つ。 - have gdef : ∀ a, g (f a) = a := by - sorry - - -- `g ∘ f = id` を使って、 - -- `g` が全射であることを示す。 - sorry diff --git a/LeanByExample/Tutorial/Exercise/KnightAndKnave.lean b/LeanByExample/Tutorial/Exercise/KnightAndKnave.lean deleted file mode 100644 index a61ee639..00000000 --- a/LeanByExample/Tutorial/Exercise/KnightAndKnave.lean +++ /dev/null @@ -1,155 +0,0 @@ -/- # 騎士と悪党のパズル - -騎士(Knight)と悪党(Knave)の論理パズルは、著名な論理学者 Raymond Smullyan によって考案されたとされています。それ以来様々な変種が考案され続けてきました。ここでは、その中でも基本的なものを Lean で形式化し、解いていきます。 - -## 概要 - -[Critical thinking web](https://philosophy.hku.hk/think/logic/knights.php) から問題を引用します。まずは自然言語で問題文を述べましょう。 - -```admonish info title="" -ある島には、騎士と悪党しか住んでいません。すべての島民は騎士であるか悪党であるかのいずれかです。騎士が話すことは常に真であり、悪党が話すことは常に偽です。 - -あなたはゾーイとメルという２人の島民に出会いました。 -ゾーイは「メルは悪党です」と言いました。 -メルは「ゾーイも私も悪党ではありません」と言いました。 -さて、ゾーイとメルはそれぞれ騎士か悪党のどちらでしょうか？ -``` - -## 形式化 - -さっそく形式化を行っていきます。まず、ある島があってそこには騎士と悪党しか住んでいないというところですが、これは `Islander` という型に `knight` と `knave` という部分集合が存在するというように形式化できます。そのうえで、島民が騎士か悪党のどちらかであることを `axiom` コマンドで仮定しましょう。 - -ここでは後で便利なように `simp` 補題も示しておくことにします。 --/ -import Lean --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- その島の住民を表す型 -/ -opaque Islander : Type - -/-- Islander の部分集合として定義した騎士の全体 -/ -opaque knight : Islander → Prop - -/-- Islander の部分集合として定義した悪党の全体 -/ -opaque knave : Islander → Prop - -/-- 人は騎士か悪党のどちらか -/ -axiom knight_or_knave (p : Islander) : knight p ∨ knave p - -/-- 人が騎士かつ悪党であることはない -/ -axiom knight_ne_knave (p : Islander) : ¬(knight p ∧ knave p) - -/-- 騎士でないことと悪党であることは同値 -/ -@[simp] theorem of_not_knight {p : Islander} : ¬ knight p ↔ knave p := by - have or := knight_or_knave p - have ne := knight_ne_knave p - constructor - all_goals - intro h - simp_all - -/-- 悪党でないことと騎士であることは同値 -/ -@[simp] theorem of_not_knave {p : Islander} : ¬ knave p ↔ knight p := by - have or := knight_or_knave p - have ne := knight_ne_knave p - constructor - all_goals - intro h - simp_all - -/- これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。-/ - -/-- ゾーイ -/ -axiom zoey : Islander - -/-- メル -/ -axiom mel : Islander - -/- 正直者であるとか嘘つきであるということを表現するために、誰がなんと発言したかを表現するための関数を用意します。その上で、それぞれの発言を愚直に形式化していきます。 -/ - -/-- p さんが body という命題を話したという事実を表す命題 -/ -opaque Islander.say (p : Islander) (body : Prop) : Prop - -variable {p : Islander} {body : Prop} - -/-- 騎士の発言内容はすべて真実 -/ -axiom statement_of_knight (h : knight p) (say : p.say body) : body - -/-- 悪党の発言内容はすべて偽 -/ -axiom statement_of_knave (h : knave p) (say : p.say body) : ¬body - -/-- ゾーイは「メルは悪党だ」と言った -/ -axiom zoey_says : zoey.say (knave mel) - -/-- メルは「ゾーイもメルも悪党ではない」と言った -/ -axiom mel_says : mel.say (¬ knave zoey ∧ ¬ knave mel) - -/- ここまでで問題文の前提部分の形式化は完了です。 - -残っているのは、「ゾーイとメルはそれぞれ騎士か悪党のどちらですか」と問う部分です。これは少し難しいです。 - -考えてみると、Lean で（証明すべき命題がわかっているときに）何かを証明するのはよくありますが、与えられた前提から何が言えるのかを明確なゴールなしに組み立てていくのはあまり見ないということにお気づきになるでしょう。この問題も、もし問いの内容が「ゾーイが騎士であることを示せ」とか「ゾーイが悪党であることを示せ」だったならば、今までの準備の下で簡単に形式化ができますが、「騎士なのか悪党なのか決定せよ」なので少し複雑になります。 - -ここでの解決方法は、`Solution` という帰納型を `inductive` コマンドで作成し、その項を作ってくださいという形式にすることです。 --/ - -/-- `p` が騎士か悪党のどちらなのか知っていることを表す型 -/ -inductive Solution (p : Islander) : Type where - | isKnight : knight p → Solution p - | isKnave : knave p → Solution p - -/- この `Solution` の項を、`p : Islander` に対して作成するときに、項が `isKnight` から来るのか `isKnave` から来るのか明示しなければなりません。そしてそのために、それぞれ `p` が騎士であるか悪党であるかのどちらかの証明が引数に要求されることになるので、問題文を表現しているといえます。 - -## 問題 - -以上の準備の下で、問題は次のように表現できます。以下の `sorry` の部分を埋めてください。 - -```admonish error title="禁止事項" -この問題では選択原理 `Classical.choice` の使用は禁止です。 -解答を書いた後で、`zoey_which` と `mel_which` に対して `#print axioms` コマンドを使用し、選択原理を使用していないことを確認してください。 - -余裕があればなぜ禁止なのか考えてみましょう。 -``` --/ - -/-- ゾーイは騎士か悪党か？-/ -noncomputable def zoey_which : Solution zoey := by - sorry - -/-- メルは騎士か悪党か？-/ -noncomputable def mel_which : Solution mel := by - sorry - ---#-- -section -/- ## 選択原理を使用していないことを確認するコマンド -/ - -open Lean Elab Command - -elab "#detect_classical " id:ident : command => do - -- 識別子(ident)を Name に変換 - let constName ← liftCoreM <| realizeGlobalConstNoOverload id - - -- 依存する公理を取得 - let axioms ← collectAxioms constName - - -- 依存公理がなかったときの処理 - if axioms.isEmpty then - logInfo m!"'{constName}' does not depend on any axioms" - return () - - -- Classical で始まる公理があるかどうかチェック - -- もしあればエラーにする - let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm - if caxes.isEmpty then - logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}" - else - throwError m!"'{constName}' depends on classical axioms: {caxes.toList}" - -end - --- 選択原理を使用していないことを確認 -#detect_classical zoey_which -#detect_classical mel_which ---#-- diff --git a/LeanByExample/Tutorial/Exercise/README.lean b/LeanByExample/Tutorial/Exercise/README.lean deleted file mode 100644 index 08da3333..00000000 --- a/LeanByExample/Tutorial/Exercise/README.lean +++ /dev/null @@ -1,21 +0,0 @@ -/- # 演習問題 -このセクションでは、演習問題を扱います。ぜひ新しいパズルゲームだと思って挑戦してみてください。 - -## 🎮 遊び方 - -問題は、前提となるライブラリや知識が少なく、難易度が低いと思われる順に並べてあります。興味があるものから挑戦してみましょう。 - -解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。 - -あるいは、Codespace を開き、`LeanByExample/Tutorial/Exercise` ディレクトリの中にある該当ファイルを開いてもよいです。 - -[![codespace badge](https://github.com/codespaces/badge.svg)](https://codespaces.new/lean-ja/lean-by-example) - -お使いの PC に Lean をインストール済みであれば、このリポジトリをクローンして VSCode で開いてください。 - -## ❓ どうしてもわからないとき - -時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 - -しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。 --/ diff --git a/LeanByExample/Tutorial/Solution/BarberParadox.lean b/LeanByExample/Tutorial/Solution/BarberParadox.lean deleted file mode 100644 index 200c203e..00000000 --- a/LeanByExample/Tutorial/Solution/BarberParadox.lean +++ /dev/null @@ -1,45 +0,0 @@ -/- # 床屋のパラドックス -集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。 - -この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。 - -以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。 - -その内容は自然言語では次のように説明できます。 - -```admonish info title="" -ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？ - -仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。 - -いずれにせよ矛盾が生じてしまうので、そんな床屋は存在しません！ -``` - -この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。 --/ -namespace Barber -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- 全体集合となる人々の集合 -/ -opaque Person : Type - -/-- p さんが q さんの髭を剃るという述語 -/ -opaque shave (p q : Person) : Prop - --- 床屋が存在するという仮定 -variable (barber : Person) - --- 床屋の信念を仮定として表現したもの -variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p) - -example : False := by - -- sorry - -- 床屋は自分自身の髭を剃るだろうか？ - replace policy := policy barber - - -- `P ↔ ¬ P` という形の仮定が得られて、これは矛盾 - simp at policy - -- sorry - -end Barber diff --git a/LeanByExample/Tutorial/Solution/CantorPairing.lean b/LeanByExample/Tutorial/Solution/CantorPairing.lean deleted file mode 100644 index 1bceaec2..00000000 --- a/LeanByExample/Tutorial/Solution/CantorPairing.lean +++ /dev/null @@ -1,192 +0,0 @@ -/- # Cantor の対関数とその全単射性 - -## はじめに - -有限集合 `A` と `B` に対して、`A` と `B` の要素数が等しいということは、`|A| = |B| = n` となる自然数 `n` が存在するということと同値です。無限集合 `X` に対しては `|X| = n` となる自然数 `n` は存在しないので、一見すると集合の要素数という概念は無限集合には拡張できないように思えます。 - -しかし、`A` と `B` の要素数が等しいということは、「`A` と `B` の間の一対一で漏れのない対応が存在する」ということとも同値です。この定義は `A` と `B` が無限集合であっても意味をなすので、この解釈をつかって集合の要素数が等しいという概念を無限集合にも拡張することができます。 - -だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。 - -無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note] - -## 問1: sum 関数 - -まず後で使うために `0` から `n` までの自然数の和を計算する関数 `sum` を定義します。演習として、以下の `sorry` を埋めてみてください。 --/ -import Mathlib.Tactic -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- `0` から `n` までの自然数の和 -/ -def sum (n : ℕ) : ℕ := - match n with - | 0 => 0 - | n + 1 => (n + 1) + sum n - -/-- `sum n = 0` となることと `n = 0` は同値 -/ -@[simp] theorem sum_zero_iff_zero {n : ℕ} : sum n = 0 ↔ n = 0 := by - -- sorry - cases n <;> simp_all [sum] - -- sorry - -/- ## 対関数とその逆関数 -上記で定義した `sum` を使いつつ、Cantor の対関数 `pair` とその逆関数 `unpair` を定義します。座標平面の中心からスタートして、折れ曲がりながら右上に向かうような動きをイメージするとわかりやすいかもしれません。 --/ - -/-- Cantor の対関数 -/ -def pair : ℕ × ℕ → ℕ - | (m, n) => sum (m + n) + m - -@[simp] theorem pair_zero : pair 0 = 0 := by rfl - -/-- カントールの対関数の逆関数 -/ -def unpair : ℕ → ℕ × ℕ - | 0 => (0, 0) - | x + 1 => - let (m, n) := unpair x - if n = 0 then (0, m + 1) - else (m + 1, n - 1) - -@[simp] theorem unpair_zero : unpair 0 = 0 := by rfl - -/- ## 問2: pair の全射性 -では `pair` が全射であることを示してみましょう。`pair ∘ unpair = id` が成り立つことを示せば十分です。以下の `sorry` の部分を埋めて証明を完成させてください。 --/ - -/-- `pair ∘ unpair = id` が成り立つ。特に `pair` は全射。-/ -theorem pair_unpair_eq_id (x : ℕ) : pair (unpair x) = x := by - -- `x` に対する帰納法を使う - induction' x with x ih - - -- `x = 0` の場合は明らか - case zero => /- sorry -/ simp - - -- `x` まで成り立つと仮定して `x + 1` でも成り立つことを示そう。 - case succ => - -- まず `unpair` の定義を展開する。 - dsimp [unpair] - split_ifs - - -- 見やすさのために `(m, n) := unpair x` とおく． - all_goals - set m := (unpair x).fst with mh - set n := (unpair x).snd with nh - - -- `n = 0` の場合 - case pos h => - -- `pair (0, m + 1) = x + 1` を示せばよい。 - show pair (0, m + 1) = x + 1 - - -- `pair` の定義を展開して、示すべきことを `sum` を使って書き直すと - -- `sum (m + 1) = x + 1` を示せば良いことが分かる。 - suffices sum (m + 1) = x + 1 from by - -- sorry - simpa [pair] - -- sorry - - -- 帰納法の仮定の主張に対しても、 - -- `pair` から `sum` に書き換えることができて、 - -- `sum m + m = x` であることが分かる。 - replace ih : sum m + m = x := by - -- sorry - simpa [pair, ←mh, ←nh, h] using ih - -- sorry - - -- 後は `sum` の定義から明らか。 - -- sorry - dsimp [sum] - omega - -- sorry - - -- `n ≠ 0` の場合 - case neg h => - -- `pair (m + 1, n - 1) = x + 1` を示せばよい。 - show pair (m + 1, n - 1) = x + 1 - - -- `pair` の定義を展開して、示すべきことを `sum` を使って書き直すと - -- `sum (m + n) + m = x` を示せば良いことが分かる。 - suffices sum (m + n) + m = x from by - -- sorry - simp only [pair] - rw [show m + 1 + (n - 1) = m + n from by omega] - omega - -- sorry - - -- 帰納法の仮定の主張に対しても、 - -- `pair` から `sum` に書き換えることができて、 - -- `sum (m + n) + m = x` が成り立つことが分かる。 - replace ih : sum (m + n) + m = x := by - -- sorry - simpa [pair, unpair, ← mh, ← nh] using ih - -- sorry - - -- 従って示すべきことが言えた。 - assumption - -/- ## 問3: 対関数の単射性 -最後に `pair` が単射であることを示してみましょう。`unpair ∘ pair = id` が成り立つことを示せば十分です。以下の `sorry` の部分を埋めて証明を完成させてください。 --/ - -/-- `unpair ∘ pair = id` が成り立つ。特に `pair` は単射。-/ -theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by - -- `x = pair (m, n)` として `x` に対する帰納法を利用する - induction' h : pair (m, n) with x ih generalizing m n - - -- `pair (m, n) = 0` のときは - -- `pair` の定義から明らか。 - case zero => /- sorry -/ simp_all [pair] - - -- `pair (m, n) = x + 1` のとき - case succ => - -- `m` がゼロかそうでないかで場合分けする - match m with - - -- `m = 0` のとき - | 0 => - -- `pair (0, n) = x + 1` により `n > 0` が成り立つ。 - have npos : n > 0 := by - -- sorry - rw [show n > 0 ↔ n ≠ 0 from Nat.pos_iff_ne_zero] - aesop - -- sorry - - -- よって `sum n = sum (n - 1) + n` と書くことができて、 - have lem : sum n = sum (n - 1) + n := by - -- sorry - nth_rw 1 [show n = (n - 1) + 1 from by omega] - dsimp only [sum] - omega - -- sorry - - -- `pair (n - 1, 0) = x` が結論できる。 - have : pair (n - 1, 0) = x := by - -- sorry - simp_all [pair] - omega - -- sorry - - -- 後は帰納法の仮定から従う。 - -- sorry - specialize ih (n-1) 0 this - simp [unpair, ih] - omega - -- sorry - - -- `m = m' + 1` のとき - | m' + 1 => - -- `pair` の定義から `pair (m', n + 1) = x` が成り立つ。 - have : pair (m', n + 1) = x := by - -- sorry - dsimp [pair] at h ⊢ - rw [show m' + 1 + n = m' + (n + 1) from by ac_rfl] at h - omega - -- sorry - - -- 後は帰納法の仮定から従う。 - -- sorry - specialize ih m' (n + 1) this - simp [unpair, ih] - -- sorry - -/- [^note]: 本項での証明を書くにあたって [Cantor の対関数の全単射性の証明](http://iso.2022.jp/math/pairing_function.pdf) を参考にいたしました。 -/ diff --git a/LeanByExample/Tutorial/Solution/CantorTheorem.lean b/LeanByExample/Tutorial/Solution/CantorTheorem.lean deleted file mode 100644 index cf769604..00000000 --- a/LeanByExample/Tutorial/Solution/CantorTheorem.lean +++ /dev/null @@ -1,247 +0,0 @@ -/- # Cantor の定理 - -Cantor の定理とは、次のような定理です。 - -```admonish info title="" -どんな集合 `A` に対しても `A` より `A` のベキ集合 `𝒫 A` の方が真に濃度が大きくなります。 - -ただしここで「真に濃度が大きい」とは、 - -1. `A` から `𝒫 A` への全射が存在しない -1. `𝒫 A` から `A` への単射が存在しない - -ということを意味しています。 -``` - -「濃度」とは、集合の「要素の個数」という概念を無限集合にも拡張したものであり、おおむね「一対一で漏れのない対応がつけられるならば、要素数が等しいと言ってよいだろう」というアイデアに基づくものです。 - -この Cantor の定理はよく知られたものであり、Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。 --/ - -/- ## 集合論の形式化 - -### 全体集合を固定する - -まず、集合の概念を Lean で表現する必要があります。 - -Lean の型 `T : Type` は直観的には「項の集まり」を意味するので、これをそのまま集合だと考えてしまって、`t : T` をもって `t ∈ T` であると見なせばよいように思えるかもしれません。しかし Lean の型システムの性質上、この解釈は途中で破綻します。 - -たとえば `S T : Type` に対して共通部分の `S ∩ T` の要素は `S` にも `T` にも属していなくてはいけませんが、これは型の一意性から実現できません。`S ∪ T` についても同様で、`S` にも `S ∪ T` にも属している要素に正しく型をつけることができません。 - -そこで全体集合 `α : Type` を固定して、その中に含まれる集まりだけを考えることにします。 --/ -import Lean --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- α を全体集合として、その部分集合の全体。 -α の部分集合と α 上の述語を同一視していることに注意。 -/ -def Set (α : Type) := α → Prop - -variable {α : Type} - -/-- `a : α` は集合 `s` に属する。数学では普通 `a ∈ s` と書かれる。 -/ -def Set.mem (s : Set α) (a : α) : Prop := s a - -/-- `s a` を `a ∈ s` と書けるようにする。 -/ -instance : Membership α (Set α) := ⟨Set.mem⟩ - -/-- `A B : Set α` に対する共通部分 -/ -def Set.inter (A B : Set α) : Set α := fun x => x ∈ A ∧ x ∈ B - -/-- `A B : Set α` に対する合併 -/ -def Set.union (A B : Set α) : Set α := fun x => x ∈ A ∨ x ∈ B - -/- このようにしておくと、上記の問題は回避することができ、`S T : Set α` の共通部分や合併をとることができます。 - -### 内包記法の定義 - -「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 `p : α → Prop` に対して内包記法 `{x : α | p x}` が使用できるようにしましょう。 - -Lean のメタプログラミングフレームワークの力を借りれば、そうしたことも可能です。 --/ -section --# - -variable {α : Type} - -/-- 述語 `p : α → Prop` に対応する集合 -/ -def setOf {α : Type} (p : α → Prop) : Set α := p - -/-- 内包表記 `{ x : α | p x }` の `x : α` の部分のための構文。 -`: α` の部分はあってもなくてもよいので `( )?` で囲っている。-/ -syntax extBinder := ident (" : " term)? - -/-- 内包表記 `{ x : α | p x }` の `{ | }` の部分のための構文。 -/ -syntax (name := setBuilder) "{" extBinder " | " term "}" : term - -/-- 内包表記の意味をマクロとして定義する -/ -macro_rules - | `({ $x:ident : $type | $p }) => `(setOf (fun ($x : $type) => $p)) - | `({ $x:ident | $p }) => `(setOf (fun ($x : _) => $p)) - --- 内包表記が使えるようになったが、コマンドの出力や infoview では --- いま定義した記法が使われないという問題がある -/-- info: setOf fun n => ∃ m, n = 2 * m : Set Nat -/ -#guard_msgs in - #check {n : Nat | ∃ m, n = 2 * m} - -/-- infoview やコマンドの出力でも内包表記を使用するようにする -/ -@[app_unexpander setOf] -def setOf.unexpander : Lean.PrettyPrinter.Unexpander - | `($_ fun $x:ident => $p) => `({ $x:ident | $p }) - | `($_ fun ($x:ident : $ty:term) => $p) => `({ $x:ident : $ty:term | $p }) - | _ => throw () - --- 正常に動作することを確認 - -/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/ -#guard_msgs in - #check {n | ∃ m, n = 2 * m} - -/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/ -#guard_msgs in - #check {n : Nat | ∃ m, n = 2 * m} - -end --# - -/- ### 全射と単射 -関数 `f : A → B` が全射であるとは、任意の `b : B` に対して `f a = b` となる `a : A` が存在することです。また、`f` が単射であるとは、任意の `a₁, a₂ : A` に対して `f a₁ = f a₂` ならば `a₁ = a₂` となることです。 - -これを Lean で表現すると次のようになります。 --/ -section --# - -variable {α β : Type} - -/-- 関数の全射性 -/ -def Function.Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b - -/-- 関数の単射性 -/ -def Function.Injective (f : α → β) : Prop := ∀ {a₁ a₂ : α}, f a₁ = f a₂ → a₁ = a₂ - -end --# -/- -```admonish warning title="注意" -上記の定義を見て、関数の定義域と値域が `A B : Set α` ではなくて `α β : Type` であることに違和感を感じられたかもしれません。型と集合は異なると上で書いたばかりなのに、なぜここでは型を使っているのでしょうか？ - -実際に `A B : Set α` に対して関数の集合 `Hom A B` を定義しようとすると、その理由がわかるかもしれません。 - -`f ∈ Hom A B` が持つべき性質として `a ∈ A → f a ∈ B` があります。`A : Set α` と `B : Set α` をそれぞれ部分型 `{ a : α // a ∈ A }`, `{b : α // b ∈ B}` と同一視すれば、`Hom A B` は関数型 `{ a : α // a ∈ A } → { b : α // b ∈ B }` になります。 - -結局関数型を考えていることになるので、`α β : Type` について考えれば十分だということになるわけです。 -``` --/ - -/- ## 問1: 全射バージョン -以上の準備のもとで、Cantor の定理を証明することができます。まずは全射バージョンから示しましょう。次の `sorry` の部分を埋めてください。 --/ -section --# - -variable {α : Type} - -open Function - -/-- ある集合からそのベキ集合への全射は存在しない -/ -theorem cantor_surjective (f : α → Set α) : ¬ Surjective f := by - -- `f` が全射であると仮定する - intro hsurj - - -- 反例になる集合 `A` を構成する - -- `α` の部分集合 `A : Set α` を `{a | a ∉ f a}` で定義する --## - let A : Set α := /- sorry -/ {a | a ∉ f a} - - -- `f` は全射なので、ある `a` が存在して `f a = A` - obtain ⟨a, ha⟩ := hsurj A - - -- `a ∈ A` は `a ∉ A` と同値である - have : a ∈ A ↔ a ∉ A := by - -- sorry - -- `f a = A` なので `a ∉ A` は `a ∉ f a` と同値 - rw [show (a ∉ A) = (a ∉ f a) from by rw [ha]] - - -- `A` の定義から `a ∈ A` は `a ∉ f a` と同値 - rw [show (a ∈ A) ↔ (a ∉ f a) from by rfl] - -- sorry - - -- これは矛盾 - simp at this - -/- ## 問2: 単射バージョン -単射バージョンも示すことができます。次の `sorry` の部分を埋めてください。 --/ - -/-- ベキ集合から元の集合への単射は存在しない -/ -theorem cantor_injective (f : Set α → α) : ¬ Injective f := by - -- `f` が単射だと仮定する - intro hinj - - -- 反例になる集合 `A` を構成する - -- `α` の部分集合 `A : Set α` を `{f B | f B ∉ B}` で定義する --## - let A : Set α := /- sorry -/ {a | ∃ B : Set α, a = f B ∧ f B ∉ B} - - -- このとき `f A ∈ A` と `f A ∉ A` が同値になる - have : (f A ∈ A) ↔ (f A ∉ A) := by - -- sorry - constructor - - -- 左から右を示す - case mp => - -- `f A ∈ A` と仮定する - intro hmem - exfalso - - -- `f A ∈ A` なので `A` の定義から、 - -- ある `B : Set α` が存在して `f A = f B` かつ `f B ∉ B` - have ⟨B, hf, hB⟩ := hmem - - -- `f` は単射なので `A = B` である - have hAB : A = B := hinj hf - - -- これは `f A ∉ A` を意味し、矛盾 - rw [← hAB] at hB - contradiction - - -- 右から左を示す - case mpr => - -- `f A ∉ A` と仮定する - intro hmem - - -- `A` の定義により、これはまさに `f A ∈ A` を意味する - -- よって矛盾 - exact ⟨A, rfl, hmem⟩ - -- sorry - - -- これは矛盾である - simp at this -end --# - -/- -```admonish warning title="注意" -[全射(単射)が存在することと、逆方向の単射(全射)が存在することはほぼ同値](./InverseSurjInj.md)なので、それを使えば全射バージョンに帰着して示せることにお気づきでしょうか。しかし、それをそのまま使うと選択原理を使用することになります。ここでは選択原理は必要ありません。 -``` --/ - ---#-- -section -/- ## 選択原理を使用していないことを確認するコマンド -/ - -open Lean Elab Command - -elab "#detect_classical " id:ident : command => do - let constName ← liftCoreM <| realizeGlobalConstNoOverload id - let axioms ← collectAxioms constName - if axioms.isEmpty then - logInfo m!"'{constName}' does not depend on any axioms" - return () - let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm - if caxes.isEmpty then - logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}" - else - throwError m!"'{constName}' depends on classical axioms: {caxes.toList}" - -end - --- 選択原理を使用していないことを確認 -#detect_classical cantor_surjective -#detect_classical cantor_injective ---#-- diff --git a/LeanByExample/Tutorial/Solution/DoubtImplication.lean b/LeanByExample/Tutorial/Solution/DoubtImplication.lean deleted file mode 100644 index ce3bc70d..00000000 --- a/LeanByExample/Tutorial/Solution/DoubtImplication.lean +++ /dev/null @@ -1,123 +0,0 @@ -/- # 「ならば」の定義を疑う - -## イントロダクション - -論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学や Lean では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。 - -自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！ - -この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。 - -## 含意が満たしていて欲しい性質 - -まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2変数関数になっているとします。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。 --/ -import Lean --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# --- 含意が満たすべき性質を満たす「何か」 -opaque Imp (P Q : Prop) : Prop - --- 含意っぽい記法の導入 --- `v` は `virtual` の略 -infixr:40 " →ᵥ " => Imp - -/- これだけだと型があるだけで中身がないので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？ `P →ᵥ Q` がおおよそ「`P` を仮定すると `Q` が示せる」という意味になるようにしたいと考えると、次のようなものが考えられるでしょう。 -/ -namespace Imp --# - -variable {P Q R : Prop} - -/-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/ -axiom imp_reflexive : P →ᵥ P - -/-- 含意は推移的 -/ -axiom imp_transitive (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R - -/-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/ -axiom imp_elim (hpq : P →ᵥ Q) (hP : P) : Q - -/-- 結論が無条件に正しいなら、仮定をつけても正しい -/ -axiom imp_intro (hQ : Q) : P →ᵥ Q - -/-- ある前提から `Q` と `R` が導出できるなら、`Q ∧ R` も導出できる -/ -axiom intro_and (hpq : P →ᵥ Q) (hpr : P →ᵥ R) : P →ᵥ (Q ∧ R) - -/-- ある前提から `Q ∧ R` が導出できるなら、`Q` も導出できる -/ -axiom elim_and_left (h : P →ᵥ (Q ∧ R)) : P →ᵥ Q - -/-- ある前提から `Q ∧ R` が導出できるなら、`R` も導出できる -/ -axiom elim_and_right (h : P →ᵥ (Q ∧ R)) : P →ᵥ R - -/-- ある前提から `Q` が導出できるなら、`Q ∨ R` が導出できる -/ -axiom intro_or_left (h : P →ᵥ Q) : P →ᵥ (Q ∨ R) - -/-- ある前提から `R` が導出できるなら、`Q ∨ R` が導出できる -/ -axiom intro_or_right (h : P →ᵥ R) : P →ᵥ (Q ∨ R) - -end Imp --# - -/- ## 問題 -以上の要請のもとで、`P →ᵥ Q` が `P → Q` に一致することが証明できます。 - -以下の `sorry` を埋めてみてください。ただし、以下のことに注意してください。 - -* 仮定した要請を全部使う必要はありません。 -* 古典論理に限った話ではないので、排中律を使わずに証明してみてください。 - --/ - -variable {P Q : Prop} - -open Imp - -/-- 上記の要請を満たす `→ᵥ` は通常の含意と一致する -/ -theorem imp_valid {P Q : Prop} : (P →ᵥ Q) ↔ (P → Q) := by - -- sorry - -- 同値の両方向を示す - constructor <;> intro h - - -- 左から右を示す - case mp => - intro hP - - -- モーダスポネンスから従う - exact imp_elim h hP - - -- 右から左を示す - case mpr => - have : P →ᵥ (P ∧ Q) := by - -- 同値な命題は入れ替えても良いので、`P ∧ Q` は `P ∧ (P → Q)` と入れ替えられる - rw [show (P ∧ Q) ↔ P ∧ (P → Q) from by simp_all] - - -- よって `intro_and` に帰着できる - apply intro_and - (show P →ᵥ P from imp_reflexive) - (show P →ᵥ (P → Q) from imp_intro h) - - -- 後は `elim_and_right` から従う - apply elim_and_right this - -- sorry - ---#-- -section -/- ## 選択原理を使用していないことを確認するコマンド -/ - -open Lean Elab Command - -elab "#detect_classical " id:ident : command => do - let constName ← liftCoreM <| realizeGlobalConstNoOverload id - let axioms ← collectAxioms constName - if axioms.isEmpty then - logInfo m!"'{constName}' does not depend on any axioms" - return () - let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm - if caxes.isEmpty then - logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}" - else - throwError m!"'{constName}' depends on classical axioms: {caxes.toList}" - -end - --- 選択原理を使用していないことを確認 -#detect_classical imp_valid ---#-- diff --git a/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean b/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean deleted file mode 100644 index 5f7869b0..00000000 --- a/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean +++ /dev/null @@ -1,328 +0,0 @@ -/- # Heyting 代数と Bool 代数 -直観主義論理において、排中律 `P ∨ ¬ P` は独立な命題であることが知られています。つまり、証明も反証(否定を証明すること)もできません。今回の演習問題では、それに関連した話題として、Bool 代数ではない Heyting 代数が存在することを示します。 - -ここでは Mathlib をなぞるように理論を構成していきます。 - -## 半順序集合 -まず準備として、半順序集合を定義します。半順序集合には順序が定義されていますが、要素を2つ与えられたときにどちらが大きいのか比較できるとは限らないことに注意してください。 --/ -import Aesop --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- 半順序集合 -/ -class PartialOrder (α : Type) extends LE α, LT α where - /-- `≤` は反射的である -/ - le_refl : ∀ a : α, a ≤ a - - /-- `≤` は推移的である -/ - le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c - - /-- `<` のデフォルト実装 -/ - lt := fun a b => a ≤ b ∧ ¬ b ≤ a - - /-- `<` と `≤` の関係 -/ - lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a - - /-- `≤` は半対称的 -/ - le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b - -/- ## 束 -半順序集合であって、任意の2つの要素 `a, b` に対して上限 `a ⊔ b` と下限 `a ⊓ b` が存在するものを束といいます。上限は最小の上界を意味し、下限は最大の下界を意味します。 - -上限の記号 `⊔` は論理和 `∨` に、下限の記号 `⊓` は論理積 `∧` に、それぞれ似ています。またそれぞれ集合の合併 `∪` と共通部分 `∩` にも似ています。これは、`Prop` と `Set α` がともに束になっていることと整合性があります。 --/ - -section Lattice - -/-- `⊔` という記号のための型クラス -/ -class Sup (α : Type) where - /-- 最小上界、上限 -/ - sup : α → α → α - -/-- `⊓` という記号のための型クラス -/ -class Inf (α : Type) where - /-- 最大下界、下限 -/ - inf : α → α → α - -@[inherit_doc] infixl:68 " ⊔ " => Sup.sup - -@[inherit_doc] infixl:69 " ⊓ " => Inf.inf - -/-- 任意の2つの要素 `a, b` に対して上限 `a ⊔ b` が存在するような半順序集合 -/ -class SemilatticeSup (α : Type) extends Sup α, PartialOrder α where - /-- `a ⊔ b` は `a` と `b` の上界になっている -/ - le_sup_left : ∀ a b : α, a ≤ a ⊔ b - - /-- `a ⊔ b` は `a` と `b` の上界になっている -/ - le_sup_right : ∀ a b : α, b ≤ a ⊔ b - - /-- `a ⊔ b` は `a`, `b` の上界の中で最小のもの -/ - sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c - -/-- 任意の2つの要素 `a, b` に対して下限 `a ⊓ b` が存在するような半順序集合 -/ -class Semilatticeinf (α : Type) extends Inf α, PartialOrder α where - /-- `a ⊓ b` は `a` と `b` の下界になっている -/ - inf_le_left : ∀ a b : α, a ⊓ b ≤ a - - /-- `a ⊓ b` は `a` と `b` の下界になっている -/ - inf_le_right : ∀ a b : α, a ⊓ b ≤ b - - /-- `a ⊓ b` は `a`, `b` の下界の中で最大のもの -/ - le_inf : ∀ a b c : α, c ≤ a → c ≤ b → c ≤ a ⊓ b - -set_option structureDiamondWarning false in --# -/-- 束 -/ -class Lattice (α : Type) extends SemilatticeSup α, Semilatticeinf α - -end Lattice - -/- ## Heyting 代数 -ここまでの準備の下、Heyting 代数を定義することができます。Heyting 代数とは束であって、以下の条件を満たすものです。 - -1. 最大の要素 `⊤` が存在する。 -2. 最小の要素 `⊥` が存在する。 -3. 下限 `· ⊓ b` の右随伴 `b ⇨ ·` が存在する。つまり任意の `a, b, c` に対して `a ⊓ b ≤ c` と `a ≤ b ⇨ c` が同値。 --/ - -section HeytingAlgebra - -/-- `⊤` という記号のための型クラス -/ -class Top (α : Type) where - /-- 最大元 -/ - top : α - -@[inherit_doc] notation "⊤" => Top.top - -/-- `⊥` という記号のための型クラス -/ -class Bot (α : Type) where - /-- 最小元 -/ - bot : α - -@[inherit_doc] notation "⊥" => Bot.bot - -/-- `⇨` という記号のための型クラス -/ -class HImp (α : Type) where - /-- Heyting 含意 `⇨` -/ - himp : α → α → α - -@[inherit_doc] infixr:60 " ⇨ " => HImp.himp - -/-- `ᶜ` という記号のためのクラス -/ -class HasCompl (α : Type) where - /-- 補元 -/ - compl : α → α - -@[inherit_doc] postfix:1024 "ᶜ" => HasCompl.compl - -/-- Heyting 代数 -/ -class HeytingAlgebra (α : Type) extends Lattice α, Top α, Bot α, HasCompl α, HImp α where - /-- ⊤ は最大元 -/ - le_top : ∀ a : α, a ≤ ⊤ - - /-- ⊥ は最小元 -/ - bot_le : ∀ a : α, ⊥ ≤ a - - /-- `· ⊓ b` の右随伴 `b ⇨ ·` が存在する -/ - le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c - - /-- 補元の定義 -/ - himp_bot (a : α) : a ⇨ ⊥ = aᶜ - -end HeytingAlgebra - -/- ## 問1 Prop は Heyting 代数 - -いよいよ問題です。`Prop` が Heyting 代数のインスタンスであることを示しましょう。 - -しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。 - -こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) の記事が参考になると思います。 - -### 問1.1 半順序集合であること --/ -section PropInstance --# - -/-- `P Q : Prop` に対して、順序関係 `P ≤ Q` を -`P → Q` が成り立つこととして定める -/ -instance : LE Prop where - le a b := a → b - -/-- `P < Q` の定義は `P → Q` かつ同値ではないこと -/ -instance : LT Prop where - lt a b := (a → b) ∧ ¬ (b → a) - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 --- 以下に示すのは一例です: -local add_aesop_rules unsafe 50% tactic [(by apply True.intro)] -local add_aesop_rules norm tactic [(by dsimp only [LE.le, LT.lt])] --## - -/-- 上記の定義のもとで `Prop` は半順序集合 -/ -instance : PartialOrder Prop where - le_refl := by aesop - le_trans := by aesop - lt_iff_le_not_le := by aesop - le_antisymm := by aesop - -/- ### 問1.2 束であること -/ - -/-- 論理和 `∨` を上限とする -/ -instance : Sup Prop where - sup a b := a ∨ b - -/-- 論理積 `∧` を下限とする -/ -instance : Inf Prop where - inf a b := a ∧ b - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 --- 以下に示すのは一例です: -local add_aesop_rules safe tactic [(by simp only [Nat.add_zero])] -local add_aesop_rules norm tactic [(by dsimp only [Sup.sup, Inf.inf] at *)] --## - -/-- 上記の定義のもとで `Prop` は束 -/ -instance : Lattice Prop where - le_sup_left := by aesop - le_sup_right := by aesop - sup_le := by aesop - inf_le_left := by aesop - inf_le_right := by aesop - le_inf := by aesop - -/- ### 問1.3 Heyting 代数であること -/ - -/-- `a ⇨ b` には `a → b` を対応させる -/ -instance : HImp Prop where - himp a b := a → b - -/-- `aᶜ` には `¬ a` を対応させる -/ -instance : HasCompl Prop where - compl a := ¬ a - -/-- True が最大元 -/ -instance : Top Prop where - top := True - -/-- False が最小元 -/ -instance : Bot Prop where - bot := False - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 --- 以下に示すのは一例です: -local add_aesop_rules norm simp [Nat.add_zero] -local add_aesop_rules norm tactic [(by dsimp only [HImp.himp, HasCompl.compl, Top.top, Bot.bot] at *)] --## - -instance : HeytingAlgebra Prop where - le_top := by aesop - bot_le := by aesop - le_himp_iff := by aesop - himp_bot := by aesop - -end PropInstance --# -/- ## 問2 Bool 代数でない Heyting 代数 -Bool 代数を定義し、Heyting 代数であって Bool 代数でない例を具体的に構成します。これにより、Heyting 代数の公理から Bool 代数の公理を証明することができないことが分かります。 - -反例の集合はシンプルで、３つの要素からなる集合として構成することができます。 --/ -section BooleanCounterExample --# - -/-- Bool 代数 -/ -class BooleanAlgebra (α : Type) extends HeytingAlgebra α where - /-- `x ⊓ xᶜ = ⊥` が成り立つ -/ - inf_compl_le_bot : ∀ x : α, x ⊓ xᶜ ≤ ⊥ - - /-- `⊤ = x ⊔ xᶜ` が成り立つ -/ - top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ - -/-- `{0, 1, 2}` という集合。これが反例になる。 -/ -abbrev Three := Fin 3 - -/- ### 問2.1 半順序集合であること -/ - --- 順序関係が既に定義されている -#synth LE Three - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 ---##-- -local add_aesop_rules safe cases [Fin] -local add_aesop_rules norm simp [Fin.le_def] -local add_aesop_rules safe tactic [(by omega)] ---##-- - -instance : PartialOrder Three where - le_refl := by aesop - le_trans := by aesop - le_antisymm := by aesop - lt_iff_le_not_le := by aesop - -/- ### 問2.2 束であること -/ - -/-- 上限の定義 -/ -instance : Sup Three where - sup a b := { - val := max a.val b.val - isLt := by omega - } - -/-- 下限の定義 -/ -instance : Inf Three where - inf a b := { - val := min a.val b.val - isLt := by omega - } - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 -local add_aesop_rules norm tactic [(by dsimp [Sup.sup, Inf.inf])] --## - -/-- 束になる -/ -instance : Lattice Three where - le_sup_left := by aesop - le_sup_right := by aesop - sup_le := by aesop - inf_le_left := by aesop - inf_le_right := by aesop - le_inf := by aesop - -/- ### 問2.3 Heyting 代数であるが Bool 代数ではないこと -/ - -/-- 最大元は2 -/ -instance : Top Three where - top := 2 - -/-- 最小元は0 -/ -instance : Bot Three where - bot := 0 - -/-- Heyting 含意の定義 -/ -instance : HImp Three where - himp a b := { - val := if a ≤ b then 2 else b.val - isLt := by aesop - } - -/-- 補元の定義 -/ -instance : HasCompl Three where - compl a := { - val := if a = 0 then 2 else 0 - isLt := by aesop - } - --- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 --- いくつルールを追加しても構いません。 -local add_aesop_rules norm tactic [(by dsimp [Bot.bot, Top.top, HImp.himp, HasCompl.compl])] --## - -/-- Heyting 代数になる -/ -instance : HeytingAlgebra Three where - le_top := by aesop - bot_le := by aesop - le_himp_iff := by aesop - himp_bot := by aesop - -/-- Three は上記の構成の下で Bool 代数ではない -/ -theorem three_not_boolean : (1 : Three) ⊔ 1ᶜ ≠ ⊤ := by aesop - -end BooleanCounterExample --# diff --git a/LeanByExample/Tutorial/Solution/InverseSurjInj.lean b/LeanByExample/Tutorial/Solution/InverseSurjInj.lean deleted file mode 100644 index 95d1b33f..00000000 --- a/LeanByExample/Tutorial/Solution/InverseSurjInj.lean +++ /dev/null @@ -1,119 +0,0 @@ -/- # 全射・単射と左逆・右逆写像 - -関数 `f : A → B` が**全射**であるとは、任意の `b : B` に対して `f a = b` となる `a : A` が存在することをいいます。また、`f` が**単射**であるとは、任意の `a₁, a₂ : A` に対して `f a₁ = f a₂` ならば `a₁ = a₂` となることをいいます。 - -これを Lean で表現すると次のようになります。 --/ -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -variable {A B : Type} - -/-- 関数の全射性 -/ -def Function.Surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b - -/-- 関数の単射性 -/ -def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a₂ → a₁ = a₂ - -/- 一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。 - -しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](#{root}/Reference/Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。 - -ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。 --/ - -/- ## 問1: 全射から逆方向の単射 -まずは、全射 `f : A → B` が存在すれば逆方向の単射 `g : B → A` も存在することを示しましょう。 - -実際にはより強く、`f ∘ g = id` を満たすような `g` が構成できます。一般に、`f ∘ g = id` が成り立つとき、`g` を `f` の右逆写像であるとか、切断(section)であるとかいいます。 --/ - --- 選択原理を使用する -open Function Classical - -/-- 全射 `f : A → B` があれば、選択原理を使用することにより -単射 `g : B → A` を作ることができる。-/ -theorem surj_to_inj (f : A → B) (hsurj : Surjective f) - : ∃ g : B → A, Injective g := by - -- まず `g` を構成する。 - -- 任意の `b : B` に対して `f` の全射性より - -- `f a = b` となる `a : A` が存在するのでそれを返す。 - --##-- - let g' : (b : B) → {a : A // f a = b} := fun b => - have h : ∃ a, f a = b := hsurj b - ⟨Classical.choose h, Classical.choose_spec h⟩ - --##-- - let g : B → A := fun b => /- sorry -/ (g' b).val - - -- `g` の定義と `f` の全射性から、`f (g b) = b` が成り立つ。 - have gdef : ∀ b, f (g b) = b := by - -- sorry - intro b - rw [show g b = (g' b).val from rfl] - simp_all [(g' b).property] - -- sorry - - -- `f ∘ g = id` を使って、 - -- `g` が単射であることを示す。 - -- sorry - exists g - intro b₁ b₂ h - replace h : b₁ = b₂ := calc - _ = f (g b₁) := by rw [gdef] - _ = f (g b₂) := by rw [h] - _ = _ := by rw [gdef] - exact h - -- sorry - -/- ## 問2: 単射から逆方向の全射 -次に `f : A → B` が単射であれば、逆方向の全射 `g : B → A` も存在することを示しましょう。 - -これも実際にはより強く、`g ∘ f = id` を満たすような `g` が構成できます。一般に、`g ∘ f = id` が成り立つとき、`g` を `f` の左逆写像であるとか、引き込み(retraction)であるとかいいます。 - -```admonish warning title="注意" -`A` が空の時には関数 `g : B → A` は構成することができないため、`A` が空でないという仮定が必要です。それは `Inhabited A` という引数により表現されています。 -``` --/ - -/-- 単射 `f : A → B` があれば、選択原理を使用することにより -全射 `g : B → A` を作ることができる。 -/ -theorem inj_to_surj [Inhabited A] (f : A → B) (hinj : Injective f) - : ∃ g : B → A, Surjective g := by - -- まず `g` を構成する。 - -- `g b` の値を構成するために、`b : B` が `f` の像に入っているかで場合分けをし、 - -- 入っていなければ適当な値、入っていれば `b = f a` となる `a` を返すようにする。 - let g : B → A := fun b => /- sorry -/ - if h : ∃ a, f a = b then Classical.choose h --## - else default --## - - -- `g` の定義と `f` の単射性から、`g (f a) = a` が成り立つ。 - have gdef : ∀ a, g (f a) = a := by - -- sorry - -- `a : A` が与えられたとする。 - intro a - - -- `g` の定義を展開する - dsimp only [g] - - -- `f a` は明らかに `f` の像に入っているということを利用して、 - -- `g` の定義の中の `if` 式を簡約する。 - split - case isFalse h => - have : ∃ a₁, f a₁ = f a := ⟨a, rfl⟩ - simp_all [this] - - -- 後は `f` の単射性から従う。 - case isTrue h => - have := Classical.choose_spec h - apply hinj - assumption - -- sorry - - -- `g ∘ f = id` を使って、 - -- `g` が全射であることを示す。 - -- sorry - exists g - intro a - exists f a - apply gdef - -- sorry diff --git a/LeanByExample/Tutorial/Solution/KnightAndKnave.lean b/LeanByExample/Tutorial/Solution/KnightAndKnave.lean deleted file mode 100644 index a4ec493c..00000000 --- a/LeanByExample/Tutorial/Solution/KnightAndKnave.lean +++ /dev/null @@ -1,210 +0,0 @@ -/- # 騎士と悪党のパズル - -騎士(Knight)と悪党(Knave)の論理パズルは、著名な論理学者 Raymond Smullyan によって考案されたとされています。それ以来様々な変種が考案され続けてきました。ここでは、その中でも基本的なものを Lean で形式化し、解いていきます。 - -## 概要 - -[Critical thinking web](https://philosophy.hku.hk/think/logic/knights.php) から問題を引用します。まずは自然言語で問題文を述べましょう。 - -```admonish info title="" -ある島には、騎士と悪党しか住んでいません。すべての島民は騎士であるか悪党であるかのいずれかです。騎士が話すことは常に真であり、悪党が話すことは常に偽です。 - -あなたはゾーイとメルという２人の島民に出会いました。 -ゾーイは「メルは悪党です」と言いました。 -メルは「ゾーイも私も悪党ではありません」と言いました。 -さて、ゾーイとメルはそれぞれ騎士か悪党のどちらでしょうか？ -``` - -## 形式化 - -さっそく形式化を行っていきます。まず、ある島があってそこには騎士と悪党しか住んでいないというところですが、これは `Islander` という型に `knight` と `knave` という部分集合が存在するというように形式化できます。そのうえで、島民が騎士か悪党のどちらかであることを `axiom` コマンドで仮定しましょう。 - -ここでは後で便利なように `simp` 補題も示しておくことにします。 --/ -import Lean --# -set_option autoImplicit false --# -set_option relaxedAutoImplicit false --# - -/-- その島の住民を表す型 -/ -opaque Islander : Type - -/-- Islander の部分集合として定義した騎士の全体 -/ -opaque knight : Islander → Prop - -/-- Islander の部分集合として定義した悪党の全体 -/ -opaque knave : Islander → Prop - -/-- 人は騎士か悪党のどちらか -/ -axiom knight_or_knave (p : Islander) : knight p ∨ knave p - -/-- 人が騎士かつ悪党であることはない -/ -axiom knight_ne_knave (p : Islander) : ¬(knight p ∧ knave p) - -/-- 騎士でないことと悪党であることは同値 -/ -@[simp] theorem of_not_knight {p : Islander} : ¬ knight p ↔ knave p := by - have or := knight_or_knave p - have ne := knight_ne_knave p - constructor - all_goals - intro h - simp_all - -/-- 悪党でないことと騎士であることは同値 -/ -@[simp] theorem of_not_knave {p : Islander} : ¬ knave p ↔ knight p := by - have or := knight_or_knave p - have ne := knight_ne_knave p - constructor - all_goals - intro h - simp_all - -/- これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。-/ - -/-- ゾーイ -/ -axiom zoey : Islander - -/-- メル -/ -axiom mel : Islander - -/- 正直者であるとか嘘つきであるということを表現するために、誰がなんと発言したかを表現するための関数を用意します。その上で、それぞれの発言を愚直に形式化していきます。 -/ - -/-- p さんが body という命題を話したという事実を表す命題 -/ -opaque Islander.say (p : Islander) (body : Prop) : Prop - -variable {p : Islander} {body : Prop} - -/-- 騎士の発言内容はすべて真実 -/ -axiom statement_of_knight (h : knight p) (say : p.say body) : body - -/-- 悪党の発言内容はすべて偽 -/ -axiom statement_of_knave (h : knave p) (say : p.say body) : ¬body - -/-- ゾーイは「メルは悪党だ」と言った -/ -axiom zoey_says : zoey.say (knave mel) - -/-- メルは「ゾーイもメルも悪党ではない」と言った -/ -axiom mel_says : mel.say (¬ knave zoey ∧ ¬ knave mel) - -/- ここまでで問題文の前提部分の形式化は完了です。 - -残っているのは、「ゾーイとメルはそれぞれ騎士か悪党のどちらですか」と問う部分です。これは少し難しいです。 - -考えてみると、Lean で（証明すべき命題がわかっているときに）何かを証明するのはよくありますが、与えられた前提から何が言えるのかを明確なゴールなしに組み立てていくのはあまり見ないということにお気づきになるでしょう。この問題も、もし問いの内容が「ゾーイが騎士であることを示せ」とか「ゾーイが悪党であることを示せ」だったならば、今までの準備の下で簡単に形式化ができますが、「騎士なのか悪党なのか決定せよ」なので少し複雑になります。 - -ここでの解決方法は、`Solution` という帰納型を `inductive` コマンドで作成し、その項を作ってくださいという形式にすることです。 --/ - -/-- `p` が騎士か悪党のどちらなのか知っていることを表す型 -/ -inductive Solution (p : Islander) : Type where - | isKnight : knight p → Solution p - | isKnave : knave p → Solution p - -/- この `Solution` の項を、`p : Islander` に対して作成するときに、項が `isKnight` から来るのか `isKnave` から来るのか明示しなければなりません。そしてそのために、それぞれ `p` が騎士であるか悪党であるかのどちらかの証明が引数に要求されることになるので、問題文を表現しているといえます。 - -## 問題 - -以上の準備の下で、問題は次のように表現できます。以下の `sorry` の部分を埋めてください。 - -```admonish error title="禁止事項" -この問題では選択原理 `Classical.choice` の使用は禁止です。 -解答を書いた後で、`zoey_which` と `mel_which` に対して `#print axioms` コマンドを使用し、選択原理を使用していないことを確認してください。 - -余裕があればなぜ禁止なのか考えてみましょう。 -``` --/ ---##-- -/- ## なぜ選択原理の使用を禁止したかについて -/ - --- 以下のように、選択原理を使用するとどちらが騎士なのかを知らなくても --- Solution の項が得られるため -noncomputable def foo : Solution zoey := by - have : Nonempty (Solution zoey) := by - cases knight_or_knave zoey - case inl h => - exact ⟨Solution.isKnight h⟩ - case inr h => - exact ⟨Solution.isKnave h⟩ - exact Classical.choice this - -/- ## 問題の解答部分 -/ - -theorem zoey_is_not_knave : ¬ knave zoey := by - -- ゾーイが悪党だと仮定する - intro h - - have mel_is_knight : knight mel := by - -- ゾーイの発言は偽なので、メルは悪党ではない - have := statement_of_knave h zoey_says - - -- よってメルは騎士 - simpa [of_not_knave] using this - - -- メルが騎士なので、メルの発言は真 - have mel_says_truth := statement_of_knight mel_is_knight mel_says - - -- したがってゾーイは騎士 - have : knight zoey := by - simp only [of_not_knave] at mel_says_truth - simp_all - - -- これは仮定に矛盾 - simp_all [knight_ne_knave] - -/-- ゾーイは騎士である -/ -theorem zoey_is_knight : knight zoey := by - have := zoey_is_not_knave - simpa using this - -/-- メルは悪党 -/ -theorem mel_is_knave : knave mel := by - -- ゾーイは騎士なのでゾーイの発言は真であり、 - -- よってメルは悪党 - exact statement_of_knight zoey_is_knight zoey_says ---##-- - -/-- ゾーイは騎士か悪党か？-/ -noncomputable def zoey_which : Solution zoey := by - -- sorry - apply Solution.isKnight - exact zoey_is_knight - -- sorry - -/-- メルは騎士か悪党か？-/ -noncomputable def mel_which : Solution mel := by - -- sorry - apply Solution.isKnave - exact mel_is_knave - -- sorry - ---#-- -section -/- ## 選択原理を使用していないことを確認するコマンド -/ - -open Lean Elab Command - -elab "#detect_classical " id:ident : command => do - -- 識別子(ident)を Name に変換 - let constName ← liftCoreM <| realizeGlobalConstNoOverload id - - -- 依存する公理を取得 - let axioms ← collectAxioms constName - - -- 依存公理がなかったときの処理 - if axioms.isEmpty then - logInfo m!"'{constName}' does not depend on any axioms" - return () - - -- Classical で始まる公理があるかどうかチェック - -- もしあればエラーにする - let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm - if caxes.isEmpty then - logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}" - else - throwError m!"'{constName}' depends on classical axioms: {caxes.toList}" - -end - --- 選択原理を使用していないことを確認 -#detect_classical zoey_which -#detect_classical mel_which ---#-- diff --git a/LeanByExample/Tutorial/Solution/README.lean b/LeanByExample/Tutorial/Solution/README.lean deleted file mode 100644 index 08da3333..00000000 --- a/LeanByExample/Tutorial/Solution/README.lean +++ /dev/null @@ -1,21 +0,0 @@ -/- # 演習問題 -このセクションでは、演習問題を扱います。ぜひ新しいパズルゲームだと思って挑戦してみてください。 - -## 🎮 遊び方 - -問題は、前提となるライブラリや知識が少なく、難易度が低いと思われる順に並べてあります。興味があるものから挑戦してみましょう。 - -解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。 - -あるいは、Codespace を開き、`LeanByExample/Tutorial/Exercise` ディレクトリの中にある該当ファイルを開いてもよいです。 - -[![codespace badge](https://github.com/codespaces/badge.svg)](https://codespaces.new/lean-ja/lean-by-example) - -お使いの PC に Lean をインストール済みであれば、このリポジトリをクローンして VSCode で開いてください。 - -## ❓ どうしてもわからないとき - -時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 - -しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。 --/ diff --git a/LeanByExample/Reference/Type/Array.lean b/LeanByExample/Type/Array.lean similarity index 92% rename from LeanByExample/Reference/Type/Array.lean rename to LeanByExample/Type/Array.lean index cdd851b6..019bb801 100644 --- a/LeanByExample/Reference/Type/Array.lean +++ b/LeanByExample/Type/Array.lean @@ -58,7 +58,7 @@ From the point of view of proofs `Array α` is just a wrapper around `List α`. /- ## インデックスアクセス -配列は [`GetElem`](#{root}/Reference/TypeClass/GetElem.md) のインスタンスであり、`i` 番目の要素を取得するために `a[i]` という記法が使用できます。 +配列は [`GetElem`](#{root}/TypeClass/GetElem.md) のインスタンスであり、`i` 番目の要素を取得するために `a[i]` という記法が使用できます。 -/ #guard #[1, 2, 3][0] = 1 diff --git a/LeanByExample/Reference/Type/Bool.lean b/LeanByExample/Type/Bool.lean similarity index 100% rename from LeanByExample/Reference/Type/Bool.lean rename to LeanByExample/Type/Bool.lean diff --git a/LeanByExample/Reference/Type/Char.lean b/LeanByExample/Type/Char.lean similarity index 100% rename from LeanByExample/Reference/Type/Char.lean rename to LeanByExample/Type/Char.lean diff --git a/LeanByExample/Reference/Type/Float.lean b/LeanByExample/Type/Float.lean similarity index 100% rename from LeanByExample/Reference/Type/Float.lean rename to LeanByExample/Type/Float.lean diff --git a/LeanByExample/Reference/Type/List.lean b/LeanByExample/Type/List.lean similarity index 97% rename from LeanByExample/Reference/Type/List.lean rename to LeanByExample/Type/List.lean index 999ceabd..23ac6745 100644 --- a/LeanByExample/Reference/Type/List.lean +++ b/LeanByExample/Type/List.lean @@ -63,7 +63,7 @@ end Hidden --# ### map -`List` は [`Functor`](#{root}/Reference/TypeClass/Functor.md) 型クラスのインスタンスになっているため `<$>` 演算子が利用できます。 +`List` は [`Functor`](#{root}/TypeClass/Functor.md) 型クラスのインスタンスになっているため `<$>` 演算子が利用できます。 -/ -- `<$>` 演算子が利用できる diff --git a/LeanByExample/Reference/Type/Macro.lean b/LeanByExample/Type/Macro.lean similarity index 72% rename from LeanByExample/Reference/Type/Macro.lean rename to LeanByExample/Type/Macro.lean index d0749f4b..a1d60ecb 100644 --- a/LeanByExample/Reference/Type/Macro.lean +++ b/LeanByExample/Type/Macro.lean @@ -44,6 +44,6 @@ attribute [macro zeroLitPar] zeroLitExpand /- ### マクロから Macro 型 -実際にマクロを定義する際は、[`notation`](#{root}/Reference/Declarative/Notation.md) コマンドや [`macro`](#{root}/Reference/Declarative/Macro.md) コマンドなどを使用するでしょう。こういったコマンドでマクロを定義したとき、それが裏で `Macro` 型の項を生成していることを確かめることができます。特定のコマンドの実行後に新たに生成された識別子の名前をリストアップすることができる、`whatsnew` コマンドを使えば可能です。以下の出力の中に `Lean.Macro` 型の項があるはずです。-/ +実際にマクロを定義する際は、[`notation`](#{root}/Declarative/Notation.md) コマンドや [`macro`](#{root}/Declarative/Macro.md) コマンドなどを使用するでしょう。こういったコマンドでマクロを定義したとき、それが裏で `Macro` 型の項を生成していることを確かめることができます。特定のコマンドの実行後に新たに生成された識別子の名前をリストアップすることができる、`whatsnew` コマンドを使えば可能です。以下の出力の中に `Lean.Macro` 型の項があるはずです。-/ whatsnew in macro "oneLit" : term => `(1) diff --git a/LeanByExample/Reference/Type/Prop.lean b/LeanByExample/Type/Prop.lean similarity index 100% rename from LeanByExample/Reference/Type/Prop.lean rename to LeanByExample/Type/Prop.lean diff --git a/LeanByExample/Reference/Type/README.lean b/LeanByExample/Type/README.lean similarity index 100% rename from LeanByExample/Reference/Type/README.lean rename to LeanByExample/Type/README.lean diff --git a/LeanByExample/Reference/Type/String.lean b/LeanByExample/Type/String.lean similarity index 100% rename from LeanByExample/Reference/Type/String.lean rename to LeanByExample/Type/String.lean diff --git a/LeanByExample/Reference/Type/Syntax.lean b/LeanByExample/Type/Syntax.lean similarity index 92% rename from LeanByExample/Reference/Type/Syntax.lean rename to LeanByExample/Type/Syntax.lean index d0f491bd..7f820d96 100644 --- a/LeanByExample/Reference/Type/Syntax.lean +++ b/LeanByExample/Type/Syntax.lean @@ -8,7 +8,7 @@ ## 定義 -`Syntax` 型は以下のように[帰納型](#{root}/Reference/Declarative/Inductive.md)として定義されています。 +`Syntax` 型は以下のように[帰納型](#{root}/Declarative/Inductive.md)として定義されています。 -/ import Lean --# namespace Hidden --# @@ -81,7 +81,7 @@ info: Lean.Syntax.node #guard_msgs in #eval parse `term "0" -/- 見ての通りすぐに複雑怪奇になってしまうので、以降は表示を簡略化しましょう。`Syntax` は [`ToString`](#{root}/Reference/TypeClass/ToString.md) のインスタンスを実装しており、これは `SourceInfo` などを含まないシンプルな表現をしてくれるので、それを利用します。-/ +/- 見ての通りすぐに複雑怪奇になってしまうので、以降は表示を簡略化しましょう。`Syntax` は [`ToString`](#{root}/TypeClass/ToString.md) のインスタンスを実装しており、これは `SourceInfo` などを含まないシンプルな表現をしてくれるので、それを利用します。-/ -- 文字列として表示するとかなり簡略化される /-- info: `true -/ diff --git a/LeanByExample/Reference/Type/Type.lean b/LeanByExample/Type/Type.lean similarity index 100% rename from LeanByExample/Reference/Type/Type.lean rename to LeanByExample/Type/Type.lean diff --git a/LeanByExample/Reference/TypeClass/Coe.lean b/LeanByExample/TypeClass/Coe.lean similarity index 95% rename from LeanByExample/Reference/TypeClass/Coe.lean rename to LeanByExample/TypeClass/Coe.lean index d48dfcc2..3f60ee6e 100644 --- a/LeanByExample/Reference/TypeClass/Coe.lean +++ b/LeanByExample/TypeClass/Coe.lean @@ -2,7 +2,7 @@ # Coe `Coe` は、型強制(coercion)と呼ばれる仕組みをユーザが定義するための型クラスです。 -ある型 `T` が期待される場所に別の型の項 `s : S` を見つけると、Lean は型エラーにする前に自動的に型変換を行うことができないか試します。ここで行われる「自動的な型変換」が型強制です。型強制を明示的に指定するには、`↑` 記号をつけて `↑x` などのようにします。なお `↑` 記号については [`[coe]`](#{root}/Reference/Attribute/Coe.md) 属性も深い関係があります。 +ある型 `T` が期待される場所に別の型の項 `s : S` を見つけると、Lean は型エラーにする前に自動的に型変換を行うことができないか試します。ここで行われる「自動的な型変換」が型強制です。型強制を明示的に指定するには、`↑` 記号をつけて `↑x` などのようにします。なお `↑` 記号については [`[coe]`](#{root}/Attribute/Coe.md) 属性も深い関係があります。 具体的には `Coe S T` という型クラスのインスタンスが定義されているとき、型 `S` の項が型 `T` に変換されます。 diff --git a/LeanByExample/Reference/TypeClass/CoeDep.lean b/LeanByExample/TypeClass/CoeDep.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/CoeDep.lean rename to LeanByExample/TypeClass/CoeDep.lean diff --git a/LeanByExample/Reference/TypeClass/CoeFun.lean b/LeanByExample/TypeClass/CoeFun.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/CoeFun.lean rename to LeanByExample/TypeClass/CoeFun.lean diff --git a/LeanByExample/Reference/TypeClass/CoeSort.lean b/LeanByExample/TypeClass/CoeSort.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/CoeSort.lean rename to LeanByExample/TypeClass/CoeSort.lean diff --git a/LeanByExample/Reference/TypeClass/Decidable.lean b/LeanByExample/TypeClass/Decidable.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/Decidable.lean rename to LeanByExample/TypeClass/Decidable.lean diff --git a/LeanByExample/Reference/TypeClass/Functor.lean b/LeanByExample/TypeClass/Functor.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/Functor.lean rename to LeanByExample/TypeClass/Functor.lean diff --git a/LeanByExample/Reference/TypeClass/GetElem.lean b/LeanByExample/TypeClass/GetElem.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/GetElem.lean rename to LeanByExample/TypeClass/GetElem.lean diff --git a/LeanByExample/Reference/TypeClass/HAdd.lean b/LeanByExample/TypeClass/HAdd.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/HAdd.lean rename to LeanByExample/TypeClass/HAdd.lean diff --git a/LeanByExample/Reference/TypeClass/HMul.lean b/LeanByExample/TypeClass/HMul.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/HMul.lean rename to LeanByExample/TypeClass/HMul.lean diff --git a/LeanByExample/Reference/TypeClass/Inhabited.lean b/LeanByExample/TypeClass/Inhabited.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/Inhabited.lean rename to LeanByExample/TypeClass/Inhabited.lean diff --git a/LeanByExample/Reference/TypeClass/LawfulFunctor.lean b/LeanByExample/TypeClass/LawfulFunctor.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/LawfulFunctor.lean rename to LeanByExample/TypeClass/LawfulFunctor.lean diff --git a/LeanByExample/Reference/TypeClass/OfNat.lean b/LeanByExample/TypeClass/OfNat.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/OfNat.lean rename to LeanByExample/TypeClass/OfNat.lean diff --git a/LeanByExample/TypeClass/README.lean b/LeanByExample/TypeClass/README.lean new file mode 100644 index 00000000..aa4b793b --- /dev/null +++ b/LeanByExample/TypeClass/README.lean @@ -0,0 +1,6 @@ +/- # 型クラス + +型クラスとは、和や積、逆数を取る演算など、複数の型に対してそれぞれのやり方で実装されるような演算を定義するものです。 + +型クラスは主に [`class`](#{root}/Declarative/Class.md) コマンドで定義され、インスタンスを宣言するには [`instance`](#{root}/Declarative/Instance.md) コマンドを使用します。 +-/ diff --git a/LeanByExample/Reference/TypeClass/Repr.lean b/LeanByExample/TypeClass/Repr.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/Repr.lean rename to LeanByExample/TypeClass/Repr.lean diff --git a/LeanByExample/Reference/TypeClass/ToString.lean b/LeanByExample/TypeClass/ToString.lean similarity index 100% rename from LeanByExample/Reference/TypeClass/ToString.lean rename to LeanByExample/TypeClass/ToString.lean diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index b1b7ae05..a87f79dd 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -6,204 +6,191 @@ --- -# 第1部: リファレンス +- [対話的コマンド](./Diagnostic/README.md) + - [#check_failure: 意図的なエラー](./Diagnostic/CheckFailure.md) + - [#check: 型を調べる](./Diagnostic/Check.md) + - [#eval: 式を評価する](./Diagnostic/Eval.md) + - [#find: ライブラリ検索](./Diagnostic/Find.md) + - [#guard_msgs: メッセージのテスト](./Diagnostic/GuardMsgs.md) + - [#guard: Bool 値のテスト](./Diagnostic/Guard.md) + - [#help: ドキュメントを見る](./Diagnostic/Help.md) + - [#html: HTMLをインフォビューに表示](./Diagnostic/Html.md) + - [#instances: インスタンスを列挙](./Diagnostic/Instances.md) + - [#lint: リンタ実行](./Diagnostic/Lint.md) + - [#print: 中身を見る](./Diagnostic/Print.md) + - [#reduce: 式を簡約する](./Diagnostic/Reduce.md) + - [#synth: 型クラスの検査](./Diagnostic/Synth.md) + - [#time: 実行時間計測](./Diagnostic/Time.md) + - [#version: バージョン表示](./Diagnostic/Version.md) + - [#whnf: 式を弱頭正規形に](./Diagnostic/Whnf.md) -- [対話的コマンド](./Reference/Diagnostic/README.md) - - [#check_failure: 意図的なエラー](./Reference/Diagnostic/CheckFailure.md) - - [#check: 型を調べる](./Reference/Diagnostic/Check.md) - - [#eval: 式を評価する](./Reference/Diagnostic/Eval.md) - - [#find: ライブラリ検索](./Reference/Diagnostic/Find.md) - - [#guard_msgs: メッセージのテスト](./Reference/Diagnostic/GuardMsgs.md) - - [#guard: Bool 値のテスト](./Reference/Diagnostic/Guard.md) - - [#help: ドキュメントを見る](./Reference/Diagnostic/Help.md) - - [#html: HTMLをインフォビューに表示](./Reference/Diagnostic/Html.md) - - [#instances: インスタンスを列挙](./Reference/Diagnostic/Instances.md) - - [#lint: リンタ実行](./Reference/Diagnostic/Lint.md) - - [#print: 中身を見る](./Reference/Diagnostic/Print.md) - - [#reduce: 式を簡約する](./Reference/Diagnostic/Reduce.md) - - [#synth: 型クラスの検査](./Reference/Diagnostic/Synth.md) - - [#time: 実行時間計測](./Reference/Diagnostic/Time.md) - - [#version: バージョン表示](./Reference/Diagnostic/Version.md) - - [#whnf: 式を弱頭正規形に](./Reference/Diagnostic/Whnf.md) +- [宣言的コマンド](./Declarative/README.md) + - [abbrev: 略称を定義する](./Declarative/Abbrev.md) + - [add_aesop_rules: aesop 改造](./Declarative/AddAesopRules.md) + - [attribute: 属性を付与する](./Declarative/Attribute.md) + - [axiom: 公理を宣言する](./Declarative/Axiom.md) + - [class: 型クラスを定義する](./Declarative/Class.md) + - [declare_aesop_rule_sets: Aesopでタクティク自作](./Declarative/DeclareAesopRuleSets.md) + - [declare_syntax_cat: 構文カテゴリ](./Declarative/DeclareSyntaxCat.md) + - [def: 関数などを定義する](./Declarative/Def.md) + - [deriving: インスタンス自動生成](./Declarative/Deriving.md) + - [elab: 構文に意味を与える](./Declarative/Elab.md) + - [example: 名前をつけずに証明](./Declarative/Example.md) + - [export: 現在の名前空間に追加](./Declarative/Export.md) + - [inductive: 帰納型を定義する](./Declarative/Inductive.md) + - [infix: 中置記法](./Declarative/Infix.md) + - [instance: インスタンスを定義する](./Declarative/Instance.md) + - [local: 有効範囲をセクションで限定](./Declarative/Local.md) + - [macro_rules: 構文展開の追加](./Declarative/MacroRules.md) + - [macro: 簡便なマクロ定義](./Declarative/Macro.md) + - [namespace: 名前空間を宣言する](./Declarative/Namespace.md) + - [noncomputable: 計算不能にする](./Declarative/Noncomputable.md) + - [notation: 記法を導入する](./Declarative/Notation.md) + - [opaque: 簡約できない名前を宣言](./Declarative/Opaque.md) + - [open: 名前空間を開く](./Declarative/Open.md) + - [partial: 再帰の停止証明をしない](./Declarative/Partial.md) + - [postfix: 後置記法](./Declarative/Postfix.md) + - [prefix: 前置記法](./Declarative/Prefix.md) + - [private: 定義を不可視にする](./Declarative/Private.md) + - [proof_wanted: 証明を公募する](./Declarative/ProofWanted.md) + - [protected: フルネームを強制する](./Declarative/Protected.md) + - [scoped: 有効範囲を名前空間で限定](./Declarative/Scoped.md) + - [section: スコープを区切る](./Declarative/Section.md) + - [set_option: オプション設定](./Declarative/SetOption.md) + - [structure: 構造体を定義する](./Declarative/Structure.md) + - [syntax: 構文を定義](./Declarative/Syntax.md) + - [termination_by: 整礎再帰を使う](./Declarative/TerminationBy.md) + - [theorem: 命題を証明する](./Declarative/Theorem.md) + - [variable: 引数を共通化する](./Declarative/Variable.md) -- [宣言的コマンド](./Reference/Declarative/README.md) - - [abbrev: 略称を定義する](./Reference/Declarative/Abbrev.md) - - [add_aesop_rules: aesop 改造](./Reference/Declarative/AddAesopRules.md) - - [attribute: 属性を付与する](./Reference/Declarative/Attribute.md) - - [axiom: 公理を宣言する](./Reference/Declarative/Axiom.md) - - [class: 型クラスを定義する](./Reference/Declarative/Class.md) - - [declare_aesop_rule_sets: Aesopでタクティク自作](./Reference/Declarative/DeclareAesopRuleSets.md) - - [declare_syntax_cat: 構文カテゴリ](./Reference/Declarative/DeclareSyntaxCat.md) - - [def: 関数などを定義する](./Reference/Declarative/Def.md) - - [deriving: インスタンス自動生成](./Reference/Declarative/Deriving.md) - - [elab: 構文に意味を与える](./Reference/Declarative/Elab.md) - - [example: 名前をつけずに証明](./Reference/Declarative/Example.md) - - [export: 現在の名前空間に追加](./Reference/Declarative/Export.md) - - [inductive: 帰納型を定義する](./Reference/Declarative/Inductive.md) - - [infix: 中置記法](./Reference/Declarative/Infix.md) - - [instance: インスタンスを定義する](./Reference/Declarative/Instance.md) - - [local: 有効範囲をセクションで限定](./Reference/Declarative/Local.md) - - [macro_rules: 構文展開の追加](./Reference/Declarative/MacroRules.md) - - [macro: 簡便なマクロ定義](./Reference/Declarative/Macro.md) - - [namespace: 名前空間を宣言する](./Reference/Declarative/Namespace.md) - - [noncomputable: 計算不能にする](./Reference/Declarative/Noncomputable.md) - - [notation: 記法を導入する](./Reference/Declarative/Notation.md) - - [opaque: 簡約できない名前を宣言](./Reference/Declarative/Opaque.md) - - [open: 名前空間を開く](./Reference/Declarative/Open.md) - - [partial: 再帰の停止証明をしない](./Reference/Declarative/Partial.md) - - [postfix: 後置記法](./Reference/Declarative/Postfix.md) - - [prefix: 前置記法](./Reference/Declarative/Prefix.md) - - [private: 定義を不可視にする](./Reference/Declarative/Private.md) - - [proof_wanted: 証明を公募する](./Reference/Declarative/ProofWanted.md) - - [protected: フルネームを強制する](./Reference/Declarative/Protected.md) - - [scoped: 有効範囲を名前空間で限定](./Reference/Declarative/Scoped.md) - - [section: スコープを区切る](./Reference/Declarative/Section.md) - - [set_option: オプション設定](./Reference/Declarative/SetOption.md) - - [structure: 構造体を定義する](./Reference/Declarative/Structure.md) - - [syntax: 構文を定義](./Reference/Declarative/Syntax.md) - - [termination_by: 整礎再帰を使う](./Reference/Declarative/TerminationBy.md) - - [theorem: 命題を証明する](./Reference/Declarative/Theorem.md) - - [variable: 引数を共通化する](./Reference/Declarative/Variable.md) +- [属性](./Attribute/README.md) + - [app_unexpander: 関数適用の表示](./Attribute/AppUnexpander.md) + - [cases_eliminator: 独自場合分け](./Attribute/CasesEliminator.md) + - [coe: 型強制 ↑ として表示させる](./Attribute/Coe.md) + - [csimp: 効率的な実装に置換](./Attribute/Csimp.md) + - [default_instance: デフォルトの解決法](./Attribute/DefaultInstance.md) + - [induction_eliminator: 独自帰納法](./Attribute/InductionEliminator.md) + - [inherit_doc: ドキュメントの継承](./Attribute/InheritDoc.md) + - [macro_inline: 短絡評価など](./Attribute/MacroInline.md) + - [match_pattern: 独自パタンマッチ](./Attribute/MatchPattern.md) + - [simps: simp 補題の自動生成](./Attribute/Simps.md) -- [属性](./Reference/Attribute/README.md) - - [app_unexpander: 関数適用の表示](./Reference/Attribute/AppUnexpander.md) - - [cases_eliminator: 独自場合分け](./Reference/Attribute/CasesEliminator.md) - - [coe: 型強制 ↑ として表示させる](./Reference/Attribute/Coe.md) - - [csimp: 効率的な実装に置換](./Reference/Attribute/Csimp.md) - - [default_instance: デフォルトの解決法](./Reference/Attribute/DefaultInstance.md) - - [induction_eliminator: 独自帰納法](./Reference/Attribute/InductionEliminator.md) - - [inherit_doc: ドキュメントの継承](./Reference/Attribute/InheritDoc.md) - - [macro_inline: 短絡評価など](./Reference/Attribute/MacroInline.md) - - [match_pattern: 独自パタンマッチ](./Reference/Attribute/MatchPattern.md) - - [simps: simp 補題の自動生成](./Reference/Attribute/Simps.md) +- [オプション](./Option/README.md) + - [autoImplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) + - [hygiene: マクロ衛生](./Option/Hygiene.md) + - [linter.flexible: 脆弱な証明を指摘する](./Option/Flexible.md) + - [linter.style.multiGoal: フォーカス強制](./Option/MultiGoal.md) + - [relaxedAutoImplicit: 更にautoImplicit](./Option/RelaxedAutoImplicit.md) -- [オプション](./Reference/Option/README.md) - - [autoImplicit: 自動束縛暗黙引数](./Reference/Option/AutoImplicit.md) - - [hygiene: マクロ衛生](./Reference/Option/Hygiene.md) - - [linter.flexible: 脆弱な証明を指摘する](./Reference/Option/Flexible.md) - - [linter.style.multiGoal: フォーカス強制](./Reference/Option/MultiGoal.md) - - [relaxedAutoImplicit: 更にautoImplicit](./Reference/Option/RelaxedAutoImplicit.md) +- [型クラス](./TypeClass/README.md) + - [Coe: 型強制](./TypeClass/Coe.md) + - [CoeDep: 依存型強制](./TypeClass/CoeDep.md) + - [CoeFun: 関数型への強制](./TypeClass/CoeFun.md) + - [CoeSort: 型宇宙への強制](./TypeClass/CoeSort.md) + - [Decidable: 決定可能](./TypeClass/Decidable.md) + - [Functor: ファンクタ](./TypeClass/Functor.md) + - [GetElem: n番目の要素を取得](./TypeClass/GetElem.md) + - [HAdd: + のための記法クラス](./TypeClass/HAdd.md) + - [HMul: * のための記法クラス](./TypeClass/HMul.md) + - [Inhabited: 有項にする](./TypeClass/Inhabited.md) + - [LawfulFunctor: ルール付きファンクタ](./TypeClass/LawfulFunctor.md) + - [OfNat: 数値リテラルを使用](./TypeClass/OfNat.md) + - [Repr: 表示方法を指定](./TypeClass/Repr.md) + - [ToString: 文字列に変換](./TypeClass/ToString.md) -- [型クラス](./Reference/TypeClass/README.md) - - [Coe: 型強制](./Reference/TypeClass/Coe.md) - - [CoeDep: 依存型強制](./Reference/TypeClass/CoeDep.md) - - [CoeFun: 関数型への強制](./Reference/TypeClass/CoeFun.md) - - [CoeSort: 型宇宙への強制](./Reference/TypeClass/CoeSort.md) - - [Decidable: 決定可能](./Reference/TypeClass/Decidable.md) - - [Functor: ファンクタ](./Reference/TypeClass/Functor.md) - - [GetElem: n番目の要素を取得](./Reference/TypeClass/GetElem.md) - - [HAdd: + のための記法クラス](./Reference/TypeClass/HAdd.md) - - [HMul: * のための記法クラス](./Reference/TypeClass/HMul.md) - - [Inhabited: 有項にする](./Reference/TypeClass/Inhabited.md) - - [LawfulFunctor: ルール付きファンクタ](./Reference/TypeClass/LawfulFunctor.md) - - [OfNat: 数値リテラルを使用](./Reference/TypeClass/OfNat.md) - - [Repr: 表示方法を指定](./Reference/TypeClass/Repr.md) - - [ToString: 文字列に変換](./Reference/TypeClass/ToString.md) +- [データ型](./Type/README.md) + - [Array: 配列](./Type/Array.md) + - [Bool: 真偽値](./Type/Bool.md) + - [Char: Unicode 文字](./Type/Char.md) + - [Float: 浮動小数点数](./Type/Float.md) + - [List: 連結リスト](./Type/List.md) + - [Macro: マクロ](./Type/Macro.md) + - [Prop: 命題全体](./Type/Prop.md) + - [String: 文字列](./Type/String.md) + - [Syntax: 具象構文木](./Type/Syntax.md) + - [Type: 型の型](./Type/Type.md) -- [データ型](./Reference/Type/README.md) - - [Array: 配列](./Reference/Type/Array.md) - - [Bool: 真偽値](./Reference/Type/Bool.md) - - [Char: Unicode 文字](./Reference/Type/Char.md) - - [Float: 浮動小数点数](./Reference/Type/Float.md) - - [List: 連結リスト](./Reference/Type/List.md) - - [Macro: マクロ](./Reference/Type/Macro.md) - - [Prop: 命題全体](./Reference/Type/Prop.md) - - [String: 文字列](./Reference/Type/String.md) - - [Syntax: 具象構文木](./Reference/Type/Syntax.md) - - [Type: 型の型](./Reference/Type/Type.md) - -- [タクティク](./Reference/Tactic/README.md) - - [<;> 生成された全ゴールに適用](./Reference/Tactic/SeqFocus.md) - - [ac_rfl: 可換性と結合性を使う](./Reference/Tactic/AcRfl.md) - - [aesop: 自明な証明の自動探索](./Reference/Tactic/Aesop.md) - - [all_goals: 全ゴールに対して適用](./Reference/Tactic/AllGoals.md) - - [apply at: apply を仮定に適用する](./Reference/Tactic/ApplyAt.md) - - [apply_assumption: 自動 apply](./Reference/Tactic/ApplyAssumption.md) - - [apply: 含意→を使う](./Reference/Tactic/Apply.md) - - [apply?: apply できるか検索](./Reference/Tactic/ApplyQuestion.md) - - [assumption: 仮定を自動で exact](./Reference/Tactic/Assumption.md) - - [by_cases: 排中律](./Reference/Tactic/ByCases.md) - - [by_contra: 背理法](./Reference/Tactic/ByContra.md) - - [by: タクティクモードに入る](./Reference/Tactic/By.md) - - [calc: 計算モードに入る](./Reference/Tactic/Calc.md) - - [cases: 場合分けをする](./Reference/Tactic/Cases.md) - - [cases': Lean3版のcases](./Reference/Tactic/CasesAp.md) - - [choose: 選択関数を得る](./Reference/Tactic/Choose.md) - - [clear: 命題や定義を削除する](./Reference/Tactic/Clear.md) - - [congr: ゴールの関数適用を外す](./Reference/Tactic/Congr.md) - - [constructor: 論理積や同値性を示す](./Reference/Tactic/Constructor.md) - - [contradiction: 矛盾を指摘](./Reference/Tactic/Contradiction.md) - - [contrapose: 対偶をとる](./Reference/Tactic/Contrapose.md) - - [conv: 変換モードに入る](./Reference/Tactic/Conv.md) - - [convert: 惜しい補題を使う](./Reference/Tactic/Convert.md) - - [decide: 決定可能な命題を示す](./Reference/Tactic/Decide.md) - - [done: 証明終了を宣言](./Reference/Tactic/Done.md) - - [dsimp: 定義に展開](./Reference/Tactic/Dsimp.md) - - [exact: 証明を直接構成](./Reference/Tactic/Exact.md) - - [exact?: exact できるか検索](./Reference/Tactic/ExactQuestion.md) - - [exfalso: 矛盾を示すことに帰着](./Reference/Tactic/Exfalso.md) - - [exists: 存在∃を示す](./Reference/Tactic/Exists.md) - - [ext: 外延性を使う](./Reference/Tactic/Ext.md) - - [field_simp: 分母を払う](./Reference/Tactic/FieldSimp.md) - - [fin_cases: 場合分けを簡潔に行う](./Reference/Tactic/FinCases.md) - - [fun_prop: 関数の諸性質を示す](./Reference/Tactic/FunProp.md) - - [funext: 関数等式を示す](./Reference/Tactic/Funext.md) - - [gcongr: 合同性を用いる](./Reference/Tactic/Gcongr.md) - - [generalize: 一般化する](./Reference/Tactic/Generalize.md) - - [guard_hyp: 仮定や補題を確認](./Reference/Tactic/GuardHyp.md) - - [have: 補題を用意する](./Reference/Tactic/Have.md) - - [hint: 複数のタクティクを同時に試す](./Reference/Tactic/Hint.md) - - [induction: 帰納法](./Reference/Tactic/Induction.md) - - [induction': inductionの構文違い](./Reference/Tactic/InductionAp.md) - - [intro: 含意→や全称∀を示す](./Reference/Tactic/Intro.md) - - [itauto: 直観主義論理の枠内で示す](./Reference/Tactic/Itauto.md) - - [left: 論理和∨を示す](./Reference/Tactic/Left.md) - - [linarith: 線形(不)等式を示す](./Reference/Tactic/Linarith.md) - - [native_decide: 実行による証明](./Reference/Tactic/NativeDecide.md) - - [nlinarith: 非線形な(不)等式を示す](./Reference/Tactic/Nlinarith.md) - - [norm_cast: 型キャストの簡略化](./Reference/Tactic/NormCast.md) - - [nth_rw: n 番目の項だけ rw](./Reference/Tactic/NthRw.md) - - [obtain: 分解して取り出す](./Reference/Tactic/Obtain.md) - - [omega: 自然数の線形計画を解く](./Reference/Tactic/Omega.md) - - [plausible: 反例を見つける](./Reference/Tactic/Plausible.md) - - [positivity: 正値性を示す](./Reference/Tactic/Positivity.md) - - [push_neg: ドモルガン](./Reference/Tactic/PushNeg.md) - - [qify: 有理数にキャストする](./Reference/Tactic/Qify.md) - - [rcases: パターン分解](./Reference/Tactic/Rcases.md) - - [refine: 穴埋め推論](./Reference/Tactic/Refine.md) - - [rel: 不等式を使う](./Reference/Tactic/Rel.md) - - [rename_i: 死んだ変数に名前を付ける](./Reference/Tactic/RenameI.md) - - [repeat: 繰り返し適用](./Reference/Tactic/Repeat.md) - - [replace: 補題の入れ替え](./Reference/Tactic/Replace.md) - - [rfl: 関係の反射性を利用する](./Reference/Tactic/Rfl.md) - - [right: 論理和∨を示す](./Reference/Tactic/Right.md) - - [ring: 可換環の等式を示す](./Reference/Tactic/Ring.md) - - [rw_search: rw で示せるか検索](./Reference/Tactic/RwSearch.md) - - [rw: 同値変形](./Reference/Tactic/Rw.md) - - [says: タクティク提案の痕跡を残す](./Reference/Tactic/Says.md) - - [set: 定義の導入](./Reference/Tactic/Set.md) - - [show: 示すべきことを宣言](./Reference/Tactic/Show.md) - - [simp_all: 仮定とゴールを全て単純化](./Reference/Tactic/SimpAll.md) - - [simp: 単純化](./Reference/Tactic/Simp.md) - - [sorry: 証明したことにする](./Reference/Tactic/Sorry.md) - - [split: if/match 式を分解](./Reference/Tactic/Split.md) - - [suffices: 十分条件に帰着](./Reference/Tactic/Suffices.md) - - [tauto: トートロジーを示す](./Reference/Tactic/Tauto.md) - - [trans: 推移律を利用する](./Reference/Tactic/Trans.md) - - [trivial: 基本的なタクティクを試す](./Reference/Tactic/Trivial.md) - - [try: 失敗をエラーにしない](./Reference/Tactic/Try.md) - - [unfold: 定義に展開](./Reference/Tactic/Unfold.md) - - [with_reducible: 透過度指定](./Reference/Tactic/WithReducible.md) - - [wlog: 一般性を失わずに特殊化](./Reference/Tactic/Wlog.md) - - [zify: 整数にキャストする](./Reference/Tactic/Zify.md) - -# 第2部: チュートリアル - -- [演習問題](./Tutorial/Exercise/README.md) - - [床屋のパラドクス](./Tutorial/Exercise/BarberParadox.md) - - [騎士と悪党のパズル](./Tutorial/Exercise/KnightAndKnave.md) - - [「ならば」の定義を疑う](./Tutorial/Exercise/DoubtImplication.md) - - [全射・単射と左逆・右逆写像](./Tutorial/Exercise/InverseSurjInj.md) - - [Cantorの定理](./Tutorial/Exercise/CantorTheorem.md) - - [Cantorの対関数の全単射性](./Tutorial/Exercise/CantorPairing.md) - - [Heying代数とBool代数](./Tutorial/Exercise/HeytingAndBooleanAlgebra.md) +- [タクティク](./Tactic/README.md) + - [<;> 生成された全ゴールに適用](./Tactic/SeqFocus.md) + - [ac_rfl: 可換性と結合性を使う](./Tactic/AcRfl.md) + - [aesop: 自明な証明の自動探索](./Tactic/Aesop.md) + - [all_goals: 全ゴールに対して適用](./Tactic/AllGoals.md) + - [apply at: apply を仮定に適用する](./Tactic/ApplyAt.md) + - [apply_assumption: 自動 apply](./Tactic/ApplyAssumption.md) + - [apply: 含意→を使う](./Tactic/Apply.md) + - [apply?: apply できるか検索](./Tactic/ApplyQuestion.md) + - [assumption: 仮定を自動で exact](./Tactic/Assumption.md) + - [by_cases: 排中律](./Tactic/ByCases.md) + - [by_contra: 背理法](./Tactic/ByContra.md) + - [by: タクティクモードに入る](./Tactic/By.md) + - [calc: 計算モードに入る](./Tactic/Calc.md) + - [cases: 場合分けをする](./Tactic/Cases.md) + - [cases': Lean3版のcases](./Tactic/CasesAp.md) + - [choose: 選択関数を得る](./Tactic/Choose.md) + - [clear: 命題や定義を削除する](./Tactic/Clear.md) + - [congr: ゴールの関数適用を外す](./Tactic/Congr.md) + - [constructor: 論理積や同値性を示す](./Tactic/Constructor.md) + - [contradiction: 矛盾を指摘](./Tactic/Contradiction.md) + - [contrapose: 対偶をとる](./Tactic/Contrapose.md) + - [conv: 変換モードに入る](./Tactic/Conv.md) + - [convert: 惜しい補題を使う](./Tactic/Convert.md) + - [decide: 決定可能な命題を示す](./Tactic/Decide.md) + - [done: 証明終了を宣言](./Tactic/Done.md) + - [dsimp: 定義に展開](./Tactic/Dsimp.md) + - [exact: 証明を直接構成](./Tactic/Exact.md) + - [exact?: exact できるか検索](./Tactic/ExactQuestion.md) + - [exfalso: 矛盾を示すことに帰着](./Tactic/Exfalso.md) + - [exists: 存在∃を示す](./Tactic/Exists.md) + - [ext: 外延性を使う](./Tactic/Ext.md) + - [field_simp: 分母を払う](./Tactic/FieldSimp.md) + - [fin_cases: 場合分けを簡潔に行う](./Tactic/FinCases.md) + - [fun_prop: 関数の諸性質を示す](./Tactic/FunProp.md) + - [funext: 関数等式を示す](./Tactic/Funext.md) + - [gcongr: 合同性を用いる](./Tactic/Gcongr.md) + - [generalize: 一般化する](./Tactic/Generalize.md) + - [guard_hyp: 仮定や補題を確認](./Tactic/GuardHyp.md) + - [have: 補題を用意する](./Tactic/Have.md) + - [hint: 複数のタクティクを同時に試す](./Tactic/Hint.md) + - [induction: 帰納法](./Tactic/Induction.md) + - [induction': inductionの構文違い](./Tactic/InductionAp.md) + - [intro: 含意→や全称∀を示す](./Tactic/Intro.md) + - [itauto: 直観主義論理の枠内で示す](./Tactic/Itauto.md) + - [left: 論理和∨を示す](./Tactic/Left.md) + - [linarith: 線形(不)等式を示す](./Tactic/Linarith.md) + - [native_decide: 実行による証明](./Tactic/NativeDecide.md) + - [nlinarith: 非線形な(不)等式を示す](./Tactic/Nlinarith.md) + - [norm_cast: 型キャストの簡略化](./Tactic/NormCast.md) + - [nth_rw: n 番目の項だけ rw](./Tactic/NthRw.md) + - [obtain: 分解して取り出す](./Tactic/Obtain.md) + - [omega: 自然数の線形計画を解く](./Tactic/Omega.md) + - [plausible: 反例を見つける](./Tactic/Plausible.md) + - [positivity: 正値性を示す](./Tactic/Positivity.md) + - [push_neg: ドモルガン](./Tactic/PushNeg.md) + - [qify: 有理数にキャストする](./Tactic/Qify.md) + - [rcases: パターン分解](./Tactic/Rcases.md) + - [refine: 穴埋め推論](./Tactic/Refine.md) + - [rel: 不等式を使う](./Tactic/Rel.md) + - [rename_i: 死んだ変数に名前を付ける](./Tactic/RenameI.md) + - [repeat: 繰り返し適用](./Tactic/Repeat.md) + - [replace: 補題の入れ替え](./Tactic/Replace.md) + - [rfl: 関係の反射性を利用する](./Tactic/Rfl.md) + - [right: 論理和∨を示す](./Tactic/Right.md) + - [ring: 可換環の等式を示す](./Tactic/Ring.md) + - [rw_search: rw で示せるか検索](./Tactic/RwSearch.md) + - [rw: 同値変形](./Tactic/Rw.md) + - [says: タクティク提案の痕跡を残す](./Tactic/Says.md) + - [set: 定義の導入](./Tactic/Set.md) + - [show: 示すべきことを宣言](./Tactic/Show.md) + - [simp_all: 仮定とゴールを全て単純化](./Tactic/SimpAll.md) + - [simp: 単純化](./Tactic/Simp.md) + - [sorry: 証明したことにする](./Tactic/Sorry.md) + - [split: if/match 式を分解](./Tactic/Split.md) + - [suffices: 十分条件に帰着](./Tactic/Suffices.md) + - [tauto: トートロジーを示す](./Tactic/Tauto.md) + - [trans: 推移律を利用する](./Tactic/Trans.md) + - [trivial: 基本的なタクティクを試す](./Tactic/Trivial.md) + - [try: 失敗をエラーにしない](./Tactic/Try.md) + - [unfold: 定義に展開](./Tactic/Unfold.md) + - [with_reducible: 透過度指定](./Tactic/WithReducible.md) + - [wlog: 一般性を失わずに特殊化](./Tactic/Wlog.md) + - [zify: 整数にキャストする](./Tactic/Zify.md) diff --git a/lake-manifest.json b/lake-manifest.json index 9729fba2..a08ce866 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -21,16 +21,6 @@ "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/Seasawher/mk-exercise.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "ff99a9be9854683448f745835ddf09fb5d800f9b", - "name": "«mk-exercise»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, diff --git a/lakefile.lean b/lakefile.lean index 512d222c..dbbd2fea 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -20,9 +20,6 @@ package «Lean by Example» where ] ++ linterOptions.map (fun s ↦ {s with name := `weak ++ s.name}) moreServerOptions := linterOptions -require «mk-exercise» from git - "https://github.com/Seasawher/mk-exercise.git" @ "main" - require mdgen from git "https://github.com/Seasawher/mdgen" @ "main" @@ -33,7 +30,7 @@ require mathlib from git lean_lib LeanByExample where -- `lake build` の実行時にビルドされるファイルの設定 -- `.submodules` と指定すると、そのディレクトリ以下の全ての Lean ファイルがビルドされる - globs := #[.submodules `LeanByExample.Reference, .submodules `LeanByExample.Tutorial.Solution] + globs := #[.submodules `LeanByExample] section Script @@ -61,14 +58,9 @@ macro_rules let end_time ← IO.monoMsNow; IO.println s!"Running {$s}: {end_time - start_time}ms") -/-- mk_exercise と mdgen と mdbook を順に実行し、 -Lean ファイルから Markdown ファイルと HTML ファイルを生成する。 - -`.\scripts\Build.ps1` を実行したほうが高速 -/ +/-- mdgen と mdbook を順に実行し、 +Lean ファイルから Markdown ファイルと HTML ファイルを生成する。-/ script build do - with_time running "mk_exercise" - runCmd "lake exe mk_exercise LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise" - with_time running "mdgen" runCmd "lake exe mdgen LeanByExample booksrc" diff --git a/scripts/Build.ps1 b/scripts/Build.ps1 deleted file mode 100644 index ce00b8c1..00000000 --- a/scripts/Build.ps1 +++ /dev/null @@ -1,10 +0,0 @@ -<# lake run build に相当するスクリプト - -lake を介することで実行が遅くなってしまうので、 -lake を介することなく実行ファイルを直接叩く。 #> - -./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise - -./.lake/packages/mdgen/.lake/build/bin/mdgen.exe LeanByExample booksrc - -mdbook build