Commit 2023-06-05 08:37 fb7ec3ed

feat: tactic gcongr for "relational congruence" (#3965) This PR implements a new tactic, gcongr, which applies "relational congruence" rules, reducing a relational goal between a LHS and RHS matching the same pattern to relational subgoals between the differing inputs to the pattern. For example,

example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
    x ^ 4 * a + c ≤ x ^ 4 * b + d := by
  gcongr
  · linarith
  · linarith

This example has the goal of proving the relation ≤ between a LHS and RHS both of the pattern

x ^ 4 * ?_ + ?_

(with inputs a, c on the left and b, d on the right); after the use of gcongr, we have the simpler goals a ≤ b and c ≤ d. For a sense of the style of argument facilitated by the tactic, this commit (which will be PR'd separately) gives >100 examples of use cases in the existing library. The tactic's syntax allows for a pattern to be provided explicitly; this is useful if a non-maximal match is desired:

example {a b c d x : ℝ} (h : a + c + 1 ≤ b + d + 1) :
    x ^ 4 * (a + c) + 5 ≤ x ^ 4 * (b + d) + 5 := by
  gcongr x ^ 4 * ?_ + 5
  linarith

This feature is the analogue for general relations of the mathlib3 congrm tactic. The "relational congruence" rules used are the library lemmas which have been tagged with the attribute @[gcongr]. For example, the first example constructs the proof term

add_le_add (mul_le_mul_of_nonneg_left _ (pow_bit0_nonneg x 2)) _

using the relational congruence lemmas add_le_add and mul_le_mul_of_nonneg_left. In this initial implementation, the @[gcongr] tagging has been set up for arithmetic head functions (+, * etc) and the relations ≤, < and congruence-mod-n. The tactic attempts to discharge side goals to these "relational congruence" lemmas (such as the side goal 0 ≤ x ^ 4 in the above application of mul_le_mul_of_nonneg_left) using the tactic gcongr_discharger, which wraps positivity but can also be extended. Side goals not discharged in this way are left for the user. Zulip discussion