證明一系列步驟終止

我有一個可以重寫lambda術語的小系統。它具有通常的（三個）確定性按值重寫規則。我沒有在這裏列出。證明一系列步驟終止

重寫模擬爲Step從一個Term到另一個。我也有可達項之間的關係，其中後者可以由第一個零或更多重寫步驟產生。

我現在想表明重寫終止（帶有值或卡住）。我已經刪除了細節，因爲我不認爲他們在這裏重要，但如果需要，我可以添加更多細節。

這裏是（在瀏覽器中或here CollaCoq）代碼：

Variable Term: Type. 
Variable Step: Term -> Term -> Prop. 
Inductive StarStep: Term -> Term -> Prop := 
| StepNone : forall t, StarStep t t 
| StepOne : forall t t', Step t t' -> forall t'', StarStep t' t'' -> StarStep t t''. 

Goal forall t : Term, 
    ~ (forall t', StarStep t t' -> exists t'', Step t' t'') -> 
    exists t', StarStep t t' /\ forall t'', ~ Step t' t''.

所以，我想告訴

如果不是那「從所有到達的情況下，說明有可能又一步「那麼存在可從t 到達的狀態t'，使得它是不可能從中走出來的。

我被困在如何繼續。我是否需要更多的信息，例如誘導或破壞（=個案分析）t？當它被否定時，我該如何使用假設中的信息？

編輯：Here are more details about Term and Step

來源

2016-12-15 larsr

注意，您可以'評論「PKGS：COQ-雷亞爾」 .'你collacoq文件的開頭，它將讓你不加載更多勒柯克庫必須重新實現字符串。 – ejgallego

我相信這是經典推理的一個實例。聲明類似於下面的命題，這是不是在建設性的設置可證：

Goal forall (A : Type) (P : A -> Prop), 
    ~ (forall x, P x) -> exists x, ~ P x.

，因爲知識，「這是不正確的，FORALL ...」不會產生一個對象，你需要證明一些東西的存在。

下面是使用經典邏輯的法律可能的解決方案：

Require Import Coq.Logic.Classical_Pred_Type. 
Require Import Coq.Logic.Classical_Prop. 

Goal forall t : Term, 
    ~ (forall t', StarStep t t' -> exists t'', Step t' t'') -> 
    exists t', StarStep t t' /\ forall t'', ~ Step t' t''. 
Proof. 
    intros t H. 
    apply not_all_ex_not in H. 
    destruct H as [tt H]. 
    apply imply_to_and in H. 
    firstorder. 
Qed.

事實上，我們甚至不需要知道StarStep什麼，因爲以前的命題以下抽象的版本是經典有效邏輯（證明保持不變）：

Goal forall (A : Type) (P Q : A -> Prop), 
    ~ (forall s, Q s -> exists t, P t) -> 
    exists s, Q s /\ forall t, ~ P t.

來源

2016-12-15 13:27:27

證明一系列步驟終止

回答

相關問題