*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Invariants on free vs. fixed variables in simplifier / proof tools*From*: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Wed, 09 Oct 2019 22:26:41 +0200*Cc*: Sebastian Skalberg <skalberg at apple.com>*Reply-to*: Norbert Schirmer <nschirmer at apple.com>

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

**Follow-Ups**:

- Previous by Date: [isabelle] Shortcut to go to definition
- Next by Date: Re: [isabelle] Invariants on free vs. fixed variables in simplifier / proof tools
- Previous by Thread: [isabelle] Shortcut to go to definition
- Next by Thread: Re: [isabelle] Invariants on free vs. fixed variables in simplifier / proof tools
- Cl-isabelle-users October 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list