Email Gateway (Aug 19 2022 at 15:15): Email Gateway (Aug 19 2022 at 15:15):From: René Neumann <rene.neumann@in.tum.de>
Hi,
I just noticed, that for a goal like
[| ...; it ⊆ S; ... |] ==> (?it it a b c) ⊆ S
force unifies "?it it a b c" with {} -- and not with 'it' as one would
expect.
I suspect, that it first tries to apply intro! rules before looking at
the assumptions. Is this the intended behavior? Or is it due to
something completely different?
A simply DIY-example:
schematic_lemma
"it ⊆ S ==> ?it ⊆ S"
by force
This results in "S ⊆ S"...
P.S.: This mattered to me, because it was part of an 'apply force+'
which then instantiated '?it' wrong...
smime.p7s
Email Gateway (Aug 19 2022 at 15:15):From: Lawrence Paulson <lp15@cam.ac.uk>
There is no right or wrong here. In the context of a broader proof search and a goal free of logical variables, backtracking should ultimately find a proof if one exists. But with logical variables in the goal, you could get anything. I would need to look at the code to see which one is preferred.
Larry Paulson
Last updated: Apr 25 2024 at 16:19 UTC