Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: to_expr behaves differently with an expected type


Scott Morrison (May 12 2022 at 02:17):

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 (May 12 2022 at 03:32):

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 (May 12 2022 at 03:42):

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 (May 12 2022 at 07:25):

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 (May 12 2022 at 07:26):

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 (May 12 2022 at 07:53):

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 (May 15 2022 at 06:55):

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

Mario Carneiro (May 15 2022 at 07:01):

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

Scott Morrison (May 15 2022 at 07:04):

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

Scott Morrison (May 15 2022 at 07:05):

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 (May 15 2022 at 07:05):

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

Mario Carneiro (May 15 2022 at 07:05):

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

Scott Morrison (May 15 2022 at 07:06):

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

Mario Carneiro (May 15 2022 at 07:06):

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

Scott Morrison (May 15 2022 at 07:07):

Just like refine does: look up the current goal.

Mario Carneiro (May 15 2022 at 07:07):

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

Mario Carneiro (May 15 2022 at 07:07):

the issue is specific to the use of quotation

Scott Morrison (May 15 2022 at 07:08):

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 (May 15 2022 at 07:09):

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

Scott Morrison (May 15 2022 at 07:10):

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

Scott Morrison (May 15 2022 at 07:11):

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

Mario Carneiro (May 15 2022 at 07:11):

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 (May 15 2022 at 07:11):

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

Scott Morrison (May 15 2022 at 07:13):

Oh,

Scott Morrison (May 15 2022 at 07:14):

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

Mario Carneiro (May 15 2022 at 07:14):

it is using the expected type there

Scott Morrison (May 15 2022 at 07:15):

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 (May 15 2022 at 07:17):

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 (May 15 2022 at 07:21):

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 (May 15 2022 at 07:21):

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 (May 15 2022 at 07:25):

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 (May 15 2022 at 07:26):

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

Scott Morrison (May 15 2022 at 07:27):

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 (May 15 2022 at 07:27):

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

Scott Morrison (May 15 2022 at 07:28):

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

Damiano Testa (May 15 2022 at 13:45):

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 (May 15 2022 at 13:46):

(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 (May 15 2022 at 13:59):

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 (May 15 2022 at 14:00):

analogous to

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

Damiano Testa (May 15 2022 at 14:00):

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

Damiano Testa (May 15 2022 at 14:13):

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 (May 15 2022 at 14:14):

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 (May 16 2022 at 11:52):

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

Gabriel Ebner (May 16 2022 at 11:53):

Probably the one from #14153

Damiano Testa (May 16 2022 at 12:03):

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 (May 16 2022 at 12:07):

@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 (May 16 2022 at 12:08):

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

Scott Morrison (May 16 2022 at 12:08):

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

Damiano Testa (May 16 2022 at 12:09):

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 (May 16 2022 at 12:10):

No, that doesn't work for me.

Scott Morrison (May 16 2022 at 12:10):

My refine' must still not be your refine'.

Damiano Testa (May 16 2022 at 12:10):

Ok, let me dig it up!

Scott Morrison (May 16 2022 at 12:10):

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

Damiano Testa (May 16 2022 at 12:14):

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 (May 16 2022 at 13:29):

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 (May 16 2022 at 13:30):

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

Damiano Testa (May 16 2022 at 13:33):

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 (May 16 2022 at 13:33):

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

Damiano Testa (May 16 2022 at 13:42):

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 (May 16 2022 at 15:40):

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 (May 16 2022 at 23:58):

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


Last updated: Dec 20 2023 at 11:08 UTC