Is it possible to define subtraction in Primitive Recursion without a predecessor function?

Question

I have an assignment where I'm writing a bunch of basic Primitive Recursive functions, one of them is subtraction. I was not provided with a definition for predecessor and think it's unlikely I can define it as eval Pred [x] = x-1. Below is my definition of PR and I have several other functions defined such as times, AND, OR, NOT, pow, true, false, and ite. Is it possible to define subtraction with only what I have here? If so can someone give me some guidance. My current thinking is I can do something like, given minus[x,y] recurse y times then return P 2 . If y > x I should return zero. Below is my definition of PR.

 import Prelude hiding (pred,and,or,not)

 data PR = Z
     | S
     | P Int
     | C PR [PR]
     | PR PR PR
     deriving Show
 eval :: PR -> [Integer] - Integer
 eval Z _ = 0
 eval S [x] = x+1
 eval (P n) xs = nth n xs
 eval (C f gs) xs = eval f (map (\g -> eval g xs) gs)
 eval (PR g h) (0:xs) = eval g xs
 eval (PR g h) (x:xs) = eval h ((x-1) : eval (PR g h) ((x-1):xs) : xs)

 nth _ [] = error "nth nil"
 nth 0 _ = error "nth index"
 nth 1 (x:_) = x
 nth (n) (_:xs) = nth (n-1) xs

 one = C S [Z]
 plus = PR (P 1) (C S [P 2])

Edit; I've found my problem is with defining the correct base case. PR (P 3) (P 1) returns P 1 - 1, which is a step in the right direction, however, I need to recurse P 3 times. I'm thinking something like PR (PR Z (P 3)) (P 1) will do it. That of course is not correct but the idea is to recurse from P 3 to Z with P 1 decrementing each time.

Answer 1

I realized the way to do this is to define predecessor using PR.

pred = PR Z (P 1)

returns x-1 or zero if x = 0.

From there modus can be defined as follows

modus = C modus' [P 2, P 1]
modus' = PR P 1 (C pred [P 2])

Which recursively decrements P 1 P 2 times or until P 1 is equal to zero.