Any powerful tactics I should know about besides `omega`?

Stream: new members

[Philogy]

Without omega by most recent and first non-trivial proof in lean would've been basically impossible. Was such a life saver.

I've heard about aesop but it doesn't seem to work very well, always applying simp and getting stuck because it can't find anything to simplify. I tried linarith a few times and also no help at all.

Wonder if there's any powerful tactic I've been missing out on that people frequently use. My proofs mainly consist of simp, rw, have, intro, apply, simp_rw and of course omega.

Because my first takeaway from writing a larger proof is "omg this is so tedious", I had to prove a lot of "obvious" lemmas just so I could rw / simp parts away like x / (x + 1) = 0 and wonder if it's the way of lean or just a skill issue on my part.

[David Loeffler]

My proofs mainly consist of simp, rw, have, intro, apply, simp_rw and of course omega.

I think the difference between novices and seasoned lean/mathlib power-users is more about the lemmas in their vocabulary, not the tactics. Most of the proofs I write are also using those same basic tactics (although I would also add refine to the list). But most of those tactics are just ways of using lemmas; so the more lemmas you know, the more you can achieve with the tactics.

[Ruben Van de Velde]

Though even more than using lemmas, I think it's about knowing what kind of lemmas you can and can't expect to find in the library, and how to find them (either by guessing the name of using the search tools)

[Yaël Dillies]

David Loeffler said:

I think the difference between novices and seasoned lean/mathlib power-users is more about the lemmas in their vocabulary, not the tactics.

I believe Heather would (like to) strongly disagree

[Michael Rothgang]

• A very useful "basic" skill: know which tactic could apply when. (For instance, do you already know when to apply rw vs apply/refine? How about simp? There is also the norm_num tactic; do you know when to use omega vs norm_num?)
• Depending on what kinds of results you'd like to prove, some more specialized tactics can be useful.
  For analysis proofs, the tactics norm_num, linarith, gcongr and positivity are useful. fun_prop/continuity/measurability can also be pretty useful there. For "simple logic" arguments, tauto can be useful.

[Alex Mobius]

Aesop at base is not much more powerful than simp, can do basic splitting and such, but doesn't even know about tauto or much more lemmas than simp. You can however tag the stuff you need a lot (your own or imported) and have it fill in the gaps in the proof structure for you.

[Philogy]

David Loeffler said:

My proofs mainly consist of simp, rw, have, intro, apply, simp_rw and of course omega.

I think the difference between novices and seasoned lean/mathlib power-users is more about the lemmas in their vocabulary, not the tactics. Most of the proofs I write are also using those same basic tactics (although I would also add refine to the list). But most of those tactics are just ways of using lemmas; so the more lemmas you know, the more you can achieve with the tactics.

Interesting, I suppose that's why, I spent a lot of time searching for simple lemmas in the list of Nat lemmas that I had to end up creating myself via just by omega. Sometimes I think it'd be useful to see what omega did, similar to how aesop has aesop? to see what lemmas it used and learn from it.

[Philogy]

Michael Rothgang said:

• A very useful "basic" skill: know which tactic could apply when. (For instance, do you already know when to apply rw vs apply/refine? How about simp? There is also the norm_num tactic; do you know when to use omega vs norm_num?)
• Depending on what kinds of results you'd like to prove, some more specialized tactics can be useful.
  For analysis proofs, the tactics norm_num, linarith, gcongr and positivity are useful. fun_prop/continuity/measurability can also be pretty useful there. For "simple logic" arguments, tauto can be useful.

Interesting, I did not know about norm_num, where do I learn?

[Yaël Dillies]

Philogy said:

Sometimes I think it'd be useful to see what omega did, similar to how aesop has aesop? to see what lemmas it used and learn from it.

omega does not really use lemmas, so your idea can't really work

[Philogy]

Yaël Dillies said:

Philogy said:

Sometimes I think it'd be useful to see what omega did, similar to how aesop has aesop? to see what lemmas it used and learn from it.

omega does not really use lemmas, so your idea can't really work

Oh I see.

[Yaël Dillies]

... by which I mean that the proof term generated by omega will be a mumble-jumble of applications of docs#Nat.succ_le_iff, docs#Nat.lt_succ_iff and various other things

[Kyle Miller]

If you want to inspect it @Philogy, you can do show_term omega to see the proof term it creates.

[Kyle Miller]

example

example : ∀ n : Nat, n < 2 → n < 3 := by? omega
/-
fun n a =>
  Decidable.byContradiction fun a_1 =>
    Omega.Constraint.not_sat'_of_isImpossible (of_decide_eq_true (id (Eq.refl true)))
      (Omega.Constraint.combine_sat'
        (Omega.Constraint.addInequality_sat
          (le_of_le_of_eq (Int.sub_nonneg_of_le (Omega.Int.ofNat_le_of_le (Nat.le_of_not_lt a_1)))
            (Eq.trans (Omega.Int.sub_congr (Eq.symm Omega.LinearCombo.coordinate_eval_0) (id (Eq.refl ↑3)))
              (Eq.symm
                (Omega.LinearCombo.sub_eval { const := 0, coeffs := [1] } { const := 3, coeffs := [] }
                  (Omega.Coeffs.ofList [↑n]))))))
        (Omega.Constraint.combine_sat'
          (Omega.Constraint.addInequality_sat
            (le_of_le_of_eq (Int.ofNat_nonneg n) (Eq.symm Omega.LinearCombo.coordinate_eval_0)))
          (Omega.tidy_sat
            (Omega.Constraint.addInequality_sat
              (le_of_le_of_eq (Int.sub_nonneg_of_le (Int.add_one_le_of_lt (Omega.Int.ofNat_lt_of_lt a)))
                (Eq.trans
                  (Omega.Int.sub_congr (id (Eq.refl ↑2))
                    (Eq.trans (Omega.Int.add_congr (Eq.symm Omega.LinearCombo.coordinate_eval_0) (id (Eq.refl 1)))
                      (Eq.symm
                        (Omega.LinearCombo.add_eval { const := 0, coeffs := [1] } { const := 1, coeffs := [] }
                          (Omega.Coeffs.ofList [↑n])))))
                  (Eq.symm
                    (Omega.LinearCombo.sub_eval { const := 2, coeffs := [] } { const := 1, coeffs := [1] }
                      (Omega.Coeffs.ofList [↑n])))))))))
-/

(@Yaël Dillies I'm not sure what it means to use or not use lemmas, but certainly omega uses omega-specific theory.)

[Yaël Dillies]

I mean that it doesn't use library lemmas the way Philogy is expecting