Zulip Chat Archive

Stream: new members

Topic: avoid repetition in proofs


Pedro Minicz (Jan 07 2022 at 17:48):

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 (Jan 07 2022 at 18:04):

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 (Jan 07 2022 at 18:43):

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 (Jan 07 2022 at 18:47):

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 (Jan 07 2022 at 18:57):

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.


Last updated: Dec 20 2023 at 11:08 UTC