# The `gcongr`

("generalized congruence") tactic #

The `gcongr`

tactic applies "generalized 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 ^ 2 * a + c ≤ x ^ 2 * 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 ^ 2 * ?_ + ?_
```

(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`

.

A pattern can 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 ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 := by
gcongr x ^ 2 * ?_ + 5
linarith
```

## Sourcing the generalized congruence lemmas #

Relevant "generalized congruence" lemmas are declared using 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 1)) _
```

using the generalized congruence lemmas `add_le_add`

and `mul_le_mul_of_nonneg_left`

. The term
`pow_bit0_nonneg x 1`

is automatically generated by a discharger (see below).

When a lemma is tagged `@[gcongr]`

, it is verified that that lemma is of "generalized congruence"
form, `f x₁ y z₁ ∼ f x₂ y z₂`

, that is, a relation between the application of a function to two
argument lists, in which the "varying argument" pairs (here `x₁`

/`x₂`

and `z₁`

/`z₂`

) are all free
variables. The "varying"/non-"varying" classification of the arguments is recorded (as an array of
booleans), and the `gcongr`

tactic will try a lemma only if it matches the goal in relation `∼`

,
head function `f`

and "varying"/non-"varying" classification for each of the inputs to `f`

. Thus,
for example, all three of the following lemmas are tagged `@[gcongr]`

and are used in different
situations according to whether the goal compares constant-left-multiplications,
constant-right-multiplications, or fully varying multiplications:

```
theorem mul_le_mul_of_nonneg_left [Mul α] [Zero α] [Preorder α] [PosMulMono α]
{a b c : α} (h : b ≤ c) (a0 : 0 ≤ a) :
a * b ≤ a * c
theorem mul_le_mul_of_nonneg_right [Mul α] [Zero α] [Preorder α] [MulPosMono α]
{a b c : α} (h : b ≤ c) (a0 : 0 ≤ a) :
b * a ≤ c * a
theorem mul_le_mul [MulZeroClass α] [Preorder α] [PosMulMono α] [MulPosMono α]
{a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) :
a * c ≤ b * d
```

The advantage of this approach is that the lemmas with fewer "varying" input pairs typically require fewer side conditions, so the tactic becomes more useful by special-casing them.

There can also be more than one generalized congruence lemma dealing with the same relation, head
function and "varying"/non-"varying" configuration, for example with purely notational head
functions which have different theories when different typeclass assumptions apply. For example,
the following lemma is stored with the same `@[gcongr]`

data as `mul_le_mul`

above, and the two
lemmas are simply tried in succession to determine which has the typeclasses relevant to the goal:

```
theorem mul_le_mul' [Mul α] [Preorder α] [CovariantClass α α (· * ·) (· ≤ ·)]
[CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a * c ≤ b * d
```

## Resolving goals #

The tactic attempts to discharge side goals to the "generalized congruence" lemmas (such as the
side goal `0 ≤ x ^ 2`

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.

The tactic also attempts to discharge "main" goals using the available hypotheses, as well as a
limited amount of forward reasoning. Such attempts are made *before* descending further into
matching by congruence. The built-in forward-reasoning includes reasoning by symmetry and
reflexivity, and this can be extended by writing tactic extensions tagged with the
`@[gcongr_forward]`

attribute.

## Introducing variables and hypotheses #

Some natural generalized congruence lemmas have "main" hypotheses which are universally quantified or have the structure of an implication, for example

```
theorem GCongr.Finset.sum_le_sum [OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι}
(h : ∀ (i : ι), i ∈ s → f i ≤ g i) :
s.sum f ≤ s.sum g
```

The tactic automatically introduces the variable `i✝ : ι`

and hypothesis `hi✝ : i✝ ∈ s`

in the
subgoal `∀ (i : ι), i ∈ s → f i ≤ g i`

generated by applying this lemma. By default this is done
anonymously, so they are inaccessible in the goal state which results. The user can name them if
needed using the syntax `gcongr with i hi`

.

## Variants #

The tactic `rel`

is a variant of `gcongr`

, intended for teaching. Local hypotheses are not
used automatically to resolve main goals, but must be invoked by name:

```
example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) :
x ^ 2 * a + c ≤ x ^ 2 * b + d := by
rel [h1, h2]
```

The `rel`

tactic is finishing-only: if fails if any main or side goals are not resolved.

Environment extension for "generalized congruence" (`gcongr`

) lemmas.

The core of the `gcongr`

tactic. Parse a goal into the form `(f _ ... _) ∼ (f _ ... _)`

,
look up any relevant @[gcongr] lemmas, try to apply them, recursively run the tactic itself on
"main" goals which are generated, and run the discharger on side goals which are generated. If there
is a user-provided template, first check that the template asks us to descend this far into the
match.

See if the term is `a = b`

and the goal is `a ∼ b`

or `b ∼ a`

, with `∼`

reflexive.

## Instances For

See if the term is `a < b`

and the goal is `a ≤ b`

.

## Instances For

See if the term is `a ∼ b`

with `∼`

symmetric and the goal is `b ∼ a`

.

## Instances For

Attempt to resolve an (implicitly) relational goal by one of a provided list of hypotheses, either with such a hypothesis directly or by a limited palette of relational forward-reasoning from these hypotheses.

## Instances For

The `gcongr`

tactic applies "generalized 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 ^ 2 * a + c ≤ x ^ 2 * 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 ^ 2 * ?_ + ?_
```

(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`

.

A pattern can 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 ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 := by
gcongr x ^ 2 * ?_ + 5
linarith
```

The "generalized 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 1)) _
```

using the generalized congruence lemmas `add_le_add`

and `mul_le_mul_of_nonneg_left`

.

The tactic attempts to discharge side goals to these "generalized congruence" lemmas (such as the
side goal `0 ≤ x ^ 2`

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.

## Instances For

The `rel`

tactic applies "generalized congruence" rules to solve a relational goal by
"substitution". For example,

```
example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) :
x ^ 2 * a + c ≤ x ^ 2 * b + d := by
rel [h1, h2]
```

In this example we "substitute" the hypotheses `a ≤ b`

and `c ≤ d`

into the LHS `x ^ 2 * a + c`

of
the goal and obtain the RHS `x ^ 2 * b + d`

, thus proving the goal.

The "generalized 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 h1 (pow_bit0_nonneg x 1)) h2
```

using the generalized congruence lemmas `add_le_add`

and `mul_le_mul_of_nonneg_left`

. If there are
no applicable generalized congruence lemmas, the tactic fails.

The tactic attempts to discharge side goals to these "generalized congruence" lemmas (such as the
side goal `0 ≤ x ^ 2`

in the above application of `mul_le_mul_of_nonneg_left`

) using the tactic
`gcongr_discharger`

, which wraps `positivity`

but can also be extended. If the side goals cannot
be discharged in this way, the tactic fails.