2

我以前发布过类似以下的问题，但尚未找到解决方案。我有一个从记录类型（有五个成员）到字符串值的存储（映射）。具有保护记录三个元素的函数并返回映射（字符串到字符串）的折叠。我需要解决一些引理，例如下面的gsc_MapsTo_iff_right。

由于我不是 Coq 专家，因此代码可能包含一些笨拙的语法（例如折叠）。对此感到抱歉。

谢谢您的帮助。

维拉亚特

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.
4

0 回答 0