polyrith found certificate but failed to close the goal

Stream: general

[Bolton Bailey]

I am getting the following error message from polyrith
polyrith found the following certificate, but it failed to close the goal:
How should I interpret this?

Interestingly, I don't get the error message when I write a bunch of set statements to simplify terms in the state, polyrith just works fine. Does polyrith refuse to work on states that are too complicated in some way?

[Bolton Bailey]

Hmm, perhaps the issue could be a multiplication inside a binder that is throwing the linear_combination call off?

[Bolton Bailey]

  linear_combination -(1 * h0022) +
      Polynomial.C (prover.2 Proof_Right_Idx.B CRS_Elements_Right_Idx.δ) *
          Polynomial.C (prover.1 Proof_Left_Idx.A CRS_Elements_Left_Idx.α) *
        h0121 +
    (-(1 *
              List.sum
                (List.map
                  (fun x =>
                    Polynomial.C (prover.1 Proof_Left_Idx.A (CRS_Elements_Left_Idx.x_pow_times_t x)) *
                      (Polynomial.X ^ ↑x * ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))) --- failed to synthesize instance HPow
                  (List.finRange (n_var - 1))) *
            Polynomial.C (prover.2 Proof_Right_Idx.B CRS_Elements_Right_Idx.δ)) -
        1 * Polynomial.C (prover.2 Proof_Right_Idx.B CRS_Elements_Right_Idx.δ) *
          List.sum
            (List.map (fun x => Polynomial.C (prover.1 Proof_Left_Idx.A (CRS_Elements_Left_Idx.q x)) * w_wit x)
              (List.finRange n_wit))) *
      h1122

[Notification Bot]

Bolton Bailey has marked this topic as resolved.

[Eric Rodriguez]

I usually see this when I try polyrith on types that aren't "fully-featured", eg the certificate requires division but I'm actually in Z (although obviously this could be made to work as it's a domain, but I digress)

[Kevin Buzzard]

Can you minimise?

[Bolton Bailey]

example [Field F] (a b c : F)  (h : a ^ ((10 : Fin 37) : ℕ) = b) (h2 : b = c) :
    a ^ ((10 : Fin 37) : ℕ) * b = b * c := by
  polyrith

[Bolton Bailey]

polyrith found the following certificate, but it failed to close the goal:
c * h + a ^ ↑10 * h2

[Eric Rodriguez]

Does ((a : Fin 37) : Nat) work instead?

[Bolton Bailey]

No same error.

[Bolton Bailey]

It seems the ↑ is messing it up. I feel like whenever I copy paste something from the infoview to the file it's often this that breaks.

[Kevin Buzzard]

linear_combination c * h + a ^ ((10 : Fin 37) : ℕ) * h2 does close the goal, so it does look like it's an up-arrow issue.

[Notification Bot]

Kevin Buzzard has marked this topic as unresolved.

[Bolton Bailey]

Is there any way to fix this, perhaps by forking polyrith and making some small tweak? For that matter, is there a way to make it so that casts that the infoview displays are displayed as (x : T) rather than ↑x?

[Kyle Miller]

For numeric literals, lean4#2933 gives pp.numericTypes to make numbers pretty print with type ascriptions, though that might not help here.

For ↑ in general, that's controlled by https://github.com/leanprover/std4/blob/main/Std/Tactic/CoeExt.lean and it doesn't have any option to pretty print type ascriptions (yet?).

[Kyle Miller]

Type ascriptions aren't the same as coercions, so maybe it would need to pretty print as (↑(x : T1) : T2) to be accurate.