Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

証明無関係の説明に誤り #576

Merged
merged 1 commit into from
Aug 5, 2024
Merged

証明無関係の説明に誤り #576

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Examples/Term/Type/Prop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,15 @@ theorem proof_irrel (P : Prop) (h1 h2 : P) : h1 = h2 := rfl
/-- info: 'Proposition.proof_irrel' does not depend on any axioms -/
#guard_msgs in #print axioms proof_irrel

/- 証明無関係の重要な帰結のひとつに、「命題から値を取り出すことができるのは、証明の中だけ」というものがあります。たとえば次のように、証明の中であれば命題を [`cases`](../../Tactic/Cases.md) や [`rcases`](../../Tactic/Rcases.md) で分解して値を取り出すことができます。-/
/- 証明無関係の重要な帰結のひとつに、「証明から値を取り出すことができるのは、証明の中だけ」というものがあります。たとえば次のように、証明の中であれば証明項を [`cases`](../../Tactic/Cases.md) や [`rcases`](../../Tactic/Rcases.md) で分解して値を取り出すことができます。-/

-- 同じ存在命題の２通りの証明
-- 2乗すると1になる整数を２通り与えた
theorem foo : ∃ x : Int, x ^ 2 = 1 := by exists 1
theorem bar : ∃ x : Int, x ^ 2 = 1 := by exists -1

def Ok.extract (h : ∃ x : Int, x ^ 2 = 1) : True := by
-- 仮定にある存在命題 `h` を分解して
-- 仮定にある証明項 `h` を分解して
-- x を取り出すことができる
rcases h with ⟨_x, _hx⟩

Expand Down