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

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

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 constraintYes, 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

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,

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 constraintYes, 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.

say,

what you are actually trying to do?Makarius

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

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> ?thesisCould you please fix your Isabelle theory?

- Gergely
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-tasksMikhail

Hello,

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:

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.

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 constraintYes, proof methods cannot extend the logical context and expect to

work properly.

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.

you say,

what you are actually trying to do?Makarius

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?

- Gergely

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

Last updated: Oct 25 2021 at 20:20 UTC