to_expr behaves differently with an expected type

Stream: metaprogramming / tactics

[Scott Morrison]

to_expr behaves differently with an expected type: observe

import algebra.big_operators.basic

open tactic

example (α : Type) : finset ℕ → α :=
begin
  (do
    e ← to_expr ``(λ s : finset ℕ, s.sum _), -- works, generating a `add_comm_monoid α` goal
    exact e),
  sorry,
  sorry
end

example (α : Type) : finset ℕ → α :=
begin
  (do
    tgt ← target,
    e ← to_expr ``(λ s : finset ℕ, s.sum _ : %%tgt), -- failed to synthesize type class instance for `add_comm_monoid α`
    exact e),
end

Is there a way I can persuade to_expr to work, generating new goals for failed typeclass inference, but with the presence of an expected type?

[Damiano Testa]

This is not an answer, but me trying to understand at least what the problem is! Is what you are asking analogous to what's below in tactic mode?

example (α : Type) : finset ℕ → α :=
begin
--  failed to synthesize type class instance for `add_comm_monoid α`
  refine λ s : finset ℕ, s.sum _,
end

example (α : Type) : finset ℕ → α :=
begin
-- works, generating a `add_comm_monoid α` goal
  apply λ s : finset ℕ, s.sum _,
end

[Damiano Testa]

If this is what it is, then there is an extended comment to i_to_expr_for_apply that may be useful, if I understood better what it said!

[Scott Morrison]

Yes, under the hood refine differs from apply by calling to_expr with the expected type before calling exact. (Perhaps I should have just asked the question about refine and apply, in fact.)

[Scott Morrison]

I did read those comments on i_to_expr_for_apply, but didn't get what I wanted. Maybe I will read them again, thanks. :-)

[Damiano Testa]

Honestly, I feel very relieved that even you have a hard time with the meta world: I find it very hard to navigate, while at the same time feel that it should be easy!

[Scott Morrison]

@Mario Carneiro, @Gabriel Ebner, do either of you know what is going on here, or a workaround?

[Mario Carneiro]

Is e ← to_expr ``(λ s : finset ℕ, @finset.sum %%tgt _ (id _) s _), an acceptable workaround?

[Scott Morrison]

Oh, that seems way too specific to this particular example.

[Scott Morrison]

If the intended use case were some variant of refine that would generate instance goals, how would refine' λ s : finset ℕ, s.sum _ possibly know where exactly it was meant to insert the %%tgt in your solution?

[Scott Morrison]

Or for that matter how would refine' decide which underscores need to be wrapped in id _?

[Mario Carneiro]

oh you don't have to insert the %%tgt there, you can keep it on the outside

[Scott Morrison]

Okay, so the second question then? How to automatically insert the ids?

[Mario Carneiro]

I'm not sure how you are getting this %%tgt from a generic elaborator

[Scott Morrison]

Just like refine does: look up the current goal.

[Mario Carneiro]

no I mean refine doesn't use quotations and antiquotation like this

[Mario Carneiro]

the issue is specific to the use of quotation

[Scott Morrison]

But here's the definition of refine:

meta def refine (e : pexpr) : tactic unit :=
do tgt : expr ← target,
   to_expr ``(%%e : %%tgt) tt >>= exact

[Scott Morrison]

So I think refine is using (anti)quotation like this.

[Scott Morrison]

And it is the to_expr step of refine that fails when if can't immediately solve the typeclass search.

[Scott Morrison]

(but would have succeeded if we hadn't given an expected type via : %%tgt)

[Mario Carneiro]

how about

  (do
    let e : pexpr := ``(λ s : finset ℕ, s.sum _),
    tgt ← target,
    e ← to_expr e,
    infer_type e >>= unify tgt,
    exact e),

[Scott Morrison]

I'll go play with that in my bigger examples. :-)

[Scott Morrison]

Oh,

[Scott Morrison]

no, this is not helping: I want the advantages of the expected type, so I don't have to write everything out.

[Mario Carneiro]

it is using the expected type there

[Scott Morrison]

e.g. if I defined

setup_tactic_parser

namespace tactic

meta def refine' (e : pexpr) : tactic unit :=
do
  tgt ← target,
  e ← to_expr e,
  infer_type e >>= unify tgt,
  exact e

namespace interactive

meta def refine' (q : parse texpr) : tactic unit :=
tactic.refine' q

end interactive

end tactic

then

example (α : Type*) : finset ℕ → α :=
begin
  refine' (λ s, s.sum _),
  show ℕ → α, exact id,
  apply_instance,
end

fails, showing refine' is not a good replacement for refine, because it can't work out the type of the lambda binder.

[Mario Carneiro]

to be fair,

  refine' (λ s:finset ℕ, (s.sum _ : α)),
  refine' (λ s, s.sum _ : finset ℕ → α),

also don't work, for the reasons you have already indicated, so I'm not sure the expected type is the issue here

[Scott Morrison]

Hmm... okay. What I want is a variant of refine so the following works:

example : Σ (α : Type), finset ℕ → α :=
begin
  let α := _,
  refine' ⟨α, λ s : finset ℕ, s.sum _⟩,
  show ℕ → α, exact id,
  apply_instance,
end

[Mario Carneiro]

I think you need to change the elaborator itself if you want it to give you back the pending typeclass goals. Like the comment for i_to_expr_for_apply says:

   Another possible fix: we modify the elaborator to return pending
   type class resolution problems, and store them in the tactic_state.

[Scott Morrison]

My last example feels like a very common step of "human reasoning" that just isn't expressible in the natural order in Lean at the moment. I really want the proof to reflect the idea "I know I want to take some sum over my finset, but I don't yet know what the codomain of the function I'm summing ought to be", so at a later step we can reflect the human idea "oh, it suffices now to take α = ℕ and use the identity function".

[Mario Carneiro]

you can still write essentially this proof with the id... it's not pretty but it works in a pinch

[Scott Morrison]

And is then completely un-explainable to a Lean beginner. :-) Which doesn't help when the goal here is to show that one can express the human chain of reasoning directly...

