2

我想证明如果字符串映射 (key*value) 是 Equiv，那么字符串列表是相等的，或者将两个 Equiv 映射转换为相等的键值对字符串。

(**defined in FMapInterface*)
Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
         (forall k, In k m <-> In k m') /\
         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').

Definition t (elt:Set) := list (X.t * elt) (**defined in FMapWeakList *).

在我的例子中，Xt 和 elt 是 String.string（字符串映射）。

Definition StringMap_to_strlist (zm : t String.string) : String.string :=
   fold (fun k v z => (k ++ v) ::  z) zm "". 


Lemma test: forall m m, 
       Equiv m m -> StringMap_to_strlist m = StringMap_to_strlist m.

例如，对于两个 Equiv 字符串映射 m 和 m'，

 m    quiv   m'
 k1:v1       k1:v1
 k3:v1       k2:v2
 k2:v2       k3:v1

对应的列表可能是： k1++v1::k3++v1::k2++v2 and k1++v1::k2++v2::k3++v1不相等。

我想证明如果映射是 Equiv，那么字符串列表是相等的，或者将两个 Equiv 映射转换为相等的键值对字符串。就我而言，字符串中键值对的顺序并不重要，因此如果可能的话，对列表进行排序是可以的。对于地图，以下列表在我的情况下是可以接受的。

k1++v1::k2++v2::k3++v1 = k1++v1::k2++v2::k3++v1

我不知道如何将 Equiv（无序类型）字符串映射转换为相等的字符串。请有人帮助我

4

0 回答 0