max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Sebastian Graf 5f4d724c2d
feat: abstract metavariables when generalizing match motives (#8099) (#11696) 
This PR improves `match` generalization such that it abstracts
metavariables in types of local variables and in the result type of the
match over the match discriminants. Previously, a metavariable in the
result type would silently default to the behavior of `generalizing :=
false`, and a metavariable in the type of a free variable would lead to
an error (#8099). Example of a `match` that elaborates now but
previously wouldn't:
```lean
example (a : Nat) (ha : a = 37) :=
    (match a with | 42 => by contradiction | n => n) = 37
```
This is because the result type of the `match` is a metavariable that
was not abstracted over `a` and hence generalization failed; the result
is that `contradiction` cannot pick up the proof `ha : 42 = 37`.
The old behavior can be recovered by passing `(generalizing := false)`
to the `match`.

Furthermore, programs such as the following can now be elaborated:
```lean
example (n : Nat) : Id (Fin (n + 1)) :=
  have jp : ?m := ?rhs
  match n with
  | 0 => ?jmp1
  | n + 1 => ?jmp2
  where finally
  case m => exact Fin (n + 1) → Id (Fin (n + 1))
  case jmp1 => exact jp ⟨0, by decide⟩
  case jmp2 => exact jp ⟨n, by omega⟩
  case rhs => exact pure
```
This is useful for the `do` elaborator.

Fixes #8099.
2025-12-16 14:34:29 +00:00
..
ArgsPacker
Constructions feat: sparse sparse casesOn splitting in match equations (#11666) 2025-12-14 14:59:45 +00:00
Match feat: abstract metavariables when generalizing match motives (#8099) (#11696) 2025-12-16 14:34:29 +00:00
Tactic feat: abstract metavariables when generalizing match motives (#8099) (#11696) 2025-12-16 14:34:29 +00:00
AbstractMVars.lean fix: instantiate mvars in types of mvars in abstractMVars (#10612) 2025-09-29 16:33:10 +00:00
AbstractNestedProofs.lean chore: more module system fixes and improvements from Mathlib porting (#10655) 2025-10-08 11:30:09 +00:00
ACLt.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
AppBuilder.lean feat: heterogeneous noConfusion (#11474) 2025-12-02 15:19:47 +00:00
ArgsPacker.lean
Basic.lean feat: abstract metavariables when generalizing match motives (#8099) (#11696) 2025-12-16 14:34:29 +00:00
BinderNameHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Canonicalizer.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
CasesInfo.lean chore: fix spelling (#11531) 2025-12-06 13:54:27 +00:00
Check.lean fix: deep recursion type checking grind proof (#11061) 2025-11-02 19:43:48 +00:00
CheckTactic.lean
Closure.lean chore: add an assertion about mkValueTypeClosure (#10954) 2025-10-25 12:59:17 +00:00
Coe.lean feat: lint coercions that are deprecated or banned in core (#11511) 2025-12-12 15:09:13 +00:00
CoeAttr.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
CollectFVars.lean
CollectMVars.lean
CompletionName.lean refactor: move operations on String.Pos.Raw to the String.Pos.Raw namespace (#10735) 2025-10-18 12:12:55 +00:00
CongrTheorems.lean refactor: use withImplicitBinderInfos and mkArrowN in more places (#11492) 2025-12-03 08:42:16 +00:00
Constructions.lean feat: sparse sparse casesOn splitting in match equations (#11666) 2025-12-14 14:59:45 +00:00
CtorIdxHInj.lean feat: grind support for .ctorIdx (#11652) 2025-12-13 13:32:19 +00:00
CtorRecognizer.lean
DecLevel.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Diagnostics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
DiscrTree.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
DiscrTreeTypes.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Eqns.lean chore: fix spelling (#11531) 2025-12-06 13:54:27 +00:00
Eval.lean fix: #guard should work with the module system (#10535) 2025-09-24 07:38:10 +00:00
ExprDefEq.lean chore: fix spelling (#11531) 2025-12-06 13:54:27 +00:00
ExprLens.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ExprTraverse.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ForEachExpr.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
FunInfo.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
GeneralizeTelescope.lean
GeneralizeVars.lean
GetUnfoldableConst.lean feat: list definitions in defeq problems that could not be unfolded for lack of @[expose] (#10158) 2025-09-23 16:13:39 +00:00
GlobalInstances.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
HasNotBit.lean perf: use Nat-based bitmask in sparse cases construction (#11200) 2025-11-17 10:05:18 +00:00
Hint.lean chore: rename Substring to Substring.Raw (#11154) 2025-11-16 09:30:04 +00:00
IndPredBelow.lean chore: fix spelling (#11531) 2025-12-06 13:54:27 +00:00
Inductive.lean
InferType.lean feat: don't count symbols in instances and proofs 2025-10-26 10:29:47 +11:00
Injective.lean feat: make noConfusion even more heterogeneous 2025-12-10 17:28:06 +01:00
Instances.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
IntInstTesters.lean
Iterator.lean
KAbstract.lean
KExprMap.lean
LazyDiscrTree.lean feat: add +all option to exact? and apply? (#11556) 2025-12-11 03:30:52 +00:00
LetToHave.lean chore: fix spelling errors (#10042) 2025-08-22 07:23:12 +00:00
LevelDefEq.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
LitValues.lean feat: support for Rat scientific literals (#10961) 2025-10-26 02:05:26 +00:00
Match.lean
MatchUtil.lean refactor: make MatchEqs a leaf module (#11493) 2025-12-03 09:15:36 +00:00
MethodSpecs.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MkIffOfInductiveProp.lean chore: minor optimizations on the critical path (#10900) 2025-10-22 19:32:26 +00:00
NatInstTesters.lean
NatTable.lean chore: fix spelling errors (#10042) 2025-08-22 07:23:12 +00:00
Offset.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Order.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
PPGoal.lean chore: do not set unused Option.Decl.group (#11307) 2025-11-21 16:44:38 +00:00
PProdN.lean fix: complete overhaul of structural recursion on inductives predicates (#9995) 2025-09-01 08:17:58 +00:00
ProdN.lean feat: new do elaborator, part 1: doElem_elab attribute (#11150) 2025-11-12 14:25:28 +00:00
RecursorInfo.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Reduce.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ReduceEval.lean feat: upstream ReduceEval instances from quote4 (#10563) 2025-09-26 04:02:55 +00:00
SameCtorUtils.lean refactor: introduce SameCtorUtils (#10316) 2025-09-10 14:32:58 +00:00
SizeOf.lean feat: mark sizeOf theorems as grind theorems (#11265) 2025-11-19 18:38:35 +00:00
Sorry.lean feat: pretty print sorry in "declaration uses 'sorry'" (#10034) 2025-09-08 12:14:42 +00:00
SplitSparseCasesOn.lean feat: sparse sparse casesOn splitting in match equations (#11666) 2025-12-14 14:59:45 +00:00
Structure.lean perf: more environment blocking avoidance (#11616) 2025-12-12 13:44:58 +00:00
SynthInstance.lean feat: remove the group field of an option description (#11305) 2025-11-24 11:40:58 +00:00
Tactic.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Transform.lean chore: fix spelling (#11531) 2025-12-06 13:54:27 +00:00
TransparencyMode.lean
TryThis.lean chore: rename String.ValidPos to String.Pos (#11240) 2025-11-24 16:40:21 +00:00
UnificationHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
WHNF.lean perf: do not consult isNoConfusion in whnf (#11571) 2025-12-09 23:36:46 +00:00