diff options
| -rw-r--r-- | .depend.coq | 6 | ||||
| -rw-r--r-- | .depend.newcoq | 6 | ||||
| -rw-r--r-- | Makefile | 5 | ||||
| -rwxr-xr-x | theories/Bool/Bool.v | 35 | ||||
| -rw-r--r-- | theories/FSets/FSet.v | 16 | ||||
| -rw-r--r-- | theories/FSets/FSetBridge.v | 720 | ||||
| -rw-r--r-- | theories/FSets/FSetInterface.v | 643 | ||||
| -rw-r--r-- | theories/FSets/FSetList.v | 1218 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 1483 | ||||
| -rw-r--r-- | theories/FSets/FSetRBT.v | 2163 | ||||
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 2 |
11 files changed, 6296 insertions, 1 deletions
diff --git a/.depend.coq b/.depend.coq index df150c945f..50e69b3de6 100644 --- a/.depend.coq +++ b/.depend.coq @@ -153,6 +153,12 @@ theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theo theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo +theories/FSets/FSet.vo: theories/FSets/FSet.v theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetRBT.vo +theories/FSets/FSetList.vo: theories/FSets/FSetList.v theories/FSets/FSetInterface.vo +theories/FSets/FSetBridge.vo: theories/FSets/FSetBridge.v theories/FSets/FSetInterface.vo +theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v contrib/omega/Omega.vo theories/FSets/FSetInterface.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Bool/Zerob.vo +theories/FSets/FSetInterface.vo: theories/FSets/FSetInterface.v theories/Bool/Bool.vo theories/Lists/PolyList.vo theories/Sorting/Sorting.vo theories/Setoids/Setoid.vo +theories/FSets/FSetRBT.vo: theories/FSets/FSetRBT.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/FSets/FSetBridge.vo contrib/omega/Omega.vo theories/ZArith/ZArith.vo theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo diff --git a/.depend.newcoq b/.depend.newcoq index 9cdc3b1da4..70a37e7d3c 100644 --- a/.depend.newcoq +++ b/.depend.newcoq @@ -153,6 +153,12 @@ newtheories/Sets/Multiset.vo: newtheories/Sets/Multiset.v newtheories/Sets/Permu newtheories/Sets/Relations_3_facts.vo: newtheories/Sets/Relations_3_facts.v newtheories/Sets/Relations_1.vo newtheories/Sets/Relations_1_facts.vo newtheories/Sets/Relations_2.vo newtheories/Sets/Relations_2_facts.vo newtheories/Sets/Relations_3.vo newtheories/Sets/Partial_Order.vo: newtheories/Sets/Partial_Order.v newtheories/Sets/Ensembles.vo newtheories/Sets/Relations_1.vo newtheories/Sets/Uniset.vo: newtheories/Sets/Uniset.v newtheories/Bool/Bool.vo newtheories/Sets/Permut.vo +newtheories/FSets/FSet.vo: newtheories/FSets/FSet.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetBridge.vo newtheories/FSets/FSetProperties.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetRBT.vo +newtheories/FSets/FSetList.vo: newtheories/FSets/FSetList.v newtheories/FSets/FSetInterface.vo +newtheories/FSets/FSetBridge.vo: newtheories/FSets/FSetBridge.v newtheories/FSets/FSetInterface.vo +newtheories/FSets/FSetProperties.vo: newtheories/FSets/FSetProperties.v newcontrib/omega/Omega.vo newtheories/FSets/FSetInterface.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Bool/Zerob.vo +newtheories/FSets/FSetInterface.vo: newtheories/FSets/FSetInterface.v newtheories/Bool/Bool.vo newtheories/Lists/PolyList.vo newtheories/Sorting/Sorting.vo newtheories/Setoids/Setoid.vo +newtheories/FSets/FSetRBT.vo: newtheories/FSets/FSetRBT.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetBridge.vo newcontrib/omega/Omega.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Adalloc.vo: newtheories/IntMap/Adalloc.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/Arith/Arith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo newtheories/IntMap/Mapcanon.vo: newtheories/IntMap/Mapcanon.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo newtheories/IntMap/Addec.vo: newtheories/IntMap/Addec.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo @@ -594,6 +594,10 @@ SETSVO=theories/Sets/Classical_sets.vo theories/Sets/Permut.vo \ theories/Sets/Multiset.vo theories/Sets/Relations_3_facts.vo \ theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo +FSETSVO=theories/FSets/FSet.vo theories/FSets/FSetList.vo \ + theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo \ + theories/FSets/FSetInterface.vo theories/FSets/FSetRBT.vo + INTMAPVO=theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo \ theories/IntMap/Addec.vo theories/IntMap/Mapcard.vo \ theories/IntMap/Addr.vo theories/IntMap/Mapc.vo \ @@ -678,6 +682,7 @@ bool: $(BOOLVO) zarith: $(ZARITHVO) lists: $(LISTSVO) sets: $(SETSVO) +fsets: $(FSETSVO) intmap: $(INTMAPVO) relations: $(RELATIONSVO) wellfounded: $(WELLFOUNDEDVO) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index d17741295b..40e1f4a680 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -503,3 +503,38 @@ Lemma absoption_orb : (b1,b2:bool) Proof. NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. Qed. + + +(** Misc. equalities between booleans (to be used by Auto) *) + +Lemma bool_1 : (b1,b2:bool)(b1=true <-> b2=true) -> b1=b2. +Proof. + Intros b1 b2; Case b1; Case b2; Intuition. +Qed. + +Lemma bool_2 : (b1,b2:bool)b1=b2 -> b1=true -> b2=true. +Proof. + Intros b1 b2; Case b1; Case b2; Intuition. +Qed. + +Lemma bool_3 : (b:bool) ~(negb b)=true -> b=true. +Proof. + Induction b; Intuition. +Qed. + +Lemma bool_4 : (b:bool) b=true -> ~(negb b)=true. +Proof. + Induction b; Intuition. +Qed. + +Lemma bool_5 : (b:bool) (negb b)=true -> ~b=true. +Proof. + Induction b; Intuition. +Qed. + +Lemma bool_6 : (b:bool) ~b=true -> (negb b)=true. +Proof. + Induction b; Intuition. +Qed. + +Hints Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6. diff --git a/theories/FSets/FSet.v b/theories/FSets/FSet.v new file mode 100644 index 0000000000..50f3799ed3 --- /dev/null +++ b/theories/FSets/FSet.v @@ -0,0 +1,16 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +Require FSetInterface. +Require FSetBridge. +Require FSetProperties. +Require FSetList. +Require FSetRBT. + diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v new file mode 100644 index 0000000000..257aa9e8bf --- /dev/null +++ b/theories/FSets/FSetBridge.v @@ -0,0 +1,720 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** This module implements bridges (as functors) from dependent + to/from non-dependent set signature. *) + +Require Export FSetInterface. +Set Implicit Arguments. + +(** * 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 }. + Proof. + Exists empty; Auto. + Save. + + Definition is_empty: (s:t){ Empty s }+{ ~(Empty s) }. + Proof. + Intros; Generalize (!is_empty_1 s) (!is_empty_2 s). + Case (is_empty s); Intuition. + Save. + + + Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }. + Proof. + Intros; Generalize (!mem_1 s x) (!mem_2 s x). + Case (mem x s); Intuition. + Save. + + Definition add : (x:elt) (s:t){ s':t | (Add x s s') }. + Proof. + Intros; Exists (add x s); Auto. + Unfold Add; Intuition. + Elim (ME.eq_dec x y); Auto. + Intros; Right. + EApply add_3; EAuto. + Apply In_1 with x; Auto. + Save. + + Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}. + Proof. + Intros; Exists (singleton x); Intuition. + Save. + + Definition remove : (x:elt)(s:t) + { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}. + Proof. + Intros; Exists (remove x s); Intuition. + Absurd (In x (remove x s)); Auto. + Apply In_1 with y; Auto. + Elim (ME.eq_dec x y); Intros; Auto. + Absurd (In x (remove x s)); Auto. + Apply In_1 with y; Auto. + EAuto. + Save. + + Definition union : (s,s':t) + { s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}. + Proof. + Intros; Exists (union s s'); Intuition. + Save. + + Definition inter : (s,s':t) + { s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}. + Proof. + Intros; Exists (inter s s'); Intuition; EAuto. + Save. + + Definition diff : (s,s':t) + { s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}. + Proof. + Intros; Exists (diff s s'); Intuition; EAuto. + Absurd (In x s'); EAuto. + Save. + + Definition equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }. + Proof. + Intros. + Generalize (!equal_1 s s') (!equal_2 s s'). + Case (equal s s');Intuition. + Save. + + Definition subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }. + Proof. + Intros. + Generalize (!subset_1 s s') (!subset_2 s s'). + Case (subset s s');Intuition. + Save. + + Definition fold : + (A:Set) + (f:elt->A->A) + { fold:t -> A -> A | (s,s':t)(a:A) + (eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) + ((Empty s) -> (eqA (fold s a) a)) /\ + ((compat_op E.eq eqA f)->(transpose eqA f) -> + (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }. + Proof. + Intros; Exists (!fold A f); Intros. + Split; Intros. + Apply fold_1; Auto. + Apply (!fold_2 s s' x A eqA); Auto. + Save. + + Definition cardinal : + {cardinal : t -> nat | (s,s':t) + ((Empty s) -> (cardinal s)=O) /\ + ((x:elt) (Add x s s') -> ~(In x s) -> + (cardinal s')=(S (cardinal s))) }. + Proof. + Intros; Exists cardinal; EAuto. + Save. + + 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)). + Proof. + Unfold compat_P compat_bool fdec; Intros. + Generalize (E.eq_sym H0); Case (Pdec x); Case (Pdec y); Ground. + Qed. + + 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)) }. + Proof. + Intros. + Exists (filter (fdec Pdec) s). + Intro H; Assert (compat_bool E.eq (fdec Pdec)); Auto. + Intuition. + EAuto. + Generalize (filter_2 H0 H1). + Unfold fdec. + Case (Pdec x); Intuition. + Inversion H2. + Apply filter_3; Auto. + Unfold fdec; Simpl. + Case (Pdec x); Intuition. + Save. + + 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) }. + Proof. + Intros. + Generalize (!for_all_1 s (fdec Pdec)) (!for_all_2 s (fdec Pdec)). + Case (for_all (fdec Pdec) s); Unfold For_all; [Left|Right]; Intros. + Assert (compat_bool E.eq (fdec Pdec)); Auto. + Generalize (H0 H3 (refl_equal ??) ? H2). + Unfold fdec. + Case (Pdec x); Intuition. + Inversion H4. + Intuition. + Absurd false=true; [Auto with bool|Apply H; Auto]. + Intro. + Unfold fdec. + Case (Pdec x); Intuition. + Save. + + 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) }. + Proof. + Intros. + Generalize (!exists_1 s (fdec Pdec)) (!exists_2 s (fdec Pdec)). + Case (exists (fdec Pdec) s); Unfold Exists; [Left|Right]; Intros. + Elim H0; Auto; Intros. + Exists x; Intuition. + Generalize H4. + Unfold fdec. + Case (Pdec x); Intuition. + Inversion H2. + Intuition. + Elim H2; Intros. + Absurd false=true; [Auto with bool|Apply H; Auto]. + Exists x; Intuition. + Unfold fdec. + Case (Pdec x); Intuition. + Save. + + 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))) }. + Proof. + Intros. + Exists (partition (fdec Pdec) s). + Generalize (!partition_1 s (fdec Pdec)) (!partition_2 s (fdec Pdec)). + Case (partition (fdec Pdec) s). + Intros s1 s2; Simpl. + Intros; Assert (compat_bool E.eq (fdec Pdec)); Auto. + Intros; Assert (compat_bool E.eq [x](negb (fdec Pdec x))). + Generalize H2; Unfold compat_bool;Intuition; Apply (f_equal ?? negb); Auto. + Intuition. + Generalize H4; Unfold For_all Equal; Intuition. + Elim (H0 x); Intros. + Assert (fdec Pdec x)=true. + EAuto. + Generalize H8; Unfold fdec; Case (Pdec x); Intuition. + Inversion H9. + Generalize H; Unfold For_all Equal; Intuition. + Elim (H0 x); Intros. + Cut ([x](negb (fdec Pdec x)) x)=true. + Unfold fdec; Case (Pdec x); Intuition. + Change ([x](negb (fdec Pdec x)) x)=true. + Apply (!filter_2 s x); Auto. + LetTac b := (fdec Pdec x); Generalize (refl_equal ? b); + Pattern -1 b; Case b; Unfold b; [Left|Right]. + Elim (H4 x); Intros _ B; Apply B; Auto. + Elim (H x); Intros _ B; Apply B; Auto. + Apply filter_3; Auto. + Rewrite H5; Auto. + EApply (filter_1 1!s 2!x H2); Elim (H4 x); Intros B _; Apply B; Auto. + EApply (filter_1 1!s 2!x H3); Elim (H x); Intros B _; Apply B; Auto. + Save. + + Definition choose : (s:t) {x:elt | (In x s)} + { Empty s }. + Proof. + Intros. + Generalize (!choose_1 s) (!choose_2 s). + Case (choose s); [Left|Right]; Auto. + Exists e; Auto. + Save. + + Definition elements : + (s:t){ l:(list elt) | (sort E.lt l)/\(x:elt)(In x s)<->(InList E.eq x l)}. + Proof. + Intros; Exists (elements s); Intuition. + Save. + + Definition min_elt : + (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }. + Proof. + Intros; Generalize (!min_elt_1 s) (!min_elt_2 s) (!min_elt_3 s). + Case (min_elt s); [Left|Right]; Auto. + Exists e; Unfold For_all; EAuto. + Save. + + Definition max_elt : + (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }. + Proof. + Intros; Generalize (!max_elt_1 s) (!max_elt_2 s) (!max_elt_3 s). + Case (max_elt s); [Left|Right]; Auto. + Exists e; Unfold For_all; EAuto. + Save. + + 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). + Proof. + Unfold empty; Case M.empty; Auto. + Save. + + 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. + Proof. + Intros; Unfold is_empty; Case (M.is_empty s); Auto. + Save. + + Lemma is_empty_2 : (s:t)(is_empty s)=true -> (Empty s). + Proof. + Intro s; Unfold is_empty; Case (M.is_empty s); Auto. + Intros; Discriminate H. + Save. + + 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. + Proof. + Intros; Unfold mem; Case (M.mem x s); Auto. + Save. + + Lemma mem_2 : (s:t)(x:elt)(mem x s)=true -> (In x s). + Proof. + Intros s x; Unfold mem; Case (M.mem x s); Auto. + Intros; Discriminate H. + Save. + + 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. + Proof. + Intros; Unfold equal; Case M.equal; Intuition. + Save. + + Lemma equal_2 : (s,s':t)(equal s s')=true -> (Equal s s'). + Proof. + Intros s s'; Unfold equal; Case (M.equal s s'); Intuition; Inversion H. + Save. + + 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. + Proof. + Intros; Unfold subset; Case M.subset; Intuition. + Save. + + Lemma subset_2 : (s,s':t)(subset s s')=true -> (Subset s s'). + Proof. + Intros s s'; Unfold subset; Case (M.subset s s'); Intuition; Inversion H. + Save. + + 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). + Proof. + Intros s x; Unfold choose; Case (M.choose s). + Destruct s0; Intros; Injection H; Intros; Subst; Auto. + Intros; Discriminate H. + Save. + + Lemma choose_2 : (s:t)(choose s)=(None ?) -> (Empty s). + Proof. + Intro s; Unfold choose; Case (M.choose s); Auto. + Destruct s0; Intros; Discriminate H. + Save. + + 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)). + Proof. + Intros; Unfold elements; Case (M.elements s); Ground. + Save. + + Lemma elements_2: (s:t)(x:elt)(InList E.eq x (elements s)) -> (In x s). + Proof. + Intros s x; Unfold elements; Case (M.elements s); Ground. + Save. + + Lemma elements_3: (s:t)(sort E.lt (elements s)). + Proof. + Intros; Unfold elements; Case (M.elements s); Ground. + Save. + + 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). + Proof. + Intros s x; Unfold min_elt; Case (M.min_elt s). + Destruct s0; Intros; Injection H; Intros; Subst; Intuition. + Intros; Discriminate H. + Save. + + Lemma min_elt_2: (s:t)(x,y:elt)(min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x). + Proof. + Intros s x y; Unfold min_elt; Case (M.min_elt s). + Unfold For_all; Destruct s0; Intros; Injection H; Intros; Subst; Ground. + Intros; Discriminate H. + Save. + + Lemma min_elt_3 : (s:t)(min_elt s) = (None ?) -> (Empty s). + Proof. + Intros s; Unfold min_elt; Case (M.min_elt s); Auto. + Destruct s0; Intros; Discriminate H. + Save. + + 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). + Proof. + Intros s x; Unfold max_elt; Case (M.max_elt s). + Destruct s0; Intros; Injection H; Intros; Subst; Intuition. + Intros; Discriminate H. + Save. + + Lemma max_elt_2: (s:t)(x,y:elt)(max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y). + Proof. + Intros s x y; Unfold max_elt; Case (M.max_elt s). + Unfold For_all; Destruct s0; Intros; Injection H; Intros; Subst; Ground. + Intros; Discriminate H. + Save. + + Lemma max_elt_3 : (s:t)(max_elt s) = (None ?) -> (Empty s). + Proof. + Intros s; Unfold max_elt; Case (M.max_elt s); Auto. + Destruct s0; Intros; Discriminate H. + Save. + + Definition add : elt -> t -> t := + [x:elt][s:t]let (s',_) = (M.add x s) in s'. + + Lemma add_1 : (s:t)(x:elt)(In x (add x s)). + Proof. + Intros; Unfold add; Case (M.add x s); Unfold Add; Ground. + Save. + + Lemma add_2 : (s:t)(x,y:elt)(In y s) -> (In y (add x s)). + Proof. + Intros; Unfold add; Case (M.add x s); Unfold Add; Ground. + Save. + + Lemma add_3 : (s:t)(x,y:elt)~(E.eq x y) -> (In y (add x s)) -> (In y s). + Proof. + Intros s x y; Unfold add; Case (M.add x s); Unfold Add; Ground. + Generalize (a y); Intuition; Absurd (E.eq x y); Auto. + Save. + + Definition remove : elt -> t -> t := + [x:elt][s:t]let (s',_) = (M.remove x s) in s'. + + Lemma remove_1 : (s:t)(x:elt)~(In x (remove x s)). + Proof. + Intros; Unfold remove; Case (M.remove x s); Ground. + Save. + + Lemma remove_2 : (s:t)(x,y:elt) + ~(E.eq x y) ->(In y s) -> (In y (remove x s)). + Proof. + Intros; Unfold remove; Case (M.remove x s); Ground. + Save. + + Lemma remove_3 : (s:t)(x,y:elt)(In y (remove x s)) -> (In y s). + Proof. + Intros s x y; Unfold remove; Case (M.remove x s); Ground. + Save. + + 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). + Proof. + Intros x y; Unfold singleton; Case (M.singleton x); Ground. + Save. + + Lemma singleton_2: (x,y:elt)(E.eq x y) -> (In y (singleton x)). + Proof. + Intros x y; Unfold singleton; Case (M.singleton x); Ground. + Save. + + 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'). + Proof. + Intros s s' x; Unfold union; Case (M.union s s'); Ground. + Save. + + Lemma union_2: (s,s':t)(x:elt)(In x s) -> (In x (union s s')). + Proof. + Intros s s' x; Unfold union; Case (M.union s s'); Ground. + Save. + + Lemma union_3: (s,s':t)(x:elt)(In x s') -> (In x (union s s')). + Proof. + Intros s s' x; Unfold union; Case (M.union s s'); Ground. + Save. + + 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). + Proof. + Intros s s' x; Unfold inter; Case (M.inter s s'); Ground. + Save. + + Lemma inter_2: (s,s':t)(x:elt)(In x (inter s s')) -> (In x s'). + Proof. + Intros s s' x; Unfold inter; Case (M.inter s s'); Ground. + Save. + + Lemma inter_3: (s,s':t)(x:elt)(In x s) -> (In x s') -> (In x (inter s s')). + Proof. + Intros s s' x; Unfold inter; Case (M.inter s s'); Ground. + Save. + + 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). + Proof. + Intros s s' x; Unfold diff; Case (M.diff s s'); Ground. + Save. + + Lemma diff_2: (s,s':t)(x:elt)(In x (diff s s')) -> ~(In x s'). + Proof. + Intros s s' x; Unfold diff; Case (M.diff s s'); Ground. + Save. + + Lemma diff_3: (s,s':t)(x:elt)(In x s) -> ~(In x s') -> (In x (diff s s')). + Proof. + Intros s s' x; Unfold diff; Case (M.diff s s'); Ground. + Save. + + Definition cardinal : t -> nat := let (f,_)= M.cardinal in f. + + Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O. + Proof. + Intros; Unfold cardinal; Case M.cardinal; Ground. + Qed. + + Lemma cardinal_2 : + (s,s':t)(x:elt)~(In x s) -> (Add x s s') -> + (cardinal s')=(S (cardinal s)). + Proof. + Intros; Unfold cardinal; Case M.cardinal; Ground. + Qed. + + Definition fold : (B:Set)(elt->B->B)->t->B->B := + [B,f]let (fold,_)= (M.fold f) in fold. + + 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). + Proof. + Intros; Unfold fold; Case (M.fold f); Ground. + Save. + + 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))). + Proof. + Intros; Unfold fold; Case (M.fold f); Ground. + Save. + + Definition f_dec : + (f: elt -> bool)(x:elt){ (f x)=true } + { (f x)<>true }. + Proof. + Intros; Case (f x); Auto with bool. + Defined. + + Lemma compat_P_aux : + (f:elt -> bool)(compat_bool E.eq f) -> (compat_P E.eq [x](f x)=true). + Proof. + Unfold compat_bool compat_P; Intros; Rewrite <- H1; Ground. + Qed. + + 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). + Proof. + Intros s x f; Unfold filter; Case M.filter; Intuition. + Generalize (i (compat_P_aux H)); Ground. + Save. + + Lemma filter_2: + (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->(In x (filter f s)) -> (f x)=true. + Proof. + Intros s x f; Unfold filter; Case M.filter; Intuition. + Generalize (i (compat_P_aux H)); Ground. + Save. + + 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)). + Proof. + Intros s x f; Unfold filter; Case M.filter; Intuition. + Generalize (i (compat_P_aux H)); Ground. + Save. + + 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. + Proof. + Intros s f; Unfold for_all; Case M.for_all; Intuition; Elim n; Auto. + Qed. + + 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). + Proof. + Intros s f; Unfold for_all; Case M.for_all; Intuition; Inversion H0. + Qed. + + 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. + Proof. + Intros s f; Unfold exists; Case M.exists; Intuition; Elim n; Auto. + Qed. + + Lemma exists_2: + (s:t)(f:elt->bool)(compat_bool E.eq f) -> + (exists f s)=true -> (Exists [x](f x)=true s). + Proof. + Intros s f; Unfold exists; Case M.exists; Intuition; Inversion H0. + Qed. + + 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)). + Proof. + Intros s f; Unfold partition; Case M.partition. + Intro p; Case p; Clear p; Intros s1 s2 H C. + Generalize (H (compat_P_aux C)); Clear H; Intro H. + Simpl; Unfold Equal; Intuition. + Apply filter_3; Ground. + Apply (H0 a); Auto. + Elim (H2 a); Intros. + Assert (In a s). + EApply filter_1; EAuto. + Elim H3; Intros; Auto. + Absurd (f a)=true. + Exact (H a H6). + EApply filter_2; EAuto. + Qed. + + Lemma partition_2: + (s:t)(f:elt->bool)(compat_bool E.eq f) -> + (Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)). + Proof. + Intros s f; Unfold partition; Case M.partition. + Intro p; Case p; Clear p; Intros s1 s2 H C. + Generalize (H (compat_P_aux C)); Clear H; Intro H. + Assert D: (compat_bool E.eq [x](negb (f x))). + Generalize C; Unfold compat_bool; Intros; Apply (f_equal ?? negb); Auto. + Simpl; Unfold Equal; Intuition. + Apply filter_3; Ground. + Generalize (H a H1); Case (f a); Intuition. + Elim (H2 a); Intros. + Assert (In a s). + EApply filter_1; EAuto. + Elim H3; Intros; Auto. + Absurd (f a)=true. + Intro. + Generalize (filter_2 D H1). + Rewrite H7; Intros H8; Inversion H8. + Exact (H0 a H6). + Qed. + + + 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. + diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v new file mode 100644 index 0000000000..ddd12838d6 --- /dev/null +++ b/theories/FSets/FSetInterface.v @@ -0,0 +1,643 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** Set interfaces *) + +Require Export Bool. +Require Export PolyList. +Require Export Sorting. +Require Export Setoid. +Set Implicit Arguments. + +(** Misc properties used in specifications. *) + +Section Misc. +Variable A,B : Set. +Variable eqA : A -> A -> Prop. +Variable eqB : B -> B -> Prop. + +(** 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 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 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 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)). + +End Misc. + +Hint InList := Constructors InList. +Hint sort := Constructors sort. +Hint lelistA := Constructors lelistA. +Hints Unfold transpose compat_bool compat_op 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: (In x (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: ~(In x (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)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))(i:A)(f:elt->A->A) + (Empty s) -> (eqA (fold f s i) i). + + Parameter fold_2: + (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))). + + (** Specification of [cardinal] *) + Parameter cardinal_1: (Empty s) -> (cardinal s)=O. + Parameter cardinal_2: + ~(In x s) -> (Add x s s') -> (cardinal s')=(S (cardinal s)). + + 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). + (*i Parameter choose_equal: + (equal s s')=true -> (compare (choose s) (choose s'))=E. i*) + + 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 + cardinal_1 cardinal_2 + 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) + { fold:t -> A -> A | (s,s':t)(a:A) + (eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) + ((Empty s) -> (eqA (fold s a) a)) /\ + ((compat_op E.eq eqA f)->(transpose eqA f) -> + (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }. + + Parameter cardinal : + {cardinal : t -> nat | (s,s':t) + ((Empty s) -> (cardinal s)=O) /\ + ((x:elt) (Add x s s') -> ~(In x s) -> (cardinal s')=(S (cardinal s)))}. + + 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). + Proof. + Intros; Intro; Absurd (O.eq y x); Auto. + Qed. + + Lemma eq_not_lt : (x,y:O.t)(O.eq x y) -> ~(O.lt x y). + Proof. + Intros; Intro; Absurd (O.eq x y); Auto. + Qed. + + Hints Resolve gt_not_eq eq_not_lt. + + Lemma eq_not_gt : (x,y:O.t)(O.eq x y) -> ~(O.lt y x). + Proof. + Auto. + Qed. + + Lemma lt_antirefl : (x:O.t)~(O.lt x x). + Proof. + Intros; Intro; Absurd (O.eq x x); Auto. + Qed. + + Lemma lt_not_gt : (x,y:O.t)(O.lt x y) -> ~(O.lt y x). + Proof. + Intros; Intro; Absurd (O.eq x x); EAuto. + Qed. + + 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). + Proof. + Intros; Case (O.compare x z); Intros; Auto. + Absurd (O.eq x y); EAuto. + Absurd (O.eq z y); EAuto. + Qed. + + Lemma eq_lt : (x,y,z:O.t)(O.eq x y) -> (O.lt y z) -> (O.lt x z). + Proof. + Intros; Case (O.compare x z); Intros; Auto. + Absurd (O.eq y z); EAuto. + Absurd (O.eq x y); EAuto. + Qed. + + 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)). + Proof. + Intros; Case (O.compare x y); Intros H'. + Absurd (O.eq x y); Auto. + Exists H'; Auto. + Absurd (O.eq x y); Auto. + Qed. + + Lemma elim_compare_lt: + (x,y:O.t) (O.lt x y) -> + (EX H : (O.lt x y) | (O.compare x y) = (Lt ? H)). + Proof. + Intros; Case (O.compare x y); Intros H'. + Exists H'; Auto. + Absurd (O.eq x y); Auto. + Absurd (O.lt x x); EAuto. + Qed. + + Lemma elim_compare_gt: + (x,y:O.t) (O.lt y x) -> + (EX H : (O.lt y x) | (O.compare x y) = (Gt ? H)). + Proof. + Intros; Case (O.compare x y); Intros H'. + Absurd (O.lt x x); EAuto. + Absurd (O.eq x y); Auto. + Exists H'; Auto. + Qed. + + 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)}. + Proof. + Intros; Elim (O.compare x y);[Right|Left|Right];Auto. + Qed. + + Lemma lt_dec : (x,y:O.t){(O.lt x y)}+{~(O.lt x y)}. + Proof. + Intros; Elim (O.compare x y);[Left|Right|Right];Auto. + Qed. + + (** 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). + Proof. + Intros; Elim H0; Intuition; EAuto. + Qed. + 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). + Proof. + Intro s; Case s; Constructor; Inversion H0; EAuto. + Qed. + + Lemma Inf_eq : (s:(list O.t))(x,y:O.t)(O.eq x y) -> (Inf y s) -> (Inf x s). + Proof. + Intro s; Case s; Constructor; Inversion H0; EApply eq_lt; EAuto. + Qed. + 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). + Proof. + Induction s. + Intros; Inversion H0. + Intros. + Inversion_clear H0; Inversion_clear H2; Inversion_clear H1. + EApply lt_eq; EAuto. + EAuto. + Qed. + + Lemma Inf_In : (l:(list O.t))(x:O.t) + ((y:O.t)(PolyList.In y l) -> (O.lt x y)) -> (Inf x l). + Proof. + Induction l; Simpl; Intros; Constructor; Auto. + Save. + + Lemma Inf_In_2 : (l:(list O.t))(x:O.t) + ((y:O.t)(In y l) -> (O.lt x y)) -> (Inf x l). + Proof. + Induction l; Simpl; Intros; Constructor; Auto. + Save. + + Lemma In_InList : (l:(list O.t))(x:O.t)(PolyList.In x l) -> (In x l). + Proof. + Induction l; Simpl; Intuition. + Subst; Auto. + Save. + Hints Resolve In_InList. + +End MoreOrderedType. + diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v new file mode 100644 index 0000000000..0c8e8287bd --- /dev/null +++ b/theories/FSets/FSetList.v @@ -0,0 +1,1218 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** This file propose an implementation of the AbstractSet non-dependant + interface by strictly ordered list. *) + +Require Export FSetInterface. + +Set Implicit Arguments. + +(* 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). + +(** In a first time, we provide sets as lists which are not necessarily sorted. + The specs are proved under the additional condition of being sorted. + And the functions outputting sets are proved to preserve this invariant. *) + +Module Raw [X : OrderedType]. + + Module E := X. + Module ME := MoreOrderedType X. + + Definition elt := E.t. + Definition t := (list elt). + + Definition empty : t := []. + + Definition is_empty : t -> bool := [l]if l then true else [_,_]false. + + (** The set operations. *) + + Fixpoint mem [x:elt; s:t] : bool := Cases s of + nil => false + | (cons y l) => Cases (E.compare x y) of + (Lt _) => false + | (Eq _) => true + | (Gt _) => (mem x l) + end + end. + + Fixpoint add [x:elt; s:t] : t := Cases s of + nil => x::[] + | (cons y l) => Cases (E.compare x y) of + (Lt _) => x::s + | (Eq _) => s + | (Gt _) => y::(add x l) + end + end. + + Definition singleton : elt -> t := [x] x::[]. + + Fixpoint remove [x:elt; s:t] : t := Cases s of + nil => [] + | (cons y l) => Cases (E.compare x y) of + (Lt _) => s + | (Eq _) => l + | (Gt _) => y::(remove x l) + end + end. + + Fixpoint union [s:t] : t -> t := Cases s of + nil => [s']s' + | (cons x l) => + Fix union_aux { union_aux / 1 : t -> t := [s']Cases s' of + nil => s + | (cons x' l') => Cases (E.compare x x') of + (Lt _ ) => x::(union l s') + | (Eq _ ) => x::(union l l') + | (Gt _) => x'::(union_aux l') + end + end} + end. + + Fixpoint inter [s:t] : t -> t := Cases s of + nil => [_] [] + | (cons x l) => + Fix inter_aux { inter_aux / 1 : t -> t := [s']Cases s' of + nil => [] + | (cons x' l') => Cases (E.compare x x') of + (Lt _ ) => (inter l s') + | (Eq _ ) => x::(inter l l') + | (Gt _) => (inter_aux l') + end + end} + end. + + Fixpoint diff [s:t] : t -> t := Cases s of + nil => [_] [] + | (cons x l) => + Fix diff_aux { diff_aux / 1 : t -> t := [s']Cases s' of + nil => s + | (cons x' l') => Cases (E.compare x x') of + (Lt _ ) => x::(diff l s') + | (Eq _ ) => (diff l l') + | (Gt _) => (diff_aux l') + end + end} + end. + + Fixpoint equal [s:t] : t -> bool := [s':t]Cases s s' of + nil nil => true + | (cons x l) (cons x' l') => Cases (E.compare x x') of + (Eq _) => (equal l l') + | _ => false + end + | _ _ => false + end. + + Fixpoint subset [s,s':t] : bool := Cases s s' of + nil _ => true + | (cons x l) (cons x' l') => Cases (E.compare x x') of + (Lt _) => false + | (Eq _) => (subset l l') + | (Gt _) => (subset s l') + end + | _ _ => false + end. + + Fixpoint fold [B:Set; f:elt->B->B; s:t] : B -> B := [i]Cases s of + nil => i + | (cons x l) => (f x (fold f l i)) + end. + + Fixpoint filter [f:elt->bool; s:t] : t := Cases s of + nil => [] + | (cons x l) => if (f x) then x::(filter f l) else (filter f l) + end. + + Fixpoint for_all [f:elt->bool; s:t] : bool := Cases s of + nil => true + | (cons x l) => if (f x) then (for_all f l) else false + end. + + Fixpoint exists [f:elt->bool; s:t] : bool := Cases s of + nil => false + | (cons x l) => if (f x) then true else (exists f l) + end. + + Fixpoint partition [f:elt->bool; s:t] : t*t := Cases s of + nil => ([],[]) + | (cons x l) => let (s1,s2) = (partition f l) in + if (f x) then (x::s1,s2) else (s1,x::s2) + end. + + Definition cardinal : t -> nat := [s](fold [_]S s O). + + Definition elements : t -> (list elt) := [x]x. + + Definition min_elt : t -> (option elt) := [s]Cases s of + nil => (None ?) + | (cons x _) => (Some ? x) + end. + + Fixpoint max_elt [s:t] : (option elt) := Cases s of + nil => (None ?) + | (cons x nil) => (Some ? x) + | (cons _ l) => (max_elt l) + end. + + Definition choose := min_elt. + + (** Proofs of set operation specifications. *) + + Definition In : elt -> t -> Prop := (InList E.eq). + Notation "'Sort' l" := (sort E.lt l) (at level 10, l at level 8). + Notation "'Inf' x l" := (lelistA E.lt x l) (at level 10, x,l at level 8). + Notation "'In' x l" := (InList E.eq x l) (at level 10, x,l at level 8). + + 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_eq: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s) := ME.In_eq. + Definition Inf_lt : (s:t)(x,y:elt)(E.lt x y) -> (Inf y s) -> (Inf x s) := ME.Inf_lt. + Definition Inf_eq : (s:t)(x,y:elt)(E.eq x y) -> (Inf y s) -> (Inf x s) := ME.Inf_eq. + Definition In_sort : (s:t)(x,a:elt)(Inf a s) -> (In x s) -> (Sort s) -> (E.lt a x) := ME.In_sort. + Hints Resolve Inf_lt Inf_eq. + Hints Immediate In_eq. + + Lemma mem_1: (s:t)(Hs:(Sort s))(x:elt)(In x s) -> (mem x s)=true. + Proof. + Induction s; Intros. + Inversion H. + Inversion_clear Hs. + Inversion_clear H0. + Simpl; Replace E.compare with X.compare; Auto. + Elim (!ME.elim_compare_eq x a); [Intros A B; Rewrite B; Auto | Auto]. + Simpl; Replace E.compare with X.compare; Auto. + Elim (!ME.elim_compare_gt x a); [Intros A B; Rewrite B; Auto | Auto]. + EApply In_sort; EAuto. + Qed. + + Lemma mem_2: (s:t)(x:elt)(mem x s)=true -> (In x s). + Proof. + Induction s. + Intros; Inversion H. + Intros a l Hrec x. + Simpl; Elim (E.compare x a); Ground. + Inversion H. + Qed. + + Lemma add_Inf : (s:t)(x,a:elt)(Inf a s)->(E.lt a x)->(Inf a (add x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition; Inversion H0; Intuition. + Qed. + Hints Resolve add_Inf. + + Lemma add_sort : (s:t)(Hs:(Sort s))(x:elt)(Sort (add x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs; Auto. + Qed. + + Lemma add_1 : (s:t)(Hs:(Sort s))(x:elt)(In x (add x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs; Ground. + Qed. + + Lemma add_2 : (s:t)(Hs:(Sort s))(x,y:elt)(In y s) -> (In y (add x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition. + Inversion_clear Hs; Inversion_clear H0; EAuto. + Qed. + + Lemma add_3 : (s:t)(Hs:(Sort s))(x,y:elt) + ~(E.eq x y) -> (In y (add x s)) -> (In y s). + Proof. + Induction s. + Simpl; Intuition. + Inversion_clear H0; Ground; Absurd (E.eq x y); Auto. + Simpl; Intros a l Hrec Hs x y; Case (E.compare x a); Intros; + Inversion_clear H0; Inversion_clear Hs; Ground; Absurd (E.eq x y); Auto. + Qed. + + Lemma remove_Inf : (s:t)(Hs:(Sort s))(x,a:elt)(Inf a s)-> + (Inf a (remove x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear H0; Ground. + Inversion_clear Hs; Ground; EAuto. + Qed. + Hints Resolve remove_Inf. + + Lemma remove_sort : (s:t)(Hs:(Sort s))(x:elt)(Sort (remove x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs; Auto. + Qed. + + Lemma remove_1 : (s:t)(Hs:(Sort s))(x:elt)~(In x (remove x s)). + Proof. + Induction s. + Simpl; Red; Intros; Inversion H. + Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs. + Inversion_clear H0. + Absurd (E.eq x a); Auto. + Absurd (E.lt a x); Auto; EApply In_sort; EAuto. + Absurd (E.lt a x); Auto; EApply In_sort; EAuto. + Inversion_clear H0; Ground. + Absurd (E.eq x a); Auto. + Qed. + + Lemma remove_2 : (s:t)(Hs:(Sort s))(x,y:elt) + ~(E.eq x y) -> (In y s) -> (In y (remove x s)). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros; Case (E.compare x a); Intuition; + Inversion_clear Hs; Inversion_clear H1; Auto. + Absurd (E.eq x y); EAuto. + Qed. + + Lemma remove_3 : (s:t)(Hs:(Sort s))(x,y:elt)(In y (remove x s)) -> (In y s). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros a l Hrec Hs x y; Case (E.compare x a); Intuition. + Inversion_clear Hs; Inversion_clear H; Ground. + Qed. + + Lemma singleton_sort : (x:elt)(Sort (singleton x)). + Proof. + Unfold singleton; Simpl; Ground. + Qed. + + Lemma singleton_1 : (x,y:elt)(In y (singleton x)) -> (E.eq x y). + Proof. + Unfold singleton; Simpl; Intuition. + Inversion_clear H; Auto; Inversion H0. + Qed. + + Lemma singleton_2 : (x,y:elt)(E.eq x y) -> (In y (singleton x)). + Proof. + Unfold singleton; Simpl; Intuition. + Qed. + + Tactic Definition DoubleInd := + Induction s; + [Simpl; Auto; Try Solve [ Intros; Inversion H ] | + Intros x l Hrec; + Induction s'; + [Simpl; Auto; Try Solve [ Intros; Inversion H ] | + Intros x' l' Hrec' Hs Hs'; Inversion Hs; Inversion Hs'; Subst; Simpl]]. + + Lemma union_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt) + (Inf a s) -> (Inf a s') -> (Inf a (union s s')). + Proof. + DoubleInd. + Intros i His His'; Inversion_clear His; Inversion_clear His'. + Case (E.compare x x'); Ground. + Qed. + Hints Resolve union_Inf. + + Lemma union_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (union s s')). + Proof. + DoubleInd; Case (E.compare x x'); Intuition; Constructor; Auto. + EAuto. + Change (Inf x' (union x::l l')); Ground. + Qed. + + Lemma union_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x (union s s')) -> (In x s)\/(In x s'). + Proof. + DoubleInd; Case (E.compare x x'); Intuition; Inversion_clear H; Intuition. + Elim (Hrec (x'::l') H1 Hs' x0); Intuition. + Elim (Hrec l' H1 H5 x0); Intuition. + Elim (H0 x0); Intuition. + Qed. + + Lemma union_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x s) -> (In x (union s s')). + Proof. + DoubleInd. + Intros i Hi; Case (E.compare x x'); Intuition; Inversion_clear Hi; Auto. + Qed. + + Lemma union_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x s') -> (In x (union s s')). + Proof. + DoubleInd. + Intros i Hi; Case (E.compare x x'); Inversion_clear Hi; Intuition; EAuto. + Qed. + + Lemma inter_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt) + (Inf a s) -> (Inf a s') -> (Inf a (inter s s')). + Proof. + DoubleInd. + Intros i His His'; Inversion His; Inversion His'; Subst. + Case (E.compare x x'); Intuition; EAuto. + Qed. + Hints Resolve inter_Inf. + + Lemma inter_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (inter s s')). + Proof. + DoubleInd; Case (E.compare x x'); EAuto. + Qed. + + Lemma inter_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x (inter s s')) -> (In x s). + Proof. + DoubleInd; Case (E.compare x x'); Intuition. + EAuto. + Inversion_clear H; EAuto. + Qed. + + Lemma inter_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x (inter s s')) -> (In x s'). + Proof. + DoubleInd; Case (E.compare x x'); Intuition; Inversion_clear H; EAuto. + Qed. + + Lemma inter_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x s) -> (In x s') -> (In x (inter s s')). + Proof. + DoubleInd. + Intros i His His'; Elim (E.compare x x'); Intuition. + + Inversion_clear His. + Absurd (E.lt i x); EAuto. + Apply In_sort with (x'::l'); Auto. + Constructor; EApply ME.eq_lt; EAuto. + EApply In_eq; EAuto. + EApply In_eq; EAuto. + + Inversion_clear His; [ EAuto | Inversion_clear His' ]; EAuto. + + Change (In i (inter x::l l')). + Inversion_clear His'. + Absurd (E.lt i x'); EAuto. + Apply In_sort with (x::l); Auto. + Constructor; EApply ME.eq_lt; EAuto. + EApply In_eq; EAuto. + EApply In_eq; EAuto. + Qed. + + Lemma diff_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt) + (Inf a s) -> (Inf a s') -> (Inf a (diff s s')). + Proof. + DoubleInd. + Intros i His His'; Inversion His; Inversion His'. + Case (E.compare x x'); Intuition;EAuto. + Qed. + Hints Resolve diff_Inf. + + Lemma diff_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (diff s s')). + Proof. + DoubleInd; Case (E.compare x x'); EAuto. + Qed. + + Lemma diff_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x (diff s s')) -> (In x s). + Proof. + DoubleInd; Case (E.compare x x'); Intuition. + Inversion_clear H; EAuto. + EAuto. + Qed. + + Lemma diff_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x (diff s s')) -> ~(In x s'). + Proof. + DoubleInd. + Intros; Intro Abs; Inversion Abs. + Case (E.compare x x'); Intuition. + + Inversion_clear H. + Absurd (E.lt x x); EAuto. + Apply In_sort with (x'::l'); Auto. + EApply In_eq; EAuto. + EAuto. + + Inversion_clear H3. + Generalize (diff_1 H1 H5 H); Intros. + Absurd (E.lt x x0); EAuto. + Apply In_sort with l; EAuto. + EAuto. + + Inversion_clear H3. + Generalize (diff_1 Hs H5 H); Intros. + Absurd (E.lt x' x'); EAuto. + Apply In_sort with (x::l); Auto. + EApply In_eq; EAuto. + EAuto. + Qed. + + Lemma diff_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + (In x s) -> ~(In x s') -> (In x (diff s s')). + Proof. + DoubleInd. + Intros i His His'; Elim (E.compare x x'); Intuition; Inversion_clear His. + EAuto. + EAuto. + Elim His'; EAuto. + EAuto. + Qed. + + Lemma equal_1: (s,s':t)(Hs:(Sort s))(Hs':(Sort s')) + (Equal s s') -> (equal s s')=true. + Proof. + Induction s; Unfold Equal. + Intro s'; Case s'; Auto. + Simpl; Intuition. + Elim (H e); Intros; Assert A : (In e []); Auto; Inversion A. + Intros x l Hrec s'. + Case s'. + Intros; Elim (H x); Intros; Assert A : (In x []); Auto; Inversion A. + Intros x' l' Hs Hs'; Inversion Hs; Inversion Hs'; Subst. + Simpl; Case (E.compare x); Intros; Auto. + + Elim (H x); Intros. + Assert A : (In x x'::l'); Auto; Inversion_clear A. + Absurd (E.eq x x'); EAuto. + Absurd (E.lt x' x); Auto. + Apply In_sort with l';EAuto. + + Apply Hrec; Intuition; Elim (H a); Intros. + Assert A : (In a x'::l'); Auto; Inversion_clear A; Auto. + Absurd (E.lt x' x); Auto. + Apply In_sort with l;Auto; + [ Apply Inf_eq with x;Auto | Apply In_eq with a; EAuto ]. + Assert A : (In a x::l); Auto; Inversion_clear A; Auto. + Absurd (E.lt x x'); Auto. + Apply In_sort with l';Auto; + [ Apply Inf_eq with x';Auto | Apply In_eq with a; EAuto ]. + + Elim (H x'); Intros. + Assert A : (In x' x::l); Auto; Inversion_clear A. + Absurd (E.eq x' x); EAuto. + Absurd (E.lt x x'); Auto. + Apply In_sort with l;EAuto. + Qed. + + Lemma equal_2: (s,s':t)(equal s s')=true -> (Equal s s'). + Proof. + Induction s; Unfold Equal. + Intro s'; Case s'; Intros. + Intuition. + Simpl in H; Discriminate H. + Intros x l Hrec s'. + Case s'. + Intros; Simpl in H; Discriminate H. + Intros x' l'; Simpl; Case (E.compare x); Intros; Auto. + Discriminate H. + Elim (Hrec l' H a); Intuition; Inversion_clear H2; EAuto. + Discriminate H. + Qed. + + Lemma subset_1: (s,s':t)(Hs:(Sort s))(Hs':(Sort s')) + (Subset s s') -> (subset s s')=true. + Proof. + Intros s s'; Generalize s' s; Clear s s'. + Induction s'; Unfold Subset. + Intro s; Case s; Auto. + Intros; Elim (H e); Intros; Assert A : (In e []); Auto; Inversion A. + Intros x' l' Hrec s; Case s. + Simpl; Auto. + Intros x l Hs Hs'; Inversion Hs; Inversion Hs'; Subst. + Simpl; Case (E.compare x); Intros; Auto. + + Assert A : (In x x'::l'); Auto; Inversion_clear A. + Absurd (E.eq x x'); EAuto. + Absurd (E.lt x' x); Auto. + Apply In_sort with l';EAuto. + + Apply Hrec; Intuition. + Assert A : (In a x'::l'); Auto; Inversion_clear A; Auto. + Absurd (E.lt x' x); Auto. + Apply In_sort with l;Auto; [ Apply Inf_eq with x;Auto | Apply In_eq with a; EAuto ]. + + Apply Hrec; Intuition. + Assert A : (In a x'::l'); Auto; Inversion_clear A; Auto. + Inversion_clear H0. + Absurd (E.lt x' x); EAuto. + Absurd (E.lt x x'); Auto. + Apply In_sort with l;EAuto. + Qed. + + Lemma subset_2: (s,s':t)(subset s s')=true -> (Subset s s'). + Proof. + Intros s s'; Generalize s' s; Clear s s'. + Induction s'; Unfold Subset. + Intro s; Case s; Auto. + Simpl; Intros; Discriminate H. + Intros x' l' Hrec s; Case s. + Intros; Inversion H0. + Intros x l; Simpl; Case (E.compare x); Intros; Auto. + Discriminate H. + Inversion_clear H0; EAuto. + EAuto. + Qed. + + Lemma empty_sort : (Sort empty). + Proof. + Unfold empty; Constructor. + Qed. + + Lemma empty_1 : (Empty empty). + Proof. + Unfold Empty empty; Intuition; Inversion H. + Qed. + + Lemma is_empty_1 : (s:t)(Empty s) -> (is_empty s)=true. + Proof. + Unfold Empty; Intro s; Case s; Simpl; Intuition. + Elim (H e); Auto. + Qed. + + Lemma is_empty_2 : (s:t)(is_empty s)=true -> (Empty s). + Proof. + Unfold Empty; Intro s; Case s; Simpl; Intuition; Inversion H0. + Qed. + + Lemma elements_1: (s:t)(x:elt)(In x s) -> (InList E.eq x (elements s)). + Proof. + Unfold elements; Auto. + Qed. + + Lemma elements_2: (s:t)(x:elt)(InList E.eq x (elements s)) -> (In x s). + Proof. + Unfold elements; Auto. + Qed. + + Lemma elements_3: (s:t)(Hs:(Sort s))(sort E.lt (elements s)). + Proof. + Unfold elements; Auto. + Qed. + + Lemma min_elt_1: (s:t)(x:elt)(min_elt s) = (Some ? x) -> (In x s). + Proof. + Intro s; Case s; Simpl; Intros; Inversion H; Auto. + Qed. + + Lemma min_elt_2: (s:t)(Hs:(Sort s))(x,y:elt) + (min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x). + Proof. + Induction s; Simpl. + Intros; Inversion H. + Intros a l; Case l; Intros; Inversion H0; Inversion_clear H1; Subst. + EAuto. + Inversion H2. + EAuto. + Inversion_clear Hs. + Inversion_clear H3. + Intro; Absurd (E.lt y e); EAuto. + Qed. + + Lemma min_elt_3: (s:t)(min_elt s) = (None ?) -> (Empty s). + Proof. + Unfold Empty; Intro s; Case s; Simpl; Intuition; Inversion H; Inversion H0. + Qed. + + Lemma max_elt_1: (s:t)(x:elt)(max_elt s) = (Some ? x) -> (In x s). + Proof. + Induction s; Simpl. + Intros; Inversion H. + Intros x l; Case l; Simpl. + Intuition. + Inversion H0; Auto. + EAuto. + Qed. + + Lemma max_elt_2: (s:t)(Hs:(Sort s))(x,y:elt) + (max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y). + Proof. + Induction s; Simpl. + Intros; Inversion H. + Intros x l; Case l; Simpl. + Intuition. + Inversion H0; Subst. + Inversion_clear H1. + Absurd (E.eq y x0); Auto. + Inversion H3. + Intros; Inversion_clear Hs; Inversion_clear H3; Inversion_clear H1. + Assert ~(E.lt x0 e). + EApply H; EAuto. + Intro. + Elim H1; Apply E.lt_trans with x; Auto; EApply ME.lt_eq; EAuto. + EApply H;EAuto. + Qed. + + Lemma max_elt_3: (s:t)(max_elt s) = (None ?) -> (Empty s). + Proof. + Unfold Empty; Induction s; Simpl. + Red; Intros; Inversion H0. + Intros x l; Case l; Simpl; Intros. + Inversion H0. + Elim (H H0 e); Auto. + Qed. + + Definition choose_1: + (s:t)(x:elt)(choose s)=(Some ? x) -> (In x s) + := min_elt_1. + + Definition choose_2: (s:t)(choose s)=(None ?) -> (Empty s) + := min_elt_3. + + 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). + Proof. + Unfold Empty; Intro s; Case s; Intros; Simpl; Intuition; Elim (H e); Auto. + Qed. + + Lemma fold_equal : + (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(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) -> (Equal s s') -> + (eqA (fold f s i) (fold f s' i)). + Proof. + Induction s; Unfold Equal; Simpl. + + Intro s'; Case s'; Intuition. + Intros. + Elim (H1 e); Intuition. + Assert X : (In e []); Auto; Inversion X. + + Intros x l Hrec s'; Case s'. + Intros. + Elim (H1 x); Intuition. + Assert X : (In x []); Auto; Inversion X. + Simpl; Intros x' l' Hs Hs' a; Intros. + Inversion_clear Hs; Inversion_clear Hs'. + Assert (E.eq x x'). + Assert (In x x'::l'). + Elim (H1 x); Auto. + Assert (In x' x::l). + Elim (H1 x'); Auto. + Inversion_clear H6; Auto. + Inversion_clear H7; Auto. + Absurd (E.lt x x'). + Apply ME.lt_not_gt. + Apply In_sort with l'; EAuto. + Apply In_sort with l; EAuto. + Apply H; Auto. + Apply (Hrec l' H2 H4 a eqA); Auto. + (* To prove (Equal l l') *) + Intuition. + Elim (H1 a0); Intros. + Assert (In a0 x'::l'). Auto. + Inversion_clear H10; Auto. + Intros; Absurd (E.lt x x'); EAuto. + Apply In_sort with l; EAuto. + Elim (H1 a0); Intros. + Assert (In a0 x::l). Auto. + Inversion_clear H10; Auto. + Intros; Absurd (E.lt x' x); EAuto. + Apply In_sort with l'; EAuto. + Qed. + + Lemma fold_2 : + (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(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))). + Proof. + Induction s; Unfold Add; Simpl. + + Intro s'; Case s'. + Intros. + Elim (H2 x); Intuition. + Assert X : (In x []); Auto; Inversion X. + Simpl; Intros. + Inversion_clear Hs'. + Apply H; Auto. + Elim (H2 e);Intuition. + Elim H5; Auto. + Intros X; Inversion X. + Apply fold_1; Auto. + Unfold Empty; Intuition. + Assert (y:elt)(In y e::l) -> (E.eq y x). + Intros; Elim (H2 y); Intuition; Inversion H7. + Assert (E.eq a x); [Ground | Idtac]. + Assert (E.eq e x); [Ground | Idtac]. + Absurd (E.lt a e); EAuto. + Apply In_sort with l; EAuto. Apply In_eq with a; EAuto. + + Intros x l Hrec s'; Case s'. + Intros. + Elim (H2 x0); Intuition. + Assert X : (In x0 []); Auto; Inversion X. + Simpl; Intros x' l' Hs Hs' a; Intros. + Inversion Hs; Inversion Hs'. + Assert (In a x'::l');[Ground|Idtac]. + (* 2 cases: x'=a or x'<a *) + (* first, x'=a *) + Inversion_clear H11. + Apply H; Auto. + Change (eqA (fold f l' i) (fold f (x::l) i)). + Apply (!fold_equal l' (x::l) H9 Hs A eqA); Auto. + (* To prove that (Equal l' (x::l)) *) + Unfold Equal. + Intuition. + Elim (H2 a2); Intros. + Elim H13; Auto. + Intros. + Absurd (E.lt x' a2); EAuto; Apply In_sort with l'; EAuto. + Elim (H2 a2); Intros. + Assert (In a2 x'::l'); Auto. + Inversion_clear H15; Auto. + Elim H1; Apply In_eq with a2; EAuto. + (* second, x'<a *) + Assert (E.lt x' a). + Apply In_sort with l'; EAuto. + Assert ~(E.eq a x). + Intro; Elim H1; Auto. + Assert (E.eq x x'). + Assert (In x x'::l'). + Elim (H2 x); Auto. + Assert (In x' x::l). + Elim (H2 x'); Intuition. + Elim H15; Auto. + Intros; Absurd (E.eq x' a); EAuto. + Inversion_clear H14; Auto. + Inversion_clear H15; Auto. + Absurd (E.lt x x'). + Apply ME.lt_not_gt. + Apply In_sort with l'; EAuto. + Apply In_sort with l; EAuto. + Apply (Seq_trans ? ? st) with (f x (f a (fold f l i))). + 2: Apply H0. + Apply H; Auto. + Apply (Hrec l' H5 H9 a A eqA); Clear Hrec; Auto. + (* To prove (Add a l l') *) + Intuition. + Elim (H2 y); Intros. + Elim H16; Auto; Intros. + Inversion_clear H18. + Absurd (E.lt x' y); EAuto; Apply In_sort with l'; EAuto. + Right; Auto. + Apply In_eq with a; Auto. + Elim (H2 y); Intuition. + Assert (In y x'::l'); Auto. + Inversion_clear H17; Auto. + Absurd (E.lt x y); EAuto; Apply In_sort with l; EAuto. + Qed. + + Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O. + Proof. + Unfold cardinal; Intros; Apply fold_1; Auto. + Intuition EAuto; Transitivity y; Auto. + Qed. + + Lemma cardinal_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) + ~(In x s) -> (Add x s s') -> (cardinal s') = (S (cardinal s)). + Proof. + Unfold cardinal; Intros. + Assert (compat_op E.eq (eq ?) [_]S). + Unfold compat_op; Auto. + Assert (transpose (eq ?) [_:elt]S). + Unfold transpose; Auto. + Refine (!fold_2 s s' Hs Hs' x nat (eq ?) ? O [_]S H1 H2 H H0). + Intuition EAuto; Transitivity y; Auto. + Qed. + + Lemma filter_Inf : + (s:t)(Hs:(Sort s))(x:elt)(f:elt->bool)(Inf x s) -> (Inf x (filter f s)). + Proof. + Induction s; Simpl. + Intuition. + Intros x l Hrec Hs a f Ha; Inversion_clear Hs; Inversion Ha. + Case (f x); [Constructor; Auto | EAuto]. + Qed. + + Lemma filter_sort : (s:t)(Hs:(Sort s))(f:elt->bool)(Sort (filter f s)). + Proof. + Induction s; Simpl. + Auto. + Intros x l Hrec Hs f; Inversion_clear Hs. + Case (f x); Auto. + Constructor; Auto. + Apply filter_Inf; Auto. + Qed. + + Lemma filter_1: (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) -> + (In x (filter f s)) -> (In x s). + Proof. + Induction s; Simpl. + Intros; Inversion H0. + Intros x l Hrec a f Hf. + Case (f x); Simpl; Ground. + Inversion H; Ground. + Qed. + + Lemma filter_2: + (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->(In x (filter f s)) -> + (f x)=true. + Proof. + Induction s; Simpl. + Intros; Inversion H0. + Intros x l Hrec a f Hf. + Generalize (Hf x); Case (f x); Simpl; Ground. + Inversion H0; Ground. + Symmetry; Ground. + Qed. + + 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)). + Proof. + Induction s; Simpl. + Intros; Inversion H0. + Intros x l Hrec a f Hf. + Generalize (Hf x); Case (f x); Simpl; Ground; Inversion H0; Ground. + Rewrite <- (H a) in H1; Auto; Discriminate H1. + Qed. + + 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. + Proof. + Induction s; Simpl; Auto; Unfold For_all. + Intros x l Hrec f Hf. + Generalize (Hf x); Case (f x); Simpl; Ground. + Rewrite (H x); Auto. + Qed. + + 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). + Proof. + Induction s; Simpl; Auto; Unfold For_all. + Intros; Inversion H1. + Intros x l Hrec f Hf. + Intros A a; Intros. + Assert (f x)=true. + Generalize A; Case (f x); Auto. + Rewrite H0 in A; Simpl in A. + Inversion H; Ground. + Rewrite (Hf a x); Auto. + Qed. + + Lemma exists_1: + (s:t)(f:elt->bool)(compat_bool E.eq f) -> (Exists [x](f x)=true s) -> + (exists f s)=true. + Proof. + Induction s; Simpl; Auto; Unfold Exists. + Intros. + Elim H0; Intuition. + Inversion H2. + Intros x l Hrec f Hf. + Generalize (Hf x); Case (f x); Simpl; Ground. + Inversion_clear H0. + Absurd (false=true); Auto with bool. + Rewrite (H x); Auto. + Rewrite <- H1. + Ground. + Ground. + Qed. + + Lemma exists_2: + (s:t)(f:elt->bool)(compat_bool E.eq f) -> (exists f s)=true -> + (Exists [x](f x)=true s). + Proof. + Induction s; Simpl; Auto; Unfold Exists. + Intros; Discriminate. + Intros x l Hrec f Hf. + Generalize (refl_equal ? (f x)); Pattern -1 (f x); Case (f x). + Intros; Exists x; Auto. + Intros; Elim (Hrec f); Auto; Ground. + Qed. + + Lemma partition_Inf_1 : + (s:t)(Hs:(Sort s))(f:elt->bool)(x:elt)(Inf x s) -> + (Inf x (fst ? ? (partition f s))). + Proof. + Induction s; Simpl. + Intuition. + Intros x l Hrec Hs f a Ha; Inversion_clear Hs; Inversion Ha. + Generalize (Hrec H f a). + Case (f x); Case (partition f l); Simpl. + Intros; Constructor; Auto. + EAuto. + Qed. + + Lemma partition_Inf_2 : + (s:t)(Hs:(Sort s))(f:elt->bool)(x:elt)(Inf x s) -> + (Inf x (snd ? ? (partition f s))). + Proof. + Induction s; Simpl. + Intuition. + Intros x l Hrec Hs f a Ha; Inversion_clear Hs; Inversion Ha. + Generalize (Hrec H f a). + Case (f x); Case (partition f l); Simpl. + EAuto. + Intros; Constructor; Auto. + Qed. + + Lemma partition_sort_1 : (s:t)(Hs:(Sort s))(f:elt->bool) + (Sort (fst ? ? (partition f s))). + Proof. + Induction s; Simpl. + Auto. + Intros x l Hrec Hs f; Inversion_clear Hs. + Generalize (Hrec H f); Generalize (partition_Inf_1 H f). + Case (f x); Case (partition f l); Simpl; Auto. + Qed. + + Lemma partition_sort_2 : (s:t)(Hs:(Sort s))(f:elt->bool) + (Sort (snd ? ? (partition f s))). + Proof. + Induction s; Simpl. + Auto. + Intros x l Hrec Hs f; Inversion_clear Hs. + Generalize (Hrec H f); Generalize (partition_Inf_2 H f). + Case (f x); Case (partition f l); Simpl; Auto. + Qed. + + Lemma partition_1: + (s:t)(f:elt->bool)(compat_bool E.eq f) -> + (Equal (fst ? ? (partition f s)) (filter f s)). + Proof. + Induction s; Simpl; Auto; Unfold Equal. + Ground. + Intros x l Hrec f Hf. + Generalize (Hrec f Hf); Clear Hrec. + Case (partition f l); Intros s1 s2; Simpl; Intros. + Case (f x); Simpl; Ground; Inversion H0; Intros; Ground. + Qed. + + Lemma partition_2: + (s:t)(f:elt->bool)(compat_bool E.eq f) -> + (Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)). + Proof. + Induction s; Simpl; Auto; Unfold Equal. + Ground. + Intros x l Hrec f Hf. + Generalize (Hrec f Hf); Clear Hrec. + Case (partition f l); Intros s1 s2; Simpl; Intros. + Case (f x); Simpl; Ground; Inversion H0; Intros; Ground. + Qed. + + Definition eq : t -> t -> Prop := Equal. + + Lemma eq_refl: (s:t)(eq s s). + Proof. + Unfold eq Equal; Intuition. + Qed. + + Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s). + Proof. + Unfold eq Equal; Ground. + Qed. + + Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s''). + Proof. + Unfold eq Equal; Ground. + Qed. + + Inductive lt : t -> t -> Prop := + lt_nil : (x:elt)(s:t)(lt [] (x::s)) + | lt_cons_lt : (x,y:elt)(s,s':t)(E.lt x y) -> (lt (x::s) (y::s')) + | lt_cons_eq : (x,y:elt)(s,s':t)(E.eq x y) -> (lt s s') -> (lt (x::s) (y::s')). + Hint lt := Constructors lt. + + Lemma lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s''). + Proof. + Intros s s' s'' H; Generalize s''; Clear s''; Elim H. + Intros x l s'' H'; Inversion_clear H'; Auto. + Intros x x' l l' E s'' H'; Inversion_clear H'; Auto. + EAuto. + Constructor 2; Apply ME.lt_eq with x'; Auto. + Intros. + Inversion_clear H3. + Constructor 2; Apply ME.eq_lt with y; Auto. + Constructor 3; EAuto. + Qed. + + Lemma lt_not_eq : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(lt s s') -> ~(eq s s'). + Proof. + Unfold eq Equal. + Intros s s' Hs Hs' H; Generalize Hs Hs'; Clear Hs Hs'; Elim H; Intros; Intro. + Elim (H0 x); Intros. + Assert X : (In x []); Auto; Inversion X. + Inversion_clear Hs; Inversion_clear Hs'. + Elim (H1 x); Intros. + Assert X : (In x y::s'0); Auto; Inversion_clear X. + Absurd (E.eq x y); EAuto. + Absurd (E.lt y x); Auto. + EApply In_sort; EAuto. + Inversion_clear Hs; Inversion_clear Hs'. + Elim H2; Auto; Intuition. + Elim (H3 a); Intros. + Assert X: (In a y::s'0); Auto; Inversion_clear X; Auto. + Absurd (E.lt x a); EAuto. + EApply In_sort with s0; EAuto. + Elim (H3 a); Intros. + Assert X: (In a x::s0); Auto; Inversion_clear X; Auto. + Absurd (E.lt y a); EAuto. + EApply In_sort with s'0; EAuto. + Qed. + + Definition compare : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Compare lt eq s s'). + Proof. + Induction s. + Intros; Case s'. + Constructor 2; Apply eq_refl. + Constructor 1; Auto. + Intros a l Hrec s'; Case s'. + Constructor 3; Auto. + Intros a' l' Hs Hs'. + Case (E.compare a a'); [ Constructor 1 | Idtac | Constructor 3 ]; Auto. + Elim (Hrec l'); [ Constructor 1 | Constructor 2 | Constructor 3 | Inversion Hs | Inversion Hs']; Auto. + Generalize e; Unfold eq Equal; Intuition; + Inversion_clear H; EAuto; Elim (e1 a0); Auto. + Defined. + +End Raw. + +(** Now, in order to really provide a functor implementing S, we + need to encapsulate everything into a type of strictly ordered lists. *) + +Module Make [X:OrderedType] <: S with Module E := X. + + Module E := X. + Module Raw := (Raw X). + + Record slist : Set := { this :> Raw.t ; sorted : (sort E.lt this) }. + Definition t := slist. + Definition elt := X.t. + + Definition In := [x:elt;s:t](Raw.In x s). + 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 := [s:t](!Raw.In_eq s). + + Definition mem := [x:elt;s:t](Raw.mem x s). + Definition mem_1 := [s:t](Raw.mem_1 (sorted s)). + Definition mem_2 := [s:t](!Raw.mem_2 s). + + Definition add := [x,s](Build_slist (Raw.add_sort (sorted s) x)). + Definition add_1 := [s:t](Raw.add_1 (sorted s)). + Definition add_2 := [s:t](Raw.add_2 (sorted s)). + Definition add_3 := [s:t](Raw.add_3 (sorted s)). + + Definition remove := [x,s](Build_slist (Raw.remove_sort (sorted s) x)). + Definition remove_1 := [s:t](Raw.remove_1 (sorted s)). + Definition remove_2 := [s:t](Raw.remove_2 (sorted s)). + Definition remove_3 := [s:t](Raw.remove_3 (sorted s)). + + Definition singleton := [x](Build_slist (Raw.singleton_sort x)). + Definition singleton_1 := Raw.singleton_1. + Definition singleton_2 := Raw.singleton_2. + + Definition union := [s,s':t](Build_slist (Raw.union_sort (sorted s) (sorted s'))). + Definition union_1 := [s,s':t](Raw.union_1 (sorted s) (sorted s')). + Definition union_2 := [s,s':t](Raw.union_2 (sorted s) (sorted s')). + Definition union_3 := [s,s':t](Raw.union_3 (sorted s) (sorted s')). + + Definition inter :=[s,s':t](Build_slist (Raw.inter_sort (sorted s) (sorted s'))). + Definition inter_1 := [s,s':t](Raw.inter_1 (sorted s) (sorted s')). + Definition inter_2 := [s,s':t](Raw.inter_2 (sorted s) (sorted s')). + Definition inter_3 := [s,s':t](Raw.inter_3 (sorted s) (sorted s')). + + Definition diff :=[s,s':t](Build_slist (Raw.diff_sort (sorted s) (sorted s'))). + Definition diff_1 := [s,s':t](Raw.diff_1 (sorted s) (sorted s')). + Definition diff_2 := [s,s':t](Raw.diff_2 (sorted s) (sorted s')). + Definition diff_3 := [s,s':t](Raw.diff_3 (sorted s) (sorted s')). + + Definition equal := [s,s':t](Raw.equal s s'). + Definition equal_1 := [s,s':t](Raw.equal_1 (sorted s) (sorted s')). + Definition equal_2 := [s,s':t](!Raw.equal_2 s s'). + + Definition subset := [s,s':t](Raw.subset s s'). + Definition subset_1 := [s,s':t](Raw.subset_1 (sorted s) (sorted s')). + Definition subset_2 := [s,s':t](!Raw.subset_2 s s'). + + Definition empty := (Build_slist Raw.empty_sort). + Definition empty_1 := Raw.empty_1. + + Definition is_empty := [s:t](Raw.is_empty s). + Definition is_empty_1 := [s:t](!Raw.is_empty_1 s). + Definition is_empty_2 := [s:t](!Raw.is_empty_2 s). + + Definition elements := [s:t](Raw.elements s). + Definition elements_1 := [s:t](!Raw.elements_1 s). + Definition elements_2 := [s:t](!Raw.elements_2 s). + Definition elements_3 := [s:t](Raw.elements_3 (sorted s)). + + Definition min_elt := [s:t](Raw.min_elt s). + Definition min_elt_1 := [s:t](!Raw.min_elt_1 s). + Definition min_elt_2 := [s:t](Raw.min_elt_2 (sorted s)). + Definition min_elt_3 := [s:t](!Raw.min_elt_3 s). + + Definition max_elt := [s:t](Raw.max_elt s). + Definition max_elt_1 := [s:t](!Raw.max_elt_1 s). + Definition max_elt_2 := [s:t](Raw.max_elt_2 (sorted s)). + Definition max_elt_3 := [s:t](!Raw.max_elt_3 s). + + Definition choose := min_elt. + Definition choose_1 := min_elt_1. + Definition choose_2 := min_elt_3. + + Definition fold := [B:Set; f: elt->B->B; s:t](!Raw.fold B f s). + Definition fold_1 := [s:t](!Raw.fold_1 s). + Definition fold_2 := [s,s':t](Raw.fold_2 (sorted s) (sorted s')). + + Definition cardinal := [s:t](Raw.cardinal s). + Definition cardinal_1 := [s:t](!Raw.cardinal_1 s). + Definition cardinal_2 := [s,s':t](Raw.cardinal_2 (sorted s) (sorted s')). + + Definition filter := [f: elt->bool; s:t](Build_slist (Raw.filter_sort (sorted s) f)). + Definition filter_1 := [s:t](!Raw.filter_1 s). + Definition filter_2 := [s:t](!Raw.filter_2 s). + Definition filter_3 := [s:t](!Raw.filter_3 s). + + Definition for_all := [f:elt->bool; s:t](Raw.for_all f s). + Definition for_all_1 := [s:t](!Raw.for_all_1 s). + Definition for_all_2 := [s:t](!Raw.for_all_2 s). + + Definition exists := [f:elt->bool; s:t](Raw.exists f s). + Definition exists_1 := [s:t](!Raw.exists_1 s). + Definition exists_2 := [s:t](!Raw.exists_2 s). + + Definition partition := [f:elt->bool; s:t] + let p = (Raw.partition f s) in + ((!Build_slist (fst ?? p) (Raw.partition_sort_1 (sorted s) f)), + (!Build_slist (snd ?? p) (Raw.partition_sort_2 (sorted s) f))). + Definition partition_1 := [s:t](!Raw.partition_1 s). + Definition partition_2 := [s:t](!Raw.partition_2 s). + + Definition eq := [s,s':t](Raw.eq s s'). + Definition eq_refl := [s:t](Raw.eq_refl s). + Definition eq_sym := [s,s':t](!Raw.eq_sym s s'). + Definition eq_trans := [s,s',s'':t](!Raw.eq_trans s s' s''). + + Definition lt := [s,s':t](Raw.lt s s'). + Definition lt_trans := [s,s',s'':t](!Raw.lt_trans s s' s''). + Definition lt_not_eq := [s,s':t](Raw.lt_not_eq (sorted s) (sorted s')). + + Definition compare : (s,s':t)(Compare lt eq s s'). + Proof. + Intros; Elim (Raw.compare (sorted s) (sorted s')); + [Constructor 1 | Constructor 2 | Constructor 3]; Auto. + Defined. + +End Make. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v new file mode 100644 index 0000000000..226205877c --- /dev/null +++ b/theories/FSets/FSetProperties.v @@ -0,0 +1,1483 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** This module proves many properties of finite sets that + are consequences of the axiomatization in [FSetInterface] *) + +Require Omega. + +Import nat_scope. +Open Scope nat_scope. + +Require Export FSetInterface. +Require Export Bool. +Require Export Sumbool. +Require Export Zerob. +Set Implicit Arguments. + +(* For proving (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)). +Auto. +Qed. + + +Module Properties [M:S]. + Import M. + Import Logic. (* for unmasking eq. *) + Import Peano. (* for unmasking lt *) + + Module ME := MoreOrderedType E. + + Section Old_Spec_Now_Properties. + + Variable s,s' : t. + Variable x,y,z : elt. + + Lemma mem_eq: + (E.eq x y) -> (mem x s)=(mem y s). + Proof. + Intros; Apply bool_1. + Generalize (!mem_1 s x) (!mem_1 s y) (!mem_2 s x) (!mem_2 s y). + Intuition. + EAuto. + Apply H0; Apply In_1 with y; Auto. + Qed. + + Lemma equal_mem_1: + ((a:elt)(mem a s)=(mem a s')) -> (equal s s')=true. + Proof. + Intros; Apply equal_1; Unfold Equal; Intuition; EAuto. + Qed. + + Lemma equal_mem_2: + (equal s s')=true -> (a:elt)(mem a s)=(mem a s'). + Proof. + Intros; Apply bool_1. + Intros; Cut (Equal s s'); [Clear H; Unfold Equal|Auto]. + Intros H; Generalize (H a); Intuition. + Qed. + + Lemma subset_mem_1: + ((a:elt)(mem a s)=true->(mem a s')=true) -> (subset s s')=true. + Proof. + Intros; Apply subset_1; Unfold Subset; Intuition; EAuto. + Qed. + + Lemma subset_mem_2: + (subset s s')=true -> (a:elt)(mem a s)=true -> (mem a s')=true. + Proof. + Intros; Apply bool_1. + Cut (Subset s s'); [Clear H; Unfold Subset|Auto]. + Intros H; Generalize (H a); Intuition. + Qed. + + Lemma empty_mem: (mem x empty)=false. + Proof. + Apply not_true_is_false; Intro; Absurd (In x empty); Auto. + Qed. + + Lemma is_empty_equal_empty: (is_empty s)=(equal s empty). + Proof. + Generalize empty_1 (!is_empty_1 s) (!is_empty_2 s) + (!equal_1 s empty) (!equal_2 s empty). + Unfold Empty Equal. + Case (is_empty s); Case (equal s empty); Intuition. + Clear H3 H1. + Symmetry; Apply H2; Intuition. + Generalize (H4 a); Intuition. + Generalize (H a); Intuition. + Clear H1 H3. + Apply H0; Intuition. + Generalize (H4 a); Intuition. + Generalize (H a); Intuition. + Qed. + + Lemma choose_mem_1: (choose s)=(Some ? x) -> (mem x s)=true. + Proof. + Auto. + Qed. + + Lemma choose_mem_2: (choose s)=(None ?) -> (is_empty s)=true. + Proof. + Auto. + Qed. + + Lemma add_mem_1: (mem x (add x s))=true. + Proof. + Auto. + Qed. + + Lemma add_mem_2: + ~ (E.eq x y) -> (mem y (add x s))=(mem y s). + Proof. + Intros; Apply bool_1; Intuition; EAuto. + Qed. + + Lemma remove_mem_1: (mem x (remove x s))=false. + Proof. + Apply not_true_is_false; Intro; Absurd (In x (remove x s)); Auto. + Qed. + + Lemma remove_mem_2: + ~ (E.eq x y) -> (mem y (remove x s))=(mem y s). + Proof. + Intros; Apply bool_1; Intuition; EAuto. + Qed. + + Lemma singleton_equal_add: + (equal (singleton x) (add x empty))=true. + Proof. + Apply equal_1; Unfold Equal; Intuition. + Apply In_1 with x; Auto. + Assert (E.eq a x); Auto. + Elim (ME.eq_dec a x); Auto. + Intros; Assert (In a empty). + EApply add_3; EAuto. + Generalize (empty_1 H0); Intuition. + Qed. + + Lemma union_mem: + (mem x (union s s'))=(orb (mem x s) (mem x s')). + Proof. + Apply bool_1; Intuition. + Elim (!union_1 s s' x); Intuition. + Elim (orb_prop ? ? H); Intuition. + Qed. + + Lemma inter_mem: + (mem x (inter s s'))=(andb (mem x s) (mem x s')). + Proof. + Apply bool_1; Intuition. + Apply andb_true_intro; Intuition EAuto. + Elim (andb_prop ?? H); Intuition. + Qed. + + Lemma diff_mem: + (mem x (diff s s'))=(andb (mem x s) (negb (mem x s'))). + Proof. + Generalize (!diff_1 s s' x) (!diff_2 s s' x) (!diff_3 s s' x). + LetTac s0 := (diff s s'). + Generalize (!mem_1 s x) (!mem_1 s' x) (!mem_1 s0 x) + (!mem_2 s x) (!mem_2 s' x) (!mem_2 s0 x). + Case (mem x s); Case (mem x s'); Case (mem x s0); Intuition. + Qed. + + Section Cardinal. + + Lemma Add_add : + (s:t)(x:elt)(Add x s (add x s)). + Proof. + Unfold Add; Intros; Intuition. + Elim (ME.eq_dec x0 y0); Intros; Auto. + Right. + EApply add_3; EAuto. + Apply In_1 with x0; Auto. + Qed. + + Lemma Add_remove : (s:t)(x:elt)(In x s) -> (Add x (remove x s) s). + Proof. + Intros; Unfold Add; Intuition. + Elim (ME.eq_dec x0 y0); Intros; Auto. + Apply In_1 with x0; Auto. + EAuto. + Qed. + + 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')). + Proof. + Unfold Equal; Intros. + Elim (ME.eq_dec x0 a); Intros; Auto. + Split; Intros. + Absurd (In x0 (remove x0 s0)); Auto; Apply In_1 with a; Auto. + Absurd (In x0 (remove x0 s'0)); Auto; Apply In_1 with a; Auto. + Elim (H0 a); Intros. + Split; Intros; Apply remove_2; Auto; + [Apply H1|Apply H2]; EApply remove_3;EAuto. + Save. + + Hints Resolve Equal_remove. + + Lemma cardinal_inv_1 : (s:t)(cardinal s)=O -> (Empty s). + Proof. + Intros; Generalize (!choose_1 s0) (!choose_2 s0). + Elim (choose s0); Intuition. + Clear H1; Assert (In a s0); Auto. + Rewrite (!cardinal_2 (remove a s0) s0 a) in H; Auto. + Inversion H. + Save. + Hints Resolve cardinal_inv_1. + + Lemma cardinal_inv_2 : + (s:t)(n:nat)(cardinal s)=(S n) -> (EX x:elt | (In x s)). + Proof. + Intros; Generalize (!choose_1 s0) (!choose_2 s0). + Elim (choose s0); Intuition. + Exists a; Auto. + Intros; Rewrite cardinal_1 in H; Auto; Inversion H. + Qed. + + Lemma Equal_cardinal_aux : (n:nat)(s,s':t)(cardinal s)=n -> + (Equal s s')->(cardinal s)=(cardinal s'). + Proof. + Induction n. + Intros. + Rewrite H. + Symmetry. + Apply cardinal_1. + Generalize (cardinal_inv_1 H) H0. + Unfold Empty Equal; Intuition. + Generalize (H1 a) (H2 a); Intuition. + Intros. + Elim (cardinal_inv_2 H0); Intros. + Assert (In x0 s'0). + Generalize (H1 x0); Intuition. + Generalize H0. + Rewrite (!cardinal_2 (remove x0 s0) s0 x0);Auto. + Rewrite (!cardinal_2 (remove x0 s'0) s'0 x0); Auto. + Qed. + + Lemma Equal_cardinal : (s,s':t)(Equal s s')->(cardinal s)=(cardinal s'). + Proof. + Intros; EApply Equal_cardinal_aux; EAuto. + Qed. + + End Cardinal. + + Hints Resolve Add_add Add_remove Equal_remove + cardinal_inv_1 Equal_cardinal. + + 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). + Proof. + Induction n. + Intros; Apply H; Auto. + Intros; Elim (cardinal_inv_2 H2); Intros. + Apply H0 with (remove x0 s0) x0; Auto. + Apply H1; Auto. + Assert (S (cardinal (remove x0 s0))) = (S n0); Auto. + Rewrite <- H2; Symmetry. + EApply cardinal_2; EAuto. + Qed. + + 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). + Proof. + Intros; EApply cardinal_induction; EAuto. + Qed. + + Section Fold. + + 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). + Proof. + Apply fold_1; Auto. + Qed. + + Lemma fold_equal: + (equal s s')=true -> (eqA (fold f s i) (fold f s' i)). + Proof. + Pattern s; Apply set_induction; Intros. + Apply (Seq_trans ?? st) with i; Auto. + Apply fold_1; Auto. + Apply Seq_sym; Auto; Apply fold_1; Auto. + Apply cardinal_inv_1; Rewrite <- (Equal_cardinal (equal_2 H0)); Auto. + Apply (Seq_trans ?? st) with (f x0 (fold f s0 i)); Auto. + Apply fold_2 with eqA:=eqA; Auto. + Apply Seq_sym; Auto; Apply fold_2 with eqA := eqA; Auto. + Generalize (equal_2 H2) H1; Unfold Add Equal; Intros; + Elim (H4 y0); Elim (H3 y0); Intuition. + 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_2 with eqA:=eqA; Auto. + Intro; Rewrite mem_1 in H; Auto; Discriminate H. + Qed. + + End Fold. + + Lemma cardinal_fold: (cardinal s)=(fold [_]S s O). + Proof. + Pattern s; Apply set_induction; Intros. + Rewrite cardinal_1; Auto; Symmetry; Apply fold_1;Auto. + Rewrite (!cardinal_2 s0 s'0 x0);Auto. + Rewrite H; Symmetry; Change S with ([_]S x0). + Apply fold_2 with eqA:=(eq nat); Auto. + Qed. + + Section Filter. + + Variable f:elt->bool. + Variable Comp: (compat_bool E.eq f). + + Lemma filter_mem: (mem x (filter f s))=(andb (mem x s) (f x)). + Proof. + Apply bool_1; Intuition. + Apply andb_true_intro; Intuition; EAuto. + Elim (andb_prop ?? H); Intuition. + Qed. + + Lemma for_all_filter: + (for_all f s)=(is_empty (filter [x](negb (f x)) s)). + Proof. + Assert Comp' : (compat_bool E.eq [x](negb (f x))). + Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb); Auto. + Apply bool_1; Intuition. + Apply is_empty_1. + Unfold Empty; Intros. + Intro. + Assert (In a s); EAuto. + Generalize (filter_2 Comp' H0). + Generalize (for_all_2 Comp H H1); Auto. + Intros Eq; Rewrite Eq; Intuition. + Apply for_all_1; Unfold For_all; Intros; Auto. + Apply bool_3. + Red; Intros. + Elim (is_empty_2 H 3!x0); Auto. + Qed. + + Lemma exists_filter: + (exists f s)=(negb (is_empty (filter f s))). + Proof. + Apply bool_1; Intuition. + Elim (exists_2 Comp H); Intuition. + Apply bool_6. + Red; Intros; Apply (is_empty_2 H0 3!x0); Auto. + Generalize (!choose_1 (filter f s)) (!choose_2 (filter f s)). + Case (choose (filter f s)). + Intros. + Clear H1. + Apply exists_1; Auto. + Exists e; Generalize (H0 e); Intuition; EAuto. + Intros. + Clear H0. + Rewrite (!is_empty_1 (filter f s)) in H; Auto. + Discriminate H. + Qed. + + Lemma partition_filter_1: + (equal (fst ? ? (partition f s)) (filter f s))=true. + Proof. + Auto. + Qed. + + Lemma partition_filter_2: + (equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s))=true. + Proof. + Auto. + Qed. + + End Filter. + End Old_Spec_Now_Properties. + + Hints Immediate + empty_mem + is_empty_equal_empty + add_mem_1 + remove_mem_1 + singleton_equal_add + union_mem + inter_mem + diff_mem + cardinal_fold + filter_mem + for_all_filter + exists_filter : set. + + Hints Resolve + equal_mem_1 + subset_mem_1 + choose_mem_1 + choose_mem_2 + add_mem_2 + remove_mem_2 : set. + +Section MoreProperties. + +(*s Properties of [equal] *) + +Lemma equal_refl: (s:t)(equal s s)=true. +Proof. +Auto with set. +Qed. + +Lemma equal_sym: (s,s':t)(equal s s')=(equal s' s). +Proof. +Intros. +Apply bool_eq_ind;Intros. +Rewrite equal_mem_1;Auto. +Symmetry;Apply equal_mem_2;Auto. +Apply (bool_eq_ind (equal s s'));Intros;Auto. +Rewrite equal_mem_1 in H;Auto. +Symmetry;Apply equal_mem_2;Auto. +Qed. + +Lemma equal_trans: + (s,u,v:t)(equal s u)=true -> (equal u v)=true -> (equal s v)=true. +Proof. +Intros. +Apply equal_mem_1;Intros. +Rewrite (equal_mem_2 H). +Apply equal_mem_2;Assumption. +Qed. + +Lemma equal_equal: + (s,t_,u:t)(equal s t_)=true -> (equal s u)=(equal t_ u). +Proof. +Intros. +Apply bool_eq_ind;Intros. +Apply equal_trans with t_;Auto with set. +Symmetry; Apply bool_eq_ind;Intros;Auto. +Rewrite <- H0. +Apply equal_trans with s;Auto with set. +Rewrite equal_sym;Auto. +Qed. + +Lemma equal_cardinal: + (s,s':t)(equal s s')=true -> (cardinal s)=(cardinal s'). +Proof. +Intros; Apply Equal_cardinal; Auto. +Qed. + +Hints Resolve equal_refl equal_cardinal equal_equal:set. +Hints Immediate equal_sym :set. + +(* Properties of [subset] *) + +Lemma subset_refl: (s:t)(subset s s)=true. +Proof. +Auto with set. +Qed. + +Lemma subset_antisym: + (s,s':t)(subset s s')=true -> (subset s' s)=true -> (equal s s')=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Apply bool_eq_ind;Intros. +EApply subset_mem_2;EAuto. +Apply (bool_eq_ind (mem a s));Intros;Auto. +Rewrite <- (subset_mem_2 H H2);Assumption. +Qed. + +Lemma subset_trans: + (s,t_,u:t)(subset s t_)=true -> (subset t_ u)=true -> (subset s u)=true. +Proof. +Intros. +Apply subset_mem_1;Intros. +Apply subset_mem_2 with t_;Intros;Auto. +Apply subset_mem_2 with s;Auto. +Qed. + +Lemma subset_equal: + (s,s':t)(equal s s')=true -> (subset s s')=true. +Proof. +Intros. +Apply subset_mem_1;Intros. +Rewrite <- (equal_mem_2 H);Auto. +Qed. + +Hints Resolve subset_refl subset_equal subset_antisym :set. + +(*s Properties of [empty] *) + +Lemma empty_cardinal: (cardinal empty)=O. +Proof. +Rewrite cardinal_fold; Auto with set. +Apply fold_1; Auto. +Qed. + +Hints Immediate empty_cardinal :set. + +(*s Properties of [choose] *) + +Lemma choose_mem_3: + (s:t)(is_empty s)=false -> {x:elt|(choose s)=(Some ? x)/\(mem x s)=true}. +Proof. +Intros. +Generalize (!choose_mem_1 s). +Generalize (!choose_mem_2 s). +Case (choose s);Intros. +Exists e;Auto. +LApply H0;Trivial;Intros. +Rewrite H in H2;Discriminate H2. +Qed. + +Lemma choose_mem_4: (choose empty)=(None ?). +Proof. +Generalize (!choose_mem_1 empty). +Case (!choose empty);Intros;Auto. +Absurd true=false;Auto with bool. +Rewrite <- (H e);Auto with set. +Qed. + +(*s Properties of [add] *) + +Lemma add_mem_3: + (s:t)(x,y:elt)(mem y s)=true -> (mem y (add x s))=true. +Proof. +Auto. +Qed. + +Lemma add_equal: + (s:t)(x:elt)(mem x s)=true -> (equal (add x s) s)=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Elim (ME.eq_dec x a); Intros; Auto with set. +Rewrite <- mem_eq with x:=x;Auto. +Rewrite <- (mem_eq s a0);Auto. +Rewrite H;Auto with set. +Qed. + +Hints Resolve add_mem_3 add_equal :set. + +Lemma add_fold: + (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA)) + (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) -> + (s:t)(x:elt)(mem x s)=true -> (eqA (fold f (add x s) i) (fold f s i)). +Proof. +Intros; Apply fold_equal with eqA:=eqA; Auto with set. +Qed. + +Lemma add_cardinal_1: + (s:t)(x:elt)(mem x s)=true -> (cardinal (add x s))=(cardinal s). +Proof. +Auto with set. +Qed. + +Lemma add_cardinal_2: + (s:t)(x:elt)(mem x s)=false -> (cardinal (add x s))=(S (cardinal s)). +Proof. +Intros. +Do 2 Rewrite cardinal_fold. +Change S with ([_]S x); Apply fold_add with eqA:=(eq nat); Auto. +Qed. + +(*s Properties of [remove] *) + +Lemma remove_mem_3: + (s:t)(x,y:elt)(mem y (remove x s))=true -> (mem y s)=true. +Proof. +Intros s x y;Elim (ME.eq_dec x y); Intro e. +Rewrite <- mem_eq with x:=x;Auto. +Rewrite <- (mem_eq s e);Auto. +Rewrite (remove_mem_1 s x);Intro H;Discriminate H. +Intros;Rewrite <- H;Symmetry;Auto with set. +Qed. + +Lemma remove_equal: + (s:t)(x:elt)(mem x s)=false -> (equal (remove x s) s)=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Elim (ME.eq_dec x a); Intros;Auto with set. +Rewrite <- mem_eq with x:=x;Auto. +Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set. +Qed. + +Hints Resolve remove_mem_3 remove_equal :set. + +Lemma add_remove: + (s:t)(x:elt)(mem x s)=true -> (equal (add x (remove x s)) s)=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Elim (ME.eq_dec x a); Intros;Auto with set. +Rewrite <- mem_eq with x:=x;Auto. +Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set. +Transitivity (mem a (remove x s));Auto with set. +Qed. + +Lemma remove_add: + (s:t)(x:elt)(mem x s)=false -> (equal (remove x (add x s)) s)=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Elim (ME.eq_dec x a); Intros;Auto with set. +Rewrite <- mem_eq with x:=x;Auto. +Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set. +Transitivity (mem a (add x s));Auto with set. +Qed. + +Hints Immediate add_remove remove_add :set. + +Lemma remove_fold_1: + (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA)) + (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) -> + (s:t)(x:elt)(mem x s)=true -> + (eqA (f x (fold f (remove x s) i)) (fold f s i)). +Proof. +Intros. +Apply Seq_sym; Auto. +Apply fold_2 with eqA:=eqA; Auto. +Apply Add_remove; Auto. +Qed. + +Lemma remove_fold_2: + (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA)) + (f:elt->A->A)(i:A) (compat_op E.eq eqA f) -> (transpose eqA f) -> + (s:t)(x:elt)(mem x s)=false -> + (eqA (fold f (remove x s) i) (fold f s i)). +Proof. +Intros. +Apply fold_equal with eqA:=eqA; Auto with set. +Qed. + +Lemma remove_cardinal_1: + (s:t)(x:elt)(mem x s)=true -> (S (cardinal (remove x s)))=(cardinal s). +Proof. +Intros. +Do 2 Rewrite cardinal_fold. +Change S with ([_]S x). +Apply remove_fold_1 with eqA:=(eq nat); Auto. +Qed. + +Lemma remove_cardinal_2: + (s:t)(x:elt)(mem x s)=false -> (cardinal (remove x s))=(cardinal s). +Proof. +Auto with set. +Qed. + +(* Properties of [is_empty] *) + +Lemma is_empty_cardinal: (s:t)(is_empty s)=(zerob (cardinal s)). +Proof. +Intros. +Apply (bool_eq_ind (is_empty s));Intros. +Rewrite (equal_cardinal 1!s 2!empty). +Rewrite empty_cardinal;Simpl;Trivial. +Rewrite <- H;Symmetry;Auto with set. +Elim (choose_mem_3 H);Intros. +Elim p;Intros. +Rewrite <- (remove_cardinal_1 H1). +Simpl;Trivial. +Qed. + +(*s Properties of [singleton] *) + +Lemma singleton_mem_1: (x:elt)(mem x (singleton x))=true. +Proof. +Intros. +Rewrite (equal_mem_2 (singleton_equal_add x));Auto with set. +Qed. + +Lemma singleton_mem_2: (x,y:elt)~(E.eq x y) -> (mem y (singleton x))=false. +Proof. +Intros. +Rewrite (equal_mem_2 (singleton_equal_add x)). +Rewrite <- (empty_mem y);Auto with set. +Qed. + +Lemma singleton_mem_3: (x,y:elt)(mem y (singleton x))=true -> (E.eq x y). +Proof. +Intros. +Elim (ME.eq_dec x y);Intros;Auto. +Qed. + +Lemma singleton_cardinal: (x:elt)(cardinal (singleton x))=(S O). +Proof. +Intros. +Rewrite (equal_cardinal (singleton_equal_add x)). +Rewrite add_cardinal_2;Auto with set. +Qed. + +(* General recursion principes based on [cardinal] *) + +Lemma cardinal_set_rec: (P:t->Set) + ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> + ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> + (P empty) -> (n:nat)(s:t)(cardinal s)=n -> (P s). +Proof. +NewInduction n; Intro s; Generalize (is_empty_cardinal s); + Intros eq1 eq2; Rewrite eq2 in eq1; Simpl in eq1. +Rewrite is_empty_equal_empty in eq1. +Rewrite equal_sym in eq1. +Apply (H empty s eq1);Auto. +Elim (choose_mem_3 eq1);Intros;Elim p;Clear p;Intros. +Apply (H (add x (remove x s)) s);Auto with set. +Apply H0;Auto with set. +Apply IHn. +Rewrite <- (remove_cardinal_1 H3) in eq2. +Inversion eq2;Trivial. +Qed. + +Lemma set_rec: (P:t->Set) + ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> + ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> + (P empty) -> (s:t)(P s). +Proof. +Intros;EApply cardinal_set_rec;EAuto. +Qed. + +Lemma cardinal_set_ind: (P:t->Prop) + ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> + ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> + (P empty) -> (n:nat)(s:t)(cardinal s)=n -> (P s). +Proof. +NewInduction n; Intro s; Generalize (is_empty_cardinal s); + Intros eq1 eq2; Rewrite eq2 in eq1; Simpl in eq1. +Rewrite is_empty_equal_empty in eq1. +Rewrite equal_sym in eq1. +Apply (H empty s eq1);Auto. +Elim (choose_mem_3 eq1);Intros;Elim p;Clear p;Intros. +Apply (H (add x (remove x s)) s);Auto with set. +Apply H0;Auto with set. +Apply IHn. +Rewrite <- (remove_cardinal_1 H3) in eq2. +Inversion eq2;Trivial. +Qed. + +Lemma set_ind: (P:t->Prop) + ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> + ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> + (P empty) -> (s:t)(P s). +Proof. +Intros;EApply cardinal_set_ind;EAuto. +Qed. + +(*s Properties of [fold] *) + +Lemma fold_commutes: + (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA)) + (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) -> (s:t)(x:elt) + (eqA (fold f s (f x i)) (f x (fold f s i))). +Proof. +Intros; Pattern s; Apply set_ind. +Intros. +Apply (Seq_trans ?? st) with (fold f s0 (f x i)). +Apply fold_equal with eqA:=eqA; Auto with set. +Rewrite equal_sym; Auto. +Apply (Seq_trans ?? st) with (f x (fold f s0 i)); Auto. +Apply H; Auto. +Apply fold_equal with eqA:=eqA; Auto. +Intros. +Apply (Seq_trans ?? st) with (f x0 (fold f s0 (f x i))). +Apply fold_add with eqA:=eqA; Auto. +Apply (Seq_trans ?? st) with (f x0 (f x (fold f s0 i))). +Apply H; Auto. +Apply (Seq_trans ?? st) with (f x (f x0 (fold f s0 i))). +Apply H0; Auto. +Apply H; Auto. +Apply Seq_sym; Auto. +Apply fold_add with eqA:=eqA; Auto. +Apply (Seq_trans ?? st) with (f x i). +Apply fold_empty; Auto. +Apply Seq_sym; Auto. +Apply H; Auto. +Apply fold_empty; Auto. +Qed. + +Lemma fold_plus: + (s:t)(p:nat)(fold [_]S s p)=(fold [_]S s O)+p. +Proof. +Assert st := (gen_st nat). +Assert fe: (compat_op E.eq (eq ?) [_:elt]S). Unfold compat_op; Auto. +Assert fp: (transpose (eq ?) [_:elt]S). Unfold transpose;Auto. +Intros s p;Pattern s;Apply set_ind. +Intros; Rewrite <- (fold_equal st p fe fp H). +Rewrite <- (fold_equal st O fe fp H);Assumption. +Intros. +Assert (p:nat)(fold [_]S (add x s0) p) = (S (fold [_]S s0 p)). +Change S with ([_]S x). +Intros; Apply fold_add with eqA:=(eq nat); Auto. +Rewrite (H1 p). +Rewrite (H1 O). +Rewrite H0. +Simpl; Auto. +Intros; Do 2 Rewrite (fold_empty st);Auto. +Qed. + +(*s Properties of [union] *) + +Lemma union_sym: + (s,s':t)(equal (union s s') (union s' s))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 2 Rewrite union_mem;Auto with bool. +Qed. + +Lemma union_subset_equal: + (s,s':t)(subset s s')=true->(equal (union s s') s')=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite union_mem. +Apply (bool_eq_ind (mem a s));Intros;Simpl;Auto with set. +Rewrite (subset_mem_2 H H0);Auto. +Qed. + +Lemma union_equal_1: + (s,s',s'':t)(equal s s')=true-> + (equal (union s s'') (union s' s''))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 2 (Rewrite union_mem;Idtac). +Rewrite (equal_mem_2 H a);Auto. +Qed. + +Lemma union_equal_2: + (s,s',s'':t)(equal s' s'')=true-> + (equal (union s s') (union s s''))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 2 (Rewrite union_mem;Idtac). +Rewrite (equal_mem_2 H a);Auto. +Qed. + +Lemma union_assoc: + (s,s',s'':t) + (equal (union (union s s') s'') (union s (union s' s'')))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 4 Rewrite union_mem. +Rewrite orb_assoc;Auto. +Qed. + +Lemma add_union_singleton: + (s:t)(x:elt)(equal (add x s) (union (singleton x) s))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite union_mem. +Elim (ME.eq_dec x a);Intros. +Rewrite <- (mem_eq (add x s) a0). +Rewrite <- (mem_eq (singleton x) a0). +Rewrite <- (mem_eq s a0). +Rewrite add_mem_1;Rewrite singleton_mem_1;Simpl;Auto. +Rewrite singleton_mem_2;Simpl;Auto with set. +Qed. + +Lemma union_add: + (s,s':t)(x:elt) + (equal (union (add x s) s') (add x (union s s')))=true. +Proof. +Intros;Apply equal_trans with (union (union (singleton x) s) s'). +Apply union_equal_1;Apply add_union_singleton. +Apply equal_trans with (union (singleton x) (union s s')). +Apply union_assoc. +Rewrite equal_sym;Apply add_union_singleton. +Qed. + +(* caracterisation of [union] via [subset] *) + +Lemma union_subset_1: + (s,s':t)(subset s (union s s'))=true. +Proof. +Intros;Apply subset_mem_1;Intros;Rewrite union_mem;Rewrite H;Auto. +Qed. + +Lemma union_subset_2: + (s,s':t)(subset s' (union s s'))=true. +Proof. +Intros;Apply subset_mem_1;Intros;Rewrite union_mem;Rewrite H;Apply orb_b_true. +Qed. + +Lemma union_subset_3: + (s,s',s'':t)(subset s s'')=true -> (subset s' s'')=true -> + (subset (union s s') s'')=true. +Proof. +Intros;Apply subset_mem_1;Intros;Rewrite union_mem in H1. +Elim (orb_true_elim ? ? H1);Intros. +Apply (subset_mem_2 H a0). +Apply (subset_mem_2 H0 b). +Qed. + +(*s Properties of [inter] *) + +Lemma inter_sym: + (s,s':t)(equal (inter s s') (inter s' s))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 2 Rewrite inter_mem. +Auto with bool. +Qed. + +Lemma inter_subset_equal: + (s,s':t)(subset s s')=true->(equal (inter s s') s)=true. +Proof. +Intros. +Apply equal_mem_1;Intros. +Rewrite inter_mem. +Apply (bool_eq_ind (mem a s));Intros;Simpl;Auto. +Rewrite (subset_mem_2 H H0);Auto. +Qed. + +Lemma inter_equal_1: + (s,s',s'':t)(equal s s')=true-> + (equal (inter s s'') (inter s' s''))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 2 (Rewrite inter_mem;Idtac). +Rewrite (equal_mem_2 H a);Auto. +Qed. + +Lemma inter_equal_2: + (s,s',s'':t)(equal s' s'')=true-> + (equal (inter s s') (inter s s''))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 2 (Rewrite inter_mem;Idtac). +Rewrite (equal_mem_2 H a);Auto. +Qed. + +Lemma inter_assoc: + (s,s',s'':t) + (equal (inter (inter s s') s'') (inter s (inter s' s'')))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Do 4 Rewrite inter_mem. +Rewrite andb_assoc;Auto. +Qed. + +Lemma union_inter_1: + (s,s',s'':t) + (equal (inter (union s s') s'') (union (inter s s'') (inter s' s'')))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite union_mem. +Do 3 Rewrite inter_mem. +Rewrite union_mem. +Apply demorgan2. +Qed. + +Lemma union_inter_2: + (s,s',s'':t) + (equal (union (inter s s') s'') (inter (union s s'') (union s' s'')))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite union_mem. +Do 2 Rewrite inter_mem. +Do 2 Rewrite union_mem. +Apply demorgan4. +Qed. + +Lemma inter_add_1: + (s,s':t)(x:elt)(mem x s')=true -> + (equal (inter (add x s) s') (add x (inter s s')))=true. +Proof. +Intros;Apply equal_trans with (inter (union (singleton x) s) s'). +Apply inter_equal_1;Apply add_union_singleton. +Apply equal_trans with (union (inter (singleton x) s') (inter s s')). +Apply union_inter_1. +Apply equal_trans with (union (singleton x) (inter s s')). +Apply union_equal_1. +Apply inter_subset_equal. +Apply subset_mem_1;Intros. +Rewrite <- (mem_eq s' (singleton_mem_3 H0));Auto. +Rewrite equal_sym;Apply add_union_singleton. +Qed. + +Lemma inter_add_2: + (s,s':t)(x:elt)(mem x s')=false -> + (equal (inter (add x s) s') (inter s s'))=true. +Proof. +Intros;Apply equal_trans with (inter (union (singleton x) s) s'). +Apply inter_equal_1;Apply add_union_singleton. +Apply equal_trans with (union (inter (singleton x) s') (inter s s')). +Apply union_inter_1. +Apply union_subset_equal. +Apply subset_mem_1;Intros. +Rewrite inter_mem in H0. +Elim (andb_prop ? ? H0);Intros. +Absurd (mem a s')=true;Auto. +Rewrite <- (mem_eq s' (singleton_mem_3 H1));Auto. +Rewrite H;Auto with bool. +Qed. + +(* caracterisation of [union] via [subset] *) + +Lemma inter_subset_1: + (s,s':t)(subset (inter s s') s)=true. +Proof. +Intros;Apply subset_mem_1;Intros;Rewrite inter_mem in H;Elim (andb_prop ? ? H);Auto. +Qed. + +Lemma inter_subset_2: + (s,s':t)(subset (inter s s') s')=true. +Proof. +Intros;Apply subset_mem_1;Intros;Rewrite inter_mem in H;Elim (andb_prop ? ? H);Auto. +Qed. + +Lemma inter_subset_3: + (s,s',s'':t)(subset s'' s)=true -> (subset s'' s')=true -> + (subset s'' (inter s s'))=true. +Intros;Apply subset_mem_1;Intros;Rewrite inter_mem. +Rewrite (subset_mem_2 H H1);Rewrite (subset_mem_2 H0 H1);Auto. +Qed. + +(*s Properties of [union],[inter],[fold] and [cardinal] *) + +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)). +Proof. +Intro A. +LetTac st := (gen_st A). +Intros;Pattern s;Apply set_ind. +Intros; Rewrite <- (fold_equal st i H H0 (inter_equal_1 s' H1)). +Rewrite <- (fold_equal st (fold f s' i) H H0 H1). +Rewrite <- (fold_equal st (fold f (inter s0 s') i) H H0 (union_equal_1 s' H1));Auto. +Intros. +Rewrite + (fold_equal st (fold f (inter (add x s0) s') i) H H0 (union_add s0 s' x)). +Generalize (refl_equal ? (mem x s')); Pattern -1 (mem x s'); Case (mem x s');Intros. +Rewrite (fold_equal st i H H0 (inter_add_1 s0 H3)). +Cut (mem x (inter s0 s'))=false;Intros. +Cut (mem x (union s0 s'))=true;Intros. +Rewrite (fold_add st i H H0 H4). +Rewrite (fold_commutes st);Auto. +Rewrite (fold_equal st (fold f (inter s0 s') i) H H0 (add_equal H5)). +Rewrite (fold_add st (fold f s' i) H H0 H1). +Rewrite H2;Auto. +Rewrite union_mem;Rewrite H3;Apply orb_b_true. +Rewrite inter_mem;Rewrite H1;Simpl;Auto. +Rewrite (fold_equal st i H H0 (inter_add_2 s0 H3)). +Cut (mem x (union s0 s'))=false;Intros. +Rewrite (fold_add st (fold f (inter s0 s') i) H H0 H4). +Rewrite (fold_add st (fold f s' i) H H0 H1). +Rewrite H2;Auto. +Rewrite union_mem;Rewrite H3; Rewrite H1;Auto. +Cut (subset empty s')=true;Intros. +Rewrite (fold_equal st i H H0 (inter_subset_equal H1)). +Do 2 Rewrite (fold_empty st);Apply fold_equal with eqA:=(eq A);Auto. +Apply union_subset_equal;Auto. +Apply subset_mem_1;Intros. +Rewrite empty_mem in H1;Absurd true=false;Auto with bool. +Qed. + +Lemma union_inter_cardinal: + (s,s':t)(cardinal (union s s'))+(cardinal (inter s s')) + = (cardinal s)+(cardinal s'). +Proof. +Intros. +Do 4 Rewrite cardinal_fold. +Do 2 Rewrite <- fold_plus. +Apply fold_union_inter;Auto. +Qed. + +Lemma fold_union: + (A:Set)(f:elt->A->A)(i:A)(compat_op E.eq (eq A) f) -> (transpose (eq A) f) -> + (s,s':t)((x:elt)(andb (mem x s) (mem x s'))=false) -> + (fold f (union s s') i)=(fold f s (fold f s' i)). +Proof. +Intros. +Assert st:= (gen_st A). +Rewrite <- (fold_union_inter i H H0 s s'). +Cut (equal (inter s s') empty)=true;Intros. +Rewrite (fold_equal st i H H0 H2). +Rewrite (fold_empty st);Auto. +Apply equal_mem_1;Intros. +Rewrite inter_mem; Rewrite empty_mem;Auto. +Qed. + +Lemma union_cardinal: + (s,s':t)((x:elt)(andb (mem x s) (mem x s'))=false) -> + (cardinal (union s s'))=(cardinal s)+(cardinal s'). +Proof. +Intros. +Do 3 Rewrite cardinal_fold. +Rewrite fold_union;Auto. +Apply fold_plus;Auto. +Qed. + +(*s Properties of [diff] *) + +Lemma diff_subset: + (s,s':t)(subset (diff s s') s)=true. +Proof. +Intros. +Apply subset_mem_1;Intros. +Rewrite diff_mem in H. +Elim (andb_prop ? ? H);Auto. +Qed. + +Lemma diff_subset_equal: + (s,s':t)(subset s s')=true->(equal (diff s s') empty)=true. +Proof. +Intros. +Apply equal_mem_1;Intros. +Rewrite empty_mem. +Rewrite diff_mem. +Generalize (!subset_mem_2 ?? H a). +Case (mem a s);Simpl;Intros;Auto. +Rewrite H0;Auto. +Qed. + +Lemma remove_inter_singleton: + (s:t)(x:elt)(equal (remove x s) (diff s (singleton x)))=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite diff_mem. +Elim (ME.eq_dec x a); Intros. +Rewrite <- (mem_eq (remove x s) a0). +Rewrite <- (mem_eq s a0). +Rewrite <- (mem_eq (singleton x) a0). +Rewrite remove_mem_1;Rewrite singleton_mem_1;Rewrite andb_b_false;Auto. +Rewrite singleton_mem_2;Auto;Simpl;Rewrite andb_b_true;Auto with set. +Qed. + +Lemma diff_inter_empty: + (s,s':t)(equal (inter (diff s s') (inter s s')) empty)=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite empty_mem;Do 2 Rewrite inter_mem;Rewrite diff_mem. +Case (mem a s);Case (mem a s');Simpl;Auto. +Qed. + +Lemma diff_inter_all: +(s,s':t)(equal (union (diff s s') (inter s s')) s)=true. +Proof. +Intros;Apply equal_mem_1;Intros. +Rewrite union_mem;Rewrite inter_mem;Rewrite diff_mem. +Case (mem a s);Case (mem a s');Simpl;Auto. +Qed. + +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). +Proof. +Intros. +Assert st := (gen_st A). +Rewrite <- (fold_union_inter i H H0 (diff s s') (inter s s')). +Rewrite (fold_equal st i H H0 (diff_inter_empty s s')). +Rewrite (fold_empty st). +Apply fold_equal with eqA:=(eq A);Auto. +Apply diff_inter_all. +Qed. + +Lemma diff_inter_cardinal: + (s,s':t)(cardinal (diff s s'))+(cardinal (inter s s'))=(cardinal s). +Proof. +Intros. +Do 3 Rewrite cardinal_fold. +Rewrite <- fold_plus. +Apply fold_diff_inter; Auto. +Qed. + +Lemma subset_cardinal: + (s,s':t)(subset s s')=true -> (le (cardinal s) (cardinal s')). +Proof. +Intros. +Rewrite <- (diff_inter_cardinal s' s). +Rewrite (equal_cardinal (inter_sym s' s)). +Rewrite (equal_cardinal (inter_subset_equal H)); Auto with arith. +Qed. + +(*s Properties of [for_all] *) + +Section For_all. + +Variable f : elt->bool. +Variable Comp : (compat_bool E.eq f). + +Local Comp' : (compat_bool E.eq [x](negb (f x))). +Proof. +Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb);Auto. +Qed. + +Lemma for_all_mem_1: + (s:t)((x:elt)(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_mem; Auto. +Rewrite empty_mem. +Generalize (H a); Case (mem a s);Intros;Auto. +Rewrite H0;Auto. +Qed. + +Lemma for_all_mem_2: + (s:t)(for_all f s)=true -> (x:elt)(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_mem; Auto. +Rewrite empty_mem. +Rewrite H0; Simpl;Intros. +Replace true with (negb false);Auto;Apply negb_sym;Auto. +Qed. + +Lemma for_all_mem_3: + (s:t)(x:elt)(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_mem; Auto. +Rewrite empty_mem. +Rewrite H. +Rewrite H0. +Simpl;Auto. +Qed. + +Lemma for_all_mem_4: + (s:t)(for_all f s)=false -> {x:elt | (mem x s)=true /\ (f x)=false}. +Intros. +Rewrite for_all_filter in H; Auto. +Elim (choose_mem_3 H);Intros;Elim p;Intros. +Exists x. +Rewrite filter_mem in H1; Auto. +Elim (andb_prop ? ? H1). +Split;Auto. +Replace false with (negb true);Auto;Apply negb_sym;Auto. +Qed. + +End For_all. + +(*s Properties of [exists] *) + +Section Exists. + +Variable f : elt->bool. +Variable Comp : (compat_bool E.eq f). + +Local Comp' : (compat_bool E.eq [x](negb (f x))). +Proof. +Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb);Auto. +Qed. + +Lemma for_all_exists: + (s:t)(exists f s)=(negb (for_all [x](negb (f x)) s)). +Proof. +Intros. +Rewrite for_all_filter; Auto. +Rewrite exists_filter; Auto. +Apply (f_equal ? ? negb). +Do 2 Rewrite is_empty_equal_empty. +Apply equal_equal. +Apply equal_mem_1;Intros. +Do 2 (Rewrite filter_mem; Auto). +Rewrite negb_elim;Auto. +Generalize Comp'; Unfold compat_bool; Intros; Apply (f_equal ? ? negb); Auto. +Qed. + +Lemma exists_mem_1: + (s:t)((x:elt)(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. +Symmetry;Apply negb_sym;Simpl;Auto. +Qed. + +Lemma exists_mem_2: + (s:t)(exists f s)=false -> (x:elt)(mem x s)=true -> (f x)=false. +Proof. +Intros. +Rewrite for_all_exists in H. +Replace false with (negb true);Auto;Apply negb_sym;Symmetry. +Rewrite (for_all_mem_2 1) Comp' 3!s);Simpl;Auto. +Replace true with (negb false);Auto;Apply negb_sym;Auto. +Qed. + +Lemma exists_mem_3: + (s:t)(x:elt)(mem x s)=true -> (f x)=true -> (exists f s)=true. +Proof. +Intros. +Rewrite for_all_exists. +Symmetry;Apply negb_sym;Simpl. +Apply for_all_mem_3 with x;Auto. +Rewrite H0;Auto. +Qed. + +Lemma exists_mem_4: + (s:t)(exists f s)=true -> {x:elt | (mem x s)=true /\ (f x)=true}. +Proof. +Intros. +Rewrite for_all_exists in H. +Elim (for_all_mem_4 1) Comp' 3!s);Intros. +Elim p;Intros. +Exists x;Split;Auto. +Replace true with (negb false);Auto;Apply negb_sym;Auto. +Replace false with (negb true);Auto;Apply negb_sym;Auto. +Qed. + +End Exists. + +Section Sum. + + +Definition sum := [f:elt -> nat; s:t](fold [x](plus (f x)) s 0). + +Definition compat_nat := [A:Set][eqA:A->A->Prop][f:A->nat] + (x,x':A)(eqA x x') -> (f x)=(f x'). +Hints Unfold compat_nat. + +Lemma sum_plus : + (f,g:elt ->nat)(compat_nat E.eq f) -> (compat_nat E.eq g) -> + (s:t)(sum [x]((f x)+(g x)) s) = (sum f s)+(sum g s). +Proof. +Unfold sum. +Intros f g Hf Hg. +Assert fc : (compat_op E.eq (eq ?) [x:elt](plus (f x))). Auto. +Assert ft : (transpose (eq ?) [x:elt](plus (f x))). Red; Intros; Omega. +Assert gc : (compat_op E.eq (eq ?) [x:elt](plus (g x))). Auto. +Assert gt : (transpose (eq ?) [x:elt](plus (g x))). Red; Intros; Omega. +Assert fgc : (compat_op E.eq (eq ?) [x:elt](plus ((f x)+(g x)))). Auto. +Assert fgt : (transpose (eq ?) [x:elt](plus ((f x)+(g x)))). Red; Intros; Omega. +Assert st := (gen_st nat). +Intros s;Pattern s; Apply set_ind. +Intros. +Rewrite <- (fold_equal st O fc ft H). +Rewrite <- (fold_equal st O gc gt H). +Rewrite <- (fold_equal st O fgc fgt H); Auto. +Assert fold_add' := [s:t; t:elt](!fold_add s t ?? st). +Intros; Do 3 (Rewrite fold_add';Auto). +Rewrite H0;Simpl;Omega. +Intros; Do 3 Rewrite (fold_empty st);Auto. +Qed. + +Lemma filter_equal : (f:elt -> bool)(compat_bool E.eq f) -> + (s,s':t)(Equal s s') -> (Equal (filter f s) (filter f s')). +Proof. +Unfold Equal; Split; Intros; Elim (H0 a); Intros; Apply filter_3; EAuto. +Qed. + +Lemma add_filter_1 : (f:elt -> bool)(compat_bool E.eq f) -> + (s,s':t)(x:elt) (f x)=true -> (Add x s s') -> (Add x (filter f s) (filter f s')). +Proof. +Unfold Add; Split; Intros; Elim (H1 y); Clear H1; Intros. +Elim H1; [ Auto | Right; EAuto | EAuto ]. +Apply filter_3; Auto. +Elim H2; Intros. +Intuition. +Apply H3; Right; EAuto. +Elim H2; Intros. +Rewrite <- H0; Auto. +EAuto. +Qed. + +Lemma add_filter_2 : (f:elt -> bool)(compat_bool E.eq f) -> + (s,s':t)(x:elt) (f x)=false -> (Add x s s') -> (Equal (filter f s) (filter f s')). +Proof. +Unfold Add Equal; Split; Intros; Elim (H1 a); Clear H1; Intros. +Elim H1; Intros. +Absurd true=false; Auto with bool. +Rewrite <- H0. +Rewrite <- (filter_2 H H2); Auto. +Apply filter_3; EAuto. +Apply H3; Right; EAuto. + +Elim H1; Intros. +Absurd true=false; Auto with bool. +Rewrite <- H0. +Rewrite <- (filter_2 H H2); Auto. +EAuto. +EAuto. +Qed. + +Lemma sum_filter : (f:elt -> bool)(compat_bool E.eq f) -> + (s:t)(sum [x](if (f x) then 1 else 0) s) = (cardinal (filter f s)). +Proof. +Unfold sum; Intros f Hf. +Assert st := (gen_st nat). +Assert fold_add' := [s:t; t:elt](!fold_add s t ?? st). +Assert cc : (compat_op E.eq (eq ?) [x:elt](plus (if (f x) then 1 else 0))). + Unfold compat_op; Intros. + Rewrite (Hf x x' H); Auto. +Assert ct : (transpose (eq ?) [x:elt](plus (if (f x) then 1 else 0))). + Unfold transpose; Intros; Omega. +Intros s;Pattern s; Apply set_ind. +Intros. +Rewrite <- (fold_equal st O cc ct H). +Rewrite <- (Equal_cardinal (filter_equal Hf (equal_2 H))); Auto. +Intros; Rewrite fold_add'; 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; Intuition. +Rewrite (cardinal_2 H1 (H4 (Add_add s0 x))); Auto. +Rewrite <- (Equal_cardinal (H4 (Add_add s0 x))); Auto. +Intros; Rewrite (fold_empty st);Auto. +Rewrite cardinal_1; Auto. +Unfold Empty; Intuition. +Elim (!empty_1 a); EAuto. +Qed. + +Lemma fold_compat : + (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA)) + (f,g:elt->A->A) + (compat_op E.eq eqA f) -> (transpose eqA f) -> + (compat_op E.eq eqA g) -> (transpose eqA g) -> + (i:A)(s:t)((x:elt)(In x s) -> (y:A)(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_ind; Intros. +Apply (Seq_trans ?? st) with (fold f s0 i). +Apply fold_equal with eqA:=eqA; Auto. +Rewrite equal_sym; Auto. +Apply (Seq_trans ?? st) with (fold g s0 i). +Apply H0; Intros; Apply H1; Auto. +Elim (equal_2 H x); Intuition. +Apply fold_equal with eqA:=eqA; Auto. +Apply (Seq_trans ?? st) with (f x (fold f s0 i)). +Apply fold_add with eqA:=eqA; Auto. +Apply (Seq_trans ?? st) with (g x (fold f s0 i)). +Apply H1; Auto with set. +Apply (Seq_trans ?? st) with (g x (fold g s0 i)). +Apply gc; Auto. +Apply Seq_sym; Auto; Apply fold_add with eqA:=eqA; Auto. +Apply (Seq_trans ?? st) with i; [Idtac | Apply Seq_sym; Auto]; Apply fold_empty; Auto. +Qed. + +Lemma sum_compat : + (f,g:elt->nat)(compat_nat E.eq f) -> (compat_nat E.eq g) -> + (s:t)((x:elt)(In x s) -> (f x)=(g x)) -> (sum f s)=(sum g s). +Intros. +Unfold sum; Apply (!fold_compat ? (eq nat)); Auto. +Unfold transpose; Intros; Omega. +Unfold transpose; Intros; Omega. +Qed. + +End Sum. + +Lemma filter_orb: (f,g:elt->bool)(compat_bool E.eq f) -> (compat_bool E.eq g) -> + (s:t)(Equal (filter [x:elt](orb (f x) (g x)) s) (union (filter f s) (filter g s))). +Proof. +Intros. +Assert (compat_bool E.eq [x](orb (f x) (g x))). + Unfold compat_bool; Intros. + Rewrite (H x y H1). + Rewrite (H0 x y H1); Auto. +Unfold Equal; Split; Intros. +Assert H3 := (filter_1 H1 H2). +Assert H4 := (filter_2 H1 H2). +Elim (orb_prop ?? H4); Intros; EAuto. +Elim (union_1 H2); Intros. +Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H H3); Auto ]. +Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H0 H3); Auto with bool]. +Qed. + +End MoreProperties. +Hints Unfold compat_nat. + +End Properties. diff --git a/theories/FSets/FSetRBT.v b/theories/FSets/FSetRBT.v new file mode 100644 index 0000000000..c91dc719a1 --- /dev/null +++ b/theories/FSets/FSetRBT.v @@ -0,0 +1,2163 @@ + (***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(** This module implements sets using red-black trees *) + +Require FSetInterface. +Require FSetList. +Require FSetBridge. + +Require Omega. +Require ZArith. + +Import Z_scope. +Open Scope Z_scope. + +Notation "[]" := (nil ?) (at level 1). +Notation "a :: l" := (cons a l) (at level 1, l at next level). + +Module Make [X : OrderedType] <: Sdep with Module E := X. + + Module E := X. + Module ME := MoreOrderedType X. + + Definition elt := X.t. + + (** * Red-black trees *) + + Inductive color : Set := red : color | black : color. + + Inductive tree : Set := + | Leaf : tree + | Node : color -> tree -> X.t -> tree -> tree. + + (** * Occurrence in a tree *) + + Inductive In_tree [x:elt] : tree -> Prop := + | IsRoot : (l,r:tree)(c:color)(y:elt) + (X.eq x y) -> (In_tree x (Node c l y r)) + | InLeft : (l,r:tree)(c:color)(y:elt) + (In_tree x l) -> (In_tree x (Node c l y r)) + | InRight : (l,r:tree)(c:color)(y:elt) + (In_tree x r) -> (In_tree x (Node c l y r)). + + Hint In_tree := Constructors In_tree. + + (** [In_tree] is color-insensitive *) + + Lemma In_color : (c,c':color)(x,y:elt)(l,r:tree) + (In_tree y (Node c l x r)) -> (In_tree y (Node c' l x r)). + Proof. + Inversion 1; Auto. + Save. + Hints Resolve In_color. + + (** * Binary search trees *) + + (** [lt_tree x s]: all elements in [s] are smaller than [x] + (resp. greater for [gt_tree]) *) + + Definition lt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt y x). + Definition gt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt x y). + + Hints Unfold lt_tree gt_tree. + + (** Results about [lt_tree] and [gt_tree] *) + + Lemma lt_leaf : (x:elt)(lt_tree x Leaf). + Proof. + Unfold lt_tree; Intros; Inversion H. + Save. + + Lemma gt_leaf : (x:elt)(gt_tree x Leaf). + Proof. + Unfold gt_tree; Intros; Inversion H. + Save. + + Lemma lt_tree_node : (x,y:elt)(l,r:tree)(c:color) + (lt_tree x l) -> (lt_tree x r) -> (X.lt y x) -> + (lt_tree x (Node c l y r)). + Proof. + Unfold lt_tree; Intuition. + Inversion_clear H2; Intuition. + Apply ME.eq_lt with y; Auto. + Save. + + Lemma gt_tree_node : (x,y:elt)(l,r:tree)(c:color) + (gt_tree x l) -> (gt_tree x r) -> (E.lt x y) -> + (gt_tree x (Node c l y r)). + Proof. + Unfold gt_tree; Intuition. + Inversion_clear H2; Intuition. + Apply ME.lt_eq with y; Auto. + Save. + + Hints Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. + + Lemma lt_node_lt : (x,y:elt)(l,r:tree)(c:color) + (lt_tree x (Node c l y r)) -> (E.lt y x). + Proof. + Intros; Apply H; Auto. + Save. + + Lemma gt_node_gt : (x,y:elt)(l,r:tree)(c:color) + (gt_tree x (Node c l y r)) -> (E.lt x y). + Proof. + Intros; Apply H; Auto. + Save. + + Lemma lt_left : (x,y:elt)(l,r:tree)(c:color) + (lt_tree x (Node c l y r)) -> (lt_tree x l). + Proof. + Intros; Red; Intros; Apply H; Auto. + Save. + + Lemma lt_right : (x,y:elt)(l,r:tree)(c:color) + (lt_tree x (Node c l y r)) -> (lt_tree x r). + Proof. + Intros; Red; Intros; Apply H; Auto. + Save. + + Lemma gt_left : (x,y:elt)(l,r:tree)(c:color) + (gt_tree x (Node c l y r)) -> (gt_tree x l). + Proof. + Intros; Red; Intros; Apply H; Auto. + Save. + + Lemma gt_right : (x,y:elt)(l,r:tree)(c:color) + (gt_tree x (Node c l y r)) -> (gt_tree x r). + Proof. + Intros; Red; Intros; Apply H; Auto. + Save. + + Hints Resolve lt_node_lt gt_node_gt + lt_left lt_right gt_left gt_right. + + Lemma lt_tree_not_in : + (x:elt)(t:tree)(lt_tree x t) -> ~(In_tree x t). + Proof. + Unfold lt_tree; Intros; Red; Intros. + Generalize (H x H0); Intro; Absurd (X.lt x x); Auto. + Save. + + Lemma lt_tree_trans : + (x,y:elt)(X.lt x y) -> (t:tree)(lt_tree x t) -> (lt_tree y t). + Proof. + Unfold lt_tree; Ground EAuto. + Save. + + Lemma gt_tree_not_in : + (x:elt)(t:tree)(gt_tree x t) -> ~(In_tree x t). + Proof. + Unfold gt_tree; Intros; Red; Intros. + Generalize (H x H0); Intro; Absurd (X.lt x x); Auto. + Save. + + Lemma gt_tree_trans : + (x,y:elt)(X.lt y x) -> (t:tree)(gt_tree x t) -> (gt_tree y t). + Proof. + Unfold gt_tree; Ground EAuto. + Save. + + Hints Resolve lt_tree_not_in lt_tree_trans + gt_tree_not_in gt_tree_trans. + + (** [bst t] : [t] is a binary search tree *) + + Inductive bst : tree -> Prop := + | BSLeaf : + (bst Leaf) + | BSNode : (x:elt)(l,r:tree)(c:color) + (bst l) -> (bst r) -> + (lt_tree x l) -> (gt_tree x r) -> + (bst (Node c l x r)). + + Hint bst := Constructors bst. + + (** Results about [bst] *) + + Lemma bst_left : (x:elt)(l,r:tree)(c:color) + (bst (Node c l x r)) -> (bst l). + Proof. + Intros x l r c H; Inversion H; Auto. + Save. + + Lemma bst_right : (x:elt)(l,r:tree)(c:color) + (bst (Node c l x r)) -> (bst r). + Proof. + Intros x l r c H; Inversion H; Auto. + Save. + + Implicits bst_left. Implicits bst_right. + Hints Resolve bst_left bst_right. + + Lemma bst_color : (c,c':color)(x:elt)(l,r:tree) + (bst (Node c l x r)) -> (bst (Node c' l x r)). + Proof. + Inversion 1; Auto. + Save. + Hints Resolve bst_color. + + (** Key fact about binary search trees: rotations preserve the + [bst] property *) + + Lemma rotate_left : (x,y:elt)(a,b,c:tree)(c1,c2,c3,c4:color) + (bst (Node c1 a x (Node c2 b y c))) -> + (bst (Node c3 (Node c4 a x b) y c)). + Proof. + Intros; Inversion H; Intuition. + Constructor; Intuition. + Constructor; EAuto. + EAuto. + Apply lt_tree_node; Intuition. + Apply lt_tree_trans with x; Auto. + Inversion H5; Auto. + Inversion H5; Auto. + Save. + + Lemma rotate_right : (x,y:elt)(a,b,c:tree)(c1,c2,c3,c4:color) + (bst (Node c3 (Node c4 a x b) y c)) -> + (bst (Node c1 a x (Node c2 b y c))). + Proof. + Intros; Inversion H; Intuition. + Constructor; Intuition. + EAuto. + Constructor; Auto. + Inversion H4; Auto. + Inversion H4; Auto. + Apply gt_tree_node; Intuition. + Inversion H4; Auto. + Apply gt_tree_trans with y; Auto. + EAuto. + Save. + + Hints Resolve rotate_left rotate_right. + + (** * Balanced red-black trees *) + + (** [rbtree n t]: [t] is a properly balanced red-black tree, i.e. it + satisfies the following two invariants: + - a red node has no red son + - any path from the root to a leaf has exactly [n] black nodes *) + + Definition is_not_red [t:tree] := Cases t of + | Leaf => True + | (Node black x0 x1 x2) => True + | (Node red x0 x1 x2) => False + end. + + Hints Unfold is_not_red. + + Inductive rbtree : nat -> tree -> Prop := + | RBLeaf : + (rbtree O Leaf) + | RBRed : (x:elt)(l,r:tree)(n:nat) + (rbtree n l) -> (rbtree n r) -> + (is_not_red l) -> (is_not_red r) -> + (rbtree n (Node red l x r)) + | RBBlack : (x:elt)(l,r:tree)(n:nat) + (rbtree n l) -> (rbtree n r) -> + (rbtree (S n) (Node black l x r)). + + Hint rbtree := Constructors rbtree. + + (** Results about [rbtree] *) + + Lemma rbtree_left : + (x:elt)(l,r:tree)(c:color) + (EX n:nat | (rbtree n (Node c l x r))) -> + (EX n:nat | (rbtree n l)). + Proof. + Intros x l r c (n,Hn); Inversion_clear Hn; Intuition EAuto. + Save. + + Lemma rbtree_right : + (x:elt)(l,r:tree)(c:color) + (EX n:nat | (rbtree n (Node c l x r))) -> + (EX n:nat | (rbtree n r)). + Proof. + Intros x l r c (n,Hn); Inversion_clear Hn; Intuition EAuto. + Save. + + Implicits rbtree_left. Implicits rbtree_right. + Hints Resolve rbtree_left rbtree_right. + + (** * Sets as red-black trees *) + + (** A set is implement as a record [t], containing a tree, + a proof that it is a binary search tree and a proof that it is + a properly balanced red-black tree *) + + Record t_ : Set := t_intro { + the_tree :> tree; + is_bst : (bst the_tree); + is_rbtree : (EX n:nat | (rbtree n the_tree)) }. + Definition t := t_. + + (** * Rotations *) + + Lemma t_is_bst : (s:t)(bst s). + Proof. + Destruct s; Auto. + Save. + Hints Resolve t_is_bst. + + (** * Logical appartness *) + + Definition In : elt -> t -> Prop := [x:elt][s:t](In_tree x s). + + 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)). + + Lemma eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s). + Proof. + Unfold In; Destruct s; Simpl; Intuition Clear is_bst0 is_rbtree0. + Induction the_tree0; Inversion_clear H0; Intuition. + Apply IsRoot; EAuto. + Save. + + Hints Resolve eq_In. + + (** * Empty set *) + + Definition t_empty : t. + Proof. + Exists Leaf; Auto; Exists O; Auto. + Defined. + + Definition empty : { s:t | (x:elt)~(In x s) }. + Proof. + Exists t_empty. + Unfold In; Red; Intros. + Inversion H. + Defined. + + (** * Emptyness test *) + + Definition is_empty : (s:t){ Empty s }+{ ~(Empty s) }. + Proof. + Unfold Empty In; Destruct s; Destruct the_tree0; Simpl; Intros. + Left; Auto. + Right; Intuition. + Apply (H t1); Auto. + Defined. + + (** * Appartness *) + + (** The [mem] function is deciding appartness. It exploits the [bst] property + to achieve logarithmic complexity. *) + + Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }. + Proof. + Intros x (s,Hs,Hrb). + Unfold In; Simpl; Clear Hrb. + Generalize Hs; Elim s; Simpl; Intros. + (* Leaf *) + Right. + Unfold In; Red; Intros; Inversion H. + (* Node *) + Elim (X.compare x t1); Intro. + (* lt x t1 *) + Case H; Intros. + EAuto. + Left; Auto. + Right; Intro. + Inversion H1; Intuition. + Absurd (X.eq x t1); Auto. + Inversion Hs0. + Absurd (In_tree x t2); EAuto. + (* eq x t1 *) + Left; Auto. + (* lt t1 x *) + Case H0; Intros. + EAuto. + Left; Auto. + Right; Intro. + Inversion H1; Intuition. + Absurd (X.eq t1 x); Auto. + Inversion Hs0. + Absurd (In_tree x t0); EAuto. + Defined. + + (** * Singleton set *) + + Definition singleton_tree [x:elt] := (Node red Leaf x Leaf). + + Lemma singleton_bst : (x:elt)(bst (singleton_tree x)). + Proof. + Unfold singleton_tree; Auto. + Save. + + Lemma singleton_rbtree : (x:elt)(EX n:nat | (rbtree n (singleton_tree x))). + Proof. + Unfold singleton_tree; EAuto. + Save. + + Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}. + Proof. + Intro x; Exists (t_intro (singleton_tree x) (singleton_bst x) + (singleton_rbtree x)). + Unfold In singleton_tree; Simpl; Intuition. + Inversion_clear H; Auto; Inversion H0. + Defined. + + (** * Insertion *) + + (** [almost_rbtree n t]: [t] may have one red-red conflict at its root; + it satisfies [rbtree n] everywhere else *) + + Inductive almost_rbtree : nat -> tree -> Prop := + | ARBLeaf : + (almost_rbtree O Leaf) + | ARBRed : (x:elt)(l,r:tree)(n:nat) + (rbtree n l) -> (rbtree n r) -> + (almost_rbtree n (Node red l x r)) + | ARBBlack : (x:elt)(l,r:tree)(n:nat) + (rbtree n l) -> (rbtree n r) -> + (almost_rbtree (S n) (Node black l x r)). + + Hint almost_rbtree := Constructors almost_rbtree. + + (** Results about [almost_rbtree] *) + + Lemma rbtree_almost_rbtree : + (n:nat)(t:tree)(rbtree n t) -> (almost_rbtree n t). + Proof. + Destruct 1; Intuition. + Save. + + Hints Resolve rbtree_almost_rbtree. + + Lemma rbtree_almost_rbtree_ex : (s:tree) + (EX n:nat | (rbtree n s)) -> (EX n:nat | (almost_rbtree n s)). + Proof. + Intros s (n,Hn); Exists n; Auto. + Save. + + Hints Resolve rbtree_almost_rbtree_ex. + + Lemma almost_rbtree_rbtree_black : (x:elt)(l,r:tree)(n:nat) + (almost_rbtree n (Node black l x r)) -> + (rbtree n (Node black l x r)). + Proof. + Inversion 1; Auto. + Save. + Hints Resolve almost_rbtree_rbtree_black. + + (** Balancing functions [lbalance] and [rbalance] (see below) require + a rather complex pattern-matching; it is realized by the following + function [conflict] which returns in the sum type [Conflict] *) + + Inductive Conflict [s:tree] : Set := + | NoConflict : + ((n:nat) (almost_rbtree n s) -> (rbtree n s)) -> + (Conflict s) + | RedRedConflict : + (a,b,c:tree)(x,y:elt) + (bst a) -> (bst b) -> (bst c) -> + (lt_tree x a) -> (gt_tree x b) -> + (lt_tree y b) -> (gt_tree y c) -> (X.lt x y) -> + ((z:elt)(In_tree z s) <-> + ((X.eq z x) \/ (X.eq z y) \/ + (In_tree z a) \/ (In_tree z b) \/ (In_tree z c))) -> + ((n:nat)(almost_rbtree n s) -> + ((rbtree n a) /\ (rbtree n b) /\ (rbtree n c))) -> + (Conflict s). + + Definition conflict : (s:tree)(bst s) -> (Conflict s). + Proof. + Destruct s; Intros. + (* s = Leaf *) + Constructor 1; Inversion 1; Auto. + (* s = Node c t0 t1 t2 *) + Induction c. + (* s = Node red t0 t1 t2 *) + Generalize H; Clear H; Case t0; Intros. + (* s = Node red Leaf t1 t2 *) + Generalize H; Clear H; Case t2; Intros. + (* s = Node red Leaf t1 Leaf *) + Constructor 1; Inversion_clear 1; Intros. + Constructor; Intuition. + (* s = Node red Leaf t1 (Node c t3 t4 t5) *) + Induction c. + (* s = Node red Leaf t1 (Node red t3 t4 t5) *) + Constructor 2 with a:=Leaf b:=t3 c:=t5 x:=t1 y:=t4; Intuition; + Solve [ Inversion_clear H; Auto; Inversion_clear H1; Auto | + Inversion_clear H0; Auto; Inversion_clear H2; Auto | + Inversion_clear H0; Auto; Inversion_clear H1; Auto | + Inversion_clear H1; Auto ]. + (* s = Node red Leaf t1 (Node black t3 t4 t5) *) + Constructor 1; Inversion_clear 1; Intros. + Constructor; Intuition. + (* s = Node red (Node c t3 t4 t5) t1 t2 *) + Induction c. + (* s = Node red (Node red t3 t4 t5) t1 t2 *) + Constructor 2 with a:=t3 b:=t5 c:=t2 x:=t4 y:=t1; Intuition; + Solve [ Inversion_clear H; Auto; Inversion_clear H0; Auto | + Inversion_clear H0; Auto; Inversion_clear H1; Auto | + Inversion_clear H1; Auto ]. + (* s = Node red (Node black t3 t4 t5) t1 t2 *) + Generalize H; Clear H; Case t2; Intros. + (* s = Node red (Node black t3 t4 t5) t1 Leaf *) + Constructor 1; Inversion_clear 1; Intros. + Constructor; Intuition. + (* s = Node red (Node black t3 t4 t5) t1 (Node c t6 t7 t8) *) + Induction c. + (* s = Node red (Node black t3 t4 t5) t1 (Node red t6 t7 t8) *) + Constructor 2 with a:=(Node black t3 t4 t5) + b:=t6 c:=t8 x:=t1 y:=t7; Intuition; + Solve [ Inversion_clear H; Auto; Inversion_clear H1; Auto | + Inversion_clear H0; Auto; Inversion_clear H2; Auto | + Inversion_clear H0; Auto; Inversion_clear H1; Auto | + Inversion_clear H1; Auto ]. + (* s = Node red (Node black t3 t4 t5) t1 (Node black t6 t7 t8) *) + Constructor 1; Inversion_clear 1; Intros. + Constructor; Intuition. + (* s = Node black t0 t1 t2 *) + Constructor 1; Inversion_clear 1; Intros. + Constructor; Intuition. + Defined. + + (** [lbalance c x l r] acts as a black node constructor, + solving a possible red-red conflict on [l], using the following + schema: +<< + B (R (R a x b) y c) z d + B (R a x (R b y c)) z d -> R (B a x b) y (R c z d) + B a x b -> B a x b +>> + The result is not necessarily a black node. *) + + Definition lbalance : + (l:tree)(x:elt)(r:tree) + (lt_tree x l) -> (gt_tree x r) -> + (bst l) -> (bst r) -> + { s:tree | + (bst s) /\ + ((n:nat)((almost_rbtree n l) /\ (rbtree n r)) -> + (rbtree (S n) s)) /\ + (y:elt)(In_tree y s) <-> ((E.eq y x)\/(In_tree y l)\/(In_tree y r)) }. + Proof. + Intros; Case (conflict l). + Assumption. + (* no conflict *) + Exists (Node black l x r); Intuition. + Inversion H3; Auto. + (* red red conflict *) + Intros; Exists (Node red (Node black a x0 b) y + (Node black c x r)); Intuition. + Constructor; Intuition. + Constructor; Intuition. + Intro z; Generalize (i z); Intuition. + Apply lt_tree_node; Intuition. + Apply lt_tree_trans with x0; Auto. + Assert (In_tree y l). Ground. + Apply gt_tree_node; Intuition. + Intro z; Generalize (i z); Intuition. + Apply X.lt_trans with x; Auto. + Apply H; Assumption. + Generalize (a0 n H4); Constructor; Intuition. + Generalize (i y0); Inversion_clear H3; Intuition; + Inversion_clear H4; Intuition. + (* bug Ground *) Generalize (i y0); Intuition. + Defined. + + (** [rbalance l x r] is similar to [lbalance], solving a possible red-red + conflict on [r]. The balancing schema is similar: +<< + B a x (R (R b y c) z d) + B a x (R b y (R c z d)) -> R (B a x b) y (R c z d) + B a x b -> B a x b +>> *) + + Definition rbalance : + (l:tree)(x:elt)(r:tree) + (lt_tree x l) -> (gt_tree x r) -> + (bst l) -> (bst r) -> + { s:tree | + (bst s) /\ + ((n:nat)((almost_rbtree n r) /\ (rbtree n l)) -> + (rbtree (S n) s)) /\ + (y:elt)(In_tree y s) <-> ((E.eq y x)\/(In_tree y l)\/(In_tree y r)) }. + Proof. + Intros; Case (conflict r). + Assumption. + (* no conflict *) + Exists (Node black l x r); Intuition. + Inversion H3; Auto. + (* red red conflict *) + Intros; Exists (Node red (Node black l x a) x0 + (Node black b y c)); Intuition. + Constructor; Intuition. + Constructor; Intuition. + Intro z; Generalize (i z); Intuition. + Assert (X.lt x x0). + Assert (In_tree x0 r). Ground. + Apply H0; Assumption. + Apply lt_tree_node; Intuition. + Apply lt_tree_trans with x; Auto. + Apply gt_tree_node; Intuition. + Apply gt_tree_trans with y; Auto. + Generalize (a0 n H4); Constructor; Intuition. + Generalize (i y0); Inversion_clear H3; Intuition; + Inversion_clear H4; Intuition. + (* bug Ground *) Generalize (i y0); Intuition. + Defined. + + (** [insert x s] inserts [x] in tree [s], resulting in a possible top red-red + conflict when [s] is red. Its code is: +<< + insert x Empty = + Node red Empty x Empty + insert x (Node red a y b) = + if lt x y then Node red (insert x a) y b + else if lt y x then Node red a y (insert x b) + else (Node c a y b) + insert x (Node black a y b) = + if lt x y then lbalance (insert x a) y b + else if lt y x then rbalance a y (insert x b) + else (Node c a y b) +>> *) + + Definition insert : + (x:elt) (s:t) + { s':tree | (bst s') /\ + ((n:nat)(rbtree n s) -> + ((almost_rbtree n s') /\ + ((is_not_red s) -> (rbtree n s')))) /\ + (y:elt)(In_tree y s') <-> ((E.eq y x) \/ (In_tree y s)) }. + Proof. + Intros x (s,Hs,Hrb). + Generalize Hs Hrb; Clear Hs Hrb; Induction s; Simpl; Intros. + (* Empty *) + Exists (singleton_tree x); Unfold singleton_tree; Simpl; Intuition. + Inversion H; EAuto. + (* Node c t0 t1 t2 *) + Simpl in Hrecs0 Hrecs1. + Induction c. + (* c = red => usual insertion in BST *) + Elim (X.compare x t0); Intro. + (* lt x t1 *) + Clear Hrecs0; Case Hrecs1; Clear Hrecs1; Intros. EAuto. EAuto. + Intuition. + Exists (Node red x0 t0 s0); Intuition. + Constructor; Intuition. + Inversion Hs; Auto. + Red; Intros. + Generalize (H2 y); Intuition. + Apply ME.eq_lt with x; Auto. + Inversion Hs; Auto. + Inversion Hs; Auto. + Inversion_clear H0; Generalize (H1 n); Intuition. (* BUG Ground *) + Generalize (H2 y); Inversion H0; Intuition. + Generalize (H2 y); Intuition. + Generalize (H2 y); Inversion H3; Intuition. + (* eq x t1 *) + Clear Hrecs1 Hrecs0. + Exists (Node red s1 t0 s0); Intuition. + Apply IsRoot; EAuto. + (* lt t1 x *) + Clear Hrecs1; Case Hrecs0; Clear Hrecs0; Intros. EAuto. EAuto. + Intuition. + Exists (Node red s1 t0 x0); Intuition. + Constructor; Intuition. + Inversion Hs; Auto. + Inversion Hs; Auto. + Red; Intros. + Generalize (H2 y); Intuition. + Apply ME.lt_eq with x; Auto. + Inversion Hs; Auto. + Inversion_clear H0; (* bug Ground *) Generalize (H1 n); Intuition. + Generalize (H2 y); Inversion H0; Intuition. + Generalize (H2 y); Intuition. + Generalize (H2 y); Inversion H3; Intuition. + + (* c = black => same code using smart constructors *) + Elim (X.compare x t0); Intro. + (* lt x t1 *) + Clear Hrecs0; Case Hrecs1; Clear Hrecs1; Intros. EAuto. EAuto. + Intuition. + Case (lbalance x0 t0 s0); Intuition. + Red; Intros. + Generalize (H2 y); Intuition. + Apply ME.eq_lt with x; Auto. + Inversion Hs; Auto. + Inversion Hs; Auto. + Inversion Hs; Auto. + Exists x1; Intuition. + Inversion_clear H3; Ground. + Inversion_clear H3; Ground. + Generalize (H2 y); Generalize (H5 y); Intuition. + Generalize (H2 y); Generalize (H5 y); Intuition. + Inversion H6; Generalize (H2 y); Generalize (H5 y); Intuition. + (* eq x t1 *) + Clear Hrecs1 Hrecs0. + Exists (Node black s1 t0 s0); Intuition. + Apply IsRoot; EAuto. + (* lt t1 x *) + Clear Hrecs1; Case Hrecs0; Clear Hrecs0; Intros. EAuto. EAuto. + Intuition. + Case (rbalance s1 t0 x0); Intuition. + Inversion Hs; Auto. + Red; Intros. + Generalize (H2 y); Intuition. + Apply ME.lt_eq with x; Auto. + Inversion Hs; Auto. + Inversion Hs; Auto. + Exists x1; Intuition. + Inversion_clear H3; Ground. + Inversion_clear H3; Ground. + Generalize (H2 y); Generalize (H5 y); Intuition. + Generalize (H2 y); Generalize (H5 y); Intuition. + Inversion H6; Generalize (H2 y); Generalize (H5 y); Intuition. + Defined. + + + (** Finally [add x s] calls [insert] and recolors the root as black: +<< + add x s = match insert x s with + | Node _ a y b -> Node black a y b + | Empty -> assert false (* absurd *) +>> *) + + Definition add : (x:elt) (s:t) { s':t | (Add x s s') }. + Proof. + Intros x s; Case (insert x s). + Elim s; Clear s; Intros s Hbs Hrb; + Simpl; Destruct x0; Intuition. + (* Leaf => absurd *) + Absurd (In_tree x Leaf). + Intro; Inversion H0. + Ground. + (* Node c t0 t1 t2 *) + Induction c. + (* c = red => changed to black *) + LetTac s' := (Node black t0 t1 t2). + Assert s'bst: (bst s'). + Unfold s'; EAuto. + Assert s'rbtree: (EX n:nat | (rbtree n s')). + Elim Hrb; Clear Hrb; Intros n Hrb. + Generalize (H1 n Hrb); Intuition. + Exists (S n); Unfold s'. + Inversion H3; Auto. + Exists (t_intro s' s'bst s'rbtree); + Unfold s' Add In; Simpl. + Intro y; Generalize (H2 y); Clear H2; Intuition; + Try (Apply In_color with red; Assumption). + Assert (In_tree y (Node red t0 t1 t2)); Auto. + Apply In_color with black; Assumption. + (* c = black => unchanged *) + Assert s'rbtree: (EX n:nat | (rbtree n (Node black t0 t1 t2))). + Elim Hrb; Clear Hrb; Intros n Hrb. + Exists n; Ground. + Exists (t_intro (Node black t0 t1 t2) H s'rbtree); Intuition. + Defined. + + (** * Deletion *) + + (* [UnbalancedLeft n t]: [t] is a tree of black height [S n] + on its left side and [n] on its right side (the root color + is taken into account, whathever it is) *) + + Inductive UnbalancedLeft : nat -> tree -> Prop := + | ULRed : (x:elt)(l,r:tree)(n:nat) + (rbtree (S n) l) -> (rbtree n r) -> + (is_not_red l) -> + (UnbalancedLeft n (Node red l x r)) + | ULBlack : (x:elt)(l,r:tree)(n:nat) + (rbtree (S n) l) -> (rbtree n r) -> + (UnbalancedLeft (S n) (Node black l x r)). + + (* when a tree is unbalanced on its left, it can be repared *) + + Definition unbalanced_left : + (s:tree)(bst s) -> + { r : tree * bool | + let (s',b) = r in + (bst s') /\ + ((is_not_red s) /\ b=false -> (is_not_red s')) /\ + ((n:nat)(UnbalancedLeft n s) -> + (if b then (rbtree n s') else (rbtree (S n) s'))) /\ + ((y:elt)(In_tree y s') <-> (In_tree y s)) }. + Proof. + Destruct s. + (* s = Leaf => Absurd *) + Intro; Exists (Leaf,false); Intuition; Inversion H0. + (* s = Node c t0 t1 t2 *) + Induction c. + (* s = Node red t0 t1 t2 *) + Destruct t0. + (* s = Node red Leaf t1 t2 => Absurd *) + Intros; Exists ((Node black Leaf t1 t2), false); Intuition. + Apply bst_color with red; Auto. + Inversion H0. + Inversion H5. + Apply In_color with black; Auto. + Apply In_color with red; Auto. + (* s = Node red (Node c0 t1 t2 t3) t4 t5 *) + Induction c0. + (* s = Node red (Node red t1 t2 t3) t4 t5 => Absurd *) + Intros; Exists ((Node black (Node red t1 t2 t3) t4 t5), false); + Intuition. + Apply bst_color with red; Auto. + Inversion H0; Elim H7. + Apply In_color with black; Auto. + Apply In_color with red; Auto. + (* s = Node red (Node black t1 t2 t3) t4 t5 *) + Intros. + Case (lbalance (Node red t1 t2 t3) t4 t5). + Inversion H; Auto. + Inversion H; Unfold gt_tree; Ground with In_color. + Inversion H; Apply bst_color with black; Auto. + Inversion H; Auto. + Intros t' Ht'; Exists (t',false); Intuition. + Elim H4. + Apply H2; Intuition. + Constructor; Inversion H1; Auto. + Inversion_clear H8; Auto. + Inversion_clear H8; Auto. + Inversion_clear H1; Auto. + Generalize (H3 y); Clear H3; Intuition. + Constructor 2; Ground with In_color. + Inversion_clear H1; Ground with In_color. + (* s = Node black t0 t1 t2 *) + Destruct t0. + (* s = Node black Leaf t1 t2 => Absurd *) + Intros; Exists ((Node black Leaf t1 t2), false); Intuition. + Inversion H0. + Inversion H4. + (* s = Node black (Node c0 t1 t2 t3) t4 t5 *) + Induction c0. + (* s = Node black (Node red t1 t2 t3) t4 t5 *) + Destruct t3. + (* s = Node black (Node red t1 t2 Leaf) t4 t5 => Absurd *) + Intros; Exists ((Node black (Node red t1 t2 Leaf) t4 t5), false); Intuition. + Inversion H0; Inversion H4; Inversion H12. + (* s = Node black (Node red t1 t2 (Node c1 t4 t5 t6)) t7 t8) *) + Induction c1. + (* s = Node black (Node red t1 t2 (Node red t4 t5 t6)) t7 t8) => absurd *) + Intros; Exists ((Node black (Node red t1 t2 (Node red t4 t5 t6)) t7 t8),false); Intuition. + Inversion H0; Inversion H4; Elim H14. + (* s = Node black (Node red t1 t2 (Node black t4 t5 t6)) t7 t8) *) + Intros. + Case (lbalance (Node red t4 t5 t6) t7 t8). + Inversion H; Unfold lt_tree; Ground with In_color. + Inversion H; Auto. + Inversion H; Inversion H4; Apply bst_color with black; Auto. + Inversion H; Auto. + Intros t' Ht'; Exists ((Node black t1 t2 t'),false); Intuition. + Constructor; Intuition. + Inversion_clear H; Inversion_clear H1; Trivial. + Inversion_clear H; Inversion_clear H1; Trivial. + Intro; Generalize (H3 y); Clear H3; Intuition. + Apply ME.lt_eq with t7; Auto. + Inversion_clear H; Apply H9; Auto. + Inversion_clear H; Inversion_clear H5; Apply H13; Ground with In_color. + Inversion_clear H; Apply X.lt_trans with t7; Auto. + Constructor; Intuition. + Inversion_clear H1; Inversion_clear H4; Trivial. + Inversion H1. + Apply H2; Intuition. + Inversion_clear H7; Constructor; Intuition. + Inversion_clear H11; Trivial. + Inversion_clear H11; Trivial. + Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition. + Ground with In_color. + Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition. + Inversion_clear H3; Intuition. + Apply InRight; Apply H5; Apply In_color with black; Trivial. + (* s = Node black (Node black t1 t2 t3) t4 t5 *) + Intros. + Case (lbalance (Node red t1 t2 t3) t4 t5). + Inversion H; Auto. + Inversion H; Auto. + Inversion H; Apply bst_color with black; Auto. + Inversion H; Auto. + Intros t' Ht'; Exists (t',true); Intuition. + Discriminate H5. + Inversion H1. + Apply H2; Intuition. + Constructor. + Inversion_clear H7; Auto. + Inversion_clear H7; Auto. + Generalize (H3 y); Clear H3; Intuition. + Constructor 2; Ground with In_color. + Inversion_clear H1; Ground with In_color. + Defined. + + + (* [UnbalancedRight n t]: [t] is a tree of black height [S n] + on its right side and [n] on its left side (the root color + is taken into account, whathever it is) *) + + Inductive UnbalancedRight : nat -> tree -> Prop := + | URRed : (x:elt)(l,r:tree)(n:nat) + (rbtree n l) -> (rbtree (S n) r) -> + (is_not_red r) -> + (UnbalancedRight n (Node red l x r)) + | URBlack : (x:elt)(l,r:tree)(n:nat) + (rbtree n l) -> (rbtree (S n) r) -> + (UnbalancedRight (S n) (Node black l x r)). + + (* when a tree is unbalanced on its right, it can be repared *) + + Definition unbalanced_right : + (s:tree)(bst s) -> + { r : tree * bool | + let (s',b) = r in + (bst s') /\ + ((is_not_red s) /\ b=false -> (is_not_red s')) /\ + ((n:nat)(UnbalancedRight n s) -> + (if b then (rbtree n s') else (rbtree (S n) s'))) /\ + ((y:elt)(In_tree y s') <-> (In_tree y s)) }. + Proof. + Destruct s. + (* s = Leaf => Absurd *) + Intro; Exists (Leaf,false); Intuition; Inversion H0. + (* s = Node c t0 t1 t2 *) + Induction c. + (* s = Node red t0 t1 t2 *) + Destruct t2. + (* s = Node red t0 t1 Leaf => Absurd *) + Intro; Exists ((Node black t0 t1 Leaf), false); Intuition. + Apply bst_color with red; Auto. + Inversion H0. + Inversion H6. + Apply In_color with black; Auto. + Apply In_color with red; Auto. + (* s = Node red t0 t1 (Node c0 t3 t4 t5) *) + Induction c0. + (* s = Node red t0 t1 (Node red t3 t4 t5) => Absurd *) + Intros; Exists ((Node black t0 t1 (Node red t3 t4 t5)), false); + Intuition. + Apply bst_color with red; Auto. + Inversion H0; Elim H7. + Apply In_color with black; Auto. + Apply In_color with red; Auto. + (* s = Node red t0 t1 (Node black t3 t4 t5) *) + Intros. + Case (rbalance t0 t1 (Node red t3 t4 t5)). + Inversion H; Auto. + Inversion H; Unfold gt_tree; Ground with In_color. + Inversion H; Auto. + Inversion H; Apply bst_color with black; Auto. + Intros t' Ht'; Exists (t',false); Intuition. + Elim H4. + Apply H2; Intuition. + Constructor; Inversion H1; Auto. + Inversion_clear H9; Auto. + Inversion_clear H9; Auto. + Inversion_clear H1; Auto. + Generalize (H3 y); Clear H3; Intuition. + Constructor 3; Ground with In_color. + Inversion_clear H1; Ground with In_color. + (* s = Node black t0 t1 t2 *) + Destruct t2. + (* s = Node black t0 t1 Leaf => Absurd *) + Intro; Exists ((Node black t0 t1 Leaf), false); Intuition. + Inversion H0. + Inversion H6. + (* s = Node black t0 t1 (Node c0 t3 t4 t5) *) + Induction c0. + (* s = Node black t0 t1 (Node red t3 t4 t5) *) + Destruct t3. + (* s = Node black t0 t1 (Node red Leaf t4 t5) => Absurd *) + Intros; Exists ((Node black t0 t1 (Node red Leaf t4 t5)), false); Intuition. + Inversion H0; Inversion H6; Inversion H10. + (* s = Node black t0 t1 (Node red (Node c1 t4 t5 t6) t7 t8) *) + Induction c1. + (* s = Node black t0 t1 (Node red (Node red t4 t5 t6) t7 t8) => Absurd *) + Intros; Exists ((Node black t0 t1 (Node red (Node red t4 t5 t6) t7 t8)),false); Intuition. + Inversion H0; Inversion H6; Elim H13. + (* s = Node black t0 t1 (Node red (Node black t4 t5 t6) t7 t8) *) + Intros. + Case (rbalance t0 t1 (Node red t4 t5 t6)). + Inversion H; Auto. + Inversion H; Unfold gt_tree; Ground with In_color. + Inversion H; Auto. + Inversion H; Inversion H5; Apply bst_color with black; Auto. + Intros t' Ht'; Exists ((Node black t' t7 t8),false); Intuition. + Constructor; Intuition. + Inversion_clear H; Inversion_clear H4; Trivial. + Intro; Generalize (H3 y); Clear H3; Intuition. + Apply ME.eq_lt with t1; Auto. + Inversion_clear H; Apply H10; Auto. + Inversion_clear H; Apply X.lt_trans with t1; Auto. + Inversion_clear H; Inversion_clear H8; Apply H12; Ground with In_color. + Inversion_clear H; Inversion_clear H4; Trivial. + Constructor; Intuition. + Inversion H1. + Apply H2; Intuition. + Inversion_clear H9; Constructor; Intuition. + Inversion_clear H10; Trivial. + Inversion_clear H10; Trivial. + Inversion_clear H1; Inversion_clear H5; Trivial. + Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition. + Ground with In_color. + Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition. + Inversion_clear H3; Intuition. + Apply InLeft; Apply H7; Apply In_color with black; Trivial. + (* s = Node black t0 t1 (Node black t3 t4 t5) *) + Intros. + Case (rbalance t0 t1 (Node red t3 t4 t5)). + Inversion H; Auto. + Inversion H; Unfold gt_tree; Ground with In_color. + Inversion H; Auto. + Inversion H; Apply bst_color with black; Auto. + Intros t' Ht'; Exists (t',true); Intuition. + Discriminate H5. + Inversion H1. + Apply H2; Intuition. + Constructor. + Inversion_clear H9; Auto. + Inversion_clear H9; Auto. + Generalize (H3 y); Clear H3; Intuition. + Constructor 3; Ground with In_color. + Inversion_clear H1; Ground with In_color. + Defined. + + Definition remove_min : + (s:tree)(bst s) -> ~s=Leaf -> + { r : tree * elt * bool | + let (s',r') = r in + let (m,b) = r' in + (bst s') /\ + ((is_not_red s) /\ b=false -> (is_not_red s')) /\ + ((n:nat) (rbtree n s) -> + (if b then (lt O n) /\ (rbtree (pred n) s') else (rbtree n s'))) /\ + ((y:elt)(In_tree y s') -> (E.lt m y)) /\ + ((y:elt)(In_tree y s) <-> (E.eq y m) \/ (In_tree y s')) }. + Proof. + Induction s. + (* s = Leaf => absurd *) + Intuition. + (* s = Node c t0 t1 t2 *) + Destruct t0. + Induction c. + (* s = Node red Leaf t1 t2 *) + Intros; Clear H H0. + Exists (t2,(t1,false)); Simpl; Intuition. + Inversion_clear H1; Auto. + Inversion_clear H; Auto. + Inversion_clear H1; Apply H5; Auto. + Inversion_clear H; Auto; Inversion H0. + (* s = Node black Leaf t1 t2 *) + Destruct t2; Intros; Clear H H0. + (* s = Node black Leaf t1 Leaf *) + Exists (Leaf,(t1,true)); Simpl; Intuition. + Inversion_clear H; Auto with arith. + Inversion_clear H; Auto. + Inversion H. + Inversion_clear H; Auto. + (* s = Node black Leaf t1 (Node c t3 t4 t5) *) + Exists ((Node black t3 t4 t5), (t1,false)); Intuition. + Inversion_clear H1; Apply bst_color with c; Auto. + Induction c. + Inversion_clear H; Inversion_clear H3; Auto. + Inversion_clear H; Inversion H3; Inversion H0. + Rewrite <- H9 in H5; Discriminate H5. + Inversion_clear H1; Apply H5; Apply In_color with black; Auto. + Inversion_clear H; Auto. + Inversion H0. + Right; Apply In_color with c; Auto. + Apply InRight; Apply In_color with black; Auto. + (* s = Node c (Node c0 t1 t2 t3) t4 t5 *) + Intros; Clear H0. + LetTac l := (Node c0 t1 t2 t3). + Case H; Clear H. (* remove_min l = l',m,d *) + Inversion H1; Auto. + Discriminate. + Destruct x; Clear x; Intro l'; Destruct p; Clear p; Intros m d. + Intuition. + Induction d. + (* d = true *) + Case (unbalanced_right (Node c l' t4 t5)). + Inversion H1; Constructor; Auto. + Intro; Ground. + Destruct x; Clear x; Intros t' d'; Intuition. + Exists (t',(m,d')); Repeat Split. + Intuition. + Intuition. + Induction c; Intuition. + (* c = red *) + Assert (lt O n). + Unfold l in H8. + Induction c0; Inversion H8; Try Apply Lt.lt_O_Sn. + Inversion H13; Inversion H17. + Inversion H14; Apply Lt.lt_O_Sn. + Induction d'; Intuition. + (* d' = true *) + Apply H7; Clear H7. + Constructor; Inversion_clear H8; Auto. + Generalize (H0 n); Intuition. + Rewrite <- (Lt.S_pred n O H11); Auto. + (* d' = false *) + Rewrite (Lt.S_pred n O H11); Auto. + Apply H7; Clear H7. + Constructor; Inversion_clear H8; Auto. + Generalize (H0 n); Intuition. + Rewrite <- (Lt.S_pred n O H11); Auto. + (* c = black *) + Assert (le n (1)) \/ (lt (O) (pred n)); [ Omega | Intuition ]. + (* n = 1 => absurd *) + Inversion H8. + Absurd (le n (1)); Auto. + Generalize (H0 n0 H15); Omega. + (* n > 1 *) + Induction d'; Intuition. + (* d' = true *) + Omega. + Apply H7; Clear H7. + Rewrite (Lt.S_pred (pred n) (O) H12); Auto. + Constructor; Inversion H8; Simpl; Auto. + Ground. + Rewrite <- (Lt.S_pred n0 (O)); Auto. Omega. + (* d' = false *) + Rewrite (Lt.S_pred n (O)); Auto. + Apply H7; Clear H7. + Rewrite (Lt.S_pred (pred n) (O) H12); Auto. + Constructor; Inversion H8; Simpl; Auto. + Ground. + Rewrite <- (Lt.S_pred n0 (O)); Auto. Omega. + Omega. + (* ∀ y:elt,(In_tree y t') → E.lt m y *) + Intros y Hy; Generalize (H10 y); Clear H10; Intuition. + Inversion_clear H8. + (* y=t4 *) + Inversion H1. + Apply ME.lt_eq with t4; Auto. + Apply H17; Ground. + (* y in l' *) + Ground. + (* y in t5 *) + Inversion H1. + Apply E.lt_trans with t4; [ Apply H17 | Apply H18]; Ground. + (* (In_tree y (Node c l t4 t5)) → (E.eq y m) ∨ In_tree y t' *) + Generalize (H10 y); Clear H10; Intuition. + Inversion_clear H10. + Ground. + Generalize (H6 y); Clear H6; Intuition. + Ground. + (* ((E.eq y m) ∨ In_tree y t') → In_tree y (Node c l t4 t5) *) + Intuition. + Ground. + Generalize (H10 y); Clear H10; Intuition. + Inversion_clear H8; Ground. + (* d = false *) + Exists ((Node c l' t4 t5),(m,false)); Simpl; Intuition. + Inversion_clear H1; Constructor; Auto. + Intro; Generalize (H6 y); Clear H6; Intuition. + Inversion_clear H3; Constructor; Auto. + Inversion_clear H3; Auto. + Inversion H1. + Apply ME.lt_eq with t4; Auto. + Apply H13; Ground. + Inversion H1. + Apply E.lt_trans with t4; [ Apply H13 | Apply H14 ]; Ground. + Generalize (H6 y); Clear H6; Intuition. + Inversion_clear H3; Intuition. + Ground. + Generalize (H6 y); Clear H6; Intuition. + Inversion_clear H7; Ground. + Defined. + + Definition blackify : + (s:tree)(bst s) -> + { r : tree * bool | + let (s',b) = r in + (is_not_red s') /\ (bst s') /\ + ((n:nat)(rbtree n s) -> + if b then (rbtree n s') else (rbtree (S n) s')) /\ + ((y:elt)(In_tree y s) <-> (In_tree y s')) }. + Proof. + Destruct s; Intros. + (* s = Leaf *) + Exists (Leaf,true); Intuition. + (* s = Node c t0 t1 t2 *) + Induction c; [ Exists ((Node black t0 t1 t2), false) + | Exists ((Node black t0 t1 t2), true) ]; + Intuition (Try Inversion H0; Auto). + Apply bst_color with red; Trivial. + Defined. + + Definition remove_aux : + (x:elt)(s:tree)(bst s) -> + { r : tree * bool | + let (s',b) = r in + (bst s') /\ + ((is_not_red s) /\ b=false -> (is_not_red s')) /\ + ((n:nat) (rbtree n s) -> + (if b then (lt O n) /\ (rbtree (pred n) s') else (rbtree n s'))) /\ + ((y:elt)(In_tree y s') <-> (~(E.eq y x) /\ (In_tree y s))) }. + Proof. + Induction s. + (* s = Leaf *) + Intros; Exists (Leaf, false); Intuition. + Inversion H0. + (* s = Node c t0 t1 t2 *) + Intros. + Case (X.compare x t1); Intro. + (* lt x t1 *) + Clear H0; Case H; Clear H. + Inversion H1; Trivial. + Intros (l',d); Induction d; Intuition. + (* d = true => unbalanced_right *) + Case (unbalanced_right (Node c l' t1 t2)). + Constructor; Inversion_clear H1; Auto. + Intro; Generalize (H4 y); Intuition. + Intros (s',d'); Intros; Exists (s',d'). + Intuition. + Clear H4 H8; Induction c. + Assert (UnbalancedRight (pred n) (Node red l' t1 t2)). + Inversion_clear H6; Generalize (H0 n); Constructor; Intuition. + Rewrite <- (S_pred n O); Trivial. + Induction d'; Intuition. + Inversion_clear H6; Ground. + Rewrite (S_pred n O); Trivial. Apply H5; Trivial. + Inversion_clear H6; Ground. + Assert (UnbalancedRight (pred n) (Node black l' t1 t2)). + Inversion H6; Simpl; Generalize (H0 n0); Intuition. + Rewrite (S_pred n0 O); Trivial. + Constructor; Intuition. + Rewrite <- (S_pred n0 O); Trivial. + Induction d'; Intuition. + Inversion_clear H6; Ground. + Rewrite (S_pred n O); Trivial. Apply H5; Trivial. + Inversion_clear H6; Ground. + (* In_tree y s' -> y <> x *) + Clear H0 H5. + Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H4. + Apply (!E.lt_not_eq x t1); Auto. + Apply E.eq_trans with y; Auto. + Intuition. + Apply (!ME.lt_not_gt y t1); Auto. + Apply ME.eq_lt with x; Trivial. + Inversion_clear H1; Auto. + (* In_tree y s' -> In_tree y (Node c t0 t1 t2)) *) + Clear H0 H5. + Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H4; Intuition. + (* In_tree y (Node c t0 t1 t2)) -> In_tree y s' *) + Clear H0 H5. + Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H10; Auto. + (* d = false => Node c l' t1 t2, false *) + Exists ((Node c l' t1 t2), false); Intuition. + Inversion_clear H1; Constructor; Intuition. + Intro; Intro; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H2; Constructor; Ground. + Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H2; Inversion_clear H1; Intuition. + Apply (!E.lt_not_eq x t1); Auto. + Apply E.eq_trans with y; Auto. + Apply (!ME.lt_not_gt y t1); Auto. + Apply ME.eq_lt with x; Trivial. + Generalize (H4 y); Clear H4; Inversion_clear H2; Intuition. + Generalize (H4 y); Clear H4; Inversion_clear H6; Intuition. + (* eq x t1 *) + Clear H H0. + Generalize Dependent t2; Destruct t2; Intros. + (* t2 = Leaf *) + Induction c. + (* c = red => t0, false *) + Exists (t0, false); Intuition. + Inversion_clear H1; Trivial. + Inversion H0. + Inversion_clear H; Trivial. + Apply (!E.lt_not_eq y t1); Auto. + Inversion_clear H1; Apply H4; Trivial. + Apply E.eq_trans with x; Auto. + Inversion_clear H2; Intuition. + Absurd (X.eq y x); Auto. + Apply E.eq_trans with t1; Auto. + Inversion H. + (* c = black => blackify t0 *) + Case (blackify t0). + Inversion_clear H1; Trivial. + Intros (s',d); Intros; Exists (s',d); Intuition. + Inversion H3; Induction d; Intuition. + Generalize (H4 y); Clear H4; Inversion_clear H1; Intuition. + Apply (!E.lt_not_eq y t1); Auto. + Apply H7; Auto. + Apply E.eq_trans with x; Auto. + Ground. + Generalize (H4 y); Clear H4; Inversion_clear H6; Intuition. + Absurd (X.eq y x); Auto. + Apply E.eq_trans with t1; Auto. + Inversion H3. + (* t2 = Node c0 t3 t4 t5 *) + Case (remove_min (Node c0 t3 t4 t5)). + Inversion_clear H1; Trivial. + Discriminate. + Intros (r',(m,d)); Induction d; Intuition. + (* d = true => unbalanced_left *) + Case (unbalanced_left (Node c t0 m r')). + Inversion_clear H1; Constructor; Trivial. + Intro; Intro; Apply E.lt_trans with t1. + Apply H7; Trivial. + Apply H8; Ground. + Intros (s',d); Intros; Exists (s',d); Intuition. + Clear H3 H5 H9; Induction c. + Assert (UnbalancedLeft (pred n) (Node red t0 m r')). + Inversion_clear H7; Generalize (H0 n); Constructor; Intuition. + Rewrite <- (S_pred n O); Trivial. + Induction d; Intuition. + Inversion_clear H7; Ground. + Rewrite (S_pred n O); Trivial. Apply H6; Trivial. + Inversion_clear H7; Ground. + Assert (UnbalancedLeft (pred n) (Node black t0 m r')). + Inversion H7; Simpl; Generalize (H0 n0); Intuition. + Rewrite (S_pred n0 O); Trivial. + Constructor; Intuition. + Rewrite <- (S_pred n0 O); Trivial. + Induction d; Intuition. + Inversion_clear H7; Ground. + Rewrite (S_pred n O); Trivial. Apply H6; Trivial. + Inversion_clear H7; Ground. + (* In_tree y s' -> y <> x *) + Clear H0 H6. + Generalize (H9 y); Clear H9; Generalize (H5 y); + Generalize (H3 y); Clear H3; Intuition. + Inversion_clear H6. + Apply (!E.lt_not_eq x m); Auto. + Inversion_clear H1. + Apply ME.eq_lt with t1; Trivial. + Apply H16; Ground. + Apply E.eq_trans with y; Auto. + Apply (!E.lt_not_eq y t1); Auto. + Inversion_clear H1; Apply H15; Trivial. + Apply E.eq_trans with x; Auto. + Intuition. + Apply (!E.lt_not_eq m y); Auto. + Apply (!ME.lt_not_gt t1 m); Auto. + Inversion_clear H1. + Apply H16; Ground. + Apply ME.lt_eq with y; Trivial. + Apply E.eq_trans with x; Auto. + (* In_tree y s' -> In_tree y (Node c t0 t1 t2)) *) + Clear H0 H4 H6. + Generalize (H9 y); Clear H9; Generalize (H5 y); Clear H5; Intuition. + Inversion_clear H4; Intuition. + (* In_tree y (Node c t0 t1 t2)) -> In_tree y s' *) + Clear H0 H4 H6. + Generalize (H9 y); Clear H9; Generalize (H5 y); Clear H5; Intuition. + Inversion_clear H11; Intuition. + Absurd (X.eq y x); Auto. + Apply E.eq_trans with t1; Auto. + (* d = false => Node c t0 m r', false *) + Exists ((Node c t0 m r'), false); Intuition. + Inversion_clear H1; Constructor; Intuition. + Intro; Intro; Apply E.lt_trans with t1. + Apply H7; Trivial. + Generalize (H5 m); Clear H5; Intuition. + Apply H8; Intuition. + Inversion_clear H2; Constructor; Ground. + Generalize (H5 y); Intuition. + Inversion_clear H2; Inversion_clear H1. + Generalize (H7 H9); Intro. + Apply (!E.lt_not_eq t1 y); Auto. + Apply H13; Trivial. + Apply E.eq_trans with x; Auto. + Apply (!E.lt_not_eq y t1); Auto. + Apply H12; Trivial. + Apply E.eq_trans with x; Auto. + Generalize (H10 H9); Intro. + Apply (!E.lt_not_eq t1 y); Auto. + Apply H13; Trivial. + Apply E.eq_trans with x; Auto. + Generalize (H5 y); Clear H5; Inversion_clear H2; Intuition. + Generalize (H5 y); Clear H5; Inversion_clear H7; Intuition. + Absurd (X.eq y x); Auto. + Apply E.eq_trans with t1; Auto. + (* lt t1 x *) + Clear H; Case H0; Clear H0. + Inversion H1; Trivial. + Intros (r',d); Induction d; Intuition. + (* d = true => unbalanced_left *) + Case (unbalanced_left (Node c t0 t1 r')). + Constructor; Inversion_clear H1; Auto. + Intro; Generalize (H4 y); Intuition. + Intros (s',d'); Intros; Exists (s',d'). + Intuition. + Clear H4 H8; Induction c. + Assert (UnbalancedLeft (pred n) (Node red t0 t1 r')). + Inversion_clear H6; Generalize (H0 n); Constructor; Intuition. + Rewrite <- (S_pred n O); Trivial. + Induction d'; Intuition. + Inversion_clear H6; Ground. + Rewrite (S_pred n O); Trivial. Apply H5; Trivial. + Inversion_clear H6; Ground. + Assert (UnbalancedLeft (pred n) (Node black t0 t1 r')). + Inversion H6; Simpl; Generalize (H0 n0); Intuition. + Rewrite (S_pred n0 O); Trivial. + Constructor; Intuition. + Rewrite <- (S_pred n0 O); Trivial. + Induction d'; Intuition. + Inversion_clear H6; Ground. + Rewrite (S_pred n O); Trivial. Apply H5; Trivial. + Inversion_clear H6; Ground. + (* In_tree y s' -> y <> x *) + Clear H0 H5. + Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H4. + Apply (!E.lt_not_eq t1 x); Auto. + Apply E.eq_trans with y; Auto. + Apply (!ME.lt_not_gt t1 y); Auto. + Apply ME.lt_eq with x; Auto. + Inversion_clear H1; Auto. + Intuition. + (* In_tree y s' -> In_tree y (Node c t0 t1 t2)) *) + Clear H0 H5. + Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H4; Intuition. + (* In_tree y (Node c t0 t1 t2)) -> In_tree y s' *) + Clear H0 H5. + Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H10; Auto. + (* d = false => Node c t0 t1 r', false *) + Exists ((Node c t0 t1 r'), false); Intuition. + Inversion_clear H1; Constructor; Intuition. + Intro; Intro; Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H2; Constructor; Ground. + Generalize (H4 y); Clear H4; Intuition. + Inversion_clear H2; Inversion_clear H1; Intuition. + Apply (!E.lt_not_eq t1 x); Auto. + Apply E.eq_trans with y; Auto. + Apply (!ME.lt_not_gt t1 y); Auto. + Apply ME.lt_eq with x; Auto. + Generalize (H4 y); Clear H4; Inversion_clear H2; Intuition. + Generalize (H4 y); Clear H4; Inversion_clear H6; Intuition. + Defined. + + Definition remove : (x:elt)(s:t) + { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}. + Proof. + Intros x (s,Hs,Hrb); Case (remove_aux x s). + Trivial. + Intros (s',b); Intuition; Clear H2. + Assert s'rbtree : (EX n:nat | (rbtree n s')). + Elim Hrb; Clear Hrb; Intros n Hn; Induction b; Ground. + Exists (t_intro s' H s'rbtree); Unfold In; Simpl; Intuition. + Defined. + + (** * of_list *) + + (** Building a red-black tree from a sorted list *) + + Set Implicit Arguments. + Record of_list_aux_Invariant [k,n:Z; l,l':(list elt); r:tree] : Prop := + make_olai + { olai_bst : (bst r); + olai_rb : (EX kn:nat | (inject_nat kn)=k /\ (rbtree kn r)); + olai_sort : (sort E.lt l'); + olai_length : (Zlength l')=(Zlength l)-n; + olai_same : + ((x:elt)(InList E.eq x l) <-> (In_tree x r) \/ (InList E.eq x l')); + olai_order : + ((x,y:elt)(In_tree x r) -> (InList E.eq y l') -> (E.lt x y)) }. + Unset Implicit Arguments. + + Lemma power_invariant : + (n,k:Z)0<k -> + (two_p k) <= n +1 <= (two_p (Zs k)) -> + let (nn,_) = (Zsplit2 (n-1)) in let (n1,n2) = nn in + (two_p (Zpred k)) <= n1+1 <= (two_p k) /\ + (two_p (Zpred k)) <= n2+1 <= (two_p k). + Proof. + Intros. + Case (Zsplit2 (n-1)). + Intros (n1,n2) X. + Generalize H0; Pattern 1 k; Rewrite (Zs_pred k). + Rewrite two_p_S; Auto with zarith. + Rewrite two_p_S; Auto with zarith. + Apply Zlt_ZERO_pred_le_ZERO; Auto. + Qed. + + Definition of_list_aux : + (k:Z) 0<=k -> + (n:Z) (two_p k) <= n+1 <= (two_p (Zs k)) -> + (l:(list elt)) (sort E.lt l) -> n <= (Zlength l) -> + { rl' : tree * (list elt) + | let (r,l')=rl' in (of_list_aux_Invariant k n l l' r) }. + Proof. + Intros k Hk; Pattern k; Apply natlike_rec2; Try Assumption. + Intro n; Case (Z_eq_dec 0 n). + (* k=0 n=0 *) + Intros Hn1 Hn2 l Hl1 Hl2; Exists (Leaf, l); Intuition. + Apply make_olai; Intuition. + Exists O; Auto. + Inversion H2. + Inversion H1. + (* k=0 n>0 (in fact 1) *) + Intros Hn1 Hn2. + Assert n=1. Rewrite two_p_S in Hn2; Simpl in Hn2; Auto with zarith. + Rewrite H. + Intro l; Case l. + (* l = [], absurd case. *) + Intros Hl1 Hl2; Unfold Zlength Zlt in Hl2; Elim Hl2; Trivial. + (* l = x::l' *) + Intros x l' Hl1 Hl2; Exists ((Node red Leaf x Leaf), l'); Intuition. + Apply make_olai; Intuition. + Exists O; Auto. + Inversion Hl1; Auto. + Rewrite Zlength_cons; Auto with zarith. + Inversion_clear H2; Auto. + Inversion_clear H3; Auto; Inversion_clear H2. + Inversion_clear H2; Try Solve [ Inversion H4 ]. + Inversion_clear Hl1. + Apply ME.In_sort with l'; Auto. + EApply ME.Inf_eq; EAuto. + (* k>0 *) + Clear k Hk; Intros k Hk Hrec n Hn l Hl1 Hl2. + Rewrite <- Zs_pred in Hrec. + Generalize (power_invariant n k Hk). + Elim (Zsplit2 (n-1)); Intros (n1,n2) (A,B) C. + Elim (C Hn); Clear C; Intros Hn1 Hn2. + (* First recursive call : (of_list_aux (Zpred k) n1 l) gives (lft,l') *) + Elim (Hrec n1 Hn1 l Hl1). + Intro p; Case p; Clear p; Intros lft l'; Case l'. + (* l' = [], absurd case. *) + Intros o; ElimType False. + Generalize (olai_length o). + Unfold 1 Zlength; Simpl; Intros X. + Assert n1 = (Zlength l). Omega. Clear X. + Rewrite <- H in Hl2. + Assert n <= n2. + Apply Zle_trans with n1; Auto; Inversion H; Omega. + Assert 0<n+1. + Apply Zlt_le_trans with (two_p k). + Generalize (two_p_gt_ZERO k); Omega. + Inversion_clear Hn; Trivial. + Omega. + (* l' = x :: l'' *) + Intros x l'' o1. + (* Second recursive call : (of_list_aux (Zpred k) n2 l'') gives (rht,l''') *) + Elim (Hrec n2 Hn2 l''); Clear Hrec. + Intro p; Case p; Clear p; Intros rht l''' o2. + Exists ((Node black lft x rht),l'''). + Apply make_olai. + (* inv1 : bst *) + Constructor; Try Solve [ EApply olai_bst; EAuto ]. + Unfold lt_tree; Intros. + Apply (olai_order o1 7!y 8!x H); Auto. + Assert sorted := (olai_sort o1). + Inversion_clear sorted. + Unfold gt_tree; Intros. + Apply ME.In_sort with l''; Auto. + Elim (olai_same o2 y); Auto. + (* inv2 : rb *) + Elim (inject_nat_complete k); [Intros kn; Case kn |Omega]. + Simpl; Intros X; Rewrite X in Hk; Absurd 0<0; Auto with zarith. + Clear kn; Intro kn. + Exists (S kn); Split; Auto. + Constructor. + Elim (olai_rb o1); Intros kn' (Hkn',Hrb); Rewrite inj_S in H. + Rewrite H in Hkn'; Rewrite <- Zpred_Sn in Hkn'. + Elim (eq_nat_dec kn kn'); Intro X; [Subst | Elim (inj_neq ?? X)]; Auto. + Elim (olai_rb o2); Intros kn' (Hkn',Hrb); Rewrite inj_S in H. + Rewrite H in Hkn'; Rewrite <- Zpred_Sn in Hkn'. + Elim (eq_nat_dec kn kn'); Intro X; [Subst | Elim (inj_neq ?? X)]; Auto. + (* inv3 : sort *) + Exact (olai_sort o2). + (* inv4 : length *) + Rewrite (olai_length o2). + Rewrite (Zpred_Sn (Zlength l'')). + Rewrite <- (Zlength_cons x l''). + Rewrite (olai_length o1); Unfold Zpred; Omega. + (* inv5 : same *) + Intro y; Generalize (olai_same o1 y); Generalize (olai_same o2 y). + Assert (InList E.eq y x::l'') <-> (E.eq y x) \/ (InList E.eq y l''). + Split; Intro H; Inversion H; Auto. + Generalize H; Clear H A B Hn Hn1 Hn2 o1 o2. + Intuition; Inversion_clear H9; Intuition. + (* inv6 : order *) + Intros a b In_r In_l'''. + Inversion_clear In_r. + Assert sorted := (olai_sort o1). + Inversion_clear sorted. + Apply ME.eq_lt with x; Auto. + Apply ME.In_sort with l''; Auto. + Generalize (olai_same o2 b); Intros (_,X); Auto. + Apply (olai_order o1 7!a 8!b); Auto. + Constructor 2. + Generalize (olai_same o2 b); Intros (_,X); Auto. + Apply (olai_order o2 7!a 8!b); Auto. + (* misc preconditions to ensure *) + Assert sorted := (olai_sort o1); Inversion_clear sorted; Trivial. + Rewrite (Zpred_Sn (Zlength l'')). + Rewrite <- (Zlength_cons x l''). + Rewrite (olai_length o1); Unfold Zpred; Omega. + Omega. + Defined. + + Definition of_list : (l:(list elt))(sort E.lt l) -> + { s : t | (x:elt)(In x s) <-> (InList E.eq x l) }. + Proof. + Intros. + LetTac n := (Zlength l). + LetTac k := (N_digits n). + Assert 0<=n. + Unfold n; Rewrite Zlength_correct; Auto with zarith. + Assert (two_p k) <= n+1 <= (two_p (Zs k)). + Unfold k; Generalize H0; Case n; Intros. + Rewrite two_p_S; Simpl; Omega. + Unfold N_digits; Generalize (log_inf_correct p); Omega. + Unfold Zle in H1; Elim H1; Auto. + Elim (of_list_aux k (ZERO_le_N_digits n) n H1 l); Auto. + Intros (r,l') o. + Assert (EX n : nat | (rbtree n r)). + Elim (olai_rb o); Intros kn Hkn; Exists kn; Intuition. + Exists (t_intro r (olai_bst o) H2). + Unfold In; Simpl. + Intro x; Generalize (olai_same o x). + Rewrite (Zlength_nil_inv l'). + Intuition; Inversion_clear H1. + Rewrite (olai_length o); Unfold n; Omega. + Unfold n; Omega. + Qed. + + (** * Elements *) + + (** [elements_tree_aux acc t] catenates the elements of [t] in infix + order to the list [acc] *) + + Fixpoint elements_tree_aux [acc:(list X.t); t:tree] : (list X.t) := + Cases t of + | Leaf => + acc + | (Node _ l x r) => + (elements_tree_aux (x :: (elements_tree_aux acc r)) l) + end. + + (** then [elements_tree] is an instanciation with an empty [acc] *) + + Definition elements_tree := (elements_tree_aux []). + + Lemma elements_tree_aux_acc_1 : + (s:tree)(acc:(list elt)) + (x:elt)(InList E.eq x acc)->(InList E.eq x (elements_tree_aux acc s)). + Proof. + Induction s; Simpl; Intuition. + Save. + Hints Resolve elements_tree_aux_acc_1. + + Lemma elements_tree_aux_1 : + (s:tree)(acc:(list elt)) + (x:elt)(In_tree x s)->(InList E.eq x (elements_tree_aux acc s)). + Proof. + Induction s; Simpl; Intuition. + Inversion H. + Inversion_clear H1; Ground. + Save. + + Lemma elements_tree_1 : + (s:tree) + (x:elt)(In_tree x s)->(InList E.eq x (elements_tree s)). + Proof. + Unfold elements_tree; Intros; Apply elements_tree_aux_1; Auto. + Save. + Hints Resolve elements_tree_1. + + Lemma elements_tree_aux_acc_2 : + (s:tree)(acc:(list elt)) + (x:elt)(InList E.eq x (elements_tree_aux acc s)) -> + (InList E.eq x acc) \/ (In_tree x s). + Proof. + Induction s; Simpl; Intuition. + Elim (H ?? H1); Intuition. + Inversion_clear H2; Intuition. + Elim (H0 ?? H3); Intuition. + Save. + Hints Resolve elements_tree_aux_acc_2. + + Lemma elements_tree_2 : + (s:tree) + (x:elt)(InList E.eq x (elements_tree s)) -> (In_tree x s). + Proof. + Unfold elements_tree; Intros. + Elim (elements_tree_aux_acc_2 ??? H); Auto. + Intros; Inversion H0. + Save. + Hints Resolve elements_tree_2. + + Lemma elements_tree_aux_sort : + (s:tree)(bst s) -> (acc:(list elt)) + (sort E.lt acc) -> + ((x:elt)(InList E.eq x acc) -> (y:elt)(In_tree y s) -> (E.lt y x)) -> + (sort E.lt (elements_tree_aux acc s)). + Proof. + Induction s; Simpl; Intuition. + Apply H. + Inversion H1; Auto. + Constructor. + Apply H0; Auto. + Inversion H1; Auto. + Apply ME.Inf_In_2. + Replace X.eq with E.eq; Replace X.lt with E.lt; Auto. + Intros. + Elim (elements_tree_aux_acc_2 t2 acc y); Intuition. + Inversion_clear H1. + Apply H9; Auto. + Intuition. + Inversion_clear H4. + Apply ME.lt_eq with t1; Auto. + Inversion_clear H1. + Apply H8; Auto. + Elim (elements_tree_aux_acc_2 ??? H6); Intuition. + Apply E.lt_trans with t1. + Inversion_clear H1; Apply H9; Auto. + Inversion_clear H1; Apply H10; Auto. + Save. + + Lemma elements_tree_sort : + (s:tree)(bst s) -> (sort E.lt (elements_tree s)). + Proof. + Intros; Unfold elements_tree; Apply elements_tree_aux_sort; Auto. + Intros; Inversion H0. + Save. + Hints Resolve elements_tree_sort. + + Definition elements : + (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}. + Proof. + Intros (s,Hs,Hrb); Unfold In; Simpl. + Exists (elements_tree s); Repeat Split. + Apply elements_tree_sort; Auto. + Apply elements_tree_1; Auto. + Apply elements_tree_2; Auto. + Defined. + + (** * Isomorphism with FSetList. *) + + Module Lists := FSetList.Make(X). + + Definition of_slist : (l:Lists.t) { s : t | (x:elt)(Lists.In x l)<->(In x s) }. + Proof. + Intros (l,Hl). + Elim (of_list l Hl); Intros s Hls. + Exists s; Unfold Lists.In Lists.Raw.In; Simpl; Ground. + Defined. + + Definition to_slist : (s:t) { l : Lists.t | (x:elt)(In x s)<->(Lists.In x l) }. + Proof. + Intro s; Elim (elements s); Intros l (Hl1, Hl2). + Exists (Lists.Build_slist Hl1). + Unfold Lists.In Lists.Raw.In; Simpl; Ground. + Defined. + + (** * Union *) + + Definition union : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}. + Proof. + Intros s s'. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Elim (of_slist (Lists.union l l')); Intros r Hr. + Exists r; Intuition. + Elim (!Lists.union_1 l l' x); Ground. + Elim (Hr x); Intros A _; Apply A; Apply (!Lists.union_2 l l' x); Ground. + Elim (Hr x); Intros A _; Apply A; Apply (!Lists.union_3 l l' x); Ground. + Defined. + + (** * Intersection *) + + Lemma inter : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}. + Proof. + Intros s s'. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Elim (of_slist (Lists.inter l l')); Intros r Hr. + Exists r; Intuition. + Elim (Hl x); Intros _ A; Apply A; Apply (!Lists.inter_1 l l' x); Ground. + Elim (Hl' x); Intros _ A; Apply A; Apply (!Lists.inter_2 l l' x); Ground. + Elim (Hr x); Intros A _; Apply A; Apply (!Lists.inter_3 l l' x); Ground. + Defined. + + (** * Difference *) + + Lemma diff : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}. + Proof. + Intros s s'. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Elim (of_slist (Lists.diff l l')); Intros r Hr. + Exists r; Intuition. + Elim (Hl x); Intros _ A; Apply A; Apply (!Lists.diff_1 l l' x); Ground. + Elim (!Lists.diff_2 l l' x); Ground. + Elim (Hr x); Intros A _; Apply A; Apply (!Lists.diff_3 l l' x); Ground. + Defined. + + (** * Equality test *) + + Lemma equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }. + Proof. + Intros s s'. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Assert (Lists.Equal l l')->(Lists.equal l l')=true. Exact (!Lists.equal_1 l l'). + Assert (Lists.equal l l')=true->(Lists.Equal l l'). Exact (!Lists.equal_2 l l'). + Generalize H H0; Case (Lists.equal l l'); Unfold Lists.Equal Equal. + Left; Intros; Generalize (H2 (refl_equal ? true)); Ground. + Right; Intros; Intro. + Absurd false=true; [ Auto with bool | Ground ]. + Defined. + + (** * Inclusion test *) + + Lemma subset : (s,s':t){ Subset s s' } + { ~(Subset s s') }. + Proof. + Intros s s'. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Assert (Lists.Subset l l')->(Lists.subset l l')=true. Exact (!Lists.subset_1 l l'). + Assert (Lists.subset l l')=true->(Lists.Subset l l'). Exact (!Lists.subset_2 l l'). + Generalize H H0; Case (Lists.subset l l'); Unfold Lists.Subset Subset. + Left; Intros; Generalize (H2 (refl_equal ? true)); Ground. + Right; Intros; Intro. + Absurd false=true; [ Auto with bool | Ground ]. + Defined. + + (** * Fold *) + + Fixpoint fold_tree [A:Set; f:elt->A->A; s:tree] : A -> A := + Cases s of + | Leaf => [a]a + | (Node _ l x r) => [a](fold_tree A f l (f x (fold_tree A f r a))) + end. + Implicits fold_tree [1]. + + Definition fold_tree' := + [A:Set; f:elt->A->A; s:tree] (Lists.Raw.fold f (elements_tree s)). + Implicits fold_tree' [1]. + + Lemma fold_tree_compat : (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) + (s:tree)(f:elt->A->A)(compat_op E.eq eqA f) -> (a,a':A)(eqA a a') -> + (eqA (fold_tree f s a) (fold_tree f s a')). + Proof. + Induction s; Simpl; Auto. + Qed. + + Lemma fold_tree_equiv_aux : (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) + (s:tree)(f:elt->A->A)(compat_op E.eq eqA f) -> (a:A; acc : (list elt)) + (eqA (Lists.Raw.fold f (elements_tree_aux acc s) a) + (fold_tree f s (Lists.Raw.fold f acc a))). + Proof. + Induction s. + Simpl; Intuition. + Simpl; Intros. + EApply (Seq_trans ?? st). + Apply H; Auto. + Apply (fold_tree_compat A eqA); Simpl; Auto. + Qed. + + Lemma fold_tree_equiv : + (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) + (s:tree)(f:elt->A->A; a:A)(compat_op E.eq eqA f) -> + (eqA (fold_tree f s a) (fold_tree' f s a)). + Proof. + Unfold fold_tree' elements_tree. + Induction s; Simpl; Auto; Intros. + Apply Seq_refl; Auto. + Apply Seq_sym; Auto. + EApply (Seq_trans ?? st). + Apply (fold_tree_equiv_aux ? eqA); Simpl; Auto. + Apply (fold_tree_compat ? eqA); Simpl; Auto. + Apply Seq_sym; Auto. + Qed. + + 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_tree f s i) i). + Proof. + Intros (s,Hs,Hrb); Unfold Empty Add In; Simpl; Clear Hs Hrb. + Case s; Simpl; Intuition. + Elim (H t1); Auto. + Save. + + 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_tree f s' i) (f x (fold_tree f s i))). + Proof. + Intros (s,Hs,Hrb) (s',Hs',Hrb'); Unfold Add In; Simpl; Intros. + EApply (Seq_trans ?? st). + Apply (fold_tree_equiv ? eqA); Auto. + EApply (Seq_trans ?? st) with (f x (fold_tree' f s i)). + Unfold fold_tree'. + Generalize (elements_tree_sort s Hs) (elements_tree_sort s' Hs'). + LetTac l := (elements_tree s). + LetTac l' := (elements_tree s'). + Intros Hl Hl'. + Apply (!Lists.Raw.fold_2 l l' Hl Hl' x A eqA) ; Auto. + Unfold Lists.Raw.Add l l'; Split; Intros; Elim (H2 y); Intuition; Elim H4; Auto. + Apply (Seq_sym ?? st). + Apply H; Auto. + Apply (fold_tree_equiv ? eqA); Auto. + Qed. + + Definition fold : + (A:Set) + (f:elt->A->A) + { fold:t -> A -> A | (s,s':t)(a:A) + (eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) + ((Empty s) -> (eqA (fold s a) a)) /\ + ((compat_op E.eq eqA f)->(transpose eqA f) -> + (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }. + Proof. + Intros A f; Exists [s:t](fold_tree f s); Split; Intros. + Apply fold_1; Auto. + Apply (fold_2 s s' x A eqA); Auto. + Defined. + + (** * Cardinal *) + + Definition cardinal : + {cardinal : t -> nat | (s,s':t) + ((Empty s) -> (cardinal s)=O) /\ + ((x:elt) (Add x s s') -> ~(In x s) -> (cardinal s')=(S (cardinal s)))}. + Proof. + Assert st : (Setoid_Theory ? (eq nat)). + Constructor; Auto; Intros; EApply trans_eq; EAuto. + Elim (fold nat [_]S); Intro f; Exists [s:t](f s O); Split; Intros. + Elim (p s s O ? st); Auto. + Elim (p s s' O ? st); Intros; EApply H2; EAuto. + Qed. + + (** * Filter *) + + Module DLists := DepOfNodep(Lists). + + 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)) }. + Proof. + Intros. + Elim (to_slist s); Intros l Hl. + Elim (DLists.filter Pdec l); Intros l' Hl'. + Elim (of_slist l'); Intros r Hr. + Exists r. + Intros C; Generalize (Hl' C); Ground. + Qed. + + Lemma 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) }. + Proof. + Intros; Unfold For_all. + Elim (to_slist s); Intros l Hl. + Elim (DLists.for_all Pdec l); Unfold Lists.For_all; Intro H; [Left|Right]; + Intro C; Generalize (H C); Ground. + Qed. + + Lemma 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) }. + Proof. + Intros; Unfold Exists. + Elim (to_slist s); Intros l Hl. + Elim (DLists.exists Pdec l); Unfold Lists.Exists; Intro H; [Left|Right]; + Intro C; Generalize (H C); Ground. + Qed. + + Lemma 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))) }. + Proof. + Intros; Unfold For_all. + Elim (to_slist s); Intros l Hl. + Elim (DLists.partition Pdec l); Unfold Lists.For_all; Intros (l1,l2) H. + Elim (of_slist l1); Intros s1 Hs1. + Elim (of_slist l2); Intros s2 Hs2. + Exists (s1,s2). + Intro Comp; Elim (H Comp); Intros A (B,C); Clear H Comp. + Intuition. + Apply A; Ground. + Apply (B x); Ground. + Elim (C x); Intros D _; Elim D; [Left|Right|Idtac]; Ground. + Ground. + Ground. + Qed. + + (** * Minimum element *) + + Definition min_elt : + (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }. + Proof. + Intros (s,Hs,Hrb). + Unfold For_all Empty In; Simpl. + Generalize Hs; Clear Hs Hrb; Induction s; Simpl; Intros. + (* s = Leaf *) + Right; Intros; Intro; Inversion H. + (* s = Node c s1 t0 s0 *) + Clear Hrecs0; Generalize Hs Hrecs1; Clear Hs Hrecs1; Case s1; Intros. + (* s1 = Leaf *) + Left; Exists t0; Intuition. + Inversion_clear H. + Absurd (X.eq x t0); Auto. + Inversion H1. + Inversion_clear Hs; Absurd (E.lt x t0); Auto. + (* s1 = Node c0 t1 t2 t3 *) + Case Hrecs1; Clear Hrecs1. + Inversion Hs; Auto. + (* a minimum for [s1] *) + Intros (m,Hm); Left; Exists m; Intuition. + Apply (H0 x); Auto. + Assert (X.lt m t0). + Inversion_clear Hs; Auto. + Inversion_clear H1; Auto. + Elim (!X.lt_not_eq x t0); [ EAuto | Auto ]. + Inversion_clear Hs. + Elim (!ME.lt_not_gt x t0); [ EAuto | Auto ]. + (* non minimum for [s1] => absurd *) + Intro; Right; Intuition. + Apply (n t2); Auto. + Defined. + + (** * Maximum element *) + + Definition max_elt : + (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }. + Proof. + Intros (s,Hs,Hrb). + Unfold For_all Empty In; Simpl. + Generalize Hs; Clear Hs Hrb; Induction s; Simpl; Intros. + (* s = Leaf *) + Right; Intros; Intro; Inversion H. + (* s = Node c s1 t0 s0 *) + Clear Hrecs1; Generalize Hs Hrecs0; Clear Hs Hrecs0; Case s0; Intros. + (* s0 = Leaf *) + Left; Exists t0; Intuition. + Inversion_clear H. + Absurd (X.eq x t0); Auto. + Inversion_clear Hs; Absurd (E.lt t0 x); Auto. + Inversion H1. + (* s0 = Node c0 t1 t2 t3 *) + Case Hrecs0; Clear Hrecs0. + Inversion Hs; Auto. + (* a maximum for [s0] *) + Intros (m,Hm); Left; Exists m; Intuition. + Apply (H0 x); Auto. + Assert (X.lt t0 m). + Inversion_clear Hs; Auto. + Inversion_clear H1; Auto. + Elim (!X.lt_not_eq x t0); [ EAuto | Auto ]. + Inversion_clear Hs. + Elim (!ME.lt_not_gt t0 x); [ EAuto | Auto ]. + (* non maximum for [s0] => absurd *) + Intro; Right; Intuition. + Apply (n t2); Auto. + Defined. + + (** * Any element *) + + Definition choose : (s:t) { x:elt | (In x s)} + { Empty s }. + Proof. + Intros (s,Hs,Hrb); Unfold Empty In; Simpl; Case s; Intuition. + Right; Intros; Inversion H. + Left; Exists t1; Auto. + Defined. + + (** * Comparison *) + + Definition eq : t -> t -> Prop := Equal. + + Definition lt : t -> t -> Prop := + [s,s':t]let (l,_) = (to_slist s) in + let (l',_) = (to_slist s') in + (Lists.lt l l'). + + Lemma eq_refl: (s:t)(eq s s). + Proof. + Unfold eq Equal; Intuition. + Save. + + Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s). + Proof. + Unfold eq Equal; Ground. + Save. + + Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s''). + Proof. + Unfold eq Equal; Ground. + Save. + + Lemma lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s''). + Proof. + Intros s s' s''; Unfold lt. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Elim (to_slist s''); Intros l'' Hl''. + Exact (!Lists.lt_trans l l' l''). + Save. + + Definition eql : t -> t -> Prop := + [s,s':t]let (l,_) = (to_slist s) in + let (l',_) = (to_slist s') in + (Lists.eq l l'). + + Lemma eq_eql : (s,s':t)(eq s s') -> (eql s s'). + Proof. + Unfold eq Equal eql Lists.eq Lists.Raw.eq Lists.Raw.Equal. + Intros s s'. + Elim (to_slist s); Unfold Lists.In Lists.Raw.In; + Simpl; Intros l Hl. + Elim (to_slist s'); Unfold Lists.In Lists.Raw.In; + Simpl; Intros l' Hl'. + Ground. + Save. + + Lemma eql_eq : (s,s':t)(eql s s') -> (eq s s'). + Proof. + Unfold eq Equal eql Lists.eq Lists.Raw.eq Lists.Raw.Equal. + Intros s s'. + Elim (to_slist s); Unfold Lists.In Lists.Raw.In; + Simpl; Intros l Hl. + Elim (to_slist s'); Unfold Lists.In Lists.Raw.In; + Simpl; Intros l' Hl'. + Ground. + Save. + + Lemma lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s'). + Proof. + Intros s s' H; Intro. + Generalize (eq_eql s s' H0). + Generalize H; Unfold lt eql. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Exact (!Lists.lt_not_eq l l'). + Save. + + Definition compare: (s,s':t)(Compare lt eq s s'). + Proof. + Intros s s'. + Cut (lt s s') -> (Compare lt eq s s'). + Cut (eq s s') -> (Compare lt eq s s'). + Cut (lt s' s) -> (Compare lt eq s s'). + Unfold 1 4 lt. + Generalize (eql_eq s s'); Unfold eql. + Elim (to_slist s); Intros l Hl. + Elim (to_slist s'); Intros l' Hl'. + Elim (Lists.compare l l'); Intuition. + Constructor 3; Trivial. + Constructor 2; Trivial. + Constructor 1; Trivial. + Defined. + +End Make. + + + diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 5dfc8ac8eb..122de1e2de 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -146,7 +146,7 @@ Apply lt_reg_r; Auto. Intuition; Elim H1; Simpl; Trivial. Qed. -Lemma Z_rec : (P:Z->Type)(P `0`) -> +Lemma natlike_rec2 : (P:Z->Type)(P `0`) -> ((z:Z)`0<z` -> (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z). Proof. Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf). |