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?

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

But it does :O

can you show a minimal example

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

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

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

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

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

err no

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

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

Last updated: Dec 07 2023 at 08:19 UTC