## 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: Dec 07 2023 at 08:19 UTC