Stream: General

Topic: Schematic variables in goal after intro

Lukas Stevens (Apr 07 2020 at 09:15):

I'm trying to use apply(intro transI relcompI) on a goal of the form trans (r O s) but this gives me schematic variables in the goal. How can I avoid this?

Manuel Eberl (Apr 07 2020 at 09:35):

Huh? "intro" shouldn't introduce any schematic variables ever.

Lukas Stevens (Apr 07 2020 at 09:41):

But it does :O

Manuel Eberl (Apr 07 2020 at 09:42):

can you show a minimal example

Lukas Stevens (Apr 07 2020 at 09:43):

lemma "trans (r O s)"
  apply(intro transI relcompI)

Lukas Stevens (Apr 07 2020 at 09:44):

For me, it produces:

proof (prove)
goal (2 subgoals):
 1. ⋀x y z. ⟦(x, y) ∈ r O s; (y, z) ∈ r O s⟧ ⟹ (x, ?b1 x y z) ∈ r
 2. ⋀x y z. ⟦(x, y) ∈ r O s; (y, z) ∈ r O s⟧ ⟹ (?b1 x y z, z) ∈ s

Manuel Eberl (Apr 07 2020 at 09:50):

I can try to investigate later. I thought "intro" wasn't supposed to produce schematic variables.

Manuel Eberl (Apr 07 2020 at 09:50):

I would just use "rule" and "assumption" by hand, or "rule" and "erule"

Manuel Eberl (Apr 07 2020 at 09:51):

apply (rule transI) apply (erule (1) relcompI)

Manuel Eberl (Apr 07 2020 at 09:51):

err no

Manuel Eberl (Apr 07 2020 at 09:51):

you'll first have to eliminate the "o" in the assumptions

Manuel Eberl (Apr 07 2020 at 09:52):

apply (elim relcompE), probably. And then "erule (2) relcompI"

Last updated: Apr 23 2024 at 12:29 UTC