Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Implicit exporting of goal state by different ...


view this post on Zulip Email Gateway (Sep 17 2020 at 17:01):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
Hello!

Recently, I experimented with implementation of Isabelle proof methods,
commands and proof elements to learn Isabelle internals more deeply as
we plan to implement Isabelle commands and methods for our program
verification framework. At some point, I encountered quite puzzling
behavior of commands done, by and qed with respect to implicit
exporting of the resulting goal state (actually, the protected initial
statement as a theorem) into the outer context. I attached an example
exposing the various behaviors. The question is whether these various
differences in behavior are expected, especially the situation when the
proof is successfully finished inside jEdit, but then fails during build
by isabelle build command. I understand that normally Isabelle methods
do not introduce local assumptions or fixed variables, so this seems not
really critical (no intent to actually implement such methods for the
users), but it would help with the general understanding to know whether
this is totally unspecified to introduce those assumptions or is merely
a pragmatic constraint

Regards, Mikhail
Bug.thy

view this post on Zulip Email Gateway (Nov 07 2020 at 21:09):

From: Makarius <makarius@sketis.net>
On 17/09/2020 19:00, Mikhail Mandrykin wrote:

Recently, I experimented with implementation of Isabelle proof methods,
commands and proof elements to learn Isabelle internals more deeply as we plan
to implement Isabelle commands and methods for our program verification
framework. At some point, I encountered quite puzzling behavior of commands
done, by and qed with respect to implicit exporting of the resulting
goal state (actually, the protected initial statement as a theorem) into the
outer context. I attached an example exposing the various behaviors. The
question is whether these various differences in behavior are expected,
especially the situation when the proof is successfully finished inside jEdit,
but then fails during build by isabelle build command.

I understand that> normally Isabelle methods do not introduce local
assumptions or fixed
variables, so this seems not really critical (no intent to actually implement
such methods for the users), but it would help with the general understanding
to know whether this is totally unspecified to introduce those assumptions or
is merely a pragmatic constraint

Yes, proof methods cannot extend the logical context and expect to work properly.

There are certain principles how proof contexts are constructed/deconstructed
by the Isar language, according to its structure. Some of this is explained in
the "implementation" manual, but the general principle of survival is to do
this in the "usual way", e.g. by looking at existing implementations in the
sources.

Your theory "Bug" looks very non-standard in various respects. Can you say,
what you are actually trying to do?

Makarius

view this post on Zulip Email Gateway (Nov 07 2020 at 22:34):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
Hello,

Your theory "Bug" looks very non-standard in various respects. Can you
say,
what you are actually trying to do?

Actually, I was preparing a small Isabelle/ML programing tutorial for
relatively experienced functional programmers (in Haskell and OCaml),
primarily for internal use, to emphasize the features that are needed to
implement custom proof methods. The tutorial was meant to be very
practically-oriented and so consisted of a set of example
implementations that would use only the interfaces from a documented set
of ML interfaces. So I proceeded in the following way: I just came up
with a problem, implemented a solution and then documented all the
interfaces used in the solution using the available documentation as
well as the knowledge obtained from inspection of the sources during the
implementation. As one of the final, more complex examples, I decided to
implement a sample triple of a proof method, an Isar command and a local
context command to support introduction of obtained facts into the local
context that would also support goal refinement with obtained variables.
This is not possible in Pure, but in HOL the Hilbert epsilon operator
can be used to extract the corresponding witness. I actually implemented
the tactic and the commands (attached the resulting sample theory as
Proof_Context.thy) and they seem to work as expected, the simplest way
to observe them in action is in the schematic_goal wf_min'' that
directly refines the statement using the obtained epsilon-expressions.
However, I myself did not fully understand the limitations of the proof
methods since they are actually context-tactics and can return a
modified context as a result, but I had not found any real examples of
methods that would alter the context in any way other than by
introduction of cases. So indeed, the logical context is never modified,
only the extra-logical part is changed. The sample method
hilbert_guess (in Proof_Context.thy) thus is not a proper method as it
breaks this convention by introducing obtained facts into the logical
context. So when I tried to compile the resulting tutorial document I
experienced the problems I described and decided to clarify whether this
is an intended limitation of proof methods, because in practice in many
cases extending the logical context with assumptions actually works (the
assumptions are exported by the done/qed commands). So because this
method is only intended as experimental exploratory code, this is not a
real issue, the real methods we implemented so far (those that work in
auxiliary local contexts) all perform the export internally and only
alter the context for extra-logical purposes e.g. remembering a
counterexample model extracted from an SMT solver (Z3). The repository
with the tutorial is available at
https://forge.ispras.ru/projects/isabelle-tutorial/repository/isabelle-tasks
. Currently, we switched to different parts of our framework
(implementing the shallow embedding and the translator), so the tutorial
is currently not actively used, but may soon be needed as constructing
the embedding also requires the use of custom automated proofs.

