Really strict guard_hyp

Stream: lean4

[Patrick Massot]

In Lean 3, the strict version of guard_hyp was sensitive even to bound variable names. I thought this was the same in Lean 4 but:

example (h : ∃ k : Nat, k = k) : True := by
  guard_hyp h :ₛ ∃ l : Nat, l = l -- I hoped this would have failed
  trivial

Is this is a bug? Is there another variant that would catch this?

[Kyle Miller]

That seems to be an oversight. lean4#6483 (still pending updating tests and fixing mathlib)

[Patrick Massot]

Thanks Kyle! I just wrote

elab "guard_hyp_strict" hyp:ident " : " val:term : tactic => withMainContext do
    let fvarid ← getFVarId hyp
    let lDecl ←
      match (← getLCtx).find? fvarid with
      | none => throwError m!"hypothesis {hyp} not found"
      | some lDecl => pure lDecl
    let e ← elabTerm val none
    let hty ← instantiateMVars lDecl.type
    unless e.equal hty do
      throwError m!"hypothesis {hyp} has type{indentExpr hty}\nnot{indentExpr e}"

example (h : ∃ k : Nat, k = k) : True := by
  guard_hyp_strict h : ∃ l : Nat, l = l -- I hoped this would have failed
  trivial

in Verbose Lean, using docs#Lean.Expr.equal just like in your fix!

[Patrick Massot]

(and copy-pasting a bit of the guard_hyp implementation of course).

[Patrick Massot]

However I wonder whether this means there should have a new MatchKind here. Do you claim the existing syntactic kind is an actual strict duplicate?

[Kyle Miller]

Maybe there could be a different matching kind (to account for whether to consume mdata), but both .alphaEq and .syntactic were using Expr.eqv (which is what == is defined to use), and Expr.equal is definitely the syntactic equality.

[Patrick Massot]

Ok, I missed that fact that == uses Expr.eqv.

[Patrick Massot]

Since you are in this corner of Lean, it would be nice if success_if_fail_with_msg could have a code action to fix the message like guard_hyp does.

[Kyle Miller]

(One side effect of this change is that now a -> b and a -> b aren't necessarily syntactically equal, since there's a hidden binder name inside these foralls.)

[Kyle Miller]

success_if_fail_with_msg seems to be a mathlib tactic

[Patrick Massot]

Weird, I was sure I checked.

[Kyle Miller]

@Mario Carneiro For #guard_*'s syntatic equality, should we have a pass that normalizes binder names for non-dependent foralls? Or do we accept that we need to use alpha equality instead of syntactic equality in such cases? Or maybe you have some other ideas?

[Patrick Massot]

Indeed it’s in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/SuccessIfFailWithMsg.lean

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kyle Miller said:

Mario Carneiro For #guard_*'s syntatic equality, should we have a pass that normalizes binder names for non-dependent foralls? Or do we accept that we need to use alpha equality instead of syntactic equality in such cases? Or maybe you have some other ideas?

Since this came up again here: I would certainly support having the normalization pass (or yet another Expr.equal' that ignores non-dependent binders.) Without it, Expr.equal ended up being near useless in my tests.