Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with function package

view this post on Zulip Email Gateway (Aug 19 2022 at 17:00):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

today we stumbled over a strange behavior of the function package, which refused some very standard function definition that relies upon locally fixed parameters.

theory Scratch
imports Main
begin

locale foo =
fixes x :: nat
begin

function f :: "nat => nat" where
"f y = (if y > x then f (y - 1) else y)"
apply pat_completeness
apply auto (* works and leaves no proof obligations *)
done (* post processing of function package fails:
exception THM 0 raised (line 726 of "thm.ML"):
forall_intr: variable "x" free in assumptions
(⋀y. x = y ⟹ P) ⟹ P *)
end
end

The above function was accepted without problems until Isabelle2013, and is refused in Isabelle2013-1/2, 2014, and also in todays repository snapshot. Perhaps it is related to the news entry for Isabelle2013-1:

Kind regards,
Christian, Florian, and René

view this post on Zulip Email Gateway (Aug 19 2022 at 17:00):

From: Manuel Eberl <eberlm@in.tum.de>
Oh dear. This looks like something I am probably responsible for. I
shall look into it in the next few days.

My first guess would be that it has something to do with my very poor
understanding of contexts.

Cheers,
Manuel

view this post on Zulip Email Gateway (Aug 19 2022 at 17:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I mae a first analysis

in function_elims.ML

fun mk_funeq 0 T (acc_vars, acc_lhs) =
let val y = Free("y", T)
in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq
(acc_lhs, y))), T) end
| mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars,
acc_lhs) =
let val xn = Free ("x" ^ Int.toString n, S)
in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end
| mk_funeq _ _ _ = raise TERM ("Not a function.", [f]);

This looks suspicious since you cannot assume that "x\d" and "y" are
fresh. You should use a pattern like

Name.variant "x" (Proof_Context.names_of ctxt)

Hope this helps,
Florian

Am 27.01.2015 um 18:59 schrieb Manuel Eberl:

Oh dear. This looks like something I am probably responsible for. I
shall look into it in the next few days.

My first guess would be that it has something to do with my very poor
understanding of contexts.

Cheers,
Manuel

On 27/01/15 18:34, René Thiemann wrote:

Dear all,

today we stumbled over a strange behavior of the function package, which refused some very standard function definition that relies upon locally fixed parameters.

theory Scratch
imports Main
begin

locale foo =
fixes x :: nat
begin

function f :: "nat => nat" where
"f y = (if y > x then f (y - 1) else y)"
apply pat_completeness
apply auto (* works and leaves no proof obligations *)
done (* post processing of function package fails:
exception THM 0 raised (line 726 of "thm.ML"):
forall_intr: variable "x" free in assumptions
(⋀y. x = y ⟹ P) ⟹ P *)
end
end

The above function was accepted without problems until Isabelle2013, and is refused in Isabelle2013-1/2, 2014, and also in todays repository snapshot. Perhaps it is related to the news entry for Isabelle2013-1:

Kind regards,
Christian, Florian, and René

signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 17:01):

From: Manuel Eberl <eberlm@in.tum.de>
The issue was actually not the one you highlighted, but another instance
of the same problem in mutual.ML.

I fixed all the occurrences of this problem in the function package and
everything seems to be running smoothly now. I already pushed the bug fix.

Thanks for your analysis and telling me how to fix it.

Cheers,
Manuel

view this post on Zulip Email Gateway (Aug 19 2022 at 17:01):

From: Makarius <makarius@sketis.net>
Just from to wording of it, is a dangerous claim to have "fixed" "all"
"bugs". It is important to develop a sense of realism of what a change
really does. The Isabelle mailing lists are full of postings of myself,
where I try to explain that over and over again.

In particular it does not make any sense to produe Isabelle changesets
"like fixed bug" -- some actual information needs to be put into a
changelog.

Here is some general information on Isabelle development:

* README_REPOSITORY

* The "implementation" manual, esp. chapter 0 and chapter 1 as a start.

* Existing examples that are known to be done properly.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 17:01):

From: Manuel Eberl <eberlm@in.tum.de>

Just from to wording of it, is a dangerous claim to have "fixed" "all"
"bugs".
That is not what I said. I said I fixed all occurrences of _this one
class_ of bug in the function package, i.e. choosing fixed names for
variables that may not be fresh in the given context. I am reasonably
sure that I caught them all, seeing as I am the one who introduced them.
Not 100% sure, but reasonably so.

I would have put information in a change log if I had found such a
change log. The only thing I was aware of was the NEWS file, but that
did not seem a suitable place. Where /am/ I supposed to describe the
change? The top of the changed file itself?

