# Zulip Chat Archive

## 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, 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 (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, _⟩, by_contradiction 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

#### Johan Commelin (Jan 16 2020 at 09:05):

@prbot :up:

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

: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