universal instantiation

Stream: new members

[Claus-Peter Becke]

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]

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]

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]

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]

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]

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

[Claus-Peter Becke]

@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]

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]

Is it really slower?

[Kevin Buzzard]

It takes more lines of code to write

[Kevin Buzzard]

Especially if you clear them afterwards