Email Gateway (Aug 23 2022 at 08:24): Email Gateway (Aug 23 2022 at 08:24):From: "John F. Hughes" <jfh@cs.brown.edu>
Suppose I want to prove something like "in a group where the order of every
element divides 3, there's an involution with only the identity element as
a fixed point". As a mathematician, I just say "Consider the involution x
-> x^2; that'll all you need!"
Similarly, if I want to prove that there are three distinct natural numbers
whose product is 12, I say "Well, 1 * 2 * 6 = 12" (or perhaps I use 1 * 3
Is there an idiomatic way to do such a proof in isabelle, i.e., to fill in
lemma tiny: "∃ (k::nat) (m::nat) (p::nat) . kmp = 12 ∧ k ≠ m ∧ k ≠ p ∧ m
≠ p"
proof -
???
[I should probably mention that Sledgehammer claims to have a proof, but
I'm not -- as you might have guessed! -- interested in this particular
fact, but rather in how to say to Isabelle, "Look! It's right here!" ]
The proof suggested is "(metis (no_types, lifting) add_right_imp_eq
numeral_Bit0 numeral_Bit1 one_eq_numeral_iff semiring_norm(83)
semiring_norm(86) semiring_normalization_rules(25)
semiring_normalization_rules(4)) (671 ms)" which hardly gives me an idiom
for such proofs.
--John
Email Gateway (Aug 23 2022 at 08:24):From: Mark Wassell <mpwassell@gmail.com>
Hi,
I can provide a few ways of doing this. The key to all of them is to
replace the dash following 'proof' with a proof method.
First, if you give the proof method rule+ then Isabelle will pick
appropriate rule automatically [1] and do this multiple times. Here the
rule it applies is exI which will unpack the existentials. This will then
leave you with 2 things to prove.
You can plug anything you like into the ? variables and so the proof is:
lemma tiny: "∃ (k::nat) (m::nat) (p::nat) . kmp = 12 ∧ k ≠ m ∧ k ≠ p ∧ m
≠ p"
proof(rule+)
show "1 * (2::nat) * 6 = 12" by simp
show "1 ≠ (2::nat) ∧ 1 ≠ (6::nat) ∧ 2 ≠ (6::nat)" by simp
qed
The fly in the ointment is that you have to add the type annotations to the
numeric constants as these are overloaded constants. I don't know if there
is a nice way to tell Isabelle that you want fix all numeric constants to
be nats within your proof or a part of your theory.
The second is a variant of the above but here you specify the actual
constant for each application of exI. This will give you the one line proof
of:
by(rule exI[where x=1],rule exI[where x=2], rule exI[where x=6], simp+)
It's interesting here that I didn't need to include the type annotation.
Also it would be nice if Isabelle was able to let you specify that you want
exI to be mapped over a list of literals [1,2,6]. One way to get around
this for your case is to include:
lemma exI3: "P x y z ⟹ ∃x y z. P x y z" by auto
and then you can do
by(rule exI3[of _ 1 2 6],auto)
Cheers
Mark
[1] Isar Reference Manual - page 6.4.2
Email Gateway (Aug 23 2022 at 08:24):From: Lawrence Paulson <lp15@cam.ac.uk>
I prefer this style when there are existential quantifiers to instantiate:
lemma tiny: "∃ (k::nat) (m::nat) (p::nat) . kmp = 12 ∧ k ≠ m ∧ k ≠ p ∧ m ≠ p"
proof -
have "1 * 3 * 4 = (12::nat)"
by auto
then show ?thesis
using numeral_eq_iff one_eq_numeral_iff by blast
qed
Larry Paulson
Email Gateway (Aug 23 2022 at 08:24):From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks to one and all for these useful approaches. I've used Larry's and it
got me where I needed to go, and pretty readably. :)
Email Gateway (Aug 23 2022 at 08:25):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 9/2/20 a las 05:15, Mark Wassell escribió:
Hello,
I have some related question, especially concerning the "plug anything"
part.
Sometimes I have to prove a result like
"∃x. P x ∧ Q x",
and I intend to use a lemma that states
lemma A: "∃x. R x".
Moreover, I know that any such x (satisfying R) will work for me. Also,
it turns out that in my example it is better to prove "P x" first and
then use this to prove "Q x".
I would like to be able to write a proof that looks like this:
lemma "∃x. P x ∧ Q x"proof (rule) (* goals here: P ?x &&& Q ?x *) obtain
x where "R x" using A by blast then show "P x" <proof> then show "Q x"
<proof> qed
This won't work (neither of the show commands) because I have an
obtained parameter in the conclusion. Nevertheless it looks like a sound
proof method, because I'm proving an existential.
I know this kind of a "feature request"; I wanted to know if there is
some way to write proofs like this, or if someone actually considered
this might be useful.
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Email Gateway (Aug 23 2022 at 08:25):From: Frédéric Boulanger <frederic.boulanger@lri.fr>
What about this:
lemma ‹∃k m p. kmp = (12::nat) ∧ k≠m ∧ k≠p ∧ m≠p›
proof -
have ‹134 = (12::nat)› by simp
moreover have ‹1≠(3::nat)› by simp
moreover have ‹1≠(4::nat)› by simp
moreover have ‹3≠(4::nat)› by simp
ultimately show ?thesis by blast
qed
or even shorter:
lemma ‹∃k m p. kmp = (12::nat) ∧ k≠m ∧ k≠p ∧ m≠p›
proof -
have ‹134 = (12::nat)› by simp
moreover have ‹1≠(3::nat) ∧ 1≠(4::nat) ∧ 3≠(4::nat)› by simp
ultimately show ?thesis by blast
qed
Some similar proof patterns are given in section 4.2.1 (page 45) of Programming and proving in Isabelle/HOL.
Frédéric
Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire de Recherche en Informatique
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât 650 Ada Lovelace, Université Paris Sud, 91405 Orsay Cedex France
+33 [0]1 69 85 14 84
Email Gateway (Aug 23 2022 at 08:25):From: Lawrence Paulson <lp15@cam.ac.uk>
You seem to be saying that you know that R(x) implies P(x) and that P(x) implies Q(x), in both cases for all x. Prove those two implications, and if you have also proved "∃x. R x", then "∃x. P x ∧ Q x" should be provable automatically provided P, Q and R aren't too complicated. And if they are, you could introduce abbreviations for them.
Larry Paulson
Email Gateway (Aug 23 2022 at 08:25):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 10/2/20 a las 08:18, Lawrence Paulson escribió:
Thank you very much; I understand this technique. The way I thought
about this was to introduce the existential at the very end:
lemma
assumes "∃x. R x"
shows "∃x. P x ∧ Q x"
proof -
obtain x where "R x" using A by blast
then
have "P x" <proof>
moreover from this
have "Q x" <proof>
ultimately
show ?thesis by auto (* or something *)
qed
The reason I asked is that the implication P(x)==>Q(x) usually depends
on too much information local to the lemma, and putting that in a
separate result would sometimes obfuscate the proof document. Also, when
the overall argument has some length, the cumulative approach
"moreover... ultimately" also seems impractical. Alternatively, I could
label the relevant facts and use them afterwards, but I want to avoid
cross-referencing and repetition as much as possible.
Thanks again.
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Email Gateway (Aug 23 2022 at 08:26):From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Hello,
Thank you very much; I understand this technique. The way I thought
about this was to introduce the existential at the very end:
it doesn't have to be very end, but after the relevant "obtain". This
might look better:
lemma
shows "∃x::'a. P x ∧ Q x"
proof -
obtain x ::'a where x: "R x" sorry
show ?thesis
proof (intro exI conjI)
show "P x" using x sorry
show "Q x" using x sorry
qed
qed
Best,
Akihisa
lemma
assumes "∃x. R x"
shows "∃x. P x ∧ Q x"
proof -
obtain x where "R x" using A by blast
then
have "P x" <proof>
moreover from this
have "Q x" <proof>
ultimately
show ?thesis by auto (* or something *)
qedThe reason I asked is that the implication P(x)==>Q(x) usually depends
on too much information local to the lemma, and putting that in a
separate result would sometimes obfuscate the proof document. Also, when
the overall argument has some length, the cumulative approach
"moreover... ultimately" also seems impractical. Alternatively, I could
label the relevant facts and use them afterwards, but I want to avoid
cross-referencing and repetition as much as possible.Thanks again.
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Last updated: Nov 21 2024 at 12:39 UTC