feat: use kernel projections in constructions

Motivation: auxiliary recursors such as `brecOn` do not depend on
user-facing projection definitions anymore.
Thus, we can simplify `whnfCore` at `TypeUtil`.

library/Init/Lean/TypeUtil.lean

@@ -159,46 +159,6 @@ else
   let val := val.betaRev revArgs;
   successK (extractIdRhs val)
 
-private def reduceAuxRec
-    (whnf : Expr → TypeUtilM σ ϕ Expr)
-    (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr)
-    (failK : Unit → TypeUtilM σ ϕ Expr) (successK : Expr → TypeUtilM σ ϕ Expr) : TypeUtilM σ ϕ Expr :=
-deltaBetaDefinition c lvls revArgs failK $ fun e =>
-  /- Remark:
-
-     `brecOn ...` unfolds to a term of the form (PProd.fst (rec ...))
-     `whnfCore` does not unfold projection functions because of lazy delta reduction at `isDefEq`.
-     For example, when solving constraints such as `(PProd.fst ?m) =?= (PProd.fst (1, 2))`
-
-     That being said, we observed a negative performance impact on
-     constraints containing `brecOn` that come from the equation compiler.
-     For example, consider the following definition
-
-     ```
-     def nastySize : List Nat → Nat
-     | []      := 1000000
-     | (a::as) := nastySize as + 1000000
-     ```
-
-     We will get a constraint of the form
-     ```
-     (List.brecOn [] ...) =?= bit0 ...
-     ```
-     The isDefEq method reduces this constraint using whnfCore. So, we obtain
-     ```
-     PProd.fst ... =?= bit0 ...
-     ```
-     This constraint is then handled by isDefEqDelta, which decides to unfold `bit0` which is a poor decision.
-     The key problem here is that we morally did not reduce `brecOn`.
-     Thus, we fix the issue by reducing the projection function if the auxiliary recursor is a brecOn.
-     This fix is a little non modular because `brecOn` auxiliary recursors are defined in
-     a completely different module, and `TypeUtil` should not be aware of them. -/
-  match c.name with
-  | Name.mkString _ "brecOn" => do
-    env ← getEnv;
-    reduceProjectionFn whnf env e (fun _ => successK e) successK
-  | _ => successK e
-
 /--
   Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
   expand let-expressions, expand assigned meta-variables.
@@ -234,7 +194,7 @@ deltaBetaDefinition c lvls revArgs failK $ fun e =>
         | ConstantInfo.quotInfo rec   => reduceQuotRecAux whnf env rec lvls e.getAppArgs done whnfCore
         | c@(ConstantInfo.defnInfo _) =>
           if reduceAuxRec? && isAuxRecursor env c.name then
-            reduceAuxRec whnf c lvls e.getAppRevArgs done whnfCore
+            deltaBetaDefinition c lvls e.getAppArgs done whnfCore
           else
             done()
         | _ => done ()

src/library/constructions/util.cpp

@@ -23,14 +23,12 @@ expr mk_and_intro(type_checker & ctx, expr const & Ha, expr const & Hb) {
     return mk_app(mk_constant(get_and_intro_name()), ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
 }
 
-expr mk_and_left(type_checker & ctx, expr const & H) {
-    expr a_and_b = ctx.whnf(ctx.infer(H));
-    return mk_app(mk_constant(get_and_left_name()), app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
+expr mk_and_left(type_checker &, expr const & H) {
+    return mk_proj(get_and_name(), nat(0), H);
 }
 
-expr mk_and_right(type_checker & ctx, expr const & H) {
-    expr a_and_b = ctx.whnf(ctx.infer(H));
-    return mk_app(mk_constant(get_and_right_name()), app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
+expr mk_and_right(type_checker &, expr const & H) {
+    return mk_proj(get_and_name(), nat(1), H);
 }
 
 expr mk_pprod(type_checker & ctx, expr const & A, expr const & B) {
@@ -47,18 +45,12 @@ expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b) {
     return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
 }
 
-expr mk_pprod_fst(type_checker & ctx, expr const & p) {
-    expr AxB = ctx.whnf(ctx.infer(p));
-    expr const & A = app_arg(app_fn(AxB));
-    expr const & B = app_arg(AxB);
-    return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p);
+expr mk_pprod_fst(type_checker &, expr const & p) {
+    return mk_proj(get_pprod_name(), nat(0), p);
 }
 
-expr mk_pprod_snd(type_checker & ctx, expr const & p) {
-    expr AxB = ctx.whnf(ctx.infer(p));
-    expr const & A = app_arg(app_fn(AxB));
-    expr const & B = app_arg(AxB);
-    return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
+expr mk_pprod_snd(type_checker &, expr const & p) {
+    return mk_proj(get_pprod_name(), nat(1), p);
 }
 
 expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop) {

src/library/type_context.cpp

@@ -635,9 +635,23 @@ optional<expr> type_context_old::reduce_projection(expr const & e) {
     return reduce_projection_core(info, e);
 }
 
-optional<expr> type_context_old::reduce_proj(expr const & /* e */) {
-    // TODO(Leo)
-    throw exception("projection reduction is only implemented in the kernel.");
+optional<expr> type_context_old::reduce_proj(expr const & e) {
+    if (!proj_idx(e).is_small())
+        return none_expr();
+    unsigned idx = proj_idx(e).get_small_value();
+    expr c = whnf(proj_expr(e));
+    buffer<expr> args;
+    expr const & mk = get_app_args(c, args);
+    if (!is_constant(mk))
+        return none_expr();
+    constant_info mk_info = env().get(const_name(mk));
+    if (!mk_info.is_constructor())
+        return none_expr();
+    unsigned nparams = mk_info.to_constructor_val().get_nparams();
+    if (nparams + idx < args.size())
+        return some_expr(args[nparams + idx]);
+    else
+        return none_expr();
 }
 
 optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {