Allowed Prop projections in kernel vs check

Stream: metaprogramming / tactics

[Eric Paul]

I was curious why the kernel and check disagree on whether the following projection is allowed. I guess this is really two questions:
Why disallow this in the kernel, and given that the kernel doesn't allow it, why let check allow it?

import Lean
import Qq
open Qq

inductive Test : Prop where
| mk (n : Nat) (_ : n = n) (p : True)

run_meta
  Lean.Meta.check q((⟨1, rfl, True.intro⟩ : Test).3)

def test : True := (⟨1, rfl, True.intro⟩ : Test).3

[Jovan Gerbscheid]

Lean.Meta.check isn't meant to check everything that the kernel checks. Note also that check works even when there are metavariables, which the kernel cannot work with.

More generally, ideally all invalid terms are caught before sending them to the kernel, but there are some checks (such as Prop projections) that only the kernel does, so that's when we get kernel errors.

In you example though, I think that that particular projection should actually be valid, but it is enough of an edge case where I understand that this wasn't added to the kernel, since you can define this projection yourself using the recursor.

[Eric Paul]

That makes sense, thanks. It does appear that check is looking at Prop projections, it just chooses to check them differently:

if (← isProp structType) && !(← isProp projType) then

Would a PR making the way check works here align with the kernel be appreciated or would that be considered a waste of time as check and the kernel line up well enough? Just trying to get a better feel for the goals in the relationship between check and the kernel.

[Aaron Liu]

What about making the kernel do what check does here? This is sound, right?

[Jovan Gerbscheid]

Interesting, it is curious then that the kernel and check have different behaviour here. It might be the most reasonable thing to fix the kernel to accept this. But people are generally extremely cautious about changes to the kernel, so I don't think this will actually happen.

It seems that this is the relevant kernel code, in C++

expr type_checker::infer_proj(expr const & e, bool infer_only) {
    expr type = whnf(infer_type_core(proj_expr(e), infer_only));
    if (!proj_idx(e).is_small())
        throw invalid_proj_exception(env(), m_lctx, e);
    unsigned idx = proj_idx(e).get_small_value();
    buffer<expr> args;
    expr const & I = get_app_args(type, args);
    if (!is_constant(I))
        throw invalid_proj_exception(env(), m_lctx, e);
    name const & I_name  = const_name(I);
    if (I_name != proj_sname(e))
        throw invalid_proj_exception(env(), m_lctx, e);
    constant_info I_info = env().get(I_name);
    if (!I_info.is_inductive())
        throw invalid_proj_exception(env(), m_lctx, e);
    inductive_val I_val = I_info.to_inductive_val();
    if (length(I_val.get_cnstrs()) != 1 || args.size() != I_val.get_nparams() + I_val.get_nindices())
        throw invalid_proj_exception(env(), m_lctx, e);

    constant_info c_info = env().get(head(I_val.get_cnstrs()));
    expr r = instantiate_type_lparams(c_info, const_levels(I));
    for (unsigned i = 0; i < I_val.get_nparams(); i++) {
        lean_assert(i < args.size());
        r = whnf(r);
        if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
        r = instantiate(binding_body(r), args[i]);
    }
    bool is_prop_type = is_prop(type);
    for (unsigned i = 0; i < idx; i++) {
        r = whnf(r);
        if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
        if (has_loose_bvars(binding_body(r))) {
            if (is_prop_type && !is_prop(binding_domain(r)))
                throw invalid_proj_exception(env(), m_lctx, e);
            r = instantiate(binding_body(r), mk_proj(I_name, i, proj_expr(e)));
        } else {
            r = binding_body(r);
        }
    }
    r = whnf(r);
    if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
    r = binding_domain(r);
    if (is_prop_type && !is_prop(r))
        throw invalid_proj_exception(env(), m_lctx, e);
    return r;
}

[Eric Paul]

Yes, that would make sense. My understanding is that it would change to the following:

