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



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




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