I did read most of the information you suggested, but could not find any
reference of where to describe such changes.

Manuel

view this post on Zulip Email Gateway (Aug 19 2022 at 17:01):

From: Makarius <makarius@sketis.net>
On Wed, 28 Jan 2015, Manuel Eberl wrote:

I would have put information in a change log if I had found such a
change log.

The changlog is what you write as commit message. It ends up in the
persistent and immutable history, which is the main documentation of the
ongoing Isabelle development process. README_REPOSITORY tries to explain
all that a bit.

Such history entries are essential for future archeaological diggings,
when new problems are exposed, usually on older attempts to "fix bugs".
In such situations it is important to see what was really going on at a
certain point of time, and what the author of a change was thinking. So
"fixed bug in foo" is not informative, but is equivalent to an empty
changelog entry.

The top of the changed file itself?

People did that before RCS and CVS. We have Mercurial today, with the
history in the history, and the source in the source. I.e. clearly
separated meta-data and data.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 17:01):

From: Makarius <makarius@sketis.net>
That works in many situations, but is a bit low-level. The Variable
module provides canonical entry points to work with local variables, e.g.
via Variable.variant_frees or Variable.variant_fixes.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 17:01):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,

Thanks for your analysis and telling me how to fix it.

well, it was no more than a rush first analysis.

It is indeed best here to use the existing infrastructure in
variable.ML, as Makarius pointed out.

One technical comment:

val name_ctxt = Variable.names_of ctxt
val (free_vars, prop, ranT, name_ctxt) =
mk_funeq arity (fastype_of f) name_ctxt ([], f);

This pattern (deliberate shadowing of names) is dangerous since it is
not robust against changed line positions. »Not robust« in the sense
that the compiler cannot detect such slips.

There are two approaches to avoid this:

a) In smooth cases, the funny combinators ||>> and |-> (##>> and #->)
can save you from mentioning sth more than once (see the Isabelle/ML
chapter in the implementation manual).

b) In complex cases, this is not feasible. Then you have to swallow the
bitter pill and give explicit indices. Popular schemas are (foo, foo',
foo'') for little occurrences and (foo1, foo2, foo3, …) for many
occurrences. In extreme cases also explicit application-domain prefixes
can be seen (cf.
http://isabelle.in.tum.de/repos/isabelle/file/df5dc24ca712/src/Pure/Isar/expression.ML#l857).
Looks like a parody on ancient line-number based programming, but is
robust against accidental position swapping.

Hope this helps,
Florian

Cheers,
Manuel

On 28/01/15 08:26, Florian Haftmann wrote:

I mae a first analysis

in function_elims.ML

fun mk_funeq 0 T (acc_vars, acc_lhs) =
let val y = Free("y", T)
in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq
(acc_lhs, y))), T) end
| mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars,
acc_lhs) =
let val xn = Free ("x" ^ Int.toString n, S)
in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end
| mk_funeq _ _ _ = raise TERM ("Not a function.", [f]);
This looks suspicious since you cannot assume that "x\d" and "y" are
fresh. You should use a pattern like

Name.variant "x" (Proof_Context.names_of ctxt)

Hope this helps,
Florian

Am 27.01.2015 um 18:59 schrieb Manuel Eberl:

Oh dear. This looks like something I am probably responsible for. I
shall look into it in the next few days.

My first guess would be that it has something to do with my very poor
understanding of contexts.

Cheers,
Manuel

On 27/01/15 18:34, René Thiemann wrote:

Dear all,

today we stumbled over a strange behavior of the function package, which refused some very standard function definition that relies upon locally fixed parameters.

theory Scratch
imports Main
begin

locale foo =
fixes x :: nat
begin

function f :: "nat => nat" where
"f y = (if y > x then f (y - 1) else y)"
apply pat_completeness
apply auto (* works and leaves no proof obligations *)
done (* post processing of function package fails:
exception THM 0 raised (line 726 of "thm.ML"):
forall_intr: variable "x" free in assumptions
(⋀y. x = y ⟹ P) ⟹ P *)
end
end

The above function was accepted without problems until Isabelle2013, and is refused in Isabelle2013-1/2, 2014, and also in todays repository snapshot. Perhaps it is related to the news entry for Isabelle2013-1:

  • Function package: For each function f, new rules f.elims are
    generated, which eliminate equalities of the form "f x = t".

  • New command 'fun_cases' derives ad-hoc elimination rules for
    function equations as simplified instances of f.elims, analogous to
    inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples.

Kind regards,
Christian, Florian, and René

signature.asc

Last updated: Nov 21 2024 at 12:39 UTC