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

- 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. - 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.
- Then we simultaneously walk along the elaborated LHS and RHS expressions
to generate a congruence.
When we reach
`cHole`

s, 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.

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

.

## Instances For

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

.

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 discrepencies.
See `Mathlib.Tactic.TermCongr.CongrResult`

.

## Instances For

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.

## Instances For

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.

## Instances For

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.

## Instances For

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

## Instances For

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.

## Instances For

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

## Instances For

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

## Instances For

Replace all `term`

antiquotations in a term using the given `expand`

function.

## Instances For

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.

## Instances For

### Congruence generation #

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

.

## Instances For

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

.

## Instances For

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

.

## Instances For

Make sure that the expected type of `pf`

is an iff by unification.

## Instances For

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

.

## Instances For

- lhs : Lean.Expr
The left-hand side of the congruence result.

- rhs : Lean.Expr
The right-hand side of the congruence result.

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.

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:

- 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.
- 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.

## Instances For

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

## Instances For

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.

## Instances For

Returns the proof that `HEq lhs rhs`

. Fails if the `CongrResult`

is inapplicable.
If `pf? = none`

, this returns the `rfl`

proof.

## Instances For

Returns a proof of `lhs ↔ rhs`

. Uses `CongrResult.eq`

.

## Instances For

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.

## Instances For

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`

.

## Instances For

Force the lhs and rhs to be defeq. For when `dsimp`

-like congruence is necessary.
Clears the proof.

## Instances For

Tries to make a congruence between `lhs`

and `rhs`

automatically.

- If they are defeq, returns a trivial congruence.
- Tries using
`Subsingleton.elim`

. - Tries
`proof_irrel_heq`

as another effort to avoid doing congruence on proofs. - 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.

## Instances For

Does `CongrResult.mkDefault`

but makes sure there are no lingering congruence holes.

## Instances For

Throw an internal error.

## Instances For

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.

## Instances For

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 #

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

.