diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 14:38:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:48 +0200 |
| commit | 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a (patch) | |
| tree | 4bf6607f8a29238bac0d87775d74f2105a1b9384 /theories/Lists | |
| parent | 8c74d3e5578caeb5c62ba462528d9972c1de17f1 (diff) | |
Temporary hack to compensate missing comma while re-printing tactic
"exists c1, c2".
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 1381 |
1 files changed, 703 insertions, 678 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index b66699220..8dba22354 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -26,83 +26,83 @@ In a special module to avoid conflicts. *) Module ListNotations. Notation " [ ] " := nil (format "[ ]") : list_scope. Notation " [ x ] " := (cons x nil) : list_scope. -Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope. +Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : + list_scope. End ListNotations. Import ListNotations. Section Lists. - Variable A : Type. + Variable (A : Type). (** Head and tail *) - Definition hd (default:A) (l:list A) := + Definition hd (default : A) (l : list A) := match l with - | [] => default - | x :: _ => x + | [] => default + | x :: _ => x end. - Definition hd_error (l:list A) := + Definition hd_error (l : list A) := match l with - | [] => None - | x :: _ => Some x + | [] => None + | x :: _ => Some x end. - Definition tl (l:list A) := - match l with - | [] => nil - | a :: m => m - end. + Definition tl (l : list A) := match l with + | [] => nil + | a :: m => m + end. (** The [In] predicate *) - Fixpoint In (a:A) (l:list A) : Prop := + Fixpoint In (a : A) (l : list A) : Prop := match l with - | [] => False - | b :: m => b = a \/ In a m + | [] => False + | b :: m => b = a \/ In a m end. End Lists. Section Facts. - Variable A : Type. + Variable (A : Type). (** *** Generic facts *) (** Discrimination *) - Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. + Theorem nil_cons : forall (x : A) (l : list A), [] <> x :: l. Proof. - intros; discriminate. + intros **; discriminate. Qed. (** Destruction *) - Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}. + Theorem destruct_list : + forall l : list A, {x : A & {tl : list A | l = x :: tl}} + {l = []}. Proof. - induction l as [|a tail]. + induction l as [| a tail]. right; reflexivity. - left; exists a, tail; reflexivity. + left; exists a; exists tail; reflexivity. Qed. - Lemma hd_error_tl_repr : forall l (a:A) r, - hd_error l = Some a /\ tl l = r <-> l = a :: r. - Proof. destruct l as [|x xs]. + Lemma hd_error_tl_repr : + forall l (a : A) r, hd_error l = Some a /\ tl l = r <-> l = a :: r. + Proof. destruct l as [| x xs]. - unfold hd_error, tl; intros a r. split; firstorder discriminate. - - intros. simpl. split. + - intros **. simpl. split. * intros (H1, H2). inversion H1. rewrite H2. reflexivity. * inversion 1. subst. auto. Qed. - Lemma hd_error_some_nil : forall l (a:A), hd_error l = Some a -> l <> nil. - Proof. unfold hd_error. destruct l; now discriminate. Qed. + Lemma hd_error_some_nil : forall l (a : A), hd_error l = Some a -> l <> nil. + Proof. unfold hd_error. destruct l; (now (discriminate)). Qed. - Theorem length_zero_iff_nil (l : list A): - length l = 0 <-> l=[]. + Theorem length_zero_iff_nil (l : list A) : length l = 0 <-> l = []. Proof. - split; [now destruct l | now intros ->]. + split; [ now (destruct l) | now (intros ->) ]. Qed. (** *** Head and tail *) @@ -112,9 +112,10 @@ Section Facts. simpl; reflexivity. Qed. - Theorem hd_error_cons : forall (l : list A) (x : A), hd_error (x::l) = Some x. + Theorem hd_error_cons : + forall (l : list A) (x : A), hd_error (x :: l) = Some x. Proof. - intros; simpl; reflexivity. + intros **; simpl; reflexivity. Qed. @@ -125,46 +126,48 @@ Section Facts. (** Characterization of [In] *) - Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). + Theorem in_eq : forall (a : A) (l : list A), In a (a :: l). Proof. simpl; auto. Qed. - Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). + Theorem in_cons : forall (a b : A) (l : list A), In b l -> In b (a :: l). Proof. simpl; auto. Qed. - Theorem not_in_cons (x a : A) (l : list A): - ~ In x (a::l) <-> x<>a /\ ~ In x l. + Theorem not_in_cons (x a : A) (l : list A) : + ~ In x (a :: l) <-> x <> a /\ ~ In x l. Proof. simpl. intuition. Qed. - Theorem in_nil : forall a:A, ~ In a []. + Theorem in_nil : forall a : A, ~ In a []. Proof. unfold not; intros a H; inversion_clear H. Qed. - Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. + Theorem in_split : + forall x (l : list A), In x l -> exists l1 l2, l = l1 ++ x :: l2. Proof. induction l; simpl; destruct 1. subst a; auto. - exists [], l; auto. - destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1), l2; simpl. apply f_equal. auto. + exists []; exists l; auto. + destruct (IHl H) as (l1, (l2, H0)). + exists (a :: l1); exists l2; simpl. apply f_equal. auto. Qed. (** Inversion *) - Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. + Lemma in_inv : + forall (a b : A) (l : list A), In b (a :: l) -> a = b \/ In b l. Proof. intros a b l H; inversion_clear H; auto. Qed. (** Decidability of [In] *) Theorem in_dec : - (forall x y:A, {x = y} + {x <> y}) -> - forall (a:A) (l:list A), {In a l} + {~ In a l}. + (forall x y : A, {x = y} + {x <> y}) -> + forall (a : A) (l : list A), {In a l} + {~ In a l}. Proof. intro H; induction l as [| a0 l IHl]. right; apply in_nil. @@ -179,41 +182,42 @@ Section Facts. (**************************) (** Discrimination *) - Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y. + Theorem app_cons_not_nil : forall (x y : list A) (a : A), [] <> x ++ a :: y. Proof. unfold not. - destruct x as [| a l]; simpl; intros. + destruct x as [| a l]; simpl; intros **. discriminate H. discriminate H. Qed. (** Concat with [nil] *) - Theorem app_nil_l : forall l:list A, [] ++ l = l. + Theorem app_nil_l : forall l : list A, [] ++ l = l. Proof. reflexivity. Qed. - Theorem app_nil_r : forall l:list A, l ++ [] = l. + Theorem app_nil_r : forall l : list A, l ++ [] = l. Proof. induction l; simpl; f_equal; auto. Qed. (* begin hide *) (* Deprecated *) - Theorem app_nil_end : forall (l:list A), l = l ++ []. + Theorem app_nil_end : forall l : list A, l = l ++ []. Proof. symmetry; apply app_nil_r. Qed. (* end hide *) (** [app] is associative *) - Theorem app_assoc : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n. + Theorem app_assoc : forall l m n : list A, l ++ m ++ n = (l ++ m) ++ n. Proof. intros l m n; induction l; simpl; f_equal; auto. Qed. (* begin hide *) (* Deprecated *) - Theorem app_assoc_reverse : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n. + Theorem app_assoc_reverse : + forall l m n : list A, (l ++ m) ++ n = l ++ m ++ n. Proof. auto using app_assoc. Qed. @@ -221,14 +225,16 @@ Section Facts. (* end hide *) (** [app] commutes with [cons] *) - Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y. + Theorem app_comm_cons : + forall (x y : list A) (a : A), a :: x ++ y = (a :: x) ++ y. Proof. auto. Qed. (** Facts deduced from the result of a concatenation *) - Theorem app_eq_nil : forall l l':list A, l ++ l' = [] -> l = [] /\ l' = []. + Theorem app_eq_nil : + forall l l' : list A, l ++ l' = [] -> l = [] /\ l' = []. Proof. destruct l as [| x l]; destruct l' as [| y l']; simpl; auto. intro; discriminate. @@ -236,18 +242,19 @@ Section Facts. Qed. Theorem app_eq_unit : - forall (x y:list A) (a:A), - x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []. + forall (x y : list A) (a : A), + x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []. Proof. - destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; - simpl. + destruct x as [| a l]; + [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl. intros a H; discriminate H. left; split; auto. right; split; auto. generalize H. generalize (app_nil_r l); intros E. - rewrite -> E; auto. - intros. + rewrite E; auto. + intros **. injection H. intro. assert ([] = l ++ a0 :: l0) by auto. @@ -255,11 +262,11 @@ Section Facts. Qed. Lemma app_inj_tail : - forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. + forall (x y : list A) (a b : A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. induction x as [| x l IHl]; - [ destruct y as [| a l] | destruct y as [| a l0] ]; - simpl; auto. + [ destruct y as [| a l] | destruct y as [| a l0] ]; + simpl; auto. - intros a b H. injection H. auto. @@ -272,19 +279,21 @@ Section Facts. apply app_cons_not_nil in H as []. - intros a0 b H. injection H as <- H0. - destruct (IHl l0 a0 b H0) as (<-,<-). + destruct (IHl l0 a0 b H0) as (<-, <-). split; auto. Qed. (** Compatibility with other operations *) - Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'. + Lemma app_length : + forall l l' : list A, length (l ++ l') = length l + length l'. Proof. induction l; simpl; auto. Qed. - Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m. + Lemma in_app_or : + forall (l m : list A) (a : A), In a (l ++ m) -> In a l \/ In a m. Proof. intros l m a. elim l; simpl; auto. @@ -296,7 +305,8 @@ Section Facts. elim (H H1); auto. Qed. - Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m). + Lemma in_or_app : + forall (l m : list A) (a : A), In a l \/ In a m -> In a (l ++ m). Proof. intros l m a. elim l; simpl; intro H. @@ -312,30 +322,29 @@ Section Facts. elim H2; auto. Qed. - Lemma in_app_iff : forall l l' (a:A), In a (l++l') <-> In a l \/ In a l'. + Lemma in_app_iff : + forall l l' (a : A), In a (l ++ l') <-> In a l \/ In a l'. Proof. split; auto using in_app_or, in_or_app. Qed. - Lemma app_inv_head: - forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Lemma app_inv_head : forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. Proof. induction l; simpl; auto; injection 1; auto. Qed. - Lemma app_inv_tail: - forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Lemma app_inv_tail : forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. Proof. intros l l1 l2; revert l1 l2 l. - induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; - simpl; auto; intros l H. + induction l1 as [| x1 l1]; destruct l2 as [| x2 l2]; simpl; auto; + intros l H. absurd (length (x2 :: l2 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite <- H; auto with arith. absurd (length (x1 :: l1 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite H; auto with arith. - injection H; clear H; intros; f_equal; eauto. + injection H; clear H; intros **; f_equal; eauto. Qed. End Facts. @@ -354,68 +363,70 @@ Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. Section Elts. - Variable A : Type. + Variable (A : Type). (*****************************) (** ** Nth element of a list *) (*****************************) - Fixpoint nth (n:nat) (l:list A) (default:A) {struct l} : A := + Fixpoint nth (n : nat) (l : list A) (default : A) {struct l} : A := match n, l with - | O, x :: l' => x - | O, other => default - | S m, [] => default - | S m, x :: t => nth m t default + | O, x :: l' => x + | O, other => default + | S m, [] => default + | S m, x :: t => nth m t default end. - Fixpoint nth_ok (n:nat) (l:list A) (default:A) {struct l} : bool := + Fixpoint nth_ok (n : nat) (l : list A) (default : A) {struct l} : bool := match n, l with - | O, x :: l' => true - | O, other => false - | S m, [] => false - | S m, x :: t => nth_ok m t default + | O, x :: l' => true + | O, other => false + | S m, [] => false + | S m, x :: t => nth_ok m t default end. Lemma nth_in_or_default : - forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}. + forall (n : nat) (l : list A) (d : A), + {In (nth n l d) l} + {nth n l d = d}. Proof. intros n l d; revert n; induction l. - right; destruct n; trivial. - - intros [|n]; simpl. + - intros [| n]; simpl. * left; auto. * destruct (IHl n); auto. Qed. Lemma nth_S_cons : - forall (n:nat) (l:list A) (d a:A), - In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). + forall (n : nat) (l : list A) (d a : A), + In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). Proof. simpl; auto. Qed. - Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A := + Fixpoint nth_error (l : list A) (n : nat) {struct n} : + option A := match n, l with - | O, x :: _ => Some x - | S n, _ :: l => nth_error l n - | _, _ => None + | O, x :: _ => Some x + | S n, _ :: l => nth_error l n + | _, _ => None end. - Definition nth_default (default:A) (l:list A) (n:nat) : A := + Definition nth_default (default : A) (l : list A) + (n : nat) : A := match nth_error l n with - | Some x => x - | None => default + | Some x => x + | None => default end. - Lemma nth_default_eq : - forall n l (d:A), nth_default d l n = nth n l d. + Lemma nth_default_eq : forall n l (d : A), nth_default d l n = nth n l d. Proof. - unfold nth_default; induction n; intros [ | ] ?; simpl; auto. + unfold nth_default; induction n; intros [| ] ?; simpl; auto. Qed. (** Results about [nth] *) Lemma nth_In : - forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l. + forall (n : nat) (l : list A) (d : A), n < length l -> In (nth n l d) l. Proof. unfold lt; induction n as [| n hn]; simpl. - destruct l; simpl; [ inversion 2 | auto ]. @@ -424,74 +435,74 @@ Section Elts. * intros d ie; right; apply hn; auto with arith. Qed. - Lemma In_nth l x d : In x l -> - exists n, n < length l /\ nth n l d = x. + Lemma In_nth l x d : In x l -> exists n, n < length l /\ nth n l d = x. Proof. - induction l as [|a l IH]. + induction l as [| a l IH]. - easy. - - intros [H|H]. + - intros [H| H]. * subst; exists 0; simpl; auto with arith. - * destruct (IH H) as (n & Hn & Hn'). + * destruct (IH H) as (n, (Hn, Hn')). exists (S n); simpl; auto with arith. Qed. Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d. Proof. - induction l; destruct n; simpl; intros; auto. + induction l; destruct n; simpl; intros **; auto. - inversion H. - apply IHl; auto with arith. Qed. - Lemma nth_indep : - forall l n d d', n < length l -> nth n l d = nth n l d'. + Lemma nth_indep : forall l n d d', n < length l -> nth n l d = nth n l d'. Proof. induction l. - inversion 1. - - intros [|n] d d'; simpl; auto with arith. + - intros [| n] d d'; simpl; auto with arith. Qed. Lemma app_nth1 : - forall l l' d n, n < length l -> nth n (l++l') d = nth n l d. + forall l l' d n, n < length l -> nth n (l ++ l') d = nth n l d. Proof. induction l. - inversion 1. - - intros l' d [|n]; simpl; auto with arith. + - intros l' d [| n]; simpl; auto with arith. Qed. Lemma app_nth2 : - forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d. + forall l l' d n, + n >= length l -> nth n (l ++ l') d = nth (n - length l) l' d. Proof. - induction l; intros l' d [|n]; auto. + induction l; intros l' d [| n]; auto. - inversion 1. - - intros; simpl; rewrite IHl; auto with arith. + - intros **; simpl; rewrite IHl; auto with arith. Qed. - Lemma nth_split n l d : n < length l -> + Lemma nth_split n l d : + n < length l -> exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n. Proof. revert l. - induction n as [|n IH]; intros [|a l] H; try easy. - - exists nil; exists l; now simpl. - - destruct (IH l) as (l1 & l2 & Hl & Hl1); auto with arith. - exists (a::l1); exists l2; simpl; split; now f_equal. + induction n as [| n IH]; intros [| a l] H; try easy. + - exists nil; exists l; (now (simpl)). + - destruct (IH l) as (l1, (l2, (Hl, Hl1))); auto with arith. + exists (a :: l1); exists l2; simpl; split; (now f_equal). Qed. (** Results about [nth_error] *) Lemma nth_error_In l n x : nth_error l n = Some x -> In x l. Proof. - revert n. induction l as [|a l IH]; intros [|n]; simpl; try easy. + revert n. induction l as [| a l IH]; intros [| n]; simpl; try easy. - injection 1; auto. - eauto. Qed. Lemma In_nth_error l x : In x l -> exists n, nth_error l n = Some x. Proof. - induction l as [|a l IH]. + induction l as [| a l IH]. - easy. - - intros [H|H]. + - intros [H| H]. * subst; exists 0; simpl; auto with arith. - * destruct (IH H) as (n,Hn). + * destruct (IH H) as (n, Hn). exists (S n); simpl; auto with arith. Qed. @@ -500,42 +511,43 @@ Section Elts. revert n. induction l; destruct n; simpl. - split; auto. - split; auto with arith. - - split; now auto with arith. + - split; (now (auto with arith)). - rewrite IHl; split; auto with arith. Qed. Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l. Proof. revert n. induction l; destruct n; simpl. - - split; [now destruct 1 | inversion 1]. - - split; [now destruct 1 | inversion 1]. - - split; now auto with arith. + - split; [ now (destruct 1) | inversion 1 ]. + - split; [ now (destruct 1) | inversion 1 ]. + - split; (now (auto with arith)). - rewrite IHl; split; auto with arith. Qed. - Lemma nth_error_split l n a : nth_error l n = Some a -> + Lemma nth_error_split l n a : + nth_error l n = Some a -> exists l1, exists l2, l = l1 ++ a :: l2 /\ length l1 = n. Proof. revert l. - induction n as [|n IH]; intros [|x l] H; simpl in *; try easy. - - exists nil; exists l. injection H; clear H; intros; now subst. - - destruct (IH _ H) as (l1 & l2 & H1 & H2). - exists (x::l1); exists l2; simpl; split; now f_equal. + induction n as [| n IH]; intros [| x l] H; simpl in *; try easy. + - exists nil; exists l. injection H; clear H; intros **; (now (subst)). + - destruct (IH _ H) as (l1, (l2, (H1, H2))). + exists (x :: l1); exists l2; simpl; split; (now f_equal). Qed. - Lemma nth_error_app1 l l' n : n < length l -> - nth_error (l++l') n = nth_error l n. + Lemma nth_error_app1 l l' n : + n < length l -> nth_error (l ++ l') n = nth_error l n. Proof. revert l. - induction n; intros [|a l] H; auto; try solve [inversion H]. + induction n; intros [| a l] H; auto; try (solve [ inversion H ]). simpl in *. apply IHn. auto with arith. Qed. - Lemma nth_error_app2 l l' n : length l <= n -> - nth_error (l++l') n = nth_error l' (n-length l). + Lemma nth_error_app2 l l' n : + length l <= n -> nth_error (l ++ l') n = nth_error l' (n - length l). Proof. revert l. - induction n; intros [|a l] H; auto; try solve [inversion H]. + induction n; intros [| a l] H; auto; try (solve [ inversion H ]). simpl in *. apply IHn. auto with arith. Qed. @@ -543,18 +555,18 @@ Section Elts. (** ** Remove *) (*****************) - Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + Hypothesis (eq_dec : forall x y : A, {x = y} + {x <> y}). Fixpoint remove (x : A) (l : list A) : list A := match l with - | [] => [] - | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + | [] => [] + | y :: tl => if eq_dec x y then remove x tl else y :: remove x tl end. Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). Proof. - induction l as [|x l]; auto. - intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. + induction l as [| x l]; auto. + intro y; simpl; destruct (eq_dec y x) as [yeqx| yneqx]. apply IHl. unfold not; intro HF; simpl in HF; destruct HF; auto. apply (IHl y); assumption. @@ -568,20 +580,20 @@ Section Elts. (** [last l d] returns the last element of the list [l], or the default value [d] if [l] is empty. *) - Fixpoint last (l:list A) (d:A) : A := - match l with + Fixpoint last (l : list A) (d : A) : A := + match l with | [] => d | [a] => a | a :: l => last l d - end. + end. (** [removelast l] remove the last element of [l] *) - Fixpoint removelast (l:list A) : list A := + Fixpoint removelast (l : list A) : list A := match l with - | [] => [] - | [a] => [] - | a :: l => a :: removelast l + | [] => [] + | [a] => [] + | a :: l => a :: removelast l end. Lemma app_removelast_last : @@ -591,34 +603,34 @@ Section Elts. destruct 1; auto. intros d _. destruct l; auto. - pattern (a0::l) at 1; rewrite IHl with d; auto; discriminate. + pattern (a0 :: l) at 1; rewrite IHl with d; auto; discriminate. Qed. Lemma exists_last : - forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}. + forall l, l <> [] -> {l' : list A & {a : A | l = l' ++ [a]}}. Proof. induction l. destruct 1; auto. intros _. destruct l. - exists [], a; auto. - destruct IHl as [l' (a',H)]; try discriminate. + exists []; exists a; auto. + destruct IHl as [l' (a', H)]; try discriminate. rewrite H. - exists (a::l'), a'; auto. + exists (a :: l'); exists a'; auto. Qed. Lemma removelast_app : - forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'. + forall l l', l' <> [] -> removelast (l ++ l') = l ++ removelast l'. Proof. induction l. simpl; auto. - simpl; intros. - assert (l++l' <> []). + simpl; intros **. + assert (l ++ l' <> []). destruct l. simpl; auto. simpl; discriminate. specialize (IHl l' H). - destruct (l++l'); [elim H0; auto|f_equal; auto]. + destruct (l ++ l'); [ elim H0; auto | f_equal; auto ]. Qed. @@ -628,23 +640,21 @@ Section Elts. Fixpoint count_occ (l : list A) (x : A) : nat := match l with - | [] => 0 - | y :: tl => - let n := count_occ tl x in - if eq_dec y x then S n else n + | [] => 0 + | y :: tl => let n := count_occ tl x in if eq_dec y x then S n else n end. (** Compatibility of count_occ with operations on list *) Theorem count_occ_In l x : In x l <-> count_occ l x > 0. Proof. - induction l as [|y l]; simpl. - - split; [destruct 1 | apply gt_irrefl]. - - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition. + induction l as [| y l]; simpl. + - split; [ destruct 1 | apply gt_irrefl ]. + - destruct eq_dec as [->| Hneq]; rewrite IHl; intuition. Qed. Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0. Proof. - rewrite count_occ_In. unfold gt. now rewrite Nat.nlt_ge, Nat.le_0_r. + rewrite count_occ_In. unfold gt. now (rewrite Nat.nlt_ge, Nat.le_0_r). Qed. Lemma count_occ_nil x : count_occ [] x = 0. @@ -652,26 +662,25 @@ Section Elts. reflexivity. Qed. - Theorem count_occ_inv_nil l : - (forall x:A, count_occ l x = 0) <-> l = []. + Theorem count_occ_inv_nil l : (forall x : A, count_occ l x = 0) <-> l = []. Proof. split. - - induction l as [|x l]; trivial. + - induction l as [| x l]; trivial. intros H. specialize (H x). simpl in H. - destruct eq_dec as [_|NEQ]; [discriminate|now elim NEQ]. - - now intros ->. + destruct eq_dec as [_| NEQ]; [ discriminate | now (elim NEQ) ]. + - now (intros ->). Qed. Lemma count_occ_cons_eq l x y : - x = y -> count_occ (x::l) y = S (count_occ l y). + x = y -> count_occ (x :: l) y = S (count_occ l y). Proof. - intros H. simpl. now destruct (eq_dec x y). + intros H. simpl. now (destruct (eq_dec x y)). Qed. Lemma count_occ_cons_neq l x y : - x <> y -> count_occ (x::l) y = count_occ l y. + x <> y -> count_occ (x :: l) y = count_occ l y. Proof. - intros H. simpl. now destruct (eq_dec x y). + intros H. simpl. now (destruct (eq_dec x y)). Qed. End Elts. @@ -682,19 +691,19 @@ End Elts. Section ListOps. - Variable A : Type. + Variable (A : Type). (*************************) (** ** Reverse *) (*************************) - Fixpoint rev (l:list A) : list A := + Fixpoint rev (l : list A) : list A := match l with - | [] => [] - | x :: l' => rev l' ++ [x] + | [] => [] + | x :: l' => rev l' ++ [x] end. - Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x. + Lemma rev_app_distr : forall x y : list A, rev (x ++ y) = rev y ++ rev x. Proof. induction x as [| a l IHl]. destruct y as [| a l]. @@ -710,13 +719,13 @@ Section ListOps. rewrite app_assoc; trivial. Qed. - Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l. + Remark rev_unit : forall (l : list A) (a : A), rev (l ++ [a]) = a :: rev l. Proof. - intros. + intros **. apply (rev_app_distr l [a]); simpl; auto. Qed. - Lemma rev_involutive : forall l:list A, rev (rev l) = l. + Lemma rev_involutive : forall l : list A, rev (rev l) = l. Proof. induction l as [| a l IHl]. simpl; auto. @@ -733,7 +742,7 @@ Section ListOps. Proof. induction l. simpl; intuition. - intros. + intros **. simpl. intuition. subst. @@ -744,19 +753,19 @@ Section ListOps. Lemma rev_length : forall l, length (rev l) = length l. Proof. - induction l;simpl; auto. + induction l; simpl; auto. rewrite app_length. rewrite IHl. simpl. elim (length l); simpl; auto. Qed. - Lemma rev_nth : forall l d n, n < length l -> - nth n (rev l) d = nth (length l - S n) l d. + Lemma rev_nth : + forall l d n, n < length l -> nth n (rev l) d = nth (length l - S n) l d. Proof. induction l. - intros; inversion H. - intros. + intros **; inversion H. + intros **. simpl in H. simpl (rev (a :: l)). simpl (length (a :: l) - S n). @@ -769,30 +778,30 @@ Section ListOps. rewrite (minus_plus_simpl_l_reverse (length l) n 1). replace (1 + length l) with (S (length l)); auto with arith. rewrite <- minus_Sn_m; auto with arith. - apply IHl ; auto with arith. + apply IHl; auto with arith. rewrite rev_length; auto. Qed. (** An alternative tail-recursive definition for reverse *) - Fixpoint rev_append (l l': list A) : list A := + Fixpoint rev_append (l l' : list A) : list A := match l with - | [] => l' - | a::l => rev_append l (a::l') + | [] => l' + | a :: l => rev_append l (a :: l') end. Definition rev' l : list A := rev_append l []. Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'. Proof. - induction l; simpl; auto; intros. + induction l; simpl; auto; intros **. rewrite <- app_assoc; firstorder. Qed. Lemma rev_alt : forall l, rev l = rev_append l []. Proof. - intros; rewrite rev_append_rev. + intros **; rewrite rev_append_rev. rewrite app_nil_r; trivial. Qed. @@ -804,27 +813,28 @@ Section ListOps. Section Reverse_Induction. Lemma rev_list_ind : - forall P:list A-> Prop, - P [] -> - (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> - forall l:list A, P (rev l). + forall P : list A -> Prop, + P [] -> + (forall (a : A) (l : list A), P (rev l) -> P (rev (a :: l))) -> + forall l : list A, P (rev l). Proof. induction l; auto. Qed. Theorem rev_ind : - forall P:list A -> Prop, - P [] -> - (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. + forall P : list A -> Prop, + P [] -> + (forall (x : A) (l : list A), P l -> P (l ++ [x])) -> + forall l : list A, P l. Proof. - intros. + intros **. generalize (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind P). auto. simpl. - intros. + intros **. apply (H0 a (rev l0)). auto. Qed. @@ -836,10 +846,10 @@ Section ListOps. (*************************) Fixpoint concat (l : list (list A)) : list A := - match l with - | nil => nil - | cons x l => x ++ concat l - end. + match l with + | nil => nil + | cons x l => x ++ concat l + end. Lemma concat_nil : concat nil = nil. Proof. @@ -853,7 +863,7 @@ Section ListOps. Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2. Proof. - intros l1; induction l1 as [|x l1 IH]; intros l2; simpl. + intros l1; induction l1 as [| x l1 IH]; intros l2; simpl. + reflexivity. + rewrite IH; apply app_assoc. Qed. @@ -862,9 +872,9 @@ Section ListOps. (** ** Decidable equality on lists *) (***********************************) - Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}. + Hypothesis (eq_dec : forall x y : A, {x = y} + {x <> y}). - Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}. + Lemma list_eq_dec : forall l l' : list A, {l = l'} + {l <> l'}. Proof. decide equality. Defined. End ListOps. @@ -879,28 +889,28 @@ End ListOps. Section Map. Variables (A : Type) (B : Type). - Variable f : A -> B. + Variable (f : A -> B). - Fixpoint map (l:list A) : list B := + Fixpoint map (l : list A) : list B := match l with - | [] => [] - | a :: t => (f a) :: (map t) + | [] => [] + | a :: t => f a :: map t end. - Lemma map_cons (x:A)(l:list A) : map (x::l) = (f x) :: (map l). + Lemma map_cons (x : A) (l : list A) : map (x :: l) = f x :: map l. Proof. reflexivity. Qed. - Lemma in_map : - forall (l:list A) (x:A), In x l -> In (f x) (map l). + Lemma in_map : forall (l : list A) (x : A), In x l -> In (f x) (map l). Proof. - induction l; firstorder (subst; auto). + induction l; firstorder subst; auto. Qed. - Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l. + Lemma in_map_iff : + forall l y, In y (map l) <-> (exists x, f x = y /\ In x l). Proof. - induction l; firstorder (subst; auto). + induction l; firstorder subst; auto. Qed. Lemma map_length : forall l, length (map l) = length l. @@ -908,23 +918,21 @@ Section Map. induction l; simpl; auto. Qed. - Lemma map_nth : forall l d n, - nth n (map l) (f d) = f (nth n l d). + Lemma map_nth : forall l d n, nth n (map l) (f d) = f (nth n l d). Proof. induction l; simpl map; destruct n; firstorder. Qed. - Lemma map_nth_error : forall n l d, - nth_error l n = Some d -> nth_error (map l) n = Some (f d). + Lemma map_nth_error : + forall n l d, nth_error l n = Some d -> nth_error (map l) n = Some (f d). Proof. - induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto. + induction n; intros [| ] ? Heq; simpl in *; inversion Heq; auto. Qed. - Lemma map_app : forall l l', - map (l++l') = (map l)++(map l'). + Lemma map_app : forall l l', map (l ++ l') = map l ++ map l'. Proof. induction l; simpl; auto. - intros; rewrite IHl; auto. + intros **; rewrite IHl; auto. Qed. Lemma map_rev : forall l, map (rev l) = rev (map l). @@ -941,17 +949,17 @@ Section Map. (** [map] and count of occurrences *) - Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}. - Hypothesis decB: forall y1 y2 : B, {y1 = y2} + {y1 <> y2}. - Hypothesis Hfinjective: forall x1 x2: A, (f x1) = (f x2) -> x1 = x2. + Hypothesis (decA : forall x1 x2 : A, {x1 = x2} + {x1 <> x2}). + Hypothesis (decB : forall y1 y2 : B, {y1 = y2} + {y1 <> y2}). + Hypothesis (Hfinjective : forall x1 x2 : A, f x1 = f x2 -> x1 = x2). - Theorem count_occ_map x l: + Theorem count_occ_map x l : count_occ decA l x = count_occ decB (map l) (f x). Proof. revert x. induction l as [| a l' Hrec]; intro x; simpl. - reflexivity. - specialize (Hrec x). - destruct (decA a x) as [H1|H1], (decB (f a) (f x)) as [H2|H2]. + destruct (decA a x) as [H1| H1], (decB (f a) (f x)) as [H2| H2]. * rewrite Hrec. reflexivity. * contradiction H2. rewrite H1. reflexivity. * specialize (Hfinjective H2). contradiction H1. @@ -960,55 +968,57 @@ Section Map. (** [flat_map] *) - Definition flat_map (f:A -> list B) := - fix flat_map (l:list A) : list B := - match l with + Definition flat_map (f : A -> list B) := + fix flat_map (l : list A) : list B := + match l with | nil => nil - | cons x t => (f x)++(flat_map t) - end. + | cons x t => f x ++ flat_map t + end. - Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), - In y (flat_map f l) <-> exists x, In x l /\ In y (f x). - Proof using A B. + Lemma in_flat_map : + forall (f : A -> list B) (l : list A) (y : B), + In y (flat_map f l) <-> (exists x, In x l /\ In y (f x)). + Proof using ((B) + (A)). clear Hfinjective. - induction l; simpl; split; intros. + induction l; simpl; split; intros **. contradiction. - destruct H as (x,(H,_)); contradiction. + destruct H as (x, (H, _)); contradiction. destruct (in_app_or _ _ _ H). exists a; auto. - destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). + destruct (IHl y) as (H1, _); destruct (H1 H0) as (x, (H2, H3)). exists x; auto. apply in_or_app. - destruct H as (x,(H0,H1)); destruct H0. + destruct H as (x, (H0, H1)); destruct H0. subst; auto. - right; destruct (IHl y) as (_,H2); apply H2. + right; destruct (IHl y) as (_, H2); apply H2. exists x; auto. Qed. End Map. -Lemma flat_map_concat_map : forall A B (f : A -> list B) l, - flat_map f l = concat (map f l). +Lemma flat_map_concat_map : + forall A B (f : A -> list B) l, flat_map f l = concat (map f l). Proof. -intros A B f l; induction l as [|x l IH]; simpl. +intros A B f l; induction l as [| x l IH]; simpl. + reflexivity. + rewrite IH; reflexivity. Qed. -Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). +Lemma concat_map : + forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). Proof. -intros A B f l; induction l as [|x l IH]; simpl. +intros A B f l; induction l as [| x l IH]; simpl. + reflexivity. + rewrite map_app, IH; reflexivity. Qed. -Lemma map_id : forall (A :Type) (l : list A), - map (fun x => x) l = l. +Lemma map_id : forall (A : Type) (l : list A), map (fun x => x) l = l. Proof. induction l; simpl; auto; rewrite IHl; auto. Qed. -Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l, +Lemma map_map : + forall (A B C : Type) (f : A -> B) (g : B -> C) l, map g (map f l) = map (fun x => g (f x)) l. Proof. induction l; simpl; auto. @@ -1016,16 +1026,18 @@ Proof. Qed. Lemma map_ext_in : - forall (A B : Type)(f g:A->B) l, (forall a, In a l -> f a = g a) -> map f l = map g l. + forall (A B : Type) (f g : A -> B) l, + (forall a, In a l -> f a = g a) -> map f l = map g l. Proof. induction l; simpl; auto. - intros; rewrite H by intuition; rewrite IHl; auto. + intros **; rewrite H by intuition; rewrite IHl; auto. Qed. Lemma map_ext : - forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l. + forall (A B : Type) (f g : A -> B), + (forall a, f a = g a) -> forall l, map f l = map g l. Proof. - intros; apply map_ext_in; auto. + intros **; apply map_ext_in; auto. Qed. @@ -1035,20 +1047,21 @@ Qed. Section Fold_Left_Recursor. Variables (A : Type) (B : Type). - Variable f : A -> B -> A. + Variable (f : A -> B -> A). - Fixpoint fold_left (l:list B) (a0:A) : A := + Fixpoint fold_left (l : list B) (a0 : A) : A := match l with - | nil => a0 - | cons b t => fold_left t (f a0 b) + | nil => a0 + | cons b t => fold_left t (f a0 b) end. - Lemma fold_left_app : forall (l l':list B)(i:A), - fold_left (l++l') i = fold_left l' (fold_left l i). + Lemma fold_left_app : + forall (l l' : list B) (i : A), + fold_left (l ++ l') i = fold_left l' (fold_left l i). Proof. induction l. simpl; auto. - intros. + intros **. simpl. auto. Qed. @@ -1056,12 +1069,13 @@ Section Fold_Left_Recursor. End Fold_Left_Recursor. Lemma fold_left_length : - forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l. + forall (A : Type) (l : list A), fold_left (fun x _ => S x) l 0 = length l. Proof. intros A l. - enough (H : forall n, fold_left (fun x _ => S x) l n = n + length l) by exact (H 0). + enough (H : forall n, fold_left (fun x _ => S x) l n = n + length l) by + exact (H 0). induction l; simpl; auto. - intros; rewrite IHl. + intros **; rewrite IHl. simpl; auto with arith. Qed. @@ -1071,32 +1085,34 @@ Qed. Section Fold_Right_Recursor. Variables (A : Type) (B : Type). - Variable f : B -> A -> A. - Variable a0 : A. + Variable (f : B -> A -> A). + Variable (a0 : A). - Fixpoint fold_right (l:list B) : A := + Fixpoint fold_right (l : list B) : A := match l with - | nil => a0 - | cons b t => f b (fold_right t) + | nil => a0 + | cons b t => f b (fold_right t) end. End Fold_Right_Recursor. - Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i, - fold_right f i (l++l') = fold_right f (fold_right f i l') l. + Lemma fold_right_app : + forall (A B : Type) (f : A -> B -> B) l l' i, + fold_right f i (l ++ l') = fold_right f (fold_right f i l') l. Proof. induction l. simpl; auto. - simpl; intros. + simpl; intros **. f_equal; auto. Qed. - Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i, + Lemma fold_left_rev_right : + forall (A B : Type) (f : A -> B -> B) l i, fold_right f i (rev l) = fold_left (fun x y => f y x) l i. Proof. induction l. simpl; auto. - intros. + intros **. simpl. rewrite fold_right_app; simpl; auto. Qed. @@ -1104,25 +1120,27 @@ End Fold_Right_Recursor. Theorem fold_symmetric : forall (A : Type) (f : A -> A -> A), (forall x y z : A, f x (f y z) = f (f x y) z) -> - forall (a0 : A), (forall y : A, f a0 y = f y a0) -> - forall (l : list A), fold_left f l a0 = fold_right f a0 l. + forall a0 : A, + (forall y : A, f a0 y = f y a0) -> + forall l : list A, fold_left f l a0 = fold_right f a0 l. Proof. intros A f assoc a0 comma0 l. - induction l as [ | a1 l ]; [ simpl; reflexivity | ]. - simpl. rewrite <- IHl. clear IHl. revert a1. induction l; [ auto | ]. + induction l as [| a1 l]; [ simpl; reflexivity | ]. + simpl. rewrite <- IHl. clear IHl. revert a1. induction l; [ auto | ]. simpl. intro. rewrite <- assoc. rewrite IHl. rewrite IHl. 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:Type)(l:list A) (l':list B) : - list (list (A * B)) := + Fixpoint list_power (A B : Type) (l : list A) (l' : list B) : + 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') + | 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. @@ -1131,20 +1149,20 @@ End Fold_Right_Recursor. (*************************************) Section Bool. - Variable A : Type. - Variable f : A -> bool. + Variable (A : Type). + Variable (f : A -> bool). (** find whether a boolean function can be satisfied by an elements of the list. *) - Fixpoint existsb (l:list A) : bool := + Fixpoint existsb (l : list A) : bool := match l with - | nil => false - | a::l => f a || existsb l + | nil => false + | a :: l => f a || existsb l end. Lemma existsb_exists : - forall l, existsb l = true <-> exists x, In x l /\ f x = true. + forall l, existsb l = true <-> (exists x, In x l /\ f x = true). Proof. induction l; simpl; intuition. inversion H. @@ -1155,32 +1173,33 @@ End Fold_Right_Recursor. rewrite H2; auto. Qed. - Lemma existsb_nth : forall l n d, n < length l -> - existsb l = false -> f (nth n l d) = false. + Lemma existsb_nth : + forall l n d, + n < length l -> existsb l = false -> f (nth n l d) = false. Proof. induction l. inversion 1. - simpl; intros. + simpl; intros **. destruct (orb_false_elim _ _ H0); clear H0; auto. - destruct n ; auto. + destruct n; auto. rewrite IHl; auto with arith. Qed. - Lemma existsb_app : forall l1 l2, - existsb (l1++l2) = existsb l1 || existsb l2. + Lemma existsb_app : + forall l1 l2, existsb (l1 ++ l2) = existsb l1 || existsb l2. Proof. induction l1; intros l2; simpl. - solve[auto]. - case (f a); simpl; solve[auto]. + solve [ auto ]. + case (f a); simpl; (solve [ auto ]). Qed. (** find whether a boolean function is satisfied by all the elements of a list. *) - Fixpoint forallb (l:list A) : bool := + Fixpoint forallb (l : list A) : bool := match l with - | nil => true - | a::l => f a && forallb l + | nil => true + | a :: l => f a && forallb l end. Lemma forallb_forall : @@ -1196,39 +1215,39 @@ End Fold_Right_Recursor. Qed. Lemma forallb_app : - forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2. + forall l1 l2, forallb (l1 ++ l2) = forallb l1 && forallb l2. Proof. induction l1; simpl. - solve[auto]. - case (f a); simpl; solve[auto]. + solve [ auto ]. + case (f a); simpl; (solve [ auto ]). Qed. (** [filter] *) - Fixpoint filter (l:list A) : list A := + Fixpoint filter (l : list A) : list A := match l with - | nil => nil - | x :: l => if f x then x::(filter l) else filter l + | nil => nil + | x :: l => if f x then x :: filter l else filter l end. Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true. Proof. induction l; simpl. intuition. - intros. - case_eq (f a); intros; simpl; intuition congruence. + intros **. + case_eq (f a); intros **; simpl; (intuition (congruence)). Qed. (** [find] *) - Fixpoint find (l:list A) : option A := + Fixpoint find (l : list A) : option A := match l with - | nil => None - | x :: tl => if f x then Some x else find tl + | nil => None + | x :: tl => if f x then Some x else find tl end. Lemma find_some l x : find l = Some x -> In x l /\ f x = true. Proof. - induction l as [|a l IH]; simpl; [easy| ]. + induction l as [| a l IH]; simpl; [ easy | ]. case_eq (f a); intros Ha Eq. * injection Eq as ->; auto. * destruct (IH Eq); auto. @@ -1236,59 +1255,55 @@ End Fold_Right_Recursor. Lemma find_none l : find l = None -> forall x, In x l -> f x = false. Proof. - induction l as [|a l IH]; simpl; [easy|]. - case_eq (f a); intros Ha Eq x IN; [easy|]. - destruct IN as [<-|IN]; auto. + induction l as [| a l IH]; simpl; [ easy | ]. + case_eq (f a); intros Ha Eq x IN; [ easy | ]. + destruct IN as [<-| IN]; auto. Qed. (** [partition] *) - Fixpoint partition (l:list A) : list A * list A := + Fixpoint partition (l : list A) : list A * list A := match l with - | nil => (nil, nil) - | x :: tl => let (g,d) := partition tl in - if f x then (x::g,d) else (g,x::d) + | nil => (nil, nil) + | x :: tl => + let (g, d) := partition tl in + if f x then (x :: g, d) else (g, x :: d) end. - Theorem partition_cons1 a l l1 l2: + Theorem partition_cons1 a l l1 l2 : partition l = (l1, l2) -> - f a = true -> - partition (a::l) = (a::l1, l2). + f a = true -> partition (a :: l) = (a :: l1, l2). Proof. - simpl. now intros -> ->. + simpl. now (intros -> ->). Qed. - Theorem partition_cons2 a l l1 l2: + Theorem partition_cons2 a l l1 l2 : partition l = (l1, l2) -> - f a=false -> - partition (a::l) = (l1, a::l2). + f a = false -> partition (a :: l) = (l1, a :: l2). Proof. - simpl. now intros -> ->. + simpl. now (intros -> ->). Qed. - Theorem partition_length l l1 l2: - partition l = (l1, l2) -> - length l = length l1 + length l2. + Theorem partition_length l l1 l2 : + partition l = (l1, l2) -> length l = length l1 + length l2. Proof. - revert l1 l2. induction l as [ | a l' Hrec]; intros l1 l2. - - now intros [= <- <- ]. - - simpl. destruct (f a), (partition l') as (left, right); - intros [= <- <- ]; simpl; rewrite (Hrec left right); auto. + revert l1 l2. induction l as [| a l' Hrec]; intros l1 l2. + - now (intros [=<- <-]). + - simpl. destruct (f a), (partition l') as (left, right); intros [=<- <-]; simpl; + rewrite (Hrec left right); auto. Qed. - Theorem partition_inv_nil (l : list A): - partition l = ([], []) <-> l = []. + Theorem partition_inv_nil (l : list A) : partition l = ([], []) <-> l = []. Proof. split. - - destruct l as [|a l' _]. + - destruct l as [| a l' _]. * intuition. - * simpl. destruct (f a), (partition l'); now intros [= -> ->]. - - now intros ->. + * simpl. destruct (f a), (partition l'); (now (intros [=-> ->])). + - now (intros ->). Qed. - Theorem elements_in_partition l l1 l2: - partition l = (l1, l2) -> - forall x:A, In x l <-> In x l1 \/ In x l2. + Theorem elements_in_partition l l1 l2 : + partition l = (l1, l2) -> forall x : A, In x l <-> In x l1 \/ In x l2. Proof. revert l1 l2. induction l as [| a l' Hrec]; simpl; intros l1 l2 Eq x. - injection Eq as <- <-. tauto. @@ -1311,34 +1326,39 @@ End Fold_Right_Recursor. (** [split] derives two lists from a list of pairs *) - Fixpoint split (l:list (A*B)) : list A * list B := + Fixpoint split (l : list (A * B)) : list A * list B := match l with - | [] => ([], []) - | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) + | [] => ([], []) + | (x, y) :: tl => + let (left, right) := split tl in (x :: left, y :: right) end. - Lemma in_split_l : forall (l:list (A*B))(p:A*B), + Lemma in_split_l : + forall (l : list (A * B)) (p : A * B), In p l -> In (fst p) (fst (split l)). Proof. - induction l; simpl; intros; auto. + induction l; simpl; intros **; auto. destruct p; destruct a; destruct (split l); simpl in *. destruct H. injection H; auto. - right; apply (IHl (a0,b) H). + right; apply (IHl (a0, b) H). Qed. - Lemma in_split_r : forall (l:list (A*B))(p:A*B), + Lemma in_split_r : + forall (l : list (A * B)) (p : A * B), In p l -> In (snd p) (snd (split l)). Proof. - induction l; simpl; intros; auto. + induction l; simpl; intros **; auto. destruct p; destruct a; destruct (split l); simpl in *. destruct H. injection H; auto. - right; apply (IHl (a0,b) H). + right; apply (IHl (a0, b) H). Qed. - Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), - nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)). + Lemma split_nth : + forall (l : list (A * B)) (n : nat) (d : A * B), + nth n l d = + (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)). Proof. induction l. destruct n; destruct d; simpl; auto. @@ -1348,15 +1368,15 @@ End Fold_Right_Recursor. apply IHl. Qed. - Lemma split_length_l : forall (l:list (A*B)), - length (fst (split l)) = length l. + Lemma split_length_l : + forall l : list (A * B), length (fst (split l)) = length l. Proof. induction l; simpl; auto. destruct a; destruct (split l); simpl; auto. Qed. - Lemma split_length_r : forall (l:list (A*B)), - length (snd (split l)) = length l. + Lemma split_length_r : + forall l : list (A * B), length (snd (split l)) = length l. Proof. induction l; simpl; auto. destruct a; destruct (split l); simpl; auto. @@ -1366,14 +1386,15 @@ End Fold_Right_Recursor. Lists given to [combine] are meant to be of same length. If not, [combine] stops on the shorter list *) - Fixpoint combine (l : list A) (l' : list B) : list (A*B) := - match l,l' with - | x::tl, y::tl' => (x,y)::(combine tl tl') - | _, _ => nil + Fixpoint combine (l : list A) (l' : list B) : + list (A * B) := + match l, l' with + | x :: tl, y :: tl' => (x, y) :: combine tl tl' + | _, _ => nil end. - Lemma split_combine : forall (l: list (A*B)), - let (l1,l2) := split l in combine l1 l2 = l. + Lemma split_combine : + forall l : list (A * B), let (l1, l2) := split l in combine l1 l2 = l. Proof. induction l. simpl; auto. @@ -1382,38 +1403,42 @@ End Fold_Right_Recursor. f_equal; auto. Qed. - Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> - split (combine l l') = (l,l'). + Lemma combine_split : + forall (l : list A) (l' : list B), + length l = length l' -> split (combine l l') = (l, l'). Proof. - induction l; destruct l'; simpl; intros; auto; try discriminate. - injection H; clear H; intros. + induction l; destruct l'; simpl; intros **; auto; try discriminate. + injection H; clear H; intros **. rewrite IHl; auto. Qed. - Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), - In (x,y) (combine l l') -> In x l. + Lemma in_combine_l : + forall (l : list A) (l' : list B) (x : A) (y : B), + In (x, y) (combine l l') -> In x l. Proof. induction l. simpl; auto. - destruct l'; simpl; auto; intros. + destruct l'; simpl; auto; intros **. contradiction. destruct H. injection H; auto. right; apply IHl with l' y; auto. Qed. - Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B), - In (x,y) (combine l l') -> In y l'. + Lemma in_combine_r : + forall (l : list A) (l' : list B) (x : A) (y : B), + In (x, y) (combine l l') -> In y l'. Proof. induction l. - simpl; intros; contradiction. - destruct l'; simpl; auto; intros. + simpl; intros **; contradiction. + destruct l'; simpl; auto; intros **. destruct H. injection H; auto. right; apply IHl with x; auto. Qed. - Lemma combine_length : forall (l:list A)(l':list B), + Lemma combine_length : + forall (l : list A) (l' : list B), length (combine l l') = min (length l) (length l'). Proof. induction l. @@ -1421,11 +1446,12 @@ End Fold_Right_Recursor. destruct l'; simpl; auto. Qed. - Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B), + Lemma combine_nth : + forall (l : list A) (l' : list B) (n : nat) (x : A) (y : B), length l = length l' -> - nth n (combine l l') (x,y) = (nth n l x, nth n l' y). + nth n (combine l l') (x, y) = (nth n l x, nth n l' y). Proof. - induction l; destruct l'; intros; try discriminate. + induction l; destruct l'; intros **; try discriminate. destruct n; simpl; auto. destruct n; simpl in *; auto. Qed. @@ -1434,52 +1460,53 @@ End Fold_Right_Recursor. [combine], it adds every possible pairs, not only those at the same position. *) - Fixpoint list_prod (l:list A) (l':list B) : - list (A * B) := + Fixpoint list_prod (l : list A) (l' : list B) : + list (A * B) := match l with - | nil => nil - | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') + | nil => nil + | cons x t => map (fun y : B => (x, y)) l' ++ list_prod t l' end. Lemma in_prod_aux : - forall (x:A) (y:B) (l:list B), - In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). + forall (x : A) (y : B) (l : list B), + In y l -> In (x, y) (map (fun y0 : B => (x, y0)) l). Proof. induction l; - [ simpl; auto - | simpl; destruct 1 as [H1| ]; - [ left; rewrite H1; trivial | right; auto ] ]. + [ simpl; auto + | simpl; destruct 1 as [H1| ]; + [ left; rewrite H1; trivial | right; auto ] ]. Qed. Lemma in_prod : - forall (l:list A) (l':list B) (x:A) (y:B), - In x l -> In y l' -> In (x, y) (list_prod l l'). + forall (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; tauto - | simpl; intros; apply in_or_app; destruct H; - [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. + [ simpl; tauto + | simpl; intros **; apply in_or_app; destruct H; + [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. Lemma in_prod_iff : - forall (l:list A)(l':list B)(x:A)(y:B), - In (x,y) (list_prod l l') <-> In x l /\ In y l'. + forall (l : list A) (l' : list B) (x : A) (y : B), + In (x, y) (list_prod l l') <-> In x l /\ In y l'. Proof. - split; [ | intros; apply in_prod; intuition ]. - induction l; simpl; intros. + split; [ | intros **; apply in_prod; intuition ]. + induction l; simpl; intros **. intuition. destruct (in_app_or _ _ _ H); clear H. - destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). - destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. - injection H2; clear H2; intros; subst; intuition. + destruct (in_map_iff (fun y : B => (a, y)) l' (x, y)) as (H1, _). + destruct (H1 H0) as (z, (H2, H3)); clear H0 H1. + injection H2; clear H2; intros **; subst; intuition. intuition. Qed. - Lemma prod_length : forall (l:list A)(l':list B), - length (list_prod l l') = (length l) * (length l'). + Lemma prod_length : + forall (l : list A) (l' : list B), + length (list_prod l l') = length l * length l'. Proof. induction l; simpl; auto. - intros. + intros **. rewrite app_length. rewrite map_length. auto. @@ -1501,12 +1528,12 @@ End Fold_Right_Recursor. (******************************) Section length_order. - Variable A : Type. + Variable (A : Type). - Definition lel (l m:list A) := length l <= length m. + Definition lel (l m : list A) := length l <= length m. - Variables a b : A. - Variables l m n : list A. + Variables (a b : A). + Variables (l m n : list A). Lemma lel_refl : lel l l. Proof. @@ -1515,7 +1542,7 @@ Section length_order. Lemma lel_trans : lel l m -> lel m n -> lel l n. Proof. - unfold lel; intros. + unfold lel; intros **. now_show (length l <= length n). apply le_trans with (length m); auto with arith. Qed. @@ -1535,7 +1562,7 @@ Section length_order. unfold lel; simpl; auto with arith. Qed. - Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'. + Lemma lel_nil : forall l' : list A, lel l' nil -> nil = l'. Proof. intro l'; elim l'; auto with arith. intros a' y H H0. @@ -1554,42 +1581,42 @@ Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: Section SetIncl. - Variable A : Type. + Variable (A : Type). - Definition incl (l m:list A) := forall a:A, In a l -> In a m. + Definition incl (l m : list A) := forall a : A, In a l -> In a m. Hint Unfold incl. - Lemma incl_refl : forall l:list A, incl l l. + Lemma incl_refl : forall l : list A, incl l l. Proof. auto. Qed. Hint Resolve incl_refl. - Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m). + Lemma incl_tl : forall (a : A) (l m : list A), incl l m -> incl l (a :: m). Proof. auto with datatypes. Qed. Hint Immediate incl_tl. - Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n. + Lemma incl_tran : forall l m n : list A, incl l m -> incl m n -> incl l n. Proof. auto. Qed. - Lemma incl_appl : forall l m n:list A, incl l n -> incl l (n ++ m). + Lemma incl_appl : forall l m n : list A, incl l n -> incl l (n ++ m). Proof. auto with datatypes. Qed. Hint Immediate incl_appl. - Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n). + Lemma incl_appr : forall l m n : list A, incl l n -> incl l (m ++ n). Proof. auto with datatypes. Qed. Hint Immediate incl_appr. Lemma incl_cons : - forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m. + forall (a : A) (l m : list A), In a m -> incl l m -> incl (a :: l) m. Proof. unfold incl; simpl; intros a l m H H0 a0 H1. now_show (In a0 m). @@ -1603,7 +1630,8 @@ Section SetIncl. Qed. Hint Resolve incl_cons. - Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. + Lemma incl_app : + forall l m n : list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. unfold incl; simpl; intros l m n H H0 a H1. now_show (In a n). @@ -1623,98 +1651,96 @@ Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons Section Cutting. - Variable A : Type. + Variable (A : Type). - Fixpoint firstn (n:nat)(l:list A) : list A := + Fixpoint firstn (n : nat) (l : list A) : list A := match n with - | 0 => nil - | S n => match l with - | nil => nil - | a::l => a::(firstn n l) - end + | 0 => nil + | S n => match l with + | nil => nil + | a :: l => a :: firstn n l + end end. - Lemma firstn_nil n: firstn n [] = []. - Proof. induction n; now simpl. Qed. + Lemma firstn_nil n : firstn n [] = []. + Proof. induction n; (now (simpl)). Qed. - Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l). - Proof. now simpl. Qed. + Lemma firstn_cons n a l : firstn (S n) (a :: l) = a :: firstn n l. + Proof. now (simpl). Qed. - Lemma firstn_all l: firstn (length l) l = l. - Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed. + Lemma firstn_all l : firstn (length l) l = l. + Proof. induction l as [| ? ? H]; simpl; [ reflexivity | now (rewrite H) ]. Qed. - Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. - Proof. induction n as [|k iHk]. - - intro. inversion 1 as [H1|?]. - rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - - destruct l as [|x xs]; simpl. + Lemma firstn_all2 n : forall l : list A, length l <= n -> firstn n l = l. + Proof. induction n as [| k iHk]. + - intro. inversion 1as [H1| ?]. + rewrite (length_zero_iff_nil l) in H1. subst. now (simpl). + - destruct l as [| x xs]; simpl. * now reflexivity. * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. Qed. - Lemma firstn_O l: firstn 0 l = []. - Proof. now simpl. Qed. + Lemma firstn_O l : firstn 0 l = []. + Proof. now (simpl). Qed. - Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. + Lemma firstn_le_length n : forall l : list A, length (firstn n l) <= n. Proof. - induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl]. + induction n as [| k iHk]; simpl; [ auto | destruct l as [| x xs]; simpl ]. - auto with arith. - apply Peano.le_n_S, iHk. Qed. - Lemma firstn_length_le: forall l:list A, forall n:nat, - n <= length l -> length (firstn n l) = n. - Proof. induction l as [|x xs Hrec]. - - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + Lemma firstn_length_le : + forall (l : list A) (n : nat), n <= length l -> length (firstn n l) = n. + Proof. induction l as [| x xs Hrec]. + - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now (simpl). - destruct n. - * now simpl. - * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + * now (simpl). + * simpl. intro H. apply le_S_n in H. now (rewrite (Hrec n H)). Qed. - Lemma firstn_app n: + Lemma firstn_app n : forall l1 l2, - firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2). - Proof. induction n as [|k iHk]; intros l1 l2. - - now simpl. - - destruct l1 as [|x xs]. - * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O. + firstn n (l1 ++ l2) = firstn n l1 ++ firstn (n - length l1) l2. + Proof. induction n as [| k iHk]; intros l1 l2. + - now (simpl). + - destruct l1 as [| x xs]. + * unfold firstn at 2, length. now (rewrite 2!app_nil_l, <- minus_n_O). * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. Qed. - Lemma firstn_app_2 n: - forall l1 l2, - firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2. - Proof. induction n as [| k iHk];intros l1 l2. + Lemma firstn_app_2 n : + forall l1 l2, firstn (length l1 + n) (l1 ++ l2) = l1 ++ firstn n l2. + Proof. induction n as [| k iHk]; intros l1 l2. - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r. rewrite firstn_app. rewrite <- minus_diag_reverse. unfold firstn at 2. rewrite app_nil_r. apply firstn_all. - - destruct l2 as [|x xs]. + - destruct l2 as [| x xs]. * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith. - * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). + * rewrite firstn_app. assert (H0 : length l1 + S k - length l1 = S k). auto with arith. - rewrite H0, firstn_all2; [reflexivity | auto with arith]. + rewrite H0, firstn_all2; [ reflexivity | auto with arith ]. Qed. - Lemma firstn_firstn: - forall l:list A, - forall i j : nat, + Lemma firstn_firstn : + forall (l : list A) (i j : nat), firstn i (firstn j l) = firstn (min i j) l. - Proof. induction l as [|x xs Hl]. - - intros. simpl. now rewrite ?firstn_nil. + Proof. induction l as [| x xs Hl]. + - intros **. simpl. now (rewrite ?firstn_nil). - destruct i. - * intro. now simpl. + * intro. now (simpl). * destruct j. - + now simpl. + + now (simpl). + simpl. f_equal. apply Hl. Qed. - Fixpoint skipn (n:nat)(l:list A) : list A := + Fixpoint skipn (n : nat) (l : list A) : list A := match n with - | 0 => l - | S n => match l with - | nil => nil - | a::l => skipn n l - end + | 0 => l + | S n => match l with + | nil => nil + | a :: l => skipn n l + end end. Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l. @@ -1730,17 +1756,17 @@ Section Cutting. induction n; destruct l; simpl; auto. Qed. - Lemma removelast_firstn : forall n l, n < length l -> - removelast (firstn (S n) l) = firstn n l. + Lemma removelast_firstn : + forall n l, n < length l -> removelast (firstn (S n) l) = firstn n l. Proof. induction n; destruct l. simpl; auto. simpl; auto. simpl; auto. - intros. + intros **. simpl in H. - change (firstn (S (S n)) (a::l)) with ((a::nil)++firstn (S n) l). - change (firstn (S n) (a::l)) with (a::firstn n l). + change (firstn (S (S n)) (a :: l)) with ((a :: nil) ++ firstn (S n) l). + change (firstn (S n) (a :: l)) with (a :: firstn n l). rewrite removelast_app. rewrite IHn; auto with arith. @@ -1749,16 +1775,16 @@ Section Cutting. inversion_clear H0. Qed. - Lemma firstn_removelast : forall n l, n < length l -> - firstn n (removelast l) = firstn n l. + Lemma firstn_removelast : + forall n l, n < length l -> firstn n (removelast l) = firstn n l. Proof. induction n; destruct l. simpl; auto. simpl; auto. simpl; auto. - intros. + intros **. simpl in H. - change (removelast (a :: l)) with (removelast ((a::nil)++l)). + change (removelast (a :: l)) with (removelast ((a :: nil) ++ l)). rewrite removelast_app. simpl; f_equal; auto with arith. intro H0; rewrite H0 in H; inversion_clear H; inversion_clear H1. @@ -1772,32 +1798,31 @@ End Cutting. Section Add. - Variable A : Type. + Variable (A : Type). (* [Add a l l'] means that [l'] is exactly [l], with [a] added once somewhere *) - Inductive Add (a:A) : list A -> list A -> Prop := - | Add_head l : Add a l (a::l) - | Add_cons x l l' : Add a l l' -> Add a (x::l) (x::l'). + Inductive Add (a : A) : list A -> list A -> Prop := + | Add_head : forall l, Add a l (a :: l) + | Add_cons : forall x l l', Add a l l' -> Add a (x :: l) (x :: l'). - Lemma Add_app a l1 l2 : Add a (l1++l2) (l1++a::l2). + Lemma Add_app a l1 l2 : Add a (l1 ++ l2) (l1 ++ a :: l2). Proof. - induction l1; simpl; now constructor. + induction l1; simpl; (now (constructor)). Qed. Lemma Add_split a l l' : - Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2. + Add a l l' -> exists l1 l2, l = l1 ++ l2 /\ l' = l1 ++ a :: l2. Proof. induction 1. - exists nil; exists l; split; trivial. - - destruct IHAdd as (l1 & l2 & Hl & Hl'). - exists (x::l1); exists l2; split; simpl; f_equal; trivial. + - destruct IHAdd as (l1, (l2, (Hl, Hl'))). + exists (x :: l1); exists l2; split; simpl; f_equal; trivial. Qed. - Lemma Add_in a l l' : Add a l l' -> - forall x, In x l' <-> In x (a::l). + Lemma Add_in a l l' : Add a l l' -> forall x, In x l' <-> In x (a :: l). Proof. - induction 1; intros; simpl in *; rewrite ?IHAdd; tauto. + induction 1; intros **; simpl in *; rewrite ?IHAdd; tauto. Qed. Lemma Add_length a l l' : Add a l l' -> length l' = S (length l). @@ -1807,17 +1832,17 @@ Section Add. Lemma Add_inv a l : In a l -> exists l', Add a l' l. Proof. - intro Ha. destruct (in_split _ _ Ha) as (l1 & l2 & ->). + intro Ha. destruct (in_split _ _ Ha) as (l1, (l2, ->)). exists (l1 ++ l2). apply Add_app. Qed. Lemma incl_Add_inv a l u v : - ~In a l -> incl (a::l) v -> Add a u v -> incl l u. + ~ In a l -> incl (a :: l) v -> Add a u v -> incl l u. Proof. intros Ha H AD y Hy. - assert (Hy' : In y (a::u)). + assert (Hy' : In y (a :: u)). { rewrite <- (Add_in AD). apply H; simpl; auto. } - destruct Hy'; [ subst; now elim Ha | trivial ]. + destruct Hy'; [ subst; (now (elim Ha)) | trivial ]. Qed. End Add. @@ -1828,111 +1853,110 @@ End Add. Section ReDun. - Variable A : Type. + Variable (A : Type). Inductive NoDup : list A -> Prop := | NoDup_nil : NoDup nil - | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). + | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x :: l). - Lemma NoDup_Add a l l' : Add a l l' -> (NoDup l' <-> NoDup l /\ ~In a l). + Lemma NoDup_Add a l l' : Add a l l' -> NoDup l' <-> NoDup l /\ ~ In a l. Proof. - induction 1 as [l|x l l' AD IH]. - - split; [ inversion_clear 1; now split | now constructor ]. + induction 1 as [l| x l l' AD IH]. + - split; [ inversion_clear 1; (now split) | now (constructor) ]. - split. + inversion_clear 1. rewrite IH in *. rewrite (Add_in AD) in *. simpl in *; split; try constructor; intuition. - + intros (N,IN). inversion_clear N. constructor. + + intros (N, IN). inversion_clear N. constructor. * rewrite (Add_in AD); simpl in *; intuition. * apply IH. split; trivial. simpl in *; intuition. Qed. Lemma NoDup_remove l l' a : - NoDup (l++a::l') -> NoDup (l++l') /\ ~In a (l++l'). + NoDup (l ++ a :: l') -> NoDup (l ++ l') /\ ~ In a (l ++ l'). Proof. apply NoDup_Add. apply Add_app. Qed. - Lemma NoDup_remove_1 l l' a : NoDup (l++a::l') -> NoDup (l++l'). + Lemma NoDup_remove_1 l l' a : NoDup (l ++ a :: l') -> NoDup (l ++ l'). Proof. - intros. now apply NoDup_remove with a. + intros **. now (apply NoDup_remove with a). Qed. - Lemma NoDup_remove_2 l l' a : NoDup (l++a::l') -> ~In a (l++l'). + Lemma NoDup_remove_2 l l' a : NoDup (l ++ a :: l') -> ~ In a (l ++ l'). Proof. - intros. now apply NoDup_remove. + intros **. now (apply NoDup_remove). Qed. - Theorem NoDup_cons_iff a l: - NoDup (a::l) <-> ~ In a l /\ NoDup l. + Theorem NoDup_cons_iff a l : NoDup (a :: l) <-> ~ In a l /\ NoDup l. Proof. split. + inversion_clear 1. now split. - + now constructor. + + now (constructor). Qed. (** Effective computation of a list without duplicates *) - Hypothesis decA: forall x y : A, {x = y} + {x <> y}. + Hypothesis (decA : forall x y : A, {x = y} + {x <> y}). Fixpoint nodup (l : list A) : list A := match l with - | [] => [] - | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs) + | [] => [] + | x :: xs => if in_dec decA x xs then nodup xs else x :: nodup xs end. Lemma nodup_In l x : In x (nodup l) <-> In x l. Proof. - induction l as [|a l' Hrec]; simpl. + induction l as [| a l' Hrec]; simpl. - reflexivity. - destruct (in_dec decA a l'); simpl; rewrite Hrec. - * intuition; now subst. + * intuition; (now (subst)). * reflexivity. Qed. - Lemma NoDup_nodup l: NoDup (nodup l). + Lemma NoDup_nodup l : NoDup (nodup l). Proof. - induction l as [|a l' Hrec]; simpl. + induction l as [| a l' Hrec]; simpl. - constructor. - destruct (in_dec decA a l'); simpl. * assumption. - * constructor; [ now rewrite nodup_In | assumption]. + * constructor; [ now (rewrite nodup_In) | assumption ]. Qed. Lemma nodup_inv k l a : nodup k = a :: l -> ~ In a l. Proof. intros H. - assert (H' : NoDup (a::l)). + assert (H' : NoDup (a :: l)). { rewrite <- H. apply NoDup_nodup. } - now inversion_clear H'. + now (inversion_clear H'). Qed. - Theorem NoDup_count_occ l: - NoDup l <-> (forall x:A, count_occ decA l x <= 1). + Theorem NoDup_count_occ l : + NoDup l <-> (forall x : A, count_occ decA l x <= 1). Proof. induction l as [| a l' Hrec]. - simpl; split; auto. constructor. - rewrite NoDup_cons_iff, Hrec, (count_occ_not_In decA). clear Hrec. split. + intros (Ha, H) x. simpl. destruct (decA a x); auto. - subst; now rewrite Ha. + subst; (now (rewrite Ha)). + split. * specialize (H a). rewrite count_occ_cons_eq in H; trivial. - now inversion H. + now (inversion H). * intros x. specialize (H x). simpl in *. destruct (decA a x); auto. - now apply Nat.lt_le_incl. + now (apply Nat.lt_le_incl). Qed. - Theorem NoDup_count_occ' l: - NoDup l <-> (forall x:A, In x l -> count_occ decA l x = 1). + Theorem NoDup_count_occ' l : + NoDup l <-> (forall x : A, In x l -> count_occ decA l x = 1). Proof. rewrite NoDup_count_occ. setoid_rewrite (count_occ_In decA). unfold gt, lt in *. - split; intros H x; specialize (H x); - set (n := count_occ decA l x) in *; clearbody n. + split; intros H x; specialize (H x); set (n := count_occ decA l x) in *; + clearbody n. (* the rest would be solved by omega if we had it here... *) - - now apply Nat.le_antisymm. + - now (apply Nat.le_antisymm). - destruct (Nat.le_gt_cases 1 n); trivial. + rewrite H; trivial. - + now apply Nat.lt_le_incl. + + now (apply Nat.lt_le_incl). Qed. (** Alternative characterisations of being without duplicates, @@ -1940,18 +1964,18 @@ Section ReDun. Lemma NoDup_nth_error l : NoDup l <-> - (forall i j, i<length l -> nth_error l i = nth_error l j -> i = j). + (forall i j, i < length l -> nth_error l i = nth_error l j -> i = j). Proof. split. - { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi E. + { intros H; induction H as [| a l Hal Hl IH]; intros i j Hi E. - inversion Hi. - destruct i, j; simpl in *; auto. * elim Hal. eapply nth_error_In; eauto. * elim Hal. eapply nth_error_In; eauto. * f_equal. apply IH; auto with arith. } - { induction l as [|a l]; intros H; constructor. - * intro Ha. apply In_nth_error in Ha. destruct Ha as (n,Hn). - assert (n < length l) by (now rewrite <- nth_error_Some, Hn). + { induction l as [| a l]; intros H; constructor. + * intro Ha. apply In_nth_error in Ha. destruct Ha as (n, Hn). + assert (n < length l) by (now (rewrite <- nth_error_Some, Hn)). specialize (H 0 (S n)). simpl in H. discriminate H; auto with arith. * apply IHl. intros i j Hi E. apply eq_add_S, H; simpl; auto with arith. } @@ -1959,18 +1983,18 @@ Section ReDun. Lemma NoDup_nth l d : NoDup l <-> - (forall i j, i<length l -> j<length l -> - nth i l d = nth j l d -> i = j). + (forall i j, + i < length l -> j < length l -> nth i l d = nth j l d -> i = j). Proof. split. - { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi Hj E. + { intros H; induction H as [| a l Hal Hl IH]; intros i j Hi Hj E. - inversion Hi. - destruct i, j; simpl in *; auto. * elim Hal. subst a. apply nth_In; auto with arith. * elim Hal. subst a. apply nth_In; auto with arith. * f_equal. apply IH; auto with arith. } - { induction l as [|a l]; intros H; constructor. - * intro Ha. eapply In_nth in Ha. destruct Ha as (n & Hn & Hn'). + { induction l as [| a l]; intros H; constructor. + * intro Ha. eapply In_nth in Ha. destruct Ha as (n, (Hn, Hn')). specialize (H 0 (S n)). simpl in H. discriminate H; eauto with arith. * apply IHl. intros i j Hi Hj E. apply eq_add_S, H; simpl; auto with arith. } @@ -1981,26 +2005,26 @@ Section ReDun. Lemma NoDup_incl_length l l' : NoDup l -> incl l l' -> length l <= length l'. Proof. - intros N. revert l'. induction N as [|a l Hal N IH]; simpl. + intros N. revert l'. induction N as [| a l Hal N IH]; simpl. - auto with arith. - intros l' H. destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } rewrite (Add_length AD). apply le_n_S. apply IH. - now apply incl_Add_inv with a l'. + now (apply incl_Add_inv with a l'). Qed. Lemma NoDup_length_incl l l' : NoDup l -> length l' <= length l -> incl l l' -> incl l' l. Proof. - intros N. revert l'. induction N as [|a l Hal N IH]. + intros N. revert l'. induction N as [| a l Hal N IH]. - destruct l'; easy. - intros l' E H x Hx. destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } rewrite (Add_in AD) in Hx. simpl in Hx. - destruct Hx as [Hx|Hx]; [left; trivial|right]. + destruct Hx as [Hx| Hx]; [ left; trivial | right ]. revert x Hx. apply (IH l''); trivial. - * apply le_S_n. now rewrite <- (Add_length AD). - * now apply incl_Add_inv with a l'. + * apply le_S_n. now (rewrite <- (Add_length AD)). + * now (apply incl_Add_inv with a l'). Qed. End ReDun. @@ -2010,10 +2034,10 @@ End ReDun. (** NB: the reciprocal result holds only for injective functions, see FinFun.v *) -Lemma NoDup_map_inv A B (f:A->B) l : NoDup (map f l) -> NoDup l. +Lemma NoDup_map_inv A B (f : A -> B) l : NoDup (map f l) -> NoDup l. Proof. induction l; simpl; inversion_clear 1; subst; constructor; auto. - intro H. now apply (in_map f) in H. + intro H. now (apply (in_map f) in H). Qed. (***********************************) @@ -2025,10 +2049,10 @@ Section NatSeq. (** [seq] computes the sequence of [len] contiguous integers that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *) - Fixpoint seq (start len:nat) : list nat := + Fixpoint seq (start len : nat) : list nat := match len with - | 0 => nil - | S len => start :: seq (S start) len + | 0 => nil + | S len => start :: seq (S start) len end. Lemma seq_length : forall len start, length (seq start len) = len. @@ -2036,41 +2060,41 @@ Section NatSeq. induction len; simpl; auto. Qed. - Lemma seq_nth : forall len start n d, - n < len -> nth n (seq start len) d = start+n. + Lemma seq_nth : + forall len start n d, n < len -> nth n (seq start len) d = start + n. Proof. - induction len; intros. + induction len; intros **. inversion H. simpl seq. destruct n; simpl. auto with arith. - rewrite IHlen;simpl; auto with arith. + rewrite IHlen; simpl; auto with arith. Qed. - Lemma seq_shift : forall len start, - map S (seq start len) = seq (S start) len. + Lemma seq_shift : + forall len start, map S (seq start len) = seq (S start) len. Proof. induction len; simpl; auto. - intros. + intros **. rewrite IHlen. auto with arith. Qed. Lemma in_seq len start n : - In n (seq start len) <-> start <= n < start+len. + In n (seq start len) <-> start <= n < start + len. Proof. - revert start. induction len; simpl; intros. - - rewrite <- plus_n_O. split;[easy|]. - intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). + revert start. induction len; simpl; intros **. + - rewrite <- plus_n_O. split; [ easy | ]. + intros (H, H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - rewrite IHlen, <- plus_n_Sm; simpl; split. - * intros [H|H]; subst; intuition auto with arith. - * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. + * intros [H| H]; subst; (intuition (auto with arith)). + * intros (H, H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. Qed. Lemma seq_NoDup len start : NoDup (seq start len). Proof. revert start; induction len; simpl; constructor; trivial. - rewrite in_seq. intros (H,_). apply (Lt.lt_irrefl _ H). + rewrite in_seq. intros (H, _). apply (Lt.lt_irrefl _ H). Qed. End NatSeq. @@ -2079,20 +2103,19 @@ Section Exists_Forall. (** * Existential and universal predicates over lists *) - Variable A:Type. + Variable (A : Type). Section One_predicate. - Variable P:A->Prop. + Variable (P : A -> Prop). Inductive Exists : list A -> Prop := - | Exists_cons_hd : forall x l, P x -> Exists (x::l) - | Exists_cons_tl : forall x l, Exists l -> Exists (x::l). + | Exists_cons_hd : forall x l, P x -> Exists (x :: l) + | Exists_cons_tl : forall x l, Exists l -> Exists (x :: l). Hint Constructors Exists. - Lemma Exists_exists (l:list A) : - Exists l <-> (exists x, In x l /\ P x). + Lemma Exists_exists (l : list A) : Exists l <-> (exists x, In x l /\ P x). Proof. split. - induction 1; firstorder. @@ -2102,97 +2125,95 @@ Section Exists_Forall. Lemma Exists_nil : Exists nil <-> False. Proof. split; inversion 1. Qed. - Lemma Exists_cons x l: - Exists (x::l) <-> P x \/ Exists l. + Lemma Exists_cons x l : Exists (x :: l) <-> P x \/ Exists l. Proof. split; inversion 1; auto. Qed. - Lemma Exists_dec l: - (forall x:A, {P x} + { ~ P x }) -> - {Exists l} + {~ Exists l}. + Lemma Exists_dec l : + (forall x : A, {P x} + {~ P x}) -> {Exists l} + {~ Exists l}. Proof. - intro Pdec. induction l as [|a l' Hrec]. - - right. now rewrite Exists_nil. - - destruct Hrec as [Hl'|Hl']. - * left. now apply Exists_cons_tl. - * destruct (Pdec a) as [Ha|Ha]. - + left. now apply Exists_cons_hd. - + right. now inversion_clear 1. + intro Pdec. induction l as [| a l' Hrec]. + - right. now (rewrite Exists_nil). + - destruct Hrec as [Hl'| Hl']. + * left. now (apply Exists_cons_tl). + * destruct (Pdec a) as [Ha| Ha]. + + left. now (apply Exists_cons_hd). + + right. now (inversion_clear 1). Qed. Inductive Forall : list A -> Prop := | Forall_nil : Forall nil - | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). + | Forall_cons : forall x l, P x -> Forall l -> Forall (x :: l). Hint Constructors Forall. - Lemma Forall_forall (l:list A): - Forall l <-> (forall x, In x l -> P x). + Lemma Forall_forall (l : list A) : Forall l <-> (forall x, In x l -> P x). Proof. split. - induction 1; firstorder; subst; auto. - induction l; firstorder. Qed. - Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a. + Lemma Forall_inv : forall (a : A) l, Forall (a :: l) -> P a. Proof. - intros; inversion H; trivial. + intros **; inversion H; trivial. Qed. - Lemma Forall_rect : forall (Q : list A -> Type), + Lemma Forall_rect : + forall Q : list A -> Type, Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l. Proof. - intros Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption. + intros Q H H'; induction l; intro; [ | eapply H', Forall_inv ]; + eassumption. Qed. Lemma Forall_dec : - (forall x:A, {P x} + { ~ P x }) -> - forall l:list A, {Forall l} + {~ Forall l}. + (forall x : A, {P x} + {~ P x}) -> + forall l : list A, {Forall l} + {~ Forall l}. Proof. - intro Pdec. induction l as [|a l' Hrec]. + intro Pdec. induction l as [| a l' Hrec]. - left. apply Forall_nil. - - destruct Hrec as [Hl'|Hl']. - + destruct (Pdec a) as [Ha|Ha]. - * left. now apply Forall_cons. - * right. now inversion_clear 1. - + right. now inversion_clear 1. + - destruct Hrec as [Hl'| Hl']. + + destruct (Pdec a) as [Ha| Ha]. + * left. now (apply Forall_cons). + * right. now (inversion_clear 1). + + right. now (inversion_clear 1). Qed. End One_predicate. - Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : - Forall (fun x => ~ P x) l <-> ~(Exists P l). + Lemma Forall_Exists_neg (P : A -> Prop) (l : list A) : + Forall (fun x => ~ P x) l <-> ~ Exists P l. Proof. rewrite Forall_forall, Exists_exists. firstorder. Qed. - Lemma Exists_Forall_neg (P:A->Prop)(l:list A) : - (forall x, P x \/ ~P x) -> - Exists (fun x => ~ P x) l <-> ~(Forall P l). + Lemma Exists_Forall_neg (P : A -> Prop) (l : list A) : + (forall x, P x \/ ~ P x) -> Exists (fun x => ~ P x) l <-> ~ Forall P l. Proof. intro Dec. split. - rewrite Forall_forall, Exists_exists; firstorder. - intros NF. - induction l as [|a l IH]. + induction l as [| a l IH]. + destruct NF. constructor. - + destruct (Dec a) as [Ha|Ha]. - * apply Exists_cons_tl, IH. contradict NF. now constructor. - * now apply Exists_cons_hd. + + destruct (Dec a) as [Ha| Ha]. + * apply Exists_cons_tl, IH. contradict NF. now (constructor). + * now (apply Exists_cons_hd). Qed. - Lemma Forall_Exists_dec (P:A->Prop) : - (forall x:A, {P x} + { ~ P x }) -> - forall l:list A, - {Forall P l} + {Exists (fun x => ~ P x) l}. + Lemma Forall_Exists_dec (P : A -> Prop) : + (forall x : A, {P x} + {~ P x}) -> + forall l : list A, {Forall P l} + {Exists (fun x => ~ P x) l}. Proof. intros Pdec l. - destruct (Forall_dec P Pdec l); [left|right]; trivial. + destruct (Forall_dec P Pdec l); [ left | right ]; trivial. apply Exists_Forall_neg; trivial. - intro x. destruct (Pdec x); [now left|now right]. + intro x. destruct (Pdec x); [ now left | now right ]. Qed. - Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> - forall l, Forall P l -> Forall Q l. + Lemma Forall_impl : + forall P Q : A -> Prop, + (forall a, P a -> Q a) -> forall l, Forall P l -> Forall Q l. Proof. intros P Q H l. rewrite !Forall_forall. firstorder. Qed. @@ -2206,45 +2227,48 @@ Section Forall2. (** [Forall2]: stating that elements of two lists are pairwise related. *) - Variables A B : Type. - Variable R : A -> B -> Prop. + Variables (A B : Type). + Variable (R : A -> B -> Prop). Inductive Forall2 : list A -> list B -> Prop := | Forall2_nil : Forall2 [] [] - | Forall2_cons : forall x y l l', - R x y -> Forall2 l l' -> Forall2 (x::l) (y::l'). + | Forall2_cons : + forall x y l l', R x y -> Forall2 l l' -> Forall2 (x :: l) (y :: l'). Hint Constructors Forall2. Theorem Forall2_refl : Forall2 [] []. - Proof. intros; apply Forall2_nil. Qed. + Proof. intros **; apply Forall2_nil. Qed. - Theorem Forall2_app_inv_l : forall l1 l2 l', + Theorem Forall2_app_inv_l : + forall l1 l2 l', Forall2 (l1 ++ l2) l' -> exists l1' l2', Forall2 l1 l1' /\ Forall2 l2 l2' /\ l' = l1' ++ l2'. Proof. - induction l1; intros. - exists [], l'; auto. + induction l1; intros **. + exists []; exists l'; auto. simpl in H; inversion H; subst; clear H. - apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->). - exists (y::l1'), l2'; simpl; auto. + apply IHl1 in H4 as (l1', (l2', (Hl1, (Hl2, ->)))). + exists (y :: l1'); exists l2'; simpl; auto. Qed. - Theorem Forall2_app_inv_r : forall l1' l2' l, + Theorem Forall2_app_inv_r : + forall l1' l2' l, Forall2 l (l1' ++ l2') -> exists l1 l2, Forall2 l1 l1' /\ Forall2 l2 l2' /\ l = l1 ++ l2. Proof. - induction l1'; intros. - exists [], l; auto. + induction l1'; intros **. + exists []; exists l; auto. simpl in H; inversion H; subst; clear H. - apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->). - exists (x::l1), l2; simpl; auto. + apply IHl1' in H4 as (l1, (l2, (Hl1, (Hl2, ->)))). + exists (x :: l1); exists l2; simpl; auto. Qed. - Theorem Forall2_app : forall l1 l2 l1' l2', + Theorem Forall2_app : + forall l1 l2 l1' l2', Forall2 l1 l1' -> Forall2 l2 l2' -> Forall2 (l1 ++ l2) (l1' ++ l2'). Proof. - intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto. + intros **. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto. Qed. End Forall2. @@ -2255,25 +2279,26 @@ Section ForallPairs. (** [ForallPairs] : specifies that a certain relation should always hold when inspecting all possible pairs of elements of a list. *) - Variable A : Type. - Variable R : A -> A -> Prop. + Variable (A : Type). + Variable (R : A -> A -> Prop). - Definition ForallPairs l := - forall a b, In a l -> In b l -> R a b. + Definition ForallPairs l := forall a b, In a l -> In b l -> R a b. (** [ForallOrdPairs] : we still check a relation over all pairs of elements of a list, but now the order of elements matters. *) Inductive ForallOrdPairs : list A -> Prop := | FOP_nil : ForallOrdPairs nil - | FOP_cons : forall a l, - Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l). + | FOP_cons : + forall a l, + Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a :: l). Hint Constructors ForallOrdPairs. - Lemma ForallOrdPairs_In : forall l, + Lemma ForallOrdPairs_In : + forall l, ForallOrdPairs l -> - forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x. + forall x y, In x l -> In y l -> x = y \/ R x y \/ R y x. Proof. induction 1. inversion 1. @@ -2285,12 +2310,12 @@ Section ForallPairs. (** [ForallPairs] implies [ForallOrdPairs]. The reverse implication is true only when [R] is symmetric and reflexive. *) - Lemma ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs l. + Lemma ForallPairs_ForallOrdPairs l : ForallPairs l -> ForallOrdPairs l. Proof. induction l; auto. intros H. constructor. - apply <- Forall_forall. intros; apply H; simpl; auto. - apply IHl. red; intros; apply H; simpl; auto. + apply <- Forall_forall. intros **; apply H; simpl; auto. + apply IHl. red; intros **; apply H; simpl; auto. Qed. Lemma ForallOrdPairs_ForallPairs : @@ -2305,22 +2330,24 @@ End ForallPairs. (** * Inversion of predicates over lists based on head symbol *) -Ltac is_list_constr c := - match c with +Ltac + is_list_constr c := + match c with | nil => idtac - | (_::_) => idtac + | _ :: _ => idtac | _ => fail - end. + end. -Ltac invlist f := - match goal with +Ltac + invlist f := + match goal with | H:f ?l |- _ => is_list_constr l; inversion_clear H; invlist f | H:f _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f | H:f _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f | H:f _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f | H:f _ _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f | _ => idtac - end. + end. @@ -2328,15 +2355,15 @@ Ltac invlist f := Hint Rewrite - rev_involutive (* rev (rev l) = l *) - rev_unit (* rev (l ++ a :: nil) = a :: rev l *) - map_nth (* nth n (map f l) (f d) = f (nth n l d) *) - map_length (* length (map f l) = length l *) - seq_length (* length (seq start len) = len *) - app_length (* length (l ++ l') = length l + length l' *) - rev_length (* length (rev l) = length l *) - app_nil_r (* l ++ nil = l *) - : list. + rev_involutive (* rev (rev l) = l *) + rev_unit (* rev (l ++ a :: nil) = a :: rev l *) + map_nth (* nth n (map f l) (f d) = f (nth n l d) *) + map_length (* length (map f l) = length l *) + seq_length (* length (seq start len) = len *) + app_length (* length (l ++ l') = length l + length l' *) + rev_length (* length (rev l) = length l *) + app_nil_r (* l ++ nil = l *) + : list. Ltac simpl_list := autorewrite with list. Ltac ssimpl_list := autorewrite with list using simpl. @@ -2366,28 +2393,26 @@ Notation rev_acc := rev_append (only parsing). Notation rev_acc_rev := rev_append_rev (only parsing). Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) -Hint Resolve app_nil_end : datatypes v62. +Hint Resolve app_nil_end: datatypes v62. (* end hide *) Section Repeat. - Variable A : Type. - Fixpoint repeat (x : A) (n: nat ) := + Variable (A : Type). + Fixpoint repeat (x : A) (n : nat) := match n with - | O => [] - | S k => x::(repeat x k) + | O => [] + | S k => x :: repeat x k end. - Theorem repeat_length x n: - length (repeat x n) = n. + Theorem repeat_length x n : length (repeat x n) = n. Proof. induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. Qed. - Theorem repeat_spec n x y: - In y (repeat x n) -> y=x. + Theorem repeat_spec n x y : In y (repeat x n) -> y = x. Proof. - induction n as [|k Hrec]; simpl; destruct 1; auto. + induction n as [| k Hrec]; simpl; destruct 1; auto. Qed. End Repeat. |