lean-ja / lean-ja/lean-by-example
inudctionOn は refine で使った方がよさそう
Open
Nobody has claimed this yet.
コード例
タクティク
データ型
- Dominant language
- Lean
- Stars
- 188
- Forks
- 15
- Avg merge
- 9h 8m
- Merged PRs (30d)
- 6
Description
theorem MyInt.add_assoc (m n k : MyInt) : m + n + k = m + (n + k) := by
-- 定義を展開して自然数の式に帰着させる
refine Quotient.inductionOn₃ m n k ?_
intro (a₁, a₂) (b₁, b₂) (c₁, c₂)
apply Quot.sound
dsimp [Setoid.r, PreInt.r]
ac_rfl
theorem MyInt.add_comm (m n : MyInt) : m + n = n + m := by
-- 定義を展開して自然数の式に帰着させる
refine Quotient.inductionOn₂ m n ?_
intro (a₁, a₂) (b₁, b₂)
apply Quot.sound
dsimp [Setoid.r, PreInt.r]
ac_rfl
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Search the repository for the MyInt.add_assoc and MyInt.add_comm examples shown in this issue, then inspect the surrounding Lean documentation. Update the inductionOn examples to use the refine-based forms illustrated here and verify that the examples still typecheck.
Written by the indexing model from the issue text.
Assessment
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100