generalize to predicate of any order

Stream: new members

[Patrick Thomas]

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]

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]

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

[Kevin Buzzard]

finish kills both these goals

[Patrick Thomas]

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

[Patrick Thomas]

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

[Patrick Thomas]

I'm guessing no?

[Patrick Thomas]

Which is fine, I'm just curious.

[Kevin Buzzard]

Your question is very imprecise.

[Patrick Thomas]

How can I clarify it?

[Kevin Buzzard]

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]

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]

Interesting.

[Kyle Miller]

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]

Does shared context mean everything after the prefixed quantifiers?

[Kyle Miller]

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

[Kyle Miller]

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]

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

[Patrick Thomas]

Cool!

[Patrick Thomas]

Thank you!

[Kyle Miller]

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]

(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.)