Lukas Stevens (Aug 06 2020 at 15:28): 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?
Manuel Eberl (Aug 06 2020 at 15:32):Hm, Simplifier.prems_of gives you the premises that are in the simpset.
Manuel Eberl (Aug 06 2020 at 15:32):I'm… not entirely sure which premises end up there and when.
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?
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.
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.
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.
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.
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?
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
Still weird, since one would expect that those premises are already part of the goal when the solver is called.
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.
Lukas Stevens (Aug 06 2020 at 15:45):Ok, then it makes sense to consider the Simplifier prems as well.
Manuel Eberl (Aug 06 2020 at 15:50):This is just a guess.
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
(Look at the output after those "simp?" commands)
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:
Manuel Eberl (Aug 06 2020 at 16:15):What did the old solver do?
Manuel Eberl (Aug 06 2020 at 16:15):The old linarith solver I mean.
Lukas Stevens (Aug 06 2020 at 16:18):It is the old order solver. It decides the theory of partial and linear orders.
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:
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?
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?
Lukas Stevens (Aug 06 2020 at 16:44):The old one also added those premises. I carelessly deleted that bit apparently.
Last updated: Apr 19 2024 at 08:19 UTC