I wanted to use the sets and tried to use the MSets library for this. But I need to write functions from one type of set to another type of set, and it interacts poorly with the Coq module system.
Here is an example of the problem I am facing. I want to have sets of type T and sets of T*T I added the projection functions proj1 and proj2 to get a set of values from a set of pairs and the add_l and add_r functions to create a set of pairs from a value and a set of values.
I am instantiating a module using nat . I create a set of nat and call add_l , but Coq does not know that SNat.t and S.S1.t same. Here I could create a set of S.S1.t types S.S1.t , but it will be more difficult if it needs to interact with a more complex environment.
Is it possible to make Coq realize that SNat.t and S.S1.t same? Or is there another solution to my problem?
Require Import MSets. Module DecidablePair (DT1:DecidableType) (DT2:DecidableType) <: DecidableType. Definition t : Type := DT1.t * DT2.t. Definition eq xy := 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 xy, {eq xy} + {~ eq xy}. 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 xe => S1.add (fst x) e) s S1.empty. Definition proj2 (s:t) := fold (fun xe => S2.add (snd x) e) s S2.empty. Definition add_l (a:S1.elt) (s2:S2.t) := S2.fold (fun xe => add (a, x) e) s2 empty. Definition add_r (s1:S1.t) (a:S2.elt) := S1.fold (fun xe => 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.
source share