Idris interactive prover won't perform rewrite on an assumption

Question

(I know the interactive prover is deprecated now in favour of elaborator reflection, but I've not got around to updating yet. Soon!)

I have the following assumptions currently available in the 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 was created using a function I wrote myself which, given natural numbers x, y, z and a proof that z ≤ y, produces a proof that x + (y - z) = (x + y) - z.

Part n x is the type of partitions of the natural number x into n pieces (each piece being a natural number), where order matters.

What I'd like to do is rewrite the type of p using pma to produce a new assumption:

p' : Part (S c) (minus (plus x m) c)

However, I tried:

let p' = rewrite pma in p

and also:

let p' = rewrite (sym pma) in p

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

rewrite did not change type letty

Where am I slipping up? I thought it might be because there's some difference between plus and + and between minus and -, but I'm pretty sure I've used them interchangeably in proofs before. Is there some other difference between the expressions that I'm missing?

I'm using Idris version 0.9.18-, if that helps.

Cactus Cactus · Accepted Answer · 2016-01-29T08:30:03

You could use pma : x + (m - c) = (x + m) - c to rewrite the type of something that is typed E1 + (E2 - E3), for some choice of E1, E2 and E3. However, you have

p : Part (S c) (plus x (minus m c))

which is not of that form. But it is of the form P (E1 + (E2 - E3)). So we need to lift your equality of

E1 + (E2 - E3) ~> (E1 + E2) - E3

to

P (E1 + (E2 - E3)) ~> P ((E1 + E2) - E3)

This is exactly what replace does:

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
replace Refl prf = prf

So in your 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)

Idris interactive prover won't perform rewrite on an assumption

1 Answers