Stream: General

Topic: Simplifier.prems_of


view this post on Zulip Lukas Stevens (Aug 06 2020 at 15:28):

Does anybody know what Simplifier.prems_of really does? Is it equivalent to the prems I would get from Subgoal.FOCUS?

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:32):

Hm, Simplifier.prems_of gives you the premises that are in the simpset.

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:32):

I'm… not entirely sure which premises end up there and when.

view this post on Zulip Lukas Stevens (Aug 06 2020 at 15:33):

I see. Is it better to insert those as premises before calling Subgoal.FOCUS or should I just append those to the premises that I get from Subgoal.FOCUS?

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:34):

My guess would be that when the Simplifier simplifies e.g. an implication P ==> Q, it will add P as a premise when simplifying Q.

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:35):

So when you do Simplifier.prems_of outside the context of a simplifier run, you will probably get an empty list.

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:35):

Lukas Stevens said:

I see. Is it better to insert those as premises before calling Subgoal.FOCUS or should I just append those to the premises that I get from Subgoal.FOCUS?

I don't really understand what you are trying to achieve.

view this post on Zulip Lukas Stevens (Aug 06 2020 at 15:36):

In my case, I am registering the tactic as a solver. I appended the Simplifier.prems_of and now some proofs work that previously failed. I am not really sure what the semantics of a solver are, i.e. when it is called and what the context is.

view this post on Zulip Lukas Stevens (Aug 06 2020 at 15:36):

Manuel Eberl said:

Lukas Stevens said:

I see. Is it better to insert those as premises before calling Subgoal.FOCUS or should I just append those to the premises that I get from Subgoal.FOCUS?

I don't really understand what you are trying to achieve.

It seems that I need those premises such that the tactic works as a solver?

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:38):

It seems I was right:

consts P :: "'a ⇒ bool"

simproc_setup foo ("P x") = 
fn _ => fn ctxt => fn _ => let val _ = @{print} (Simplifier.prems_of ctxt) in NONE end


lemma "P x"
  apply simp? (* no premises *)
  oops

lemma "Q ⟹ P x"
  apply simp? (* premises: [Q] *)
  oops

lemma "⋀y. Q y ⟹ P x"
  apply simp? (* premises: [Q :000] *)
  oops

view this post on Zulip Lukas Stevens (Aug 06 2020 at 15:40):

Still weird, since one would expect that those premises are already part of the goal when the solver is called.

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:43):

My expectation would be the following: the solver is called on the entire goal when everything else has failed (except maybe before the loopers; I can never remember the order). Since it works on the entire goal, there are probably no premises. However, the simplifier is also used recursively to solve preconditions of conditional rewrite rules, and if the solver is called for one of those, there might be premises in the context.

view this post on Zulip Lukas Stevens (Aug 06 2020 at 15:45):

Ok, then it makes sense to consider the Simplifier prems as well.

view this post on Zulip Manuel Eberl (Aug 06 2020 at 15:50):

This is just a guess.

view this post on Zulip Manuel Eberl (Aug 06 2020 at 16:02):

Looks like I guessed correctly. Perhaps this snippet is illuminating to you:

consts
  P :: "'a ⇒ bool"
  Q :: "'a ⇒ bool"
  P' :: "'a ⇒ bool"

lemma [simp]: "Q x ⟹ P x = P' x"
  sorry

setup map_theory_simpset (fn ctxt =>
let
  val solver =
    Simplifier.mk_solver "foo"
      (fn ctxt => fn i => fn thm =>
        let
          val _ = Pretty.writeln (Pretty.str " ")
          val _ = @{print} "SOLVER INVOCATION"
          val _ = Pretty.writeln (Pretty.block (Pretty.str "Premises: " ::
                    map (Syntax.pretty_term ctxt o Thm.prop_of) (Simplifier.prems_of ctxt)))
          val _ = Pretty.writeln (Pretty.block [Pretty.str "Goal: ", Syntax.pretty_term ctxt (Thm.concl_of thm)])
          val _ = @{print} "END SOLVER INVOCATION"
        in
          Seq.empty
        end)
in
  ctxt addSolver solver
end)


lemma "P x"
  apply simp?
  oops

lemma "R ⟹ P x"
  apply simp?
  oops

lemma "⋀y. R y ⟹ P x"
  apply simp?
  oops

view this post on Zulip Manuel Eberl (Aug 06 2020 at 16:03):

(Look at the output after those "simp?" commands)

view this post on Zulip Lukas Stevens (Aug 06 2020 at 16:14):

Thank you, I will have a look at it. The solver now works for all of Main at least :party_ball:

view this post on Zulip Manuel Eberl (Aug 06 2020 at 16:15):

What did the old solver do?

view this post on Zulip Manuel Eberl (Aug 06 2020 at 16:15):

The old linarith solver I mean.

view this post on Zulip Lukas Stevens (Aug 06 2020 at 16:18):

It is the old order solver. It decides the theory of partial and linear orders.

view this post on Zulip Lukas Stevens (Aug 06 2020 at 16:20):

The new solver is a bit more powerful in the theory of partial orders. While the core is verified it is quite hard to get the glue code right :sweat_smile:

view this post on Zulip Manuel Eberl (Aug 06 2020 at 16:41):

Then I don't understand. If we're talking about the old solver, then why do things suddenly not work anymore?

view this post on Zulip Manuel Eberl (Aug 06 2020 at 16:42):

Or if we are talking about your new one after all, my question was: how does the old one treat premises?

view this post on Zulip Lukas Stevens (Aug 06 2020 at 16:44):

The old one also added those premises. I carelessly deleted that bit apparently.


Last updated: Aug 15 2022 at 02:13 UTC