How to use Refl in a "with" clause

user_12243262 0
Viewed 37

I want to prove a fact about the parity of numbers.

I started out with the following definition:

data Parity = Even | Odd 

revParity : Parity -> Parity
revParity Even = Odd
revParity Odd = Even

parity : Nat -> Parity
parity Z = Even -- zero is even
parity (S p) = revParity $ parity p -- inverse parity

In a lot of cases, i figured out it was simpler to pattern match on the parity, using the "with" syntax. For example:

test: (n:Nat) -> (parity (S n) = Even) -> (parity n = Odd)
test n eq with (parity n)
  test n eq | Odd = Refl
  test n eq | Even impossible

But then, I try something very similar :

data Prop: Nat -> Type where
  FromPar: {n: Nat} -> (parity n = Odd) -> Prop n

test2: (n: Nat) -> (parity (S n) = Even) -> Prop n
test2 n eq with (parity n)
  test2 n eq | Odd = FromPar Refl

I know that in the branch the types of parity n and Odd are the same, but I can't create an element of type parity n = Odd.

I get the following error:

While processing right hand side of with block in test2. Can't solve constraint between:
Odd and parity n.

Is there something I am doing wrong ? Can I create a Refl in this "with" branch ?

Is it possible to use this technique or do I have to use "rewrite" or define another function instead ?

idris with-statement equality types
1 Answers

You need to bring in scope a proof that parity n = Odd, because otherwise after you pattern match on its result, its connection to parity n is lost:

To use a dependent pattern match for theorem proving, it is sometimes necessary to explicitly construct the proof resulting from the pattern match. To do this, you can postfix the with clause with proof p and the proof generated by the pattern match will be in scope and named p.

So in your case, you can do this:

test2: (n: Nat) -> (parity (S n) = Even) -> Prop n
test2 n eq with (parity n) proof p
  test2 n eq | Odd = FromPar p
user_4774760
Related