expr type_checker::infer_proj(expr const & e, bool infer_only) {
   ...
    bool is_prop_type = is_prop(type);
    for (unsigned i = 0; i < idx; i++) {
        r = whnf(r);
        if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
        if (has_loose_bvars(binding_body(r))) {
            //if (is_prop_type && !is_prop(binding_domain(r)))
               // throw invalid_proj_exception(env(), m_lctx, e);
            r = instantiate(binding_body(r), mk_proj(I_name, i, proj_expr(e)));
        } else {
            r = binding_body(r);
        }
    }
    r = whnf(r);
    if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
    r = binding_domain(r);
    if (is_prop_type && !is_prop(r))
        throw invalid_proj_exception(env(), m_lctx, e);
    return r;
}

We get rid of the check inside of the for loop that throws if one of the arguments before the idx is not a Prop and then the line if (is_prop_type && !is_prop(r)) at the end does the sufficient check.

[Jovan Gerbscheid]

The following commit has introduced this extra check in the kernel: https://github.com/leanprover/lean4/commit/3746005f5fc35d030d26ced2f7bcaabc295224c2

It seems that specifically the following example is why this extra check was introduced:

theorem witness_eq (h : ∃ x : Nat, True) : h.2 = h.2 := rfl -- kernel error

[Aaron Liu]

But that one is sound too

[Jovan Gerbscheid]

I don't know exactly

[Eric Paul]

Nice find with that commit.
This is my understanding:

theorem witness_eq (h : ∃ x : Nat, x = x) : h.2 = h.2 := rfl

Here the type of h.2 is (h.1 = h.1) and we're not allowed to have h.1 appear anywhere in the type?

This corresponds to the code

            if (is_prop_type && !is_prop(binding_domain(r)))
                throw invalid_proj_exception(env(), m_lctx, e);
            r = instantiate(binding_body(r), mk_proj(I_name, i, proj_expr(e)));

Which is creating a projection mk_proj(I_name, i, proj_expr(e)) at an index i < idx which we're often not allowed to do and that's why the check is there above it.

[Aaron Liu]

oh I thought #check wouldn't accept this

[Eric Paul]

Indeed, this now just appears to be an issue where check allows terms with invalid types.

import Lean
import Qq
open Lean Meta Qq

run_meta
  let projectedTerm := q((⟨3, rfl⟩ : ∃x, x = x).2)
  check projectedTerm -- succeeds
  check (← inferType projectedTerm) -- fails

The fix would be just adding that same if statement in this loop that was added to the kernel

      for i in *...idx do
        ctorType ← whnf ctorType
        match ctorType with
        | .forallE _ _ body _ =>
          if body.hasLooseBVars then
            -- ADD: Ensure that `mkProj structName i e` is valid here
            ctorType := body.instantiate1 <| mkProj structName i e
          else
            ctorType := body
        | _ => failed ()

Thanks for all the help, this makes a lot more sense now!

[Aaron Liu]

Can't we just look at the type of the projection?

[Aaron Liu]

Why do we need to looks at the constructor?

[Eric Paul]

I'm not exactly sure what you mean, this code is from inferProjType

[Jovan Gerbscheid]

I think the code was written in this ungeneral way for efficiency. It is easy to work around it by reordering your arguments:

import Lean
import Qq
open Qq

inductive Test : Prop where
| mk (p : True) (n : Nat) (_ : n = n)

run_meta
  Lean.Meta.check q((⟨True.intro, 1, rfl⟩ : Test).3)

def test : True := (⟨True.intro, 1, rfl⟩ : Test).3

[Kyle Miller]

In a previous discussion, there was a suggestion to make the kernel more restrictive with its primitive projections and only allow those that can actually be implemented with a recursor. Related issue: lean4#7637

It seems reasonable to me that the check for primitive projections could be simplified to whether the type supports large elimination. Proofs are usually not reduced, so I'm not sure that primitive projections are necessary in the Prop-elimination case. Plus, definitional proof irrelevance means structure eta doesn't need primitive projections

(Side note: A sufficiently smart elaborator could 'allow' primitive projections on Exists in Prop contexts, constructively. The idea would be if v.1 or v.2 appears, you find all occurrences, abstract them out, and insert an Exists.recOn. Easier though would be to be able to register that v.1 is v.choose and v.2 is v.choose_spec.)