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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- Lean.Meta.Match.forallAltVarsTelescope altType altNumParams numDiscrEqs k = Lean.Meta.Match.forallAltVarsTelescope.go✝ altType altNumParams numDiscrEqs k #[] #[] #[] 0 altType

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- Lean.Meta.Match.mkAppDiscrEqs alt heqs numDiscrEqs = do let __do_lift ← Lean.Meta.inferType alt Lean.Meta.Match.mkAppDiscrEqs.go✝ alt heqs numDiscrEqs alt __do_lift 0

Instances For

source
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

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Match.SimpH.M (α : Type) :
Type
Equations

- Lean.Meta.Match.SimpH.M = StateRefT' IO.RealWorld Lean.Meta.Match.SimpH.State Lean.MetaM

Instances For

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

source
partial def Lean.Meta.Match.SimpH.go :
M Bool
source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Instances For

source
@[export lean_get_match_equations_for]
def Lean.Meta.Match.getEquationsForImpl (matchDeclName : Name) :
MetaM MatchEqns
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
opaque Lean.Meta.Match.matchCongrEqnsExt :
EnvExtension (PHashMap Name (Array Name))
source
def Lean.Meta.Match.registerMatchCongrEqns (matchDeclName : Name) (eqnNames : Array Name) :
CoreM Unit
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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 unrestricted 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