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
Similar to forallTelescopeReducing
, but
Eliminates arguments for named parameters and the associated equation proofs.
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 alternativealt
that has typealtType
.ys.size <= args.size
mask[i]
is true if the hypotheses has not been eliminated.mask.size == args.size
.type
is the resulting type foraltType
.
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 withh : discr
.args
are the arguments for the alternativealt
that has typealtType
.ys.size <= args.size
mask[i]
is true if the hypotheses has not been eliminated.mask.size == args.size
.type
is the resulting type foraltType
.
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
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
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
Instances For
Instances For
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
- solved : InjectionAnyResult
- failed : InjectionAnyResult
- subgoal
(fvarId : FVarId)
(mvarId : MVarId)
: InjectionAnyResult
fvarId
refers to the local declaration selected for the application of theinjection
tactic.
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
Equations
- Lean.Meta.Match.congrEqnThmSuffixBase = "congr_eq"
Instances For
Instances For
Instances For
Returns true
if s
is of the form congr_eq_<idx>
Equations
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
Equations
- One or more equations did not get rendered due to their size.