Function bad_fun_eta

crates/kernel/src/tutorial/defeq.rs:107–167

()

  /// BAD: eta should NOT identify functions with different bodies.
  #[test]
  fn bad_fun_eta() {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

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

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

    let (id, c) = mk_thm("funEtaBad", 0, vec![], ty, val);