Documentation

Lean.Meta.Match.MatchEqs

Helper method for proveCondEqThm. Given a goal of the form C.rec ... xMajor = rhs, apply cases xMajor.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Lean.Meta.Match.forallAltVarsTelescope {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array ExprArray ExprArray BoolExprMetaM α) :

        Similar to forallTelescopeReducing, but

        1. Eliminates arguments for named parameters and the associated equation proofs.

        2. Instantiate the Unit parameter of an otherwise argumentless alternative.

        It does not handle the equality parameters associated with the h : discr notation.

        The continuation k takes four arguments ys args mask type.

        • ys are variables for the hypotheses that have not been eliminated.
        • args are the arguments for the alternative alt that has type altType. ys.size <= args.size
        • mask[i] is true if the hypotheses has not been eliminated. mask.size == args.size.
        • type is the resulting type for altType.

        We use the mask to build the splitter proof. See mkSplitterProof.

        This can be used to use the alternative of a match expression in its splitter.

        Equations
        Instances For
          partial def Lean.Meta.Match.forallAltVarsTelescope.go {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array ExprArray ExprArray BoolExprMetaM α) (ys args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.Meta.Match.forallAltTelescope {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array ExprArray ExprArray ExprArray BoolExprMetaM α) :

            Extension of forallAltTelescope that continues further:

            Equality parameters associated with the h : discr notation are replaced with rfl proofs. Recall that this kind of parameter always occurs after the parameters corresponding to pattern variables.

            The continuation k takes four arguments ys args mask type.

            • ys are variables for the hypotheses that have not been eliminated.
            • eqs are variables for equality hypotheses associated with discriminants annotated with h : discr.
            • args are the arguments for the alternative alt that has type altType. ys.size <= args.size
            • mask[i] is true if the hypotheses has not been eliminated. mask.size == args.size.
            • type is the resulting type for altType.

            We use the mask to build the splitter proof. See mkSplitterProof.

            This can be used to use the alternative of a match expression in its splitter.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              partial def Lean.Meta.Match.forallAltTelescope.go {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array ExprArray ExprArray ExprArray BoolExprMetaM α) (ys eqs args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) :
              def Lean.Meta.Match.mkAppDiscrEqs (alt : Expr) (heqs : Array Expr) (numDiscrEqs : Nat) :

              Given an application of an matcher arm alt that is expecting the numDiscrEqs, and an array of discr = pattern equalities (one for each discriminant), apply those that are expected by the alternative.

              Equations
              Instances For
                partial def Lean.Meta.Match.mkAppDiscrEqs.go (alt : Expr) (heqs : Array Expr) (numDiscrEqs : Nat) (e ty : Expr) (i : Nat) :

                State for the equational theorem hypothesis simplifier.

                Recall that each equation contains additional hypotheses to ensure the associated case does not taken by previous cases. We have one hypothesis for each previous case.

                Each hypothesis is of the form forall xs, eqsFalse

                We use tactics to minimize code duplication.

                Instances For

                  Auxiliary tactic that tries to replace as many variables as possible and then apply contradiction. We use it to discard redundant hypotheses.

                  def Lean.Meta.Match.proveCondEqThm (matchDeclName : Name) (type : Expr) (heqPos heqNum : Nat := 0) :

                  Helper method for proving a conditional equational theorem associated with an alternative of the match-eliminator matchDeclName. type contains the type of the theorem.

                  The heqPos/heqNum arguments indicate that these hypotheses are Eq/HEq hypotheses to substitute first; this is used for the generalized match equations.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    partial def Lean.Meta.Match.proveCondEqThm.go (matchDeclName : Name) (mvarId : MVarId) (depth : Nat) :
                    Instances For
                      @[export lean_get_match_equations_for]
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Lean.Meta.Match.getEquationsForImpl.go (matchDeclName baseName splitterName : Name) :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Lean.Meta.Match.registerMatchcongrEqns (matchDeclName : Name) (eqnNames : Array Name) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Generate the congruence equations for the given match auxiliary declaration. The congruence equations have a completely unrestriced left-hand side (arbitrary discriminants), and take propositional equations relating the discriminants to the patterns as arguments. In this sense they combine a congruence lemma with the regular equation lemma. Since the motive depends on the discriminants, they are HEq equations.

                            The code duplicates a fair bit of the logic above, and has to repeat the calculation of the notAlts. One could avoid that and generate the generalized equations eagerly above, but they are not always needed, so for now we live with the code duplication.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Lean.Meta.Match.genMatchCongrEqns.go (matchDeclName baseName : Name) :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For