Типы отливок в 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.

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