Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: FSetEqProperties.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** * Finite sets library *)

(** This module proves many properties of finite sets that
    are consequences of the axiomatization in [FsetInterface]
    Contrary to the functor in [FsetProperties] it uses
    sets operations instead of predicates over sets, i.e.
    [mem x s=true] instead of [In x s],
    [equal s s'=true] instead of [Equal s s'], etc. *)

Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.

Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
Module Import MP := WProperties_fun E M.
Import FM Dec.F.
Import M.

Definition Add := MP.Add.

Section BasicProperties.

(** Some old specifications written with boolean equalities. *)

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

Lemma mem_eq:
  E.eq x y -> mem x s=mem y s.
Proof.
intro H; rewrite H; auto.
Qed.

Lemma equal_mem_1:
  (forall a, mem a s=mem a s') -> equal s s'=true.
Proof.
intros; apply equal_1; unfold Equal; intros.
do 2 rewrite mem_iff; rewrite H; tauto.
Qed.

Lemma equal_mem_2:
  equal s s'=true -> forall a, mem a s=mem a s'.
Proof.
intros; rewrite (equal_2 H); auto.
Qed.

Lemma subset_mem_1:
  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
Proof.
intros; apply subset_1; unfold Subset; intros a.
do 2 rewrite mem_iff; auto.
Qed.

Lemma subset_mem_2:
  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
Proof.
intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
Qed.

Lemma empty_mem: mem x empty=false.
Proof.
rewrite <- not_mem_iff; auto with set.
Qed.

Lemma is_empty_equal_empty: is_empty s = equal s empty.
Proof.
apply bool_1; split; intros.
auto with set.
rewrite <- is_empty_iff; auto with set.
Qed.

Lemma choose_mem_1: choose s=Some x -> mem x s=true.
Proof.
auto with set.
Qed.

Lemma choose_mem_2: choose s=None -> is_empty s=true.
Proof.
auto with set.
Qed.

Lemma add_mem_1: mem x (add x s)=true.
Proof.
auto with set.
Qed.

Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
Proof.
apply add_neq_b.
Qed.

Lemma remove_mem_1: mem x (remove x s)=false.
Proof.
rewrite <- not_mem_iff; auto with set.
Qed.

Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
Proof.
apply remove_neq_b.
Qed.

Lemma singleton_equal_add:
  equal (singleton x) (add x empty)=true.
Proof.
rewrite (singleton_equal_add x); auto with set.
Qed.

Lemma union_mem:
  mem x (union s s')=mem x s || mem x s'.
Proof.
apply union_b.
Qed.

Lemma inter_mem:
  mem x (inter s s')=mem x s && mem x s'.
Proof.
apply inter_b.
Qed.

Lemma diff_mem:
  mem x (diff s s')=mem x s && negb (mem x s').
Proof.
apply diff_b.
Qed.

(** properties of [mem] *)

Lemma mem_3 : ~In x s -> mem x s=false.
Proof.
intros; rewrite <- not_mem_iff; auto.
Qed.

Lemma mem_4 : mem x s=false -> ~In x s.
Proof.
intros; rewrite not_mem_iff; auto.
Qed.

(** Properties of [equal] *)

Lemma equal_refl: equal s s=true.
Proof.
auto with set.
Qed.

Lemma equal_sym: equal s s'=equal s' s.
Proof.
intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
Qed.

Lemma equal_trans:
equal s s'=true -> equal s' s''=true -> equal s s''=true.
Proof.
intros; rewrite (equal_2 H); auto.
Qed.

Lemma equal_equal:
equal s s'=true -> equal s s''=equal s' s''.
Proof.
intros; rewrite (equal_2 H); auto.
Qed.

Lemma equal_cardinal:
equal s s'=true -> cardinal s=cardinal s'.
Proof.
auto with set fset.
Qed.

(* Properties of [subset] *)

Lemma subset_refl: subset s s=true.
Proof.
auto with set.
Qed.

Lemma subset_antisym:
subset s s'=true -> subset s' s=true -> equal s s'=true.
Proof.
auto with set.
Qed.

Lemma subset_trans:
subset s s'=true -> subset s' s''=true -> subset s s''=true.
Proof.
do 3 rewrite <- subset_iff; intros.
apply subset_trans with s'; auto.
Qed.

Lemma subset_equal:
equal s s'=true -> subset s s'=true.
Proof.
auto with set.
Qed.

(** Properties of [choose] *)

Lemma choose_mem_3:
is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
Proof.
intros.
generalize (@choose_1 s) (@choose_2 s).
destruct (choose s);intros.
exists e;auto with set.
generalize (H1 Logic.eq_refl); clear H1.
intros; rewrite (is_empty_1 H1) in H; discriminate.
Qed.

Lemma choose_mem_4: choose empty=None.
Proof.
generalize (@choose_1 empty).
case (@choose empty);intros;auto.
elim (@empty_1 e); auto.
Qed.

(** Properties of [add] *)

Lemma add_mem_3:
mem y s=true -> mem y (add x s)=true.
Proof.
auto with set.
Qed.

Lemma add_equal:
mem x s=true -> equal (add x s) s=true.
Proof.
auto with set.
Qed.

(** Properties of [remove] *)

Lemma remove_mem_3:
mem y (remove x s)=true -> mem y s=true.
Proof.
rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
Qed.

Lemma remove_equal:
mem x s=false -> equal (remove x s) s=true.
Proof.
intros; apply equal_1; apply remove_equal.
rewrite not_mem_iff; auto.
Qed.

Lemma add_remove:
mem x s=true -> equal (add x (remove x s)) s=true.
Proof.
intros; apply equal_1; apply add_remove; auto with set.
Qed.

Lemma remove_add:
mem x s=false -> equal (remove x (add x s)) s=true.
Proof.
intros; apply equal_1; apply remove_add; auto.
rewrite not_mem_iff; auto.
Qed.

(** Properties of [is_empty] *)

Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
Proof.
intros; apply bool_1; split; intros.
rewrite MP.cardinal_1; simpl; auto with set.
assert (cardinal s = 0) by (apply zerob_true_elim; auto).
auto with set fset.
Qed.

(** Properties of [singleton] *)

Lemma singleton_mem_1: mem x (singleton x)=true.
Proof.
auto with set.
Qed.

Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
Proof.
intros; rewrite singleton_b.
unfold eqb; destruct (E.eq_dec x y); intuition.
Qed.

Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
Proof.
intros; apply singleton_1; auto with set.
Qed.

(** Properties of [union] *)

Lemma union_sym:
equal (union s s') (union s' s)=true.
Proof.
auto with set.
Qed.

Lemma union_subset_equal:
subset s s'=true -> equal (union s s') s'=true.
Proof.
auto with set.
Qed.

Lemma union_equal_1:
equal s s'=true-> equal (union s s'') (union s' s'')=true.
Proof.
auto with set.
Qed.

Lemma union_equal_2:
equal s' s''=true-> equal (union s s') (union s s'')=true.
Proof.
auto with set.
Qed.

