refactor: Introduce PProdN module (#4807)

code to create nested `PProd`s, and project out, and related functions were scattered in variuos places. This unifies them in `Lean.Meta.PProdN`. It also consistently avoids the terminal `True` or `PUnit`, for slightly easier to read constructions.
2024-07-22 13:56:50 +02:00 · 2024-07-22 13:56:50 +02:00 · 3a4d2cded3
commit 3a4d2cded3
parent 22ae04f3e7
10 changed files with 201 additions and 286 deletions
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@ -5,11 +5,11 @@ Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Util.HasConstCache
+import Lean.Meta.PProdN
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.Structural.FunPacker
 import Lean.Elab.PreDefinition.Structural.RecArgInfo

 namespace Lean.Elab.Structural
@ -21,11 +21,11 @@ private def throwToBelowFailed : MetaM α :=
 partial def searchPProd (e : Expr) (F : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
  match (← whnf e) with
  | .app (.app (.const `PProd _) d1) d2 =>
-        (do searchPProd d1 (← mkAppM ``PProd.fst #[F]) k)
-    <|> (do searchPProd d2 (← mkAppM `PProd.snd #[F]) k)
+        (do searchPProd d1 (.proj ``PProd 0 F) k)
+    <|> (do searchPProd d2 (.proj ``PProd 1 F) k)
  | .app (.app (.const `And _) d1) d2 =>
-        (do searchPProd d1 (← mkAppM `And.left #[F]) k)
-    <|> (do searchPProd d2 (← mkAppM `And.right #[F]) k)
+        (do searchPProd d1 (.proj `And 0 F) k)
+    <|> (do searchPProd d2 (.proj `And 1 F) k)
  | .const `PUnit _
  | .const `True _ => throwToBelowFailed
  | _ => k e F
@ -85,7 +85,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
        return ((← mkFreshUserName `C), fun _ => pure t)
    withLocalDeclsD CDecls fun Cs => do
      -- We have to pack these canary motives like we packed the real motives
-      let packedCs ← positions.mapMwith packMotives motiveTypes Cs
+      let packedCs ← positions.mapMwith PProdN.packLambdas motiveTypes Cs
      let belowDict := mkAppN pre packedCs
      let belowDict := mkAppN belowDict finalArgs
      trace[Elab.definition.structural] "initial belowDict for {Cs}:{indentExpr belowDict}"
@ -250,7 +250,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
  let brecOnAux := brecOnCons 0
  -- Infer the type of the packed motive arguments
  let packedMotiveTypes ← inferArgumentTypesN indGroup.numMotives brecOnAux
-  let packedMotives ← positions.mapMwith packMotives packedMotiveTypes motives
+  let packedMotives ← positions.mapMwith PProdN.packLambdas packedMotiveTypes motives

  return fun n => mkAppN (brecOnCons n) packedMotives

@ -289,12 +289,11 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
    let brecOn := brecOnConst recArgInfo.indIdx
    let brecOn := mkAppN brecOn indexMajorArgs
    let packedFTypes ← inferArgumentTypesN positions.size brecOn
-    let packedFArgs ← positions.mapMwith packFArgs packedFTypes FArgs
+    let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
    let brecOn := mkAppN brecOn packedFArgs
    let some poss := positions.find? (·.contains fnIdx)
      | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← if poss.size = 1 then pure brecOn else
-      mkPProdProjN (poss.getIdx? fnIdx).get! brecOn
+    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
    mkLambdaFVars ys (mkAppN brecOn otherArgs)

 end Lean.Elab.Structural
--- a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
@ -1,126 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joachim Breitner
-/
-prelude
-import Lean.Meta.InferType
-
-/-!
-This module contains the logic that packs the motives and FArgs of multiple functions into one,
-to allow structural mutual recursion where the number of functions is not exactly the same
-as the number of inductive data types in the mutual inductive group.
-
-The private helper functions related to `PProd` here should at some point be moved to their own
-module, so that they can be used elsewhere (e.g. `FunInd`), and possibly unified with the similar
-constructions for well-founded recursion (see `ArgsPacker` module).
-/
-
-namespace Lean.Elab.Structural
-open Meta
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ ∧ True`, return the proof of `Pᵢ` -/
-def mkPProdProjN (i : Nat) (e : Expr) : MetaM Expr := do
-  let mut value := e
-  for _ in [:i] do
-      value ← mkPProdSnd value
-  value ← mkPProdFst value
-  return value
-
-/--
-Combines motives from different functions that recurse on the same parameter type into a single
-function returning a `PProd` type.
-
-For example
-```
-packMotives (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
-```
-will return
-```
-fun (n : Nat) (PProd Nat (Fin n → Fin n))
-```
-
-It is the identity if `motives.size = 1`.
-
-It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no motive is given.
-(this is the reason we need the expected type in the `motiveType` parameter).
-
-/
-def packMotives (motiveType : Expr) (motives : Array Expr) : MetaM Expr := do
-  if motives.size = 1 then
-    return motives[0]!
-  trace[Elab.definition.structural] "packing Motives\nexpected: {motiveType}\nmotives: {motives}"
-  forallTelescope motiveType fun xs sort => do
-    unless sort.isSort do
-      throwError "packMotives: Unexpected motiveType {motiveType}"
-    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
-    -- we pass `C`, a plain FVar, here
-    let motives := motives.map (·.beta xs)
-    let packedMotives ← mkNProd sort.sortLevel! motives
-    mkLambdaFVars xs packedMotives
-
-/--
-Combines the F-args from different functions that recurse on the same parameter type into a single
-function returning a `PProd` value. See `packMotives`
-
-It is the identity if `motives.size = 1`.
-/
-def packFArgs (FArgType : Expr) (FArgs : Array Expr) : MetaM Expr := do
-  if FArgs.size = 1 then
-    return FArgs[0]!
-  forallTelescope FArgType fun xs body => do
-    let lvl ← getLevel body
-    let FArgs := FArgs.map (·.beta xs)
-    let packedFArgs ← mkNProdMk lvl FArgs
-    mkLambdaFVars xs packedFArgs
-
-
-end Lean.Elab.Structural
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@ -665,27 +665,6 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do
  else
    mkAppM ``Iff.of_eq #[h]

-/--
-Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`.
-If `n = 0` returns a proof of `True`.
-If `n = 1` returns the proof of `P₁`.
-/
-def mkAndIntroN : Array Expr → MetaM Expr
-| #[] => return mkConst ``True.intro []
-| #[e] => return e
-| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back
-
-
-/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/
-def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do
-  let mut value := e
-  for _ in [:i] do
-      value := mkProj ``And 1 value
-  if i + 1 < n then
-      value := mkProj ``And 0 value
-  return value
-
-
 builtin_initialize do
  registerTraceClass `Meta.appBuilder
  registerTraceClass `Meta.appBuilder.result (inherited := true)
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@ -6,6 +6,7 @@ Authors: Joachim Breitner

 prelude
 import Lean.Meta.AppBuilder
+import Lean.Meta.PProdN
 import Lean.Meta.ArgsPacker.Basic

 /-!
@ -518,7 +519,7 @@ def curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr := do
  let mut es := #[]
  for i in [:argsPacker.numFuncs] do
    es := es.push (← argsPacker.curryProj e i)
-  mkAndIntroN es
+  PProdN.mk 0 es

 /--
 Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e`
@ -533,7 +534,7 @@ where
  | [], acc => k acc
  | t::ts, acc => do
    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
-    withLocalDecl name .default t fun x => do
+    withLocalDeclD name t fun x => do
      go ts (acc.push x)

 /--
--- a/src/Lean/Meta/Constructions/BRecOn.lean
+++ b/src/Lean/Meta/Constructions/BRecOn.lean
@ -8,67 +8,18 @@ import Lean.Meta.InferType
 import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.CompletionName
+import Lean.Meta.PProdN

 namespace Lean
 open Meta

-section PProd
-
-/--!
-Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
-instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
-elsewhere.
-/
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-end PProd
+/-- Transforms `e : xᵢ → (t₁ ×' t₂)` into `(xᵢ → t₁) ×' (xᵢ → t₂) -/
+private def etaPProd (xs : Array Expr) (e : Expr) : MetaM Expr := do
+  if xs.isEmpty then return e
+  let r := mkAppN e xs
+  let r₁ ← mkLambdaFVars xs (← mkPProdFst r)
+  let r₂ ← mkLambdaFVars xs (← mkPProdSnd r)
+  mkPProdMk r₁ r₂

 /--
 If `minorType` is the type of a minor premies of a recursor, such as
@ -91,7 +42,7 @@ private def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorT
 where
  ibelow := rlvl matches .zero
  go (prods : Array Expr) : List Expr → MetaM Expr
-  | [] => mkNProd rlvl prods
+  | [] => PProdN.pack rlvl prods
  | arg::args => do
    let argType ← inferType arg
    forallTelescope argType fun arg_args arg_type => do
@ -243,7 +194,7 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
  forallTelescope minorType fun minor_args minor_type => do
    let rec go (prods : Array Expr) : List Expr → MetaM Expr
      | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
-          let b ← mkNProdMk rlvl prods
+          let b ← PProdN.mk rlvl prods
          let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn
            | throwError m!"Did not find {minor_type} in {motives}"
          mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
@ -256,14 +207,8 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
              let type' ← mkForallFVars arg_args
                (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
              withLocalDeclD name type' fun arg' => do
-                if arg_args.isEmpty then
-                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
-                else
-                  let r := mkAppN arg' arg_args
-                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
-                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
-                  let r ← mkPProdMk r₁ r₂
-                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
+                let r ← etaPProd arg_args arg'
+                mkLambdaFVars #[arg'] (← go (prods.push r) args)
            else
              mkLambdaFVars #[arg] (← go prods args)
    go #[] minor_args.toList
--- a/src/Lean/Meta/PProdN.lean
+++ b/src/Lean/Meta/PProdN.lean
@ -0,0 +1,145 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Meta.InferType
+
+/-!
+This module provides functios to pack and unpack values using nested `PProd` or `And`,
+as used in the `.below` construction, in the `.brecOn` construction for mutual recursion and
+and the `mutual_induct` construction.
+
+It uses `And` (equivalent to `PProd.{0}` when possible).
+
+The nesting is `t₁ ×' (t₂ ×' t₃)`, not `t₁ ×' (t₂ ×' (t₃ ×' PUnit))`. This is more readable,
+slightly shorter, and means that the packing is the identity if `n=1`, which we rely on in some
+places. It comes at the expense that hat projection needs to know `n`.
+
+Packing an empty list uses `True` or `PUnit` depending on the given `lvl`.
+
+Also see `Lean.Meta.ArgsPacker` for a similar module for `PSigma` and `PSum`, used by well-founded recursion.
+-/
+
+
+namespace Lean.Meta
+
+/-- Given types `t₁` and `t₂`, produces `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/
+def mkPProd (e1 e2 : Expr) : MetaM Expr := do
+  let lvl1 ← getLevel e1
+  let lvl2 ← getLevel e2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp2 (.const `And []) e1 e2
+  else
+    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
+
+/-- Given values of typs `t₁` and `t₂`, produces value of type `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/
+def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
+  let t1 ← inferType e1
+  let t2 ← inferType e2
+  let lvl1 ← getLevel t1
+  let lvl2 ← getLevel t2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
+  else
+    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
+
+/-- `PProd.fst` or `And.left` (using `.proj`) -/
+def mkPProdFst (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 0 e
+  | And _ _ => return .proj ``And 0 e
+  | _ => panic! "mkPProdFst: cannot handle{indentExpr e}\nof type{indentExpr t}"
+
+/-- `PProd.snd` or `And.right` (using `.proj`) -/
+def mkPProdSnd (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 1 e
+  | And _ _ => return .proj ``And 1 e
+  | _ => panic! "mkPProdSnd: cannot handle{indentExpr e}\nof type{indentExpr t}"
+
+
+
+namespace PProdN
+
+/-- Given types `tᵢ`, produces `t₁ ×' t₂ ×' t₃` -/
+def pack (lvl : Level) (xs : Array Expr) : MetaM Expr := do
+  if xs.size = 0 then
+    if lvl matches .zero then return .const ``True []
+                         else return .const ``PUnit [lvl]
+  let xBack := xs.back
+  xs.pop.foldrM mkPProd xBack
+
+/-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃` -/
+def mk (lvl : Level) (xs : Array Expr) : MetaM Expr := do
+  if xs.size = 0 then
+    if lvl matches .zero then return .const ``True.intro []
+                         else return .const ``PUnit.unit [lvl]
+  let xBack := xs.back
+  xs.pop.foldrM mkPProdMk xBack
+
+/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/
+def proj (n i : Nat) (e : Expr) : MetaM Expr := do
+  let mut value := e
+  for _ in [:i] do
+      value ← mkPProdSnd value
+  if i+1 < n then
+    mkPProdFst value
+  else
+    pure value
+
+
+
+/--
+Packs multiple type-forming lambda expressions taking the same parameters using `PProd`.
+
+The parameter `type` is the common type of the these expressions
+
+For example
+```
+packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
+```
+will return
+```
+fun (n : Nat) => (Nat ×' (Fin n → Fin n))
+```
+
+It is the identity if `es.size = 1`.
+
+It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no expressions are given.
+(this is the reason we need the expected type in the `type` parameter).
+
+-/
+def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
+  if es.size = 1 then
+    return es[0]!
+  forallTelescope type fun xs sort => do
+    assert! sort.isSort
+    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
+    -- we pass `C`, a plain FVar, here
+    let es' := es.map (·.beta xs)
+    let packed ← PProdN.pack sort.sortLevel! es'
+    mkLambdaFVars xs packed
+
+/--
+The value analogue to `PProdN.packLambdas`.
+
+It is the identity if `es.size = 1`.
+-/
+def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
+  if es.size = 1 then
+    return es[0]!
+  forallTelescope type fun xs body => do
+    let lvl ← getLevel body
+    let es' := es.map (·.beta xs)
+    let packed ← PProdN.mk lvl es'
+    mkLambdaFVars xs packed
+
+
+end PProdN
+
+end Lean.Meta
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
+import Lean.Meta.PProdN
 import Lean.Elab.PreDefinition.WF.Eqns
 import Lean.Elab.PreDefinition.Structural.Eqns
 import Lean.Elab.Command
@ -188,21 +189,6 @@ def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [
  let b := b.instantiate1 (.fvar x)
  k x b

-/-- `PProd.fst` or `And.left` -/
-def mkFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd t₁ t₂ => return mkApp3 (.const ``PProd.fst t.getAppFn.constLevels!) t₁ t₂ e
-  | And t₁ t₂ => return mkApp3 (.const ``And.left []) t₁ t₂ e
-  | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` -/
-def mkSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd t₁ t₂ => return mkApp3 (.const ``PProd.snd t.getAppFn.constLevels!) t₁ t₂ e
-  | And t₁ t₂ => return mkApp3 (.const ``And.right []) t₁ t₂ e
-  | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}"

 /--
 A monad to help collecting inductive hypothesis.
@ -310,7 +296,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
              forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
                let #[newIH'] := newIH' | unreachable!
                let altIHs ← M.exec <| foldAndCollect oldIH' newIH'.fvarId! isRecCall alt
-                let altIH ← mkAndIntroN altIHs
+                let altIH ← PProdN.mk 0 altIHs
                mkLambdaFVars #[newIH'] altIH)
          (onRemaining := fun _ => pure #[mkFVar newIH])
        let ihMatcherApp'' ← ihMatcherApp'.inferMatchType
@ -328,11 +314,6 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
          (onRemaining := fun _ => pure #[])
        return matcherApp'.toExpr

-    -- These projections can be type changing, so re-infer their type arguments
-    match_expr e with
-    | PProd.fst _ _ e => mkFst (← foldAndCollect oldIH newIH isRecCall e)
-    | PProd.snd _ _ e => mkSnd (← foldAndCollect oldIH newIH isRecCall e)
-    | _ =>

    if e.getAppArgs.any (·.isFVarOf oldIH) then
      -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
@ -371,6 +352,10 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
    | .mdata m b =>
      pure <| .mdata m (← foldAndCollect oldIH newIH isRecCall b)

+    -- These projections can be type changing (to And), so re-infer their type arguments
+    | .proj ``PProd 0 e => mkPProdFst (← foldAndCollect oldIH newIH isRecCall e)
+    | .proj ``PProd 1 e => mkPProdSnd (← foldAndCollect oldIH newIH isRecCall e)
+
    | .proj t i e =>
      pure <| .proj t i (← foldAndCollect oldIH newIH isRecCall e)

@ -690,7 +675,6 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
    { name := inductName, levelParams := us, type := eTyp, value := e' }
  return inductName

-
 /--
 In the type of `value`, reduces
 * Beta-redexes
@ -806,7 +790,7 @@ def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): Met
      let value ← forallTelescope ci.type fun xs _body => do
        let value := .const ci.name (levelParams.map mkLevelParam)
        let value := mkAppN value xs
-        let value := mkProjAndN eqnInfo.declNames.size idx value
+        let value ← PProdN.proj eqnInfo.declNames.size idx value
        mkLambdaFVars xs value
      let type ← inferType value
      addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value }
--- a/tests/lean/run/letrecInProofs.lean
+++ b/tests/lean/run/letrecInProofs.lean
@ -19,7 +19,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
      have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l := right x s l
      have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r := right x s r
      have hl : x ≠ l ∧ x ≮ l := h.1
-      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have hr : x ≠ r ∧ x ≮ r := h.2
      have ihl : node s x ≠ l ∧ node s x ≮ l := ihl hl.2
      have ihr : node s x ≠ r ∧ node s x ≮ r := ihr hr.2
      apply And.intro
@ -31,7 +31,6 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
      focus
        apply And.intro
        apply ihl
-        apply And.intro _ trivial
        apply ihr
  let rec left (x t : Tree) (b : Tree) (h : x ≮ b) : node x t ≠ b ∧ node x t ≮ b := by
    match b, h with
@ -42,7 +41,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
      have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l := left x t l
      have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r := left x t r
      have hl : x ≠ l ∧ x ≮ l := h.1
-      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have hr : x ≠ r ∧ x ≮ r := h.2
      have ihl : node x t ≠ l ∧ node x t ≮ l := ihl hl.2
      have ihr : node x t ≠ r ∧ node x t ≮ r := ihr hr.2
      apply And.intro
@ -54,19 +53,17 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
      focus
        apply And.intro
        apply ihl
-        apply And.intro _ trivial
        apply ihr
  let rec aux : (x : Tree) → x ≮ x
    | leaf     => trivial
    | node l r => by
        have ih₁ : l ≮ l := aux l
        have ih₂ : r ≮ r := aux r
-        show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) ∧ True
+        show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r)
        apply And.intro
        focus
          apply left
          assumption
-        apply And.intro _ trivial
        focus
          apply right
          assumption
@ -78,7 +75,7 @@ open Tree

 theorem ex1 (x : Tree) : x ≠ node leaf (node x leaf) := by
  intro h
-  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.2.1.1

 theorem ex2 (x : Tree) : x ≠ node x leaf := by
  intro h
@ -86,4 +83,4 @@ theorem ex2 (x : Tree) : x ≠ node x leaf := by

 theorem ex3 (x y : Tree) : x ≠ node y x := by
  intro h
-  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1
--- a/tests/lean/run/nestedInductiveConstructions.lean
+++ b/tests/lean/run/nestedInductiveConstructions.lean
@ -12,11 +12,10 @@ inductive Tree where | node  : List Tree → Tree
 info: @[reducible] protected def Ex1.Tree.below.{u} : {motive_1 : Tree → Sort u} →
  {motive_2 : List.{0} Tree → Sort u} → Tree → Sort (max 1 u) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u) + 1}
-    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+  Tree.rec.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
    t
 -/
 #guard_msgs in
@ -26,11 +25,10 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex1.Tree.below_1.{u} : {motive_1 : Tree → Sort u} →
  {motive_2 : List.{0} Tree → Sort u} → List.{0} Tree → Sort (max 1 u) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u) + 1}
-    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+  Tree.rec_1.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
    t
 -/
 #guard_msgs in
@ -40,8 +38,8 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex1.Tree.ibelow_1 : {motive_1 : Tree → Prop} →
  {motive_2 : List.{0} Tree → Prop} → List.{0} Tree → Prop :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{1} (fun a a_ih => And (And (motive_2 a) a_ih) True) True
-    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (And (motive_2 tail) tail_ih) True)) t
+  Tree.rec_1.{1} (fun a a_ih => And (motive_2 a) a_ih) True
+    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (motive_2 tail) tail_ih)) t
 -/
 #guard_msgs in
 #print Tree.ibelow_1
@ -82,16 +80,15 @@ info: @[reducible] protected def Ex2.Tree.below.{u} : {motive_1 : Tree → Sort
 fun {motive_1} {motive_2} {motive_3} t =>
  Tree.rec.{(max 1 u) + 1}
    (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
    PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
    PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
    t
 -/
 #guard_msgs in
@ -104,16 +101,15 @@ info: @[reducible] protected def Ex2.Tree.below_1.{u} : {motive_1 : Tree → Sor
 fun {motive_1} {motive_2} {motive_3} t =>
  Tree.rec_1.{(max 1 u) + 1}
    (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
    PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
    PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
    t
 -/
 #guard_msgs in
@ -126,16 +122,15 @@ info: @[reducible] protected def Ex2.Tree.below_2.{u} : {motive_1 : Tree → Sor
 fun {motive_1} {motive_2} {motive_3} t =>
  Tree.rec_2.{(max 1 u) + 1}
    (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
    PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
    PUnit.{max 1 u}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
    t
 -/
 #guard_msgs in
@ -169,12 +164,10 @@ inductive Tree : Type u where | node : List Tree → Tree
 info: @[reducible] protected def Ex3.Tree.below.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
  {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max 1 u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u_1) + 1, u}
-    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
-    PUnit.{max 1 u_1}
+  Tree.rec.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
    t
 -/
 #guard_msgs in
@ -184,12 +177,10 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex3.Tree.below_1.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
  {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max 1 u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u_1) + 1, u}
-    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
-    PUnit.{max 1 u_1}
+  Tree.rec_1.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
    (fun head tail head_ih tail_ih =>
      PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
    t
 -/
 #guard_msgs in
--- a/tests/lean/unusedLet.lean.expected.out
+++ b/tests/lean/unusedLet.lean.expected.out
@ -8,5 +8,5 @@ fun x =>
      | 0 => fun x => 1
      | n.succ => fun x =>
        let y := 42;
-        2 * x.fst.fst)
+        2 * x.1.1)
      f