Convert timing out

Stream: general

[Bolton Bailey]

Here is a mwe. It gives deterministic timeout. But if I remove the mv_polynomial.bind₁ call from the hypothesis and the goal, it does exactly what I want, namely to convert it to a comparison of the lambdas. Why should this extra function cause it to time out?

import data.mv_polynomial.monad

open_locale big_operators

variables (F : Type) [field F]

example (proof_elems_index : Type) (n_crs n_sample : ℕ) (twin1 twin2: fin n_crs)
  (crs_elems : (fin n_crs) → (mv_polynomial (fin n_sample) F))
  (agm: proof_elems_index → fin n_crs → F)
  (c : mv_polynomial proof_elems_index F)
  (poly_checks_pass':
    ⇑(mv_polynomial.bind₁
      (λ (pf_idx : proof_elems_index),
        ∑ (crs_idx : fin n_crs),
          agm pf_idx crs_idx
            •
          ite (crs_idx = twin1) (crs_elems twin1 + crs_elems twin2) (ite (crs_idx = twin2) 0 (crs_elems crs_idx)))) c = 0) :
  ⇑(mv_polynomial.bind₁
    (λ (pf_idx : proof_elems_index),
      ∑ (crs_idx : fin n_crs),
      agm pf_idx (ite (crs_idx = twin2) twin1 crs_idx)
        • crs_elems crs_idx)) c = 0 :=
begin
  convert poly_checks_pass',
end

[Reid Barton]

Well there's no particular reason why it shouldn't time out -- after all, maybe if we just unfold mv_polynomial.bind₁ a bit we will find out that poly_checks_pass' already has the desired type?

[Reid Barton]

And often "a bit" turns into "rather a lot" especially when the answer is that the types aren't the same in the end.

[Reid Barton]

You could start with an explicit apply congr_arg mv_polynomial.bind₁ or something.

[Reid Barton]

Probably not exactly right because of the coercion

[Bolton Bailey]

I would also have expected rw <- poly_checks_pass', congr' 1, to work, but that times out too.

[Bolton Bailey]

Why would it unfold mv_polynomial.bind₁ at all, it's there in both propositions, why shouldn't convert just eliminate it?

[Bolton Bailey]

Ok, I finally got it in the state I wanted with rw <- poly_checks_pass', apply congr, apply congr, refl, apply congr, refl,.

[Bolton Bailey]

This is still very confusing to me because I thought that congr worked essentially like repeatedly applying apply congr and refl until they failed. Can someone explain what the distinction is in how congr actually works?

[Junyan Xu]

It's indeed quite peculiar. The following also works; looks like it's checking coe_fn = coe_fn that is slow.

  rw ← poly_checks_pass',
  apply congr_fun, dsimp only,
  apply congr, refl, /- works (so does `apply congr_arg`), but `apply congr rfl`, `congr` and `congr' 1` all time out. The goal solved by `refl` is `coe_fn = coe_fn`. -/
  congr,

[Kevin Buzzard]

refine congr rfl _, works fine. My guess is that the issue isn't the rfl, could it be the apply bug? congr uses applyc which uses apply.