Idris: proof that specific terms are impossible

Question

Idris version: 0.9.16

---

I am attempting to describe constructions generated from a base value and an iterated step function:

namespace Iterate
  data Iterate : (base : a) -> (step : a -> a) -> a -> Type where
    IBase : Iterate base step base
    IStep : Iterate base step v -> Iterate base step (step v)

Using this I can define Plus, describing constructs from iterated addition of a jump value:

namespace Plus
  Plus : (base : Nat) -> (jump : Nat) -> Nat -> Type
  Plus base jump = Iterate base (\v => jump + v)

Simple example uses of this:

namespace PlusExamples
  Even : Nat -> Type; Even = Plus 0 2
  even0 : Even 0; even0 = IBase
  even2 : Even 2; even2 = IStep even0
  even4 : Even 4; even4 = IStep even2

  Odd  : Nat -> Type; Odd  = Plus 1 2
  odd1 : Odd 1; odd1 = IBase
  odd3 : Odd 3; odd3 = IStep odd1

  Fizz : Nat -> Type; Fizz = Plus 0 3
  fizz0 : Fizz 0; fizz0 = IBase
  fizz3 : Fizz 3; fizz3 = IStep fizz0
  fizz6 : Fizz 6; fizz6 = IStep fizz3

  Buzz : Nat -> Type; Buzz = Plus 0 5
  buzz0 : Buzz 0; buzz0 = IBase
  buzz5 : Buzz 5; buzz5 = IStep buzz0
  buzz10 : Buzz 10; buzz10 = IStep buzz5

The following describes that values below the base are impossible:

  noLess : (base : Nat) ->
           (i : Fin base) ->
           Plus base jump (finToNat i) ->
           Void
  noLess Z     FZ     m     impossible
  noLess (S b) FZ     IBase impossible
  noLess (S b) (FS i) IBase impossible

And the following for values between base and jump + base:

  noBetween : (base : Nat) ->
              (predJump : Nat) ->
              (i : Fin predJump) ->
              Plus base (S predJump) (base + S (finToNat i)) ->
              Void
  noBetween b Z     FZ     m     impossible
  noBetween b (S s) FZ     IBase impossible
  noBetween b (S s) (FS i) IBase impossible

---

I am having trouble defining the following function:

noJump : (Plus base jump n -> Void) -> Plus base jump (jump + n) -> Void
noJump f m = ?noJump_rhs

That is: if n isn't base plus a natural multiple of jump, then neither is jump + n.

If I ask Idris to case split m it only shows me IBase - then I get stuck.

Would someone point me in the right direction?

---

Edit 0: Applying induction to m gives me the following message:

Induction needs an eliminator for Iterate.Iterate.Iterate

---

Edit 1: Name updates and here is a copy of the source: http://lpaste.net/125873

Answer 1

I think there's a good reason to get stuck on the IBase case of this proof, which is that the theorem is false! Consider:

noplus532 : Plus 5 3 2 -> Void
noplus532 IBase impossible
noplus532 (IStep _) impossible

plus535 : Plus 5 3 (3 + 2)
plus535 = IBase