The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

Dear friends,

I have an old project (large one) in which I have a few functions, their specifications, and their correctness theorem along with their correctness proofs. Now I have redefined some of the functions and even input-output types. Although my new input types have changed, but the actual values and computations are the same. It's the types at each input instance that have changed (not their actual values and computations) and old functions are replaced with more efficient versions now (See a minimum example below.).

Now I want to restate some of the theorems in terms of new input-output types and functions. The goal is to do this with a minimum amount of new proofs or minimum efforts by using old functions and their correctness proofs.  

Basically, I want to show a bijection between the outputs of new and old programs and then want to use it to show the correctness of the theorems without redoing the old work again (which means using the old work as a black box). Please suggest some ideas.

Have a great day.

- Suneel

--------------------------------

(* Old input type *)

Record r_old:Type:= Mk_r{
                        a:> nat;
                        b: nat;
                        }.

(* Current input type is *)

Record r_new:Type:= Mk_r{
                        c: nat;
                        d: nat;
                        }.

(* I have a = c and b = d. *)

(* Old function *)

Definition f_old (B: list r_old): (list r_old):= f_old ( Sort_old a_dec B).

(* New function *)

Definition f_new (B: list r_old): (list r_new):= f_new ( Sort_new c_dec B).

(* Note: 

    Sort_new is more efficient than Sort_old. 

    The elements of B are all unique.

    f_new and f_old are the "same" programs in the sense that they do exactly the same calculations. Also is there any way to avoid writing f_new?*)