Expr.isArrow / arrow? too picky?

Stream: lean4

[Joachim Breitner]

I’d like to double-check my understanding of the lean type system here.

Consider this code

import Lean

structure Test where
  ty : Type
  val : ty

#check fun n => (Test.mk Nat n).val
#check congrArg (fun n => (Test.mk Nat n).val)

open Lean Elab Command Meta

elab "#test" : command => runTermElabM fun _ => do
    let s  ← `(fun n => (Test.mk Nat n).val)
    let e ← (Lean.Elab.Term.elabTerm s none).run' {}
    Lean.Meta.check e
    Lean.logInfo m!"Expression: {Lean.indentExpr e}"
    Lean.logInfo m!"Type: {Lean.indentExpr (←inferType e)}"
    Lean.logInfo m!"arrow?: {(←inferType e).arrow?}"

#test

The expression

fun n => (Test.mk Nat n).val

has type

 (n : Nat) → { ty := Nat, val := n }.ty

so it is not obviously non-dependent. But according to the next check, I can use it with congrArg, which requires a non-dependent function:

congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

I conclude that the type checker will reduce that expression enough to infer β as Nat here. And that passing such a function to congrArg is type-correct.

Furthermore, Lean’s function docs#Expr.isArrow and docs#Expr.arrow?, which will not accept that type, are simply too conservative, and thus the helper function mkCongrArg’s checks are actually too strict, and just because that function complains does not mean I am building something invalid here.

So far so correct? (Context is https://github.com/leanprover/lean4/pull/3121 where I’d be building such terms and I wonder if that is kosher.)

[Mario Carneiro]

It's not the typechecker's responsibility to prove that this arrow is nondependent, it's the elaborator's

[Mario Carneiro]

because you have to pass α and β to the function

[Mario Carneiro]

the typechecker just ensures that the type of f is α → β, so the elaborator will work out that α and β are Nat and pass that, and then the typechecker verifies that (n : Nat) → { ty := Nat, val := n }.ty is defeq to Nat -> Nat, which means that in context n : Nat, { ty := Nat, val := n }.ty == Nat, which checks out

[Joachim Breitner]

Ah, yes, that makes sense. And when I am the one constructing Exprs, it's my responsibility to figure out β.

In the context of my PR I am using the type of e before abstraction, so _if_ the function is actually non-dependent, this should check out. If it is properly dependent, then this will not type-check. Probably I should move the unless (← isTypeCorrect motive) do check further down, and run it on the full eqPrf.

I wonder if I can construct a test case where this matters.

Anyways, thanks for the clarification!

[Joachim Breitner]

Here is a little puzzle for adversiarly minded minds who want to help me find good test cases:

Can you pass an equality heq and some term e to this tactic so that isTypeCorrect motive but not isTypeCorrect eqPrf, likely by passing something that’s causing the motive to be dependently typed?

import Lean

open Lean Elab Command Meta

elab "test" hs:term " and " es:term : tactic =>do
    let heq ← Lean.Elab.Term.elabTerm hs none
    let e ← Lean.Elab.Term.elabTerm es none
    Lean.Meta.check e
    Lean.Meta.check heq
    let heqType ← instantiateMVars (← inferType heq)
    let some (α, lhs, rhs) ← matchEq? heqType | unreachable!
    let eAbst ← kabstract e lhs
    -- construct rewrite proof
    let eNew := eAbst.instantiate1 rhs
    let eNew ← instantiateMVars eNew
    let eType ← inferType e
    let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
    unless (← isTypeCorrect motive) do
      throwError "motive is not type correct"
    let u1 ← getLevel α
    let u2 ← getLevel eType
    let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
    unless (← isTypeCorrect eqPrf) do
      throwError "eqPrf is not type correct"
    Lean.logInfo m!"eqPrf: {Lean.indentExpr eqPrf}"
    Lean.logInfo m!"eqPrf type: {Lean.indentExpr (←inferType eqPrf)}"
    Lean.logInfo m!"eNew: {Lean.indentExpr eNew}"
    Lean.logInfo m!"eNew type: {Lean.indentExpr (←inferType eNew)}"

def D2 : (b : Bool) → Bool.rec Unit Nat b
  | false => ()
  | true => 0

def D3 : (b : Bool) → Type
  | false => Unit
  | true => Nat

def mwe2 (h : true = false)
  -- (P : (t : Nat) -> D t)
  (i : D3 false)
  : D3 true
  := by
    test h and i
    sorry

[Mario Carneiro]

def mwe2 (h : true = false) (D : Bool → Type) (f : ∀ b, D b) : True := by
  test h and f true

[Joachim Breitner]

Thanks! Almost what I need, let me make it a bit harder: The term e has to be a type, such as the current goal.

Here is a variant of the puzzle using getMainGoal:

import Lean

open Lean Elab Command Meta Tactic

elab "test" hs:term : tactic =>do
    let heq ← Lean.Elab.Term.elabTerm hs none
    let e ← (← getMainGoal).getType
    Lean.Meta.check e
    Lean.Meta.check heq
    let heqType ← instantiateMVars (← inferType heq)
    let some (α, lhs, rhs) ← matchEq? heqType | unreachable!
    let eAbst ← kabstract e lhs
    -- construct rewrite proof
    let eNew := eAbst.instantiate1 rhs
    let eNew ← instantiateMVars eNew
    let eType ← inferType e
    let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
    unless (← isTypeCorrect motive) do
      throwError "motive is not type correct"
    let u1 ← getLevel α
    let u2 ← getLevel eType
    let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
    unless (← isTypeCorrect eqPrf) do
      throwError "eqPrf is not type correct"
    Lean.logInfo m!"eqPrf: {Lean.indentExpr eqPrf}"
    Lean.logInfo m!"eqPrf type: {Lean.indentExpr (←inferType eqPrf)}"
    Lean.logInfo m!"eNew: {Lean.indentExpr eNew}"
    Lean.logInfo m!"eNew type: {Lean.indentExpr (←inferType eNew)}"

[Mario Carneiro]

def mwe2 (h : true = false) (D : Bool → Type) (f : ∀ b, D b) (P : D true → Prop) : P (f true) := by
  test h

[Joachim Breitner]

Ah, but this gives “motive is not type correct”, not “eqPrf is not type correct”.

Basically I am trying to figure out if the check

unless (← isTypeCorrect eqPrf)

is redundant or not (edited).

[Mario Carneiro]

well it's clearly not here, since that's the error that triggers in this case

[Joachim Breitner]

Sorry,. I meant the other one :-)

[Mario Carneiro]

I think it's not likely to be possible in this case, because the type of a type is a universe, and universes can't have essential dependencies on local variables

[Joachim Breitner]

It seems for that I need to construct a goal whose sort(?) is dependent on e.

[Joachim Breitner]

Great, that’s the kind of argument was looking for. Thanks!

[Mario Carneiro]

note that the word "essential" there is important, it is possible for the type of a type to have inessential dependencies

[Mario Carneiro]

example:

def K (x : α) (y : β) : β := y
example (h : true = false) (A : (b : Bool) → K b Type) : A true := by
  test h

This works however because it's okay to type both sides of the equality as K true Type in this example

[Joachim Breitner]

Thanks, I’ll throw this into the test suite

[Mario Carneiro]

Oh but here's a counterexample after all:

def mwe2 (h : true = false) (A : (b : Bool) → if b then Prop else Nat) : A true := by
  test h

[Joachim Breitner]

Oh, darn. This would (if I leave out the second check and use that in rw) lead to

example (h : true = false) (A : (b : Bool) → if b then Prop else Nat) : A true :=
  by -- Error: type expected
    rw [h]
    exact 0

i.e. an error at the by rather than the rw.

So I have these options

• Include both checks in the code (slower than the status quo, maybe a worry in something as common as rw?)
• Only do the second check, maybe change the error message to “motive not well-typed or dependent”
• Only do the first check, because these situations are quite unlikely
• Don't mess with rw :-)

[Mario Carneiro]

I'm not clear on why you don't just check that motive is a nondependent arrow

[Joachim Breitner]

Because of this:

./././Mathlib/CategoryTheory/Limits/IsLimit.lean:538:20: error: AppBuilder for 'congrArg', non-dependent function expected
  fun _a ↦ { pt := pt✝, π := _a }.π.app j
has type
  (_a : (Functor.cones F).obj (op pt✝)) → ((const J).obj { pt := pt✝, π := _a }.pt).obj j ⟶ F.obj j

so at least using arrow? is too picky, it seems.

[Mario Carneiro]

This already comes up elsewhere in the elaborator, it is addressed by using whnf to try to eliminate the fvar

[Joachim Breitner]

Oh, does weak head normal form help? Didn’t expect that

[Mario Carneiro]

not in general, but it works in a lot of real world cases

[Joachim Breitner]

But if some are left and rw doesn’t work there then that’s bad, isn’t it?
Ah, I guess i should just check

unless (← isTypeCorrect eqPrf)
``
and only if that fails, check some more things for good error messages.

[Mario Carneiro]

But if some are left and rw doesn’t work there then that’s bad, isn’t it?

rw never claimed to be complete, IMO this is a courtesy to avoid the "motive is not type correct" error

[Mario Carneiro]

in most cases where this comes up you should really have used dsimp first

[Mario Carneiro]

I think that even just using arrow? is fine

[Mario Carneiro]

besides, this is just an optimization, right? You can still use Eq.rec which allows a dependent function there

[Joachim Breitner]

Not sure what you mean is an optimization there? The check?

(It’s an “optional convenience” in the sense that if we’d not do the check, stuff fails later.)

I think that even just using arrow? is fine

That would make that refactoring a breaking change. But I see the point: The motive in the IsLimit example is dependent (if only in a superficial sense) and rw doesn’t do dependent rewrites, and it’s reasonable for it to fail.

[Joachim Breitner]

How does

          unless (← isTypeCorrect eqPrf) do
            unless (← isTypeCorrect motive) do
              throwTacticEx `rewrite mvarId "motive is not type correct"
            unless motive.isArrow do
              throwTacticEx `rewrite mvarId "motive is dependent"
            throwTacticEx `rewrite mvarId "equality proof is not type correct"

