Как доказать единственность функции в Coq при задании спецификации?

Question

Учитывая спецификацию функции, например, specification_of_sum, как доказать в 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

Следующая начало, по существу, как 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.

Answer 2

Вам необходимо доказать это, используя индукцию по адресу 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].