Additions to Lean.Meta.CongrTheorems

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

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 : FastSubsingleton α] (a b : α) : a = b

theorem Lean.Meta.FastSubsingleton.helim {α β : Sort u} [FastSubsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≍ b

@[instance 100]

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

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

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

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

instance Lean.Meta.instFastSubsingletonPUnit : FastSubsingleton PUnit

instance Lean.Meta.instFastIsEmptyEmpty : FastIsEmpty Empty

instance Lean.Meta.instFastIsEmptyFalse : FastIsEmpty False

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

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

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

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.

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.

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