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/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 93% rename from LeanByExample/Declarative/Private.lean rename to LeanByExample/Reference/Declarative/Private.lean index ad1a627f..9b5a5d07 100644 --- a/LeanByExample/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 --# 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/Exercise/BarberParadox.lean b/LeanByExample/Tutorial/Exercise/BarberParadox.lean similarity index 100% rename from Exercise/BarberParadox.lean rename to LeanByExample/Tutorial/Exercise/BarberParadox.lean diff --git a/Exercise/CantorPairing.lean b/LeanByExample/Tutorial/Exercise/CantorPairing.lean similarity index 100% rename from Exercise/CantorPairing.lean rename to LeanByExample/Tutorial/Exercise/CantorPairing.lean diff --git a/Exercise/CantorTheorem.lean b/LeanByExample/Tutorial/Exercise/CantorTheorem.lean similarity index 100% rename from Exercise/CantorTheorem.lean rename to LeanByExample/Tutorial/Exercise/CantorTheorem.lean diff --git a/Exercise/DoubtImplication.lean b/LeanByExample/Tutorial/Exercise/DoubtImplication.lean similarity index 100% rename from Exercise/DoubtImplication.lean rename to LeanByExample/Tutorial/Exercise/DoubtImplication.lean diff --git a/Exercise/HeytingAndBooleanAlgebra.lean b/LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean similarity index 98% rename from Exercise/HeytingAndBooleanAlgebra.lean rename to LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean index ddd8a3ad..1192ceca 100644 --- a/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/Exercise/InverseSurjInj.lean b/LeanByExample/Tutorial/Exercise/InverseSurjInj.lean similarity index 92% rename from Exercise/InverseSurjInj.lean rename to LeanByExample/Tutorial/Exercise/InverseSurjInj.lean index 10990a4b..60da256b 100644 --- a/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/Exercise/KnightAndKnave.lean b/LeanByExample/Tutorial/Exercise/KnightAndKnave.lean similarity index 100% rename from Exercise/KnightAndKnave.lean rename to LeanByExample/Tutorial/Exercise/KnightAndKnave.lean diff --git a/LeanByExample/Solution/README.lean b/LeanByExample/Tutorial/Exercise/README.lean similarity index 83% rename from LeanByExample/Solution/README.lean rename to LeanByExample/Tutorial/Exercise/README.lean index 9f6608c7..66443f92 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) @@ -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/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 98% rename from LeanByExample/Solution/HeytingAndBooleanAlgebra.lean rename to LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean index 14185bc7..9fba5e4f 100644 --- a/LeanByExample/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/Solution/InverseSurjInj.lean b/LeanByExample/Tutorial/Solution/InverseSurjInj.lean similarity index 94% rename from LeanByExample/Solution/InverseSurjInj.lean rename to LeanByExample/Tutorial/Solution/InverseSurjInj.lean index dd639a68..95d1b33f 100644 --- a/LeanByExample/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/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/Exercise/README.lean b/LeanByExample/Tutorial/Solution/README.lean similarity index 83% rename from Exercise/README.lean rename to LeanByExample/Tutorial/Solution/README.lean index 9f6608c7..66443f92 100644 --- a/Exercise/README.lean +++ b/LeanByExample/Tutorial/Solution/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) @@ -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/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..47b3721f 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -6,182 +6,186 @@ --- -- [対話的コマンド](./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) +# 第1部: リファレンス -- [宣言的コマンド](./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/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) -- [属性](./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/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) -- [オプション](./Option/README.md) - - [autoImplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) - - [hygiene: マクロ衛生](./Option/Hygiene.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) -- [型クラス](./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/Option/README.md) + - [autoImplicit: 自動束縛暗黙引数](./Reference/Option/AutoImplicit.md) + - [hygiene: マクロ衛生](./Reference/Option/Hygiene.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/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) -- [タクティク](./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/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) -- [演習問題](./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) +- [タクティク](./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) + +# 第2部: チュートリアル + +- [演習問題](./Tutorial/Exercise/README.md) + - [床屋のパラドクス](./Tutorial/Exercise/BarberParadox.md) + - [騎士と悪党のパズル](./Tutorial/Exercise/KnightAndKnave.md) + - [「ならば」の定義を疑う](./Tutorial/Exercise/DoubtImplication.md) + - [全射・単射と左逆・右逆写像](./Tutorial/Exercise/InverseSurjInj.md) + - [Cantorの定理](./Tutorial/Exercise/CantorTheorem.md) + - [Cantorの対関数の全単射性](./Tutorial/Exercise/CantorPairing.md) + - [Heying代数とBool代数](./Tutorial/Exercise/HeytingAndBooleanAlgebra.md) 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", 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