仕様が与えられたCoqの関数の一意性を証明する方法は？

Question

例えば、specification_of_sumのような関数の仕様が与えられた場合、そのような関数が1つだけ存在することを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. 

Answer 1

次の開始は、本質的です。

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が必要です。

Answer 2

誘導を使用してこれを証明する必要があります。nあなたの仕様が0とn.+1のケースをカバーしているので、誘導を使用するのは当然です。

誘導については、基本的にあなたが選んだCoqの本を読むことができます。

あなた仕様の使用方法の例は次のとおりです。ejgallegoは、すでに述べたよう

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].