типы Кастинг в Coq

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. 

Однако ни один из вышеперечисленных способов не даст вам большие успехи в доказательстве, таким образом, реальный вопрос, является то, что оригинал цель был.