鑄造類型

Question

我的定義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. 

我還想寫另一個定義my_def2類似my_def1像下面添加一個公理proj_bytes vl總是返回Some bl，所以：

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

我的問題是我怎樣才能完成my_def2並編寫相關axiom約proj_bytes vl？

或者問題是我如何從類型list memval轉換爲list byte [decode_int接受list byte]

這裏是memval定義：

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

Answer 1

你有兩種做法，讓我們先要做一些準備工作：

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. 

然後，你可以定義你的公理：

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

你破壞了這個公理並用內心平等。但是，你可以猜測這種方法有點不方便。

這可能是最好假裝有一個默認值進行破壞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. 

然而，沒有上述方法會給你一個證明巨大的進步，因此，真正的問題是你的原目的是。