Regards, Mikhail

Makarius писал 2020-11-08 00:09:

On 17/09/2020 19:00, Mikhail Mandrykin wrote:

Recently, I experimented with implementation of Isabelle proof
methods,
commands and proof elements to learn Isabelle internals more deeply as
we plan
to implement Isabelle commands and methods for our program
verification
framework. At some point, I encountered quite puzzling behavior of
commands
done, by and qed with respect to implicit exporting of the
resulting
goal state (actually, the protected initial statement as a theorem)
into the
outer context. I attached an example exposing the various behaviors.
The
question is whether these various differences in behavior are
expected,
especially the situation when the proof is successfully finished
inside jEdit,
but then fails during build by isabelle build command.

I understand that> normally Isabelle methods do not introduce local
assumptions or fixed
variables, so this seems not really critical (no intent to actually
implement
such methods for the users), but it would help with the general
understanding
to know whether this is totally unspecified to introduce those
assumptions or
is merely a pragmatic constraint

Yes, proof methods cannot extend the logical context and expect to
work properly.

There are certain principles how proof contexts are
constructed/deconstructed
by the Isar language, according to its structure. Some of this is
explained in
the "implementation" manual, but the general principle of survival is
to do
this in the "usual way", e.g. by looking at existing implementations in
the
sources.

Your theory "Bug" looks very non-standard in various respects. Can you
say,
what you are actually trying to do?

Makarius
Proof_Context.thy

view this post on Zulip Email Gateway (Nov 07 2020 at 22:54):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
Mikhail Mandrykin писал 2020-11-08 01:33:

The repository with the tutorial is available at
https://forge.ispras.ru/projects/isabelle-tutorial/repository/isabelle-tasks
Sorry, it seems this link won't work, if anyone is interested I uploaded
a mirror on GitHub at https://github.com/schrodibear/isabelle-tasks

Mikhail

Hello,

Your theory "Bug" looks very non-standard in various respects. Can you
say,
what you are actually trying to do?

Actually, I was preparing a small Isabelle/ML programing tutorial for
relatively experienced functional programmers (in Haskell and OCaml),
primarily for internal use, to emphasize the features that are needed
to implement custom proof methods. The tutorial was meant to be very
practically-oriented and so consisted of a set of example
implementations that would use only the interfaces from a documented
set of ML interfaces. So I proceeded in the following way: I just came
up with a problem, implemented a solution and then documented all the
interfaces used in the solution using the available documentation as
well as the knowledge obtained from inspection of the sources during
the implementation. As one of the final, more complex examples, I
decided to implement a sample triple of a proof method, an Isar
command and a local context command to support introduction of
obtained facts into the local context that would also support goal
refinement with obtained variables. This is not possible in Pure, but
in HOL the Hilbert epsilon operator can be used to extract the
corresponding witness. I actually implemented the tactic and the
commands (attached the resulting sample theory as Proof_Context.thy)
and they seem to work as expected, the simplest way to observe them in
action is in the schematic_goal wf_min'' that directly refines the
statement using the obtained epsilon-expressions. However, I myself
did not fully understand the limitations of the proof methods since
they are actually context-tactics and can return a modified context as
a result, but I had not found any real examples of methods that would
alter the context in any way other than by introduction of cases. So
indeed, the logical context is never modified, only the extra-logical
part is changed. The sample method hilbert_guess (in
Proof_Context.thy) thus is not a proper method as it breaks this
convention by introducing obtained facts into the logical context. So
when I tried to compile the resulting tutorial document I experienced
the problems I described and decided to clarify whether this is an
intended limitation of proof methods, because in practice in many
cases extending the logical context with assumptions actually works
(the assumptions are exported by the done/qed commands). So
because this method is only intended as experimental exploratory code,
this is not a real issue, the real methods we implemented so far
(those that work in auxiliary local contexts) all perform the export
internally and only alter the context for extra-logical purposes e.g.
remembering a counterexample model extracted from an SMT solver (Z3).
The repository with the tutorial is available at
https://forge.ispras.ru/projects/isabelle-tutorial/repository/isabelle-tasks
. Currently, we switched to different parts of our framework
(implementing the shallow embedding and the translator), so the
tutorial is currently not actively used, but may soon be needed as
constructing the embedding also requires the use of custom automated
proofs.

