Email Gateway (Aug 22 2022 at 19:19): Email Gateway (Aug 22 2022 at 19:19):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Dear list,
It is a bit awkward to see that to prove a trivial lemma on natural numbers
requires syntactic fiddling on the notation of sets. It looks like the
whole reasoning machinery behind assumes a certain syntactic notation for
sets.
For example the lemma in the sequel requires me to apply (**) twice as
substitution just to get in a syntactic form where I can apply the
reasoning machinery provided by the library. Namely, it is awkward to see
that the notation {0..n::nat} is better than {na::nat. na ≤n} when proving
stuff on ∑ .
My question is why not just having the same syntactic sugar for both
notations? Any limitations to have an abbreviation of the form {na::nat. na
≤n} == {0..n::nat}? Or just because ∑ is too general? Is there an existing
AFP entry or an Isabelle theory that introduces these kind of abbreviations
when sets are specialized for natural numbers?
lemma "∑{na::nat. na ≤n} = ((n * (n +1)) div 2)"
proof -
have **: "⋀n. {na::nat. na ≤n} = {0.. n}"
by auto
show ?thesis
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
assume H1: "∑{na. na ≤ n} = n * (n + 1) div 2"
have *:"∑{naa. naa ≤ Suc n} = ∑{naa. naa ≤ n} + Suc n"
apply (subst **)
apply (subst **)
using sum.atLeast0_atMost_Suc
apply blast
done
show ?case
apply (subst *)
apply (subst H1)
apply (simp)
done
qed
qed
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 19:20):From: Lawrence Paulson <lp15@cam.ac.uk>
In logic there are always many ways of writing the same thing. But as regards Isabelle’s automation, as a general rule, you should prefer to minimise the use of bound variables. In this case, {na::nat. na ≤n} looks much more complicated to Isabelle than {0..n::nat}. More generally, consider replacing {x. P x & Q x} by the obvious intersection, et cetera.
Larry Paulson
Last updated: Apr 30 2024 at 04:19 UTC