Documentation

Mathlib.Lean.Meta.CongrTheorems

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.

Equations
Instances For

    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.
    Instances For

      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

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

        Instances

          The subsingleton instance.

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

          Instances
            theorem Lean.Meta.FastSubsingleton.elim {α : Sort u} [h : Lean.Meta.FastSubsingleton α] (a : α) (b : α) :
            a = b
            @[instance 100]
            Equations
            • =
            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
            • =

            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

              Like subsingletonElim but uses FastSubsingleton to fail fast.

              Equations
              • One or more equations did not get rendered due to their size.
              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 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.
                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

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

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

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

                        Driver for trySolveCore.

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