我想使用集合,为此尝试使用MSets库.但我需要将函数从一种类型的集合写入另一种类型的集合,并且它与Coq的模块系统交互不良.
这是我面临的一个问题的例子.我想要一套类型T和套T*T.我加入投影功能proj1和proj2从一组对,和功能的获得一组值add_l并add_r创建从一个值组对和一组值.
我实例化我的模块nat.我创建了一组nat并调用add_l,但Coq并不知道这一点SNat.t并且S.S1.t是相同的.在这里,我可以直接创建一组类型S.S1.t,但如果它必须与更复杂的环境进行交互将会更加困难.
有可能让Coq理解SNat.t并且S.S1.t是一样的吗？或者我的问题有另一种解决方案吗？
Require Import MSets.
Module DecidablePair (DT1:DecidableType) (DT2:DecidableType) <: DecidableType.
Definition t : Type := DT1.t * DT2.t.
Definition eq x y := DT1.eq (fst x) (fst y) /\ DT2.eq (snd x) (snd y).
Lemma eq_equiv : Equivalence eq.
Proof.
split.
- split; reflexivity.
- split; symmetry; apply H.
- split.
+ transitivity (fst y). apply H. apply H0.
+ transitivity (snd y). apply H. apply H0.
Qed.
Lemma eq_dec : forall x y, {eq x y} + {~ eq x y}.
Proof.
intros.
destruct (DT1.eq_dec (fst x) (fst y)).
- destruct (DT2.eq_dec (snd x) (snd y)).
+ left. split; assumption.
+ right. intros contra. apply n. apply contra.
- right. intros contra. apply n. apply contra.
Qed.
End DecidablePair.
Module MakePair (DT1: DecidableType) (DT2:DecidableType) <: WSets.
Module S1 := MSetWeakList.Make DT1.
Module S2 := MSetWeakList.Make DT2.
Module DT := DecidablePair DT1 DT2.
Include MSetWeakList.Make DT.
Definition proj1 (s:t) := fold (fun x e => S1.add (fst x) e) s S1.empty.
Definition proj2 (s:t) := fold (fun x e => S2.add (snd x) e) s S2.empty.
Definition add_l (a:S1.elt) (s2:S2.t) := S2.fold (fun x e => add (a, x) e) s2 empty.
Definition add_r (s1:S1.t) (a:S2.elt) := S1.fold (fun x e => add (x, a) e) s1 empty.
End MakePair.
Module SNat := MSetWeakList.Make Nat_as_DT.
Module S := MakePair Nat_as_DT Nat_as_DT.
Definition s1 := SNat.add 0 (SNat.add 4 SNat.empty).
Definition s := S.add_l 1 s1.