Weird rewrite problem with Coq: https://github.com/bollu/SCEV-coq/commit/9c62cb17765189f34c1170c314f97539d6c60e06

problem.md

Goal

  IHn : (PureCRRec begin1' cr1) # n + (PureCRRec begin2' cr2) # n =
        (PureCRRec (begin1' + begin2') p) # n
  ============================
  (PureCRRec begin1' cr1) # n + (PureCRRec begin2' cr2) # n +
  (cr1 # (S n) + cr2 # (S n)) =
  (PureCRRec (begin1' + begin2') p) # n + p # (S n)

Tactic run:

rewrite IHn.

Rewrite error

Error:
Found no subterm matching "(PureCRRec begin1' cr1) # n +
                           (PureCRRec begin2' cr2) # n" in the current goal.

I don't understand this, the goal state is clearly in the goal, so what's the problem?

Commit, project:

• Commit 9c62cb17765189f34c1
• githb.com/bollu/scev-coq

Full goal state

                              ring0, ring1 : R
  add0, mul0, sub0 : R -> R -> R
  opp : R -> R
  ring_eq : R -> R -> Prop
  Ro : Ring_ops
  H : Ring
  begin1' : R
  cr1 : PureCR plus
  IHcr1 : forall cr2 pureout : PureSumCR,
          zip_purecrs_eq_len cr1 cr2 = Some pureout ->
          forall n : nat, cr1 # n + cr2 # n = pureout # n
  begin2' : R
  cr2 : PureCR plus
  IHcr2 : forall pureout : PureSumCR,
          zip_purecrs_eq_len (PureCRRec begin1' cr1) cr2 =
          Some pureout ->
          forall n : nat,
          (PureCRRec begin1' cr1) # n + cr2 # n = pureout # n
  pureout : PureSumCR
  p : PureCR plus
  ZIP_CR1_CR2 : zip_purecrs_eq_len cr1 cr2 = Some p
  ZIP : Some (PureCRRec (begin1' + begin2') p) = Some pureout
  n : nat
  H1 : PureCRRec (begin1' + begin2') p = pureout
  IHn : (PureCRRec begin1' cr1) # n + (PureCRRec begin2' cr2) # n =
        (PureCRRec (begin1' + begin2') p) # n
  ============================
  (PureCRRec begin1' cr1) # n + (PureCRRec begin2' cr2) # n +
  (cr1 # (S n) + cr2 # (S n)) =
  (PureCRRec (begin1' + begin2') p) # n + p # (S n)