Simplifier & meta All · Beginner Questions

Hi again! Can someone help me understand better how the simplifier uses quantified (meta or HOL) assumptions? I am looking at the following toy example:

schematic_goal foo: ‹(⋀x. P x y0) ⟹ P x0 ?y0›
  using [[simp_trace]]
  (* [1]Adding rewrite rule "??.unknown": P ?x2 y0 ≡ True  *)
  apply simp (* FAIL :-( *)
  oops

schematic_goal bar: ‹P ?x0 y0 ⟹ P x0 ?y0›
  by simp (* SUCCEED *)

I don't quite follow, since the simp trace output in the first schematic goal seems to suggest that even with P ?x2 y0 ≡ True, the simp attempt would fail, but this isn't the case as demonstrated by the second schematic goal.

Hanno Becker (Jun 06 2023 at 07:55):

Kevin Kappelmann (Jun 06 2023 at 07:59):

I do not know, but note that if you rewrite the second goal to match your insight from the first goal, it also won't finish:

schematic_goal bar: ‹P ?x0 y0 ≡ True ⟹ P x0 ?y0›
  using [[simp_trace]]
  by simp (* fails*)

Kevin Kappelmann (Jun 06 2023 at 08:01):

Might have something to do with the fact that the simplifier does not instantiate unknowns during rewrites, but the solver may instantiate unknowns. From the reference manual, page 229:
image.png

Hanno Becker (Jun 06 2023 at 08:21):

Kevin Kappelmann (Jun 06 2023 at 08:26):

lemma eq_True_eq_self: "((P :: bool) ≡ True) ≡ Trueprop P" by rule simp_all

ML ‹
  fun asm_solver ctxt =
    REPEAT_DETERM o (EqSubst.eqsubst_asm_tac ctxt [0] @{thms eq_True_eq_self})
    THEN' assume_tac ctxt
  fun add_asm_solver ctxt = ctxt addSolver Simplifier.mk_solver "asm_solver" asm_solver
›

schematic_goal ‹P ?x0 y0 ≡ True ⟹ P x0 ?y0›
  by (tactic ‹simp_tac @{context} 1›)
  oops

schematic_goal ‹P ?x0 y0 ≡ True ⟹ P x0 ?y0›
  by (tactic ‹simp_tac (add_asm_solver @{context}) 1›)

Hanno Becker (Jun 06 2023 at 08:28):

That would not yet solve the original goal, though, would it? Probably one should call eresolve on meta_allE as well?

Kevin Kappelmann (Jun 06 2023 at 08:40):

schematic_goal foo: ‹(⋀x. P x y0) ⟹ P x0 ?y0›
  using [[simp_trace]]
  by (tactic ‹simp_tac (add_asm_solver @{context}) 1›)

But I do not know why (maybe the simplifier already does some magic such that assume_tac works). But yeah, using meta_allE probably makes the solver more stable.

Hanno Becker (Jun 06 2023 at 08:42):

Interesting... maybe the solver also has access to the rewrite rules added by the simplifier

Hanno Becker (Jun 06 2023 at 08:54):

Hm, puzzling.. at least prems_of ctxt is empty by the time asm_solver is invoked

Stream: Beginner Questions

Topic: Simplifier & meta All

Hanno Becker (Jun 05 2023 at 06:24):