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
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.