tactic for linear_ordered_add_comm_groups

Stream: new members

[Raphael Appenzeller]

I use linear_ordered_add_comm_group and wonder if there is a nice tactic like ring that solves basic statements like the following:

lemma example (Λ : Type* ) [linear_ordered_add_comm_group Λ] (a b c : Λ ): a - b + c = c + a - b :=

I have tried all the following, all of which do not work: library_search, ring, group, linarith, simp.

[Eric Wieser]

abel?

[Raphael Appenzeller]

This is pretty good and solves the example. Which tactic could I use to simplify the order-aspects? linarith?

[Raphael Appenzeller]

For example, the following Lemma is somewhat time-consuming to solve by hand and it feels like a tactic might be able to do it. Is there a way to write less?

lemma ex (Λ : Type* ) [linear_ordered_add_comm_group Λ] (txf tyf fa fb f1a f1b f2a f2b : Λ )
(h1 :txf - fa + f1a ≤ f1b) (h2 : f2a ≤ tyf - fb + f2b) (h3: f1b - f1a + (f2b - f2a) = fb -fa): txf ≤ tyf :=
begin
  have h4 : txf ≤ f1b - f1a + fa  , -- using h1
  have h4' : txf - fa + f1a + (fa - f1a) ≤ f1b  + ( fa -f1a),
  apply add_le_add_right h1 (fa - f1a),
  abel at h4',
  abel,
  exact h4', -- proved h4

  have h5 : f1b - f1a + fa = f2a - f2b + fb, -- using h3
  have h5' : f1b - f1a + (f2b - f2a) + (fa - f2b + f2a) = fb - fa + (fa - f2b + f2a),
  exact congr_fun (congr_arg has_add.add h3) (fa - f2b + f2a),
  abel at h5',
  abel,
  exact h5', -- proved h5

  have h6 : f2a - f2b + fb ≤ tyf, -- using h2
  have h6' : f2a + (fb - f2b) ≤ tyf - fb + f2b + (fb - f2b),
  apply add_le_add_right h2 (fb - f2b),
  abel at h6',
  abel,
  exact h6', -- proved h6

  rw h5 at h4,
  exact le_trans h4 h6,
end

[Ruben Van de Velde]

This is less:

lemma ex (Λ : Type*) [linear_ordered_add_comm_group Λ]
  (txf tyf fa fb f1a f1b f2a f2b : Λ)
  (h1 : txf - fa + f1a ≤ f1b)
  (h2 : f2a ≤ tyf - fb + f2b)
  (h3 : f1b - f1a + (f2b - f2a) = fb - fa) :
  txf ≤ tyf :=
calc txf
    ≤ f1b + (fa - f1a) : by rwa [←sub_le_iff_le_add, ←sub_add]
... = f2a - (f2b - fb) : by { rw ←add_eq_of_eq_sub h3, abel }
... ≤ tyf : by rwa [sub_le_iff_le_add, sub_eq_neg_add, ←add_assoc, ←sub_eq_add_neg]

(I particularly tried to have the one abel call do as much as possible)

[Ruben Van de Velde]

The last line could also be

... ≤ tyf : by { rw [sub_le_iff_le_add], convert h2 using 1, abel }

which might be more conceptual (is that the right word?)

[Raphael Appenzeller]

Thank you so much!