Email Gateway (Aug 22 2022 at 15:17): Email Gateway (Aug 22 2022 at 15:17):From: Lars Hupel <hupel@in.tum.de>
Dear list,
let's say I have a goal state that looks like this:
1. (⋀x. P x)
2. (⋀x. Q x)
I want to perform mutual induction on "P" and "Q". To use the "induct"
tactic effectively I need to obtain a goal state more like this:
1. ⋀x y. P x &&& Q y
That is, quantification is outside. Then, I can use the usual mechanisms
("Subgoal.FOCUS_PARAMS") to set up a local context, which makes my goal
state look like this:
1. P :000 &&& Q :001
... which in turn can be fed to "induct".
I currently have a solution which goes from my initial goal state to the
desired goal state by applying these rewrite rules:
⋀P Q. ((⋀x. PROP P x) &&& PROP Q) ≡ (⋀x. PROP P x &&& PROP Q)
⋀P Q. (PROP P &&& (⋀x. PROP Q x)) ≡ (⋀x. PROP P &&& PROP Q x)
Is there anything out there that already does what I want?
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:17):From: Makarius <makarius@sketis.net>
On 21/03/17 15:47, Lars Hupel wrote:
let's say I have a goal state that looks like this:
1. (⋀x. P x)
2. (⋀x. Q x)I want to perform mutual induction on "P" and "Q". To use the "induct"
tactic effectively I need to obtain a goal state more like this:1. ⋀x y. P x &&& Q y
You did not say how you got there. Note that
Goal.recover_conjunction_tac happens to be available for this, because
it is occasionally needed in obscure situations.
That is, quantification is outside. Then, I can use the usual mechanisms
("Subgoal.FOCUS_PARAMS") to set up a local context, which makes my goal
state look like this:1. P :000 &&& Q :001
... which in turn can be fed to "induct".
I currently have a solution which goes from my initial goal state to the
desired goal state by applying these rewrite rules:⋀P Q. ((⋀x. PROP P x) &&& PROP Q) ≡ (⋀x. PROP P x &&& PROP Q)
⋀P Q. (PROP P &&& (⋀x. PROP Q x)) ≡ (⋀x. PROP P &&& PROP Q x)Is there anything out there that already does what I want?
The last two rewrite rules look OK for such special rearrangements. E.g.
when wrapped-up into a separate proof method.
There are very few such tools to operate in Pure rule or goal structure,
because the usual Isar way is to operate on the problem structure as
provided by the user, and avoid loosing that structure in the first place.
Sometimes that is difficult or impossible, then special tweaks need to
be applied. So looking from a distance, the canonical question is: Where
does the situation of two separate subgoals with separate parameter
scopes come from? Is that the result of another tool?
Makarius
Email Gateway (Aug 22 2022 at 15:17):From: Lars Hupel <hupel@in.tum.de>
This particular goal state arises in a tool. In a nutshell, I start with
"Goal.prove_common" and supply multiple propositions (let's say "P" and
"Q"). Then, I need to preprocess these propositions (let's say some
extensionality rule) so that I can apply induction. Hence, I need to
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC