I can easily prove this goal
schematic_goal "⋀x. P x ⟹ P ?x"
by (rule someI)
I can also prove
schematic_goal "⋀x y. P x y ⟹ P ?x ?y"
using for example
"P x y ⟹ P (fst (Eps (λ(x, y). P x y))) (snd (Eps (λ(x, y). P x y)))"
But what do I do for the following?
schematic_goal "⋀x y. P x y ⟹ P ?x y"
For, I assume technical, reasons that I don't quite understand
?x can't be instantiated with
x in all these cases, which is why I have to resort to
Eps. In the last case I'd have to instantiate
?x with something that doesn't depend on
y, but I in general no value for
?x has to exist that satisfies
P x y for all
Do your really mean
(⋀x y. P x y) ⟹ P ?x ?y?
that is also the reason why
x cannot be instantiated with
x: they don't live in the same scope…
schematic_goal "(P x y ⟹ P ?x y)" by assumption
Are you saying that
⋀x y. P x y ⟹ P ?x ?y is the same as
(⋀x y. P x y) ⟹ P ?x ?y because it really doesn't seem like it from the syntax highlighting in jedit. Also,
⋀x y. (P x y ⟹ P ?x ?y) still doesn't work
oh no sorry you are right
⋀x y. (P x y ⟹ P ?x ?y) : this is a scope problem: you are trying to instantiate the global variable
?x with a local variable that only exists under
this is also why you don't have that problem with the
P x y ⟹ P ?x ?y: you instantiate the global variable with a global variable
Yeah, that's why I have to come up with a constant through
Eps and why the following works, where I make
?x explicitly dependent on the local
schematic_goal "(⋀x y. P x y ⟹ P (?x x) y)" by assumption
I have some cases in "real code" where I have schematics in the conclusion like
P ?x from a rule application and a premise like
∃x. P x, which introduces a new local when I eliminate the quantifier which then can't be used to instantiate
?x. Sometimes I can mitigate this by eliminating the
∃x before applying the rule. But doing this automatically early enough is extremely hard.
⋀x y. P x y ⟹ P ?x y is the situation I encounter, that's why I'm asking about it.
As far as I understand this is an entirely technical problem, not a logical one, because
lemma "⋀x. P x" is equivalent to
lemma "P x". So I was hoping to find a solution to turn
⋀x y. P x y ⟹ P ?x y into
P x y ⟹ P ?x y or some solution involving the choice operator.
can't you just change your theorem to require
\<exists>x. P x y?
It creates multiple new goals containing the schematic variable
I meant: changing the location where you actually need that theorem
because I have a hard time imagining where you could need such a theorem
After some consideration I think you're right. This issue doesn't occcur with properly written rules. I want to look into this again at some point though.
Last updated: Dec 07 2023 at 08:19 UTC