Different behaviour in `example` and `TermElabM`

Stream: metaprogramming / tactics

[Leni Aniva]

Why does the first one fail and the second succeed? (Lean v4.25.2) The two targets look identical

example (a b c : Nat) (h : ¬a.le b) : ∀ (s : Decidable (a + c ≤ b + c)), (if s : a + c ≤ b + c then b + c else a + c) = a + c :=
  Nat.decLe (a + b) (b + c)

#eval do
  let statement ← Elab.Term.elabTerm (← `(term|∀ (a b c : Nat) (h : ¬a.le b) (s : Decidable (a + c ≤ b + c)), (if s : a + c ≤ b + c then b + c else a + c) = a + c)) .none
  Meta.forallBoundedTelescope statement (.some 4) λ _fvars target => do
    let sol ← Elab.Term.elabTerm (← `(term|Nat.decLe (a + b) (b + c))) (.some target)
    let goal := (← Meta.mkFreshExprSyntheticOpaqueMVar target).mvarId!
    logInfo s!"{← Meta.ppGoal goal}"
    let flag ← goal.checkedAssign sol
    Meta.check (.mvar goal)
    logInfo s!"{flag}"

Notably it doesn't matter if I write Nat.decLe (a + b) or Nat.decLe (a + c)

[Leni Aniva]

Also, is there a programmatical way to solve this? Both rfl and simp can't handle the goal in example

[Robin Arnez]

Documentation of checkedAssign:

Returns true if mvarId := val was successfully assigned. This method uses the same assignment validation performed by isDefEq, but it does not check whether the types match.

[Leni Aniva]

Robin Arnez said:

Documentation of checkedAssign:

Returns true if mvarId := val was successfully assigned. This method uses the same assignment validation performed by isDefEq, but it does not check whether the types match.

Meta.check succeeds

Maybe thats not enough

[Robin Arnez]

See #lean4 > `check` doesn't check bvar/mvar/fvar exists @ 💬

[Jovan Gerbscheid]

If you want to verify that the types match, you should do that yourself, by running isDefEq (← inferType sol) target.

Instead, a better solution in this example may be to use elabTermEnsuringType, which checks this for you, and also inserts a coercion if necessary.