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

Stream: maths

[Kevin Buzzard]

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,
    contradiction,
  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?

@XenaProject I think I have a better paper proof of "union of algebraic sets is algebraic", and I formalized it, unfortunately in Coq because I do not speak Lean (can only read it), here: https://gist.github.com/andrejbauer/4dd8fa975fc98c9cc48dfdc776abde23

- Andrej Bauer (@andrejbauer)

[Johan Commelin]

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

[Kenny Lau]

wow it's Andrej Bauer himself!

[Kenny Lau]

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

[Johan Commelin]

Wut! Isn't that illegal?

[Sebastien Gouezel]

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, _⟩,
  by_contradiction h,
  push_neg at h,
  rcases h with ⟨⟨x, hx⟩, ⟨y, hy⟩⟩,
  simpa [hx, hy] using H x y
end

[Mario Carneiro]

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

[Johan Commelin]

@prbot :up:

[Mario Carneiro]

:robot: #1887

[Patrick Massot]

@Sebastien Gouezel you are complicating things.

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

[Mario Carneiro]

This should really be by super

[Patrick Massot]

or ⟨by tauto, by contrapose! ; tauto⟩

[Sebastien Gouezel]

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

[Kevin Buzzard]

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]

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]

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 :-/