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