def Lean.Meta.casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId)

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

partial def Lean.Meta.casesOnStuckLHS.findFVar? (e : Expr) : MetaM (Option FVarId)

def Lean.Meta.casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId))

def Lean.Meta.Match.unfoldNamedPattern (e : Expr) : MetaM Expr

def Lean.Meta.Match.forallAltVarsTelescope {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array Expr → Array Expr → Array Bool → Expr → MetaM α) : MetaM α

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.

partial def Lean.Meta.Match.forallAltVarsTelescope.go {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array Expr → Array Expr → Array Bool → Expr → MetaM α) (ys args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α

def Lean.Meta.Match.forallAltVarsTelescope.isNamedPatternProof (type h : Expr) : Bool

def Lean.Meta.Match.forallAltTelescope {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array Expr → Array Expr → Array Expr → Array Bool → Expr → MetaM α) : MetaM α

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.

partial def Lean.Meta.Match.forallAltTelescope.go {α : Type} (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : Array Expr → Array Expr → Array Expr → Array Bool → Expr → MetaM α) (ys eqs args : Array Expr) (mask : Array Bool) (i : Nat) (type : Expr) : MetaM α

def Lean.Meta.Match.mkAppDiscrEqs (alt : Expr) (heqs : Array Expr) (numDiscrEqs : Nat) : MetaM Expr

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.

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

structure Lean.Meta.Match.SimpH.State : Type

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, eqs → False

We use tactics to minimize code duplication.

• mvarId : MVarId
• xs : List FVarId
• eqs : List FVarId
• eqsNew : List FVarId

@[reducible, inline]

abbrev Lean.Meta.Match.SimpH.M (α : Type) : Type

partial def Lean.Meta.Match.SimpH.trySubstVarsAndContradiction (mvarId : MVarId) (forbidden : FVarIdSet := ∅) : MetaM Bool

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

partial def Lean.Meta.Match.SimpH.go : M Bool

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

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.

partial def Lean.Meta.Match.proveCondEqThm.go (matchDeclName : Name) (mvarId : MVarId) (depth : Nat) : MetaM Unit

inductive Lean.Meta.Match.InjectionAnyResult : Type

• solved : InjectionAnyResult
• failed : InjectionAnyResult
• subgoal (fvarId : FVarId) (mvarId : MVarId) : InjectionAnyResult

  fvarId refers to the local declaration selected for the application of the injection tactic.

@[export lean_get_match_equations_for]

def Lean.Meta.Match.getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns

def Lean.Meta.Match.getEquationsForImpl.go (matchDeclName baseName splitterName : Name) : MetaM Unit

def Lean.Meta.Match.congrEqnThmSuffixBase : String

def Lean.Meta.Match.congrEqnThmSuffixBasePrefix : String

def Lean.Meta.Match.congrEqn1ThmSuffix : String

def Lean.Meta.Match.isCongrEqnReservedNameSuffix (s : String) : Bool

Returns true if s is of the form congr_eq_<idx>

opaque Lean.Meta.Match.matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name))

def Lean.Meta.Match.registerMatchcongrEqns (matchDeclName : Name) (eqnNames : Array Name) : CoreM Unit

def Lean.Meta.Match.genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name)

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.

def Lean.Meta.Match.genMatchCongrEqns.go (matchDeclName baseName : Name) : MetaM Unit