如何HOLCF證明清單的雙重逆轉並沒有改變它

Question

下面是一個簡單的理論寫在普通HOL：

theory ToyList 
    imports Main 
begin 

no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) 
hide_type list 
hide_const rev 

datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) 

primrec snoc :: "'a list => 'a => 'a list" (infixr "#>" 65) 
    where 
    "[] #> y = y # []" | 
    "(x # xs) #> y = x # (xs #> y)" 

primrec rev :: "'a list => 'a list" 
    where 
    "rev [] = []" | 
    "rev (x # xs) = (rev xs) #> x" 

lemma rev_snoc [simp]: "rev(xs #> y) = y # (rev xs)" 
    apply(induct_tac xs) 
    apply(auto) 
done 

theorem rev_rev [simp]: "rev(rev xs) = xs" 
    apply(induct_tac xs) 
    apply(auto) 
done 

end 

snoc是cons相反。它將一個項目添加到列表的末尾。

我想通過HOLCF證明類似的引理。在第一階段，我只考慮嚴格的名單。我在HOLCF中聲明瞭嚴格的列表域。此外，我聲明瞭兩個遞歸函數：

• ssnoc - 追加到一個列表
• srev結束的項目 - 反轉列表

前綴s的意思是 「嚴格」。

theory Test 
    imports HOLCF 
begin 

domain 'a SList = SNil | SCons "'a" "'a SList" 

fixrec ssnoc :: "'a SList → 'a → 'a SList" 
    where 
    "ssnoc ⋅ SNil ⋅ x = SCons ⋅ x ⋅ SNil" | 
    "ssnoc ⋅ ⊥ ⋅ x = ⊥" | 
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ ssnoc ⋅ (SCons ⋅ x ⋅ xs) ⋅ y = SCons ⋅ x ⋅ (ssnoc ⋅ xs ⋅ y)" 

fixrec srev :: "'a SList → 'a SList" 
    where 
    "srev ⋅ ⊥ = ⊥" | 
    "srev ⋅ SNil = SNil" | 
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ srev ⋅ (SCons ⋅ x ⋅ xs) = ssnoc ⋅ (srev ⋅ xs) ⋅ x" 

lemma srev_singleton [simp]: 
    "srev ⋅ (SCons ⋅ a ⋅ SNil) = SCons ⋅ a ⋅ SNil" 
    apply(induct) 
    apply(simp_all) 
done 

lemma srev_ssnoc [simp]: 
    "srev ⋅ (ssnoc ⋅ xs ⋅ a) = SCons ⋅ a ⋅ (srev ⋅ xs)" 
    apply(induct xs) 
    apply(simp_all) 
done 

lemma srev_srev [simp]: 
    "srev ⋅ (srev ⋅ xs) = xs" 
    apply(induct xs) 
    apply(simp_all) 
done 

end 

我想證明列表的那個雙逆轉等於原始列表（srev_srev引理）。我宣佈兩個輔助引理：

• srev_singleton - 單身名單的反向是原單列表
• srev_ssnoc - 列表的逆轉等於從原來的名單追加逆轉的最後一個項目啓動列表原列表的其餘項目

但我不能證明任何引理。你能指出錯誤嗎？

爲什麼在函數定義中必須使用前提"x ≠ ⊥ ∧ xs ≠ ⊥"？我爲什麼要明確聲明"srev ⋅ ⊥ = ⊥"和"ssnoc ⋅ ⊥ ⋅ x = ⊥"。我想在HOLCF默認情況下，如果任何參數未定義，函數都是未定義的。

Answer 1

如果你的目的是要示範清單一拉哈斯克爾（又名「懶名單」），那麼你應該使用類似：

domain 'a list = Nil ("[]") | Cons (lazy 'a) (lazy "'a list") (infix ":" 65) 

（注意是「懶」的註釋Cons）。那麼你不需要你的第三個等式的假設。例如，

fixrec append :: "'a list → 'a list → 'a list" 
    where 
    "append $ [] $ ys = ys" 
    | "append $ (x : xs) $ ys = x : (append $ xs $ ys)" 

你叫什麼ssnoc和

fixrec reverse :: "'a list → 'a list" 
    where 
    "reverse $ [] = []" 
    | "reverse $ (x : xs) = append $ xs $ (x : [])" 

反向。

但是，由於這種類型的列表允許「無限」值，因此您將無法證明reverse $ (reverse $ xs) = xs通常保持不變（因爲它不）。這隻適用於有限清單，可以用歸納法來表徵。 （例如，請參閱https://arxiv.org/abs/1306.1340以獲得更詳細的討論。）

但是，如果您不想爲懶惰列表建模（即，實際上不希望數據類型中的「懶惰」註釋），那麼您的方程如果沒有這些假設，可能就不會成立現在如果方程式有這些假設，它們只能用於滿足假設的情況。所以獲得，你將無法證明（沒有額外的假設）reverse $ (reverse $ xs) = xs。也許有可能通過歸納謂詞獲得適當的假設，但我沒有進一步調查。

更新：在HOLCF打了一下，有嚴格的名單後，我有一些更多的評論：

首先，我的猜測是，在fixrec規範的前提條件是必要的，因爲在內部結構，但我們之後能夠擺脫它們。

我設法證明你的引理如下。爲了完整起見，我給出了我的理論文件的全部內容。首先確保符號不與現有的衝突：

no_notation 
    List.Nil ("[]") and 
    Set.member ("op :") and 
    Set.member ("(_/ : _)" [51, 51] 50) 

然後定義嚴格的名單

domain 'a list = Nil ("[]") | Cons 'a "'a list" (infixr ":" 65) 

和功能snoc類型。

fixrec snoc :: "'a list → 'a → 'a list" 
    where 
    "snoc $ [] $ y = y : []" 
    | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ snoc $ (x:xs) $ y = x : snoc $ xs $ y" 

現在，我們得到第二方程無條件變種：

1. 顯示該snoc是在其第一個參數嚴格（注意fixrec_simp使用）。
2. 顯示snoc在其第二個參數（這裏需要歸納）中是嚴格的。
3. 最後，通過所有三個變量的案例分析獲得方程。

lemma snoc_bot1 [simp]: "snoc $ ⊥ $ y = ⊥" by fixrec_simp 
lemma snoc_bot2 [simp]: "snoc $ xs $ ⊥ = ⊥" by (induct xs) simp_all 
lemma snoc_Cons [simp]: "snoc $ (x:xs) $ y = x : snoc $ xs $ y" 
    by (cases "x = ⊥"; cases "xs = ⊥"; cases "y = ⊥";simp) 

然後函數reverse

fixrec reverse :: "'a list → 'a list" 
    where 
    "reverse $ [] = []" 
    | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ reverse $ (x : xs) = snoc $ (reverse $ xs) $ x" 

，再第二次方程無條件變種：

lemma reverse_bot [simp]: "reverse $ ⊥ = ⊥" by fixrec_simp 
lemma reverse_Cons [simp]: "reverse $ (x : xs) = snoc $ (reverse $ xs) $ x" 
    by (cases "x = ⊥"; cases "xs = ⊥"; simp) 

現在引理約reverse和snoc你也有：

lemma reverse_snoc [simp]: "reverse $ (snoc $ xs $ y) = y : reverse $ xs" 
    by (induct xs) simp_all 

最後所需的引理：

lemma reverse_reverse [simp]: 
    "reverse $ (reverse $ xs) = xs" 
    by (induct xs) simp_all 

我得到這個解決方案是由剛剛尋找到你的失敗嘗試的其餘子目標的方式，然後獲得更多的失敗嘗試，看看其餘子目標，重複，...