如何證明Coq中的證明定義

我目前與Coq一起工作，遇到一個我不知道如何解決的問題。假設我們正在使用給定的類型，我將採用nat作爲示例，並且我想使用可能失敗的函數f。爲了彌補失敗，我們將f定義爲nat -> option nat。如何證明Coq中的證明定義

現在我有一個給定的假設下H: nat -> bool其中，f不會失敗，我甚至已經證明了引理

Lemma no_error_in_f : forall (n:nat), H n = true -> exists (u:nat), f n = Some u.

我要定義一個函數g: nat->nat賦予的f上n如果H n結果是滿意的，只是給予n否則。這個函數應該有明確的定義，但我不知道如何正確定義它。如果我嘗試像 Definition g (n:nat) := if H n then f n else n.這樣幼稚的東西，那麼在打字系統中就有問題了。

有誰知道如何收集所有元素並告訴系統該定義是合法的嗎？

來源

2016-01-23 tben

我在這裏給出一個與問題中給出的假設相同的假設。

Axiom f : nat -> option nat. 
Axiom H : nat -> bool. 
Axiom no_error_in_f : forall n, 
    H n = true -> exists u, f n = Some u. 

Lemma no_error_in_f_bis : forall n, 
    H n = true -> f n <> None. 
Proof. 
    intros. apply no_error_in_f in H0. destruct H0. rewrite H0. discriminate. 
Qed. 

Definition g n := 
    match H n as b return H n = b -> _ with 
    | true => fun H => 
    match f n as f0 return f n = f0 -> _ with 
    | Some n0 => fun _ => n0 
    | None => fun H0 => match no_error_in_f_bis n H H0 with end 
    end eq_refl 
    | false => fun _ => n 
    end eq_refl.

我用另一種比引理no_error_in_f，這樣更方便證明False。請注意，此功能的兩個想法（使用return結構match，破壞False的證明顯示分支不可達）在這裏解釋：http://adam.chlipala.net/cpdt/html/Subset.html。

來源

2016-01-24 14:30:16 eponier

您的開發中存在兩個問題。一種是你不能使用no_error_in_f在Coq中定義g而不假設其他公理，因爲Coq不允許從證明中提取計算信息（有關更多詳細信息，請檢查here）。另一個問題是，您不能在if表達式中使用H，因爲它返回Prop而不是bool（有關更多詳細信息，請檢查this answer）。

來源

2016-01-23 19:03:38

對不起，我犯了一個錯誤，第二個錯誤沒有出現，因爲'H n'是'bool'類型，我的引理的謂詞是'H n = true'。我會編輯這個。對於第一個問題，我想到了像False_rec之類的東西，或者類似的東西 – tben

我已經找到一種方法來做到這一點，這是我的解決方案，如果有人有興趣：

Definition g (n:nat) :nat := (match (H n) as a return a = H n -> nat with | true => (fun H_true => (match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) | false => n end) (eq_refl H n).

對於那些想知道這意味着什麼，False_rec採取的第二個參數中證明誰的錯誤並證明匹配是不可能的。術語

(match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) 具有類型f n = f n-> nat，當我將其應用到證明eq_refl (f n)（這是一個證明，F 2 N = F N，所以被鍵入f n = f n），I得到nat。這個技巧可以讓我獲得H1這是一個證明f n = None使用平等和模式匹配的reflexevity得到的證明，並且我要在我的證明中使用False。

其他比賽也一樣。

來源

2016-01-24 11:52:38 tben

我理解這個想法，但是您的解決方案不會按原樣進行類型檢查。你能糾正它，以便它與你提出的假設一致嗎？ – eponier

如何證明Coq中的證明定義

回答

相關問題