diff options
Diffstat (limited to 'theories/Lists')
| -rwxr-xr-x | theories/Lists/List.v | 741 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 467 | ||||
| -rwxr-xr-x | theories/Lists/MonoList.v | 212 | ||||
| -rw-r--r-- | theories/Lists/PolyList.v | 642 | ||||
| -rw-r--r-- | theories/Lists/PolyListSyntax.v | 10 | ||||
| -rwxr-xr-x | theories/Lists/Streams.v | 171 | ||||
| -rwxr-xr-x | theories/Lists/TheoryList.v | 445 |
7 files changed, 1234 insertions, 1454 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 7e6cf4c880..1eb095c149 100755 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -8,254 +8,643 @@ (*i $Id$ i*) -(* This file is a copy of file MonoList.v *) +Require Import Le. -(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) -Require Le. +Section Lists. -Parameter List_Dom:Set. -Definition A := List_Dom. +Variable A : Set. -Inductive list : Set := nil : list | cons : A -> list -> list. +Set Implicit Arguments. -Fixpoint app [l:list] : list -> list - := [m:list]<list>Cases l of - nil => m - | (cons a l1) => (cons a (app l1 m)) - end. +Inductive list : Set := + | nil : list + | cons : A -> list -> list. +Infix "::" := cons (at level 60, right associativity) : list_scope. -Lemma app_nil_end : (l:list)(l=(app l nil)). +Open Scope list_scope. + +(*************************) +(** Discrimination *) +(*************************) + +Lemma nil_cons : forall (a:A) (m:list), nil <> a :: m. Proof. - Intro l ; Elim l ; Simpl ; Auto. - Induction 1; Auto. + intros; discriminate. 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)). +(*************************) +(** 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. - Intros l m n ; Elim l ; Simpl ; Auto with list. - Induction 1; Auto with list. + induction l; simpl in |- *; auto. + rewrite <- IHl; auto. Qed. -Hints Resolve app_ass : list v62. +Hint Resolve app_nil_end. + +Ltac now_show c := change c in |- *. -Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n). +Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n. Proof. - Auto with list. + intros. induction l; simpl in |- *; auto. + now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n). + rewrite <- IHl; auto. Qed. -Hints Resolve ass_app : list v62. +Hint Resolve app_ass. -Definition tail := - [l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list. - +Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n. +Proof. + auto. +Qed. +Hint Resolve ass_app. -Lemma nil_cons : (a:A)(m:list)~nil=(cons a m). - Intros; Discriminate. +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 *) +(** Length of lists *) (****************************************) -Fixpoint length [l:list] : nat - := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end. +Fixpoint length (l:list) : nat := + match l with + | nil => 0 + | _ :: m => S (length m) + end. (******************************) -(* Length order of lists *) +(** Length order of lists *) (******************************) Section length_order. -Definition lel := [l,m:list](le (length l) (length m)). +Definition lel (l m:list) := length l <= length m. -Hints Unfold lel : list. +Variables a b : A. +Variables l m n : list. -Variables a,b:A. -Variables l,m,n:list. - -Lemma lel_refl : (lel l l). +Lemma lel_refl : lel l l. Proof. - Unfold lel ; Auto with list. + unfold lel in |- *; auto with arith. Qed. -Lemma lel_trans : (lel l m)->(lel m n)->(lel l n). +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. + 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 (cons a l) (cons b m)). +Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with arith. Qed. -Lemma lel_cons : (lel l m)->(lel l (cons b m)). +Lemma lel_cons : lel l m -> lel l (b :: m). Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with arith. Qed. -Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m). +Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with arith. Qed. -Lemma lel_nil : (l':list)(lel l' nil)->(nil=l'). +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 (le (S (length y)) O); Auto with list arith. + 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. -Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62. +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 *) +(***************************) -Fixpoint In [a:A;l:list] : Prop := - Cases l of - nil => False - | (cons b m) => (b=a)\/(In a m) - end. +Definition incl (l m:list) := forall a:A, In a l -> In a m. +Hint Unfold incl. -Lemma in_eq : (a:A)(l:list)(In a (cons a l)). +Lemma incl_refl : forall l:list, incl l l. Proof. - Simpl ; Auto with list. + auto. Qed. -Hints Resolve in_eq : list v62. +Hint Resolve incl_refl. -Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)). +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (a :: m). Proof. - Simpl ; Auto with list. + auto. Qed. -Hints Resolve in_cons : list v62. +Hint Immediate incl_tl. -Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)). +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. 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)). + auto. +Qed. + +Lemma incl_appl : forall l m n:list, incl l n -> incl l (n ++ 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). + auto. +Qed. +Hint Immediate incl_appl. + +Lemma incl_appr : forall l m n:list, incl l n -> incl l (m ++ n). Proof. - Auto with list. + auto. Qed. -Hints Resolve incl_refl : list v62. +Hint Immediate incl_appr. -Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)). +Lemma incl_cons : + forall (a:A) (l m:list), In a m -> incl l m -> incl (a :: l) m. Proof. - Auto with list. + 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. -Hints Immediate incl_tl : list v62. +Hint Resolve incl_cons. -Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n). +Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (l ++ m) n. Proof. - Auto with list. + 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 incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)). +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. - Auto with list. + 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. -Hints Immediate incl_appl : list v62. -Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)). +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. - Auto with list. + induction l as [| a l IHl]; simpl in |- *; + [ auto + | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ]. 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). +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. - 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). + 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. - 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. + 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.
\ No newline at end of file diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 4b7083c0a9..f2fb20f722 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -16,374 +16,383 @@ This allow to "hide" the definitions, functions and theorems of PolyList and to see only the ones of ListSet *) -Require PolyList. +Require Import List. Set Implicit Arguments. -V7only [Implicits nil [1].]. Section first_definitions. Variable A : Set. - Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}. + Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}. - Definition set := (list A). + Definition set := list A. - Definition empty_set := (!nil ?) : set. + Definition empty_set : set := nil. - 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 + 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] : bool := - Cases x of + Fixpoint set_mem (a:A) (x:set) {struct x} : bool := + match x with | nil => false - | (cons a1 x1) => Cases (Aeq_dec a a1) of - | (left _) => true - | (right _) => (set_mem a x1) - end + | 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] : set := - Cases x of + Fixpoint set_remove (a:A) (x:set) {struct x} : set := + match x with | nil => empty_set - | (cons a1 x1) => Cases (Aeq_dec a a1) of - | (left _) => x1 - | (right _) => (cons a1 (set_remove a x1)) - end + | 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 := - 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) + 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] : set := - Cases y of + Fixpoint set_union (x y:set) {struct y} : set := + match y with | nil => x - | (cons a1 y1) => (set_add a1 (set_union x y1)) + | 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 + Fixpoint set_diff (x y:set) {struct x} : set := + match x with | nil => nil - | (cons a1 x1) => if (set_mem a1 y) - then (set_diff x1 y) - else (set_add a1 (set_diff x1 y)) + | 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). + Definition set_In : A -> set -> Prop := In (A:=A). - Lemma set_In_dec : (a:A; x:set){(set_In a x)}+{~(set_In a x)}. + Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}. Proof. - Unfold set_In. + unfold set_In 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. + 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 : - (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)). + 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. - Induction x; Simpl; Intros. - Assumption. - Elim (Aeq_dec a a0); Auto with datatypes. + simple induction x; simpl in |- *; 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)). + 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. - 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. + 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 : - (a:A)(x:set)(set_mem a x)=true -> (set_In a x). + forall (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. + simple induction x; simpl in |- *. + 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. + forall (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. + 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 : - (a:A)(x:set)(set_mem a x)=false -> ~(set_In a x). + forall (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. + 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 : - (a:A)(x:set)~(set_In a x) -> (set_mem a x)=false. + forall (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. + 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 : (a,b:A)(x:set) - (set_In a x) -> (set_In a (set_add b x)). + 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; 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 ]. + 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 : (a,b:A)(x:set) - a=b -> (set_In a (set_add b x)). + Lemma set_add_intro2 : + forall (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 ]. + 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. - Hints Resolve set_add_intro1 set_add_intro2. + Hint 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)). + 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. + 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). + 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. - 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. + 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 : (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. + 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. - Hints Resolve set_add_intro set_add_elim set_add_elim2. + Hint 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. + Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set. Proof. - Induction x; Simpl. - Discriminate. - Intros; Elim (Aeq_dec a a0); Intros; Discriminate. + simple induction x; simpl in |- *. + 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)). + Lemma set_union_intro1 : + forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). Proof. - Induction y; Simpl; Auto with datatypes. + simple induction y; simpl in |- *; auto with datatypes. Qed. - Lemma set_union_intro2 : (a:A)(x,y:set) - (set_In a y) -> (set_In a (set_union x y)). + Lemma set_union_intro2 : + forall (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. + simple induction y; simpl in |- *. + tauto. + intros; elim H0; auto with datatypes. Qed. - Hints Resolve set_union_intro2 set_union_intro1. + Hint 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)). + 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. + 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). + 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. - Induction y; Simpl. - Auto with datatypes. - Intros. - Generalize (set_add_elim H0). - Intros [H1 | H1]. - Auto with datatypes. - Tauto. + 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 : (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. + 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 : (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. + 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 : (a:A)(x,y:set) - (set_In a x) -> (set_In a y) -> (set_In a (set_inter x y)). + 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. - 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]. + 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 : (a:A)(x,y:set) - (set_In a (set_inter x y)) -> (set_In a x). + Lemma set_inter_elim1 : + forall (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. + 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 : (a:A)(x,y:set) - (set_In a (set_inter x y)) -> (set_In a y). + Lemma set_inter_elim2 : + forall (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. + 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. - Hints Resolve set_inter_elim1 set_inter_elim2. + Hint 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). + 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. + 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)). + 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. - 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. + 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 : (a:A)(x,y:set) - (set_In a (set_diff x y)) -> (set_In a x). + Lemma set_diff_elim1 : + forall (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. + 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 : (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. + 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 : (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). + 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. -Hints Resolve set_diff_intro set_diff_trivial. +Hint Resolve set_diff_intro set_diff_trivial. End first_definitions. Section other_definitions. - Variables A,B : Set. + Variables A B : Set. - Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B). + 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 1!A 2!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 1!A 2!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 1!B 2!A). + Definition set_fold_left : (B -> A -> B) -> set A -> B -> B := + fold_left (A:=B) (B:=A). - Definition set_fold_right : (A -> B -> B) -> (set A) -> B -> B := - [f][x][b](fold_right f b x). + Definition set_fold_right (f:A -> B -> B) (x:set A) + (b:B) : B := fold_right f b x. End other_definitions. -V7only [Implicits nil [].]. -Unset Implicit Arguments. +Unset Implicit Arguments.
\ No newline at end of file diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v index 528e61ab08..28e52a4152 100755 --- a/theories/Lists/MonoList.v +++ b/theories/Lists/MonoList.v @@ -10,97 +10,105 @@ (** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) -Require Le. +Require Import Le. -Parameter List_Dom:Set. +Parameter List_Dom : Set. Definition A := List_Dom. -Inductive list : Set := nil : list | cons : A -> list -> list. +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. +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 : (l:list)(l=(app l nil)). +Lemma app_nil_end : forall l:list, l = app l nil. Proof. - Intro l ; Elim l ; Simpl ; Auto. - Induction 1; Auto. + intro l; elim l; simpl in |- *; auto. + simple induction 1; auto. Qed. -Hints Resolve app_nil_end : list v62. +Hint Resolve app_nil_end: list v62. -Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)). +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 ; Auto with list. - Induction 1; Auto with list. + intros l m n; elim l; simpl in |- *; auto with list. + simple induction 1; auto with list. Qed. -Hints Resolve app_ass : list v62. +Hint Resolve app_ass: list v62. -Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n). +Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n. Proof. - Auto with list. + auto with list. Qed. -Hints Resolve ass_app : list v62. +Hint Resolve ass_app: list v62. -Definition tail := - [l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list. +Definition tail (l:list) : list := + match l return list with + | cons _ m => m + | _ => nil + end. -Lemma nil_cons : (a:A)(m:list)~nil=(cons a m). - Intros; Discriminate. +Lemma nil_cons : forall (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. +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](le (length l) (length m)). +Definition lel (l m:list) := length l <= length m. -Hints Unfold lel : list. +Hint Unfold lel: list. -Variables a,b:A. -Variables l,m,n:list. +Variables a b : A. +Variables l m n : list. -Lemma lel_refl : (lel l l). +Lemma lel_refl : lel l l. Proof. - Unfold lel ; Auto with list. + unfold lel in |- *; auto with list. Qed. -Lemma lel_trans : (lel l m)->(lel m n)->(lel l n). +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. + 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)). +Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m). Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with list arith. Qed. -Lemma lel_cons : (lel l m)->(lel l (cons b m)). +Lemma lel_cons : lel l m -> lel l (cons b m). Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with list arith. Qed. -Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m). +Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m. Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with list arith. Qed. -Lemma lel_nil : (l':list)(lel l' nil)->(nil=l'). +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. + intro l'; elim l'; auto with list arith. + intros a' y H H0. (* <list>nil=(cons a' y) ============================ H0 : (lel (cons a' y) nil) @@ -108,35 +116,36 @@ Proof. y : list a' : A l' : list *) - Absurd (le (S (length y)) O); Auto with list arith. + absurd (S (length y) <= 0); 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. +Hint 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. +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 : (a:A)(l:list)(In a (cons a l)). +Lemma in_eq : forall (a:A) (l:list), In a (cons a l). Proof. - Simpl ; Auto with list. + simpl in |- *; auto with list. Qed. -Hints Resolve in_eq : list v62. +Hint Resolve in_eq: list v62. -Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)). +Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l). Proof. - Simpl ; Auto with list. + simpl in |- *; auto with list. Qed. -Hints Resolve in_cons : list v62. +Hint 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)). +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 ; Auto with list. - Intros a0 y H H0. + 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)) @@ -146,81 +155,82 @@ Proof. a : A m : list l : list *) - Elim H0 ; Auto with list. - Intro H1. + 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. + elim (H H1); auto with list. Qed. -Hints Immediate in_app_or : list v62. +Hint 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)). +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 ; Intro H. + 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. + elim H; auto with list; intro H0. (* (In a m) ============================ H0 : False *) - Elim H0. (* subProof completed *) - Intros y H0 H1. + 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. + 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. + elim H2; auto with list. Qed. -Hints Resolve in_or_app : list v62. +Hint Resolve in_or_app: list v62. -Definition incl := [l,m:list](a:A)(In a l)->(In a m). +Definition incl (l m:list) := forall a:A, In a l -> In a m. -Hints Unfold incl : list v62. +Hint Unfold incl: list v62. -Lemma incl_refl : (l:list)(incl l l). +Lemma incl_refl : forall l:list, incl l l. Proof. - Auto with list. + auto with list. Qed. -Hints Resolve incl_refl : list v62. +Hint Resolve incl_refl: list v62. -Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)). +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m). Proof. - Auto with list. + auto with list. Qed. -Hints Immediate incl_tl : list v62. +Hint Immediate incl_tl: list v62. -Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n). +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. Proof. - Auto with list. + auto with list. Qed. -Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)). +Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m). Proof. - Auto with list. + auto with list. Qed. -Hints Immediate incl_appl : list v62. +Hint Immediate incl_appl: list v62. -Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)). +Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n). Proof. - Auto with list. + auto with list. Qed. -Hints Immediate incl_appr : list v62. +Hint Immediate incl_appr: list v62. -Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m). +Lemma incl_cons : + forall (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. + unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. (* (In a0 m) ============================ H1 : (<A>a=a0)\/(In a0 l) @@ -230,21 +240,21 @@ Proof. m : list l : list a : A *) - Elim H1. + elim H1. (* 1 (<A>a=a0)->(In a0 m) *) - Elim H1 ; Auto with list ; Intro H2. + elim H1; auto with list; intro H2. (* (<A>a=a0)->(In a0 m) ============================ H2 : <A>a=a0 *) - Elim H2 ; Auto with list. (* solves subgoal *) + elim H2; auto with list. (* solves subgoal *) (* 2 (In a0 l)->(In a0 m) *) - Auto with list. + auto with list. Qed. -Hints Resolve incl_cons : list v62. +Hint Resolve incl_cons: list v62. -Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n). +Lemma incl_app : forall 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. + unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. (* (In a n) ============================ H1 : (In a (app l m)) @@ -254,6 +264,6 @@ Proof. n : list m : list l : list *) - Elim (in_app_or l m a) ; Auto with list. + elim (in_app_or l m a); auto with list. Qed. -Hints Resolve incl_app : list v62. +Hint Resolve incl_app: list v62.
\ No newline at end of file diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v deleted file mode 100644 index 50b203d4e5..0000000000 --- a/theories/Lists/PolyList.v +++ /dev/null @@ -1,642 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ 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. diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v deleted file mode 100644 index a4b6a57aae..0000000000 --- a/theories/Lists/PolyListSyntax.v +++ /dev/null @@ -1,10 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 9bbbe0e46c..19c564eb96 100755 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -16,115 +16,123 @@ Section Streams. Variable A : Set. -CoInductive Set Stream := Cons : A->Stream->Stream. +CoInductive Stream : Set := + Cons : A -> Stream -> Stream. -Definition hd := - [x:Stream] Cases x of (Cons a _) => a end. +Definition hd (x:Stream) := match x with + | Cons a _ => a + end. -Definition tl := - [x:Stream] Cases x of (Cons _ s) => s end. +Definition tl (x:Stream) := match x with + | 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. +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 : nat->Stream->A := [n:nat][s:Stream](hd (Str_nth_tl n s)). +Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s). -Lemma unfold_Stream :(x:Stream)x=(Cases x of (Cons a s) => (Cons a s) end). +Lemma unfold_Stream : + forall x:Stream, x = match x with + | Cons a s => Cons a s + end. Proof. - Intro x. - Case x. - Trivial. + 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)). +Lemma tl_nth_tl : + forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s). Proof. - Induction n; Simpl; Auto. + simple induction n; simpl in |- *; 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. +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 - : (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. +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 : (s1,s2:Stream) - ((hd s1)=(hd s2))-> - (EqSt (tl s1) (tl s2)) - ->(EqSt s1 s2). +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 *) -Tactic Definition CoInduction proof := - Cofix proof; Intros; Constructor; - [Clear proof | Try (Apply proof;Clear proof)]. +Ltac 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. +Theorem EqSt_reflex : forall 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. +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 : - (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. +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 : - (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. + 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 : - (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)). +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. +Variable P : Stream -> Prop. (*i Inductive Exists : Stream -> Prop := @@ -132,21 +140,21 @@ Inductive Exists : Stream -> Prop := | 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). +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 := - forall : (x:Stream)(P x)->(ForAll (tl x))->(ForAll 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 : (x:Stream)(Inv x)->(P x). -Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)). +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 : (x:Stream)(Inv x)->(ForAll x). -(CoInduction ForAll_coind);Auto. +Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x. +coinduction ForAll_coind; auto. Qed. End Co_Induction_ForAll. @@ -155,16 +163,15 @@ 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))). +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). +CoFixpoint const : Stream A := Cons a const. End Constant_Stream. -Unset Implicit Arguments. +Unset Implicit Arguments.
\ No newline at end of file diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index c7abe31da9..da23394c0a 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -10,32 +10,32 @@ (** Some programs and results about lists following CAML Manual *) -Require Export PolyList. +Require Export List. Set Implicit Arguments. -Chapter Lists. +Section Lists. -Variable A : Set. +Variable A : Set. (**********************) (** The null function *) (**********************) -Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l. +Definition Isnil (l:list A) : Prop := nil = l. -Lemma Isnil_nil : (Isnil (nil A)). -Red; Auto. +Lemma Isnil_nil : Isnil nil. +red in |- *; auto. Qed. -Hints Resolve Isnil_nil. +Hint Resolve Isnil_nil. -Lemma not_Isnil_cons : (a:A)(l:(list A))~(Isnil (cons a l)). -Unfold Isnil. -Intros; Discriminate. +Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l). +unfold Isnil in |- *. +intros; discriminate. Qed. -Hints Resolve Isnil_nil not_Isnil_cons. +Hint Resolve Isnil_nil not_Isnil_cons. -Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}. -Intro l; Case l;Auto. +Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}. +intro l; case l; auto. (* Realizer (fun l => match l with | nil => true @@ -48,10 +48,11 @@ 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. +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 @@ -64,10 +65,11 @@ 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. +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 @@ -76,11 +78,12 @@ Realizer (fun l => match l with *) 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. +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 @@ -94,25 +97,25 @@ Qed. (****************************************) (* 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. +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 : (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. +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 : (l:(list A)){m:nat|(length l)=m}. -Intro l. Apply (Length_l_pf l O). +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). *) @@ -121,43 +124,42 @@ 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. +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 A)) - | allS_cons : (a:A)(l:(list A))(P a)->(AllS P l)->(AllS P (cons a l)). -Hints Resolve allS_nil allS_cons. +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 : (a,b:A){a=b}+{~a=b}. +Hypothesis eqA_dec : forall 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) +Fixpoint mem (a:A) (l:list A) {struct l} : bool := + match l with + | nil => false + | b :: m => if eqA_dec a b then fun H => true else fun 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. +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. *) @@ -167,146 +169,157 @@ 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. +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. -Hints Immediate fst_nth_nth. +Hint 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. +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 : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(le n (length l)). -NewInduction 1; Simpl; Auto with arith. +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)] : 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. +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 : (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. +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 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. +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 : (a:A)(l:(list A)) - {n:nat|(fst_nth_spec l n a)}+{(AllS [b:A]~a=b l)}. +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 (S O)); Auto. -Intros (n,P); Left; Exists n; Auto. -Rewrite (minus_n_O n); Trivial. +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. -Variable R,P : A -> Prop. +Variables 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. +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)]Cases l of - nil => False - | (cons b m) => (R b)\/(InR m) - end. +Definition InR_inv (l:list A) := + match l with + | nil => False + | b :: m => R b \/ InR m + end. -Lemma InR_INV : (l:(list A))(InR l)->(InR_inv l). -NewInduction 1; Simpl; Auto. +Lemma InR_INV : forall l:list A, InR l -> InR_inv l. +induction 1; simpl in |- *; 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). +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 : (l,m:(list A))((InR l)\/(InR m))->(InR (app l m)). -Intros l m [|]. -NewInduction 1; Simpl; Auto. -Intro. NewInduction l; Simpl; Auto. +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 : (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. +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 : (a:A){(R a)}+{(P a)}. +Hypothesis RS_dec : forall 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. +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 : (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. +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. *) @@ -315,26 +328,27 @@ 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. +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. *) @@ -345,17 +359,20 @@ 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. +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 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)). +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). -Hints Resolve allS_assoc_nil allS_assoc_cons. +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 @@ -364,13 +381,14 @@ Hints Resolve allS_assoc_nil allS_assoc_cons. (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. +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. *) @@ -380,7 +398,6 @@ 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. - +Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons: + datatypes. +Hint Immediate fst_nth_nth: datatypes. |