Lean4
/-- Implementation for both `mk_iff` and `mk_iff_of_inductive_prop`.
-/
def mkIffOfInductivePropImpl (ind : Name) (rel : Name) (relStx : Syntax) : MetaM Unit := do
let .inductInfo inductVal ← getConstInfo ind |
throwError"mk_iff only applies to inductive declarations"
let constrs := inductVal.ctors
let params := inductVal.numParams
let type := inductVal.type
let univNames := inductVal.levelParams
let univs := univNames.map mkLevelParam
let (thmTy, shape) ←
Meta.forallTelescope type fun fvars ty ↦ do
if !ty.isProp then
throwError"mk_iff only applies to prop-valued declarations"
let lhs := mkAppN (mkConst ind univs) fvars
let fvars' := fvars.toList
let shape_rhss ← constrs.mapM (constrToProp univs (fvars'.take params) (fvars'.drop params))
let (shape, rhss) := shape_rhss.unzip
pure (← mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)), shape)
let mvar ← mkFreshExprMVar (some thmTy)
let mvarId := mvar.mvarId!
let (fvars, mvarId') ← mvarId.intros
let [mp, mpr] ← mvarId'.apply (mkConst `Iff.intro) |
throwError"failed to split goal"
toCases mp shape
let ⟨mprFvar, mpr'⟩ ← mpr.intro1
toInductive mpr' constrs ((fvars.toList.take params).map .fvar) shape mprFvar
addDecl <|
.thmDecl
{ name := rel
levelParams := univNames
type := thmTy
value := ← instantiateMVars mvar }
addDeclarationRangesFromSyntax rel (← getRef) relStx
addConstInfo relStx rel
