[isabelle] Invariants on free vs. fixed variables in simplifier / proof tools



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:
* Fix every free variable in the context before calling a proof tool.
* Always set the 'body' flag in the context before calling a proof tool.
* Declare a term to the context before calling a proof tool.

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

--

Norbert Schirmer (nschirmer at apple.com <mailto:nschirmer at apple.com>)
 SEG Formal Verification





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.