Casting types in coq

Question

I have the definition my_def1:

Require Import compcert.common.Memory.
Require Import compcert.common.Values.
Require Import compcert.lib.Integers.  

Definition my_def1 (vl: list memval) : val :=
 match proj_bytes vl with
    | Some bl => Vint(Int.sign_ext 16 (Int.repr (decode_int bl)))
    | None => Vundef
 end.

I would like to write another definition my_def2 similar to my_def1 like below and add an axiom that proj_bytes vl always return Some bl, So:

Definition my_def2 (vl: list memval) : val :=
   Vint(Int.sign_ext 16 (Int.repr (decode_int ((*?*)) )))
end.

My question is how can I complete my_def2 and write the related axiom about proj_bytes vl?

Or the question is how can I cast from the type list memval to list byte [decode_int accepts list byte]?

And here is the definition for memval:

Inductive memval : Type :=
  Undef : memval
 | Byte : byte -> memval
 | Fragment : val -> quantity -> nat -> memval

Answer 1

You have two approaches, lets do some preliminaries first:

Variable (memval byte : Type).
Variable (proj_bytes : list memval -> option byte).

Inductive val := Vundef | VInt : byte -> val.

Definition my_def1 (vl: list memval) : val :=
 match proj_bytes vl with
    | Some bl => VInt bl
    | None    => Vundef
 end.

Then, you could define your axiom as:

Axiom pb1 : forall vl , { v | proj_bytes vl = Some v }.

You destruct this axiom and rewrite with the inner equality. However, this approach is a bit incovenient as you can guess.

It may be better to pretend to have a default value to destruct proj_bytes:

Variable (byte_def : byte).

Definition bsel vl :=
  match proj_bytes vl with
  | Some bl => bl
  | None    => byte_def
  end.

Definition my_def2 (vl: list memval) : val := VInt (bsel vl).

Lemma my_defP vl : my_def1 vl = my_def2 vl.
Proof.
now destruct (pb1 vl) as [b H]; unfold my_def1, my_def2, bsel; rewrite H.
Qed.

However, none of the above methods will give you great advances in a proof, thus the real question is what your original purpose was.