congr(...) congruence quotations

This module defines a term elaborator for generating congruence lemmas from patterns written using quotation syntax. One can write congr($hf $hx) with hf : f = f' and hx : x = x' to get f x = f' x'. While in simple cases it might be possible to use congr_arg or congr_fun, congruence quotations are more general, since for example f could have implicit arguments, complicated dependent types, and subsingleton instance arguments such as Decidable or Fintype.

The implementation strategy is the following:

1. The pattern is elaborated twice, once with each hole replaced by the LHS and again with each hole replaced by the RHS. We do not force the hole to have any particular type while elaborating, but if the hole has a type with an obvious LHS or RHS, then we propagate this information outward. We use Mathlib.Tactic.TermCongr.cHole with metadata for these replacements to hold onto the hole itself.
2. Once the pattern has been elaborated twice, we unify them against the respective LHS and RHS of the target type if the target has a type with an obvious LHS and RHS. This can fill in some metavariables and help typeclass inference make progress.
3. Then we simultaneously walk along the elaborated LHS and RHS expressions to generate a congruence. When we reach cHoles, we make sure they elaborated in a compatible way. Each Expr type has some logic to come up with a suitable congruence. For applications we use a version of Lean.Meta.mkHCongrWithArity that tries to fill in some of the equality proofs using subsingleton lemmas.

The point of elaborating the expression twice is that we let the elaborator handle activities like synthesizing instances, etc., specialized to LHS or RHS, without trying to derive one side from the other.

During development there was a version using simp transformations, but there was no way to inform simp about the expected RHS, which could cause simp to fail because it eagerly wants to solve for instance arguments. The current version is able to use the expected LHS and RHS to fill in arguments before solving for instance arguments.

def Mathlib.Tactic.TermCongr.termCongr : Lean.ParserDescr

congr(expr) generates an congruence from an expression containing congruence holes of the form $h or $(h). In these congruence holes, h : a = b indicates that, in the generated congruence, on the left-hand side a is substituted for $h and on the right-hand side b is substituted for $h.

For example, if h : a = b then congr(1 + $h) : 1 + a = 1 + b.

This is able to make use of the expected type, for example (congr(_ + $h) : 1 + _ = _) with h : x = y gives 1 + x = 1 + y. The expected type can be an Iff, Eq, or HEq. If there is no expected type, then it generates an equality.

Note: the process of generating a congruence lemma involves elaborating the pattern using terms with attached metadata and a reducible wrapper. We try to avoid doing so, but these terms can leak into the local context through unification. This can potentially break tactics that are sensitive to metadata or reducible functions. Please report anything that goes wrong with congr(...) lemmas on Zulip.

For debugging, you can set set_option trace.Elab.congr true.

Equations

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

Congruence holes

This section sets up the way congruence holes are elaborated for congr(...) quotations. The basic problem is that if we have $h with h : x = y, we need to elaborate it once as x and once as y, and in both cases the term needs to remember that it's associated to h.

@[reducible]

def Mathlib.Tactic.TermCongr.cHole {α : Sort u} (val : α) {p : Prop} (_pf : p) : α

For holding onto the hole's value along with the value of either the LHS or RHS of the hole. These occur wrapped in metadata so that they always appear as function application with exactly four arguments.

Note that there is no relation between val and the proof. We need to decouple these to support letting the proof's elaboration be deferred until we know whether we want an iff, eq, or heq, while also allowing it to choose to elaborate as an iff, eq, or heq. Later, the congruence generator handles any discrepancies. See Mathlib.Tactic.TermCongr.CongrResult.

Equations

• val = val

def Mathlib.Tactic.TermCongr.unexpandCHole : Lean.PrettyPrinter.Unexpander

For error reporting purposes, make the hole pretty print as its value. We can still see that it is a hole in the info view on mouseover.

Equations

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

def Mathlib.Tactic.TermCongr.mkCHole (forLhs : Bool) (val : Lean.Expr) (pf : Lean.Expr) : Lean.MetaM Lean.Expr

