avoid repetition in proofs

Stream: new members

[Pedro Minicz]

Is there an easy way to avoid repetition in the proof below? I often end up repeating myself when proving biconditionals, I wonder if there is a technique or tactic that can be used in such cases.

import tactic

noncomputable theory

axiom Set : Type
axiom mem : Set → Set → Prop
instance : has_mem Set Set := ⟨mem⟩

@[ext] axiom extensionality {A B : Set} (h : ∀ x, x ∈ A ↔ x ∈ B) : A = B
axiom pairing (a b : Set) : ∃ P : Set, ∀ x, x ∈ P ↔ x = a ∨ x = b

lemma fst_eq_fst_of_pair_eq_pair {a₁ a₂ b₁ b₂ : Set}
  (h : ∀ z : Set, (∀ w, w ∈ z ↔ w = a₁) ∨ (∀ w, w ∈ z ↔ w = a₁ ∨ w = b₁) ↔
                  (∀ w, w ∈ z ↔ w = a₂) ∨ (∀ w, w ∈ z ↔ w = a₂ ∨ w = b₂)) : a₁ = a₂ :=
begin
  ext x,
  split; intro hx,
  { obtain ⟨P, hP⟩ := pairing a₂ a₂,
    simp only [or_self] at hP,
    obtain ⟨h₁, h₂⟩ := h P,
    clear h h₁,
    simp [hP] at h₂,
    cases h₂,
    { rwa h₂ },
    { have := h₂ a₁,
      simp at this,
      specialize h₂ a₂,
      simp at h₂,
      cases h₂,
      { rwa h₂ },
      { substs h₂,
        rwa ←this } } },
  -- Basically the same as above...
  { obtain ⟨P, hP⟩ := pairing a₁ a₁,
    simp only [or_self] at hP,
    obtain ⟨h₁, h₂⟩ := h P,
    clear h h₂,
    simp [hP] at h₁,
    cases h₁,
    { rwa h₁ },
    { have := h₁ a₂,
      simp at this,
      specialize h₁ a₁,
      simp at h₁,
      cases h₁,
      { rwa h₁ },
      { substs h₁,
        rwa ←this } } }
end

[Stuart Presnell]

One thing you could try is to prove a general statement of the principle you’re using as have aux_lemma : … and then apply that in each of the two cases.

[Henrik Böving]

Taking Stuart's thought a little further. If you want to avoid repeating yourself it's quite often possible the same way as we do in regular programming, if we have a function and notice we are repeating ourselves just pull out stuff into an additional function. And since proof=function this applies here as well.

Alternatively you could look into proof combinators such as e.g. ; which repeats a tactic on all subgoals create by another statement (there are many more) or more heavily automated proofs.

[Patrick Johnson]

The right way to do it would be to write another lemma and cover the differences between the cases by the lemma parameters. There is also docs#tactic.wlog that reduces multiple subgoals to just one, if you prove that the generality is not lost.

BTW, in this particular case, finish seems to be smart enough to prove it automatically:

lemma fst_eq_fst_of_pair_eq_pair {a₁ a₂ b₁ b₂ : Set}
  (h : ∀ z : Set, (∀ w, w ∈ z ↔ w = a₁) ∨ (∀ w, w ∈ z ↔ w = a₁ ∨ w = b₁) ↔
                  (∀ w, w ∈ z ↔ w = a₂) ∨ (∀ w, w ∈ z ↔ w = a₂ ∨ w = b₂)) : a₁ = a₂ :=
begin
  obtain ⟨s₁, h₁⟩ := pairing a₁ a₁, obtain ⟨s₂, h₂⟩ := pairing a₂ a₂,
  have h₃ := h s₁, have h₄ := h s₂, finish,
end

[Stuart Presnell]

Sometimes it makes sense to pull out a separate lemma, but if you're planning to PR something to mathlib you should consider whether that lemma is something that will be used more generally or if it's only of interest for this one specific proof. In the latter case you should perhaps just inline it.