Email Gateway (Aug 18 2022 at 12:05): Email Gateway (Aug 18 2022 at 12:05):From: Perry James <perry@dsrg.org>
Hi,
I'm having trouble proving the lemma below. My first idea was to "apply
(cases n)" since there are only 12 values of n that satisfy the assumption,
but that's not possible since n is bound. Also, applying arith, algebra, and
auto have no effect.
Is there any way to make progress?
Thanks in advance,
Perry
lemma " !! q qa n. [| 0 < n; int n <= 12; int n * q = 12; int n * qa = 18 |]
==> int n <= 6"
Email Gateway (Aug 18 2022 at 12:05):From: Amine Chaieb <chaieb@in.tum.de>
Here is a proof:
lemma
fixes q qa n
assumes n0: "n > 0" and n12: "int n <= 12"
and nq: "int n * q = 12" and nqa: "int n * qa = 18"
shows "int n <= 6"
proof-
from nq nqa
have "int n dvd 12" "int n dvd 18" unfolding dvd_def by auto
hence th: "n dvd 12" "n dvd 18" unfolding int_dvd_iff by auto
from gcd_greatest[OF th] have "n dvd 6" by (simp add: gcd.simps)
(* This is actually stronger than the final conclusion *)
hence "n <= 6" by (rule dvd_imp_le, simp)
then show "int n <= 6" by simp
qed
Some parts of the proof should be done automatically by algebra, but
apparently there is a bug (on my TODO).
Hope it helps,
Amine.
Perry James wrote:
Email Gateway (Aug 18 2022 at 12:05):From: John Matthews <matthews@galois.com>
Hi Perry,
You need to use case_tac rather than cases when n is bound by a meta-
quantifier in a subgoal, at least if you are carrying out an apply-
style proof. case_tac also works when the variable is not bound, and
like all other proof methods ending in _tac, you can apply it to other
than the first subgoal (e.g. apply (case_tac[3] ...)), to multiple
subgoals (e.g. apply (case_tac[1-3]...)), or to all subgoals (e.g.
apply (case_tac[!] ...)).
I'm not sure why cases doesn't allow you to split on meta-bound
variables, as this would be less confusing for new users. Similarly
for induct vs. induct_tac. Feature request?
-john
Email Gateway (Aug 18 2022 at 12:05):From: Makarius <makarius@sketis.net>
In a proper Isar proof you can never access hidden information from the
goal state, such as bound parameters. The case_tac/induct_tac versions
merely imitate the old tactical behaviour.
In your example there was no point to bind the outer parameters anyway,
and you can start right away on the problem presented in an open form
(fixes/assumes/shows, with fixes optionally implicit).
Makarius
Email Gateway (Aug 18 2022 at 12:05):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
Firstly, you can use (case_tac n) instead of (cases n) to do more or less
exactly the same thing, except that n can be a qyantified variable. This
follows a pattern in isabelle, with induct_tac, rule_tac, drule_tac etc
allowing in various ways the specification of a constant that only exists
within the context of the rule.
Something to think about for your particular case - you're working with an
assumption that a variable is less than a constant, in this case n <= 12.
There's a trick for getting all the cases at once. Oddly, I don't seem to
be able to get it working for <= thisevening, but consider the trick for
n < 12:
lemma n_less_val_disj:
"m ~= (0 :: nat) ==>
(n < m) = (n = m - 1 | n < m - 1)"
apply (case_tac n, simp_all)
apply fastsimp
apply (case_tac m, simp_all)
apply fastsimp
done
lemma test_this:
"n < (12 :: nat) ==> P"
apply (simp add: n_less_val_disj)
oops
The reduction to cases can more or less take care of itself. I'm sure
there's a nice way to do this for int n <= 12, but I'll leave you to
figure out what it might be.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 12:06):From: Perry James <perry@dsrg.org>
Hi Thomas,
Thanks for your reply. The trick in n_less_val_disj will be added to my
bag. I've played with variations on it and am not having much luck.
The problem I'm having is that the values in my lemma are ints, not
nats. Even though n itself is a nat, it is cast to int for the
comparisons. Thus all the nice tools for working with the much simpler nats
are not available (at least with my limited skills).
Best regards,
Perry
Email Gateway (Aug 18 2022 at 12:06):From: Tobias Nipkow <nipkow@in.tum.de>
As this goal only involves linear arithmetic, it can be solved
automatically:
by arith
Tobias
Email Gateway (Aug 18 2022 at 12:06):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
Perhaps a more direct specialisation to your problem is to use the
"int _ <= _" pattern in the helper lemma. Also, as Tobias points out,
these helpers can be proven by arith:
lemma int_le_val_disj:
"m > 0 ==> (int n <= m) = (int n = m | int n <= m - 1)"
by arith
lemma "int n <= 12 ==> P"
apply (simp add: int_le_val_disj)
oops
A similar trick was used in our project to prove that
{0 ..< 5} was equal to {0, 1, 2, 3, 4} - once again,
specialisation to the syntactic form in which the <
appears was helpful.
Yours,
Thomas.
Last updated: May 03 2024 at 08:18 UTC