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 On 14/02/2021 16:44, Peter Lammich wrote:
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) -- Peter
Description: S/MIME Cryptographic Signature