Email Gateway (Aug 18 2022 at 12:03): Email Gateway (Aug 18 2022 at 12:03):From: Glauber Cabral <glauber.sp@gmail.com>
Hi everybody.
I'm using Isabelle to prove HasCASL specifications and I'm still learning
how to use both "technologies" to my master thesis. Sorry if this question
is too newbie, but I couldn't find any solution by myself.
I've been writing proofs only with apply (method) because Isabelle is not
the main focus right now and I thought it should be enough at this moment to
write proofs this way.
The problem is that I could not find any example or explanation about how to
use contradiction method. When I use it, I got 2 goals: P x y and not P x y,
and I couldn't find how to make Isabelle relates P with a function I've
already created. Can anyone tell me where do I found any explanation or
example to understand how it works?
I'd like to ask something else that I'm not sure. If I escape a proof of a
theorem/lemma with oops, I cannot use this thm/lemma in the next proofs,
right?Just to be sure, although I know using this without proving it would
not make sense...
Thanks in advance,
Glauber Cabral
Email Gateway (Aug 18 2022 at 12:04):From: Amine Chaieb <chaieb@in.tum.de>
Glauber Cabral wrote:
Yes. If you want to use the fact, although unproven, you can use the
"sorry" method, which proves anything.
Amine.
Email Gateway (Aug 18 2022 at 12:04):From: Lawrence Paulson <lp15@cam.ac.uk>
You will find it much easier if you read the examples in the Tutorial
rather than just trying out all the different methods. The
contradiction method is not used very often.
Larry Paulson
Email Gateway (Aug 18 2022 at 12:04):From: Lawrence Paulson <lp15@cam.ac.uk>
If you wish to prove a theorem by contradiction, the usual approach is
to begin with the following line:
apply (rule ccontr)
Its effect should be self explanatory.
Larry Paulson
Email Gateway (Aug 18 2022 at 12:04):From: Amine Chaieb <chaieb@in.tum.de>
You will find that the following "scheme" also works for Isar proofs:
proof-
{assume "~P"
have False <proof>}
then show ?thesis by metis/blast/simp
qed
Lawrence Paulson wrote:
Email Gateway (Aug 18 2022 at 12:04):From: Glauber Cabral <glauber.sp@gmail.com>
Dear Lawrence.
I've already read the Isabelle tutorial. This method is not explained there
(as, you've told, it's not used often). And I've found only how to
instantiate variables in a theorem, usin *rule_tac methods.
I wanted to use contradiction method because proof by contradiction was the
only way I found to prove Assymetry of Strict total order using only
Irreflexivity and Transitivity axioms.
Thanks,
Glauber
Email Gateway (Aug 18 2022 at 12:05):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Glauber Cabral <glauber.sp@gmail.com>:
The "contradiction" method simply applies the not-elimination rule, notE:
lemma notE: "[| ~P; P |] ==> R"
Note that unlike most lemmas, the conclusion is totally unrelated to
the assumptions. If you write "apply contradiction" in an apply-style
proof, Isabelle matches "R" against your current subgoal, but "P" is
still totally unconstrained, so your new subgoals will have schematic
variables (usually shown with question marks, like "?P"). In your
case, the "?P" schematic variable is parametrized over x and y because
your subgoal is universally quantified over those variables, and ?P is
allowed to depend on them.
Schematic variables can be instantiated at any time by matching them
with other rules or assumptions. For example, if you have a subgoal
that looks like "~ foo ==> ~ ?P", you can discharge it by typing
"apply assumption" which will instantiate ?P to foo. All occurrences
of ?P in other subgoals will then be replaced by foo.
Schematic variables can be awkward to deal with in apply-style proofs.
Instead of "apply contradiction", you might prefer to explicitly
instantiate P using rule_tac, e.g. "apply (rule_tac P="foo" in notE)".
Alternatively, the "contradiction" method is more useful in Isar-style proofs:
lemma
fixes x y :: nat
assumes A: "x < y" and B: "y < x"
shows "False"
proof (contradiction)
show "x < x"
using A B by (rule less_trans)
show "¬ x < x"
by (rule less_not_refl)
qed
lemma
fixes x y :: nat
assumes A: "x < y" and B: "y < x"
shows "False"
proof -
have 1: "x < x"
using A B by (rule less_trans)
have 2: "¬ x < x"
by (rule less_not_refl)
from 1 2 show "False"
by contradiction
qed
Hope this helps,
Email Gateway (Aug 18 2022 at 12:05):From: Glauber Cabral <glauber.sp@gmail.com>
Hi Brian.
Thank you for this explanation. It helped me me to understand how
contradiction works. I've already tried to instantiate P with *rule_tac
methods, but I guess I did some mistake and that didn't work.
The ccontr worked for me, as it was told in the list.
Best regards,
Glauber
Last updated: May 03 2024 at 12:27 UTC