From c214cf1ede8efc9ecf5b5b50a98d3ff2372b97d8 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 07:22:40 +0900 Subject: [PATCH 1/7] =?UTF-8?q?=E3=83=87=E3=82=A3=E3=83=AC=E3=82=AF?= =?UTF-8?q?=E3=83=88=E3=83=AA=E6=A7=8B=E6=88=90=E5=A4=89=E6=9B=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/CONTRIBUTING.md | 2 +- .github/workflows/sync.yml | 8 +- Exercise/README.lean | 2 +- .../Attribute/AppUnexpander.lean | 0 .../Attribute/CasesEliminator.lean | 0 .../{ => Reference}/Attribute/Coe.lean | 0 .../{ => Reference}/Attribute/Csimp.lean | 0 .../Attribute/DefaultInstance.lean | 0 .../Attribute/InductionEliminator.lean | 0 .../{ => Reference}/Attribute/InheritDoc.lean | 0 .../Attribute/MatchPattern.lean | 0 .../{ => Reference}/Attribute/README.lean | 0 .../{ => Reference}/Attribute/Simps.lean | 0 .../{ => Reference}/Declarative/Abbrev.lean | 0 .../Declarative/AddAesopRules.lean | 0 .../Declarative/Attribute.lean | 0 .../{ => Reference}/Declarative/Axiom.lean | 0 .../{ => Reference}/Declarative/Class.lean | 0 .../Declarative/DeclareSyntaxCat.lean | 0 .../{ => Reference}/Declarative/Def.lean | 0 .../{ => Reference}/Declarative/Deriving.lean | 0 .../{ => Reference}/Declarative/Elab.lean | 0 .../{ => Reference}/Declarative/Example.lean | 0 .../{ => Reference}/Declarative/Export.lean | 0 .../Declarative/Inductive.lean | 0 .../{ => Reference}/Declarative/Infix.lean | 0 .../{ => Reference}/Declarative/Instance.lean | 0 .../{ => Reference}/Declarative/Local.lean | 0 .../{ => Reference}/Declarative/Macro.lean | 0 .../Declarative/MacroRules.lean | 0 .../Declarative/Namespace.lean | 0 .../Declarative/Noncomputable.lean | 0 .../{ => Reference}/Declarative/Notation.lean | 0 .../{ => Reference}/Declarative/Opaque.lean | 0 .../{ => Reference}/Declarative/Open.lean | 0 .../{ => Reference}/Declarative/Partial.lean | 0 .../{ => Reference}/Declarative/Postfix.lean | 0 .../{ => Reference}/Declarative/Prefix.lean | 0 .../{ => Reference}/Declarative/Private.lean | 0 .../Declarative/ProofWanted.lean | 0 .../Declarative/Protected.lean | 0 .../{ => Reference}/Declarative/README.lean | 0 .../{ => Reference}/Declarative/Scoped.lean | 0 .../{ => Reference}/Declarative/Section.lean | 0 .../Declarative/SetOption.lean | 0 .../Declarative/Structure.lean | 0 .../{ => Reference}/Declarative/Syntax.lean | 0 .../Declarative/TerminationBy.lean | 0 .../{ => Reference}/Declarative/Theorem.lean | 0 .../{ => Reference}/Declarative/Variable.lean | 0 .../{ => Reference}/Diagnostic/Check.lean | 0 .../Diagnostic/CheckFailure.lean | 0 .../{ => Reference}/Diagnostic/Eval.lean | 0 .../{ => Reference}/Diagnostic/Find.lean | 0 .../{ => Reference}/Diagnostic/Guard.lean | 0 .../{ => Reference}/Diagnostic/GuardMsgs.lean | 0 .../{ => Reference}/Diagnostic/Help.lean | 0 .../{ => Reference}/Diagnostic/Instances.lean | 0 .../{ => Reference}/Diagnostic/Print.lean | 0 .../{ => Reference}/Diagnostic/README.lean | 0 .../{ => Reference}/Diagnostic/Reduce.lean | 0 .../{ => Reference}/Diagnostic/Synth.lean | 0 .../{ => Reference}/Diagnostic/Time.lean | 0 .../{ => Reference}/Diagnostic/Whnf.lean | 0 .../{ => Reference}/Option/AutoImplicit.lean | 0 .../{ => Reference}/Option/Flexible.lean | 0 .../{ => Reference}/Option/Hygiene.lean | 0 .../{ => Reference}/Option/README.lean | 0 .../{ => Reference}/Tactic/AcRfl.lean | 0 .../{ => Reference}/Tactic/Aesop.lean | 0 .../{ => Reference}/Tactic/AllGoals.lean | 0 .../{ => Reference}/Tactic/Apply.lean | 0 .../Tactic/ApplyAssumption.lean | 0 .../{ => Reference}/Tactic/ApplyAt.lean | 0 .../{ => Reference}/Tactic/ApplyQuestion.lean | 0 .../{ => Reference}/Tactic/Assumption.lean | 0 LeanByExample/{ => Reference}/Tactic/By.lean | 0 .../{ => Reference}/Tactic/ByCases.lean | 0 .../{ => Reference}/Tactic/ByContra.lean | 0 .../{ => Reference}/Tactic/Calc.lean | 0 .../{ => Reference}/Tactic/Cases.lean | 0 .../{ => Reference}/Tactic/CasesAp.lean | 0 .../{ => Reference}/Tactic/Choose.lean | 0 .../{ => Reference}/Tactic/Clear.lean | 0 .../{ => Reference}/Tactic/Congr.lean | 0 .../{ => Reference}/Tactic/Constructor.lean | 0 .../{ => Reference}/Tactic/Contradiction.lean | 0 .../{ => Reference}/Tactic/Contrapose.lean | 0 .../{ => Reference}/Tactic/Conv.lean | 0 .../{ => Reference}/Tactic/Convert.lean | 0 .../{ => Reference}/Tactic/Decide.lean | 0 .../{ => Reference}/Tactic/Done.lean | 0 .../{ => Reference}/Tactic/Dsimp.lean | 0 .../{ => Reference}/Tactic/Exact.lean | 0 .../{ => Reference}/Tactic/ExactQuestion.lean | 0 .../{ => Reference}/Tactic/Exfalso.lean | 0 .../{ => Reference}/Tactic/Exists.lean | 0 LeanByExample/{ => Reference}/Tactic/Ext.lean | 0 .../{ => Reference}/Tactic/FieldSimp.lean | 0 .../{ => Reference}/Tactic/FinCases.lean | 0 .../{ => Reference}/Tactic/FunProp.lean | 0 .../{ => Reference}/Tactic/Funext.lean | 0 .../{ => Reference}/Tactic/Gcongr.lean | 0 .../{ => Reference}/Tactic/Generalize.lean | 0 .../{ => Reference}/Tactic/GuardHyp.lean | 0 .../{ => Reference}/Tactic/Have.lean | 0 .../{ => Reference}/Tactic/Hint.lean | 0 .../{ => Reference}/Tactic/Induction.lean | 0 .../{ => Reference}/Tactic/InductionAp.lean | 0 .../{ => Reference}/Tactic/Intro.lean | 0 .../{ => Reference}/Tactic/Itauto.lean | 0 .../{ => Reference}/Tactic/Left.lean | 0 .../{ => Reference}/Tactic/Linarith.lean | 0 .../{ => Reference}/Tactic/NativeDecide.lean | 0 .../{ => Reference}/Tactic/Nlinarith.lean | 0 .../{ => Reference}/Tactic/NormCast.lean | 0 .../{ => Reference}/Tactic/NthRw.lean | 0 .../{ => Reference}/Tactic/Obtain.lean | 0 .../{ => Reference}/Tactic/Omega.lean | 0 .../{ => Reference}/Tactic/Positivity.lean | 0 .../{ => Reference}/Tactic/PushNeg.lean | 0 .../{ => Reference}/Tactic/Qify.lean | 0 .../{ => Reference}/Tactic/README.lean | 0 .../{ => Reference}/Tactic/Rcases.lean | 0 .../{ => Reference}/Tactic/Refine.lean | 0 LeanByExample/{ => Reference}/Tactic/Rel.lean | 0 .../{ => Reference}/Tactic/RenameI.lean | 0 .../{ => Reference}/Tactic/Repeat.lean | 0 .../{ => Reference}/Tactic/Replace.lean | 0 LeanByExample/{ => Reference}/Tactic/Rfl.lean | 0 .../{ => Reference}/Tactic/Right.lean | 0 .../{ => Reference}/Tactic/Ring.lean | 0 LeanByExample/{ => Reference}/Tactic/Rw.lean | 0 .../{ => Reference}/Tactic/RwSearch.lean | 0 .../{ => Reference}/Tactic/Says.lean | 0 .../{ => Reference}/Tactic/SeqFocus.lean | 0 LeanByExample/{ => Reference}/Tactic/Set.lean | 0 .../{ => Reference}/Tactic/Show.lean | 0 .../{ => Reference}/Tactic/Simp.lean | 0 .../{ => Reference}/Tactic/SlimCheck.lean | 0 .../{ => Reference}/Tactic/Sorry.lean | 0 .../{ => Reference}/Tactic/Split.lean | 0 .../{ => Reference}/Tactic/Suffices.lean | 0 .../{ => Reference}/Tactic/Tauto.lean | 0 .../{ => Reference}/Tactic/Trans.lean | 0 .../{ => Reference}/Tactic/Trivial.lean | 0 LeanByExample/{ => Reference}/Tactic/Try.lean | 0 .../{ => Reference}/Tactic/Unfold.lean | 0 .../{ => Reference}/Tactic/WithReducible.lean | 0 .../{ => Reference}/Tactic/Wlog.lean | 0 LeanByExample/{ => Reference}/Type/Char.lean | 0 LeanByExample/{ => Reference}/Type/Float.lean | 0 LeanByExample/{ => Reference}/Type/List.lean | 0 LeanByExample/{ => Reference}/Type/Prop.lean | 0 .../{ => Reference}/Type/README.lean | 0 .../{ => Reference}/Type/String.lean | 0 LeanByExample/{ => Reference}/Type/Type.lean | 0 .../{ => Reference}/TypeClass/Coe.lean | 0 .../{ => Reference}/TypeClass/CoeDep.lean | 0 .../{ => Reference}/TypeClass/CoeFun.lean | 0 .../{ => Reference}/TypeClass/CoeSort.lean | 0 .../{ => Reference}/TypeClass/Decidable.lean | 0 .../{ => Reference}/TypeClass/GetElem.lean | 0 .../{ => Reference}/TypeClass/Inhabited.lean | 0 .../{ => Reference}/TypeClass/OfNat.lean | 0 .../{ => Reference}/TypeClass/README.lean | 0 .../{ => Reference}/TypeClass/Repr.lean | 0 .../{ => Reference}/TypeClass/ToString.lean | 0 .../Tutorial/Exercise/BarberParadox.lean | 39 ++ .../Tutorial/Exercise/CantorPairing.lean | 156 ++++++++ .../Tutorial/Exercise/CantorTheorem.lean | 211 +++++++++++ .../Tutorial/Exercise/DoubtImplication.lean | 99 +++++ .../Exercise/HeytingAndBooleanAlgebra.lean | 317 ++++++++++++++++ .../Tutorial/Exercise/InverseSurjInj.lean | 76 ++++ .../Tutorial/Exercise/KnightAndKnave.lean | 155 ++++++++ .../Exercise}/README.lean | 2 +- .../Solution/BarberParadox.lean | 0 .../Solution/CantorPairing.lean | 0 .../Solution/CantorTheorem.lean | 0 .../Solution/DoubtImplication.lean | 0 .../Solution/HeytingAndBooleanAlgebra.lean | 0 .../Solution/InverseSurjInj.lean | 0 .../Solution/KnightAndKnave.lean | 0 LeanByExample/Tutorial/Solution/README.lean | 19 + assets/filePlay.js | 6 - booksrc/SUMMARY.md | 344 +++++++++--------- lakefile.lean | 14 +- scripts/Build.ps1 | 3 +- 188 files changed, 1255 insertions(+), 198 deletions(-) rename LeanByExample/{ => Reference}/Attribute/AppUnexpander.lean (100%) rename LeanByExample/{ => Reference}/Attribute/CasesEliminator.lean (100%) rename LeanByExample/{ => Reference}/Attribute/Coe.lean (100%) rename LeanByExample/{ => Reference}/Attribute/Csimp.lean (100%) rename LeanByExample/{ => Reference}/Attribute/DefaultInstance.lean (100%) rename LeanByExample/{ => Reference}/Attribute/InductionEliminator.lean (100%) rename LeanByExample/{ => Reference}/Attribute/InheritDoc.lean (100%) rename LeanByExample/{ => Reference}/Attribute/MatchPattern.lean (100%) rename LeanByExample/{ => Reference}/Attribute/README.lean (100%) rename LeanByExample/{ => Reference}/Attribute/Simps.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Abbrev.lean (100%) rename LeanByExample/{ => Reference}/Declarative/AddAesopRules.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Attribute.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Axiom.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Class.lean (100%) rename LeanByExample/{ => Reference}/Declarative/DeclareSyntaxCat.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Def.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Deriving.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Elab.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Example.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Export.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Inductive.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Infix.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Instance.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Local.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Macro.lean (100%) rename LeanByExample/{ => Reference}/Declarative/MacroRules.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Namespace.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Noncomputable.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Notation.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Opaque.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Open.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Partial.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Postfix.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Prefix.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Private.lean (100%) rename LeanByExample/{ => Reference}/Declarative/ProofWanted.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Protected.lean (100%) rename LeanByExample/{ => Reference}/Declarative/README.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Scoped.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Section.lean (100%) rename LeanByExample/{ => Reference}/Declarative/SetOption.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Structure.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Syntax.lean (100%) rename LeanByExample/{ => Reference}/Declarative/TerminationBy.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Theorem.lean (100%) rename LeanByExample/{ => Reference}/Declarative/Variable.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Check.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/CheckFailure.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Eval.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Find.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Guard.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/GuardMsgs.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Help.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Instances.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Print.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/README.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Reduce.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Synth.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Time.lean (100%) rename LeanByExample/{ => Reference}/Diagnostic/Whnf.lean (100%) rename LeanByExample/{ => Reference}/Option/AutoImplicit.lean (100%) rename LeanByExample/{ => Reference}/Option/Flexible.lean (100%) rename LeanByExample/{ => Reference}/Option/Hygiene.lean (100%) rename LeanByExample/{ => Reference}/Option/README.lean (100%) rename LeanByExample/{ => Reference}/Tactic/AcRfl.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Aesop.lean (100%) rename LeanByExample/{ => Reference}/Tactic/AllGoals.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Apply.lean (100%) rename LeanByExample/{ => Reference}/Tactic/ApplyAssumption.lean (100%) rename LeanByExample/{ => Reference}/Tactic/ApplyAt.lean (100%) rename LeanByExample/{ => Reference}/Tactic/ApplyQuestion.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Assumption.lean (100%) rename LeanByExample/{ => Reference}/Tactic/By.lean (100%) rename LeanByExample/{ => Reference}/Tactic/ByCases.lean (100%) rename LeanByExample/{ => Reference}/Tactic/ByContra.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Calc.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Cases.lean (100%) rename LeanByExample/{ => Reference}/Tactic/CasesAp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Choose.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Clear.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Congr.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Constructor.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Contradiction.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Contrapose.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Conv.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Convert.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Decide.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Done.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Dsimp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Exact.lean (100%) rename LeanByExample/{ => Reference}/Tactic/ExactQuestion.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Exfalso.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Exists.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Ext.lean (100%) rename LeanByExample/{ => Reference}/Tactic/FieldSimp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/FinCases.lean (100%) rename LeanByExample/{ => Reference}/Tactic/FunProp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Funext.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Gcongr.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Generalize.lean (100%) rename LeanByExample/{ => Reference}/Tactic/GuardHyp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Have.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Hint.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Induction.lean (100%) rename LeanByExample/{ => Reference}/Tactic/InductionAp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Intro.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Itauto.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Left.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Linarith.lean (100%) rename LeanByExample/{ => Reference}/Tactic/NativeDecide.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Nlinarith.lean (100%) rename LeanByExample/{ => Reference}/Tactic/NormCast.lean (100%) rename LeanByExample/{ => Reference}/Tactic/NthRw.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Obtain.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Omega.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Positivity.lean (100%) rename LeanByExample/{ => Reference}/Tactic/PushNeg.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Qify.lean (100%) rename LeanByExample/{ => Reference}/Tactic/README.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Rcases.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Refine.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Rel.lean (100%) rename LeanByExample/{ => Reference}/Tactic/RenameI.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Repeat.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Replace.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Rfl.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Right.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Ring.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Rw.lean (100%) rename LeanByExample/{ => Reference}/Tactic/RwSearch.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Says.lean (100%) rename LeanByExample/{ => Reference}/Tactic/SeqFocus.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Set.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Show.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Simp.lean (100%) rename LeanByExample/{ => Reference}/Tactic/SlimCheck.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Sorry.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Split.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Suffices.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Tauto.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Trans.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Trivial.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Try.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Unfold.lean (100%) rename LeanByExample/{ => Reference}/Tactic/WithReducible.lean (100%) rename LeanByExample/{ => Reference}/Tactic/Wlog.lean (100%) rename LeanByExample/{ => Reference}/Type/Char.lean (100%) rename LeanByExample/{ => Reference}/Type/Float.lean (100%) rename LeanByExample/{ => Reference}/Type/List.lean (100%) rename LeanByExample/{ => Reference}/Type/Prop.lean (100%) rename LeanByExample/{ => Reference}/Type/README.lean (100%) rename LeanByExample/{ => Reference}/Type/String.lean (100%) rename LeanByExample/{ => Reference}/Type/Type.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/Coe.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/CoeDep.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/CoeFun.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/CoeSort.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/Decidable.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/GetElem.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/Inhabited.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/OfNat.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/README.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/Repr.lean (100%) rename LeanByExample/{ => Reference}/TypeClass/ToString.lean (100%) create mode 100644 LeanByExample/Tutorial/Exercise/BarberParadox.lean create mode 100644 LeanByExample/Tutorial/Exercise/CantorPairing.lean create mode 100644 LeanByExample/Tutorial/Exercise/CantorTheorem.lean create mode 100644 LeanByExample/Tutorial/Exercise/DoubtImplication.lean create mode 100644 LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean create mode 100644 LeanByExample/Tutorial/Exercise/InverseSurjInj.lean create mode 100644 LeanByExample/Tutorial/Exercise/KnightAndKnave.lean rename LeanByExample/{Solution => Tutorial/Exercise}/README.lean (91%) rename LeanByExample/{ => Tutorial}/Solution/BarberParadox.lean (100%) rename LeanByExample/{ => Tutorial}/Solution/CantorPairing.lean (100%) rename LeanByExample/{ => Tutorial}/Solution/CantorTheorem.lean (100%) rename LeanByExample/{ => Tutorial}/Solution/DoubtImplication.lean (100%) rename LeanByExample/{ => Tutorial}/Solution/HeytingAndBooleanAlgebra.lean (100%) rename LeanByExample/{ => Tutorial}/Solution/InverseSurjInj.lean (100%) rename LeanByExample/{ => Tutorial}/Solution/KnightAndKnave.lean (100%) create mode 100644 LeanByExample/Tutorial/Solution/README.lean diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index fac39544..1db01092 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -16,7 +16,7 @@ ## 開発の流れ * このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に `lake exe cache get` を実行してください。 -* `Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。 +* `LeanByExample/Tutorial/Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。 * 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば mk_exercise の実行と markdown の生成と `mdbook build` が一括実行されます。 ## ルール diff --git a/.github/workflows/sync.yml b/.github/workflows/sync.yml index 8cc04024..5f1a406d 100644 --- a/.github/workflows/sync.yml +++ b/.github/workflows/sync.yml @@ -36,13 +36,13 @@ jobs: # いったん演習ファイルを全て削除している - name: run mk_exercise run: | - rm -r Exercise - lake run mk_exercise + rm -r LeanByExample/Tutorial/Exercise + lake exe mk_exercise LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise - name: detect diff id: diff run: | - git add -N Exercise + git add -N LeanByExample/Tutorial/Exercise git diff --name-only --exit-code continue-on-error: true @@ -51,6 +51,6 @@ jobs: run: | git config user.name "GitHub Action" git config user.email "action@github.com" - git add Exercise + git add LeanByExample/Tutorial/Exercise git commit -m "generated by GitHub Action" git push origin HEAD:${{ github.event.pull_request.head.ref }} diff --git a/Exercise/README.lean b/Exercise/README.lean index 9f6608c7..674b4ba8 100644 --- a/Exercise/README.lean +++ b/Exercise/README.lean @@ -7,7 +7,7 @@ 解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。 -Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`Exercise` ディレクトリの中にある該当ファイルを開いてください。 +Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`LeanByExample/Tutorial/Exercise` ディレクトリの中にある該当ファイルを開いてください。 [![codespace badge](https://github.com/codespaces/badge.svg)](https://codespaces.new/lean-ja/lean-by-example) diff --git a/LeanByExample/Attribute/AppUnexpander.lean b/LeanByExample/Reference/Attribute/AppUnexpander.lean similarity index 100% rename from LeanByExample/Attribute/AppUnexpander.lean rename to LeanByExample/Reference/Attribute/AppUnexpander.lean diff --git a/LeanByExample/Attribute/CasesEliminator.lean b/LeanByExample/Reference/Attribute/CasesEliminator.lean similarity index 100% rename from LeanByExample/Attribute/CasesEliminator.lean rename to LeanByExample/Reference/Attribute/CasesEliminator.lean diff --git a/LeanByExample/Attribute/Coe.lean b/LeanByExample/Reference/Attribute/Coe.lean similarity index 100% rename from LeanByExample/Attribute/Coe.lean rename to LeanByExample/Reference/Attribute/Coe.lean diff --git a/LeanByExample/Attribute/Csimp.lean b/LeanByExample/Reference/Attribute/Csimp.lean similarity index 100% rename from LeanByExample/Attribute/Csimp.lean rename to LeanByExample/Reference/Attribute/Csimp.lean diff --git a/LeanByExample/Attribute/DefaultInstance.lean b/LeanByExample/Reference/Attribute/DefaultInstance.lean similarity index 100% rename from LeanByExample/Attribute/DefaultInstance.lean rename to LeanByExample/Reference/Attribute/DefaultInstance.lean diff --git a/LeanByExample/Attribute/InductionEliminator.lean b/LeanByExample/Reference/Attribute/InductionEliminator.lean similarity index 100% rename from LeanByExample/Attribute/InductionEliminator.lean rename to LeanByExample/Reference/Attribute/InductionEliminator.lean diff --git a/LeanByExample/Attribute/InheritDoc.lean b/LeanByExample/Reference/Attribute/InheritDoc.lean similarity index 100% rename from LeanByExample/Attribute/InheritDoc.lean rename to LeanByExample/Reference/Attribute/InheritDoc.lean diff --git a/LeanByExample/Attribute/MatchPattern.lean b/LeanByExample/Reference/Attribute/MatchPattern.lean similarity index 100% rename from LeanByExample/Attribute/MatchPattern.lean rename to LeanByExample/Reference/Attribute/MatchPattern.lean diff --git a/LeanByExample/Attribute/README.lean b/LeanByExample/Reference/Attribute/README.lean similarity index 100% rename from LeanByExample/Attribute/README.lean rename to LeanByExample/Reference/Attribute/README.lean diff --git a/LeanByExample/Attribute/Simps.lean b/LeanByExample/Reference/Attribute/Simps.lean similarity index 100% rename from LeanByExample/Attribute/Simps.lean rename to LeanByExample/Reference/Attribute/Simps.lean diff --git a/LeanByExample/Declarative/Abbrev.lean b/LeanByExample/Reference/Declarative/Abbrev.lean similarity index 100% rename from LeanByExample/Declarative/Abbrev.lean rename to LeanByExample/Reference/Declarative/Abbrev.lean diff --git a/LeanByExample/Declarative/AddAesopRules.lean b/LeanByExample/Reference/Declarative/AddAesopRules.lean similarity index 100% rename from LeanByExample/Declarative/AddAesopRules.lean rename to LeanByExample/Reference/Declarative/AddAesopRules.lean diff --git a/LeanByExample/Declarative/Attribute.lean b/LeanByExample/Reference/Declarative/Attribute.lean similarity index 100% rename from LeanByExample/Declarative/Attribute.lean rename to LeanByExample/Reference/Declarative/Attribute.lean diff --git a/LeanByExample/Declarative/Axiom.lean b/LeanByExample/Reference/Declarative/Axiom.lean similarity index 100% rename from LeanByExample/Declarative/Axiom.lean rename to LeanByExample/Reference/Declarative/Axiom.lean diff --git a/LeanByExample/Declarative/Class.lean b/LeanByExample/Reference/Declarative/Class.lean similarity index 100% rename from LeanByExample/Declarative/Class.lean rename to LeanByExample/Reference/Declarative/Class.lean diff --git a/LeanByExample/Declarative/DeclareSyntaxCat.lean b/LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean similarity index 100% rename from LeanByExample/Declarative/DeclareSyntaxCat.lean rename to LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean diff --git a/LeanByExample/Declarative/Def.lean b/LeanByExample/Reference/Declarative/Def.lean similarity index 100% rename from LeanByExample/Declarative/Def.lean rename to LeanByExample/Reference/Declarative/Def.lean diff --git a/LeanByExample/Declarative/Deriving.lean b/LeanByExample/Reference/Declarative/Deriving.lean similarity index 100% rename from LeanByExample/Declarative/Deriving.lean rename to LeanByExample/Reference/Declarative/Deriving.lean diff --git a/LeanByExample/Declarative/Elab.lean b/LeanByExample/Reference/Declarative/Elab.lean similarity index 100% rename from LeanByExample/Declarative/Elab.lean rename to LeanByExample/Reference/Declarative/Elab.lean diff --git a/LeanByExample/Declarative/Example.lean b/LeanByExample/Reference/Declarative/Example.lean similarity index 100% rename from LeanByExample/Declarative/Example.lean rename to LeanByExample/Reference/Declarative/Example.lean diff --git a/LeanByExample/Declarative/Export.lean b/LeanByExample/Reference/Declarative/Export.lean similarity index 100% rename from LeanByExample/Declarative/Export.lean rename to LeanByExample/Reference/Declarative/Export.lean diff --git a/LeanByExample/Declarative/Inductive.lean b/LeanByExample/Reference/Declarative/Inductive.lean similarity index 100% rename from LeanByExample/Declarative/Inductive.lean rename to LeanByExample/Reference/Declarative/Inductive.lean diff --git a/LeanByExample/Declarative/Infix.lean b/LeanByExample/Reference/Declarative/Infix.lean similarity index 100% rename from LeanByExample/Declarative/Infix.lean rename to LeanByExample/Reference/Declarative/Infix.lean diff --git a/LeanByExample/Declarative/Instance.lean b/LeanByExample/Reference/Declarative/Instance.lean similarity index 100% rename from LeanByExample/Declarative/Instance.lean rename to LeanByExample/Reference/Declarative/Instance.lean diff --git a/LeanByExample/Declarative/Local.lean b/LeanByExample/Reference/Declarative/Local.lean similarity index 100% rename from LeanByExample/Declarative/Local.lean rename to LeanByExample/Reference/Declarative/Local.lean diff --git a/LeanByExample/Declarative/Macro.lean b/LeanByExample/Reference/Declarative/Macro.lean similarity index 100% rename from LeanByExample/Declarative/Macro.lean rename to LeanByExample/Reference/Declarative/Macro.lean diff --git a/LeanByExample/Declarative/MacroRules.lean b/LeanByExample/Reference/Declarative/MacroRules.lean similarity index 100% rename from LeanByExample/Declarative/MacroRules.lean rename to LeanByExample/Reference/Declarative/MacroRules.lean diff --git a/LeanByExample/Declarative/Namespace.lean b/LeanByExample/Reference/Declarative/Namespace.lean similarity index 100% rename from LeanByExample/Declarative/Namespace.lean rename to LeanByExample/Reference/Declarative/Namespace.lean diff --git a/LeanByExample/Declarative/Noncomputable.lean b/LeanByExample/Reference/Declarative/Noncomputable.lean similarity index 100% rename from LeanByExample/Declarative/Noncomputable.lean rename to LeanByExample/Reference/Declarative/Noncomputable.lean diff --git a/LeanByExample/Declarative/Notation.lean b/LeanByExample/Reference/Declarative/Notation.lean similarity index 100% rename from LeanByExample/Declarative/Notation.lean rename to LeanByExample/Reference/Declarative/Notation.lean diff --git a/LeanByExample/Declarative/Opaque.lean b/LeanByExample/Reference/Declarative/Opaque.lean similarity index 100% rename from LeanByExample/Declarative/Opaque.lean rename to LeanByExample/Reference/Declarative/Opaque.lean diff --git a/LeanByExample/Declarative/Open.lean b/LeanByExample/Reference/Declarative/Open.lean similarity index 100% rename from LeanByExample/Declarative/Open.lean rename to LeanByExample/Reference/Declarative/Open.lean diff --git a/LeanByExample/Declarative/Partial.lean b/LeanByExample/Reference/Declarative/Partial.lean similarity index 100% rename from LeanByExample/Declarative/Partial.lean rename to LeanByExample/Reference/Declarative/Partial.lean diff --git a/LeanByExample/Declarative/Postfix.lean b/LeanByExample/Reference/Declarative/Postfix.lean similarity index 100% rename from LeanByExample/Declarative/Postfix.lean rename to LeanByExample/Reference/Declarative/Postfix.lean diff --git a/LeanByExample/Declarative/Prefix.lean b/LeanByExample/Reference/Declarative/Prefix.lean similarity index 100% rename from LeanByExample/Declarative/Prefix.lean rename to LeanByExample/Reference/Declarative/Prefix.lean diff --git a/LeanByExample/Declarative/Private.lean b/LeanByExample/Reference/Declarative/Private.lean similarity index 100% rename from LeanByExample/Declarative/Private.lean rename to LeanByExample/Reference/Declarative/Private.lean diff --git a/LeanByExample/Declarative/ProofWanted.lean b/LeanByExample/Reference/Declarative/ProofWanted.lean similarity index 100% rename from LeanByExample/Declarative/ProofWanted.lean rename to LeanByExample/Reference/Declarative/ProofWanted.lean diff --git a/LeanByExample/Declarative/Protected.lean b/LeanByExample/Reference/Declarative/Protected.lean similarity index 100% rename from LeanByExample/Declarative/Protected.lean rename to LeanByExample/Reference/Declarative/Protected.lean diff --git a/LeanByExample/Declarative/README.lean b/LeanByExample/Reference/Declarative/README.lean similarity index 100% rename from LeanByExample/Declarative/README.lean rename to LeanByExample/Reference/Declarative/README.lean diff --git a/LeanByExample/Declarative/Scoped.lean b/LeanByExample/Reference/Declarative/Scoped.lean similarity index 100% rename from LeanByExample/Declarative/Scoped.lean rename to LeanByExample/Reference/Declarative/Scoped.lean diff --git a/LeanByExample/Declarative/Section.lean b/LeanByExample/Reference/Declarative/Section.lean similarity index 100% rename from LeanByExample/Declarative/Section.lean rename to LeanByExample/Reference/Declarative/Section.lean diff --git a/LeanByExample/Declarative/SetOption.lean b/LeanByExample/Reference/Declarative/SetOption.lean similarity index 100% rename from LeanByExample/Declarative/SetOption.lean rename to LeanByExample/Reference/Declarative/SetOption.lean diff --git a/LeanByExample/Declarative/Structure.lean b/LeanByExample/Reference/Declarative/Structure.lean similarity index 100% rename from LeanByExample/Declarative/Structure.lean rename to LeanByExample/Reference/Declarative/Structure.lean diff --git a/LeanByExample/Declarative/Syntax.lean b/LeanByExample/Reference/Declarative/Syntax.lean similarity index 100% rename from LeanByExample/Declarative/Syntax.lean rename to LeanByExample/Reference/Declarative/Syntax.lean diff --git a/LeanByExample/Declarative/TerminationBy.lean b/LeanByExample/Reference/Declarative/TerminationBy.lean similarity index 100% rename from LeanByExample/Declarative/TerminationBy.lean rename to LeanByExample/Reference/Declarative/TerminationBy.lean diff --git a/LeanByExample/Declarative/Theorem.lean b/LeanByExample/Reference/Declarative/Theorem.lean similarity index 100% rename from LeanByExample/Declarative/Theorem.lean rename to LeanByExample/Reference/Declarative/Theorem.lean diff --git a/LeanByExample/Declarative/Variable.lean b/LeanByExample/Reference/Declarative/Variable.lean similarity index 100% rename from LeanByExample/Declarative/Variable.lean rename to LeanByExample/Reference/Declarative/Variable.lean diff --git a/LeanByExample/Diagnostic/Check.lean b/LeanByExample/Reference/Diagnostic/Check.lean similarity index 100% rename from LeanByExample/Diagnostic/Check.lean rename to LeanByExample/Reference/Diagnostic/Check.lean diff --git a/LeanByExample/Diagnostic/CheckFailure.lean b/LeanByExample/Reference/Diagnostic/CheckFailure.lean similarity index 100% rename from LeanByExample/Diagnostic/CheckFailure.lean rename to LeanByExample/Reference/Diagnostic/CheckFailure.lean diff --git a/LeanByExample/Diagnostic/Eval.lean b/LeanByExample/Reference/Diagnostic/Eval.lean similarity index 100% rename from LeanByExample/Diagnostic/Eval.lean rename to LeanByExample/Reference/Diagnostic/Eval.lean diff --git a/LeanByExample/Diagnostic/Find.lean b/LeanByExample/Reference/Diagnostic/Find.lean similarity index 100% rename from LeanByExample/Diagnostic/Find.lean rename to LeanByExample/Reference/Diagnostic/Find.lean diff --git a/LeanByExample/Diagnostic/Guard.lean b/LeanByExample/Reference/Diagnostic/Guard.lean similarity index 100% rename from LeanByExample/Diagnostic/Guard.lean rename to LeanByExample/Reference/Diagnostic/Guard.lean diff --git a/LeanByExample/Diagnostic/GuardMsgs.lean b/LeanByExample/Reference/Diagnostic/GuardMsgs.lean similarity index 100% rename from LeanByExample/Diagnostic/GuardMsgs.lean rename to LeanByExample/Reference/Diagnostic/GuardMsgs.lean diff --git a/LeanByExample/Diagnostic/Help.lean b/LeanByExample/Reference/Diagnostic/Help.lean similarity index 100% rename from LeanByExample/Diagnostic/Help.lean rename to LeanByExample/Reference/Diagnostic/Help.lean diff --git a/LeanByExample/Diagnostic/Instances.lean b/LeanByExample/Reference/Diagnostic/Instances.lean similarity index 100% rename from LeanByExample/Diagnostic/Instances.lean rename to LeanByExample/Reference/Diagnostic/Instances.lean diff --git a/LeanByExample/Diagnostic/Print.lean b/LeanByExample/Reference/Diagnostic/Print.lean similarity index 100% rename from LeanByExample/Diagnostic/Print.lean rename to LeanByExample/Reference/Diagnostic/Print.lean diff --git a/LeanByExample/Diagnostic/README.lean b/LeanByExample/Reference/Diagnostic/README.lean similarity index 100% rename from LeanByExample/Diagnostic/README.lean rename to LeanByExample/Reference/Diagnostic/README.lean diff --git a/LeanByExample/Diagnostic/Reduce.lean b/LeanByExample/Reference/Diagnostic/Reduce.lean similarity index 100% rename from LeanByExample/Diagnostic/Reduce.lean rename to LeanByExample/Reference/Diagnostic/Reduce.lean diff --git a/LeanByExample/Diagnostic/Synth.lean b/LeanByExample/Reference/Diagnostic/Synth.lean similarity index 100% rename from LeanByExample/Diagnostic/Synth.lean rename to LeanByExample/Reference/Diagnostic/Synth.lean diff --git a/LeanByExample/Diagnostic/Time.lean b/LeanByExample/Reference/Diagnostic/Time.lean similarity index 100% rename from LeanByExample/Diagnostic/Time.lean rename to LeanByExample/Reference/Diagnostic/Time.lean diff --git a/LeanByExample/Diagnostic/Whnf.lean b/LeanByExample/Reference/Diagnostic/Whnf.lean similarity index 100% rename from LeanByExample/Diagnostic/Whnf.lean rename to LeanByExample/Reference/Diagnostic/Whnf.lean diff --git a/LeanByExample/Option/AutoImplicit.lean b/LeanByExample/Reference/Option/AutoImplicit.lean similarity index 100% rename from LeanByExample/Option/AutoImplicit.lean rename to LeanByExample/Reference/Option/AutoImplicit.lean diff --git a/LeanByExample/Option/Flexible.lean b/LeanByExample/Reference/Option/Flexible.lean similarity index 100% rename from LeanByExample/Option/Flexible.lean rename to LeanByExample/Reference/Option/Flexible.lean diff --git a/LeanByExample/Option/Hygiene.lean b/LeanByExample/Reference/Option/Hygiene.lean similarity index 100% rename from LeanByExample/Option/Hygiene.lean rename to LeanByExample/Reference/Option/Hygiene.lean diff --git a/LeanByExample/Option/README.lean b/LeanByExample/Reference/Option/README.lean similarity index 100% rename from LeanByExample/Option/README.lean rename to LeanByExample/Reference/Option/README.lean diff --git a/LeanByExample/Tactic/AcRfl.lean b/LeanByExample/Reference/Tactic/AcRfl.lean similarity index 100% rename from LeanByExample/Tactic/AcRfl.lean rename to LeanByExample/Reference/Tactic/AcRfl.lean diff --git a/LeanByExample/Tactic/Aesop.lean b/LeanByExample/Reference/Tactic/Aesop.lean similarity index 100% rename from LeanByExample/Tactic/Aesop.lean rename to LeanByExample/Reference/Tactic/Aesop.lean diff --git a/LeanByExample/Tactic/AllGoals.lean b/LeanByExample/Reference/Tactic/AllGoals.lean similarity index 100% rename from LeanByExample/Tactic/AllGoals.lean rename to LeanByExample/Reference/Tactic/AllGoals.lean diff --git a/LeanByExample/Tactic/Apply.lean b/LeanByExample/Reference/Tactic/Apply.lean similarity index 100% rename from LeanByExample/Tactic/Apply.lean rename to LeanByExample/Reference/Tactic/Apply.lean diff --git a/LeanByExample/Tactic/ApplyAssumption.lean b/LeanByExample/Reference/Tactic/ApplyAssumption.lean similarity index 100% rename from LeanByExample/Tactic/ApplyAssumption.lean rename to LeanByExample/Reference/Tactic/ApplyAssumption.lean diff --git a/LeanByExample/Tactic/ApplyAt.lean b/LeanByExample/Reference/Tactic/ApplyAt.lean similarity index 100% rename from LeanByExample/Tactic/ApplyAt.lean rename to LeanByExample/Reference/Tactic/ApplyAt.lean diff --git a/LeanByExample/Tactic/ApplyQuestion.lean b/LeanByExample/Reference/Tactic/ApplyQuestion.lean similarity index 100% rename from LeanByExample/Tactic/ApplyQuestion.lean rename to LeanByExample/Reference/Tactic/ApplyQuestion.lean diff --git a/LeanByExample/Tactic/Assumption.lean b/LeanByExample/Reference/Tactic/Assumption.lean similarity index 100% rename from LeanByExample/Tactic/Assumption.lean rename to LeanByExample/Reference/Tactic/Assumption.lean diff --git a/LeanByExample/Tactic/By.lean b/LeanByExample/Reference/Tactic/By.lean similarity index 100% rename from LeanByExample/Tactic/By.lean rename to LeanByExample/Reference/Tactic/By.lean diff --git a/LeanByExample/Tactic/ByCases.lean b/LeanByExample/Reference/Tactic/ByCases.lean similarity index 100% rename from LeanByExample/Tactic/ByCases.lean rename to LeanByExample/Reference/Tactic/ByCases.lean diff --git a/LeanByExample/Tactic/ByContra.lean b/LeanByExample/Reference/Tactic/ByContra.lean similarity index 100% rename from LeanByExample/Tactic/ByContra.lean rename to LeanByExample/Reference/Tactic/ByContra.lean diff --git a/LeanByExample/Tactic/Calc.lean b/LeanByExample/Reference/Tactic/Calc.lean similarity index 100% rename from LeanByExample/Tactic/Calc.lean rename to LeanByExample/Reference/Tactic/Calc.lean diff --git a/LeanByExample/Tactic/Cases.lean b/LeanByExample/Reference/Tactic/Cases.lean similarity index 100% rename from LeanByExample/Tactic/Cases.lean rename to LeanByExample/Reference/Tactic/Cases.lean diff --git a/LeanByExample/Tactic/CasesAp.lean b/LeanByExample/Reference/Tactic/CasesAp.lean similarity index 100% rename from LeanByExample/Tactic/CasesAp.lean rename to LeanByExample/Reference/Tactic/CasesAp.lean diff --git a/LeanByExample/Tactic/Choose.lean b/LeanByExample/Reference/Tactic/Choose.lean similarity index 100% rename from LeanByExample/Tactic/Choose.lean rename to LeanByExample/Reference/Tactic/Choose.lean diff --git a/LeanByExample/Tactic/Clear.lean b/LeanByExample/Reference/Tactic/Clear.lean similarity index 100% rename from LeanByExample/Tactic/Clear.lean rename to LeanByExample/Reference/Tactic/Clear.lean diff --git a/LeanByExample/Tactic/Congr.lean b/LeanByExample/Reference/Tactic/Congr.lean similarity index 100% rename from LeanByExample/Tactic/Congr.lean rename to LeanByExample/Reference/Tactic/Congr.lean diff --git a/LeanByExample/Tactic/Constructor.lean b/LeanByExample/Reference/Tactic/Constructor.lean similarity index 100% rename from LeanByExample/Tactic/Constructor.lean rename to LeanByExample/Reference/Tactic/Constructor.lean diff --git a/LeanByExample/Tactic/Contradiction.lean b/LeanByExample/Reference/Tactic/Contradiction.lean similarity index 100% rename from LeanByExample/Tactic/Contradiction.lean rename to LeanByExample/Reference/Tactic/Contradiction.lean diff --git a/LeanByExample/Tactic/Contrapose.lean b/LeanByExample/Reference/Tactic/Contrapose.lean similarity index 100% rename from LeanByExample/Tactic/Contrapose.lean rename to LeanByExample/Reference/Tactic/Contrapose.lean diff --git a/LeanByExample/Tactic/Conv.lean b/LeanByExample/Reference/Tactic/Conv.lean similarity index 100% rename from LeanByExample/Tactic/Conv.lean rename to LeanByExample/Reference/Tactic/Conv.lean diff --git a/LeanByExample/Tactic/Convert.lean b/LeanByExample/Reference/Tactic/Convert.lean similarity index 100% rename from LeanByExample/Tactic/Convert.lean rename to LeanByExample/Reference/Tactic/Convert.lean diff --git a/LeanByExample/Tactic/Decide.lean b/LeanByExample/Reference/Tactic/Decide.lean similarity index 100% rename from LeanByExample/Tactic/Decide.lean rename to LeanByExample/Reference/Tactic/Decide.lean diff --git a/LeanByExample/Tactic/Done.lean b/LeanByExample/Reference/Tactic/Done.lean similarity index 100% rename from LeanByExample/Tactic/Done.lean rename to LeanByExample/Reference/Tactic/Done.lean diff --git a/LeanByExample/Tactic/Dsimp.lean b/LeanByExample/Reference/Tactic/Dsimp.lean similarity index 100% rename from LeanByExample/Tactic/Dsimp.lean rename to LeanByExample/Reference/Tactic/Dsimp.lean diff --git a/LeanByExample/Tactic/Exact.lean b/LeanByExample/Reference/Tactic/Exact.lean similarity index 100% rename from LeanByExample/Tactic/Exact.lean rename to LeanByExample/Reference/Tactic/Exact.lean diff --git a/LeanByExample/Tactic/ExactQuestion.lean b/LeanByExample/Reference/Tactic/ExactQuestion.lean similarity index 100% rename from LeanByExample/Tactic/ExactQuestion.lean rename to LeanByExample/Reference/Tactic/ExactQuestion.lean diff --git a/LeanByExample/Tactic/Exfalso.lean b/LeanByExample/Reference/Tactic/Exfalso.lean similarity index 100% rename from LeanByExample/Tactic/Exfalso.lean rename to LeanByExample/Reference/Tactic/Exfalso.lean diff --git a/LeanByExample/Tactic/Exists.lean b/LeanByExample/Reference/Tactic/Exists.lean similarity index 100% rename from LeanByExample/Tactic/Exists.lean rename to LeanByExample/Reference/Tactic/Exists.lean diff --git a/LeanByExample/Tactic/Ext.lean b/LeanByExample/Reference/Tactic/Ext.lean similarity index 100% rename from LeanByExample/Tactic/Ext.lean rename to LeanByExample/Reference/Tactic/Ext.lean diff --git a/LeanByExample/Tactic/FieldSimp.lean b/LeanByExample/Reference/Tactic/FieldSimp.lean similarity index 100% rename from LeanByExample/Tactic/FieldSimp.lean rename to LeanByExample/Reference/Tactic/FieldSimp.lean diff --git a/LeanByExample/Tactic/FinCases.lean b/LeanByExample/Reference/Tactic/FinCases.lean similarity index 100% rename from LeanByExample/Tactic/FinCases.lean rename to LeanByExample/Reference/Tactic/FinCases.lean diff --git a/LeanByExample/Tactic/FunProp.lean b/LeanByExample/Reference/Tactic/FunProp.lean similarity index 100% rename from LeanByExample/Tactic/FunProp.lean rename to LeanByExample/Reference/Tactic/FunProp.lean diff --git a/LeanByExample/Tactic/Funext.lean b/LeanByExample/Reference/Tactic/Funext.lean similarity index 100% rename from LeanByExample/Tactic/Funext.lean rename to LeanByExample/Reference/Tactic/Funext.lean diff --git a/LeanByExample/Tactic/Gcongr.lean b/LeanByExample/Reference/Tactic/Gcongr.lean similarity index 100% rename from LeanByExample/Tactic/Gcongr.lean rename to LeanByExample/Reference/Tactic/Gcongr.lean diff --git a/LeanByExample/Tactic/Generalize.lean b/LeanByExample/Reference/Tactic/Generalize.lean similarity index 100% rename from LeanByExample/Tactic/Generalize.lean rename to LeanByExample/Reference/Tactic/Generalize.lean diff --git a/LeanByExample/Tactic/GuardHyp.lean b/LeanByExample/Reference/Tactic/GuardHyp.lean similarity index 100% rename from LeanByExample/Tactic/GuardHyp.lean rename to LeanByExample/Reference/Tactic/GuardHyp.lean diff --git a/LeanByExample/Tactic/Have.lean b/LeanByExample/Reference/Tactic/Have.lean similarity index 100% rename from LeanByExample/Tactic/Have.lean rename to LeanByExample/Reference/Tactic/Have.lean diff --git a/LeanByExample/Tactic/Hint.lean b/LeanByExample/Reference/Tactic/Hint.lean similarity index 100% rename from LeanByExample/Tactic/Hint.lean rename to LeanByExample/Reference/Tactic/Hint.lean diff --git a/LeanByExample/Tactic/Induction.lean b/LeanByExample/Reference/Tactic/Induction.lean similarity index 100% rename from LeanByExample/Tactic/Induction.lean rename to LeanByExample/Reference/Tactic/Induction.lean diff --git a/LeanByExample/Tactic/InductionAp.lean b/LeanByExample/Reference/Tactic/InductionAp.lean similarity index 100% rename from LeanByExample/Tactic/InductionAp.lean rename to LeanByExample/Reference/Tactic/InductionAp.lean diff --git a/LeanByExample/Tactic/Intro.lean b/LeanByExample/Reference/Tactic/Intro.lean similarity index 100% rename from LeanByExample/Tactic/Intro.lean rename to LeanByExample/Reference/Tactic/Intro.lean diff --git a/LeanByExample/Tactic/Itauto.lean b/LeanByExample/Reference/Tactic/Itauto.lean similarity index 100% rename from LeanByExample/Tactic/Itauto.lean rename to LeanByExample/Reference/Tactic/Itauto.lean diff --git a/LeanByExample/Tactic/Left.lean b/LeanByExample/Reference/Tactic/Left.lean similarity index 100% rename from LeanByExample/Tactic/Left.lean rename to LeanByExample/Reference/Tactic/Left.lean diff --git a/LeanByExample/Tactic/Linarith.lean b/LeanByExample/Reference/Tactic/Linarith.lean similarity index 100% rename from LeanByExample/Tactic/Linarith.lean rename to LeanByExample/Reference/Tactic/Linarith.lean diff --git a/LeanByExample/Tactic/NativeDecide.lean b/LeanByExample/Reference/Tactic/NativeDecide.lean similarity index 100% rename from LeanByExample/Tactic/NativeDecide.lean rename to LeanByExample/Reference/Tactic/NativeDecide.lean diff --git a/LeanByExample/Tactic/Nlinarith.lean b/LeanByExample/Reference/Tactic/Nlinarith.lean similarity index 100% rename from LeanByExample/Tactic/Nlinarith.lean rename to LeanByExample/Reference/Tactic/Nlinarith.lean diff --git a/LeanByExample/Tactic/NormCast.lean b/LeanByExample/Reference/Tactic/NormCast.lean similarity index 100% rename from LeanByExample/Tactic/NormCast.lean rename to LeanByExample/Reference/Tactic/NormCast.lean diff --git a/LeanByExample/Tactic/NthRw.lean b/LeanByExample/Reference/Tactic/NthRw.lean similarity index 100% rename from LeanByExample/Tactic/NthRw.lean rename to LeanByExample/Reference/Tactic/NthRw.lean diff --git a/LeanByExample/Tactic/Obtain.lean b/LeanByExample/Reference/Tactic/Obtain.lean similarity index 100% rename from LeanByExample/Tactic/Obtain.lean rename to LeanByExample/Reference/Tactic/Obtain.lean diff --git a/LeanByExample/Tactic/Omega.lean b/LeanByExample/Reference/Tactic/Omega.lean similarity index 100% rename from LeanByExample/Tactic/Omega.lean rename to LeanByExample/Reference/Tactic/Omega.lean diff --git a/LeanByExample/Tactic/Positivity.lean b/LeanByExample/Reference/Tactic/Positivity.lean similarity index 100% rename from LeanByExample/Tactic/Positivity.lean rename to LeanByExample/Reference/Tactic/Positivity.lean diff --git a/LeanByExample/Tactic/PushNeg.lean b/LeanByExample/Reference/Tactic/PushNeg.lean similarity index 100% rename from LeanByExample/Tactic/PushNeg.lean rename to LeanByExample/Reference/Tactic/PushNeg.lean diff --git a/LeanByExample/Tactic/Qify.lean b/LeanByExample/Reference/Tactic/Qify.lean similarity index 100% rename from LeanByExample/Tactic/Qify.lean rename to LeanByExample/Reference/Tactic/Qify.lean diff --git a/LeanByExample/Tactic/README.lean b/LeanByExample/Reference/Tactic/README.lean similarity index 100% rename from LeanByExample/Tactic/README.lean rename to LeanByExample/Reference/Tactic/README.lean diff --git a/LeanByExample/Tactic/Rcases.lean b/LeanByExample/Reference/Tactic/Rcases.lean similarity index 100% rename from LeanByExample/Tactic/Rcases.lean rename to LeanByExample/Reference/Tactic/Rcases.lean diff --git a/LeanByExample/Tactic/Refine.lean b/LeanByExample/Reference/Tactic/Refine.lean similarity index 100% rename from LeanByExample/Tactic/Refine.lean rename to LeanByExample/Reference/Tactic/Refine.lean diff --git a/LeanByExample/Tactic/Rel.lean b/LeanByExample/Reference/Tactic/Rel.lean similarity index 100% rename from LeanByExample/Tactic/Rel.lean rename to LeanByExample/Reference/Tactic/Rel.lean diff --git a/LeanByExample/Tactic/RenameI.lean b/LeanByExample/Reference/Tactic/RenameI.lean similarity index 100% rename from LeanByExample/Tactic/RenameI.lean rename to LeanByExample/Reference/Tactic/RenameI.lean diff --git a/LeanByExample/Tactic/Repeat.lean b/LeanByExample/Reference/Tactic/Repeat.lean similarity index 100% rename from LeanByExample/Tactic/Repeat.lean rename to LeanByExample/Reference/Tactic/Repeat.lean diff --git a/LeanByExample/Tactic/Replace.lean b/LeanByExample/Reference/Tactic/Replace.lean similarity index 100% rename from LeanByExample/Tactic/Replace.lean rename to LeanByExample/Reference/Tactic/Replace.lean diff --git a/LeanByExample/Tactic/Rfl.lean b/LeanByExample/Reference/Tactic/Rfl.lean similarity index 100% rename from LeanByExample/Tactic/Rfl.lean rename to LeanByExample/Reference/Tactic/Rfl.lean diff --git a/LeanByExample/Tactic/Right.lean b/LeanByExample/Reference/Tactic/Right.lean similarity index 100% rename from LeanByExample/Tactic/Right.lean rename to LeanByExample/Reference/Tactic/Right.lean diff --git a/LeanByExample/Tactic/Ring.lean b/LeanByExample/Reference/Tactic/Ring.lean similarity index 100% rename from LeanByExample/Tactic/Ring.lean rename to LeanByExample/Reference/Tactic/Ring.lean diff --git a/LeanByExample/Tactic/Rw.lean b/LeanByExample/Reference/Tactic/Rw.lean similarity index 100% rename from LeanByExample/Tactic/Rw.lean rename to LeanByExample/Reference/Tactic/Rw.lean diff --git a/LeanByExample/Tactic/RwSearch.lean b/LeanByExample/Reference/Tactic/RwSearch.lean similarity index 100% rename from LeanByExample/Tactic/RwSearch.lean rename to LeanByExample/Reference/Tactic/RwSearch.lean diff --git a/LeanByExample/Tactic/Says.lean b/LeanByExample/Reference/Tactic/Says.lean similarity index 100% rename from LeanByExample/Tactic/Says.lean rename to LeanByExample/Reference/Tactic/Says.lean diff --git a/LeanByExample/Tactic/SeqFocus.lean b/LeanByExample/Reference/Tactic/SeqFocus.lean similarity index 100% rename from LeanByExample/Tactic/SeqFocus.lean rename to LeanByExample/Reference/Tactic/SeqFocus.lean diff --git a/LeanByExample/Tactic/Set.lean b/LeanByExample/Reference/Tactic/Set.lean similarity index 100% rename from LeanByExample/Tactic/Set.lean rename to LeanByExample/Reference/Tactic/Set.lean diff --git a/LeanByExample/Tactic/Show.lean b/LeanByExample/Reference/Tactic/Show.lean similarity index 100% rename from LeanByExample/Tactic/Show.lean rename to LeanByExample/Reference/Tactic/Show.lean diff --git a/LeanByExample/Tactic/Simp.lean b/LeanByExample/Reference/Tactic/Simp.lean similarity index 100% rename from LeanByExample/Tactic/Simp.lean rename to LeanByExample/Reference/Tactic/Simp.lean diff --git a/LeanByExample/Tactic/SlimCheck.lean b/LeanByExample/Reference/Tactic/SlimCheck.lean similarity index 100% rename from LeanByExample/Tactic/SlimCheck.lean rename to LeanByExample/Reference/Tactic/SlimCheck.lean diff --git a/LeanByExample/Tactic/Sorry.lean b/LeanByExample/Reference/Tactic/Sorry.lean similarity index 100% rename from LeanByExample/Tactic/Sorry.lean rename to LeanByExample/Reference/Tactic/Sorry.lean diff --git a/LeanByExample/Tactic/Split.lean b/LeanByExample/Reference/Tactic/Split.lean similarity index 100% rename from LeanByExample/Tactic/Split.lean rename to LeanByExample/Reference/Tactic/Split.lean diff --git a/LeanByExample/Tactic/Suffices.lean b/LeanByExample/Reference/Tactic/Suffices.lean similarity index 100% rename from LeanByExample/Tactic/Suffices.lean rename to LeanByExample/Reference/Tactic/Suffices.lean diff --git a/LeanByExample/Tactic/Tauto.lean b/LeanByExample/Reference/Tactic/Tauto.lean similarity index 100% rename from LeanByExample/Tactic/Tauto.lean rename to LeanByExample/Reference/Tactic/Tauto.lean diff --git a/LeanByExample/Tactic/Trans.lean b/LeanByExample/Reference/Tactic/Trans.lean similarity index 100% rename from LeanByExample/Tactic/Trans.lean rename to LeanByExample/Reference/Tactic/Trans.lean diff --git a/LeanByExample/Tactic/Trivial.lean b/LeanByExample/Reference/Tactic/Trivial.lean similarity index 100% rename from LeanByExample/Tactic/Trivial.lean rename to LeanByExample/Reference/Tactic/Trivial.lean diff --git a/LeanByExample/Tactic/Try.lean b/LeanByExample/Reference/Tactic/Try.lean similarity index 100% rename from LeanByExample/Tactic/Try.lean rename to LeanByExample/Reference/Tactic/Try.lean diff --git a/LeanByExample/Tactic/Unfold.lean b/LeanByExample/Reference/Tactic/Unfold.lean similarity index 100% rename from LeanByExample/Tactic/Unfold.lean rename to LeanByExample/Reference/Tactic/Unfold.lean diff --git a/LeanByExample/Tactic/WithReducible.lean b/LeanByExample/Reference/Tactic/WithReducible.lean similarity index 100% rename from LeanByExample/Tactic/WithReducible.lean rename to LeanByExample/Reference/Tactic/WithReducible.lean diff --git a/LeanByExample/Tactic/Wlog.lean b/LeanByExample/Reference/Tactic/Wlog.lean similarity index 100% rename from LeanByExample/Tactic/Wlog.lean rename to LeanByExample/Reference/Tactic/Wlog.lean diff --git a/LeanByExample/Type/Char.lean b/LeanByExample/Reference/Type/Char.lean similarity index 100% rename from LeanByExample/Type/Char.lean rename to LeanByExample/Reference/Type/Char.lean diff --git a/LeanByExample/Type/Float.lean b/LeanByExample/Reference/Type/Float.lean similarity index 100% rename from LeanByExample/Type/Float.lean rename to LeanByExample/Reference/Type/Float.lean diff --git a/LeanByExample/Type/List.lean b/LeanByExample/Reference/Type/List.lean similarity index 100% rename from LeanByExample/Type/List.lean rename to LeanByExample/Reference/Type/List.lean diff --git a/LeanByExample/Type/Prop.lean b/LeanByExample/Reference/Type/Prop.lean similarity index 100% rename from LeanByExample/Type/Prop.lean rename to LeanByExample/Reference/Type/Prop.lean diff --git a/LeanByExample/Type/README.lean b/LeanByExample/Reference/Type/README.lean similarity index 100% rename from LeanByExample/Type/README.lean rename to LeanByExample/Reference/Type/README.lean diff --git a/LeanByExample/Type/String.lean b/LeanByExample/Reference/Type/String.lean similarity index 100% rename from LeanByExample/Type/String.lean rename to LeanByExample/Reference/Type/String.lean diff --git a/LeanByExample/Type/Type.lean b/LeanByExample/Reference/Type/Type.lean similarity index 100% rename from LeanByExample/Type/Type.lean rename to LeanByExample/Reference/Type/Type.lean diff --git a/LeanByExample/TypeClass/Coe.lean b/LeanByExample/Reference/TypeClass/Coe.lean similarity index 100% rename from LeanByExample/TypeClass/Coe.lean rename to LeanByExample/Reference/TypeClass/Coe.lean diff --git a/LeanByExample/TypeClass/CoeDep.lean b/LeanByExample/Reference/TypeClass/CoeDep.lean similarity index 100% rename from LeanByExample/TypeClass/CoeDep.lean rename to LeanByExample/Reference/TypeClass/CoeDep.lean diff --git a/LeanByExample/TypeClass/CoeFun.lean b/LeanByExample/Reference/TypeClass/CoeFun.lean similarity index 100% rename from LeanByExample/TypeClass/CoeFun.lean rename to LeanByExample/Reference/TypeClass/CoeFun.lean diff --git a/LeanByExample/TypeClass/CoeSort.lean b/LeanByExample/Reference/TypeClass/CoeSort.lean similarity index 100% rename from LeanByExample/TypeClass/CoeSort.lean rename to LeanByExample/Reference/TypeClass/CoeSort.lean diff --git a/LeanByExample/TypeClass/Decidable.lean b/LeanByExample/Reference/TypeClass/Decidable.lean similarity index 100% rename from LeanByExample/TypeClass/Decidable.lean rename to LeanByExample/Reference/TypeClass/Decidable.lean diff --git a/LeanByExample/TypeClass/GetElem.lean b/LeanByExample/Reference/TypeClass/GetElem.lean similarity index 100% rename from LeanByExample/TypeClass/GetElem.lean rename to LeanByExample/Reference/TypeClass/GetElem.lean diff --git a/LeanByExample/TypeClass/Inhabited.lean b/LeanByExample/Reference/TypeClass/Inhabited.lean similarity index 100% rename from LeanByExample/TypeClass/Inhabited.lean rename to LeanByExample/Reference/TypeClass/Inhabited.lean diff --git a/LeanByExample/TypeClass/OfNat.lean b/LeanByExample/Reference/TypeClass/OfNat.lean similarity index 100% rename from LeanByExample/TypeClass/OfNat.lean rename to LeanByExample/Reference/TypeClass/OfNat.lean diff --git a/LeanByExample/TypeClass/README.lean b/LeanByExample/Reference/TypeClass/README.lean similarity index 100% rename from LeanByExample/TypeClass/README.lean rename to LeanByExample/Reference/TypeClass/README.lean diff --git a/LeanByExample/TypeClass/Repr.lean b/LeanByExample/Reference/TypeClass/Repr.lean similarity index 100% rename from LeanByExample/TypeClass/Repr.lean rename to LeanByExample/Reference/TypeClass/Repr.lean diff --git a/LeanByExample/TypeClass/ToString.lean b/LeanByExample/Reference/TypeClass/ToString.lean similarity index 100% rename from LeanByExample/TypeClass/ToString.lean rename to LeanByExample/Reference/TypeClass/ToString.lean diff --git a/LeanByExample/Tutorial/Exercise/BarberParadox.lean b/LeanByExample/Tutorial/Exercise/BarberParadox.lean new file mode 100644 index 00000000..c49fe40f --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/BarberParadox.lean @@ -0,0 +1,39 @@ +/- # 床屋のパラドックス +集合論が提唱された当初、任意の述語 `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 new file mode 100644 index 00000000..9da84c22 --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/CantorPairing.lean @@ -0,0 +1,156 @@ +/- # 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 summ_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 new file mode 100644 index 00000000..4d1cf68f --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/CantorTheorem.lean @@ -0,0 +1,211 @@ +/- # 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 new file mode 100644 index 00000000..335e88a2 --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/DoubtImplication.lean @@ -0,0 +1,99 @@ +/- # 「ならば」の定義を疑う + +## イントロダクション + +論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「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 new file mode 100644 index 00000000..ddd8a3ad --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean @@ -0,0 +1,317 @@ +/- # 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 + +/-- 束 -/ +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`](../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 new file mode 100644 index 00000000..10990a4b --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean @@ -0,0 +1,76 @@ +/- # 全射・単射と左逆・右逆写像 + +関数 `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`](../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 new file mode 100644 index 00000000..a61ee639 --- /dev/null +++ b/LeanByExample/Tutorial/Exercise/KnightAndKnave.lean @@ -0,0 +1,155 @@ +/- # 騎士と悪党のパズル + +騎士(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/Solution/README.lean b/LeanByExample/Tutorial/Exercise/README.lean similarity index 91% rename from LeanByExample/Solution/README.lean rename to LeanByExample/Tutorial/Exercise/README.lean index 9f6608c7..674b4ba8 100644 --- a/LeanByExample/Solution/README.lean +++ b/LeanByExample/Tutorial/Exercise/README.lean @@ -7,7 +7,7 @@ 解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。 -Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`Exercise` ディレクトリの中にある該当ファイルを開いてください。 +Lean 4 Playground を使いたくない事情がある場合は、Codespace を開き、`LeanByExample/Tutorial/Exercise` ディレクトリの中にある該当ファイルを開いてください。 [![codespace badge](https://github.com/codespaces/badge.svg)](https://codespaces.new/lean-ja/lean-by-example) diff --git a/LeanByExample/Solution/BarberParadox.lean b/LeanByExample/Tutorial/Solution/BarberParadox.lean similarity index 100% rename from LeanByExample/Solution/BarberParadox.lean rename to LeanByExample/Tutorial/Solution/BarberParadox.lean diff --git a/LeanByExample/Solution/CantorPairing.lean b/LeanByExample/Tutorial/Solution/CantorPairing.lean similarity index 100% rename from LeanByExample/Solution/CantorPairing.lean rename to LeanByExample/Tutorial/Solution/CantorPairing.lean diff --git a/LeanByExample/Solution/CantorTheorem.lean b/LeanByExample/Tutorial/Solution/CantorTheorem.lean similarity index 100% rename from LeanByExample/Solution/CantorTheorem.lean rename to LeanByExample/Tutorial/Solution/CantorTheorem.lean diff --git a/LeanByExample/Solution/DoubtImplication.lean b/LeanByExample/Tutorial/Solution/DoubtImplication.lean similarity index 100% rename from LeanByExample/Solution/DoubtImplication.lean rename to LeanByExample/Tutorial/Solution/DoubtImplication.lean diff --git a/LeanByExample/Solution/HeytingAndBooleanAlgebra.lean b/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean similarity index 100% rename from LeanByExample/Solution/HeytingAndBooleanAlgebra.lean rename to LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean diff --git a/LeanByExample/Solution/InverseSurjInj.lean b/LeanByExample/Tutorial/Solution/InverseSurjInj.lean similarity index 100% rename from LeanByExample/Solution/InverseSurjInj.lean rename to LeanByExample/Tutorial/Solution/InverseSurjInj.lean diff --git a/LeanByExample/Solution/KnightAndKnave.lean b/LeanByExample/Tutorial/Solution/KnightAndKnave.lean similarity index 100% rename from LeanByExample/Solution/KnightAndKnave.lean rename to LeanByExample/Tutorial/Solution/KnightAndKnave.lean diff --git a/LeanByExample/Tutorial/Solution/README.lean b/LeanByExample/Tutorial/Solution/README.lean new file mode 100644 index 00000000..674b4ba8 --- /dev/null +++ b/LeanByExample/Tutorial/Solution/README.lean @@ -0,0 +1,19 @@ +/- # 演習問題 +このセクションでは、演習問題を扱います。ぜひ新しいパズルゲームだと思って挑戦してみてください。 + +## 🎮 遊び方 + +問題は、前提となるライブラリや知識が少なく、難易度が低いと思われる順に並べてあります。興味があるものから挑戦してみましょう。 + +解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。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) + +## ❓ どうしてもわからないとき + +時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 + +しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。 +-/ diff --git a/assets/filePlay.js b/assets/filePlay.js index 9ea657da..66e47a87 100644 --- a/assets/filePlay.js +++ b/assets/filePlay.js @@ -20,12 +20,6 @@ function filePlay() { "/LeanByExample/", ); - // 演習問題のファイルのみ、`LeanByExample` ディレクトリではなくて `Exercise` ディレクトリにある - editButtonLink.href = editButtonLink.href.replace( - "/LeanByExample/Exercise/", - "/Exercise/", - ); - // URL を書き換える fetch(editButtonLink.href) .then((response) => response.text()) diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index d4c89743..19e01cc6 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -6,182 +6,182 @@ --- -- [対話的コマンド](./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) - - [#instances: インスタンスを列挙](./Diagnostic/Instances.md) - - [#print: 中身を見る](./Diagnostic/Print.md) - - [#reduce: 式を簡約する](./Diagnostic/Reduce.md) - - [#synth: 型クラスの検査](./Diagnostic/Synth.md) - - [#time: 実行時間計測](./Diagnostic/Time.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) + - [#instances: インスタンスを列挙](./Reference/Diagnostic/Instances.md) + - [#print: 中身を見る](./Reference/Diagnostic/Print.md) + - [#reduce: 式を簡約する](./Reference/Diagnostic/Reduce.md) + - [#synth: 型クラスの検査](./Reference/Diagnostic/Synth.md) + - [#time: 実行時間計測](./Reference/Diagnostic/Time.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_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_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) - - [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) + - [match_pattern: 独自パタンマッチ](./Reference/Attribute/MatchPattern.md) + - [simps: simp 補題の自動生成](./Reference/Attribute/Simps.md) -- [オプション](./Option/README.md) - - [autoImplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) - - [hygiene: マクロ衛生](./Option/Hygiene.md) +- [オプション](./Reference/Option/README.md) + - [autoImplicit: 自動束縛暗黙引数](./Reference/Option/AutoImplicit.md) + - [hygiene: マクロ衛生](./Reference/Option/Hygiene.md) -- [型クラス](./TypeClass/README.md) - - [Coe: 型強制](./TypeClass/Coe.md) - - [CoeDep: 依存型強制](./TypeClass/CoeDep.md) - - [CoeFun: 関数型への強制](./TypeClass/CoeFun.md) - - [CoeSort: 型宇宙への強制](./TypeClass/CoeSort.md) - - [Decidable: 決定可能](./TypeClass/Decidable.md) - - [GetElem: n番目の要素を取得](./TypeClass/GetElem.md) - - [Inhabited: 有項にする](./TypeClass/Inhabited.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) + - [GetElem: n番目の要素を取得](./Reference/TypeClass/GetElem.md) + - [Inhabited: 有項にする](./Reference/TypeClass/Inhabited.md) + - [OfNat: 数値リテラルを使用](./Reference/TypeClass/OfNat.md) + - [Repr: 表示方法を指定](./Reference/TypeClass/Repr.md) + - [ToString: 文字列に変換](./Reference/TypeClass/ToString.md) -- [型](./Type/README.md) - - [Char: Unicode 文字](./Type/Char.md) - - [Float: 浮動小数点数](./Type/Float.md) - - [List: 連結リスト](./Type/List.md) - - [Prop: 命題全体](./Type/Prop.md) - - [String: 文字列](./Type/String.md) - - [Type: 型全体](./Type/Type.md) +- [型](./Reference/Type/README.md) + - [Char: Unicode 文字](./Reference/Type/Char.md) + - [Float: 浮動小数点数](./Reference/Type/Float.md) + - [List: 連結リスト](./Reference/Type/List.md) + - [Prop: 命題全体](./Reference/Type/Prop.md) + - [String: 文字列](./Reference/Type/String.md) + - [Type: 型全体](./Reference/Type/Type.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) - - [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: 単純化](./Tactic/Simp.md) - - [slim_check: 反例を見つける](./Tactic/SlimCheck.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) +- [タクティク](./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) + - [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: 単純化](./Reference/Tactic/Simp.md) + - [slim_check: 反例を見つける](./Reference/Tactic/SlimCheck.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) -- [演習問題](./Exercise/README.md) - - [床屋のパラドクス](./Exercise/BarberParadox.md) - - [騎士と悪党のパズル](./Exercise/KnightAndKnave.md) - - [「ならば」の定義を疑う](./Exercise/DoubtImplication.md) - - [全射・単射と左逆・右逆写像](./Exercise/InverseSurjInj.md) - - [Cantorの定理](./Exercise/CantorTheorem.md) - - [Cantorの対関数の全単射性](./Exercise/CantorPairing.md) - - [Heying代数とBool代数](./Exercise/HeytingAndBooleanAlgebra.md) +- [演習問題](./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) diff --git a/lakefile.lean b/lakefile.lean index 5174092f..a653994a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -24,7 +24,7 @@ require mathlib from git lean_lib LeanByExample where -- `lake build` の実行時にビルドされるファイルの設定 -- `.submodules` と指定すると、そのディレクトリ以下の全ての Lean ファイルがビルドされる - globs := #[.submodules `LeanByExample] + globs := #[.submodules `LeanByExample.Reference, .submodules `LeanByExample.Tutorial.Solution] section Script @@ -43,12 +43,6 @@ def runCmd (input : String) : IO Unit := do else if !out.stdout.isEmpty then IO.println out.stdout -/-- mk_exercise を実行し、演習問題の解答に -解答部分を sorry に置き換えるなどの処理を施して演習問題ファイルを生成する。-/ -script mk_exercise do - runCmd "lake exe mk_exercise LeanByExample/Solution Exercise" - return 0 - syntax (name := with_time) "with_time" "running" str doElem : doElem macro_rules @@ -63,13 +57,11 @@ Lean ファイルから Markdown ファイルと HTML ファイルを生成す `.\scripts\Build.ps1` を実行したほうが高速 -/ script build do - -- `lake run mk_exercise` を使用すると遅くなってしまうのでコピペしている with_time running "mk_exercise" - runCmd "lake exe mk_exercise LeanByExample/Solution Exercise" + runCmd "lake exe mk_exercise LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise" with_time running "mdgen" - runCmd "lake exe mdgen LeanByExample booksrc"; - runCmd "lake exe mdgen Exercise booksrc/Exercise" + runCmd "lake exe mdgen LeanByExample booksrc" with_time running "mdbook" runCmd "mdbook build" diff --git a/scripts/Build.ps1 b/scripts/Build.ps1 index ce47618a..ce00b8c1 100644 --- a/scripts/Build.ps1 +++ b/scripts/Build.ps1 @@ -3,9 +3,8 @@ lake を介することで実行が遅くなってしまうので、 lake を介することなく実行ファイルを直接叩く。 #> -./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe LeanByExample/Solution Exercise +./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe LeanByExample/Tutorial/Solution LeanByExample/Tutorial/Exercise -./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Exercise booksrc/Exercise ./.lake/packages/mdgen/.lake/build/bin/mdgen.exe LeanByExample booksrc mdbook build From 2e4285fb21de0664058ff49206156dfb5fa2b989 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 07:26:29 +0900 Subject: [PATCH 2/7] =?UTF-8?q?=E4=B8=8D=E8=A6=81=E3=81=AB=E3=81=AA?= =?UTF-8?q?=E3=81=A3=E3=81=9F=20Exercise=20=E3=83=87=E3=82=A3=E3=83=AC?= =?UTF-8?q?=E3=82=AF=E3=83=88=E3=83=AA=E3=82=92=E6=B6=88=E3=81=99?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Exercise/BarberParadox.lean | 39 --- Exercise/CantorPairing.lean | 156 ------------ Exercise/CantorTheorem.lean | 211 ---------------- Exercise/DoubtImplication.lean | 99 -------- Exercise/HeytingAndBooleanAlgebra.lean | 317 ------------------------- Exercise/InverseSurjInj.lean | 76 ------ Exercise/KnightAndKnave.lean | 155 ------------ Exercise/README.lean | 19 -- 8 files changed, 1072 deletions(-) delete mode 100644 Exercise/BarberParadox.lean delete mode 100644 Exercise/CantorPairing.lean delete mode 100644 Exercise/CantorTheorem.lean delete mode 100644 Exercise/DoubtImplication.lean delete mode 100644 Exercise/HeytingAndBooleanAlgebra.lean delete mode 100644 Exercise/InverseSurjInj.lean delete mode 100644 Exercise/KnightAndKnave.lean delete mode 100644 Exercise/README.lean diff --git a/Exercise/BarberParadox.lean b/Exercise/BarberParadox.lean deleted file mode 100644 index c49fe40f..00000000 --- a/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/Exercise/CantorPairing.lean b/Exercise/CantorPairing.lean deleted file mode 100644 index 9da84c22..00000000 --- a/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 summ_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/Exercise/CantorTheorem.lean b/Exercise/CantorTheorem.lean deleted file mode 100644 index 4d1cf68f..00000000 --- a/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/Exercise/DoubtImplication.lean b/Exercise/DoubtImplication.lean deleted file mode 100644 index 335e88a2..00000000 --- a/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/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean deleted file mode 100644 index ddd8a3ad..00000000 --- a/Exercise/HeytingAndBooleanAlgebra.lean +++ /dev/null @@ -1,317 +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 - -/-- 束 -/ -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`](../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/Exercise/InverseSurjInj.lean b/Exercise/InverseSurjInj.lean deleted file mode 100644 index 10990a4b..00000000 --- a/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`](../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/Exercise/KnightAndKnave.lean b/Exercise/KnightAndKnave.lean deleted file mode 100644 index a61ee639..00000000 --- a/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/Exercise/README.lean b/Exercise/README.lean deleted file mode 100644 index 674b4ba8..00000000 --- a/Exercise/README.lean +++ /dev/null @@ -1,19 +0,0 @@ -/- # 演習問題 -このセクションでは、演習問題を扱います。ぜひ新しいパズルゲームだと思って挑戦してみてください。 - -## 🎮 遊び方 - -問題は、前提となるライブラリや知識が少なく、難易度が低いと思われる順に並べてあります。興味があるものから挑戦してみましょう。 - -解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。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) - -## ❓ どうしてもわからないとき - -時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 - -しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。 --/ From 90aa598bac90df3cb24519bd9af252c2363835ee Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 07:38:05 +0900 Subject: [PATCH 3/7] =?UTF-8?q?=E7=9B=AE=E6=AC=A1=E3=81=AE=E7=B7=A8?= =?UTF-8?q?=E9=9B=86?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- booksrc/SUMMARY.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 19e01cc6..47b3721f 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -6,6 +6,8 @@ --- +# 第1部: リファレンス + - [対話的コマンド](./Reference/Diagnostic/README.md) - [#check_failure: 意図的なエラー](./Reference/Diagnostic/CheckFailure.md) - [#check: 型を調べる](./Reference/Diagnostic/Check.md) @@ -177,6 +179,8 @@ - [with_reducible: 透過度指定](./Reference/Tactic/WithReducible.md) - [wlog: 一般性を失わずに特殊化](./Reference/Tactic/Wlog.md) +# 第2部: チュートリアル + - [演習問題](./Tutorial/Exercise/README.md) - [床屋のパラドクス](./Tutorial/Exercise/BarberParadox.md) - [騎士と悪党のパズル](./Tutorial/Exercise/KnightAndKnave.md) From 43ced5a542e76a501a6c3250d781edf34db66848 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 22:18:33 +0900 Subject: [PATCH 4/7] =?UTF-8?q?=E3=83=AA=E3=83=B3=E3=82=AF=E3=81=AE?= =?UTF-8?q?=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Tutorial/Exercise/README.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanByExample/Tutorial/Exercise/README.lean b/LeanByExample/Tutorial/Exercise/README.lean index 674b4ba8..66443f92 100644 --- a/LeanByExample/Tutorial/Exercise/README.lean +++ b/LeanByExample/Tutorial/Exercise/README.lean @@ -15,5 +15,5 @@ Lean 4 Playground を使いたくない事情がある場合は、Codespace を 時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 -しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。 +しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。 -/ From 2a63f0aa98388775435e7f296852a68e52bcfdcb Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 22:21:30 +0900 Subject: [PATCH 5/7] =?UTF-8?q?mdgen=20=E3=81=AE=E6=9B=B4=E6=96=B0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Tutorial/Exercise/README.lean | 2 +- lake-manifest.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Tutorial/Exercise/README.lean b/LeanByExample/Tutorial/Exercise/README.lean index 66443f92..674b4ba8 100644 --- a/LeanByExample/Tutorial/Exercise/README.lean +++ b/LeanByExample/Tutorial/Exercise/README.lean @@ -15,5 +15,5 @@ Lean 4 Playground を使いたくない事情がある場合は、Codespace を 時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 -しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。 +しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。 -/ diff --git a/lake-manifest.json b/lake-manifest.json index b14bce9b..1d02f672 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d07724c3f70b6df81b49535095a35151c4a5e42c", + "rev": "ea278cb4a948c563cd9cda7068290fcaa6d240db", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", From 8ff34a0291c15237bb0d6a66fdc9f3810aec62cd Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 22:42:35 +0900 Subject: [PATCH 6/7] =?UTF-8?q?=E3=83=AA=E3=83=B3=E3=82=AF=E5=88=87?= =?UTF-8?q?=E3=82=8C=E3=81=AE=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean | 2 +- LeanByExample/Tutorial/Exercise/InverseSurjInj.lean | 2 +- LeanByExample/Tutorial/Exercise/README.lean | 2 +- LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean | 2 +- LeanByExample/Tutorial/Solution/InverseSurjInj.lean | 2 +- LeanByExample/Tutorial/Solution/README.lean | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean b/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean index ddd8a3ad..1192ceca 100644 --- a/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean +++ b/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean @@ -136,7 +136,7 @@ end HeytingAlgebra しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。 -こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Declarative/AddAesopRules.md) の記事が参考になると思います。 +こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) の記事が参考になると思います。 ### 問1.1 半順序集合であること -/ diff --git a/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean b/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean index 10990a4b..60da256b 100644 --- a/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean +++ b/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean @@ -17,7 +17,7 @@ def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a /- 一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。 -しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。 +しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](#{root}/Reference/Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。 ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。 -/ diff --git a/LeanByExample/Tutorial/Exercise/README.lean b/LeanByExample/Tutorial/Exercise/README.lean index 674b4ba8..66443f92 100644 --- a/LeanByExample/Tutorial/Exercise/README.lean +++ b/LeanByExample/Tutorial/Exercise/README.lean @@ -15,5 +15,5 @@ Lean 4 Playground を使いたくない事情がある場合は、Codespace を 時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 -しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。 +しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。 -/ diff --git a/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean b/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean index 14185bc7..9fba5e4f 100644 --- a/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean +++ b/LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean @@ -136,7 +136,7 @@ end HeytingAlgebra しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。 -こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Declarative/AddAesopRules.md) の記事が参考になると思います。 +こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) の記事が参考になると思います。 ### 問1.1 半順序集合であること -/ diff --git a/LeanByExample/Tutorial/Solution/InverseSurjInj.lean b/LeanByExample/Tutorial/Solution/InverseSurjInj.lean index dd639a68..95d1b33f 100644 --- a/LeanByExample/Tutorial/Solution/InverseSurjInj.lean +++ b/LeanByExample/Tutorial/Solution/InverseSurjInj.lean @@ -17,7 +17,7 @@ def Function.Injective (f : A → B) : Prop := ∀ {a₁ a₂ : A}, f a₁ = f a /- 一見すると、全射と単射はペアになる概念とは思えないかもしれません。束縛変数の数も違いますし、意味上もまったく独立した概念のように見えます。 -しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。 +しかし、`A` が空でないと仮定すれば、選択原理 [`Classical.choice`](#{root}/Reference/Declarative/Axiom.md#ClassicalChoice) を使うことによって、全射 `f : A → B` があれば逆方向の単射 `g : B → A` が構成でき、逆に単射 `f : A → B` があれば逆方向の全射 `g : B → A` を構成することができます。 ある意味で、全射と単射はペアをなす概念であると言えるかもしれないですね。今回の演習問題のテーマはこの定理です。 -/ diff --git a/LeanByExample/Tutorial/Solution/README.lean b/LeanByExample/Tutorial/Solution/README.lean index 674b4ba8..66443f92 100644 --- a/LeanByExample/Tutorial/Solution/README.lean +++ b/LeanByExample/Tutorial/Solution/README.lean @@ -15,5 +15,5 @@ Lean 4 Playground を使いたくない事情がある場合は、Codespace を 時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。 -しかし、自力で解いた後に解答を見るのは構いません。解答は [`Examples/Solution`](https://github.com/lean-ja/lean-by-example/tree/main/Examples/Solution) ディレクトリに置いてあります。 +しかし、自力で解いた後に解答を見るのは構いません。解答は `LeanByExample/Tutorial/Solution` ディレクトリに置いてあります。 -/ From 4dc783b5dff864c50e4af7401a6401cc53902259 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 22:46:25 +0900 Subject: [PATCH 7/7] =?UTF-8?q?=E3=83=93=E3=83=AB=E3=83=89=E3=81=8C?= =?UTF-8?q?=E9=80=9A=E3=82=89=E3=81=AA=E3=81=84=E5=95=8F=E9=A1=8C=E3=82=92?= =?UTF-8?q?=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Declarative/Private.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanByExample/Reference/Declarative/Private.lean b/LeanByExample/Reference/Declarative/Private.lean index ad1a627f..9b5a5d07 100644 --- a/LeanByExample/Reference/Declarative/Private.lean +++ b/LeanByExample/Reference/Declarative/Private.lean @@ -3,7 +3,7 @@ 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。 -/ -import Examples.Declarative.Protected -- protected のページをインポート +import LeanByExample.Reference.Declarative.Protected -- protected のページをインポート import Lean namespace Private --#