嵌套∃和平等的簡化表述

Question

我碰到一個證明來了，我不能輕鬆地自動直到我把這個引理成伊莎貝爾的簡化器設置：

lemma ex_ex_eq_hint: 
    "(∃x. (∃xs ys. x = f xs ys ∧ P xs ys) ∧ Q x) ⟷ 
    (∃xs ys. Q (f xs ys) ∧ P xs ys)" 
    by auto 

現在我想知道：是否有一個很好的理由簡化器或古典推理器不能一般地自動執行這種簡化？有沒有更多的這個引理的一般形式，可以添加到默認的simpset來實現這一點？

Answer 1

在Isabelle2015中，簡化器知道許多規則來消除由等式確定的存在性約束變量。對於你的情況下，相關的有simp_thms(36-40)：

• (∃x. ?P) ⟷ ?P
• ∃x. x = ?t
• ∃x. ?t = x
• (∃x. x = ?t ∧ ?P x) ⟷ ?P ?t
• (∃x. ?t = x ∧ ?P x) ⟷ ?P ?t

此外，ex_simps(1-2)推existentials成合取如果一方不不是離子結合的變量：

• (∃x. ?P x ∧ ?Q) ⟷ (∃x. ?P x) ∧ ?Q
• (∃x. ?P ∧ ?Q x) ⟷ ?P ∧ (∃x. ?Q x)

在許多情況下，這些規則是足夠的，以消除存在量詞。然而，在你的情況下，還存在xs和ys之間的其他存在量詞。原則上，上述規則和ex_comm即(∃x y. ?P x y) ⟷ (∃y x. ?P x y)（以及op &的關聯性，無論如何都是默認的簡單規則）就足以通過重寫來證明您的引理。然而，人們必須將存在的從中拉出來，然後對量詞進行排列，使得x被綁定在最內層。在一般情況下，這些步驟都不是需要的。而且，交換性也受到伊莎貝爾的術語順序的限制，所以簡化器甚至可能不會採用這種方式。

因此，這個問題一般不能用一組有限的重寫規則來解決，因爲可能有任意多的量詞嵌套。然而，它可以通過一個簡化形式來解決，該簡單形式在存在量詞上觸發並且搜索量化的謂語詞以得到被綁定變量的平等。如果平等出現在可以消除存在的位置，那麼它必須在現場制定適當的重寫規則（轉換可能對此有用）。

但是，simproc應該確保它不會過多地干擾目標的結構。在你的例子中已經可以看到一些這樣的干擾。在左側，謂詞Q不在內部量詞的範圍內，但它在右側。

這意味着在所有情況下這種轉換是不可取的。例如，在左邊，auto,fastforce等所使用的古典推理可以歸入一個存在量詞，然後使用經典推理通過分析Q來找到x的實例。這可能導致進一步簡化等於x = f xs ys，這可能導致進一步的實例化。相反，在右側，推理者首先必須爲存在量詞引入兩個原理變量，然後才能開始查看Q。

總之，我建議你分析一下你的設置，看看爲什麼這種形式的量詞嵌套在目標狀態下完全發生。也許你可以對它進行調整，使得一切都可以與現有規則配合使用。