look? In the happy path only one isTypeCorrect is used, and in the unhappy path we put in a little low-cost effort to print a somewhat helpful error message, leading to

example (h : true = false) (A : (b : Bool) → if b then Prop else Nat) : A true :=
  by
    rw [h] -- tactic 'rewrite' failed, motive is dependent
    exact 0

[Mario Carneiro]

Not sure what you mean is an optimization there? The check?

You haven't really said what all this is for, but I'm guessing that you are testing an improved version of rw which uses congrArg instead of Eq.rec. What I'm saying is that if you can't use congrArg because of the requirement on f, then just fall back to the original proof method with Eq.rec and that way no existing cases break

[Joachim Breitner]

Using congrArg is fine (as far as I can tell), even in the example above, as you explained: Once I specify β it’s ok if the motive is “superficially dependent”. But the .arrow? function wouldn’t allow it, so I can’t use it (without breaking code) to bail out early with a helpful error message.

[Joachim Breitner]

This is for https://github.com/leanprover/lean4/pull/3121

[Mario Carneiro]

Using isTypeCorrect is a heavy hammer here in the first place. You just need to check whether two things are defeq

[Joachim Breitner]

I didn’t dare to remove Chersterton’s hammer yet :-)

[Mario Carneiro]

well you need one of them, you are adding a second fence though