Regards, Mikhail

Makarius писал 2020-11-08 00:09:

On 17/09/2020 19:00, Mikhail Mandrykin wrote:

Recently, I experimented with implementation of Isabelle proof
methods,
commands and proof elements to learn Isabelle internals more deeply
as we plan
to implement Isabelle commands and methods for our program
verification
framework. At some point, I encountered quite puzzling behavior of
commands
done, by and qed with respect to implicit exporting of the
resulting
goal state (actually, the protected initial statement as a theorem)
into the
outer context. I attached an example exposing the various behaviors.
The
question is whether these various differences in behavior are
expected,
especially the situation when the proof is successfully finished
inside jEdit,
but then fails during build by isabelle build command.

I understand that> normally Isabelle methods do not introduce local
assumptions or fixed
variables, so this seems not really critical (no intent to actually
implement
such methods for the users), but it would help with the general
understanding
to know whether this is totally unspecified to introduce those
assumptions or
is merely a pragmatic constraint

Yes, proof methods cannot extend the logical context and expect to
work properly.

There are certain principles how proof contexts are
constructed/deconstructed
by the Isar language, according to its structure. Some of this is
explained in
the "implementation" manual, but the general principle of survival is
to do
this in the "usual way", e.g. by looking at existing implementations
in the
sources.

Your theory "Bug" looks very non-standard in various respects. Can you
say,
what you are actually trying to do?

Makarius

view this post on Zulip Email Gateway (Nov 07 2020 at 23:03):

From: Makarius <makarius@sketis.net>
On 07/11/2020 23:33, Mikhail Mandrykin wrote:

However, I myself did
not fully understand the limitations of the proof methods since they are
actually context-tactics and can return a modified context as a result, but I
had not found any real examples of methods that would alter the context in any
way other than by introduction of cases. So indeed, the logical context is
never modified, only the extra-logical part is changed.

That is indeed an important observation, both for this concrete situation and
as a general principle in Isabelle: things that are never done (or only in odd
exceptional situations) can lead to undefined behaviour.

Put to the extreme, you can do almost arbitrary non-sense with Isabelle,
especially in conjunction with logical operations where the programming
interfaces cannot guarantee the structural integrity of the concepts behind
it: A theorem might be a theorem, but it could be non-sense or break other
tools or infrastructure (like Isar proof language elements).

The
repository with the tutorial is available at
https://forge.ispras.ru/projects/isabelle-tutorial/repository/isabelle-tasks

That seems to be non-public.

Makarius

view this post on Zulip Email Gateway (Nov 09 2020 at 16:23):

From: Mikhail Mandrykin <mandrykin@ispras.ru>

Could you please fix your Isabelle theory?

In Isabelle2020 it seems to be slight incompatibility in the definition
of asym inductive predicate in Relation.thy: it was simplified in
the development version (would-be 2021) by removing an extra premise
irrefl R, which causes the failure. I pushed a fix into Isabelle2020
compatibility branch

Mikhail

Buday Gergely писал 2020-11-09 12:29:

I cloned your github repository and ran

isabelle build -D .

to get

Running Tasks ...
Tasks FAILED
(see also
C:\Users\EKE\.isabelle\Isabelle2020\heaps\polyml-5.8.1_x86_64_32-windows\log\Tasks)
\<Longrightarrow> ?thesis
\<lbrakk>bij ?f;
 \<And>x.
    \<lbrakk>?y = ?f x;
     \<And>x'. ?y = ?f x' \<Longrightarrow> x' = x\<rbrakk>
    \<Longrightarrow> ?thesis\<rbrakk>
\<Longrightarrow> ?thesis

Could you please fix your Isabelle theory?

11/7/2020 11:53 PM keltezéssel, Mikhail Mandrykin írta:

Mikhail Mandrykin писал 2020-11-08 01:33:

The repository with the tutorial is available at
https://forge.ispras.ru/projects/isabelle-tutorial/repository/isabelle-tasks
Sorry, it seems this link won't work, if anyone is interested I
uploaded a mirror on GitHub at
https://github.com/schrodibear/isabelle-tasks

Mikhail

Hello,

Your theory "Bug" looks very non-standard in various respects. Can
you say,
what you are actually trying to do?