Create the congruence hole. Used by elabCHole.

Saves the current mvarCounter as a proxy for age. We use this to avoid reprocessing old congruence holes that happened to leak into the local context.

Equations

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

def Mathlib.Tactic.TermCongr.cHole? (e : Lean.Expr) (mvarCounterSaved? : optParam (Option ℕ) none) : Option (Bool × Lean.Expr × Lean.Expr)

If the expression is a congruence hole, returns (forLhs, sideVal, pf). If mvarCounterSaved? is not none, then only returns the hole if it is at least as recent.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.TermCongr.cHole? e mvarCounterSaved? = none

def Mathlib.Tactic.TermCongr.hasCHole (mvarCounterSaved : ℕ) (e : Lean.Expr) : Option Lean.Expr

Returns any subexpression that is a recent congruence hole.

Equations

• Mathlib.Tactic.TermCongr.hasCHole mvarCounterSaved e = Lean.Expr.find? (fun (e' : Lean.Expr) => (Mathlib.Tactic.TermCongr.cHole? e' (some mvarCounterSaved)).isSome) e

def Mathlib.Tactic.TermCongr.removeCHoles (e : Lean.Expr) : Lean.Expr

Eliminate all congruence holes from an expression by replacing them with their values.

Equations

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

def Mathlib.Tactic.TermCongr.elabCHole (h : Lean.Syntax) (forLhs : Bool) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Elaborates a congruence hole and returns either the left-hand side or the right-hand side, annotated with information necessary to generate a congruence lemma.

Equations

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

def Mathlib.Tactic.TermCongr.cHoleExpand : Lean.ParserDescr

(Internal for congr(...)) Elaborates to an expression satisfying cHole? that equals the LHS or RHS of h, if the LHS or RHS is available after elaborating h. Uses the expected type as a hint.

Equations

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

def Mathlib.Tactic.TermCongr.elabCHoleExpand : Lean.Elab.Term.TermElab

(Internal for congr(...)) Elaborates to an expression satisfying cHole? that equals the LHS or RHS of h, if the LHS or RHS is available after elaborating h. Uses the expected type as a hint.

Equations

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

def Mathlib.Tactic.TermCongr.processAntiquot (t : Lean.Term) (expand : Lean.Term → Lean.Elab.TermElabM Lean.Term) : Lean.Elab.TermElabM Lean.Term

Replace all term antiquotations in a term using the given expand function.

Equations

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

def Mathlib.Tactic.TermCongr.elaboratePattern (t : Lean.Term) (expectedType? : Option Lean.Expr) (forLhs : Bool) : Lean.Elab.TermElabM Lean.Expr

Given the pattern t in congr(t), elaborate it for the given side by replacing antiquotations with cHole% terms, and ensure the elaborated term is of the expected type.

Equations

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

Congruence generation

def Mathlib.Tactic.TermCongr.mkEqForExpectedType (expectedType? : Option Lean.Expr) : Lean.MetaM Lean.Expr

Ensures the expected type is an equality. Returns the equality. The returned expression satisfies Lean.Expr.eq?.

Equations

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

def Mathlib.Tactic.TermCongr.mkHEqForExpectedType (expectedType? : Option Lean.Expr) : Lean.MetaM Lean.Expr

Ensures the expected type is a HEq. Returns the HEq. This expression satisfies Lean.Expr.heq?.

Equations

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

def Mathlib.Tactic.TermCongr.mkIffForExpectedType (expectedType? : Option Lean.Expr) : Lean.MetaM Lean.Expr

Ensures the expected type is an iff. Returns the iff. This expression satisfies Lean.Expr.iff?.

Equations

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

def Mathlib.Tactic.TermCongr.ensureIff (pf : Lean.Expr) : Lean.MetaM Lean.Expr

Make sure that the expected type of pf is an iff by unification.

Equations

