Email Gateway (Aug 22 2022 at 10:58): Email Gateway (Aug 22 2022 at 10:58):From: noam neer <noamneer@gmail.com>
in the following simple (and artificial) example, the proof of lemma 'tl2'
fails at its firsy 'apply'. it seems the simplifier couldn't apply lemma
'tl1' at all, even though a proof with 'rule' instead of 'simp' does work.
can anyone explain this to me?
theory tmp_prop
imports Complex_Main
begin
definition fff :: "real ⇒ real ⇒ real"
where "fff x y = 0"
lemma tl1: "x≠0 ==> (fff x y) = 0"
by (simp add: fff_def)
lemma tl2: "x≠0 ==> (fff x y) = 0"
using [[simp_trace]]
apply (simp only: tl1 [of x y])
oops
(* a proof that does work -
apply (rule tl1 [of x y])
apply simp
*)
end
Email Gateway (Aug 22 2022 at 10:59):From: Manuel Eberl <eberlm@in.tum.de>
The problem has to do with how the simplifier turns facts into simp rules.
In your example, you have the fact "x ≠ 0", and the simplifier turns
that into the simp rule "(x = 0) = False". In order to apply the rule
tl1[of x y] that you added as a simp rule, the simplifier has to solve
the precondition "x ≠ 0".
What happens is that this precondition gets rewritten with the above
simp rule, so you end up with "¬False" and then the simplifier gets
stuck because you used "simp only:" and therefore have no simp rules for
something like "¬False".
If you do "apply (simp only: not_False_eq_True tl1[of x y])", everything
works out fine.
Email Gateway (Aug 22 2022 at 10:59):From: Lars Noschinski <noschinl@in.tum.de>
Manuel already gave an answer. I guess you arrived at that by
investigating some behaviour you did not understand. In such cases, the
use of "simp_thms" with "simp only:" can be useful -- it contains all
the basic logic rules you expect the simplifier to know..
Email Gateway (Aug 22 2022 at 10:59):From: noam neer <noamneer@gmail.com>
thanx for the answers. but I just tried the same proof with
apply (simp (no_asm_simp) only: tl1 [of x y])
if Manuel's explanation is correct this should have worked,
because the "x~=0" should have stayed unchanged.
but this fails too. what am I missing?
Email Gateway (Aug 22 2022 at 10:59):From: Lars Noschinski <noschinl@in.tum.de>
The simplifier can only work with (conditional equations) of the form
"[|_|] ==> _ == _". Anything, which does not have this form is converted
first. This includes steps as
x = y ----> x == y
~P ----> P == False
P ----> P == True
This behaviour is hard-coded for each logic and cannot be disabled.
-- Lars
Email Gateway (Aug 22 2022 at 11:01):From: noam neer <noamneer@gmail.com>
OK. but now I tried a different condition -
lemma tl3: "x>1 ==> (fff x y) = 0"
using [[simp_trace]]
using [[simp_trace_depth_limit=2]]
apply (simp (no_asm_simp) only: tl1 [of x y])
done
the proof worked though I don't understand why.
here the simplifier has to prove "x~=0" from "x>1",
and from the trace output it seems he adds many rules
that enable him to prove this. why is he adding them?
is this the lin arith module at work?
and another question - was there an attempt to add backtracking abilities
to the simplifier, like in 'blast'? seems it'd be usefull.
thanx
Email Gateway (Aug 22 2022 at 11:02):From: Thomas Sewell <thomas.sewell@nicta.com.au>
You are right, there is something pretty strange going on here. The
'only:' mode of simp is meant to turn off anything that might surprise you.
In general the simplifier trace can be quite confusing, because the
simplifier sometimes runs simprocs and other tools which then call back
to the simplifier. The tracing mode is set globally, so you see an inner
trace mixed into your trace which explains what happened on the
recursive call.
It looks like this is what happens here. Unfortunately the simp trace
isn't detailed enough to figure out what the tool that is working here
is, or how it got called.
OK, so, from my quick reading, "simp only:" calls
Raw_Simplifier.clear_simpset, which drops the rules, congs, procs, etc,
but keeps the mksimps mechanism, the term order, subgoal tactic and
"solvers".
Indeed, lin_arith is added as a "solver" (see "addSolver" in
global_setup in src/HOL/Tools/lin_arith.ML). And solvers are not removed
by the "simp only:" command. You could do some ML work to force the
non-default solvers out of the simpset, which would make the simplifier
a bit more predictable. Or just accept that it's a bit of a headache.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 24 2024 at 04:17 UTC