如何在給定規範的Coq中證明函數的唯一性？

給定一個函數的規範，例如specification_of_sum，我如何在Coq中證明只有一個這樣的函數存在？如何在給定規範的Coq中證明函數的唯一性？

我正在學習數學，我可以證明這一點，但我的Coq技能是有限的（使用rewrite和apply證明）。

我發現下面的代碼片段，我一直在努力一段時間。

我嘗試展開證明中的規範，但使用我的老朋友rewrite似乎沒有讓我走得更遠。

有人可以解釋如何使用簡單的語法來解決這個問題嗎？

Definition specification_of_sum (sum : (nat -> nat) -> nat -> nat) := 
    forall f : nat -> nat, 
    sum f 0 = f 0 
    /\ 
    forall n' : nat, 
     sum f (S n') = sum f n' + f (S n'). 

(* ********** *) 

Theorem there_is_only_one_sum : 
    forall sum1 sum2 : (nat -> nat) -> nat -> nat, 
    specification_of_sum sum1 -> 
    specification_of_sum sum2 -> 
    forall (f : nat -> nat) 
      (n : nat), 
     sum1 f n = sum2 f n. 
Proof. 
Abort.

來源

2016-11-17 Shuzheng

下面開始基本上如ejgallego已經描述。

intros sum1 sum2 H1 H2 f n. (* introduce all the hypotheses *)          
unfold specification_of_sum in *. (* unfold definition in all places *)        
specialize H1 with (f := f). (* narrow statement to be about f *)         
specialize H2 with (f := f). (* narrow statement to be about f *)         
inversion_clear H1. (* split up the AND statements *)            
inversion_clear H2.                     
(* induction on n, and do rewrites *)

我已經包含了一些更基本的命令，使它更慢但更簡單。其餘的證明只需要rewrite和reflexivity。

來源

2016-11-18 02:27:47

謝謝，這是需要啓動我的證明:-) – Shuzheng

是否有可能用「簡單」的東西替代inversion_clear？ – Shuzheng

事實上，倒置清晰並不是處理假設的正確方法，您在我的答案中使用了正確的方式（介紹模式）。 – ejgallego

您需要在n上使用感應來證明這一點。想一想，你的規範涵蓋了0和n.+1的情況，因此使用歸納法是很自然的。

你可以閱讀關於感應的基本上你所選擇的Coq書籍。

如何使用您的具體的一個例子是：

intros sum1 sum2 s1_spec s2_spec f n. 
specialize (s1_spec f) as [s1_spec0 s1_specS]. 
specialize (s2_spec f) as [s2_spec0 s2_specS].

來源

2016-11-17 18:21:32 ejgallego

但我找不到使用該規範的語法。我如何重寫或應用它？能給我看看麼？ – Shuzheng

我建議你使用'specialize（spec1 f）'，其中'spec1'是'sum1'的規範。您也可以在spec1中展開'specification_of_sum'，但這不是必需的，定義通常會在Coq中自動擴展。 – ejgallego

你會舉一個例子嗎？我不斷收到錯誤。 – Shuzheng

如何在給定規範的Coq中證明函數的唯一性？

回答

相關問題