1

我有定义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 vlSome 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
4

1 回答 1

2

你有两种方法，让我们先做一些准备工作：

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.

但是，上述方法都不会在证明方面给您带来很大的进步，因此真正的问题是您最初的目的是什么。

于 2016-10-14T01:00:02.840 回答