You can make any of the methods you discuss work, but to reiterate, the simplest is a straight resistor divider. R1 goes from the ~12V high source to the PIC pin. R2 goes from the pic pin to ground.
Then: Vpin = vsource*(R2/(R1+R2)) As I stated above, the biggest Vsource you will see is 14.4V. The biggest Vpin you can stand is 5V.
so 14.4=5*(R2/(R1+R2)).
So 14.4/5 =R2/(R1+R2)
so 2.88 =R2/(R1+R2)
Now go hunting for the standard resistor values that when plugged into R1 and R2 = 2.88
Look for values between 1K and 100K
You probably won't find an exact match (43K & 15K might be close enough), although to be as safe as possible, err on R1 being just a bit higher than the ration implies.