diff options
Diffstat (limited to 'theories7/Lists')
| -rwxr-xr-x | theories7/Lists/List.v | 261 | ||||
| -rw-r--r-- | theories7/Lists/ListSet.v | 389 | ||||
| -rwxr-xr-x | theories7/Lists/MonoList.v | 259 | ||||
| -rw-r--r-- | theories7/Lists/PolyList.v | 646 | ||||
| -rw-r--r-- | theories7/Lists/PolyListSyntax.v | 10 | ||||
| -rwxr-xr-x | theories7/Lists/Streams.v | 170 | ||||
| -rwxr-xr-x | theories7/Lists/TheoryList.v | 386 |
7 files changed, 2121 insertions, 0 deletions
diff --git a/theories7/Lists/List.v b/theories7/Lists/List.v new file mode 100755 index 00000000..574b2688 --- /dev/null +++ b/theories7/Lists/List.v @@ -0,0 +1,261 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: List.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*) + +(* This file is a copy of file MonoList.v *) + +(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) + +Require Le. + +Parameter List_Dom:Set. +Definition 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/theories7/Lists/ListSet.v b/theories7/Lists/ListSet.v new file mode 100644 index 00000000..9bf259da --- /dev/null +++ b/theories7/Lists/ListSet.v @@ -0,0 +1,389 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ListSet.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*) + +(** 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. + +Set Implicit Arguments. +V7only [Implicits nil [1].]. + +Section first_definitions. + + Variable A : Set. + Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}. + + Definition set := (list A). + + Definition empty_set := (!nil ?) : set. + + Fixpoint set_add [a:A; x:set] : set := + Cases x of + | nil => (cons a nil) + | (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 + | (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 + | (cons a1 x1) => if (set_mem a1 y) + then (set_diff x1 y) + else (set_add a1 (set_diff x1 y)) + end. + + + 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. ***) + Induction x. + Auto. + Intros a0 x0 Ha0. Case (Aeq_dec a a0); Intro eq. + Rewrite eq; Simpl; Auto with datatypes. + Elim Ha0. + Auto with datatypes. + Right; Simpl; Unfold not; Intros [Hc1 | Hc2 ]; Auto with datatypes. + Qed. + + 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. + Qed. + + Lemma set_mem_ind2 : + (B:Set)(P:B->Prop)(y,z:B)(a:A)(x:set) + ((set_In a x) -> (P y)) + ->(~(set_In a x) -> (P z)) + ->(P (if (set_mem a x) then y else z)). + + Proof. + Induction x; Simpl; Intros. + Apply H0; Red; Trivial. + Case (Aeq_dec a a0); Auto with datatypes. + Intro; Apply H; Intros; Auto. + Apply H1; Red; Intro. + Case H3; Auto. + Qed. + + + 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. + Qed. + + 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. + Qed. + + 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. + Qed. + + 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. + Qed. + + 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 ]. + Qed. + + 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 ]. + Qed. + + 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. + Qed. + + 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). + Simpl; Tauto. + Simpl; Intros; Elim H0. + Trivial with datatypes. + Tauto. + Tauto. + Qed. + + Lemma set_add_elim2 : (a,b:A)(x:set) + (set_In a (set_add b x)) -> ~(a=b) -> (set_In a x). + Intros a b x H; Case (set_add_elim H); Intros; Trivial. + Case H1; Trivial. + Qed. + + Hints Resolve set_add_intro set_add_elim set_add_elim2. + + 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. + Qed. + + + 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. + Qed. + + 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. + Qed. + + 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. + Qed. + + 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. + Qed. + + Lemma set_union_emptyL : (a:A)(x:set)(set_In a (set_union empty_set x)) -> (set_In a x). + Intros a x H; Case (set_union_elim H); Auto Orelse Contradiction. + Qed. + + + Lemma set_union_emptyR : (a:A)(x:set)(set_In a (set_union x empty_set)) -> (set_In a x). + Intros a x H; Case (set_union_elim H); Auto Orelse Contradiction. + Qed. + + + 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]. + Qed. + + 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. + Qed. + + Lemma set_inter_elim2 : (a:A)(x,y:set) + (set_In a (set_inter x y)) -> (set_In a y). + Proof. + Induction x. + Simpl; 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. + Qed. + + 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. + Qed. + + 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. + Simpl; 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. + Qed. + + Lemma set_diff_elim1 : (a:A)(x,y:set) + (set_In a (set_diff x y)) -> (set_In a x). + Proof. + Induction x. + Simpl; 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. + Qed. + + Lemma set_diff_elim2 : (a:A)(x,y:set) + (set_In a (set_diff x y)) -> ~(set_In a y). + Intros a x y; Elim x; Simpl. + Intros; Contradiction. + Intros a0 l Hrec. + Apply set_mem_ind2; Auto. + Intros H1 H2; Case (set_add_elim H2); Intros; Auto. + Rewrite H; Trivial. + Qed. + + Lemma set_diff_trivial : (a:A)(x:set)~(set_In a (set_diff x x)). + Red; Intros a x H. + Apply (set_diff_elim2 H). + Apply (set_diff_elim1 H). + Qed. + +Hints Resolve set_diff_intro set_diff_trivial. + + +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. + +V7only [Implicits nil [].]. +Unset Implicit Arguments. diff --git a/theories7/Lists/MonoList.v b/theories7/Lists/MonoList.v new file mode 100755 index 00000000..2ab78f7f --- /dev/null +++ b/theories7/Lists/MonoList.v @@ -0,0 +1,259 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: MonoList.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*) + +(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) + +Require Le. + +Parameter List_Dom:Set. +Definition 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/theories7/Lists/PolyList.v b/theories7/Lists/PolyList.v new file mode 100644 index 00000000..e69ecd10 --- /dev/null +++ b/theories7/Lists/PolyList.v @@ -0,0 +1,646 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: PolyList.v,v 1.2.2.1 2004/07/16 19:31:28 herbelin Exp $ i*) + +Require Le. + + +Section Lists. + +Variable A : Set. + +Set Implicit Arguments. + +Inductive list : Set := nil : list | cons : A -> list -> list. + +Infix "::" cons (at level 7, right associativity) : list_scope + V8only (at level 60, right associativity). + +Open Scope list_scope. + +(*************************) +(** Discrimination *) +(*************************) + +Lemma nil_cons : (a:A)(m:list)~(nil=(cons a m)). +Proof. + Intros; Discriminate. +Qed. + +(*************************) +(** 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 : list_scope + V8only RIGHTA 60 "++". + +Lemma app_nil_end : (l:list)l=(l^nil). +Proof. + NewInduction l ; Simpl ; Auto. + Rewrite <- IHl; Auto. +Qed. +Hints Resolve app_nil_end. + +Tactic Definition now_show c := Change c. +V7only [Tactic Definition NowShow := now_show.]. + +Lemma app_ass : (l,m,n : list)((l^m)^ n)=(l^(m^n)). +Proof. + Intros. NewInduction l ; Simpl ; Auto. + NowShow '(cons a (app (app l m) n))=(cons a (app l (app m n))). + Rewrite <- IHl; 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. + +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. + NewDestruct x;NewDestruct y;Simpl;Auto. + Intros H;Discriminate H. + Intros;Discriminate H. +Qed. + +Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)). +Proof. +Unfold not . + NewDestruct x;Simpl;Intros. + Discriminate H. + Discriminate H. +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. + NewDestruct x;NewDestruct 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. + NewInduction x as [|x l IHl];NewDestruct y;Simpl;Auto. + Intros a b H. + Injection H. + Auto. + Intros a0 b H. + Injection H;Intros. + Generalize (app_cons_not_nil H0) ;NewDestruct 1. + Intros a b H. + Injection H;Intros. + Cut nil=(l^(cons a nil));Auto. + Intro. + Generalize (app_cons_not_nil H2) ;NewDestruct 1. + Intros a0 b H. + Injection H;Intros. + NewDestruct (IHl l0 a0 b H0). + Split;Auto. + Rewrite <- H1;Rewrite <- H2;Reflexivity. +Qed. + +(*************************) +(** Head and tail *) +(*************************) + +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. + +(****************************************) +(** 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. + NowShow '(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. + NowShow '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. + NewInduction l as [|a0 l IHl]. + Right; Apply in_nil. + NewDestruct (H a0 a); Simpl; Auto. + NewDestruct IHl; Simpl; Auto. + Right; Unfold not; Intros [Hc1 | Hc2]; Auto. +Qed. + +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. + NowShow '(a0=a\/(In a y))\/(In a m). + Elim H0 ; Auto. + Intro H1. + NowShow '(a0=a\/(In a y))\/(In a 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. + NowShow '(In a m). + Elim H ; Auto ; Intro H0. + NowShow '(In a m). + Elim H0. (* subProof completed *) + Intros y H0 H1. + NowShow 'H=a\/(In a (app y m)). + Elim H1 ; Auto 4. + Intro H2. + NowShow 'H=a\/(In a (app y m)). + Elim H2 ; Auto. +Qed. +Hints Resolve in_or_app. + +(***************************) +(** Set 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. + NowShow '(In a0 m). + Elim H1. + NowShow 'a=a0->(In a0 m). + Elim H1 ; Auto ; Intro H2. + NowShow 'a=a0->(In a0 m). + Elim H2 ; Auto. (* solves subgoal *) + NowShow '(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. + NowShow '(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. *) +Proof. + Intros n l d; Generalize n; NewInduction l; Intro n0. + Right; Case n0; Trivial. + Case n0; Simpl. + Auto. + Intro n1; Elim (IHl n1); Auto. +Qed. + +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)). +Proof. + Simpl; Auto. +Qed. + +Fixpoint nth_error [l:list;n:nat] : (Exc A) := + Cases n l of + | O (cons x _) => (Value x) + | (S n) (cons _ l) => (nth_error l n) + | _ _ => Error + end. + +Definition nth_default : A -> list -> nat -> A := + [default,l,n]Cases (nth_error l n) of + | (Some x) => x + | None => default + end. + +Lemma nth_In : + (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l). + +Proof. +Unfold lt; NewInduction n as [|n hn]; Simpl. +NewDestruct l ; Simpl ; [ Inversion 2 | Auto]. +NewDestruct l as [|a l hl] ; Simpl. +Inversion 2. +Intros d ie ; Right ; Apply hn ; Auto with arith. +Qed. + +(********************************) +(** Decidable equality on lists *) +(********************************) + + +Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}. +Proof. + NewInduction x as [|a l IHl]; NewDestruct y as [|a0 l0]; Auto. + NewDestruct (H a a0) as [e|e]. + NewDestruct (IHl l0) as [e'|e']. + Left; Rewrite e; Rewrite e'; Trivial. + Right; Red; Intro. + Apply e'; Injection H0; Trivial. + Right; Red; Intro. + Apply e; Injection H0; Trivial. +Qed. + +(*************************) +(** Reverse *) +(*************************) + +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. + NewInduction x as [|a l IHl]. + NewDestruct y. + Simpl. + Auto. + + Simpl. + Apply app_nil_end;Auto. + + Intro y. + Simpl. + Rewrite (IHl y). + 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. + NewInduction l as [|a l IHl]. + Simpl;Auto. + + Simpl. + Rewrite (rev_unit (rev l) a). + Rewrite -> IHl;Auto. +Qed. + +(*********************************************) +(** Reverse Induction Principle on Lists *) +(*********************************************) + +Section Reverse_Induction. + +Unset Implicit Arguments. + +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. + NewInduction l; Auto. +Qed. +Set Implicit Arguments. + +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. + +Implicits nil [1]. + +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 + | (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)). +Proof. + NewInduction l as [|a l IHl]; Simpl; + [ Auto + | NewDestruct 1; + [ Left; Apply f_equal with f:=f; Assumption + | Auto] + ]. +Qed. + +Fixpoint flat_map [A,B:Set; f:A->(list B); l:(list A)] : (list B) := + Cases l of + nil => nil + | (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 + | (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)). +Proof. + NewInduction l; + [ Simpl; Auto + | Simpl; NewDestruct 1 as [H1|]; + [ Left; Rewrite H1; Trivial + | Right; Auto] + ]. +Qed. + +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')). +Proof. + NewInduction l; + [ Simpl; Tauto + | Simpl; Intros; Apply in_or_app; NewDestruct H; + [ Left; Rewrite H; Apply in_prod_aux; Assumption + | Right; Auto] + ]. +Qed. + +(** [(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 nil) + | (cons x t) => (flat_map [f:(list A*B)](map [y:B](cons (x,y) f) l') + (list_power t l')) + end. + +(************************************) +(** Left-to-right iterator on lists *) +(************************************) + +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. + +(************************************) +(** Right-to-left iterator on lists *) +(************************************) + +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). +Proof. +NewDestruct l as [|a l]. +Reflexivity. +Simpl. +Rewrite <- H0. +Generalize a0 a. +NewInduction l as [|a3 l IHl]; Simpl. +Trivial. +Intros. +Rewrite H. +Rewrite (H0 a2). +Rewrite <- (H a1). +Rewrite (H0 a1). +Rewrite IHl. +Reflexivity. +Qed. + +End Functions_on_lists. + +V7only [Implicits nil [].]. + +(** Exporting list notations *) + +V8Infix "::" cons (at level 60, right associativity) : list_scope. + +Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 60 "++". + +Open Scope list_scope. + +Delimits Scope list_scope with list. + +Bind Scope list_scope with list. diff --git a/theories7/Lists/PolyListSyntax.v b/theories7/Lists/PolyListSyntax.v new file mode 100644 index 00000000..15c57166 --- /dev/null +++ b/theories7/Lists/PolyListSyntax.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: PolyListSyntax.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + diff --git a/theories7/Lists/Streams.v b/theories7/Lists/Streams.v new file mode 100755 index 00000000..ccfc4895 --- /dev/null +++ b/theories7/Lists/Streams.v @@ -0,0 +1,170 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Streams.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +Set Implicit Arguments. + +(** Streams *) + +Section Streams. + +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. +Qed. +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. +Qed. + +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. +Qed. + +(** 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 := + 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. + +(*i +Inductive Exists : Stream -> Prop := + | Here : forall x:Stream, P x -> Exists x + | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x. +i*) + +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. +Variable A : Set. +Variable a : A. +CoFixpoint const : (Stream A) := (Cons a const). +End Constant_Stream. + +Unset Implicit Arguments. diff --git a/theories7/Lists/TheoryList.v b/theories7/Lists/TheoryList.v new file mode 100755 index 00000000..f7adda70 --- /dev/null +++ b/theories7/Lists/TheoryList.v @@ -0,0 +1,386 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: TheoryList.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Some programs and results about lists following CAML Manual *) + +Require Export PolyList. +Set Implicit Arguments. +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. +Qed. +Hints Resolve Isnil_nil. + +Lemma not_Isnil_cons : (a:A)(l:(list A))~(Isnil (cons a l)). +Unfold Isnil. +Intros; Discriminate. +Qed. + +Hints Resolve Isnil_nil not_Isnil_cons. + +Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}. +Intro l; Case l;Auto. +(* +Realizer (fun l => match l with + | nil => true + | _ => false + end). +*) +Qed. + +(************************) +(** The Uncons function *) +(************************) + +Lemma Uncons : (l:(list A)){a : A & { m: (list A) | (cons a m)=l}}+{Isnil l}. +Intro l; Case l. +Auto. +Intros a m; Intros; Left; Exists a; Exists m; Reflexivity. +(* +Realizer (fun l => match l with + | nil => error + | (cons a m) => value (a,m) + end). +*) +Qed. + +(********************************) +(** The head function *) +(********************************) + +Lemma Hd : (l:(list A)){a : A | (EX m:(list A) |(cons a m)=l)}+{Isnil l}. +Intro l; Case l. +Auto. +Intros a m; Intros; Left; Exists a; Exists m; Reflexivity. +(* +Realizer (fun l => match l with + | nil => error + | (cons a m) => value a + end). +*) +Qed. + +Lemma Tl : (l:(list A)){m:(list A)| (EX a:A |(cons a m)=l) + \/ ((Isnil l) /\ (Isnil m)) }. +Intro l; Case l. +Exists (nil A); Auto. +Intros a m; Intros; Exists m; Left; Exists a; Reflexivity. +(* +Realizer (fun l => match l with + | nil => nil + | (cons a m) => m + end). +*) +Qed. + +(****************************************) +(** Length of lists *) +(****************************************) + +(* length is defined in List *) +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}. +NewInduction l as [|a m lrec]. +Intro n; Exists n; Simpl; Auto. +Intro n; Elim (lrec (S n)); Simpl; Intros. +Exists x; Transitivity (S (plus n (length m))); Auto. +(* +Realizer Length_l. +*) +Qed. + +Lemma Length : (l:(list A)){m:nat|(length l)=m}. +Intro l. Apply (Length_l_pf l O). +(* +Realizer (fun l -> Length_l_pf l O). +*) +Qed. + +(*******************************) +(** 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. +Qed. + +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)}. +Intros a l. +NewInduction l. +Auto. +Elim (eqA_dec a a0). +Auto. +Simpl. Elim IHl; Auto. +(* +Realizer mem. +*) +Qed. + +(*********************************) +(** 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). +NewInduction 1; Auto. +Qed. +Hints Immediate fst_nth_nth. + +Lemma nth_lt_O : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(lt O n). +NewInduction 1; Auto. +Qed. + +Lemma nth_le_length : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(le n (length l)). +NewInduction 1; Simpl; Auto with arith. +Qed. + +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)}. +NewInduction l as [|a l IHl]. +Intro n; Case n; Simpl; Auto with arith. +Intro n; NewDestruct n as [|[|n1]]; Simpl; Auto. +Left; Exists a; Auto. +NewDestruct (IHl (S n1)) as [[b]|o]. +Left; Exists b; Auto. +Right; NewDestruct o. +Absurd (S n1)=O; Auto. +Auto with arith. +(* +Realizer Nth_func. +*) +Qed. + +Lemma Item : (l:(list A))(n:nat){a:A|(nth_spec l (S n) a)}+{(le (length l) n)}. +Intros l n; Case (Nth l (S n)); Intro. +Case s; Intro a; Left; Exists a; Auto. +Right; Case o; Intro. +Absurd (S n)=O; Auto. +Auto with arith. +Qed. + +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)}. +NewInduction l as [|b m irec]. +Auto. +Intro p. +NewDestruct (eqA_dec a b) as [e|e]. +Left; Exists p. +NewDestruct e; Elim minus_Sn_m; Trivial; Elim minus_n_n; Auto with arith. +NewDestruct (irec (S p)) as [[n H]|]. +Left; Exists 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. +Auto. +Qed. + +Lemma Index : (a:A)(l:(list A)) + {n:nat|(fst_nth_spec l n a)}+{(AllS [b:A]~a=b l)}. + +Intros a l; Case (Index_p a l (S O)); Auto. +Intros (n,P); Left; Exists n; Auto. +Rewrite (minus_n_O n); Trivial. +(* +Realizer (fun a l -> Index_p a l (S O)). +*) +Qed. + +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). +NewInduction 1; Simpl; Auto. +Qed. + +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). +Qed. + +Lemma InR_or_app : (l,m:(list A))((InR l)\/(InR m))->(InR (app l m)). +Intros l m [|]. +NewInduction 1; Simpl; Auto. +Intro. NewInduction l; Simpl; Auto. +Qed. + +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. +Qed. + +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)}. +NewInduction l as [|a m [[b H1 H2]|H]]; Auto. +Left; Exists b; Auto. +NewDestruct (RS_dec a). +Left; Exists a; Auto. +Auto. +(* +Realizer find. +*) +Qed. + +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)}. +NewInduction l as [|a m [[b H1]|H]]. +Auto. +Left; Exists b; NewDestruct H1 as [a' H2 H3]; Exists a'; Auto. +NewDestruct (TS_dec a) as [[c H1]|]. +Left; Exists c. +Exists a; Auto. +Auto. +(* +Realizer try_find. +*) +Qed. + +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. + +(* The specification seems too weak: it is enough to return b if the + list has at least an element (a,b); probably the intention is to have + the specification + + (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}. +*) + +Lemma Assoc : (a:A)(l:(list A*B))(B+{(AllS_assoc [a':A]~(a=a') l)}). +NewInduction l as [|[a' b] m assrec]. Auto. +NewDestruct (eqA_dec a a'). +Left; Exact b. +NewDestruct assrec as [b'|]. +Left; Exact b'. +Right; Auto. +(* +Realizer assoc. +*) +Qed. + +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. + |