Lemma union_assoc:
equal (union (union s s') s'') (union s (union s' s''))=true.
Proof.
auto with set.
Qed.

Lemma add_union_singleton:
equal (add x s) (union (singleton x) s)=true.
Proof.
auto with set.
Qed.

Lemma union_add:
equal (union (add x s) s') (add x (union s s'))=true.
Proof.
auto with set.
Qed.

(* characterisation of [union] via [subset] *)

Lemma union_subset_1: subset s (union s s')=true.
Proof.
auto with set.
Qed.

Lemma union_subset_2: subset s' (union s s')=true.
Proof.
auto with set.
Qed.

Lemma union_subset_3:
subset s s''=true -> subset s' s''=true ->
  subset (union s s') s''=true.
Proof.
intros; apply subset_1; apply union_subset_3; auto with set.
Qed.

(** Properties of [inter] *)

Lemma inter_sym: equal (inter s s') (inter s' s)=true.
Proof.
auto with set.
Qed.

Lemma inter_subset_equal:
subset s s'=true -> equal (inter s s') s=true.
Proof.
auto with set.
Qed.

Lemma inter_equal_1:
equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
Proof.
auto with set.
Qed.

Lemma inter_equal_2:
equal s' s''=true -> equal (inter s s') (inter s s'')=true.
Proof.
auto with set.
Qed.

Lemma inter_assoc:
equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
Proof.
auto with set.
Qed.

Lemma union_inter_1:
equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
Proof.
auto with set.
Qed.

Lemma union_inter_2:
equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
Proof.
auto with set.
Qed.

Lemma inter_add_1: mem x s'=true ->
equal (inter (add x s) s') (add x (inter s s'))=true.
Proof.
auto with set.
Qed.

Lemma inter_add_2: mem x s'=false ->
equal (inter (add x s) s') (inter s s')=true.
Proof.
intros; apply equal_1; apply inter_add_2.
rewrite not_mem_iff; auto.
Qed.

(* characterisation of [union] via [subset] *)

