Email Gateway (Oct 02 2023 at 17:30): Email Gateway (Oct 02 2023 at 17:30):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear all,
find attached two little theories related to fractional parts.
The first one are useful facts about arithmetic of frac, which, somewhat
surprisingly, seem not available in the current distribution.
The second one contains motivation for the first one, namely the
interpretation of the addition modulo one as an Abelian group.
Is this of a general interest?
Stepan
P.S.: I also have a third little theory showing that the unit interval
is an abstract metric space with the obvious circular distance (the only
nontrivial part being the triangle inequality). However, importing the
"HOL-Analysis.Abstract_Metric_Spaces" takes quite some time, and the
theory is used only twice in HOL, and never in AFP.
BTW, the time required for import is hardly necessary.
Abstract_Metric_Spaces.thy itself takes over 5 minutes on my machine,
and it contains proofs requiring many seconds. These are mostly familiar
time consuming smt one-liners most likely found by sledgehammer.
For example, line 3995
by (smt (verit, ccfv_threshold) comp_apply f g Pi_iff
uniformly_continuous_map_def)
taking over 7 sec. can be reduced to under 100ms by
using f g
unfolding uniformly_continuous_map_def comp_apply Pi_iff
by metis.
Fractional_Part_Arithmetic.thy
Unit_Interval_Group.thy
Email Gateway (Oct 03 2023 at 11:52):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Stepan, thanks for the fractional part material, which I’d like to incorporate into the repository. Also thanks for the suggestions to improve the build time of Abstract_Metric_Spaces, Which I have also incorporated. But remember, unless you are a developer (i.e. working with a regularly changing code base), you only ever have to build HOL-Analysis once.
It would be interesting to see your third example.
Larry
Email Gateway (Oct 03 2023 at 16:15):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear Larry,
thanks for you feedback. I enclose the third theory (I should mention
this is a joint work with Stepan Starosta). The theory also includes an
alternative approach using quotient_type of reals. I will appreciate any
comment concerning the comparison of the two approaches. My impression
is that the locale approach is (and is considered) the better and more
flexible option, although it requires a lot of superscripts and carriers...
As I mentioned in am older post (which went unnoticed) an intermediate
goal was to show that an irrational number generates a dense subgroup of
the real unit interval. As far as I can see, existing theories,
including the abstract spaces are not of much help. I will be happy if I
am wrong.
Two more comments:
yes, I am aware of the possibility to build the heap of the persistent
heap of HOL-Analysis. Just a side remark: if I am not missing something
basic, this is inconvenient not only for development, but also for
exploring. I imagine a situation in which I want to see or show somebody
how reals are defined, running into "Cannot update finished theory" with
very little possibilities, an have to restart, and wait anyway if I want
to see more.
in general, the situation is quite common that sledgehammer comes with
some crazy looking smt proof which takes ages, but it is quite
straightforward to unpack it into a super fast proof, which moreover
gives the right insight. I wonder whether this process could be somehow
facilitated. To start with, we use a macro written by Martin Raska which
transforms "by (smt A B C)" into "using A B C by smt" (and the same for
metis)
Best regards
Stepan
Last updated: Jan 04 2025 at 20:18 UTC