# Zulip Chat Archive

## Stream: new members

### Topic: generalize to predicate of any order

#### Patrick Thomas (Sep 26 2020 at 20:14):

Is there a way to generalize something like this to predicates `P`

and `Q`

of any order?

```
example {α : Type} {P : α → Prop} {Q : α → Prop} (h : ∀ x : α, P x → Q x) : (∀ x : α, P x) → (∀ x : α, Q x) :=
assume a1 : ∀ x : α, P x,
assume x' : α,
have s1 : P x' := a1 x',
have s2 : P x' → Q x' := h x',
s2 s1
```

#### Patrick Thomas (Sep 26 2020 at 21:05):

That is combine these and the rest in the pattern into one theorem and proof:

```
example {α : Type} {P Q : α → Prop} (h : ∀ x : α, P x → Q x) :
(∀ x : α, P x) → (∀ x : α, Q x) := sorry
example {α β : Type} {P Q : α → β → Prop} (h : ∀ x : α, ∀ y : β, P x y → Q x y) :
(∀ x : α, ∀ y : β, P x y) → (∀ x : α, ∀ y : β, Q x y) := sorry
```

#### Patrick Thomas (Sep 27 2020 at 19:23):

Would creating a tactic be necessary to accomplish something like this?

#### Kevin Buzzard (Sep 27 2020 at 19:24):

`finish`

kills both these goals

#### Patrick Thomas (Sep 27 2020 at 19:25):

I know. I'm wondering more for my understanding of what is possible and necessary.

#### Patrick Thomas (Sep 27 2020 at 19:27):

That is, is there a way to generalize it without tactics?

#### Patrick Thomas (Sep 27 2020 at 19:27):

I'm guessing no?

#### Patrick Thomas (Sep 27 2020 at 19:28):

Which is fine, I'm just curious.

#### Kevin Buzzard (Sep 27 2020 at 19:28):

Your question is very imprecise.

#### Patrick Thomas (Sep 27 2020 at 19:28):

How can I clarify it?

#### Kevin Buzzard (Sep 27 2020 at 19:30):

You asked if it's possible to "combine" infinitely many examples into "one theorem and proof". I don't know what it means to combine two terms in Lean. One tactic solves your examples. Is there another well-formed question which can be asked here?

#### Kyle Miller (Sep 27 2020 at 19:31):

I think the question is about doing reasoning under a collection of universal quantifiers. I've been thinking about something similar, and I think this is an example of what's known as a "reader monad" in Haskell. (The full monad isn't necessary here, I don't think. Maybe just the applicative part?) But, this is only for one layer of quantifiers; you'd still have to nest monads.

#### Patrick Thomas (Sep 27 2020 at 19:33):

Interesting.

#### Kyle Miller (Sep 27 2020 at 19:34):

There's a tactic I was working on for entering a shared context, but it only lives in this Zulip thread right now: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Automatic.20intro.2Fcases.2Fspecialize.2Fuse.20dance/near/203767478

#### Patrick Thomas (Sep 27 2020 at 19:50):

Does shared context mean everything after the prefixed quantifiers?

#### Kyle Miller (Sep 27 2020 at 19:53):

Yeah, and that the quantified variables are assumed to have the same values.

#### Kyle Miller (Sep 27 2020 at 19:54):

Anyway, I did an experiment, and it looks like it's possible to create an ultra modus ponens using typeclasses:

```
class has_mp (α : Sort*) (β : Sort*) (γ : Sort*) :=
(mp : α → β → γ)
def mp {α : Sort*} {β : Sort*} {γ : Sort*} [has_mp α β γ] (f : α) (x : β) : γ := has_mp.mp f x
instance regular_mp {α : Sort*} {β : Sort*} : has_mp (α → β) α β :=
{ mp := λ f x, f x }
instance ultra_mp {X : Sort*} {α : X → Sort*} {β : X → Sort*} {γ : X → Sort*} [h : ∀ (x : X), has_mp (γ x) (α x) (β x)] :
has_mp (Π (x : X), γ x) (Π (x : X), α x) (Π (x : X), β x) :=
{ mp := λ f' x' y, mp (f' y) (x' y) }
example {α : Type} {P Q : α → Prop} (h : ∀ x : α, P x → Q x) :
(∀ x : α, P x) → (∀ x : α, Q x) := λ z, mp h z
example {α β : Type} {P Q : α → β → Prop} (h : ∀ x : α, ∀ y : β, P x y → Q x y) :
(∀ x : α, ∀ y : β, P x y) → (∀ x : α, ∀ y : β, Q x y) := λ z, mp h z
```

#### Kyle Miller (Sep 27 2020 at 19:56):

I'm sort of surprised it actually worked! This should let you apply functions underneath any number of foralls/pis

#### Patrick Thomas (Sep 27 2020 at 19:58):

Cool!

#### Patrick Thomas (Sep 27 2020 at 19:58):

Thank you!

#### Kyle Miller (Sep 27 2020 at 20:00):

Yep, it works for at least one more layer of foralls:

```
example {α β γ : Type} {P Q : α → β → γ → Prop} (h : ∀ (x : α) (y : β) (z : γ), P x y z → Q x y z) :
(∀ (x : α) (y : β) (z : γ), P x y z) → (∀ (x : α) (y : β) (z : γ), Q x y z) := λ z, mp h z
```

#### Kyle Miller (Sep 27 2020 at 20:05):

(Caveat: I'm not sure any of this is a good idea in practice, but it's cool that it seems to work at least in these basic examples.)

Last updated: Dec 20 2023 at 11:08 UTC