Idris：如何在定义中使用'with'块重写/解决？

当我打开这个文件：Idris：如何在定义中使用'with'块重写/解决？

%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

我得到：

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

我下一步该做什么这不是明显对我。

如果我调用“让引理”功能（在Emacs），结果是什么，是无效的伊德里斯，即：

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

与n个例子= 5显示的东西我试图证明是非常正确的。

（在这个例子中的动机是我想定义依赖性类型的类型偶数和奇数自然数，即PNAT即使和PNAT奇）

来源

2017-04-12 Philip Dorrell

这是非常接近nat2PNat功能你已经定义过。只需在n上进行模式匹配并将with (nat2PNat n)添加到非零情况：

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

来源

2017-04-12 09:38:03

这对我来说确实有效。我发现最后一个'nat2PNat_Sn（S n）'不是必需的，可以省略。此外，我将假设“make lemma”生成有效的Idris代码的失败是一个错误，我将在Idris Github项目中提出这个问题，看看会发生什么。 –

如果你遗漏了'nat2PNat_Sn（S n）'，那么'nat2PNat_Sn'将不会是全部，这是你总是从样张中得到的。或者我误解了你？ –

安东，我确实希望自己的代码是完整的，但是我在顶部有一个“总计”，如果我的任何证明都不完整，应该已经发出抱怨。我的理解是，您可以在'|'的左侧写入初始函数表达式的重写版本如果'|'右边的匹配为您提供有关该表达的其他信息。但在这种情况下，它不会，所以没有任何好处（即我们已经知道它是'nat2PNat_Sn（S n）'，并且匹配'（nat2PNat n）'到'（p ** pn）'不会给我们任何有关'nat2PNat_Sn（S n）'的详细信息）。 –

Idris：如何在定义中使用'with'块重写/解决？

回答

相关问题