## Stream: new members

### Topic: universal instantiation

#### Claus-Peter Becke (Sep 07 2020 at 08:32):

In the following context I would like to apply the universal instantiation to use the Modus Polens to prove the goal.

example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
begin
intro h1,
intro h2,
intro x,
end


What results after having applied these tactics is the following:

tactic failed, there are unsolved goals
state:
α : Type u_1,
p q : α → Prop,
h1 : ∀ (x : α), p x → q x,
h2 : ∀ (x : α), p x,
x : α
⊢ q x


After having chosen x as an arbitrary object it should be possible, I suppose, to use the universal instantiation with respect to the x's in the hypotheses. At the end the application of the Modus Ponens should close the goal. But I don't find a way to apply the universal instantiation.

#### Anne Baanen (Sep 07 2020 at 08:36):

The apply tactic takes a term of the form a -> b -> ... -> c or of the form ∀ x y, a x y -> b x -> ... -> c x y and applies it to a goal of the form c or c x y respectively:

variables {p q : ℕ → Prop}
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
begin
intro h1,
intro h2,
intro x,
apply h1, -- Goal: ⊢ p x
end


#### Anne Baanen (Sep 07 2020 at 08:38):

In this case, because the goal is q x and h1 has type ∀ a, p a -> q a, it tries to match q x with q ?a, deduces that ?a = x, so it already fills in the first argument to h1.

#### Anne Baanen (Sep 07 2020 at 08:40):

You can also create a term applying h1 to x manually:

variables {p q : ℕ → Prop}
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
begin
intro h1,
intro h2,
intro x,
have h1x := h1 x, -- Goal: h1x : p x -> q x ⊢ q x
end


#### Scott Morrison (Sep 07 2020 at 10:12):

or:

variables {p q : ℕ → Prop}
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
begin
intros, solve_by_elim,
end


#### Scott Morrison (Sep 07 2020 at 10:12):

(which just wildly applies apply to everything that it can see until it wins :-)

#### Claus-Peter Becke (Sep 07 2020 at 10:44):

@Anne Baanen, Scott Morrison.
Thank you very much for your support. That worked pretty well. This time I preferred the have-tactic to prove the assumption step by step. Your hints were very helpful.

#### Kevin Buzzard (Sep 07 2020 at 11:28):

Just to remark that using have is the way that mathematicians have traditionally been taught to argue, but it's slower to do in lean, and if you don't tidy up after yourself you get a bunch of superfluous hypotheses in your context. You can solve the goal in two lines with apply and I guess in fact in one line using exact. It's advisable to get into practice killing easy goals quickly by learning how to reason on the goal

#### Johan Commelin (Sep 07 2020 at 11:29):

Is it really slower?

#### Kevin Buzzard (Sep 07 2020 at 11:36):

It takes more lines of code to write

#### Kevin Buzzard (Sep 07 2020 at 11:36):

Especially if you clear them afterwards

Last updated: Dec 20 2023 at 11:08 UTC