Getting expected type in TermElabM

Stream: lean4

[Adam Topaz]

Do we have some way to obtaining the Expr associated to the expected type in TermElabM?
As a basic example, say I want to write a term elaborator foo% that would work in the following cases:

example : Nat := foo%
example : Rat := foo%

giving 0 in the Nat case and 1 in the Rat case, and resulting in an error in all other cases.

[Kyle Miller]

Yes you can. It seems the only way to optionally get an expected type at the moment is if you write a separate syntax and term_elab

syntax (name := fooStx) "foo%" : term

@[term_elab fooStx]
def elabFoo : Term.TermElab := fun stx expectedType? => do
  match stx with
  | `(foo%) => ...
  | _ => throwUnsupportedSyntax

[Adam Topaz]

Ah great. Thanks Kyle!

[Kyle Miller]

There's some syntax for the elab command to require an expected type, but that causes the elaborator to postpone until it knows the expected type, and if it can't know one it throws an error.

[Kyle Miller]

I guess that actually would work for you.

[Adam Topaz]

What's that syntax?

[Kyle Miller]

import Lean

open Lean Elab Term

elab "foo%" : term <= expectedType => do
  let expectedType ← instantiateMVars expectedType
  match expectedType with
  | .const ``Nat .. => elabTerm (← `((37 : Nat))) none
  | .const ``Rat .. => elabTerm (← `((17 : Rat))) none
  | _ => throwError "The expected type should be Nat or Rat, not{indentD expectedType}"

example : Nat := foo%
example : Rat := foo%

[Adam Topaz]

All the discussion about iterated products in Tao's PFR project made me curious about how automation could help. So I made an elaborator that automatically constructs "obvious" equivalences between iterated products, regardless of how they're associated. The reason for my question is that I wanted to make this as convenient as possible to use. There are two variants now: prod_assoc% for when the types can be infered and prod_assoc(..., ...) requiring the user to provide them explicitly. This still feels hacky to me. Does anyone have any suggestions for how to best make this work?

the draft PR is here: #8551 (with examples at the bottom of the file)

[Kyle Miller]

You could avoid the special case of prod_assoc(..., ...) by using the syntax

(prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ)

[Adam Topaz]

Sure, that's only slightly more verbose than prod_assoc(..., ...)

[Adam Topaz]

What I really want is to be able to write prod_assoc(_, ...) if I know that the input can be inferred but not the output, and similarly with the two interchanged.

[Adam Topaz]

But maybe (prod_assoc% : _ ≃ α × (β × γ) × δ) is good enough in that case.

[Adam Topaz]

Hmm.... This still fails:

elab "associate%" : term <= expectedType => do
  match expectedType with
    | .app (.app (.const ``Equiv _) a) b => do
      mkProdEquiv a b
    | _ => throwError "Expected type {expectedType} is not of the form `α ≃ β`."

example {α β γ δ : Type*} (x : (α × β) × (γ × δ)) : α × (β × γ) × δ := associate% x

Do you have any hints for how to make this work?

[Kyle Miller]

I just got this example to work:

example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ :=
  (prod_assoc% : _ ≃ α × β × γ × δ).trans prod_assoc%

[Kyle Miller]

code

-- after your `mkProdEquiv`

syntax (name := prodAssocStx) "prod_assoc_internal%" : term

open Elab in
@[term_elab prodAssocStx]
def elabProdAssoc : Term.TermElab := fun stx expectedType? => do
  match stx with
  | `(prod_assoc_internal%) => do
    let some expectedType ← Term.tryPostponeIfHasMVars? expectedType?
          | throwError "expected type must be known"
    let .app (.app (.const ``Equiv _) a) b := expectedType
          | throwError "Expected type {expectedType} is not of the form `α ≃ β`."
    mkProdEquiv a b
  | _ => throwUnsupportedSyntax

macro "prod_assoc%" : term => `((prod_assoc_internal% : _ ≃ _))

variable {α β γ δ : Type*}

example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ := by
  have := (prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ)
  exact this
example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ := prod_assoc%

example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ :=
  (prod_assoc% : _ ≃ α × β × γ × δ).trans prod_assoc%

[Adam Topaz]

Nice! I'll take a closer look after I eat some lunch :)

[Adam Topaz]

Awesome! with your code Kyle this works as well:

example {α β γ δ : Type*} (x : (α × β) × (γ × δ)) : α × (β × γ) × δ := prod_assoc% x

[Adam Topaz]

I think that PR should be ready to review now :) Thanks again Kyle!

[Kyle Miller]

I'm enjoying these Lean 4 days of Lean. We've got a lot of flexibility now!