types de coulée dans coq

Question

J'ai la définition 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. 

Je voudrais écrire une autre définition my_def2 similaire à my_def1 comme ci-dessous et ajoutez un axiome qui proj_bytes vl reviennent toujours Some bl, donc:

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

Ma question est comment puis-je remplir my_def2 et écrire le axiom à propos de proj_bytes vl?

Ou la question est de savoir comment puis-je jeter le type list memval-list byte [decode_int accepte list byte]?

Et voici la définition de memval:

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

Answer 1

Vous avez deux approches, permet de faire des préliminaires d'abord:

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. 

Ensuite, vous pouvez définir votre axiome:

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

Vous détruire cet axiome et réécrire avec le égalité intérieure. Cependant, cette approche est un peu intéressante, comme vous pouvez le deviner.

Il peut être préférable de faire semblant d'avoir une valeur par défaut pour détruire 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. 

Cependant, aucune des méthodes ci-dessus vous donnera de grands progrès dans la preuve, donc la vraie question est ce que votre original le but était.