以前に次のような問題を投稿しましたが、まだ解決策が見つかりません。レコード タイプ (5 つのメンバーを持つ) から文字列値へのストア (マッピング) があります。レコードの 3 つの要素を保護する関数を使用したフォールドで、マッピング (文字列から文字列へ) を返します。以下のgsc_MapsTo_iff_rightのようないくつかの補題を解決する必要があります。
私は Coq の専門家ではないので、コードには厄介な構文 (fold など) が含まれている可能性があります。そのために残念。
ご協力ありがとうございました。
ウィラヤット
Require String.
Record c_id : Type := build_c_id {
c_id_d : String.string;
c_id_p : String.string;
c_id_s : bool;
c_id_h : bool;
c_id_k : String.string
}.
Definition skey := String.string.
Definition st (elt:Type) := list (String.string * elt).
Variable elt : Type.
Parameter Sadd : skey -> String.string -> st String.string -> st String.string.
Parameter SMapsTo : skey -> String.string -> st String.string -> Prop.
Definition ckey := c_id.
Definition ct (e:Type) := list (ckey * elt).
Implicit Type cm: ct elt.
Parameter Cadd : ckey -> String.string -> ct String.string -> st String.string.
Parameter CMapsTo : ckey -> String.string -> ct String.string -> Prop.
Parameter elements : ct String.string -> list (ckey*String.string).
Fixpoint rec_fold {A : Type} (f: ckey -> String.string -> A -> A) (l : list (ckey * String.string)) (b: A) : A :=
match l with
| nil => b
| cons (k, v) t => f k v (rec_fold f t b)
end.
Fixpoint fold {A: Type} (f: ckey -> String.string -> A -> A)
(cm: ct String.string) (b:A) : A :=
rec_fold f (elements cm) b.
Parameter empty : st String.string.
Axiom str_dec : forall a b : String.string, {a = b} + {a <> b}.
Definition str_eqdec (a b: String.string):bool :=
if str_dec a b then true else false.
Notation "x =?= y" := (str_eqdec x y) (at level 30).
Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
Notation "x & y" := (andb x y) (at level 40).
Definition get_sc (d p: String.string) (ckm: ct String.string)
: st String.string :=
fold
(fun cki v zm => if d =?= cki.(c_id_d) &
p =?= cki.(c_id_p) &
(negb (cki.(c_id_s)))
then Sadd cki.(c_id_k) v zm
else zm )
ckm
empty.
Lemma gsc_MapsTo_iff_right:
forall p d zk zv zh cm,
CMapsTo (build_c_id d p false zh zk) zv cm ->
SMapsTo zk zv (get_sc d p cm).
Proof.
Admitted.