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'塊重寫/解決？

回答

相關問題