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_def1proj_bytes vlSome bl

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

私の質問は、関連する情報をどのように完成させmy_def2て書くことができますか?axiomproj_bytes vl

list memvalまたは、タイプから list byte[ decode_intaccepts list byte]にキャストするにはどうすればよいですか?

の定義は次のmemvalとおりです。

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

1 に答える 1

2

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 に答える