Email Gateway (Aug 22 2022 at 10:11): Email Gateway (Aug 22 2022 at 10:11):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Bertram et al,
Neither source says that these facts are hidden and only used
internally.
Secondly, I feel that there is a tangible advantage of making these
facts available, which to my mind means that they should also be
discoverable through find_theorems, though not necessarily by
sledgehammer. (Can those two visibilities be separated in Isabelle?)
One advantage is that it allows unfolding locale definitions
selectively. But perhaps more importantly, by having the definitions
as theorems, they become compatible with existing proof tactics (for
example, I can add loc_def as a simp rule to auto; I cannot do that
with unfold_locales).
first, some terminology to make issues more clear:
The facts (or, the locale predicate with corresponding facts) is not
»hidden«, otherwise it would not be accessible through the name space,
which is not the case.
Instead, it is »concealed«, which is no more than an internal flag
which some parts of the system (including find_theorems and probabliby
sledgehammer) are free to interpret in a certain fashion. For the case
of find_theorems, it just skips these on search.
Hence, the definition and rules for locale predicates are accessible,
and this is used throughout the distribution for some low-level
constructions. Their naming convention is firmly established since 2007
(?) and with some familiarity it should not be difficult to use them in
advanced satisfiability proofs for locale expressions etc. pp.
It is indeed arguable why locale predicates must be concealed et all,
but I guess this has something to do with sledgehammer!?
The reasoning seems to be that the locale predicate (and hence its
definition) is more or less an implementation detail of locales, so you
shouldn't access it directly.
I tend to put it this way: Isabelle has a module system (locales) which
is founded in its the logical calculus itself, hence you are free to
intermix them in formally sound ways. But then you are loosing a
certain discipline which normally is imposed by the way the module
system is implemented, so you have to establish your own discipline in
order not to screw up the practical (re)usability of the system.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:12):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
It is indeed arguable why locale predicates must be concealed et all,
but I guess this has something to do with sledgehammer!?
I doubt it has anything to do with Sledgehammer.
Jasmin
Email Gateway (Aug 22 2022 at 10:14):From: Larry Paulson <lp15@cam.ac.uk>
I've stumbled across a related issue with find_theorems that certainly seems wrong. I was searching for the theorem Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type class axiom here:
class dist_norm = dist + norm + minus +
assumes dist_norm: "dist x y = norm (x - y)"
Calling find_theorems with suitable patterns, such as
dist "norm (_-_)”
does not return this theorem among the results, but clearly it should.
Larry
Email Gateway (Aug 22 2022 at 10:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
There is nothing wrong with type classes here:
class involutory =
fixes f :: "'a ⇒ 'a"
assumes involutory: "f (f x) = x"
begin
lemma involutory3:
"f (f (f x)) = f x"
by (fact involutory)
end
find_theorems "f"
It seems to be a constraint issue:
find_theorems "_ = norm (_ - _)"
~> 'a::real_normed_vector is inferred
find_theorems "_ = norm ((_::'a::dist_norm) - _)"
~> typing error
Maybe some naughty tweaking of sort constraints or an unforseen
behaviour of coercions, but these are mere guesses. I do not understand
these parts of the type class hierarchy.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:21):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Donnerstag, den 25.06.2015, 16:50 +0200 schrieb Florian Haftmann:
There is nothing wrong with type classes here:
class involutory =
fixes f :: "'a ⇒ 'a"
assumes involutory: "f (f x) = x"
beginlemma involutory3:
"f (f (f x)) = f x"
by (fact involutory)end
find_theorems "f"
It seems to be a constraint issue:
find_theorems "_ = norm (_ - _)"
~> 'a::real_normed_vector is inferred
find_theorems "_ = norm ((_::'a::dist_norm) - _)"
~> typing errorMaybe some naughty tweaking of sort constraints or an unforseen
behaviour of coercions, but these are mere guesses. I do not understand
these parts of the type class hierarchy.
Yes, in Real_Vector_Spaces are a couple of "add_const_constraint"s for
dist, open, and norm. These give a nicer user experience when only
working with the semantic typeclasses. Obviously, if one needs to
instantiate syntactic typelcasses it is more complicated.
Am 19.06.2015 um 17:22 schrieb Larry Paulson:
I've stumbled across a related issue with find_theorems that certainly seems wrong. I was searching for the theorem Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type class axiom here:
class dist_norm = dist + norm + minus +
assumes dist_norm: "dist x y = norm (x - y)"Calling find_theorems with suitable patterns, such as
dist "norm (_-_)”
does not return this theorem among the results, but clearly it should.
Larry
On 14 Jun 2015, at 18:35, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:
Hi Bertram et al,
Neither source says that these facts are hidden and only used
internally.Secondly, I feel that there is a tangible advantage of making these
facts available, which to my mind means that they should also be
discoverable through find_theorems, though not necessarily by
sledgehammer. (Can those two visibilities be separated in Isabelle?)
One advantage is that it allows unfolding locale definitions
selectively. But perhaps more importantly, by having the definitions
as theorems, they become compatible with existing proof tactics (for
example, I can add loc_def as a simp rule to auto; I cannot do that
with unfold_locales).first, some terminology to make issues more clear:
The facts (or, the locale predicate with corresponding facts) is not
»hidden«, otherwise it would not be accessible through the name space,
which is not the case.Instead, it is »concealed«, which is no more than an internal flag
which some parts of the system (including find_theorems and probabliby
sledgehammer) are free to interpret in a certain fashion. For the case
of find_theorems, it just skips these on search.Hence, the definition and rules for locale predicates are accessible,
and this is used throughout the distribution for some low-level
constructions. Their naming convention is firmly established since 2007
(?) and with some familiarity it should not be difficult to use them in
advanced satisfiability proofs for locale expressions etc. pp.It is indeed arguable why locale predicates must be concealed et all,
but I guess this has something to do with sledgehammer!?The reasoning seems to be that the locale predicate (and hence its
definition) is more or less an implementation detail of locales, so you
shouldn't access it directly.I tend to put it this way: Isabelle has a module system (locales) which
is founded in its the logical calculus itself, hence you are free to
intermix them in formally sound ways. But then you are loosing a
certain discipline which normally is imposed by the way the module
system is implemented, so you have to establish your own discipline in
order not to screw up the practical (re)usability of the system.Cheers,
Florian--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Email Gateway (Aug 22 2022 at 10:21):From: Larry Paulson <lp15@cam.ac.uk>
We clearly need to look at how type inference affects find_theorems.
The missing at sea (dist_norm) belongs to the type class of the same name, of which real_normed_vector is a subclass. It seems obvious that the pattern "_ = norm (_ - _)” should pick up
dist_norm: "dist x y = norm (x - y)"
Larry
Email Gateway (Aug 22 2022 at 10:35):From: Lars Noschinski <noschinl@in.tum.de>
The reasoning seems to be that the locale predicate (and hence its
definition) is more or less an implementation detail of locales, so you
shouldn't access it directly. The similarly, the lemmas establishing
locale relationships are hidden from the public view. This also effects
sledgehammer.
-- Lars
Email Gateway (Aug 22 2022 at 10:36):From: Larry Paulson <lp15@cam.ac.uk>
I agree with this view. There are many theorems that probably shouldn’t be given to sledgehammer, though the only justification for this would be that they are unlikely to be helpful for finding proofs. But it should be possible to search for them. I have been tripped up here as well.
Larry Paulson
Last updated: Apr 26 2024 at 16:20 UTC