Lean4
/-- Converts an inductive constructor `c` into a `Shape` that will be used later in
while proving the iff theorem, and a proposition representing the constructor.
-/
def constrToProp (univs : List Level) (params : List Expr) (idxs : List Expr) (c : Name) : MetaM (Shape × Expr) := do
let type := (← getConstInfo c).instantiateTypeLevelParams univs
let type' ←
Meta.forallBoundedTelescope type (params.length) fun fvars ty ↦ do
pure <| ty.replaceFVars fvars params.toArray
Meta.forallTelescope type' fun fvars ty ↦ do
let idxs_inst := ty.getAppArgs.toList.drop params.length
let (bs, eqs, subst) := compactRelation fvars.toList (idxs.zip idxs_inst)
let eqs ←
eqs.mapM
(fun ⟨idx, inst⟩ ↦ do
let ty ← idx.fvarId!.getType
let instTy ← inferType inst
let u := (← inferType ty).sortLevel!
if ← isDefEq ty instTy then
pure (mkApp3 (.const `Eq [u]) ty idx inst)
else
pure (mkApp4 (.const `HEq [u]) ty idx instTy inst))
let (n, r) ←
match bs.filterMap id, eqs with
| [], [] =>
do
pure (some 0, (mkConst `True))
| bs', [] =>
do
let t : Expr ← bs'.getLast!.fvarId!.getType
let l := (← inferType t).sortLevel!
if l == Level.zero then
do
let r ← mkExistsList (List.init bs') t
pure (none, subst r)
else
do
let r ← mkExistsList bs' (mkConst `True)
pure (some 0, subst r)
| bs', _ =>
do
let r ← mkExistsList bs' (mkAndList eqs)
pure (some eqs.length, subst r)
pure (⟨bs.map Option.isSome, n⟩, r)
