Library FSetInterface

Misc properties used in specifications.

Section Misc.
Variable A,B : Set.
Variable eqA : A -> A -> Prop.
Variable eqB : B -> B -> Prop.

Compatibility of a boolean function with respect to an equality.


Definition compat_bool := [f:A->bool] (x,y:A)(eqA x y) -> (f x)=(f y).

Compatibility of a predicate with respect to an equality.


Definition compat_P := [P:A->Prop](x,y:A)(eqA x y) -> (P x) -> (P y).

Being in a list modulo an equality relation.


Inductive InList [x:A] : (list A) -> Prop :=
  | InList_cons_hd : (y:A)(l:(list A))(eqA x y) -> (InList x (cons y l))
  | InList_cons_tl : (y:A)(l:(list A))(InList x l) -> (InList x (cons y l)).

A list without redondancy.


Inductive Unique : (list A) -> Prop :=
  | Unique_nil : (Unique (nil A))
  | Unique_cons : (x:A)(l:(list A)) ~(InList x l) -> (Unique l) -> (Unique (cons x l)).

End Misc.

Hint InList := Constructors InList.
Hint InList := Constructors Unique.
Hint sort := Constructors sort.
Hint lelistA := Constructors lelistA.
Hints Unfold compat_bool compat_P.

Ordered types

Inductive Compare [X:Set; lt,eq:X->X->Prop; x,y:X] : Set :=
  | Lt : (lt x y) -> (Compare lt eq x y)
  | Eq : (eq x y) -> (Compare lt eq x y)
  | Gt : (lt y x) -> (Compare lt eq x y).

Module Type OrderedType.

  Parameter t : Set.

  Parameter eq : t -> t -> Prop.
  Parameter lt : t -> t -> Prop.

  Axiom eq_refl : (x:t) (eq x x).
  Axiom eq_sym : (x,y:t) (eq x y) -> (eq y x).
  Axiom eq_trans : (x,y,z:t) (eq x y) -> (eq y z) -> (eq x z).
 
  Axiom lt_trans : (x,y,z:t) (lt x y) -> (lt y z) -> (lt x z).
  Axiom lt_not_eq : (x,y:t) (lt x y) -> ~(eq x y).

  Parameter compare : (x,y:t)(Compare lt eq x y).

   Hints Immediate eq_sym.
   Hints Resolve eq_refl eq_trans lt_not_eq lt_trans.

End OrderedType.

Non-dependent signature Signature S presents sets as purely informative programs together with axioms

Module Type S.

  Declare Module E : OrderedType.
  Definition elt := E.t.

  Parameter t : Set.

the abstract type of sets


 
  Parameter empty: t.


The empty set.

  Parameter is_empty: t -> bool.


Test whether a set is empty or not.

  Parameter mem: elt -> t -> bool.


mem x s tests whether x belongs to the set s.

  Parameter add: elt -> t -> t.


add x s returns a set containing all elements of s, plus x. If x was already in s, s is returned unchanged.

  Parameter singleton: elt -> t.


singleton x returns the one-element set containing only x.

  Parameter remove: elt -> t -> t.


remove x s returns a set containing all elements of s, except x. If x was not in s, s is returned unchanged.

  Parameter union: t -> t -> t.


Set union.

  Parameter inter: t -> t -> t.


Set intersection.

  Parameter diff: t -> t -> t.


Set difference.

  Parameter eq : t -> t -> Prop.
  Parameter lt : t -> t -> Prop.
  Parameter compare: (s,s':t)(Compare lt eq s s').


Total ordering between sets. Can be used as the ordering function for doing sets of sets.

  Parameter equal: t -> t -> bool.


equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

  Parameter subset: t -> t -> bool.


subset s1 s2 tests whether the set s1 is a subset of the set s2.

Coq comment: iter is useless in a purely functional world




iter: (elt -> unit) -> set -> unit. i




iter f s applies f in turn to all elements of s. The order in which the elements of s are presented to f is unspecified.

  Parameter fold: (A:Set)(elt -> A -> A) -> t -> A -> A.


fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s. The order in which elements of s are presented to f is unspecified.

  Parameter for_all: (elt -> bool) -> t -> bool.


for_all p s checks if all elements of the set satisfy the predicate p.

  Parameter exists: (elt -> bool) -> t -> bool.


exists p s checks if at least one element of the set satisfies the predicate p.

  Parameter filter: (elt -> bool) -> t -> t.


filter p s returns the set of all elements in s that satisfy predicate p.

  Parameter partition: (elt -> bool) -> t -> t * t.


