| This module implements bridges (as functors) from dependent to/from non-dependent set signature. |
Require Export FSetInterface.
Set Implicit Arguments.
Set Ground Depth 2.
From non-dependent signature
|
Module DepOfNodep [M:S] <: Sdep with Module E := M.E.
Import M.
Module ME := MoreOrderedType E.
Definition empty: { s:t | Empty s }.
Definition is_empty: (s:t){ Empty s }+{ ~(Empty s) }.
Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.
Definition add : (x:elt) (s:t){ s':t | (Add x s s') }.
Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.
Definition remove : (x:elt)(s:t)
{ s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.
Definition union : (s,s':t)
{ s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.
Definition inter : (s,s':t)
{ s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.
Definition diff : (s,s':t)
{ s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.
Definition equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
Definition subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }.
Definition fold :
(A:Set)(f:elt->A->A)(s:t)(i:A)
{ r : A | (EX l:(list elt) |
(Unique E.eq l) /\
((x:elt)(In x s)<->(InList E.eq x l)) /\
r = (fold_right f i l)) }.
Definition cardinal :
(s:t) { r : nat | (EX l:(list elt) |
(Unique E.eq l) /\
((x:elt)(In x s)<->(InList E.eq x l)) /\
r = (length l)) }.
Definition fdec :=
[P:elt->Prop; Pdec:(x:elt){P x}+{~(P x)}; x:elt]
if (Pdec x) then [_]true else [_]false.
Lemma compat_P_aux :
(P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(compat_P E.eq P) ->
(compat_bool E.eq (fdec Pdec)).
Hints Resolve compat_P_aux.
Definition filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
{ s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.
Definition for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
{ (compat_P E.eq P) -> (For_all P s) } +
{ (compat_P E.eq P) -> ~(For_all P s) }.
Definition exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
{ (compat_P E.eq P) -> (Exists P s) } +
{ (compat_P E.eq P) -> ~(Exists P s) }.
Definition partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
{ partition : t*t |
let (s1,s2) = partition in
(compat_P E.eq P) ->
((For_all P s1) /\
(For_all ([x]~(P x)) s2) /\
(x:elt)(In x s)<->((In x s1)\/(In x s2))) }.
Definition choose : (s:t) {x:elt | (In x s)} + { Empty s }.
Definition elements :
(s:t){ l:(list elt) | (sort E.lt l)/\(x:elt)(In x s)<->(InList E.eq x l)}.
Definition min_elt :
(s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.
Definition max_elt :
(s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.
Definition elt := elt.
Definition t := t.
Definition In := In.
Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
Definition Empty := [s](a:elt)~(In a s).
Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
Definition eq_In := In_1.
Definition eq := eq.
Definition lt := lt.
Definition eq_refl := eq_refl.
Definition eq_sym := eq_sym.
Definition eq_trans := eq_trans.
Definition lt_trans := lt_trans.
Definition lt_not_eq := lt_not_eq.
Definition compare := compare.
End DepOfNodep.
From dependent signature
|
Module NodepOfDep [M:Sdep] <: S with Module E := M.E.
Import M.
Module ME := MoreOrderedType E.
Definition empty : t := let (s,_) = M.empty in s.
Lemma empty_1 : (Empty empty).
Definition is_empty : t -> bool :=
[s:t]if (M.is_empty s) then [_]true else [_]false.
Lemma is_empty_1 : (s:t)(Empty s) -> (is_empty s)=true.
Lemma is_empty_2 : (s:t)(is_empty s)=true -> (Empty s).
Definition mem : elt -> t -> bool :=
[x:elt][s:t]if (M.mem x s) then [_]true else [_]false.
Lemma mem_1 : (s:t)(x:elt)(In x s) -> (mem x s)=true.
Lemma mem_2 : (s:t)(x:elt)(mem x s)=true -> (In x s).
Definition equal : t -> t -> bool :=
[s,s']if (M.equal s s') then [_]true else [_]false.
Lemma equal_1 : (s,s':t)(Equal s s') -> (equal s s')=true.
Lemma equal_2 : (s,s':t)(equal s s')=true -> (Equal s s').
Definition subset : t -> t -> bool :=
[s,s']if (M.subset s s') then [_]true else [_]false.
Lemma subset_1 : (s,s':t)(Subset s s') -> (subset s s')=true.
Lemma subset_2 : (s,s':t)(subset s s')=true -> (Subset s s').
Definition choose : t -> (option elt) :=
[s:t]Cases (M.choose s) of (inleft (exist x _)) => (Some ? x)
| (inright _) => (None ?) end.
Lemma choose_1 : (s:t)(x:elt) (choose s)=(Some ? x) -> (In x s).
Lemma choose_2 : (s:t)(choose s)=(None ?) -> (Empty s).
Definition elements : t -> (list elt) := [s] let (l,_) = (M.elements s) in l.
Lemma elements_1: (s:t)(x:elt)(In x s) -> (InList E.eq x (elements s)).
Lemma elements_2: (s:t)(x:elt)(InList E.eq x (elements s)) -> (In x s).
Lemma elements_3: (s:t)(sort E.lt (elements s)).
Definition min_elt : t -> (option elt) :=
[s:t]Cases (M.min_elt s) of (inleft (exist x _)) => (Some ? x)
| (inright _) => (None ?) end.
Lemma min_elt_1: (s:t)(x:elt)(min_elt s) = (Some ? x) -> (In x s).
Lemma min_elt_2: (s:t)(x,y:elt)(min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x).
Lemma min_elt_3 : (s:t)(min_elt s) = (None ?) -> (Empty s).
Definition max_elt : t -> (option elt) :=
[s:t]Cases (M.max_elt s) of (inleft (exist x _)) => (Some ? x)
| (inright _) => (None ?) end.
Lemma max_elt_1: (s:t)(x:elt)(max_elt s) = (Some ? x) -> (In x s).
Lemma max_elt_2: (s:t)(x,y:elt)(max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y).
Lemma max_elt_3 : (s:t)(max_elt s) = (None ?) -> (Empty s).
Definition add : elt -> t -> t :=
[x:elt][s:t]let (s',_) = (M.add x s) in s'.
Lemma add_1 : (s:t)(x,y:elt)(E.eq y x) -> (In y (add x s)).
Lemma add_2 : (s:t)(x,y:elt)(In y s) -> (In y (add x s)).
Lemma add_3 : (s:t)(x,y:elt)~(E.eq x y) -> (In y (add x s)) -> (In y s).
Definition remove : elt -> t -> t :=
[x:elt][s:t]let (s',_) = (M.remove x s) in s'.
Lemma remove_1 : (s:t)(x,y:elt)(E.eq y x) -> ~(In y (remove x s)).
Lemma remove_2 : (s:t)(x,y:elt)
~(E.eq x y) ->(In y s) -> (In y (remove x s)).
Lemma remove_3 : (s:t)(x,y:elt)(In y (remove x s)) -> (In y s).
Definition singleton : elt -> t := [x]let (s,_) = (M.singleton x) in s.
Lemma singleton_1 : (x,y:elt)(In y (singleton x)) -> (E.eq x y).
Lemma singleton_2: (x,y:elt)(E.eq x y) -> (In y (singleton x)).
Definition union : t -> t -> t :=
[s,s']let (s'',_) = (M.union s s') in s''.
Lemma union_1: (s,s':t)(x:elt)(In x (union s s')) -> (In x s)\/(In x s').
Lemma union_2: (s,s':t)(x:elt)(In x s) -> (In x (union s s')).
Lemma union_3: (s,s':t)(x:elt)(In x s') -> (In x (union s s')).
Definition inter : t -> t -> t :=
[s,s']let (s'',_) = (M.inter s s') in s''.
Lemma inter_1: (s,s':t)(x:elt)(In x (inter s s')) -> (In x s).
Lemma inter_2: (s,s':t)(x:elt)(In x (inter s s')) -> (In x s').
Lemma inter_3: (s,s':t)(x:elt)(In x s) -> (In x s') -> (In x (inter s s')).
Definition diff : t -> t -> t :=
[s,s']let (s'',_) = (M.diff s s') in s''.
Lemma diff_1: (s,s':t)(x:elt)(In x (diff s s')) -> (In x s).
Lemma diff_2: (s,s':t)(x:elt)(In x (diff s s')) -> ~(In x s').
Lemma diff_3: (s,s':t)(x:elt)(In x s) -> ~(In x s') -> (In x (diff s s')).
Definition cardinal : t -> nat := [s]let (f,_)= (M.cardinal s) in f.
Lemma cardinal_1 :
(s:t)(EX l:(list elt) |
(Unique E.eq l) /\
((x:elt)(In x s)<->(InList E.eq x l)) /\
(cardinal s)=(length l)).
Definition fold : (B:Set)(elt->B->B)->t->B->B :=
[B,f,i,s]let (fold,_)= (M.fold f i s) in fold.
Lemma fold_1:
(s:t)(A:Set)(i:A)(f:elt->A->A)
(EX l:(list elt) |
(Unique E.eq l) /\
((x:elt)(In x s)<->(InList E.eq x l)) /\
(fold f s i)=(fold_right f i l)).
Definition f_dec :
(f: elt -> bool)(x:elt){ (f x)=true } + { (f x)<>true }.
Lemma compat_P_aux :
(f:elt -> bool)(compat_bool E.eq f) -> (compat_P E.eq [x](f x)=true).
Hints Resolve compat_P_aux.
Definition filter : (elt -> bool) -> t -> t :=
[f,s]let (s',_) = (!M.filter [x](f x)=true (f_dec f) s) in s'.
Lemma filter_1: (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->
(In x (filter f s)) -> (In x s).
Lemma filter_2:
(s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->(In x (filter f s)) -> (f x)=true.
Lemma filter_3:
(s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->
(In x s) -> (f x)=true -> (In x (filter f s)).
Definition for_all: (elt -> bool) -> t -> bool :=
[f,s]if (!M.for_all [x](f x)=true (f_dec f) s) then [_]true else [_]false.
Lemma for_all_1:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(For_all [x](f x)=true s) -> (for_all f s)=true.
Lemma for_all_2:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->(for_all f s)=true -> (For_all [x](f x)=true s).
Definition exists: (elt -> bool) -> t -> bool :=
[f,s]if (!M.exists [x](f x)=true (f_dec f) s) then [_]true else [_]false.
Lemma exists_1:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(Exists [x](f x)=true s) -> (exists f s)=true.
Lemma exists_2:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(exists f s)=true -> (Exists [x](f x)=true s).
Definition partition : (elt -> bool) -> t -> t*t :=
[f,s]let (p,_) = (!M.partition [x](f x)=true (f_dec f) s) in p.
Lemma partition_1:
(s:t)(f:elt->bool)(compat_bool E.eq f) -> (Equal (fst ? ? (partition f s)) (filter f s)).
Lemma partition_2:
(s:t)(f:elt->bool)(compat_bool E.eq f) ->
(Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)).
Module E:=E.
Definition elt := elt.
Definition t := t.
Definition In := In.
Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
Definition Empty := [s](a:elt)~(In a s).
Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
Definition eq := eq.
Definition lt := lt.
Definition eq_refl := eq_refl.
Definition eq_sym := eq_sym.
Definition eq_trans := eq_trans.
Definition lt_trans := lt_trans.
Definition lt_not_eq := lt_not_eq.
Definition compare := compare.
End NodepOfDep.