Lean4
/-- Proves the right to left direction of a generated iff theorem.
-/
def toInductive (mvar : MVarId) (cs : List Name) (gs : List Expr) (s : List Shape) (h : FVarId) : MetaM Unit := do
match s.length with
| 0 =>
do
let _ ← mvar.cases h
pure ()
| (n + 1) =>
do
let subgoals ← nCasesSum n mvar h
let _ ←
(cs.zip (subgoals.zip s)).mapM fun ⟨constr_name, ⟨h, mv⟩, bs, e⟩ ↦ do
let n := (bs.filter id).length
let (mvar', _fvars) ←
match e with
| none =>
nCasesProd (n - 1) mv h
| some 0 =>
do
let ⟨mvar', fvars⟩ ← nCasesProd n mv h
let mvar'' ← mvar'.tryClear fvars.getLast!
pure ⟨mvar'', fvars⟩
| some (e + 1) =>
do
let (mv', fvars) ← nCasesProd n mv h
let lastfv := fvars.getLast!
let (mv2, fvars') ← nCasesProd e mv' lastfv
let (_, mv3) ← mv2.revert fvars'.toArray
let mv4 ←
fvars'.foldlM
(fun mv _ ↦ do
let ⟨fv, mv'⟩ ← mv.intro1;
subst mv' fv)
mv3
pure (mv4, fvars)
mvar'.withContext do
let fvarIds := (← getLCtx).getFVarIds.toList
let gs := fvarIds.take gs.length
let hs := (fvarIds.reverse.take n).reverse
let m := gs.map some ++ listBoolMerge bs hs
let args ←
m.mapM fun a ↦
match a with
| some v => pure (mkFVar v)
| none => mkFreshExprMVar none
let c ← mkConstWithFreshMVarLevels constr_name
let e := mkAppN c args.toArray
let t ← inferType e
let mt ← mvar'.getType
let _ ← isDefEq t mt
mvar'.assign e