partition p s returns a pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate p, and s2 is the set of all the elements of s that do not satisfy p.

  Parameter cardinal: t -> nat.


Return the number of elements of a set.




Coq comment: nat instead of int ...

  Parameter elements: t -> (list elt).


Return the list of all elements of the given set. The returned list is sorted in increasing order with respect to the ordering Ord.compare, where Ord is the argument given to {!Set.Make}.

  Parameter min_elt: t -> (option elt).


Return the smallest element of the given set (with respect to the Ord.compare ordering), or raise Not_found if the set is empty.




Coq comment: Not_found is represented by the option type

  Parameter max_elt: t -> (option elt).


Same as {!Set.S.min_elt}, but returns the largest element of the given set.




Coq comment: Not_found is represented by the option type

  Parameter choose: t -> (option elt).


Return one element of the given set, or raise Not_found if the set is empty. Which element is chosen is unspecified, but equal elements will be chosen for equal sets.




Coq comment: Not_found is represented by the option type




Coq comment: We do not necessary choose equal elements from equal sets.

   Section Spec.

   Variable s,s',s'' : t.
   Variable x,y,z : elt.

  Parameter In : elt -> t -> Prop.
  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)).

Specification of In


  Parameter In_1: (E.eq x y) -> (In x s) -> (In y s).

Specification of eq


  Parameter eq_refl: (eq s s).
  Parameter eq_sym: (eq s s') -> (eq s' s).
  Parameter eq_trans: (eq s s') -> (eq s' s'') -> (eq s s'').
 


Specification of lt


  Parameter lt_trans : (lt s s') -> (lt s' s'') -> (lt s s'').
  Parameter lt_not_eq : (lt s s') -> ~(eq s s').

Specification of mem


  Parameter mem_1: (In x s) -> (mem x s)=true.
  Parameter mem_2: (mem x s)=true -> (In x s).
 


Specification of equal


  Parameter equal_1: (Equal s s') -> (equal s s')=true.
  Parameter equal_2: (equal s s')=true -> (Equal s s').

Specification of subset


  Parameter subset_1: (Subset s s') -> (subset s s')=true.
  Parameter subset_2: (subset s s')=true -> (Subset s s').

Specification of empty


  Parameter empty_1: (Empty empty).

Specification of is_empty


  Parameter is_empty_1: (Empty s) -> (is_empty s)=true.
  Parameter is_empty_2: (is_empty s)=true -> (Empty s).
 


Specification of add


  Parameter add_1: (E.eq y x) -> (In y (add x s)).
  Parameter add_2: (In y s) -> (In y (add x s)).
  Parameter add_3: ~(E.eq x y) -> (In y (add x s)) -> (In y s).

Specification of remove


  Parameter remove_1: (E.eq y x) -> ~(In y (remove x s)).
  Parameter remove_2: ~(E.eq x y) -> (In y s) -> (In y (remove x s)).
  Parameter remove_3: (In y (remove x s)) -> (In y s).

Specification of singleton


  Parameter singleton_1: (In y (singleton x)) -> (E.eq x y).
  Parameter singleton_2: (E.eq x y) -> (In y (singleton x)).

