Does anybody know what Simplifier.prems_of really does? Is it equivalent to the prems I would get from Subgoal.FOCUS?
Hm, Simplifier.prems_of
gives you the premises that are in the simpset.
I'm… not entirely sure which premises end up there and when.
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?
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
.
So when you do Simplifier.prems_of
outside the context of a simplifier run, you will probably get an empty list.
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.
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.
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?
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.
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.
Ok, then it makes sense to consider the Simplifier prems as well.
This is just a guess.
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)
Thank you, I will have a look at it. The solver now works for all of Main at least :party_ball:
What did the old solver do?
The old linarith solver I mean.
It is the old order solver. It decides the theory of partial and linear orders.
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:
Then I don't understand. If we're talking about the old solver, then why do things suddenly not work anymore?
Or if we are talking about your new one after all, my question was: how does the old one treat premises?
The old one also added those premises. I carelessly deleted that bit apparently.
Last updated: Oct 12 2024 at 20:18 UTC