我想证明一个关于数的奇偶性的事实。
我从以下定义开始:
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 吗?
是否可以使用这种技术,或者我是否必须使用“重写”或定义另一个函数来代替?
最佳答案
您需要bring in scope a proof that parity n = Odd
,因为否则在您对其结果进行模式匹配后,它与 parity n
的连接将丢失:
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 withproof p
and the proof generated by the pattern match will be in scope and namedp
.
所以在你的情况下,你可以这样做:
test2: (n: Nat) -> (parity (S n) = Even) -> Prop n
test2 n eq with (parity n) proof p
test2 n eq | Odd = FromPar p
关于types - 如何在 "with"子句中使用 Refl,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/68800006/