funext n times

Stream: general

[Yury G. Kudryashov]

I want to prove inside a metaprogram f = g, where f and g are n-ary functions to Prop. Is there a way to ask Lean to run funext and return a list of FVarIds and a new MVarId like docs#Lean.MVarId.intros does for intro?

[Alex J. Best]

You should be able to docs#Lean.MVarId.apply funext n times I guess, I don't know of a better way

[Yury G. Kudryashov]

I came up with (not tested yet):

def funext1 (mvarId : MVarId) (n : Option Name) : MetaM (FVarId × MVarId) := do
  let [mvarId'] ← mvarId.apply (mkConst `funext) | throwError "Expected one goal"
  mvarId'.intro <| n.getD (← mkFreshUserName `a)

def funextList (mvarId : MVarId) (names : List (Option Name)) : MetaM (List FVarId × MVarId) :=
  names.foldlM (fun ⟨fvarIds, mvarId⟩ name ↦ do
    let ⟨fvarId, mvarId⟩ ← funext1 mvarId name
    pure (fvarIds ++ [fvarId], mvarId)) ([], mvarId)

def funextN (mvarId : MVarId) (n : Nat) : MetaM (List FVarId × MVarId) :=
  funextList mvarId (.replicate n none)

[Yury G. Kudryashov]

Is there a way to write funextList so that it doesn't rebuild fvarIds every time? Should I use List.cons instead, then reverse? Or there is a better function?

[Kyle Miller]

Have it return Array FVarId and use fvarIds.push fvarId instead

[Yury G. Kudryashov]

Something like this?

def funext1 (mvarId : MVarId) (n : Option Name) : MetaM (FVarId × MVarId) := do
  let [mvarId'] ← mvarId.apply (mkConst `funext) | throwError "Expected one goal"
  mvarId'.intro <| n.getD (← mkFreshUserName `a)

def funextArray (mvarId : MVarId) (names : Array (Option Name)) : MetaM (Array FVarId × MVarId) :=
  names.foldlM (fun ⟨fvarIds, mvarId⟩ name ↦ do
    let ⟨fvarId, mvarId⟩ ← funext1 mvarId name
    pure (fvarIds.push fvarId, mvarId)) (.mkEmpty names.size, mvarId)

def funextN (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
  funextArray mvarId (.mkArray n none)

[Kyle Miller]

mkConst isn't right -- that doesn't set up universe level parameters correctly. You need docs#Lean.Meta.mkConstWithFreshMVarLevels (Mathlib gives docs#Lean.mkConst' for short, though it seems to be its own implementation)

[Yury G. Kudryashov]

I'll use&test it later today. Thanks!