Idris: proof that specific conditions are not possible

Question

Idris Version: 0.9.16

---

I am trying to describe constructs created from base value and step iteration:

 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 by describing the constructs from the iterated addition of the jump value:

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

A simple example of using 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 base not possible:

  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 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 fm = ?noJump_rhs 

That is: if n not base plus the natural multiple of jump , then neither one nor the other jump + n .

If I ask Idris about the breakdown of case m , he will only show me IBase - then I'm stuck.

Will 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

To Change 0: to enter the type, it needs a special qualifier:

 %elim data Iterate = <your definition> 

To the main question: it’s a pity that I did not read all of your code, I only want to make some suggestion for falsifying the evidence. From my experience (I even studied the standard library sources to find out some help), when you need to prove Not a ( a -> Void ), often you can use some Not b ( b -> Void ) and a way to convert a to b , then just pass it on to the second proof. For example, very simple evidence that one list cannot be a prefix of another if they have different heads:

 %elim data Prefix : List a -> List a -> Type where pEmpty : Prefix Nil ys pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys) prefixNotCons : Not (x = y) -> Not (Prefix (x :: xs) (y :: ys)) prefixNotCons r (pNext _) = r refl 

In your case, I suppose you need to combine some evidence.