The Coq mailing list

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

Dear Mukesh,

Thanks again for this suggestion. I would try to avoid this axiom presently.

Regards,

Suneel

On Mon, Jul 24, 2023 at 11:57 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

No worries. Also, if you don't mind functional extensionality [1], then you can prove: Theorem same_f_old_new : f_new  = fun r => List.map f (f_old r)  and use it to replace f_new (it will make rewrite a bit easier).

Best,

Mukesh

 

[1] https://coq.inria.fr/library/Coq.Logic.FunctionalExtensionality.html

On Mon, Jul 24, 2023 at 6:52 PM Suneel Sarswat <suneel.sarswat AT gmail.com> wrote:

Dear Mukesh,

Thanks a lot for this answer. This is natural and I am feeling bad about my laziness. 

Also thanks for the last two theorems, this will be anyway needed.  

Have a great day.

Regards,

Suneel

On Mon, Jul 24, 2023 at 10:34 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi Suneel,

I am not sure if it's exactly going to help in your case but you can prove a lemma like this:

 Theorem same_f_old_new : forall (r : list r_old), f_new r = List.map f (f_old r).
 
And use it to replace (f_new r) with (List.map f (f_old r), and hopefully, after this you can use the theorems related to f_old.  (I must confess that I don't understand coercions (:>) very well so it is quite possible that there might be an easier solution, or this one may not work).

Best,
Mukesh

Require Import List.

Section Rec.

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

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

  Definition f (u : r_old) : r_new :=
    match u as _ return r_new with
    | mk_old a b => mk_new a b 
    end.

  Definition g (u : r_new) : r_old :=
  match u as _ return r_old with
  | mk_new a b => mk_old a b
  end.

  (* This might come handy *) 
  Theorem first : forall (r : r_old), g (f r) = r.
  Proof.
    intro r.
    refine match r with 
    | mk_old a b => eq_refl 
    end.
  Qed.
  
  Theorem second : forall (r : r_new), f (g r) = r.
  Proof.
    intro r.
    refine match r with 
    | mk_new a b => eq_refl 
    end.
  Qed.
(* end of handy theorems *)


  (* Your definition of f_old *)
  Definition f_old (B: list r_old) : (list r_old).
  Admitted.

  (* Your definition of f_new *)
  Definition f_new (B: list r_old): (list r_new).
  Admitted.


  Theorem same_fold_new_old : forall (r : list r_old), f_new r = List.map f (f_old r).
  Proof.
  Admitted.

  (* I don't think you need this but we never know :) *)

  Theorem same_fold_old_new : forall (r : list r_old), f_old r = List.map g (f_new r).
  Proof.
  Admitted.

End Rec.

On Mon, Jul 24, 2023 at 12:54 PM 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?*)