Additions to Lean.Meta.CongrTheorems
#
Generates a congruence lemma for a function f
for numArgs
of its arguments.
The only Lean.Meta.CongrArgKind
kinds that appear in such a lemma
are .eq
, .heq
, and .subsingletonInst
.
The resulting lemma proves either an Eq
or a HEq
depending on whether the types
of the LHS and RHS are equal or not.
This function is a wrapper around Lean.Meta.mkHCongrWithArity
.
It transforms the resulting congruence lemma by trying to automatically prove hypotheses
using subsingleton lemmas, and if they are so provable they are recorded with .subsingletonInst
.
Note that this is slightly abusing .subsingletonInst
since
(1) the argument might not be for a Decidable
instance and
(2) the argument might not even be an instance.
Instances For
Process the congruence theorem by trying to preprove arguments using prove
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Close the goal given only the fvars in params
, or else fails.
Instances For
mkRichHCongr fType funInfo fixedFun fixedParams forceHEq
create a congruence lemma to prove that Eq/HEq (f a₁ ... aₙ) (f' a₁' ... aₙ')
.
The functions have type fType
and the number of arguments is governed by the funInfo
data.
Each argument produces an Eq/HEq aᵢ aᵢ'
hypothesis, but we also provide these hypotheses
the additional facts that the preceding equalities have been proved (unlike in mkHCongrWithArity
).
The first two arguments of the resulting theorem are for f
and f'
, followed by a proof
of f = f'
, unless fixedFun
is true
(see below).
When including hypotheses about previous hypotheses, we make use of dependency information and only include relevant equalities.
The argument fty
denotes the type of f
. The arity of the resulting congruence lemma is
controlled by the size of the info
array.
For the purpose of generating nicer lemmas (to help to_additive
for example),
this function supports generating lemmas where certain parameters
are meant to be fixed:

If
fixedFun
isfalse
(the default) then the lemma starts with three arguments forf
,f'
, andh : f = f'
. Otherwise, iffixedFun
istrue
then the lemma starts with justf
. 
If the
fixedParams
argument hastrue
for a particular argument index, then this is a hint that the congruence lemma may use the same parameter for both sides of the equality. There is no guarantee  it respects it if the types are equal for that parameter (i.e., if the parameter does not depend on nonfixed parameters).
If forceHEq
is true
then the conclusion of the generated theorem is a HEq
.
Otherwise it might be an Eq
if the equality is homogeneous.
This is the interpretation of the CongrArgKind
s in the generated congruence theorem:
.eq
corresponds to having three arguments(x : α) (x' : α) (h : x = x')
. Note thath
might have additional hypotheses..heq
corresponds to having three arguments(x : α) (x' : α') (h : HEq x x')
Note thath
might have additional hypotheses..fixed
corresponds to having a single argument(x : α)
that is fixed between the LHS and RHS.subsingletonInst
corresponds to having two arguments(x : α) (x' : α')
for which the congruence generator was able to prove thatHEq x x'
already. This is a slight abuse of thisCongrArgKind
since this is used even for types that are not subsingleton typeclasses.
Note that the first entry in this array is for the function itself.
Instances For
Similar to doing forallBoundedTelescope
twice, but makes use of the fixed
array, which
is used as a hint for whether both variables should be the same. This is only a hint though,
since we respect it only if the binding domains are equal.
We affix '
to the second list of variables, and all the variables are introduced
with default binder info. Calls k
with the xs, ys, and a revised fixed
array
Instances For
Introduce variables for equalities between the arrays of variables. Uses fixedParams
to control whether to introduce an equality for each pair. The array of triples passed to k
consists of (1) the simple congr lemma HEq arg, (2) the richer HEq arg, and (3) how to
compute 1 in terms of 2.
Instances For
Given a type that is a bunch of equalities implying a goal (for example, a basic congruence lemma), prove it if possible. Basic congruence lemmas should be provable by this. There are some extra tricks for handling arguments to richer congruence lemmas.
Instances For
Driver for trySolveCore
.