[Mario Carneiro]

not sure what to tell you... I'm not up to patching lean right now

[Scott Morrison]

No, that's great already. Knowing that I'm not just missing something is an excellent answer. :-)

[Damiano Testa]

I've just been working with the congr_with_pattern_match and for this reason, I think that it could be a solution to everything. :wink:

Do you think that you might be able to do a similarly assisted pattern-matching, where the three inputs are

• the given expression with metavariables e,
• itself again eas the lhs and
• the actual target as the rhs?

[Damiano Testa]

(I can try, but since I only recursed inside expr.apps, it will take me a while to get to a stage where it recurses far enough into an expr that I can really see if it applies (refines?) or not.)

[Damiano Testa]

E.g., simply changing

meta def refine' (e : pexpr) : tactic unit :=
do
  tgt ← target,
  e' ← to_expr e >>= infer_type,trace e',
  equate_with_pattern e' e' tgt

and then doing

example (α : Type*) : finset ℕ → α :=
begin
  refine' (λ s : finset ℕ, s.sum _),
/-  Goals:
α: Type ?
⊢ finset ℕ → α
α: Type ?
s: finset ℕ
⊢ Type ?
α: Type ?
s: finset ℕ
⊢ add_comm_monoid ?m_1
α: Type ?
s: finset ℕ
⊢ ℕ → ?m_1
-/
end

[Damiano Testa]

analogous to

example (α : Type*) : finset ℕ → α :=
begin
  apply (λ s : finset ℕ, s.sum _),
/-  Goals:
α: Type ?
s: finset ℕ
⊢ add_comm_monoid α
α: Type ?
s: finset ℕ
⊢ ℕ → α
-/
end

[Damiano Testa]

It possibly needs a tiny little bit more of unification, but seems like a possible compromise, maybe.

[Damiano Testa]

This might work:

meta def tactic.refine' (e : pexpr) : tactic unit :=
do
  tgt ← target,
  e' ← to_expr e tt ff >>= infer_type,   --    <---  added the ascription `tt ff` to `to_expr`
  equate_with_pattern e' tgt e',
  unify e' tgt,  --  added unification, since I mistakenly removed it from the copied code
  apply e  --  `apply` not `exact`!

[Damiano Testa]

example (α : Type*) : finset ℕ → α :=
begin
  refine' (λ s : finset ℕ, s.sum _),  -- don't know how to get rid of the type annotation  `s : finset ℕ`
/-
2 goals
α: Type ?
s: finset ℕ
⊢ add_comm_monoid α

α: Type ?
s: finset ℕ
⊢ ℕ → α
-/
end

[Scott Morrison]

@Damiano Testa, where do I get this equate_with_pattern from?

[Gabriel Ebner]

Probably the one from #14153

[Damiano Testa]

Indeed, it is that one. Although, I could not get it to work with your example:

example (α : Type*) : finset ℕ → α :=
begin
  refine' (λ s, s.sum _),
  show ℕ → α, exact id,
  apply_instance,
end

[Scott Morrison]

@Damiano Testa, I'm not certain what you're suggesting, but this is my attempt to reconstruct it. Could you confirm this is what you intended?

import algebra.big_operators.basic

setup_tactic_parser

namespace tactic

