Email Gateway (Aug 22 2022 at 20:47): Email Gateway (Aug 22 2022 at 20:47):From: Christoph Madlener <madlener@in.tum.de>
Hello,
I am writing some simprocs and encountered a problem when using
simproc_setup to install them. As you can see in the attached example,
when multiple patterns for the simproc contain the same variable, the
simproc isn't triggered for any of the given patterns. (I also
encountered a case where the simproc was triggered for some, but not all
given patterns)
The problem can be avoided by either using unique identifiers, calling
simproc_setup multiple times or using Simplifier.make_simproc - note
that for the latter the patterns work as expected. I also attached an
example with working solutions.
Best regards,
Christoph
Simproc_Match_Not_Working.thy
Simproc_Match_Working.thy
Email Gateway (Aug 22 2022 at 20:47):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Christoph,
The problem is type inference. With ("prod f A" | "sum f B"), f gets the
type 'a::type ⇒ 'b::{comm_monoid_add,comm_monoid_mult}. However, in your
lemmas, you get only either comm_monoid_add or comm_monoid_mult but not
both. If you force the types to have both:
lemma "(\<Sum>i=1..3. i) = (\<Sum>i=0..2. (i ::
'b::{zero,numeral,ord,comm_monoid_add,comm_monoid_mult}) + 1)"
then the simproc triggers. The reason why [\<^term>\<open>prod f A\<close>,
\<^term>\<open>sum f A\<close>] works is that the type inference is done
separately in the two expressions instead of being done together.
Best regards,
Mathias
Le jeu. 24 oct. 2019 à 09:30, Christoph Madlener <madlener@in.tum.de> a
écrit :
Email Gateway (Aug 22 2022 at 20:47):From: Tobias Nipkow <nipkow@in.tum.de>
This raises the question why type inference is applied to two alternative
patterns simultaneously. Function definitions (fun in Isabelle) don't do that
and it would be better if the simproc setup didn't do it either.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 20:47):From: "lammich@in.tum.de" <lammich@in.tum.de>
Another common beginner's trap is the simultaneous type inference on lemmas.
At some point, you write down a list of statements in a single lemma. This
perfectly makes sense if the statements are related and are proved with the
same by (auto...) method. However it is all too easy to have such lemmas a
less general type than intended, due to all statements being typed
simultaneously. I still run into this trap occasionally...
Peter
Email Gateway (Aug 22 2022 at 20:47):From: Christoph Madlener <madlener@in.tum.de>
Ok, thank you all for your replies. I see what is happening now. I'm
just asking myself if this behavior is intended or "just came to be"?
What I can say though is that it obviously wasn't the behavior I was
expecting and as far as I can tell it is also not documented (although
I'm
also not sure what a good place for this information would be).
Email Gateway (Aug 22 2022 at 20:48):From: Makarius <makarius@sketis.net>
Type inference is very useful, but there are sometimes situations where
users get confused (very rarely). Luckily this is a non-issue today with
the Isabelle Prover IDE: CTRL-hover tells you about inferred types.
These are the traditional guidelines to isolate problems in
specifications and implementations.
If something does not work unexpectedly:
(a) Inferred types might be more general or more special than expected.
(b) The context might be wrong.
The latter refers to type Proof.context in Isabelle/ML.
Makarius
Email Gateway (Aug 22 2022 at 20:48):From: Manuel Eberl <eberlm@in.tum.de>
Dear Makarius,
I don't really undestand what you're trying to say.
The question at hand is: Is the behaviour of simproc_setup here (type
checking all the different patterns simultaneously, in the same context)
what it is supposed to do or not?
I would argue that this is very much /not/ what it is supposed to do and
that every pattern should fix variables and be type-checked
independently. The patterns are independent of one another – why should
they have a shared name space?
What is your opinion?
Manuel
Email Gateway (Aug 22 2022 at 20:48):From: Makarius <makarius@sketis.net>
The default answer: by default the behaviour of the system is correct
and as intended. There can be nonetheless situations of user confusion:
the system provides tools to work that out, notably for type-inference.
'simproc_setup' might be an odd corner case from the past -- I can't say
on the spot, but 10min of inspecting of the sources and the history
don't show any irregularities so far.
Generally, it is a bad idea to change established behaviour on the spot,
just because the true reasons for it are forgotten, or take a long time
to investigate. The Isabelle jargon for that is "brownian motion":
something could be done like this or like that, and there is no clear
indication for either side. Adhoc changes would make it oscilate back
and forth over time, and break other applications for no particular reason.
Makarius
Email Gateway (Aug 22 2022 at 20:48):From: Tobias Nipkow <nipkow@in.tum.de>
This question is not specific to Isabelle but overlaps with functional
programming in general and should have an abstract answer. As I mentioned, the
"fun" command typechecks equations separately, and not because this is Isabelle
but because this is the standard in functional programming (for good reasons).
Thus I had concluded that simproc_setup should behave the same. But the issue is
more subtle. The simproc patterns do not guard different equations but one and
the same object, the function definition. Hence they are akin to "disjunctive
patterns" in OCaml. Type inference for disjunctive patterns is simultaneous,
again for good reasons, because the variables are used in the single body that
follows the patterns. But patterns in simprocs are again slightly different in
that the variables are never used and thus there is no need for simultaneous
type inference.
My conclusion is that simproc_patterns are different enough from normal and from
disjunctive patterns that there is no abstract argument that they should behave
like either.
In the absence of a strong abstract argument, I would indeed leave things as
they are.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 20:48):From: Makarius <makarius@sketis.net>
On 25/10/2019 12:31, Tobias Nipkow wrote:
This question is not specific to Isabelle but overlaps with functional
programming in general and should have an abstract answer. As I
mentioned, the "fun" command typechecks equations separately, and not
because this is Isabelle but because this is the standard in functional
programming (for good reasons). Thus I had concluded that simproc_setup
should behave the same. But the issue is more subtle. The simproc
patterns do not guard different equations but one and the same object,
the function definition. Hence they are akin to "disjunctive patterns"
in OCaml. Type inference for disjunctive patterns is simultaneous, again
for good reasons, because the variables are used in the single body that
follows the patterns. But patterns in simprocs are again slightly
different in that the variables are never used and thus there is no need
for simultaneous type inference.
These are good observations, and hint at various possibilities of the
design space (also going back to approx. 2007).
The implementation in terms of existing Isabelle concepts is another
issue: when we started to support separate variable scopes as in
'function' or 'inductive', it was a genuine feature addition that
required approx. 10 years to get properly implemented. As a consequence
of recent consolidation, the PIDE markup informs the user about the
difference: blue variables for a simultaneous global scope (e.g.
'simproc_setup') vs. green variables for local bindings with independent
type inference (e.g. in 'function'). Note that "blue" could also mean
"legacy variable treatment, without proper scoping". Moreover, blue
variables still lack the scope-group markup for PIDE.
Generally, I find our situation of scopes and type inference less
confusing than e.g. in Scala. In any case, when I use one of these
rather complex languages (Scala, TypeScript, Haskell etc.) I always rely
on the IDE to tell me what has been worked out by the system.
My conclusion is that simproc_patterns are different enough from normal
and from disjunctive patterns that there is no abstract argument that
they should behave like either.In the absence of a strong abstract argument, I would indeed leave
things as they are.
I do agree with the conclusion.
Makarius
Email Gateway (Aug 22 2022 at 20:48):From: Makarius <makarius@sketis.net>
The "list of statements" is actually just a single big statement of the
general form:
lemma
fixes xs
assumes a: As and b: Bs
shows c: Cs and d: Ds
where everything is simultaneously inferred -- without that there would
be a lot of confusion in applications, as empirically proven 20 years ago.
A special case is the following multi-conclusion statement:
lemma c: Cs and d: Ds
That is still a single lemma, not multiple ones. The concept of such
simultanous facts stems from 'assume' and 'have' in Isar, which mostly
behave the same way.
By explaining complex statements properly, user confusion can be
minimized. An alternative is to teach users early on to rely on the
Prover IDE for the details.
Makarius
Last updated: Apr 27 2024 at 04:17 UTC