Actually, I was preparing a small Isabelle/ML programing tutorial for
relatively experienced functional programmers (in Haskell and OCaml),
primarily for internal use, to emphasize the features that are needed
to implement custom proof methods. The tutorial was meant to be very
practically-oriented and so consisted of a set of example
implementations that would use only the interfaces from a documented
set of ML interfaces. So I proceeded in the following way: I just
came
up with a problem, implemented a solution and then documented all the
interfaces used in the solution using the available documentation as
well as the knowledge obtained from inspection of the sources during
the implementation. As one of the final, more complex examples, I
decided to implement a sample triple of a proof method, an Isar
command and a local context command to support introduction of
obtained facts into the local context that would also support goal
refinement with obtained variables. This is not possible in Pure, but
in HOL the Hilbert epsilon operator can be used to extract the
corresponding witness. I actually implemented the tactic and the
commands (attached the resulting sample theory as Proof_Context.thy)
and they seem to work as expected, the simplest way to observe them
in
action is in the schematic_goal wf_min'' that directly refines the
statement using the obtained epsilon-expressions. However, I myself
did not fully understand the limitations of the proof methods since
they are actually context-tactics and can return a modified context
as
a result, but I had not found any real examples of methods that would
alter the context in any way other than by introduction of cases. So
indeed, the logical context is never modified, only the extra-logical
part is changed. The sample method hilbert_guess (in
Proof_Context.thy) thus is not a proper method as it breaks this
convention by introducing obtained facts into the logical context. So
when I tried to compile the resulting tutorial document I experienced
the problems I described and decided to clarify whether this is an
intended limitation of proof methods, because in practice in many
cases extending the logical context with assumptions actually works
(the assumptions are exported by the done/qed commands). So
because this method is only intended as experimental exploratory
code,
this is not a real issue, the real methods we implemented so far
(those that work in auxiliary local contexts) all perform the export
internally and only alter the context for extra-logical purposes e.g.
remembering a counterexample model extracted from an SMT solver (Z3).
The repository with the tutorial is available at
https://forge.ispras.ru/projects/isabelle-tutorial/repository/isabelle-tasks
. Currently, we switched to different parts of our framework
(implementing the shallow embedding and the translator), so the
tutorial is currently not actively used, but may soon be needed as
constructing the embedding also requires the use of custom automated
proofs.

Regards, Mikhail

Makarius писал 2020-11-08 00:09:

On 17/09/2020 19:00, Mikhail Mandrykin wrote:

Recently, I experimented with implementation of Isabelle proof
methods,
commands and proof elements to learn Isabelle internals more deeply
as we plan
to implement Isabelle commands and methods for our program
verification
framework. At some point, I encountered quite puzzling behavior of
commands
done, by and qed with respect to implicit exporting of the
resulting
goal state (actually, the protected initial statement as a theorem)
into the
outer context. I attached an example exposing the various
behaviors. The
question is whether these various differences in behavior are
expected,
especially the situation when the proof is successfully finished
inside jEdit,
but then fails during build by isabelle build command.

I understand that> normally Isabelle methods do not introduce local
assumptions or fixed
variables, so this seems not really critical (no intent to actually
implement
such methods for the users), but it would help with the general
understanding
to know whether this is totally unspecified to introduce those
assumptions or
is merely a pragmatic constraint

Yes, proof methods cannot extend the logical context and expect to
work properly.

There are certain principles how proof contexts are
constructed/deconstructed
by the Isar language, according to its structure. Some of this is
explained in
the "implementation" manual, but the general principle of survival
is to do
this in the "usual way", e.g. by looking at existing implementations
in the
sources.

Your theory "Bug" looks very non-standard in various respects. Can
you say,
what you are actually trying to do?

Makarius

view this post on Zulip Email Gateway (Nov 10 2020 at 10:11):

From: Buday Gergely via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I cloned your github repository and ran

isabelle build -D .

to get

Running Tasks ...
Tasks FAILED
(see also
C:\Users\EKE\.isabelle\Isabelle2020\heaps\polyml-5.8.1_x86_64_32-windows\log\Tasks)
\<Longrightarrow> ?thesis
\<lbrakk>bij ?f;
 \<And>x.
    \<lbrakk>?y = ?f x;
     \<And>x'. ?y = ?f x' \<Longrightarrow> x' = x\<rbrakk>
    \<Longrightarrow> ?thesis\<rbrakk>
\<Longrightarrow> ?thesis

Could you please fix your Isabelle theory?

11/7/2020 11:53 PM keltezéssel, Mikhail Mandrykin írta:


Last updated: Sep 28 2021 at 19:14 UTC