aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Lists/List.v1381
-rw-r--r--theories/MSets/MSetGenTree.v12
-rw-r--r--theories/MSets/MSetList.v10
-rw-r--r--theories/Reals/PSeries_reg.v2
-rw-r--r--theories/Structures/EqualitiesFacts.v2
5 files changed, 716 insertions, 691 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.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 154c2384c..4f5b6cde4 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -983,7 +983,7 @@ Proof.
apply (StrictOrder_Irreflexive (elements s2)); auto.
intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
(s2'' & s3' & B2' & B3 & E2' & E3 & L23).
- exists s1', s3'; do 4 (split; trivial).
+ exists s1'; exists s3'; do 4 (split; trivial).
assert (eqlistA X.eq (elements s2') (elements s2'')).
apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
rewrite <- eq_Leq. transitivity s2; auto. symmetry; auto.
@@ -995,11 +995,11 @@ Instance lt_compat : Proper (eq==>eq==>iff) lt.
Proof.
intros s1 s2 E12 s3 s4 E34. split.
intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
- exists s1', s3'; do 2 (split; trivial).
+ exists s1'; exists s3'; do 2 (split; trivial).
split. transitivity s1; auto. symmetry; auto.
split; auto. transitivity s3; auto. symmetry; auto.
intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
- exists s1', s3'; do 2 (split; trivial).
+ exists s1'; exists s3'; do 2 (split; trivial).
split. transitivity s2; auto.
split; auto. transitivity s4; auto.
Qed.
@@ -1079,8 +1079,8 @@ Proof.
intros.
destruct (compare_Cmp s1 s2); constructor.
rewrite eq_Leq; auto.
- intros; exists s1, s2; repeat split; auto.
- intros; exists s2, s1; repeat split; auto.
+ intros; exists s1; exists s2; repeat split; auto.
+ intros; exists s2; exists s1; repeat split; auto.
Qed.
@@ -1144,4 +1144,4 @@ Proof.
apply mindepth_cardinal.
Qed.
-End Props. \ No newline at end of file
+End Props.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index fb0d1ad9d..4c0ce86b4 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -795,7 +795,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
apply (StrictOrder_Irreflexive s2); auto.
intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
(s2'' & s3' & B2' & B3 & E2' & E3 & L23).
- exists s1', s3'.
+ exists s1'; exists s3'.
repeat rewrite <- isok_iff in *.
do 4 (split; trivial).
assert (eqlistA X.eq s2' s2'').
@@ -809,11 +809,11 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
intros s1 s2 E12 s3 s4 E34. split.
intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
- exists s1', s3'; do 2 (split; trivial).
+ exists s1'; exists s3'; do 2 (split; trivial).
split. transitivity s1; auto. symmetry; auto.
split; auto. transitivity s3; auto. symmetry; auto.
intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
- exists s1', s3'; do 2 (split; trivial).
+ exists s1'; exists s3'; do 2 (split; trivial).
split. transitivity s2; auto.
split; auto. transitivity s4; auto.
Qed.
@@ -829,8 +829,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
intros s s' Hs Hs'.
destruct (compare_spec_aux s s'); constructor; auto.
- exists s, s'; repeat split; auto using @ok.
- exists s', s; repeat split; auto using @ok.
+ exists s; exists s'; repeat split; auto using @ok.
+ exists s'; exists s; repeat split; auto using @ok.
Qed.
End MakeRaw.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index 03ac6582b..3d29a5bbf 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -54,7 +54,7 @@ rewrite Rplus_comm; apply Rplus_lt_compat_l, Rmult_lt_compat_r.
apply Rlt_trans with z; assumption.
destruct (boule_of_interval _ _ cmp) as [c [r [P1 P2]]].
assert (0 < /2) by (apply Rinv_0_lt_compat, Rlt_0_2).
-exists c, r; split.
+exists c; exists r; split.
destruct h; unfold Boule; simpl; apply Rabs_def1.
apply Rplus_lt_reg_l with c; rewrite P2;
replace (c + (z - c)) with (z * / 2 + z * / 2) by field.
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index cee3d63f0..ece8db5b7 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -110,7 +110,7 @@ Module KeyDecidableType(D:DecidableType).
unfold In, MapsTo.
setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
firstorder.
- exists (snd x), x; auto.
+ exists (snd x); exists x; auto.
Qed.
Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False.