The Coq mailing list

["D. Ben Knoble" <ben.knoble AT gmail.com>]

I should think that, given some relation R between old and new input
(say, a = c, b = d, as in your code), you could prove "forall x y, R x
y -> f_old x = f_new y". Then in your proofs, you could rewrite "f_new
y" to "f_old x", and your goals would be (1) similar to the "old"
goal(s) and (2) "R x y".

Note that the details might be a little subtle since your functions
consume lists of the input type (so you would probably need something
like "Forall R xs ys" as a hypothesis).

On Mon, Jul 24, 2023 at 7:54 AM Suneel Sarswat <suneel.sarswat AT gmail.com> 
wrote:
>
> 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?*)
>


-- 
D. Ben Knoble