meta def equate_with_pattern : expr → expr → expr → tactic unit
| (expr.app f e) (expr.app f0 e0) (expr.app f1 e1) := do
  match e with
  | (expr.mvar _ _ _) := do
    el ← mk_app `eq [e0, e1],
    n ← get_unused_name "h",
    assert n el,
    interactive.rotate,
    get_local n >>= rewrite_target,
    equate_with_pattern f f0 f1
  | _ := do equate_with_pattern e e0 e1 *> equate_with_pattern f f0 f1
  end
| _ _ _ := skip

meta def refine' (e : pexpr) : tactic unit :=
do
  tgt ← target,
  e' ← to_expr e tt ff >>= infer_type,   --    <---  added the ascription `tt ff` to `to_expr`
  equate_with_pattern e' tgt e',
  unify e' tgt,  --  added unification, since I mistakenly removed it from the copied code
  apply e' >> skip --  `apply` not `exact`!

namespace interactive

meta def refine' (q : parse texpr) : tactic unit :=
tactic.refine' q

end interactive

end tactic

example : Σ (α : Type), finset ℕ → α :=
begin
  let α := _,
  refine ⟨α, _⟩,
  refine' λ s : finset ℕ, s.sum _, -- invalid apply tactic, failed to unify `finset ℕ → α` with  `Type`
  show ℕ → α, exact id,
  apply_instance,
end

[Scott Morrison]

(Note in the line apply e in your version, I had to change this to apply e' >> skip. Hopefully that is correct?

[Scott Morrison]

This doesn't work for me, still. I've noted the error above `-- invalid apply tactic, failed to unify finset ℕ → α with Type```.

[Damiano Testa]

Scott, this is indeed what I had. It does not work for me either, but worked on the simpler examples that started the chat:

example (α : Type*) : finset ℕ → α :=
begin
  refine' (λ s : finset ℕ, s.sum _),  -- don't know how to get rid of the type annotation  `s : finset ℕ`
/-
2 goals
α: Type ?
s: finset ℕ
⊢ add_comm_monoid α

α: Type ?
s: finset ℕ
⊢ ℕ → α
-/
end

[Scott Morrison]

No, that doesn't work for me.

[Scott Morrison]

My refine' must still not be your refine'.

[Damiano Testa]

Ok, let me dig it up!

[Scott Morrison]

Could you post a self-contained code block that contains the last example you posted?

[Damiano Testa]

I'm failing to reproduce: I must have changed something else. I have a meeting now, but will get back to you as soon as I am done!

[Damiano Testa]

Ok, I do not know whether this is useful, but I think that this is what I had:

import tactic.interactive
import algebra.gcd_monoid.finset

namespace tactic.interactive
open tactic interactive
setup_tactic_parser

meta def decomp : expr → expr → expr → tactic unit
| (expr.app f e) (expr.app f0 e0) (expr.app f1 e1) :=
  match e with
  | (expr.mvar _ _ _) := do
    el ← mk_app `eq [e0, e1],
    n ← get_unused_name "h",
    assert n el,
    swap,
    decomp f f0 f1,
    rotate_right 1
  | _ := do decomp f f0 f1 *> decomp e e0 e1
  end
| _ _ _ := skip

meta def refine' (e : parse texpr) : tactic unit :=
do
  tgt ← target,
  e' ← to_expr e tt ff >>= infer_type,
  decomp e' tgt e',
  unify e' tgt,
  apply e

end tactic.interactive

example (α : Type*) : finset ℕ → α :=
begin
  refine' (λ s : finset ℕ, s.sum _),
/-2 goals
α: Type ?
s: finset ℕ
⊢ add_comm_monoid α
α: Type ?
s: finset ℕ
⊢ ℕ → α
-/
end

[Damiano Testa]

I wonder whether I simply implemented an inefficient version of apply, though...

[Damiano Testa]

I am confused: this now seems to work:

example : Σ (α : Type), finset ℕ → α :=
begin
  let α := _,
  refine ⟨α, _⟩,
  refine' λ s : finset ℕ, s.sum _, -- invalid apply tactic, failed to unify `finset ℕ → α` with  `Type`
  show ℕ → α, exact id,
  apply_instance,
end

[Damiano Testa]

Scott, if you can verify any of the above and let me know any discrepancies, I would be happy to debug!

[Damiano Testa]

Scott, looking at the last quoted example, I learned that show ... does what I thought any_goals { show ... } did. This tripped me up!

I thought that show and change were synonyms.

[Damiano Testa]

Scott Morrison said:

Hmm... okay. What I want is a variant of refine so the following works:

example : Σ (α : Type), finset ℕ → α :=
begin
  let α := _,
  refine' ⟨α, λ s : finset ℕ, s.sum _⟩, -- invalid apply tactic, failed to unify `finset ℕ → α` with  `Type`
  show ℕ → α, exact id,
  apply_instance,
end

@Scott Morrison , I think that all that what all my playing around reduces to is that apply works here as refine', but this is exactly where you started, so I have been walking around in circles:

import algebra.big_operators.basic

example : Σ (α : Type), finset ℕ → α :=
begin
  let α := _,
  refine ⟨α, _⟩,
  apply λ s : finset ℕ, s.sum _,  -- three goals: `add_comm_monoid α`, `ℕ → α`, `Type`
  show ℕ → α, exact id,
  apply_instance,
end

Sorry about the noise. :face_palm:

[Scott Morrison]

It's okay. :-) Thanks for taking a look at it.