Email Gateway (Aug 18 2022 at 09:42): Email Gateway (Aug 18 2022 at 09:42):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello,
I'm trying to write some simple proofs and in particular I want to
demonstrate the follow
ALL (a::nat) (b::nat). a>0 AND b>0 --> EXISTS c d. ad<bc
but I don't find the correct way.
I fixed 'a' and 'b' and assumed 'a>0' and 'b>0 ', now I want demonstrate the
EXISTS formulae showing that a possible instantiation of 'c' and 'd' is
respectively (a+1) and 1.
In each my effort I reach the error
empty result sequence -- proof command failed
and I don't know how resolve it.
This is my proof sketch:
lemma
fixes a and b
assumes a1:"0<(a::nat)" and b1:"0<(b::nat)"
shows "\<exists>d c. ad<bc"
proof -
have a2: "a<(a+1)" by (arith)
from b1 and Nat.Suc_leI have a3: "1<=b" by (simp)
have a4: "(0::nat)<1" by (auto)
have a5: "a1<b(a+1)"
using a3 and a4 and a2 and a1 and b1 and
Ring_and_Field.mult_le_less_imp_less [where a="1" and b="b" and c="a" and
d="a+1"]
by (simp)
Now from
a * 1 < b * (a + 1)
I would demonstrate the thesis but I don't know how to do that.
Can anyone help me?
Thanks
Email Gateway (Aug 18 2022 at 09:42):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
You just need to use the Ex-Introduction rule, i.e. append
thus ?thesis
apply(rule_tac x="1" in exI) apply (rule_tac x="a+1" in exI)
by simp
to your proof.
Amine.
Email Gateway (Aug 18 2022 at 09:42):From: Alexander Krauss <krauss@in.tum.de>
Hello Gabriele,
Amine wrote:
Nicer still, and more in the Isar spirit:
Replace "proof -" by "proof (intro exI)". This applies exI in
backward style,
leaving you a schematic goal.
Replace the last "have" by "show", since this is already an instance
of the goal.
add "qed" in the end :-)
If you had only one existential quantifier instead of two, you could
even drop the "(intro exI)", but in your case, this would only
eliminate one of the quantifications... The "intro" method applies the
supplied introduction rules repeatedly.
Alex
Last updated: May 03 2024 at 08:18 UTC