勒柯克：如何證明如果語句涉及字符串？

Question

我有一個string b和string a上比較，如果有平等的string c，否則有string x。我知道的假設fun x <= fun c。我如何證明以下陳述？ fun是一些函數，它發生在string並返回nat。

fun (if a == b then c else x) <= S (fun c) 

的邏輯似乎是顯而易見的，但我無法將拆分COQ的if語句。任何幫助，將不勝感激。

謝謝！

Answer 1

如果您可以編寫if-then-else語句，則表示測試表達式a == b處於帶有兩個構造函數（如bool）或（sumbool）的類型。我首先假設類型是bool。在這種情況下，證明過程中的最佳方法是輸入以下命令。

case_eq (a == b); intros hyp_ab. 

這會產生兩個目標。在第一個，你將有一個假設

hyp_ab : a == b = true 

斷言測試成功和目標的結論有以下形狀（IF-THEN-ELSE由然後分支代替）：

樂趣ç< = S（FUN C）

在第二個目標，你將有一個假設

hyp_ab : a == b = false 

並且目標結論具有以下形狀（if-then-else被替換爲其他分支）。

fun x <= S (fun c) 

你應該能夠從那裏繼續。

在另一方面，從勒柯克的String庫與返回類型{a = b}+{a <> b}功能string_dec。如果你的符號a == b是string_dec a b一個漂亮的符號，最好是使用以下策略：

destruct (a == b) as [hyp_ab | hyp_ab]. 

行爲將是非常接近到什麼上述我，只是更容易使用。

直觀地說，當你的原因上IF-THEN-ELSE聲明，您可以使用如下命令case_eq，destruct，或case導致您單獨學習兩次執行路徑，記得在一個假設你爲什麼把每個這些執行路徑。

Answer 2

讓我補充伊夫斯的回答，指出一個普遍的「視圖」模式，在許多情況下運作良好，需要進行案例分析。我將使用數學補償的內置支持，但該技術是不特定的。

假設您最初的目標：

From mathcomp Require Import all_ssreflect. 

Variables (T : eqType) (a b : T). 
Lemma u : (if a == b then 0 else 1) = 2. 
Proof. 

現在，你可以使用case_eq + simpl到達下一步驟;但是，您也可以使用更專業的「查看」引理來匹配。例如，你可以使用ifP：

ifP : forall (A : Type) (b : bool) (vT vF : A), 
     if_spec b vT vF (b = false) b (if b then vT else vF) 

其中if_spec是：

Inductive if_spec (A : Type) (b : bool) (vT vF : A) (not_b : Prop) : bool -> A -> Set := 
    IfSpecTrue : b -> if_spec b vT vF not_b true vT 
    | IfSpecFalse : not_b -> if_spec b vT vF not_b false vF 

這看起來有點混亂，最重要的一點是參數類型家庭bool -> A -> Set。第一個練習是「證明ifP引理！」。

事實上，如果我們在證明使用ifP，我們得到：

case: ifP. 
Goal 1: (a == b) = true -> 0 = 2 
Goal 2: (a == b) = false -> 1 = 2 

需要注意的是，我們沒有指定任何東西！的確，形式爲{ A } + { B }的引理只是這種視圖模式的特例。這個技巧適用於許多其他情況，例如，您也可以使用eqP，它有一個關於布爾等於和命題相關的規範。如果你這樣做：

case: eqP. 

你會得到：

Goal 1: a = b -> 0 = 2 
Goal 2: a <> b -> 1 = 2 

這是非常方便的。實際上，eqP基本上是type_dec原理的通用版本。