Why rewrite does not change type of expression in

In (*1) one can read next

rewrite prf in expr

If we have prf : x = y, and the required type for expr is some property of x, the rewrite ... in syntax will search for x in the required type of expr and replace it with y.

Now, I have next piece of code (you can copy it to editor and try ctrl-l)

module Test

plusCommZ : y = plus y 0
plusCommZ {y = Z} = Refl
plusCommZ {y = (S k)} = cong $ plusCommZ {y = k}

plusCommS : S (plus y k) = plus y (S k)
plusCommS {y = Z} = Refl
plusCommS {y = (S j)} {k} = let ih = plusCommS {y=j} {k=k} in cong ih

plusComm : (x, y : Nat) -> plus x y = plus y x
plusComm Z y = plusCommZ
plusComm (S k) y =
  let
    ih = plusComm k y
    prfXeqY = sym ih
    expr = plusCommS {k=k} {y=y}
    -- res = rewrite prfXeqY in expr
  in ?hole

below is how hole looks like

- + Test.hole [P]
 `--          k : Nat
              y : Nat
             ih : plus k y = plus y k
        prfXeqY : plus y k = plus k y
           expr : S (plus y k) = plus y (S k)
     -----------------------------------------
      Test.hole : S (plus k y) = plus y (S k)

The Question. It looks to me like expr (from *1) in commented line equals to S (plus y k) = plus y (S k). And prf equals to plus y k = plus k y where x is plus y k and y is plus k y. And rewrite should search for x (namely for plus y k) in expr (namely S (plus y k) = plus y (S k) and should replace x with y (namely with plus k y). And result (res) should be S (plus k y) = plus y (S k).

But this does not work.

I have next answer from idris

rewriting plus y k to plus k y did not change type letty

I could guess rewrite is intended to change type of the resulting expression only. So, it is not working within body of let expression, but only in it's 'in' part. Is this correct?

(*1) http://docs.idris-lang.org/en/latest/proofs/patterns.html

PS. Example from tutoral works fine. I'm just curious to know why the way I've tryed to use rewrite didn't work.

回答1:

Though not stated explicitly stated in the docs, rewrite is syntax-sugary invocation of an Elab tactics script (defined around here).

To why your example does not work: the "required type of expr" isn't found; with just res = rewrite prfXeqY in expr alone, it is unclear, which type res should have (even the unifier could resolve this with let res = … in res.) If you specify the required type, it works as expected:

res = the (S (plus k y) = plus y (S k)) (rewrite prfXeqY in expr)

回答2:

Unfortunately you did not provide the exact line which makes your code misbehave, somehow you must have done something strange, since with your reasoning you outlined above the code works well:

  let
    ih = plusComm k y -- plus k y = plus y k
    px = plusCommS {k=k} {y=y} -- S (plus y k) = plus y (S k)
    in rewrite ih in px