classical.skolem after two foralls

Stream: general

[Kevin Buzzard]

classical.skolem turns a forall, exists into an exists, forall. This works:

example : ∀ (a : ℤ), ∃ b : ℤ, b < a :=
begin
  simp [classical.skolem],
  -- ⊢ ∃ (f : ℤ → ℤ), ∀ (x : ℤ), f x < x
  sorry
end

But I was expecting this to work too:

example : ∀ (a b : ℤ), ∃ c : ℤ, c < a + b :=
begin
  simp [classical.skolem], -- simplify tactic failed to simplify
end

I don't understand why Lean doesn't rewrite once, let alone twice.

[Kevin Buzzard]

example : ∀ (a b : ℤ), ∃ c : ℤ, c < a + b :=
begin
  intro a,
  simp [classical.skolem],
  revert a,
  simp [classical.skolem],
  sorry
end

works

[Kenny Lau]

probably higher order unification?

[Kevin Buzzard]

Really? I'm just switching a forall and an exists. Here is the application.

import topology.basic

def hausdorff (X : Type) [topological_space X] : Prop :=
∀ x y : X, x ≠ y → ∃ U V : set X, is_open U ∧ is_open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅

def hausdorff' (X : Type) [topological_space X] : Prop :=
∃ U V : Π (x y : X), x ≠ y → set X,
  ∀ x y h,
  is_open (U x y h) ∧
  is_open (V x y h) ∧
  x ∈ (U x y h) ∧
  y ∈ (V x y h) ∧
  (U x y h) ∩ (V x y h) = ∅

variables {X : Type} [topological_space X]

theorem hausdorff_iff : hausdorff X ↔ hausdorff' X :=
begin
  split,
  { intro h,
    choose U V hUV using h,
    use U,
    use V,
    exact hUV
  },
  { intro h,
    intro x,
    simp only [classical.skolem],
    revert x,
    simp only [classical.skolem],
    exact h,
  }
  -- { rintro ⟨U, V, hUV⟩,
  --   intros x y hxy,
  --   use (U x y hxy),
  --   use (V x y hxy),
  --   exact hUV x y hxy }
end

I want the proof in the <- direction to be simp [classical.skolem]

[Kevin Buzzard]

I've been talking to too many constructivists on Twitter