如何從FMapInterface.MapsTo獲取FMapInterface.In，反之亦然？

從手動FMapInterface.In定義爲：如何從FMapInterface.MapsTo獲取FMapInterface.In，反之亦然？

Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.

所以，我期待的是展開一個術語In k m會產生exists e, MapsTo k e m。

然而，在Coq的8.4pl4，鑑於這樣的：

______________________________________(1/1) 
In (elt:=t) k m

通過發出執行unfold產量

______________________________________(1/1) 
Raw.In0 t (this m)

一個Print M（其中M是所討論的模塊）我得到

Module M 
: Sig 
. 
. 
. 
    End 
:= (FMapAVL.Make ID)

我的解決方案是使用引理find_mapsto_iff和in_find_iff（來自FMapFacts），但看起來過於複雜。爲什麼不展開定義的工作？

來源

2014-12-03 Tiago Cogumbreiro

您確定初始In是FMapInterface.In？你可以設置打印全部或東西？ – Ptival 2014-12-04 00:36:51

事實上，它不是最初的FMapInterface.In。它是FMapAVL.Make的一個實例（注意'Print M'的輸出）。 – 2014-12-04 10:01:05

模塊FMapInterface（來自FMapAVL.Make獲得）的實例改變的In定義，所以該基本屬性在實例丟失。

取而代之，結果必須證明在FMapInterface的等級。解決方案是創建一個具有這兩個屬性的輔助模塊。

Require Coq.FSets.FMapFacts. 
Require Coq.FSets.FMapInterface. 

Module MapUtil (Import M:FMapInterface.WS). 
    Module F := FMapFacts.Facts M. 
    Import F. 
    Lemma mapsto_to_in: 
    forall elt k e m, 
    MapsTo (elt:=elt) k e m -> 
    In k m. 
    Proof. 
    intros. 
    unfold In. 
    exists e. 
    assumption. 
    Qed. 

    Lemma in_to_mapsto : forall (elt:Type) m x, 
    In x m -> exists (e:elt), MapsTo x e m. 
    Proof. 
    intros. 
    unfold In in H. 
    assumption. 
    Qed. 
End MapUtil.

使用上述模塊如下使用Coq.FSets.FMapFacts的相同的模式。例如：

Require Import Coq.Structures.OrderedTypeEx. (* Imports: Nat_as_OT *) 
Require Import Coq.FSets.FMapAVL.   (* Imports: FMapAVL.Make *) 
Module Map_Nat := FMapAVL.Make Nat_as_OT. (* Defines a map with nats as keys. *) 
Module Map_Nat_Util := MapUtil Map_Nat.  (* Defines an instance of module MapUtil. *)

來源

2014-12-04 10:12:00

如何從FMapInterface.MapsTo獲取FMapInterface.In，反之亦然？

回答

相關問題