## Stream: maths

### Topic: (∀ x : U, P x) ∨ (∀ y : V, Q y) ↔ ∀ (x : U) (y : V), P x ∨ Q

#### Kevin Buzzard (Jan 16 2020 at 08:12):

This fact comes up in Andrej Bauer's proof of a result in my alg geom course. Here's a classical proof:

import tactic

example (U V : Type) (P : U → Prop) (Q : V → Prop) :
(∀ x : U, P x) ∨ (∀ y : V, Q y) ↔ ∀ (x : U) (y : V), P x ∨ Q y :=
begin
split,
intro h,
intros x y,
cases h with h1 h2,
left, exact h1 x,
right, exact h2 y,
intro h,
classical,
by_cases h : (∀ (x : U), P x),
left, exact h,
right,
intro y,
push_neg at h,
cases h with x hx,
replace h := h x y,
cases h,
assumption,
end


I'm assuming (a) there is no constructive proof and (b) this fact will be in the library somewhere. How do I use automation to find it? I couldn't get library_search to work. If I could find it in the library I could verify that it was in the classical part. Do I need to pepper the claim with decidable_somethings?

#### Johan Commelin (Jan 16 2020 at 08:17):

If Andrej formalised it, doesn't that imply that a constructive proof exists?

#### Kenny Lau (Jan 16 2020 at 08:19):

wow it's Andrej Bauer himself!

#### Kenny Lau (Jan 16 2020 at 08:21):

(* We assume excluded middle *)
Axiom lem : forall p : Prop, p \/ ~ p.


#### Johan Commelin (Jan 16 2020 at 08:23):

Wut! Isn't that illegal?

#### Sebastien Gouezel (Jan 16 2020 at 08:59):

Slightly golfed:

example (U V : Type) (P : U → Prop) (Q : V → Prop) :
(∀ x : U, P x) ∨ (∀ y : V, Q y) ↔ ∀ (x : U) (y : V), P x ∨ Q y :=
begin
refine ⟨by tauto, λH, _⟩,
push_neg at h,
rcases h with ⟨⟨x, hx⟩, ⟨y, hy⟩⟩,
simpa [hx, hy] using H x y
end


#### Mario Carneiro (Jan 16 2020 at 08:59):

Eh, please don't ignore good old fashioned looking at files. What I did: The theorem is obviously in logic.basic, it uses forall and or so look for forall_or. Found one distribution lemma, the other is missing, result:

import tactic.interactive logic.basic

protected theorem classical.forall_or_distrib_right
{α} {q : Prop} {p : α → Prop} : (∀x, p x ∨ q) ↔ (∀x, p x) ∨ q :=
by simp [or_comm, classical.forall_or_distrib_left]

example (U V : Type) (P : U → Prop) (Q : V → Prop) :
(∀ x : U, P x) ∨ (∀ y : V, Q y) ↔ ∀ (x : U) (y : V), P x ∨ Q y :=
begin
rw ← classical.forall_or_distrib_right,
simp [classical.forall_or_distrib_left.symm],
end


@prbot :up:

:robot: #1887

#### Patrick Massot (Jan 16 2020 at 09:32):

@Sebastien Gouezel you are complicating things.

begin
refine ⟨by tauto, _⟩,
contrapose!,
tauto
end


#### Mario Carneiro (Jan 16 2020 at 09:33):

This should really be by super

#### Patrick Massot (Jan 16 2020 at 09:34):

or ⟨by tauto, by contrapose! ; tauto⟩

#### Sebastien Gouezel (Jan 16 2020 at 09:38):

Yes, much better. Or now, by library_search :)

#### Kevin Buzzard (Jan 16 2020 at 14:32):

Eh, please don't ignore good old fashioned looking at files.

This is exactly what I want to ignore :-) Mathlib has a high entry bar for mathematicians because we have no hammer and they don't know the names of any lemmas or where to look for them. Bauer says it's called the "Dual Frobenius Law".

#### Kevin Buzzard (Jan 16 2020 at 14:33):

Sebastien told me in Pittsburgh that he doesn't know how to do a rewrite in Isabelle and doesn't know the names of any of the lemmas he uses, because they just use automation over there. This usage model is much more suited to mathematicians, I think.

#### Kevin Buzzard (Jan 16 2020 at 15:03):

Sebastien Gouezel you are complicating things.

begin
refine ⟨by tauto, _⟩,
contrapose!,
tauto
end


Wait -- we can't do it in one tactic? I still don't really understand what is going on here under the hood. Why do tauto! or finish not kill it in one line? I've never even heard of contrapose! :-/ I understand which goals should be closed by simp now but apparently I still don't get this stuff. It all falls under the "trivial to a mathematician" category, doesn't it? What even is super? Answers of the form "it's a superposition solver, dummy" will not help :-/

Last updated: May 19 2021 at 03:22 UTC