Parallel proofs

Stream: new members

[Trevor Hyde]

Suppose we have a proof which at some point requires splitting a hypothesis P ∨ Q and proceeding by cases. Except for some quick step that depends on the two cases, the rest of the proof is syntactically identical in each case. Is there a way, in tactic mode, to do this without repeating all the steps?

Here is a concrete example close to what I had in mind. After the rintro the proofs proceed identically until the left/right steps.

import Mathlib.Tactic

def is_open (U : Set ℝ) : Prop :=
  ∀ v ∈ U, ∃ ε > 0, ∀ u, |u - v| < ε → u ∈ U

-- Union of open sets is open
theorem open_union_open
  (U V : Set ℝ)
  (hU : is_open U)
  (hV : is_open V)
  : is_open (U ∪ V) := by
    rintro x (hxU | hxV)
    · have ⟨ε,hε,hU'⟩ := hU x hxU
      use ε
      constructor
      · assumption
      · intro u hu
        left
        apply hU' u hu
        done
      done
    · have ⟨ε,hε,hU'⟩ := hV x hxV
      use ε
      constructor
      · assumption
      · intro u hu
        right
        apply hU' u hu
        done
      done
    done

Ideally I'd like to be able to do something like this where the argument proceeds in parallel for both goals, and when we need to do something different we could just split ( step for goal 1 | step for goal 2) and then proceed in parallel.

-- Dreaming
theorem open_union_open
  (U V : Set ℝ)
  (hU : is_open U)
  (hV : is_open V)
  : is_open (U ∪ V) := by
    rintro x (hxU | hxV)
   (have ⟨ε,hε,hU'⟩ := hU x hxU | have ⟨ε,hε,hU'⟩ := hV x hxV)
   use ε
   constructor
   · assumption
   · intro u hu
     (left | right)
     apply hU' u hu

[Niels Voss]

A couple things you might want to look at are the all_goals and any_goals tactics, as well as the <;> tactic combinator. If you write tac1 <;> tac2 Lean will run tac2 on every goal that is created from tac1.

Sometimes, wlog is useful as well, especially when the proof is mostly symmetric.

[Chris Wong]

It's a bit fiddly, but this seems like what wlog is designed for.

[Chris Wong]

I'd start the proof with something like

intro x
wlog hx : x ∈ U generalizing U V

[Kyle Miller]

wlog seems better to me, but there's a <;> [tac1; tac2] combinator for running different tactics in each case. I don't see it used very often.

By the way, after the first step, the goals can be solved by simp +contextual [*].

theorem open_union_open
  (U V : Set ℝ)
  (hU : is_open U)
  (hV : is_open V)
  : is_open (U ∪ V) := by
    rintro x (hxU | hxV)
    <;> [have ⟨ε,hε,hU'⟩ := hU x hxU; have ⟨ε,hε,hU'⟩ := hV x hxV]
    <;> (use ε; simp +contextual [*])

[Dan Velleman]

Another approach is to prove a lemma that you can then apply in both cases, like this:

import Mathlib.Tactic

def is_open (U : Set ℝ) : Prop :=
  ∀ v ∈ U, ∃ ε > 0, ∀ u, |u - v| < ε → u ∈ U

lemma open_union_left
  (U V : Set ℝ)
  (hU : is_open U)
  (x : ℝ)
  (hxU : x ∈ U)
  : ∃ ε > 0, ∀ (u : ℝ), |u - x| < ε → u ∈ U ∪ V := by
  have ⟨ε, hε, hU'⟩ := hU x hxU
  use ε
  constructor
  · assumption
  · intro u hu
    left
    exact hU' u hu
    done
  done

-- Union of open sets is open
theorem open_union_open
  (U V : Set ℝ)
  (hU : is_open U)
  (hV : is_open V)
  : is_open (U ∪ V) := by
    rintro x (hxU | hxV)
    · exact open_union_left U V hU x hxU
      done
    · rewrite [Set.union_comm]
      exact open_union_left V U hV x hxV
      done
    done

[Trevor Hyde]

Kyle Miller said:

wlog seems better to me, but there's a <;> [tac1; tac2] combinator for running different tactics in each case. I don't see it used very often.

By the way, after the first step, the goals can be solved by simp +contextual [*].

theorem open_union_open
  (U V : Set ℝ)
  (hU : is_open U)
  (hV : is_open V)
  : is_open (U ∪ V) := by
    rintro x (hxU | hxV)
    <;> [have ⟨ε,hε,hU'⟩ := hU x hxU; have ⟨ε,hε,hU'⟩ := hV x hxV]
    <;> (use ε; simp +contextual [*])

This feels like magic. How does the simp +contextual [*] line work?

[Chris Wong]

Dan Velleman said:

Another approach is to prove a lemma that you can then apply in both cases, like this:

…

Yep, this is what wlog does (more or less).