Additions to Lean.Meta.CongrTheorems

def Lean.Meta.mkHCongrWithArity' (f : Lean.Expr) (numArgs : Nat) : 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 (Array.toList thm.argKinds) #[] #[] #[]

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

Process the congruence theorem by trying to pre-prove arguments using 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.

def Lean.Meta.mkRichHCongr (fType : Lean.Expr) (info : Lean.Meta.FunInfo) (fixedFun : optParam Bool false) (fixedParams : optParam (Array Bool) #[]) (forceHEq : optParam 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 : Nat) (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 : Nat) (fixed : Array Bool) (k : Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.MetaM α) (i : Nat) (ftyx : Lean.Expr) (ftyy : Lean.Expr) (xs : Array Lean.Expr) (ys : Array Lean.Expr) (fixed' : Array Bool) : Lean.MetaM α

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