Stream: General

Topic: schematic goals with Eps

Leander Behr (Oct 20 2022 at 15:13):

I can easily prove this goal

schematic_goal "⋀x. P x ⟹ P ?x"

via

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 y.

Mathias Fleury (Oct 20 2022 at 15:26):

Do your really mean (⋀x y. P x y) ⟹ P ?x ?y?

Mathias Fleury (Oct 20 2022 at 15:27):

that is also the reason why x cannot be instantiated with x: they don't live in the same scope…

Mathias Fleury (Oct 20 2022 at 15:28):

schematic_goal "(P x y ⟹ P ?x y)"
  by assumption

Leander Behr (Oct 20 2022 at 15:33):

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 by assumption.

Mathias Fleury (Oct 20 2022 at 15:34):

oh no sorry you are right

Mathias Fleury (Oct 20 2022 at 15:35):

⋀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 ⋀

Mathias Fleury (Oct 20 2022 at 15:36):

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

Leander Behr (Oct 20 2022 at 15:42):

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 x.

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.

Leander Behr (Oct 20 2022 at 15:47):

Actually ⋀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.

Mathias Fleury (Oct 20 2022 at 15:49):

can't you just change your theorem to require \<exists>x. P x y?

Leander Behr (Oct 20 2022 at 15:57):

It creates multiple new goals containing the schematic variable

Mathias Fleury (Oct 20 2022 at 16:42):

I meant: changing the location where you actually need that theorem

Mathias Fleury (Oct 20 2022 at 16:42):

because I have a hard time imagining where you could need such a theorem

Leander Behr (Nov 06 2022 at 16:40):

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: Apr 19 2024 at 04:17 UTC