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 α] [MulLeftMono α]
    [MulRightMono α] {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.

structure Mathlib.Tactic.GCongr.GCongrKey : Type

GCongrKey is the key used to store and look up gcongr lemmas.

• relName : Lean.Name

  The name of the relation. For example, a + b ≤ a + c has relName := `LE.le.

• head : Lean.Name

  The name of the head function. For example, a + b ≤ a + c has head := `HAdd.hAdd.

• varyingArgs : Array Bool

  The array of which arguments in the application of head are different. For example, a + b ≤ a + c has #[false, false, false, false, false, true].

instance Mathlib.Tactic.GCongr.instInhabitedGCongrKey : Inhabited GCongrKey

Equations

• Mathlib.Tactic.GCongr.instInhabitedGCongrKey = { default := { relName := default, head := default, varyingArgs := default } }

instance Mathlib.Tactic.GCongr.instBEqGCongrKey : BEq GCongrKey

Equations

• Mathlib.Tactic.GCongr.instBEqGCongrKey = { beq := Mathlib.Tactic.GCongr.beqGCongrKey✝ }

instance Mathlib.Tactic.GCongr.instHashableGCongrKey : Hashable GCongrKey

Equations

• Mathlib.Tactic.GCongr.instHashableGCongrKey = { hash := Mathlib.Tactic.GCongr.hashGCongrKey✝ }

structure Mathlib.Tactic.GCongr.GCongrLemma : Type

Structure recording the data for a "generalized congruence" (gcongr) lemma.

• declName : Lean.Name

  The name of the lemma.

• mainSubgoals : Array (Nat × Nat × Nat)

  mainSubgoals are the subgoals on which gcongr will be recursively called. They store

  • the index of the hypothesis
  • the index of the arguments in the conclusion
  • the number of parameters in the hypothesis

instance Mathlib.Tactic.GCongr.instInhabitedGCongrLemma : Inhabited GCongrLemma

Equations

• Mathlib.Tactic.GCongr.instInhabitedGCongrLemma = { default := { declName := default, mainSubgoals := default } }

instance Mathlib.Tactic.GCongr.instReprGCongrLemma : Repr GCongrLemma

Equations

• Mathlib.Tactic.GCongr.instReprGCongrLemma = { reprPrec := Mathlib.Tactic.GCongr.reprGCongrLemma✝ }

opaque Mathlib.Tactic.GCongr.gcongrExt : Lean.SimpleScopedEnvExtension (GCongrKey × GCongrLemma) (Std.HashMap GCongrKey (Array GCongrLemma))

Environment extension for "generalized congruence" (gcongr) lemmas.

def Mathlib.Tactic.GCongr.getCongrAppFnArgs (e : Lean.Expr) : Option (Lean.Name × Array Lean.Expr)

Given an application f a₁ .. aₙ, return the name of f, and the array of arguments aᵢ.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.getRel (e : Lean.Expr) : Option (Lean.Name × Lean.Expr × Lean.Expr)

If e is of the form r a b, return (r, a, b).

Equations

• Mathlib.Tactic.GCongr.getRel ((rel.app lhs).app rhs) = Option.map (fun (x : Lean.Name) => (x, lhs, rhs)) rel.getAppFn.constName?
• Mathlib.Tactic.GCongr.getRel (Lean.Expr.forallE binderName lhs rhs binderInfo) = if (!rhs.hasLooseBVars) = true then some (`_Implies, lhs, rhs) else none
• Mathlib.Tactic.GCongr.getRel e = none

def Mathlib.Tactic.GCongr.makeGCongrLemma (decl : Lean.Name) (declTy : Lean.Expr) (numHyps : Nat) : Lean.MetaM (GCongrKey × GCongrLemma)

Construct the GCongrKey and GCongrLemma data from a given lemma.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.tacticGcongr_discharger : Lean.ParserDescr

Equations

• Mathlib.Tactic.GCongr.tacticGcongr_discharger = Lean.ParserDescr.node `Mathlib.Tactic.GCongr.tacticGcongr_discharger 1024 (Lean.ParserDescr.nonReservedSymbol "gcongr_discharger" false)

def Mathlib.Tactic.GCongr.gcongrDischarger (goal : Lean.MVarId) : Lean.MetaM Unit

This is used as the default side-goal discharger, it calls the gcongr_discharger extensible tactic.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.exactRefl : ForwardExt

See if the term is a = b and the goal is a ∼ b or b ∼ a, with ∼ reflexive.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.symmExact : ForwardExt

See if the term is a ∼ b with ∼ symmetric and the goal is b ∼ a.

Equations

• Mathlib.Tactic.GCongr.symmExact = { eval := fun (h : Lean.Expr) (goal : Lean.MVarId) => do let __do_lift ← goal.applySymm __do_lift.assignIfDefEq h }

def Mathlib.Tactic.GCongr.exact : ForwardExt

Equations

• Mathlib.Tactic.GCongr.exact = { eval := fun (e : Lean.Expr) (m : Lean.MVarId) => m.assignIfDefEq e }

def Lean.MVarId.gcongrForward (hs : Array Expr) (g : MVarId) : MetaM Unit

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.gcongrForwardDischarger (goal : Lean.MVarId) : Lean.MetaM Unit

This is used as the default main-goal discharger, consisting of running Lean.MVarId.gcongrForward (trying a term together with limited forward-reasoning on that term) on each nontrivial hypothesis.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.containsHole (template : Lean.Expr) : Lean.MetaM Bool

Determine whether template contains a ?_. This guides the gcongr tactic when it is given a template.

Equations

• One or more equations did not get rendered due to their size.

The lemmas rel_imp_rel, rel_trans and rel_trans' are too general to be tagged with @[gcongr], so instead we use getTransLemma? to look up these lemmas.

theorem Mathlib.Tactic.GCongr.rel_imp_rel {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] {a b c d : α} (h₁ : r c a) (h₂ : r b d) : r a b → r c d

theorem Mathlib.Tactic.GCongr.rel_trans {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] {a b c : α} (h : r a b) : r b c → r a c

theorem Mathlib.Tactic.GCongr.rel_trans' {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] {a b c : α} (h : r b c) : r a b → r a c

def Mathlib.Tactic.GCongr.getTransLemma? (key : GCongrKey) : Array GCongrLemma

getTransLemma? constructs a GCongrLemma for gcongr goals of the form a ≺ b → c ≺ d. This will be tried if there is no other available @[gcongr] lemma. For example, the relation a ≡ b [ZMOD n] has an instance of IsTrans, so a congruence of the form a ≡ b [ZMOD n] → c ≡ d [ZMOD n] can be solved with rel_imp_rel, rel_trans or rel_trans'.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.MVarId.gcongr (g : MVarId) (template : Option Expr) (names : List (TSyntax `Lean.binderIdent)) (inGRewrite : Bool := false) (mainGoalDischarger : MVarId → MetaM Unit := Mathlib.Tactic.GCongr.gcongrForwardDischarger) (sideGoalDischarger : MVarId → MetaM Unit := Mathlib.Tactic.GCongr.gcongrDischarger) : MetaM (Bool × List (TSyntax `Lean.binderIdent) × Array MVarId)

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.

def Mathlib.Tactic.GCongr.tacticGcongr__With___ : Lean.ParserDescr

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.

gcongr will descend into binders (for example sums or suprema). To name the bound variables, use with:

example {f g : ℕ → ℝ≥0∞} (h : ∀ n, f n ≤ g n) : ⨆ n, f n ≤ ⨆ n, g n := by
  gcongr with i
  exact h i

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.GCongr.«tacticRel[_]» : Lean.ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.