Additions to Lean.Meta.CongrTheorems

def Lean.Meta.mkHCongrWithArity' (f : Lean.Expr) (numArgs : ℕ) : Lean.MetaM Lean.Meta.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 #[] #[] #[] #[]

def Lean.Meta.mkHCongrWithArity'.process (cthm : Lean.Meta.CongrTheorem) (type : Lean.Expr) (argKinds : List Lean.Meta.CongrArgKind) (argKinds' : Array Lean.Meta.CongrArgKind) (params args : Array Lean.Expr) (letArgs : Array (Lean.Expr × Lean.Expr)) : Lean.MetaM Lean.Meta.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 CongrArgKinds, which this function recurses on.
• argKinds' is the accumulated array of CongrArgKinds, 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.

Equations

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

def Lean.Meta.mkHCongrWithArity'.prove (g : Lean.MVarId) (params : Array Lean.Expr) : Lean.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.

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

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

• inst : Subsingleton α

  The subsingleton instance.

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

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

• inst : IsEmpty α

theorem Lean.Meta.FastSubsingleton.elim {α : Sort u} [h : Lean.Meta.FastSubsingleton α] (a b : α) : a = b

@[instance 100]

instance Lean.Meta.instFastSubsingletonOfFastIsEmpty {α : Type u} [inst : Lean.Meta.FastIsEmpty α] : Lean.Meta.FastSubsingleton α

Equations

• ⋯ = ⋯

instance Lean.Meta.instFastSubsingleton {p : Prop} : Lean.Meta.FastSubsingleton p

Equations

• ⋯ = ⋯

instance Lean.Meta.instFastSubsingletonDecidable {p : Prop} : Lean.Meta.FastSubsingleton (Decidable p)

Equations

• ⋯ = ⋯

instance Lean.Meta.instFastSubsingletonFinOfNatNat : Lean.Meta.FastSubsingleton (Fin 1)

Equations

• Lean.Meta.instFastSubsingletonFinOfNatNat = ⋯

instance Lean.Meta.instFastSubsingletonPUnit : Lean.Meta.FastSubsingleton PUnit.{u_1}

Equations

• Lean.Meta.instFastSubsingletonPUnit = ⋯

instance Lean.Meta.instFastIsEmptyEmpty : Lean.Meta.FastIsEmpty Empty

Equations

• Lean.Meta.instFastIsEmptyEmpty = ⋯

instance Lean.Meta.instFastIsEmptyFalse : Lean.Meta.FastIsEmpty False

Equations

• Lean.Meta.instFastIsEmptyFalse = ⋯

instance Lean.Meta.instFastIsEmptyFinOfNatNat : Lean.Meta.FastIsEmpty (Fin 0)

Equations

• Lean.Meta.instFastIsEmptyFinOfNatNat = ⋯

instance Lean.Meta.instFastSubsingletonForallOfFastIsEmpty {α : Sort u} [inst : Lean.Meta.FastIsEmpty α] {β : α → Sort v} : Lean.Meta.FastSubsingleton ((x : α) → β x)

Equations

• ⋯ = ⋯

instance Lean.Meta.instFastSubsingletonForall {α : Sort u} {β : α → Sort v} [inst : ∀ (x : α), Lean.Meta.FastSubsingleton (β x)] : Lean.Meta.FastSubsingleton ((x : α) → β x)

Equations

• ⋯ = ⋯

def Lean.Meta.withSubsingletonAsFast {α : Type} [Inhabited α] (mx : (Lean.Expr → Lean.Expr) → Lean.MetaM α) : Lean.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.

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

Like subsingletonElim but uses FastSubsingleton to fail fast.

Equations

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

def Lean.Meta.mkRichHCongr (fType : Lean.Expr) (info : Lean.Meta.FunInfo) (fixedFun : Bool := false) (fixedParams : Array Bool := #[]) (forceHEq : Bool := false) : Lean.MetaM Lean.Meta.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 CongrArgKinds 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 : HEq 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 HEq 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.

def Lean.Meta.mkRichHCongr.doubleTelescope {α : Type} (fty : Lean.Expr) (numVars : ℕ) (fixed : Array Bool) (k : Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.MetaM α) : Lean.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 #[] #[] #[]

partial def Lean.Meta.mkRichHCongr.doubleTelescope.loop {α : Type} (numVars : ℕ) (fixed : Array Bool) (k : Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.MetaM α) (i : ℕ) (ftyx ftyy : Lean.Expr) (xs ys : Array Lean.Expr) (fixed' : Array Bool) : Lean.MetaM α

def Lean.Meta.mkRichHCongr.withNewEqs (info : Lean.Meta.FunInfo) {α : Type} (xs ys : Array Lean.Expr) (fixedParams : Array Bool) (k : Array Lean.Meta.CongrArgKind → Array (Option (Lean.Expr × Lean.Expr × Lean.Expr)) → Lean.MetaM α) : Lean.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 #[] #[]

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

def Lean.Meta.mkRichHCongr.trySolveCore (mvarId : Lean.MVarId) : Lean.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.

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

Driver for trySolveCore.

Equations

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