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)

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

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.

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

From: Peter Lammich <lammich@in.tum.de>

Thanks Larry and Thomas, that works a treat for my examples!

Last updated: Jul 15 2022 at 23:21 UTC