有沒有一種很好的方法來阻止自動發生在目標中的beta減少？

Question

假設您想證明(fun (x : unit) => false) <> (fun (x : unit) => true)。證明這一點的明顯方法是將intro一些H : (fun _ : unit => false) = (fun _ : unit => true)和使用H進行重寫以證明false = (fun x => false) tt = (fun x => true) tt = true)。但是，如果您嘗試這樣做，Coq會自動降低測試版本，您將不再有(fun x => false)和(fun x => true)作爲可以用H重寫的子項。

我得到解決這類問題的方法是定義類似app{X Y}(f : X -> Y)(x : X) := f x，然後使用app來阻止測試版的縮減。然而，這感覺有點冒險，所以我想知道是否有更好的方法來避免這些問題。

Answer 1

我不知道是否有以避免此類問題

勒柯克盲目β在許多情況下減少了更好的方式，有沒有什麼好辦法來告訴它不要。 （更糟糕的是，在我看來，Coq認爲它總是可以ζ-減少，如果你使用很多let s，這可能會導致在定義時間爆發指數。）

我用來隱藏β- redexes比你的要輕一些;她在標準庫中有id : forall {A}, A -> A，因此當我想阻止β減少時，我通常只是將我的λ包裝在id中。

更多重量級的解決方案是使用像RTac這樣的反射自動化技術，原則上可以讓您更細緻地控制，或者自己推出OCaml策略庫（或您自己的rewrite），它不會盲目它不會觸及的子項中的β減少。

一個不同重量級的解決方案是在錯誤跟蹤器上打開一個錯誤，rewrite不應該在它不會觸及的子項中進行β減少，並獲得Coq開發人員爲您解決問題。