Library FSetBridge

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 S to dependent signature Sdep.

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 }.

  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_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 Sdep to non-dependent signature S.

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 In_1 := eq_In.

  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.


Index
This page has been generated by coqdoc