Email Gateway (Aug 22 2022 at 09:49): Email Gateway (Aug 22 2022 at 09:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear readers,
In Isabelle/HOL, I would like to reason about a polymorphic predicate P which is closed
under function composition. Since the concrete definition of the predicate is very tedious
and not relevant for the reasoning, I prefer to work just with the closure properties of
P. However, I have not found a nice way to accomplish that. Ideas and pointers are welcome.
Here are the details. The predicate P should have type "('a => 'b) => bool" and satisfy
properties such as the following (type variables may be restricted to some sort if needed):
Clearly, I cannot just define a locale l that fixes P as a parameter and assumes the
properties 1-3, because this does not typecheck as P occurs with different type instances.
Neither does inductive & friends work (for the same reason).
I could define "P" as "%_. True" and derive properties 1-3 from this. However, my theorem
is of the form
(ALL x. P x --> foo x) ==> P something ==> P something_more_complicated
where the first assumption is folded in a definition. Unfortunately, foo does not hold for
all x. Thus, defining "P" as "%_. True" would allow me to derive False from the first
assumption. So I could circumvent the actual proof of deriving the conclusion from the
second assumption.
I think of axiomatising properties 1-3 for P declared as a global constant with consts. In
a separate theory, I could show that "%_. True" satisfies all the properties stated. In my
understanding, this should ensure that the axioms do not introduce inconsistencies
anywhere. Still, as the theorem is proven in a scope where P is only axiomatised, I cannot
derive False from the first assumption in its proof. In fact, the theorem also holds for
the metamodel of HOL in which P is interpreted as the predicate that I am too lazy to
define (provided that it exists at all, but that's another issue). Is this argument
correct? Are there better ways to approach this?
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:50):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,
if there would be a nice way for doing this in HOL, we could simplify a
lot of things in the BNF package.
One approach that comes to mind is to use a locale with several
monomorphic copies of P (as many as you need to express the propetries).
Whether this works without being to painful, depends on what you
actually are proving. For BNFs we have used some (trivial) theorems that
are preconditioned with something like "M = M1 o M2" which is later
instantiated with the map_comp theorem (see e.g. src/HOL/BNF_Comp).
Best wishes,
Dmitriy
Email Gateway (Aug 22 2022 at 09:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
Thanks for the confirmation that there is no easy solution. Several monomorphic copies
probably do not scale, because my reasoning will involve various instances of the types.
So even in simple cases, I need at least 10 copies and I'd have to figure out in each case
which copy I need.
What do you think of my axiomatic suggestion?
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:50):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,
it sounds ok, in the sense that it will not introduce inconsistencies.
What I'm not sure about is how you plan to further work with your
predicate---do you need to integrate it with some other theories or is
(ALL x. P x --> foo x) ==> P something ==> P something_more_complicated
really the final theorem you are after?
Dmitriy
Email Gateway (Aug 22 2022 at 09:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
My plans are currently that something of the stated form will be my final theorem. Of
course, foo, something, and something_more_complicated depend on a huge number of other
definitions. So what do you mean by integration with other theories? In any case, I should
never have to do a case analysis or induction over my predicate - everything should follow
from the closure properties (of which there are many more than the ones I listed).
I guess that I will start by axiomatising the properties I need. Maybe I can find a
student to do the tedious construction later and derive the axioms from that.
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:50):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,
On 15.05.2015 11:34, Andreas Lochbihler wrote:
Hi Dmitriy,
My plans are currently that something of the stated form will be my
final theorem. Of course, foo, something, and
something_more_complicated depend on a huge number of other
definitions. So what do you mean by integration with other theories?
I meant something like instantiating the predicate.
In any case, I should never have to do a case analysis or induction
over my predicate - everything should follow from the closure
properties (of which there are many more than the ones I listed).
Yes, I've inferred that from the fact that the closure properties you've
listed don't give you anything very tedious to define (neither
inductively nor coinductively).
I guess that I will start by axiomatising the properties I need. Maybe
I can find a student to do the tedious construction later and derive
the axioms from that.
Another idea (going back to you %x. True definition):
context begin
private definition "Q x = True"
definition "P = Q"
lemma props:
"P id"
"P f ⟹ P g ⟹ P (f o g)"
"P (λx. c)"
unfolding P_def Q_def by simp_all
end
This makes it kind of hard (if possible at all) to access the definition
of Q. You prospective student would need to replace just a definition
rather than an axiomatization then ;-)
Dmitriy
Email Gateway (Aug 22 2022 at 09:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
My plans are currently that something of the stated form will be my final theorem. Of
course, foo, something, and something_more_complicated depend on a huge number of other
definitions. So what do you mean by integration with other theories?
I meant something like instantiating the predicate.
No, I do not think that this will be needed.
Another idea (going back to you %x. True definition):
context begin
private definition "Q x = True"
definition "P = Q"
lemma props:
"P id"
"P f ⟹ P g ⟹ P (f o g)"
"P (λx. c)"
unfolding P_def Q_def by simp_allend
This makes it kind of hard (if possible at all) to access the definition of Q. You
prospective student would need to replace just a definition rather than an axiomatization
then ;-)
Interesting idea, but I am not yet convinced. If I want to explain my proof to someone
else, I'd have to convince them that I am proving the statement only using props, but not
using Q_def. It is easier to argue that I am only using the axioms if there is nothing
else available in the theorem prover. Otherwise, I'd have to explain the whole concept of
name spaces and contexts. Moreover, I do not know how strict name spaces enforce
privateness. I'd expect that there are corner cases where the enforcement might fail
(blind shot: extract the proof terms for props and get the references to the theorem Q_def
from that?).
In the end, replacing the axiomatisation or the bogus definition should amount to the same
effort.
Andreas
Email Gateway (Aug 22 2022 at 09:50):From: Johannes Hölzl <hoelzl@in.tum.de>
Hm, then you need to ensure that Sledgehammer, Nitpick, Quickcheck do
not find the definition of Q. Otherwise you get a lot of warnings or
"false" proofs. Is "private" enough to guarantee this?
Email Gateway (Aug 22 2022 at 09:51):From: Makarius <makarius@sketis.net>
No. The new 'private' and 'qualified' command prefixes merely affect name
space accesses. Thus they do hardly anything at all. Only the surface
presentation of formal entities is modified.
Think of it like 'private' in Java or Scala, which is in some sense just a
joke as proven here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015-RC1/src/Pure/General/untyped.scala
It is easy to do similar things with 'private' name space entries within
the Isabelle context, using perfectly normal Isabelle/ML operations.
Back to the purpose of this thread: maybe the 'specification' command can
do a job here, although it is a bit old and not yet localized.
Makarius
Email Gateway (Aug 22 2022 at 09:51):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
Back to the purpose of this thread: maybe the 'specification' command can do a job here,
although it is a bit old and not yet localized.
I tried specification, but it did not work. It complains that the specified constant
occurs in different variants and I should add type constraints to make them the same. But
this defeats the point, because I want the predicate to have different type instances in
the axioms.
Best,
Andreas
Last updated: Apr 19 2024 at 01:05 UTC