Idris: How do I rewrite/solve using a 'with' block in a definition?

Question

When I load this file:

%default total

data Parity = Even | Odd

opposite: Parity -> Parity
opposite Even = Odd
opposite Odd  = Even

data PNat : Parity -> Type where
     PZ : PNat Even
     PS : PNat p -> PNat $ opposite p

nat2PNat : Nat -> (p ** PNat p)
nat2PNat Z    = (Even ** PZ)
nat2PNat (S x) with (nat2PNat x)
     | (p1 ** px) = (opposite(p1) ** (PS px))

nat2PNat_5 : nat2PNat 5 = (Odd ** PS (PS (PS (PS (PS PZ)))))
nat2PNat_5 = Refl

nat2PNat_S5 : nat2PNat (S 5) = (opposite (fst (nat2PNat 5)) ** (PS (snd (nat2PNat 5))))
nat2PNat_S5 = Refl

nat2PNat_Sn : (n : Nat) -> nat2PNat (S n) = (opposite (fst (nat2PNat n)) ** (PS (snd (nat2PNat n))))
nat2PNat_Sn n = ?rhs

I get:

- + Main.rhs [P]
 `--         n : Nat
     ---------------------------------------------------------
      Main.rhs : with block in Main.nat2PNat (nat2PNat n) n =
     (opposite (fst (nat2PNat n)) ** PS (snd (nat2PNat n)))

It's not obvious to me what I should do next.

If I invoke the "Make lemma" function (in Emacs), the result is something that is not valid Idris, ie:

rhs : (n : Nat) -> with block in Main.nat2PNat (nat2PNat n) n = (opposite (fst (nat2PNat n)) ** PS (snd (nat2PNat n)))

The examples with n = 5 shows that the thing I'm attempting to prove is plausibly correct.

(The motivation for this example is I want to define dependently-typed types for even and odd natural numbers, ie PNat Even and PNat Odd.)

Anton Trunov Anton Trunov · Accepted Answer · 2017-04-12T09:38:03

It's very close to the nat2PNat function you've defined earlier. Just pattern-match on n and add with (nat2PNat n) to the non-zero case:

nat2PNat_Sn : (n : Nat) -> nat2PNat (S n) = (opposite (fst (nat2PNat n)) ** (PS (snd (nat2PNat n))))
nat2PNat_Sn Z = Refl
nat2PNat_Sn (S n) with (nat2PNat n)
  nat2PNat_Sn (S n) | (p ** pn) = Refl

Idris: How do I rewrite/solve using a 'with' block in a definition?

1 Answers