Anonymous `apply` or `specialize`

Stream: new members

[nrs]

If I have these inaccessible hypotheses,

a✝ : ∀ (x : α), p x ∧ q x
x✝ : α

is there a way to either use apply anonymously or specialize anonymously?

[Kyle Miller]

No, you are either supposed to name the hypotheses at the place where they were introduced (this is usually possible) or name them with rename_i or next ... =>

[Kyle Miller]

(Please give a #mwe for more specific advice)

[nrs]

Kyle Miller said:

No, you are either supposed to name the hypotheses at the place where they were introduced (this is usually possible) or name them with rename_i or next ... =>

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) := by
  intro h x
  cases h
  rename_i a b
  specialize a x
  specialize b x
  apply And.intro <;> assumption

For example, it seems to me natural in the above proof to abstract away this part:

  rename_i a b
  specialize a x
  specialize b x

by directly specializing all possible statements

[Kyle Miller]

An example of using a tactic that can name the new hypotheses:

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) := by
  intro h x
  obtain ⟨a, b⟩ := h
  specialize a x
  specialize b x
  apply And.intro <;> assumption

[Kyle Miller]

This can be combined with intro:

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) := by
  intro ⟨a, b⟩ x
  specialize a x
  specialize b x
  apply And.intro <;> assumption

[Kyle Miller]

(You can use constructor instead of apply And.intro. It does the same thing, but you don't need to know the name And.intro)

[nrs]

Kyle Miller said:

(You can use constructor instead of apply And.intro. It does the same thing, but you don't need to know the name And.intro)

ah very cool tips! thanks a lot, way sleeker looking

[Jireh Loreaux]

I know this isn't directly the content of the question, but I wouldn't use specialize here, as I don't think it's contributing anything. Of course, you can golf this all the way down to:

universe u
variable {X : Type u} {p q : X → Prop}

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) :=
  fun ⟨a, b⟩ x ↦ ⟨a x, b x⟩

[Jireh Loreaux]

Or, if you have allow a very small import:

import Init.PropLemmas

universe u
variable {X : Type u} {p q : X → Prop}

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) :=
  forall_and.mpr

[nrs]

Jireh Loreaux said:

I know this isn't directly the content of the question, but I wouldn't use specialize here, as I don't think it's contributing anything. Of course, you can golf this all the way down to:

universe u
variable {X : Type u} {p q : X → Prop}

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) :=
  fun ⟨a, b⟩ x ↦ ⟨a x, b x⟩

woah! that is probably the most optimized version possible and nevertheless very clear in what it does. thanks!!

[Kyle Miller]

And of course, this is a basic logical tautology, so the tauto tactic works too :smile:

example : (∀ x, p x) ∧ (∀ x, q x) -> (∀ x, p x ∧ q x) := by tauto

[Jireh Loreaux]

I didn't remember that tauto handles ∀. And in fact, it doesn't according to #help tactic tauto. @Kyle Miller what exactly is in scope for tauto?

[Kyle Miller]

@Jireh Loreaux Oh, it seems that I've misunderstood the scope of tauto, and it accidentally works here.

This is a tautology, but tauto fails for it:

example : (∀ x, p x) ∧ (∀ x, q x) ↔ (∀ x, p x ∧ q x) := by tauto