• Mathlib.Tactic.TermCongr.ensureIff pf = do let __do_lift ← Lean.Meta.inferType pf discard (Mathlib.Tactic.TermCongr.mkIffForExpectedType (some __do_lift)) pure pf

inductive Mathlib.Tactic.TermCongr.CongrType : Type

A request for a type of congruence lemma from a CongrResult.

• eq: Mathlib.Tactic.TermCongr.CongrType
• heq: Mathlib.Tactic.TermCongr.CongrType

structure Mathlib.Tactic.TermCongr.CongrResult : Type

A congruence lemma between two expressions. The proof is generated dynamically, depending on whether the resulting lemma should be an Eq or a HEq. If generating a proof impossible, then the generator can throw an error. This can be due to either an Eq proof being impossible or due to the lhs/rhs not being defeq to the lhs/rhs of the generated proof, which can happen for user-supplied congruence holes.

This complexity is to support two features:

1. The user is free to supply Iff, Eq, and HEq lemmas in congurence holes, and we're able to transform them into whatever is appropriate for a given congruence lemma.
2. If the congrence hole is a metavariable, then we can specialize that hole to an Iff, Eq, or HEq depending on what's necessary at that site.

• lhs : Lean.Expr

  The left-hand side of the congruence result.

• rhs : Lean.Expr

  The right-hand side of the congruence result.

• pf? : Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr)

  A generator for an Eq lhs rhs or HEq lhs rhs proof. If such a proof is impossible, the generator can throw an error. The inferred type of the generated proof needs only be defeq to Eq lhs rhs or HEq lhs rhs. This function can assign metavariables when constructing the proof.

  If pf? = none, then lhs and rhs are defeq, and the proof is by reflexivity.

def Mathlib.Tactic.TermCongr.CongrResult.isRfl (res : Mathlib.Tactic.TermCongr.CongrResult) : Bool

Returns whether the proof is by reflexivity. Such congruence proofs are trivial.

Equations

• res.isRfl = res.pf?.isNone

def Mathlib.Tactic.TermCongr.CongrResult.eq (res : Mathlib.Tactic.TermCongr.CongrResult) : Lean.MetaM Lean.Expr

Returns the proof that lhs = rhs. Fails if the CongrResult is inapplicable. Throws an error if the lhs and rhs have non-defeq types. If pf? = none, this returns the rfl proof.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.heq (res : Mathlib.Tactic.TermCongr.CongrResult) : Lean.MetaM Lean.Expr

Returns the proof that HEq lhs rhs. Fails if the CongrResult is inapplicable. If pf? = none, this returns the rfl proof.

Equations

• res.heq = match res.pf? with | some pf => pf Mathlib.Tactic.TermCongr.CongrType.heq | none => Lean.Meta.mkHEqRefl res.lhs

def Mathlib.Tactic.TermCongr.CongrResult.iff (res : Mathlib.Tactic.TermCongr.CongrResult) : Lean.MetaM Lean.Expr

Returns a proof of lhs ↔ rhs. Uses CongrResult.eq.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.trans (res1 : Mathlib.Tactic.TermCongr.CongrResult) (res2 : Mathlib.Tactic.TermCongr.CongrResult) : Mathlib.Tactic.TermCongr.CongrResult

Combine two congruence proofs using transitivity. Does not check that res1.rhs is defeq to res2.lhs. If both res1 and res2 are trivial then the result is trivial.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.mk' (lhs : Lean.Expr) (rhs : Lean.Expr) (pf : Lean.Expr) : Mathlib.Tactic.TermCongr.CongrResult

Make a CongrResult from a LHS, a RHS, and a proof of an Iff, Eq, or HEq. The proof is allowed to have a metavariable for its type. Validates the inputs and throws errors in the pf? function.

The pf? function is responsible for finally unifying the type of pf with lhs and rhs.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.mk'.toEqPf (lhs : Lean.Expr) (pf : Lean.Expr) : Lean.MetaM Lean.Expr

