How to prove uniqueness of a function in Coq given a specification?

0
votes

Given a specification of a function, e.g., specification_of_sum, how do I prove in Coq that only one such function exists?

I am studying mathematics, and I could prove this in hand, but my skills in Coq are limited (proving using rewrite and apply).

I found the code snippet below, which I've been struggling with for some time now.

I try to unfold the specification in the proof, but using my old friend rewrite doesn't seem to let me go further.

Can someone explain how to approach this problem using simple syntax?

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.
2
functional-programmingcoq

2 Answers

1
votes

You need to prove this using induction on n. Think of it, your specification covers the cases for 0 and n.+1, thus it is natural to use induction.

You can read about induction in basically the Coq book of your choice.

An example on how to use your specification is:

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

The following start is essentially as ejgallego already described.

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 *)

I have included a few more basic commands to make it slower but simpler. The rest of the proof only requires rewrite and reflexivity.