# Zulip Chat Archive

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