Given a pf of an Iff, Eq, or HEq, return a proof of Eq. If pf is not obviously any of these, weakly try inserting propext to make an Iff and otherwise unify the type with Eq.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.mk'.toHEqPf (lhs : Lean.Expr) (rhs : Lean.Expr) (pf : Lean.Expr) : Lean.MetaM Lean.Expr

Given a pf of an Iff, Eq, or HEq, return a proof of HEq. If pf is not obviously any of these, weakly try making it be an Eq or an Iff, and otherwise make it be a HEq.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.mk'.ensureSidesDefeq (lhs : Lean.Expr) (rhs : Lean.Expr) (pf : Lean.Expr) : Lean.MetaM Lean.Expr

Get the sides of the type of pf and unify them with the respective lhs and rhs.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.defeq (res : Mathlib.Tactic.TermCongr.CongrResult) : Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult

Force the lhs and rhs to be defeq. For when dsimp-like congruence is necessary. Clears the proof.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.mkDefault (lhs : Lean.Expr) (rhs : Lean.Expr) : Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult

Tries to make a congruence between lhs and rhs automatically.

1. If they are defeq, returns a trivial congruence.
2. Tries using Subsingleton.elim.
3. Tries proof_irrel_heq as another effort to avoid doing congruence on proofs.
4. Otherwise throws an error.

Note: mkAppM uses withNewMCtxDepth, which prevents typeclass inference from accidentally specializing Sort _ to Prop, which could otherwise happen because there is a Subsingleton Prop instance.

Equations

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

def Mathlib.Tactic.TermCongr.CongrResult.mkDefault' (mvarCounterSaved : ℕ) (lhs : Lean.Expr) (rhs : Lean.Expr) : Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult

Does CongrResult.mkDefault but makes sure there are no lingering congruence holes.

Equations

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

def Mathlib.Tactic.TermCongr.throwCongrEx {α : Type} (lhs : Lean.Expr) (rhs : Lean.Expr) (msg : Lean.MessageData) : Lean.MetaM α

Throw an internal error.

Equations

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

def Mathlib.Tactic.TermCongr.mkCongrOfCHole? (mvarCounterSaved : ℕ) (lhs : Lean.Expr) (rhs : Lean.Expr) : Lean.MetaM (Option Mathlib.Tactic.TermCongr.CongrResult)

If lhs or rhs is a congruence hole, then process it. Only process ones that are at least as new as mvarCounterSaved since nothing prevents congruence holes from leaking into the local context.

Equations

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

partial def Mathlib.Tactic.TermCongr.mkCongrOf (depth : ℕ) (mvarCounterSaved : ℕ) (lhs : Lean.Expr) (rhs : Lean.Expr) : Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult

Walks along both lhs and rhs simultaneously to create a congruence lemma between them.

Where they are desynchronized, we fall back to the base case (using CongrResult.mkDefault') since it's likely due to unification with the expected type, from _ placeholders or implicit arguments being filled in.

Elaborating congruence quotations

def Mathlib.Tactic.TermCongr.elabTermCongr : Lean.Elab.Term.TermElab

congr(expr) generates an congruence from an expression containing congruence holes of the form $h or $(h). In these congruence holes, h : a = b indicates that, in the generated congruence, on the left-hand side a is substituted for $h and on the right-hand side b is substituted for $h.

For example, if h : a = b then congr(1 + $h) : 1 + a = 1 + b.

This is able to make use of the expected type, for example (congr(_ + $h) : 1 + _ = _) with h : x = y gives 1 + x = 1 + y. The expected type can be an Iff, Eq, or HEq. If there is no expected type, then it generates an equality.

Note: the process of generating a congruence lemma involves elaborating the pattern using terms with attached metadata and a reducible wrapper. We try to avoid doing so, but these terms can leak into the local context through unification. This can potentially break tactics that are sensitive to metadata or reducible functions. Please report anything that goes wrong with congr(...) lemmas on Zulip.

For debugging, you can set set_option trace.Elab.congr true.

Equations

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