let in statement

Stream: lean4

[Jon Eugster]

I have a couple of teaching exercises (in a NNG-like game) about concretely defined functions and currenctly I use the following syntax for the locally defined function f:

-- import Mathlib  -- optional

example : let f : Nat → Nat := fun x ↦ 2 * x; f 4 = 8 := by
  intro f
  -- the actual exercise starts:
  rfl

I prefer this over def f := because

a) it's visible in the context (a player does only see the context, not the code before the exercise) and
b) it does not pollute any namespace with random defs.

What I dislike is that they are forced to always enter intro f as a first step and until then the goal looks rather taunting.

Does anybody have a better idea how I could write a statement such that the start of the proof is in a similar state to what it looks like after intro f currently?

f: Nat → Nat := fun x => 2 * x
⊢ f 4 = 8

Or maybe more concretely, what does intro f exactly do at this stage?

Could I achieve this in meta-code since I already replaced example by a custom elab "Statement" sig:declSig val:declVal : command => do _ which then calls elabCommand eventually (see here)

[Patrick Massot]

Sure, you could put your intro in your custom command.

[Eric Wieser]

It would be nice if theorem foo (x : Nat) (let f := _) (h : f x < 2) or similar were legal

[Jon Eugster]

Patrick Massot said:

Sure, you could put your intro in your custom command.

But if I dont know how many lets there are (0 or more) and I dont want to intro anything else (like a \forall following the let), it's not quite as simple, is it?

[Jon Eugster]

Eric Wieser said:

It would be nice if theorem foo (x : Nat) (let f := _) (h : f x < 2) or similar were legal

Would you estimate that's something one could make legal with the required meta-coding skills?:thinking:

[Patrick Massot]

You would need a intro_lets tactic.

[Patrick Massot]

This should be pretty easy.

[Jon Eugster]

You do have a point

[Eric Wieser]

Jon Eugster said:

Eric Wieser said:

It would be nice if theorem foo (x : Nat) (let f := _) (h : f x < 2) or similar were legal

Would you estimate that's something one could make legal with the required meta-coding skills?:thinking:

I think this probably would be much easier as a core change; I think extending existing syntax externally is quite awkward.

[Eric Wieser]

It might at least be worth writing an rfc

[Jon Eugster]

Patrick Massot said:

You would need a intro_lets tactic.

Indeed, after realising what I need to do it wasn't that complicated:

let_intros

import Lean.Elab.Binders
import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Intro

/-!
# `let_intros` Tactic

`let_intros` is a weaker form of `intros` aimed to only introduce `let` statements,
but not for example `∀`-binders.
-/

namespace GameServer

open Lean Meta Elab Parser Tactic

/--
Copied from `Lean.Meta.getIntrosSize`.
-/
private partial def getLetIntrosSize : Expr → Nat
  -- | .forallE _ _ b _ => getLetIntrosSize b + 1
  | .letE _ _ _ b _  => getLetIntrosSize b + 1
  | .mdata _ b       => getLetIntrosSize b
  | e                =>
    if let some (_, _, _, b) := e.letFun? then
      getLetIntrosSize b + 1
    else
      0

/--
Copied and from `Lean.MVarId.intros`.
-/
def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
  let type ← mvarId.getType
  let type ← instantiateMVars type
  let n := getLetIntrosSize type
  if n == 0 then
    return (#[], mvarId)
  else
    -- `introNP` preserves the binder names
    mvarId.introNP n

/--
`let_intros` introduces all `let` statements that are preceeding the proof. Concretely
it does a subset of what `intros` does.

If names are provided, it will introduce as many `let` statements as there are names.
-/
syntax (name := letIntros) "let_intros" (ppSpace colGt (ident <|> hole))* : tactic

@[tactic letIntros] def evalLetIntros : Tactic := fun stx => do
  match stx with
  | `(tactic| let_intros) => liftMetaTactic fun mvarId => do
    let (_, mvarId) ← mvarId.letIntros
    return [mvarId]
  | `(tactic| let_intros $ids*) => do
    let fvars ← liftMetaTacticAux fun mvarId => do
      let (fvars, mvarId) ← mvarId.introN ids.size (ids.map getNameOfIdent').toList
      return (fvars, [mvarId])
    withMainContext do
      for stx in ids, fvar in fvars do
        Term.addLocalVarInfo stx (mkFVar fvar)
  | _ => throwUnsupportedSyntax

This introduces all let statements:

example (f : Nat) :
    let f := fun x ↦ x + 1
    let g : Nat → Nat := fun y ↦ y
    ∀ x : Nat, x ≤ f x := by
  let_intros
  /-
  f✝ : Nat
  f : Nat → Nat := fun x => x + 1
  g : Nat → Nat := fun y => y
  ⊢ ∀ (x : Nat), x ≤ f x
  -/
  intro x
  exact Nat.le_succ x

Thanks for the hint!

[Kyle Miller]

The extract_lets tactic theoretically supports this, but apparently extract_lets at ⊢ is a parse error because there are zero hypotheses. You can still use it, if you create syntax with zero hypotheses:

elab "let_intros" (ppSpace colGt (ident <|> hole))* : tactic => do
  Lean.Elab.Tactic.evalTactic <| ← `(tactic| extract_lets at $(#[])* ⊢)

If you wanted to make a PR to make the location clause optional for extract_lets, then you could have extract_lets act just on the goal.

Or maybe you could add let_intros to that file for acting on just the goal? The extract_lets command is meant to be for hypotheses anyway, and it's not a good name for acting on the goal.

This is the meta implementation for acting on the goal: docs#Lean.MVarId.extractLets And this is the tactic driver: docs#Mathlib.evalExtractLet

[Jon Eugster]

#11400 cleans up extract_lets.

(I don't have any opinion on the tactic naming, so I just left it as is.)

[Eric Wieser]

Eric Wieser said:

It would be nice if theorem foo (x : Nat) (let f := _) (h : f x < 2) or similar were legal

I made an RFC for this at lean4#6091