Email Gateway (Aug 22 2022 at 20:43): Email Gateway (Aug 22 2022 at 20:43):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle Users,
While using the simplifier to rewrite a cterm I encountered a subtle issue (described below).
I wonder if I have either encountered a bug in the simplifier or otherwise I was
breaking some assumptions / invariants on the relation of free variables in a term
vs. fixed variables in the context.
I did not find the answer in the implementation manual, hence my question here:
Are there any assumptions / invariants / (strong) guidelines on the usage of
free vs. fixed variables in the simplifier (or other proof tools in general) ?
I have rules in mind like:
Or is it the other way around and the responsibility of the proof tool to do a proper setup?
Here the issue I stumbled upon.
Simplifies to True as expected.
lemma "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1"
apply simp
done
Does not simplify to True
declare [[linarith_trace=true]]
ML_val ‹
val ct = @{cterm "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1"}
val test = Simplifier.asm_full_rewrite @{context} ct
›
Diagnoses with ‹linarith_trace› reveals that linarith accidently (re)uses variable name "a"
as "fresh" name for @{term "b 0"} which in turn makes the proof fail as it collides with the
already present free variable "a".
My guess (without inspecting the actual code) is, that linarith creates new variable names merely
refering to the context, e.g. with @{ML Variable.variant_fixes} without additionally considering the
free (and not fixed) variables in the present term, e.g. with @{ML Term.variant_frees}.
When fixing and declaring the variables it simplifies to True as expected.
ML_val ‹
val ctxt0 = @{context};
val ([b, a, n], ctxt1) = ctxt0 |> Variable.add_fixes ["b", "a", "n"];
val t = Syntax.read_term ctxt1 "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1";
val ctxt2 = ctxt1 |> Variable.declare_term t;
val ct = Thm.cterm_of ctxt2 t;
val test = Simplifier.asm_full_rewrite ctxt2 ct;
›
Actually, just declaring the term already has the desired effect.
ML_val ‹
val ctxt0 = @{context};
val t = Syntax.read_term ctxt0 "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1";
val ctxt1 = ctxt0 |> Variable.declare_term t;
val ct = Thm.cterm_of ctxt1 t;
val test = Simplifier.asm_full_rewrite ctxt1 ct;
›
Alternatively, setting the ‹body› flag in the context also has the desired effect.
ML_val ‹
val ct = @{cterm "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1"}
val test = Simplifier.asm_full_rewrite (Variable.set_body true @{context}) ct
›
Regards,
Norbert
Email Gateway (Aug 22 2022 at 20:43):From: Makarius <makarius@sketis.net>
I will look at your examples in detail later, but here are some abstract
notes.
Generally, you should make your formal items as official in the context
as possible: the minimum is a variant of Variable.declare_term, but it
is better to use Variable.add_fixes or similar to make it really right.
Sometimes the latter is not possible for historical reasons.
There are many intermediate situations for variables in the context, for
the sake of old tools that don't register properly in the context. It
would be better to be really strict about demanding everything to be
properly "fixed" in the context, but this will break some old tools.
Ah, and the word "bug" has not meaning in the Isabelle context:
everything is so complex that we can only talk about behaviour that is
expected / unexpected, simple / complex, desirable / undesirable,
changeable / unchangeable (for now).
The usual strategy of survival is to do things in a "canonical" way,
including certain context disciplines. (Example: normally you should
not change context flags like "is_body": that belongs to the system
infrastructure, not the user-space tools).
Makarius
Email Gateway (Aug 22 2022 at 20:48):From: Makarius <makarius@sketis.net>
On 09/10/2019 22:26, Norbert Schirmer via Cl-isabelle-users wrote:
Are there any assumptions / invariants / (strong) guidelines on the usage of
free vs. fixed variables in the simplifier (or other proof tools in general) ?
I have rules in mind like: * Fix every free variable in the context before calling a proof tool.
This should work, but it is not necessary in the strict sense.
- Always set the 'body' flag in the context before calling a proof tool.
Don't do this -- the flag is managed by the system infrastructure, not
user tools.
- Declare a term to the context before calling a proof tool.
Always do that, explicitly or implicitly via other operations that
ensure that terms become "part of the context" in the proper way. This
is avtually the main conclusion of this thread.
Does not simplify to True
declare [[linarith_trace=true]]
ML_val ‹
val ct = @{cterm "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1"}
val test = Simplifier.asm_full_rewrite @{context} ct
›Diagnoses with ‹linarith_trace› reveals that linarith accidently (re)uses variable name "a"
as "fresh" name for @{term "b 0"} which in turn makes the proof fail as it collides with the
already present free variable "a".My guess (without inspecting the actual code) is, that linarith creates new variable names merely
refering to the context, e.g. with @{ML Variable.variant_fixes} without additionally considering the
free (and not fixed) variables in the present term, e.g. with @{ML Term.variant_frees}.
The "refering to the context" to create new variables is correct. The
"merely" wording reveals a wrong (outdated) understanding how things
work. All terms participating in manipulations by proof tools need to be
formally part of the context. It is neither efficient nor sufficient to
re-inspect e.g. a goal state -- like was done routinely many years.
Actually, just declaring the term already has the desired effect.
ML_val ‹
val ctxt0 = @{context};
val t = Syntax.read_term ctxt0 "b (0::nat) + (a::int) ≤ n ⟹ b 0 + a ≤ n + 1";
val ctxt1 = ctxt0 |> Variable.declare_term t;
val ct = Thm.cterm_of ctxt1 t;
val test = Simplifier.asm_full_rewrite ctxt1 ct;
›
That is the standard approach, but note that the Syntax.read_term
invocation is only correct by accident in this example. In general the
local variables a, b would have to be somehow reserved in the context
beforehand, e.g. via Variable.add_fixes. Some newer tools also have a
convenient 'for' notation for that (e.g. proof method "ind_cases" in
Isabelle/HOL). You probably won't need that technique right now, but
knowing it in advance can avoid many old problems from 20 years ago.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC