如何在"with“子句中使用Refl
如何在"with“子句中使用Refl
提问于 2021-08-16 09:00:19
我想证明一个关于数字均等的事实。
我从以下定义开始：
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 = Odd的元素。
我得到以下错误：
同时处理右手边的与块在test2中。无法解决以下之间的约束：
奇数和奇偶
我做错什么了吗？我可以在这个"with“分支中创建一个Refl吗？
是否可以使用这种技术，还是必须使用“重写”或定义另一个函数？
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-08-18 05:13:40
您需要bring in scope a proof that parity n = Odd，因为否则在模式匹配其结果之后，它与parity n的连接将丢失：
将依赖模式匹配用于定理证明，有时需要显式构造由模式匹配产生的证明。为此，您可以将
with子句与proof p联系起来，模式匹配生成的证据将位于范围内并命名为p。
所以在你的例子中，你可以这样做：
test2: (n: Nat) -> (parity (S n) = Even) -> Prop n
test2 n eq with (parity n) proof p
test2 n eq | Odd = FromPar p页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/68800006
复制相关文章
相似问题
腾讯云开发者
