Constructing proofs for a decision function in Idris

I am trying to create a decision function for a type representing two consecutive elements in a modular space.

(This code is derived from this excellent answer to a previous question of mine.)

data PreceedsN : Nat -> Nat -> Nat -> Type where
    PreceedsS : {auto prf : S a `LT` m} -> PreceedsN m a (S a)
    PreceedsZ : {auto prf : S a = m} -> PreceedsN m a Z

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S a `cmp` m)
    doesPreceedN (S a + S d) a b     | CmpLT d with (S a `decEq` b)
        doesPreceedN (S a + S d) a b | CmpLT d | Yes prf = Yes ?bIsSa
        doesPreceedN (S a + S d) a b | CmpLT d | No contra = No ?bNotSa
    doesPreceedN (S m) m b     | CmpEQ   with (b `decEq` 0)
        doesPreceedN (S m) m Z | CmpEQ | Yes prf = Yes PreceedsZ
        doesPreceedN (S m) m b | CmpEQ | No contra = No ?saIsmAndbIsNotZ
    doesPreceedN (S m) (m + (S d)) b | CmpGT d = No ?saCannotBeGTm

I've done my best, but I'm not knowledgable enough yet to construct the necessary proofs on my own, especially the proofs of contradiction. Could you walk me through how to fill one or more of the holes in the code above?

Also, if you use any handy tools, like absurd, impossible, or tactics, could you explain how they work and the part they play in the proof?

Solution

While the prfs in the PreceedsN-constructor needs a LTE proof (LT a b is just a synonym for LTE (S a) b), your first cmp just splits S a. Instead, you should directly get the LTE proof:

doesPreceedN m a b with (S (S a) `isLTE` m)

If you don't need to reuse all the variables, omitting the repetition in the with cases makes things a bit prettier. So to repeat your version with the LTE, we have:

  | (Yes lte) = case (decEq b (S a)) of
      Yes Refl => PreceedsS
      No notlte => No ?contra_notlte
  | (No notlte) with (decEq (S a) m)
    | Yes eq = case b of
      Z => Yes PreceedsZ
      (S b) => No ?contra_notZ
    | No noteq = No ?contra_noteq

In all these cases you need a to prove some a -> Void, so you can assume, you have that a. You can either create a lemma (your editor might have bindings for that) or use a lambda with a case split. For short functions like here, I favor the latter. For ?contra_notZ:

No (\contra => case contra of prec => ?contra_notZ)

If you split on prec, you'd have:

No (\contra => case contra of PreceedsS => ?contra_notZ)

Inspecting the hole, you'll see that you have:

notlte : LTE (S (S b)) m -> Void
prf : LTE (S (S b)) m

prf is the implicit argument of PreceedsS, so to get it in scope, you can match against it:

No (\contra => case contra of (PreceedsS {prf}) => notlte prf)

?contra_noteq can be solved similiary.

The lambda for ?contra_notlte:

No notlte => No (\contra => case contra of
  PreceedsS => ?contra_notlte_1
  PreceedsZ => ?contra_notlte_2)

Checking the types gives:

:t ?contra_notlte_1
notlte : (S a = S a) -> Void
:t ?contra_notlte_2
lte : LTE (S (S a)) m
prf : S a = m

?contra_notlte_2 is the trickiest, because you can't just apply notlte. But you can see that after lte : LTE (S m) m should be false, so we create a function for it:

notLTE : Not (LTE (S n) n)
notLTE LTEZero impossible
notLTE (LTESucc lte) = notLTE lte

Now we have:

PreceedsZ {prf} => notLTE ?contra_notlte_2
?contra_notlte_2 : LTE (S n) n

I tried to replace the hole with (rewrite prf in lte), but that didn't work, because the tactic didn't find the right property to rewrite. But we can be explicit about that:

PreceedsZ {prf} => notLTE (replace prf lte)

> Type mismatch between
        LTE (S (S a)) m
and
        P (S a)

So we set P explicitly by setting {P=(\x => LTE (S x) m)}.

The result:

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S (S a) `isLTE` m)
  | (Yes lte) = case (decEq b (S a)) of
    Yes Refl => Yes PreceedsS
    No notlte => No (\contra => case contra of
      PreceedsS => notlte Refl
      PreceedsZ {prf} => notLTE  (replace prf {P=(\x => LTE (S x) m)} lte))
  | (No notlte) with (decEq (S a) m)
    | Yes eq = case b of
      Z => Yes PreceedsZ
      (S b) => No (\contra => case contra of (PreceedsS {prf}) => notlte prf)
    | No noteq = No (\contra => case contra of 
        PreceedsS {prf} => notlte prf
        PreceedsZ {prf} => noteq prf)

replace : (x = y) -> P x -> P y just rewrites a part of a type. For example, with (n + m = m + n) we can replace the n + m part of Vect (n + m) a to Vect (m + n) a. Here P=\to_replace => Vect to_replace a, so P is just a function Type -> Type.

In doesPreceedN we needed to be explicit about P. Most of the time, rewrite … in … (a tactic) can find this P automatically and apply replace. replace on the other hand is just a simple function :printdef replace:

replace : (x = y) -> P x -> P y
replace Refl prf = prf