Email Gateway (Feb 14 2021 at 15:45): Email Gateway (Feb 14 2021 at 15:45):From: Peter Lammich <lammich@in.tum.de>
Hi List,
in my current formalization, I frequently end up with goals that I feel
should be solvable by auto or blast, but they get stuck due to
containing a precondition similar to this:
(∀a. (∃x y. a = f x y ∧ P x y) ⟶ Q a)
The exact precondition can vary in the number of universal and
existential quantified variables, and the position and number of the
determining a = ... conjuncts, e.g.
(∀a b. (∃x y. a = f x y ∧ P x y ∧ b=g x) ⟶ Q a b)
Anyway, the above preconditions are, obviously, equal to the following
simpler ones:
"∀x y. P x y ⟶ Q (f x y)"
"∀x y. P x y ⟶ Q (f x y) (g x)"
currently, I have to manually prove these equivalences, for every
instance of quantified variables, etc, and then can solve the goal
easily by rewriting and auto.
Is there any way, e.g. a simproc or so, to automate this process, or is
my only solution to bloat up the otherwise fully automatic proofs by
those weird auxiliary lemmas (of which I could, of course, prove
instances for the most common cases globally and add them to the
simpset)
Email Gateway (Feb 14 2021 at 17:58):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Peter,
I don't think there is any automation for this. I automated "(∀x. x = t --> P x)
= P t" and variations on this, but without nested quantifiers. I am sure the
latter could be added and it would be worth it, but somebody would need to do
it. I am happy to provide pointers...
Tobias
smime.p7s
Email Gateway (Feb 15 2021 at 10:16):From: Thomas Sewell <tals4@cam.ac.uk>
You can pull the existentials up so that there are only foralls using
the symmetric versions of the all_simps rewrites.
Try out
apply (simp only: all_simps[symmetric] cong: imp_cong)
I'm not sure how consistently that will work, but that followed by
regular simplification got me the expected result in all the simple
test cases I typed.
BTW, I have a dim recollection that I used to see goals like this more
often. The "a = .." and "b = .." looks like it came from "(a, b)" being
in the image of some projection, maybe. I think I managed to get more
image/map type constructions to simplify a bit before quantifiers
appeared.
Best regards,
Thomas.
Email Gateway (Feb 15 2021 at 10:36):From: Lawrence Paulson <lp15@cam.ac.uk>
Try this:
apply (simp flip: ex_simps all_simps)
Your example is a rare case in which prenexing is actually a good idea.
Larry
Email Gateway (Feb 16 2021 at 12:27):From: Peter Lammich <lammich@in.tum.de>
Thanks Larry and Thomas, that works a treat for my examples!
Last updated: Jan 04 2025 at 20:18 UTC