Gergely Buday (Jul 26 2023 at 14:40): Gergely Buday (Jul 26 2023 at 14:40):I am trying to prove double negation with implication elimination and introduction:
lemma "A ⟶ ¬¬A"
proof -
assume a: A
assume anot: "A ⟶ False"
from anot a have False by (rule HOL.mp)
from this have anotnot: "(A ⟶ False) ⟶ False" by (rule impI)
have anotnot_def: "(A ⟶ False) ⟶ False ≡ ¬¬A" unfolding not_def .
from anotnot have "¬¬A" unfolding anotnot_def .
from this have ?thesis by (rule impI)
It seems that I am almost done but of course "almost" might be far from the solution.
I get the following proof state:
have A ⟶ ¬ ¬ A
proof (state)
this:
A ⟶ ¬ ¬ A
goal (1 subgoal):
1. A ⟶ ¬ ¬ A
Why am I not getting finished here? When I try to have show insted of have in the last line, I get
proof (chain)
picking this:
¬ ¬ A
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(A) ⟹ (A ⟶ False) ⟹ A ⟶ ¬ ¬ A
showing my two assumptions. Do you have an explanation?
Gergely Buday (Jul 26 2023 at 15:03):ChatGPT came up with a simpler one. After some cosmetic changes, it became
lemma double_negation_intro: "P ⟶ ¬¬P"
proof (rule impI)
assume "P"
show "¬¬P"
proof (rule notI)
assume "¬P"
with ‹P› show False by contradiction
qed
qed
Take the cursor and move it to the first proof -
Mathias Fleury (Jul 26 2023 at 15:09):Then look at the state panel
Mathias Fleury (Jul 26 2023 at 15:09):look at the goal
Mathias Fleury (Jul 26 2023 at 15:09):really look at the goal
Mathias Fleury (Jul 26 2023 at 15:10):and remember that assume introduces assumptions with ⟹
Last updated: Dec 21 2024 at 16:20 UTC