dec_trivial with metavariables

Stream: mathlib4

[David Ang]

What's the equivalent of dec_trivial where the statement has metavariables? Mathport tells me it's decide but it can't solve 0 < n + 1 where n is a natural number since it has the metavariable n.

[Ruben Van de Velde]

That looks like a variable, not a metavariable

[Yury G. Kudryashov]

I think that dec_trivial in Lean 3 tried to start the decision procedure even if the goal had variables. It looks like in Lean 4 it doesn't.

[Yury G. Kudryashov]

So, you should use a lemma (e.g., docs4#Nat.succ_pos in this case) and add a porting note.

[Kyle Miller]

The word you're looking for is "free variable" by the way. The error that decide gives is "expected type must not contain free or meta variables". A metavariable pretty prints as ?m for some name m.

When the issue is free variables, sometimes you can revert all the variables that the goal depends on before doing decide. That said, decide doesn't seem like the right solution for this goal.

[Yury G. Kudryashov]

As far as I understand, in Lean 3 dec_trivial tried to apply the algorithm from the decidable instance and succeeded if the algorithm didn't need any structural information that is not available.

[Yury G. Kudryashov]

E.g., in this case we know that RHS is Nat.succ _, so we can immediately say that 0 < n + 1 is true.

[Kyle Miller]

I tried turning off the check, and in this case it still can't decide that 0 < n + 1 is true.

open Lean Elab Term Meta Tactic

private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
  let mut expectedType ← instantiateMVars expectedType
  if expectedType.hasFVar then
    expectedType ← zetaReduce expectedType
  return expectedType

elab "decide'" : tactic => do
  closeMainGoalUsing fun expectedType => do
    let expectedType ← preprocessPropToDecide expectedType
    let d ← mkDecide expectedType
    let d ← instantiateMVars d
    let r ← withDefault <| whnf d
    unless r.isConstOf ``true do
      throwError "failed to reduce to 'true'{indentExpr r}"
    let s := d.appArg! -- get instance from `d`
    let rflPrf ← mkEqRefl (toExpr true)
    return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf

example (n : Nat) : 0 < n + 1 := by
  decide'
  /-
  failed to reduce to 'true'
  Decidable.rec (fun h ↦ (fun x ↦ false) h) (fun h ↦ (fun x ↦ true) h) (Nat.decLt 0 (n + 1))
  -/

[Kyle Miller]

It seems like when it reduces the expression it's able to get Nat.rec (fun x ↦ true) (fun n n_ih x ↦ true) n PUnit.unit, but it's not able to see that this is true independent of the value of n.

[David Ang]

Yeah it's a free variable (my bad), but in my defense I did have a (more complicated) example that has a bunch of metavariables :P