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并编写有关proj_bytes vl__的相关axiom？

或者问题是我如何从list memval类型转换为list byte [__decode_int accepts 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.

然而，上述任何一种方法都不会给你很大的进步，因此真正的问题是你最初的目的是什么。