Library FSetProperties

Two-argument functions that allow to reorder its arguments.


Definition transpose := [f:A->B->B](x,y:A)(z:B)(eqB (f x (f y z)) (f y (f x z))).

Compatibility of a two-argument function with respect to two equalities.


Definition compat_op := [f:A->B->B](x,x':A)(y,y':B)(eqA x x') -> (eqB y y') ->
 (eqB (f x y) (f x' y')).

Compatibility of a function upon natural numbers.


Definition compat_nat := [f:A->nat] (x,x':A)(eqA x x') -> (f x)=(f x').

End Misc.
Hints Unfold transpose compat_op compat_nat.

To prove (Setoid_Theory ? (eq ?))


Tactic Definition ST :=
  Constructor; Intros;[ Trivial | Symmetry; Trivial | EApply trans_eq; EAuto ].
Hint st : core := Extern 1 (Setoid_Theory ? (eq ?)) ST.

Definition gen_st : (A:Set)(Setoid_Theory ? (eq A)).

Usual syntax for lists. CAVEAT: the Coq cast "::" will no longer be available.


Notation "[]" := (nil ?) (at level 1).
Notation "a :: l" := (cons a l) (at level 1, l at next level).

Module Properties [M:S].
  Import M.
  Import Logic.
  Import Peano.
  
  Module ME := MoreOrderedType E.

Alternative (weaker) specification for fold, based on empty (fold_1) and add (fold_2).

   Section Old_Spec_Now_Properties.

Results about lists without duplicates

    Section Unique_Remove.

   Fixpoint remove_list [x:elt;s:(list elt)] : (list elt) := Cases s of
      nil => []
    | (cons y l) => if (ME.eq_dec x y) then [_]l else [_]y::(remove_list x l)
   end.

   Lemma remove_list_correct :
    (s:(list elt))(x:elt)(Unique E.eq s) ->
    (Unique E.eq (remove_list x s)) /\
    ((y:elt)(InList E.eq y (remove_list x s))<->(InList E.eq y s)/\~(E.eq x y)).

   Local ListEq := [l,l'](y:elt)(InList E.eq y l)<->(InList E.eq y l').
   Local ListAdd := [x,l,l'](y:elt)(InList E.eq y l')<->(E.eq y x)\/(InList E.eq y l).

   Lemma remove_list_equal :
    (s,s':(list elt))(x:elt)(Unique E.eq x::s) -> (Unique E.eq s') ->
    (ListEq x::s s') -> (ListEq s (remove_list x s')).

   Lemma remove_list_add :
    (s,s':(list elt))(x,x':elt)(Unique E.eq s) -> (Unique E.eq x'::s') ->
    ~(E.eq x x') -> ~(InList E.eq x s) ->
    (ListAdd x s x'::s') -> (ListAdd x (remove_list x' s) s').

   Lemma remove_list_fold_right :
    (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
    (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
    (s:(list elt))(x:elt)(Unique E.eq s) -> (InList E.eq x s) ->
    (eqA (fold_right f i s) (f x (fold_right f i (remove_list x s)))).

   Lemma fold_right_equal :
    (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
    (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
    (s,s':(list elt))(Unique E.eq s) -> (Unique E.eq s') -> (ListEq s s') ->
    (eqA (fold_right f i s) (fold_right f i s')).

   Lemma fold_right_add :
    (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
    (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
    (s',s:(list elt))(x:elt)(Unique E.eq s) -> (Unique E.eq s') -> ~(InList E.eq x s) ->
    (ListAdd x s s') ->
    (eqA (fold_right f i s') (f x (fold_right f i s))).

   End Unique_Remove.

An alternate (and previous) specification for fold was based on the recursive structure of a set. It is now lemmas fold_1 and fold_2.

  Lemma fold_1:
   (s:t)(A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))(i:A)(f:elt->A->A)
   (Empty s) -> (eqA (fold f s i) i).

  Lemma fold_2 :
     (s,s':t)(x:elt)(A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
     (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) -> ~(In x s) ->
     (Add x s s') -> (eqA (fold f s' i) (f x (fold f s i))).

Similar specification for cardinal.

  Lemma cardinal_fold : (s:t)(cardinal s)=(fold [_]S s O).

  Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O.

  Lemma cardinal_2 :
    (s,s':t)(x:elt)~(In x s) -> (Add x s s') -> (cardinal s') = (S (cardinal s)).

   Hints Resolve cardinal_1 cardinal_2.

   End Old_Spec_Now_Properties.

Induction principle over sets

  Lemma Add_add :
    (s:t)(x:elt)(Add x s (add x s)).

  Lemma Add_remove : (s:t)(x:elt)(In x s) -> (Add x (remove x s) s).
 
   Hints Resolve Add_add Add_remove.

  Lemma Equal_remove : (s,s':t)(x:elt)(In x s)->(Equal s s')->
     (Equal (remove x s) (remove x s')).

   Hints Resolve Equal_remove.

  Lemma cardinal_inv_1 : (s:t)(cardinal s)=O -> (Empty s).
   Hints Resolve cardinal_inv_1.
 
  Lemma cardinal_inv_2 :
     (s:t)(n:nat)(cardinal s)=(S n) -> (EX x:elt | (In x s)).

  Lemma Equal_cardinal_aux : (n:nat)(s,s':t)(cardinal s)=n ->
       (Equal s s')->(cardinal s)=(cardinal s').

  Lemma Equal_cardinal : (s,s':t)(Equal s s')->(cardinal s)=(cardinal s').

   Hints Resolve Add_add Add_remove Equal_remove
                cardinal_inv_1 Equal_cardinal.

  Lemma empty_cardinal: (cardinal empty)=O.

  Lemma empty_cardinal_2 : (s:t)(Empty s) -> (cardinal s)=O.

   Hints Immediate empty_cardinal empty_cardinal_2 : set.

  Lemma cardinal_induction : (P : t -> Prop)
     ((s:t)(Empty s)->(P s)) ->
     ((s,s':t)(P s) -> (x:elt)~(In x s) -> (Add x s s') -> (P s')) ->
     (n:nat)(s:t)(cardinal s)=n -> (P s).

  Lemma set_induction : (P : t -> Prop)
     ((s:t)(Empty s)->(P s)) ->
     ((s,s':t)(P s) -> (x:elt)~(In x s) -> (Add x s s') -> (P s')) ->
     (s:t)(P s).

Other formulation of fold_1 and fold_2.

   Section Fold.

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

   Variable A:Set.
   Variable eqA:A->A->Prop.
   Variable st:(Setoid_Theory ? eqA).
   Variable i:A.
   Variable f:elt->A->A.
   Variable Comp:(compat_op E.eq eqA f).
   Variable Assoc:(transpose eqA f).
 
  Lemma fold_empty: (eqA (fold f empty i) i).

  Lemma fold_equal:
    (Equal s s') -> (eqA (fold f s i) (fold f s' i)).
   
  Lemma fold_add:
    ~(In x s) -> (eqA (fold f (add x s) i) (f x (fold f s i))).

   End Fold.

properties of Equal

  Lemma equal_refl : (s:t)(Equal s s).

  Lemma equal_sym : (s,s':t)(Equal s s') -> (Equal s' s).

  Lemma equal_trans :
    (s,u,v:t)(Equal s u) -> (Equal u v) -> (Equal s v).

   Hints Resolve equal_refl equal_trans : set.
   Hints Immediate equal_sym : set.

properties of Subset

  Lemma subset_refl : (s:t)(Subset s s).

  Lemma subset_antisym :
    (s,s':t)(Subset s s') -> (Subset s' s) -> (Equal s s').

  Lemma subset_trans :
   (s,t_,u:t)(Subset s t_) -> (Subset t_ u) -> (Subset s u).

  Lemma subset_equal :
    (s,s':t)(Equal s s') -> (Subset s s').

  Lemma subset_empty :
    (s:t)(Subset empty s).

  Lemma subset_remove_3 :
    (s1,s2:t)(x:elt)
    (Subset s1 s2) -> (Subset (remove x s1) s2).

  Lemma subset_diff :
    (s1,s2,s3:t)
    (Subset s1 s3) -> (Subset (diff s1 s2) s3).

  Lemma subset_add_3 :
    (s1,s2:t)(x:elt)
    (In x s2) -> (Subset s1 s2) -> (Subset (add x s1) s2).

  Lemma subset_add_2 :
    (s1,s2:t)(x:elt)
    (Subset s1 s2) -> (Subset s1 (add x s2)).

  Lemma in_subset :
    (s1,s2:t)(x:elt)
    (In x s1) -> (Subset s1 s2) -> (In x s2).

   Hints Resolve subset_refl subset_equal subset_antisym
                subset_trans subset_empty subset_remove_3
                subset_diff subset_add_3 subset_add_2 in_subset
                : set.

properties of empty

  Lemma empty_is_empty_1 : (s:t)(Empty s) -> (Equal s empty).

  Lemma empty_is_empty_2 : (s:t)(Equal s empty) -> (Empty s).

   Hints Resolve empty_is_empty_1 empty_is_empty_2 : set.

properties of add

   Tactic Definition Add_ y x s :=
    Generalize (!add_1 s x y) (!add_2 s x y) (!add_3 s x y).

  Lemma add_equal :
    (s:t)(x:elt)(In x s) -> (Equal (add x s) s).

   Hints Resolve add_equal :set.

properties of remove

   Tactic Definition Remove_ a x s :=
    Generalize (!remove_1 s x a) (!remove_2 s x a) (!remove_3 s x a).

  Lemma remove_equal:
    (s:t)(x:elt)~(In x s) -> (Equal (remove x s) s).

   Hints Resolve remove_equal : set.

properties of add and remove

  Lemma add_remove:
    (s:t)(x:elt)(In x s) -> (Equal (add x (remove x s)) s).

  Lemma remove_add:
    (s:t)(x:elt)~(In x s) -> (Equal (remove x (add x s)) s).

   Hints Immediate add_remove remove_add :set.

properties of singleton

   Tactic Definition Singleton a x :=
    Generalize (!singleton_1 x a) (!singleton_2 x a).

  Lemma singleton_equal_add : (x:elt)
    (Equal (singleton x) (add x empty)).

  Lemma singleton_cardinal: (x:elt)(cardinal (singleton x))=(S O).

   Hints Resolve singleton_equal_add singleton_cardinal : set.

properties of union

   Tactic Definition Union a s s' :=
    Generalize (!union_1 s s' a) (!union_2 s s' a) (!union_3 s s' a).

  Lemma union_sym :
    (s,s':t)(Equal (union s s') (union s' s)).

  Lemma union_subset_equal :
    (s,s':t)(Subset s s') -> (Equal (union s s') s').

  Lemma union_equal_1 :
    (s,s',s'':t)(Equal s s') ->
    (Equal (union s s'') (union s' s'')).

  Lemma union_equal_2 :
    (s,s',s'':t)(Equal s' s'') ->
    (Equal (union s s') (union s s'')).

  Lemma union_assoc :
    (s,s',s'':t)
    (Equal (union (union s s') s'') (union s (union s' s''))).

   Hints Resolve union_subset_equal union_equal_1 union_equal_2
                union_assoc : set.
   Hints Immediate union_sym.

  Lemma add_union_singleton:
    (s:t)(x:elt)(Equal (add x s) (union (singleton x) s)).

  Lemma union_add:
    (s,s':t)(x:elt)
    (Equal (union (add x s) s') (add x (union s s'))).

  Lemma union_subset_1 :
    (s,s':t)(Subset s (union s s')).

  Lemma union_subset_2:
    (s,s':t)(Subset s' (union s s')).

  Lemma subset_union :
    (s,s',s'':t)(Subset s s'') -> (Subset s' s'') ->
    (Subset (union s s') s'').

   Hints Resolve add_union_singleton union_add union_subset_1
                union_subset_2 subset_union : set.

properties of inter

   Tactic Definition Inter a s s' :=
    Generalize (!inter_1 s s' a) (!inter_2 s s' a) (!inter_3 s s' a).

  Lemma inter_sym:
   (s,s':t)(Equal (inter s s') (inter s' s)).

  Lemma inter_subset_equal:
    (s,s':t)(Subset s s') -> (Equal (inter s s') s).

  Lemma inter_equal_1:
    (s,s',s'':t)(Equal s s') ->
    (Equal (inter s s'') (inter s' s'')).

  Lemma inter_equal_2:
    (s,s',s'':t)(Equal s' s'') ->
    (Equal (inter s s') (inter s s'')).

   Hints Immediate inter_sym : set.
   Hints Resolve inter_subset_equal inter_equal_1 inter_equal_2 : set.

  Lemma inter_assoc:
    (s,s',s'':t)
    (Equal (inter (inter s s') s'') (inter s (inter s' s''))).

  Lemma union_inter_1:
    (s,s',s'':t)
    (Equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))).

  Lemma union_inter_2:
    (s,s',s'':t)
    (Equal (union (inter s s') s'') (inter (union s s'') (union s' s''))).

  Lemma inter_add_1:
    (s,s':t)(x:elt)(In x s') ->
    (Equal (inter (add x s) s') (add x (inter s s'))).

  Lemma inter_add_2:
    (s,s':t)(x:elt)~(In x s') ->
    (Equal (inter (add x s) s') (inter s s')).

   Hints Resolve inter_assoc union_inter_1 union_inter_2
                inter_add_1 inter_add_2 : set.

properties of Subset

  Lemma inter_subset_1:
    (s,s':t)(Subset (inter s s') s).

  Lemma inter_subset_2:
    (s,s':t)(Subset (inter s s') s').

  Lemma inter_subset_3:
    (s,s',s'':t)(Subset s'' s) -> (Subset s'' s') ->
    (Subset s'' (inter s s')).

   Hints Resolve inter_subset_1 inter_subset_2 inter_subset_3 : set.

Properties of diff

   Tactic Definition Diff a s s' :=
    Generalize (!diff_1 s s' a) (!diff_2 s s' a) (!diff_3 s s' a).

  Lemma diff_subset:
    (s,s':t)(Subset (diff s s') s).

  Lemma diff_subset_equal:
   (s,s':t)(Subset s s') -> (Equal (diff s s') empty).

  Lemma remove_inter_singleton:
    (s:t)(x:elt)(Equal (remove x s) (diff s (singleton x))).

  Lemma diff_inter_empty:
    (s,s':t)(Equal (inter (diff s s') (inter s s')) empty).

  Lemma In_dec : (x:elt)(s:t){ (In x s) }+ { ~(In x s) }.

  Lemma diff_inter_all:
    (s,s':t)(Equal (union (diff s s') (inter s s')) s).

   Hints Resolve diff_subset diff_subset_equal
                remove_inter_singleton diff_inter_empty
                diff_inter_all : set.

  Lemma fold_plus:
    (s:t)(p:nat)(fold [_]S s p)=(fold [_]S s O)+p.

properties of cardinal

  Lemma empty_inter_1 : (s,s':t)(Empty s) -> (Empty (inter s s')).

  Lemma empty_inter_2 : (s,s':t)(Empty s') -> (Empty (inter s s')).

  Lemma empty_union_1 : (s,s':t)(Empty s) -> (Equal (union s s') s').

  Lemma empty_union_2 : (s,s':t)(Empty s) -> (Equal (union s' s) s').

  Lemma empty_diff_1 : (s,s':t)(Empty s) -> (Empty (diff s s')).

  Lemma empty_diff_2 : (s,s':t)(Empty s) -> (Equal (diff s' s) s').

   Hints Resolve empty_inter_1 empty_inter_2
                empty_union_1 empty_union_2
                empty_diff_1 empty_diff_2 : set.

  Lemma union_Add : (s,s',s'':t)(x:elt)
    (Add x s s') -> (Add x (union s s'') (union s' s'')).

  Lemma inter_Add : (s,s',s'':t)(x:elt)
    (In x s'') -> (Add x s s') -> (Add x (inter s s'') (inter s' s'')).

  Lemma union_Equal : (s,s',s'':t)(x:elt)
    (In x s'') -> (Add x s s') -> (Equal (union s s'') (union s' s'')).

  Lemma inter_Add_2 :(s,s',s'':t)(x:elt)
    ~(In x s'') -> (Add x s s') -> (Equal (inter s s'') (inter s' s'')).

  Lemma not_in_union : (x:elt)(s,s':t)
    ~(In x s) -> ~(In x s') -> ~(In x (union s s')).

   Hints Resolve union_Add inter_Add union_Equal inter_Add_2
                not_in_union : set.

  Lemma fold_commutes:
    (A:Set)
    (f:elt->A->A)(i:A)(compat_op E.eq (eq ?) f) -> (transpose (eq ?) f) -> (s:t)(x:elt)
    (fold f s (f x i)) = (f x (fold f s i)).

  Lemma fold_union_inter:
    (A:Set)
    (f:elt->A->A)(i:A)(compat_op E.eq (eq ?) f) -> (transpose (eq ?) f) ->
    (s,s':t)(fold f (union s s') (fold f (inter s s') i))
     = (fold f s (fold f s' i)).

  Lemma fold_diff_inter:
    (A:Set)(f:elt->A->A)(i:A)(compat_op E.eq (eq A) f) -> (transpose (eq A) f) ->
    (s,s':t)(fold f (diff s s') (fold f (inter s s') i))=(fold f s i).

  Lemma diff_inter_cardinal:
    (s,s':t)(cardinal (diff s s'))+(cardinal (inter s s'))=(cardinal s).

  Lemma subset_cardinal:
    (s,s':t)(Subset s s') -> (le (cardinal s) (cardinal s')).

  Lemma union_inter_cardinal:
    (s,s':t)(cardinal (union s s'))+(cardinal (inter s s'))
     = (cardinal s)+(cardinal s').

  Lemma union_cardinal :
    (s,s':t)(le (cardinal (union s s')) (plus (cardinal s) (cardinal s'))).

  Lemma add_cardinal_1:
    (s:t)(x:elt)(In x s) -> (cardinal (add x s))=(cardinal s).

  Lemma add_cardinal_2:
    (s:t)(x:elt)~(In x s) -> (cardinal (add x s))=(S (cardinal s)).

   Hints Resolve subset_cardinal union_cardinal
                add_cardinal_1 add_cardinal_2.

End Properties.