Lemma inter_subset_1: subset (inter s s') s=true.
Proof.
auto with set.
Qed.

Lemma inter_subset_2: subset (inter s s') s'=true.
Proof.
auto with set.
Qed.

Lemma inter_subset_3:
subset s'' s=true -> subset s'' s'=true ->
  subset s'' (inter s s')=true.
Proof.
intros; apply subset_1; apply inter_subset_3; auto with set.
Qed.

(** Properties of [diff] *)

Lemma diff_subset: subset (diff s s') s=true.
Proof.
auto with set.
Qed.

Lemma diff_subset_equal:
subset s s'=true -> equal (diff s s') empty=true.
Proof.
auto with set.
Qed.

Lemma remove_inter_singleton:
equal (remove x s) (diff s (singleton x))=true.
Proof.
auto with set.
Qed.

Lemma diff_inter_empty:
equal (inter (diff s s') (inter s s')) empty=true.
Proof.
auto with set.
Qed.

Lemma diff_inter_all:
equal (union (diff s s') (inter s s')) s=true.
Proof.
auto with set.
Qed.

End BasicProperties.

Hint Immediate empty_mem is_empty_equal_empty add_mem_1
   remove_mem_1 singleton_equal_add union_mem inter_mem
   diff_mem equal_sym add_remove remove_add : set.
Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
   subset_refl subset_equal subset_antisym
   add_mem_3 add_equal remove_mem_3 remove_equal : set.

(** General recursion principle *)

Lemma set_rec:  forall (P:t->Type),
(forall s s', equal s s'=true -> P s -> P s') ->
(forall s x, mem x s=false -> P s -> P (add x s)) ->
P empty -> forall s, P s.
Proof.
intros.
apply set_induction; auto; intros.
apply X with empty; auto with set.
apply X with (add x s0); auto with set.
apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
apply X0; auto with set; apply mem_3; auto.
Qed.

(** Properties of [fold] *)

Lemma exclusive_set : forall s s' x,
~(In x s/\In x s') <-> mem x s && mem x s'=false.
Proof.
intros; do 2 rewrite mem_iff.
destruct (mem x s); destruct (mem x s'); intuition.
Qed.

Section Fold.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
Variables (i:A).
Variables (s s':t)(x:elt).

Lemma fold_empty: (fold f empty i) = i.
Proof.
apply fold_empty; auto.
Qed.

Lemma fold_equal:
equal s s'=true -> eqA (fold f s i) (fold f s' i).
Proof.
intros; apply fold_equal with (eqA:=eqA); auto with set.
Qed.

Lemma fold_add:
mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
Proof.
intros; apply fold_add with (eqA:=eqA); auto.
rewrite not_mem_iff; auto.
Qed.

Lemma add_fold:
  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
Proof.
intros; apply add_fold with (eqA:=eqA); auto with set.
Qed.

Lemma remove_fold_1:
mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
Proof.
intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
Qed.

Lemma remove_fold_2:
mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
Proof.
intros; apply remove_fold_2 with (eqA:=eqA); auto.
rewrite not_mem_iff; auto.
Qed.

Lemma fold_union:
(forall x, mem x s && mem x s'=false) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i)).
Proof.
intros; apply fold_union with (eqA:=eqA); auto.
intros; rewrite exclusive_set; auto.
Qed.

End Fold.

(** Properties of [cardinal] *)

Lemma add_cardinal_1:
forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
Proof.
auto with set fset.
Qed.

Lemma add_cardinal_2:
forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
Proof.
intros; apply add_cardinal_2; auto.
rewrite not_mem_iff; auto.
Qed.

Lemma remove_cardinal_1:
forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
Proof.
intros; apply remove_cardinal_1; auto with set.
Qed.

Lemma remove_cardinal_2:
forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
Proof.
intros; apply Equal_cardinal; apply equal_2; auto with set.
Qed.

Lemma union_cardinal:
forall s s', (forall x, mem x s && mem x s'=false) ->
cardinal (union s s')=cardinal s+cardinal s'.
Proof.
intros; apply union_cardinal; auto; intros.
rewrite exclusive_set; auto.
Qed.

Lemma subset_cardinal:
forall s s', subset s s'=true -> cardinal s<=cardinal s'.
Proof.
intros; apply subset_cardinal; auto with set.
Qed.

Section Bool.

(** Properties of [filter] *)

Variable f:elt->bool.
Variable Comp: Proper (E.eq==>Logic.eq) f.

Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).
Proof.
repeat red; intros; f_equal; auto.
Qed.

Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
Proof.
intros; apply filter_b; auto.
Qed.

Lemma for_all_filter:
forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
Proof.
intros; apply bool_1; split; intros.
apply is_empty_1.
unfold Empty; intros.
rewrite filter_iff; auto.
red; destruct 1.
rewrite <- (@for_all_iff s f) in H; auto.
rewrite (H a H0) in H1; discriminate.
apply for_all_1; auto; red; intros.
revert H; rewrite <- is_empty_iff.
unfold Empty; intro H; generalize (H x); clear H.
rewrite filter_iff; auto.
destruct (f x); auto.
Qed.

Lemma exists_filter :
forall s, exists_ f s=negb (is_empty (filter f s)).
Proof.
intros; apply bool_1; split; intros.
destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
apply bool_6.
red; intros; apply (@is_empty_2 _ H0 a); auto with set.
generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
destruct (choose (filter f s)).
intros H0 _; apply exists_1; auto.
exists e; generalize (H0 e); rewrite filter_iff; auto.
intros _ H0.
rewrite (is_empty_1 (H0 Logic.eq_refl)) in H; auto; discriminate.
Qed.

Lemma partition_filter_1:
forall s, equal (fst (partition f s)) (filter f s)=true.
Proof.
auto with set.
Qed.

Lemma partition_filter_2:
forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
Proof.
auto with set.
Qed.

Lemma filter_add_1 : forall s x, f x = true ->
filter f (add x s) [=] add x (filter f s).
Proof.
red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
intuition.
rewrite <- H; apply Comp; auto.
Qed.

Lemma filter_add_2 : forall s x, f x = false ->
filter f (add x s) [=] filter f s.
Proof.
red; intros; do 2 (rewrite filter_iff; auto); set_iff.
intuition.
assert (f x = f a) by (apply Comp; auto).
rewrite H in H1; rewrite H2 in H1; discriminate.
Qed.

Lemma add_filter_1 : forall s s' x,
f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
Proof.
unfold Add, MP.Add; intros.
repeat rewrite filter_iff; auto.
rewrite H0; clear H0.
assert (E.eq x y -> f y = true) by
(intro H0; rewrite <- (Comp _ _ H0); auto).
tauto.
Qed.

Lemma add_filter_2 : forall s s' x,
f x=false -> (Add x s s') -> filter f s [=] filter f s'.
Proof.
unfold Add, MP.Add, Equal; intros.
repeat rewrite filter_iff; auto.
rewrite H0; clear H0.
assert (f a = true -> ~E.eq x a).
intros H0 H1.
rewrite (Comp _ _ H1) in H.
rewrite H in H0; discriminate.
tauto.
Qed.

Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
Proof.
clear Comp' Comp f.
intros.
assert (compat_bool E.eq (fun x => orb (f x) (g x))).
  unfold compat_bool, Proper, respectful; intros.
  rewrite (H x y H1);  rewrite (H0 x y H1); auto.
unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
assert (f a || g a = true <-> f a = true \/ g a = true).
  split; auto with bool.
  intro H3; destruct (orb_prop _ _ H3); auto.
tauto.
Qed.

Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
Proof.
unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
Qed.

(** Properties of [for_all] *)

Lemma for_all_mem_1: forall s,
(forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
Proof.
intros.
rewrite for_all_filter; auto.
rewrite is_empty_equal_empty.
apply equal_mem_1;intros.
rewrite filter_b; auto.
rewrite empty_mem.
generalize (H a); case (mem a s);intros;auto.
rewrite H0;auto.
Qed.

Lemma for_all_mem_2: forall s,
(for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true.
Proof.
intros.
rewrite for_all_filter in H; auto.
rewrite is_empty_equal_empty in H.
generalize (equal_mem_2 _ _ H x).
rewrite filter_b; auto.
rewrite empty_mem.
rewrite H0; simpl;intros.
rewrite <- negb_false_iff; auto.
Qed.

Lemma for_all_mem_3:
forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
Proof.
intros.
apply (bool_eq_ind (for_all f s));intros;auto.
rewrite for_all_filter in H1; auto.
rewrite is_empty_equal_empty in H1.
generalize (equal_mem_2 _ _ H1 x).
rewrite filter_b; auto.
rewrite empty_mem.
rewrite H.
rewrite H0.
simpl;auto.
Qed.

Lemma for_all_mem_4:
forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
Proof.
intros.
rewrite for_all_filter in H; auto.
destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
exists x.
rewrite filter_b in H1; auto.
elim (andb_prop _ _ H1).
split;auto.
rewrite <- negb_true_iff; auto.
Qed.

(** Properties of [exists] *)

Lemma for_all_exists:
forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
Proof.
intros.
rewrite for_all_b; auto.
rewrite exists_b; auto.
induction (elements s); simpl; auto.
destruct (f a); simpl; auto.
Qed.

End Bool.
Section Bool'.

Variable f:elt->bool.
Variable Comp: compat_bool E.eq f.

Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
Proof.
unfold compat_bool, Proper, respectful in *; intros; f_equal; auto.
Qed.

Lemma exists_mem_1:
forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
Proof.
intros.
rewrite for_all_exists; auto.
rewrite for_all_mem_1;auto with bool.
intros;generalize (H x H0);intros.
rewrite negb_true_iff; auto.
Qed.

Lemma exists_mem_2:
forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false.
Proof.
intros.
rewrite for_all_exists in H; auto.
rewrite negb_false_iff in H.
rewrite <- negb_true_iff.
apply for_all_mem_2 with (2:=H); auto.
Qed.

Lemma exists_mem_3:
forall s x, mem x s=true -> f x=true -> exists_ f s=true.
Proof.
intros.
rewrite for_all_exists; auto.
rewrite negb_true_iff.
apply for_all_mem_3 with x;auto.
rewrite negb_false_iff; auto.
Qed.

Lemma exists_mem_4:
forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
Proof.
intros.
rewrite for_all_exists in H; auto.
rewrite negb_true_iff in H.
destruct (for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,p); auto.
elim p;intros.
exists x;split;auto.
rewrite <-negb_false_iff; auto.
Qed.

End Bool'.

Section Sum.

(** Adding a valuation function on all elements of a set. *)

Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
Notation compat_opL := (compat_op E.eq Logic.eq).
Notation transposeL := (transpose Logic.eq).

Lemma sum_plus :
  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
    forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
Proof.
unfold sum.
intros f g Hf Hg.
assert (fc : compat_opL (fun x:elt =>plus (f x))).  red; auto with fset.
assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset.
assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
intros s;pattern s; apply set_rec.
intros.
rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
intros; do 3 (rewrite (fold_add _ _ st);auto).
rewrite H0;simpl;omega.
do 3 rewrite fold_empty;auto.
Qed.

Lemma sum_filter : forall f, (compat_bool E.eq f) ->
  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
Proof.
unfold sum; intros f Hf.
assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
repeat red; intros.
rewrite (Hf _ _ H); auto.
assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
red; intros; omega.
intros s;pattern s; apply set_rec.
intros.
change elt with E.t.
rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
intros; rewrite (fold_add _ _ st _ cc ct); auto.
generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
assert (~ In x (filter f s0)).
intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
case (f x); simpl; intros.
rewrite (MP.cardinal_2 H1 (H2 Logic.eq_refl (MP.Add_add s0 x))); auto.
rewrite <- (MP.Equal_cardinal (H3 Logic.eq_refl (MP.Add_add s0 x))); auto.
intros; rewrite fold_empty;auto.
rewrite MP.cardinal_1; auto.
unfold Empty; intros.
rewrite filter_iff; auto; set_iff; tauto.
Qed.

Lemma fold_compat :
  forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
  (f g:elt->A->A),
  (compat_op E.eq eqA f) -> (transpose eqA f) ->
  (compat_op E.eq eqA g) -> (transpose eqA g) ->
  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) ->
  (eqA (fold f s i) (fold g s i)).
Proof.
intros A eqA st f g fc ft gc gt i.
intro s; pattern s; apply set_rec; intros.
transitivity (fold f s0 i).
apply fold_equal with (eqA:=eqA); auto.
rewrite equal_sym; auto.
transitivity (fold g s0 i).
apply H0; intros; apply H1; auto with set.
elim  (equal_2 H x); auto with set; intros.
apply fold_equal with (eqA:=eqA); auto with set.
transitivity (f x (fold f s0 i)).
apply fold_add with (eqA:=eqA); auto with set.
transitivity (g x (fold f s0 i)); auto with set.
transitivity (g x (fold g s0 i)); auto with set.
apply gc; auto with *.
symmetry; apply fold_add with (eqA:=eqA); auto.
do 2 rewrite fold_empty; reflexivity.
Qed.

Lemma sum_compat :
  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
  forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
intros.
unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.
intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
Qed.

End Sum.

End WEqProperties_fun.

(** Now comes variants for self-contained weak sets and for full sets.
    For these variants, only one argument is necessary. Thanks to
    the subtyping [WS<=S], the [EqProperties] functor which is meant to be
    used on modules [(M:S)] can simply be an alias of [WEqProperties]. *)

Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
Module EqProperties := WEqProperties.

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.