diff options
Diffstat (limited to 'theories/Lists')
| -rwxr-xr-x | theories/Lists/List.v | 655 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 398 | ||||
| -rwxr-xr-x | theories/Lists/MonoList.v | 269 | ||||
| -rwxr-xr-x | theories/Lists/Streams.v | 177 | ||||
| -rwxr-xr-x | theories/Lists/TheoryList.v | 403 | ||||
| -rwxr-xr-x | theories/Lists/intro.tex | 24 |
6 files changed, 1926 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v new file mode 100755 index 00000000..c3f65d67 --- /dev/null +++ b/theories/Lists/List.v @@ -0,0 +1,655 @@ +(************************************************************************) +(* 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.9.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) + +Require Import Le. + + +Section Lists. + +Variable A : Set. + +Set Implicit Arguments. + +Inductive list : Set := + | nil : list + | cons : A -> list -> list. + +Infix "::" := cons (at level 60, right associativity) : list_scope. + +Open Scope list_scope. + +(*************************) +(** Discrimination *) +(*************************) + +Lemma nil_cons : forall (a:A) (m:list), nil <> a :: m. +Proof. + intros; discriminate. +Qed. + +(*************************) +(** Concatenation *) +(*************************) + +Fixpoint app (l m:list) {struct l} : list := + match l with + | nil => m + | a :: l1 => a :: app l1 m + end. + +Infix "++" := app (right associativity, at level 60) : list_scope. + +Lemma app_nil_end : forall l:list, l = l ++ nil. +Proof. + induction l; simpl in |- *; auto. + rewrite <- IHl; auto. +Qed. +Hint Resolve app_nil_end. + +Ltac now_show c := change c in |- *. + +Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n. +Proof. + intros. induction l; simpl in |- *; auto. + now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n). + rewrite <- IHl; auto. +Qed. +Hint Resolve app_ass. + +Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n. +Proof. + auto. +Qed. +Hint Resolve ass_app. + +Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y. +Proof. + auto. +Qed. + +Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil. +Proof. + destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl in |- *; auto. + intros H; discriminate H. + intros; discriminate H. +Qed. + +Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y. +Proof. +unfold not in |- *. + destruct x as [| a l]; simpl in |- *; intros. + discriminate H. + discriminate H. +Qed. + +Lemma app_eq_unit : + forall (x y:list) (a:A), + x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil. + +Proof. + destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl in |- *. + 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 ++ a0 :: l0); auto. + intro. + generalize (app_cons_not_nil _ _ _ H1); intro. + elim H2. +Qed. + +Lemma app_inj_tail : + forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b. +Proof. + induction x as [| x l IHl]; + [ destruct y as [| a l] | destruct y as [| a l0] ]; + simpl in |- *; auto. + intros a b H. + injection H. + auto. + intros a0 b H. + injection H; intros. + generalize (app_cons_not_nil _ _ _ H0); destruct 1. + intros a b H. + injection H; intros. + cut (nil = l ++ a :: nil); auto. + intro. + generalize (app_cons_not_nil _ _ _ H2); destruct 1. + intros a0 b H. + injection H; intros. + destruct (IHl l0 a0 b H0). + split; auto. + rewrite <- H1; rewrite <- H2; reflexivity. +Qed. + +(*************************) +(** Head and tail *) +(*************************) + +Definition head (l:list) := + match l with + | nil => error + | x :: _ => value x + end. + +Definition tail (l:list) : list := + match l with + | nil => nil + | a :: m => m + end. + +(****************************************) +(** Length of lists *) +(****************************************) + +Fixpoint length (l:list) : nat := + match l with + | nil => 0 + | _ :: m => S (length m) + end. + +(******************************) +(** Length order of lists *) +(******************************) + +Section length_order. +Definition lel (l m:list) := length l <= length m. + +Variables a b : A. +Variables l m n : list. + +Lemma lel_refl : lel l l. +Proof. + unfold lel in |- *; auto with arith. +Qed. + +Lemma lel_trans : lel l m -> lel m n -> lel l n. +Proof. + unfold lel in |- *; intros. + now_show (length l <= length n). + apply le_trans with (length m); auto with arith. +Qed. + +Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). +Proof. + unfold lel in |- *; simpl in |- *; auto with arith. +Qed. + +Lemma lel_cons : lel l m -> lel l (b :: m). +Proof. + unfold lel in |- *; simpl in |- *; auto with arith. +Qed. + +Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. +Proof. + unfold lel in |- *; simpl in |- *; auto with arith. +Qed. + +Lemma lel_nil : forall l':list, lel l' nil -> nil = l'. +Proof. + intro l'; elim l'; auto with arith. + intros a' y H H0. + now_show (nil = a' :: y). + absurd (S (length y) <= 0); auto with arith. +Qed. +End length_order. + +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons. + +(*********************************) +(** The [In] predicate *) +(*********************************) + +Fixpoint In (a:A) (l:list) {struct l} : Prop := + match l with + | nil => False + | b :: m => b = a \/ In a m + end. + +Lemma in_eq : forall (a:A) (l:list), In a (a :: l). +Proof. + simpl in |- *; auto. +Qed. +Hint Resolve in_eq. + +Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (a :: l). +Proof. + simpl in |- *; auto. +Qed. +Hint Resolve in_cons. + +Lemma in_nil : forall a:A, ~ In a nil. +Proof. + unfold not in |- *; intros a H; inversion_clear H. +Qed. + + +Lemma in_inv : forall (a b:A) (l:list), In b (a :: l) -> a = b \/ In b l. +Proof. + intros a b l H; inversion_clear H; auto. +Qed. + +Lemma In_dec : + (forall x y:A, {x = y} + {x <> y}) -> + forall (a:A) (l:list), {In a l} + {~ In a l}. + +Proof. + induction l as [| a0 l IHl]. + right; apply in_nil. + destruct (H a0 a); simpl in |- *; auto. + destruct IHl; simpl in |- *; auto. + right; unfold not in |- *; intros [Hc1| Hc2]; auto. +Qed. + +Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m. +Proof. + intros l m a. + elim l; simpl in |- *; auto. + intros a0 y H H0. + now_show ((a0 = a \/ In a y) \/ In a m). + elim H0; auto. + intro H1. + now_show ((a0 = a \/ In a y) \/ In a m). + elim (H H1); auto. +Qed. +Hint Immediate in_app_or. + +Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (l ++ m). +Proof. + intros l m a. + elim l; simpl in |- *; intro H. + now_show (In a m). + elim H; auto; intro H0. + now_show (In a m). + elim H0. (* subProof completed *) + intros y H0 H1. + now_show (H = a \/ In a (y ++ m)). + elim H1; auto 4. + intro H2. + now_show (H = a \/ In a (y ++ m)). + elim H2; auto. +Qed. +Hint Resolve in_or_app. + +(***************************) +(** Set inclusion on list *) +(***************************) + +Definition incl (l m:list) := forall a:A, In a l -> In a m. +Hint Unfold incl. + +Lemma incl_refl : forall l:list, incl l l. +Proof. + auto. +Qed. +Hint Resolve incl_refl. + +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (a :: m). +Proof. + auto. +Qed. +Hint Immediate incl_tl. + +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. +Proof. + auto. +Qed. + +Lemma incl_appl : forall l m n:list, incl l n -> incl l (n ++ m). +Proof. + auto. +Qed. +Hint Immediate incl_appl. + +Lemma incl_appr : forall l m n:list, incl l n -> incl l (m ++ n). +Proof. + auto. +Qed. +Hint Immediate incl_appr. + +Lemma incl_cons : + forall (a:A) (l m:list), In a m -> incl l m -> incl (a :: l) m. +Proof. + unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. + now_show (In a0 m). + elim H1. + now_show (a = a0 -> In a0 m). + elim H1; auto; intro H2. + now_show (a = a0 -> In a0 m). + elim H2; auto. (* solves subgoal *) + now_show (In a0 l -> In a0 m). + auto. +Qed. +Hint Resolve incl_cons. + +Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (l ++ m) n. +Proof. + unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. + now_show (In a n). + elim (in_app_or _ _ _ H1); auto. +Qed. +Hint Resolve incl_app. + +(**************************) +(** Nth element of a list *) +(**************************) + +Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A := + match n, l with + | O, x :: l' => x + | O, other => default + | S m, nil => default + | S m, x :: t => nth m t default + end. + +Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool := + match n, l with + | O, x :: l' => true + | O, other => false + | S m, nil => false + | S m, x :: t => nth_ok m t default + end. + +Lemma nth_in_or_default : + forall (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; induction l; intro n0. + right; case n0; trivial. + case n0; simpl in |- *. + auto. + intro n1; elim (IHl n1); auto. +Qed. + +Lemma nth_S_cons : + forall (n:nat) (l:list) (d a:A), + In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). +Proof. + simpl in |- *; auto. +Qed. + +Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A := + match n, l with + | O, x :: _ => value x + | S n, _ :: l => nth_error l n + | _, _ => error + end. + +Definition nth_default (default:A) (l:list) (n:nat) : A := + match nth_error l n with + | Some x => x + | None => default + end. + +Lemma nth_In : + forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l. + +Proof. +unfold lt in |- *; induction n as [| n hn]; simpl in |- *. +destruct l; simpl in |- *; [ inversion 2 | auto ]. +destruct l as [| a l hl]; simpl in |- *. +inversion 2. +intros d ie; right; apply hn; auto with arith. +Qed. + +(********************************) +(** Decidable equality on lists *) +(********************************) + + +Lemma list_eq_dec : + (forall x y:A, {x = y} + {x <> y}) -> forall x y:list, {x = y} + {x <> y}. +Proof. + induction x as [| a l IHl]; destruct y as [| a0 l0]; auto. + destruct (H a a0) as [e| e]. + destruct (IHl l0) as [e'| e']. + left; rewrite e; rewrite e'; trivial. + right; red in |- *; intro. + apply e'; injection H0; trivial. + right; red in |- *; intro. + apply e; injection H0; trivial. +Qed. + +(*************************) +(** Reverse *) +(*************************) + +Fixpoint rev (l:list) : list := + match l with + | nil => nil + | x :: l' => rev l' ++ x :: nil + end. + +Lemma distr_rev : forall x y:list, rev (x ++ y) = rev y ++ rev x. +Proof. + induction x as [| a l IHl]. + destruct y as [| a l]. + simpl in |- *. + auto. + + simpl in |- *. + apply app_nil_end; auto. + + intro y. + simpl in |- *. + rewrite (IHl y). + apply (app_ass (rev y) (rev l) (a :: nil)). +Qed. + +Remark rev_unit : forall (l:list) (a:A), rev (l ++ a :: nil) = a :: rev l. +Proof. + intros. + apply (distr_rev l (a :: nil)); simpl in |- *; auto. +Qed. + +Lemma rev_involutive : forall l:list, rev (rev l) = l. +Proof. + induction l as [| a l IHl]. + simpl in |- *; auto. + + simpl in |- *. + 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 : + forall P:list -> Prop, + P nil -> + (forall (a:A) (l:list), P (rev l) -> P (rev (a :: l))) -> + forall l:list, P (rev l). +Proof. + induction l; auto. +Qed. +Set Implicit Arguments. + +Lemma rev_ind : + forall P:list -> Prop, + P nil -> + (forall (x:A) (l:list), P l -> P (l ++ x :: nil)) -> forall l:list, P l. +Proof. + intros. + generalize (rev_involutive l). + intros E; rewrite <- E. + apply (rev_list_ind P). + auto. + + simpl in |- *. + intros. + apply (H0 a (rev l0)). + auto. +Qed. + +End Reverse_Induction. + +End Lists. + +Implicit Arguments nil [A]. + +Hint Resolve nil_cons app_nil_end ass_app app_ass: datatypes v62. +Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62. +Hint Immediate app_eq_nil: datatypes v62. +Hint Resolve app_eq_unit app_inj_tail: datatypes v62. +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: + datatypes v62. +Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. +Hint 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 := + match l with + | nil => nil + | cons a t => cons (f a) (map t) + end. +End Map. + +Lemma in_map : + forall (A B:Set) (f:A -> B) (l:list A) (x:A), In x l -> In (f x) (map f l). +Proof. + induction l as [| a l IHl]; simpl in |- *; + [ auto + | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ]. +Qed. + +Fixpoint flat_map (A B:Set) (f:A -> list B) (l:list A) {struct l} : + list B := + match l with + | nil => nil + | cons x t => app (f x) (flat_map f t) + end. + +Fixpoint list_prod (A B:Set) (l:list A) (l':list B) {struct l} : + list (A * B) := + match l with + | nil => nil + | cons x t => app (map (fun y:B => (x, y)) l') (list_prod t l') + end. + +Lemma in_prod_aux : + forall (A B:Set) (x:A) (y:B) (l:list B), + In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). +Proof. + induction l; + [ simpl in |- *; auto + | simpl in |- *; destruct 1 as [H1| ]; + [ left; rewrite H1; trivial | right; auto ] ]. +Qed. + +Lemma in_prod : + forall (A 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. + induction l; + [ simpl in |- *; tauto + | simpl in |- *; intros; apply in_or_app; destruct 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) (l':list B) {struct l} : + list (list (A * B)) := + match l with + | nil => cons nil nil + | cons x t => + flat_map (fun f:list (A * B) => map (fun 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) (a0:A) {struct l} : A := + match l with + | 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 := + match l with + | nil => a0 + | cons b t => f b (fold_right t) + end. +End Fold_Right_Recursor. + +Theorem fold_symmetric : + forall (A:Set) (f:A -> A -> A), + (forall x y z:A, f x (f y z) = f (f x y) z) -> + (forall x y:A, f x y = f y x) -> + forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l. +Proof. +destruct l as [| a l]. +reflexivity. +simpl in |- *. +rewrite <- H0. +generalize a0 a. +induction l as [| a3 l IHl]; simpl in |- *. +trivial. +intros. +rewrite H. +rewrite (H0 a2). +rewrite <- (H a1). +rewrite (H0 a1). +rewrite IHl. +reflexivity. +Qed. + +End Functions_on_lists. + + +(** Exporting list notations *) + +Infix "::" := cons (at level 60, right associativity) : list_scope. + +Infix "++" := app (right associativity, at level 60) : list_scope. + +Open Scope list_scope. + +(** Declare Scope list_scope with key list *) +Delimit Scope list_scope with list. + +Bind Scope list_scope with list. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v new file mode 100644 index 00000000..d5ecad9c --- /dev/null +++ b/theories/Lists/ListSet.v @@ -0,0 +1,398 @@ +(************************************************************************) +(* 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.13.2.1 2004/07/16 19:31:05 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 Import List. + +Set Implicit Arguments. + +Section first_definitions. + + Variable A : Set. + Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}. + + Definition set := list A. + + Definition empty_set : set := nil. + + Fixpoint set_add (a:A) (x:set) {struct x} : set := + match x with + | nil => a :: nil + | a1 :: x1 => + match Aeq_dec a a1 with + | left _ => a1 :: x1 + | right _ => a1 :: set_add a x1 + end + end. + + + Fixpoint set_mem (a:A) (x:set) {struct x} : bool := + match x with + | nil => false + | a1 :: x1 => + match Aeq_dec a a1 with + | 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) {struct x} : set := + match x with + | nil => empty_set + | a1 :: x1 => + match Aeq_dec a a1 with + | left _ => x1 + | right _ => a1 :: set_remove a x1 + end + end. + + Fixpoint set_inter (x:set) : set -> set := + match x with + | nil => fun y => nil + | a1 :: x1 => + fun y => + if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y + end. + + Fixpoint set_union (x y:set) {struct y} : set := + match y with + | nil => x + | 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 y:set) {struct x} : set := + match x with + | nil => nil + | 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 (A:=A). + + Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}. + + Proof. + unfold set_In in |- *. + (*** Realizer set_mem. Program_all. ***) + simple induction x. + auto. + intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq. + rewrite eq; simpl in |- *; auto with datatypes. + elim Ha0. + auto with datatypes. + right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2]; + auto with datatypes. + Qed. + + Lemma set_mem_ind : + forall (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. + simple induction x; simpl in |- *; intros. + assumption. + elim (Aeq_dec a a0); auto with datatypes. + Qed. + + Lemma set_mem_ind2 : + forall (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. + simple induction x; simpl in |- *; intros. + apply H0; red in |- *; trivial. + case (Aeq_dec a a0); auto with datatypes. + intro; apply H; intros; auto. + apply H1; red in |- *; intro. + case H3; auto. + Qed. + + + Lemma set_mem_correct1 : + forall (a:A) (x:set), set_mem a x = true -> set_In a x. + Proof. + simple induction x; simpl in |- *. + discriminate. + intros a0 l; elim (Aeq_dec a a0); auto with datatypes. + Qed. + + Lemma set_mem_correct2 : + forall (a:A) (x:set), set_In a x -> set_mem a x = true. + Proof. + simple induction x; simpl in |- *. + 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 : + forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x. + Proof. + simple induction x; simpl in |- *. + tauto. + intros a0 l; elim (Aeq_dec a a0). + intros; discriminate H0. + unfold not in |- *; intros; elim H1; auto with datatypes. + Qed. + + Lemma set_mem_complete2 : + forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false. + Proof. + simple induction x; simpl in |- *. + tauto. + intros a0 l; elim (Aeq_dec a a0). + intros; elim H0; auto with datatypes. + tauto. + Qed. + + Lemma set_add_intro1 : + forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x). + + Proof. + unfold set_In in |- *; simple induction x; simpl in |- *. + 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 : + forall (a b:A) (x:set), a = b -> set_In a (set_add b x). + + Proof. + unfold set_In in |- *; simple induction x; simpl in |- *. + auto with datatypes. + intros a0 l H Hab. + elim (Aeq_dec b a0); + [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *; + auto with datatypes + | auto with datatypes ]. + Qed. + + Hint Resolve set_add_intro1 set_add_intro2. + + Lemma set_add_intro : + forall (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 : + forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x. + + Proof. + unfold set_In in |- *. + simple induction x. + simpl in |- *; intros [H1| H2]; auto with datatypes. + simpl in |- *; do 3 intro. + elim (Aeq_dec b a0). + simpl in |- *; tauto. + simpl in |- *; intros; elim H0. + trivial with datatypes. + tauto. + tauto. + Qed. + + Lemma set_add_elim2 : + forall (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. + + Hint Resolve set_add_intro set_add_elim set_add_elim2. + + Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set. + Proof. + simple induction x; simpl in |- *. + discriminate. + intros; elim (Aeq_dec a a0); intros; discriminate. + Qed. + + + Lemma set_union_intro1 : + forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). + Proof. + simple induction y; simpl in |- *; auto with datatypes. + Qed. + + Lemma set_union_intro2 : + forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y). + Proof. + simple induction y; simpl in |- *. + tauto. + intros; elim H0; auto with datatypes. + Qed. + + Hint Resolve set_union_intro2 set_union_intro1. + + Lemma set_union_intro : + forall (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 : + forall (a:A) (x y:set), + set_In a (set_union x y) -> set_In a x \/ set_In a y. + Proof. + simple induction y; simpl in |- *. + auto with datatypes. + intros. + generalize (set_add_elim _ _ _ H0). + intros [H1| H1]. + auto with datatypes. + tauto. + Qed. + + Lemma set_union_emptyL : + forall (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 || contradiction. + Qed. + + + Lemma set_union_emptyR : + forall (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 || contradiction. + Qed. + + + Lemma set_inter_intro : + forall (a:A) (x y:set), + set_In a x -> set_In a y -> set_In a (set_inter x y). + Proof. + simple induction x. + auto with datatypes. + simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy. + simpl in |- *; rewrite Ha0a. + generalize (set_mem_correct1 a y). + generalize (set_mem_complete1 a y). + elim (set_mem a y); simpl in |- *; 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 : + forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x. + Proof. + simple induction x. + auto with datatypes. + simpl in |- *; intros a0 l Hrec y. + generalize (set_mem_correct1 a0 y). + elim (set_mem a0 y); simpl in |- *; intros. + elim H0; eauto with datatypes. + eauto with datatypes. + Qed. + + Lemma set_inter_elim2 : + forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y. + Proof. + simple induction x. + simpl in |- *; tauto. + simpl in |- *; intros a0 l Hrec y. + generalize (set_mem_correct1 a0 y). + elim (set_mem a0 y); simpl in |- *; intros. + elim H0; + [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ]. + eauto with datatypes. + Qed. + + Hint Resolve set_inter_elim1 set_inter_elim2. + + Lemma set_inter_elim : + forall (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 : + forall (a:A) (x y:set), + set_In a x -> ~ set_In a y -> set_In a (set_diff x y). + Proof. + simple induction x. + simpl in |- *; tauto. + simpl in |- *; 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 : + forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x. + Proof. + simple induction x. + simpl in |- *; tauto. + simpl in |- *; 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 : + forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y. + intros a x y; elim x; simpl in |- *. + 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 : forall (a:A) (x:set), ~ set_In a (set_diff x x). + red in |- *; intros a x H. + apply (set_diff_elim2 _ _ _ H). + apply (set_diff_elim1 _ _ _ H). + Qed. + +Hint 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 (A:=A) (B:=B). + + (** [B^A], set of applications from [A] to [B] *) + Definition set_power : set A -> set B -> set (set (A * B)) := + list_power (A:=A) (B:=B). + + Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B). + + Definition set_fold_left : (B -> A -> B) -> set A -> B -> B := + fold_left (A:=B) (B:=A). + + Definition set_fold_right (f:A -> B -> B) (x:set A) + (b:B) : B := fold_right f b x. + + +End other_definitions. + +Unset Implicit Arguments.
\ No newline at end of file diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v new file mode 100755 index 00000000..d639a39d --- /dev/null +++ b/theories/Lists/MonoList.v @@ -0,0 +1,269 @@ +(************************************************************************) +(* 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.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) + +(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) + +Require Import Le. + +Parameter List_Dom : Set. +Definition A := List_Dom. + +Inductive list : Set := + | nil : list + | cons : A -> list -> list. + +Fixpoint app (l m:list) {struct l} : list := + match l return list with + | nil => m + | cons a l1 => cons a (app l1 m) + end. + + +Lemma app_nil_end : forall l:list, l = app l nil. +Proof. + intro l; elim l; simpl in |- *; auto. + simple induction 1; auto. +Qed. +Hint Resolve app_nil_end: list v62. + +Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n). +Proof. + intros l m n; elim l; simpl in |- *; auto with list. + simple induction 1; auto with list. +Qed. +Hint Resolve app_ass: list v62. + +Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n. +Proof. + auto with list. +Qed. +Hint Resolve ass_app: list v62. + +Definition tail (l:list) : list := + match l return list with + | cons _ m => m + | _ => nil + end. + + +Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m. + intros; discriminate. +Qed. + +(****************************************) +(* Length of lists *) +(****************************************) + +Fixpoint length (l:list) : nat := + match l return nat with + | cons _ m => S (length m) + | _ => 0 + end. + +(******************************) +(* Length order of lists *) +(******************************) + +Section length_order. +Definition lel (l m:list) := length l <= length m. + +Hint Unfold lel: list. + +Variables a b : A. +Variables l m n : list. + +Lemma lel_refl : lel l l. +Proof. + unfold lel in |- *; auto with list. +Qed. + +Lemma lel_trans : lel l m -> lel m n -> lel l n. +Proof. + unfold lel in |- *; 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 in |- *; simpl in |- *; auto with list arith. +Qed. + +Lemma lel_cons : lel l m -> lel l (cons b m). +Proof. + unfold lel in |- *; simpl in |- *; auto with list arith. +Qed. + +Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m. +Proof. + unfold lel in |- *; simpl in |- *; auto with list arith. +Qed. + +Lemma lel_nil : forall 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 (S (length y) <= 0); auto with list arith. +Qed. +End length_order. + +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list + v62. + +Fixpoint In (a:A) (l:list) {struct l} : Prop := + match l with + | nil => False + | cons b m => b = a \/ In a m + end. + +Lemma in_eq : forall (a:A) (l:list), In a (cons a l). +Proof. + simpl in |- *; auto with list. +Qed. +Hint Resolve in_eq: list v62. + +Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l). +Proof. + simpl in |- *; auto with list. +Qed. +Hint Resolve in_cons: list v62. + +Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m. +Proof. + intros l m a. + elim l; simpl in |- *; 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. +Hint Immediate in_app_or: list v62. + +Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m). +Proof. + intros l m a. + elim l; simpl in |- *; 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. +Hint Resolve in_or_app: list v62. + +Definition incl (l m:list) := forall a:A, In a l -> In a m. + +Hint Unfold incl: list v62. + +Lemma incl_refl : forall l:list, incl l l. +Proof. + auto with list. +Qed. +Hint Resolve incl_refl: list v62. + +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m). +Proof. + auto with list. +Qed. +Hint Immediate incl_tl: list v62. + +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. +Proof. + auto with list. +Qed. + +Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m). +Proof. + auto with list. +Qed. +Hint Immediate incl_appl: list v62. + +Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n). +Proof. + auto with list. +Qed. +Hint Immediate incl_appr: list v62. + +Lemma incl_cons : + forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m. +Proof. + unfold incl in |- *; simpl in |- *; 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. +Hint Resolve incl_cons: list v62. + +Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n. +Proof. + unfold incl in |- *; simpl in |- *; 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. +Hint Resolve incl_app: list v62.
\ No newline at end of file diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v new file mode 100755 index 00000000..3c433ba2 --- /dev/null +++ b/theories/Lists/Streams.v @@ -0,0 +1,177 @@ +(************************************************************************) +(* 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.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) + +Set Implicit Arguments. + +(** Streams *) + +Section Streams. + +Variable A : Set. + +CoInductive Stream : Set := + Cons : A -> Stream -> Stream. + + +Definition hd (x:Stream) := match x with + | Cons a _ => a + end. + +Definition tl (x:Stream) := match x with + | Cons _ s => s + end. + + +Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream := + match n with + | O => s + | S m => Str_nth_tl m (tl s) + end. + +Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s). + + +Lemma unfold_Stream : + forall x:Stream, x = match x with + | Cons a s => Cons a s + end. +Proof. + intro x. + case x. + trivial. +Qed. + +Lemma tl_nth_tl : + forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s). +Proof. + simple induction n; simpl in |- *; auto. +Qed. +Hint Resolve tl_nth_tl: datatypes v62. + +Lemma Str_nth_tl_plus : + forall (n m:nat) (s:Stream), + Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s. +simple induction n; simpl in |- *; intros; auto with datatypes. +rewrite <- H. +rewrite tl_nth_tl; trivial with datatypes. +Qed. + +Lemma Str_nth_plus : + forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s. +intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus; + trivial with datatypes. +Qed. + +(** Extensional Equality between two streams *) + +CoInductive EqSt : Stream -> Stream -> Prop := + eqst : + forall s1 s2:Stream, + hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. + +(** A coinduction principle *) + +Ltac coinduction proof := + cofix proof; intros; constructor; + [ clear proof | try (apply proof; clear proof) ]. + + +(** Extensional equality is an equivalence relation *) + +Theorem EqSt_reflex : forall s:Stream, EqSt s s. +coinduction EqSt_reflex. +reflexivity. +Qed. + +Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1. +coinduction Eq_sym. +case H; intros; symmetry in |- *; assumption. +case H; intros; assumption. +Qed. + + +Theorem trans_EqSt : + forall 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 : + forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2. +unfold Str_nth in |- *; simple induction n. +intros s1 s2 H; case H; trivial with datatypes. +intros m hypind. +simpl in |- *. +intros s1 s2 H. +apply hypind. +case H; trivial with datatypes. +Qed. + +Theorem ntheq_eqst : + forall s1 s2:Stream, + (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2. +coinduction Equiv2. +apply (H 0). +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 : forall x:Stream, P x -> Exists x + | Further : forall x:Stream, Exists (tl x) -> Exists x. + +CoInductive ForAll : Stream -> Prop := + HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x. + + +Section Co_Induction_ForAll. +Variable Inv : Stream -> Prop. +Hypothesis InvThenP : forall x:Stream, Inv x -> P x. +Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x). + +Theorem ForAll_coind : forall 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 (s:Stream A) : Stream B := 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.
\ No newline at end of file diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v new file mode 100755 index 00000000..fbeb97ce --- /dev/null +++ b/theories/Lists/TheoryList.v @@ -0,0 +1,403 @@ +(************************************************************************) +(* 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.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Some programs and results about lists following CAML Manual *) + +Require Export List. +Set Implicit Arguments. +Section Lists. + +Variable A : Set. + +(**********************) +(** The null function *) +(**********************) + +Definition Isnil (l:list A) : Prop := nil = l. + +Lemma Isnil_nil : Isnil nil. +red in |- *; auto. +Qed. +Hint Resolve Isnil_nil. + +Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l). +unfold Isnil in |- *. +intros; discriminate. +Qed. + +Hint Resolve Isnil_nil not_Isnil_cons. + +Lemma Isnil_dec : forall 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 : + forall l:list A, {a : A & {m : list A | 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 : + forall l:list A, {a : A | exists m : list A, 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 : + forall l:list A, + {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}. +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) {struct l} : 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}. +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}. +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. + +Inductive AllS (P:A -> Prop) : list A -> Prop := + | allS_nil : AllS P nil + | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l). +Hint Resolve allS_nil allS_cons. + +Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}. + +Fixpoint mem (a:A) (l:list A) {struct l} : 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}. +intros a l. +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. +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. +induction 1; auto. +Qed. + +Lemma nth_le_length : + forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l. +induction 1; simpl in |- *; auto with arith. +Qed. + +Fixpoint Nth_func (l:list A) (n:nat) {struct l} : 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}. +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}. +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) {struct l} : 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}. +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}. + +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. +induction 1; simpl in |- *; auto. +Qed. + +Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l. +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). +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. +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}. +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 : Set. +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}. +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 : Set. +Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : + 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}. +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 allS_nil allS_cons: + datatypes. +Hint Immediate fst_nth_nth: datatypes. diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex new file mode 100755 index 00000000..344bba59 --- /dev/null +++ b/theories/Lists/intro.tex @@ -0,0 +1,24 @@ +\section{Lists}\label{Lists} + +This library includes the following files: + +\begin{itemize} + +\item {\tt List.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY + WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD. + +\item {\tt PolyList.v} contains definitions of (polymorphic) lists, + functions on lists such as head, tail, map, append and prove some + properties of these functions. Implicit arguments are used in this + library, so you should read the Referance Manual about implicit + arguments before using it. + +\item {\tt TheoryList.v} contains complementary results on lists. Here + a more theoric 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. + +\end{itemize} |