[Joachim Breitner]

The isTypeCorrect eqPrf should be rather close in effect to the old isTypeCorrect motive (note that the old motive was fun a => @Eq eType e (e[a/lhs]), so type-checking that prevented unwanted dependencies). Looking at it like this I am make more fuss about this than I needed to, I guess.

[Mario Carneiro]

here's the two things:

    unless (← withLocalDeclD `_a α fun a => isDefEq (eAbst.instantiate1 a) eType) do
      throwError "eqPrf is not type correct"

[Mario Carneiro]

isTypeCorrect motive + that should ensure eqPrf is valid

[Joachim Breitner]

Thanks! I was wonder how I can just do the that isDefEq easily, but was shying away from that because of that bit of midly noisy context manipulation. But it’s not too bad after all.

[Joachim Breitner]

This check seems stricter than isTypeCorrect eqPrf, however: It now complains about

def K (x : α) (y : β) : β := y
example (h : true = false) (A : (b : Bool) → K b Type) (h2 : A false) : A true := by
  rw [h]
  exact h2

(the “non-essential dependency”), where isTypeCorrect eqPrf was happy, it seems.

Not that I mind rejecting that example, just checking if this is expected.

[Joachim Breitner]

Ignore that. After changing it to

    unless (← withLocalDeclD `_a α fun a => do isDefEq (← inferType (eAbst.instantiate1 a)) eType) do

(which I think you intended) it’s still happy with that example.

[Kyle Miller]

Have you seen that simp tries to replace its auto-generated congruence lemmas (which are proved with nested Eq.recs) with congrFun, congrArg, and congr? This seems similar in spirit to what you seem to be up to, which I'm guessing is replacing rw's Eq.rec proof in a similar way.