diff options
| -rwxr-xr-x | theories/Lists/List.v | 251 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 331 | ||||
| -rw-r--r-- | theories/Lists/PolyList.v | 621 | ||||
| -rw-r--r-- | theories/Lists/PolyListSyntax.v | 7 | ||||
| -rwxr-xr-x | theories/Lists/Streams.v | 165 | ||||
| -rwxr-xr-x | theories/Lists/TheoryList.v | 309 |
6 files changed, 1684 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v new file mode 100755 index 000000000..96dcfbb50 --- /dev/null +++ b/theories/Lists/List.v @@ -0,0 +1,251 @@ + +(* $Id$ *) + +(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED *) +Require Le. + +Parameter List_Dom:Set. +Local A := List_Dom. + +Inductive list : Set := nil : list | cons : A -> list -> list. + +Fixpoint app [l:list] : list -> list + := [m:list]<list>Cases l of + nil => m + | (cons a l1) => (cons a (app l1 m)) + end. + + +Lemma app_nil_end : (l:list)(l=(app l nil)). +Proof. + Intro l ; Elim l ; Simpl ; Auto. + Induction 1; Auto. +Qed. +Hints Resolve app_nil_end : list v62. + +Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)). +Proof. + Intros l m n ; Elim l ; Simpl ; Auto with list. + Induction 1; Auto with list. +Qed. +Hints Resolve app_ass : list v62. + +Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n). +Proof. + Auto with list. +Qed. +Hints Resolve ass_app : list v62. + +Definition tail := + [l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list. + + +Lemma nil_cons : (a:A)(m:list)~nil=(cons a m). + Intros; Discriminate. +Qed. + +(****************************************) +(* Length of lists *) +(****************************************) + +Fixpoint length [l:list] : nat + := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end. + +(******************************) +(* Length order of lists *) +(******************************) + +Section length_order. +Definition lel := [l,m:list](le (length l) (length m)). + +Hints Unfold lel : list. + +Variables a,b:A. +Variables l,m,n:list. + +Lemma lel_refl : (lel l l). +Proof. + Unfold lel ; Auto with list. +Qed. + +Lemma lel_trans : (lel l m)->(lel m n)->(lel l n). +Proof. + Unfold lel ; Intros. + Apply le_trans with (length m) ; Auto with list. +Qed. + +Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)). +Proof. + Unfold lel ; Simpl ; Auto with list arith. +Qed. + +Lemma lel_cons : (lel l m)->(lel l (cons b m)). +Proof. + Unfold lel ; Simpl ; Auto with list arith. +Qed. + +Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m). +Proof. + Unfold lel ; Simpl ; Auto with list arith. +Qed. + +Lemma lel_nil : (l':list)(lel l' nil)->(nil=l'). +Proof. + Intro l' ; Elim l' ; Auto with list arith. + Intros a' y H H0. + (* <list>nil=(cons a' y) + ============================ + H0 : (lel (cons a' y) nil) + H : (lel y nil)->(<list>nil=y) + y : list + a' : A + l' : list *) + Absurd (le (S (length y)) O); Auto with list arith. +Qed. +End length_order. + +Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62. + +Fixpoint In [a:A;l:list] : Prop := + Cases l of + nil => False + | (cons b m) => (b=a)\/(In a m) + end. + +Lemma in_eq : (a:A)(l:list)(In a (cons a l)). +Proof. + Simpl ; Auto with list. +Qed. +Hints Resolve in_eq : list v62. + +Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)). +Proof. + Simpl ; Auto with list. +Qed. +Hints Resolve in_cons : list v62. + +Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)). +Proof. + Intros l m a. + Elim l ; Simpl ; Auto with list. + Intros a0 y H H0. + (* ((<A>a0=a)\/(In a y))\/(In a m) + ============================ + H0 : (<A>a0=a)\/(In a (app y m)) + H : (In a (app y m))->((In a y)\/(In a m)) + y : list + a0 : A + a : A + m : list + l : list *) + Elim H0 ; Auto with list. + Intro H1. + (* ((<A>a0=a)\/(In a y))\/(In a m) + ============================ + H1 : (In a (app y m)) *) + Elim (H H1) ; Auto with list. +Qed. +Hints Immediate in_app_or : list v62. + +Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)). +Proof. + Intros l m a. + Elim l ; Simpl ; Intro H. + (* 1 (In a m) + ============================ + H : False\/(In a m) + a : A + m : list + l : list *) + Elim H ; Auto with list ; Intro H0. + (* (In a m) + ============================ + H0 : False *) + Elim H0. (* subProof completed *) + Intros y H0 H1. + (* 2 (<A>H=a)\/(In a (app y m)) + ============================ + H1 : ((<A>H=a)\/(In a y))\/(In a m) + H0 : ((In a y)\/(In a m))->(In a (app y m)) + y : list *) + Elim H1 ; Auto 4 with list. + Intro H2. + (* (<A>H=a)\/(In a (app y m)) + ============================ + H2 : (<A>H=a)\/(In a y) *) + Elim H2 ; Auto with list. +Qed. +Hints Resolve in_or_app : list v62. + +Definition incl := [l,m:list](a:A)(In a l)->(In a m). + +Hints Unfold incl : list v62. + +Lemma incl_refl : (l:list)(incl l l). +Proof. + Auto with list. +Qed. +Hints Resolve incl_refl : list v62. + +Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)). +Proof. + Auto with list. +Qed. +Hints Immediate incl_tl : list v62. + +Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n). +Proof. + Auto with list. +Qed. + +Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)). +Proof. + Auto with list. +Qed. +Hints Immediate incl_appl : list v62. + +Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)). +Proof. + Auto with list. +Qed. +Hints Immediate incl_appr : list v62. + +Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m). +Proof. + Unfold incl ; Simpl ; Intros a l m H H0 a0 H1. + (* (In a0 m) + ============================ + H1 : (<A>a=a0)\/(In a0 l) + a0 : A + H0 : (a:A)(In a l)->(In a m) + H : (In a m) + m : list + l : list + a : A *) + Elim H1. + (* 1 (<A>a=a0)->(In a0 m) *) + Elim H1 ; Auto with list ; Intro H2. + (* (<A>a=a0)->(In a0 m) + ============================ + H2 : <A>a=a0 *) + Elim H2 ; Auto with list. (* solves subgoal *) + (* 2 (In a0 l)->(In a0 m) *) + Auto with list. +Qed. +Hints Resolve incl_cons : list v62. + +Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n). +Proof. + Unfold incl ; Simpl ; Intros l m n H H0 a H1. + (* (In a n) + ============================ + H1 : (In a (app l m)) + a : A + H0 : (a:A)(In a m)->(In a n) + H : (a:A)(In a l)->(In a n) + n : list + m : list + l : list *) + Elim (in_app_or l m a) ; Auto with list. +Qed. +Hints Resolve incl_app : list v62. 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. diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v new file mode 100644 index 000000000..1fe019af3 --- /dev/null +++ b/theories/Lists/PolyList.v @@ -0,0 +1,621 @@ + +(* $Id$ *) + +Require Le. + + +Section Lists. + +Variable A : Set. + +Implicit Arguments On. + +Inductive list : Set := nil : list | cons : A -> list -> list. + +(*************************) +(* Concatenation *) +(*************************) + +Fixpoint app [l:list] : list -> list + := [m:list]Cases l of + nil => m + | (cons a l1) => (cons a (app l1 m)) + end. + +Infix RIGHTA 7 "^" app. + +Lemma app_nil_end : (l:list)l=(l^nil). +Proof. + Induction l ; Simpl ; Auto. + (* l : list + ============================ + (a:A)(y:list) + y=(app y nil)->(cons a y)=(cons a (app y nil)) *) + Induction 1; Auto. +Qed. +Hints Resolve app_nil_end. + +Lemma app_ass : (l,m,n : list)((l^m)^ n)=(l^(m^n)). +Proof. + Intros l m n ; Elim l ; Simpl ; Auto. + (* l : list + m : list + n : list + ============================ + (a:A)(y:list)(app (app y m) n)=(app y (app m n)) + ->(cons a (app (app y m) n))=(cons a (app y (app m n))) *) + Induction 1; Auto. +Qed. +Hints Resolve app_ass. + +Lemma ass_app : (l,m,n : list)(l^(m^n))=((l^m)^n). +Proof. + Auto. +Qed. +Hints Resolve ass_app. + +Definition head := + [l:list]Cases l of + | nil => Error + | (cons x _) => (Value x) + end. + +Definition tail : list -> list := + [l:list]Cases l of + | nil => nil + | (cons a m) => m + end. + +Lemma nil_cons : (a:A)(m:list)~(nil=(cons a m)). +Intros; Discriminate. +Qed. + +Lemma app_comm_cons : (x,y:list)(a:A) (cons a (x^y))=((cons a x)^y). +Proof. + Auto. +Qed. + +Lemma app_eq_nil: (x,y:list) (x^y)=nil -> x=nil /\ y=nil. +Proof. + (Destruct x;Destruct y;Simpl;Auto). + (Intros H;Discriminate H). + (Intros a0 l0 H;Discriminate H). +Qed. + +Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)). +Proof. +Unfold not . + (Induction x;Simpl;Intros). + Discriminate H. + Discriminate H0. +Qed. + +Lemma app_eq_unit:(x,y:list)(a:A) + (x^y)=(cons a nil)-> (x=nil)/\ y=(cons a nil) \/ x=(cons a nil)/\ y=nil. + +Proof. + (Destruct x;Destruct y;Simpl). + (Intros a H;Discriminate H). + (Left;Split;Auto). + (Right;Split;Auto). + Generalize H . + (Generalize (app_nil_end l) ;Intros E). + (Rewrite <- E;Auto). + Intros. + Injection H. + Intro. + (Cut nil=(l^(cons a0 l0));Auto). + Intro. + Generalize (app_cons_not_nil H1); Intro. + Elim H2. +Qed. + +Lemma app_inj_tail : (x,y:list)(a,b:A) + (x^(cons a nil))=(y^(cons b nil)) -> x=y /\ a=b. +Proof. + (Induction x;Induction y;Simpl;Auto). + Intros. + Injection H. + Auto. + Intros. + (Injection H0;Intros). + (Generalize (app_cons_not_nil H1) ;Induction 1). + Intros. + (Injection H0;Intros). + (Cut nil=(l^(cons a0 nil));Auto). + Intro. + (Generalize (app_cons_not_nil H3) ;Induction 1). + Intros. + (Injection H1;Intros). + Generalize (H l0 a1 b H2) . + (Induction 1;Split;Auto). + (Rewrite <- H3;Rewrite <- H5;Auto). +Qed. + +(****************************************) +(* Length of lists *) +(****************************************) + +Fixpoint length [l:list] : nat + := Cases l of nil => O | (cons _ m) => (S (length m)) end. + +(******************************) +(* Length order of lists *) +(******************************) + +Section length_order. +Definition lel := [l,m:list](le (length l) (length m)). + +Variables a,b:A. +Variables l,m,n:list. + +Lemma lel_refl : (lel l l). +Proof. + Unfold lel ; Auto with arith. +Qed. + +Lemma lel_trans : (lel l m)->(lel m n)->(lel l n). +Proof. + Unfold lel ; Intros. + (* H0 : (le (length m) (length n)) + H : (le (length l) (length m)) + ============================ + (le (length l) (length n)) *) + Apply le_trans with (length m) ; Auto with arith. +Qed. + +Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)). +Proof. + Unfold lel ; Simpl ; Auto with arith. +Qed. + +Lemma lel_cons : (lel l m)->(lel l (cons b m)). +Proof. + Unfold lel ; Simpl ; Auto with arith. +Qed. + +Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m). +Proof. + Unfold lel ; Simpl ; Auto with arith. +Qed. + +Lemma lel_nil : (l':list)(lel l' nil)->(nil=l'). +Proof. + Intro l' ; Elim l' ; Auto with arith. + Intros a' y H H0. + (* l' : list + a' : A + y : list + H : (lel y nil)->nil=y + H0 : (lel (cons a' y) nil) + ============================ + nil=(cons a' y) *) + Absurd (le (S (length y)) O); Auto with arith. +Qed. +End length_order. + +Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons +. + +(*********************************) +(* The In predicate *) +(*********************************) + +Fixpoint In [a:A;l:list] : Prop := + Cases l of nil => False | (cons b m) => (b=a)\/(In a m) end. + +Lemma in_eq : (a:A)(l:list)(In a (cons a l)). +Proof. + Simpl ; Auto. +Qed. +Hints Resolve in_eq. + +Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)). +Proof. + Simpl ; Auto. +Qed. +Hints Resolve in_cons. + +Lemma in_nil : (a:A)~(In a nil). +Proof. +Unfold not; Intros a H; Inversion_clear H. +Qed. + + +Lemma in_inv : (a,b:A)(l:list) + (In b (cons a l)) -> a=b \/ (In b l). +Proof. + Intros a b l H ; Inversion_clear H ; Auto. +Qed. + +Lemma In_dec : ((x,y:A){x=y}+{~x=y}) -> (a:A)(l:list){(In a l)}+{~(In a l)}. + +Proof. + Induction l. + Right; Apply in_nil. + Intros; Elim H0; Simpl; Elim (H a0 a); Auto. + Right; Unfold not; Intros [Hc1 | Hc2]; Auto. +Save. + +Lemma in_app_or : (l,m:list)(a:A)(In a (l^m))->((In a l)\/(In a m)). +Proof. + Intros l m a. + Elim l ; Simpl ; Auto. + Intros a0 y H H0. + (* a0=a\/(In a y))\/(In a m) + ============================ + H0 : a0=a\/(In a (app y m)) + H : (In a (app y m))->((In a y)\/(In a m)) + y : list + a0 : A + a : A + m : list + l : list *) + Elim H0 ; Auto. + Intro H1. + (* (a0=a\/(In a y))\/(In a m) + ============================ + H1 : (In a (app y m)) *) + Elim (H H1) ; Auto. +Qed. +Hints Immediate in_app_or. + +Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (l^m)). +Proof. + Intros l m a. + Elim l ; Simpl ; Intro H. + (* 1 (In a m) + ============================ + H : False\/(In a m) + a : A + m : list + l : list *) + Elim H ; Auto ; Intro H0. + (* (In a m) + ============================ + H0 : False *) + Elim H0. (* subProof completed *) + Intros y H0 H1. + (* 2 H=a\/(In a (app y m)) + ============================ + H1 : (H=a\/(In a y))\/(In a m) + H0 : ((In a y)\/(In a m))->(In a (app y m)) + y : list *) + Elim H1 ; Auto 4. + Intro H2. + (* H=a\/(In a (app y m)) + ============================ + H2 : H=a\/(In a y) *) + Elim H2 ; Auto. +Qed. +Hints Resolve in_or_app. + +(**********************) +(* Inclusion on list *) +(**********************) +Definition incl := [l,m:list](a:A)(In a l)->(In a m). +Hints Unfold incl. + +Lemma incl_refl : (l:list)(incl l l). +Proof. + Auto. +Qed. +Hints Resolve incl_refl. + +Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)). +Proof. + Auto. +Qed. +Hints Immediate incl_tl. + +Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n). +Proof. + Auto. +Qed. + +Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (n^m)). +Proof. + Auto. +Qed. +Hints Immediate incl_appl. + +Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (m^n)). +Proof. + Auto. +Qed. +Hints Immediate incl_appr. + +Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m). +Proof. + Unfold incl ; Simpl ; Intros a l m H H0 a0 H1. + (* a : A + l : list + m : list + H : (In a m) + H0 : (a:A)(In a l)->(In a m) + a0 : A + H1 : a=a0\/(In a0 l) + ============================ + (In a0 m) *) + Elim H1. + (* 1 a=a0->(In a0 m) *) + Elim H1 ; Auto ; Intro H2. + (* H2 : a=a0 + ============================ + a=a0->(In a0 m) *) + Elim H2 ; Auto. (* solves subgoal *) + (* 2 (In a0 l)->(In a0 m) *) + Auto. +Qed. +Hints Resolve incl_cons. + +Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (l^m) n). +Proof. + Unfold incl ; Simpl ; Intros l m n H H0 a H1. + (* l : list + n : list + m : list + H : (a:A)(In a l)->(In a n) + H0 : (a:A)(In a m)->(In a n) + a : A + H1 : (In a (app l m)) + ============================ + (In a n) *) + Elim (in_app_or H1); Auto. +Qed. +Hints Resolve incl_app. + +(*************************) +(* Nth element of a list *) +(*************************) +Fixpoint nth [n:nat; l:list] : A->A := + [default]Cases n l of + O (cons x l') => x + | O other => default + | (S m) nil => default + | (S m) (cons x t) => (nth m t default) + end. + +Fixpoint nth_ok [n:nat; l:list] : A->bool := + [default]Cases n l of + O (cons x l') => true + | O other => false + | (S m) nil => false + | (S m) (cons x t) => (nth_ok m t default) + end. + +Lemma nth_in_or_default : + (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}. +Realizer nth_ok. +Program_all. +Save. + +Lemma nth_S_cons : + (n:nat)(l:list)(d:A)(a:A)(In (nth n l d) l) + ->(In (nth (S n) (cons a l) d) (cons a l)). +Simpl; Auto. +Save. + +(***** +Lemma nth_In : + (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l). + +Unfold lt; Intros n l d Hnl. +Inversion Hnl. +Generalize H0; Elim l; +[ Simpl; Intros; Inversion H1 +| ] + +Unfold lt; Induction l; +[ Simpl; Intros; Inversion H +| Simpl; Intros; +]. +******) + + +(*********************************************) +(* Reverse Induction Principle on Lists *) +(*********************************************) +Section Reverse_Induction. + +Variable leA: A->A->Prop. + +Fixpoint rev [l:list] : list := + Cases l of + nil => nil + | (cons x l') => (rev l')^(cons x nil) + end. + +Lemma distr_rev : + (x,y:list) (rev (x^y))=((rev y)^(rev x)). +Proof. + Induction x. + Induction y. + Simpl. + Auto. + + Simpl. + Intros. + (Apply app_nil_end;Auto). + + Intros. + Simpl. + (Generalize (H y) ;Intros E;Rewrite -> E). + Apply (app_ass (rev y) (rev l) (cons a nil)). +Qed. + +Remark rev_unit : (l:list)(a:A) (rev l^(cons a nil))= (cons a (rev l)). +Proof. + Intros. + (Apply (distr_rev l (cons a nil));Simpl;Auto). +Qed. + +Lemma idempot_rev : (l:list)(rev (rev l))=l. +Proof. + Induction l. + (Simpl;Auto). + + Intros. + Simpl. + Generalize (rev_unit (rev l0) a); Intros. + Rewrite -> H0. + Rewrite -> H;Auto. +Qed. + +Implicit Arguments Off. +Remark rev_list_ind: (P:list->Prop) + (P nil) + ->((a:A)(l:list)(P (rev l))->(P (rev (cons a l)))) + ->(l:list) (P (rev l)). +Proof. + Induction l; Auto. +Qed. +Implicit Arguments On. + +Lemma rev_ind : + (P:list->Prop) + (P nil)-> + ((x:A)(l:list)(P l)->(P l^(cons x nil))) + ->(l:list)(P l). +Proof. + Intros. + Generalize (idempot_rev l) . + (Intros E;Rewrite <- E). + Apply (rev_list_ind P). + Auto. + + Simpl. + Intros. + Apply (H0 a (rev l0)). + Auto. +Qed. + +End Reverse_Induction. + +End Lists. + +Hints Resolve nil_cons app_nil_end ass_app app_ass : datatypes v62. +Hints Resolve app_comm_cons app_cons_not_nil : datatypes v62. +Hints Immediate app_eq_nil : datatypes v62. +Hints Resolve app_eq_unit app_inj_tail : datatypes v62. +Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons + : datatypes v62. +Hints Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app : datatypes v62. +Hints Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons incl_app + : datatypes v62. + +Section Functions_on_lists. + +(***************************************************************) +(* Some generic functions on lists and basic functions of them *) +(***************************************************************) + +Section Map. +Variables A,B:Set. +Variable f:A->B. +Fixpoint map [l:(list A)] : (list B) := + Cases l of + nil => (nil B) + | (cons a t) => (cons (f a) (map t)) + end. +End Map. + +Lemma in_map : (A,B:Set)(f:A->B)(l:(list A))(x:A) + (In x l) -> (In (f x) (map f l)). +Induction l; Simpl; +[ Auto +| Intros; Elim H0; Intros; + [ Left; Apply f_equal with f:=f; Assumption + | Auto] +]. +Save. + +Fixpoint flat_map [A,B:Set; f:A->(list B); l:(list A)] : (list B) := + Cases l of + nil => (nil B) + | (cons x t) => (app (f x) (flat_map f t)) + end. + +Fixpoint list_prod [A:Set; B:Set; l:(list A)] : (list B)->(list A*B) := + [l']Cases l of + nil => (nil A*B) + | (cons x t) => (app (map [y:B](x,y) l') + (list_prod t l')) + end. + +Lemma in_prod_aux : + (A:Set)(B:Set)(x:A)(y:B)(l:(list B)) + (In y l) -> (In (x,y) (map [y0:B](x,y0) l)). +Induction l; +[ Simpl; Auto +| Simpl; Intros; Elim H0; + [ Left; Rewrite H1; Trivial + | Right; Auto] +]. +Save. + +Lemma in_prod : (A:Set)(B:Set)(l:(list A))(l':(list B)) + (x:A)(y:B)(In x l)->(In y l')->(In (x,y) (list_prod l l')). +Induction l; +[ Simpl; Tauto +| Simpl; Intros; Apply in_or_app; Elim H0; Clear H0; + [ Left; Rewrite H0; Apply in_prod_aux; Assumption + | Right; Auto] +]. +Save. + +(* (list_power x y) is y^x, or the set of sequences of elts of y + indexed by elts of x, sorted in lexicographic order. *) + +Fixpoint list_power [A,B:Set; l:(list A)] : (list B)->(list (list A*B)) := + [l']Cases l of + nil => (cons (nil A*B) (nil ?)) + | (cons x t) => (flat_map [f:(list A*B)](map [y:B](cons (x,y) f) l') + (list_power t l')) + end. + +Section Fold_Left_Recursor. +Variables A,B:Set. +Variable f:A->B->A. +Fixpoint fold_left[l:(list B)] : A -> A := +[a0]Cases l of + nil => a0 + | (cons b t) => (fold_left t (f a0 b)) + end. +End Fold_Left_Recursor. + +Section Fold_Right_Recursor. +Variables A,B:Set. +Variable f:B->A->A. +Variable a0:A. +Fixpoint fold_right [l:(list B)] : A := + Cases l of + nil => a0 + | (cons b t) => (f b (fold_right t)) + end. +End Fold_Right_Recursor. + +(* +Theorem fold_symmetric : + (A:Set)(f:A->A->A) + ((x,y,z:A)(f x (f y z))=(f (f x y) z)) + ->((x,y:A)(f x y)=(f y x)) + ->(a0:A)(l:(list A))(fold_left f l a0)=(fold_right f a0 l). +Induction l. +Reflexivity. +Simpl; Intros. +Rewrite <- H1. +Generalize a0 a. +Elim l0; Simpl. +Trivial. +Intros. +Repeat Rewrite H2. +Do 2 Rewrite H. +Rewrite (H0 a1 a3). +Reflexivity. +Save. +*) + +End Functions_on_lists. + +Implicit Arguments Off. diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v new file mode 100644 index 000000000..a19a3dcc1 --- /dev/null +++ b/theories/Lists/PolyListSyntax.v @@ -0,0 +1,7 @@ + +(* $Id$ *) + +(* Syntax for list concatenation *) +Require PolyList. + +Infix RIGHTA 7 "^" app. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v new file mode 100755 index 000000000..6b7ffca5e --- /dev/null +++ b/theories/Lists/Streams.v @@ -0,0 +1,165 @@ + +(* $Id$ *) + +Implicit Arguments On. + +Section Streams. (* The set of streams : definition *) + +Variable A : Set. + +CoInductive Set Stream := Cons : A->Stream->Stream. + + +Definition hd := + [x:Stream] Cases x of (Cons a _) => a end. + +Definition tl := + [x:Stream] Cases x of (Cons _ s) => s end. + + +Fixpoint Str_nth_tl [n:nat] : Stream->Stream := + [s:Stream] Cases n of + O => s + |(S m) => (Str_nth_tl m (tl s)) + end. + +Definition Str_nth : nat->Stream->A := [n:nat][s:Stream](hd (Str_nth_tl n s)). + + +Lemma unfold_Stream :(x:Stream)x=(Cases x of (Cons a s) => (Cons a s) end). +Proof. + Intro x. + Case x. + Trivial. +Qed. + +Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)). +Proof. + Induction n; Simpl; Auto. +Save. +Hints Resolve tl_nth_tl : datatypes v62. + +Lemma Str_nth_tl_plus +: (n,m:nat)(s:Stream)(Str_nth_tl n (Str_nth_tl m s))=(Str_nth_tl (plus n m) s). +Induction n; Simpl; Intros; Auto with datatypes. +Rewrite <- H. +Rewrite tl_nth_tl; Trivial with datatypes. +Save. + +Lemma Str_nth_plus + : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s). +Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes. +Save. + +(* Extensional Equality between two streams *) + +CoInductive EqSt : Stream->Stream->Prop := + eqst : (s1,s2:Stream) + ((hd s1)=(hd s2))-> + (EqSt (tl s1) (tl s2)) + ->(EqSt s1 s2). + +(* A coinduction principle *) + +Tactic Definition CoInduction [$proof] := + [ <:tactic:<( Cofix $proof; (Intros; (Constructor; + [Clear $proof | Try (Apply $proof;Clear $proof)])))>> ]. + + +(* Extensional equality is an equivalence relation *) + + +Theorem EqSt_reflex : (s:Stream)(EqSt s s). +CoInduction EqSt_reflex. +Reflexivity. +Qed. + +Theorem sym_EqSt : + (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1). +CoInduction Eq_sym. +(Case H;Intros;Symmetry;Assumption). +(Case H;Intros;Assumption). +Qed. + + +Theorem trans_EqSt : + (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3). +CoInduction Eq_trans. +Transitivity (hd s2). +(Case H; Intros; Assumption). +(Case H0; Intros; Assumption). +Apply (Eq_trans (tl s1) (tl s2) (tl s3)). +(Case H; Trivial with datatypes). +(Case H0; Trivial with datatypes). +Qed. + +(* +The definition given is equivalent to require the elements at each position to be equal +*) + +Theorem eqst_ntheq : + (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2). +Unfold Str_nth; Induction n. +Intros s1 s2 H; Case H; Trivial with datatypes. +Intros m hypind. +Simpl. +Intros s1 s2 H. +Apply hypind. +(Case H; Trivial with datatypes). +Qed. + +Theorem ntheq_eqst : + (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2). +CoInduction Equiv2. +Apply (H O). +Intros n; Apply (H (S n)). +Qed. + +Section Stream_Properties. + +Variable P : Stream->Prop. + +(* +Inductive Exists : Stream -> Prop := + Here : (x:Stream)(P x) ->(Exists x) | + Further : (x:Stream)~(P x)->(Exists (tl x))->(Exists x). +*) + +Inductive Exists : Stream -> Prop := + Here : (x:Stream)(P x) ->(Exists x) | + Further : (x:Stream)(Exists (tl x))->(Exists x). + +CoInductive ForAll : Stream -> Prop := + forall : (x:Stream)(P x)->(ForAll (tl x))->(ForAll x). + + +Section Co_Induction_ForAll. +Variable Inv : Stream -> Prop. +Hypothesis InvThenP : (x:Stream)(Inv x)->(P x). +Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)). + +Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x). +CoInduction ForAll_coind;Auto. +Qed. +End Co_Induction_ForAll. + +End Stream_Properties. + +End Streams. + +Section Map. +Variables A,B : Set. +Variable f : A->B. +CoFixpoint map : (Stream A)->(Stream B) := + [s:(Stream A)](Cons (f (hd s)) (map (tl s))). +End Map. + +Section Constant_Stream. +Variables A : Set. +Variable a : A. +CoFixpoint const : (Stream A) := (Cons a const). +End Constant_Stream. + + + +Implicit Arguments Off. diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v new file mode 100755 index 000000000..d97b207f0 --- /dev/null +++ b/theories/Lists/TheoryList.v @@ -0,0 +1,309 @@ + +(* $Id$ *) + +(* Some programs and results about lists following CAML Manual *) + +Require Export PolyList. +Implicit Arguments On. +Chapter Lists. + +Variable A : Set. + +(*********************) +(* The null function *) +(*********************) + +Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l. + +Lemma Isnil_nil : (Isnil (nil A)). +Red; Auto. +Save. +Hints Resolve Isnil_nil. + +Lemma not_Isnil_cons : (a:A)(l:(list A))~(Isnil (cons a l)). +Unfold Isnil. +Intros; Discriminate. +Save. + +Hints Resolve Isnil_nil not_Isnil_cons. + +Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}. +Realizer [l:(list A)]Cases l of + | nil => true + | _ => false + end. +Program_all. +Save. + +(***********************) +(* The Uncons function *) +(***********************) + +Lemma Uncons : (l:(list A)){a : A & { m: (list A) | (cons a m)=l}}+{Isnil l}. +Realizer [l:(list A)]<(Exc A*(list A))>Cases l of + | nil => Error + | (cons a m) => (Value (a,m)) + end. +Program_all. +Save. + +(********************************) +(* The head function *) +(********************************) + +Lemma Hd : (l:(list A)){a : A | (EX m:(list A) |(cons a m)=l)}+{Isnil l}. +Realizer [l:(list A)]<(Exc A)>Cases l of + | nil => Error + | (cons a m) => (Value a) + end. +Program_all. + Exists m; Auto. +Save. + +Lemma Tl : (l:(list A)){m:(list A)| (EX a:A |(cons a m)=l) + \/ ((Isnil l) /\ (Isnil m)) }. +Realizer [l:(list A)]Cases l of + | nil => (nil A) + | (cons a m) => m + end. +Program_all. + Left; Exists a; Auto. +Save. + +(****************************************) +(* Length of lists *) +(****************************************) + +(* length is defined in PolyList *) +Fixpoint Length_l [l:(list A)] : nat -> nat + := [n:nat] Cases l of + nil => n + | (cons _ m) => (Length_l m (S n)) + end. + +(* A tail recursive version *) +Lemma Length_l_pf : (l:(list A))(n:nat){m:nat|(plus n (length l))=m}. +Realizer Length_l. +Program_all. +Simpl; Auto. +Elim e; Simpl; Auto. +Save. + +Lemma Length : (l:(list A)){m:nat|(length l)=m}. +Realizer [l:(list A)](Length_l_pf l O). +Program_all. +Save. + +(*******************************) +(* Members of lists *) +(*******************************) +Inductive In_spec [a:A] : (list A) -> Prop := + | in_hd : (l:(list A))(In_spec a (cons a l)) + | in_tl : (l:(list A))(b:A)(In a l)->(In_spec a (cons b l)). +Hints Resolve in_hd in_tl. +Hints Unfold In. +Hints Resolve in_cons. + +Theorem In_In_spec : (a:A)(l:(list A))(In a l) <-> (In_spec a l). +Split. +Elim l; [ Intros; Contradiction + | Intros; Elim H0; + [ Intros; Rewrite H1; Auto + | Auto ]]. +Intros; Elim H; Auto. +Save. + +Inductive AllS [P:A->Prop] : (list A) -> Prop + := allS_nil : (AllS P (nil A)) + | allS_cons : (a:A)(l:(list A))(P a)->(AllS P l)->(AllS P (cons a l)). +Hints Resolve allS_nil allS_cons. + +Hypothesis eqA_dec : (a,b:A){a=b}+{~a=b}. + +Fixpoint mem [a:A; l:(list A)] : bool := + Cases l of + nil => false + | (cons b m) => if (eqA_dec a b) then [H]true else [H](mem a m) + end. + +Hints Unfold In. +Lemma Mem : (a:A)(l:(list A)){(In a l)}+{(AllS [b:A]~b=a l)}. +Realizer mem. +Program_all. +Save. + +(**********************************) +(* Index of elements *) +(**********************************) + +Require Le. +Require Lt. + +Inductive nth_spec : (list A)->nat->A->Prop := + nth_spec_O : (a:A)(l:(list A))(nth_spec (cons a l) (S O) a) +| nth_spec_S : (n:nat)(a,b:A)(l:(list A)) + (nth_spec l n a)->(nth_spec (cons b l) (S n) a). +Hints Resolve nth_spec_O nth_spec_S. + +Inductive fst_nth_spec : (list A)->nat->A->Prop := + fst_nth_O : (a:A)(l:(list A))(fst_nth_spec (cons a l) (S O) a) +| fst_nth_S : (n:nat)(a,b:A)(l:(list A))(~a=b)-> + (fst_nth_spec l n a)->(fst_nth_spec (cons b l) (S n) a). +Hints Resolve fst_nth_O fst_nth_S. + +Lemma fst_nth_nth : (l:(list A))(n:nat)(a:A)(fst_nth_spec l n a)->(nth_spec l n a). +Induction 1; Auto. +Save. +Hints Immediate fst_nth_nth. + +Lemma nth_lt_O : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(lt O n). +Induction 1; Auto. +Save. + +Lemma nth_le_length : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(le n (length l)). + Induction 1; Simpl; Auto with arith. +Save. + +Fixpoint Nth_func [l:(list A)] : nat -> (Exc A) + := [n:nat] Cases l n of + (cons a _) (S O) => (value A a) + | (cons _ l') (S (S p)) => (Nth_func l' (S p)) + | _ _ => Error + end. + +Lemma Nth : (l:(list A))(n:nat) + {a:A|(nth_spec l n a)}+{(n=O)\/(lt (length l) n)}. +Realizer Nth_func. +Program_all. +Simpl; Elim n; Auto with arith. +(Elim o; Intro); [Absurd ((S p)=O); Auto with arith | Auto with arith]. +Save. + +Lemma Item : (l:(list A))(n:nat){a:A|(nth_spec l (S n) a)}+{(le (length l) n)}. +Realizer [l:(list A)][n:nat](Nth l (S n)). +Program_all. +Elim o; Intro; [Absurd ((S n)=O); Auto with arith | Auto with arith]. +Save. + +Require Minus. +Require DecBool. + +Fixpoint index_p [a:A;l:(list A)] : nat -> (Exc nat) := + Cases l of nil => [p]Error + | (cons b m) => [p](ifdec (eqA_dec a b) (Value p) (index_p a m (S p))) + end. + +Lemma Index_p : (a:A)(l:(list A))(p:nat) + {n:nat|(fst_nth_spec l (minus (S n) p) a)}+{(AllS [b:A]~a=b l)}. +Realizer index_p. +Program_all. +Elim e; Elim minus_Sn_m; Trivial; Elim minus_n_n; Auto with arith. +Elim minus_Sn_m; Auto with arith. +Apply lt_le_weak; Apply lt_O_minus_lt; Apply nth_lt_O with m a; Auto with arith. +Save. + +Lemma Index : (a:A)(l:(list A)) + {n:nat|(fst_nth_spec l n a)}+{(AllS [b:A]~a=b l)}. +Realizer [a:A][l:(list A)](Index_p a l (S O)). +Program_all. +Rewrite (minus_n_O n0); Auto with arith. +Save. + +Section Find_sec. +Variable R,P : A -> Prop. + +Inductive InR : (list A) -> Prop + := inR_hd : (a:A)(l:(list A))(R a)->(InR (cons a l)) + | inR_tl : (a:A)(l:(list A))(InR l)->(InR (cons a l)). +Hints Resolve inR_hd inR_tl. + +Definition InR_inv := + [l:(list A)]Cases l of + nil => False + | (cons b m) => (R b)\/(InR m) + end. + +Lemma InR_INV : (l:(list A))(InR l)->(InR_inv l). +Induction 1; Simpl; Auto. +Save. + +Lemma InR_cons_inv : (a:A)(l:(list A))(InR (cons a l))->((R a)\/(InR l)). +Intros a l H; Exact (InR_INV H). +Save. + +Lemma InR_or_app : (l,m:(list A))((InR l)\/(InR m))->(InR (app l m)). +Induction 1. +Induction 1; Simpl; Auto. +Intro; Elim l; Simpl; Auto. +Save. + +Lemma InR_app_or : (l,m:(list A))(InR (app l m))->((InR l)\/(InR m)). +Intros l m; Elim l; Simpl; Auto. +Intros b l' Hrec IAc; Elim (InR_cons_inv IAc);Auto. +Intros; Elim Hrec; Auto. +Save. + +Hypothesis RS_dec : (a:A){(R a)}+{(P a)}. + +Fixpoint find [l:(list A)] : (Exc A) := + Cases l of nil => Error + | (cons a m) => (ifdec (RS_dec a) (Value a) (find m)) + end. + +Lemma Find : (l:(list A)){a:A | (In a l) & (R a)}+{(AllS P l)}. +Realizer find. +Program_all. +Save. + +Variable B : Set. +Variable T : A -> B -> Prop. + +Variable TS_dec : (a:A){c:B| (T a c)}+{(P a)}. + +Fixpoint try_find [l:(list A)] : (Exc B) := + Cases l of + nil => Error + | (cons a l1) => + Cases (TS_dec a) of + (inleft (exist c _)) => (Value c) + | (inright _) => (try_find l1) + end + end. + +Lemma Try_find : (l:(list A)){c:B|(EX a:A |(In a l) & (T a c))}+{(AllS P l)}. +Realizer try_find. +Program_all. +Exists a; Auto. +Elim e; Intros a1 H1 H2. +Exists a1; Auto. +Save. + +End Find_sec. + +Section Assoc_sec. + +Variable B : Set. +Fixpoint assoc [a:A;l:(list A*B)] : (Exc B) := + Cases l of nil => Error + | (cons (a',b) m) => (ifdec (eqA_dec a a') (Value b) (assoc a m)) + end. + +Inductive AllS_assoc [P:A -> Prop]: (list A*B) -> Prop := + allS_assoc_nil : (AllS_assoc P (nil A*B)) + | allS_assoc_cons : (a:A)(b:B)(l:(list A*B)) + (P a)->(AllS_assoc P l)->(AllS_assoc P (cons (a,b) l)). + +Hints Resolve allS_assoc_nil allS_assoc_cons. + +Lemma Assoc : (a:A)(l:(list A*B))(B+{(AllS_assoc [a':A]~(a=a') l)}). +Realizer assoc. +Program_all. +Save. + +End Assoc_sec. + +End Lists. + +Hints Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons + : datatypes. +Hints Immediate fst_nth_nth : datatypes. |