Specification of union


  Parameter union_1: (In x (union s s')) -> (In x s)\/(In x s').
  Parameter union_2: (In x s) -> (In x (union s s')).
  Parameter union_3: (In x s') -> (In x (union s s')).

Specification of inter


  Parameter inter_1: (In x (inter s s')) -> (In x s).
  Parameter inter_2: (In x (inter s s')) -> (In x s').
  Parameter inter_3: (In x s) -> (In x s') -> (In x (inter s s')).

Specification of diff


  Parameter diff_1: (In x (diff s s')) -> (In x s).
  Parameter diff_2: (In x (diff s s')) -> ~(In x s').
  Parameter diff_3: (In x s) -> ~(In x s') -> (In x (diff s s')).
 


Specification of fold


  Parameter fold_1:
   (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)).

Specification of cardinal


  Parameter cardinal_1:
    (EX l:(list elt) |
        (Unique E.eq l) /\
        ((x:elt)(In x s)<->(InList E.eq x l)) /\
        (cardinal s)=(length l)).

   Section Filter.
  
   Variable f:elt->bool.

Specification of filter


  Parameter filter_1: (compat_bool E.eq f) -> (In x (filter f s)) -> (In x s).
  Parameter filter_2: (compat_bool E.eq f) -> (In x (filter f s)) -> (f x)=true.
  Parameter filter_3:
    (compat_bool E.eq f) -> (In x s) -> (f x)=true -> (In x (filter f s)).

Specification of for_all


  Parameter for_all_1:
    (compat_bool E.eq f) -> (For_all [x](f x)=true s) -> (for_all f s)=true.
  Parameter for_all_2:
    (compat_bool E.eq f) -> (for_all f s)=true -> (For_all [x](f x)=true s).

Specification of exists


  Parameter exists_1:
    (compat_bool E.eq f) -> (Exists [x](f x)=true s) -> (exists f s)=true.
  Parameter exists_2:
    (compat_bool E.eq f) -> (exists f s)=true -> (Exists [x](f x)=true s).

Specification of partition


  Parameter partition_1:
    (compat_bool E.eq f) -> (Equal (fst ? ? (partition f s)) (filter f s)).
  Parameter partition_2:
    (compat_bool E.eq f) ->
    (Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)).

Specification of elements


  Parameter elements_1: (In x s) -> (InList E.eq x (elements s)).
  Parameter elements_2: (InList E.eq x (elements s)) -> (In x s).
  Parameter elements_3: (sort E.lt (elements s)).

Specification of min_elt


  Parameter min_elt_1: (min_elt s) = (Some ? x) -> (In x s).
  Parameter min_elt_2: (min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x).
  Parameter min_elt_3: (min_elt s) = (None ?) -> (Empty s).

Specification of max_elt


  Parameter max_elt_1: (max_elt s) = (Some ? x) -> (In x s).
  Parameter max_elt_2: (max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y).
  Parameter max_elt_3: (max_elt s) = (None ?) -> (Empty s).

Specification of choose


  Parameter choose_1: (choose s)=(Some ? x) -> (In x s).
  Parameter choose_2: (choose s)=(None ?) -> (Empty s).
   End Filter.
   End Spec.

  Notation "∅" := empty.
  Notation "a ⋃ b" := (union a b) (at level 1).
  Notation "a ⋂ b" := (inter a b) (at level 1).
  Notation "∥ a ∥" := (cardinal a) (at level 1).
  Notation "a ∈ b" := (In a b) (at level 1).
  Notation "a ∉ b" := ~(In a b) (at level 1).
  Notation "a ≡ b" := (Equal a b) (at level 1).
  Notation "a ≢ b" := ~(Equal a b) (at level 1).
  Notation "a ⊆ b" := (Subset a b) (at level 1).
  Notation "a ⊈ b" := ~(Subset a b) (at level 1).

   Hints Immediate
  In_1.
  
   Hints Resolve
  mem_1 mem_2
  equal_1 equal_2
  subset_1 subset_2
  empty_1
  is_empty_1 is_empty_2
  choose_1
  choose_2
  add_1 add_2 add_3
  remove_1 remove_2 remove_3
  singleton_1 singleton_2
  union_1 union_2 union_3
  inter_1 inter_2 inter_3
  diff_1 diff_2 diff_3
  filter_1 filter_2 filter_3
  for_all_1 for_all_2
  exists_1 exists_2
  partition_1 partition_2
  elements_1 elements_2 elements_3
  min_elt_1 min_elt_2 min_elt_3
  max_elt_1 max_elt_2 max_elt_3.

End S.

Dependent signature Signature Sdep presents sets using dependent types

Module Type Sdep.

  Declare Module E : OrderedType.
  Definition elt := E.t.

  Parameter t : Set.

  Parameter eq : t -> t -> Prop.
  Parameter lt : t -> t -> Prop.
  Parameter compare: (s,s':t)(Compare lt eq s s').

  Parameter eq_refl: (s:t)(eq s s).
  Parameter eq_sym: (s,s':t)(eq s s') -> (eq s' s).
  Parameter eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').
  Parameter lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').
  Parameter lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s').

  Parameter In : elt -> t -> Prop.
  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)).

  Parameter eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s).

  Parameter empty : { s:t | Empty s }.

  Parameter is_empty : (s:t){ Empty s }+{ ~(Empty s) }.

  Parameter mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.

  Parameter add : (x:elt) (s:t) { s':t | (Add x s s') }.

  Parameter singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.
  
  Parameter remove : (x:elt)(s:t)
                     { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.

  Parameter union : (s,s':t)
                    { s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.

  Parameter inter : (s,s':t)
                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.

  Parameter diff : (s,s':t)
                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.

  Parameter equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
 
  Parameter subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }.

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

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

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

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

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

  Parameter elements :
     (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}.

  Parameter min_elt :
     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.

  Parameter max_elt :
     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.

  Parameter choose : (s:t) { x:elt | (In x s)} + { Empty s }.

  Notation "∅" := empty.
  Notation "a ⋃ b" := (union a b) (at level 1).
  Notation "a ⋂ b" := (inter a b) (at level 1).
  Notation "a ∈ b" := (In a b) (at level 1).
  Notation "a ∉ b" := ~(In a b) (at level 1).
  Notation "a ≡ b" := (Equal a b) (at level 1).
  Notation "a ≢ b" := ~(Equal a b) (at level 1).
  Notation "a ⊆ b" := (Subset a b) (at level 1).
  Notation "a ⊈ b" := ~(Subset a b) (at level 1).
        
End Sdep.

Ordered types properties

Additional properties that can be derived from signature OrderedType.

Module MoreOrderedType [O:OrderedType].

  Lemma gt_not_eq : (x,y:O.t)(O.lt y x) -> ~(O.eq x y).
 
  Lemma eq_not_lt : (x,y:O.t)(O.eq x y) -> ~(O.lt x y).

   Hints Resolve gt_not_eq eq_not_lt.

  Lemma eq_not_gt : (x,y:O.t)(O.eq x y) -> ~(O.lt y x).
  
  Lemma lt_antirefl : (x:O.t)~(O.lt x x).

  Lemma lt_not_gt : (x,y:O.t)(O.lt x y) -> ~(O.lt y x).

   Hints Resolve eq_not_gt lt_antirefl lt_not_gt.

  Lemma lt_eq : (x,y,z:O.t)(O.lt x y) -> (O.eq y z) -> (O.lt x z).
 
  Lemma eq_lt : (x,y,z:O.t)(O.eq x y) -> (O.lt y z) -> (O.lt x z).

   Hints Immediate eq_lt lt_eq.

  Lemma elim_compare_eq:
   (x,y:O.t) (O.eq x y) ->
      (EX H : (O.eq x y) | (O.compare x y) = (Eq ? H)).

  Lemma elim_compare_lt:
   (x,y:O.t) (O.lt x y) ->
      (EX H : (O.lt x y) | (O.compare x y) = (Lt ? H)).

  Lemma elim_compare_gt:
   (x,y:O.t) (O.lt y x) ->
      (EX H : (O.lt y x) | (O.compare x y) = (Gt ? H)).

   Tactic Definition Comp_eq x y :=
    Elim (!elim_compare_eq x y);
    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto].

   Tactic Definition Comp_lt x y :=
    Elim (!elim_compare_lt x y);
    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto].

   Tactic Definition Comp_gt x y :=
    Elim (!elim_compare_gt x y);
    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto].

  Lemma eq_dec : (x,y:O.t){(O.eq x y)}+{~(O.eq x y)}.
 
  Lemma lt_dec : (x,y:O.t){(O.lt x y)}+{~(O.lt x y)}.

Results concerning lists modulo E.eq


  
  Notation "'Sort' l" := (sort O.lt l) (at level 10, l at level 8).
  Notation "'Inf' x l" := (lelistA O.lt x l) (at level 10, x,l at level 8).
  Notation "'In' x l" := (InList O.eq x l) (at level 10, x,l at level 8).

  Lemma In_eq: (s:(list O.t))(x,y:O.t)(O.eq x y) -> (In x s) -> (In y s).
   Hints Immediate In_eq.
  
  Lemma Inf_lt : (s:(list O.t))(x,y:O.t)(O.lt x y) -> (Inf y s) -> (Inf x s).
 
  Lemma Inf_eq : (s:(list O.t))(x,y:O.t)(O.eq x y) -> (Inf y s) -> (Inf x s).
   Hints Resolve Inf_lt Inf_eq.

  Lemma In_sort: (s:(list O.t))(x,a:O.t)(Inf a s) -> (In x s) -> (Sort s) -> (O.lt a x).
  
  Lemma Inf_In : (l:(list O.t))(x:O.t)
    ((y:O.t)(PolyList.In y l) -> (O.lt x y)) -> (Inf x l).
 
  Lemma Inf_In_2 : (l:(list O.t))(x:O.t)
    ((y:O.t)(In y l) -> (O.lt x y)) -> (Inf x l).
  
  Lemma In_InList : (l:(list O.t))(x:O.t)(PolyList.In x l) -> (In x l).
   Hints Resolve In_InList.

  Lemma Sort_Unique : (l:(list O.t))(Sort l) -> (Unique O.eq l).

End MoreOrderedType.