theories/Lists

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@508 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 331 insertions, 0 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
new file mode 100644
index 000000000..6de241d18
--- /dev/null
+++ b/theories/Lists/ListSet.v
@@ -0,0 +1,331 @@
+
+(* $Id$ *)
+
+(* A Library for finite sets, implemented as lists *)
+(* A Library with similar interface will soon be available under
+  the name TreeSet in the theories/TREES directory *)
+
+(* PolyList is loaded, but not exported *)
+(* This allow to "hide" the definitions, functions and theorems of PolyList
+ and to see only the ones of ListSet *)
+Require PolyList.
+
+Implicit Arguments On.
+
+Section first_definitions.
+
+
+  Variable A : Set.
+  Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}.
+
+  Definition set := (list A).
+
+  Definition empty_set := (nil A).
+
+  Fixpoint set_add [a:A; x:set] : set :=
+    Cases x of
+    | nil => (cons a (nil A))
+    | (cons a1 x1) => Cases (Aeq_dec a a1) of 
+                    | (left _) => (cons a1 x1) 
+                    | (right _) => (cons a1 (set_add a x1))
+                   end
+    end.
+
+
+  Fixpoint set_mem [a:A; x:set] : bool :=
+    Cases x of
+    | nil => false
+    | (cons a1 x1) => Cases (Aeq_dec a a1) of 
+                    | (left _) => true 
+                    | (right _) => (set_mem a x1)
+                   end
+    end.
+ 
+  (* If a belongs to x, removes a from x. If not, does nothing *)
+  Fixpoint set_remove [a:A; x:set] : set :=
+    Cases x of
+    | nil => empty_set
+    | (cons a1 x1) => Cases (Aeq_dec a a1) of 
+                    | (left _) => x1 
+                    | (right _) => (cons a1 (set_remove a x1))
+                   end
+    end.
+
+  Fixpoint set_inter [x:set] : set -> set :=
+    Cases x of
+    | nil => [y](nil A)
+    | (cons a1 x1) => [y]if (set_mem a1 y) 
+                      then (cons a1 (set_inter x1 y))
+		      else (set_inter x1 y)
+    end.
+
+  Fixpoint set_union [x,y:set] : set :=
+    Cases y of
+    | nil => x
+    | (cons a1 y1) => (set_add a1 (set_union x y1))
+    end.
+        
+  (* returns the set of all els of x that does not belong to y *)
+  Fixpoint set_diff [x:set] : set -> set :=
+    [y]Cases x of
+    | nil => (nil A)
+    | (cons a1 x1) => if (set_mem a1 y) 
+                      then (set_diff x1 y)
+		      else (set_add a1 (set_diff x1 y))
+    end.
+   
+  (** 
+  Inductive set_In : A -> set -> Prop :=
+    set_In_singl : (a:A)(x:set)(set_In a (cons a (nil A))) 
+  | set_In_add : (a,b:A)(x:set)(set_In a x)->(set_In a (set_add b x))
+  .
+  **)
+
+  Definition set_In : A -> set -> Prop := (In 1!A).
+
+  Lemma set_In_dec : (a:A; x:set){(set_In a x)}+{~(set_In a x)}.
+
+  Proof.
+    Unfold set_In.
+    Realizer set_mem.
+    Program_all.
+    Rewrite e; Simpl; Auto with datatypes.
+    Simpl; Unfold not; Intros [Hc1 | Hc2 ]; Auto with datatypes.
+  Save.
+
+  Lemma set_mem_ind : 
+    (B:Set)(P:B->Prop)(y,z:B)(a:A)(x:set)
+      ((set_In a x) -> (P y))
+       ->(P z)
+       ->(P (if (set_mem a x) then y else z)).
+
+  Proof.
+    Induction x; Simpl; Intros.
+    Assumption.
+    Elim (Aeq_dec a a0); Auto with datatypes.
+  Save.
+
+  Lemma set_mem_correct1 :
+    (a:A)(x:set)(set_mem a x)=true -> (set_In a x).
+  Proof.
+    Induction x; Simpl.
+    Discriminate.
+    Intros a0 l; Elim (Aeq_dec a a0); Auto with datatypes.
+  Save.
+
+  Lemma set_mem_correct2 :
+    (a:A)(x:set)(set_In a x) -> (set_mem a x)=true.
+  Proof.
+    Induction x; Simpl.
+    Intro Ha; Elim Ha.
+    Intros a0 l; Elim (Aeq_dec a a0); Auto with datatypes.
+    Intros H1 H2 [H3 | H4].
+    Absurd a0=a; Auto with datatypes.
+    Auto with datatypes.
+  Save.
+
+  Lemma set_mem_complete1 :
+    (a:A)(x:set)(set_mem a x)=false -> ~(set_In a x).
+  Proof.
+    Induction x; Simpl.
+    Tauto.
+    Intros a0 l; Elim (Aeq_dec a a0).
+    Intros; Discriminate H0.
+    Unfold not; Intros; Elim H1; Auto with datatypes.
+  Save.
+
+  Lemma set_mem_complete2 :
+    (a:A)(x:set)~(set_In a x) -> (set_mem a x)=false.
+  Proof.
+    Induction x; Simpl.
+    Tauto.
+    Intros a0 l; Elim (Aeq_dec a a0).
+    Intros; Elim H0; Auto with datatypes.
+    Tauto.
+  Save.
+
+  Lemma set_add_intro1 : (a,b:A)(x:set) 
+    (set_In a x) -> (set_In a (set_add b x)).
+
+  Proof.
+    Unfold set_In; Induction x; Simpl.
+    Auto with datatypes.
+    Intros a0 l H [ Ha0a | Hal ].
+    Elim (Aeq_dec b a0); Left; Assumption.
+    Elim (Aeq_dec b a0); Right; [ Assumption | Auto with datatypes ].
+  Save.
+
+  Lemma set_add_intro2 : (a,b:A)(x:set) 
+    a=b -> (set_In a (set_add b x)).
+
+  Proof.
+    Unfold set_In; Induction x; Simpl.
+    Auto with datatypes.
+    Intros a0 l H Hab.
+    Elim (Aeq_dec b a0); 
+    [ Rewrite Hab; Intro Hba0; Rewrite Hba0; Simpl; Auto with datatypes
+    | Auto with datatypes ].
+  Save.
+
+  Hints Resolve set_add_intro1 set_add_intro2.
+
+  Lemma set_add_intro : (a,b:A)(x:set) 
+    a=b\/(set_In a x) -> (set_In a (set_add b x)).
+  
+  Proof.
+    Intros a b x [H1 | H2] ; Auto with datatypes.
+  Save.
+ 
+  Lemma set_add_elim : (a,b:A)(x:set) 
+    (set_In a (set_add b x)) -> a=b\/(set_In a x).
+
+  Proof.
+    Unfold set_In.
+    Induction x.
+    Simpl; Intros [H1|H2]; Auto with datatypes.
+    Simpl; Do 3 Intro.
+    Elim (Aeq_dec b a0).
+    Tauto.
+    Simpl; Intros; Elim H0.
+    Trivial with datatypes.
+    Tauto.
+    Tauto.
+  Save.
+
+  Hints Resolve set_add_intro set_add_elim.
+
+  Lemma set_add_not_empty : (a:A)(x:set)~(set_add a x)=empty_set.
+  Proof.
+    Induction x; Simpl.
+    Discriminate.
+    Intros; Elim  (Aeq_dec a a0); Intros; Discriminate.
+  Save.   
+
+
+  Lemma set_union_intro1 : (a:A)(x,y:set)
+    (set_In a x) -> (set_In a (set_union x y)).
+  Proof.
+    Induction y; Simpl; Auto with datatypes.
+  Save.
+
+  Lemma set_union_intro2 : (a:A)(x,y:set)
+    (set_In a y) -> (set_In a (set_union x y)).
+  Proof.
+    Induction y; Simpl.
+    Tauto.
+    Intros; Elim H0; Auto with datatypes.
+  Save.
+
+  Hints Resolve set_union_intro2 set_union_intro1.
+
+  Lemma set_union_intro : (a:A)(x,y:set)
+    (set_In a x)\/(set_In a y) -> (set_In a (set_union x y)).
+  Proof.
+    Intros; Elim H; Auto with datatypes.
+  Save.
+
+  Lemma set_union_elim : (a:A)(x,y:set)
+    (set_In a (set_union x y)) -> (set_In a x)\/(set_In a y).
+  Proof.
+    Induction y; Simpl.
+    Auto with datatypes.
+    Intros.
+    Generalize (set_add_elim H0).
+    Intros [H1 | H1].
+    Auto with datatypes.
+    Tauto.
+  Save.
+
+  Lemma set_inter_intro :  (a:A)(x,y:set)
+    (set_In a x) -> (set_In a y) -> (set_In a (set_inter x y)).
+  Proof.
+    Induction x.
+    Auto with datatypes.
+    Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hy.
+    Simpl; Rewrite Ha0a.
+    Generalize (!set_mem_correct1 a y).
+    Generalize (!set_mem_complete1 a y).
+    Elim (set_mem a y); Simpl; Intros.
+    Auto with datatypes.
+    Absurd (set_In a y); Auto with datatypes.
+    Elim (set_mem a0 y); [ Right; Auto with datatypes | Auto with datatypes].     
+  Save.
+
+  Lemma set_inter_elim1 : (a:A)(x,y:set)
+    (set_In a (set_inter x y)) -> (set_In a x).
+  Proof.
+    Induction x.
+    Auto with datatypes.
+    Simpl; Intros a0 l Hrec y.
+    Generalize (!set_mem_correct1 a0 y).
+    Elim (set_mem a0 y); Simpl; Intros.
+    Elim H0; EAuto with datatypes.
+    EAuto with datatypes.
+  Save.
+
+  Lemma set_inter_elim2 : (a:A)(x,y:set)
+    (set_In a (set_inter x y)) -> (set_In a y).
+  Proof.
+    Induction x.
+    Tauto.
+    Simpl; Intros a0 l Hrec y.
+    Generalize (!set_mem_correct1 a0 y).
+    Elim (set_mem a0 y); Simpl; Intros.
+    Elim H0; [ Intro Hr; Rewrite <- Hr; EAuto with datatypes  | EAuto with datatypes ] .
+    EAuto with datatypes.
+  Save.
+
+  Hints Resolve set_inter_elim1 set_inter_elim2.
+
+  Lemma set_inter_elim : (a:A)(x,y:set)
+    (set_In a (set_inter x y)) -> (set_In a x)/\(set_In a y).
+  Proof.
+    EAuto with datatypes.
+  Save. 
+
+  Lemma set_diff_intro : (a:A)(x,y:set)
+    (set_In a x) -> ~(set_In a y) -> (set_In a (set_diff x y)).
+  Proof.
+    Induction x.
+    Tauto.
+    Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hay.
+    Rewrite Ha0a; Generalize (set_mem_complete2 Hay).
+    Elim (set_mem a y); [ Intro Habs; Discriminate Habs | Auto with datatypes ].
+    Elim (set_mem a0 y); Auto with datatypes.
+  Save.
+
+  Lemma set_diff_elim1 : (a:A)(x,y:set)
+    (set_In a (set_diff x y)) -> (set_In a x).
+  Proof.
+    Induction x.
+    Tauto.
+    Simpl; Intros a0 l Hrec y; Elim (set_mem a0 y).
+    EAuto with datatypes.
+    Intro; Generalize (set_add_elim  H).
+    Intros [H1 | H2]; EAuto with datatypes.
+  Save.
+
+End first_definitions.
+
+Section other_definitions.
+
+  Variables A,B : Set.
+
+  Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B).
+
+  (* B^A, set of applications from A to B *)
+  Definition set_power : (set A) -> (set B) -> (set (set A*B)) := 
+    (list_power 1!A 2!B).
+
+  Definition set_map : (A->B) -> (set A) ->  (set B) := (map 1!A 2!B).
+
+  Definition set_fold_left : (B -> A -> B) -> (set A) -> B -> B := 
+     (fold_left 1!B 2!A).
+
+  Definition set_fold_right : (A -> B -> B) -> (set A) -> B -> B  := 
+     [f][x][b](fold_right f b x).
+
+ 
+End other_definitions.
+
+Implicit Arguments Off.