# Additions to `Lean.Meta.CongrTheorems` #

source
def Lean.Meta.mkHCongrWithArity' (f : Expr) (numArgs : ℕ) :
MetaM CongrTheorem

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.

Equations

- Lean.Meta.mkHCongrWithArity' f numArgs = do let thm ← Lean.Meta.mkHCongrWithArity f numArgs Lean.Meta.mkHCongrWithArity'.process thm thm.type thm.argKinds.toList #[] #[] #[] #[]

Instances For

source
def Lean.Meta.mkHCongrWithArity'.process (cthm : CongrTheorem) (type : Expr) (argKinds : List CongrArgKind) (argKinds' : Array CongrArgKind) (params args : Array Expr) (letArgs : Array (Expr × Expr)) :
MetaM CongrTheorem

Process the congruence theorem by trying to pre-prove arguments using `prove`.

- `cthm` is the original `CongrTheorem`, modified only after visiting every argument.
- `type` is type of the congruence theorem, after all the parameters so far have been applied.
- `argKinds` is the list of `CongrArgKind`s, which this function recurses on.
- `argKinds'` is the accumulated array of `CongrArgKind`s, which is the original array but with some kinds replaced by `.subsingletonInst`.
- `params` is the new list of parameters, as fvars that need to be abstracted at the end.
- `args` is the list of arguments (fvars) to supply to `cthm.proof` before abstracting `params`.
- `letArgs` records `(fvar, expr)` assignments for each `fvar` that was solved for by `prove`.

Instances For

source
def Lean.Meta.mkHCongrWithArity'.prove (g : MVarId) (params : Array Expr) :
MetaM Unit

Close the goal given only the fvars in `params`, or else fails.

Equations

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

Instances For

source
class Lean.Meta.FastSubsingleton (α : Sort u) :
Prop

A version of `Subsingleton` with few instances. It should fail fast.

- inst : Subsingleton α

  The subsingleton instance.

Instances

source
class Lean.Meta.FastIsEmpty (α : Sort u) :
Prop

A version of `IsEmpty` with few instances. It should fail fast.

- inst : IsEmpty α

Instances

source
theorem Lean.Meta.FastSubsingleton.elim {α : Sort u} [h : FastSubsingleton α] (a b : α) :
a = b
source
theorem Lean.Meta.FastSubsingleton.helim {α β : Sort u} [FastSubsingleton α] (h₂ : α = β) (a : α) (b : β) :
a ≍ b
source
@[instance 100]
instance Lean.Meta.instFastSubsingletonOfFastIsEmpty {α : Type u} [inst : FastIsEmpty α] :
FastSubsingleton α
source
instance Lean.Meta.instFastSubsingleton {p : Prop} :
FastSubsingleton p
source
instance Lean.Meta.instFastSubsingletonDecidable {p : Prop} :
FastSubsingleton (Decidable p)
source
instance Lean.Meta.instFastSubsingletonFinOfNatNat :
FastSubsingleton (Fin 1)
source
instance Lean.Meta.instFastSubsingletonPUnit :
FastSubsingleton PUnit.{u_1}
source
instance Lean.Meta.instFastIsEmptyEmpty :
FastIsEmpty Empty
source
instance Lean.Meta.instFastIsEmptyFalse :
FastIsEmpty False
source
instance Lean.Meta.instFastIsEmptyFinOfNatNat :
FastIsEmpty (Fin 0)
source
instance Lean.Meta.instFastSubsingletonForallOfFastIsEmpty {α : Sort u} [inst : FastIsEmpty α] {β : α → Sort v} :
FastSubsingleton ((x : α) → β x)
source
instance Lean.Meta.instFastSubsingletonForall {α : Sort u} {β : α → Sort v} [inst : ∀ (x : α), FastSubsingleton (β x)] :
FastSubsingleton ((x : α) → β x)
source
def Lean.Meta.withSubsingletonAsFast {α : Type} [Inhabited α] (mx : (Expr → Expr) → MetaM α) :
MetaM α

Runs `mx` in a context where all local `Subsingleton` and `IsEmpty` instances have associated `FastSubsingleton` and `FastIsEmpty` instances. The function passed to `mx` eliminates these instances from expressions, since they are only locally valid inside this context.

Equations

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

Instances For

source
def Lean.Meta.fastSubsingletonElim (mvarId : MVarId) :
MetaM Bool

Like `subsingletonElim` but uses `FastSubsingleton` to fail fast.

Equations

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

Instances For

source
def Lean.Meta.mkRichHCongr (fType : Expr) (info : FunInfo) (fixedFun : Bool := false) (fixedParams : Array Bool := #[]) (forceHEq : Bool := false) :
MetaM CongrTheorem

`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` is `false` (the default) then the lemma starts with three arguments for `f`, `f'`, and `h : f = f'`. Otherwise, if `fixedFun` is `true` then the lemma starts with just `f`.

- If the `fixedParams` argument has `true` 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 non-fixed 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 that `h` might have additional hypotheses.
- `.heq` corresponds to having three arguments `(x : α) (x' : α') (h : x ≍ x')` Note that `h` 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 that `x ≍ x'` already. This is a slight abuse of this `CongrArgKind` 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.

Equations

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

Instances For

source
def Lean.Meta.mkRichHCongr.doubleTelescope {α : Type} (fty : Expr) (numVars : ℕ) (fixed : Array Bool) (k : Array Expr → Array Expr → Array Bool → MetaM α) :
MetaM α

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

Equations

- Lean.Meta.mkRichHCongr.doubleTelescope fty numVars fixed k = Lean.Meta.mkRichHCongr.doubleTelescope.loop numVars fixed k 0 fty fty #[] #[] #[]

Instances For

source
partial def Lean.Meta.mkRichHCongr.doubleTelescope.loop {α : Type} (numVars : ℕ) (fixed : Array Bool) (k : Array Expr → Array Expr → Array Bool → MetaM α) (i : ℕ) (ftyx ftyy : Expr) (xs ys : Array Expr) (fixed' : Array Bool) :
MetaM α
source
def Lean.Meta.mkRichHCongr.withNewEqs (info : FunInfo) {α : Type} (xs ys : Array Expr) (fixedParams : Array Bool) (k : Array CongrArgKind → Array (Option (Expr × Expr × Expr)) → MetaM α) :
MetaM α

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.

Equations

- Lean.Meta.mkRichHCongr.withNewEqs info xs ys fixedParams k = Lean.Meta.mkRichHCongr.withNewEqs.loop info xs ys fixedParams k 0 #[] #[]

Instances For

source
partial def Lean.Meta.mkRichHCongr.withNewEqs.loop (info : FunInfo) {α : Type} (xs ys : Array Expr) (fixedParams : Array Bool) (k : Array CongrArgKind → Array (Option (Expr × Expr × Expr)) → MetaM α) (i : ℕ) (kinds : Array CongrArgKind) (eqs : Array (Option (Expr × Expr × Expr))) :
MetaM α
source
def Lean.Meta.mkRichHCongr.trySolveCore (mvarId : MVarId) :
MetaM Unit

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.

Equations

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

Instances For

source
def Lean.Meta.mkRichHCongr.trySolve (ty : Expr) :
MetaM (Option Expr)

Driver for `trySolveCore`.

Equations

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

Instances For