Email Gateway (Aug 19 2022 at 09:01): Email Gateway (Aug 19 2022 at 09:01):From: Tobias Nipkow <nipkow@in.tum.de>
Am 19/10/2012 03:13, schrieb Christian Sternagel:
Note that the abbreviations "thus == then show" and "hence == then have"
are merely historical accidents. They require fewer bytes in memory,
but more typing by the user and more explanations to newcomers. The
reason is that the chaining or not chaining for elementary 'show' and
'have' elements are often changed during the proof development. And
there are further combinators like 'also' and 'moreover' that can be
combined with 'have' or 'show', and other goal elements like 'obtain'
that can participate in the chaining of facts in the same manner.So there is a large combinatorial space of
(then | from | with | ... | also | finally | moreover | ultimately)
(have | show | obtain | interpret ...)which is better spelled out as such explicitly, without the somewhat
pointless shortcuts 'hence' and 'thus' getting in the way.
I figure you thus (sorry) discourage the usage of "hence" and "thus". I have
often wondered myself whether I should use those idioms or not. Currently I do,
but especially your point about "chaining or not chaining" is very true and
hence (sorry again) "hence" and "thus" almost always cause more typing than they
save. I guess it is a reasonable convention to not use them in your proves?
Just as reasonable as using them - it's a pro-choice system ;-)
Tobias
cheers
chris
Last updated: Apr 18 2024 at 01:05 UTC