Function good_n_rec_reduction

crates/kernel/src/tutorial/reduction.rs:613–668

()

    // N.add : N → N → N :=
    //   N.rec.{1} (motive := fun _ => N → N)
    //     (fun m => m)                          -- zero case
    //     (fun n ih m => N.succ (ih m))         -- succ case
    let motive = nlam("_", nat(), pi(nat(), nat())); // fun _ => N → N

    // zero case: fun m => m
    let zero_case = nlam("m", nat(), var(0));

    // succ case: fun n ih m => N.succ (ih m)
    // depth 3: m=var(0), ih=var(1) : N → N, n=var(2) : N
    let succ_case = nlam(
      "n",
      nat(),
      nlam(
        "ih",
        pi(nat(), nat()),
        nlam("m", nat(), app(cnst("N.succ", &[]), app(var(1), var(0)))),
      ),
    );

    let add_val =
      apps(cnst("N.rec", &[usucc(uzero())]), &[motive, zero_case, succ_case]);
    let (add_id, add_c) = mk_defn(
      "N.add",
      0,
      vec![],
      pi(nat(), pi(nat(), nat())),
      add_val,
      ReducibilityHints::Abbrev,
    );
    env.insert(add_id, add_c);

    // Test 1: ∀ m, N.add N.zero m = m
    // N.add N.zero = (N.rec ...) N.zero → reduces zero case → fun m => m
    // So N.add N.zero m = m
    let ty1 = npi(
      "m",
      nat(),
      eq_expr(
        usucc(uzero()),
        nat(),
        app(app(cnst("N.add", &[]), cnst("N.zero", &[])), var(0)),
        var(0),
      ),
    );
    let val1 = nlam("m", nat(), eq_refl_expr(usucc(uzero()), nat(), var(0)));
    let (id1, c1) = mk_thm("nAddZero", 0, vec![], ty1, val1);
    env.insert(id1.clone(), c1);
    check_accepts(&mut env, &id1);
  }

  /// N.add N.succ reduction: N.add (N.succ n) m = N.succ (N.add n m)
  #[test]
  fn good_n_rec_reduction_succ() {
    let mut env = nat_env();
    let nat = || cnst("N", &[]);

    let motive = nlam("_", nat(), pi(nat(), nat()));