Function good_fun_eta

crates/kernel/src/tutorial/defeq.rs:61–102

()

  /// funEta : ∀ (α β : Type) (f : α → β), (fun x => f x) = f := fun _ _ f => rfl
  #[test]
  fn good_fun_eta() {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    // ∀ (α : Type) (β : Type) (f : α → β), (fun x => f x) = f
    // At f_ty position (depth 2): α=var(1), β=var(0)
    // α → β at depth 2: pi(var(1), var(1)) — inside pi body β shifts from 0→1
    let f_ty = pi(var(1), var(1));
    // Inside body (depth 3): f=var(0), β=var(1), α=var(2)
    // eta_lhs = fun (x : α) => f x. α at depth 3 = var(2).
    // Inside lambda (depth 4): x=var(0), f=var(1), β=var(2), α=var(3)
    let eta_lhs = nlam("x", var(2), app(var(1), var(0)));
    // α → β at depth 3: pi(var(2), var(2)) — inside pi body β shifts from 1→2
    let eq_app = apps(
      cnst("Eq", &[usucc(uzero())]),
      &[pi(var(2), var(2)), eta_lhs, var(0)],
    );
    let ty = npi("α", sort1(), npi("β", sort1(), npi("f", f_ty, eq_app)));

    // fun α β f => Eq.refl.{1} (α → β) f
    // At depth 3 inside val: f=var(0), β=var(1), α=var(2)
    let val = nlam(
      "α",
      sort1(),
      nlam(
        "β",
        sort1(),
        nlam(
          "f",
          pi(var(1), var(1)),
          apps(
            cnst("Eq.refl", &[usucc(uzero())]),
            &[pi(var(2), var(2)), var(0)],
          ),
        ),
      ),
    );

    let (id, c) = mk_thm("funEta", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// funEtaBad : ∀ (α β : Type) (g : α → α) (f : α → β), (fun x => f (g x)) = f
  /// BAD: eta should NOT identify functions with different bodies.