Email Gateway (Aug 22 2022 at 21:09): Email Gateway (Aug 22 2022 at 21:09):From: Tobias Nipkow <nipkow@in.tum.de>
A student of mine has a problem with the following setup:
ML‹
val focus_tac = Subgoal.FOCUS (K no_tac)
›
setup ‹
map_theory_simpset (fn ctxt => ctxt
addSolver (mk_solver "focus_solver" focus_tac))
›
In some cases this raises the error "Duplicate fixed variable(s)". Here is an
example from the Multiset theory:
This works:
size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq]
but creates a thm with both ?x and a bound x. Applying the simplified attribute
with the above setup raises "Duplicate fixed variable(s): x":
size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
Any help is appreciated.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 21:10):From: "Jackson, Vincent (Data61, Kensington NSW)" <Vincent.Jackson@data61.csiro.au>
Ah, this reminds me of a problem I ran into a while ago.
The following produces the wonderfully helpful error Duplicate fixed variable(s): "".
ML ‹
@{cterm "⋀a. x + (f x) ≤ y ∧ a = x + (if x = 0 then 1 else Suc y) div 2"}
|> Goal.init
|> Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} => simp_tac ctxt 1)
(Simplifier.add_cong @{thm HOL.conj_cong} @{context}) 1
|> Seq.hd
›
There seems to be some interaction between simp and cong rules which causes this sort of problem. Replacing Simplifier.add_cong @{thm HOL.conj_cong} @{context} with @{context} prevents the error from occuring.
Unfortunately, I can't offer a solution, but if anyone has a resolution to this problem, it would also be helpful to me.
Thanks,
Vincent
Vincent Jackson
Proof Engineer | Trustworthy Systems
CSIRO's Data61
E Vincent.Jackson@data61.csiro.au<mailto:Vincent.Jackson@data61.csiro.au>
1466 UNSW Sydney, NSW, Australia
www.data61.csiro.au
Email Gateway (Aug 22 2022 at 21:10):From: Makarius <makarius@sketis.net>
Proof tools often implicitly assume a proper goal context, but here
"simplified" operates in a global theory. The example can be made work like this:
theory Scratch
imports Main "HOL-Library.Multiset"
begin
ML ‹
fun focus_tac ctxt =
Subgoal.FOCUS (K no_tac) ctxt;
›
setup ‹
map_theory_simpset (fn ctxt => ctxt
addSolver (mk_solver "focus_solver" focus_tac))
›
notepad
begin
thm size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq,
simplified]
end
Here the notepad provides a proper proof body. In ML the same effect can be
achieved like this:
ML ‹
val ctxt = \<^context>;
val thm = @{thm size_multiset_overloaded_def[THEN fun_cong, unfolded
size_multiset_eq]};
Simplifier.asm_full_simplify (Variable.set_body true ctxt) thm;
›
Alternatively, focus_tac can be made more robust like this:
ML ‹
fun focus_tac ctxt =
Subgoal.FOCUS (K no_tac) (Variable.set_body true ctxt);
›
(Normally proof tools should not have to change context flags like that.)
The deeper reason why the Simplifier is a bit unfriendly here: it pretends to
be a plain inference rule, but uses tactical reasoning internally (e.g. the
solver). I will see if its builtin policies can be changed to avoid such
surprises.
Makarius
Email Gateway (Aug 22 2022 at 21:10):From: Makarius <makarius@sketis.net>
This example contains directly visible programming mistakes concerning the
context discipline:
* Tactical reasoning always requires a proper goal context (not a global
theory context like @{context} of the above ML command).
* Goal statements need to be properly declared to the context.
Here is a more standard approach:
theory Scratch
imports Main
begin
ML ‹
val ctxt = @{context};
val ct = @{cterm ‹⋀a. x + (f x) ≤ y ∧ a = x + (if x = 0 then 1 else Suc y)
div 2›};
val goal_ctxt = ctxt
|> Variable.set_body true
|> Variable.declare_term (Thm.term_of ct);
Goal.init ct
|> Subgoal.FOCUS_PARAMS (fn {context = focus_ctxt, ...} => simp_tac
focus_ctxt 1)
(Simplifier.add_cong @{thm HOL.conj_cong} goal_ctxt) 1
|> Seq.hd;
›
end
Of course, Goal.init / Seq.hd is a fairly low-level way to work with tactics:
Goal.prove provides the template for the full setup, including Goal.init,
Variable.set_body trueVariable.declare_term.
Further stylistic notes on the modified example snippet:
* The static antiquotations @{context} and @{cterm} are only used in the
"prelude", not the ML body text. Thus it is possible to turn a successful
experiment into a function on ctxt and ct, without referring to inlined
compile-time values by accident.
* ML bindings like "ctxt" should never be re-used in local scopes: abive I
have taken the care to be clear about ctxt, goal_ctxt, focus_ctxt. Unlike
IntelliJ IDEA, our Isabelle/ML does not warn about "suspicious" rebindings
like "val ctxt = f ctxt", but Isabelle/jEdit can help to clean up odd sources
that use that style reliably.
Makarius
Email Gateway (Aug 22 2022 at 21:10):From: Makarius <makarius@sketis.net>
There is now the following minimal change to make the internal tactical
reasoning more robust in this respect:
https://isabelle.in.tum.de/repos/isabelle/rev/1be996d8bb98
That is for the next release, presumably Isabelle2020 (June 2020). There are
further related changes already present and potentially still coming. Any
discussions about such ongoing development may happen on isabelle-dev as usual.
Generally, projects with Isabelle should use the official release, and live
with such small workarounds as above. There is nothing strictly wrong here,
just a small inconvenience.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC