Elab term ensuring value

Stream: lean4

[Patrick Massot]

I know docs#Lean.Elab.Tactic.elabTermEnsuringType allow to elaborate a term while ensuring is has a given type (t : Expr). I need a variant where I want to elaborate a term while ensuring its value is defEq to a given expression. Does that exist?

[Mario Carneiro]

just elaborate it and then isDefEq the result

[Patrick Massot]

The defEq would come too late. Typically the term would be 0 < 1 and I want to compare it to (0 : Int) < 1.

[Eric Wieser]

Can you make a #mwe? Does elaborating rfl : $t = $input work?

[Patrick Massot]

The context is porting Lean verbose to Lean 4. There I have a version of suffices that allows to list multiple goals that have to be defEq to the goals created by apply.

import Mathlib.Tactic

open Lean Elab Tactic Meta

def bySufficesTac (fact : Term) (goals : Array Term) : TacticM Unit := do
  let mainGoal ← getMainGoal
  mainGoal.withContext do
  let newGoals ← mainGoal.apply (← elabTerm fact none)
  if newGoals.length != goals.size then
    throwError "Applying this leads to {newGoals.length} goals, not {goals.size}."
  let mut newerGoals : Array MVarId := #[]
  for (goal, announced) in newGoals.zip goals.toList do
    let announcedExpr ← elabTermEnsuringType announced none
    newerGoals := newerGoals.push (← goal.replaceTargetDefEq announcedExpr)
  replaceMainGoal newerGoals.toList

declare_syntax_cat maybeApplied
syntax term : maybeApplied
syntax term "applied to" term : maybeApplied
syntax term "applied to [" term,* "]" : maybeApplied

def maybeAppliedToTerm : TSyntax `maybeApplied → MetaM Term
| `(maybeApplied| $e:term) => pure e
| `(maybeApplied| $e:term applied to $x:term) => `($e $x)
| `(maybeApplied| $e:term applied to [$args:term,*]) => `($e $args*)
| _ => pure ⟨Syntax.missing⟩ -- This should never happen

elab "By " e:maybeApplied "it suffices to prove " "that "? colGt arg:term : tactic => do
bySufficesTac (← maybeAppliedToTerm e) #[arg]

example (Q : Prop) (h : ∀ n : ℤ, n > 0 → Q)  : Q := by
  --suffices 1 > 0 from h 1 this
  By h applied to (1 : ℤ) it suffices to prove (1 > 0)
  norm_num

[Patrick Massot]

The example at the bottom fails. Ideally it would work with no type ascription at all.

[Patrick Massot]

The suffices call does work (but only because there is only one auxiliary goal).

[Eric Wieser]

Eric Wieser said:

Does elaborating rfl : $t = $input work?

It doesn't

[Eric Wieser]

have : $t := (?_ : $actual_goal) seems to work

[Eric Wieser]

In fact, you can look at how show works, since that seems to do the right thing

[Thomas Murrills]

I think you’ll want to elaborate the term with mayPostpone := true (as an argument to elabTermEnsuringType) and wrap part of the code in Term.withSynthesize. The issue with using Nat instead of Int is the use of instances, and we want to postpone synthesizing an instance until after the isDefEq.

[Thomas Murrills]

See this thread for an example of doing exactly this kind of thing; skip to the last message(s) for some relevant code

[Patrick Massot]

@Thomas Murrills that seems useful but I can't find any combination of those things that actually work. Do you think you could fix my mwe?

[Kyle Miller]

I haven't read this whole thread carefully yet, but watch out that docs#Lean.Elab.Term.elabTermEnsuringType and docs#Lean.Elab.Tactic.elabTermEnsuringType are different functions with different properties. The latter chooses default instances for example, so an isDefEq would definitely come too late.

[Patrick Massot]

I had to read your message several times before I was able to spot the difference...

[Patrick Massot]

But switching to Lean.Elab.Term.elabTermEnsuringType doesn seem to help.

[Kyle Miller]

It takes some more work than just switching. Here:

import Mathlib.Tactic

open Lean Elab Tactic Meta

def bySufficesTac (fact : Term) (goals : Array Term) : TacticM Unit := do
  let mainGoal ← getMainGoal
  mainGoal.withContext do
  let newGoals ← mainGoal.apply (← elabTerm fact none)
  if newGoals.length != goals.size then
    throwError "Applying this leads to {newGoals.length} goals, not {goals.size}."
  let mut newerGoals : Array MVarId := #[]
  for (goal, announced) in newGoals.zip goals.toList do
    let announcedExpr ← Term.withSynthesize do
      let e ← Term.elabTerm announced none
      -- The `withAssignableSyntheticOpaque` is to be able to assign ?_ metavariables
      unless ← withAssignableSyntheticOpaque <| isDefEq e (← goal.getType) do
        throwError "Announced term{indentD e}\nis not definitionally equal to goal{
          ""}{indentD (← goal.getType)}"
      pure e
    newerGoals := newerGoals.push (← goal.replaceTargetDefEq announcedExpr)
  replaceMainGoal newerGoals.toList

declare_syntax_cat maybeApplied
syntax term : maybeApplied
syntax term "applied to" term : maybeApplied
syntax term "applied to [" term,* "]" : maybeApplied

def maybeAppliedToTerm : TSyntax `maybeApplied → MetaM Term
| `(maybeApplied| $e:term) => pure e
| `(maybeApplied| $e:term applied to $x:term) => `($e $x)
| `(maybeApplied| $e:term applied to [$args:term,*]) => `($e $args*)
| _ => pure ⟨Syntax.missing⟩ -- This should never happen

elab "By " e:maybeApplied "it suffices to prove " "that "? colGt arg:term : tactic => do
  bySufficesTac (← maybeAppliedToTerm e) #[arg]

example (Q : Prop) (h : ∀ n : ℤ, n > 0 → Q)  : Q := by
  By h applied to (1 : ℤ) it suffices to prove (1 > 0)
  norm_num

[Kyle Miller]

(withAssignableSyntheticOpaque isn't necessary for your example; and actually maybe it should be removed. When it's safe isn't so clear to me, but it can be annoying when it's missing from tactics.)

[Kyle Miller]

The key is that the isDefEq is happening before the extra synthesis that occurs during Term.withSynthesize

[Patrick Massot]

Great, thank you very much! This will probably be useful in other places as well.

[Kyle Miller]

I think Thomas's suggestion could be incorporated, since Tactic.elabTerm does set up different error recovery options sometimes, but I don't really know when that's used.

let e ← elabTerm announced none (mayPostpone := true)

[Patrick Massot]

That's not the same elabTerm.

[Patrick Massot]

Your doesn't have that argument, right?

[Kyle Miller]

I know, it's different, but it calls Term.elabTerm itself, and it doesn't break your example at least. I think the point is that Tactic.elabTerm makes your tactic work better for tactics like first | ... | ..., since first wants to turn off the error->sorry feature

[Kyle Miller]

But maybe you want to turn off error->sorry for your own tactic. In that case, make sure to wrap Term.withoutErrToSorry, and it seems Tactic.elabTerm wouldn't give you anything.

[Patrick Massot]

I'm sorry (or error?) but I don't understand your latest message.

[Kyle Miller]

By default, elaboration errors (like type mismatches) get turned into sorry terms, but if you elaborate from within Term.withoutErrToSorry, they raise exceptions instead.

[Patrick Massot]

I got that, but the end of you sentence is mysterious.

[Kyle Miller]

I mean if you use Term.withoutErrToSorry, it looks like there's no point in using Tactic.elabTerm (mayPostpone := true) instead of Term.elabTerm. The former conditionally does Term.withoutErrToSorry if the tactic state is in no recovery mode.

[Patrick Massot]

Ok.

[Patrick Massot]

Does the order of Term.withoutErrToSorry and Term.withSynthesize matter?

[Patrick Massot]

I currently have:

def elabTermEnsuringValue (t : Term) (val : Expr) : TermElabM Expr :=
  Term.withSynthesize do
  Term.withoutErrToSorry do
  let e ← Term.elabTerm t none
  -- The `withAssignableSyntheticOpaque` is to be able to assign ?_ metavariables
  unless ← withAssignableSyntheticOpaque <| isDefEq e val do
    throwError "Given term{indentD e}\nis not definitionally equal to the expected{
      ""}{indentD val}"
  return e

[Thomas Murrills]

Just to clarify an earlier point, Tactic.elabTermEnsuringType only chooses default instances when mayPostpone := false, right? (Using mayPostpone := true seems to avoid that choice, but I’m on mobile.)

[Kyle Miller]

Yes, that's my understanding. It'll also throw errors if instance problems are not solvable, which is fine.