max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add elimAuxIndices

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-05 12:44:24 -08:00
parent 8d7ed8a9b8
commit 6fb526ee00
1 changed files with 20 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/Init/Lean/Meta/Tactic/Cases.lean
View file

@ -155,6 +155,17 @@ else do
ctx.majorTypeIndices.any (fun index => decl.fvarId == index.fvarId!) || -- decl is one of the indices
mctx.findLocalDeclDependsOn decl (fun fvarId => ctx.majorTypeIndices.all $ fun idx => idx.fvarId! != fvarId) -- or does not depend on any index
private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array InductionSubgoal) : MetaM (Array InductionSubgoal) :=
let indicesFVarIds := s₁.indicesFVarIds;
s₂.mapM $ fun s => do
indicesFVarIds.foldlM
(fun s indexFVarId =>
let indexFVarId' := s.subst.get indexFVarId;
(do mvarId ← clear s.mvarId indexFVarId'; pure { mvarId := mvarId, subst := s.subst.erase indexFVarId, .. s })
<|>
(pure s))
s
def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) : MetaM (Array CasesSubgoal) :=
withMVarContext mvarId $ do
checkNotAssigned mvarId `cases;
@ -162,12 +173,17 @@ withMVarContext mvarId $ do
match context? with
| none => throwTacticEx `cases mvarId "not applicable to the given hypothesis"
| some ctx =>
let ctors := ctx.inductiveVal.ctors.toArray;
let casesOn := mkCasesOnFor ctx.inductiveVal.name;
condM (hasIndepIndices ctx)
(do
r ← induction mvarId majorFVarId (mkCasesOnFor ctx.inductiveVal.name) givenNames useUnusedNames;
let ctors := ctx.inductiveVal.ctors.toArray;
pure $ r.mapIdx $ fun i s => { ctorName := ctors.get! i, toInductionSubgoal := s })
(throwTacticEx `cases mvarId "WIP")
s ← induction mvarId majorFVarId casesOn givenNames useUnusedNames;
pure $ s.mapIdx $ fun i s => { ctorName := ctors.get! i, toInductionSubgoal := s })
(do
s₁ ← generalizeIndices mvarId majorFVarId;
s₂ ← induction s₁.mvarId s₁.fvarId casesOn givenNames useUnusedNames;
s₂ ← elimAuxIndices s₁ s₂;
pure $ s₂.mapIdx $ fun i s => { ctorName := ctors.get! i, toInductionSubgoal := s })
end Cases