types - 如何在 "with"子句中使用 Refl

Question

我想证明一个关于数的奇偶性的事实。

我从以下定义开始:

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

在很多情况下，我发现使用“with”语法在奇偶校验上进行模式匹配更简单。例如:

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

但是，我尝试了一些非常相似的东西:

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

我知道在分支中 parity n 和 Odd 的类型是相同的，但我无法创建 parity n = 类型的元素奇数。

我收到以下错误:

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

我做错了什么吗？我可以在这个“with”分支中创建一个 Refl 吗？

是否可以使用这种技术，或者我是否必须使用“重写”或定义另一个函数来代替？

Answer 1

您需要bring in scope a proof that parity n = Odd ，因为否则在您对其结果进行模式匹配后，它与 parity n 的连接将丢失:

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

所以在你的情况下，你可以这样做:

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