proof - Idris interactive prover won't perform rewrite on an assumption -

(i know interactive prover deprecated in favour of elaborator reflection, i've not got around updating yet. soon!)

i have following assumptions available in prover (among others):

x : nat c : nat m : nat lte : lte c m pma : x + (m - c) = (x + m) - c p : part (s c) (plus x (minus m c)) 

pma created using function wrote myself which, given natural numbers x, y, z , proof z ≤ y, produces proof x + (y - z) = (x + y) - z.

part n x type of partitions of natural number x n pieces (each piece being natural number), order matters.

what i'd rewrite type of p using pma produce new assumption:

p' : part (s c) (minus (plus x m) c) 

however, tried:

let p' = rewrite pma in p 

and also:

let p' = rewrite (sym pma) in p 

because can never remember way round rewrite works, , in both cases got:

rewrite did not change type letty 

where slipping up? thought might because there's difference between plus , + , between minus , -, i'm pretty sure i've used them interchangeably in proofs before. there other difference between expressions i'm missing?

i'm using idris version 0.9.18-, if helps.

you use pma : x + (m - c) = (x + m) - c rewrite type of typed e1 + (e2 - e3), choice of e1, e2 , e3. however, have

p : part (s c) (plus x (minus m c)) 

which not of form. is of form p (e1 + (e2 - e3)). need lift equality of

e1 + (e2 - e3) ~> (e1 + e2) - e3 

to

p (e1 + (e2 - e3)) ~> p ((e1 + e2) - e3) 

this replace does:

replace : {a:_} -> {x:_} -> {y:_} -> {p : -> type} -> x = y -> p x -> p y replace refl prf = prf 

so in particular case, given

pma : x + (m - c) = (x + m) - c 

then

replace {part (s c)} pma : part (s c) (x + (m - c)) -> part (s c) ((x + m) - c) 

and in particular,

replace {part (s c)} pma p : part (s c) ((x + m) - c)