summaryrefslogtreecommitdiff
path: root/theories/Lists
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /theories/Lists
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'theories/Lists')
-rw-r--r--theories/Lists/List.v27
-rw-r--r--theories/Lists/ListSet.v4
-rw-r--r--theories/Lists/ListTactics.v4
-rw-r--r--theories/Lists/SetoidList.v11
-rw-r--r--theories/Lists/StreamMemo.v2
-rw-r--r--theories/Lists/Streams.v4
-rw-r--r--theories/Lists/TheoryList.v423
-rwxr-xr-xtheories/Lists/intro.tex4
-rw-r--r--theories/Lists/vo.itarget1
9 files changed, 26 insertions, 454 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4c14008c..ecadddbc 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: List.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-Require Import Le Gt Minus Min Bool.
+Require Import Le Gt Minus Bool.
Set Implicit Arguments.
@@ -55,9 +53,16 @@ Section Lists.
End Lists.
-(* Keep these notations local to prevent conflicting notations *)
-Local Notation "[ ]" := nil : list_scope.
-Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
+(** Standard notations for lists.
+In a special module to avoid conflict. *)
+Module ListNotations.
+Notation " [ ] " := nil : list_scope.
+Notation " [ x ] " := (cons x nil) : list_scope.
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
+End ListNotations.
+
+Import ListNotations.
(** ** Facts about lists *)
@@ -119,7 +124,7 @@ Section Facts.
unfold not; intros a H; inversion_clear H.
Qed.
- Theorem in_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2.
+ Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2.
Proof.
induction l; simpl; destruct 1.
subst a; auto.
@@ -254,7 +259,7 @@ Section Facts.
Qed.
- (** Compatibility wtih other operations *)
+ (** Compatibility with other operations *)
Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'.
Proof.
@@ -1643,7 +1648,7 @@ Proof. exact Forall2_nil. Qed.
Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l',
Forall2 R (l1 ++ l2) l' ->
- exists l1', exists l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'.
+ exists l1' l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'.
Proof.
induction l1; intros.
exists [], l'; auto.
@@ -1654,7 +1659,7 @@ Qed.
Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l,
Forall2 R l (l1' ++ l2') ->
- exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
+ exists l1 l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
Proof.
induction l1'; intros.
exists [], l; auto.
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 56df3f9c..d67baf57 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ListSet.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** A Library for finite sets, implemented as lists *)
(** List is loaded, but not exported.
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 08669499..3343aa6f 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ListTactics.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import BinPos.
Require Import List.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index ec31f37d..97915055 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: SetoidList.v 12919 2010-04-10 16:30:44Z herbelin $ *)
-
Require Export List.
Require Export Sorting.
Require Export Setoid Basics Morphisms.
@@ -82,6 +80,10 @@ Qed.
Definition inclA l l' := forall x, InA x l -> InA x l'.
Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
+Lemma incl_nil l : inclA nil l.
+Proof. intro. intros. inversion H. Qed.
+Hint Resolve incl_nil : list.
+
(** lists with same elements modulo [eqA] at the same place *)
Inductive eqlistA : list A -> list A -> Prop :=
@@ -159,8 +161,7 @@ Qed.
Hint Resolve In_InA.
Lemma InA_split : forall l x, InA x l ->
- exists l1, exists y, exists l2,
- eqA x y /\ l = l1++y::l2.
+ exists l1 y l2, eqA x y /\ l = l1++y::l2.
Proof.
induction l; intros; inv.
exists (@nil A); exists a; exists l; auto.
@@ -747,7 +748,7 @@ rewrite filter_In in H; destruct H.
eapply SortA_InfA_InA; eauto.
Qed.
-Implicit Arguments eq [ [A] ].
+Arguments eq {A} x _.
Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index 1ab4fa9d..45490c62 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 02d17211..7a6f38fc 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Streams.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Set Implicit Arguments.
(** Streams *)
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
deleted file mode 100644
index 498a9dca..00000000
--- a/theories/Lists/TheoryList.v
+++ /dev/null
@@ -1,423 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: TheoryList.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(** Some programs and results about lists following CAML Manual *)
-
-Require Export List.
-Set Implicit Arguments.
-
-Local Notation "[ ]" := nil (at level 0).
-Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
-
-Section Lists.
-
-Variable A : Type.
-
-(**********************)
-(** The null function *)
-(**********************)
-
-Definition Isnil (l:list A) : Prop := nil = l.
-
-Lemma Isnil_nil : Isnil nil.
-Proof.
-red in |- *; auto.
-Qed.
-Hint Resolve Isnil_nil.
-
-Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l).
-Proof.
-unfold Isnil in |- *.
-intros; discriminate.
-Qed.
-
-Hint Resolve Isnil_nil not_Isnil_cons.
-
-Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}.
-Proof.
-intro l; case l; auto.
-(*
-Realizer (fun l => match l with
- | nil => true
- | _ => false
- end).
-*)
-Qed.
-
-(************************)
-(** The Uncons function *)
-(************************)
-
-Lemma Uncons :
- forall l:list A, {a : A & {m : list A | a :: m = l}} + {Isnil l}.
-Proof.
-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 :
- forall l:list A, {a : A | exists m : list A, a :: m = l} + {Isnil l}.
-Proof.
-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 :
- forall l:list A,
- {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}.
-Proof.
-intro l; case l.
-exists (nil (A:=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) (n:nat) : nat :=
- match l with
- | nil => n
- | _ :: m => Length_l m (S n)
- end.
-
-(* A tail recursive version *)
-Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}.
-Proof.
-induction l as [| a m lrec].
-intro n; exists n; simpl in |- *; auto.
-intro n; elim (lrec (S n)); simpl in |- *; intros.
-exists x; transitivity (S (n + length m)); auto.
-(*
-Realizer Length_l.
-*)
-Qed.
-
-Lemma Length : forall l:list A, {m : nat | length l = m}.
-Proof.
-intro l. apply (Length_l_pf l 0).
-(*
-Realizer (fun l -> Length_l_pf l O).
-*)
-Qed.
-
-(*******************************)
-(** Members of lists *)
-(*******************************)
-Inductive In_spec (a:A) : list A -> Prop :=
- | in_hd : forall l:list A, In_spec a (a :: l)
- | in_tl : forall (l:list A) (b:A), In a l -> In_spec a (b :: l).
-Hint Resolve in_hd in_tl.
-Hint Unfold In.
-Hint Resolve in_cons.
-
-Theorem In_In_spec : forall (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.
-
-Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
-
-Fixpoint mem (a:A) (l:list A) : bool :=
- match l with
- | nil => false
- | b :: m => if eqA_dec a b then true else mem a m
- end.
-
-Hint Unfold In.
-Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}.
-Proof.
-induction l.
-auto.
-elim (eqA_dec a a0).
-auto.
-simpl in |- *. elim IHl; auto.
-(*
-Realizer mem.
-*)
-Qed.
-
-(*********************************)
-(** Index of elements *)
-(*********************************)
-
-Require Import Le.
-Require Import Lt.
-
-Inductive nth_spec : list A -> nat -> A -> Prop :=
- | nth_spec_O : forall (a:A) (l:list A), nth_spec (a :: l) 1 a
- | nth_spec_S :
- forall (n:nat) (a b:A) (l:list A),
- nth_spec l n a -> nth_spec (b :: l) (S n) a.
-Hint Resolve nth_spec_O nth_spec_S.
-
-Inductive fst_nth_spec : list A -> nat -> A -> Prop :=
- | fst_nth_O : forall (a:A) (l:list A), fst_nth_spec (a :: l) 1 a
- | fst_nth_S :
- forall (n:nat) (a b:A) (l:list A),
- a <> b -> fst_nth_spec l n a -> fst_nth_spec (b :: l) (S n) a.
-Hint Resolve fst_nth_O fst_nth_S.
-
-Lemma fst_nth_nth :
- forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a.
-Proof.
-induction 1; auto.
-Qed.
-Hint Immediate fst_nth_nth.
-
-Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n.
-Proof.
-induction 1; auto.
-Qed.
-
-Lemma nth_le_length :
- forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l.
-Proof.
-induction 1; simpl in |- *; auto with arith.
-Qed.
-
-Fixpoint Nth_func (l:list A) (n:nat) : Exc A :=
- match l, n with
- | a :: _, S O => value a
- | _ :: l', S (S p) => Nth_func l' (S p)
- | _, _ => error
- end.
-
-Lemma Nth :
- forall (l:list A) (n:nat),
- {a : A | nth_spec l n a} + {n = 0 \/ length l < n}.
-Proof.
-induction l as [| a l IHl].
-intro n; case n; simpl in |- *; auto with arith.
-intro n; destruct n as [| [| n1]]; simpl in |- *; auto.
-left; exists a; auto.
-destruct (IHl (S n1)) as [[b]| o].
-left; exists b; auto.
-right; destruct o.
-absurd (S n1 = 0); auto.
-auto with arith.
-(*
-Realizer Nth_func.
-*)
-Qed.
-
-Lemma Item :
- forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}.
-Proof.
-intros l n; case (Nth l (S n)); intro.
-case s; intro a; left; exists a; auto.
-right; case o; intro.
-absurd (S n = 0); auto.
-auto with arith.
-Qed.
-
-Require Import Minus.
-Require Import DecBool.
-
-Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat :=
- match l with
- | nil => fun p => error
- | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p))
- end.
-
-Lemma Index_p :
- forall (a:A) (l:list A) (p:nat),
- {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}.
-Proof.
-induction l as [| b m irec].
-auto.
-intro p.
-destruct (eqA_dec a b) as [e| e].
-left; exists p.
-destruct e; elim minus_Sn_m; trivial; elim minus_n_n; auto with arith.
-destruct (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 :
- forall (a:A) (l:list A),
- {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}.
-
-Proof.
-intros a l; case (Index_p a l 1); 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.
-Variables R P : A -> Prop.
-
-Inductive InR : list A -> Prop :=
- | inR_hd : forall (a:A) (l:list A), R a -> InR (a :: l)
- | inR_tl : forall (a:A) (l:list A), InR l -> InR (a :: l).
-Hint Resolve inR_hd inR_tl.
-
-Definition InR_inv (l:list A) :=
- match l with
- | nil => False
- | b :: m => R b \/ InR m
- end.
-
-Lemma InR_INV : forall l:list A, InR l -> InR_inv l.
-Proof.
-induction 1; simpl in |- *; auto.
-Qed.
-
-Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l.
-Proof.
-intros a l H; exact (InR_INV H).
-Qed.
-
-Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m).
-Proof.
-intros l m [| ].
-induction 1; simpl in |- *; auto.
-intro. induction l; simpl in |- *; auto.
-Qed.
-
-Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m.
-Proof.
-intros l m; elim l; simpl in |- *; auto.
-intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto.
-intros; elim Hrec; auto.
-Qed.
-
-Hypothesis RS_dec : forall a:A, {R a} + {P a}.
-
-Fixpoint find (l:list A) : Exc A :=
- match l with
- | nil => error
- | a :: m => ifdec (RS_dec a) (value a) (find m)
- end.
-
-Lemma Find : forall l:list A, {a : A | In a l & R a} + {AllS P l}.
-Proof.
-induction l as [| a m [[b H1 H2]| H]]; auto.
-left; exists b; auto.
-destruct (RS_dec a).
-left; exists a; auto.
-auto.
-(*
-Realizer find.
-*)
-Qed.
-
-Variable B : Type.
-Variable T : A -> B -> Prop.
-
-Variable TS_dec : forall a:A, {c : B | T a c} + {P a}.
-
-Fixpoint try_find (l:list A) : Exc B :=
- match l with
- | nil => error
- | a :: l1 =>
- match TS_dec a with
- | inleft (exist c _) => value c
- | inright _ => try_find l1
- end
- end.
-
-Lemma Try_find :
- forall l:list A, {c : B | exists2 a : A, In a l & T a c} + {AllS P l}.
-Proof.
-induction l as [| a m [[b H1]| H]].
-auto.
-left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto.
-destruct (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 : Type.
-Fixpoint assoc (a:A) (l:list (A * B)) :
- Exc B :=
- match l with
- | nil => error
- | (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
- | allS_assoc_cons :
- forall (a:A) (b:B) (l:list (A * B)),
- P a -> AllS_assoc P l -> AllS_assoc P ((a, b) :: l).
-
-Hint 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 :
- forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}.
-Proof.
-induction l as [| [a' b] m assrec]. auto.
-destruct (eqA_dec a a').
-left; exact b.
-destruct assrec as [b'| ].
-left; exact b'.
-right; auto.
-(*
-Realizer assoc.
-*)
-Qed.
-
-End Assoc_sec.
-
-End Lists.
-
-Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons : datatypes.
-Hint Immediate fst_nth_nth: datatypes.
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index 0051e2c2..e849967c 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -13,10 +13,6 @@ This library includes the following files:
\item {\tt ListSet.v} contains definitions and properties of finite
sets, implemented as lists.
-\item {\tt TheoryList.v} contains complementary results on lists. Here
- a more theoretic point of view is assumed : one extracts functions
- from propositions, rather than defining functions and then prove them.
-
\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
coinductive type. Basic facts are stated and proved. The streams are
also polymorphic.
diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget
index d2a31367..adcfba49 100644
--- a/theories/Lists/vo.itarget
+++ b/theories/Lists/vo.itarget
@@ -4,4 +4,3 @@ List.vo
SetoidList.vo
StreamMemo.vo
Streams.vo
-TheoryList.vo