Change the scope of quantifiers or apply tactics inside

Stream: general

[Avi Craimer]

In proving theorems I sometimes find I'm trying to prove something with the form:

(∀ (a b : X ), P a → Q b) → R

How can I shift the scope of the forall to get?

(∀ (a b : X ), P a → Q b → R)

The motivation is that the way the intro tactic works makes it difficult to do certain things to the hypothesis once it's moved out of the main goal.

e.g., when I use intro h1 it gives me:

h1: (∀ (a b : X ), P a → Q b)
⊢ R

So I cannot use intro h1 a b since there are not longer any quantified a b in the goal.

One concrete example where this has been an issue is when X is a finite type and I want to use the cases tactic to evaluate all possible values for a and b. I can't use cases a b unless I can get a and b as hypotheses.

This could also be solved if there was a tactic that worked like cases but applied inside the scope of logical connectives.

[cairunze cairunze]

it might not be true if we want to pull those quantifiers out.
Assuming X is not empty, the following is true.
((∀a∀b(Pa→Qb))→R)↔(∃a∃b((Pa→Qb)→R))
see, https://www.umsu.de/trees/#((~6a~6b(Pa~5Qb))~5R)~4(~7a~7b((Pa~5Qb)~5R))

[Kim Morrison]

Those things are definitely not logically equivalent, so Lean will correctly not allow you to do this.

[Avi Craimer]

Just to clarify, in the cases I need to use this I definitely could prove it on a case-by-case basis. I just was wondering if there was a tactics-based way of doing this so I don't have to prove a bunch of extra obvious statements.

[Mario Carneiro]

the theorem is in general false, so there must be something more to the question

[Avi Craimer]

In practice this problem occurs with universal quantifiers over variables of type PUnit. Since there is only one value for this type a specialization to the single value also proves the universal. I believe this is done with the cases tactic. It works fine if I've got a universal as a complete statement in the main goal, but I can't figure apply the tactic when I have a complex goal such as

(∀ (a b : PUnit ), P a → Q b) → R

Here I can intro the whole universal into a hypothesis but then I can't apply cases to the hypothesis.

It may be there is a different tactic I don't know about that solves this.

[Mario Carneiro]

it's still in general false even without the quantifiers

[Mario Carneiro]

(A -> B) -> C is not the same as A -> (B -> C)

[Avi Craimer]

That's not what I'm sayin.

I believe this holds:

(∀ (a b : X ), (P a → Q b)) → R

Iff

(∀ (a b : X ), (P a → Q b) → R)

Assuming R does not contain variables a or b.

We aren't re-associating inside the body of forall, just expanding the scope of the quantifier to include R

[Mario Carneiro]

the parentheses are different than the first time

[Avi Craimer]

My mistake.

[Mario Carneiro]

but this is also not true unless X is a singleton type

[Avi Craimer]

@Mario Carneiro to avoid the XY help-desk issues you mentioned in the context of my other question, I want to clarify that the specific of changing the quantifier scope is less important to solving my problem, than the more general question of how to solve the issue of not being able to apply certain tactics to a hypothesis in the tactics state.

[Mario Carneiro]

the tactics you can apply to a hypothesis or the goal are based on the valid rules of natural deduction

[Mario Carneiro]

obviously these are different, so it's not always the same operations you can perform

[Avi Craimer]

Ok, so maybe it would help to make the question hyper-specific.

Suppose you have:

(∀ (a b : X ), (P a → Q b)) → R
such that X has finitely many inhabitants.

How do I prove (∀ (a b : X ), (P a → Q b)) by proving it for every inhabitant.

Note: I can't use cases since (∀ (a b : X ), (P a → Q b)) is not the main goal.

[Mauricio Collares]

Any time (∀ (a b : X ), (P a → Q b)) is false (for example, X = Fin 2, P 0 = True, P 1 = True, Q 0 = True, Q 1 = False), it holds that (∀ (a b : X ), (P a → Q b)) → R is true. So I don't understand why you want to prove (∀ (a b : X ), (P a → Q b)).

[Kevin Buzzard]

@Avi Craimer this discussion could be the poster child for demonstrating why it's best to ask questions with #mwe s. Can you show some fully compiling lean code with a (provable) sorry which you would like to fill in? I think that way it will be possible to understand much better what the actual question is.