Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 16 2020 at 08:17):

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

view this post on Zulip Kenny Lau (Jan 16 2020 at 08:19):

wow it's Andrej Bauer himself!

view this post on Zulip Kenny Lau (Jan 16 2020 at 08:21):

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

view this post on Zulip Johan Commelin (Jan 16 2020 at 08:23):

Wut! Isn't that illegal?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 16 2020 at 09:05):

@prbot :up:

view this post on Zulip Mario Carneiro (Jan 16 2020 at 09:16):

:robot: #1887

view this post on Zulip Patrick Massot (Jan 16 2020 at 09:32):

@Sebastien Gouezel you are complicating things.

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

view this post on Zulip Mario Carneiro (Jan 16 2020 at 09:33):

This should really be by super

view this post on Zulip Patrick Massot (Jan 16 2020 at 09:34):

or ⟨by tauto, by contrapose! ; tauto⟩

view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 09:38):

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

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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